← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/ihs/math-lemmas.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/ihs/math-lemmas.lisp
25
25
;; arithmetic libraries to the extent we can.  There are a few lemmas from
26
26
;; the original math-lemmas.lisp.
27
27
 
 
28
; Modified by Jared Davis, October 2014, to port documentation to xdoc.
 
29
 
28
30
(in-package "ACL2")
29
31
 
30
32
(include-book "arithmetic/top" :dir :system)
31
33
(include-book "ihs-init")
32
 
 
33
 
(deflabel math-lemmas
34
 
  :doc ":doc-section ihs
35
 
  A book of theories about +, -, *, /, and EXPT, built on the
36
 
  arithmetic package of Matt Kaufmann.~/
37
 
 
38
 
  This book defines the following theories.
39
 
  ~/~/")
40
 
 
41
 
(defthm cancel-equal-+-*
 
34
(include-book "std/util/defrule" :dir :system)
 
35
 
 
36
(defxdoc math-lemmas
 
37
  :parents (ihs)
 
38
  :short "A book of theories about +, -, *, /, and EXPT, built on the
 
39
  arithmetic package of Matt Kaufmann.")
 
40
 
 
41
(local (xdoc::set-default-parents math-lemmas))
 
42
 
 
43
(defrule cancel-equal-+-*
 
44
  :short "Rewrite: @('(equal (+ x y) x)') and @('(equal (* x y) x)');
 
45
          also commutative forms."
42
46
  (and (equal (equal (+ x y) x)
43
47
              (and (acl2-numberp x) (equal (fix y) 0)))
44
48
       (equal (equal (+ y x) x)
49
53
       (equal (equal (* x y) y)
50
54
              (and (acl2-numberp y)
51
55
                   (or (equal y 0) (equal x 1)))))
52
 
  :hints (("Goal" :in-theory (enable equal-*-x-y-x)))
53
 
  :doc ":doc-section math-lemmas
54
 
   Rewrite: x + y = x EQUAL y = 0;
55
 
            x * y = x EQUAL x = 0 or y = 1;
56
 
            also commutative forms.
57
 
   ~/~/~/")
 
56
  :enable equal-*-x-y-x)
58
57
 
59
 
(defthm normalize-equal-0
 
58
(defrule normalize-equal-0
 
59
  :short "Rewrite @('(equal (- x) 0)'), @('(equal (+ x y) 0)'), and
 
60
@('(equal (* x y) 0)')."
60
61
  (and (equal (equal (- x) 0) (equal (fix x) 0))
61
62
       (equal (equal (+ x y) 0) (equal (fix x) (- y)))
62
 
       (equal (equal (* x y) 0) (or (equal (fix x) 0) (equal (fix y) 0))))
63
 
  :doc ":doc-section math-lemmas
64
 
  Rewrite: -x = 0 EQUAL x = 0;
65
 
           x + y = 0 EQUAL x = -y;
66
 
           x * y = 0 EQUAL x = 0 or y = 0.
67
 
  ~/~/~/")
68
 
 
69
 
(deftheory acl2-numberp-algebra
70
 
  (union-theories
71
 
   (defun-theory
72
 
     '(EQUAL EQL = /= IFF FORCE BINARY-+ BINARY-* UNARY-- UNARY-/
73
 
             ACL2-NUMBERP
74
 
             ;; 1+ 1- ; removed in 1.8
75
 
             ZEROP FIX ZP ZIP))
76
 
   '(eqlablep-recog
77
 
     commutativity-of-+ COMMUTATIVITY-OF-* inverse-of-+
78
 
     associativity-of-+ associativity-of-* commutativity-2-of-+
79
 
     commutativity-2-of-* unicity-of-0 functional-self-inversion-of-minus
80
 
     unicity-of-1 default-*-1 default-*-2
81
 
     default-<-1 default-<-2 default-+-1 default-+-2
82
 
     inverse-of-* functional-self-inversion-of-/ minus-cancellation-on-right
83
 
     minus-cancellation-on-left /-cancellation-on-left
84
 
     /-cancellation-on-right
85
 
     equal-*-x-y-y cancel-equal-+-* normalize-equal-0
86
 
     left-cancellation-for-* left-cancellation-for-+
87
 
     equal-minus-0 zero-is-only-zero-divisor
88
 
     equal-minus-minus equal-/-/ default-unary-minus equal-/ equal-*-/-2
89
 
     functional-commutativity-of-minus-*-left
90
 
     functional-commutativity-of-minus-*-right
91
 
     reciprocal-minus equal-minus-minus distributivity-of-/-over-*
92
 
     distributivity
93
 
     distributivity-of-minus-over-+))
94
 
  :doc ":doc-section math-lemmas
95
 
  A basic theory of algebra for all ACL2-NUMBERPs.
96
 
  ~/
97
 
  
98
 
  This theory includes the following lemmas:
99
 
  ~/
100
 
 
101
 
  The ACL2-NUMBERP-ALGEBRA theory is designed to be a simple, compact basis
 
63
       (equal (equal (* x y) 0) (or (equal (fix x) 0) (equal (fix y) 0)))))
 
64
 
 
65
(defsection acl2-numberp-algebra
 
66
  :short "A basic theory of algebra for all @(see acl2-numberp)s."
 
67
 
 
68
  :long "<p>The ACL2-NUMBERP-ALGEBRA theory is designed to be a simple, compact basis
102
69
  for building other theories.  This theory contains a minimal set of rules
103
70
  for basic algebraic manipulation including associativity and commutativity,
104
71
  simplification, cancellation, and normalization.  It is extended by the
105
72
  theories RATIONALP-ALGEBRA and INTEGERP-ALGEBRA to include selected linear
106
73
  rules and rules for integers respectively.  This theory also contains the
107
74
  DEFUN-THEORY (which see) of all built-in function symbols that would
108
 
  normally occur during reasoning about the ACL2-NUMBERPs.
109
 
 
110
 
  We used keep this theory (and book) separate but roughly equal to the books
111
 
  maintained by Matt K. in order to have a solid, simple, and predictable
112
 
  foundation on which to build the rest of the books in the IHS
113
 
  hierarchy.  However it was decided that this was too much trouble
114
 
  and we just select the rules of Matt K. that we want.~/
115
 
 
116
 
  :cite cancel-equal-+-*")
117
 
 
118
 
(defthm rewrite-linear-equalities-to-iff
119
 
   (equal (equal (< w x) (< y z))
120
 
          (iff (< w x) (< y z)))
121
 
   :doc ":doc-section math-lemmas
122
 
    Rewrite: (EQUAL (< w x) (< y z)) = (IFF (< w x) (< y z)).
123
 
    ~/~/
124
 
 
125
 
   Some proofs of linear equalities don't work when presented as equalities
126
 
   because they need to be proved by linear arithmetic, but linear arithmetic
127
 
   only works at the literal level.  This lemma allows you to state the
128
 
   equality as an equality rewrite rule, but breaks the equality into
129
 
   literals for the proof.")
130
 
 
131
 
(defthm normalize-<-minus-/
 
75
  normally occur during reasoning about the ACL2-NUMBERPs.</p>
 
76
 
 
77
  <p>We used keep this theory (and book) separate but roughly equal to the
 
78
  books maintained by Matt K. in order to have a solid, simple, and predictable
 
79
  foundation on which to build the rest of the books in the IHS hierarchy.
 
80
  However it was decided that this was too much trouble and we just select the
 
81
  rules of Matt K. that we want.</p>"
 
82
 
 
83
  (deftheory acl2-numberp-algebra
 
84
    (union-theories
 
85
     (defun-theory
 
86
       '(EQUAL EQL = /= IFF FORCE BINARY-+ BINARY-* UNARY-- UNARY-/
 
87
               ACL2-NUMBERP
 
88
               ;; 1+ 1- ; removed in 1.8
 
89
               ZEROP FIX ZP ZIP))
 
90
     '(eqlablep-recog
 
91
       commutativity-of-+ COMMUTATIVITY-OF-* inverse-of-+
 
92
       associativity-of-+ associativity-of-* commutativity-2-of-+
 
93
       commutativity-2-of-* unicity-of-0 functional-self-inversion-of-minus
 
94
       unicity-of-1 default-*-1 default-*-2
 
95
       default-<-1 default-<-2 default-+-1 default-+-2
 
96
       inverse-of-* functional-self-inversion-of-/ minus-cancellation-on-right
 
97
       minus-cancellation-on-left /-cancellation-on-left
 
98
       /-cancellation-on-right
 
99
       equal-*-x-y-y cancel-equal-+-* normalize-equal-0
 
100
       left-cancellation-for-* left-cancellation-for-+
 
101
       equal-minus-0 zero-is-only-zero-divisor
 
102
       equal-minus-minus equal-/-/ default-unary-minus equal-/ equal-*-/-2
 
103
       functional-commutativity-of-minus-*-left
 
104
       functional-commutativity-of-minus-*-right
 
105
       reciprocal-minus equal-minus-minus distributivity-of-/-over-*
 
106
       distributivity
 
107
       distributivity-of-minus-over-+))))
 
108
 
 
109
(defrule rewrite-linear-equalities-to-iff
 
110
  :short "Rewrite: @('(EQUAL (< w x) (< y z))') &rarr; @('(IFF (< w x) (< y z))')."
 
111
  :long "<p>Some proofs of linear equalities don't work when presented as
 
112
  equalities because they need to be proved by linear arithmetic, but linear
 
113
  arithmetic only works at the literal level.  This lemma allows you to state
 
114
  the equality as an equality rewrite rule, but breaks the equality into
 
115
  literals for the proof.</p>"
 
116
  (equal (equal (< w x) (< y z))
 
117
         (iff (< w x) (< y z))))
 
118
 
 
119
(defrule normalize-<-minus-/
 
120
  :short "Rewrite inequalities between 0 and negated or reciprocal terms, and
 
121
  @('(< (- x) (- y))')."
132
122
  (and (equal (< (- x) 0)     (< 0 x))
133
123
       (equal (< 0 (- x))     (< x 0))
134
124
 
136
126
 
137
127
       (implies (real/rationalp x)
138
128
                (and (equal (< 0 (/ x)) (< 0 x))
139
 
                     (equal (< (/ x) 0) (< x 0)))))
140
 
  :doc ":doc-section math-lemmas
141
 
  Rewrite: -x < 0 EQUAL 0 < x;
142
 
          -x < -y EQUAL y < x;
143
 
          0 < 1/x EQUAL 0 < x; 
144
 
          1/x < 0 EQUAL x < 0.
145
 
  ~/~/~/")
146
 
 
147
 
(deftheory rationalp-algebra
148
 
  (union-theories
149
 
   (theory 'ACL2-NUMBERP-ALGEBRA)
150
 
   (union-theories
151
 
    (defun-theory '(NUMERATOR DENOMINATOR < ABS PLUSP MINUSP MIN MAX SIGNUM
152
 
                              RFIX))
153
 
    '(equal-*-/-1 *-r-denominator-r
154
 
      default-denominator numerator-minus
155
 
      equal-denominator-1 numerator-when-integerp
156
 
      <-y-*-y-x <-*-y-x-y <-*-/-right <-*-/-right-commuted
157
 
      <-*-/-left <-*-/-left-commuted
158
 
      <-*-left-cancel <-0-minus /-preserves-positive /-preserves-negative
159
 
      rewrite-linear-equalities-to-iff
160
 
      normalize-<-minus-/
161
 
      <-unary-/-negative-left <-unary-/-negative-right
162
 
      <-unary-/-positive-left <-unary-/-positive-right)))
163
 
  :doc ":doc-section math-lemmas
164
 
  A basic theory of algebra for all RATIONALPs.
165
 
  ~/
166
 
 
167
 
  This theory includes the ACL2-NUMBERP-ALGEBRA theory, along with the
168
 
  following lemmas about the rationals:
169
 
  ~/
170
 
 
171
 
  This theory extends ACL2-NUMBERP-ALGEBRA to include theorems about
172
 
  NUMERATOR and DENOMINATOR, and simple cancellationn and normalization
173
 
  theorems and other simple theorems for inequalities.")
174
 
 
175
 
(defthm normalize-<-/-to-*
 
129
                     (equal (< (/ x) 0) (< x 0))))))
 
130
 
 
131
(defsection rationalp-algebra
 
132
  :short "A basic theory of algebra for all @(see rationalp)s."
 
133
  :long "<p>This theory includes the @(see acl2-numberp-algebra) theory along
 
134
with additional lemmas about the rationals.</p>
 
135
 
 
136
<p>This theory extends ACL2-NUMBERP-ALGEBRA to include theorems about NUMERATOR
 
137
and DENOMINATOR, and simple cancellation and normalization theorems and other
 
138
simple theorems for inequalities.</p>"
 
139
 
 
140
  (deftheory rationalp-algebra
 
141
    (union-theories
 
142
     (theory 'ACL2-NUMBERP-ALGEBRA)
 
143
     (union-theories
 
144
      (defun-theory '(NUMERATOR DENOMINATOR < ABS PLUSP MINUSP MIN MAX SIGNUM
 
145
                                RFIX))
 
146
      '(equal-*-/-1 *-r-denominator-r
 
147
                    default-denominator numerator-minus
 
148
                    equal-denominator-1 numerator-when-integerp
 
149
                    <-y-*-y-x <-*-y-x-y <-*-/-right <-*-/-right-commuted
 
150
                    <-*-/-left <-*-/-left-commuted
 
151
                    <-*-left-cancel <-0-minus /-preserves-positive /-preserves-negative
 
152
                    rewrite-linear-equalities-to-iff
 
153
                    normalize-<-minus-/
 
154
                    <-unary-/-negative-left <-unary-/-negative-right
 
155
                    <-unary-/-positive-left <-unary-/-positive-right)))))
 
156
 
 
157
(defrule normalize-<-/-to-*
 
158
  :parents (math-lemmas prefer-*-to-/)
 
159
  :short "Rewrite: Replace @('x < 1/y') with @('x*y < 1') or @('x*y > 1'),
 
160
  based on the sign of y."
176
161
  (implies (and (real/rationalp x)
177
162
                (real/rationalp y)
178
163
                (not (equal y 0)))
179
164
           (and (equal (< x (/ y)) (if (< y 0) (< 1 (* x y)) (< (* x y) 1)))
180
 
                (equal (< (/ y) x) (if (< y 0) (< (* x y) 1) (< 1 (* x y))))))
181
 
  :doc ":doc-section math-lemmas
182
 
  Rewrite: Replace x < 1/y with x*y < 1 or x*y > 1, based on the sign of y.
183
 
  ~/~/~/")
 
165
                (equal (< (/ y) x) (if (< y 0) (< (* x y) 1) (< 1 (* x y)))))))
184
166
 
185
 
(defthm normalize-<-/-to-*-3
 
167
(defrule normalize-<-/-to-*-3
 
168
  :parents (math-lemmas prefer-*-to-/)
 
169
  :short "Rewrite: Replace @('x < y/z') and @('x > y/z') with @('x*z < y') or
 
170
  @('x*z > y'), depending on the sign of z."
186
171
  (implies (and (real/rationalp x)
187
172
                (real/rationalp y)
188
173
                (real/rationalp z)
195
180
                       (if (< z 0) (< (* x z) y) (< y (* x z))))
196
181
                (equal (< (* (/ z) y) x)
197
182
                       (if (< z 0) (< (* x z) y) (< y (* x z))))))
198
 
  :hints
199
 
  (("Goal"
200
 
    ;;  Disable base lemmas and use cancel-<-* instead.
201
 
    :in-theory (disable <-unary-/-negative-left <-unary-/-negative-right
202
 
                        <-unary-/-positive-left <-unary-/-positive-left
203
 
                        <-*-right-cancel)
204
 
    :use (:instance <-*-right-cancel (x (* x z)) (y y) (z (/ z)))))
205
 
  :doc ":doc-section math-lemmas
206
 
  Rewrite: Replace x < y/z and x > y/z with x*z < y or x*z > y, depending on
207
 
  the sign of z.
208
 
  ~/~/~/")
 
183
  ;;  Disable base lemmas and use cancel-<-* instead.
 
184
  :disable (<-unary-/-negative-left <-unary-/-negative-right
 
185
                                    <-unary-/-positive-left <-unary-/-positive-left
 
186
                                    <-*-right-cancel)
 
187
  :use (:instance <-*-right-cancel (x (* x z)) (y y) (z (/ z))))
209
188
 
210
 
(defthm normalize-equal-/-to-*
 
189
(defrule normalize-equal-/-to-*
 
190
  :parents (math-lemmas prefer-*-to-/)
 
191
  :short "Rewrite: Replace @('x = y/z') with @('x*z = y')."
211
192
  (implies (and (acl2-numberp z)
212
193
                (not (equal z 0)))
213
194
           (and (equal (equal x (* y (/ z)))
215
196
                            (equal (* x z) (fix y))))
216
197
                (equal (equal x (* (/ z) y))
217
198
                       (and (acl2-numberp x)
218
 
                            (equal (* x z) (fix y))))))
219
 
  :doc ":doc-section math-lemmas
220
 
  Rewrite: Replace x = y/z with x*z = y.
221
 
  ~/~/~/")
222
 
 
223
 
(deftheory prefer-*-to-/
224
 
  '(normalize-<-/-to-* normalize-<-/-to-*-3 normalize-equal-/-to-*)
225
 
  :doc ":doc-section math-lemmas
226
 
  A small theory of lemmas that eliminate / in favor of *.
227
 
  ~/
228
 
 
229
 
  This is a small theory of rules that eliminate / from equalites and
230
 
  inequalities in favor of *, e.g., x < y/z is rewritten to x*y < z for
231
 
  positive z.  This theory is comaptible with the ALGEBRA theories, i.e., it
232
 
  should not cause looping.  The following lemmas are included:
233
 
  ~/
234
 
 
235
 
  These rules are not included in RATIONALP-ALGEBRA bacause it is not clear
236
 
  that we should prefer x*y < z to x < y/z, or x*y = z to x = y/z. In the
237
 
  case of the lemma NORMALIZE-EQUAL-/-TO-*, there is no reason to suspect
238
 
  that `y' is a better term than `x'; in fact, the whole point of the proofs
239
 
  using these libraries may have to do with a representation involving /.
240
 
  So, unless someone provides a convincing reason to the contrary, these
241
 
  rules will remain separate from the RATIONALP-ALGEBRA theory.
242
 
 
243
 
  Note, however, that in certain cases this theory is just the thing that
244
 
  needs to be ENABLEd to make the proofs work.  Keep it in mind.~/
245
 
 
246
 
  :cite normalize-<-/-to-* 
247
 
  :cite normalize-<-/-to-*-3
248
 
  :cite normalize-equal-/-to-*
249
 
  ")
 
199
                            (equal (* x z) (fix y)))))))
 
200
 
 
201
(defsection prefer-*-to-/
 
202
  :short "A small theory of lemmas that eliminate / in favor of *."
 
203
 
 
204
  :long "<p>This is a small theory of rules that eliminate / from equalites and
 
205
  inequalities in favor of *, e.g., @('x < y/z') is rewritten to @('x*y < z')
 
206
  for positive z.  This theory is compatible with the ALGEBRA theories, i.e.,
 
207
  it should not cause looping.</p>
 
208
 
 
209
  <p>These rules are not included in @(see rationalp-algebra) because it is not
 
210
  clear that we should prefer @('x*y < z') to @('x < y/z'), or @('x*y = z') to
 
211
  @('x = y/z'). In the case of the lemma @(see normalize-equal-/-to-*), there
 
212
  is no reason to suspect that `y' is a better term than `x'; in fact, the
 
213
  whole point of the proofs using these libraries may have to do with a
 
214
  representation involving /.  So, unless someone provides a convincing reason
 
215
  to the contrary, these rules will remain separate from the @(see
 
216
  rationalp-algebra) theory.</p>
 
217
 
 
218
  <p>Note, however, that in certain cases this theory is just the thing that
 
219
  needs to be ENABLEd to make the proofs work.  Keep it in mind.</p>"
 
220
 
 
221
  (deftheory prefer-*-to-/
 
222
    '(normalize-<-/-to-*
 
223
      normalize-<-/-to-*-3
 
224
      normalize-equal-/-to-*)))
250
225
 
251
226
(in-theory (disable prefer-*-to-/))
252
227
 
253
 
(defthm integerp-+-minus-*
254
 
  (and
255
 
   (implies
256
 
    (integerp i)
257
 
    (integerp (- i)))
258
 
 
259
 
   (implies
260
 
    (and (integerp i)
261
 
         (integerp j))
262
 
    (and
263
 
     (integerp (+ i j))
264
 
     (integerp (- i j))
265
 
     (integerp (* i j)))))
266
 
  :doc ":doc-section math-lemmas
267
 
  Rewrite: -i, i + j, i - j, and i * j are integers, when i and j are
268
 
  integers.
269
 
  ~/~/
270
 
 
271
 
  The system has powerful enough type reasoning to `get' these facts
 
228
(defrule integerp-+-minus-*
 
229
  :short "Rewrite: -i, i + j, i - j, and i * j are integers, when i and j are
 
230
  integers."
 
231
  :long "<p>The system has powerful enough type reasoning to `get' these facts
272
232
  automatically most of the time.  There are cases, however, where we need to
273
 
  bring the full power of the rewriter to bear on the problem.  In general
274
 
  one would like to keep lemmas like this to a minimum so as to avoid
275
 
  swamping the rewriter.~/")
276
 
 
277
 
(deftheory integerp-algebra
278
 
  (union-theories
279
 
   (theory 'RATIONALP-ALGEBRA)
280
 
   (union-theories
281
 
    (defun-theory '(INTEGERP INTEGER-ABS))
282
 
    '(integerp-+-minus-* integerp==>denominator=1 <-minus-zero natp-rw posp-rw)))
283
 
  :doc ":doc-section math-lemmas
284
 
  A basic theory of algebra for all INTEGERPs.
285
 
  ~/
286
 
 
287
 
  This theory consists of the ACL2-NUMBERP-ALGEBRA and RATIONALP-ALGEBRA
288
 
  theories, aloing with the follwing lemmas about the integers.
289
 
  ~/
290
 
 
291
 
  This theory extends ACL2-RATIONALP-ALGEBRA to include theorems about
292
 
  NUMERATOR and DENOMINATOR for integers, and other special theorems about
293
 
  integers.")
294
 
 
295
 
(deftheory expt-algebra
296
 
  '((expt) (:type-prescription expt)
297
 
    expt-type-prescription-nonzero
298
 
    expt-type-prescription-positive
299
 
    expt-type-prescription-integerp
300
 
    right-unicity-of-1-for-expt functional-commutativity-of-expt-/-base
301
 
    expt-minus exponents-add exponents-multiply
302
 
    expt->-1 
303
 
    expt-is-increasing-for-base>1 expt-is-decreasing-for-pos-base<1
304
 
    expt-is-weakly-increasing-for-base>1
305
 
    expt-is-weakly-decreasing-for-pos-base<1)
306
 
    :doc ":doc-section math-lemmas
307
 
  A theory of EXPT which is compatible with the ALGEBRA theories.~/
308
 
 
309
 
  This theory contains the following documeted lemmas:
310
 
  ~/
311
 
 
312
 
  This theory contains :TYPE-PRESCRIPTIONS, simpification, normalization and
313
 
  selected :LINEAR rules for EXPT.  This theory will not be useful unless the
314
 
  INTEGERP-ALGEBRA theory, or something similar is ENABLEd.")
315
 
 
316
 
(deftheory ihs-math
317
 
  (union-theories (theory 'integerp-algebra)
318
 
                  (theory 'expt-algebra))
319
 
  :doc ":doc-section math-lemmas
320
 
  The default theory of +, -, *, /, and EXPT for the IHS library.
321
 
  ~/
322
 
 
323
 
  This theory simply consists of the theories INTEGERP-ALGEBRA and
324
 
  EXPT-ALGEBRA. 
325
 
  ~/
326
 
 
327
 
  This theory is the default theory exported by this book.  This theory will
328
 
  normally be ENABLEd by every book in the IHS library.~/
329
 
 
330
 
  :cite integerp-algebra
331
 
  :cite expt-algebra
332
 
  ")
 
233
  bring the full power of the rewriter to bear on the problem.  In general one
 
234
  would like to keep lemmas like this to a minimum so as to avoid swamping the
 
235
  rewriter.</p>"
 
236
  (and (implies (integerp i)
 
237
                (integerp (- i)))
 
238
       (implies (and (integerp i)
 
239
                     (integerp j))
 
240
                (and (integerp (+ i j))
 
241
                     (integerp (- i j))
 
242
                     (integerp (* i j))))))
 
243
 
 
244
(defsection integerp-algebra
 
245
  :parents (math-lemmas ihs-math)
 
246
  :short "A basic theory of algebra for all INTEGERPs."
 
247
  :long "<p>this theory consists of the @(see acl2-numberp-algebra) and @(see
 
248
  rationalp-algebra) theories, along with additional lemmas about the
 
249
  integers.</p>"
 
250
 
 
251
  (deftheory integerp-algebra
 
252
    (union-theories
 
253
     (theory 'RATIONALP-ALGEBRA)
 
254
     (union-theories
 
255
      (defun-theory '(INTEGERP INTEGER-ABS))
 
256
      '(integerp-+-minus-* integerp==>denominator=1 <-minus-zero natp-rw posp-rw)))))
 
257
 
 
258
 
 
259
(defsection expt-algebra
 
260
  :parents (math-lemmas ihs-math)
 
261
  :short "A theory of EXPT which is compatible with the ALGEBRA theories."
 
262
  :long "<p>This theory contains :TYPE-PRESCRIPTIONS, simpification,
 
263
  normalization and selected :LINEAR rules for @(see EXPT.)  This theory will
 
264
  not be useful unless the @(see integerp-algebra) theory, or something similar
 
265
  is ENABLEd.</p>"
 
266
 
 
267
  (deftheory expt-algebra
 
268
    '((expt) (:type-prescription expt)
 
269
      expt-type-prescription-nonzero
 
270
      expt-type-prescription-positive
 
271
      expt-type-prescription-integerp
 
272
      right-unicity-of-1-for-expt functional-commutativity-of-expt-/-base
 
273
      expt-minus exponents-add exponents-multiply
 
274
      expt->-1
 
275
      expt-is-increasing-for-base>1 expt-is-decreasing-for-pos-base<1
 
276
      expt-is-weakly-increasing-for-base>1
 
277
      expt-is-weakly-decreasing-for-pos-base<1)))
 
278
 
 
279
(defsection ihs-math
 
280
  :short "The default theory of +, -, *, /, and EXPT for the IHS library."
 
281
  :long "<p>This theory simply consists of the theories @(see INTEGERP-ALGEBRA)
 
282
and @(see EXPT-ALGEBRA).</p>
 
283
 
 
284
<p>This theory is the default theory exported by the @('ihs/math-lemmas') book.
 
285
This theory will normally be ENABLEd by every book in the IHS library.</p>"
 
286
 
 
287
  (deftheory ihs-math
 
288
    (union-theories (theory 'integerp-algebra)
 
289
                    (theory 'expt-algebra))))
 
290
 
 
291