20 binder |
22 binder |
21 bn::"assg \<Rightarrow> atom set" |
23 bn::"assg \<Rightarrow> atom set" |
22 where |
24 where |
23 "bn (As x t) = {atom x}" |
25 "bn (As x t) = {atom x}" |
24 |
26 |
25 |
|
26 thm permute_trm_raw_permute_assg_raw.simps[no_vars] |
27 thm permute_trm_raw_permute_assg_raw.simps[no_vars] |
27 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] |
28 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] |
28 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
29 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
29 |
30 |
30 ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*} |
31 ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*} |
31 ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *} |
32 ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *} |
32 |
33 |
33 (* |
|
34 lemma empty_eqvt[eqvt]: |
|
35 shows "p \<bullet> {} = {}" |
|
36 unfolding empty_def |
|
37 by (perm_simp) (rule refl) |
|
38 *) |
|
39 lemma |
|
40 "(p \<bullet> {}) = {}" |
|
41 thm eqvts_raw |
|
42 thm eqvts |
|
43 apply(perm_strict_simp) |
|
44 |
|
45 |
|
46 lemma |
34 lemma |
47 shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)" |
35 shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)" |
48 and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)" |
36 and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)" |
49 and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)" |
37 and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)" |
50 apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct) |
38 apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct) |
51 apply(simp_all) |
39 apply(perm_simp add: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps, rule refl)+ |
52 apply(perm_simp) |
40 done |
53 apply(rule refl) |
|
54 apply(perm_simp) |
|
55 apply(rule refl) |
|
56 apply(perm_simp) |
|
57 apply(rule refl) |
|
58 apply(simp add: fv_trm_raw.simps) |
|
59 |
41 |
60 |
42 |
61 |
43 |
62 ML {* Inductive.the_inductive *} |
44 ML {* Inductive.the_inductive *} |
63 thm trm_assg.fv |
45 thm trm_assg.fv |