Filtering...

k-induction

books/tools/k-induction
other
(in-package "ACL2")
posp-pk-kencapsulate
(encapsulate ((pk (n params) t) (pk-k nil t) (pk-badguy (n params) t))
  (local (defun pk (n params) (declare (ignore n params)) t))
  (local (defun pk-k nil 1))
  (local (defun pk-badguy (n params) (declare (ignore n params)) 0))
  (defthm posp-pk-k
    (posp (pk-k))
    :rule-classes :type-prescription)
  (defthm natp-pk-badguy
    (natp (pk-badguy n params))
    :rule-classes :type-prescription)
  (defthm pk-badguy-range
    (implies (and (natp n) (not (pk n params)))
      (and (< (pk-badguy n params) n)
        (>= (pk-badguy n params) (- n (pk-k)))))
    :rule-classes (:linear :rewrite))
  (defthm pk-badguy-is-counterexample
    (implies (and (natp n) (not (pk n params)))
      (not (pk (pk-badguy n params) params)))))
pk-inductionfunction
(defun pk-induction
  (n params)
  (if (or (zp n) (pk n params))
    t
    (pk-induction (pk-badguy n params) params)))
pk-0theorem
(defthm pk-0
  (pk 0 params)
  :hints (("Goal" :use ((:instance pk-badguy-range (n 0))))))
pk-holdstheorem
(defthm pk-holds
  (implies (natp n) (pk n params))
  :hints (("Goal" :induct (pk-induction n params))))
q-3-propertiesencapsulate
(encapsulate ((q (n x y) t))
  (local (defun q (n x y) (declare (ignore n x y)) t))
  (defthm q-3-properties
    (and (q 0 x y)
      (q 1 x y)
      (q 2 x y)
      (implies (and (natp n)
          (<= 3 n)
          (q (- n 3) x y)
          (q (- n 2) x y)
          (q (- n 1) x y))
        (q n x y)))))
q-paramsfunction
(defun q-params
  (n params)
  (q n (nth 0 params) (nth 1 params)))
q-params-badguyfunction
(defun q-params-badguy
  (n params)
  (cond ((zp n) 0)
    ((not (q-params (- n 1) params)) (- n 1))
    ((equal n 1) 0)
    ((not (q-params (- n 2) params)) (- n 2))
    ((equal n 2) 0)
    (t (- n 3))))
q-params-holdstheorem
(defthmd q-params-holds
  (implies (natp n) (q-params n params))
  :hints (("Goal" :use ((:functional-instance pk-holds
        (pk q-params)
        (pk-k (lambda nil 3))
        (pk-badguy q-params-badguy))))))
q-holdstheorem
(defthm q-holds
  (implies (natp n) (q n x y))
  :hints (("Goal" :use ((:instance q-params-holds (params (list x y)))))))