41 structure CancelNumeralFactorCommon = |
41 structure CancelNumeralFactorCommon = |
42 struct |
42 struct |
43 val mk_coeff = mk_coeff |
43 val mk_coeff = mk_coeff |
44 val dest_coeff = dest_coeff 1 |
44 val dest_coeff = dest_coeff 1 |
45 val trans_tac = fn _ => trans_tac |
45 val trans_tac = fn _ => trans_tac |
|
46 |
|
47 val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s |
|
48 val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps |
|
49 val norm_ss3 = HOL_ss addsimps mult_ac |
46 fun norm_tac ss = |
50 fun norm_tac ss = |
47 let val HOL_ss' = Simplifier.inherit_context ss HOL_ss in |
51 ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) |
48 ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s)) |
52 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) |
49 THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps)) |
53 THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) |
50 THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac)) |
54 |
51 end |
55 val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps |
52 fun numeral_simp_tac ss = |
56 fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) |
53 ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps)) |
|
54 val simplify_meta_eq = |
57 val simplify_meta_eq = |
55 Int_Numeral_Simprocs.simplify_meta_eq |
58 Int_Numeral_Simprocs.simplify_meta_eq |
56 [add_0, add_0_right, |
59 [add_0, add_0_right, |
57 mult_zero_left, mult_zero_right, mult_1, mult_1_right]; |
60 mult_zero_left, mult_zero_right, mult_1, mult_1_right]; |
58 end |
61 end |
248 val dest_sum = dest_prod |
251 val dest_sum = dest_prod |
249 val mk_coeff = mk_coeff |
252 val mk_coeff = mk_coeff |
250 val dest_coeff = dest_coeff |
253 val dest_coeff = dest_coeff |
251 val find_first = find_first [] |
254 val find_first = find_first [] |
252 val trans_tac = fn _ => trans_tac |
255 val trans_tac = fn _ => trans_tac |
253 fun norm_tac ss = |
256 val norm_ss = HOL_ss addsimps mult_1s @ mult_ac |
254 ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac)) |
257 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) |
255 end; |
258 end; |
256 |
259 |
257 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in |
260 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in |
258 rat_arith.ML works for all fields.*) |
261 rat_arith.ML works for all fields.*) |
259 structure EqCancelFactor = ExtractCommonTermFun |
262 structure EqCancelFactor = ExtractCommonTermFun |