Filtering...

arithmetic-theory

books/arithmetic-3/bind-free/arithmetic-theory

Included Books

basic common building-blocks collect
other
(in-package "ACL2")
local
(local (include-book "basic"))
include-book
(include-book "common")
include-book
(include-book "building-blocks")
local
(local (include-book "collect"))
local
(local (in-theory (enable collect-*)))
local
(local (in-theory (enable collect-+)))
arith-bubble-downfunction
(defun arith-bubble-down
  (x match)
  (declare (xargs :guard t)
    (ignore match))
  x)
local
(local (defthm temp510
    (implies (and (rationalp x) (rationalp y))
      (equal (equal (+ x y) 0) (equal x (- y))))))
other
(table acl2-defaults-table :state-ok t)
arith-find-matching-factor-gather-exponentsfunction
(defun arith-find-matching-factor-gather-exponents
  (to-match x)
  (declare (xargs :guard (and (true-listp to-match) (pseudo-termp x))))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((arith-matching-factor-gather-exponents-p to-match (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (arith-find-matching-factor-gather-exponents to-match
            (arg2 x)))
        ((arith-matching-factor-gather-exponents-p to-match (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((arith-matching-factor-gather-exponents-p to-match x) (list (cons 'match x)))
    (t nil)))
arith-normalize-factors-gather-exponentstheorem
(defthm arith-normalize-factors-gather-exponents
  (implies (and (bind-free (arith-find-matching-factor-gather-exponents (arith-factor-pattern-gather-exponents x)
          y)
        (match))
      (syntaxp (proveably-non-zero x mfc state)))
    (equal (* x y) (* (arith-bubble-down x match) y))))
local
(local (in-theory (disable arith-normalize-factors-gather-exponents)))
arith-find-matching-factor-scatter-exponentsfunction
(defun arith-find-matching-factor-scatter-exponents
  (to-match x)
  (declare (xargs :guard (and (true-listp to-match) (pseudo-termp x))))
  (cond ((eq (fn-symb x) 'binary-*) (cond ((arith-matching-factor-scatter-exponents-p to-match
           (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-*) (arith-find-matching-factor-scatter-exponents to-match
            (arg2 x)))
        ((arith-matching-factor-scatter-exponents-p to-match
           (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((arith-matching-factor-scatter-exponents-p to-match x) (list (cons 'match x)))
    (t nil)))
arith-normalize-factors-scatter-exponentstheorem
(defthm arith-normalize-factors-scatter-exponents
  (implies (and (bind-free (arith-find-matching-factor-scatter-exponents (arith-factor-pattern-scatter-exponents x)
          y)
        (match))
      (syntaxp (proveably-non-zero x mfc state)))
    (equal (* x y) (* (arith-bubble-down x match) y))))
local
(local (in-theory (disable arith-normalize-factors-scatter-exponents)))
arith-find-matching-addendfunction
(defun arith-find-matching-addend
  (to-match x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (cond ((matching-addend-p to-match (arg1 x)) (list (cons 'match (arg1 x))))
        ((eq (fn-symb (arg2 x)) 'binary-+) (arith-find-matching-addend to-match (arg2 x)))
        ((matching-addend-p to-match (arg2 x)) (list (cons 'match (arg2 x))))
        (t nil)))
    ((matching-addend-p to-match x) (list (cons 'match x)))
    (t nil)))
arith-normalize-addendstheorem
(defthm arith-normalize-addends
  (implies (bind-free (arith-find-matching-addend (addend-pattern x) y)
      (match))
    (equal (+ x y) (+ (arith-bubble-down x match) y))))
local
(local (in-theory (disable arith-normalize-addends)))
|arith (- (- x))|theorem
(defthm |arith (- (- x))|
  (implies (acl2-numberp x) (equal (- (- x)) x)))
|arith (- (+ x y))|theorem
(defthm |arith (- (+ x y))|
  (equal (- (+ x y)) (+ (- x) (- y))))
|arith (* y x)|theorem
(defthm |arith (* y x)| (equal (* y x) (* x y)))
|arith (* y (* x z))|theorem
(defthm |arith (* y (* x z))|
  (equal (* y (* x z)) (* x (* y z))))
|arith (* (* x y) z)|theorem
(defthm |arith (* (* x y) z)|
  (equal (* (* x y) z) (* x (* y z))))
|arith (* 1 x)|theorem
(defthm |arith (* 1 x)|
  (implies (acl2-numberp x) (equal (* 1 x) x)))
|arith (* x 1)|theorem
(defthm |arith (* x 1)|
  (implies (acl2-numberp x) (equal (* x 1) x)))
|arith (* 0 x)|theorem
(defthm |arith (* 0 x)| (equal (* 0 x) 0))
|arith (* x 0)|theorem
(defthm |arith (* x 0)| (equal (* x 0) 0))
|arith (* -1 x)|theorem
(defthm |arith (* -1 x)| (equal (* -1 x) (- x)))
|arith (/ (/ x))|theorem
(defthm |arith (/ (/ x))|
  (implies (acl2-numberp x) (equal (/ (/ x)) x)))
|arith (/ (* x y))|theorem
(defthm |arith (/ (* x y))|
  (equal (/ (* x y)) (* (/ x) (/ y))))
|arith (* x (+ y z))|theorem
(defthm |arith (* x (+ y z))|
  (equal (* x (+ y z)) (+ (* x y) (* x z))))
local
(local (in-theory (disable distributivity)))
|arith (* (+ x y) z)|theorem
(defthm |arith (* (+ x y) z)|
  (equal (* (+ x y) z) (+ (* x z) (* y z))))
|arith (* x (- y))|theorem
(defthm |arith (* x (- y))|
  (implies (syntaxp (not (quotep y)))
    (equal (* x (- y)) (- (* x y)))))
|arith (* (- x) y)|theorem
(defthm |arith (* (- x) y)|
  (implies (syntaxp (not (quotep x)))
    (equal (* (- x) y) (- (* x y)))))
|arith (- (* c x))|theorem
(defthm |arith (- (* c x))|
  (implies (syntaxp (quotep c))
    (equal (- (* c x)) (* (- c) x))))
|arith (/ (- x))|theorem
(defthm |arith (/ (- x))|
  (implies (syntaxp (not (quotep x)))
    (equal (/ (- x)) (- (/ x)))))
|arith (expt (+ x y) 2)|theorem
(defthm |arith (expt (+ x y) 2)|
  (implies (syntaxp (rewriting-goal-literal x mfc state))
    (equal (expt (+ x y) 2) (+ (expt x 2) (* 2 x y) (expt y 2))))
  :hints (("Goal" :expand (expt (+ x y) 2))))
|arith (expt (+ x y) 3)|theorem
(defthm |arith (expt (+ x y) 3)|
  (implies (syntaxp (rewriting-goal-literal x mfc state))
    (equal (expt (+ x y) 3)
      (+ (expt x 3)
        (* 3 (expt x 2) y)
        (* 3 x (expt y 2))
        (expt y 3))))
  :hints (("Goal" :expand ((expt (+ x y) 3) (expt (+ x y) 2)))))
|arith (* c (* d x))|theorem
(defthm |arith (* c (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (* c (* d x)) (* (* c d) x))))
|arith (expt x 0)|theorem
(defthm |arith (expt x 0)| (equal (expt x 0) 1))
|arith (expt 0 n)|theorem
(defthm |arith (expt 0 n)|
  (equal (expt 0 n)
    (if (zip n)
      1
      0)))
|arith (expt x 1)|theorem
(defthm |arith (expt x 1)|
  (implies (acl2-numberp x) (equal (expt x 1) x)))
|arith (expt 1 n)|theorem
(defthm |arith (expt 1 n)| (equal (expt 1 n) 1))
|arith (expt x -1)|theorem
(defthm |arith (expt x -1)| (equal (expt x -1) (/ x)))
|arith (expt (/ x) n)|theorem
(defthm |arith (expt (/ x) n)|
  (equal (expt (/ x) n) (/ (expt x n))))
|arith (expt x (- n))|theorem
(defthm |arith (expt x (- n))|
  (implies (syntaxp (negative-addends-p n))
    (equal (expt x n) (/ (expt x (- n))))))
|arith (expt 1/c n)|theorem
(defthm |arith (expt 1/c n)|
  (implies (and (syntaxp (quotep x))
      (syntaxp (rationalp (unquote x)))
      (syntaxp (not (integerp (unquote x))))
      (syntaxp (equal (numerator x) 1)))
    (equal (expt x n) (/ (expt (/ x) n)))))
|arith (expt 4 n)|theorem
(defthm |arith (expt 4 n)|
  (implies (integerp n) (equal (expt 4 n) (expt 2 (* 2 n)))))
|arith (expt 8 n)|theorem
(defthm |arith (expt 8 n)|
  (implies (integerp n) (equal (expt 8 n) (expt 2 (* 3 n)))))
|arith (expt 16 n)|theorem
(defthm |arith (expt 16 n)|
  (implies (integerp n) (equal (expt 16 n) (expt 2 (* 4 n)))))
|arith (expt (* x y) n)|theorem
(defthm |arith (expt (* x y) n)|
  (equal (expt (* x y) n) (* (expt x n) (expt y n))))
|arith (expt (expt x m) n)|theorem
(defthm |arith (expt (expt x m) n)|
  (implies (and (integerp m) (integerp n))
    (equal (expt (expt x m) n) (expt x (* m n)))))
|arith (expt x (+ m n))|theorem
(defthm |arith (expt x (+ m n))|
  (implies (and (integerp m) (integerp n))
    (equal (expt x (+ m n))
      (if (equal (+ m n) 0)
        1
        (* (expt x m) (expt x n))))))
|arith (expt x (+ m n)) non-zero x|theorem
(defthm |arith (expt x (+ m n)) non-zero x|
  (implies (and (not (equal 0 x))
      (acl2-numberp x)
      (integerp m)
      (integerp n))
    (equal (expt x (+ m n)) (* (expt x m) (expt x n))))
  :hints (("Goal" :use (|(expt x (+ m n))|))))
|arith (fix x)|theorem
(defthm |arith (fix x)|
  (implies (acl2-numberp x) (equal (fix x) x)))
|arith (* (numerator x) (/ (denominator x)))|theorem
(defthm |arith (* (numerator x) (/ (denominator x)))|
  (implies (rationalp x)
    (equal (* (numerator x) (/ (denominator x))) x)))
|arith (* c (* d x))|theorem
(defthm |arith (* c (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (* c (* d x)) (* (* c d) x))))
arith-collect-*function
(defun arith-collect-*
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (* x y))
arith-collect-*-problem-findertheorem
(defthm arith-collect-*-problem-finder
  (implies (equal x x) (equal (arith-collect-* x y) (* x y))))
in-theory
(in-theory (disable arith-collect-*-problem-finder))
|arith (* (expt x n) (expt y n))|theorem
(defthm |arith (* (expt x n) (expt y n))|
  (implies (integerp n)
    (equal (arith-collect-* (expt x n) (expt y n))
      (expt (* x y) n))))
|arith (* x x)|theorem
(defthm |arith (* x x)|
  (equal (arith-collect-* x x) (expt x 2)))
|arith (* x (/ x))|theorem
(defthm |arith (* x (/ x))|
  (equal (arith-collect-* x (/ x))
    (if (equal (fix x) 0)
      0
      1)))
|arith (* x (expt x n))|theorem
(defthm |arith (* x (expt x n))|
  (implies (integerp n)
    (equal (arith-collect-* x (expt x n))
      (if (equal (fix x) 0)
        0
        (expt x (+ n 1))))))
|arith (* x (expt (- x) n))|theorem
(defthm |arith (* x (expt (- x) n))|
  (implies (integerp n)
    (equal (arith-collect-* x (expt (- x) n))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (expt x (+ n 1)))
        (t (- (expt x (+ n 1))))))))
|arith (* x (/ (expt x n)))|theorem
(defthm |arith (* x (/ (expt x n)))|
  (implies (integerp n)
    (equal (arith-collect-* x (/ (expt x n)))
      (if (equal (fix x) 0)
        0
        (/ (expt x (- n 1)))))))
|arith (* x (/ (expt (- x) n)))|theorem
(defthm |arith (* x (/ (expt (- x) n)))|
  (implies (integerp n)
    (equal (arith-collect-* x (/ (expt (- x) n)))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (/ (expt x (- n 1))))
        (t (- (/ (expt x (- n 1)))))))))
|arith (* (/ x) (expt x n))|theorem
(defthm |arith (* (/ x) (expt x n))|
  (implies (integerp n)
    (equal (arith-collect-* (/ x) (expt x n))
      (if (equal (fix x) 0)
        0
        (expt x (- n 1))))))
|arith (* (/ x) (expt (- x) n))|theorem
(defthm |arith (* (/ x) (expt (- x) n))|
  (implies (integerp n)
    (equal (arith-collect-* (/ x) (expt (- x) n))
      (cond ((equal (fix x) 0) 0)
        ((evenp n) (expt x (- n 1)))
        (t (- (expt x (- n 1))))))))
|arith (* (expt x m) (expt x n))|theorem
(defthm |arith (* (expt x m) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))
|arith (* (expt (- x) m) (expt x n))|theorem
(defthm |arith (* (expt (- x) m) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (expt x m) (expt (- x) n))|theorem
(defthm |arith (* (expt x m) (expt (- x) n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (/ (expt x m)) (expt x n))|theorem
(defthm |arith (* (/ (expt x m)) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))
|arith (* (/ (expt (- x) m)) (expt x n))|theorem
(defthm |arith (* (/ (expt (- x) m)) (expt x n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (/ (expt x m)) (expt (- x) n))|theorem
(defthm |arith (* (/ (expt x m)) (expt (- x) n))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (expt x m) (/ (expt x n)))|theorem
(defthm |arith (* (expt x m) (/ (expt x n)))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))
|arith (* (expt (- x) m) (/ (expt x n)))|theorem
(defthm |arith (* (expt (- x) m) (/ (expt x n)))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (expt x m) (/ (expt (- x) n)))|theorem
(defthm |arith (* (expt x m) (/ (expt (- x) n)))|
  (implies (and (integerp m) (integerp n))
    (equal (arith-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))))))))
|arith (* (expt c n) (expt d n))|theorem
(defthm |arith (* (expt c n) (expt d n))|
  (implies (and (integerp n) (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (arith-collect-* (expt c n) (expt d n))
      (expt (* c d) n))))
|arith (expt x c)|theorem
(defthm |arith (expt x c)|
  (implies (and (syntaxp (quotep c)) (integerp c) (not (equal c 0)))
    (equal (expt x c)
      (cond ((< c 0) (* (/ x) (expt x (+ c 1))))
        (t (* x (expt x (- c 1)))))))
  :hints (("Goal" :in-theory (disable |arith (expt x (+ m n)) non-zero x|
       |arith (expt x (+ m n))|
       |(expt x (+ m n)) non-zero x|
       |(expt x (+ m n))|))))
|(arith-collect-* y x)|theorem
(defthm |(arith-collect-* y x)|
  (equal (arith-collect-* y x) (arith-collect-* x y)))
|arith (+ c (+ d x))|theorem
(defthm |arith (+ c (+ d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (+ c (+ d x)) (+ (+ c d) x))))
arith-collect-+function
(defun arith-collect-+
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (+ x y))
arith-collect-+-problem-findertheorem
(defthm arith-collect-+-problem-finder
  (implies (equal x x) (equal (arith-collect-+ x y) (+ x y))))
in-theory
(in-theory (disable arith-collect-+-problem-finder))
|arith (+ x x)|theorem
(defthm |arith (+ x x)|
  (equal (arith-collect-+ x x) (* 2 x)))
|arith (+ x (- x))|theorem
(defthm |arith (+ x (- x))|
  (equal (arith-collect-+ x (- x)) 0))
|arith (+ x (* c x))|theorem
(defthm |arith (+ x (* c x))|
  (implies (syntaxp (quotep c))
    (equal (arith-collect-+ x (* c x)) (* (+ c 1) x))))
|arith (+ (- x) (* c x))|theorem
(defthm |arith (+ (- x) (* c x))|
  (implies (syntaxp (quotep c))
    (equal (arith-collect-+ (- x) (* c x)) (* (- c 1) x))))
|arith (+ (* c x) (* d x))|theorem
(defthm |arith (+ (* c x) (* d x))|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (arith-collect-+ (* c x) (* d x)) (* (+ c d) x))))
|(arith-collect-+ y x)|theorem
(defthm |(arith-collect-+ y x)|
  (equal (arith-collect-+ y x) (arith-collect-+ x y)))
arith-bubble-down-*-problem-findertheorem
(defthm arith-bubble-down-*-problem-finder
  (implies (equal x x)
    (equal (* (arith-bubble-down x match) y) (* x y))))
in-theory
(in-theory (disable arith-bubble-down-*-problem-finder))
arith-bubble-down-*-bubble-downtheorem
(defthm arith-bubble-down-*-bubble-down
  (equal (* (arith-bubble-down x match) y z)
    (* y (arith-bubble-down x match) z)))
arith-bubble-down-*-match-1theorem
(defthm arith-bubble-down-*-match-1
  (implies (syntaxp (equal match y))
    (equal (* (arith-bubble-down x match) y)
      (arith-collect-* x y))))
arith-bubble-down-*-match-2theorem
(defthm arith-bubble-down-*-match-2
  (implies (syntaxp (equal match y))
    (equal (* y (arith-bubble-down x match))
      (arith-collect-* x y))))
arith-bubble-down-*-match-3theorem
(defthm arith-bubble-down-*-match-3
  (implies (syntaxp (equal match y))
    (equal (* (arith-bubble-down x match) y z)
      (* (arith-collect-* x y) z))))
arith-bubble-down-+-problem-findertheorem
(defthm arith-bubble-down-+-problem-finder
  (implies (equal x x)
    (equal (+ (arith-bubble-down x match) y) (+ x y))))
in-theory
(in-theory (disable arith-bubble-down-+-problem-finder))
arith-bubble-down-+-bubble-downtheorem
(defthm arith-bubble-down-+-bubble-down
  (equal (+ (arith-bubble-down x match) y z)
    (+ y (arith-bubble-down x match) z)))
arith-bubble-down-+-match-1theorem
(defthm arith-bubble-down-+-match-1
  (implies (syntaxp (equal match y))
    (equal (+ (arith-bubble-down x match) y)
      (arith-collect-+ x y))))
arith-bubble-down-+-match-2theorem
(defthm arith-bubble-down-+-match-2
  (implies (syntaxp (equal match y))
    (equal (+ y (arith-bubble-down x match))
      (arith-collect-+ x y))))
arith-bubble-down-+-match-3theorem
(defthm arith-bubble-down-+-match-3
  (implies (syntaxp (equal match y))
    (equal (+ (arith-bubble-down x match) y z)
      (+ (arith-collect-+ x y) z))))
in-theory
(in-theory (disable arith-bubble-down))
in-theory
(in-theory (disable arith-collect-*))
in-theory
(in-theory (disable arith-collect-+))