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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;
;; basic-arithmetic-helper.lisp
;;
;; RK 3/15/99 The following is copied from the books of Cowles
;; and adapted to the needs at hand.
;; (Note from Matt Kaufmann: While this appears to be fair use,
;; John Cowles has granted explicit permission for this in an
;; email to me on 8/5/2013.)
(in-package "ACL2")
(encapsulate
()
(local
(defthm commutativity-2-of-*-lemma
(implies (and (acl2-numberp x)
(acl2-numberp y)
(acl2-numberp z))
(equal (* (* x y) z)
(* (* y x) z)))
:rule-classes nil
:hints (("Goal"
:in-theory (disable associativity-of-*)))))
(defthm commutativity-2-of-*
(equal (* x (* y z))
(* y (* x z)))
:hints
(("Goal"
:use commutativity-2-of-*-lemma)))
)
(encapsulate
()
(local
(defthm equiv-1-implies-equiv-*
(implies (equal x1 x2)
(equal (* x1 y)
(* x2 y)))
:rule-classes nil))
(defthm right-cancellation-for-*
(equal (equal (* x z) (* y z))
(or (equal 0 (fix z))
(equal (fix x) (fix y))))
:hints (("Subgoal 9"
:use (:instance
equiv-1-implies-equiv-*
(x1 (* x z))
(x2 (* y z))
(y (/ z))))))
)
(encapsulate
()
(local
(defthm uniqueness-of-*-inverses-lemma
(implies (and (acl2-numberp x)
(not (equal x 0))
(acl2-numberp y)
(equal (* x y)
1))
(equal (/ x) y))
:rule-classes nil
:hints (("Goal"
:use (:instance
right-cancellation-for-*
(x y)
(y (/ x))
(z x))))))
(defthm equal-/
(equal (equal (/ x) y)
(if (not (equal (fix x) 0))
(equal 1 (* x y))
(equal y 0)))
:hints (("Goal" :use uniqueness-of-*-inverses-lemma)))
)
(defthm functional-self-inversion-of-/
(equal (/ (/ x)) (fix x)))
(encapsulate
()
(local
(defthm distributivity-of-/-over-*-lemma
(implies (and (acl2-numberp x)
(not (equal x 0))
(acl2-numberp y)
(not (equal y 0)))
(equal (/ (* x y))
(* (/ x) (/ y))))
:rule-classes nil
:hints (("Goal"
:use (:instance
equal-/
(x (* x y))
(y (* (/ x) (/ y))))))))
(defthm distributivity-of-/-over-*
(equal (/ (* x y))
(* (/ x) (/ y)))
:hints (("Goal"
:use distributivity-of-/-over-*-lemma)))
)
(encapsulate
()
(local
(defthm uniqueness-of-+-inverses-lemma
(implies (and (acl2-numberp x)
(acl2-numberp y)
(equal (+ x y)
0))
(equal (- x) y))
:rule-classes nil))
(defthm functional-commutativity-of-minus-*-right
(implies (syntaxp (not (quotep y)))
(equal (* x (- y))
(- (* x y))))
:hints (("Goal"
:use ((:instance
Uniqueness-of-+-inverses-lemma
(x (* x y))
(y (* x (- y))))
(:instance
distributivity
(z (- y)))))))
)
(encapsulate
()
(local
(defthm equal-/-/-lemma
(implies
(and (acl2-numberp a)
(acl2-numberp b)
(not (equal a 0))
(not (equal b 0)))
(equal (equal (/ a) (/ b))
(equal a b)))
:rule-classes nil
:hints
(("Goal"
:use ((:instance
(:theorem
(implies
(and (acl2-numberp a)
(acl2-numberp b)
(not (equal a 0))
(not (equal b 0)))
(implies (equal a b)
(equal (/ a) (/ b)))))
(a (/ a)) (b (/ b))))))))
(defthm equal-/-/
(equal (equal (/ a) (/ b))
(equal (fix a) (fix b)))
:hints (("Goal" :use equal-/-/-lemma)))
)
|
