(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Early_Bisim imports Strong_Early_Sim begin lemma monoAux: "A ⊆ B ⟹ P ↝[A] Q ⟶ P ↝[B] Q" by(auto intro: Strong_Early_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 bisimCoinductAux[case_names bisim, case_conclusion StrongBisim step, consumes 1]: assumes p: "(P, Q) ∈ X" and step: "⋀P Q. (P, Q) ∈ X ⟹ P ↝[(X ∪ bisim)] Q ∧ (Q, P) ∈ bisim ∪ X" shows "P ∼ Q" proof - have aux: "X ∪ bisim = {(P, Q). (P, Q) ∈ X ∨ P ∼ Q}" by blast from p show ?thesis by(coinduct, force dest: step simp add: aux) qed lemma bisimCoinduct[consumes 1, case_names cSim cSym]: fixes P :: pi and Q :: pi assumes "(P, Q) ∈ X" and "⋀R S. (R, S) ∈ X ⟹ R ↝[(X ∪ bisim)] S" and "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X" shows "P ∼ Q" using assms by(coinduct rule: bisimCoinductAux) auto lemma weak_coinduct[case_names bisim, case_conclusion StrongBisim 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: bisimCoinductAux) case (bisim P) from step[OF this] show ?case using Strong_Early_Sim.monotonic by blast qed lemma bisimWeakCoinduct[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)" apply(rule monoI) by(auto intro: Strong_Early_Sim.monotonic) lemma bisimE: fixes P :: pi and Q :: pi assumes "P ∼ Q" shows "P ↝[bisim] Q" and "Q ∼ P" using assms by(auto intro: bisim.cases) lemma bisimClosed[eqvt]: 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::name prm) P Q. P ∼ Q}" from assms have "(p ∙ P, p ∙ Q) ∈ ?X" by auto thus ?thesis proof(coinduct rule: bisimWeakCoinduct) case(cSim P Q) moreover { fix P Q fix p::"name prm" assume "P ↝[bisim] Q" moreover have "bisim ⊆ ?X" by(auto, rule_tac x="[]" in exI) auto moreover have "eqvt ?X" by(auto simp add: eqvt_def pt2[OF pt_name_inst, THEN sym]) blast ultimately have "(p ∙ P) ↝[?X] (p ∙ Q)" by(rule Strong_Early_Sim.eqvtI) } ultimately show ?case by(blast dest: bisimE) next case(cSym P Q) thus ?case by(blast dest: bisimE) qed qed lemma eqvt[simp]: shows "eqvt bisim" by(auto simp add: eqvt_def eqvts) lemma reflexive: fixes P :: pi shows "P ∼ P" proof - have "(P, P) ∈ Id" by simp then show ?thesis by(coinduct rule: bisimWeakCoinduct) (auto intro: Strong_Early_Sim.reflexive) qed 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 = "bisim O bisim" from assms have "(P, R) ∈ ?X" by blast thus ?thesis proof(coinduct rule: bisimWeakCoinduct) case(cSim P Q) moreover { fix P Q R assume "P ∼ Q" and "Q ∼ R" hence "P ↝[bisim] Q" and "Q ↝[bisim] R" by(metis bisimE)+ moreover from eqvt have "eqvt ?X" by(auto simp add: eqvtTrans) moreover have "bisim O bisim ⊆ ?X" by auto ultimately have "P ↝[?X] R" by(rule Strong_Early_Sim.transitive) } ultimately show ?case by auto next case(cSym P Q) thus ?case by(auto dest: bisimE) qed qed end