# Theory After

```(*
Author:   Benedikt Seidl
*)

section ‹The ``after''-Function›

theory After
imports
LTL.LTL LTL.Equivalence_Relations Syntactic_Fragments_and_Stability
begin

subsection ‹Definition of af›

primrec af_letter :: "'a ltln ⇒ 'a set ⇒ 'a ltln"
where
"af_letter true⇩n ν = true⇩n"
| "af_letter false⇩n ν = false⇩n"
| "af_letter prop⇩n(a) ν = (if a ∈ ν then true⇩n else false⇩n)"
| "af_letter nprop⇩n(a) ν  = (if a ∉ ν then true⇩n else false⇩n)"
| "af_letter (φ and⇩n ψ) ν = (af_letter φ ν) and⇩n (af_letter ψ ν)"
| "af_letter (φ or⇩n ψ) ν = (af_letter φ ν) or⇩n (af_letter ψ ν)"
| "af_letter (X⇩n φ) ν = φ"
| "af_letter (φ U⇩n ψ) ν = (af_letter ψ ν) or⇩n ((af_letter φ ν) and⇩n (φ U⇩n ψ))"
| "af_letter (φ R⇩n ψ) ν = (af_letter ψ ν) and⇩n ((af_letter φ ν) or⇩n (φ R⇩n ψ))"
| "af_letter (φ W⇩n ψ) ν = (af_letter ψ ν) or⇩n ((af_letter φ ν) and⇩n (φ W⇩n ψ))"
| "af_letter (φ M⇩n ψ) ν = (af_letter ψ ν) and⇩n ((af_letter φ ν) or⇩n (φ M⇩n ψ))"

abbreviation af :: "'a ltln ⇒ 'a set list ⇒ 'a ltln"
where
"af φ w ≡ foldl af_letter φ w"

lemma af_decompose:
"af (φ and⇩n ψ) w = (af φ w) and⇩n (af ψ w)"
"af (φ or⇩n ψ) w = (af φ w) or⇩n (af ψ w)"
by (induction w rule: rev_induct) simp_all

lemma af_simps[simp]:
"af true⇩n w = true⇩n"
"af false⇩n w = false⇩n"
"af (X⇩n φ) (x # xs) = af φ xs"
by (induction w) simp_all

lemma af_ite_simps[simp]:
"af (if P then true⇩n else false⇩n) w = (if P then true⇩n else false⇩n)"
"af (if P then false⇩n else true⇩n) w = (if P then false⇩n else true⇩n)"
by simp_all

lemma af_subsequence_append:
"i ≤ j ⟹ j ≤ k ⟹ af (af φ (w [i → j])) (w [j → k]) = af φ (w [i → k])"
by (metis foldl_append le_Suc_ex map_append subsequence_def upt_add_eq_append)

lemma af_subsequence_U:
"af (φ U⇩n ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) or⇩n ((af φ (w [0 → Suc n])) and⇩n af (φ U⇩n ψ) (w [1 → Suc n]))"
by (induction n) fastforce+

lemma af_subsequence_U':
"af (φ U⇩n ψ) (a # xs) = (af ψ (a # xs)) or⇩n ((af φ (a # xs)) and⇩n af (φ U⇩n ψ) xs)"

lemma af_subsequence_R:
"af (φ R⇩n ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) and⇩n ((af φ (w [0 → Suc n])) or⇩n af (φ R⇩n ψ) (w [1 → Suc n]))"
by (induction n) fastforce+

lemma af_subsequence_R':
"af (φ R⇩n ψ) (a # xs) = (af ψ (a # xs)) and⇩n ((af φ (a # xs)) or⇩n af (φ R⇩n ψ) xs)"

lemma af_subsequence_W:
"af (φ W⇩n ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) or⇩n ((af φ (w [0 → Suc n])) and⇩n af (φ W⇩n ψ) (w [1 → Suc n]))"
by (induction n) fastforce+

lemma af_subsequence_W':
"af (φ W⇩n ψ) (a # xs) = (af ψ (a # xs)) or⇩n ((af φ (a # xs)) and⇩n af (φ W⇩n ψ) xs)"

lemma af_subsequence_M:
"af (φ M⇩n ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) and⇩n ((af φ (w [0 → Suc n])) or⇩n af (φ M⇩n ψ) (w [1 → Suc n]))"
by (induction n) fastforce+

lemma af_subsequence_M':
"af (φ M⇩n ψ) (a # xs) = (af ψ (a # xs)) and⇩n ((af φ (a # xs)) or⇩n af (φ M⇩n ψ) xs)"

lemma suffix_build[simp]:
"suffix (Suc n) (x ## xs) = suffix n xs"
by fastforce

lemma af_letter_build:
"(x ## w) ⊨⇩n φ ⟷ w ⊨⇩n af_letter φ x"
proof (induction φ arbitrary: x w)
case (Until_ltln φ ψ)
then show ?case
unfolding ltln_expand_Until by force
next
case (Release_ltln φ ψ)
then show ?case
unfolding ltln_expand_Release by force
next
case (WeakUntil_ltln φ ψ)
then show ?case
unfolding ltln_expand_WeakUntil by force
next
case (StrongRelease_ltln φ ψ)
then show ?case
unfolding ltln_expand_StrongRelease by force
qed simp+

lemma af_ltl_continuation:
"(w ⌢ w') ⊨⇩n φ ⟷ w' ⊨⇩n af φ w"
proof (induction w arbitrary: φ w')
case (Cons x xs)
then show ?case
using af_letter_build by fastforce
qed simp

subsection ‹Range of the after function›

lemma af_letter_atoms:
"atoms_ltln (af_letter φ ν) ⊆ atoms_ltln φ"
by (induction φ) auto

lemma af_atoms:
"atoms_ltln (af φ w) ⊆ atoms_ltln φ"
by (induction w rule: rev_induct) (simp, insert af_letter_atoms, fastforce)

lemma af_letter_nested_prop_atoms:
"nested_prop_atoms (af_letter φ ν) ⊆ nested_prop_atoms φ"
by (induction φ) auto

lemma af_nested_prop_atoms:
"nested_prop_atoms (af φ w) ⊆ nested_prop_atoms φ"
by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms, blast)

lemma af_letter_range:
"range (af_letter φ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
using af_letter_nested_prop_atoms by blast

lemma af_range:
"range (af φ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
using af_nested_prop_atoms by blast

subsection ‹Subformulas of the after function›

lemma af_letter_subformulas⇩μ:
"subformulas⇩μ (af_letter φ ξ) = subformulas⇩μ φ"
by (induction φ) auto

lemma af_subformulas⇩μ:
"subformulas⇩μ (af φ w) = subformulas⇩μ φ"
using af_letter_subformulas⇩μ
by (induction w arbitrary: φ rule: rev_induct) (simp, fastforce)

lemma af_letter_subformulas⇩ν:
"subformulas⇩ν (af_letter φ ξ) = subformulas⇩ν φ"
by (induction φ) auto

lemma af_subformulas⇩ν:
"subformulas⇩ν (af φ w) = subformulas⇩ν φ"
using af_letter_subformulas⇩ν
by (induction w arbitrary: φ rule: rev_induct) (simp, fastforce)

subsection ‹Stability and the after function›

lemma 𝒢ℱ_af:
"𝒢ℱ (af φ (prefix i w)) (suffix i w) = 𝒢ℱ φ (suffix i w)"
unfolding 𝒢ℱ_semantics' af_subformulas⇩μ by blast

lemma ℱ_af:
"ℱ (af φ (prefix i w)) (suffix i w) = ℱ φ (suffix i w)"
unfolding ℱ_semantics' af_subformulas⇩μ by blast

lemma ℱ𝒢_af:
"ℱ𝒢 (af φ (prefix i w)) (suffix i w) = ℱ𝒢 φ (suffix i w)"
unfolding ℱ𝒢_semantics' af_subformulas⇩ν by blast

lemma 𝒢_af:
"𝒢 (af φ (prefix i w)) (suffix i w) = 𝒢 φ (suffix i w)"
unfolding 𝒢_semantics' af_subformulas⇩ν by blast

subsection ‹Congruence›

lemma af_letter_lang_congruent:
"φ ∼⇩L ψ ⟹ af_letter φ ν ∼⇩L af_letter ψ ν"
unfolding ltl_lang_equiv_def
using af_letter_build by blast

lemma af_lang_congruent:
"φ ∼⇩L ψ ⟹ af φ w ∼⇩L af ψ w"
unfolding ltl_lang_equiv_def using af_ltl_continuation
by (induction φ) blast+

lemma af_letter_subst:
"af_letter φ ν = subst φ (λψ. Some (af_letter ψ ν))"
by (induction φ) auto

lemma af_letter_prop_congruent:
"φ ⟶⇩P ψ ⟹ af_letter φ ν ⟶⇩P af_letter ψ ν"
"φ ∼⇩P ψ ⟹ af_letter φ ν ∼⇩P af_letter ψ ν"
by (metis af_letter_subst subst_respects_ltl_prop_entailment)+

lemma af_prop_congruent:
"φ ⟶⇩P ψ ⟹ af φ w ⟶⇩P af ψ w"
"φ ∼⇩P ψ ⟹ af φ w ∼⇩P af ψ w"
by (induction w arbitrary: φ ψ) (insert af_letter_prop_congruent, fastforce+)

lemma af_letter_const_congruent:
"φ ∼⇩C ψ ⟹ af_letter φ ν ∼⇩C af_letter ψ ν"
by (metis af_letter_subst subst_respects_ltl_const_entailment)

lemma af_const_congruent:
"φ ∼⇩C ψ ⟹ af φ w ∼⇩C af ψ w"
by (induction w arbitrary: φ ψ) (insert af_letter_const_congruent, fastforce+)

lemma af_letter_one_step_back:
"{x. 𝒜 ⊨⇩P af_letter x σ} ⊨⇩P φ ⟷ 𝒜 ⊨⇩P af_letter φ σ"
by (induction φ) simp_all

subsection ‹Implications›

lemma af_F_prefix_prop:
"af (F⇩n φ) w ⟶⇩P af (F⇩n φ) (w' @ w)"
by (induction w') (simp add: ltl_prop_implies_def af_decompose(1,2))+

lemma af_G_prefix_prop:
"af (G⇩n φ) (w' @ w) ⟶⇩P af (G⇩n φ) w"
by (induction w') (simp add: ltl_prop_implies_def af_decompose(1,2))+

lemma af_F_prefix_lang:
"w ⊨⇩n af (F⇩n φ) ys ⟹ w ⊨⇩n af (F⇩n φ) (xs @ ys)"
using af_F_prefix_prop ltl_prop_implication_implies_ltl_implication by blast

lemma af_G_prefix_lang:
"w ⊨⇩n af (G⇩n φ) (xs @ ys) ⟹ w ⊨⇩n af (G⇩n φ) ys"
using af_G_prefix_prop ltl_prop_implication_implies_ltl_implication by blast

lemma af_F_prefix_const_equiv_true:
"af (F⇩n φ) w ∼⇩C true⇩n ⟹ af (F⇩n φ) (w' @ w) ∼⇩C true⇩n"
using af_F_prefix_prop ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_true_implies_true by blast

lemma af_G_prefix_const_equiv_false:
"af (G⇩n φ) w ∼⇩C false⇩n ⟹ af (G⇩n φ) (w' @ w) ∼⇩C false⇩n"
using af_G_prefix_prop ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_false_implied_by_false by blast

lemma af_F_prefix_lang_equiv_true:
"af (F⇩n φ) w ∼⇩L true⇩n ⟹ af (F⇩n φ) (w' @ w) ∼⇩L true⇩n"
unfolding ltl_lang_equiv_def
using af_F_prefix_lang by fastforce

lemma af_G_prefix_lang_equiv_false:
"af (G⇩n φ) w ∼⇩L false⇩n ⟹ af (G⇩n φ) (w' @ w) ∼⇩L false⇩n"
unfolding ltl_lang_equiv_def
using af_G_prefix_lang by fastforce

locale af_congruent = ltl_equivalence +
assumes
af_letter_congruent: "φ ∼ ψ ⟹ af_letter φ ν ∼ af_letter ψ ν"
begin

lemma af_congruentness:
"φ ∼ ψ ⟹ af φ xs ∼ af ψ xs"
by (induction xs arbitrary: φ ψ) (insert af_letter_congruent, fastforce+)

lemma af_append_congruent:
"af φ w ∼ af ψ w ⟹ af φ (w @ w') ∼ af ψ (w @ w')"

lemma af_append_true:
"af φ w ∼ true⇩n ⟹ af φ (w @ w') ∼ true⇩n"
using af_congruentness by fastforce

lemma af_append_false:
"af φ w ∼ false⇩n ⟹ af φ (w @ w') ∼ false⇩n"
using af_congruentness by fastforce

lemma prefix_append_subsequence:
"i ≤ j ⟹ (prefix i w) @ (w [i → j]) = prefix j w"

lemma af_prefix_congruent:
"i ≤ j ⟹ af φ (prefix i w) ∼ af ψ (prefix i w) ⟹ af φ (prefix j w) ∼ af ψ (prefix j w)"
by (metis af_congruentness foldl_append prefix_append_subsequence)+

lemma af_prefix_true:
"i ≤ j ⟹ af φ (prefix i w) ∼ true⇩n ⟹ af φ (prefix j w) ∼ true⇩n"
by (metis af_append_true prefix_append_subsequence)

lemma af_prefix_false:
"i ≤ j ⟹ af φ (prefix i w) ∼ false⇩n ⟹ af φ (prefix j w) ∼ false⇩n"
by (metis af_append_false prefix_append_subsequence)

end

interpretation lang_af_congruent: af_congruent "(∼⇩L)"
by unfold_locales (rule af_letter_lang_congruent)

interpretation prop_af_congruent: af_congruent "(∼⇩P)"
by unfold_locales (rule af_letter_prop_congruent)

interpretation const_af_congruent: af_congruent "(∼⇩C)"
by unfold_locales (rule af_letter_const_congruent)

subsection ‹After in @{term μLTL} and @{term νLTL}›

lemma valid_prefix_implies_ltl:
"af φ (prefix i w) ∼⇩L true⇩n ⟹ w ⊨⇩n φ"
proof -
assume "af φ (prefix i w) ∼⇩L true⇩n"

then have "suffix i w ⊨⇩n af φ (prefix i w)"
unfolding ltl_lang_equiv_def using semantics_ltln.simps(1) by blast

then show "w ⊨⇩n φ"
using af_ltl_continuation by force
qed

lemma ltl_implies_satisfiable_prefix:
"w ⊨⇩n φ ⟹ ¬ (af φ (prefix i w) ∼⇩L false⇩n)"
proof -
assume "w ⊨⇩n φ"

then have "suffix i w ⊨⇩n af φ (prefix i w)"
using af_ltl_continuation by fastforce

then show "¬ (af φ (prefix i w) ∼⇩L false⇩n)"
unfolding ltl_lang_equiv_def using semantics_ltln.simps(2) by blast
qed

lemma μLTL_implies_valid_prefix:
"φ ∈ μLTL ⟹ w ⊨⇩n φ ⟹ ∃i. af φ (prefix i w) ∼⇩C true⇩n"
proof (induction φ arbitrary: w)
case True_ltln
then show ?case
using ltl_const_equiv_equivp equivp_reflp by fastforce
next
case (Prop_ltln x)
then show ?case
by (metis af_letter.simps(3) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(3) subsequence_singleton)
next
case (Nprop_ltln x)
then show ?case
by (metis af_letter.simps(4) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(4) subsequence_singleton)
next
case (And_ltln φ1 φ2)

then obtain i1 i2 where "af φ1 (prefix i1 w) ∼⇩C true⇩n" and "af φ2 (prefix i2 w) ∼⇩C true⇩n"
by fastforce

then have "af φ1 (prefix (i1 + i2) w) ∼⇩C true⇩n" and "af φ2 (prefix (i2 + i1) w) ∼⇩C true⇩n"

then have "af (φ1 and⇩n φ2) (prefix (i1 + i2) w) ∼⇩C true⇩n"

then show ?case
by blast
next
case (Or_ltln φ1 φ2)

then obtain i where "af φ1 (prefix i w) ∼⇩C true⇩n ∨ af φ2 (prefix i w) ∼⇩C true⇩n"
by auto

then show ?case
unfolding af_decompose by auto
next
case (Next_ltln φ)

then obtain i where "af φ (prefix i (suffix 1 w)) ∼⇩C true⇩n"
by fastforce

then show ?case
by (metis (no_types, lifting) One_nat_def add.right_neutral af_simps(3) foldl_Nil foldl_append subsequence_append subsequence_shift subsequence_singleton)
next
case (Until_ltln φ1 φ2)

then obtain k where "suffix k w ⊨⇩n φ2" and "∀j<k. suffix j w ⊨⇩n φ1"
by fastforce

then show ?case
proof (induction k arbitrary: w)
case 0

then obtain i where "af φ2 (prefix i w) ∼⇩C true⇩n"
using Until_ltln by fastforce

then have "af φ2 (prefix (Suc i) w) ∼⇩C true⇩n"
using const_af_congruent.af_prefix_true le_SucI by blast

then have "af (φ1 U⇩n φ2) (prefix (Suc i) w) ∼⇩C true⇩n"
unfolding af_subsequence_U by simp

then show ?case
by blast
next
case (Suc k)

then have "suffix k (suffix 1 w) ⊨⇩n φ2" and "∀j<k. suffix j (suffix 1 w) ⊨⇩n φ1"

then obtain i where i_def: "af (φ1 U⇩n φ2) (prefix i (suffix 1 w)) ∼⇩C true⇩n"
using Suc.IH by blast

obtain j where "af φ1 (prefix j w) ∼⇩C true⇩n"
using Until_ltln Suc by fastforce

then have "af φ1 (prefix (Suc (j + i)) w) ∼⇩C true⇩n"
using const_af_congruent.af_prefix_true le_SucI le_add1 by blast

moreover

from i_def have "af (φ1 U⇩n φ2) (w [1 → Suc (j + i)]) ∼⇩C true⇩n"
by (metis One_nat_def const_af_congruent.af_prefix_true le_add2 plus_1_eq_Suc subsequence_shift)

ultimately

have "af (φ1 U⇩n φ2) (prefix (Suc (j + i)) w) ∼⇩C true⇩n"
unfolding af_subsequence_U by simp

then show ?case
by blast
qed
next
case (StrongRelease_ltln φ1 φ2)

then obtain k where "suffix k w ⊨⇩n φ1" and "∀j≤k. suffix j w ⊨⇩n φ2"
by fastforce

then show ?case
proof (induction k arbitrary: w)
case 0

then obtain i1 i2 where "af φ1 (prefix i1 w) ∼⇩C true⇩n" and "af φ2 (prefix i2 w) ∼⇩C true⇩n"
using StrongRelease_ltln by fastforce

then have "af φ1 (prefix (Suc (i1 + i2)) w) ∼⇩C true⇩n" and "af φ2 (prefix (Suc (i2 + i1)) w) ∼⇩C true⇩n"
using const_af_congruent.af_prefix_true le_SucI le_add1 by blast+

then have "af (φ1 M⇩n φ2) (prefix (Suc (i1 + i2)) w) ∼⇩C true⇩n"

then show ?case
by blast
next
case (Suc k)

then have "suffix k (suffix 1 w) ⊨⇩n φ1" and "∀j≤k. suffix j (suffix 1 w) ⊨⇩n φ2"

then obtain i where i_def: "af (φ1 M⇩n φ2) (prefix i (suffix 1 w)) ∼⇩C true⇩n"
using Suc.IH by blast

obtain j where "af φ2 (prefix j w) ∼⇩C true⇩n"
using StrongRelease_ltln Suc by fastforce

then have "af φ2 (prefix (Suc (j + i)) w) ∼⇩C true⇩n"
using const_af_congruent.af_prefix_true le_SucI le_add1 by blast

moreover

from i_def have "af (φ1 M⇩n φ2) (w [1 → Suc (j + i)]) ∼⇩C true⇩n"
by (metis One_nat_def const_af_congruent.af_prefix_true le_add2 plus_1_eq_Suc subsequence_shift)

ultimately

have "af (φ1 M⇩n φ2) (prefix (Suc (j + i)) w) ∼⇩C true⇩n"
unfolding af_subsequence_M by simp

then show ?case
by blast
qed
qed force+

lemma satisfiable_prefix_implies_νLTL:
"φ ∈ νLTL ⟹ ∄i. af φ (prefix i w) ∼⇩C false⇩n ⟹ w ⊨⇩n φ"
proof (erule contrapos_np, induction φ arbitrary: w)
case False_ltln
then show ?case
using ltl_const_equiv_equivp equivp_reflp by fastforce
next
case (Prop_ltln x)
then show ?case
by (metis af_letter.simps(3) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(3) subsequence_singleton)
next
case (Nprop_ltln x)
then show ?case
by (metis af_letter.simps(4) foldl_Cons foldl_Nil ltl_const_equiv_equivp equivp_reflp semantics_ltln.simps(4) subsequence_singleton)
next
case (And_ltln φ1 φ2)

then obtain i where "af φ1 (prefix i w) ∼⇩C false⇩n ∨ af φ2 (prefix i w) ∼⇩C false⇩n"
by auto

then show ?case
unfolding af_decompose by auto
next
case (Or_ltln φ1 φ2)

then obtain i1 i2 where "af φ1 (prefix i1 w) ∼⇩C false⇩n" and "af φ2 (prefix i2 w) ∼⇩C false⇩n"
by fastforce

then have "af φ1 (prefix (i1 + i2) w) ∼⇩C false⇩n" and "af φ2 (prefix (i2 + i1) w) ∼⇩C false⇩n"

then have "af (φ1 or⇩n φ2) (prefix (i1 + i2) w) ∼⇩C false⇩n"

then show ?case
by blast
next
case (Next_ltln φ)

then obtain i where "af φ (prefix i (suffix 1 w)) ∼⇩C false⇩n"
by fastforce

then show ?case
by (metis (no_types, lifting) One_nat_def add.right_neutral af_simps(3) foldl_Nil foldl_append subsequence_append subsequence_shift subsequence_singleton)
next
case (Release_ltln φ1 φ2)

then obtain k where "¬ suffix k w ⊨⇩n φ2" and "∀j<k. ¬ suffix j w ⊨⇩n φ1"
by fastforce

then show ?case
proof (induction k arbitrary: w)
case 0

then obtain i where "af φ2 (prefix i w) ∼⇩C false⇩n"
using Release_ltln by fastforce

then have "af φ2 (prefix (Suc i) w) ∼⇩C false⇩n"
using const_af_congruent.af_prefix_false le_SucI by blast

then have "af (φ1 R⇩n φ2) (prefix (Suc i) w) ∼⇩C false⇩n"
unfolding af_subsequence_R by simp

then show ?case
by blast
next
case (Suc k)

then have "¬ suffix k (suffix 1 w) ⊨⇩n φ2" and "∀j<k. ¬ suffix j (suffix 1 w) ⊨⇩n φ1"

then obtain i where i_def: "af (φ1 R⇩n φ2) (prefix i (suffix 1 w)) ∼⇩C false⇩n"
using Suc.IH by blast

obtain j where "af φ1 (prefix j w) ∼⇩C false⇩n"
using Release_ltln Suc by fastforce

then have "af φ1 (prefix (Suc (j + i)) w) ∼⇩C false⇩n"
using const_af_congruent.af_prefix_false le_SucI le_add1 by blast

moreover

from i_def have "af (φ1 R⇩n φ2) (w [1 → Suc (j + i)]) ∼⇩C false⇩n"
by (metis One_nat_def const_af_congruent.af_prefix_false le_add2 plus_1_eq_Suc subsequence_shift)

ultimately

have "af (φ1 R⇩n φ2) (prefix (Suc (j + i)) w) ∼⇩C false⇩n"
unfolding af_subsequence_R by auto

then show ?case
by blast
qed
next
case (WeakUntil_ltln φ1 φ2)

then obtain k where "¬ suffix k w ⊨⇩n φ1" and "∀j≤k. ¬ suffix j w ⊨⇩n φ2"
by fastforce

then show ?case
proof (induction k arbitrary: w)
case 0

then obtain i1 i2 where "af φ1 (prefix i1 w) ∼⇩C false⇩n" and "af φ2 (prefix i2 w) ∼⇩C false⇩n"
using WeakUntil_ltln by fastforce

then have "af φ1 (prefix (Suc (i1 + i2)) w) ∼⇩C false⇩n" and "af φ2 (prefix (Suc (i2 + i1)) w) ∼⇩C false⇩n"
using const_af_congruent.af_prefix_false le_SucI le_add1 by blast+

then have "af (φ1 W⇩n φ2) (prefix (Suc (i1 + i2)) w) ∼⇩C false⇩n"

then show ?case
by blast
next
case (Suc k)

then have "¬ suffix k (suffix 1 w) ⊨⇩n φ1" and "∀j≤k. ¬ suffix j (suffix 1 w) ⊨⇩n φ2"

then obtain i where i_def: "af (φ1 W⇩n φ2) (prefix i (suffix 1 w)) ∼⇩C false⇩n"
using Suc.IH by blast

obtain j where "af φ2 (prefix j w) ∼⇩C false⇩n"
using WeakUntil_ltln Suc by fastforce

then have "af φ2 (prefix (Suc (j + i)) w) ∼⇩C false⇩n"
using const_af_congruent.af_prefix_false le_SucI le_add1 by blast

moreover

from i_def have "af (φ1 W⇩n φ2) (w [1 → Suc (j + i)]) ∼⇩C false⇩n"
by (metis One_nat_def const_af_congruent.af_prefix_false le_add2 plus_1_eq_Suc subsequence_shift)

ultimately

have "af (φ1 W⇩n φ2) (prefix (Suc (j + i)) w) ∼⇩C false⇩n"
unfolding af_subsequence_W by simp

then show ?case
by blast
qed
qed force+

context ltl_equivalence
begin

lemma valid_prefix_implies_ltl:
"af φ (prefix i w) ∼ true⇩n ⟹ w ⊨⇩n φ"
using valid_prefix_implies_ltl eq_implies_lang by blast

lemma ltl_implies_satisfiable_prefix:
"w ⊨⇩n φ ⟹ ¬ (af φ (prefix i w) ∼ false⇩n)"
using ltl_implies_satisfiable_prefix eq_implies_lang by blast

lemma μLTL_implies_valid_prefix:
"φ ∈ μLTL ⟹ w ⊨⇩n φ ⟹ ∃i. af φ (prefix i w) ∼ true⇩n"
using μLTL_implies_valid_prefix const_implies_eq by blast

lemma satisfiable_prefix_implies_νLTL:
"φ ∈ νLTL ⟹ ∄i. af φ (prefix i w) ∼ false⇩n ⟹ w ⊨⇩n φ"
using satisfiable_prefix_implies_νLTL const_implies_eq by blast

lemma af_μLTL:
"φ ∈ μLTL ⟹ w ⊨⇩n φ ⟷ (∃i. af φ (prefix i w) ∼ true⇩n)"
using valid_prefix_implies_ltl μLTL_implies_valid_prefix by blast

lemma af_νLTL:
"φ ∈ νLTL ⟹ w ⊨⇩n φ ⟷ (∀i. ¬ (af φ (prefix i w) ∼ false⇩n))"
using ltl_implies_satisfiable_prefix satisfiable_prefix_implies_νLTL by blast

lemma af_μLTL_GF:
"φ ∈ μLTL ⟹ w ⊨⇩n G⇩n (F⇩n φ) ⟷ (∀i. ∃j. af (F⇩n φ) (w[i → j]) ∼ true⇩n)"
proof -
assume "φ ∈ μLTL"

then have "F⇩n φ ∈ μLTL"
by simp

have "w ⊨⇩n G⇩n (F⇩n φ) ⟷ (∀i. suffix i w ⊨⇩n F⇩n φ)"
by simp
also have "… ⟷ (∀i. ∃j. af (F⇩n φ) (prefix j (suffix i w)) ∼ true⇩n)"
using af_μLTL[OF ‹F⇩n φ ∈ μLTL›] by blast
also have "… ⟷ (∀i. ∃j. af (F⇩n φ) (prefix (j - i) (suffix i w)) ∼ true⇩n)"
also have "… ⟷ (∀i. ∃j. af (F⇩n φ) (w[i → j]) ∼ true⇩n)"
unfolding subsequence_prefix_suffix ..
finally show ?thesis
by blast
qed

lemma af_νLTL_FG:
"φ ∈ νLTL ⟹ w ⊨⇩n F⇩n (G⇩n φ) ⟷ (∃i. ∀j. ¬ (af (G⇩n φ) (w[i → j]) ∼ false⇩n))"
proof -
assume "φ ∈ νLTL"

then have "G⇩n φ ∈ νLTL"
by simp

have "w ⊨⇩n F⇩n (G⇩n φ) ⟷ (∃i. suffix i w ⊨⇩n G⇩n φ)"
by force
also have "… ⟷ (∃i. ∀j. ¬ (af (G⇩n φ) (prefix j (suffix i w)) ∼ false⇩n))"
using af_νLTL[OF ‹G⇩n φ ∈ νLTL›] by blast
also have "… ⟷ (∃i. ∀j. ¬ (af (G⇩n φ) (prefix (j - i) (suffix i w)) ∼ false⇩n))"
also have "… ⟷ (∃i. ∀j. ¬ (af (G⇩n φ) (w[i → j]) ∼ false⇩n))"
unfolding subsequence_prefix_suffix ..
finally show ?thesis
by blast
qed

end

text ‹Bring Propositional Equivalence into scope›

interpretation af_congruent "(∼⇩P)"
by unfold_locales (rule af_letter_prop_congruent)

end
```