SSL Weak_Semantics.thy

(* 
   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" (‹_ ==>^{^}_ ≺ _› [80, 80, 80] 80)
  where "P ==>^{^}α ≺ P' ≡ P ==>α ≺ P' ∨ (α = τ ∧ P = P')"

lemma weakEmptyTrans[simp]:
  fixes P :: ccs

  shows "P ==>^{^}τ ≺ 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 ==>^{^}α ≺ P'"
  and     "[α = τ; P = P'] ==> Prop (τ) P"
  and     "P ==>α ≺ 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 ==>α ≺ P'"

  shows "P ==>^{^}α ≺ P'"
using assms
by(auto simp add: weakTrans_def)

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

  assumes "P ⟼α ≺ P'"

  shows "P ==>^{^}α ≺ P'"
using assms
by(auto dest: transitionWeakCongTransition weakCongTransitionWeakTransition)

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

  shows "α.(P) ==>^{^}α ≺ P"
by(auto simp add: weakTrans_def intro: weakCongAction)

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

  assumes "P ==>^{^}α ≺ P'"
  and     "P ≠ P'"

  shows "P ⊕ Q ==>^{^}α ≺ 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 ==>^{^}α ≺ Q'"
  and     "Q ≠ Q'"

  shows "P ⊕ Q ==>^{^}α ≺ 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 ==>^{^}α ≺ P'"

  shows "P ∥ Q ==>^{^}α ≺ P' ∥ 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 ==>^{^}α ≺ Q'"

  shows "P ∥ Q ==>^{^}α ≺ P ∥ 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 ==>^{^}α ≺ P'"
  and     "Q ==>^{^}(coAction α) ≺ Q'"
  and     "α ≠ τ"

  shows "P ∥ Q ==>^{^}τ ≺ P' ∥ 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 ==>^{^}α ≺ P'"
  and     "x ♯ α"

  shows "(νx)P ==>^{^}α ≺ (νx)P'"
using assms
by(auto simp add: weakTrans_def intro: weakCongRes)

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

  assumes "P ∥ !P ==>^{^}α ≺ P'"
  and     "P' ≠ P ∥ !P"

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

end