Theory LTL_Master_Theorem.Advice

(*
    Author:   Benedikt Seidl
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹Advice functions›

theory Advice
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
  "(Xn ψ)[X]ν = Xn (ψ[X]ν)"
| "(ψ1 andn ψ2)[X]ν = (ψ1[X]ν) andn (ψ2[X]ν)"
| "(ψ1 orn ψ2)[X]ν = (ψ1[X]ν) orn (ψ2[X]ν)"
| "(ψ1 Wn ψ2)[X]ν = (ψ1[X]ν) Wn (ψ2[X]ν)"
| "(ψ1 Rn ψ2)[X]ν = (ψ1[X]ν) Rn (ψ2[X]ν)"
| "(ψ1 Un ψ2)[X]ν = (if (ψ1 Un ψ2) ∈ X then (ψ1[X]ν) Wn (ψ2[X]ν) else falsen)"
| "(ψ1 Mn ψ2)[X]ν = (if (ψ1 Mn ψ2) ∈ X then (ψ1[X]ν) Rn (ψ2[X]ν) else falsen)"
| "φ[_]ν = φ"

fun FG_advice :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln" ("_[_]μ" [90,60] 89)
where
  "(Xn ψ)[Y]μ = Xn (ψ[Y]μ)"
| "(ψ1 andn ψ2)[Y]μ = (ψ1[Y]μ) andn (ψ2[Y]μ)"
| "(ψ1 orn ψ2)[Y]μ = (ψ1[Y]μ) orn (ψ2[Y]μ)"
| "(ψ1 Un ψ2)[Y]μ = (ψ1[Y]μ) Un (ψ2[Y]μ)"
| "(ψ1 Mn ψ2)[Y]μ = (ψ1[Y]μ) Mn (ψ2[Y]μ)"
| "(ψ1 Wn ψ2)[Y]μ = (if (ψ1 Wn ψ2) ∈ Y then truen else (ψ1[Y]μ) Un (ψ2[Y]μ))"
| "(ψ1 Rn ψ2)[Y]μ = (if (ψ1 Rn ψ2) ∈ Y then truen else (ψ1[Y]μ) Mn (ψ2[Y]μ))"
| "φ[_]μ = φ"

lemma GF_advice_νLTL:
  "φ[X]ν ∈ νLTL"
  "φ ∈ νLTL ⟹ φ[X]ν = φ"
  by (induction φ) auto

lemma FG_advice_μLTL:
  "φ[X]μ ∈ μLTL"
  "φ ∈ μLTL ⟹ φ[X]μ = φ"
  by (induction φ) auto


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

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

lemma GF_advice_subfrmlsn_card:
  "card (subfrmlsn (φ[X]ν)) ≤ card (subfrmlsn φ)"
proof -
  have "card (subfrmlsn (φ[X]ν)) ≤ card {ψ[X]ν | ψ. ψ ∈ subfrmlsn φ}"
    by (simp add: subfrmlsn_finite GF_advice_subfrmlsn card_mono)

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

  finally show ?thesis .
qed

lemma FG_advice_subfrmlsn_card:
  "card (subfrmlsn (φ[Y]μ)) ≤ card (subfrmlsn φ)"
proof -
  have "card (subfrmlsn (φ[Y]μ)) ≤ card {ψ[Y]μ | ψ. ψ ∈ subfrmlsn φ}"
    by (simp add: subfrmlsn_finite FG_advice_subfrmlsn card_mono)

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

  finally show ?thesis .
qed

lemma GF_advice_monotone:
  "X ⊆ Y ⟹ w ⊨n φ[X]ν ⟹ w ⊨n φ[Y]ν"
proof (induction φ arbitrary: w)
  case (Until_ltln φ ψ)
  then show ?case
    by (cases "φ Un ψ ∈ 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 "φ Mn ψ ∈ X") (simp_all, blast)
qed auto

lemma FG_advice_monotone:
  "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 "φ Rn ψ ∈ X") (auto, blast)
next
  case (WeakUntil_ltln φ ψ)
  then show ?case
    by (cases "φ Wn ψ ∈ X") (auto, blast)
next
  case (StrongRelease_ltln φ ψ)
  then show ?case by (simp, blast)
qed auto

lemma GF_advice_ite_simps[simp]:
  "(if P then truen else falsen)[X]ν = (if P then truen else falsen)"
  "(if P then falsen else truen)[X]ν = (if P then falsen else truen)"
  by simp_all

lemma FG_advice_ite_simps[simp]:
  "(if P then truen else falsen)[Y]μ = (if P then truen else falsen)"
  "(if P then falsen else truen)[Y]μ = (if P then falsen else truen)"
  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)"
  by (simp add: nested_prop_atomsν_def nested_prop_atoms_finite)

lemma nested_prop_atomsμ_finite:
  "finite (nested_prop_atomsμ φ X)"
  by (simp add: nested_prop_atomsμ_def 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)

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 GF_advice_nested_prop_atomsν:
  "nested_prop_atoms (φ[X]ν) ⊆ nested_prop_atomsν φ X"
  by (induction φ) (unfold nested_prop_atomsν_def, force+)

lemma FG_advice_nested_prop_atomsμ:
  "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

lemma GF_advice_nested_prop_atoms_card:
  "card (nested_prop_atoms (φ[X]ν)) ≤ card (nested_prop_atoms φ)"
proof -
  have "card (nested_prop_atoms (φ[X]ν)) ≤ card (nested_prop_atomsν φ X)"
    by (simp add: nested_prop_atomsν_finite GF_advice_nested_prop_atomsν card_mono)

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

lemma FG_advice_nested_prop_atoms_card:
  "card (nested_prop_atoms (φ[Y]μ)) ≤ card (nested_prop_atoms φ)"
proof -
  have "card (nested_prop_atoms (φ[Y]μ)) ≤ card (nested_prop_atomsμ φ Y)"
    by (simp add: nested_prop_atomsμ_finite FG_advice_nested_prop_atomsμ card_mono)

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



subsection ‹Intersecting the Advice Set›

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

lemma GF_advice_inter_subformulas:
  "φ[X ∩ subformulasμ φ]ν = φ[X]ν"
  using GF_advice_inter by blast

lemma GF_advice_minus_subformulas:
  "ψ ∉ 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

lemma GF_advice_minus_size:
  "⟦size φ ≤ size ψ; φ ≠ ψ⟧ ⟹ φ[X - {ψ}]ν = φ[X]ν"
  using subfrmlsn_size subformulasμ_subfrmlsn GF_advice_minus_subformulas
  by fastforce


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

lemma FG_advice_inter_subformulas:
  "φ[Y ∩ subformulasν φ]μ = φ[Y]μ"
  using FG_advice_inter by blast

lemma FG_advice_minus_subformulas:
  "ψ ∉ 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

lemma FG_advice_minus_size:
  "⟦size φ ≤ size ψ; φ ≠ ψ⟧ ⟹ φ[Y - {ψ}]μ = φ[Y]μ"
  using subfrmlsn_size subformulasν_subfrmlsn FG_advice_minus_subformulas
  by fastforce

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



subsection ‹Correctness GF-advice function›

lemma GF_advice_a1:
  "⟦ℱ φ 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 Wn φ2) w ⊆ ℱ (φ1 Un φ2) w"
    by fastforce
  then have "ℱ (φ1 Wn φ2) w ⊆ X" and "w ⊨n φ1 Wn φ2"
    using Until_ltln.prems ltln_strong_to_weak by blast+
  then have "w ⊨n φ1[X]ν Wn φ2[X]ν"
    using Until_ltln.IH
    by simp (meson ℱ_suffix subset_trans sup.boundedE)

  moreover

  have "w ⊨n φ1 Un φ2"
    using Until_ltln.prems by simp
  then have "φ1 Un φ2 ∈ ℱ (φ1 Un φ2) w"
    by force
  then have "φ1 Un φ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 Rn φ2) w ⊆ ℱ (φ1 Mn φ2) w"
    by fastforce
  then have "ℱ (φ1 Rn φ2) w ⊆ X" and "w ⊨n φ1 Rn φ2"
    using StrongRelease_ltln.prems ltln_strong_to_weak by blast+
  then have "w ⊨n φ1[X]ν Rn φ2[X]ν"
    using StrongRelease_ltln.IH
    by simp (meson ℱ_suffix subset_trans sup.boundedE)

  moreover

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

  ultimately show ?case
    by auto
qed auto

lemma GF_advice_a2_helper:
  "⟦∀ψ ∈ X. w ⊨n Gn (Fn ψ); w ⊨n φ[X]ν⟧ ⟹ w ⊨n φ"
proof (induction φ arbitrary: w)
  case (Next_ltln φ)
  then show ?case
    unfolding GF_advice.simps semantics_ltln.simps(7)
    using GF_suffix by blast
next
  case (Until_ltln φ1 φ2)

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

  moreover

  have "w ⊨n (φ1 Un φ2)[X]ν"
    using Until_ltln.prems by simp
  then have "w ⊨n (φ1[X]ν) Wn (φ2[X]ν)"
    unfolding GF_advice.simps using ‹φ1 Un φ2 ∈ X› by simp
  then have "w ⊨n φ1 Wn φ2"
    unfolding GF_advice.simps semantics_ltln.simps(10)
    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
    unfolding GF_advice.simps semantics_ltln.simps(9)
    by (metis GF_suffix Release_ltln.IH Release_ltln.prems(1))
next
  case (WeakUntil_ltln φ1 φ2)
  then show ?case
    unfolding GF_advice.simps semantics_ltln.simps(10)
    by (metis GF_suffix)
next
  case (StrongRelease_ltln φ1 φ2)

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

  moreover

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

  ultimately show ?case
    using ltln_weak_to_strong by blast
qed auto

lemma GF_advice_a2:
  "⟦X ⊆ 𝒢ℱ φ w; w ⊨n φ[X]ν⟧ ⟹ w ⊨n φ"
  by (metis GF_advice_a2_helper 𝒢ℱ_elim subset_eq)

lemma GF_advice_a3:
  "⟦X = ℱ φ w; X = 𝒢ℱ φ w⟧ ⟹ w ⊨n φ ⟷ w ⊨n φ[X]ν"
  using GF_advice_a1 GF_advice_a2 by fastforce



subsection ‹Correctness FG-advice function›

lemma FG_advice_b1:
  "⟦ℱ𝒢 φ 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 Rn φ2 ∈ Y")
    case False
    then have "φ1 Rn φ2 ∉ ℱ𝒢 (φ1 Rn φ2) w"
      using Release_ltln.prems by blast
    then have "¬ w ⊨n Gn φ2"
      by fastforce
    then have "w ⊨n φ1 Mn φ2"
      using Release_ltln.prems ltln_weak_to_strong by blast

    moreover

    have "ℱ𝒢 (φ1 Mn φ2) w ⊆ ℱ𝒢 (φ1 Rn φ2) w"
      by fastforce
    then have "ℱ𝒢 (φ1 Mn φ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 Wn φ2 ∈ Y")
    case False
    then have "φ1 Wn φ2 ∉ ℱ𝒢 (φ1 Wn φ2) w"
      using WeakUntil_ltln.prems by blast
    then have "¬ w ⊨n Gn φ1"
      by fastforce
    then have "w ⊨n φ1 Un φ2"
      using WeakUntil_ltln.prems ltln_weak_to_strong by blast

    moreover

    have "ℱ𝒢 (φ1 Un φ2) w ⊆ ℱ𝒢 (φ1 Wn φ2) w"
      by fastforce
    then have "ℱ𝒢 (φ1 Un φ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

lemma FG_advice_b2_helper:
  "⟦∀ψ ∈ Y. w ⊨n Gn ψ; 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 Rn φ2 ∈ Y")
    case True
    then show ?thesis
      using Release_ltln.prems by force
  next
    case False
    then have "w ⊨n (φ1[Y]μ) Mn (φ2[Y]μ)"
      using Release_ltln.prems by simp
    then have "w ⊨n φ1 Mn φ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 Wn φ2 ∈ Y")
    case True
    then show ?thesis
      using WeakUntil_ltln.prems by force
  next
    case False
    then have "w ⊨n (φ1[Y]μ) Un (φ2[Y]μ)"
      using WeakUntil_ltln.prems by simp
    then have "w ⊨n φ1 Un φ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

lemma FG_advice_b2:
  "⟦Y ⊆ 𝒢 φ w; w ⊨n φ[Y]μ⟧ ⟹ w ⊨n φ"
  by (metis FG_advice_b2_helper 𝒢_elim subset_eq)

lemma FG_advice_b3:
  "⟦Y = ℱ𝒢 φ w; Y = 𝒢 φ w⟧ ⟹ w ⊨n φ ⟷ w ⊨n φ[Y]μ"
  using FG_advice_b1 FG_advice_b2 by fastforce



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

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

  then have "w ⊨n af_letter ((φ1 Un φ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 Rn φ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 Wn φ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 Mn φ2)[X]ν) x"
    using af_letter_build by blast

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

lemma FG_advice_af_letter:
  "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
    unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
    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 Rn φ2 ∈ Y")
    apply simp
    unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
    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 Wn φ2 ∈ Y")
    apply simp
    unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
    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
    unfolding af_letter.simps FG_advice.simps semantics_ltln.simps(5,6)
    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

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

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

lemma GF_advice_af_2:
  "w ⊨n φ[X]ν ⟹ suffix i w ⊨n (af φ (prefix i w))[X]ν"
  using GF_advice_af by force

lemma FG_advice_af_2:
  "suffix i w ⊨n (af φ (prefix i w))[X]μ ⟹ w ⊨n φ[X]μ"
  using FG_advice_af by force

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

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

lemma GF_advice_sync:
  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]ν"
    using le_add1 Suc.prems by blast

  define k where "k ≡ k1 + k2"

  have "⋀i. i < Suc n ⟹ k ≥ index i"
    unfolding k_def by (metis leq1 leq2 less_SucE trans_le_add1 trans_le_add2)

  moreover

  {
    have "⋀i. i < n ⟹ suffix k w ⊨n af (formula i) (w [(index i) → k])[X]ν"
      unfolding k_def
      by (metis GF_advice_af_2[OF suffix1, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq1 add.commute le_add1)

    moreover

    have "suffix k w ⊨n af (formula n) (w [index n → k])[X]ν"
      unfolding k_def
      by (metis GF_advice_af_2[OF suffix2, unfolded suffix_suffix prefix_suffix_subsequence] af_subsequence_append leq2 add.commute le_add1)

    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

lemma GF_advice_sync_and:
  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

lemma GF_advice_sync_less:
  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

lemma GF_advice_sync_lesseq:
  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
        by (simp add: min_def add.commute)
    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

lemma af_subsequence_U_GF_advice:
  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 (φ Un ψ) (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 (φ Un ψ) (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

lemma af_subsequence_M_GF_advice:
  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 (φ Mn ψ) (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 (φ Mn ψ) (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

lemma af_subsequence_R_GF_advice:
  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 (φ Rn ψ) (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 (φ Rn ψ) (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

lemma af_subsequence_W_GF_advice:
  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 (φ Wn ψ) (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 (φ Wn ψ) (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

lemma af_subsequence_R_GF_advice_connect:
  assumes "i ≤ n"
  assumes "suffix n w ⊨n af (φ Rn ψ) (w [i → n])[X]ν"
  assumes "⋀j. j ≤ i ⟹ suffix n w ⊨n ((af ψ (w [j → n]))[X]ν)"
  shows "suffix (Suc n) w ⊨n (af (φ Rn ψ) (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 (φ Rn ψ) (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 (φ Rn ψ) (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

lemma af_subsequence_W_GF_advice_connect:
  assumes "i ≤ n"
  assumes "suffix n w ⊨n af (φ Wn ψ) (w [i → n])[X]ν"
  assumes "⋀j. j < i ⟹ suffix n w ⊨n ((af φ (w [j → n]))[X]ν)"
  shows "suffix (Suc n) w ⊨n (af (φ Wn ψ) (prefix (Suc n) w))[X]ν"
  using assms
proof (induction i arbitrary: w n)
  case 0
  have "suffix (Suc n) w ⊨n af_letter (af (φ Wn ψ) (prefix n w)) (w n)[X]ν"
    by (simp add: "0.prems"(2) GF_advice_af_letter)
  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 (φ Wn ψ) (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›

lemma GF_advice_prop_entailment:
  "𝒜 ⊨P φ[X]ν ⟹ {ψ. ψ[X]ν ∈ 𝒜} ⊨P φ"
  "falsen ∉ 𝒜 ⟹ {ψ. ψ[X]ν ∈ 𝒜} ⊨P φ ⟹ 𝒜 ⊨P φ[X]ν"
  by (induction φ) (auto, meson, meson)

lemma GF_advice_iff_prop_entailment:
  "falsen ∉ 𝒜 ⟹ 𝒜 ⊨P φ[X]ν ⟷ {ψ. ψ[X]ν ∈ 𝒜} ⊨P φ"
  by (metis GF_advice_prop_entailment)

lemma FG_advice_prop_entailment:
  "truen ∈ 𝒜 ⟹ 𝒜 ⊨P φ[Y]μ ⟹ {ψ. ψ[Y]μ ∈ 𝒜} ⊨P φ"
  "{ψ. ψ[Y]μ ∈ 𝒜} ⊨P φ ⟹ 𝒜 ⊨P φ[Y]μ"
  by (induction φ) auto

lemma FG_advice_iff_prop_entailment:
  "truen ∈ 𝒜 ⟹ 𝒜 ⊨P φ[X]μ ⟷ {ψ. ψ[X]μ ∈ 𝒜} ⊨P φ"
  by (metis FG_advice_prop_entailment)

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

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

lemma GF_advice_prop_congruent:
  "φ ⟶P ψ ⟹ φ[X]ν ⟶P ψ[X]ν"
  "φ ∼P ψ ⟹ φ[X]ν ∼P ψ[X]ν"
  by (metis GF_advice_subst subst_respects_ltl_prop_entailment)+

lemma FG_advice_prop_congruent:
  "φ ⟶P ψ ⟹ φ[X]μ ⟶P ψ[X]μ"
  "φ ∼P ψ ⟹ φ[X]μ ∼P ψ[X]μ"
  by (metis FG_advice_subst subst_respects_ltl_prop_entailment)+


subsection ‹GF-advice with Equivalence Relations›

locale GF_advice_congruent = ltl_equivalence +
  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

interpretation prop_GF_advice_compatible: GF_advice_congruent "(∼P)" "id"
  by unfold_locales (simp add: GF_advice_af GF_advice_prop_congruent(2))+

end