Theory Weak_Early_Semantics

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Semantics
  imports Weak_Early_Step_Semantics
begin

definition weakFreeTransition :: "pi ⇒ freeRes ⇒ pi ⇒ bool" (‹_ ⟹⇧^_ ≺ _› [80, 80, 80] 80) 
  where "P ⟹⇧^α ≺ P' ≡ P ⟹α ≺ P' ∨ (α = τ ∧ P = P')"

lemma weakTransitionI:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  shows "P ⟹α ≺ P' ⟹ P ⟹⇧^α ≺ P'"
  and   "P ⟹⇧^τ ≺ P"
by(auto simp add: weakFreeTransition_def)

lemma transitionCases[consumes 1, case_names Step Stay]:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "P ⟹⇧^α ≺ P'"
  and     "P ⟹α ≺ P' ⟹ F α P'"
  and     "F (τ) P"

  shows "F α P'"
using assms
by(auto simp add: weakFreeTransition_def)

lemma singleActionChain:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "P ⟼α ≺ P'"

  shows "P ⟹⇧^α ≺ P'"
using assms
by(auto dest: singleActionChain intro: weakTransitionI)

lemma Tau:
  fixes P :: pi

  shows "τ.(P) ⟹⇧^ τ ≺  P"
by(auto intro: Weak_Early_Step_Semantics.Tau
   simp add: weakFreeTransition_def)

lemma Input:
  fixes a :: name
  and   x :: name
  and   u :: name
  and   P :: pi

  shows "a<x>.P ⟹⇧^ a<u> ≺ P[x::=u]"
by(auto intro: Weak_Early_Step_Semantics.Input
   simp add: weakFreeTransition_def)
  
lemma Output:
  fixes a :: name
  and   b :: name
  and   P :: pi

  shows "a{b}.P ⟹⇧^a[b] ≺ P"
by(auto intro: Weak_Early_Step_Semantics.Output
   simp add: weakFreeTransition_def)

lemma Par1F:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   Q  :: pi

  assumes "P ⟹⇧^α ≺ P'"

  shows "P ∥ Q ⟹⇧^α ≺ (P' ∥ Q)"
using assms
by(auto intro: Weak_Early_Step_Semantics.Par1F
   simp add: weakFreeTransition_def residual.inject)

lemma Par2F:
  fixes Q :: pi
  and   α  :: freeRes
  and   Q' :: pi
  and   P  :: pi

  assumes QTrans: "Q ⟹⇧^α ≺ Q'"

  shows "P ∥ Q ⟹⇧^α ≺ (P ∥ Q')"
using assms
by(auto intro: Weak_Early_Step_Semantics.Par2F
   simp add: weakFreeTransition_def residual.inject)


lemma ResF:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   x  :: name

  assumes "P ⟹⇧^α ≺ P'"
  and     "x ♯ α"

  shows "<νx>P ⟹⇧^α ≺ <νx>P'"
using assms
by(auto intro: Weak_Early_Step_Semantics.ResF
   simp add: weakFreeTransition_def residual.inject)

lemma Bang:
  fixes P  :: pi
  and   Rs :: residual

  assumes "P ∥ !P ⟹⇧^α ≺ P'"
  and     "P' ≠ P ∥ !P"
  
  shows "!P ⟹⇧^α ≺ P'"
using assms
by(auto intro: Weak_Early_Step_Semantics.Bang
   simp add: weakFreeTransition_def residual.inject)

lemma tauTransitionChain[simp]:
  fixes P  :: pi
  and   P' :: pi

  shows "P ⟹⇧^τ ≺ P' = P ⟹⇩τ P'"
apply(auto dest: Weak_Early_Step_Semantics.tauTransitionChain
      simp add: weakFreeTransition_def)
by(erule rtrancl.cases) (auto intro: transitionI)

lemma tauStepTransitionChain[simp]:
  fixes P  :: pi
  and   P' :: pi

  assumes "P ≠ P'"

  shows "P ⟹τ ≺ P' = P ⟹⇩τ P'"
using assms
apply(auto dest: Weak_Early_Step_Semantics.tauTransitionChain
      simp add: weakFreeTransition_def)
by(erule rtrancl.cases) (auto intro: transitionI)

lemma chainTransitionAppend:
  fixes P   :: pi
  and   P'  :: pi
  and   Rs  :: residual
  and   a   :: name
  and   x   :: name
  and   P'' :: pi
  and   α   :: freeRes

  shows "P ⟹⇩τ P'' ⟹ P'' ⟹⇧^α ≺ P'  ⟹ P ⟹⇧^α ≺ P'"
  and   "P ⟹⇧^α ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹⇧^α ≺ P'"
by(auto intro: chainTransitionAppend simp add: weakFreeTransition_def dest: Weak_Early_Step_Semantics.tauTransitionChain)

lemma freshTauTransition:
  fixes P :: pi
  and   c :: name

  assumes "P ⟹⇧^τ ≺ P'"
  and     "c ♯ P"

  shows "c ♯ P'"
using assms
by(auto intro: Weak_Early_Step_Semantics.freshTauTransition
   simp add: weakFreeTransition_def residual.inject)

lemma freshOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟹⇧^a[b] ≺ P'"
  and     "c ♯ P"

  shows "c ♯ P'"
using assms
by(auto intro: Weak_Early_Step_Semantics.freshOutputTransition
   simp add: weakFreeTransition_def residual.inject)

lemma eqvtI:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   p  :: "name prm"

  assumes "P ⟹⇧^α ≺ P'"

  shows "(p ∙ P) ⟹⇧^(p ∙ α) ≺ (p ∙ P')"
using assms
by(auto intro: Weak_Early_Step_Semantics.eqvtI
   simp add: weakFreeTransition_def residual.inject)

lemma freshInputTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟹⇧^a<b> ≺ P'"
  and     "c ♯ P"
  and     "c ≠ b"

  shows "c ♯ P'"
using assms
by(auto intro: Weak_Early_Step_Semantics.freshInputTransition
   simp add: weakFreeTransition_def residual.inject)

lemmas freshTransition = freshBoundOutputTransition freshOutputTransition
                         freshInputTransition freshTauTransition

end