num-list-fns - ACL2 Book

other

(in-package "DEFDATA")

other

(set-verify-guards-eagerness 2)

2+-listpfunction

(defun 2+-listp
  (x)
  (if (atom x)
    (null x)
    (and (integerp (car x))
      (<= 2 (car x))
      (2+-listp (cdr x)))))

pos-listpfunction

(defun pos-listp
  (l)
  (declare (xargs :guard t))
  (cond ((atom l) (eq l nil))
    (t (and (posp (car l)) (pos-listp (cdr l))))))

other

(defthm 2+-listp-forward-to-pos-listp
  (implies (2+-listp x)
    (pos-listp x))
  :rule-classes :forward-chaining)

other

(defthm pos-listp-forward-to-nat-listp
  (implies (pos-listp x)
    (nat-listp x))
  :rule-classes :forward-chaining)

other

(defthm nat-listp-forward-to-integer-listp
  (implies (nat-listp x)
    (integer-listp x))
  :rule-classes :forward-chaining)

other

(defthm rational-listp-forward-to-acl2-number-listp
  (implies (rational-listp x)
    (acl2-number-listp x))
  :rule-classes :forward-chaining)

other

(defthm acl2-number-listp-forward-to-true-listp
  (implies (rational-listp x)
    (acl2-number-listp x))
  :rule-classes :forward-chaining)

sum-listfunction

(defun sum-list
  (l)
  (declare (xargs :guard (acl2-number-listp l)))
  (if (endp l)
    0
    (+ (car l) (sum-list (cdr l)))))

product-listfunction

(defun product-list
  (l)
  (declare (xargs :guard (acl2-number-listp l)))
  (if (endp l)
    1
    (* (car l)
      (product-list (cdr l)))))

max-nat-listfunction

(defun max-nat-list
  (l)
  (declare (xargs :guard (rational-listp l)))
  (if (endp l)
    0
    (max (car l)
      (max-nat-list (cdr l)))))

scalefunction

(defun scale
  (l x)
  (declare (xargs :guard (and (acl2-number-listp l)
        (acl2-numberp x))))
  (if (endp l)
    nil
    (cons (* (car l) x)
      (scale (cdr l) x))))

shiftfunction

(defun shift
  (l x)
  (declare (xargs :guard (and (acl2-number-listp l)
        (acl2-numberp x))))
  (if (endp l)
    nil
    (cons (+ (car l) x)
      (shift (cdr l) x))))

list-exptfunction

(defun list-expt
  (base l)
  (declare (xargs :guard (and (acl2-numberp base)
        (nat-listp l))))
  (if (endp l)
    nil
    (cons (expt base (car l))
      (list-expt base (cdr l)))))

<=-listsfunction

(defun <=-lists
  (l1 l2)
  (declare (xargs :guard (and (rational-listp l1)
        (rational-listp l2)
        (= (len l1) (len l2)))))
  (if (mbe :logic (or (endp l1) (endp l2))
      :exec (endp l1))
    (mbe :logic (and (endp l1) (endp l2))
      :exec t)
    (and (<= (car l1) (car l2))
      (<=-lists (cdr l1) (cdr l2)))))

all-<=function

(defun all-<=
  (l v)
  (declare (xargs :guard (and (rationalp v)
        (rational-listp l))))
  (if (endp l)
    t
    (and (<= (car l) v)
      (all-<= (cdr l) v))))

*-listsfunction

(defun *-lists
  (l1 l2)
  (declare (xargs :guard (and (rational-listp l1)
        (rational-listp l2)
        (= (len l1) (len l2)))))
  (if (mbe :logic (or (endp l1) (endp l2))
      :exec (endp l1))
    nil
    (cons (* (car l1) (car l2))
      (*-lists (cdr l1) (cdr l2)))))

+-listsfunction

(defun +-lists
  (l1 l2)
  (declare (xargs :guard (and (rational-listp l1)
        (rational-listp l2)
        (= (len l1) (len l2)))))
  (if (mbe :logic (or (endp l1) (endp l2))
      :exec (endp l1))
    nil
    (cons (+ (car l1) (car l2))
      (+-lists (cdr l1) (cdr l2)))))

make-list-logicfunction

(defun make-list-logic
  (e size)
  (declare (xargs :guard nil))
  (if (zp size)
    nil
    (cons e
      (make-list-logic e (- size 1)))))

pfixfunction

(defun pfix
  (x)
  (if (posp x)
    x
    1))

pos-list-fixfunction

(defun pos-list-fix
  (x)
  (if (atom x)
    nil
    (cons (pfix (car x))
      (pos-list-fix (cdr x)))))