# Theory af

theory af
imports LTL_FGXU List2
```(*
Author:      Salomon Sickert
*)

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)"

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 𝒢 ⟹ 𝒢 ⊨⇩P φ ⟹ 𝒢 ⊨⇩P af_G_letter φ ν"
by (induction φ) (simp_all, blast+)

lemma af⇩G_sat_core:
"Only_G 𝒢 ⟹ 𝒢 ⊨⇩P φ ⟹ 𝒢 ⊨⇩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 𝒢 ⟹ i ≤ j ⟹ 𝒢 ⊨⇩P af⇩G φ (w [0 → i]) ⟹ 𝒢 ⊨⇩P af⇩G φ (w [0 → j])"
by (metis af⇩G_sat_core foldl_append subsequence_append le_add_diff_inverse)

lemma af⇩G_eval⇩G:
"Only_G 𝒢 ⟹ 𝒢 ⊨⇩P af⇩G (eval⇩G 𝒢 φ) w ⟷ 𝒢 ⊨⇩P eval⇩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_eval⇩G':
assumes "S ⊨⇩P eval⇩G 𝒢 (af⇩G φ w)"
assumes "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨⇩P G ψ"
assumes "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length w ⟹ S ⊨⇩P eval⇩G 𝒢 (af⇩G ψ (drop i w))"
shows   "S ⊨⇩P af φ w"
using assms
proof (induction φ arbitrary: w)
case (LTLGlobal φ)
hence "G φ ∈ 𝒢"
unfolding af⇩G_simps eval⇩G.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 eval⇩G 𝒢 (af⇩G φ w')"
using LTLGlobal.prems ‹G φ ∈ 𝒢› by simp
hence "S ⊨⇩P x"
using LTLGlobal(1)[OF ‹S ⊨⇩P eval⇩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 𝒢 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 𝒢 (af⇩G φ w')" and "w' ∈ set (suffixes w)"
using x_def ‹S ⊨⇩P x› by auto
hence "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length w' ⟹ S ⊨⇩P eval⇩G 𝒢 (af⇩G ψ (drop i w'))"
using LTLFinal.prems by (auto simp add: suffixes_alt_def subsequence_def)
moreover
have "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨⇩P eval⇩G 𝒢 (G ψ)"
using LTLFinal by simp
ultimately
have "S ⊨⇩P af φ w'"
using LTLFinal.IH[OF ‹S ⊨⇩P eval⇩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 ψ ∈ 𝒢" and "Suc i < length (x#xs)"
hence "S ⊨⇩P eval⇩G 𝒢 (af⇩G ψ (drop (Suc i) (x#xs)))"
using LTLNext.prems unfolding Cons by blast
hence "S ⊨⇩P eval⇩G 𝒢 (af⇩G ψ (drop i xs))"
by simp
}
hence "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length xs ⟹ S ⊨⇩P eval⇩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 𝒢 (af⇩G ψ (x # xs))"
moreover
have "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length (x#xs) ⟹ S ⊨⇩P eval⇩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 𝒢 (af⇩G (φ U ψ) xs)" and "S ⊨⇩P eval⇩G 𝒢 (af⇩G φ (x # xs))"
moreover
have "⋀ψ i. G ψ ∈ 𝒢 ⟹ i < length (x#xs) ⟹ S ⊨⇩P eval⇩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_eval⇩G:
assumes "S ⊨⇩P eval⇩G 𝒢 (af⇩G φ (w [0→j]))"
assumes "⋀ψ. G ψ ∈ 𝒢 ⟹ S ⊨⇩P G ψ"
assumes "⋀ψ i. G ψ ∈ 𝒢 ⟹ i ≤ j ⟹ S ⊨⇩P eval⇩G 𝒢 (af⇩G ψ (w [i → j]))"
shows "S ⊨⇩P af φ (w [0→j])"
using af⇩G_implies_af_eval⇩G'[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⇩𝔘")
where
"af⇩𝔘 φ w ≡ (foldl af_letter_opt φ w)"

abbreviation af_G_opt :: "'a ltl ⇒ 'a set list ⇒ 'a ltl" ("af⇩G⇩𝔘")
where
"af⇩G⇩𝔘 φ 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⇩𝔘 (Unf φ) w"
"Unf⇩G (af⇩G φ w) = af⇩G⇩𝔘 (Unf⇩G φ) w"
by (induction w arbitrary: φ)

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 ψ ⟹ 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⇩𝔘")
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 ("↑af⇩G⇩𝔘")
where
"↑af⇩G⇩𝔘 ≡ 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 𝒢 ⟹ 𝒢 ⊨⇩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 (↑af⇩G⇩𝔘 φ ν)"
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⇩𝔘 Φ ν"
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⇩𝔘 = (λφ ν. ↑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 Unf⇩G_𝒢:
"Only_G 𝒢 ⟹ 𝒢 ⊨⇩P φ ⟹ 𝒢 ⊨⇩P Unf⇩G φ"
by (induction φ) auto

hide_fact (open) respectfulness nested_propos

end
```