67 |
68 |
68 notepad begin |
69 notepad begin |
69 fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1" |
70 fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1" |
70 { |
71 { |
71 assume "a + - b = u" have "(a + c) - (b + c) = u" |
72 assume "a + - b = u" have "(a + c) - (b + c) = u" |
72 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
73 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
73 next |
74 next |
74 assume "10 + (2 * l + oo) = uu" |
75 assume "10 + (2 * l + oo) = uu" |
75 have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" |
76 have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" |
76 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
77 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
77 next |
78 next |
78 assume "-3 + (i + (j + k)) = y" |
79 assume "-3 + (i + (j + k)) = y" |
79 have "(i + j + 12 + k) - 15 = y" |
80 have "(i + j + 12 + k) - 15 = y" |
80 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
81 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
81 next |
82 next |
82 assume "7 + (i + (j + k)) = y" |
83 assume "7 + (i + (j + k)) = y" |
83 have "(i + j + 12 + k) - 5 = y" |
84 have "(i + j + 12 + k) - 5 = y" |
84 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
85 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
85 next |
86 next |
86 assume "-4 * (u * v) + (2 * x + y) = w" |
87 assume "-4 * (u * v) + (2 * x + y) = w" |
87 have "(2*x - (u*v) + y) - v*3*u = w" |
88 have "(2*x - (u*v) + y) - v*3*u = w" |
88 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
89 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
89 next |
90 next |
90 assume "2 * x * u * v + y = w" |
91 assume "2 * x * u * v + y = w" |
91 have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w" |
92 have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w" |
92 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
93 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
93 next |
94 next |
94 assume "3 * (u * v) + (2 * x * u * v + y) = w" |
95 assume "3 * (u * v) + (2 * x * u * v + y) = w" |
95 have "(2*x*u*v + (u*v)*4 + y) - v*u = w" |
96 have "(2*x*u*v + (u*v)*4 + y) - v*u = w" |
96 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
97 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
97 next |
98 next |
98 assume "-3 * (u * v) + (- (x * u * v) + - y) = w" |
99 assume "-3 * (u * v) + (- (x * u * v) + - y) = w" |
99 have "u*v - (x*u*v + (u*v)*4 + y) = w" |
100 have "u*v - (x*u*v + (u*v)*4 + y) = w" |
100 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
101 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
101 next |
102 next |
102 assume "a + - c = d" |
103 assume "a + - c = d" |
103 have "a + -(b+c) + b = d" |
104 have "a + -(b+c) + b = d" |
104 apply (simp only: minus_add_distrib) |
105 apply (simp only: minus_add_distrib) |
105 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
106 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
106 next |
107 next |
107 assume "-2 * b + (a + - c) = d" |
108 assume "-2 * b + (a + - c) = d" |
108 have "a + -(b+c) - b = d" |
109 have "a + -(b+c) - b = d" |
109 apply (simp only: minus_add_distrib) |
110 apply (simp only: minus_add_distrib) |
110 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
111 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
111 next |
112 next |
112 assume "-7 + (i + (j + (k + (- u + - y)))) = z" |
113 assume "-7 + (i + (j + (k + (- u + - y)))) = z" |
113 have "(i + j + -2 + k) - (u + 5 + y) = z" |
114 have "(i + j + -2 + k) - (u + 5 + y) = z" |
114 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
115 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
115 next |
116 next |
116 assume "-27 + (i + (j + k)) = y" |
117 assume "-27 + (i + (j + k)) = y" |
117 have "(i + j + -12 + k) - 15 = y" |
118 have "(i + j + -12 + k) - 15 = y" |
118 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
119 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
119 next |
120 next |
120 assume "27 + (i + (j + k)) = y" |
121 assume "27 + (i + (j + k)) = y" |
121 have "(i + j + 12 + k) - -15 = y" |
122 have "(i + j + 12 + k) - -15 = y" |
122 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
123 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
123 next |
124 next |
124 assume "3 + (i + (j + k)) = y" |
125 assume "3 + (i + (j + k)) = y" |
125 have "(i + j + -12 + k) - -15 = y" |
126 have "(i + j + -12 + k) - -15 = y" |
126 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
127 by (tactic {* test @{context} [@{simproc int_combine_numerals}] *}) fact |
127 } |
128 } |
128 end |
129 end |
129 |
130 |
130 subsection {* @{text inteq_cancel_numerals} *} |
131 subsection {* @{text inteq_cancel_numerals} *} |
131 |
132 |
132 notepad begin |
133 notepad begin |
133 fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1" |
134 fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1" |
134 { |
135 { |
135 assume "u = 0" have "2*u = u" |
136 assume "u = 0" have "2*u = u" |
136 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
137 by (tactic {* test @{context} [@{simproc inteq_cancel_numerals}] *}) fact |
137 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
138 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
138 next |
139 next |
139 assume "i + (j + k) = 3 + (u + y)" |
140 assume "i + (j + k) = 3 + (u + y)" |
140 have "(i + j + 12 + k) = u + 15 + y" |
141 have "(i + j + 12 + k) = u + 15 + y" |
141 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
142 by (tactic {* test @{context} [@{simproc inteq_cancel_numerals}] *}) fact |
142 next |
143 next |
143 assume "7 + (j + (i + k)) = y" |
144 assume "7 + (j + (i + k)) = y" |
144 have "(i + j*2 + 12 + k) = j + 5 + y" |
145 have "(i + j*2 + 12 + k) = j + 5 + y" |
145 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
146 by (tactic {* test @{context} [@{simproc inteq_cancel_numerals}] *}) fact |
146 next |
147 next |
147 assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" |
148 assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" |
148 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" |
149 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" |
149 by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact |
150 by (tactic {* test @{context} [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact |
150 } |
151 } |
151 end |
152 end |
152 |
153 |
153 subsection {* @{text intless_cancel_numerals} *} |
154 subsection {* @{text intless_cancel_numerals} *} |
154 |
155 |
155 notepad begin |
156 notepad begin |
156 fix b c i j k u y :: "'a::linordered_idom" |
157 fix b c i j k u y :: "'a::linordered_idom" |
157 { |
158 { |
158 assume "y < 2 * b" have "y - b < b" |
159 assume "y < 2 * b" have "y - b < b" |
159 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
160 by (tactic {* test @{context} [@{simproc intless_cancel_numerals}] *}) fact |
160 next |
161 next |
161 assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" |
162 assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" |
162 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
163 by (tactic {* test @{context} [@{simproc intless_cancel_numerals}] *}) fact |
163 next |
164 next |
164 assume "i + (j + k) < 8 + (u + y)" |
165 assume "i + (j + k) < 8 + (u + y)" |
165 have "(i + j + -3 + k) < u + 5 + y" |
166 have "(i + j + -3 + k) < u + 5 + y" |
166 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
167 by (tactic {* test @{context} [@{simproc intless_cancel_numerals}] *}) fact |
167 next |
168 next |
168 assume "9 + (i + (j + k)) < u + y" |
169 assume "9 + (i + (j + k)) < u + y" |
169 have "(i + j + 3 + k) < u + -6 + y" |
170 have "(i + j + 3 + k) < u + -6 + y" |
170 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
171 by (tactic {* test @{context} [@{simproc intless_cancel_numerals}] *}) fact |
171 } |
172 } |
172 end |
173 end |
173 |
174 |
174 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
175 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
175 |
176 |
176 notepad begin |
177 notepad begin |
177 fix x y :: "'a::{idom,ring_char_0}" |
178 fix x y :: "'a::{idom,ring_char_0}" |
178 { |
179 { |
179 assume "3*x = 4*y" have "9*x = 12 * y" |
180 assume "3*x = 4*y" have "9*x = 12 * y" |
180 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
181 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
181 next |
182 next |
182 assume "-3*x = 4*y" have "-99*x = 132 * y" |
183 assume "-3*x = 4*y" have "-99*x = 132 * y" |
183 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
184 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
184 next |
185 next |
185 assume "111*x = -44*y" have "999*x = -396 * y" |
186 assume "111*x = -44*y" have "999*x = -396 * y" |
186 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
187 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
187 next |
188 next |
188 assume "11*x = 9*y" have "-99*x = -81 * y" |
189 assume "11*x = 9*y" have "-99*x = -81 * y" |
189 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
190 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
190 next |
191 next |
191 assume "2*x = y" have "-2 * x = -1 * y" |
192 assume "2*x = y" have "-2 * x = -1 * y" |
192 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
193 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
193 next |
194 next |
194 assume "2*x = y" have "-2 * x = -y" |
195 assume "2*x = y" have "-2 * x = -y" |
195 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
196 by (tactic {* test @{context} [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
196 } |
197 } |
197 end |
198 end |
198 |
199 |
199 subsection {* @{text int_div_cancel_numeral_factors} *} |
200 subsection {* @{text int_div_cancel_numeral_factors} *} |
200 |
201 |
201 notepad begin |
202 notepad begin |
202 fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}" |
203 fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}" |
203 { |
204 { |
204 assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" |
205 assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" |
205 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
206 by (tactic {* test @{context} [@{simproc int_div_cancel_numeral_factors}] *}) fact |
206 next |
207 next |
207 assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" |
208 assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" |
208 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
209 by (tactic {* test @{context} [@{simproc int_div_cancel_numeral_factors}] *}) fact |
209 next |
210 next |
210 assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z" |
211 assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z" |
211 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
212 by (tactic {* test @{context} [@{simproc int_div_cancel_numeral_factors}] *}) fact |
212 next |
213 next |
213 assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z" |
214 assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z" |
214 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
215 by (tactic {* test @{context} [@{simproc int_div_cancel_numeral_factors}] *}) fact |
215 next |
216 next |
216 assume "(2*x) div y = z" |
217 assume "(2*x) div y = z" |
217 have "(-2 * x) div (-1 * y) = z" |
218 have "(-2 * x) div (-1 * y) = z" |
218 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
219 by (tactic {* test @{context} [@{simproc int_div_cancel_numeral_factors}] *}) fact |
219 } |
220 } |
220 end |
221 end |
221 |
222 |
222 subsection {* @{text ring_less_cancel_numeral_factor} *} |
223 subsection {* @{text ring_less_cancel_numeral_factor} *} |
223 |
224 |
224 notepad begin |
225 notepad begin |
225 fix x y :: "'a::linordered_idom" |
226 fix x y :: "'a::linordered_idom" |
226 { |
227 { |
227 assume "3*x < 4*y" have "9*x < 12 * y" |
228 assume "3*x < 4*y" have "9*x < 12 * y" |
228 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
229 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
229 next |
230 next |
230 assume "-3*x < 4*y" have "-99*x < 132 * y" |
231 assume "-3*x < 4*y" have "-99*x < 132 * y" |
231 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
232 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
232 next |
233 next |
233 assume "111*x < -44*y" have "999*x < -396 * y" |
234 assume "111*x < -44*y" have "999*x < -396 * y" |
234 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
235 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
235 next |
236 next |
236 assume "9*y < 11*x" have "-99*x < -81 * y" |
237 assume "9*y < 11*x" have "-99*x < -81 * y" |
237 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
238 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
238 next |
239 next |
239 assume "y < 2*x" have "-2 * x < -y" |
240 assume "y < 2*x" have "-2 * x < -y" |
240 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
241 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
241 next |
242 next |
242 assume "23*y < x" have "-x < -23 * y" |
243 assume "23*y < x" have "-x < -23 * y" |
243 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
244 by (tactic {* test @{context} [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
244 } |
245 } |
245 end |
246 end |
246 |
247 |
247 subsection {* @{text ring_le_cancel_numeral_factor} *} |
248 subsection {* @{text ring_le_cancel_numeral_factor} *} |
248 |
249 |
249 notepad begin |
250 notepad begin |
250 fix x y :: "'a::linordered_idom" |
251 fix x y :: "'a::linordered_idom" |
251 { |
252 { |
252 assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" |
253 assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" |
253 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
254 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
254 next |
255 next |
255 assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y" |
256 assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y" |
256 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
257 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
257 next |
258 next |
258 assume "111*x \<le> -44*y" have "999*x \<le> -396 * y" |
259 assume "111*x \<le> -44*y" have "999*x \<le> -396 * y" |
259 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
260 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
260 next |
261 next |
261 assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y" |
262 assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y" |
262 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
263 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
263 next |
264 next |
264 assume "y \<le> 2*x" have "-2 * x \<le> -1 * y" |
265 assume "y \<le> 2*x" have "-2 * x \<le> -1 * y" |
265 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
266 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
266 next |
267 next |
267 assume "23*y \<le> x" have "-x \<le> -23 * y" |
268 assume "23*y \<le> x" have "-x \<le> -23 * y" |
268 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
269 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
269 next |
270 next |
270 assume "y \<le> 0" have "0 \<le> y * -2" |
271 assume "y \<le> 0" have "0 \<le> y * -2" |
271 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
272 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
272 next |
273 next |
273 assume "- x \<le> y" have "- (2 * x) \<le> 2*y" |
274 assume "- x \<le> y" have "- (2 * x) \<le> 2*y" |
274 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
275 by (tactic {* test @{context} [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
275 } |
276 } |
276 end |
277 end |
277 |
278 |
278 subsection {* @{text divide_cancel_numeral_factor} *} |
279 subsection {* @{text divide_cancel_numeral_factor} *} |
279 |
280 |
280 notepad begin |
281 notepad begin |
281 fix x y z :: "'a::{field_inverse_zero,ring_char_0}" |
282 fix x y z :: "'a::{field_inverse_zero,ring_char_0}" |
282 { |
283 { |
283 assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" |
284 assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" |
284 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
285 by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact |
285 next |
286 next |
286 assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" |
287 assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" |
287 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
288 by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact |
288 next |
289 next |
289 assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z" |
290 assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z" |
290 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
291 by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact |
291 next |
292 next |
292 assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z" |
293 assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z" |
293 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
294 by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact |
294 next |
295 next |
295 assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z" |
296 assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z" |
296 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
297 by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact |
297 } |
298 } |
298 end |
299 end |
299 |
300 |
300 subsection {* @{text ring_eq_cancel_factor} *} |
301 subsection {* @{text ring_eq_cancel_factor} *} |
301 |
302 |
302 notepad begin |
303 notepad begin |
303 fix a b c d k x y :: "'a::idom" |
304 fix a b c d k x y :: "'a::idom" |
304 { |
305 { |
305 assume "k = 0 \<or> x = y" have "x*k = k*y" |
306 assume "k = 0 \<or> x = y" have "x*k = k*y" |
306 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
307 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
307 next |
308 next |
308 assume "k = 0 \<or> 1 = y" have "k = k*y" |
309 assume "k = 0 \<or> 1 = y" have "k = k*y" |
309 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
310 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
310 next |
311 next |
311 assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b" |
312 assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b" |
312 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
313 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
313 next |
314 next |
314 assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)" |
315 assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)" |
315 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
316 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
316 next |
317 next |
317 assume "k = 0 \<or> x = y" have "x*k = k*y" |
318 assume "k = 0 \<or> x = y" have "x*k = k*y" |
318 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
319 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
319 next |
320 next |
320 assume "k = 0 \<or> 1 = y" have "k = k*y" |
321 assume "k = 0 \<or> 1 = y" have "k = k*y" |
321 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
322 by (tactic {* test @{context} [@{simproc ring_eq_cancel_factor}] *}) fact |
322 } |
323 } |
323 end |
324 end |
324 |
325 |
325 subsection {* @{text int_div_cancel_factor} *} |
326 subsection {* @{text int_div_cancel_factor} *} |
326 |
327 |
327 notepad begin |
328 notepad begin |
328 fix a b c d k uu x y :: "'a::semiring_div" |
329 fix a b c d k uu x y :: "'a::semiring_div" |
329 { |
330 { |
330 assume "(if k = 0 then 0 else x div y) = uu" |
331 assume "(if k = 0 then 0 else x div y) = uu" |
331 have "(x*k) div (k*y) = uu" |
332 have "(x*k) div (k*y) = uu" |
332 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
333 by (tactic {* test @{context} [@{simproc int_div_cancel_factor}] *}) fact |
333 next |
334 next |
334 assume "(if k = 0 then 0 else 1 div y) = uu" |
335 assume "(if k = 0 then 0 else 1 div y) = uu" |
335 have "(k) div (k*y) = uu" |
336 have "(k) div (k*y) = uu" |
336 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
337 by (tactic {* test @{context} [@{simproc int_div_cancel_factor}] *}) fact |
337 next |
338 next |
338 assume "(if b = 0 then 0 else a * c) = uu" |
339 assume "(if b = 0 then 0 else a * c) = uu" |
339 have "(a*(b*c)) div b = uu" |
340 have "(a*(b*c)) div b = uu" |
340 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
341 by (tactic {* test @{context} [@{simproc int_div_cancel_factor}] *}) fact |
341 next |
342 next |
342 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
343 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
343 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
344 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
344 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
345 by (tactic {* test @{context} [@{simproc int_div_cancel_factor}] *}) fact |
345 } |
346 } |
346 end |
347 end |
347 |
348 |
348 lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z" |
349 lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z" |
349 oops -- "FIXME: need simproc to cover this case" |
350 oops -- "FIXME: need simproc to cover this case" |
407 |
408 |
408 notepad begin |
409 notepad begin |
409 fix x y z :: "'a::linordered_idom" |
410 fix x y z :: "'a::linordered_idom" |
410 { |
411 { |
411 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z" |
412 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z" |
412 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
413 by (tactic {* test @{context} [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
413 next |
414 next |
414 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y" |
415 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y" |
415 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
416 by (tactic {* test @{context} [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
416 } |
417 } |
417 end |
418 end |
418 |
419 |
419 subsection {* @{text field_combine_numerals} *} |
420 subsection {* @{text field_combine_numerals} *} |
420 |
421 |
421 notepad begin |
422 notepad begin |
422 fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}" |
423 fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}" |
423 { |
424 { |
424 assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" |
425 assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" |
425 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
426 by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact |
426 next |
427 next |
427 assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" |
428 assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" |
428 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
429 by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact |
429 next |
430 next |
430 assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu" |
431 assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu" |
431 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
432 by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact |
432 next |
433 next |
433 assume "y + z = uu" |
434 assume "y + z = uu" |
434 have "x / 2 + y - 3 * x / 6 + z = uu" |
435 have "x / 2 + y - 3 * x / 6 + z = uu" |
435 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
436 by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact |
436 next |
437 next |
437 assume "1 / 15 * x + y = uu" |
438 assume "1 / 15 * x + y = uu" |
438 have "7 * x / 5 + y - 4 * x / 3 = uu" |
439 have "7 * x / 5 + y - 4 * x / 3 = uu" |
439 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
440 by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact |
440 } |
441 } |
441 end |
442 end |
442 |
443 |
443 lemma |
444 lemma |
444 fixes x :: "'a::{linordered_field_inverse_zero}" |
445 fixes x :: "'a::{linordered_field_inverse_zero}" |
445 shows "2/3 * x + x / 3 = uu" |
446 shows "2/3 * x + x / 3 = uu" |
446 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
447 apply (tactic {* test @{context} [@{simproc field_combine_numerals}] *})? |
447 oops -- "FIXME: test fails" |
448 oops -- "FIXME: test fails" |
448 |
449 |
449 subsection {* @{text nat_combine_numerals} *} |
450 subsection {* @{text nat_combine_numerals} *} |
450 |
451 |
451 notepad begin |
452 notepad begin |
452 fix i j k m n u :: nat |
453 fix i j k m n u :: nat |
453 { |
454 { |
454 assume "4*k = u" have "k + 3*k = u" |
455 assume "4*k = u" have "k + 3*k = u" |
455 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
456 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
456 next |
457 next |
457 (* FIXME "Suc (i + 3) \<equiv> i + 4" *) |
458 (* FIXME "Suc (i + 3) \<equiv> i + 4" *) |
458 assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" |
459 assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" |
459 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
460 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
460 next |
461 next |
461 (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *) |
462 (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *) |
462 assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" |
463 assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" |
463 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
464 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
464 next |
465 next |
465 assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" |
466 assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" |
466 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
467 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
467 next |
468 next |
468 assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u" |
469 assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u" |
469 have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u" |
470 have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u" |
470 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
471 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
471 next |
472 next |
472 assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" |
473 assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" |
473 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
474 by (tactic {* test @{context} [@{simproc nat_combine_numerals}] *}) fact |
474 } |
475 } |
475 end |
476 end |
476 |
477 |
477 subsection {* @{text nateq_cancel_numerals} *} |
478 subsection {* @{text nateq_cancel_numerals} *} |
478 |
479 |
479 notepad begin |
480 notepad begin |
480 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
481 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
481 { |
482 { |
482 assume "Suc 0 * u = 0" have "2*u = (u::nat)" |
483 assume "Suc 0 * u = 0" have "2*u = (u::nat)" |
483 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
484 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
484 next |
485 next |
485 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
486 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
486 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
487 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
487 next |
488 next |
488 assume "i + (j + k) = 3 * Suc 0 + (u + y)" |
489 assume "i + (j + k) = 3 * Suc 0 + (u + y)" |
489 have "(i + j + 12 + k) = u + 15 + y" |
490 have "(i + j + 12 + k) = u + 15 + y" |
490 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
491 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
491 next |
492 next |
492 assume "7 * Suc 0 + (i + (j + k)) = u + y" |
493 assume "7 * Suc 0 + (i + (j + k)) = u + y" |
493 have "(i + j + 12 + k) = u + 5 + y" |
494 have "(i + j + 12 + k) = u + 5 + y" |
494 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
495 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
495 next |
496 next |
496 assume "11 * Suc 0 + (i + (j + k)) = u + y" |
497 assume "11 * Suc 0 + (i + (j + k)) = u + y" |
497 have "(i + j + 12 + k) = Suc (u + y)" |
498 have "(i + j + 12 + k) = Suc (u + y)" |
498 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
499 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
499 next |
500 next |
500 assume "i + (j + k) = 2 * Suc 0 + (u + y)" |
501 assume "i + (j + k) = 2 * Suc 0 + (u + y)" |
501 have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))" |
502 have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))" |
502 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
503 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
503 next |
504 next |
504 assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0" |
505 assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0" |
505 have "2*y + 3*z + 2*u = Suc (u)" |
506 have "2*y + 3*z + 2*u = Suc (u)" |
506 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
507 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
507 next |
508 next |
508 assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0" |
509 assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0" |
509 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)" |
510 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)" |
510 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
511 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
511 next |
512 next |
512 assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = |
513 assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = |
513 2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))" |
514 2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))" |
514 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = |
515 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = |
515 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" |
516 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" |
516 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
517 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
517 next |
518 next |
518 assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv" |
519 assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv" |
519 have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)" |
520 have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)" |
520 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
521 by (tactic {* test @{context} [@{simproc nateq_cancel_numerals}] *}) fact |
521 } |
522 } |
522 end |
523 end |
523 |
524 |
524 subsection {* @{text natless_cancel_numerals} *} |
525 subsection {* @{text natless_cancel_numerals} *} |
525 |
526 |
526 notepad begin |
527 notepad begin |
527 fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a" |
528 fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a" |
528 fix c i j k l m oo u uu vv w y z w' y' z' :: "nat" |
529 fix c i j k l m oo u uu vv w y z w' y' z' :: "nat" |
529 { |
530 { |
530 assume "0 < j" have "(2*length xs < 2*length xs + j)" |
531 assume "0 < j" have "(2*length xs < 2*length xs + j)" |
531 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
532 by (tactic {* test @{context} [@{simproc natless_cancel_numerals}] *}) fact |
532 next |
533 next |
533 assume "0 < j" have "(2*length xs < length xs * 2 + j)" |
534 assume "0 < j" have "(2*length xs < length xs * 2 + j)" |
534 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
535 by (tactic {* test @{context} [@{simproc natless_cancel_numerals}] *}) fact |
535 next |
536 next |
536 assume "i + (j + k) < u + y" |
537 assume "i + (j + k) < u + y" |
537 have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))" |
538 have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))" |
538 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
539 by (tactic {* test @{context} [@{simproc natless_cancel_numerals}] *}) fact |
539 next |
540 next |
540 assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u" |
541 assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u" |
541 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
542 by (tactic {* test @{context} [@{simproc natless_cancel_numerals}] *}) fact |
542 } |
543 } |
543 end |
544 end |
544 |
545 |
545 subsection {* @{text natle_cancel_numerals} *} |
546 subsection {* @{text natle_cancel_numerals} *} |
546 |
547 |
548 fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a" |
549 fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a" |
549 fix c e i j k l oo u uu vv w y z w' y' z' :: "nat" |
550 fix c e i j k l oo u uu vv w y z w' y' z' :: "nat" |
550 { |
551 { |
551 assume "u + y \<le> 36 * Suc 0 + (i + (j + k))" |
552 assume "u + y \<le> 36 * Suc 0 + (i + (j + k))" |
552 have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)" |
553 have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)" |
553 by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact |
554 by (tactic {* test @{context} [@{simproc natle_cancel_numerals}] *}) fact |
554 next |
555 next |
555 assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0" |
556 assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0" |
556 have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)" |
557 have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)" |
557 by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact |
558 by (tactic {* test @{context} [@{simproc natle_cancel_numerals}] *}) fact |
558 next |
559 next |
559 assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1" |
560 assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1" |
560 by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact |
561 by (tactic {* test @{context} [@{simproc natle_cancel_numerals}] *}) fact |
561 next |
562 next |
562 assume "5 + length l3 = 0" |
563 assume "5 + length l3 = 0" |
563 have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \<le> length (compT P E A ST mxr e))" |
564 have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \<le> length (compT P E A ST mxr e))" |
564 by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact |
565 by (tactic {* test @{context} [@{simproc natle_cancel_numerals}] *}) fact |
565 next |
566 next |
566 assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0" |
567 assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0" |
567 have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \<le> length (compT P E A ST mxr e))" |
568 have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \<le> length (compT P E A ST mxr e))" |
568 by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact |
569 by (tactic {* test @{context} [@{simproc natle_cancel_numerals}] *}) fact |
569 } |
570 } |
570 end |
571 end |
571 |
572 |
572 subsection {* @{text natdiff_cancel_numerals} *} |
573 subsection {* @{text natdiff_cancel_numerals} *} |
573 |
574 |
574 notepad begin |
575 notepad begin |
575 fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a" |
576 fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a" |
576 fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat" |
577 fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat" |
577 { |
578 { |
578 assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y" |
579 assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y" |
579 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
580 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
580 next |
581 next |
581 assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y" |
582 assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y" |
582 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
583 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
583 next |
584 next |
584 assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y" |
585 assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y" |
585 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
586 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
586 next |
587 next |
587 assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y" |
588 assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y" |
588 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
589 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
589 next |
590 next |
590 assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y" |
591 assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y" |
591 have "(i + j + 2 + k) - 1 = y" |
592 have "(i + j + 2 + k) - 1 = y" |
592 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
593 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
593 next |
594 next |
594 assume "i + (j + k) - Suc 0 * Suc 0 = y" |
595 assume "i + (j + k) - Suc 0 * Suc 0 = y" |
595 have "(i + j + 1 + k) - 2 = y" |
596 have "(i + j + 1 + k) - 2 = y" |
596 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
597 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
597 next |
598 next |
598 assume "2 * x + y - 2 * (u * v) = w" |
599 assume "2 * x + y - 2 * (u * v) = w" |
599 have "(2*x + (u*v) + y) - v*3*u = w" |
600 have "(2*x + (u*v) + y) - v*3*u = w" |
600 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
601 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
601 next |
602 next |
602 assume "2 * x * u * v + (5 + y) - 0 = w" |
603 assume "2 * x * u * v + (5 + y) - 0 = w" |
603 have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w" |
604 have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w" |
604 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
605 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
605 next |
606 next |
606 assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w" |
607 assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w" |
607 have "(2*x*u*v + (u*v)*4 + y) - v*u = w" |
608 have "(2*x*u*v + (u*v)*4 + y) - v*u = w" |
608 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
609 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
609 next |
610 next |
610 assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w" |
611 assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w" |
611 have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w" |
612 have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w" |
612 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
613 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
613 next |
614 next |
614 assume "Suc (Suc 0 * (u * v)) - 0 = w" |
615 assume "Suc (Suc 0 * (u * v)) - 0 = w" |
615 have "Suc ((u*v)*4) - v*3*u = w" |
616 have "Suc ((u*v)*4) - v*3*u = w" |
616 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
617 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
617 next |
618 next |
618 assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w" |
619 assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w" |
619 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
620 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
620 next |
621 next |
621 assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz" |
622 assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz" |
622 have "(i + j + 32 + k) - (u + 15 + y) = zz" |
623 have "(i + j + 32 + k) - (u + 15 + y) = zz" |
623 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
624 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
624 next |
625 next |
625 assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v" |
626 assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v" |
626 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
627 by (tactic {* test @{context} [@{simproc natdiff_cancel_numerals}] *}) fact |
627 } |
628 } |
628 end |
629 end |
629 |
630 |
630 subsection {* Factor-cancellation simprocs for type @{typ nat} *} |
631 subsection {* Factor-cancellation simprocs for type @{typ nat} *} |
631 |
632 |
635 |
636 |
636 notepad begin |
637 notepad begin |
637 fix a b c d k x y uu :: nat |
638 fix a b c d k x y uu :: nat |
638 { |
639 { |
639 assume "k = 0 \<or> x = y" have "x*k = k*y" |
640 assume "k = 0 \<or> x = y" have "x*k = k*y" |
640 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
641 by (tactic {* test @{context} [@{simproc nat_eq_cancel_factor}] *}) fact |
641 next |
642 next |
642 assume "k = 0 \<or> Suc 0 = y" have "k = k*y" |
643 assume "k = 0 \<or> Suc 0 = y" have "k = k*y" |
643 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
644 by (tactic {* test @{context} [@{simproc nat_eq_cancel_factor}] *}) fact |
644 next |
645 next |
645 assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b" |
646 assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b" |
646 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
647 by (tactic {* test @{context} [@{simproc nat_eq_cancel_factor}] *}) fact |
647 next |
648 next |
648 assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)" |
649 assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)" |
649 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
650 by (tactic {* test @{context} [@{simproc nat_eq_cancel_factor}] *}) fact |
650 next |
651 next |
651 assume "0 < k \<and> x < y" have "x*k < k*y" |
652 assume "0 < k \<and> x < y" have "x*k < k*y" |
652 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
653 by (tactic {* test @{context} [@{simproc nat_less_cancel_factor}] *}) fact |
653 next |
654 next |
654 assume "0 < k \<and> Suc 0 < y" have "k < k*y" |
655 assume "0 < k \<and> Suc 0 < y" have "k < k*y" |
655 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
656 by (tactic {* test @{context} [@{simproc nat_less_cancel_factor}] *}) fact |
656 next |
657 next |
657 assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b" |
658 assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b" |
658 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
659 by (tactic {* test @{context} [@{simproc nat_less_cancel_factor}] *}) fact |
659 next |
660 next |
660 assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)" |
661 assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)" |
661 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
662 by (tactic {* test @{context} [@{simproc nat_less_cancel_factor}] *}) fact |
662 next |
663 next |
663 assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y" |
664 assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y" |
664 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
665 by (tactic {* test @{context} [@{simproc nat_le_cancel_factor}] *}) fact |
665 next |
666 next |
666 assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y" |
667 assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y" |
667 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
668 by (tactic {* test @{context} [@{simproc nat_le_cancel_factor}] *}) fact |
668 next |
669 next |
669 assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b" |
670 assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b" |
670 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
671 by (tactic {* test @{context} [@{simproc nat_le_cancel_factor}] *}) fact |
671 next |
672 next |
672 assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)" |
673 assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)" |
673 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
674 by (tactic {* test @{context} [@{simproc nat_le_cancel_factor}] *}) fact |
674 next |
675 next |
675 assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu" |
676 assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu" |
676 by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact |
677 by (tactic {* test @{context} [@{simproc nat_div_cancel_factor}] *}) fact |
677 next |
678 next |
678 assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu" |
679 assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu" |
679 by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact |
680 by (tactic {* test @{context} [@{simproc nat_div_cancel_factor}] *}) fact |
680 next |
681 next |
681 assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu" |
682 assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu" |
682 by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact |
683 by (tactic {* test @{context} [@{simproc nat_div_cancel_factor}] *}) fact |
683 next |
684 next |
684 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
685 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
685 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
686 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
686 by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact |
687 by (tactic {* test @{context} [@{simproc nat_div_cancel_factor}] *}) fact |
687 next |
688 next |
688 assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)" |
689 assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)" |
689 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
690 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_factor}] *}) fact |
690 next |
691 next |
691 assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)" |
692 assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)" |
692 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
693 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_factor}] *}) fact |
693 next |
694 next |
694 assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" |
695 assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" |
695 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
696 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_factor}] *}) fact |
696 next |
697 next |
697 assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))" |
698 assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))" |
698 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
699 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_factor}] *}) fact |
699 next |
700 next |
700 assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" |
701 assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" |
701 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
702 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_factor}] *}) fact |
702 } |
703 } |
703 end |
704 end |
704 |
705 |
705 subsection {* Numeral-cancellation simprocs for type @{typ nat} *} |
706 subsection {* Numeral-cancellation simprocs for type @{typ nat} *} |
706 |
707 |
707 notepad begin |
708 notepad begin |
708 fix x y z :: nat |
709 fix x y z :: nat |
709 { |
710 { |
710 assume "3 * x = 4 * y" have "9*x = 12 * y" |
711 assume "3 * x = 4 * y" have "9*x = 12 * y" |
711 by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact |
712 by (tactic {* test @{context} [@{simproc nat_eq_cancel_numeral_factor}] *}) fact |
712 next |
713 next |
713 assume "3 * x < 4 * y" have "9*x < 12 * y" |
714 assume "3 * x < 4 * y" have "9*x < 12 * y" |
714 by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact |
715 by (tactic {* test @{context} [@{simproc nat_less_cancel_numeral_factor}] *}) fact |
715 next |
716 next |
716 assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y" |
717 assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y" |
717 by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact |
718 by (tactic {* test @{context} [@{simproc nat_le_cancel_numeral_factor}] *}) fact |
718 next |
719 next |
719 assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z" |
720 assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z" |
720 by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact |
721 by (tactic {* test @{context} [@{simproc nat_div_cancel_numeral_factor}] *}) fact |
721 next |
722 next |
722 assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)" |
723 assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)" |
723 by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact |
724 by (tactic {* test @{context} [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact |
724 } |
725 } |
725 end |
726 end |
726 |
727 |
727 subsection {* Integer numeral div/mod simprocs *} |
728 subsection {* Integer numeral div/mod simprocs *} |
728 |
729 |
729 notepad begin |
730 notepad begin |
730 have "(10::int) div 3 = 3" |
731 have "(10::int) div 3 = 3" |
731 by (tactic {* test [@{simproc binary_int_div}] *}) |
732 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
732 have "(10::int) mod 3 = 1" |
733 have "(10::int) mod 3 = 1" |
733 by (tactic {* test [@{simproc binary_int_mod}] *}) |
734 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
734 have "(10::int) div -3 = -4" |
735 have "(10::int) div -3 = -4" |
735 by (tactic {* test [@{simproc binary_int_div}] *}) |
736 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
736 have "(10::int) mod -3 = -2" |
737 have "(10::int) mod -3 = -2" |
737 by (tactic {* test [@{simproc binary_int_mod}] *}) |
738 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
738 have "(-10::int) div 3 = -4" |
739 have "(-10::int) div 3 = -4" |
739 by (tactic {* test [@{simproc binary_int_div}] *}) |
740 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
740 have "(-10::int) mod 3 = 2" |
741 have "(-10::int) mod 3 = 2" |
741 by (tactic {* test [@{simproc binary_int_mod}] *}) |
742 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
742 have "(-10::int) div -3 = 3" |
743 have "(-10::int) div -3 = 3" |
743 by (tactic {* test [@{simproc binary_int_div}] *}) |
744 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
744 have "(-10::int) mod -3 = -1" |
745 have "(-10::int) mod -3 = -1" |
745 by (tactic {* test [@{simproc binary_int_mod}] *}) |
746 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
746 have "(8452::int) mod 3 = 1" |
747 have "(8452::int) mod 3 = 1" |
747 by (tactic {* test [@{simproc binary_int_mod}] *}) |
748 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
748 have "(59485::int) div 434 = 137" |
749 have "(59485::int) div 434 = 137" |
749 by (tactic {* test [@{simproc binary_int_div}] *}) |
750 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
750 have "(1000006::int) mod 10 = 6" |
751 have "(1000006::int) mod 10 = 6" |
751 by (tactic {* test [@{simproc binary_int_mod}] *}) |
752 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
752 have "10000000 div 2 = (5000000::int)" |
753 have "10000000 div 2 = (5000000::int)" |
753 by (tactic {* test [@{simproc binary_int_div}] *}) |
754 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
754 have "10000001 mod 2 = (1::int)" |
755 have "10000001 mod 2 = (1::int)" |
755 by (tactic {* test [@{simproc binary_int_mod}] *}) |
756 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
756 have "10000055 div 32 = (312501::int)" |
757 have "10000055 div 32 = (312501::int)" |
757 by (tactic {* test [@{simproc binary_int_div}] *}) |
758 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
758 have "10000055 mod 32 = (23::int)" |
759 have "10000055 mod 32 = (23::int)" |
759 by (tactic {* test [@{simproc binary_int_mod}] *}) |
760 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
760 have "100094 div 144 = (695::int)" |
761 have "100094 div 144 = (695::int)" |
761 by (tactic {* test [@{simproc binary_int_div}] *}) |
762 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
762 have "100094 mod 144 = (14::int)" |
763 have "100094 mod 144 = (14::int)" |
763 by (tactic {* test [@{simproc binary_int_mod}] *}) |
764 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
764 end |
765 end |
765 |
766 |
766 end |
767 end |