(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Early_Bisim_Pres imports Strong_Early_Bisim_Pres Weak_Early_Sim_Pres Weak_Early_Bisim_SC Weak_Early_Bisim begin (************ Preservation rules ************) lemma tauPres: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "τ.(P) ≈ τ.(Q)" proof - let ?X = "{(τ.(P), τ.(Q)) | P Q. P ≈ Q}" from ‹P ≈ Q› have "(τ.(P), τ.(Q)) ∈ ?X" by auto thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P Q) thus ?case by(force intro: Weak_Early_Sim_Pres.tauPres) next case(cSym P Q) thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject) qed qed lemma outputPres: fixes P :: pi and Q :: pi and a :: name and b :: name assumes "P ≈ Q" shows "a{b}.P ≈ a{b}.Q" proof - let ?X = "{(a{b}.(P), a{b}.(Q)) | P Q a b. P ≈ Q}" from ‹P ≈ Q› have "(a{b}.(P), a{b}.(Q)) ∈ ?X" by auto thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P Q) thus ?case by(force intro: Weak_Early_Sim_Pres.outputPres) next case(cSym P Q) thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject) qed qed lemma inputPres: fixes P :: pi and Q :: pi and a :: name and x :: name assumes PSimQ: "∀y. P[x::=y] ≈ Q[x::=y]" shows "a<x>.P ≈ a<x>.Q" proof - let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. ∀y. P[x::=y] ≈ Q[x::=y]}" { fix axP axQ p assume "(axP, axQ) ∈ ?X" then obtain a x P Q where A: "∀y. P[x::=y] ≈ Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q" by auto have "⋀y. ((p::name prm) ∙ P)[(p ∙ x)::=y] ≈ (p ∙ Q)[(p ∙ x)::=y]" proof - fix y from A have "P[x::=(rev p ∙ y)] ≈ Q[x::=(rev p ∙ y)]" by blast hence "(p ∙ (P[x::=(rev p ∙ y)])) ≈ p ∙ (Q[x::=(rev p ∙ y)])" by(rule eqvts) thus "(p ∙ P)[(p ∙ x)::=y] ≈ (p ∙ Q)[(p ∙ x)::=y]" by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst]) qed hence "((p::name prm) ∙ axP, p ∙ axQ) ∈ ?X" using B C by auto } hence "eqvt ?X" by(simp add: eqvt_def) from PSimQ have "(a<x>.P, a<x>.Q) ∈ ?X" by auto thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P Q) thus ?case using ‹eqvt ?X› by(force intro: Weak_Early_Sim_Pres.inputPres) next case(cSym P Q) thus ?case by(blast dest: weakBisimE) qed qed lemma resPres: fixes P :: pi and Q :: pi and x :: name assumes "P ≈ Q" shows "<νx>P ≈ <νx>Q" proof - let ?X = "{(<νx>P, <νx>Q) | x P Q. P ≈ Q}" from ‹P ≈ Q› have "(<νx>P, <νx>Q) ∈ ?X" by blast thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim xP xQ) { fix P Q x assume "P ≈ Q" hence "P ↝<weakBisim> Q" by(rule weakBisimE) moreover have "⋀P Q x. P ≈ Q ⟹ (<νx>P, <νx>Q) ∈ ?X ∪ weakBisim" by blast moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast moreover have "eqvt weakBisim" by simp moreover have "eqvt (?X ∪ weakBisim)" by(auto simp add: eqvt_def dest: Weak_Early_Bisim.eqvtI)+ ultimately have "<νx>P ↝<(?X ∪ weakBisim)> <νx>Q" by(rule Weak_Early_Sim_Pres.resPres) } with ‹(xP, xQ) ∈ ?X› show ?case by blast next case(cSym xP xQ) thus ?case by(blast dest: Weak_Early_Bisim.symetric) qed qed lemma matchPres: fixes P :: pi and Q :: pi and a :: name and b :: name assumes "P ≈ Q" shows "[a⌢b]P ≈ [a⌢b]Q" proof - let ?X = "{([a⌢b]P, [a⌢b]Q) | a b P Q. P ≈ Q}" from ‹P ≈ Q› have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by blast thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim abP abQ) { fix P Q a b assume "P ≈ Q" hence "P ↝<weakBisim> Q" by(rule weakBisimE) moreover have "weakBisim ⊆ (?X ∪ weakBisim)" by blast moreover have "⋀P Q a. P ≈ Q ⟹ [a⌢a]P ≈ Q" by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.matchId Weak_Early_Bisim.transitive) ultimately have"[a⌢b]P ↝<(?X ∪ weakBisim)> [a⌢b]Q" by(rule Weak_Early_Sim_Pres.matchPres) } with ‹(abP, abQ) ∈ ?X› show ?case by blast next case(cSym abP abQ) thus ?case by(blast dest: Weak_Early_Bisim.symetric) qed qed lemma mismatchPres: fixes P :: pi and Q :: pi and a :: name and b :: name assumes "P ≈ Q" shows "[a≠b]P ≈ [a≠b]Q" proof - let ?X = "{([a≠b]P, [a≠b]Q)| a b P Q. P ≈ Q}" from ‹P ≈ Q› have "([a≠b]P, [a≠b]Q) ∈ ?X" by blast thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim abP abQ) { fix P Q a b assume "P ≈ Q" hence "P ↝<weakBisim> Q" by(rule weakBisimE) moreover have "weakBisim ⊆ (?X ∪ weakBisim)" by blast moreover have "⋀P Q a b. ⟦P ≈ Q; a ≠ b⟧ ⟹ [a≠b]P ≈ Q" by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.mismatchId Weak_Early_Bisim.transitive) ultimately have "[a≠b]P ↝<(?X ∪ weakBisim)> [a≠b]Q" by(rule Weak_Early_Sim_Pres.mismatchPres) } with ‹(abP, abQ) ∈ ?X› show ?case by blast next case(cSym abP abQ) thus ?case by(blast dest: Weak_Early_Bisim.symetric) qed qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi assumes "P ≈ Q" shows "P ∥ R ≈ Q ∥ R" proof - let ?X = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P R Q. P ≈ Q}" have BC: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto from ‹P ≈ Q› have "(P ∥ R, Q ∥ R) ∈ ?X" by(blast intro: BC) thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSym PR QR) { fix P Q R lst assume "P ≈ Q" moreover hence "P ↝<weakBisim> Q" by(rule weakBisimE) moreover have "⋀P Q R. P ≈ Q ⟹ (P ∥ R, Q ∥ R) ∈ ?X" using BC by blast moreover { fix PR QR x assume "(PR, QR) ∈ ?X" then obtain lst P Q R where "P ≈ Q" and A: "PR = resChain lst (P ∥ R)" and B: "QR = resChain lst (Q ∥ R)" by auto from A have "<νx>PR = resChain (x#lst) (P ∥ R)" by auto moreover from B have "<νx>QR = resChain (x#lst) (Q ∥ R)" by auto ultimately have "(<νx>PR, <νx>QR) ∈ ?X" using ‹P ≈ Q› by blast } note Res = this ultimately have "P ∥ R ↝<?X> Q ∥ R" by(rule_tac Weak_Early_Sim_Pres.parPres) moreover have "eqvt ?X" by(auto simp add: eqvt_def) (blast intro: eqvts) ultimately have "resChain lst (P ∥ R) ↝<?X> resChain lst (Q ∥ R)" using Res by(rule_tac Weak_Early_Sim_Pres.resChainI) hence "resChain lst (P ∥ R) ↝<(?X ∪ weakBisim)> resChain lst (Q ∥ R)" by(force intro: Weak_Early_Sim.monotonic) } with ‹(PR, QR) ∈ ?X› show "PR ↝<(?X ∪ weakBisim)> QR" by blast next case(cSym PR QR) thus ?case by(blast dest: Weak_Early_Bisim.symetric) qed qed lemma bangPres: fixes P :: pi and Q :: pi assumes PBisimQ: "P ≈ Q" shows "!P ≈ !Q" proof - let ?X = "(bangRel weakBisim)" let ?Y = "Strong_Early_Bisim.bisim O (bangRel weakBisim) O Strong_Early_Bisim.bisim" from Weak_Early_Bisim.eqvt Strong_Early_Bisim.eqvt have eqvtY: "eqvt ?Y" by(blast intro: eqvtBangRel) have XsubY: "?X ⊆ ?Y" by(auto intro: Strong_Early_Bisim.reflexive) have RelStay: "⋀P Q. (P ∥ !P, Q) ∈ ?Y ⟹ (!P, Q) ∈ ?Y" proof(auto) fix P Q R T assume PBisimQ: "P ∥ !P ∼⇩_{e}Q" and QBRR: "(Q, R) ∈ bangRel weakBisim" and RBisimT: "R ∼⇩_{e}T" have "!P ∼⇩_{e}Q" proof - have "!P ∼⇩_{e}P ∥ !P" by(rule Strong_Early_Bisim_SC.bangSC) thus ?thesis using PBisimQ by(rule Strong_Early_Bisim.transitive) qed with QBRR RBisimT show "(!P, T) ∈ ?Y" by blast qed have ParCompose: "⋀P Q R T. ⟦P ≈ Q; (R, T) ∈ ?Y⟧ ⟹ (P ∥ R, Q ∥ T) ∈ ?Y" proof - fix P Q R T assume PBisimQ: "P ≈ Q" and RYT: "(R, T) ∈ ?Y" thus "(P ∥ R, Q ∥ T) ∈ ?Y" proof(auto) fix T' R' assume T'BisimT: "T' ∼⇩_{e}T" and RBisimR': "R ∼⇩_{e}R'" and R'BRT': "(R', T') ∈ bangRel weakBisim" have "P ∥ R ∼⇩_{e}P ∥ R'" proof - from RBisimR' have "R ∥ P ∼⇩_{e}R' ∥ P" by(rule Strong_Early_Bisim_Pres.parPres) moreover have "P ∥ R ∼⇩_{e}R ∥ P" and "R' ∥ P ∼⇩_{e}P ∥ R'" by(rule Strong_Early_Bisim_SC.parSym)+ ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive) qed moreover from PBisimQ R'BRT' have "(P ∥ R', Q ∥ T') ∈ bangRel weakBisim" by(rule BRPar) moreover have "Q ∥ T' ∼⇩_{e}Q ∥ T" proof - from T'BisimT have "T' ∥ Q ∼⇩_{e}T ∥ Q" by(rule Strong_Early_Bisim_Pres.parPres) moreover have "Q ∥ T' ∼⇩_{e}T' ∥ Q" and "T ∥ Q ∼⇩_{e}Q ∥ T" by(rule Strong_Early_Bisim_SC.parSym)+ ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive) qed ultimately show ?thesis by blast qed qed have ResCong: "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(auto intro: BRRes Strong_Early_Bisim_Pres.resPres transitive) have Sim: "⋀P Q. (P, Q) ∈ ?X ⟹ P ↝<?Y> Q" proof - fix P Q assume "(P, Q) ∈ ?X" thus "P ↝<?Y> Q" proof(induct) case(BRBang P Q) have "P ≈ Q" by fact moreover hence "P ↝<weakBisim> Q" by(blast dest: weakBisimE) moreover have "⋀P Q. P ≈ Q ⟹ P ↝<weakBisim> Q" by(blast dest: weakBisimE) moreover from Strong_Early_Bisim.eqvt Weak_Early_Bisim.eqvt have "eqvt ?Y" by(blast intro: eqvtBangRel) ultimately show "!P ↝<?Y> !Q" using ParCompose ResCong RelStay XsubY by(rule_tac Weak_Early_Sim_Pres.bangPres, simp_all) next case(BRPar P Q R T) have PBiSimQ: "P ≈ Q" by fact moreover have RBangRelT: "(R, T) ∈ ?X" by fact have RSimT: "R ↝<?Y> T" by fact moreover from PBiSimQ have "P ↝<weakBisim> Q" by(blast dest: weakBisimE) moreover from RBangRelT have "(R, T) ∈ ?Y" by(blast intro: Strong_Early_Bisim.reflexive) ultimately show "P ∥ R ↝<?Y> Q ∥ T" using ParCompose ResCong eqvt eqvtY by(rule_tac Weak_Early_Sim_Pres.parCompose) next case(BRRes P Q x) have "P ↝<?Y> Q" by fact thus "<νx>P ↝<?Y> <νx>Q" using ResCong eqvtY XsubY by(rule_tac Weak_Early_Sim_Pres.resPres, simp_all) qed qed from PBisimQ have "(!P, !Q) ∈ ?X" by(rule BRBang) moreover from Weak_Early_Bisim.eqvt have "eqvt (bangRel weakBisim)" by(rule eqvtBangRel) ultimately show ?thesis apply(coinduct rule: Weak_Early_Bisim.transitive_coinduct_weak) apply(blast intro: Sim) by(blast dest: bangRelSymetric Weak_Early_Bisim.symetric intro: Strong_Early_Bisim.reflexive) qed lemma bangRelSubWeakBisim: shows "bangRel weakBisim ⊆ weakBisim" proof(auto) fix a b assume "(a, b) ∈ bangRel weakBisim" thus "a ≈ b" proof(induct) fix P Q assume "P ≈ Q" thus "!P ≈ !Q" by(rule bangPres) next fix P Q R T assume "R ≈ T" and "P ≈ Q" thus "R ∥ P ≈ T ∥ Q" by(metis parPres parSym Weak_Early_Bisim.transitive) next fix P Q fix a::name assume "P ≈ Q" thus "<νa>P ≈ <νa>Q" by(rule resPres) qed qed end