Filtering...

flag-tests

books/tools/flag-tests

Included Books

flag top install-not-normalized
other
(in-package "ACL2")
include-book
(include-book "flag")
local
(local (include-book "arithmetic-3/bind-free/top" :dir :system))
other
(logic)
other
(make-flag flag-pseudo-termp
  pseudo-termp
  :flag-var flag
  :flag-mapping ((pseudo-termp term) (pseudo-term-listp list))
  :defthm-macro-name defthm-pseudo-termp)
encapsulate
(encapsulate nil
  (set-enforce-redundancy t)
  (make-flag pseudo-termp
    :flag-var flag
    :flag-mapping ((pseudo-termp term) (pseudo-term-listp list))
    :defthm-macro-name defthm-pseudo-termp))
in-theory
(in-theory (disable (:type-prescription pseudo-termp)
    (:type-prescription pseudo-term-listp)))
encapsulate
(encapsulate nil
  (value-triple 1)
  (local (defthm-pseudo-termp type-of-pseudo-termp
      (term (booleanp (pseudo-termp x))
        :rule-classes :rewrite :doc nil)
      (list (booleanp (pseudo-term-listp lst))))))
encapsulate
(encapsulate nil
  (value-triple 2)
  (local (defthm-pseudo-termp type-of-pseudo-termp2
      (defthm booleanp-of-pseudo-termp
        (booleanp (pseudo-termp x))
        :rule-classes :rewrite :doc nil
        :flag term)
      :skip-others t)))
encapsulate
(encapsulate nil
  (value-triple 3)
  (local (in-theory (disable pseudo-termp pseudo-term-listp)))
  (local (defthm-pseudo-termp type-of-pseudo-termp
      (term (booleanp (pseudo-termp x))
        :hints ('(:expand ((pseudo-termp x))))
        :rule-classes :rewrite :doc nil)
      (list (booleanp (pseudo-term-listp lst))
        :hints ('(:expand ((pseudo-term-listp lst))))))))
encapsulate
(encapsulate nil
  (value-triple 4)
  (local (defthm-pseudo-termp (term (booleanp (pseudo-termp x))
        :rule-classes :rewrite :doc nil
        :name type-of-pseudo-termp)
      (list (booleanp (pseudo-term-listp lst)) :skip t))))
encapsulate
(encapsulate nil
  (value-triple 5)
  (local (defthm-pseudo-termp (defthm type-of-pseudo-termp
        (booleanp (pseudo-termp x))
        :rule-classes :rewrite :doc nil
        :flag term)
      (defthm type-of-pseudo-term-listp
        (booleanp (pseudo-term-listp lst))
        :flag list
        :skip t))))
encapsulate
(encapsulate nil
  (value-triple 6)
  (local (defthm-pseudo-termp (defthm type-of-pseudo-termp
        (booleanp (pseudo-termp x))
        :rule-classes :type-prescription :doc nil
        :flag term)
      (defthm pseudo-termp-equal-t
        (equal (equal (pseudo-termp x) t) (pseudo-termp x))
        :rule-classes :rewrite :doc nil
        :flag term)
      (list (booleanp (pseudo-term-listp lst)) :skip t))))
other
(defstobj term-bucket (terms))
terms-into-bucketmutual-recursion
(mutual-recursion (defun terms-into-bucket
    (x term-bucket)
    (declare (xargs :stobjs (term-bucket) :verify-guards nil))
    (cond ((or (atom x) (quotep x)) (let ((term-bucket (update-terms (cons x (terms term-bucket)) term-bucket)))
          (mv 1 term-bucket)))
      (t (mv-let (numterms term-bucket)
          (terms-into-bucket-list (cdr x) term-bucket)
          (let ((term-bucket (update-terms (cons x (terms term-bucket)) term-bucket)))
            (mv (+ numterms 1) term-bucket))))))
  (defun terms-into-bucket-list
    (x term-bucket)
    (declare (xargs :stobjs (term-bucket)))
    (if (atom x)
      (mv 0 term-bucket)
      (mv-let (num-car term-bucket)
        (terms-into-bucket (car x) term-bucket)
        (mv-let (num-cdr term-bucket)
          (terms-into-bucket-list (cdr x) term-bucket)
          (mv (+ num-car num-cdr) term-bucket))))))
other
(make-flag flag-terms-into-bucket terms-into-bucket)
encapsulate
(encapsulate nil
  (set-ignore-ok t)
  (mutual-recursion (defun ignore-test-f
      (x)
      (if (consp x)
        (let ((y (+ x 1)))
          (ignore-test-g (cdr x)))
        nil))
    (defun ignore-test-g
      (x)
      (if (consp x)
        (ignore-test-f (cdr x))
        nil))))
other
(make-flag flag-ignore-test ignore-test-f)
my-evenpmutual-recursion
(mutual-recursion (defun my-evenp
    (x)
    (if (zp x)
      t
      (my-oddp (- x 1))))
  (defun my-oddp
    (x)
    (if (zp x)
      nil
      (my-evenp (- x 1)))))
other
(make-flag flag-my-evenp
  my-evenp
  :flag-mapping ((my-evenp :even) (my-oddp :odd)))
encapsulate
(encapsulate nil
  (defthm-flag-my-evenp defthmd-test
    (defthmd my-evenp-of-increment
      (implies (natp x) (equal (my-evenp (+ 1 x)) (my-oddp x)))
      :flag :even)
    (defthm my-oddp-of-increment
      (implies (natp x) (equal (my-oddp (+ 1 x)) (my-evenp x)))
      :flag :odd)))
other
(make-event (b* ((ens (ens state)) ((when (active-runep '(:rewrite my-evenp-of-increment))) (er soft
          'defthmd-test
          "Expected my-evenp-of-increment to be disabled."))
      ((unless (active-runep '(:rewrite my-oddp-of-increment))) (er soft
          'defthmd-test
          "Expected my-oddp-of-increment to be enabled.")))
    (value '(value-triple :success))))
local
(local (in-theory (disable my-evenp my-oddp evenp oddp)))
encapsulate
(encapsulate nil
  (local (defthm-flag-my-evenp hints-test-1
      (defthm my-evenp-is-evenp
        (implies (natp x) (equal (my-evenp x) (evenp x)))
        :flag :even)
      (defthm my-oddp-is-oddp
        (implies (natp x) (equal (my-oddp x) (oddp x)))
        :flag :odd)
      :hints (("Goal" :in-theory (enable my-evenp my-oddp evenp oddp)
         :expand ((my-evenp x) (my-oddp x) (evenp x) (oddp x)))))))
encapsulate
(encapsulate nil
  (local (defthm-flag-my-evenp hints-test-2
      (defthm my-evenp-is-evenp
        (implies (natp x) (equal (my-evenp x) (evenp x)))
        :flag :even)
      (defthm my-oddp-is-oddp
        (implies (natp x) (equal (my-oddp x) (oddp x)))
        :flag :odd)
      :hints (("Subgoal *1/3" :in-theory (enable natp)) ("Goal" :in-theory (enable my-evenp my-oddp evenp oddp)
          :expand ((my-evenp x) (my-oddp x) (evenp x) (oddp x)))))))
local
(local (progn (defun nat-list-equiv
      (x y)
      (if (atom x)
        (atom y)
        (and (consp y)
          (equal (nfix (car x)) (nfix (car y)))
          (nat-list-equiv (cdr x) (cdr y)))))
    (defun sum-pairs-list
      (x)
      (if (atom x)
        nil
        (if (atom (cdr x))
          (list (nfix (car x)))
          (cons (+ (nfix (car x)) (nfix (cadr x)))
            (sum-pairs-list (cddr x))))))
    (defequiv nat-list-equiv)
    (def-doublevar-induction sum-pairs-list-double
      :orig-fn sum-pairs-list
      :old-var x
      :new-var y)
    (defthm sum-pairs-list-nat-list-equiv-congruence
      (implies (nat-list-equiv x y)
        (equal (sum-pairs-list x) (sum-pairs-list y)))
      :rule-classes :congruence :hints (("goal" :induct (sum-pairs-list-double x y))))))
include-book
(include-book "misc/install-not-normalized" :dir :system)
evenlpmutual-recursion
(mutual-recursion (defun evenlp
    (x)
    (if (atom x)
      t
      (oddlp (cdr x))))
  (defun oddlp
    (x)
    (if (atom x)
      nil
      (evenlp (cdr x)))))
other
(install-not-normalized evenlp)
other
(make-flag evenlp :body :last)
other
(assert-event (equal (body 'flag-evenlp nil (w state))
    '(return-last 'progn
      (throw-nonexec-error 'flag-evenlp (cons flag (cons x 'nil)))
      (if (equal flag 'evenlp)
        (if (atom x)
          't
          (flag-evenlp 'oddlp (cdr x)))
        (if (atom x)
          'nil
          (flag-evenlp 'evenlp (cdr x)))))))
other
(make-flag flag2-evenlp evenlp)
other
(assert-event (equal (body 'flag2-evenlp nil (w state))
    '(return-last 'progn
      (throw-nonexec-error 'flag2-evenlp
        (cons flag (cons x 'nil)))
      (if (equal flag 'evenlp)
        (if (consp x)
          (flag2-evenlp 'oddlp (cdr x))
          't)
        (if (consp x)
          (flag2-evenlp 'evenlp (cdr x))
          'nil)))))
evenlp$re-normalizedtheorem
(defthm evenlp$re-normalized
  (equal (evenlp x)
    (if (consp x)
      (oddlp (cdr x))
      't))
  :rule-classes ((:definition :install-body t
     :clique (evenlp oddlp)
     :controller-alist ((evenlp t) (oddlp t)))))
other
(make-flag flag3-evenlp evenlp :body :last)
other
(assert-event (equal (body 'flag3-evenlp nil (w state))
    '(return-last 'progn
      (throw-nonexec-error 'flag3-evenlp
        (cons flag (cons x 'nil)))
      (if (equal flag 'evenlp)
        (if (consp x)
          (flag3-evenlp 'oddlp (cdr x))
          't)
        (if (atom x)
          'nil
          (flag3-evenlp 'evenlp (cdr x)))))))
other
(make-event `(make-flag flag4-evenlp
    evenlp
    :body ((evenlp ,(INSTALL-NOT-NORMALIZED-NAME 'EVENLP)) (oddlp ,(INSTALL-NOT-NORMALIZED-NAME 'ODDLP)))))
other
(assert-event (equal (body 'flag4-evenlp nil (w state))
    '(return-last 'progn
      (throw-nonexec-error 'flag4-evenlp
        (cons flag (cons x 'nil)))
      (if (equal flag 'evenlp)
        (if (atom x)
          't
          (flag4-evenlp 'oddlp (cdr x)))
        (if (atom x)
          'nil
          (flag4-evenlp 'evenlp (cdr x)))))))
my-nat-listpmutual-recursion
(mutual-recursion (defun my-nat-listp
    (x)
    (if (consp x)
      (and (natp (car x)) (my-nat-listp (cdr x)))
      (eq x nil))))
other
(make-flag flag-my-nat-listp my-nat-listp)
other
(defthm-flag-my-nat-listp (defthm type-of-my-nat-listp
    (booleanp (my-nat-listp x))
    :flag my-nat-listp
    :hints ('(:in-theory '(booleanp) :expand ((my-nat-listp x)))))
  :hints (("Goal" :in-theory '((:i flag-my-nat-listp)))))