equal
deleted
inserted
replaced
21 bn::"assg \<Rightarrow> atom set" |
21 bn::"assg \<Rightarrow> atom set" |
22 where |
22 where |
23 "bn (As x t) = {atom x}" |
23 "bn (As x t) = {atom x}" |
24 |
24 |
25 |
25 |
|
26 thm permute_trm_raw_permute_assg_raw.simps[no_vars] |
26 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_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] |
27 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
28 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
29 |
|
30 ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*} |
|
31 ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *} |
|
32 |
|
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 |
|
47 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)" |
|
49 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) |
|
51 apply(simp_all) |
|
52 apply(perm_simp) |
|
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) |
28 |
59 |
29 |
60 |
30 |
61 |
31 ML {* Inductive.the_inductive *} |
62 ML {* Inductive.the_inductive *} |
32 thm trm_assg.fv |
63 thm trm_assg.fv |