Theory Export_Code

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Code Generation›

theory Export_Code
  imports Main LTL_Compat LTL_Rabin_Impl 
    "HOL-Library.AList_Mapping" (* Future, Performance: Replace by LC *) 
    LTL.Rewriting
    "HOL-Library.Code_Target_Numeral" 
begin

subsection ‹External Interface›

― ‹Fix the type to match the type of the LTL parser›

definition 
  "ltlc_to_rabin eager mode (φ⇩_c :: String.literal ltlc) ≡
    (let
      φ⇩_n = ltlc_to_ltln φ⇩_c;
      Σ = map set (subseqs (atoms_list φ⇩_n));
      φ = ltln_to_ltl (simplify mode φ⇩_n)
     in
      (if eager then ltl_to_generalized_rabin⇩_C_af⇩_𝔘 Σ φ else ltl_to_generalized_rabin⇩_C_af Σ φ))"

theorem ltlc_to_rabin_exec_correct:
  assumes "range w ⊆ Pow (atoms_ltlc φ⇩_c)"
  shows "w ⊨⇩_c φ⇩_c ⟷ accept⇩_G⇩_R_LTS (ltlc_to_rabin eager mode φ⇩_c) w" 
  (is "?lhs = ?rhs")
proof -
  let ?φ⇩_n = "ltlc_to_ltln φ⇩_c"
  let ?Σ = "map set (subseqs (atoms_list ?φ⇩_n))"
  let ?φ = "ltln_to_ltl (simplify mode ?φ⇩_n)"

  have "set ?Σ = Pow (atoms_ltln ?φ⇩_n)"
    unfolding atoms_list_correct[symmetric] subseqs_powset[symmetric] list.set_map ..  
  hence R: "range w ⊆ set ?Σ"
    using assms ltlc_to_ltln_atoms[symmetric] by metis

  have "w ⊨⇩_c φ⇩_c ⟷ w ⊨ ?φ"
    by (simp only: ltlc_to_ltln_semantics simplify_correct ltln_to_ltl_semantics)
  also
  have "… ⟷ ?rhs"
    using ltl_to_generalized_rabin⇩_C_af⇩_𝔘_correct[OF R] ltl_to_generalized_rabin⇩_C_af_correct[OF R] 
    unfolding ltlc_to_rabin_def Let_def by auto
  finally
  show ?thesis
    by simp
qed

subsection ‹Normalize Equivalence Classes During DFS-Search›

fun norm_rep
where
  "norm_rep (i, (q, ν, p)) (q', ν', p') = (
    let 
      eq_q = (q = q'); eq_p = (p = p');
      q'' = if eq_q then q' else if q = p' then p' else q;
      p'' = if eq_p then p' else if p = q' then q' else p
    in 
      (i | (eq_q & eq_p & ν = ν'), q'', ν, p''))"

fun norm_fold :: "('a, 'b) transition ⇒ ('a, 'b) transition list ⇒ (bool * 'a * 'b * 'a)"
where
  "norm_fold (q, ν, p) xs = foldl_break norm_rep fst (False, q, ν, if q = p then q else p) xs"

definition norm_insert :: "('a, 'b) transition ⇒ ('a, 'b) transition list ⇒ (bool * ('a, 'b) transition list)"
where
  "norm_insert x xs ≡ let (i, x') = norm_fold x xs in if i then (i, xs) else (i, x' # xs)" 

lemma norm_fold:
  "norm_fold (q, ν, p) xs = ((q, ν, p) ∈ set xs, q, ν, p)"
proof (induction xs rule: rev_induct)
  case (snoc x xs)
    obtain q' ν' p' where x_def: "x = (q', ν', p')"
      by (blast intro: prod_cases3)
    show ?case
      using snoc by (auto simp add: x_def foldl_break_append)
qed simp  

lemma norm_insert: 
  "norm_insert x xs = (x ∈ set xs, List.insert x xs)"
proof -
  obtain q ν p where x_def: "x = (q, ν, p)"
    by (blast intro: prod_cases3)
  show ?thesis
    unfolding x_def norm_insert_def norm_fold by simp
qed
 
declare list_dfs_def [code del]
declare norm_insert_def [code_unfold]

lemma list_dfs_norm_insert [code]: 
  "list_dfs succ S [] = S"
  "list_dfs succ S (x # xs) = (let (memb, S') = norm_insert x S in list_dfs succ S' (if memb then xs else succ x @ xs))"
  unfolding list_dfs_def Let_def norm_insert by simp+ 

subsection ‹Register Code Equations›

lemma [code]:
  "↑Δ⇩_× f (AList_Mapping.Mapping xs) c = AList_Mapping.Mapping (map_ran (λa b. f a b c) xs)"
proof -
  have "⋀x. (Δ⇩_× f (map_of xs) c) x = (map_of (map (λ(k, v). (k, f k v c)) xs)) x"
    by (induction xs) auto
  thus ?thesis
    by (transfer; simp add: map_ran_def)
qed

lemmas ltl_to_rabin_base_code_export [code, code_unfold] =
  ltl_to_rabin_base_code_def.ltl_to_generalized_rabin⇩_C.simps
  ltl_to_rabin_base_code_def.reachable_transitions⇩_C_def 
  ltl_to_rabin_base_code_def.mappings⇩_C_code 
  ltl_to_rabin_base_code_def.delta⇩_C.simps
  ltl_to_rabin_base_code_def.initial⇩_C.simps 
  ltl_to_rabin_base_code_def.Acc_inf⇩_C.simps 
  ltl_to_rabin_base_code_def.Acc_fin⇩_C.simps
  ltl_to_rabin_base_code_def.max_rank_of⇩_C_def

lemmas M_fin⇩_C_lhs [code del, code_unfold] = 
  M_fin⇩_C_af⇩_𝔘_lhs_def M_fin⇩_C_af_lhs_def 

― ‹Test code export›
export_code true⇩_c Iff_ltlc Nop true Abs AList_Mapping.Mapping set ltlc_to_rabin checking

― ‹Export translator (and also constructors)›
export_code true⇩_c Iff_ltlc Nop true Abs AList_Mapping.Mapping set ltlc_to_rabin 
  in SML module_name LTL file ‹../Code/LTL_to_DRA_Translator.sml›

end