natp-posp

(in-package "ACL2")

(defsection arithmetic/natp-posp
  :parents (arithmetic-1)
  :short "Lemmas for reasoning about when the basic arithmetic operators
produce natural and positive integer results."
  :long "<p>This is a good, lightweight book for working with @(see natp) and
@(see posp).</p>

<p>For a somewhat heavier and more comprehensive alternative, you may also wish
to see the @(see arith-equivs) book, which introduces, @(see equivalence) relations
like @(see int-equiv) and @(see nat-equiv), and many useful @(see congruence) rules
about these equivalences.</p>"
  (defthm natp-fc-1
    (implies (natp x) (<= 0 x))
    :rule-classes :forward-chaining)
  (defthm natp-fc-2
    (implies (natp x) (integerp x))
    :rule-classes :forward-chaining)
  (defthm posp-fc-1
    (implies (posp x) (< 0 x))
    :rule-classes :forward-chaining)
  (defthm posp-fc-2
    (implies (posp x) (integerp x))
    :rule-classes :forward-chaining)
  (defthm natp-rw
    (implies (and (integerp x) (<= 0 x)) (natp x)))
  (defthm posp-rw
    (implies (and (integerp x) (< 0 x)) (posp x)))
  (defthm |(natp a)  <=>  (posp a+1)|
    (implies (integerp a) (equal (posp (+ 1 a)) (natp a))))
  (encapsulate nil
    (local (defthm posp-natp-l1
        (implies (posp (+ -1 x)) (natp (+ -1 (+ -1 x))))))
    (defthm posp-natp
      (implies (posp (+ -1 x)) (natp (+ -2 x)))
      :hints (("goal" :use posp-natp-l1))))
  (defthm natp-*
    (implies (and (natp a) (natp b)) (natp (* a b))))
  (defthm natp-posp
    (implies (and (natp a) (not (equal a 0))) (posp a)))
  (defthm natp-posp--1
    (equal (natp (+ -1 q)) (posp q))
    :hints (("goal" :in-theory (enable posp natp))))
  (defthm |x < y  =>  0 < -x+y|
    (implies (and (integerp x) (integerp y) (< x y))
      (posp (+ (- x) y)))
    :rule-classes ((:type-prescription)))
  (defthm |x < y  =>  0 < y-x|
    (implies (and (integerp x) (integerp y) (< x y))
      (posp (+ y (- x))))
    :rule-classes ((:type-prescription)))
  (in-theory (disable natp posp)))