Theory Logical_Characterization

theory Logical_Characterization
imports af Preliminaries2
(*  
    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 = {}"
| "𝒢FG1 and φ2) w = 𝒢FG φ1 w ∪ 𝒢FG φ2 w"
| "𝒢FG1 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, hide_lams) 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