(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Cong_Subst_SC imports Weak_Late_Cong_Subst Strong_Late_Bisim_Subst_SC begin (******** Structural Congruence **********) (******** The ν-operator *****************) lemma resComm: fixes P :: pi shows "<νa><νb>P ≃⇧^{s}<νb><νa>P" proof - have "<νa><νb>P ∼⇧^{s}<νb><νa>P" by(rule Strong_Late_Bisim_Subst_SC.resComm) thus ?thesis by(rule strongEqWeakCong) qed (******** Match *********) lemma matchId: fixes a :: name and P :: pi shows "[a⌢a]P ≃⇧^{s}P" proof - have "[a⌢a]P ∼⇧^{s}P" by(rule Strong_Late_Bisim_Subst_SC.matchId) thus ?thesis by(rule strongEqWeakCong) qed (******** Mismatch *********) lemma matchNil: fixes a :: name and P :: pi shows "[a≠a]P ≃⇧^{s}𝟬" proof - have "[a≠a]P ∼⇧^{s}𝟬" by(rule Strong_Late_Bisim_Subst_SC.mismatchNil) thus ?thesis by(rule strongEqWeakCong) qed (******** The +-operator *********) lemma sumSym: fixes P :: pi and Q :: pi shows "P ⊕ Q ≃⇧^{s}Q ⊕ P" proof - have "P ⊕ Q ∼⇧^{s}Q ⊕ P" by(rule Strong_Late_Bisim_Subst_SC.sumSym) thus ?thesis by(rule strongEqWeakCong) qed lemma sumAssoc: fixes P :: pi and Q :: pi and R :: pi shows "(P ⊕ Q) ⊕ R ≃⇧^{s}P ⊕ (Q ⊕ R)" proof - have "(P ⊕ Q) ⊕ R ∼⇧^{s}P ⊕ (Q ⊕ R)" by(rule Strong_Late_Bisim_Subst_SC.sumAssoc) thus ?thesis by(rule strongEqWeakCong) qed lemma sumZero: fixes P :: pi shows "P ⊕ 𝟬 ≃⇧^{s}P" proof - have "P ⊕ 𝟬 ∼⇧^{s}P" by(rule Strong_Late_Bisim_Subst_SC.sumZero) thus ?thesis by(rule strongEqWeakCong) qed (******** The |-operator *********) lemma parZero: fixes P :: pi shows "P ∥ 𝟬 ≃⇧^{s}P" proof - have "P ∥ 𝟬 ∼⇧^{s}P" by(rule Strong_Late_Bisim_Subst_SC.parZero) thus ?thesis by(rule strongEqWeakCong) qed lemma parSym: fixes P :: pi and Q :: pi shows "P ∥ Q ≃⇧^{s}Q ∥ P" proof - have "P ∥ Q ∼⇧^{s}Q ∥ P" by(rule Strong_Late_Bisim_Subst_SC.parSym) thus ?thesis by(rule strongEqWeakCong) qed lemma scopeExtPar: fixes P :: pi and Q :: pi and x :: name assumes "x ♯ P" shows "<νx>(P ∥ Q) ≃⇧^{s}P ∥ <νx>Q" proof - from assms have "<νx>(P ∥ Q) ∼⇧^{s}P ∥ <νx>Q" by(rule Strong_Late_Bisim_Subst_SC.scopeExtPar) thus ?thesis by(rule strongEqWeakCong) qed lemma scopeExtPar': fixes P :: pi and Q :: pi and x :: name assumes xFreshQ: "x ♯ Q" shows "<νx>(P ∥ Q) ≃⇧^{s}(<νx>P) ∥ Q" proof - from assms have "<νx>(P ∥ Q) ∼⇧^{s}(<νx>P) ∥ Q" by(rule Strong_Late_Bisim_Subst_SC.scopeExtPar') thus ?thesis by(rule strongEqWeakCong) qed lemma parAssoc: fixes P :: pi and Q :: pi and R :: pi shows "(P ∥ Q) ∥ R ≃⇧^{s}P ∥ (Q ∥ R)" proof - have "(P ∥ Q) ∥ R ∼⇧^{s}P ∥ (Q ∥ R)" by(rule Strong_Late_Bisim_Subst_SC.parAssoc) thus ?thesis by(rule strongEqWeakCong) qed lemma scopeFresh: fixes P :: pi and a :: name assumes aFreshP: "a ♯ P" shows "<νa>P ≃⇧^{s}P" proof - from assms have "<νa>P ∼⇧^{s}P" by(rule Strong_Late_Bisim_Subst_SC.scopeFresh) thus ?thesis by(rule strongEqWeakCong) qed lemma scopeExtSum: fixes P :: pi and Q :: pi and x :: name assumes "x ♯ P" shows "<νx>(P ⊕ Q) ≃⇧^{s}P ⊕ <νx>Q" proof - from assms have "<νx>(P ⊕ Q) ∼⇧^{s}P ⊕ <νx>Q" by(rule Strong_Late_Bisim_Subst_SC.scopeExtSum) thus ?thesis by(rule strongEqWeakCong) qed lemma bangSC: fixes P shows "!P ≃⇧^{s}P ∥ !P" proof - have "!P ∼⇧^{s}P ∥ !P" by(rule Strong_Late_Bisim_Subst_SC.bangSC) thus ?thesis by(rule strongEqWeakCong) qed end