← 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/ed4aa.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/ed4aa.lisp
 
1
; ACL2 Euclidean Domain books -- Book 4aa -- 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 quantifiers (defun-sk) and is 
 
7
;  non-executable.
 
8
 
 
9
; Copyright (C) 2005  John R. Cowles, University of Wyoming
 
10
 
 
11
; This book is free software; you can redistribute it and/or modify
 
12
; it under the terms of the GNU General Public License as published by
 
13
; the Free Software Foundation; either version 2 of the License, or
 
14
; (at your option) any later version.
 
15
 
 
16
; This book is distributed in the hope that it will be useful,
 
17
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
18
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
19
; GNU General Public License for more details.
 
20
 
 
21
; You should have received a copy of the GNU General Public License
 
22
; along with this book; if not, write to the Free Software
 
23
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
24
 
 
25
; Written by:
 
26
; John Cowles
 
27
; Department of Computer Science
 
28
; University of Wyoming
 
29
; Laramie, WY 82071-3682 U.S.A.
 
30
 
 
31
; Last modified Feb. 06.
 
32
 
 
33
#| 
 
34
To certify this book, first, create a world with the following package:
 
35
 
 
36
(defpkg "INT-MOD"
 
37
  (set-difference-eq
 
38
   (union-eq *acl2-exports*
 
39
             *common-lisp-symbols-from-main-lisp-package*)
 
40
; Subtracted 12/4/2012 by Matt K. for addition to *acl2-exports*
 
41
   '(nat-listp acl2-number-listp)))
 
42
 
 
43
   (certify-book "ed4aa" 
 
44
                 1
 
45
                 nil ;;compile-flg
 
46
                 )
 
47
|#
 
48
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
49
;; The Integers are an Euclidean Doamin:
 
50
 
 
51
;;  integerp  ; Predicate for set of Euclidean Domain elements.
 
52
;;  equal     ; Equality predicate for Euclidean Domain elements.
 
53
;;  identity  ; Choose unique equivalence class representative for equal. 
 
54
;;  +         ; Addition in Euclidean Domain.
 
55
;;  *         ; Multiplication in Euclidean Domain. 
 
56
;;  -         ; Unary minus in Euclidean Domain.
 
57
;;  0         ; 0 element in Euclidean Domain.
 
58
;;  1         ; 1 element in Euclidean Domain.
 
59
;;  abs       ; Natp size of each nonzero Euclidean Domain element. 
 
60
;;  floor     ; Quotient in Euclidean Domain.
 
61
;;  mod       ; Remainder in Euclidean Domain.
 
62
 
 
63
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
64
;; An Euclidean Domain is an integral domain, together with a Size function
 
65
;; from nonzero domain elements into the nonnegative integers, that
 
66
;; satisfies the Division Propery:
 
67
;; 
 
68
;; Division Propery. For all domain elements x and all nonzero domain
 
69
;;             elements y there are domain elements q and r such that
 
70
 
 
71
;;        x = yq + r and either r is the domain's zero or Size(r) < Size(y)
 
72
 
 
73
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
74
;; An Integral Domain is a commutative ring with no zero-divisors.
 
75
 
 
76
;; A Zero-Divisor in a commutative ring is a nonzero ring element, x, such
 
77
;; that there is a nonzero ring element y such that the product xy equals
 
78
;; the zero element of the ring.
 
79
 
 
80
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
81
;; A Commutative Ring is a nonempty set with two binary operations, addition
 
82
;; and multiplication, an unary operation, minus, and a ring element, zero,
 
83
;; such that 
 
84
 
 
85
;; (1) the binary operations are commutative and associative,
 
86
;; (2) multiplication distributes over addition,
 
87
;; (3) zero is an identity for addition, and
 
88
;; (4) minus produces an additive inverse
 
89
 
 
90
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
91
;; Every Euclidean Domain has a multiplicative identity.
 
92
;;   See Book 1 of ACL2 Euclidean Domain books, ed1.lisp, for a proof.
 
93
 
 
94
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
95
;; There is no loss of generality in assuming the
 
96
;;   Multiplicative Size Property:
 
97
 
 
98
;;     For all nonzero domain elements x and y, Size(x) <= Size(xy).
 
99
 
 
100
;;     If the original Size function does not satisfy this property,
 
101
;;     then it can replaced by another that does satisfy this and the
 
102
;;     division property.
 
103
;;      See Book 2 of the ACL2 Euclidean Domain books, ed2.lisp, 
 
104
;;      for a proof.
 
105
 
 
106
;;  In fact, for integers x and y, (abs (* x y)) = (* (abs x)(abs y)).
 
107
;;   So, if integer y differs from 0, then (<= 1 (abs y)); then for
 
108
;;   any integer x, (abs x) =  (* (abs x) 1) <= (* (abs x)(abs y))
 
109
;;                                            = (abs (* x y)).
 
110
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
111
(in-package "INT-MOD")
 
112
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
113
; Make temporary use of an ACL2 Arithmetic Book and a book containing facts
 
114
;  about FLOOR and MOD to help certify this book
 
115
 
 
116
(local
 
117
 (include-book "arithmetic/top" :dir :system 
 
118
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
119
; support provisional certification:
 
120
;              :uncertified-okp nil     
 
121
               :defaxioms-okp nil 
 
122
               :skip-proofs-okp nil))
 
123
 
 
124
(local
 
125
 (include-book "ihs/quotient-remainder-lemmas" :dir :system 
 
126
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
127
; support provisional certification:
 
128
;              :uncertified-okp nil     
 
129
               :defaxioms-okp nil 
 
130
               :skip-proofs-okp nil))
 
131
 
 
132
(local
 
133
 (in-theory (disable acl2::quotient-remainder-functions)))
 
134
 
 
135
;; Make temporary use of an ACL2 Euclidean Domain Book:
 
136
(local
 
137
 (include-book "ed3"
 
138
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
139
; support provisional certification:
 
140
;              :uncertified-okp nil     
 
141
               :defaxioms-okp nil 
 
142
               :skip-proofs-okp nil))
 
143
 
 
144
;; AXIOMS
 
145
;;; Integral Domain Axioms:
 
146
(defthm
 
147
  Closure-Laws
 
148
  (and (implies (integerp x)
 
149
                (and (implies (integerp y)
 
150
                              (and (integerp (+ x y))
 
151
                                   (integerp (* x y))))
 
152
                     (integerp (- x))))
 
153
       (integerp 0)
 
154
       (integerp 1))
 
155
  :rule-classes nil)
 
156
 
 
157
(defthm
 
158
  Equivalence-Law
 
159
  (implies (integerp x)
 
160
           (and (equal x x)  
 
161
                (implies (integerp y)
 
162
                         (and (booleanp (equal x y))
 
163
                              (implies (equal x y) 
 
164
                                       (equal y x))
 
165
                              (implies (integerp z)
 
166
                                       (implies (and (equal x y)
 
167
                                                     (equal y z))
 
168
                                                (equal x z)))))))
 
169
  :rule-classes nil)
 
170
 
 
171
(defthm
 
172
  Congruence-Laws
 
173
  (implies (equal y1 y2)
 
174
           (and (iff (integerp y1)
 
175
                     (integerp y2))
 
176
                (implies (and (integerp y1)
 
177
                              (integerp y2))
 
178
                         (and (implies (integerp x)
 
179
                                       (and (equal (+ x y1)
 
180
                                                   (+ x y2))
 
181
                                            (equal (* x y1)
 
182
                                                   (* x y2))))
 
183
                              (implies (integerp z)
 
184
                                       (and (equal (+ y1 z)
 
185
                                                   (+ y2 z))
 
186
                                            (equal (* y1 z)
 
187
                                                   (* y2 z))))
 
188
                              (equal (- y1)
 
189
                                     (- y2))))))
 
190
  :rule-classes nil)
 
191
 
 
192
(defthm
 
193
  Closure-of-identity
 
194
  (implies (integerp x)
 
195
           (integerp (identity x)))
 
196
  :rule-classes nil)
 
197
 
 
198
(defthm
 
199
  Equivalence-class-Laws
 
200
  (and (implies (integerp x)
 
201
                (equal (identity x) x))
 
202
       (implies (and (integerp y1)
 
203
                     (integerp y2)
 
204
                     (equal y1 y2))
 
205
                (equal (identity y1)
 
206
                       (identity y2))))
 
207
  :rule-classes nil)
 
208
 
 
209
(defthm
 
210
  Commutativity-Laws
 
211
  (implies (and (integerp x)
 
212
                (integerp y))
 
213
           (and (equal (+ x y)
 
214
                       (+ y x))
 
215
                (equal (* x y)
 
216
                       (* y x))))
 
217
  :rule-classes nil)
 
218
 
 
219
(defthm
 
220
  Associativity-Laws
 
221
  (implies (and (integerp x)
 
222
                (integerp y)
 
223
                (integerp z))
 
224
           (and (equal (+ (+ x y) z)
 
225
                       (+ x (+ y z)))
 
226
                (equal (* (* x y) z)
 
227
                       (* x (* y z)))))
 
228
  :rule-classes nil)
 
229
 
 
230
(defthm
 
231
  Left-Distributivity-Law
 
232
  (implies (and (integerp x)
 
233
                (integerp y)
 
234
                (integerp z))
 
235
           (equal (* x (+ y z))
 
236
                  (+ (* x y)
 
237
                       (* x z))))
 
238
  :rule-classes nil)
 
239
 
 
240
(defthm
 
241
  Left-Unicity-Laws
 
242
  (implies (integerp x)
 
243
           (and (equal (+ 0 x)
 
244
                       x)
 
245
                (equal (* 1 x)
 
246
                       x)))
 
247
  :rule-classes nil)
 
248
 
 
249
(defthm
 
250
  Right-Inverse-Law
 
251
  (implies (integerp x)
 
252
           (equal (+ x (- x))
 
253
                  0))
 
254
  :rule-classes nil)
 
255
 
 
256
(defthm
 
257
  Zero-Divisor-Law
 
258
  (implies (and (integerp x)
 
259
                (integerp y))
 
260
           (equal (equal (* x y) 0)
 
261
                  (or (equal x 0)
 
262
                      (equal y 0))))
 
263
  :rule-classes nil)
 
264
 
 
265
;; Euclidean Domain Axioms:
 
266
(defthm
 
267
  Natp-abs
 
268
  (implies (and (integerp x)
 
269
                (not (equal x 0)))
 
270
           (and (integerp (abs x))
 
271
                (>= (abs x) 0)))
 
272
  :rule-classes ((:type-prescription
 
273
                  :corollary
 
274
                  (implies (integerp x)
 
275
                           (and (integerp (abs x))
 
276
                                (>= (abs x) 0))))
 
277
                 (:linear
 
278
                  :corollary
 
279
                  (implies (and (integerp x)
 
280
                                (not (equal x 0)))
 
281
                           (> (abs x) 0)))))
 
282
 
 
283
(defthm
 
284
  Congruence-for-abs
 
285
  (implies (and (integerp y1)
 
286
                (integerp y2)
 
287
                (equal y1 y2))
 
288
           (equal (abs y1)
 
289
                  (abs y2)))
 
290
  :rule-classes nil)
 
291
 
 
292
(defthm
 
293
  Closure-of-floor-&-mod
 
294
  (implies (and (integerp x)
 
295
                (integerp y)
 
296
                (not (equal y 0)))
 
297
           (and (integerp (floor x y))
 
298
                (integerp (mod x y))))
 
299
  :rule-classes nil)
 
300
 
 
301
(defthm
 
302
  Congruence-for-floor-&-mod
 
303
  (implies (and (integerp y1)
 
304
                (integerp y2)
 
305
                (equal y1 y2))
 
306
           (and (implies (and (integerp x)
 
307
                              (not (equal y1 0)))
 
308
                         (and (equal (floor x y1)
 
309
                                     (floor x y2))
 
310
                              (equal (mod x y1)
 
311
                                     (mod x y2))))
 
312
                (implies (and (integerp z)
 
313
                              (not (equal z 0)))
 
314
                         (and (equal (floor y1 z)
 
315
                                     (floor y2 z))
 
316
                              (equal (mod y1 z)
 
317
                                     (mod y2 z))))))
 
318
  :rule-classes nil)
 
319
 
 
320
(defthm
 
321
  Division-property
 
322
  (implies (and (integerp x)
 
323
                (integerp y)
 
324
                (not (equal y 0)))
 
325
           (and (equal x (+ (* y (floor x y))
 
326
                            (mod x y)))
 
327
                (or (equal (mod x y) 0)
 
328
                    (< (abs (mod x y))
 
329
                       (abs y)))))
 
330
  :rule-classes ((:rewrite
 
331
                  :corollary
 
332
                  (implies (and (integerp x)
 
333
                                (integerp y)
 
334
                                (not (equal y 0))
 
335
                                (not (equal (mod x y) 0)))
 
336
                           (< (abs (mod x y))
 
337
                              (abs y))))
 
338
                 (:linear
 
339
                  :corollary
 
340
                  (implies (and (integerp x)
 
341
                                (integerp y)
 
342
                                (not (equal y 0))
 
343
                                (not (equal (mod x y)0)))
 
344
                           (< (abs (mod x y))
 
345
                              (abs y))))))
 
346
 
 
347
(defthm
 
348
  Abs-*
 
349
  (implies (and (integerp x)
 
350
                (not (equal x 0))
 
351
                (integerp y)
 
352
                (not (equal y 0)))
 
353
           (<= (abs x) 
 
354
               (abs (* x y))))
 
355
  :rule-classes (:linear 
 
356
                 (:rewrite
 
357
                  :corollary
 
358
                  (and (implies (and (integerp x)
 
359
                                     (integerp y))
 
360
                                (equal (abs (* x y))
 
361
                                       (* (abs x)(abs y))))
 
362
                       (implies (and (integerp x)
 
363
                                     (not (equal x 0))
 
364
                                     (integerp y)
 
365
                                     (not (equal y 0)))
 
366
                                (<= (abs x) 
 
367
                                    (abs (* x y))))))) 
 
368
  :hints (("Goal"
 
369
           :in-theory (disable (:definition abs))
 
370
           :use ((:instance
 
371
                  (:theorem
 
372
                   (implies (and (integerp x)
 
373
                                 (> x 0)
 
374
                                 (integerp y)
 
375
                                 (> y 0))
 
376
                            (<= x (* x y))))
 
377
                  (x (abs x))
 
378
                  (y (abs y)))
 
379
                 (:theorem
 
380
                  (implies (and (integerp x)
 
381
                                (integerp y))
 
382
                           (equal (abs (* x y))
 
383
                                  (* (abs x)(abs y)))))))
 
384
          ("Subgoal 1"
 
385
           :in-theory (enable (:definition abs)))))
 
386
 
 
387
(in-theory (disable (:definition abs)))
 
388
 
 
389
;;;;;;;;;;;;;;;;;;;;
 
390
;; Divides-p theory: 
 
391
 
 
392
;;  Divides-p is defined using quantifiers (defun-sk) and
 
393
;;   is non-executable
 
394
 
 
395
(defun-sk
 
396
  divides-p (x y)
 
397
  (exists z (and (integerp x)
 
398
                 (integerp z)
 
399
                 (equal (* x z)
 
400
                        y))))
 
401
 
 
402
;;;;;;;;;;;;;;;;;
 
403
;; Unit-p theory:
 
404
 
 
405
(defun
 
406
  unit-p (x)
 
407
  (divides-p x 1))
 
408
 
 
409
(defthm
 
410
  Abs-unit-p=1
 
411
  (implies (unit-p x)
 
412
           (equal (abs x)
 
413
                  1))
 
414
  :rule-classes nil
 
415
  :hints (("Goal"
 
416
           :use (:instance
 
417
                 (:functional-instance
 
418
                  acl2::Size-unit-p=Size-1_e
 
419
                  (acl2::edp integerp)
 
420
                  (acl2::=_e equal)
 
421
                  (acl2::C_=_e identity)
 
422
                  (acl2::binary-+_e binary-+)
 
423
                  (acl2::binary-*_e binary-*)
 
424
                  (acl2::-_e unary--)
 
425
                  (acl2::0_e (lambda () 0))
 
426
                  (acl2::1_e (lambda () 1))
 
427
                  (acl2::size abs)
 
428
                  (acl2::q_e floor)
 
429
                  (acl2::r_e mod)
 
430
                  (acl2::divides-p divides-p)
 
431
                  (acl2::divides-p-witness divides-p-witness)
 
432
                  (acl2::unit-p unit-p))
 
433
                 (acl2::x x)))))
 
434
 
 
435
(defthm
 
436
  Abs=1-implies-unit-p
 
437
  (implies (and (integerp x)
 
438
                (not (equal x 0))
 
439
                (equal (abs x)
 
440
                       1))
 
441
           (unit-p x))
 
442
  :rule-classes nil
 
443
  :hints (("Goal"
 
444
           :use (:instance
 
445
                 (:functional-instance
 
446
                  acl2::Size=Size-1_e-implies-unit-p
 
447
                  (acl2::edp integerp)
 
448
                  (acl2::=_e equal)
 
449
                  (acl2::C_=_e identity)
 
450
                  (acl2::binary-+_e binary-+)
 
451
                  (acl2::binary-*_e binary-*)
 
452
                  (acl2::-_e unary--)
 
453
                  (acl2::0_e (lambda () 0))
 
454
                  (acl2::1_e (lambda () 1))
 
455
                  (acl2::size abs)
 
456
                  (acl2::q_e floor)
 
457
                  (acl2::r_e mod)
 
458
                  (acl2::divides-p divides-p)
 
459
                  (acl2::divides-p-witness divides-p-witness)
 
460
                  (acl2::unit-p unit-p))
 
461
                 (acl2::x x)))))
 
462
 
 
463
(defthm
 
464
  unit-p=_+1_or_-1
 
465
  (equal (unit-p x)
 
466
         (or (equal x 1)
 
467
             (equal x -1)))
 
468
  :hints (("Goal"
 
469
           :in-theory (enable abs)
 
470
           :use (Abs-unit-p=1
 
471
                 Abs=1-implies-unit-p))))
 
472
 
 
473
(defthm
 
474
  Abs-<-abs-*
 
475
  (implies (and (not (unit-p y))
 
476
                (integerp x)
 
477
                (not (equal x 0))
 
478
                (integerp y)
 
479
                (not (equal y 0)))
 
480
           (< (abs x)
 
481
              (abs (* x y))))
 
482
  :rule-classes (:linear 
 
483
                 :rewrite)  
 
484
  :hints (("Goal"
 
485
           :in-theory (e/d ((:definition abs)) 
 
486
                           ((:definition unit-p))))))
 
487
 
 
488
;;;;;;;;;;;;;;;;;;;;;;;;
 
489
;; Reducible-p and
 
490
;; Irreducible-p theory:
 
491
 
 
492
;;  Reducible-p is defined using quantifiers (defun-sk) and
 
493
;;   is non-executable
 
494
 
 
495
(defun-sk
 
496
  reducible-p (x)
 
497
  (exists (y z)(and (integerp y)
 
498
                    (integerp z)
 
499
                    (not (unit-p y))
 
500
                    (not (unit-p z))
 
501
                    (equal (* y z) x))))
 
502
 
 
503
(defun
 
504
  irreducible-p (x)
 
505
  (and (integerp x)
 
506
       (not (unit-p x))
 
507
       (not (reducible-p x))))
 
508
 
 
509
(defthm
 
510
  Irreducible-p-implies-prime-property
 
511
  (implies (and (irreducible-p x)
 
512
                (integerp y)
 
513
                (integerp z)
 
514
                (divides-p x (* y z)))
 
515
           (or (divides-p x y)
 
516
               (divides-p x z)))
 
517
  :rule-classes nil
 
518
  :hints (("Goal"
 
519
           :by (:instance
 
520
                (:functional-instance
 
521
                 acl2::Irreducible-p-implies-prime-property
 
522
                 (acl2::edp integerp)
 
523
                 (acl2::=_e equal)
 
524
                 (acl2::C_=_e identity)
 
525
                 (acl2::binary-+_e binary-+)
 
526
                 (acl2::binary-*_e binary-*)
 
527
                 (acl2::-_e unary--)
 
528
                 (acl2::0_e (lambda () 0))
 
529
                 (acl2::1_e (lambda () 1))
 
530
                 (acl2::size abs)
 
531
                 (acl2::q_e floor)
 
532
                 (acl2::r_e mod)
 
533
                 (acl2::divides-p divides-p)
 
534
                 (acl2::divides-p-witness divides-p-witness)
 
535
                 (acl2::unit-p unit-p)
 
536
                 (acl2::reducible-p reducible-p)
 
537
                 (acl2::reducible-p-witness reducible-p-witness)
 
538
                 (acl2::irreducible-p irreducible-p))
 
539
                (acl2::x x)
 
540
                (acl2::y y)
 
541
                (acl2::z z)))
 
542
          ("Subgoal 3"
 
543
           :in-theory (disable unit-p=_+1_or_-1
 
544
                               (:definition reducible-p)
 
545
                               (:definition divides-p)))
 
546
          ("Subgoal 2"
 
547
           :use (:instance
 
548
                 reducible-p-suff
 
549
                 (x acl2::x)
 
550
                 (y acl2::y)
 
551
                 (z acl2::z)))))
 
552
 
 
553
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
554
;; Factorization existence theory:
 
555
 
 
556
(defun
 
557
  irreducible-factors (x)
 
558
  "Return a list, lst, of irreducible
 
559
   elements of integerp, so that if x is 
 
560
   in integerp, x is not 0, and x is not
 
561
   an unit, then x = product of the
 
562
   members in lst."
 
563
  (declare (xargs :measure (if (integerp x)
 
564
                               (abs x)
 
565
                               0)
 
566
                  :hints (("Subgoal 2"
 
567
                           :in-theory (disable (:definition mv-nth)
 
568
                                               (:definition unit-p))
 
569
                           :use (:instance
 
570
                                 abs-<-abs-*
 
571
                                 (x (mv-nth 1 (reducible-p-witness x)))
 
572
                                 (y (mv-nth 0 (reducible-p-witness x)))))
 
573
                          ("Subgoal 1"
 
574
                           :in-theory (disable (:definition mv-nth)
 
575
                                               (:definition unit-p))
 
576
                           :use (:instance
 
577
                                 abs-<-abs-*
 
578
                                 (x (mv-nth 0 (reducible-p-witness x)))
 
579
                                 (y (mv-nth 1 (reducible-p-witness x))))))))
 
580
  (cond ((or (not (integerp x))
 
581
             (equal x 0)
 
582
             (equal (abs x) 1))
 
583
         nil)
 
584
        ((reducible-p x)
 
585
         (mv-let (y z)
 
586
                 (reducible-p-witness x)
 
587
                 (append (irreducible-factors y)
 
588
                         (irreducible-factors z))))
 
589
        (t (list x))))
 
590
 
 
591
(defun
 
592
  integerp-listp (lst)
 
593
  (if (consp lst)
 
594
      (and (integerp (car lst))
 
595
           (integerp-listp (cdr lst)))
 
596
      t))
 
597
 
 
598
(defun
 
599
  irreducible-listp (lst)
 
600
  (if (consp lst)
 
601
      (and (irreducible-p (car lst))
 
602
           (irreducible-listp (cdr lst)))
 
603
      t))
 
604
 
 
605
(defun
 
606
  *-lst (lst)
 
607
  (if (consp lst)
 
608
      (if (integerp (car lst))
 
609
          (* (car lst)(*-lst (cdr lst)))
 
610
          0)
 
611
      1))
 
612
 
 
613
(defthm
 
614
  IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
615
  (and (true-listp (irreducible-factors x))
 
616
       (integerp-listp  (irreducible-factors x))
 
617
       (irreducible-listp (irreducible-factors x))
 
618
       (implies (and (integerp x)
 
619
                     (not (equal x 0))
 
620
                     (not (unit-p x)))
 
621
                (equal (*-lst (irreducible-factors x)) x)))
 
622
  :rule-classes nil
 
623
  :hints (("Goal"
 
624
           :by (:instance
 
625
                (:functional-instance
 
626
                 acl2::IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
627
                 (acl2::edp integerp)
 
628
                 (acl2::=_e equal)
 
629
                 (acl2::C_=_e identity)
 
630
                 (acl2::binary-+_e binary-+)
 
631
                 (acl2::binary-*_e binary-*)
 
632
                 (acl2::-_e unary--)
 
633
                 (acl2::0_e (lambda () 0))
 
634
                 (acl2::1_e (lambda () 1))
 
635
                 (acl2::size abs)
 
636
                 (acl2::q_e floor)
 
637
                 (acl2::r_e mod)
 
638
                 (acl2::divides-p divides-p)
 
639
                 (acl2::divides-p-witness divides-p-witness)
 
640
                 (acl2::unit-p unit-p)
 
641
                 (acl2::reducible-p reducible-p)
 
642
                 (acl2::reducible-p-witness reducible-p-witness)
 
643
                 (acl2::irreducible-p irreducible-p)
 
644
                 (acl2::irreducible-factors irreducible-factors)
 
645
                 (acl2::irreducible-listp irreducible-listp)
 
646
                 (acl2::edp-listp integerp-listp)
 
647
                 (acl2::*_e-lst *-lst))
 
648
                (acl2::x x)))
 
649
          ("Subgoal 3"
 
650
           :in-theory (disable (:definition irreducible-p)))
 
651
          ("Subgoal 1"
 
652
           :in-theory (disable (:definition mv-nth)
 
653
                               (:definition reducible-p)))))
 
654
 
 
655
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
656
;; Unit-associates-p theory:
 
657
 
 
658
;;  Unit-associates-p is defined using quantifiers (defun-sk) and
 
659
;;   is non-executable
 
660
 
 
661
(defun-sk
 
662
  unit-associates-p (x y)
 
663
  (exists u (if (and (integerp x)
 
664
                     (integerp y))
 
665
                (and (unit-p u)
 
666
                     (equal (* u x)
 
667
                            y))
 
668
                (equal x y))))
 
669
 
 
670
(defthm
 
671
  Irreducible-p-unit-associates
 
672
  (implies (and (divides-p x y)
 
673
                (not (unit-p x))
 
674
                (irreducible-p y))
 
675
           (unit-associates-p x y))
 
676
  :rule-classes nil
 
677
  :hints (("Goal"
 
678
           :use (:instance
 
679
                 (:functional-instance
 
680
                  acl2::Irreducible-p-unit-associates
 
681
                  (acl2::edp integerp)
 
682
                  (acl2::=_e equal)
 
683
                  (acl2::C_=_e identity)
 
684
                  (acl2::binary-+_e binary-+)
 
685
                  (acl2::binary-*_e binary-*)
 
686
                  (acl2::-_e unary--)
 
687
                  (acl2::0_e (lambda () 0))
 
688
                  (acl2::1_e (lambda () 1))
 
689
                  (acl2::size abs)
 
690
                  (acl2::q_e floor)
 
691
                  (acl2::r_e mod)
 
692
                  (acl2::divides-p divides-p)
 
693
                  (acl2::divides-p-witness divides-p-witness)
 
694
                  (acl2::unit-p unit-p)
 
695
                  (acl2::reducible-p reducible-p)
 
696
                  (acl2::reducible-p-witness reducible-p-witness)
 
697
                  (acl2::irreducible-p irreducible-p)
 
698
                  (acl2::unit-associates-p unit-associates-p)             
 
699
                  (acl2::unit-associates-p-witness unit-associates-p-witness))
 
700
                 (acl2::x x)
 
701
                 (acl2::y y)))
 
702
          ("Subgoal 2"
 
703
           :use (:instance
 
704
                 unit-associates-p-suff
 
705
                 (x acl2::x)
 
706
                 (y acl2::y)))
 
707
          ("Subgoal 1"
 
708
           :in-theory (disable unit-p=_+1_or_-1))))
 
709
 
 
710
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
711
;; Unique factorization theory:
 
712
 
 
713
(defun
 
714
  Member-unit-associate (x lst)
 
715
  "Determine if an unit-associate
 
716
   of x is a member of lst."
 
717
  (cond ((atom lst)
 
718
         nil)
 
719
        ((unit-associates-p x (car lst))
 
720
         lst)
 
721
        (t (member-unit-associate x (cdr lst)))))
 
722
 
 
723
(defun
 
724
  Delete-one-unit-associate (x lst)
 
725
  "Return the result of deleting one occurrence 
 
726
   of an unit-associate of x from the list lst."
 
727
  (if (consp lst)
 
728
      (if (unit-associates-p x (car lst))
 
729
          (cdr lst)
 
730
          (cons (car lst)(delete-one-unit-associate x (cdr lst))))
 
731
      lst))
 
732
 
 
733
(defun
 
734
  Bag-equal-unit-associates (lst1 lst2)
 
735
  "Return T iff lst1 and lst2 have the same
 
736
   members, up to unit-associates, with the
 
737
   same multiplicity, up to unit-associates."
 
738
  (if (consp lst1)
 
739
      (and (member-unit-associate (car lst1) lst2)
 
740
           (bag-equal-unit-associates (cdr lst1)
 
741
                                      (delete-one-unit-associate (car lst1) 
 
742
                                                                 lst2)))
 
743
      (atom lst2)))
 
744
 
 
745
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
746
;; Show that bag-equal-unit-associates has the expected properties:
 
747
 
 
748
;;  Lisp objects that are bag-equal-unit-associates have the same length.
 
749
 
 
750
;;  Lisp objects that are bag-equal-unit-associates have the same members
 
751
;;       up to unit-associates.
 
752
 
 
753
;;  Elements in Lisp objects that are bag-equal-unit-associates occur
 
754
;;  in each object with the same multiplicity up to unit-associates.
 
755
 
 
756
(defthm
 
757
  Bag-equal-unit-associates->equal-len
 
758
  (implies (bag-equal-unit-associates lst1 lst2)
 
759
           (equal (len lst1)
 
760
                  (len lst2)))
 
761
  :rule-classes nil
 
762
  :hints (("Goal"
 
763
           :by (:instance
 
764
                (:functional-instance
 
765
                 acl2::Bag-equal-unit-associates->equal-len
 
766
                 (acl2::edp integerp)
 
767
                 (acl2::=_e equal)
 
768
                 (acl2::C_=_e identity)
 
769
                 (acl2::binary-+_e binary-+)
 
770
                 (acl2::binary-*_e binary-*)
 
771
                 (acl2::-_e unary--)
 
772
                 (acl2::0_e (lambda () 0))
 
773
                 (acl2::1_e (lambda () 1))
 
774
                 (acl2::size abs)
 
775
                 (acl2::q_e floor)
 
776
                 (acl2::r_e mod)
 
777
                 (acl2::divides-p divides-p)
 
778
                 (acl2::divides-p-witness divides-p-witness)
 
779
                 (acl2::unit-p unit-p)
 
780
                 (acl2::unit-associates-p unit-associates-p)
 
781
                 (acl2::unit-associates-p-witness unit-associates-p-witness)
 
782
                 (acl2::Member-unit-associate Member-unit-associate)
 
783
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
784
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
785
                (acl2::lst1 lst1)
 
786
                (acl2::lst2 lst2)))))
 
787
 
 
788
(defthm
 
789
  Bag-equal-unit-associates->iff-member-unit-associate
 
790
  (implies (bag-equal-unit-associates lst1 lst2)
 
791
           (iff (member-unit-associate x lst1)
 
792
                (member-unit-associate x lst2)))
 
793
  :rule-classes nil
 
794
  :hints (("Goal"
 
795
           :by (:instance
 
796
                (:functional-instance
 
797
                 acl2::Bag-equal-unit-associates->iff-member-unit-associate
 
798
                 (acl2::edp integerp)
 
799
                 (acl2::=_e equal)
 
800
                 (acl2::C_=_e identity)
 
801
                 (acl2::binary-+_e binary-+)
 
802
                 (acl2::binary-*_e binary-*)
 
803
                 (acl2::-_e unary--)
 
804
                 (acl2::0_e (lambda () 0))
 
805
                 (acl2::1_e (lambda () 1))
 
806
                 (acl2::size abs)
 
807
                 (acl2::q_e floor)
 
808
                 (acl2::r_e mod)
 
809
                 (acl2::divides-p divides-p)
 
810
                 (acl2::divides-p-witness divides-p-witness)
 
811
                 (acl2::unit-p unit-p)
 
812
                 (acl2::unit-associates-p unit-associates-p)
 
813
                 (acl2::unit-associates-p-witness unit-associates-p-witness)
 
814
                 (acl2::Member-unit-associate Member-unit-associate)
 
815
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
816
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
817
                (acl2::lst1 lst1)
 
818
                (acl2::lst2 lst2)))))
 
819
 
 
820
(defun
 
821
  Multiplicity-unit-associate (x lst)
 
822
  (if (consp lst)
 
823
      (if (unit-associates-p x (car lst))
 
824
          (+ 1 (multiplicity-unit-associate x (cdr lst)))
 
825
          (multiplicity-unit-associate x (cdr lst)))
 
826
      0))
 
827
 
 
828
(defthm
 
829
  Bag-equal-unit-associates->equal-multiplicity-unit-associate 
 
830
  (implies (bag-equal-unit-associates lst1 lst2)
 
831
           (equal (multiplicity-unit-associate x lst1)
 
832
                  (multiplicity-unit-associate x lst2)))
 
833
  :rule-classes nil
 
834
  :hints (("Goal"
 
835
           :by (:instance
 
836
                (:functional-instance
 
837
                 acl2::Bag-equal-unit-associates->equal-multiplicity-unit-associate
 
838
                 (acl2::edp integerp)
 
839
                 (acl2::=_e equal)
 
840
                 (acl2::C_=_e identity)
 
841
                 (acl2::binary-+_e binary-+)
 
842
                 (acl2::binary-*_e binary-*)
 
843
                 (acl2::-_e unary--)
 
844
                 (acl2::0_e (lambda () 0))
 
845
                 (acl2::1_e (lambda () 1))
 
846
                 (acl2::size abs)
 
847
                 (acl2::q_e floor)
 
848
                 (acl2::r_e mod)
 
849
                 (acl2::divides-p divides-p)
 
850
                 (acl2::divides-p-witness divides-p-witness)
 
851
                 (acl2::unit-p unit-p)
 
852
                 (acl2::unit-associates-p unit-associates-p)
 
853
                 (acl2::unit-associates-p-witness unit-associates-p-witness)
 
854
                 (acl2::Member-unit-associate Member-unit-associate)
 
855
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
856
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates)
 
857
                 (acl2::Multiplicity-unit-associate Multiplicity-unit-associate))
 
858
                (acl2::x x)
 
859
                (acl2::lst1 lst1)
 
860
                (acl2::lst2 lst2)))))
 
861
 
 
862
(defthm
 
863
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
864
  (implies (and (irreducible-listp lst1)
 
865
                (irreducible-listp lst2)
 
866
                (unit-associates-p (*-lst lst1)
 
867
                                   (*-lst lst2)))
 
868
          (bag-equal-unit-associates lst1 lst2))
 
869
  :rule-classes nil
 
870
  :hints (("Goal"
 
871
           :by (:instance
 
872
                (:functional-instance
 
873
                 acl2::IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
874
                 (acl2::edp integerp)
 
875
                 (acl2::=_e equal)
 
876
                 (acl2::C_=_e identity)
 
877
                 (acl2::binary-+_e binary-+)
 
878
                 (acl2::binary-*_e binary-*)
 
879
                 (acl2::-_e unary--)
 
880
                 (acl2::0_e (lambda () 0))
 
881
                 (acl2::1_e (lambda () 1))
 
882
                 (acl2::size abs)
 
883
                 (acl2::q_e floor)
 
884
                 (acl2::r_e mod)
 
885
                 (acl2::divides-p divides-p)
 
886
                 (acl2::divides-p-witness divides-p-witness)
 
887
                 (acl2::unit-p unit-p)
 
888
                 (acl2::reducible-p reducible-p)
 
889
                 (acl2::reducible-p-witness reducible-p-witness)
 
890
                 (acl2::irreducible-p irreducible-p)
 
891
                 (acl2::irreducible-listp irreducible-listp)
 
892
                 (acl2::*_e-lst *-lst)
 
893
                 (acl2::unit-associates-p unit-associates-p)
 
894
                 (acl2::unit-associates-p-witness unit-associates-p-witness)
 
895
                 (acl2::Member-unit-associate Member-unit-associate)
 
896
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
897
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
898
                (acl2::lst1 lst1)
 
899
                (acl2::lst2 lst2)))))
 
900
 
 
901
(defthm
 
902
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
903
  (implies (and (irreducible-listp lst1)
 
904
                (irreducible-listp lst2)
 
905
                (equal (*-lst lst1)
 
906
                       (*-lst lst2)))
 
907
          (bag-equal-unit-associates lst1 lst2))
 
908
  :rule-classes nil
 
909
  :hints (("Goal"
 
910
           :by (:instance
 
911
                (:functional-instance
 
912
                 acl2::IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
913
                 (acl2::edp integerp)
 
914
                 (acl2::=_e equal)
 
915
                 (acl2::C_=_e identity)
 
916
                 (acl2::binary-+_e binary-+)
 
917
                 (acl2::binary-*_e binary-*)
 
918
                 (acl2::-_e unary--)
 
919
                 (acl2::0_e (lambda () 0))
 
920
                 (acl2::1_e (lambda () 1))
 
921
                 (acl2::size abs)
 
922
                 (acl2::q_e floor)
 
923
                 (acl2::r_e mod)
 
924
                 (acl2::divides-p divides-p)
 
925
                 (acl2::divides-p-witness divides-p-witness)
 
926
                 (acl2::unit-p unit-p)
 
927
                 (acl2::reducible-p reducible-p)
 
928
                 (acl2::reducible-p-witness reducible-p-witness)
 
929
                 (acl2::irreducible-p irreducible-p)
 
930
                 (acl2::irreducible-listp irreducible-listp)
 
931
                 (acl2::*_e-lst *-lst)
 
932
                 (acl2::unit-associates-p unit-associates-p)
 
933
                 (acl2::unit-associates-p-witness unit-associates-p-witness)
 
934
                 (acl2::Member-unit-associate Member-unit-associate)
 
935
                 (acl2::Delete-one-unit-associate Delete-one-unit-associate)
 
936
                 (acl2::Bag-equal-unit-associates Bag-equal-unit-associates))
 
937
                (acl2::lst1 lst1)
 
938
                (acl2::lst2 lst2)))))