(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Step_Semantics imports Late_Tau_Chain begin definition inputTransition :: "pi ⇒ name ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool" (‹_ ⟹⇩_{l}_ in _→_<_> ≺ _› [80, 80, 80, 80, 80] 80) where "P ⟹⇩_{l}u in P'' →a<x> ≺ P' ≡ ∃P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩_{τ}P'" definition transition :: "(pi × Late_Semantics.residual) set" where "transition ≡ {x. ∃P P' α P'' P'''. P ⟹⇩_{τ}P' ∧ P' ⟼α ≺ P'' ∧ P'' ⟹⇩_{τ}P''' ∧ x = (P, α ≺ P''')} ∪ {x. ∃P P' a y P'' P'''. P ⟹⇩_{τ}P' ∧ (P' ⟼(a<νy> ≺ P'')) ∧ P'' ⟹⇩_{τ}P''' ∧ x = (P, (a<νy> ≺ P'''))}" abbreviation weakTransition_judge :: "pi ⇒ Late_Semantics.residual ⇒ bool" (‹_ ⟹⇩_{l}_› [80, 80] 80) where "P ⟹⇩_{l}Rs ≡ (P, Rs) ∈ transition" lemma weakNonInput[dest]: fixes P :: pi and a :: name and x :: name and P' :: pi assumes "P ⟹⇩_{l}a<x> ≺ P'" shows False using assms by(auto simp add: transition_def residual.inject) lemma transitionI: fixes P :: pi and P''' :: pi and α :: freeRes and P'' :: pi and P' :: pi and a :: name and x :: name and u :: name shows "⟦P ⟹⇩_{τ}P'''; P''' ⟼α ≺ P''; P'' ⟹⇩_{τ}P'⟧ ⟹ P ⟹⇩_{l}α ≺ P'" and "⟦P ⟹⇩_{τ}P'''; P''' ⟼a<νx> ≺ P''; P'' ⟹⇩_{τ}P'⟧ ⟹ P ⟹⇩_{l}a<νx> ≺ P'" and "⟦P ⟹⇩_{τ}P'''; P''' ⟼a<x> ≺ P''; P''[x::=u] ⟹⇩_{τ}P'⟧ ⟹ P ⟹⇩_{l}u in P''→a<x> ≺ P'" proof - assume "P ⟹⇩_{τ}P'''" and "P''' ⟼ α ≺ P''" and "P'' ⟹⇩_{τ}P'" thus "P ⟹⇩_{l}α ≺ P'" by(force simp add: transition_def) next assume "P ⟹⇩_{τ}P'''" and "P''' ⟼a<νx> ≺ P''" and "P'' ⟹⇩_{τ}P'" thus "P ⟹⇩_{l}a<νx> ≺ P'" by(force simp add: transition_def) next assume "P ⟹⇩_{τ}P'''" and "P''' ⟼a<x> ≺ P''" and "P''[x::=u] ⟹⇩_{τ}P'" thus "P ⟹⇩_{l}u in P''→a<x> ≺ P'" by(force simp add: inputTransition_def) qed lemma transitionE: fixes P :: pi and α :: freeRes and P' :: pi and P'' :: pi and a :: name and u :: name and x :: name shows "P ⟹⇩_{l}α ≺ P' ⟹ ∃P'' P'''. P ⟹⇩_{τ}P'' ∧ P'' ⟼α ≺ P''' ∧ P''' ⟹⇩_{τ}P'" (is "_ ⟹ ?thesis1") and "⟦P ⟹⇩_{l}a<νx> ≺ P'; x ♯ P⟧ ⟹ ∃P'' P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩_{τ}P'" and "⟦P ⟹⇩_{l}u in P''→a<x> ≺ P'⟧ ⟹ ∃P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩_{τ}P'" proof - assume "P ⟹⇩_{l}α ≺ P'" thus ?thesis1 by(auto simp add: transition_def residual.inject) next assume "P ⟹⇩_{l}a<νx> ≺ P'" and "x ♯ P" thus "∃P'' P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩_{τ}P'" using [[hypsubst_thin = true]] apply(auto simp add: transition_def residualInject name_abs_eq) apply(rule_tac x="[(x, y)] ∙ P''" in exI) apply(rule_tac x=P' in exI) apply(clarsimp) apply(auto) apply(subgoal_tac "x ♯ P''") apply(simp add: alphaBoundResidual name_swap) using freshChain apply(force dest: freshBoundDerivative) using eqvtChainI by simp next assume PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" thus "∃P'''. P ⟹⇩_{τ}P''' ∧ P''' ⟼ a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩_{τ}P'" by(auto simp add: inputTransition_def) qed lemma alphaInput: fixes P :: pi and u :: name and P'' :: pi and a :: name and x :: name and P' :: pi and y :: name assumes PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and yFreshP: "y ♯ P" shows "P ⟹⇩_{l}u in ([(x, y)] ∙ P'')→a<y> ≺ P'" proof(cases "x=y") assume "x=y" with PTrans show ?thesis by simp next assume xineqy: "x≠y" from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain yFreshP have "y ♯ P'''" by(rule freshChain) with P'''Trans xineqy have yFreshP'': "y ♯ P''" by(blast dest: freshBoundDerivative) with P'''Trans have "P''' ⟼a<y> ≺ [(x, y)] ∙ P''" by(simp add: alphaBoundResidual) moreover from P''Chain yFreshP'' have "([(x, y)] ∙ P'')[y::=u] ⟹⇩_{τ}P'" by(simp add: renaming name_swap) ultimately show ?thesis using PChain by(blast intro: transitionI) qed lemma tauActionChain: fixes P :: pi and P' :: pi shows "P ⟹⇩_{l}τ ≺ P' ⟹ P ⟹⇩_{τ}P'" and "P ≠ P' ⟹ P ⟹⇩_{τ}P' ⟹ P ⟹⇩_{l}τ ≺ P'" proof - assume "P ⟹⇩_{l}τ ≺ P'" then obtain P'' P''' where "P ⟹⇩_{τ}P''" and "P'' ⟼τ ≺ P'''" and "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) thus "P ⟹⇩_{τ}P'" by auto next assume "P ⟹⇩_{τ}P'" and "P ≠ P'" thus "P ⟹⇩_{l}τ ≺ P'" proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have "P ⟹⇩_{τ}P''" and "P'' ⟼ τ ≺ P'''" by fact+ moreover have "P''' ⟹⇩_{τ}P'''" by simp ultimately show ?case by(rule transitionI) qed qed lemma singleActionChain: fixes P :: pi and a :: name and x :: name and α :: freeRes and u :: name shows "P ⟼a<νx> ≺ P' ⟹ P ⟹⇩_{l}a<νx> ≺ P'" and "⟦P ⟼a<x> ≺ P'⟧ ⟹ P ⟹⇩_{l}u in P'→a<x> ≺ P'[x::=u]" and "P ⟼α ≺ P' ⟹ P ⟹⇩_{l}α ≺ P'" proof - assume "P ⟼a<νx> ≺ P'" moreover have "P ⟹⇩_{τ}P" by simp moreover have "P' ⟹⇩_{τ}P'" by simp ultimately show "P ⟹⇩_{l}a<νx> ≺ P'" by(blast intro: transitionI) next assume "P ⟼a<x> ≺ P'" moreover have "P ⟹⇩_{τ}P" by simp moreover have "P'[x::=u] ⟹⇩_{τ}P'[x::=u]" by simp ultimately show "P ⟹⇩_{l}u in P'→a<x> ≺ P'[x::=u]" by(blast intro: transitionI) next assume "P ⟼α ≺ P'" moreover have "P ⟹⇩_{τ}P" by simp moreover have "P' ⟹⇩_{τ}P'" by simp ultimately show "P ⟹⇩_{l}α ≺ P'" by(blast intro: transitionI) qed lemma Tau: fixes P :: pi shows "τ.(P) ⟹⇩_{l}τ ≺ P" proof - have "τ.(P) ⟹⇩_{τ}τ.(P)" by simp moreover have "τ.(P) ⟼τ ≺ P" by(rule transitions.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 ⟹⇩_{l}u in P→a<x> ≺ P[x::=u]" proof - have "a<x>.P ⟹⇩_{τ}a<x>.P" by simp moreover have "a<x>.P ⟼ a<x> ≺ P" by(rule 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 ⟹⇩_{l}a[b] ≺ P" proof - have "a{b}.P ⟹⇩_{τ}a{b}.P" by simp moreover have "a{b}.P ⟼a[b] ≺ P" by(rule transitions.Output) moreover have "P ⟹⇩_{τ}P" by simp ultimately show ?thesis by(rule transitionI) qed lemma Match: fixes P :: pi and Rs :: residual and a :: name and u :: name and b :: name and x :: name and P' :: pi shows "P ⟹⇩_{l}Rs ⟹ [a⌢a]P ⟹⇩_{l}Rs" and "P ⟹⇩_{l}u in P''→b<x> ≺ P' ⟹ [a⌢a]P ⟹⇩_{l}u in P''→b<x> ≺ P'" proof - assume PTrans: "P ⟹⇩_{l}Rs" thus "[a⌢a]P ⟹⇩_{l}Rs" proof(nominal_induct avoiding: P rule: residual.strong_inducts) case(BoundR b x P') have PTrans: "P ⟹⇩_{l}b«x» ≺ P'" and xFreshP: "x ♯ P" by fact+ from PTrans obtain b' where beq: "b = BoundOutputS b'" by(cases b) auto with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼b'<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "[a⌢a]P ⟹⇩_{τ}[a⌢a]P" by simp moreover from P''Trans have "[a⌢a]P'' ⟼ b'<νx> ≺ P'''" by(rule Match) ultimately show ?thesis using beq P'''Trans by(blast intro: transitionI) next assume "P ≠ P''" with PTrans have "[a⌢a]P ⟹⇩_{τ}P''" by(rule matchChain) thus ?thesis using beq P''Trans P'''Trans by(blast intro: transitionI) qed next case(FreeR α P') have "P ⟹⇩_{l}α ≺ P'" by fact then obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼ α ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "[a⌢a]P ⟹⇩_{τ}[a⌢a]P" by simp moreover from P''Trans have "[a⌢a]P'' ⟼ α ≺ P'''" by(rule transitions.Match) ultimately show ?thesis using P'''Trans by(blast intro: transitionI) next assume "P ≠ P''" with PTrans have "[a⌢a]P ⟹⇩_{τ}P''" by(rule matchChain) thus ?thesis using P''Trans P'''Trans by(rule transitionI) qed qed next assume "P ⟹⇩_{l}u in P''→b<x> ≺ P'" then obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼b<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) show "[a⌢a]P ⟹⇩_{l}u in P''→b<x> ≺ P'" proof(cases "P=P'''") assume "P=P'''" moreover have "[a⌢a]P ⟹⇩_{τ}[a⌢a]P" by simp moreover from P'''Trans have "[a⌢a]P''' ⟼b<x> ≺ P''" by(rule Late_Semantics.Match) ultimately show ?thesis using P''Chain by(blast intro: transitionI) next assume "P ≠ P'''" with PChain 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 Rs :: residual and a :: name and c :: name and u :: name and b :: name and x :: name and P' :: pi shows "⟦P ⟹⇩_{l}Rs; a ≠ c⟧ ⟹ [a≠c]P ⟹⇩_{l}Rs" and "⟦P ⟹⇩_{l}u in P''→b<x> ≺ P'; a ≠ c⟧ ⟹ [a≠c]P ⟹⇩_{l}u in P''→b<x> ≺ P'" proof - assume PTrans: "P ⟹⇩_{l}Rs" and aineqc: "a ≠ c" thus "[a≠c]P ⟹⇩_{l}Rs" proof(nominal_induct avoiding: P rule: residual.strong_inducts) case(BoundR b x P') have PTrans: "P ⟹⇩_{l}b«x» ≺ P'" and xFreshP: "x ♯ P" by fact+ from PTrans obtain b' where beq: "b = BoundOutputS b'" by(cases b, auto) with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼b'<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "[a≠c]P ⟹⇩_{τ}[a≠c]P" by simp moreover from P''Trans aineqc have "[a≠c]P'' ⟼b'<νx> ≺ P'''" by(rule transitions.Mismatch) ultimately show ?thesis using beq P'''Trans by(blast intro: transitionI) next assume "P ≠ P''" with PTrans aineqc have "[a≠c]P ⟹⇩_{τ}P''" by(rule mismatchChain) thus ?thesis using beq P''Trans P'''Trans by(blast intro: transitionI) qed next case(FreeR α P') have "P ⟹⇩_{l}α ≺ P'" by fact then obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼ α ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "[a≠c]P ⟹⇩_{τ}[a≠c]P" by simp moreover from P''Trans ‹a ≠ c› have "[a≠c]P'' ⟼ α ≺ P'''" by(rule transitions.Mismatch) ultimately show ?thesis using P'''Trans by(blast intro: transitionI) next assume "P ≠ P''" with PTrans aineqc have "[a≠c]P ⟹⇩_{τ}P''" by(rule mismatchChain) thus ?thesis using P''Trans P'''Trans by(rule transitionI) qed qed next assume aineqc: "a ≠ c" assume "P ⟹⇩_{l}u in P''→b<x> ≺ P'" then obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼b<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) show "[a≠c]P ⟹⇩_{l}u in P''→b<x> ≺ P'" proof(cases "P=P'''") assume "P=P'''" moreover have "[a≠c]P ⟹⇩_{τ}[a≠c]P" by simp moreover from P'''Trans aineqc have "[a≠c]P''' ⟼b<x> ≺ P''" by(rule Late_Semantics.Mismatch) ultimately show ?thesis using P''Chain by(blast intro: transitionI) next assume "P ≠ P'''" with PChain aineqc have "[a≠c]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 Trans: "P ⟹⇩_{l}a[b] ≺ P'" and aInEqb: "a ≠ b" shows "<νb>P ⟹⇩_{l}a<νb> ≺ P'" proof - from Trans obtain P'' P''' where A: "P ⟹⇩_{τ}P''" and B: "P'' ⟼a[b] ≺ P'''" and C: "P''' ⟹⇩_{τ}P'" by(force dest: transitionE) from A have "<νb>P ⟹⇩_{τ}<νb>P''" by(rule ResChain) moreover from B aInEqb have "<νb>P'' ⟼a<νb> ≺ P'''" by(rule Open) ultimately show ?thesis using C by(force simp add: transition_def) qed lemma Sum1: fixes P :: pi and Rs :: residual and Q :: pi and u :: name and P'' :: pi and a :: name and x :: name and P' :: pi shows "P ⟹⇩_{l}Rs ⟹ P ⊕ Q ⟹⇩_{l}Rs" and "P ⟹⇩_{l}u in P''→a<x> ≺ P' ⟹ P ⊕ Q ⟹⇩_{l}u in P''→a<x> ≺ P'" proof - assume "P ⟹⇩_{l}Rs" thus "P ⊕ Q ⟹⇩_{l}Rs" proof(nominal_induct avoiding: P rule: residual.strong_inducts) case(BoundR a x P' P) have PTrans: "P ⟹⇩_{l}a«x» ≺ P'" and xFreshP: "x ♯ P" by fact+ from PTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto) with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼a'<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from P''Trans have "P'' ⊕ Q ⟼a'<νx> ≺ P'''" by(rule transitions.Sum1) ultimately show ?thesis using P'''Trans aeq by(blast intro: transitionI) next assume "P ≠ P''" with PTrans have "P ⊕ Q ⟹⇩_{τ}P''" by(rule sum1Chain) thus ?thesis using P''Trans P'''Trans aeq by(blast intro: transitionI) qed next case(FreeR α P') have "P ⟹⇩_{l}α ≺ P'" by fact then obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼ α ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) show ?case proof(cases "P = P''") assume "P = P''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from P''Trans have "P'' ⊕ Q ⟼ α ≺ P'''" by(rule transitions.Sum1) ultimately show ?thesis using P'''Trans by(blast intro: transitionI) next assume "P ≠ P''" with PTrans have "P ⊕ Q ⟹⇩_{τ}P''" by(rule sum1Chain) thus ?thesis using P''Trans P'''Trans by(rule transitionI) qed qed next assume "P ⟹⇩_{l}u in P''→a<x> ≺ P'" then obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) show "P ⊕ Q ⟹⇩_{l}u in P''→a<x> ≺ P'" proof(cases "P = P'''") assume "P = P'''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from P'''Trans have "P''' ⊕ Q ⟼a<x> ≺ P''" by(rule transitions.Sum1) ultimately show ?thesis using P''Chain by(blast intro: transitionI) next assume "P ≠ P'''" with PChain have "P ⊕ Q ⟹⇩_{τ}P'''" by(rule sum1Chain) thus ?thesis using P'''Trans P''Chain by(blast intro: transitionI) qed qed lemma Sum2: fixes Q :: pi and Rs :: residual and P :: pi and u :: name and Q'' :: pi and a :: name and x :: name and Q' :: pi shows "Q ⟹⇩_{l}Rs ⟹ P ⊕ Q ⟹⇩_{l}Rs" and "Q ⟹⇩_{l}u in Q''→a<x> ≺ Q' ⟹ P ⊕ Q ⟹⇩_{l}u in Q''→a<x> ≺ Q'" proof - assume "Q ⟹⇩_{l}Rs" thus "P ⊕ Q ⟹⇩_{l}Rs" proof(nominal_induct avoiding: Q rule: residual.strong_inducts) case(BoundR a x Q' Q) have QTrans: "Q ⟹⇩_{l}a«x» ≺ Q'" and xFreshQ: "x ♯ Q" by fact+ from QTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto) with QTrans xFreshQ obtain Q'' Q''' where QTrans: "Q ⟹⇩_{τ}Q''" and Q''Trans: "Q'' ⟼a'<νx> ≺ Q'''" and Q'''Trans: "Q''' ⟹⇩_{τ}Q'" by(blast dest: transitionE) show ?case proof(cases "Q = Q''") assume "Q = Q''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from Q''Trans have "P ⊕ Q'' ⟼a'<νx> ≺ Q'''" by(rule transitions.Sum2) ultimately show ?thesis using Q'''Trans aeq by(blast intro: transitionI) next assume "Q ≠ Q''" with QTrans have "P ⊕ Q ⟹⇩_{τ}Q''" by(rule sum2Chain) thus ?thesis using Q''Trans Q'''Trans aeq by(blast intro: transitionI) qed next case(FreeR α Q') have "Q ⟹⇩_{l}α ≺ Q'" by fact then obtain Q'' Q''' where QTrans: "Q ⟹⇩_{τ}Q''" and Q''Trans: "Q'' ⟼ α ≺ Q'''" and Q'''Trans: "Q''' ⟹⇩_{τ}Q'" by(blast dest: transitionE) show ?case proof(cases "Q = Q''") assume "Q = Q''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from Q''Trans have "P ⊕ Q'' ⟼ α ≺ Q'''" by(rule transitions.Sum2) ultimately show ?thesis using Q'''Trans by(blast intro: transitionI) next assume "Q ≠ Q''" with QTrans have "P ⊕ Q ⟹⇩_{τ}Q''" by(rule sum2Chain) thus ?thesis using Q''Trans Q'''Trans by(rule transitionI) qed qed next assume "Q ⟹⇩_{l}u in Q''→a<x> ≺ Q'" then obtain Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<x> ≺ Q''" and Q''Chain: "Q''[x::=u] ⟹⇩_{τ}Q'" by(blast dest: transitionE) show "P ⊕ Q ⟹⇩_{l}u in Q''→a<x> ≺ Q'" proof(cases "Q = Q'''") assume "Q = Q'''" moreover have "P ⊕ Q ⟹⇩_{τ}P ⊕ Q" by simp moreover from Q'''Trans have "P ⊕ Q''' ⟼a<x> ≺ Q''" by(rule transitions.Sum2) ultimately show ?thesis using Q''Chain by(blast intro: transitionI) next assume "Q ≠ Q'''" with QChain have "P ⊕ Q ⟹⇩_{τ}Q'''" by(rule sum2Chain) thus ?thesis using Q'''Trans Q''Chain by(blast intro: transitionI) qed qed lemma Par1B: fixes P :: pi and a :: name and x :: name and P' :: pi and u :: name and P'' :: pi shows "⟦P ⟹⇩_{l}a<νx> ≺ P'; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩_{l}a<νx> ≺ (P' ∥ Q)" and "⟦P ⟹⇩_{l}u in P''→a<x> ≺ P'; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩_{l}u in (P'' ∥ Q)→a<x> ≺ P' ∥ Q" proof - assume PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" assume xFreshQ: "x ♯ Q" have Goal: "⋀P a x P' Q. ⟦P ⟹⇩_{l}a<νx> ≺ P'; x ♯ P; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩_{l}a<νx> ≺ (P' ∥ Q)" proof - fix P a x P' Q assume PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" assume xFreshP: "x ♯ P" assume xFreshQ: "x ♯ (Q::pi)" from PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼a<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans have "P ∥ Q ⟹⇩_{τ}P'' ∥ Q" by(rule Par1Chain) moreover from P''Trans xFreshQ have "P'' ∥ Q ⟼a<νx> ≺ (P''' ∥ Q)" by(rule Par1B) moreover from P'''Trans have "P''' ∥ Q ⟹⇩_{τ}P' ∥ Q" by(rule Par1Chain) ultimately show "P ∥ Q ⟹⇩_{l}a<νx> ≺ (P' ∥ Q)" by(rule transitionI) qed have "∃c::name. c ♯ (P, P', Q)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshP': "c ♯ P'" and cFreshQ: "c ♯ Q" by(force simp add: fresh_prod) from cFreshP' have "a<νx> ≺ P' = a<νc> ≺ ([(x, c)] ∙ P')" by(rule alphaBoundResidual) moreover have "a<νx> ≺ (P' ∥ Q) = a<νc> ≺ (([(x, c)] ∙ P') ∥ Q)" proof - from cFreshP' cFreshQ have "c ♯ P' ∥ Q" by simp hence "a<νx> ≺ (P' ∥ Q) = a<νc> ≺ ([(x, c)] ∙ (P' ∥ Q))" by(rule alphaBoundResidual) with cFreshQ xFreshQ show ?thesis by(simp add: name_fresh_fresh) qed ultimately show "P ∥ Q ⟹⇩_{l}a<νx> ≺ P' ∥ Q" using PTrans cFreshP cFreshQ by(force intro: Goal) next assume PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and xFreshQ: "x ♯ Q" from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q" by(rule Par1Chain) moreover from P'''Trans xFreshQ have "P''' ∥ Q ⟼a<x> ≺ (P'' ∥ Q)" by(rule Par1B) moreover have "(P'' ∥ Q)[x::=u] ⟹⇩_{τ}P' ∥ Q" proof - from P''Chain have "P''[x::=u] ∥ Q ⟹⇩_{τ}P' ∥ Q" by(rule Par1Chain) with xFreshQ show ?thesis by(simp add: forget) qed ultimately show "P ∥ Q ⟹⇩_{l}u in (P'' ∥ Q)→a<x> ≺ (P' ∥ Q)" by(rule transitionI) qed lemma Par1F: fixes P :: pi and α :: freeRes and P' :: pi assumes PTrans: "P ⟹⇩_{l}α ≺ P'" shows "P ∥ Q ⟹⇩_{l}α ≺ (P' ∥ Q)" proof - from PTrans obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼α ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans have "P ∥ Q ⟹⇩_{τ}P'' ∥ Q" by(rule Par1Chain) moreover from P''Trans have "P'' ∥ Q ⟼α ≺ (P''' ∥ Q)" by(rule transitions.Par1F) moreover from P'''Trans 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 and u :: name and Q'' :: pi shows "Q ⟹⇩_{l}a<νx> ≺ Q' ⟹ x ♯ P ⟹ P ∥ Q ⟹⇩_{l}a<νx> ≺ (P ∥ Q')" and "Q ⟹⇩_{l}u in Q''→a<x> ≺ Q' ⟹ x ♯ P ⟹ P ∥ Q ⟹⇩_{l}u in (P ∥ Q'')→a<x> ≺ P ∥ Q'" proof - assume QTrans: "Q ⟹⇩_{l}a<νx> ≺ Q'" assume xFreshP: "x ♯ P" have Goal: "⋀Q a x Q' P. ⟦Q ⟹⇩_{l}a<νx> ≺ Q'; x ♯ Q; x ♯ P⟧ ⟹ P ∥ Q ⟹⇩_{l}a<νx> ≺ (P ∥ Q')" proof - fix Q a x Q' P assume QTrans: "Q ⟹⇩_{l}a<νx> ≺ Q'" assume xFreshQ: "x ♯ Q" assume xFreshP: "x ♯ (P::pi)" from QTrans xFreshQ obtain Q'' Q''' where QTrans: "Q ⟹⇩_{τ}Q''" and Q''Trans: "Q'' ⟼a<νx> ≺ Q'''" and Q'''Trans: "Q''' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QTrans have "P ∥ Q ⟹⇩_{τ}P ∥ Q''" by(rule Par2Chain) moreover from Q''Trans xFreshP have "P ∥ Q'' ⟼a<νx> ≺ (P ∥ Q''')" by(rule Par2B) moreover from Q'''Trans have "P ∥ Q''' ⟹⇩_{τ}P ∥ Q'" by(rule Par2Chain) ultimately show "P ∥ Q ⟹⇩_{l}a<νx> ≺ (P ∥ Q')" by(rule transitionI) qed have "∃c::name. c ♯ (Q, Q', P)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshQ: "c ♯ Q" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P" by(force simp add: fresh_prod) from cFreshQ' have "a<νx> ≺ Q' = a<νc> ≺ ([(x, c)] ∙ Q')" by(rule alphaBoundResidual) moreover have "a<νx> ≺ (P ∥ Q') = a<νc> ≺ (P ∥ ([(x, c)] ∙ Q'))" proof - from cFreshQ' cFreshP have "c ♯ P ∥ Q'" by simp hence "a<νx> ≺ (P ∥ Q') = a<νc> ≺ ([(x, c)] ∙ (P ∥ Q'))" by(rule alphaBoundResidual) with cFreshP xFreshP show ?thesis by(simp add: name_fresh_fresh) qed ultimately show "P ∥ Q ⟹⇩_{l}a<νx> ≺ P ∥ Q'" using QTrans cFreshQ cFreshP by(force intro: Goal) next assume QTrans: "Q ⟹⇩_{l}u in Q''→a<x> ≺ Q'" and xFreshP: "x ♯ P" from QTrans obtain Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<x> ≺ Q''" and Q''Chain: "Q''[x::=u] ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QChain have "P ∥ Q ⟹⇩_{τ}P ∥ Q'''" by(rule Par2Chain) moreover from Q'''Trans xFreshP have "P ∥ Q''' ⟼a<x> ≺ (P ∥ Q'')" by(rule Par2B) moreover have "(P ∥ Q'')[x::=u] ⟹⇩_{τ}P ∥ Q'" proof - from Q''Chain have "P ∥ (Q''[x::=u]) ⟹⇩_{τ}P ∥ Q'" by(rule Par2Chain) with xFreshP show ?thesis by(simp add: forget) qed ultimately show "P ∥ Q ⟹⇩_{l}u in (P ∥ Q'')→a<x> ≺ (P ∥ Q')" by(rule transitionI) qed lemma Par2F: fixes Q :: pi and α :: freeRes and Q' :: pi assumes QTrans: "Q ⟹⇩_{l}α ≺ Q'" shows "P ∥ Q ⟹⇩_{l}α ≺ (P ∥ Q')" proof - from QTrans obtain Q'' Q''' where QTrans: "Q ⟹⇩_{τ}Q''" and Q''Trans: "Q'' ⟼α ≺ Q'''" and Q'''Trans: "Q''' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QTrans have "P ∥ Q ⟹⇩_{τ}P ∥ Q''" by(rule Par2Chain) moreover from Q''Trans have "P ∥ Q'' ⟼α ≺ (P ∥ Q''')" by(rule transitions.Par2F) moreover from Q'''Trans have "P ∥ Q''' ⟹⇩_{τ}P ∥ Q'" by(rule Par2Chain) ultimately show ?thesis by(rule transitionI) qed lemma Comm1: fixes P :: pi and b :: name and P'' :: pi and a :: name and x :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹⇩_{l}b in P'' →a<x> ≺ P'" and QTrans: "Q ⟹⇩_{l}a[b] ≺ Q'" shows "P ∥ Q ⟹⇩_{l}τ ≺ P' ∥ Q'" proof - from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=b] ⟹⇩_{τ}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''[x::=b] ∥ Q''" by(rule Comm1) moreover from P''Chain Q''Chain have "P''[x::=b] ∥ 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 x :: name and Q'' :: pi and Q' :: pi assumes PTrans: "P ⟹⇩_{l}a[b] ≺ P'" and QTrans: "Q ⟹⇩_{l}b in Q''→a<x> ≺ Q'" shows "P ∥ Q ⟹⇩_{l}τ ≺ 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''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<x> ≺ Q''" and Q''Chain: "Q''[x::=b] ⟹⇩_{τ}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''[x::=b])" by(rule Comm2) moreover from P''Chain Q''Chain have "P'' ∥ (Q''[x::=b]) ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) ultimately show ?thesis by(rule transitionI) qed lemma Close1: fixes P :: pi and y :: name and P'' :: pi and a :: name and x :: name and P' :: pi and Q :: pi and Q' :: pi assumes PTrans: "P ⟹⇩_{l}y in P''→a<x> ≺ P'" and QTrans: "Q ⟹⇩_{l}a<νy> ≺ Q'" and yFreshP: "y ♯ P" and yFreshQ: "y ♯ Q" shows "P ∥ Q ⟹⇩_{l}τ ≺ <νy>(P' ∥ Q')" proof - from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=y] ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans yFreshQ obtain Q'' Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<νy> ≺ Q''" and Q''Chain: "Q'' ⟹⇩_{τ}Q'" by(blast dest: transitionE) from PChain yFreshP have yFreshP''': "y ♯ P'''" by(rule freshChain) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from P'''Trans Q'''Trans yFreshP''' have "P''' ∥ Q''' ⟼τ ≺ <νy>(P''[x::=y] ∥ Q'')" by(rule Close1) moreover have "<νy>(P''[x::=y] ∥ Q'') ⟹⇩_{τ}<νy>(P' ∥ Q')" proof - from P''Chain Q''Chain have "P''[x::=y] ∥ Q'' ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) thus ?thesis by(rule ResChain) qed ultimately show "P ∥ Q ⟹⇩_{l}τ ≺ <νy>(P' ∥ Q')" by(rule transitionI) qed lemma Close2: fixes P :: pi and y :: name and a :: name and x :: name and P' :: pi and Q :: pi and Q'' :: pi and Q' :: pi assumes PTrans: "P ⟹⇩_{l}a<νy> ≺ P'" and QTrans: "Q ⟹⇩_{l}y in Q''→a<x> ≺ Q'" and yFreshP: "y ♯ P" and yFreshQ: "y ♯ Q" shows "P ∥ Q ⟹⇩_{l}τ ≺ <νy>(P' ∥ Q')" proof - from PTrans yFreshP obtain P'' P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<νy> ≺ P''" and P''Chain: "P'' ⟹⇩_{τ}P'" by(blast dest: transitionE) from QTrans obtain Q''' where QChain: "Q ⟹⇩_{τ}Q'''" and Q'''Trans: "Q''' ⟼a<x> ≺ Q''" and Q''Chain: "Q''[x::=y] ⟹⇩_{τ}Q'" by(blast dest: transitionE) from QChain yFreshQ have yFreshQ''': "y ♯ Q'''" by(rule freshChain) from PChain QChain have "P ∥ Q ⟹⇩_{τ}P''' ∥ Q'''" by(rule chainPar) moreover from P'''Trans Q'''Trans yFreshQ''' have "P''' ∥ Q''' ⟼τ ≺ <νy>(P'' ∥ (Q''[x::=y]))" by(rule Close2) moreover have "<νy>(P'' ∥ (Q''[x::=y])) ⟹⇩_{τ}<νy>(P' ∥ Q')" proof - from P''Chain Q''Chain have "P'' ∥ (Q''[x::=y]) ⟹⇩_{τ}P' ∥ Q'" by(rule chainPar) thus ?thesis by(rule ResChain) qed ultimately show "P ∥ Q ⟹⇩_{l}τ ≺ <νy>(P' ∥ Q')" by(rule transitionI) qed lemma ResF: fixes P :: pi and α :: freeRes and P' :: pi and x :: name assumes PTrans: "P ⟹⇩_{l}α ≺ P'" and xFreshAlpha: "x ♯ α" shows "<νx>P ⟹⇩_{l}α ≺ <ν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 xFreshAlpha have "<νx>P'' ⟼α ≺ <νx>P'''" by(rule transitions.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 and u :: name and P'' :: pi shows "⟦P ⟹⇩_{l}a<νx> ≺ P'; y ≠ a; y ≠ x; x ♯ P⟧ ⟹ <νy>P ⟹⇩_{l}a<νx> ≺ (<νy>P')" and "⟦P ⟹⇩_{l}u in P''→a<x> ≺ P'; y ≠ a; y ≠ x; y ≠ u⟧ ⟹ <νy>P ⟹⇩_{l}u in (<νy>P'')→a<x> ≺ (<νy>P')" proof - assume PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" and yineqa: "y ≠ a" and yineqx: "y ≠ x" and xFreshP: "x ♯ P" from PTrans xFreshP 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 yineqa yineqx have "<νy>P'' ⟼a<νx> ≺ (<νy>P''')" by(force intro: ResB) moreover from P'''Chain have "<νy>P''' ⟹⇩_{τ}<νy>P'" by(rule ResChain) ultimately show "<νy>P ⟹⇩_{l}a<νx> ≺ <νy>P'" by(rule transitionI) next assume PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and yineqa: "y ≠ a" and yineqx: "y ≠ x" and yinequ: "y ≠ u" from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "<νy>P ⟹⇩_{τ}<νy>P'''" by(rule ResChain) moreover from P'''Trans yineqa yineqx have "<νy>P''' ⟼a<x> ≺ (<νy>P'')" by(force intro: ResB) moreover have "(<νy>P'')[x::=u] ⟹⇩_{τ}<νy>P'" proof - from P''Chain have "<νy>(P''[x::=u]) ⟹⇩_{τ}<νy>P'" by(rule ResChain) with yineqx yinequ show ?thesis by(simp add: eqvt_subs[THEN sym]) qed ultimately show "<νy>P ⟹⇩_{l}u in (<νy>P'')→a<x> ≺ <νy>P'" by(rule transitionI) qed lemma Bang: fixes P :: pi and Rs :: residual and u :: name and P'' :: pi and a :: name and x :: name and P' :: pi shows "P ∥ !P ⟹⇩_{l}Rs ⟹ !P ⟹⇩_{l}Rs" and "P ∥ !P ⟹⇩_{l}u in P''→a<x> ≺ P' ⟹ !P ⟹⇩_{l}u in P''→a<x> ≺ P'" proof - assume "P ∥ !P ⟹⇩_{l}Rs" thus "!P ⟹⇩_{l}Rs" proof(nominal_induct avoiding: P rule: residual.strong_inducts) case(BoundR a x P' P) assume xFreshP: "x ♯ P" assume PTrans: "P ∥ !P ⟹⇩_{l}a«x» ≺ P'" from PTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto) with PTrans xFreshP 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 ⟹⇩_{l}a«x» ≺ P'" proof(cases "P'' = P ∥ !P") assume "P'' = P ∥ !P" moreover with P''Trans have "!P ⟼a'<νx> ≺ P'''" by(blast intro: transitions.Bang) ultimately show ?thesis using PChain P'''Chain aeq by(simp, rule_tac transitionI, auto) next assume "P'' ≠ P ∥ !P" with PChain have "!P ⟹⇩_{τ}P''" by(rule bangChain) with P''Trans P'''Chain aeq show ?thesis by(blast intro: transitionI) qed next fix α P' P assume "P ∥ !P ⟹⇩_{l}α ≺ 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 ⟹⇩_{l}α ≺ P'" proof(cases "P'' = P ∥ !P") assume "P'' = P ∥ !P" moreover with P''Trans have "!P ⟼α ≺ P'''" by(blast intro: transitions.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 next assume "P ∥ !P ⟹⇩_{l}u in P''→a<x> ≺ P'" then obtain P''' where PChain: "P ∥ !P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(force dest: transitionE) show "!P ⟹⇩_{l}u in P''→a<x> ≺ P'" proof(cases "P''' = P ∥ !P") assume "P''' = P ∥ !P" moreover with P'''Trans have "!P ⟼a<x> ≺ P''" by(blast intro: transitions.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 ⟹⇩_{l}τ ≺ P'" shows "P ⟹⇩_{τ}P'" using assms by(auto simp add: transition_def residualInject) lemma chainTransitionAppend: fixes P :: pi and P' :: pi and Rs :: residual and a :: name and x :: name and P'' :: pi and u :: name and P''' :: pi and α :: freeRes shows "P ⟹⇩_{τ}P' ⟹ P' ⟹⇩_{l}Rs ⟹ P ⟹⇩_{l}Rs" and "P ⟹⇩_{τ}P'' ⟹ P'' ⟹⇩_{l}u in P'''→a<x> ≺ P' ⟹ P ⟹⇩_{l}u in P'''→a<x> ≺ P'" and "P ⟹⇩_{l}a<νx> ≺ P'' ⟹ P'' ⟹⇩_{τ}P' ⟹ x ♯ P ⟹ P ⟹⇩_{l}a<νx> ≺ P'" and "P ⟹⇩_{l}u in P'''→a<x> ≺ P'' ⟹ P'' ⟹⇩_{τ}P' ⟹ P ⟹⇩_{l}u in P'''→a<x> ≺ P'" and "P ⟹⇩_{l}α ≺ P'' ⟹ P'' ⟹⇩_{τ}P' ⟹ P ⟹⇩_{l}α ≺ P'" proof - assume "P ⟹⇩_{τ}P'" and "P' ⟹⇩_{l}Rs" thus "P ⟹⇩_{l}Rs" by(auto simp add: transition_def residualInject) (blast dest: rtrancl_trans)+ next assume "P ⟹⇩_{τ}P''" and "P'' ⟹⇩_{l}u in P'''→a<x> ≺ P'" thus "P ⟹⇩_{l}u in P'''→a<x> ≺ P'" apply(auto simp add: inputTransition_def residualInject) by(blast dest: rtrancl_trans)+ next assume PTrans: "P ⟹⇩_{l}a<νx> ≺ P''" assume P''Chain: "P'' ⟹⇩_{τ}P'" assume xFreshP: "x ♯ P" from PTrans xFreshP 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 ⟹⇩_{l}a<νx> ≺ P'" by(rule transitionI) next assume PTrans: "P ⟹⇩_{l}u in P'''→a<x> ≺ P''" assume P''Chain: "P'' ⟹⇩_{τ}P'" from PTrans obtain P'''' where PChain: "P ⟹⇩_{τ}P''''" and P''''Trans: "P'''' ⟼a<x> ≺ P'''" and P'''Chain: "P'''[x::=u] ⟹⇩_{τ}P''" by(blast dest: transitionE) from P'''Chain P''Chain have "P'''[x::=u] ⟹⇩_{τ}P'" by auto with PChain P''''Trans show "P ⟹⇩_{l}u in P'''→a<x> ≺ P'" by(blast intro: transitionI) next assume PTrans: "P ⟹⇩_{l}α ≺ 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 ⟹⇩_{l}α ≺ P'" by(rule transitionI) qed lemma freshInputTransition: fixes P :: pi and a :: name and x :: name and u :: name and P'' :: pi and P' :: pi and c :: name assumes PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and cFreshP: "c ♯ P" and cinequ: "c ≠ u" shows "c ♯ P'" proof - from PTrans obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain cFreshP have cFreshP''': "c ♯ P'''" by(rule freshChain) show "c ♯ P'" proof(cases "x=c") assume xeqc: "x=c" from cinequ have "c ♯ P''[c::=u]" apply - by(rule fresh_fact2) with P''Chain xeqc show ?thesis by(force intro: freshChain) next assume xineqc: "x≠c" with P'''Trans cFreshP''' have "c ♯ P''" by(blast dest: freshBoundDerivative) with cinequ have "c ♯ P''[x::=u]" apply - apply(rule fresh_fact1) by simp with P''Chain show ?thesis by(rule freshChain) qed qed lemma freshBoundOutputTransition: fixes P :: pi and a :: name and x :: name and P' :: pi and c :: name assumes PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" and cFreshP: "c ♯ P" and cineqx: "c ≠ x" shows "c ♯ P'" proof - have Goal: "⋀P a x P' c. ⟦P ⟹⇩_{l}a<νx> ≺ P'; x ♯ P; c ♯ P; c ≠ x⟧ ⟹ c ♯ P'" proof - fix P a x P' c assume PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" assume xFreshP: "x ♯ P" assume cFreshP: "(c::name) ♯ P" assume cineqx: "c ≠ x" from PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼a<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans cFreshP have "c ♯ P''" by(rule freshChain) with P''Trans cineqx have "c ♯ P'''" by(blast dest: Late_Semantics.freshBoundDerivative) with P'''Trans show "c ♯ P'" by(rule freshChain) qed have "∃d::name. d ♯ (P, P', c)" by(blast intro: name_exists_fresh) then obtain d::name where dFreshP: "d ♯ P" and dFreshP': "d ♯ P'" and cineqd: "c ≠ d" by(force simp add: fresh_prod) from PTrans dFreshP' have "P ⟹⇩_{l}a<νd> ≺ ([(x, d)] ∙ P')" by(simp add: alphaBoundResidual) hence "c ♯ [(x, d)] ∙ P'" using dFreshP cFreshP cineqd by(rule Goal) with cineqd cineqx show ?thesis by(simp add: name_fresh_left name_calc) qed lemma freshTauTransition: fixes P :: pi and c :: name assumes PTrans: "P ⟹⇩_{l}τ ≺ P'" and cFreshP: "c ♯ P" shows "c ♯ P'" proof - from PTrans have "P ⟹⇩_{τ}P'" by(rule tauTransitionChain) thus ?thesis using cFreshP by(rule freshChain) qed lemma freshOutputTransition: fixes P :: pi and a :: name and b :: name and P' :: pi and c :: name assumes PTrans: "P ⟹⇩_{l}a[b] ≺ P'" and cFreshP: "c ♯ P" shows "c ♯ P'" proof - from PTrans obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼a[b] ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans cFreshP have "c ♯ P''" by(rule freshChain) with P''Trans have "c ♯ P'''" by(blast dest: Late_Semantics.freshFreeDerivative) with P'''Trans show ?thesis by(rule freshChain) qed lemma eqvtI: fixes P :: pi and Rs :: residual and perm :: "name prm" and u :: name and P'' :: pi and a :: name and x :: name and P' :: pi shows "P ⟹⇩_{l}Rs ⟹ (perm ∙ P) ⟹⇩_{l}(perm ∙ Rs)" and "P ⟹⇩_{l}u in P''→a<x> ≺ P' ⟹ (perm ∙ P) ⟹⇩_{l}(perm ∙ u) in (perm ∙ P'')→(perm ∙ a)<(perm ∙ x)> ≺ (perm ∙ P')" proof - assume "P ⟹⇩_{l}Rs" thus "(perm ∙ P) ⟹⇩_{l}(perm ∙ Rs)" proof(nominal_induct Rs avoiding: P rule: residual.strong_inducts) case(BoundR a x P' P) have PTrans: "P ⟹⇩_{l}a«x» ≺ P'" by fact moreover then obtain b where aeqb: "a = BoundOutputS b" by(cases a, auto) moreover have "x ♯ P" by fact ultimately obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼b<νx> ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans have "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P'')" by(rule eqvtChainI) moreover from P''Trans have "(perm ∙ P'') ⟼ (perm ∙ (b<νx> ≺ P'''))" by(rule eqvts) moreover from P'''Trans have "(perm ∙ P''') ⟹⇩_{τ}(perm ∙ P')" by(rule eqvtChainI) ultimately show ?case using aeqb by(force intro: transitionI) next case(FreeR α P' P) have "P ⟹⇩_{l}α ≺ P'" by fact then obtain P'' P''' where PTrans: "P ⟹⇩_{τ}P''" and P''Trans: "P'' ⟼α ≺ P'''" and P'''Trans: "P''' ⟹⇩_{τ}P'" by(blast dest: transitionE) from PTrans have "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P'')" by(rule eqvtChainI) moreover from P''Trans have "(perm ∙ P'') ⟼ (perm ∙ (α ≺ P'''))" by(rule eqvts) moreover from P'''Trans have "(perm ∙ P''') ⟹⇩_{τ}(perm ∙ P')" by(rule eqvtChainI) ultimately show ?case by(force intro: transitionI) qed next assume "P ⟹⇩_{l}u in P''→a<x> ≺ P'" then obtain P''' where PChain: "P ⟹⇩_{τ}P'''" and P'''Trans: "P''' ⟼a<x> ≺ P''" and P''Chain: "P''[x::=u] ⟹⇩_{τ}P'" by(blast dest: transitionE) from PChain have "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P''')" by(rule eqvtChainI) moreover from P'''Trans have "(perm ∙ P''') ⟼ (perm ∙ (a<x> ≺ P''))" by(rule eqvts) moreover from P''Chain have "(perm ∙ P''[x::=u]) ⟹⇩_{τ}(perm ∙ P')" by(rule eqvtChainI) ultimately show "(perm ∙ P) ⟹⇩_{l}(perm ∙ u) in (perm ∙ P'')→(perm ∙ a)<(perm ∙ x)> ≺ (perm ∙ P')" by(force intro: transitionI simp add: eqvt_subs[THEN sym] perm_bij) qed lemmas freshTransition = freshBoundOutputTransition freshOutputTransition freshInputTransition freshTauTransition end