natp-posp

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

local

(local (include-book "../../support/top"))

natp-fc-1theorem

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

natp-fc-2theorem

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

posp-fc-1theorem

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

posp-fc-2theorem

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

natp-rwtheorem

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

posp-rwtheorem

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

natp-posptheorem

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

|(posp (+ c x))|theorem

(defthm |(posp (+ c x))|
  (implies (and (syntaxp (quotep c)) (< 0 c) (integerp a))
    (equal (posp (+ c a)) (natp (+ (- c 1) a)))))

|(natp (+ c x))|theorem

(defthm |(natp (+ c x))|
  (implies (and (syntaxp (quotep c)) (< c 0) (integerp a))
    (equal (natp (+ c x)) (posp (+ (+ c 1) x)))))

|(natp (* x y))|theorem

(defthm |(natp (* x y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp x)
      (integerp y))
    (equal (natp (* x y))
      (or (and (natp x) (natp y)) (and (natp (- x)) (natp (- y)))))))

|(natp (* x y)) backchaining|theorem

(defthm |(natp (* x y)) backchaining|
  (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
      (natp x)
      (natp y))
    (natp (* x y))))

|(posp (* x y))|theorem

(defthm |(posp (* x y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp x)
      (integerp y))
    (equal (posp (* x y))
      (or (and (posp x) (posp y)) (and (posp (- x)) (posp (- y)))))))

|(posp (* x y)) backchaining|theorem

(defthm |(posp (* x y)) backchaining|
  (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
      (posp x)
      (posp y))
    (posp (* x y))))

|x < y => 0 < -x+y|theorem

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

|x < y => 0 < y-x|theorem

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

|x < y => 0 <= -x+y|theorem

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

|x < y => 0 <= y-x|theorem

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

in-theory

(in-theory (disable natp posp))

Included Books