101 simproc_setup int_combine_numerals |
101 simproc_setup int_combine_numerals |
102 ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") = |
102 ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") = |
103 {* fn phi => Numeral_Simprocs.combine_numerals *} |
103 {* fn phi => Numeral_Simprocs.combine_numerals *} |
104 |
104 |
105 simproc_setup field_combine_numerals |
105 simproc_setup field_combine_numerals |
106 ("(i::'a::{field_inverse_zero, number_ring}) + j" |
106 ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j" |
107 |"(i::'a::{field_inverse_zero, number_ring}) - j") = |
107 |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") = |
108 {* fn phi => Numeral_Simprocs.field_combine_numerals *} |
108 {* fn phi => Numeral_Simprocs.field_combine_numerals *} |
109 |
109 |
110 simproc_setup inteq_cancel_numerals |
110 simproc_setup inteq_cancel_numerals |
111 ("(l::'a::number_ring) + m = n" |
111 ("(l::'a::number_ring) + m = n" |
112 |"(l::'a::number_ring) = m + n" |
112 |"(l::'a::number_ring) = m + n" |
139 |"- (l::'a::{linordered_idom,number_ring}) \<le> m" |
139 |"- (l::'a::{linordered_idom,number_ring}) \<le> m" |
140 |"(l::'a::{linordered_idom,number_ring}) \<le> - m") = |
140 |"(l::'a::{linordered_idom,number_ring}) \<le> - m") = |
141 {* fn phi => Numeral_Simprocs.le_cancel_numerals *} |
141 {* fn phi => Numeral_Simprocs.le_cancel_numerals *} |
142 |
142 |
143 simproc_setup ring_eq_cancel_numeral_factor |
143 simproc_setup ring_eq_cancel_numeral_factor |
144 ("(l::'a::{idom,number_ring}) * m = n" |
144 ("(l::'a::{idom,ring_char_0,number_ring}) * m = n" |
145 |"(l::'a::{idom,number_ring}) = m * n") = |
145 |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") = |
146 {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *} |
146 {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *} |
147 |
147 |
148 simproc_setup ring_less_cancel_numeral_factor |
148 simproc_setup ring_less_cancel_numeral_factor |
149 ("(l::'a::{linordered_idom,number_ring}) * m < n" |
149 ("(l::'a::{linordered_idom,number_ring}) * m < n" |
150 |"(l::'a::{linordered_idom,number_ring}) < m * n") = |
150 |"(l::'a::{linordered_idom,number_ring}) < m * n") = |
154 ("(l::'a::{linordered_idom,number_ring}) * m <= n" |
154 ("(l::'a::{linordered_idom,number_ring}) * m <= n" |
155 |"(l::'a::{linordered_idom,number_ring}) <= m * n") = |
155 |"(l::'a::{linordered_idom,number_ring}) <= m * n") = |
156 {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *} |
156 {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *} |
157 |
157 |
158 simproc_setup int_div_cancel_numeral_factors |
158 simproc_setup int_div_cancel_numeral_factors |
159 ("((l::'a::{semiring_div,number_ring}) * m) div n" |
159 ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n" |
160 |"(l::'a::{semiring_div,number_ring}) div (m * n)") = |
160 |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") = |
161 {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} |
161 {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} |
162 |
162 |
163 simproc_setup divide_cancel_numeral_factor |
163 simproc_setup divide_cancel_numeral_factor |
164 ("((l::'a::{field_inverse_zero,number_ring}) * m) / n" |
164 ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n" |
165 |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)" |
165 |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)" |
166 |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") = |
166 |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") = |
167 {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} |
167 {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} |
168 |
168 |
169 simproc_setup ring_eq_cancel_factor |
169 simproc_setup ring_eq_cancel_factor |
170 ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = |
170 ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") = |
171 {* fn phi => Numeral_Simprocs.eq_cancel_factor *} |
171 {* fn phi => Numeral_Simprocs.eq_cancel_factor *} |