Filtering...

simplify

books/arithmetic-3/bind-free/simplify

Included Books

simplify-helper basic common top
other
(in-package "ACL2")
local
(local (include-book "simplify-helper"))
local
(local (include-book "basic"))
include-book
(include-book "common")
other
(table acl2-defaults-table :state-ok t)
local
(local (defthm rewrite-equal-<-to-iff-<
    (equal (equal (< a b) (< c d)) (iff (< a b) (< c d)))))
local
(local (encapsulate nil
    (local (include-book "../pass1/top"))
    (defthm equal-*-/-1
      (equal (equal (* (/ x) y) z)
        (if (equal (fix x) 0)
          (equal z 0)
          (and (acl2-numberp z) (equal (fix y) (* x z))))))
    (defthm equal-*-/-2
      (equal (equal (* y (/ x)) z)
        (if (equal (fix x) 0)
          (equal z 0)
          (and (acl2-numberp z) (equal (fix y) (* z x))))))))
insert-0function
(defun insert-0
  (x y)
  (declare (xargs :guard t))
  (declare (ignore x))
  y)
insert-0-x-ytheorem
(defthm insert-0-x-y (equal (insert-0 x y) y))
insert-0-x-xtheorem
(defthm insert-0-x-x
  (implies (equal x 0) (equal (insert-0 x x) 0)))
insert-0-+theorem
(defthm insert-0-+
  (equal (insert-0 x (+ y z))
    (+ (insert-0 x y) (insert-0 x z))))
insert-0-*theorem
(defthm insert-0-*
  (equal (insert-0 x (* y z))
    (* (insert-0 x y) (insert-0 x z))))
in-theory
(in-theory (disable insert-0))
other
(theory-invariant (not (active-runep '(:definition insert-0)))
  :error nil)
addend-valfunction
(defun addend-val
  (addend)
  (declare (xargs :guard (pseudo-termp addend)))
  (cond ((variablep addend) 1)
    ((fquotep addend) 1)
    ((eq (ffn-symb addend) 'unary--) (addend-val (arg1 addend)))
    ((and (eq (ffn-symb addend) 'binary-*)
       (rational-constant-p (arg1 addend))) (unquote (arg1 addend)))
    (t 1)))
factorsfunction
(defun factors
  (product)
  (declare (xargs :guard (pseudo-termp product)))
  (if (eq (fn-symb product) 'binary-*)
    (cons (fargn product 1) (factors (fargn product 2)))
    (list product)))
make-productfunction
(defun make-product
  (factors)
  (declare (xargs :guard (true-listp factors)))
  (cond ((null factors) ''1)
    ((null (cdr factors)) (car factors))
    ((null (cddr factors)) (list 'binary-* (car factors) (cadr factors)))
    (t (list 'binary-* (car factors) (make-product (cdr factors))))))
remainder-bbbfunction
(defun remainder-bbb
  (common-factors sum)
  (declare (xargs :guard (and (true-listp common-factors) (pseudo-termp sum))))
  (if (eq (fn-symb sum) 'binary-+)
    (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
             common-factors))))
      (list 'binary-+
        first
        (remainder-bbb common-factors (fargn sum 2))))
    (make-product (set-difference-equal (factors sum) common-factors))))
common-factors-aaafunction
(defun common-factors-aaa
  (factors sum)
  (declare (xargs :measure (acl2-count sum)
      :guard (and (true-listp factors) (pseudo-termp sum))))
  (cond ((null factors) nil)
    ((eq (fn-symb sum) 'binary-+) (common-factors-aaa (intersection-equal factors (factors (fargn sum 1)))
        (fargn sum 2)))
    (t (intersection-equal factors (factors sum)))))
simplify-terms-such-as-a+ab-rel-0-fnfunction
(defun simplify-terms-such-as-a+ab-rel-0-fn
  (sum)
  (declare (xargs :guard (pseudo-termp sum)))
  (if (eq (fn-symb sum) 'binary-+)
    (let ((common-factors (common-factors-aaa (factors (fargn sum 1)) (fargn sum 2))))
      (if common-factors
        (let ((common (make-product common-factors)) (remainder (remainder-bbb common-factors sum)))
          (list (cons 'common common) (cons 'remainder remainder)))
        nil))
    nil))
simplify-terms-such-as-a+ab-=-0theorem
(defthm simplify-terms-such-as-a+ab-=-0
  (implies (and (bind-free (simplify-terms-such-as-a+ab-rel-0-fn sum)
        (common remainder))
      (acl2-numberp common)
      (acl2-numberp remainder)
      (equal sum (* common remainder)))
    (equal (equal sum 0)
      (or (equal common 0) (equal remainder 0)))))
simplify-terms-such-as-a+ab-<-0theorem
(defthm simplify-terms-such-as-a+ab-<-0
  (implies (and (bind-free (simplify-terms-such-as-a+ab-rel-0-fn sum)
        (common remainder))
      (rationalp common)
      (rationalp remainder)
      (equal sum (* common remainder)))
    (equal (< sum 0)
      (cond ((< common 0) (< 0 remainder))
        ((< 0 common) (< remainder 0))
        (t nil)))))
simplify-terms-such-as-0-<-a+abtheorem
(defthm simplify-terms-such-as-0-<-a+ab
  (implies (and (bind-free (simplify-terms-such-as-a+ab-rel-0-fn sum)
        (common remainder))
      (rationalp common)
      (rationalp remainder)
      (equal sum (* common remainder)))
    (equal (< 0 sum)
      (cond ((< 0 common) (< 0 remainder))
        ((< common 0) (< remainder 0))
        (t nil)))))
factor-val-gather-exponents1function
(defun factor-val-gather-exponents1
  (exponent)
  (declare (xargs :guard (pseudo-termp exponent)))
  (cond ((variablep exponent) 1)
    ((rational-constant-p exponent) (unquote exponent))
    ((eq (ffn-symb exponent) 'binary-*) (if (rational-constant-p (arg1 exponent))
        (unquote (arg1 exponent))
        1))
    ((eq (ffn-symb exponent) 'binary-+) (+ (factor-val-gather-exponents1 (arg1 exponent))
        (factor-val-gather-exponents1 (arg2 exponent))))
    (t 1)))
factor-val-gather-exponentsfunction
(defun factor-val-gather-exponents
  (factor)
  (declare (xargs :guard (pseudo-termp factor)))
  (cond ((variablep factor) 1)
    ((fquotep factor) 1)
    ((eq (ffn-symb factor) 'unary-/) (factor-val-gather-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'unary--) (factor-val-gather-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'expt) (factor-val-gather-exponents1 (arg2 factor)))
    (t 1)))
factor-val-scatter-exponents1function
(defun factor-val-scatter-exponents1
  (exponent)
  (declare (xargs :guard (pseudo-termp exponent)))
  (cond ((variablep exponent) 1)
    ((rational-constant-p exponent) (unquote exponent))
    ((eq (ffn-symb exponent) 'binary-*) (if (rational-constant-p (arg1 exponent))
        (unquote (arg1 exponent))
        1))
    ((eq (ffn-symb exponent) 'binary-+) (+ (factor-val-scatter-exponents1 (arg1 exponent))
        (factor-val-scatter-exponents1 (arg2 exponent))))
    (t 1)))
factor-val-scatter-exponentsfunction
(defun factor-val-scatter-exponents
  (factor)
  (declare (xargs :guard (pseudo-termp factor)))
  (cond ((variablep factor) 1)
    ((fquotep factor) 1)
    ((eq (ffn-symb factor) 'unary-/) (factor-val-scatter-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'unary--) (factor-val-scatter-exponents (arg1 factor)))
    ((eq (ffn-symb factor) 'expt) (factor-val-scatter-exponents1 (arg2 factor)))
    (t 1)))
addend-info-entryfunction
(defun addend-info-entry
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (list (addend-pattern x) (addend-val x) x))
info-entry-pfunction
(defun info-entry-p
  (x)
  (declare (xargs :guard t))
  (and (true-listp x) (rationalp (cadr x))))
addend-info-listfunction
(defun addend-info-list
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (if (eq (fn-symb x) 'binary-+)
    (cons (addend-info-entry (arg1 x))
      (addend-info-list (arg2 x)))
    (list (addend-info-entry x))))
info-list-pfunction
(defun info-list-p
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (info-entry-p (car x)) (info-list-p (cdr x)))
    (eq x nil)))
rationalp-of-addend-valtheorem
(defthm rationalp-of-addend-val
  (implies (pseudo-termp x) (rationalp (addend-val x))))
info-list-p-of-addend-info-listtheorem
(defthm info-list-p-of-addend-info-list
  (implies (pseudo-termp x)
    (info-list-p (addend-info-list x))))
assoc-addendfunction
(defun assoc-addend
  (x info-list)
  (declare (xargs :guard (info-list-p info-list)))
  (cond ((endp info-list) nil)
    ((matching-addend-patterns-p x (caar info-list)) (car info-list))
    (t (assoc-addend x (cdr info-list)))))
first-match-in-addend-info-listsfunction
(defun first-match-in-addend-info-lists
  (info-list1 info-list2)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-addend (car (car info-list1)) info-list2)))
      (if temp
        (if (<= (cadr (car info-list1)) (cadr temp))
          (caddr (car info-list1))
          (caddr temp))
        (first-match-in-addend-info-lists (cdr info-list1)
          info-list2)))))
find-matching-addendsfunction
(defun find-matching-addends
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((info-list1 (addend-info-list lhs)) (info-list2 (addend-info-list rhs))
      (match (first-match-in-addend-info-lists info-list1 info-list2)))
    (if match
      (list (cons 'x match))
      nil)))
simplify-sums-equaltheorem
(defthm simplify-sums-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-matching-addends lhs rhs) (x)))
    (equal (equal lhs rhs) (equal (+ (- x) lhs) (+ (- x) rhs)))))
local
(local (in-theory (disable simplify-sums-equal)))
simplify-sums-<theorem
(defthm simplify-sums-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-matching-addends lhs rhs) (x)))
    (equal (< lhs rhs) (< (+ (- x) lhs) (+ (- x) rhs)))))
local
(local (in-theory (disable simplify-sums-<)))
negative-addend-pfunction
(defun negative-addend-p
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (or (and (quotep x) (rationalp (unquote x)) (< (unquote x) 0))
    (and (eq (fn-symb x) 'unary--)
      (or (variablep (arg1 x))
        (not (equal (ffn-symb (arg1 x)) 'unary--))))
    (and (eq (fn-symb x) 'binary-*)
      (rational-constant-p (arg1 x))
      (< (unquote (arg1 x)) 0))))
find-negative-addend1function
(defun find-negative-addend1
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((not (eq (fn-symb x) 'binary-+)) (if (negative-addend-p x)
        x
        nil))
    ((negative-addend-p (arg1 x)) (arg1 x))
    ((eq (fn-symb (arg2 x)) 'binary-+) (find-negative-addend1 (arg2 x)))
    ((negative-addend-p (arg2 x)) (arg2 x))
    (t nil)))
find-negative-addendfunction
(defun find-negative-addend
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let ((temp1 (find-negative-addend1 lhs)))
    (if temp1
      (list (cons 'x temp1))
      (let ((temp2 (find-negative-addend1 rhs)))
        (if temp2
          (list (cons 'x temp2))
          nil)))))
prefer-positive-addends-equaltheorem
(defthm prefer-positive-addends-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (or (equal (fn-symb lhs) 'binary-+)
          (equal (fn-symb rhs) 'binary-+)))
      (bind-free (find-negative-addend lhs rhs) (x)))
    (equal (equal lhs rhs) (equal (+ (- x) lhs) (+ (- x) rhs)))))
local
(local (in-theory (disable prefer-positive-addends-equal)))
prefer-positive-addends-<theorem
(defthm prefer-positive-addends-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (or (equal (fn-symb lhs) 'binary-+)
          (equal (fn-symb rhs) 'binary-+)))
      (bind-free (find-negative-addend lhs rhs) (x)))
    (equal (< lhs rhs) (< (+ (- x) lhs) (+ (- x) rhs)))))
local
(local (in-theory (disable prefer-positive-addends-<)))
factor-gather-exponents-info-entryfunction
(defun factor-gather-exponents-info-entry
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (list (factor-pattern-gather-exponents x)
    (factor-val-gather-exponents x)
    x))
assoc-factor-gather-exponentsfunction
(defun assoc-factor-gather-exponents
  (x info-list)
  (declare (xargs :guard (info-list-p info-list)))
  (cond ((endp info-list) nil)
    ((matching-factor-gather-exponents-patterns-p x
       (caar info-list)) (car info-list))
    (t (assoc-factor-gather-exponents x (cdr info-list)))))
factor-gather-exponents-intersect-info-listsfunction
(defun factor-gather-exponents-intersect-info-lists
  (info-list1 info-list2)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-gather-exponents (caar info-list1) info-list2)))
      (cond ((not temp) (factor-gather-exponents-intersect-info-lists (cdr info-list1)
            info-list2))
        ((<= (cadr temp) (cadr (car info-list1))) (cons temp
            (factor-gather-exponents-intersect-info-lists (cdr info-list1)
              info-list2)))
        (t (cons (car info-list1)
            (factor-gather-exponents-intersect-info-lists (cdr info-list1)
              info-list2)))))))
info-entry-p-of-assoc-factor-gather-exponentstheorem
(defthm info-entry-p-of-assoc-factor-gather-exponents
  (implies (and (info-list-p info-list)
      (assoc-factor-gather-exponents x info-list))
    (info-entry-p (assoc-factor-gather-exponents x info-list))))
info-list-p-of-factor-gather-exponents-intersect-info-liststheorem
(defthm info-list-p-of-factor-gather-exponents-intersect-info-lists
  (implies (and (info-list-p info-list-1) (info-list-p info-list-2))
    (info-list-p (factor-gather-exponents-intersect-info-lists info-list-1
        info-list-2))))
rationalp-of-factor-val-gather-exponentstheorem
(defthm rationalp-of-factor-val-gather-exponents
  (rationalp (factor-val-gather-exponents x))
  :rule-classes :type-prescription)
factor-gather-exponents-info-listfunction
(defun factor-gather-exponents-info-list
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((temp (factor-gather-exponents-info-list (arg2 x))))
        (if temp
          (factor-gather-exponents-intersect-info-lists temp
            (factor-gather-exponents-info-list (arg1 x)))
          nil)))
    ((eq (fn-symb x) 'binary-*) (cons (factor-gather-exponents-info-entry (arg1 x))
        (factor-gather-exponents-info-list (arg2 x))))
    (t (list (factor-gather-exponents-info-entry x)))))
info-list-p-of-factor-gather-exponents-info-listtheorem
(defthm info-list-p-of-factor-gather-exponents-info-list
  (implies (pseudo-termp x)
    (info-list-p (factor-gather-exponents-info-list x))))
first-match-in-factor-gather-exponents-info-listsfunction
(defun first-match-in-factor-gather-exponents-info-lists
  (info-list1 info-list2)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-gather-exponents (car (car info-list1))
           info-list2)))
      (if temp
        (if (<= (cadr (car info-list1)) (cadr temp))
          (caddr (car info-list1))
          (caddr temp))
        (first-match-in-factor-gather-exponents-info-lists (cdr info-list1)
          info-list2)))))
find-matching-factors-gather-exponentsfunction
(defun find-matching-factors-gather-exponents
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((info-list1 (factor-gather-exponents-info-list lhs)) (info-list2 (if info-list1
          (factor-gather-exponents-info-list rhs)
          nil))
      (match (if info-list2
          (first-match-in-factor-gather-exponents-info-lists info-list1
            info-list2)
          nil)))
    (if match
      (list (cons 'x match))
      nil)))
simplify-products-gather-exponents-equaltheorem
(defthm simplify-products-gather-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-matching-factors-gather-exponents lhs rhs)
        (x))
      (case-split (acl2-numberp x)))
    (equal (equal lhs rhs)
      (if (equal x 0)
        (equal (insert-0 x lhs) (insert-0 x rhs))
        (equal (* (/ x) lhs) (* (/ x) rhs))))))
local
(local (in-theory (disable simplify-products-gather-exponents-equal)))
first-rational-match-in-factor-gather-exponents-info-listsfunction
(defun first-rational-match-in-factor-gather-exponents-info-lists
  (info-list1 info-list2 mfc state)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-gather-exponents (car (car info-list1))
           info-list2)))
      (if (and temp (proveably-rational (caddr temp) mfc state))
        (if (<= (cadr (car info-list1)) (cadr temp))
          (caddr (car info-list1))
          (caddr temp))
        (first-rational-match-in-factor-gather-exponents-info-lists (cdr info-list1)
          info-list2
          mfc
          state)))))
find-rational-matching-factors-gather-exponentsfunction
(defun find-rational-matching-factors-gather-exponents
  (lhs rhs mfc state)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((info-list1 (factor-gather-exponents-info-list lhs)) (info-list2 (if info-list1
          (factor-gather-exponents-info-list rhs)
          nil))
      (match (if info-list2
          (first-rational-match-in-factor-gather-exponents-info-lists info-list1
            info-list2
            mfc
            state)
          nil)))
    (if match
      (list (cons 'x match))
      nil)))
simplify-products-gather-exponents-<theorem
(defthm simplify-products-gather-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-rational-matching-factors-gather-exponents lhs
          rhs
          mfc
          state)
        (x))
      (case-split (rationalp x)))
    (equal (< lhs rhs)
      (cond ((equal x 0) (< (insert-0 x lhs) (insert-0 x rhs)))
        ((< 0 x) (< (* (/ x) lhs) (* (/ x) rhs)))
        (t (< (* (/ x) rhs) (* (/ x) lhs)))))))
local
(local (in-theory (disable simplify-products-gather-exponents-<)))
factor-scatter-exponents-info-entryfunction
(defun factor-scatter-exponents-info-entry
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (list (factor-pattern-scatter-exponents x)
    (factor-val-scatter-exponents x)
    x))
assoc-factor-scatter-exponentsfunction
(defun assoc-factor-scatter-exponents
  (x info-list)
  (declare (xargs :guard (info-list-p info-list)))
  (cond ((endp info-list) nil)
    ((matching-factor-scatter-exponents-patterns-p x
       (caar info-list)) (car info-list))
    (t (assoc-factor-scatter-exponents x (cdr info-list)))))
factor-scatter-exponents-intersect-info-listsfunction
(defun factor-scatter-exponents-intersect-info-lists
  (info-list1 info-list2)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-scatter-exponents (caar info-list1)
           info-list2)))
      (cond ((not temp) (factor-scatter-exponents-intersect-info-lists (cdr info-list1)
            info-list2))
        ((<= (cadr temp) (cadr (car info-list1))) (cons temp
            (factor-scatter-exponents-intersect-info-lists (cdr info-list1)
              info-list2)))
        (t (cons (car info-list1)
            (factor-scatter-exponents-intersect-info-lists (cdr info-list1)
              info-list2)))))))
info-entry-p-of-assoc-factor-scatter-exponentstheorem
(defthm info-entry-p-of-assoc-factor-scatter-exponents
  (implies (and (info-list-p info-list)
      (assoc-factor-scatter-exponents x info-list))
    (info-entry-p (assoc-factor-scatter-exponents x info-list))))
info-list-p-of-factor-scatter-exponents-intersect-info-liststheorem
(defthm info-list-p-of-factor-scatter-exponents-intersect-info-lists
  (implies (and (info-list-p info-list-1) (info-list-p info-list-2))
    (info-list-p (factor-scatter-exponents-intersect-info-lists info-list-1
        info-list-2))))
rationalp-of-factor-val-scatter-exponentstheorem
(defthm rationalp-of-factor-val-scatter-exponents
  (rationalp (factor-val-scatter-exponents x))
  :rule-classes :type-prescription)
factor-scatter-exponents-info-listfunction
(defun factor-scatter-exponents-info-list
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((eq (fn-symb x) 'binary-+) (let ((temp (factor-scatter-exponents-info-list (arg2 x))))
        (if temp
          (factor-scatter-exponents-intersect-info-lists temp
            (factor-scatter-exponents-info-list (arg1 x)))
          nil)))
    ((eq (fn-symb x) 'binary-*) (cons (factor-scatter-exponents-info-entry (arg1 x))
        (factor-scatter-exponents-info-list (arg2 x))))
    (t (list (factor-scatter-exponents-info-entry x)))))
info-list-p-of-factor-gather-exponents-info-listtheorem
(defthm info-list-p-of-factor-gather-exponents-info-list
  (implies (pseudo-termp x)
    (info-list-p (factor-gather-exponents-info-list x))))
first-match-in-factor-scatter-exponents-info-listsfunction
(defun first-match-in-factor-scatter-exponents-info-lists
  (info-list1 info-list2)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-scatter-exponents (car (car info-list1))
           info-list2)))
      (if temp
        (if (<= (cadr (car info-list1)) (cadr temp))
          (caddr (car info-list1))
          (caddr temp))
        (first-match-in-factor-scatter-exponents-info-lists (cdr info-list1)
          info-list2)))))
find-matching-factors-scatter-exponentsfunction
(defun find-matching-factors-scatter-exponents
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((info-list1 (factor-scatter-exponents-info-list lhs)) (info-list2 (if info-list1
          (factor-scatter-exponents-info-list rhs)
          nil))
      (match (if info-list2
          (first-match-in-factor-scatter-exponents-info-lists info-list1
            info-list2)
          nil)))
    (if match
      (list (cons 'x match))
      nil)))
simplify-products-scatter-exponents-equaltheorem
(defthm simplify-products-scatter-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-matching-factors-scatter-exponents lhs rhs)
        (x))
      (case-split (acl2-numberp x)))
    (equal (equal lhs rhs)
      (if (equal x 0)
        (equal (insert-0 x lhs) (insert-0 x rhs))
        (equal (* (/ x) lhs) (* (/ x) rhs))))))
local
(local (in-theory (disable simplify-products-scatter-exponents-equal)))
first-rational-match-in-factor-scatter-exponents-info-listsfunction
(defun first-rational-match-in-factor-scatter-exponents-info-lists
  (info-list1 info-list2 mfc state)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-factor-scatter-exponents (car (car info-list1))
           info-list2)))
      (if (and temp (proveably-rational (caddr temp) mfc state))
        (if (<= (cadr (car info-list1)) (cadr temp))
          (caddr (car info-list1))
          (caddr temp))
        (first-rational-match-in-factor-scatter-exponents-info-lists (cdr info-list1)
          info-list2
          mfc
          state)))))
find-rational-matching-factors-scatter-exponentsfunction
(defun find-rational-matching-factors-scatter-exponents
  (lhs rhs mfc state)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((info-list1 (factor-scatter-exponents-info-list lhs)) (info-list2 (if info-list1
          (factor-scatter-exponents-info-list rhs)
          nil))
      (match (if info-list2
          (first-rational-match-in-factor-scatter-exponents-info-lists info-list1
            info-list2
            mfc
            state)
          nil)))
    (if match
      (list (cons 'x match))
      nil)))
simplify-products-scatter-exponents-<theorem
(defthm simplify-products-scatter-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (bind-free (find-rational-matching-factors-scatter-exponents lhs
          rhs
          mfc
          state)
        (x))
      (case-split (rationalp x)))
    (equal (< lhs rhs)
      (cond ((equal x 0) (< (insert-0 x lhs) (insert-0 x rhs)))
        ((< 0 x) (< (* (/ x) lhs) (* (/ x) rhs)))
        (t (< (* (/ x) rhs) (* (/ x) lhs)))))))
local
(local (in-theory (disable simplify-products-scatter-exponents-<)))
find-negative-factor-scatter-exponents2function
(defun find-negative-factor-scatter-exponents2
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'unary-/) x)
    ((eq (ffn-symb x) 'expt) (cond ((eq (fn-symb (arg1 x)) 'unary-/) x)
        ((and (quotep (arg1 x))
           (not (integerp (cadr (arg1 x))))
           (rationalp (cadr (arg1 x)))
           (eql (numerator (cadr (arg1 x))) 1)) x)
        ((eq (fn-symb (arg2 x)) 'unary--) x)
        ((and (eq (fn-symb (arg2 x)) 'binary-*)
           (rational-constant-p (arg1 (arg2 x)))
           (< (unquote (arg1 (arg2 x))) 0)) x)
        (t nil)))
    ((eq (ffn-symb x) 'binary-*) (let ((temp (find-negative-factor-scatter-exponents2 (arg1 x))))
        (if temp
          temp
          (find-negative-factor-scatter-exponents2 (arg2 x)))))
    (t nil)))
find-negative-factor-scatter-exponents1function
(defun find-negative-factor-scatter-exponents1
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'binary-+) (let ((temp (find-negative-factor-scatter-exponents2 (arg1 x))))
        (if temp
          temp
          (find-negative-factor-scatter-exponents1 (arg2 x)))))
    (t (find-negative-factor-scatter-exponents2 x))))
find-negative-factor-scatter-exponentsfunction
(defun find-negative-factor-scatter-exponents
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let ((temp1 (find-negative-factor-scatter-exponents1 lhs)))
    (if temp1
      (list (cons 'x temp1))
      (let ((temp2 (find-negative-factor-scatter-exponents1 rhs)))
        (if temp2
          (list (cons 'x temp2))
          nil)))))
prefer-positive-exponents-scatter-exponents-equaltheorem
(defthm prefer-positive-exponents-scatter-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (equal rhs ''0)))
      (syntaxp (not (equal lhs ''0)))
      (bind-free (find-negative-factor-scatter-exponents lhs rhs)
        (x))
      (case-split (acl2-numberp x)))
    (equal (equal lhs rhs)
      (if (equal x 0)
        (equal (insert-0 x lhs) (insert-0 x rhs))
        (equal (* (/ x) lhs) (* (/ x) rhs))))))
find-rational-negative-factor-scatter-exponents2function
(defun find-rational-negative-factor-scatter-exponents2
  (x mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'unary-/) (if (proveably-rational x mfc state)
        x
        nil))
    ((eq (ffn-symb x) 'expt) (cond ((eq (fn-symb (arg1 x)) 'unary-/) (if (proveably-rational x mfc state)
            x
            nil))
        ((and (quotep (arg1 x))
           (not (integerp (cadr (arg1 x))))
           (rationalp (cadr (arg1 x)))
           (eql (numerator (cadr (arg1 x))) 1)) (if (proveably-rational x mfc state)
            x
            nil))
        ((eq (fn-symb (arg2 x)) 'unary--) (if (proveably-rational x mfc state)
            x
            nil))
        ((and (eq (fn-symb (arg2 x)) 'binary-*)
           (rational-constant-p (arg1 (arg2 x)))
           (< (unquote (arg1 (arg2 x))) 0)) (if (proveably-rational x mfc state)
            x
            nil))
        (t nil)))
    ((eq (ffn-symb x) 'binary-*) (let ((temp (find-rational-negative-factor-scatter-exponents2 (arg1 x)
             mfc
             state)))
        (if temp
          temp
          (find-rational-negative-factor-scatter-exponents2 (arg2 x)
            mfc
            state))))
    (t nil)))
find-rational-negative-factor-scatter-exponents1function
(defun find-rational-negative-factor-scatter-exponents1
  (x mfc state)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'binary-+) (let ((temp (find-rational-negative-factor-scatter-exponents2 (arg1 x)
             mfc
             state)))
        (if temp
          temp
          (find-rational-negative-factor-scatter-exponents1 (arg2 x)
            mfc
            state))))
    (t (find-rational-negative-factor-scatter-exponents2 x
        mfc
        state))))
find-rational-negative-factor-scatter-exponentsfunction
(defun find-rational-negative-factor-scatter-exponents
  (lhs rhs mfc state)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let ((temp1 (find-rational-negative-factor-scatter-exponents1 lhs
         mfc
         state)))
    (if temp1
      (list (cons 'x temp1))
      (let ((temp2 (find-rational-negative-factor-scatter-exponents1 rhs
             mfc
             state)))
        (if temp2
          (list (cons 'x temp2))
          nil)))))
prefer-positive-exponents-scatter-exponents-<theorem
(defthm prefer-positive-exponents-scatter-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (equal rhs ''0)))
      (syntaxp (not (equal lhs ''0)))
      (bind-free (find-rational-negative-factor-scatter-exponents lhs
          rhs
          mfc
          state)
        (x))
      (case-split (rationalp x)))
    (equal (< lhs rhs)
      (cond ((equal x 0) (< (insert-0 x lhs) (insert-0 x rhs)))
        ((< 0 x) (< (* (/ x) lhs) (* (/ x) rhs)))
        (t (< (* (/ x) rhs) (* (/ x) lhs)))))))