(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Early_Step_Sim_Pres imports Weak_Early_Step_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 a x Q') 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 add: pi.inject residual.inject) have "τ.(P) ⟹ τ ≺ P" by(rule Weak_Early_Step_Semantics.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 Weak_Early_Step_Semantics.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" and Rel' :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "a{b}.P ↝«Rel» a{b}.Q" proof(induct rule: simCases) case(Bound c x Q') 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 Weak_Early_Step_Semantics.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'" shows "[a⌢b]P ↝«Rel'» [a⌢b]Q" proof(induct rule: simCases) case(Bound c x Q') 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 PTrans: "P ⟹α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Match) with RelRel' PRel show ?case by blast 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'" shows "[a≠b]P ↝«Rel'» [a≠b]Q" proof(induct rule: simCases) case(Bound c x Q') 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 "Q ⟼α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟹α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans ‹a ≠ b› have "[a≠b]P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Mismatch) with RelRel' PRel show ?case by blast qed qed lemma sumPres: fixes P :: pi and Q :: pi and R :: pi assumes PSimQ: "P ↝«Rel» Q" and RelRel': "Rel ⊆ Rel'" and C: "Id ⊆ Rel'" shows "P ⊕ R ↝«Rel'» Q ⊕ R" proof(induct rule: simCases) case(Bound a x Q') have "x ♯ P ⊕ R" by fact hence xFreshP: "(x::name) ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⊕ R ⟼a<νx> ≺ Q'" by fact thus ?case proof(induct rule: sumCases) case Sum1 have "Q ⟼a<νx> ≺ Q'" by fact with xFreshP PSimQ obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "P ⊕ R ⟹a<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Sum1) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast next case Sum2 from ‹R ⟼a<νx> ≺ Q'› have "P ⊕ R ⟼a<νx> ≺ Q'" by(rule Early_Semantics.Sum2) hence "P ⊕ R ⟹a<νx> ≺ Q'" by(rule Weak_Early_Step_Semantics.singleActionChain) moreover from C have "(Q', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Free α Q') have "Q ⊕ R ⟼α ≺ Q'" by fact thus ?case proof(induct rule: sumCases) case Sum1 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 "P ⊕ R ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Sum1) with RelRel' PRel show ?case by blast next case Sum2 from ‹R ⟼α ≺ Q'› have "P ⊕ R ⟼α ≺ Q'" by(rule Early_Semantics.Sum2) hence "P ⊕ R ⟹α ≺ Q'" by(rule Weak_Early_Step_Semantics.singleActionChain) moreover from C have "(Q', Q') ∈ Rel'" by blast ultimately show ?case by blast qed qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi and T :: pi and Rel :: "(pi × pi) set" 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 - show ?thesis proof(induct rule: simCases) case(Bound a x Q') have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ∥ R ⟼a<νx> ≺ Q'" by fact thus ?case proof(induct rule: parCasesB) case(cPar1 Q') have QTrans: "Q ⟼ a<νx> ≺ Q'" 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' have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cPar2 R') from ‹R ⟼ a<νx> ≺ R'› ‹x ♯ P› have "P ∥ R ⟼a<νx> ≺ (P ∥ R')" by(rule Early_Semantics.Par2B) hence "P ∥ R ⟹ a<νx> ≺ (P ∥ R')" by(rule Weak_Early_Step_Semantics.singleActionChain) moreover from PRelQ have "(P ∥ R', Q ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast qed next case(Free α QR') have "Q ∥ R ⟼ α ≺ QR'" 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_Step_Semantics.Par1F) moreover from PRel have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(blast intro: Par) ultimately show ?case by blast next case(cPar2 R') from ‹R ⟼α ≺ R'› have "P ∥ R ⟼α ≺ (P ∥ R')" by(rule Early_Semantics.Par2F) hence "P ∥ R ⟹α ≺ (P ∥ R')" by(rule Weak_Early_Step_Semantics.singleActionChain) moreover from PRelQ have "(P ∥ R', Q ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cComm1 Q' R' a b) have QTrans: "Q ⟼ a<b> ≺ Q'" and RTrans: "R ⟼ a[b] ≺ R'" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹a[b] ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain) with PTrans have "P ∥ R ⟹ τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1) moreover from P'RelQ' have "(P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cComm2 Q' R' a b) have QTrans: "Q ⟼a[b] ≺ Q'" and RTrans: "R ⟼a<b> ≺ R'" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹a<b> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain) with PTrans have "P ∥ R ⟹ τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2) moreover from P'RelQ' have "(P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cClose1 Q' R' a x) have QTrans: "Q ⟼a<x> ≺ Q'" and RTrans: "R ⟼a<νx> ≺ R'" 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(blast dest: simE) from RTrans have "R ⟹a<νx> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain) with PTrans have Trans: "P ∥ R ⟹ τ ≺ <νx>(P' ∥ R')" using ‹x ♯ P› by(rule Weak_Early_Step_Semantics.Close1) moreover from P'RelQ' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ R')) ∈ Rel'" by(blast intro: Par Res) ultimately show ?case by blast next case(cClose2 Q' R' a x) have QTrans: "Q ⟼a<νx> ≺ Q'" and RTrans: "R ⟼a<x> ≺ R'" 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 RTrans have "R ⟹a<x> ≺ R'" by(rule Weak_Early_Step_Semantics.singleActionChain) with PTrans have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')" using ‹x ♯ R› by(rule Weak_Early_Step_Semantics.Close2) moreover from P'RelQ' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ R')) ∈ Rel'" by(blast intro: Par Res) ultimately show ?case by blast qed qed 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 C1: "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>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[of _ "(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(rule Weak_Early_Step_Semantics.Open) hence "<νx>P ⟹a<νy> ≺ ([(y, x)] ∙ P')" using ‹y ♯ P› ‹y ≠ x› by(force simp add: weakTransitionAlpha 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 C1) 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: Weak_Early_Step_Semantics.ResF C1 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 x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>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 C1: "Rel ⊆ Rel'" and eqvtRel: "eqvt Rel'" shows "!P ↝«bangRel Rel'» !Q" proof - let ?Sim = "λP Rs. (∀a x Q'. Rs = a<νx> ≺ Q' ⟶ x ♯ P ⟶ (∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ bangRel Rel')) ∧ (∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ bangRel Rel'))" from eqvtRel have EqvtBangRel: "eqvt(bangRel Rel')" by(rule eqvtBangRel) from C1 have BRelRel': "⋀P Q. (P, Q) ∈ bangRel Rel ⟹ (P, Q) ∈ bangRel Rel'" by(auto intro: bangRelSubset) { fix Pa Rs assume "!Q ⟼ Rs" and "(Pa, !Q) ∈ bangRel Rel" hence "?Sim Pa Rs" using PRelQ proof(nominal_induct avoiding: Pa P rule: bangInduct) case(Par1B a x Q' Pa P) have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+ thus "?Sim Pa (a<νx> ≺ (Q' ∥ !Q))" proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" by fact have PBRQ: "(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 alpha') 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 PTrans xFreshR have "P ∥ R ⟹a<νx> ≺ (P' ∥ R)" by(force intro: Weak_Early_Step_Semantics.Par1B) moreover from P'RelQ' PBRQ BRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q' ∥ !Q) ∈ bangRel Rel'" by blast next fix y assume "(y::name) ♯ Q'" and "y ♯ P" and "y ♯ R" and "y ♯ Q" from QTrans ‹y ♯ Q'› have "Q ⟼a<νy> ≺ ([(x, y)] ∙ Q')" by(simp add: alphaBoundOutput) moreover from PRelQ have "P ↝«Rel'» Q" by(rule Sim) ultimately obtain P' where PTrans: "P ⟹a<νy> ≺ P'" and P'RelQ': "(P', [(x, y)] ∙ Q') ∈ Rel'" using ‹y ♯ P› by(blast dest: simE) from PTrans ‹y ♯ R› have "P ∥ R ⟹a<νy> ≺ (P' ∥ R)" by(force intro: Weak_Early_Step_Semantics.Par1B) moreover from P'RelQ' PBRQ BRelRel' have "(P' ∥ R, ([(x, y)] ∙ Q') ∥ !Q) ∈ bangRel Rel'" by(metis Rel.BRPar) with ‹x ♯ Q› ‹y ♯ Q› have "(P' ∥ R, ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel'" by(simp add: name_fresh_fresh name_swap) ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel'" by blast qed qed next case(Par1F α Q' Pa P) have QTrans: "Q ⟼α ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and BR: "(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 RRel: "(P', Q') ∈ Rel'" by(blast dest: simE) from PTrans have "P ∥ R ⟹α ≺ P' ∥ R" by(rule Weak_Early_Step_Semantics.Par1F) moreover from RRel BR BRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(metis Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹α ≺ P' ∧ (P', Q' ∥ !Q) ∈ bangRel Rel'" by blast qed qed next case(Par2B a x Q' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<νx> ≺ Q')" by simp have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+ thus "?Sim Pa (a<νx> ≺ (Q ∥ Q'))" proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ from EqvtBangRel show "?Sim (P ∥ R) (a<νx> ≺ (Q ∥ Q'))" proof(auto simp add: residual.inject alpha') from RBRQ have "?Sim R (a<νx> ≺ Q')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'BRQ': "(R', Q') ∈ (bangRel Rel')" by(metis simE) from RTrans xFreshP have "P ∥ R ⟹a<νx> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B) moreover from PRelQ R'BRQ' C1 have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel')" by(blast dest: Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q ∥ Q') ∈ bangRel Rel'" by blast next fix y assume "(y::name) ♯ Q" and "y ♯ Q'" and "y ♯ P" and "y ♯ R" from RBRQ have "?Sim R (a<νx> ≺ Q')" by(rule IH) 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'BRQ': "(R', ([(x, y)] ∙ Q')) ∈ (bangRel Rel')" by(metis simE) from RTrans ‹y ♯ P› have "P ∥ R ⟹a<νy> ≺ (P ∥ R')" by(auto intro: Weak_Early_Step_Semantics.Par2B) moreover from PRelQ R'BRQ' C1 have "(P ∥ R', Q ∥ ([(x, y)] ∙ Q')) ∈ (bangRel Rel')" by(blast dest: Rel.BRPar) with ‹y ♯ Q› ‹x ♯ Q› have "(P ∥ R', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ (bangRel Rel')" by(simp add: name_swap name_fresh_fresh) ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ bangRel Rel'" by blast qed qed next case(Par2F α Q' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (α ≺ Q')" by simp have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from RBRQ IH have "∃R'. R ⟹α ≺ R' ∧ (R', Q') ∈ bangRel Rel'" by(metis simE) then obtain R' where RTrans: "R ⟹α ≺ R'" and R'RelQ': "(R', Q') ∈ bangRel Rel'" by blast from RTrans have "P ∥ R ⟹α ≺ P ∥ R'" by(rule Weak_Early_Step_Semantics.Par2F) moreover from PRelQ R'RelQ' C1 have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel'" by(blast dest: Rel.BRPar) ultimately show " ∃P'. P ∥ R ⟹α ≺ P' ∧ (P', Q ∥ Q') ∈ bangRel Rel'" by blast qed qed next case(Comm1 a Q' b Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a[b] ≺ Q'')" by simp have QTrans: "Q ⟼a<b> ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(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(blast dest: simE) from IH RBRQ have RTrans: "∃R'. R ⟹a[b] ≺ R' ∧ (R', Q'') ∈ bangRel Rel'" by(metis simE) then obtain R' where RTrans: "R ⟹a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'" by blast from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ bangRel Rel'" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', Q' ∥ Q'') ∈ bangRel Rel'" by blast qed qed next case(Comm2 a b Q' Q'') hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<b> ≺ Q'')" by simp have QTrans: "Q ⟼ a[b] ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(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(blast dest: simE) from IH RBRQ have RTrans: "∃R'. R ⟹a<b> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'" by(metis simE) then obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'" by blast from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ bangRel Rel'" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', Q' ∥ Q'') ∈ bangRel Rel'" by blast qed qed next case(Close1 a x Q' Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟶ ?Sim Pa (a<νx> ≺ Q'')" by simp have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have xFreshQ: "x ♯ Q" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact moreover have xFreshPa: "x ♯ Pa" by fact ultimately show ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(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 RBRQ xFreshR IH have "∃R'. R ⟹a<νx> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'" by(metis simE) then obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'" by blast 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'')) ∈ bangRel Rel'" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel'" by blast qed qed next case(Close2 a x Q' Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<x> ≺ Q'')" by simp have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have xFreshQ: "x ♯ Q" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(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 RBRQ IH have "∃R'. R ⟹a<x> ≺ R' ∧ (R', Q'') ∈ bangRel Rel'" by auto then obtain R' where RTrans: "R ⟹a<x> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel'" by blast 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'')) ∈ bangRel Rel'" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟹τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel'" by blast qed qed next case(Bang Rs Pa P) hence IH: "⋀Pa. (Pa, Q ∥ !Q) ∈ bangRel Rel ⟹ ?Sim Pa Rs" by simp have "(Pa, !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 BRPar) with IH have "?Sim (P ∥ !P) Rs" by simp thus ?case by(force intro: Weak_Early_Step_Semantics.Bang) qed qed } moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) ultimately show ?thesis by(auto simp add: weakStepSimulation_def) qed (* lemma bangPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝<Rel'> Q" and RelRel': "⋀P Q. (P, Q) ∈ Rel ⟹ (P, Q) ∈ Rel'" and eqvtRel': "eqvt Rel'" shows "!P ↝<bangRel Rel'> !Q" proof - from eqvtRel' have EqvtBangRel': "eqvt (bangRel Rel')" by(rule eqvtBangRel) from RelRel' have BRelRel': "⋀P Q. (P, Q) ∈ bangRel Rel ⟹ (P, Q) ∈ bangRel Rel'" by(auto intro: bangRelSubset) have "⋀Rs P. ⟦!Q ⟼ Rs; (P, !Q) ∈ bangRel Rel⟧ ⟹ weakSimStepAct P Rs P (bangRel Rel')" proof - fix Rs P assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel" thus "weakSimStepAct P Rs P (bangRel Rel')" 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 EqvtBangRel' show ?case proof(induct rule: simActBoundCases) case BoundOutput with 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 have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: Rel.BRPar BRelRel') ultimately show ?case 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(induct rule: simActFreeCases) case Der 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_Step_Semantics.Par1F) moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: Rel.BRPar BRelRel') ultimately show ?case by blast qed qed next case(Par2B a x Q' P) have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<νx> ≺ Q') P (bangRel Rel')" by fact 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+ from EqvtBangRel' show ?case proof(induct rule: simActBoundCases) case BoundOutput with IH RBangRelQ have "weakSimStepAct R (a<νx> ≺ Q') R (bangRel Rel')" by blast with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'BangRelQ': "(R', Q') ∈ bangRel Rel'" by(simp add: weakSimStepAct_def, blast) 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') ∈ (bangRel Rel')" by(blast intro: Rel.BRPar RelRel') ultimately show ?case by blast qed qed next case(Par2F α Q' P) have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (α ≺ Q') P (bangRel Rel')" 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(induct rule: simActFreeCases) case Der from RBangRelQ have "weakSimStepAct R (α ≺ Q') R (bangRel Rel')" by(rule IH) then obtain R' where RTrans: "R ⟹α ≺ R'" and R'RelQ': "(R', Q') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from RTrans have "P ∥ R ⟹α ≺ P ∥ R'" by(rule Weak_Early_Step_Semantics.Par2F) moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel')" by(blast intro: Rel.BRPar RelRel') ultimately show ?case by blast qed qed next case(Comm1 a Q' b Q'' P) have QTrans: "Q ⟼ a<b> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a[b] ≺ Q'') P (bangRel Rel')" 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(induct rule: simActFreeCases) case Der 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(blast dest: simE) from RBangRelQ have "weakSimStepAct R (a[b] ≺ Q'') R (bangRel Rel')" by(rule IH) then obtain R' where RTrans: "R ⟹a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')" by(rule Weak_Early_Step_Semantics.Comm1) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ (bangRel Rel')" by(rule Rel.BRPar) ultimately show ?case by blast qed qed next case(Comm2 a b Q' Q'' P) have QTrans: "Q ⟼a[b] ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<b> ≺ Q'') P (bangRel Rel')" 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(induct rule: simActFreeCases) case Der 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(blast dest: simE) from RBangRelQ have "weakSimStepAct R (a<b> ≺ Q'') R (bangRel Rel')" by(rule IH) then obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'BangRelQ'': "(R', Q'') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')" by(rule Weak_Early_Step_Semantics.Comm2) moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ (bangRel Rel')" by(rule Rel.BRPar) ultimately show ?case by blast qed qed next case(Close1 a x Q' Q'' P) have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<νx> ≺ Q'') P (bangRel Rel')" 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(induct rule: simActFreeCases) case Der 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(blast dest: simE) from RBangRelQ have "weakSimStepAct R (a<νx> ≺ Q'') R (bangRel Rel')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans RTrans xFreshP xFreshR 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'')) ∈ (bangRel Rel')" by(force intro: Rel.BRPar Rel.BRRes) ultimately show ?case by blast qed qed next case(Close2 a x Q' Q'' P) have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimStepAct P (a<x> ≺ Q'') P (bangRel Rel')" 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(induct rule: simActFreeCases) case Der 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 "weakSimStepAct R (a<x> ≺ Q'') R (bangRel Rel')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟹a<x> ≺ R'" and R'RelQ'': "(R', Q'') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans RTrans xFreshP 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'')) ∈ (bangRel Rel')" by(force intro: Rel.BRPar Rel.BRRes) ultimately show ?case by blast qed qed next case(Bang Rs) have IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ weakSimStepAct P Rs P (bangRel Rel')" by fact 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 "weakSimStepAct (P ∥ !P) Rs (P ∥ !P) (bangRel Rel')" by(rule IH) thus ?case proof(simp (no_asm) add: weakSimStepAct_def, auto) fix Q' a x assume "weakSimStepAct (P ∥ !P) (a<νx> ≺ Q') (P ∥ !P) (bangRel Rel')" and "x ♯ P" then obtain P' where PTrans: "(P ∥ !P) ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans have "!P ⟹a<νx> ≺ P'" by(force intro: Weak_Early_Step_Semantics.Bang simp add: weakTransition_def) with P'RelQ' show "∃P'. !P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ (bangRel Rel')" by blast next fix Q' α assume "weakSimStepAct (P ∥ !P) (α ≺ Q') (P ∥ !P) (bangRel Rel')" then obtain P' where PTrans: "(P ∥ !P) ⟹α ≺ P'" and P'RelQ': "(P', Q') ∈ (bangRel Rel')" by(simp add: weakSimStepAct_def, blast) from PTrans have "!P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Bang) with P'RelQ' show "∃P'. !P ⟹α ≺ P' ∧ (P', Q') ∈ (bangRel Rel')" by blast qed qed qed qed moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) ultimately show ?thesis by(simp add: simDef) qed *) end