(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Early_Step_Semantics imports Early_Tau_Chain begin lemma inputSupportDerivative: assumes "P ⟼a<x> ≺ P'" shows "(supp P') - {x} ⊆ supp P" using assms apply(nominal_induct rule: inputInduct) apply(auto simp add: pi.supp abs_supp supp_atm) apply(rule ccontr) apply(simp add: fresh_def[symmetric]) apply(drule_tac fresh_fact1) apply(rotate_tac 4) apply assumption apply(simp add: fresh_def) apply force apply(case_tac "x ♯ P") apply(drule_tac fresh_fact1) apply(rotate_tac 2) apply assumption apply(simp add: fresh_def) apply force apply(rotate_tac 2) apply(drule_tac fresh_fact2) apply(simp add: fresh_def) by force lemma outputSupportDerivative: fixes P :: pi and a :: name and b :: name and P' :: pi assumes "P ⟼a[b] ≺ P'" shows "(supp P') ⊆ ((supp P)::name set)" using assms by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp) lemma boundOutputSupportDerivative: assumes "P ⟼a<νx> ≺ P'" and "x ♯ P" shows "(supp P') - {x} ⊆ supp P" using assms by(nominal_induct rule: boundOutputInduct) (auto simp add: pi.supp abs_supp supp_atm dest: outputSupportDerivative) lemma tauSupportDerivative: assumes "P ⟼τ ≺ P'" shows "((supp P')::name set) ⊆ supp P" using assms proof(nominal_induct rule: tauInduct) case(Tau P) thus ?case by(force simp add: pi.supp) next case(Match P) thus ?case by(force simp add: pi.supp) next case(Mismatch P) thus ?case by(force simp add: pi.supp) next case(Sum1 P) thus ?case by(force simp add: pi.supp) next case(Sum2 P) thus ?case by(force simp add: pi.supp) next case(Par1 P) thus ?case by(force simp add: pi.supp) next case(Par2 P) thus ?case by(force simp add: pi.supp) next case(Comm1 P a b P' Q Q') from ‹P ⟼a<b> ≺ P'› have "(supp P') - {b} ⊆ supp P" by(rule inputSupportDerivative) moreover from ‹Q ⟼ a[b] ≺ Q'› have "((supp Q')::name set) ⊆ supp Q" by(rule outputSupportDerivative) moreover from ‹Q ⟼ a[b] ≺ Q'› have "b ∈ supp Q" by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp supp_atm) ultimately show ?case by(auto simp add: pi.supp) next case(Comm2 P a b P' Q Q') from ‹P ⟼ a[b] ≺ P'› have "((supp P')::name set) ⊆ supp P" by(rule outputSupportDerivative) moreover from ‹Q ⟼a<b> ≺ Q'› have "(supp Q') - {b} ⊆ supp Q" by(rule inputSupportDerivative) moreover from ‹P ⟼ a[b] ≺ P'› have "b ∈ supp P" by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp supp_atm) ultimately show ?case by(auto simp add: pi.supp) next case(Close1 P a x P' Q Q') thus ?case by(auto dest: inputSupportDerivative boundOutputSupportDerivative simp add: abs_supp pi.supp) next case(Close2 P a x P' Q Q') thus ?case by(auto dest: inputSupportDerivative boundOutputSupportDerivative simp add: abs_supp pi.supp) next case(Res P P' x) thus ?case by(force simp add: pi.supp abs_supp) next case(Bang P P') thus ?case by(force simp add: pi.supp) qed lemma tauChainSupportDerivative: fixes P :: pi and P' :: pi assumes "P ⟹⇩_{τ}P'" shows "((supp P')::name set) ⊆ (supp P)" using assms by(induct rule: tauChainInduct) (auto dest: tauSupportDerivative) definition outputTransition :: "pi ⇒ name ⇒ name ⇒ pi ⇒ bool" (‹_ ⟹_<ν_> ≺ _› [80, 80, 80, 80] 80) where "P ⟹a<νx> ≺ P' ≡ ∃P''' P''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩_{τ}P'" definition freeTransition :: "pi ⇒ freeRes⇒ pi ⇒ bool" (‹_ ⟹_ ≺ _› [80, 80, 80] 80) where "P ⟹α ≺ P' ≡ ∃P''' P''. P ⟹⇩_{τ}P''' ∧ P''' ⟼α ≺ P'' ∧ P'' ⟹⇩_{τ}P'" lemma transitionI: fixes P :: pi and P''' :: pi and α :: freeRes and P'' :: pi and P' :: pi and a :: name and x :: name shows "⟦P ⟹⇩_{τ}P'''; P''' ⟼α ≺ P''; P'' ⟹⇩_{τ}P'⟧ ⟹ P ⟹α ≺ P'" and "⟦P ⟹⇩_{τ}P'''; P''' ⟼a<νx> ≺ P''; P'' ⟹⇩_{τ}P'⟧ ⟹ P ⟹a<νx> ≺ P'" by(auto simp add: outputTransition_def freeTransition_def) lemma transitionE: fixes P :: pi and α :: freeRes and P' :: pi and a :: name and x :: name shows "P ⟹α ≺ P' ⟹ (∃P'' P'''. P ⟹⇩_{τ}P'' ∧ P'' ⟼α ≺ P''' ∧ P''' ⟹⇩_{τ}P')" and "P ⟹a<νx> ≺ P' ⟹ ∃P'' P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩_{τ}P'" by(auto simp add: outputTransition_def freeTransition_def) lemma weakTransitionAlpha: fixes P :: pi and a :: name and x :: name and P' :: pi and y :: name assumes PTrans: "P ⟹a<νx> ≺ P'" and "y ♯ P" shows "P ⟹a<νy> ≺ ([(x, y)] ∙ P')" proof(cases "y=x") case True with PTrans show ?thesis by simp next case False from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) note PChain moreover from PChain ‹y ♯ P› have "y ♯ P'''" by(rule freshChain) with P'''Trans have "y ♯ P''" using ‹y ≠ x› by(rule freshTransition) with P'''Trans have "P''' ⟼a<νy> ≺ ([(x, y)] ∙ P'')" by(simp add: alphaBoundOutput name_swap) moreover from P''Chain have "([(x, y)] ∙ P'') ⟹⇩_{τ}([(x, y)] ∙ P')" by(rule eqvtChainI) ultimately show ?thesis by(rule transitionI) qed lemma singleActionChain: fixes P :: pi and Rs :: residual shows "P ⟼a<νx> ≺ P' ⟹ P ⟹a<νx> ≺ P'" and "P ⟼α ≺ P' ⟹ P ⟹α ≺ P'" proof - have "P ⟹⇩_{τ}P" by simp moreover assume "P ⟼a<νx> ≺ P'" moreover have "P' ⟹⇩_{τ}P'" by simp ultimately show "P ⟹a<νx> ≺ P'" by(rule transitionI) next have "P ⟹⇩_{τ}P" by simp moreover assume "P ⟼α ≺ P'" moreover have "P' ⟹⇩_{τ}P'" by simp ultimately show "P ⟹α ≺ P'" by(rule transitionI) qed lemma Tau: fixes P :: pi shows "τ.(P) ⟹ τ ≺ P" proof - have "τ.(P) ⟹⇩_{τ}τ.(P)" by simp moreover have "τ.(P) ⟼τ ≺ P" by(rule Early_Semantics.Tau) moreover have "P ⟹⇩_{τ}P" by simp ultimately show ?thesis by(rule transitionI) qed lemma Input: fixes a :: name and x :: name and u :: name and P :: pi shows "a<x>.P ⟹ a<u> ≺ P[x::=u]" proof - have "a<x>.P ⟹⇩_{τ}a<x>.P" by simp moreover have "a<x>.P ⟼ a<u> ≺ P[x::=u]" by(rule Early_Semantics.Input) moreover have "P[x::=u] ⟹⇩_{τ}P[x::=u]" by simp ultimately show ?thesis by(rule transitionI) qed lemma Output: fixes a :: name and b :: name and P :: pi shows "a{b}.P ⟹a[b] ≺ P" proof - have "a{b}.P ⟹⇩_{τ}a{b}.P" by simp moreover have "a{b}.P ⟼a[b] ≺ P" by(rule Early_Semantics.Output) moreover have "P ⟹⇩_{τ}P" by simp ultimately show ?thesis by(rule transitionI) qed lemma Match: fixes P :: pi and b :: name and x :: name and a :: name and P' :: pi and α :: freeRes shows "P ⟹b<νx> ≺ P' ⟹ [a⌢a]P ⟹b<νx> ≺ P'" and "P ⟹α ≺ P' ⟹ [a⌢a]P ⟹α ≺ P'" proof - assume "P ⟹ b<νx> ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼b<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) show "[a⌢a]P ⟹b<νx> ≺ P'" proof(cases "P = P'''") case True have "[a⌢a]P ⟹⇩_{τ}[a⌢a]P" by simp moreover from ‹P = P'''› P'''Trans have "[a⌢a]P ⟼ b<νx> ≺ P''" by(rule_tac Early_Semantics.Match) auto ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹P ≠ P'''› have "[a⌢a]P ⟹⇩_{τ}P'''" by(rule matchChain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed next assume "P ⟹α ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) show "[a⌢a]P ⟹α ≺ P'" proof(cases "P = P'''") case True have "[a⌢a]P ⟹⇩_{τ}[a⌢a]P" by simp moreover from ‹P = P'''› P'''Trans have "[a⌢a]P ⟼α ≺ P''" by(rule_tac Early_Semantics.Match) auto ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹P ≠ P'''› have "[a⌢a]P ⟹⇩_{τ}P'''" by(rule matchChain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed qed lemma Mismatch: fixes P :: pi and c :: name and x :: name and a :: name and b :: name and P' :: pi and α :: freeRes shows "⟦P ⟹c<νx> ≺ P'; a ≠ b⟧ ⟹ [a≠b]P ⟹c<νx> ≺ P'" and "⟦P ⟹α ≺ P'; a ≠ b⟧ ⟹ [a≠b]P ⟹α ≺ P'" proof - assume "P ⟹c<νx> ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼c<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) assume "a ≠ b" show "[a≠b]P ⟹c<νx> ≺ P'" proof(cases "P = P'''") case True have "[a≠b]P ⟹⇩_{τ}[a≠b]P" by simp moreover from ‹P = P'''› ‹a ≠ b› P'''Trans have "[a≠b]P ⟼ c<νx> ≺ P''" by(rule_tac Early_Semantics.Mismatch) auto ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹a ≠ b› ‹P ≠ P'''› have "[a≠b]P ⟹⇩_{τ}P'''" by(rule mismatchChain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed next assume "P ⟹α ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) assume "a ≠ b" show "[a≠b]P ⟹α ≺ P'" proof(cases "P = P'''") case True have "[a≠b]P ⟹⇩_{τ}[a≠b]P" by simp moreover from ‹P = P'''› ‹a ≠ b› P'''Trans have "[a≠b]P ⟼α ≺ P''" by(rule_tac Early_Semantics.Mismatch) auto ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹a ≠ b› ‹P ≠ P'''› have "[a≠b]P ⟹⇩_{τ}P'''" by(rule mismatchChain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed qed lemma Open: fixes P :: pi and a :: name and b :: name and P' :: pi assumes PTrans: "P ⟹a[b] ≺ P'" and "a ≠ b" shows "<νb>P ⟹a<νb> ≺ P'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a[b] ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) from PChain have "<νb>P ⟹⇩_{τ}<νb>P'''" by(rule ResChain) moreover from P'''Trans ‹a ≠ b› have "<νb>P''' ⟼a<νb> ≺ P''" by(rule Open) ultimately show ?thesis using P''Chain by(rule transitionI) qed lemma Sum1: fixes P :: pi and a :: name and x :: name and P' :: pi and Q :: pi and α :: freeRes shows "P ⟹a<νx> ≺ P' ⟹ P ⊕ Q ⟹a<νx> ≺ P'" and "P ⟹α ≺ P' ⟹ P ⊕ Q ⟹α ≺ P'" proof - assume "P ⟹a<νx> ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) show "P ⊕ Q ⟹a<νx> ≺ P'" proof(cases "P = P'''") case True have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from P'''Trans ‹P = P'''› have "P ⊕ Q ⟼ a<νx> ≺ P''" by(blast intro: Sum1) ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹P ≠ P'''› have "P ⊕ Q ⟹⇩_{τ}P'''" by(rule sum1Chain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed next assume "P ⟹α ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) show "P ⊕ Q ⟹α ≺ P'" proof(cases "P = P'''") case True have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from P'''Trans ‹P = P'''› have "P ⊕ Q ⟼α ≺ P''" by(blast intro: Sum1) ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹P ≠ P'''› have "P ⊕ Q ⟹⇩_{τ}P'''" by(rule sum1Chain) thus ?thesis using P'''Trans P''Chain by(rule transitionI) qed qed lemma Sum2: fixes Q :: pi and a :: name and x :: name and Q' :: pi and P :: pi and α :: freeRes shows "Q ⟹a<νx> ≺ Q' ⟹ P ⊕ Q ⟹a<νx> ≺ Q'" and "Q ⟹α ≺ Q' ⟹ P ⊕ Q ⟹α ≺ Q'" proof - assume "Q ⟹a<νx> ≺ Q'" then obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(force dest: transitionE) show "P ⊕ Q ⟹a<νx> ≺ Q'" proof(cases "Q = Q'''") case True have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from Q'''Trans ‹Q = Q'''› have "P ⊕ Q ⟼a<νx> ≺ Q''" by(blast intro: Sum2) ultimately show ?thesis using Q''Chain by(rule transitionI) next case False from QChain ‹Q ≠ Q'''› have "P ⊕ Q ⟹⇩_{τ}Q'''" by(rule sum2Chain) thus ?thesis using Q'''Trans Q''Chain by(rule transitionI) qed next assume "Q ⟹α ≺ Q'" then obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼α ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(force dest: transitionE) show "P ⊕ Q ⟹α ≺ Q'" proof(cases "Q = Q'''") case True have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from Q'''Trans ‹Q = Q'''› have "P ⊕ Q ⟼α ≺ Q''" by(blast intro: Sum2) ultimately show ?thesis using Q''Chain by(rule transitionI) next case False from QChain ‹Q ≠ Q'''› have "P ⊕ Q ⟹⇩_{τ}Q'''" by(rule sum2Chain) thus ?thesis using Q'''Trans Q''Chain by(rule transitionI) qed qed lemma Par1B: fixes P :: pi and a :: name and x :: name and P' :: pi and Q :: pi assumes PTrans: "P ⟹a<νx> ≺ P'" and "x ♯ Q" shows "P ∥ Q ⟹a<νx> ≺ (P' ∥ Q)" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q" by(rule Par1Chain) moreover from P'''Trans ‹x ♯ Q› have "P''' ∥ Q ⟼a<νx> ≺ (P'' ∥ Q)" by(rule Early_Semantics.Par1B) moreover from P''Chain have "P'' ∥ Q ⟹⇩_{τ}P' ∥ Q" by(rule Par1Chain) ultimately show "P ∥ Q ⟹a<νx> ≺ (P' ∥ Q)" by(rule transitionI) qed lemma Par1F: fixes P :: pi and α :: freeRes and P' :: pi and Q :: pi assumes PTrans: "P ⟹α ≺ P'" shows "P ∥ Q ⟹α ≺ (P' ∥ Q)" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q" by(rule Par1Chain) moreover from P'''Trans have "P''' ∥ Q ⟼α ≺ (P'' ∥ Q)" by(rule Early_Semantics.Par1F) moreover from P''Chain have "P'' ∥ Q ⟹⇩_{τ}P' ∥ Q" by(rule Par1Chain) ultimately show ?thesis by(rule transitionI) qed lemma Par2B: fixes Q :: pi and a :: name and x :: name and Q' :: pi and P :: pi assumes QTrans: "Q ⟹a<νx> ≺ Q'" and "x ♯ P" shows "P ∥ Q ⟹a<νx> ≺ (P ∥ Q')" proof - from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QChain have "P ∥ Q ⟹⇩_{τ}P ∥ Q'''" by(rule Par2Chain) moreover from Q'''Trans ‹x ♯ P› have "P ∥ Q''' ⟼a<νx> ≺ (P ∥ Q'')" by(rule Early_Semantics.Par2B) moreover from Q''Chain have "P ∥ Q'' ⟹⇩_{τ}P ∥ Q'" by(rule Par2Chain) ultimately show "P ∥ Q ⟹a<νx> ≺ (P ∥ Q')" by(rule transitionI) qed lemma Par2F: fixes Q :: pi and α :: freeRes and Q' :: pi and P :: pi assumes QTrans: "Q ⟹α ≺ Q'" shows "P ∥ Q ⟹α ≺ (P ∥ Q')" proof - from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼α ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QChain have "P ∥ Q ⟹⇩_{τ}P ∥ Q'''" by(rule Par2Chain) moreover from Q'''Trans have "P ∥ Q''' ⟼α ≺ (P ∥ Q'')" by(rule Early_Semantics.Par2F) moreover from Q''Chain have "P ∥ Q'' ⟹⇩_{τ}P ∥ Q'" by(rule Par2Chain) ultimately show ?thesis by(rule transitionI) qed lemma Comm1: fixes P :: pi and a :: name and b :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹a<b> ≺ P'" and QTrans: "Q ⟹a[b] ≺ Q'" shows "P ∥ Q ⟹τ ≺ P' ∥ Q'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<b> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a[b] ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ P'' ∥ Q''" by(rule Early_Semantics.Comm1) moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) ultimately show ?thesis by(rule transitionI) qed lemma Comm2: fixes P :: pi and a :: name and b :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹a[b] ≺ P'" and QTrans: "Q ⟹a<b> ≺ Q'" shows "P ∥ Q ⟹τ ≺ P' ∥ Q'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a[b] ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<b> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ P'' ∥ Q''" by(rule Early_Semantics.Comm2) moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) ultimately show ?thesis by(rule transitionI) qed lemma Close1: fixes P :: pi and a :: name and x :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹a<x> ≺ P'" and QTrans: "Q ⟹a<νx> ≺ Q'" and "x ♯ P" shows "P ∥ Q ⟹τ ≺ <νx>(P' ∥ Q')" proof - from PTrans obtain P''' P'' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from PChain ‹x ♯ P› have "x ♯ P'''" by(rule freshChain) with P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ <νx>(P'' ∥ Q'')" by(rule Early_Semantics.Close1) moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) hence "<νx>(P'' ∥ Q'') ⟹⇩_{τ}<νx>(P' ∥ Q')" by(rule ResChain) ultimately show ?thesis by(rule transitionI) qed lemma Close2: fixes P :: pi and a :: name and x :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹a<νx> ≺ P'" and QTrans: "Q ⟹a<x> ≺ Q'" and xFreshQ: "x ♯ Q" shows "P ∥ Q ⟹τ ≺ <νx>(P' ∥ Q')" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<x> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from QChain ‹x ♯ Q› have "x ♯ Q'''" by(rule freshChain) with P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ <νx>(P'' ∥ Q'')" by(rule Early_Semantics.Close2) moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) hence "<νx>(P'' ∥ Q'') ⟹⇩_{τ}<νx>(P' ∥ Q')" by(rule ResChain) ultimately show ?thesis by(rule transitionI) qed lemma ResF: fixes P :: pi and α :: freeRes and P' :: pi and x :: name assumes PTrans: "P ⟹α ≺ P'" and "x ♯ α" shows "<νx>P ⟹α ≺ <νx>P'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "<νx>P ⟹⇩_{τ}<νx>P'''" by(rule ResChain) moreover from P'''Trans ‹x ♯ α› have "<νx>P''' ⟼α ≺ <νx>P''" by(rule Early_Semantics.ResF) moreover from P''Chain have "<νx>P'' ⟹⇩_{τ}<νx>P'" by(rule ResChain) ultimately show ?thesis by(rule transitionI) qed lemma ResB: fixes P :: pi and a :: name and x :: name and P' :: pi and y :: name assumes PTrans: "P ⟹a<νx> ≺ P'" and "y ≠ a" and "y ≠ x" shows "<νy>P ⟹a<νx> ≺ (<νy>P')" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "<νy>P ⟹⇩_{τ}<νy>P'''" by(rule ResChain) moreover from P'''Trans ‹y ≠ a› ‹y ≠ x› have "<νy>P''' ⟼a<νx> ≺ (<νy>P'')" by(rule Early_Semantics.ResB) moreover from P''Chain have "<νy>P'' ⟹⇩_{τ}<νy>P'" by(rule ResChain) ultimately show ?thesis by(rule transitionI) qed lemma Bang: fixes P :: pi and Rs :: residual shows "P ∥ !P ⟹a<νx> ≺ P' ⟹ !P ⟹a<νx> ≺ P'" and "P ∥ !P ⟹α ≺ P' ⟹ !P ⟹α ≺ P'" proof - assume PTrans: "P ∥ !P ⟹ a<νx> ≺ P'" from PTrans obtain P'' P''' where PChain: "P ∥ !P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(force dest: transitionE) show "!P ⟹a<νx> ≺ P'" proof(cases "P''' = P ∥ !P") case True have "!P ⟹⇩_{τ}!P" by simp moreover from P'''Trans ‹P''' = P ∥ !P› have "!P ⟼a<νx> ≺ P''" by(blast intro: Early_Semantics.Bang) ultimately show ?thesis using P''Chain by(rule transitionI) next case False from PChain ‹P''' ≠ P ∥ !P› have "!P ⟹⇩_{τ}P'''" by(rule bangChain) with P'''Trans P''Chain show ?thesis by(blast intro: transitionI) qed next fix α P' P assume "P ∥ !P ⟹α ≺ P'" then obtain P'' P''' where PChain: "P ∥ !P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼α ≺ P'''" and P'''Chain: "P''' ⟹⇩_{τ}P'" by(force dest: transitionE) show "!P ⟹α ≺ P'" proof(cases "P'' = P ∥ !P") assume "P'' = P ∥ !P" moreover with P''Trans have "!P ⟼α ≺ P'''" by(blast intro: Bang) ultimately show ?thesis using PChain P'''Chain by(rule_tac transitionI, auto) next assume "P'' ≠ P ∥ !P" with PChain have "!P ⟹⇩_{τ}P''" by(rule bangChain) with P''Trans P'''Chain show ?thesis by(blast intro: transitionI) qed qed lemma tauTransitionChain: fixes P :: pi and P' :: pi assumes "P ⟹τ ≺ P'" shows "P ⟹⇩_{τ}P'" using assms by(force dest: transitionE tauActTauChain) lemma chainTransitionAppend: fixes P :: pi and P' :: pi and Rs :: residual and a :: name and x :: name and P'' :: pi and α :: freeRes shows "P ⟹a<νx> ≺ P'' ⟹ P'' ⟹⇩_{τ}P' ⟹ P ⟹a<νx> ≺ P'" and "P ⟹α ≺ P'' ⟹ P'' ⟹⇩_{τ}P' ⟹ P ⟹α ≺ P'" and "P ⟹⇩_{τ}P'' ⟹ P'' ⟹a<νx> ≺ P' ⟹ P ⟹a<νx> ≺ P'" and "P ⟹⇩_{τ}P'' ⟹ P'' ⟹α ≺ P' ⟹ P ⟹α ≺ P'" proof - assume PTrans: "P ⟹ a<νx> ≺ P''" assume P''Chain: "P'' ⟹⇩_{τ}P'" from PTrans obtain P''' P'''' where PChain: "P ⟹⇩_{τ}P''''" and P''''Trans: "P'''' ⟼a<νx> ≺ P'''" and P'''Chain: "P''' ⟹⇩_{τ}P''" by(blast dest: transitionE) from P'''Chain P''Chain have "P''' ⟹⇩_{τ}P'" by auto with PChain P''''Trans show "P ⟹a<νx> ≺ P'" by(rule transitionI) next assume PTrans: "P ⟹α ≺ P''" assume P''Chain: "P'' ⟹⇩_{τ}P'" from PTrans obtain P''' P'''' where PChain: "P ⟹⇩_{τ}P''''" and P''''Trans: "P'''' ⟼α ≺ P'''" and P'''Chain: "P''' ⟹⇩_{τ}P''" by(blast dest: transitionE) from P'''Chain P''Chain have "P''' ⟹⇩_{τ}P'" by auto with PChain P''''Trans show "P ⟹α ≺ P'" by(rule transitionI) next assume PChain: "P ⟹⇩_{τ}P''" assume P''Trans: "P'' ⟹ a<νx> ≺ P'" from P''Trans obtain P''' P'''' where P''Chain: "P'' ⟹⇩_{τ}P''''" and P''''Trans: "P'''' ⟼a<νx> ≺ P'''" and P'''Chain: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain P''Chain have "P ⟹⇩_{τ}P''''" by auto thus "P ⟹a<νx> ≺ P'" using P''''Trans P'''Chain by(rule transitionI) next assume PChain: "P ⟹⇩_{τ}P''" assume P''Trans: "P'' ⟹α ≺ P'" from P''Trans obtain P''' P'''' where P''Chain: "P'' ⟹⇩_{τ}P''''" and P''''Trans: "P'''' ⟼α ≺ P'''" and P'''Chain: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain P''Chain have "P ⟹⇩_{τ}P''''" by auto thus "P ⟹α ≺ P'" using P''''Trans P'''Chain by(rule transitionI) qed lemma freshBoundOutputTransition: fixes P :: pi and a :: name and x :: name and P' :: pi and c :: name assumes PTrans: "P ⟹a<νx> ≺ P'" and "c ♯ P" and "c ≠ x" shows "c ♯ P'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain) with P'''Trans have "c ♯ P''" using ‹c ≠ x› by(rule Early_Semantics.freshTransition) with P''Chain show "c ♯ P'" by(rule freshChain) qed lemma freshTauTransition: fixes P :: pi and c :: name assumes PTrans: "P ⟹τ ≺ P'" and "c ♯ P" shows "c ♯ P'" proof - from PTrans have "P ⟹⇩_{τ}P'" by(rule tauTransitionChain) thus ?thesis using ‹c ♯ P› by(rule freshChain) qed lemma freshOutputTransition: fixes P :: pi and a :: name and b :: name and P' :: pi and c :: name assumes PTrans: "P ⟹a[b] ≺ P'" and "c ♯ P" shows "c ♯ P'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a[b] ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain) with P'''Trans have "c ♯ P''" by(rule Early_Semantics.freshTransition) with P''Chain show ?thesis by(rule freshChain) qed lemma eqvtI[eqvt]: fixes P :: pi and a :: name and x :: name and P' :: pi and p :: "name prm" and α :: freeRes shows "P ⟹a<νx> ≺ P' ⟹ (p ∙ P) ⟹(p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P')" and "P ⟹α ≺ P' ⟹ (p ∙ P) ⟹(p ∙ α) ≺ (p ∙ P')" proof - assume "P ⟹a<νx> ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νx> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "(p ∙ P) ⟹⇩_{τ}(p ∙ P''')" by(rule eqvtChainI) moreover from P'''Trans have "(p ∙ P''') ⟼ (p ∙ (a<νx> ≺ P''))" by(rule TransitionsEarly.eqvt) hence "(p ∙ P''') ⟼ (p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P'')" by(simp add: eqvts) moreover from P''Chain have "(p ∙ P'') ⟹⇩_{τ}(p ∙ P')" by(rule eqvtChainI) ultimately show "(p ∙ P) ⟹(p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P')" by(rule transitionI) next assume "P ⟹α ≺ P'" then obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼α ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "(p ∙ P) ⟹⇩_{τ}(p ∙ P''')" by(rule eqvtChainI) moreover from P'''Trans have "(p ∙ P''') ⟼ (p ∙ (α ≺ P''))" by(rule TransitionsEarly.eqvt) hence "(p ∙ P''') ⟼ (p ∙ α) ≺ (p ∙ P'')" by(simp add: eqvts) moreover from P''Chain have "(p ∙ P'') ⟹⇩_{τ}(p ∙ P')" by(rule eqvtChainI) ultimately show "(p ∙ P) ⟹(p ∙ α) ≺ (p ∙ P')" by(rule transitionI) qed lemma freshInputTransition: fixes P :: pi and a :: name and b :: name and P' :: pi and c :: name assumes PTrans: "P ⟹a<b> ≺ P'" and "c ♯ P" and "c ≠ b" shows "c ♯ P'" proof - from PTrans obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<b> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain) with P'''Trans have "c ♯ P''" using ‹c ≠ b› by(rule Early_Semantics.freshInputTransition) with P''Chain show ?thesis by(rule freshChain) qed lemmas freshTransition = freshBoundOutputTransition freshOutputTransition freshInputTransition freshTauTransition end