# Theory Logical_Characterization

theory Logical_Characterization
imports af Preliminaries2
```(*
Author:      Salomon Sickert
*)

section ‹Logical Characterization Theorems›

theory Logical_Characterization
imports Main af "Auxiliary/Preliminaries2"
begin

subsection ‹Eventually True G-Subformulae›

fun 𝒢⇩F⇩G :: "'a ltl ⇒ 'a set word ⇒ 'a ltl set"
where
"𝒢⇩F⇩G true w = {}"
| "𝒢⇩F⇩G (false) w = {}"
| "𝒢⇩F⇩G (p(a)) w = {}"
| "𝒢⇩F⇩G (np(a)) w = {}"
| "𝒢⇩F⇩G (φ⇩1 and φ⇩2) w = 𝒢⇩F⇩G φ⇩1 w ∪ 𝒢⇩F⇩G φ⇩2 w"
| "𝒢⇩F⇩G (φ⇩1 or φ⇩2) w = 𝒢⇩F⇩G φ⇩1 w ∪ 𝒢⇩F⇩G φ⇩2 w"
| "𝒢⇩F⇩G (F φ) w = 𝒢⇩F⇩G φ w"
| "𝒢⇩F⇩G (G φ) w = (if w ⊨ F G φ then {G φ} ∪ 𝒢⇩F⇩G φ w else 𝒢⇩F⇩G φ w)"
| "𝒢⇩F⇩G (X φ) w = 𝒢⇩F⇩G φ w"
| "𝒢⇩F⇩G (φ U ψ) w = 𝒢⇩F⇩G φ w ∪ 𝒢⇩F⇩G ψ w"

lemma 𝒢⇩F⇩G_alt_def:
"𝒢⇩F⇩G φ w = {G ψ | ψ. G ψ ∈ ❙G φ ∧ w ⊨ F (G ψ)}"
by (induction φ arbitrary: w) (simp; blast)+

lemma 𝒢⇩F⇩G_Only_G:
"Only_G (𝒢⇩F⇩G φ w)"
by (induction φ) auto

lemma 𝒢⇩F⇩G_suffix[simp]:
"𝒢⇩F⇩G φ (suffix i w) = 𝒢⇩F⇩G φ w"
unfolding 𝒢⇩F⇩G_alt_def LTL_FG_suffix ..

subsection ‹Eventually Provable and Almost All Eventually Provable›

abbreviation 𝔓
where
"𝔓 φ 𝒢 w i ≡ ∃j. 𝒢 ⊨⇩P af⇩G φ (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 (af⇩G φ 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

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 af⇩G φ (w [(i - 1) → k])"
"threshold φ w 𝒢 = Some i ⟹ j ≥ i ⟹ ∃k. 𝒢 ⊨⇩P af⇩G φ (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"
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 ⊨ φ ⟹ 𝔓 φ (𝒢⇩F⇩G φ w) w 0"
proof (induction φ arbitrary: w)
case (LTLProp a)
hence "{} ⊨⇩P af⇩G (p(a)) (w [0 → 1])"
thus ?case
by blast
next
case (LTLPropNeg a)
hence "{} ⊨⇩P af⇩G (np(a)) (w [0 → 1])"
thus ?case
by blast
next
case (LTLAnd φ⇩1 φ⇩2)
obtain i⇩1 i⇩2 where "(𝒢⇩F⇩G φ⇩1 w) ⊨⇩P af⇩G φ⇩1 (w [0 → i⇩1])" and "(𝒢⇩F⇩G φ⇩2 w) ⊨⇩P af⇩G φ⇩2 (w [0 → i⇩2])"
using LTLAnd unfolding ltl_semantics.simps by blast
have "(𝒢⇩F⇩G φ⇩1 w) ⊨⇩P af⇩G φ⇩1 (w [0 → i⇩1 + i⇩2])" and "(𝒢⇩F⇩G φ⇩2 w) ⊨⇩P af⇩G φ⇩2 (w [0 → i⇩2 + i⇩1])"
using af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G _ ‹(𝒢⇩F⇩G φ⇩1 w) ⊨⇩P af⇩G φ⇩1 (w [0 → i⇩1])›]
using af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G _ ‹(𝒢⇩F⇩G φ⇩2 w) ⊨⇩P af⇩G φ⇩2 (w [0 → i⇩2])›]
by simp+
thus ?case
by (simp only: af⇩G_decompose add.commute) auto
next
case (LTLOr φ⇩1 φ⇩2)
thus ?case
unfolding af⇩G_decompose by (cases "w ⊨ φ⇩1") force+
next
case (LTLNext φ)
obtain i where "(𝒢⇩F⇩G φ w) ⊨⇩P af⇩G φ (suffix 1 w [0 → i])"
using LTLNext(1)[OF LTLNext(2)[unfolded ltl_semantics.simps]]
unfolding 𝒢⇩F⇩G_suffix by blast
hence "(𝒢⇩F⇩G (X φ) w) ⊨⇩P af⇩G (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 "𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (suffix i w [0 → j])"
using LTLFinal 𝒢⇩F⇩G_suffix by blast
hence A: "𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (suffix i w [0 → Suc j])"
using af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G, of j "Suc j", OF le_SucI] by blast
from af⇩G_keeps_F_and_S[OF _ A] have "𝒢⇩F⇩G φ w ⊨⇩P af⇩G (F φ) (w [0 → Suc (i + j)])"
unfolding subsequence_shift subsequence_append Suc_eq_plus1 by simp
thus ?case
using 𝒢⇩F⇩G.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 "𝒢⇩F⇩G ψ w ⊨⇩P af⇩G ψ (w [0 → i])"
using LTLUntil by (metis suffix_0)
hence "𝒢⇩F⇩G ψ w ⊨⇩P af⇩G ψ (w [0 → Suc i])"
using af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G, of i "Suc i", OF  le_SucI] by auto
hence "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G (φ U ψ) (w [0 → Suc i])"
unfolding af⇩G_subsequence_U ltl_prop_entailment.simps 𝒢⇩F⇩G.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: "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G (φ U ψ) (suffix 1 w [0 → i])"
using Suc(1)[of "suffix 1 w"] unfolding LTL_FG_suffix 𝒢⇩F⇩G_alt_def by blast
obtain j where j_def: "𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (w [0 → j])"
using LTLUntil(1)[OF ‹w ⊨ φ›] by auto
hence "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G φ (w [0 → j])"
by auto

hence "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G φ (w [0 → j + (i + 1)])"
by (blast intro: af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G le_add1])
moreover
have "1 + (i + j) = j + (i + 1)"
by arith
have "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G (φ U ψ) (w [1 → j + (i + 1)])"
using af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_Only_G le_add1 i_def, of j]
unfolding subsequence_shift 𝒢⇩F⇩G_suffix ‹1 + (i + j) = j + (i + 1)› by simp
ultimately
have "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G (φ U ψ) (w [1 → Suc (j + i)]) and af⇩G φ (w [0 → Suc (j + i)])"
by simp
hence "𝒢⇩F⇩G (φ U ψ) w ⊨⇩P af⇩G (φ U ψ) (w [0 → Suc (j + i)])"
unfolding af⇩G_subsequence_U ltl_prop_entailment.simps by blast
thus ?case
using af⇩G_subsequence_U ltl_prop_entailment.simps by blast
qed
qed simp+

lemma ltl_implies_provable_almost_all:
"w ⊨ φ ⟹ ∀⇩∞i. 𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (w [0 → i])"
using ltl_implies_provable af⇩G_sat_core_generalized[OF 𝒢⇩F⇩G_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 k⇩1 where k1_def: "⋀ψ i. ψ ∈ 𝒢 ∪ ❙G ψ' ⟹ suffix k⇩1 w ⊨ ψ = suffix (k⇩1 + 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 k⇩2 where k2_def: "∀i ≥ k⇩2. ∃j. 𝔓 ψ' 𝒢 w i"
using ‹𝔓⇩∞ ψ' 𝒢 w› unfolding almost_all_eventually_provable_def MOST_nat_le by blast

{
fix i
assume "i ≥ max k⇩1 k⇩2"
hence "i ≥ k⇩1" and "i ≥ k⇩2"
by simp+
then obtain j' where "𝒢 ⊨⇩P af⇩G ψ' (w [i → j'])"
using k2_def by blast
then obtain j where "𝒢 ⊨⇩P af⇩G ψ' (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 k⇩1 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 k⇩1 k⇩2› 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 ⊨ af⇩G ψ' (w [i → i + j])"
using ltl_models_equiv_prop_entailment by blast

obtain c where "i = k⇩1 + c"
using ‹i ≥ k⇩1› 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 af⇩G_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_𝒢⇩F⇩G:
"closed (𝒢⇩F⇩G φ 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 𝒢⇩F⇩G_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 "𝔓⇩∞ φ (𝒢⇩F⇩G φ w) w"
unfolding 𝒢⇩F⇩G_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. af⇩G φ (w [i → j])) [the (threshold φ w 𝒢) ..< Suc j])"

lemma almost_all_suffixes_model_ℱ:
assumes "closed 𝒢 w"
assumes "G φ ∈ 𝒢"
shows "∀⇩∞j. suffix j w ⊨ eval⇩G 𝒢 (ℱ φ 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"
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 af⇩G φ (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 af⇩G φ (w [i → j''])" and "i ≤ j''"
by (blast )
have "suffix j w ⊨ eval⇩G 𝒢 (af⇩G φ (w [i → j]))"
proof (cases "j'' ≤ j")
case True
hence "𝒢 ⊨⇩P af⇩G φ (w [i → j])"
using af⇩G_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 af⇩G φ (w [i → j''])› nat_add_left_cancel_le )
hence "𝒢 ⊨⇩P eval⇩G 𝒢 (af⇩G φ (w [i → j]))"
unfolding eval⇩G_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 eval⇩G 𝒢 (af⇩G φ (w [i → j]))"
by blast
thus ?thesis
unfolding ltl_models_equiv_prop_entailment[symmetric] by simp
next
case False
hence "𝒢 ⊨⇩P eval⇩G 𝒢 (af⇩G (af⇩G φ (w [i → j])) (w [j → j'']))"
unfolding foldl_append[symmetric] eval⇩G_prop_entailment
by (metis le_iff_add ‹i ≤ j› map_append upt_add_eq_append nat_le_linear subsequence_def ‹𝒢 ⊨⇩P af⇩G φ (w [i → j''])›)
hence "𝒢 ⊨⇩P af⇩G (eval⇩G 𝒢 (af⇩G φ (w [i → j]))) (w [j → j''])" (is "𝒢 ⊨⇩P ?af⇩G")
using af⇩G_eval⇩G[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 ⊨ ?af⇩G"
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 (eval⇩G 𝒢 (af⇩G φ (w [i → j]))) ⊆ ❙G φ" (is "?G ⊆ _")
using eval⇩G_G_nested by force
ultimately
have "⋀ψ. ψ ∈ ?G ⟹ suffix j w ⊨ ψ = suffix j'' w ⊨ ψ"
by auto
}
ultimately
show ?thesis
using af⇩G_ltl_continuation_suffix[of "eval⇩G 𝒢 (af⇩G φ (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. eval⇩G 𝒢 (af⇩G φ (w [i → j]))) [k..<Suc j])"
unfolding And_semantics set_map set_upt image_def by force
hence "suffix j w ⊨ eval⇩G 𝒢 (And (map (λi. af⇩G φ (w [i → j])) [k..<Suc j]))"
unfolding eval⇩G_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 ⊨ eval⇩G 𝒢 (ℱ ψ 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 af⇩G ψ (w [i → j])"
using threshold_properties(2)[OF assms(1)] by blast
hence "∀m. ∃j. 𝒢' ⊨⇩P af⇩G ψ ((suffix l w) [m → j])"
unfolding subsequence_shift using ‹k ≤ l› ‹∀i ≥ k. ∃j. 𝒢' ⊨⇩P af⇩G ψ (w [i → j])›
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"
hence "(i + pos) ∈ set [k..<Suc (i + j)]"
using ‹pos ≤ j› by auto
hence "af⇩G φ ((suffix i w) [pos → j]) ∈ set (map (λia. af⇩G φ (subsequence w ia (i + j))) [k..<Suc (i + j)])"
unfolding subsequence_shift set_map by blast
hence "S ⊨⇩P af⇩G φ ((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 accept⇩M
where
"accept⇩M φ 𝒢 w ≡ (∀⇩∞j. ∀S. (∀ψ. G ψ ∈ 𝒢 ⟶ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G 𝒢 (ℱ ψ w 𝒢 j)) ⟶ S ⊨⇩P af φ (w [0 → j]))"

assumes "w ⊨ φ"
assumes "⋀ψ. G ψ ∈ 𝒢⇩F⇩G φ w ⟹ threshold ψ w (𝒢⇩F⇩G φ w) = Some 0"
shows "accept⇩M φ (𝒢⇩F⇩G φ w) w"
proof -
obtain i where "𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (w [0 → i])"
using ltl_implies_provable[OF ‹w ⊨ φ›] by metis
{
fix S j
assume assm1: "j ≥ i"
assume assm2: "⋀ψ. G ψ ∈ 𝒢⇩F⇩G φ w ⟹ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ w) (ℱ ψ w (𝒢⇩F⇩G φ w) j)"
moreover
{
have "𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (w [0 → j])"
using ‹𝒢⇩F⇩G φ w ⊨⇩P af⇩G φ (w [0 → i])› ‹j ≥ i›
by (metis af⇩G_sat_core_generalized 𝒢⇩F⇩G_Only_G)
moreover
have "𝒢⇩F⇩G φ w ⊆ S"
using assm2 unfolding 𝒢⇩F⇩G_alt_def by auto
ultimately
have "S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ w) (af⇩G φ (w [0 → j]))"
using eval⇩G_prop_entailment by blast
}
moreover
{
fix ψ assume "G ψ ∈ 𝒢⇩F⇩G φ w"
hence "the (threshold ψ w (𝒢⇩F⇩G φ w)) = 0" and "S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ w) (ℱ ψ w (𝒢⇩F⇩G φ w) j)"
using assms assm2 option.sel by metis+
hence "⋀i. i ≤ j ⟹ S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ w) (af⇩G ψ (w[i → j]))"
unfolding ℱ_def And_prop_entailment eval⇩G_And_map by auto
}
ultimately
have "S ⊨⇩P af φ (w [0 → j])"
using af⇩G_implies_af_eval⇩G[of _ _ φ] by presburger
}
thus ?thesis
unfolding accept⇩M_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 φ ∈ 𝒢⇩F⇩G (F G φ) w" and "𝒢⇩F⇩G (F G φ) w ⊆ ❙G (F G φ)"
unfolding 𝒢⇩F⇩G_alt_def by auto
thus ?rhs
using closed_𝒢⇩F⇩G by metis
qed (blast intro: closed_FG)

theorem ltl_logical_characterization:
"w ⊨ φ ⟷ (∃𝒢 ⊆ ❙G φ. accept⇩M φ 𝒢 w ∧ closed 𝒢 w)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs

obtain k where k_def: "⋀ψ. G ψ ∈ 𝒢⇩F⇩G φ w ⟹ threshold ψ (suffix k w) (𝒢⇩F⇩G φ w) = Some 0"
using threshold_closed[OF closed_𝒢⇩F⇩G] 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: "𝒢⇩F⇩G φ' w' = 𝒢⇩F⇩G φ w"
unfolding 𝒢⇩F⇩G_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

(* Apply helper lemma *)
have "accept⇩M φ' (𝒢⇩F⇩G φ' 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 ψ ∈ 𝒢⇩F⇩G φ' w' ⟶ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ' w') (ℱ ψ w' (𝒢⇩F⇩G φ' w') j)) ⟹ S ⊨⇩P af φ' (w' [0 → j])"
unfolding accept⇩M_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 ψ ∈ (𝒢⇩F⇩G φ' w') ⟶ S ⊨⇩P G ψ ∧ S ⊨⇩P eval⇩G (𝒢⇩F⇩G φ' w') (ℱ ψ w (𝒢⇩F⇩G φ' w') (k + j' + j)))"
moreover
{
fix ψ
assume "G ψ ∈ 𝒢⇩F⇩G φ' w'" (is "_ ∈ ?𝒢")
hence "𝔓⇩∞ ψ ?𝒢 w"
unfolding 𝒢_eq using closed_𝒢⇩F⇩G by blast
have "⋀S. S ⊨⇩P eval⇩G ?𝒢 (ℱ ψ w ?𝒢 (k + j' + j)) ⟹ S ⊨⇩P eval⇩G ?𝒢 (ℱ ψ w' ?𝒢 (j' + j))"
using ℱ_drop[OF ‹𝔓⇩∞ ψ (𝒢⇩F⇩G φ' w') w›, of _ k "j' + j"] eval⇩G_respectfulness(1)[unfolded ltl_prop_implies_def]
moreover
assume "S ⊨⇩P eval⇩G ?𝒢 (ℱ ψ w ?𝒢 (k + j' + j))"
ultimately
have "S ⊨⇩P eval⇩G ?𝒢 (ℱ ψ w' ?𝒢 (j' + j))"
by simp
}
ultimately
have "S ⊨⇩P ?af"
using j'_def unfolding φ'_eq add.assoc by simp
}
hence "accept⇩M φ (𝒢⇩F⇩G φ w) w"
unfolding accept⇩M_def MOST_nat_le 𝒢_eq by (metis le_Suc_ex)
moreover
have "𝒢⇩F⇩G φ w ⊆ ❙G φ"
unfolding 𝒢⇩F⇩G_alt_def by auto
ultimately
show ?rhs
by (metis closed_𝒢⇩F⇩G)
next
assume ?rhs

then obtain 𝒢 where 𝒢_prop: "𝒢 ⊆ ❙G φ" "finite 𝒢" "Only_G 𝒢" "accept⇩M φ 𝒢 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 eval⇩G 𝒢 (ℱ ψ w 𝒢 j')) ⟶ S ⊨⇩P af φ (w [0 → j'])"
using ‹accept⇩M φ 𝒢 w› unfolding accept⇩M_def MOST_nat_le by presburger
obtain j' where lemma19: "⋀j ψ. j ≥ j' ⟹ G ψ ∈ 𝒢 ⟹ suffix j w ⊨ eval⇩G 𝒢 (ℱ ψ 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 eval⇩G 𝒢 (ℱ ψ 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' ⊨ eval⇩G 𝒢 (ℱ ψ w 𝒢 k)"
using lemma19[OF _ ‹G ψ ∈ 𝒢›, of k]
unfolding w'_def k_def by fastforce
ultimately
have "S ⊨⇩P G ψ" and "S ⊨⇩P eval⇩G 𝒢 (ℱ ψ 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
```