Filtering...

collect

books/arithmetic-3/bind-free/collect

Included Books

top basic-helper
other
(in-package "ACL2")
local
(local (include-book "../pass1/top"))
local
(local (include-book "basic-helper"))
local
(local (defthm hack516 (equal (expt x (- m)) (/ (expt x m)))))
|(+ c (+ d x))|theorem
(defthm |(+ c (+ d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (+ c (+ d x)) (+ (+ c d) x))))
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 (equal x x) (equal (collect-+ x y) (+ x y))))
in-theory
(in-theory (disable collect-+-problem-finder))
other
(theory-invariant (not (active-runep '(:rewrite collect-+-problem-finder)))
  :error nil)
|(+ 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 (or (not (active-runep '(:rewrite collect-+)))
    (and (active-runep '(:rewrite |(collect-+ y x)|))
      (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))|))))
  :error nil)
in-theory
(in-theory (disable collect-+))
other
(theory-invariant (not (active-runep '(:definition collect-+)))
  :error nil)
|(* c (* d x))|theorem
(defthm |(* c (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (* c (* d x)) (* (* c d) x))))
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 (equal x x) (equal (collect-* x y) (* x y))))
in-theory
(in-theory (disable collect-*-problem-finder))
other
(theory-invariant (not (active-runep '(:rewrite collect-*-problem-finder)))
  :error nil)
|(* (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))))
|(* 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 (fix x) 0)
      0
      1)))
|(* x (expt x n))|theorem
(defthm |(* x (expt x n))|
  (implies (integerp n)
    (equal (collect-* x (expt x n))
      (if (equal (fix x) 0)
        0
        (expt x (+ n 1))))))
|(* x (expt (- x) n))|theorem
(defthm |(* x (expt (- x) n))|
  (implies (integerp n)
    (equal (collect-* x (expt (- x) n))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (expt x (+ n 1)))
        (t (- (expt x (+ n 1))))))))
|(* x (/ (expt x n)))|theorem
(defthm |(* x (/ (expt x n)))|
  (implies (integerp n)
    (equal (collect-* x (/ (expt x n)))
      (if (equal (fix x) 0)
        0
        (/ (expt x (- n 1)))))))
|(* x (/ (expt (- x) n)))|theorem
(defthm |(* x (/ (expt (- x) n)))|
  (implies (integerp n)
    (equal (collect-* x (/ (expt (- x) n)))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (/ (expt x (- n 1))))
        (t (- (/ (expt x (- n 1)))))))))
|(* (/ x) (expt x n))|theorem
(defthm |(* (/ x) (expt x n))|
  (implies (integerp n)
    (equal (collect-* (/ x) (expt x n))
      (if (equal (fix x) 0)
        0
        (expt x (- n 1))))))
|(* (/ x) (/ (expt x n)))|theorem
(defthm |(* (/ x) (/ (expt x n)))|
  (implies (integerp n)
    (equal (collect-* (/ x) (/ (expt x n)))
      (if (equal (fix x) 0)
        0
        (/ (expt x (+ n 1)))))))
|(* (/ x) (expt (- x) n))|theorem
(defthm |(* (/ x) (expt (- x) n))|
  (implies (integerp n)
    (equal (collect-* (/ x) (expt (- x) n))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (expt x (- n 1)))
        (t (- (expt x (- n 1))))))))
|(* (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 (fix x) 0) (not (equal m 0)) (not (equal n 0)))
        0
        (expt x (+ m 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))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp m) (expt x (+ m n)))
        (t (- (expt x (+ m 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))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp n) (expt x (+ m n)))
        (t (- (expt x (+ m 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 (fix x) 0) (not (equal m 0)) (not (equal n 0)))
        0
        (expt x (- n m))))))
|(* (/ (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))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp m) (expt x (- n m)))
        (t (- (expt x (- n m))))))))
|(* (/ (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))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp n) (expt x (- n m)))
        (t (- (expt x (- n m))))))))
|(* (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 (fix x) 0) (not (equal m 0)) (not (equal n 0)))
        0
        (expt x (- m 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)))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp m) (expt x (- m n)))
        (t (- (expt x (- m 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)))
      (cond ((and (equal (fix x) 0) (not (equal m 0)) (not (equal n 0))) 0)
        ((evenp n) (expt x (- m n)))
        (t (- (expt x (- m n))))))))
|(collect-* y x)|theorem
(defthm |(collect-* y x)|
  (equal (collect-* y x) (collect-* x y)))
other
(theory-invariant (or (not (active-runep '(:rewrite collect-*)))
    (and (active-runep '(:rewrite |(collect-* y x)|))
      (active-runep '(:rewrite |(* (expt x n) (expt y n))|))
      (active-runep '(:rewrite |(* x x)|))
      (active-runep '(:rewrite |(* x (/ x))|))
      (active-runep '(:rewrite |(* x (expt x n))|))
      (active-runep '(:rewrite |(* x (expt (- x) n))|))
      (active-runep '(:rewrite |(* x (/ (expt x n)))|))
      (active-runep '(:rewrite |(* x (/ (expt (- x) n)))|))
      (active-runep '(:rewrite |(* (/ x) (expt x n))|))
      (active-runep '(:rewrite |(* (/ x) (expt (- x) n))|))
      (active-runep '(:rewrite |(* (expt x m) (expt x n))|))
      (active-runep '(:rewrite |(* (expt (- x) m) (expt x n))|))
      (active-runep '(:rewrite |(* (expt x m) (expt (- x) n))|))
      (active-runep '(:rewrite |(* (/ (expt x m)) (expt x n))|))
      (active-runep '(:rewrite |(* (/ (expt (- x) m)) (expt x n))|))
      (active-runep '(:rewrite |(* (/ (expt x m)) (expt (- x) n))|))
      (active-runep '(:rewrite |(* (expt x m) (/ (expt x n)))|))
      (active-runep '(:rewrite |(* (expt (- x) m) (/ (expt x n)))|))
      (active-runep '(:rewrite |(* (expt x m) (/ (expt (- x) n)))|))))
  :error nil)
in-theory
(in-theory (disable collect-*))
other
(theory-invariant (not (active-runep '(:definition collect-*)))
  :error nil)
local
(local (in-theory (enable collect-+ collect-*)))
bubble-downfunction
(defun bubble-down
  (x match)
  (declare (xargs :guard t))
  (declare (ignore match))
  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 (not (active-runep '(:rewrite bubble-down-+-problem-finder)))
  :error nil)
bubble-down-+-bubble-downtheorem
(defthm bubble-down-+-bubble-down
  (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 (or (not (active-runep '(:rewrite bubble-down)))
    (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))))
  :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 (not (active-runep '(:rewrite bubble-down-*-problem-finder)))
  :error nil)
bubble-down-*-bubble-downtheorem
(defthm bubble-down-*-bubble-down
  (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 (or (not (active-runep '(:rewrite bubble-down)))
    (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))))
  :error nil)
in-theory
(in-theory (disable bubble-down (:executable-counterpart bubble-down)))
other
(theory-invariant (and (not (active-runep '(:rewrite bubble-down)))
    (not (active-runep '(:executable-counterpart bubble-down))))
  :error nil)