Theory Strong_Late_Bisim_SC

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

lemma nilBisim[dest]:
  fixes a :: name
  and   b :: name
  and   x :: name
  and   P :: pi

  shows "τ.(P) ∼ 𝟬 ⟹ False"
  and   "a<x>.P ∼ 𝟬 ⟹ False"
  and   "a{b}.P ∼ 𝟬 ⟹ False"
  and   "𝟬 ∼ τ.(P) ⟹ False"
  and   "𝟬 ∼ a<x>.P ⟹ False"
  and   "𝟬 ∼ a{b}.P ⟹ False"
by(auto dest: bisimE symmetric)

(******** Structural Congruence **********)

lemma matchId:
  fixes a :: name
  and   P :: pi

  shows "[a⌢a]P ∼ P"
proof -
  let ?X = "{([a⌢a]P, P), (P, [a⌢a]P)}"
  have "([a⌢a]P, P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: matchIdLeft matchIdRight reflexive)
qed

lemma matchNil:
  fixes a :: name
  and   b :: name

  assumes "a ≠ b"

  shows "[a⌢b]P ∼ 𝟬"
proof -
  let ?X = "{([a⌢b]P, 𝟬), (𝟬, [a⌢b]P)}"
  have "([a⌢b]P, 𝟬) ∈ ?X" by simp
  thus ?thesis using ‹a ≠ b›
    by(coinduct rule: bisimCoinduct) (auto intro: matchNilLeft nilSimRight reflexive)
qed

lemma mismatchId:
  fixes a :: name
  and   b :: name
  and   P :: pi

  assumes "a ≠ b"

  shows "[a≠b]P ∼ P"
proof -
  let ?X = "{([a≠b]P, P), (P, [a≠b]P)}"
  have "([a≠b]P, P) ∈ ?X" by simp
  thus ?thesis using ‹a ≠ b›
    by(coinduct rule: bisimCoinduct) (auto intro: mismatchIdLeft mismatchIdRight reflexive)
qed

lemma mismatchNil:
  fixes a :: name
  and   P :: pi
  
  shows "[a≠a]P ∼ 𝟬"
proof -
  let ?X = "{([a≠a]P, 𝟬), (𝟬, [a≠a]P)}"
  have "([a≠a]P, 𝟬) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: mismatchNilLeft nilSimRight reflexive)
qed
(******** The ν-operator *****************)

lemma nilRes:
  fixes x :: name

  shows "<νx>𝟬 ∼ 𝟬"
proof -
  let ?X = "{(<νx>𝟬, 𝟬), (𝟬, <νx>𝟬)}"
  have "(<νx>𝟬, 𝟬) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: nilSimRight resNilRight)
qed

lemma resComm:
  fixes x :: name
  and   y :: name
  and   P :: pi
  
  shows "<νx><νy>P ∼ <νy><νx>P"
proof -
  let ?X = "{(<νx><νy>P, <νy><νx>P) | x y P. True}"
  have "(<νx><νy>P, <νy><νx>P) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim xyP yxP)
    {
      fix x y P
      have "⋀x y P. (<νx><νy>P, <νy><νx>P) ∈ ?X ∪ bisim" by auto
      moreover have "Id ⊆ ?X ∪ bisim" by(auto intro: reflexive)
      moreover have "eqvt ?X" by(force simp add: eqvt_def)
      hence "eqvt(?X ∪ bisim)" by auto
      ultimately have "<νx><νy>P ↝[(?X ∪ bisim)] <νy><νx>P" by(rule resComm)
    }
    with ‹(xyP, yxP) ∈ ?X› show ?case by auto
  next
    case(cSym xyP yxP)
    thus ?case by auto
  qed
qed

(******** The +-operator *********)

lemma sumSym:
  fixes P :: pi
  and   Q :: pi
  
  shows "P ⊕ Q ∼ Q ⊕ P"
proof -
  let ?X = "{(P ⊕ Q, Q ⊕ P), (Q ⊕ P, P ⊕ Q)}"
  have "(P ⊕ Q, Q ⊕ P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumSym)
qed

lemma sumIdemp:
  fixes P :: pi
  
  shows "P ⊕ P ∼ P"
proof -
  let ?X = "{(P ⊕ P, P), (P, P ⊕ P)}"
  have "(P ⊕ P, P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumIdempLeft sumIdempRight)
qed

lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  shows "(P ⊕ Q) ⊕ R ∼ P ⊕ (Q ⊕ R)"
proof -
  let ?X = "{((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)), (P ⊕ (Q ⊕ R), (P ⊕ Q) ⊕ R)}"
  have "((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumAssocLeft sumAssocRight)
qed

lemma sumZero:
  fixes P :: pi
  
  shows "P ⊕ 𝟬 ∼ P"
proof -
  let ?X = "{(P ⊕ 𝟬, P), (P, P ⊕ 𝟬)}"
  have "(P ⊕ 𝟬, P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumZeroLeft sumZeroRight)
qed

(******** The |-operator *********)

lemma parZero:
  fixes P :: pi
  
  shows "P ∥ 𝟬 ∼ P"
proof -
  let ?X = "{(P ∥ 𝟬, P) | P. True} ∪ {(P, P ∥ 𝟬) | P . True}"
  have "(P ∥ 𝟬, P) ∈ ?X" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct, auto intro: parZeroRight parZeroLeft)
qed

lemma parSym:
  fixes P :: pi
  and   Q :: pi

  shows "P ∥ Q ∼ Q ∥ P"
proof -
  let ?X = "{(resChain lst (P ∥ Q), resChain lst (Q ∥ P)) | lst P Q. True}"
  have "(P ∥ Q, Q ∥ P) ∈ ?X" by(blast intro: resChain.base[THEN sym])
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim PQ QP)
    {
      fix lst P Q
      have "⋀P Q. (P ∥ Q, Q ∥ P) ∈ ?X ∪ bisim" by(blast intro: resChain.base[THEN sym])
      moreover have Res: "⋀x P Q. (P, Q) ∈ ?X ∪ bisim ⟹ (<νx>P, <νx>Q) ∈ ?X ∪ bisim"
        by(auto intro: resPres resChain.step[THEN sym])
      ultimately have "P ∥ Q ↝[(?X ∪ bisim)] Q ∥ P" by(rule parSym)
      moreover have "eqvt ?X" by(force simp add: eqvt_def) 
      hence "eqvt(?X ∪ bisim)" by auto
      ultimately have "resChain lst (P ∥ Q) ↝[(?X ∪ bisim)] resChain lst (Q ∥ P)" using Res
        by(rule resChainI)
    }
    with ‹(PQ, QP) ∈ ?X› show ?case by auto
  next
    case(cSym PQ QP)
    thus ?case by auto
  qed
qed

lemma scopeExtPar:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x ♯ P"

  shows "<νx>(P ∥ Q) ∼ P ∥ <νx>Q"
proof -
  let ?X = "{(resChain lst (<νx>(P ∥ Q)), resChain lst (P ∥ <νx>Q)) | lst x P Q. x ♯ P} ∪
            {(resChain lst (P ∥ <νx>Q), resChain lst (<νx>(P ∥ Q))) | lst x P Q. x ♯ P}"
  let ?Y = "bisim O (?X ∪ bisim) O bisim"

  have Res: "⋀P Q x. (P, Q) ∈ ?X ⟹ (<νx>P, <νx>Q) ∈ ?X" by(blast intro: resChain.step[THEN sym])

  from ‹x ♯ P› have "(<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?X" by(blast intro: resChain.base[THEN sym])
  moreover have EqvtX: "eqvt ?X" by(fastforce simp add: eqvt_def name_fresh_left name_rev_per)
  ultimately show ?thesis
  proof(coinduct rule: bisimTransitiveCoinduct)
    case(cSim P Q)
    {
      fix P Q lst x
      assume "(x::name) ♯ (P::pi)"
      moreover have "Id ⊆ ?Y" by(blast intro: reflexive)
      moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast
      moreover have "⋀P Q x. x ♯ P ⟹ (<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?Y"
        by(blast intro: resChain.base[THEN sym] reflexive)
      moreover {
        fix P Q x y
        have "<νx><νy>(P ∥ Q) ∼ <νy><νx>(P ∥ Q)" by(rule resComm)
        moreover assume "x ♯ P"
        hence "(<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?X" by(fastforce intro: resChain.base[THEN sym])
        hence "(<νy><νx>(P ∥ Q), <νy>(P ∥ <νx>Q)) ∈ ?X" by(rule Res)
        ultimately have  "(<νx><νy>(P ∥ Q), <νy>(P ∥ <νx>Q)) ∈ ?Y" by(blast intro: reflexive)
      }
      ultimately have "<νx>(P ∥ Q) ↝[?Y] (P ∥ <νx>Q)" by(rule scopeExtParLeft) 
      moreover note ‹eqvt ?Y›
      moreover from Res have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y"
        by(blast intro: resChain.step[THEN sym] dest: resPres)
      ultimately have "resChain lst (<νx>(P ∥ Q)) ↝[?Y] resChain lst (P ∥ <νx>Q)" 
        by(rule resChainI)
    }
    moreover {
      fix P Q lst x
      assume "(x::name) ♯ (P::pi)"
      moreover have "Id ⊆ ?Y" by(blast intro: reflexive)
      moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast
      moreover have "⋀P Q x. x ♯ P ⟹ (P ∥ <νx>Q, <νx>(P ∥ Q)) ∈ ?Y"
        by(blast intro: resChain.base[THEN sym] reflexive)
      moreover {
        fix P Q x y
        have "<νy><νx>(P ∥ Q) ∼ <νx><νy>(P ∥ Q)" by(rule resComm)
        moreover assume "x ♯ P"
        hence "(P ∥ <νx>Q, <νx>(P ∥ Q)) ∈ ?X" by(fastforce intro: resChain.base[THEN sym])
        hence "(<νy>(P ∥ <νx>Q), <νy><νx>(P ∥ Q)) ∈ ?X" by(rule Res)
        ultimately have  "(<νy>(P ∥ <νx>Q), <νx><νy>(P ∥ Q)) ∈ ?Y" by(blast intro: reflexive)
      }
      ultimately have "(P ∥ <νx>Q) ↝[?Y] <νx>(P ∥ Q)" 
        by(rule scopeExtParRight) 
      moreover note ‹eqvt ?Y›
      moreover from Res have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y"
        by(blast intro: resChain.step[THEN sym] dest: resPres)
      ultimately have "resChain lst (P ∥ <νx>Q) ↝[?Y] resChain lst (<νx>(P ∥ Q))" 
        by(rule resChainI)
    }
    ultimately show ?case using ‹(P, Q) ∈ ?X› by auto
  next
    case(cSym P Q)
    thus ?case 
      by auto (blast dest: symmetric transitive intro: resChain.base[THEN sym] reflexive)+
  qed
qed

lemma scopeExtPar':
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes xFreshQ: "x ♯ Q"

  shows "<νx>(P ∥ Q) ∼ (<νx>P) ∥ Q"
proof -
  have "<νx>(P ∥ Q) ∼ <νx>(Q ∥ P)"
  proof -
    have "P ∥ Q ∼ Q ∥ P" by(rule parSym)
    thus ?thesis by(rule resPres)
  qed
  moreover from xFreshQ have "<νx>(Q ∥ P) ∼ Q ∥ (<νx>P)" by(rule scopeExtPar)
  moreover have "Q ∥ <νx>P ∼ (<νx>P) ∥ Q" by(rule parSym)
  ultimately show ?thesis by(blast intro: transitive)
qed

lemma parAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  shows "(P ∥ Q) ∥ R ∼ P ∥ (Q ∥ R)"
proof -
  let ?X = "{(resChain lst ((P ∥ Q) ∥ R), resChain lst (P ∥ (Q ∥ R))) | lst P Q R. True}"
  let ?Y = "bisim O (?X ∪ bisim) O bisim"

  have ResX: "⋀P Q x. (P, Q) ∈ ?X ⟹ (<νx>P, <νx>Q) ∈ ?X" 
    by(blast intro: resChain.step[symmetric])
  hence ResY: "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y"
    by(blast intro: resChain.step[symmetric] dest: resPres)

  have "((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?X" by(blast intro: resChain.base[symmetric])
  moreover have "eqvt ?X" by(fastforce simp add: eqvt_def) 
  ultimately show ?thesis
  proof(coinduct rule: bisimTransitiveCoinduct)
    case(cSim P Q)
    {
      fix P Q R lst
      have "⋀P Q R. ((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?Y" by(blast intro: reflexive resChain.base[symmetric])
      moreover have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(blast intro: resChain.step[symmetric] resPres)
      moreover {
        fix P Q R x
        have "(<νx>((P ∥ Q) ∥ R), <νx>(P ∥ (Q ∥ R))) ∈ ?X" by(rule_tac ResX) (blast intro: resChain.base[symmetric])
        moreover assume "x ♯ P"
        hence "<νx>(P ∥ (Q ∥ R)) ∼ P ∥ <νx>(Q ∥ R)" by(rule scopeExtPar)
        ultimately have "(<νx>((P ∥ Q) ∥ R), P ∥ <νx>(Q ∥ R)) ∈ ?Y" by(blast intro: reflexive)
      }
      moreover {
        fix P Q R x
        have "(<νx>((P ∥ Q) ∥ R), <νx>(P ∥ (Q ∥ R))) ∈ ?X" by(rule_tac ResX) (blast intro: resChain.base[symmetric])
        moreover assume "x ♯ R"
        hence "<νx>(P ∥ Q) ∥ R ∼ <νx>((P ∥ Q) ∥ R)" by(metis scopeExtPar' symmetric)
        ultimately have "(<νx>(P ∥ Q) ∥ R, <νx>(P ∥ (Q ∥ R))) ∈ ?Y" by(blast intro: reflexive)
      }
      ultimately have "(P ∥ Q) ∥ R ↝[?Y] P ∥ (Q ∥ R)" by(rule parAssocLeft)
      moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast
      ultimately have "resChain lst ((P ∥ Q) ∥ R) ↝[?Y] resChain lst (P ∥ (Q ∥ R))" using ResY
        by(rule resChainI)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    {
      fix P Q R lst
      have "P ∥ (Q ∥ R) ∼ (R ∥ Q) ∥ P" by(metis parPres parSym transitive)
      moreover have "((R ∥ Q) ∥ P, R ∥ (Q ∥ P)) ∈ ?X" by(blast intro: resChain.base[symmetric])
      moreover have "R ∥ (Q ∥ P) ∼ (P ∥ Q) ∥ R" by(metis parPres parSym transitive)
      ultimately have "(P ∥ (Q ∥ R), (P ∥ Q) ∥ R) ∈ ?Y" by blast
      hence "(resChain lst (P ∥ (Q ∥ R)), resChain lst ((P ∥ Q) ∥ R)) ∈ ?Y" using ResY
        by(induct lst) auto
    }
    with ‹(P, Q) ∈ ?X› show ?case by blast
  qed
qed

lemma scopeFresh:
  fixes x :: name
  and   P :: pi

  assumes "x ♯ P"

  shows "<νx>P ∼ P"
proof -
  have "<νx>P ∼ <νx>P ∥ 𝟬" by(rule parZero[THEN symmetric])

  moreover have "<νx>P ∥ 𝟬 ∼ 𝟬 ∥ <νx>P" by(rule parSym)
  moreover have "𝟬 ∥ <νx>P ∼ <νx>(𝟬 ∥ P)" by(rule scopeExtPar[THEN symmetric]) auto
  moreover have "<νx>(𝟬 ∥ P) ∼ <νx>(P ∥ 𝟬)" by(rule resPres[OF parSym])
  moreover from ‹x ♯ P› have "<νx>(P ∥ 𝟬) ∼ P ∥ <νx>𝟬" by(rule scopeExtPar)
  moreover have  "P ∥ <νx>𝟬 ∼ <νx>𝟬 ∥ P" by(rule parSym)
  moreover have "<νx>𝟬 ∥ P ∼ 𝟬 ∥ P" by(rule parPres[OF nilRes])
  moreover have "𝟬 ∥ P ∼ P ∥ 𝟬" by(rule parSym)
  moreover have "P ∥ 𝟬 ∼ P" by(rule parZero)
  ultimately show ?thesis by(metis transitive)
qed

lemma sumRes:
  fixes x :: name
  and   P :: pi
  and   Q :: pi

  shows "<νx>(P ⊕ Q) ∼ (<νx>P) ⊕ (<νx>Q)"
proof -
  let ?X = "{(<νx>(P ⊕ Q), <νx>P ⊕ <νx>Q) | x P Q. True} ∪
            {(<νx>P ⊕ <νx>Q, <νx>(P ⊕ Q)) | x P Q. True}"
  have "(<νx>(P ⊕ Q), <νx>P ⊕ <νx>Q) ∈ ?X" by auto
  moreover have "eqvt ?X" by(fastforce simp add: eqvt_def)
  ultimately show ?thesis
    by(coinduct rule: bisimCoinduct) (fastforce intro: sumResLeft sumResRight reflexive)+
qed


lemma scopeExtSum:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes "x ♯ P"

  shows "<νx>(P ⊕ Q) ∼ P ⊕ <νx>Q"
proof -
  have "<νx>(P ⊕ Q) ∼ <νx>P ⊕ <νx>Q" by(rule sumRes)
  moreover from ‹x ♯ P› have "<νx>P ⊕ <νx>Q ∼ P ⊕ <νx>Q"
    by(rule sumPres[OF scopeFresh])
  ultimately show ?thesis by(rule transitive)
qed

lemma bangSC:
  fixes P :: pi

  shows "!P ∼ P ∥ !P"
proof -
  let ?X = "{(!P, P ∥ !P), (P ∥ !P, !P)}"
  have "(!P, P ∥ !P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: bangLeftSC bangRightSC reflexive)
qed

lemma resNil:
  fixes x :: name
  and   y :: name
  and   P :: pi
  and   b :: name

  shows "<νx>x<y>.P ∼ 𝟬"
  and   "<νx>x{b}.P ∼ 𝟬"
proof -
  let ?X = "{(<νx>x<y>.P, 𝟬), (𝟬, <νx>x<y>.P)}"
  have "(<νx>x<y>.P, 𝟬) ∈ ?X" by simp
  thus "<νx>x<y>.P ∼ 𝟬"
    by(coinduct rule: bisimCoinduct) (auto simp add: simulation_def)
next
  let ?X = "{(<νx>x{b}.P, 𝟬), (𝟬, <νx>x{b}.P)}"
  have "(<νx>x{b}.P, 𝟬) ∈ ?X" by simp
  thus "<νx>x{b}.P ∼ 𝟬"
    by(coinduct rule: bisimCoinduct) (auto simp add: simulation_def)
qed

lemma resInput:
  fixes x :: name
  and   a :: name
  and   y :: name
  and   P :: pi

  assumes "x ≠ a"
  and     "x ≠ y"

  shows "<νx>a<y>.P ∼ a<y>.(<νx>P)"
proof -
  let ?X = "{(<νx>a<y>.P, a<y>.(<νx>P)) | x a y P. x ≠ a ∧ x ≠ y} ∪
            {(a<y>.(<νx>P), <νx>a<y>.P) | x a y P. x ≠ a ∧ x ≠ y}"
  from assms have "(<νx>a<y>.P, a<y>.(<νx>P)) ∈ ?X" by auto
  moreover have "eqvt ?X" by(fastforce simp add: eqvt_def pt_bij[OF pt_name_inst, OF at_name_inst])
  ultimately show ?thesis
    by(coinduct rule: bisimCoinduct) (fastforce intro: resInputLeft reflexive resInputRight)+
qed

lemma resOutput:
  fixes x :: name
  and   a :: name
  and   b :: name
  and   P :: pi

  assumes "x ≠ a"
  and     "x ≠ b"

  shows "<νx>a{b}.P ∼ a{b}.(<νx>P)"
proof -
  let ?X = "{(<νx>a{b}.P, a{b}.(<νx>P)) | x a b P. x ≠ a ∧ x ≠ b} ∪
            {(a{b}.(<νx>P), <νx>a{b}.P) | x a b P. x ≠ a ∧ x ≠ b}"
  from assms have "(<νx>a{b}.P, a{b}.(<νx>P)) ∈ ?X" by blast
  moreover have "eqvt ?X" by(fastforce simp add: eqvt_def pt_bij[OF pt_name_inst, OF at_name_inst])
  ultimately show ?thesis
    by(coinduct rule: bisimCoinduct) (fastforce intro: resOutputLeft resOutputRight reflexive)+
qed

lemma resTau:
  fixes x :: name
  and   P :: pi

  shows "<νx>τ.(P) ∼ τ.(<νx>P)"
proof -
  let ?X = "{(<νx>τ.(P), τ.(<νx>P)), (τ.(<νx>P), <νx>τ.(P))}"
  have "(<νx>τ.(P), τ.(<νx>P)) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (fastforce intro: resTauLeft resTauRight reflexive)+
qed

inductive structCong :: "pi ⇒ pi ⇒ bool" (‹_ ≡⇩s _› [70, 70] 70)
where
  Refl: "P ≡⇩s P"
| Sym:  "P ≡⇩s Q ⟹ Q ≡⇩s P"
| Trans: "⟦P ≡⇩s Q; Q ≡⇩s R⟧ ⟹ P ≡⇩s R"

| SumComm: "P ⊕ Q ≡⇩s Q ⊕ P"
| SumAssoc: "(P ⊕ Q) ⊕ R ≡⇩s P ⊕ (Q ⊕ R)"
| SumId: "P ⊕ 𝟬 ≡⇩s P"

| ParComm: "P ∥ Q ≡⇩s Q ∥ P"
| ParAssoc: "(P ∥ Q) ∥ R ≡⇩s P ∥ (Q ∥ R)"
| ParId: "P ∥ 𝟬 ≡⇩s P"

| MatchId: "[a⌢a]P ≡⇩s P"

| ResNil: "<νx>𝟬 ≡⇩s 𝟬"
| ResComm: "<νx><νy>P ≡⇩s <νy><νx>P"
| ResSum: "<νx>(P ⊕ Q) ≡⇩s <νx>P ⊕ <νx>Q"
| ScopeExtPar: "x ♯ P ⟹ <νx>(P ∥ Q) ≡⇩s P ∥ <νx>Q"
| InputRes: "⟦x ≠ a; x ≠ y⟧ ⟹ <νx>a<y>.P ≡⇩s a<y>.(<νx>P)"
| OutputRes: "⟦x ≠ a; x ≠ b⟧ ⟹ <νx>a{b}.P ≡⇩s a{b}.(<νx>P)"
| TauRes: "<νx>τ.(P) ≡⇩s τ.(<νx>P)"

| BangUnfold: "!P ≡⇩s P ∥ !P"

lemma structCongBisim:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≡⇩s Q"

  shows "P ∼ Q"
using assms
by(induct rule: structCong.induct)
  (auto intro: reflexive symmetric transitive sumSym sumAssoc sumZero parSym parAssoc parZero
               nilRes resComm resInput resOutput resTau sumRes scopeExtPar bangSC matchId mismatchId)

end