equal
deleted
inserted
replaced
50 lemma lookup_eqvt[eqvt]: |
50 lemma lookup_eqvt[eqvt]: |
51 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
51 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
52 apply(induct Ts T rule: lookup.induct) |
52 apply(induct Ts T rule: lookup.induct) |
53 apply(simp_all) |
53 apply(simp_all) |
54 done |
54 done |
|
55 |
|
56 lemma TEST1: |
|
57 assumes "x = Inl y" |
|
58 shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)" |
|
59 using assms by simp |
|
60 |
|
61 lemma TEST2: |
|
62 assumes "x = Inr y" |
|
63 shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)" |
|
64 using assms by simp |
55 |
65 |
56 lemma test: |
66 lemma test: |
57 assumes a: "\<exists>y. f x = Inl y" |
67 assumes a: "\<exists>y. f x = Inl y" |
58 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
68 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
59 using a |
69 using a |
273 apply (rule perm_supp_eq) |
283 apply (rule perm_supp_eq) |
274 apply (simp add: fresh_def fresh_star_def) |
284 apply (simp add: fresh_def fresh_star_def) |
275 apply blast |
285 apply blast |
276 done |
286 done |
277 |
287 |
|
288 |
|
289 termination (eqvt) by lexicographic_order |
|
290 |
|
291 thm subst_substs.eqvt[no_vars] |
|
292 thm subst_def |
|
293 thm substs_def |
|
294 thm Sum_Type.Projr.simps |
|
295 |
|
296 lemma |
|
297 shows "(p \<bullet> subst x y) = subst (p \<bullet> x) (p \<bullet> y)" |
|
298 and "(p \<bullet> substs x' y') = substs (p \<bullet> x') (p \<bullet> y')" |
|
299 unfolding subst_def substs_def |
|
300 thm permute_fun_app_eq |
|
301 thm Sum_Type.Projl_def sum_rec_def |
|
302 apply(simp add: permute_fun_def) |
|
303 unfolding subst_substs_sumC_def |
|
304 thm subst_substs.eqvt |
|
305 apply(case_tac x) |
|
306 apply(simp) |
|
307 apply(case_tac a) |
|
308 apply(simp) |
|
309 thm subst_def |
|
310 apply(simp) |
|
311 |
278 section {* defined as two separate nominal datatypes *} |
312 section {* defined as two separate nominal datatypes *} |
279 |
313 |
280 nominal_datatype ty2 = |
314 nominal_datatype ty2 = |
281 Var2 "name" |
315 Var2 "name" |
282 | Fun2 "ty2" "ty2" |
316 | Fun2 "ty2" "ty2" |