Filtering...

install-not-normalized-tests

books/misc/install-not-normalized-tests

Included Books

install-not-normalized must-fail must-succeed
other
(in-package "ACL2")
include-book
(include-book "install-not-normalized")
local
(local (include-book "std/testing/must-fail" :dir :system))
local
(local (include-book "std/testing/must-succeed" :dir :system))
my-testmacro
(defmacro my-test
  (&rest forms)
  `(local (encapsulate nil
      (local (in-theory (current-theory :here)))
      (local (progn ,@FORMS)))))
other
(my-test (defun return-nil (x) (declare (ignore x)) nil)
  (defun foo (x) (return-nil x))
  (must-fail (fn-is-body foo :hints (("Goal" :in-theory '(foo)))))
  (must-fail (fn-is-body foo
      :hints (("Goal" :expand ((foo x))
         :in-theory (theory 'minimal-theory)))))
  (install-not-normalized foo)
  (must-succeed (fn-is-body foo
      :hints (("Goal" :in-theory '(foo$not-normalized)))))
  (must-succeed (fn-is-body foo
      :hints (("Goal" :expand ((foo x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun return-nil (x) (declare (ignore x)) nil)
  (defun foo (x) (return-nil x))
  (install-not-normalized foo
    :defthm-name 'foo$not-normalized)
  (must-succeed (fn-is-body foo
      :hints (("Goal" :in-theory '(foo$not-normalized)))))
  (must-succeed (fn-is-body foo
      :hints (("Goal" :expand ((foo x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun return-nil (x) (declare (ignore x)) nil)
  (defun foo (x) (return-nil x))
  (install-not-normalized foo
    :defthm-name 'foo-is-unnormalized-body)
  (must-succeed (fn-is-body foo
      :hints (("Goal" :in-theory '(foo-is-unnormalized-body)))))
  (must-succeed (fn-is-body foo
      :hints (("Goal" :expand ((foo x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (defun f-norm
    (x)
    (if (my-t)
      (if (consp x)
        (cons (car x) (f-norm (cdr x)))
        (my-zero))
      (my-nil)))
  (must-fail (fn-is-body f-norm :hints (("Goal" :in-theory '(f-norm)))))
  (must-fail (fn-is-body f-norm
      :hints (("Goal" :expand ((f-norm x))
         :in-theory (theory 'minimal-theory)))))
  (install-not-normalized f-norm)
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :in-theory '(f-norm$not-normalized)))))
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :expand ((f-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (defun f-norm
    (x)
    (if (my-t)
      (if (consp x)
        (cons (car x) (f-norm (cdr x)))
        (my-zero))
      (my-nil)))
  (install-not-normalized f-norm
    :defthm-name 'f-norm$not-normalized)
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :in-theory '(f-norm$not-normalized)))))
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :expand ((f-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (defun f-norm
    (x)
    (if (my-t)
      (if (consp x)
        (cons (car x) (f-norm (cdr x)))
        (my-zero))
      (my-nil)))
  (install-not-normalized f-norm :defthm-name 'f-norm-alt-def)
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :in-theory '(f-norm-alt-def)))))
  (must-succeed (fn-is-body f-norm
      :hints (("Goal" :expand ((f-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f1-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f2-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f2-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f1-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (must-fail (fn-is-body f1-norm :hints (("Goal" :in-theory '(f1-norm)))))
  (must-fail (fn-is-body f1-norm
      :hints (("Goal" :expand ((f1-norm x))
         :in-theory (theory 'minimal-theory)))))
  (install-not-normalized f1-norm)
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :in-theory '(f1-norm$not-normalized)))))
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :expand ((f1-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :in-theory '(f2-norm$not-normalized)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :expand ((f2-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f1-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f2-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f2-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f1-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (install-not-normalized f1-norm
    :defthm-name 'f1-norm$not-normalized)
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :in-theory '(f1-norm$not-normalized)))))
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :expand ((f1-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :in-theory '(f2-norm$not-normalized)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :expand ((f2-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f1-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f2-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f2-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f1-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (install-not-normalized f1-norm
    :defthm-name 'f1-norm-new-def)
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :in-theory '(f1-norm-new-def)))))
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :expand ((f1-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :in-theory '(f2-norm$not-normalized)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :expand ((f2-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f1-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f2-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f2-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f1-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (install-not-normalized f1-norm
    :defthm-name '((f1-norm f1-norm-new-def) (f2-norm f2-norm-new-def)))
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :in-theory '(f1-norm-new-def)))))
  (must-succeed (fn-is-body f1-norm
      :hints (("Goal" :expand ((f1-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :in-theory '(f2-norm-new-def)))))
  (must-succeed (fn-is-body f2-norm
      :hints (("Goal" :expand ((f2-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f3-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f4-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f4-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f3-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (must-fail (fn-is-body f3-norm :hints (("Goal" :in-theory '(f3-norm)))))
  (must-fail (fn-is-body f3-norm
      :hints (("Goal" :expand ((f3-norm x))
         :in-theory (theory 'minimal-theory)))))
  (install-not-normalized f3-norm :allp nil)
  (must-succeed (fn-is-body f3-norm
      :hints (("Goal" :in-theory '(f3-norm$not-normalized)))))
  (must-succeed (fn-is-body f3-norm
      :hints (("Goal" :expand ((f3-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-fail (fn-is-body f4-norm
      :hints (("Goal" :in-theory '(f4-norm$not-normalized)))))
  (must-fail (fn-is-body f4-norm
      :hints (("Goal" :expand ((f4-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun my-t nil t)
  (defun my-nil nil nil)
  (defun my-zero nil 0)
  (mutual-recursion (defun f3-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f4-norm (cdr x)))
          (my-zero))
        (my-nil)))
    (defun f4-norm
      (x)
      (if (my-t)
        (if (consp x)
          (cons (car x) (f3-norm (cdr x)))
          (my-zero))
        (my-nil))))
  (install-not-normalized f3-norm
    :allp nil
    :defthm-name 'f3-norm-new)
  (must-succeed (fn-is-body f3-norm
      :hints (("Goal" :in-theory '(f3-norm-new)))))
  (must-succeed (fn-is-body f3-norm
      :hints (("Goal" :expand ((f3-norm x))
         :in-theory (theory 'minimal-theory)))))
  (must-fail (fn-is-body f4-norm
      :hints (("Goal" :in-theory '(f4-norm$not-normalized)))))
  (must-fail (fn-is-body f4-norm
      :hints (("Goal" :expand ((f4-norm x))
         :in-theory (theory 'minimal-theory))))))
other
(my-test (defun f5 (x) (cons x x))
  (defun g5 (x) (car (f5 x)))
  (defthm g5-identity (equal (g5 x) x))
  (in-theory (disable f5 g5))
  (thm (equal (g5 a) a))
  (install-not-normalized g5)
  (thm (equal (g5 a) a))
  (in-theory (enable g5$not-normalized))
  (must-fail (thm (equal (g5 a) a))))
other
(my-test (defun f5 (x) (cons x x))
  (defun g5 (x) (car (f5 x)))
  (defthm g5-identity (equal (g5 x) x))
  (in-theory (disable f5 g5))
  (thm (equal (g5 a) a))
  (install-not-normalized g5 :enable :auto)
  (thm (equal (g5 a) a))
  (in-theory (enable g5$not-normalized))
  (must-fail (thm (equal (g5 a) a))))
other
(my-test (defun f5 (x) (cons x x))
  (defun g5 (x) (car (f5 x)))
  (defthm g5-identity (equal (g5 x) x))
  (in-theory (disable f5 g5))
  (thm (equal (g5 a) a))
  (install-not-normalized g5 :enable nil)
  (thm (equal (g5 a) a)))
other
(my-test (defun f5 (x) (cons x x))
  (defun g5 (x) (car (f5 x)))
  (defthm g5-identity (equal (g5 x) x))
  (in-theory (disable f5 g5))
  (thm (equal (g5 a) a))
  (install-not-normalized g5 :enable t)
  (must-fail (thm (equal (g5 a) a))))
other
(my-test (defun f5 (x) (cons x x))
  (defun g5 (x) (car (f5 x)))
  (defthm g5-identity (equal (g5 x) x))
  (in-theory (disable f5 g5))
  (thm (equal (g5 a) a))
  (in-theory (e/d ((:d g5)) ((:e g5) (:t g5))))
  (install-not-normalized g5)
  (must-fail (thm (equal (g5 a) a))))