Theory LTL.Equivalence_Relations

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

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 andn φ2 ∼L truen ⟷ φ1 ∼L truen ∧ φ2 ∼L truen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_and_false[intro, simp]:
  "φ1 ∼L falsen ⟹ φ1 andn φ2 ∼L falsen"
  "φ2 ∼L falsen ⟹ φ1 andn φ2 ∼L falsen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_false[simp]:
  "φ1 orn φ2 ∼L falsen ⟷ φ1 ∼L falsen ∧ φ2 ∼L falsen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_const[intro, simp]:
  "φ1 ∼L truen ⟹ φ1 orn φ2 ∼L truen"
  "φ2 ∼L truen ⟹ φ1 orn φ2 ∼L truen"
  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 truen = True"
| "𝒜 ⊨P falsen = False"
| "𝒜 ⊨P φ andn ψ = (𝒜 ⊨P φ ∧ 𝒜 ⊨P ψ)"
| "𝒜 ⊨P φ orn ψ = (𝒜 ⊨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 χ"
  by (simp add: ltl_prop_equiv_def)

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

lemma ltl_prop_equiv_false:
  "φ ∼P falsen ⟷ ¬ 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 truen ⟹ x ⟶P y ⟹ y ∼P truen"
  by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

lemma ltl_prop_equiv_false_implied_by_false:
  "y ∼P falsen ⟹ x ⟶P y ⟹ x ∼P falsen"
  by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

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 truen = Yes"
| "eval falsen = No"
| "eval (φ andn ψ) = eval_and (eval φ) (eval ψ)"
| "eval (φ orn ψ) = 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 truen ⟷ eval φ = Yes"
  "φ ∼C falsen ⟷ eval φ = No"
  unfolding ltl_const_equiv_def by force+

lemma ltl_const_equiv_and_const[simp]:
  "φ1 andn φ2 ∼C truen ⟷ φ1 ∼C truen ∧ φ2 ∼C truen"
  "φ1 andn φ2 ∼C falsen ⟷ φ1 ∼C falsen ∨ φ2 ∼C falsen"
  unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_or_const[simp]:
  "φ1 orn φ2 ∼C truen ⟷ φ1 ∼C truen ∨ φ2 ∼C truen"
  "φ1 orn φ2 ∼C falsen ⟷ φ1 ∼C falsen ∧ φ2 ∼C falsen"
  unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_other[simp]:
  "φ ∼C propn(a) ⟷ φ = propn(a)"
  "φ ∼C npropn(a) ⟷ φ = npropn(a)"
  "φ ∼C Xn ψ ⟷ φ = Xn ψ"
  "φ ∼C ψ1 Un ψ2 ⟷ φ = ψ1 Un ψ2"
  "φ ∼C ψ1 Rn ψ2 ⟷ φ = ψ1 Rn ψ2"
  "φ ∼C ψ1 Wn ψ2 ⟷ φ = ψ1 Wn ψ2"
  "φ ∼C ψ1 Mn ψ2 ⟷ φ = ψ1 Mn ψ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 truen ⟷ φ ∼P truen"
  "φ ∼C falsen ⟷ φ ∼P falsen"
  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 andn ψ2)")
    case Yes

    then have "φ ∼C truen"
      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 falsen"
      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 orn ψ2)")
    case Yes

    then have "φ ∼C truen"
      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 falsen"
      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 ltlnL = "'a ltln" / "(∼L)"
  by (rule ltl_lang_equiv_equivp)

instantiation ltlnL :: (type) equal
begin

lift_definition ltlnL_eq_test :: "'a ltlnL ⇒ 'a ltlnL ⇒ bool" is "λx y. x ∼L y"
  by (metis ltlnL.abs_eq_iff)

definition
  eqL: "equal_class.equal ≡ ltlnL_eq_test"

instance
  by (standard; simp add: eqL ltlnL_eq_test.rep_eq, metis Quotient_ltlnL Quotient_rel_rep)

end


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

instantiation ltlnP :: (type) equal
begin

lift_definition ltlnP_eq_test :: "'a ltlnP ⇒ 'a ltlnP ⇒ bool" is "λx y. x ∼P y"
  by (metis ltlnP.abs_eq_iff)

definition
  eqP: "equal_class.equal ≡ ltlnP_eq_test"

instance
  by (standard; simp add: eqP ltlnP_eq_test.rep_eq, metis Quotient_ltlnP Quotient_rel_rep)

end


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

instantiation ltlnC :: (type) equal
begin

lift_definition ltlnC_eq_test :: "'a ltlnC ⇒ 'a ltlnC ⇒ bool" is "λx y. x ∼C y"
  by (metis ltlnC.abs_eq_iff)

definition
  eqC: "equal_class.equal ≡ ltlnC_eq_test"

instance
  by (standard; simp add: eqC ltlnC_eq_test.rep_eq, metis Quotient_ltlnC Quotient_rel_rep)

end



subsection ‹Cardinality of propositional quotient sets›

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

lemma Rep_Abs_prop_entailment[simp]:
  "𝒜 ⊨P rep_ltlnP (abs_ltlnP φ) = 𝒜 ⊨P φ"
  by (metis Quotient3_ltlnP Quotient3_rep_abs ltl_prop_equiv_def)

lemma sat_models_Abs:
  "𝒜 ∈ sat_models (abs_ltlnP φ) = 𝒜 ⊨P φ"
  by (simp add: sat_models_def)

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

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

  then show "φ = ψ"
    by (meson Quotient3_ltlnP Quotient3_rel_rep)
qed


fun prop_atoms :: "'a ltln ⇒ 'a ltln set"
where
  "prop_atoms truen = {}"
| "prop_atoms falsen = {}"
| "prop_atoms (φ andn ψ) = prop_atoms φ ∪ prop_atoms ψ"
| "prop_atoms (φ orn ψ) = prop_atoms φ ∪ prop_atoms ψ"
| "prop_atoms φ = {φ}"

fun nested_prop_atoms :: "'a ltln ⇒ 'a ltln set"
where
  "nested_prop_atoms truen = {}"
| "nested_prop_atoms falsen = {}"
| "nested_prop_atoms (φ andn ψ) = nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ orn ψ) = nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (Xn φ) = {Xn φ} ∪ nested_prop_atoms φ"
| "nested_prop_atoms (φ Un ψ) = {φ Un ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ Rn ψ) = {φ Rn ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ Wn ψ) = {φ Wn ψ} ∪ nested_prop_atoms φ ∪ nested_prop_atoms ψ"
| "nested_prop_atoms (φ Mn ψ) = {φ Mn ψ} ∪ 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]:
  "truen ∉ prop_atoms φ"
  "falsen ∉ prop_atoms φ"
  "φ1 andn φ2 ∉ prop_atoms φ"
  "φ1 orn φ2 ∉ prop_atoms φ"
  by (induction φ) auto

lemma nested_prop_atoms_notin[simp]:
  "truen ∉ nested_prop_atoms φ"
  "falsen ∉ nested_prop_atoms φ"
  "φ1 andn φ2 ∉ nested_prop_atoms φ"
  "φ1 orn φ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_ltlnP φ) ∩ Pow P = sat_models (abs_ltlnP ψ) ∩ Pow P"
  shows
    "φ ∼P ψ"
proof -
  from assms have "∀𝒜. (𝒜 ∩ P) ⊨P φ ⟷ (𝒜 ∩ P) ⊨P ψ"
    by (auto simp: sat_models_Abs)

  with assms show "φ ∼P ψ"
    by (simp add: prop_atoms_entailment_inter ltl_prop_equiv_def)
qed

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

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

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

lemma sat_models_card:
  "finite P ⟹ card ({sat_models (abs_ltlnP φ) ∩ 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_ltlnP ψ | ψ. 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_ltlnP ψ | ψ. 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_ltlnP ψ |ψ. nested_prop_atoms ψ ⊆ P} ⊆ {abs_ltlnP ψ |ψ. prop_atoms ψ ⊆ P}"
  using prop_atoms_nested_prop_atoms by blast

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

lemma prop_equiv_card':
  "finite P ⟹ card {abs_ltlnP ψ | ψ. 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 truen m = truen"
| "subst falsen m = falsen"
| "subst (φ andn ψ) m = subst φ m andn subst ψ m"
| "subst (φ orn ψ) m = subst φ m orn 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