Theory Weak_Semantics

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

definition weakTrans :: "ccs => act => ccs => bool" ("_ ==>⇧^_ \<prec> _" [80, 80, 80] 80)
  where "P ==>⇧^α \<prec> P' ≡ P ==>α \<prec> P' ∨ (α = τ ∧ P = P')"

lemma weakEmptyTrans[simp]:
  fixes P :: ccs

  shows "P ==>⇧^τ \<prec> P"
by(auto simp add: weakTrans_def)

lemma weakTransCases[consumes 1, case_names Base Step]:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P ==>⇧^α \<prec> P'"
  and     "[|α = τ; P = P'|] ==> Prop (τ) P"
  and     "P ==>α \<prec> P' ==> Prop α P'"

  shows "Prop α P'"
using assms
by(auto simp add: weakTrans_def)

lemma weakCongTransitionWeakTransition:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P ==>α \<prec> P'"

  shows "P ==>⇧^α \<prec> P'"
using assms
by(auto simp add: weakTrans_def)

lemma transitionWeakTransition:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P \<longmapsto>α \<prec> P'"

  shows "P ==>⇧^α \<prec> P'"
using assms
by(auto dest: transitionWeakCongTransition weakCongTransitionWeakTransition)

lemma weakAction:
  fixes a :: name
  and   P :: ccs

  shows "α.(P) ==>⇧^α \<prec> P"
by(auto simp add: weakTrans_def intro: weakCongAction)

lemma weakSum1:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>⇧^α \<prec> P'"
  and     "P ≠ P'"

  shows "P ⊕ Q ==>⇧^α \<prec> P'"
using assms
by(auto simp add: weakTrans_def intro: weakCongSum1)

lemma weakSum2:
  fixes Q  :: ccs
  and   α  :: act
  and   Q' :: ccs
  and   P  :: ccs

  assumes "Q ==>⇧^α \<prec> Q'"
  and     "Q ≠ Q'"

  shows "P ⊕ Q ==>⇧^α \<prec> Q'"
using assms
by(auto simp add: weakTrans_def intro: weakCongSum2)

lemma weakPar1:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>⇧^α \<prec> P'"

  shows "P \<parallel> Q ==>⇧^α \<prec> P' \<parallel> Q"
using assms
by(auto simp add: weakTrans_def intro: weakCongPar1)

lemma weakPar2:
  fixes Q  :: ccs
  and   α  :: act
  and   Q' :: ccs
  and   P  :: ccs

  assumes "Q ==>⇧^α \<prec> Q'"

  shows "P \<parallel> Q ==>⇧^α \<prec> P \<parallel> Q'"
using assms
by(auto simp add: weakTrans_def intro: weakCongPar2)

lemma weakSync:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>⇧^α \<prec> P'"
  and     "Q ==>⇧^(coAction α) \<prec> Q'"
  and     "α ≠ τ"

  shows "P \<parallel> Q ==>⇧^τ \<prec> P' \<parallel> Q'"
using assms
by(auto simp add: weakTrans_def intro: weakCongSync)

lemma weakRes:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   x  :: name

  assumes "P ==>⇧^α \<prec> P'"
  and     "x \<sharp> α"

  shows "(|νx|)),P ==>⇧^α \<prec> (|νx|)),P'"
using assms
by(auto simp add: weakTrans_def intro: weakCongRes)

lemma weakRepl:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P \<parallel> !P ==>⇧^α \<prec> P'"
  and     "P' ≠ P \<parallel> !P"

  shows "!P ==>α \<prec> P'"
using assms
by(auto simp add: weakTrans_def intro: weakCongRepl)

end