Theory LTL_Master_Theorem.After

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

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 truen ν = truen"
| "af_letter falsen ν = falsen"
| "af_letter propn(a) ν = (if a ∈ ν then truen else falsen)"
| "af_letter npropn(a) ν  = (if a ∉ ν then truen else falsen)"
| "af_letter (φ andn ψ) ν = (af_letter φ ν) andn (af_letter ψ ν)"
| "af_letter (φ orn ψ) ν = (af_letter φ ν) orn (af_letter ψ ν)"
| "af_letter (Xn φ) ν = φ"
| "af_letter (φ Un ψ) ν = (af_letter ψ ν) orn ((af_letter φ ν) andn (φ Un ψ))"
| "af_letter (φ Rn ψ) ν = (af_letter ψ ν) andn ((af_letter φ ν) orn (φ Rn ψ))"
| "af_letter (φ Wn ψ) ν = (af_letter ψ ν) orn ((af_letter φ ν) andn (φ Wn ψ))"
| "af_letter (φ Mn ψ) ν = (af_letter ψ ν) andn ((af_letter φ ν) orn (φ Mn ψ))"

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


lemma af_decompose:
  "af (φ andn ψ) w = (af φ w) andn (af ψ w)"
  "af (φ orn ψ) w = (af φ w) orn (af ψ w)"
  by (induction w rule: rev_induct) simp_all

lemma af_simps[simp]:
  "af truen w = truen"
  "af falsen w = falsen"
  "af (Xn φ) (x # xs) = af φ xs"
  by (induction w) simp_all

lemma af_ite_simps[simp]:
  "af (if P then truen else falsen) w = (if P then truen else falsen)"
  "af (if P then falsen else truen) w = (if P then falsen else truen)"
  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 (φ Un ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) orn ((af φ (w [0 → Suc n])) andn af (φ Un ψ) (w [1 → Suc n]))"
  by (induction n) fastforce+

lemma af_subsequence_U':
  "af (φ Un ψ) (a # xs) = (af ψ (a # xs)) orn ((af φ (a # xs)) andn af (φ Un ψ) xs)"
  by (simp add: af_decompose)

lemma af_subsequence_R:
  "af (φ Rn ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) andn ((af φ (w [0 → Suc n])) orn af (φ Rn ψ) (w [1 → Suc n]))"
  by (induction n) fastforce+

lemma af_subsequence_R':
  "af (φ Rn ψ) (a # xs) = (af ψ (a # xs)) andn ((af φ (a # xs)) orn af (φ Rn ψ) xs)"
  by (simp add: af_decompose)

lemma af_subsequence_W:
  "af (φ Wn ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) orn ((af φ (w [0 → Suc n])) andn af (φ Wn ψ) (w [1 → Suc n]))"
  by (induction n) fastforce+

lemma af_subsequence_W':
  "af (φ Wn ψ) (a # xs) = (af ψ (a # xs)) orn ((af φ (a # xs)) andn af (φ Wn ψ) xs)"
  by (simp add: af_decompose)

lemma af_subsequence_M:
  "af (φ Mn ψ) (w [0 → Suc n]) = (af ψ (w [0 → Suc n])) andn ((af φ (w [0 → Suc n])) orn af (φ Mn ψ) (w [1 → Suc n]))"
  by (induction n) fastforce+

lemma af_subsequence_M':
  "af (φ Mn ψ) (a # xs) = (af ψ (a # xs)) andn ((af φ (a # xs)) orn af (φ Mn ψ) xs)"
  by (simp add: af_decompose)

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 (Fn φ) w ⟶P af (Fn φ) (w' @ w)"
  by (induction w') (simp add: ltl_prop_implies_def af_decompose(1,2))+

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


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

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


lemma af_F_prefix_const_equiv_true:
  "af (Fn φ) w ∼C truen ⟹ af (Fn φ) (w' @ w) ∼C truen"
  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 (Gn φ) w ∼C falsen ⟹ af (Gn φ) (w' @ w) ∼C falsen"
  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 (Fn φ) w ∼L truen ⟹ af (Fn φ) (w' @ w) ∼L truen"
  unfolding ltl_lang_equiv_def
  using af_F_prefix_lang by fastforce

lemma af_G_prefix_lang_equiv_false:
  "af (Gn φ) w ∼L falsen ⟹ af (Gn φ) (w' @ w) ∼L falsen"
  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')"
  by (simp add: af_congruentness)

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

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

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

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) ∼ truen ⟹ af φ (prefix j w) ∼ truen"
  by (metis af_append_true prefix_append_subsequence)

lemma af_prefix_false:
  "i ≤ j ⟹ af φ (prefix i w) ∼ falsen ⟹ af φ (prefix j w) ∼ falsen"
  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 truen ⟹ w ⊨n φ"
proof -
  assume "af φ (prefix i w) ∼L truen"

  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 falsen)"
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 falsen)"
    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 truen"
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 truen" and "af φ2 (prefix i2 w) ∼C truen"
    by fastforce

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

  then have "af (φ1 andn φ2) (prefix (i1 + i2) w) ∼C truen"
    unfolding af_decompose by (simp add: add.commute)

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

  then obtain i where "af φ1 (prefix i w) ∼C truen ∨ af φ2 (prefix i w) ∼C truen"
    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 truen"
    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 truen"
      using Until_ltln by fastforce

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

    then have "af (φ1 Un φ2) (prefix (Suc i) w) ∼C truen"
      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"
      by (simp add: Suc.prems)+

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

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

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

    moreover

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

    ultimately

    have "af (φ1 Un φ2) (prefix (Suc (j + i)) w) ∼C truen"
      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 truen" and "af φ2 (prefix i2 w) ∼C truen"
      using StrongRelease_ltln by fastforce

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

    then have "af (φ1 Mn φ2) (prefix (Suc (i1 + i2)) w) ∼C truen"
      unfolding af_subsequence_M by (simp add: add.commute)

    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"
      by (simp add: Suc.prems)+

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

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

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

    moreover

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

    ultimately

    have "af (φ1 Mn φ2) (prefix (Suc (j + i)) w) ∼C truen"
      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 falsen ⟹ 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 falsen ∨ af φ2 (prefix i w) ∼C falsen"
    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 falsen" and "af φ2 (prefix i2 w) ∼C falsen"
    by fastforce

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

  then have "af (φ1 orn φ2) (prefix (i1 + i2) w) ∼C falsen"
    unfolding af_decompose by (simp add: add.commute)

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

  then obtain i where "af φ (prefix i (suffix 1 w)) ∼C falsen"
    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 falsen"
      using Release_ltln by fastforce

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

    then have "af (φ1 Rn φ2) (prefix (Suc i) w) ∼C falsen"
      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"
      by (simp add: Suc.prems)+

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

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

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

    moreover

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

    ultimately

    have "af (φ1 Rn φ2) (prefix (Suc (j + i)) w) ∼C falsen"
      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 falsen" and "af φ2 (prefix i2 w) ∼C falsen"
      using WeakUntil_ltln by fastforce

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

    then have "af (φ1 Wn φ2) (prefix (Suc (i1 + i2)) w) ∼C falsen"
      unfolding af_subsequence_W by (simp add: add.commute)

    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"
      by (simp add: Suc.prems)+

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

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

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

    moreover

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

    ultimately

    have "af (φ1 Wn φ2) (prefix (Suc (j + i)) w) ∼C falsen"
      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) ∼ truen ⟹ w ⊨n φ"
  using valid_prefix_implies_ltl eq_implies_lang by blast

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


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

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


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

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


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

  then have "Fn φ ∈ μLTL"
    by simp

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

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

  then have "Gn φ ∈ νLTL"
    by simp

  have "w ⊨n Fn (Gn φ) ⟷ (∃i. suffix i w ⊨n Gn φ)"
    by force
  also have "… ⟷ (∃i. ∀j. ¬ (af (Gn φ) (prefix j (suffix i w)) ∼ falsen))"
    using af_νLTL[OF ‹Gn φ ∈ νLTL›] by blast
  also have "… ⟷ (∃i. ∀j. ¬ (af (Gn φ) (prefix (j - i) (suffix i w)) ∼ falsen))"
    by (metis diff_add_inverse)
  also have "… ⟷ (∃i. ∀j. ¬ (af (Gn φ) (w[i → j]) ∼ falsen))"
    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