Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

13 files changed, 655 insertions, 0 deletions

diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/README b/books/workshops/2002/medina-palomo-alonso/support/section-3/README
new file mode 100644
index 0000000..e5b4c55
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/README
@@ -0,0 +1,62 @@
+     Implementation in ACL2 of Well-Founded Polynomial Orderings
+
+The code under this directory explains the ideas behind section 3 in
+an abstract setting, hiding implementation details and properties
+which are not detailed in the corresponding paper. It has been tested
+under ACL2 2.6/GCL 2.4.
+
+* *.acl2:
+
+Package definitions (TER, MON, UPOL and NPOL) and certification commands.
+
+* term.lisp:
+
+Terms (TER package). An encapsulation of the term ordering, the
+ordinal embedding and their properties (mainly the well-foundedness of
+the term ordering). See [1] for implementation details.
+
+* monomial.lisp:
+
+Monomials (MON package). The monomial ordering, the ordinal embedding
+and their properties (mainly the well-foundedness of the monomial
+ordering.
+
+* upol.lisp:
+
+Unnormalized polynomials (UPOL package). It just implements the
+recognizers for unnormalized polynomials and objects in normal
+form. The remaining functions of the polynomial encapsulation
+presented in section 2 are not needed to implement the polynomial
+ordering.
+
+* ordinal-ordering.lisp:
+
+Some useful theorems about the ordinal ordering, e0-ord-<. It is
+proved that e0-ord-< is a partial strict order.
+
+* npol-ordering-1.lisp:
+
+Normalized polynomials (NPOL package). It explains how the monomial
+ordering is lifted to normalized polynomials. It is assumed that the
+monomial ordinal embedding does not produce zero.
+
+* npol-ordering-2.lisp:
+
+Normalized polynomials (NPOL package). It explains how the monomial
+ordering is lifted to normalized polynomials. In this case it is not
+assumed that the monomial ordinal embedding is not zero. It is shown
+that it is always possible to build a modified ordinal embedding
+holding this property without imposing any additional constraint. This
+approach has the advantage of separating two concerns: the development
+of monomial orderings and the development of induced polynomial
+orderings.
+
+Encapsulated events are developed in (event names may have changed):
+
+[1] Medina Bulo, I., Alonso Jiménez, J. A., Palomo Lozano, F.:
+    Automatic Verification of Polynomial Rings Fundamental Properties in ACL2.  
+    The University of Texas at Austin, Department of Computer Sciences.	
+    Technical Report 0029 (2000)
+
+Inmaculada Medina Bulo		Francisco Palomo Lozano
+inmaculada.medina@uca.es	francisco.palomo@uca.es
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.acl2
new file mode 100644
index 0000000..fe75ad7
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "monomial" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.lisp
new file mode 100644
index 0000000..25afbf2
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/monomial.lisp
@@ -0,0 +1,119 @@
+;;; ---------
+;;; Monomials
+;;; ---------
+
+(in-package "MON")
+
+(include-book "term")
+
+;;; ---------
+;;; Functions
+;;; ---------
+
+(deflabel start-of-functions)
+
+;;; Recognizer.
+
+(defun monomialp (a)
+  (declare (xargs :guard t))
+  (and (consp a)
+       (acl2-numberp (first a))
+       (termp (rest a))))
+
+;;; ...
+
+;;; Coefficient.
+
+(defun coefficient (a)
+  (declare (xargs :guard (consp a)))
+  (first a))
+
+;;; Term.
+
+(defun term (a)
+  (declare (xargs :guard (consp a)))
+  (rest a))
+
+;;; Recognizer for null monomials.
+
+(defun nullp (a)
+  (declare (xargs :guard (consp a)))
+  (equal (coefficient a) 0))
+
+;;; Term equality.
+
+(defun =T (a b)
+  (declare (xargs :guard (and (consp a) (consp b))))
+  (equal (term a) (term b)))
+
+;;; Monomial ordering.
+
+(defun < (a b)
+  (declare (xargs :guard (and (consp a) (consp b))))
+  (TER::< (term a) (term b)))
+
+;;; Ordinal embedding.
+
+(defun monomial->o-p (a)
+  (declare (xargs :guard (consp a)))
+  (term->o-p (term a)))
+
+;;; The theory of monomial functions.
+
+(deftheory functions
+  (set-difference-theories (universal-theory :here)
+                           (universal-theory 'start-of-functions)))
+
+;;; ----------
+;;; Properties
+;;; ----------
+
+;;; Equivalence and congruences.
+
+(defequiv =T)
+
+(defcong =T equal (term a) 1)
+(defcong =T equal (< a b) 1)
+(defcong =T equal (< a b) 2)
+(defcong =T equal (monomial->o-p a) 1)
+
+;;; ...
+
+;;; The monomial ordering is a partial strict order.
+
+(defthm |~(a < a)|
+  (not (< a a)))
+
+(defthm |a < b & b < c => a < c|
+  (implies (and (< a b) (< b c)) (< a c)))
+
+;;; Antisymmetry of the monomial ordering.
+
+(defthm |a < b => ~(b < a)|
+  (implies (< a b)
+	   (not (< b a)))
+  :hints (("Goal"
+	   :in-theory (disable |a < b & b < c => a < c|)
+	   :use (:instance |a < b & b < c => a < c| (c a)))))
+
+;;; The ordinal embedding does not produce 0.
+
+(defthm |~(monomial->o-p(a) = 0)|
+  (not (equal (monomial->o-p a) 0)))
+
+;;; Well-foundedness of the monomial ordering.
+
+(defthm well-foundedness-of-<
+  (and (implies (monomialp a)
+		(o-p (monomial->o-p a)))
+       (implies (and (monomialp a) (monomialp b)
+		     (< a b))
+		(o< (monomial->o-p a)
+		    (monomial->o-p b))))
+  :rule-classes (:rewrite :well-founded-relation))
+
+;;; +++++++++++++++++++
+;;; Abstraction barrier
+;;; +++++++++++++++++++
+
+(in-theory (disable functions))
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.acl2
new file mode 100644
index 0000000..348f2bb
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "npol-ordering-1" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.lisp
new file mode 100644
index 0000000..219fe30
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-1.lisp
@@ -0,0 +1,84 @@
+;;; ----------------------
+;;; Normalized polynomials
+;;; ----------------------
+
+(in-package "NPOL")
+
+(include-book "upol")
+(include-book "ordinal-ordering")
+(include-book "../../../../../ordinals/ordinals-without-arithmetic")
+
+;;; ---------
+;;; Functions
+;;; ---------
+
+;;; Recognizer.
+
+(defun polynomialp (p)
+  (declare (xargs :guard t))
+  (and (UPOL::polynomialp p) (UPOL::nfp p)))
+
+;;; ...
+
+;;; Polynomial ordering.
+
+(defun < (p q)
+  (declare (xargs :guard (and (polynomialp p) (polynomialp q))))
+  (cond ((or (endp p) (endp q))
+         (not (endp q)))
+	((MON::=T (first p) (first q))
+         (< (rest p) (rest q)))
+        (t
+         (MON::< (first p) (first q)))))
+
+;;; Ordinal embedding.
+
+(defun polynomial->o-p (p)
+  (declare (xargs :guard (polynomialp p)))
+  (if (endp p)
+      0
+    (make-ord (monomial->o-p (first p))
+	      1
+	      (polynomial->o-p (rest p)))))
+
+;;; ----------
+;;; Properties
+;;; ----------
+
+;;; ...
+
+;;; The polynomial ordering is a partial strict order.
+
+(defthm |~(p < p)|
+  (not (< p p)))
+
+(defthm |p < q & q < r => p < r|
+  (implies (and (< p q) (< q r))
+	   (< p r)))
+
+;;; Antisymmetry of the polynomial ordering.
+
+(defthm |p < q => ~(q < p)|
+  (implies (< p q)
+	   (not (< q p)))
+  :hints (("Goal"
+	   :in-theory (disable |p < q & q < r => p < r|)
+	   :use (:instance |p < q & q < r => p < r| (r p)))))
+
+;;; Correctness of the ordinal embedding.
+
+(defthm correctness-of-polynomial->o-p
+  (implies (polynomialp p)
+           (o-p (polynomial->o-p p))))
+
+;;; Well-foundedness of the polynomial ordering.
+
+(defthm well-foundedness-of-<
+  (and (implies (polynomialp p)
+                (o-p (polynomial->o-p p)))
+       (implies (and (polynomialp p) (polynomialp q)
+                     (< p q))
+                (o< (polynomial->o-p p)
+                    (polynomial->o-p q))))
+  :hints (("Goal" :in-theory (enable acl2::|a < b  =>  ~(a = b)|)))
+  :rule-classes :well-founded-relation)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.acl2
new file mode 100644
index 0000000..c3f3e08
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "npol-ordering-2" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.lisp
new file mode 100644
index 0000000..7d77229
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/npol-ordering-2.lisp
@@ -0,0 +1,129 @@
+;;; ----------------------
+;;; Normalized polynomials
+;;; ----------------------
+
+; Includes mods for v2-8 for ordinal changes.
+
+(in-package "NPOL")
+
+(include-book "upol")
+(include-book "ordinal-ordering")
+(include-book "../../../../../ordinals/ordinals-without-arithmetic")
+
+;;; NOTE:
+;;;
+;;; From now on we won't assume that the ordinal embedding of a
+;;; term/monomial is not zero. Instead, it will be shown that it is
+;;; always possible to build a modified ordinal embedding holding this
+;;; property without imposing any additional constraint. This approach
+;;; has the advantage of separating two concerns: the development of
+;;; monomial orderings and the development of induced polynomial
+;;; orderings.
+
+(in-theory (disable TER::|~(term->o-p(a) = 0)|
+		    MON::|~(monomial->o-p(a) = 0)|))
+
+;;; ---------
+;;; Functions
+;;; ---------
+
+;;; Recognizer.
+
+(defun polynomialp (p)
+  (declare (xargs :guard t))
+  (and (UPOL::polynomialp p) (UPOL::nfp p)))
+
+;;; ...
+
+;;; Polynomial ordering.
+
+(defun < (p q)
+  (declare (xargs :guard (and (polynomialp p) (polynomialp q))))
+  (cond ((or (endp p) (endp q))
+         (not (endp q)))
+	((MON::=T (first p) (first q))
+         (< (rest p) (rest q)))
+        (t
+         (MON::< (first p) (first q)))))
+
+;;; Modified monomial ordinal embedding.
+
+(defun modified-monomial->o-p (a)
+  (declare (xargs :guard (monomialp a)
+		  :guard-hints (("goal"
+				 :in-theory (enable monomialp)))))
+  (acl2::o+ (monomial->o-p a) 1))
+
+;;; Polynomial ordinal embedding.
+
+(defun polynomial->o-p (p)
+  (declare (xargs :guard (polynomialp p)))
+  (if (endp p)
+      0
+    (make-ord (modified-monomial->o-p (first p))
+	      1
+	      (polynomial->o-p (rest p)))))
+
+;;; ----------
+;;; Properties
+;;; ----------
+
+;;; ...
+
+;;; The polynomial ordering is a partial strict order.
+
+(defthm |~(p < p)|
+  (not (< p p)))
+
+(defthm |p < q & q < r => p < r|
+  (implies (and (< p q) (< q r))
+	   (< p r)))
+
+;;; Antisymmetry of the polynomial ordering.
+
+(defthm |p < q => ~(q < p)|
+  (implies (< p q)
+	   (not (< q p)))
+  :hints (("Goal"
+	   :in-theory (disable |p < q & q < r => p < r|)
+	   :use (:instance |p < q & q < r => p < r| (r p)))))
+
+;;; Congruence.
+
+(defcong MON::=T equal (modified-monomial->o-p a) 1)
+
+;;; The monomial ordinal embedding does not produce 0.
+
+(defthm |~(modified-monomial->o-p(a) = 0)|
+  (implies (monomialp a)
+	   (not (equal (modified-monomial->o-p a) 0))))
+
+;;; Well-foundedness of the monomial ordering w.r.t. the modified
+;;; monomial ordinal embedding.
+
+(defthm modified-well-foundedness-of-<
+  (and (implies (monomialp a)
+		(o-p (modified-monomial->o-p a)))
+       (implies (and (monomialp a) (monomialp b)
+		     (MON::< a b))
+		(o< (modified-monomial->o-p a)
+			  (modified-monomial->o-p b))))
+  :rule-classes (:rewrite :well-founded-relation))
+
+;;; Correctness of the polynomial ordinal embedding.
+
+(defthm correctness-of-polynomial->o-p
+  (implies (polynomialp p)
+           (o-p (polynomial->o-p p))))
+
+;;; Well-foundedness of the polynomial ordering.
+
+(defthm well-foundedness-of-<
+  (and (implies (polynomialp p)
+                (o-p (polynomial->o-p p)))
+       (implies (and (polynomialp p) (polynomialp q)
+                     (< p q))
+                (o< (polynomial->o-p p)
+                    (polynomial->o-p q))))
+  :hints (("Goal" :in-theory (enable acl2::|a < b  =>  ~(a = b)|)))
+  :rule-classes :well-founded-relation)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.acl2
new file mode 100644
index 0000000..0ccc96f
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "ordinal-ordering" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.lisp
new file mode 100644
index 0000000..7c89c38
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/ordinal-ordering.lisp
@@ -0,0 +1,22 @@
+;;; ----------------
+;;; Ordinal ordering
+;;; ----------------
+
+(in-package "ACL2")
+
+;;; The ordinal ordering is a partial strict order.
+
+(defthm |~(a o< a)|
+  (not (o< a a)))
+
+(defthm |a o< b & b o< c => a o< c|
+  (implies (and (o< a b) (o< b c)) (o< a c)))
+
+;;; Antisymmetry of the ordinal ordering.
+
+(defthm |a o< b => ~(b o< a)|
+  (implies (o< a b)
+           (not (o< b a)))
+  :hints (("Goal"
+	   :in-theory (disable |a o< b & b o< c => a o< c|)
+	   :use (:instance |a o< b & b o< c => a o< c| (c a)))))
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2
new file mode 100644
index 0000000..6ff70ab
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "term" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/term.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.lisp
new file mode 100644
index 0000000..e17da65
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/term.lisp
@@ -0,0 +1,64 @@
+;;; -----
+;;; Terms
+;;; -----
+
+(in-package "TER")
+
+(encapsulate
+  ((termp (a) t)
+   ;;; ...
+   (< (a b) t)
+   (term->o-p (a) t))
+
+  ;;; ---------------
+  ;;; Local witnesses
+  ;;; ---------------
+
+  ;;; Recognizer.
+
+  (local
+    (defun termp (a)
+      (acl2-numberp a)))
+
+  ;;; ...
+
+  ;;; Term ordering.
+
+  (local
+    (defun < (a b)
+      (o< (nfix a) (nfix b))))
+
+  ;;; Ordinal embedding.
+
+  (local
+    (defun term->o-p (a)
+      (+ (nfix a) 1)))
+
+  ;;; ------
+  ;;; Axioms
+  ;;; ------
+
+  ;;; ...
+
+  ;;; The term ordering is a partial strict order.
+
+  (defthm |~(a < a)|
+    (not (< a a)))
+
+  (defthm |a < b & b < c => a < c|
+    (implies (and (< a b) (< b c)) (< a c)))
+
+  ;;; The ordinal embedding does not produce 0.
+
+  (defthm |~(term->o-p(a) = 0)|
+    (not (equal (term->o-p a) 0)))
+
+  ;;; Well-foundedness of the term ordering.
+
+  (defthm well-foundedness-of-<
+    (and (implies (termp a)
+		  (o-p (term->o-p a)))
+	 (implies (and (termp a) (termp b)
+		       (< a b))
+		  (o< (term->o-p a) (term->o-p b))))
+    :rule-classes (:rewrite :well-founded-relation)))
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.acl2 b/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.acl2
new file mode 100644
index 0000000..fc28c2f
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.acl2
@@ -0,0 +1,24 @@
+;;; --------
+;;; Packages
+;;; --------
+
+(defconst *acl2-and-lisp-exports*
+  (set-difference-eq ; modified 5/26/2015 by Matt K.
+   (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*)
+   '(termp)))
+
+(defpkg "TER"
+  (set-difference-eq *acl2-and-lisp-exports* '(<)))
+
+(defpkg "MON"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(TER::termp TER::term->o-p)))
+
+(defpkg "UPOL"
+  (union-eq *acl2-and-lisp-exports* '(MON::monomialp)))
+
+(defpkg "NPOL"
+  (union-eq (set-difference-eq *acl2-and-lisp-exports* '(<))
+	    '(MON::monomialp MON::monomial->o-p ACL2::make-ord)))
+
+(certify-book "upol" ? t)
diff --git a/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.lisp b/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.lisp
new file mode 100644
index 0000000..264eb11
--- /dev/null
+++ b/books/workshops/2002/medina-palomo-alonso/support/section-3/upol.lisp
@@ -0,0 +1,31 @@
+;;; ------------------------
+;;; Unnormalized polynomials
+;;; ------------------------
+
+(in-package "UPOL")
+
+(include-book "monomial")
+
+;;; Recognizer.
+
+(defun polynomialp (p)
+  (declare (xargs :guard t))
+  (if (atom p)
+      (equal p nil)
+    (and (monomialp (first p))
+	 (polynomialp (rest p)))))
+
+;;; Recognizer for objects in normal form.
+
+(defun nfp (p)
+  (declare (xargs :guard t))
+  (if (atom p)
+      (equal p nil)
+    (and (consp (first p))
+	 (not (MON::nullp (first p)))
+	 (or (atom (rest p))
+	     (and (consp (second p))
+		  (MON::< (second p) (first p))))
+	 (nfp (rest p)))))
+
+;;; ...