| changeset 1277 | 6eacf60ce41d |
| parent 1270 | 8c3cf9f4f5f2 |
| child 1300 | 22a084c9316b |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
14 |
14 |
15 thm rtrm4.recs |
15 thm rtrm4.recs |
16 |
16 |
17 (* there cannot be a clause for lists, as *) |
17 (* there cannot be a clause for lists, as *) |
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
19 setup {* snd o define_raw_perms ["rtrm4"] ["Term4.rtrm4"] *} |
19 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} |
20 |
20 |
21 (* "repairing" of the permute function *) |
21 (* "repairing" of the permute function *) |
22 lemma repaired: |
22 lemma repaired: |
23 fixes ts::"rtrm4 list" |
23 fixes ts::"rtrm4 list" |
24 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
24 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
27 done |
27 done |
28 |
28 |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
31 |
31 |
32 local_setup {* snd o define_fv_alpha "Term4.rtrm4" [ |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
33 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
33 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
34 print_theorems |
34 print_theorems |
35 |
35 |
36 notation |
36 notation |
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |