common-factor-defuns

Included Books

other

(in-package "ACL2")

include-book

(include-book "inverted-factor")

my-intersection-equalfunction

(defund my-intersection-equal
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (cond ((endp x) nil)
    ((member-equal (car x) y) (cons (car x) (my-intersection-equal (cdr x) y)))
    (t (my-intersection-equal (cdr x) y))))

adjoin-equalfunction

(defun adjoin-equal
  (x l)
  (declare (xargs :guard (true-listp l)))
  (if (member-equal x l)
    l
    (cons x l)))

remove-onefunction

(defund remove-one
  (x l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
    ((equal x (car l)) (cdr l))
    (t (cons (car l) (remove-one x (cdr l))))))

remove-one-preserves-true-listptheorem

(defthm remove-one-preserves-true-listp
  (implies (true-listp l) (true-listp (remove-one x l)))
  :hints (("Goal" :in-theory (enable remove-one))))

get-factors-of-productfunction

(defund get-factors-of-product
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (consp term))
    (list term)
    (if (not (equal (car term) 'binary-*))
      (list term)
      (adjoin-equal (cadr term)
        (get-factors-of-product (caddr term))))))

get-factors-of-product-true-listptheorem

(defthm get-factors-of-product-true-listp
  (true-listp (get-factors-of-product term))
  :hints (("Goal" :in-theory (enable get-factors-of-product))))

in-theory

(in-theory (disable true-listp
    factor-syntaxp
    product-syntaxp
    sum-of-products-syntaxp))

find-inverted-factors-in-listfunction

(defund find-inverted-factors-in-list
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (if (endp lst)
    nil
    (if (and (consp (car lst)) (equal (caar lst) 'unary-/))
      (cons (car lst) (find-inverted-factors-in-list (cdr lst)))
      (find-inverted-factors-in-list (cdr lst)))))

remove-cancelling-factor-pairs-helperfunction

(defund remove-cancelling-factor-pairs-helper
  (inverted-factor-lst lst)
  (declare (xargs :guard (and (true-listp lst) (true-listp inverted-factor-lst))))
  (if (endp inverted-factor-lst)
    lst
    (let* ((inverted-factor (car inverted-factor-lst)) (non-inverted-factor (and (consp inverted-factor)
            (consp (cdr inverted-factor))
            (cadr inverted-factor))))
      (if (member-equal non-inverted-factor lst)
        (remove-cancelling-factor-pairs-helper (cdr inverted-factor-lst)
          (remove-one inverted-factor
            (remove-one non-inverted-factor lst)))
        (remove-cancelling-factor-pairs-helper (cdr inverted-factor-lst)
          lst)))))

remove-cancelling-factor-pairs-helper-preserves-true-listptheorem

(defthm remove-cancelling-factor-pairs-helper-preserves-true-listp
  (implies (true-listp l)
    (true-listp (remove-cancelling-factor-pairs-helper i l)))
  :hints (("Goal" :in-theory (enable remove-cancelling-factor-pairs-helper))))

remove-cancelling-factor-pairsfunction

(defund remove-cancelling-factor-pairs
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (let* ((inverted-factor-lst (find-inverted-factors-in-list lst)))
    (if inverted-factor-lst
      (remove-cancelling-factor-pairs-helper inverted-factor-lst
        lst)
      lst)))

remove-cancelling-factor-pairs-preserves-true-listptheorem

(defthm remove-cancelling-factor-pairs-preserves-true-listp
  (implies (true-listp l)
    (true-listp (remove-cancelling-factor-pairs l)))
  :hints (("Goal" :in-theory (enable remove-cancelling-factor-pairs))))

find-common-factors-in-sum-of-products-auxfunction

(defund find-common-factors-in-sum-of-products-aux
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (not (sum-of-products-syntaxp term))
    nil
    (if (not (consp term))
      (list term)
      (case (car term)
        (binary-+ (my-intersection-equal (get-factors-of-product (cadr term))
            (find-common-factors-in-sum-of-products-aux (caddr term))))
        (otherwise (get-factors-of-product term))))))

find-common-factors-in-sum-of-products-aux-true-listptheorem

(defthm find-common-factors-in-sum-of-products-aux-true-listp
  (true-listp (find-common-factors-in-sum-of-products-aux term))
  :hints (("Goal" :in-theory (enable find-common-factors-in-sum-of-products-aux))))

find-common-factors-in-sum-of-productsfunction

(defund find-common-factors-in-sum-of-products
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (remove-cancelling-factor-pairs (find-common-factors-in-sum-of-products-aux term)))

find-common-factors-in-sum-of-products-true-listptheorem

(defthm find-common-factors-in-sum-of-products-true-listp
  (true-listp (find-common-factors-in-sum-of-products term))
  :hints (("Goal" :in-theory (enable find-common-factors-in-sum-of-products))))

make-product-from-list-of-factorsfunction

(defund make-product-from-list-of-factors
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (if (endp lst)
    1
    (if (endp (cdr lst))
      (car lst)
      (list 'binary-*
        (car lst)
        (make-product-from-list-of-factors (cdr lst))))))

find-common-factors-to-cancelfunction

(defun find-common-factors-to-cancel
  (lhs rhs)
  (declare (xargs :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (remove-cancelling-factor-pairs (my-intersection-equal (find-common-factors-in-sum-of-products lhs)
      (find-common-factors-in-sum-of-products rhs))))

bind-k-to-common-factorsfunction

(defund bind-k-to-common-factors
  (lhs rhs)
  (declare (xargs :guard-hints (("Goal" :use (:instance remove-cancelling-factor-pairs-preserves-true-listp
           (l (my-intersection-equal (find-common-factors-in-sum-of-products lhs)
               (find-common-factors-in-sum-of-products rhs))))))
      :guard (and (pseudo-termp lhs) (pseudo-termp rhs))))
  (let* ((common-factor-list (find-common-factors-to-cancel lhs rhs)))
    (if (endp common-factor-list)
      nil
      (list (cons 'k
          (make-product-from-list-of-factors common-factor-list))))))