Filtering...

collect

books/arithmetic-5/lib/basic-ops/collect

Included Books

building-blocks top expt-helper
other
(in-package "ACL2")
include-book
(include-book "building-blocks")
local
(local (include-book "../../support/top"))
local
(local (include-book "expt-helper"))
local
(local (defthm hack516 (equal (expt x (- m)) (/ (expt x m)))))
collect-+function
(defun collect-+
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (+ x y))
collect-+-problem-findertheorem
(defthm collect-+-problem-finder
  (implies (and (cw "There is a missing rule for collect-+.  ~
                       Please report this to the maintainers of ~
                       ACL2.  The offending pattern is:~%~
                       (collect-+ ~x0 ~x1)."
        x
        y)
      (not (equal x x)))
    (equal (collect-+ x y) (+ x y))))
|(+ x x)|theorem
(defthm |(+ x x)| (equal (collect-+ x x) (* 2 x)))
|(+ x (- x))|theorem
(defthm |(+ x (- x))| (equal (collect-+ x (- x)) 0))
|(+ x (* c x))|theorem
(defthm |(+ x (* c x))|
  (implies (syntaxp (quotep c))
    (equal (collect-+ x (* c x)) (* (+ c 1) x))))
|(+ (- x) (* c x))|theorem
(defthm |(+ (- x) (* c x))|
  (implies (syntaxp (quotep c))
    (equal (collect-+ (- x) (* c x)) (* (- c 1) x))))
|(+ (* c x) (* d x))|theorem
(defthm |(+ (* c x) (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (collect-+ (* c x) (* d x)) (* (+ c d) x))))
|(collect-+ y x)|theorem
(defthm |(collect-+ y x)|
  (equal (collect-+ y x) (collect-+ x y)))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (active-runep '(:rewrite |(+ x x)|))
      (active-runep '(:rewrite |(+ x (- x))|))
      (active-runep '(:rewrite |(+ x (* c x))|))
      (active-runep '(:rewrite |(+ (- x) (* c x))|))
      (active-runep '(:rewrite |(+ (* c x) (* d x))|))
      (active-runep '(:rewrite |(collect-+ y x)|)))
    t)
  :error nil)
in-theory
(in-theory (disable collect-+))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (not (active-runep '(:definition collect-+)))
    t)
  :error nil)
pow-2function
(defun pow-2
  (x to-bind)
  (let ((pow (power-of-2-generalized x)))
    (if pow
      `((,TO-BIND quote ,POW))
      nil)))
collect-*function
(defun collect-*
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (* x y))
collect-*-problem-findertheorem
(defthm collect-*-problem-finder
  (implies (and (cw "There is a missing rule for collect-*.  ~
                       Please report this to the maintainers of ~
                       ACL2.  The offending pattern is:~%~
                       (collect-* ~x0 ~x1)."
        x
        y)
      (not (equal x x)))
    (equal (collect-* x y) (* x y))))
|(* x x)|theorem
(defthm |(* x x)| (equal (collect-* x x) (expt x 2)))
|(* x (/ x))|theorem
(defthm |(* x (/ x))|
  (equal (collect-* x (/ x))
    (if (equal (if (acl2-numberp x)
          x
          0)
        0)
      0
      1)))
|(* x (expt x n))|theorem
(defthm |(* x (expt x n))|
  (implies (integerp n)
    (equal (collect-* x (expt x n))
      (if (equal (if (acl2-numberp x)
            x
            0)
          0)
        0
        (expt x (+ n 1))))))
|(* c (expt d n))|theorem
(defthm |(* c (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* c (expt d n))
      (if (equal (fix c) 0)
        0
        (expt 2 (+ c-pow (* d-pow n)))))))
|(* (- c) (expt c n))|theorem
(defthm |(* (- c) (expt c n))|
  (implies (and (syntaxp (numeric-constant-p c)) (integerp n))
    (equal (collect-* (- c) (expt c n))
      (if (equal (fix c) 0)
        0
        (- (expt c (+ n 1)))))))
|(* (- c) (expt d n))|theorem
(defthm |(* (- c) (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (- c) (expt d n))
      (if (equal (fix c) 0)
        0
        (- (expt 2 (+ c-pow (* d-pow n))))))))
|(* (/ x) (expt x n))|theorem
(defthm |(* (/ x) (expt x n))|
  (implies (integerp n)
    (equal (collect-* (/ x) (expt x n))
      (if (equal (if (acl2-numberp x)
            x
            0)
          0)
        0
        (expt x (- n 1))))))
|(* (/ c) (expt d n))|theorem
(defthm |(* (/ c) (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (/ c) (expt d n))
      (if (equal (fix c) 0)
        0
        (expt 2 (+ (- c-pow) (* d-pow n)))))))
|(* (- (/ c)) (expt c n))|theorem
(defthm |(* (- (/ c)) (expt c n))|
  (implies (and (syntaxp (numeric-constant-p c)) (integerp n))
    (equal (collect-* (- (/ c)) (expt c n))
      (if (equal (fix c) 0)
        0
        (- (expt c (- n 1)))))))
|(* (- (/ c)) (expt d n))|theorem
(defthm |(* (- (/ c)) (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (- (/ c)) (expt d n))
      (if (equal (fix c) 0)
        0
        (- (expt 2 (+ (- c-pow) (* d-pow n))))))))
|(* x (/ (expt x n)))|theorem
(defthm |(* x (/ (expt x n)))|
  (implies (integerp n)
    (equal (collect-* x (/ (expt x n)))
      (if (equal (if (acl2-numberp x)
            x
            0)
          0)
        0
        (/ (expt x (- n 1)))))))
|(* c (/ (expt d n)))|theorem
(defthm |(* c (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* c (/ (expt d n)))
      (if (equal (fix c) 0)
        0
        (/ (expt 2 (+ (- c-pow) (* d-pow n))))))))
|(* (- c) (/ (expt c n)))|theorem
(defthm |(* (- c) (/ (expt c n)))|
  (implies (and (syntaxp (numeric-constant-p c)) (integerp n))
    (equal (collect-* (- c) (/ (expt c n)))
      (if (equal (fix c) 0)
        0
        (- (/ (expt c (- n 1))))))))
|(* (- c) (/ (expt d n)))|theorem
(defthm |(* (- c) (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (- c) (/ (expt d n)))
      (if (equal (fix c) 0)
        0
        (- (/ (expt 2 (+ (- c-pow) (* d-pow n)))))))))
|(* (/ x) (/ (expt x n)))|theorem
(defthm |(* (/ x) (/ (expt x n)))|
  (implies (integerp n)
    (equal (collect-* (/ x) (/ (expt x n)))
      (if (equal (if (acl2-numberp x)
            x
            0)
          0)
        0
        (/ (expt x (+ n 1)))))))
|(* (/ c) (/ (expt d n)))|theorem
(defthm |(* (/ c) (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (/ c) (/ (expt d n)))
      (if (equal (fix c) 0)
        0
        (/ (expt 2 (+ c-pow (* d-pow n))))))))
|(* (- (/ c)) (/ (expt c n)))|theorem
(defthm |(* (- (/ c)) (/ (expt c n)))|
  (implies (and (syntaxp (numeric-constant-p c)) (integerp n))
    (equal (collect-* (- (/ c)) (/ (expt c n)))
      (if (equal (fix c) 0)
        0
        (- (/ (expt c (+ n 1))))))))
|(* (- (/ c)) (/ (expt d n)))|theorem
(defthm |(* (- (/ c)) (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp n))
    (equal (collect-* (- (/ c)) (/ (expt d n)))
      (if (equal (fix c) 0)
        0
        (- (/ (expt 2 (+ c-pow (* d-pow n)))))))))
|(* (expt x m) (expt x n))|theorem
(defthm |(* (expt x m) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (collect-* (expt x m) (expt x n))
      (if (and (equal (if (acl2-numberp x)
              x
              0)
            0)
          (not (equal m 0))
          (not (equal n 0)))
        0
        (expt x (+ m n))))))
|(* (expt c m) (expt d n))|theorem
(defthm |(* (expt c m) (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp m)
      (integerp n))
    (equal (collect-* (expt c m) (expt d n))
      (if (or (and (equal (fix c) 0) (not (equal m 0)))
          (and (equal (fix d) 0) (not (equal n 0))))
        0
        (expt 2 (+ (* c-pow m) (* d-pow n)))))))
|(* (/ (expt x m)) (expt x n))|theorem
(defthm |(* (/ (expt x m)) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (collect-* (/ (expt x m)) (expt x n))
      (if (and (equal (if (acl2-numberp x)
              x
              0)
            0)
          (not (equal m 0))
          (not (equal n 0)))
        0
        (expt x (- n m))))))
|(* (/ (expt c m)) (expt d n))|theorem
(defthm |(* (/ (expt c m)) (expt d n))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp m)
      (integerp n))
    (equal (collect-* (/ (expt c m)) (expt d n))
      (if (or (and (equal (fix c) 0) (not (equal m 0)))
          (and (equal (fix d) 0) (not (equal n 0))))
        0
        (expt 2 (+ (* (- c-pow) m) (* d-pow n)))))))
|(* (expt x m) (/ (expt x n)))|theorem
(defthm |(* (expt x m) (/ (expt x n)))|
  (implies (and (integerp m) (integerp n))
    (equal (collect-* (expt x m) (/ (expt x n)))
      (if (and (equal (if (acl2-numberp x)
              x
              0)
            0)
          (not (equal m 0))
          (not (equal n 0)))
        0
        (expt x (- m n))))))
|(* (expt c m) (/ (expt d n)))|theorem
(defthm |(* (expt c m) (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp m)
      (integerp n))
    (equal (collect-* (expt c m) (/ (expt d n)))
      (if (or (and (equal (fix c) 0) (not (equal m 0)))
          (and (equal (fix d) 0) (not (equal n 0))))
        0
        (expt 2 (+ (* c-pow m) (* (- d-pow) n)))))))
|(* (/ (expt x m)) (/ (expt x n)))|theorem
(defthm |(* (/ (expt x m)) (/ (expt x n)))|
  (implies (and (integerp m) (integerp n))
    (equal (collect-* (/ (expt x m)) (/ (expt x n)))
      (if (and (equal (if (acl2-numberp x)
              x
              0)
            0)
          (not (equal m 0))
          (not (equal n 0)))
        0
        (/ (expt x (+ m n)))))))
|(* (/ (expt c m)) (/ (expt d n)))|theorem
(defthm |(* (/ (expt c m)) (/ (expt d n)))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (rational-constant-p d))
      (bind-free (pow-2 c 'c-pow) (c-pow))
      (bind-free (pow-2 d 'd-pow) (d-pow))
      (integerp c-pow)
      (integerp d-pow)
      (equal c (expt 2 c-pow))
      (equal d (expt 2 d-pow))
      (integerp m)
      (integerp n))
    (equal (collect-* (/ (expt c m)) (/ (expt d n)))
      (if (or (and (equal (fix c) 0) (not (equal m 0)))
          (and (equal (fix d) 0) (not (equal n 0))))
        0
        (/ (expt 2 (+ (* c-pow m) (* d-pow n))))))))
|(* (expt x n) (expt y n))|theorem
(defthm |(* (expt x n) (expt y n))|
  (implies (integerp n)
    (equal (collect-* (expt x n) (expt y n)) (expt (* x y) n))))
|(collect-* y x)|theorem
(defthm |(collect-* y x)|
  (equal (collect-* y x) (collect-* x y)))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (active-runep '(:rewrite |(* x x)|))
      (active-runep '(:rewrite |(* x (/ x))|))
      (active-runep '(:rewrite |(* x (expt x n))|))
      (active-runep '(:rewrite |(* c (expt d n))|))
      (active-runep '(:rewrite |(* (- c) (expt c n))|))
      (active-runep '(:rewrite |(* (- c) (expt d n))|))
      (active-runep '(:rewrite |(* (/ x) (expt x n))|))
      (active-runep '(:rewrite |(* (/ c) (expt d n))|))
      (active-runep '(:rewrite |(* (- (/ c)) (expt c n))|))
      (active-runep '(:rewrite |(* (- (/ c)) (expt d n))|))
      (active-runep '(:rewrite |(* x (/ (expt x n)))|))
      (active-runep '(:rewrite |(* c (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (- c) (/ (expt c n)))|))
      (active-runep '(:rewrite |(* (- c) (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (/ x) (/ (expt x n)))|))
      (active-runep '(:rewrite |(* (/ c) (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (- (/ c)) (/ (expt c n)))|))
      (active-runep '(:rewrite |(* (- (/ c)) (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (expt x m) (expt x n))|))
      (active-runep '(:rewrite |(* (expt c m) (expt d n))|))
      (active-runep '(:rewrite |(* (/ (expt x m)) (expt x n))|))
      (active-runep '(:rewrite |(* (/ (expt c m)) (expt d n))|))
      (active-runep '(:rewrite |(* (expt x m) (/ (expt x n)))|))
      (active-runep '(:rewrite |(* (expt c m) (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (/ (expt x m)) (/ (expt x n)))|))
      (active-runep '(:rewrite |(* (/ (expt c m)) (/ (expt d n)))|))
      (active-runep '(:rewrite |(* (expt x n) (expt y n))|))
      (active-runep '(:rewrite |(collect-* y x)|)))
    t)
  :error nil)
in-theory
(in-theory (disable collect-*))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (not (active-runep '(:definition collect-*)))
    t)
  :error nil)
local
(local (in-theory (enable collect-+ collect-*)))
bubble-downfunction
(defun bubble-down
  (x match)
  (declare (xargs :guard t))
  (declare (ignore match))
  x)
|(acl2-numberp (bubble-down x match))|theorem
(defthm |(acl2-numberp (bubble-down x match))|
  (equal (acl2-numberp (bubble-down x match))
    (acl2-numberp x)))
bubble-down-+-problem-findertheorem
(defthm bubble-down-+-problem-finder
  (implies (equal x x)
    (equal (+ (bubble-down x match) y) (+ x y))))
in-theory
(in-theory (disable bubble-down-+-problem-finder))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (not (active-runep '(:rewrite bubble-down-+-problem-finder)))
    t)
  :error nil)
bubble-down-+-bubble-downtheorem
(defthm bubble-down-+-bubble-down
  (implies (equal x x)
    (equal (+ (bubble-down x match) y z)
      (+ y (bubble-down x match) z))))
bubble-down-+-match-1theorem
(defthm bubble-down-+-match-1
  (implies (syntaxp (equal match y))
    (equal (+ (bubble-down x match) y) (collect-+ x y))))
bubble-down-+-match-2theorem
(defthm bubble-down-+-match-2
  (implies (syntaxp (equal match y))
    (equal (+ y (bubble-down x match)) (collect-+ x y))))
bubble-down-+-match-3theorem
(defthm bubble-down-+-match-3
  (implies (syntaxp (equal match y))
    (equal (+ (bubble-down x match) y z) (+ (collect-+ x y) z))))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (active-runep '(:rewrite bubble-down-+-bubble-down))
      (active-runep '(:rewrite bubble-down-+-match-1))
      (active-runep '(:rewrite bubble-down-+-match-2))
      (active-runep '(:rewrite bubble-down-+-match-3)))
    t)
  :error nil)
bubble-down-*-problem-findertheorem
(defthm bubble-down-*-problem-finder
  (implies (equal x x)
    (equal (* (bubble-down x match) y) (* x y))))
in-theory
(in-theory (disable bubble-down-*-problem-finder))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (not (active-runep '(:rewrite bubble-down-*-problem-finder)))
    t)
  :error nil)
bubble-down-*-bubble-downtheorem
(defthm bubble-down-*-bubble-down
  (implies (equal x x)
    (equal (* (bubble-down x match) y z)
      (* y (bubble-down x match) z))))
bubble-down-*-match-1theorem
(defthm bubble-down-*-match-1
  (implies (syntaxp (equal match y))
    (equal (* (bubble-down x match) y) (collect-* x y))))
bubble-down-*-match-2theorem
(defthm bubble-down-*-match-2
  (implies (syntaxp (equal match y))
    (equal (* y (bubble-down x match)) (collect-* x y))))
bubble-down-*-match-3theorem
(defthm bubble-down-*-match-3
  (implies (syntaxp (equal match y))
    (equal (* (bubble-down x match) y z) (* (collect-* x y) z))))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (active-runep '(:rewrite bubble-down-*-bubble-down))
      (active-runep '(:rewrite bubble-down-*-match-1))
      (active-runep '(:rewrite bubble-down-*-match-2))
      (active-runep '(:rewrite bubble-down-*-match-3)))
    t)
  :error nil)
in-theory
(in-theory (disable bubble-down (:executable-counterpart bubble-down)))
other
(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (not (active-runep '(:rewrite bubble-down)))
      (not (active-runep '(:executable-counterpart bubble-down))))
    t)
  :error nil)