Theory Extra_Equivalence_Relations

(*
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹Additional Equivalence Relations›

theory Extra_Equivalence_Relations
imports
  LTL.LTL LTL.Equivalence_Relations After Advice
begin

subsection ‹Propositional Equivalence with Implicit LTL Unfolding›

fun Unf :: "'a ltln ⇒ 'a ltln"
where
  "Unf (φ Un ψ) = ((φ Un ψ) andn Unf φ) orn Unf ψ"
| "Unf (φ Wn ψ) = ((φ Wn ψ) andn Unf φ) orn Unf ψ"
| "Unf (φ Mn ψ) = ((φ Mn ψ) orn Unf φ) andn Unf ψ"
| "Unf (φ Rn ψ) = ((φ Rn ψ) orn Unf φ) andn Unf ψ"
| "Unf (φ andn ψ) = Unf φ andn Unf ψ"
| "Unf (φ orn ψ) = Unf φ orn 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 φ"
  by (simp add: Unf_sound ltl_lang_equiv_def)

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 ltlnQ = "'a ltln" / "(∼Q)"
  by (rule ltl_prop_unfold_equiv_equivp)

instantiation ltlnQ :: (type) equal
begin

lift_definition ltlnQ_eq_test :: "'a ltlnQ ⇒ 'a ltlnQ ⇒ bool" is "λx y. x ∼Q y"
  by (metis ltlnQ.abs_eq_iff)

definition
  eqQ: "equal_class.equal ≡ ltlnQ_eq_test"

instance
  by (standard; simp add: eqQ ltlnQ_eq_test.rep_eq, metis Quotient_ltlnQ 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 ψ) ν"
    by (simp add: prop_af_congruent.af_letter_congruent)
  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

lemma GF_advice_prop_unfold_congruent:
  assumes "φ ∼Q ψ"
  shows "(Unf φ)[X]ν ∼Q (Unf ψ)[X]ν"
proof -
  have "Unf φ ∼P Unf ψ"
    using assms
    by (simp add: ltl_prop_unfold_equiv_def ltl_prop_equiv_def)
  then have "(Unf φ)[X]ν ∼P (Unf ψ)[X]ν"
    by (simp add: GF_advice_prop_congruent(2))
  then show "(Unf φ)[X]ν ∼Q (Unf ψ)[X]ν"
    by (simp add: ltl_prop_equiv_implies_ltl_prop_unfold_equiv)
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 Un φ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 Mn φ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
    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(8) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
next
  case (Release_ltln φ1 φ2)
  then show ?case
    unfolding Unf.simps
    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter One_nat_def af_letter.simps(9) build_first semantics_ltln.simps(5) semantics_ltln.simps(6))
next
  case (WeakUntil_ltln φ1 φ2)
  then show ?case
    unfolding Unf.simps
    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(10) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
next
  case (StrongRelease_ltln φ1 φ2)
  then show ?case
    unfolding Unf.simps
    by (metis GF_advice.simps(2) GF_advice.simps(3) GF_advice_af_letter af_letter.simps(11) build_split semantics_ltln.simps(5) semantics_ltln.simps(6))
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_ltlnP_implies_abs_ltlnQ:
  "abs_ltlnP φ = abs_ltlnP ψ ⟶ abs_ltlnQ φ = abs_ltlnQ ψ"
  by (simp add: ltl_prop_equiv_implies_ltl_prop_unfold_equiv ltlnP.abs_eq_iff ltlnQ.abs_eq_iff)

lemmas prop_unfold_equiv_helper = refine_image[of abs_ltlnP abs_ltlnQ, OF abs_ltlnP_implies_abs_ltlnQ]

lemma prop_unfold_equiv_finite:
  "finite P ⟹ finite {abs_ltlnQ ψ |ψ. 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_ltlnQ ψ |ψ. 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)

interpretation prop_unfold_GF_advice_compatible: GF_advice_congruent "(∼Q)" Unf
  by unfold_locales (simp_all add: unfolding_prop_unfold_idem prop_unfold_equivalence.eq_sym unfolding_monotonic Unf_eventually_equivalent GF_advice_prop_unfold_congruent)

end