114 ) |
114 ) |
115 |
115 |
116 val ring_cancel_numeral_factors = |
116 val ring_cancel_numeral_factors = |
117 map Bin_Simprocs.prep_simproc |
117 map Bin_Simprocs.prep_simproc |
118 [("ring_eq_cancel_numeral_factor", |
118 [("ring_eq_cancel_numeral_factor", |
119 ["(l::'a::{ordered_ring,number_ring}) * m = n", |
119 ["(l::'a::{ordered_idom,number_ring}) * m = n", |
120 "(l::'a::{ordered_ring,number_ring}) = m * n"], |
120 "(l::'a::{ordered_idom,number_ring}) = m * n"], |
121 EqCancelNumeralFactor.proc), |
121 EqCancelNumeralFactor.proc), |
122 ("ring_less_cancel_numeral_factor", |
122 ("ring_less_cancel_numeral_factor", |
123 ["(l::'a::{ordered_ring,number_ring}) * m < n", |
123 ["(l::'a::{ordered_idom,number_ring}) * m < n", |
124 "(l::'a::{ordered_ring,number_ring}) < m * n"], |
124 "(l::'a::{ordered_idom,number_ring}) < m * n"], |
125 LessCancelNumeralFactor.proc), |
125 LessCancelNumeralFactor.proc), |
126 ("ring_le_cancel_numeral_factor", |
126 ("ring_le_cancel_numeral_factor", |
127 ["(l::'a::{ordered_ring,number_ring}) * m <= n", |
127 ["(l::'a::{ordered_idom,number_ring}) * m <= n", |
128 "(l::'a::{ordered_ring,number_ring}) <= m * n"], |
128 "(l::'a::{ordered_idom,number_ring}) <= m * n"], |
129 LeCancelNumeralFactor.proc), |
129 LeCancelNumeralFactor.proc), |
130 ("int_div_cancel_numeral_factors", |
130 ("int_div_cancel_numeral_factors", |
131 ["((l::int) * m) div n", "(l::int) div (m * n)"], |
131 ["((l::int) * m) div n", "(l::int) div (m * n)"], |
132 DivCancelNumeralFactor.proc)]; |
132 DivCancelNumeralFactor.proc)]; |
133 |
133 |
247 val find_first = find_first [] |
247 val find_first = find_first [] |
248 val trans_tac = trans_tac |
248 val trans_tac = trans_tac |
249 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) |
249 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) |
250 end; |
250 end; |
251 |
251 |
252 (*mult_cancel_left requires an ordered ring, such as int. The version in |
252 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in |
253 rat_arith.ML works for all fields.*) |
253 rat_arith.ML works for all fields.*) |
254 structure EqCancelFactor = ExtractCommonTermFun |
254 structure EqCancelFactor = ExtractCommonTermFun |
255 (open CancelFactorCommon |
255 (open CancelFactorCommon |
256 val prove_conv = Bin_Simprocs.prove_conv |
256 val prove_conv = Bin_Simprocs.prove_conv |
257 val mk_bal = HOLogic.mk_eq |
257 val mk_bal = HOLogic.mk_eq |