Theory Transition_Functions

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Transition Functions for Deterministic Automata›

theory Transition_Functions
imports
  "../Logical_Characterization/After"
  "../Logical_Characterization/Advice"
begin

text ‹
  This theory defines three functions based on the ``after''-function
  which we use as transition functions for deterministic automata.
›

locale transition_functions =
  af_congruent + GF_advice_congruent
begin

subsection ‹After Functions with Resets for @{term "GF(μLTL)"} and @{term "FG(νLTL)"}›

definition af_letterF :: "'a ltln ⇒ 'a ltln ⇒ 'a set ⇒ 'a ltln"
where
  "af_letterF φ ψ ν = (if ψ ∼ truen then Fn φ else af_letter ψ ν)"

definition af_letterG :: "'a ltln ⇒ 'a ltln ⇒ 'a set ⇒ 'a ltln"
where
  "af_letterG φ ψ ν = (if ψ ∼ falsen then Gn φ else af_letter ψ ν)"

abbreviation afF :: "'a ltln ⇒ 'a ltln ⇒ 'a set list ⇒ 'a ltln"
where
  "afF φ ψ w ≡ foldl (af_letterF φ) ψ w"

abbreviation afG :: "'a ltln ⇒ 'a ltln ⇒ 'a set list ⇒ 'a ltln"
where
  "afG φ ψ w ≡ foldl (af_letterG φ) ψ w"


lemma afF_step:
  "afF φ ψ w ∼ truen ⟹ afF φ ψ (w @ [ν]) = Fn φ"
  by (induction w rule: rev_induct) (auto simp: af_letterF_def)

lemma afG_step:
  "afG φ ψ w ∼ falsen ⟹ afG φ ψ (w @ [ν]) = Gn φ"
  by (induction w rule: rev_induct) (auto simp: af_letterG_def)

lemma afF_segments:
  "afF φ ψ w = Fn φ ⟹ afF φ ψ (w @ w') = afF φ (Fn φ) w'"
  by simp

lemma afG_segments:
  "afG φ ψ w = Gn φ ⟹ afG φ ψ (w @ w') = afG φ (Gn φ) w'"
  by simp


lemma af_not_true_implies_af_equals_afF:
  "(⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ truen) ⟹ afF φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
  case (snoc x xs)

  then have "afF φ ψ xs = af ψ xs"
    by simp

  moreover

  have "¬ af ψ xs ∼ truen"
    using snoc.prems by blast

  ultimately show ?case
    by (metis af_letterF_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma af_not_false_implies_af_equals_afG:
  "(⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ falsen) ⟹ afG φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
  case (snoc x xs)

  then have "afG φ ψ xs = af ψ xs"
    by simp

  moreover

  have "¬ af ψ xs ∼ falsen"
    using snoc.prems by blast

  ultimately show ?case
    by (metis af_letterG_def foldl_Cons foldl_Nil foldl_append)
qed simp


lemma afF_not_true_implies_af_equals_afF:
  "(⋀xs ys. w = xs @ ys ⟹ ¬ afF φ ψ xs ∼ truen) ⟹ afF φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
  case (snoc x xs)

  then have "afF φ ψ xs = af ψ xs"
    by simp

  moreover

  have "¬ afF φ ψ xs ∼ truen"
    using snoc.prems by blast

  ultimately show ?case
    by (metis af_letterF_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma afG_not_false_implies_af_equals_afG:
  "(⋀xs ys. w = xs @ ys ⟹ ¬ afG φ ψ xs ∼ falsen) ⟹ afG φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
  case (snoc x xs)

  then have "afG φ ψ xs = af ψ xs"
    by simp

  moreover

  have "¬ afG φ ψ xs ∼ falsen"
    using snoc.prems by blast

  ultimately show ?case
    by (metis af_letterG_def foldl_Cons foldl_Nil foldl_append)
qed simp


lemma afF_true_implies_af_true:
  "afF φ ψ w ∼ truen ⟹ af ψ w ∼ truen"
  by (metis af_append_true af_not_true_implies_af_equals_afF)

lemma afG_false_implies_af_false:
  "afG φ ψ w ∼ falsen ⟹ af ψ w ∼ falsen"
  by (metis af_append_false af_not_false_implies_af_equals_afG)


lemma af_equiv_true_afF_prefix_true:
  "af ψ w ∼ truen ⟹ ∃xs ys. w = xs @ ys ∧ afF φ ψ xs ∼ truen"
proof (induction w rule: rev_induct)
  case (snoc a w)
  then show ?case
  proof (cases "af ψ w ∼ truen")
    case False

    then have "⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ truen"
      using af_append_true by blast

    then have "afF φ ψ w = af ψ w"
      using af_not_true_implies_af_equals_afF by auto

    then have "afF φ ψ (w @ [a]) = af ψ (w @ [a])"
      by (simp add: False af_letterF_def)

    then show ?thesis
      by (metis append_Nil2 snoc.prems)
  qed (insert snoc, force)
qed (simp add: const_implies_eq)

lemma af_equiv_false_afG_prefix_false:
  "af ψ w ∼ falsen ⟹ ∃xs ys. w = xs @ ys ∧ afG φ ψ xs ∼ falsen"
proof (induction w rule: rev_induct)
  case (snoc a w)
  then show ?case
  proof (cases "af ψ w ∼ falsen")
    case False

    then have "⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ falsen"
      using af_append_false by blast

    then have "afG φ ψ w = af ψ w"
      using af_not_false_implies_af_equals_afG by auto

    then have "afG φ ψ (w @ [a]) = af ψ (w @ [a])"
      by (simp add: False af_letterG_def)

    then show ?thesis
      by (metis append_Nil2 snoc.prems)
  qed (insert snoc, force)
qed (simp add: const_implies_eq)


lemma append_take_drop:
  "w = xs @ ys ⟷ xs = take (length xs) w ∧ ys = drop (length xs) w"
  by (metis append_eq_conv_conj)

lemma subsequence_split:
  "(w [i → j]) = xs @ ys ⟹ xs = (w [i → i + length xs])"
  by (simp add: append_take_drop) (metis add_diff_cancel_left' subsequence_length subsequence_prefix_suffix)

lemma subsequence_append_general:
  "i ≤ k ⟹ k ≤ j ⟹ (w [i → j]) = (w [i → k]) @ (w [k → j])"
  by (metis le_Suc_ex map_append subsequence_def upt_add_eq_append)


lemma afF_semantics_rtl:
  assumes
    "∀i. ∃j>i. afF φ (Fn φ) (w [0 → j]) ∼ truen"
  shows
    "∀i. ∃j. af (Fn φ) (w [i → j]) ∼L truen"
proof
  fix i
  from assms obtain j where "j > i" and "afF φ (Fn φ) (w [0 → j]) ∼ truen"
    by blast
  then have X: "afF φ (Fn φ) (w [0 → Suc j]) = Fn φ"
    using afF_step by auto

  obtain k where "k > j" and "afF φ (Fn φ) (w [0 → k]) ∼ truen"
    using assms using Suc_le_eq by blast
  then have "afF φ (Fn φ) (w [Suc j → k]) ∼ truen"
    using afF_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
  then have "af (Fn φ) (w [Suc j → k]) ∼ truen"
    using afF_true_implies_af_true by blast
  then show "∃k. af (Fn φ) (w [i → k]) ∼L truen"
    by (metis (full_types) af_F_prefix_lang_equiv_true eq_implies_lang subsequence_append_general Suc_le_eq ‹i < j› ‹j < k› less_SucI order.order_iff_strict)
qed

lemma afF_semantics_ltr:
  assumes
    "∀i. ∃j. af (Fn φ) (w [i → j]) ∼ truen"
  shows
    "∀i. ∃j>i. afF φ (Fn φ) (w [0 → j]) ∼ truen"
proof (rule ccontr)
  define resets where "resets = {i. afF φ (Fn φ) (w [0 → i]) ∼ truen}"
  define m where "m = (if resets = {} then 0 else Suc (Max resets))"

  assume "¬ (∀i. ∃j>i. afF φ (Fn φ) (w [0 → j]) ∼ truen)"

  then have "finite resets"
    using infinite_nat_iff_unbounded resets_def by force
  then have "resets ≠ {} ⟹ afF φ (Fn φ) (w [0 → Max resets]) ∼ truen"
    unfolding resets_def using Max_in by blast
  then have m_reset: "afF φ (Fn φ) (w [0 → m]) = Fn φ"
    unfolding m_def using afF_step by auto

  {
    fix i
    assume "i ≥ m"

    with m_reset have "¬ afF φ (Fn φ) (w [0 → i]) ∼ truen"
      by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq resets_def)
    with m_reset have "¬ afF φ  (Fn φ)(w [m → i]) ∼ truen"
      by (metis (mono_tags, opaque_lifting) ‹m ≤ i› afF_segments bot_nat_def le0 subsequence_append_general)
  }

  then have "∄j. afF φ (Fn φ) (w [m → j]) ∼ truen"
    by (metis le_cases subseq_to_smaller)
  then have "∄j. af (Fn φ) (w [m → j]) ∼ truen"
    by (metis af_equiv_true_afF_prefix_true subsequence_split)
  then show False
    using assms by blast
qed


lemma afG_semantics_rtl:
  assumes
    "∃i. ∀j>i. ¬ afG φ (Gn φ) (w [0 → j]) ∼ falsen"
  shows
    "∃i. ∀j. ¬ af (Gn φ) (w [i → j]) ∼ falsen"
proof
  define resets where "resets = {i. afG φ (Gn φ) (w [0 → i]) ∼ falsen}"
  define m where "m = (if resets = {} then 0 else Suc (Max resets))"

  from assms have "finite resets"
    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)
  then have "resets ≠ {} ⟹ afG φ (Gn φ) (w [0 → Max resets]) ∼ falsen"
    unfolding resets_def using Max_in by blast
  then have m_reset: "afG φ (Gn φ) (w [0 → m]) = Gn φ"
    unfolding m_def using afG_step by auto

  {
    fix i
    assume "i ≥ m"

    with m_reset have "¬ afG φ (Gn φ) (w [0 → i]) ∼ falsen"
      by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq resets_def)
    with m_reset have "¬ afG φ (Gn φ) (w [m → i]) ∼ falsen"
      by (metis (mono_tags, opaque_lifting) ‹m ≤ i› afG_segments bot_nat_def le0 subsequence_append_general)
  }

  then have "∀j. ¬ afG φ (Gn φ) (w [m → j]) ∼ falsen"
    by (metis le_cases subseq_to_smaller)
  then show "∀j. ¬ af (Gn φ) (w [m → j]) ∼ falsen"
    by (metis af_equiv_false_afG_prefix_false subsequence_split)
qed

lemma afG_semantics_ltr:
  assumes
    "∃i. ∀j. ¬ af (Gn φ) (w [i → j]) ∼L falsen"
  shows
    "∃i. ∀j>i. ¬ afG φ (Gn φ) (w [0 → j]) ∼ falsen"
proof (rule ccontr, auto)
  assume 1: "∀i. ∃j>i. afG φ (Gn φ) (w [0 → j]) ∼ falsen"

  {
    fix i
    obtain j where "j > i" and "afG φ (Gn φ) (w [0 → j]) ∼ falsen"
      using 1 by blast
    then have X: "afG φ (Gn φ) (w [0 → Suc j]) = Gn φ"
      using afG_step by auto

    obtain k where "k > j" and "afG φ (Gn φ) (w [0 → k]) ∼ falsen"
      using 1 using Suc_le_eq by blast
    then have "afG φ (Gn φ) (w [Suc j → k]) ∼ falsen"
      using afG_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
    then have "af (Gn φ) (w [Suc j → k]) ∼ falsen"
      using afG_false_implies_af_false by fastforce
    then have "af (Gn φ) (w [Suc j → k]) ∼L falsen"
      using eq_implies_lang by fastforce
    then have "af (Gn φ) (w [i → k]) ∼L falsen"
      by (metis (full_types) af_G_prefix_lang_equiv_false subsequence_append_general Suc_le_eq ‹i < j› ‹j < k› less_SucI order.order_iff_strict)
    then have "∃j. af (Gn φ) (w [i → j]) ∼L falsen"
      by fast
  }

  then show False
    using assms by blast
qed



subsection ‹After Function using GF-advice›

definition af_letterν :: "'a ltln set ⇒ 'a ltln × 'a ltln ⇒ 'a set ⇒ 'a ltln × 'a ltln"
where
  "af_letterν X p ν = (if snd p ∼ falsen
    then (af_letter (fst p) ν, (normalise (af_letter (fst p) ν))[X]ν)
    else (af_letter (fst p) ν, af_letter (snd p) ν))"

abbreviation afν :: "'a ltln set ⇒ 'a ltln × 'a ltln ⇒ 'a set list ⇒ 'a ltln × 'a ltln"
where
  "afν X p w ≡ foldl (af_letterν X) p w"

lemma af_letterν_fst[simp]:
  "fst (af_letterν X p ν) = af_letter (fst p) ν"
  by (simp add: af_letterν_def)

lemma af_letterν_snd[simp]:
  "snd p ∼ falsen ⟹ snd (af_letterν X p ν) = (normalise (af_letter (fst p) ν))[X]ν"
  "¬ (snd p) ∼ falsen ⟹ snd (af_letterν X p ν) = af_letter (snd p) ν"
  by (simp_all add: af_letterν_def)

lemma afν_fst:
  "fst (afν X p w) = af (fst p) w"
  by (induction w rule: rev_induct) simp+

lemma afν_snd:
  "¬ af (snd p) w ∼ falsen ⟹ snd (afν X p w) = af (snd p) w"
  by (induction w rule: rev_induct) (simp_all, metis af_letterν_snd(2) af_letter.simps(2) af_letter_congruent)

lemma afν_snd':
  "∀i. ¬ snd (afν X p (take i w)) ∼ falsen ⟹ snd (afν X p w) = af (snd p) w"
  by (induction w rule: rev_induct) (simp_all, metis af_letterν_snd(2) diff_is_0_eq foldl_Nil le_cases take_all take_eq_Nil)

lemma afν_step:
  "snd (afν X (ξ, ζ) w) ∼ falsen ⟹ snd (afν X (ξ, ζ) (w @ [ν])) = (normalise (af ξ (w @ [ν])))[X]ν"
  by (simp add: afν_fst)

lemma afν_segments:
  "afν X (ξ, ζ) w = (af ξ w, (af ξ w)[X]ν) ⟹ afν X (ξ, ζ) (w @ w') = afν X (af ξ w, (af ξ w)[X]ν) w'"
  by (induction w' rule: rev_induct) fastforce+


lemma afν_semantics_ltr:
  assumes
    "∃i. suffix i w ⊨n (af φ (prefix i w))[X]ν"
  shows
    "∃m. ∀k≥m. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Suc k) w)) ∼ falsen"
proof
  define resets where "resets = {i. snd (afν X (φ, (normalise φ)[X]ν) (prefix i w)) ∼ falsen}"
  define m where "m = (if resets = {} then 0 else Suc (Max resets))"

  from assms obtain i where 1: "suffix i w ⊨n (af φ (prefix i w))[X]ν"
    by blast

  {
    fix j
    assume "i ≤ j" and "j ∈ resets"

    let ?φ = "af φ (prefix (Suc j) w)"

    from 1 have "∀n. suffix n (suffix i w) ⊨n (normalise (af φ (prefix i w @ prefix n (suffix i w))))[X]ν"
      using normalise_monotonic by (simp add: GF_advice_af)

    then have "suffix (Suc j) w ⊨n (normalise (af φ (prefix (Suc j) w)))[X]ν"
      by (metis (no_types) ‹i ≤ j› add.right_neutral le_SucI le_Suc_ex subsequence_append subsequence_shift suffix_suffix)

    then have "∀k>j. ¬ af ((normalise (af φ (prefix (Suc j) w)))[X]ν) (w [Suc j → k]) ∼ falsen"
      by (metis ltl_implies_satisfiable_prefix subsequence_prefix_suffix)

    then have "∀k>j. ¬ snd (afν X (?φ, (normalise ?φ)[X]ν) (w [Suc j → k])) ∼ falsen"
      by (metis afν_snd snd_eqD)

    moreover

    {
      have "fst (afν X (φ, (normalise φ)[X]ν) (prefix (Suc j) w)) = ?φ"
        by (simp add: afν_fst)

      moreover

      have "snd (afν X (φ, (normalise φ)[X]ν) (prefix j w)) ∼ falsen"
        using ‹j ∈ resets› resets_def by blast

      ultimately have "afν X (φ, (normalise φ)[X]ν) (prefix (Suc j) w) = (?φ, (normalise ?φ)[X]ν)"
        by (metis (no_types) afν_step prod.collapse subseq_to_Suc zero_le)
    }

    ultimately have "∀k>j. ¬ snd (afν X (φ, (normalise φ)[X]ν) ((w [0 → Suc j]) @ (w [Suc j → k]))) ∼ falsen"
      by (simp add: afν_segments)

    then have "∀k>j. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix k w)) ∼ falsen"
      by (metis Suc_leI le0 subsequence_append_general)

    then have "∀k ∈ resets. k ≤ j"
      using ‹j ∈ resets› resets_def le_less_linear by blast
  }

  then have "finite resets"
    by (meson finite_nat_set_iff_bounded_le infinite_nat_iff_unbounded_le)

  then have "resets ≠ {} ⟹ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Max resets) w)) ∼ falsen"
    using Max_in resets_def by blast

  then have "∀k≥m. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix k w)) ∼ falsen"
    by (metis (mono_tags, lifting) Max_ge Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq order.trans resets_def)

  then show "∀k≥m. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Suc k) w)) ∼ falsen"
    using le_SucI by blast
qed

lemma afν_semantics_rtl:
  assumes
    "∃n. ∀k≥n. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Suc k) w)) ∼ falsen"
  shows
    "∃i. suffix i w ⊨n af φ (prefix i w)[X]ν"
proof -
  define resets where "resets = {i. snd (afν X (φ, (normalise φ)[X]ν) (prefix i w)) ∼ falsen}"
  define m where "m = (if resets = {} then 0 else Suc (Max resets))"

  from assms obtain n where "∀k≥n. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Suc k) w)) ∼ falsen"
    by blast

  then have "∀k>n. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix k w)) ∼ falsen"
    by (metis le_SucE lessE less_imp_le_nat)

  then have "finite resets"
    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)

  then have "∀i≥m. ¬ snd (afν X (φ, (normalise φ)[X]ν) (prefix i w)) ∼ falsen"
    unfolding resets_def m_def using Max_ge not_less_eq_eq by auto

  then have "∀i. ¬ snd (afν X (φ, (normalise φ)[X]ν) ((w [0 → m]) @ (w [m → i]))) ∼ falsen"
    by (metis le0 nat_le_linear subseq_to_smaller subsequence_append_general)

  moreover

  let ?φ = "af φ (prefix m w)"

  have "resets ≠ {} ⟹ snd (afν X (φ, (normalise φ)[X]ν) (prefix (Max resets) w)) ∼ falsen"
    using Max_in ‹finite resets› resets_def by blast

  then have prefix_φ': "snd (afν X (φ, (normalise φ)[X]ν) (prefix m w)) = (normalise ?φ)[X]ν"
    by (auto simp: GF_advice_congruent m_def afν_fst)

  ultimately have "∀i. ¬ snd (afν X (?φ, (normalise ?φ)[X]ν) (w [m → i])) ∼ falsen"
    by (metis afν_fst foldl_append fst_conv prod.collapse)

  then have "∀i. ¬ af ((normalise ?φ)[X]ν) (w [m → i]) ∼ falsen"
    by (metis prefix_φ' afν_fst afν_snd' fst_conv prod.collapse subsequence_take)

  then have "suffix m w ⊨n (normalise (af φ (prefix m w)))[X]ν"
    by (metis GF_advice_νLTL(1) satisfiable_prefix_implies_νLTL add.right_neutral subsequence_shift)

  from this[THEN normalise_eventually_equivalent]
    show "∃i. suffix i w ⊨n af φ (prefix i w)[X]ν"
    by (metis add.commute af_subsequence_append le_add1 le_add_same_cancel1 prefix_suffix_subsequence suffix_suffix)
qed

end


subsection ‹Reachability Bounds›

text ‹
  We show that the reach of each after-function is bounded by the atomic
  propositions of the input formula.
›

locale transition_functions_size = transition_functions +
  assumes
    normalise_nested_propos: "nested_prop_atoms φ ⊇ nested_prop_atoms (normalise φ)"
begin

lemma af_letterF_nested_prop_atoms:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ) ⟹ nested_prop_atoms (af_letterF φ ψ ν) ⊆ nested_prop_atoms (Fn φ)"
  by (induction ψ) (auto simp: af_letterF_def, insert af_letter_nested_prop_atoms, blast+)

lemma afF_nested_prop_atoms:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ) ⟹ nested_prop_atoms (afF φ ψ w) ⊆ nested_prop_atoms (Fn φ)"
  by (induction w rule: rev_induct) (insert af_letterF_nested_prop_atoms, auto)

lemma af_letterF_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ) ⟹ range (af_letterF φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ)}"
  using af_letterF_nested_prop_atoms by blast

lemma afF_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ) ⟹ range (afF φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ)}"
  using afF_nested_prop_atoms by blast

lemma af_letterG_nested_prop_atoms:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ) ⟹ nested_prop_atoms (af_letterG φ ψ ν) ⊆ nested_prop_atoms (Gn φ)"
  by (induction ψ) (auto simp: af_letterG_def, insert af_letter_nested_prop_atoms, blast+)

lemma afG_nested_prop_atoms:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ) ⟹ nested_prop_atoms (afG φ ψ w) ⊆ nested_prop_atoms (Gn φ)"
  by (induction w rule: rev_induct) (insert af_letterG_nested_prop_atoms, auto)

lemma af_letterG_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ) ⟹ range (af_letterG φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ)}"
  using af_letterG_nested_prop_atoms by blast

lemma afG_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ) ⟹ range (afG φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ)}"
  using afG_nested_prop_atoms by blast

lemma af_letterν_snd_nested_prop_atoms_helper:
  "snd p ∼ falsen ⟹ nested_prop_atoms (snd (af_letterν X p ν)) ⊆ nested_prop_atomsν (fst p) X"
  "¬ snd p ∼ falsen ⟹ nested_prop_atoms (snd (af_letterν X p ν)) ⊆ nested_prop_atoms (snd p)"
  by (simp_all add: af_letter_nested_prop_atoms nested_prop_atomsν_def)
     (metis GF_advice_nested_prop_atomsν af_letter_nested_prop_atoms nested_prop_atomsν_subset dual_order.trans nested_prop_atomsν_def normalise_nested_propos)

lemma af_letterν_fst_nested_prop_atoms:
  "nested_prop_atoms (fst (af_letterν X p ν)) ⊆ nested_prop_atoms (fst p)"
  by (simp add: af_letter_nested_prop_atoms)

lemma af_letterν_snd_nested_prop_atoms:
  "nested_prop_atoms (snd (af_letterν X p ν)) ⊆ (nested_prop_atomsν (fst p) X) ∪ (nested_prop_atoms (snd p))"
  using af_letterν_snd_nested_prop_atoms_helper by blast

lemma af_letterν_fst_range:
  "range (fst ∘ af_letterν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)}"
  using af_letterν_fst_nested_prop_atoms by force

lemma af_letterν_snd_range:
  "range (snd ∘ af_letterν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
  using af_letterν_snd_nested_prop_atoms by force

lemma af_letterν_range:
  "range (af_letterν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
proof -
  have "range (af_letterν X p) ⊆ range (fst ∘ af_letterν X p) × range (snd ∘ af_letterν X p)"
    by (simp add: image_subset_iff mem_Times_iff)

  also have "… ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
    using af_letterν_fst_range af_letterν_snd_range by blast

  finally show ?thesis .
qed

lemma afν_fst_nested_prop_atoms:
  "nested_prop_atoms (fst (afν X p w)) ⊆ nested_prop_atoms (fst p)"
  by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms, blast)

lemma af_letter_nested_prop_atomsν:
  "nested_prop_atomsν (af_letter φ ν) X ⊆ nested_prop_atomsν φ X"
  by (induction φ) (simp_all add: nested_prop_atomsν_def, blast+)

lemma afν_fst_nested_prop_atomsν:
  "nested_prop_atomsν (fst (afν X p w)) X ⊆ nested_prop_atomsν (fst p) X"
  by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atomsν, blast)

lemma afν_fst_range:
  "range (fst ∘ afν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)}"
  using afν_fst_nested_prop_atoms by fastforce

lemma afν_snd_nested_prop_atoms:
  "nested_prop_atoms (snd (afν X p w)) ⊆ (nested_prop_atomsν (fst p) X) ∪ (nested_prop_atoms (snd p))"
proof (induction w arbitrary: p rule: rev_induct)
  case (snoc x xs)

  let ?p = "afν X p xs"

  have "nested_prop_atoms (snd (afν X p (xs @ [x]))) ⊆ (nested_prop_atomsν (fst ?p) X) ∪ (nested_prop_atoms (snd ?p))"
    by (simp add: af_letterν_snd_nested_prop_atoms)

  then show ?case
    using snoc afν_fst_nested_prop_atomsν by blast
qed (simp add: nested_prop_atomsν_def)

lemma afν_snd_range:
  "range (snd ∘ afν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
  using afν_snd_nested_prop_atoms by fastforce

lemma afν_range:
  "range (afν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
proof -
  have "range (afν X p) ⊆ range (fst ∘ afν X p) × range (snd ∘ afν X p)"
    by (simp add: image_subset_iff mem_Times_iff)

  also have "… ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atomsν (fst p) X) ∪ nested_prop_atoms (snd p)}"
    using afν_fst_range afν_snd_range by blast

  finally show ?thesis .
qed

end

end