list-defuns - ACL2 Book

other

(in-package "ACL2")

list-fix-execmacro

(defmacro list-fix-exec (x) `(true-list-fix-exec ,X))

other

(table macro-aliases-table
  'list-fix-exec
  'true-list-fix-exec)

in-theory

(in-theory (disable list-fix-exec))

list-fixmacro

(defmacro list-fix (x) `(true-list-fix ,X))

other

(table macro-aliases-table 'list-fix 'true-list-fix)

in-theory

(in-theory (disable list-fix))

list-fix-exec-removalencapsulate

(encapsulate nil
  (local (in-theory (enable list-fix list-fix-exec)))
  (defthm list-fix-exec-removal
    (equal (list-fix-exec x) (list-fix x)))
  (local (defthm list-fix-when-true-listp
      (implies (true-listp x) (equal (list-fix x) x))))
  (defun-inline llist-fix
    (x)
    (declare (xargs :guard (true-listp x)))
    (mbe :logic (list-fix x) :exec x)))

fast-list-equivfunction

(defund fast-list-equiv
  (x y)
  (declare (xargs :guard t))
  (if (consp x)
    (and (consp y)
      (equal (car x) (car y))
      (fast-list-equiv (cdr x) (cdr y)))
    (atom y)))

list-equivfunction

(defund list-equiv
  (x y)
  (declare (xargs :guard t
      :guard-hints (("Goal" :in-theory (enable fast-list-equiv list-fix)))))
  (mbe :logic (equal (list-fix x) (list-fix y))
    :exec (fast-list-equiv x y)))

other

(defequiv list-equiv
  :hints (("Goal" :in-theory (enable list-equiv))))

set-equivfunction

(defun set-equiv
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (and (subsetp-equal x y) (subsetp-equal y x)))

encapsulate

(encapsulate nil
  (local (defthm l0 (implies (subsetp x (cdr y)) (subsetp x y))))
  (local (defthm l1 (subsetp x x)))
  (local (defthm l2
      (implies (and (member a x) (subsetp x y)) (member a y))))
  (local (defthm l3
      (implies (and (subsetp x y) (subsetp y z)) (subsetp x z))))
  (defequiv set-equiv)
  (local (defthm r0
      (equal (subsetp-equal (list-fix x) y) (subsetp-equal x y))
      :hints (("Goal" :in-theory (enable list-fix)))))
  (local (defthm r1
      (iff (member-equal a (list-fix x)) (member-equal a x))
      :hints (("Goal" :in-theory (enable list-fix)))))
  (local (defthm r2
      (equal (subsetp-equal x (list-fix y)) (subsetp-equal x y))))
  (local (defthm r3
      (equal (set-equiv (list-fix x) y) (set-equiv x y))))
  (local (defthm r4
      (equal (set-equiv x (list-fix y)) (set-equiv x y))))
  (defrefinement list-equiv
    set-equiv
    :hints (("Goal" :in-theory (e/d (list-equiv) (set-equiv r4))
       :use ((:instance r4 (y x)) (:instance r4 (x y)))))))

binary-append-without-guardfunction

(defun binary-append-without-guard
  (x y)
  (declare (xargs :guard t))
  (mbe :logic (append x y)
    :exec (if (consp x)
      (cons (car x) (binary-append-without-guard (cdr x) y))
      y)))

append-without-guardmacro

(defmacro append-without-guard
  (x y &rest rst)
  (xxxjoin 'binary-append-without-guard (list* x y rst)))

other

(add-macro-alias append-without-guard
  binary-append-without-guard)

revappend-without-guardfunction

(defun revappend-without-guard
  (x y)
  (declare (xargs :guard t))
  (mbe :logic (revappend x y)
    :exec (if (consp x)
      (revappend-without-guard (cdr x) (cons (car x) y))
      y)))

rconsfunction

(defund rcons
  (a x)
  (declare (xargs :guard t))
  (append-without-guard x (list a)))

revfunction

(defund rev
  (x)
  (declare (xargs :guard t :verify-guards nil))
  (mbe :logic (if (consp x)
      (append (rev (cdr x)) (list (car x)))
      nil)
    :exec (revappend-without-guard x nil)))

encapsulate

(encapsulate nil
  (local (defthm l1
      (equal (append (append rv (list x1)) y)
        (append rv (cons x1 y)))))
  (local (defthm l2
      (equal (revappend x y) (append (rev x) y))
      :hints (("Goal" :in-theory (enable rev)))))
  (verify-guards rev
    :hints (("Goal" :in-theory (enable rev)))))

prefixpfunction

(defund prefixp
  (x y)
  (declare (xargs :guard t))
  (if (consp x)
    (and (consp y)
      (equal (car x) (car y))
      (prefixp (cdr x) (cdr y)))
    t))

suffixpfunction

(defund suffixp
  (x y)
  (declare (xargs :guard t))
  (or (equal x y) (and (consp y) (suffixp x (cdr y)))))

flattenfunction

(defund flatten
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (append-without-guard (car x) (flatten (cdr x)))
    nil))

repeatfunction

(defund repeat
  (n x)
  (declare (xargs :guard (natp n) :verify-guards nil))
  (mbe :logic (if (zp n)
      nil
      (cons x (repeat (- n 1) x)))
    :exec (make-list n :initial-element x)))

replicatemacro

(defmacro replicate (n x) `(repeat ,N ,X))

other

(add-macro-alias replicate repeat)

local

(local (encapsulate nil
    (local (defthm l0
        (equal (append (replicate n x) (cons x acc))
          (cons x (append (replicate n x) acc)))
        :hints (("Goal" :in-theory (enable replicate)))))
    (defthm make-list-ac-redef
      (equal (make-list-ac n x acc) (append (replicate n x) acc))
      :hints (("Goal" :in-theory (enable repeat))))))

other

(verify-guards repeat
  :hints (("Goal" :in-theory (enable repeat))))

all-equalpencapsulate

(encapsulate nil
  (local (in-theory (enable repeat list-fix)))
  (defun all-equalp
    (a x)
    (declare (xargs :guard t :verify-guards nil))
    (let ((__function__ 'all-equalp))
      (declare (ignorable __function__))
      (mbe :logic (equal (list-fix x) (repeat (len x) a))
        :exec (if (consp x)
          (and (equal a (car x)) (all-equalp a (cdr x)))
          t))))
  (verify-guards all-equalp))

final-cdrfunction

(defund final-cdr
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    x
    (final-cdr (cdr x))))

local

(local (defthm nthcdr-of-nil (equal (nthcdr n nil) nil)))

rest-nfunction

(defun rest-n
  (n x)
  (declare (xargs :guard (natp n)))
  (mbe :logic (nthcdr n x)
    :exec (cond ((zp n) x)
      ((atom x) nil)
      (t (rest-n (- n 1) (cdr x))))))

first-nfunction

(defun first-n
  (n x)
  (declare (xargs :guard (natp n) :verify-guards nil))
  (mbe :logic (take n x)
    :exec (cond ((zp n) nil)
      ((atom x) (make-list n))
      (t (cons (car x) (first-n (- n 1) (cdr x)))))))

encapsulate

(encapsulate nil
  (local (defthm take-when-atom
      (implies (atom x) (equal (take n x) (replicate n nil)))
      :hints (("Goal" :in-theory (enable replicate)))))
  (verify-guards first-n
    :hints (("Goal" :in-theory (enable replicate)))))

same-lengthpfunction

(defun same-lengthp
  (x y)
  (declare (xargs :guard t))
  (mbe :logic (equal (len x) (len y))
    :exec (if (consp x)
      (and (consp y) (same-lengthp (cdr x) (cdr y)))
      (not (consp y)))))

sublistpfunction

(defund sublistp
  (x y)
  (declare (xargs :guard t))
  (cond ((prefixp x y) t)
    ((atom y) nil)
    (t (sublistp x (cdr y)))))

listposfunction

(defund listpos
  (x y)
  (declare (xargs :guard t))
  (cond ((prefixp x y) 0)
    ((atom y) nil)
    (t (let ((pos-in-cdr (listpos x (cdr y))))
        (and pos-in-cdr (+ 1 pos-in-cdr))))))

duplicity-execfunction

(defund duplicity-exec
  (a x n)
  (declare (xargs :guard (natp n)))
  (if (atom x)
    n
    (duplicity-exec a
      (cdr x)
      (if (equal (car x) a)
        (+ 1 n)
        n))))

duplicityfunction

(defund duplicity
  (a x)
  (declare (xargs :guard t :verify-guards nil))
  (mbe :logic (cond ((atom x) 0)
      ((equal (car x) a) (+ 1 (duplicity a (cdr x))))
      (t (duplicity a (cdr x))))
    :exec (duplicity-exec a x 0)))

local

(local (defthm duplicity-exec-removal
    (implies (natp n)
      (equal (duplicity-exec a x n) (+ (duplicity a x) n)))
    :hints (("Goal" :in-theory (enable duplicity duplicity-exec)))))

other

(verify-guards duplicity
  :hints (("Goal" :in-theory (enable duplicity))))