Theory LTL_Rabin

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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

lemma ltl_semi_mojmir: 
  assumes "finite Σ"
  assumes "range w ⊆ Σ"
  shows "semi_mojmir Σ ↑afG (Abs ψ) w"
proof 
  fix ψ
  have nonempty_Σ: "Σ ≠ {}"
    using assms by auto
  show "finite (reach Σ ↑afG (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 Σ "↑afG" "Abs φ" w "{q. 𝒢 ⊨P Rep q}" .

― ‹Import abbreviations from parent locale to simplify terms›
abbreviation "δR ≡ step"
abbreviation "qR ≡ initial"
abbreviation "AccR j ≡ (failR ∪ mergeR j, succeedR j)"
abbreviation "max_rankR ≡ max_rank"
abbreviation "smallest_accepting_rankR ≡ smallest_accepting_rank"
abbreviation "acceptR' ≡ accept"
abbreviation "𝒮R ≡ 𝒮"

lemma Rep_token_run_af:
  "Rep (token_run x n) ≡P afG φ (w [x → n])"
proof -
  have "token_run x n = Abs (afG φ ((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 afG φ ((suffix x w) [0 → (n - x)])"
    using ltlP_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 Σ "↑afG" "Abs φ" w "{q. 𝒢 ⊨P Rep q}"
proof
  show "⋀q ν. q ∈ {q. 𝒢 ⊨P Rep q} ⟹ ↑afGq ν ∈ {q. 𝒢 ⊨P Rep q}"
    using wellformed_𝒢 af_G_letter_sat_core_lifted by auto
  have nonempty_Σ: "Σ ≠ {}"
    using bounded_w by blast
  show "finite (reach Σ ↑afG(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 afG φ (map w [i + 0..<i + (j - i)])) = 𝔓 φ 𝒢 w i"
        by (auto simp add: subsequence_def, metis add_diff_cancel_left' le_Suc_ex nat_le_linear upt_conv_Nil )
    hence "(∃j. 𝒢 ⊨P afG φ (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 ↑afG(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 ⟷ acceptR (δR, qR, {AccR i | i. i < max_rankR}) 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.qR φ, {ltl_FG_to_rabin_def.AccR Σ φ 𝒢 i | i. i < ltl_FG_to_rabin_def.max_rankR Σ φ})"

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 ψ ∈ 𝒢 ⟶ acceptR (ltl_to_rabin Σ ψ 𝒢) w))"
proof -
  have "⋀𝒢 ψ. 𝒢 ⊆ G (G φ) ⟹ G ψ ∈ 𝒢 ⟹ (𝔓∞ ψ 𝒢 w ⟷ acceptR (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 ⟷ acceptR (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 n1 where "⋀m q. m ≥ n1 ⟹ ((∃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 n2 where "⋀x. x < k ⟹ token_succeeds x ⟹ token_run x n2 ∈ ?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 {n1, n2, k}"
  
  (* Prove properties for the larger n *)
  {
    fix m q
    assume "n ≤ m"
    hence "n1 ≤ 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 ≥ n1 ⟹ ((∃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 n2 ∈ ?F› Max.coboundedI[of "{n1, n2, k}"] 
    using token_stays_in_final_states[of _ n2] 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 afG ψ (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 afG ψ (w [x → m])"
            using ‹⋀x. k ≤ x ⟹ x ≤ Suc m ⟹ S ⊨P afG ψ (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 afG ψ (w [x → m])"
          using Rep_token_run_af unfolding q_def ltl_prop_equiv_def by simp
      }
      hence "∀x ∈ (set (map (λi. afG ψ (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 qm = (λk. if k ∈ K then Some (qm 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_pairR δ q0 P w) = accepting_pairGR δ q0 (combine_pairs 𝒫) w"
  by auto

lemma combine_pairs2:
  "combine_pairs 𝒫 ∈ α ⟹ (⋀P. P ∈ 𝒫 ⟹ accepting_pairR δ q0 P w ) ⟹ acceptGR (δ, q0, α) w"
  using combine_pairs_prop[of 𝒫 δ q0 w] by fastforce

lemma combine_pairs'_prop: 
  "(∀P ∈ 𝒫. accepting_pairR δ q0 P w) = accepting_pairGR δ q0 (combine_pairs' 𝒫) w"
  by auto

fun ltl_FG_to_generalized_rabin :: "'a ltl ⇒ ('a ltl ⇀ 'a ltlP ⇀ 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.qR (theG χ)),
    {combine_pairs' {embed_pair χ (ltl_FG_to_rabin_def.AccR Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢} 
      | 𝒢 π. 𝒢 ⊆ G (G φ) ∧ G φ ∈ 𝒢 ∧ (∀χ. π χ < ltl_FG_to_rabin_def.max_rankR Σ (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.qR (theG x)" 
          by (auto simp add: LTL_Rabin.product_initial_state.simps) 
        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
qed (simp add: reach_def)

theorem ltl_FG_to_generalized_rabin_correct:
  assumes "range w ⊆ Σ"
  shows "w ⊨ F G φ = acceptGR (𝒫 φ) w"
  (is "?lhs = ?rhs")
proof
  define r where "r = runt (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 runt.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 ψ ∈ 𝒢 ⟶ acceptR (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_rankR Σ (theG ψ) 𝒢 w) else 0)"
      for ψ
    let ?P' = "{↿⇩χ (ltl_FG_to_rabin_def.AccR Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢}"
     
    have "∀P ∈ ?P'. accepting_pairR (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
    proof 
      fix P
      assume "P ∈ ?P'"
      then obtain χ where P_def: "P = ↿⇩χ (ltl_FG_to_rabin_def.AccR Σ (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χ = runt δℛ qℛ w"
      
      moreover

      have "accept" and "acceptR (δℛ, qℛ, {Accℛ j | j. j < max_rank}) w" 
        using ‹χ ∈ 𝒢› ‹∃χ'. χ = G χ'› ‹∀ψ. G ψ ∈ 𝒢 ⟶ acceptR (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_pairR δℛ qℛ (Accℛ (π χ)) w"
        using ‹acceptR (δℛ, qℛ, {Accℛ j | j. j < max_rank}) w› LeastI[of "λi. accepting_pairR δℛ qℛ (Accℛ i) w"] 
        by (auto simp add: smallest_accepting_rankℛ_def)

      ultimately

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

      moreover

      have 1: "(ι× (G (G φ)) (λχ. ltl_FG_to_rabin_def.qR (theG χ))) χ = Some qℛ"
        using ‹χ ∈ 𝒢› ‹𝒢 ⊆ G (G φ)› by (simp add: LTL_Rabin.product_initial_state.simps subset_iff) 
      have 2: "finite (range (runt 
              (Δ× (λχ. ltl_FG_to_rabin_def.δR Σ (theG χ)))
              (ι× (G (G φ)) (λχ. ltl_FG_to_rabin_def.qR (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_pairR (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
        unfolding P_def r_def by simp
    qed
    hence "accepting_pairGR (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 ψ ∈ 𝒢 ⟶ acceptR (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_rankR"
        using smallest_accepting_rank_properties π_def ‹ψ ∈ 𝒢› by auto
    }
    hence "⋀χ. π χ < ltl_FG_to_rabin_def.max_rankR Σ (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 acceptGR_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.AccR Σ (theG χ) 𝒢 (π χ)) | χ. χ ∈ 𝒢}" (is "P = combine_pairs' ?P'") 
      and "accepting_pairGR (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w"
      and "𝒢 ⊆ G (G φ)" and "G φ ∈ 𝒢" and "⋀χ. π χ < ltl_FG_to_rabin_def.max_rankR Σ (theG χ)"
      unfolding acceptGR_def by auto
    moreover
    hence P'_def: "⋀P. P ∈ ?P' ⟹ accepting_pairR (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 ψ ∈ 𝒢 ⟶ acceptR (ltl_to_rabin Σ ψ 𝒢) w"
    proof (rule+)
      fix ψ
      assume "G ψ ∈ 𝒢"
      define χ where "χ = G ψ" 
      define P where "P = ↿⇩χ (ltl_FG_to_rabin_def.AccR Σ ψ 𝒢 (π χ))"
      hence "χ ∈ 𝒢" and "theG χ = ψ" 
        using χ_def ‹G ψ ∈ 𝒢› by simp+
      hence "P ∈ ?P'" 
        unfolding P_def by auto
      hence "accepting_pairR (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χ = runt δℛ qℛ w"
      
      have "limit r ∩ fst P = {}" and "limit r ∩ snd P ≠ {}"
        using ‹accepting_pairR (fst (𝒫 φ)) (fst (snd (𝒫 φ))) P w› 
        unfolding r_def accepting_pairR_def by metis+

      moreover

      have 1: "(ι× (G (G φ)) (λχ. ltl_FG_to_rabin_def.qR (theG χ))) (G ψ) = Some qℛ"
        using ‹G ψ ∈ 𝒢› ‹𝒢 ⊆ G (G φ)› by (auto simp add: LTL_Rabin.product_initial_state.simps subset_iff)
      have 2: "finite (range (runt (Δ× (λχ. ltl_FG_to_rabin_def.δR Σ (theG χ))) (ι× (G (G φ)) (λχ. ltl_FG_to_rabin_def.qR (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_pairR δℛ qℛ (Accℛ (π χ)) w"
        unfolding rχ_def by simp 
      hence "acceptR (δℛ, qℛ, {Accℛ j | j. j < max_rank}) w"
        using ‹⋀χ. π χ < ltl_FG_to_rabin_def.max_rankR Σ (theG χ)› ‹theG χ = ψ› 
        unfolding acceptR_simp accepting_pairR_def fst_conv snd_conv by blast 
      thus "acceptR (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 ltlP ⇒ 'a set ⇒ 'a ltlP"
  fixes
    δM :: "'a ltlP ⇒ 'a set ⇒ 'a ltlP"
  fixes
    q0 :: "'a ltl ⇒ 'a ltlP"
  fixes 
    q0M :: "'a ltl ⇒ 'a ltlP"
  fixes
    M_fin :: "('a ltl ⇀ nat) ⇒ ('a ltlP × ('a ltl ⇀ 'a ltlP ⇀ nat), 'a set) transition set"
begin

― ‹Transition Function and Initial State›

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

fun initial
where
  "initial φ = (q0 φ, ι× (G φ) (semi_mojmir_def.initial o q0M o theG))"

― ‹Acceptance Condition›

definition max_rank_of
where
  "max_rank_of Σ ψ ≡ semi_mojmir_def.max_rank Σ δM (q0M (theG ψ))"

fun Acc_fin
where
  "Acc_fin Σ π χ = ⋃(embed_transition_snd ` ⋃(embed_transition χ ` 
     (mojmir_to_rabin_def.failR Σ δM (q0M (theG χ)) {q. dom π ↑⊨P q}
     ∪ mojmir_to_rabin_def.mergeR δM (q0M (theG χ)) {q. dom π ↑⊨P q} (the (π χ)))))"

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

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

fun rabin_pairs :: "'a set set ⇒ 'a ltl ⇒ ('a ltlP × ('a ltl ⇀ 'a ltlP ⇀ 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 ltlP × ('a ltl ⇀ 'a ltlP ⇀ 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 Σ δ (q0 φ))"
  assumes
    mojmir_to_rabin: "Only_G 𝒢 ⟹ mojmir_to_rabin Σ δM (q0M ψ) w {q. 𝒢 ↑⊨P q}" 
begin 

lemma semi_mojmir:
  "semi_mojmir Σ δM (q0M ψ) 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 add: reach_def)
    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 (runt (delta Σ) (initial φ) w) ≠ {}"
  by (metis emptyE finite_Σ limit_nonemptyE finite_reach bounded_w runt_finite) 

lemma run_properties:
  fixes φ
  defines "r ≡ run (delta Σ) (initial φ) w"
  shows "fst (r i) = foldl δ (q0 φ) (w [0 → i])"
    and "⋀χ q. χ ∈ G φ ⟹ the (snd (r i) χ) q = semi_mojmir_def.state_rank Σ δM (q0M (theG χ)) w q i"
proof -
  have sm: "⋀ψ. semi_mojmir Σ δM (q0M ψ) w"
    using mojmir_to_rabin[of "{}"] unfolding mojmir_to_rabin_def mojmir_def by simp
  have "r i = (foldl δ (q0 φ) (w [0 → i]), 
    λχ. if χ ∈ G φ then Some (λψ. foldl (semi_mojmir_def.step Σ δM (q0M (theG χ))) (semi_mojmir_def.initial (q0M (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 δ (q0 φ) (w [0 → i]), 
    λχ. if χ ∈ G φ then Some (λψ. semi_mojmir_def.state_rank Σ δM (q0M (theG χ)) w ψ i) else None)"
    unfolding semi_mojmir.state_rank_step_foldl[OF sm] r_def by simp

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

lemma acceptGR_I:
  assumes "acceptGR (𝒜 Σ φ) w"
  obtains π where "dom π ⊆ G φ" 
    and "⋀χ. χ ∈ dom π ⟹ the (π χ) < max_rank_of Σ χ"
    and "accepting_pairR (delta Σ) (initial φ) (M_fin π, UNIV) w"
    and "⋀χ. χ ∈ dom π ⟹ accepting_pairR (delta Σ) (initial φ) (Acc Σ π χ) w"
proof -
  from assms obtain P where "P ∈ rabin_pairs Σ φ" and "accepting_pairGR (delta Σ) (initial φ) P w"
    unfolding acceptGR_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 (runt (delta Σ) (initial φ) w) ∩ UNIV ≠ {}"
    using run_limit_not_empty assms by simp
  ultimately
  have "accepting_pairR (delta Σ) (initial φ) (M_fin π, UNIV) w" 
    and "⋀χ. χ ∈ dom π ⟹ accepting_pairR (delta Σ) (initial φ) (Acc Σ π χ) w"
    unfolding P_def accepting_pairGR_simp accepting_pairR_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 "q0M ψ" w "{q. dom π ↑⊨P q}"
  by (metis mojmir_to_rabin ‹dom π ⊆ G φ› 𝒢_elements)

lemma Acc_property:
  "accepting_pairR (delta Σ) (initial φ) (Acc Σ π (G ψ)) w ⟷ accepting_pairR 𝔐.δℛ 𝔐.qℛ (𝔐.Accℛ (the (π (G ψ)))) w"
  (is "?Acc = ?Accℛ")
proof -  
  define r rψ where "r = runt (delta Σ) (initial φ) w" and "rψ = runt 𝔐.δℛ 𝔐.qℛ w"
  hence "finite (range r)"
    using runt_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 (runt (Δ× (semi_mojmir_def.step Σ δM o q0M 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_pairR_def by blast 
qed

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

lemma Acc_to_mojmir_accept:
  "⟦accepting_pairR (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:
  "⟦acceptR 𝔐.ℛ w; π (G ψ) = 𝔐.smallest_accepting_rank⟧ ⟹ accepting_pairR (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_pairR (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_pairR (delta Σ) (initial φ) (M_fin π, UNIV) w"
  assumes "⋀χ. χ ∈ dom π ⟹ accepting_pairR (delta Σ) (initial φ) (Acc Σ π χ) w"
  obtains π𝒜 where "dom π = dom π𝒜"
    and "⋀χ. χ ∈ dom π𝒜 ⟹ π𝒜 χ = mojmir_def.smallest_accepting_rank Σ δM (q0M (theG χ)) w {q. dom π𝒜 ↑⊨P q}"
    and "accepting_pairR (delta Σ) (initial φ) (M_fin π𝒜, UNIV) w" 
    and "⋀χ. χ ∈ dom π𝒜 ⟹ accepting_pairR (delta Σ) (initial φ) (Acc Σ π𝒜 χ) w"
proof -
  define 𝒢 where "𝒢 = dom π"
  note 𝒢_properties[OF dom_subset]

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

  moreover
  
  {
    fix χ assume "χ ∈ dom π"
  
    interpret 𝔐: mojmir_to_rabin Σ δM "q0M (theG χ)" w "{q. dom π ↑⊨P q}"
      by (metis mojmir_to_rabin ‹dom π ⊆ G φ› 𝒢_elements)
  
    from ‹χ ∈ dom π› have "accepting_pairR (delta Σ) (initial φ) (Acc Σ π χ) w"
      using assms(4) by blast
    hence "accepting_pairR 𝔐.δℛ 𝔐.qℛ (𝔐.Accℛ (the (π χ))) w" 
      by (metis ‹χ ∈ dom π› Acc_property[OF _ dom_subset] ‹Only_G (dom π)› ltl.sel(8))
    moreover
    hence "acceptR (𝔐.δℛ, 𝔐.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 
      by (simp add: 𝔐.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_pairR (delta Σ) (initial φ) (M_fin π𝒜, UNIV) w"
    using assms unfolding accepting_pairR_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 (q0M (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 (q0M (theG χ)) w {q. dom π𝒜 ↑⊨P q}"
      using ‹G (theG χ) ∈ dom π𝒜› ‹χ = G (theG χ)› π𝒜_def ‹dom π = dom π𝒜›[symmetric] by simp
    ultimately
    have "accepting_pairR (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 ltlP × ('a ltl ⇀ 'a ltlP ⇀ 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 ↑evalG (dom π) q)) ⟶ S ↑⊨P φ')}"

locale ltl_to_rabin_af = ltl_to_rabin_base "↑af" "↑afG" "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 ⊨ φ = acceptGR (ltl_to_generalized_rabin Σ φ) w"
  (is "?lhs = ?rhs")
proof
  let ?Δ = "δ𝒜 Σ"
  let ?q0 = "ι𝒜 φ"
  let ?F = "F𝒜 Σ φ"
 
  ― ‹Preliminary facts needed by both proof directions›
  define r where "r = runt ?Δ ?q0 w"
  have r_alt_def': "⋀i. fst (fst (r i)) = Abs (af φ (w [0 → i]))"
    using run_properties(1) unfolding r_def runt.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 Σ ↑afG(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 runt_finite[OF finite_reach] bounded_w finite_Σ
    by (simp add: r_def)

  ― ‹Assuming @{term "w ⊨ φ"} holds, we prove that @{term "ltl_to_generalized_rabin Σ φ"} accepts @{term w}›
  {
    assume ?lhs
    then obtain 𝒢 where "𝒢 ⊆ G φ" and "acceptM φ 𝒢 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_rankR Σ (theG χ) 𝒢 w) else None)"
      for χ
    
    have 𝔐_accept: "⋀ψ. G ψ ∈ 𝒢 ⟹ ltl_FG_to_rabin_def.acceptR' ψ 𝒢 w"
      using ‹closed 𝒢 w› ‹ltl_FG_to_rabin Σ 𝒢 w› ltl_FG_to_rabin.ltl_to_rabin_correct_exposed' by blast
    have "⋀ψ. G ψ ∈ 𝒢 ⟹ acceptR (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_rankR Σ (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_pairR ?Δ ?q0 (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 evalG 𝒢 (ℱ ψ w 𝒢 j)) ⟶ S ⊨P af φ (w [0 → j])"
          using ‹acceptM φ 𝒢 w› unfolding MOST_nat_le acceptM_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 ↑evalG 𝒢 q"
            hence assm2: "⋀χ. χ ∈ 𝒢 ⟹ ∀q. (∃j ≥ the (π χ). the (?m χ) q = Some j) ⟶ S ⊨P evalG 𝒢 (Rep q)"
              unfolding ltl_prop_entails_abs.rep_eq evalG_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 evalG 𝒢 (Rep q)"
                using ‹𝒢 ⊆ S› evalG_prop_entailment by blast
              hence "⋀q. q ∈ Rep ` 𝔐.𝒮 j ⟹ S ⊨P evalG 𝒢 q"
                using assm2 ‹G ψ ∈ 𝒢› unfolding 𝒮_def by auto
  
              ultimately
              have "S ⊨P evalG 𝒢 (ℱ ψ w 𝒢 j)"
                by (rule evalG_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_rankR Σ (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_pairR_simp ..
      qed
  
      moreover
  
      have "⋀χ. χ ∈ 𝒢 ⟹ accepting_pairR ?Δ ?q0 (Acc Σ π χ) w"
      proof -
        fix χ assume "χ ∈ 𝒢"
        then obtain ψ where "χ = G ψ" and "G ψ ∈ 𝒢" 
          using ‹Only_G 𝒢› by fastforce 
        thus "?thesis χ"
          using ‹⋀ψ. G ψ ∈ 𝒢 ⟹ acceptR (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_pairGR ?Δ ?q0 (M_fin π ∪ ⋃{Acc_fin Σ π χ | χ. χ ∈ dom π}, {Acc_inf π χ | χ. χ ∈ dom π}) w"
        unfolding accepting_pairGR_def accepting_pairR_def fst_conv snd_conv ‹𝒢 = dom π› by blast
    }
    ultimately
    show ?rhs
      unfolding ltl_to_rabin_base_def.ltl_to_generalized_rabin.simps acceptGR_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_rankR Σ (theG χ)"
      and 2: "accepting_pairR ?Δ ?q0 (M_fin π', UNIV) w"
      and 3: "⋀χ. χ ∈ dom π' ⟹ accepting_pairR ?Δ ?q0 (Acc Σ π' χ) w"
      using acceptGR_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.acceptR' (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_rankR Σ (theG χ) (dom π) w"
      and "accepting_pairR (δ𝒜 Σ) (ι𝒜 φ) (M_fin π, UNIV) w" 
      and "⋀χ. χ ∈ dom π ⟹ accepting_pairR (δ𝒜 Σ) (ι𝒜 φ) (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 "acceptM φ 𝒢 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_pairR  ?Δ ?q0 (M_fin π, UNIV) w› limit_inter_empty[OF ‹finite (range r)›, of "M_fin π"]
        unfolding r_def[symmetric] MOST_nat_le accepting_pairR_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 evalG 𝒢 (ℱ ψ 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 evalG 𝒢 (ℱ ψ w 𝒢 j)"
              using 𝒢_def' ‹G ψ ∈ 𝒢› by simp
            moreover 
            have "S ⊇ 𝒢"
              using 𝒢_def' ‹Only_G 𝒢› by auto
            hence "⋀x. x ∈ 𝒢 ⟹ S ⊨P evalG 𝒢 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 evalG 𝒢 (Rep q)"
              using evalG_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 evalG 𝒢 (Rep q)"
            using  ‹χ ∈ 𝒢›[unfolded 𝒢_def ‹dom π' = dom π›]
            unfolding ‹χ = G ψ› ‹⋀χ. χ ∈ dom π ⟹ π χ = ltl_FG_to_rabin_def.smallest_accepting_rankR Σ (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 evalG 𝒢 (Rep q))) ⟹ S ⊨P Rep ?φ'"
          apply (insert i_def[OF ‹j ≥ i›])
          apply (simp add: evalG_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 "acceptM φ 𝒢 w"
        unfolding acceptM_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 ↑afG 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 ⊨ φ = acceptGR (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