Theory Contrasimulation

section ‹Contrasimulation›

theory Contrasimulation
imports
  Weak_Relations
begin

context lts_tau
begin

subsection ‹Definition of Contrasimulation›

definition contrasimulation ::
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹contrasimulation R ≡ ∀ p q p' A . (∀ a ∈ set(A). a ≠ τ) ∧ R p q ∧ (p ⇒$ A p') ⟶
    (∃ q'. (q ⇒$ A q') ∧ R q' p')›

lemma contrasim_simpler_def:
  shows ‹contrasimulation R =
    (∀ p q p' A . R p q ∧ (p ⇒$ A p') ⟶ (∃ q'. (q ⇒$ A q') ∧ R q' p'))›
proof -
  have ‹⋀A. ∀a∈set (filter (λa. a ≠ τ) A). a ≠ τ› by auto
  then show ?thesis
    unfolding contrasimulation_def
    using word_steps_ignore_tau_addition word_steps_ignore_tau_removal
    by metis
qed

abbreviation contrasimulated_by :: ‹'s ⇒ 's ⇒ bool› (‹_ ⊑c  _› [60, 60] 65)
  where ‹contrasimulated_by p q ≡ ∃ R . contrasimulation R ∧ R p q›

lemma contrasim_preorder_is_contrasim:
  shows ‹contrasimulation (λ p q . p ⊑c q)›
  unfolding contrasimulation_def
  by metis

lemma contrasim_preorder_is_greatest:
  assumes ‹contrasimulation R›
  shows ‹⋀ p q. R p q ⟹ p ⊑c q›
  using assms by auto

lemma contrasim_tau_step:
  ‹contrasimulation (λ p1 q1 . q1 ⟼* tau p1)›
  unfolding contrasimulation_def
  using steps.simps tau_tau tau_word_concat
  by metis

lemma contrasim_trans_constructive:
  fixes R1 R2
  defines
    ‹R ≡ λ p q . ∃ pq . (R1 p pq ∧ R2 pq q) ∨ (R2 p pq ∧ R1 pq q)›
  assumes
    R1_def: ‹contrasimulation R1› ‹R1 p pq› and
    R2_def: ‹contrasimulation R2› ‹R2 pq q›
  shows
    ‹R p q› ‹contrasimulation R›
  using assms(2,3,4,5) unfolding R_def contrasimulation_def by metis+

lemma contrasim_trans:
  assumes
    ‹p ⊑c pq›
    ‹pq ⊑c q›
  shows
    ‹p ⊑c q›
  using assms contrasim_trans_constructive by blast

lemma contrasim_refl:
  shows
    ‹p ⊑c p›
  using contrasim_tau_step steps.refl by blast

lemma contrasimilarity_equiv:
  defines ‹contrasimilarity ≡ λ p q. p ⊑c q ∧ q ⊑c p›
  shows ‹equivp contrasimilarity›
proof -
  have ‹reflp contrasimilarity›
    using contrasim_refl unfolding contrasimilarity_def reflp_def by blast
  moreover have ‹symp contrasimilarity›
    unfolding contrasimilarity_def symp_def by blast
  moreover have ‹transp contrasimilarity›
    using contrasim_trans unfolding contrasimilarity_def transp_def by meson
  ultimately show ?thesis using equivpI by blast
qed

lemma contrasim_implies_trace_incl:
  assumes ‹contrasimulation R›
  shows ‹trace_inclusion R›
by (metis assms contrasim_simpler_def trace_inclusion_def) 

lemma contrasim_coupled:
  assumes
    ‹contrasimulation R›
    ‹R p q›
  shows
    ‹∃ q'. q ⟼* tau q' ∧ R q' p›
  using assms steps.refl[of p tau] weak_step_seq.simps(1)
  unfolding contrasim_simpler_def by blast

lemma contrasim_taufree_symm:
  assumes
    ‹contrasimulation R›
    ‹R p q›
    ‹stable_state q›
  shows
    ‹R q p›
  using contrasim_coupled assms stable_tauclosure_only_loop by blast

lemma symm_contrasim_is_weak_bisim:
  assumes
    ‹contrasimulation R›
    ‹⋀ p q. R p q ⟹ R q p›
  shows
    ‹weak_bisimulation R›
  using assms unfolding contrasim_simpler_def weak_sim_word weak_bisim_weak_sim by blast

lemma contrasim_weakest_bisim:
  assumes
    ‹contrasimulation R›
    ‹⋀ p q a. p ⟼ a q ⟹ ¬ tau a›
  shows
    ‹bisimulation R›
  using assms contrasim_taufree_symm symm_contrasim_is_weak_bisim weak_bisim_taufree_strong
  by blast

lemma symm_weak_sim_is_contrasim:
  assumes
    ‹weak_simulation R›
    ‹⋀ p q. R p q ⟹ R q p›
  shows
    ‹contrasimulation R›
  using assms unfolding contrasim_simpler_def weak_sim_word by blast

subsection ‹Intermediate Relation Mimicking Contrasim›

definition mimicking :: "('s ⇒ 's set ⇒ bool) ⇒ 's ⇒ 's set ⇒ bool" where 
‹mimicking R p' Q' ≡ ∃p Q A.
  R p Q ∧ p ⇒$A p' ∧ 
  (∀a ∈ set A. a ≠ τ) ∧ 
  Q' = (dsuccs_seq_rec (rev A) Q)›

definition set_lifted :: "('s ⇒ 's ⇒ bool) ⇒ 's ⇒ 's set ⇒ bool" where 
‹set_lifted R p Q ≡ ∃q. R p q ∧ Q = {q}›

lemma R_is_in_mimicking_of_R : 
  assumes ‹R p Q›
  shows ‹mimicking R p Q›
  using assms steps.refl lts_tau.weak_step_seq.simps(1)
  unfolding mimicking_def by fastforce

lemma mimicking_of_C_guarantees_tau_succ:
  assumes
    ‹contrasimulation C›
    ‹mimicking (set_lifted C) p Q›
    ‹p ⇒^τ p'›
  shows ‹∃q'. q' ∈ (weak_tau_succs Q) ∧ mimicking (set_lifted C) q' {p'}›
proof -
  obtain p0 Q0 A q0
      where ‹(set_lifted C) p0 Q0› ‹p0 ⇒$A p› ‹∀a ∈ set A. a ≠ τ› ‹Q0 = {q0}› 
        and Q_def: ‹Q = (dsuccs_seq_rec (rev A) Q0)› 
      using mimicking_def assms set_lifted_def by metis
  hence ‹C p0 q0› using set_lifted_def by auto 
  have ‹p0 ⇒$(A@[τ]) p'› using ‹p0 ⇒$A p›  ‹p ⇒^τ  p'› rev_seq_step_concat by auto
  hence word: ‹p0 ⇒$A p'› 
    by (metis ‹∀a∈set A. a ≠ τ› app_tau_taufree_list tau_def weak_step_over_tau)
  then obtain q' where ‹q0 ⇒$A q'› ‹C q' p'› 
    using assms contrasimulation_def[of ‹C›] ‹C p0 q0› ‹∀a ∈ set A. a ≠ τ› by blast
  hence ‹(set_lifted C) q' {p'}› using set_lifted_def by auto
  hence in_mimicking: ‹mimicking (set_lifted C) q' {p'}› using R_is_in_mimicking_of_R  by auto
  have ‹q' ∈ weak_tau_succs (dsuccs_seq_rec (rev A) Q0)› 
    using ‹Q0 = {q0}› ‹q0 ⇒$ A q'›
    by (simp add: word_reachable_implies_in_dsuccs) 
  hence ‹q' ∈ weak_tau_succs Q› using Q_def by simp 
  thus ‹∃q'. q' ∈ weak_tau_succs Q ∧ mimicking (set_lifted C) q' {p'}› using in_mimicking by auto
qed

lemma mimicking_of_C_guarantees_action_succ:
 assumes 
    ‹contrasimulation C›
    ‹mimicking (set_lifted C) p Q›
    ‹p =⊳a p'›
    ‹a ≠ τ›
  shows ‹mimicking (set_lifted C) p' (dsuccs a Q)›
proof -
  obtain p0 Q0 A q0
    where ‹(set_lifted C) p0 Q0› ‹p0 ⇒$A p› ‹Q0 = {q0}› ‹∀a ∈ set A. a ≠ τ › 
      and Q_def: ‹Q = (dsuccs_seq_rec (rev A) Q0)› 
    using mimicking_def assms set_lifted_def by metis
  then obtain CS where CS_def: ‹contrasimulation CS ∧ CS p0 q0› 
    using assms set_lifted_def by (metis singleton_inject) 
  have notau: ‹∀a ∈ set (A@[a]). a ≠ τ› 
    using ‹a ≠ τ› ‹∀a ∈ set A. a ≠ τ › by auto
  have  ‹p ⇒a  p'› using assms(3,4) steps.refl tau_def by auto 
  hence word: ‹p0 ⇒$(A@[a]) p'›
    using ‹p0 ⇒$A p›  rev_seq_step_concat
    by (meson steps.step steps_concat)
  then obtain q' where ‹q0 ⇒$(A@[a]) q' ∧ CS q' p'› 
    using CS_def contrasimulation_def[of ‹CS›] notau
    by fastforce
  hence ‹q' ∈ weak_tau_succs (dsuccs_seq_rec (rev (A@[a])) {q0})› 
    using word_reachable_implies_in_dsuccs by blast
  then obtain q1 where ‹q1 ∈ dsuccs_seq_rec (rev (A@[a])) {q0}› ‹q1 ⇒^τ q'›
    using weak_tau_succs_def[of ‹dsuccs_seq_rec (rev (A@[a])) {q0}›] by auto
  thus ?thesis
    using word mimicking_def[of ‹(set_lifted C)›] ‹(set_lifted C) p0 Q0› 
      ‹Q0 = {q0}› Q_def notau simp_dsuccs_seq_rev by meson
qed

subsection ‹Over-Approximating Contrasimulation by a Single-Step Version›

definition contrasim_step ::
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹contrasim_step R ≡ ∀ p q p' a .
    R p q ∧ (p ⇒^a p') ⟶
    (∃ q'. (q ⇒^a q')
         ∧ R q' p')›

lemma contrasim_step_weaker_than_seq:
  assumes
    ‹contrasimulation R›
  shows
    ‹contrasim_step R›
  unfolding contrasim_step_def
proof ((rule allI impI)+)
  fix p q p' a
  assume
    ‹R p q ∧ p ⇒^a  p'›
  hence
    ‹R p q› ‹p ⇒^a  p'› by safe
  hence ‹p ⇒$ [a]  p'› by safe
  then obtain q' where ‹R q' p'› ‹q ⇒$ [a]  q'›
    using assms `R p q` unfolding contrasim_simpler_def by blast
  hence ‹q ⇒^a  q'› by blast
  thus ‹∃q'. q ⇒^a  q' ∧ R q' p'› using `R q' p'` by blast
qed

lemma contrasim_step_seq_coincide_for_sims:
  assumes
    ‹contrasim_step R›
    ‹weak_simulation R›
  shows
    ‹contrasimulation R›
  unfolding contrasimulation_def
proof (clarify)
  fix p q p' A
  assume
    ‹R p q›
    ‹p ⇒$ A  p'›
  thus ‹∃q'. q ⇒$ A  q' ∧ R q' p'›
  proof (induct A arbitrary: p p' q)
    case Nil
    then show ?case using assms(1) unfolding contrasim_step_def
      using tau_tau weak_step_seq.simps(1) by blast
  next
    case (Cons a A)
    then obtain p1 where p1_def: ‹p ⇒^a p1› ‹p1 ⇒$ (A)  p'› by auto
    then obtain q1 where q1_def: ‹q ⇒^a q1› ‹R p1 q1›
      using assms(2) `R p q` unfolding weak_sim_weak_premise by blast
    then obtain q' where ‹q1 ⇒$ (A)  q'› ‹R q' p'› using p1_def(2) Cons(1) by blast
    then show ?case using q1_def(1) by auto
  qed
qed

end
end