125 |
125 |
126 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
126 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
128 in |
128 in |
129 first_conv_wrapper |
129 first_conv_wrapper |
130 [ More_Conv.rewrs_conv pre_thms, |
130 [ Conv.rewrs_conv pre_thms, |
131 eqvt_apply_conv, |
131 eqvt_apply_conv, |
132 eqvt_lambda_conv, |
132 eqvt_lambda_conv, |
133 More_Conv.rewrs_conv post_thms, |
133 Conv.rewrs_conv post_thms, |
134 progress_info_conv ctxt strict_flag excluded |
134 progress_info_conv ctxt strict_flag excluded |
135 ] ctrm |
135 ] ctrm |
136 end |
136 end |
137 |
137 |
138 (* the eqvt-tactics first eta-normalise goals in |
138 (* the eqvt-tactics first eta-normalise goals in |
139 order to avoid problems with inductions in the |
139 order to avoid problems with inductions in the |
140 equivaraince command. *) |
140 equivaraince command. *) |
141 |
141 |
142 (* raises an error if some permutations cannot be eliminated *) |
142 (* raises an error if some permutations cannot be eliminated *) |
143 fun eqvt_strict_tac ctxt user_thms excluded = |
143 fun eqvt_strict_tac ctxt user_thms excluded = |
144 CONVERSION (More_Conv.top_conv |
144 CONVERSION (Conv.top_conv |
145 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) |
145 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) |
146 |
146 |
147 (* prints a warning message if some permutations cannot be eliminated *) |
147 (* prints a warning message if some permutations cannot be eliminated *) |
148 fun eqvt_tac ctxt user_thms excluded = |
148 fun eqvt_tac ctxt user_thms excluded = |
149 CONVERSION (More_Conv.top_conv |
149 CONVERSION (Conv.top_conv |
150 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) |
150 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) |
151 |
151 |
152 (* setup of the configuration value *) |
152 (* setup of the configuration value *) |
153 val setup = |
153 val setup = |
154 trace_eqvt_setup |
154 trace_eqvt_setup |