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