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"
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"
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
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)"
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)› moreoverfrom xvecFreshB have"set (xvec) ♯* ((ν*zvec)B)" by (simp add: boundOutputFreshSet) (simp add: fresh_star_def) ultimatelyhave"((ν*zvec)B) = p ∙ ((ν*zvec)B)" by (rule_tac pt_freshs_freshs [symmetric]) auto thenshow ?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"
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
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
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 moreoverwith‹(ν*xvec)M ≺' P = (ν*yvec)N ≺' Q›have"yvec = []" by(case_tac yvec) auto ultimatelyshow ?caseby 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 ?caseby 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 ?caseby 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"
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"
moreoverobtain 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 moreoverwith Eq have"yvec = []" by(case_tac yvec) auto ultimatelyshow ?caseusing 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 moreoverfrom‹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)
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"
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) thenobtain 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+ moreoverhave"(ν*xvec)(νx)B = (ν*yvec)(νy)B'"by fact ultimatelyshow ?caseby(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+ thenobtain 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 moreoverfrom xineqx' xineqy' xFreshB' have"x ♯ [(x', y')] ∙ B'"by(simp add: fresh_left calc_atm) moreoverfrom xineqx' xineqy' xFreshyvec' have"x ♯ [(x', y')] ∙ yvec'"by(simp add: fresh_left calc_atm) ultimatelyhave"(ν*xvec')B = (ν*([(x', y')] ∙ yvec'))([(x, ([(x', y')] ∙ y))] ∙ [(x', y')] ∙ B')"using Eq' xFreshxvec' L'' by(rule_tac Suc) moreoverfrom 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 ultimatelyshow ?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 ?caseby 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"
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" moreoverobtain 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 moreoverwith Eq have"yvec = []" by(case_tac yvec) auto ultimatelyshow ?caseusing 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)+ moreoverfrom‹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 moreovernote‹xvec' ♯* R›‹length xvec' = n› ultimatelyobtain 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) moreoverfrom xFreshQR have"x ♯(ν*yvec')N ≺' Q" by(force simp add: boundOutputFresh) ultimatelyshow ?thesis using‹P = T ∥ R›‹xvec=x#xvec'›‹yvec=y#yvec'› xFreshQR by(force simp add: alphaBoundOutput name_swap eqvts) qed qed ultimatelyshow ?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"
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" moreoverobtain 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 moreoverwith Eq have"yvec = []" by(case_tac yvec) auto ultimatelyshow ?caseusing 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) moreovernote‹xvec' ♯* yvec'›‹length xvec' = n› ultimatelyobtain 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 moreoverfrom‹P = T ∥ (p ∙ [(x, y)] ∙ R)›have"P = T ∥ ((p @ [(x, y)]) ∙ R)" by(simp add: pt2[OF pt_name_inst]) moreoverfrom 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 ultimatelyshow ?thesis using‹xvec=x#xvec'›‹yvec=y#yvec'› by(rule_tac x="p@[(x, y)]"in exI) force qed qed ultimatelyshow ?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"
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" moreoverobtain 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 moreoverwith Eq have"yvec = []" by(case_tac yvec) auto ultimatelyshow ?caseusing 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)+ moreoverfrom‹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 moreovernote‹xvec' ♯* Q›‹length xvec' = n› ultimatelyobtain 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) moreoverfrom xFreshQR have"x ♯(ν*yvec')N ≺' R" by(force simp add: boundOutputFresh) ultimatelyshow ?thesis using‹P = Q ∥ T›‹xvec=x#xvec'›‹yvec=y#yvec'› xFreshQR by(force simp add: alphaBoundOutput name_swap eqvts) qed qed ultimatelyshow ?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"
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"
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"
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"
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"
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
assumes"∧M N. α = M(N)==> Prop" and"∧M xvec N. α = M(ν*xvec)⟨N⟩==> Prop" and"α = τ ==> Prop"
showsProp using assms by(nominal_induct α rule: action.strong_induct) auto
lemma actionPar1Dest: fixes α :: "('a::fs_name) action" and P :: "('a, 'b::fs_name, 'c::fs_name) psi" and β :: "('a::fs_name) action" and Q :: "('a, 'b, 'c) psi" and R :: "('a, 'b, 'c) psi"
assumes"α ≺ P = β ≺ (Q ∥ R)" and"bn α ♯* bn β"
obtains T p where"set p ⊆ set(bn α) × set(bn β)"and"P = T ∥ (p ∙ R)"and"α ≺ T = β ≺ Q" using assms apply(cases rule: actionCases[where α=α]) apply(auto simp add: residualInject) by(drule_tac boundOutputPar1Dest') auto
lemma actionPar2Dest: fixes α :: "('a::fs_name) action" and P :: "('a, 'b::fs_name, 'c::fs_name) psi" and β :: "('a::fs_name) action" and Q :: "('a, 'b, 'c) psi" and R :: "('a, 'b, 'c) psi"
assumes"α ≺ P = β ≺ (Q ∥ R)" and"bn α ♯* bn β"
obtains T p where"set p ⊆ set(bn α) × set(bn β)"and"P = (p ∙ Q) ∥ T"and"α ≺ T = β ≺ R" using assms apply(cases rule: actionCases[where α=α]) apply(auto simp add: residualInject) by(drule_tac boundOutputPar2Dest') auto
lemma actionScopeDest: fixes α :: "('a::fs_name) action" and P :: "('a, 'b::fs_name, 'c::fs_name) psi" fixes β :: "('a::fs_name) action" and x :: name and Q :: "('a, 'b, 'c) psi"
lemma nilTrans[dest]: fixes Ψ :: '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 × ('a, 'b, 'c) psi) list" and Ψ' :: 'b
obtains p where"set p ⊆ set(bn α) × set(bn(p ∙ α))"and"distinctPerm p"and"β = p ∙ α"and"Q = p ∙ P"and"bn α ♯* β"and"bn α ♯* Q"and"bn(p ∙ α) ♯* α"and"bn(p ∙ α) ♯* P" using assms proof(nominal_induct α rule: action.strong_induct) case(In M N) thus ?caseby(simp add: residualInject) next case(Out M xvec N) thus ?case by(auto simp add: residualInject)
(drule_tac boundOutputChainEq'', auto) next case Tau thus ?caseby(simp add: residualInject) qed
lemma semanticsInduct[consumes 3, case_names cAlpha cInput cOutput cCase cPar1 cPar2 cComm1 cComm2 cOpen cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a action → ('a, 'b, 'c) psi → bool" and C :: "'d::fs_name"
assumes"Ψ ⊳ P ⟼α ≺ P'" and"bn α ♯* (subject α)" and"distinct(bn α)" and rAlpha: "∧Ψ P α P' p C. [bn α ♯* Ψ; bn α ♯* P; bn α ♯* (subject α); bn α ♯* C; bn α ♯* (bn(p ∙ α)); set p ⊆ set(bn α) × set(bn(p ∙ α)); distinctPerm p; (bn(p ∙ α)) ♯* α; (bn(p ∙ α)) ♯* P'; Prop C Ψ P α P']==> Prop C Ψ P (p ∙ α) (p ∙ P')" and rInput: "∧Ψ M K xvec N Tvec P C. [Ψ ⊨ M ↔ K; distinct xvec; set xvec ⊆ supp N; length xvec = length Tvec; xvec ♯* Ψ; xvec ♯* M; xvec ♯* K; xvec ♯* C]==> Prop C Ψ (M(λ*xvec N).P) (K((N[xvec::=Tvec]))) (P[xvec::=Tvec])" and rOutput: "∧Ψ M K N P C. [Ψ ⊨ M ↔ K]==> Prop C Ψ (M⟨N⟩.P) (K⟨N⟩) P" and rCase: "∧Ψ P α P' φ Cs C. [Ψ ⊳ P ⟼α ≺ P'; ∧C. Prop C Ψ P α P'; (φ, P) mem Cs; Ψ ⊨ φ; guarded P]==> Prop C Ψ (Cases Cs) α P'" and rPar1: "∧Ψ ΨQ P α P' AQ Q C. [Ψ ⊗ ΨQ⊳ P ⟼α ≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P α P'; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* α; AQ♯* P'; AQ♯* C; distinct(bn α); bn α ♯* Q; bn α ♯* Ψ; bn α ♯* ΨQ; bn α ♯* P; bn α ♯* subject α; bn α ♯* C]==> Prop C Ψ (P ∥ Q) α (P' ∥ Q)" and rPar2: "∧Ψ ΨP Q α Q' AP P C. [Ψ ⊗ ΨP⊳ Q ⟼α ≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨP) Q α Q'; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* α; AP♯* Q'; AP♯* C; distinct(bn α); bn α ♯* Q; bn α ♯* Ψ; bn α ♯* ΨP; bn α ♯* P; bn α ♯* subject α; bn α ♯* C]==> Prop C Ψ (P ∥ Q) α (P ∥ Q')" and rComm1: "∧Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; ∧C. Prop C (Ψ ⊗ ΨQ) P (M(N)) P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(ν*xvec)⟨N⟩≺ Q'; ∧C. Prop C (Ψ ⊗ ΨP) Q (K(ν*xvec)⟨N⟩) Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; distinct xvec; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) (τ) ((ν*xvec)(P' ∥ Q'))" and rComm2: "∧Ψ ΨQ P M xvec N P' AP ΨP Q K Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; ∧C. Prop C (Ψ ⊗ ΨQ) P (M(ν*xvec)⟨N⟩) P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'; ∧C. Prop C (Ψ ⊗ ΨP) Q (K(N)) Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; distinct xvec; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) (τ) ((ν*xvec)(P' ∥ Q'))" and rOpen: "∧Ψ P M xvec yvec N P' x C. [Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'; x ∈ supp N; ∧C. Prop C Ψ P (M(ν*(xvec@yvec))⟨N⟩) P'; x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ yvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; distinct xvec; distinct yvec; yvec ♯* Ψ; yvec ♯* P; yvec ♯* M; yvec ♯* C; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) (M(ν*(xvec@x#yvec))⟨N⟩) P'" and rScope: "∧Ψ P α P' x C. [Ψ ⊳ P ⟼α ≺ P'; ∧C. Prop C Ψ P α P'; x ♯ Ψ; x ♯ α; bn α ♯* Ψ; bn α ♯* P; bn α ♯* (subject α); x ♯ C; bn α ♯* C; distinct(bn α)]==> Prop C Ψ ((νx)P) α ((νx)P')" and rBang: "∧Ψ P α P' C. [Ψ ⊳ P ∥ !P ⟼α ≺ P'; guarded P; ∧C. Prop C Ψ (P ∥ !P) α P']==> Prop C Ψ (!P) α P'"
shows"Prop C Ψ P α P'" using‹Ψ ⊳ P ⟼α ≺ P'›‹bn α ♯* (subject α)›‹distinct(bn α)› proof(nominal_induct x3=="α ≺ P'" avoiding: α C arbitrary: P' rule: semantics.strong_induct) case(cInput Ψ M K xvec N Tvec P α C P') thus ?caseby(force intro: rInput simp add: residualInject) next case(Output Ψ M K N P α C P') thus ?caseby(force intro: rOutput simp add: residualInject) next case(Case Ψ P Rs φ Cs α C) thus ?caseby(auto intro: rCase) next case(cPar1 Ψ ΨQ P α P' Q AQ α' C P'') note‹α ≺ (P' ∥ Q) = α' ≺ P''› moreoverfrom‹bn α ♯* α'›have"bn α ♯* (bn α')"by auto moreovernote‹distinct (bn α)›‹distinct(bn α')› moreoverfrom‹bn α ♯* subject α›‹bn α' ♯* subject α'› have"bn α ♯* (α ≺ P' ∥ Q)"and"bn α' ♯* (α' ≺ P'')"by simp+ ultimatelyobtain p where S: "(set p) ⊆ (set(bn α)) × (set(bn(p ∙ α)))"and"distinctPerm p" and αEq: "α' = p ∙ α"and P'eq: "P'' = p ∙ (P' ∥ Q)"and"(bn(p ∙ α)) ♯* α" and"(bn(p ∙ α)) ♯* (P' ∥ Q)" by(rule residualEq)
lemma outputInduct[consumes 1, case_names cOutput cCase cPar1 cPar2 cOpen cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a → ('a, 'b, 'c) boundOutput → bool" and C :: "'d::fs_name"
assumes"Ψ ⊳ P ⟼ROut M B" and rOutput: "∧Ψ M K N P C. [Ψ ⊨ M ↔ K]==> Prop C Ψ (M⟨N⟩.P) K (N ≺' P)" and rCase: "∧Ψ P M B φ Cs C. [Ψ ⊳ P ⟼(ROut M B); ∧C. Prop C Ψ P M B; (φ, P) mem Cs; Ψ ⊨ φ; guarded P]==> Prop C Ψ (Cases Cs) M B" and rPar1: "∧Ψ ΨQ P M xvec N P' AQ Q C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P M ((ν*xvec)N ≺' P'); AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* xvec; AQ♯* N; AQ♯* P'; AQ♯* C; xvec ♯* Q; xvec ♯* Ψ; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M ((ν*xvec)N ≺' (P' ∥ Q))" and rPar2: "∧Ψ ΨP Q M xvec N Q' AP P C. [Ψ ⊗ ΨP⊳ Q ⟼M(ν*xvec)⟨N⟩≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨP) Q M ((ν*xvec)N ≺' Q'); AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* xvec; AP♯* N; AP♯* Q'; AP♯* C; xvec ♯* P; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* Q; xvec ♯* M; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M ((ν*xvec)N ≺' (P ∥ Q'))" and rOpen: "∧Ψ P M xvec yvec N P' x C. [Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'; x ∈ supp N; ∧C. Prop C Ψ P M ((ν*(xvec@yvec))N ≺' P'); x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ yvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; xvec ♯* yvec; yvec ♯* Ψ; yvec ♯* P; yvec ♯* M; yvec ♯* C; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) M ((ν*(xvec@x#yvec))N ≺' P')" and rScope: "∧Ψ P M xvec N P' x C. [Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; ∧C. Prop C Ψ P M ((ν*xvec)N ≺' P'); x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ N; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) M ((ν*xvec)N ≺' (νx)P')" and rBang: "∧Ψ P M B C. [Ψ ⊳ P ∥ !P ⟼(ROut M B); guarded P; ∧C. Prop C Ψ (P ∥ !P) M B]==> Prop C Ψ (!P) M B" shows"Prop C Ψ P M B" using‹Ψ ⊳ P ⟼(ROut M B)› proof(nominal_induct Ψ P Rs=="(ROut M B)" avoiding: C arbitrary: B rule: semantics.strong_induct) case(cInput Ψ M K xvec N Tvec P C) thus ?caseby(simp add: residualInject) next case(Output Ψ M K N P C) thus ?caseby(force simp add: residualInject intro: rOutput) next case(Case Ψ P Rs φ Cs C) thus ?caseby(force intro: rCase) next case(cPar1 Ψ ΨQ P α P' Q AQ C) thus ?caseby(force intro: rPar1 simp add: residualInject) next case(cPar2 Ψ ΨP Q α Q' P AP C) thus ?caseby(force intro: rPar2 simp add: residualInject) next case cComm1 thus ?caseby(simp add: residualInject) next case cComm2 thus ?caseby(simp add: residualInject) next case(cOpen Ψ P M xvec yvec N P' x C B) thus ?caseby(force intro: rOpen simp add: residualInject) next case(cScope Ψ P M α P' x C) thus ?caseby(force intro: rScope simp add: residualInject) next case(Bang Ψ P Rs C) thus ?caseby(force intro: rBang) qed
lemma boundOutputBindObject: fixes Ψ :: '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
shows"y ∈ supp(object α)" using assms proof(nominal_induct avoiding: P' arbitrary: y rule: semanticsInduct) case(cAlpha Ψ P α P' p P'' y) from‹y ∈ set(bn(p ∙ α))›have"(p ∙ y) ∈ (p ∙ set(bn(p ∙ α)))" by(rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) hence"(p ∙ y) ∈ set(bn α)"using‹distinctPerm p› by(simp add: eqvts) hence"(p ∙ y) ∈ supp(object α)"by(rule cAlpha) hence"(p ∙ p ∙ y) ∈ (p ∙ supp(object α))" by(rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) thus ?caseusing‹distinctPerm p› by(simp add: eqvts) next case cInput thus ?caseby(simp add: supp_list_nil) next case cOutput thus ?caseby(simp add: supp_list_nil) next case cCase thus ?caseby simp next case cPar1 thus ?caseby simp next case cPar2 thus ?caseby simp next case cComm1 thus ?caseby(simp add: supp_list_nil) next case cComm2 thus ?caseby(simp add: supp_list_nil) next case cOpen thus ?caseby(auto simp add: supp_list_cons supp_list_append supp_atm supp_some) next case cScope thus ?caseby simp next case cBang thus ?caseby simp qed
lemma alphaBoundOutputChain': fixes yvec :: "name list" and xvec :: "name list" and B :: "('a, 'b, 'c) boundOutput"
shows"(ν*xvec)B = (ν*yvec)([xvec yvec] ∙v B)" using assms proof(induct rule: composePermInduct) case cBase show ?caseby 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"
shows"distinct(bn β)" using assms proof(rule_tac actionCases[where α=α], auto simp add: residualInject supp_some) fix xvec M yvec N assume Eq: "(ν*xvec)N ≺' P = (ν*yvec)M ≺' Q" assume"distinct xvec"and"xvec ♯* M"and"xvec ♯* yvec"and"xvec ♯* Q" assume Mem: "∧x. x ∈ set xvec ==> x ∈ (supp N)" show"distinct yvec" proof - from Eq have"length xvec = length yvec" by(rule boundOutputChainEqLength) with Eq ‹distinct xvec›‹xvec ♯* yvec›‹xvec ♯* M›‹xvec ♯* Q› Mem show ?thesis proof(induct n=="length xvec" arbitrary: xvec yvec M Q rule: nat.induct) case(zero xvec yvec M Q) thus ?caseby simp next case(Suc n xvec yvec M Q) have L: "length xvec = length yvec"and"Suc n = length xvec"by fact+ thenobtain 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 ♯* yvec"and xvecDist: "distinct xvec"by fact+ with xEq yEq have xineqy: "x ≠ y"and xvec'Freshyvec': "xvec' ♯* yvec'" and xvec'Dist: "distinct xvec'"and xFreshxvec': "x ♯ xvec'" and xFreshyvec': "x ♯ yvec'"and yFreshxvec': "y ♯ xvec'" by auto have Eq: "(ν*xvec)N ≺' P = (ν*yvec)M ≺' Q"by fact with xEq yEq xineqy have Eq': "(ν*xvec')N ≺' P = (ν*([(x, y)] ∙ yvec'))([(x, y)] ∙ M) ≺' ([(x, y)] ∙ Q)" by(simp add: boundOutput.inject alpha eqvts) moreoverhave Mem:"∧x. x ∈ set xvec ==> x ∈ supp N"by fact with xEq have"∧x. x ∈ set xvec' ==> x ∈ supp N"by simp moreoverhave"xvec ♯* M"by fact with xEq xFreshxvec' yFreshxvec' have"xvec' ♯* ([(x, y)] ∙ M)"by simp moreoverhave xvecFreshQ: "xvec ♯* Q"by fact with xEq xFreshxvec' yFreshxvec' have"xvec' ♯* ([(x, y)] ∙ Q)"by simp moreoverhave"Suc n = length xvec"by fact with xEq have"n = length xvec'"by simp moreoverfrom xvec'Freshyvec' xFreshxvec' yFreshxvec' have"xvec' ♯* ([(x, y)] ∙ yvec')" by simp moreoverfrom L' have"length xvec' = length([(x, y)] ∙ yvec')"by simp ultimatelyhave"distinct([(x, y)] ∙ yvec')"using xvec'Dist by(rule_tac Suc) (assumption | simp)+ hence"distinct yvec'"by simp from Mem xEq have xSuppN: "x ∈ supp N"by simp from L ‹distinct xvec›‹xvec ♯* yvec›‹xvec ♯* M›‹xvec ♯* Q› have"(ν*yvec)M ≺' Q = (ν*xvec)([yvec xvec] ∙v M) ≺' ([yvec xvec] ∙v Q)" by(simp add: alphaBoundOutputChain'') with Eq have"N = [yvec xvec] ∙v M"by simp with xEq yEq have"N = [(y, x)] ∙ [yvec' xvec'] ∙v M" by simp with xSuppN have ySuppM: "y ∈ supp([yvec' xvec'] ∙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 ♯ yvec'" proof(simp add: fresh_def, rule notI) assume"y ∈ supp yvec'" hence"y mem yvec'" by(induct yvec') (auto simp add: supp_list_nil supp_list_cons supp_atm) moreoverfrom‹xvec ♯* M› xEq xFreshxvec' have"xvec' ♯* M"by simp ultimatelyhave"y ♯ [yvec' xvec'] ∙v M"using L' xvec'Freshyvec' xvec'Dist by(force intro: freshChainPerm) with ySuppM show"False"by(simp add: fresh_def) qed with‹distinct yvec'› yEq show ?caseby simp qed qed qed
lemma boundOutputDistinct: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi"
assumes"Ψ ⊳ P ⟼α ≺ P'"
shows"distinct(bn α)" using assms proof(nominal_induct Ψ P x3=="α ≺ P'" avoiding: α P' rule: semantics.strong_induct) case cInput thus ?caseby(simp add: residualInject) next caseOutput thus ?caseby(simp add: residualInject) next caseCase thus ?caseby(simp add: residualInject) next case cPar1 thus ?caseby(force intro: alphaDistinct boundOutputBindObject) next case cPar2 thus ?caseby(force intro: alphaDistinct boundOutputBindObject) next case cComm1 thus ?caseby(simp add: residualInject) next case cComm2 thus ?caseby(simp add: residualInject) next case(cOpen Ψ P M xvec yvec N P' x α P'') note‹M(ν*(xvec@x#yvec))⟨N⟩≺ P' = α ≺ P''› moreoverfrom‹xvec ♯* yvec›‹x ♯ xvec›‹x ♯ yvec›‹distinct xvec›‹distinct yvec› have"distinct(bn(M(ν*(xvec@x#yvec))⟨N⟩))" by auto (simp add: fresh_star_def fresh_def name_list_supp) moreover { fix y from‹Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'›‹x ∈ supp N›‹x ♯ xvec›‹x ♯ yvec›‹x ♯ M›‹x ♯ Ψ›‹distinct xvec›‹distinct yvec›‹xvec ♯* Ψ›‹xvec ♯* P›‹xvec ♯* M›‹xvec ♯* yvec›‹yvec ♯* Ψ›‹yvec ♯* P›‹yvec ♯* M› have"Ψ ⊳(νx)P ⟼M(ν*(xvec@x#yvec))⟨N⟩≺ P'"by(rule semantics.cOpen) moreovermoreoverfrom‹xvec ♯* M›‹x ♯ M›‹yvec ♯* M› have"bn(M(ν*(xvec@x#yvec))⟨N⟩) ♯* (subject(M(ν*(xvec@x#yvec))⟨N⟩))" by simp moreovernote‹distinct(bn(M(ν*(xvec@x#yvec))⟨N⟩))› moreoverassume"y ∈ set(bn(M(ν*(xvec@x#yvec))⟨N⟩))"
ultimatelyhave"y ∈ supp(object(M(ν*(xvec@x#yvec))⟨N⟩))" by(rule_tac boundOutputBindObject)
} moreoverfrom‹xvec ♯* α›‹x ♯ α›‹yvec ♯* α› have"bn(M(ν*(xvec@x#yvec))⟨N⟩) ♯* bn α"and"bn(M(ν*(xvec@x#yvec))⟨N⟩) ♯* object α"by simp+ moreoverfrom‹xvec ♯* P''›‹x ♯ P''›‹yvec ♯* P''› have"bn(M(ν*(xvec@x#yvec))⟨N⟩) ♯* P''"by simp ultimatelyshow ?caseby(rule alphaDistinct) next case cScope thus ?case by(rule_tac alphaDistinct, auto) (rule_tac boundOutputBindObject, auto) next case Bang thus ?caseby simp qed
lemma inputDistinct: fixes Ψ :: 'b and M :: 'a and xvec :: "name list" and N :: 'a and P :: "('a, 'b, 'c) psi" and Rs :: "('a, 'b, 'c) residual"
assumes"Ψ ⊳ M(λ*xvec N).P ⟼ Rs"
shows"distinct xvec" using assms by(nominal_induct Ψ P=="M(λ*xvec N).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 Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and yvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a → name list → 'a → ('a, 'b, 'c) psi → bool" and C :: "'d::fs_name"
assumes"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" and"xvec ♯* M" and rAlpha: "∧Ψ P M xvec N P' p C. [xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; xvec ♯* C; xvec ♯* (p ∙ xvec); set p ⊆ set xvec × set(p ∙ xvec); distinctPerm p; (p ∙ xvec) ♯* N; (p ∙ xvec) ♯* P'; Prop C Ψ P M xvec N P']==> Prop C Ψ P M (p ∙ xvec) (p ∙ N) (p ∙ P')" and rOutput: "∧Ψ M K N P C. [Ψ ⊨ M ↔ K]==> Prop C Ψ (M⟨N⟩.P) K ([]) N P" and rCase: "∧Ψ P M xvec N P' φ Cs C. [Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; ∧C. Prop C Ψ P M xvec N P'; (φ, P) mem Cs; Ψ ⊨ φ; guarded P]==> Prop C Ψ (Cases Cs) M xvec N P'" and rPar1: "∧Ψ ΨQ P M xvec N P' AQ Q C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P M xvec N P'; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* xvec; AQ♯* N; AQ♯* P'; AQ♯* C; xvec ♯* Q; xvec ♯* Ψ; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M xvec N (P' ∥ Q)" and rPar2: "∧Ψ ΨP Q M xvec N Q' AP P C. [Ψ ⊗ ΨP⊳ Q ⟼M(ν*xvec)⟨N⟩≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨP) Q M xvec N Q'; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* xvec; AP♯* N; AP♯* Q'; AP♯* C; xvec ♯* Q; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* P; xvec ♯* M; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M xvec N (P ∥ Q')" and rOpen: "∧Ψ P M xvec yvec N P' x C. [Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'; x ∈ supp N; ∧C. Prop C Ψ P M (xvec@yvec) N P'; x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ yvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; yvec ♯* Ψ; yvec ♯* P; yvec ♯* M; yvec ♯* C; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) M (xvec@x#yvec) N P'" and rScope: "∧Ψ P M xvec N P' x C. [Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; ∧C. Prop C Ψ P M xvec N P'; x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ N; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) M xvec N ((νx)P')" and rBang: "∧Ψ P M xvec N P' C. [Ψ ⊳ P ∥ !P ⟼M(ν*xvec)⟨N⟩≺ P'; guarded P; ∧C. Prop C Ψ (P ∥ !P) M xvec N P']==> Prop C Ψ (!P) M xvec N P'" shows"Prop C Ψ P M xvec N P'" proof - note‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'› moreoverfrom‹xvec ♯* M›have"bn(M(ν*xvec)⟨N⟩) ♯* subject(M(ν*xvec)⟨N⟩)"by simp moreoverfrom‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'›have"distinct(bn(M(ν*xvec)⟨N⟩))" by(rule boundOutputDistinct) ultimatelyshow ?thesis proof(nominal_induct Ψ P α=="M(ν*xvec)⟨N⟩" P' avoiding: C arbitrary: M xvec N rule: semanticsInduct) case(cAlpha Ψ P α P' p C M xvec N) from‹(p ∙ α) = M(ν*xvec)⟨N⟩›have"(p ∙ p ∙ α) = p ∙ (M(ν*xvec)⟨N⟩)" by(simp add: fresh_bij) with‹distinctPerm p›have A: "α = (p ∙ M)(ν*(p ∙ xvec))⟨(p ∙ N)⟩" by(simp add: eqvts) with‹bn α ♯* Ψ›‹bn α ♯* P›‹bn α ♯* subject α ›‹bn α ♯* C›‹bn α ♯* bn(p ∙ α)›‹distinctPerm p› have"(p ∙ xvec) ♯* Ψ"and"(p ∙ xvec) ♯* P"and"(p ∙ xvec) ♯* (p ∙ M)"and"(p ∙ xvec)♯* C"and"(p ∙ xvec) ♯* (p ∙ p ∙ xvec)" by auto moreoverfrom A ‹set p ⊆ set(bn α) × set(bn(p ∙ α))›‹distinctPerm p› have S: "set p ⊆ set(p ∙ xvec) × set(p ∙ p ∙ xvec)"by simp moreovernote‹distinctPerm p› moreoverfrom A ‹bn(p ∙ α) ♯* α›‹bn(p ∙ α) ♯* P'› have"(p ∙ p ∙ xvec) ♯* (p ∙ N)"and"(p ∙ p ∙ xvec) ♯* P'"by simp+ moreoverfrom A have"Prop C Ψ P (p ∙ M) (p ∙ xvec) (p ∙ N) P'" by(rule cAlpha) ultimatelyhave"Prop C Ψ P (p ∙ M) (p ∙ p ∙ xvec) (p ∙ p ∙ N) (p ∙ P')" by(rule rAlpha) moreoverfrom A ‹bn α ♯* subject α›have"(p ∙ xvec) ♯* (p ∙ M)"by simp hence"xvec ♯* M"by(simp add: fresh_star_bij) from A ‹bn(p ∙ α) ♯* α›‹distinctPerm p›have"xvec ♯* (p ∙ M)"by simp hence"(p ∙ xvec) ♯* (p ∙ p ∙ M)"by(simp add: fresh_star_bij) with‹distinctPerm p›have"(p ∙ xvec) ♯* M"by simp with‹xvec ♯* M› S ‹distinctPerm p›have"(p ∙ M) = M"by simp ultimatelyshow ?caseusing S ‹distinctPerm p›by simp next case cInput thus ?caseby(simp add: residualInject) next case cOutput thus ?caseby(force dest: rOutput simp add: action.inject) next case cCase thus ?caseby(force intro: rCase) next case cPar1 thus ?caseby(force intro: rPar1) next case cPar2 thus ?caseby(force intro: rPar2) next case cComm1 thus ?caseby(simp add: action.inject) next case cComm2 thus ?caseby(simp add: action.inject) next case cOpen thus ?caseby(fastforce intro: rOpen simp add: action.inject) next case cScope thus ?caseby(fastforce intro: rScope) next case cBang thus ?caseby(fastforce intro: rBang) qed qed
lemma inputInduct[consumes 1, case_names cInput cCase cPar1 cPar2 cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a → 'a → ('a, 'b, 'c) psi → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼M(N)≺ P'" and rInput: "∧Ψ M K xvec N Tvec P C. [Ψ ⊨ M ↔ K; distinct xvec; set xvec ⊆ supp N; length xvec = length Tvec; xvec ♯* Ψ; xvec ♯* M; xvec ♯* K; xvec ♯* C]==> Prop C Ψ (M(λ*xvec N).P) K (N[xvec::=Tvec]) (P[xvec::=Tvec])" and rCase: "∧Ψ P M N P' φ Cs C. [Ψ ⊳ P ⟼M(N)≺ P'; ∧C. Prop C Ψ P M N P'; (φ, P) mem Cs; Ψ⊨ φ; guarded P]==> Prop C Ψ (Cases Cs) M N P'" and rPar1: "∧Ψ ΨQ P M N P' AQ Q C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P M N P'; distinct AQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* N; AQ♯* P'; AQ♯* C]==> Prop C Ψ (P ∥ Q) M N (P' ∥ Q)" and rPar2: "∧Ψ ΨP Q M N Q' AP P C. [Ψ ⊗ ΨP⊳ Q ⟼M(N)≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨP) Q M N Q'; distinct AP; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* N; AP♯* Q'; AP♯* C]==> Prop C Ψ (P ∥ Q) M N (P ∥ Q')" and rScope: "∧Ψ P M N P' x C. [Ψ ⊳ P ⟼M(N)≺ P'; ∧C. Prop C Ψ P M N P'; x ♯ Ψ; x ♯ M; x ♯ N; x ♯ C]==> Prop C Ψ ((νx)P) M N ((νx)P')" and rBang: "∧Ψ P M N P' C. [Ψ ⊳ P ∥ !P ⟼M(N)≺ P'; guarded P; ∧C. Prop C Ψ (P ∥ !P) M N P']==> Prop C Ψ (!P) M N P'" shows"Prop C Ψ P M N P'" using Trans proof(nominal_induct Ψ P Rs=="M(N)≺ P'" avoiding: C arbitrary: P' rule: semantics.strong_induct) case(cInput Ψ M K xvec N Tvec P C) thus ?case by(force intro: rInput simp add: residualInject action.inject) next case(Output Ψ M K N P C) thus ?caseby(simp add: residualInject) next case(Case Ψ P Rs φ CS C) thus ?caseby(force intro: rCase) next case(cPar1 Ψ ΨQ P α P' Q AQ C P'') thus ?caseby(force intro: rPar1 simp add: residualInject) next case(cPar2 Ψ ΨP Q α Q' xvec P C Q'') thus ?caseby(force intro: rPar2 simp add: residualInject) next case(cComm1 Ψ ΨQ P M N P' xvec ΨP Q K zvec Q' yvec C PQ) thus ?caseby(simp add: residualInject) next case(cComm2 Ψ ΨQ P M zvec N P' xvec ΨP Q K yvec Q' C PQ) thus ?caseby(simp add: residualInject) next case(cOpen Ψ P M xvec N P' x yvec C P'') thus ?caseby(simp add: residualInject) next case(cScope Ψ P α P' x C P'') thus ?caseby(force intro: rScope simp add: residualInject) next case(Bang Ψ P Rs C) thus ?caseby(force intro: rBang) qed
lemma tauInduct[consumes 1, case_names cCase cPar1 cPar2 cComm1 cComm2 cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and Rs :: "('a, 'b, 'c) residual" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼τ ≺ P'" and rCase: "∧Ψ P P' φ Cs C. [Ψ ⊳ P ⟼τ ≺ P'; ∧C. Prop C Ψ P P'; (φ, P) mem Cs; Ψ ⊨ φ; guarded P]==> Prop C Ψ (Cases Cs) P'" and rPar1: "∧Ψ ΨQ P P' AQ Q C. [Ψ ⊗ ΨQ⊳ P ⟼τ ≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P P'; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* P'; AQ♯* C]==> Prop C Ψ (P ∥ Q) (P' ∥ Q)" and rPar2: "∧Ψ ΨP Q Q' AP P C. [Ψ ⊗ ΨP⊳ Q ⟼τ ≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨP) Q Q'; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* Q'; AP♯* C]==> Prop C Ψ (P ∥ Q) (P ∥ Q')" and rComm1: "∧Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(ν*xvec)⟨N⟩≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) ((ν*xvec)(P' ∥ Q'))" and rComm2: "∧Ψ ΨQ P M xvec N P' AP ΨP Q K Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) ((ν*xvec)(P' ∥ Q'))" and rScope: "∧Ψ P P' x C. [Ψ ⊳ P ⟼τ ≺ P'; ∧C. Prop C Ψ P P'; x ♯ Ψ; x ♯ C]==> Prop C Ψ ((νx)P) ((νx)P')" and rBang: "∧Ψ P P' C. [Ψ ⊳ P ∥ !P ⟼τ ≺ P'; guarded P; ∧C. Prop C Ψ (P ∥ !P) P']==> Prop C Ψ (!P) P'" shows"Prop C Ψ P P'" using Trans proof(nominal_induct Ψ P Rs=="τ ≺ P'" avoiding: C arbitrary: P' rule: semantics.strong_induct) case(cInput M K xvec N Tvec P C) thus ?caseby(simp add: residualInject) next case(Output Ψ M K N P C) thus ?caseby(simp add: residualInject) next case(Case Ψ P Rs φ Cs C) thus ?caseby(force intro: rCase simp add: residualInject) next case(cPar1 Ψ ΨQ P α P' AQ Q C P'') thus ?caseby(force intro: rPar1 simp add: residualInject) next case(cPar2 Ψ ΨP Q α Q' AP P C Q'') thus ?caseby(force intro: rPar2 simp add: residualInject) next case(cComm1 Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ C PQ) thus ?caseby(force intro: rComm1 simp add: residualInject) next case(cComm2 Ψ ΨQ P M xvec N P' AP ΨP Q' AQ C PQ) thus ?caseby(force intro: rComm2 simp add: residualInject) next case(cOpen Ψ P M xvec N P' x yvec C P'') thus ?caseby(simp add: residualInject) next case(cScope Ψ P α P' x C P'') thus ?caseby(force intro: rScope simp add: residualInject) next case(Bang Ψ P Rs C ) thus ?caseby(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 Ψ :: 'b and P :: "('a, 'b, 'c) psi" and Rs :: "('a, 'b, 'c) residual" and AP :: "name list" and ΨP :: 'b andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) residual → name list → 'b → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼ Rs" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and rAlpha: "∧Ψ P AP ΨP p Rs C. [AP♯* Ψ; AP♯* P; AP♯* (p ∙ AP); AP♯* Rs; AP♯* C; set p ⊆ set AP× set(p ∙ AP); distinctPerm p; Prop C Ψ P Rs AP ΨP]==> Prop C Ψ P Rs (p ∙ AP) (p ∙ ΨP)" and rInput: "∧Ψ M K xvec N Tvec P C. [Ψ ⊨ M ↔ K; distinct xvec; set xvec ⊆ supp N; length xvec = length Tvec; xvec ♯* Ψ; xvec ♯* M; xvec ♯* K; xvec ♯* C]==> Prop C Ψ (M(λ*xvec N).P) (K((N[xvec::=Tvec]))≺ (P[xvec::=Tvec])) ([]) (1)" and rOutput: "∧Ψ M K N P C. Ψ ⊨ M ↔ K ==> Prop C Ψ (M⟨N⟩.P) (K⟨N⟩≺ P) ([]) (1)" and rCase: "∧Ψ P Rs φ Cs AP ΨP C. [Ψ ⊳ P ⟼ Rs; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P Rs AP ΨP; (φ, P) mem Cs; Ψ ⊨ φ; guarded P; ΨP≃1; (supp ΨP) = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* Rs; AP♯* C]==> Prop C Ψ (Cases Cs) Rs ([]) (1)" and rPar1: "∧Ψ ΨQ P α P' AQ Q AP ΨP C. [Ψ ⊗ ΨQ⊳ P ⟼α ≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P (α ≺ P') AP ΨP; distinct(bn α); AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* α; AP♯* P'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* α; AQ♯* P'; AQ♯* ΨP; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; bn α ♯* subject α; bn α ♯* ΨP; bn α ♯* ΨQ; AP♯* C; AQ♯* C; bn α ♯* C]==> Prop C Ψ (P ∥ Q) (α ≺ (P' ∥ Q)) (AP@AQ) (ΨP⊗ ΨQ)" and rPar2: "∧Ψ ΨP Q α Q' AP P AQ ΨQ C. [Ψ ⊗ ΨP⊳ Q ⟼α ≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨP) Q (α ≺ Q') AQ ΨQ; distinct(bn α); AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* α; AP♯* Q'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* α; AQ♯* Q'; AQ♯* ΨP; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; bn α ♯* subject α; bn α ♯* ΨP; bn α ♯* ΨQ; AP♯* C; AQ♯* C; bn α ♯* C]==> Prop C Ψ (P ∥ Q) (α ≺ (P ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rComm1: "∧Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨQ) P ((M(N)) ≺ P') AP ΨP; Ψ ⊗ ΨP⊳ Q ⟼K(ν*xvec)⟨N⟩≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; ∧C. Prop C (Ψ ⊗ ΨP) Q (K(ν*xvec)⟨N⟩≺ Q') AQ ΨQ; distinct xvec; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) (τ ≺(ν*xvec)(P' ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rComm2: "∧Ψ ΨQ P M xvec N P' AP ΨP Q K Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C (Ψ ⊗ ΨQ) P (M(ν*xvec)⟨N⟩≺ P') AP ΨP; Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨP) Q (K(N)≺ Q') AQ ΨQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; distinct xvec; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) (τ ≺(ν*xvec)(P' ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rOpen: "∧Ψ P M xvec yvec N P' x AP ΨP C. [Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P (M(ν*(xvec@yvec))⟨N⟩≺ P') AP ΨP; x ∈ supp N; x ♯ Ψ; x ♯ M; x ♯ AP; x ♯ xvec; x ♯ yvec; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* xvec; AP♯* yvec; xvec ♯* yvec; distinct xvec; distinct yvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; xvec ♯* ΨP; yvec ♯* ΨP; yvec ♯* Ψ; yvec ♯* P; yvec ♯* M; AP♯* C; x ♯ C; xvec ♯* C; yvec ♯* C]==> Prop C Ψ ((νx)P) (M(ν*(xvec@x#yvec))⟨N⟩≺ P') (x#AP) ΨP" and rScope: "∧Ψ P α P' x AP ΨP C. [Ψ ⊳ P ⟼α ≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P (α ≺ P') AP ΨP; x ♯ Ψ; x ♯ α; x ♯ AP; AP♯* Ψ; AP♯* P; AP♯* α; AP♯* P'; distinct(bn α); bn α ♯* Ψ; bn α ♯* P; bn α ♯* subject α; bn α ♯* ΨP; AP♯* C; x ♯ C; bn α ♯* C]==> Prop C Ψ ((νx)P) (α ≺ ((νx)P')) (x#AP) ΨP" and rBang: "∧Ψ P Rs AP ΨP C. [Ψ ⊳ P ∥ !P ⟼ Rs; guarded P; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ (P ∥ !P) Rs AP (ΨP⊗1); ΨP≃1; supp ΨP = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* Rs; AP♯* C]==> Prop C Ψ (!P) Rs ([]) (1)" shows"Prop C Ψ P Rs AP ΨP" using Trans FrP ‹distinct AP› proof(nominal_induct avoiding: AP ΨP C rule: semantics.strong_induct) case(cInput Ψ M K xvec N Tvec P AP ΨP C) from‹extractFrame (M(λ*xvec N).P) = ⟨AP, ΨP⟩› have"AP = []"and"ΨP = 1" by auto with‹Ψ ⊨ M ↔ K›‹distinct xvec›‹set xvec ⊆ supp N›‹length xvec = length Tvec› ‹xvec ♯* Ψ›‹xvec ♯* M›‹xvec ♯* K›‹xvec ♯* C› show ?caseby(blast intro: rInput) next case(Output Ψ M K N P AP ΨP) from‹extractFrame (M⟨N⟩.P) = ⟨AP, ΨP⟩› have"AP = []"and"ΨP = 1" by auto with‹Ψ ⊨ M ↔ K›show ?case by(blast intro: rOutput) next case(Case Ψ P Rs φ Cs AcP ΨcP C) obtain AP ΨPwhere FrP: "extractFrame P = ⟨AP, ΨP⟩"and"distinct AP" and"AP♯* (Ψ, P, Rs, C)" by(rule freshFrame) hence"AP♯* Ψ"and"AP♯* P"and"AP♯* Rs"and"AP♯* C" by simp+ note‹Ψ ⊳ P ⟼ Rs› FrP ‹distinct AP› moreoverfrom FrP ‹distinct AP›‹∧AP ΨP C. [extractFrame P = ⟨AP, ΨP⟩; distinct AP]==> Prop C Ψ P Rs AP ΨP› have"∧C. Prop C Ψ P Rs AP ΨP"by simp moreovernote‹(φ, P) mem Cs›‹Ψ ⊨ φ›‹guarded P› moreoverfrom‹guarded P› FrP have"ΨP≃1"and"supp ΨP = ({}::name set)"by(metis guardedStatEq)+ moreovernote‹AP♯* Ψ›‹AP♯* P›‹AP♯* Rs›‹AP♯* C› ultimatelyhave"Prop C Ψ (Cases Cs) Rs ([]) (1)" by(rule rCase) thus ?caseusing‹extractFrame(Cases Cs) = ⟨AcP, ΨcP⟩›by simp next case(cPar1 Ψ ΨQ P α P' Q AQ APQ ΨPQ C) obtain AP ΨPwhere FrP: "extractFrame P = ⟨AP, ΨP⟩"and"distinct AP" "AP♯* (P, Q, Ψ, α, P', AQ, APQ, C, ΨQ)" by(rule freshFrame) hence"AP♯* P"and"AP♯* Q"and"AP♯* Ψ"and"AP♯* α"and"AP♯* P'" and"AP♯* AQ"and"AP♯* APQ"and"AP♯* C"and"AP♯* ΨQ" by simp+
moreoverfrom FrP ‹distinct AP›‹∧AP ΨP C. [extractFrame P = ⟨AP, ΨP⟩; distinct AP]==> Prop C (Ψ ⊗ ΨQ) P (α ≺ P') AP ΨP› have"∧C. Prop C (Ψ ⊗ ΨQ) P (α ≺ P') AP ΨP"by simp
lemma inputFrameInduct[consumes 3, case_names cAlpha cInput cCase cPar1 cPar2 cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a → 'a → ('a, 'b, 'c) psi → name list → 'b → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼M(N)≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and rAlpha: "∧Ψ P M N P' AP ΨP p C. [AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* (p ∙ AP); AP♯* C; set p ⊆ set AP× set(p ∙ AP); distinctPerm p; Prop C Ψ P M N P' AP ΨP]==> Prop C Ψ P M N P' (p ∙ AP) (p ∙ ΨP)" and rInput: "∧Ψ M K xvec N Tvec P C. [Ψ ⊨ M ↔ K; distinct xvec; set xvec ⊆ supp N; length xvec = length Tvec; xvec ♯* Ψ; xvec ♯* M; xvec ♯* K; xvec ♯* C]==> Prop C Ψ (M(λ*xvec N).P) K (N[xvec::=Tvec]) (P[xvec::=Tvec]) ([]) (1)" and rCase: "∧Ψ P M N P' φ Cs AP ΨP C. [Ψ ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P M N P' AP ΨP; (φ, P) mem Cs; Ψ ⊨ φ; guarded P; ΨP≃1; (supp ΨP) = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* C]==> Prop C Ψ (Cases Cs) M N P' ([]) (1)" and rPar1: "∧Ψ ΨQ P M N P' AQ Q AP ΨP C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P M N P' AP ΨP; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* N; AP♯* P'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* N; AQ♯* P'; AQ♯* ΨP; AP♯* C; AQ♯* C]==> Prop C Ψ (P ∥ Q) M N (P' ∥ Q) (AP@AQ) (ΨP⊗ ΨQ)" and rPar2: "∧Ψ ΨP Q M N Q' AP P AQ ΨQ C. [Ψ ⊗ ΨP⊳ Q ⟼M(N)≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨP) Q M N Q' AQ ΨQ; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* N; AP♯* Q'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* N; AQ♯* Q'; AQ♯* ΨP; AP♯* C; AQ♯* C]==> Prop C Ψ (P ∥ Q) M N (P ∥ Q') (AP@AQ) (ΨP⊗ ΨQ)" and rScope: "∧Ψ P M N P' x AP ΨP C. [Ψ ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P M N P' AP ΨP; x ♯ Ψ; x ♯ M; x ♯ N; x ♯ AP; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* C; x ♯ C]==> Prop C Ψ ((νx)P) M N ((νx)P') (x#AP) ΨP" and rBang: "∧Ψ P M N P' AP ΨP C. [Ψ ⊳ P ∥ !P ⟼M(N)≺ P'; guarded P; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ (P ∥ !P) M N P' AP (ΨP⊗1); ΨP≃1; (supp ΨP) = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* C]==> Prop C Ψ (!P) M N P' ([]) (1)" shows"Prop C Ψ P M N P' AP ΨP" using assms by(nominal_induct Ψ P Rs=="M(N)≺ P'" AP ΨP avoiding: C arbitrary: P' rule: semanticsFrameInduct)
(auto simp add: residualInject)
lemma outputFrameInduct[consumes 3, case_names cAlpha cOutput cCase cPar1 cPar2 cOpen cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" and AP :: "name list" and ΨP :: 'b andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → 'a → ('a, 'b, 'c) boundOutput → name list → 'b → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼ROut M B" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and rAlpha: "∧Ψ P M AP ΨP p B C. [AP♯* Ψ; AP♯* P; AP♯* M; AP♯* (p ∙ AP); AP♯* B; AP♯* C; set p ⊆ set AP× set(p ∙ AP); distinctPerm p; Prop C Ψ P M B AP ΨP]==> Prop C Ψ P M B (p ∙ AP) (p ∙ ΨP)" and rOutput: "∧Ψ M K N P C. Ψ ⊨ M ↔ K ==> Prop C Ψ (M⟨N⟩.P) K (N ≺' P) ([]) (1)" and rCase: "∧Ψ P M B φ Cs AP ΨP C. [Ψ ⊳ P ⟼(ROut M B); extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P M B AP ΨP; (φ, P) mem Cs; Ψ ⊨ φ; guarded P; ΨP≃1; (supp ΨP) = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* M; AP♯* B; AP♯* C]==> Prop C Ψ (Cases Cs) M B ([]) (1)" and rPar1: "∧Ψ ΨQ P M xvec N P' AQ Q AP ΨP C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P M ((ν*xvec)N ≺' P') AP ΨP; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* xvec; AP♯* N; AP♯* P'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* xvec; AQ♯* N; AQ♯* P'; AQ♯* ΨP; xvec ♯* Ψ; xvec ♯* P; xvec ♯* Q; xvec ♯* M; xvec ♯* ΨP; xvec ♯* ΨQ; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M ((ν*xvec)N ≺' (P' ∥ Q)) (AP@AQ) (ΨP⊗ ΨQ)" and rPar2: "∧Ψ ΨP Q M xvec N Q' AP P AQ ΨQ C. [Ψ ⊗ ΨP⊳ Q ⟼M(ν*xvec)⟨N⟩≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨP) Q M ((ν*xvec)N ≺' Q') AQ ΨQ; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* M; AP♯* xvec; AP♯* N; AP♯* Q'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* M; AQ♯* xvec; AQ♯* N; AQ♯* Q'; AQ♯* ΨP; xvec ♯* Ψ; xvec ♯* P; xvec ♯* Q; xvec ♯* M; xvec ♯* ΨP; xvec ♯* ΨQ; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) M ((ν*xvec)N ≺' (P ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rOpen: "∧Ψ P M xvec yvec N P' x AP ΨP C. [Ψ ⊳ P ⟼M(ν*(xvec@yvec))⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P M ((ν*(xvec@yvec))N ≺' P') AP ΨP; x ∈ supp N; x ♯ Ψ; x ♯ M; x ♯ AP; x ♯ xvec; x ♯ yvec; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* xvec; AP♯* yvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; xvec ♯* ΨP; yvec ♯* Ψ; yvec ♯* P; yvec ♯* M; AP♯* C; x ♯ C; xvec ♯* C; yvec ♯* C]==> Prop C Ψ ((νx)P) M ((ν*(xvec@x#yvec))N ≺' P') (x#AP) ΨP" and rScope: "∧Ψ P M xvec N P' x AP ΨP C. [Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P M ((ν*xvec)N ≺' P') AP ΨP; x ♯ Ψ; x ♯ M; x ♯ xvec; x ♯ N; x ♯ AP; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* xvec; xvec ♯* Ψ; xvec ♯* P; xvec ♯* M; xvec ♯* ΨP; AP♯* C; x ♯ C; xvec ♯* C]==> Prop C Ψ ((νx)P) M ((ν*xvec)N ≺' ((νx)P')) (x#AP) ΨP" and rBang: "∧Ψ P M B AP ΨP C. [Ψ ⊳ P ∥ !P ⟼ROut M B; guarded P; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ (P ∥ !P) M B AP (ΨP⊗1); ΨP≃1; supp ΨP = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* M; AP♯* C]==> Prop C Ψ (!P) M B ([]) (1)" shows"Prop C Ψ P M B AP ΨP" proof -
{ fix B assume"Ψ ⊳ P ⟼ROut M B" hence"Prop C Ψ P M B AP ΨP"using FrP ‹distinct AP› proof(nominal_induct Ψ P Rs=="ROut M B" AP ΨP avoiding: C arbitrary: B rule: semanticsFrameInduct) case cAlpha thus ?caseby(fastforce intro: rAlpha) next case cInput thus ?caseby(simp add: residualInject) next case cOutput thus ?caseby(force intro: rOutput simp add: residualInject) next case cCase thus ?caseby(force intro: rCase simp add: residualInject) next case cPar1 thus ?case by(fastforce intro: rPar1 simp add: residualInject) next case cPar2 thus ?case by(fastforce intro: rPar2 simp add: residualInject) next case cComm1 thus ?caseby(simp add: residualInject) next case cComm2 thus ?caseby(simp add: residualInject) next case cOpen thus ?caseby(fastforce intro: rOpen simp add: residualInject) next case cScope thus ?caseby(force intro: rScope simp add: residualInject) next case cBang thus ?caseby(force intro: rBang simp add: residualInject) qed
} with Trans show ?thesis by(simp add: residualInject) qed
lemma tauFrameInduct[consumes 3, case_names cAlpha cCase cPar1 cPar2 cComm1 cComm2 cScope cBang]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and P' :: "('a, 'b, 'c) psi" andProp :: "'d::fs_name → 'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi → name list → 'b → bool" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ⟼τ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and rAlpha: "∧Ψ P P' AP ΨP p C. [AP♯* Ψ; AP♯* P; AP♯* P'; AP♯* (p ∙ AP); AP♯* C; set p ⊆ set AP× set (p ∙ AP); distinctPerm p; Prop C Ψ P P' AP ΨP]==> Prop C Ψ P P' (p ∙ AP) (p ∙ ΨP)" and rCase: "∧Ψ P P' φ Cs AP ΨP C. [Ψ ⊳ P ⟼τ ≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P P' AP ΨP; (φ, P) mem Cs; Ψ ⊨ φ; guarded P; ΨP≃1; (supp ΨP) = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* P'; AP♯* C]==> Prop C Ψ (Cases Cs) P' ([]) (1)" and rPar1: "∧Ψ ΨQ P P' AQ Q AP ΨP C. [Ψ ⊗ ΨQ⊳ P ⟼τ ≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨQ) P P' AP ΨP; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* P'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* P'; AQ♯* ΨP; AP♯* C; AQ♯* C]==> Prop C Ψ (P ∥ Q) (P' ∥ Q) (AP@AQ) (ΨP⊗ ΨQ)" and rPar2: "∧Ψ ΨP Q Q' AP P AQ ΨQ C. [Ψ ⊗ ΨP⊳ Q ⟼τ ≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; ∧C. Prop C (Ψ ⊗ ΨP) Q Q' AQ ΨQ; AP♯* P; AP♯* Q; AP♯* Ψ; AP♯* Q'; AP♯* AQ; AP♯* ΨQ; AQ♯* P; AQ♯* Q; AQ♯* Ψ; AQ♯* Q'; AQ♯* ΨP; AP♯* C; AQ♯* C]==> Prop C Ψ (P ∥ Q) (P ∥ Q') (AP@AQ) (ΨP⊗ ΨQ)" and rComm1: "∧Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(ν*xvec)⟨N⟩≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; distinct xvec; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) ((ν*xvec)(P' ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rComm2: "∧Ψ ΨQ P M xvec N P' AP ΨP Q K Q' AQ C. [Ψ ⊗ ΨQ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K; distinct xvec; AP♯* Ψ; AP♯* ΨQ; AP♯* P; AP♯* M; AP♯* N; AP♯* P'; AP♯* Q; AP♯* Q'; AP♯* AQ; AP♯* xvec; AQ♯* Ψ; AQ♯* ΨP; AQ♯* P; AQ♯* N; AQ♯* P'; AQ♯* Q; AQ♯* K; AQ♯* Q'; AQ♯* xvec; xvec ♯* Ψ; xvec ♯* ΨP; xvec ♯* ΨQ; xvec ♯* P; xvec ♯* M; xvec ♯* Q; xvec ♯* K; AP♯* C; AQ♯* C; xvec ♯* C]==> Prop C Ψ (P ∥ Q) ((ν*xvec)(P' ∥ Q')) (AP@AQ) (ΨP⊗ ΨQ)" and rScope: "∧Ψ P P' x AP ΨP C. [Ψ ⊳ P ⟼τ ≺ P'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ P P' AP ΨP; x ♯ Ψ; x ♯ AP; AP♯* Ψ; AP♯* P; AP♯* P'; AP♯* C; x ♯ C]==> Prop C Ψ ((νx)P) ((νx)P') (x#AP) ΨP" and rBang: "∧Ψ P P' AP ΨP C. [Ψ ⊳ P ∥ !P ⟼τ ≺ P'; guarded P; extractFrame P = ⟨AP, ΨP⟩; distinct AP; ∧C. Prop C Ψ (P ∥ !P) P' AP (ΨP⊗1); ΨP≃1; supp ΨP = ({}::name set); AP♯* Ψ; AP♯* P; AP♯* P'; AP♯* C]==> Prop C Ψ (!P) P' ([]) (1)" shows"Prop C Ψ P P' AP ΨP" using Trans FrP ‹distinct AP› proof(nominal_induct Ψ P Rs=="τ ≺ P'" AP ΨP avoiding: C arbitrary: P' rule: semanticsFrameInduct) case cAlpha thus ?caseby(force intro: rAlpha simp add: residualInject) next case cInput thus ?caseby(simp add: residualInject) next case cOutput thus ?caseby(simp add: residualInject) next case cCase thus ?caseby(force intro: rCase simp add: residualInject) next case cPar1 thus ?caseby(force intro: rPar1 simp add: residualInject) next case cPar2 thus ?caseby(force intro: rPar2 simp add: residualInject) next case cComm1 thus ?caseby(force intro: rComm1 simp add: residualInject) next case cComm2 thus ?caseby(force intro: rComm2 simp add: residualInject) next case cOpen thus ?caseby(simp add: residualInject) next case cScope thus ?caseby(force intro: rScope simp add: residualInject) next case cBang thus ?caseby(force intro: rBang simp add: residualInject) qed
lemma inputFreshDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and"x ♯ P" and"x ♯ N"
shows"x ♯ P'" proof - have"bn(M(N)) ♯* subject(M(N))"and"distinct(bn(M(N)))"by simp+ with‹Ψ ⊳ P ⟼M(N)≺ P'›show ?thesis using‹x ♯ P›‹x ♯ N› proof(nominal_induct Ψ P α=="M(N)" P' avoiding: x rule: semanticsInduct) case(cAlpha Ψ P α P' p x) thus ?caseby simp next case(cInput Ψ M' K xvec N' Tvec P x) from‹K((N'[xvec::=Tvec])) = M(N)›have"M = K"and NeqN': "N = N'[xvec::=Tvec]"by(simp add: action.inject)+ note‹length xvec = length Tvec›‹distinct xvec›then moreoverhave"x ♯ Tvec"using‹set xvec ⊆ supp N'›‹x ♯ N› NeqN' by(blast intro: substTerm.subst3) moreoverfrom‹xvec ♯* x›‹x ♯ M'(λ*xvec N').P› have"x ♯ P"by(simp add: inputChainFresh) (simp add: name_list_supp fresh_def) ultimatelyshow ?caseusing‹xvec ♯* x›by auto next case(cOutput Ψ M K N P x) thus ?caseby simp next case(cCase Ψ P P' φ Cs x) thus ?caseby(induct Cs, auto) next case(cPar1 Ψ ΨQ P P' xvec Q x) thus ?caseby simp next case(cPar2 Ψ ΨP Q Q' xvec P x) thus ?caseby simp next case(cComm1 Ψ ΨQ P M N P' AP ΨP Q K xvec Q' AQ x) thus ?caseby simp next case(cComm2 Ψ ΨQ P M xwec N P' AP ΨP Q K Q' AQ x) thus ?caseby simp next case(cOpen Ψ P M xvec yvec N P' x y) thus ?caseby simp next case(cScope Ψ P P' x y) thus ?caseby(simp add: abs_fresh) next case(cBang Ψ P P' x) thus ?caseby simp qed qed
lemma inputFreshChainDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and xvec :: "name list"
shows"xvec ♯* P'" using assms by(induct xvec)
(auto intro: inputFreshDerivative)
lemma outputFreshDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name
shows"x ♯ N" and"x ♯ P'" proof - note‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'› moreoverfrom‹xvec ♯* M›have"bn(M(ν*xvec)⟨N⟩) ♯* subject(M(ν*xvec)⟨N⟩)"by simp moreoverfrom‹distinct xvec›have"distinct(bn(M(ν*xvec)⟨N⟩))"by simp ultimatelyshow"x ♯ N"using‹x ♯ P›‹x ♯ xvec› proof(nominal_induct Ψ P α=="M(ν*xvec)⟨N⟩" P' avoiding: x arbitrary: M xvec N rule: semanticsInduct) case(cAlpha Ψ P α P' p x M xvec N) have S: "set p ⊆ set(bn α) × set(bn(p ∙ α))"by fact from‹(p ∙ α) = M(ν*xvec)⟨N⟩›have"(p ∙ p ∙ α) = p ∙ (M(ν*xvec)⟨N⟩)"by(simp add: fresh_star_bij) with‹distinctPerm p›have"α = (p ∙ M)(ν*(p ∙ xvec))⟨(p ∙ N)⟩"by simp moreoverfrom‹(p ∙ α) = M(ν*xvec)⟨N⟩›‹x ♯ xvec›have"x ♯ (bn(p ∙ α))"by simp with‹(bn α) ♯* x›‹x ♯ xvec› S have"x ♯ (p ∙ xvec)" by(drule_tac pt_fresh_bij1[OF pt_name_inst, OF at_name_inst, where pi=p and x=xvec]) simp ultimatelyhave"x ♯ (p ∙ N)"using‹x ♯ P›by(rule_tac cAlpha) hence"(p ∙ x) ♯ (p ∙ p ∙ N)"by(simp add: pt_fresh_bij1[OF pt_name_inst, OF at_name_inst]) with‹distinctPerm p›‹bn(α) ♯* x›‹x ♯ (bn(p ∙ α))›S show ?caseby simp next case cInput thus ?caseby simp next case cOutput thus ?caseby(simp add: action.inject) next case cCase thus ?case by(rule_tac cCase) (auto dest: memFresh) next case cPar1 thus ?caseby simp next case cPar2 thus ?caseby simp next case cComm1 thus ?caseby simp next case cComm2 thus ?caseby simp next case(cOpen Ψ P M xvec yvec N P' x y M' zvec N') from‹M(ν*(xvec@x#yvec))⟨N⟩ = M'(ν*zvec)⟨N'⟩›have"zvec = xvec@x#yvec"and"N = N'" by(simp add: action.inject)+ from‹y ♯(νx)P›‹x ♯ y›have"y ♯ P"by(simp add: abs_fresh) moreoverfrom‹y ♯ zvec›‹zvec = xvec@x#yvec›have "y ♯ (xvec@yvec)" by simp ultimatelyhave"y ♯ N"by(rule_tac cOpen) auto with‹N = N'›show ?caseby simp next case cScope thus ?caseby(auto simp add: abs_fresh) next case cBang thus ?caseby simp qed next note‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'› moreoverfrom‹xvec ♯* M›have"bn(M(ν*xvec)⟨N⟩) ♯* subject(M(ν*xvec)⟨N⟩)"by simp moreoverfrom‹distinct xvec›have"distinct(bn(M(ν*xvec)⟨N⟩))"by simp ultimatelyshow"x ♯ P'"using‹x ♯ P›‹x ♯ xvec› proof(nominal_induct Ψ P α=="M(ν*xvec)⟨N⟩" P' avoiding: x arbitrary: M xvec N rule: semanticsInduct) case(cAlpha Ψ P α P' p x M xvec N) have S: "set p ⊆ set(bn α) × set(bn(p ∙ α))"by fact from‹(p ∙ α) = M(ν*xvec)⟨N⟩›have"(p ∙ p ∙ α) = p ∙ (M(ν*xvec)⟨N⟩)"by(simp add: fresh_star_bij) with‹distinctPerm p›have"α = (p ∙ M)(ν*(p ∙ xvec))⟨(p ∙ N)⟩"by simp moreoverfrom‹(p ∙ α) = M(ν*xvec)⟨N⟩›‹x ♯ xvec›have"x ♯ (bn(p ∙ α))"by simp with‹(bn α) ♯* x›‹x ♯ xvec› S have"x ♯ (p ∙ xvec)" by(drule_tac pt_fresh_bij1[OF pt_name_inst, OF at_name_inst, where pi=p and x=xvec]) simp ultimatelyhave"x ♯ P'"using‹x ♯ P›by(rule_tac cAlpha) hence"(p ∙ x) ♯ (p ∙ P')"by(simp add: pt_fresh_bij1[OF pt_name_inst, OF at_name_inst]) with‹distinctPerm p›‹bn(α) ♯* x›‹x ♯ (bn(p ∙ α))›S show ?caseby simp next case cInput thus ?caseby simp next case cOutput thus ?caseby(simp add: action.inject) next case cCase thus ?caseby(fastforce simp add: action.inject dest: memFresh) next case cPar1 thus ?caseby simp next case cPar2 thus ?caseby simp next case cComm1 thus ?caseby simp next case cComm2 thus ?caseby simp next case(cOpen Ψ P M xvec yvec N P' x y M' zvec N') from‹M(ν*(xvec@x#yvec))⟨N⟩ = M'(ν*zvec)⟨N'⟩›have"zvec = xvec@x#yvec" by(simp add: action.inject) from‹y ♯(νx)P›‹x ♯ y›have"y ♯ P"by(simp add: abs_fresh) moreoverfrom‹y ♯ zvec›‹zvec = xvec@x#yvec›have "y ♯ (xvec@yvec)" by simp ultimatelyshow"y ♯ P'"by(rule_tac cOpen) auto next case cScope thus ?caseby(auto simp add: abs_fresh) next case cBang thus ?caseby simp qed qed
lemma outputFreshChainDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and yvec :: "name list"
lemma tauFreshDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and P' :: "('a, 'b, 'c) psi" and x :: name
assumes"Ψ ⊳ P ⟼τ ≺ P'" and"x ♯ P"
shows"x ♯ P'" proof - have"bn(τ) ♯* subject(τ)"and"distinct(bn(τ))"by simp+ with‹Ψ ⊳ P ⟼τ ≺ P'›show ?thesis using‹x ♯ P› proof(nominal_induct Ψ P α=="(τ::('a action))" P' avoiding: x rule: semanticsInduct) case cAlpha thus ?caseby simp next case cInput thus ?caseby simp next case cOutput thus ?caseby simp next case cCase thus ?caseby(auto dest: memFresh) next case cPar1 thus ?caseby simp next case cPar2 thus ?caseby simp next case cComm1 thus ?case by(fastforce dest: inputFreshDerivative outputFreshDerivative simp add: resChainFresh) next case cComm2 thus ?case by(fastforce dest: inputFreshDerivative outputFreshDerivative simp add: resChainFresh) next case cOpen thus ?caseby simp next case cScope thus ?caseby(simp add: abs_fresh) next case cBang thus ?caseby simp qed qed
lemma tauFreshChainDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and xvec :: "name list"
assumes"Ψ ⊳ P ⟼τ ≺ P'" and"xvec ♯* P"
shows"xvec ♯* P'" using assms by(induct xvec) (auto intro: tauFreshDerivative)
lemma freeFreshDerivative: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi" and x :: name
shows"α ≺ P = (p ∙ α) ≺ (p ∙ P)" using assms apply(rule_tac α=α in actionCases) apply(simp only: eqvts bn.simps) apply simp apply(simp add: boundOutputChainAlpha'' residualInject) by simp
lemma Par1: fixes Ψ :: 'b and ΨQ :: 'b and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi" and AQ :: "name list" and Q :: "('a, 'b, 'c) psi"
thus ?thesis using‹bn(q ∙ α) ♯* α›‹bn(q ∙ α) ♯* Q'›‹bn α ♯* subject α›‹bn(q ∙ α) ♯* P›‹bn α ♯* P› Sq by(force simp add: residualAlpha) qed
} note Goal = this from‹extractFrame P = ⟨AP, ΨP⟩›‹AP♯* Ψ›‹AP♯* Q›‹AP♯* α› obtain AP' where FrP: "extractFrame P = ⟨AP', ΨP⟩"and"distinct AP'"and"AP' ♯* Ψ"and"AP' ♯* Q"and"AP' ♯* α" by(rule_tac C="(Ψ, Q, α)"in distinctFrame) auto show ?thesis proof(induct rule: actionCases[where α=α]) case(cInput M N) from Trans FrP ‹AP' ♯* Ψ›‹AP' ♯* Q›‹AP' ♯* α›‹distinct AP'›‹bn α ♯* P› show ?caseusing‹α = M(N)›by(force intro: Goal) next case cTau from Trans FrP ‹AP' ♯* Ψ›‹AP' ♯* Q›‹AP' ♯* α›‹distinct AP'›‹bn α ♯* P› show ?caseusing‹α = τ›by(force intro: Goal) next case(cOutput M xvec N) from‹α = M(ν*xvec)⟨N⟩›‹AP' ♯* α›‹bn α ♯* P›have"xvec ♯* AP'"and"xvec ♯* P" by simp+ obtain p where"(p ∙ xvec) ♯* N"and"(p ∙ xvec) ♯* Q'"and"(p ∙ xvec) ♯* P" and"(p ∙ xvec) ♯* M"and"(p ∙ xvec) ♯* AP'" and S: "set p ⊆ set xvec × set(p ∙ xvec)" by(rule_tac xvec=xvec and c="(N, Q', P, M, AP')"in name_list_avoiding) auto from Trans ‹α=M(ν*xvec)⟨N⟩›have"Ψ ⊗ ΨP⊳ Q ⟼M(ν*xvec)⟨N⟩≺ Q'"by simp with‹(p ∙ xvec) ♯* N›‹(p ∙ xvec) ♯* Q'› S have"Ψ ⊗ ΨP⊳ Q ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩≺ (p ∙ Q')" by(simp add: boundOutputChainAlpha'' create_residual.simps) moreoverfrom‹xvec ♯* AP'›‹(p ∙ xvec) ♯* AP'›‹AP' ♯* α› S have"AP' ♯* (p ∙ α)"by(simp add: freshChainSimps del: actionFreshChain) ultimatelyhave"Ψ ⊳ P ∥ Q ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩≺ P ∥ (p ∙ Q')" using FrP ‹AP' ♯* Ψ›‹AP' ♯* Q›‹distinct AP'›‹(p ∙ xvec) ♯* P›‹AP' ♯* α› ‹(p ∙ xvec) ♯* M›‹α = M(ν*xvec)⟨N⟩› by(force intro: Goal) with‹(p ∙ xvec) ♯* N›‹(p ∙ xvec) ♯* Q'›‹(p ∙ xvec) ♯* P›‹xvec ♯* P› S ‹α = M(ν*xvec)⟨N⟩› show ?case by(simp add: boundOutputChainAlpha'' eqvts create_residual.simps) qed qed
lemmaOpen: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and yvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name
obtain p::"name prm"where"(p ∙ xvec) ♯* Ψ"and"(p ∙ xvec) ♯* P"and"(p ∙ xvec) ♯* M"and"(p ∙ xvec) ♯* xvec" and"(p ∙ xvec) ♯* N"and"(p ∙ xvec) ♯* P'"and"x ♯ (p ∙ xvec)" and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" by(rule_tac xvec=xvec and c="(Ψ, P, M, xvec, N, P', x)"in name_list_avoiding)
(auto simp add: eqvts fresh_star_prod) from‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'›‹(p ∙ xvec) ♯* N›‹(p ∙ xvec) ♯* P'› S have"Ψ ⊳ P ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩≺ (p ∙ P')" by(simp add: boundOutputChainAlpha'' create_residual.simps) moreoverhence"distinct(p ∙ xvec)"by(force dest: boundOutputDistinct) moreovernote‹x ♯ Ψ›‹x ♯ M›‹x ♯ (p ∙ xvec)› moreoverfrom‹x ♯ xvec›‹x ♯ p ∙ xvec›‹x ♯ N› S have"x ♯ (p ∙ N)" by(simp add: fresh_left del: freshAlphaSwap) ultimatelyhave"Ψ ⊳(νx)P ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩≺(νx)(p ∙ P')"using‹(p ∙ xvec) ♯* Ψ›‹(p ∙ xvec) ♯* P›‹(p ∙ xvec) ♯* M› by(rule_tac cScope) auto moreoverfrom‹x ♯ xvec›‹x ♯ p ∙ xvec› S have"p ∙ x = x"by simp ultimatelyhave"Ψ ⊳(νx)P ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩≺ (p ∙ ((νx)P'))"by simp moreoverfrom‹(p ∙ xvec) ♯* P'›‹x ♯ xvec›‹x ♯ (p ∙ xvec)›have"(p ∙ xvec) ♯* (νx)P'" by(simp add: abs_fresh_star) ultimatelyhave"Ψ ⊳(νx)P ⟼M(ν*xvec)⟨N⟩≺(νx)P'"using‹(p ∙ xvec) ♯* N› S by(simp add: boundOutputChainAlpha'' create_residual.simps)
} note Goal = this show ?thesis proof(induct rule: actionCases[where α=α]) case(cInput M N) with assms show ?caseby(force intro: cScope) next case(cOutput M xvec N) with assms show ?caseby(force intro: Goal) next case cTau with assms show ?caseby(force intro: cScope) qed qed
lemma inputSwapFrameSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name and y :: name
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and"x ♯ P" and"y ♯ P"
shows"([(x, y)] ∙ Ψ) ⊳ P ⟼ ([(x, y)] ∙ M)(N)≺ P'" using assms proof(nominal_induct avoiding: x y rule: inputInduct) case(cInput Ψ M K xvec N Tvec P x y) from‹x ♯ M(λ*xvec N).P›have"x ♯ M"by simp from‹y ♯ M(λ*xvec N).P›have"y ♯ M"by simp from‹Ψ ⊨ M ↔ K›have"([(x, y)] ∙ Ψ) ⊨ ([(x, y)] ∙ M) ↔ ([(x, y)] ∙ K)" by(rule chanEqClosed) with‹x ♯ M›‹y ♯ M›have"([(x, y)] ∙ Ψ) ⊨ M ↔ ([(x, y)] ∙ K)" by(simp) thus ?caseusing‹distinct xvec›‹set xvec ⊆ supp N›‹length xvec = length Tvec› by(rule Input) next case(cCase Ψ P M N P' φ Cs x y) from‹x ♯ Cases Cs›‹y ♯ Cases Cs›‹(φ, P) mem Cs›have"x ♯ φ"and"x ♯ P"and"y ♯ φ"and"y ♯ P" by(auto dest: memFresh) from‹x ♯ P›‹y ♯ P›have"([(x ,y)] ∙ Ψ) ⊳ P ⟼ ([(x, y)] ∙ M)(N)≺ P'"by(rule cCase) moreovernote‹(φ, P) mem Cs› moreoverfrom‹Ψ ⊨ φ›have"([(x, y)] ∙ Ψ) ⊨ ([(x, y)] ∙ φ)"by(rule statClosed) with‹x ♯ φ›‹y ♯ φ›have"([(x, y)] ∙ Ψ) ⊨ φ"by simp ultimatelyshow ?caseusing‹guarded P›by(rule Case) next case(cPar1 Ψ ΨQ P M N P' AQ Q x y) from‹x ♯ P ∥ Q›have"x ♯ P"and"x ♯ Q"by simp+ from‹y ♯ P ∥ Q›have"y ♯ P"and"y ♯ Q"by simp+ from‹x ♯ P›‹y ♯ P›‹∧x y. [x ♯ P; y ♯ P]==> ([(x, y)] ∙ (Ψ ⊗ ΨQ)) ⊳ P ⟼([(x, y)]∙ M)(N)≺ P'› have"([(x, y)] ∙ Ψ) ⊗ ([(x, y)] ∙ ΨQ) ⊳ P ⟼([(x, y)] ∙ M)(N)≺ P'" by(simp add: eqvts)
moreoverfrom‹extractFrame P = ⟨AP, ΨP⟩›have"([(x, y)] ∙ (extractFrame P)) = ([(x, y)] ∙⟨AP, ΨP⟩)" by simp with‹AP♯* x›‹x ♯ P›‹AP♯* y›‹y ♯ P›have"⟨AP, ([(x, y)] ∙ ΨP)⟩ = extractFrame P" by(simp add: eqvts) moreoverfrom‹AP♯* Ψ›have"([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]) with‹AP♯* x›‹AP♯* y›have"AP♯* ([(x, y)] ∙ Ψ)"by simp moreoverfrom‹AP♯* M›have"([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ M)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]) with‹AP♯* x›‹AP♯* y›have"AP♯* ([(x, y)] ∙ M)"by simp ultimatelyshow ?caseusing‹AP♯* Q›‹AP♯* N› by(rule_tac Par2) auto next case(cScope Ψ P M N P' z x y) from‹x ♯(νz)P›‹z ♯ x›have"x ♯ P"by(simp add: abs_fresh) from‹y ♯(νz)P›‹z ♯ y›have"y ♯ P"by(simp add: abs_fresh) from‹x ♯ P›‹y ♯ P›‹∧x y. [x ♯ P; y ♯ P]==> ([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(N)≺ P'› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(N)≺ P'"by simp moreoverwith‹z ♯ Ψ›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ Ψ" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ Ψ"by simp moreoverwith‹z ♯ M›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ M" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ M"by simp ultimatelyshow ?caseusing‹z ♯ N› by(rule_tac Scope) (assumption | simp)+ next case(cBang Ψ P M N P' x y) thus ?caseby(force intro: Bang) qed
lemma inputPermFrameSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and p :: "name prm" and Xs :: "name set" and Ys :: "name set"
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and S: "set p ⊆ Xs × Ys" and"Xs ♯* P" and"Ys ♯* P"
shows"(p ∙ Ψ) ⊳ P ⟼ (p ∙ M)(N)≺ P'" using S proof(induct p) case Nil from‹Ψ ⊳ P ⟼M(N)≺ P'› show ?caseby simp next case(Cons a p) from‹set(a#p) ⊆ Xs × Ys›have"set p ⊆ Xs × Ys"by auto with‹set p ⊆ Xs × Ys ==> (p ∙ Ψ) ⊳ P ⟼ (p ∙ M)(N)≺ P'› have Trans: "(p ∙ Ψ) ⊳ P ⟼ (p ∙ M)(N)≺ P'"by simp from‹set(a#p) ⊆ Xs × Ys›show ?case proof(cases a, clarsimp) fix a b assume"a ∈ Xs"and"b ∈ Ys" with‹Xs ♯* P›‹Ys ♯* P› have"a ♯ P"and"b ♯ P" by(auto simp add: fresh_star_def) with Trans show"([(a, b)] ∙ p ∙ Ψ) ⊳ P ⟼ ([(a, b)] ∙ p ∙ M)(N)≺ P'" by(rule inputSwapFrameSubject) qed qed
lemma inputSwapSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name and y :: name
shows"Ψ ⊳ P ⟼ ([(x, y)] ∙ M)(N)≺ P'" proof - from‹Ψ ⊳ P ⟼M(N)≺ P'›‹x ♯ P›‹y ♯ P› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(N)≺ P'" by(rule inputSwapFrameSubject) with‹x ♯ Ψ›‹y ♯ Ψ›show ?thesis by simp qed
lemma inputPermSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and p :: "name prm" and Xs :: "name set" and Ys :: "name set"
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and S: "set p ⊆ Xs × Ys" and"Xs ♯* P" and"Ys ♯* P" and"Xs ♯* Ψ" and"Ys ♯* Ψ"
shows"Ψ ⊳ P ⟼ (p ∙ M)(N)≺ P'" proof - from‹Ψ ⊳ P ⟼M(N)≺ P'› S ‹Xs ♯* P›‹Ys ♯* P› have"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(N)≺ P'" by(rule inputPermFrameSubject) with‹Xs ♯* Ψ›‹Ys ♯* Ψ› S show ?thesis by simp qed
lemma inputSwapFrame: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and x :: name and y :: name
shows"([(x, y)] ∙ Ψ) ⊳ P ⟼ M(N)≺ P'" proof - from‹Ψ ⊳ P ⟼M(N)≺ P'›‹x ♯ P›‹y ♯ P› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(N)≺ P'" by(rule inputSwapFrameSubject) with‹x ♯ M›‹y ♯ M›show ?thesis by simp qed
lemma inputPermFrame: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and p :: "name prm" and Xs :: "name set" and Ys :: "name set"
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and S: "set p ⊆ Xs × Ys" and"Xs ♯* P" and"Ys ♯* P" and"Xs ♯* M" and"Ys ♯* M"
shows"(p ∙ Ψ) ⊳ P ⟼ M(N)≺ P'" proof - from‹Ψ ⊳ P ⟼M(N)≺ P'› S ‹Xs ♯* P›‹Ys ♯* P› have"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(N)≺ P'" by(rule inputPermFrameSubject) with‹Xs ♯* M›‹Ys ♯* M› S show ?thesis by simp qed
lemma inputAlpha: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and p :: "name prm" and xvec :: "name list"
moreoverfrom‹extractFrame P = ⟨AP, ΨP⟩›have"([(x, y)] ∙⟨AP, ΨP⟩) = ([(x, y)] ∙ (extractFrame P))" by simp with‹AP♯* x›‹x ♯ P›‹AP♯* y›‹y ♯ P›have"⟨AP, ([(x, y)] ∙ ΨP)⟩ = extractFrame P" by(simp add: eqvts) moreoverfrom‹AP♯* Ψ›have"([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]) with‹AP♯* x›‹AP♯* y›have"AP♯* ([(x, y)] ∙ Ψ)"by simp moreoverfrom‹AP♯* M›have"([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ M)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]) with‹AP♯* x›‹AP♯* y›have"AP♯* ([(x, y)] ∙ M)"by simp ultimatelyshow ?caseusing‹AP♯* Q›‹AP♯* N›‹xvec ♯* P›‹AP♯* xvec› by(rule_tac Par2) auto next case(cOpen Ψ P M xvec yvec N P' z x y) from‹x ♯(νz)P›‹z ♯ x›have"x ♯ P"by(simp add: abs_fresh) from‹y ♯(νz)P›‹z ♯ y›have"y ♯ P"by(simp add: abs_fresh) from‹x ♯ P›‹y ♯ P›‹∧x y. [x ♯ P; y ♯ P]==> ([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*(xvec@yvec))⟨N⟩≺ P'› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*(xvec@yvec))⟨N⟩≺ P'"by simp moreoverwith‹z ♯ Ψ›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ Ψ" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ Ψ"by simp moreoverwith‹z ♯ M›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ M" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ M"by simp ultimatelyshow ?caseusing‹z ∈ supp N›‹z ♯ xvec›‹z ♯ yvec› by(rule_tac Open) (assumption | simp)+ next case(cScope Ψ P M xvec N P' z x y) from‹x ♯(νz)P›‹z ♯ x›have"x ♯ P"by(simp add: abs_fresh) from‹y ♯(νz)P›‹z ♯ y›have"y ♯ P"by(simp add: abs_fresh) from‹x ♯ P›‹y ♯ P›‹∧x y. [x ♯ P; y ♯ P]==> ([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*xvec)⟨N⟩≺ P'› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*xvec)⟨N⟩≺ P'"by simp moreoverwith‹z ♯ Ψ›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ Ψ" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ Ψ"by simp moreoverwith‹z ♯ M›have"([(x, y)] ∙ z) ♯ [(x, y)] ∙ M" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) with‹z ♯ x›‹z ♯ y›have"z ♯ [(x, y)] ∙ M"by simp ultimatelyshow ?caseusing‹z ♯ N›‹z ♯ xvec› by(rule_tac Scope) (assumption | simp)+ next case(cBang Ψ P M B x y) thus ?caseby(force intro: Bang) qed
lemma outputPermFrameSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and p :: "name prm" and yvec :: "name list" and zvec :: "name list"
assumes"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" and S: "set p ⊆ set yvec × set zvec" and"yvec ♯* P" and"zvec ♯* P"
shows"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'" proof -
{ fix xvec N P' Xs YS assume"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'"and"xvec ♯* M"and"xvec ♯* yvec"and"xvec ♯* zvec" have"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'"using S proof(induct p) case Nil from‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'› show ?caseby simp next case(Cons a p) from‹set(a#p) ⊆ set yvec × set zvec›have"set p ⊆ set yvec × set zvec"by auto thenhave Trans: "(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'"by(rule Cons) from‹set(a#p) ⊆ set yvec × set zvec›show ?case proof(cases a, clarsimp) fix x y note Trans moreoverfrom‹xvec ♯* yvec›‹xvec ♯* zvec›‹set p ⊆ set yvec × set zvec›‹xvec ♯* M›have"xvec ♯* (p ∙ M)" by(simp add: freshChainSimps) moreoverassume"x ∈ set yvec"and"y ∈ set zvec" with‹yvec ♯* P›‹zvec ♯* P›have"x ♯ P"and"y ♯ P" by(auto simp add: fresh_star_def) ultimatelyshow"([(x, y)] ∙ p ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ p ∙ M)(ν*xvec)⟨N⟩≺ P'" by(rule outputSwapFrameSubject) qed qed
} note Goal = this obtain q::"name prm"where"(q ∙ xvec) ♯* yvec"and"(q ∙ xvec) ♯* zvec"and"(q ∙ xvec) ♯* xvec" and"(q ∙ xvec) ♯* N"and"(q ∙ xvec) ♯* P'"and"(q ∙ xvec) ♯* M" and Sq: "(set q) ⊆ (set xvec) × (set(q ∙ xvec))" by(rule_tac xvec=xvec and c="(P, xvec, yvec, zvec, N, M, P')"in name_list_avoiding) auto with‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'›have"Ψ ⊳ P ⟼M(ν*(q ∙ xvec))⟨(q ∙ N)⟩≺ (q ∙ P')" by(simp add: boundOutputChainAlpha'' residualInject) hence"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*(q ∙ xvec))⟨(q ∙ N)⟩≺ (q ∙ P')" using‹(q ∙ xvec) ♯* M›‹(q ∙ xvec) ♯* yvec›‹(q ∙ xvec) ♯* zvec› by(rule Goal) with‹(q ∙ xvec) ♯* N›‹(q ∙ xvec) ♯* P'› Sq show ?thesis by(simp add: boundOutputChainAlpha'' residualInject) qed
lemma outputSwapSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" and x :: name and y :: name
shows"Ψ ⊳ P ⟼([(x, y)] ∙ M)(ν*xvec)⟨N⟩≺ P'" proof - from‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'›‹xvec ♯* M›‹x ♯ P›‹y ♯ P› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*xvec)⟨N⟩≺ P'" by(rule outputSwapFrameSubject) with‹x ♯ Ψ›‹y ♯ Ψ›show ?thesis by simp qed
lemma outputPermSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" and p :: "name prm" and yvec :: "name list" and zvec :: "name list"
assumes"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" and S: "set p ⊆ set yvec × set zvec" and"yvec ♯* P" and"zvec ♯* P" and"yvec ♯* Ψ" and"zvec ♯* Ψ"
shows"Ψ ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'" proof - from assms have"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'" by(rule_tac outputPermFrameSubject) with S ‹yvec ♯* Ψ›‹zvec ♯* Ψ›show ?thesis by simp qed
lemma outputSwapFrame: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" and x :: name and y :: name
shows"([(x, y)] ∙ Ψ) ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" proof - from‹Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'›‹xvec ♯* M›‹x ♯ P›‹y ♯ P› have"([(x, y)] ∙ Ψ) ⊳ P ⟼([(x, y)] ∙ M)(ν*xvec)⟨N⟩≺ P'" by(rule outputSwapFrameSubject) with‹x ♯ M›‹y ♯ M›show ?thesis by simp qed
lemma outputPermFrame: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and B :: "('a, 'b, 'c) boundOutput" and p :: "name prm" and yvec :: "name list" and zvec :: "name list"
assumes"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" and S: "set p ⊆ set yvec × set zvec" and"yvec ♯* P" and"zvec ♯* P" and"yvec ♯* M" and"zvec ♯* M"
shows"(p ∙ Ψ) ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" proof - from assms have"(p ∙ Ψ) ⊳ P ⟼(p ∙ M)(ν*xvec)⟨N⟩≺ P'" by(rule_tac outputPermFrameSubject) with S ‹yvec ♯* M›‹zvec ♯* M›show ?thesis by simp qed
lemma Comm1: fixes Ψ :: 'b and ΨQ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b and Q :: "('a, 'b, 'c) psi" and K :: 'a and xvec :: "name list" and Q' :: "('a, 'b, 'c) psi" and AQ :: "name list"
shows"Ψ ⊳ P ∥ Q ⟼τ ≺(ν*xvec)(P' ∥ Q')" proof -
{ fix Ψ :: 'b and ΨQ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b and Q :: "('a, 'b, 'c) psi" and K :: 'a and xvec :: "name list" and Q' :: "('a, 'b, 'c) psi" and AQ :: "name list"
lemma Comm2: fixes Ψ :: 'b and ΨQ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b and Q :: "('a, 'b, 'c) psi" and K :: 'a and Q' :: "('a, 'b, 'c) psi" and AQ :: "name list"
shows"Ψ ⊳ P ∥ Q ⟼τ ≺(ν*xvec)(P' ∥ Q')" proof -
{ fix Ψ :: 'b and ΨQ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b and Q :: "('a, 'b, 'c) psi" and K :: 'a and Q' :: "('a, 'b, 'c) psi" and AQ :: "name list"
obtains p where"set p ⊆ set xvec × set(p ∙ xvec)"and"distinctPerm p"and"yvec = p ∙ xvec" proof - assume"∧p. [set p ⊆ set xvec × set (p ∙ xvec); distinctPerm p; yvec = p ∙ xvec]==> thesis" moreoverobtain n where"n = length xvec"by auto with assms have"∃p. (set p) ⊆ (set xvec) × set (yvec) ∧ distinctPerm p ∧ yvec = p∙ xvec" proof(induct n arbitrary: xvec yvec) case(0 xvec yvec) thus ?caseby simp next case(Suc n xvec yvec) from‹Suc n = length xvec› obtain x xvec' where"xvec = x#xvec'"and"length xvec' = n" by(case_tac xvec) auto from‹length xvec = length yvec›‹xvec = x # xvec'› obtain y yvec' where"length xvec' = length yvec'"and"yvec = y#yvec'" by(case_tac yvec) auto from‹xvec = x#xvec'›‹yvec=y#yvec'›‹xvec ♯* yvec› have"x ≠ y"and"xvec' ♯* yvec'"and"x ♯ yvec'"and"y ♯ xvec'" by(auto simp add: fresh_list_cons) 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+ from‹Suc n = length xvec›‹xvec=x#xvec'›have"n = length xvec'"by simp with‹length xvec' = length yvec'›‹xvec' ♯* yvec'›‹distinct xvec'›‹distinct yvec'› obtain p where S: "set p ⊆ set xvec' × set yvec'"and"distinctPerm p"and"yvec' = p ∙xvec'" by(drule_tac Suc) auto from S have"set((x, y)#p) ⊆ set(x#xvec') × set(y#yvec')"by auto moreoverfrom‹x ♯ xvec'›‹x ♯ yvec'›‹y ♯ xvec'›‹y ♯ yvec'› S have"x ♯ p"and"y ♯p" apply(induct p) by(auto simp add: fresh_list_nil fresh_list_cons fresh_prod name_list_supp) (auto simp add: fresh_def)
with S ‹distinctPerm p›‹x ≠ y›have"distinctPerm((x, y)#p)"by auto moreoverfrom‹yvec' = p ∙ xvec'›‹x ♯ p›‹y ♯ p›‹x ♯ xvec'›‹y ♯ xvec'›have"(y#yvec') = ((x, y)#p) ∙ (x#xvec')" by(simp add: calc_atm freshChainSimps) ultimatelyshow ?caseusing‹xvec=x#xvec'›‹yvec=y#yvec'› by blast qed ultimatelyshow ?thesis by blast qed
lemma parInputCases[consumes 1, case_names cPar1 cPar2]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and Q :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and R :: "('a, 'b, 'c) psi" and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ∥ Q ⟼M(N)≺ R" and rPar1: "∧P' AQ ΨQ. [Ψ ⊗ ΨQ⊳ P ⟼M(N)≺ P'; extractFrame Q = ⟨AQ, ΨQ⟩; distinct AQ; AQ♯* Ψ; AQ♯* P; AQ♯* Q; AQ♯* M; AQ♯* N; AQ♯* C]==> Prop (P' ∥ Q)" and rPar2: "∧Q' AP ΨP. [Ψ ⊗ ΨP⊳ Q ⟼M(N)≺ Q'; extractFrame P = ⟨AP, ΨP⟩; distinct AP; AP♯* Ψ; AP♯* P; AP♯* Q; AP♯* M; AP♯* N; AP♯* C]==> Prop (P ∥ Q')" shows"Prop R" proof - from Trans obtain α where"Ψ ⊳ P ∥ Q ⟼α ≺ R"and"bn α ♯* Ψ"and"bn α ♯* P"and"bn α ♯* Q"and"bn α ♯* subject α"and"α = M(N)"by auto thus ?thesis using rPar1 rPar2 by(induct rule: parCases) (auto simp add: residualInject) qed
lemma parOutputCases[consumes 5, case_names cPar1 cPar2]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and Q :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and R :: "('a, 'b, 'c) psi" and C :: "'d::fs_name"
shows"xvec ♯* the(subject α) = xvec ♯* subject α" using assms by(cases rule: actionCases) auto
lemma obtainPrefix: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b and B :: "name list"
obtains M where"Ψ ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" using assms proof(nominal_induct avoiding: B arbitrary: thesis rule: semanticsFrameInduct') case(cAlpha Ψ P α P' p AP ΨP B) thenobtain M where subjEq: "Ψ ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" by(rule_tac cAlpha) auto from‹set p ⊆ set(bn α) × set(bn(p ∙ α))›‹bn α ♯* subject α›‹bn(p ∙ α) ♯* α› subjEq have"Ψ ⊗ ΨP⊨ the(subject(p ∙ α)) ↔ M" by(simp add: subjectEqvt[symmetric]) thus ?caseusing cAlpha ‹B ♯* M› by auto next case(cFrameAlpha Ψ P AP ΨP p α P' B) thenobtain M where subjEq: "Ψ ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" by(rule_tac cFrameAlpha) auto have S: "set p ⊆ set AP× set (p ∙ AP)"by fact from subjEq have"(p ∙ (Ψ ⊗ ΨP)) ⊨ (p ∙ the(subject α)) ↔ (p ∙ M)" by(rule chanEqClosed) with‹AP♯* Ψ›‹(p ∙ AP) ♯* Ψ›‹(p ∙ AP) ♯* subject α› S ‹α ≠ τ›‹AP♯* α› have"Ψ ⊗ (p ∙ ΨP) ⊨ the(subject α) ↔ (p ∙ M)" by(simp add: eqvts del: subjectEqvt) moreoverfrom‹B ♯* M›have"(p ∙ B) ♯* (p ∙ M)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]) with‹AP♯* B›‹(p ∙ AP) ♯* B› S have"B ♯* (p ∙ M)"by(simp add: eqvts) ultimatelyshow ?caseby(rule cFrameAlpha) next case(cInput Ψ M K xvec N Tvec P B) from‹Ψ ⊨ M ↔ K›have"Ψ ⊗1⊨ M ↔ K" by(blast intro: statEqEnt AssertionStatEqSym[OF Identity]) hence"Ψ ⊗1⊨ K ↔ M"by(rule chanEqSym) moreoverfrom‹B ♯* (M(λ*xvec N).P)›have"B ♯* M"by simp ultimatelyshow ?caseby(rule_tac cInput) auto next case(cOutput Ψ M K N P B) from‹Ψ ⊨ M ↔ K›have"Ψ ⊗1⊨ M ↔ K" by(blast intro: statEqEnt AssertionStatEqSym[OF Identity]) hence"Ψ ⊗1⊨ K ↔ M" by(rule chanEqSym) moreoverfrom‹B ♯* (M⟨N⟩.P)›have"B ♯* M"by simp ultimatelyshow ?caseby(rule_tac cOutput) auto next case(cCase Ψ P α P' φ Cs AP ΨP B) thenobtain M where"Ψ ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" by(rule_tac cCase) (auto dest: memFreshChain) with‹ΨP≃1›show ?caseby(blast intro: cCase statEqEnt compositionSym Identity) next case(cPar1 Ψ ΨQ P α P' AQ Q AP ΨP B) thenobtain M where"(Ψ ⊗ ΨQ) ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" apply(rule_tac cPar1) by assumption auto thus ?case by(metis cPar1 statEqEnt Associativity Commutativity AssertionStatEqTrans Composition) next case(cPar2 Ψ ΨP Q α Q' AP P AQ ΨQ B) thenobtain M where"(Ψ ⊗ ΨP) ⊗ ΨQ⊨ the(subject α) ↔ M"and"B ♯* M" by(rule_tac cPar2) auto thus ?caseby(metis cPar2 statEqEnt Associativity) next case cComm1 thus ?caseby simp next case cComm2 thus ?caseby simp next case(cOpen Ψ P M xvec yvec N P' x AP ΨP B) thenobtain K where"Ψ ⊗ ΨP⊨ M ↔ K"and"B ♯* K" apply(rule_tac cOpen) by force auto thus ?caseby(fastforce intro: cOpen) next case(cScope Ψ P α P' x AP ΨP B) thenobtain M where"Ψ ⊗ ΨP⊨ the(subject α) ↔ M"and"B ♯* M" by(rule_tac cScope) auto thus ?caseby(fastforce intro: cScope) next case(cBang Ψ P α P' AP ΨP B) thenobtain K where"Ψ ⊗ ΨP⊗1⊨ the(subject α) ↔ K"and"B ♯* K" by(rule_tac cBang) auto with‹ΨP≃1›show ?caseby(metis cBang statEqEnt compositionSym Identity) qed
lemma inputRenameSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b
assumes"Ψ ⊳ P ⟼M(N)≺ P'" and"extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and"Ψ ⊗ ΨP⊨ M ↔ K" and"AP♯* Ψ" and"AP♯* P" and"AP♯* M" and"AP♯* K"
shows"Ψ ⊳ P ⟼K(N)≺ P'" using assms proof(nominal_induct avoiding: K rule: inputFrameInduct) case(cAlpha Ψ P M N P' AP ΨP p K) have S: "set p ⊆ set AP× set (p ∙ AP)"by fact from‹Ψ ⊗ (p ∙ ΨP) ⊨ M ↔ K›have"(p ∙ (Ψ ⊗ (p ∙ ΨP))) ⊨ (p ∙ M) ↔ (p ∙ K)" by(rule chanEqClosed) with S ‹distinctPerm p›‹AP♯* Ψ›‹AP♯* M›‹AP♯* K›‹(p ∙ AP) ♯* Ψ›‹(p ∙ AP) ♯* M›‹(p ∙ AP) ♯* K› have"Ψ ⊗ ΨP⊨ M ↔ K"by(simp add: eqvts) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹[Ψ ⊗ ΨP⊨ M ↔ K; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* K]==> Ψ ⊳ P ⟼K(N)≺ P'› show ?caseby blast next case(cInput Ψ M K xvec N Tvec P K') from‹Ψ ⊗1⊨ K ↔ K'›have"Ψ ⊨ K ↔ K'" by(blast intro: statEqEnt Identity) with‹Ψ ⊨ M ↔ K›have"Ψ ⊨ M ↔ K'" by(rule chanEqTrans) thus ?caseusing‹distinct xvec›‹set xvec ⊆ supp N›‹length xvec = length Tvec› by(rule Input) next case(cCase Ψ P M N P' φ Cs AP ΨP K) from‹Ψ ⊗1⊨ M ↔ K›‹ΨP≃1›have"Ψ ⊗ ΨP⊨ M ↔ K" by(blast intro: statEqEnt Identity compositionSym AssertionStatEqSym) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [Ψ ⊗ ΨP⊨ M ↔ K; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* K]==> Ψ ⊳ P ⟼K(N)≺ P'› have"Ψ ⊳ P ⟼K(N)≺ P'"by force thus ?caseusing‹(φ, P) mem Cs›‹Ψ ⊨ φ›‹guarded P›by(rule Case) next case(cPar1 Ψ ΨQ P M N P' AQ Q AP ΨP K) from‹Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K›have"(Ψ ⊗ ΨQ) ⊗ ΨP⊨ M ↔ K" by(metis statEqEnt Associativity Composition AssertionStatEqTrans Commutativity) with‹AP♯* Ψ›‹AP♯* ΨQ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [(Ψ ⊗ ΨQ) ⊗ ΨP⊨ M ↔ K; AP♯* (Ψ ⊗ ΨQ); AP♯* P; AP♯* M; AP♯* K]==> Ψ ⊗ ΨQ⊳ P ⟼K(N)≺ P'› have"Ψ ⊗ ΨQ⊳ P ⟼K(N)≺ P'"by force thus ?caseusing‹extractFrame Q = ⟨AQ, ΨQ⟩›‹AQ♯* Ψ›‹AQ♯* P›‹AQ♯* K›‹AQ♯* N› by(rule_tac Par1) auto next case(cPar2 Ψ ΨP Q M N Q' AP P AQ ΨQ K) from‹Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K›have"(Ψ ⊗ ΨP) ⊗ ΨQ⊨ M ↔ K" by(rule statEqEnt[OF AssertionStatEqSym[OF Associativity]]) with‹AQ♯* Ψ›‹AQ♯* ΨP›‹AQ♯* Q›‹AQ♯* M›‹AQ♯* K› ‹∧K. [(Ψ ⊗ ΨP) ⊗ ΨQ⊨ M ↔ K; AQ♯* (Ψ ⊗ ΨP); AQ♯* Q; AQ♯* M; AQ♯* K]==> Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'› have"Ψ ⊗ ΨP⊳ Q ⟼K(N)≺ Q'"by force thus ?caseusing‹extractFrame P = ⟨AP, ΨP⟩›‹AP♯* Ψ›‹AP♯* Q›‹AP♯* K›‹AP♯* N› by(rule_tac Par2) auto next case(cScope Ψ P M N P' x AP ΨP) hence"Ψ ⊳ P ⟼K(N)≺ P'"by force with‹x ♯ Ψ›‹x ♯ K›‹x ♯ N›show ?case by(rule_tac Scope) auto next case(cBang Ψ P M N P' AP ΨP K) from‹Ψ ⊗1⊨ M ↔ K›‹ΨP≃1›have"Ψ ⊗ ΨP⊗1⊨ M ↔ K" by(blast intro: statEqEnt Identity compositionSym AssertionStatEqSym) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [Ψ ⊗ ΨP⊗1⊨ M ↔ K; AP♯* Ψ; AP♯* (P ∥ !P); AP♯* M; AP♯* K]==> Ψ ⊳ P ∥ !P ⟼K(N)≺ P'› have"Ψ ⊳ P ∥ !P ⟼K(N)≺ P'"by force thus ?caseusing‹guarded P›by(rule Bang) qed
lemma outputRenameSubject: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and M :: 'a and xvec :: "name list" and N :: 'a and P' :: "('a, 'b, 'c) psi" and AP :: "name list" and ΨP :: 'b
assumes"Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩≺ P'" and"extractFrame P = ⟨AP, ΨP⟩" and"distinct AP" and"Ψ ⊗ ΨP⊨ M ↔ K" and"AP♯* Ψ" and"AP♯* P" and"AP♯* M" and"AP♯* K"
shows"Ψ ⊳ P ⟼K(ν*xvec)⟨N⟩≺ P'" using assms apply(simp add: residualInject) proof(nominal_induct avoiding: K rule: outputFrameInduct) case(cAlpha Ψ P M AP ΨP p B K) have S: "set p ⊆ set AP× set(p ∙ AP)"by fact from‹Ψ ⊗ (p ∙ ΨP) ⊨ M ↔ K›have"(p ∙ (Ψ ⊗ (p ∙ ΨP))) ⊨ (p ∙ M) ↔ (p ∙ K)" by(rule chanEqClosed) with S ‹distinctPerm p›‹AP♯* Ψ›‹AP♯* M›‹AP♯* K›‹(p ∙ AP) ♯* Ψ›‹(p ∙ AP) ♯* M›‹(p ∙ AP) ♯* K› have"Ψ ⊗ ΨP⊨ M ↔ K"by(simp add: eqvts) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› show ?caseby(blast intro: cAlpha) next case(cOutput Ψ M K N P K') from‹Ψ ⊗1⊨ K ↔ K'›have"Ψ ⊨ K ↔ K'" by(blast intro: statEqEnt Identity) with‹Ψ ⊨ M ↔ K›have"Ψ ⊨ M ↔ K'" by(rule chanEqTrans) thus ?caseusingOutputby(force simp add: residualInject) next case(cCase Ψ P M B φ Cs AP ΨP K) from‹Ψ ⊗1⊨ M ↔ K›‹ΨP≃1›have"Ψ ⊗ ΨP⊨ M ↔ K" by(blast intro: statEqEnt Identity compositionSym AssertionStatEqSym) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [Ψ ⊗ ΨP⊨ M ↔ K; AP♯* Ψ; AP♯* P; AP♯* M; AP♯* K]==> Ψ ⊳ P ⟼(ROut K B)› have"Ψ ⊳ P ⟼ROut K B"by force thus ?caseusing‹(φ, P) mem Cs›‹Ψ ⊨ φ›‹guarded P›by(rule Case) next case(cPar1 Ψ ΨQ P M xvec N P' AQ Q AP ΨP K) from‹Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K›have"(Ψ ⊗ ΨQ) ⊗ ΨP⊨ M ↔ K" by(metis statEqEnt Associativity Composition AssertionStatEqTrans Commutativity) with‹AP♯* Ψ›‹AP♯* ΨQ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [(Ψ ⊗ ΨQ) ⊗ ΨP⊨ M ↔ K; AP♯* (Ψ ⊗ ΨQ); AP♯* P; AP♯* M; AP♯* K]==> Ψ ⊗ ΨQ⊳ P ⟼(ROut K ((ν*xvec)N ≺' P'))› have"Ψ ⊗ ΨQ⊳ P ⟼K(ν*xvec)⟨N⟩≺ P'"by(force simp add: residualInject) thus ?caseusing‹extractFrame Q = ⟨AQ, ΨQ⟩›‹xvec ♯* Q›‹AQ♯* Ψ›‹AQ♯* P›‹AQ♯* K›‹AQ♯* xvec›‹AQ♯* N› Par1[where α="K(ν*xvec)⟨N⟩"] by(auto simp add: residualInject) next case(cPar2 Ψ ΨP Q M xvec N Q' AP P AQ ΨQ K) from‹Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K›have"(Ψ ⊗ ΨP) ⊗ ΨQ⊨ M ↔ K" by(rule statEqEnt[OF AssertionStatEqSym[OF Associativity]]) with‹AQ♯* Ψ›‹AQ♯* ΨP›‹AQ♯* Q›‹AQ♯* M›‹AQ♯* K› ‹∧K. [(Ψ ⊗ ΨP) ⊗ ΨQ⊨ M ↔ K; AQ♯* (Ψ ⊗ ΨP); AQ♯* Q; AQ♯* M; AQ♯* K]==> Ψ ⊗ ΨP⊳ Q ⟼ROut K ((ν*xvec)N ≺' Q')› have"Ψ ⊗ ΨP⊳ Q ⟼ROut K ((ν*xvec)N ≺' Q')"by force thus ?caseusing‹extractFrame P = ⟨AP, ΨP⟩›‹xvec ♯* P›‹AP♯* Ψ›‹AP♯* Q›‹AP♯* K›‹AP♯* xvec›‹AP♯* N› Par2[where α="K(ν*xvec)⟨N⟩"] by(auto simp add: residualInject) next case(cOpen Ψ P M xvec yvec N P' x AP ΨP) hence"Ψ ⊳ P ⟼K(ν*(xvec@yvec))⟨N⟩≺ P'"by(force simp add: residualInject) with‹x ∈ supp N›‹x ♯ Ψ›‹x ♯ K›‹x ♯ xvec›‹x ♯ yvec›Openshow ?case by(auto simp add: residualInject) next case(cScope Ψ P M xvec N P' x AP ΨP) hence"Ψ ⊳ P ⟼K(ν*xvec)⟨N⟩≺ P'"by(force simp add: residualInject) with‹x ♯ Ψ›‹x ♯ K›‹x ♯ xvec›‹x ♯ N› Scope[where α="K(ν*xvec)⟨N⟩"] show ?case by(auto simp add: residualInject) next case(cBang Ψ P M B AP ΨP K) from‹Ψ ⊗1⊨ M ↔ K›‹ΨP≃1›have"Ψ ⊗ ΨP⊗1⊨ M ↔ K" by(blast intro: statEqEnt Identity compositionSym AssertionStatEqSym) with‹AP♯* Ψ›‹AP♯* P›‹AP♯* M›‹AP♯* K› ‹∧K. [Ψ ⊗ ΨP⊗1⊨ M ↔ K; AP♯* Ψ; AP♯* (P ∥ !P); AP♯* M; AP♯* K]==> Ψ ⊳ P ∥ !P ⟼ROut K B› have"Ψ ⊳ P ∥ !P ⟼ROut K B"by force thus ?caseusing‹guarded P›by(rule Bang) qed
lemma parCasesSubject[consumes 7, case_names cPar1 cPar2 cComm1 cComm2]: fixes Ψ :: 'b and P :: "('a, 'b, 'c) psi" and Q :: "('a, 'b, 'c) psi" and α :: "'a action" and R :: "('a, 'b, 'c) psi" and C :: "'d::fs_name" and yvec :: "name list"
shows"Prop α R" using Trans ‹bn α ♯* Ψ›‹bn α ♯* P›‹bn α ♯* Q›‹bn α ♯* subject α› proof(induct rule: parCases[where C="(C, yvec)"]) case(cPar1 P' AQ ΨQ) thus ?caseby(rule_tac rPar1) auto next case(cPar2 Q' AP ΨP) thus ?caseby(rule_tac rPar2) auto next case(cComm1 ΨQ M N P' AP ΨP K xvec Q' AQ) from‹AP♯* (C, yvec)›‹AQ♯* (C, yvec)›‹xvec ♯* (C, yvec)› have"AP♯* C"and"AQ♯* C"and"xvec ♯* C"and"AP♯* yvec"and"AQ♯* yvec"and"xvec ♯* yvec" by simp+
have FrP: "extractFrame P = ⟨AP, ΨP⟩"and FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" and MeqK: "Ψ ⊗ ΨP⊗ ΨQ⊨ M ↔ K"by fact+
lemma inputCases[consumes 1, case_names cInput]: fixes Ψ :: 'b and M :: 'a and xvec :: "name list" and N :: 'a and P :: "('a, 'b, 'c) psi" and α :: "'a action" and P' :: "('a, 'b, 'c) psi"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.