Theory Weak_Late_Semantics

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

definition weakTransition :: "(pi × residual) set"
  where "weakTransition ≡ Weak_Late_Step_Semantics.transition ∪ {x. ∃P. x = (P, τ ≺ P)}"

abbreviation weakLateTransition_judge :: "pi ⇒ residual ⇒ bool" (‹_ ⟹⇩l⇧^_› [80, 80] 80)
  where "P ⟹⇩l⇧^Rs ≡ (P, Rs) ∈ weakTransition"

lemma transitionI:
  fixes P  :: pi
  and   Rs :: residual
  and   P' :: pi

  shows "P ⟹⇩l Rs ⟹ P ⟹⇩l⇧^Rs"
  and   "P ⟹⇩l⇧^τ ≺ P"
proof -
  assume "P ⟹⇩l Rs"
  thus "P ⟹⇩l⇧^Rs" by(simp add: weakTransition_def)
next
  show "P ⟹⇩l⇧^τ ≺ P" by(simp add: weakTransition_def)
qed

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

  assumes "P ⟹⇩l⇧^ Rs"
  and     "P ⟹⇩l Rs ⟹ F Rs"
  and     "Rs = τ ≺ P ⟹ F (τ ≺ P)"

  shows "F Rs"
using assms
by(auto simp add: weakTransition_def)

lemma singleActionChain:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  
  assumes "P ⟼α ≺ P'"
  
  shows "P ⟹⇩l⇧^(α ≺ P')"
using assms
by(auto intro: Weak_Late_Step_Semantics.singleActionChain
  simp add: weakTransition_def)

lemma Tau:
  fixes P :: pi

  shows "τ.(P) ⟹⇩l⇧^ τ ≺  P"
by(auto intro: Weak_Late_Step_Semantics.Tau
   simp add: weakTransition_def)
  
lemma Output:
  fixes a :: name
  and   b :: name
  and   P :: pi

  shows "a{b}.P ⟹⇩l⇧^a[b] ≺ P"
by(auto intro: Weak_Late_Step_Semantics.Output
   simp add: weakTransition_def)

lemma Match:
  fixes a  :: name
  and   P  :: pi
  and   b  :: name
  and   x  :: name
  and   P' :: pi
  and   α  :: freeRes

  shows "P ⟹⇩l⇧^b<νx> ≺ P' ⟹ [a⌢a]P ⟹⇩l⇧^b<νx> ≺ P'"
  and   "P ⟹⇩l⇧^α ≺ P' ⟹ P ≠ P' ⟹ [a⌢a]P ⟹⇩l⇧^α ≺ P'"
by(auto simp add: residual.inject weakTransition_def intro: Weak_Late_Step_Semantics.Match)

lemma Mismatch:
  fixes a  :: name
  and   c  :: name
  and   P  :: pi
  and   b  :: name
  and   x  :: name
  and   P' :: pi
  and   α  :: freeRes

  shows "⟦P ⟹⇩l⇧^b<νx> ≺ P'; a ≠ c⟧ ⟹ [a≠c]P ⟹⇩l⇧^b<νx> ≺ P'"
  and   "P ⟹⇩l⇧^α ≺ P' ⟹ P ≠ P' ⟹ a ≠ c ⟹ [a≠c]P ⟹⇩l⇧^α ≺ P'"
by(auto simp add: residual.inject weakTransition_def intro: Weak_Late_Step_Semantics.Mismatch)

lemma Open:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes Trans:  "P ⟹⇩l⇧^a[b] ≺ P'"
  and     aInEqb: "a ≠ b"

  shows "<νb>P ⟹⇩l⇧^a<νb> ≺ P'"
using assms
by(auto intro: Weak_Late_Step_Semantics.Open
  simp add: weakTransition_def residual.inject)

lemma Par1B:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi

  assumes PTrans: "P ⟹⇩l⇧^a<νx> ≺ P'"
  and     xFreshQ: "x ♯ Q"

  shows "P ∥ Q ⟹⇩l⇧^a<νx> ≺ (P' ∥ Q)"
using assms
by(auto intro: Weak_Late_Step_Semantics.Par1B
  simp add: weakTransition_def residual.inject)

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

  assumes PTrans: "P ⟹⇩l⇧^α ≺ P'"

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

lemma Par2B:
  fixes Q  :: pi
  and   a  :: name
  and   x  :: name
  and   Q' :: pi

  assumes QTrans: "Q ⟹⇩l⇧^a<νx> ≺ Q'"
  and     xFreshP: "x ♯ P"

  shows "P ∥ Q ⟹⇩l⇧^a<νx> ≺ (P ∥ Q')"
using assms
by(auto intro: Weak_Late_Step_Semantics.Par2B
  simp add: weakTransition_def residual.inject)

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

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

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

lemma Comm1:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P'' :: pi
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi
  
  assumes PTrans: "P ⟹⇩lb in P''→a<x> ≺ P'"
  and     QTrans: "Q ⟹⇩l⇧^a[b] ≺ Q'"

  shows "P ∥ Q ⟹⇩l⇧^τ ≺ P' ∥ Q'"
using assms
by(auto intro: Weak_Late_Step_Semantics.Comm1
  simp add: weakTransition_def residual.inject)

lemma Comm2:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   Q'' :: pi
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi
  
  assumes PTrans: "P ⟹⇩l⇧^a[b] ≺ P'"
  and     QTrans: "Q ⟹⇩lb in Q''→a<x> ≺ Q'"

  shows "P ∥ Q ⟹⇩l⇧^τ ≺ P' ∥ Q'"
using assms
by(auto intro: Weak_Late_Step_Semantics.Comm2
  simp add: weakTransition_def residual.inject)

lemma Close1:
  fixes P  :: pi
  and   y  :: name
  and   P'' :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi
  
  assumes PTrans: "P ⟹⇩ly in P''→a<x> ≺ P'"
  and     QTrans: "Q ⟹⇩l⇧^a<νy> ≺ Q'"
  and     xFreshP: "y ♯ P"
  and     xFreshQ: "y ♯ Q"

  shows "P ∥ Q ⟹⇩l⇧^τ ≺ <νy>(P' ∥ Q')"
using assms
by(auto intro: Weak_Late_Step_Semantics.Close1
  simp add: weakTransition_def residual.inject)

lemma Close2:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   y  :: name
  and   Q'' :: pi
  and   Q' :: pi
  
  assumes PTrans: "P ⟹⇩l⇧^a<νy> ≺ P'"
  and     QTrans: "Q ⟹⇩ly in Q''→a<x> ≺ Q'"
  and     xFreshP: "y ♯ P"
  and     xFreshQ: "y ♯ Q"

  shows "P ∥ Q ⟹⇩l⇧^τ ≺ <νy>(P' ∥ Q')"
using assms
by(auto intro: Weak_Late_Step_Semantics.Close2
  simp add: weakTransition_def residual.inject)

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

  assumes PTrans: "P ⟹⇩l⇧^α ≺ P'"
  and     xFreshAlpha: "x ♯ α"

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

lemma ResB:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   y  :: name

  assumes PTrans: "P ⟹⇩l⇧^a<νx> ≺ P'"
  and     yineqa: "y ≠ a"
  and     yineqx: "y ≠ x"
  and     xFreshP: "x ♯ P"

  shows "<νy>P ⟹⇩l⇧^a<νx> ≺ (<νy>P')"
using assms
by(auto intro: Weak_Late_Step_Semantics.ResB
  simp add: weakTransition_def residual.inject)

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

  assumes "P ∥ !P ⟹⇩l⇧^ Rs"
  and     "Rs ≠ τ ≺ P ∥ !P"
  
  shows "!P ⟹⇩l⇧^ Rs"
using assms
by(auto intro: Weak_Late_Step_Semantics.Bang
  simp add: weakTransition_def residual.inject)

lemma tauTransitionChain:
  fixes P  :: pi
  and   P' :: pi

  assumes "P ⟹⇩l⇧^τ ≺ P'"

  shows "P ⟹⇩τ P'"
using assms
by(auto intro: Weak_Late_Step_Semantics.tauTransitionChain
  simp add: weakTransition_def residual.inject transition_def)
  
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' ⟹⇩l⇧^ Rs ⟹ P ⟹⇩l⇧^ Rs"
  and   "P ⟹⇩l⇧^a<νx> ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ x ♯ P ⟹ P ⟹⇩l⇧^a<νx> ≺ P'"
  and   "P ⟹⇩l⇧^α ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹⇩l⇧^α ≺ P'"
proof -
  assume "P ⟹⇩τ P'" and "P' ⟹⇩l⇧^ Rs"
  thus "P ⟹⇩l⇧^ Rs"
    by(auto intro: Weak_Late_Step_Semantics.chainTransitionAppend
                   Weak_Late_Step_Semantics.tauActionChain
       simp add: weakTransition_def residual.inject)
next
  assume "P ⟹⇩l⇧^a<νx> ≺ P''" and "P'' ⟹⇩τ P'" and "x ♯ P"
  thus "P ⟹⇩l⇧^a<νx> ≺ P'"
    by(auto intro: Weak_Late_Step_Semantics.chainTransitionAppend
       simp add: weakTransition_def residual.inject)
next
  assume "P ⟹⇩l⇧^α ≺ P''" and "P'' ⟹⇩τ P'"
  thus "P ⟹⇩l⇧^α ≺ P'"
    apply(case_tac "P''=P'")
    by(auto dest: Weak_Late_Step_Semantics.chainTransitionAppend
                     Weak_Late_Step_Semantics.tauActionChain
       simp add: weakTransition_def residual.inject)
qed

lemma weakEqWeakTransitionAppend:
  fixes P   :: pi
  and   P'  :: pi
  and   α   :: freeRes
  and   P'' :: pi
  
  assumes PTrans: "P ⟹⇩lτ ≺ P'"
  and     P'Trans: "P' ⟹⇩l⇧^α ≺ P''"
  
  shows "P ⟹⇩lα ≺ P''"
proof(cases "α=τ")
  assume alphaEqTau: "α = τ"
  with P'Trans have "P' ⟹⇩τ P''" by(blast intro: tauTransitionChain)
  with PTrans alphaEqTau show ?thesis
    by(blast intro: Weak_Late_Step_Semantics.chainTransitionAppend)
next
  assume alphaIneqTau: "α ≠ τ"
  from PTrans have "P ⟹⇩τ P'" by(rule Weak_Late_Step_Semantics.tauTransitionChain)
  moreover from P'Trans alphaIneqTau have "P' ⟹⇩lα ≺ P''"
    by(auto simp add: weakTransition_def residual.inject)
  ultimately show ?thesis
    by(rule Weak_Late_Step_Semantics.chainTransitionAppend)
qed
    
lemma freshBoundOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   c  :: name

  assumes PTrans: "P ⟹⇩l⇧^a<νx> ≺ P'"
  and     cFreshP: "c ♯ P"
  and     cineqx: "c ≠ x"

  shows "c ♯ P'"
using assms
by(auto intro: Weak_Late_Step_Semantics.freshBoundOutputTransition
  simp add: weakTransition_def residual.inject)

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

  assumes PTrans: "P ⟹⇩l⇧^τ ≺ P'"
  and     cFreshP: "c ♯ P"

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

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

  assumes PTrans: "P ⟹⇩l⇧^a[b] ≺ P'"
  and     cFreshP: "c ♯ P"

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

lemma eqvtI:
  fixes P    :: pi
  and   Rs   :: residual
  and   perm :: "name prm"

  assumes "P ⟹⇩l⇧^ Rs"

  shows "(perm ∙ P) ⟹⇩l⇧^ (perm ∙ Rs)"
using assms
by(auto intro: Weak_Late_Step_Semantics.eqvtI
  simp add: weakTransition_def residual.inject)

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

  assumes PTrans: "P ⟹⇩l⇧^a<b> ≺ P'"
  and     cFreshP: "c ♯ P"
  and     cineqb: "c ≠ b"

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

lemmas freshTransition = freshBoundOutputTransition freshOutputTransition
                         freshInputTransition freshTauTransition

end