(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Early_Bisim imports Weak_Early_Sim Strong_Early_Bisim begin lemma monoAux: "A ⊆ B ⟹ P ↝<A> Q ⟶ P ↝<B> Q" by(auto intro: Weak_Early_Sim.monotonic) coinductive_set weakBisim :: "(pi × pi) set" where step: "⟦P ↝<weakBisim> Q; (Q, P) ∈ weakBisim⟧ ⟹ (P, Q) ∈ weakBisim" monos monoAux abbreviation weakEarlyBisimJudge (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 ∪ weakBisim" 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 weakBisimWeakCoinductAux[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) from step[OF this] show ?case using Weak_Early_Sim.monotonic by blast qed lemma weakBisimCoinduct[consumes 1, case_names cSim cSym]: fixes P :: pi and Q :: pi and X :: "(pi × pi) set" assumes "(P, Q) ∈ X" and "⋀R S. (R, S) ∈ X ⟹ R ↝<(X ∪ weakBisim)> S" and "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X" shows "P ≈ Q" using assms by(coinduct rule: weakBisimCoinductAux) auto lemma weakBisimWeakCoinduct[consumes 1, case_names cSim cSym]: fixes P :: pi and Q :: pi and X :: "(pi × pi) set" 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: weakBisimWeakCoinductAux) auto lemma weakBisimE: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "P ↝<weakBisim> Q" and "Q ≈ P" using assms by(auto dest: weakBisim.cases) lemma weakBisimI: fixes P :: pi and Q :: pi assumes "P ↝<weakBisim> Q" and "Q ≈ P" shows "P ≈ Q" using assms by(auto intro: weakBisim.intros) lemma eqvt[simp]: 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_Early_Sim.eqvtI) qed ultimately show "(perm ∙ P) ≈ (perm ∙ Q)" by(coinduct rule: weakBisimWeakCoinductAux, blast dest: weakBisimE) qed lemma eqvtI[eqvt]: 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 strongBisimWeakBisim: fixes P :: pi and Q :: pi assumes "P ∼ Q" shows "P ≈ Q" proof - from ‹P ∼ Q› show ?thesis proof(coinduct rule: weakBisimWeakCoinduct) case(cSim P Q) from ‹P ∼ Q› have "P ↝[bisim] Q" by(rule bisimE) thus "P ↝<bisim> Q" by(rule strongSimWeakSim) next case(cSym P Q) thus ?case by(rule bisimE) qed qed lemma reflexive: fixes P :: pi shows "P ≈ P" proof - have "(P, P) ∈ Id" by simp thus ?thesis by(coinduct rule: weakBisimCoinduct) (auto intro: Weak_Early_Sim.reflexive) qed lemma symetric: fixes P :: pi and Q :: pi assumes "P ≈ Q" shows "Q ≈ P" using assms by(auto dest: weakBisimE) lemma transitive: fixes P :: pi and Q :: pi and R :: pi assumes "P ≈ Q" and "Q ≈ R" shows "P ≈ R" proof - let ?X = "weakBisim O weakBisim" from assms have "(P, R) ∈ ?X" by blast thus ?thesis proof(coinduct rule: weakBisimCoinduct) case(cSim P R) from ‹(P, R) ∈ ?X› obtain Q where "P ≈ Q" and "Q ≈ R" by auto from ‹Q ≈ R› have "Q ↝<weakBisim> R" by(rule weakBisimE) moreover have "eqvt ?X" by auto moreover have "?X ⊆ ?X" by simp ultimately show "P ↝<(?X ∪ weakBisim)> R" using weakBisimE(1) ‹P ≈ Q› by(rule_tac Weak_Early_Sim.transitive) auto next case(cSym P R) thus ?case by(auto dest: symetric) qed qed lemma weakBisimWeakUpto[case_names cSim cSym, consumes 1]: assumes p: "(P, Q) ∈ X" and Eqvt: "eqvt X" and rSim: "⋀P Q. (P, Q) ∈ X ⟹ P ↝<(weakBisim O X O bisim)> Q" and rSym: "⋀ P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X" shows "P ≈ Q" proof - let ?X = "weakBisim O X O weakBisim" let ?Y = "weakBisim O X O bisim" from Eqvt eqvt have "eqvt ?X" by blast from Strong_Early_Bisim.eqvt Eqvt eqvt have "eqvt ?Y" by blast from ‹(P, Q) ∈ X› have "(P, Q) ∈ ?X" by(blast intro: Strong_Early_Bisim.reflexive reflexive) thus ?thesis proof(coinduct rule: weakBisimWeakCoinduct) case(cSim P Q) { fix P P' Q' Q assume "P ≈ P'" and "(P', Q') ∈ X" and "Q' ≈ Q" from ‹Q' ≈ Q› have "Q' ↝<weakBisim> Q" by(rule weakBisimE) moreover note ‹eqvt ?Y› ‹eqvt ?X› moreover have "?Y O weakBisim ⊆ ?X" by(blast dest: strongBisimWeakBisim transitive) moreover { fix P Q assume "(P, Q) ∈ ?Y" then obtain P' Q' where "P ≈ P'" and "(P', Q') ∈ X" and "Q' ∼ Q" by auto from ‹(P', Q') ∈ X› have "P' ↝<?Y> Q'" by(rule rSim) moreover from ‹Q' ∼ Q› have "Q' ↝[bisim] Q" by(rule bisimE) moreover note ‹eqvt ?Y› moreover have "?Y O bisim ⊆ ?Y" by(auto dest: Strong_Early_Bisim.transitive) ultimately have "P' ↝<?Y> Q" by(rule strongAppend) moreover note ‹P ≈ P'› moreover have "weakBisim O ?Y ⊆ ?Y" by(blast dest: transitive) ultimately have "P ↝<?Y> Q" using weakBisimE(1) eqvt ‹eqvt ?Y› by(rule_tac Weak_Early_Sim.transitive) } moreover from ‹(P', Q') ∈ X› have "(P', Q') ∈ ?Y" by(blast intro: reflexive Strong_Early_Bisim.reflexive) ultimately have "P' ↝<?X> Q" by(rule Weak_Early_Sim.transitive) moreover note ‹P ≈ P'› moreover have "weakBisim O ?X ⊆ ?X" by(blast dest: transitive) ultimately have "P ↝<?X> Q" using weakBisimE(1) eqvt ‹eqvt ?X› by(rule_tac Weak_Early_Sim.transitive) } with ‹(P, Q) ∈ ?X› show ?case by auto next case(cSym P Q) thus ?case apply auto by(blast dest: bisimE rSym weakBisimE) qed qed lemma weakBisimUpto[case_names cSim cSym, consumes 1]: assumes p: "(P, Q) ∈ X" and Eqvt: "eqvt X" and rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝<(weakBisim O (X ∪ weakBisim) O bisim)> S" and rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X" shows "P ≈ Q" proof - from p have "(P, Q) ∈ X ∪ weakBisim" by simp thus ?thesis using Eqvt apply(coinduct rule: weakBisimWeakUpto) apply(auto dest: rSim rSym weakBisimE) apply(rule Weak_Early_Sim.monotonic) apply(blast dest: weakBisimE) apply(auto simp add: relcomp_unfold) by(metis reflexive Strong_Early_Bisim.reflexive transitive) qed lemma transitive_coinduct_weak[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) ∈ bisim O X O bisim" shows "P ≈ Q" proof - let ?X = "bisim O X O bisim" from ‹(P, Q) ∈ X› have "(P, Q) ∈ ?X" by(blast intro: Strong_Early_Bisim.reflexive) thus ?thesis proof(coinduct rule: weakBisimWeakCoinduct) case(cSim P Q) { fix P P' Q' Q assume PBisimP': "P ∼ P'" assume P'SimQ': "P' ↝<?X> Q'" assume Q'SimQ: "Q' ↝[bisim] Q" have "P ↝<?X> Q" proof - have "P' ↝<?X> Q" proof - have "?X O bisim ⊆ ?X" by(blast intro: Strong_Early_Bisim.transitive) moreover from Strong_Early_Bisim.eqvt Eqvt have "eqvt ?X" by blast ultimately show ?thesis using P'SimQ' Q'SimQ by(rule_tac strongAppend) qed moreover have "eqvt bisim" by(rule Strong_Early_Bisim.eqvt) moreover from Strong_Early_Bisim.eqvt Eqvt have "eqvt ?X" by blast moreover have "bisim O ?X ⊆ ?X" by(blast intro: Strong_Early_Bisim.transitive) moreover have "⋀P Q. P ∼ Q ⟹ P ↝<bisim> Q" by(blast dest: Strong_Early_Bisim.bisimE strongSimWeakSim) ultimately show ?thesis using PBisimP' by(rule Weak_Early_Sim.transitive) qed } thus ?case using ‹(P, Q) ∈ ?X› rSim by (blast dest: Strong_Early_Bisim.bisimE) next case(cSym P Q) { fix P P' Q' Q assume "P ∼ P'" and "(P', Q') ∈ X" and "Q' ∼ Q" from ‹(P', Q') ∈ X› have "(Q', P') ∈ ?X" by(rule rSym) with ‹P ∼ P'› ‹Q' ∼ Q› have "(Q, P) ∈ ?X" apply auto apply(drule_tac Strong_Early_Bisim.bisimE(2)) apply(drule Strong_Early_Bisim.transitive[where Q=P']) apply assumption apply(drule_tac Strong_Early_Bisim.bisimE(2)) apply(drule Strong_Early_Bisim.transitive[where Q=Q']) apply assumption by auto } thus ?case using ‹(P, Q) ∈ ?X› by auto qed qed end