Resolve some conflicts between ihs and arithmetic-5

This makes it possible to do:

  (include-book "arithmetic-5/top" :dir :system)
  (include-book "ihs/ihs-lemmas" :dir :system)

By fixing several name conflicts.  I haven't gotten other books updated yet.

Quick summary of changes:

  1. Renamed IHS rule FLOOR-BOUNDS to FLOOR-BOUNDED-BY-/
  2. Renamed IHS rule MOD-X-Y-=-X to MOD-X-Y-=-X-FOR-RATIONALS
  3. Renamed IHS rule MOD-X-Y-=-X+Y to MOD-X-Y-=-X+Y-FOR-RATIONALS
  4. Renamed IHS rule MOD-BOUNDS to MOD-BOUNDED-BY-MODULUS
  5. Improved IHS rule RATIONALP-MOD to drop (rationalp x) hyp
  6. Renamed IHS rule MOD-X-I*J to MOD-X-I*J-OF-POSITIVES

Details of conflicts and resolutions follow.

----------------------------------

1. Conflict for FLOOR-BOUNDS:

arithmetic-5/lib/floor-mod/floor-mod-basic.lisp:

  (deftheory floor-bounds
    '((:linear linear-floor-bounds-1)
      (:linear linear-floor-bounds-2)
      (:linear linear-floor-bounds-3)))

ihs/quotient-remainder-lemmas.lisp:

  (defthm floor-bounds
    (implies (qr-guard x y)
             (and (< (- (/ x y) 1) (floor x y))
                  (<= (floor x y) (/ x y))))
    :rule-classes ((:linear :trigger-terms ((floor x y)))
                   (:generalize)))

Resolution: Renamed the IHS rule to FLOOR-BOUNDED-BY-/

2. Conflict for MOD-X-Y-=-X

arithmetic-5/lib/floor-mod/floor-mod-basic.lisp:

  (defthm mod-x-y-=-x
    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
		  (acl2-numberp x)
		  (acl2-numberp y)
                  (real/rationalp (/ x y)))
             (equal (equal (mod x y) x)
                    (or (equal y 0)
                        (and (<= 0 x)
                             (< x y))
                        (and (<= x 0)
                             (< y x)))))
    :rule-classes ((:rewrite)
                   (:rewrite
                    :backchain-limit-lst (1 3 1)
                    :corollary
                    (implies (and (acl2-numberp x)
                                  (real/rationalp (/ x y))
                                  (equal y 0))
                             (equal (mod x y) x)))
                   (:rewrite
                    :backchain-limit-lst (1 3 1 1)
                    :corollary
                    (implies (and (acl2-numberp x)
                                  (real/rationalp (/ x y))
                                  (<= 0 x)
                                  (< x y))
                             (equal (mod x y) x)))
                   (:rewrite
                    :backchain-limit-lst (1 3 1 1)
                    :corollary
                    (implies (and (acl2-numberp x)
                                  (real/rationalp (/ x y))
                                  (<= x 0)
                                  (< y x))
                             (equal (mod x y) x)))))

ihs/quotient-remainder-lemmas.lisp:

  (defthm mod-x-y-=-x
    (implies (qr-guard x y)
             (equal (equal (mod x y) x)
                    (or (and (>= x 0) (> y 0) (< x y))
                        (and (<= x 0) (< y 0) (> x y)))))
    :rule-classes
    ((:rewrite)
     (:generalize)
     (:rewrite :corollary (implies (and (>= x 0) (> y 0) (< x y) (qr-guard x y))
                                   (equal (mod x y) x)))
     (:rewrite :corollary (implies (and (<= x 0) (< y 0) (> x y) (qr-guard x y))
                                   (equal (mod x y) x)))))

Resolution: Renamed the IHS rule to MOD-X-Y-=-X-FOR-RATIONALS

3. Conflict for MOD-X-Y-=-X+Y

arithmetic-5/lib/floor-mod/floor-mod-basic.lisp:

  (defthm mod-x-y-=-x+y
    (implies (and (acl2-numberp y)
                  (real/rationalp (/ x y)))
             (equal (equal (mod x y) (+ x y))
                    (or (equal y 0)
                        (and (< 0 y)
                             (< x 0)
                             (<= (- x) y))
                        (and (< y 0)
                             (< 0 x)
                             (<= x (- y))))))
    :rule-classes ((:rewrite
                    :corollary
                    (implies (and (syntaxp (rewriting-goal-literal x mfc state))
                                  (acl2-numberp y)
                                  (real/rationalp (/ x y))
                                  (equal (+ x y) z))
                             (equal (equal (mod x y) z)
                                    (or (equal y 0)
                                        (and (< 0 y)
                                             (< x 0)
                                             (<= (- x) y))
                                        (and (< y 0)
                                             (< 0 x)
                                             (<= x (- y)))))))
                   (:rewrite
                    :backchain-limit-lst (3 1 1 1)
                    :corollary
                    (implies (and (real/rationalp (/ x y))
                                  (< 0 y)
                                  (< x 0)
                                  (<= (- x) y))
                             (equal (mod x y) (+ x y))))
                   (:rewrite
                    :backchain-limit-lst (3 1 1 1)
                    :corollary
                    (implies (and (real/rationalp (/ x y))
                                  (< y 0)
                                  (< 0 x)
                                  (<= x (- y)))
                             (equal (mod x y) (+ x y))))))

ihs/quotient-remainder-lemmas.lisp:

  (defthm mod-x-y-=-x+y
    (implies (qr-guard x y)
             (equal (equal (mod x y) (+ x y))
                    (or (and (> x 0) (< y 0) (<= x (- y)))
                        (and (< x 0) (> y 0) (<= (- x) y)))))
    :rule-classes
    ((:rewrite)
     (:generalize)
     (:rewrite :corollary (implies (and (> x 0) (< y 0) (<= x y) (qr-guard x y))
                                   (equal (mod x y) (+ x y))))
     (:rewrite :corollary (implies (and (< x 0) (> y 0) (<= (- x) y) (qr-guard x y))
                                   (equal (mod x y) (+ x y))))))

Resolution: Renamed the IHS rule to MOD-X-Y-=-X+Y-FOR-RATIONALS

4. Conflict for MOD-BOUNDS

arithmetic-5/lib/floor-mod/floor-mod-basic.lisp:

  (deftheory mod-bounds
    '((:linear mod-bounds-1)
      (:linear mod-bounds-2)
      (:linear mod-bounds-3)))

ihs/quotient-remainder-lemmas.lisp:

  (defthm mod-bounds
    (and (implies (and (> y 0)
                       (qr-guard x y))
                  (< (mod x y) y))
         (implies (and (< y 0)
                       (qr-guard x y))
                  (> (mod x y) y)))
    :rule-classes ((:linear :trigger-terms ((mod x y)))
                   (:generalize)))

Resolution: Renamed the IHS rule to MOD-BOUNDED-BY-MODULUS

5. Conflict for RATIONALP-MOD

arithmetic-5/lib/floor-mod/floor-mod-basic.lisp:

  #-non-standard-analysis
  (defthm rationalp-mod
    (implies (rationalp x)
             (rationalp (mod x y)))
    :rule-classes (:rewrite :type-prescription))

  #+non-standard-analysis
  (defthm rationalp-mod
    (implies (and (rationalp x)
                  (rationalp y))
             (rationalp (mod x y)))
    :rule-classes (:rewrite :type-prescription))

ihs/quotient-remainder-lemmas.lisp:

  (defthm rationalp-mod
    (implies (and (rationalp x)
                  (rationalp y))
             (rationalp (mod x y)))
    :hints (("Goal" :in-theory (enable mod rationalp-+)))
    :rule-classes (:rewrite :type-prescription))

Resolution: improved IHS rule to match arithmetic-5

6. Conflict for MOD-X-I*J

arithmetic-5/lib/floor-mod/more-floor-mod.lisp:

(defthm mod-x-i*j
  (implies (and (< 0 j)
		(integerp i)
		(integerp j)
		(real/rationalp x)
		(INTEGERP (* (/ J) (FLOOR X I))))
	   (equal (mod x (* i j))
		  (mod x i))))

ihs/quotient-remainder-lemmas.lisp:

(defthm mod-x-i*j
    (implies (and (> i 0)
                  (> j 0)
                  (force (integerp i))
                  (force (integerp j))
                  (force (real/rationalp x)))
             (equal (mod x (* i j))
                    (+ (mod x i) (* i (mod (floor x i) j)))))
    :hints (("Goal" :use mod-x-i*j-crock)))

Resolution: Renamed IHS rule to MOD-X-I*J-OF-POSITIVES
fix up all books to accommodate ihs name changes
update release notes
Merge pull request #297 from jaredcdavis/conflict

resolve some name conflicts