# Theory Extra_Equivalence_Relations

```(*
Author:   Salomon Sickert
*)

theory Extra_Equivalence_Relations
imports
begin

subsection ‹Propositional Equivalence with Implicit LTL Unfolding›

fun Unf :: "'a ltln ⇒ 'a ltln"
where
"Unf (φ U⇩n ψ) = ((φ U⇩n ψ) and⇩n Unf φ) or⇩n Unf ψ"
| "Unf (φ W⇩n ψ) = ((φ W⇩n ψ) and⇩n Unf φ) or⇩n Unf ψ"
| "Unf (φ M⇩n ψ) = ((φ M⇩n ψ) or⇩n Unf φ) and⇩n Unf ψ"
| "Unf (φ R⇩n ψ) = ((φ R⇩n ψ) or⇩n Unf φ) and⇩n Unf ψ"
| "Unf (φ and⇩n ψ) = Unf φ and⇩n Unf ψ"
| "Unf (φ or⇩n ψ) = Unf φ or⇩n Unf ψ"
| "Unf φ = φ"

lemma Unf_sound:
"w ⊨⇩n Unf φ ⟷ w ⊨⇩n φ"
proof (induction φ arbitrary: w)
case (Until_ltln φ1 φ2)
then show ?case
by (simp, metis less_linear not_less0 suffix_0)
next
case (Release_ltln φ1 φ2)
then show ?case
by (simp, metis less_linear not_less0 suffix_0)
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
by (simp, metis bot.extremum_unique bot_nat_def less_eq_nat.simps(1) suffix_0)
qed (simp_all, fastforce)

lemma Unf_lang_equiv:
"φ ∼⇩L Unf φ"

lemma Unf_idem:
"Unf (Unf φ) ∼⇩P Unf φ"
by (induction φ) (auto simp: ltl_prop_equiv_def)

definition ltl_prop_unfold_equiv :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼⇩Q" 75)
where
"φ ∼⇩Q ψ ≡ (Unf φ) ∼⇩P (Unf ψ)"

lemma ltl_prop_unfold_equiv_equivp:
"equivp (∼⇩Q)"
by (metis ltl_prop_equiv_equivp ltl_prop_unfold_equiv_def equivpI equivp_def reflpI sympI transpI)

lemma unfolding_prop_unfold_idem:
"Unf φ ∼⇩Q φ"
unfolding ltl_prop_unfold_equiv_def by (rule Unf_idem)

lemma unfolding_is_subst: "Unf φ = subst φ (λψ. Some (Unf ψ))"
by (induction φ) auto

lemma ltl_prop_equiv_implies_ltl_prop_unfold_equiv:
"φ ∼⇩P ψ ⟹ φ ∼⇩Q ψ"
by (metis ltl_prop_unfold_equiv_def unfolding_is_subst subst_respects_ltl_prop_entailment(2))

lemma ltl_prop_unfold_equiv_implies_ltl_lang_equiv:
"φ ∼⇩Q ψ ⟹ φ ∼⇩L ψ"
by (metis ltl_prop_equiv_implies_ltl_lang_equiv ltl_lang_equiv_def Unf_sound ltl_prop_unfold_equiv_def)

lemma ltl_prop_unfold_equiv_gt_and_lt:
"(∼⇩C) ≤ (∼⇩Q)" "(∼⇩P) ≤ (∼⇩Q)" "(∼⇩Q) ≤ (∼⇩L)"
using ltl_prop_equiv_implies_ltl_prop_unfold_equiv ltl_prop_equivalence.ge_const_equiv ltl_prop_unfold_equiv_implies_ltl_lang_equiv
by blast+

quotient_type 'a ltln⇩Q = "'a ltln" / "(∼⇩Q)"
by (rule ltl_prop_unfold_equiv_equivp)

instantiation ltln⇩Q :: (type) equal
begin

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

definition
eq⇩Q: "equal_class.equal ≡ ltln⇩Q_eq_test"

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

end

lemma af_letter_unfolding:
"af_letter (Unf φ) ν ∼⇩P af_letter φ ν"
by (induction φ) (simp_all add: ltl_prop_equiv_def, blast+)

lemma af_letter_prop_unfold_congruent:
assumes "φ ∼⇩Q ψ"
shows "af_letter φ ν ∼⇩Q af_letter ψ ν"
proof -
have "Unf φ ∼⇩P Unf ψ"
using assms by (simp add: ltl_prop_unfold_equiv_def ltl_prop_equiv_def)
then have "af_letter (Unf φ) ν ∼⇩P af_letter (Unf ψ) ν"
then have "af_letter φ ν ∼⇩P af_letter ψ ν"
by (metis af_letter_unfolding ltl_prop_equivalence.eq_sym ltl_prop_equivalence.eq_trans)
then show "af_letter φ ν ∼⇩Q af_letter ψ ν"
by (rule ltl_prop_equiv_implies_ltl_prop_unfold_equiv)
qed

assumes "φ ∼⇩Q ψ"
shows "(Unf φ)[X]⇩ν ∼⇩Q (Unf ψ)[X]⇩ν"
proof -
have "Unf φ ∼⇩P Unf ψ"
using assms
then have "(Unf φ)[X]⇩ν ∼⇩P (Unf ψ)[X]⇩ν"
then show "(Unf φ)[X]⇩ν ∼⇩Q (Unf ψ)[X]⇩ν"
qed

interpretation prop_unfold_equivalence: ltl_equivalence "(∼⇩Q)"
by unfold_locales (metis ltl_prop_unfold_equiv_equivp ltl_prop_unfold_equiv_gt_and_lt)+

interpretation af_congruent "(∼⇩Q)"
by unfold_locales (rule af_letter_prop_unfold_congruent)

lemma unfolding_monotonic:
"w ⊨⇩n φ[X]⇩ν ⟹ w ⊨⇩n (Unf φ)[X]⇩ν"
proof (induction φ)
case (Until_ltln φ1 φ2)
then show ?case
by (cases "(φ1 U⇩n φ2) ∈ X") force+
next
case (Release_ltln φ1 φ2)
then show ?case
using ltln_expand_Release by auto
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
using ltln_expand_WeakUntil by auto
next
case (StrongRelease_ltln φ1 φ2)
then show ?case
by (cases "(φ1 M⇩n φ2) ∈ X") force+
qed auto

lemma unfolding_next_step_equivalent:
"w ⊨⇩n (Unf φ)[X]⇩ν ⟹ suffix 1 w ⊨⇩n (af_letter φ (w 0))[X]⇩ν"
proof (induction φ)
case (Next_ltln φ)
then show ?case
unfolding Unf.simps by (metis GF_advice_af_letter build_split)
next
case (Until_ltln φ1 φ2)
then show ?case
unfolding Unf.simps
next
case (Release_ltln φ1 φ2)
then show ?case
unfolding Unf.simps
next
case (WeakUntil_ltln φ1 φ2)
then show ?case
unfolding Unf.simps
next
case (StrongRelease_ltln φ1 φ2)
then show ?case
unfolding Unf.simps
qed auto

lemma nested_prop_atoms_Unf:
"nested_prop_atoms (Unf φ) ⊆ nested_prop_atoms φ"
by (induction φ) auto

(* TODO move somewhere?? *)
lemma refine_image:
assumes "⋀x y. f x = f y ⟶ g x = g y"
assumes "finite (f ` X)"
shows "finite (g ` X)"
and "card (f ` X) ≥ card (g ` X)"
proof -
obtain Y where "Y ⊆ X" and "finite Y" and Y_def: "f ` X = f ` Y"
using assms by (meson finite_subset_image subset_refl)
moreover
{
fix x
assume "x ∈ X"
then have "g x ∈ g ` Y"
by (metis (no_types, opaque_lifting) ‹x ∈ X› assms(1) Y_def image_iff)
}
then have "g ` X = g ` Y"
using assms ‹Y ⊆ X› by blast
ultimately
show "finite (g ` X)"
by simp

from ‹finite Y› have "card (f ` Y) ≥ card (g ` Y)"
proof (induction Y rule: finite_induct)
case (insert x F)

then have 1: "finite (g ` F)" and 2: "finite (f ` F)"
by simp_all

have "f x ∈ f ` F ⟹ g x ∈ g ` F"
using assms(1) by blast

then show ?case
using insert by (simp add: card_insert_if[OF 1] card_insert_if[OF 2])
qed simp

then show "card (f ` X) ≥ card (g ` X)"
by (simp add: Y_def ‹g ` X = g ` Y›)
qed

lemma abs_ltln⇩P_implies_abs_ltln⇩Q:
"abs_ltln⇩P φ = abs_ltln⇩P ψ ⟶ abs_ltln⇩Q φ = abs_ltln⇩Q ψ"
by (simp add: ltl_prop_equiv_implies_ltl_prop_unfold_equiv ltln⇩P.abs_eq_iff ltln⇩Q.abs_eq_iff)

lemmas prop_unfold_equiv_helper = refine_image[of abs_ltln⇩P abs_ltln⇩Q, OF abs_ltln⇩P_implies_abs_ltln⇩Q]

lemma prop_unfold_equiv_finite:
"finite P ⟹ finite {abs_ltln⇩Q ψ |ψ. prop_atoms ψ ⊆ P}"
using prop_unfold_equiv_helper(1)[OF prop_equiv_finite[unfolded image_Collect[symmetric]]]
unfolding image_Collect[symmetric] .

lemma prop_unfold_equiv_card:
"finite P ⟹ card {abs_ltln⇩Q ψ |ψ. prop_atoms ψ ⊆ P} ≤ 2 ^ 2 ^ card P"
using prop_unfold_equiv_helper(2)[OF prop_equiv_finite[unfolded image_Collect[symmetric]]] prop_equiv_card
unfolding image_Collect[symmetric]
by fastforce

lemma Unf_eventually_equivalent:
"w ⊨⇩n Unf φ[X]⇩ν ⟹ ∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν"
by (metis (full_types) One_nat_def foldl.simps(1) foldl.simps(2) subsequence_singleton unfolding_next_step_equivalent)