(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Early_Sim_Pres imports Weak_Early_Sim begin lemma tauPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "τ.(P) ↝<Rel> τ.(Q)" proof(induct rule: simCases) case(Bound Q' a x) have "τ.(Q) ⟼a<νx> ≺ Q'" by fact hence False by(induct rule: tauCases', auto) thus ?case by simp next case(Free Q' α) have "τ.(Q) ⟼(α ≺ Q')" by fact thus ?case proof(induct rule: tauCases', auto simp only: pi.inject residual.inject) have "τ.(P) ⟹⇧^{^}τ ≺ P" by(rule Tau) with PRelQ show "∃P'. τ.(P) ⟹⇧^{^}τ ≺ P' ∧ (P', Q) ∈ Rel" by blast qed qed lemma inputPres: fixes P :: pi and x :: name and Q :: pi and a :: name and Rel :: "(pi × pi) set" assumes PRelQ: "∀y. (P[x::=y], Q[x::=y]) ∈ Rel" and Eqvt: "eqvt Rel" shows "a<x>.P ↝<Rel> a<x>.Q" using Eqvt proof(induct rule: simCasesCont[where C="(x, a, P, Q)"]) case(Bound b y Q') from ‹y ♯ (x, a, P, Q)› have "y ≠ x" "y ≠ a" "y ♯ P" "y ♯ Q" by simp+ from ‹a<x>.Q ⟼b<νy> ≺ Q'› ‹y ≠ a› ‹y ≠ x› ‹y ♯ Q› show ?case by(erule_tac inputCases') auto next case(Free α Q') from ‹a<x>.Q ⟼ α ≺ Q'› show ?case proof(induct rule: inputCases) case(cInput u) have "a<x>.P ⟹⇧^{^}(a<u>) ≺ P[x::=u]" by(rule Input) moreover from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by auto ultimately show ?case by blast qed qed lemma outputPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "a{b}.P ↝<Rel> a{b}.Q" proof(induct rule: simCases) case(Bound Q' c x) have "a{b}.Q ⟼c<νx> ≺ Q'" by fact hence False by(induct rule: outputCases', auto) thus ?case by simp next case(Free Q' α) have "a{b}.Q ⟼α ≺ Q'" by fact thus "∃P'. a{b}.P ⟹⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel" proof(induct rule: outputCases', auto simp add: pi.inject residual.inject) have "a{b}.P ⟹⇧^{^}a[b] ≺ P" by(rule Output) with PRelQ show "∃P'. a{b}.P ⟹⇧^{^}a[b] ≺ P' ∧ (P', Q) ∈ Rel" by blast qed qed lemma matchPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel> Q" and RelRel': "Rel ⊆ Rel'" and RelStay: "⋀R S c. (R, S) ∈ Rel ⟹ ([c⌢c]R, S) ∈ Rel" shows "[a⌢b]P ↝<Rel'> [a⌢b]Q" proof(induct rule: simCases) case(Bound Q' c x) have "x ♯ [a⌢b]P" by fact hence xFreshP: "(x::name) ♯ P" by simp have "[a⌢b]Q ⟼c<νx> ≺ Q'" by fact thus ?case proof(induct rule: matchCases) case Match have "Q ⟼c<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟹c<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Match) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Free Q' α) have "[a⌢b]Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: matchCases) case Match have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where "P ⟹⇧^{^}α ≺ P'" and "(P', Q') ∈ Rel" by(blast dest: simE) thus ?case proof(induct rule: transitionCases) case Step have "P ⟹α ≺ P'" by fact hence "[a⌢a]P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Match) with RelRel' ‹(P', Q') ∈ Rel› show ?case by(force simp add: weakFreeTransition_def) next case Stay have "[a⌢a]P ⟹⇧^{^}τ ≺ [a⌢a]P" by(simp add: weakFreeTransition_def) moreover from ‹(P, Q') ∈ Rel› have "([a⌢a]P, Q') ∈ Rel" by(blast intro: RelStay) ultimately show ?case using RelRel' by blast qed qed qed lemma mismatchPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel> Q" and RelRel': "Rel ⊆ Rel'" and RelStay: "⋀R S c d. ⟦(R, S) ∈ Rel; c ≠ d⟧ ⟹ ([c≠d]R, S) ∈ Rel" shows "[a≠b]P ↝<Rel'> [a≠b]Q" proof(induct rule: simCases) case(Bound Q' c x) have "x ♯ [a≠b]P" by fact hence xFreshP: "(x::name) ♯ P" by simp have "[a≠b]Q ⟼c<νx> ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case Mismatch have aineqb: "a ≠ b" by fact have "Q ⟼c<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟹c<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans aineqb have "[a≠b]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Mismatch) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Free Q' α) have "[a≠b]Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case Mismatch have aineqb: "a ≠ b" by fact have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where "P ⟹⇧^{^}α ≺ P'" and "(P', Q') ∈ Rel" by(blast dest: simE) thus ?case proof(induct rule: transitionCases) case Step have "P ⟹α ≺ P'" by fact hence "[a≠b]P ⟹α ≺ P'" using aineqb by(rule Weak_Early_Step_Semantics.Mismatch) with RelRel' ‹(P', Q') ∈ Rel› show ?case by(force simp add: weakFreeTransition_def) next case Stay have "[a≠b]P ⟹⇧^{^}τ ≺ [a≠b]P" by(simp add: weakFreeTransition_def) moreover from ‹(P, Q') ∈ Rel› aineqb have "([a≠b]P, Q') ∈ Rel" by(blast intro: RelStay) ultimately show ?case using RelRel' by blast qed qed qed lemma parCompose: fixes P :: pi and Q :: pi and R :: pi and S :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" and Rel'' :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel> Q" and RSimT: "R ↝<Rel'> S" and PRelQ: "(P, Q) ∈ Rel" and RRel'T: "(R, S) ∈ Rel'" and Par: "⋀P' Q' R' S'. ⟦(P', Q') ∈ Rel; (R', S') ∈ Rel'⟧ ⟹ (P' ∥ R', Q' ∥ S') ∈ Rel''" and Res: "⋀T U x. (T, U) ∈ Rel'' ⟹ (<νx>T, <νx>U) ∈ Rel''" shows "P ∥ R ↝<Rel''> Q ∥ S" proof - show ?thesis proof(induct rule: simCases) case(Bound Q' a x) have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ∥ S ⟼a<νx> ≺ Q'" by fact thus ?case proof(induct rule: parCasesB) case(cPar1 Q') have QTrans: "Q ⟼ a<νx> ≺ Q'" and xFreshT: "x ♯ S" by fact+ from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟹a<νx> ≺ (P' ∥ R)" by(rule Weak_Early_Step_Semantics.Par1B) moreover from P'RelQ' RRel'T have "(P' ∥ R, Q' ∥ S) ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cPar2 S') have STrans: "S ⟼ a<νx> ≺ S'" and xFreshQ: "x ♯ Q" by fact+ from xFreshR RSimT STrans obtain R' where RTrans:"R ⟹a<νx> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: simE) from RTrans xFreshP xFreshR have ParTrans: "P ∥ R ⟹a<νx> ≺ (P ∥ R')" by(blast intro: Weak_Early_Step_Semantics.Par2B) moreover from PRelQ R'Rel'T' have "(P ∥ R', Q ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast qed next case(Free QT' α) have "Q ∥ S ⟼ α ≺ QT'" by fact thus ?case proof(induct rule: parCasesF[of _ _ _ _ _ "(P, R)"]) case(cPar1 Q') have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟹⇧^{^}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have Trans: "P ∥ R ⟹⇧^{^}α ≺ P' ∥ R" by(rule Weak_Early_Semantics.Par1F) moreover from PRel RRel'T have "(P' ∥ R, Q' ∥ S) ∈ Rel''" by(blast intro: Par) ultimately show ?case by blast next case(cPar2 S') have "S ⟼ α ≺ S'" by fact with RSimT obtain R' where RTrans: "R ⟹⇧^{^}α ≺ R'" and RRel: "(R', S') ∈ Rel'" by(blast dest: simE) from RTrans have Trans: "P ∥ R ⟹⇧^{^}α ≺ P ∥ R'" by(rule Weak_Early_Semantics.Par2F) moreover from PRelQ RRel have "(P ∥ R', Q ∥ S') ∈ Rel''" by(blast intro: Par) ultimately show ?case by blast next case(cComm1 Q' S' a b) have QTrans: "Q ⟼ a<b> ≺ Q'" and STrans: "S ⟼ a[b] ≺ S'" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RSimT STrans obtain R' where RTrans: "R ⟹a[b] ≺ R'" and RRel: "(R', S') ∈ Rel'" by(fastforce dest: simE simp add: weakFreeTransition_def) from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1) hence "P ∥ R ⟹⇧^{^}τ ≺ P' ∥ R'" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from P'RelQ' RRel have "(P' ∥ R', Q' ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cComm2 Q' S' a b) have QTrans: "Q ⟼a[b] ≺ Q'" and STrans: "S ⟼a<b> ≺ S'" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹a[b] ≺ P'" and PRel: "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RSimT STrans obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(fastforce dest: simE simp add: weakFreeTransition_def) from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2) hence "P ∥ R ⟹⇧^{^}τ ≺ P' ∥ R'" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from PRel R'Rel'T' have "(P' ∥ R', Q' ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cClose1 Q' S' a x) have QTrans: "Q ⟼a<x> ≺ Q'" and STrans: "S ⟼a<νx> ≺ S'" by fact+ have "x ♯ (P, R)" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by(simp add: fresh_prod)+ from PSimQ QTrans obtain P' where PTrans: "P ⟹a<x> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RSimT STrans xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: simE) from PTrans RTrans xFreshP have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" by(rule Weak_Early_Step_Semantics.Close1) hence "P ∥ R ⟹⇧^{^}τ ≺ <νx>(P' ∥ R')" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from P'RelQ' R'Rel'T' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ S')) ∈ Rel''" by(blast intro: Par Res) ultimately show ?case by blast next case(cClose2 Q' S' a x) have QTrans: "Q ⟼a<νx> ≺ Q'" and STrans: "S ⟼a<x> ≺ S'" by fact+ have "x ♯ (P, R)" by fact hence xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by(simp add: fresh_prod)+ from PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from RSimT STrans obtain R' where RTrans: "R ⟹a<x> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(fastforce dest: simE simp add: weakFreeTransition_def) from PTrans RTrans xFreshR have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" by(rule Weak_Early_Step_Semantics.Close2) hence "P ∥ R ⟹⇧^{^}τ ≺ <νx>(P' ∥ R')" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from P'RelQ' R'Rel'T' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ S')) ∈ Rel''" by(blast intro: Par Res) ultimately show ?case by blast qed qed qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi and a :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel> Q" and PRelQ: "(P, Q) ∈ Rel" and Par: "⋀S T U. (S, T) ∈ Rel ⟹ (S ∥ U, T ∥ U) ∈ Rel'" and Res: "⋀S T x. (S, T) ∈ Rel' ⟹ (<νx>S, <νx>T) ∈ Rel'" shows "P ∥ R ↝<Rel'> Q ∥ R" proof - note PSimQ moreover have RSimR: "R ↝<Id> R" by(auto intro: reflexive) moreover note PRelQ moreover have "(R, R) ∈ Id" by auto moreover from Par have "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Id⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel'" by auto ultimately show ?thesis using Res by(rule parCompose) qed lemma resPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and x :: name and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel> Q" and ResRel: "⋀R S y. (R, S) ∈ Rel ⟹ (<νy>R, <νy>S) ∈ Rel'" and RelRel': "Rel ⊆ Rel'" and EqvtRel: "eqvt Rel" and EqvtRel': "eqvt Rel'" shows "<νx>P ↝<Rel'> <νx>Q" proof - from EqvtRel' show ?thesis proof(induct rule: simCasesCont[where C="(P, x)"]) case(Bound a y Q') have Trans: "<νx>Q ⟼a<νy> ≺ Q'" by fact have "y ♯ (P, x)" by fact hence yineqx: "y ≠ x" and yFreshP: "y ♯ P" by(simp add: fresh_prod)+ from Trans yineqx show ?case proof(induct rule: resCasesB) case(Open Q') have QTrans: "Q ⟼a[x] ≺ Q'" and aineqx: "a ≠ x" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹⇧^{^}a[x] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans aineqx have "<νx>P ⟹a<νx> ≺ P'" by(force intro: Weak_Early_Step_Semantics.Open simp add: weakFreeTransition_def) with ‹y ♯ P› ‹y ≠ x› have "<νx>P ⟹a<νy> ≺ ([(y, x)] ∙ P')" by(force intro: weakTransitionAlpha simp add: abs_fresh name_swap) moreover from EqvtRel P'RelQ' RelRel' have "([(y, x)] ∙ P', [(y, x)] ∙ Q') ∈ Rel'" by(blast intro: eqvtRelI) ultimately show ?case by blast next case(Res Q') have QTrans: "Q ⟼a<νy> ≺ Q'" and xineqa: "x ≠ a" by fact+ from PSimQ yFreshP QTrans obtain P' where PTrans: "P ⟹a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans xineqa yineqx yFreshP have ResTrans: "<νx>P ⟹a<νy> ≺ (<νx>P')" by(blast intro: Weak_Early_Step_Semantics.ResB) moreover from P'RelQ' have "((<νx>P'), (<νx>Q')) ∈ Rel'" by(rule ResRel) ultimately show ?case by blast qed next case(Free α Q') have QTrans: "<νx>Q ⟼ α ≺ Q'" by fact have "∃c::name. c ♯ (P, Q, Q', α)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshQ: "c ♯ Q" and cFreshAlpha: "c ♯ α" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P" by(force simp add: fresh_prod) from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(simp add: alphaRes) moreover have "∃P'.<νc>([(x, c)] ∙ P) ⟹⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel'" proof - from QTrans cFreshQ have "<νc>([(x, c)] ∙ Q) ⟼α ≺ Q'" by(simp add: alphaRes) moreover have "c ♯ α" by(rule cFreshAlpha) moreover from PSimQ EqvtRel have "([(x, c)] ∙ P) ↝<Rel> ([(x, c)] ∙ Q)" by(blast intro: eqvtI) ultimately show ?thesis apply(induct rule: resCasesF, auto simp add: residual.inject pi.inject name_abs_eq) by(blast intro: ResF ResRel dest: simE) qed ultimately show ?case by force qed qed lemma resChainI: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and lst :: "name list" assumes eqvtRel: "eqvt Rel" and Res: "⋀R S y. (R, S) ∈ Rel ⟹ (<νy>R, <νy>S) ∈ Rel" and PRelQ: "P ↝<Rel> Q" shows "(resChain lst) P ↝<Rel> (resChain lst) Q" proof - show ?thesis proof(induct lst) (* Base case *) from PRelQ show "resChain [] P ↝<Rel> resChain [] Q" by simp next (* Inductive step *) fix a lst assume IH: "(resChain lst P) ↝<Rel> (resChain lst Q)" moreover from Res have "⋀P Q a. (P, Q) ∈ Rel ⟹ (<νa>P, <νa>Q) ∈ Rel" by simp moreover have "Rel ⊆ Rel" by simp ultimately have "<νa>(resChain lst P) ↝<Rel> <νa>(resChain lst Q)" using eqvtRel by(rule_tac resPres) thus "resChain (a # lst) P ↝<Rel> resChain (a # lst) Q" by simp qed qed lemma bangPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝<Rel> S" and ParComp: "⋀R S T U. ⟦(R, S) ∈ Rel; (T, U) ∈ Rel'⟧ ⟹ (R ∥ T, S ∥ U) ∈ Rel'" and Res: "⋀R S x. (R, S) ∈ Rel' ⟹ (<νx>R, <νx>S) ∈ Rel'" and RelStay: "⋀R S. (R ∥ !R, S) ∈ Rel' ⟹ (!R, S) ∈ Rel'" and BangRelRel': "(bangRel Rel) ⊆ Rel'" and eqvtRel': "eqvt Rel'" shows "!P ↝<Rel'> !Q" proof - let ?Sim = "λP Rs. (∀a x Q'. Rs = a<νx> ≺ Q' ⟶ x ♯ P ⟶ (∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel')) ∧ (∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟹⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel'))" { fix Rs P assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel" hence "?Sim P Rs" using PRelQ proof(nominal_induct avoiding: P rule: bangInduct) case(Par1B a x Q') have QTrans: "Q ⟼a<νx> ≺ Q'" and xFreshQ: "x ♯ Q" by fact+ have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelT: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ from PRelQ have PSimQ: "P ↝<Rel> Q" by(rule Sim) from ‹x ♯ P› ‹x ♯ Q› show ?case proof(auto simp add: residual.inject alpha' name_fresh_fresh) from PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟹a<νx>≺ (P' ∥ R)" by(rule Weak_Early_Step_Semantics.Par1B) moreover from P'RelQ' RBangRelT BangRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ Rel'" by(blast intro: Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q' ∥ !Q) ∈ Rel'" by blast next fix y assume "(y::name) ♯ Q'" and "y ♯ P" and "y ♯ R" from QTrans ‹y ♯ Q'› have "Q ⟼a<νy> ≺ ([(x, y)] ∙ Q')" by(simp add: alphaBoundOutput) with PSimQ ‹y ♯ P› obtain P' where PTrans: "P ⟹a<νy> ≺ P'" and P'RelQ': "(P', [(x, y)] ∙ Q') ∈ Rel" by(blast dest: simE) from PTrans ‹y ♯ R› have "P ∥ R ⟹a<νy>≺ (P' ∥ R)" by(rule Weak_Early_Step_Semantics.Par1B) moreover from P'RelQ' RBangRelT BangRelRel' have "(P' ∥ R, ([(y, x)] ∙ Q') ∥ !Q) ∈ Rel'" by(fastforce intro: Rel.BRPar simp add: name_swap) ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q') ∥ !Q) ∈ Rel'" by blast qed qed next case(Par1F α Q' P) have QTrans: "Q ⟼α ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝<Rel> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹⇧^{^}α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "P ∥ R ⟹⇧^{^}α ≺ P' ∥ R" by(rule Weak_Early_Semantics.Par1F) moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹⇧^{^}α ≺ P' ∧ (P', Q' ∥ !Q) ∈ Rel'" using BangRelRel' by blast qed qed next case(Par2B a x Q' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<νx> ≺ Q')" by simp have xFreshQ: "x ♯ Q" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ show ?case using ‹x ♯ Q› proof(auto simp add: residual.inject alpha' name_fresh_fresh) from IH RBangRelQ have "?Sim R (a<νx> ≺ Q')" by blast with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'BangRelQ': "(R', Q') ∈ Rel'" by(blast dest: simE) from RTrans xFreshP have "P ∥ R ⟹a<νx> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B) moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule ParComp) ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q ∥ Q') ∈ Rel'" by blast next fix y assume "(y::name) ♯ Q'" and "y ♯ R" and "y ♯ P" from IH RBangRelQ have "?Sim R (a<νx> ≺ Q')" by blast with ‹y ♯ Q'› have "?Sim R (a<νy> ≺ ([(x, y)] ∙ Q'))" by(simp add: alphaBoundOutput) with ‹y ♯ R›obtain R' where RTrans: "R ⟹a<νy> ≺ R'" and R'BangRelQ': "(R', [(x, y)] ∙ Q') ∈ Rel'" by(blast dest: simE) from RTrans ‹y ♯ P› have "P ∥ R ⟹a<νy> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B) moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ ([(y, x)] ∙ Q')) ∈ Rel'" by(fastforce intro: ParComp simp add: name_swap) ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', Q ∥ ([(y, x)] ∙ Q')) ∈ Rel'" by blast qed qed next case(Par2F α Q' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (α ≺ Q')" by simp have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from RBangRelQ have "?Sim R (α ≺ Q')" by(rule IH) then obtain R' where RTrans: "R ⟹⇧^{^}α ≺ R'" and R'RelQ': "(R', Q') ∈ Rel'" by(blast dest: simE) from RTrans have "P ∥ R ⟹⇧^{^}α ≺ P ∥ R'" by(rule Weak_Early_Semantics.Par2F) moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule ParComp) ultimately show "∃P'. P ∥ R ⟹⇧^{^}α ≺ P' ∧ (P', Q ∥ Q') ∈ Rel'" by blast qed qed next case(Comm1 a Q' b Q'' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a[b] ≺ Q'')" by simp have QTrans: "Q ⟼ a<b> ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝<Rel> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RBangRelQ have "?Sim R (a[b] ≺ Q'')" by(rule IH) then obtain R' where RTrans: "R ⟹a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ Rel'" by(fastforce dest: simE simp add: weakFreeTransition_def) from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')" by(rule Weak_Early_Step_Semantics.Comm1) hence "P ∥ R ⟹⇩_{τ}P' ∥ R'" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ Rel'" by(rule ParComp) ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧^{*}∧ (P', Q' ∥ Q'') ∈ Rel'" by auto qed qed next case(Comm2 a b Q' Q'' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<b> ≺ Q'')" by simp have QTrans: "Q ⟼a[b] ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝<Rel> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RBangRelQ have "?Sim R (a<b> ≺ Q'')" by(rule IH) then obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'BangRelQ'': "(R', Q'') ∈ Rel'" by(fastforce dest: simE simp add: weakFreeTransition_def) from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')" by(rule Weak_Early_Step_Semantics.Comm2) hence "P ∥ R ⟹⇩_{τ}P' ∥ R'" by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain) moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ Rel'" by(rule ParComp) ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧^{*}∧ (P', Q' ∥ Q'') ∈ Rel'" by auto qed qed next case(Close1 a x Q' Q'' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<νx> ≺ Q'')" by simp have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝<Rel> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹a<x> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: weakFreeTransition_def) from RBangRelQ have "?Sim R (a<νx> ≺ Q'') " by(rule IH) with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'RelQ'': "(R', Q'') ∈ Rel'" by(blast dest: simE) from PTrans RTrans xFreshP have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" by(rule Weak_Early_Step_Semantics.Close1) moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ Rel'" by(force intro: ParComp Res) ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧^{*}∧ (P', <νx>(Q' ∥ Q'')) ∈ Rel'" by auto qed qed next case(Close2 a x Q' Q'' P) hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<x> ≺ Q'')" by simp have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝<Rel> Q" by(rule Sim) with QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from RBangRelQ have "?Sim R (a<x> ≺ Q'')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟹a<x> ≺ R'" and R'RelQ'': "(R', Q'') ∈ Rel'" by(fastforce simp add: weakFreeTransition_def) from PTrans RTrans xFreshR have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" by(rule Weak_Early_Step_Semantics.Close2) moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ Rel'" by(force intro: ParComp Res) ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧^{*}∧ (P', <νx>(Q' ∥ Q'')) ∈ Rel'" by auto qed qed next case(Bang Rs) hence IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ ?Sim P Rs" by simp have "(P, !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRBangCases) case(BRBang P) have PRelQ: "(P, Q) ∈ Rel" by fact hence "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) with PRelQ have "(P ∥ !P, Q ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) hence IH: "?Sim (P ∥ !P) Rs" by(rule IH) show ?case proof(intro conjI allI impI) fix Q' a x assume "Rs = a<νx> ≺ Q'" and "x ♯ !P" then obtain P' where PTrans: "(P ∥ !P) ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" using IH by(auto simp add: residual.inject) from PTrans have "!P ⟹a<νx> ≺ P'" by(force intro: Weak_Early_Step_Semantics.Bang simp add: weakFreeTransition_def) with P'RelQ' show "∃P'. !P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel'" by blast next fix Q' α assume "Rs = α ≺ Q'" then obtain P' where PTrans: "(P ∥ !P) ⟹⇧^{^}α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" using IH by auto from PTrans show "∃P'. !P ⟹⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel'" using P'RelQ' proof(induct rule: transitionCases) case Step have "P ∥ !P ⟹α ≺ P'" by fact hence "!P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Bang) with P'RelQ' show ?case by(force simp add: weakFreeTransition_def) next case Stay have "!P ⟹⇧^{^}τ ≺ !P" by(simp add: weakFreeTransition_def) moreover assume "(P ∥ !P, Q') ∈ Rel'" hence "(!P, Q') ∈ Rel'" by(blast intro: RelStay) ultimately show ?case by blast qed qed qed qed } moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) ultimately show ?thesis by(auto simp add: weakSimulation_def) qed lemma bangRelSim: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and Rel'l :: "(pi × pi) set" assumes PBangRelQ: "(P, Q) ∈ bangRel Rel" and Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝<Rel> S" and ParComp: "⋀R S T U. ⟦(R, S) ∈ Rel; (T, U) ∈ Rel'⟧ ⟹ (R ∥ T, S ∥ U) ∈ Rel'" and Res: "⋀R S x. (R, S) ∈ Rel' ⟹ (<νx>R, <νx>S) ∈ Rel'" and RelStay: "⋀R S. (R ∥ !R, S) ∈ Rel' ⟹ (!R, S) ∈ Rel'" and BangRelRel': "(bangRel Rel) ⊆ Rel'" and eqvtRel': "eqvt Rel'" and Eqvt: "eqvt Rel" shows "P ↝<Rel'> Q" proof - from PBangRelQ show ?thesis proof(induct rule: bangRel.induct) case(BRBang P Q) have PRelQ: "(P, Q) ∈ Rel" by fact thus ?case using ParComp Res BangRelRel' eqvtRel' Eqvt RelStay Sim by(rule_tac bangPres) next case(BRPar P Q R T) have "(P, Q) ∈ Rel" by fact moreover hence "P ↝<Rel> Q" by(rule Sim) moreover have "R ↝<Rel'> T" by fact moreover have "(R, T) ∈ bangRel Rel" by fact ultimately show ?case using ParComp eqvtRel' Res Eqvt BangRelRel' by(blast intro: parCompose) next case(BRRes P Q x) have "P ↝<Rel'> Q" by fact thus ?case using BangRelRel' eqvtRel' Res by(blast intro: resPres) qed qed end