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 "jk. 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 "jk. 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 "jk. ¬ 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 "jk. ¬ 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