1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
; ACL2 Univariate Polynomials over a Field books -- (Unnormalized) Polynomials
; Copyright (C) 2006 John R. Cowles and Ruben A. Gamboa, University of
; Wyoming
; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
;; Modified by J. Cowles
;; Last modified July 2006 (for ACL2 Version 3.0).
;; Based on
;;; -------------------------------------------------------------------
;;; Polinomios
;;;
;;; Autores:
;;;
;;; Inmaculada Medina Bulo
;;; Francisco Palomo Lozano
;;;
;;; Descripción:
;;;
;;; Representación abstracta de los polinomios mediante listas propias
;;; de ACL2 formadas por monomios que contienen coeficientes y
;;; términos abstractos.
;;; -------------------------------------------------------------------
#|
To certify this book, first, create a world with the following packages:
(in-package "ACL2")
(defconst *import-symbols*
(set-difference-eq
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*)
'(null + * - < = / commutativity-of-* associativity-of-*
commutativity-of-+ associativity-of-+ distributivity)))
(defpkg "FLD"
*import-symbols*)
(defpkg "FUTER"
*import-symbols*)
(defpkg "FUMON"
(union-eq *import-symbols*
'(FLD::fdp FUTER::terminop)))
(defpkg "FUPOL"
(union-eq *import-symbols*
'(FUTER::naturalp FUTER::terminop FUMON::monomio FUMON::coeficiente
FUMON::termino FUMON::monomiop)))
(certify-book "fupolinomio"
5
nil ;;compile-flg
)
|#
(in-package "FUPOL")
;;(include-book "monomio")
(include-book "fumonomio"
:load-compiled-file nil)
;;; ---------
;;; Funciones
;;; ---------
;;; Accesores
(defmacro primero (p)
`(first ,p))
(defmacro resto (p)
`(rest ,p))
;;; Reconocedor
(defun polinomiop (p)
(if (atom p)
(equal p nil)
(and (monomiop (primero p)) (polinomiop (resto p)))))
;;; Polinomio nulo en forma normal
;;; NOTA:
;;;
;;; Posteriormente definiremos la igualdad semántica entre
;;; polinomios. Entonces, esta definición corresponderá al
;;; representante canónico de la clase de equivalencia formada por los
;;; polinomios nulos.
(defmacro nulo () nil)
;;; NOTA:
;;;
;;; La siguiente versión se emplea en los casos base de las funciones
;;; recursivas que trabajan con polinomios.
(defmacro nulop (p)
`(atom ,p))
;;; -----------
;;; Propiedades
;;; -----------
;;; Clausura
(defthm polinomiop-resto
(implies (polinomiop p)
(polinomiop (resto p)))
:rule-classes :type-prescription)
|
