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