172 (*To perform binary arithmetic. The "left" rewriting handles patterns |
172 (*To perform binary arithmetic. The "left" rewriting handles patterns |
173 created by the simprocs, such as 3 * (5 * x). *) |
173 created by the simprocs, such as 3 * (5 * x). *) |
174 val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym, |
174 val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym, |
175 add_number_of_left, mult_number_of_left] @ |
175 add_number_of_left, mult_number_of_left] @ |
176 bin_arith_simps @ bin_rel_simps; |
176 bin_arith_simps @ bin_rel_simps; |
|
177 |
|
178 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms |
|
179 during re-arrangement*) |
|
180 val non_add_bin_simps = |
|
181 bin_simps \\ [add_number_of_left, number_of_add RS sym]; |
177 |
182 |
178 (*To evaluate binary negations of coefficients*) |
183 (*To evaluate binary negations of coefficients*) |
179 val zminus_simps = NCons_simps @ |
184 val zminus_simps = NCons_simps @ |
180 [zminus_1_eq_m1, number_of_minus RS sym, |
185 [zminus_1_eq_m1, number_of_minus RS sym, |
181 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
186 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
213 val find_first_coeff = find_first_coeff [] |
218 val find_first_coeff = find_first_coeff [] |
214 val trans_tac = trans_tac |
219 val trans_tac = trans_tac |
215 val norm_tac = |
220 val norm_tac = |
216 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
221 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
217 diff_simps@zminus_simps@zadd_ac)) |
222 diff_simps@zminus_simps@zadd_ac)) |
218 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
223 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@int_mult_minus_simps)) |
219 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
224 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
220 zadd_ac@zmult_ac)) |
225 zadd_ac@zmult_ac)) |
221 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
226 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
222 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
227 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
223 end; |
228 end; |
280 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
285 val prove_conv = Bin_Simprocs.prove_conv_nohyps |
281 val trans_tac = trans_tac |
286 val trans_tac = trans_tac |
282 val norm_tac = |
287 val norm_tac = |
283 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
288 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ |
284 diff_simps@zminus_simps@zadd_ac)) |
289 diff_simps@zminus_simps@zadd_ac)) |
285 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
290 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@int_mult_minus_simps)) |
286 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
291 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
287 zadd_ac@zmult_ac)) |
292 zadd_ac@zmult_ac)) |
288 val numeral_simp_tac = ALLGOALS |
293 val numeral_simp_tac = ALLGOALS |
289 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
294 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
290 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
295 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |