lexicographic-book

Included Books

ordinals-without-arithmetic top-with-meta

other

(in-package "ACL2")

include-book

(include-book "ordinals-without-arithmetic")

local

(local (include-book "top-with-meta"))

lexpfunction

(defun lexp
  (x)
  (declare (xargs :guard t))
  (or (natp x) (and (consp x) (nat-listp x))))

d<function

(defun d<
  (x y)
  (declare (xargs :guard (and (nat-listp x) (nat-listp y))))
  (and (consp x)
    (consp y)
    (or (< (car x) (car y))
      (and (= (car x) (car y)) (d< (cdr x) (cdr y))))))

l<function

(defun l<
  (x y)
  (declare (xargs :guard (and (lexp x) (lexp y))))
  (or (< (len x) (len y))
    (and (= (len x) (len y))
      (if (atom x)
        (< x y)
        (d< x y)))))

lsttoofunction

(defun lsttoo
  (x)
  (declare (xargs :guard (nat-listp x)))
  (if (endp x)
    0
    (o+ (o* (o^ (omega) (len x)) (1+ (car x))) (lsttoo (cdr x)))))

ltoofunction

(defun ltoo
  (x)
  (declare (xargs :guard (lexp x)))
  (if (atom x)
    (mbe :logic (nfix x) :exec x)
    (lsttoo x)))

o-p-lsttootheorem

(defthm o-p-lsttoo (implies (nat-listp x) (o-p (lsttoo x))))

local

(local (defthm len-0 (equal (equal (len x) 0) (atom x))))

ltoo-0theorem

(defthm ltoo-0
  (implies (nat-listp y)
    (equal (equal (lsttoo y) 0) (equal y nil))))

o-first-expt-ltootheorem

(defthm o-first-expt-ltoo
  (implies (and (consp x) (nat-listp x))
    (equal (o-first-expt (lsttoo x)) (len x))))

o-first-coeff-ltooencapsulate

(encapsulate nil
  (local (defthm o-first-coeff-ltoo-helper
      (implies (and (consp x)
          (natp (car x))
          (equal (o-first-coeff (lsttoo (cdr x))) (1+ (cadr x)))
          (nat-listp (cdr x)))
        (equal (o-first-coeff (o+ (o* (o^ (omega) (1+ (len (cdr x)))) (1+ (car x)))
              (lsttoo (cdr x))))
          (1+ (car x))))
      :hints (("goal" :use (:instance o-first-expt-ltoo (x (cdr x)))))))
  (defthm o-first-coeff-ltoo
    (implies (and (consp x) (nat-listp x))
      (equal (o-first-coeff (lsttoo x)) (1+ (car x))))))

local

(local (in-theory (enable o<)))

well-founded-l<-case-2encapsulate

(encapsulate nil
  (local (defthm well-founded-l<-case-2-helper
      (implies (and (consp y)
          (not (d< (cdr x) (cdr y)))
          (consp x)
          (nat-listp x)
          (nat-listp y)
          (equal (len x) (len y))
          (d< x y))
        (o< (lsttoo x) (lsttoo y)))
      :hints (("goal" :use ((:instance o-first-expt-ltoo) (:instance o-first-expt-ltoo (x y))
           (:instance o-first-coeff-ltoo)
           (:instance o-first-coeff-ltoo (x y)))))))
  (local (defthm well-founded-l<-case-2-helper-2
      (implies (and (consp y)
          (not (d< (cdr x) (cdr y)))
          (consp x)
          (nat-listp x)
          (nat-listp y)
          (equal (len x) (len y))
          (d< x y))
        (o< (lsttoo x) (lsttoo y)))
      :hints (("goal" :in-theory (disable lsttoo)))
      :rule-classes :forward-chaining))
  (defthm well-founded-l<-case-2
    (implies (and (consp x)
        (nat-listp x)
        (consp y)
        (nat-listp y)
        (equal (len x) (len y))
        (d< x y))
      (o< (lsttoo x) (lsttoo y)))))

well-founded-l<theorem

(defthm well-founded-l<
  (and (implies (lexp x) (o-p (ltoo x)))
    (implies (and (lexp x) (lexp y) (l< x y))
      (o< (ltoo x) (ltoo y))))
  :rule-classes :well-founded-relation)

llist-macrofunction

(defun llist-macro
  (lst)
  (declare (xargs :guard t))
  (if (consp lst)
    `((nfix ,(CAR LST)) ,@(LLIST-MACRO (CDR LST)))
    nil))

llistmacro

(defmacro llist (&rest lst) (cons 'list (llist-macro lst)))