Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.
(* Theory be Kirstin Peters *)+ −
+ − theory Pi+ −
imports "../Nominal2"+ −
begin+ −
+ − atom_decl name+ −
+ − subsection {* Capture-Avoiding Substitution of Names *}+ −
+ − definition+ −
subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)+ −
where+ −
"a[b:::=c] \<equiv> if (a = b) then c else a"+ −
+ − declare subst_name_def[simp]+ −
+ − lemma subst_name_mix_eqvt[eqvt]:+ −
fixes p :: perm+ −
and a :: name+ −
and b :: name+ −
and c :: name+ −
+ − shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"+ −
proof -+ −
show ?thesis+ −
by(auto)+ −
qed+ −
+ − nominal_primrec+ −
subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"+ −
where+ −
"subst_name_list a [] = a"+ −
| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"+ −
apply(auto)+ −
apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")+ −
unfolding eqvt_def+ −
apply(rule allI)+ −
apply(simp add: permute_fun_def)+ −
apply(rule ext)+ −
apply(rule ext)+ −
apply(simp add: permute_bool_def)+ −
apply(rule iffI)+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="- p \<bullet> x" in meta_spec)+ −
apply(drule_tac x="- p \<bullet> xa" in meta_spec)+ −
apply(simp)+ −
apply(drule_tac x="-p" in meta_spec)+ −
apply(drule_tac x="x" in meta_spec)+ −
apply(drule_tac x="xa" in meta_spec)+ −
apply(simp)+ −
apply(erule subst_name_list_graph.induct)+ −
apply(perm_simp)+ −
apply(rule subst_name_list_graph.intros)+ −
apply(perm_simp)+ −
apply(rule subst_name_list_graph.intros)+ −
apply(simp)+ −
apply(rule_tac y="b" in list.exhaust)+ −
by(auto)+ −
+ − termination (eqvt)+ −
by (lexicographic_order)+ −
+ − + − section {* The Synchronous Pi-Calculus *}+ −
+ − subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}+ −
+ − nominal_datatype+ −
guardedTerm_mix = Output name name piMix ("_!<_>\<onesuperior>._" [120, 120, 110] 110)+ −
| Input name b::name P::piMix binds b in P ("_?<_>\<onesuperior>._" [120, 120, 110] 110)+ −
| Tau piMix ("<\<tau>\<onesuperior>>._" [110] 110)+ −
and sumList_mix = SumNil ("\<zero>\<onesuperior>")+ −
| AddSummand guardedTerm_mix sumList_mix (infixr "\<oplus>\<onesuperior>" 65)+ −
and piMix = Res a::name P::piMix binds a in P ("<\<nu>_>\<onesuperior>_" [100, 100] 100)+ −
| Par piMix piMix (infixr "\<parallel>\<onesuperior>" 85)+ −
| Match name name piMix ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)+ −
| Sum sumList_mix ("\<oplus>\<onesuperior>{_}" 90)+ −
| Rep name b::name P::piMix binds b in P ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)+ −
| Succ ("succ\<onesuperior>")+ −
+ − lemmas piMix_strong_induct = guardedTerm_mix_sumList_mix_piMix.strong_induct+ −
lemmas piMix_fresh = guardedTerm_mix_sumList_mix_piMix.fresh+ −
lemmas piMix_eq_iff = guardedTerm_mix_sumList_mix_piMix.eq_iff+ −
lemmas piMix_distinct = guardedTerm_mix_sumList_mix_piMix.distinct+ −
lemmas piMix_size = guardedTerm_mix_sumList_mix_piMix.size+ −
+ − subsection {* Alpha-Conversion Lemmata *}+ −
+ − lemma alphaRes_mix:+ −
fixes a :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"+ −
proof(cases "a = z")+ −
assume "a = z"+ −
thus ?thesis+ −
by(simp)+ −
next+ −
assume "a \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+ −
qed+ −
+ − lemma alphaInput_mix:+ −
fixes a :: name+ −
and b :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"+ −
proof(cases "b = z")+ −
assume "b = z"+ −
thus ?thesis+ −
by(simp)+ −
next+ −
assume "b \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+ −
qed+ −
+ − lemma alphaRep_mix:+ −
fixes a :: name+ −
and b :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"+ −
proof(cases "b = z")+ −
assume "b = z"+ −
thus ?thesis+ −
by(simp)+ −
next+ −
assume "b \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+ −
qed+ −
+ − subsection {* Capture-Avoiding Substitution of Names *}+ −
+ − lemma testl:+ −
assumes a: "\<exists>y. f = Inl y"+ −
shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)"+ −
using a by auto+ −
+ − lemma testrr:+ −
assumes a: "\<exists>y. f = Inr (Inr y)"+ −
shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))"+ −
using a by auto+ −
+ − lemma testlr:+ −
assumes a: "\<exists>y. f = Inr (Inl y)"+ −
shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))"+ −
using a by auto+ −
+ − nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")+ −
subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and+ −
subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and+ −
subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)+ −
where+ −
"(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"+ −
| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"+ −
| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"+ −
| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"+ −
| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"+ −
| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"+ −
| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"+ −
| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"+ −
| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"+ −
| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"+ −
| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"+ −
apply(auto simp add: piMix_distinct piMix_eq_iff)+ −
apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")+ −
unfolding eqvt_def+ −
apply(rule allI)+ −
apply(simp add: permute_fun_def)+ −
apply(rule ext)+ −
apply(rule ext)+ −
apply(simp add: permute_bool_def)+ −
apply(rule iffI)+ −
apply(drule_tac x="p" in meta_spec)+ −
apply(drule_tac x="- p \<bullet> x" in meta_spec)+ −
apply(drule_tac x="- p \<bullet> xa" in meta_spec)+ −
apply(simp)+ −
apply(drule_tac x="-p" in meta_spec)+ −
apply(drule_tac x="x" in meta_spec)+ −
apply(drule_tac x="xa" in meta_spec)+ −
apply(simp)+ −
--"Equivariance"+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+ −
apply(simp)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp (no_asm_use) only: eqvts) + −
apply(subst testl)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(subst testlr)+ −
apply(rotate_tac 2)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(perm_simp)+ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(blast)+ −
apply(blast)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+ −
apply(simp)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(subst testrr)+ −
apply(rotate_tac 2)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(perm_simp)+ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(blast)+ −
apply(blast)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(blast)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testlr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(blast)+ −
apply(simp (no_asm_use) only: eqvts)+ −
apply(subst testrr)+ −
apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply(blast)++ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+ −
apply(blast)+ −
apply(perm_simp)+ −
apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+ −
--"Covered all cases"+ −
apply(case_tac x)+ −
apply(simp)+ −
apply(case_tac a)+ −
apply(simp)+ −
apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))+ −
apply(blast)+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(blast)+ −
apply(simp)+ −
apply(blast)+ −
apply(simp)+ −
apply(case_tac b)+ −
apply(simp)+ −
apply(case_tac a)+ −
apply(simp)+ −
apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))+ −
apply(blast)+ −
apply(blast)+ −
apply(simp)+ −
apply(case_tac ba)+ −
apply(simp)+ −
apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(blast)+ −
apply(blast)+ −
apply(blast)+ −
apply(auto simp add: fresh_star_def)[1]+ −
apply(blast)+ −
apply(simp)+ −
apply(blast)+ −
--"compatibility"+ −
apply (simp add: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])+ −
apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")+ −
apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")+ −
apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")+ −
prefer 2+ −
apply (simp add: eqvt_at_def subs_mix_def)+ −
apply rule+ −
apply (subst testrr)+ −
apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)+ −
apply (simp add: THE_default_def)+ −
apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")+ −
apply simp_all[2]+ −
apply auto[1]+ −
apply (erule_tac x="x" in allE)+ −
apply simp+ −
apply (thin_tac "\<forall>p\<Colon>perm.+ −
p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =+ −
(if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x+ −
then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x+ −
else Inr (Inr undefined))")+ −
apply (thin_tac "\<forall>p\<Colon>perm.+ −
p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x+ −
then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x+ −
else Inr (Inr undefined)) =+ −
(if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x+ −
then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+ −
subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x+ −
else Inr (Inr undefined))")+ −
apply (thin_tac "atom b \<sharp> (xa, ya)")+ −
apply (thin_tac "atom ba \<sharp> (xa, ya)")+ −
apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")+ −
apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)+ −
apply assumption+ −
apply (metis Inr_not_Inl)+ −
apply (metis Inr_not_Inl)+ −
apply (metis Inr_not_Inl)+ −
apply (metis Inr_inject Inr_not_Inl)+ −
apply (metis Inr_inject Inr_not_Inl)+ −
apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr+ −
(Sum_Type.Projr+ −
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply (rule_tac x="Sum_Type.Projr+ −
(Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>+ −
Sum_Type.Projr+ −
(Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr+ −
(Sum_Type.Projr+ −
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl+ −
(Sum_Type.Projr+ −
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr+ −
(Sum_Type.Projr+ −
(subsGuard_mix_subsList_mix_subs_mix_sum+ −
(Inr (Inr (Pb, xb, y)))))" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply (rule_tac x="succ\<onesuperior>" in exI)+ −
apply clarify+ −
apply (rule the1_equality)+ −
apply blast apply assumption+ −
apply simp+ −
(* Here the only real goal compatibility is left *)+ −
apply (erule Abs_lst1_fcb)+ −
apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)+ −
apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")+ −
apply simp+ −
apply (erule fresh_eqvt_at)+ −
apply (simp_all add: fresh_Pair finite_supp eqvts eqvt_at_def fresh_Pair swap_fresh_fresh)+ −
done+ −
+ − termination (eqvt)+ −
by (lexicographic_order)+ −
+ − lemma forget_mix:+ −
fixes g :: guardedTerm_mix+ −
and xg :: sumList_mix+ −
and P :: piMix+ −
and x :: name+ −
and y :: name+ −
+ − shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"+ −
and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"+ −
and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"+ −
proof -+ −
show "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"+ −
and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"+ −
and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"+ −
using assms+ −
apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)+ −
by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)+ −
qed+ −
+ − lemma fresh_fact_mix:+ −
fixes g :: guardedTerm_mix+ −
and xg :: sumList_mix+ −
and P :: piMix+ −
and x :: name+ −
and y :: name+ −
and z :: name+ −
+ − assumes "atom z \<sharp> y"+ −
+ − shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"+ −
and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"+ −
and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"+ −
proof -+ −
show "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"+ −
and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"+ −
and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"+ −
using assms+ −
apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)+ −
by(auto simp add: piMix_fresh fresh_at_base)+ −
qed+ −
+ − lemma substitution_lemma_mix:+ −
fixes g :: guardedTerm_mix+ −
and xg :: sumList_mix+ −
and P :: piMix+ −
and s :: name+ −
and u :: name+ −
and x :: name+ −
and y :: name+ −
+ − assumes "x \<noteq> y"+ −
and "atom x \<sharp> u"+ −
+ − shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"+ −
and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"+ −
and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"+ −
proof -+ −
show "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"+ −
and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"+ −
and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"+ −
using assms+ −
apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)+ −
apply(simp_all add: fresh_fact_mix forget_mix)+ −
by(auto simp add: fresh_at_base)+ −
qed+ −
+ − lemma perm_eq_subst_mix:+ −
fixes g :: guardedTerm_mix+ −
and xg :: sumList_mix+ −
and P :: piMix+ −
and x :: name+ −
and y :: name+ −
+ − shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"+ −
and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"+ −
and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"+ −
proof -+ −
show "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"+ −
and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"+ −
and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"+ −
apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)+ −
by(auto simp add: piMix_fresh fresh_at_base)+ −
qed+ −
+ − lemma subst_id_mix:+ −
fixes g :: guardedTerm_mix+ −
and xg :: sumList_mix+ −
and P :: piMix+ −
and x :: name+ −
+ − shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"+ −
proof -+ −
show "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"+ −
apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)+ −
by(auto)+ −
qed+ −
+ − lemma alphaRes_subst_mix:+ −
fixes a :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"+ −
proof(cases "a = z")+ −
assume "a = z"+ −
thus ?thesis+ −
by(simp add: subst_id_mix)+ −
next+ −
assume "a \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: alphaRes_mix perm_eq_subst_mix)+ −
qed+ −
+ − lemma alphaInput_subst_mix:+ −
fixes a :: name+ −
and b :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"+ −
proof(cases "b = z")+ −
assume "b = z"+ −
thus ?thesis+ −
by(simp add: subst_id_mix)+ −
next+ −
assume "b \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: alphaInput_mix perm_eq_subst_mix)+ −
qed+ −
+ − lemma alphaRep_subst_mix:+ −
fixes a :: name+ −
and b :: name+ −
and P :: piMix+ −
and z :: name+ −
+ − assumes "atom z \<sharp> P"+ −
+ − shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"+ −
proof(cases "b = z")+ −
assume "b = z"+ −
thus ?thesis+ −
by(simp add: subst_id_mix)+ −
next+ −
assume "b \<noteq> z"+ −
thus ?thesis+ −
using assms+ −
by(simp add: alphaRep_mix perm_eq_subst_mix)+ −
qed+ −
+ − inductive+ −
fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"+ −
where+ −
"fresh_list_guard_mix [] g"+ −
| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"+ −
+ − equivariance fresh_list_guard_mix+ −
nominal_inductive fresh_list_guard_mix+ −
done+ −
+ − inductive+ −
fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"+ −
where+ −
"fresh_list_sumList_mix [] xg"+ −
| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"+ −
+ − equivariance fresh_list_sumList_mix+ −
nominal_inductive fresh_list_sumList_mix+ −
done+ −
+ − inductive+ −
fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"+ −
where+ −
"fresh_list_mix [] P"+ −
| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"+ −
+ − equivariance fresh_list_mix+ −
nominal_inductive fresh_list_mix+ −
done+ −
+ − end+ −