# Theory LTL_Rabin_Impl

theory LTL_Rabin_Impl
imports LTL_Rabin_Unfold_Opt af_Impl Mojmir_Rabin_Impl
```(*
Author:      Salomon Sickert
*)

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_fin⇩C :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltl⇩P × ('a ltl, 'a ltl⇩P list) mapping, 'a set) transition ⇒ bool"
begin

― ‹Transition Function and Initial State›

fun delta⇩C
where
"delta⇩C Σ = δ × ↑Δ⇩× (nxt Σ δ⇩M o q⇩0⇩M o theG)"

fun initial⇩C
where
"initial⇩C φ = (q⇩0 φ, Mapping.tabulate (G_list φ) (init o q⇩0⇩M o theG))"

― ‹Acceptance Condition›

definition max_rank_of⇩C
where
"max_rank_of⇩C Σ ψ = card (Set.filter (Not o semi_mojmir_def.sink (set Σ) δ⇩M (q⇩0⇩M (theG ψ))) (Q⇩L Σ δ⇩M (q⇩0⇩M (theG ψ))))"

fun Acc_fin⇩C
where
"Acc_fin⇩C Σ π χ ((_, 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 (q⇩0⇩M (theG χ)) (ltl_prop_entails_abs 𝒢) t
∨ merge_filt δ⇩M (q⇩0⇩M (theG χ)) (ltl_prop_entails_abs 𝒢) (the (Mapping.lookup π χ)) t)"

fun Acc_inf⇩C
where
"Acc_inf⇩C π χ ((_, 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 (q⇩0⇩M (theG χ)) (ltl_prop_entails_abs 𝒢) (the (Mapping.lookup π χ)) t)"

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

definition reachable_transitions⇩C
where
"reachable_transitions⇩C Σ φ ≡ δ⇩L Σ (delta⇩C (set Σ)) (initial⇩C φ)"

fun ltl_to_generalized_rabin⇩C
where
"ltl_to_generalized_rabin⇩C Σ φ = (
let
δ_LTS = reachable_transitions⇩C Σ φ;
α_fin_filter = λπ t. M_fin⇩C φ π t ∨ (∃χ ∈ Mapping.keys π. Acc_fin⇩C (set Σ) π χ t);
to_pair = λπ. (Set.filter (α_fin_filter π) δ_LTS, (λχ. Set.filter (Acc_inf⇩C π χ) δ_LTS) ` Mapping.keys π);
α = to_pair ` (mappings⇩C Σ φ) ― ‹Multi-thread here!, prove ‹mappings (set …)› equation›
in
(δ_LTS, initial⇩C φ, α))"

lemma mappings⇩C_code:
"mappings⇩C Σ φ = (
let
Gs = G_list φ;
max_rank = Mapping.lookup (Mapping.tabulate Gs (max_rank_of⇩C Σ))
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_of⇩C Σ χ)} | xs. xs ∈ set ` (set (subseqs (G_list φ)))}"
unfolding mappings⇩C_def G_eq_G_list subseqs_powset by auto
also
have "… = ⋃{{π. Mapping.keys π = set xs ∧ (∀χ ∈ set xs. the (Mapping.lookup π χ) < max_rank_of⇩C Σ χ)} |
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 Σ (delta⇩C Σ) (initial⇩C φ)"
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 q⇩0⇩M o theG)) (Mapping.tabulate (G_list φ) (init o q⇩0⇩M o theG)) w i"
unfolding reach_def delta⇩C.simps initial⇩C.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 q⇩0⇩M 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_fin⇩C_correct: "⟦t ∈ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ); dom π ⊆ ❙G φ⟧ ⟹
abstract_transition t ∈ M_fin π = M_fin⇩C φ (Mapping.Mapping π) t"
begin

lemma finite_reach⇩C:
"finite (reach⇩t Σ (delta⇩C Σ) (initial⇩C φ))"
proof -
note finite_reach'
moreover
have "(⋀x. x ∈ ❙G φ ⟹ finite (reach Σ ((nxt Σ δ⇩M o q⇩0⇩M o theG) x) ((init o q⇩0⇩M o theG) x)))"
using semi_mojmir.finite_Q[OF semi_mojmir] unfolding G_eq_G_list semi_mojmir_def.Q⇩E_def by simp
hence "finite (reach Σ (↑Δ⇩× (nxt Σ δ⇩M o q⇩0⇩M o theG)) (Mapping.tabulate (G_list φ) (init o q⇩0⇩M 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 Σ (delta⇩C Σ) (initial⇩C φ))"
using finite_reach_simple_product by fastforce
thus ?thesis
using finite_Σ by (simp add: finite_reach⇩t)
qed

lemma max_rank_of⇩C_eq:
assumes "Σ = set Σ'"
shows "max_rank_of⇩C Σ' ψ = max_rank_of Σ ψ"
proof -
interpret 𝔐: semi_mojmir "set Σ'" δ⇩M "q⇩0⇩M (theG ψ)" w
using semi_mojmir assms by force
show ?thesis
unfolding max_rank_of_def max_rank_of⇩C_def Q⇩L_reach[OF 𝔐.finite_reach] semi_mojmir_def.max_rank_def
by (simp add: Set.filter_def set_diff_eq assms)
qed

lemma reachable_transitions⇩C_eq:
assumes "Σ = set Σ'"
shows "reachable_transitions⇩C Σ' φ = reach⇩t Σ (delta⇩C Σ) (initial⇩C φ)"
by (simp only: reachable_transitions⇩C_def δ⇩L_reach[OF finite_reach⇩C[unfolded assms]] assms)

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

let ?δ⇩2 = "Δ⇩× (λχ. semi_mojmir_def.step Σ δ⇩M (q⇩0⇩M (theG χ)))"
let ?q⇩2 = "ι⇩× (❙G φ) (λχ. semi_mojmir_def.initial (q⇩0⇩M (theG χ)))"

let ?δ⇩2' = "↑Δ⇩× (nxt Σ δ⇩M o q⇩0⇩M o theG)"
let ?q⇩2' = "Mapping.tabulate (G_list φ) (init o q⇩0⇩M o theG)"

{
fix q
assume "q ∉ ❙G φ"
hence "?q⇩2 q = None" and "Mapping.lookup (run ?δ⇩2' ?q⇩2' 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 ?q⇩2 w i q = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ⇩2' ?q⇩2' w i) q"
using product_run_None by (simp del: nxt.simps rk.simps)
}

moreover

{
fix q j
assume "q ∈ ❙G φ"
hence init: "?q⇩2 q = Some (semi_mojmir_def.initial (q⇩0⇩M (theG q)))"
and "Mapping.lookup (run ?δ⇩2' ?q⇩2' w i) q = Some (run ((nxt Σ δ⇩M ∘ q⇩0⇩M ∘ theG) q) ((init ∘ q⇩0⇩M ∘ 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 ?q⇩2 w i q = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ⇩2' ?q⇩2' w i) q"
unfolding product_run_Some[of "ι⇩× (❙G φ) (λχ. semi_mojmir_def.initial (q⇩0⇩M (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 ?q⇩2 w i = (λm. (map_option rk) o (Mapping.lookup m)) (run ?δ⇩2' ?q⇩2' w i)"
by blast
}
hence "⋀i. run (delta Σ) (initial φ) w i = abstract_state (run (delta⇩C Σ) (initial⇩C φ) 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 ∈ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ)"
assumes "χ ∈ ❙G φ"
shows Acc_fin⇩C_correct:
"abstract_transition t ∈ Acc_fin Σ π χ ⟷ Acc_fin⇩C Σ (Mapping.Mapping π) χ t" (is ?t1)
and Acc_inf⇩C_correct:
"abstract_transition t ∈ Acc_inf π χ ⟷ Acc_inf⇩C (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 Σ (delta⇩C Σ) (initial⇩C φ)"
and "(z, z') ∈ reach Σ (delta⇩C Σ) (initial⇩C φ)"
using assms(1) unfolding reach⇩t_def reach_def run⇩t.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 (q⇩0⇩M (theG χ)) (ltl_prop_entails_abs (dom π)) (the (Mapping.lookup y χ), ν, [])
= ((the (map_option rk (Mapping.lookup y χ)), ν, (λx. Some 0)) ∈ mojmir_to_rabin_def.fail⇩R Σ δ⇩M (q⇩0⇩M (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 (q⇩0⇩M (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.merge⇩R δ⇩M (q⇩0⇩M (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 (q⇩0⇩M (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.succeed⇩R δ⇩M (q⇩0⇩M (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.fail⇩R_def [simp]
note mojmir_to_rabin_def.merge⇩R_def [simp]
note mojmir_to_rabin_def.succeed⇩R_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_rabin⇩C_correct:
assumes "Σ = set Σ'"
shows "accept⇩G⇩R (ltl_to_generalized_rabin Σ φ) w ⟷ accept⇩G⇩R_LTS (ltl_to_generalized_rabin⇩C Σ' φ) w"
(is "?lhs ⟷ ?rhs")
proof
let ?δ = "delta Σ"
let ?q⇩0 = "initial φ"

let ?δ⇩C = "delta⇩C Σ"
let ?q⇩0⇩C = "initial⇩C φ"
let ?reach⇩C = "reach⇩t Σ (delta⇩C Σ) (initial⇩C φ)"

note reachable_transitions⇩C_simp[simp] = reachable_transitions⇩C_eq[OF assms]
note max_rank_of⇩C_simp[simp] = max_rank_of⇩C_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_fin⇩C φ (Mapping.Mapping π) t} ∪ {t. ∃χ ∈ dom π. Acc_fin⇩C Σ (Mapping.Mapping π) χ t}"
let ?inf = "{{t. Acc_inf⇩C (Mapping.Mapping π) χ t} | χ. χ ∈ dom π}"

have finite_reach': "finite (reach⇩t Σ (delta Σ) (initial φ))"
by (meson finite_reach finite_Σ finite_reach⇩t)

have run_abstraction_correct':
"run⇩t (delta Σ) (initial φ) w = abstract_transition o (run⇩t (delta⇩C Σ) (initial⇩C φ) w)"
using run_abstraction_correct comp_def by auto

have "accepting_pair⇩G⇩R ?δ ?q⇩0 ?F w ⟷ accepting_pair⇩G⇩R ?δ⇩C  ?q⇩0⇩C (?fin, ?inf) w" (is "?l ⟷ _")
by (rule accepting_pair⇩G⇩R_abstract[OF finite_reach' finite_reach⇩C bounded_w];
insert ‹dom π ⊆ ❙G φ› M_fin⇩C_correct Acc_fin⇩C_correct Acc_inf⇩C_correct run_abstraction_correct'; blast)
also
have "… ⟷ accepting_pair⇩G⇩R_LTS ?reach⇩C ?q⇩0⇩C (?fin ∩ ?reach⇩C, (λI. I ∩ ?reach⇩C) ` ?inf) w" (is "_ ⟷ ?r")
using bounded_w by (simp only: accepting_pair⇩G⇩R_LTS[symmetric] accepting_pair⇩G⇩R_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_pair⇩G⇩R (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_pair⇩G⇩R_LTS ?reach⇩C ?q⇩0⇩C (({t. M_fin⇩C φ π' t} ∪ {t. ∃χ ∈ Mapping.keys π'. Acc_fin⇩C Σ π' χ t}) ∩ ?reach⇩C,
(λI. I ∩ ?reach⇩C) ` {{t. Acc_inf⇩C π' χ 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_rabin⇩C.simps Let_def)
apply (intro accept⇩G⇩R_LTS_I)
apply (insert acc_pair_LTS; auto simp add: assms[symmetric] mappings⇩C_def)
apply (insert 1 2; unfold  ‹dom π = Mapping.keys π'›; unfold ‹π = Mapping.lookup π'›)
by (auto simp add: assms[symmetric] Set.filter_def image_def mappings⇩C_def)
}

moreover

{
assume ?rhs
obtain Fin Inf where "(Fin, Inf) ∈ snd (snd (ltl_to_generalized_rabin⇩C Σ' φ))"
and 4: "accepting_pair⇩G⇩R_LTS ?reach⇩C (initial⇩C φ) (Fin, Inf) w"
using accept⇩G⇩R_LTS_E[OF ‹?rhs›] apply (simp add: Let_def assms del: accept⇩G⇩R_LTS.simps) by auto

then obtain π where Y: "(Fin, Inf) = (Set.filter (λt. M_fin⇩C φ π t ∨ (∃χ ∈ Mapping.keys π. Acc_fin⇩C Σ π χ t)) ?reach⇩C,
(λχ. Set.filter (Acc_inf⇩C π χ) ?reach⇩C) ` (Mapping.keys π))"
and 1: "Mapping.keys π ⊆ ❙G φ" and 2: "⋀χ. χ ∈ Mapping.keys π ⟹ the (Mapping.lookup π χ) < max_rank_of Σ χ"
unfolding ltl_to_generalized_rabin⇩C.simps Let_def fst_conv snd_conv mappings⇩C_def assms reachable_transitions⇩C_simp max_rank_of⇩C_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 ∈ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ). M_fin⇩C φ π a ∨ (∃χ∈Mapping.keys π. Acc_fin⇩C Σ π χ a)}, {y. ∃x∈Mapping.keys π. y = {a ∈ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ). Acc_inf⇩C π x a}})
= ((Collect (M_fin⇩C φ π) ∪ {t. ∃χ∈Mapping.keys π. Acc_fin⇩C Σ π χ t}) ∩ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ), {y. ∃x∈{Collect (Acc_inf⇩C π χ) |χ. χ ∈ Mapping.keys π}. y = x ∩ reach⇩t Σ (delta⇩C Σ) (initial⇩C φ)})"
by auto
hence "accepting_pair⇩G⇩R (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.accept⇩G⇩R_I, blast; auto)
}
qed

end

subsection ‹Generalized Deterministic Rabin Automaton (af)›

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

fun M_fin⇩C_af :: "'a ltl ⇒ ('a ltl, nat) mapping ⇒ ('a ltl⇩P × (('a ltl, ('a ltl⇩P list)) mapping), 'a set) transition ⇒ bool"
where
"M_fin⇩C_af φ π ((φ', m'), _) = Not ((M_fin⇩C_af_lhs φ π m') ↑⟶⇩P  φ')"

lemma M_fin⇩C_af_correct:
assumes "t ∈ reach⇩t Σ (ltl_to_rabin_base_code_def.delta⇩C ↑af ↑af⇩G Abs Σ) (ltl_to_rabin_base_code_def.initial⇩C Abs Abs φ)"
assumes "dom π ⊆ ❙G φ"
shows "abstract_transition t ∈ M_fin π = M_fin⇩C_af φ (Mapping.Mapping π) t"
proof -
let ?delta = "ltl_to_rabin_base_code_def.delta⇩C ↑af ↑af⇩G Abs Σ"
let ?initial = "ltl_to_rabin_base_code_def.initial⇩C 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: reach⇩t_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 (↑eval⇩G (dom π)) (drop (the (π χ)) (the (Mapping.lookup y χ)))))
⟷ S ↑⊨⇩P (Abs χ) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G (dom π) q)"
using D1[THEN drop_rk, of _ "the (π χ)"] N1[THEN option.map_sel, of _ rk]
}

hence "S ↑⊨⇩P (M_fin⇩C_af_lhs φ (Mapping.Mapping π) y)
⟷ (∀χ ∈ dom π. S ↑⊨⇩P (Abs χ) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G (dom π) q))"
unfolding M_fin⇩C_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_rabin⇩C_af ≡ ltl_to_rabin_base_code_def.ltl_to_generalized_rabin⇩C ↑af ↑af⇩G Abs Abs M_fin⇩C_af"

theorem ltl_to_generalized_rabin⇩C_af_correct:
assumes "range w ⊆ set Σ"
shows "w ⊨ φ ⟷ accept⇩G⇩R_LTS (ltl_to_generalized_rabin⇩C_af Σ φ) w"
(is "?lhs ⟷ ?rhs")
proof -
have X: "ltl_to_rabin_base_code ↑af ↑af⇩G Abs Abs M_fin (set Σ) w M_fin⇩C_af"
using ltl_to_generalized_rabin_af_wellformed[OF finite_set assms] M_fin⇩C_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 ⟷ accept⇩G⇩R (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_rabin⇩C_correct[OF X]
unfolding ltl_to_generalized_rabin⇩C_af_def by simp
finally
show ?thesis .
qed

subsection ‹Generalized Deterministic Rabin Automaton (eager af)›

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

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

lemma M_fin⇩C_af⇩𝔘_correct:
assumes "t ∈ reach⇩t Σ (ltl_to_rabin_base_code_def.delta⇩C ↑af⇩𝔘 ↑af⇩G⇩𝔘 (Abs ∘ Unf⇩G) Σ) (ltl_to_rabin_base_code_def.initial⇩C (Abs ∘ Unf) (Abs ∘ Unf⇩G) φ)"
assumes "dom π ⊆ ❙G φ"
shows "abstract_transition t ∈ M⇩𝔘_fin π = M_fin⇩C_af⇩𝔘 φ (Mapping.Mapping π) t"
proof -
let ?delta = "ltl_to_rabin_base_code_def.delta⇩C ↑af⇩𝔘 ↑af⇩G⇩𝔘 (Abs ∘ Unf⇩G) Σ"
let ?initial = "ltl_to_rabin_base_code_def.initial⇩C (Abs ∘ Unf) (Abs ∘ Unf⇩G) φ"

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: reach⇩t_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 χ) (↑eval⇩G (dom π) (Abs (theG χ)))) (map (↑eval⇩G (dom π) o (λq. ↑step q ν)) (drop (the (π χ)) (the (Mapping.lookup y χ)))))
⟷ S ↑⊨⇩P Abs χ ∧ S ↑⊨⇩P ↑eval⇩G (dom π) (Abs (theG χ)) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G (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_fin⇩C_af⇩𝔘_lhs φ (Mapping.Mapping π) y ν)
⟷ ((∀χ ∈ dom π. (S ↑⊨⇩P Abs χ ∧ S ↑⊨⇩P ↑eval⇩G (dom π) (Abs (theG χ)) ∧ (∀q. (∃j ≥ the (π χ). the (?m' χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G (dom π) (↑step q ν)))))"
unfolding M_fin⇩C_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_rabin⇩C_af⇩𝔘 ≡ ltl_to_rabin_base_code_def.ltl_to_generalized_rabin⇩C ↑af⇩𝔘 ↑af⇩G⇩𝔘 (Abs ∘ Unf) (Abs ∘ Unf⇩G) M_fin⇩C_af⇩𝔘"

theorem ltl_to_generalized_rabin⇩C_af⇩𝔘_correct:
assumes "range w ⊆ set Σ"
shows "w ⊨ φ ⟷ accept⇩G⇩R_LTS (ltl_to_generalized_rabin⇩C_af⇩𝔘 Σ φ) w"
(is "?lhs ⟷ ?rhs")
proof -
have X: "ltl_to_rabin_base_code ↑af⇩𝔘 ↑af⇩G⇩𝔘 (Abs ∘ Unf) (Abs ∘ Unf⇩G) M⇩𝔘_fin (set Σ) w M_fin⇩C_af⇩𝔘"
using ltl_to_generalized_rabin_af⇩𝔘_wellformed[OF finite_set assms] M_fin⇩C_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 ⟷ accept⇩G⇩R (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_rabin⇩C_correct[OF X]
unfolding ltl_to_generalized_rabin⇩C_af⇩𝔘_def by simp
finally
show ?thesis .
qed

end
```