(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Sim imports Late_Semantics1 Rel begin definition derivative :: "pi ⇒ pi ⇒ subject ⇒ name ⇒ (pi × pi) set ⇒ bool" where "derivative P Q a x Rel ≡ case a of InputS b ⇒ (∀u. (P[x::=u], Q[x::=u]) ∈ Rel) | BoundOutputS b ⇒ (P, Q) ∈ Rel" definition simulation :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" (‹_ ↝[_] _› [80, 80, 80] 80) where "P ↝[Rel] Q ≡ (∀a x Q'. Q ⟼a«x» ≺ Q' ∧ x ♯ P ⟶ (∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x Rel)) ∧ (∀α Q'. Q ⟼α ≺ Q' ⟶ (∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel))" lemma monotonic: fixes A :: "(pi × pi) set" and B :: "(pi × pi) set" and P :: pi and P' :: pi assumes "P ↝[A] P'" and "A ⊆ B" shows "P ↝[B] P'" using assms apply(auto simp add: simulation_def derivative_def) by(case_tac a) fastforce+ lemma derivativeMonotonic: fixes A :: "(pi × pi) set" and B :: "(pi × pi) set" and P :: pi and Q :: pi and a :: subject and x :: name assumes "derivative P Q a x A" and "A ⊆ B" shows "derivative P Q a x B" using assms by(case_tac a, auto simp add: derivative_def) lemma derivativeEqvtI: fixes P :: pi and Q :: pi and a :: subject and x :: name and Rel :: "(pi × pi) set" and perm :: "name prm" assumes Der: "derivative P Q a x Rel" and Eqvt: "eqvt Rel" shows "derivative (perm ∙ P) (perm ∙ Q) (perm ∙ a) (perm ∙ x) Rel" using assms apply(case_tac a, auto simp add: derivative_def) apply(erule_tac x="rev perm ∙ u" in allE) apply(drule_tac perm=perm in eqvtRelI) apply(blast) apply(force simp add: eqvt_subs name_per_rev) by(force simp add: eqvt_def) lemma derivativeEqvtI2: fixes P :: pi and Q :: pi and a :: subject and x :: name and Rel :: "(pi × pi) set" and perm :: "name prm" assumes Der: "derivative P Q a x Rel" and Eqvt: "eqvt Rel" shows "derivative (perm ∙ P) (perm ∙ Q) a (perm ∙ x) Rel" using assms apply(case_tac a, auto simp add: derivative_def) apply(erule_tac x="rev perm ∙ u" in allE) apply(drule_tac perm=perm in eqvtRelI) apply(blast) apply(force simp add: eqvt_subs name_per_rev) by(force simp add: eqvt_def) lemma freshUnit[simp]: fixes y :: name shows "y ♯ ()" by(auto simp add: fresh_def supp_unit) lemma simCasesCont[consumes 1, case_names Bound Free]: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and C :: "'a::fs_name" assumes Eqvt: "eqvt Rel" and Bound: "⋀a x Q'. ⟦Q ⟼ a«x» ≺ Q'; x ♯ P; x ♯ Q; x ♯ a; x ♯ C⟧ ⟹ ∃P'. P ⟼ a«x» ≺ P' ∧ derivative P' Q' a x Rel" and Free: "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" shows "P ↝[Rel] Q" using Free proof(auto simp add: simulation_def) fix a x Q' assume "(x::name) ♯ P" assume Trans: "Q ⟼ a«x» ≺ Q'" obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ a" and "y ♯ C" and "y ♯ Q'" and "y ≠ x" by(generate_fresh "name") auto from Trans ‹y ♯ Q'› have "Q ⟼ a«y» ≺ [(x, y)] ∙ Q'" by(simp add: alphaBoundResidual) hence "∃P'. P ⟼ a«y» ≺ P' ∧ derivative P' ([(x, y)] ∙ Q') a y Rel" using ‹y ♯ P› ‹y ♯ Q› ‹y ♯ a› ‹y ♯ C› by(rule Bound) then obtain P' where PTrans: "P ⟼ a«y» ≺ P'" and PDer: "derivative P' ([(x, y)] ∙ Q') a y Rel" by blast from PTrans ‹x ♯ P› ‹y ≠ x› have "x ♯ P'" by(force intro: freshBoundDerivative) with PTrans have "P ⟼ a«x» ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual name_swap) moreover have "derivative ([(x, y)] ∙ P') Q' a x Rel" proof - from PDer Eqvt have "derivative ([(x, y)] ∙ P') ([(x, y)] ∙ [(x, y)] ∙ Q') a ([(x, y)] ∙ y) Rel" by(rule derivativeEqvtI2) with ‹y ≠ x› show ?thesis by(simp add: name_calc) qed ultimately show "∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x Rel" by blast qed lemma simCases[case_names Bound Free]: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes Bound: "⋀a y Q'. ⟦Q ⟼ a«y» ≺ Q'; y ♯ P⟧ ⟹ ∃P'. P ⟼ a«y» ≺ P' ∧ derivative P' Q' a y Rel" and Free: "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" shows "P ↝[Rel] Q" using assms by(auto simp add: simulation_def) lemma resSimCases[consumes 1, case_names BoundOutput BoundR FreeR]: fixes x :: name and P :: pi and Rel :: "(pi × pi) set" and Q :: pi and C :: "'a::fs_name" assumes Eqvt: "eqvt Rel" and BoundO: "⋀Q' a. ⟦Q ⟼a[x] ≺ Q'; a ≠ x⟧ ⟹ ∃P'. P ⟼a<νx> ≺ P' ∧ (P', Q') ∈ Rel" and BR: "⋀Q' a y. ⟦Q ⟼a«y» ≺ Q'; x ♯ a; x ≠ y; y ♯ C⟧ ⟹ ∃P'. P ⟼a«y» ≺ P' ∧ derivative P' (<νx>Q') a y Rel" and BF: "⋀Q' α. ⟦Q ⟼α ≺ Q'; x ♯ α⟧ ⟹ ∃P'. P ⟼α ≺ P' ∧ (P', <νx>Q') ∈ Rel" shows "P ↝[Rel] <νx>Q" using Eqvt proof(induct rule: simCasesCont[where C="(C, x, Q)"]) case(Bound a y Q') have "y ♯ (C, x, Q)" by fact hence yFreshC: "y ♯ C" and yineqx: "y ≠ x" and "y ♯ Q" by(simp add: fresh_prod)+ have "<νx>Q ⟼a«y» ≺ Q'" by fact thus ?case using yineqx ‹y ♯ Q› proof(induct rule: resCasesB) case(cOpen a' Q') have "Q ⟼a'[x] ≺ Q'" and "a' ≠ x" by fact+ then obtain P' where PTrans: "P ⟼a'<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(force dest: BoundO) from PTrans ‹y ♯ P› yineqx have "y ♯ P'" by(force dest: freshBoundDerivative) with PTrans have "P ⟼a'<νy> ≺ ([(x, y)] ∙ P')" by(simp add: alphaBoundResidual) moreover from P'RelQ' Eqvt have "([(x, y)] ∙ P', [(x, y)] ∙ Q') ∈ Rel" by(auto simp add: eqvt_def) ultimately show ?case by(force simp add: derivative_def name_swap) next case(cRes Q') have "Q ⟼a«y» ≺ Q'" and "x ♯ a" by fact+ with yineqx yFreshC show ?case by(force dest: BR) qed next case(Free α Q') have "<νx>Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: resCasesF) case(cRes Q') have "Q ⟼α ≺ Q'" and "x ♯ α" by fact+ thus ?case by(rule BF) qed qed lemma simE: fixes P :: pi and Rel :: "(pi × pi) set" and Q :: pi and a :: subject and x :: name and Q' :: pi assumes "P ↝[Rel] Q" shows "Q ⟼ a«x» ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟼ a«x» ≺ P' ∧ (derivative P' Q' a x Rel)" and "Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" using assms by(simp add: simulation_def)+ lemma eqvtI: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and perm :: "name prm" assumes Sim: "P ↝[Rel] Q" and RelRel': "Rel ⊆ Rel'" and EqvtRel': "eqvt Rel'" shows "(perm ∙ P) ↝[Rel'] (perm ∙ Q)" proof(induct rule: simCases) case(Bound a y Q') have QTrans: "(perm ∙ Q) ⟼ a«y» ≺ Q'" and yFreshP: "y ♯ perm ∙ P" by fact+ from QTrans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a«y» ≺ Q')" by(rule transitions.eqvt) hence "Q ⟼ (rev perm ∙ a)«(rev perm ∙ y)» ≺ (rev perm ∙ Q')" by(simp add: name_rev_per) moreover from yFreshP have "(rev perm ∙ y) ♯ P" by(simp add: name_fresh_left) ultimately have "∃P'. P ⟼ (rev perm ∙ a)«rev perm ∙ y» ≺ P' ∧ derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel" using Sim by(force intro: simE) then obtain P' where PTrans: "P ⟼ (rev perm ∙ a)«rev perm ∙ y» ≺ P'" and Pderivative: "derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel" by blast from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ a)«rev perm ∙ y» ≺ P')" by(rule transitions.eqvt) hence L1: "(perm ∙ P) ⟼ a«y» ≺ (perm ∙ P')" by(simp add: name_per_rev) from Pderivative RelRel' have "derivative P' (rev perm ∙ Q') (rev perm ∙ a) (rev perm ∙ y) Rel'" by(rule derivativeMonotonic) hence "derivative (perm ∙ P') (perm ∙ (rev perm ∙ Q')) (perm ∙ (rev perm ∙ a)) (perm ∙ (rev perm ∙ y)) Rel'" using EqvtRel' by(rule derivativeEqvtI) hence "derivative (perm ∙ P') Q' a y Rel'" by(simp add: name_per_rev) with L1 show ?case by blast next case(Free α Q') have "(perm ∙ Q) ⟼ α ≺ Q'" by fact hence "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (α ≺ Q')" by(rule transitions.eqvt) hence "Q ⟼ (rev perm ∙ α) ≺ (rev perm ∙ Q')" by(simp add: name_rev_per) with Sim have "∃P'. P ⟼ (rev perm ∙ α) ≺ P' ∧ (P', (rev perm ∙ Q')) ∈ Rel" by(force intro: simE) then obtain P' where PTrans: "P ⟼ (rev perm ∙ α) ≺ P'" and PRel: "(P', (rev perm ∙ Q')) ∈ Rel" by blast from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ α)≺ P')" by(rule transitions.eqvt) hence L1: "(perm ∙ P) ⟼ α ≺ (perm ∙ P')" by(simp add: name_per_rev) from PRel EqvtRel' RelRel' have "((perm ∙ P'), (perm ∙ (rev perm ∙ Q'))) ∈ Rel'" by(force intro: eqvtRelI) hence "((perm ∙ P'), Q') ∈ Rel'" by(simp add: name_per_rev) with L1 show "∃P'. (perm ∙ P) ⟼α ≺ P' ∧ (P', Q') ∈ Rel'" by blast qed lemma derivativeReflexive: fixes P :: pi and a :: subject and x :: name and Rel :: "(pi × pi) set" assumes "Id ⊆ Rel" shows "derivative P P a x Rel" using assms apply(cases a) by(auto simp add: derivative_def) (* lemma simActFreeCases[consumes 0, case_names Der]: fixes P :: pi and α :: freeRes and Q' :: pi and Rel :: "(pi × pi) set" assumes "∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel" shows "simAct P (α ≺ Q') P Rel" using assms by(simp add: simAct_def residualInject) *) (*****************Reflexivity and transitivity*********************) lemma reflexive: fixes P :: pi and Rel :: "(pi × pi) set" assumes "Id ⊆ Rel" shows "P ↝[Rel] P" using assms by(auto simp add: simulation_def derivativeReflexive) lemma transitive: fixes P :: pi and Q :: pi and R :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" and Rel'' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and QSimR: "Q ↝[Rel'] R" and Eqvt': "eqvt Rel''" and Trans: "Rel O Rel' ⊆ Rel''" shows "P ↝[Rel''] R" using Eqvt' proof(induct rule: simCasesCont[where C=Q]) case(Bound a x R') have RTrans: "R ⟼ a«x» ≺ R'" by fact from ‹x ♯ Q› QSimR RTrans obtain Q' where QTrans: "Q ⟼ a«x» ≺ Q'" and QDer: "derivative Q' R' a x Rel'" by(blast dest: simE) with QTrans ‹x ♯ P› PSimQ obtain P' where PTrans: "P ⟼ a«x» ≺ P'" and PDer: "derivative P' Q' a x Rel" by(blast dest: simE) moreover from PDer QDer Trans have "derivative P' R' a x Rel''" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast next case(Free α R') have RTrans: "R ⟼ α ≺ R'" by fact with QSimR obtain Q' where QTrans: "Q ⟼ α ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'" by(blast dest: simE) from QTrans PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast with PTrans show ?case by blast qed end