equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Testing of arithmetic simprocs *} |
5 header {* Testing of arithmetic simprocs *} |
6 |
6 |
7 theory Simproc_Tests |
7 theory Simproc_Tests |
8 imports Main |
8 imports (*Main*) "../Numeral_Simprocs" |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 This theory tests the various simprocs defined in |
12 This theory tests the various simprocs defined in |
13 @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests |
13 @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests |
41 and rewrites subtraction to negation. Ideally it should behave more |
41 and rewrites subtraction to negation. Ideally it should behave more |
42 like Groups.abel_cancel_sum, preserving the shape of terms as much as |
42 like Groups.abel_cancel_sum, preserving the shape of terms as much as |
43 possible. *) |
43 possible. *) |
44 |
44 |
45 notepad begin |
45 notepad begin |
46 fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring" |
46 fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1" |
47 { |
47 { |
48 assume "a + - b = u" have "(a + c) - (b + c) = u" |
48 assume "a + - b = u" have "(a + c) - (b + c) = u" |
49 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
49 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
50 next |
50 next |
51 assume "10 + (2 * l + oo) = uu" |
51 assume "10 + (2 * l + oo) = uu" |
105 end |
105 end |
106 |
106 |
107 subsection {* @{text inteq_cancel_numerals} *} |
107 subsection {* @{text inteq_cancel_numerals} *} |
108 |
108 |
109 notepad begin |
109 notepad begin |
110 fix i j k u vv w y z w' y' z' :: "'a::number_ring" |
110 fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1" |
111 { |
111 { |
112 assume "u = 0" have "2*u = u" |
112 assume "u = 0" have "2*u = u" |
113 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
113 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
114 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
114 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
115 next |
115 next |
128 end |
128 end |
129 |
129 |
130 subsection {* @{text intless_cancel_numerals} *} |
130 subsection {* @{text intless_cancel_numerals} *} |
131 |
131 |
132 notepad begin |
132 notepad begin |
133 fix b c i j k u y :: "'a::{linordered_idom,number_ring}" |
133 fix b c i j k u y :: "'a::linordered_idom" |
134 { |
134 { |
135 assume "y < 2 * b" have "y - b < b" |
135 assume "y < 2 * b" have "y - b < b" |
136 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
136 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
137 next |
137 next |
138 assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" |
138 assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" |
149 end |
149 end |
150 |
150 |
151 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
151 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
152 |
152 |
153 notepad begin |
153 notepad begin |
154 fix x y :: "'a::{idom,ring_char_0,number_ring}" |
154 fix x y :: "'a::{idom,ring_char_0}" |
155 { |
155 { |
156 assume "3*x = 4*y" have "9*x = 12 * y" |
156 assume "3*x = 4*y" have "9*x = 12 * y" |
157 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
157 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
158 next |
158 next |
159 assume "-3*x = 4*y" have "-99*x = 132 * y" |
159 assume "-3*x = 4*y" have "-99*x = 132 * y" |
174 end |
174 end |
175 |
175 |
176 subsection {* @{text int_div_cancel_numeral_factors} *} |
176 subsection {* @{text int_div_cancel_numeral_factors} *} |
177 |
177 |
178 notepad begin |
178 notepad begin |
179 fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}" |
179 fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}" |
180 { |
180 { |
181 assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" |
181 assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" |
182 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
182 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
183 next |
183 next |
184 assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" |
184 assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" |
197 end |
197 end |
198 |
198 |
199 subsection {* @{text ring_less_cancel_numeral_factor} *} |
199 subsection {* @{text ring_less_cancel_numeral_factor} *} |
200 |
200 |
201 notepad begin |
201 notepad begin |
202 fix x y :: "'a::{linordered_idom,number_ring}" |
202 fix x y :: "'a::linordered_idom" |
203 { |
203 { |
204 assume "3*x < 4*y" have "9*x < 12 * y" |
204 assume "3*x < 4*y" have "9*x < 12 * y" |
205 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
205 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
206 next |
206 next |
207 assume "-3*x < 4*y" have "-99*x < 132 * y" |
207 assume "-3*x < 4*y" have "-99*x < 132 * y" |
222 end |
222 end |
223 |
223 |
224 subsection {* @{text ring_le_cancel_numeral_factor} *} |
224 subsection {* @{text ring_le_cancel_numeral_factor} *} |
225 |
225 |
226 notepad begin |
226 notepad begin |
227 fix x y :: "'a::{linordered_idom,number_ring}" |
227 fix x y :: "'a::linordered_idom" |
228 { |
228 { |
229 assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" |
229 assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" |
230 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
230 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
231 next |
231 next |
232 assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y" |
232 assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y" |
253 end |
253 end |
254 |
254 |
255 subsection {* @{text divide_cancel_numeral_factor} *} |
255 subsection {* @{text divide_cancel_numeral_factor} *} |
256 |
256 |
257 notepad begin |
257 notepad begin |
258 fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}" |
258 fix x y z :: "'a::{field_inverse_zero,ring_char_0}" |
259 { |
259 { |
260 assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" |
260 assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" |
261 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
261 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
262 next |
262 next |
263 assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" |
263 assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" |
319 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
319 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
320 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
320 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
321 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
321 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
322 } |
322 } |
323 end |
323 end |
|
324 |
|
325 lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z" |
|
326 oops -- "FIXME: need simproc to cover this case" |
324 |
327 |
325 subsection {* @{text divide_cancel_factor} *} |
328 subsection {* @{text divide_cancel_factor} *} |
326 |
329 |
327 notepad begin |
330 notepad begin |
328 fix a b c d k uu x y :: "'a::field_inverse_zero" |
331 fix a b c d k uu x y :: "'a::field_inverse_zero" |
391 end |
394 end |
392 |
395 |
393 subsection {* @{text field_combine_numerals} *} |
396 subsection {* @{text field_combine_numerals} *} |
394 |
397 |
395 notepad begin |
398 notepad begin |
396 fix x y z uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}" |
399 fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}" |
397 { |
400 { |
398 assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" |
401 assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" |
399 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
402 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
400 next |
403 next |
401 assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" |
404 assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" |
413 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
416 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
414 } |
417 } |
415 end |
418 end |
416 |
419 |
417 lemma |
420 lemma |
418 fixes x :: "'a::{linordered_field_inverse_zero,number_ring}" |
421 fixes x :: "'a::{linordered_field_inverse_zero}" |
419 shows "2/3 * x + x / 3 = uu" |
422 shows "2/3 * x + x / 3 = uu" |
420 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
423 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
421 oops -- "FIXME: test fails" |
424 oops -- "FIXME: test fails" |
422 |
425 |
423 subsection {* @{text nat_combine_numerals} *} |
426 subsection {* @{text nat_combine_numerals} *} |
446 assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" |
449 assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" |
447 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
450 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
448 } |
451 } |
449 end |
452 end |
450 |
453 |
451 (*negative numerals: FAIL*) |
|
452 lemma "Suc (i + j + -3 + k) = u" |
|
453 apply (tactic {* test [@{simproc nat_combine_numerals}] *})? |
|
454 oops |
|
455 |
|
456 subsection {* @{text nateq_cancel_numerals} *} |
454 subsection {* @{text nateq_cancel_numerals} *} |
457 |
455 |
458 notepad begin |
456 notepad begin |
459 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
457 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
460 { |
458 { |
461 assume "Suc 0 * u = 0" have "2*u = u" |
459 assume "Suc 0 * u = 0" have "2*u = (u::nat)" |
462 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
460 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
463 next |
461 next |
464 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
462 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
465 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
463 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
466 next |
464 next |
502 |
500 |
503 subsection {* @{text natless_cancel_numerals} *} |
501 subsection {* @{text natless_cancel_numerals} *} |
504 |
502 |
505 notepad begin |
503 notepad begin |
506 fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a" |
504 fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a" |
507 fix c i j k l oo u uu vv w y z w' y' z' :: "nat" |
505 fix c i j k l m oo u uu vv w y z w' y' z' :: "nat" |
508 { |
506 { |
509 assume "0 < j" have "(2*length xs < 2*length xs + j)" |
507 assume "0 < j" have "(2*length xs < 2*length xs + j)" |
510 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
508 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
511 next |
509 next |
512 assume "0 < j" have "(2*length xs < length xs * 2 + j)" |
510 assume "0 < j" have "(2*length xs < length xs * 2 + j)" |
516 have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))" |
514 have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))" |
517 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
515 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
518 next |
516 next |
519 assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u" |
517 assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u" |
520 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
518 by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact |
521 next |
|
522 (* FIXME: negative numerals fail |
|
523 have "(i + j + -23 + (k::nat)) < u + 15 + y" |
|
524 apply (tactic {* test [@{simproc natless_cancel_numerals}] *})? |
|
525 sorry |
|
526 have "(i + j + 3 + (k::nat)) < u + -15 + y" |
|
527 apply (tactic {* test [@{simproc natless_cancel_numerals}] *})? |
|
528 sorry*) |
|
529 } |
519 } |
530 end |
520 end |
531 |
521 |
532 subsection {* @{text natle_cancel_numerals} *} |
522 subsection {* @{text natle_cancel_numerals} *} |
533 |
523 |
609 have "(i + j + 32 + k) - (u + 15 + y) = zz" |
599 have "(i + j + 32 + k) - (u + 15 + y) = zz" |
610 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
600 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
611 next |
601 next |
612 assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v" |
602 assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v" |
613 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
603 by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact |
614 next |
|
615 (* FIXME: negative numerals fail |
|
616 have "(i + j + -12 + k) - 15 = y" |
|
617 apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? |
|
618 sorry |
|
619 have "(i + j + 12 + k) - -15 = y" |
|
620 apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? |
|
621 sorry |
|
622 have "(i + j + -12 + k) - -15 = y" |
|
623 apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? |
|
624 sorry*) |
|
625 } |
604 } |
626 end |
605 end |
627 |
606 |
628 subsection {* Factor-cancellation simprocs for type @{typ nat} *} |
607 subsection {* Factor-cancellation simprocs for type @{typ nat} *} |
629 |
608 |