(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Bisim imports Weak_Late_Sim Strong_Late_Bisim begin lemma monoAux: "A ⊆ B ⟹ P ↝⇧^{^}<A> Q ⟶ P ↝⇧^{^}<B> Q" by(auto intro: Weak_Late_Sim.monotonic) coinductive_set weakBisim :: "(pi × pi) set" where step: "⟦P ↝⇧^{^}<weakBisim> Q; (Q, P) ∈ weakBisim⟧ ⟹ (P, Q) ∈ weakBisim" monos monoAux abbreviation "weakBisimJudge" (infixr ‹≈› 65) where "P ≈ Q ≡ (P, Q) ∈ weakBisim" lemma weakBisimCoinductAux[case_names weakBisim, case_conclusion weakBisim step, consumes 1]: assumes p: "(P, Q) ∈ X" and step: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<(X ∪ weakBisim)> Q ∧ ((Q, P) ∈ X ∨ Q ≈ P)" shows "P ≈ Q" proof - have aux: "X ∪ weakBisim = {(P, Q). (P, Q) ∈ X ∨ P ≈ Q}" by blast from p show ?thesis by(coinduct, force dest: step simp add: aux) qed lemma weakBisimCoinduct[consumes 1, case_names cSim cSym]: fixes P :: pi and Q :: pi assumes "(P, Q) ∈ X" and "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<(X ∪ weakBisim)> Q" and "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X" shows "P ≈ Q" using assms by(coinduct rule: weakBisimCoinductAux) auto lemma weak_coinduct[case_names weakBisim, case_conclusion weakBisim step, consumes 1]: assumes p: "(P, Q) ∈ X" and step: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<X> Q ∧ (Q, P) ∈ X" shows "P ≈ Q" using p proof(coinduct rule: weakBisimCoinductAux) case (weakBisim P Q) from step[OF this] show ?case using Weak_Late_Sim.monotonic by blast qed lemma weakBisimWeakCoinduct[consumes 1, case_names cSim cSym]: fixes P :: pi and Q :: pi assumes "(P, Q) ∈ X" and "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<X> Q" and "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X" shows "P ≈ Q" using assms by(coinduct rule: weak_coinduct) auto lemma monotonic: "mono(λp x1 x2. ∃P Q. x1 = P ∧ x2 = Q ∧ P ↝⇧^{^}<{(xa, x). p xa x}> Q ∧ Q ↝⇧^{^}<{(xa, x). p xa x}> P)" by(auto intro: monoI Weak_Late_Sim.monotonic) lemma unfoldE: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "P ↝⇧^{^}<weakBisim> Q" and "Q ≈ P" using assms by(auto intro: weakBisim.cases) lemma unfoldI: fixes P :: pi and Q :: pi assumes "P ↝⇧^{^}<weakBisim> Q" and "Q ≈ P" shows "P ≈ Q" using assms by(auto intro: weakBisim.cases) lemma eqvt: shows "eqvt weakBisim" proof(auto simp add: eqvt_def) let ?X = "{x. ∃P Q (perm::name prm). P ≈ Q ∧ x = (perm ∙ P, perm ∙ Q)}" fix P Q fix perm::"name prm" assume PBiSimQ: "P ≈ Q" hence "(perm ∙ P, perm ∙ Q) ∈ ?X" by blast moreover have "⋀P Q perm::name prm. ⟦P ↝⇧^{^}<weakBisim> Q⟧ ⟹ (perm ∙ P) ↝⇧^{^}<?X> (perm ∙ Q)" proof - fix P Q fix perm::"name prm" assume "P ↝⇧^{^}<weakBisim> Q" moreover have "weakBisim ⊆ ?X" proof(auto) fix P Q assume "P ≈ Q" moreover have "P = ([]::name prm) ∙ P" and "Q = ([]::name prm) ∙ Q" by auto ultimately show "∃P' Q'. P' ≈ Q' ∧ (∃(perm::name prm). P = perm ∙ P' ∧ Q = perm ∙ Q')" by blast qed moreover have "eqvt ?X" proof(auto simp add: eqvt_def) fix P Q fix perm1::"name prm" fix perm2::"name prm" assume "P ≈ Q" moreover have "perm1 ∙ perm2 ∙ P = (perm1 @ perm2) ∙ P" by(simp add: pt2[OF pt_name_inst]) moreover have "perm1 ∙ perm2 ∙ Q = (perm1 @ perm2) ∙ Q" by(simp add: pt2[OF pt_name_inst]) ultimately show "∃P' Q'. P' ≈ Q' ∧ (∃(perm::name prm). perm1 ∙ perm2 ∙ P = perm ∙ P' ∧ perm1 ∙ perm2 ∙ Q = perm ∙ Q')" by blast qed ultimately show "(perm ∙ P) ↝⇧^{^}<?X> (perm ∙ Q)" by(rule Weak_Late_Sim.eqvtI) qed ultimately show "(perm ∙ P) ≈ (perm ∙ Q)" by(coinduct rule: weak_coinduct, blast dest: unfoldE) qed lemma eqvtI: fixes P :: pi and Q :: pi and perm :: "name prm" assumes "P ≈ Q" shows "(perm ∙ P) ≈ (perm ∙ Q)" using assms by(rule eqvtRelI[OF eqvt]) lemma weakBisimEqvt[simp]: shows "eqvt weakBisim" by(auto simp add: eqvt_def eqvtI) lemma strongBisimWeakBisim: fixes P :: pi and Q :: pi assumes PSimQ: "P ∼ Q" shows "P ≈ Q" proof - have "⋀P Q. P ↝[bisim] Q ⟹ P ↝⇧^{^}<(bisim ∪ weakBisim)> Q" proof - fix P Q assume "P ↝[bisim] Q" hence "P ↝⇧^{^}<bisim> Q" by(rule strongSimWeakSim) thus "P ↝⇧^{^}<(bisim ∪ weakBisim)> Q" by(blast intro: Weak_Late_Sim.monotonic) qed with PSimQ show ?thesis by(coinduct rule: weakBisimCoinductAux, force dest: Strong_Late_Bisim.bisimE symmetric) qed lemma reflexive: fixes P :: pi shows "P ≈ P" proof - have "(P, P) ∈ Id" by simp then show ?thesis proof (coinduct rule: weak_coinduct) case (weakBisim P Q) have "(P, Q) ∈ Id" by fact thus ?case by(auto intro: Weak_Late_Sim.reflexive) qed qed lemma symmetric: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "Q ≈ P" using assms by(auto dest: unfoldE intro: unfoldI) lemma transitive: fixes P :: pi and Q :: pi and R :: pi assumes PBiSimQ: "P ≈ Q" and QBiSimR: "Q ≈ R" shows "P ≈ R" proof - let ?X = "weakBisim O weakBisim" from assms have "(P, R) ∈ ?X" by blast moreover have "⋀P Q R. ⟦Q ↝⇧^{^}<weakBisim> R; P ≈ Q⟧ ⟹ P ↝⇧^{^}<(?X ∪ weakBisim)> R" proof - fix P Q R assume PBiSimQ: "P ≈ Q" assume "Q ↝⇧^{^}<weakBisim> R" moreover have "eqvt weakBisim" by(rule eqvt) moreover from eqvt have "eqvt (?X ∪ weakBisim)" by(auto simp add: eqvtTrans) moreover have "weakBisim O weakBisim ⊆ ?X ∪ weakBisim" by auto moreover have "⋀P Q. P ≈ Q ⟹ P ↝⇧^{^}<weakBisim> Q" by(rule unfoldE) ultimately show "P ↝⇧^{^}<(?X ∪ weakBisim)> R" using PBiSimQ by(rule Weak_Late_Sim.transitive) qed ultimately show ?thesis apply(coinduct rule: weakBisimCoinduct, auto) by(blast dest: unfoldE symmetric)+ qed lemma transitive_coinduct_weak[case_names WeakBisimEarly, case_conclusion WeakBisimEarly step, consumes 2]: assumes p: "(P, Q) ∈ X" and Eqvt: "eqvt X" and step: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<(bisim O X O bisim)> Q ∧ (Q, P) ∈ X" shows "P ≈ Q" proof - let ?X = "bisim O X O bisim" have Sim: "⋀P P' Q' Q. ⟦P ∼ P'; P'↝⇧^{^}<?X> Q'; Q' ↝[bisim] Q⟧ ⟹ P ↝⇧^{^}<?X> Q" proof - fix P P' Q' Q assume PBisimP': "P ∼ P'" assume P'SimQ': "P' ↝⇧^{^}<?X> Q'" assume Q'SimQ: "Q' ↝[bisim] Q" show "P ↝⇧^{^}<?X> Q" proof - have "P' ↝⇧^{^}<?X> Q" proof - have "?X O bisim ⊆ ?X" by(blast intro: Strong_Late_Bisim.transitive) moreover from Strong_Late_Bisim.bisimEqvt Eqvt have "eqvt ?X" by blast ultimately show ?thesis using P'SimQ' Q'SimQ by(blast intro: strongAppend) qed moreover have "eqvt bisim" by(rule Strong_Late_Bisim.bisimEqvt) moreover from Strong_Late_Bisim.bisimEqvt Eqvt have "eqvt ?X" by blast moreover have "bisim O ?X ⊆ ?X" by(blast intro: Strong_Late_Bisim.transitive) moreover have "⋀P Q. P ∼ Q ⟹ P ↝⇧^{^}<bisim> Q" by(blast dest: Strong_Late_Bisim.bisimE strongSimWeakSim) ultimately show ?thesis using PBisimP' by(rule Weak_Late_Sim.transitive) qed qed from p have "(P, Q) ∈ ?X" by(blast intro: Strong_Late_Bisim.reflexive) moreover from step Sim have "⋀P Q. (P, Q) ∈ ?X ⟹ P ↝⇧^{^}<?X> Q ∧ (Q, P) ∈ ?X" by(blast dest: Strong_Late_Bisim.bisimE Strong_Late_Bisim.symmetric) ultimately show ?thesis by(rule weak_coinduct) qed lemma weakBisimTransitiveCoinduct[case_names cSim cSym, consumes 2]: assumes p: "(P, Q) ∈ X" and Eqvt: "eqvt X" and rSim: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^{^}<(bisim O X O bisim)> Q" and rSym: "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X" shows "P ≈ Q" using assms by(coinduct rule: transitive_coinduct_weak) auto end