Filtering...

integerp-meta

books/arithmetic-5/lib/basic-ops/integerp-meta

Included Books

building-blocks top default-hint
other
(in-package "ACL2")
include-book
(include-book "building-blocks")
local
(local (include-book "../../support/top"))
local
(local (include-book "default-hint"))
local
(local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
       hist
       pspv))))
other
(table acl2-defaults-table :state-ok t)
other
(table acl2-defaults-table :verify-guards-eagerness 0)
intp-+function
(defun intp-+
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (+ x y))
intp-*function
(defun intp-*
  (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (* x y))
meta-integerp-unhidefunction
(defun meta-integerp-unhide
  (x)
  (declare (xargs :guard t))
  x)
meta-integerp-unhide-hidetheorem
(defthm meta-integerp-unhide-hide
  (equal (meta-integerp-unhide (hide x)) x)
  :hints (("Goal" :expand ((hide x)))))
in-theory
(in-theory (disable meta-integerp-unhide
    (:executable-counterpart meta-integerp-unhide)))
other
(defevaluator intp-eva
  intp-eva-lst
  ((intp-+ x y) (intp-* x y)
    (binary-+ x y)
    (binary-* x y)
    (integerp x)
    (rationalp x)
    (hide x)
    (meta-integerp-unhide x)
    (if x
      y
      z)
    (equal x y)
    (fix x)))
intp-1theorem
(defthm intp-1
  (implies (and (integerp x) (integerp y))
    (integerp (intp-* x y))))
intp-2theorem
(defthm intp-2
  (implies (and (integerp x) (integerp y))
    (integerp (intp-+ x y))))
intp-3theorem
(defthm intp-3
  (implies (and (rationalp x) (rationalp y))
    (rationalp (intp-* x y))))
intp-4theorem
(defthm intp-4
  (implies (and (rationalp x) (rationalp y))
    (rationalp (intp-+ x y))))
nintp-1theorem
(defthm nintp-1
  (implies (and (acl2-numberp x) (not (integerp x)) (integerp y))
    (not (integerp (intp-+ x y)))))
nintp-2theorem
(defthm nintp-2
  (implies (and (integerp x) (acl2-numberp y) (not (integerp y)))
    (not (integerp (intp-+ x y)))))
nintp-3theorem
(defthm nintp-3
  (implies (and (acl2-numberp x) (not (rationalp x)) (rationalp y))
    (not (rationalp (intp-+ x y)))))
nintp-4theorem
(defthm nintp-4
  (implies (and (rationalp x) (acl2-numberp y) (not (rationalp y)))
    (not (rationalp (intp-+ x y)))))
leavesfunction
(defun leaves
  (term bin-op)
  (declare (xargs :guard (symbolp bin-op)))
  (cond ((atom term) (if (eq bin-op 'binary-+)
        (list ''0)
        (list ''1)))
    ((eq (fn-symb term) bin-op) (if (eq (fn-symb (arg2 term)) bin-op)
        (cons (arg1 term) (leaves (arg2 term) bin-op))
        (list (arg1 term) (arg2 term))))
    (t (list term))))
treefunction
(defun tree
  (leaves bin-op)
  (declare (xargs :guard (symbolp bin-op)))
  (cond ((atom leaves) (if (eq bin-op 'binary-+)
        ''0
        ''1))
    ((atom (cdr leaves)) (list 'fix (car leaves)))
    ((atom (cddr leaves)) (list bin-op (car leaves) (cadr leaves)))
    (t (list bin-op (car leaves) (tree (cdr leaves) bin-op)))))
big-treefunction
(defun big-tree
  (bags big-bin-op bin-op)
  (declare (xargs :guard (and (symbolp big-bin-op) (symbolp bin-op))))
  (cond ((atom bags) (if (eq bin-op 'binary-+)
        ''0
        ''1))
    ((atom (cdr bags)) (tree (car bags) bin-op))
    ((atom (cddr bags)) (list big-bin-op
        (tree (car bags) bin-op)
        (tree (cadr bags) bin-op)))
    (t (list big-bin-op
        (tree (car bags) bin-op)
        (big-tree (cdr bags) big-bin-op bin-op)))))
bag-leavesfunction
(defun bag-leaves
  (leaves mfc state intp-bags non-intp-bags intp-flag)
  (declare (xargs :guard t))
  (if (atom leaves)
    (mv intp-bags non-intp-bags)
    (let ((rewriting-result (if intp-flag
           (mfc-rw+ '(integerp x) `((x . ,(CAR LEAVES))) t t mfc state)
           (mfc-rw+ '(rationalp x)
             `((x . ,(CAR LEAVES)))
             t
             t
             mfc
             state))))
      (cond ((equal rewriting-result *t*) (bag-leaves (cdr leaves)
            mfc
            state
            (cons (list (car leaves)) intp-bags)
            non-intp-bags
            intp-flag))
        ((equal rewriting-result *nil*) (bag-leaves (cdr leaves)
            mfc
            state
            intp-bags
            (cons (list (car leaves)) non-intp-bags)
            intp-flag))
        (t (bag-leaves (cdr leaves)
            mfc
            state
            intp-bags
            non-intp-bags
            intp-flag))))))
bag-termsfunction
(defun bag-terms
  (type-alist bin-op intp-bags non-intp-bags intp-flag)
  (declare (xargs :guard (and (type-alistp type-alist)
        (or (equal bin-op 'binary-+) (equal bin-op 'binary-*)))))
  (cond ((atom type-alist) (mv intp-bags non-intp-bags))
    ((variablep (caar type-alist)) (bag-terms (cdr type-alist)
        bin-op
        intp-bags
        non-intp-bags
        intp-flag))
    ((ts-subsetp (cadr (car type-alist))
       (if intp-flag
         *ts-integer*
         *ts-rational*)) (bag-terms (cdr type-alist)
        bin-op
        (cons (leaves (caar type-alist) bin-op) intp-bags)
        non-intp-bags
        intp-flag))
    ((and (ts-subsetp (cadr (car type-alist)) *ts-acl2-number*)
       (ts-subsetp (cadr (car type-alist))
         (ts-complement (if intp-flag
             *ts-integer*
             *ts-rational*)))) (bag-terms (cdr type-alist)
        bin-op
        intp-bags
        (cons (leaves (caar type-alist) bin-op) non-intp-bags)
        intp-flag))
    (t (bag-terms (cdr type-alist)
        bin-op
        intp-bags
        non-intp-bags
        intp-flag))))
subtract-leaffunction
(defun subtract-leaf
  (leaf leaves)
  (declare (xargs :guard (true-listp leaves)))
  (cond ((endp leaves) (mv nil nil))
    ((equal leaf (car leaves)) (mv t (cdr leaves)))
    (t (mv-let (flag new-leaves)
        (subtract-leaf leaf (cdr leaves))
        (if flag
          (mv t (cons (car leaves) new-leaves))
          (mv nil leaves))))))
subtract-bagfunction
(defun subtract-bag
  (bag leaves)
  (declare (xargs :guard (and (true-listp bag) (true-listp leaves))))
  (cond ((endp bag) (mv t leaves))
    ((endp (cdr bag)) (subtract-leaf (car bag) leaves))
    (t (mv-let (flag new-leaves)
        (subtract-bag (cdr bag) leaves)
        (if flag
          (subtract-leaf (car bag) new-leaves)
          (mv nil nil))))))
collect-bags-intpfunction
(defun collect-bags-intp
  (leaves intp-bags)
  (declare (xargs :guard (and (true-listp leaves) (true-list-listp intp-bags))))
  (cond ((endp leaves) (mv t nil))
    ((endp intp-bags) (mv nil nil))
    (t (mv-let (flag new-leaves)
        (subtract-bag (car intp-bags) leaves)
        (if flag
          (mv-let (flag new-bags)
            (collect-bags-intp new-leaves (cdr intp-bags))
            (if flag
              (mv t (cons (car intp-bags) new-bags))
              (collect-bags-intp leaves (cdr intp-bags))))
          (collect-bags-intp leaves (cdr intp-bags)))))))
collect-bags-non-intpfunction
(defun collect-bags-non-intp
  (leaves intp-bags non-intp-bags)
  (declare (xargs :guard (and (true-listp leaves)
        (true-list-listp intp-bags)
        (true-list-listp non-intp-bags))))
  (cond ((endp non-intp-bags) (mv nil nil))
    (t (mv-let (flag new-leaves)
        (subtract-bag (car non-intp-bags) leaves)
        (if (and flag (consp new-leaves))
          (mv-let (flag bag-list)
            (collect-bags-intp new-leaves intp-bags)
            (if flag
              (mv t (cons (car non-intp-bags) bag-list))
              (collect-bags-non-intp leaves intp-bags (cdr non-intp-bags))))
          (collect-bags-non-intp leaves intp-bags (cdr non-intp-bags)))))))
collect-bagsfunction
(defun collect-bags
  (leaves intp-bags non-intp-bags bin-op)
  (declare (xargs :guard (and (true-listp leaves)
        (true-list-listp intp-bags)
        (true-list-listp non-intp-bags))))
  (mv-let (flag bag-list)
    (if (eq bin-op 'binary-+)
      (collect-bags-non-intp leaves intp-bags non-intp-bags)
      (mv nil nil))
    (if flag
      (mv flag bag-list)
      (collect-bags-intp leaves intp-bags))))
meta-integerpfunction
(defun meta-integerp
  (term mfc state)
  (declare (xargs :guard (pseudo-termp term)))
  (if (eq (fn-symb term) 'integerp)
    (let ((bin-op (fn-symb (fargn term 1))))
      (if (and (member-eq bin-op '(binary-+ binary-*))
          (eq (fn-symb (fargn (fargn term 1) 2)) bin-op))
        (let ((leaves (leaves (fargn term 1) bin-op)))
          (mv-let (intp-leaves non-intp-leaves)
            (bag-leaves leaves mfc state nil nil t)
            (mv-let (intp-bags non-intp-bags)
              (bag-terms (mfc-type-alist mfc)
                bin-op
                intp-leaves
                non-intp-leaves
                t)
              (mv-let (flag bag-list)
                (collect-bags leaves intp-bags non-intp-bags bin-op)
                (if flag
                  `(integerp (meta-integerp-unhide (hide ,(BIG-TREE BAG-LIST
  (IF (EQ BIN-OP 'BINARY-+)
      'INTP-+
      'INTP-*)
  BIN-OP))))
                  term)))))
        term))
    term))
meta-rationalpfunction
(defun meta-rationalp
  (term mfc state)
  (declare (xargs :guard (pseudo-termp term)))
  (if (eq (fn-symb term) 'rationalp)
    (let ((bin-op (fn-symb (fargn term 1))))
      (if (and (member-eq bin-op '(binary-+ binary-*))
          (eq (fn-symb (fargn (fargn term 1) 2)) bin-op))
        (let ((leaves (leaves (fargn term 1) bin-op)))
          (mv-let (intp-leaves non-intp-leaves)
            (bag-leaves leaves mfc state nil nil nil)
            (mv-let (intp-bags non-intp-bags)
              (bag-terms (mfc-type-alist mfc)
                bin-op
                intp-leaves
                non-intp-leaves
                nil)
              (mv-let (flag bag-list)
                (collect-bags leaves intp-bags non-intp-bags bin-op)
                (if flag
                  `(rationalp (meta-integerp-unhide (hide ,(BIG-TREE BAG-LIST
  (IF (EQ BIN-OP 'BINARY-+)
      'INTP-+
      'INTP-*)
  BIN-OP))))
                  term)))))
        term))
    term))
encapsulate
(encapsulate nil
  (local (encapsulate nil
      (local (defthm niq-bounds
          (implies (and (integerp i) (<= 0 i) (integerp j) (< 0 j))
            (and (<= (nonnegative-integer-quotient i j) (/ i j))
              (< (+ (/ i j) -1) (nonnegative-integer-quotient i j))))
          :hints (("Subgoal *1/1''" :use (:instance normalize-<-/-to-*-3-3 (x 1) (y i) (z j))))
          :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))))
      (local (defthm floor-bounds-1
          (implies (and (real/rationalp x) (real/rationalp y))
            (and (< (+ (/ x y) -1) (floor x y))
              (<= (floor x y) (/ x y))))
          :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))
      (local (defthm floor-bounds-2
          (implies (and (real/rationalp x)
              (real/rationalp y)
              (integerp (/ x y)))
            (equal (floor x y) (/ x y)))
          :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))
      (local (defthm floor-bounds-3
          (implies (and (real/rationalp x)
              (real/rationalp y)
              (not (integerp (/ x y))))
            (< (floor x y) (/ x y)))
          :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))
      (local (in-theory (disable floor)))
      (local (defun ind-hint
          (x y n)
          (declare (xargs :measure (abs (ifix x))))
          (cond ((or (zip x) (zip y) (zp n)) t)
            ((equal x -1) t)
            (t (ind-hint (floor x 2) (floor y 2) (+ -1 n))))))
      (local (defthm one
          (implies (and (integerp x)
              (integerp n)
              (< 0 n)
              (<= (- (expt 2 n)) x))
            (equal (< (floor x 2) (- (* 1/2 (expt 2 n)))) nil))))
      (local (defthm two-x
          (implies (and (< x 4) (<= -4 x) (integerp x))
            (or (equal x -4)
              (equal x -3)
              (equal x -2)
              (equal x -1)
              (equal x 0)
              (equal x 1)
              (equal x 2)
              (equal x 3)))
          :rule-classes nil))
      (local (defthm two-y
          (implies (and (< y 4) (<= -4 y) (integerp y))
            (or (equal y -4)
              (equal y -3)
              (equal y -2)
              (equal y -1)
              (equal y 0)
              (equal y 1)
              (equal y 2)
              (equal y 3)))
          :rule-classes nil))
      (local (defthm foo
          (implies (and (integerp x)
              (integerp n)
              (< 1 n)
              (< x (* 1/2 (expt 2 n))))
            (< (+ 1 (* 2 x)) (expt 2 n)))))
      (local (defthm logand-bounds
          (implies (and (integerp x)
              (<= (- (expt 2 n)) x)
              (< x (expt 2 n))
              (integerp y)
              (<= (- (expt 2 n)) y)
              (< y (expt 2 n))
              (integerp n)
              (< 1 n))
            (and (<= (- (expt 2 n)) (logand x y))
              (< (logand x y) (expt 2 n))))
          :hints (("Goal" :in-theory (disable floor expt)
             :induct (ind-hint x y n)
             :do-not '(generalize)) ("Subgoal *1/3.18" :use (two-x two-y))
            ("Subgoal *1/3.17" :use (two-x two-y))
            ("Subgoal *1/3.16" :use (two-x two-y))
            ("Subgoal *1/3.15" :use (two-x two-y))
            ("Subgoal *1/3.14" :use (two-x two-y))
            ("Subgoal *1/3.13" :use (two-x two-y)))))
      (defthm logand-thm
        (implies (and (integerp x)
            (<= *min-type-set* x)
            (<= x *max-type-set*)
            (integerp y)
            (<= *min-type-set* y)
            (<= y *max-type-set*))
          (and (<= *min-type-set* (logand x y))
            (<= (logand x y) *max-type-set*)))
        :hints (("Goal" :use ((:instance logand-bounds
              (n (length *actual-primitive-types*)))))))))
  (verify-guards intp-+)
  (verify-guards intp-*)
  (verify-guards leaves)
  (local (defthm pseudo-term-listp-leaves
      (implies (and (pseudo-termp x)
          (or (equal bin-op 'binary-+) (equal bin-op 'binary-*)))
        (pseudo-term-listp (leaves x bin-op)))))
  (verify-guards tree)
  (verify-guards big-tree)
  (verify-guards bag-leaves)
  (local (defthm pseudo-term-list-listp-bag-leaves
      (implies (and (pseudo-term-listp x)
          (pseudo-term-list-listp y)
          (pseudo-term-list-listp z))
        (and (pseudo-term-list-listp (car (bag-leaves x mfc state y z flag)))
          (pseudo-term-list-listp (mv-nth 1 (bag-leaves x mfc state y z flag)))))))
  (verify-guards bag-terms)
  (local (defthm pseudo-term-list-listp-bag-terms
      (implies (and (type-alistp type-alist)
          (or (equal bin-op 'binary-+) (equal bin-op 'binary-*))
          (pseudo-term-list-listp intp-bags)
          (pseudo-term-list-listp non-intp-bags))
        (and (pseudo-term-list-listp (car (bag-terms type-alist bin-op intp-bags non-intp-bags flag)))
          (pseudo-term-list-listp (mv-nth 1
              (bag-terms type-alist bin-op intp-bags non-intp-bags flag)))))))
  (verify-guards subtract-leaf)
  (local (defthm true-listp-subtract-leaf
      (implies (true-listp leaves)
        (true-listp (mv-nth 1 (subtract-leaf leaf leaves))))))
  (verify-guards subtract-bag :otf-flg t)
  (local (defthm true-listp-subtract-bag
      (implies (true-listp leaves)
        (true-listp (mv-nth 1 (subtract-bag leaf leaves))))))
  (verify-guards collect-bags-intp)
  (verify-guards collect-bags-non-intp)
  (verify-guards collect-bags)
  (local (encapsulate nil
      (local (defthm pseudo-term-list-listp-collect-bags-intp
          (implies (and (true-listp leaves) (pseudo-term-list-listp intp-bags))
            (pseudo-term-list-listp (mv-nth 1 (collect-bags-intp leaves intp-bags))))))
      (local (defthm pseudo-term-list-listp-collect-bags-non-intp
          (implies (and (true-listp leaves)
              (pseudo-term-list-listp intp-bags)
              (pseudo-term-list-listp non-intp-bags))
            (pseudo-term-list-listp (mv-nth 1
                (collect-bags-non-intp leaves intp-bags non-intp-bags))))))
      (defthm pseudo-term-list-listp-collect-bags
        (implies (and (true-listp leaves)
            (pseudo-term-list-listp intp-bags)
            (pseudo-term-list-listp non-intp-bags)
            (or (equal bin-op 'binary-+) (equal bin-op 'binary-*)))
          (pseudo-term-list-listp (mv-nth 1
              (collect-bags leaves intp-bags non-intp-bags bin-op)))))))
  (local (defthm pseudo-term-list-listp-implies-true-list-listp
      (implies (pseudo-term-list-listp x) (true-list-listp x))))
  (verify-guards meta-integerp
    :hints (("Goal" :in-theory (disable bag-leaves bag-terms collect-bags))))
  (verify-guards meta-rationalp
    :hints (("Goal" :in-theory (disable bag-leaves bag-terms collect-bags)))))
meta-integerp-correctencapsulate
(encapsulate nil
  (local (defun tree-2
      (leaves bin-op)
      (cond ((endp leaves) (if (eq bin-op 'binary-+)
            ''0
            ''1))
        (t (list bin-op (car leaves) (tree-2 (cdr leaves) bin-op))))))
  (local (defthm trees
      (implies (or (eq bin-op 'binary-+) (eq bin-op 'binary-*))
        (equal (intp-eva (tree leaves bin-op) a)
          (intp-eva (tree-2 leaves bin-op) a)))))
  (local (in-theory (disable tree)))
  (local (defun big-tree-2
      (bags big-bin-op bin-op)
      (cond ((endp bags) (if (eq bin-op 'binary-+)
            ''0
            ''1))
        (t (list big-bin-op
            (tree (car bags) bin-op)
            (big-tree-2 (cdr bags) big-bin-op bin-op))))))
  (local (defthm big-tree-big-tree-2
      (and (equal (intp-eva (big-tree bags 'intp-+ 'binary-+) a)
          (intp-eva (big-tree-2 bags 'binary-+ 'binary-+) a))
        (equal (intp-eva (big-tree bags 'intp-* 'binary-*) a)
          (intp-eva (big-tree-2 bags 'binary-* 'binary-*) a)))))
  (local (in-theory (disable big-tree)))
  (local (defthm tree-2-leaves
      (implies (and (or (eq bin-op 'binary-+) (eq bin-op 'binary-*))
          (eq (fn-symb term) bin-op))
        (equal (intp-eva (tree-2 (leaves term bin-op) bin-op) a)
          (intp-eva term a)))
      :hints (("Subgoal 2" :induct t) ("Subgoal 1" :induct t))))
  (local (defthm acl2-numberp-tree-2
      (implies (or (eq bin-op 'binary-+) (eq bin-op 'binary-*))
        (acl2-numberp (intp-eva (tree-2 x bin-op) a)))
      :rule-classes :type-prescription))
  (local (defthm subtract-leaf-good-+
      (mv-let (flag new-leaves)
        (subtract-leaf leaf leaves)
        (implies flag
          (equal (+ (intp-eva leaf a)
              (intp-eva (tree-2 new-leaves 'binary-+) a))
            (intp-eva (tree-2 leaves 'binary-+) a))))))
  (local (defthm subtract-leaf-good-*
      (mv-let (flag new-leaves)
        (subtract-leaf leaf leaves)
        (implies flag
          (equal (* (intp-eva leaf a)
              (intp-eva (tree-2 new-leaves 'binary-*) a))
            (intp-eva (tree-2 leaves 'binary-*) a))))))
  (local (defthm subtract-bag-good-+
      (mv-let (flag new-leaves)
        (subtract-bag bag leaves)
        (implies flag
          (equal (+ (intp-eva (tree-2 bag 'binary-+) a)
              (intp-eva (tree-2 new-leaves 'binary-+) a))
            (intp-eva (tree-2 leaves 'binary-+) a))))
      :hints (("Subgoal *1/3" :use ((:instance subtract-leaf-good-+
            (leaf (car bag))
            (leaves (mv-nth 1 (subtract-bag (cdr bag) leaves)))))
         :in-theory (disable subtract-leaf-good-+ tree)))))
  (local (defthm subtract-bag-good-*
      (mv-let (flag new-leaves)
        (subtract-bag bag leaves)
        (implies flag
          (equal (* (intp-eva (tree-2 bag 'binary-*) a)
              (intp-eva (tree-2 new-leaves 'binary-*) a))
            (intp-eva (tree-2 leaves 'binary-*) a))))
      :hints (("Subgoal *1/3" :use ((:instance subtract-leaf-good-*
            (leaf (car bag))
            (leaves (mv-nth 1 (subtract-bag (cdr bag) leaves)))))
         :in-theory (disable subtract-leaf-good-* tree)))))
  (local (defthm collect-bags-intp-good-+
      (mv-let (flag bags)
        (collect-bags-intp leaves intp-bags)
        (implies (and flag (consp leaves))
          (equal (intp-eva (big-tree-2 bags 'binary-+ 'binary-+) a)
            (intp-eva (tree-2 leaves 'binary-+) a))))
      :hints (("Subgoal *1/4'5'" :use ((:instance subtract-bag-good-+ (bag intp-bags1)))
         :in-theory (disable subtract-bag-good-+)))))
  (local (defthm collect-bags-intp-good-*
      (mv-let (flag bags)
        (collect-bags-intp leaves intp-bags)
        (implies (and flag (consp leaves))
          (equal (intp-eva (big-tree-2 bags 'binary-* 'binary-*) a)
            (intp-eva (tree-2 leaves 'binary-*) a))))
      :hints (("Subgoal *1/4'5'" :use ((:instance subtract-bag-good-* (bag intp-bags1)))
         :in-theory (disable subtract-bag-good-*)))))
  (local (defthm collect-bags-good
      (mv-let (flag bags)
        (collect-bags leaves intp-bags non-intp-bags bin-op)
        (implies (and flag
            (member-eq bin-op '(binary-+ binary-*))
            (consp leaves))
          (equal (intp-eva (big-tree-2 bags bin-op bin-op) a)
            (intp-eva (tree-2 leaves bin-op) a))))))
  (local (defthm big-tree-term
      (mv-let (flag bags)
        (collect-bags (leaves term bin-op)
          intp-bags
          non-intp-bags
          bin-op)
        (implies (and flag
            (or (and (eq intp-bin-op 'intp-+) (eq bin-op 'binary-+))
              (and (eq intp-bin-op 'intp-*) (eq bin-op 'binary-*)))
            (eq (fn-symb term) bin-op))
          (equal (intp-eva (big-tree bags intp-bin-op bin-op) a)
            (intp-eva term a))))
      :hints (("Goal" :in-theory (disable leaves collect-bags tree-2)))))
  (local (in-theory (disable leaves
        bag-leaves
        bag-terms
        collect-bags
        big-tree
        intp-+
        intp-*)))
  (defthm meta-integerp-correct
    (equal (intp-eva term a)
      (intp-eva (meta-integerp term mfc state) a))
    :rule-classes ((:meta :trigger-fns (integerp))))
  (defthm meta-rationalp-correct
    (equal (intp-eva term a)
      (intp-eva (meta-rationalp term mfc state) a))
    :rule-classes ((:meta :trigger-fns (rationalp)))))
in-theory
(in-theory (disable leaves
    tree
    big-tree
    bag-leaves
    bag-terms
    subtract-leaf
    subtract-bag
    collect-bags-intp
    collect-bags-non-intp
    collect-bags
    meta-integerp
    meta-rationalp))
in-theory
(in-theory (disable intp-+ intp-*))