(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Bisim_Pres imports Weak_Late_Bisim_SC Weak_Late_Sim_Pres Strong_Late_Bisim_SC begin lemma tauPres: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "τ.(P) ≈ τ.(Q)" proof - let ?X = "{(τ.(P), τ.(Q)) | P Q. P ≈ Q}" from assms have "(τ.(P), τ.(Q)) ∈ ?X" by auto thus ?thesis by(coinduct rule: weakBisimCoinduct) (auto simp add: pi.inject intro: Weak_Late_Sim_Pres.tauPres symmetric) 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 eqvtI) 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: inputPres) next case(cSym P Q) thus ?case by(blast dest: symmetric) 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)) | a b P Q. P ≈ Q}" from assms have "(a{b}.(P), a{b}.(Q)) ∈ ?X" by auto thus ?thesis by(coinduct rule: weakBisimCoinduct) (auto simp add: pi.inject intro: Weak_Late_Sim_Pres.outputPres symmetric) qed lemma resPres: fixes P :: pi and Q :: pi and x :: name assumes PBiSimQ: "P ≈ Q" shows "<νx>P ≈ <νx>Q" proof - let ?X = "{x. ∃P Q. P ≈ Q ∧ (∃a. x = (<νa>P, <νa>Q))}" from PBiSimQ have "(<νx>P, <νx>Q) ∈ ?X" by blast moreover have "⋀P Q a. P ↝⇧^{^}<weakBisim> Q ⟹ <νa>P ↝⇧^{^}<(?X ∪ weakBisim)> <νa>Q" proof - fix P Q a assume PSimQ: "P ↝⇧^{^}<weakBisim> Q" moreover have "⋀P Q a. P ≈ Q ⟹ (<νa>P, <νa>Q) ∈ ?X ∪ weakBisim" by blast moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast moreover have "eqvt weakBisim" by(rule eqvt) moreover have "eqvt (?X ∪ weakBisim)" by(auto simp add: eqvt_def dest: eqvtI)+ ultimately show "<νa>P ↝⇧^{^}<(?X ∪ weakBisim)> <νa>Q" by(rule Weak_Late_Sim_Pres.resPres) qed ultimately show ?thesis using PBiSimQ by(coinduct rule: weakBisimCoinductAux, blast dest: unfoldE) 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 assms have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by auto thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P Q) { fix P Q a b assume "P ≈ Q" hence "P ↝⇧^{^}<weakBisim> Q" by(rule unfoldE) moreover { fix P Q a assume "P ≈ Q" moreover have "[a⌢a]P ≈ P" by(rule matchId) ultimately have "[a⌢a]P ≈ Q" by(blast intro: transitive) } moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast ultimately have "[a⌢b]P ↝⇧^{^}<(?X ∪ weakBisim)> [a⌢b]Q" by(rule matchPres) } with ‹(P, Q) ∈ ?X› show ?case by auto next case(cSym P Q) thus ?case by(auto simp add: pi.inject dest: symmetric) 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 assms have "([a≠b]P, [a≠b]Q) ∈ ?X" by auto thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P Q) { fix P Q a b assume "P ≈ Q" hence "P ↝⇧^{^}<weakBisim> Q" by(rule unfoldE) moreover { fix P Q a b assume "P ≈ Q" and "(a::name) ≠ b" note ‹P ≈ Q› moreover from ‹a ≠ b› have "[a≠b]P ≈ P" by(rule mismatchId) ultimately have "[a≠b]P ≈ Q" by(blast intro: transitive) } moreover have "weakBisim ⊆ ?X ∪ weakBisim" by blast ultimately have "[a≠b]P ↝⇧^{^}<(?X ∪ weakBisim)> [a≠b]Q" by(rule mismatchPres) } with ‹(P, Q) ∈ ?X› show ?case by auto next case(cSym P Q) thus ?case by(auto simp add: pi.inject dest: symmetric) qed qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi assumes "P ≈ Q" shows "P ∥ R ≈ Q ∥ R" proof - let ?ParSet = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P Q R. P ≈ Q}" have BC: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto from assms have "(P ∥ R, Q ∥ R) ∈ ?ParSet" by(blast intro: BC) thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim PR QR) { fix P Q R lst assume "P ≈ Q" from eqvtI have "eqvt (?ParSet ∪ weakBisim)" by(auto simp add: eqvt_def, blast) moreover have "⋀P Q a. (P, Q) ∈ ?ParSet ∪ weakBisim ⟹ (<νa>P, <νa>Q) ∈ ?ParSet ∪ weakBisim" by(blast intro: resChain.step[THEN sym] resPres) moreover { from ‹P ≈ Q› have "P ↝⇧^{^}<weakBisim> Q" by(rule unfoldE) moreover note ‹P ≈ Q› moreover { fix P Q R assume "P ≈ Q" moreover have "P ∥ R = resChain [] (P ∥ R)" by simp moreover have "Q ∥ R = resChain [] (Q ∥ R)" by simp ultimately have "(P ∥ R, Q ∥ R) ∈ ?ParSet ∪ weakBisim" by blast } moreover { fix P Q a assume A: "(P, Q) ∈ ?ParSet ∪ weakBisim" hence "(<νa>P, <νa>Q) ∈ ?ParSet ∪ weakBisim" (is "?goal") apply(auto intro: resPres) by(rule_tac x="a#lst" in exI) auto } ultimately have "(P ∥ R) ↝⇧^{^}<(?ParSet ∪ weakBisim)> (Q ∥ R)" using eqvt ‹eqvt(?ParSet ∪ weakBisim)› by(rule Weak_Late_Sim_Pres.parPres) } ultimately have "resChain lst (P ∥ R) ↝⇧^{^}<(?ParSet ∪ weakBisim)> resChain lst (Q ∥ R)" by(rule resChainI) } with ‹(PR, QR) ∈ ?ParSet› show ?case by blast next case(cSym PR QR) thus ?case by(auto dest: symmetric) 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_Late_Bisim.bisim O (bangRel weakBisim) O Strong_Late_Bisim.bisim" from eqvt Strong_Late_Bisim.bisimEqvt have eqvtY: "eqvt ?Y" by(blast intro: eqvtBangRel) have XsubY: "?X ⊆ ?Y" by(auto intro: Strong_Late_Bisim.reflexive) have RelStay: "⋀P Q. (P ∥ !P, Q) ∈ ?Y ⟹ (!P, Q) ∈ ?Y" proof(auto) fix P Q R T assume PBisimQ: "P ∥ !P ∼ Q" and QBRR: "(Q, R) ∈ bangRel weakBisim" and RBisimT: "R ∼ T" have "!P ∼ Q" proof - have "!P ∼ P ∥ !P" by(rule Strong_Late_Bisim_SC.bangSC) thus ?thesis using PBisimQ by(rule Strong_Late_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' ∼ T" and RBisimR': "R ∼ R'" and R'BRT': "(R', T') ∈ bangRel weakBisim" have "P ∥ R ∼ P ∥ R'" proof - from RBisimR' have "R ∥ P ∼ R' ∥ P" by(rule Strong_Late_Bisim_Pres.parPres) moreover have "P ∥ R ∼ R ∥ P" and "R' ∥ P ∼ P ∥ R'" by(rule Strong_Late_Bisim_SC.parSym)+ ultimately show ?thesis by(blast intro: Strong_Late_Bisim.transitive) qed moreover from PBisimQ R'BRT' have "(P ∥ R', Q ∥ T') ∈ bangRel weakBisim" by(rule BRPar) moreover have "Q ∥ T' ∼ Q ∥ T" proof - from T'BisimT have "T' ∥ Q ∼ T ∥ Q" by(rule Strong_Late_Bisim_Pres.parPres) moreover have "Q ∥ T' ∼ T' ∥ Q" and "T ∥ Q ∼ Q ∥ T" by(rule Strong_Late_Bisim_SC.parSym)+ ultimately show ?thesis by(blast intro: Strong_Late_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_Late_Bisim_Pres.resPres transitive) from PBisimQ have "(!P, !Q) ∈ ?X" by(rule BRBang) moreover from eqvt have "eqvt (bangRel weakBisim)" by(rule eqvtBangRel) ultimately show ?thesis proof(coinduct rule: weakBisimTransitiveCoinduct) case(cSim P Q) from ‹(P, Q) ∈ ?X› show "P ↝⇧^{^}<?Y> Q" proof(induct) case(BRBang P Q) have "P ≈ Q" by fact moreover hence "P ↝⇧^{^}<weakBisim> Q" by(blast dest: unfoldE) moreover have "⋀P Q. P ≈ Q ⟹ P ↝⇧^{^}<weakBisim> Q" by(blast dest: unfoldE) moreover from Strong_Late_Bisim.bisimEqvt eqvt have "eqvt ?Y" by(blast intro: eqvtBangRel) ultimately show "!P ↝⇧^{^}<?Y> !Q" using ParCompose ResCong RelStay XsubY by(rule_tac Weak_Late_Sim_Pres.bangPres, simp_all) next case(BRPar P Q R T) have PBiSimQ: "P ≈ Q" by fact have RBangRelT: "(R, T) ∈ ?X" by fact have RSimT: "R ↝⇧^{^}<?Y> T" by fact moreover from PBiSimQ have "P ↝⇧^{^}<weakBisim> Q" by(blast dest: unfoldE) moreover from RBangRelT have "(R, T) ∈ ?Y" by(blast intro: Strong_Late_Bisim.reflexive) ultimately show "P ∥ R ↝⇧^{^}<?Y> Q ∥ T" using ParCompose ResCong eqvt eqvtY ‹P ≈ Q› by(rule_tac Weak_Late_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_Late_Sim_Pres.resPres, simp_all) qed next case(cSym P Q) thus ?case by(metis symmetric bangRelSymetric) qed qed end