src/HOL/ex/Simproc_Tests.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 48559 686cc7c47589 child 51717 9e7d1c139569 permissions -rw-r--r--
introduce order topology
1 (*  Title:      HOL/ex/Simproc_Tests.thy
2     Author:     Brian Huffman
3 *)
5 header {* Testing of arithmetic simprocs *}
7 theory Simproc_Tests
8 imports Main
9 begin
11 text {*
12   This theory tests the various simprocs defined in @{file
13   "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
14   Many of the tests are derived from commented-out code originally
15   found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
16 *}
18 subsection {* ML bindings *}
20 ML {*
21   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
22 *}
24 subsection {* Cancellation simprocs from @{text Nat.thy} *}
27   fix a b c d :: nat
28   {
29     assume "b = Suc c" have "a + b = Suc (c + a)"
30       by (tactic {* test [@{simproc nateq_cancel_sums}] *}) fact
31   next
32     assume "b < Suc c" have "a + b < Suc (c + a)"
33       by (tactic {* test [@{simproc natless_cancel_sums}] *}) fact
34   next
35     assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
36       by (tactic {* test [@{simproc natle_cancel_sums}] *}) fact
37   next
38     assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
39       by (tactic {* test [@{simproc natdiff_cancel_sums}] *}) fact
40   }
41 end
43 schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
44   by (tactic {* test [@{simproc natle_cancel_sums}] *}) (rule le0)
45 (* TODO: test more simprocs with schematic variables *)
47 subsection {* Abelian group cancellation simprocs *}
50   fix a b c u :: "'a::ab_group_add"
51   {
52     assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
53       by (tactic {* test [@{simproc group_cancel_diff}] *}) fact
54   next
55     assume "a + 0 = b + 0" have "a + c = b + c"
56       by (tactic {* test [@{simproc group_cancel_eq}] *}) fact
57   }
58 end
59 (* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
61 subsection {* @{text int_combine_numerals} *}
63 (* FIXME: int_combine_numerals often unnecessarily regroups addition
64 and rewrites subtraction to negation. Ideally it should behave more
65 like Groups.abel_cancel_sum, preserving the shape of terms as much as
66 possible. *)
69   fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1"
70   {
71     assume "a + - b = u" have "(a + c) - (b + c) = u"
72       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
73   next
74     assume "10 + (2 * l + oo) = uu"
75     have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
76       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
77   next
78     assume "-3 + (i + (j + k)) = y"
79     have "(i + j + 12 + k) - 15 = y"
80       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
81   next
82     assume "7 + (i + (j + k)) = y"
83     have "(i + j + 12 + k) - 5 = y"
84       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
85   next
86     assume "-4 * (u * v) + (2 * x + y) = w"
87     have "(2*x - (u*v) + y) - v*3*u = w"
88       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
89   next
90     assume "2 * x * u * v + y = w"
91     have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
92       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
93   next
94     assume "3 * (u * v) + (2 * x * u * v + y) = w"
95     have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
96       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
97   next
98     assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
99     have "u*v - (x*u*v + (u*v)*4 + y) = w"
100       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
101   next
102     assume "a + - c = d"
103     have "a + -(b+c) + b = d"
104       apply (simp only: minus_add_distrib)
105       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
106   next
107     assume "-2 * b + (a + - c) = d"
108     have "a + -(b+c) - b = d"
109       apply (simp only: minus_add_distrib)
110       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
111   next
112     assume "-7 + (i + (j + (k + (- u + - y)))) = z"
113     have "(i + j + -2 + k) - (u + 5 + y) = z"
114       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
115   next
116     assume "-27 + (i + (j + k)) = y"
117     have "(i + j + -12 + k) - 15 = y"
118       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
119   next
120     assume "27 + (i + (j + k)) = y"
121     have "(i + j + 12 + k) - -15 = y"
122       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
123   next
124     assume "3 + (i + (j + k)) = y"
125     have "(i + j + -12 + k) - -15 = y"
126       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
127   }
128 end
130 subsection {* @{text inteq_cancel_numerals} *}
133   fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1"
134   {
135     assume "u = 0" have "2*u = u"
136       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
137 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
138   next
139     assume "i + (j + k) = 3 + (u + y)"
140     have "(i + j + 12 + k) = u + 15 + y"
141       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
142   next
143     assume "7 + (j + (i + k)) = y"
144     have "(i + j*2 + 12 + k) = j + 5 + y"
145       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
146   next
147     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       by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
150   }
151 end
153 subsection {* @{text intless_cancel_numerals} *}
156   fix b c i j k u y :: "'a::linordered_idom"
157   {
158     assume "y < 2 * b" have "y - b < b"
159       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
160   next
161     assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
162       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
163   next
164     assume "i + (j + k) < 8 + (u + y)"
165     have "(i + j + -3 + k) < u + 5 + y"
166       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
167   next
168     assume "9 + (i + (j + k)) < u + y"
169     have "(i + j + 3 + k) < u + -6 + y"
170       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
171   }
172 end
174 subsection {* @{text ring_eq_cancel_numeral_factor} *}
177   fix x y :: "'a::{idom,ring_char_0}"
178   {
179     assume "3*x = 4*y" have "9*x = 12 * y"
180       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
181   next
182     assume "-3*x = 4*y" have "-99*x = 132 * y"
183       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
184   next
185     assume "111*x = -44*y" have "999*x = -396 * y"
186       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
187   next
188     assume "11*x = 9*y" have "-99*x = -81 * y"
189       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
190   next
191     assume "2*x = y" have "-2 * x = -1 * y"
192       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
193   next
194     assume "2*x = y" have "-2 * x = -y"
195       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
196   }
197 end
199 subsection {* @{text int_div_cancel_numeral_factors} *}
202   fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
203   {
204     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   next
207     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   next
210     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   next
213     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   next
216     assume "(2*x) div y = z"
217     have "(-2 * x) div (-1 * y) = z"
218       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
219   }
220 end
222 subsection {* @{text ring_less_cancel_numeral_factor} *}
225   fix x y :: "'a::linordered_idom"
226   {
227     assume "3*x < 4*y" have "9*x < 12 * y"
228       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
229   next
230     assume "-3*x < 4*y" have "-99*x < 132 * y"
231       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
232   next
233     assume "111*x < -44*y" have "999*x < -396 * y"
234       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
235   next
236     assume "9*y < 11*x" have "-99*x < -81 * y"
237       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
238   next
239     assume "y < 2*x" have "-2 * x < -y"
240       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
241   next
242     assume "23*y < x" have "-x < -23 * y"
243       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
244   }
245 end
247 subsection {* @{text ring_le_cancel_numeral_factor} *}
250   fix x y :: "'a::linordered_idom"
251   {
252     assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
253       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
254   next
255     assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
256       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
257   next
258     assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
259       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
260   next
261     assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
262       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
263   next
264     assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
265       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
266   next
267     assume "23*y \<le> x" have "-x \<le> -23 * y"
268       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
269   next
270     assume "y \<le> 0" have "0 \<le> y * -2"
271       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
272   next
273     assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
274       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
275   }
276 end
278 subsection {* @{text divide_cancel_numeral_factor} *}
281   fix x y z :: "'a::{field_inverse_zero,ring_char_0}"
282   {
283     assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
284       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
285   next
286     assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
287       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
288   next
289     assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
290       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
291   next
292     assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
293       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
294   next
295     assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
296       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
297   }
298 end
300 subsection {* @{text ring_eq_cancel_factor} *}
303   fix a b c d k x y :: "'a::idom"
304   {
305     assume "k = 0 \<or> x = y" have "x*k = k*y"
306       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
307   next
308     assume "k = 0 \<or> 1 = y" have "k = k*y"
309       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
310   next
311     assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
312       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
313   next
314     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   next
317     assume "k = 0 \<or> x = y" have "x*k = k*y"
318       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
319   next
320     assume "k = 0 \<or> 1 = y" have "k = k*y"
321       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
322   }
323 end
325 subsection {* @{text int_div_cancel_factor} *}
328   fix a b c d k uu x y :: "'a::semiring_div"
329   {
330     assume "(if k = 0 then 0 else x div y) = uu"
331     have "(x*k) div (k*y) = uu"
332       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
333   next
334     assume "(if k = 0 then 0 else 1 div y) = uu"
335     have "(k) div (k*y) = uu"
336       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
337   next
338     assume "(if b = 0 then 0 else a * c) = uu"
339     have "(a*(b*c)) div b = uu"
340       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
341   next
342     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       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
345   }
346 end
348 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"
351 subsection {* @{text divide_cancel_factor} *}
354   fix a b c d k uu x y :: "'a::field_inverse_zero"
355   {
356     assume "(if k = 0 then 0 else x / y) = uu"
357     have "(x*k) / (k*y) = uu"
358       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
359   next
360     assume "(if k = 0 then 0 else 1 / y) = uu"
361     have "(k) / (k*y) = uu"
362       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
363   next
364     assume "(if b = 0 then 0 else a * c / 1) = uu"
365     have "(a*(b*c)) / b = uu"
366       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
367   next
368     assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
369     have "(a*(b*c)) / (d*b*(x*a)) = uu"
370       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
371   }
372 end
374 lemma
375   fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
376   shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
377 oops -- "FIXME: need simproc to cover this case"
379 subsection {* @{text linordered_ring_less_cancel_factor} *}
382   fix x y z :: "'a::linordered_idom"
383   {
384     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
385       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
386   next
387     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
388       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
389   next
390     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
391       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
392   next
393     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
394       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
395   next
396     txt "This simproc now uses the simplifier to prove that terms to
397       be canceled are positive/negative."
398     assume z_pos: "0 < z"
399     assume "x < y" have "z*x < z*y"
400       by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
401         addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
402         addsimps [@{thm z_pos}]) 1) *}) fact
403   }
404 end
406 subsection {* @{text linordered_ring_le_cancel_factor} *}
409   fix x y z :: "'a::linordered_idom"
410   {
411     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   next
414     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   }
417 end
419 subsection {* @{text field_combine_numerals} *}
422   fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}"
423   {
424     assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
425       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
426   next
427     assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
428       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
429   next
430     assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
431       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
432   next
433     assume "y + z = uu"
434     have "x / 2 + y - 3 * x / 6 + z = uu"
435       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
436   next
437     assume "1 / 15 * x + y = uu"
438     have "7 * x / 5 + y - 4 * x / 3 = uu"
439       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
440   }
441 end
443 lemma
444   fixes x :: "'a::{linordered_field_inverse_zero}"
445   shows "2/3 * x + x / 3 = uu"
446 apply (tactic {* test [@{simproc field_combine_numerals}] *})?
447 oops -- "FIXME: test fails"
449 subsection {* @{text nat_combine_numerals} *}
452   fix i j k m n u :: nat
453   {
454     assume "4*k = u" have "k + 3*k = u"
455       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
456   next
457     (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
458     assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
459       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
460   next
461     (* 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       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
464   next
465     assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
466       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
467   next
468     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       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
471   next
472     assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
473       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
474   }
475 end
477 subsection {* @{text nateq_cancel_numerals} *}
480   fix i j k l oo u uu vv w y z w' y' z' :: "nat"
481   {
482     assume "Suc 0 * u = 0" have "2*u = (u::nat)"
483       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
484   next
485     assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
486       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
487   next
488     assume "i + (j + k) = 3 * Suc 0 + (u + y)"
489     have "(i + j + 12 + k) = u + 15 + y"
490       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
491   next
492     assume "7 * Suc 0 + (i + (j + k)) = u + y"
493     have "(i + j + 12 + k) = u + 5 + y"
494       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
495   next
496     assume "11 * Suc 0 + (i + (j + k)) = u + y"
497     have "(i + j + 12 + k) = Suc (u + y)"
498       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
499   next
500     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       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
503   next
504     assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
505     have "2*y + 3*z + 2*u = Suc (u)"
506       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
507   next
508     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       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
511   next
512     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     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       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
517   next
518     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       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
521   }
522 end
524 subsection {* @{text natless_cancel_numerals} *}
527   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   {
530     assume "0 < j" have "(2*length xs < 2*length xs + j)"
531       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
532   next
533     assume "0 < j" have "(2*length xs < length xs * 2 + j)"
534       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
535   next
536     assume "i + (j + k) < u + y"
537     have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
538       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
539   next
540     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   }
543 end
545 subsection {* @{text natle_cancel_numerals} *}
548   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   {
551     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       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
554   next
555     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       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
558   next
559     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   next
562     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       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
565   next
566     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       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
569   }
570 end
572 subsection {* @{text natdiff_cancel_numerals} *}
575   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   {
578     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   next
581     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   next
584     assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
585       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
586   next
587     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   next
590     assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
591     have "(i + j + 2 + k) - 1 = y"
592       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
593   next
594     assume "i + (j + k) - Suc 0 * Suc 0 = y"
595     have "(i + j + 1 + k) - 2 = y"
596       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
597   next
598     assume "2 * x + y - 2 * (u * v) = w"
599     have "(2*x + (u*v) + y) - v*3*u = w"
600       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
601   next
602     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       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
605   next
606     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       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
609   next
610     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       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
613   next
614     assume "Suc (Suc 0 * (u * v)) - 0 = w"
615     have "Suc ((u*v)*4) - v*3*u = w"
616       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
617   next
618     assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
619       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
620   next
621     assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
622     have "(i + j + 32 + k) - (u + 15 + y) = zz"
623       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
624   next
625     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   }
628 end
630 subsection {* Factor-cancellation simprocs for type @{typ nat} *}
632 text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
633 @{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
634 @{text nat_dvd_cancel_factor}. *}
637   fix a b c d k x y uu :: nat
638   {
639     assume "k = 0 \<or> x = y" have "x*k = k*y"
640       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
641   next
642     assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
643       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
644   next
645     assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
646       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
647   next
648     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   next
651     assume "0 < k \<and> x < y" have "x*k < k*y"
652       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
653   next
654     assume "0 < k \<and> Suc 0 < y" have "k < k*y"
655       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
656   next
657     assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
658       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
659   next
660     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   next
663     assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
664       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
665   next
666     assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
667       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
668   next
669     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   next
672     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   next
675     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   next
678     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   next
681     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   next
684     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       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
687   next
688     assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
689       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
690   next
691     assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
692       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
693   next
694     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   next
697     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   next
700     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   }
703 end
705 subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
708   fix x y z :: nat
709   {
710     assume "3 * x = 4 * y" have "9*x = 12 * y"
711       by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
712   next
713     assume "3 * x < 4 * y" have "9*x < 12 * y"
714       by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
715   next
716     assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
717       by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
718   next
719     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   next
722     assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
723       by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
724   }
725 end
727 subsection {* Integer numeral div/mod simprocs *}
730   have "(10::int) div 3 = 3"
731     by (tactic {* test [@{simproc binary_int_div}] *})
732   have "(10::int) mod 3 = 1"
733     by (tactic {* test [@{simproc binary_int_mod}] *})
734   have "(10::int) div -3 = -4"
735     by (tactic {* test [@{simproc binary_int_div}] *})
736   have "(10::int) mod -3 = -2"
737     by (tactic {* test [@{simproc binary_int_mod}] *})
738   have "(-10::int) div 3 = -4"
739     by (tactic {* test [@{simproc binary_int_div}] *})
740   have "(-10::int) mod 3 = 2"
741     by (tactic {* test [@{simproc binary_int_mod}] *})
742   have "(-10::int) div -3 = 3"
743     by (tactic {* test [@{simproc binary_int_div}] *})
744   have "(-10::int) mod -3 = -1"
745     by (tactic {* test [@{simproc binary_int_mod}] *})
746   have "(8452::int) mod 3 = 1"
747     by (tactic {* test [@{simproc binary_int_mod}] *})
748   have "(59485::int) div 434 = 137"
749     by (tactic {* test [@{simproc binary_int_div}] *})
750   have "(1000006::int) mod 10 = 6"
751     by (tactic {* test [@{simproc binary_int_mod}] *})
752   have "10000000 div 2 = (5000000::int)"
753     by (tactic {* test [@{simproc binary_int_div}] *})
754   have "10000001 mod 2 = (1::int)"
755     by (tactic {* test [@{simproc binary_int_mod}] *})
756   have "10000055 div 32 = (312501::int)"
757     by (tactic {* test [@{simproc binary_int_div}] *})
758   have "10000055 mod 32 = (23::int)"
759     by (tactic {* test [@{simproc binary_int_mod}] *})
760   have "100094 div 144 = (695::int)"
761     by (tactic {* test [@{simproc binary_int_div}] *})
762   have "100094 mod 144 = (14::int)"
763     by (tactic {* test [@{simproc binary_int_mod}] *})
764 end
766 end