Theory Contrasimulation

section ‹Contrasimulation›

theory Contrasimulation
imports
  Weak_Relations
begin

context lts_tau
begin

subsection ‹Definition of Contrasimulation›

definition contrasim ::
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹contrasim 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 ‹contrasim 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 contrasim_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 . contrasim R ∧ R p q›

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

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

lemma contrasim_tau_step:
  ‹contrasim (λ p1 q1 . q1 ⟼* tau p1)›
  unfolding contrasim_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: ‹contrasim R1› ‹R1 p pq› and
    R2_def: ‹contrasim R2› ‹R2 pq q›
  shows
    ‹R p q› ‹contrasim R›
  using assms(2,3,4,5) unfolding R_def contrasim_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 contrasim_coupled:
  assumes
    ‹contrasim 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
    ‹contrasim 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
    ‹contrasim 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
    ‹contrasim 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
    ‹contrasim R›
  using assms unfolding contrasim_simpler_def weak_sim_word by blast

subsection ‹Intermediate Relation Mimicking Contrasim›

definition F :: "(('s ⇒ ('s set) ⇒ bool)) ⇒ ('s ⇒ ('s set) ⇒ bool)" where 
‹F 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_type :: "('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ ('s set) ⇒ bool)" where 
‹set_type R p Q ≡ ∃q. R p q ∧ Q = {q}›

lemma R_is_in_F_of_R : 
  assumes ‹R p Q›
  shows ‹F R p Q›
proof -
  have Q_cond: ‹Q = dsuccs_seq_rec (rev []) Q›  by simp 
  have p_cond: ‹p ⇒$[] p› using steps.simps weak_step_seq.simps(1) by blast 
  thus ‹F R p Q› using Q_cond F_def ‹R p Q›
    by (metis bex_empty empty_set tau_tau)
qed

lemma F_of_C_guarantees_tau_succ:
  assumes 
    ‹contrasim C›
    ‹F (set_type C) p Q›
    ‹p ⇒^τ p'›
  shows ‹∃q'. q' ∈ (weak_tau_succs Q) ∧ F (set_type C) q' {p'}›
proof -
  obtain p0 Q0 A q0
      where ‹(set_type C) p0 Q0› ‹p0 ⇒$A p› ‹∀a ∈ set A. a ≠ τ› ‹Q0 = {q0}› 
        and Q_def: ‹Q = (dsuccs_seq_rec (rev A) Q0)› 
      using F_def assms set_type_def by metis
  hence ‹C p0 q0› using set_type_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 contrasim_def[of ‹C›] ‹C p0 q0› ‹∀a ∈ set A. a ≠ τ› by blast
  hence ‹(set_type C) q' {p'}› using set_type_def by auto
  hence inF: ‹F (set_type C) q' {p'}› using R_is_in_F_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 ∧ F (set_type C) q' {p'}› using inF by auto
qed

lemma F_of_C_guarantees_action_succ :
 assumes 
    ‹contrasim C›
    ‹F (set_type C) p Q›
    ‹p =⊳a p'›
    ‹a ≠ τ›
  shows ‹F (set_type C) p' (dsuccs a Q)›
proof -
  obtain p0 Q0 A q0
    where ‹(set_type C) p0 Q0› ‹p0 ⇒$A p› ‹Q0 = {q0}› ‹∀a ∈ set A. a ≠ τ › 
      and Q_def: ‹Q = (dsuccs_seq_rec (rev A) Q0)› 
    using F_def assms set_type_def by metis
  then obtain CS where CS_def: ‹contrasim CS ∧ CS p0 q0› 
    using assms set_type_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 contrasim_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 F_def[of ‹(set_type C)›] ‹(set_type C) p0 Q0› 
      ‹Q0 = {q0}› Q_def notau simp_dsuccs_seq_rev by meson
qed

end
end