# Theory Equivalence_Relations

theory Equivalence_Relations
imports LTL
```(*
Author:   Benedikt Seidl
*)

section ‹Equivalence Relations for LTL formulas›

theory Equivalence_Relations
imports
LTL
begin

subsection ‹Language Equivalence›

definition ltl_lang_equiv :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼⇩L" 75)
where
"φ ∼⇩L ψ ≡ ∀w. w ⊨⇩n φ ⟷ w ⊨⇩n ψ"

lemma ltl_lang_equiv_equivp:
"equivp (∼⇩L)"
unfolding ltl_lang_equiv_def
by (simp add: equivpI reflp_def symp_def transp_def)

lemma ltl_lang_equiv_and_true[simp]:
"φ⇩1 and⇩n φ⇩2 ∼⇩L true⇩n ⟷ φ⇩1 ∼⇩L true⇩n ∧ φ⇩2 ∼⇩L true⇩n"
unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_and_false[intro, simp]:
"φ⇩1 ∼⇩L false⇩n ⟹ φ⇩1 and⇩n φ⇩2 ∼⇩L false⇩n"
"φ⇩2 ∼⇩L false⇩n ⟹ φ⇩1 and⇩n φ⇩2 ∼⇩L false⇩n"
unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_false[simp]:
"φ⇩1 or⇩n φ⇩2 ∼⇩L false⇩n ⟷ φ⇩1 ∼⇩L false⇩n ∧ φ⇩2 ∼⇩L false⇩n"
unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_const[intro, simp]:
"φ⇩1 ∼⇩L true⇩n ⟹ φ⇩1 or⇩n φ⇩2 ∼⇩L true⇩n"
"φ⇩2 ∼⇩L true⇩n ⟹ φ⇩1 or⇩n φ⇩2 ∼⇩L true⇩n"
unfolding ltl_lang_equiv_def by auto

subsection ‹Propositional Equivalence›

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

lemma ltl_prop_entailment_monotonI[intro]:
"S ⊨⇩P φ ⟹ S ⊆ S' ⟹ S' ⊨⇩P φ"
by (induction φ) auto

lemma ltl_models_equiv_prop_entailment:
"w ⊨⇩n φ ⟷ {ψ. w ⊨⇩n ψ} ⊨⇩P φ"
by (induction φ) auto

definition ltl_prop_equiv :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼⇩P" 75)
where
"φ ∼⇩P ψ ≡ ∀𝒜. 𝒜 ⊨⇩P φ ⟷ 𝒜 ⊨⇩P ψ"

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

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

lemma ltl_prop_equiv_equivp:
"equivp (∼⇩P)"
by (simp add: ltl_prop_equiv_def equivpI reflp_def symp_def transp_def)

lemma ltl_prop_equiv_trans[trans]:
"φ ∼⇩P ψ ⟹ ψ ∼⇩P χ ⟹ φ ∼⇩P χ"

lemma ltl_prop_equiv_true:
"φ ∼⇩P true⇩n ⟷ {} ⊨⇩P φ"
using bot.extremum ltl_prop_entailment.simps(1) ltl_prop_equiv_def by blast

lemma ltl_prop_equiv_false:
"φ ∼⇩P false⇩n ⟷ ¬ UNIV ⊨⇩P φ"
by (meson ltl_prop_entailment.simps(2) ltl_prop_entailment_monotonI ltl_prop_equiv_def top_greatest)

lemma ltl_prop_equiv_true_implies_true:
"x ∼⇩P true⇩n ⟹ x ⟶⇩P y ⟹ y ∼⇩P true⇩n"

lemma ltl_prop_equiv_false_implied_by_false:
"y ∼⇩P false⇩n ⟹ x ⟶⇩P y ⟹ x ∼⇩P false⇩n"

lemma ltl_prop_implication_implies_ltl_implication:
"w ⊨⇩n φ ⟹ φ ⟶⇩P ψ ⟹ w ⊨⇩n ψ"
using ltl_models_equiv_prop_entailment ltl_prop_implies_def by blast

lemma ltl_prop_equiv_implies_ltl_lang_equiv:
"φ ∼⇩P ψ ⟹ φ ∼⇩L ψ"
using ltl_lang_equiv_def ltl_prop_implication_implies_ltl_implication ltl_prop_implies_equiv by blast

lemma ltl_prop_equiv_lt_ltl_lang_equiv[simp]:
"(∼⇩P) ≤ (∼⇩L)"
using ltl_prop_equiv_implies_ltl_lang_equiv by blast

subsection ‹Constants Equivalence›

datatype tvl = Yes | No | Maybe

definition eval_and :: "tvl ⇒ tvl ⇒ tvl"
where
"eval_and φ ψ =
(case (φ, ψ) of
(Yes, Yes) ⇒ Yes
| (No, _) ⇒ No
| (_, No) ⇒ No
| _ ⇒ Maybe)"

definition eval_or :: "tvl ⇒ tvl ⇒ tvl"
where
"eval_or φ ψ =
(case (φ, ψ) of
(No, No) ⇒ No
| (Yes, _) ⇒ Yes
| (_, Yes) ⇒ Yes
| _ ⇒ Maybe)"

fun eval :: "'a ltln ⇒ tvl"
where
"eval true⇩n = Yes"
| "eval false⇩n = No"
| "eval (φ and⇩n ψ) = eval_and (eval φ) (eval ψ)"
| "eval (φ or⇩n ψ) = eval_or (eval φ) (eval ψ)"
| "eval φ = Maybe"

lemma eval_and_const[simp]:
"eval_and φ ψ = No ⟷ φ = No ∨ ψ = No"
"eval_and φ ψ = Yes ⟷ φ = Yes ∧ ψ = Yes"
unfolding eval_and_def
by (cases φ; cases ψ, auto)+

lemma eval_or_const[simp]:
"eval_or φ ψ = Yes ⟷ φ = Yes ∨ ψ = Yes"
"eval_or φ ψ = No ⟷ φ = No ∧ ψ = No"
unfolding eval_or_def
by (cases φ; cases ψ, auto)+

lemma eval_prop_entailment:
"eval φ = Yes ⟷ {} ⊨⇩P φ"
"eval φ = No ⟷ ¬ UNIV ⊨⇩P φ"
by (induction φ) auto

definition ltl_const_equiv :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼⇩C" 75)
where
"φ ∼⇩C ψ ≡ φ = ψ ∨ (eval φ = eval ψ ∧ eval ψ ≠ Maybe)"

lemma ltl_const_equiv_equivp:
"equivp (∼⇩C)"
unfolding ltl_const_equiv_def
by (intro equivpI reflpI sympI transpI) auto

lemma ltl_const_equiv_const:
"φ ∼⇩C true⇩n ⟷ eval φ = Yes"
"φ ∼⇩C false⇩n ⟷ eval φ = No"
unfolding ltl_const_equiv_def by force+

lemma ltl_const_equiv_and_const[simp]:
"φ⇩1 and⇩n φ⇩2 ∼⇩C true⇩n ⟷ φ⇩1 ∼⇩C true⇩n ∧ φ⇩2 ∼⇩C true⇩n"
"φ⇩1 and⇩n φ⇩2 ∼⇩C false⇩n ⟷ φ⇩1 ∼⇩C false⇩n ∨ φ⇩2 ∼⇩C false⇩n"
unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_or_const[simp]:
"φ⇩1 or⇩n φ⇩2 ∼⇩C true⇩n ⟷ φ⇩1 ∼⇩C true⇩n ∨ φ⇩2 ∼⇩C true⇩n"
"φ⇩1 or⇩n φ⇩2 ∼⇩C false⇩n ⟷ φ⇩1 ∼⇩C false⇩n ∧ φ⇩2 ∼⇩C false⇩n"
unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_other[simp]:
"φ ∼⇩C prop⇩n(a) ⟷ φ = prop⇩n(a)"
"φ ∼⇩C nprop⇩n(a) ⟷ φ = nprop⇩n(a)"
"φ ∼⇩C X⇩n ψ ⟷ φ = X⇩n ψ"
"φ ∼⇩C ψ⇩1 U⇩n ψ⇩2 ⟷ φ = ψ⇩1 U⇩n ψ⇩2"
"φ ∼⇩C ψ⇩1 R⇩n ψ⇩2 ⟷ φ = ψ⇩1 R⇩n ψ⇩2"
"φ ∼⇩C ψ⇩1 W⇩n ψ⇩2 ⟷ φ = ψ⇩1 W⇩n ψ⇩2"
"φ ∼⇩C ψ⇩1 M⇩n ψ⇩2 ⟷ φ = ψ⇩1 M⇩n ψ⇩2"
using ltl_const_equiv_def by fastforce+

lemma ltl_const_equiv_no_const_singleton:
"eval ψ = Maybe ⟹ φ ∼⇩C ψ ⟹ φ = ψ"
unfolding ltl_const_equiv_def by fastforce

lemma ltl_const_equiv_implies_prop_equiv:
"φ ∼⇩C true⇩n ⟷ φ ∼⇩P true⇩n"
"φ ∼⇩C false⇩n ⟷ φ ∼⇩P false⇩n"
unfolding ltl_const_equiv_const eval_prop_entailment ltl_prop_equiv_def
by auto

lemma ltl_const_equiv_no_const_prop_equiv:
"eval ψ = Maybe ⟹ φ ∼⇩C ψ ⟹ φ ∼⇩P ψ"
using ltl_const_equiv_no_const_singleton equivp_reflp[OF ltl_prop_equiv_equivp]
by blast

lemma ltl_const_equiv_implies_ltl_prop_equiv:
"φ ∼⇩C ψ ⟹ φ ∼⇩P ψ"
proof (induction ψ)
case (And_ltln ψ1 ψ2)

show ?case
proof (cases "eval (ψ1 and⇩n ψ2)")
case Yes

then have "φ ∼⇩C true⇩n"
by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp)
then show ?thesis
by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv)
next
case No

then have "φ ∼⇩C false⇩n"
by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp)
then show ?thesis
by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv)
next
case Maybe

then show ?thesis
using And_ltln.prems ltl_const_equiv_no_const_prop_equiv by force
qed
next
case (Or_ltln ψ1 ψ2)

then show ?case
proof (cases "eval (ψ1 or⇩n ψ2)")
case Yes

then have "φ ∼⇩C true⇩n"
by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp)
then show ?thesis
by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv)
next
case No

then have "φ ∼⇩C false⇩n"
by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp)
then show ?thesis
by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv)
next
case Maybe

then show ?thesis
using Or_ltln.prems ltl_const_equiv_no_const_prop_equiv by force
qed
qed (simp_all add: ltl_const_equiv_implies_prop_equiv equivp_reflp[OF ltl_prop_equiv_equivp])

lemma ltl_const_equiv_lt_ltl_prop_equiv[simp]:
"(∼⇩C) ≤ (∼⇩P)"
using ltl_const_equiv_implies_ltl_prop_equiv by blast

subsection ‹Quotient types›

quotient_type 'a ltln⇩L = "'a ltln" / "(∼⇩L)"
by (rule ltl_lang_equiv_equivp)

instantiation ltln⇩L :: (type) equal
begin

lift_definition ltln⇩L_eq_test :: "'a ltln⇩L ⇒ 'a ltln⇩L ⇒ bool" is "λx y. x ∼⇩L y"
by (metis ltln⇩L.abs_eq_iff)

definition
eq⇩L: "equal_class.equal ≡ ltln⇩L_eq_test"

instance
by (standard; simp add: eq⇩L ltln⇩L_eq_test.rep_eq, metis Quotient_ltln⇩L Quotient_rel_rep)

end

quotient_type 'a ltln⇩P = "'a ltln" / "(∼⇩P)"
by (rule ltl_prop_equiv_equivp)

instantiation ltln⇩P :: (type) equal
begin

lift_definition ltln⇩P_eq_test :: "'a ltln⇩P ⇒ 'a ltln⇩P ⇒ bool" is "λx y. x ∼⇩P y"
by (metis ltln⇩P.abs_eq_iff)

definition
eq⇩P: "equal_class.equal ≡ ltln⇩P_eq_test"

instance
by (standard; simp add: eq⇩P ltln⇩P_eq_test.rep_eq, metis Quotient_ltln⇩P Quotient_rel_rep)

end

quotient_type 'a ltln⇩C = "'a ltln" / "(∼⇩C)"
by (rule ltl_const_equiv_equivp)

instantiation ltln⇩C :: (type) equal
begin

lift_definition ltln⇩C_eq_test :: "'a ltln⇩C ⇒ 'a ltln⇩C ⇒ bool" is "λx y. x ∼⇩C y"
by (metis ltln⇩C.abs_eq_iff)

definition
eq⇩C: "equal_class.equal ≡ ltln⇩C_eq_test"

instance
by (standard; simp add: eq⇩C ltln⇩C_eq_test.rep_eq, metis Quotient_ltln⇩C Quotient_rel_rep)

end

subsection ‹Cardinality of propositional quotient sets›

definition sat_models :: "'a ltln⇩P ⇒ 'a ltln set set"
where
"sat_models φ = {𝒜. 𝒜 ⊨⇩P rep_ltln⇩P φ}"

lemma Rep_Abs_prop_entailment[simp]:
"𝒜 ⊨⇩P rep_ltln⇩P (abs_ltln⇩P φ) = 𝒜 ⊨⇩P φ"
by (metis Quotient3_ltln⇩P Quotient3_rep_abs ltl_prop_equiv_def)

lemma sat_models_Abs:
"𝒜 ∈ sat_models (abs_ltln⇩P φ) = 𝒜 ⊨⇩P φ"

lemma sat_models_inj:
"inj sat_models"
proof (rule injI)
fix φ ψ :: "'a ltln⇩P"
assume "sat_models φ = sat_models ψ"

then have "rep_ltln⇩P φ ∼⇩P rep_ltln⇩P ψ"
unfolding sat_models_def ltl_prop_equiv_def by force

then show "φ = ψ"
by (meson Quotient3_ltln⇩P Quotient3_rel_rep)
qed

fun prop_atoms :: "'a ltln ⇒ 'a ltln set"
where
"prop_atoms true⇩n = {}"
| "prop_atoms false⇩n = {}"
| "prop_atoms (φ and⇩n ψ) = prop_atoms φ ∪ prop_atoms ψ"
| "prop_atoms (φ or⇩n ψ) = prop_atoms φ ∪ prop_atoms ψ"
| "prop_atoms φ = {φ}"

fun nested_prop_atoms :: "'a ltln ⇒ 'a ltln set"
where
"nested_prop_atoms true⇩n = {}"
| "nested_prop_atoms false⇩n = {}"
| "nested_prop_atoms (φ and⇩n ψ) = nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ or⇩n ψ) = nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (X⇩n φ) = {X⇩n φ} ∪ nested_prop_atoms φ"
| "nested_prop_atoms (φ U⇩n ψ) = {φ U⇩n ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ R⇩n ψ) = {φ R⇩n ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ W⇩n ψ) = {φ W⇩n ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ M⇩n ψ) = {φ M⇩n ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms φ = {φ}"

lemma prop_atoms_nested_prop_atoms:
"prop_atoms φ ⊆ nested_prop_atoms φ"
by (induction φ) auto

lemma prop_atoms_subfrmlsn:
"prop_atoms φ ⊆ subfrmlsn φ"
by (induction φ) auto

lemma nested_prop_atoms_subfrmlsn:
"nested_prop_atoms φ ⊆ subfrmlsn φ"
by (induction φ) auto

lemma prop_atoms_notin[simp]:
"true⇩n ∉ prop_atoms φ"
"false⇩n ∉ prop_atoms φ"
"φ⇩1 and⇩n φ⇩2 ∉ prop_atoms φ"
"φ⇩1 or⇩n φ⇩2 ∉ prop_atoms φ"
by (induction φ) auto

lemma nested_prop_atoms_notin[simp]:
"true⇩n ∉ nested_prop_atoms φ"
"false⇩n ∉ nested_prop_atoms φ"
"φ⇩1 and⇩n φ⇩2 ∉ nested_prop_atoms φ"
"φ⇩1 or⇩n φ⇩2 ∉ nested_prop_atoms φ"
by (induction φ) auto

lemma prop_atoms_finite:
"finite (prop_atoms φ)"
by (induction φ) auto

lemma nested_prop_atoms_finite:
"finite (nested_prop_atoms φ)"
by (induction φ) auto

lemma prop_atoms_entailment_iff:
"φ ∈ prop_atoms ψ ⟹ 𝒜 ⊨⇩P φ ⟷ φ ∈ 𝒜"
by (induction φ) auto

lemma prop_atoms_entailment_inter:
"prop_atoms φ ⊆ P ⟹ (𝒜 ∩ P) ⊨⇩P φ = 𝒜 ⊨⇩P φ"
by (induction φ) auto

lemma nested_prop_atoms_entailment_inter:
"nested_prop_atoms φ ⊆ P ⟹ (𝒜 ∩ P) ⊨⇩P φ = 𝒜 ⊨⇩P φ"
by (induction φ) auto

lemma sat_models_inter_inj_helper:
assumes
"prop_atoms φ ⊆ P"
and
"prop_atoms ψ ⊆ P"
and
"sat_models (abs_ltln⇩P φ) ∩ Pow P = sat_models (abs_ltln⇩P ψ) ∩ Pow P"
shows
"φ ∼⇩P ψ"
proof -
from assms have "∀𝒜. (𝒜 ∩ P) ⊨⇩P φ ⟷ (𝒜 ∩ P) ⊨⇩P ψ"
by (auto simp: sat_models_Abs)

with assms show "φ ∼⇩P ψ"
qed

lemma sat_models_inter_inj:
"inj_on (λφ. sat_models φ ∩ Pow P) {abs_ltln⇩P φ |φ. prop_atoms φ ⊆ P}"
by (auto simp: inj_on_def sat_models_inter_inj_helper ltln⇩P.abs_eq_iff)

lemma sat_models_pow_pow:
"{sat_models (abs_ltln⇩P φ) ∩ Pow P | φ. prop_atoms φ ⊆ P} ⊆ Pow (Pow P)"
by (auto simp: sat_models_def)

lemma sat_models_finite:
"finite P ⟹ finite {sat_models (abs_ltln⇩P φ) ∩ Pow P | φ. prop_atoms φ ⊆ P}"
using sat_models_pow_pow finite_subset by fastforce

lemma sat_models_card:
"finite P ⟹ card ({sat_models (abs_ltln⇩P φ) ∩ Pow P | φ. prop_atoms φ ⊆ P}) ≤ 2 ^ 2 ^ card P"
by (metis (mono_tags, lifting) sat_models_pow_pow Pow_def card_Pow card_mono finite_Collect_subsets)

lemma image_filter:
"f ` {g a | a. P a} = {f (g a) | a. P a}"
by blast

lemma prop_equiv_finite:
"finite P ⟹ finite {abs_ltln⇩P ψ | ψ. prop_atoms ψ ⊆ P}"
by (auto simp: image_filter sat_models_finite finite_imageD[OF _ sat_models_inter_inj])

lemma prop_equiv_card:
"finite P ⟹ card {abs_ltln⇩P ψ | ψ. prop_atoms ψ ⊆ P} ≤ 2 ^ 2 ^ card P"
by (auto simp: image_filter sat_models_card card_image[OF sat_models_inter_inj, symmetric])

lemma prop_equiv_subset:
"{abs_ltln⇩P ψ |ψ. nested_prop_atoms ψ ⊆ P} ⊆ {abs_ltln⇩P ψ |ψ. prop_atoms ψ ⊆ P}"
using prop_atoms_nested_prop_atoms by blast

lemma prop_equiv_finite':
"finite P ⟹ finite {abs_ltln⇩P ψ | ψ. nested_prop_atoms ψ ⊆ P}"
using prop_equiv_finite prop_equiv_subset finite_subset by fast

lemma prop_equiv_card':
"finite P ⟹ card {abs_ltln⇩P ψ | ψ. nested_prop_atoms ψ ⊆ P} ≤ 2 ^ 2 ^ card P"
by (metis (mono_tags, lifting) prop_equiv_card prop_equiv_subset prop_equiv_finite card_mono le_trans)

subsection ‹Substitution›

fun subst :: "'a ltln ⇒ ('a ltln ⇀ 'a ltln) ⇒ 'a ltln"
where
"subst true⇩n m = true⇩n"
| "subst false⇩n m = false⇩n"
| "subst (φ and⇩n ψ) m = subst φ m and⇩n subst ψ m"
| "subst (φ or⇩n ψ) m = subst φ m or⇩n 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 eval_subst:
"eval φ = Yes ⟹ eval (subst φ m) = Yes"
"eval φ = No ⟹ eval (subst φ m) = No"
by (meson empty_subsetI eval_prop_entailment ltl_prop_entailment_monotonI ltl_prop_equiv_subst_S subset_UNIV)+

lemma subst_respects_ltl_const_entailment:
"φ ∼⇩C ψ ⟹ subst φ m ∼⇩C subst ψ m"
unfolding ltl_const_equiv_def
by (cases "eval ψ") (metis eval_subst(1), metis eval_subst(2), blast)

subsection ‹Order of Equivalence Relations›

locale ltl_equivalence =
fixes
eq :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼" 75)
assumes
eq_equivp: "equivp (∼)"
and
ge_const_equiv: "(∼⇩C) ≤ (∼)"
and
le_lang_equiv: "(∼) ≤ (∼⇩L)"
begin

lemma eq_implies_ltl_equiv:
"φ ∼ ψ ⟹ w ⊨⇩n φ = w ⊨⇩n ψ"
using le_lang_equiv ltl_lang_equiv_def by blast

lemma const_implies_eq:
"φ ∼⇩C ψ ⟹ φ ∼ ψ"
using ge_const_equiv by blast

lemma eq_implies_lang:
"φ ∼ ψ ⟹ φ ∼⇩L ψ"
using le_lang_equiv by blast

lemma eq_refl[simp]:
"φ ∼ φ"
by (meson eq_equivp equivp_reflp)

lemma eq_sym[sym]:
"φ ∼ ψ ⟹ ψ ∼ φ"
by (meson eq_equivp equivp_symp)

lemma eq_trans[trans]:
"φ ∼ ψ ⟹ ψ ∼ χ ⟹ φ ∼ χ"
by (meson eq_equivp equivp_transp)

end

interpretation ltl_lang_equivalence: ltl_equivalence "(∼⇩L)"
using ltl_lang_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
by unfold_locales blast+

interpretation ltl_prop_equivalence: ltl_equivalence "(∼⇩P)"
using ltl_prop_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
by unfold_locales blast+

interpretation ltl_const_equivalence: ltl_equivalence "(∼⇩C)"
using ltl_const_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
by unfold_locales blast+

end
```