176 |
176 |
177 (*Apply the given rewrite (if present) just once*) |
177 (*Apply the given rewrite (if present) just once*) |
178 fun trans_tac None = all_tac |
178 fun trans_tac None = all_tac |
179 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
179 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
180 |
180 |
181 fun prove_conv name tacs sg (t, u) = |
181 fun prove_conv name tacs sg (hyps: thm list) (t,u) = |
182 if t aconv u then None |
182 if t aconv u then None |
183 else |
183 else |
184 let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) |
184 let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) |
185 in Some |
185 in Some |
186 (prove_goalw_cterm [] ct (K tacs) |
186 (prove_goalw_cterm [] ct (K tacs) |
187 handle ERROR => error |
187 handle ERROR => error |
188 ("The error(s) above occurred while trying to prove " ^ |
188 ("The error(s) above occurred while trying to prove " ^ |
189 string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) |
189 string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) |
190 end; |
190 end; |
|
191 |
|
192 (*version without the hyps argument*) |
|
193 fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []; |
191 |
194 |
192 fun simplify_meta_eq rules = |
195 fun simplify_meta_eq rules = |
193 mk_meta_eq o |
196 mk_meta_eq o |
194 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
197 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
195 |
198 |
266 val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
269 val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
267 val dest_sum = dest_sum |
270 val dest_sum = dest_sum |
268 val mk_coeff = mk_coeff |
271 val mk_coeff = mk_coeff |
269 val dest_coeff = dest_coeff 1 |
272 val dest_coeff = dest_coeff 1 |
270 val left_distrib = left_zadd_zmult_distrib RS trans |
273 val left_distrib = left_zadd_zmult_distrib RS trans |
271 val prove_conv = prove_conv "int_combine_numerals" |
274 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
272 val trans_tac = trans_tac |
275 val trans_tac = trans_tac |
273 val norm_tac = ALLGOALS |
276 val norm_tac = ALLGOALS |
274 (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
277 (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
275 zminus_simps@zadd_ac)) |
278 zminus_simps@zadd_ac)) |
276 THEN ALLGOALS |
279 THEN ALLGOALS |