types

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

local

(local (include-book "types-helper"))

local

(local (defthm equal-to-iff-1
    (equal (equal (rationalp x) (rationalp y))
      (iff (rationalp x) (rationalp y)))))

local

(local (defthm equal-to-iff-1-real-case
    (equal (equal (real/rationalp x) (real/rationalp y))
      (iff (real/rationalp x) (real/rationalp y)))))

local

(local (defthm equal-to-iff-2
    (equal (equal (integerp x) (integerp y))
      (iff (integerp x) (integerp y)))))

|(rationalp (- x))|theorem

(defthm |(rationalp (- x))|
  (implies (acl2-numberp x)
    (equal (rationalp (- x)) (rationalp x))))

|(integerp (- x))|theorem

(defthm |(integerp (- x))|
  (implies (acl2-numberp x)
    (equal (integerp (- x)) (integerp x))))

rationalp-/theorem

(defthm rationalp-/
  (implies (acl2-numberp x)
    (equal (rationalp (/ x)) (rationalp x))))

not-integerp-/-1theorem

(defthm not-integerp-/-1
  (implies (< 1 x) (not (integerp (/ x)))))

not-integerp-/-2theorem

(defthm not-integerp-/-2
  (implies (< x -1) (not (integerp (/ x)))))

integerp-/theorem

(defthm integerp-/
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp x))
    (equal (integerp (/ x))
      (or (equal x -1) (equal x 0) (equal x 1)))))

rationalp-xtheorem

(defthm rationalp-x
  (implies (integerp x) (rationalp x))
  :rule-classes ((:rewrite :backchain-limit-lst 2)))

acl2-numberp-xtheorem

(defthm acl2-numberp-x
  (implies (rationalp x) (acl2-numberp x))
  :rule-classes ((:rewrite :backchain-limit-lst 3)))

Included Books