Theory Logical_Characterization

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section β€ΉLogical Characterization Theoremsβ€Ί

theory Logical_Characterization
  imports Main af "Auxiliary/Preliminaries2"
begin

subsection β€ΉEventually True G-Subformulaeβ€Ί

fun 𝒒FG :: "'a ltl β‡’ 'a set word β‡’ 'a ltl set"
where
  "𝒒FG true w = {}"
| "𝒒FG (false) w = {}"
| "𝒒FG (p(a)) w = {}"
| "𝒒FG (np(a)) w = {}"
| "𝒒FG (Ο†1 and Ο†2) w = 𝒒FG Ο†1 w βˆͺ 𝒒FG Ο†2 w"
| "𝒒FG (Ο†1 or Ο†2) w = 𝒒FG Ο†1 w βˆͺ 𝒒FG Ο†2 w"
| "𝒒FG (F Ο†) w = 𝒒FG Ο† w"
| "𝒒FG (G Ο†) w = (if w ⊨ F G Ο† then {G Ο†} βˆͺ 𝒒FG Ο† w else 𝒒FG Ο† w)"
| "𝒒FG (X Ο†) w = 𝒒FG Ο† w"
| "𝒒FG (Ο† U ψ) w = 𝒒FG Ο† w βˆͺ 𝒒FG ψ w"
 
lemma 𝒒FG_alt_def:
  "𝒒FG Ο† w = {G ψ | ψ. G ψ ∈ G Ο† ∧ w ⊨ F (G ψ)}"
  by (induction Ο† arbitrary: w) (simp; blast)+

lemma 𝒒FG_Only_G:
  "Only_G (𝒒FG Ο† w)"
   by (induction Ο†) auto

lemma 𝒒FG_suffix[simp]:
  "𝒒FG Ο† (suffix i w) = 𝒒FG Ο† w"
  unfolding 𝒒FG_alt_def LTL_FG_suffix ..

subsection β€ΉEventually Provable and Almost All Eventually Provableβ€Ί

abbreviation 𝔓
where
  "𝔓 Ο† 𝒒 w i ≑ βˆƒj. 𝒒 ⊨P afG Ο† (w [i β†’ j])"

definition almost_all_eventually_provable :: "'a ltl β‡’ 'a ltl set β‡’ 'a set word β‡’ bool" (β€Ήπ”“βˆžβ€Ί) 
where
  "π”“βˆž Ο† 𝒒 w ≑ βˆ€βˆži. 𝔓 Ο† 𝒒 w i"

subsubsection β€ΉProof Rulesβ€Ί

lemma almost_all_eventually_provable_monotonI[intro]:
  "π”“βˆž Ο† 𝒒 w ⟹ 𝒒 βŠ† 𝒒' ⟹ π”“βˆž Ο† 𝒒' w"
  unfolding almost_all_eventually_provable_def MOST_nat_le by blast

lemma almost_all_eventually_provable_restrict_to_G:
  "π”“βˆž Ο† 𝒒 w ⟹ Only_G 𝒒 ⟹ π”“βˆž Ο† (𝒒 ∩ G Ο†) w"
proof -
  assume "Only_G 𝒒" and "π”“βˆž Ο† 𝒒 w"
  moreover
  hence "β‹€Ο†. 𝒒 ⊨P Ο† = (𝒒 ∩ G Ο†) ⊨P Ο†"
    using LTL_prop_entailment_restrict_to_propos propos_subset
    unfolding G_nested_propos_alt_def by blast
  ultimately
  show ?thesis
    unfolding almost_all_eventually_provable_def by force
qed

fun G_depth :: "'a ltl β‡’ nat"
where 
  "G_depth (Ο† and ψ) = max (G_depth Ο†) (G_depth ψ)"
| "G_depth (Ο† or ψ) = max (G_depth Ο†) (G_depth ψ)"
| "G_depth (F Ο†) = G_depth Ο†"
| "G_depth (G Ο†) = G_depth Ο† + 1"
| "G_depth (X Ο†) = G_depth Ο†"
| "G_depth (Ο† U ψ) = max (G_depth Ο†) (G_depth ψ)"
| "G_depth Ο† = 0"

lemma almost_all_eventually_provable_restrict_to_G_depth:
  assumes "π”“βˆž Ο† 𝒒 w"
  assumes "Only_G 𝒒"
  shows "π”“βˆž Ο† (𝒒 ∩ {ψ. G_depth ψ ≀ G_depth Ο†}) w"
proof -
  { 
    fix Ο† 
    have "𝒒 ⊨P Ο† = (𝒒 ∩ {ψ. G_depth ψ ≀ G_depth Ο†}) ⊨P Ο†"
      by (induction Ο†) (insert β€ΉOnly_G 𝒒›, auto) 
  } 
  note Unfold1 = this
  
  {
    fix w
    { 
      fix Ο† Ξ½ 
      have "{ψ. G_depth ψ ≀ G_depth (af_G_letter Ο† Ξ½)} = {ψ. G_depth ψ ≀ G_depth Ο†}" 
        by (induction Ο†) (unfold af_G_letter.simps G_depth.simps, simp_all, (metis le_max_iff_disj mem_Collect_eq)+) 
    }
    hence "{ψ. G_depth ψ ≀ G_depth (afG Ο† w)} = {ψ. G_depth ψ ≀ G_depth Ο†}"
      by (induction w arbitrary: Ο† rule: rev_induct) fastforce+
  }
  note Unfold2 = this

  from assms(1) show ?thesis
    unfolding almost_all_eventually_provable_def Unfold1 Unfold2 .
qed

lemma almost_all_eventually_provable_suffix:
  "π”“βˆž Ο† 𝒒' w ⟹ π”“βˆž Ο† 𝒒' (suffix i w)"
  unfolding almost_all_eventually_provable_def MOST_nat_le
  by (metis Nat.add_0_right subsequence_shift subsequence_prefix_suffix suffix_0 add.assoc diff_zero trans_le_add2) 

subsubsection β€ΉThresholdβ€Ί

text β€ΉThe first index, such that the formula is eventually provable from this time onβ€Ί

fun threshold :: "'a ltl β‡’ 'a set  word β‡’ 'a ltl set β‡’ nat option"
where
  "threshold Ο† w 𝒒 = index (Ξ»j. 𝔓 Ο† 𝒒 w j)"

lemma threshold_properties:
  "threshold Ο† w 𝒒 = Some i ⟹ 0 < i ⟹ Β¬ 𝒒 ⊨P afG Ο† (w [(i - 1) β†’ k])"
  "threshold Ο† w 𝒒 = Some i ⟹ j β‰₯ i ⟹ βˆƒk. 𝒒 ⊨P afG Ο† (w [j β†’ k])"
  using index_properties unfolding threshold.simps by blast+

lemma threshold_suffix:
  assumes "threshold Ο† w 𝒒 = Some k"
  assumes "threshold Ο† (suffix i w) 𝒒 = Some k'"
  shows "k ≀ k' + i"
proof (rule ccontr)
  assume "Β¬k ≀ k' + i"
  hence "k > k' + i"
    by arith
  then obtain j where "k = k' + i + Suc j"
    by (metis Suc_diff_Suc le_Suc_eq le_add1 le_add_diff_inverse less_imp_Suc_add)
  hence "0 < k" and "k' + i + Suc j - 1 = i + (k' + j)"
    using β€Ήk > k' + iβ€Ί by arith+
  show False
    using threshold_properties(1)[OF assms(1) β€Ή0 < kβ€Ί] threshold_properties(2)[OF assms(2), of "k' + j", OF le_add1] 
    unfolding subsequence_shift β€Ήk = k' + i + Suc jβ€Ί β€Ήk' + i + Suc j - 1 = i + (k' + j)β€Ί by blast
qed

subsubsection β€ΉRelation to LTL semanticsβ€Ί

lemma ltl_implies_provable:
  "w ⊨ Ο† ⟹ 𝔓 Ο† (𝒒FG Ο† w) w 0"
proof (induction Ο† arbitrary: w)
  case (LTLProp a)
    hence "{} ⊨P afG (p(a)) (w [0 β†’ 1])"
      by (simp add: subsequence_def)
    thus ?case 
      by blast
next
  case (LTLPropNeg a)
    hence "{} ⊨P afG (np(a)) (w [0 β†’ 1])"
      by (simp add: subsequence_def)
    thus ?case 
      by blast
next
  case (LTLAnd Ο†1 Ο†2)
    obtain i1 i2 where "(𝒒FG Ο†1 w) ⊨P afG Ο†1 (w [0 β†’ i1])" and "(𝒒FG Ο†2 w) ⊨P afG Ο†2 (w [0 β†’ i2])"
      using LTLAnd unfolding ltl_semantics.simps by blast
    have "(𝒒FG Ο†1 w) ⊨P afG Ο†1 (w [0 β†’ i1 + i2])" and "(𝒒FG Ο†2 w) ⊨P afG Ο†2 (w [0 β†’ i2 + i1])"
      using afG_sat_core_generalized[OF 𝒒FG_Only_G _ β€Ή(𝒒FG Ο†1 w) ⊨P afG Ο†1 (w [0 β†’ i1])β€Ί]
      using afG_sat_core_generalized[OF 𝒒FG_Only_G _ β€Ή(𝒒FG Ο†2 w) ⊨P afG Ο†2 (w [0 β†’ i2])β€Ί]
      by simp+
    thus ?case 
      by (simp only: afG_decompose add.commute) auto
next
  case (LTLOr Ο†1 Ο†2)
    thus ?case 
      unfolding afG_decompose by (cases "w ⊨ Ο†1") force+
next
  case (LTLNext Ο†)
    obtain i where "(𝒒FG Ο† w) ⊨P afG Ο† (suffix 1 w [0 β†’ i])"
      using LTLNext(1)[OF LTLNext(2)[unfolded ltl_semantics.simps]] 
      unfolding 𝒒FG_suffix by blast
    hence "(𝒒FG (X Ο†) w) ⊨P afG (X Ο†) (w [0 β†’ 1 + i])"  
      unfolding subsequence_shift subsequence_append by (simp add: subsequence_def)
    thus ?case
      by blast
next
  case (LTLFinal Ο†)
    then obtain i where "suffix i w ⊨ Ο†" 
      by auto
    then obtain j where "𝒒FG Ο† w ⊨P afG Ο† (suffix i w [0 β†’ j])"
      using LTLFinal 𝒒FG_suffix by blast
    hence A: "𝒒FG Ο† w ⊨P afG Ο† (suffix i w [0 β†’ Suc j])"
      using afG_sat_core_generalized[OF 𝒒FG_Only_G, of j "Suc j", OF le_SucI] by blast
    from afG_keeps_F_and_S[OF _ A] have "𝒒FG Ο† w ⊨P afG (F Ο†) (w [0 β†’ Suc (i + j)])"  
      unfolding subsequence_shift subsequence_append Suc_eq_plus1 by simp
    thus ?case
      using 𝒒FG.simps(7) by blast
next
  case (LTLUntil Ο† ψ)
    then obtain k where "suffix k w ⊨ ψ" and "βˆ€j < k. suffix j w ⊨ Ο†"
      by auto
    thus ?case
    proof (induction k arbitrary: w)
      case 0
        then obtain i where "𝒒FG ψ w ⊨P afG ψ (w [0 β†’ i])"
          using LTLUntil by (metis suffix_0) 
        hence "𝒒FG ψ w ⊨P afG ψ (w [0 β†’ Suc i])"
          using afG_sat_core_generalized[OF 𝒒FG_Only_G, of i "Suc i", OF  le_SucI] by auto
        hence "𝒒FG (Ο† U ψ) w ⊨P afG (Ο† U ψ) (w [0 β†’ Suc i])"
          unfolding afG_subsequence_U ltl_prop_entailment.simps 𝒒FG.simps by blast  
        thus ?case
          by blast  
    next
      case (Suc k)
        hence "w ⊨ Ο†" and "suffix k (suffix 1 w) ⊨ ψ" and "βˆ€j<k. suffix j (suffix 1 w) ⊨ Ο†"
          unfolding suffix_0 suffix_suffix by (auto, metis Suc_less_eq)+
        then obtain i where i_def: "𝒒FG (Ο† U ψ) w ⊨P afG (Ο† U ψ) (suffix 1 w [0 β†’ i])"
          using Suc(1)[of "suffix 1 w"] unfolding LTL_FG_suffix 𝒒FG_alt_def by blast
        obtain j where j_def: "𝒒FG Ο† w ⊨P afG Ο† (w [0 β†’ j])"
          using LTLUntil(1)[OF β€Ήw ⊨ Ο†β€Ί] by auto
        hence "𝒒FG (Ο† U ψ) w ⊨P afG Ο† (w [0 β†’ j])"
          by auto

        hence "𝒒FG (Ο† U ψ) w ⊨P afG Ο† (w [0 β†’ j + (i + 1)])"
          by (blast intro: afG_sat_core_generalized[OF 𝒒FG_Only_G le_add1])
        moreover
        have "1 + (i + j) = j + (i + 1)"
          by arith
        have "𝒒FG (Ο† U ψ) w ⊨P afG (Ο† U ψ) (w [1 β†’ j + (i + 1)])"
          using afG_sat_core_generalized[OF 𝒒FG_Only_G le_add1 i_def, of j]
          unfolding subsequence_shift 𝒒FG_suffix β€Ή1 + (i + j) = j + (i + 1)β€Ί by simp
        ultimately
        have "𝒒FG (Ο† U ψ) w ⊨P afG (Ο† U ψ) (w [1 β†’ Suc (j + i)]) and afG Ο† (w [0 β†’ Suc (j + i)])"
          by simp
        hence "𝒒FG (Ο† U ψ) w ⊨P afG (Ο† U ψ) (w [0 β†’ Suc (j + i)])"
          unfolding afG_subsequence_U ltl_prop_entailment.simps by blast 
        thus ?case
          using afG_subsequence_U ltl_prop_entailment.simps by blast
    qed
qed simp+

lemma ltl_implies_provable_almost_all:
  "w ⊨ Ο† ⟹ βˆ€βˆži. 𝒒FG Ο† w ⊨P afG Ο† (w [0 β†’ i])"
  using ltl_implies_provable afG_sat_core_generalized[OF 𝒒FG_Only_G] 
  unfolding MOST_nat_le by metis

subsubsection β€ΉClosed Setsβ€Ί

abbreviation closed
where
  "closed 𝒒 w ≑ finite 𝒒 ∧ Only_G 𝒒 ∧ (βˆ€Οˆ. G ψ ∈ 𝒒 ⟢ π”“βˆž ψ 𝒒 w)"

lemma closed_FG:
  assumes "closed 𝒒 w"
  assumes "G ψ ∈ 𝒒"
  shows "w ⊨ F G ψ"
proof - 
  have "finite 𝒒" and "Only_G 𝒒" and "(β‹€Οˆ. G ψ ∈ 𝒒 ⟹ π”“βˆž ψ 𝒒 w)"
    using assms by simp+
  moreover
  note β€ΉG ψ ∈ 𝒒›
  ultimately
  show "w ⊨ F G ψ" 
  proof (induction arbitrary: ψ rule: finite_ranking_induct[where f = G_depth])
    case (insert x 𝒒)
      (* Split ψ' out *)
      then obtain ψ' where "x = G ψ'"
        by auto
      {
        fix ψ assume "G ψ ∈ insert x 𝒒" (is "_ ∈ ?𝒒'")
        hence "π”“βˆž ψ (?𝒒' ∩ {ψ'. G_depth ψ' ≀ G_depth ψ}) w"  
          using insert(4-5) by (blast dest: almost_all_eventually_provable_restrict_to_G_depth)
        moreover
        have "G_depth ψ < G_depth x"
          using insert(2) β€ΉG ψ ∈ insert x 𝒒› β€Ήx = G ψ'β€Ί by force
        ultimately
        have "π”“βˆž ψ 𝒒 w"
          by auto
      }
      hence "π”“βˆž ψ' 𝒒 w" and "closed 𝒒 w"
        using insert β€Ήx = G ψ'β€Ί by simp+
  
      (* Wait until all G-subformulae are "stable" *)
      have "Only_G 𝒒" and "Only_G (𝒒 βˆͺ G ψ')" and "finite (𝒒 βˆͺ G ψ')"
        using G_nested_finite G_nested_propos_Only_G insert by blast+
      then obtain k1 where k1_def: "β‹€Οˆ i. ψ ∈ 𝒒 βˆͺ G ψ' ⟹ suffix k1 w ⊨ ψ = suffix (k1 + i) w ⊨ ψ" 
        by (blast intro: ltl_G_stabilize)
       
      (* Wait until the formula is provable for all suffixes *)
      hence "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ w ⊨ F (G ψ)"
        using insert β€Ήclosed 𝒒 wβ€Ί by simp
      then obtain k2 where k2_def: "βˆ€i β‰₯ k2. βˆƒj. 𝔓 ψ' 𝒒 w i"
        using β€Ήπ”“βˆž ψ' 𝒒 wβ€Ί unfolding almost_all_eventually_provable_def MOST_nat_le by blast
       
      {
        fix i 
        assume "i β‰₯ max k1 k2"
        hence "i β‰₯ k1" and "i β‰₯ k2"
          by simp+
        then obtain j' where "𝒒 ⊨P afG ψ' (w [i β†’ j'])"
          using k2_def by blast
        then obtain j where "𝒒 ⊨P afG ψ' (w [i β†’ i + j])"
          by (cases "i ≀ j'") (blast dest: le_Suc_ex, metis subsequence_empty le_add_diff_inverse nat_le_linear)
        moreover
        have "β‹€Οˆ. G ψ ∈ 𝒒  ⟹ suffix k1 w ⊨ G ψ"
          using ltl_G_stabilize_property[OF β€Ήfinite (𝒒 βˆͺ G ψ')β€Ί β€ΉOnly_G (𝒒 βˆͺ G ψ')β€Ί k1_def]
          using β€Ήβ‹€Οˆ. G ψ ∈ 𝒒 ⟹ w ⊨ F (G ψ)β€Ί by blast
        hence "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ suffix (i + j) w ⊨ G ψ"
          by (metis β€Ήi β‰₯ max k1 k2β€Ί LTL_suffix_G suffix_suffix le_Suc_ex max.cobounded1) 
        hence "β‹€Οˆ. ψ ∈ 𝒒 ⟹ suffix (i + j) w ⊨ ψ"
          using β€ΉOnly_G 𝒒› by fast
        ultimately
        have Suffix: "suffix (i + j) w ⊨ afG ψ' (w [i β†’ i + j])"
          using ltl_models_equiv_prop_entailment by blast 
        
        obtain c where "i = k1 + c"
          using β€Ήi β‰₯ k1β€Ί unfolding le_iff_add by blast
        hence Stable: "βˆ€Οˆ ∈ G ψ'. suffix i w ⊨ ψ = suffix j (suffix i w) ⊨ ψ"
          using k1_def k1_def[of _ "c + j"] unfolding suffix_suffix add.assoc[symmetric] by blast
        from Suffix have "suffix i w ⊨ ψ'"
          unfolding suffix_suffix subsequence_shift afG_ltl_continuation_suffix[OF Stable] by simp
      }
      hence "w ⊨ F G ψ'"
        unfolding MOST_nat_le LTL_FG_almost_all_suffixes by blast 
      thus ?case
        using insert using β€Ήβ‹€Οˆ. G ψ ∈ 𝒒 ⟹ w ⊨ F G Οˆβ€Ί β€Ήx = G ψ'β€Ί by auto
  qed blast
qed

lemma closed_𝒒FG:
  "closed (𝒒FG Ο† w) w"
proof (induction Ο†)
  case (LTLGlobal Ο†)  
    thus ?case 
    proof (cases "w ⊨ F G Ο†")
      case True
        hence "βˆ€βˆži. suffix i w ⊨ Ο†"
          using LTL_FG_almost_all_suffixes by blast
        then obtain i where "βˆ€j β‰₯ i. suffix j w ⊨ Ο†"
          unfolding MOST_nat_le by blast
        {
          fix k
          assume "k β‰₯ i"
          hence "suffix k w ⊨ Ο†"
            using β€Ήβˆ€jβ‰₯i. suffix j w ⊨ Ο†β€Ί by blast
          hence "𝔓 Ο† {G ψ |ψ. w ⊨ F G ψ} (suffix k w) 0"
            using LTL_FG_suffix 
            by (blast dest: ltl_implies_provable[unfolded 𝒒FG_alt_def])
          hence "𝔓 Ο† {G ψ |ψ. w ⊨ F G ψ} w k"
            unfolding subsequence_shift by auto
        }
        hence "π”“βˆž Ο† {G ψ | ψ. w ⊨ F G ψ} w"
          using almost_all_eventually_provable_def[of Ο† _ w]
          unfolding MOST_nat_le by auto
        hence "π”“βˆž Ο† (𝒒FG Ο† w) w"
          unfolding 𝒒FG_alt_def
          using almost_all_eventually_provable_restrict_to_G by blast
        thus ?thesis
          using LTLGlobal insert by auto
    qed auto
qed auto

subsubsection β€ΉConjunction of Eventually Provable Formulasβ€Ί

definition β„± 
where 
  "β„± Ο† w 𝒒 j = And (map (Ξ»i. afG Ο† (w [i β†’ j])) [the (threshold Ο† w 𝒒) ..< Suc j])"

lemma almost_all_suffixes_model_β„±:
  assumes "closed 𝒒 w"
  assumes "G Ο† ∈ 𝒒"
  shows "βˆ€βˆžj. suffix j w ⊨ evalG 𝒒 (β„± Ο† w 𝒒 j)"
proof -
  have "Only_G 𝒒"
    using assms(1) by simp
  hence "𝒒 βŠ† {Ο‡. w ⊨ F Ο‡}" and "π”“βˆž Ο† 𝒒 w"
    using closed_FG[OF assms(1)] assms by auto
  then obtain k where "threshold Ο† w 𝒒 = Some k"
    by (simp add: almost_all_eventually_provable_def)
  hence k_def: "k = the (threshold Ο† w 𝒒)"
    by simp
  moreover
  have "finite (G Ο† βˆͺ 𝒒)" and "Only_G (G Ο† βˆͺ 𝒒)"
    using assms(1) G_nested_finite unfolding G_nested_propos_alt_def by auto
  then obtain l where S: "β‹€j ψ. ψ ∈ G Ο† βˆͺ 𝒒 ⟹ suffix l w ⊨ ψ = suffix (l + j) w ⊨ ψ"
    using ltl_G_stabilize by metis
  hence 𝒒_sat:"β‹€j ψ. G ψ ∈ 𝒒 ⟹ suffix (l + j) w ⊨ G ψ"
    using ltl_G_stabilize_property ‹𝒒 βŠ† {Ο‡. w ⊨ F Ο‡}β€Ί by blast
  {
    fix j
    assume "l ≀ j"
    {
      fix i 
      assume "k ≀ i" "i ≀ j"
      then obtain j' where "j = i + j'" 
        by (blast dest: le_Suc_ex)
      hence "βˆƒj β‰₯ i. 𝒒 ⊨P afG Ο† (w [i β†’ j])"
        using β€Ήπ”“βˆž Ο† 𝒒 wβ€Ί unfolding almost_all_eventually_provable_def MOST_nat_le
        by (metis β€Ήk ≀ iβ€Ί β€Ήthreshold Ο† w 𝒒 = Some kβ€Ί threshold_properties(2) linear subsequence_empty)  
      then obtain j'' where "𝒒 ⊨P afG Ο† (w [i β†’ j''])" and "i ≀ j''"
        by (blast )
      have "suffix j w ⊨ evalG 𝒒 (afG Ο† (w [i β†’ j]))"
      proof (cases "j'' ≀ j")
        case True
          hence "𝒒 ⊨P afG Ο† (w [i β†’ j])"
            using afG_sat_core_generalized[OF β€ΉOnly_G 𝒒›, of _ j' Ο† "suffix i w"] le_Suc_ex[OF β€Ήi ≀ j''β€Ί] le_Suc_ex[OF β€Ήj'' ≀ jβ€Ί]  
            by (metis add.right_neutral subsequence_shift β€Ήj = i + j'β€Ί ‹𝒒 ⊨P afG Ο† (w [i β†’ j''])β€Ί nat_add_left_cancel_le ) 
          hence "𝒒 ⊨P evalG 𝒒 (afG Ο† (w [i β†’ j]))"
            unfolding evalG_prop_entailment .
          moreover
          have "𝒒 βŠ† {Ο‡. suffix j w ⊨ Ο‡}"
            using 𝒒_sat β€Ήl ≀ jβ€Ί β€ΉOnly_G 𝒒› by (fast dest: le_Suc_ex)
          ultimately
          have "{Ο‡. suffix j w ⊨ Ο‡} ⊨P evalG 𝒒 (afG Ο† (w [i β†’ j]))"
            by blast
          thus ?thesis
            unfolding ltl_models_equiv_prop_entailment[symmetric] by simp
      next
        case False
          hence "𝒒 ⊨P evalG 𝒒 (afG (afG Ο† (w [i β†’ j])) (w [j β†’ j'']))"
            unfolding foldl_append[symmetric] evalG_prop_entailment
            by (metis le_iff_add β€Ήi ≀ jβ€Ί map_append upt_add_eq_append nat_le_linear subsequence_def ‹𝒒 ⊨P afG Ο† (w [i β†’ j''])β€Ί) 
          hence "𝒒 ⊨P afG (evalG 𝒒 (afG Ο† (w [i β†’ j]))) (w [j β†’ j''])" (is "𝒒 ⊨P ?afG")
            using afG_evalG[OF β€ΉOnly_G 𝒒›] by blast
          moreover
          have "l ≀ j''"
            using False β€Ήl ≀ jβ€Ί by linarith
          hence "𝒒 βŠ† {Ο‡. suffix j'' w ⊨ Ο‡}"
            using 𝒒_sat β€ΉOnly_G 𝒒› by (fast dest: le_Suc_ex)
          ultimately
          have "suffix j'' w ⊨ ?afG"
            using ltl_models_equiv_prop_entailment[symmetric] by blast
          moreover
          {
            have "β‹€Οˆ. ψ ∈ G Ο† βˆͺ 𝒒 ⟹ suffix j w ⊨ ψ = suffix j'' w ⊨ ψ"
              using S β€Ήl ≀ jβ€Ί β€Ήl ≀ j''β€Ί by (metis le_add_diff_inverse)
            moreover
            have "G (evalG 𝒒 (afG Ο† (w [i β†’ j]))) βŠ† G Ο†" (is "?G βŠ† _")
              using evalG_G_nested by force
            ultimately
            have "β‹€Οˆ. ψ ∈ ?G ⟹ suffix j w ⊨ ψ = suffix j'' w ⊨ ψ"
              by auto
          }
          ultimately
          show ?thesis
            using afG_ltl_continuation_suffix[of "evalG 𝒒 (afG Ο† (w [i β†’ j]))" "suffix j w", unfolded suffix_suffix]
            by (metis False le_Suc_ex nat_le_linear add_diff_cancel_left' subsequence_prefix_suffix)
      qed   
    }
    hence "suffix j w ⊨ And (map (Ξ»i. evalG 𝒒 (afG Ο† (w [i β†’ j]))) [k..<Suc j])"
      unfolding And_semantics set_map set_upt image_def by force 
    hence "suffix j w ⊨ evalG 𝒒 (And (map (Ξ»i. afG Ο† (w [i β†’ j])) [k..<Suc j]))"
      unfolding evalG_And_map map_map comp_def .
  }
  thus ?thesis 
    unfolding β„±_def And_semantics MOST_nat_le k_def[symmetric] by meson
qed

lemma almost_all_commutative'':
  assumes "finite S"
  assumes "Only_G S"
  assumes "β‹€x. G x ∈ S ⟹ βˆ€βˆži. P x (i::nat)"
  shows "βˆ€βˆži. βˆ€x. G x ∈ S ⟢ P x i"
proof -
  from assms have "(β‹€x. x ∈ S ⟹ βˆ€βˆži. P (theG x) (i::nat))"
    by fastforce
  with assms(1) have "βˆ€βˆži. βˆ€x ∈ S. P (theG x) i"
    using almost_all_commutative' by force
  thus ?thesis
    using assms(2) unfolding MOST_nat_le by force
qed

lemma almost_all_suffixes_model_β„±_generalized:
  assumes "closed 𝒒 w"
  shows "βˆ€βˆžj. βˆ€Οˆ. G ψ ∈ 𝒒 ⟢ suffix j w ⊨ evalG 𝒒 (β„± ψ w 𝒒 j)"
  using almost_all_suffixes_model_β„±[OF assms] almost_all_commutative''[of 𝒒] assms by fast

subsection β€ΉTechnical Lemmasβ€Ί

lemma threshold_suffix_2:
  assumes "threshold ψ w 𝒒' = Some k"
  assumes "k ≀ l"
  shows "threshold ψ (suffix l w) 𝒒' = Some 0"
proof -
  have "π”“βˆž ψ 𝒒' w"
    using β€Ήthreshold ψ w 𝒒' = Some kβ€Ί  option.distinct(1)
    unfolding threshold.simps index.simps almost_all_eventually_provable_def by metis
  hence "π”“βˆž ψ 𝒒' (suffix l w)"
    using almost_all_eventually_provable_suffix by blast
  moreover
  have "βˆ€i β‰₯ k. βˆƒj. 𝒒' ⊨P afG ψ (w [i β†’ j])" 
    using threshold_properties(2)[OF assms(1)] by blast
  hence "βˆ€m. βˆƒj. 𝒒' ⊨P afG ψ ((suffix l w) [m β†’ j])"
    unfolding subsequence_shift using β€Ήk ≀ lβ€Ί β€Ήβˆ€i β‰₯ k. βˆƒj. 𝒒' ⊨P afG ψ (w [i β†’ j])β€Ί 
    by (metis (mono_tags, opaque_lifting) leI less_imp_add_positive order_refl subsequence_empty trans_le_add1)
  ultimately
  show ?thesis
    by simp
qed

lemma threshold_closed:
  assumes "closed 𝒒 w"
  shows "βˆƒk. βˆ€Οˆ. G ψ ∈ 𝒒 ⟢ threshold ψ (suffix k w) 𝒒 = Some 0"
proof -
  define k where "k = Max {the (threshold ψ w 𝒒) | ψ. G ψ ∈ 𝒒}" (is "_ = Max ?S")

  have "finite 𝒒" and "Only_G 𝒒" and "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ π”“βˆž ψ 𝒒 w"
    using assms by blast+
  hence "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ βˆƒk. threshold ψ w 𝒒 = Some k"
    unfolding almost_all_eventually_provable_def by simp
  moreover
  have "?S = (Ξ»x. the (threshold (theG x) w 𝒒)) ` 𝒒"
    unfolding image_def using β€ΉOnly_G 𝒒› ltl.sel(8) by metis 
  hence "finite ?S"
    using β€Ήfinite 𝒒› finite_imageI by simp
  hence "β‹€Οˆ k'. G ψ ∈ 𝒒 ⟹ threshold ψ w 𝒒 = Some k' ⟹ k' ≀ k"
    by (metis (mono_tags, lifting) CollectI Max_ge k_def option.sel)  
  ultimately
  have "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ threshold ψ (suffix k w) 𝒒 = Some 0"
    using threshold_suffix[of _ w 𝒒 _ k 0] threshold_suffix_2 by blast
  thus ?thesis
    by blast
qed

lemma β„±_drop:
  assumes "π”“βˆž Ο† 𝒒' w"
  assumes "S ⊨P β„± Ο† w 𝒒' (i + j)"
  shows "S ⊨P β„± Ο† (suffix i w) 𝒒' j"
proof - 
  obtain k k' where k_def: "threshold Ο† w 𝒒' = Some k" and k'_def: "threshold Ο† (suffix i w) 𝒒' = Some k'"
    using assms almost_all_eventually_provable_suffix 
    unfolding threshold.simps index.simps almost_all_eventually_provable_def by fastforce
  hence k_def_2: "the (threshold Ο† w 𝒒') = k" and k'_def_2: "the (threshold Ο† (suffix i w) 𝒒') = k'"
    by simp+
  moreover
  hence "k ≀ i + j ⟹ S ⊨P Ο†"
    using β€ΉS ⊨P β„± Ο† w 𝒒' (i + j)β€Ί unfolding β„±_def And_semantics And_prop_entailment by (simp add: subsequence_def)
  moreover
  have "k' ≀ j ⟹ k ≀ i + j"
    using k_def k'_def threshold_suffix by fastforce 
  ultimately
  have "the (threshold Ο† (suffix i w) 𝒒') ≀ j ⟹ S ⊨P Ο†"
    by blast
  moreover
  {
    fix pos
    assume "k' ≀ pos" and "pos ≀ j"
    have "k ≀ i + pos"
      by (metis threshold_suffix k_def k'_def β€Ήk' ≀ posβ€Ί add.commute add_le_cancel_right order.trans) 
    hence "(i + pos) ∈ set [k..<Suc (i + j)]"
      using β€Ήpos ≀ jβ€Ί by auto
    hence "afG Ο† ((suffix i w) [pos β†’ j]) ∈ set (map (Ξ»ia. afG Ο† (subsequence w ia (i + j))) [k..<Suc (i + j)])"
      unfolding subsequence_shift set_map by blast
    hence "S ⊨P afG Ο† ((suffix i w) [pos β†’ j])"  
      using assms(2) unfolding β„±_def And_prop_entailment k_def_2 by (cases "k ≀ i + j") auto
  }
  ultimately
  show ?thesis
     unfolding β„±_def And_prop_entailment k'_def_2 by auto
qed

subsection β€ΉMain Resultsβ€Ί

definition acceptM
where
  "acceptM Ο† 𝒒 w ≑ (βˆ€βˆžj. βˆ€S. (βˆ€Οˆ. G ψ ∈ 𝒒 ⟢ S ⊨P G ψ ∧ S ⊨P evalG 𝒒 (β„± ψ w 𝒒 j)) ⟢ S ⊨P af Ο† (w [0 β†’ j]))"

lemma lemmaD:
  assumes "w ⊨ Ο†"
  assumes "β‹€Οˆ. G ψ ∈ 𝒒FG Ο† w ⟹ threshold ψ w (𝒒FG Ο† w) = Some 0"
  shows "acceptM Ο† (𝒒FG Ο† w) w"
proof -
  obtain i where "𝒒FG Ο† w ⊨P afG Ο† (w [0 β†’ i])"
    using ltl_implies_provable[OF β€Ήw ⊨ Ο†β€Ί] by metis
  {
    fix S j
    assume assm1: "j β‰₯ i"
    assume assm2: "β‹€Οˆ. G ψ ∈ 𝒒FG Ο† w ⟹ S ⊨P G ψ ∧ S ⊨P evalG (𝒒FG Ο† w) (β„± ψ w (𝒒FG Ο† w) j)"
    moreover
    {
      have "𝒒FG Ο† w ⊨P afG Ο† (w [0 β†’ j])"
        using ‹𝒒FG Ο† w ⊨P afG Ο† (w [0 β†’ i])β€Ί β€Ήj β‰₯ iβ€Ί 
        by (metis afG_sat_core_generalized 𝒒FG_Only_G) 
      moreover
      have "𝒒FG Ο† w βŠ† S"
        using assm2 unfolding 𝒒FG_alt_def by auto
      ultimately
      have "S ⊨P evalG (𝒒FG Ο† w) (afG Ο† (w [0 β†’ j]))"
        using evalG_prop_entailment by blast
    }
    moreover
    {
      fix ψ assume "G ψ ∈ 𝒒FG Ο† w"
      hence "the (threshold ψ w (𝒒FG Ο† w)) = 0" and "S ⊨P evalG (𝒒FG Ο† w) (β„± ψ w (𝒒FG Ο† w) j)"
        using assms assm2 option.sel by metis+
      hence "β‹€i. i ≀ j ⟹ S ⊨P evalG (𝒒FG Ο† w) (afG ψ (w[i β†’ j]))" 
        unfolding β„±_def And_prop_entailment evalG_And_map by auto
    }
    ultimately
    have "S ⊨P af Ο† (w [0 β†’ j])"
      using afG_implies_af_evalG[of _ _ Ο†] by presburger
  }
  thus ?thesis
     unfolding acceptM_def MOST_nat_le by meson 
qed

theorem ltl_FG_logical_characterization:
  "w ⊨ F G Ο† ⟷ (βˆƒπ’’ βŠ† G (F G Ο†). G Ο† ∈ 𝒒 ∧ closed 𝒒 w)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  hence "G Ο† ∈ 𝒒FG (F G Ο†) w" and "𝒒FG (F G Ο†) w βŠ† G (F G Ο†)"
    unfolding 𝒒FG_alt_def by auto
  thus ?rhs
    using closed_𝒒FG by metis
qed (blast intro: closed_FG)

theorem ltl_logical_characterization:
  "w ⊨ Ο† ⟷ (βˆƒπ’’ βŠ† G Ο†. acceptM Ο† 𝒒 w ∧ closed 𝒒 w)"
  (is "?lhs ⟷ ?rhs")
proof 
  assume ?lhs

  obtain k where k_def: "β‹€Οˆ. G ψ ∈ 𝒒FG Ο† w ⟹ threshold ψ (suffix k w) (𝒒FG Ο† w) = Some 0"
    using threshold_closed[OF closed_𝒒FG] by blast

  (* Define new constants *)
  define w' where "w' = suffix k w"
  define Ο†' where "Ο†' = af Ο† (w[0 β†’ k])"

  (* Facts about w' and Ο†' *)
  from β€Ή?lhsβ€Ί have "w' ⊨ Ο†'"
    unfolding af_ltl_continuation_suffix[of w Ο† k] w'_def Ο†'_def .   
  have G_eq: "G Ο†' = G Ο†"
    unfolding Ο†'_def G_af_simp ..
  have 𝒒_eq: "𝒒FG Ο†' w' = 𝒒FG Ο† w"
    unfolding 𝒒FG_alt_def w'_def Ο†'_def G_af_simp LTL_FG_suffix ..
  have Ο†'_eq: "β‹€j. af Ο†' (w' [0 β†’j]) = af Ο† (w [0 β†’ k + j])"
    unfolding Ο†'_def w'_def foldl_append[symmetric] subsequence_shift
    unfolding Nat.add_0_right by (metis subsequence_append) 

  (* Apply helper lemma *)
  have "acceptM Ο†' (𝒒FG Ο†' w') w'"
    using lemmaD[OF β€Ήw' ⊨ Ο†'β€Ί] k_def 
    unfolding 𝒒_eq w'_def[symmetric] by blast

  then obtain j' where j'_def: "β‹€j S. j β‰₯ j' ⟹ 
    (βˆ€Οˆ. G ψ ∈ 𝒒FG Ο†' w' ⟢ S ⊨P G ψ ∧ S ⊨P evalG (𝒒FG Ο†' w') (β„± ψ w' (𝒒FG Ο†' w') j)) ⟹ S ⊨P af Ο†' (w' [0 β†’ j])"
    unfolding acceptM_def MOST_nat_le by blast

 
  (* Change formula, s.t. it matches ?lhs *)
  {
    fix j S
    let ?af = "af Ο† (w[0 β†’ k + j' + j])"
    assume "(βˆ€Οˆ. G ψ ∈ (𝒒FG Ο†' w') ⟢ S ⊨P G ψ ∧ S ⊨P evalG (𝒒FG Ο†' w') (β„± ψ w (𝒒FG Ο†' w') (k + j' + j)))"
    moreover
    {
      fix ψ
      assume "G ψ ∈ 𝒒FG Ο†' w'" (is "_ ∈ ?𝒒")
      hence "π”“βˆž ψ ?𝒒 w"
        unfolding 𝒒_eq using closed_𝒒FG by blast
      have "β‹€S. S ⊨P evalG ?𝒒 (β„± ψ w ?𝒒 (k + j' + j)) ⟹ S ⊨P evalG ?𝒒 (β„± ψ w' ?𝒒 (j' + j))"
        using β„±_drop[OF β€Ήπ”“βˆž ψ (𝒒FG Ο†' w') wβ€Ί, of _ k "j' + j"] evalG_respectfulness(1)[unfolded ltl_prop_implies_def] 
        unfolding add.assoc w'_def by metis
      moreover 
      assume "S ⊨P evalG ?𝒒 (β„± ψ w ?𝒒 (k + j' + j))"
      ultimately
      have "S ⊨P evalG ?𝒒 (β„± ψ w' ?𝒒 (j' + j))"
         by simp
    }
    ultimately
    have "S ⊨P ?af"
      using j'_def unfolding Ο†'_eq add.assoc by simp
  }
  hence "acceptM Ο† (𝒒FG Ο† w) w"
    unfolding acceptM_def MOST_nat_le 𝒒_eq by (metis le_Suc_ex) 
  moreover
  have "𝒒FG Ο† w βŠ† G Ο†"
    unfolding 𝒒FG_alt_def by auto
  ultimately
  show ?rhs
    by (metis closed_𝒒FG)
next
  assume ?rhs

  then obtain 𝒒 where 𝒒_prop: "𝒒 βŠ† G Ο†" "finite 𝒒" "Only_G 𝒒" "acceptM Ο† 𝒒 w" "closed 𝒒 w"
    using 𝒒_elements 𝒒_finite by blast
  then obtain i where "β‹€Ο‡ j. Ο‡ ∈ 𝒒 ⟹ suffix i w ⊨ Ο‡ = suffix (i + j) w ⊨ Ο‡"
    using ltl_G_stabilize by blast
  hence i_def: "β‹€Οˆ. G ψ ∈ 𝒒 ⟹ suffix i w ⊨ G ψ"
    using ltl_G_stabilize_property[OF β€Ήfinite 𝒒› β€ΉOnly_G 𝒒›] 𝒒_prop closed_FG[of 𝒒] by blast
  obtain j where j_def: "β‹€j' S. j' β‰₯ j ⟹ 
    (βˆ€Οˆ. G ψ ∈ 𝒒 ⟢ S ⊨P G ψ ∧ S ⊨P evalG 𝒒 (β„± ψ w 𝒒 j')) ⟢ S ⊨P af Ο† (w [0 β†’ j'])"
    using β€ΉacceptM Ο† 𝒒 wβ€Ί unfolding acceptM_def MOST_nat_le by presburger
  obtain j' where lemma19: "β‹€j ψ. j β‰₯ j' ⟹ G ψ ∈ 𝒒 ⟹ suffix j w ⊨ evalG 𝒒 (β„± ψ w 𝒒 j)"
    using almost_all_suffixes_model_β„±_generalized[OF β€Ήclosed 𝒒 wβ€Ί] unfolding MOST_nat_le by blast
  
  (* Define new constants *)
  define k where "k = max (max i j) j'"
  define w' where "w' = suffix k w"
  define Ο†' where "Ο†' = af Ο† (w[0 β†’ k])"
  define S where "S = {Ο‡. w' ⊨ Ο‡}"

  have "(β‹€Οˆ. G ψ ∈ 𝒒 ⟹ S ⊨P G ψ ∧ S ⊨P evalG 𝒒 (β„± ψ w 𝒒 k)) ⟹ S ⊨P Ο†'"
    using j_def[of k S] unfolding Ο†'_def k_def by fastforce
  moreover
  {
    fix ψ
    assume "G ψ ∈ 𝒒"
    have "β‹€j. i ≀ j ⟹ suffix i w ⊨ G ψ ⟹ suffix j w ⊨ G ψ"
      by (metis LTL_suffix_G le_Suc_ex suffix_suffix)
    hence "w' ⊨ G ψ"
      unfolding w'_def k_def max_def 
      using i_def[OF β€ΉG ψ ∈ 𝒒›] by simp
    moreover
    have "w' ⊨ evalG 𝒒 (β„± ψ w 𝒒 k)"
      using lemma19[OF _ β€ΉG ψ ∈ 𝒒›, of k]
      unfolding w'_def k_def by fastforce
    ultimately
    have "S ⊨P G ψ" and "S ⊨P evalG 𝒒 (β„± ψ w 𝒒 k)" 
      unfolding S_def ltl_models_equiv_prop_entailment[symmetric] by blast+
  }
  ultimately
  have "S ⊨P Ο†'"
    by simp
  hence "w' ⊨ Ο†'"
    using S_def ltl_models_equiv_prop_entailment by blast
  thus ?lhs
    using w'_def Ο†'_def af_ltl_continuation_suffix by blast
qed

end