blob: 6095b59a2c4328e8b92c65b9e0db68b787c91075 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(in-package "POL")
(include-book "addition")
;;; -------------------
;;; Polynomial negation
;;; -------------------
(defun - (p)
(cond ((or (not (polynomialp p)) (nullp p))
*null*)
(t
(polynomial (monomial (COMMON-LISP::- (coefficient (first p)))
(term (first p)))
(- (rest p))))))
;;; Type rule.
(defthm polynomialp--
(polynomialp (- p))
:rule-classes :type-prescription)
;;; Addition of a polynomial to its negative equals to the additive
;;; identity polynomial.
(defthm +--
(= (+ p (- p)) *null*))
;;; Polynomial negation distributes over addition of monomial and
;;; polynomial.
(defthm --distributes-+-monomial
(implies (and (monomialp m) (polynomialp p))
(equal (- (+-monomial m p))
(+-monomial (monomial (COMMON-LISP::- (coefficient m)) (term m))
(- p)))))
;;; Polynomial negation distributes over polynomial addition.
(defthm --distributes-+
(= (- (+ p1 p2)) (+ (- p1) (- p2))))
|
