```(*
Author:   Benedikt Seidl
Author:   Salomon Sickert
*)

imports
LTL.LTL LTL.Equivalence_Relations
Syntactic_Fragments_and_Stability After
begin

subsection ‹The GF and FG Advice Functions›

fun GF_advice :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln" ("_[_]⇩ν" [90,60] 89)
where
"(X⇩n ψ)[X]⇩ν = X⇩n (ψ[X]⇩ν)"
| "(ψ⇩1 and⇩n ψ⇩2)[X]⇩ν = (ψ⇩1[X]⇩ν) and⇩n (ψ⇩2[X]⇩ν)"
| "(ψ⇩1 or⇩n ψ⇩2)[X]⇩ν = (ψ⇩1[X]⇩ν) or⇩n (ψ⇩2[X]⇩ν)"
| "(ψ⇩1 W⇩n ψ⇩2)[X]⇩ν = (ψ⇩1[X]⇩ν) W⇩n (ψ⇩2[X]⇩ν)"
| "(ψ⇩1 R⇩n ψ⇩2)[X]⇩ν = (ψ⇩1[X]⇩ν) R⇩n (ψ⇩2[X]⇩ν)"
| "(ψ⇩1 U⇩n ψ⇩2)[X]⇩ν = (if (ψ⇩1 U⇩n ψ⇩2) ∈ X then (ψ⇩1[X]⇩ν) W⇩n (ψ⇩2[X]⇩ν) else false⇩n)"
| "(ψ⇩1 M⇩n ψ⇩2)[X]⇩ν = (if (ψ⇩1 M⇩n ψ⇩2) ∈ X then (ψ⇩1[X]⇩ν) R⇩n (ψ⇩2[X]⇩ν) else false⇩n)"
| "φ[_]⇩ν = φ"

fun FG_advice :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln" ("_[_]⇩μ" [90,60] 89)
where
"(X⇩n ψ)[Y]⇩μ = X⇩n (ψ[Y]⇩μ)"
| "(ψ⇩1 and⇩n ψ⇩2)[Y]⇩μ = (ψ⇩1[Y]⇩μ) and⇩n (ψ⇩2[Y]⇩μ)"
| "(ψ⇩1 or⇩n ψ⇩2)[Y]⇩μ = (ψ⇩1[Y]⇩μ) or⇩n (ψ⇩2[Y]⇩μ)"
| "(ψ⇩1 U⇩n ψ⇩2)[Y]⇩μ = (ψ⇩1[Y]⇩μ) U⇩n (ψ⇩2[Y]⇩μ)"
| "(ψ⇩1 M⇩n ψ⇩2)[Y]⇩μ = (ψ⇩1[Y]⇩μ) M⇩n (ψ⇩2[Y]⇩μ)"
| "(ψ⇩1 W⇩n ψ⇩2)[Y]⇩μ = (if (ψ⇩1 W⇩n ψ⇩2) ∈ Y then true⇩n else (ψ⇩1[Y]⇩μ) U⇩n (ψ⇩2[Y]⇩μ))"
| "(ψ⇩1 R⇩n ψ⇩2)[Y]⇩μ = (if (ψ⇩1 R⇩n ψ⇩2) ∈ Y then true⇩n else (ψ⇩1[Y]⇩μ) M⇩n (ψ⇩2[Y]⇩μ))"
| "φ[_]⇩μ = φ"

"φ[X]⇩ν ∈ νLTL"
"φ ∈ νLTL ⟹ φ[X]⇩ν = φ"
by (induction φ) auto

"φ[X]⇩μ ∈ μLTL"
"φ ∈ μLTL ⟹ φ[X]⇩μ = φ"
by (induction φ) auto

"subfrmlsn (φ[X]⇩ν) ⊆ {ψ[X]⇩ν | ψ. ψ ∈ subfrmlsn φ}"
by (induction φ) force+

"subfrmlsn (φ[Y]⇩μ) ⊆ {ψ[Y]⇩μ | ψ. ψ ∈ subfrmlsn φ}"
by (induction φ) force+

"card (subfrmlsn (φ[X]⇩ν)) ≤ card (subfrmlsn φ)"
proof -
have "card (subfrmlsn (φ[X]⇩ν)) ≤ card {ψ[X]⇩ν | ψ. ψ ∈ subfrmlsn φ}"

also have "… ≤ card (subfrmlsn φ)"
by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite)

finally show ?thesis .
qed

"card (subfrmlsn (φ[Y]⇩μ)) ≤ card (subfrmlsn φ)"
proof -
have "card (subfrmlsn (φ[Y]⇩μ)) ≤ card {ψ[Y]⇩μ | ψ. ψ ∈ subfrmlsn φ}"

also have "… ≤ card (subfrmlsn φ)"
by (metis Collect_mem_eq card_image_le image_Collect subfrmlsn_finite)

finally show ?thesis .
qed

"X ⊆ Y ⟹ w ⊨⇩n φ[X]⇩ν ⟹ w ⊨⇩n φ[Y]⇩ν"
proof (induction φ arbitrary: w)
case (Until_ltln φ ψ)
then show ?case
by (cases "φ U⇩n ψ ∈ X") (simp_all, blast)
next
case (Release_ltln φ ψ)
then show ?case by (simp, blast)
next
case (WeakUntil_ltln φ ψ)
then show ?case by (simp, blast)
next
case (StrongRelease_ltln φ ψ)
then show ?case
by (cases "φ M⇩n ψ ∈ X") (simp_all, blast)
qed auto

"X ⊆ Y ⟹ w ⊨⇩n φ[X]⇩μ ⟹ w ⊨⇩n φ[Y]⇩μ"
proof (induction φ arbitrary: w)
case (Until_ltln φ ψ)
then show ?case by (simp, blast)
next
case (Release_ltln φ ψ)
then show ?case
by (cases "φ R⇩n ψ ∈ X") (auto, blast)
next
case (WeakUntil_ltln φ ψ)
then show ?case
by (cases "φ W⇩n ψ ∈ X") (auto, blast)
next
case (StrongRelease_ltln φ ψ)
then show ?case by (simp, blast)
qed auto

"(if P then true⇩n else false⇩n)[X]⇩ν = (if P then true⇩n else false⇩n)"
"(if P then false⇩n else true⇩n)[X]⇩ν = (if P then false⇩n else true⇩n)"
by simp_all

"(if P then true⇩n else false⇩n)[Y]⇩μ = (if P then true⇩n else false⇩n)"
"(if P then false⇩n else true⇩n)[Y]⇩μ = (if P then false⇩n else true⇩n)"
by simp_all

subsection ‹Advice Functions on Nested Propositions›

definition nested_prop_atoms⇩ν :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln set"
where
"nested_prop_atoms⇩ν φ X = {ψ[X]⇩ν | ψ. ψ ∈ nested_prop_atoms φ}"

definition nested_prop_atoms⇩μ :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln set"
where
"nested_prop_atoms⇩μ φ X = {ψ[X]⇩μ | ψ. ψ ∈ nested_prop_atoms φ}"

lemma nested_prop_atoms⇩ν_finite:
"finite (nested_prop_atoms⇩ν φ X)"

lemma nested_prop_atoms⇩μ_finite:
"finite (nested_prop_atoms⇩μ φ X)"

lemma nested_prop_atoms⇩ν_card:
"card (nested_prop_atoms⇩ν φ X) ≤ card (nested_prop_atoms φ)"
unfolding nested_prop_atoms⇩ν_def
by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite)

lemma nested_prop_atoms⇩μ_card:
"card (nested_prop_atoms⇩μ φ X) ≤ card (nested_prop_atoms φ)"
unfolding nested_prop_atoms⇩μ_def
by (metis Collect_mem_eq card_image_le image_Collect nested_prop_atoms_finite)

"nested_prop_atoms (φ[X]⇩ν) ⊆ nested_prop_atoms⇩ν φ X"
by (induction φ) (unfold nested_prop_atoms⇩ν_def, force+)

"nested_prop_atoms (φ[Y]⇩μ) ⊆ nested_prop_atoms⇩μ φ Y"
by (induction φ) (unfold nested_prop_atoms⇩μ_def, force+)

lemma nested_prop_atoms⇩ν_subset:
"nested_prop_atoms φ ⊆ nested_prop_atoms ψ ⟹ nested_prop_atoms⇩ν φ X ⊆ nested_prop_atoms⇩ν ψ X"
unfolding nested_prop_atoms⇩ν_def by blast

lemma nested_prop_atoms⇩μ_subset:
"nested_prop_atoms φ ⊆ nested_prop_atoms ψ ⟹ nested_prop_atoms⇩μ φ Y ⊆ nested_prop_atoms⇩μ ψ Y"
unfolding nested_prop_atoms⇩μ_def by blast

"card (nested_prop_atoms (φ[X]⇩ν)) ≤ card (nested_prop_atoms φ)"
proof -
have "card (nested_prop_atoms (φ[X]⇩ν)) ≤ card (nested_prop_atoms⇩ν φ X)"

then show ?thesis
using nested_prop_atoms⇩ν_card le_trans by blast
qed

"card (nested_prop_atoms (φ[Y]⇩μ)) ≤ card (nested_prop_atoms φ)"
proof -
have "card (nested_prop_atoms (φ[Y]⇩μ)) ≤ card (nested_prop_atoms⇩μ φ Y)"

then show ?thesis
using nested_prop_atoms⇩μ_card le_trans by blast
qed

"X ∩ subformulas⇩μ φ ⊆ S ⟹ φ[X ∩ S]⇩ν = φ[X]⇩ν"
by (induction φ) auto

"φ[X ∩ subformulas⇩μ φ]⇩ν = φ[X]⇩ν"

"ψ ∉ subformulas⇩μ φ ⟹ φ[X - {ψ}]⇩ν = φ[X]⇩ν"
proof -
assume "ψ ∉ subformulas⇩μ φ"
then have "subformulas⇩μ φ ∩ X ⊆ X - {ψ}"
by blast
then show "φ[X - {ψ}]⇩ν = φ[X]⇩ν"
by (metis GF_advice_inter Diff_subset Int_absorb1 inf.commute)
qed

"⟦size φ ≤ size ψ; φ ≠ ψ⟧ ⟹ φ[X - {ψ}]⇩ν = φ[X]⇩ν"
by fastforce

"Y ∩ subformulas⇩ν φ ⊆ S ⟹ φ[Y ∩ S]⇩μ = φ[Y]⇩μ"
by (induction φ) auto

"φ[Y ∩ subformulas⇩ν φ]⇩μ = φ[Y]⇩μ"

"ψ ∉ subformulas⇩ν φ ⟹ φ[Y - {ψ}]⇩μ = φ[Y]⇩μ"
proof -
assume "ψ ∉ subformulas⇩ν φ"
then have "subformulas⇩ν φ ∩ Y ⊆ Y - {ψ}"
by blast
then show "φ[Y - {ψ}]⇩μ  = φ[Y]⇩μ"
by (metis FG_advice_inter Diff_subset Int_absorb1 inf.commute)
qed

"⟦size φ ≤ size ψ; φ ≠ ψ⟧ ⟹ φ[Y - {ψ}]⇩μ = φ[Y]⇩μ"
by fastforce

"⟦ψ ∉ Y; size φ < size ψ⟧ ⟹ φ[insert ψ Y]⇩μ = φ[Y]⇩μ"
by (metis FG_advice_minus_size Diff_insert_absorb less_imp_le neq_iff)

"⟦ℱ φ w ⊆ X; w ⊨⇩n φ⟧ ⟹ w ⊨⇩n φ[X]⇩ν"
proof (induction φ arbitrary: w)
case (Next_ltln φ)
then show ?case
using ℱ_suffix by simp blast
next
case (Until_ltln φ1 φ2)

have "ℱ (φ1 W⇩n φ2) w ⊆ ℱ (φ1 U⇩n φ2) w"
by fastforce
then have "ℱ (φ1 W⇩n φ2) w ⊆ X" and "w ⊨⇩n φ1 W⇩n φ2"
using Until_ltln.prems ltln_strong_to_weak by blast+
then have "w ⊨⇩n φ1[X]⇩ν W⇩n φ2[X]⇩ν"
using Until_ltln.IH
by simp (meson ℱ_suffix subset_trans sup.boundedE)

moreover

have "w ⊨⇩n φ1 U⇩n φ2"
using Until_ltln.prems by simp
then have "φ1 U⇩n φ2 ∈ ℱ (φ1 U⇩n φ2) w"
by force
then have "φ1 U⇩n φ2 ∈ X"
using Until_ltln.prems by fast

ultimately show ?case
by auto
next
case (Release_ltln φ1 φ2)
then show ?case
by simp (meson ℱ_suffix subset_trans sup.boundedE)
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
by simp (meson ℱ_suffix subset_trans sup.boundedE)
next
case (StrongRelease_ltln φ1 φ2)

have "ℱ (φ1 R⇩n φ2) w ⊆ ℱ (φ1 M⇩n φ2) w"
by fastforce
then have "ℱ (φ1 R⇩n φ2) w ⊆ X" and "w ⊨⇩n φ1 R⇩n φ2"
using StrongRelease_ltln.prems ltln_strong_to_weak by blast+
then have "w ⊨⇩n φ1[X]⇩ν R⇩n φ2[X]⇩ν"
using StrongRelease_ltln.IH
by simp (meson ℱ_suffix subset_trans sup.boundedE)

moreover

have "w ⊨⇩n φ1 M⇩n φ2"
using StrongRelease_ltln.prems by simp
then have "φ1 M⇩n φ2 ∈ ℱ (φ1 M⇩n φ2) w"
by force
then have "φ1 M⇩n φ2 ∈ X"
using StrongRelease_ltln.prems by fast

ultimately show ?case
by auto
qed auto

"⟦∀ψ ∈ X. w ⊨⇩n G⇩n (F⇩n ψ); w ⊨⇩n φ[X]⇩ν⟧ ⟹ w ⊨⇩n φ"
proof (induction φ arbitrary: w)
case (Next_ltln φ)
then show ?case
using GF_suffix by blast
next
case (Until_ltln φ1 φ2)

then have "φ1 U⇩n φ2 ∈ X"
using ccontr[of "φ1 U⇩n φ2 ∈ X"] by force
then have "w ⊨⇩n F⇩n φ2"
using Until_ltln.prems by fastforce

moreover

have "w ⊨⇩n (φ1 U⇩n φ2)[X]⇩ν"
using Until_ltln.prems by simp
then have "w ⊨⇩n (φ1[X]⇩ν) W⇩n (φ2[X]⇩ν)"
unfolding GF_advice.simps using ‹φ1 U⇩n φ2 ∈ X› by simp
then have "w ⊨⇩n φ1 W⇩n φ2"
by (metis GF_suffix Until_ltln.IH Until_ltln.prems(1))

ultimately show ?case
using ltln_weak_to_strong by blast
next
case (Release_ltln φ1 φ2)
then show ?case
by (metis GF_suffix Release_ltln.IH Release_ltln.prems(1))
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
by (metis GF_suffix)
next
case (StrongRelease_ltln φ1 φ2)

then have "φ1 M⇩n φ2 ∈ X"
using ccontr[of "φ1 M⇩n φ2 ∈ X"] by force
then have "w ⊨⇩n F⇩n φ1"
using StrongRelease_ltln.prems by fastforce

moreover

have "w ⊨⇩n (φ1 M⇩n φ2)[X]⇩ν"
using StrongRelease_ltln.prems by simp
then have "w ⊨⇩n (φ1[X]⇩ν) R⇩n (φ2[X]⇩ν)"
unfolding GF_advice.simps using ‹φ1 M⇩n φ2 ∈ X› by simp
then have "w ⊨⇩n φ1 R⇩n φ2"
by (metis GF_suffix StrongRelease_ltln.IH StrongRelease_ltln.prems(1))

ultimately show ?case
using ltln_weak_to_strong by blast
qed auto

"⟦X ⊆ 𝒢ℱ φ w; w ⊨⇩n φ[X]⇩ν⟧ ⟹ w ⊨⇩n φ"

"⟦X = ℱ φ w; X = 𝒢ℱ φ w⟧ ⟹ w ⊨⇩n φ ⟷ w ⊨⇩n φ[X]⇩ν"

"⟦ℱ𝒢 φ w ⊆ Y; w ⊨⇩n φ⟧ ⟹ w ⊨⇩n φ[Y]⇩μ"
proof (induction φ arbitrary: w)
case (Next_ltln φ)
then show ?case
using ℱ𝒢_suffix by simp blast
next
case (Until_ltln φ1 φ2)
then show ?case
by simp (metis ℱ𝒢_suffix)
next
case (Release_ltln φ1 φ2)

show ?case
proof (cases "φ1 R⇩n φ2 ∈ Y")
case False
then have "φ1 R⇩n φ2 ∉ ℱ𝒢 (φ1 R⇩n φ2) w"
using Release_ltln.prems by blast
then have "¬ w ⊨⇩n G⇩n φ2"
by fastforce
then have "w ⊨⇩n φ1 M⇩n φ2"
using Release_ltln.prems ltln_weak_to_strong by blast

moreover

have "ℱ𝒢 (φ1 M⇩n φ2) w ⊆ ℱ𝒢 (φ1 R⇩n φ2) w"
by fastforce
then have "ℱ𝒢 (φ1 M⇩n φ2) w ⊆ Y"
using Release_ltln.prems by blast

ultimately show ?thesis
using Release_ltln.IH by simp (metis ℱ𝒢_suffix)
qed simp
next
case (WeakUntil_ltln φ1 φ2)

show ?case
proof (cases "φ1 W⇩n φ2 ∈ Y")
case False
then have "φ1 W⇩n φ2 ∉ ℱ𝒢 (φ1 W⇩n φ2) w"
using WeakUntil_ltln.prems by blast
then have "¬ w ⊨⇩n G⇩n φ1"
by fastforce
then have "w ⊨⇩n φ1 U⇩n φ2"
using WeakUntil_ltln.prems ltln_weak_to_strong by blast

moreover

have "ℱ𝒢 (φ1 U⇩n φ2) w ⊆ ℱ𝒢 (φ1 W⇩n φ2) w"
by fastforce
then have "ℱ𝒢 (φ1 U⇩n φ2) w ⊆ Y"
using WeakUntil_ltln.prems by blast

ultimately show ?thesis
using WeakUntil_ltln.IH by simp (metis ℱ𝒢_suffix)
qed simp
next
case (StrongRelease_ltln φ1 φ2)
then show ?case
by simp (metis ℱ𝒢_suffix)
qed auto

"⟦∀ψ ∈ Y. w ⊨⇩n G⇩n ψ; w ⊨⇩n φ[Y]⇩μ⟧ ⟹ w ⊨⇩n φ"
proof (induction φ arbitrary: w)
case (Until_ltln φ1 φ2)
then show ?case
by simp (metis (no_types, lifting) suffix_suffix)
next
case (Release_ltln φ1 φ2)
then show ?case
proof (cases "φ1 R⇩n φ2 ∈ Y")
case True
then show ?thesis
using Release_ltln.prems by force
next
case False
then have "w ⊨⇩n (φ1[Y]⇩μ) M⇩n (φ2[Y]⇩μ)"
using Release_ltln.prems by simp
then have "w ⊨⇩n φ1 M⇩n φ2"
using Release_ltln
by simp (metis (no_types, lifting) suffix_suffix)
then show ?thesis
using ltln_strong_to_weak by fast
qed
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
proof (cases "φ1 W⇩n φ2 ∈ Y")
case True
then show ?thesis
using WeakUntil_ltln.prems by force
next
case False
then have "w ⊨⇩n (φ1[Y]⇩μ) U⇩n (φ2[Y]⇩μ)"
using WeakUntil_ltln.prems by simp
then have "w ⊨⇩n φ1 U⇩n φ2"
using WeakUntil_ltln
by simp (metis (no_types, lifting) suffix_suffix)
then show ?thesis
using ltln_strong_to_weak by fast
qed
next
case (StrongRelease_ltln φ1 φ2)
then show ?case
by simp (metis (no_types, lifting) suffix_suffix)
qed auto

"⟦Y ⊆ 𝒢 φ w; w ⊨⇩n φ[Y]⇩μ⟧ ⟹ w ⊨⇩n φ"

"⟦Y = ℱ𝒢 φ w; Y = 𝒢 φ w⟧ ⟹ w ⊨⇩n φ ⟷ w ⊨⇩n φ[Y]⇩μ"

subsection ‹Advice Functions and the ``after'' Function›

"(x ## w) ⊨⇩n φ[X]⇩ν ⟹ w ⊨⇩n (af_letter φ x)[X]⇩ν"
proof (induction φ)
case (Until_ltln φ1 φ2)

then have "w ⊨⇩n af_letter ((φ1 U⇩n φ2)[X]⇩ν) x"
using af_letter_build by blast

then show ?case
using Until_ltln.IH af_letter_build by fastforce
next
case (Release_ltln φ1 φ2)

then have "w ⊨⇩n af_letter ((φ1 R⇩n φ2)[X]⇩ν) x"
using af_letter_build by blast

then show ?case
using Release_ltln.IH af_letter_build by auto
next
case (WeakUntil_ltln φ1 φ2)

then have "w ⊨⇩n af_letter ((φ1 W⇩n φ2)[X]⇩ν) x"
using af_letter_build by blast

then show ?case
using WeakUntil_ltln.IH af_letter_build by auto
next
case (StrongRelease_ltln φ1 φ2)

then have "w ⊨⇩n af_letter ((φ1 M⇩n φ2)[X]⇩ν) x"
using af_letter_build by blast

then show ?case
using StrongRelease_ltln.IH af_letter_build by force
qed auto

"w ⊨⇩n (af_letter φ x)[Y]⇩μ ⟹ (x ## w) ⊨⇩n φ[Y]⇩μ"
proof (induction φ)
case (Prop_ltln a)
then show ?case
using semantics_ltln.simps(3) by fastforce
next
case (Until_ltln φ1 φ2)
then show ?case
using af_letter_build apply (cases "w ⊨⇩n af_letter φ2 x[Y]⇩μ") apply force
by (metis af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6))
next
case (Release_ltln φ1 φ2)
then show ?case
apply (cases "φ1 R⇩n φ2 ∈ Y")
apply simp
using af_letter_build  apply (cases "w ⊨⇩n af_letter φ1 x[Y]⇩μ") apply force
by (metis (full_types) af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6))
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
apply (cases "φ1 W⇩n φ2 ∈ Y")
apply simp
using af_letter_build  apply (cases "w ⊨⇩n af_letter φ2 x[Y]⇩μ") apply force
by (metis (full_types) af_letter.simps(8) semantics_ltln.simps(5) semantics_ltln.simps(6))
next
case (StrongRelease_ltln φ1 φ2)
then show ?case
using af_letter_build apply (cases "w ⊨⇩n af_letter φ1 x[Y]⇩μ") apply force
by (metis af_letter.simps(11) semantics_ltln.simps(5) semantics_ltln.simps(6))
qed auto

"(w ⌢ w') ⊨⇩n φ[X]⇩ν ⟹ w' ⊨⇩n (af φ w)[X]⇩ν"
by (induction w arbitrary: φ) (simp, insert GF_advice_af_letter, fastforce)

"w' ⊨⇩n (af φ w)[X]⇩μ ⟹ (w ⌢ w') ⊨⇩n φ[X]⇩μ"
by (induction w arbitrary: φ) (simp, insert FG_advice_af_letter, fastforce)

"w ⊨⇩n φ[X]⇩ν ⟹ suffix i w ⊨⇩n (af φ (prefix i w))[X]⇩ν"

"suffix i w ⊨⇩n (af φ (prefix i w))[X]⇩μ ⟹ w ⊨⇩n φ[X]⇩μ"

(* TODO move to Omega_Words_Fun.thy ?? *)
lemma prefix_suffix_subsequence: "prefix i (suffix j w) = (w [j → i + j])"

text ‹We show this generic lemma to prove the following theorems:›

fixes index :: "nat ⇒ nat"
fixes formula :: "nat ⇒ 'a ltln"
assumes "⋀i. i < n ⟹ ∃j. suffix ((index i) + j) w ⊨⇩n af (formula i) (w [index i → (index i) + j])[X]⇩ν"
shows "∃k. (∀i < n. k ≥ index i ∧ suffix k w ⊨⇩n af (formula i) (w [index i → k])[X]⇩ν)"
using assms
proof (induction n)
case (Suc n)

obtain k1 where leq1: "⋀i. i < n ⟹ k1 ≥ index i"
and suffix1: "⋀i. i < n ⟹ suffix k1 w ⊨⇩n af (formula i) (w [(index i) → k1])[X]⇩ν"
using Suc less_SucI by blast

obtain k2 where leq2: "k2 ≥ index n"
and suffix2: "suffix k2 w ⊨⇩n af (formula n) (w [index n → k2])[X]⇩ν"

define k where "k ≡ k1 + k2"

have "⋀i. i < Suc n ⟹ k ≥ index i"

moreover

{
have "⋀i. i < n ⟹ suffix k w ⊨⇩n af (formula i) (w [(index i) → k])[X]⇩ν"
unfolding k_def

moreover

have "suffix k w ⊨⇩n af (formula n) (w [index n → k])[X]⇩ν"
unfolding k_def

ultimately

have "⋀i. i ≤ n ⟹ suffix k w ⊨⇩n af (formula i) (w [(index i) → k])[X]⇩ν"
using nat_less_le by blast
}

ultimately

show ?case
by (meson less_Suc_eq_le)
qed simp

assumes "∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν"
assumes "∃i. suffix i w ⊨⇩n af ψ (prefix i w)[X]⇩ν"
shows "∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν ∧ suffix i w ⊨⇩n af ψ (prefix i w)[X]⇩ν"
proof -
let ?formula = "λi :: nat. (if (i = 0) then φ else ψ)"

have assms: "⋀i. i < 2 ⟹ ∃j. suffix j w ⊨⇩n af (?formula i) (w [0 → j])[X]⇩ν"
using assms by simp
obtain k where k_def: "⋀i :: nat. i < 2 ⟹ suffix k w ⊨⇩n af (if i = 0 then φ else ψ) (prefix k w)[X]⇩ν"
using GF_advice_sync[of "2" "λi. 0" w ?formula, simplified, OF assms, simplified] by blast
show ?thesis
using k_def[of 0] k_def[of 1] by auto
qed

assumes "⋀i. i < n ⟹ ∃j. suffix (i + j) w ⊨⇩n af φ (w [i → j + i])[X]⇩ν"
assumes "∃j. suffix (n + j) w ⊨⇩n af ψ (w [n → j + n])[X]⇩ν"
shows "∃k ≥ n. (∀j < n. suffix k w ⊨⇩n af φ (w [j → k])[X]⇩ν) ∧ suffix k w ⊨⇩n af ψ (w [n → k])[X]⇩ν"
proof -
let ?index = "λi. min i n"
let ?formula = "λi. if (i < n) then φ else ψ"

{
fix i
assume "i < Suc n"
then have min_def: "min i n = i"
by simp
have "∃j. suffix ((?index i) + j) w ⊨⇩n af (?formula i) (w [?index i → (?index i) + j])[X]⇩ν"
unfolding min_def
by (cases "i < n")
(metis (full_types) assms(1) add.commute, metis (full_types) assms(2) ‹i < Suc n› add.commute  less_SucE)
}

then obtain k where leq: "(⋀i. i < Suc n ⟹ min i n ≤ k)"
and suffix: "⋀i. i < Suc n ⟹ suffix k w ⊨⇩n af (if i < n then φ else ψ) (w [min i n → k])[X]⇩ν"
using GF_advice_sync[of "Suc n" ?index w ?formula X] by metis

have "∀j < n. suffix k w ⊨⇩n af φ (w [j → k])[X]⇩ν"
using suffix by (metis (full_types) less_SucI min.strict_order_iff)

moreover

have "suffix k w ⊨⇩n af ψ (w [n → k])[X]⇩ν"
using suffix[of n, simplified] by blast

moreover

have "k ≥ n"
using leq by presburger

ultimately
show ?thesis
by auto
qed

assumes "⋀i. i ≤ n ⟹ ∃j. suffix (i + j) w ⊨⇩n af φ (w [i → j + i])[X]⇩ν"
assumes "∃j. suffix (n + j) w ⊨⇩n af ψ (w [n → j + n])[X]⇩ν"
shows "∃k ≥ n. (∀j ≤ n. suffix k w ⊨⇩n af φ (w [j → k])[X]⇩ν) ∧ suffix k w ⊨⇩n af ψ (w [n → k])[X]⇩ν"
proof -
let ?index = "λi. min i n"
let ?formula = "λi. if (i ≤ n) then φ else ψ"

{
fix i
assume "i < Suc (Suc n)"
hence "∃j. suffix ((?index i) + j) w ⊨⇩n af (?formula i) (w [?index i → (?index i) + j])[X]⇩ν"
proof (cases "i < Suc n")
case True
then have min_def: "min i n = i"
by simp
show ?thesis
unfolding min_def by (metis (full_types) assms(1) Suc_leI Suc_le_mono True add.commute)
next
case False
then have i_def: "i = Suc n"
using ‹i < Suc (Suc n)› less_antisym by blast
have min_def: "min i n = n"
unfolding i_def by simp
show ?thesis
using assms(2) False
qed
}

then obtain k where leq: "(⋀i. i ≤ Suc n ⟹ min i n ≤ k)"
and suffix: "⋀i :: nat. i < Suc (Suc n) ⟹ suffix k w ⊨⇩n af (if i ≤ n then φ else ψ) (w [min i n → k])[X]⇩ν"
using GF_advice_sync[of "Suc (Suc n)" ?index w ?formula X]
by (metis (no_types, opaque_lifting) less_Suc_eq min_le_iff_disj)

have "∀j ≤ n. suffix k w ⊨⇩n af φ (w [j → k])[X]⇩ν"
using suffix by (metis (full_types) le_SucI less_Suc_eq_le min.orderE)

moreover

have "suffix k w ⊨⇩n af ψ (w [n → k])[X]⇩ν"
using suffix[of "Suc n", simplified] by linarith

moreover

have "k ≥ n"
using leq by presburger

ultimately
show ?thesis
by auto
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n ((af ψ (w [i → n]))[X]⇩ν)"
assumes "⋀j. j < i ⟹ suffix n w ⊨⇩n ((af φ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ U⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
then have A: "suffix n w ⊨⇩n ((af ψ (w [0 → n]))[X]⇩ν)"
by blast
then have "suffix (Suc n) w ⊨⇩n (af ψ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF A, of 1] by simp
then show ?case
unfolding GF_advice.simps af_subsequence_U semantics_ltln.simps by blast
next
case (Suc i)
have "suffix (Suc n) w ⊨⇩n (af φ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1]
by simp
moreover
have B: "(Suc (n - 1)) = n"
using Suc by simp
note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
then have "suffix (Suc n) w ⊨⇩n (af (φ U⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
ultimately
show ?case
unfolding af_subsequence_U semantics_ltln.simps GF_advice.simps by blast
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n ((af φ (w [i → n]))[X]⇩ν)"
assumes "⋀j. j ≤ i ⟹ suffix n w ⊨⇩n ((af ψ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ M⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
then have A: "suffix n w ⊨⇩n ((af ψ (w [0 → n]))[X]⇩ν)"
by blast
have "suffix (Suc n) w ⊨⇩n (af ψ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF A, of 1] by simp
moreover
have "suffix (Suc n) w ⊨⇩n (af φ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto
ultimately
show ?case
unfolding af_subsequence_M GF_advice.simps semantics_ltln.simps by blast
next
case (Suc i)
have "suffix 1 (suffix n w) ⊨⇩n af (af ψ (prefix n w)) [suffix n w 0][X]⇩ν"
by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
then have "suffix (Suc n) w ⊨⇩n (af ψ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
moreover
have B: "(Suc (n - 1)) = n"
using Suc by simp
note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
then have "suffix (Suc n) w ⊨⇩n (af (φ M⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
ultimately
show ?case
unfolding af_subsequence_M semantics_ltln.simps GF_advice.simps by blast
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n ((af φ (w [i → n]))[X]⇩ν)"
assumes "⋀j. j ≤ i ⟹ suffix n w ⊨⇩n ((af ψ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ R⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
then have A: "suffix n w ⊨⇩n ((af ψ (w [0 → n]))[X]⇩ν)"
by blast
have "suffix (Suc n) w ⊨⇩n (af ψ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF A, of 1] by simp
moreover
have "suffix (Suc n) w ⊨⇩n (af φ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by auto
ultimately
show ?case
unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast
next
case (Suc i)
have "suffix 1 (suffix n w) ⊨⇩n af (af ψ (prefix n w)) [suffix n w 0][X]⇩ν"
by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
then have "suffix (Suc n) w ⊨⇩n (af ψ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
moreover
have B: "(Suc (n - 1)) = n"
using Suc by simp
note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
then have "suffix (Suc n) w ⊨⇩n (af (φ R⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
ultimately
show ?case
unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n ((af ψ (w [i → n]))[X]⇩ν)"
assumes "⋀j. j < i ⟹ suffix n w ⊨⇩n ((af φ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ W⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
then have A: "suffix n w ⊨⇩n ((af ψ (w [0 → n]))[X]⇩ν)"
by blast
have "suffix (Suc n) w ⊨⇩n (af ψ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF A, of 1] by simp
then show ?case
unfolding af_subsequence_W GF_advice.simps semantics_ltln.simps by blast
next
case (Suc i)
have "suffix (Suc n) w ⊨⇩n (af φ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1]
by simp
moreover
have B: "(Suc (n - 1)) = n"
using Suc by simp
note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
then have "suffix (Suc n) w ⊨⇩n (af (φ W⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
ultimately
show ?case
unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n af (φ R⇩n ψ) (w [i → n])[X]⇩ν"
assumes "⋀j. j ≤ i ⟹ suffix n w ⊨⇩n ((af ψ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ R⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
then have A: "suffix n w ⊨⇩n ((af ψ (w [0 → n]))[X]⇩ν)"
by blast
have "suffix (Suc n) w ⊨⇩n (af ψ (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF A, of 1] by simp
moreover
have "suffix (Suc n) w ⊨⇩n (af (φ R⇩n ψ) (w [0 → Suc n]))[X]⇩ν"
using GF_advice_af_2[OF "0.prems"(2), of 1, unfolded suffix_suffix] by simp
ultimately
show ?case
unfolding af_subsequence_R GF_advice.simps semantics_ltln.simps by blast
next
case (Suc i)
have "suffix 1 (suffix n w) ⊨⇩n af (af ψ (prefix n w)) [suffix n w 0][X]⇩ν"
by (metis (no_types) GF_advice_af_2 Suc.prems(3) plus_1_eq_Suc subsequence_singleton suffix_0 suffix_suffix zero_le)
then have "suffix (Suc n) w ⊨⇩n (af ψ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
moreover
have B: "(Suc (n - 1)) = n"
using Suc by simp
note Suc.IH[of _ "suffix 1 w", unfolded subsequence_shift suffix_suffix]
then have "suffix (Suc n) w ⊨⇩n (af (φ R⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono plus_1_eq_Suc Suc.prems)
ultimately
show ?case
unfolding af_subsequence_R semantics_ltln.simps GF_advice.simps by blast
qed

assumes "i ≤ n"
assumes "suffix n w ⊨⇩n af (φ W⇩n ψ) (w [i → n])[X]⇩ν"
assumes "⋀j. j < i ⟹ suffix n w ⊨⇩n ((af φ (w [j → n]))[X]⇩ν)"
shows "suffix (Suc n) w ⊨⇩n (af (φ W⇩n ψ) (prefix (Suc n) w))[X]⇩ν"
using assms
proof (induction i arbitrary: w n)
case 0
have "suffix (Suc n) w ⊨⇩n af_letter (af (φ W⇩n ψ) (prefix n w)) (w n)[X]⇩ν"
moreover
have "prefix (Suc n) w = prefix n w @ [w n]"
using subseq_to_Suc by blast
ultimately show ?case
by (metis (no_types) foldl.simps(1) foldl.simps(2) foldl_append)
next
case (Suc i)
have "suffix (Suc n) w ⊨⇩n (af φ (prefix (Suc n) w))[X]⇩ν"
using Suc.prems(3)[OF zero_less_Suc, THEN GF_advice_af_2, unfolded suffix_suffix, of 1] by simp
moreover
have "n > 0" and B: "(Suc (n - 1)) = n"
using Suc by simp+
note Suc.IH[of "n - 1" "suffix 1 w", unfolded suffix_suffix] Suc.prems
then have "suffix (Suc n) w ⊨⇩n (af (φ W⇩n ψ) (w [1 → (Suc n)]))[X]⇩ν"
by (metis B One_nat_def Suc_le_mono Suc_mono plus_1_eq_Suc subsequence_shift)
ultimately
show ?case
unfolding af_subsequence_W unfolding semantics_ltln.simps GF_advice.simps by simp
qed

subsection ‹Advice Functions and Propositional Entailment›

"𝒜 ⊨⇩P φ[X]⇩ν ⟹ {ψ. ψ[X]⇩ν ∈ 𝒜} ⊨⇩P φ"
"false⇩n ∉ 𝒜 ⟹ {ψ. ψ[X]⇩ν ∈ 𝒜} ⊨⇩P φ ⟹ 𝒜 ⊨⇩P φ[X]⇩ν"
by (induction φ) (auto, meson, meson)

"false⇩n ∉ 𝒜 ⟹ 𝒜 ⊨⇩P φ[X]⇩ν ⟷ {ψ. ψ[X]⇩ν ∈ 𝒜} ⊨⇩P φ"

"true⇩n ∈ 𝒜 ⟹ 𝒜 ⊨⇩P φ[Y]⇩μ ⟹ {ψ. ψ[Y]⇩μ ∈ 𝒜} ⊨⇩P φ"
"{ψ. ψ[Y]⇩μ ∈ 𝒜} ⊨⇩P φ ⟹ 𝒜 ⊨⇩P φ[Y]⇩μ"
by (induction φ) auto

"true⇩n ∈ 𝒜 ⟹ 𝒜 ⊨⇩P φ[X]⇩μ ⟷ {ψ. ψ[X]⇩μ ∈ 𝒜} ⊨⇩P φ"

"φ[X]⇩ν = subst φ (λψ. Some (ψ[X]⇩ν))"
by (induction φ) auto

"φ[X]⇩μ = subst φ (λψ. Some (ψ[X]⇩μ))"
by (induction φ) auto

"φ ⟶⇩P ψ ⟹ φ[X]⇩ν ⟶⇩P ψ[X]⇩ν"
"φ ∼⇩P ψ ⟹ φ[X]⇩ν ∼⇩P ψ[X]⇩ν"

"φ ⟶⇩P ψ ⟹ φ[X]⇩μ ⟶⇩P ψ[X]⇩μ"
"φ ∼⇩P ψ ⟹ φ[X]⇩μ ∼⇩P ψ[X]⇩μ"

fixes
normalise :: "'a ltln ⇒ 'a ltln"
assumes
normalise_eq: "φ ∼ normalise φ"
assumes
normalise_monotonic: "w ⊨⇩n φ[X]⇩ν ⟹ w ⊨⇩n (normalise φ)[X]⇩ν"
assumes
normalise_eventually_equivalent:
"w ⊨⇩n (normalise φ)[X]⇩ν ⟹ (∃i. suffix i w ⊨⇩n (af φ (prefix i w))[X]⇩ν)"
assumes
GF_advice_congruent: "φ ∼ ψ ⟹ (normalise φ)[X]⇩ν ∼ (normalise ψ)[X]⇩ν"
begin

lemma normalise_language_equivalent[simp]:
"w ⊨⇩n normalise φ ⟷ w ⊨⇩n φ"
using normalise_eq ltl_lang_equiv_def eq_implies_lang by blast

end