		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-1

Arithmetic/natp-posp

Lemmas for reasoning about when the basic arithmetic operators produce natural and positive integer results.

This is a good, lightweight book for working with natp and posp.

For a somewhat heavier and more comprehensive alternative, you may also wish to see the arith-equivs book, which introduces, equivalence relations like int-equiv and nat-equiv, and many useful congruence rules about these equivalences.

Definitions and Theorems

Theorem: natp-fc-1

(defthm natp-fc-1
  (implies (natp x) (<= 0 x))
  :rule-classes :forward-chaining)

Theorem: natp-fc-2

(defthm natp-fc-2
  (implies (natp x) (integerp x))
  :rule-classes :forward-chaining)

Theorem: posp-fc-1

(defthm posp-fc-1
  (implies (posp x) (< 0 x))
  :rule-classes :forward-chaining)

Theorem: posp-fc-2

(defthm posp-fc-2
  (implies (posp x) (integerp x))
  :rule-classes :forward-chaining)

Theorem: natp-rw

(defthm natp-rw
  (implies (and (integerp x) (<= 0 x))
           (natp x)))

Theorem: posp-rw

(defthm posp-rw
  (implies (and (integerp x) (< 0 x))
           (posp x)))

Theorem: (natp a) <=> (posp a+1)

(defthm |(natp a)  <=>  (posp a+1)|
  (implies (integerp a)
           (equal (posp (+ 1 a)) (natp a))))

Theorem: posp-natp

(defthm posp-natp
  (implies (posp (+ -1 x))
           (natp (+ -2 x))))

Theorem: natp-*

(defthm natp-*
  (implies (and (natp a) (natp b))
           (natp (* a b))))

Theorem: natp-posp

(defthm natp-posp
  (implies (and (natp a) (not (equal a 0)))
           (posp a)))

Theorem: natp-posp--1

(defthm natp-posp--1
  (equal (natp (+ -1 q)) (posp q)))

Theorem: x < y => 0 < -x+y

(defthm |x < y  =>  0 < -x+y|
  (implies (and (integerp x) (integerp y) (< x y))
           (posp (+ (- x) y)))
  :rule-classes ((:type-prescription)))

Theorem: x < y => 0 < y-x

(defthm |x < y  =>  0 < y-x|
  (implies (and (integerp x) (integerp y) (< x y))
           (posp (+ y (- x))))
  :rule-classes ((:type-prescription)))