Theory LTL_Rabin_Unfold_Opt

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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
qed (simp add: reach_def)

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
qed (simp add: reach_def)

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]  
    by (simp add: step_abs.abs_eq)
  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
        qed (simp add: q_def)
      }
      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⇩𝔘)"
      by (meson le_add1 limit_range_suffix_incr)+
    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