# Theory LTL_Rabin_Unfold_Opt

theory LTL_Rabin_Unfold_Opt
imports LTL_Rabin
```(*
Author:      Salomon Sickert
*)

section ‹Eager Unfolding Optimisation›

theory LTL_Rabin_Unfold_Opt
imports Main LTL_Rabin
begin

subsection ‹Preliminary Facts›

lemma finite_reach_af_opt:
"finite (reach Σ ↑af⇩𝔘 (Abs φ))"
proof (cases "Σ ≠ {}")
case True
thus ?thesis
using af_abs_opt.finite_abs_reach unfolding af_abs_opt.abs_reach_def reach_foldl_def[OF True]
using finite_subset[of "{foldl ↑af⇩𝔘 (Abs φ) w |w. set w ⊆ Σ}" "{foldl ↑af⇩𝔘 (Abs φ) w |w. True}"]
unfolding af_letter_abs_opt_def
by blast

lemma finite_reach_af_G_opt:
"finite (reach Σ ↑af⇩G⇩𝔘 (Abs φ))"
proof (cases "Σ ≠ {}")
case True
thus ?thesis
using af_G_abs_opt.finite_abs_reach unfolding af_G_abs_opt.abs_reach_def reach_foldl_def[OF True]
using finite_subset[of "{foldl ↑af⇩G⇩𝔘 (Abs φ) w |w. set w ⊆ Σ}" "{foldl ↑af⇩G⇩𝔘 (Abs φ) w |w. True}"]
unfolding af_G_letter_abs_opt_def
by blast

lemma wellformed_mojmir_opt:
assumes "Only_G 𝒢"
assumes "finite Σ"
assumes "range w ⊆ Σ"
shows "mojmir Σ ↑af⇩G⇩𝔘 (Abs φ) w {q. 𝒢 ⊨⇩P Rep q}"
proof -
have "∀q ν. q ∈ {q. 𝒢 ⊨⇩P Rep q} ⟶ af_G_letter_abs_opt q ν ∈ {q. 𝒢 ⊨⇩P Rep q}"
using ‹Only_G 𝒢› af_G_letter_opt_sat_core_lifted by auto
thus "?thesis"
using finite_reach_af_G_opt assms by (unfold_locales; auto)
qed

locale ltl_FG_to_rabin_opt_def =
fixes
Σ :: "'a set set"
fixes
φ :: "'a ltl"
fixes
𝒢 :: "'a ltl set"
fixes
w :: "'a set word"
begin

sublocale mojmir_to_rabin_def Σ "↑af⇩G⇩𝔘" "Abs (Unf⇩G φ)" w "{q. 𝒢 ⊨⇩P Rep q}" .

end

locale ltl_FG_to_rabin_opt = ltl_FG_to_rabin_opt_def +
assumes
wellformed_𝒢: "Only_G 𝒢"
assumes
bounded_w: "range w ⊆ Σ"
assumes
finite_Σ: "finite Σ"
begin

sublocale mojmir_to_rabin Σ "↑af⇩G⇩𝔘" "Abs (Unf⇩G φ)" w "{q. 𝒢 ⊨⇩P Rep q}"
proof
show "⋀q ν. q ∈ {q. 𝒢 ⊨⇩P Rep q} ⟹ ↑af⇩G⇩𝔘 q ν ∈ {q. 𝒢 ⊨⇩P Rep q}"
using wellformed_𝒢 af_G_letter_opt_sat_core_lifted by auto
have nonempty_Σ: "Σ ≠ {}"
using bounded_w by blast
show "finite (reach Σ ↑af⇩G⇩𝔘 (Abs (Unf⇩G φ)))" (is "finite ?A")
using finite_reach_af_G_opt wellformed_𝒢 by blast
qed (insert finite_Σ bounded_w)

end

subsection ‹Equivalences between the standard and the eager Mojmir construction›

context
fixes
Σ :: "'a set set"
fixes
φ :: "'a ltl"
fixes
𝒢 :: "'a ltl set"
fixes
w :: "'a set word"
assumes
context_assms: "Only_G 𝒢" "finite Σ" "range w ⊆ Σ"
begin

― ‹Create an interpretation of the mojmir locale for the standard construction›
interpretation 𝔐: ltl_FG_to_rabin Σ φ 𝒢 w
by (unfold_locales; insert context_assms; auto)

― ‹Create an interpretation of the mojmir locale for the optimised construction›
interpretation 𝔘: ltl_FG_to_rabin_opt Σ φ 𝒢 w
by (unfold_locales; insert context_assms; auto)

lemma unfold_token_run_eq:
assumes "x ≤ n"
shows "𝔐.token_run x (Suc n) = ↑step (𝔘.token_run x n) (w n)"
(is "?lhs = ?rhs")
proof -
have "x + (n - x) = n" and "x + (Suc n - x) = Suc n"
using assms by arith+
have "w [x → Suc n] = w [x → n] @ [w n]"
unfolding upt_Suc subsequence_def using assms by simp

have "af⇩G φ (w [x → Suc n]) = step (af⇩G⇩𝔘 (Unf⇩G φ) (w [x → n])) (w n)" (is "?l = ?r")
unfolding af_to_af_opt[symmetric] ‹w [x → Suc n] = w [x → n] @ [w n]› foldl_append
using af_letter_alt_def by auto
moreover
have "?lhs = Abs ?l"
unfolding 𝔐.token_run.simps run_foldl
using subsequence_shift ‹x + (Suc n - x) = Suc n› Nat.add_0_right subsequence_def
by (metis af_G_abs.f_foldl_abs_alt_def af_G_abs.f_foldl_abs.abs_eq af_G_letter_abs_def)
moreover
have "Abs ?r = ?rhs"
unfolding 𝔘.token_run.simps run_foldl subsequence_def[symmetric]
unfolding subsequence_shift ‹x + (n - x) = n› Nat.add_0_right af_G_letter_abs_opt_def
unfolding af_G_abs_opt.f_foldl_abs_alt_def[unfolded af_G_abs_opt.f_foldl_abs.abs_eq, symmetric]
ultimately
show "?lhs = ?rhs"
by presburger
qed

lemma unfold_token_succeeds_eq:
"𝔐.token_succeeds x = 𝔘.token_succeeds x"
proof
assume "𝔐.token_succeeds x"

then obtain n where "⋀m. m > n ⟹ 𝔐.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q}"
unfolding 𝔐.token_succeeds_alt_def MOST_nat by blast
then obtain n where "𝔐.token_run x (Suc n) ∈ {q. 𝒢 ⊨⇩P Rep q}" and "x ≤ n"
by (cases "x ≤ n") auto

hence 1: "𝒢 ⊨⇩P Rep (step_abs (𝔘.token_run x n) (w n))"
using unfold_token_run_eq by fastforce
moreover
have "Suc n - x = Suc (n - x)" and "x + (n - x) = n"
using ‹x ≤ n› by arith+
ultimately
have "𝔘.token_run x (Suc n) = Unf⇩G_abs (step_abs (𝔘.token_run x n) (w n))"
unfolding af_G_letter_abs_opt_split by simp

hence "𝒢 ⊨⇩P Rep (𝔘.token_run x (Suc n))"
using 1 Unf⇩G_𝒢[OF ‹Only_G 𝒢›] by (simp add: Rep_Abs_equiv Unf⇩G_abs_def)
thus "𝔘.token_succeeds x"
unfolding 𝔘.token_succeeds_def by blast
next
assume "𝔘.token_succeeds x"

then obtain n where "⋀m. m > n ⟹ 𝔘.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q}"
unfolding 𝔘.token_succeeds_alt_def MOST_nat by blast
then obtain n where "𝔘.token_run x n ∈ {q. 𝒢 ⊨⇩P Rep q}" and "x ≤ n"
by (cases "x ≤ n") (fastforce, auto)

hence "𝒢 ⊨⇩P Rep (step_abs (𝔘.token_run x n) (w n))"
using step_𝒢[OF ‹Only_G 𝒢›] Rep_step[unfolded ltl_prop_equiv_def] by blast
thus "𝔐.token_succeeds x"
unfolding 𝔐.token_succeeds_def unfold_token_run_eq[OF ‹x ≤ n›, symmetric] by blast
qed

lemma unfold_accept_eq:
"𝔐.accept = 𝔘.accept"
unfolding 𝔐.accept_def 𝔘.accept_def MOST_nat_le unfold_token_succeeds_eq ..

lemma unfold_𝒮_eq:
assumes "𝔐.accept"
shows "∀⇩∞n. 𝔐.𝒮 (Suc n) = (λq. step_abs q (w n)) ` (𝔘.𝒮 n) ∪ {Abs φ} ∪ {q. 𝒢 ⊨⇩P Rep q}"
proof -
― ‹Obtain lower bounds for proof›
obtain i⇩𝔐 where i⇩𝔐_def: "𝔐.smallest_accepting_rank = Some i⇩𝔐"
using assms unfolding 𝔐.smallest_accepting_rank_def by simp
obtain n⇩𝔐 where n⇩𝔐_def: "⋀x m. m ≥ n⇩𝔐 ⟹ 𝔐.token_succeeds x = (m < x ∨ (∃j≥i⇩𝔐. 𝔐.rank x m = Some j) ∨ 𝔐.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q})"
using 𝔐.token_smallest_accepting_rank[OF i⇩𝔐_def] unfolding MOST_nat_le by metis

have "𝔘.accept"
using assms unfold_accept_eq by simp
obtain i⇩𝔘 where i⇩𝔘_def: "𝔘.smallest_accepting_rank = Some i⇩𝔘"
using ‹𝔘.accept› unfolding 𝔘.smallest_accepting_rank_def by simp
obtain n⇩𝔘 where n⇩𝔘_def: "⋀x m. m ≥ n⇩𝔘 ⟹ 𝔘.token_succeeds x = (m < x ∨ (∃j≥i⇩𝔘. 𝔘.rank x m = Some j) ∨ 𝔘.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q})"
using 𝔘.token_smallest_accepting_rank[OF i⇩𝔘_def] unfolding MOST_nat_le by metis

show ?thesis
proof (unfold MOST_nat_le, rule, rule, rule)
fix m
assume "m ≥ max n⇩𝔐 n⇩𝔘"
hence "m ≥ n⇩𝔐" and "m ≥ n⇩𝔘" and "Suc m ≥ n⇩𝔐"
by simp+
― ‹Using the properties of @{term n⇩𝔐} and @{term n⇩𝔘} and the lemma @{thm unfold_token_succeeds_eq},
we prove that the behaviour of x in @{text 𝔐} and @{text 𝔘} is similar in regards to
creation time, accepting rank or final states.›
hence token_trans: "⋀x. Suc m < x ∨ (∃j≥i⇩𝔐. 𝔐.rank x (Suc m) = Some j) ∨ 𝔐.token_run x (Suc m) ∈ {q. 𝒢 ⊨⇩P Rep q}
⟷ m < x ∨ (∃j≥i⇩𝔘. 𝔘.rank x m = Some j) ∨ 𝔘.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q}"
using n⇩𝔐_def n⇩𝔘_def unfolding unfold_token_succeeds_eq by presburger

show "𝔐.𝒮 (Suc m) = (λq. step_abs q (w m)) ` (𝔘.𝒮 m) ∪ {Abs φ} ∪ {q. 𝒢 ⊨⇩P Rep q}" (is "?lhs = ?rhs")
proof
{
fix q assume "∃j≥i⇩𝔐. 𝔐.state_rank q (Suc m) = Some j"
moreover
then obtain x where q_def: "q = 𝔐.token_run x (Suc m)" and "x ≤ Suc m"
using 𝔐.push_down_state_rank_tokens by fastforce
ultimately
have "∃j≥i⇩𝔐. 𝔐.rank x (Suc m) = Some j"
using 𝔐.rank_eq_state_rank by metis
hence token_cases: "(∃j≥i⇩𝔘. 𝔘.rank x m = Some j) ∨ 𝔘.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q} ∨ x = Suc m"
using token_trans[of x] 𝔐.rank_Some_time by fastforce
have "q ∈ ?rhs"
proof (cases "x ≠ Suc m")
case True
hence "x ≤ m"
using ‹x ≤ Suc m› by arith
have "𝔘.token_run x m ∈ {q. 𝒢 ⊨⇩P Rep q} ⟹ 𝒢 ⊨⇩P Rep q"
unfolding ‹q = 𝔐.token_run x (Suc m)› unfold_token_run_eq[OF ‹x ≤ m›]
using Rep_step[unfolded ltl_prop_equiv_def] step_𝒢[OF ‹Only_G 𝒢›] by blast
moreover
{
assume "∃j ≥ i⇩𝔘. 𝔘.rank x m = Some j"
moreover
define q' where "q' = 𝔘.token_run x m"
ultimately
have "∃j ≥ i⇩𝔘. 𝔘.state_rank q' m = Some j"
unfolding 𝔘.rank_eq_state_rank[OF ‹x ≤ m›] q'_def by blast
hence "q' ∈ 𝔘.𝒮 m"
using assms i⇩𝔘_def by simp
moreover
have "q = step_abs q' (w m)"
unfolding q_def q'_def unfold_token_run_eq[OF ‹x ≤ m›] ..
ultimately
have "q ∈ (λq. step_abs q (w m)) ` (𝔘.𝒮 m)"
by blast
}
ultimately
show ?thesis
using token_cases True by blast
}
thus "?lhs ⊆ ?rhs"
unfolding 𝔐.𝒮.simps i⇩𝔐_def option.sel by blast
next
{
fix q
assume "q ∈ (λq. step_abs q (w m)) ` (𝔘.𝒮 m)"
then obtain q' where q_def: "q = step_abs q' (w m)" and "q' ∈ 𝔘.𝒮 m"
by blast
hence "q ∈ ?lhs"
proof (cases "𝒢 ⊨⇩P Rep q'")
case False
hence "∃j ≥ i⇩𝔘. 𝔘.state_rank q' m = Some j"
using ‹q' ∈ 𝔘.𝒮 m› unfolding 𝔘.𝒮.simps i⇩𝔘_def option.sel by blast
moreover
then obtain x where q'_def: "q' = 𝔘.token_run x m" and "x ≤ m" and "x ≤ Suc m"
using 𝔘.push_down_state_rank_tokens by force
ultimately
have "∃j ≥ i⇩𝔘. 𝔘.rank x m = Some j"
unfolding 𝔘.rank_eq_state_rank[OF ‹x ≤ m›] q'_def by blast
hence "(∃j≥i⇩𝔐. 𝔐.rank x (Suc m) = Some j) ∨ 𝔐.token_run x (Suc m) ∈ {q. 𝒢 ⊨⇩P Rep q}"
using token_trans[of x] 𝔘.rank_Some_time by fastforce
moreover
have "𝔐.token_run x (Suc m) = q"
unfolding q_def q'_def unfold_token_run_eq[OF ‹x ≤ m›] ..
ultimately
have "(∃j≥i⇩𝔐. 𝔐.state_rank q (Suc m) = Some j) ∨ q ∈ {q. 𝒢 ⊨⇩P Rep q}"
using 𝔐.rank_eq_state_rank[OF ‹x ≤ Suc m›] by metis
thus ?thesis
unfolding 𝔐.𝒮.simps option.sel i⇩𝔐_def by blast
qed (insert step_𝒢[OF ‹Only_G 𝒢›, of "Rep q'"], unfold q_def Rep_step[unfolded ltl_prop_equiv_def, rule_format, symmetric], auto)
}
moreover
have "(∃j≥i⇩𝔐. 𝔐.rank (Suc m) (Suc m) = Some j) ∨ 𝒢 ⊨⇩P Rep (Abs φ)"
using token_trans[of "Suc m"] by simp
hence "Abs φ ∈ ?lhs"
using i⇩𝔐_def 𝔐.rank_eq_state_rank[OF order_refl] by (cases "𝒢 ⊨⇩P Rep (Abs φ)") simp+
ultimately
show "?lhs ⊇ ?rhs"
unfolding 𝔐.𝒮.simps by blast
qed
qed
qed

end

subsection ‹Automaton Definition›

fun M⇩𝔘_fin :: "('a ltl ⇀ nat) ⇒ ('a ltl⇩P × ('a ltl ⇀ 'a ltl⇩P ⇀ nat), 'a set) transition set"
where
"M⇩𝔘_fin π = {((φ', m), ν, p). ¬(∀S. (∀χ ∈ (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 ν))) ⟶ S ↑⊨⇩P (↑step φ' ν))}"

locale ltl_to_rabin_af_unf = ltl_to_rabin_base "↑af⇩𝔘" "↑af⇩G⇩𝔘" "Abs o Unf" "Abs o Unf⇩G" M⇩𝔘_fin begin

abbreviation "δ⇩𝔘 ≡ delta"
abbreviation "ι⇩𝔘 ≡ initial"
abbreviation "Acc⇩𝔘_fin ≡ Acc_fin"
abbreviation "Acc⇩𝔘_inf ≡ Acc_inf"
abbreviation "F⇩𝔘 ≡ rabin_pairs"
abbreviation "Acc⇩𝔘 ≡ Acc"
abbreviation "𝒜⇩𝔘 ≡ ltl_to_generalized_rabin"

subsection ‹Properties›

subsection ‹Correctness Theorem›

lemma unfold_optimisation_correct_M:
assumes "dom π⇩𝒜 ⊆ ❙G φ"
assumes "dom π⇩𝔘 = dom π⇩𝒜"
assumes "⋀χ. χ ∈ dom π⇩𝒜 ⟹ π⇩𝒜 χ = mojmir_def.smallest_accepting_rank Σ ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ↑⊨⇩P q}"
assumes "⋀χ. χ ∈ dom π⇩𝔘 ⟹ π⇩𝔘 χ = mojmir_def.smallest_accepting_rank Σ af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) w {q. dom π⇩𝔘 ↑⊨⇩P q}"
shows "accepting_pair⇩R (ltl_to_rabin_af.δ⇩𝒜 Σ) (ltl_to_rabin_af.ι⇩𝒜 φ) (M_fin π⇩𝒜, UNIV) w ⟷ accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (M⇩𝔘_fin π⇩𝔘, UNIV) w"
proof -
― ‹Preliminary Facts›
note 𝒢_properties[OF ‹dom π⇩𝒜 ⊆ ❙G φ›]

interpret 𝒜: ltl_to_rabin_af
using ltl_to_generalized_rabin_af_wellformed bounded_w finite_Σ by auto

― ‹Define constants for both runs›
define r⇩𝒜 r⇩𝔘
where "r⇩𝒜 = run⇩t (ltl_to_rabin_af.δ⇩𝒜 Σ) (ltl_to_rabin_af.ι⇩𝒜 φ) w"
and "r⇩𝔘 = run⇩t (δ⇩𝔘 Σ) (ι⇩𝔘 φ) w"
hence "finite (range r⇩𝒜)" and "finite (range r⇩𝔘)"
using run⇩t_finite[OF 𝒜.finite_reach] run⇩t_finite[OF finite_reach] bounded_w finite_Σ by simp+

― ‹Prove that the limit of both runs behave the same in respect to the M acceptance condition›
have "limit r⇩𝒜 ∩ M_fin π⇩𝒜 = {} ⟷ limit r⇩𝔘 ∩ M⇩𝔘_fin π⇩𝔘 = {}"
proof -
have "ltl_FG_to_rabin Σ (dom π⇩𝒜) w"
by (unfold_locales; insert 𝒢_elements[OF ‹dom π⇩𝒜 ⊆ ❙G φ›] finite_Σ bounded_w)
hence X: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ mojmir_def.accept ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ⊨⇩P Rep q}"
by (metis assms(3)[unfolded ltl_prop_entails_abs.rep_eq] ltl_FG_to_rabin.smallest_accepting_rank_properties(1) domD)
have "∀⇩∞i. ∀χ ∈ dom π⇩𝒜. mojmir_def.𝒮 Σ ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ⊨⇩P Rep q} (Suc i)
= (λq. step_abs q (w i)) ` (mojmir_def.𝒮 Σ ↑af⇩G⇩𝔘 (Abs (Unf⇩G (theG χ))) w {q. dom π⇩𝒜 ⊨⇩P Rep q} i) ∪ {Abs (theG χ)} ∪ {q. dom π⇩𝒜 ⊨⇩P Rep q}"
using almost_all_commutative'[OF ‹finite (dom π⇩𝒜)›] X unfold_𝒮_eq[OF ‹Only_G (dom π⇩𝒜)›] finite_Σ bounded_w by simp

then obtain i where i_def: "⋀j χ. j ≥ i ⟹ χ ∈ dom π⇩𝒜 ⟹ mojmir_def.𝒮 Σ ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ⊨⇩P Rep q} (Suc j)
= (λq. step_abs q (w j)) ` (mojmir_def.𝒮 Σ ↑af⇩G⇩𝔘 (Abs (Unf⇩G (theG χ))) w {q. dom π⇩𝒜 ⊨⇩P Rep q} j) ∪ {Abs (theG χ)} ∪ {q. dom π⇩𝒜 ⊨⇩P Rep q}"
unfolding MOST_nat_le by blast

obtain j where "limit r⇩𝒜 = range (suffix j r⇩𝒜)"
and "limit r⇩𝔘 = range (suffix j r⇩𝔘)"
using ‹finite (range r⇩𝒜)› ‹finite (range r⇩𝔘)›
by (rule common_range_limit)
hence "limit r⇩𝒜 = range (suffix (j + i + 1) r⇩𝒜)"
and "limit r⇩𝔘 = range (suffix (j + i) r⇩𝔘)"
moreover
have "⋀j. j ≥ i ⟹ r⇩𝒜 (Suc j) ∈ M_fin π⇩𝒜 ⟷ r⇩𝔘 j ∈ M⇩𝔘_fin π⇩𝔘"
proof -
fix j
assume "j ≥ i"

obtain φ⇩𝒜 m⇩𝒜 x where r⇩𝒜_def': "r⇩𝒜 (Suc j) = ((φ⇩𝒜, m⇩𝒜), w (Suc j), x)"
unfolding r⇩𝒜_def run⇩t.simps using prod.exhaust by fastforce

obtain φ⇩𝔘 m⇩𝔘 y where r⇩𝔘_def': "r⇩𝔘 j = ((φ⇩𝔘, m⇩𝔘), w j, y)"
unfolding r⇩𝔘_def run⇩t.simps using prod.exhaust by fastforce

have m⇩𝒜_def: "⋀χ q. χ ∈ ❙G φ ⟹ the (m⇩𝒜 χ) q = semi_mojmir_def.state_rank Σ ↑af⇩G (Abs (theG χ)) w q (Suc j)"
using 𝒜.run_properties(2)[of _ φ "Suc j"] r⇩𝒜_def'[unfolded r⇩𝒜_def] prod.sel  by simp

have m⇩𝔘_def: "⋀χ q. χ ∈ ❙G φ ⟹ the (m⇩𝔘 χ) q = semi_mojmir_def.state_rank Σ ↑af⇩G⇩𝔘 (Abs (Unf⇩G (theG χ))) w q j"
using run_properties(2)[of _ φ j] r⇩𝔘_def'[unfolded r⇩𝔘_def] prod.sel by simp

{
have upt_Suc_0: "[0..<Suc j] = [0..<j] @ [j]"
by simp
have "Rep (fst (fst (r⇩𝒜 (Suc j)))) ≡⇩P step (Rep (fst (fst (r⇩𝔘 j)))) (w j)"
unfolding r⇩𝒜_def r⇩𝔘_def run⇩t.simps fst_conv 𝒜.run_properties(1)[of φ "Suc j"] run_properties(1) comp_apply
unfolding subsequence_def upt_Suc_0 map_append map_def list.map af_abs_equiv Unf_abs.abs_eq using Rep_step by auto
hence A: "⋀S. S ⊨⇩P Rep φ⇩𝒜 ⟷ S ⊨⇩P step (Rep φ⇩𝔘) (w j)"
unfolding r⇩𝒜_def' r⇩𝔘_def' prod.sel ltl_prop_equiv_def ..

{
fix S assume "⋀χ. χ ∈ dom π⇩𝒜 ⟹ S ⊨⇩P χ"
hence "dom π⇩𝒜 ⊆ S"
using ‹Only_G (dom π⇩𝒜)› assms by (metis ltl_prop_entailment.simps(8) subsetI)
{
fix χ assume "χ ∈ dom π⇩𝒜"

interpret 𝔐: ltl_FG_to_rabin Σ "theG χ" "dom π⇩𝒜"
by (unfold_locales, insert ‹Only_G (dom π⇩𝒜)› bounded_w finite_Σ)
interpret 𝔘: ltl_FG_to_rabin_opt Σ "theG χ" "dom π⇩𝒜"
by (unfold_locales, insert ‹Only_G (dom π⇩𝒜)› bounded_w finite_Σ)

have "⋀q ν. dom π⇩𝒜 ⊨⇩P Rep q ⟹ dom π⇩𝒜 ⊨⇩P Rep (step_abs q ν)"
using ‹Only_G (dom π⇩𝒜)› by (metis ltl_prop_equiv_def Rep_step step_𝒢)
then have subsetStep: "⋀ν. (λq. step_abs q ν) ` {q. dom π⇩𝒜 ⊨⇩P Rep q} ⊆ {q. dom π⇩𝒜 ⊨⇩P Rep q}"
by auto

let ?P = "λq. S ⊨⇩P eval⇩G (dom π⇩𝒜) (Rep q)"
have "⋀q ν. (dom π⇩𝒜) ⊨⇩P Rep q ⟹ ?P q"
using ‹Only_G (dom π⇩𝒜)› eval⇩G_prop_entailment ‹(dom π⇩𝒜) ⊆ S› by blast
hence "⋀q. q ∈ {q. (dom π⇩𝒜) ⊨⇩P Rep q} ⟹ ?P q"
by simp
moreover
have Y: "𝔐.𝒮 (Suc j) = (λq. step_abs q (w j)) ` (𝔘.𝒮 j) ∪ {Abs (theG χ)} ∪ {q. dom π⇩𝒜 ⊨⇩P Rep q}"
using i_def[OF ‹j ≥ i› ‹χ ∈ dom π⇩𝒜›] by simp

have 1: "𝔐.smallest_accepting_rank = (π⇩𝒜 χ)"
and 2: "𝔘.smallest_accepting_rank = (π⇩𝔘 χ)"
and 3: "χ ∈ ❙G φ"
using ‹χ ∈ dom π⇩𝒜› assms[unfolded ltl_prop_entails_abs.rep_eq] by auto
ultimately
have "(∀q ∈ 𝔐.𝒮 (Suc j). ?P q) = (∀q ∈ (λq. step_abs q (w j)) ` (𝔘.𝒮 j) ∪ {Abs (theG χ)}. ?P q)"
unfolding Y by blast
hence 4: "(∀q. (∃j ≥ the (π⇩𝒜 χ). the (m⇩𝒜 χ) q = Some j) ⟶ ?P q) = ((∀q. (∃j ≥ the (π⇩𝔘 χ). the (m⇩𝔘 χ) q = Some j) ⟶ ?P (step_abs q (w j))) ∧ ?P (Abs (theG χ)))"
using ‹⋀q. q ∈ {q. dom π⇩𝒜 ⊨⇩P Rep q} ⟹ ?P q› subsetStep
unfolding m⇩𝒜_def[OF 3, symmetric] m⇩𝔘_def[OF 3, symmetric] 𝔐.𝒮.simps 𝔘.𝒮.simps 1 2 Set.image_Un option.sel by blast
have "S ⊨⇩P χ ∧ (∀q. (∃j ≥ the (π⇩𝒜 χ). the (m⇩𝒜 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (Rep q)) ⟷
S ⊨⇩P χ ∧ S ⊨⇩P eval⇩G (dom π⇩𝒜) (theG χ) ∧ (∀q. (∃j ≥ the (π⇩𝔘 χ). the (m⇩𝔘 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (step (Rep q) (w j)))"
unfolding 4 using eval⇩G_respectfulness(2)[OF Rep_Abs_equiv, unfolded ltl_prop_equiv_def]
using eval⇩G_respectfulness(2)[OF Rep_step, unfolded ltl_prop_equiv_def] by blast
}
hence "((∀χ ∈ dom π⇩𝒜. S ⊨⇩P χ ∧ (∀q. (∃j ≥ the (π⇩𝒜 χ). the (m⇩𝒜 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (Rep q))) ⟶ S ⊨⇩P Rep φ⇩𝒜)
⟷ ((∀χ ∈ dom π⇩𝔘. S ⊨⇩P χ ∧ S ⊨⇩P eval⇩G (dom π⇩𝔘) (theG χ) ∧ (∀q. (∃j ≥ the (π⇩𝔘 χ). the (m⇩𝔘 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝔘) (step (Rep q) (w j)))) ⟶ S ⊨⇩P step (Rep φ⇩𝔘) (w j))"
by (simp add: ‹⋀χ. χ ∈ dom π⇩𝒜 ⟹ (S ⊨⇩P χ ∧ (∀q. (∃j≥the (π⇩𝒜 χ). the (m⇩𝒜 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (Rep q))) = (S ⊨⇩P χ ∧ S ⊨⇩P eval⇩G (dom π⇩𝒜) (theG χ) ∧ (∀q. (∃j≥the (π⇩𝔘 χ). the (m⇩𝔘 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (step (Rep q) (w j))))› A assms(2))
}
hence "(∀S. (∀χ ∈ dom π⇩𝒜. S ⊨⇩P χ ∧ (∀q. (∃j ≥ the (π⇩𝒜 χ). the (m⇩𝒜 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝒜) (Rep q))) ⟶ S ⊨⇩P Rep φ⇩𝒜) ⟷
(∀S. (∀χ ∈ dom π⇩𝔘. S ⊨⇩P χ ∧ S ⊨⇩P eval⇩G (dom π⇩𝔘) (theG χ) ∧ (∀q. (∃j ≥ the (π⇩𝔘 χ). the (m⇩𝔘 χ) q = Some j) ⟶ S ⊨⇩P eval⇩G (dom π⇩𝔘) (step (Rep q) (w j)))) ⟶ S ⊨⇩P step (Rep φ⇩𝔘) (w j))"
unfolding assms by auto
}
hence "((φ⇩𝒜, m⇩𝒜), w (Suc j), x) ∈ M_fin π⇩𝒜 ⟷ ((φ⇩𝔘, m⇩𝔘), w j, y) ∈ M⇩𝔘_fin π⇩𝔘"
unfolding M_fin.simps M⇩𝔘_fin.simps ltl_prop_entails_abs.abs_eq[symmetric] eval⇩G_abs.abs_eq[symmetric] ltl⇩P_abs_rep step_abs.abs_eq[symmetric] by blast
thus "?thesis j"
unfolding r⇩𝒜_def' r⇩𝔘_def' .
qed
hence "⋀n. r⇩𝒜 (j + i + 1 + n) ∈ M_fin π⇩𝒜 ⟷ r⇩𝔘 (j + i + n) ∈ M⇩𝔘_fin π⇩𝔘"
by simp
hence "range (suffix (j + i + 1) r⇩𝒜) ∩ M_fin π⇩𝒜 = {} ⟷ range (suffix (j + i) r⇩𝔘) ∩ M⇩𝔘_fin π⇩𝔘 = {}"
unfolding suffix_def by blast
ultimately
show "limit r⇩𝒜 ∩ M_fin π⇩𝒜 = {} ⟷ limit r⇩𝔘 ∩ M⇩𝔘_fin π⇩𝔘 = {}"
by force
qed
moreover
have "limit r⇩𝒜 ∩ UNIV ≠ {}" and "limit r⇩𝔘 ∩ UNIV ≠ {}"
using limit_nonempty ‹finite (range r⇩𝔘)› ‹finite (range r⇩𝒜)› by auto
ultimately
show ?thesis
unfolding accepting_pair⇩R_def fst_conv snd_conv r⇩𝒜_def[symmetric] r⇩𝔘_def[symmetric] Let_def by blast
qed

theorem ltl_to_generalized_rabin_correct:
"w ⊨ φ ⟷ accept⇩G⇩R (𝒜⇩𝔘 Σ φ) w"
(is "_ ⟷ ?rhs")
proof (unfold ltl_to_generalized_rabin_af_correct[OF finite_Σ bounded_w], standard)
let ?lhs = "accept⇩G⇩R (ltl_to_generalized_rabin_af Σ φ) w"

interpret 𝒜: ltl_to_rabin_af Σ w
using ltl_to_generalized_rabin_af_wellformed bounded_w finite_Σ by auto

{
assume ?lhs
then obtain π where I: "dom π ⊆ ❙G φ"
and II:  "⋀χ. χ ∈ dom π ⟹ the (π χ) < 𝒜.max_rank_of Σ χ"
and III: "accepting_pair⇩R (ltl_to_rabin_af.δ⇩𝒜 Σ) (ltl_to_rabin_af.ι⇩𝒜 φ) (M_fin π, UNIV) w"
and IV:  "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (𝒜.δ⇩𝒜 Σ) (ltl_to_rabin_af.ι⇩𝒜 φ) (𝒜.Acc Σ π χ) w"
by (unfold ltl_to_generalized_rabin_af.simps; blast intro: 𝒜.accept⇩G⇩R_I)

― ‹Normalise @{text π} to the smallest accepting ranks›
then obtain π⇩𝒜 where A: "dom π = dom π⇩𝒜"
and B: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ π⇩𝒜 χ = mojmir_def.smallest_accepting_rank Σ ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ↑⊨⇩P q}"
and C: "accepting_pair⇩R (𝒜.δ⇩𝒜 Σ) (𝒜.ι⇩𝒜 φ) (M_fin π⇩𝒜, UNIV) w"
and D: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ accepting_pair⇩R (𝒜.δ⇩𝒜 Σ) (𝒜.ι⇩𝒜 φ) (𝒜.Acc Σ π⇩𝒜 χ) w"
using 𝒜.normalize_π by blast

― ‹Properties about the domain of @{text π}›
note 𝒢_properties[OF ‹dom π ⊆ ❙G φ›]
hence 𝔐_Accept: "⋀χ. χ ∈ dom π ⟹ mojmir_def.accept af_G_letter_abs (Abs (theG χ)) w {q. dom π ↑⊨⇩P q}"
using I II IV 𝒜.Acc_to_mojmir_accept unfolding ltl_to_rabin_base_def.max_rank_of_def by (metis ltl.sel(8))
hence 𝔘_Accept: "⋀χ. χ ∈ dom π ⟹ mojmir_def.accept af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) w {q. dom π ↑⊨⇩P q}"
using unfold_accept_eq[OF ‹Only_G (dom π)› finite_Σ bounded_w] unfolding ltl_prop_entails_abs.rep_eq by blast

― ‹Define @{text π} for the other automaton›
define π⇩𝔘
where "π⇩𝔘 χ = (if χ ∈ dom π then mojmir_def.smallest_accepting_rank Σ af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) w {q. dom π ↑⊨⇩P q} else None)"
for χ

have 1: "dom π⇩𝔘 = dom π"
using 𝔘_Accept by (auto simp add: π⇩𝔘_def dom_def mojmir_def.smallest_accepting_rank_def)
hence "dom π⇩𝔘 = dom π⇩𝒜" and "dom π⇩𝒜 ⊆ ❙G φ" and "dom π⇩𝔘 ⊆ ❙G φ"
using A ‹dom π ⊆ ❙G φ› by blast+
have 2: "⋀χ. χ ∈ dom π⇩𝔘 ⟹ π⇩𝔘 χ = mojmir_def.smallest_accepting_rank Σ af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) w {q. dom π⇩𝔘 ↑⊨⇩P q}"
using 1 unfolding ‹dom π⇩𝔘 = dom π› π⇩𝔘_def by simp
hence 3: "⋀χ. χ ∈ dom π⇩𝔘 ⟹ the (π⇩𝔘 χ) < semi_mojmir_def.max_rank Σ af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) "
using wellformed_mojmir_opt[OF 𝒢_elements[OF ‹dom π⇩𝔘 ⊆ ❙G φ›] finite_Σ bounded_w, THEN mojmir.smallest_accepting_rank_properties(6)]
unfolding ltl_prop_entails_abs.rep_eq by fastforce

― ‹Use correctness of the translation of individual accepting pairs›
have Acc: "⋀χ. χ ∈ dom π⇩𝔘 ⟹ accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (Acc⇩𝔘 Σ π⇩𝔘 χ) w"
using mojmir_accept_to_Acc[OF _ ‹dom π⇩𝔘 ⊆ ❙G φ›] 𝒢_elements[OF ‹dom π⇩𝔘 ⊆ ❙G φ›]
using 1 2[of "G _"] 3[of "G _"] 𝔘_Accept[of "G _"] ltl.sel(8) unfolding comp_apply by metis
have M: "accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (M⇩𝔘_fin π⇩𝔘, UNIV) w"
using unfold_optimisation_correct_M[OF ‹dom π⇩𝒜 ⊆ ❙G φ› ‹dom π⇩𝔘 = dom π⇩𝒜› B 2] C
using ‹dom π⇩𝔘 = dom π⇩𝒜› by blast+

show ?rhs
using Acc 3 ‹dom π⇩𝔘 ⊆ ❙G φ› combine_rabin_pairs_UNIV[OF M combine_rabin_pairs]
by (simp only: accept⇩G⇩R_def fst_conv snd_conv ltl_to_generalized_rabin.simps rabin_pairs.simps max_rank_of_def comp_apply) blast
}

{
assume ?rhs
then obtain π where I: "dom π ⊆ ❙G φ"
and II:  "⋀χ. χ ∈ dom π ⟹ the (π χ) < max_rank_of Σ χ"
and III: "accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (M⇩𝔘_fin π, UNIV) w"
and IV:  "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (Acc⇩𝔘 Σ π χ) w"
by (blast intro: accept⇩G⇩R_I)

― ‹Normalize @{text π} to the smallest accepting ranks›
then obtain π⇩𝔘 where A: "dom π = dom π⇩𝔘"
and B: "⋀χ. χ ∈ dom π⇩𝔘 ⟹ π⇩𝔘 χ = mojmir_def.smallest_accepting_rank Σ ↑af⇩G⇩𝔘 (Abs (Unf⇩G (theG χ))) w {q. dom π⇩𝔘 ↑⊨⇩P q}"
and C: "accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (M⇩𝔘_fin π⇩𝔘, UNIV) w"
and D: "⋀χ. χ ∈ dom π⇩𝔘 ⟹ accepting_pair⇩R (δ⇩𝔘 Σ) (ι⇩𝔘 φ) (Acc⇩𝔘 Σ π⇩𝔘 χ) w"
using normalize_π unfolding comp_apply by blast

― ‹Properties about the domain of @{text π}›
note 𝒢_properties[OF ‹dom π ⊆ ❙G φ›]
hence 𝔘_Accept: "⋀χ. χ ∈ dom π ⟹ mojmir_def.accept af_G_letter_abs_opt (Abs (Unf⇩G (theG χ))) w {q. dom π ↑⊨⇩P q}"
using I II IV Acc_to_mojmir_accept unfolding max_rank_of_def comp_apply by (metis ltl.sel(8))
hence 𝔐_Accept: "⋀χ. χ ∈ dom π ⟹ mojmir_def.accept af_G_letter_abs (Abs (theG χ)) w {q. dom π ↑⊨⇩P q}"
using unfold_accept_eq[OF ‹Only_G (dom π)› finite_Σ bounded_w]
unfolding ltl_prop_entails_abs.rep_eq by blast

― ‹Define @{text π} for the other automaton›
define π⇩𝒜
where "π⇩𝒜 χ = (if χ ∈ dom π then mojmir_def.smallest_accepting_rank Σ ↑af⇩G (Abs (theG χ)) w {q. dom π ↑⊨⇩P q} else None)"
for χ

have 1: "dom π⇩𝒜 = dom π"
using 𝔐_Accept by (auto simp add: π⇩𝒜_def dom_def mojmir_def.smallest_accepting_rank_def)
hence "dom π⇩𝔘 = dom π⇩𝒜" and "dom π⇩𝒜 ⊆ ❙G φ" and "dom π⇩𝔘 ⊆ ❙G φ"
using A ‹dom π ⊆ ❙G φ› by blast+
hence "ltl_FG_to_rabin Σ (dom π⇩𝒜) w"
by (unfold_locales; insert 𝒢_elements[OF ‹dom π⇩𝒜 ⊆ ❙G φ›] finite_Σ bounded_w)
have 2: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ π⇩𝒜 χ = mojmir_def.smallest_accepting_rank Σ ↑af⇩G (Abs (theG χ)) w {q. dom π⇩𝒜 ↑⊨⇩P q}"
using 1 unfolding ‹dom π⇩𝒜 = dom π› π⇩𝒜_def by simp
hence 3: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ the (π⇩𝒜 χ) < semi_mojmir_def.max_rank Σ ↑af⇩G (Abs (theG χ))"
using ltl_FG_to_rabin.smallest_accepting_rank_properties(6)[OF ‹ltl_FG_to_rabin Σ (dom π⇩𝒜) w›]
unfolding ltl_prop_entails_abs.rep_eq by fastforce

― ‹Use correctness of the translation of individual accepting pairs›
have Acc: "⋀χ. χ ∈ dom π⇩𝒜 ⟹ accepting_pair⇩R (𝒜.δ⇩𝒜 Σ) (𝒜.ι⇩𝒜 φ) (𝒜.Acc Σ π⇩𝒜 χ) w"
using 𝒜.mojmir_accept_to_Acc[OF _ ‹dom π⇩𝒜 ⊆ ❙G φ›] 𝒢_elements[OF ‹dom π⇩𝒜 ⊆ ❙G φ›]
using 1 2[of "G _"] 3[of "G _"] 𝔐_Accept[of "G _"] ltl.sel(8) by metis
have M: "accepting_pair⇩R (𝒜.δ⇩𝒜 Σ) (𝒜.ι⇩𝒜 φ) (M_fin π⇩𝒜, UNIV) w"
using unfold_optimisation_correct_M[OF ‹dom π⇩𝒜 ⊆ ❙G φ› ‹dom π⇩𝔘 = dom π⇩𝒜› 2 B] C
using ‹dom π⇩𝔘 = dom π⇩𝒜› by blast+

show ?lhs
using Acc 3 ‹dom π⇩𝒜 ⊆ ❙G φ› combine_rabin_pairs_UNIV[OF M combine_rabin_pairs]
by (simp only: accept⇩G⇩R_def fst_conv snd_conv 𝒜.ltl_to_generalized_rabin.simps 𝒜.rabin_pairs.simps
ltl_to_generalized_rabin_af.simps  𝒜.max_rank_of_def comp_apply) blast
}
qed

end

fun ltl_to_generalized_rabin_af⇩𝔘
where
"ltl_to_generalized_rabin_af⇩𝔘 Σ φ = ltl_to_rabin_base_def.ltl_to_generalized_rabin ↑af⇩𝔘 ↑af⇩G⇩𝔘 (Abs ∘ Unf) (Abs ∘ Unf⇩G) M⇩𝔘_fin Σ φ"

lemma ltl_to_generalized_rabin_af⇩𝔘_wellformed:
"finite Σ ⟹ range w ⊆ Σ ⟹ ltl_to_rabin_af_unf Σ w"
apply (unfold_locales)
apply (auto simp add: af_G_letter_opt_sat_core_lifted ltl_prop_entails_abs.rep_eq intro: finite_reach_af_opt finite_reach_af_G_opt)
apply (meson le_trans ltl_semi_mojmir[unfolded semi_mojmir_def])+
done

theorem ltl_to_generalized_rabin_af⇩𝔘_correct:
assumes "finite Σ"
assumes "range w ⊆ Σ"
shows "w ⊨ φ = accept⇩G⇩R (ltl_to_generalized_rabin_af⇩𝔘 Σ φ) w"
using ltl_to_generalized_rabin_af⇩𝔘_wellformed[OF assms, THEN ltl_to_rabin_af_unf.ltl_to_generalized_rabin_correct] by simp

thm ltl_FG_to_generalized_rabin_correct ltl_to_generalized_rabin_af_correct ltl_to_generalized_rabin_af⇩𝔘_correct

end
```