Theory af

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹af - Unfolding Functions›

theory af
  imports Main LTL_FGXU "Auxiliary/List2"
begin

subsection ‹af›

fun af_letter :: "'a ltl ⇒ 'a set ⇒ 'a ltl"
where
  "af_letter true ν = true"
| "af_letter false ν = false"
| "af_letter p(a) ν = (if a ∈ ν then true else false)"
| "af_letter (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_letter (φ and ψ) ν = (af_letter φ ν) and (af_letter ψ ν)"
| "af_letter (φ or ψ) ν = (af_letter φ ν) or (af_letter ψ ν)"
| "af_letter (X φ) ν = φ"
| "af_letter (G φ) ν = (G φ) and (af_letter φ ν)"
| "af_letter (F φ) ν = (F φ) or (af_letter φ ν)"
| "af_letter (φ U ψ) ν = (φ U ψ and (af_letter φ ν)) or (af_letter ψ ν)"

abbreviation af :: "'a ltl ⇒ 'a set list ⇒ 'a ltl" ("af")
where
  "af φ w ≡ foldl af_letter φ w"

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

lemma af_simps[simp]:
  "af true w = true"
  "af false w = false"
  "af (X φ) (x#xs) = af φ (xs)"
  by (induction w) simp_all

lemma af_F:
  "af (F φ) w = Or (F φ # map (af φ) (suffixes w))"
proof (induction w)
  case (Cons x xs)
    have "af (F φ) (x # xs) = af (af_letter (F φ) x) xs"
      by simp
    also
    have "… = (af (F φ) xs) or (af (af_letter (φ) x) xs)"
      unfolding af_decompose[symmetric] by simp
    finally
    show ?case using Cons Or_append_syntactic by force
qed simp

lemma af_G:
  "af (G φ) w = And (G φ # map (af φ) (suffixes w))"
proof (induction w)
  case (Cons x xs)
    have "af (G φ) (x # xs) = af (af_letter (G φ) x) xs"
      by simp
    also
    have "… = (af (G φ) xs) and (af (af_letter (φ) x) xs)"
      unfolding af_decompose[symmetric] by simp
    finally
    show ?case using Cons Or_append_syntactic by force
qed simp

lemma af_U:
  "af (φ U ψ) (x#xs) = (af (φ U ψ) xs and af φ (x#xs)) or af ψ (x#xs)"
  by (induction xs) (simp add: af_decompose)+

lemma af_respectfulness:
  "φ ⟶P ψ ⟹ af_letter φ ν ⟶P af_letter ψ ν"
  "φ ≡P ψ ⟹ af_letter φ ν ≡P af_letter ψ ν"
proof -
  { 
    fix φ 
    have "af_letter φ ν = subst φ (λχ. Some (af_letter χ ν))" 
      by (induction φ) auto 
  }
  thus "φ ⟶P ψ ⟹ af_letter φ ν ⟶P af_letter ψ ν"
    and "φ ≡P ψ ⟹ af_letter φ ν ≡P af_letter ψ ν"
    using subst_respects_ltl_prop_entailment by metis+
qed

lemma af_respectfulness':
  "φ ⟶P ψ ⟹ af φ w ⟶P af ψ w"
  "φ ≡P ψ ⟹ af φ w ≡P af ψ w"
  by (induction w arbitrary: φ ψ) (insert af_respectfulness, fastforce+)

lemma af_nested_propos:
  "nested_propos (af_letter φ ν) ⊆ nested_propos φ"
  by (induction φ) auto

subsection ‹@{term afG}›

fun af_G_letter :: "'a ltl ⇒ 'a set ⇒ 'a ltl"
where
  "af_G_letter true ν = true"
| "af_G_letter false ν = false"
| "af_G_letter p(a) ν = (if a ∈ ν then true else false)"
| "af_G_letter (np(a)) ν  = (if a ∉ ν then true else false)"
| "af_G_letter (φ and ψ) ν = (af_G_letter φ ν) and (af_G_letter ψ ν)"
| "af_G_letter (φ or ψ) ν = (af_G_letter φ ν) or (af_G_letter ψ ν)"
| "af_G_letter (X φ) ν = φ"
| "af_G_letter (G φ) ν = (G φ)"
| "af_G_letter (F φ) ν = (F φ) or (af_G_letter φ ν)"
| "af_G_letter (φ U ψ) ν = (φ U ψ and (af_G_letter φ ν)) or (af_G_letter ψ ν)"

abbreviation afG :: "'a ltl ⇒ 'a set list ⇒ 'a ltl"
where
  "afG φ w ≡ (foldl af_G_letter φ w)"

lemma afG_decompose:
  "afG (φ and ψ) w = (afG φ w) and (afG ψ w)"
  "afG (φ or ψ) w = (afG φ w) or (afG ψ w)"
  by (induction w rule: rev_induct) simp_all

lemma afG_simps[simp]:
  "afG true w = true"
  "afG false w = false"
  "afG (G φ) w = G φ"
  "afG (X φ) (x#xs) = afG φ (xs)"
  by (induction w) simp_all

lemma afG_F:
  "afG (F φ) w = Or (F φ # map (afG φ) (suffixes w))"
proof (induction w)
  case (Cons x xs)
    have "afG (F φ) (x # xs) = afG (af_G_letter (F φ) x) xs"
      by simp
    also
    have "… = (afG (F φ) xs) or (afG (af_G_letter (φ) x) xs)"
      unfolding afG_decompose[symmetric] by simp
    finally
    show ?case using Cons Or_append_syntactic by force
qed simp

lemma afG_U:
  "afG (φ U ψ) (x#xs) = (afG (φ U ψ) xs and afG φ (x#xs)) or afG ψ (x#xs)"
  by (simp add: afG_decompose)

lemma afG_subsequence_U:
  "afG (φ U ψ) (w [0 → Suc n]) = (afG (φ U ψ) (w [1 → Suc n]) and afG φ (w [0 → Suc n])) or afG ψ (w [0 → Suc n])"
proof -
  have "⋀n. w [0 → Suc n] = w 0 # w [1 → Suc n]"
    using subsequence_append[of w 1] by (simp add: subsequence_def upt_conv_Cons) 
  thus ?thesis
    using afG_U by metis
qed

lemma af_G_respectfulness:
  "φ ⟶P ψ ⟹ af_G_letter φ ν ⟶P af_G_letter ψ ν"
  "φ ≡P ψ ⟹ af_G_letter φ ν ≡P af_G_letter ψ ν"
proof -
  { 
    fix φ 
    have "af_G_letter φ ν = subst φ (λχ. Some (af_G_letter χ ν))" 
      by (induction φ) auto 
  }
  thus "φ ⟶P ψ ⟹ af_G_letter φ ν ⟶P af_G_letter ψ ν"
    and "φ ≡P ψ ⟹ af_G_letter φ ν ≡P af_G_letter ψ ν"
    using subst_respects_ltl_prop_entailment by metis+
qed

lemma af_G_respectfulness':
  "φ ⟶P ψ ⟹ afG φ w ⟶P afG ψ w"
  "φ ≡P ψ ⟹ afG φ w ≡P afG ψ w"
  by (induction w arbitrary: φ ψ) (insert af_G_respectfulness, fastforce+) 

lemma af_G_nested_propos:
  "nested_propos (af_G_letter φ ν) ⊆ nested_propos φ"
  by (induction φ) auto

lemma af_G_letter_sat_core:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P φ ⟹ 𝒢 ⊨P af_G_letter φ ν"
  by (induction φ) (simp_all, blast+)

lemma afG_sat_core:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P φ ⟹ 𝒢 ⊨P afG φ w"
  using af_G_letter_sat_core by (induction w rule: rev_induct) (simp_all, blast)

lemma afG_sat_core_generalized:
  "Only_G 𝒢 ⟹ i ≤ j ⟹ 𝒢 ⊨P afG φ (w [0 → i]) ⟹ 𝒢 ⊨P afG φ (w [0 → j])"
  by (metis afG_sat_core foldl_append subsequence_append le_add_diff_inverse)

lemma afG_evalG:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P afG (evalG 𝒢 φ) w ⟷ 𝒢 ⊨P evalG 𝒢 (afG φ w)" 
  by (induction φ) (simp_all add: evalG_prop_entailment afG_decompose)

lemma afG_keeps_F_and_S:
  assumes "ys ≠ []"
  assumes "S ⊨P afG φ ys"
  shows "S ⊨P afG (F φ) (xs @ ys)"
proof -
  have "afG φ ys ∈ set (map (afG φ) (suffixes (xs @ ys)))"
    using assms(1) unfolding suffixes_append map_append
    by (induction ys rule: List.list_nonempty_induct) auto
  thus ?thesis
    unfolding afG_F Or_prop_entailment using assms(2) by force
qed

subsection ‹G-Subformulae Simplification›

lemma G_af_simp[simp]:
  "G (af φ w) = G φ"
proof -
  { fix φ ν have "G (af_letter φ ν) = G φ" by (induction φ) auto }
  thus ?thesis
    by (induction w arbitrary: φ rule: rev_induct) fastforce+
qed

lemma G_afG_simp[simp]:
  "G (afG φ w) = G φ"
proof -
  { fix φ ν have "G (af_G_letter φ ν) = G φ" by (induction φ) auto }
  thus ?thesis
    by (induction w arbitrary: φ rule: rev_induct) fastforce+
qed

subsection ‹Relation between af and $af_G$›

lemma af_G_letter_free_F:
  "G φ = {} ⟹ G (af_letter φ ν) = {}"
  "G φ = {} ⟹ G (af_G_letter φ ν) = {}"
  by (induction φ) auto

lemma af_G_free:
  assumes "G φ = {}"
  shows "af φ w = afG φ w"
  using assms
proof (induction w arbitrary: φ)
  case (Cons x xs)
    hence "af (af_letter φ x) xs = afG (af_letter φ x) xs"
      using af_G_letter_free_F[OF Cons.prems, THEN Cons.IH] by blast
    moreover
    have "af_letter φ x = af_G_letter φ x"
      using Cons.prems by (induction φ) auto
    ultimately
    show ?case 
      by simp
qed simp

lemma af_equals_afG_base_cases:
  "af true w = afG true w"
  "af false w = afG false w"
  "af p(a) w = afG p(a) w"
  "af (np(a)) w = afG (np(a)) w"
  by (auto intro: af_G_free)

lemma af_implies_afG:
  "S ⊨P af φ w ⟹ S ⊨P afG φ w"
proof (induction w arbitrary: S rule: rev_induct)
  case (snoc x xs)
    hence "S ⊨P af_letter (af φ xs) x"
      by simp
    hence "S ⊨P af_letter (afG φ xs) x"
      using af_respectfulness(1) snoc.IH unfolding ltl_prop_implies_def by blast
    moreover
    {
      fix φ 
      have "⋀ν. S ⊨P af_letter φ ν ⟹ S ⊨P af_G_letter φ ν"
        by (induction φ) auto
    }
    ultimately
    show ?case
      using snoc.prems foldl_append by simp
qed simp

lemma af_implies_afG_2:
  "w ⊨ af φ xs ⟹ w ⊨ afG φ xs"
  by (metis ltl_prop_implication_implies_ltl_implication af_implies_afG ltl_prop_implies_def)

lemma afG_implies_af_evalG':
  assumes "S ⊨P evalG 𝒢 (afG φ w)"
  assumes "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨P G ψ"
  assumes "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length w ⟹ S ⊨P evalG 𝒢 (afG ψ (drop i w))" 
  shows   "S ⊨P af φ w"
  using assms
proof (induction φ arbitrary: w)
  case (LTLGlobal φ)
    hence "G φ ∈ 𝒢"
      unfolding afG_simps evalG.simps by (cases "G φ ∈ 𝒢") simp+
    hence "S ⊨P G φ"
      using LTLGlobal by simp
    moreover
    {
      fix x
      assume "x ∈ set (map (af φ) (suffixes w))"
      then obtain w' where "x = af φ w'" and "w' ∈ set (suffixes w)"
        by auto
      then obtain i where "w' = drop i w" and "i < length w"
        by (auto simp add: suffixes_alt_def subsequence_def)
      hence "S ⊨P evalG 𝒢 (afG φ w')"
        using LTLGlobal.prems ‹G φ ∈ 𝒢› by simp
      hence "S ⊨P x"
        using LTLGlobal(1)[OF ‹S ⊨P evalG 𝒢 (afG φ w')›] LTLGlobal(3-4) drop_drop
        unfolding ‹x = af φ w'› ‹w' = drop i w› by simp
    }
    ultimately
    show ?case
      unfolding af_G evalG_And_map And_prop_entailment by simp
next
  case (LTLFinal φ)
    then obtain x where x_def: "x ∈ set (F φ # map (evalG 𝒢 o afG φ) (suffixes w))" 
      and "S ⊨P x"
      unfolding Or_prop_entailment afG_F evalG_Or_map by force
    hence "∃y ∈ set (F φ # map (af φ) (suffixes w)). S ⊨P y"
    proof (cases "x ≠ F φ")
      case True
        then obtain w' where "S ⊨P evalG 𝒢 (afG φ w')" and "w' ∈ set (suffixes w)"
          using x_def ‹S ⊨P x› by auto
        hence "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length w' ⟹ S ⊨P evalG 𝒢 (afG ψ (drop i w'))"
          using LTLFinal.prems by (auto simp add: suffixes_alt_def subsequence_def)
        moreover
        have "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨P evalG 𝒢 (G ψ)"
          using LTLFinal by simp
        ultimately
        have "S ⊨P af φ w'"
          using LTLFinal.IH[OF ‹S ⊨P evalG 𝒢 (afG φ w')›] using assms(2) by blast 
        thus ?thesis
          using ‹w' ∈ set (suffixes w)› by auto
    qed simp
    thus ?case
      unfolding af_F Or_prop_entailment evalG_Or_map by simp
next
  case (LTLNext φ)
    thus ?case
    proof (cases w)
      case (Cons x xs)
        {
          fix ψ i
          assume "G ψ ∈ 𝒢" and "Suc i < length (x#xs)"
          hence "S ⊨P evalG 𝒢 (afG ψ (drop (Suc i) (x#xs)))"
            using LTLNext.prems unfolding Cons by blast
          hence "S ⊨P evalG 𝒢 (afG ψ (drop i xs))"
            by simp
        }
        hence "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length xs ⟹ S ⊨P evalG 𝒢 (afG ψ (drop i xs))"
          by simp
        thus ?thesis
          using LTLNext Cons by simp
    qed simp
next
  case (LTLUntil φ ψ)
    thus ?case
    proof (induction w)
      case (Cons x xs)
        {
          assume "S ⊨P evalG 𝒢 (afG ψ (x # xs))"
          moreover
          have "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length (x#xs) ⟹ S ⊨P evalG 𝒢 (afG ψ (drop i (x#xs)))"
            using Cons by simp
          ultimately
          have "S ⊨P af ψ (x # xs)"
            using Cons.prems by blast
          hence ?case
            unfolding af_U by simp
        }
        moreover
        {
          assume "S ⊨P evalG 𝒢 (afG (φ U ψ) xs)" and "S ⊨P evalG 𝒢 (afG φ (x # xs))"
          moreover
          have "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length (x#xs) ⟹ S ⊨P evalG 𝒢 (afG ψ (drop i (x#xs)))"
            using Cons by simp
          ultimately
          have "S ⊨P af φ (x # xs)" and "S ⊨P af (φ U ψ) xs"  
            using Cons by (blast, force) 
          hence ?case
            unfolding af_U by simp
        }
        ultimately
        show ?case
          using Cons(4) unfolding afG_U by auto
    qed simp
next
  case (LTLProp a)
    thus ?case
    proof (cases w)
      case (Cons x xs)
        thus ?thesis
          using LTLProp by (cases "a ∈ x") simp+
    qed simp
next
  case (LTLPropNeg a)
    thus ?case
    proof (cases w)
      case (Cons x xs)
        thus ?thesis
          using LTLPropNeg by (cases "a ∈ x") simp+
    qed simp
qed (unfold af_equals_afG_base_cases afG_decompose af_decompose, auto)

lemma afG_implies_af_evalG:
  assumes "S ⊨P evalG 𝒢 (afG φ (w [0→j]))"
  assumes "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨P G ψ"
  assumes "⋀ψ i. G ψ ∈ 𝒢 ⟹ i ≤ j ⟹ S ⊨P evalG 𝒢 (afG ψ (w [i → j]))" 
  shows "S ⊨P af φ (w [0→j])"
  using afG_implies_af_evalG'[OF assms(1-2), unfolded subsequence_length subsequence_drop] assms(3) by force 

subsection ‹Continuation›

― ‹af fulfills the infinite continuation w' of a word after skipping some finite prefix w.
    Corresponds to Lemma 7 in arXiv: 1402.3388v2›

lemma af_ltl_continuation:
  "(w ⌢ w') ⊨ φ ⟷ w' ⊨ af φ w"
proof (induction w arbitrary: φ w')
  case (Cons x xs)
    have "((x # xs) ⌢ w') 0 = x"
      unfolding conc_def nth_Cons_0 by simp
    moreover
    have "suffix 1 ((x # xs) ⌢ w') = xs ⌢ w'"
      unfolding suffix_def conc_def by fastforce
    moreover
    {
      fix φ :: "'a ltl"
      have "⋀w. w ⊨ φ ⟷ suffix 1 w ⊨ af_letter φ (w 0)"
        by (induction φ) ((unfold LTL_F_one_step_unfolding LTL_G_one_step_unfolding LTL_U_one_step_unfolding)?, auto)
    }
    ultimately
    have "((x # xs) ⌢ w') ⊨ φ ⟷ (xs ⌢ w') ⊨ af_letter φ x"
      by metis
    also
    have "… ⟷ w' ⊨ af φ (x#xs)"
      using Cons.IH by simp
    finally
    show ?case .
qed simp

lemma af_ltl_continuation_suffix:
  "w ⊨ φ ⟷ suffix i w ⊨ af φ (w[0 → i])"
  using af_ltl_continuation prefix_suffix subsequence_def by metis

lemma af_G_ltl_continuation:
  "∀ψ ∈ G φ. w' ⊨ ψ = (w ⌢ w') ⊨ ψ ⟹ (w ⌢ w') ⊨ φ ⟷ w' ⊨ afG φ w"
proof (induction w arbitrary: w' φ)
  case (Cons x xs)
    {
      fix ψ :: "'a ltl" fix  w w' w'' 
      assume "w'' ⊨ G ψ = ((w @ w') ⌢ w'') ⊨ G ψ"
      hence "w'' ⊨ G ψ = (w' ⌢  w'') ⊨ G ψ" and "(w' ⌢ w'') ⊨ G ψ = ((w @ w') ⌢ w'') ⊨ G ψ"
        by (induction w' arbitrary: w) (metis LTL_suffix_G suffix_conc_length conc_conc)+
    }
    note G_stable = this
    have A: "∀ψ∈G (afG φ [x]). w' ⊨ ψ = (xs ⌢ w') ⊨ ψ"
      using G_stable(1)[of w' _ "[x]"] Cons.prems unfolding G_afG_simp conc_conc append.simps unfolding G_nested_propos_alt_def by blast
    have B: "∀ψ∈G φ. ([x] ⌢ xs ⌢ w') ⊨ ψ = (xs ⌢ w') ⊨ ψ"
      using G_stable(2)[of w' _ "[x]"] Cons.prems unfolding conc_conc append.simps unfolding G_nested_propos_alt_def by blast 
    hence "([x] ⌢ xs ⌢ w') ⊨ φ = (xs ⌢ w') ⊨ afG φ [x]"
    proof (induction φ)
      case (LTLFinal φ)
        thus ?case
          unfolding LTL_F_one_step_unfolding
          by (auto simp add: suffix_conc_length[of "[x]", simplified])
    next
      case (LTLUntil φ ψ)
        thus ?case
          unfolding LTL_U_one_step_unfolding
          by (auto simp add: suffix_conc_length[of "[x]", simplified])
    qed (auto simp add: conc_fst[of 0 "[x]"] suffix_conc_length[of "[x]", simplified])
    also
    have "... = w' ⊨ afG φ (x # xs)"
      using Cons.IH[of "afG φ [x]" w'] A by simp
    finally
    show ?case unfolding conc_conc 
      by simp
qed simp

lemma afG_ltl_continuation_suffix:
  "∀ψ ∈ G φ. w ⊨ ψ = (suffix i w) ⊨ ψ ⟹ w ⊨ φ ⟷ suffix i w ⊨ afG φ (w [0 → i])"  
  by (metis af_G_ltl_continuation[of φ "suffix i w"] prefix_suffix subsequence_def)

subsection ‹Eager Unfolding @{term af} and @{term afG}› 

fun Unf :: "'a ltl ⇒ 'a ltl"
where
  "Unf (F φ) = F φ or Unf φ"
| "Unf (G φ) = G φ and Unf φ" 
| "Unf (φ U ψ) = (φ U ψ and Unf φ) or Unf ψ"
| "Unf (φ and ψ) = Unf φ and Unf ψ"
| "Unf (φ or ψ) = Unf φ or Unf ψ"
| "Unf φ = φ"

fun UnfG :: "'a ltl ⇒ 'a ltl"
where
  "UnfG (F φ) = F φ or UnfG φ"
| "UnfG (G φ) = G φ" 
| "UnfG (φ U ψ) = (φ U ψ and UnfG φ) or UnfG ψ"
| "UnfG (φ and ψ) = UnfG φ and UnfG ψ"
| "UnfG (φ or ψ) = UnfG φ or UnfG ψ"
| "UnfG φ = φ"

fun step :: "'a ltl ⇒ 'a set ⇒ 'a ltl"
where
  "step p(a) ν = (if a ∈ ν then true else false)"
| "step (np(a)) ν = (if a ∉ ν then true else false)"
| "step (X φ) ν = φ"
| "step (φ and ψ) ν = step φ ν and step ψ ν"
| "step (φ or ψ) ν = step φ ν or step ψ ν"
| "step φ ν = φ"

fun af_letter_opt
where
  "af_letter_opt φ ν = Unf (step φ ν)"

fun af_G_letter_opt
where
  "af_G_letter_opt φ ν = UnfG (step φ ν)"

abbreviation af_opt :: "'a ltl ⇒ 'a set list ⇒ 'a ltl" ("af𝔘")
where
  "af𝔘 φ w ≡ (foldl af_letter_opt φ w)"

abbreviation af_G_opt :: "'a ltl ⇒ 'a set list ⇒ 'a ltl" ("afG𝔘")
where
  "afG𝔘 φ w ≡ (foldl af_G_letter_opt φ w)"

lemma af_letter_alt_def:
  "af_letter φ ν = step (Unf φ) ν"
  "af_G_letter φ ν = step (UnfG φ) ν"
  by (induction φ) simp_all

lemma af_to_af_opt:
  "Unf (af φ w) = af𝔘 (Unf φ) w"
  "UnfG (afG φ w) = afG𝔘 (UnfG φ) w"
  by (induction w arbitrary: φ)
     (simp_all add: af_letter_alt_def)

lemma af_equiv:
  "af φ (w @ [ν]) = step (af𝔘 (Unf φ) w) ν"
  using af_to_af_opt(1) by (metis af_letter_alt_def(1) foldl_Cons foldl_Nil foldl_append)

lemma af_equiv':
  "af φ (w [0 → Suc i]) = step (af𝔘 (Unf φ) (w [0 → i])) (w i)"
  using af_equiv unfolding subsequence_def by auto

subsection ‹Lifted Functions›

lemma respectfulness:
  "φ ⟶P ψ ⟹ af_letter_opt φ ν ⟶P af_letter_opt ψ ν"
  "φ ≡P ψ ⟹ af_letter_opt φ ν ≡P af_letter_opt ψ ν"
  "φ ⟶P ψ ⟹ af_G_letter_opt φ ν ⟶P af_G_letter_opt ψ ν"
  "φ ≡P ψ ⟹ af_G_letter_opt φ ν ≡P af_G_letter_opt ψ ν"
  "φ ⟶P ψ ⟹ step φ ν ⟶P step ψ ν"
  "φ ≡P ψ ⟹ step φ ν ≡P step ψ ν"
  "φ ⟶P ψ ⟹ Unf φ ⟶P Unf ψ"
  "φ ≡P ψ ⟹ Unf φ ≡P Unf ψ"
  "φ ⟶P ψ ⟹ UnfG φ ⟶P UnfG ψ"
  "φ ≡P ψ ⟹ UnfG φ ≡P UnfG ψ"
  using decomposable_function_subst[of "λχ. af_letter_opt χ ν", simplified] af_letter_opt.simps
  using decomposable_function_subst[of "λχ. af_G_letter_opt χ ν", simplified] af_G_letter_opt.simps
  using decomposable_function_subst[of "λχ. step χ ν", simplified]
  using decomposable_function_subst[of Unf, simplified] 
  using decomposable_function_subst[of UnfG, simplified]
  using subst_respects_ltl_prop_entailment by metis+

lemma nested_propos:
  "nested_propos (step φ ν) ⊆ nested_propos φ"
  "nested_propos (Unf φ) ⊆ nested_propos φ"
  "nested_propos (UnfG φ) ⊆ nested_propos φ"
  "nested_propos (af_letter_opt φ ν) ⊆ nested_propos φ"
  "nested_propos (af_G_letter_opt φ ν) ⊆ nested_propos φ"
  by (induction φ) auto

text ‹Lift functions and bind to new names›

interpretation af_abs: lift_ltl_transformer af_letter
  using lift_ltl_transformer_def af_respectfulness af_nested_propos by blast

definition af_letter_abs ("↑af")
where
  "↑af ≡ af_abs.f_abs"

interpretation af_G_abs: lift_ltl_transformer af_G_letter
  using lift_ltl_transformer_def af_G_respectfulness af_G_nested_propos by blast

definition af_G_letter_abs ("↑afG")
where
  "↑afG ≡ af_G_abs.f_abs"

interpretation af_abs_opt: lift_ltl_transformer af_letter_opt
  using lift_ltl_transformer_def respectfulness nested_propos by blast

definition af_letter_abs_opt ("↑af𝔘")
where
  "↑af𝔘 ≡ af_abs_opt.f_abs"

interpretation af_G_abs_opt: lift_ltl_transformer af_G_letter_opt
  using lift_ltl_transformer_def respectfulness nested_propos by blast

definition af_G_letter_abs_opt ("↑afG𝔘")
where
  "↑afG𝔘 ≡ af_G_abs_opt.f_abs"

lift_definition step_abs :: "'a ltlP ⇒ 'a set ⇒ 'a ltlP" ("↑step") is step
  by (insert respectfulness)

lift_definition Unf_abs :: "'a ltlP ⇒ 'a ltlP" ("↑Unf") is Unf
  by (insert respectfulness)

lift_definition UnfG_abs :: "'a ltlP ⇒ 'a ltlP" ("↑UnfG") is UnfG
  by (insert respectfulness)

subsubsection ‹Properties›

lemma af_G_letter_opt_sat_core:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P φ ⟹ 𝒢 ⊨P af_G_letter_opt φ ν"
  by (induction φ) auto 

lemma af_G_letter_sat_core_lifted:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P Rep φ ⟹ 𝒢 ⊨P Rep (af_G_letter_abs φ ν)"
  by (metis af_G_letter_sat_core Quotient_ltl_prop_equiv_quotient[THEN Quotient_rep_abs] Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_abs_rep] af_G_abs.f_abs.abs_eq ltl_prop_equiv_def af_G_letter_abs_def) 

lemma af_G_letter_opt_sat_core_lifted:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P Rep φ ⟹ 𝒢 ⊨P Rep (↑afG𝔘 φ ν)"
  unfolding af_G_letter_abs_opt_def
  by (metis af_G_letter_opt_sat_core Quotient_ltl_prop_equiv_quotient[THEN Quotient_rep_abs] Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_abs_rep] af_G_abs_opt.f_abs.abs_eq ltl_prop_equiv_def) 

lemma af_G_letter_abs_opt_split:
  "↑UnfG (↑step Φ ν) = ↑afG𝔘 Φ ν"
  unfolding af_G_letter_abs_opt_def step_abs_def comp_def af_G_abs_opt.f_abs_def 
  using map_fun_apply UnfG_abs.abs_eq af_G_letter_opt.simps by auto

lemma af_unfold: 
  "↑af = (λφ ν. ↑step (↑Unf φ) ν)" 
  by (metis Unf_abs_def af_abs.f_abs.abs_eq af_letter_abs_def af_letter_alt_def(1) ltlP_abs_rep map_fun_apply step_abs.abs_eq)
 
lemma af_opt_unfold: 
  "↑af𝔘 = (λφ ν. ↑Unf (↑step φ ν))"
  by (metis (no_types, lifting) Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient Unf_abs.abs_eq af_abs_opt.f_abs.abs_eq af_letter_abs_opt_def af_letter_opt.elims id_apply map_fun_apply  step_abs_def)

lemma af_abs_equiv:
  "foldl ↑af ψ (xs @ [x]) = ↑step (foldl ↑af𝔘 (↑Unf ψ) xs) x" 
  unfolding af_unfold af_opt_unfold by (induction xs arbitrary: x ψ rule: rev_induct) simp+

lemma Rep_Abs_equiv: 
  "Rep (Abs φ) ≡P φ"
  using Rep_Abs_prop_entailment unfolding ltl_prop_equiv_def by auto

lemma Rep_step: 
  "Rep (↑step Φ ν) ≡P step (Rep Φ) ν"
  by (metis Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient ltl_prop_equiv_quotient.abs_eq_iff step_abs.abs_eq)

lemma step_𝒢:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P φ ⟹ 𝒢 ⊨P step φ ν"
  by (induction φ) auto

lemma UnfG_𝒢:
  "Only_G 𝒢 ⟹ 𝒢 ⊨P φ ⟹ 𝒢 ⊨P UnfG φ"
  by (induction φ) auto

hide_fact (open) respectfulness nested_propos

end