Theory Strong_Equivalences

section ‹Strong Equivalences›

theory Strong_Equivalences
  imports Labeled_Transition_Systems
begin

context lts begin

subsection ‹Trivial notions of equality›

subsubsection ‹Identity›

definition identical :: ‹'s ⇒ 's ⇒ bool›
  where ‹identical p q ≡ p = q›

text ‹It's reflexive›
lemma identical_reflexive:
  shows ‹identical p p›
  unfolding identical_def using refl .

lemma non_identity:
  assumes ‹p ≠ q›
  shows ‹¬ identical p q›
  using assms unfolding identical_def .

text ‹It's an equivalence.›
lemma identity_equivalence:
  shows ‹equivp identical›
proof (rule equivpI)
  show ‹reflp identical› unfolding reflp_def using allI identical_reflexive . (* by simp *)
next
  show ‹symp identical› unfolding symp_def
  proof (rule+)
    fix x y
    assume ‹identical x y›
    then have ‹x = y› unfolding identical_def .
    with sym have ‹y = x› .
    then show ‹identical y x› unfolding identical_def .
  qed
next
  show ‹transp identical›
    unfolding transp_def identical_def by blast
qed

subsubsection ‹Universal equality›

definition universal_equal :: ‹'s ⇒ 's ⇒ bool›
  where ‹universal_equal p q ≡ True›

lemma universal_equal_equivalence:
  shows ‹equivp universal_equal›
  unfolding equivp_def universal_equal_def by simp

subsection ‹Trace Equality›

text ‹Trace preorder as inclusion of trace sets›
definition trace_preordered :: ‹'s ⇒ 's ⇒ bool› (infix ‹≲T› 80) where
    ‹p ≲T q ≡ traces p ⊆ traces q›

text ‹Trace equivalence as mutual preorder›
abbreviation trace_equivalent (infix ‹≃T› 80) where
  ‹p ≃T q ≡ p ≲T q ∧ q ≲T p›

text ‹Trace preorder is transitive›
lemma trace_preorder_transitive:
  shows ‹transp (≲T)›
  unfolding trace_preordered_def
by (standard, blast)

lemma trace_equivalence_equiv:
  shows ‹equivp trace_equivalent›
proof (rule equivpI)
  show ‹transp trace_equivalent›
    using trace_preorder_transitive
    unfolding transp_def
    by blast
next
  show ‹reflp trace_equivalent›
    unfolding reflp_def trace_preordered_def by blast
next
  show ‹symp trace_equivalent›
    unfolding symp_def trace_preordered_def by blast
qed

subsection ‹Isomorphism›

definition isomorphism :: ‹('s ⇒ 's) ⇒ bool›
  where ‹isomorphism f ≡ bij f ∧ (∀p p' a. p ⟼ a p' ⟷ (f p) ⟼ a (f p'))›

definition is_isomorphic_to (infix ‹≃ISO› 80)
  where ‹p ≃ISO q ≡ ∃f. f p = q ∧ isomorphism f›

text ‹Isomorphism yields an equivalence›

lemma iso_equivalence_equiv:
  shows ‹equivp is_isomorphic_to›
proof (rule equivpI)
  show ‹reflp is_isomorphic_to›
    unfolding reflp_def is_isomorphic_to_def isomorphism_def by (metis bij_id id_apply)
next
  show ‹symp is_isomorphic_to›
    unfolding symp_def is_isomorphic_to_def isomorphism_def by (metis (no_types, opaque_lifting) bij_iff)
next
  show ‹transp is_isomorphic_to›
    unfolding transp_def is_isomorphic_to_def
  proof safe
    fix p f1 f2
    assume ‹isomorphism f1› ‹isomorphism f2›
    then have ‹isomorphism (f2 ∘ f1)› unfolding isomorphism_def using bij_comp by auto
    then show ‹∃fb. fb p = f2 (f1 p) ∧ isomorphism fb› unfolding comp_def by auto
  qed
qed

text ‹Isomorphism equivalence is closed under steps
  (i.e. isomorphism equivalence is a simulation, but we have not yet defined this notion.)
›
lemma iso_sim:
  assumes
    ‹is_isomorphic_to p q›
    ‹p ⟼ a p'›
  shows ‹∃q'. q ⟼ a q' ∧ is_isomorphic_to p' q'›
using assms unfolding is_isomorphic_to_def isomorphism_def by blast

text ‹Isomorphic states have the same traces.›
text ‹Teaching hint: Inductive proofs›

lemma iso_implies_trace_preord:
  assumes ‹is_isomorphic_to p q›
  shows ‹trace_preordered p q›
  unfolding trace_preordered_def
proof safe
  fix tr p'
  assume ‹p ⟼$tr p'›
  thus ‹∃p'. q ⟼$tr p'› using assms
  proof (induct tr arbitrary: p q p')
    case Nil
    then show ?case using empty_trace_trivial by blast
  next
    case (Cons a tr p q p')
    from ‹p ⟼$(a # tr) p'›
      obtain p'' where ‹p ⟼a p''› ‹p'' ⟼$ tr p'›
      by (cases, auto)
    then show ?case
      using iso_sim[OF ‹is_isomorphic_to p q› ‹p ⟼a p''›]
        Cons(1) sstep by blast
  qed
qed
―‹Actually, this is more like a corollary of later lemmas.›

corollary iso_implies_trace_eq:
  assumes ‹is_isomorphic_to p q›
  shows ‹trace_equivalent p q›
  using assms iso_implies_trace_preord iso_equivalence_equiv
  unfolding equivp_def by simp

subsection ‹Simulation preorder and equivalence›

text ‹Two states are simulation preordered if they can be related by
  a simulation relation.›

definition simulation
  where ‹simulation R ≡
    ∀p q a p'. p ⟼ a p' ∧ R p q ⟶ (∃q'. q ⟼ a q' ∧ R p' q')›

definition simulated_by (infix ‹≲S› 80)
  where ‹p ≲S q ≡ ∃R. R p q ∧ simulation R›

abbreviation similar (infix ‹≃S› 80)
  where ‹p ≃S q ≡ p ≲S q ∧ q ≲S p›

lemma id_sim:
  shows ‹simulation identical›
  unfolding simulation_def identical_def by blast

lemma simulation_composition:
  assumes
    ‹simulation R1›
    ‹simulation R2›
  shows
    ‹simulation (λp q. ∃p'. R1 p p' ∧ R2 p' q)›
  using assms unfolding simulation_def by blast

lemma simulation_union:
  assumes
    ‹simulation R1›
    ‹simulation R2›
  shows
    ‹simulation (λp q. R1 p q ∨ R2 p q)›
  using assms unfolding simulation_def by blast

lemma simulation_preorder_transitive:
  shows ‹transp (≲S)›
  unfolding transp_def simulated_by_def
  using simulation_composition
  by (metis (mono_tags, lifting))

lemma iso_is_sim:
  shows ‹simulation is_isomorphic_to›
  using iso_sim unfolding simulated_by_def simulation_def by blast

corollary iso_implies_sim:
  assumes ‹is_isomorphic_to p q›
  shows ‹simulated_by p q›
  using assms iso_is_sim unfolding simulated_by_def by blast

lemma sim_implies_trace_preord:
  assumes ‹p ≲S q›
  shows ‹p ≲T q›
  unfolding trace_preordered_def
proof safe
  fix tr p'
  assume ‹p ⟼$tr p'›
  thus ‹∃p'. q ⟼$tr p'› using assms
  proof (induct tr arbitrary: p q p')
    case Nil
    then show ?case using empty_trace_trivial by blast
  next
    case (Cons a tr p q p')
    from ‹p ⟼$(a # tr) p'›
      obtain p'' where p''_spec: ‹p ⟼a p''› ‹p'' ⟼$ tr p'›
      by (cases, auto)
    then obtain R q' where ‹simulation R› ‹R p q› ‹R p'' q'›
      using Cons unfolding simulated_by_def simulation_def by blast
    then show ?case
      using Cons step_sequence.sstep p''_spec
        simulated_by_def simulation_def by metis
  qed
qed


lemma sim_eq_implies_trace_eq:
  assumes ‹p ≃S q›
  shows ‹p ≃T q›
  using assms sim_implies_trace_preord by blast

text ‹Two states are bisimilar if they can be related by a symmetric simulation.›
definition bisimilar (infix ‹≃B› 80) where
  ‹bisimilar p q ≡ ∃R. simulation R ∧ symp R ∧ R p q›

text ‹Bisimilarity is a simulation.›
lemma bisim_sim:
  shows ‹simulation bisimilar›
  unfolding bisimilar_def simulation_def by blast

lemma bisimilarity_equiv:
  shows ‹equivp (≃B)›
proof (rule equivpI)
  show ‹reflp (≃B)›
    using id_sim DEADID.rel_symp
    unfolding bisimilar_def identical_def
    by (metis (mono_tags, lifting) reflpI)
next
  show ‹symp (≃B)›
    unfolding bisimilar_def
    by (smt (verit, best) sympE sympI)
next
  show ‹transp (≃B)›
    unfolding transp_def bisimilar_def
  proof safe
    fix p p' q R1 R2
    assume case_assms:
      ‹simulation R1› ‹symp R1› ‹R1 p p'›
      ‹simulation R2› ‹symp R2› ‹R2 p' q›
    hence ‹simulation (λp q. (∃p'. R1 p p' ∧ R2 p' q) ∨ (∃p'. R2 p p' ∧ R1 p' q))›
      using simulation_composition simulation_union by blast
    moreover have
      ‹symp (λp q. (∃p'. R1 p p' ∧ R2 p' q) ∨ (∃p'. R2 p p' ∧ R1 p' q))›
      using case_assms(2,5) unfolding symp_def by blast
    ultimately show ‹∃R. simulation R ∧ symp R ∧ R p q›
      using case_assms(3,6) by blast
  qed
qed

text ‹Bisimilarity is a bisimulation.›
lemma bisim_bisim:
  shows ‹simulation bisimilar ∧ symp bisimilar›
  using bisim_sim bisimilarity_equiv equivpE by blast

lemma bisim_implies_sim:
  assumes ‹p ≃B q›
  shows ‹p ≃S q›
  using assms bisim_bisim
  unfolding simulated_by_def
  by (metis sympE)

lemma iso_implies_bisim:
  assumes ‹p ≃ISO q›
  shows ‹p ≃B q›
using assms iso_is_sim equivpE[OF iso_equivalence_equiv] bisimilar_def by blast

end

end