20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 |
24 |
25 text {* can lift *} |
|
26 |
|
27 thm distinct |
25 thm distinct |
28 thm trm_raw_assg_raw.inducts |
26 thm induct |
29 thm trm_raw.exhaust |
27 thm exhaust |
30 thm assg_raw.exhaust |
|
31 thm fv_defs |
28 thm fv_defs |
32 thm bn_defs |
29 thm bn_defs |
33 thm perm_simps |
30 thm perm_simps |
34 thm perm_laws |
|
35 thm trm_raw_assg_raw.size(9 - 16) |
|
36 thm eq_iff |
31 thm eq_iff |
37 thm eq_iff_simps |
32 thm fv_bn_eqvt |
38 thm bn_defs |
|
39 thm fv_eqvt |
|
40 thm bn_eqvt |
|
41 thm size_eqvt |
33 thm size_eqvt |
42 |
34 |
43 |
|
44 ML {* |
|
45 val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct}) |
|
46 *} |
|
47 |
|
48 ML {* |
|
49 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.inducts} |
|
50 *} |
|
51 |
|
52 ML {* |
|
53 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw.exhaust} |
|
54 *} |
|
55 |
|
56 ML {* |
|
57 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms assg_raw.exhaust} |
|
58 *} |
|
59 |
|
60 ML {* |
|
61 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_defs} |
|
62 *} |
|
63 |
|
64 ML {* |
|
65 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
66 *} |
|
67 |
|
68 ML {* |
|
69 val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps} |
|
70 *} |
|
71 |
|
72 ML {* |
|
73 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws} |
|
74 *} |
|
75 |
|
76 ML {* |
|
77 val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
78 prod.cases} |
|
79 *} |
|
80 |
|
81 ML {* |
|
82 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff} |
|
83 *} |
|
84 |
|
85 ML {* |
|
86 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps} |
|
87 *} |
|
88 |
|
89 ML {* |
|
90 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs} |
|
91 *} |
|
92 |
|
93 ML {* |
|
94 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt} |
|
95 *} |
|
96 |
|
97 ML {* |
|
98 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt} |
|
99 *} |
|
100 |
|
101 ML {* |
|
102 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt} |
|
103 *} |
|
104 |
35 |
105 |
36 |
106 |
37 |
107 |
38 |
108 lemma supp_fv: |
39 lemma supp_fv: |