• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
        • Inequalities-of-products
        • Basic-product-normalization
        • Inequalities-of-reciprocals
        • Arithmetic/natp-posp
        • Basic-expt-normalization
        • More-rational-identities
        • Inequalities-of-exponents
        • Basic-sum-normalization
        • Basic-rational-identities
        • Basic-expt-type-rules
        • Inequalities-of-sums
        • Basic-products-with-negations
        • Fc
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

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