322 have "(a*(b*c)) / (d*b*(x*a)) = uu" |
322 have "(a*(b*c)) / (d*b*(x*a)) = uu" |
323 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
323 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
324 } |
324 } |
325 end |
325 end |
326 |
326 |
327 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" |
327 lemma |
|
328 fixes a b c d x y z :: "'a::linordered_field_inverse_zero" |
|
329 shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z" |
328 oops -- "FIXME: need simproc to cover this case" |
330 oops -- "FIXME: need simproc to cover this case" |
329 |
|
330 |
331 |
331 subsection {* @{text linordered_ring_less_cancel_factor} *} |
332 subsection {* @{text linordered_ring_less_cancel_factor} *} |
332 |
333 |
333 notepad begin |
334 notepad begin |
334 fix x y z :: "'a::linordered_idom" |
335 fix x y z :: "'a::linordered_idom" |
382 have "7 * x / 5 + y - 4 * x / 3 = uu" |
383 have "7 * x / 5 + y - 4 * x / 3 = uu" |
383 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
384 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
384 } |
385 } |
385 end |
386 end |
386 |
387 |
387 lemma "2/3 * (x::rat) + x / 3 = uu" |
388 lemma |
|
389 fixes x :: "'a::{linordered_field_inverse_zero,number_ring}" |
|
390 shows "2/3 * x + x / 3 = uu" |
388 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
391 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
389 oops -- "FIXME: test fails" |
392 oops -- "FIXME: test fails" |
390 |
393 |
|
394 subsection {* @{text nat_combine_numerals} *} |
|
395 |
|
396 notepad begin |
|
397 fix i j k m n u :: nat |
|
398 { |
|
399 assume "4*k = u" have "k + 3*k = u" |
|
400 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
401 next |
|
402 assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" |
|
403 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
404 next |
|
405 assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" |
|
406 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
407 next |
|
408 assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" |
|
409 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
410 next |
|
411 assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u" |
|
412 have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u" |
|
413 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
414 next |
|
415 assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u" |
|
416 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact |
|
417 } |
|
418 end |
|
419 |
|
420 (*negative numerals: FAIL*) |
|
421 lemma "Suc (i + j + -3 + k) = u" |
|
422 apply (tactic {* test [@{simproc nat_combine_numerals}] *})? |
|
423 oops |
|
424 |
391 subsection {* @{text nateq_cancel_numerals} *} |
425 subsection {* @{text nateq_cancel_numerals} *} |
392 |
426 |
393 notepad begin |
427 notepad begin |
394 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
428 fix i j k l oo u uu vv w y z w' y' z' :: "nat" |
395 { |
429 { |
396 assume "Suc 0 * u = 0" have "2*u = (u::nat)" |
430 assume "Suc 0 * u = 0" have "2*u = u" |
397 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
431 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
398 next |
432 next |
399 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
433 assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)" |
400 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
434 by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact |
401 next |
435 next |
558 apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? |
592 apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? |
559 sorry*) |
593 sorry*) |
560 } |
594 } |
561 end |
595 end |
562 |
596 |
563 end |
597 subsection {* Factor-cancellation simprocs for type @{typ nat} *} |
|
598 |
|
599 text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor}, |
|
600 @{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and |
|
601 @{text nat_dvd_cancel_factor}. *} |
|
602 |
|
603 notepad begin |
|
604 fix a b c d k x y uu :: nat |
|
605 { |
|
606 assume "k = 0 \<or> x = y" have "x*k = k*y" |
|
607 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
|
608 next |
|
609 assume "k = 0 \<or> Suc 0 = y" have "k = k*y" |
|
610 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
|
611 next |
|
612 assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b" |
|
613 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
|
614 next |
|
615 assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)" |
|
616 by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact |
|
617 next |
|
618 assume "0 < k \<and> x < y" have "x*k < k*y" |
|
619 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
|
620 next |
|
621 assume "0 < k \<and> Suc 0 < y" have "k < k*y" |
|
622 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
|
623 next |
|
624 assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b" |
|
625 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
|
626 next |
|
627 assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)" |
|
628 by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact |
|
629 next |
|
630 assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y" |
|
631 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
|
632 next |
|
633 assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y" |
|
634 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
|
635 next |
|
636 assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b" |
|
637 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
|
638 next |
|
639 assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)" |
|
640 by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact |
|
641 next |
|
642 assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu" |
|
643 by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact |
|
644 next |
|
645 assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu" |
|
646 by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact |
|
647 next |
|
648 assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu" |
|
649 by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact |
|
650 next |
|
651 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
|
652 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
|
653 by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact |
|
654 next |
|
655 assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)" |
|
656 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
|
657 next |
|
658 assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)" |
|
659 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
|
660 next |
|
661 assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)" |
|
662 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
|
663 next |
|
664 assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))" |
|
665 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
|
666 next |
|
667 assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))" |
|
668 by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact |
|
669 } |
|
670 end |
|
671 |
|
672 end |