← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/cowles-gamboa-euclid/Euclid/ed4ab.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/workshops/2006/cowles-gamboa-euclid/Euclid/ed4ab.lisp
 
1
; ACL2 Euclidean Domain books -- Book 4ab -- Example: Integers.
 
2
;  The Integers are shown to be an Euclidean Domain with
 
3
;  unique factorization. Here Size is abs; Quotient is floor
 
4
;  and Remainder is mod.
 
5
 
 
6
;  This version uses computable Skolem functions [in place of
 
7
;  quantifiers (defun-sk)] and is executable. The name of
 
8
;  each computable Skolem function, contains a $ symbol.
 
9
 
 
10
; Copyright (C) 2005  John R. Cowles, University of Wyoming
 
11
 
 
12
; This book is free software; you can redistribute it and/or modify
 
13
; it under the terms of the GNU General Public License as published by
 
14
; the Free Software Foundation; either version 2 of the License, or
 
15
; (at your option) any later version.
 
16
 
 
17
; This book is distributed in the hope that it will be useful,
 
18
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
19
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
20
; GNU General Public License for more details.
 
21
 
 
22
; You should have received a copy of the GNU General Public License
 
23
; along with this book; if not, write to the Free Software
 
24
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
25
 
 
26
; Written by:
 
27
; John Cowles
 
28
; Department of Computer Science
 
29
; University of Wyoming
 
30
; Laramie, WY 82071-3682 U.S.A.
 
31
 
 
32
; Last modified Feb. 06.
 
33
 
 
34
#| 
 
35
To certify this book, first, create a world with the following package:
 
36
 
 
37
(defpkg "INT-MOD"
 
38
  (set-difference-eq
 
39
   (union-eq *acl2-exports*
 
40
             *common-lisp-symbols-from-main-lisp-package*)
 
41
; Subtracted 12/4/2012 by Matt K. for addition to *acl2-exports*
 
42
   '(nat-listp acl2-number-listp)))
 
43
 
 
44
(certify-book "ed4ab" 
 
45
              1)
 
46
|#
 
47
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
48
;; The Integers are an Euclidean Doamin:
 
49
 
 
50
;;  integerp  ; Predicate for set of Euclidean Domain elements. 
 
51
;;  equal     ; Equality predicate for Euclidean Domain elements.
 
52
;;  identity  ; Choose unique equivalence class representative for equal. 
 
53
;;  +         ; Addition in Euclidean Domain.
 
54
;;  *         ; Multiplication in Euclidean Domain. 
 
55
;;  -         ; Unary minus in Euclidean Domain.
 
56
;;  0         ; 0 element in Euclidean Domain.
 
57
;;  1         ; 1 element in Euclidean Domain.
 
58
;;  abs       ; Natp size of each nonzero Euclidean Domain element. 
 
59
;;  floor     ; Quotient in Euclidean Domain.
 
60
;;  mod       ; Remainder in Euclidean Domain.
 
61
 
 
62
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
63
;; An Euclidean Domain is an integral domain, together with a Size function
 
64
;; from nonzero domain elements into the nonnegative integers, that
 
65
;; satisfies the Division Propery:
 
66
;; 
 
67
;; Division Propery. For all domain elements x and all nonzero domain
 
68
;;             elements y there are domain elements q and r such that
 
69
 
 
70
;;        x = yq + r and either r is the domain's zero or Size(r) < Size(y)
 
71
 
 
72
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
73
;; An Integral Domain is a commutative ring with no zero-divisors.
 
74
 
 
75
;; A Zero-Divisor in a commutative ring is a nonzero ring element, x, such
 
76
;; that there is a nonzero ring element y such that the product xy equals
 
77
;; the zero element of the ring.
 
78
 
 
79
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
80
;; A Commutative Ring is a nonempty set with two binary operations, addition
 
81
;; and multiplication, an unary operation, minus, and a ring element, zero,
 
82
;; such that 
 
83
 
 
84
;; (1) the binary operations are commutative and associative,
 
85
;; (2) multiplication distributes over addition,
 
86
;; (3) zero is an identity for addition, and
 
87
;; (4) minus produces an additive inverse
 
88
 
 
89
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
90
;; Every Euclidean Domain has a multiplicative identity.
 
91
;;   See Book 1 of ACL2 Euclidean Domain books, ed1.lisp, for a proof.
 
92
 
 
93
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
94
;; There is no loss of generality in assuming the
 
95
;;   Multiplicative Size Property:
 
96
 
 
97
;;     For all nonzero domain elements x and y, Size(x) <= Size(xy).
 
98
 
 
99
;;     If the original Size function does not satisfy this property,
 
100
;;     then it can replaced by another that does satisfy this and the
 
101
;;     division property.
 
102
;;      See Book 2 of the ACL2 Euclidean Domain books, ed2.lisp, 
 
103
;;      for a proof.
 
104
 
 
105
;;  In fact, for integers x and y, (abs (* x y)) = (* (abs x)(abs y)).
 
106
;;   So, if integer y differs from 0, then (<= 1 (abs y)); then for
 
107
;;   any integer x, (abs x) =  (* (abs x) 1) <= (* (abs x)(abs y))
 
108
;;                                            = (abs (* x y)).
 
109
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
110
(in-package "INT-MOD")
 
111
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
112
; Make temporary use of an ACL2 Arithmetic Book and a book containing facts
 
113
;  about FLOOR and MOD to help certify this book
 
114
 
 
115
(local
 
116
 (include-book "arithmetic/top" :dir :system 
 
117
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
118
; support provisional certification:
 
119
;              :uncertified-okp nil     
 
120
               :defaxioms-okp nil 
 
121
               :skip-proofs-okp nil))
 
122
 
 
123
(local
 
124
 (include-book "ihs/quotient-remainder-lemmas" :dir :system 
 
125
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
126
; support provisional certification:
 
127
;              :uncertified-okp nil     
 
128
               :defaxioms-okp nil 
 
129
               :skip-proofs-okp nil))
 
130
 
 
131
(local
 
132
 (in-theory (disable acl2::quotient-remainder-functions)))
 
133
 
 
134
;; Make temporary use of an ACL2 Euclidean Domain Book:
 
135
(local
 
136
 (include-book "ed3"
 
137
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
138
; support provisional certification:
 
139
;              :uncertified-okp nil     
 
140
               :defaxioms-okp nil 
 
141
               :skip-proofs-okp nil))
 
142
 
 
143
;; AXIOMS
 
144
;;; Integral Domain Axioms:
 
145
(defthm
 
146
  Closure-Laws
 
147
  (and (implies (integerp x)
 
148
                (and (implies (integerp y)
 
149
                              (and (integerp (+ x y))
 
150
                                   (integerp (* x y))))
 
151
                     (integerp (- x))))
 
152
       (integerp 0)
 
153
       (integerp 1))
 
154
  :rule-classes nil)
 
155
 
 
156
(defthm
 
157
  Equivalence-Law
 
158
  (implies (integerp x)
 
159
           (and (equal x x)  
 
160
                (implies (integerp y)
 
161
                         (and (booleanp (equal x y))
 
162
                              (implies (equal x y) 
 
163
                                       (equal y x))
 
164
                              (implies (integerp z)
 
165
                                       (implies (and (equal x y)
 
166
                                                     (equal y z))
 
167
                                                (equal x z)))))))
 
168
  :rule-classes nil)
 
169
 
 
170
(defthm
 
171
  Congruence-Laws
 
172
  (implies (equal y1 y2)
 
173
           (and (iff (integerp y1)
 
174
                     (integerp y2))
 
175
                (implies (and (integerp y1)
 
176
                              (integerp y2))
 
177
                         (and (implies (integerp x)
 
178
                                       (and (equal (+ x y1)
 
179
                                                   (+ x y2))
 
180
                                            (equal (* x y1)
 
181
                                                   (* x y2))))
 
182
                              (implies (integerp z)
 
183
                                       (and (equal (+ y1 z)
 
184
                                                   (+ y2 z))
 
185
                                            (equal (* y1 z)
 
186
                                                   (* y2 z))))
 
187
                              (equal (- y1)
 
188
                                     (- y2))))))
 
189
  :rule-classes nil)
 
190
 
 
191
(defthm
 
192
  Closure-of-identity
 
193
  (implies (integerp x)
 
194
           (integerp (identity x)))
 
195
  :rule-classes nil)
 
196
 
 
197
(defthm
 
198
  Equivalence-class-Laws
 
199
  (and (implies (integerp x)
 
200
                (equal (identity x) x))
 
201
       (implies (and (integerp y1)
 
202
                     (integerp y2)
 
203
                     (equal y1 y2))
 
204
                (equal (identity y1)
 
205
                       (identity y2))))
 
206
  :rule-classes nil)
 
207
 
 
208
(defthm
 
209
  Commutativity-Laws
 
210
  (implies (and (integerp x)
 
211
                (integerp y))
 
212
           (and (equal (+ x y)
 
213
                       (+ y x))
 
214
                (equal (* x y)
 
215
                       (* y x))))
 
216
  :rule-classes nil)
 
217
 
 
218
(defthm
 
219
  Associativity-Laws
 
220
  (implies (and (integerp x)
 
221
                (integerp y)
 
222
                (integerp z))
 
223
           (and (equal (+ (+ x y) z)
 
224
                       (+ x (+ y z)))
 
225
                (equal (* (* x y) z)
 
226
                       (* x (* y z)))))
 
227
  :rule-classes nil)
 
228
 
 
229
(defthm
 
230
  Left-Distributivity-Law
 
231
  (implies (and (integerp x)
 
232
                (integerp y)
 
233
                (integerp z))
 
234
           (equal (* x (+ y z))
 
235
                  (+ (* x y)
 
236
                       (* x z))))
 
237
  :rule-classes nil)
 
238
 
 
239
(defthm
 
240
  Left-Unicity-Laws
 
241
  (implies (integerp x)
 
242
           (and (equal (+ 0 x)
 
243
                       x)
 
244
                (equal (* 1 x)
 
245
                       x)))
 
246
  :rule-classes nil)
 
247
 
 
248
(defthm
 
249
  Right-Inverse-Law
 
250
  (implies (integerp x)
 
251
           (equal (+ x (- x))
 
252
                  0))
 
253
  :rule-classes nil)
 
254
 
 
255
(defthm
 
256
  Zero-Divisor-Law
 
257
  (implies (and (integerp x)
 
258
                (integerp y))
 
259
           (equal (equal (* x y) 0)
 
260
                  (or (equal x 0)
 
261
                      (equal y 0))))
 
262
  :rule-classes nil)
 
263
 
 
264
;; Euclidean Domain Axioms:
 
265
(defthm
 
266
  Natp-abs
 
267
  (implies (and (integerp x)
 
268
                (not (equal x 0)))
 
269
           (and (integerp (abs x))
 
270
                (>= (abs x) 0)))
 
271
  :rule-classes ((:type-prescription
 
272
                  :corollary
 
273
                  (implies (integerp x)
 
274
                           (and (integerp (abs x))
 
275
                                (>= (abs x) 0))))
 
276
                 (:linear
 
277
                  :corollary
 
278
                  (implies (and (integerp x)
 
279
                                (not (equal x 0)))
 
280
                           (> (abs x) 0)))))
 
281
 
 
282
(defthm
 
283
  Congruence-for-abs
 
284
  (implies (and (integerp y1)
 
285
                (integerp y2)
 
286
                (equal y1 y2))
 
287
           (equal (abs y1)
 
288
                  (abs y2)))
 
289
  :rule-classes nil)
 
290
 
 
291
(defthm
 
292
  Closure-of-floor-&-mod
 
293
  (implies (and (integerp x)
 
294
                (integerp y)
 
295
                (not (equal y 0)))
 
296
           (and (integerp (floor x y))
 
297
                (integerp (mod x y))))
 
298
  :rule-classes nil)
 
299
 
 
300
(defthm
 
301
  Congruence-for-floor-&-mod
 
302
  (implies (and (integerp y1)
 
303
                (integerp y2)
 
304
                (equal y1 y2))
 
305
           (and (implies (and (integerp x)
 
306
                              (not (equal y1 0)))
 
307
                         (and (equal (floor x y1)
 
308
                                     (floor x y2))
 
309
                              (equal (mod x y1)
 
310
                                     (mod x y2))))
 
311
                (implies (and (integerp z)
 
312
                              (not (equal z 0)))
 
313
                         (and (equal (floor y1 z)
 
314
                                     (floor y2 z))
 
315
                              (equal (mod y1 z)
 
316
                                     (mod y2 z))))))
 
317
  :rule-classes nil)
 
318
 
 
319
(defthm
 
320
  Division-property
 
321
  (implies (and (integerp x)
 
322
                (integerp y)
 
323
                (not (equal y 0)))
 
324
           (and (equal x (+ (* y (floor x y))
 
325
                            (mod x y)))
 
326
                (or (equal (mod x y) 0)
 
327
                    (< (abs (mod x y))
 
328
                       (abs y)))))
 
329
  :rule-classes ((:rewrite
 
330
                  :corollary
 
331
                  (implies (and (integerp x)
 
332
                                (integerp y)
 
333
                                (not (equal y 0))
 
334
                                (not (equal (mod x y) 0)))
 
335
                           (< (abs (mod x y))
 
336
                              (abs y))))
 
337
                 (:linear
 
338
                  :corollary
 
339
                  (implies (and (integerp x)
 
340
                                (integerp y)
 
341
                                (not (equal y 0))
 
342
                                (not (equal (mod x y)0)))
 
343
                           (< (abs (mod x y))
 
344
                              (abs y))))))
 
345
 
 
346
(defthm
 
347
  Abs-*
 
348
  (implies (and (integerp x)
 
349
                (not (equal x 0))
 
350
                (integerp y)
 
351
                (not (equal y 0)))
 
352
           (<= (abs x) 
 
353
               (abs (* x y))))
 
354
  :rule-classes (:linear 
 
355
                 (:rewrite
 
356
                  :corollary
 
357
                  (and (implies (and (integerp x)
 
358
                                     (integerp y))
 
359
                                (equal (abs (* x y))
 
360
                                       (* (abs x)(abs y))))
 
361
                       (implies (and (integerp x)
 
362
                                     (not (equal x 0))
 
363
                                     (integerp y)
 
364
                                     (not (equal y 0)))
 
365
                                (<= (abs x) 
 
366
                                    (abs (* x y))))))) 
 
367
  :hints (("Goal"
 
368
           :in-theory (disable (:definition abs))
 
369
           :use ((:instance
 
370
                  (:theorem
 
371
                   (implies (and (integerp x)
 
372
                                 (> x 0)
 
373
                                 (integerp y)
 
374
                                 (> y 0))
 
375
                            (<= x (* x y))))
 
376
                  (x (abs x))
 
377
                  (y (abs y)))
 
378
                 (:theorem
 
379
                  (implies (and (integerp x)
 
380
                                (integerp y))
 
381
                           (equal (abs (* x y))
 
382
                                  (* (abs x)(abs y)))))))
 
383
          ("Subgoal 1"
 
384
           :in-theory (enable (:definition abs)))))
 
385
 
 
386
(in-theory (disable (:definition abs)))
 
387
 
 
388
;;;;;;;;;;;;;;;;;;;;
 
389
;; Divides-p theory: 
 
390
 
 
391
;; (defun-sk
 
392
;;   divides-p (x y)
 
393
;;   (exists z (and (integerp x)
 
394
;;                  (integerp z)
 
395
;;                  (equal (* x z)
 
396
;;                         y))))
 
397
 
 
398
;; Computable Skolem function
 
399
(defun
 
400
  Divides-p$-witness (x y)
 
401
  (declare (xargs :guard 
 
402
                  (and (acl2-numberp x)
 
403
                       (acl2-numberp y))))
 
404
  (if (not (= x 0))
 
405
      (let ((q (* y (/ x))))
 
406
           (if (integerp q)
 
407
               q
 
408
               0))
 
409
      0))
 
410
 
 
411
(defun
 
412
  Divides-p (x y)
 
413
  (declare (xargs :guard 
 
414
                  (and (acl2-numberp x)
 
415
                       (acl2-numberp y))))
 
416
  (let ((z (divides-p$-witness x y)))
 
417
       (and (integerp x)
 
418
            (integerp z)
 
419
            (= (* x z) y))))
 
420
 
 
421
(defthm
 
422
  Divides-p-suff
 
423
  (implies (and (integerp x)
 
424
                (integerp z)
 
425
                (equal (* x z) y))
 
426
           (divides-p x y))
 
427
  :rule-classes ((:rewrite
 
428
                  :corollary
 
429
                  (implies (and (equal (* x z) y)
 
430
                                (integerp x)
 
431
                                (integerp z))
 
432
                           (divides-p x y)))))
 
433
 
 
434
(in-theory (disable (:definition divides-p$-witness)))
 
435
 
 
436
;;;;;;;;;;;;;;;;;
 
437
;; Unit-p theory:
 
438
 
 
439
(defun
 
440
  Unit-p (x)
 
441
  (declare (xargs :guard 
 
442
                  (acl2-numberp x)))
 
443
  (divides-p x 1))
 
444
 
 
445
(defthm
 
446
  Abs-unit-p=1
 
447
  (implies (unit-p x)
 
448
           (equal (abs x)
 
449
                  1))
 
450
  :rule-classes nil
 
451
  :hints (("Goal"
 
452
           :use (:instance
 
453
                 (:functional-instance
 
454
                  acl2::Size-unit-p=Size-1_e
 
455
                  (acl2::edp integerp)
 
456
                  (acl2::=_e equal)
 
457
                  (acl2::C_=_e identity)
 
458
                  (acl2::binary-+_e binary-+)
 
459
                  (acl2::binary-*_e binary-*)
 
460
                  (acl2::-_e unary--)
 
461
                  (acl2::0_e (lambda () 0))
 
462
                  (acl2::1_e (lambda () 1))
 
463
                  (acl2::size abs)
 
464
                  (acl2::q_e floor)
 
465
                  (acl2::r_e mod)
 
466
                  (acl2::divides-p divides-p)
 
467
                  (acl2::divides-p-witness divides-p$-witness)
 
468
                  (acl2::unit-p unit-p))
 
469
                 (acl2::x x)))
 
470
          ("Subgoal 2"
 
471
           :by (:instance
 
472
                 Divides-p-suff
 
473
                 (x acl2::x)
 
474
                 (y acl2::y)
 
475
                 (z acl2::z)))))
 
476
 
 
477
(defthm
 
478
  Abs=1-implies-unit-p
 
479
  (implies (and (integerp x)
 
480
                (not (equal x 0))
 
481
                (equal (abs x)
 
482
                       1))
 
483
           (unit-p x))
 
484
  :rule-classes nil
 
485
  :hints (("Goal"
 
486
           :use (:instance
 
487
                 (:functional-instance
 
488
                  acl2::Size=Size-1_e-implies-unit-p
 
489
                  (acl2::edp integerp)
 
490
                  (acl2::=_e equal)
 
491
                  (acl2::C_=_e identity)
 
492
                  (acl2::binary-+_e binary-+)
 
493
                  (acl2::binary-*_e binary-*)
 
494
                  (acl2::-_e unary--)
 
495
                  (acl2::0_e (lambda () 0))
 
496
                  (acl2::1_e (lambda () 1))
 
497
                  (acl2::size abs)
 
498
                  (acl2::q_e floor)
 
499
                  (acl2::r_e mod)
 
500
                  (acl2::divides-p divides-p)
 
501
                  (acl2::divides-p-witness divides-p$-witness)
 
502
                  (acl2::unit-p unit-p))
 
503
                 (acl2::x x)))))
 
504
 
 
505
(defthm
 
506
  Unit-p=_+1_or_-1
 
507
  (equal (unit-p x)
 
508
         (or (equal x 1)
 
509
             (equal x -1)))
 
510
  :hints (("Goal"
 
511
           :in-theory (enable abs)
 
512
           :use (Abs-unit-p=1
 
513
                 Abs=1-implies-unit-p))))
 
514
 
 
515
(defthm
 
516
  Abs-<-abs-*
 
517
  (implies (and (not (unit-p y))
 
518
                (integerp x)
 
519
                (not (equal x 0))
 
520
                (integerp y)
 
521
                (not (equal y 0)))
 
522
           (< (abs x)
 
523
              (abs (* x y))))
 
524
  :rule-classes (:linear 
 
525
                 :rewrite)  
 
526
  :hints (("Goal"
 
527
           :in-theory (e/d ((:definition abs)) 
 
528
                           ((:definition unit-p))))))
 
529
 
 
530
;;;;;;;;;;;;;;;;;;;;;;;;
 
531
;; Reducible-p and
 
532
;; Irreducible-p theory:
 
533
 
 
534
;; (defun-sk
 
535
;;   reducible-p (x)
 
536
;;   (exists (y z)(and (integerp y)
 
537
;;                     (integerp z)
 
538
;;                     (not (unit-p y))
 
539
;;                     (not (unit-p z))
 
540
;;                     (equal (* y z) x))))
 
541
 
 
542
(defun
 
543
  Greatest-factor (x y)
 
544
  "Return the largest z such that z|x and
 
545
   1 < z <= y. If no such z exists return |x|."
 
546
  (declare (xargs :guard 
 
547
                  (and (real/rationalp x)
 
548
                       (integerp y)
 
549
                       (>= y 0))))
 
550
  (cond ((or (zp y)(= y 1))
 
551
         (abs x))
 
552
        ((divides-p y x) y)
 
553
        (t (greatest-factor x (- y 1)))))
 
554
 
 
555
(defthm
 
556
  Natp-greatest-factor
 
557
  (implies (and (integerp x)
 
558
                (integerp y)
 
559
                (>= y 0))
 
560
           (and (integerp (greatest-factor x y))
 
561
                (>= (greatest-factor x y) 0)))
 
562
  :rule-classes :type-prescription)
 
563
 
 
564
(defthm
 
565
  Divides-p-greatest-factor
 
566
  (implies (integerp x)
 
567
           (divides-p (greatest-factor x y) x))
 
568
  :hints (("Goal"
 
569
           :in-theory (enable (:definition abs)
 
570
                              (:definition divides-p$-witness)))))
 
571
 
 
572
(defthm
 
573
  x>1-forward
 
574
  (implies (and (not (equal x 1))
 
575
                (not (zp x)))
 
576
           (> x 1))
 
577
  :rule-classes :forward-chaining)
 
578
 
 
579
(defthm
 
580
  Not-integerp-/-a
 
581
  (implies (and (rationalp y)
 
582
                (> y 1))
 
583
           (not (integerp (/ y))))
 
584
  :hints (("Goal"
 
585
           :use (:theorem
 
586
                 (implies (and (rationalp y)
 
587
                               (> y 1))
 
588
                          (< (/ y) 1))))))
 
589
 
 
590
(defthm
 
591
  Not-integerp-/-b-lemma
 
592
  (implies (and (rationalp y)
 
593
                (> y 1))
 
594
           (> (- (/ y)) -1))
 
595
  :rule-classes nil
 
596
  :hints (("Goal"
 
597
           :use (:instance
 
598
                 (:theorem
 
599
                  (implies (< x y)
 
600
                           (> (- x)(- y))))
 
601
                 (x (/ y))
 
602
                 (y 1)))))
 
603
 
 
604
(defthm
 
605
  Not-integerp-/-b
 
606
  (implies (and (rationalp y)
 
607
                (> y 1))
 
608
           (not (integerp (- (/ y)))))
 
609
  :hints (("Goal"
 
610
           :use Not-integerp-/-b-lemma)))
 
611
 
 
612
(defthm
 
613
  Greatest-factor=1
 
614
  (implies (rationalp y)
 
615
           (equal (equal (greatest-factor x y) 1)
 
616
                  (or (equal x 1)
 
617
                      (equal x -1))))
 
618
  :hints (("Goal"
 
619
           :in-theory (enable (:definition abs)
 
620
                              (:definition divides-p$-witness)))))
 
621
 
 
622
(defthm
 
623
  Greatest-factor->-1
 
624
  (implies (> i 1)
 
625
           (> (greatest-factor i j) 1))
 
626
  :rule-classes :linear
 
627
  :hints (("Goal"
 
628
           :in-theory (enable (:definition abs)))))
 
629
 
 
630
(defthm
 
631
  Greatest-factor->-1-a
 
632
  (implies (< i -1)
 
633
           (> (greatest-factor i j) 1))
 
634
  :rule-classes :linear
 
635
  :hints (("Goal"
 
636
           :in-theory (enable (:definition abs)))))
 
637
 
 
638
(defthm
 
639
  Greatest-factor->=-divisor
 
640
  (implies (and (divides-p z x)
 
641
                (integerp y)
 
642
                (< 1 z)
 
643
                (<= z y))
 
644
           (>= (greatest-factor x y) z))
 
645
  :rule-classes :linear)
 
646
 
 
647
(defthm
 
648
  Greatest-factor-<=-y
 
649
  (implies (and (divides-p z x)
 
650
                (integerp y)
 
651
                (< 1 z)
 
652
                (<= z y))
 
653
           (<= (greatest-factor x y) y))
 
654
  :rule-classes :linear)
 
655
 
 
656
;; Computable Skolem function
 
657
(defun
 
658
  Reducible-p$-witness (x)
 
659
  (declare (xargs :guard (integerp x)))
 
660
  (let ((gf (greatest-factor x (nfix (- (abs x) 1)))))
 
661
       (mv (divides-p$-witness gf x) gf)))
 
662
 
 
663
(defun 
 
664
  Reducible-p (x)
 
665
  (declare (xargs :guard (integerp x)))
 
666
  (mv-let (y z)
 
667
          (reducible-p$-witness x)
 
668
          (and (integerp y)
 
669
               (integerp z)
 
670
               (not (unit-p y))
 
671
               (not (unit-p z))
 
672
               (= (* y z) x))))
 
673
 
 
674
(in-theory (disable (:definition Reducible-p$-witness)))
 
675
 
 
676
(in-theory (enable (:definition divides-p$-witness)))
 
677
 
 
678
(defthm
 
679
  Subgoal-7.4
 
680
  (implies (and (integerp y)
 
681
                (integerp z)
 
682
                (not (equal y -1))
 
683
                (not (equal z -1))
 
684
                (< y 0)
 
685
                (< z 0)
 
686
                (<= 1 (* y z)))
 
687
           (not (equal (divides-p$-witness (greatest-factor (* y z) 
 
688
                                                            (+ -1 (* y z)))
 
689
                                           (* y z))
 
690
                       1)))
 
691
  :rule-classes nil
 
692
  :hints (("Goal"
 
693
           :use ((:instance
 
694
                  Greatest-factor-<=-y
 
695
                  (x (* y z))
 
696
                  (y (+ -1 (* y z)))
 
697
                  (z (- z)))
 
698
                 (:instance
 
699
                  (:theorem
 
700
                   (implies (and (integerp b)
 
701
                                 (not (equal b 0))
 
702
                                 (equal (* a (/ b)) 1))
 
703
                            (equal a b)))
 
704
                  (a (* y z))
 
705
                  (b (greatest-factor (* y z) (+ -1 (* y z)))))
 
706
                 (:instance
 
707
                  (:theorem
 
708
                   (implies (and (integerp a)
 
709
                                 (integerp b)
 
710
                                 (>= a 2)
 
711
                                 (>= b 2))
 
712
                            (>= (* (- a 1) b) 1)))
 
713
                 (a (- y))
 
714
                 (b (- z)))))))
 
715
 
 
716
(defthm
 
717
  Subgoal-7.3-lemma
 
718
  (implies (and (integerp a)
 
719
                (integerp b)
 
720
                (integerp y)
 
721
                (integerp z)
 
722
                (<= y a)
 
723
                (<= z b)
 
724
                (< a 0)
 
725
                (< b 0))
 
726
           (>= (* y z)(* a b)))
 
727
  :rule-classes nil
 
728
  :hints (("Goal"
 
729
           :use ((:theorem
 
730
                  (implies (and (integerp a)
 
731
                                (integerp y)
 
732
                                (integerp z)
 
733
                                (<= y a)
 
734
                                (<= z b)
 
735
                                (< b 0))
 
736
                           (>= (* y z)(* a z))))
 
737
                 (:theorem
 
738
                  (implies (and (integerp a)
 
739
                                (integerp b)
 
740
                                (integerp z)
 
741
                                (<= z b)
 
742
                                (< a 0))
 
743
                           (>= (* a z)(* a b))))))
 
744
          ("Subgoal 3"
 
745
           :in-theory (disable acl2::<-*-left-cancel
 
746
                               acl2::<-*-right-cancel))))
 
747
 
 
748
(defthm
 
749
  Subgoal-7.3-lemma-a
 
750
  (implies (and (integerp y)
 
751
                (integerp z)
 
752
                (<= y -2)
 
753
                (<= z -2))
 
754
           (>= (* y z) 4))
 
755
  :rule-classes nil
 
756
  :hints (("Goal"
 
757
           :use (:instance
 
758
                 subgoal-7.3-lemma
 
759
                 (a -2)
 
760
                 (b -2)))))
 
761
 
 
762
(defthm
 
763
  Subgoal-7.3
 
764
  (implies (and (integerp y)
 
765
                (integerp z)
 
766
                (not (equal y -1))
 
767
                (not (equal z -1))
 
768
                (< y 0)
 
769
                (< z 0))
 
770
           (not (equal (* y z) 1)))
 
771
  :rule-classes nil
 
772
  :hints (("Goal"
 
773
           :use subgoal-7.3-lemma-a)))
 
774
 
 
775
(defthm
 
776
  Subgoal-7.1
 
777
  (implies (and (integerp y)
 
778
                (integerp z)
 
779
                (not (equal y -1))
 
780
                (not (equal z -1))
 
781
                (< y 0)
 
782
                (< z 0)
 
783
                (<= 1 (* y z)))
 
784
           (equal (* (greatest-factor (* y z) (+ -1 (* y z)))
 
785
                     (divides-p$-witness (greatest-factor (* y z) (+ -1 (* y z)))
 
786
                                         (* y z)))
 
787
                  (* y z)))
 
788
  :rule-classes nil
 
789
  :hints (("Subgoal 3"
 
790
           :use (:instance
 
791
                 Greatest-factor->-1
 
792
                 (i (* y z))
 
793
                 (j (+ -1 (* y z)))))
 
794
          ("Subgoal 1"
 
795
           :in-theory (disable divides-p-greatest-factor)
 
796
           :use (:instance
 
797
                 divides-p-greatest-factor
 
798
                 (x (* y z))
 
799
                 (y (+ -1 (* y z)))))))
 
800
 
 
801
(defthm
 
802
  Subgoal-5.3-lemma
 
803
  (implies (and (integerp a)
 
804
                (integerp b)
 
805
                (integerp y)
 
806
                (integerp z)
 
807
                (>= y a)
 
808
                (<= z b)
 
809
                (> a 0)
 
810
                (< b 0))
 
811
           (<= (* y z)(* a b)))
 
812
  :rule-classes nil
 
813
  :hints (("Goal"
 
814
           :use ((:theorem
 
815
                  (implies (and (integerp a)
 
816
                                (integerp y)
 
817
                                (integerp z)
 
818
                                (>= y a)
 
819
                                (<= z b)
 
820
                                (< b 0))
 
821
                           (<= (* y z)(* a z))))
 
822
                 (:theorem
 
823
                  (implies (and (integerp a)
 
824
                                (integerp b)
 
825
                                (integerp z)
 
826
                                (<= z b)
 
827
                                (> a 0))
 
828
                           (<= (* a z)(* a b))))))
 
829
          ("Subgoal 3"
 
830
           :in-theory (disable acl2::<-*-left-cancel
 
831
                               acl2::<-*-right-cancel))))
 
832
 
 
833
(defthm
 
834
  Subgoal-5.3-lemma-a
 
835
  (implies (and (integerp y)
 
836
                (integerp z)
 
837
                (>= y 2)
 
838
                (<= z -2))
 
839
           (<= (* y z) -4))
 
840
  :rule-classes nil
 
841
  :hints (("Goal"
 
842
           :use (:instance
 
843
                 subgoal-5.3-lemma
 
844
                 (a 2)
 
845
                 (b -2)))))
 
846
 
 
847
(defthm
 
848
  Subgoal-5.3
 
849
  (implies (and (integerp y)
 
850
                (integerp z)
 
851
                (not (equal y 1))
 
852
                (not (equal z -1))
 
853
                (>= y 0)
 
854
                (< z 0))
 
855
           (not (equal (* y z) -1)))
 
856
  :rule-classes nil
 
857
  :hints (("Goal"
 
858
           :use subgoal-5.3-lemma-a)))
 
859
 
 
860
(defthm
 
861
  Subgoal-5.2
 
862
  (implies (and (integerp y)
 
863
                (integerp z)
 
864
                (not (equal y 1))
 
865
                (not (equal z -1))
 
866
                (<= 0 y)
 
867
                (< z 0)
 
868
                (<= 1 (- (* y z))))
 
869
           (not (equal (divides-p$-witness (greatest-factor (* y z)
 
870
                                                            (+ -1 (- (* y z))))
 
871
                                           (* y z))
 
872
                       -1)))
 
873
  :rule-classes nil
 
874
  :hints (("Goal"
 
875
           :use ((:instance
 
876
                  Greatest-factor-<=-y
 
877
                  (x (* y z))
 
878
                  (y (+ -1 (- (* y z))))
 
879
                  (z (- z)))
 
880
                 (:instance
 
881
                  (:theorem
 
882
                   (implies (and (integerp b)
 
883
                                 (not (equal b 0))
 
884
                                 (equal (* a (/ b)) -1))
 
885
                            (equal (- a) b)))
 
886
                  (a (* y z))
 
887
                  (b (greatest-factor (* y z) (+ -1 (- (* y z))))))
 
888
                 (:instance
 
889
                  (:theorem
 
890
                   (implies (and (integerp a)
 
891
                                 (integerp b)
 
892
                                 (>= a 2)
 
893
                                 (>= b 2))
 
894
                            (>= (* (- a 1) b) 1)))
 
895
                 (a  y)
 
896
                 (b (- z)))))))
 
897
 
 
898
(defthm
 
899
  Subgoal-5.1
 
900
  (implies (and (integerp y)
 
901
                (integerp z)
 
902
                (not (equal y 1))
 
903
                (not (equal z -1))
 
904
                (<= 0 y)
 
905
                (< z 0)
 
906
                (<= 1 (- (* y z))))
 
907
           (equal (* (greatest-factor (* y z)
 
908
                                      (+ -1 (- (* y z))))
 
909
                     (divides-p$-witness (greatest-factor (* y z)
 
910
                                                          (+ -1 (- (* y z))))
 
911
                                         (* y z)))
 
912
                  (* y z)))
 
913
  :rule-classes nil
 
914
  :hints (("Subgoal 3"
 
915
           :use (:instance
 
916
                 Greatest-factor->-1-a
 
917
                 (i (* y z))
 
918
                 (j (+ -1 (- (* y z))))))
 
919
          ("Subgoal 1"
 
920
           :in-theory (disable divides-p-greatest-factor)
 
921
           :use (:instance
 
922
                 divides-p-greatest-factor
 
923
                 (x (* y z))
 
924
                 (y (+ -1 (- (* y z))))))))
 
925
 
 
926
(defthm
 
927
  Subgoal-1.4
 
928
  (implies (and (integerp y)
 
929
                (integerp z)
 
930
                (not (equal y 1))
 
931
                (not (equal z 1))
 
932
                (<= 0 y)
 
933
                (<= 0 z)
 
934
                (<= 1 (* y z)))
 
935
           (not (equal (divides-p$-witness (greatest-factor (* y z) 
 
936
                                                            (+ -1 (* y z)))
 
937
                                           (* y z))
 
938
                       1)))
 
939
  :rule-classes nil
 
940
  :hints (("Goal"
 
941
           :use ((:instance
 
942
                  Greatest-factor-<=-y
 
943
                  (x (* y z))
 
944
                  (y (+ -1 (* y z))))
 
945
                 (:instance
 
946
                  (:theorem
 
947
                   (implies (and (integerp b)
 
948
                                 (not (equal b 0))
 
949
                                 (equal (* a (/ b)) 1))
 
950
                            (equal a b)))
 
951
                  (a (* y z))
 
952
                  (b (greatest-factor (* y z) (+ -1 (* y z)))))
 
953
                 (:instance
 
954
                  (:theorem
 
955
                   (implies (and (integerp a)
 
956
                                 (integerp b)
 
957
                                 (>= a 2)
 
958
                                 (>= b 2))
 
959
                            (>= (* (- a 1) b) 1)))
 
960
                 (a y)
 
961
                 (b z))))))
 
962
 
 
963
(defthm
 
964
  Subgoal-1.3-lemma
 
965
  (implies (and (integerp a)
 
966
                (integerp b)
 
967
                (integerp y)
 
968
                (integerp z)
 
969
                (>= y a)
 
970
                (>= z b)
 
971
                (> a 0)
 
972
                (> b 0))
 
973
           (>= (* y z)(* a b)))
 
974
  :rule-classes nil
 
975
  :hints (("Goal"
 
976
           :use ((:theorem
 
977
                  (implies (and (integerp a)
 
978
                                (integerp y)
 
979
                                (integerp z)
 
980
                                (>= y a)
 
981
                                (>= z b)
 
982
                                (> b 0))
 
983
                           (>= (* y z)(* a z))))
 
984
                 (:theorem
 
985
                  (implies (and (integerp a)
 
986
                                (integerp b)
 
987
                                (integerp z)
 
988
                                (>= z b)
 
989
                                (> a 0))
 
990
                           (>= (* a z)(* a b))))))
 
991
          ("Subgoal 3"
 
992
           :in-theory (disable acl2::<-*-left-cancel
 
993
                               acl2::<-*-right-cancel))))
 
994
 
 
995
(defthm
 
996
  Subgoal-1.3-lemma-a
 
997
  (implies (and (integerp y)
 
998
                (integerp z)
 
999
                (>= y 2)
 
1000
                (>= z 2))
 
1001
           (>= (* y z) 4))
 
1002
  :rule-classes nil
 
1003
  :hints (("Goal"
 
1004
           :use (:instance
 
1005
                 subgoal-1.3-lemma
 
1006
                 (a 2)
 
1007
                 (b 2)))))
 
1008
 
 
1009
(defthm
 
1010
  Subgoal-1.3
 
1011
  (implies (and (integerp y)
 
1012
                (integerp z)
 
1013
                (not (equal y 1))
 
1014
                (not (equal z 1))
 
1015
                (>= y 0)
 
1016
                (>= z 0))
 
1017
           (not (equal (* y z) 1)))
 
1018
  :rule-classes nil
 
1019
  :hints (("Goal"
 
1020
           :use subgoal-1.3-lemma-a)))
 
1021
 
 
1022
(in-theory (enable (:definition abs)))
 
1023
 
 
1024
(defthm
 
1025
  Subgoal-1.1
 
1026
  (implies (and (integerp y)
 
1027
                (integerp z)
 
1028
                (not (equal y 1))
 
1029
                (not (equal z 1))
 
1030
                (<= 0 y)
 
1031
                (<= 0 z)
 
1032
                (<= 1 (* y z)))
 
1033
           (equal (* (greatest-factor (* y z) (+ -1 (* y z)))
 
1034
                     (divides-p$-witness (greatest-factor (* y z) (+ -1 (* y z)))
 
1035
                                         (* y z)))
 
1036
                  (* y z)))
 
1037
  :rule-classes nil
 
1038
  :hints (("Subgoal 3"
 
1039
           :use (:instance
 
1040
                 Greatest-factor->-1
 
1041
                 (i (* y z))
 
1042
                 (j (+ -1 (* y z)))))
 
1043
          ("Subgoal 1"
 
1044
           :in-theory (disable divides-p-greatest-factor)
 
1045
           :use (:instance
 
1046
                 divides-p-greatest-factor
 
1047
                 (x (* y z))
 
1048
                 (y (+ -1 (* y z)))))))
 
1049
 
 
1050
(in-theory (disable (:definition divides-p$-witness)
 
1051
                    (:definition unit-p)))
 
1052
 
 
1053
(in-theory (enable (:definition reducible-p$-witness)))
 
1054
 
 
1055
(defthm
 
1056
  Reducible-p-suff
 
1057
  (implies (and (integerp y)
 
1058
                (integerp z)
 
1059
                (not (unit-p y))
 
1060
                (not (unit-p z))
 
1061
                (equal (* y z) x))
 
1062
           (reducible-p x))
 
1063
  :rule-classes ((:rewrite
 
1064
                  :corollary
 
1065
                  (implies (and (equal (* y z) x)
 
1066
                                (integerp y)
 
1067
                                (integerp z)
 
1068
                                (not (unit-p y))
 
1069
                                (not (unit-p z)))
 
1070
                           (reducible-p x))))
 
1071
  :hints (("Subgoal 7.4"
 
1072
           :by Subgoal-7.4)
 
1073
          ("Subgoal 7.3"
 
1074
           :by Subgoal-7.3)
 
1075
          ("Subgoal 7.2"
 
1076
           :in-theory (enable (:definition divides-p$-witness)))
 
1077
          ("Subgoal 7.1"
 
1078
           :by Subgoal-7.1)
 
1079
          ("Subgoal 5.4"
 
1080
           :in-theory (enable (:definition divides-p$-witness)))
 
1081
          ("Subgoal 5.3"
 
1082
           :by Subgoal-5.3)
 
1083
          ("Subgoal 5.2"
 
1084
           :by Subgoal-5.2)
 
1085
          ("Subgoal 5.1"
 
1086
           :by Subgoal-5.1)
 
1087
          ("Subgoal 3.4"
 
1088
           :in-theory (enable (:definition divides-p$-witness)))
 
1089
          ("Subgoal 3.3"
 
1090
           :use (:instance
 
1091
                 Subgoal-5.3
 
1092
                 (y z)
 
1093
                 (z y)))
 
1094
          ("Subgoal 3.2"
 
1095
           :use (:instance
 
1096
                 Subgoal-5.2
 
1097
                 (y z)
 
1098
                 (z y)))
 
1099
          ("Subgoal 3.1"
 
1100
           :use (:instance
 
1101
                 Subgoal-5.1
 
1102
                 (y z)
 
1103
                 (z y)))
 
1104
          ("Subgoal 1.4"
 
1105
           :by Subgoal-1.4)
 
1106
          ("Subgoal 1.3"
 
1107
           :by Subgoal-1.3)
 
1108
          ("Subgoal 1.2"
 
1109
           :in-theory (enable (:definition divides-p$-witness)))
 
1110
          ("Subgoal 1.1"
 
1111
           :by Subgoal-1.1)))
 
1112
 
 
1113
(in-theory (disable (:definition abs)
 
1114
                    (:definition reducible-p$-witness)))
 
1115
 
 
1116
(defun
 
1117
  Irreducible-p (x)
 
1118
  (declare (xargs :guard t))
 
1119
  (and (integerp x)
 
1120
       (not (unit-p x))
 
1121
       (not (reducible-p x))))
 
1122
 
 
1123
(defthm
 
1124
  Irreducible-p-implies-prime-property
 
1125
  (implies (and (irreducible-p x)
 
1126
                (integerp y)
 
1127
                (integerp z)
 
1128
                (divides-p x (* y z)))
 
1129
           (or (divides-p x y)
 
1130
               (divides-p x z)))
 
1131
  :rule-classes nil
 
1132
  :hints (("Goal"
 
1133
           :by (:instance
 
1134
                (:functional-instance
 
1135
                 acl2::Irreducible-p-implies-prime-property
 
1136
                 (acl2::edp integerp)
 
1137
                 (acl2::=_e equal)
 
1138
                 (acl2::C_=_e identity)
 
1139
                 (acl2::binary-+_e binary-+)
 
1140
                 (acl2::binary-*_e binary-*)
 
1141
                 (acl2::-_e unary--)
 
1142
                 (acl2::0_e (lambda () 0))
 
1143
                 (acl2::1_e (lambda () 1))
 
1144
                 (acl2::size abs)
 
1145
                 (acl2::q_e floor)
 
1146
                 (acl2::r_e mod)
 
1147
                 (acl2::divides-p divides-p)
 
1148
                 (acl2::divides-p-witness divides-p$-witness)
 
1149
                 (acl2::unit-p unit-p)
 
1150
                 (acl2::reducible-p reducible-p)
 
1151
                 (acl2::reducible-p-witness reducible-p$-witness)
 
1152
                 (acl2::irreducible-p irreducible-p))
 
1153
                (acl2::x x)
 
1154
                (acl2::y y)
 
1155
                (acl2::z z)))
 
1156
          ("Subgoal 3"
 
1157
           :in-theory (disable unit-p=_+1_or_-1
 
1158
                               (:definition reducible-p)
 
1159
                               (:definition divides-p)))
 
1160
          ("Subgoal 2"
 
1161
           :by (:instance
 
1162
                reducible-p-suff
 
1163
                (x acl2::x)
 
1164
                (y acl2::y)
 
1165
                (z acl2::z)))))
 
1166
 
 
1167
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1168
;; Factorization existence theory:
 
1169
 
 
1170
(defun
 
1171
  Irreducible-factors (x)
 
1172
  "Return a list, lst, of irreducible
 
1173
   elements of integerp, so that if x is 
 
1174
   in integerp, x is not 0, and x is not
 
1175
   an unit, then x = product of the
 
1176
   members in lst."
 
1177
  (declare (xargs :guard t
 
1178
                  :measure (if (integerp x)
 
1179
                               (abs x)
 
1180
                               0)
 
1181
                  :hints (("Subgoal 2"
 
1182
                           :in-theory (disable (:definition mv-nth)
 
1183
                                               (:definition unit-p))
 
1184
                           :use (:instance
 
1185
                                 abs-<-abs-*
 
1186
                                 (x (mv-nth 1 (reducible-p$-witness x)))
 
1187
                                 (y (mv-nth 0 (reducible-p$-witness x)))))
 
1188
                          ("Subgoal 1"
 
1189
                           :in-theory (disable (:definition mv-nth)
 
1190
                                               (:definition unit-p))
 
1191
                           :use (:instance
 
1192
                                 abs-<-abs-*
 
1193
                                 (x (mv-nth 0 (reducible-p$-witness x)))
 
1194
                                 (y (mv-nth 1 (reducible-p$-witness x))))))))
 
1195
  (cond ((or (not (integerp x))
 
1196
             (= x 0)
 
1197
             (= (abs x) 1))
 
1198
         nil)
 
1199
        ((reducible-p x)
 
1200
         (mv-let (y z)
 
1201
                 (reducible-p$-witness x)
 
1202
                 (append (irreducible-factors y)
 
1203
                         (irreducible-factors z))))
 
1204
        (t (list x))))
 
1205
 
 
1206
(defun
 
1207
  Integerp-listp (lst)
 
1208
  (declare (xargs :guard t))
 
1209
  (if (consp lst)
 
1210
      (and (integerp (car lst))
 
1211
           (integerp-listp (cdr lst)))
 
1212
      t))
 
1213
 
 
1214
(defun
 
1215
  Irreducible-listp (lst)
 
1216
  (declare (xargs :guard t))
 
1217
  (if (consp lst)
 
1218
      (and (irreducible-p (car lst))
 
1219
           (irreducible-listp (cdr lst)))
 
1220
      t))
 
1221
 
 
1222
(defun
 
1223
  *-lst (lst)
 
1224
  (declare (xargs :guard t))
 
1225
  (if (consp lst)
 
1226
      (if (integerp (car lst))
 
1227
          (* (car lst)(*-lst (cdr lst)))
 
1228
          0)
 
1229
      1))
 
1230
 
 
1231
(defthm
 
1232
  IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
1233
  (and (true-listp (irreducible-factors x))
 
1234
       (integerp-listp  (irreducible-factors x))
 
1235
       (irreducible-listp (irreducible-factors x))
 
1236
       (implies (and (integerp x)
 
1237
                     (not (equal x 0))
 
1238
                     (not (unit-p x)))
 
1239
                (equal (*-lst (irreducible-factors x)) x)))
 
1240
  :rule-classes nil
 
1241
  :hints (("Goal"
 
1242
           :by (:instance
 
1243
                (:functional-instance
 
1244
                 acl2::IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
1245
                 (acl2::edp integerp)
 
1246
                 (acl2::=_e equal)
 
1247
                 (acl2::C_=_e identity)
 
1248
                 (acl2::binary-+_e binary-+)
 
1249
                 (acl2::binary-*_e binary-*)
 
1250
                 (acl2::-_e unary--)
 
1251
                 (acl2::0_e (lambda () 0))
 
1252
                 (acl2::1_e (lambda () 1))
 
1253
                 (acl2::size abs)
 
1254
                 (acl2::q_e floor)
 
1255
                 (acl2::r_e mod)
 
1256
                 (acl2::divides-p divides-p)
 
1257
                 (acl2::divides-p-witness divides-p$-witness)
 
1258
                 (acl2::unit-p unit-p)
 
1259
                 (acl2::reducible-p reducible-p)
 
1260
                 (acl2::reducible-p-witness reducible-p$-witness)
 
1261
                 (acl2::irreducible-p irreducible-p)
 
1262
                 (acl2::irreducible-factors irreducible-factors)
 
1263
                 (acl2::irreducible-listp irreducible-listp)
 
1264
                 (acl2::edp-listp integerp-listp)
 
1265
                 (acl2::*_e-lst *-lst))
 
1266
                (acl2::x x)))
 
1267
          ("Subgoal 3"
 
1268
           :in-theory (disable (:definition irreducible-p)))
 
1269
          ("Subgoal 1"
 
1270
           :in-theory (disable (:definition mv-nth)
 
1271
                               (:definition reducible-p)))))
 
1272
 
 
1273
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1274
;; Unit-associates-p theory:
 
1275
 
 
1276
;; (defun-sk
 
1277
;;   unit-associates-p (x y)
 
1278
;;   (exists u (if (and (integerp x)
 
1279
;;                   (integerp y))
 
1280
;;              (and (unit-p u)
 
1281
;;                   (equal (* u x)
 
1282
;;                          y))
 
1283
;;              (equal x y))))
 
1284
 
 
1285
;; Computable Skolem function
 
1286
(defun
 
1287
  Unit-associates-p$-witness (x y)
 
1288
  (declare (xargs :guard
 
1289
                  (and (acl2-numberp x)
 
1290
                       (acl2-numberp y))))
 
1291
  (if (not (= x 0))
 
1292
      (* y (/ x))
 
1293
      1))
 
1294
 
 
1295
(defun
 
1296
  Unit-associates-p (x y)
 
1297
  (declare (xargs :guard
 
1298
                  (and (acl2-numberp x)
 
1299
                       (acl2-numberp y))))
 
1300
  (let ((u (unit-associates-p$-witness x y)))
 
1301
       (if (and (integerp x) 
 
1302
                (integerp y))
 
1303
           (and (unit-p u)
 
1304
                (= (* u x) y))
 
1305
           (= x y))))
 
1306
 
 
1307
(defthm 
 
1308
  Unit-associates-p-suff
 
1309
  (implies (if (and (integerp x) 
 
1310
                    (integerp y))
 
1311
               (and (unit-p u) 
 
1312
                    (equal (* u x) y))
 
1313
               (equal x y))
 
1314
           (unit-associates-p x y)))
 
1315
 
 
1316
(in-theory (disable (:definition Unit-associates-p$-witness)))
 
1317
 
 
1318
(defthm
 
1319
  Irreducible-p-unit-associates
 
1320
  (implies (and (divides-p x y)
 
1321
                (not (unit-p x))
 
1322
                (irreducible-p y))
 
1323
           (unit-associates-p x y))
 
1324
  :rule-classes nil
 
1325
  :hints (("Goal"
 
1326
           :use (:instance
 
1327
                 (:functional-instance
 
1328
                  acl2::Irreducible-p-unit-associates
 
1329
                  (acl2::edp integerp)
 
1330
                  (acl2::=_e equal)
 
1331
                  (acl2::C_=_e identity)
 
1332
                  (acl2::binary-+_e binary-+)
 
1333
                  (acl2::binary-*_e binary-*)
 
1334
                  (acl2::-_e unary--)
 
1335
                  (acl2::0_e (lambda () 0))
 
1336
                  (acl2::1_e (lambda () 1))
 
1337
                  (acl2::size abs)
 
1338
                  (acl2::q_e floor)
 
1339
                  (acl2::r_e mod)
 
1340
                  (acl2::divides-p divides-p)
 
1341
                  (acl2::divides-p-witness divides-p$-witness)
 
1342
                  (acl2::unit-p unit-p)
 
1343
                  (acl2::reducible-p reducible-p)
 
1344
                  (acl2::reducible-p-witness reducible-p$-witness)
 
1345
                  (acl2::irreducible-p irreducible-p)
 
1346
                  (acl2::unit-associates-p unit-associates-p)
 
1347
                  (acl2::unit-associates-p-witness unit-associates-p$-witness))
 
1348
                 (acl2::x x)
 
1349
                 (acl2::y y)))
 
1350
          ("Subgoal 2"
 
1351
           :use (:instance
 
1352
                 unit-associates-p-suff
 
1353
                 (x acl2::x)
 
1354
                 (y acl2::y)))
 
1355
          ("Subgoal 1"
 
1356
           :in-theory (disable unit-p=_+1_or_-1))))
 
1357
 
 
1358
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1359
;; Unique factorization theory:
 
1360
 
 
1361
(defun
 
1362
  acl2-number-listp (l)
 
1363
  (declare (xargs :guard t))
 
1364
  (if (consp l)
 
1365
      (and (acl2-numberp (car l))
 
1366
           (acl2-number-listp (cdr l)))
 
1367
      t))
 
1368
 
 
1369
(defun
 
1370
  Member-unit-associate (x lst)
 
1371
  "Determine if an unit-associate
 
1372
   of x is a member of lst."
 
1373
  (declare (xargs :guard (and (acl2-numberp x)
 
1374
                              (acl2-number-listp lst))))
 
1375
  (cond ((atom lst)
 
1376
         nil)
 
1377
        ((unit-associates-p x (car lst))
 
1378
         lst)
 
1379
        (t (member-unit-associate x (cdr lst)))))
 
1380
 
 
1381
(defun
 
1382
  Delete-one-unit-associate (x lst)
 
1383
  "Return the result of deleting one occurrence 
 
1384
   of an unit-associate of x from the list lst."
 
1385
  (declare (xargs :guard (and (acl2-numberp x)
 
1386
                              (acl2-number-listp lst))))
 
1387
  (if (consp lst)
 
1388
      (if (unit-associates-p x (car lst))
 
1389
          (cdr lst)
 
1390
          (cons (car lst)(delete-one-unit-associate x (cdr lst))))
 
1391
      lst))
 
1392
 
 
1393
(defun
 
1394
  Bag-equal-unit-associates (lst1 lst2)
 
1395
  "Return T iff lst1 and lst2 have the same
 
1396
   members, up to unit-associates, with the
 
1397
   same multiplicity, up to unit-associates."
 
1398
  (declare (xargs :guard (and (acl2-number-listp lst1)
 
1399
                              (acl2-number-listp lst2))))
 
1400
  (if (consp lst1)
 
1401
      (and (member-unit-associate (car lst1) lst2)
 
1402
           (bag-equal-unit-associates (cdr lst1)
 
1403
                                      (delete-one-unit-associate (car lst1) 
 
1404
                                                                 lst2)))
 
1405
      (atom lst2)))
 
1406
 
 
1407
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1408
;; Show that bag-equal-unit-associates has the expected properties:
 
1409
 
 
1410
;;  Lisp objects that are bag-equal-unit-associates have the same length.
 
1411
 
 
1412
;;  Lisp objects that are bag-equal-unit-associates have the same members.
 
1413
;;       up to unit-associates.
 
1414
 
 
1415
;;  Elements in Lisp objects that are bag-equal-unit-associates occur
 
1416
;;  in each object with the same multiplicity up to unit-associates.
 
1417
 
 
1418
(defthm
 
1419
  Bag-equal-unit-associates->equal-len
 
1420
  (implies (bag-equal-unit-associates lst1 lst2)
 
1421
           (equal (len lst1)
 
1422
                  (len lst2)))
 
1423
  :rule-classes nil
 
1424
  :hints (("Goal"
 
1425
           :by (:instance
 
1426
                (:functional-instance
 
1427
                 acl2::Bag-equal-unit-associates->equal-len
 
1428
                 (acl2::edp integerp)
 
1429
                 (acl2::=_e equal)
 
1430
                 (acl2::C_=_e identity)
 
1431
                 (acl2::binary-+_e binary-+)
 
1432
                 (acl2::binary-*_e binary-*)
 
1433
                 (acl2::-_e unary--)
 
1434
                 (acl2::0_e (lambda () 0))
 
1435
                 (acl2::1_e (lambda () 1))
 
1436
                 (acl2::size abs)
 
1437
                 (acl2::q_e floor)
 
1438
                 (acl2::r_e mod)
 
1439
                 (acl2::divides-p divides-p)
 
1440
                 (acl2::divides-p-witness divides-p$-witness)
 
1441
                 (acl2::unit-p unit-p)
 
1442
                 (acl2::unit-associates-p unit-associates-p)
 
1443
                 (acl2::unit-associates-p-witness unit-associates-p$-witness)
 
1444
                 (acl2::Member-unit-associate Member-unit-associate)
 
1445
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
1446
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
1447
                (acl2::lst1 lst1)
 
1448
                (acl2::lst2 lst2)))))
 
1449
 
 
1450
(defthm
 
1451
  Bag-equal-unit-associates->iff-member-unit-associate
 
1452
  (implies (bag-equal-unit-associates lst1 lst2)
 
1453
           (iff (member-unit-associate x lst1)
 
1454
                (member-unit-associate x lst2)))
 
1455
  :rule-classes nil
 
1456
  :hints (("Goal"
 
1457
           :by (:instance
 
1458
                (:functional-instance
 
1459
                 acl2::Bag-equal-unit-associates->iff-member-unit-associate
 
1460
                 (acl2::edp integerp)
 
1461
                 (acl2::=_e equal)
 
1462
                 (acl2::C_=_e identity)
 
1463
                 (acl2::binary-+_e binary-+)
 
1464
                 (acl2::binary-*_e binary-*)
 
1465
                 (acl2::-_e unary--)
 
1466
                 (acl2::0_e (lambda () 0))
 
1467
                 (acl2::1_e (lambda () 1))
 
1468
                 (acl2::size abs)
 
1469
                 (acl2::q_e floor)
 
1470
                 (acl2::r_e mod)
 
1471
                 (acl2::divides-p divides-p)
 
1472
                 (acl2::divides-p-witness divides-p$-witness)
 
1473
                 (acl2::unit-p unit-p)
 
1474
                 (acl2::unit-associates-p unit-associates-p)
 
1475
                 (acl2::unit-associates-p-witness unit-associates-p$-witness)
 
1476
                 (acl2::Member-unit-associate Member-unit-associate)
 
1477
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
1478
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
1479
                (acl2::lst1 lst1)
 
1480
                (acl2::lst2 lst2)))))
 
1481
 
 
1482
(defun
 
1483
  Multiplicity-unit-associate (x lst)
 
1484
  (declare (xargs :guard (and (acl2-numberp x)
 
1485
                              (acl2-number-listp lst))))
 
1486
  (if (consp lst)
 
1487
      (if (unit-associates-p x (car lst))
 
1488
          (+ 1 (multiplicity-unit-associate x (cdr lst)))
 
1489
          (multiplicity-unit-associate x (cdr lst)))
 
1490
      0))
 
1491
 
 
1492
(defthm
 
1493
  Bag-equal-unit-associates->equal-multiplicity-unit-associate 
 
1494
  (implies (bag-equal-unit-associates lst1 lst2)
 
1495
           (equal (multiplicity-unit-associate x lst1)
 
1496
                  (multiplicity-unit-associate x lst2)))
 
1497
  :rule-classes nil
 
1498
  :hints (("Goal"
 
1499
           :by (:instance
 
1500
                (:functional-instance
 
1501
                 acl2::Bag-equal-unit-associates->equal-multiplicity-unit-associate
 
1502
                 (acl2::edp integerp)
 
1503
                 (acl2::=_e equal)
 
1504
                 (acl2::C_=_e identity)
 
1505
                 (acl2::binary-+_e binary-+)
 
1506
                 (acl2::binary-*_e binary-*)
 
1507
                 (acl2::-_e unary--)
 
1508
                 (acl2::0_e (lambda () 0))
 
1509
                 (acl2::1_e (lambda () 1))
 
1510
                 (acl2::size abs)
 
1511
                 (acl2::q_e floor)
 
1512
                 (acl2::r_e mod)
 
1513
                 (acl2::divides-p divides-p)
 
1514
                 (acl2::divides-p-witness divides-p$-witness)
 
1515
                 (acl2::unit-p unit-p)
 
1516
                 (acl2::unit-associates-p unit-associates-p)
 
1517
                 (acl2::unit-associates-p-witness unit-associates-p$-witness)
 
1518
                 (acl2::Member-unit-associate Member-unit-associate)
 
1519
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
1520
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates)
 
1521
                 (acl2::Multiplicity-unit-associate Multiplicity-unit-associate))
 
1522
                (acl2::x x)
 
1523
                (acl2::lst1 lst1)
 
1524
                (acl2::lst2 lst2)))))
 
1525
 
 
1526
(defthm
 
1527
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
1528
  (implies (and (irreducible-listp lst1)
 
1529
                (irreducible-listp lst2)
 
1530
                (unit-associates-p (*-lst lst1)
 
1531
                                   (*-lst lst2)))
 
1532
          (bag-equal-unit-associates lst1 lst2))
 
1533
  :rule-classes nil
 
1534
  :hints (("Goal"
 
1535
           :by (:instance
 
1536
                (:functional-instance
 
1537
                 acl2::IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
1538
                 (acl2::edp integerp)
 
1539
                 (acl2::=_e equal)
 
1540
                 (acl2::C_=_e identity)
 
1541
                 (acl2::binary-+_e binary-+)
 
1542
                 (acl2::binary-*_e binary-*)
 
1543
                 (acl2::-_e unary--)
 
1544
                 (acl2::0_e (lambda () 0))
 
1545
                 (acl2::1_e (lambda () 1))
 
1546
                 (acl2::size abs)
 
1547
                 (acl2::q_e floor)
 
1548
                 (acl2::r_e mod)
 
1549
                 (acl2::divides-p divides-p)
 
1550
                 (acl2::divides-p-witness divides-p$-witness)
 
1551
                 (acl2::unit-p unit-p)
 
1552
                 (acl2::reducible-p reducible-p)
 
1553
                 (acl2::reducible-p-witness reducible-p$-witness)
 
1554
                 (acl2::irreducible-p irreducible-p)
 
1555
                 (acl2::irreducible-listp irreducible-listp)
 
1556
                 (acl2::*_e-lst *-lst)
 
1557
                 (acl2::unit-associates-p unit-associates-p)
 
1558
                 (acl2::unit-associates-p-witness unit-associates-p$-witness)
 
1559
                 (acl2::Member-unit-associate Member-unit-associate)
 
1560
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
1561
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
1562
                (acl2::lst1 lst1)
 
1563
                (acl2::lst2 lst2)))))
 
1564
 
 
1565
(defthm
 
1566
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
1567
  (implies (and (irreducible-listp lst1)
 
1568
                (irreducible-listp lst2)
 
1569
                (equal (*-lst lst1)
 
1570
                       (*-lst lst2)))
 
1571
          (bag-equal-unit-associates lst1 lst2))
 
1572
  :rule-classes nil
 
1573
  :hints (("Goal"
 
1574
           :by (:instance
 
1575
                (:functional-instance
 
1576
                 acl2::IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
1577
                 (acl2::edp integerp)
 
1578
                 (acl2::=_e equal)
 
1579
                 (acl2::C_=_e identity)
 
1580
                 (acl2::binary-+_e binary-+)
 
1581
                 (acl2::binary-*_e binary-*)
 
1582
                 (acl2::-_e unary--)
 
1583
                 (acl2::0_e (lambda () 0))
 
1584
                 (acl2::1_e (lambda () 1))
 
1585
                 (acl2::size abs)
 
1586
                 (acl2::q_e floor)
 
1587
                 (acl2::r_e mod)
 
1588
                 (acl2::divides-p divides-p)
 
1589
                 (acl2::divides-p-witness divides-p$-witness)
 
1590
                 (acl2::unit-p unit-p)
 
1591
                 (acl2::reducible-p reducible-p)
 
1592
                 (acl2::reducible-p-witness reducible-p$-witness)
 
1593
                 (acl2::irreducible-p irreducible-p)
 
1594
                 (acl2::irreducible-listp irreducible-listp)
 
1595
                 (acl2::*_e-lst *-lst)
 
1596
                 (acl2::unit-associates-p unit-associates-p)
 
1597
                 (acl2::unit-associates-p-witness unit-associates-p$-witness)
 
1598
                 (acl2::Member-unit-associate Member-unit-associate)
 
1599
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
1600
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
1601
                (acl2::lst1 lst1)
 
1602
                (acl2::lst2 lst2)))))