equal
deleted
inserted
replaced
25 proof - |
25 proof - |
26 show ?thesis |
26 show ?thesis |
27 by(auto) |
27 by(auto) |
28 qed |
28 qed |
29 |
29 |
30 nominal_primrec |
30 nominal_function |
31 subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name" |
31 subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name" |
32 where |
32 where |
33 "subst_name_list a [] = a" |
33 "subst_name_list a [] = a" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
35 apply(simp add: eqvt_def subst_name_list_graph_aux_def) |
35 apply(simp add: eqvt_def subst_name_list_graph_aux_def) |
141 lemma testlr: |
141 lemma testlr: |
142 assumes a: "\<exists>y. f = Inr (Inl y)" |
142 assumes a: "\<exists>y. f = Inr (Inl y)" |
143 shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))" |
143 shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))" |
144 using a by auto |
144 using a by auto |
145 |
145 |
146 nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))") |
146 nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))") |
147 subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and |
147 subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and |
148 subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and |
148 subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and |
149 subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100) |
149 subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100) |
150 where |
150 where |
151 "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])" |
151 "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])" |