Quelle Semantics.thy
Sprache: Isabelle
|
|
(*
Title: Psi-calculi
Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Semantics
imports Frame
begin
nominal_datatype ('a, 'b, 'c) boundOutput =
BOut "'a::fs_name" "('a, 'b::fs_name, 'c::fs_name) psi" (‹_ ≺'' _› [110, 110] 110)
| BStep "«name¬ ('a, 'b, 'c) boundOutput" (‹(ν_)_› [110, 110] 110)
primrec BOresChain :: "name list ==> ('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput ==>
('a, 'b, 'c) boundOutput" where
Base: "BOresChain [] B = B"
| Step: "BOresChain (x#xs) B = (νx)(BOresChain xs B)"
abbreviation
BOresChainJudge (‹(ν*_)_› [80, 80] 80) where "(ν*xvec)B ≡ BOresChain xvec B"
lemma BOresChainEqvt[eqvt]:
fixes perm :: "name prm"
and lst :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
shows "perm ∙ ((ν*xvec)B) = (ν*(perm ∙ xvec))(perm ∙ B)"
by(induct_tac xvec, auto)
lemma BOresChainSimps[simp]:
fixes xvec :: "name list"
and N :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and N' :: 'a
and P' :: "('a, 'b, 'c) psi"
and B :: "('a, 'b, 'c) boundOutput"
and B' :: "('a, 'b, 'c) boundOutput"
shows "((ν*xvec)N ≺' P = N' ≺' P') = (xvec = [] ∧ N = N' ∧ P = P')"
and "(N' ≺' P' = (ν*xvec)N ≺' P) = (xvec = [] ∧ N = N' ∧ P = P')"
and "(N' ≺' P' = N ≺' P) = (N = N' ∧ P = P')"
and "((ν*xvec)B = (ν*xvec)B') = (B = B')"
by(induct xvec) (auto simp add: boundOutput.inject alpha)
lemma outputFresh[simp]:
fixes Xs :: "name set"
and xvec :: "name list"
and N :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "(Xs ♯* (N ≺' P)) = ((Xs ♯* N) ∧ (Xs ♯* P))"
and "(xvec ♯* (N ≺' P)) = ((xvec ♯* N) ∧ (xvec ♯* P))"
by(auto simp add: fresh_star_def)
lemma boundOutputFresh:
fixes x :: name
and xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
shows "(x ♯ ((ν*xvec)B)) = (x ∈ set xvec ∨ x ♯ B)"
by (induct xvec) (simp_all add: abs_fresh)
lemma boundOutputFreshSet:
fixes Xs :: "name set"
and xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
and x :: name
shows "Xs ♯* ((ν*xvec)B) = (∀x∈Xs. x ∈ set xvec ∨ x ♯ B)"
and "yvec ♯* ((ν*xvec)B) = (∀x∈(set yvec). x ∈ set xvec ∨ x ♯ B)"
and "Xs ♯* ((νx)B) = Xs ♯* [x].B"
and "xvec ♯* ((νx)B) = xvec ♯* [x].B"
by(simp add: fresh_star_def boundOutputFresh)+
lemma BOresChainSupp:
fixes xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
shows "(supp((ν*xvec)B)::name set) = (supp B) - (supp xvec)"
by(induct xvec)
(auto simp add: boundOutput.supp supp_list_nil supp_list_cons abs_supp supp_atm)
lemma boundOutputFreshSimps[simp]:
fixes Xs :: "name set"
and xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
and x :: name
shows "Xs ♯* xvec ==> (Xs ♯* ((ν*xvec)B)) = (Xs ♯* B)"
and "yvec ♯* xvec ==> yvec ♯* ((ν*xvec)B) = yvec ♯* B"
and "xvec ♯* ((ν*xvec)B)"
and "x ♯ xvec ==> x ♯ (ν*xvec)B = x ♯ B"
apply(simp add: boundOutputFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
apply(simp add: boundOutputFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
apply(simp add: boundOutputFreshSet)
by(simp add: BOresChainSupp fresh_def)
lemma boundOutputChainAlpha:
fixes p :: "name prm"
and xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
assumes xvecFreshB: "(p ∙ xvec) ♯* B"
and S: "set p ⊆ set xvec × set (p ∙ xvec)"
and "(set xvec) ⊆ (set yvec)"
shows "((ν*yvec)B) = ((ν*(p ∙ yvec))(p ∙ B))"
proof -
note pt_name_inst at_name_inst S
moreover from ‹(set xvec) ⊆ (set yvec)› have "set xvec ♯* ((ν*yvec)B)"
by(force simp add: boundOutputFreshSet)
moreover from xvecFreshB ‹(set xvec) ⊆ (set yvec)› have "set (p ∙ xvec) ♯* ((ν*yvec)B)"
by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
ultimately have "((ν*yvec)B) = p ∙ ((ν*yvec)B)"
by (rule_tac pt_freshs_freshs [symmetric])
then show ?thesis by(simp add: eqvts)
qed
lemma boundOutputChainAlpha':
fixes p :: "name prm"
and xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
and zvec :: "name list"
assumes xvecFreshB: "xvec ♯* B"
and S: "set p ⊆ set xvec × set yvec"
and "yvec ♯* ((ν*zvec)B)"
shows "((ν*zvec)B) = ((ν*(p ∙ zvec))(p ∙ B))"
proof -
note pt_name_inst at_name_inst S ‹yvec ♯* ((ν*zvec)B)›
moreover from xvecFreshB have "set (xvec) ♯* ((ν*zvec)B)"
by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
ultimately have "((ν*zvec)B) = p ∙ ((ν*zvec)B)"
by (rule_tac pt_freshs_freshs [symmetric]) auto
then show ?thesis by(simp add: eqvts)
qed
lemma boundOutputChainAlpha'':
fixes p :: "name prm"
and xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
assumes "(p ∙ xvec) ♯* M"
and "(p ∙ xvec) ♯* P"
and "set p ⊆ set xvec × set (p ∙ xvec)"
and "(set xvec) ⊆ (set yvec)"
shows "((ν*yvec)M ≺' P) = ((ν*(p ∙ yvec))(p ∙ M) ≺' (p ∙ P))"
using assms
by(subst boundOutputChainAlpha) auto
lemma boundOutputChainSwap:
fixes x :: name
and y :: name
and N :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and xvec :: "name list"
assumes "y ♯ N"
and "y ♯ P"
and "x ∈ (set xvec)"
shows "(ν*xvec)N ≺' P = (ν*([(x, y)] ∙ xvec))([(x ,y)] ∙ N) ≺' ([(x, y)] ∙ P)"
proof(case_tac "x=y")
assume "x=y"
thus ?thesis by simp
next
assume "x ≠ y"
with assms show ?thesis
by(rule_tac xvec="[x]" in boundOutputChainAlpha'') (auto simp add: calc_atm)
qed
lemma alphaBoundOutput:
fixes x :: name
and y :: name
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
assumes "y ♯ B"
shows "(νx)B = (νy)([(x, y)] ∙ B)"
using assms
by(auto simp add: boundOutput.inject alpha fresh_left calc_atm)
lemma boundOutputEqFresh:
fixes B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and C :: "('a, 'b, 'c) boundOutput"
and x :: name
and y :: name
assumes "(νx)B = (νy)C"
and "x ♯ B"
shows "y ♯ C"
using assms
by(auto simp add: boundOutput.inject alpha fresh_left calc_atm)
lemma boundOutputEqSupp:
fixes B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and C :: "('a, 'b, 'c) boundOutput"
and x :: name
and y :: name
assumes "(νx)B = (νy)C"
and "x ∈ supp B"
shows "y ∈ supp C"
using assms
apply(auto simp add: boundOutput.inject alpha fresh_left calc_atm)
apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
by(simp add: eqvts calc_atm)
lemma boundOutputChainEq:
fixes xvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
and B' :: "('a, 'b, 'c) boundOutput"
assumes "(ν*xvec)B = (ν*yvec)B'"
and "xvec ♯* yvec"
and "length xvec = length yvec"
shows "∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ distinctPerm p ∧ B = p ∙ B' ∧ (set (map fst p)) ⊆ (supp B) ∧ xvec ♯* B' ∧ yvec ♯* B"
proof -
obtain n where "n = length xvec" by auto
with assms show ?thesis
proof(induct n arbitrary: xvec yvec B B')
case(0 xvec yvec B B')
have Eq: "(ν*xvec)B = (ν*yvec)B'" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with ‹length xvec = length yvec› have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec B B')
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)B = (ν*yvec)B'› ‹xvec = x # xvec'› ‹length xvec = length yvec›
obtain y yvec' where "(ν*(x#xvec'))B = (ν*(y#yvec'))B'"
and "yvec = y#yvec'" and "length xvec' = length yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')B) = (νy)((ν*yvec')B')"
by simp
from ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹xvec ♯* yvec›
have "x ≠ y" and "xvec' ♯* yvec'" and "x ♯ yvec'" and "y ♯ xvec'"
by auto
have IH: "∧xvec yvec B B'. [(ν*xvec)(B::('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput) = (ν*yvec)B'; xvec ♯* yvec; length xvec = length yvec; n = length xvec] ==> ∃p. (set p) ⊆ (set xvec) × (set yvec) ∧ distinctPerm p ∧ B = p ∙ B' ∧ set(map fst p) ⊆ supp B ∧ xvec ♯* B' ∧ yvec ♯* B"
by fact
from EQ ‹x ≠ y› have EQ': "(ν*xvec')B = ([(x, y)] ∙ ((ν*yvec')B'))"
and xFreshB': "x ♯ ((ν*yvec')B')"
and yFreshB: "y ♯ ((ν*xvec')B)"
by(metis boundOutput.inject alpha)+
from xFreshB' ‹x ♯ yvec'› have "x ♯ B'"
by(auto simp add: boundOutputFresh) (simp add: fresh_def name_list_supp)+
from yFreshB ‹y ♯ xvec'› have "y ♯ B"
by(auto simp add: boundOutputFresh) (simp add: fresh_def name_list_supp)+
show ?case
proof(case_tac "x ♯ (ν*xvec')B")
assume xFreshB: "x ♯ (ν*xvec')B"
with EQ have yFreshB': "y ♯ (ν*yvec')B'"
by(rule boundOutputEqFresh)
with xFreshB' EQ' have "(ν*xvec')B = (ν*yvec')B'"
by(simp)
with ‹xvec' ♯* yvec'› ‹length xvec' = length yvec'› ‹length xvec' = n› IH
obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "distinctPerm p" and "B = p ∙ B'"
and "set(map fst p) ⊆ supp B" and "xvec' ♯* B'" and "yvec' ♯* B"
by blast
from S have "(set p) ⊆ set(x#xvec') × set(y#yvec')" by auto
moreover note ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹distinctPerm p› ‹B = p ∙ B'›
‹xvec' ♯* B'› ‹x ♯ B'› ‹x ♯ B'› ‹yvec' ♯* B› ‹y ♯ B› ‹set(map fst p) ⊆ supp B›
ultimately show ?case by auto
next
assume "¬(x ♯ (ν*xvec')B)"
hence xSuppB: "x ∈ supp((ν*xvec')B)"
by(simp add: fresh_def)
with EQ have ySuppB': "y ∈ supp ((ν*yvec')B')"
by(rule boundOutputEqSupp)
hence "y ♯ yvec'"
by(induct yvec') (auto simp add: boundOutput.supp abs_supp)
with ‹x ♯ yvec'› EQ' have "(ν*xvec')B = (ν*yvec')([(x, y)] ∙ B')"
by(simp add: eqvts)
with ‹xvec' ♯* yvec'› ‹length xvec' = length yvec'› ‹length xvec' = n› IH
obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "distinctPerm p" and "B = p ∙ [(x, y)] ∙ B'"
and "set(map fst p) ⊆ supp B" and "xvec' ♯* ([(x, y)] ∙ B')" and "yvec' ♯* B"
by blast
from xSuppB have "x ♯ xvec'"
by(induct xvec') (auto simp add: boundOutput.supp abs_supp)
with ‹x ♯ yvec'› ‹y ♯ xvec'› ‹y ♯ yvec'› S have "x ♯ p" and "y ♯ p"
apply(induct p)
by(auto simp add: name_list_supp) (auto simp add: fresh_def)
from S have "(set ((x, y)#p)) ⊆ (set(x#xvec')) × (set(y#yvec'))"
by force
moreover from ‹x ≠ y› ‹x ♯ p› ‹y ♯ p› S ‹distinctPerm p›
have "distinctPerm((x,y)#p)" by simp
moreover from ‹B = p ∙ [(x, y)] ∙ B'› ‹x ♯ p› ‹y ♯ p› have "B = [(x, y)] ∙ p ∙ B'"
by(subst perm_compose) simp
hence "B = ((x, y)#p) ∙ B'" by simp
moreover from ‹xvec' ♯* ([(x, y)] ∙ B')› have "([(x, y)] ∙ xvec') ♯* ([(x, y)] ∙ [(x, y)] ∙ B')"
by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹x ♯ xvec'› ‹y ♯ xvec'› ‹x ♯ B'› have "(x#xvec') ♯* B'" by simp
moreover from ‹y ♯ B› ‹yvec' ♯* B› have "(y#yvec') ♯* B" by simp
moreover from ‹set(map fst p) ⊆ supp B› xSuppB ‹x ♯ xvec'›
have "set(map fst ((x, y)#p)) ⊆ supp B"
by(simp add: BOresChainSupp)
ultimately show ?case using ‹xvec=x#xvec'› ‹yvec=y#yvec'›
by metis
qed
qed
qed
lemma boundOutputChainEqLength:
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: "'a::fs_name"
and Q :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q"
shows "length xvec = length yvec"
proof -
obtain n where "n = length xvec" by auto
with assms show ?thesis
proof(induct n arbitrary: xvec yvec M P N Q)
case(0 xvec yvec M P N Q)
from ‹0 = length xvec› have "xvec = []" by auto
moreover with ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q› have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case by simp
next
case(Suc n xvec yvec M P N Q)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' Q"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' Q)"
by simp
have IH: "∧xvec yvec M P N Q. [(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q::('a, 'b, 'c) psi); n = length xvec] ==> length xvec = length yvec"
by fact
show ?case
proof(case_tac "x = y")
assume "x = y"
with EQ have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' Q"
by(simp add: alpha boundOutput.inject)
with IH ‹length xvec' = n› have "length xvec' = length yvec'"
by blast
with ‹xvec = x#xvec'› ‹yvec=y#yvec'›
show ?case by simp
next
assume "x ≠ y"
with EQ have "(ν*xvec')M ≺' P = [(x, y)] ∙ (ν*yvec')N ≺' Q"
by(simp add: alpha boundOutput.inject)
hence "(ν*xvec')M ≺' P = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(simp add: eqvts)
with IH ‹length xvec' = n› have "length xvec' = length ([(x, y)] ∙ yvec')"
by blast
hence "length xvec' = length yvec'"
by simp
with ‹xvec = x#xvec'› ‹yvec=y#yvec'›
show ?case by simp
qed
qed
qed
lemma boundOutputChainEq':
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q"
and "xvec ♯* yvec"
shows "∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ distinctPerm p ∧ M = p ∙ N ∧ P = p ∙ Q ∧ xvec ♯* N ∧ xvec ♯* Q ∧ yvec ♯* M ∧ yvec ♯* P"
using assms
apply(frule_tac boundOutputChainEqLength)
apply(drule_tac boundOutputChainEq)
by(auto simp add: boundOutput.inject)
lemma boundOutputChainEq'':
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q"
and "xvec ♯* yvec"
and "distinct xvec"
and "distinct yvec"
obtains p where "(set p) ⊆ (set xvec) × set (p ∙ xvec)" and "distinctPerm p" and "yvec = p ∙ xvec" and "N = p ∙ M" and "Q = p ∙ P" and "xvec ♯* N" and "xvec ♯* Q" and "(p ∙ xvec) ♯* M" and "(p ∙ xvec) ♯* P"
proof -
assume "∧p. [set p ⊆ set xvec × set (p ∙ xvec); distinctPerm p; yvec = p ∙ xvec; N = p ∙ M; Q = p ∙ P; xvec ♯* N; xvec ♯* Q; (p ∙ xvec) ♯* M; (p ∙ xvec) ♯* P] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ distinctPerm p ∧ yvec = p ∙ xvec ∧ N = p ∙ M ∧ Q = p ∙ P ∧ xvec ♯* N ∧ xvec ♯* Q ∧ (p ∙ xvec) ♯* M ∧ (p ∙ xvec) ♯* P"
proof(induct n arbitrary: xvec yvec M P N Q)
case(0 xvec yvec M P N Q)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M P N Q)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' Q"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' Q)"
by simp
from ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹xvec ♯* yvec›
have "x ≠ y" and "xvec' ♯* yvec'" and "x ♯ yvec'" and "y ♯ xvec'"
by auto
from ‹distinct xvec› ‹distinct yvec› ‹xvec=x#xvec'› ‹yvec=y#yvec'› have "x ♯ xvec'" and "y ♯ yvec'" and "distinct xvec'" and "distinct yvec'"
by simp+
have IH: "∧xvec yvec M P N Q. [(ν*xvec)(M::'a) ≺' (P::('a, 'b, 'c) psi) = (ν*yvec)N ≺' Q; xvec ♯* yvec; distinct xvec; distinct yvec; n = length xvec] ==> ∃p. (set p) ⊆ (set xvec) × (set yvec) ∧ distinctPerm p ∧ yvec = p ∙ xvec ∧ N = p ∙ M ∧ Q = p ∙ P ∧ xvec ♯* N ∧ xvec ♯* Q ∧ (p ∙ xvec) ♯* M ∧ (p ∙ xvec) ♯* P"
by fact
from EQ ‹x ≠ y› ‹x ♯ yvec'› ‹y ♯ yvec'› ‹y ♯ xvec'› ‹x ♯ xvec'› have "(ν*xvec')M ≺' P = (ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)" and "x ♯ N" and "x ♯ Q" and "y ♯ M" and "y ♯ P"
apply -
apply(simp add: boundOutput.inject alpha eqvts)
apply(simp add: boundOutput.inject alpha eqvts)
apply(simp add: boundOutput.inject alpha eqvts)
by(simp add: boundOutput.inject alpha' eqvts)+
with ‹xvec' ♯* yvec'› ‹distinct xvec'› ‹distinct yvec'› ‹length xvec' = n› IH
obtain p where S: "(set p) ⊆ (set xvec') × (set yvec')" and "distinctPerm p" and "yvec' = p ∙ xvec'" and "([(x, y)] ∙ N) = p ∙ M" and "([(x, y)] ∙ Q) = p ∙ P" and "xvec' ♯* ([(x, y)] ∙ N)" and "xvec' ♯* ([(x, y)] ∙ Q)" and "yvec' ♯* M" and "yvec' ♯* P"
by metis
from S have "set((x, y)#p) ⊆ set(x#xvec') × set(y#yvec')" by auto
moreover from ‹x ♯ xvec'› ‹x ♯ yvec'› ‹y ♯ xvec'› ‹y ♯ yvec'› S have "x ♯ p" and "y ♯ p"
apply(induct p)
by(auto simp add: fresh_prod name_list_supp) (auto simp add: fresh_def)
with S ‹distinctPerm p› ‹x ≠ y› have "distinctPerm((x, y)#p)" by auto
moreover from ‹yvec' = p ∙ xvec'› ‹x ♯ p› ‹y ♯ p› ‹x ♯ xvec'› ‹y ♯ xvec'› have "(y#yvec') = ((x, y)#p) ∙ (x#xvec')"
by(simp add: eqvts calc_atm perm_compose freshChainSimps)
moreover from ‹([(x, y)] ∙ N) = p ∙ M›
have "([(x, y)] ∙ [(x, y)] ∙ N) = [(x, y)] ∙ p ∙ M"
by(simp add: pt_bij)
hence "N = ((x, y)#p) ∙ M" by simp
moreover from ‹([(x, y)] ∙ Q) = p ∙ P›
have "([(x, y)] ∙ [(x, y)] ∙ Q) = [(x, y)] ∙ p ∙ P"
by(simp add: pt_bij)
hence "Q = ((x, y)#p) ∙ P" by simp
moreover from ‹xvec' ♯* ([(x, y)] ∙ N)› have "([(x, y)] ∙ xvec') ♯* ([(x, y)] ∙ [(x, y)] ∙ N)"
by(subst fresh_star_bij)
with ‹x ♯ xvec'› ‹y ♯ xvec'› have "xvec' ♯* N" by simp
with ‹x ♯ N› have "(x#xvec') ♯* N" by simp
moreover from ‹xvec' ♯* ([(x, y)] ∙ Q)› have "([(x, y)] ∙ xvec') ♯* ([(x, y)] ∙ [(x, y)] ∙ Q)"
by(subst fresh_star_bij)
with ‹x ♯ xvec'› ‹y ♯ xvec'› have "xvec' ♯* Q" by simp
with ‹x ♯ Q› have "(x#xvec') ♯* Q" by simp
moreover from ‹y ♯ M› ‹yvec' ♯* M› have "(y#yvec') ♯* M" by simp
moreover from ‹y ♯ P› ‹yvec' ♯* P› have "(y#yvec') ♯* P" by simp
ultimately show ?case using ‹xvec=x#xvec'› ‹yvec=y#yvec'›
by metis
qed
ultimately show ?thesis by blast
qed
lemma boundOutputEqSupp':
fixes x :: name
and xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and y :: name
and yvec :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
assumes Eq: "(νx)((ν*xvec)M ≺' P) = (νy)((ν*yvec)N ≺' Q)"
and "x ≠ y"
and "x ♯ yvec"
and "x ♯ xvec"
and "y ♯ xvec"
and "y ♯ yvec"
and "xvec ♯* yvec"
and "x ∈ supp M"
shows "y ∈ supp N"
proof -
from Eq ‹x ≠ y› ‹x ♯ yvec› ‹y ♯ yvec› have "(ν*xvec)M ≺' P = (ν*yvec)([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(simp add: boundOutput.inject alpha eqvts)
then obtain p where S: "set p ⊆ set xvec × set yvec" and "M = p ∙ [(x, y)] ∙ N" and "distinctPerm p" using ‹xvec ♯* yvec›
by(blast dest: boundOutputChainEq')
with ‹x ∈ supp M› have "x ∈ supp(p ∙ [(x, y)] ∙ N)" by simp
hence "(p ∙ x) ∈ p ∙ supp(p ∙ [(x, y)] ∙ N)"
by(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])
with ‹x ♯ xvec› ‹x ♯ yvec› S ‹distinctPerm p› have "x ∈ supp([(x, y)] ∙ N)"
by(simp add: eqvts)
hence "([(x, y)] ∙ x) ∈ ([(x, y)] ∙ (supp([(x, y)] ∙ N)))"
by(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])
with ‹x ≠ y› show ?thesis by(simp add: calc_atm eqvts)
qed
lemma boundOutputChainOpenIH:
fixes xvec :: "name list"
and x :: name
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
and yvec :: "name list"
and y :: name
and B' :: "('a, 'b, 'c) boundOutput"
assumes Eq: "(ν*xvec)((νx)B) = (ν*yvec)((νy)B')"
and L: "length xvec = length yvec"
and xFreshB': "x ♯ B'"
and xFreshxvec: "x ♯ xvec"
and xFreshyvec: "x ♯ yvec"
shows "(ν*xvec)B = (ν*yvec)([(x, y)] ∙ B')"
using assms
proof(induct n=="length xvec" arbitrary: xvec yvec y B' rule: nat.induct)
case(zero xvec yvec y B')
have "0 = length xvec" and "length xvec = length yvec" by fact+
moreover have "(ν*xvec)(νx)B = (ν*yvec)(νy)B'" by fact
ultimately show ?case by(auto simp add: boundOutput.inject alpha)
next
case(Suc n xvec yvec y B')
have L: "length xvec = length yvec" and "Suc n = length xvec" by fact+
then obtain x' xvec' y' yvec' where xEq: "xvec = x'#xvec'" and yEq: "yvec = y'#yvec'"
and L': "length xvec' = length yvec'"
by(cases xvec, auto, cases yvec, auto)
have xFreshB': "x ♯ B'" by fact
have "x ♯ xvec" and "x ♯ yvec" by fact+
with xEq yEq have xineqx': "x ≠ x'" and xFreshxvec': "x ♯ xvec'"
and xineqy': "x ≠ y'" and xFreshyvec': "x ♯ yvec'"
by simp+
have "(ν*xvec)(νx)B = (ν*yvec)(νy)B'" by fact
with xEq yEq have Eq: "(νx')((ν*xvec')(νx)B) = (νy')((ν*yvec')(νy)B')" by simp
have "Suc n = length xvec" by fact
with xEq have L'': "n = length xvec'" by simp
have "(νx')((ν*xvec')B) = (νy')((ν*yvec')([(x, y)] ∙ B'))"
proof(case_tac "x'=y'")
assume x'eqy': "x' = y'"
with Eq have "(ν*xvec')(νx)B = (ν*yvec')(νy)B'" by(simp add: boundOutput.inject alpha)
hence "(ν*xvec')B = (ν*yvec')([(x, y)] ∙ B')" using L' xFreshB' xFreshxvec' xFreshyvec' L''
by(rule_tac Suc)
with x'eqy' show ?thesis by(simp add: boundOutput.inject alpha)
next
assume x'ineqy': "x' ≠ y'"
with Eq have Eq': "(ν*xvec')(νx)B = (ν*([(x', y')] ∙ yvec'))(ν([(x', y')] ∙ y))([(x', y')] ∙ B')"
and x'FreshB': "x' ♯ (ν*yvec')(νy)B'"
by(simp add: boundOutput.inject alpha eqvts)+
from L' have "length xvec' = length ([(x', y')] ∙ yvec')" by simp
moreover from xineqx' xineqy' xFreshB' have "x ♯ [(x', y')] ∙ B'" by(simp add: fresh_left calc_atm)
moreover from xineqx' xineqy' xFreshyvec' have "x ♯ [(x', y')] ∙ yvec'" by(simp add: fresh_left calc_atm)
ultimately have "(ν*xvec')B = (ν*([(x', y')] ∙ yvec'))([(x, ([(x', y')] ∙ y))] ∙ [(x', y')] ∙ B')" using Eq' xFreshxvec' L''
by(rule_tac Suc)
moreover from x'FreshB' have "x' ♯ (ν*yvec')([(x, y)] ∙ B')"
proof(case_tac "x' ♯ yvec'")
assume "x' ♯ yvec'"
with x'FreshB' have x'FreshB': "x' ♯ (νy)B'"
by(simp add: fresh_def BOresChainSupp)
show ?thesis
proof(case_tac "x'=y")
assume x'eqy: "x' = y"
show ?thesis
proof(case_tac "x=y")
assume "x=y"
with xFreshB' x'eqy show ?thesis by(simp add: BOresChainSupp fresh_def)
next
assume "x ≠ y"
with ‹x ♯ B'› have "y ♯ [(x, y)] ∙ B'" by(simp add: fresh_left calc_atm)
with x'eqy show ?thesis by(simp add: BOresChainSupp fresh_def)
qed
next
assume x'ineqy: "x' ≠ y"
with x'FreshB' have "x' ♯ B'" by(simp add: abs_fresh)
with xineqx' x'ineqy have "x' ♯ ([(x, y)] ∙ B')" by(simp add: fresh_left calc_atm)
thus ?thesis by(simp add: BOresChainSupp fresh_def)
qed
next
assume "¬x' ♯ yvec'"
thus ?thesis by(simp add: BOresChainSupp fresh_def)
qed
ultimately show ?thesis using x'ineqy' xineqx' xineqy'
apply(simp add: boundOutput.inject alpha eqvts)
apply(subst perm_compose[of "[(x', y')]"])
by(simp add: calc_atm)
qed
with xEq yEq show ?case by simp
qed
lemma boundOutputPar1Dest:
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)"
and "xvec ♯* R"
and "yvec ♯* R"
obtains T where "P = T ∥ R" and "(ν*xvec)M ≺' T = (ν*yvec)N ≺' Q"
proof -
assume "∧T. [P = T ∥ R; (ν*xvec)M ≺' T = (ν*yvec)N ≺' Q] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃T. P = T ∥ R ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' Q"
proof(induct n arbitrary: xvec yvec M N P Q R)
case(0 xvec yvec M N P Q R)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M N P Q R)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' (Q ∥ R)"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' (Q ∥ R))"
by simp
from ‹xvec ♯* R› ‹yvec ♯* R› ‹xvec = x#xvec'› ‹yvec = y#yvec'›
have "x ♯ R" and "xvec' ♯* R" and "y ♯ R" and "yvec' ♯* R" by auto
show ?case
proof(case_tac "x = y")
assume "x = y"
with EQ have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha)
with ‹xvec' ♯* R› ‹yvec' ♯* R› ‹length xvec' = n›
obtain T where "P = T ∥ R" and "(ν*xvec')M ≺' T = (ν*yvec')N ≺' Q"
by(drule_tac Suc) auto
with ‹xvec=x#xvec'› ‹yvec=y#yvec'› ‹x=y› show ?case
by(force simp add: boundOutput.inject alpha)
next
assume "x ≠ y"
with EQ ‹x ♯ R› ‹y ♯ R›
have "(ν*xvec')M ≺' P = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' (([(x, y)] ∙ Q) ∥ R)"
and xFreshQR: "x ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha eqvts)+
moreover from ‹yvec' ♯* R› have "([(x, y)] ∙ yvec') ♯* ([(x, y)] ∙ R)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹x ♯ R› ‹y ♯ R› have "([(x, y)] ∙ yvec') ♯* R" by simp
moreover note ‹xvec' ♯* R› ‹length xvec' = n›
ultimately obtain T where "P = T ∥ R" and A: "(ν*xvec')M ≺' T = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(drule_tac Suc) auto
from A have "(νx)((ν*xvec')M ≺' T) = (νx)((ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q))"
by(simp add: boundOutput.inject alpha)
moreover from xFreshQR have "x ♯ (ν*yvec')N ≺' Q"
by(force simp add: boundOutputFresh)
ultimately show ?thesis using ‹P = T ∥ R› ‹xvec=x#xvec'› ‹yvec=y#yvec'› xFreshQR
by(force simp add: alphaBoundOutput name_swap eqvts)
qed
qed
ultimately show ?thesis
by blast
qed
lemma boundOutputPar1Dest':
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)"
and "xvec ♯* yvec"
obtains T p where "set p ⊆ set xvec × set yvec" and "P = T ∥ (p ∙ R)" and "(ν*xvec)M ≺' T = (ν*yvec)N ≺' Q"
proof -
assume "∧p T. [set p ⊆ set xvec × set yvec; P = T ∥ (p ∙ R); (ν*xvec)M ≺' T = (ν*yvec)N ≺' Q] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃p T. set p ⊆ set xvec × set yvec ∧ P = T ∥ (p ∙ R) ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' Q"
proof(induct n arbitrary: xvec yvec M N P Q R)
case(0 xvec yvec M N P Q R)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M N P Q R)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' (Q ∥ R)"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence Eq: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' (Q ∥ R))"
by simp
from ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹xvec ♯* yvec› have "x ≠ y" and "x ♯ yvec'" and "y ♯ xvec'" and "xvec' ♯* yvec'"
by auto
from Eq ‹x ≠ y› have Eq': "(ν*xvec')M ≺' P = [(x, y)] ∙ (ν*yvec')N ≺' (Q ∥ R)"
and xFreshQR: "x ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha)+
have IH: "∧xvec yvec M N P Q R. [(ν*xvec)M ≺' (P::('a, 'b, 'c) psi) = (ν*yvec)N ≺' (Q ∥ R); xvec ♯* yvec; n = length xvec] ==> ∃p T. set p ⊆ set xvec × set yvec ∧ P = T ∥ (p ∙ R) ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' Q"
by fact
show ?case
proof(case_tac "x ♯ (ν*xvec')M ≺' P")
assume "x ♯ (ν*xvec')M ≺' P"
with Eq have yFreshQR: "y ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(rule boundOutputEqFresh)
with Eq' xFreshQR have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' (Q ∥ R)"
by simp
with ‹xvec' ♯* yvec'› ‹length xvec' = n›
obtain p T where S: "set p ⊆ set xvec' × set yvec'" and "P = T ∥ (p ∙ R)" and A: "(ν*xvec')M ≺' T = (ν*yvec')N ≺' Q"
by(drule_tac IH) auto
from yFreshQR xFreshQR have yFreshQ: "y ♯ (ν*yvec')N ≺' Q" and xFreshQ: "x ♯ (ν*yvec')N ≺' Q"
by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
hence "(νx)((ν*yvec')N ≺' Q) = (νy)((ν*yvec')N ≺' Q)" by (subst alphaBoundOutput) simp+
with A have "(νx)((ν*xvec')M ≺' T) = (νy)((ν*yvec')N ≺' Q)" by simp
with ‹xvec=x#xvec'› ‹yvec=y#yvec'› S ‹P = T ∥ (p ∙ R)› show ?case
by auto
next
assume "¬(x ♯ (ν*xvec')M ≺' P)"
hence "x ∈ supp((ν*xvec')M ≺' P)" by(simp add: fresh_def)
with Eq have "y ∈ supp((ν*yvec')N ≺' (Q ∥ R))"
by(rule boundOutputEqSupp)
hence "y ♯ yvec'" by(simp add: BOresChainSupp fresh_def)
with Eq' ‹x ♯ yvec'› have "(ν*xvec')M ≺' P = (ν*yvec')([(x, y)] ∙ N) ≺' (([(x, y)] ∙ Q) ∥ ([(x, y)] ∙ R))"
by(simp add: eqvts)
moreover note ‹xvec' ♯* yvec'› ‹length xvec' = n›
ultimately obtain p T where S: "set p ⊆ set xvec' × set yvec'" and "P = T ∥ (p ∙ [(x, y)] ∙ R)" and A: "(ν*xvec')M ≺' T = (ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(drule_tac IH) auto
from S have "set(p@[(x, y)]) ⊆ set(x#xvec') × set(y#yvec')" by auto
moreover from ‹P = T ∥ (p ∙ [(x, y)] ∙ R)› have "P = T ∥ ((p @ [(x, y)]) ∙ R)"
by(simp add: pt2[OF pt_name_inst])
moreover from xFreshQR have xFreshQ: "x ♯ (ν*yvec')N ≺' Q"
by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
with ‹x ♯ yvec'› ‹y ♯ yvec'› ‹x ≠ y› have "y ♯ (ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(simp add: fresh_left calc_atm)
with ‹x ♯ yvec'› ‹y ♯ yvec'› have "(νx)((ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)) = (νy)((ν*yvec')N ≺' Q)"
by(subst alphaBoundOutput) (assumption | simp add: eqvts)+
with A have "(νx)((ν*xvec')M ≺' T) = (νy)((ν*yvec')N ≺' Q)" by simp
ultimately show ?thesis using ‹xvec=x#xvec'› ‹yvec=y#yvec'›
by(rule_tac x="p@[(x, y)]" in exI) force
qed
qed
ultimately show ?thesis
by blast
qed
lemma boundOutputPar2Dest:
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)"
and "xvec ♯* Q"
and "yvec ♯* Q"
obtains T where "P = Q ∥ T" and "(ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
proof -
assume "∧T. [P = Q ∥ T; (ν*xvec)M ≺' T = (ν*yvec)N ≺' R] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃T. P = Q ∥ T ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
proof(induct n arbitrary: xvec yvec M N P Q R)
case(0 xvec yvec M N P Q R)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M N P Q R)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' (Q ∥ R)"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' (Q ∥ R))"
by simp
from ‹xvec ♯* Q› ‹yvec ♯* Q› ‹xvec = x#xvec'› ‹yvec = y#yvec'›
have "x ♯ Q" and "xvec' ♯* Q" and "y ♯ Q" and "yvec' ♯* Q" by auto
have IH: "∧xvec yvec M N P Q R. [(ν*xvec)M ≺' (P::('a, 'b, 'c) psi) = (ν*yvec)N ≺' (Q ∥ R); xvec ♯* Q; yvec ♯* Q; n = length xvec] ==> ∃T. P = Q ∥ T ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
by fact
show ?case
proof(case_tac "x = y")
assume "x = y"
with EQ have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha)
with ‹xvec' ♯* Q› ‹yvec' ♯* Q› ‹length xvec' = n›
obtain T where "P = Q ∥ T" and "(ν*xvec')M ≺' T = (ν*yvec')N ≺' R"
by(drule_tac IH) auto
with ‹xvec=x#xvec'› ‹yvec=y#yvec'› ‹x=y› show ?case
by(force simp add: boundOutput.inject alpha)
next
assume "x ≠ y"
with EQ ‹x ♯ Q› ‹y ♯ Q›
have "(ν*xvec')M ≺' P = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' (Q ∥ ([(x, y)] ∙ R))"
and xFreshQR: "x ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha eqvts)+
moreover from ‹yvec' ♯* Q› have "([(x, y)] ∙ yvec') ♯* ([(x, y)] ∙ Q)"
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹x ♯ Q› ‹y ♯ Q› have "([(x, y)] ∙ yvec') ♯* Q" by simp
moreover note ‹xvec' ♯* Q› ‹length xvec' = n›
ultimately obtain T where "P = Q ∥ T" and A: "(ν*xvec')M ≺' T = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ R)"
by(drule_tac IH) auto
from A have "(νx)((ν*xvec')M ≺' T) = (νx)((ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ R))"
by(simp add: boundOutput.inject alpha)
moreover from xFreshQR have "x ♯ (ν*yvec')N ≺' R"
by(force simp add: boundOutputFresh)
ultimately show ?thesis using ‹P = Q ∥ T› ‹xvec=x#xvec'› ‹yvec=y#yvec'› xFreshQR
by(force simp add: alphaBoundOutput name_swap eqvts)
qed
qed
ultimately show ?thesis
by blast
qed
lemma boundOutputPar2Dest':
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)"
and "xvec ♯* yvec"
obtains T p where "set p ⊆ set xvec × set yvec" and "P = (p ∙ Q) ∥ T" and "(ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
proof -
assume "∧p T. [set p ⊆ set xvec × set yvec; P = (p ∙ Q) ∥ T; (ν*xvec)M ≺' T = (ν*yvec)N ≺' R] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃p T. set p ⊆ set xvec × set yvec ∧ P = (p ∙ Q) ∥ T ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
proof(induct n arbitrary: xvec yvec M N P Q R)
case(0 xvec yvec M N P Q R)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M N P Q R)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' (Q ∥ R)› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' (Q ∥ R)"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence Eq: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' (Q ∥ R))"
by simp
from ‹xvec = x#xvec'› ‹yvec=y#yvec'› ‹xvec ♯* yvec› have "x ≠ y" and "x ♯ yvec'" and "y ♯ xvec'" and "xvec' ♯* yvec'"
by auto
from Eq ‹x ≠ y› have Eq': "(ν*xvec')M ≺' P = [(x, y)] ∙ (ν*yvec')N ≺' (Q ∥ R)"
and xFreshQR: "x ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(simp add: boundOutput.inject alpha)+
have IH: "∧xvec yvec M N P Q R. [(ν*xvec)M ≺' (P::('a, 'b, 'c) psi) = (ν*yvec)N ≺' (Q ∥ R); xvec ♯* yvec; n = length xvec] ==> ∃p T. set p ⊆ set xvec × set yvec ∧ P = (p ∙ Q) ∥ T ∧ (ν*xvec)M ≺' T = (ν*yvec)N ≺' R"
by fact
show ?case
proof(case_tac "x ♯ (ν*xvec')M ≺' P")
assume "x ♯ (ν*xvec')M ≺' P"
with Eq have yFreshQR: "y ♯ (ν*yvec')N ≺' (Q ∥ R)"
by(rule boundOutputEqFresh)
with Eq' xFreshQR have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' (Q ∥ R)"
by simp
with ‹xvec' ♯* yvec'› ‹length xvec' = n›
obtain p T where S: "set p ⊆ set xvec' × set yvec'" and "P = (p ∙ Q) ∥ T" and A: "(ν*xvec')M ≺' T = (ν*yvec')N ≺' R"
by(drule_tac IH) auto
from yFreshQR xFreshQR have yFreshR: "y ♯ (ν*yvec')N ≺' R" and xFreshQ: "x ♯ (ν*yvec')N ≺' R"
by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
hence "(νx)((ν*yvec')N ≺' R) = (νy)((ν*yvec')N ≺' R)" by (subst alphaBoundOutput) simp+
with A have "(νx)((ν*xvec')M ≺' T) = (νy)((ν*yvec')N ≺' R)" by simp
with ‹xvec=x#xvec'› ‹yvec=y#yvec'› S ‹P = (p ∙ Q) ∥ T› show ?case
by auto
next
assume "¬(x ♯ (ν*xvec')M ≺' P)"
hence "x ∈ supp((ν*xvec')M ≺' P)" by(simp add: fresh_def)
with Eq have "y ∈ supp((ν*yvec')N ≺' (Q ∥ R))"
by(rule boundOutputEqSupp)
hence "y ♯ yvec'" by(simp add: BOresChainSupp fresh_def)
with Eq' ‹x ♯ yvec'› have "(ν*xvec')M ≺' P = (ν*yvec')([(x, y)] ∙ N) ≺' (([(x, y)] ∙ Q) ∥ ([(x, y)] ∙ R))"
by(simp add: eqvts)
moreover note ‹xvec' ♯* yvec'› ‹length xvec' = n›
ultimately obtain p T where S: "set p ⊆ set xvec' × set yvec'" and "P = (p ∙ [(x, y)] ∙ Q) ∥ T" and A: "(ν*xvec')M ≺' T = (ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ R)"
by(drule_tac IH) auto
from S have "set(p@[(x, y)]) ⊆ set(x#xvec') × set(y#yvec')" by auto
moreover from ‹P = (p ∙ [(x, y)] ∙ Q) ∥ T› have "P = ((p @ [(x, y)]) ∙ Q) ∥ T"
by(simp add: pt2[OF pt_name_inst])
moreover from xFreshQR have xFreshR: "x ♯ (ν*yvec')N ≺' R"
by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
with ‹x ♯ yvec'› ‹y ♯ yvec'› ‹x ≠ y› have "y ♯ (ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ R)"
by(simp add: fresh_left calc_atm)
with ‹x ♯ yvec'› ‹y ♯ yvec'› have "(νx)((ν*yvec')([(x, y)] ∙ N) ≺' ([(x, y)] ∙ R)) = (νy)((ν*yvec')N ≺' R)"
by(subst alphaBoundOutput) (assumption | simp add: eqvts)+
with A have "(νx)((ν*xvec')M ≺' T) = (νy)((ν*yvec')N ≺' R)" by simp
ultimately show ?thesis using ‹xvec=x#xvec'› ‹yvec=y#yvec'›
by(rule_tac x="p@[(x, y)]" in exI) force
qed
qed
ultimately show ?thesis
by blast
qed
lemma boundOutputApp:
fixes xvec :: "name list"
and yvec :: "name list"
and B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
shows "(ν*(xvec@yvec))B = (ν*xvec)((ν*yvec)B)"
by(induct xvec) auto
lemma openInjectAuxAuxAux:
fixes x :: name
and xvec :: "name list"
shows "∃y yvec. x # xvec = yvec @ [y] ∧ length xvec = length yvec"
apply(induct xvec arbitrary: x)
apply auto
apply(subgoal_tac "∃y yvec. a # xvec = yvec @ [y] ∧ length xvec = length yvec")
apply(clarify)
apply(rule_tac x=y in exI)
by auto
lemma openInjectAuxAux:
fixes xvec1 :: "name list"
and xvec2 :: "name list"
and yvec :: "name list"
assumes "length(xvec1@xvec2) = length yvec"
shows "∃yvec1 yvec2. yvec = yvec1@yvec2 ∧ length xvec1 = length yvec1 ∧ length xvec2 = length yvec2"
using assms
apply(induct yvec arbitrary: xvec1)
apply simp
apply simp
apply(case_tac xvec1)
apply simp
apply simp
apply(subgoal_tac "∃yvec1 yvec2.
yvec = yvec1 @ yvec2 ∧ length list = length yvec1 ∧ length xvec2 = length yvec2")
apply(clarify)
apply(rule_tac x="a#yvec1" in exI)
apply(rule_tac x=yvec2 in exI)
by auto
lemma openInjectAux:
fixes xvec1 :: "name list"
and x :: name
and xvec2 :: "name list"
and yvec :: "name list"
assumes "length(xvec1@x#xvec2) = length yvec"
shows "∃yvec1 y yvec2. yvec = yvec1@y#yvec2 ∧ length xvec1 = length yvec1 ∧ length xvec2 = length yvec2"
using assms
apply(case_tac yvec)
apply simp
apply simp
apply(subgoal_tac "∃(yvec1::name list) (yvec2::name list). yvec1@yvec2 = list ∧ length xvec1 = length yvec1 ∧ length xvec2 = length yvec2")
apply(clarify)
apply hypsubst_thin
apply simp
apply(subgoal_tac "∃y (yvec::name list). a # yvec1 = yvec @ [y] ∧ length yvec1 = length yvec")
apply(clarify)
apply(rule_tac x=yvec in exI)
apply(rule_tac x=y in exI)
apply simp
apply(rule_tac x=yvec2 in exI)
apply simp
apply(rule openInjectAuxAuxAux)
apply(insert openInjectAuxAux)
apply simp
by blast
lemma boundOutputOpenDest:
fixes yvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and xvec1 :: "name list"
and x :: name
and xvec2 :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
assumes Eq: "(ν*(xvec1@x#xvec2))M ≺' P = (ν*yvec)N ≺' Q"
and "x ♯ xvec1"
and "x ♯ yvec"
and "x ♯ N"
and "x ♯ Q"
and "distinct yvec"
obtains yvec1 y yvec2 where "yvec=yvec1@y#yvec2" and "length xvec1 = length yvec1" and "length xvec2 = length yvec2"
and "(ν*(xvec1@xvec2))M ≺' P = (ν*(yvec1@yvec2))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
proof -
assume Ass: "∧yvec1 y yvec2.
[yvec = yvec1 @ y # yvec2; length xvec1 = length yvec1; length xvec2 = length yvec2;
(ν*(xvec1 @ xvec2))M ≺' P = (ν*(yvec1 @ yvec2))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)]
==> thesis"
from Eq have "length(xvec1@x#xvec2) = length yvec" by(rule boundOutputChainEqLength)
then obtain yvec1 y yvec2 where A: "yvec = yvec1@y#yvec2" and "length xvec1 = length yvec1"
and "length xvec2 = length yvec2"
by(metis openInjectAux sym)
from ‹distinct yvec› A have "y ♯ yvec2" by simp
from A ‹x ♯ yvec› have "x ♯ yvec2" and "x ♯ yvec1" by simp+
with Eq ‹length xvec1 = length yvec1› ‹x ♯ N› ‹x ♯ Q› ‹y ♯ yvec2› ‹x ♯ xvec1› A
have "(ν*(xvec1@xvec2))M ≺' P = (ν*(yvec1@yvec2))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(force dest: boundOutputChainOpenIH simp add: boundOutputApp BOresChainSupp fresh_def boundOutput.supp eqvts)
with ‹length xvec1 = length yvec1› ‹length xvec2 = length yvec2› A Ass show ?thesis
by blast
qed
lemma boundOutputOpenDest':
fixes yvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and xvec1 :: "name list"
and x :: name
and xvec2 :: "name list"
and N :: 'a
and Q :: "('a, 'b, 'c) psi"
assumes Eq: "(ν*(xvec1@x#xvec2))M ≺' P = (ν*yvec)N ≺' Q"
and "x ♯ xvec1"
and "x ♯ yvec"
and "x ♯ N"
and "x ♯ Q"
obtains yvec1 y yvec2 where "yvec=yvec1@y#yvec2" and "length xvec1 = length yvec1" and "length xvec2 = length yvec2"
and "(ν*(xvec1@xvec2))M ≺' P = (ν*(yvec1@[(x, y)] ∙ yvec2))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
proof -
assume Ass: "∧yvec1 y yvec2.
[yvec = yvec1 @ y # yvec2; length xvec1 = length yvec1; length xvec2 = length yvec2;
(ν*(xvec1 @ xvec2))M ≺' P = (ν*(yvec1 @ ([(x, y)] ∙ yvec2)))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)]
==> thesis"
from Eq have "length(xvec1@x#xvec2) = length yvec" by(rule boundOutputChainEqLength)
then obtain yvec1 y yvec2 where A: "yvec = yvec1@y#yvec2" and "length xvec1 = length yvec1"
and "length xvec2 = length yvec2"
by(metis openInjectAux sym)
from A ‹x ♯ yvec› have "x ♯ yvec2" and "x ♯ yvec1" by simp+
with Eq ‹length xvec1 = length yvec1› ‹x ♯ N› ‹x ♯ Q› ‹x ♯ xvec1› A
have "(ν*(xvec1@xvec2))M ≺' P = (ν*(yvec1@([(x, y)] ∙ yvec2)))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(force dest: boundOutputChainOpenIH simp add: boundOutputApp BOresChainSupp fresh_def boundOutput.supp eqvts)
with ‹length xvec1 = length yvec1› ‹length xvec2 = length yvec2› A Ass show ?thesis
by blast
qed
lemma boundOutputScopeDest:
fixes xvec :: "name list"
and M :: "'a::fs_name"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and yvec :: "name list"
and N :: 'a
and x :: name
and Q :: "('a, 'b, 'c) psi"
assumes "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (νz)Q"
and "z ♯ xvec"
and "z ♯ yvec"
obtains R where "P = (νz)R" and "(ν*xvec)M ≺' R = (ν*yvec)N ≺' Q"
proof -
assume "∧R. [P = (νz)R; (ν*xvec)M ≺' R = (ν*yvec)N ≺' Q] ==> thesis"
moreover obtain n where "n = length xvec" by auto
with assms have "∃R. P = (νz)R ∧ (ν*xvec)M ≺' R = (ν*yvec)N ≺' Q"
proof(induct n arbitrary: xvec yvec M N P Q z)
case(0 xvec yvec M N P Q z)
have Eq: "(ν*xvec)M ≺' P = (ν*yvec)N ≺' (νz)Q" by fact
from ‹0 = length xvec› have "xvec = []" by auto
moreover with Eq have "yvec = []"
by(case_tac yvec) auto
ultimately show ?case using Eq
by(simp add: boundOutput.inject)
next
case(Suc n xvec yvec M N P Q z)
from ‹Suc n = length xvec›
obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
by(case_tac xvec) auto
from ‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' ((νz)Q)› ‹xvec = x # xvec'›
obtain y yvec' where "(ν*(x#xvec'))M ≺' P = (ν*(y#yvec'))N ≺' (νz)Q"
and "yvec = y#yvec'"
by(case_tac yvec) auto
hence EQ: "(νx)((ν*xvec')M ≺' P) = (νy)((ν*yvec')N ≺' (νz)Q)"
by simp
from ‹z ♯ xvec› ‹z ♯ yvec› ‹xvec = x#xvec'› ‹yvec = y#yvec'›
have "z ≠ x" and "z ≠ y" and "z ♯ xvec'" and "z ♯ yvec'"
by simp+
have IH: "∧xvec yvec M N P Q z. [(ν*xvec)M ≺' (P::('a, 'b, 'c) psi) = (ν*yvec)N ≺' (νz)Q; z ♯ xvec; z ♯ yvec; n = length xvec] ==> ∃R. P = (νz)R ∧ (ν*xvec)M ≺' R = (ν*yvec)N ≺' Q"
by fact
show ?case
proof(case_tac "x = y")
assume "x = y"
with EQ have "(ν*xvec')M ≺' P = (ν*yvec')N ≺' (νz)Q"
by(simp add: boundOutput.inject alpha)
with ‹z ♯ xvec'› ‹z ♯ yvec'› ‹length xvec' = n›
obtain R where "P = (νz)R" and "(ν*xvec')M ≺' R = (ν*yvec')N ≺' Q"
by(drule_tac IH) auto
with ‹xvec=x#xvec'› ‹yvec=y#yvec'› ‹x=y› show ?case
by(force simp add: boundOutput.inject alpha)
next
assume "x ≠ y"
with EQ ‹z ≠ x› ‹z ≠ y›
have "(ν*xvec')M ≺' P = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' (νz)([(x, y)] ∙ Q)"
and xFreshzQ: "x ♯ (ν*yvec')N ≺' (νz)Q"
by(simp add: boundOutput.inject alpha eqvts)+
moreover from ‹z ≠ x› ‹z ≠ y› ‹z ♯ yvec'› ‹x ≠ y› have "z ♯ ([(x, y)] ∙ yvec')"
by(simp add: fresh_left calc_atm)
moreover note ‹z ♯ xvec'› ‹length xvec' = n›
ultimately obtain R where "P = (νz)R" and A: "(ν*xvec')M ≺' R = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q)"
by(drule_tac IH) auto
from A have "(νx)((ν*xvec')M ≺' R) = (νx)((ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ N) ≺' ([(x, y)] ∙ Q))"
by(simp add: boundOutput.inject alpha)
moreover from xFreshzQ ‹z ≠ x› have "x ♯ (ν*yvec')N ≺' Q"
by(simp add: boundOutputFresh abs_fresh)
ultimately show ?thesis using ‹P = (νz)R› ‹xvec=x#xvec'› ‹yvec=y#yvec'› xFreshzQ
by(force simp add: alphaBoundOutput name_swap eqvts)
qed
qed
ultimately show ?thesis
by blast
qed
nominal_datatype ('a, 'b, 'c) residual =
RIn "'a::fs_name" 'a "('a, 'b::fs_name, 'c::fs_name) psi"
| ROut 'a "('a, 'b, 'c) boundOutput"
| RTau "('a, 'b, 'c) psi"
nominal_datatype 'a action = In "'a::fs_name" 'a (‹_(_)› [90, 90] 90)
| Out "'a::fs_name" "name list" 'a (‹_(ν*_)⟨_⟩› [90, 90, 90] 90)
| Tau (‹τ› 90)
nominal_primrec bn :: "('a::fs_name) action ==> name list"
where
"bn (M(N)) = []"
| "bn (M(ν*xvec)⟨N⟩) = xvec"
| "bn (τ) = []"
by(rule TrueI)+
lemma bnEqvt[eqvt]:
fixes p :: "name prm"
and α :: "('a::fs_name) action"
shows "(p ∙ bn α) = bn(p ∙ α)"
by(nominal_induct α rule: action.strong_induct) auto
nominal_primrec create_residual :: "('a::fs_name) action ==> ('a, 'b::fs_name, 'c::fs_name) psi ==> ('a, 'b, 'c) residual" (‹_ ≺ _› [80, 80] 80)
where
"(M(N)) ≺ P = RIn M N P"
| "M(ν*xvec)⟨N⟩ ≺ P = ROut M ((ν*xvec)(N ≺' P))"
| "τ ≺ P = (RTau P)"
by(rule TrueI)+
nominal_primrec subject :: "('a::fs_name) action ==> 'a option"
where
"subject (M(N)) = Some M"
| "subject (M(ν*xvec)⟨N⟩) = Some M"
| "subject (τ) = None"
by(rule TrueI)+
nominal_primrec object :: "('a::fs_name) action ==> 'a option"
where
"object (M(N)) = Some N"
| "object (M(ν*xvec)⟨N⟩) = Some N"
| "object (τ) = None"
by(rule TrueI)+
lemma optionFreshChain[simp]:
fixes xvec :: "name list"
and X :: "name set"
shows "xvec ♯* (Some x) = xvec ♯* x"
and "X ♯* (Some x) = X ♯* x"
and "xvec ♯* None"
and "X ♯* None"
by(auto simp add: fresh_star_def fresh_some fresh_none)
lemmas [simp] = fresh_some fresh_none
lemma actionFresh[simp]:
fixes x :: name
and α :: "('a::fs_name) action"
shows "(x ♯ α) = (x ♯ (subject α) ∧ x ♯ (bn α) ∧ x ♯ (object α))"
by(nominal_induct α rule: action.strong_induct) auto
lemma actionFreshChain[simp]:
fixes X :: "name set"
and α :: "('a::fs_name) action"
and xvec :: "name list"
shows "(X ♯* α) = (X ♯* (subject α) ∧ X ♯* (bn α) ∧ X ♯* (object α))"
and "(xvec ♯* α) = (xvec ♯* (subject α) ∧ xvec ♯* (bn α) ∧ xvec ♯* (object α))"
by(auto simp add: fresh_star_def)
lemma subjectEqvt[eqvt]:
fixes p :: "name prm"
and α :: "('a::fs_name) action"
shows "(p ∙ subject α) = subject(p ∙ α)"
by(nominal_induct α rule: action.strong_induct) auto
lemma okjectEqvt[eqvt]:
fixes p :: "name prm"
and α :: "('a::fs_name) action"
shows "(p ∙ object α) = object(p ∙ α)"
by(nominal_induct α rule: action.strong_induct) auto
lemma create_residualEqvt[eqvt]:
fixes p :: "name prm"
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "(p ∙ (α ≺ P)) = (p ∙ α) ≺ (p ∙ P)"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: eqvts)
lemma residualFresh:
fixes x :: name
and α :: "'a::fs_name action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "(x ♯ (α ≺ P)) = (x ♯ (subject α) ∧ (x ∈ (set(bn(α))) ∨ (x ♯ object(α) ∧ x ♯ P)))"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: fresh_some fresh_none boundOutputFresh)
lemma residualFresh2[simp]:
fixes x :: name
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "x ♯ α"
and "x ♯ P"
shows "x ♯ α ≺ P"
using assms
by(nominal_induct α rule: action.strong_induct) auto
lemma residualFreshChain2[simp]:
fixes xvec :: "name list"
and X :: "name set"
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "[xvec ♯* α; xvec ♯* P] ==> xvec ♯* (α ≺ P)"
and "[X ♯* α; X ♯* P] ==> X ♯* (α ≺ P)"
by(auto simp add: fresh_star_def)
lemma residualFreshSimp[simp]:
fixes x :: name
and M :: "'a::fs_name"
and N :: 'a
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "x ♯ (M(N) ≺ P) = (x ♯ M ∧ x ♯ N ∧ x ♯ P)"
and "x ♯ (M(ν*xvec)⟨N⟩ ≺ P) = (x ♯ M ∧ x ♯ ((ν*xvec)(N ≺' P)))"
and "x ♯ (τ ≺ P) = (x ♯ P)"
by(auto simp add: residualFresh)
lemma residualInject':
shows "(α ≺ P = RIn M N Q) = (P = Q ∧ α = M(N))"
and "(α ≺ P = ROut M B) = (∃xvec N. α = M(ν*xvec)⟨N⟩ ∧ B = (ν*xvec)(N ≺' P))"
and "(α ≺ P = RTau Q) = (α = τ ∧ P = Q)"
and "(RIn M N Q = α ≺ P) = (P = Q ∧ α = M(N))"
and "(ROut M B = α ≺ P) = (∃xvec N. α = M(ν*xvec)⟨N⟩ ∧ B = (ν*xvec)(N ≺' P))"
and "(RTau Q = α ≺ P) = (α = τ ∧ P = Q)"
proof -
show "(α ≺ P = RIn M N Q) = (P = Q ∧ α = M(N))"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
next
show "(α ≺ P = ROut M B) = (∃xvec N. α = M(ν*xvec)⟨N⟩ ∧ B = (ν*xvec)(N ≺' P))"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
next
show "(α ≺ P = RTau Q) = (α = τ ∧ P = Q)"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
next
show "(RIn M N Q = α ≺ P) = (P = Q ∧ α = M(N))"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
next
show "(ROut M B = α ≺ P) = (∃xvec N. α = M(ν*xvec)⟨N⟩ ∧ B = (ν*xvec)(N ≺' P))"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
next
show "(RTau Q = α ≺ P) = (α = τ ∧ P = Q)"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residual.inject action.inject)
qed
lemma residualFreshChainSimp[simp]:
fixes xvec :: "name list"
and X :: "name set"
and M :: "'a::fs_name"
and N :: 'a
and yvec :: "name list"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "xvec ♯* (M(N) ≺ P) = (xvec ♯* M ∧ xvec ♯* N ∧ xvec ♯* P)"
and "xvec ♯* (M(ν*yvec)⟨N⟩ ≺ P) = (xvec ♯* M ∧ xvec ♯* ((ν*yvec)(N ≺' P)))"
and "xvec ♯* (τ ≺ P) = (xvec ♯* P)"
and "X ♯* (M(N) ≺ P) = (X ♯* M ∧ X ♯* N ∧ X ♯* P)"
and "X ♯* (M(ν*yvec)⟨N⟩ ≺ P) = (X ♯* M ∧ X ♯* ((ν*yvec)(N ≺' P)))"
and "X ♯* (τ ≺ P) = (X ♯* P)"
by(auto simp add: fresh_star_def)
lemma residualFreshChainSimp2[simp]:
fixes xvec :: "name list"
and X :: "name set"
and M :: "'a::fs_name"
and N :: 'a
and yvec :: "name list"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
shows "xvec ♯* (RIn M N P) = (xvec ♯* M ∧ xvec ♯* N ∧ xvec ♯* P)"
and "xvec ♯* (ROut M B) = (xvec ♯* M ∧ xvec ♯* B)"
and "xvec ♯* (RTau P) = (xvec ♯* P)"
and "X ♯* (RIn M N P) = (X ♯* M ∧ X ♯* N ∧ X ♯* P)"
and "X ♯* (ROut M B) = (X ♯* M ∧ X ♯* B)"
and "X ♯* (RTau P) = (X ♯* P)"
by(auto simp add: fresh_star_def)
lemma freshResidual3[dest]:
fixes x :: name
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "x ♯ bn α"
and "x ♯ α ≺ P"
shows "x ♯ α" and "x ♯ P"
using assms
by(nominal_induct rule: action.strong_induct) auto
lemma freshResidualChain3[dest]:
fixes xvec :: "name list"
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "xvec ♯* (α ≺ P)"
and "xvec ♯* bn α"
shows "xvec ♯* α" and "xvec ♯* P"
using assms
by(nominal_induct rule: action.strong_induct) auto
lemma freshResidual4[dest]:
fixes x :: name
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "x ♯ α ≺ P"
shows "x ♯ subject α"
using assms
by(nominal_induct rule: action.strong_induct) auto
lemma freshResidualChain4[dest]:
fixes xvec :: "name list"
and α :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
assumes "xvec ♯* (α ≺ P)"
shows "xvec ♯* subject α"
using assms
by(nominal_induct rule: action.strong_induct) auto
lemma alphaOutputResidual:
fixes M :: "'a::fs_name"
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and p :: "name prm"
assumes "(p ∙ xvec) ♯* N"
and "(p ∙ xvec) ♯* P"
and "set p ⊆ set xvec × set(p ∙ xvec)"
and "set xvec ⊆ set yvec"
shows "M(ν*yvec)⟨N⟩ ≺ P = M(ν*(p ∙ yvec))⟨(p ∙ N)⟩ ≺ (p ∙ P)"
using assms
by(simp add: boundOutputChainAlpha'')
lemmas[simp del] = create_residual.simps
lemma residualInject'':
assumes "bn α = bn β"
shows "(α ≺ P = β ≺ Q) = (α = β ∧ P = Q)"
using assms
apply(nominal_induct α rule: action.strong_induct)
apply(auto simp add: residual.inject create_residual.simps residualInject' action.inject boundOutput.inject)
by(rule_tac x="bn β" in exI) auto
lemmas residualInject = residual.inject create_residual.simps residualInject' residualInject''
lemma bnFreshResidual[simp]:
fixes α :: "('a::fs_name) action"
shows "(bn α) ♯* (α ≺ P) = bn α ♯* (subject α)"
by(nominal_induct α rule: action.strong_induct)
(auto simp add: residualFresh fresh_some fresh_star_def)
lemma actionCases[case_names cInput cOutput cTau]:
fixes α :: "('a::fs_name) action"
assumes "∧M N. α = M(N) ==> Prop"
and "∧M xvec N. α = M(ν*xvec)⟨N⟩ ==> Prop"
and "α = τ ==> Prop"
shows Prop
using assms
by(nominal_induct \<alpha> rule: action.strong_induct) auto
lemma actionPar1Dest:
fixes \<alpha> :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and \<beta> :: "('a::fs_name) action"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "\<alpha> \<prec> P = \<beta> \<prec> (Q \<parallel> R)"
and "bn \<alpha> \<sharp>* bn \<beta>"
obtains T p where "set p \<subseteq> set(bn \<alpha>) \<times> set(bn \<beta>)" and "P = T \<parallel> (p \<bullet> R)" and "\<alpha> \<prec> T = \<beta> \<prec> Q"
using assms
apply(cases rule: actionCases[where \<alpha>=\<alpha>])
apply(auto simp add: residualInject)
by(drule_tac boundOutputPar1Dest') auto
lemma actionPar2Dest:
fixes \<alpha> :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
and \<beta> :: "('a::fs_name) action"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "\<alpha> \<prec> P = \<beta> \<prec> (Q \<parallel> R)"
and "bn \<alpha> \<sharp>* bn \<beta>"
obtains T p where "set p \<subseteq> set(bn \<alpha>) \<times> set(bn \<beta>)" and "P = (p \<bullet> Q) \<parallel> T" and "\<alpha> \<prec> T = \<beta> \<prec> R"
using assms
apply(cases rule: actionCases[where \<alpha>=\<alpha>])
apply(auto simp add: residualInject)
by(drule_tac boundOutputPar2Dest') auto
lemma actionScopeDest:
fixes \<alpha> :: "('a::fs_name) action"
and P :: "('a, 'b::fs_name, 'c::fs_name) psi"
fixes \<beta> :: "('a::fs_name) action"
and x :: name
and Q :: "('a, 'b, 'c) psi"
assumes "\<alpha> \<prec> P = \<beta> \<prec> \<lparr>\<nu>x\<rparr>Q"
and "x \<sharp> bn \<alpha>"
and "x \<sharp> bn \<beta>"
obtains R where "P = \<lparr>\<nu>x\<rparr>R" and "\<alpha> \<prec> R = \<beta> \<prec> Q"
using assms
apply(cases rule: actionCases[where \<alpha>=\<alpha>])
apply(auto simp add: residualInject)
by(drule_tac boundOutputScopeDest) auto
abbreviation
outputJudge (\<open>_\<langle>_\<rangle>\<close> [110, 110] 110) where "M\<langle>N\<rangle> \<equiv> M\<lparr>\<nu>*([])\<rparr>\<langle>N\<rangle>"
declare [[unify_trace_bound=100]]
locale env = substPsi substTerm substAssert substCond +
assertion SCompose' SImp' SBottom' SChanEq'
for substTerm :: "('a::fs_name) \<Rightarrow> name list \<Rightarrow> 'a::fs_name list \<Rightarrow> 'a"
and substAssert :: "('b::fs_name) \<Rightarrow> name list \<Rightarrow> 'a::fs_name list \<Rightarrow> 'b"
and substCond :: "('c::fs_name) \<Rightarrow> name list \<Rightarrow> 'a::fs_name list \<Rightarrow> 'c"
and SCompose' :: "'b \<Rightarrow> 'b \<Rightarrow> 'b"
and SImp' :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
and SBottom' :: 'b
and SChanEq' :: "'a \<Rightarrow> 'a \<Rightarrow> 'c"
begin
notation SCompose' (infixr \<open>\<otimes>\<close> 90)
notation SImp' (\<open>_ \<turnstile> _\<close> [85, 85] 85)
notation FrameImp (\<open>_ \<turnstile>\<^sub>F _\<close> [85, 85] 85)
abbreviation
FBottomJudge (\<open>\<bottom>\<^sub>F\<close> 90) where "\<bottom>\<^sub>F \<equiv> (FAssert SBottom')"
notation SChanEq' (\<open>_ \<leftrightarrow> _\<close> [90, 90] 90)
notation substTerm (\<open>_[_::=_]\<close> [100, 100, 100] 100)
notation subs (\<open>_[_::=_]\<close> [100, 100, 100] 100)
notation AssertionStatEq (\<open>_ \<simeq> _\<close> [80, 80] 80)
notation FrameStatEq (\<open>_ \<simeq>\<^sub>F _\<close> [80, 80] 80)
notation SBottom' (\<open>\<one>\<close> 190)
abbreviation insertAssertion' (\<open>insertAssertion\<close>) where "insertAssertion' \<equiv> assertionAux.insertAssertion (\<otimes>)"
inductive semantics :: "'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow> ('a, 'b, 'c) residual \<Rightarrow> bool"
(\<open>_ \<rhd> _ \<longmapsto> _\<close> [50, 50, 50] 50)
where
cInput: "\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K; distinct xvec; set xvec \<subseteq> supp N; xvec \<sharp>* Tvec;
length xvec = length Tvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* M; xvec \<sharp>* K\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> K\<lparr>(N[xvec::=Tvec])\<rparr> \<prec> P[xvec::=Tvec]"
| Output: "\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto> K\<langle>N\<rangle> \<prec> P"
| Case: "\<lbrakk>\<Psi> \<rhd> P \<longmapsto> Rs; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> Cases Cs \<longmapsto> Rs"
| cPar1: "\<lbrakk>(\<Psi> \<otimes> \<Psi>\<^sub>Q) \<rhd> P \<longmapsto>\<alpha> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* P'; distinct(bn \<alpha>);
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* (subject \<alpha>)\<rbrakk> \<Longrightarrow>
\<Psi> \<rhd> P \<parallel> Q \<longmapsto>\<alpha> \<prec> (P' \<parallel> Q)"
| cPar2: "\<lbrakk>(\<Psi> \<otimes> \<Psi>\<^sub>P) \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* Q'; distinct(bn \<alpha>);
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* (subject \<alpha>)\<rbrakk> \<Longrightarrow>
\<Psi> \<rhd> P \<parallel> Q \<longmapsto>\<alpha> \<prec> (P \<parallel> Q')"
| cComm1: "\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto> M\<lparr>N\<rparr> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto> K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec;
A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P; A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P';
A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q'; A\<^sub>Q \<sharp>* xvec; distinct xvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K\<rbrakk> \<Longrightarrow>
\<Psi> \<rhd> P \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')"
| cComm2: "\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto> K\<lparr>N\<rparr> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec;
A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P; A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P';
A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q'; A\<^sub>Q \<sharp>* xvec; distinct xvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K\<rbrakk> \<Longrightarrow>
\<Psi> \<rhd> P \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')"
| cOpen: "\<lbrakk>\<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; x \<in> supp N; x \<sharp> xvec; x \<sharp> yvec; x \<sharp> M; x \<sharp> \<Psi>;
distinct xvec; distinct yvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* yvec; yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M\<rbrakk> \<Longrightarrow>
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<longmapsto> M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P'"
| cScope: "\<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; x \<sharp> \<Psi>; x \<sharp> \<alpha>; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* (subject \<alpha>); distinct(bn \<alpha>)\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<longmapsto>\<alpha> \<prec> (\<lparr>\<nu>x\<rparr>P')"
| Bang: "\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto> Rs; guarded P\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> !P \<longmapsto> Rs"
abbreviation
semanticsBottomJudge (\<open>_ \<longmapsto> _\<close> [50, 50] 50) where "P \<longmapsto> Rs \<equiv> \<one> \<rhd> P \<longmapsto> Rs"
equivariance env.semantics
nominal_inductive2 env.semantics
avoids cInput: "set xvec"
| cPar1: "set A\<^sub>Q \<union> set(bn \<alpha>)"
| cPar2: "set A\<^sub>P \<union> set(bn \<alpha>)"
| cComm1: "set A\<^sub>P \<union> set A\<^sub>Q \<union> set xvec"
| cComm2: "set A\<^sub>P \<union> set A\<^sub>Q \<union> set xvec"
| cOpen: "{x} \<union> set xvec \<union> set yvec"
| cScope: "{x} \<union> set(bn \<alpha>)"
apply(auto intro: substTerm.subst4Chain subst4Chain simp add: abs_fresh residualFresh)
apply(force simp add: fresh_star_def abs_fresh)
apply(simp add: boundOutputFresh)
apply(simp add: boundOutputFreshSet)
apply(simp add: boundOutputFreshSet)
by(simp add: fresh_star_def abs_fresh)
lemma nilTrans[dest]:
fixes \<Psi> :: 'b
and Rs :: "('a, 'b, 'c) residual"
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
and K :: 'a
and yvec :: "name list"
and N' :: 'a
and P' :: "('a, 'b, 'c) psi"
and CsP :: "('c \<times> ('a, 'b, 'c) psi) list"
and \<Psi>' :: 'b
shows "\<Psi> \<rhd> \<zero> \<longmapsto> Rs \<Longrightarrow> False"
and "\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto>K\<lparr>\<nu>*yvec\<rparr>\<langle>N'\<rangle> \<prec> P' \<Longrightarrow> False"
and "\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto>\<tau> \<prec> P' \<Longrightarrow> False"
and "\<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto>K\<lparr>N'\<rparr> \<prec> P' \<Longrightarrow> False"
and "\<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto>\<tau> \<prec> P' \<Longrightarrow> False"
and "\<Psi> \<rhd> \<lbrace>\<Psi>'\<rbrace> \<longmapsto> Rs \<Longrightarrow> False"
apply(cases rule: semantics.cases) apply auto
apply(cases rule: semantics.cases) apply(auto simp add: residualInject)
apply(cases rule: semantics.cases) apply(auto simp add: residualInject)
apply(cases rule: semantics.cases) apply(auto simp add: residualInject)
apply(cases rule: semantics.cases) apply(auto simp add: residualInject)
by(cases rule: semantics.cases) (auto simp add: residualInject)
lemma residualEq:
fixes \<alpha> :: "'a action"
and P :: "('a, 'b, 'c) psi"
and \<beta> :: "'a action"
and Q :: "('a, 'b, 'c) psi"
assumes "\<alpha> \<prec> P = \<beta> \<prec> Q"
and "bn \<alpha> \<sharp>* (bn \<beta>)"
and "distinct(bn \<alpha>)"
and "distinct(bn \<beta>)"
and "bn \<alpha> \<sharp>* (\<alpha> \<prec> P)"
and "bn \<beta> \<sharp>* (\<beta> \<prec> Q)"
obtains p where "set p \<subseteq> set(bn \<alpha>) \<times> set(bn(p \<bullet> \<alpha>))" and "distinctPerm p" and "\<beta> = p \<bullet> \<alpha>" and "Q = p \<bullet> P" and "bn \<alpha> \<sharp>* \<beta>" and "bn \<alpha> \<sharp>* Q" and "bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>" and "bn(p \<bullet> \<alpha>) \<sharp>* P"
using assms
proof(nominal_induct \<alpha> rule: action.strong_induct)
case(In M N)
thus ?case by(simp add: residualInject)
next
case(Out M xvec N)
thus ?case
by(auto simp add: residualInject)
(drule_tac boundOutputChainEq'', auto)
next
case Tau
thus ?case by(simp add: residualInject)
qed
lemma semanticsInduct[consumes 3, case_names cAlpha cInput cOutput cCase cPar1 cPar2 cComm1 cComm2 cOpen cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and \<alpha> :: "'a action"
and P' :: "('a, 'b, 'c) psi"
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
'a action \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
and "bn \<alpha> \<sharp>* (subject \<alpha>)"
and "distinct(bn \<alpha>)"
and rAlpha: "\<And>\<Psi> P \<alpha> P' p C. \<lbrakk>bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* (subject \<alpha>);
bn \<alpha> \<sharp>* C; bn \<alpha> \<sharp>* (bn(p \<bullet> \<alpha>));
set p \<subseteq> set(bn \<alpha>) \<times> set(bn(p \<bullet> \<alpha>)); distinctPerm p;
(bn(p \<bullet> \<alpha>)) \<sharp>* \<alpha>; (bn(p \<bullet> \<alpha>)) \<sharp>* P'; Prop C \<Psi> P \<alpha> P'\<rbrakk> \<Longrightarrow>
Prop C \<Psi> P (p \<bullet> \<alpha>) (p \<bullet> P')"
and rInput: "\<And>\<Psi> M K xvec N Tvec P C.
\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K; distinct xvec; set xvec \<subseteq> supp N;
length xvec = length Tvec; xvec \<sharp>* \<Psi>;
xvec \<sharp>* M; xvec \<sharp>* K; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (M\<lparr>\<lambda>*xvec N\<rparr>.P)
(K\<lparr>(N[xvec::=Tvec])\<rparr>) (P[xvec::=Tvec])"
and rOutput: "\<And>\<Psi> M K N P C. \<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K\<rbrakk> \<Longrightarrow> Prop C \<Psi> (M\<langle>N\<rangle>.P) (K\<langle>N\<rangle>) P"
and rCase: "\<And>\<Psi> P \<alpha> P' \<phi> Cs C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; \<And>C. Prop C \<Psi> P \<alpha> P'; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (Cases Cs) \<alpha> P'"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P \<alpha> P' A\<^sub>Q Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<alpha> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P \<alpha> P';
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* C; distinct(bn \<alpha>); bn \<alpha> \<sharp>* Q;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) \<alpha> (P' \<parallel> Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q \<alpha> Q' A\<^sub>P P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q \<alpha> Q';
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* C; distinct(bn \<alpha>); bn \<alpha> \<sharp>* Q;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) \<alpha> (P \<parallel> Q')"
and rComm1: "\<And>\<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; \<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (M\<lparr>N\<rparr>) P';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; \<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) Q';
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q'; distinct xvec;
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
and rComm2: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; \<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) P';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'; \<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>N\<rparr>) Q';
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q'; distinct xvec;
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
and rOpen: "\<And>\<Psi> P M xvec yvec N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; x \<in> supp N; \<And>C. Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle>) P';
x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> xvec; x \<sharp> yvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; distinct xvec; distinct yvec;
yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; yvec \<sharp>* C; x \<sharp> C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) P'"
and rScope: "\<And>\<Psi> P \<alpha> P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; \<And>C. Prop C \<Psi> P \<alpha> P';
x \<sharp> \<Psi>; x \<sharp> \<alpha>; bn \<alpha> \<sharp>* \<Psi>;
bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* (subject \<alpha>); x \<sharp> C; bn \<alpha> \<sharp>* C; distinct(bn \<alpha>)\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) \<alpha> (\<lparr>\<nu>x\<rparr>P')"
and rBang: "\<And>\<Psi> P \<alpha> P' C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>\<alpha> \<prec> P'; guarded P; \<And>C. Prop C \<Psi> (P \<parallel> !P) \<alpha> P'\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (!P) \<alpha> P'"
shows "Prop C \<Psi> P \<alpha> P'"
using \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> \<open>bn \<alpha> \<sharp>* (subject \<alpha>)\<close> \<open>distinct(bn \<alpha>)\<close>
proof(nominal_induct x3=="\<alpha> \<prec> P'" avoiding: \<alpha> C arbitrary: P' rule: semantics.strong_induct)
case(cInput \<Psi> M K xvec N Tvec P \<alpha> C P')
thus ?case by(force intro: rInput simp add: residualInject)
next
case(Output \<Psi> M K N P \<alpha> C P')
thus ?case by(force intro: rOutput simp add: residualInject)
next
case(Case \<Psi> P Rs \<phi> Cs \<alpha> C)
thus ?case by(auto intro: rCase)
next
case(cPar1 \<Psi> \<Psi>\<^sub>Q P \<alpha> P' Q A\<^sub>Q \<alpha>' C P'')
note \<open>\<alpha> \<prec> (P' \<parallel> Q) = \<alpha>' \<prec> P''\<close>
moreover from \<open>bn \<alpha> \<sharp>* \<alpha>'\<close> have "bn \<alpha> \<sharp>* (bn \<alpha>')" by auto
moreover note \<open>distinct (bn \<alpha>)\<close> \<open>distinct(bn \<alpha>')\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha>' \<sharp>* subject \<alpha>'\<close>
have "bn \<alpha> \<sharp>* (\<alpha> \<prec> P' \<parallel> Q)" and "bn \<alpha>' \<sharp>* (\<alpha>' \<prec> P'')" by simp+
ultimately obtain p where S: "(set p) \<subseteq> (set(bn \<alpha>)) \<times> (set(bn(p \<bullet> \<alpha>)))" and "distinctPerm p"
and \<alpha>Eq: "\<alpha>' = p \<bullet> \<alpha>" and P'eq: "P'' = p \<bullet> (P' \<parallel> Q)" and "(bn(p \<bullet> \<alpha>)) \<sharp>* \<alpha>"
and "(bn(p \<bullet> \<alpha>)) \<sharp>* (P' \<parallel> Q)"
by(rule residualEq)
note \<open>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> \<open>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> \<open>distinct A\<^sub>Q\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close>
have "\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P \<alpha> P'" by(rule_tac cPar1) auto
moreover note \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* P'\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
\<open>bn \<alpha> \<sharp>* Q\<close> \<open>distinct(bn \<alpha>)\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>Q\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) \<alpha> (P' \<parallel> Q)"
by(rule_tac rPar1)
with \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* bn \<alpha>'\<close> S \<open>distinctPerm p\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* (P' \<parallel> Q)\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
have "Prop C \<Psi> (P \<parallel> Q) (p \<bullet> \<alpha>) (p \<bullet> (P' \<parallel> Q))"
by(rule_tac rAlpha) auto
with \<alpha>Eq P'eq \<open>distinctPerm p\<close> show ?case by simp
next
case(cPar2 \<Psi> \<Psi>\<^sub>P Q \<alpha> Q' P A\<^sub>P \<alpha>' C Q'')
note \<open>\<alpha> \<prec> (P \<parallel> Q') = \<alpha>' \<prec> Q''\<close>
moreover from \<open>bn \<alpha> \<sharp>* \<alpha>'\<close> have "bn \<alpha> \<sharp>* (bn \<alpha>')" by auto
moreover note \<open>distinct (bn \<alpha>)\<close> \<open>distinct(bn \<alpha>')\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha>' \<sharp>* subject \<alpha>'\<close>
have "bn \<alpha> \<sharp>* (\<alpha> \<prec> P \<parallel> Q')" and "bn \<alpha>' \<sharp>* (\<alpha>' \<prec> Q'')" by simp+
ultimately obtain p where S: "(set p) \<subseteq> (set(bn \<alpha>)) \<times> (set(bn(p \<bullet> \<alpha>)))" and "distinctPerm p"
and \<alpha>Eq: "\<alpha>' = p \<bullet> \<alpha>" and Q'eq: "Q'' = p \<bullet> (P \<parallel> Q')" and "(bn(p \<bullet> \<alpha>)) \<sharp>* \<alpha>"
and "(bn(p \<bullet> \<alpha>)) \<sharp>* (P \<parallel> Q')"
by(rule residualEq)
note \<open>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close> \<open>distinct A\<^sub>P\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close>
have "\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q \<alpha> Q'" by(rule_tac cPar2) auto
moreover note \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* Q'\<close> \<open>A\<^sub>P \<sharp>* C\<close>
\<open>bn \<alpha> \<sharp>* Q\<close> \<open>distinct(bn \<alpha>)\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>P\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) \<alpha> (P \<parallel> Q')"
by(rule_tac rPar2)
with \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* (bn \<alpha>')\<close> S \<open>distinctPerm p\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* (P \<parallel> Q')\<close>
have "Prop C \<Psi> (P \<parallel> Q) (p \<bullet> \<alpha>) (p \<bullet> (P \<parallel> Q'))"
by(rule_tac rAlpha) auto
with \<alpha>Eq Q'eq \<open>distinctPerm p\<close> show ?case by simp
next
case(cComm1 \<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q \<alpha> C P'')
hence "Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
by(rule_tac rComm1) (assumption | simp)+
thus ?case using \<open>\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q') = \<alpha> \<prec> P''\<close>
by(simp add: residualInject)
next
case(cComm2 \<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q \<alpha> C P'')
hence "Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
by(rule_tac rComm2) (assumption | simp)+
thus ?case using \<open>\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q') = \<alpha> \<prec> P''\<close>
by(simp add: residualInject)
next
case(cOpen \<Psi> P M xvec yvec N P' x \<alpha> C P'')
note \<open>M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P' = \<alpha> \<prec> P''\<close>
moreover from \<open>xvec \<sharp>* \<alpha>\<close> \<open>x \<sharp> \<alpha>\<close> \<open>yvec \<sharp>* \<alpha>\<close> have "(xvec@x#yvec) \<sharp>* (bn \<alpha>)"
by auto
moreover from \<open>xvec \<sharp>* yvec\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> \<open>distinct xvec\<close> \<open>distinct yvec\<close>
have "distinct(xvec@x#yvec)"
by(auto simp add: fresh_star_def) (simp add: fresh_def name_list_supp)
moreover note \<open>distinct(bn \<alpha>)\<close>
moreover from \<open>xvec \<sharp>* M\<close> \<open>x \<sharp> M\<close> \<open>yvec \<sharp>* M\<close> have "(xvec@x#yvec) \<sharp>* M" by auto
hence "(xvec@x#yvec) \<sharp>* (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P')" by auto
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> have "bn \<alpha> \<sharp>* (\<alpha> \<prec> P'')" by simp
ultimately obtain p where S: "(set p) \<subseteq> (set(xvec@x#yvec)) \<times> (set(p \<bullet> (xvec@x#yvec)))" and "distinctPerm p"
and \<alpha>eq: "\<alpha> = (p \<bullet> M)\<lparr>\<nu>*(p \<bullet> (xvec@x#yvec))\<rparr>\<langle>(p \<bullet> N)\<rangle>" and P'eq: "P'' = (p \<bullet> P')"
and A: "(xvec@x#yvec) \<sharp>* ((p \<bullet> M)\<lparr>\<nu>*(p \<bullet> (xvec@x#yvec))\<rparr>\<langle>(p \<bullet> N)\<rangle>)"
and B: "(p \<bullet> (xvec@x#yvec)) \<sharp>* (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>)"
and C: "(p \<bullet> (xvec@x#yvec)) \<sharp>* P'"
by(rule_tac residualEq) (assumption | simp)+
note \<open>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'\<close> \<open>x \<in> (supp N)\<close>
moreover {
fix C
from \<open>xvec \<sharp>* M\<close> \<open>yvec \<sharp>* M\<close> have "(xvec@yvec) \<sharp>* M" by simp
moreover from \<open>distinct xvec\<close> \<open>distinct yvec\<close> \<open>xvec \<sharp>* yvec\<close> have "distinct(xvec@yvec)"
by auto (simp add: fresh_star_def name_list_supp fresh_def)
ultimately have "Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle>) P'" by(rule_tac cOpen) auto
}
moreover note \<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* M\<close>
\<open>yvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P\<close> \<open>yvec \<sharp>* M\<close> \<open>yvec \<sharp>* C\<close> \<open>x \<sharp> C\<close> \<open>xvec \<sharp>* C\<close> \<open>distinct xvec\<close> \<open>distinct yvec\<close>
ultimately have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) P'"
by(rule_tac rOpen)
with \<open>xvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>yvec \<sharp>* P\<close> \<open>xvec \<sharp>* M\<close> \<open>yvec \<sharp>* M\<close>
\<open>yvec \<sharp>* C\<close> S \<open>distinctPerm p\<close> \<open>x \<sharp> C\<close> \<open>xvec \<sharp>* C\<close>
\<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> A B C
have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (p \<bullet> (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>)) (p \<bullet> P')"
apply(rule_tac \<alpha>="M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>" in rAlpha)
apply(assumption | simp)+
apply(fastforce simp add: fresh_star_def abs_fresh)
by(assumption | simp)+
with \<alpha>eq P'eq show ?case by simp
next
case(cScope \<Psi> P \<alpha> P' x \<alpha>' C P'')
note \<open>\<alpha> \<prec> (\<lparr>\<nu>x\<rparr>P') = \<alpha>' \<prec> P''\<close>
moreover from \<open>bn \<alpha> \<sharp>* \<alpha>'\<close> have "bn \<alpha> \<sharp>* (bn \<alpha>')" by auto
moreover note \<open>distinct (bn \<alpha>)\<close> \<open>distinct(bn \<alpha>')\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha>' \<sharp>* subject \<alpha>'\<close>
have "bn \<alpha> \<sharp>* (\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P')" and "bn \<alpha>' \<sharp>* (\<alpha>' \<prec> P'')" by simp+
ultimately obtain p where S: "(set p) \<subseteq> (set(bn \<alpha>)) \<times> (set(bn(p \<bullet> \<alpha>)))" and "distinctPerm p"
and \<alpha>Eq: "\<alpha>' = p \<bullet> \<alpha>" and P'eq: "P'' = p \<bullet> (\<lparr>\<nu>x\<rparr>P')" and "(bn(p \<bullet> \<alpha>)) \<sharp>* \<alpha>"
and "(bn(p \<bullet> \<alpha>)) \<sharp>* (\<lparr>\<nu>x\<rparr>P')"
by(rule residualEq)
note \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close>
moreover from \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close>
have "\<And>C. Prop C \<Psi> P \<alpha> P'" by(rule_tac cScope) auto
moreover note \<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> \<alpha>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close>
\<open>x \<sharp> C\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>distinct(bn \<alpha>)\<close>
ultimately have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) \<alpha> (\<lparr>\<nu>x\<rparr>P')"
by(rule rScope)
with \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>x \<sharp> \<alpha>\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* (bn \<alpha>')\<close> S \<open>distinctPerm p\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* (\<lparr>\<nu>x\<rparr>P')\<close>
have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (p \<bullet> \<alpha>) (p \<bullet> (\<lparr>\<nu>x\<rparr>P'))"
by(rule_tac rAlpha) simp+
with \<alpha>Eq P'eq \<open>distinctPerm p\<close> show ?case by simp
next
case(Bang \<Psi> P Rs \<alpha> C)
thus ?case by(rule_tac rBang) auto
qed
lemma outputInduct[consumes 1, case_names cOutput cCase cPar1 cPar2 cOpen cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and B :: "('a, 'b, 'c) boundOutput"
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
'a \<Rightarrow> ('a, 'b, 'c) boundOutput \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes "\<Psi> \<rhd> P \<longmapsto>ROut M B"
and rOutput: "\<And>\<Psi> M K N P C. \<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K\<rbrakk> \<Longrightarrow> Prop C \<Psi> (M\<langle>N\<rangle>.P) K (N \<prec>' P)"
and rCase: "\<And>\<Psi> P M B \<phi> Cs C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>(ROut M B); \<And>C. Prop C \<Psi> P M B; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (Cases Cs) M B"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>Q Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' P');
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* M;
A\<^sub>Q \<sharp>* xvec; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* C; xvec \<sharp>* Q;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' (P' \<parallel> Q))"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q M xvec N Q' A\<^sub>P P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' Q');
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* M;
A\<^sub>P \<sharp>* xvec; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* C; xvec \<sharp>* P;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* Q; xvec \<sharp>* M; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' (P \<parallel> Q'))"
and rOpen: "\<And>\<Psi> P M xvec yvec N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; x \<in> supp N; \<And>C. Prop C \<Psi> P M (\<lparr>\<nu>*(xvec@yvec)\<rparr>N \<prec>' P');
x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> xvec; x \<sharp> yvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* yvec; yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; yvec \<sharp>* C; x \<sharp> C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) M (\<lparr>\<nu>*(xvec@x#yvec)\<rparr>N \<prec>' P')"
and rScope: "\<And>\<Psi> P M xvec N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; \<And>C. Prop C \<Psi> P M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' P');
x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> xvec; x \<sharp> N; xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M;
x \<sharp> C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' \<lparr>\<nu>x\<rparr>P')"
and rBang: "\<And>\<Psi> P M B C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>(ROut M B); guarded P; \<And>C. Prop C \<Psi> (P \<parallel> !P) M B\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (!P) M B"
shows "Prop C \<Psi> P M B"
using \<open>\<Psi> \<rhd> P \<longmapsto>(ROut M B)\<close>
proof(nominal_induct \<Psi> P Rs=="(ROut M B)" avoiding: C arbitrary: B rule: semantics.strong_induct)
case(cInput \<Psi> M K xvec N Tvec P C)
thus ?case by(simp add: residualInject)
next
case(Output \<Psi> M K N P C)
thus ?case by(force simp add: residualInject intro: rOutput)
next
case(Case \<Psi> P Rs \<phi> Cs C)
thus ?case by(force intro: rCase)
next
case(cPar1 \<Psi> \<Psi>\<^sub>Q P \<alpha> P' Q A\<^sub>Q C)
thus ?case by(force intro: rPar1 simp add: residualInject)
next
case(cPar2 \<Psi> \<Psi>\<^sub>P Q \<alpha> Q' P A\<^sub>P C)
thus ?case by(force intro: rPar2 simp add: residualInject)
next
case cComm1
thus ?case by(simp add: residualInject)
next
case cComm2
thus ?case by(simp add: residualInject)
next
case(cOpen \<Psi> P M xvec yvec N P' x C B)
thus ?case by(force intro: rOpen simp add: residualInject)
next
case(cScope \<Psi> P M \<alpha> P' x C)
thus ?case by(force intro: rScope simp add: residualInject)
next
case(Bang \<Psi> P Rs C)
thus ?case by(force intro: rBang)
qed
lemma boundOutputBindObject:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and yvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and y :: name
assumes "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
and "bn \<alpha> \<sharp>* subject \<alpha>"
and "distinct(bn \<alpha>)"
and "y \<in> set(bn \<alpha>)"
shows "y \<in> supp(object \<alpha>)"
using assms
proof(nominal_induct avoiding: P' arbitrary: y rule: semanticsInduct)
case(cAlpha \<Psi> P \<alpha> P' p P'' y)
from \<open>y \<in> set(bn(p \<bullet> \<alpha>))\<close> have "(p \<bullet> y) \<in> (p \<bullet> set(bn(p \<bullet> \<alpha>)))"
by(rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
hence "(p \<bullet> y) \<in> set(bn \<alpha>)" using \<open>distinctPerm p\<close>
by(simp add: eqvts)
hence "(p \<bullet> y) \<in> supp(object \<alpha>)" by(rule cAlpha)
hence "(p \<bullet> p \<bullet> y) \<in> (p \<bullet> supp(object \<alpha>))"
by(rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
thus ?case using \<open>distinctPerm p\<close>
by(simp add: eqvts)
next
case cInput
thus ?case by(simp add: supp_list_nil)
next
case cOutput
thus ?case by(simp add: supp_list_nil)
next
case cCase
thus ?case by simp
next
case cPar1
thus ?case by simp
next
case cPar2
thus ?case by simp
next
case cComm1
thus ?case by(simp add: supp_list_nil)
next
case cComm2
thus ?case by(simp add: supp_list_nil)
next
case cOpen
thus ?case by(auto simp add: supp_list_cons supp_list_append supp_atm supp_some)
next
case cScope
thus ?case by simp
next
case cBang
thus ?case by simp
qed
lemma alphaBoundOutputChain':
fixes yvec :: "name list"
and xvec :: "name list"
and B :: "('a, 'b, 'c) boundOutput"
assumes "length xvec = length yvec"
and "yvec \<sharp>* B"
and "yvec \<sharp>* xvec"
and "distinct yvec"
shows "\<lparr>\<nu>*xvec\<rparr>B = \<lparr>\<nu>*yvec\<rparr>([xvec yvec] \<bullet>\<^sub>v B)"
using assms
proof(induct rule: composePermInduct)
case cBase
show ?case by simp
next
case(cStep x xvec y yvec)
thus ?case
apply auto
by(subst alphaBoundOutput[of y]) (auto simp add: eqvts)
qed
lemma alphaBoundOutputChain'':
fixes yvec :: "name list"
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "length xvec = length yvec"
and "yvec \<sharp>* N"
and "yvec \<sharp>* P"
and "yvec \<sharp>* xvec"
and "distinct yvec"
shows "\<lparr>\<nu>*xvec\<rparr>(N \<prec>' P) = \<lparr>\<nu>*yvec\<rparr>(([xvec yvec] \<bullet>\<^sub>v N) \<prec>' ([xvec yvec] \<bullet>\<^sub>v P))"
proof -
from assms have "\<lparr>\<nu>*xvec\<rparr>(N \<prec>' P) = \<lparr>\<nu>*yvec\<rparr>([xvec yvec] \<bullet>\<^sub>v (N \<prec>' P))"
by(simp add: alphaBoundOutputChain')
thus ?thesis by simp
qed
lemma alphaDistinct:
fixes xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
and yvec :: "name list"
and M :: 'a
and Q :: "('a, 'b, 'c) psi"
assumes "\<alpha> \<prec> P = \<beta> \<prec> Q"
and "distinct(bn \<alpha>)"
and "\<And>x. x \<in> set(bn \<alpha>) \<Longrightarrow> x \<in> supp(object \<alpha>)"
and "bn \<alpha> \<sharp>* bn \<beta>"
and "bn \<alpha> \<sharp>* (object \<beta>)"
and "bn \<alpha> \<sharp>* Q"
shows "distinct(bn \<beta>)"
using assms
proof(rule_tac actionCases[where \<alpha>=\<alpha>], auto simp add: residualInject supp_some)
fix xvec M yvec N
assume Eq: "\<lparr>\<nu>*xvec\<rparr>N \<prec>' P = \<lparr>\<nu>*yvec\<rparr>M \<prec>' Q"
assume "distinct xvec" and "xvec \<sharp>* M" and "xvec \<sharp>* yvec" and "xvec \<sharp>* Q"
assume Mem: "\<And>x. x \<in> set xvec \<Longrightarrow> x \<in> (supp N)"
show "distinct yvec"
proof -
from Eq have "length xvec = length yvec"
by(rule boundOutputChainEqLength)
with Eq \<open>distinct xvec\<close> \<open>xvec \<sharp>* yvec\<close> \<open>xvec \<sharp>* M\<close> \<open>xvec \<sharp>* Q\<close> Mem show ?thesis
proof(induct n=="length xvec" arbitrary: xvec yvec M Q rule: nat.induct)
case(zero xvec yvec M Q)
thus ?case by simp
next
case(Suc n xvec yvec M Q)
have L: "length xvec = length yvec" and "Suc n = length xvec" by fact+
then obtain x xvec' y yvec' where xEq: "xvec = x#xvec'" and yEq: "yvec = y#yvec'"
and L': "length xvec' = length yvec'"
by(cases xvec, auto, cases yvec, auto)
have xvecFreshyvec: "xvec \<sharp>* yvec" and xvecDist: "distinct xvec" by fact+
with xEq yEq have xineqy: "x \<noteq> y" and xvec'Freshyvec': "xvec' \<sharp>* yvec'"
and xvec'Dist: "distinct xvec'" and xFreshxvec': "x \<sharp> xvec'"
and xFreshyvec': "x \<sharp> yvec'" and yFreshxvec': "y \<sharp> xvec'"
by auto
have Eq: "\<lparr>\<nu>*xvec\<rparr>N \<prec>' P = \<lparr>\<nu>*yvec\<rparr>M \<prec>' Q" by fact
with xEq yEq xineqy have Eq': "\<lparr>\<nu>*xvec'\<rparr>N \<prec>' P = \<lparr>\<nu>*([(x, y)] \<bullet> yvec')\<rparr>([(x, y)] \<bullet> M) \<prec>' ([(x, y)] \<bullet> Q)"
by(simp add: boundOutput.inject alpha eqvts)
moreover have Mem:"\<And>x. x \<in> set xvec \<Longrightarrow> x \<in> supp N" by fact
with xEq have "\<And>x. x \<in> set xvec' \<Longrightarrow> x \<in> supp N" by simp
moreover have "xvec \<sharp>* M" by fact
with xEq xFreshxvec' yFreshxvec' have "xvec' \<sharp>* ([(x, y)] \<bullet> M)" by simp
moreover have xvecFreshQ: "xvec \<sharp>* Q" by fact
with xEq xFreshxvec' yFreshxvec' have "xvec' \<sharp>* ([(x, y)] \<bullet> Q)" by simp
moreover have "Suc n = length xvec" by fact
with xEq have "n = length xvec'" by simp
moreover from xvec'Freshyvec' xFreshxvec' yFreshxvec' have "xvec' \<sharp>* ([(x, y)] \<bullet> yvec')"
by simp
moreover from L' have "length xvec' = length([(x, y)] \<bullet> yvec')" by simp
ultimately have "distinct([(x, y)] \<bullet> yvec')" using xvec'Dist
by(rule_tac Suc) (assumption | simp)+
hence "distinct yvec'" by simp
from Mem xEq have xSuppN: "x \<in> supp N" by simp
from L \<open>distinct xvec\<close> \<open>xvec \<sharp>* yvec\<close> \<open>xvec \<sharp>* M\<close> \<open>xvec \<sharp>* Q\<close>
have "\<lparr>\<nu>*yvec\<rparr>M \<prec>' Q = \<lparr>\<nu>*xvec\<rparr>([yvec xvec] \<bullet>\<^sub>v M) \<prec>' ([yvec xvec] \<bullet>\<^sub>v Q)"
by(simp add: alphaBoundOutputChain'')
with Eq have "N = [yvec xvec] \<bullet>\<^sub>v M" by simp
with xEq yEq have "N = [(y, x)] \<bullet> [yvec' xvec'] \<bullet>\<^sub>v M"
by simp
with xSuppN have ySuppM: "y \<in> supp([yvec' xvec'] \<bullet>\<^sub>v M)"
by(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
(simp add: calc_atm eqvts name_swap)
have "y \<sharp> yvec'"
proof(simp add: fresh_def, rule notI)
assume "y \<in> supp yvec'"
hence "y mem yvec'"
by(induct yvec') (auto simp add: supp_list_nil supp_list_cons supp_atm)
moreover from \<open>xvec \<sharp>* M\<close> xEq xFreshxvec' have "xvec' \<sharp>* M" by simp
ultimately have "y \<sharp> [yvec' xvec'] \<bullet>\<^sub>v M" using L' xvec'Freshyvec' xvec'Dist
by(force intro: freshChainPerm)
with ySuppM show "False" by(simp add: fresh_def)
qed
with \<open>distinct yvec'\<close> yEq show ?case by simp
qed
qed
qed
lemma boundOutputDistinct:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and \<alpha> :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
shows "distinct(bn \<alpha>)"
using assms
proof(nominal_induct \<Psi> P x3=="\<alpha> \<prec> P'" avoiding: \<alpha> P' rule: semantics.strong_induct)
case cInput
thus ?case by(simp add: residualInject)
next
case Output
thus ?case by(simp add: residualInject)
next
case Case
thus ?case by(simp add: residualInject)
next
case cPar1
thus ?case by(force intro: alphaDistinct boundOutputBindObject)
next
case cPar2
thus ?case by(force intro: alphaDistinct boundOutputBindObject)
next
case cComm1
thus ?case by(simp add: residualInject)
next
case cComm2
thus ?case by(simp add: residualInject)
next
case(cOpen \<Psi> P M xvec yvec N P' x \<alpha> P'')
note \<open>M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P' = \<alpha> \<prec> P''\<close>
moreover from \<open>xvec \<sharp>* yvec\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> \<open>distinct xvec\<close> \<open>distinct yvec\<close>
have "distinct(bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>))"
by auto (simp add: fresh_star_def fresh_def name_list_supp)
moreover {
fix y
from \<open>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'\<close> \<open>x \<in> supp N\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> \<Psi>\<close> \<open>distinct xvec\<close> \<open>distinct yvec\<close> \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* M\<close> \<open>xvec \<sharp>* yvec\<close> \<open>yvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P\<close> \<open>yvec \<sharp>* M\<close>
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<longmapsto>M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P'" by(rule semantics.cOpen)
moreover moreover from \<open>xvec \<sharp>* M\<close> \<open>x \<sharp> M\<close> \<open>yvec \<sharp>* M\<close>
have "bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) \<sharp>* (subject(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>))"
by simp
moreover note \<open>distinct(bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>))\<close>
moreover assume "y \<in> set(bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>))"
ultimately have "y \<in> supp(object(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>))"
by(rule_tac boundOutputBindObject)
}
moreover from \<open>xvec \<sharp>* \<alpha>\<close> \<open>x \<sharp> \<alpha>\<close> \<open>yvec \<sharp>* \<alpha>\<close>
have "bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) \<sharp>* bn \<alpha>" and "bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) \<sharp>* object \<alpha>" by simp+
moreover from \<open>xvec \<sharp>* P''\<close> \<open>x \<sharp> P''\<close> \<open>yvec \<sharp>* P''\<close>
have "bn(M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle>) \<sharp>* P''" by simp
ultimately show ?case by(rule alphaDistinct)
next
case cScope
thus ?case
by(rule_tac alphaDistinct, auto) (rule_tac boundOutputBindObject, auto)
next
case Bang
thus ?case by simp
qed
lemma inputDistinct:
fixes \<Psi> :: 'b
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
and Rs :: "('a, 'b, 'c) residual"
assumes "\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> Rs"
shows "distinct xvec"
using assms
by(nominal_induct \<Psi> P=="M\<lparr>\<lambda>*xvec N\<rparr>.P" Rs avoiding: xvec N P rule: semantics.strong_induct)
(auto simp add: psi.inject intro: alphaInputDistinct)
lemma outputInduct'[consumes 2, case_names cAlpha cOutput cCase cPar1 cPar2 cOpen cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and yvec :: "name list"
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
'a \<Rightarrow> name list \<Rightarrow> 'a \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes "\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
and "xvec \<sharp>* M"
and rAlpha: "\<And>\<Psi> P M xvec N P' p C. \<lbrakk>xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* C; xvec \<sharp>* (p \<bullet> xvec);
set p \<subseteq> set xvec \<times> set(p \<bullet> xvec); distinctPerm p;
(p \<bullet> xvec) \<sharp>* N; (p \<bullet> xvec) \<sharp>* P'; Prop C \<Psi> P M xvec N P'\<rbrakk> \<Longrightarrow>
Prop C \<Psi> P M (p \<bullet> xvec) (p \<bullet> N) (p \<bullet> P')"
and rOutput: "\<And>\<Psi> M K N P C. \<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K\<rbrakk> \<Longrightarrow> Prop C \<Psi> (M\<langle>N\<rangle>.P) K ([]) N P"
and rCase: "\<And>\<Psi> P M xvec N P' \<phi> Cs C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; \<And>C. Prop C \<Psi> P M xvec N P'; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (Cases Cs) M xvec N P'"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>Q Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P M xvec N P';
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* M;
A\<^sub>Q \<sharp>* xvec; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* C; xvec \<sharp>* Q;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M xvec N (P' \<parallel> Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q M xvec N Q' A\<^sub>P P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q M xvec N Q';
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* M;
A\<^sub>P \<sharp>* xvec; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* C; xvec \<sharp>* Q;
xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M xvec N (P \<parallel> Q')"
and rOpen: "\<And>\<Psi> P M xvec yvec N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; x \<in> supp N; \<And>C. Prop C \<Psi> P M (xvec@yvec) N P';
x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> xvec; x \<sharp> yvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M;
yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; yvec \<sharp>* C; x \<sharp> C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) M (xvec@x#yvec) N P'"
and rScope: "\<And>\<Psi> P M xvec N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; \<And>C. Prop C \<Psi> P M xvec N P';
x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> xvec; x \<sharp> N; xvec \<sharp>* \<Psi>;
xvec \<sharp>* P; xvec \<sharp>* M; x \<sharp> C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) M xvec N (\<lparr>\<nu>x\<rparr>P')"
and rBang: "\<And>\<Psi> P M xvec N P' C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; guarded P; \<And>C. Prop C \<Psi> (P \<parallel> !P) M xvec N P'\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (!P) M xvec N P'"
shows "Prop C \<Psi> P M xvec N P'"
proof -
note \<open>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<close>
moreover from \<open>xvec \<sharp>* M\<close> have "bn(M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* subject(M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>)" by simp
moreover from \<open>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<close> have "distinct(bn(M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>))"
by(rule boundOutputDistinct)
ultimately show ?thesis
proof(nominal_induct \<Psi> P \<alpha>=="M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>" P' avoiding: C arbitrary: M xvec N rule: semanticsInduct)
case(cAlpha \<Psi> P \<alpha> P' p C M xvec N)
from \<open>(p \<bullet> \<alpha>) = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>\<close> have "(p \<bullet> p \<bullet> \<alpha>) = p \<bullet> (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>)"
by(simp add: fresh_bij)
with \<open>distinctPerm p\<close> have A: "\<alpha> = (p \<bullet> M)\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle>"
by(simp add: eqvts)
with \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha> \<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* bn(p \<bullet> \<alpha>)\<close> \<open>distinctPerm p\<close>
have "(p \<bullet> xvec) \<sharp>* \<Psi>" and "(p \<bullet> xvec) \<sharp>* P" and "(p \<bullet> xvec) \<sharp>* (p \<bullet> M)" and "(p \<bullet> xvec) \<sharp>* C" and "(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> xvec)"
by auto
moreover from A \<open>set p \<subseteq> set(bn \<alpha>) \<times> set(bn(p \<bullet> \<alpha>))\<close> \<open>distinctPerm p\<close>
have S: "set p \<subseteq> set(p \<bullet> xvec) \<times> set(p \<bullet> p \<bullet> xvec)" by simp
moreover note \<open>distinctPerm p\<close>
moreover from A \<open>bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>\<close> \<open>bn(p \<bullet> \<alpha>) \<sharp>* P'\<close>
have "(p \<bullet> p \<bullet> xvec) \<sharp>* (p \<bullet> N)" and "(p \<bullet> p \<bullet> xvec) \<sharp>* P'" by simp+
moreover from A have "Prop C \<Psi> P (p \<bullet> M) (p \<bullet> xvec) (p \<bullet> N) P'"
by(rule cAlpha)
ultimately have "Prop C \<Psi> P (p \<bullet> M) (p \<bullet> p \<bullet> xvec) (p \<bullet> p \<bullet> N) (p \<bullet> P')"
by(rule rAlpha)
moreover from A \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> have "(p \<bullet> xvec) \<sharp>* (p \<bullet> M)" by simp
hence "xvec \<sharp>* M" by(simp add: fresh_star_bij)
from A \<open>bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>\<close> \<open>distinctPerm p\<close> have "xvec \<sharp>* (p \<bullet> M)" by simp
hence "(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> M)" by(simp add: fresh_star_bij)
with \<open>distinctPerm p\<close> have "(p \<bullet> xvec) \<sharp>* M" by simp
with \<open>xvec \<sharp>* M\<close> S \<open>distinctPerm p\<close> have "(p \<bullet> M) = M" by simp
ultimately show ?case using S \<open>distinctPerm p\<close> by simp
next
case cInput
thus ?case by(simp add: residualInject)
next
case cOutput
thus ?case by(force dest: rOutput simp add: action.inject)
next
case cCase
thus ?case by(force intro: rCase)
next
case cPar1
thus ?case by(force intro: rPar1)
next
case cPar2
thus ?case by(force intro: rPar2)
next
case cComm1
thus ?case by(simp add: action.inject)
next
case cComm2
thus ?case by(simp add: action.inject)
next
case cOpen
thus ?case by(fastforce intro: rOpen simp add: action.inject)
next
case cScope
thus ?case by(fastforce intro: rScope)
next
case cBang
thus ?case by(fastforce intro: rBang)
qed
qed
lemma inputInduct[consumes 1, case_names cInput cCase cPar1 cPar2 cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes Trans: "\<Psi> \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'"
and rInput: "\<And>\<Psi> M K xvec N Tvec P C.
\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K; distinct xvec; set xvec \<subseteq> supp N;
length xvec = length Tvec; xvec \<sharp>* \<Psi>;
xvec \<sharp>* M; xvec \<sharp>* K; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (M\<lparr>\<lambda>*xvec N\<rparr>.P)
K (N[xvec::=Tvec]) (P[xvec::=Tvec])"
and rCase: "\<And>\<Psi> P M N P' \<phi> Cs C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; \<And>C. Prop C \<Psi> P M N P'; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (Cases Cs) M N P'"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>Q Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P M N P'; distinct A\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* M; A\<^sub>Q \<sharp>* N;
A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M N (P' \<parallel> Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q M N Q' A\<^sub>P P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>M\<lparr>N\<rparr> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q M N Q'; distinct A\<^sub>P;
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N;
A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) M N (P \<parallel> Q')"
and rScope: "\<And>\<Psi> P M N P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; \<And>C. Prop C \<Psi> P M N P'; x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> N; x \<sharp> C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) M N (\<lparr>\<nu>x\<rparr>P')"
and rBang: "\<And>\<Psi> P M N P' C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; guarded P; \<And>C. Prop C \<Psi> (P \<parallel> !P) M N P'\<rbrakk> \<Longrightarrow> Prop C \<Psi> (!P) M N P'"
shows "Prop C \<Psi> P M N P'"
using Trans
proof(nominal_induct \<Psi> P Rs=="M\<lparr>N\<rparr> \<prec> P'" avoiding: C arbitrary: P' rule: semantics.strong_induct)
case(cInput \<Psi> M K xvec N Tvec P C)
thus ?case
by(force intro: rInput simp add: residualInject action.inject)
next
case(Output \<Psi> M K N P C)
thus ?case by(simp add: residualInject)
next
case(Case \<Psi> P Rs \<phi> CS C)
thus ?case by(force intro: rCase)
next
case(cPar1 \<Psi> \<Psi>\<^sub>Q P \<alpha> P' Q A\<^sub>Q C P'')
thus ?case by(force intro: rPar1 simp add: residualInject)
next
case(cPar2 \<Psi> \<Psi>P Q \<alpha> Q' xvec P C Q'')
thus ?case by(force intro: rPar2 simp add: residualInject)
next
case(cComm1 \<Psi> \<Psi>Q P M N P' xvec \<Psi>P Q K zvec Q' yvec C PQ)
thus ?case by(simp add: residualInject)
next
case(cComm2 \<Psi> \<Psi>Q P M zvec N P' xvec \<Psi>P Q K yvec Q' C PQ)
thus ?case by(simp add: residualInject)
next
case(cOpen \<Psi> P M xvec N P' x yvec C P'')
thus ?case by(simp add: residualInject)
next
case(cScope \<Psi> P \<alpha> P' x C P'')
thus ?case by(force intro: rScope simp add: residualInject)
next
case(Bang \<Psi> P Rs C)
thus ?case by(force intro: rBang)
qed
lemma tauInduct[consumes 1, case_names cCase cPar1 cPar2 cComm1 cComm2 cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rs :: "('a, 'b, 'c) residual"
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
('a, 'b, 'c) psi \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes Trans: "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'"
and rCase: "\<And>\<Psi> P P' \<phi> Cs C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'; \<And>C. Prop C \<Psi> P P'; (\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (Cases Cs) P'"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P P' A\<^sub>Q Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<tau> \<prec> P'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P P';
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>;
A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (P' \<parallel> Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q Q' A\<^sub>P P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<tau> \<prec> Q'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q Q';
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>;
A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (P \<parallel> Q')"
and rComm1: "\<And>\<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
and rComm2: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
and rScope: "\<And>\<Psi> P P' x C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'; \<And>C. Prop C \<Psi> P P'; x \<sharp> \<Psi>; x \<sharp> C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (\<lparr>\<nu>x\<rparr>P')"
and rBang: "\<And>\<Psi> P P' C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>\<tau> \<prec> P'; guarded P; \<And>C. Prop C \<Psi> (P \<parallel> !P) P'\<rbrakk> \<Longrightarrow> Prop C \<Psi> (!P) P'"
shows "Prop C \<Psi> P P'"
using Trans
proof(nominal_induct \<Psi> P Rs=="\<tau> \<prec> P'" avoiding: C arbitrary: P' rule: semantics.strong_induct)
case(cInput M K xvec N Tvec P C)
thus ?case by(simp add: residualInject)
next
case(Output \<Psi> M K N P C)
thus ?case by(simp add: residualInject)
next
case(Case \<Psi> P Rs \<phi> Cs C)
thus ?case by(force intro: rCase simp add: residualInject)
next
case(cPar1 \<Psi> \<Psi>\<^sub>Q P \<alpha> P' A\<^sub>Q Q C P'')
thus ?case by(force intro: rPar1 simp add: residualInject)
next
case(cPar2 \<Psi> \<Psi>\<^sub>P Q \<alpha> Q' A\<^sub>P P C Q'')
thus ?case by(force intro: rPar2 simp add: residualInject)
next
case(cComm1 \<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q C PQ)
thus ?case by(force intro: rComm1 simp add: residualInject)
next
case(cComm2 \<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>P Q' A\<^sub>Q C PQ)
thus ?case by(force intro: rComm2 simp add: residualInject)
next
case(cOpen \<Psi> P M xvec N P' x yvec C P'')
thus ?case by(simp add: residualInject)
next
case(cScope \<Psi> P \<alpha> P' x C P'')
thus ?case by(force intro: rScope simp add: residualInject)
next
case(Bang \<Psi> P Rs C )
thus ?case by(force intro: rBang simp add: residualInject)
qed
lemma semanticsFrameInduct[consumes 3, case_names cAlpha cInput cOutput cCase cPar1 cPar2 cComm1 cComm2 cOpen cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rs :: "('a, 'b, 'c) residual"
and A\<^sub>P :: "name list"
and \<Psi>\<^sub>P :: 'b
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
('a, 'b, 'c) residual \<Rightarrow> name list \<Rightarrow> 'b \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes Trans: "\<Psi> \<rhd> P \<longmapsto> Rs"
and FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
and "distinct A\<^sub>P"
and rAlpha: "\<And>\<Psi> P A\<^sub>P \<Psi>\<^sub>P p Rs C. \<lbrakk>A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* (p \<bullet> A\<^sub>P); A\<^sub>P \<sharp>* Rs; A\<^sub>P \<sharp>* C;
set p \<subseteq> set A\<^sub>P \<times> set(p \<bullet> A\<^sub>P); distinctPerm p;
Prop C \<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> P Rs (p \<bullet> A\<^sub>P) (p \<bullet> \<Psi>\<^sub>P)"
and rInput: "\<And>\<Psi> M K xvec N Tvec P C.
\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K; distinct xvec; set xvec \<subseteq> supp N;
length xvec = length Tvec; xvec \<sharp>* \<Psi>;
xvec \<sharp>* M; xvec \<sharp>* K; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (M\<lparr>\<lambda>*xvec N\<rparr>.P)
(K\<lparr>(N[xvec::=Tvec])\<rparr> \<prec> (P[xvec::=Tvec])) ([]) (\<one>)"
and rOutput: "\<And>\<Psi> M K N P C. \<Psi> \<turnstile> M \<leftrightarrow> K \<Longrightarrow> Prop C \<Psi> (M\<langle>N\<rangle>.P) (K\<langle>N\<rangle> \<prec> P) ([]) (\<one>)"
and rCase: "\<And>\<Psi> P Rs \<phi> Cs A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> Rs; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P; \<And>C. Prop C \<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P;
(\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P; \<Psi>\<^sub>P \<simeq> \<one>; (supp \<Psi>\<^sub>P) = ({}::name set);
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Rs; A\<^sub>P \<sharp>* C\<rbrakk> \<Longrightarrow> Prop C \<Psi> (Cases Cs) Rs ([]) (\<one>)"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P \<alpha> P' A\<^sub>Q Q A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<alpha> \<prec> P';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P; distinct(bn \<alpha>);
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P' \<parallel> Q)) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q \<alpha> Q' A\<^sub>P P A\<^sub>Q \<Psi>\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<alpha> \<prec> Q';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (\<alpha> \<prec> Q') A\<^sub>Q \<Psi>\<^sub>Q; distinct(bn \<alpha>);
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* Q'; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rComm1: "\<And>\<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P ((M\<lparr>N\<rparr>) \<prec> P') A\<^sub>P \<Psi>\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q') A\<^sub>Q \<Psi>\<^sub>Q; distinct xvec;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rComm2: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P') A\<^sub>P \<Psi>\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>N\<rparr> \<prec> Q') A\<^sub>Q \<Psi>\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K; distinct xvec;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rOpen: "\<And>\<Psi> P M xvec yvec N P' x A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P') A\<^sub>P \<Psi>\<^sub>P; x \<in> supp N; x \<sharp> \<Psi>; x \<sharp> M;
x \<sharp> A\<^sub>P; x \<sharp> xvec; x \<sharp> yvec; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* xvec; A\<^sub>P \<sharp>* yvec; xvec \<sharp>* yvec; distinct xvec; distinct yvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* \<Psi>\<^sub>P; yvec \<sharp>* \<Psi>\<^sub>P;
yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; A\<^sub>P \<sharp>* C; x \<sharp> C; xvec \<sharp>* C; yvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P') (x#A\<^sub>P) \<Psi>\<^sub>P"
and rScope: "\<And>\<Psi> P \<alpha> P' x A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C \<Psi> P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P;
x \<sharp> \<Psi>; x \<sharp> \<alpha>; x \<sharp> A\<^sub>P; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P;
A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; distinct(bn \<alpha>);
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P;
A\<^sub>P \<sharp>* C; x \<sharp> C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (\<alpha> \<prec> (\<lparr>\<nu>x\<rparr>P')) (x#A\<^sub>P) \<Psi>\<^sub>P"
and rBang: "\<And>\<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto> Rs; guarded P; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C \<Psi> (P \<parallel> !P) Rs A\<^sub>P (\<Psi>\<^sub>P \<otimes> \<one>); \<Psi>\<^sub>P \<simeq> \<one>; supp \<Psi>\<^sub>P = ({}::name set);
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Rs; A\<^sub>P \<sharp>* C\<rbrakk> \<Longrightarrow> Prop C \<Psi> (!P) Rs ([]) (\<one>)"
shows "Prop C \<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P"
using Trans FrP \<open>distinct A\<^sub>P\<close>
proof(nominal_induct avoiding: A\<^sub>P \<Psi>\<^sub>P C rule: semantics.strong_induct)
case(cInput \<Psi> M K xvec N Tvec P A\<^sub>P \<Psi>\<^sub>P C)
from \<open>extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P) = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close>
have "A\<^sub>P = []" and "\<Psi>\<^sub>P = \<one>"
by auto
with \<open>\<Psi> \<turnstile> M \<leftrightarrow> K\<close> \<open>distinct xvec\<close> \<open>set xvec \<subseteq> supp N\<close> \<open>length xvec = length Tvec\<close>
\<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* M\<close> \<open>xvec \<sharp>* K\<close> \<open>xvec \<sharp>* C\<close>
show ?case by(blast intro: rInput)
next
case(Output \<Psi> M K N P A\<^sub>P \<Psi>\<^sub>P)
from \<open>extractFrame (M\<langle>N\<rangle>.P) = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close>
have "A\<^sub>P = []" and "\<Psi>\<^sub>P = \<one>"
by auto
with \<open>\<Psi> \<turnstile> M \<leftrightarrow> K\<close> show ?case
by(blast intro: rOutput)
next
case(Case \<Psi> P Rs \<phi> Cs A\<^sub>c\<^sub>P \<Psi>\<^sub>c\<^sub>P C)
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "distinct A\<^sub>P"
and "A\<^sub>P \<sharp>* (\<Psi>, P, Rs, C)"
by(rule freshFrame)
hence "A\<^sub>P \<sharp>* \<Psi>" and "A\<^sub>P \<sharp>* P" and "A\<^sub>P \<sharp>* Rs" and "A\<^sub>P \<sharp>* C"
by simp+
note \<open>\<Psi> \<rhd> P \<longmapsto> Rs\<close> FrP \<open>distinct A\<^sub>P\<close>
moreover from FrP \<open>distinct A\<^sub>P\<close> \<open>\<And>A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P\<close>
have "\<And>C. Prop C \<Psi> P Rs A\<^sub>P \<Psi>\<^sub>P" by simp
moreover note \<open>(\<phi>, P) mem Cs\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close>
moreover from \<open>guarded P\<close> FrP have "\<Psi>\<^sub>P \<simeq> \<one>" and "supp \<Psi>\<^sub>P = ({}::name set)" by(metis guardedStatEq)+
moreover note \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Rs\<close> \<open>A\<^sub>P \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (Cases Cs) Rs ([]) (\<one>)"
by(rule rCase)
thus ?case using \<open>extractFrame(Cases Cs) = \<langle>A\<^sub>c\<^sub>P, \<Psi>\<^sub>c\<^sub>P\<rangle>\<close> by simp
next
case(cPar1 \<Psi> \<Psi>\<^sub>Q P \<alpha> P' Q A\<^sub>Q A\<^sub>P\<^sub>Q \<Psi>\<^sub>P\<^sub>Q C)
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "distinct A\<^sub>P"
"A\<^sub>P \<sharp>* (P, Q, \<Psi>, \<alpha>, P', A\<^sub>Q, A\<^sub>P\<^sub>Q, C, \<Psi>\<^sub>Q)"
by(rule freshFrame)
hence "A\<^sub>P \<sharp>* P" and "A\<^sub>P \<sharp>* Q" and "A\<^sub>P \<sharp>* \<Psi>" and "A\<^sub>P \<sharp>* \<alpha>" and "A\<^sub>P \<sharp>* P'"
and "A\<^sub>P \<sharp>* A\<^sub>Q" and "A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q" and "A\<^sub>P \<sharp>* C" and "A\<^sub>P \<sharp>* \<Psi>\<^sub>Q"
by simp+
have FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>" by fact
from \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> FrP have "A\<^sub>Q \<sharp>* \<Psi>\<^sub>P"
by(force dest: extractFrameFreshChain)
from \<open>bn \<alpha> \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> FrP have "bn \<alpha> \<sharp>* \<Psi>\<^sub>P"
by(force dest: extractFrameFreshChain)
from \<open>extractFrame(P \<parallel> Q) = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>\<close> FrP FrQ \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close>
have "\<langle>(A\<^sub>P@A\<^sub>Q), \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q\<rangle> = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>"
by simp
moreover from \<open>distinct A\<^sub>P\<close> \<open>distinct A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> have "distinct(A\<^sub>P@A\<^sub>Q)"
by(auto simp add: fresh_star_def fresh_def name_list_supp)
ultimately obtain p where S: "set p \<subseteq> set(A\<^sub>P@A\<^sub>Q) \<times> set((p \<bullet> A\<^sub>P)@(p \<bullet> A\<^sub>Q))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>P\<^sub>Q = p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)" and Aeq: "A\<^sub>P\<^sub>Q = (p \<bullet> A\<^sub>P)@(p \<bullet> A\<^sub>Q)"
using \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>distinct A\<^sub>P\<^sub>Q\<close>
by(rule_tac frameChainEq') (assumption | simp add: eqvts)+
note \<open>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> FrP \<open>distinct A\<^sub>P\<close> FrQ \<open>distinct A\<^sub>Q\<close>
moreover from FrP \<open>distinct A\<^sub>P\<close> \<open>\<And>A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P\<rbrakk> \<Longrightarrow> Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P\<close>
have "\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P" by simp
moreover note \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close>
\<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* P'\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close> \<open>distinct(bn \<alpha>)\<close>
\<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>P\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>Q\<close>
\<open>A\<^sub>P \<sharp>* C\<close> \<open>A\<^sub>Q \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P' \<parallel> Q)) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
by(rule_tac rPar1)
with \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* C\<close>
\<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* P'\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
S \<open>distinctPerm p\<close> Aeq
have "Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P' \<parallel> Q)) (p \<bullet> (A\<^sub>P@A\<^sub>Q)) (p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q))"
by(rule_tac rAlpha) (assumption | simp add: eqvts)+
with \<Psi>eq Aeq show ?case by(simp add: eqvts)
next
case(cPar2 \<Psi> \<Psi>\<^sub>P Q \<alpha> Q' P A\<^sub>P A\<^sub>P\<^sub>Q \<Psi>\<^sub>P\<^sub>Q C)
obtain A\<^sub>Q \<Psi>\<^sub>Q where FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>" and "distinct A\<^sub>Q"
"A\<^sub>Q \<sharp>* (P, Q, \<Psi>, \<alpha>, Q', A\<^sub>P, A\<^sub>P\<^sub>Q, C, \<Psi>\<^sub>P)"
by(rule freshFrame)
hence "A\<^sub>Q \<sharp>* P" and "A\<^sub>Q \<sharp>* Q" and "A\<^sub>Q \<sharp>* \<Psi>" and "A\<^sub>Q \<sharp>* \<alpha>" and "A\<^sub>Q \<sharp>* Q'"
and "A\<^sub>Q \<sharp>* A\<^sub>P" and "A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q" and "A\<^sub>Q \<sharp>* C" and "A\<^sub>Q \<sharp>* \<Psi>\<^sub>P"
by simp+
from \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<close> have "A\<^sub>P \<sharp>* A\<^sub>Q" by simp
have FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" by fact
from \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<close> FrQ have "A\<^sub>P \<sharp>* \<Psi>\<^sub>Q"
by(force dest: extractFrameFreshChain)
from \<open>bn \<alpha> \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> FrQ have "bn \<alpha> \<sharp>* \<Psi>\<^sub>Q"
by(force dest: extractFrameFreshChain)
from \<open>extractFrame(P \<parallel> Q) = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>\<close> FrP FrQ \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close>
have "\<langle>(A\<^sub>P@A\<^sub>Q), \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q\<rangle> = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>"
by simp
moreover from \<open>distinct A\<^sub>P\<close> \<open>distinct A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> have "distinct(A\<^sub>P@A\<^sub>Q)"
by(auto simp add: fresh_star_def fresh_def name_list_supp)
ultimately obtain p where S: "(set p \<subseteq> (set(A\<^sub>P@A\<^sub>Q)) \<times> (set A\<^sub>P\<^sub>Q))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>P\<^sub>Q = p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)" and Aeq: "A\<^sub>P\<^sub>Q = ((p \<bullet> A\<^sub>P)@(p \<bullet> A\<^sub>Q))"
using \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>distinct A\<^sub>P\<^sub>Q\<close>
by(rule_tac frameChainEq') (assumption | simp add: eqvts)+
note \<open>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> FrP \<open>distinct A\<^sub>P\<close> FrQ \<open>distinct A\<^sub>Q\<close>
moreover from FrQ \<open>distinct A\<^sub>Q\<close> \<open>\<And>A\<^sub>Q \<Psi>\<^sub>Q C. \<lbrakk>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q\<rbrakk> \<Longrightarrow> Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (\<alpha> \<prec> Q') A\<^sub>Q \<Psi>\<^sub>Q\<close>
have "\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (\<alpha> \<prec> Q') A\<^sub>Q \<Psi>\<^sub>Q" by simp
moreover note \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* Q'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close>
\<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* Q'\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close> \<open>distinct(bn \<alpha>)\<close>
\<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>P\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>Q\<close>
\<open>A\<^sub>P \<sharp>* C\<close> \<open>A\<^sub>Q \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
by(rule_tac rPar2)
with \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* Q'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* C\<close>
\<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* Q'\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
S \<open>distinctPerm p\<close> Aeq
have "Prop C \<Psi> (P \<parallel> Q) (\<alpha> \<prec> (P \<parallel> Q')) (p \<bullet> (A\<^sub>P@A\<^sub>Q)) (p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q))"
by(rule_tac rAlpha) (assumption | simp add: eqvts)+
with \<Psi>eq Aeq show ?case by(simp add: eqvts)
next
case(cComm1 \<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q A\<^sub>P\<^sub>Q \<Psi>\<^sub>P\<^sub>Q C)
from \<open>distinct A\<^sub>P\<close> \<open>distinct A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> have "distinct(A\<^sub>P@A\<^sub>Q)"
by(auto simp add: fresh_star_def fresh_def name_list_supp)
from cComm1 have "Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
by(rule_tac rComm1)
moreover from \<open>extractFrame(P \<parallel> Q) = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>\<close> \<open>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close> \<open>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close>
\<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close>
have "\<langle>(A\<^sub>P@A\<^sub>Q), (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)\<rangle> = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>"
by simp
with \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>distinct(A\<^sub>P@A\<^sub>Q)\<close> \<open>distinct A\<^sub>P\<^sub>Q\<close>
obtain p where S: "(set p \<subseteq> (set(A\<^sub>P@A\<^sub>Q)) \<times> (set A\<^sub>P\<^sub>Q))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>P\<^sub>Q = p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)" and Aeq: "A\<^sub>P\<^sub>Q = p \<bullet> (A\<^sub>P@A\<^sub>Q)"
by(rule_tac frameChainEq') (assumption | simp)+
moreover note \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* xvec\<close>
\<open>A\<^sub>Q \<sharp>* xvec\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>Q \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* Q'\<close> \<open>A\<^sub>Q \<sharp>* Q'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close>
\<open>A\<^sub>P \<sharp>* C\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (p \<bullet> (A\<^sub>P@A\<^sub>Q)) (p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q))"
by(rule_tac rAlpha) auto
with \<Psi>eq Aeq show ?case by simp
next
case(cComm2 \<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q A\<^sub>P\<^sub>Q \<Psi>\<^sub>P\<^sub>Q C)
from \<open>distinct A\<^sub>P\<close> \<open>distinct A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> have "distinct(A\<^sub>P@A\<^sub>Q)"
by(auto simp add: fresh_star_def fresh_def name_list_supp)
from cComm2 have "Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
by(rule_tac rComm2)
moreover from \<open>extractFrame(P \<parallel> Q) = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>\<close> \<open>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>\<close> \<open>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close>
\<open>A\<^sub>P \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P\<close>
have "\<langle>(A\<^sub>P@A\<^sub>Q), (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)\<rangle> = \<langle>A\<^sub>P\<^sub>Q, \<Psi>\<^sub>P\<^sub>Q\<rangle>"
by simp
with \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>distinct(A\<^sub>P@A\<^sub>Q)\<close> \<open>distinct A\<^sub>P\<^sub>Q\<close>
obtain p where S: "(set p \<subseteq> (set(A\<^sub>P@A\<^sub>Q)) \<times> (set A\<^sub>P\<^sub>Q))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>P\<^sub>Q = p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)" and Aeq: "A\<^sub>P\<^sub>Q = p \<bullet> (A\<^sub>P@A\<^sub>Q)"
by(rule_tac frameChainEq') (assumption | simp)+
moreover note \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>P \<sharp>* xvec\<close>
\<open>A\<^sub>Q \<sharp>* xvec\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>Q \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* Q'\<close> \<open>A\<^sub>Q \<sharp>* Q'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>P\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* A\<^sub>P\<^sub>Q\<close>
\<open>A\<^sub>P \<sharp>* C\<close> \<open>A\<^sub>Q \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (P \<parallel> Q) (\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (p \<bullet> (A\<^sub>P@A\<^sub>Q)) (p \<bullet> (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q))"
by(rule_tac rAlpha) auto
with \<Psi>eq Aeq show ?case by simp
next
case(cOpen \<Psi> P M xvec yvec N P' x A\<^sub>x\<^sub>P \<Psi>\<^sub>x\<^sub>P C)
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "distinct A\<^sub>P"
and "A\<^sub>P \<sharp>* (\<Psi>, P, M, xvec, yvec, N, P', A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P, C, x)"
by(rule freshFrame)
hence "A\<^sub>P \<sharp>* \<Psi>" and "A\<^sub>P \<sharp>* P" and "A\<^sub>P \<sharp>* M" and "A\<^sub>P \<sharp>* xvec"and "A\<^sub>P \<sharp>* yvec" and "A\<^sub>P \<sharp>* N" and "A\<^sub>P \<sharp>* P'"
and "A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P" and "A\<^sub>P \<sharp>* \<Psi>\<^sub>x\<^sub>P" and "A\<^sub>P \<sharp>* C" and "x \<sharp> A\<^sub>P"
by simp+
from \<open>xvec \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* xvec\<close> FrP have "xvec \<sharp>* \<Psi>\<^sub>P"
by(force dest: extractFrameFreshChain)
from \<open>yvec \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* yvec\<close> FrP have "yvec \<sharp>* \<Psi>\<^sub>P"
by(force dest: extractFrameFreshChain)
from \<open>extractFrame(\<lparr>\<nu>x\<rparr>P) = \<langle>A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P\<rangle>\<close> FrP
have "\<langle>(x#A\<^sub>P), \<Psi>\<^sub>P\<rangle> = \<langle>A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P\<rangle>"
by simp
moreover from \<open>x \<sharp> A\<^sub>P\<close> \<open>distinct A\<^sub>P\<close> have "distinct(x#A\<^sub>P)" by simp
ultimately obtain p where S: "set p \<subseteq> set (x#A\<^sub>P) \<times> set (p \<bullet> (x#A\<^sub>P))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>x\<^sub>P = p \<bullet> \<Psi>\<^sub>P" and Aeq: "A\<^sub>x\<^sub>P = (p \<bullet> x)#(p \<bullet> A\<^sub>P)"
using \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close>\<open>x \<sharp> A\<^sub>x\<^sub>P\<close> \<open>distinct A\<^sub>x\<^sub>P\<close>
by(rule_tac frameChainEq') (assumption | simp add: eqvts)+
note \<open>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'\<close> FrP \<open>distinct A\<^sub>P\<close>
moreover from FrP \<open>distinct A\<^sub>P\<close> \<open>\<And>A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P') A\<^sub>P \<Psi>\<^sub>P\<close>
have "\<And>C. Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P') A\<^sub>P \<Psi>\<^sub>P" by simp
moreover note \<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> \<open>x \<in> supp N\<close> \<open>x \<sharp> A\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* M\<close> \<open>A\<^sub>P \<sharp>* xvec\<close> \<open>A\<^sub>P \<sharp>* yvec\<close> \<open>A\<^sub>P \<sharp>* N\<close> \<open>A\<^sub>P \<sharp>* P'\<close>
\<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* M\<close> \<open>xvec \<sharp>* \<Psi>\<^sub>P\<close> \<open>yvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P\<close> \<open>yvec \<sharp>* M\<close> \<open>yvec \<sharp>* \<Psi>\<^sub>P\<close>
\<open>A\<^sub>P \<sharp>* C\<close> \<open>x \<sharp> C\<close> \<open>xvec \<sharp>* C\<close> \<open>yvec \<sharp>* C\<close> \<open>xvec \<sharp>* yvec\<close> \<open>distinct xvec\<close> \<open>distinct yvec\<close>
ultimately have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P') (x#A\<^sub>P) \<Psi>\<^sub>P"
by(rule_tac rOpen)
with \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* M\<close> \<open>A\<^sub>P \<sharp>* xvec\<close> \<open>A\<^sub>P \<sharp>* yvec\<close> \<open>A\<^sub>P \<sharp>* N\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* C\<close> \<open>x \<sharp> A\<^sub>x\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close> \<open>x \<sharp> A\<^sub>P\<close>
\<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> C\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close> Aeq
S \<open>distinctPerm p\<close>
have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P') (p \<bullet> (x#A\<^sub>P)) (p \<bullet> \<Psi>\<^sub>P)"
by(rule_tac A\<^sub>P="x#A\<^sub>P" in rAlpha) (assumption | simp add: abs_fresh fresh_star_def boundOutputFresh)+
with \<Psi>eq Aeq show ?case by(simp add: eqvts)
next
case(cScope \<Psi> P \<alpha> P' x A\<^sub>x\<^sub>P \<Psi>\<^sub>x\<^sub>P C)
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "distinct A\<^sub>P"
and "A\<^sub>P \<sharp>* (\<Psi>, P, \<alpha>, P', A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P, C, x)"
by(rule freshFrame)
hence "A\<^sub>P \<sharp>* \<Psi>" and "A\<^sub>P \<sharp>* P" and "A\<^sub>P \<sharp>* \<alpha>" and "A\<^sub>P \<sharp>* P'"
and "A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P" and "A\<^sub>P \<sharp>* \<Psi>\<^sub>x\<^sub>P" and "A\<^sub>P \<sharp>* C" and "x \<sharp> A\<^sub>P"
by simp+
from \<open>bn \<alpha> \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> FrP have "bn \<alpha> \<sharp>* \<Psi>\<^sub>P"
by(force dest: extractFrameFreshChain)
from \<open>extractFrame(\<lparr>\<nu>x\<rparr>P) = \<langle>A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P\<rangle>\<close> FrP
have "\<langle>(x#A\<^sub>P), \<Psi>\<^sub>P\<rangle> = \<langle>A\<^sub>x\<^sub>P, \<Psi>\<^sub>x\<^sub>P\<rangle>"
by simp
moreover from \<open>x \<sharp> A\<^sub>P\<close> \<open>distinct A\<^sub>P\<close> have "distinct(x#A\<^sub>P)" by simp
ultimately obtain p where S: "set p \<subseteq> set (x#A\<^sub>P) \<times> set (p \<bullet> (x#A\<^sub>P))" and "distinctPerm p"
and \<Psi>eq: "\<Psi>\<^sub>x\<^sub>P = p \<bullet> \<Psi>\<^sub>P" and Aeq: "A\<^sub>x\<^sub>P = (p \<bullet> x)#(p \<bullet> A\<^sub>P)"
using \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close>\<open>x \<sharp> A\<^sub>x\<^sub>P\<close> \<open>distinct A\<^sub>x\<^sub>P\<close>
by(rule_tac frameChainEq') (assumption | simp add: eqvts)+
note \<open>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'\<close> FrP \<open>distinct A\<^sub>P\<close>
moreover from FrP \<open>distinct A\<^sub>P\<close> \<open>\<And>A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P\<close>
have "\<And>C. Prop C \<Psi> P (\<alpha> \<prec> P') A\<^sub>P \<Psi>\<^sub>P" by simp
moreover note \<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> \<alpha>\<close> \<open>x \<sharp> A\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>distinct(bn \<alpha>)\<close>
\<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* C\<close> \<open>x \<sharp> C\<close> \<open>bn \<alpha> \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (\<alpha> \<prec> (\<lparr>\<nu>x\<rparr>P')) (x#A\<^sub>P) \<Psi>\<^sub>P"
by(rule_tac rScope)
with \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* \<alpha>\<close> \<open>A\<^sub>P \<sharp>* P'\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* C\<close> \<open>x \<sharp> A\<^sub>x\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>x\<^sub>P\<close> \<open>x \<sharp> A\<^sub>P\<close>
\<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> \<alpha>\<close> \<open>x \<sharp> C\<close> Aeq
S \<open>distinctPerm p\<close>
have "Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (\<alpha> \<prec> (\<lparr>\<nu>x\<rparr>P')) (p \<bullet> (x#A\<^sub>P)) (p \<bullet> \<Psi>\<^sub>P)"
by(rule_tac A\<^sub>P="x#A\<^sub>P" in rAlpha) (assumption | simp add: abs_fresh fresh_star_def)+
sessions
next
case \> RsA<subb\sub <>\^>b\^>PCjava.lang.StringIndexOutOfBoundsException: Index 67 out of bounds for length 67
obtain A\<^sub>P \<Psi>\<^sub>P where FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>" and "distinct A\<^sub>P"
and "A\<^sub>P \<sharp>* (\<Psi>, P, Rs, C)"
by(rule freshFrame)
hence "A\<^sub>P \<sharp>* \<Psi>" and "A\<^sub>P \<sharp>* P" and "A\<^sub>P \<sharp>* Rs" and "A\<^sub>P \<sharp>* C"
by simp+
note \<open>\<Psi> \<rhd> P \<parallel> !P \<longmapsto> Rs\<close> \<open>guarded P\<close> FrP \<open>distinct A\<^sub>P\<close>
moreover from FrP have "extractFrame (P \<parallel> !P) = \<langle>A\<^sub>P, \<Psi>\<^sub>P \<otimes> \<one>\<rangle>"
by simp
with \<open>distinct A\<^sub>P\<close> \<open>\<And>A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>extractFrame (P \<parallel> !P) = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> (P \<parallel> !P) Rs A\<^sub>P \<Psi>\<^sub>P\<close>
have "\<And>C. Prop C \<Psi> (P \<parallel> !P) Rs A\<^sub>P (\<Psi>\<^sub>P \<otimes> \<one>)" by simp
moreover from \<open>guarded P\<close> FrP have "\<Psi>\<^sub>P \<simeq> \<one>" and "supp \<Psi>\<^sub>P = ({}::name set)" by(metis guardedStatEq)+
moreover note \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* Rs\<close> \<open>A\<^sub>P \<sharp>* C\<close>
ultimately have "Prop C \<Psi> (!P) Rs ([]) (\<one>)"
by(rule rBang)
thus ?case using \<open>extractFrame(!P) = \<langle>A\<^sub>b\<^sub>P, \<Psi>\<^sub>b\<^sub>P\<rangle>\<close> by simp
qed
lemma semanticsFrameInduct'[consumes 5, case_names cAlpha cFrameAlpha cInput cOutput cCase cPar1 cPar2 cComm1 cComm2 cOpen cScope cBang]:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rs :: "('a, 'b, 'c) residual"
and A\<^sub>P :: "name list"
and \<Psi>\<^sub>P :: 'b
and Prop :: "'d::fs_name \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow> 'a action \<Rightarrow>
('a, 'b, 'c) psi \<Rightarrow> name list \<Rightarrow> 'b \<Rightarrow> bool"
and C :: "'d::fs_name"
assumes Trans: "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
and FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
and "distinct A\<^sub>P"
and "bn \<alpha> \<sharp>* subject \<alpha>"
and "distinct(bn \<alpha>)"
and rAlpha: "\<And>\<Psi> P \<alpha> P' p A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P;
bn \<alpha> \<sharp>* C; bn \<alpha> \<sharp>* (p \<bullet> \<alpha>); A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* C;
set p \<subseteq> set(bn \<alpha>) \<times> set(bn(p \<bullet> \<alpha>)); distinctPerm p;
bn(p \<bullet> \<alpha>) \<sharp>* \<alpha>; (bn(p \<bullet> \<alpha>)) \<sharp>* P'; Prop C \<Psi> P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P\<rbrakk> \<Longrightarrow>
Prop C \<Psi> P (p \<bullet> \<alpha>) (p \<bullet> P') A\<^sub>P \<Psi>\<^sub>P"
and rFrameAlpha: "\<And>\<Psi> P A\<^sub>P \<Psi>\<^sub>P p \<alpha> P' C. \<lbrakk>A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* (p \<bullet> A\<^sub>P); A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* C;
set p \<subseteq> set A\<^sub>P \<times> set(p \<bullet> A\<^sub>P); distinctPerm p; A\<^sub>P \<sharp>* subject \<alpha>;
Prop C \<Psi> P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P\<rbrakk> \<Longrightarrow> Prop C \<Psi> P \<alpha> P' (p \<bullet> A\<^sub>P) (p \<bullet> \<Psi>\<^sub>P)"
and rInput: "\<And>\<Psi> M K xvec N Tvec P C.
\<lbrakk>\<Psi> \<turnstile> M \<leftrightarrow> K; distinct xvec; set xvec \<subseteq> supp N;
length xvec = length Tvec; xvec \<sharp>* \<Psi>;
xvec \<sharp>* M; xvec \<sharp>* K; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (M\<lparr>\<lambda>*xvec N\<rparr>.P)
(K\<lparr>(N[xvec::=Tvec])\<rparr>) (P[xvec::=Tvec]) ([]) (\<one>)"
and rOutput: "\<And>\<Psi> M K N P C. \<Psi> \<turnstile> M \<leftrightarrow> K \<Longrightarrow> Prop C \<Psi> (M\<langle>N\<rangle>.P) (K\<langle>N\<rangle>) P ([]) (\<one>)"
and rCase: "\<And>\<Psi> P \<alpha> P' \<phi> Cs A\<^sub>P \<Psi>\<^sub>P C. \<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P; \<And>C. Prop C \<Psi> P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P;
(\<phi>, P) mem Cs; \<Psi> \<turnstile> \<phi>; guarded P; \<Psi>\<^sub>P \<simeq> \<one>; (supp \<Psi>\<^sub>P) = ({}::name set);
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* C\<rbrakk> \<Longrightarrow> Prop C \<Psi> (Cases Cs) \<alpha> P' ([]) (\<one>)"
and rPar1: "\<And>\<Psi> \<Psi>\<^sub>Q P \<alpha> P' A\<^sub>Q Q A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>\<alpha> \<prec> P';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P;
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) \<alpha> (P' \<parallel> Q) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rPar2: "\<And>\<Psi> \<Psi>\<^sub>P Q \<alpha> Q' A\<^sub>P P A\<^sub>Q \<Psi>\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>\<alpha> \<prec> Q';
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q \<alpha> Q' A\<^sub>Q \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* Q'; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; bn \<alpha> \<sharp>* \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) \<alpha> (P \<parallel> Q') (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rComm1: "\<And>\<Psi> \<Psi>\<^sub>Q P M N P' A\<^sub>P \<Psi>\<^sub>P Q K xvec Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (M\<lparr>N\<rparr>) P' A\<^sub>P \<Psi>\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K; distinct xvec;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) Q' A\<^sub>Q \<Psi>\<^sub>Q;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rComm2: "\<And>\<Psi> \<Psi>\<^sub>Q P M xvec N P' A\<^sub>P \<Psi>\<^sub>P Q K Q' A\<^sub>Q C.
\<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>Q) P (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) P' A\<^sub>P \<Psi>\<^sub>P;
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'; extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q;
\<And>C. Prop C (\<Psi> \<otimes> \<Psi>\<^sub>P) Q (K\<lparr>N\<rparr>) Q' A\<^sub>Q \<Psi>\<^sub>Q;
\<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K; distinct xvec;
A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* Q; A\<^sub>P \<sharp>* Q'; A\<^sub>P \<sharp>* A\<^sub>Q; A\<^sub>P \<sharp>* xvec; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* \<Psi>\<^sub>P;
A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* N; A\<^sub>Q \<sharp>* P'; A\<^sub>Q \<sharp>* Q; A\<^sub>Q \<sharp>* K; A\<^sub>Q \<sharp>* Q';
A\<^sub>Q \<sharp>* xvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* \<Psi>\<^sub>P; xvec \<sharp>* \<Psi>\<^sub>Q; xvec \<sharp>* P; xvec \<sharp>* M;
xvec \<sharp>* Q; xvec \<sharp>* K; A\<^sub>P \<sharp>* C; A\<^sub>Q \<sharp>* C; xvec \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (P \<parallel> Q) (\<tau>) (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')) (A\<^sub>P@A\<^sub>Q) (\<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q)"
and rOpen: "\<And>\<Psi> P M xvec yvec N P' x A\<^sub>P \<Psi>\<^sub>P y C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C \<Psi> P (M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle>) P' A\<^sub>P \<Psi>\<^sub>P; x \<in> supp N; x \<sharp> \<Psi>; x \<sharp> M;
x \<sharp> A\<^sub>P; x \<sharp> xvec; x \<sharp> yvec; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P';
A\<^sub>P \<sharp>* xvec; A\<^sub>P \<sharp>* yvec; xvec \<sharp>* yvec; distinct xvec; distinct yvec;
xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* \<Psi>\<^sub>P;
yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; A\<^sub>P \<sharp>* C; x \<sharp> C; xvec \<sharp>* C; yvec \<sharp>* C;
y \<noteq> x; y \<sharp> \<Psi>; y \<sharp> P; y \<sharp> M; y \<sharp> xvec; y \<sharp> yvec; y \<sharp> N; y \<sharp> P'; y \<sharp> A\<^sub>P; y \<sharp> \<Psi>\<^sub>P; y \<sharp> C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) (M\<lparr>\<nu>*(xvec@y#yvec)\<rparr>\<langle>([(x, y)] \<bullet> N)\<rangle>) ([(x, y)] \<bullet> P') (x#A\<^sub>P) \<Psi>\<^sub>P"
and rScope: "\<And>\<Psi> P \<alpha> P' x A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P;
\<And>C. Prop C \<Psi> P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P;
x \<sharp> \<Psi>; x \<sharp> \<alpha>; x \<sharp> A\<^sub>P; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P;
A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P';
bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P;
A\<^sub>P \<sharp>* C; x \<sharp> C; bn \<alpha> \<sharp>* C\<rbrakk> \<Longrightarrow>
Prop C \<Psi> (\<lparr>\<nu>x\<rparr>P) \<alpha> (\<lparr>\<nu>x\<rparr>P') (x#A\<^sub>P) \<Psi>\<^sub>P"
and rBang: "\<And>\<Psi> P \<alpha> P' A\<^sub>P \<Psi>\<^sub>P C.
\<lbrakk>\<Psi> \<rhd> P \<parallel> !P \<longmapsto>\<alpha> \<prec> P'; guarded P; extractFrame P = \<lang | |