Theory LTL_Rabin_Unfold_Opt

theory LTL_Rabin_Unfold_Opt
imports LTL_Rabin
(*  
    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 Σ ↑afG𝔘 (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 ↑afG𝔘 (Abs φ) w |w. set w ⊆ Σ}" "{foldl ↑afG𝔘 (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 Σ ↑afG𝔘 (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 Σ "↑afG𝔘" "Abs (UnfG φ)" 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 Σ "↑afG𝔘" "Abs (UnfG φ)" w "{q. 𝒢 ⊨P Rep q}"
proof
  show "⋀q ν. q ∈ {q. 𝒢 ⊨P Rep q} ⟹ ↑afG𝔘 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 Σ ↑afG𝔘 (Abs (UnfG φ)))" (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 "afG φ (w [x → Suc n]) = step (afG𝔘 (UnfG φ) (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) = UnfG_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 UnfG_𝒢[OF ‹Only_G 𝒢›] by (simp add: Rep_Abs_equiv UnfG_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 ltlP × ('a ltl ⇀ 'a ltlP ⇀ nat), 'a set) transition set"
where
  "M𝔘_fin π = {((φ', m), ν, p). ¬(∀S. (∀χ ∈ (dom π). S ↑⊨P Abs χ ∧ S ↑⊨P ↑evalG (dom π) (Abs (theG χ)) ∧ (∀q. (∃j ≥ the (π χ). the (m χ) q = Some j) ⟶ S ↑⊨P ↑evalG (dom π) (↑step q ν))) ⟶ S ↑⊨P (↑step φ' ν))}"

locale ltl_to_rabin_af_unf = ltl_to_rabin_base "↑af𝔘" "↑afG𝔘" "Abs o Unf" "Abs o UnfG" 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 Σ ↑afG (Abs (theG χ)) w {q. dom π𝒜 ↑⊨P q}"
  assumes "⋀χ. χ ∈ dom π𝔘 ⟹ π𝔘 χ = mojmir_def.smallest_accepting_rank Σ af_G_letter_abs_opt (Abs (UnfG (theG χ))) w {q. dom π𝔘 ↑⊨P q}"
  shows "accepting_pairR (ltl_to_rabin_af.δ𝒜 Σ) (ltl_to_rabin_af.ι𝒜 φ) (M_fin π𝒜, UNIV) w ⟷ accepting_pairR𝔘 Σ) (ι𝔘 φ) (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𝒜 = runt (ltl_to_rabin_af.δ𝒜 Σ) (ltl_to_rabin_af.ι𝒜 φ) w"
      and "r𝔘 = runt𝔘 Σ) (ι𝔘 φ) w"
  hence "finite (range r𝒜)" and "finite (range r𝔘)"
    using runt_finite[OF 𝒜.finite_reach] runt_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 ↑afG (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.𝒮 Σ ↑afG (Abs (theG χ)) w {q. dom π𝒜P Rep q} (Suc i)
       = (λq. step_abs q (w i)) ` (mojmir_def.𝒮 Σ ↑afG𝔘 (Abs (UnfG (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.𝒮 Σ ↑afG (Abs (theG χ)) w {q. dom π𝒜P Rep q} (Suc j)
       = (λq. step_abs q (w j)) ` (mojmir_def.𝒮 Σ ↑afG𝔘 (Abs (UnfG (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 runt.simps using prod.exhaust by fastforce

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

      have m𝒜_def: "⋀χ q. χ ∈ G φ ⟹ the (m𝒜 χ) q = semi_mojmir_def.state_rank Σ ↑afG (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 Σ ↑afG𝔘 (Abs (UnfG (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 runt.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 evalG (dom π𝒜) (Rep q)"
            have "⋀q ν. (dom π𝒜) ⊨P Rep q ⟹ ?P q"
              using ‹Only_G (dom π𝒜)› evalG_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 evalG (dom π𝒜) (Rep q)) ⟷
              S ⊨P χ ∧ S ⊨P evalG (dom π𝒜) (theG χ) ∧ (∀q. (∃j ≥ the (π𝔘 χ). the (m𝔘 χ) q = Some j) ⟶ S ⊨P evalG (dom π𝒜) (step (Rep q) (w j)))"
              unfolding 4 using evalG_respectfulness(2)[OF Rep_Abs_equiv, unfolded ltl_prop_equiv_def]
              using evalG_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 evalG (dom π𝒜) (Rep q))) ⟶ S ⊨P Rep φ𝒜)
            ⟷ ((∀χ ∈ dom π𝔘. S ⊨P χ ∧ S ⊨P evalG (dom π𝔘) (theG χ) ∧ (∀q. (∃j ≥ the (π𝔘 χ). the (m𝔘 χ) q = Some j) ⟶ S ⊨P evalG (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 evalG (dom π𝒜) (Rep q))) = (S ⊨P χ ∧ S ⊨P evalG (dom π𝒜) (theG χ) ∧ (∀q. (∃j≥the (π𝔘 χ). the (m𝔘 χ) q = Some j) ⟶ S ⊨P evalG (dom π𝒜) (step (Rep q) (w j))))› A assms(2))
        }
        hence "(∀S. (∀χ ∈ dom π𝒜. S ⊨P χ ∧ (∀q. (∃j ≥ the (π𝒜 χ). the (m𝒜 χ) q = Some j) ⟶ S ⊨P evalG (dom π𝒜) (Rep q))) ⟶ S ⊨P Rep φ𝒜) ⟷ 
        (∀S. (∀χ ∈ dom π𝔘. S ⊨P χ ∧ S ⊨P evalG (dom π𝔘) (theG χ) ∧ (∀q. (∃j ≥ the (π𝔘 χ). the (m𝔘 χ) q = Some j) ⟶ S ⊨P evalG (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] evalG_abs.abs_eq[symmetric] ltlP_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_pairR_def fst_conv snd_conv r𝒜_def[symmetric] r𝔘_def[symmetric] Let_def by blast
qed

theorem ltl_to_generalized_rabin_correct:
  "w ⊨ φ ⟷ acceptGR (𝒜𝔘 Σ φ) w" 
  (is "_ ⟷ ?rhs")
proof (unfold ltl_to_generalized_rabin_af_correct[OF finite_Σ bounded_w], standard)
  let ?lhs = "acceptGR (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_pairR (ltl_to_rabin_af.δ𝒜 Σ) (ltl_to_rabin_af.ι𝒜 φ) (M_fin π, UNIV) w"
      and IV:  "⋀χ. χ ∈ dom π ⟹ accepting_pairR (𝒜.δ𝒜 Σ) (ltl_to_rabin_af.ι𝒜 φ) (𝒜.Acc Σ π χ) w"
      by (unfold ltl_to_generalized_rabin_af.simps; blast intro: 𝒜.acceptGR_I)
 
    ― ‹Normalise @{text π} to the smallest accepting ranks›
    then obtain π𝒜 where A: "dom π = dom π𝒜"
      and B: "⋀χ. χ ∈ dom π𝒜 ⟹ π𝒜 χ = mojmir_def.smallest_accepting_rank Σ ↑afG (Abs (theG χ)) w {q. dom π𝒜 ↑⊨P q}"
      and C: "accepting_pairR (𝒜.δ𝒜 Σ) (𝒜.ι𝒜 φ) (M_fin π𝒜, UNIV) w" 
      and D: "⋀χ. χ ∈ dom π𝒜 ⟹ accepting_pairR (𝒜.δ𝒜 Σ) (𝒜.ι𝒜 φ) (𝒜.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 (UnfG (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 (UnfG (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 (UnfG (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 (UnfG (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_pairR𝔘 Σ) (ι𝔘 φ) (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_pairR𝔘 Σ) (ι𝔘 φ) (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: acceptGR_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_pairR𝔘 Σ) (ι𝔘 φ) (M𝔘_fin π, UNIV) w"
      and IV:  "⋀χ. χ ∈ dom π ⟹ accepting_pairR𝔘 Σ) (ι𝔘 φ) (Acc𝔘 Σ π χ) w"
      by (blast intro: acceptGR_I)
  
    ― ‹Normalize @{text π} to the smallest accepting ranks›
    then obtain π𝔘 where A: "dom π = dom π𝔘"
      and B: "⋀χ. χ ∈ dom π𝔘 ⟹ π𝔘 χ = mojmir_def.smallest_accepting_rank Σ ↑afG𝔘 (Abs (UnfG (theG χ))) w {q. dom π𝔘 ↑⊨P q}"
      and C: "accepting_pairR𝔘 Σ) (ι𝔘 φ) (M𝔘_fin π𝔘, UNIV) w" 
      and D: "⋀χ. χ ∈ dom π𝔘 ⟹ accepting_pairR𝔘 Σ) (ι𝔘 φ) (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 (UnfG (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 Σ ↑afG (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 Σ ↑afG (Abs (theG χ)) w {q. dom π𝒜 ↑⊨P q}"
      using 1 unfolding ‹dom π𝒜 = dom π› π𝒜_def by simp
    hence 3: "⋀χ. χ ∈ dom π𝒜 ⟹ the (π𝒜 χ) < semi_mojmir_def.max_rank Σ ↑afG (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_pairR (𝒜.δ𝒜 Σ) (𝒜.ι𝒜 φ) (𝒜.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_pairR (𝒜.δ𝒜 Σ) (𝒜.ι𝒜 φ) (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: acceptGR_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𝔘 ↑afG𝔘 (Abs ∘ Unf) (Abs ∘ UnfG) 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 ⊨ φ = acceptGR (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