| changeset 1183 | cb3da5b540f2 |
| parent 1181 | 788a59d2d7aa |
| 1182:3c32f91fa771 | 1183:cb3da5b540f2 |
|---|---|
23 primrec |
23 primrec |
24 bv1 |
24 bv1 |
25 where |
25 where |
26 "bv1 (BUnit) = {}" |
26 "bv1 (BUnit) = {}" |
27 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
29 |
29 |
30 local_setup {* define_raw_fv "Terms.rtrm1" |
30 local_setup {* define_raw_fv "Terms.rtrm1" |
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
32 [[], [[]], [[], []]]] *} |
32 [[], [[]], [[], []]]] *} |
33 print_theorems |
33 print_theorems |
56 |
56 |
57 (* Shouyld we derive it? But bv is given by the user? *) |
57 (* Shouyld we derive it? But bv is given by the user? *) |
58 lemma bv1_eqvt[eqvt]: |
58 lemma bv1_eqvt[eqvt]: |
59 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
59 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
60 apply (induct x) |
60 apply (induct x) |
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt) |
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) |
62 done |
62 done |
63 |
63 |
64 lemma fv_rtrm1_eqvt[eqvt]: |
64 lemma fv_rtrm1_eqvt[eqvt]: |
65 shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
65 shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
66 apply (induct t) |
66 apply (induct t) |