def-bound-theorems-tests

(in-package "STD")

(include-book "def-bound-theorems")

(defund foo
  (x)
  (if (unsigned-byte-p 8 x)
    x
    0))

(defthm-unsigned-byte-p unsigned-byte-p-foo
  :bound 8
  :concl (foo x)
  :gen-type t
  :gen-linear t
  :hints (("Goal" :in-theory (enable foo))))

(defund bar
  (x)
  (if (unsigned-byte-p 1 x)
    x
    0))

(defthm-unsigned-byte-p unsigned-byte-p-bar
  :bound 1
  :concl (bar x)
  :gen-type t
  :gen-linear t
  :hints (("Goal" :in-theory (enable bar))))

(defund decrement (x) (+ -1 x))

(defthm-unsigned-byte-p unsigned-byte-p-decrement
  :bound 8
  :hyp (and (unsigned-byte-p 8 x) (< 0 x))
  :concl (decrement x)
  :gen-type t
  :gen-linear t
  :hints (("Goal" :in-theory (enable decrement))))