Filtering...

default

books/kestrel/acl2-arrays/default
other
(in-package "ACL2")
in-theory
(in-theory (disable default))
default-introtheorem
(defthm default-intro
  (equal (cadr (assoc-keyword :default (cdr (header name l))))
    (default name l))
  :hints (("Goal" :in-theory (enable default))))
other
(theory-invariant (incompatible (:rewrite default-intro)
    (:definition default)))
default-intro2theorem
(defthmd default-intro2
  (equal (cadr (assoc-keyword :default (cdr (assoc-equal :header l))))
    (default name l))
  :hints (("Goal" :in-theory (e/d (default header) (default-intro)))))
other
(theory-invariant (incompatible (:rewrite default-intro2)
    (:definition default)))
default-of-niltheorem
(defthm default-of-nil
  (equal (default name nil) nil)
  :hints (("Goal" :in-theory (e/d (default) (default-intro)))))
default-of-constheorem
(defthm default-of-cons
  (equal (default name (cons a x))
    (if (equal :header (car a))
      (cadr (assoc-keyword :default (cdr a)))
      (default name x)))
  :hints (("Goal" :in-theory (e/d (default header) (default-intro)))))
default-of-acons-of-headertheorem
(defthm default-of-acons-of-header
  (equal (default name (acons :header header x))
    (cadr (assoc-keyword :default header)))
  :hints (("Goal" :in-theory (e/d (default header) (default-intro)))))
normalize-default-nametheorem
(defthmd normalize-default-name
  (implies (syntaxp (not (equal name '':fake-name)))
    (equal (default name l) (default :fake-name l)))
  :hints (("Goal" :in-theory (e/d (default) (default-intro)))))