Quelle  af.thy

(*  
    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 af_G}›

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 af_G :: "'a ltl ==> 'a set list ==> 'a ltl"
where
  "af_G φ w ≡ (foldl af_G_letter φ w)"

lemma af_{G_decompose}:
  "af_G (φ and ψ) w = (af_G φ w) and (af_G ψ w)"
  "af_G (φ or ψ) w = (af_G φ w) or (af_G ψ w)"
  by (induction w rule: rev_induct) simp_all

lemma af_{G_simps}[simp]:
  "af_G true w = true"
  "af_G false w = false"
  "af_G (G φ) w = G φ"
  "af_G (X φ) (x#xs) = af_G φ (xs)"
  by (induction w) simp_all

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

lemma af_{G_U}:
  "af_G (φ U ψ) (x#xs) = (af_G (φ U ψ) xs and af_G φ (x#xs)) or af_G ψ (x#xs)"
  by (simp add: af_{G_decompose})

lemma af_{G_subsequence_U}:
  "af_G (φ U ψ) (w [0 → Suc n]) = (af_G (φ U ψ) (w [1 → Suc n]) and af_G φ (w [0 → Suc n])) or af_G ψ (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 af_{G_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 ψ ==> af_G φ w ⟶_P af_G ψ w"
  "φ ≡_P ψ ==> af_G φ w ≡_P af_G ψ 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 G ==> G ⊨_P φ ==> G ⊨_P af_G_letter φ ν"
  by (induction φ) (simp_all, blast+)

lemma af_{G_sat_core}:
  "Only_G G ==> G ⊨_P φ ==> G ⊨_P af_G φ w"
  using af_G_letter_sat_core by (induction w rule: rev_induct) (simp_all, blast)

lemma af_{G_sat_core_generalized}:
  "Only_G G ==> i ≤ j ==> G ⊨_P af_G φ (w [0 → i]) ==> G ⊨_P af_G φ (w [0 → j])"
  by (metis af_{G_sat_core} foldl_append subsequence_append le_add_diff_inverse)

lemma af_{G_evalG}:
  "Only_G G ==> G ⊨_P af_G (eval_G G φ) w ⟷ G ⊨_P eval_G G (af_G φ w)" 
  by (induction φ) (simp_all add: eval_{G_prop_entailment} af_{G_decompose})

lemma af_{G_keeps_F_and_S}:
  assumes "ys ≠ []"
  assumes "S ⊨_P af_G φ ys"
  shows "S ⊨_P af_G (F φ) (xs @ ys)"
proof -
  have "af_G φ ys ∈ set (map (af_G φ) (suffixes (xs @ ys)))"
    using assms(1) unfolding suffixes_append map_append
    by (induction ys rule: List.list_nonempty_induct) auto
  thus ?thesis
    unfolding af_{G_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_af_{G_simp}[simp]:
  "G (af_G φ 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 = af_G φ w"
  using assms
proof (induction w arbitrary: φ)
  case (Cons x xs)
    hence "af (af_letter φ x) xs = af_G (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_af_{G_base_cases}:
  "af true w = af_G true w"
  "af false w = af_G false w"
  "af p(a) w = af_G p(a) w"
  "af (np(a)) w = af_G (np(a)) w"
  by (auto intro: af_G_free)

lemma af_implies_af_G:
  "S ⊨_P af φ w ==> S ⊨_P af_G φ 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 (af_G φ 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_af_{G_2}:
  "w ⊨ af φ xs ==> w ⊨ af_G φ xs"
  by (metis ltl_prop_implication_implies_ltl_implication af_implies_af_G ltl_prop_implies_def)

lemma af_{G_implies_af_evalG}':
  assumes "S ⊨_P eval_G G (af_G φ w)"
  assumes "∧ψ. G ψ ∈ G ==> S ⊨_P G ψ"
  assumes "∧ψ i. G ψ ∈ G ==> i < length w ==> S ⊨_P eval_G G (af_G ψ (drop i w))" 
  shows   "S ⊨_P af φ w"
  using assms
proof (induction φ arbitrary: w)
  case (LTLGlobal φ)
    hence "G φ ∈ G"
      unfolding af_{G_simps} eval_G.simps by (cases "G φ ∈ 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 eval_G G (af_G φ w')"
        using LTLGlobal.prems ‹G φ ∈ G› by simp
      hence "S ⊨_P x"
        using LTLGlobal(1)[OF ‹S ⊨_P eval_G G (af_G φ w')›] LTLGlobal(3-4) drop_drop
        unfolding ‹x = af φ w'› ‹w' = drop i w› by simp
    }
    ultimately
    show ?case
      unfolding af_G eval_{G_And_map} And_prop_entailment by simp
next
  case (LTLFinal φ)
    then obtain x where x_def: "x ∈ set (F φ # map (eval_G G o af_G φ) (suffixes w))" 
      and "S ⊨_P x"
      unfolding Or_prop_entailment af_{G_F} eval_{G_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 eval_G G (af_G φ w')" and "w' ∈ set (suffixes w)"
          using x_def ‹S ⊨_P x› by auto
        hence "∧ψ i. G ψ ∈ G ==> i < length w' ==> S ⊨_P eval_G G (af_G ψ (drop i w'))"
          using LTLFinal.prems by (auto simp add: suffixes_alt_def subsequence_def)
        moreover
        have "∧ψ. G ψ ∈ G ==> S ⊨_P eval_G G (G ψ)"
          using LTLFinal by simp
        ultimately
        have "S ⊨_P af φ w'"
          using LTLFinal.IH[OF ‹S ⊨_P eval_G G (af_G φ 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 eval_{G_Or_map} by simp
next
  case (LTLNext φ)
    thus ?case
    proof (cases w)
      case (Cons x xs)
        {
          fix ψ i
          assume "G ψ ∈ G" and "Suc i < length (x#xs)"
          hence "S ⊨_P eval_G G (af_G ψ (drop (Suc i) (x#xs)))"
            using LTLNext.prems unfolding Cons by blast
          hence "S ⊨_P eval_G G (af_G ψ (drop i xs))"
            by simp
        }
        hence "∧ψ i. G ψ ∈ G ==> i < length xs ==> S ⊨_P eval_G G (af_G ψ (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 eval_G G (af_G ψ (x # xs))"
          moreover
          have "∧ψ i. G ψ ∈ G ==> i < length (x#xs) ==> S ⊨_P eval_G G (af_G ψ (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 eval_G G (af_G (φ U ψ) xs)" and "S ⊨_P eval_G G (af_G φ (x # xs))"
          moreover
          have "∧ψ i. G ψ ∈ G ==> i < length (x#xs) ==> S ⊨_P eval_G G (af_G ψ (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 af_{G_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_af_{G_base_cases} af_{G_decompose} af_decompose, auto)

lemma af_{G_implies_af_evalG}:
  assumes "S ⊨_P eval_G G (af_G φ (w [0→j]))"
  assumes "∧ψ. G ψ ∈ G ==> S ⊨_P G ψ"
  assumes "∧ψ i. G ψ ∈ G ==> i ≤ j ==> S ⊨_P eval_G G (af_G ψ (w [i → j]))" 
  shows "S ⊨_P af φ (w [0→j])"
  using af_{G_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' ⊨ af_G φ 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 (af_G φ [x]). w' ⊨ ψ = (xs ⌢ w') ⊨ ψ"
      using G_stable(1)[of w' _ "[x]"] Cons.prems unfolding G_af_{G_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') ⊨ af_G φ [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' ⊨ af_G φ (x # xs)"
      using Cons.IH[of "af_G φ [x]" w'] A by simp
    finally
    show ?case unfolding conc_conc 
      by simp
qed simp

lemma af_{G_ltl_continuation_suffix}:
  "∀ψ ∈ G φ. w ⊨ ψ = (suffix i w) ⊨ ψ ==> w ⊨ φ ⟷ suffix i w ⊨ af_G φ (w [0 → i])"  
  by (metis af_G_ltl_continuation[of φ "suffix i w"] prefix_suffix subsequence_def)

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

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 Unf_G :: "'a ltl ==> 'a ltl"
where
  "Unf_G (F φ) = F φ or Unf_G φ"
| "Unf_G (G φ) = G φ" 
| "Unf_G (φ U ψ) = (φ U ψ and Unf_G φ) or Unf_G ψ"
| "Unf_G (φ and ψ) = Unf_G φ and Unf_G ψ"
| "Unf_G (φ or ψ) = Unf_G φ or Unf_G ψ"
| "Unf_G φ = φ"

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 φ ν = Unf_G (step φ ν)"

abbreviation af_opt :: "'a ltl ==> 'a set list ==> 'a ltl" (‹af_\U›)
where
  "af_\<UU> φ w ≡ (foldl af_letter_opt φ w)"

abbreviation af_G_opt :: "'a ltl ==> 'a set list ==> 'a ltl" (‹af_G\U›)
where
  "af_G\<UU> φ w ≡ (foldl af_G_letter_opt φ w)"

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

lemma af_to_af_opt:
  "Unf (af φ w) = af_\<UU> (Unf φ) w"
  "Unf_G (af_G φ w) = af_G\<UU> (Unf_G φ) w"
  by (induction w arbitrary: φ)
     (simp_all add: af_letter_alt_def)

lemma af_equiv:
  "af φ (w @ [ν]) = step (af_\<UU> (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_\<UU> (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 ψ ==> Unf_G φ ⟶_P Unf_G ψ"
  "φ ≡_P ψ ==> Unf_G φ ≡_P Unf_G ψ"
  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 Unf_G, simplified]
  using subst_respects_ltl_prop_entailment by metis+

lemma nested_propos:
  "nested_propos (step φ ν) ⊆ nested_propos φ"
  "nested_propos (Unf φ) ⊆ nested_propos φ"
  "nested_propos (Unf_G φ) ⊆ 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 (‹↑af_G›)
where
  "↑af_G ≡ 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_\U›)
where
  "↑af_\<UU> ≡ 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 (‹↑af_G\U›)
where
  "↑af_G\<UU> ≡ af_G_abs_opt.f_abs"

lift_definition step_abs :: "'a ltl_P ==> 'a set ==> 'a ltl_P" (‹↑step›) is step
  by (insert respectfulness)

lift_definition Unf_abs :: "'a ltl_P ==> 'a ltl_P" (‹↑Unf›) is Unf
  by (insert respectfulness)

lift_definition Unf_{G_abs} :: "'a ltl_P ==> 'a ltl_P" (‹↑Unf_G›) is Unf_G
  by (insert respectfulness)

subsubsection ‹Properties›

lemma af_G_letter_opt_sat_core:
  "Only_G G ==> G ⊨_P φ ==> G ⊨_P af_G_letter_opt φ ν"
  by (induction φ) auto 

lemma af_G_letter_sat_core_lifted:
  "Only_G G ==> G ⊨_P Rep φ ==> G ⊨_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 G ==> G ⊨_P Rep φ ==> G ⊨_P Rep (↑af_G\<UU> φ ν)"
  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:
  "↑Unf_G (↑step Φ ν) = ↑af_G\<UU> Φ ν"
  unfolding af_G_letter_abs_opt_def step_abs_def comp_def af_G_abs_opt.f_abs_def 
  using map_fun_apply Unf_{G_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) ltl_{P_abs_rep} map_fun_apply step_abs.abs_eq)
 
lemma af_opt_unfold: 
  "↑af_\<UU> = (λφ ν. ↑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_\<UU> (↑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_G:
  "Only_G G ==> G ⊨_P φ ==> G ⊨_P step φ ν"
  by (induction φ) auto

lemma Unf_{G_}G:
  "Only_G G ==> G ⊨_P φ ==> G ⊨_P Unf_G φ"
  by (induction φ) auto

hide_fact (open) respectfulness nested_propos

end