42 thm bn_defs |
40 thm bn_defs |
43 thm fv_eqvt |
41 thm fv_eqvt |
44 thm bn_eqvt |
42 thm bn_eqvt |
45 thm size_eqvt |
43 thm size_eqvt |
46 |
44 |
|
45 ML {* |
|
46 fun lifted ctxt qtys rthm = |
|
47 let |
|
48 (* When the theorem is atomized, eta redexes are contracted, |
|
49 so we do it both in the original theorem *) |
|
50 val rthm' = Drule.eta_contraction_rule rthm |
|
51 val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt |
|
52 val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'') |
|
53 in |
|
54 Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1)) |
|
55 |> singleton (ProofContext.export ctxt' ctxt) |
|
56 end |
|
57 *} |
47 |
58 |
48 ML {* |
59 ML {* |
49 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
60 val _ = timeit (fn () => map (lifted @{context} [@{typ trm}, @{typ assg}]) @{thms distinct}) |
50 *} |
61 *} |
51 |
62 |
52 ML {* |
63 ML {* |
53 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
64 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.inducts} |
54 *} |
65 *} |
55 |
66 |
56 ML {* |
67 ML {* |
57 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust} |
68 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw.exhaust} |
58 *} |
69 *} |
59 |
70 |
60 ML {* |
71 ML {* |
61 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust} |
72 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms assg_raw.exhaust} |
62 *} |
73 *} |
63 |
74 |
64 ML {* |
75 ML {* |
65 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
76 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_defs} |
66 *} |
77 *} |
67 |
78 |
68 ML {* |
79 ML {* |
69 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
80 val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.size(9 - 16)} |
70 *} |
81 *} |
71 |
82 |
72 ML {* |
83 ML {* |
73 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps} |
84 val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_simps} |
74 *} |
85 *} |
75 |
86 |
76 ML {* |
87 ML {* |
77 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
88 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_laws} |
78 *} |
89 *} |
79 |
90 |
80 ML {* |
91 ML {* |
81 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
92 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) |
82 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
93 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
83 prod.cases]} |
94 prod.cases]} |
84 *} |
95 *} |
85 |
96 |
86 ML {* |
97 ML {* |
87 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
98 val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) |
88 @{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
99 @{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
89 prod.cases]} |
100 prod.cases]} |
90 *} |
101 *} |
91 |
102 |
92 ML {* |
103 ML {* |
93 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs} |
104 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_defs} |
94 *} |
105 *} |
95 |
106 |
96 ML {* |
107 ML {* |
97 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt} |
108 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_eqvt} |
98 *} |
109 *} |
99 |
110 |
100 ML {* |
111 ML {* |
101 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt} |
112 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_eqvt} |
102 *} |
113 *} |
103 |
114 |
104 ML {* |
115 ML {* |
105 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt} |
116 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms size_eqvt} |
106 *} |
117 *} |
107 |
118 |
108 |
119 |
109 |
120 |
110 lemma supp_fv: |
121 lemma supp_fv: |