128 |
128 |
129 subsection {* Capture-Avoiding Substitution of Names *} |
129 subsection {* Capture-Avoiding Substitution of Names *} |
130 |
130 |
131 lemma testl: |
131 lemma testl: |
132 assumes a: "\<exists>y. f = Inl y" |
132 assumes a: "\<exists>y. f = Inl y" |
133 shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)" |
133 shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)" |
134 using a by auto |
134 using a by auto |
135 |
135 |
136 lemma testrr: |
136 lemma testrr: |
137 assumes a: "\<exists>y. f = Inr (Inr y)" |
137 assumes a: "\<exists>y. f = Inr (Inr y)" |
138 shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))" |
138 shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))" |
139 using a by auto |
139 using a by auto |
140 |
140 |
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 "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))") |
146 nominal_primrec (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])" |
238 apply (metis Inr_not_Inl) |
238 apply (metis Inr_not_Inl) |
239 apply (metis Inr_not_Inl) |
239 apply (metis Inr_not_Inl) |
240 apply (metis Inr_not_Inl) |
240 apply (metis Inr_not_Inl) |
241 apply (metis Inr_inject Inr_not_Inl) |
241 apply (metis Inr_inject Inr_not_Inl) |
242 apply (metis Inr_inject Inr_not_Inl) |
242 apply (metis Inr_inject Inr_not_Inl) |
243 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr |
243 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr |
244 (Sum_Type.Projr |
244 (Sum_Type.projr |
245 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
245 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
246 apply clarify |
246 apply clarify |
247 apply (rule the1_equality) |
247 apply (rule the1_equality) |
248 apply blast apply assumption |
248 apply blast apply assumption |
249 apply (rule_tac x="Sum_Type.Projr |
249 apply (rule_tac x="Sum_Type.projr |
250 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
250 (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
251 Sum_Type.Projr |
251 Sum_Type.projr |
252 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
252 (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
253 apply clarify |
253 apply clarify |
254 apply (rule the1_equality) |
254 apply (rule the1_equality) |
255 apply blast apply assumption |
255 apply blast apply assumption |
256 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr |
256 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr |
257 (Sum_Type.Projr |
257 (Sum_Type.projr |
258 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
258 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
259 apply clarify |
259 apply clarify |
260 apply (rule the1_equality) |
260 apply (rule the1_equality) |
261 apply blast apply assumption |
261 apply blast apply assumption |
262 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl |
262 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl |
263 (Sum_Type.Projr |
263 (Sum_Type.projr |
264 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
264 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
265 apply clarify |
265 apply clarify |
266 apply (rule the1_equality) |
266 apply (rule the1_equality) |
267 apply blast apply assumption |
267 apply blast apply assumption |
268 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr |
268 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr |
269 (Sum_Type.Projr |
269 (Sum_Type.projr |
270 (subsGuard_mix_subsList_mix_subs_mix_sum |
270 (subsGuard_mix_subsList_mix_subs_mix_sum |
271 (Inr (Inr (Pb, xb, y)))))" in exI) |
271 (Inr (Inr (Pb, xb, y)))))" in exI) |
272 apply clarify |
272 apply clarify |
273 apply (rule the1_equality) |
273 apply (rule the1_equality) |
274 apply blast apply assumption |
274 apply blast apply assumption |
331 apply (metis Inr_not_Inl) |
331 apply (metis Inr_not_Inl) |
332 apply (metis Inr_not_Inl) |
332 apply (metis Inr_not_Inl) |
333 apply (metis Inr_not_Inl) |
333 apply (metis Inr_not_Inl) |
334 apply (metis Inr_inject Inr_not_Inl) |
334 apply (metis Inr_inject Inr_not_Inl) |
335 apply (metis Inr_inject Inr_not_Inl) |
335 apply (metis Inr_inject Inr_not_Inl) |
336 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr |
336 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr |
337 (Sum_Type.Projr |
337 (Sum_Type.projr |
338 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
338 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
339 apply clarify |
339 apply clarify |
340 apply (rule the1_equality) |
340 apply (rule the1_equality) |
341 apply blast apply assumption |
341 apply blast apply assumption |
342 apply (rule_tac x="Sum_Type.Projr |
342 apply (rule_tac x="Sum_Type.projr |
343 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
343 (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
344 Sum_Type.Projr |
344 Sum_Type.projr |
345 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
345 (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
346 apply clarify |
346 apply clarify |
347 apply (rule the1_equality) |
347 apply (rule the1_equality) |
348 apply blast apply assumption |
348 apply blast apply assumption |
349 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr |
349 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr |
350 (Sum_Type.Projr |
350 (Sum_Type.projr |
351 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
351 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
352 apply clarify |
352 apply clarify |
353 apply (rule the1_equality) |
353 apply (rule the1_equality) |
354 apply blast apply assumption |
354 apply blast apply assumption |
355 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl |
355 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl |
356 (Sum_Type.Projr |
356 (Sum_Type.projr |
357 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
357 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
358 apply clarify |
358 apply clarify |
359 apply (rule the1_equality) |
359 apply (rule the1_equality) |
360 apply blast apply assumption |
360 apply blast apply assumption |
361 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr |
361 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr |
362 (Sum_Type.Projr |
362 (Sum_Type.projr |
363 (subsGuard_mix_subsList_mix_subs_mix_sum |
363 (subsGuard_mix_subsList_mix_subs_mix_sum |
364 (Inr (Inr (Pb, xb, y)))))" in exI) |
364 (Inr (Inr (Pb, xb, y)))))" in exI) |
365 apply clarify |
365 apply clarify |
366 apply (rule the1_equality) |
366 apply (rule the1_equality) |
367 apply blast apply assumption |
367 apply blast apply assumption |