Theory Weak_Sim

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Sim
  imports Weak_Semantics Strong_Sim
begin

definition weakSimulation :: "ccs ⇒ (ccs × ccs) set ⇒ ccs ⇒ bool"   (‹_ ↝⇧^<_> _› [80, 80, 80] 80)
where
  "P ↝⇧^<Rel> Q ≡ ∀a Q'. Q ⟼a ≺ Q' ⟶ (∃P'. P ⟹⇧^a ≺ P' ∧ (P', Q') ∈ Rel)"

lemma weakSimI[case_names Sim]:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "⋀α Q'. Q ⟼α ≺ Q' ⟹ ∃P'. P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel"

  shows "P ↝⇧^<Rel> Q"
using assms
by(auto simp add: weakSimulation_def)

lemma weakSimE:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   α   :: act
  and   Q'  :: ccs

  assumes "P ↝⇧^<Rel> Q"
  and     "Q ⟼α ≺ Q'"

  obtains P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
using assms
by(auto simp add: weakSimulation_def)

lemma simTauChain:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   Q'  :: ccs

  assumes "Q ⟹⇩τ Q'"
  and     "(P, Q) ∈ Rel"
  and     Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝⇧^<Rel> S"

  obtains P' where "P ⟹⇩τ P'" and "(P', Q') ∈ Rel"
using ‹Q ⟹⇩τ Q'› ‹(P, Q) ∈ Rel›
proof(induct arbitrary: thesis rule: tauChainInduct)
  case Base
  from ‹(P, Q) ∈ Rel› show ?case
    by(force intro: Base)
next
  case(Step Q'' Q')
  from ‹(P, Q) ∈ Rel› obtain P'' where "P ⟹⇩τ P''" and "(P'', Q'') ∈ Rel"
    by(blast intro: Step)
  from ‹(P'', Q'') ∈ Rel› have "P'' ↝⇧^<Rel> Q''" by(rule Sim)
  then obtain P' where "P'' ⟹⇧^τ ≺ P'" and "(P', Q') ∈ Rel" using ‹Q'' ⟼τ ≺ Q'› by(rule weakSimE)
  with ‹P ⟹⇩τ P''› show thesis
    by(force simp add: weakTrans_def weakCongTrans_def intro: Step)
qed

lemma simE2:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   α   :: act
  and   Q'  :: ccs

  assumes "(P, Q) ∈ Rel"
  and     "Q ⟹⇧^α ≺ Q'"
  and     Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝⇧^<Rel> S"
  
  obtains P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
proof -
  assume Goal: "⋀P'. ⟦P ⟹⇧^α ≺ P'; (P', Q') ∈ Rel⟧ ⟹ thesis"
  moreover from ‹Q ⟹⇧^α ≺ Q'› have "∃P'. P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel"
  proof(induct rule: weakTransCases)
    case Base
    from ‹(P, Q) ∈ Rel› show ?case by force
  next
    case Step
    from ‹Q ⟹α ≺ Q'› obtain Q''' Q''
    where QChain: "Q ⟹⇩τ Q'''" and Q'''Trans: "Q''' ⟼α ≺ Q''" and Q''Chain: "Q'' ⟹⇩τ Q'"
      by(rule weakCongTransE)
    from QChain ‹(P, Q) ∈ Rel› Sim obtain P''' where PChain: "P ⟹⇩τ P'''" and "(P''', Q''') ∈ Rel"
      by(rule simTauChain)
    from ‹(P''', Q''') ∈ Rel› have "P''' ↝⇧^<Rel> Q'''" by(rule Sim)
    then obtain P'' where P'''Trans: "P''' ⟹⇧^α ≺ P''" and "(P'', Q'') ∈ Rel" using Q'''Trans by(rule weakSimE)
    from Q''Chain ‹(P'', Q'') ∈ Rel› Sim obtain P' where P''Chain: "P'' ⟹⇩τ P'" and "(P', Q') ∈ Rel"
      by(rule simTauChain)
    from P'''Trans P''Chain Step show ?thesis
    proof(induct rule: weakTransCases)
      case Base
      from PChain ‹P''' ⟹⇩τ P'› have "P ⟹⇧^τ ≺ P'"
      proof(induct rule: tauChainInduct)
        case Base
        from ‹P ⟹⇩τ P'› show ?case
        proof(induct rule: tauChainInduct)
          case Base
          show ?case by simp
        next
          case(Step P' P'')
          thus ?case by(fastforce simp add: weakTrans_def weakCongTrans_def)
        qed
      next
        case(Step P''' P'')
        thus ?case by(fastforce simp add: weakTrans_def weakCongTrans_def)
      qed
      with ‹(P', Q') ∈ Rel› show ?case by blast
    next
      case Step
      thus ?case using ‹(P', Q') ∈ Rel› PChain
        by(rule_tac x=P' in exI) (force simp add: weakTrans_def weakCongTrans_def)
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma reflexive:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "Id ⊆ Rel"

  shows "P ↝⇧^<Rel> P"
using assms
by(auto simp add: weakSimulation_def intro: transitionWeakCongTransition weakCongTransitionWeakTransition)
  
lemma transitive:
  fixes P     :: ccs
  and   Rel   :: "(ccs × ccs) set"
  and   Q     :: ccs
  and   Rel'  :: "(ccs × ccs) set"
  and   R     :: ccs
  and   Rel'' :: "(ccs × ccs) set"
  
  assumes "(P, Q) ∈ Rel"
  and     "Q ↝⇧^<Rel'> R"
  and     "Rel O Rel' ⊆ Rel''"
  and     "⋀S T. (S, T) ∈ Rel ⟹ S ↝⇧^<Rel> T"
  
  shows "P ↝⇧^<Rel''> R"
proof(induct rule: weakSimI)
  case(Sim α R')
  thus ?case using assms
    apply(drule_tac Q=R in weakSimE, auto)
    by(drule_tac Q=Q in simE2, auto)
qed

lemma weakMonotonic:
  fixes P :: ccs
  and   A :: "(ccs × ccs) set"
  and   Q :: ccs
  and   B :: "(ccs × ccs) set"

  assumes "P ↝⇧^<A> Q"
  and     "A ⊆ B"

  shows "P ↝⇧^<B> Q"
using assms
by(fastforce simp add: weakSimulation_def)

lemma simWeakSim:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "P ↝[Rel] Q"
  
  shows "P ↝⇧^<Rel> Q"
using assms
by(rule_tac weakSimI, auto)
  (blast dest: simE transitionWeakTransition)

end