149 fun prep_simproc thy (name, pats, proc) = |
149 fun prep_simproc thy (name, pats, proc) = |
150 Simplifier.simproc_global thy name pats proc; |
150 Simplifier.simproc_global thy name pats proc; |
151 |
151 |
152 structure CancelNumeralsCommon = |
152 structure CancelNumeralsCommon = |
153 struct |
153 struct |
154 val mk_sum = (fn _ : typ => mk_sum) |
154 val mk_sum = (fn _ : typ => mk_sum) |
155 val dest_sum = dest_sum |
155 val dest_sum = dest_sum |
156 val mk_coeff = mk_coeff |
156 val mk_coeff = mk_coeff |
157 val dest_coeff = dest_coeff 1 |
157 val dest_coeff = dest_coeff 1 |
158 val find_first_coeff = find_first_coeff [] |
158 val find_first_coeff = find_first_coeff [] |
159 val trans_tac = ArithData.gen_trans_tac @{thm iff_trans} |
159 fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans} |
160 |
160 |
161 val norm_ss1 = |
161 val norm_ss1 = |
162 simpset_of (put_simpset ZF_ss @{context} |
162 simpset_of (put_simpset ZF_ss @{context} |
163 addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}) |
163 addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}) |
164 val norm_ss2 = |
164 val norm_ss2 = |
231 (*version without the hyps argument*) |
231 (*version without the hyps argument*) |
232 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; |
232 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; |
233 |
233 |
234 structure CombineNumeralsData = |
234 structure CombineNumeralsData = |
235 struct |
235 struct |
236 type coeff = int |
236 type coeff = int |
237 val iszero = (fn x => x = 0) |
237 val iszero = (fn x => x = 0) |
238 val add = op + |
238 val add = op + |
239 val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *) |
239 val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *) |
240 val dest_sum = dest_sum |
240 val dest_sum = dest_sum |
241 val mk_coeff = mk_coeff |
241 val mk_coeff = mk_coeff |
242 val dest_coeff = dest_coeff 1 |
242 val dest_coeff = dest_coeff 1 |
243 val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} |
243 val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} |
244 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
244 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
245 val trans_tac = ArithData.gen_trans_tac @{thm trans} |
245 fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans} |
246 |
246 |
247 val norm_ss1 = |
247 val norm_ss1 = |
248 simpset_of (put_simpset ZF_ss @{context} |
248 simpset_of (put_simpset ZF_ss @{context} |
249 addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys) |
249 addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys) |
250 val norm_ss2 = |
250 val norm_ss2 = |
279 the "sum" of #3, x, #4; the literals are then multiplied*) |
279 the "sum" of #3, x, #4; the literals are then multiplied*) |
280 |
280 |
281 |
281 |
282 structure CombineNumeralsProdData = |
282 structure CombineNumeralsProdData = |
283 struct |
283 struct |
284 type coeff = int |
284 type coeff = int |
285 val iszero = (fn x => x = 0) |
285 val iszero = (fn x => x = 0) |
286 val add = op * |
286 val add = op * |
287 val mk_sum = (fn _ : typ => mk_prod) |
287 val mk_sum = (fn _ : typ => mk_prod) |
288 val dest_sum = dest_prod |
288 val dest_sum = dest_prod |
289 fun mk_coeff(k,t) = if t=one then mk_numeral k |
289 fun mk_coeff(k,t) = |
290 else raise TERM("mk_coeff", []) |
290 if t = one then mk_numeral k |
|
291 else raise TERM("mk_coeff", []) |
291 fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) |
292 fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) |
292 val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} |
293 val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} |
293 val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" |
294 val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" |
294 val trans_tac = ArithData.gen_trans_tac @{thm trans} |
295 fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans} |
295 |
296 |
296 |
297 val norm_ss1 = |
297 |
298 simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps) |
298 val norm_ss1 = |
299 val norm_ss2 = |
299 simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps) |
300 simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ |
300 val norm_ss2 = |
301 bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys) |
301 simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ |
302 fun norm_tac ctxt = |
302 bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys) |
303 ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) |
303 fun norm_tac ctxt = |
304 THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) |
304 ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt)) |
305 |
305 THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt)) |
306 val numeral_simp_ss = |
306 |
307 simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys) |
307 val numeral_simp_ss = |
308 fun numeral_simp_tac ctxt = |
308 simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys) |
309 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) |
309 fun numeral_simp_tac ctxt = |
310 val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); |
310 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) |
|
311 val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); |
|
312 end; |
311 end; |
313 |
312 |
314 |
313 |
315 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); |
314 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); |
316 |
315 |