Theory LTL_Rabin

theory LTL_Rabin
imports Mojmir_Rabin Logical_Characterization
```(*
Author:      Salomon Sickert
*)

section ‹Translation from LTL to (Deterministic Transitions-Based) Generalised Rabin Automata›

theory LTL_Rabin
imports Main Mojmir_Rabin Logical_Characterization
begin

subsection ‹Preliminary Facts›

lemma run_af_G_letter_abs_eq_Abs_af_G_letter:
"run ↑af⇩G (Abs φ) w i = Abs (run af_G_letter φ w i)"
by (induction i) (simp, metis af_G_abs.f_foldl_abs.abs_eq af_G_abs.f_foldl_abs_alt_def run_foldl af_G_letter_abs_def)

lemma finite_reach_af:
"finite (reach Σ ↑af (Abs φ))"
proof (cases "Σ ≠ {}")
case True
thus ?thesis
using af_abs.finite_abs_reach unfolding af_abs.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_def
by (blast)

lemma ltl_semi_mojmir:
assumes "finite Σ"
assumes "range w ⊆ Σ"
shows "semi_mojmir Σ ↑af⇩G (Abs ψ) w"
proof
fix ψ
have nonempty_Σ: "Σ ≠ {}"
using assms by auto
show "finite (reach Σ ↑af⇩G (Abs ψ))" (is "finite ?A")
using af_G_abs.finite_abs_reach finite_subset[where A = ?A, where B = "lift_ltl_transformer.abs_reach af_G_letter (Abs ψ)"]
unfolding af_G_abs.abs_reach_def af_G_letter_abs_def reach_foldl_def[OF nonempty_Σ] by blast
qed (insert assms, auto)

subsection ‹Single Secondary Automaton›

locale ltl_FG_to_rabin_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 φ" w "{q. 𝒢 ⊨⇩P Rep q}" .

― ‹Import abbreviations from parent locale to simplify terms›
abbreviation "δ⇩R ≡ step"
abbreviation "q⇩R ≡ initial"
abbreviation "Acc⇩R j ≡ (fail⇩R ∪ merge⇩R j, succeed⇩R j)"
abbreviation "max_rank⇩R ≡ max_rank"
abbreviation "smallest_accepting_rank⇩R ≡ smallest_accepting_rank"
abbreviation "accept⇩R' ≡ accept"
abbreviation "𝒮⇩R ≡ 𝒮"

lemma Rep_token_run_af:
"Rep (token_run x n) ≡⇩P af⇩G φ (w [x → n])"
proof -
have "token_run x n = Abs (af⇩G φ ((suffix x w) [0 → (n - x)]))"
by (simp add: subsequence_def run_foldl; metis af_G_abs.f_foldl_abs.abs_eq af_G_abs.f_foldl_abs_alt_def af_G_letter_abs_def)
hence "Rep (token_run x n) ≡⇩P af⇩G φ ((suffix x w) [0 → (n - x)])"
using ltl⇩P_abs_rep ltl_prop_equiv_quotient.abs_eq_iff by auto
thus ?thesis
unfolding ltl_prop_equiv_def subsequence_shift by (cases "x ≤ n"; simp add: subsequence_def)
qed

end

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

sublocale mojmir_to_rabin Σ "↑af⇩G" "Abs φ" w "{q. 𝒢 ⊨⇩P Rep q}"
proof
show "⋀q ν. q ∈ {q. 𝒢 ⊨⇩P Rep q} ⟹ ↑af⇩Gq ν ∈ {q. 𝒢 ⊨⇩P Rep q}"
using wellformed_𝒢 af_G_letter_sat_core_lifted by auto
have nonempty_Σ: "Σ ≠ {}"
using bounded_w by blast
show "finite (reach Σ ↑af⇩G(Abs φ))" (is "finite ?A")
using af_G_abs.finite_abs_reach finite_subset[where A = ?A, where B = "lift_ltl_transformer.abs_reach af_G_letter (Abs φ)"]
unfolding af_G_abs.abs_reach_def af_G_letter_abs_def reach_foldl_def[OF nonempty_Σ] by blast
qed (insert finite_Σ bounded_w)

lemma ltl_to_rabin_correct_exposed':
"𝔓⇩∞ φ 𝒢 w ⟷ accept"
proof -
{
fix i
have "(∃j. 𝒢 ⊨⇩P af⇩G φ (map w [i + 0..<i + (j - i)])) = 𝔓 φ 𝒢 w i"
hence "(∃j. 𝒢 ⊨⇩P af⇩G φ (w [i → j])) ⟷ (∃j. 𝒢 ⊨⇩P run af_G_letter φ (suffix i w) (j-i))"
(is "?l ⟷ _")
unfolding run_foldl using subsequence_shift subsequence_def by metis
also
have "… ⟷ (∃j. 𝒢 ⊨⇩P Rep (run ↑af⇩G(Abs φ) (suffix i w) (j-i)))"
using Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_rep_abs]
unfolding ltl_prop_equiv_def run_af_G_letter_abs_eq_Abs_af_G_letter by blast
also
have "… ⟷ (∃j. token_run i j ∈ {q. 𝒢 ⊨⇩P Rep q})"
by simp
also
have "… ⟷ token_succeeds i"
(is "_ ⟷ ?r")
unfolding token_succeeds_def by auto
finally
have "?l ⟷ ?r" .
}
thus "?thesis"
by (simp only: almost_all_eventually_provable_def accept_def)
qed

lemma ltl_to_rabin_correct_exposed:
"𝔓⇩∞ φ 𝒢 w ⟷ accept⇩R (δ⇩R, q⇩R, {Acc⇩R i | i. i < max_rank⇩R}) w"
unfolding ltl_to_rabin_correct_exposed' mojmir_accept_iff_rabin_accept ..

― ‹Import lemmas from parent locale to simplify assumptions›
lemmas max_rank_lowerbound = max_rank_lowerbound
lemmas state_rank_step_foldl = state_rank_step_foldl
lemmas smallest_accepting_rank_properties = smallest_accepting_rank_properties
lemmas wellformed_ℛ = wellformed_ℛ

end

fun ltl_to_rabin
where
"ltl_to_rabin Σ φ 𝒢 = (ltl_FG_to_rabin_def.δ⇩R Σ φ, ltl_FG_to_rabin_def.q⇩R φ, {ltl_FG_to_rabin_def.Acc⇩R Σ φ 𝒢 i | i. i < ltl_FG_to_rabin_def.max_rank⇩R Σ φ})"

context
fixes
Σ :: "'a set set"
assumes
finite_Σ: "finite Σ"
begin

lemma ltl_to_rabin_correct:
assumes "range w ⊆ Σ"
shows "w ⊨ F G φ = (∃𝒢 ⊆ ❙G (G φ). G φ ∈ 𝒢 ∧ (∀ψ. G ψ ∈ 𝒢 ⟶ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w))"
proof -
have "⋀𝒢 ψ. 𝒢 ⊆ ❙G (G φ) ⟹ G ψ ∈ 𝒢 ⟹ (𝔓⇩∞ ψ 𝒢 w ⟷ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w)"
proof -
fix 𝒢 ψ
assume "𝒢 ⊆ ❙G (G φ)" "G ψ ∈ 𝒢"
then interpret ltl_FG_to_rabin Σ ψ 𝒢
using finite_Σ assms G_nested_propos_alt_def
by (unfold_locales; auto)
show "(𝔓⇩∞ ψ 𝒢 w ⟷ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w)"
using ltl_to_rabin_correct_exposed by simp
qed
thus ?thesis
using 𝒢_elements[of _ "G φ"] 𝒢_finite[of _ "G φ"]
unfolding ltl_FG_logical_characterization G_nested_propos.simps
by meson
qed

end

subsubsection ‹LTL-to-Mojmir Lemmas›

lemma ℱ_eq_𝒮:
assumes finite_Σ: "finite Σ"
assumes bounded_w: "range w ⊆ Σ"
assumes "closed 𝒢 w"
assumes "G ψ ∈ 𝒢"
shows "∀⇩∞j. (∀S. (S ⊨⇩P ℱ ψ w 𝒢 j ∧ 𝒢 ⊆ S) ⟷ (∀q. q ∈ (ltl_FG_to_rabin_def.𝒮⇩R Σ ψ 𝒢 w j) ⟶ S ⊨⇩P Rep q))"
proof -
let ?F = "{q. 𝒢 ⊨⇩P Rep q}"

define k where "k = the (threshold ψ w 𝒢)"
hence "threshold ψ w 𝒢 = Some k"
using assms unfolding threshold.simps index.simps almost_all_eventually_provable_def  by simp

have "Only_G 𝒢"
using assms G_nested_propos_alt_def by blast
then interpret ltl_FG_to_rabin Σ ψ 𝒢 w
using finite_Σ bounded_w by (unfold_locales, auto)

have "accept"
using ltl_to_rabin_correct_exposed' assms by blast
then obtain i where "smallest_accepting_rank = Some i"
unfolding smallest_accepting_rank_def by force

(* Wait until succeeding states can be recognised *)
obtain n⇩1 where "⋀m q. m ≥ n⇩1 ⟹ ((∃x ∈ configuration q m. token_succeeds x) ⟶ q ∈ 𝒮 m) ∧ (q ∈ 𝒮 m ⟶ (∀x ∈ configuration q m. token_succeeds x))"
using succeeding_states[OF ‹smallest_accepting_rank = Some i›] unfolding MOST_nat_le by blast
(* Wait until all "early" succeeding tokens reached the final states *)
obtain n⇩2 where "⋀x. x < k ⟹ token_succeeds x ⟹ token_run x n⇩2 ∈ ?F"
by (induction k) (simp, metis token_stays_in_final_states add.commute le_neq_implies_less not_less not_less_eq token_succeeds_def)

define n where "n = Max {n⇩1, n⇩2, k}"

(* Prove properties for the larger n *)
{
fix m q
assume "n ≤ m"
hence "n⇩1 ≤ m"
unfolding n_def by simp
hence "((∃x ∈ configuration q m. token_succeeds x) ⟶ q ∈ 𝒮 m) ∧ (q ∈ 𝒮 m ⟶ (∀x ∈ configuration q m. token_succeeds x))"
using ‹⋀m q. m ≥ n⇩1 ⟹ ((∃x ∈ configuration q m. token_succeeds x) ⟶ q ∈ 𝒮 m) ∧ (q ∈ 𝒮 m ⟶ (∀x ∈ configuration q m. token_succeeds x))› by blast
}
hence n_def_1: "⋀m q. m ≥ n ⟹ ((∃x ∈ configuration q m. token_succeeds x) ⟶ q ∈ 𝒮 m) ∧ (q ∈ 𝒮 m ⟶ (∀x ∈ configuration q m. token_succeeds x))"
by presburger
have n_def_2: "⋀x m. x < k ⟹ m ≥ n ⟹ token_succeeds x ⟹ token_run x m ∈ ?F"
using ‹⋀x. x < k ⟹ token_succeeds x ⟹ token_run x n⇩2 ∈ ?F› Max.coboundedI[of "{n⇩1, n⇩2, k}"]
using token_stays_in_final_states[of _ n⇩2] le_Suc_ex unfolding n_def by force

{
fix S m
assume "n ≤ m"
hence "k ≤ m" "n ≤ Suc m"
using n_def by simp+

{
assume "S ⊨⇩P ℱ ψ w 𝒢 m" "𝒢 ⊆ S"
hence "⋀x. k ≤ x ⟹ x ≤ Suc m ⟹ S ⊨⇩P af⇩G ψ (w [x → m])"
unfolding And_prop_entailment ℱ_def k_def[symmetric] subsequence_def
using ‹k ≤ m› by auto
fix q assume "q ∈ 𝒮 m"

have "S ⊨⇩P Rep q"
proof (cases "q ∈ ?F")
case False
moreover
from False obtain j where "state_rank q m = Some j" and "j ≥ i"
using ‹q ∈ 𝒮 m› ‹smallest_accepting_rank = Some i› by force
then obtain x where x: "x ∈ configuration q m" "token_run x m = q"
by force
moreover
from x have "token_succeeds x"
using n_def_1[OF ‹n ≤ m›] ‹q ∈ 𝒮 m› by blast
ultimately
have "S ⊨⇩P af⇩G ψ (w [x → m])"
using ‹⋀x. k ≤ x ⟹ x ≤ Suc m ⟹ S ⊨⇩P af⇩G ψ (w [x → m])›[of x] n_def_2[OF _ ‹n ≤ m›] by fastforce
thus ?thesis
using Rep_token_run_af unfolding ‹token_run x m = q›[symmetric] ltl_prop_equiv_def by simp
qed (insert ‹𝒢 ⊆ S›, blast)
}

moreover

{
assume "⋀q. q ∈ 𝒮 m ⟹ S ⊨⇩P Rep q"
hence "⋀q. q ∈ ?F ⟹ S ⊨⇩P Rep q"
by simp
have "𝒢 ⊆ S"
proof
fix x assume "x ∈ 𝒢"
with ‹Only_G 𝒢› show "x ∈ S"
using ‹⋀q. q ∈ ?F ⟹ S ⊨⇩P Rep q›[of "Abs x"] by auto
qed

{
fix x assume "k ≤ x" "x ≤ m"
define q where "q = token_run x m"

hence "token_succeeds x"
using threshold_properties[OF ‹threshold ψ w 𝒢 = Some k›] ‹x ≥ k› Rep_token_run_af
unfolding token_succeeds_def ltl_prop_equiv_def by blast
hence "q ∈ 𝒮 m"
using n_def_1[OF ‹n ≤ m›, of q] ‹x ≤ m›
unfolding q_def configuration.simps by blast
hence "S ⊨⇩P Rep q"
by (rule ‹⋀q. q ∈ 𝒮 m ⟹ S ⊨⇩P Rep q›)
hence "S ⊨⇩P af⇩G ψ (w [x → m])"
using Rep_token_run_af unfolding q_def ltl_prop_equiv_def by simp
}
hence "∀x ∈ (set (map (λi. af⇩G ψ (w [i → m])) [k..<Suc m])). S ⊨⇩P x"
unfolding set_map set_upt by fastforce
hence "S ⊨⇩P ℱ ψ w 𝒢 m" and "𝒢 ⊆ S"
unfolding ℱ_def And_prop_entailment[of S] k_def[symmetric]
using ‹k ≤ m› ‹𝒢 ⊆ S› by simp+
}
ultimately
have "(S ⊨⇩P ℱ ψ w 𝒢 m ∧ 𝒢 ⊆ S) ⟷ (∀q. q ∈ 𝒮 m ⟶ S ⊨⇩P Rep q)"
by blast
}
thus ?thesis
unfolding MOST_nat_le by blast
qed

lemma ℱ_eq_𝒮_generalized:
assumes finite_Σ: "finite Σ"
assumes bounded_w: "range w ⊆ Σ"
assumes "closed 𝒢 w"
shows "∀⇩∞j. ∀ψ. G ψ ∈ 𝒢 ⟶ (∀S. (S ⊨⇩P ℱ ψ w 𝒢 j ∧ 𝒢 ⊆ S) ⟷ (∀q. q ∈ (ltl_FG_to_rabin_def.𝒮⇩R Σ ψ 𝒢) w j ⟶ S ⊨⇩P Rep q))"
proof -
have "Only_G 𝒢" and "finite 𝒢"
using assms by simp+
show ?thesis
using almost_all_commutative''[OF ‹finite 𝒢› ‹Only_G 𝒢›] ℱ_eq_𝒮[OF assms] by simp
qed

subsection ‹Product of Secondary Automata›

context
fixes
Σ :: "'a set set"
begin

fun product_initial_state :: "'a set ⇒ ('a ⇒ 'b) ⇒ ('a ⇀ 'b)" ("ι⇩×")
where
"ι⇩× K q⇩m = (λk. if k ∈ K then Some (q⇩m k) else None)"

fun combine_pairs :: "(('a, 'b) transition set × ('a, 'b) transition set) set ⇒ (('a, 'b) transition set × ('a, 'b) transition set set)"
where
"combine_pairs P = (⋃(fst ` P), snd ` P)"

fun combine_pairs' :: "(('a ltl ⇒ ('a ltl_prop_equiv_quotient ⇒ nat option) option, 'a set) transition set × ('a ltl ⇒ ('a ltl_prop_equiv_quotient ⇒ nat option) option, 'a set) transition set) set ⇒ (('a ltl ⇒ ('a ltl_prop_equiv_quotient ⇒ nat option) option, 'a set) transition set × ('a ltl ⇒ ('a ltl_prop_equiv_quotient ⇒ nat option) option, 'a set) transition set set)"
where
"combine_pairs' P = (⋃(fst ` P), snd ` P)"

lemma combine_pairs_prop:
"(∀P ∈ 𝒫. accepting_pair⇩R δ q⇩0 P w) = accepting_pair⇩G⇩R δ q⇩0 (combine_pairs 𝒫) w"
by auto

lemma combine_pairs2:
"combine_pairs 𝒫 ∈ α ⟹ (⋀P. P ∈ 𝒫 ⟹ accepting_pair⇩R δ q⇩0 P w ) ⟹ accept⇩G⇩R (δ, q⇩0, α) w"
using combine_pairs_prop[of 𝒫 δ q⇩0 w] by fastforce

lemma combine_pairs'_prop:
"(∀P ∈ 𝒫. accepting_pair⇩R δ q⇩0 P w) = accepting_pair⇩G⇩R δ q⇩0 (combine_pairs' 𝒫) w"
by auto

fun ltl_FG_to_generalized_rabin :: "'a ltl ⇒ ('a ltl ⇀ 'a ltl⇩P ⇀ nat, 'a set) generalized_rabin_automaton" ("𝒫")
where
"ltl_FG_to_generalized_rabin φ = (
Δ⇩× (λχ. ltl_FG_to_rabin_def.δ⇩R Σ (theG χ)),
ι⇩× (❙G (G φ)) (λχ. ltl_FG_to_rabin_def.q⇩R (theG χ)),
{combine_pairs' {embed_pair χ (ltl_FG_to_rabin_def.Acc⇩R Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢}
| 𝒢 π. 𝒢 ⊆ ❙G (G φ) ∧ G φ ∈ 𝒢 ∧ (∀χ. π χ < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ))})"

context
assumes
finite_Σ: "finite Σ"
begin

lemma ltl_FG_to_generalized_rabin_wellformed:
"finite (reach Σ (fst (𝒫 φ)) (fst (snd (𝒫 φ))))"
proof (cases "Σ = {}")
case False
have "finite (reach Σ (Δ⇩× (λχ. ltl_FG_to_rabin_def.δ⇩R Σ (theG χ))) (fst (snd (𝒫 φ))))"
proof (rule finite_reach_product, goal_cases)
case 1
show ?case
using G_nested_finite(1) by (auto simp add: dom_def LTL_Rabin.product_initial_state.simps)
next
case (2 x)
hence "the (fst (snd (𝒫 φ)) x) = ltl_FG_to_rabin_def.q⇩R (theG x)"
thus ?case
using ltl_FG_to_rabin.wellformed_ℛ[unfolded ltl_FG_to_rabin_def, of "{}" _ Σ "theG x"] finite_Σ False by fastforce
qed
thus ?thesis
by fastforce

theorem ltl_FG_to_generalized_rabin_correct:
assumes "range w ⊆ Σ"
shows "w ⊨ F G φ = accept⇩G⇩R (𝒫 φ) w"
(is "?lhs = ?rhs")
proof
define r where "r = run⇩t (fst (𝒫 φ)) (fst (snd (𝒫 φ))) w"

have [intro]: "⋀i. w i ∈ Σ" and "Σ ≠ {}"
using assms by auto

{
let ?S = "(reach Σ (fst (𝒫 φ)) (fst (snd (𝒫 φ))) ) × Σ × (reach Σ (fst (𝒫 φ)) (fst (snd (𝒫 φ))))"

have "⋀n. r n ∈ ?S"
unfolding run⇩t.simps run_foldl reach_foldl_def[OF ‹Σ ≠ {}›] r_def by fastforce
hence "range r ⊆ ?S" and  "finite ?S"
using ltl_FG_to_generalized_rabin_wellformed assms ‹finite Σ› by (blast, fast)
}
hence "finite (range r)"
by (blast dest: finite_subset)

{
assume ?lhs
then obtain 𝒢 where "𝒢 ⊆ ❙G (G φ)" and "G φ ∈ 𝒢" and "∀ψ. G ψ ∈ 𝒢 ⟶ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w"
unfolding ltl_to_rabin_correct[OF ‹finite Σ› ‹range w ⊆ Σ›] unfolding ltl_to_rabin.simps by auto

note 𝒢_properties[OF ‹𝒢 ⊆ ❙G (G φ)›]
hence "ltl_FG_to_rabin Σ 𝒢 w"
using ‹finite Σ› ‹range w ⊆ Σ› unfolding ltl_FG_to_rabin_def by auto

define π where "π ψ =
(if ψ ∈ 𝒢 then the (ltl_FG_to_rabin_def.smallest_accepting_rank⇩R Σ (theG ψ) 𝒢 w) else 0)"
for ψ
let ?P' = "{❙↿⇩χ (ltl_FG_to_rabin_def.Acc⇩R Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢}"

have "∀P ∈ ?P'. accepting_pair⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
proof
fix P
assume "P ∈ ?P'"
then obtain χ where P_def: "P = ❙↿⇩χ (ltl_FG_to_rabin_def.Acc⇩R Σ (theG χ) 𝒢 (π χ))"
and "χ ∈ 𝒢"
by blast
hence "∃χ'. χ = G χ'"
using ‹𝒢 ⊆ ❙G (G φ)› G_nested_propos_alt_def by auto

interpret ltl_FG_to_rabin Σ "theG χ" 𝒢 w
by (insert ‹ltl_FG_to_rabin Σ 𝒢 w›)

define r⇩χ where "r⇩χ = run⇩t δ⇩ℛ q⇩ℛ w"

moreover

have "accept" and "accept⇩R (δ⇩ℛ, q⇩ℛ, {Acc⇩ℛ j | j. j < max_rank}) w"
using ‹χ ∈ 𝒢› ‹∃χ'. χ = G χ'› ‹∀ψ. G ψ ∈ 𝒢 ⟶ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w›
using mojmir_accept_iff_rabin_accept by auto

hence "smallest_accepting_rank⇩ℛ = Some (π χ)"
unfolding π_def smallest_accepting_rank_def Mojmir_rabin_smallest_accepting_rank[symmetric]
using ‹χ ∈ 𝒢› by simp
hence "accepting_pair⇩R δ⇩ℛ q⇩ℛ (Acc⇩ℛ (π χ)) w"
using ‹accept⇩R (δ⇩ℛ, q⇩ℛ, {Acc⇩ℛ j | j. j < max_rank}) w› LeastI[of "λi. accepting_pair⇩R δ⇩ℛ q⇩ℛ (Acc⇩ℛ i) w"]

ultimately

have "limit r⇩χ ∩ fst (Acc⇩ℛ (π χ)) = {}" and "limit r⇩χ ∩ snd (Acc⇩ℛ (π χ)) ≠ {}"
by simp+

moreover

have 1: "(ι⇩× (❙G (G φ)) (λχ. ltl_FG_to_rabin_def.q⇩R (theG χ))) χ = Some q⇩ℛ"
using ‹χ ∈ 𝒢› ‹𝒢 ⊆ ❙G (G φ)› by (simp add: LTL_Rabin.product_initial_state.simps subset_iff)
have 2: "finite (range (run⇩t
(Δ⇩× (λχ. ltl_FG_to_rabin_def.δ⇩R Σ (theG χ)))
(ι⇩× (❙G (G φ)) (λχ. ltl_FG_to_rabin_def.q⇩R (theG χ)))
w))"
using ‹finite (range r)›[unfolded r_def] by simp

ultimately
have "limit r ∩ fst P = {}" and "limit r ∩ snd P ≠ {}"
using product_run_embed_limit_finiteness[OF 1 2]
unfolding r_def r⇩χ_def P_def by auto
thus "accepting_pair⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
unfolding P_def r_def by simp
qed
hence "accepting_pair⇩G⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) (combine_pairs' ?P') w"
using combine_pairs'_prop by blast
moreover
{
fix ψ
assume "ψ ∈ 𝒢"
hence "∃χ. ψ = G χ"
using ‹𝒢 ⊆ ❙G (G φ)› G_nested_propos_alt_def by auto

interpret ltl_FG_to_rabin Σ "theG ψ" 𝒢 w
by (insert ‹ltl_FG_to_rabin Σ 𝒢 w›)

have "accept"
using ‹ψ ∈ 𝒢› ‹∃χ. ψ = G χ› ‹∀ψ. G ψ ∈ 𝒢 ⟶ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w›  mojmir_accept_iff_rabin_accept by auto
then obtain i where "smallest_accepting_rank = Some i"
unfolding smallest_accepting_rank_def by fastforce
hence "π ψ < max_rank⇩R"
using smallest_accepting_rank_properties π_def ‹ψ ∈ 𝒢› by auto
}
hence "⋀χ. π χ < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)"
unfolding π_def using ltl_FG_to_rabin.max_rank_lowerbound[OF ‹ltl_FG_to_rabin Σ 𝒢 w›] by force
hence "combine_pairs' ?P' ∈ snd (snd (𝒫 φ))"
using ‹𝒢 ⊆ ❙G (G φ)› ‹G φ ∈ 𝒢› by auto
ultimately
show ?rhs
unfolding accept⇩G⇩R_simp2 ltl_FG_to_generalized_rabin.simps fst_conv snd_conv by blast
}

{
assume ?rhs
then obtain 𝒢 π P where "P = combine_pairs' {❙↿⇩χ (ltl_FG_to_rabin_def.Acc⇩R Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢}" (is "P = combine_pairs' ?P'")
and "accepting_pair⇩G⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
and "𝒢 ⊆ ❙G (G φ)" and "G φ ∈ 𝒢" and "⋀χ. π χ < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)"
unfolding accept⇩G⇩R_def by auto
moreover
hence P'_def: "⋀P. P ∈ ?P' ⟹ accepting_pair⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
using combine_pairs'_prop by meson
note 𝒢_properties[OF ‹𝒢 ⊆ ❙G (G φ)›]
hence "ltl_FG_to_rabin Σ 𝒢 w"
using ‹finite Σ› ‹range w ⊆ Σ› unfolding ltl_FG_to_rabin_def by auto
have "∀ψ. G ψ ∈ 𝒢 ⟶ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w"
proof (rule+)
fix ψ
assume "G ψ ∈ 𝒢"
define χ where "χ = G ψ"
define P where "P = ❙↿⇩χ (ltl_FG_to_rabin_def.Acc⇩R Σ ψ 𝒢 (π χ))"
hence "χ ∈ 𝒢" and "theG χ = ψ"
using χ_def ‹G ψ ∈ 𝒢› by simp+
hence "P ∈ ?P'"
unfolding P_def by auto
hence "accepting_pair⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
using P'_def by blast

interpret ltl_FG_to_rabin Σ ψ 𝒢 w
by (insert ‹ltl_FG_to_rabin Σ 𝒢 w›)

define r⇩χ where "r⇩χ = run⇩t δ⇩ℛ q⇩ℛ w"

have "limit r ∩ fst P = {}" and "limit r ∩ snd P ≠ {}"
using ‹accepting_pair⇩R (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w›
unfolding r_def accepting_pair⇩R_def by metis+

moreover

have 1: "(ι⇩× (❙G (G φ)) (λχ. ltl_FG_to_rabin_def.q⇩R (theG χ))) (G ψ) = Some q⇩ℛ"
using ‹G ψ ∈ 𝒢› ‹𝒢 ⊆ ❙G (G φ)› by (auto simp add: LTL_Rabin.product_initial_state.simps subset_iff)
have 2: "finite (range (run⇩t (Δ⇩× (λχ. ltl_FG_to_rabin_def.δ⇩R Σ (theG χ))) (ι⇩× (❙G (G φ)) (λχ. ltl_FG_to_rabin_def.q⇩R (theG χ)))  w))"
using ‹finite (range r)›[unfolded r_def] by simp
have "⋀S. limit r ∩ (⋃ (↿⇩χ ` S)) = {} ⟷ limit r⇩χ ∩ S = {}"
using product_run_embed_limit_finiteness[OF 1 2] by (simp add: r_def r⇩χ_def χ_def)

ultimately
have "limit r⇩χ ∩ fst (Acc⇩ℛ (π χ)) = {}" and "limit r⇩χ ∩ snd (Acc⇩ℛ (π χ)) ≠ {}"
unfolding P_def fst_conv snd_conv embed_pair.simps by meson+
hence "accepting_pair⇩R δ⇩ℛ q⇩ℛ (Acc⇩ℛ (π χ)) w"
unfolding r⇩χ_def by simp
hence "accept⇩R (δ⇩ℛ, q⇩ℛ, {Acc⇩ℛ j | j. j < max_rank}) w"
using ‹⋀χ. π χ < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)› ‹theG χ = ψ›
unfolding accept⇩R_simp accepting_pair⇩R_def fst_conv snd_conv by blast
thus "accept⇩R (ltl_to_rabin Σ ψ 𝒢) w"
by simp
qed
ultimately
show ?lhs
unfolding ltl_to_rabin_correct[OF ‹finite Σ› assms] by auto
}
qed

end

end

subsection ‹Automaton Template›

― ‹This locale provides the construction template for all composed constructions.›

locale ltl_to_rabin_base_def =
fixes
δ :: "'a ltl⇩P ⇒ 'a set ⇒ 'a ltl⇩P"
fixes
δ⇩M :: "'a ltl⇩P ⇒ 'a set ⇒ 'a ltl⇩P"
fixes
q⇩0 :: "'a ltl ⇒ 'a ltl⇩P"
fixes
q⇩0⇩M :: "'a ltl ⇒ 'a ltl⇩P"
fixes
M_fin :: "('a ltl ⇀ nat) ⇒ ('a ltl⇩P × ('a ltl ⇀ 'a ltl⇩P ⇀ nat), 'a set) transition set"
begin

― ‹Transition Function and Initial State›

fun delta
where
"delta Σ = δ × Δ⇩× (semi_mojmir_def.step Σ δ⇩M o q⇩0⇩M o theG)"

fun initial
where
"initial φ = (q⇩0 φ, ι⇩× (❙G φ) (semi_mojmir_def.initial o q⇩0⇩M o theG))"

― ‹Acceptance Condition›

definition max_rank_of
where
"max_rank_of Σ ψ ≡ semi_mojmir_def.max_rank Σ δ⇩M (q⇩0⇩M (theG ψ))"

fun Acc_fin
where
"Acc_fin Σ π χ = ⋃(embed_transition_snd ` ⋃(embed_transition χ `
(mojmir_to_rabin_def.fail⇩R Σ δ⇩M (q⇩0⇩M (theG χ)) {q. dom π ↑⊨⇩P q}
∪ mojmir_to_rabin_def.merge⇩R δ⇩M (q⇩0⇩M (theG χ)) {q. dom π ↑⊨⇩P q} (the (π χ)))))"

fun Acc_inf
where
"Acc_inf π χ = ⋃(embed_transition_snd ` ⋃(embed_transition χ `
(mojmir_to_rabin_def.succeed⇩R δ⇩M (q⇩0⇩M (theG χ)) {q. dom π ↑⊨⇩P q} (the (π χ)))))"

abbreviation Acc
where
"Acc Σ π χ ≡ (Acc_fin Σ π χ, Acc_inf π χ)"

fun rabin_pairs :: "'a set set ⇒ 'a ltl ⇒ ('a ltl⇩P × ('a ltl ⇀ 'a ltl⇩P ⇀ nat), 'a set) generalized_rabin_condition"
where
"rabin_pairs Σ φ = {(M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π})
| π. dom π ⊆ ❙G φ ∧ (∀χ ∈ dom π. the (π χ) < max_rank_of Σ χ)}"

fun ltl_to_generalized_rabin :: "'a set set ⇒ 'a ltl ⇒ ('a ltl⇩P × ('a ltl ⇀ 'a ltl⇩P ⇀ nat), 'a set) generalized_rabin_automaton" ("𝒜")
where
"𝒜 Σ φ = (delta Σ, initial φ, rabin_pairs Σ φ)"

end

locale ltl_to_rabin_base = ltl_to_rabin_base_def +
fixes
Σ :: "'a set set"
fixes
w :: "'a set word"
assumes
finite_Σ: "finite Σ"
assumes
bounded_w: "range w ⊆ Σ"
assumes
M_fin_monotonic: "dom π = dom π' ⟹ (⋀χ. χ ∈ dom π ⟹ the (π χ) ≤ the (π' χ)) ⟹ M_fin π ⊆ M_fin π'"
assumes
finite_reach': "finite (reach Σ δ (q⇩0 φ))"
assumes
mojmir_to_rabin: "Only_G 𝒢 ⟹ mojmir_to_rabin Σ δ⇩M (q⇩0⇩M ψ) w {q. 𝒢 ↑⊨⇩P q}"
begin

lemma semi_mojmir:
"semi_mojmir Σ δ⇩M (q⇩0⇩M ψ) w"
using mojmir_to_rabin[of "{}"] by (simp add: mojmir_to_rabin_def mojmir_def)

lemma finite_reach:
"finite (reach Σ (delta Σ) (initial φ))"
apply (cases "Σ = {}")
apply (simp only: ltl_to_rabin_base_def.initial.simps ltl_to_rabin_base_def.delta.simps)
apply (rule finite_reach_simple_product[OF finite_reach' finite_reach_product])
apply (insert mojmir_to_rabin[of "{}", unfolded mojmir_to_rabin_def mojmir_def])
apply (auto simp add: dom_def intro: G_nested_finite semi_mojmir.wellformed_ℛ)
done

lemma run_limit_not_empty:
"limit (run⇩t (delta Σ) (initial φ) w) ≠ {}"
by (metis emptyE finite_Σ limit_nonemptyE finite_reach bounded_w run⇩t_finite)

lemma run_properties:
fixes φ
defines "r ≡ run (delta Σ) (initial φ) w"
shows "fst (r i) = foldl δ (q⇩0 φ) (w [0 → i])"
and "⋀χ q. χ ∈ ❙G φ ⟹ the (snd (r i) χ) q = semi_mojmir_def.state_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w q i"
proof -
have sm: "⋀ψ. semi_mojmir Σ δ⇩M (q⇩0⇩M ψ) w"
using mojmir_to_rabin[of "{}"] unfolding mojmir_to_rabin_def mojmir_def by simp
have "r i = (foldl δ (q⇩0 φ) (w [0 → i]),
λχ. if χ ∈ ❙G φ then Some (λψ. foldl (semi_mojmir_def.step Σ δ⇩M (q⇩0⇩M (theG χ))) (semi_mojmir_def.initial (q⇩0⇩M (theG χ))) (map w [0..< i]) ψ) else None)"
proof (induction i)
case (Suc i)
show ?case
unfolding r_def run_foldl upt_Suc less_eq_nat.simps if_True map_append foldl_append
unfolding Suc[unfolded r_def run_foldl] subsequence_def by auto
qed (auto simp add: subsequence_def r_def)
hence state_run: "r i = (foldl δ (q⇩0 φ) (w [0 → i]),
λχ. if χ ∈ ❙G φ then Some (λψ. semi_mojmir_def.state_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w ψ i) else None)"
unfolding semi_mojmir.state_rank_step_foldl[OF sm] r_def by simp

show "fst (r i) = foldl δ (q⇩0 φ) (w [0 → i])"
using state_run by fastforce
show "⋀χ q. χ ∈ ❙G φ ⟹ the (snd (r i) χ) q = semi_mojmir_def.state_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w q i"
unfolding state_run by force
qed

lemma accept⇩G⇩R_I:
assumes "accept⇩G⇩R (𝒜 Σ φ) w"
obtains π where "dom π ⊆ ❙G φ"
and "⋀χ. χ ∈ dom π ⟹ the (π χ) < max_rank_of Σ χ"
and "accepting_pair⇩R (delta Σ) (initial φ) (M_fin π, UNIV) w"
and "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π χ) w"
proof -
from assms obtain P where "P ∈ rabin_pairs Σ φ" and "accepting_pair⇩G⇩R (delta Σ) (initial φ) P w"
unfolding accept⇩G⇩R_def ltl_to_generalized_rabin.simps fst_conv snd_conv by blast
moreover
then obtain π where "dom π ⊆ ❙G φ" and "∀χ ∈ dom π. the (π χ) < max_rank_of Σ χ"
and P_def: "P = (M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π})"
by auto
have "limit (run⇩t (delta Σ) (initial φ) w) ∩ UNIV ≠ {}"
using run_limit_not_empty assms by simp
ultimately
have "accepting_pair⇩R (delta Σ) (initial φ) (M_fin π, UNIV) w"
and "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π χ) w"
unfolding P_def accepting_pair⇩G⇩R_simp accepting_pair⇩R_simp by blast+ (* Slow... *)
thus ?thesis
using that ‹dom π ⊆ ❙G φ› ‹∀χ ∈ dom π. the (π χ) < max_rank_of Σ χ› by blast
qed

context
fixes
φ :: "'a ltl"
begin

context
fixes
ψ :: "'a ltl"
fixes
π :: "'a ltl ⇀ nat"
assumes
"G ψ ∈ dom π"
assumes
"dom π ⊆ ❙G φ"
begin

interpretation 𝔐: mojmir_to_rabin Σ δ⇩M "q⇩0⇩M ψ" w "{q. dom π ↑⊨⇩P q}"
by (metis mojmir_to_rabin ‹dom π ⊆ ❙G φ› 𝒢_elements)

lemma Acc_property:
"accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π (G ψ)) w ⟷ accepting_pair⇩R 𝔐.δ⇩ℛ 𝔐.q⇩ℛ (𝔐.Acc⇩ℛ (the (π (G ψ)))) w"
(is "?Acc = ?Acc⇩ℛ")
proof -
define r r⇩ψ where "r = run⇩t (delta Σ) (initial φ) w" and "r⇩ψ = run⇩t 𝔐.δ⇩ℛ 𝔐.q⇩ℛ w"
hence "finite (range r)"
using run⇩t_finite[OF finite_reach] bounded_w finite_Σ
by (blast dest: finite_subset)

have "⋀S. limit r⇩ψ ∩ S = {} ⟷ limit r ∩ ⋃(embed_transition_snd ` (⋃ ((embed_transition (G ψ)) ` S))) = {}"
proof -
fix S
have 1: "snd (initial φ) (G ψ) = Some 𝔐.q⇩ℛ"
using ‹G ψ ∈ dom π› ‹dom π ⊆ ❙G φ› by auto
have 2: "finite (range (run⇩t (Δ⇩× (semi_mojmir_def.step Σ δ⇩M o q⇩0⇩M o theG)) (snd (initial φ)) w))"
using ‹finite (range r)› r_def comp_apply
by (auto intro: product_run_finite_snd cong del: image_cong_simp)
show "?thesis S"
unfolding r_def r⇩ψ_def product_run_embed_limit_finiteness[OF 1 2, unfolded ltl.sel comp_def, symmetric]
using product_run_embed_limit_finiteness_snd[OF  ‹finite (range r)›[unfolded r_def delta.simps initial.simps]]
by (auto simp del: simple_product.simps product.simps product_initial_state.simps simp add: comp_def cong del: SUP_cong_simp)
qed
hence "limit r ∩ fst (Acc Σ π (G ψ)) = {} ∧ limit r ∩ snd (Acc Σ π (G ψ)) ≠ {}
⟷ limit r⇩ψ ∩ fst (𝔐.Acc⇩ℛ (the (π (G ψ)))) = {} ∧ limit r⇩ψ ∩ snd (𝔐.Acc⇩ℛ (the (π (G ψ)))) ≠ {}"
unfolding fst_conv snd_conv by simp
thus "?Acc ⟷ ?Acc⇩ℛ"
unfolding r⇩ψ_def r_def accepting_pair⇩R_def by blast
qed

lemma Acc_to_rabin_accept:
"⟦accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π (G ψ)) w; the (π (G ψ)) < 𝔐.max_rank⟧ ⟹ accept⇩R 𝔐.ℛ w"
unfolding Acc_property by auto

lemma Acc_to_mojmir_accept:
"⟦accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π (G ψ)) w; the (π (G ψ)) < 𝔐.max_rank⟧ ⟹ 𝔐.accept"
using Acc_to_rabin_accept unfolding 𝔐.mojmir_accept_iff_rabin_accept by auto

lemma rabin_accept_to_Acc:
"⟦accept⇩R 𝔐.ℛ w; π (G ψ) = 𝔐.smallest_accepting_rank⟧ ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π (G ψ)) w"
unfolding Acc_property 𝔐.Mojmir_rabin_smallest_accepting_rank
using 𝔐.smallest_accepting_rank⇩ℛ_properties 𝔐.smallest_accepting_rank⇩ℛ_def
by (metis (no_types, lifting) option.sel)

lemma mojmir_accept_to_Acc:
"⟦𝔐.accept; π (G ψ) = 𝔐.smallest_accepting_rank⟧ ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π (G ψ)) w"
unfolding 𝔐.mojmir_accept_iff_rabin_accept by (blast dest: rabin_accept_to_Acc)

end

lemma normalize_π:
assumes dom_subset: "dom π ⊆ ❙G φ"
assumes "⋀χ. χ ∈ dom π ⟹ the (π χ) < max_rank_of Σ χ"
assumes "accepting_pair⇩R (delta Σ) (initial φ) (M_fin π, UNIV) w"
assumes "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π χ) w"
obtains π⇩𝒜 where "dom π = dom π⇩𝒜"
and "⋀χ. χ ∈ dom π⇩𝒜 ⟹ π⇩𝒜 χ = mojmir_def.smallest_accepting_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w {q. dom π⇩𝒜 ↑⊨⇩P q}"
and "accepting_pair⇩R (delta Σ) (initial φ) (M_fin π⇩𝒜, UNIV) w"
and "⋀χ. χ ∈ dom π⇩𝒜 ⟹ accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π⇩𝒜 χ) w"
proof -
define 𝒢 where "𝒢 = dom π"
note 𝒢_properties[OF dom_subset]

define π⇩𝒜
where "π⇩𝒜 = (λχ.  mojmir_def.smallest_accepting_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w {q. dom π ↑⊨⇩P q}) |` 𝒢"

moreover

{
fix χ assume "χ ∈ dom π"

interpret 𝔐: mojmir_to_rabin Σ δ⇩M "q⇩0⇩M (theG χ)" w "{q. dom π ↑⊨⇩P q}"
by (metis mojmir_to_rabin ‹dom π ⊆ ❙G φ› 𝒢_elements)

from ‹χ ∈ dom π› have "accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π χ) w"
using assms(4) by blast
hence "accepting_pair⇩R 𝔐.δ⇩ℛ 𝔐.q⇩ℛ (𝔐.Acc⇩ℛ (the (π χ))) w"
by (metis ‹χ ∈ dom π› Acc_property[OF _ dom_subset] ‹Only_G (dom π)› ltl.sel(8))
moreover
hence "accept⇩R (𝔐.δ⇩ℛ, 𝔐.q⇩ℛ, {𝔐.Acc⇩ℛ j | j. j < 𝔐.max_rank}) w"
using assms(2)[OF ‹χ ∈ dom π›] unfolding max_rank_of_def by auto
ultimately
have "the (𝔐.smallest_accepting_rank⇩ℛ) ≤ the (π χ)" and "𝔐.smallest_accepting_rank ≠ None"
using Least_le[of _ "the (π χ)"] assms(2)[OF ‹χ ∈ dom π›] 𝔐.mojmir_accept_iff_rabin_accept option.distinct(1) 𝔐.smallest_accepting_rank_def
hence "the (π⇩𝒜 χ) ≤ the (π χ)" and "χ ∈ dom π⇩𝒜"
unfolding π⇩𝒜_def dom_restrict using assms(2) ‹χ ∈ dom π› by (simp add: 𝔐.Mojmir_rabin_smallest_accepting_rank 𝒢_def, subst dom_def, simp add: 𝒢_def)
}

hence "dom π = dom π⇩𝒜"
unfolding π⇩𝒜_def dom_restrict 𝒢_def by auto

moreover

note 𝒢_properties[OF dom_subset, unfolded ‹dom π = dom π⇩𝒜›]

have "M_fin π⇩𝒜 ⊆ M_fin π"
using ‹dom π = dom π⇩𝒜› by (simp add: M_fin_monotonic ‹⋀χ. χ ∈ dom π ⟹ the (π⇩𝒜 χ) ≤ the (π χ)›)
hence "accepting_pair⇩R (delta Σ) (initial φ) (M_fin π⇩𝒜, UNIV) w"
using assms unfolding accepting_pair⇩R_simp by blast

moreover

― ‹Goal 2›
{
fix χ assume "χ ∈ dom π⇩𝒜"
hence "χ = G (theG χ)"
unfolding ‹dom π = dom π⇩𝒜›[symmetric] ‹Only_G (dom π)› by (metis ‹Only_G (dom π⇩𝒜)› ‹χ ∈ dom π⇩𝒜› ltl.collapse(6) ltl.disc(58))
moreover
hence "G (theG χ) ∈ dom π⇩𝒜"
using ‹χ ∈ dom π⇩𝒜› by simp
moreover
hence X: "mojmir_def.accept δ⇩M (q⇩0⇩M (theG χ)) w {q. dom π ↑⊨⇩P q}"
using assms(1,2,4) ‹dom π ⊆ ❙G φ› ltl.sel(8) Acc_to_mojmir_accept ‹dom π = dom π⇩𝒜› by (metis max_rank_of_def)
have Y: "π⇩𝒜 (G theG χ) = mojmir_def.smallest_accepting_rank Σ δ⇩M (q⇩0⇩M (theG χ)) w {q. dom π⇩𝒜 ↑⊨⇩P q}"
using ‹G (theG χ) ∈ dom π⇩𝒜› ‹χ = G (theG χ)› π⇩𝒜_def ‹dom π = dom π⇩𝒜›[symmetric] by simp
ultimately
have "accepting_pair⇩R (delta Σ) (initial φ) (Acc Σ π⇩𝒜 χ) w"
using mojmir_accept_to_Acc[OF ‹G (theG χ) ∈ dom π⇩𝒜› ‹dom π ⊆ ❙G φ›[unfolded ‹dom π = dom π⇩𝒜›] X[unfolded ‹dom π = dom π⇩𝒜›] Y] by simp
}

ultimately

show ?thesis
using that[of π⇩𝒜] restrict_in unfolding ‹dom π = dom π⇩𝒜› 𝒢_def
by (metis (no_types, lifting))
qed

end

end

subsection ‹Generalized Deterministic Rabin Automaton›

― ‹Instantiate Automaton Template›

subsubsection ‹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 χ ∧ (∀q. (∃j ≥ the (π χ). the (m χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G (dom π) q)) ⟶ S ↑⊨⇩P φ')}"

locale ltl_to_rabin_af = ltl_to_rabin_base "↑af" "↑af⇩G" "Abs" "Abs" M_fin begin

abbreviation "δ⇩𝒜 ≡ delta"
abbreviation "ι⇩𝒜 ≡ initial"
abbreviation "Acc⇩𝒜 ≡ Acc"
abbreviation "F⇩𝒜 ≡ rabin_pairs"
abbreviation "𝒜 ≡ ltl_to_generalized_rabin"

subsubsection ‹Correctness Theorem›

theorem ltl_to_generalized_rabin_correct:
"w ⊨ φ = accept⇩G⇩R (ltl_to_generalized_rabin Σ φ) w"
(is "?lhs = ?rhs")
proof
let ?Δ = "δ⇩𝒜 Σ"
let ?q⇩0 = "ι⇩𝒜 φ"
let ?F = "F⇩𝒜 Σ φ"

― ‹Preliminary facts needed by both proof directions›
define r where "r = run⇩t ?Δ ?q⇩0 w"
have r_alt_def': "⋀i. fst (fst (r i)) = Abs (af φ (w [0 → i]))"
using run_properties(1) unfolding r_def run⇩t.simps fst_conv
by (metis af_abs.f_foldl_abs.abs_eq af_abs.f_foldl_abs_alt_def af_letter_abs_def)
have r_alt_def'': "⋀χ i q. χ ∈ ❙G φ ⟹ the (snd (fst (r i)) χ) q = semi_mojmir_def.state_rank Σ ↑af⇩G(Abs (theG χ)) w q i"
using run_properties(2) r_def by force
have φ'_def: "⋀i. af φ (w [0 → i]) ≡⇩P Rep (fst (fst (r i)))"
by (metis r_alt_def' Quotient3_ltl_prop_equiv_quotient ltl_prop_equiv_quotient.abs_eq_iff Quotient3_abs_rep)

have "finite (range r)"
using run⇩t_finite[OF finite_reach] bounded_w finite_Σ

― ‹Assuming @{term "w ⊨ φ"} holds, we prove that @{term "ltl_to_generalized_rabin Σ φ"} accepts @{term w}›
{
assume ?lhs
then obtain 𝒢 where "𝒢 ⊆ ❙G φ" and "accept⇩M φ 𝒢 w" and "closed 𝒢 w"
unfolding ltl_logical_characterization by blast

note 𝒢_properties[OF ‹𝒢 ⊆ ❙G φ›]
hence "ltl_FG_to_rabin Σ 𝒢 w"
using finite_Σ bounded_w unfolding ltl_FG_to_rabin_def by auto

define π
where "π χ = (if χ ∈ 𝒢 then (ltl_FG_to_rabin_def.smallest_accepting_rank⇩R Σ (theG χ) 𝒢 w) else None)"
for χ

have 𝔐_accept: "⋀ψ. G ψ ∈ 𝒢 ⟹ ltl_FG_to_rabin_def.accept⇩R' ψ 𝒢 w"
using ‹closed 𝒢 w› ‹ltl_FG_to_rabin Σ 𝒢 w› ltl_FG_to_rabin.ltl_to_rabin_correct_exposed' by blast
have "⋀ψ. G ψ ∈ 𝒢 ⟹ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w"
using ‹closed 𝒢 w› unfolding ltl_FG_to_rabin.ltl_to_rabin_correct_exposed[OF ‹ltl_FG_to_rabin Σ 𝒢 w›] by simp

{
fix ψ assume "G ψ ∈ 𝒢"
interpret 𝔐: ltl_FG_to_rabin Σ ψ 𝒢 w
by (insert ‹ltl_FG_to_rabin Σ 𝒢 w›)
obtain i where "𝔐.smallest_accepting_rank = Some i"
using 𝔐_accept[OF ‹G ψ ∈ 𝒢›]
unfolding 𝔐.smallest_accepting_rank_def by fastforce
hence "the (π (G ψ)) < 𝔐.max_rank" and "π (G ψ) ≠ None"
using 𝔐.smallest_accepting_rank_properties ‹G ψ ∈ 𝒢›
unfolding π_def by simp+
}
hence "𝒢 = dom π" and "⋀χ. χ ∈ 𝒢 ⟹ the (π χ) < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)"
using ‹Only_G 𝒢› π_def unfolding dom_def by auto

hence "(M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π}) ∈ ?F"
using ‹𝒢 ⊆ ❙G φ› max_rank_of_def by auto

moreover

{
have "accepting_pair⇩R ?Δ ?q⇩0 (M_fin π, UNIV) w"
proof -
(* Wait until the Mojmir automata provide enough information *)
obtain i where i_def:
"⋀j. j ≥ i ⟹ ∀S. (∀ψ. G ψ ∈ 𝒢 ⟶ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G 𝒢 (ℱ ψ w 𝒢 j)) ⟶ S ⊨⇩P af φ (w [0 → j])"
using ‹accept⇩M φ 𝒢 w› unfolding MOST_nat_le accept⇩M_def by blast

(* Wait until the states with succeeding tokens are (prop.) equivalent to ℱ *)
obtain i' where i'_def:
"⋀j ψ S. j ≥ i' ⟹ G ψ ∈ 𝒢 ⟹ (S ⊨⇩P ℱ ψ w 𝒢 j ∧ 𝒢 ⊆ S) = (∀q. q ∈ ltl_FG_to_rabin_def.𝒮⇩R Σ ψ 𝒢 w j ⟶ S ⊨⇩P Rep q)"
using ℱ_eq_𝒮_generalized[OF finite_Σ bounded_w ‹closed 𝒢 w›] unfolding MOST_nat_le by presburger

(* From now on the run does not visit forbidden states *)
have "⋀j. j ≥ max i i' ⟹ r j ∉ M_fin π"
proof -
fix j
assume "j ≥ max i i'"

let ?φ' = "fst (fst (r j))"
let ?m = "snd (fst (r j))"

{
fix S
assume "⋀χ. χ ∈ 𝒢 ⟹ S ↑⊨⇩P Abs χ"
hence assm1: "⋀χ. χ ∈ 𝒢 ⟹ S ⊨⇩P χ"
using ltl_prop_entails_abs.abs_eq by blast
assume "⋀χ. χ ∈ 𝒢 ⟹ ∀q. (∃j ≥ the (π χ). the (?m χ) q = Some j) ⟶ S ↑⊨⇩P ↑eval⇩G 𝒢 q"
hence assm2: "⋀χ. χ ∈ 𝒢 ⟹ ∀q. (∃j ≥ the (π χ). the (?m χ) q = Some j) ⟶ S ⊨⇩P eval⇩G 𝒢 (Rep q)"
unfolding ltl_prop_entails_abs.rep_eq eval⇩G_abs_def by simp

{
fix ψ
assume "G ψ ∈ 𝒢"
hence "G ψ ∈ ❙G φ" and "𝒢 ⊆ S"
using ‹𝒢 ⊆ ❙G φ› assm1 ‹Only_G 𝒢› by (blast, force)

interpret 𝔐: ltl_FG_to_rabin Σ ψ 𝒢 w
by (unfold_locales; insert ‹Only_G 𝒢› finite_Σ bounded_w; blast)

have "⋀S. (⋀q. q ∈ 𝔐.𝒮 j ⟹ S ⊨⇩P Rep q) ⟹ S ⊨⇩P ℱ ψ w 𝒢 j"
using i'_def ‹G ψ ∈ 𝒢› ‹j ≥ max i i'› max.bounded_iff by metis
hence "⋀S. (⋀q. q ∈ Rep ` 𝔐.𝒮 j ⟹ S ⊨⇩P q) ⟹ S ⊨⇩P ℱ ψ w 𝒢 j"
by simp

moreover

have 𝒮_def: "𝔐.𝒮 j = {q. 𝒢 ⊨⇩P Rep q} ∪ {q . ∃j'. the (π (G ψ)) ≤ j' ∧ the (?m (G ψ)) q = Some j'}"
using r_alt_def''[OF ‹G ψ ∈ ❙G φ›, unfolded ltl.sel, of j] ‹G ψ ∈ 𝒢› by (simp add: π_def)
have "⋀q. 𝒢 ⊨⇩P Rep q ⟹ S ⊨⇩P eval⇩G 𝒢 (Rep q)"
using ‹𝒢 ⊆ S› eval⇩G_prop_entailment by blast
hence "⋀q. q ∈ Rep ` 𝔐.𝒮 j ⟹ S ⊨⇩P eval⇩G 𝒢 q"
using assm2 ‹G ψ ∈ 𝒢› unfolding 𝒮_def by auto

ultimately
have "S ⊨⇩P eval⇩G 𝒢 (ℱ ψ w 𝒢 j)"
by (rule eval⇩G_respectfulness_generalized)
}
hence "S ⊨⇩P af φ (w [0 → j])"
by (metis max.bounded_iff i_def ‹j ≥ max i i'› ‹⋀χ. χ ∈ 𝒢 ⟹ S ⊨⇩P χ›)
hence "S ⊨⇩P Rep ?φ'"
using φ'_def ltl_prop_equiv_def by blast
hence "S ↑⊨⇩P ?φ'"
using ltl_prop_entails_abs.rep_eq by blast
}
thus "r j ∉ M_fin π"
using ‹⋀χ. χ ∈ 𝒢 ⟹ the (π χ) < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)› ‹𝒢 = dom π› by fastforce
qed
hence "range (suffix (max i i') r) ∩ M_fin π = {}"
unfolding suffix_def by (blast intro: le_add1 elim: rangeE)
hence "limit r ∩ M_fin π = {}"
using limit_in_range_suffix[of r] by blast
moreover
have "limit r ∩ UNIV ≠ {}"
using ‹finite (range r)› by (simp, metis empty_iff limit_nonemptyE)
ultimately
show ?thesis
unfolding r_def accepting_pair⇩R_simp ..
qed

moreover

have "⋀χ. χ ∈ 𝒢 ⟹ accepting_pair⇩R ?Δ ?q⇩0 (Acc Σ π χ) w"
proof -
fix χ assume "χ ∈ 𝒢"
then obtain ψ where "χ = G ψ" and "G ψ ∈ 𝒢"
using ‹Only_G 𝒢› by fastforce
thus "?thesis χ"
using ‹⋀ψ. G ψ ∈ 𝒢 ⟹ accept⇩R (ltl_to_rabin Σ ψ 𝒢) w›[OF ‹G ψ ∈ 𝒢›]
using rabin_accept_to_Acc[of ψ π] ‹G ψ ∈ 𝒢› ‹𝒢 ⊆ ❙G φ› ‹χ ∈ 𝒢›
unfolding ltl.sel unfolding ‹χ = G ψ› ‹𝒢 = dom π› using π_def ‹𝒢 = dom π› ltl.sel(8) unfolding ltl_prop_entails_abs.rep_eq ltl_to_rabin.simps
by (metis (no_types, lifting) Collect_cong)
qed
ultimately
have "accepting_pair⇩G⇩R ?Δ ?q⇩0 (M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π}) w"
unfolding accepting_pair⇩G⇩R_def accepting_pair⇩R_def fst_conv snd_conv ‹𝒢 = dom π› by blast
}
ultimately
show ?rhs
unfolding ltl_to_rabin_base_def.ltl_to_generalized_rabin.simps accept⇩G⇩R_def fst_conv snd_conv by blast
}

― ‹Assuming @{term "ltl_to_generalized_rabin Σ φ"} accepts @{term w}, we prove that @{term "w ⊨ φ"} holds›
{
assume ?rhs
obtain π' where 0: "dom π' ⊆ ❙G φ"
and 1: "⋀χ. χ ∈ dom π' ⟹ the (π' χ) < ltl_FG_to_rabin_def.max_rank⇩R Σ (theG χ)"
and 2: "accepting_pair⇩R ?Δ ?q⇩0 (M_fin π', UNIV) w"
and 3: "⋀χ. χ ∈ dom π' ⟹ accepting_pair⇩R ?Δ ?q⇩0 (Acc Σ π' χ) w"
using accept⇩G⇩R_I[OF ‹?rhs›] unfolding max_rank_of_def by blast

define 𝒢 where "𝒢 = dom π'"
hence "𝒢 ⊆ ❙G φ"
using ‹dom π' ⊆ ❙G φ› by simp

moreover

note 𝒢_properties[OF ‹dom π' ⊆ ❙G φ›[unfolded 𝒢_def[symmetric]]]
ultimately
have 𝔐_Accept: "⋀χ. χ ∈ 𝒢 ⟹ ltl_FG_to_rabin_def.accept⇩R' (theG χ) 𝒢 w"
using Acc_to_mojmir_accept[OF _ 0 3, of "theG _"] 1[of "G theG _", unfolded ltl.sel] 𝒢_def
unfolding ltl_prop_entails_abs.rep_eq by (metis (no_types) ltl.sel(8))

― ‹Normalise @{text π} to the smallest accepting ranks›
obtain π where "dom π' = dom π"
and "⋀χ. χ ∈ dom π ⟹ π χ = ltl_FG_to_rabin_def.smallest_accepting_rank⇩R Σ (theG χ) (dom π) w"
and "accepting_pair⇩R (δ⇩𝒜 Σ) (ι⇩𝒜 φ) (M_fin π, UNIV) w"
and "⋀χ. χ ∈ dom π ⟹ accepting_pair⇩R (δ⇩𝒜 Σ) (ι⇩𝒜 φ) (Acc Σ π χ) w"
using normalize_π[OF 0 _ 2 3] 1 unfolding max_rank_of_def ltl_prop_entails_abs.rep_eq by blast

have "ltl_FG_to_rabin Σ 𝒢 w"
using finite_Σ bounded_w ‹Only_G 𝒢› unfolding ltl_FG_to_rabin_def by auto

have "closed 𝒢 w"
using 𝔐_Accept ‹Only_G 𝒢› ltl.sel(8) ‹finite 𝒢›
unfolding ltl_FG_to_rabin.ltl_to_rabin_correct_exposed'[OF ‹ltl_FG_to_rabin Σ 𝒢 w›, symmetric] by fastforce

moreover

have "accept⇩M φ 𝒢 w"
proof -
(* Wait until the run gets trapped in the "good" states *)
obtain i where i_def: "⋀j. j ≥ i ⟹ r j ∉ M_fin π"
using ‹accepting_pair⇩R  ?Δ ?q⇩0 (M_fin π, UNIV) w› limit_inter_empty[OF ‹finite (range r)›, of "M_fin π"]
unfolding r_def[symmetric] MOST_nat_le accepting_pair⇩R_def by auto

(* Wait until the states with succeeding tokens are (prop.) equivalent to ℱ *)
obtain i' where i'_def:
"⋀j ψ S. j ≥ i' ⟹ G ψ ∈ 𝒢 ⟹ (S ⊨⇩P ℱ ψ w 𝒢 j ∧ 𝒢 ⊆ S) = (∀q. q ∈ ltl_FG_to_rabin_def.𝒮⇩R Σ ψ 𝒢 w j ⟶ S ⊨⇩P Rep q)"
using ℱ_eq_𝒮_generalized[OF finite_Σ bounded_w ‹closed 𝒢 w›] unfolding MOST_nat_le by presburger

{
fix j S
assume "j ≥ max i i'"
hence "j ≥ i" and "j ≥ i'"
by simp+
assume 𝒢_def': "∀ψ. G ψ ∈ 𝒢 ⟶ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G 𝒢 (ℱ ψ w 𝒢 j)"

let ?φ' = "fst (fst (r j))"
let ?m = "snd (fst (r j))"

have "⋀χ. χ ∈ 𝒢 ⟹ S ⊨⇩P χ"
using 𝒢_def' ‹𝒢 ⊆ ❙G φ› unfolding G_nested_propos_alt_def by auto
moreover

(* Proof that the chosen S propositionally implies all succeeding states of the projected Mojmir automaton *)
{
fix χ
assume "χ ∈ 𝒢"
then obtain ψ where "χ = G ψ" and "G ψ ∈ 𝒢"
using ‹Only_G 𝒢› by auto
hence "G ψ ∈ ❙G φ"
using ‹𝒢 ⊆ ❙G φ› by blast

interpret 𝔐: ltl_FG_to_rabin Σ ψ 𝒢 w
by (insert ‹ltl_FG_to_rabin Σ 𝒢 w›)

{
fix q
assume "q ∈ 𝔐.𝒮 j"
hence "S ⊨⇩P eval⇩G 𝒢 (ℱ ψ w 𝒢 j)"
using 𝒢_def' ‹G ψ ∈ 𝒢› by simp
moreover
have "S ⊇ 𝒢"
using 𝒢_def' ‹Only_G 𝒢› by auto
hence "⋀x. x ∈ 𝒢 ⟹ S ⊨⇩P eval⇩G 𝒢 x"
using ‹Only_G 𝒢› ‹S ⊇ 𝒢› by fastforce
moreover
{
fix S
assume "⋀x. x ∈ 𝒢 ∪ {ℱ ψ w 𝒢 j} ⟹ S ⊨⇩P x"
hence "𝒢 ⊆ S" and "S ⊨⇩P ℱ ψ w 𝒢 j"
using ‹Only_G 𝒢› by fastforce+
hence "S ⊨⇩P Rep q"
using ‹q ∈ ltl_FG_to_rabin_def.𝒮⇩R Σ ψ 𝒢 w j›
using i'_def[OF ‹j ≥ i'› ‹G ψ ∈ 𝒢›] by blast
}
ultimately
have "S ⊨⇩P eval⇩G 𝒢 (Rep q)"
using eval⇩G_respectfulness_generalized[of "𝒢 ∪ {ℱ ψ w 𝒢 j}" "Rep q" S 𝒢]
by blast
}
moreover
have "𝔐.𝒮 j = {q. 𝒢 ⊨⇩P Rep q} ∪ {q . ∃j'. the 𝔐.smallest_accepting_rank ≤ j' ∧ the (?m (G ψ)) q = Some j'}"
unfolding 𝔐.𝒮.simps using run_properties(2)[OF ‹G ψ ∈ ❙G φ›] r_def by simp
ultimately
have "⋀q j. j ≥ the (π χ) ⟹ the (?m χ) q = Some j ⟹ S ⊨⇩P eval⇩G 𝒢 (Rep q)"
using  ‹χ ∈ 𝒢›[unfolded 𝒢_def ‹dom π' = dom π›]
unfolding ‹χ = G ψ› ‹⋀χ. χ ∈ dom π ⟹ π χ = ltl_FG_to_rabin_def.smallest_accepting_rank⇩R Σ (theG χ) (dom π) w›[OF ‹χ ∈ 𝒢›[unfolded 𝒢_def ‹dom π' = dom π›], unfolded ‹χ = G ψ›] ltl.sel(8)
unfolding  ‹𝒢 ≡ dom π'›[symmetric] ‹dom π' = dom π›[symmetric] by blast
}
moreover

have "(⋀χ. χ ∈ 𝒢 ⟹ S ⊨⇩P χ ∧ (∀q. ∀j' ≥ the (π χ). the (?m χ) q = Some j' ⟶ S ⊨⇩P eval⇩G 𝒢 (Rep q))) ⟹ S ⊨⇩P Rep ?φ'"
apply (insert i_def[OF ‹j ≥ i›])
apply (simp add: eval⇩G_abs_def ltl_prop_entails_abs.rep_eq case_prod_beta option.case_eq_if)
apply (unfold ‹𝒢 ≡ dom π'›[symmetric] ‹dom π' = dom π›[symmetric])
apply meson
done

ultimately

have "S ⊨⇩P Rep ?φ'"
by fast
hence "S ⊨⇩P af φ (w [0 → j])"
using φ'_def ltl_prop_equiv_def by blast
}
thus "accept⇩M φ 𝒢 w"
unfolding accept⇩M_def MOST_nat_le by blast
qed

ultimately
show ?lhs
using ‹𝒢 ⊆ ❙G φ› ltl_logical_characterization by 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 Abs M_fin Σ φ"

lemma ltl_to_generalized_rabin_af_wellformed:
"finite Σ ⟹ range w ⊆ Σ ⟹ ltl_to_rabin_af Σ w"
apply (unfold_locales)
apply (auto simp add: af_G_letter_sat_core_lifted ltl_prop_entails_abs.rep_eq intro: finite_reach_af)
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.ltl_to_generalized_rabin_correct] by simp

thm ltl_to_generalized_rabin_af_correct ltl_FG_to_generalized_rabin_correct

end
```