number-list-defuns

Included Books

other

(in-package "ACL2")

include-book

(include-book "list-defuns")

other

(deflabel number-list-defuns-section)

real/rational-listpmacro

(defmacro real/rational-listp (x) `(rational-listp ,X))

naturalpmacro

(defmacro naturalp (x) `(and (integerp ,X) (<= 0 ,X)))

natural-listpfunction

(defun natural-listp
  (l)
  "Recognize a list of naturals."
  (declare (xargs :guard t))
  (cond ((atom l) (eq l nil))
    (t (and (naturalp (car l)) (natural-listp (cdr l))))))

maxlistfunction

(defun maxlist
  (l)
  "The largest element of a non-empty list of real/rationals."
  (declare (xargs :guard (and (real/rational-listp l) (consp l))))
  (cond ((endp (cdr l)) (car l))
    (t (max (car l) (maxlist (cdr l))))))

minlistfunction

(defun minlist
  (l)
  "The smallest element of a non-empty list of real/rationals."
  (declare (xargs :guard (and (real/rational-listp l) (consp l))))
  (cond ((endp (cdr l)) (car l))
    (t (min (car l) (minlist (cdr l))))))

sumfunction

(defun sum
  (l)
  "The sum of the elements of a list of real/rationals."
  (declare (xargs :guard (real/rational-listp l)))
  (cond ((endp l) 0) (t (+ (car l) (sum (cdr l))))))

excess-naturalfunction

(defun excess-natural
  (l)
  "The least upper bound of a list of naturals."
  (declare (xargs :guard (natural-listp l)))
  (if (consp l)
    (+ 1 (maxlist l))
    0))

numerically-sortedfunction

(defun numerically-sorted
  (l)
  "Recognize a list of real/rationals sorted in ascending order."
  (declare (xargs :guard (real/rational-listp l)))
  (cond ((endp l) t)
    ((endp (cdr l)) t)
    (t (and (<= (car l) (cadr l)) (numerically-sorted (cdr l))))))

numeric-insertfunction

(defun numeric-insert
  (x l)
  "Insert the real/rational x immediately before the first element of
   list L that is larger than x."
  (declare (xargs :guard (and (real/rationalp x) (real/rational-listp l))))
  (cond ((endp l) (list x))
    ((< (car l) x) (cons (car l) (numeric-insert x (cdr l))))
    (t (cons x l))))

numeric-sortfunction

(defun numeric-sort
  (l)
  "Sort a list of real/rationals into ascending order."
  (declare (xargs :guard (real/rational-listp l)))
  (cond ((endp l) nil)
    (t (numeric-insert (car l) (numeric-sort (cdr l))))))

real/rationalp-maxlisttheorem

(defthm real/rationalp-maxlist
  (implies (and (real/rational-listp l) (consp l))
    (real/rationalp (maxlist l)))
  :rule-classes (:rewrite :type-prescription))

real/rationalp-minlisttheorem

(defthm real/rationalp-minlist
  (implies (and (real/rational-listp l) (consp l))
    (real/rationalp (minlist l)))
  :rule-classes (:rewrite :type-prescription))

real/rationalp-sumtheorem

(defthm real/rationalp-sum
  (implies (real/rational-listp l) (real/rationalp (sum l)))
  :rule-classes (:rewrite :type-prescription))

naturalp-excess-naturaltheorem

(defthm naturalp-excess-natural
  (implies (natural-listp l) (naturalp (excess-natural l)))
  :rule-classes (:rewrite :type-prescription))

real/rational-listp-numeric-inserttheorem

(defthm real/rational-listp-numeric-insert
  (implies (and (real/rationalp x) (real/rational-listp l))
    (real/rational-listp (numeric-insert x l)))
  :rule-classes (:rewrite :type-prescription))

real/rational-listp-numeric-sorttheorem

(defthm real/rational-listp-numeric-sort
  (implies (real/rational-listp l)
    (real/rational-listp (numeric-sort l)))
  :rule-classes (:rewrite :type-prescription))

other

(deftheory number-list-defuns
  (set-difference-theories (current-theory :here)
    (current-theory 'number-list-defuns-section)))