170 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
170 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, |
171 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
171 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; |
172 |
172 |
173 (*To let us treat subtraction as addition*) |
173 (*To let us treat subtraction as addition*) |
174 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
174 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus]; |
|
175 |
|
176 (*push the unary minus down: - x * y = x * - y *) |
|
177 val int_minus_mult_eq_1_to_2 = |
|
178 [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard; |
|
179 |
|
180 (*to extract again any uncancelled minuses*) |
|
181 val int_minus_from_mult_simps = |
|
182 [zminus_zminus, zmult_zminus, zmult_zminus_right]; |
|
183 |
|
184 (*combine unary minus with numeric literals, however nested within a product*) |
|
185 val int_mult_minus_simps = |
|
186 [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2]; |
175 |
187 |
176 (*Apply the given rewrite (if present) just once*) |
188 (*Apply the given rewrite (if present) just once*) |
177 fun trans_tac None = all_tac |
189 fun trans_tac None = all_tac |
178 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
190 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
179 |
191 |
205 val dest_sum = dest_sum |
217 val dest_sum = dest_sum |
206 val mk_coeff = mk_coeff |
218 val mk_coeff = mk_coeff |
207 val dest_coeff = dest_coeff 1 |
219 val dest_coeff = dest_coeff 1 |
208 val find_first_coeff = find_first_coeff [] |
220 val find_first_coeff = find_first_coeff [] |
209 val trans_tac = trans_tac |
221 val trans_tac = trans_tac |
210 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
222 val norm_tac = |
211 zminus_simps@zadd_ac)) |
223 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
212 THEN ALLGOALS |
224 zminus_simps@zadd_ac)) |
213 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
225 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
214 bin_simps@zadd_ac@zmult_ac)) |
226 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
|
227 zadd_ac@zmult_ac)) |
215 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
228 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
216 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
229 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
217 end; |
230 end; |
218 |
231 |
219 |
232 |
271 val mk_coeff = mk_coeff |
284 val mk_coeff = mk_coeff |
272 val dest_coeff = dest_coeff 1 |
285 val dest_coeff = dest_coeff 1 |
273 val left_distrib = left_zadd_zmult_distrib RS trans |
286 val left_distrib = left_zadd_zmult_distrib RS trans |
274 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
287 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
275 val trans_tac = trans_tac |
288 val trans_tac = trans_tac |
276 val norm_tac = ALLGOALS |
289 val norm_tac = |
277 (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
290 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ |
278 zminus_simps@zadd_ac)) |
291 zminus_simps@zadd_ac)) |
279 THEN ALLGOALS |
292 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
280 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
293 THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ |
281 bin_simps@zadd_ac@zmult_ac)) |
294 zadd_ac@zmult_ac)) |
282 val numeral_simp_tac = ALLGOALS |
295 val numeral_simp_tac = ALLGOALS |
283 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
296 (simp_tac (HOL_ss addsimps add_0s@bin_simps)) |
284 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
297 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s) |
285 end; |
298 end; |
286 |
299 |