number-list-defthms

other

(in-package "ACL2")

include-book

(include-book "number-list-defuns")

include-book

(include-book "deflist")

other

(deflabel number-list-defthms-section)

real/rational-listpmacro

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

other

(deflist rational-listp
  (l)
  rationalp
  (:options :omit-defun))

other

(deflist integer-listp (l) integerp (:options :omit-defun))

other

(deflist natural-listp
  (l)
  (lambda (x) (naturalp x))
  (:options :omit-defun))

natural-listp-forward-to-integer-listptheorem

(defthm natural-listp-forward-to-integer-listp
  (implies (natural-listp l) (integer-listp l))
  :rule-classes :forward-chaining)

integer-listp-forward-to-eqlable-listptheorem

(defthm integer-listp-forward-to-eqlable-listp
  (implies (integer-listp l) (eqlable-listp l)))

<=maxlisttheorem

(defthm <=maxlist
  (implies (member-equal x l) (<= x (maxlist l)))
  :rule-classes (:rewrite :linear :forward-chaining))

minlist<=theorem

(defthm minlist<=
  (implies (member-equal x l) (<= (minlist l) x))
  :rule-classes (:rewrite :linear :forward-chaining))

member-equal-maxlisttheorem

(defthm member-equal-maxlist
  (implies (and (real/rational-listp l) (consp l))
    (member-equal (maxlist l) l)))

member-equal-minlisttheorem

(defthm member-equal-minlist
  (implies (and (real/rational-listp l) (consp l))
    (member-equal (minlist l) l)))

member-equal-excess-naturaltheorem

(defthm member-equal-excess-natural
  (implies (natural-listp l)
    (not (member-equal (excess-natural l) l)))
  :hints (("Goal" :do-not-induct t
     :use ((:instance <=maxlist (x (excess-natural l)) (l l)))
     :in-theory (disable <=maxlist))))

numerically-sorted-numeric-inserttheorem

(defthm numerically-sorted-numeric-insert
  (implies (and (real/rationalp x)
      (real/rational-listp l)
      (numerically-sorted l))
    (numerically-sorted (numeric-insert x l)))
  :hints (("Goal" :induct (numeric-insert x l))))

numerically-sorted-numeric-sorttheorem

(defthm numerically-sorted-numeric-sort
  (implies (real/rational-listp l)
    (numerically-sorted (numeric-sort l))))

other

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

number-list-defthms

Included Books