(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Bisim imports Strong_Late_Sim begin lemma monoAux: "A ⊆ B ⟹ P ↝[A] Q ⟶ P ↝[B] Q" by(auto intro: Strong_Late_Sim.monotonic) coinductive_set bisim :: "(pi × pi) set" where step: "⟦P ↝[bisim] Q; (Q, P) ∈ bisim⟧ ⟹ (P, Q) ∈ bisim" monos monoAux abbreviation strongBisimJudge (infixr ‹∼› 65) where "P ∼ Q ≡ (P, Q) ∈ bisim" lemma monotonic': "mono(λS. {(P, Q) |P Q. P ↝[S] Q ∧ Q ↝[S] P})" apply(rule monoI) by(auto dest: monoAux) 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)" apply(rule monoI) by(auto intro: Strong_Late_Sim.monotonic) lemma bisimCoinduct[case_names cSim cSym , consumes 1]: assumes p: "(P, Q) ∈ X" and rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝[(X ∪ bisim)] S" and rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X" shows "P ∼ Q" proof - have aux: "X ∪ bisim = {(P, Q). (P, Q) ∈ X ∨ P ∼ Q}" by blast from p show ?thesis apply(coinduct, auto) apply(fastforce dest: rSim simp add: aux) by(fastforce dest: rSym) qed lemma bisimE: fixes P :: pi and Q :: pi assumes "P ∼ Q" shows "P ↝[bisim] Q" using assms by(auto intro: bisim.cases) lemma bisimI: fixes P :: pi and Q :: pi assumes "P ↝[bisim] Q" and "Q ∼ P" shows "P ∼ Q" using assms by(rule bisim.intros) definition old_bisim :: "(pi × pi) set ⇒ bool" where "old_bisim Rel ≡ ∀(P, Q) ∈ Rel. P ↝[Rel] Q ∧ (Q, P) ∈ Rel" lemma oldBisimBisimEq: shows "(⋃{Rel. (old_bisim Rel)}) = bisim" (is "?LHS = ?RHS") proof show "?LHS ⊆ ?RHS" proof auto fix P Q Rel assume "(P, Q) ∈ Rel" and "old_bisim Rel" thus "P ∼ Q" proof(coinduct rule: bisimCoinduct) case(cSim P Q) with ‹old_bisim Rel› show ?case by(fastforce simp add: old_bisim_def intro: Strong_Late_Sim.monotonic) next case(cSym P Q) with ‹old_bisim Rel› show ?case by(auto simp add: old_bisim_def) qed qed next show "?RHS ⊆ ?LHS" proof auto fix P Q assume "P ∼ Q" moreover hence "old_bisim bisim" by(auto simp add: old_bisim_def dest: bisim.cases) ultimately show "∃Rel. old_bisim Rel ∧ (P, Q) ∈ Rel" by blast qed qed lemma reflexive: fixes P :: pi shows "P ∼ P" proof - have "(P, P) ∈ Id" by simp thus ?thesis by(coinduct rule: bisimCoinduct, auto intro: Strong_Late_Sim.reflexive) qed lemma symmetric: fixes P :: pi and Q :: pi assumes "P ∼ Q" shows "Q ∼ P" using assms by(auto dest: bisim.cases) lemma bisimClosed: fixes P :: pi and Q :: pi and p :: "name prm" assumes "P ∼ Q" shows "(p ∙ P) ∼ (p ∙ Q)" proof - let ?X = "{(p ∙ P, p ∙ Q) | P Q (p::name prm). P ∼ Q}" from ‹P ∼ Q› have "(p ∙ P, p ∙ Q) ∈ ?X" by blast thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim pP pQ) from ‹(pP, pQ) ∈ ?X› obtain P Q p where "P ∼ Q" and "pP = (p::name prm) ∙ P" and "pQ = p ∙ Q" by auto from ‹P ∼ Q› have "P ↝[bisim] Q" by(rule bisimE) moreover have "bisim ⊆ ?X" proof fix x assume "x ∈ bisim" moreover have "x = (([]::name prm) ∙ x)" by auto ultimately show "x ∈ ?X" apply(case_tac x) by(clarify, simp only: eqvts) metis 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'. (∃(perm::name prm). perm1 ∙ perm2 ∙ P = perm ∙ P' ∧ perm1 ∙ perm2 ∙ Q = perm ∙ Q') ∧ P' ∼ Q'" by blast qed ultimately have "(p ∙ P) ↝[?X] (p ∙ Q)" by(rule Strong_Late_Sim.eqvtI) with ‹pP = p ∙ P› ‹pQ = p ∙ Q› show ?case by(force intro: Strong_Late_Sim.monotonic) next case(cSym P Q) thus ?case by(auto intro: symmetric) qed qed lemma bisimEqvt[simp]: shows "eqvt bisim" by(auto simp add: eqvt_def bisimClosed) lemma transitive: fixes P :: pi and Q :: pi and R :: pi assumes "P ∼ Q" and "Q ∼ R" shows "P ∼ R" proof - let ?X = "bisim O bisim" from assms have "(P, R) ∈ ?X" by blast thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim P R) thus ?case by(fastforce intro: Strong_Late_Sim.transitive dest: bisimE simp add: eqvtTrans) next case(cSym P R) thus ?case by(auto dest: symmetric) qed qed lemma bisimTransitiveCoinduct[case_names cSim cSym, case_conclusion bisim step, consumes 2]: assumes "(P, Q) ∈ X" and "eqvt X" and rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝[(bisim O (X ∪ bisim) O bisim)] S" and rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ bisim O (X ∪ bisim) O bisim" shows "P ∼ Q" proof - let ?X = "bisim O (X ∪ bisim) O bisim" from ‹(P, Q) ∈ X› have "(P, Q) ∈ ?X" by(auto intro: reflexive) thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim P Q) { fix P P' Q' Q assume "P ∼ P'" and "(P', Q') ∈ X ∪ bisim" and "Q' ∼ Q" have "P ↝[(?X ∪ bisim)] Q" proof(cases "(P', Q') ∈ X") case True from ‹P ∼ P'› have "P ↝[bisim] P'" by(rule bisimE) moreover from ‹(P', Q') ∈ X› have "P' ↝[(?X)] Q'" by(rule rSim) moreover from ‹eqvt X› bisimEqvt have "eqvt(?X ∪ bisim)" by blast moreover have "bisim O ?X ⊆ ?X ∪ bisim" by(auto dest: transitive) ultimately have "P ↝[(?X ∪ bisim)] Q'" by(rule Strong_Late_Sim.transitive) moreover from ‹Q' ∼ Q› have "Q' ↝[bisim] Q" by(rule bisimE) moreover note ‹eqvt(?X ∪ bisim)› moreover have "(?X ∪ bisim) O bisim ⊆ ?X ∪ bisim" by auto (blast dest: transitive)+ ultimately show ?thesis by(rule Strong_Late_Sim.transitive) next case False from ‹(P', Q') ∉ X› ‹(P', Q') ∈ X ∪ bisim› have "P' ∼ Q'" by simp with ‹P ∼ P'› ‹Q' ∼ Q› have "P ∼ Q" by(blast dest: transitive) hence "P ↝[bisim] Q" by(rule bisimE) moreover have "bisim ⊆ ?X ∪ bisim" by auto ultimately show ?thesis by(rule Strong_Late_Sim.monotonic) qed } with ‹(P, Q) ∈ ?X› show ?case by auto case(cSym P Q) { fix P P' Q' Q assume "P ∼ P'" and "(P', Q') ∈ X ∪ bisim" and "Q' ∼ Q" have "(Q, P) ∈ bisim O (X ∪ bisim) O bisim" proof(cases "(P', Q') ∈ X") case True from ‹(P', Q') ∈ X› have "(Q', P') ∈ ?X" by(rule rSym) then obtain Q'' P'' where "Q' ∼ Q''" and "(Q'', P'') ∈ X ∪ bisim" and "P'' ∼ P'" by auto from ‹Q' ∼ Q› ‹Q' ∼ Q''› have "Q ∼ Q''" by(metis transitive symmetric) moreover from ‹P ∼ P'› ‹P'' ∼ P'› have "P'' ∼ P" by(metis transitive symmetric) ultimately show ?thesis using ‹(Q'', P'') ∈ X ∪ bisim› by blast next case False from ‹(P', Q') ∉ X› ‹(P', Q') ∈ X ∪ bisim› have "P' ∼ Q'" by simp with ‹P ∼ P'› ‹Q' ∼ Q› have "Q ∼ P" by(metis transitive symmetric) thus ?thesis by(blast intro: reflexive) qed } with ‹(P, Q) ∈ ?X› show ?case by blast qed qed end