# Theory LTL_FGXU

theory LTL_FGXU
imports Omega_Words_Fun
```(*
Author:      Salomon Sickert
*)

section ‹LTL (in Negation-Normal-Form, FGXU-Syntax)›

theory LTL_FGXU
imports Main "HOL-Library.Omega_Words_Fun"
begin

text ‹Inspired/Based on schimpf/LTL›

subsection ‹Syntax›

datatype (vars: 'a) ltl  =
LTLTrue                       ("true")
| LTLFalse                      ("false")
| LTLProp 'a                    ("p'(_')")
| LTLPropNeg 'a                 ("np'(_')" [86] 85)
| LTLAnd "'a ltl" "'a ltl"      ("_ and _" [83,83] 82)
| LTLOr "'a ltl" "'a ltl"       ("_ or _" [82,82] 81)
| LTLNext "'a ltl"              ("X _" [88] 87)
| LTLGlobal (theG: "'a ltl")    ("G _" [85] 84)
| LTLFinal "'a ltl"             ("F _" [84] 83)
| LTLUntil "'a ltl" "'a ltl"    ("_ U _" [87,87] 86)

subsection ‹Semantics›

fun ltl_semantics :: "['a set word, 'a ltl] ⇒ bool" (infix "⊨" 80)
where
"w ⊨ true = True"
| "w ⊨ false = False"
| "w ⊨ p(q) = (q ∈ w 0)"
| "w ⊨ np(q) = (q ∉ w 0)"
| "w ⊨ φ and ψ = (w ⊨ φ ∧ w ⊨ ψ)"
| "w ⊨ φ or ψ = (w ⊨ φ ∨ w ⊨ ψ)"
| "w ⊨ X φ = (suffix 1 w ⊨ φ)"
| "w ⊨ G φ = (∀k. suffix k w ⊨ φ)"
| "w ⊨ F φ = (∃k. suffix k w ⊨ φ)"
| "w ⊨ φ U ψ = (∃k. suffix k w ⊨ ψ ∧ (∀j < k. suffix j w ⊨ φ))"

fun ltl_prop_entailment :: "['a ltl set, 'a ltl] ⇒ bool" (infix "⊨⇩P" 80)
where
"𝒜 ⊨⇩P true = True"
| "𝒜 ⊨⇩P false = False"
| "𝒜 ⊨⇩P φ and ψ = (𝒜 ⊨⇩P φ ∧ 𝒜 ⊨⇩P ψ)"
| "𝒜 ⊨⇩P φ or ψ = (𝒜 ⊨⇩P φ ∨ 𝒜 ⊨⇩P ψ)"
| "𝒜 ⊨⇩P φ = (φ ∈ 𝒜)"

subsubsection ‹Properties›

lemma LTL_G_one_step_unfolding:
"w ⊨ G φ ⟷ (w ⊨ φ ∧ w ⊨ X (G φ))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence "w ⊨ φ"
using suffix_0[of w] ltl_semantics.simps(8)[of w φ] by metis
moreover
from ‹?lhs› have "w ⊨ X (G φ)"
by simp
ultimately
show ?rhs by simp
next
assume ?rhs
hence "w ⊨ X (G φ)" by simp
hence "∀k. suffix (k + 1) w ⊨ φ" by force
hence "∀k > 0. suffix k w ⊨ φ"
by (metis Suc_eq_plus1 gr0_implies_Suc)
moreover
from ‹?rhs› have "(suffix 0 w) ⊨ φ" by simp
ultimately
show ?lhs
using neq0_conv ltl_semantics.simps(8)[of w φ] by blast
qed

lemma LTL_F_one_step_unfolding:
"w ⊨ F φ ⟷ (w ⊨ φ ∨ w ⊨ X (F φ))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain k where "suffix k w ⊨ φ" by fastforce
thus ?rhs by (cases k) auto
next
assume ?rhs
thus ?lhs
using suffix_0[of w] suffix_suffix[of _ 1 w] by (metis ltl_semantics.simps(7) ltl_semantics.simps(9))
qed

lemma LTL_U_one_step_unfolding:
"w ⊨ φ U ψ ⟷ (w ⊨ ψ ∨ (w ⊨ φ ∧ w ⊨ X (φ U ψ)))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain k where "suffix k w ⊨ ψ" and "∀j<k. suffix j w ⊨ φ"
by force
thus ?rhs
by (cases k) auto
next
assume ?rhs
thus ?lhs
proof (cases "w ⊨ ψ")
case False
hence "w ⊨ φ ∧ w ⊨ X (φ U ψ)"
using ‹?rhs› by blast
obtain k where "suffix k (suffix 1 w) ⊨ ψ" and "∀j<k. suffix j (suffix 1 w) ⊨ φ"
using False ‹?rhs› by force
moreover
{
fix j assume "j < 1 + k"
hence "suffix j w ⊨ φ"
using ‹w ⊨ φ ∧ w ⊨ X (φ U ψ)› ‹∀j<k. suffix j (suffix 1 w) ⊨ φ›[unfolded suffix_suffix]
by (cases j) simp+
}
ultimately
show ?thesis
by auto
qed force
qed

lemma LTL_GF_infinitely_many_suffixes:
"w ⊨ G (F φ) = (∃⇩∞i. suffix i w ⊨ φ)"
(is "?lhs = ?rhs")
proof
let ?S = "{i | i j. suffix (i + j) w ⊨ φ}"
let ?S' = "{i + j | i j. suffix (i + j) w ⊨ φ}"

assume ?lhs
hence "infinite ?S"
by auto
moreover
have "∀s ∈ ?S. ∃s' ∈ ?S'. s ≤ s'"
by fastforce
ultimately
have "infinite ?S'"
using infinite_nat_iff_unbounded_le le_trans by meson
moreover
have "?S' = {k | k. suffix k w ⊨ φ}"
ultimately
have "infinite {k | k. suffix k w ⊨ φ}"
by metis
thus ?rhs unfolding Inf_many_def by force
next
assume ?rhs
{
fix i
from ‹?rhs› obtain k where "i ≤ k" and "suffix k w ⊨ φ"
using INFM_nat_le[of "λn. suffix n w ⊨ φ"] by blast
then obtain j where "k = i + j"
using le_iff_add[of i k] by fast
hence "suffix j (suffix i w) ⊨ φ"
using ‹suffix k w ⊨ φ› suffix_suffix by fastforce
hence "suffix i w ⊨ F φ" by auto
}
thus ?lhs by auto
qed

lemma LTL_FG_almost_all_suffixes:
"w ⊨ F G φ = (∀⇩∞i. suffix i w ⊨ φ)"
(is "?lhs = ?rhs")
proof
let ?S = "{k. ¬ suffix k w ⊨ φ}"

assume ?lhs
then obtain i where "suffix i w ⊨ G φ"
by fastforce
hence "⋀j. j ≥ i ⟹ (suffix j w ⊨ φ)"
using le_iff_add[of i] by auto
hence "⋀j. ¬suffix j w ⊨ φ ⟹ j < i"
using le_less_linear by blast
hence "?S ⊆ {k. k < i}"
by blast
hence "finite ?S"
using finite_subset by fast
thus ?rhs
unfolding Alm_all_def Inf_many_def by presburger
next
assume ?rhs
obtain S where S_def: "S = {k. ¬ suffix k w ⊨ φ}" by blast
hence "finite S"
using ‹?rhs› unfolding Alm_all_def Inf_many_def by fast
then obtain i where "i = Max S" by blast
{
fix j
assume "i < j"
hence "j ∉ S"
using ‹i = Max S› Max.coboundedI[OF ‹finite S›] less_le_not_le by blast
hence "suffix j w ⊨ φ" using S_def by fast
}
hence "∀j > i. (suffix j w ⊨ φ)" by simp
hence "suffix (Suc i) w ⊨ G φ" by auto
thus ?lhs
using ltl_semantics.simps(9)[of w "G φ"] by blast
qed

lemma LTL_FG_suffix:
"(suffix i w) ⊨ F (G φ) = w ⊨ F (G φ)"
proof -
have "(∃m. ∀n≥m. suffix n w ⊨ φ) = (∃m. ∀n≥m. suffix n (suffix i w) ⊨ φ)" (is "?l = ?r")
proof
assume ?r
then obtain m where "∀n≥m. suffix n (suffix i w) ⊨ φ"
by blast
hence "∀n≥i+m. suffix n w ⊨ φ"
thus ?l
by auto
qed (metis suffix_suffix trans_le_add2)
thus ?thesis
unfolding LTL_FG_almost_all_suffixes MOST_nat_le ..
qed

lemma LTL_GF_suffix:
"(suffix i w) ⊨ G (F φ) = w ⊨ G (F φ)"
proof -
have "(∀m. ∃n≥m. suffix n w ⊨ φ) = (∀m. ∃n≥m. suffix n (suffix i w) ⊨ φ)" (is "?l = ?r")
proof
assume ?l
thus ?r
qed (metis suffix_suffix trans_le_add2)
thus ?thesis
unfolding LTL_GF_infinitely_many_suffixes INFM_nat_le ..
qed

lemma LTL_suffix_G:
"w ⊨ G φ ⟹ suffix i w ⊨ G φ"
using suffix_0 suffix_suffix by (induction i) simp_all

lemma LTL_prop_entailment_monotonI[intro]:
"S ⊨⇩P φ ⟹ S ⊆ S' ⟹ S' ⊨⇩P φ"
by (induction rule: ltl_prop_entailment.induct) auto

lemma ltl_models_equiv_prop_entailment:
"w ⊨ φ = {χ. w ⊨ χ} ⊨⇩P φ"
by (induction φ) auto

subsubsection ‹Limit Behaviour of the G-operator›

abbreviation Only_G
where
"Only_G S ≡ ∀x ∈ S. ∃y. x = G y"

lemma ltl_G_stabilize:
assumes "finite 𝒢"
assumes "Only_G 𝒢"
obtains i where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
proof -
have "finite 𝒢 ⟹ Only_G 𝒢 ⟹ ∃i. ∀χ ∈ 𝒢. ∀j. suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
proof (induction rule: finite_induct)
case (insert χ 𝒢)
then obtain i⇩1  where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i⇩1 w ⊨ χ = suffix (i⇩1 + j) w ⊨ χ"
by blast
moreover
from insert obtain ψ where "χ = G ψ"
by blast
have "∃i. ∀j. suffix i w ⊨ G ψ = suffix (i + j) w ⊨ G ψ"
by (metis LTL_suffix_G plus_nat.add_0 suffix_0 suffix_suffix)
then obtain i⇩2 where "⋀j. suffix i⇩2 w ⊨ χ = suffix (i⇩2 + j) w ⊨ χ"
unfolding ‹χ = G ψ› by blast
ultimately
have "⋀χ' j. χ' ∈ 𝒢 ∪ {χ} ⟹ suffix (i⇩1 + i⇩2) w ⊨ χ' = suffix (i⇩1 + i⇩2 + j) w ⊨ χ'"
unfolding Un_iff singleton_iff by (metis add.commute add.left_commute)
thus ?case
by blast
qed simp
with assms obtain i where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
by blast
thus ?thesis
using that by blast
qed

lemma ltl_G_stabilize_property:
assumes "finite 𝒢"
assumes "Only_G 𝒢"
assumes "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
assumes "G ψ ∈ 𝒢 ∩ {χ. w ⊨ F χ}"
shows "suffix i w ⊨ G ψ"
proof -
obtain j where "suffix j w ⊨ G ψ"
using assms by fastforce
thus "suffix i w ⊨ G ψ"
by (cases "i ≤ j", insert assms, unfold le_iff_add, blast,
metis (erased, lifting) LTL_suffix_G ‹suffix j w ⊨ G ψ› le_add_diff_inverse nat_le_linear suffix_suffix)
qed

subsection ‹Subformulae›

subsubsection ‹Propositions›

fun propos :: "'a ltl ⇒'a ltl set"
where
"propos true = {}"
| "propos false = {}"
| "propos (φ and ψ) = propos φ ∪ propos ψ"
| "propos (φ or ψ) = propos φ ∪ propos ψ"
| "propos φ = {φ}"

fun nested_propos :: "'a ltl ⇒'a ltl set"
where
"nested_propos true = {}"
| "nested_propos false = {}"
| "nested_propos (φ and ψ) = nested_propos φ ∪ nested_propos ψ"
| "nested_propos (φ or ψ) = nested_propos φ ∪ nested_propos ψ"
| "nested_propos (F φ) = {F φ} ∪ nested_propos φ"
| "nested_propos (G φ) = {G φ} ∪ nested_propos φ"
| "nested_propos (X φ) = {X φ} ∪ nested_propos φ"
| "nested_propos (φ U ψ) = {φ U ψ} ∪ nested_propos φ ∪ nested_propos ψ"
| "nested_propos φ = {φ}"

lemma finite_propos:
"finite (propos φ)" "finite (nested_propos φ)"
by (induction φ) simp+

lemma propos_subset:
"propos φ ⊆ nested_propos φ"
by (induction φ) auto

lemma LTL_prop_entailment_restrict_to_propos:
"S ⊨⇩P φ = (S ∩ propos φ) ⊨⇩P φ"
by (induction φ) auto

lemma propos_foldl:
assumes "⋀x y. propos (f x y) = propos x ∪ propos y"
shows "⋃{propos y |y. y = i ∨ y ∈ set xs} = propos (foldl f i xs)"
proof (induction xs rule: rev_induct)
case (snoc x xs)
have "⋃{propos y |y. y = i ∨ y ∈ set (xs@[x])} = ⋃{propos y |y. y = i ∨ y ∈ set xs} ∪ propos x"
by auto
also
have "… = propos (foldl f i xs) ∪ propos x"
using snoc by auto
also
have "… = propos (foldl f i (xs@[x]))"
using assms by simp
finally
show ?case .
qed simp

subsubsection ‹G-Subformulae›

text ‹Notation for paper: mathds{G}›

fun G_nested_propos :: "'a ltl ⇒'a ltl set" ("❙G")
where
"❙G (φ and ψ) = ❙G φ ∪ ❙G ψ"
| "❙G (φ or ψ) = ❙G φ ∪ ❙G ψ"
| "❙G (F φ) = ❙G φ"
| "❙G (G φ) = ❙G φ ∪ {G φ}"
| "❙G (X φ) = ❙G φ"
| "❙G (φ U ψ) = ❙G φ ∪ ❙G ψ"
| "❙G φ = {}"

lemma G_nested_finite:
"finite (❙G φ)"
by (induction φ) auto

lemma G_nested_propos_alt_def:
"❙G φ = nested_propos φ ∩ {ψ. (∃x. ψ = G x)}"
by (induction φ) auto

lemma G_nested_propos_Only_G:
"Only_G (❙G φ)"
unfolding G_nested_propos_alt_def by blast

lemma G_not_in_G:
"G φ ∉ ❙G φ"
proof -
have "⋀χ. χ ∈ ❙G φ ⟹ size φ ≥ size χ"
by (induction φ) fastforce+
thus ?thesis
by fastforce
qed

lemma G_subset_G:
"ψ ∈ ❙G φ ⟹ ❙G ψ ⊆ ❙G φ"
"G ψ ∈ ❙G φ ⟹ ❙G ψ ⊆ ❙G φ"
by (induction φ) auto

lemma 𝒢_properties:
assumes "𝒢 ⊆ ❙G φ"
shows 𝒢_finite: "finite 𝒢" and 𝒢_elements: "Only_G 𝒢"
using assms G_nested_finite G_nested_propos_alt_def by (blast dest: finite_subset)+

subsection ‹Propositional Implication and Equivalence›

definition ltl_prop_implies :: "['a ltl, 'a ltl] ⇒ bool" (infix "⟶⇩P" 75)
where
"φ ⟶⇩P ψ ≡ ∀𝒜. 𝒜 ⊨⇩P φ ⟶ 𝒜 ⊨⇩P ψ"

definition ltl_prop_equiv :: "['a ltl, 'a ltl] ⇒ bool" (infix "≡⇩P" 75)
where
"φ ≡⇩P ψ ≡ ∀𝒜. 𝒜 ⊨⇩P φ ⟷ 𝒜 ⊨⇩P ψ"

lemma ltl_prop_implies_equiv:
"φ ⟶⇩P ψ ∧ ψ ⟶⇩P φ ⟷ φ ≡⇩P ψ"
unfolding ltl_prop_implies_def ltl_prop_equiv_def by meson

lemma ltl_prop_equiv_equivp:
"equivp (≡⇩P)"
by (blast intro: equivpI[of "(≡⇩P)", simplified transp_def symp_def reflp_def ltl_prop_equiv_def])

lemma [trans]:
"φ ≡⇩P ψ ⟹ ψ ≡⇩P χ ⟹ φ ≡⇩P χ"
using ltl_prop_equiv_equivp[THEN equivp_transp] .

subsubsection ‹Quotient Type for Propositional Equivalence›

quotient_type 'a ltl_prop_equiv_quotient = "'a ltl" / "(≡⇩P)"
morphisms Rep Abs
by (simp add: ltl_prop_equiv_equivp)

type_synonym 'a ltl⇩P = "'a ltl_prop_equiv_quotient"

instantiation ltl_prop_equiv_quotient :: (type) equal begin

lift_definition ltl_prop_equiv_quotient_eq_test :: "'a ltl⇩P ⇒ 'a ltl⇩P ⇒ bool" is "λx y. x ≡⇩P y"
by (metis ltl_prop_equiv_quotient.abs_eq_iff)

definition
eq: "equal_class.equal ≡ ltl_prop_equiv_quotient_eq_test"

instance
by (standard; simp add: eq ltl_prop_equiv_quotient_eq_test.rep_eq, metis Quotient_ltl_prop_equiv_quotient Quotient_rel_rep)

end

lemma ltl⇩P_abs_rep: "Abs (Rep φ) = φ"
by (meson Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient)

lift_definition ltl_prop_entails_abs :: "'a ltl set ⇒ 'a ltl⇩P ⇒ bool" ("_ ↑⊨⇩P _") is "(⊨⇩P)"
by (simp add: ltl_prop_equiv_def)

lift_definition ltl_prop_implies_abs :: "'a ltl⇩P ⇒ 'a ltl⇩P ⇒ bool" ("_ ↑⟶⇩P _") is "(⟶⇩P)"
by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

subsubsection ‹Propositional Equivalence implies LTL Equivalence›

lemma ltl_prop_implication_implies_ltl_implication:
"w ⊨ φ ⟹ φ ⟶⇩P ψ ⟹ w ⊨ ψ"
using [[unfold_abs_def = false]]
unfolding ltl_prop_implies_def ltl_models_equiv_prop_entailment by simp

lemma ltl_prop_equiv_implies_ltl_equiv:
"φ ≡⇩P ψ ⟹ w ⊨ φ = w ⊨ ψ"
using ltl_prop_implication_implies_ltl_implication ltl_prop_implies_equiv by blast

subsection ‹Substitution›

fun subst :: "'a ltl ⇒ ('a ltl ⇀ 'a ltl) ⇒ 'a ltl"
where
"subst true m = true"
| "subst false m = false"
| "subst (φ and ψ) m = subst φ m and subst ψ m"
| "subst (φ or ψ) m = subst φ m or subst ψ m"
| "subst φ m = (case m φ of Some φ' ⇒ φ' | None ⇒ φ)"

text ‹Based on Uwe Schoening's Translation Lemma (Logic for CS, p. 54)›

lemma ltl_prop_equiv_subst_S:
"S ⊨⇩P subst φ m = ((S - dom m) ∪ {χ | χ χ'. χ ∈ dom m ∧ m χ = Some χ' ∧ S ⊨⇩P χ'}) ⊨⇩P φ"
by (induction φ) (auto split: option.split)

lemma subst_respects_ltl_prop_entailment:
"φ ⟶⇩P ψ ⟹ subst φ m ⟶⇩P subst ψ m"
"φ ≡⇩P ψ ⟹ subst φ m ≡⇩P subst ψ m"
unfolding ltl_prop_equiv_def ltl_prop_implies_def ltl_prop_equiv_subst_S by blast+

lemma subst_respects_ltl_prop_entailment_generalized:
"(⋀𝒜. (⋀x. x ∈ S ⟹ 𝒜 ⊨⇩P x) ⟹ 𝒜 ⊨⇩P y) ⟹ (⋀x. x ∈ S ⟹ 𝒜 ⊨⇩P subst x m) ⟹ 𝒜 ⊨⇩P subst y m"
unfolding ltl_prop_equiv_subst_S by simp

lemma decomposable_function_subst:
"⟦f true = true; f false = false; ⋀φ ψ. f (φ and ψ) = f φ and f ψ; ⋀φ ψ. f (φ or ψ) = f φ or f ψ⟧ ⟹ f φ = subst φ (λχ. Some (f χ))"
by (induction φ) auto

subsubsection ‹And›

lemma foldl_LTLAnd_prop_entailment:
"S ⊨⇩P foldl LTLAnd i xs = (S ⊨⇩P i ∧ (∀y ∈ set xs. S ⊨⇩P y))"
by (induction xs arbitrary: i) auto

fun And :: "'a ltl list ⇒ 'a ltl"
where
"And [] = true"
| "And (x#xs) = foldl LTLAnd x xs"

lemma And_prop_entailment:
"S ⊨⇩P And xs = (∀x ∈ set xs. S ⊨⇩P x)"
using foldl_LTLAnd_prop_entailment by (cases xs) auto

lemma And_propos:
"propos (And xs) = ⋃{propos x| x. x ∈ set xs}"
proof (cases xs)
case Nil
thus ?thesis by simp
next
case (Cons x xs)
thus ?thesis
using propos_foldl[of LTLAnd x] by auto
qed

lemma And_semantics:
"w ⊨ And xs = (∀x ∈ set xs. w ⊨ x)"
proof -
have And_propos': "⋀x. x ∈ set xs ⟹ propos x ⊆ propos (And xs)"
using And_propos by blast

have "w ⊨ And xs = {χ. χ ∈ propos (And xs) ∧ w ⊨ χ} ⊨⇩P (And xs)"
using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
also
have "… = (∀x ∈ set xs. {χ. χ ∈ propos (And xs) ∧ w ⊨ χ} ⊨⇩P x)"
using And_prop_entailment by auto
also
have "… = (∀x ∈ set xs. {χ. χ ∈ propos x ∧ w ⊨ χ} ⊨⇩P x)"
using LTL_prop_entailment_restrict_to_propos And_propos' by blast
also
have "… = (∀x ∈ set xs. w ⊨ x)"
using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
finally
show ?thesis .
qed

lemma And_append_syntactic:
"xs ≠ [] ⟹ And (xs @ ys) = And ((And xs)#ys)"
by (induction xs rule: list_nonempty_induct) simp+

lemma And_append_S:
"S ⊨⇩P And (xs @ ys) = S ⊨⇩P And xs and And ys"
using And_prop_entailment[of S] by auto

lemma And_append:
"And (xs @ ys) ≡⇩P And xs and And ys"
unfolding ltl_prop_equiv_def using And_append_S by blast

subsubsection ‹Lifted Variant›

lift_definition and_abs :: "'a ltl⇩P ⇒ 'a ltl⇩P ⇒ 'a ltl⇩P" ("_ ↑and _") is "λx y. x and y"
unfolding ltl_prop_equiv_def by simp

fun And_abs :: "'a ltl⇩P list ⇒ 'a ltl⇩P" ("↑And")
where
"↑And xs = foldl and_abs (Abs true) xs"

lemma foldl_LTLAnd_prop_entailment_abs:
"S ↑⊨⇩P foldl and_abs i xs = (S ↑⊨⇩P i ∧ (∀y∈set xs. S ↑⊨⇩P y))"
by (induction xs arbitrary: i)
(simp_all add: and_abs_def ltl_prop_entails_abs.abs_eq, metis ltl_prop_entails_abs.rep_eq)

lemma And_prop_entailment_abs:
"S ↑⊨⇩P ↑And xs = (∀x ∈ set xs. S ↑⊨⇩P x)"
by (simp add: foldl_LTLAnd_prop_entailment_abs ltl_prop_entails_abs.abs_eq)

lemma and_abs_conjunction:
"S ↑⊨⇩P φ ↑and ψ ⟷ S ↑⊨⇩P φ ∧ S ↑⊨⇩P ψ"
by (metis and_abs.abs_eq ltl⇩P_abs_rep ltl_prop_entailment.simps(3) ltl_prop_entails_abs.abs_eq)

subsubsection ‹Or›

lemma foldl_LTLOr_prop_entailment:
"S ⊨⇩P foldl LTLOr i xs = (S ⊨⇩P i ∨ (∃y ∈ set xs. S ⊨⇩P y))"
by (induction xs arbitrary: i) auto

fun Or :: "'a ltl list ⇒ 'a ltl"
where
"Or [] = false"
| "Or (x#xs) = foldl LTLOr x xs"

lemma Or_prop_entailment:
"S ⊨⇩P Or xs = (∃x ∈ set xs. S ⊨⇩P x)"
using foldl_LTLOr_prop_entailment by (cases xs) auto

lemma Or_propos:
"propos (Or xs) = ⋃{propos x| x. x ∈ set xs}"
proof (cases xs)
case Nil
thus ?thesis by simp
next
case (Cons x xs)
thus ?thesis
using propos_foldl[of LTLOr x] by auto
qed

lemma Or_semantics:
"w ⊨ Or xs = (∃x ∈ set xs. w ⊨ x)"
proof -
have Or_propos': "⋀x. x ∈ set xs ⟹ propos x ⊆ propos (Or xs)"
using Or_propos by blast

have "w ⊨ Or xs = {χ. χ ∈ propos (Or xs) ∧ w ⊨ χ} ⊨⇩P (Or xs)"
using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
also
have "… = (∃x ∈ set xs. {χ. χ ∈ propos (Or xs) ∧ w ⊨ χ} ⊨⇩P x)"
using Or_prop_entailment by auto
also
have "… = (∃x ∈ set xs. {χ. χ ∈ propos x ∧ w ⊨ χ} ⊨⇩P x)"
using LTL_prop_entailment_restrict_to_propos Or_propos' by blast
also
have "… = (∃x ∈ set xs. w ⊨ x)"
using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
finally
show ?thesis .
qed

lemma Or_append_syntactic:
"xs ≠ [] ⟹ Or (xs @ ys) = Or ((Or xs)#ys)"
by (induction xs rule: list_nonempty_induct) simp+

lemma Or_append_S:
"S ⊨⇩P Or (xs @ ys) = S ⊨⇩P Or xs or Or ys"
using Or_prop_entailment[of S] by auto

lemma Or_append:
"Or (xs @ ys) ≡⇩P Or xs or Or ys"
unfolding ltl_prop_equiv_def using Or_append_S by blast

subsubsection ‹\$eval_G\$›

― ‹Partly evaluate a formula by only considering G-subformulae›

fun eval⇩G
where
"eval⇩G S (φ and ψ) = eval⇩G S φ and eval⇩G S ψ"
| "eval⇩G S (φ or ψ) = eval⇩G S φ or eval⇩G S ψ"
| "eval⇩G S (G φ) = (if G φ ∈ S then true else false)"
| "eval⇩G S φ = φ"

― ‹Syntactic Properties›

lemma eval⇩G_And_map:
"eval⇩G S (And xs) = And (map (eval⇩G S) xs)"
proof (induction xs rule: rev_induct)
case (snoc x xs)
thus ?case
by (cases xs) simp+
qed simp

lemma eval⇩G_Or_map:
"eval⇩G S (Or xs) = Or (map (eval⇩G S) xs)"
proof (induction xs rule: rev_induct)
case (snoc x xs)
thus ?case
by (cases xs) simp+
qed simp

lemma eval⇩G_G_nested:
"❙G (eval⇩G 𝒢 φ) ⊆ ❙G φ"
by (induction φ) (simp_all, blast+)

lemma eval⇩G_subst:
"eval⇩G S φ = subst φ (λχ. Some (eval⇩G S χ))"
by (induction φ) simp_all

― ‹Semantic Properties›

lemma eval⇩G_prop_entailment:
"S ⊨⇩P eval⇩G S φ ⟷ S ⊨⇩P φ"
by (induction φ, auto)

lemma eval⇩G_respectfulness:
"φ ⟶⇩P ψ ⟹ eval⇩G S φ ⟶⇩P eval⇩G S ψ"
"φ ≡⇩P ψ ⟹ eval⇩G S φ ≡⇩P eval⇩G S ψ"
using subst_respects_ltl_prop_entailment eval⇩G_subst by metis+

lemma eval⇩G_respectfulness_generalized:
"(⋀𝒜. (⋀x. x ∈ S ⟹ 𝒜 ⊨⇩P x) ⟹ 𝒜 ⊨⇩P y) ⟹ (⋀x. x ∈ S ⟹ 𝒜 ⊨⇩P eval⇩G P x) ⟹ 𝒜 ⊨⇩P eval⇩G P y"
using subst_respects_ltl_prop_entailment_generalized[of S y 𝒜] eval⇩G_subst[of P] by metis

lift_definition eval⇩G_abs :: "'a ltl set ⇒ 'a ltl⇩P ⇒ 'a ltl⇩P" ("↑eval⇩G") is eval⇩G
by (insert eval⇩G_respectfulness(2))

subsection ‹Finite Quotient Set›

text ‹If we restrict formulas to a finite set of propositions, the set of quotients of these is finite›

lemma Rep_Abs_prop_entailment[simp]:
"A ⊨⇩P Rep (Abs φ) = A ⊨⇩P φ"
using Quotient3_ltl_prop_equiv_quotient[THEN rep_abs_rsp]
by (auto simp add: ltl_prop_equiv_def)

fun sat_models :: "'a ltl_prop_equiv_quotient ⇒ 'a ltl set set"
where
"sat_models a = {A. A ⊨⇩P Rep(a)}"

lemma sat_models_invariant:
"A ∈ sat_models (Abs φ) = A ⊨⇩P φ"
using Rep_Abs_prop_entailment by auto

lemma sat_models_inj:
"inj sat_models"
using Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_rel_rep]
by (auto simp add: ltl_prop_equiv_def inj_on_def)

lemma sat_models_finite_image:
assumes "finite P"
shows "finite (sat_models ` {Abs φ | φ. nested_propos φ ⊆ P})"
proof -
have "sat_models (Abs φ) = {A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P}" (is "?lhs = ?rhs")
if "nested_propos φ ⊆ P" for φ
proof
have "⋀A B. A ∈ sat_models (Abs φ) ⟹ A ∪ B ∈ sat_models (Abs φ)"
unfolding sat_models_invariant by blast
moreover
have "{A | A. A ⊆ P ∧ A ⊨⇩P φ} ⊆ sat_models (Abs φ)"
using sat_models_invariant by fast
ultimately
show "?rhs ⊆ ?lhs"
by blast
next
have "propos φ ⊆ P"
using that propos_subset by blast
have "A ∈ {A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P}"
if "A ∈ sat_models (Abs φ)" for A
proof (standard, goal_cases prems)
case prems
then have "A ⊨⇩P φ"
using that sat_models_invariant by blast
then obtain C D where "C = (A ∩ P)" and "D = A - P" and "A = C ∪ D"
by blast
then have "C ⊨⇩P φ" and "C ⊆ P" and "D ⊆ UNIV - P"
using ‹A ⊨⇩P φ› LTL_prop_entailment_restrict_to_propos ‹propos φ ⊆ P› by blast+
then have "C ∪ D ∈ {A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P}"
by blast
thus ?case
using ‹A = C ∪ D› by simp
qed
thus "?lhs ⊆ ?rhs"
by blast
qed
hence Equal: "{sat_models (Abs φ) | φ. nested_propos φ ⊆ P} = {{A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
by (metis (lifting, no_types))

have Finite: "finite {{A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
proof -
let ?map = "λP S. {A ∪ B | A B. A ∈ S ∧ B ⊆ UNIV - P}"
obtain S' where S'_def: "S' = {{A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
by blast
obtain S where S_def: "S = {{A | A. A ⊆ P ∧ A ⊨⇩P φ} | φ. nested_propos φ ⊆ P}"
by blast

― ‹Prove S and ?map applied to it is finite›
hence "S ⊆ Pow (Pow P)"
by blast
hence "finite S"
using ‹finite P› finite_Pow_iff infinite_super by fast
hence "finite {?map P A | A. A ∈ S}"
by fastforce

― ‹Prove that S' can be embedded into S using ?map›

have "S' ⊆ {?map P A | A. A ∈ S}"
proof
fix A
assume "A ∈ S'"
then obtain φ where "nested_propos φ ⊆ P"
and "A = {A ∪ B | A B. A ⊆ P ∧ A ⊨⇩P φ ∧ B ⊆ UNIV - P}"
using S'_def by blast
then have "?map P {A | A. A ⊆ P ∧ A ⊨⇩P φ} = A"
by simp
moreover
have "{A | A. A ⊆ P ∧ A ⊨⇩P φ} ∈ S"
using ‹nested_propos φ ⊆ P› S_def by auto
ultimately
show "A ∈ {?map P A | A. A ∈ S}"
by blast
qed

show ?thesis
using rev_finite_subset[OF ‹finite {?map P A | A. A ∈ S}› ‹S' ⊆ {?map P A | A. A ∈ S}›]
unfolding S'_def .
qed

have Finite2: "finite {sat_models (Abs φ) | φ. nested_propos φ ⊆ P}"
unfolding Equal using Finite by blast
have Equal2: "sat_models ` {Abs φ | φ. nested_propos φ ⊆ P} = {sat_models (Abs φ) | φ. nested_propos φ ⊆ P}"
by blast

show ?thesis
unfolding Equal2 using Finite2 by blast
qed

lemma ltl_prop_equiv_quotient_restricted_to_P_finite:
assumes "finite P"
shows "finite {Abs φ | φ. nested_propos φ ⊆ P}"
proof -
have "inj_on sat_models {Abs φ |φ. nested_propos φ ⊆ P}"
using sat_models_inj subset_inj_on by auto
thus ?thesis
using finite_imageD[OF sat_models_finite_image[OF assms]] by fast
qed

locale lift_ltl_transformer =
fixes
f :: "'a ltl ⇒ 'b ⇒ 'a ltl"
assumes
respectfulness: "φ ≡⇩P ψ ⟹ f φ ν ≡⇩P f ψ ν"
assumes
nested_propos_bounded: "nested_propos (f φ ν) ⊆ nested_propos φ"
begin

lift_definition f_abs :: "'a ltl⇩P ⇒ 'b ⇒ 'a ltl⇩P" is f
using respectfulness .

lift_definition f_foldl_abs :: "'a ltl⇩P ⇒ 'b list ⇒ 'a ltl⇩P" is "foldl f"
proof -
fix φ ψ :: "'a ltl" fix w :: "'b list" assume "φ ≡⇩P ψ"
thus "foldl f φ w ≡⇩P foldl f ψ w"
using respectfulness by (induction w arbitrary: φ ψ) simp+
qed

lemma f_foldl_abs_alt_def:
"f_foldl_abs (Abs φ) w = foldl f_abs (Abs φ) w"
by (induction w rule: rev_induct) (unfold f_foldl_abs.abs_eq foldl.simps foldl_append, (metis f_abs.abs_eq)+)

definition abs_reach :: "'a ltl_prop_equiv_quotient ⇒ 'a ltl_prop_equiv_quotient set"
where
"abs_reach Φ = {foldl f_abs Φ w |w. True}"

lemma finite_abs_reach:
"finite (abs_reach (Abs φ))"
proof -
{
fix w
have "nested_propos (foldl f φ w) ⊆ nested_propos φ"
by (induction w arbitrary: φ) (simp, metis foldl_Cons nested_propos_bounded subset_trans)
}
hence "abs_reach (Abs φ) ⊆ {Abs χ | χ. nested_propos χ ⊆ nested_propos φ}"
unfolding abs_reach_def f_foldl_abs_alt_def[symmetric] f_foldl_abs.abs_eq by blast
thus ?thesis
using ltl_prop_equiv_quotient_restricted_to_P_finite finite_propos
by (blast dest: finite_subset)
qed

end

end
```