Filtering...

gentle

books/misc/gentle
other
(in-package "ACL2")
gentle-carother
(defabbrev gentle-car
  (x)
  (if (consp x)
    (car x)
    nil))
gentle-cdrother
(defabbrev gentle-cdr
  (x)
  (if (consp x)
    (cdr x)
    nil))
gentle-caarother
(defabbrev gentle-caar (x) (gentle-car (gentle-car x)))
gentle-cadrother
(defabbrev gentle-cadr (x) (gentle-car (gentle-cdr x)))
gentle-cdarother
(defabbrev gentle-cdar (x) (gentle-cdr (gentle-car x)))
gentle-cddrother
(defabbrev gentle-cddr (x) (gentle-cdr (gentle-cdr x)))
gentle-caaarother
(defabbrev gentle-caaar (x) (gentle-car (gentle-caar x)))
gentle-cadarother
(defabbrev gentle-cadar (x) (gentle-car (gentle-cdar x)))
gentle-cdaarother
(defabbrev gentle-cdaar (x) (gentle-cdr (gentle-caar x)))
gentle-cddarother
(defabbrev gentle-cddar (x) (gentle-cdr (gentle-cdar x)))
gentle-caadrother
(defabbrev gentle-caadr (x) (gentle-car (gentle-cadr x)))
gentle-caddrother
(defabbrev gentle-caddr (x) (gentle-car (gentle-cddr x)))
gentle-cdadrother
(defabbrev gentle-cdadr (x) (gentle-cdr (gentle-cadr x)))
gentle-cdddrother
(defabbrev gentle-cdddr (x) (gentle-cdr (gentle-cddr x)))
gentle-caaaarother
(defabbrev gentle-caaaar (x) (gentle-car (gentle-caaar x)))
gentle-cadaarother
(defabbrev gentle-cadaar (x) (gentle-car (gentle-cdaar x)))
gentle-cdaaarother
(defabbrev gentle-cdaaar (x) (gentle-cdr (gentle-caaar x)))
gentle-cddaarother
(defabbrev gentle-cddaar (x) (gentle-cdr (gentle-cdaar x)))
gentle-caadarother
(defabbrev gentle-caadar (x) (gentle-car (gentle-cadar x)))
gentle-caddarother
(defabbrev gentle-caddar (x) (gentle-car (gentle-cddar x)))
gentle-cdadarother
(defabbrev gentle-cdadar (x) (gentle-cdr (gentle-cadar x)))
gentle-cdddarother
(defabbrev gentle-cdddar (x) (gentle-cdr (gentle-cddar x)))
gentle-caaadrother
(defabbrev gentle-caaadr (x) (gentle-car (gentle-caadr x)))
gentle-cadadrother
(defabbrev gentle-cadadr (x) (gentle-car (gentle-cdadr x)))
gentle-cdaadrother
(defabbrev gentle-cdaadr (x) (gentle-cdr (gentle-caadr x)))
gentle-cddadrother
(defabbrev gentle-cddadr (x) (gentle-cdr (gentle-cdadr x)))
gentle-caaddrother
(defabbrev gentle-caaddr (x) (gentle-car (gentle-caddr x)))
gentle-cadddrother
(defabbrev gentle-cadddr (x) (gentle-car (gentle-cdddr x)))
gentle-cdaddrother
(defabbrev gentle-cdaddr (x) (gentle-cdr (gentle-caddr x)))
gentle-cddddrother
(defabbrev gentle-cddddr (x) (gentle-cdr (gentle-cdddr x)))
other
(defn gentle-revappend
  (x y)
  (mbe :logic (revappend x y)
    :exec (if (atom x)
      y
      (gentle-revappend (cdr x) (cons (car x) y)))))
other
(defn gentle-reverse
  (x)
  (mbe :logic (reverse x)
    :exec (if (stringp x)
      (reverse x)
      (gentle-revappend x nil))))
other
(defn gentle-strip-cars
  (l)
  (if (atom l)
    nil
    (cons (if (atom (car l))
        (car l)
        (car (car l)))
      (gentle-strip-cars (cdr l)))))
other
(defn gentle-strip-cdrs
  (l)
  (if (atom l)
    nil
    (cons (if (atom (car l))
        (car l)
        (cdr (car l)))
      (gentle-strip-cdrs (cdr l)))))
other
(defn gentle-member-eq
  (x y)
  (declare (xargs :guard (symbolp x)))
  (mbe :logic (member-equal x y)
    :exec (cond ((atom y) nil)
      ((eq x (car y)) y)
      (t (gentle-member-eq x (cdr y))))))
other
(defn gentle-member-eql
  (x y)
  (declare (xargs :guard (eqlablep x)))
  (mbe :logic (member-equal x y)
    :exec (cond ((atom y) nil)
      ((eql x (car y)) y)
      (t (gentle-member-eql x (cdr y))))))
other
(defn gentle-member-equal
  (x y)
  (mbe :logic (member-equal x y)
    :exec (cond ((atom y) nil)
      ((equal x (car y)) y)
      (t (gentle-member-equal x (cdr y))))))
other
(defn gentle-member
  (x y)
  (mbe :logic (member-equal x y)
    :exec (cond ((symbolp x) (gentle-member-eq x y))
      ((or (characterp x) (acl2-numberp x)) (gentle-member-eql x y))
      (t (gentle-member-equal x y)))))
other
(defn gentle-last
  (l)
  (mbe :logic (last l)
    :exec (if (or (atom l) (atom (cdr l)))
      l
      (gentle-last (cdr l)))))
other
(defn gentle-take
  (n l)
  "Unlike TAKE, GENTLE-TAKE fills at the end with NILs, if necessary, to
 always return a list n long."
  (cond ((not (posp n)) nil)
    ((atom l) (make-list n))
    (t (cons (car l) (gentle-take (1- n) (cdr l))))))
true-listp-of-make-list-actheorem
(defthm true-listp-of-make-list-ac
  (equal (true-listp (make-list-ac n val ac)) (true-listp ac))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp ac)
        (true-listp (make-list-ac n val ac))))))
true-listp-of-gentle-taketheorem
(defthm true-listp-of-gentle-take
  (true-listp (gentle-take n l))
  :rule-classes :type-prescription)
other
(defn defnp
  (x)
  (and (consp x)
    (symbolp (car x))
    (eq (car x) 'defn)
    (consp (cdr x))
    (symbolp (cadr x))
    (consp (cddr x))
    (symbol-listp (caddr x))
    (consp (cdddr x))
    (true-listp (cdddr x))))
other
(defn defn-listp
  (x)
  (if (atom x)
    (null x)
    (and (defnp (car x)) (defn-listp (cdr x)))))
mu-defn-fnfunction
(defun mu-defn-fn
  (l)
  (declare (xargs :guard (defn-listp l)))
  (if (atom l)
    nil
    (cons `(defun ,(CADR (CAR L))
        ,(CADDR (CAR L))
        (declare (xargs :guard t))
        ,@(CDDDR (CAR L)))
      (mu-defn-fn (cdr l)))))
mu-defnmacro
(defmacro mu-defn
  (&rest l)
  `(mutual-recursion ,@(MU-DEFN-FN L)))