← 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/fld-u-poly/fucongruencias-suma.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/fld-u-poly/fucongruencias-suma.lisp
 
1
; ACL2 Univariate Polynomials over a Field books -- Sum Congruences
 
2
;; Congruences for Sums of Univariate Polynomials over a Field
 
3
; Copyright (C) 2006  John R. Cowles and Ruben A. Gamboa, University of
 
4
; 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
;; Modified by J. Cowles
 
21
 
 
22
;;   Last modified July 2006 (for ACL2 Version 3.0).
 
23
 
 
24
;; Based on
 
25
;;; ------------------------------------------------------------------
 
26
;;; Congruencia de la igualdad con la suma de polinomios
 
27
;;;
 
28
;;; Autores:
 
29
;;;
 
30
;;; Inmaculada Medina Bulo
 
31
;;; Francisco Palomo Lozano
 
32
;;;
 
33
;;; Descripci�n:
 
34
;;;
 
35
;;; Aqu� se demuestran las congruencias de la igualdad de polinomios
 
36
;;; con la suma. Las demostraciones son complejas debido a que
 
37
;;; necesitan reglas expansivas. Estas reglas son peligrosas, ya que
 
38
;;; pueden producir f�cilmente ciclos en el demostrador. Para
 
39
;;; restringir su aplicaci�n caben dos opciones:
 
40
;;;
 
41
;;; 1. Desactivarlas y usarlas expl�citamente donde sea necesario. Una
 
42
;;; variante es no generar la regla en absoluto (es decir, introducir
 
43
;;; el teorema con la clases de reglas vac�a).
 
44
;;;
 
45
;;; 2. Restringir su aplicaci�n sint�cticamente para prevenir
 
46
;;; expansiones en cadena. Esto se puede lograr graciasa syntaxp.
 
47
;;;
 
48
;;; Elegimos la segunda opci�n porque se consigue un mayor grado de
 
49
;;; automatizaci�n y hace a las demostraciones menos sensibles a los
 
50
;;; cambios.
 
51
;;; ------------------------------------------------------------------
 
52
#|
 
53
To certify this book, first, create a world with the following packages:
 
54
 
 
55
(in-package "ACL2")
 
56
 
 
57
(defconst *import-symbols*
 
58
  (set-difference-eq
 
59
   (union-eq *acl2-exports*
 
60
             *common-lisp-symbols-from-main-lisp-package*)
 
61
     '(null + * - < = / commutativity-of-* associativity-of-* 
 
62
            commutativity-of-+ associativity-of-+ distributivity)))
 
63
 
 
64
(defpkg "FLD"
 
65
  *import-symbols*)
 
66
 
 
67
(defpkg "FUTER"
 
68
  *import-symbols*)
 
69
 
 
70
(defpkg "FUMON"
 
71
  (union-eq *import-symbols*
 
72
            '(FLD::fdp FUTER::terminop)))
 
73
 
 
74
(defpkg "FUPOL"
 
75
  (union-eq *import-symbols*
 
76
            '(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
 
77
                            FUMON::termino FUMON::monomiop)))
 
78
 
 
79
(certify-book "fucongruencias-suma"
 
80
              5
 
81
              nil ;;compile-flg
 
82
              )
 
83
|#
 
84
(in-package "FUPOL")
 
85
 
 
86
;;(include-book "suma")
 
87
(include-book "fusuma"
 
88
              :load-compiled-file nil)
 
89
 
 
90
;;; ----------------------------------------------------
 
91
;;; Congruencia de la igualdad de polinomios con la suma
 
92
;;; ----------------------------------------------------
 
93
 
 
94
;;; Segundo par�metro
 
95
 
 
96
;;; NOTA:
 
97
;;;
 
98
;;; Esta propiedad es expansiva; restringimos su aplicaci�n sint�cticamente
 
99
 
 
100
(defthm
 
101
  polinomiop-implies-true-listp
 
102
  (implies (polinomiop p)
 
103
           (true-listp p))
 
104
  :rule-classes :compound-recognizer)
 
105
 
 
106
(defthm
 
107
  Right-identity-append
 
108
  (implies (true-listp p)
 
109
           (equal (append p nil) p)))
 
110
 
 
111
(defthm |p + q = p + fn(q)|
 
112
  (implies (syntaxp (not (and (consp q) (eq (primero q) 'fn))))
 
113
           (= (+ p q) (+ p (fn q)))))
 
114
 
 
115
(defthm
 
116
  =P-implies-=P-append-1
 
117
  (implies (=P p1 p2)
 
118
           (=P (append p1 q)
 
119
               (append p2 q)))
 
120
  :rule-classes :congruence)
 
121
 
 
122
(defthm
 
123
  =P-implies-=P-append-2
 
124
  (implies (=P q1 q2)
 
125
           (=P (append p q1)
 
126
               (append p q2)))
 
127
  :rule-classes :congruence)
 
128
 
 
129
(defthm
 
130
  =P-implies-=P-fn
 
131
  (implies (=P p1 p2)
 
132
           (=P (fn p1)
 
133
               (fn p2)))
 
134
  :rule-classes :congruence)
 
135
 
 
136
;;(defcong = = (+ p q) 2)
 
137
(defthm
 
138
  =-implies-=-+-2
 
139
  (implies (= q1 q2)
 
140
           (= (+ p q1)
 
141
              (+ p q2)))
 
142
  :rule-classes :congruence)
 
143
 
 
144
;;; Primer par�metro
 
145
 
 
146
;; (defcong = = (+ p q) 1
 
147
;;   :hints (("Goal"
 
148
;;         :in-theory (disable |p + q = q + p| + =)
 
149
;;         :use (|p + q = q + p|
 
150
;;               (:instance |p + q = q + p| (p p-equiv))))))
 
151
(defthm
 
152
  =-implies-=-+-1
 
153
  (implies (= p1 p2)
 
154
           (= (+ p1 q)
 
155
              (+ p2 q)))
 
156
  :rule-classes :congruence
 
157
  :hints (("Goal"
 
158
           :in-theory (disable |p + q = q + p| + =)
 
159
           :use ((:instance
 
160
                  |p + q = q + p|
 
161
                  (p p1))
 
162
                 (:instance 
 
163
                  |p + q = q + p|
 
164
                  (p p2))))))
 
165
 
 
166
;;; NOTA:
 
167
;;;
 
168
;;; Esta propiedad es expansiva; restringimos su aplicaci�n sint�cticamente
 
169
 
 
170
(defthm |p + q = fn(p) + q|
 
171
  (implies (syntaxp (not (and (consp p) (eq (primero p) 'fn))))
 
172
           (= (+ p q) (+ (fn p) q)))
 
173
  :hints (("Goal"
 
174
           :in-theory (disable |p + q = p + fn(q)|)
 
175
           :use ((:instance |p + q = p + fn(q)| (p q) (q p))))))
 
176
 
 
177
(defthm |fn(p) + fn(q) = p + q|
 
178
  (= (+ (fn p) (fn q)) (+ p q)))
 
179
 
 
180
(in-theory (disable |p + q = p + fn(q)|
 
181
                    |p + q = fn(p) + q|
 
182
                    |fn(p) + fn(q) = p + q|))