Filtering...

e0-ordinal

books/ordinals/e0-ordinal

Included Books

ordinal-definitions top ordinal-isomorphism
other
(in-package "ACL2")
include-book
(include-book "ordinal-definitions")
include-book
(include-book "xdoc/top" :dir :system)
local
(local (include-book "ordinal-isomorphism"))
other
(defsection e0-ord-<
  :parents (ordinals)
  :short "The old ordering function for ACL2 ordinals."
  :long "<p>See @(see o<) for the current new ordering function for ACL2
ordinals.</p>

<p>The functions @('e0-ordinalp') and @(see e0-ord-<) were replaced in ACL2
Version 2.8 by @(see o-p) and @(see o<), respectively.  However, books created
before that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.</p>

<p>To use the old functions in termination proofs, you can do:</p>

@({
    (include-book "ordinals/e0-ordinal" :dir :system)
    (set-well-founded-relation e0-ord-<)
})

<p>See @(see set-well-founded-relation).</p>

<p>For a more thorough discussion of these functions, see the documentation at
the end of community book @('ordinals/e0-ordinal.lisp').</p>"
  (defun e0-ord-<
    (x y)
    (declare (xargs :guard t))
    (if (consp x)
      (if (consp y)
        (if (e0-ord-< (car x) (car y))
          t
          (if (equal (car x) (car y))
            (e0-ord-< (cdr x) (cdr y))
            nil))
        nil)
      (if (consp y)
        t
        (< (if (real/rationalp x)
            x
            0)
          (if (real/rationalp y)
            y
            0))))))
other
(defsection e0-ordinalp
  :parents (ordinals)
  :short "The old recognizer for ACL2 ordinals."
  :long "<p>See @(see o-p) for the current recognizer for ACL2 ordinals.</p>

<p>The functions @('e0-ordinalp') and @(see e0-ord-<) were replaced in ACL2
Version 2.8 by @(see o-p) and @(see o<), respectively.  However, books created
before that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.</p>

<p>To use the old functions in termination proofs, you can do:</p>

@({
    (include-book "ordinals/e0-ordinal" :dir :system)
    (set-well-founded-relation e0-ord-<)
})

<p>See @(see set-well-founded-relation).</p>

<p>For a more thorough discussion of these functions, see the documentation at
the end of community book @('ordinals/e0-ordinal.lisp').</p>"
  (defun e0-ordinalp
    (x)
    (declare (xargs :guard t))
    (if (consp x)
      (and (e0-ordinalp (car x))
        (not (equal (car x) 0))
        (e0-ordinalp (cdr x))
        (or (atom (cdr x)) (not (e0-ord-< (car x) (cadr x)))))
      (and (integerp x) (>= x 0)))))
copynfunction
(defun copyn
  (a n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
    nil
    (cons a (copyn a (1- n)))))
ctoafunction
(defun ctoa
  (x)
  (declare (xargs :guard (o-p x)))
  (if (o-finp x)
    x
    (append (copyn (ctoa (o-first-expt x)) (o-first-coeff x))
      (ctoa (o-rst x)))))
ctoa-<-equivtheorem
(defthm ctoa-<-equiv
  (implies (and (o-p x) (o-p y))
    (equal (e0-ord-< (ctoa x) (ctoa y)) (o< x y))))
|oc.x <=> oa(ctoa.x)|theorem
(defthm |oc.x  <=>  oa(ctoa.x)|
  (implies (o-p x) (e0-ordinalp (ctoa x)))
  :rule-classes ((:forward-chaining) (:rewrite)))
other
(verify-guards ocmp)
other
(verify-guards ob+)
atocfunction
(defun atoc
  (a)
  (declare (xargs :guard (e0-ordinalp a)))
  (if (atom a)
    a
    (o+ (omega-term (atoc (car a)) 1) (atoc (cdr a)))))
|oa.x <=> oc(atoc.x)|theorem
(defthm |oa.x  <=>  oc(atoc.x)|
  (implies (e0-ordinalp x) (o-p (atoc x))))
atoc-<-equivtheorem
(defthm atoc-<-equiv
  (implies (and (e0-ordinalp x) (e0-ordinalp y))
    (equal (o< (atoc x) (atoc y)) (e0-ord-< x y))))
e0-ordinal-well-founded-cnftheorem
(defthm e0-ordinal-well-founded-cnf
  (and (implies (e0-ordinalp x) (o-p (atoc x)))
    (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-< x y))
      (o< (atoc x) (atoc y))))
  :rule-classes :well-founded-relation)
in-theory
(in-theory (disable atoc ctoa))