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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
(in-package "ACL2")
(include-book "polynomial-defuns")
(local (include-book "arithmetic-5/top" :dir :system))
(defthmd eval-polynomial-expt-correct-lemma
(implies (and (real/rational-polynomial-p poly)
(real/rationalp x)
(integerp n)
(<= 0 n))
(equal (eval-polynomial-expt-aux poly x n)
(* (expt x n)
(eval-polynomial poly x)))))
(defthmd eval-polynomial-expt-correct
(implies (and (real/rational-polynomial-p poly)
(real/rationalp x))
(equal (eval-polynomial-expt poly x)
(eval-polynomial poly x)))
:hints (("Goal"
:use ((:instance eval-polynomial-expt-correct-lemma
(n 0))))))
(defthm real-polynomial-scale-polynomial
(implies (and (real/rational-polynomial-p poly)
(real/rationalp c))
(real/rational-polynomial-p (scale-polynomial poly c))))
(defthm eval-scale-polynomial
(implies (and (real/rational-polynomial-p poly)
(real/rationalp c))
(equal (eval-polynomial (scale-polynomial poly c) x)
(* c (eval-polynomial poly x)))))
(defthm eval-scale-expt-polynomial
(implies (and (real/rational-polynomial-p poly)
(real/rationalp c)
(real/rationalp x))
(equal (eval-polynomial-expt (scale-polynomial poly c) x)
(* c (eval-polynomial-expt poly x))))
:hints (("Goal" :do-not-induct t
:in-theory (e/d (eval-polynomial-expt-correct)
(eval-polynomial-expt
scale-polynomial)))))
(defthm consp-scale-polnomial
(equal (consp (scale-polynomial poly c))
(consp poly)))
(defthm real-polynomial-+
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2))
(real/rational-polynomial-p (polynomial-+ poly1 poly2))))
(defthm eval-polynomial-+
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2)
(real/rationalp x))
(equal (eval-polynomial (polynomial-+ poly1 poly2) x)
(+ (eval-polynomial poly1 x)
(eval-polynomial poly2 x)))))
(defthm eval-polynomial-expt-+
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2)
(real/rationalp x))
(equal (eval-polynomial-expt (polynomial-+ poly1 poly2) x)
(+ (eval-polynomial-expt poly1 x)
(eval-polynomial-expt poly2 x))))
:hints (("Goal"
:in-theory (e/d (eval-polynomial-expt-correct)
(eval-polynomial-expt
polynomial-+)))))
(defthm consp-polnomial-+
(equal (consp (polynomial-+ poly1 poly2))
(or (consp poly1)
(consp poly2))))
(defthm real-polynomial-*
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2))
(real/rational-polynomial-p (polynomial-* poly1 poly2))))
(defthm eval-polynomial-*
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2)
(real/rationalp x))
(equal (eval-polynomial (polynomial-* poly1 poly2) x)
(* (eval-polynomial poly1 x)
(eval-polynomial poly2 x)))))
(defthm eval-polynomial-expt-*
(implies (and (real/rational-polynomial-p poly1)
(real/rational-polynomial-p poly2)
(real/rationalp x))
(equal (eval-polynomial-expt (polynomial-* poly1 poly2) x)
(* (eval-polynomial-expt poly1 x)
(eval-polynomial-expt poly2 x))))
:hints (("Goal"
:in-theory (e/d (eval-polynomial-expt-correct)
(eval-polynomial-expt
polynomial-*)))))
(defthm consp-polnomial-*
(equal (consp (polynomial-* poly1 poly2))
(consp poly1)))
(defthm numberp-car-poly
(implies (real/rational-polynomial-p poly)
(equal (acl2-numberp (car poly))
(consp poly))))
|
