limits - ACL2 Book

other

(in-package "LRAT")

other

(defconst *2^0* (expt 2 0))

other

(defconst *2^1* (expt 2 1))

other

(defconst *2^2* (expt 2 2))

other

(defconst *2^3* (expt 2 3))

other

(defconst *2^4* (expt 2 4))

other

(defconst *2^5* (expt 2 5))

other

(defconst *2^6* (expt 2 6))

other

(defconst *2^8* (expt 2 8))

other

(defconst *2^10* (expt 2 10))

other

(defconst *2^16* (expt 2 16))

other

(defconst *2^24* (expt 2 24))

other

(defconst *2^28* (expt 2 28))

other

(defconst *2^32* (expt 2 32))

other

(defconst *2^40* (expt 2 40))

other

(defconst *2^48* (expt 2 48))

other

(defconst *2^56* (expt 2 56))

other

(defconst *2^57* (expt 2 57))

other

(defconst *2^58* (expt 2 58))

other

(defconst *2^59* (expt 2 59))

other

(defconst *2^60* (expt 2 60))

other

(defconst *2^64* (expt 2 64))

other

(defconst *nmax* *2^59*)

other

(defconst *-nmax* (- *nmax*))

u01macro

(defmacro u01
  (x)
  `(the (unsigned-byte 1) ,LRAT::X))

u02macro

(defmacro u02
  (x)
  `(the (unsigned-byte 2) ,LRAT::X))

u03macro

(defmacro u03
  (x)
  `(the (unsigned-byte 3) ,LRAT::X))

u04macro

(defmacro u04
  (x)
  `(the (unsigned-byte 4) ,LRAT::X))

u05macro

(defmacro u05
  (x)
  `(the (unsigned-byte 5) ,LRAT::X))

u06macro

(defmacro u06
  (x)
  `(the (unsigned-byte 6) ,LRAT::X))

u08macro

(defmacro u08
  (x)
  `(the (unsigned-byte 8) ,LRAT::X))

u10macro

(defmacro u10
  (x)
  `(the (unsigned-byte 10) ,LRAT::X))

u16macro

(defmacro u16
  (x)
  `(the (unsigned-byte 16) ,LRAT::X))

u24macro

(defmacro u24
  (x)
  `(the (unsigned-byte 24) ,LRAT::X))

u28macro

(defmacro u28
  (x)
  `(the (unsigned-byte 28) ,LRAT::X))

u32macro

(defmacro u32
  (x)
  `(the (unsigned-byte 32) ,LRAT::X))

u40macro

(defmacro u40
  (x)
  `(the (unsigned-byte 40) ,LRAT::X))

u48macro

(defmacro u48
  (x)
  `(the (unsigned-byte 48) ,LRAT::X))

u56macro

(defmacro u56
  (x)
  `(the (unsigned-byte 56) ,LRAT::X))

u59macro

(defmacro u59
  (x)
  `(the (unsigned-byte 59) ,LRAT::X))

u60macro

(defmacro u60
  (x)
  `(the (unsigned-byte 60) ,LRAT::X))

u64macro

(defmacro u64
  (x)
  `(the (unsigned-byte 64) ,LRAT::X))

s01macro

(defmacro s01
  (x)
  `(the (signed-byte 1) ,LRAT::X))

s02macro

(defmacro s02
  (x)
  `(the (signed-byte 2) ,LRAT::X))

s03macro

(defmacro s03
  (x)
  `(the (signed-byte 3) ,LRAT::X))

s04macro

(defmacro s04
  (x)
  `(the (signed-byte 4) ,LRAT::X))

s05macro

(defmacro s05
  (x)
  `(the (signed-byte 5) ,LRAT::X))

s06macro

(defmacro s06
  (x)
  `(the (signed-byte 6) ,LRAT::X))

s08macro

(defmacro s08
  (x)
  `(the (signed-byte 8) ,LRAT::X))

s10macro

(defmacro s10
  (x)
  `(the (signed-byte 10) ,LRAT::X))

s16macro

(defmacro s16
  (x)
  `(the (signed-byte 16) ,LRAT::X))

s24macro

(defmacro s24
  (x)
  `(the (signed-byte 24) ,LRAT::X))

s28macro

(defmacro s28
  (x)
  `(the (signed-byte 28) ,LRAT::X))

s32macro

(defmacro s32
  (x)
  `(the (signed-byte 32) ,LRAT::X))

s40macro

(defmacro s40
  (x)
  `(the (signed-byte 40) ,LRAT::X))

s48macro

(defmacro s48
  (x)
  `(the (signed-byte 48) ,LRAT::X))

s56macro

(defmacro s56
  (x)
  `(the (signed-byte 56) ,LRAT::X))

s57macro

(defmacro s57
  (x)
  `(the (signed-byte 57) ,LRAT::X))

s58macro

(defmacro s58
  (x)
  `(the (signed-byte 58) ,LRAT::X))

s59macro

(defmacro s59
  (x)
  `(the (signed-byte 59) ,LRAT::X))

s60macro

(defmacro s60
  (x)
  `(the (signed-byte 60) ,LRAT::X))

s64macro

(defmacro s64
  (x)
  `(the (signed-byte 64) ,LRAT::X))

n01macro

(defmacro n01
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^1*)))

n02macro

(defmacro n02
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^2*)))

n03macro

(defmacro n03
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^3*)))

n04macro

(defmacro n04
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^4*)))

n05macro

(defmacro n05
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^5*)))

n06macro

(defmacro n06
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^6*)))

n08macro

(defmacro n08
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^8*)))

n10macro

(defmacro n10
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^10*)))

n16macro

(defmacro n16
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^16*)))

n24macro

(defmacro n24
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^24*)))

n28macro

(defmacro n28
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^28*)))

n32macro

(defmacro n32
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^32*)))

n40macro

(defmacro n40
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^40*)))

n48macro

(defmacro n48
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^48*)))

n56macro

(defmacro n56
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^56*)))

n57macro

(defmacro n57
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^57*)))

n58macro

(defmacro n58
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^58*)))

n59macro

(defmacro n59
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^59*)))

n60macro

(defmacro n60
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^60*)))

n64macro

(defmacro n64
  (x)
  `(logand ,LRAT::X ,(1- LRAT::*2^64*)))

i01macro

(defmacro i01
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^1*))))
    (if (>= sx *2^0*)
      (+ sx (- *2^1*))
      sx)))

i02macro

(defmacro i02
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^2*))))
    (if (>= sx *2^1*)
      (+ sx (- *2^2*))
      sx)))

i03macro

(defmacro i03
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^3*))))
    (if (>= sx *2^2*)
      (+ sx (- *2^3*))
      sx)))

i04macro

(defmacro i04
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^4*))))
    (if (>= sx *2^3*)
      (+ sx (- *2^4*))
      sx)))

i05macro

(defmacro i05
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^5*))))
    (if (>= sx *2^4*)
      (+ sx (- *2^5*))
      sx)))

i06macro

(defmacro i06
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^6*))))
    (if (>= sx *2^5*)
      (+ sx (- *2^6*))
      sx)))

i08macro

(defmacro i08
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^8*))))
    (if (>= sx *2^7*)
      (+ sx (- *2^8*))
      sx)))

i10macro

(defmacro i10
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^10*))))
    (if (>= sx *2^9*)
      (+ sx (- *2^10*))
      sx)))

i16macro

(defmacro i16
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^16*))))
    (if (>= sx *2^15*)
      (+ sx (- *2^16*))
      sx)))

i24macro

(defmacro i24
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^24*))))
    (if (>= sx *2^23*)
      (+ sx (- *2^24*))
      sx)))

i32macro

(defmacro i32
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^32*))))
    (if (>= sx *2^31*)
      (+ sx (- *2^32*))
      sx)))

i40macro

(defmacro i40
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^40*))))
    (if (>= sx *2^39*)
      (+ sx (- *2^40*))
      sx)))

i48macro

(defmacro i48
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^48*))))
    (if (>= sx *2^47*)
      (+ sx (- *2^48*))
      sx)))

i56macro

(defmacro i56
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^56*))))
    (if (>= sx *2^55*)
      (+ sx (- *2^56*))
      sx)))

i57macro

(defmacro i57
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^57*))))
    (if (>= sx *2^56*)
      (+ sx (- *2^57*))
      sx)))

i58macro

(defmacro i58
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^58*))))
    (if (>= sx *2^57*)
      (+ sx (- *2^58*))
      sx)))

i60macro

(defmacro i60
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^60*))))
    (if (>= sx *2^59*)
      (+ sx (- *2^60*))
      sx)))

i64macro

(defmacro i64
  (x)
  `(let ((sx (logand ,LRAT::X ,(1- LRAT::*2^64*))))
    (if (>= sx *2^63*)
      (+ sx (- *2^64*))
      sx)))

n01pmacro

(defmacro n01p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^1*))))

n02pmacro

(defmacro n02p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^2*))))

n03pmacro

(defmacro n03p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^3*))))

n04pmacro

(defmacro n04p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^4*))))

n05pmacro

(defmacro n05p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^5*))))

n06pmacro

(defmacro n06p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^6*))))

n08pmacro

(defmacro n08p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^8*))))

n10pmacro

(defmacro n10p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^10*))))

n16pmacro

(defmacro n16p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^16*))))

n24pmacro

(defmacro n24p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^24*))))

n28pmacro

(defmacro n28p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^28*))))

n32pmacro

(defmacro n32p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^32*))))

n40pmacro

(defmacro n40p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^40*))))

n48pmacro

(defmacro n48p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^48*))))

n56pmacro

(defmacro n56p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^56*))))

n57pmacro

(defmacro n57p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^57*))))

n58pmacro

(defmacro n58p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^58*))))

n59pmacro

(defmacro n59p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^59*))))

n60pmacro

(defmacro n60p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^60*))))

n64pmacro

(defmacro n64p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= 0 x)
      (< x *2^64*))))

i01pmacro

(defmacro i01p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^0*) x)
      (< x *2^0*))))

i02pmacro

(defmacro i02p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^1*) x)
      (< x *2^1*))))

i03pmacro

(defmacro i03p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^2*) x)
      (< x *2^2*))))

i04pmacro

(defmacro i04p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^3*) x)
      (< x *2^3*))))

i05pmacro

(defmacro i05p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^4*) x)
      (< x *2^4*))))

i06pmacro

(defmacro i06p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^5*) x)
      (< x *2^5*))))

i08pmacro

(defmacro i08p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^7*) x)
      (< x *2^7*))))

i10pmacro

(defmacro i10p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^9*) x)
      (< x *2^9*))))

i16pmacro

(defmacro i16p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^15*) x)
      (< x *2^15*))))

i24pmacro

(defmacro i24p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^23*) x)
      (< x *2^23*))))

i28pmacro

(defmacro i28p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^27*) x)
      (< x *2^27*))))

i32pmacro

(defmacro i32p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^31*) x)
      (< x *2^31*))))

i40pmacro

(defmacro i40p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^39*) x)
      (< x *2^39*))))

i48pmacro

(defmacro i48p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^47*) x)
      (< x *2^47*))))

i56pmacro

(defmacro i56p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^55*) x)
      (< x *2^55*))))

i57pmacro

(defmacro i57p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^56*) x)
      (< x *2^56*))))

i58pmacro

(defmacro i58p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^57*) x)
      (< x *2^57*))))

i60pmacro

(defmacro i60p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^59*) x)
      (< x *2^59*))))

i64pmacro

(defmacro i64p
  (x)
  `(let ((x ,LRAT::X))
    (and (integerp x)
      (<= (- *2^63*) x)
      (< x *2^63*))))

n59-listpfunction

(defun n59-listp
  (xs)
  (declare (xargs :guard t))
  (if (atom xs)
    (null xs)
    (and (n59p (car xs))
      (n59-listp (cdr xs)))))

other

(defthm n59-listp-forward
  (implies (n59-listp x)
    (true-listp x))
  :rule-classes (:forward-chaining :rewrite))

other

(defthm nth-n59-listp
  (implies (and (n59-listp xs)
      (natp i)
      (< i (len xs)))
    (n59p (nth i xs)))
  :rule-classes ((:type-prescription :corollary (implies (and (n59-listp xs)
         (natp i)
         (< i (len xs)))
       (natp (nth i xs)))) (:linear :corollary (implies (and (n59-listp xs)
          (natp i)
          (< i (len xs)))
        (and (<= 0 (nth i xs))
          (< (nth i xs) *2^59*))))))

i60-listpfunction

(defun i60-listp
  (xs)
  (declare (xargs :guard t))
  (if (atom xs)
    (null xs)
    (and (i60p (car xs))
      (i60-listp (cdr xs)))))

other

(defthm i60-listp-forward
  (implies (i60-listp x)
    (true-listp x))
  :rule-classes (:forward-chaining :rewrite))

other

(defthm nth-i60-listp
  (implies (and (i60-listp xs)
      (natp i)
      (< i (len xs)))
    (i60p (nth i xs)))
  :rule-classes ((:type-prescription :corollary (implies (and (i60-listp xs)
         (natp i)
         (< i (len xs)))
       (integerp (nth i xs)))) (:linear :corollary (implies (and (i60-listp xs)
          (natp i)
          (< i (len xs)))
        (and (<= (- *2^59*) (nth i xs))
          (< (nth i xs) *2^59*))))))