integerp-meta - ACL2 Book

Included Books

top

other

(in-package "ACL2")

local

(local (include-book "../pass1/top"))

other

(table acl2-defaults-table :state-ok t)

ts-fixfunction

(defun ts-fix
  (x)
  (let ((int-x (ifix x)))
    (if (and (<= *min-type-set* int-x) (<= int-x *max-type-set*))
      int-x
      0)))

intp-+function

(defun intp-+ (x y) (+ x y))

intp-*function

(defun intp-* (x y) (* x y))

other

(defevaluator intp-eva
  intp-eva-lst
  ((intp-+ x y) (intp-* x y)
    (binary-+ x y)
    (binary-* x y)
    (integerp 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))))

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)))))

leavesfunction

(defun leaves
  (term bin-op)
  (cond ((atom term) (if (eq bin-op 'binary-+)
        ''0
        ''1))
    ((eq (fn-symb term) bin-op) (if (eq (fn-symb (fargn term 2)) bin-op)
        (cons (fargn term 1) (leaves (fargn term 2) bin-op))
        (list (fargn term 1) (fargn term 2))))
    (t (list term))))

treefunction

(defun tree
  (leaves bin-op)
  (cond ((endp leaves) (if (eq bin-op 'binary-+)
        ''0
        ''1))
    ((endp (cdr leaves)) (list 'fix (car leaves)))
    ((endp (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)
  (cond ((endp bags) (if (eq bin-op 'binary-+)
        ''0
        ''1))
    ((endp (cdr bags)) (tree (car bags) bin-op))
    ((endp (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)
  (if (endp leaves)
    (mv intp-bags non-intp-bags)
    (let ((leaf-type (ts-fix (mfc-ts (car leaves) mfc state))))
      (cond ((ts-subsetp leaf-type *ts-integer*) (bag-leaves (cdr leaves)
            mfc
            state
            (cons (list (car leaves)) intp-bags)
            non-intp-bags))
        ((and (ts-subsetp leaf-type *ts-acl2-number*)
           (ts-subsetp leaf-type (ts-complement *ts-integer*))) (bag-leaves (cdr leaves)
            mfc
            state
            intp-bags
            (cons (list (car leaves)) non-intp-bags)))
        (t (bag-leaves (cdr leaves) mfc state intp-bags non-intp-bags))))))

bag-termsfunction

(defun bag-terms
  (type-alist bin-op intp-bags non-intp-bags)
  (cond ((endp type-alist) (mv intp-bags non-intp-bags))
    ((variablep (caar type-alist)) (bag-terms (cdr type-alist) bin-op intp-bags non-intp-bags))
    ((ts-subsetp (cadr (car type-alist)) *ts-integer*) (bag-terms (cdr type-alist)
        bin-op
        (cons (leaves (caar type-alist) bin-op) intp-bags)
        non-intp-bags))
    ((and (ts-subsetp (cadr (car type-alist)) *ts-acl2-number*)
       (ts-subsetp (cadr (car type-alist))
         (ts-complement *ts-integer*))) (bag-terms (cdr type-alist)
        bin-op
        intp-bags
        (cons (leaves (caar type-alist) bin-op) non-intp-bags)))
    (t (bag-terms (cdr type-alist) bin-op intp-bags non-intp-bags))))

subtract-leaffunction

(defun subtract-leaf
  (leaf 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)
  (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 leaves))))))

collect-bags-intpfunction

(defun collect-bags-intp
  (leaves 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)
  (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)
  (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)
  (if (consp term)
    (let ((bin-op (fn-symb (fargn term 1))))
      (if (and (member-eq bin-op '(binary-+ binary-*))
          (eq (fn-symb term) 'integerp)
          (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)
            (mv-let (intp-bags non-intp-bags)
              (bag-terms (mfc-type-alist mfc)
                bin-op
                intp-leaves
                non-intp-leaves)
              (mv-let (flag bag-list)
                (collect-bags leaves intp-bags non-intp-bags bin-op)
                (if flag
                  `(integerp ,(BIG-TREE BAG-LIST
  (IF (EQ BIN-OP 'BINARY-+)
      'INTP-+
      'INTP-*)
  BIN-OP))
                  term)))))
        term))
    term))

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)))))

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))

in-theory

(in-theory (disable intp-+ intp-*))