← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/arithmetic-5/lib/floor-mod/floor-mod-basic.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/arithmetic-5/lib/floor-mod/floor-mod-basic.lisp
592
592
 
593
593
 
594
594
(defthm floor-=-x/y
 
595
  ;; [Jared] modified on 2014-07-29 to make compatible with ihs/quotient-remainder-lemmas.
 
596
  ;;
 
597
  ;; The original IHS rule had the following rule classes:
 
598
  ;; ((:rewrite)
 
599
  ;;  (:generalize)
 
600
  ;;  (:rewrite :corollary (implies (and (equal r (/ x y))
 
601
  ;;                                     (integerp r))
 
602
  ;;                                (equal (floor x y) r))))
 
603
  ;;
 
604
  ;; The original arithmetic-5 rule has the following rule-classes:
 
605
  ;;
 
606
  ;; (:rewrite :corollary (implies (integerp (/ x y))
 
607
  ;;                               (equal (floor x y)
 
608
  ;;                                      (/ x y))))
 
609
  ;; (:rewrite :corollary (implies (equal (* x (/ y)) z)
 
610
  ;;                               (equal (equal (floor x y) z)
 
611
  ;;                                      (integerp z))))
 
612
  ;;
 
613
  ;; Solution: DO ALL THE THINGS.
595
614
  (equal (equal (floor x y) (* x (/ y)))
596
615
         (integerp (/ x y)))
597
 
  :rule-classes ((:rewrite
598
 
                  :corollary
599
 
                  (implies (integerp (/ x y))
600
 
                           (equal (floor x y)
601
 
                                  (/ x y))))
602
 
                 (:rewrite
603
 
                  :corollary
604
 
                  (implies (equal (* x (/ y)) z)
605
 
                           (equal (equal (floor x y) z)
606
 
                                  (integerp z))))))
 
616
  :rule-classes ((:rewrite)
 
617
                 (:generalize)
 
618
                 (:rewrite :corollary (implies (and (equal r (/ x y))
 
619
                                                    (integerp r))
 
620
                                               (equal (floor x y) r)))
 
621
                 (:rewrite :corollary (implies (integerp (/ x y))
 
622
                                               (equal (floor x y)
 
623
                                                      (/ x y))))
 
624
                 (:rewrite :corollary (implies (equal (* x (/ y)) z)
 
625
                                               (equal (equal (floor x y) z)
 
626
                                                      (integerp z))))))
607
627
 
608
628
(defthm mod-nonnegative
609
629
  (implies (and (real/rationalp (/ x y))