Theory LTL_Rabin_Impl

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Executable Translation from LTL to Rabin Automata›

theory LTL_Rabin_Impl
  imports Main "../Auxiliary/Map2" "../LTL_Rabin" "../LTL_Rabin_Unfold_Opt" af_Impl Mojmir_Rabin_Impl
begin

subsection ‹Template›

subsubsection ‹Definition›

locale ltl_to_rabin_base_code_def = ltl_to_rabin_base_def +
  fixes
    M_finC :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltlP × ('a ltl, 'a ltlP list) mapping, 'a set) transition ⇒ bool"
begin

― ‹Transition Function and Initial State›

fun deltaC
where
  "deltaC Σ = δ × ↑Δ× (nxt Σ δM o q0M o theG)"

fun initialC
where
  "initialC φ = (q0 φ, Mapping.tabulate (G_list φ) (init o q0M o theG))"

― ‹Acceptance Condition›

definition max_rank_ofC
where
  "max_rank_ofC Σ ψ = card (Set.filter (Not o semi_mojmir_def.sink (set Σ) δM (q0M (theG ψ))) (QL Σ δM (q0M (theG ψ))))"

fun Acc_finC
where
  "Acc_finC Σ π χ ((_, m'), ν, _) = (
    let 
      t = (the (Mapping.lookup m' χ), ν, []); ― ‹Third element is unused. Hence it is safe to pass a dummy value.›
      𝒢 = Mapping.keys π
    in 
      fail_filt Σ δM (q0M (theG χ)) (ltl_prop_entails_abs 𝒢) t 
    ∨ merge_filt δM (q0M (theG χ)) (ltl_prop_entails_abs 𝒢) (the (Mapping.lookup π χ)) t)"

fun Acc_infC
where
  "Acc_infC π χ ((_, m'), ν, _) = (
    let 
      t = (the (Mapping.lookup m' χ), ν, []); ― ‹Third element is unused. Hence it is safe to pass a dummy value.›
      𝒢 = Mapping.keys π
    in 
      succeed_filt δM (q0M (theG χ)) (ltl_prop_entails_abs 𝒢) (the (Mapping.lookup π χ)) t)"

definition mappingsC :: "'a set list ⇒ 'a ltl ⇒ ('a ltl, nat) mapping set"
where
  "mappingsC Σ φ ≡ {π. Mapping.keys π ⊆ G φ ∧ (∀χ ∈ (Mapping.keys π). the (Mapping.lookup π χ) < max_rank_ofC Σ χ)}"

definition reachable_transitionsC
where
  "reachable_transitionsC Σ φ ≡ δL Σ (deltaC (set Σ)) (initialC φ)"

fun ltl_to_generalized_rabinC
where
  "ltl_to_generalized_rabinC Σ φ = (
    let
      δ_LTS = reachable_transitionsC Σ φ; 
      α_fin_filter = λπ t. M_finC φ π t ∨ (∃χ ∈ Mapping.keys π. Acc_finC (set Σ) π χ t);
      to_pair = λπ. (Set.filter (α_fin_filter π) δ_LTS, (λχ. Set.filter (Acc_infC π χ) δ_LTS) ` Mapping.keys π);
      α = to_pair ` (mappingsC Σ φ) ― ‹Multi-thread here!, prove ‹mappings (set …)› equation›
    in
      (δ_LTS, initialC φ, α))"

lemma mappingsC_code:
  "mappingsC Σ φ = (
    let 
      Gs = G_list φ; 
      max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_ofC Σ))
    in 
      set (concat (map (mapping_generator_list (λx. [0 ..< the (max_rank x)])) (subseqs Gs))))"
  (is "?lhs = ?rhs")
proof -
  {
    fix xs :: "'a ltl list"
    have subset_G: "⋀x. x ∈ set (subseqs (xs)) ⟹ set x ⊆ set xs"
      apply (induction xs)
      apply (simp)
      by (insert subseqs_powset; blast)
  }
  hence subset_G: "⋀x. x ∈ set (subseqs (G_list φ)) ⟹ set x ⊆ G φ"
    unfolding G_eq_G_list by auto

  have "?lhs = ⋃{{π. Mapping.keys π = xs ∧ (∀χ∈Mapping.keys π. the (Mapping.lookup π χ) < max_rank_ofC Σ χ)} | xs. xs ∈ set ` (set (subseqs (G_list φ)))}"
    unfolding mappingsC_def G_eq_G_list subseqs_powset by auto
  also
  have "… = ⋃{{π. Mapping.keys π = set xs ∧ (∀χ ∈ set xs. the (Mapping.lookup π χ) < max_rank_ofC Σ χ)} |
       xs. xs ∈ set (subseqs (G_list φ))}"
    by auto
  also
  have "… = ?rhs"
    using subset_G 
      by (auto simp add: Let_def mapping_generator_code [symmetric]
        lookup_tabulate G_eq_G_list [symmetric] mapping_generator_set_eq
        cong del: SUP_cong_simp; blast)
  finally
  show ?thesis
    by simp
qed

lemma reach_delta_initial:
  assumes "(x, y) ∈ reach Σ (deltaC Σ) (initialC φ)"
  assumes "χ ∈ G φ"
  shows "Mapping.lookup y χ ≠ None" (is ?t1)
    and "distinct (the (Mapping.lookup y χ))" (is ?t2)
proof -
  from assms(1) obtain w i where y_def: "y = run (↑Δ× (nxt Σ δM o q0M o theG)) (Mapping.tabulate (G_list φ) (init o q0M o theG)) w i"
    unfolding reach_def deltaC.simps initialC.simps simple_product_run by fast
  from assms(2) nxt_run_distinct show ?t1 
    unfolding y_def using product_abs_run_Some[of "Mapping.tabulate (G_list φ) (init o q0M o theG)" χ] unfolding G_eq_G_list 
    unfolding lookup_tabulate by fastforce
  with nxt_run_distinct show ?t2
    unfolding y_def using lookup_tabulate  
    by (metis (no_types) G_eq_G_list assms(2) comp_eq_dest_lhs option.sel product_abs_run_Some) 
qed

end

subsubsection ‹Correctness›

fun abstract_state :: "'x × ('y, 'z list) mapping ⇒ 'x × ('y ⇀ 'z ⇀ nat)" 
where
  "abstract_state (a, b) = (a, (map_option rk) o (Mapping.lookup b))"

fun abstract_transition
where
  "abstract_transition (q, ν, q') = (abstract_state q, ν, abstract_state q')"

locale ltl_to_rabin_base_code = ltl_to_rabin_base + ltl_to_rabin_base_code_def + 
  assumes 
    M_finC_correct: "⟦t ∈ reacht Σ (deltaC Σ) (initialC φ); dom π ⊆ G φ⟧ ⟹
      abstract_transition t ∈ M_fin π = M_finC φ (Mapping.Mapping π) t"
begin

lemma finite_reachC:
  "finite (reacht Σ (deltaC Σ) (initialC φ))"
proof -
  note finite_reach'
  moreover
  have "(⋀x. x ∈ G φ ⟹ finite (reach Σ ((nxt Σ δM o q0M o theG) x) ((init o q0M o theG) x)))"
    using semi_mojmir.finite_Q[OF semi_mojmir] unfolding G_eq_G_list semi_mojmir_def.QE_def by simp 
  hence "finite (reach Σ (↑Δ× (nxt Σ δM o q0M o theG)) (Mapping.tabulate (G_list φ) (init o q0M o theG)))"
    by (metis (no_types) finite_reach_product_abs[OF finite_keys_tabulate] G_eq_G_list  keys_tabulate lookup_tabulate_Some)
  ultimately
  have "finite (reach Σ (deltaC Σ) (initialC φ))"
    using finite_reach_simple_product by fastforce 
  thus ?thesis
    using finite_Σ by (simp add: finite_reacht) 
qed 

lemma max_rank_ofC_eq:
  assumes "Σ = set Σ'"
  shows "max_rank_ofC Σ' ψ = max_rank_of Σ ψ"
proof -
  interpret 𝔐: semi_mojmir "set Σ'" δM "q0M (theG ψ)" w
    using semi_mojmir assms by force
  show ?thesis
    unfolding max_rank_of_def max_rank_ofC_def QL_reach[OF 𝔐.finite_reach] semi_mojmir_def.max_rank_def
    by (simp add: Set.filter_def set_diff_eq assms)
qed

lemma reachable_transitionsC_eq:
  assumes "Σ = set Σ'"
  shows "reachable_transitionsC Σ' φ = reacht Σ (deltaC Σ) (initialC φ)"
  by (simp only: reachable_transitionsC_def δL_reach[OF finite_reachC[unfolded assms]] assms)

lemma run_abstraction_correct:
  "run (delta Σ) (initial φ) w = abstract_state o (run (deltaC Σ) (initialC φ) w)"
proof -
  {
    fix i

    let ?δ2 = "Δ× (λχ. semi_mojmir_def.step Σ δM (q0M (theG χ)))"
    let ?q2 = "ι× (G φ) (λχ. semi_mojmir_def.initial (q0M (theG χ)))"

    let ?δ2' = "↑Δ× (nxt Σ δM o q0M o theG)"    
    let ?q2' = "Mapping.tabulate (G_list φ) (init o q0M o theG)"
    
    {
      fix q
      assume "q ∉ G φ"
      hence "?q2 q = None" and "Mapping.lookup (run ?δ2' ?q2' w i) q = None"
        using G_eq_G_list product_abs_run_None by (simp, metis domIff keys_dom_lookup keys_tabulate)
      hence "run ?δ2 ?q2 w i q = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ2' ?q2' w i) q"
        using product_run_None by (simp del: nxt.simps rk.simps)
    }

    moreover 

    {
      fix q j
      assume "q ∈ G φ"
      hence init: "?q2 q = Some (semi_mojmir_def.initial (q0M (theG q)))" 
        and "Mapping.lookup (run ?δ2' ?q2' w i) q = Some (run ((nxt Σ δM ∘ q0M ∘ theG) q) ((init ∘ q0M ∘ theG) q) w i)"
        apply (simp del: nxt.simps)  
        apply (metis G_eq_G_list ‹q ∈ G φ› lookup_tabulate product_abs_run_Some) 
        done
      hence "run ?δ2 ?q2 w i q = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ2' ?q2' w i) q"
        unfolding product_run_Some[of "ι× (G φ) (λχ. semi_mojmir_def.initial (q0M (theG χ)))" q, OF init] 
        by (simp del: product.simps nxt.simps rk.simps; unfold map_of_map semi_mojmir.nxt_run_step_run[OF semi_mojmir]; simp) 
    }

    ultimately

    have "run ?δ2 ?q2 w i = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ2' ?q2' w i)"
      by blast
  }
  hence "⋀i. run (delta Σ) (initial φ) w i = abstract_state (run (deltaC Σ) (initialC φ) w i)"
    using finite_Σ bounded_w by (simp add: simple_product_run comp_def del: simple_product.simps)
  thus ?thesis
    by auto
qed

lemma 
  assumes "t ∈ reacht Σ (deltaC Σ) (initialC φ)"
  assumes "χ ∈ G φ"
  shows Acc_finC_correct: 
    "abstract_transition t ∈ Acc_fin Σ π χ ⟷ Acc_finC Σ (Mapping.Mapping π) χ t" (is ?t1)
    and Acc_infC_correct: 
    "abstract_transition t ∈ Acc_inf π χ ⟷ Acc_infC (Mapping.Mapping π) χ t" (is ?t2)
proof -
  obtain x y ν z z' where t_def [simp]: "t = ((x, y), ν, (z, z'))"
    by (metis prod.collapse)
  have "(x, y) ∈ reach Σ (deltaC Σ) (initialC φ)"
    and "(z, z') ∈ reach Σ (deltaC Σ) (initialC φ)"
    using assms(1) unfolding reacht_def reach_def runt.simps t_def by blast+
  then obtain m m' where [simp]: "Mapping.lookup y χ = Some m" 
    and "Mapping.lookup y χ ≠ None" 
    and [simp]: "Mapping.lookup z' χ = Some m'"
    using assms(2) by (blast dest: reach_delta_initial)+

  have FF [simp]: "fail_filt Σ δM (q0M (theG χ)) (ltl_prop_entails_abs (dom π)) (the (Mapping.lookup y χ), ν, []) 
    = ((the (map_option rk (Mapping.lookup y χ)), ν, (λx. Some 0)) ∈ mojmir_to_rabin_def.failR Σ δM (q0M (theG χ)) {q. dom π ↑⊨P q})"
    unfolding option.map_sel[OF ‹Mapping.lookup y χ ≠ None›] fail_filt_eq[where y = "[]", symmetric] by simp  

  have MF [simp]: "⋀i. merge_filt δM (q0M (theG χ)) (ltl_prop_entails_abs (dom π)) i (the (Mapping.lookup y χ), ν, [])
    = ((the (map_option rk (Mapping.lookup y χ)), ν, (λx. Some 0)) ∈ mojmir_to_rabin_def.mergeR δM (q0M (theG χ)) {q. dom π ↑⊨P q} i)"
    unfolding option.map_sel[OF ‹Mapping.lookup y χ ≠ None›] merge_filt_eq[where y = "[]", symmetric] by simp  

  have SF [simp]: "⋀i. succeed_filt δM (q0M (theG χ)) (ltl_prop_entails_abs (dom π)) i (the (Mapping.lookup y χ), ν, [])
    = ((the (map_option rk (Mapping.lookup y χ)), ν, (λx. Some 0)) ∈ mojmir_to_rabin_def.succeedR δM (q0M (theG χ)) {q. dom π ↑⊨P q} i)"
    unfolding option.map_sel[OF ‹Mapping.lookup y χ ≠ None›] succeed_filt_eq[where y = "[]", symmetric] by simp  

  note mojmir_to_rabin_def.failR_def [simp] 
  note mojmir_to_rabin_def.mergeR_def [simp]
  note mojmir_to_rabin_def.succeedR_def [simp]

  show ?t1 and ?t2 
    by (simp_all add: Let_def keys.abs_eq lookup.abs_eq del: rk.simps) 
       (rule; metis option.distinct(1) option.sel option.collapse rk_facts(1))+
qed


theorem ltl_to_generalized_rabinC_correct:
  assumes "Σ = set Σ'"
  shows "acceptGR (ltl_to_generalized_rabin Σ φ) w ⟷ acceptGR_LTS (ltl_to_generalized_rabinC Σ' φ) w" 
  (is "?lhs ⟷ ?rhs")
proof
  let ?δ = "delta Σ"
  let ?q0 = "initial φ"
 
  let ?δC = "deltaC Σ"
  let ?q0C = "initialC φ"
  let ?reachC = "reacht Σ (deltaC Σ) (initialC φ)"

  note reachable_transitionsC_simp[simp] = reachable_transitionsC_eq[OF assms] 
  note max_rank_ofC_simp[simp] = max_rank_ofC_eq[OF assms]

  {
    fix π :: "'a ltl ⇒ nat option"
    assume π_wellformed: "dom π ⊆ G φ"
       
    let ?F = "(M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π})"
    let ?fin = "{t. M_finC φ (Mapping.Mapping π) t} ∪ {t. ∃χ ∈ dom π. Acc_finC Σ (Mapping.Mapping π) χ t}"
    let ?inf = "{{t. Acc_infC (Mapping.Mapping π) χ t} | χ. χ ∈ dom π}"
    
    have finite_reach': "finite (reacht Σ (delta Σ) (initial φ))"
      by (meson finite_reach finite_Σ finite_reacht) 

    have run_abstraction_correct': 
      "runt (delta Σ) (initial φ) w = abstract_transition o (runt (deltaC Σ) (initialC φ) w)"
      using run_abstraction_correct comp_def by auto

    have "accepting_pairGR ?δ ?q0 ?F w ⟷ accepting_pairGR ?δC  ?q0C (?fin, ?inf) w" (is "?l ⟷ _")
      by (rule accepting_pairGR_abstract[OF finite_reach' finite_reachC bounded_w];
          insert ‹dom π ⊆ G φ› M_finC_correct Acc_finC_correct Acc_infC_correct run_abstraction_correct'; blast)
    also 
    have "… ⟷ accepting_pairGR_LTS ?reachC ?q0C (?fin ∩ ?reachC, (λI. I ∩ ?reachC) ` ?inf) w" (is "_ ⟷ ?r")
      using bounded_w by (simp only: accepting_pairGR_LTS[symmetric] accepting_pairGR_restrict[symmetric])
    finally
    have "?l ⟷ ?r" .
  }
 
  note X = this

  {
    assume ?lhs
    then obtain π where 1: "dom π ⊆ G φ" 
      and 2: "⋀χ. χ ∈ dom π ⟹ the (π χ) < max_rank_of Σ χ"
      and 3: "accepting_pairGR (delta Σ) (initial φ) (M_fin π ∪ ⋃{Acc_fin Σ π χ |χ. χ ∈ dom π}, {Acc_inf π χ |χ. χ ∈ dom π}) w" 
      by auto
    
    define π' where "π' = Mapping.Mapping π"
    
    have "dom π = Mapping.keys π'" and "π = Mapping.lookup π'"
      by (simp_all add: keys.abs_eq lookup.abs_eq π'_def)

    have acc_pair_LTS: "accepting_pairGR_LTS ?reachC ?q0C (({t. M_finC φ π' t} ∪ {t. ∃χ ∈ Mapping.keys π'. Acc_finC Σ π' χ t}) ∩ ?reachC,
        (λI. I ∩ ?reachC) ` {{t. Acc_infC π' χ t} | χ. χ ∈ Mapping.keys π'}) w"
      using 3 unfolding X[OF 1] unfolding ‹dom π = Mapping.keys π'› π'_def[symmetric] by simp

    show ?rhs
      apply (unfold ltl_to_generalized_rabinC.simps Let_def)
      apply (intro acceptGR_LTS_I)
      apply (insert acc_pair_LTS; auto simp add: assms[symmetric] mappingsC_def)
      apply (insert 1 2; unfold  ‹dom π = Mapping.keys π'›; unfold ‹π = Mapping.lookup π'›)
      by (auto simp add: assms[symmetric] Set.filter_def image_def mappingsC_def)
  }
  
  moreover 

  {
    assume ?rhs
    obtain Fin Inf where "(Fin, Inf) ∈ snd (snd (ltl_to_generalized_rabinC Σ' φ))"
      and 4: "accepting_pairGR_LTS ?reachC (initialC φ) (Fin, Inf) w"
       using acceptGR_LTS_E[OF ‹?rhs›] apply (simp add: Let_def assms del: acceptGR_LTS.simps) by auto
    
    then obtain π where Y: "(Fin, Inf) = (Set.filter (λt. M_finC φ π t ∨ (∃χ ∈ Mapping.keys π. Acc_finC Σ π χ t)) ?reachC,
        (λχ. Set.filter (Acc_infC π χ) ?reachC) ` (Mapping.keys π))"
        and 1: "Mapping.keys π ⊆ G φ" and 2: "⋀χ. χ ∈ Mapping.keys π ⟹ the (Mapping.lookup π χ) < max_rank_of Σ χ"
      unfolding ltl_to_generalized_rabinC.simps Let_def fst_conv snd_conv mappingsC_def assms reachable_transitionsC_simp max_rank_ofC_simp by auto
    define π' where "π' = Mapping.rep π"
    have "dom π' = Mapping.keys π" and "Mapping.Mapping π' = π"
      by (simp_all add: π'_def mapping.rep_inverse keys.rep_eq)
    have 1: "dom π' ⊆ G φ" and 2: "⋀χ. χ ∈ dom π' ⟹ the (π' χ) < max_rank_of Σ χ"
      using 1 2 unfolding  π'_def Mapping.keys.rep_eq Mapping.mapping.rep_inverse by (simp add: lookup.rep_eq)+
    moreover
    have "({a ∈ reacht Σ (deltaC Σ) (initialC φ). M_finC φ π a ∨ (∃χ∈Mapping.keys π. Acc_finC Σ π χ a)}, {y. ∃x∈Mapping.keys π. y = {a ∈ reacht Σ (deltaC Σ) (initialC φ). Acc_infC π x a}})
      = ((Collect (M_finC φ π) ∪ {t. ∃χ∈Mapping.keys π. Acc_finC Σ π χ t}) ∩ reacht Σ (deltaC Σ) (initialC φ), {y. ∃x∈{Collect (Acc_infC π χ) |χ. χ ∈ Mapping.keys π}. y = x ∩ reacht Σ (deltaC Σ) (initialC φ)})" 
      by auto
    hence "accepting_pairGR (delta Σ) (initial φ) (M_fin π' ∪ ⋃{Acc_fin Σ π' χ | χ. χ ∈ dom π'}, {Acc_inf π' χ | χ. χ ∈ dom π'}) w"
      unfolding X[OF 1] using 4 unfolding Y Set.filter_def unfolding ‹dom π' = Mapping.keys π› ‹Mapping.Mapping π' = π› image_def by simp    
    ultimately
    show ?lhs  
      unfolding ltl_to_generalized_rabin.simps
      by (intro Rabin.acceptGR_I, blast; auto) 
  }
qed

end 

subsection ‹Generalized Deterministic Rabin Automaton (af)›

definition M_finC_af_lhs :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltl, ('a ltlP list)) mapping ⇒ 'a ltlP"
where
  "M_finC_af_lhs φ π m' ≡ 
    let
      𝒢 = Mapping.keys π;
      𝒢L = filter (λx. x ∈ 𝒢) (G_list φ);
      mk_conj = λχ. foldl and_abs (Abs χ) (map (↑evalG 𝒢) (drop (the (Mapping.lookup π χ)) (the (Mapping.lookup m' χ))))
    in 
      ↑And (map mk_conj 𝒢L)"

fun M_finC_af :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltlP × (('a ltl, ('a ltlP list)) mapping), 'a set) transition ⇒ bool"
where
  "M_finC_af φ π ((φ', m'), _) = Not ((M_finC_af_lhs φ π m') ↑⟶P  φ')"

lemma M_finC_af_correct:
  assumes "t ∈ reacht Σ (ltl_to_rabin_base_code_def.deltaC ↑af ↑afG Abs Σ) (ltl_to_rabin_base_code_def.initialC Abs Abs φ)"
  assumes "dom π ⊆ G φ"
  shows "abstract_transition t ∈ M_fin π = M_finC_af φ (Mapping.Mapping π) t"
proof -
  let ?delta = "ltl_to_rabin_base_code_def.deltaC ↑af ↑afG Abs Σ"
  let ?initial = "ltl_to_rabin_base_code_def.initialC Abs Abs φ"
  
  obtain x y ν z z' where t_def [simp]: "t = ((x, y), ν, (z, z'))"
    by (metis prod.collapse)
  have "(x, y) ∈ reach Σ ?delta ?initial"
    using assms(1) by (simp add: reacht_def reach_def; blast)
  hence N1: "⋀χ. χ ∈ dom π ⟹ Mapping.lookup y χ ≠ None"
    and D1: "⋀χ. χ ∈ dom π ⟹ distinct (the (Mapping.lookup y χ))"
    using assms(2) by (blast dest: ltl_to_rabin_base_code_def.reach_delta_initial)+

  {
    fix S
    let ?m' = "λχ. map_option rk (Mapping.lookup y χ)"
    
    {
      fix χ
      assume "χ ∈ dom π"
      hence "S ↑⊨P (foldl and_abs (Abs χ) (map (↑evalG (dom π)) (drop (the (π χ)) (the (Mapping.lookup y χ)))))
         ⟷ S ↑⊨P (Abs χ) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨P ↑evalG (dom π) q)"
        using D1[THEN drop_rk, of _ "the (π χ)"] N1[THEN option.map_sel, of _ rk]
        by (auto simp add: foldl_LTLAnd_prop_entailment_abs)
    }

    hence "S ↑⊨P (M_finC_af_lhs φ (Mapping.Mapping π) y)
      ⟷ (∀χ ∈ dom π. S ↑⊨P (Abs χ) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨P ↑evalG (dom π) q))"
      unfolding M_finC_af_lhs_def Let_def And_prop_entailment_abs set_map Ball_def keys.abs_eq lookup.abs_eq 
      using assms(2) by (simp add: image_def inter_set_filter[symmetric] G_eq_G_list[symmetric]; blast)
  }
  thus ?thesis
    by (simp add: ltl_prop_implies_def ltl_prop_implies_abs_def ltl_prop_entails_abs_def)
qed 

definition 
  "ltl_to_generalized_rabinC_af ≡ ltl_to_rabin_base_code_def.ltl_to_generalized_rabinC ↑af ↑afG Abs Abs M_finC_af"

theorem ltl_to_generalized_rabinC_af_correct:
  assumes "range w ⊆ set Σ"
  shows "w ⊨ φ ⟷ acceptGR_LTS (ltl_to_generalized_rabinC_af Σ φ) w" 
  (is "?lhs ⟷ ?rhs")
proof -
  have X: "ltl_to_rabin_base_code ↑af ↑afG Abs Abs M_fin (set Σ) w M_finC_af"
    using ltl_to_generalized_rabin_af_wellformed[OF finite_set assms] M_finC_af_correct assms
    unfolding ltl_to_rabin_af_def ltl_to_rabin_base_code_def ltl_to_rabin_base_code_axioms_def by blast
  have "?lhs ⟷ acceptGR (ltl_to_generalized_rabin_af (set Σ) φ) w"
    using assms ltl_to_generalized_rabin_af_correct by auto
  also 
  have "… ⟷ ?rhs"
    using ltl_to_rabin_base_code.ltl_to_generalized_rabinC_correct[OF X]
    unfolding ltl_to_generalized_rabinC_af_def by simp
  finally
  show ?thesis .
qed

subsection ‹Generalized Deterministic Rabin Automaton (eager af)›

definition M_finC_af𝔘_lhs :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltl, ('a ltlP list)) mapping ⇒ 'a set ⇒ 'a ltlP"
where
  "M_finC_af𝔘_lhs φ π m' ν ≡ 
    let
      𝒢 = Mapping.keys π;
      𝒢L = filter (λx. x ∈ 𝒢) (G_list φ);
      mk_conj = λχ. foldl and_abs (and_abs (Abs χ) (↑evalG 𝒢 (Abs (theG χ)))) (map (↑evalG 𝒢 o (λq. ↑step q ν)) (drop (the (Mapping.lookup π χ)) (the (Mapping.lookup m' χ))))
    in 
      ↑And (map mk_conj 𝒢L)"

fun M_finC_af𝔘 :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltlP × (('a ltl, ('a ltlP list)) mapping), 'a set) transition ⇒ bool"
where
  "M_finC_af𝔘 φ π ((φ', m'), ν, _) = Not ((M_finC_af𝔘_lhs φ π m' ν) ↑⟶P (↑step φ' ν))"

lemma M_finC_af𝔘_correct:
  assumes "t ∈ reacht Σ (ltl_to_rabin_base_code_def.deltaC ↑af𝔘 ↑afG𝔘 (Abs ∘ UnfG) Σ) (ltl_to_rabin_base_code_def.initialC (Abs ∘ Unf) (Abs ∘ UnfG) φ)"
  assumes "dom π ⊆ G φ"
  shows "abstract_transition t ∈ M𝔘_fin π = M_finC_af𝔘 φ (Mapping.Mapping π) t"
proof -
  let ?delta = "ltl_to_rabin_base_code_def.deltaC ↑af𝔘 ↑afG𝔘 (Abs ∘ UnfG) Σ"
  let ?initial = "ltl_to_rabin_base_code_def.initialC (Abs ∘ Unf) (Abs ∘ UnfG) φ"
  
  obtain x y ν z z' where t_def [simp]: "t = ((x, y), ν, (z, z'))"
    by (metis prod.collapse)
  have "(x, y) ∈ reach Σ ?delta ?initial"
    using assms(1) by (simp add: reacht_def reach_def; blast)
  hence N1: "⋀χ. χ ∈ dom π ⟹ Mapping.lookup y χ ≠ None"
    and D1: "⋀χ. χ ∈ dom π ⟹ distinct (the (Mapping.lookup y χ))"
    using assms(2) by (blast dest: ltl_to_rabin_base_code_def.reach_delta_initial)+

  {
    fix S
    let ?m' = "λχ. map_option rk (Mapping.lookup y χ)"
    
    {
      fix χ
      assume "χ ∈ dom π"
      hence "S ↑⊨P (foldl and_abs (and_abs (Abs χ) (↑evalG (dom π) (Abs (theG χ)))) (map (↑evalG (dom π) o (λq. ↑step q ν)) (drop (the (π χ)) (the (Mapping.lookup y χ)))))
         ⟷ S ↑⊨P Abs χ ∧ S ↑⊨P ↑evalG (dom π) (Abs (theG χ)) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨P ↑evalG (dom π) (↑step q ν))"
        using D1[THEN drop_rk, of _ "the (π χ)"] N1[THEN option.map_sel, of _ rk]
        by (auto simp add: foldl_LTLAnd_prop_entailment_abs and_abs_conjunction simp del: rk.simps)
    }

    hence "S ↑⊨P (M_finC_af𝔘_lhs φ (Mapping.Mapping π) y ν)
      ⟷ ((∀χ ∈ dom π. (S ↑⊨P Abs χ ∧ S ↑⊨P ↑evalG (dom π) (Abs (theG χ)) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨P ↑evalG (dom π) (↑step q ν)))))"
      unfolding M_finC_af𝔘_lhs_def Let_def And_prop_entailment_abs set_map Ball_def keys.abs_eq lookup.abs_eq 
      using assms(2) by (simp add: image_def inter_set_filter[symmetric] G_eq_G_list[symmetric]; blast)
  }
  thus ?thesis
    by (simp add: ltl_prop_implies_def ltl_prop_implies_abs_def ltl_prop_entails_abs_def)
qed 

definition 
  "ltl_to_generalized_rabinC_af𝔘 ≡ ltl_to_rabin_base_code_def.ltl_to_generalized_rabinC ↑af𝔘 ↑afG𝔘 (Abs ∘ Unf) (Abs ∘ UnfG) M_finC_af𝔘"

theorem ltl_to_generalized_rabinC_af𝔘_correct:
  assumes "range w ⊆ set Σ"
  shows "w ⊨ φ ⟷ acceptGR_LTS (ltl_to_generalized_rabinC_af𝔘 Σ φ) w" 
  (is "?lhs ⟷ ?rhs")
proof -
  have X: "ltl_to_rabin_base_code ↑af𝔘 ↑afG𝔘 (Abs ∘ Unf) (Abs ∘ UnfG) M𝔘_fin (set Σ) w M_finC_af𝔘"
    using ltl_to_generalized_rabin_af𝔘_wellformed[OF finite_set assms] M_finC_af𝔘_correct assms
    unfolding ltl_to_rabin_af_unf_def ltl_to_rabin_base_code_def ltl_to_rabin_base_code_axioms_def by blast
  have "?lhs ⟷ acceptGR (ltl_to_generalized_rabin_af𝔘 (set Σ) φ) w"
    using assms ltl_to_generalized_rabin_af𝔘_correct by auto
  also 
  have "… ⟷ ?rhs"
    using ltl_to_rabin_base_code.ltl_to_generalized_rabinC_correct[OF X]
    unfolding ltl_to_generalized_rabinC_af𝔘_def by simp
  finally
  show ?thesis .
qed

end