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" (‹_ ⟹⇧^_ ≺ _› [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