← 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/ed3.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/ed3.lisp
 
1
; ACL2 Euclidean Domain books -- Book 3 -- Algebraic Theory 
 
2
;  Convenient notation and events for using the theory of an
 
3
;  Euclidean Domain.
 
4
; Copyright (C) 2005  John R. Cowles, University of Wyoming
 
5
 
 
6
; This book is free software; you can redistribute it and/or modify
 
7
; it under the terms of the GNU General Public License as published by
 
8
; the Free Software Foundation; either version 2 of the License, or
 
9
; (at your option) any later version.
 
10
 
 
11
; This book is distributed in the hope that it will be useful,
 
12
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
; GNU General Public License for more details.
 
15
 
 
16
; You should have received a copy of the GNU General Public License
 
17
; along with this book; if not, write to the Free Software
 
18
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
19
 
 
20
; Written by:
 
21
; John Cowles
 
22
; Department of Computer Science
 
23
; University of Wyoming
 
24
; Laramie, WY 82071-3682 U.S.A.
 
25
 
 
26
; Last modified Feb. 2006.
 
27
 
 
28
#|
 
29
To certify this book, first, create a world with the following packages:
 
30
 
 
31
(DEFPKG "ACL2-ASG"
 
32
  (SET-DIFFERENCE-EQUAL
 
33
   (UNION-EQ *ACL2-EXPORTS* 
 
34
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
35
   '(ZERO)))
 
36
 
 
37
(DEFPKG "ACL2-AGP"
 
38
  (SET-DIFFERENCE-EQUAL
 
39
   (UNION-EQ *ACL2-EXPORTS* 
 
40
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
41
   '(ZERO)))
 
42
 
 
43
(DEFPKG "ACL2-CRG"
 
44
  (SET-DIFFERENCE-EQUAL
 
45
   (UNION-EQ *ACL2-EXPORTS* 
 
46
             *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)
 
47
   '(ZERO)))
 
48
 
 
49
(certify-book "ed3"
 
50
              3   
 
51
              nil ;;compile-flg
 
52
              )
 
53
 
 
54
|#
 
55
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
56
;; An Euclidean Domain is an integral domain, together with a Size function
 
57
;; from nonzero domain elements into the nonnegative integers, that
 
58
;; satisfies the Division Propery:
 
59
;; 
 
60
;; Division Propery. For all domain elements x and all nonzero domain
 
61
;;             elements y there are domain elements q and r such that
 
62
 
 
63
;;        x = yq + r and either r is the domain's zero or Size(r) < Size(y)
 
64
 
 
65
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
66
;; An Integral Domain is a commutative ring with no zero-divisors.
 
67
 
 
68
;; A Zero-Divisor in a commutative ring is a nonzero ring element, x, such
 
69
;; that there is a nonzero ring element y such that the product xy equals
 
70
;; the zero element of the ring.
 
71
 
 
72
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
73
;; A Commutative Ring is a nonempty set with two binary operations, addition
 
74
;; and multiplication, an unary operation, minus, and a ring element, zero,
 
75
;; such that 
 
76
 
 
77
;; (1) the binary operations are commutative and associative,
 
78
;; (2) multiplication distributes over addition,
 
79
;; (3) zero is an identity for addition, and
 
80
;; (4) minus produces an additive inverse
 
81
 
 
82
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
83
;; This book assumes the result reported in ed1.lisp which is Book 1 of
 
84
;; ACL2 Euclidean Domain books
 
85
 
 
86
;;                  Multiplicative Identity Existence
 
87
 
 
88
;; That is, every Euclidean Domain has a multiplicative identity.
 
89
 
 
90
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
91
;; This book also assumes the result reported in ed2.lisp which is Book 2
 
92
;; of the ACL2 Euclidean Domain books.
 
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
 
 
103
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
104
;; Brief Contents of This Book
 
105
 
 
106
;;  Axioms and convenient notation for
 
107
;;   the theory of an Euclidean Domain.
 
108
 
 
109
;;  Integral Domain Theory.
 
110
 
 
111
;;  Divides-p Theory. 
 
112
 
 
113
;; ;; (defun-sk
 
114
;; ;;   Divides-p (x y)
 
115
;; ;;   (exists z (and (edp x)
 
116
;; ;;                  (edp z)
 
117
;; ;;                  (=_e (*_e x z)
 
118
;; ;;                       y))))
 
119
 
 
120
;; Associates-p Theory.
 
121
 
 
122
;; ;; (defun
 
123
;; ;;   Associates-p (x y)
 
124
;; ;;   (if (and (edp x)
 
125
;; ;;            (edp y))
 
126
;; ;;       (and (divides-p x y)
 
127
;; ;;            (divides-p y x))
 
128
;; ;;       (equal x y)))
 
129
 
 
130
;; Unit-p Theory.
 
131
 
 
132
;; ;; (defun
 
133
;; ;;   Unit-p (x)
 
134
;; ;;   (divides-p x (1_e)))
 
135
 
 
136
;; Reducible-p and
 
137
;;  Irreducible-p Theory.
 
138
 
 
139
;; ;; (defun-sk
 
140
;; ;;   Reducible-p (x)
 
141
;; ;;   (exists (y z)(and (edp y)
 
142
;; ;;                     (edp z)
 
143
;; ;;                     (not (unit-p y))
 
144
;; ;;                     (not (unit-p z))
 
145
;; ;;                     (=_e (*_e y z) x))))
 
146
 
 
147
;; ;; (defun
 
148
;; ;;   Irreducible-p (x)
 
149
;; ;;   (and (edp x)
 
150
;; ;;        (not (unit-p x))
 
151
;; ;;        (not (reducible-p x))))
 
152
 
 
153
;; Factorization Existence Theory.
 
154
 
 
155
;; ;; (defthm
 
156
;; ;;   IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
157
;; ;;   (and (true-listp (irreducible-factors x))
 
158
;; ;;        (edp-listp  (irreducible-factors x))
 
159
;; ;;        (irreducible-listp (irreducible-factors x))
 
160
;; ;;        (implies (and (edp x)
 
161
;; ;;                      (not (=_e x (0_e)))
 
162
;; ;;                      (not (unit-p x)))
 
163
;; ;;                 (=_e (*_e-lst (irreducible-factors x)) x)))
 
164
;; ;;   :rule-classes nil)
 
165
 
 
166
;; GCD Theory.
 
167
 
 
168
;; ;; Determine if g is a gcd of x and y.
 
169
;; ;; (defun-sk
 
170
;; ;;   gcd-p (x y g)
 
171
;; ;;   (forall d (and (divides-p g x)
 
172
;; ;;                  (divides-p g y)
 
173
;; ;;                  (implies (and (divides-p d x)
 
174
;; ;;                                (divides-p d y))
 
175
;; ;;                           (divides-p d g)))))
 
176
 
 
177
;; Unit-associates-p Theory.
 
178
 
 
179
;; ;; (defun-sk
 
180
;; ;;   unit-associates-p (x y)
 
181
;; ;;   (exists u (if (and (edp x)
 
182
;; ;;                      (edp y))
 
183
;; ;;                 (and (unit-p u)
 
184
;; ;;                      (=_e (*_e u x)
 
185
;; ;;                           y))
 
186
;; ;;                 (equal x y))))
 
187
;; ;; Unit-associates-p is equivalent to Associates-p.
 
188
 
 
189
;; Unique Factorization Theory.
 
190
 
 
191
;; ;; (defthm
 
192
;; ;;   IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
193
;; ;;   (implies (and (irreducible-listp lst1)
 
194
;; ;;                 (irreducible-listp lst2)
 
195
;; ;;                 (unit-associates-p (*_e-lst lst1)
 
196
;; ;;                                    (*_e-lst lst2)))
 
197
;; ;;           (bag-equal-unit-associates lst1 lst2))
 
198
;; ;;   :hints (("Goal"
 
199
;; ;;            ...)))
 
200
 
 
201
;; ;; (defthm
 
202
;; ;;   IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
203
;; ;;   (implies (and (irreducible-listp lst1)
 
204
;; ;;                 (irreducible-listp lst2)
 
205
;; ;;                 (=_e (*_e-lst lst1)
 
206
;; ;;                      (*_e-lst lst2)))
 
207
;; ;;           (bag-equal-unit-associates lst1 lst2))
 
208
;; ;;   :hints (("Goal"
 
209
;; ;;            ...)))
 
210
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
211
(in-package "ACL2")
 
212
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
213
; Make temporary use of an ACL2 Arithmetic Book to help certify this book,
 
214
 
 
215
(local
 
216
 (include-book "arithmetic/top" :dir :system 
 
217
; Matt K.: Commenting out use of :uncertified-okp after v4-3 in order to
 
218
; support provisional certification:
 
219
;              :uncertified-okp nil     
 
220
               :defaxioms-okp nil 
 
221
               :skip-proofs-okp nil))
 
222
 
 
223
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
224
;; Axioms and convenient notation for
 
225
;;  the theory of an Euclidean Domain.
 
226
 
 
227
(encapsulate
 
228
 ; Signatures
 
229
 (((edp *) => *)          ; x is in Euclidean Domain iff (NOT (EQUAL (edp x) NIL)).
 
230
  ((=_e * *) => *)        ; Equality predicate for Euclidean Domain elements.
 
231
  ((C_=_e *) => *)        ; Choose unique equivalence class representative for =_e.
 
232
  ((binary-+_e * *) => *) ; Addition in Euclidean Domain.
 
233
  ((binary-*_e * *) => *) ; Multiplication in Euclidean Domain. 
 
234
  ((-_e *) => *)          ; Unary minus in Euclidean Domain.
 
235
  ((0_e) => *)            ; 0 element in Euclidean Domain.
 
236
  ((1_e) => *)            ; 1 element in Euclidean Domain.
 
237
  ((size *) => *)         ; Natp size of each nonzero Euclidean Domain element. 
 
238
  ((q_e * *) => *)        ; Quotient in Euclidean Domain.
 
239
  ((r_e * *) => *))       ; Remainder in Euclidean Domain.
 
240
 
 
241
 ; Witnesses:
 
242
 (local (defun 
 
243
          edp (x)
 
244
          (rationalp x)))
 
245
 
 
246
 (local (defun
 
247
          =_e (x y)
 
248
          (equal x y)))
 
249
 
 
250
 (local (defun
 
251
          C_=_e (x)
 
252
          (identity x)))
 
253
 
 
254
 (local (defun
 
255
          binary-+_e (x y)
 
256
          (+ x y)))
 
257
 
 
258
 (local (defun
 
259
          binary-*_e (x y)
 
260
          (* x y)))
 
261
 
 
262
 (local (defun
 
263
          -_e (x)
 
264
          (- x)))
 
265
 
 
266
 (local (defun
 
267
          0_e ()
 
268
          0))
 
269
 
 
270
 (local (defun
 
271
          1_e ()
 
272
          1))
 
273
 
 
274
 (local (defun
 
275
          size (x)
 
276
          (declare (ignore x))
 
277
          0))
 
278
 
 
279
 (local (defun
 
280
          q_e (x y)
 
281
          (/ x y)))
 
282
 
 
283
 (local (defun
 
284
          r_e (x y)
 
285
          (declare (ignore x y))
 
286
          0))
 
287
 
 
288
 ; Convenient Notation:
 
289
 (defmacro
 
290
   +_e (&rest rst)
 
291
   (if rst
 
292
       (if (cdr rst)
 
293
           (xxxjoin 'binary-+_e rst)
 
294
           (list 'binary-+_e '(0_e)(car rst)))
 
295
       '(0_e)))
 
296
 
 
297
 (defmacro
 
298
   *_e (&rest rst)
 
299
   (if rst
 
300
       (if (cdr rst)
 
301
           (xxxjoin 'binary-*_e rst)
 
302
           (list 'binary-*_e '(1_e)(car rst)))
 
303
       '(1_e)))
 
304
 
 
305
 ; AXIOMS
 
306
 ; Integral Domain Axioms:
 
307
 (defthm
 
308
   Closure-Laws
 
309
   (and (implies (edp x)
 
310
                 (and (implies (edp y)
 
311
                               (and (edp (+_e x y))
 
312
                                    (edp (*_e x y))))
 
313
                      (edp (-_e x))))
 
314
        (edp (0_e))
 
315
        (edp (1_e))))
 
316
 
 
317
 (defthm
 
318
    Equivalence-Law
 
319
    (implies (edp x)
 
320
             (and (=_e x x)  
 
321
                  (implies (edp y)
 
322
                           (and (booleanp (=_e x y))
 
323
                                (implies (=_e x y) 
 
324
                                         (=_e y x))
 
325
                                (implies (edp z)
 
326
                                         (implies (and (=_e x y)
 
327
                                                       (=_e y z))
 
328
                                                  (=_e x z))))))))
 
329
 
 
330
 (defthm
 
331
   Congruence-Laws
 
332
   (implies (=_e y1 y2)
 
333
            (and (iff (edp y1)
 
334
                      (edp y2))
 
335
                 (implies (and (edp y1)
 
336
                               (edp y2))
 
337
                          (and (implies (edp x)
 
338
                                        (and (=_e (+_e x y1)
 
339
                                                  (+_e x y2))
 
340
                                             (=_e (*_e x y1)
 
341
                                                  (*_e x y2))))
 
342
                               (implies (edp z)
 
343
                                        (and (=_e (+_e y1 z)
 
344
                                                  (+_e y2 z))
 
345
                                             (=_e (*_e y1 z)
 
346
                                                  (*_e y2 z))))
 
347
                               (=_e (-_e y1)
 
348
                                    (-_e y2))))))
 
349
   :rule-classes nil)
 
350
 
 
351
 (defthm
 
352
   Closure-of-C_=_e
 
353
   (implies (edp x)
 
354
            (edp (C_=_e x))))
 
355
 
 
356
 (defthm
 
357
   Equivalence-class-Laws
 
358
   (and (implies (edp x)
 
359
                 (=_e (C_=_e x) x))
 
360
        (implies (and (edp y1)
 
361
                      (edp y2)
 
362
                      (=_e y1 y2))
 
363
                 (equal (C_=_e y1)
 
364
                        (C_=_e y2))))
 
365
   :rule-classes nil)
 
366
 
 
367
 (defthm
 
368
   Commutativity-Laws
 
369
   (implies (and (edp x)
 
370
                 (edp y))
 
371
            (and (=_e (+_e x y)
 
372
                      (+_e y x))
 
373
                 (=_e (*_e x y)
 
374
                      (*_e y x)))))
 
375
 
 
376
 (defthm
 
377
   Associativity-Laws
 
378
   (implies (and (edp x)
 
379
                 (edp y)
 
380
                 (edp z))
 
381
            (and (=_e (+_e (+_e x y) z)
 
382
                      (+_e x (+_e y z)))
 
383
                 (=_e (*_e (*_e x y) z)
 
384
                      (*_e x (*_e y z))))))
 
385
 
 
386
 (defthm
 
387
   Left-Distributivity-Law
 
388
   (implies (and (edp x)
 
389
                 (edp y)
 
390
                 (edp z))
 
391
            (=_e (*_e x (+_e y z))
 
392
                 (+_e (*_e x y)
 
393
                      (*_e x z)))))
 
394
 
 
395
 (defthm
 
396
   Left-Unicity-Laws
 
397
   (implies (edp x)
 
398
            (and (=_e (+_e (0_e) x)
 
399
                      x)
 
400
                 (=_e (*_e (1_e) x)
 
401
                      x))))
 
402
 
 
403
 (defthm
 
404
   Right-Inverse-Law
 
405
   (implies (edp x)
 
406
            (=_e (+_e x (-_e x))
 
407
                 (0_e))))
 
408
 
 
409
 (defthm
 
410
   Zero-Divisor-Law
 
411
   (implies (and (edp x)
 
412
                 (edp y))
 
413
            (equal (=_e (*_e x y)(0_e))
 
414
                   (or (=_e x (0_e))
 
415
                       (=_e y (0_e))))))
 
416
 
 
417
 ; Euclidean Domain Axioms:
 
418
 (defthm
 
419
   Natp-size
 
420
   (implies (and (edp x)
 
421
                 (not (=_e x (0_e))))
 
422
            (and (integerp (size x))
 
423
                 (>= (size x) 0)))
 
424
   :rule-classes (:type-prescription
 
425
                  :rewrite))
 
426
 
 
427
 (defthm
 
428
   Congruence-for-Size
 
429
   (implies (and (edp y1)
 
430
                 (edp y2)
 
431
                 (=_e y1 y2))
 
432
            (equal (size y1)
 
433
                   (size y2)))
 
434
   :rule-classes nil)
 
435
 
 
436
 (defthm
 
437
   Closure-of-q_e-&-r_e
 
438
   (implies (and (edp x)
 
439
                 (edp y)
 
440
                 (not (=_e y (0_e))))
 
441
            (and (edp (q_e x y))
 
442
                 (edp (r_e x y)))))
 
443
 
 
444
 (defthm
 
445
   Congruence-for-q_e-&-r_e
 
446
   (implies (and (edp y1)
 
447
                 (edp y2)
 
448
                 (=_e y1 y2))
 
449
            (and (implies (and (edp x)
 
450
                               (not (=_e y1 (0_e))))
 
451
                          (and (=_e (q_e x y1)
 
452
                                    (q_e x y2))
 
453
                               (=_e (r_e x y1)
 
454
                                    (r_e x y2))))
 
455
                 (implies (and (edp z)
 
456
                               (not (=_e z (0_e))))
 
457
                          (and (=_e (q_e y1 z)
 
458
                                    (q_e y2 z))
 
459
                               (=_e (r_e y1 z)
 
460
                                    (r_e y2 z))))))
 
461
   :rule-classes nil)
 
462
                 
 
463
 (defthm
 
464
   Division-property
 
465
   (implies (and (edp x)
 
466
                 (edp y)
 
467
                 (not (=_e y (0_e))))
 
468
            (and (=_e x (+_e (*_e y (q_e x y))
 
469
                             (r_e x y)))
 
470
                 (or (=_e (r_e x y)(0_e))
 
471
                     (< (size (r_e x y))
 
472
                        (size y)))))
 
473
   :rule-classes nil)
 
474
 
 
475
 (defthm
 
476
   Size-*_e
 
477
   (implies (and (edp x)
 
478
                 (not (=_e x (0_e)))
 
479
                 (edp y)
 
480
                 (not (=_e y (0_e))))
 
481
            (<= (size x) 
 
482
                (size (*_e x y))))
 
483
   :rule-classes (:linear :rewrite))
 
484
 ) ; end encapsulate
 
485
 
 
486
(add-invisible-fns binary-+_e -_e)
 
487
(add-invisible-fns -_e -_e)
 
488
 
 
489
(add-binop +_e binary-+_e)
 
490
(add-binop *_e binary-*_e)
 
491
 
 
492
(defun
 
493
  ==_e (x1 x2)
 
494
  "==_e nicely extends =_e 
 
495
   to entire ACL2 universe."
 
496
  (if (edp x1)
 
497
      (if (edp x2)
 
498
          (=_e x1 x2)
 
499
          nil)
 
500
      (if (edp x2)
 
501
          nil
 
502
          (equal x1 x2))))
 
503
 
 
504
(defun
 
505
  binary-++_e (x y)
 
506
  "binary-++_e nicely extends +_e
 
507
   to entire ACL2 universe."
 
508
  (if (and (edp x)
 
509
           (edp y))
 
510
      (+_e x y)
 
511
      x))
 
512
 
 
513
(defun
 
514
  binary-**_e (x y)
 
515
  "binary-**_e nicely extends *_e
 
516
   to entire ACL2 universe."
 
517
  (if (and (edp x)
 
518
           (edp y))
 
519
      (*_e x y)
 
520
      x))
 
521
 
 
522
; Convenient Notation:
 
523
(defmacro
 
524
  ++_e (&rest rst)
 
525
  (if rst
 
526
      (if (cdr rst)
 
527
          (xxxjoin 'binary-++_e rst)
 
528
          (list 'binary-++_e '(0_e)(car rst)))
 
529
      '(0_e)))
 
530
 
 
531
(defmacro
 
532
  **_e (&rest rst)
 
533
  (if rst
 
534
      (if (cdr rst)
 
535
          (xxxjoin 'binary-**_e rst)
 
536
          (list 'binary-**_e '(1_e)(car rst)))
 
537
      '(1_e)))
 
538
 
 
539
(add-invisible-fns binary-++_e -_e)
 
540
 
 
541
(add-binop ++_e binary-++_e)
 
542
(add-binop **_e binary-**_e)
 
543
 
 
544
;; Restate Integral Domain Axioms in
 
545
;;  terms of ==_e, C_==_e, ++_e, and **_e
 
546
;;  in place of =_e, C_=_e, +_e, +_e, and *_e.
 
547
 
 
548
(defthm
 
549
  Closure-Laws-for-++_e-&-**_e
 
550
  (implies (and (edp x)
 
551
                (edp y))
 
552
           (and (edp (++_e x y))
 
553
                (edp (**_e x y)))))
 
554
 
 
555
(defthm
 
556
  ==_e-Equivalence-Law
 
557
  (and (booleanp (==_e x y))
 
558
       (==_e x x)  
 
559
       (implies (==_e x y) 
 
560
                (==_e y x))
 
561
       (implies (and (==_e x y)
 
562
                     (==_e y z))
 
563
                (==_e x z)))
 
564
  :rule-classes :equivalence)
 
565
 
 
566
(defthm
 
567
   ==_e-implies-iff-edp
 
568
   (implies (==_e y1 y2)
 
569
            (iff (edp y1)
 
570
                 (edp y2)))
 
571
   :rule-classes :congruence)
 
572
 
 
573
(defthm
 
574
   ==_e-implies-==_e-++_e-1
 
575
   (implies (==_e y1 y2)
 
576
            (==_e (++_e y1 z)
 
577
                  (++_e y2 z)))
 
578
   :rule-classes :congruence
 
579
   :hints (("Goal"
 
580
            :use congruence-laws)))
 
581
 
 
582
(defthm
 
583
   ==_e-implies-==_e-++_e-2
 
584
   (implies (==_e y1 y2)
 
585
            (==_e (++_e x y1)
 
586
                  (++_e x y2)))
 
587
   :rule-classes :congruence
 
588
   :hints (("Goal"
 
589
            :use congruence-laws)))
 
590
 
 
591
(defthm
 
592
   ==_e-implies-==_e-**_e-1
 
593
   (implies (==_e y1 y2)
 
594
            (==_e (**_e y1 z)
 
595
                  (**_e y2 z)))
 
596
   :rule-classes :congruence
 
597
   :hints (("Goal"
 
598
            :use congruence-laws)))
 
599
 
 
600
(defthm
 
601
   ==_e-implies-==_e-**_e-2
 
602
   (implies (==_e y1 y2)
 
603
            (==_e (**_e x y1)
 
604
                  (**_e x y2)))
 
605
   :rule-classes :congruence
 
606
   :hints (("Goal"
 
607
            :use congruence-laws)))
 
608
 
 
609
(defthm
 
610
  ==_e-implies-==_e_-_e
 
611
  (implies (==_e y1 y2)
 
612
           (==_e (-_e y1)
 
613
                 (-_e y2)))
 
614
  :rule-classes :congruence
 
615
  :hints (("Goal"
 
616
           :use congruence-laws)))
 
617
 
 
618
(defun
 
619
  C_==_e (x)
 
620
  "C_==_e nicely extends C_=_e 
 
621
   to entire ACL2 universe."
 
622
  (if (edp x)
 
623
      (C_=_e x)
 
624
      x))
 
625
 
 
626
(defthm
 
627
  ==_e-C_==_e
 
628
  (==_e (C_==_e x) x)
 
629
  :hints (("Goal"
 
630
           :use Equivalence-class-Laws)))
 
631
 
 
632
(defthm
 
633
  ==_e-implies-equal-C_==_e
 
634
  (implies (==_e y1 y2)
 
635
           (equal (C_==_e y1)
 
636
                  (C_==_e y2)))
 
637
  :rule-classes :congruence
 
638
  :hints (("Goal"
 
639
           :use Equivalence-class-Laws)))
 
640
 
 
641
(defthm
 
642
  Commutativity-Laws-for-++_e-&-**_e
 
643
  (implies (and (edp x)
 
644
                (edp y))
 
645
           (and (==_e (++_e x y)
 
646
                      (++_e y x))
 
647
                (==_e (**_e x y)
 
648
                      (**_e y x)))))
 
649
 
 
650
(defthm
 
651
  Associativity-Laws-for-++_e-&-**_e
 
652
  (implies (and (edp x)
 
653
                (edp y)
 
654
                (edp z))
 
655
           (and (==_e (++_e (++_e x y) z)
 
656
                      (++_e x (++_e y z)))
 
657
                (==_e (**_e (**_e x y) z)
 
658
                      (**_e x (**_e y z)))))
 
659
  :hints (("Goal"
 
660
           :in-theory (disable Commutativity-Laws-for-++_e-&-**_e)))) 
 
661
 
 
662
(defthm
 
663
  Left-Distributivity-Law-for-++_e-&-**_e
 
664
  (implies (and (edp x)
 
665
                (edp y)
 
666
                (edp z))
 
667
           (==_e (**_e x (++_e y z))
 
668
                 (++_e (**_e x y)
 
669
                       (**_e x z)))))
 
670
 
 
671
(defthm
 
672
   Left-Unicity-Laws-for-++_e-&-**_e
 
673
   (implies (edp x)
 
674
            (and (==_e (++_e (0_e) x)
 
675
                       x)
 
676
                 (==_e (**_e (1_e) x)
 
677
                       x))))
 
678
 
 
679
(defthm
 
680
  Right-Inverse-Law-for-++_e
 
681
  (implies (edp x)
 
682
           (==_e (++_e x (-_e x))
 
683
                 (0_e))))
 
684
 
 
685
(defthm
 
686
  Zero-Divisor-Law-for-**_e
 
687
  (implies (and (edp x)
 
688
                (edp y))
 
689
           (equal (==_e (**_e x y)(0_e))
 
690
                  (or (==_e x (0_e))
 
691
                      (==_e y (0_e))))))
 
692
 
 
693
;; Restate Euclidean Domain Axioms in
 
694
;;  terms of ==_e, ++_e, **_e, qq_e, and rr_e
 
695
;;  in place of =_e, +_e, +_e, and *_e, q_e, and r_e.
 
696
 
 
697
(defthm
 
698
  Natp-size-==_e
 
699
  (implies (and (edp x)
 
700
                (not (==_e x (0_e))))
 
701
           (and (integerp (size x))
 
702
                (>= (size x) 0)))
 
703
  :rule-classes (:type-prescription
 
704
                 :rewrite))
 
705
 
 
706
(defthm
 
707
  ==_e-implies-equal-size
 
708
  (implies (==_e y1 y2)
 
709
           (equal (size y1)
 
710
                  (size y2)))
 
711
  :rule-classes :congruence
 
712
  :hints (("Goal"
 
713
           :use Congruence-for-Size)))
 
714
 
 
715
(defun
 
716
  qq_e (x y)
 
717
  "qq_e nicely extends q_e
 
718
   to entire ACL2 universe."
 
719
  (if (and (edp x)
 
720
           (edp y)
 
721
           (not (==_e y (0_e))))
 
722
      (q_e x y)
 
723
      x))
 
724
 
 
725
(defun
 
726
  rr_e (x y)
 
727
  "rr_e nicely extends r_e
 
728
   to entire ACL2 universe."
 
729
  (if (and (edp x)
 
730
           (edp y)
 
731
           (not (==_e y (0_e))))
 
732
      (r_e x y)
 
733
      x))
 
734
 
 
735
(defthm
 
736
  Closure-of-qq_e-&-rr_e
 
737
  (implies (and (edp x)
 
738
                (edp y)
 
739
                (not (==_e y (0_e))))
 
740
           (and (edp (qq_e x y))
 
741
                (edp (rr_e x y)))))
 
742
 
 
743
(defthm
 
744
  ==_e-implies-==_e-qq_e-1
 
745
  (implies (==_e y1 y2)
 
746
           (==_e (qq_e y1 z)
 
747
                 (qq_e y2 z)))
 
748
  :rule-classes :congruence
 
749
  :hints (("Goal"
 
750
           :use Congruence-for-q_e-&-r_e)))
 
751
 
 
752
(defthm
 
753
  ==_e-implies-==_e-qq_e-2
 
754
  (implies (==_e y1 y2)
 
755
           (==_e (qq_e x y1)
 
756
                 (qq_e x y2)))
 
757
  :rule-classes :congruence
 
758
  :hints (("Goal"
 
759
           :use Congruence-for-q_e-&-r_e)))
 
760
 
 
761
(defthm
 
762
  ==_e-implies-==_e-rr_e-1
 
763
  (implies (==_e y1 y2)
 
764
           (==_e (rr_e y1 z)
 
765
                 (rr_e y2 z)))
 
766
  :rule-classes :congruence
 
767
  :hints (("Goal"
 
768
           :use Congruence-for-q_e-&-r_e)))
 
769
 
 
770
(defthm
 
771
  ==_e-implies-==_e-rr_e-2
 
772
  (implies (==_e y1 y2)
 
773
           (==_e (rr_e x y1)
 
774
                 (rr_e x y2)))
 
775
  :rule-classes :congruence
 
776
  :hints (("Goal"
 
777
           :use Congruence-for-q_e-&-r_e)))
 
778
 
 
779
(defthm
 
780
  Division-property-for-qq_e-&-rr_e
 
781
  (implies (and (edp x)
 
782
                (edp y)
 
783
                (not (==_e y (0_e))))
 
784
           (and (==_e x (++_e (**_e y (qq_e x y))
 
785
                              (rr_e x y)))
 
786
                (or (==_e (rr_e x y)(0_e))
 
787
                    (< (size (rr_e x y))
 
788
                       (size y)))))
 
789
  :rule-classes ((:elim
 
790
                  :corollary
 
791
                  (implies (and (edp x)
 
792
                                (edp y)
 
793
                                (not (==_e y (0_e))))
 
794
                           (==_e (++_e (rr_e x y)
 
795
                                       (**_e y (qq_e x y)))
 
796
                                 x)))
 
797
                 (:rewrite
 
798
                  :corollary
 
799
                  (implies (and (edp x)
 
800
                                (edp y)
 
801
                                (not (==_e y (0_e))))
 
802
                           (and (==_e (++_e (rr_e x y)
 
803
                                            (**_e y (qq_e x y)))
 
804
                                      x)
 
805
                                (implies (not (==_e (rr_e x y) (0_e)))
 
806
                                         (< (size (rr_e x y))
 
807
                                            (size y))))))
 
808
                 (:linear
 
809
                  :corollary
 
810
                  (implies (and (edp x)
 
811
                                (edp y)
 
812
                                (not (==_e y (0_e)))
 
813
                                (not (==_e (rr_e x y)(0_e))))
 
814
                           (< (size (rr_e x y))
 
815
                              (size y)))))
 
816
   :hints (("Goal"
 
817
            :in-theory (disable commutativity-laws-for-++_e-&-**_e)
 
818
            :use Division-property)))
 
819
 
 
820
(defthm
 
821
  Size-**_e
 
822
  (implies (and (edp x)
 
823
                (not (==_e x (0_e)))
 
824
                (edp y)
 
825
                (not (==_e y (0_e))))
 
826
           (<= (size x) 
 
827
               (size (**_e x y))))
 
828
  :rule-classes (:linear :rewrite))
 
829
 
 
830
(in-theory (disable (:definition ==_e)
 
831
                    (:definition C_==_e)
 
832
                    (:definition binary-++_e)
 
833
                    (:definition binary-**_e)
 
834
                    (:definition qq_e)
 
835
                    (:definition rr_e)))
 
836
 
 
837
;;;;;;;;;;;;;;;;;;;;;;;;;;
 
838
;; Integral Domain Theory:
 
839
 
 
840
(defthm
 
841
  Right-Unicity-Laws
 
842
  (implies (edp x)
 
843
           (and (==_e (++_e x (0_e))
 
844
                      x)
 
845
                (==_e (**_e x (1_e))
 
846
                      x))))
 
847
 
 
848
(defthm
 
849
  Right-Distributivity-Law
 
850
  (implies (and (edp x)
 
851
                (edp y)
 
852
                (edp z))
 
853
           (==_e (**_e (++_e x y) z)
 
854
                 (++_e (**_e x z)
 
855
                       (**_e y z)))))
 
856
 
 
857
(defthm
 
858
  Commutativity-2-Laws
 
859
  (implies (and (edp x)
 
860
                (edp y)
 
861
                (edp z))
 
862
           (and (==_e (++_e x y z)
 
863
                      (++_e y x z))
 
864
                (==_e (**_e x y z)
 
865
                      (**_e y x z))))
 
866
  :hints (("Goal"
 
867
           :use ((:instance
 
868
                  (:functional-instance
 
869
                   acl2-asg::commutativity-2-of-op
 
870
                   (acl2-asg::equiv ==_e)
 
871
                   (acl2-asg::pred edp)
 
872
                   (acl2-asg::op binary-++_e))
 
873
                  (acl2-asg::x x)
 
874
                  (acl2-asg::y y)
 
875
                  (acl2-asg::z z))
 
876
                 (:instance
 
877
                  (:functional-instance
 
878
                   acl2-asg::commutativity-2-of-op
 
879
                   (acl2-asg::equiv ==_e)
 
880
                   (acl2-asg::pred edp)
 
881
                   (acl2-asg::op binary-**_e))
 
882
                  (acl2-asg::x x)
 
883
                  (acl2-asg::y y)
 
884
                  (acl2-asg::z z))))))
 
885
 
 
886
(defthm
 
887
  Nullity-Laws
 
888
  (implies (edp x)
 
889
           (and (==_e (**_e (0_e) x)
 
890
                      (0_e))
 
891
                (==_e (**_e x (0_e))
 
892
                      (0_e)))))
 
893
 
 
894
(defthm
 
895
  Involution-Law
 
896
  (implies (edp x)
 
897
           (==_e (-_e (-_e x))
 
898
                 x))
 
899
  :hints (("Goal"
 
900
           :use ((:instance
 
901
                  (:functional-instance
 
902
                   acl2-agp::Involution-of-inv
 
903
                   (acl2-agp::equiv ==_e)
 
904
                   (acl2-agp::pred edp)
 
905
                   (acl2-agp::op binary-++_e)
 
906
                   (acl2-agp::id 0_e)
 
907
                   (acl2-agp::inv -_e))
 
908
                  (acl2-agp::x x))))))
 
909
 
 
910
(defthm
 
911
  Inverse-Distributive-Law
 
912
  (implies (and (edp x)
 
913
                (edp y))
 
914
           (==_e (-_e (++_e x y))
 
915
                 (++_e (-_e x)(-_e y))))
 
916
  :hints (("Goal"
 
917
           :use ((:instance
 
918
                  (:functional-instance
 
919
                   acl2-agp::Distributivity-of-inv-over-op
 
920
                   (acl2-agp::equiv ==_e)
 
921
                   (acl2-agp::pred edp)
 
922
                   (acl2-agp::op binary-++_e)
 
923
                   (acl2-agp::id 0_e)
 
924
                   (acl2-agp::inv -_e))
 
925
                  (acl2-agp::x x)
 
926
                  (acl2-agp::y y))))))
 
927
 
 
928
(defthm
 
929
  Inverse-Cancellation-Laws
 
930
  (implies (and (edp x)
 
931
                (edp y))
 
932
           (and (==_e (++_e x y (-_e x))
 
933
                      y)
 
934
                (==_e (++_e x (-_e x) y)
 
935
                      y)))
 
936
  :hints (("Goal"
 
937
           :use ((:instance
 
938
                  (:functional-instance
 
939
                   acl2-agp::inv-cancellation-on-right
 
940
                   (acl2-agp::equiv ==_e)
 
941
                   (acl2-agp::pred edp)
 
942
                   (acl2-agp::op binary-++_e)
 
943
                   (acl2-agp::id 0_e)
 
944
                   (acl2-agp::inv -_e))
 
945
                  (acl2-agp::x x)
 
946
                  (acl2-agp::y y))))))
 
947
 
 
948
(defthm
 
949
  Cancellation-Laws-for-++_e
 
950
  (implies (and (edp x)
 
951
                (edp y)
 
952
                (edp z))
 
953
           (and (equal (==_e (++_e x z)(++_e y z))
 
954
                       (==_e x y))
 
955
                (equal (==_e (++_e z x)(++_e z y))
 
956
                       (==_e x y))
 
957
                (equal (==_e (++_e z x)(++_e y z))
 
958
                       (==_e x y))
 
959
                (equal (==_e (++_e x z)(++_e z y))
 
960
                       (==_e x y))))
 
961
  :hints (("Goal" 
 
962
           :use ((:instance
 
963
                  (:functional-instance
 
964
                   acl2-agp::Right-cancellation-for-op
 
965
                   (acl2-agp::equiv ==_e)
 
966
                   (acl2-agp::pred edp)
 
967
                   (acl2-agp::op binary-++_e)
 
968
                   (acl2-agp::id 0_e)
 
969
                   (acl2-agp::inv -_e))
 
970
                  (acl2-agp::x x)
 
971
                  (acl2-agp::y y)
 
972
                  (acl2-agp::z z))))))
 
973
 
 
974
(defthm 
 
975
  Functional-Commutativity-Laws-1
 
976
  (implies (and (edp x)
 
977
                (edp y))
 
978
           (and (==_e (**_e x (-_e y))
 
979
                      (-_e (**_e x y)))
 
980
                (==_e (**_e (-_e y) x)
 
981
                      (-_e (**_e y x)))))
 
982
  :hints (("Goal"
 
983
           :use ((:instance
 
984
                  (:functional-instance
 
985
                   acl2-crg::functional-commutativity-of-minus-times-right
 
986
                   (acl2-crg::equiv ==_e)
 
987
                   (acl2-crg::pred edp)
 
988
                   (acl2-crg::plus binary-++_e)
 
989
                   (acl2-crg::times binary-**_e)
 
990
                   (acl2-crg::zero 0_e)
 
991
                   (acl2-crg::minus -_e))
 
992
                  (acl2-crg::x x)
 
993
                  (acl2-crg::y y))))))
 
994
 
 
995
(defthm
 
996
  -_e-0
 
997
  (==_e (-_e (0_e))
 
998
        (0_e))
 
999
  :hints (("Goal"
 
1000
           :use (:instance
 
1001
                 Cancellation-Laws-for-++_e
 
1002
                 (x (-_e (0_e)))
 
1003
                 (y (0_e))
 
1004
                 (z (0_e))))))
 
1005
 
 
1006
(defthm
 
1007
  Equal_-_e-zero
 
1008
  (implies (edp x)
 
1009
           (equal (==_e (0_e)(-_e x))
 
1010
                  (==_e (0_e) x)))
 
1011
  :hints (("Goal"
 
1012
           :use (:instance
 
1013
                 ==_e-implies-==_e_-_e
 
1014
                 (y1 (0_e))
 
1015
                 (y2 (-_e x))))))
 
1016
 
 
1017
(defthm
 
1018
  ==_e-Inverses-Law
 
1019
  (implies (and (edp x)
 
1020
                (edp y))
 
1021
           (equal (==_e (-_e x)(-_e y))
 
1022
                  (==_e x y)))
 
1023
  :hints (("Goal"
 
1024
           :use (:instance
 
1025
                 ==_e-implies-==_e_-_e
 
1026
                 (y1 (-_e x))
 
1027
                 (y2 (-_e y))))))
 
1028
 
 
1029
(defthm
 
1030
  Idempotent-Law
 
1031
  (implies (edp x)
 
1032
           (equal (==_e (++_e x x) x)
 
1033
                  (==_e x (0_e))))
 
1034
  :hints (("Goal"
 
1035
           :use ((:instance
 
1036
                  (:functional-instance
 
1037
                   acl2-agp::Uniqueness-of-id-as-op-idempotent
 
1038
                   (acl2-agp::equiv ==_e)
 
1039
                   (acl2-agp::pred edp)
 
1040
                   (acl2-agp::op binary-++_e)
 
1041
                   (acl2-agp::id 0_e)
 
1042
                   (acl2-agp::inv -_e))
 
1043
                  (acl2-agp::x x))))))
 
1044
 
 
1045
(defthm
 
1046
  ==_e_-_e-0_e
 
1047
  (implies (and (edp x)
 
1048
                (edp y))
 
1049
           (equal (==_e (++_e x (-_e y))(0_e))
 
1050
                  (==_e x y)))
 
1051
  :hints (("Goal"
 
1052
           :use (:instance
 
1053
                 Cancellation-Laws-for-++_e
 
1054
                 (x (++_e x (-_e y)))
 
1055
                 (y (0_e))
 
1056
                 (z y)))))
 
1057
 
 
1058
(defthm
 
1059
  Cancellation-Laws-for-**_e
 
1060
  (implies (and (edp x)
 
1061
                (edp y)
 
1062
                (edp z))
 
1063
           (and (equal (==_e (**_e x z)(**_e y z))
 
1064
                       (or (==_e z (0_e))
 
1065
                           (==_e x y)))
 
1066
                (equal (==_e (**_e x z)(**_e z y))
 
1067
                       (or (==_e z (0_e))
 
1068
                           (==_e x y)))
 
1069
                (equal (==_e (**_e z x)(**_e y z))
 
1070
                       (or (==_e z (0_e))
 
1071
                           (==_e x y)))
 
1072
                (equal (==_e (**_e z x)(**_e z y))
 
1073
                       (or (==_e z (0_e))
 
1074
                           (==_e x y)))))
 
1075
  :hints (("Goal"
 
1076
           :use ((:instance
 
1077
                  Zero-Divisor-Law-for-**_e
 
1078
                  (x (++_e x (-_e y)))
 
1079
                  (y z))))))
 
1080
 
 
1081
(defthm
 
1082
  Projection-Laws
 
1083
  (implies (and (edp x)
 
1084
                (edp y))
 
1085
           (and (equal (==_e (**_e x y) x)
 
1086
                       (or (==_e x (0_e))
 
1087
                           (==_e y (1_e))))
 
1088
                (equal (==_e (**_e y x) x)
 
1089
                       (or (==_e x (0_e))
 
1090
                           (==_e y (1_e))))
 
1091
                (equal (==_e (++_e x y) x)
 
1092
                       (==_e y (0_e)))
 
1093
                (equal (==_e (++_e y x) x)
 
1094
                       (==_e y (0_e)))))
 
1095
  :hints (("Goal"
 
1096
           :use ((:instance
 
1097
                  Cancellation-Laws-for-**_e
 
1098
                  (z x)(x y)(y (1_e)))
 
1099
                 (:instance
 
1100
                  Cancellation-Laws-for-++_e
 
1101
                  (z x)(x y)(y (0_e)))))))
 
1102
 
 
1103
(defthm
 
1104
  Commutativity-of-==_e
 
1105
  (equal (==_e x y)
 
1106
         (==_e y x))
 
1107
  :rule-classes nil
 
1108
  :hints (("Goal"
 
1109
           :use ((:theorem
 
1110
                  (implies (==_e x y)
 
1111
                           (==_e y x)))))))
 
1112
 
 
1113
(defthm
 
1114
  Projection-Laws-1
 
1115
  (implies (and (edp x)
 
1116
                (edp y))
 
1117
           (and (equal (==_e x (**_e x y))
 
1118
                       (or (==_e x (0_e))
 
1119
                           (==_e y (1_e))))
 
1120
                (equal (==_e x (**_e y x))
 
1121
                       (or (==_e x (0_e))
 
1122
                           (==_e y (1_e))))
 
1123
                (equal (==_e x (++_e x y))
 
1124
                       (==_e y (0_e)))
 
1125
                (equal (==_e x (++_e y x))
 
1126
                       (==_e y (0_e)))))
 
1127
  :hints (("Goal"
 
1128
           :use ((:instance
 
1129
                  Commutativity-of-==_e
 
1130
                  (y (**_e x y)))
 
1131
                 (:instance
 
1132
                  Commutativity-of-==_e
 
1133
                  (y (++_e x y)))))))
 
1134
 
 
1135
(defthm
 
1136
  1_e-0_e
 
1137
  (implies (and (edp x)
 
1138
                (not (==_e x (0_e))))
 
1139
           (not (==_e (1_e)(0_e))))
 
1140
  :rule-classes ((:rewrite
 
1141
                  :corollary
 
1142
                  (implies (and (not (==_e x (0_e)))
 
1143
                                (edp x))
 
1144
                           (not (==_e (1_e)(0_e))))))
 
1145
  :hints (("Goal"
 
1146
           :use Left-Unicity-Laws-for-++_e-&-**_e)))
 
1147
 
 
1148
;;;;;;;;;;;;;;;;;;;;
 
1149
;; Divides-p theory: 
 
1150
 
 
1151
(defun-sk
 
1152
  Divides-p (x y)
 
1153
  (exists z (and (edp x)
 
1154
                 (edp z)
 
1155
                 (=_e (*_e x z)
 
1156
                      y))))
 
1157
 
 
1158
(defun-sk
 
1159
  Divides-p1 (x y)
 
1160
  (exists z (and (edp x)
 
1161
                 (edp z)
 
1162
                 (==_e (**_e x z)
 
1163
                       y))))
 
1164
 
 
1165
(defthm
 
1166
  Divides-p-implies-divides-p1
 
1167
  (implies (divides-p x y)
 
1168
           (divides-p1 x y))
 
1169
  :rule-classes nil
 
1170
  :hints (("Goal"
 
1171
           :in-theory (enable (:definition ==_e)
 
1172
                              (:definition binary-**_e))
 
1173
            :use (:instance
 
1174
                  congruence-laws
 
1175
                  (y1 (*_e x (divides-p-witness x y)))
 
1176
                  (y2 y)))))
 
1177
 
 
1178
(defthm
 
1179
  Divides-p1-implies-divides-p
 
1180
  (implies (divides-p1 x y)
 
1181
           (divides-p x y))
 
1182
  :rule-classes nil
 
1183
  :hints (("Goal"
 
1184
           :in-theory (enable (:definition ==_e)
 
1185
                              (:definition binary-**_e)))))
 
1186
 
 
1187
(defthm
 
1188
  Divides-p-iff-divides-p1
 
1189
  (iff (divides-p x y)
 
1190
       (divides-p1 x y))
 
1191
  :rule-classes nil
 
1192
  :hints (("Goal"
 
1193
           :use (Divides-p-implies-divides-p1
 
1194
                 Divides-p1-implies-divides-p))))
 
1195
 
 
1196
(defthm
 
1197
  Booleanp-divides-p
 
1198
  (Booleanp (divides-p x y)) 
 
1199
  :rule-classes :type-prescription
 
1200
  :hints (("Goal"
 
1201
           :use (:instance
 
1202
                 congruence-laws
 
1203
                 (y1 (*_e x (divides-p-witness x y)))
 
1204
                 (y2 y)))))
 
1205
 
 
1206
(defthm
 
1207
  Divides-p-=-divides-p1
 
1208
  (equal (divides-p x y)
 
1209
         (divides-p1 x y))
 
1210
  :rule-classes nil
 
1211
  :hints (("Goal"
 
1212
           :in-theory (disable (:definition divides-p)
 
1213
                               (:definition divides-p1))
 
1214
           :use Divides-p-iff-divides-p1)))
 
1215
 
 
1216
(defun
 
1217
  Divides-pp-witness (x y)
 
1218
  "Divides-pp-witness nicely
 
1219
   modifies divides-p1-witness."
 
1220
  (divides-p1-witness (C_==_e x)(C_==_e y)))
 
1221
 
 
1222
(defthm
 
1223
  ==_e-implies-==_e-divides-pp-witness-1
 
1224
  (implies (==_e y1 y2)
 
1225
           (==_e (divides-pp-witness y1 z)
 
1226
                 (divides-pp-witness y2 z)))
 
1227
  :rule-classes :congruence)
 
1228
 
 
1229
(defthm
 
1230
  ==_e-implies-==_e-divides-pp-witness-2
 
1231
  (implies (==_e y1 y2)
 
1232
           (==_e (divides-pp-witness x y1)
 
1233
                 (divides-pp-witness x y2)))
 
1234
  :rule-classes :congruence)
 
1235
 
 
1236
(defun
 
1237
  Divides-pp (x y)
 
1238
  (let ((z (divides-pp-witness x y)))
 
1239
       (and (edp x)
 
1240
            (edp z)
 
1241
            (==_e (**_e x z) y))))
 
1242
 
 
1243
(defthm
 
1244
  ==_e-implies-equal-divides-pp-1
 
1245
  (implies (==_e y1 y2)
 
1246
           (equal (divides-pp y1 z)
 
1247
                  (divides-pp y2 z)))
 
1248
  :rule-classes :congruence)
 
1249
 
 
1250
(defthm
 
1251
  ==_e-implies-equal-divides-pp-2
 
1252
  (implies (==_e y1 y2)
 
1253
           (equal (divides-pp x y1)
 
1254
                  (divides-pp x y2)))
 
1255
  :rule-classes :congruence)
 
1256
 
 
1257
(defthm
 
1258
  Divides-pp-suff
 
1259
  (implies (and (edp x)
 
1260
                (edp z)
 
1261
                (==_e (**_e x z) y))
 
1262
           (divides-pp x y))
 
1263
  :hints (("Goal"
 
1264
           :in-theory (disable divides-p1-suff)
 
1265
           :use (:instance
 
1266
                 divides-p1-suff
 
1267
                 (x (C_==_e x))
 
1268
                 (y (C_==_e y))))))
 
1269
 
 
1270
(in-theory (disable (:definition Divides-pp-witness)
 
1271
                    (:executable-counterpart divides-pp)))
 
1272
 
 
1273
(defthm
 
1274
  Divides-p1-=-Divides-pp
 
1275
  (equal (divides-p1 x y)
 
1276
         (divides-pp x y))
 
1277
  :rule-classes nil
 
1278
  :hints (("Goal"
 
1279
           :use ((:theorem
 
1280
                  (implies (divides-p1 x y)
 
1281
                           (divides-pp x y)))
 
1282
                 (:theorem
 
1283
                  (implies (divides-pp x y)
 
1284
                           (divides-p1 x y)))))))
 
1285
 
 
1286
(defthm
 
1287
  Divides-p-=-Divides-pp
 
1288
  (equal (divides-p x y)
 
1289
         (divides-pp x y))
 
1290
  :rule-classes nil
 
1291
  :hints (("Goal"
 
1292
           :use (Divides-p-=-Divides-p1
 
1293
                 Divides-p1-=-Divides-pp))))
 
1294
 
 
1295
(defthm
 
1296
  Divides-pp-edp-1
 
1297
  (implies (divides-pp x y)
 
1298
           (edp x))
 
1299
  :rule-classes :forward-chaining)
 
1300
 
 
1301
(defthm
 
1302
  Divides-pp-edp-2
 
1303
  (implies (divides-pp x y)
 
1304
           (edp y))
 
1305
  :rule-classes :forward-chaining
 
1306
  :hints (("goal"
 
1307
           :use (:instance
 
1308
                 Closure-Laws-for-++_e-&-**_e
 
1309
                 (y (divides-pp-witness x y))))))
 
1310
 
 
1311
(defthm
 
1312
  Divides-pp-edp-divides-pp-witness
 
1313
  (implies (divides-pp x y)
 
1314
           (edp (divides-pp-witness x y))))
 
1315
 
 
1316
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1317
;; (O_e) is greatest element with 
 
1318
;;  respect to divides-pp relation.
 
1319
(defthm
 
1320
  Greatest-divides-pp=0_e
 
1321
  (implies (edp x)
 
1322
           (divides-pp x (0_e))))
 
1323
 
 
1324
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1325
;; (1_e) is least element with 
 
1326
;;  respect to divides-pp relation.
 
1327
(defthm
 
1328
  Least-divides-pp=1_e
 
1329
  (implies (edp x)
 
1330
           (divides-pp (1_e) x)))
 
1331
 
 
1332
(defthm
 
1333
  Transitivity-divides-pp-lemma
 
1334
  (implies (and (edp x)
 
1335
                (edp (divides-pp-witness x y))
 
1336
                (edp (divides-pp-witness y z))
 
1337
                (==_e (**_e x (divides-pp-witness x y)) y)
 
1338
                (==_e (**_e y (divides-pp-witness y z)) z))
 
1339
           (==_e (**_e x
 
1340
                       (divides-pp-witness x y)
 
1341
                       (divides-pp-witness y z))
 
1342
                 z))
 
1343
  :hints (("goal"
 
1344
           :use (:instance
 
1345
                 Associativity-laws-for-++_e-&-**_e
 
1346
                 (y (divides-pp-witness x y))
 
1347
                 (z (divides-pp-witness y z))))))
 
1348
 
 
1349
(defthm
 
1350
  Transitivity-divides-pp
 
1351
  (implies (and (divides-pp x y)
 
1352
                (divides-pp y z))
 
1353
           (divides-pp x z))
 
1354
  :rule-classes (:rewrite
 
1355
                 :forward-chaining)
 
1356
  :hints (("Goal" 
 
1357
           :use (:instance
 
1358
                 Divides-pp-suff
 
1359
                 (y z)
 
1360
                 (z (**_e (divides-pp-witness x y)
 
1361
                          (divides-pp-witness y z)))))))
 
1362
 
 
1363
(defthm
 
1364
  Divides-pp-++_e
 
1365
  (implies (and (divides-pp x y)
 
1366
                (divides-pp x z))
 
1367
           (divides-pp x (++_e y z)))
 
1368
  :hints (("Goal" 
 
1369
           :use (:instance
 
1370
                 divides-pp-suff
 
1371
                 (y (++_e y z))
 
1372
                 (z (++_e (divides-pp-witness x y)
 
1373
                          (divides-pp-witness x z)))))))
 
1374
 
 
1375
(defthm
 
1376
  Divides-pp--_e
 
1377
  (implies (and (divides-pp x y)
 
1378
                (divides-pp x z))
 
1379
           (divides-pp x (++_e y (-_e z))))
 
1380
  :hints (("Goal" 
 
1381
           :use (:instance
 
1382
                 divides-p1-suff
 
1383
                 (y (++_e y (-_e z)))
 
1384
                 (z (++_e (divides-pp-witness x y)
 
1385
                          (-_e (divides-pp-witness x z))))))))
 
1386
 
 
1387
(defthm
 
1388
  Divides-pp-**_e
 
1389
  (implies (and (edp v)
 
1390
                (divides-pp x y))
 
1391
           (and (divides-pp x (**_e y v))
 
1392
                (divides-pp x (**_e v y))))
 
1393
  :hints (("Goal"
 
1394
           :in-theory (disable divides-pp-edp-2)
 
1395
           :use ((:instance
 
1396
                  divides-pp-suff
 
1397
                  (y (**_e v y))
 
1398
                  (z (**_e v (divides-pp-witness x y))))
 
1399
                 divides-pp-edp-2))))
 
1400
 
 
1401
(defthm
 
1402
  Divides-pp-witness-0_e
 
1403
  (implies (and (edp x)
 
1404
                (not (==_e x (0_e))))
 
1405
           (==_e (divides-pp-witness x (0_e))
 
1406
                 (0_e)))
 
1407
  :hints (("Goal"
 
1408
           :in-theory (disable divides-pp-suff
 
1409
                               Greatest-divides-pp=0_e)
 
1410
           :use (:instance
 
1411
                 divides-pp-suff
 
1412
                 (y (0_e))
 
1413
                 (z (0_e))))))
 
1414
 
 
1415
(defthm
 
1416
  Rr_e=0-implies-divides-pp
 
1417
  (implies (and (edp x)
 
1418
                (not (==_e x (0_e)))
 
1419
                (edp y)
 
1420
                (==_e (rr_e y x)(0_e)))
 
1421
           (divides-pp x y))
 
1422
  :hints (("Goal"
 
1423
           :in-theory (disable closure-of-qq_e-&-rr_e)
 
1424
           :use ((:instance
 
1425
                  divides-pp-suff
 
1426
                  (z (qq_e y x)))
 
1427
                 (:instance
 
1428
                  closure-of-qq_e-&-rr_e
 
1429
                  (x y)
 
1430
                  (y x))))))
 
1431
 
 
1432
(defthm
 
1433
  Divides-pp-implies-rr_e=0-lemma
 
1434
  (implies (and (divides-pp x y)
 
1435
                (not (==_e x (0_e))))
 
1436
           (==_e (**_e x (++_e (divides-pp-witness x y)
 
1437
                               (-_e (qq_e y x))))
 
1438
                 (rr_e y x)))
 
1439
  :hints (("Goal"
 
1440
           :in-theory (disable closure-of-qq_e-&-rr_e
 
1441
                               divides-pp-edp-2)
 
1442
           :use ((:instance
 
1443
                  closure-of-qq_e-&-rr_e
 
1444
                  (x y)
 
1445
                  (y x))
 
1446
                 divides-pp-edp-2))))
 
1447
 
 
1448
(defthm
 
1449
  Divides-pp-implies-rr_e=0-lemma-1
 
1450
  (implies (and (==_e (divides-pp-witness x y)(qq_e y x))
 
1451
                (edp x)
 
1452
                (edp y)
 
1453
                (==_e (**_e x (divides-pp-witness x y)) y)
 
1454
                (not (==_e x (0_e))))
 
1455
           (==_e (rr_e y x)(0_e)))
 
1456
  :hints (("goal"
 
1457
           :in-theory (disable closure-of-qq_e-&-rr_e)
 
1458
           :use (:instance
 
1459
                 closure-of-qq_e-&-rr_e
 
1460
                 (x y)
 
1461
                 (y x)))))
 
1462
 
 
1463
(defthm
 
1464
  Divides-p-implies-rr_e=0
 
1465
  (implies (and (divides-pp x y)
 
1466
                (not (==_e x (0_e))))
 
1467
           (==_e (rr_e y x)(0_e)))
 
1468
  :hints (("Goal"
 
1469
           :in-theory (disable divides-pp-edp-2)
 
1470
           :use (divides-pp-edp-2
 
1471
                 (:instance
 
1472
                  Size-**_e
 
1473
                  (y (++_e (divides-pp-witness x y)
 
1474
                           (-_e (qq_e y x)))))))))
 
1475
 
 
1476
(defthm
 
1477
  Divides-pp-implies-witness=qq_e
 
1478
  (implies (and (divides-pp x y)
 
1479
                (not (==_e x (0_e))))
 
1480
           (==_e (divides-pp-witness x y)
 
1481
                 (qq_e y x)))
 
1482
  :hints (("Goal"
 
1483
           :in-theory (disable divides-pp-edp-2
 
1484
                               divides-pp-edp-divides-pp-witness)
 
1485
           :use (divides-pp-edp-2
 
1486
                 (:instance
 
1487
                  Cancellation-Laws-for-**_e
 
1488
                  (z x)
 
1489
                  (x (divides-pp-witness x y))
 
1490
                  (y (qq_e y x)))
 
1491
                 (:instance
 
1492
                  Division-property-for-qq_e-&-rr_e
 
1493
                  (x y)
 
1494
                  (y x))))))
 
1495
 
 
1496
;;;;;;;;;;;;;;;;;;;;;;;
 
1497
;; Associates-p theory:
 
1498
 
 
1499
(defun
 
1500
  Associates-p (x y)
 
1501
  (if (and (edp x)
 
1502
           (edp y))
 
1503
      (and (divides-p x y)
 
1504
           (divides-p y x))
 
1505
      (equal x y)))
 
1506
 
 
1507
(defun
 
1508
  Associates-pp (x y)
 
1509
  (if (and (edp x)
 
1510
           (edp y))
 
1511
      (and (divides-pp x y)
 
1512
           (divides-pp y x))
 
1513
      (equal x y)))
 
1514
 
 
1515
(defthm
 
1516
  Associates-p-=-Associates-pp
 
1517
  (equal (associates-p x y)
 
1518
         (associates-pp x y))
 
1519
  :rule-classes nil
 
1520
  :hints (("Goal"
 
1521
           :in-theory (disable (:definition divides-p)
 
1522
                               (:definition divides-pp))
 
1523
           :use (Divides-p-=-Divides-pp
 
1524
                 (:instance
 
1525
                  Divides-p-=-Divides-pp
 
1526
                  (x y)
 
1527
                  (y x))))))
 
1528
 
 
1529
(defthm 
 
1530
  Associates-pp-is-an-equivalence 
 
1531
  (and (booleanp (associates-pp x y)) 
 
1532
       (associates-pp x x) 
 
1533
       (implies (associates-pp x y) 
 
1534
                (associates-pp y x)) 
 
1535
       (implies (and (associates-pp x y)
 
1536
                     (associates-pp y z))
 
1537
                (associates-pp x z)))
 
1538
  :rule-classes :equivalence
 
1539
  :hints (("Goal"
 
1540
           :in-theory (disable divides-pp))))
 
1541
 
 
1542
(defthm
 
1543
  ==_e-implies-equal-associates-pp-1
 
1544
  (implies (==_e y1 y2)
 
1545
           (equal (associates-pp y1 z)
 
1546
                  (associates-pp y2 z)))
 
1547
  :rule-classes :congruence
 
1548
  :hints (("Goal"
 
1549
           :in-theory (disable (:definition divides-pp)))
 
1550
          ("Subgoal 2"
 
1551
           :in-theory (enable (:definition ==_e)))
 
1552
          ("Subgoal 1"
 
1553
           :in-theory (enable (:definition ==_e)))))
 
1554
 
 
1555
(defthm
 
1556
  ==_e-implies-equal-associates-pp-2
 
1557
  (implies (==_e y1 y2)
 
1558
           (equal (associates-pp x y1)
 
1559
                  (associates-pp x y2)))
 
1560
  :rule-classes :congruence
 
1561
  :hints (("Goal"
 
1562
           :in-theory (disable (:definition divides-pp)))
 
1563
          ("Subgoal 2"
 
1564
           :in-theory (enable (:definition ==_e)))
 
1565
          ("Subgoal 1"
 
1566
           :in-theory (enable (:definition ==_e)))))
 
1567
 
 
1568
(defthm
 
1569
  ==_e-refines-associates-pp
 
1570
  (implies (==_e x y)
 
1571
           (associates-pp x y))
 
1572
  :rule-classes :refinement)
 
1573
 
 
1574
(defthm
 
1575
  Associates-pp-implies-equal-divides-pp-1
 
1576
  (implies (associates-pp x1 x2)
 
1577
           (equal (divides-pp x1 y)
 
1578
                  (divides-pp x2 y)))
 
1579
  :rule-classes :congruence
 
1580
  :hints (("Goal"
 
1581
           :use ((:instance
 
1582
                  Transitivity-divides-pp
 
1583
                  (x x2)
 
1584
                  (y x1)
 
1585
                  (z y))
 
1586
                 (:instance
 
1587
                  Transitivity-divides-pp
 
1588
                  (x x1)
 
1589
                  (y x2)
 
1590
                  (z y))))))
 
1591
 
 
1592
(defthm
 
1593
  Associates-pp-implies-equal-divides-pp-2
 
1594
  (implies (associates-pp y1 y2)
 
1595
           (equal (divides-pp x y1)
 
1596
                  (divides-pp x y2)))
 
1597
  :rule-classes :congruence
 
1598
  :hints (("Goal"
 
1599
           :in-theory (disable 
 
1600
                       associates-pp-implies-equal-divides-pp-1)
 
1601
           :use ((:instance
 
1602
                  Transitivity-divides-pp
 
1603
                  (y y1)
 
1604
                  (z y2))
 
1605
                 (:instance
 
1606
                  Transitivity-divides-pp
 
1607
                  (y y2)
 
1608
                  (z y1))))))
 
1609
 
 
1610
(defthm
 
1611
  Divides-pp-<=-Size
 
1612
  (implies (and (divides-pp x y)
 
1613
                (not (==_e y (0_e))))
 
1614
           (<= (size x)
 
1615
               (size y)))
 
1616
  :hints (("Goal"
 
1617
           :in-theory (disable divides-pp-implies-witness=qq_e)
 
1618
           :use (:instance
 
1619
                 Size-**_e
 
1620
                 (y (divides-pp-witness x y))))))
 
1621
 
 
1622
(defthm
 
1623
  Associates-pp-implies-equal-Size-lemma-1
 
1624
  (implies (and (associates-pp x y)
 
1625
                (not (==_e y (0_e))))
 
1626
           (equal (Size x)
 
1627
                  (Size y)))
 
1628
  :rule-classes nil
 
1629
  :hints (("Goal"
 
1630
           :in-theory (disable (:definition divides-pp))
 
1631
           :use (Divides-pp-<=-Size
 
1632
                 (:instance
 
1633
                  Divides-pp-<=-Size
 
1634
                  (x y)
 
1635
                  (y x))
 
1636
                 (:theorem
 
1637
                  (implies (and (associates-pp x y)
 
1638
                                (not (==_e y (0_e))))
 
1639
                           (not (==_e x (0_e)))))))
 
1640
          ("Subgoal 1"
 
1641
           :in-theory (enable (:definition divides-pp)))))
 
1642
 
 
1643
(defthm
 
1644
  Associates-pp-implies-equal-Size-lemma-2
 
1645
  (implies (and (associates-pp x y)
 
1646
                (not (==_e x (0_e))))
 
1647
           (equal (Size x)
 
1648
                  (Size y)))
 
1649
  :rule-classes nil
 
1650
  :hints (("Goal"
 
1651
           :in-theory (disable (:definition divides-pp))
 
1652
           :use (Divides-pp-<=-Size
 
1653
                 (:instance
 
1654
                  Divides-pp-<=-Size
 
1655
                  (x y)
 
1656
                  (y x))
 
1657
                 (:theorem
 
1658
                  (implies (and (associates-pp x y)
 
1659
                                (not (==_e x (0_e))))
 
1660
                           (not (==_e y (0_e)))))))
 
1661
          ("Subgoal 1"
 
1662
           :in-theory (enable (:definition divides-pp)))))
 
1663
 
 
1664
(defthm
 
1665
  Associates-pp-implies-equal-Size
 
1666
  (implies (associates-pp x1 x2)
 
1667
           (equal (size x1)
 
1668
                  (size x2)))
 
1669
  :rule-classes :congruence
 
1670
  :hints (("Goal"
 
1671
           :cases ((not (==_e x2 (0_e)))
 
1672
                   (not (==_e x1 (0_e)))))
 
1673
          ("Subgoal 2"
 
1674
           :by (:instance
 
1675
                Associates-pp-implies-equal-Size-lemma-1
 
1676
                (x x1)
 
1677
                (y x2)))
 
1678
          ("Subgoal 1"
 
1679
           :by (:instance
 
1680
                Associates-pp-implies-equal-Size-lemma-2
 
1681
                (x x1)
 
1682
                (y x2)))))
 
1683
 
 
1684
;;;;;;;;;;;;;;;;;
 
1685
;; Unit-p theory:
 
1686
 
 
1687
(defun
 
1688
  Unit-p (x)
 
1689
  (divides-p x (1_e)))
 
1690
 
 
1691
(defun
 
1692
  Unit-p1 (x)
 
1693
  (divides-p1 x (1_e)))
 
1694
 
 
1695
(defun
 
1696
  Unit-pp (x)
 
1697
  (divides-pp x (1_e)))
 
1698
 
 
1699
(defthm
 
1700
  Unit-p-=-unit-p1
 
1701
  (equal (unit-p x)
 
1702
         (unit-p1 x))
 
1703
  :rule-classes nil
 
1704
  :hints (("Goal"
 
1705
           :use (:instance
 
1706
                 Divides-p-=-Divides-p1
 
1707
                 (y (1_e))))))
 
1708
 
 
1709
(defthm
 
1710
  Unit-p1-=-unit-pp
 
1711
  (equal (unit-p1 x)
 
1712
         (unit-pp x))
 
1713
  :rule-classes nil
 
1714
  :hints (("Goal"
 
1715
           :use (:instance
 
1716
                 Divides-p1-=-Divides-pp
 
1717
                 (y (1_e))))))
 
1718
 
 
1719
(defthm
 
1720
  Unit-p-=-Unit-pp
 
1721
  (equal (unit-p x)
 
1722
         (unit-pp x))
 
1723
  :rule-classes nil
 
1724
  :hints (("Goal"
 
1725
           :use (:instance
 
1726
                 Divides-p-=-Divides-pp
 
1727
                 (y (1_e))))))
 
1728
 
 
1729
(defthm
 
1730
  ==_e-implies-equal-unit-pp
 
1731
  (implies (==_e x1 x2)
 
1732
           (equal (unit-pp x1)
 
1733
                  (unit-pp x2)))
 
1734
  :rule-classes :congruence)
 
1735
 
 
1736
(defthm
 
1737
  Associates-pp-implies-equal-unit-pp
 
1738
  (implies (associates-pp x1 x2)
 
1739
           (equal (unit-pp x1)
 
1740
                  (unit-pp x2)))
 
1741
  :rule-classes :congruence)
 
1742
 
 
1743
(defthm
 
1744
  Unit-pp-1_e
 
1745
  (unit-pp (1_e)))
 
1746
 
 
1747
(defthm
 
1748
  Unit-pp-_-_e-1_e
 
1749
  (unit-pp (-_e (1_e)))
 
1750
  :hints (("Goal"
 
1751
           :use (:instance
 
1752
                 Divides-pp-suff
 
1753
                 (x (-_e (1_e)))
 
1754
                 (y (1_e))
 
1755
                 (z (-_e (1_e)))))))
 
1756
 
 
1757
(defthm
 
1758
  Size-unit-pp=Size-1_e
 
1759
  (implies (unit-pp x)
 
1760
           (equal (size x)
 
1761
                  (size (1_e))))
 
1762
  :rule-classes nil
 
1763
  :hints (("Goal"
 
1764
           :in-theory (disable (:definition associates-pp))
 
1765
           :use (:theorem
 
1766
                 (implies (unit-pp x)
 
1767
                          (associates-pp x (1_e)))))
 
1768
          ("Subgoal 1"
 
1769
           :in-theory (enable (:definition associates-pp)))))
 
1770
 
 
1771
(defthm
 
1772
  Size-unit-p=Size-1_e
 
1773
  (implies (unit-p x)
 
1774
           (equal (size x)
 
1775
                  (size (1_e))))
 
1776
  :rule-classes nil
 
1777
  :hints (("Goal"
 
1778
           :in-theory (disable (:definition unit-p)
 
1779
                               (:definition unit-pp))
 
1780
           :use (unit-p-=-unit-pp
 
1781
                 Size-unit-pp=Size-1_e))))
 
1782
 
 
1783
(defthm
 
1784
  Size->=-Size-1_e
 
1785
  (implies (and (not (==_e x (0_e)))
 
1786
                (edp x))
 
1787
           (>= (size x)(size (1_e))))
 
1788
  :rule-classes (:linear
 
1789
                 :rewrite))
 
1790
 
 
1791
(defthm
 
1792
  Rr_e-1_e-x=0_e
 
1793
  (implies (and (edp x)
 
1794
                (not (==_e x (0_e)))
 
1795
                (equal (size x)
 
1796
                       (size (1_e))))
 
1797
           (==_e (rr_e (1_e) x)(0_e))))
 
1798
 
 
1799
(defthm
 
1800
  Size=Size-1_e-implies-unit-pp
 
1801
  (implies (and (edp x)
 
1802
                (not (==_e x (0_e)))
 
1803
                (equal (size x)
 
1804
                       (size (1_e))))
 
1805
           (unit-pp x)))
 
1806
 
 
1807
(defthm
 
1808
  Size=Size-1_e-implies-unit-p
 
1809
  (implies (and (edp x)
 
1810
                (not (=_e x (0_e)))
 
1811
                (equal (size x)
 
1812
                       (size (1_e))))
 
1813
           (unit-p x))
 
1814
  :hints (("Goal"
 
1815
           :in-theory (e/d ((:definition ==_e))
 
1816
                           ((:definition unit-p)
 
1817
                            (:definition unit-pp)
 
1818
                            Size=Size-1_e-implies-unit-pp))
 
1819
           :use (unit-p-=-unit-pp
 
1820
                 Size=Size-1_e-implies-unit-pp))))
 
1821
 
 
1822
(defthm
 
1823
  Size-<-Size-**_e-lemma-1
 
1824
  (implies (and (edp x)
 
1825
                (not (==_e x (0_e)))
 
1826
                (edp y)
 
1827
                (not (==_e y (0_e))))
 
1828
           (==_e (++_e x
 
1829
                       (-_e (**_e x y (qq_e x (**_e x y)))))
 
1830
                 (rr_e x (**_e x y))))
 
1831
  :rule-classes nil
 
1832
  :hints (("Goal"
 
1833
           :use ((:instance
 
1834
                  Division-property-for-qq_e-&-rr_e
 
1835
                  (y (**_e x y)))
 
1836
                 (:instance
 
1837
                  (:theorem
 
1838
                   (implies (and (edp x)
 
1839
                                 (edp y)
 
1840
                                 (edp z))
 
1841
                            (iff (==_e x (++_e y z))
 
1842
                                 (==_e y (++_e x (-_e z))))))
 
1843
                  (y (rr_e x (**_e x y)))
 
1844
                  (z (**_e x y (qq_e x (**_e x y)))))))))
 
1845
 
 
1846
(defthm
 
1847
  Size-<-Size-**_e-lemma-2
 
1848
  (implies (and (edp x)
 
1849
                (not (==_e x (0_e)))
 
1850
                (edp y)
 
1851
                (not (==_e y (0_e)))
 
1852
                (not (==_e (rr_e x (**_e x y))
 
1853
                           (0_e))))
 
1854
           (>= (Size (rr_e x (**_e x y)))
 
1855
               (Size x)))
 
1856
  :rule-classes nil
 
1857
  :hints (("Goal"
 
1858
           :use (Size-<-Size-**_e-lemma-1))))
 
1859
 
 
1860
(defthm
 
1861
  Size-<-Size-**_e-lemma-3
 
1862
  (implies (and (edp x)
 
1863
                (not (==_e x (0_e)))
 
1864
                (edp y)
 
1865
                (not (==_e y (0_e)))
 
1866
                (equal (Size x)
 
1867
                       (Size (**_e x y))))
 
1868
           (unit-pp y))
 
1869
  :rule-classes nil
 
1870
  :hints (("Goal"
 
1871
           :use (Size-<-Size-**_e-lemma-2
 
1872
                 (:instance
 
1873
                  divides-pp-suff
 
1874
                  (y (1_e))
 
1875
                  (x y)
 
1876
                  (z (qq_e x (**_e x y))))
 
1877
                 (:instance
 
1878
                  Division-property-for-qq_e-&-rr_e
 
1879
                  (y (**_e x y)))))))
 
1880
 
 
1881
(defthm
 
1882
  Size-<-Size-**_e
 
1883
  (implies (and (not (unit-pp y))
 
1884
                (edp x)
 
1885
                (not (==_e x (0_e)))
 
1886
                (edp y)
 
1887
                (not (==_e y (0_e))))
 
1888
           (< (Size x)
 
1889
              (Size (**_e x y))))
 
1890
  :rule-classes (:linear 
 
1891
                 :rewrite)
 
1892
  :hints (("Goal"
 
1893
           :use Size-<-Size-**_e-lemma-3)
 
1894
          ("[1]Subgoal 2"
 
1895
           :use (:theorem
 
1896
                 (implies (and (edp x)
 
1897
                               (not (==_e x (0_e)))
 
1898
                               (edp y)
 
1899
                               (not (==_e y (0_e))))
 
1900
                          (integerp (size (**_e x y))))))
 
1901
          ("[1]Subgoal 1"
 
1902
           :use (:theorem
 
1903
                 (implies (and (edp x)
 
1904
                               (not (==_e x (0_e)))
 
1905
                               (edp y)
 
1906
                               (not (==_e y (0_e))))
 
1907
                          (integerp (size (**_e x y))))))))
 
1908
 
 
1909
(defthm
 
1910
  Unit-pp-divides-pp-witness
 
1911
  (implies (unit-pp x)
 
1912
           (unit-pp (divides-pp-witness x (1_e)))))
 
1913
 
 
1914
(defthm
 
1915
  Divides-pp-witness-divides-pp-witness
 
1916
  (implies (unit-pp x)
 
1917
           (==_e (divides-pp-witness (divides-pp-witness x (1_e))
 
1918
                                     (1_e))
 
1919
                 x))
 
1920
  :hints (("Goal"
 
1921
           :in-theory (disable divides-pp-implies-witness=qq_e)
 
1922
           :use (Unit-pp-divides-pp-witness
 
1923
                 (:instance
 
1924
                  Cancellation-Laws-for-**_e
 
1925
                  (z (divides-pp-witness x (1_e)))
 
1926
                  (y (divides-pp-witness (divides-pp-witness x (1_e))
 
1927
                                         (1_e))))
 
1928
                 (:instance
 
1929
                  1_e-0_e
 
1930
                  (x (divides-pp-witness (0_e)(0_e))))))
 
1931
          ("Subgoal 2"
 
1932
           :use 1_e-0_e)))
 
1933
 
 
1934
(defthm
 
1935
  Unit-pp-closure-**_e
 
1936
  (implies (and (unit-pp u)
 
1937
                (unit-pp v))
 
1938
           (unit-pp (**_e u v)))
 
1939
  :hints (("Goal"
 
1940
           :in-theory (disable divides-pp-edp-1)
 
1941
           :use (:instance
 
1942
                 divides-pp-suff
 
1943
                 (x (**_e u v))
 
1944
                 (y (1_e))
 
1945
                 (z (**_e (divides-pp-witness u (1_e))
 
1946
                          (divides-pp-witness v (1_e))))))))
 
1947
 
 
1948
(defthm
 
1949
  Inverse-Cancellation-Laws-**_e
 
1950
  (implies (and (edp u)
 
1951
                (edp x)
 
1952
                (edp y)
 
1953
                (==_e (**_e u x)(1_e)))
 
1954
           (and (==_e (**_e u x y) y)
 
1955
                (==_e (**_e u y x) y)
 
1956
                (==_e (**_e x u y) y)
 
1957
                (==_e (**_e x y u) y)
 
1958
                (==_e (**_e y u x) y)
 
1959
                (==_e (**_e y x u) y)))
 
1960
  :hints (("Goal"
 
1961
           :use (:instance
 
1962
                 associativity-laws-for-++_e-&-**_e
 
1963
                 (x u)
 
1964
                 (y x)
 
1965
                 (z y)))))
 
1966
 
 
1967
(defthm
 
1968
  Unit-pp-**_e-inverse
 
1969
  (implies (and (unit-pp u)
 
1970
                (edp x)
 
1971
                (==_e (**_e u x)
 
1972
                      y))
 
1973
           (==_e (**_e y (divides-pp-witness u (1_e)))
 
1974
                 x))
 
1975
  :rule-classes ((:rewrite
 
1976
                  :corollary
 
1977
                  (implies (and (unit-pp u)
 
1978
                                (==_e (**_e u x)
 
1979
                                      y)
 
1980
                                (edp x))
 
1981
                           (==_e (**_e y (divides-pp-witness u (1_e)))
 
1982
                                 x)))))
 
1983
 
 
1984
(defthm
 
1985
  Unit-pp-Inverse-Distributive-Law
 
1986
  (implies (and (unit-pp x)
 
1987
                (unit-pp y))
 
1988
           (==_e (divides-pp-witness (**_e x y)(1_e))
 
1989
                 (**_e (divides-pp-witness x (1_e))
 
1990
                       (divides-pp-witness y (1_e)))))
 
1991
  :hints (("Goal"
 
1992
           :by (:instance
 
1993
                (:functional-instance
 
1994
                 acl2-agp::Distributivity-of-inv-over-op
 
1995
                 (acl2-agp::equiv ==_e)
 
1996
                 (acl2-agp::pred unit-pp)
 
1997
                 (acl2-agp::op binary-**_e)
 
1998
                 (acl2-agp::id 1_e)
 
1999
                 (acl2-agp::inv (lambda (x)(divides-pp-witness x (1_e)))))
 
2000
                (acl2-agp::x x)
 
2001
                (acl2-agp::y y)))
 
2002
          ("Subgoal 3"
 
2003
; Changed after v4-3 by Kaufmann/Moore, for tau system --
 
2004
; tau on {"Subgoal 3"} tau off: {"Subgoal 8"}
 
2005
           :use (:instance
 
2006
                 Unit-pp-closure-**_e
 
2007
                 (u acl2-agp::x)
 
2008
                 (v acl2-agp::y)))))
 
2009
 
 
2010
(defthm
 
2011
  Divides-pp-witness-1_e
 
2012
  (==_e (divides-pp-witness (1_e)(1_e))
 
2013
        (1_e))
 
2014
  :hints (("Goal"
 
2015
           :in-theory (disable least-divides-pp=1_e                       
 
2016
                               divides-pp-suff)
 
2017
           :use (:instance
 
2018
                 divides-pp-suff
 
2019
                 (x (1_e))
 
2020
                 (y (1_e))
 
2021
                 (z (1_e))))))
 
2022
 
 
2023
(defthm
 
2024
  Divides-pp-witness-_-_e-1_e
 
2025
  (==_e (divides-pp-witness (-_e (1_e))(1_e))
 
2026
        (-_e (1_e)))
 
2027
  :hints (("Goal"
 
2028
           :use (:instance
 
2029
                 Unit-pp-**_e-inverse
 
2030
                 (u (-_e (1_e)))
 
2031
                 (x (-_e (1_e)))
 
2032
                 (y (1_e))))))
 
2033
 
 
2034
(defthm
 
2035
  Not-Unit-pp-0_e
 
2036
  (implies (and (not (==_e x (0_e)))
 
2037
                (edp x))
 
2038
           (not (unit-pp (0_e))))
 
2039
  :hints (("Goal"
 
2040
           :in-theory (disable 1_e-0_e)
 
2041
           :use 1_e-0_e)))
 
2042
 
 
2043
(defthm
 
2044
  Unit-pp-0_e
 
2045
  (implies (==_e (1_e)(0_e))
 
2046
           (unit-pp (0_e))))
 
2047
 
 
2048
(defthm
 
2049
  Unit-pp-edp
 
2050
  (implies (unit-pp x)
 
2051
           (edp x))
 
2052
  :rule-classes :forward-chaining)
 
2053
 
 
2054
(defthm
 
2055
  Unit-pp-**_e=>unit-pp-factor-left
 
2056
  (implies (and (edp x)
 
2057
                (edp y)
 
2058
                (unit-pp (**_e x y)))
 
2059
           (unit-pp x))
 
2060
  :rule-classes nil
 
2061
  :hints (("Goal"
 
2062
           :use (:instance
 
2063
                 divides-pp-suff
 
2064
                 (y (1_e))
 
2065
                 (z (**_e y (divides-pp-witness (**_e x y)(1_e))))))))
 
2066
 
 
2067
(defthm
 
2068
  Unit-pp-**_e=>unit-pp-factor-right
 
2069
  (implies (and (edp x)
 
2070
                (edp y)
 
2071
                (unit-pp (**_e x y)))
 
2072
           (unit-pp y))
 
2073
  :rule-classes nil
 
2074
  :hints (("Goal"
 
2075
           :use (:instance
 
2076
                 Unit-pp-**_e=>unit-pp-factor-left
 
2077
                 (x y)
 
2078
                 (y x)))))
 
2079
 
 
2080
(in-theory (disable (:executable-counterpart unit-p)
 
2081
                    (:executable-counterpart unit-p1)
 
2082
                    (:executable-counterpart unit-pp)))
 
2083
                    
 
2084
;;;;;;;;;;;;;;;;;;;;;;;;
 
2085
;; Reducible-p and
 
2086
;; Irreducible-p theory:
 
2087
 
 
2088
(defun-sk
 
2089
  Reducible-p (x)
 
2090
  (exists (y z)(and (edp y)
 
2091
                    (edp z)
 
2092
                    (not (unit-p y))
 
2093
                    (not (unit-p z))
 
2094
                    (=_e (*_e y z) x))))
 
2095
 
 
2096
(defun-sk
 
2097
  Reducible-p1 (x)
 
2098
  (exists (y z)(and (edp y)
 
2099
                    (edp z)
 
2100
                    (not (unit-p1 y))
 
2101
                    (not (unit-p1 z))
 
2102
                    (==_e (**_e y z) x))))
 
2103
 
 
2104
(defthm
 
2105
  Reducible-p1-suff-1
 
2106
  (implies (and (==_e (**_e y z) x)
 
2107
                (edp y)
 
2108
                (edp z)
 
2109
                (not (unit-p y))
 
2110
                (not (unit-p z)))
 
2111
           (reducible-p1 x))
 
2112
  :rule-classes nil
 
2113
  :hints (("Goal"
 
2114
           :in-theory (disable (:definition unit-p)
 
2115
                               (:definition unit-p1))
 
2116
           :use ((:instance
 
2117
                  unit-p-=-unit-p1
 
2118
                  (x y))
 
2119
                 (:instance
 
2120
                  unit-p-=-unit-p1
 
2121
                  (x z))))))
 
2122
 
 
2123
(defthm
 
2124
  Reducible-p1-suff-2
 
2125
  (implies (and (=_e (*_e y z) x)
 
2126
                (edp y)
 
2127
                (edp z)
 
2128
                (not (unit-p y))
 
2129
                (not (unit-p z)))
 
2130
           (reducible-p1 x))
 
2131
  :hints (("Goal"
 
2132
           :in-theory (e/d ((:definition ==_e)
 
2133
                            (:definition binary-**_e))
 
2134
                           ((:definition reducible-p1)
 
2135
                            (:definition unit-p)))
 
2136
           :use (Reducible-p1-suff-1
 
2137
                 (:instance
 
2138
                  congruence-laws
 
2139
                  (y1 (*_e y z))
 
2140
                  (y2 x))))))
 
2141
 
 
2142
(defthm
 
2143
  Reducible-p-implies-reducible-p1
 
2144
  (implies (reducible-p x)
 
2145
           (reducible-p1 x))
 
2146
  :rule-classes nil
 
2147
  :hints (("Goal"
 
2148
           :in-theory (disable (:definition reducible-p1)
 
2149
                               (:definition unit-p)))))
 
2150
 
 
2151
(defthm
 
2152
  Reducible-p-suff-1
 
2153
  (implies (and (=_e (*_e y z) x)
 
2154
                (edp y)
 
2155
                (edp z)
 
2156
                (not (unit-p1 y))
 
2157
                (not (unit-p1 z)))
 
2158
           (reducible-p x))
 
2159
  :rule-classes nil
 
2160
  :hints (("Goal"
 
2161
           :in-theory (disable (:definition unit-p)
 
2162
                               (:definition unit-p1))
 
2163
           :use ((:instance
 
2164
                  unit-p-=-unit-p1
 
2165
                  (x y))
 
2166
                 (:instance
 
2167
                  unit-p-=-unit-p1
 
2168
                  (x z))))))
 
2169
 
 
2170
(defthm
 
2171
  Reducible-p-suff-2
 
2172
  (implies (and (==_e (**_e y z) x)
 
2173
                (edp y)
 
2174
                (edp z)
 
2175
                (not (unit-p1 y))
 
2176
                (not (unit-p1 z)))
 
2177
           (reducible-p x))
 
2178
  :hints (("Goal"
 
2179
           :in-theory (e/d ((:definition ==_e)
 
2180
                            (:definition binary-**_e))
 
2181
                           ((:definition reducible-p)
 
2182
                            (:definition unit-p1)))
 
2183
           :use Reducible-p-suff-1)))
 
2184
 
 
2185
(in-theory (disable (:executable-counterpart binary-**_e)))
 
2186
 
 
2187
(defthm
 
2188
  Reducible-p1-implies-reducible-p
 
2189
  (implies (reducible-p1 x)
 
2190
           (reducible-p x))
 
2191
  :rule-classes nil
 
2192
  :hints (("Goal"
 
2193
           :in-theory (disable (:definition reducible-p)
 
2194
                               (:definition unit-p1)))))
 
2195
 
 
2196
(defthm
 
2197
  Reducible-p-iff-reducible-p1
 
2198
  (iff (reducible-p x)
 
2199
       (reducible-p1 x))
 
2200
  :rule-classes nil
 
2201
  :hints (("Goal"
 
2202
           :use (Reducible-p-implies-reducible-p1
 
2203
                 Reducible-p1-implies-reducible-p))))
 
2204
 
 
2205
(defthm
 
2206
  Booleanp-reducible-p
 
2207
  (Booleanp (reducible-p x)) 
 
2208
  :rule-classes :type-prescription
 
2209
  :hints (("Goal"
 
2210
           :in-theory (disable (:definition unit-p))
 
2211
           :use (:instance
 
2212
                 congruence-laws
 
2213
                 (y1 (*_e (mv-nth 0 (reducible-p-witness x))
 
2214
                         (mv-nth 1 (reducible-p-witness x))))
 
2215
                 (y2 x)))))
 
2216
 
 
2217
(defthm
 
2218
  Reducible-p-=-reducible-p1
 
2219
  (equal (reducible-p x)
 
2220
         (reducible-p1 x))
 
2221
  :rule-classes nil
 
2222
  :hints (("Goal"
 
2223
           :in-theory (disable (:definition reducible-p)
 
2224
                               (:definition reducible-p1))
 
2225
           :use Reducible-p-iff-reducible-p1)))
 
2226
 
 
2227
(defun
 
2228
  Reducible-pp-witness (x)
 
2229
  "Reducible-pp-witness nicely
 
2230
   modifies reducible-p1-witness."
 
2231
  (reducible-p1-witness (C_==_e x)))
 
2232
 
 
2233
(defthm
 
2234
  ==_e-implies-equal-reducible-pp-witness
 
2235
  (implies (==_e y1 y2)
 
2236
           (equal (reducible-pp-witness y1)
 
2237
                  (reducible-pp-witness y2)))
 
2238
  :rule-classes :congruence)
 
2239
 
 
2240
(defun
 
2241
  Reducible-pp (x)
 
2242
  (mv-let (y z)
 
2243
          (reducible-pp-witness x)
 
2244
          (and (edp y)
 
2245
               (edp z)
 
2246
               (not (unit-pp y))
 
2247
               (not (unit-pp z))
 
2248
               (==_e (**_e y z) x))))
 
2249
 
 
2250
(defthm
 
2251
  ==_e-implies-equal-reducible-pp
 
2252
  (implies (==_e y1 y2)
 
2253
           (equal (reducible-pp y1)
 
2254
                  (reducible-pp y2)))
 
2255
  :rule-classes :congruence)
 
2256
 
 
2257
(defthm
 
2258
  Reducible-p1-suff-3
 
2259
  (implies (and (edp y)
 
2260
                (edp z)
 
2261
                (not (unit-pp y))
 
2262
                (not (unit-pp z))
 
2263
                (==_e (**_e y z) x))
 
2264
           (reducible-p1 x))
 
2265
  :hints (("Goal"
 
2266
           :use ((:instance
 
2267
                  Unit-p1-=-Unit-pp
 
2268
                  (x y))
 
2269
                 (:instance
 
2270
                  Unit-p1-=-Unit-pp
 
2271
                  (x z))))))
 
2272
 
 
2273
(defthm
 
2274
  Reducible-pp-suff
 
2275
  (implies (and (==_e (**_e y z) x)
 
2276
                (edp y)
 
2277
                (edp z)
 
2278
                (not (unit-pp y))
 
2279
                (not (unit-pp z)))
 
2280
           (reducible-pp x))
 
2281
  :hints (("Goal"
 
2282
           :in-theory (disable reducible-p1-suff-3)
 
2283
           :use (:instance
 
2284
                 reducible-p1-suff-3
 
2285
                 (x (C_==_e x))))))
 
2286
 
 
2287
(in-theory (disable (:definition reducible-pp-witness)
 
2288
                    (:executable-counterpart reducible-pp)))
 
2289
 
 
2290
(defthm
 
2291
  Reducible-p1-implies-reducible-pp
 
2292
  (implies (reducible-p1 x)
 
2293
           (reducible-pp x))
 
2294
  :rule-classes nil
 
2295
  :hints (("Goal"
 
2296
           :in-theory (disable unit-p1 unit-pp
 
2297
                               (:definition reducible-pp))
 
2298
          :use ((:instance
 
2299
                 Reducible-pp-suff
 
2300
                 (y (car (reducible-p1-witness x)))
 
2301
                 (z (mv-nth 1 (reducible-p1-witness x))))
 
2302
                (:instance
 
2303
                 unit-p1-=-unit-pp
 
2304
                 (x (car (reducible-p1-witness x))))
 
2305
                (:instance 
 
2306
                 unit-p1-=-unit-pp
 
2307
                 (x (mv-nth 1 (reducible-p1-witness x))))))))
 
2308
 
 
2309
(defthm
 
2310
  Reducible-pp-implies-reducible-p1
 
2311
  (implies (reducible-pp x)
 
2312
           (reducible-p1 x))
 
2313
  :rule-classes nil
 
2314
  :hints (("Goal"
 
2315
           :in-theory (disable unit-p1 unit-pp
 
2316
                               (:definition reducible-p1))
 
2317
          :use ((:instance
 
2318
                 Reducible-p1-suff-3
 
2319
                 (y (car (reducible-pp-witness x)))
 
2320
                 (z (mv-nth 1 (reducible-pp-witness x))))))))
 
2321
 
 
2322
(defthm
 
2323
  Reducible-p1-=-reducible-pp
 
2324
  (equal (reducible-p1 x)
 
2325
         (reducible-pp x))
 
2326
  :rule-classes nil
 
2327
  :hints (("Goal"
 
2328
           :in-theory (disable reducible-p1
 
2329
                               reducible-pp)
 
2330
           :use (Reducible-p1-implies-reducible-pp
 
2331
                 Reducible-pp-implies-reducible-p1))))
 
2332
 
 
2333
(defthm
 
2334
  Reducible-p-=-reducible-pp
 
2335
  (equal (reducible-p x)
 
2336
         (reducible-pp x))
 
2337
  :rule-classes nil
 
2338
  :hints (("Goal"
 
2339
           :use (Reducible-p1-=-reducible-pp
 
2340
                 Reducible-p-=-reducible-p1))))
 
2341
 
 
2342
(defthm
 
2343
  Reducible-pp-edp
 
2344
  (implies (reducible-pp x)
 
2345
           (edp x))
 
2346
  :rule-classes :forward-chaining
 
2347
  :hints (("Goal"
 
2348
           :use (:instance 
 
2349
                 closure-laws-for-++_e-&-**_e
 
2350
                 (x (mv-nth 0 (reducible-pp-witness x)))
 
2351
                 (y (mv-nth 1 (reducible-pp-witness x)))))))
 
2352
 
 
2353
(defthm
 
2354
  Reducible-pp-0_e
 
2355
  (implies (and (not (==_e x (0_e)))
 
2356
                (edp x))
 
2357
           (reducible-pp (0_e)))
 
2358
  :hints (("Goal"
 
2359
           :in-theory (disable (:definition unit-pp)
 
2360
                               (:definition reducible-pp))
 
2361
           :use (:instance
 
2362
                 reducible-pp-suff
 
2363
                 (x (0_e))
 
2364
                 (y (0_e))
 
2365
                 (z (0_e))))))
 
2366
 
 
2367
(defthm
 
2368
  Unit-pp-not-reducible-pp
 
2369
  (implies (unit-pp x)
 
2370
           (not (reducible-pp x)))
 
2371
  :hints (("Goal"
 
2372
           :in-theory (disable (:definition unit-pp))
 
2373
           :use (:instance
 
2374
                 unit-pp-**_e=>unit-pp-factor-left
 
2375
                 (x (mv-nth 0 (reducible-pp-witness x)))
 
2376
                 (y (mv-nth 1 (reducible-pp-witness x)))))))
 
2377
 
 
2378
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2379
;; Now, define Irreducible-p so that some form of unique
 
2380
;; factorization (into irreducible elements) can be
 
2381
;; proved for Euclidean Domains.
 
2382
 
 
2383
;;  Clearly (0_e) can be factored in many ways, if the
 
2384
;;   Euclidean Domain is not trivial (that is, if the
 
2385
;;   domain contains at least two distinct elements). 
 
2386
;;  Also any factorization of (0_e) must contain at
 
2387
;;   least one (0_e).
 
2388
 
 
2389
;;  Also units can be factored in many ways. For example
 
2390
;;   (-_e (1_e)) = (*_e (-_e (1_e))(-_e (1_e))(-_e (1_e))) 
 
2391
;;               = (*_e (-_e (1_e))(-_e (1_e))(-_e (1_e))
 
2392
;;                                 (-_e (1_e))(-_e (1_e)))
 
2393
;;  Unique factorization should at least imply that any two
 
2394
;;   factorizations contain the same number of factors. 
 
2395
 
 
2396
;; Irreducible elements are non-zero, non-unit, non-reducible
 
2397
;;  elements of the domain.
 
2398
 
 
2399
(defun
 
2400
  Irreducible-p (x)
 
2401
  (and (edp x)
 
2402
       (not (unit-p x))
 
2403
       (not (reducible-p x))))
 
2404
 
 
2405
(in-theory (disable (:executable-counterpart irreducible-p)))
 
2406
 
 
2407
(defun
 
2408
  Irreducible-pp (x)
 
2409
  (and (edp x)
 
2410
       (not (unit-pp x))
 
2411
       (not (reducible-pp x))))
 
2412
 
 
2413
(in-theory (disable (:executable-counterpart irreducible-pp)))
 
2414
 
 
2415
(defthm
 
2416
  ==_e-implies-equal-irreducible-pp
 
2417
  (implies (==_e y1 y2)
 
2418
           (equal (irreducible-pp y1)
 
2419
                  (irreducible-pp y2)))
 
2420
  :rule-classes :congruence)
 
2421
 
 
2422
(defthm
 
2423
  Irreducible-p-=-irreducible-pp
 
2424
  (equal (irreducible-p x)
 
2425
         (irreducible-pp x))
 
2426
  :rule-classes nil
 
2427
  :hints (("Goal"
 
2428
           :in-theory (disable (:definition reducible-p)
 
2429
                               (:definition reducible-pp)
 
2430
                               (:definition unit-p)
 
2431
                               (:definition unit-pp))
 
2432
           :use (Unit-p-=-Unit-pp
 
2433
                 Reducible-p-=-reducible-pp))))
 
2434
 
 
2435
(defthm
 
2436
  Irreducible-pp-not-0_e
 
2437
  (implies (irreducible-pp x)
 
2438
           (not (==_e x (0_e))))
 
2439
  :rule-classes :forward-chaining
 
2440
  :hints (("Goal"
 
2441
           :in-theory (disable (:definition reducible-pp)
 
2442
                               (:definition unit-pp))
 
2443
           :use Unit-pp-0_e)))
 
2444
 
 
2445
(defthm
 
2446
  Irreducible-pp-implies-unit-pp-factor
 
2447
  (implies (and (irreducible-pp x)
 
2448
                (edp y)
 
2449
                (edp z)
 
2450
                (==_e (**_e y z) x))
 
2451
           (or (unit-pp y)
 
2452
               (unit-pp z)))
 
2453
  :rule-classes ((:rewrite
 
2454
                  :corollary
 
2455
                  (and (implies (and (==_e (**_e y z) x)
 
2456
                                     (irreducible-pp x)
 
2457
                                     (not (unit-pp y))
 
2458
                                     (edp y)
 
2459
                                     (edp z))
 
2460
                                (unit-pp z))
 
2461
                       (implies (and (==_e (**_e y z) x)
 
2462
                                     (irreducible-pp x)
 
2463
                                     (not (unit-pp z))
 
2464
                                     (edp y)
 
2465
                                     (edp z))
 
2466
                                (unit-pp y)))))
 
2467
  :hints (("Goal"
 
2468
           :use reducible-pp-suff)))
 
2469
 
 
2470
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2471
;; Factorization existence theory:
 
2472
 
 
2473
(defun
 
2474
  Irreducible-factors-1 (x)
 
2475
  "Return a list, lst, of irreducible
 
2476
   elements of edp, so that if x is 
 
2477
   in edp, x is not ==_e to 0_e, and x
 
2478
   is not an unit, then x ==_e product
 
2479
   of the members in lst."
 
2480
  (declare (xargs :measure (if (and (edp x)
 
2481
                                    (not (==_e x (0_e))))
 
2482
                               (Size x)
 
2483
                               0)
 
2484
                  :hints (("subgoal 2"
 
2485
                           :in-theory (disable (:definition mv-nth)
 
2486
                                               reducible-pp-edp)
 
2487
                           :use (:instance
 
2488
                                 size-<-size-**_e
 
2489
                                 (x (mv-nth 1 (reducible-pp-witness x)))
 
2490
                                 (y (mv-nth 0 (reducible-pp-witness x)))))
 
2491
                          ("subgoal 1"
 
2492
                           :in-theory (disable (:definition mv-nth)
 
2493
                                               reducible-pp-edp)
 
2494
                           :use (:instance
 
2495
                                 size-<-size-**_e
 
2496
                                 (x (mv-nth 0 (reducible-pp-witness x)))
 
2497
                                 (y (mv-nth 1 (reducible-pp-witness x))))))))
 
2498
  (cond ((or (not (edp x))
 
2499
             (==_e x (0_e))
 
2500
             (equal (Size x)
 
2501
                    (Size (1_e))))
 
2502
         nil)
 
2503
        ((reducible-pp x)
 
2504
         (mv-let (y z)
 
2505
                 (reducible-pp-witness x)
 
2506
                 (append (irreducible-factors-1 y)
 
2507
                         (irreducible-factors-1 z))))
 
2508
        (t (list x))))
 
2509
 
 
2510
(in-theory (disable (:executable-counterpart irreducible-factors-1)))
 
2511
 
 
2512
(defthm
 
2513
  Size-<-size-*_e
 
2514
  (implies (and (not (unit-p y))
 
2515
                (edp x)
 
2516
                (not (=_e x (0_e)))
 
2517
                (edp y)
 
2518
                (not (=_e y (0_e))))
 
2519
           (< (size x) (size (*_e x y))))
 
2520
  :rule-classes nil
 
2521
  :hints (("goal" 
 
2522
           :in-theory (e/d ((:definition ==_e)
 
2523
                            (:definition binary-**_e))
 
2524
                           ((:definition unit-p)
 
2525
                            (:definition unit-pp)))
 
2526
           :use (size-<-size-**_e
 
2527
                 unit-p-=-unit-pp
 
2528
                 (:instance
 
2529
                  unit-p-=-unit-pp
 
2530
                  (x y))))))
 
2531
 
 
2532
(defun
 
2533
  Irreducible-factors (x)
 
2534
  "Return a list, lst, of irreducible
 
2535
   elements of edp, so that if x is 
 
2536
   in edp, x is not =_e to 0_e, and x
 
2537
   is not an unit, then x =_e product
 
2538
   of the members in lst."
 
2539
  (declare (xargs :measure (if (and (edp x)
 
2540
                                    (not (=_e x (0_e))))
 
2541
                               (Size x)
 
2542
                               0)
 
2543
                  :hints (("subgoal 2"
 
2544
                           :in-theory (disable (:definition mv-nth)
 
2545
                                               (:definition unit-p)
 
2546
                                               Zero-Divisor-Law)
 
2547
                           :use ((:instance
 
2548
                                  equivalence-law
 
2549
                                  (y (*_e (mv-nth 0 (reducible-p-witness x))
 
2550
                                          (mv-nth 1 (reducible-p-witness x))))
 
2551
                                  (z (0_e)))
 
2552
                                 (:instance
 
2553
                                  Zero-Divisor-Law
 
2554
                                  (x (mv-nth 0 (reducible-p-witness x)))
 
2555
                                  (y (mv-nth 1 (reducible-p-witness x))))
 
2556
                                 (:instance
 
2557
                                  size-<-size-*_e
 
2558
                                  (x (mv-nth 1 (reducible-p-witness x)))
 
2559
                                  (y (mv-nth 0 (reducible-p-witness x))))
 
2560
                                 (:instance
 
2561
                                  Congruence-for-Size
 
2562
                                  (y1 (*_e (mv-nth 0 (reducible-p-witness x))
 
2563
                                           (mv-nth 1 (reducible-p-witness x))))
 
2564
                                  (y2 (*_e (mv-nth 1 (reducible-p-witness x))
 
2565
                                           (mv-nth 0 (reducible-p-witness x)))))
 
2566
                                 (:instance
 
2567
                                  Congruence-for-Size
 
2568
                                  (y1 (*_e (mv-nth 0 (reducible-p-witness x))
 
2569
                                           (mv-nth 1 (reducible-p-witness x))))
 
2570
                                  (y2 x))))
 
2571
                          ("subgoal 1"
 
2572
                           :in-theory (disable (:definition mv-nth)
 
2573
                                               (:definition unit-p)
 
2574
                                               Zero-Divisor-Law)
 
2575
                           :use ((:instance
 
2576
                                  equivalence-law
 
2577
                                  (y (*_e (mv-nth 0 (reducible-p-witness x))
 
2578
                                          (mv-nth 1 (reducible-p-witness x))))
 
2579
                                  (z (0_e)))
 
2580
                                 (:instance
 
2581
                                  Zero-Divisor-Law
 
2582
                                  (x (mv-nth 0 (reducible-p-witness x)))
 
2583
                                  (y (mv-nth 1 (reducible-p-witness x))))
 
2584
                                 (:instance
 
2585
                                  size-<-size-*_e
 
2586
                                  (x (mv-nth 0 (reducible-p-witness x)))
 
2587
                                  (y (mv-nth 1 (reducible-p-witness x))))
 
2588
                                 (:instance
 
2589
                                  Congruence-for-Size
 
2590
                                  (y1 (*_e (mv-nth 0 (reducible-p-witness x))
 
2591
                                           (mv-nth 1 (reducible-p-witness x))))
 
2592
                                  (y2 x)))))))
 
2593
  (cond ((or (not (edp x))
 
2594
             (=_e x (0_e))
 
2595
             (equal (Size x)
 
2596
                    (Size (1_e))))
 
2597
         nil)
 
2598
        ((reducible-p x)
 
2599
         (mv-let (y z)
 
2600
                 (reducible-p-witness x)
 
2601
                 (append (irreducible-factors y)
 
2602
                         (irreducible-factors z))))
 
2603
        (t (list x))))
 
2604
 
 
2605
; No longer needed after v3-6-1 (essentially part of axioms.lisp):
 
2606
; (defthm
 
2607
;   True-listp-append
 
2608
;   (implies (true-listp lst2)
 
2609
;            (true-listp (append lst1 lst2)))
 
2610
;   :rule-classes :type-prescription)
 
2611
 
 
2612
(defthm
 
2613
  True-listp-irreducible-factors-1
 
2614
  (true-listp (irreducible-factors-1 x))
 
2615
  :rule-classes :type-prescription
 
2616
  :hints (("Goal"
 
2617
           :in-theory (disable (:definition unit-pp)
 
2618
                               (:definition reducible-pp)))))
 
2619
 
 
2620
(defthm
 
2621
  True-listp-irreducible-factors
 
2622
  (true-listp (irreducible-factors x))
 
2623
  :rule-classes :type-prescription
 
2624
  :hints (("Goal"
 
2625
           :in-theory (disable (:definition unit-p)
 
2626
                               (:definition reducible-p)))))
 
2627
 
 
2628
(defun
 
2629
  Irreducible-listp-1 (lst)
 
2630
  (if (consp lst)
 
2631
      (and (irreducible-pp (car lst))
 
2632
           (irreducible-listp-1 (cdr lst)))
 
2633
      t))
 
2634
 
 
2635
(defun
 
2636
  Irreducible-listp (lst)
 
2637
  (if (consp lst)
 
2638
      (and (irreducible-p (car lst))
 
2639
           (irreducible-listp (cdr lst)))
 
2640
      t))
 
2641
 
 
2642
(defthm
 
2643
  Irreducible-listp-1-append
 
2644
  (implies (and (irreducible-listp-1 lst1)
 
2645
                (irreducible-listp-1 lst2))
 
2646
           (irreducible-listp-1 (append lst1 lst2)))
 
2647
  :hints (("goal"
 
2648
           :in-theory (disable (:definition irreducible-pp)))))
 
2649
 
 
2650
(defthm
 
2651
  Irreducible-listp-append
 
2652
  (implies (and (irreducible-listp lst1)
 
2653
                (irreducible-listp lst2))
 
2654
           (irreducible-listp (append lst1 lst2)))
 
2655
  :hints (("goal"
 
2656
           :in-theory (disable (:definition irreducible-p)))))
 
2657
 
 
2658
(defthm
 
2659
  Size-implies-irreducible-pp
 
2660
  (implies (and (edp x)
 
2661
                (not (equal (size x)
 
2662
                            (size (1_e))))
 
2663
                (not (reducible-pp x)))
 
2664
           (irreducible-pp x))
 
2665
  :hints (("Goal"
 
2666
           :in-theory (disable (:definition reducible-pp)
 
2667
                               (:definition unit-pp))
 
2668
           :use Size-unit-pp=Size-1_e)))
 
2669
 
 
2670
(defthm
 
2671
  Size-implies-irreducible-p
 
2672
  (implies (and (edp x)
 
2673
                (not (equal (size x)
 
2674
                            (size (1_e))))
 
2675
                (not (reducible-p x)))
 
2676
           (irreducible-p x))
 
2677
  :hints (("Goal"
 
2678
           :in-theory (disable (:definition reducible-p)
 
2679
                               (:definition unit-p))
 
2680
           :use Size-unit-p=Size-1_e)))
 
2681
 
 
2682
(defthm
 
2683
  Irreducible-listp-1-irreducible-factors-1
 
2684
  (irreducible-listp-1 (irreducible-factors-1 x))
 
2685
  :hints (("Goal"
 
2686
           :in-theory (disable (:definition reducible-pp)
 
2687
                               (:definition unit-pp)))))
 
2688
 
 
2689
(defthm
 
2690
  Irreducible-listp-irreducible-factors
 
2691
  (irreducible-listp (irreducible-factors x))
 
2692
  :hints (("Goal"
 
2693
           :in-theory (disable (:definition reducible-p)
 
2694
                               (:definition unit-p)))))
 
2695
 
 
2696
(defun
 
2697
  Edp-listp (lst)
 
2698
  (if (consp lst)
 
2699
      (and (edp (car lst))
 
2700
           (edp-listp (cdr lst)))
 
2701
      t))
 
2702
 
 
2703
(defthm
 
2704
  Irreducible-listp-1-implies-edp-listp
 
2705
  (implies (irreducible-listp-1 lst)
 
2706
           (edp-listp lst)))
 
2707
 
 
2708
(defthm
 
2709
  Irreducible-listp-implies-edp-listp
 
2710
  (implies (irreducible-listp lst)
 
2711
           (edp-listp lst)))
 
2712
 
 
2713
(defthm
 
2714
  Edp-listp-irreducible-factors-1
 
2715
  (edp-listp (irreducible-factors-1 x)))
 
2716
 
 
2717
(defthm
 
2718
  Edp-listp-irreducible-factors
 
2719
  (edp-listp (irreducible-factors x)))
 
2720
 
 
2721
(defun
 
2722
  **_e-lst (lst)
 
2723
  (if (consp lst)
 
2724
      (if (edp (car lst))
 
2725
          (**_e (car lst)(**_e-lst (cdr lst)))
 
2726
          (0_e))
 
2727
      (1_e)))
 
2728
 
 
2729
(in-theory (disable (:executable-counterpart **_e-lst)))
 
2730
 
 
2731
(defun
 
2732
  *_e-lst (lst)
 
2733
  (if (consp lst)
 
2734
      (if (edp (car lst))
 
2735
          (*_e (car lst)(*_e-lst (cdr lst)))
 
2736
          (0_e))
 
2737
      (1_e)))
 
2738
 
 
2739
(in-theory (disable (:executable-counterpart *_e-lst)))
 
2740
 
 
2741
(defthm
 
2742
  Edp-**_e-lst
 
2743
  (edp (**_e-lst lst)))
 
2744
 
 
2745
(defthm
 
2746
  Edp-*_e-lst
 
2747
  (edp (*_e-lst lst)))
 
2748
 
 
2749
(defthm
 
2750
  **_e-lst-append
 
2751
  (==_e (**_e-lst (append lst1 lst2))
 
2752
        (**_e (**_e-lst lst1)
 
2753
              (**_e-lst lst2))))
 
2754
 
 
2755
(defthm
 
2756
  *_e-lst-=-**_e-lst
 
2757
  (equal (*_e-lst lst)
 
2758
         (**_e-lst lst))
 
2759
  :rule-classes nil
 
2760
  :hints (("Subgoal *1/1"
 
2761
           :in-theory (enable (:definition binary-**_e)))))
 
2762
 
 
2763
(defthm
 
2764
  *_e-lst-append
 
2765
  (=_e (*_e-lst (append lst1 lst2))
 
2766
       (*_e (*_e-lst lst1)
 
2767
            (*_e-lst lst2)))
 
2768
  :hints (("Goal"
 
2769
           :in-theory (e/d ((:definition ==_e)
 
2770
                            (:definition binary-**_e))
 
2771
                           (**_e-lst-append))
 
2772
           :use (**_e-lst-append
 
2773
                 (:instance
 
2774
                  *_e-lst-=-**_e-lst
 
2775
                  (lst (append lst1 lst2)))
 
2776
                 (:instance
 
2777
                  *_e-lst-=-**_e-lst
 
2778
                  (lst lst1))
 
2779
                 (:instance
 
2780
                  *_e-lst-=-**_e-lst
 
2781
                  (lst lst2))))))
 
2782
 
 
2783
(defthm
 
2784
  **_e-lst-irreducible-factors-1
 
2785
  (implies (and (edp x)
 
2786
                (not (==_e x (0_e)))
 
2787
                (not (unit-pp x)))
 
2788
           (==_e (**_e-lst (irreducible-factors-1 x)) x))
 
2789
  :hints (("Goal"
 
2790
           :in-theory (disable (:definition mv-nth)
 
2791
                               (:definition unit-pp)
 
2792
 
 
2793
; The authors want unit-pp to stay in the problem.  But the enabled rewrite rule
 
2794
; (DEFTHM UNIT-PP-NOT-REDUCIBLE-PP
 
2795
;  (IMPLIES (UNIT-PP X)
 
2796
;           (NOT (REDUCIBLE-PP X))))
 
2797
; is also a tau rule that removes unit-pp given the earlier assumption of
 
2798
; (reducible-pp x).  So we must ensure that the tau-system is disabled.
 
2799
 
 
2800
                               (:executable-counterpart tau-system)
 
2801
                               ))))
 
2802
 
 
2803
(defthm
 
2804
  Right-unicity-law-for-*_e
 
2805
  (implies (edp x)
 
2806
           (=_e (*_e x (1_e)) x))
 
2807
  :hints (("Goal"
 
2808
           :in-theory (disable Left-Unicity-Laws
 
2809
                               Equivalence-law)
 
2810
           :use (Left-Unicity-Laws
 
2811
                 (:instance
 
2812
                  Equivalence-law
 
2813
                  (x (*_e x (1_e)))
 
2814
                  (y (*_e (1_e) x))
 
2815
                  (z x))))))
 
2816
 
 
2817
(defthm
 
2818
  *_e-congruence
 
2819
  (implies (and (edp x1)
 
2820
                (edp x2)
 
2821
                (edp y1)
 
2822
                (edp y2)
 
2823
                (=_e x1 x2)
 
2824
                (=_e y1 y2))
 
2825
           (=_e (*_e x1 y1)
 
2826
                (*_e x2 y2)))
 
2827
  :rule-classes nil
 
2828
  :hints (("Goal"
 
2829
           :use ((:instance
 
2830
                  Congruence-laws
 
2831
                  (y1 x1)
 
2832
                  (y2 x2)
 
2833
                  (z y1))
 
2834
                 (:instance
 
2835
                  Congruence-laws
 
2836
                  (x x2))
 
2837
                 (:instance
 
2838
                  Equivalence-law
 
2839
                  (x (*_e x1 y1))
 
2840
                  (y (*_e x2 y1))
 
2841
                  (z (*_e x2 y2)))))))
 
2842
 
 
2843
(defthm
 
2844
  *_e-lst-irreducible-factors
 
2845
  (implies (and (edp x)
 
2846
                (not (=_e x (0_e)))
 
2847
                (not (unit-p x)))
 
2848
           (=_e (*_e-lst (irreducible-factors x)) x))
 
2849
  :hints (("Goal"
 
2850
           :do-not generalize
 
2851
           :in-theory (disable (:definition mv-nth)
 
2852
                               (:definition unit-p)))
 
2853
          ("Subgoal *1/17"
 
2854
           :in-theory (disable (:definition mv-nth)
 
2855
                               (:definition unit-p)
 
2856
                               Equivalence-law)
 
2857
           :use ((:instance
 
2858
                  *_e-congruence
 
2859
                  (x1 (*_e-lst (irreducible-factors 
 
2860
                                (mv-nth 0 (reducible-p-witness x)))))
 
2861
                  (x2 (mv-nth 0 (reducible-p-witness x)))
 
2862
                  (y1 (*_e-lst (irreducible-factors 
 
2863
                                (mv-nth 1 (reducible-p-witness x)))))
 
2864
                  (y2 (mv-nth 1 (reducible-p-witness x))))
 
2865
                 (:instance
 
2866
                  equivalence-law
 
2867
                  (x (*_e-lst (append (irreducible-factors 
 
2868
                                       (mv-nth 0 (reducible-p-witness x)))
 
2869
                                      (irreducible-factors 
 
2870
                                       (mv-nth 1 (reducible-p-witness x))))))
 
2871
                  (y (*_e (*_e-lst (irreducible-factors 
 
2872
                                    (mv-nth 0 (reducible-p-witness x))))
 
2873
                          (*_e-lst (irreducible-factors 
 
2874
                                    (mv-nth 1 (reducible-p-witness x))))))
 
2875
                  (z (*_e (mv-nth 0 (reducible-p-witness x))
 
2876
                          (mv-nth 1 (reducible-p-witness x)))))
 
2877
                 (:instance
 
2878
                  equivalence-law
 
2879
                  (x (*_e-lst (append (irreducible-factors 
 
2880
                                       (mv-nth 0 (reducible-p-witness x)))
 
2881
                                      (irreducible-factors 
 
2882
                                       (mv-nth 1 (reducible-p-witness x))))))
 
2883
                  (y (*_e (mv-nth 0 (reducible-p-witness x))
 
2884
                          (mv-nth 1 (reducible-p-witness x))))
 
2885
                  (z x))))
 
2886
          ("subgoal *1/15"
 
2887
           :use (:instance
 
2888
                 (:theorem
 
2889
                  (implies (and (edp x)
 
2890
                                (edp y)
 
2891
                                (edp z)
 
2892
                                (=_e x y)
 
2893
                                (=_e x z))
 
2894
                           (=_e y z)))
 
2895
                 (x (*_e (mv-nth 0 (reducible-p-witness x))
 
2896
                         (mv-nth 1 (reducible-p-witness x))))
 
2897
                 (y x)
 
2898
                 (z (0_e))))
 
2899
          ("subgoal *1/9"
 
2900
           :use (:instance
 
2901
                 (:theorem
 
2902
                  (implies (and (edp x)
 
2903
                                (edp y)
 
2904
                                (edp z)
 
2905
                                (=_e x y)
 
2906
                                (=_e x z))
 
2907
                           (=_e y z)))
 
2908
                 (x (*_e (mv-nth 0 (reducible-p-witness x))
 
2909
                         (mv-nth 1 (reducible-p-witness x))))
 
2910
                 (y x)
 
2911
                 (z (0_e))))
 
2912
          ("subgoal *1/7"
 
2913
           :use (:instance
 
2914
                 (:theorem
 
2915
                  (implies (and (edp x)
 
2916
                                (edp y)
 
2917
                                (edp z)
 
2918
                                (=_e x y)
 
2919
                                (=_e x z))
 
2920
                           (=_e y z)))
 
2921
                 (x (*_e (mv-nth 0 (reducible-p-witness x))
 
2922
                         (mv-nth 1 (reducible-p-witness x))))
 
2923
                 (y x)
 
2924
                 (z (0_e))))))
 
2925
 
 
2926
(defthm
 
2927
  IRREDUCIBLE-FACTORIZATION-EXISTENCE
 
2928
  (and (true-listp (irreducible-factors x))
 
2929
       (edp-listp  (irreducible-factors x))
 
2930
       (irreducible-listp (irreducible-factors x))
 
2931
       (implies (and (edp x)
 
2932
                     (not (=_e x (0_e)))
 
2933
                     (not (unit-p x)))
 
2934
                (=_e (*_e-lst (irreducible-factors x)) x)))
 
2935
  :rule-classes nil
 
2936
  :hints (("Goal"
 
2937
           :in-theory (disable (:definition unit-p)))))
 
2938
 
 
2939
;;;;;;;;;;;;;;
 
2940
;; GCD Theory:
 
2941
 
 
2942
;;Determine if g is a gcd of x and y.
 
2943
(defun-sk
 
2944
  gcd-p (x y g)
 
2945
  (forall d (and (divides-p g x)
 
2946
                 (divides-p g y)
 
2947
                 (implies (and (divides-p d x)
 
2948
                               (divides-p d y))
 
2949
                          (divides-p d g)))))
 
2950
 
 
2951
(defun
 
2952
  Gcd-pp-witness (x y g)
 
2953
  "Gcd-pp-witness nicely
 
2954
   modifies Gcd-p-witness."
 
2955
  (gcd-p-witness (C_==_e x)
 
2956
                 (C_==_e y)
 
2957
                 (C_==_e g)))
 
2958
 
 
2959
(defthm
 
2960
  ==_e-implies-==_e-gcd-pp-witness-1
 
2961
  (implies (==_e x1 x2)
 
2962
           (==_e (gcd-pp-witness x1 y g)
 
2963
                 (gcd-pp-witness x2 y g)))
 
2964
  :rule-classes :congruence)
 
2965
 
 
2966
(defthm
 
2967
  ==_e-implies-==_e-gcd-pp-witness-2
 
2968
  (implies (==_e y1 y2)
 
2969
           (==_e (gcd-pp-witness x y1 g)
 
2970
                 (gcd-pp-witness x y2 g)))
 
2971
  :rule-classes :congruence)
 
2972
 
 
2973
(defthm
 
2974
  ==_e-implies-==_e-gcd-pp-witness-3
 
2975
  (implies (==_e g1 g2)
 
2976
           (==_e (gcd-pp-witness x y g1)
 
2977
                 (gcd-pp-witness x y g2)))
 
2978
  :rule-classes :congruence)
 
2979
 
 
2980
(defun
 
2981
  Gcd-pp (x y g)
 
2982
  (let ((d (gcd-pp-witness x y g)))
 
2983
       (and (divides-pp g x)
 
2984
            (divides-pp g y)
 
2985
            (implies (and (divides-pp d x)
 
2986
                          (divides-pp d y))
 
2987
                     (divides-pp d g)))))
 
2988
 
 
2989
(defthm
 
2990
  ==_e-implies-equal-gcd-pp-1
 
2991
  (implies (==_e x1 x2)
 
2992
           (equal (gcd-pp x1 y g)
 
2993
                  (gcd-pp x2 y g)))
 
2994
  :rule-classes :congruence)
 
2995
 
 
2996
(defthm
 
2997
  ==_e-implies-equal-gcd-pp-2
 
2998
  (implies (==_e y1 y2)
 
2999
           (equal (gcd-pp x y1 g)
 
3000
                  (gcd-pp x y2 g)))
 
3001
  :rule-classes :congruence)
 
3002
 
 
3003
(defthm
 
3004
  ==_e-implies-equal-gcd-pp-3
 
3005
  (implies (==_e g1 g2)
 
3006
           (equal (gcd-pp x y g1)
 
3007
                  (gcd-pp x y g2)))
 
3008
  :rule-classes :congruence)
 
3009
 
 
3010
(defthm
 
3011
  Gcd-p-necc-1
 
3012
  (implies (not (and (divides-pp g x)
 
3013
                     (divides-pp g y)
 
3014
                     (implies (and (divides-pp d x)
 
3015
                                   (divides-pp d y))
 
3016
                              (divides-pp d g))))
 
3017
           (not (gcd-p x y g)))
 
3018
  :hints (("Goal"
 
3019
           :in-theory (disable (:definition divides-p)
 
3020
                               (:definition divides-pp)
 
3021
                               (:definition gcd-p))
 
3022
           :use (gcd-p-necc
 
3023
                 (:instance
 
3024
                  divides-p-=-divides-pp
 
3025
                  (x g)
 
3026
                  (y x))
 
3027
                 (:instance
 
3028
                  divides-p-=-divides-pp
 
3029
                  (x g))
 
3030
                 (:instance
 
3031
                  divides-p-=-divides-pp
 
3032
                  (x d)
 
3033
                  (y x))
 
3034
                 (:instance
 
3035
                  divides-p-=-divides-pp
 
3036
                  (x d))
 
3037
                 (:instance
 
3038
                  divides-p-=-divides-pp
 
3039
                  (x d)
 
3040
                  (y g))))))
 
3041
 
 
3042
(defthm
 
3043
  Gcd-pp-necc-lemma-1
 
3044
  (implies (not (and (divides-pp g x)
 
3045
                     (divides-pp g y)
 
3046
                     (implies (and (divides-pp d x)
 
3047
                                   (divides-pp d y))
 
3048
                              (divides-pp d g))))
 
3049
           (not (and (divides-p (C_==_e g)(C_==_e x))
 
3050
                     (divides-p (C_==_e g)(C_==_e y))
 
3051
                     (implies (and (divides-p (gcd-p-witness (C_==_e x)
 
3052
                                                             (C_==_e y)
 
3053
                                                             (C_==_e g)) 
 
3054
                                              (C_==_e x)) 
 
3055
                                   (divides-p (gcd-p-witness (C_==_e x)
 
3056
                                                             (C_==_e y)
 
3057
                                                             (C_==_e g))
 
3058
                                              (C_==_e y)))
 
3059
                              (divides-p (gcd-p-witness (C_==_e x)
 
3060
                                                        (C_==_e y)
 
3061
                                                        (C_==_e g))
 
3062
                                         (C_==_e g))))))
 
3063
  :rule-classes nil
 
3064
  :hints (("Goal"
 
3065
           :in-theory (disable (:definition divides-p)
 
3066
                               (:definition divides-pp))
 
3067
           :use (:instance
 
3068
                 gcd-p-necc-1
 
3069
                 (x (C_==_e x))
 
3070
                 (y (C_==_e y))
 
3071
                 (g (C_==_e g))))))
 
3072
 
 
3073
(defthm
 
3074
  Gcd-pp-necc-lemma-2
 
3075
  (implies (not (and (divides-p (C_==_e g)(C_==_e x))
 
3076
                     (divides-p (C_==_e g)(C_==_e y))
 
3077
                     (implies (and (divides-p (gcd-p-witness (C_==_e x)
 
3078
                                                             (C_==_e y)
 
3079
                                                             (C_==_e g)) 
 
3080
                                              (C_==_e x)) 
 
3081
                                   (divides-p (gcd-p-witness (C_==_e x)
 
3082
                                                             (C_==_e y)
 
3083
                                                             (C_==_e g))
 
3084
                                              (C_==_e y)))
 
3085
                              (divides-p (gcd-p-witness (C_==_e x)
 
3086
                                                        (C_==_e y)
 
3087
                                                        (C_==_e g))
 
3088
                                         (C_==_e g)))))
 
3089
           (not (and (divides-pp g x)
 
3090
                     (divides-pp g y)
 
3091
                     (implies (and (divides-pp (gcd-pp-witness x
 
3092
                                                               y
 
3093
                                                               g) 
 
3094
                                               x) 
 
3095
                                   (divides-pp (gcd-pp-witness x
 
3096
                                                               y
 
3097
                                                               g)
 
3098
                                               y))
 
3099
                              (divides-pp (gcd-pp-witness x
 
3100
                                                          y
 
3101
                                                          g)
 
3102
                                          g)))))
 
3103
  :rule-classes nil
 
3104
  :hints (("Goal"
 
3105
          :in-theory (disable (:definition divides-p)
 
3106
                              (:definition divides-pp))
 
3107
          :use ((:instance
 
3108
                 divides-p-=-divides-pp
 
3109
                 (x (C_==_e g))
 
3110
                 (y (C_==_e x)))
 
3111
                (:instance
 
3112
                 divides-p-=-divides-pp
 
3113
                 (x (C_==_e g))
 
3114
                 (y (C_==_e y)))
 
3115
                (:instance
 
3116
                 divides-p-=-divides-pp
 
3117
                 (x (gcd-p-witness (C_==_e x)
 
3118
                                   (C_==_e y)
 
3119
                                   (C_==_e g))) 
 
3120
                 (y (C_==_e x)))
 
3121
                (:instance
 
3122
                 divides-p-=-divides-pp
 
3123
                 (x (gcd-p-witness (C_==_e x)
 
3124
                                   (C_==_e y)
 
3125
                                   (C_==_e g))) 
 
3126
                 (y (C_==_e y)))
 
3127
                (:instance
 
3128
                 divides-p-=-divides-pp
 
3129
                 (x (gcd-p-witness (C_==_e x)
 
3130
                                   (C_==_e y)
 
3131
                                   (C_==_e g))) 
 
3132
                 (y (C_==_e g)))))))
 
3133
        
 
3134
(defthm
 
3135
  Gcd-pp-necc
 
3136
  (implies (not (and (divides-pp g x)
 
3137
                     (divides-pp g y)
 
3138
                     (implies (and (divides-pp d x)
 
3139
                                   (divides-pp d y))
 
3140
                              (divides-pp d g))))
 
3141
           (not (gcd-pp x y g)))
 
3142
  :hints (("Goal"
 
3143
           :in-theory (disable (:definition divides-pp)
 
3144
                               (:definition divides-p)
 
3145
                               (:definition gcd-pp-witness))
 
3146
           :use (Gcd-pp-necc-lemma-1
 
3147
                 Gcd-pp-necc-lemma-2))))
 
3148
 
 
3149
(in-theory (disable (:definition gcd-pp-witness)
 
3150
                    (:executable-counterpart gcd-pp)))
 
3151
           
 
3152
(defthm
 
3153
  Gcd-p-implies-gcd-pp
 
3154
  (implies (gcd-p x y g)
 
3155
           (gcd-pp x y g))
 
3156
  :rule-classes nil
 
3157
  :hints (("Goal"
 
3158
           :in-theory (disable (:definition divides-pp)
 
3159
                               (:definition gcd-p))
 
3160
           :use (:instance
 
3161
                 Gcd-p-necc-1
 
3162
                 (d (gcd-pp-witness x y g))))))
 
3163
 
 
3164
(defthm
 
3165
  Gcd-pp-implies-gcd-p
 
3166
  (implies (gcd-pp x y g)
 
3167
           (gcd-p x y g))
 
3168
  :rule-classes nil
 
3169
  :hints (("Goal"
 
3170
           :in-theory (disable (:definition divides-p)
 
3171
                               (:definition divides-pp)
 
3172
                               (:definition gcd-pp))
 
3173
           :use ((:instance
 
3174
                  Gcd-pp-necc
 
3175
                  (d (gcd-p-witness x y g)))
 
3176
                 (:instance
 
3177
                  divides-p-=-divides-pp
 
3178
                  (x g)
 
3179
                  (y x))
 
3180
                 (:instance
 
3181
                  divides-p-=-divides-pp
 
3182
                  (x g))
 
3183
                 (:instance
 
3184
                  divides-p-=-divides-pp
 
3185
                  (x (gcd-p-witness x y g))
 
3186
                  (y g))
 
3187
                 (:instance
 
3188
                  divides-p-=-divides-pp
 
3189
                  (x (gcd-p-witness x y g))
 
3190
                  (y x))
 
3191
                 (:instance
 
3192
                  divides-p-=-divides-pp
 
3193
                  (x (gcd-p-witness x y g)))))))
 
3194
 
 
3195
(defthm
 
3196
  Gcd-p-=-gcd-pp
 
3197
  (equal (gcd-p x y g)
 
3198
         (gcd-pp x y g))
 
3199
  :rule-classes nil
 
3200
  :hints (("Goal"
 
3201
           :in-theory (disable (:definition gcd-p)
 
3202
                               (:definition gcd-pp))
 
3203
           :use (Gcd-p-implies-gcd-pp
 
3204
                 Gcd-pp-implies-gcd-p))))
 
3205
 
 
3206
;;For nonzero element x and element y of edp, choose elements
 
3207
;; z0,z1 of edp so that the linear combination x z0 + y z1 is
 
3208
;; a nonzero element and has Size n (if they exists).
 
3209
(defchoose
 
3210
  Bezout1 (z0 z1)(x y n)
 
3211
  (and (edp x)
 
3212
       (not (==_e x (0_e)))
 
3213
       (edp y)
 
3214
       (edp z0)
 
3215
       (edp z1)
 
3216
       (not (==_e (++_e (**_e x z0)
 
3217
                        (**_e y z1))
 
3218
                  (0_e)))
 
3219
       (equal (Size (++_e (**_e x z0)
 
3220
                          (**_e y z1)))
 
3221
              (nfix n))))
 
3222
 
 
3223
(defthm
 
3224
  Bezout1-property
 
3225
  (and (true-listp (Bezout1 x y n))
 
3226
       (implies (and (integerp n)
 
3227
                     (>= n 0)
 
3228
                     (edp x)
 
3229
                     (not (==_e x (0_e)))
 
3230
                     (edp y)
 
3231
                     (edp z0)
 
3232
                     (edp z1)
 
3233
                     (not (==_e (++_e (**_e x z0)
 
3234
                                      (**_e y z1))
 
3235
                                (0_e)))
 
3236
                     (equal (Size (++_e (**_e x z0)
 
3237
                                        (**_e y z1)))
 
3238
                            n))
 
3239
                (and (edp (mv-nth 0 (Bezout1 x y n)))
 
3240
                     (edp (mv-nth 1 (Bezout1 x y n)))
 
3241
                     (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3242
                                      (**_e y (mv-nth 1 (Bezout1 x y n))))
 
3243
                                (0_e)))
 
3244
                     (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3245
                                        (**_e y (mv-nth 1 (Bezout1 x y n)))))
 
3246
                            n))))
 
3247
  :rule-classes ((:rewrite
 
3248
                  :corollary
 
3249
                  (and (true-listp (Bezout1 x y n))
 
3250
                       (implies (and (integerp n)
 
3251
                                     (>= n 0)
 
3252
                                     (edp x)
 
3253
                                     (not (==_e x (0_e)))
 
3254
                                     (edp y)
 
3255
                                     (equal (Size (++_e (**_e x z0)
 
3256
                                                        (**_e y z1)))
 
3257
                                            n)
 
3258
                                     (not (==_e (++_e (**_e x z0)
 
3259
                                                      (**_e y z1))
 
3260
                                                (0_e)))
 
3261
                                     (edp z0)
 
3262
                                     (edp z1))
 
3263
                                (and (edp (mv-nth 0 (Bezout1 x y n)))
 
3264
                                     (edp (mv-nth 1 (Bezout1 x y n)))
 
3265
                                     (not (==_e (++_e (**_e x 
 
3266
                                                            (mv-nth 0
 
3267
                                                                    (Bezout1 x y n)))
 
3268
                                                      (**_e y 
 
3269
                                                           (mv-nth 1
 
3270
                                                                   (Bezout1 x y n))))
 
3271
                                                (0_e)))
 
3272
                                     (equal (Size (++_e (**_e x 
 
3273
                                                              (mv-nth 0 
 
3274
                                                                      (Bezout1 x y n)))
 
3275
                                                        (**_e y 
 
3276
                                                              (mv-nth 1 
 
3277
                                                                      (Bezout1 x y n)))
 
3278
                                                        ))
 
3279
                                            n)))))
 
3280
                 (:type-prescription
 
3281
                  :corollary
 
3282
                  (true-listp (Bezout1 x y n))))
 
3283
  :hints (("Goal"
 
3284
           :use Bezout1)))
 
3285
 
 
3286
(defthm
 
3287
  Bezout1-properties-Size
 
3288
  (implies (and (edp x)
 
3289
                (not (==_e x (0_e)))
 
3290
                (edp y)
 
3291
                (edp z0)
 
3292
                (edp z1)
 
3293
                (not (==_e (++_e (**_e x z0)
 
3294
                                 (**_e y z1))
 
3295
                           (0_e))))
 
3296
           (and (edp (mv-nth 0 (Bezout1 x y (Size (++_e (**_e x z0)
 
3297
                                                        (**_e y z1))))))
 
3298
                (edp (mv-nth 1 (Bezout1 x y (Size (++_e (**_e x z0)
 
3299
                                                        (**_e y z1))))))
 
3300
                (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y (Size (++_e (**_e x z0)
 
3301
                                                                            (**_e y z1))
 
3302
                                                                      ))))
 
3303
                                 (**_e y (mv-nth 1 (Bezout1 x y (Size (++_e (**_e x z0)
 
3304
                                                                            (**_e y z1))
 
3305
                                                                      )))))
 
3306
                           (0_e)))
 
3307
                (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y (Size (++_e (**_e x z0)
 
3308
                                                                              (**_e y z1)
 
3309
                                                                              )))))
 
3310
                                   (**_e y (mv-nth 1 (Bezout1 x y (Size (++_e (**_e x z0)
 
3311
                                                                              (**_e y z1)
 
3312
                                                                              ))))))) 
 
3313
                       (Size (++_e (**_e x z0)
 
3314
                                   (**_e y z1))))))
 
3315
  :hints (("Goal"
 
3316
           :use (:instance
 
3317
                 Bezout1-property
 
3318
                 (n (Size (++_e (**_e x z0)
 
3319
                                (**_e y z1))))))))
 
3320
 
 
3321
(defthm
 
3322
  Bezout1-properties-Size-1_e-0_e
 
3323
  (implies (and (edp x)
 
3324
                (not (==_e x (0_e)))
 
3325
                (edp y))
 
3326
           (and (edp (mv-nth 0 (Bezout1 x y (Size x))))
 
3327
                (edp (mv-nth 1 (Bezout1 x y (Size x))))
 
3328
                (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y (Size x))))
 
3329
                                 (**_e y (mv-nth 1 (Bezout1 x y (Size x)))))
 
3330
                           (0_e)))
 
3331
                (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y (Size x))))
 
3332
                                   (**_e y (mv-nth 1 (Bezout1 x y (Size x)))))) 
 
3333
                       (Size x))))
 
3334
  :hints (("Goal"
 
3335
           :use (:instance
 
3336
                 Bezout1-properties-Size
 
3337
                 (z0 (1_e))
 
3338
                 (z1 (0_e))))))
 
3339
 
 
3340
(defun
 
3341
  Find-smallest-n (x y n)
 
3342
  "Find smallest natp n such that the first two elements 
 
3343
   of the true list (Bezout1 x y n) are in edp, the linear
 
3344
   combination
 
3345
               (++_e (**_e x 
 
3346
                           (mv-nth 0 (Bezout1 x y n)))
 
3347
                     (**_e y 
 
3348
                           (mv-nth 1 (Bezout1 x y n))))
 
3349
   is nonzero, and the size of the linear conbination is n."
 
3350
  (declare (xargs :measure (let ((n (nfix n)))
 
3351
                                    (nfix (- (Size x) n)))))
 
3352
  (if (and (edp x)
 
3353
           (not (==_e x (0_e)))
 
3354
           (edp y))
 
3355
      (let ((n (nfix n)))
 
3356
           (if (and (< n (size x))
 
3357
                    (mv-let (z0 z1)
 
3358
                            (Bezout1 x y n)
 
3359
                            (not (and (edp z0)
 
3360
                                      (edp z1)
 
3361
                                      (not (==_e (++_e (**_e x z0) 
 
3362
                                                       (**_e y z1))
 
3363
                                                 (0_e)))
 
3364
                                      (equal (Size (++_e (**_e x z0)
 
3365
                                                         (**_e y z1)))
 
3366
                                             n)))))
 
3367
               (Find-smallest-n x y (+ n 1))
 
3368
               n))
 
3369
      n))
 
3370
 
 
3371
(in-theory (disable (:executable-counterpart Find-smallest-n)))
 
3372
 
 
3373
(defthm
 
3374
  Integerp-Find-smallest-n
 
3375
  (implies (integerp n)
 
3376
           (integerp (Find-smallest-n x y n)))
 
3377
  :rule-classes :type-prescription)
 
3378
 
 
3379
(defthm
 
3380
  Natp-Find-smallest-n
 
3381
  (implies (and (edp x)
 
3382
                (not (==_e x (0_e)))
 
3383
                (edp y))
 
3384
           (and (integerp (Find-smallest-n x y n))
 
3385
                (>= (Find-smallest-n x y n) 0)))
 
3386
  :rule-classes :type-prescription)
 
3387
 
 
3388
(defthm
 
3389
  Find-smallest-n-Size-x
 
3390
  (implies (<= n (Size x))
 
3391
           (<= (Find-smallest-n x y n)
 
3392
               (Size x))))
 
3393
 
 
3394
(defthm
 
3395
  Bezout1-Find-smallest-n
 
3396
  (implies (and (integerp n)
 
3397
                (<= 0 n)
 
3398
                (<= n (Size x))
 
3399
                (edp x)
 
3400
                (not (==_e x (0_e)))
 
3401
                (edp y))
 
3402
           (and (edp (mv-nth 0 (Bezout1 x y (Find-smallest-n x y n))))
 
3403
                (edp (mv-nth 1 (Bezout1 x y (Find-smallest-n x y n))))
 
3404
                (not (==_e (++_e (**_e x 
 
3405
                                       (mv-nth 0 
 
3406
                                               (Bezout1 x y (Find-smallest-n x y n)))
 
3407
                                       )
 
3408
                                 (**_e y 
 
3409
                                       (mv-nth 1 
 
3410
                                               (Bezout1 x y (Find-smallest-n x y n)))
 
3411
                                       )
 
3412
                                 )
 
3413
                           (0_e)))
 
3414
                (equal (Size (++_e (**_e x 
 
3415
                                         (mv-nth 0 
 
3416
                                                 (Bezout1 x y (Find-smallest-n x y n))
 
3417
                                                 )
 
3418
                                         )
 
3419
                                   (**_e y 
 
3420
                                         (mv-nth 1 
 
3421
                                                 (Bezout1 x y (Find-smallest-n x y n))
 
3422
                                                 )
 
3423
                                         ))) 
 
3424
                       (Find-smallest-n x y n))))
 
3425
  :hints (("Goal"
 
3426
           :in-theory (disable (:definition mv-nth)))))
 
3427
 
 
3428
(defthm
 
3429
  Not-Size-Bezout1-n-=-n
 
3430
  (implies (and (integerp k)
 
3431
                (integerp n)
 
3432
                (<= 0 k)
 
3433
                (<= k n)
 
3434
                (< n (Find-smallest-n x y k))
 
3435
                (edp x)
 
3436
                (not (==_e x (0_e)))
 
3437
                (edp y))
 
3438
           (not (and (edp (mv-nth 0 (Bezout1 x y n)))
 
3439
                     (edp (mv-nth 1 (Bezout1 x y n)))
 
3440
                     (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3441
                                      (**_e y (mv-nth 1 (Bezout1 x y n))))
 
3442
                                (0_e)))
 
3443
                (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3444
                                   (**_e y (mv-nth 1 (Bezout1 x y n))))) 
 
3445
                       n))))
 
3446
  :rule-classes ((:rewrite
 
3447
                  :corollary
 
3448
                  (implies (and (< n (Find-smallest-n x y k))
 
3449
                                (integerp k)
 
3450
                                (integerp n)
 
3451
                                (<= 0 k)
 
3452
                                (<= k n)                                
 
3453
                                (edp x)
 
3454
                                (not (==_e x (0_e)))
 
3455
                                (edp y)
 
3456
                                (edp (mv-nth 0 (Bezout1 x y n)))
 
3457
                                (edp (mv-nth 1 (Bezout1 x y n)))
 
3458
                                (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3459
                                                 (**_e y (mv-nth 1 (Bezout1 x y n))))
 
3460
                                           (0_e))))
 
3461
                           (not (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3462
                                                   (**_e y (mv-nth 1 (Bezout1 x y n)))
 
3463
                                                   )) 
 
3464
                                       n))))))
 
3465
 
 
3466
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
3467
;; (Find-smallest-n x y 0),
 
3468
;;   provided x is a nonzero element of edp, 
 
3469
;;   finds the smallest natp n such that 
 
3470
;;          (and (edp (mv-nth 0 (Bezout1 x y n)))
 
3471
;;               (edp (mv-nth 1 (Bezout1 x y n)))
 
3472
;;               (not (equal (+_e (*_e x (mv-nth 0 (Bezout1 x y n)))
 
3473
;;                                (*_e y (mv-nth 1 (Bezout1 x y n))))
 
3474
;;                           (0_e)))
 
3475
;;               (equal (Size (+_e (*_e x (mv-nth 0 (Bezout1 x y n)))
 
3476
;;                                 (*_e y (mv-nth 1 (Bezout1 x y n))))) 
 
3477
;;                      n))
 
3478
;;   (if it exists).
 
3479
 
 
3480
(defthm
 
3481
  Natp-Find-smallest-n-0
 
3482
  (implies (and (edp x)
 
3483
                (not (==_e x (0_e)))
 
3484
                (edp y))
 
3485
           (and (integerp (Find-smallest-n x y 0))
 
3486
                (>= (Find-smallest-n x y 0) 0)))
 
3487
  :rule-classes nil)
 
3488
 
 
3489
(defthm
 
3490
  Bezout1-Find-smallest-n-0
 
3491
  (implies (and (edp x)
 
3492
                (not (==_e x (0_e)))
 
3493
                (edp y))
 
3494
           (and (edp (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3495
                (edp (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3496
                (not (==_e (++_e (**_e x 
 
3497
                                       (mv-nth 0 
 
3498
                                               (Bezout1 x y (Find-smallest-n x y 0)))
 
3499
                                       )
 
3500
                                 (**_e y 
 
3501
                                       (mv-nth 1 
 
3502
                                               (Bezout1 x y (Find-smallest-n x y 0)))
 
3503
                                       )
 
3504
                                 )
 
3505
                           (0_e)))
 
3506
                (equal (Size (++_e (**_e x 
 
3507
                                         (mv-nth 0 
 
3508
                                                 (Bezout1 x y (Find-smallest-n x y 0))
 
3509
                                                 )
 
3510
                                         )
 
3511
                                   (**_e y 
 
3512
                                         (mv-nth 1 
 
3513
                                                 (Bezout1 x y (Find-smallest-n x y 0))
 
3514
                                                 )
 
3515
                                         ))) 
 
3516
                       (Find-smallest-n x y 0))))
 
3517
  :hints (("Goal"
 
3518
           :use (:instance
 
3519
                 Bezout1-Find-smallest-n
 
3520
                 (n 0)))))
 
3521
 
 
3522
(defthm
 
3523
  Not-Size-Bezout1-n-=-n-1
 
3524
  (implies (and (integerp n)
 
3525
                (<= 0 n)
 
3526
                (< n (Find-smallest-n x y 0))
 
3527
                (edp x)
 
3528
                (not (==_e x (0_e)))
 
3529
                (edp y))
 
3530
           (not (and (edp (mv-nth 0 (Bezout1 x y n)))
 
3531
                     (edp (mv-nth 1 (Bezout1 x y n)))
 
3532
                     (not (==_e (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3533
                                      (**_e y (mv-nth 1 (Bezout1 x y n))))
 
3534
                                (0_e)))
 
3535
                     (equal (Size (++_e (**_e x (mv-nth 0 (Bezout1 x y n)))
 
3536
                                        (**_e y (mv-nth 1 (Bezout1 x y n))))) 
 
3537
                            n))))
 
3538
  :rule-classes nil
 
3539
  :hints (("Goal"
 
3540
           :by (:instance
 
3541
                 Not-Size-Bezout1-n-=-n
 
3542
                 (k 0)))))
 
3543
 
 
3544
(defthm
 
3545
  Size->=-Find-smallest-n-0
 
3546
  (implies (and (edp x)
 
3547
                (not (==_e x (0_e)))
 
3548
                (edp y)
 
3549
                (edp z0)
 
3550
                (edp z1)
 
3551
                (not (==_e (++_e (**_e x z0)
 
3552
                                 (**_e y z1))
 
3553
                           (0_e))))
 
3554
           (>= (Size (++_e (**_e x z0)
 
3555
                           (**_e y z1)))
 
3556
               (Find-smallest-n x y 0)))
 
3557
  :rule-classes (:rewrite 
 
3558
                 :linear)
 
3559
  :hints (("Goal"
 
3560
           :in-theory (disable (:definition mv-nth))
 
3561
           :use (:instance
 
3562
                 Not-Size-Bezout1-n-=-n-1
 
3563
                 (n (Size (++_e (**_e x z0)
 
3564
                                (**_e y z1))))))))
 
3565
 
 
3566
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
3567
;; The next sequence of equations and inequalities
 
3568
;;  is used to establish the existence of the gcd
 
3569
;;  of any two elements of edp when at least one 
 
3570
;;  of the elements is nonzero. Any gcd of two 
 
3571
;;  elements can always be written as a linear
 
3572
;;  combination of the two elements.
 
3573
 
 
3574
(defthm
 
3575
  Equation-0
 
3576
  (implies (and (edp a)
 
3577
                (edp b)
 
3578
                (edp c))
 
3579
           (iff (==_e (++_e a b) c)
 
3580
                (==_e (++_e c (-_e b)) a)))
 
3581
  :rule-classes nil)
 
3582
 
 
3583
(defthm
 
3584
  Equation-1
 
3585
  (implies (and (edp a)
 
3586
                (edp b)
 
3587
                (edp c))
 
3588
           (equal (==_e (++_e a b) c)
 
3589
                  (==_e (++_e c (-_e b)) a)))
 
3590
  :rule-classes nil
 
3591
  :hints (("Goal"
 
3592
           :use Equation-0)))
 
3593
 
 
3594
(defthm
 
3595
  Equation-2
 
3596
  (implies (and (edp x)
 
3597
                (edp y)
 
3598
                (not (==_e y (0_e))))
 
3599
           (==_e (++_e x 
 
3600
                       (-_e (**_e y
 
3601
                                  (qq_e x y))))
 
3602
                 (rr_e x y)))
 
3603
  :rule-classes nil
 
3604
  :hints (("Goal"
 
3605
           :use (:instance
 
3606
                 Equation-1
 
3607
                 (a (rr_e x y))
 
3608
                 (b (**_e y
 
3609
                         (qq_e x y)))
 
3610
                 (c x)))))
 
3611
 
 
3612
(defthm
 
3613
  Equation-3
 
3614
  (implies (and (edp x)
 
3615
                (not (==_e x (0_e)))
 
3616
                (edp y))
 
3617
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3618
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3619
                           )))
 
3620
                (==_e (++_e x 
 
3621
                            (-_e (**_e lc
 
3622
                                       (qq_e x lc))))
 
3623
                      (rr_e x lc))))
 
3624
  :rule-classes nil
 
3625
  :hints (("Goal"
 
3626
           :in-theory (disable (:definition find-smallest-n)
 
3627
                               (:definition mv-nth))
 
3628
           :use (:instance
 
3629
                 Equation-2
 
3630
                 (y (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3631
                          (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3632
                          ))))))
 
3633
 
 
3634
(defthm
 
3635
  Equation-3a
 
3636
  (implies (and (edp x)
 
3637
                (not (==_e x (0_e)))
 
3638
                (edp y))
 
3639
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3640
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3641
                           )))
 
3642
                (==_e (++_e y 
 
3643
                            (-_e (**_e lc
 
3644
                                       (qq_e y lc))))
 
3645
                      (rr_e y lc))))
 
3646
  :rule-classes nil
 
3647
  :hints (("Goal"
 
3648
           :in-theory (disable (:definition find-smallest-n)
 
3649
                               (:definition mv-nth))
 
3650
           :use (:instance
 
3651
                 Equation-2
 
3652
                 (x y)
 
3653
                 (y (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3654
                          (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3655
                          ))))))
 
3656
 
 
3657
(defthm
 
3658
  Inequality-4
 
3659
  (implies (and (edp x)
 
3660
                (not (==_e x (0_e)))
 
3661
                (edp y))
 
3662
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3663
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3664
                           )))
 
3665
                (or (==_e (++_e x 
 
3666
                                (-_e (**_e lc
 
3667
                                           (qq_e x lc))))
 
3668
                          (0_e))
 
3669
                    (< (Size (++_e x 
 
3670
                                  (-_e (**_e lc
 
3671
                                             (qq_e x lc)))))
 
3672
                       (Find-smallest-n x y 0)))))
 
3673
  :rule-classes nil
 
3674
  :hints (("Goal"
 
3675
           :in-theory (disable (:definition find-smallest-n)
 
3676
                               (:definition mv-nth))
 
3677
           :use Equation-3)))
 
3678
 
 
3679
(defthm
 
3680
  Inequality-4a
 
3681
  (implies (and (edp x)
 
3682
                (not (==_e x (0_e)))
 
3683
                (edp y))
 
3684
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3685
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3686
                           )))
 
3687
                (or (==_e (++_e y 
 
3688
                                (-_e (**_e lc
 
3689
                                           (qq_e y lc))))
 
3690
                          (0_e))
 
3691
                    (< (Size (++_e y 
 
3692
                                  (-_e (**_e lc
 
3693
                                             (qq_e y lc)))))
 
3694
                       (Find-smallest-n x y 0)))))
 
3695
  :rule-classes nil
 
3696
  :hints (("Goal"
 
3697
           :in-theory (disable (:definition find-smallest-n)
 
3698
                               (:definition mv-nth))
 
3699
           :use Equation-3a)))
 
3700
 
 
3701
(defthm
 
3702
  Equation-5
 
3703
  (implies (and (edp x)
 
3704
                (edp y)
 
3705
                (edp q)
 
3706
                (edp b0)
 
3707
                (edp b1))
 
3708
           (==_e (++_e x 
 
3709
                       (-_e (**_e (++_e (**_e x b0)
 
3710
                                        (**_e y b1))
 
3711
                                  q)))
 
3712
                 (++_e (**_e x 
 
3713
                             (++_e (1_e)
 
3714
                                   (-_e (**_e b0 q))))
 
3715
                      (-_e (**_e y b1 q)))))
 
3716
  :rule-classes nil)
 
3717
 
 
3718
(defthm
 
3719
  Equation-5a
 
3720
  (implies (and (edp x)
 
3721
                (edp y)
 
3722
                (edp q)
 
3723
                (edp b0)
 
3724
                (edp b1))
 
3725
           (==_e (++_e y 
 
3726
                       (-_e (**_e (++_e (**_e x b0)
 
3727
                                        (**_e y b1))
 
3728
                                  q)))
 
3729
                  (++_e (**_e y 
 
3730
                              (++_e (1_e)
 
3731
                                    (-_e (**_e b1 q))))
 
3732
                        (-_e (**_e x b0 q)))))
 
3733
  :rule-classes nil)
 
3734
 
 
3735
(defthm
 
3736
  Equation-6
 
3737
  (implies (and (edp x)
 
3738
                (not (==_e x (0_e)))
 
3739
                (edp y))
 
3740
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3741
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3742
                           ))
 
3743
                 (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3744
                 (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))))
 
3745
                (==_e (++_e x 
 
3746
                            (-_e (**_e lc
 
3747
                                       (qq_e x lc))))
 
3748
                      (++_e (**_e x 
 
3749
                                  (++_e (1_e)
 
3750
                                        (-_e (**_e b0
 
3751
                                                   (qq_e x lc)))))
 
3752
                            (++_e (**_e y
 
3753
                                        (-_e (**_e b1
 
3754
                                                   (qq_e x lc)))))))))
 
3755
  :rule-classes nil
 
3756
  :hints (("Goal"
 
3757
           :in-theory (disable (:definition find-smallest-n)
 
3758
                               (:definition mv-nth))
 
3759
           :use (:instance
 
3760
                 Equation-5
 
3761
                 (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3762
                 (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3763
                 (q (qq_e x
 
3764
                          (++_e (**_e x 
 
3765
                                      (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3766
                                (**_e y 
 
3767
                                      (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3768
                                )))))))
 
3769
 
 
3770
(defthm
 
3771
  Equation-6a
 
3772
  (implies (and (edp x)
 
3773
                (not (==_e x (0_e)))
 
3774
                (edp y))
 
3775
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3776
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3777
                           ))
 
3778
                 (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3779
                 (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))))
 
3780
                (==_e (++_e y 
 
3781
                            (-_e (**_e lc
 
3782
                                       (qq_e y lc))))
 
3783
                      (++_e (**_e y 
 
3784
                                  (++_e (1_e)
 
3785
                                        (-_e (**_e b1 
 
3786
                                                   (qq_e y lc)))))
 
3787
                            (-_e (**_e x 
 
3788
                                       (**_e b0 
 
3789
                                             (qq_e y lc))))))))
 
3790
  :rule-classes nil
 
3791
  :hints (("Goal"
 
3792
           :in-theory (disable (:definition find-smallest-n)
 
3793
                               (:definition mv-nth))
 
3794
           :use (:instance
 
3795
                 Equation-5a
 
3796
                 (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3797
                 (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3798
                 (q (qq_e y
 
3799
                          (++_e (**_e x 
 
3800
                                      (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3801
                                (**_e y 
 
3802
                                      (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3803
                                )))))))
 
3804
 
 
3805
(defthm
 
3806
  Inequality-7
 
3807
  (implies (and (edp x)
 
3808
                (not (==_e x (0_e)))
 
3809
                (edp y))
 
3810
           (let* ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3811
                            (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3812
                            ))
 
3813
                  (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3814
                  (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3815
                  (z0 (++_e (1_e)
 
3816
                            (-_e (**_e b0
 
3817
                                       (qq_e x lc)))))
 
3818
                  (z1 (-_e (**_e b1
 
3819
                                 (qq_e x lc)))))
 
3820
                 (or (==_e (++_e (**_e x z0)
 
3821
                                 (**_e y z1))
 
3822
                           (0_e))
 
3823
                     (>= (Size (++_e (**_e x z0)
 
3824
                                     (**_e y z1)))
 
3825
                         (Find-smallest-n x y 0)))))
 
3826
  :rule-classes nil
 
3827
  :hints (("Goal"
 
3828
           :in-theory (disable (:definition mv-nth)
 
3829
                               (:definition find-smallest-n))
 
3830
           :use (:instance
 
3831
                 Size->=-Find-smallest-n-0
 
3832
                 (z0 (++_e (1_e)
 
3833
                           (-_e (**_e (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0)))
 
3834
                                      (qq_e x 
 
3835
                                            (++_e 
 
3836
                                             (**_e x 
 
3837
                                                   (mv-nth 0 
 
3838
                                                           (Bezout1 x
 
3839
                                                                    y 
 
3840
                                                                    (Find-smallest-n x y 0)))
 
3841
                                                   )
 
3842
                                             (**_e y 
 
3843
                                                   (mv-nth 1 
 
3844
                                                           (Bezout1 x
 
3845
                                                                    y 
 
3846
                                                                    (Find-smallest-n x y 0)))
 
3847
                                                   )))))))
 
3848
                 (z1 (-_e
 
3849
                      (**_e (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))
 
3850
                            (qq_e x 
 
3851
                                  (++_e 
 
3852
                                   (**_e x 
 
3853
                                         (mv-nth 0 
 
3854
                                                 (Bezout1 x y (Find-smallest-n x y 0)
 
3855
                                                          )))
 
3856
                                   (**_e y 
 
3857
                                         (mv-nth 1 
 
3858
                                                 (Bezout1 x y (Find-smallest-n x y 0)
 
3859
                                                          ))))))))))))
 
3860
 
 
3861
(defthm
 
3862
  Inequality-7a
 
3863
  (implies (and (edp x)
 
3864
                (not (==_e x (0_e)))
 
3865
                (edp y))
 
3866
           (let* ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3867
                            (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3868
                            ))
 
3869
                  (b0 (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3870
                  (b1 (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3871
                  (z1 (++_e (1_e)
 
3872
                            (-_e (**_e b1
 
3873
                                       (qq_e y lc)))))
 
3874
                  (z0 (-_e (**_e b0
 
3875
                                 (qq_e y lc)))))
 
3876
                 (or (==_e (++_e (**_e x z0)
 
3877
                                 (**_e y z1))
 
3878
                           (0_e))
 
3879
                     (>= (Size (++_e (**_e x z0)
 
3880
                                     (**_e y z1)))
 
3881
                         (Find-smallest-n x y 0)))))
 
3882
  :rule-classes nil
 
3883
  :hints (("Goal"
 
3884
           :in-theory (disable (:definition mv-nth)
 
3885
                               (:definition find-smallest-n))
 
3886
           :use (:instance
 
3887
                 Size->=-Find-smallest-n-0
 
3888
                 (z1 (++_e (1_e)
 
3889
                           (-_e (**_e (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))
 
3890
                                      (qq_e y 
 
3891
                                            (++_e 
 
3892
                                             (**_e x 
 
3893
                                                   (mv-nth 0 
 
3894
                                                           (Bezout1 x
 
3895
                                                                    y 
 
3896
                                                                    (Find-smallest-n x y 0)))
 
3897
                                                   )
 
3898
                                             (**_e y 
 
3899
                                                   (mv-nth 1 
 
3900
                                                           (Bezout1 x
 
3901
                                                                    y 
 
3902
                                                                    (Find-smallest-n x y 0)))
 
3903
                                                   )))))))
 
3904
                 (z0 (-_e
 
3905
                      (**_e (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0)))
 
3906
                            (qq_e y 
 
3907
                                  (++_e 
 
3908
                                   (**_e x 
 
3909
                                         (mv-nth 0 
 
3910
                                                 (Bezout1 x y (Find-smallest-n x y 0)
 
3911
                                                          )))
 
3912
                                   (**_e y 
 
3913
                                         (mv-nth 1 
 
3914
                                                 (Bezout1 x y (Find-smallest-n x y 0)
 
3915
                                                          ))))))))))))
 
3916
 
 
3917
(defthm
 
3918
  Equation-8
 
3919
  (implies (and (edp x)
 
3920
                (not (==_e x (0_e)))
 
3921
                (edp y))
 
3922
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3923
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3924
                           )))
 
3925
                (==_e (**_e lc
 
3926
                            (qq_e x lc))
 
3927
                      x)))
 
3928
  :rule-classes nil
 
3929
  :hints (("Goal"
 
3930
           :in-theory (disable (:definition find-smallest-n)
 
3931
                               (:definition mv-nth)
 
3932
                               right-distributivity-law)
 
3933
           :use (Inequality-4
 
3934
                 Equation-6
 
3935
                 Inequality-7))))
 
3936
 
 
3937
(defthm
 
3938
  Equation-8a
 
3939
  (implies (and (edp x)
 
3940
                (not (==_e x (0_e)))
 
3941
                (edp y))
 
3942
           (let ((lc (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3943
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))
 
3944
                           )))
 
3945
                (==_e (**_e lc
 
3946
                            (qq_e y lc))
 
3947
                      y)))
 
3948
  :rule-classes nil
 
3949
  :hints (("Goal"
 
3950
           :in-theory (disable (:definition find-smallest-n)
 
3951
                               (:definition mv-nth)
 
3952
                               right-distributivity-law)
 
3953
           
 
3954
           :use (Inequality-4a
 
3955
                 Equation-6a
 
3956
                 Inequality-7a))))
 
3957
 
 
3958
(defthm
 
3959
  Divides-pp-Bezout1-x
 
3960
  (implies (and (edp x)
 
3961
                (not (==_e x (0_e)))
 
3962
                (edp y))
 
3963
           (divides-pp (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3964
                             (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))))
 
3965
                       x))
 
3966
  :hints (("Goal"
 
3967
           :in-theory (disable (:definition find-smallest-n)
 
3968
                               (:definition mv-nth))
 
3969
           :use (Equation-8
 
3970
                 (:instance
 
3971
                  divides-pp-suff
 
3972
                  (x (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3973
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))))
 
3974
                  (y x)
 
3975
                  (z (qq_e x (++_e (**_e x 
 
3976
                                         (mv-nth 0 
 
3977
                                                 (Bezout1 x y (Find-smallest-n x y 0)))
 
3978
                                         )
 
3979
                                   (**_e y 
 
3980
                                         (mv-nth 1 
 
3981
                                                 (Bezout1 x y (Find-smallest-n x y 0)))
 
3982
                                         )))))))))
 
3983
 
 
3984
(defthm
 
3985
  Divides-pp-Bezout1-y
 
3986
  (implies (and (edp x)
 
3987
                (not (==_e x (0_e)))
 
3988
                (edp y))
 
3989
           (divides-pp (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3990
                             (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0)))))
 
3991
                       y))
 
3992
  :hints (("Goal"
 
3993
           :in-theory (disable (:definition find-smallest-n)
 
3994
                               (:definition mv-nth))
 
3995
           :use (Equation-8a
 
3996
                 (:instance
 
3997
                  divides-pp-suff
 
3998
                  (x (++_e (**_e x (mv-nth 0 (Bezout1 x y (Find-smallest-n x y 0))))
 
3999
                           (**_e y (mv-nth 1 (Bezout1 x y (Find-smallest-n x y 0))))))
 
4000
                  (z (qq_e y (++_e (**_e x 
 
4001
                                         (mv-nth 0 
 
4002
                                                 (Bezout1 x y (Find-smallest-n x y 0)))
 
4003
                                         )
 
4004
                                   (**_e y 
 
4005
                                         (mv-nth 1 
 
4006
                                                 (Bezout1 x y (Find-smallest-n x y 0))))
 
4007
                                   ))))))))
 
4008
 
 
4009
(defun
 
4010
  Bezout (x y)
 
4011
  "Return (mv b0 b1) so that
 
4012
   x b0 + y b1 is a gcd of x and y."
 
4013
  (if (and (edp x)
 
4014
           (not (==_e x (0_e)))
 
4015
           (edp y))
 
4016
      (Bezout1 x y (Find-smallest-n x y 0))
 
4017
      (mv (0_e)(1_e))))
 
4018
 
 
4019
(defthm
 
4020
  Edp-mv-nth-Bezout
 
4021
  (and (edp (mv-nth 0 (Bezout x y)))
 
4022
       (edp (mv-nth 1 (Bezout x y))))
 
4023
  :hints (("goal"
 
4024
           :in-theory (disable (:definition mv-nth)
 
4025
                               (:definition find-smallest-n)))))
 
4026
 
 
4027
(defthm
 
4028
  Gcd-pp-mv-nth-Bezout
 
4029
  (implies (and (edp x)
 
4030
                (edp y))
 
4031
           (gcd-pp x y (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4032
                             (**_e y (mv-nth 1 (Bezout x y))))))
 
4033
  :hints (("goal"
 
4034
           :in-theory (disable (:definition mv-nth)
 
4035
                               (:definition find-smallest-n)))))
 
4036
 
 
4037
(defthm
 
4038
  nth-mv-nth
 
4039
  (equal (nth k lst)(mv-nth k lst)))
 
4040
 
 
4041
(defthm
 
4042
  Gcd-pp-nth-Bezout
 
4043
  (implies (and (edp x)
 
4044
                (edp y))
 
4045
           (gcd-pp x y (++_e (**_e x (nth 0 (Bezout x y)))
 
4046
                             (**_e y (nth 1 (Bezout x y))))))
 
4047
  :hints (("goal"
 
4048
           :in-theory (disable (:definition mv-nth)
 
4049
                               (:definition find-smallest-n)))))
 
4050
 
 
4051
(in-theory (disable nth-mv-nth))
 
4052
 
 
4053
(defthm
 
4054
  1st-2nd-mv-nth
 
4055
  (and (equal (first lst)(mv-nth 0 lst))
 
4056
       (equal (second lst)(mv-nth 1 lst))))
 
4057
 
 
4058
(defthm
 
4059
  Gcd-pp-Bezout
 
4060
  (implies (and (edp x)
 
4061
                (edp y))
 
4062
           (Gcd-pp x y (++_e (**_e x (first  (Bezout x y)))
 
4063
                             (**_e y (second (Bezout x y))))))
 
4064
  :hints (("goal"
 
4065
           :in-theory (disable (:definition mv-nth)
 
4066
                               (:definition find-smallest-n)))))
 
4067
 
 
4068
(in-theory (disable 1st-2nd-mv-nth))
 
4069
 
 
4070
(defthm
 
4071
  COMMON-divisor-mv-nth-Bezout
 
4072
  (implies (and (edp x)
 
4073
                (edp y))
 
4074
           (and (divides-pp (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4075
                                  (**_e y (mv-nth 1 (Bezout x y))))
 
4076
                            x)
 
4077
                (divides-pp (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4078
                                  (**_e y (mv-nth 1 (Bezout x y))))
 
4079
                            y)))
 
4080
  :hints (("goal"
 
4081
           :in-theory (disable (:definition mv-nth)
 
4082
                               (:definition find-smallest-n)))))
 
4083
 
 
4084
(defthm
 
4085
  GREATEST-common-divisor-mv-nth-Bezout
 
4086
  (implies (and (divides-pp d x)
 
4087
                (divides-pp d y))
 
4088
           (divides-pp d (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4089
                               (**_e y (mv-nth 1 (Bezout x y))))))
 
4090
  :hints (("Goal"
 
4091
           :in-theory (disable (:definition mv-nth)
 
4092
                               (:definition bezout)))))
 
4093
 
 
4094
(defthm
 
4095
  Gcd-pp-associates-pp
 
4096
  (implies (and (gcd-pp x y g1)
 
4097
                (gcd-pp x y g2))
 
4098
           (equal (associates-pp g1 g2) t))
 
4099
  :hints (("goal"
 
4100
           :use ((:instance
 
4101
                  gcd-pp-necc
 
4102
                  (g g1)
 
4103
                  (d g2))
 
4104
                 (:instance
 
4105
                  gcd-pp-necc
 
4106
                  (g g2)
 
4107
                  (d g1))))))
 
4108
 
 
4109
(defthm
 
4110
  Gcd-pp-edp-1
 
4111
  (implies (gcd-pp x y g)
 
4112
           (edp x))
 
4113
  :rule-classes :forward-chaining
 
4114
  :hints (("goal"
 
4115
           :in-theory (disable (:definition divides-pp)))))
 
4116
 
 
4117
(defthm
 
4118
  Gcd-pp-edp-2
 
4119
  (implies (gcd-pp x y g)
 
4120
           (edp y))
 
4121
  :rule-classes :forward-chaining
 
4122
  :hints (("goal"
 
4123
           :in-theory (disable (:definition divides-pp)))))
 
4124
 
 
4125
(defthm
 
4126
  Gcd-pp-edp-3
 
4127
  (implies (gcd-pp x y g)
 
4128
           (edp g))
 
4129
  :rule-classes :forward-chaining)
 
4130
 
 
4131
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
4132
;; Show that any gcd of two edp elements can
 
4133
;;  always be written as a linear combination
 
4134
;;  of the two elements.
 
4135
 
 
4136
(defthm
 
4137
  Gcd=linear-combination
 
4138
  (implies (gcd-pp x y g)
 
4139
           (==_e (++_e (**_e x 
 
4140
                             (mv-nth 0 (Bezout x y))
 
4141
                             (divides-pp-witness
 
4142
                              (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4143
                                    (**_e y (mv-nth 1 (Bezout x y))))
 
4144
                              g))
 
4145
                       (**_e y 
 
4146
                             (mv-nth 1 (Bezout x y))
 
4147
                             (divides-pp-witness
 
4148
                              (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4149
                                    (**_e y (mv-nth 1 (Bezout x y))))
 
4150
                              g)))
 
4151
                 g))
 
4152
  :hints (("Goal"
 
4153
           :in-theory (disable (:definition bezout)
 
4154
                               (:definition mv-nth)
 
4155
                               gcd-pp-mv-nth-Bezout
 
4156
                               gcd-pp-associates-pp)
 
4157
          :use (gcd-pp-mv-nth-Bezout
 
4158
                (:instance
 
4159
                 gcd-pp-associates-pp
 
4160
                 (g2 g)
 
4161
                 (g1 (++_e (**_e x (mv-nth 0 (Bezout x y)))
 
4162
                           (**_e y (mv-nth 1 (Bezout x y))))))))))
 
4163
 
 
4164
(defthm
 
4165
  Associates-pp-implies-equal-gcd-pp-1
 
4166
  (implies (associates-pp x1 x2)
 
4167
           (equal (gcd-pp x1 y g)
 
4168
                  (gcd-pp x2 y g)))
 
4169
  :rule-classes :congruence
 
4170
  :hints (("Goal"
 
4171
           :in-theory (disable (:definition divides-pp))
 
4172
           :use ((:instance
 
4173
                  gcd-pp-necc
 
4174
                  (d (gcd-pp-witness x2 y g))
 
4175
                  (x x1))
 
4176
                 (:instance
 
4177
                  gcd-pp-necc
 
4178
                  (d (gcd-pp-witness x1 y g))
 
4179
                  (x x2))))))
 
4180
 
 
4181
(defthm
 
4182
  Associates-pp-implies-iff-gcd-pp-2
 
4183
  (implies (associates-pp y1 y2)
 
4184
           (iff (gcd-pp x y1 g)
 
4185
                (gcd-pp x y2 g)))
 
4186
  :rule-classes nil
 
4187
  :hints (("Goal"
 
4188
           :in-theory (disable (:definition divides-pp))
 
4189
           :use ((:instance
 
4190
                  gcd-pp-necc
 
4191
                  (d (gcd-pp-witness x y2 g))
 
4192
                  (y y1))
 
4193
                 (:instance
 
4194
                  gcd-pp-necc
 
4195
                  (d (gcd-pp-witness x y1 g))
 
4196
                  (y y2))))))
 
4197
 
 
4198
(defthm
 
4199
  Associates-pp-implies-equal-gcd-pp-2
 
4200
  (implies (associates-pp y1 y2)
 
4201
           (equal (gcd-pp x y1 g)
 
4202
                  (gcd-pp x y2 g)))
 
4203
  :rule-classes :congruence
 
4204
  :hints (("Goal"
 
4205
           :use (Associates-pp-implies-iff-gcd-pp-2
 
4206
                 (:instance
 
4207
                  (:theorem
 
4208
                   (implies (and (booleanp x)
 
4209
                                 (booleanp y))
 
4210
                            (equal (iff x y)
 
4211
                                   (equal x y))))
 
4212
                  (x (gcd-pp x y1 g))
 
4213
                  (y (gcd-pp x y2 g)))))))
 
4214
 
 
4215
(defthm
 
4216
  Associates-pp-implies-iff-gcd-pp-3
 
4217
  (implies (associates-pp g1 g2)
 
4218
           (iff (gcd-pp x y g1)
 
4219
                (gcd-pp x y g2)))
 
4220
  :rule-classes nil
 
4221
  :hints (("Goal"
 
4222
           :in-theory (disable (:definition divides-pp))
 
4223
           :use ((:instance
 
4224
                  gcd-pp-necc
 
4225
                  (d (gcd-pp-witness x y g2))
 
4226
                  (g g1))
 
4227
                 (:instance
 
4228
                  gcd-pp-necc
 
4229
                  (d (gcd-pp-witness x y g1))
 
4230
                  (g g2))))))
 
4231
 
 
4232
(defthm
 
4233
  Associates-pp-implies-equal-gcd-pp-3
 
4234
  (implies (associates-pp g1 g2)
 
4235
           (equal (gcd-pp x y g1)
 
4236
                  (gcd-pp x y g2)))
 
4237
  :rule-classes :congruence
 
4238
  :hints (("Goal"
 
4239
           :use (Associates-pp-implies-iff-gcd-pp-3
 
4240
                 (:instance
 
4241
                  (:theorem
 
4242
                   (implies (and (booleanp x)
 
4243
                                 (booleanp y))
 
4244
                            (equal (iff x y)
 
4245
                                   (equal x y))))
 
4246
                  (x (gcd-pp x y g1))
 
4247
                  (y (gcd-pp x y g2)))))))
 
4248
 
 
4249
(defthm
 
4250
  Linear-combination-divides-pp-gcd
 
4251
  (implies (gcd-pp x y g)
 
4252
           (divides-pp (++_e (**_e x 
 
4253
                                   (mv-nth 0 (bezout x y)))
 
4254
                             (**_e y
 
4255
                                   (mv-nth 1 (bezout x y))))
 
4256
                       g))
 
4257
  :hints (("goal"
 
4258
           :in-theory (disable  (:definition gcd-pp)
 
4259
                                (:definition bezout)
 
4260
                                (:definition divides-pp)
 
4261
                                gcd-pp-associates-pp)
 
4262
           :use (gcd-pp-mv-nth-bezout
 
4263
                 (:instance
 
4264
                  gcd-pp-associates-pp
 
4265
                  (g1 (++_e (**_e x 
 
4266
                                  (mv-nth 0 (bezout x y)))
 
4267
                            (**_e y
 
4268
                                  (mv-nth 1 (bezout x y)))))
 
4269
                  (g2 g))))))
 
4270
 
 
4271
(defthm
 
4272
  Edp-divides-p-witness-linear-combination
 
4273
  (implies (gcd-pp x y g)
 
4274
           (edp (divides-pp-witness (++_e (**_e x (mv-nth 0 (bezout x y)))
 
4275
                                          (**_e y (mv-nth 1 (bezout x y))))
 
4276
                                    g)))
 
4277
  :hints (("goal"
 
4278
           :in-theory (disable (:definition bezout)
 
4279
                               (:definition divides-pp)
 
4280
                               (:definition mv-nth)))))
 
4281
 
 
4282
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
4283
;; Unit-associates-p theory:
 
4284
 
 
4285
(defun-sk
 
4286
  Unit-associates-p (x y)
 
4287
  (exists u (if (and (edp x)
 
4288
                     (edp y))
 
4289
                (and (unit-p u)
 
4290
                     (=_e (*_e u x)
 
4291
                           y))
 
4292
                (equal x y))))
 
4293
 
 
4294
(defun-sk
 
4295
  Unit-associates-p1 (x y)
 
4296
  (exists u (if (and (edp x)
 
4297
                     (edp y))
 
4298
                (and (unit-p u)
 
4299
                     (==_e (**_e u x)
 
4300
                           y))
 
4301
                (equal x y))))
 
4302
 
 
4303
(defthm
 
4304
  *_e-=-**_e
 
4305
  (implies (and (edp x)
 
4306
                (edp y))
 
4307
           (equal (*_e x y)(**_e x y)))
 
4308
  :rule-classes nil
 
4309
  :hints (("Goal"
 
4310
           :in-theory (enable (:definition binary-**_e)))))
 
4311
 
 
4312
(defthm
 
4313
  =_e-=-==_e
 
4314
  (implies (and (edp x)
 
4315
                (edp y))
 
4316
           (equal (=_e x y)(==_e x y)))
 
4317
  :rule-classes nil
 
4318
  :hints (("Goal"
 
4319
           :in-theory (enable (:definition ==_e)))))
 
4320
 
 
4321
(defthm
 
4322
  Unit-p-implies-edp
 
4323
  (implies (unit-p x)
 
4324
           (edp x)))
 
4325
 
 
4326
(defthm
 
4327
  Unit-associates-p-implies-unit-associates-p1
 
4328
  (implies (unit-associates-p x y)
 
4329
           (unit-associates-p1 x y))
 
4330
  :rule-classes nil
 
4331
  :hints (("Goal"
 
4332
           :in-theory (disable (:definition unit-p)
 
4333
                               (:definition unit-associates-p1))
 
4334
           :use ((:instance
 
4335
                  unit-associates-p1-suff
 
4336
                  (u (unit-associates-p-witness x y)))
 
4337
                 (:instance
 
4338
                  *_e-=-**_e
 
4339
                  (x (unit-associates-p-witness x y))
 
4340
                  (y x))
 
4341
                 (:instance
 
4342
                  =_e-=-==_e
 
4343
                  (x (**_e (unit-associates-p-witness x y) x)))))))
 
4344
 
 
4345
(defthm
 
4346
  Unit-associates-p1-implies-unit-associates-p
 
4347
  (implies (unit-associates-p1 x y)
 
4348
           (unit-associates-p x y))
 
4349
  :rule-classes nil
 
4350
  :hints (("Goal"
 
4351
           :in-theory (disable (:definition unit-p)
 
4352
                               (:definition unit-associates-p))
 
4353
           :use ((:instance
 
4354
                  unit-associates-p-suff
 
4355
                  (u (unit-associates-p1-witness x y)))
 
4356
                 (:instance
 
4357
                  *_e-=-**_e
 
4358
                  (x (unit-associates-p1-witness x y))
 
4359
                  (y x))
 
4360
                 (:instance
 
4361
                  =_e-=-==_e
 
4362
                  (x (**_e (unit-associates-p1-witness x y) x)))))))
 
4363
 
 
4364
(defthm
 
4365
  Unit-associates-p-iff-unit-associates-p1
 
4366
  (iff (unit-associates-p x y)
 
4367
       (unit-associates-p1 x y))
 
4368
  :rule-classes nil
 
4369
  :hints (("Goal"
 
4370
           :use (Unit-associates-p-implies-unit-associates-p1
 
4371
                 Unit-associates-p1-implies-unit-associates-p))))
 
4372
 
 
4373
(defthm
 
4374
  Booleanp-unit-associates-p
 
4375
  (booleanp (unit-associates-p x y))
 
4376
  :rule-classes :type-prescription)
 
4377
 
 
4378
(defthm
 
4379
  Unit-associates-p-=-unit-associates-p1
 
4380
  (equal (unit-associates-p x y)
 
4381
         (unit-associates-p1 x y))
 
4382
  :rule-classes nil
 
4383
  :hints (("Goal"
 
4384
           :in-theory (disable (:definition unit-associates-p)
 
4385
                               (:definition unit-associates-p1))
 
4386
           :use Unit-associates-p-iff-unit-associates-p1)))
 
4387
 
 
4388
(defun
 
4389
  Unit-associates-pp-witness (x y)
 
4390
  "Unit-associates-pp-witness nicely
 
4391
   modifies unit-associates-p1-witness."
 
4392
  (unit-associates-p1-witness (C_==_e x)
 
4393
                              (C_==_e y)))
 
4394
 
 
4395
(defthm
 
4396
  ==_e-implies-==_e-associates-pp-witness-1
 
4397
  (implies (==_e x1 x2)
 
4398
           (==_e (Unit-associates-pp-witness x1 y)
 
4399
                 (Unit-associates-pp-witness x2 y)))
 
4400
  :rule-classes :congruence)
 
4401
 
 
4402
(defthm
 
4403
  ==_e-implies-==_e-associates-pp-witness-2
 
4404
  (implies (==_e y1 y2)
 
4405
           (==_e (Unit-associates-pp-witness x y1)
 
4406
                 (Unit-associates-pp-witness x y2)))
 
4407
  :rule-classes :congruence)
 
4408
 
 
4409
(defun
 
4410
  Unit-associates-pp (x y)
 
4411
  (let ((u (unit-associates-pp-witness x y)))
 
4412
       (if (and (edp x)
 
4413
                (edp y))
 
4414
           (and (unit-pp u)
 
4415
                (==_e (**_e u x) y))
 
4416
           (equal x y))))
 
4417
 
 
4418
(defthm
 
4419
  ==_e-=-equal
 
4420
  (implies (not (edp y1))
 
4421
           (equal (==_e y1 y2)
 
4422
                  (equal y1 y2)))
 
4423
  :rule-classes nil
 
4424
  :hints (("Goal"
 
4425
           :in-theory (enable (:definition ==_e)))))
 
4426
 
 
4427
(defthm
 
4428
  ==_e-implies-equal-unit-associates-pp-1
 
4429
  (implies (==_e y1 y2)
 
4430
           (equal (unit-associates-pp y1 z)
 
4431
                  (unit-associates-pp y2 z)))
 
4432
  :rule-classes :congruence
 
4433
  :hints (("Goal"
 
4434
           :use ==_e-=-equal)))
 
4435
 
 
4436
(in-theory (disable (:definition divides-pp)))
 
4437
 
 
4438
(defthm
 
4439
  ==_e-implies-equal-unit-associates-pp-2
 
4440
  (implies (==_e y1 y2)
 
4441
           (equal (unit-associates-pp x y1)
 
4442
                  (unit-associates-pp x y2)))
 
4443
  :rule-classes :congruence
 
4444
  :hints (("Goal"
 
4445
           :use ==_e-=-equal)))
 
4446
 
 
4447
(defthm
 
4448
  Unit-associates-pp-suff
 
4449
  (implies (if (and (edp x)
 
4450
                    (edp y))
 
4451
               (and (unit-pp u)
 
4452
                    (==_e (**_e u x) y))
 
4453
               (equal x y))
 
4454
           (unit-associates-pp x y))
 
4455
  :hints (("Goal"
 
4456
           :in-theory (disable unit-associates-p1-suff
 
4457
                               (:definition unit-p)
 
4458
                               (:definition unit-pp))
 
4459
           :use ((:instance
 
4460
                  unit-associates-p1-suff
 
4461
                  (x (C_==_e x))
 
4462
                  (y (C_==_e y)))
 
4463
                 (:instance
 
4464
                  unit-p-=-unit-pp
 
4465
                  (x u))
 
4466
                 (:instance
 
4467
                  unit-p-=-unit-pp
 
4468
                  (x (unit-associates-p1-witness (c_==_e x)
 
4469
                                                 (c_==_e y))))))))
 
4470
 
 
4471
(in-theory (disable (:definition unit-associates-pp-witness)
 
4472
                    (:executable-counterpart unit-associates-pp)))
 
4473
 
 
4474
(defthm
 
4475
  Unit-associates-p1-implies-unit-associates-pp
 
4476
  (implies (unit-associates-p1 x y)
 
4477
           (unit-associates-pp x y))
 
4478
  :rule-classes nil
 
4479
  :hints (("Goal"
 
4480
           :in-theory (disable (:definition unit-p)
 
4481
                               (:definition unit-pp))
 
4482
           :use ((:instance
 
4483
                  Unit-associates-pp-suff
 
4484
                  (u (unit-associates-p1-witness x y)))
 
4485
                 (:instance
 
4486
                  unit-p-=-unit-pp
 
4487
                  (x (unit-associates-p1-witness x y)))))))
 
4488
 
 
4489
(defthm
 
4490
  Unit-associates-pp-implies-unit-associates-p1
 
4491
  (implies (unit-associates-pp x y)
 
4492
           (unit-associates-p1 x y))
 
4493
  :rule-classes nil
 
4494
  :hints (("Goal"
 
4495
           :in-theory (disable (:definition unit-p)
 
4496
                               (:definition unit-pp))
 
4497
           :use ((:instance
 
4498
                  Unit-associates-p1-suff
 
4499
                  (u (unit-associates-pp-witness x y)))
 
4500
                 (:instance
 
4501
                  unit-p-=-unit-pp
 
4502
                  (x (unit-associates-pp-witness x y)))))))
 
4503
 
 
4504
(defthm
 
4505
  Unit-associates-p1-iff-unit-associates-pp
 
4506
  (iff (unit-associates-p1 x y)
 
4507
       (unit-associates-pp x y))
 
4508
  :rule-classes nil
 
4509
  :hints (("Goal"
 
4510
           :use (Unit-associates-p1-implies-unit-associates-pp
 
4511
                 Unit-associates-pp-implies-unit-associates-p1))))
 
4512
 
 
4513
(defthm
 
4514
  Unit-associates-p1-=-unit-associates-pp
 
4515
  (equal (unit-associates-p1 x y)
 
4516
         (unit-associates-pp x y))
 
4517
  :rule-classes nil
 
4518
  :hints (("Goal"
 
4519
           :in-theory (disable (:definition unit-associates-p1)
 
4520
                               (:definition unit-associates-pp))
 
4521
           :use Unit-associates-p1-iff-unit-associates-pp)))
 
4522
 
 
4523
(defthm
 
4524
  Unit-associates-p-=-unit-associates-pp
 
4525
  (equal (unit-associates-p x y)
 
4526
         (unit-associates-pp x y))
 
4527
  :rule-classes nil
 
4528
  :hints (("Goal"
 
4529
           :in-theory (disable (:definition unit-associates-p)
 
4530
                               (:definition unit-associates-p1)
 
4531
                               (:definition unit-associates-pp))
 
4532
           :use (Unit-associates-p-=-unit-associates-p1
 
4533
                 Unit-associates-p1-=-unit-associates-pp))))
 
4534
 
 
4535
(defthm
 
4536
  Reflexivity-unit-associates-pp
 
4537
  (unit-associates-pp x x)
 
4538
  :hints (("Goal"
 
4539
           :in-theory (disable (:definition unit-associates-pp))
 
4540
           :use (:instance
 
4541
                 unit-associates-pp-suff
 
4542
                 (u (1_e))
 
4543
                 (y x)))))
 
4544
 
 
4545
(set-backchain-limit 1)
 
4546
 
 
4547
(defthm
 
4548
  Symmetry-unit-associates-pp
 
4549
  (implies (unit-associates-pp x y)
 
4550
           (unit-associates-pp y x))
 
4551
  :hints (("Goal"
 
4552
           :in-theory (disable unit-pp-**_e-inverse
 
4553
                               (:definition unit-pp))
 
4554
           :use ((:instance
 
4555
                  unit-associates-pp-suff
 
4556
                  (u (divides-pp-witness (unit-associates-pp-witness x y) 
 
4557
                                         (1_e)))
 
4558
                  (x y)
 
4559
                  (y x))
 
4560
                 (:instance 
 
4561
                  unit-pp-**_e-inverse
 
4562
                  (u (unit-associates-pp-witness x y)))))
 
4563
          ("Subgoal 2"
 
4564
           :in-theory (enable (:definition unit-pp)))
 
4565
          ("Subgoal 1"
 
4566
           :in-theory (enable (:definition unit-pp)))))
 
4567
 
 
4568
(defthm
 
4569
  Transitivity-unit-associates-pp
 
4570
  (implies (and (unit-associates-pp x y)
 
4571
                (unit-associates-pp y z))
 
4572
           (unit-associates-pp x z))
 
4573
  :hints (("Goal"
 
4574
           :in-theory (disable (:definition unit-pp)
 
4575
                               commutativity-laws-for-++_e-&-**_e)
 
4576
           :use ((:instance
 
4577
                  unit-associates-pp-suff
 
4578
                  (u (**_e (unit-associates-pp-witness y z)
 
4579
                           (unit-associates-pp-witness x y)))
 
4580
                  (y z))))))
 
4581
 
 
4582
(set-backchain-limit nil)
 
4583
 
 
4584
(defthm 
 
4585
  Unit-associates-pp-is-an-equivalence 
 
4586
  (and (booleanp (unit-associates-pp x y)) 
 
4587
       (unit-associates-pp x x) 
 
4588
       (implies (unit-associates-pp x y) 
 
4589
                (unit-associates-pp y x)) 
 
4590
       (implies (and (unit-associates-pp x y)
 
4591
                     (unit-associates-pp y z))
 
4592
                (unit-associates-pp x z)))
 
4593
  :rule-classes :equivalence
 
4594
  :hints (("Goal"
 
4595
           :in-theory (disable (:definition unit-associates-pp)))))
 
4596
 
 
4597
(in-theory (disable Reflexivity-unit-associates-pp
 
4598
                    Symmetry-unit-associates-pp
 
4599
                    Transitivity-unit-associates-pp))
 
4600
 
 
4601
(defthm
 
4602
  Associates-pp-implies-iff-edp
 
4603
  (implies (associates-pp x y)
 
4604
           (iff (edp x)
 
4605
                (edp y)))
 
4606
  :rule-classes :congruence)
 
4607
 
 
4608
(set-backchain-limit 1)
 
4609
 
 
4610
(defthm
 
4611
  Associates-pp-refines-unit-associates-pp-lemma-1
 
4612
  (implies (and (edp x)
 
4613
                (not (==_e x (0_e)))
 
4614
                (associates-pp x y))
 
4615
           (==_e (**_e (divides-pp-witness x y)
 
4616
                       (divides-pp-witness y x))
 
4617
                 (1_e)))
 
4618
  :hints (("Goal"
 
4619
           :in-theory (e/d ((:definition divides-pp))
 
4620
                           (divides-pp-implies-witness=qq_e
 
4621
                            divides-pp-edp-divides-pp-witness))
 
4622
           :use ((:instance
 
4623
                  projection-laws
 
4624
                  (y (**_e (divides-pp-witness x y)
 
4625
                           (divides-pp-witness y x))))))))
 
4626
 
 
4627
(set-backchain-limit 2)
 
4628
 
 
4629
(defthm
 
4630
  Associates-pp-refines-unit-associates-pp-lemma-2
 
4631
  (implies (and (edp x)
 
4632
                (not (==_e x (0_e)))
 
4633
                (associates-pp x y))
 
4634
           (unit-pp (divides-pp-witness x y)))
 
4635
  :hints (("Goal"
 
4636
           :in-theory (enable (:definition divides-pp))
 
4637
           :use 
 
4638
           Associates-pp-refines-unit-associates-pp-lemma-1)))
 
4639
 
 
4640
(defthm
 
4641
  Associates-pp-refines-unit-associates-pp-lemma-3
 
4642
  (implies (and (edp x)
 
4643
                (not (==_e x (0_e)))
 
4644
                (associates-pp x y))
 
4645
           (unit-associates-pp x y))
 
4646
  :rule-classes nil
 
4647
  :hints (("Goal"
 
4648
           :in-theory (e/d ((:definition divides-pp))
 
4649
                           ((:definition unit-pp)
 
4650
                            divides-pp-implies-witness=qq_e
 
4651
                            unit-associates-pp-suff))
 
4652
           :use (:instance 
 
4653
                 Unit-associates-pp-suff
 
4654
                 (u (divides-pp-witness x y))))))
 
4655
 
 
4656
(defthm
 
4657
  Associates-pp-refines-unit-associates-pp
 
4658
  (implies (associates-pp x y)
 
4659
           (unit-associates-pp x y))
 
4660
  :rule-classes :refinement
 
4661
  :hints (("Goal"
 
4662
           :in-theory (e/d ((:definition divides-pp))
 
4663
                           ((:definition unit-pp)
 
4664
                            (:definition unit-associates-pp)))
 
4665
           :cases ((not (edp x))
 
4666
                   (==_e x (0_e))))
 
4667
          ("Subgoal 3"
 
4668
           :use Associates-pp-refines-unit-associates-pp-lemma-3)
 
4669
          ("Subgoal 1"
 
4670
           :use (:instance
 
4671
                 unit-associates-pp-suff
 
4672
                 (u (1_e))))))
 
4673
 
 
4674
(defthm
 
4675
  Unit-associates-pp-implies-iff-edp
 
4676
  (implies (unit-associates-pp x y)
 
4677
           (iff (edp x)
 
4678
                (edp y)))
 
4679
  :rule-classes :congruence)
 
4680
 
 
4681
(defthm
 
4682
  Unit-associates-pp-refines-associates-pp-lemma-1
 
4683
  (implies (and (edp x)
 
4684
                (unit-associates-pp x y))
 
4685
          (divides-pp x y))
 
4686
  :hints (("Goal"
 
4687
           :in-theory (disable (:definition unit-pp)
 
4688
                               (:definition divides-pp)))))
 
4689
 
 
4690
(defthm
 
4691
  Unit-associates-pp-refines-associates-pp
 
4692
  (implies (unit-associates-pp x y)
 
4693
           (associates-pp x y))
 
4694
  :rule-classes :refinement
 
4695
  :hints (("Goal"
 
4696
           :cases ((edp x)))
 
4697
          ("Subgoal 1"
 
4698
           :in-theory (disable (:definition unit-associates-pp)))))
 
4699
 
 
4700
(defthm
 
4701
  Unit-associates-pp-implies-reducible-pp-lemma-1
 
4702
  (implies (and (not (edp (unit-associates-pp-witness x y)))
 
4703
                (unit-associates-pp x y)
 
4704
                (edp (mv-nth 0 (reducible-pp-witness x)))
 
4705
                (edp (mv-nth 1 (reducible-pp-witness x)))
 
4706
                (not (unit-pp (mv-nth 0 (reducible-pp-witness x))))
 
4707
                (not (unit-pp (mv-nth 1 (reducible-pp-witness x))))
 
4708
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4709
                            (mv-nth 1 (reducible-pp-witness x)))
 
4710
                      x))
 
4711
           (reducible-pp y))
 
4712
  :hints (("Goal"
 
4713
           :in-theory (disable (:definition unit-pp)
 
4714
                               (:definition reducible-pp)))))
 
4715
 
 
4716
(defthm
 
4717
  Unit-associates-pp-implies-reducible-pp-lemma-2
 
4718
  (implies (and (not (==_e (**_e (unit-associates-pp-witness x y)
 
4719
                                 x)
 
4720
                           y))
 
4721
                (not (unit-pp (**_e (mv-nth 0 (reducible-pp-witness x))
 
4722
                                    (unit-associates-pp-witness x y))))
 
4723
                (unit-associates-pp x y)
 
4724
                (edp (mv-nth 0 (reducible-pp-witness x)))
 
4725
                (edp (mv-nth 1 (reducible-pp-witness x)))
 
4726
                (not (unit-pp (mv-nth 0 (reducible-pp-witness x))))
 
4727
                (not (unit-pp (mv-nth 1 (reducible-pp-witness x))))
 
4728
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4729
                            (mv-nth 1 (reducible-pp-witness x)))
 
4730
                      x))
 
4731
           (reducible-pp y))
 
4732
  :hints (("Goal"
 
4733
           :in-theory (disable (:definition unit-pp)
 
4734
                               (:definition reducible-pp)))))
 
4735
 
 
4736
(defthm
 
4737
  Unit-associates-pp-implies-reducible-pp-lemma-3
 
4738
  (implies (and (not (==_e (**_e (**_e (unit-associates-pp-witness x y)
 
4739
                                       (mv-nth 0 (reducible-pp-witness x)))
 
4740
                                 (mv-nth 1 (reducible-pp-witness x)))
 
4741
                           y))
 
4742
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4743
                            (mv-nth 1 (reducible-pp-witness x))
 
4744
                            (unit-associates-pp-witness x y))
 
4745
                      y)
 
4746
                (not (unit-pp (**_e (mv-nth 0 (reducible-pp-witness x))
 
4747
                                    (unit-associates-pp-witness x y))))
 
4748
                (unit-associates-pp x y)
 
4749
                (edp (mv-nth 0 (reducible-pp-witness x)))
 
4750
                (edp (mv-nth 1 (reducible-pp-witness x)))
 
4751
                (not (unit-pp (mv-nth 0 (reducible-pp-witness x))))
 
4752
                (not (unit-pp (mv-nth 1 (reducible-pp-witness x))))
 
4753
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4754
                            (mv-nth 1 (reducible-pp-witness x)))
 
4755
                      x))
 
4756
           (reducible-pp y))
 
4757
  :hints (("Goal"
 
4758
           :in-theory (disable (:definition unit-pp)
 
4759
                               (:definition reducible-pp)))))
 
4760
 
 
4761
(defthm
 
4762
  Unit-associates-pp-implies-reducible-pp-lemma-4
 
4763
  (implies (and (unit-pp (**_e (unit-associates-pp-witness x y)
 
4764
                               (mv-nth 0 (reducible-pp-witness x))))
 
4765
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4766
                            (mv-nth 1 (reducible-pp-witness x))
 
4767
                            (unit-associates-pp-witness x y))
 
4768
                      y)
 
4769
                (not (unit-pp (**_e (mv-nth 0 (reducible-pp-witness x))
 
4770
                                    (unit-associates-pp-witness x y))))
 
4771
                (unit-associates-pp x y)
 
4772
                (edp (mv-nth 0 (reducible-pp-witness x)))
 
4773
                (edp (mv-nth 1 (reducible-pp-witness x)))
 
4774
                (not (unit-pp (mv-nth 0 (reducible-pp-witness x))))
 
4775
                (not (unit-pp (mv-nth 1 (reducible-pp-witness x))))
 
4776
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4777
                            (mv-nth 1 (reducible-pp-witness x)))
 
4778
                      x))
 
4779
           (reducible-pp y))
 
4780
  :hints (("Goal"
 
4781
           :in-theory (disable (:definition unit-pp)
 
4782
                               (:definition reducible-pp)))))
 
4783
 
 
4784
(defthm
 
4785
  Unit-associates-pp-implies-reducible-pp-lemma-5
 
4786
  (implies (and (not (edp (**_e (unit-associates-pp-witness x y)
 
4787
                                (mv-nth 0 (reducible-pp-witness x)))))
 
4788
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4789
                            (mv-nth 1 (reducible-pp-witness x))
 
4790
                            (unit-associates-pp-witness x y))
 
4791
                      y)
 
4792
                (not (unit-pp (**_e (mv-nth 0 (reducible-pp-witness x))
 
4793
                                    (unit-associates-pp-witness x y))))
 
4794
                (unit-associates-pp x y)
 
4795
                (edp (mv-nth 0 (reducible-pp-witness x)))
 
4796
                (edp (mv-nth 1 (reducible-pp-witness x)))
 
4797
                (not (unit-pp (mv-nth 0 (reducible-pp-witness x))))
 
4798
                (not (unit-pp (mv-nth 1 (reducible-pp-witness x))))
 
4799
                (==_e (**_e (mv-nth 0 (reducible-pp-witness x))
 
4800
                            (mv-nth 1 (reducible-pp-witness x)))
 
4801
                      x))
 
4802
           (reducible-pp y))
 
4803
  :hints (("Goal"
 
4804
           :in-theory (disable (:definition unit-pp)
 
4805
                               (:definition reducible-pp)))))
 
4806
 
 
4807
(defthm
 
4808
  Unit-associates-pp-implies-reducible-pp
 
4809
  (implies (and (unit-associates-pp x y)
 
4810
                (reducible-pp x))
 
4811
           (reducible-pp y))
 
4812
  :rule-classes nil
 
4813
  :hints (("Goal"
 
4814
           :in-theory (disable (:definition mv-nth)
 
4815
                               (:definition unit-pp)
 
4816
                               (:definition reducible-pp)
 
4817
                               (:definition unit-associates-pp)
 
4818
                               reducible-pp-edp
 
4819
                               reducible-pp-suff)
 
4820
           :expand ((reducible-pp x))
 
4821
           :use ((:instance
 
4822
                  reducible-pp-suff
 
4823
                  (x y)
 
4824
                  (y (**_e (unit-associates-pp-witness x y)
 
4825
                           (mv-nth 0 (reducible-pp-witness x))))
 
4826
                  (z (mv-nth 1 (reducible-pp-witness x))))
 
4827
                 (:instance
 
4828
                  (:theorem
 
4829
                   (implies (and (edp a)
 
4830
                                 (edp b)
 
4831
                                 (edp c)
 
4832
                                 (==_e (**_e c x) y)
 
4833
                                 (==_e (**_e a b) x))
 
4834
                            (==_e (**_e a b c) y)))
 
4835
                  (a (mv-nth 0 (reducible-pp-witness x)))
 
4836
                  (b (mv-nth 1 (reducible-pp-witness x)))
 
4837
                  (c (unit-associates-pp-witness x y)))
 
4838
                 (:instance
 
4839
                  unit-pp-**_e=>unit-pp-factor-right
 
4840
                  (x (unit-associates-pp-witness x y))
 
4841
                  (y (mv-nth 0 (reducible-pp-witness x))))))))
 
4842
 
 
4843
(in-theory (disable Unit-associates-pp-implies-reducible-pp-lemma-1
 
4844
                    Unit-associates-pp-implies-reducible-pp-lemma-2
 
4845
                    Unit-associates-pp-implies-reducible-pp-lemma-3
 
4846
                    Unit-associates-pp-implies-reducible-pp-lemma-4
 
4847
                    Unit-associates-pp-implies-reducible-pp-lemma-5))
 
4848
 
 
4849
(defthm
 
4850
  Unit-associates-pp-implies-equal-reducible-pp
 
4851
  (implies (unit-associates-pp x y)
 
4852
           (equal (reducible-pp x)
 
4853
                  (reducible-pp y)))
 
4854
  :rule-classes :congruence
 
4855
  :hints (("Goal"
 
4856
           :in-theory (disable (:definition reducible-pp)
 
4857
                               (:definition unit-associates-pp))
 
4858
           :use (unit-associates-pp-implies-reducible-pp
 
4859
                 (:instance
 
4860
                  Unit-associates-pp-implies-reducible-pp
 
4861
                  (x y)
 
4862
                  (y x))))))
 
4863
 
 
4864
(defthm
 
4865
  Unit-associates-pp-implies-equal-irreducible-pp
 
4866
  (implies (unit-associates-pp x y)
 
4867
           (equal (irreducible-pp x)
 
4868
                  (irreducible-pp y)))
 
4869
  :rule-classes :congruence
 
4870
  :hints (("Goal"
 
4871
           :in-theory (disable (:definition reducible-pp)
 
4872
                               (:definition unit-associates-pp)))))
 
4873
 
 
4874
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
4875
;; Unique factorization theory:
 
4876
 
 
4877
(defun
 
4878
  Member-unit-associate (x lst)
 
4879
  "Determine if an unit-associate-p
 
4880
   of x is a member of lst."
 
4881
  (cond ((atom lst)
 
4882
         nil)
 
4883
        ((unit-associates-p x (car lst))
 
4884
         lst)
 
4885
        (t (member-unit-associate x (cdr lst)))))
 
4886
 
 
4887
(defun
 
4888
  Member-unit-associate-pp (x lst)
 
4889
  "Determine if an unit-associate-pp
 
4890
   of x is a member of lst."
 
4891
  (cond ((atom lst)
 
4892
         nil)
 
4893
        ((unit-associates-pp x (car lst))
 
4894
         lst)
 
4895
        (t (member-unit-associate-pp x (cdr lst)))))
 
4896
 
 
4897
(in-theory (disable (:definition unit-associates-p)))
 
4898
(in-theory (disable (:definition unit-associates-pp)))
 
4899
 
 
4900
(defthm
 
4901
  Member-unit-associate-=-member-unit-associate-pp
 
4902
  (equal (member-unit-associate x lst)
 
4903
        (member-unit-associate-pp x lst))
 
4904
  :rule-classes nil
 
4905
  :hints (("Subgoal *1/3"
 
4906
           :use (:instance 
 
4907
                 Unit-associates-p-=-unit-associates-pp
 
4908
                 (y (car lst))))
 
4909
          ("Subgoal *1/2"
 
4910
           :use (:instance 
 
4911
                 Unit-associates-p-=-unit-associates-pp
 
4912
                 (y (car lst))))))
 
4913
 
 
4914
(defun
 
4915
  Delete-one-unit-associate (x lst)
 
4916
  "Return the result of deleting one occurrence 
 
4917
   of an unit-associate-p of x from the list lst."
 
4918
  (if (consp lst)
 
4919
      (if (unit-associates-p x (car lst))
 
4920
          (cdr lst)
 
4921
          (cons (car lst)(delete-one-unit-associate x (cdr lst))))
 
4922
      lst))
 
4923
 
 
4924
(defun
 
4925
  Delete-one-unit-associate-pp (x lst)
 
4926
  "Return the result of deleting one occurrence 
 
4927
   of an unit-associate-pp of x from the list lst."
 
4928
  (if (consp lst)
 
4929
      (if (unit-associates-pp x (car lst))
 
4930
          (cdr lst)
 
4931
          (cons (car lst)(delete-one-unit-associate-pp x (cdr lst))))
 
4932
      lst))
 
4933
 
 
4934
(defthm
 
4935
  Delete-one-unit-associate-=-Delete-one-unit-associate-pp
 
4936
  (equal (Delete-one-unit-associate x lst)
 
4937
         (Delete-one-unit-associate-pp x lst))
 
4938
  :rule-classes nil
 
4939
  :hints (("Subgoal *1/2"
 
4940
           :use (:instance 
 
4941
                 Unit-associates-p-=-unit-associates-pp
 
4942
                 (y (car lst))))
 
4943
          ("Subgoal *1/1"
 
4944
           :use (:instance 
 
4945
                 Unit-associates-p-=-unit-associates-pp
 
4946
                 (y (car lst))))))
 
4947
 
 
4948
(defun
 
4949
  Bag-equal-unit-associates (lst1 lst2)
 
4950
  "Return T iff lst1 and lst2 have the same
 
4951
   members, up to unit-associates-p, with the
 
4952
   same multiplicity, up to unit-associates-p."
 
4953
  (if (consp lst1)
 
4954
      (and (member-unit-associate (car lst1) lst2)
 
4955
           (bag-equal-unit-associates (cdr lst1)
 
4956
                                      (delete-one-unit-associate (car lst1) 
 
4957
                                                                 lst2)))
 
4958
      (atom lst2)))
 
4959
 
 
4960
(defun
 
4961
  Bag-equal-unit-associates-pp (lst1 lst2)
 
4962
  "Return T iff lst1 and lst2 have the same
 
4963
   members, up to unit-associates-pp, with the
 
4964
   same multiplicity, up to unit-associates-pp."
 
4965
  (if (consp lst1)
 
4966
      (and (member-unit-associate-pp (car lst1) lst2)
 
4967
           (bag-equal-unit-associates-pp (cdr lst1)
 
4968
                                         (delete-one-unit-associate-pp (car lst1) 
 
4969
                                                                       lst2)))
 
4970
      (atom lst2)))
 
4971
 
 
4972
(defthm
 
4973
  Bag-equal-unit-associates-=-Bag-equal-unit-associates-pp
 
4974
  (equal (Bag-equal-unit-associates lst1 lst2)
 
4975
         (Bag-equal-unit-associates-pp lst1 lst2))
 
4976
  :rule-classes nil
 
4977
  :hints (("Subgoal *1/2"
 
4978
           :use (:instance
 
4979
                 Member-unit-associate-=-member-unit-associate-pp
 
4980
                 (x (car lst1))
 
4981
                 (lst lst2)))
 
4982
          ("Subgoal *1/1"
 
4983
           :use ((:instance
 
4984
                  Member-unit-associate-=-member-unit-associate-pp
 
4985
                  (x (car lst1))
 
4986
                  (lst lst2))
 
4987
                 (:instance
 
4988
                  Delete-one-unit-associate-=-Delete-one-unit-associate-pp
 
4989
                  (x (car lst1))
 
4990
                  (lst lst2))))))
 
4991
 
 
4992
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
4993
;; Show that bag-equal-unit-associates has the expected properties:
 
4994
 
 
4995
;;  Lisp objects that are bag-equal-unit-associates have the same length.
 
4996
 
 
4997
;;  Lisp objects that are bag-equal-unit-associates have the same members,
 
4998
;;   up to unit-associates-p
 
4999
 
 
5000
;;  Elements in Lisp objects that are bag-equal-unit-associates occur
 
5001
;;  in each object with the same multiplicity, up to unit-associates-p.
 
5002
 
 
5003
(defthm
 
5004
  Len-delete-one-unit-associate
 
5005
  (implies (member-unit-associate x lst)
 
5006
           (equal (+ 1 (len (delete-one-unit-associate x lst)))
 
5007
                  (len lst))))
 
5008
 
 
5009
(defthm
 
5010
  Len-delete-one-unit-associate-pp
 
5011
  (implies (member-unit-associate-pp x lst)
 
5012
           (equal (+ 1 (len (delete-one-unit-associate-pp x lst)))
 
5013
                  (len lst))))
 
5014
 
 
5015
(defthm
 
5016
  Bag-equal-unit-associates->equal-len
 
5017
  (implies (bag-equal-unit-associates lst1 lst2)
 
5018
           (equal (len lst1)
 
5019
                  (len lst2)))
 
5020
  :rule-classes nil)
 
5021
 
 
5022
(defthm
 
5023
  Bag-equal-unit-associates-pp->equal-len
 
5024
  (implies (bag-equal-unit-associates-pp lst1 lst2)
 
5025
           (equal (len lst1)
 
5026
                  (len lst2)))
 
5027
  :rule-classes nil)
 
5028
 
 
5029
(defthm
 
5030
  Member-unit-associate-pp-delete-one-unit-associate-pp
 
5031
  (implies (not (unit-associates-pp x y))
 
5032
           (iff (member-unit-associate-pp x 
 
5033
                                          (delete-one-unit-associate-pp y lst))
 
5034
                (member-unit-associate-pp x lst))))
 
5035
 
 
5036
(defthm
 
5037
  Unit-associates-pp-member-unit-associate-pp
 
5038
  (implies (and (unit-associates-pp x y)
 
5039
                (member-unit-associate-pp y lst))
 
5040
           (member-unit-associate-pp x lst)))
 
5041
 
 
5042
(defthm
 
5043
  Unit-associates-pp-implies-iff-member-unit-associate-pp
 
5044
  (implies (unit-associates-pp x1 x2)
 
5045
           (iff (member-unit-associate-pp x1 lst)
 
5046
                (member-unit-associate-pp x2 lst)))
 
5047
  :rule-classes :congruence)
 
5048
 
 
5049
(in-theory (disable Unit-associates-pp-member-unit-associate-pp))
 
5050
 
 
5051
(defthm
 
5052
  Bag-equal-unit-associates-pp->iff-member-unit-associate-pp
 
5053
  (implies (bag-equal-unit-associates-pp lst1 lst2)
 
5054
           (iff (member-unit-associate-pp x lst1)
 
5055
                (member-unit-associate-pp x lst2)))
 
5056
  :rule-classes nil)
 
5057
 
 
5058
(defthm
 
5059
  Bag-equal-unit-associates->iff-member-unit-associate
 
5060
  (implies (bag-equal-unit-associates lst1 lst2)
 
5061
           (iff (member-unit-associate x lst1)
 
5062
                (member-unit-associate x lst2)))
 
5063
  :rule-classes nil
 
5064
  :hints (("Goal"
 
5065
           :use (Bag-equal-unit-associates-pp->iff-member-unit-associate-pp
 
5066
                 Bag-equal-unit-associates-=-Bag-equal-unit-associates-pp
 
5067
                 (:instance
 
5068
                  Member-unit-associate-=-member-unit-associate-pp
 
5069
                  (lst lst1))
 
5070
                 (:instance
 
5071
                  Member-unit-associate-=-member-unit-associate-pp
 
5072
                  (lst lst2))))))
 
5073
 
 
5074
(defun
 
5075
  Multiplicity-unit-associate (x lst)
 
5076
  (if (consp lst)
 
5077
      (if (unit-associates-p x (car lst))
 
5078
          (+ 1 (multiplicity-unit-associate x (cdr lst)))
 
5079
          (multiplicity-unit-associate x (cdr lst)))
 
5080
      0))
 
5081
 
 
5082
(defun
 
5083
  Multiplicity-unit-associate-pp (x lst)
 
5084
  (if (consp lst)
 
5085
      (if (unit-associates-pp x (car lst))
 
5086
          (+ 1 (multiplicity-unit-associate-pp x (cdr lst)))
 
5087
          (multiplicity-unit-associate-pp x (cdr lst)))
 
5088
      0))
 
5089
 
 
5090
(defthm
 
5091
  Multiplicity-unit-associate-=-Multiplicity-unit-associate-pp
 
5092
  (equal (Multiplicity-unit-associate x lst)
 
5093
         (Multiplicity-unit-associate-pp x lst))
 
5094
  :rule-classes nil
 
5095
  :hints (("Subgoal *1/2"
 
5096
           :use (:instance 
 
5097
                 Unit-associates-p-=-unit-associates-pp
 
5098
                 (y (car lst))))
 
5099
          ("Subgoal *1/1"
 
5100
           :use (:instance 
 
5101
                 Unit-associates-p-=-unit-associates-pp
 
5102
                 (y (car lst))))))
 
5103
 
 
5104
(defthm
 
5105
  Multiplicity-unit-associate-pp-delete-one-unit-associate-pp-1
 
5106
  (implies (and (member-unit-associate-pp y lst)
 
5107
                (unit-associates-pp x y))
 
5108
           (equal (+ 1 (multiplicity-unit-associate-pp 
 
5109
                        x 
 
5110
                        (delete-one-unit-associate-pp y lst)))
 
5111
                  (multiplicity-unit-associate-pp x lst))))
 
5112
 
 
5113
(defthm
 
5114
  Multiplicity-unit-associate-pp-delete-one-unit-associate-pp-2
 
5115
  (implies (not (unit-associates-pp x y))
 
5116
           (equal (multiplicity-unit-associate-pp 
 
5117
                   x 
 
5118
                   (delete-one-unit-associate-pp y lst))
 
5119
                  (multiplicity-unit-associate-pp x lst))))
 
5120
 
 
5121
(defthm
 
5122
  Bag-equal-unit-associates-pp->equal-multiplicity-unit-associate-pp 
 
5123
  (implies (bag-equal-unit-associates-pp lst1 lst2)
 
5124
           (equal (multiplicity-unit-associate-pp x lst1)
 
5125
                  (multiplicity-unit-associate-pp x lst2)))
 
5126
  :rule-classes nil)
 
5127
 
 
5128
(defthm
 
5129
  Bag-equal-unit-associates->equal-multiplicity-unit-associate 
 
5130
  (implies (bag-equal-unit-associates lst1 lst2)
 
5131
           (equal (multiplicity-unit-associate x lst1)
 
5132
                  (multiplicity-unit-associate x lst2)))
 
5133
  :rule-classes nil
 
5134
  :hints (("Goal"
 
5135
           :use (Bag-equal-unit-associates-pp->equal-multiplicity-unit-associate-pp
 
5136
                 Bag-equal-unit-associates-=-Bag-equal-unit-associates-pp
 
5137
                 (:instance 
 
5138
                  Multiplicity-unit-associate-=-Multiplicity-unit-associate-pp
 
5139
                  (lst lst1))
 
5140
                 (:instance 
 
5141
                  Multiplicity-unit-associate-=-Multiplicity-unit-associate-pp
 
5142
                  (lst lst2))))))
 
5143
 
 
5144
(defthm
 
5145
  Divides-pp-member-unit-associate-pp-**_e-lst
 
5146
  (implies (and (edp-listp lst)
 
5147
                (member-unit-associate-pp x lst))
 
5148
           (divides-pp x (**_e-lst lst)))
 
5149
  :hints (("Goal"
 
5150
           :in-theory (disable (:definition divides-pp)
 
5151
                               unit-associates-pp-refines-associates-pp-lemma-1
 
5152
                               irreducible-listp-implies-edp-listp
 
5153
                               irreducible-listp-1-implies-edp-listp))))
 
5154
 
 
5155
(defthm
 
5156
  Divisors-of-irreducible-pp
 
5157
  (implies (and (irreducible-pp x)
 
5158
                (divides-pp d x))
 
5159
           (or (unit-associates-pp d x)
 
5160
               (unit-pp d)))
 
5161
  :rule-classes nil
 
5162
  :hints (("Goal"
 
5163
           :in-theory (e/d ((:definition divides-pp))
 
5164
                           ((:definition unit-pp)
 
5165
                            (:definition reducible-pp)))
 
5166
           :use (:instance 
 
5167
                 unit-associates-pp-suff
 
5168
                 (u (divides-pp-witness d x))
 
5169
                 (x d)
 
5170
                 (y x)))))
 
5171
 
 
5172
(defthm
 
5173
  Gcd-pp-of-irreducible-pp
 
5174
  (implies (and (irreducible-pp x)
 
5175
                (gcd-pp x y g))
 
5176
           (or (unit-associates-pp g x)
 
5177
               (unit-pp g)))
 
5178
  :rule-classes nil
 
5179
  :hints (("Goal"
 
5180
           :in-theory (disable (:definition irreducible-pp))
 
5181
           :use (:instance
 
5182
                 Divisors-of-irreducible-pp
 
5183
                 (d g)))))
 
5184
 
 
5185
(defthm
 
5186
  Gcd-pp-of-irreducible-pp-divides-pp
 
5187
  (implies (and (irreducible-pp x)
 
5188
                (gcd-pp x y g))
 
5189
           (or (divides-pp x y)
 
5190
               (unit-pp g)))
 
5191
  :rule-classes nil
 
5192
  :hints (("Goal"
 
5193
           :in-theory (disable (:definition irreducible-pp))
 
5194
           :use Gcd-pp-of-irreducible-pp)))
 
5195
 
 
5196
(defthm
 
5197
  Unit-pp-Bezout
 
5198
  (implies (and (edp x)
 
5199
                (irreducible-pp x)
 
5200
                (edp y)
 
5201
                (not (divides-pp x y)))
 
5202
           (unit-pp (++_e (**_e x (first  (Bezout x y)))
 
5203
                          (**_e y (second (Bezout x y))))))
 
5204
  :hints (("Goal"
 
5205
           :use (gcd-pp-Bezout
 
5206
                 (:instance
 
5207
                  Gcd-pp-of-irreducible-pp-divides-pp
 
5208
                  (g (++_e (**_e x (first  (Bezout x y)))
 
5209
                           (**_e y (second (Bezout x y))))))))))
 
5210
 
 
5211
(defthm
 
5212
  Associate-pp-unit-pp
 
5213
  (implies (and (unit-pp x)
 
5214
                (unit-pp y))
 
5215
           (equal (associates-pp x y) t)))
 
5216
 
 
5217
(defthm
 
5218
  Irreducible-pp-gcd=1_e
 
5219
  (implies (and (irreducible-pp x)
 
5220
                (edp y) 
 
5221
                (not (divides-pp x y)))
 
5222
           (gcd-pp x y (1_e)))
 
5223
  :hints (("Goal"
 
5224
           :in-theory (disable (:definition associates-pp)
 
5225
                               (:definition bezout)
 
5226
                               (:definition unit-pp)
 
5227
                               (:definition gcd-pp)
 
5228
                               unit-associates-pp-refines-associates-pp-lemma-1
 
5229
                               Unit-pp-Bezout)
 
5230
           :use ((:instance
 
5231
                  Associate-pp-unit-pp
 
5232
                  (x (++_e (**_e x (first  (Bezout x y)))
 
5233
                           (**_e y (second (Bezout x y)))))
 
5234
                  (y (1_e)))
 
5235
                 Unit-pp-Bezout))))
 
5236
 
 
5237
(defthm
 
5238
  Edp-linear-combination
 
5239
  (implies (gcd-pp x y g)
 
5240
           (edp (divides-pp-witness (++_e (**_e x (mv-nth 0 (bezout x y)))
 
5241
                                          (**_e y (mv-nth 1 (bezout x y))))
 
5242
                                    g)))
 
5243
  :hints (("goal"
 
5244
           :in-theory (disable (:definition bezout)
 
5245
                               (:definition mv-nth)))))
 
5246
 
 
5247
(in-theory (disable unit-associates-pp-refines-associates-pp-lemma-1))
 
5248
 
 
5249
(set-backchain-limit 3)
 
5250
 
 
5251
(defthm
 
5252
  Prime-property-lemma
 
5253
  (implies (and (gcd-pp x y (1_e))
 
5254
                (divides-pp x (**_e y z))
 
5255
                (edp z))
 
5256
           (divides-pp x z))
 
5257
  :hints (("goal"
 
5258
           :in-theory (disable (:definition gcd-pp)
 
5259
                               (:definition bezout)
 
5260
                               (:definition mv-nth)
 
5261
                               gcd=linear-combination)
 
5262
           :use ((:instance
 
5263
                  (:theorem
 
5264
                   (implies (==_e x y)
 
5265
                            (==_e (**_e x z)
 
5266
                                  (**_e y z))))
 
5267
                  (x (++_e (**_e x 
 
5268
                                 (mv-nth 0 (bezout x y))
 
5269
                                 (divides-pp-witness 
 
5270
                                  (++_e (**_e x (mv-nth 0 (bezout x y)))
 
5271
                                        (**_e y (mv-nth 1 (bezout x y))))
 
5272
                                  (1_e)))
 
5273
                           (**_e y 
 
5274
                                 (mv-nth 1 (bezout x y))
 
5275
                                 (divides-pp-witness 
 
5276
                                  (++_e (**_e x (mv-nth 0 (bezout x y)))
 
5277
                                        (**_e y (mv-nth 1 (bezout x y))))
 
5278
                                  (1_e)))))
 
5279
                  (y (1_e)))
 
5280
                 (:instance
 
5281
                  gcd=linear-combination
 
5282
                  (g (1_e)))
 
5283
                 (:instance 
 
5284
                  (:theorem
 
5285
                   (implies (and (edp c)
 
5286
                                 (edp d)
 
5287
                                 (divides-pp x a)
 
5288
                                 (divides-pp x b))
 
5289
                            (divides-pp x (++_e (**_e a c)
 
5290
                                                (**_e b d)))))
 
5291
                  (a x)
 
5292
                  (b (**_e y z))
 
5293
                  (c (**_e z
 
5294
                           (mv-nth 0 (bezout x y))
 
5295
                           (divides-pp-witness 
 
5296
                            (++_e (**_e x 
 
5297
                                        (mv-nth 0 (bezout x y)))
 
5298
                                  (**_e y
 
5299
                                        (mv-nth 1 (bezout x y))))
 
5300
                            (1_e))))
 
5301
                  (d (**_e (mv-nth 1 (bezout x y))
 
5302
                           (divides-pp-witness 
 
5303
                            (++_e (**_e x 
 
5304
                                        (mv-nth 0 (bezout x y)))
 
5305
                                  (**_e y (mv-nth 1 (bezout x y))))
 
5306
                            (1_e)))))))))
 
5307
 
 
5308
(defthm
 
5309
  Irreducible-pp-implies-prime-property
 
5310
  (implies (and (irreducible-pp x)
 
5311
                (edp y)
 
5312
                (edp z)
 
5313
                (divides-pp x (**_e y z)))
 
5314
           (or (divides-pp x y)
 
5315
               (divides-pp x z)))
 
5316
  :rule-classes ((:rewrite
 
5317
                  :corollary
 
5318
                  (and (implies (and (irreducible-pp x)
 
5319
                                     (divides-pp x (**_e y z))
 
5320
                                     (edp y)
 
5321
                                     (edp z)
 
5322
                                     (not (divides-pp x y)))
 
5323
                                (divides-pp x z))
 
5324
                       (implies (and (irreducible-pp x)
 
5325
                                     (divides-pp x (**_e y z))
 
5326
                                     (edp y)
 
5327
                                     (edp z)
 
5328
                                     (not (divides-pp x z)))
 
5329
                                (divides-pp x y)))))
 
5330
  :hints (("Goal"
 
5331
           :in-theory (disable (:definition gcd-pp)
 
5332
                               (:definition irreducible-pp)
 
5333
                               Irreducible-pp-gcd=1_e)
 
5334
           :use Irreducible-pp-gcd=1_e)))
 
5335
 
 
5336
(defthm
 
5337
  Irreducible-p-implies-prime-property
 
5338
  (implies (and (irreducible-p x)
 
5339
                (edp y)
 
5340
                (edp z)
 
5341
                (divides-p x (*_e y z)))
 
5342
           (or (divides-p x y)
 
5343
               (divides-p x z)))
 
5344
  :rule-classes nil
 
5345
  :hints (("Goal"
 
5346
           :in-theory (disable Irreducible-pp-implies-prime-property
 
5347
                               (:definition irreducible-pp)
 
5348
                               (:definition irreducible-p)
 
5349
                               (:definition divides-p))
 
5350
           :use (Irreducible-pp-implies-prime-property
 
5351
                 Irreducible-p-=-irreducible-pp
 
5352
                 Divides-p-=-Divides-pp
 
5353
                 (:instance
 
5354
                  Divides-p-=-Divides-pp
 
5355
                  (y z))
 
5356
                 (:instance
 
5357
                  Divides-p-=-Divides-pp
 
5358
                  (y (*_e y z)))
 
5359
                 (:instance
 
5360
                  *_e-=-**_e
 
5361
                  (x y)
 
5362
                  (y z))))))
 
5363
 
 
5364
(defthm
 
5365
  Irreducible-pp-unit-associates
 
5366
  (implies (and (divides-pp x y)
 
5367
                (not (unit-pp x))
 
5368
                (irreducible-pp y))
 
5369
           (equal (unit-associates-pp x y) t))
 
5370
  :hints (("Goal"
 
5371
           :in-theory (e/d ((:definition divides-pp))
 
5372
                           ((:definition irreducible-pp)
 
5373
                            (:definition unit-pp)))
 
5374
           :use ((:instance
 
5375
                  irreducible-pp-implies-unit-pp-factor
 
5376
                  (x y)
 
5377
                  (y x)
 
5378
                  (z (divides-pp-witness x y)))
 
5379
                 (:instance
 
5380
                  unit-associates-pp-suff
 
5381
                  (u (divides-pp-witness x y)))))))
 
5382
 
 
5383
(defthm
 
5384
  Irreducible-p-unit-associates
 
5385
  (implies (and (divides-p x y)
 
5386
                (not (unit-p x))
 
5387
                (irreducible-p y))
 
5388
           (unit-associates-p x y))
 
5389
  :rule-classes nil
 
5390
  :hints (("Goal"
 
5391
           :in-theory (disable Irreducible-pp-unit-associates
 
5392
                               (:definition irreducible-pp)
 
5393
                               (:definition irreducible-p)
 
5394
                               (:definition unit-pp)
 
5395
                               (:definition unit-p)
 
5396
                               (:definition unit-associates-pp)
 
5397
                               (:definition unit-associates-p))
 
5398
           :use (Irreducible-pp-unit-associates
 
5399
                 Divides-p-=-Divides-pp
 
5400
                 Unit-p-=-Unit-pp
 
5401
                 (:instance
 
5402
                  Irreducible-p-=-irreducible-pp
 
5403
                  (x y))
 
5404
                 Unit-associates-p-=-unit-associates-pp))))
 
5405
 
 
5406
(defthm
 
5407
  Edp-Irreducible-pp
 
5408
  (implies (irreducible-pp x)
 
5409
           (edp x))
 
5410
  :rule-classes :forward-chaining)
 
5411
 
 
5412
(defthm
 
5413
  Divides-pp-**_e-lst-implies-member-unit-associate-lemma
 
5414
  (implies (and (irreducible-pp x)
 
5415
                (not (unit-pp x))
 
5416
                (edp-listp lst)
 
5417
                (irreducible-listp-1 lst)
 
5418
                (divides-pp x (**_e-lst lst)))
 
5419
           (member-unit-associate-pp x lst))
 
5420
  :hints (("Goal"
 
5421
           :in-theory (disable irreducible-listp-implies-edp-listp
 
5422
                               (:definition irreducible-pp)))))
 
5423
 
 
5424
(defthm
 
5425
  Irreducible-pp-not-unit-pp
 
5426
  (implies (irreducible-pp x)
 
5427
           (not (unit-pp x)))
 
5428
  :rule-classes :forward-chaining)
 
5429
 
 
5430
(defthm
 
5431
  Divides-pp-**_e-lst-implies-member-unit-associate-pp
 
5432
  (implies (and (irreducible-pp x)
 
5433
                (irreducible-listp-1 lst)
 
5434
                (divides-pp x (**_e-lst lst)))
 
5435
           (member-unit-associate-pp x lst))
 
5436
  :hints (("Goal"
 
5437
           :in-theory (disable (:definition irreducible-pp)))))
 
5438
 
 
5439
(defthm
 
5440
  Edp-Unit-associates-pp-witness
 
5441
  (implies (and (edp x)
 
5442
                (unit-associates-pp x y))
 
5443
          (edp (unit-associates-pp-witness x y)))
 
5444
  :hints (("Goal"
 
5445
           :in-theory (e/d ((:definition unit-associates-pp))
 
5446
                           ((:definition unit-pp))))))
 
5447
 
 
5448
(defthm
 
5449
  ==_e-**_e-Unit-associates-pp-witness
 
5450
  (implies (and (edp x)
 
5451
                (unit-associates-pp x y))
 
5452
           (==_e (**_e x (unit-associates-pp-witness x y)) y))
 
5453
  :hints (("Goal"
 
5454
           :in-theory (e/d ((:definition unit-associates-pp))
 
5455
                           ((:definition unit-pp))))))
 
5456
 
 
5457
(defthm
 
5458
  ==_e-**_e-Unit-associates-pp-witness-1
 
5459
  (implies (and (edp x)
 
5460
                (unit-associates-pp (**_e x (**_e-lst lst1))
 
5461
                                    (**_e-lst lst2)))
 
5462
           (==_e (**_e x 
 
5463
                       (**_e-lst lst1)
 
5464
                       (unit-associates-pp-witness (**_e x (**_e-lst lst1))
 
5465
                                                   (**_e-lst lst2)))
 
5466
                 (**_e-lst lst2)))
 
5467
  :hints (("Goal"
 
5468
           :in-theory (disable ==_e-**_e-Unit-associates-pp-witness
 
5469
                               (:definition unit-pp))
 
5470
           :use (:instance
 
5471
                 ==_e-**_e-Unit-associates-pp-witness
 
5472
                 (x (**_e x (**_e-lst lst1)))
 
5473
                 (y (**_e-lst lst2))))))
 
5474
 
 
5475
(defthm
 
5476
  **_e-irreducible-pp-**_e-lst-implies-member-unit-associate-pp-lemma
 
5477
  (implies (and (unit-associates-pp (**_e x (**_e-lst lst1))
 
5478
                                    (**_e-lst lst2))
 
5479
                (edp x))
 
5480
           (divides-pp x (**_e-lst lst2)))
 
5481
  :hints (("Goal"
 
5482
           :in-theory (disable (:definition unit-pp))
 
5483
           :use (:instance
 
5484
                 divides-pp-suff
 
5485
                 (y (**_e-lst lst2))
 
5486
                 (z (**_e (unit-associates-pp-witness (**_e x (**_e-lst lst1))
 
5487
                                                      (**_e-lst lst2))
 
5488
                          (**_e-lst lst1)))))))
 
5489
 
 
5490
(defthm
 
5491
  **_e-irreducible-pp-**_e-lst-implies-member-unit-associate-pp
 
5492
  (implies (and (unit-associates-pp (**_e x (**_e-lst lst1))
 
5493
                                    (**_e-lst lst2))
 
5494
                (irreducible-pp x)
 
5495
                (irreducible-listp-1 lst2))
 
5496
           (member-unit-associate-pp x lst2))
 
5497
  :hints (("Goal"
 
5498
           :in-theory (disable (:definition reducible-pp)
 
5499
                               (:definition unit-pp)))))
 
5500
 
 
5501
(defthm
 
5502
  **_e-lst-of-irreducible-listp-1-not-unit-associate-pp-1_e
 
5503
  (implies (and (irreducible-listp-1 lst)
 
5504
                (consp lst))
 
5505
           (not (unit-associates-pp (1_e)(**_e-lst lst))))
 
5506
  :hints (("Goal"
 
5507
           :in-theory (disable (:definition unit-p)
 
5508
                               (:definition reducible-pp)))))
 
5509
 
 
5510
(defthm
 
5511
  Irreducible-listp-1-delete-one-unit-associate-pp
 
5512
  (implies (and (member-unit-associate-pp x lst)
 
5513
                (irreducible-listp-1 lst))
 
5514
           (irreducible-listp-1 (delete-one-unit-associate-pp x lst)))
 
5515
  :hints (("Goal"
 
5516
           :in-theory (disable (:definition unit-pp)
 
5517
                               (:definition reducible-pp)))))
 
5518
 
 
5519
(defthm
 
5520
  Unit-associates-pp-**_e-lst-implies-member-unit-associate-pp
 
5521
  (implies (and (irreducible-pp x)
 
5522
                (irreducible-listp-1 lst)
 
5523
                (unit-associates-pp x (**_e-lst lst)))
 
5524
           (member-unit-associate-pp x lst))
 
5525
  :hints (("goal"
 
5526
           :in-theory (disable (:definition reducible-pp)
 
5527
                               (:definition unit-pp)))))
 
5528
 
 
5529
(set-backchain-limit 1)
 
5530
 
 
5531
(defthm
 
5532
  Reducible-pp-**_e
 
5533
  (implies (and (edp x)
 
5534
                (reducible-pp y))
 
5535
           (reducible-pp (**_e x y)))
 
5536
  :rule-classes ((:rewrite
 
5537
                  :corollary
 
5538
                  (implies (and (edp x)
 
5539
                                (reducible-pp y))
 
5540
                           (and (reducible-pp (**_e x y))
 
5541
                                (reducible-pp (**_e y x))))
 
5542
                  :hints (("Goal"
 
5543
                           :in-theory (disable (:definition reducible-pp))))))
 
5544
  :hints (("goal"
 
5545
           :in-theory (disable (:definition unit-pp)
 
5546
                               (:definition mv-nth)
 
5547
                               (:rewrite reducible-pp-suff))
 
5548
           :use ((:instance
 
5549
                  reducible-pp-suff
 
5550
                  (x (**_e x y))
 
5551
                  (y (**_e x (mv-nth 0 (reducible-pp-witness y))))
 
5552
                  (z (mv-nth 1 (reducible-pp-witness y))))
 
5553
                 (:instance
 
5554
                  unit-pp-**_e=>unit-pp-factor-right
 
5555
                  (y (mv-nth 0 (reducible-pp-witness y))))))))
 
5556
 
 
5557
(defthm
 
5558
  Reducible-pp-**_e-1
 
5559
  (implies (and (edp x)
 
5560
                (edp y)
 
5561
                (not (unit-pp x))
 
5562
                (not (unit-pp y)))
 
5563
           (reducible-pp (**_e x y)))
 
5564
  :hints (("goal"
 
5565
           :in-theory (disable (:definition reducible-pp)
 
5566
                               (:definition unit-pp))
 
5567
           :use (:instance
 
5568
                 reducible-pp-suff
 
5569
                 (x (**_e x y))
 
5570
                 (y x)
 
5571
                 (z y)))))
 
5572
 
 
5573
(defthm
 
5574
  Reducible-pp-**_e-lst
 
5575
  (implies (and (irreducible-listp-1 lst)
 
5576
                (consp lst)
 
5577
                (consp (cdr lst)))
 
5578
           (reducible-pp (**_e-lst lst)))
 
5579
  :hints (("goal"
 
5580
           :in-theory (disable (:definition reducible-pp)
 
5581
                               (:definition unit-pp)))))
 
5582
 
 
5583
(defthm
 
5584
  Not-irreducible-pp-1_e
 
5585
  (not (irreducible-pp (1_e))))
 
5586
 
 
5587
(defthm
 
5588
  Irreducible-listp-1-irreducible-pp-member-unit-associate-pp
 
5589
  (implies (and (member-unit-associate-pp x lst)
 
5590
                (irreducible-listp-1 lst))
 
5591
           (irreducible-pp x))
 
5592
  :hints (("Goal"
 
5593
           :in-theory (disable (:definition irreducible-pp)))))
 
5594
 
 
5595
(set-backchain-limit 3)
 
5596
 
 
5597
(defthm
 
5598
  Unit-associates-pp-**_e-lst-implies-member-unit-associate-pp-1
 
5599
  (implies (and (unit-associates-pp (**_e-lst lst1)
 
5600
                                    (**_e-lst lst2))
 
5601
                (irreducible-listp-1 lst1)
 
5602
                (irreducible-listp-1 lst2)
 
5603
                (member-unit-associate-pp x lst1))
 
5604
           (member-unit-associate-pp x lst2))
 
5605
  :hints (("Goal"
 
5606
           :in-theory (disable (:definition member-unit-associate-pp)))))
 
5607
 
 
5608
(defthm
 
5609
  Member-unit-associate-pp-edp-listp-implies-edp
 
5610
  (implies (and (member-unit-associate-pp x lst)
 
5611
                (edp-listp lst))
 
5612
           (edp x)))
 
5613
 
 
5614
(defthm
 
5615
  Unit-pp-unit-associates-pp-witness
 
5616
  (implies (and (edp x)
 
5617
                (unit-associates-pp x y))
 
5618
           (unit-pp (unit-associates-pp-witness x y)))
 
5619
  :rule-classes nil
 
5620
  :hints (("Goal"
 
5621
           :in-theory (e/d ((:definition unit-associates-pp))
 
5622
                           ((:definition unit-pp))))))
 
5623
 
 
5624
(defthm
 
5625
  ==_e-**_e-Unit-associates-pp-witness-a
 
5626
  (implies (and (edp x)
 
5627
                (edp z)
 
5628
                (unit-associates-pp x y))
 
5629
           (==_e (**_e x z (unit-associates-pp-witness x y))
 
5630
                 (**_e y z)))
 
5631
  :rule-classes nil
 
5632
  :hints (("Goal"
 
5633
           :in-theory (disable ==_e-**_e-Unit-associates-pp-witness
 
5634
                               cancellation-laws-for-**_e
 
5635
                               ==_e-implies-==_e-**_e-1)
 
5636
           :use (==_e-**_e-Unit-associates-pp-witness
 
5637
                 (:instance
 
5638
                  ==_e-implies-==_e-**_e-1
 
5639
                  (y1 (**_e x (unit-associates-pp-witness x y)))
 
5640
                  (y2 y))))))
 
5641
 
 
5642
(defthm
 
5643
  Unit-associates-pp-**_e-1
 
5644
  (implies (and (unit-associates-pp x y)
 
5645
                (edp x)
 
5646
                (edp z))
 
5647
           (unit-associates-pp (**_e x z)
 
5648
                               (**_e y z)))
 
5649
  :rule-classes nil
 
5650
  :hints (("Goal"
 
5651
           :in-theory (disable (:definition unit-pp))
 
5652
           :use ((:instance
 
5653
                  unit-associates-pp-suff
 
5654
                  (x (**_e x z))
 
5655
                  (y (**_e y z))
 
5656
                  (u (unit-associates-pp-witness x y)))
 
5657
                 Unit-pp-unit-associates-pp-witness
 
5658
                 ==_e-**_e-Unit-associates-pp-witness-a))))
 
5659
 
 
5660
(defthm
 
5661
  Unit-associates-pp-==_e-**_e-2
 
5662
  (implies (and (unit-associates-pp x y)
 
5663
                (edp x)
 
5664
                (edp z))
 
5665
           (unit-associates-pp (**_e z x)
 
5666
                               (**_e z y)))
 
5667
  :rule-classes nil
 
5668
  :hints (("Goal"
 
5669
           :use Unit-associates-pp-**_e-1)))
 
5670
 
 
5671
(defthm
 
5672
  Unit-associates-pp-**_e-**_e-lst-delete-one-unit-associate-lemma
 
5673
  (implies (and (unit-associates-pp 
 
5674
                 (**_e x (**_e-lst (delete-one-unit-associate-pp x (cdr lst))))
 
5675
                 (**_e-lst (cdr lst)))
 
5676
                (edp (car lst))
 
5677
                (edp-listp (cdr lst))
 
5678
                (member-unit-associate-pp x (cdr lst)))
 
5679
           (unit-associates-pp (**_e x 
 
5680
                                     (car lst)
 
5681
                                     (**_e-lst 
 
5682
                                      (delete-one-unit-associate-pp x 
 
5683
                                                                    (cdr lst))))
 
5684
                               (**_e (car lst) (**_e-lst (cdr lst)))))
 
5685
 :hints (("goal"
 
5686
          :in-theory (disable (:definition unit-pp))
 
5687
          :use (:instance
 
5688
                Unit-associates-pp-==_e-**_e-2
 
5689
                (z (car lst))
 
5690
                (x (**_e x (**_e-lst (delete-one-unit-associate-pp x (cdr lst)))))
 
5691
                (y (**_e-lst (cdr lst)))))))
 
5692
 
 
5693
(defthm
 
5694
  Unit-associates-pp-**_e-**_e-lst-delete-one-unit-associate
 
5695
  (implies (and (edp-listp lst)
 
5696
                (member-unit-associate-pp x lst))
 
5697
           (unit-associates-pp (**_e x (**_e-lst 
 
5698
                                        (delete-one-unit-associate-pp x
 
5699
                                                                      lst)))
 
5700
                               (**_e-lst lst)))
 
5701
  :hints (("Goal"
 
5702
           :in-theory (disable (:definition unit-pp)))
 
5703
          ("Subgoal *1/1"
 
5704
           :use (:instance
 
5705
                 Unit-associates-pp-**_e-1
 
5706
                 (z (**_e-lst (cdr lst)))
 
5707
                 (y (car lst))))))
 
5708
 
 
5709
(defthm
 
5710
  Unit-associates-pp-**_e-cancellation
 
5711
  (implies (and (unit-associates-pp (**_e x y)
 
5712
                                    (**_e x z))
 
5713
                (not (==_e x (0_e)))
 
5714
                (edp x)
 
5715
                (edp y)
 
5716
                (edp z))
 
5717
           (unit-associates-pp y z))
 
5718
  :rule-classes nil
 
5719
  :hints (("Goal"
 
5720
           :in-theory (e/d ((:definition unit-associates-pp))
 
5721
                           ((:definition unit-pp)))
 
5722
           :use (:instance
 
5723
                 unit-associates-pp-suff
 
5724
                 (x y)
 
5725
                 (y z) 
 
5726
                 (u (unit-associates-pp-witness (**_e x y)
 
5727
                                                (**_e x z)))))))
 
5728
 
 
5729
(defthm
 
5730
  Unit-associates-pp-**_e-**_e-lst-delete-one-unit-associate-pp-cancellation
 
5731
  (implies (and (unit-associates-pp (**_e x (**_e-lst lst1))
 
5732
                                    (**_e-lst lst2))
 
5733
                (irreducible-pp x)
 
5734
                (edp-listp lst1)
 
5735
                (irreducible-listp-1 lst2))
 
5736
           (unit-associates-pp (**_e-lst (delete-one-unit-associate-pp x lst2))
 
5737
                               (**_e-lst lst1)))
 
5738
  :hints (("Goal"
 
5739
           :in-theory (disable (:definition reducible-pp)
 
5740
                               (:definition unit-pp))
 
5741
           :use (Irreducible-pp-not-0_e
 
5742
                 (:instance
 
5743
                  Unit-associates-pp-**_e-cancellation
 
5744
                  (y (**_e-lst (delete-one-unit-associate-pp x lst2)))
 
5745
                  (z (**_e-lst lst1)))))))
 
5746
 
 
5747
(defthm
 
5748
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general-1
 
5749
  (implies (and (irreducible-listp-1 lst1)
 
5750
                (irreducible-listp-1 lst2)
 
5751
                (unit-associates-pp (**_e-lst lst1)
 
5752
                                    (**_e-lst lst2)))
 
5753
          (bag-equal-unit-associates-pp lst1 lst2))
 
5754
  :hints (("Goal"
 
5755
           :in-theory (disable (:definition reducible-pp)
 
5756
                               (:definition unit-pp)))))
 
5757
 
 
5758
(defthm
 
5759
  Irreducible-listp-=-irreducible-listp-1
 
5760
  (equal (irreducible-listp lst)
 
5761
         (irreducible-listp-1 lst))
 
5762
  :rule-classes nil
 
5763
  :hints (("Subgoal *1/2"
 
5764
           :in-theory (disable (:definition irreducible-pp)
 
5765
                               (:definition irreducible-p))
 
5766
           :use (:instance
 
5767
                 Irreducible-p-=-irreducible-pp
 
5768
                 (x (car lst))))
 
5769
          ("Subgoal *1/1"
 
5770
           :in-theory (disable (:definition irreducible-pp)
 
5771
                               (:definition irreducible-p))
 
5772
           :use (:instance
 
5773
                 Irreducible-p-=-irreducible-pp
 
5774
                 (x (car lst))))))
 
5775
 
 
5776
(defthm
 
5777
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general
 
5778
  (implies (and (irreducible-listp lst1)
 
5779
                (irreducible-listp lst2)
 
5780
                (unit-associates-p (*_e-lst lst1)
 
5781
                                   (*_e-lst lst2)))
 
5782
          (bag-equal-unit-associates lst1 lst2))
 
5783
  :hints (("Goal"
 
5784
           :use (IRREDUCIBLE-FACTORIZATION-UNIQUENESS-general-1
 
5785
                 (:instance
 
5786
                  Irreducible-listp-=-irreducible-listp-1
 
5787
                  (lst lst1))
 
5788
                 (:instance
 
5789
                  Irreducible-listp-=-irreducible-listp-1
 
5790
                  (lst lst2))
 
5791
                 (:instance
 
5792
                  *_e-lst-=-**_e-lst
 
5793
                  (lst lst1))
 
5794
                 (:instance
 
5795
                  *_e-lst-=-**_e-lst
 
5796
                  (lst lst2))
 
5797
                 (:instance 
 
5798
                  unit-associates-p-=-unit-associates-pp
 
5799
                  (x (*_e-lst lst1))
 
5800
                  (y (*_e-lst lst2)))
 
5801
                 bag-equal-unit-associates-=-bag-equal-unit-associates-pp))))
 
5802
 
 
5803
(defthm
 
5804
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS-1
 
5805
  (implies (and (irreducible-listp-1 lst1)
 
5806
                (irreducible-listp-1 lst2)
 
5807
                (==_e (**_e-lst lst1)
 
5808
                      (**_e-lst lst2)))
 
5809
          (bag-equal-unit-associates-pp lst1 lst2))
 
5810
  :rule-classes nil
 
5811
  :hints (("Goal"
 
5812
           :in-theory (disable (:definition irreducible-pp)))))
 
5813
 
 
5814
(defthm
 
5815
  IRREDUCIBLE-FACTORIZATION-UNIQUENESS
 
5816
  (implies (and (irreducible-listp lst1)
 
5817
                (irreducible-listp lst2)
 
5818
                (=_e (*_e-lst lst1)
 
5819
                     (*_e-lst lst2)))
 
5820
          (bag-equal-unit-associates lst1 lst2))
 
5821
  :rule-classes nil
 
5822
  :hints (("Goal"
 
5823
           :use (IRREDUCIBLE-FACTORIZATION-UNIQUENESS-1
 
5824
                 (:instance
 
5825
                  Irreducible-listp-=-irreducible-listp-1
 
5826
                  (lst lst1))
 
5827
                 (:instance
 
5828
                  Irreducible-listp-=-irreducible-listp-1
 
5829
                  (lst lst2))
 
5830
                 (:instance
 
5831
                  *_e-lst-=-**_e-lst
 
5832
                  (lst lst1))
 
5833
                 (:instance
 
5834
                  *_e-lst-=-**_e-lst
 
5835
                  (lst lst2))
 
5836
                 (:instance
 
5837
                  =_e-=-==_e
 
5838
                  (x (*_e-lst lst1))
 
5839
                  (y (*_e-lst lst2)))
 
5840
                 bag-equal-unit-associates-=-bag-equal-unit-associates-pp))))