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 Σ ↑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  (ji𝔐. 𝔐.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  (ji𝔘. 𝔘.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  (ji𝔐. 𝔐.rank x (Suc m) = Some j)  𝔐.token_run x (Suc m)  {q. 𝒢 P Rep q}
       m < x  (ji𝔘. 𝔘.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 "ji𝔐. 𝔐.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 "ji𝔐. 𝔐.rank x (Suc m) = Some j"
          using 𝔐.rank_eq_state_rank by metis
        hence token_cases: "(ji𝔘. 𝔘.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 "(ji𝔐. 𝔐.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 "(ji𝔐. 𝔐.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 "(ji𝔐. 𝔐.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. (jthe (π𝒜 χ). the (m𝒜 χ) q = Some j)  S P evalG (dom π𝒜) (Rep q))) = (S P χ  S P evalG (dom π𝒜) (theG χ)  (q. (jthe (π𝔘 χ). 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