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" |
113 |"(l::'a::number_ring) - m = n" |
113 |"(l::'a::number_ring) - m = n" |
114 |"(l::'a::number_ring) = m - n" |
114 |"(l::'a::number_ring) = m - n" |
115 |"(l::'a::number_ring) * m = n" |
115 |"(l::'a::number_ring) * m = n" |
116 |"(l::'a::number_ring) = m * n") = |
116 |"(l::'a::number_ring) = m * n" |
|
117 |"- (l::'a::number_ring) = m" |
|
118 |"(l::'a::number_ring) = - m") = |
117 {* fn phi => Numeral_Simprocs.eq_cancel_numerals *} |
119 {* fn phi => Numeral_Simprocs.eq_cancel_numerals *} |
118 |
120 |
119 simproc_setup intless_cancel_numerals |
121 simproc_setup intless_cancel_numerals |
120 ("(l::'a::{linordered_idom,number_ring}) + m < n" |
122 ("(l::'a::{linordered_idom,number_ring}) + m < n" |
121 |"(l::'a::{linordered_idom,number_ring}) < m + n" |
123 |"(l::'a::{linordered_idom,number_ring}) < m + n" |
122 |"(l::'a::{linordered_idom,number_ring}) - m < n" |
124 |"(l::'a::{linordered_idom,number_ring}) - m < n" |
123 |"(l::'a::{linordered_idom,number_ring}) < m - n" |
125 |"(l::'a::{linordered_idom,number_ring}) < m - n" |
124 |"(l::'a::{linordered_idom,number_ring}) * m < n" |
126 |"(l::'a::{linordered_idom,number_ring}) * m < n" |
125 |"(l::'a::{linordered_idom,number_ring}) < m * n") = |
127 |"(l::'a::{linordered_idom,number_ring}) < m * n" |
|
128 |"- (l::'a::{linordered_idom,number_ring}) < m" |
|
129 |"(l::'a::{linordered_idom,number_ring}) < - m") = |
126 {* fn phi => Numeral_Simprocs.less_cancel_numerals *} |
130 {* fn phi => Numeral_Simprocs.less_cancel_numerals *} |
127 |
131 |
128 simproc_setup intle_cancel_numerals |
132 simproc_setup intle_cancel_numerals |
129 ("(l::'a::{linordered_idom,number_ring}) + m \<le> n" |
133 ("(l::'a::{linordered_idom,number_ring}) + m \<le> n" |
130 |"(l::'a::{linordered_idom,number_ring}) \<le> m + n" |
134 |"(l::'a::{linordered_idom,number_ring}) \<le> m + n" |
131 |"(l::'a::{linordered_idom,number_ring}) - m \<le> n" |
135 |"(l::'a::{linordered_idom,number_ring}) - m \<le> n" |
132 |"(l::'a::{linordered_idom,number_ring}) \<le> m - n" |
136 |"(l::'a::{linordered_idom,number_ring}) \<le> m - n" |
133 |"(l::'a::{linordered_idom,number_ring}) * m \<le> n" |
137 |"(l::'a::{linordered_idom,number_ring}) * m \<le> n" |
134 |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") = |
138 |"(l::'a::{linordered_idom,number_ring}) \<le> m * n" |
|
139 |"- (l::'a::{linordered_idom,number_ring}) \<le> m" |
|
140 |"(l::'a::{linordered_idom,number_ring}) \<le> - m") = |
135 {* fn phi => Numeral_Simprocs.le_cancel_numerals *} |
141 {* fn phi => Numeral_Simprocs.le_cancel_numerals *} |
136 |
142 |
137 simproc_setup ring_eq_cancel_numeral_factor |
143 simproc_setup ring_eq_cancel_numeral_factor |
138 ("(l::'a::{idom,number_ring}) * m = n" |
144 ("(l::'a::{idom,number_ring}) * m = n" |
139 |"(l::'a::{idom,number_ring}) = m * n") = |
145 |"(l::'a::{idom,number_ring}) = m * n") = |