Theory "numeral_bit"

Signature

Definitions

BIT_REV_def

|- (!x y. BIT_REV 0 x y = y) /\
   !n x y. BIT_REV (SUC n) x y = BIT_REV n (x DIV 2) (2 * y + SBIT (ODD x) 0)

BIT_MODF_def

|- (!f x b e y. BIT_MODF 0 f x b e y = y) /\
   !n f x b e y.
     BIT_MODF (SUC n) f x b e y =
     BIT_MODF n f (x DIV 2) (b + 1) (2 * e) (if f b (ODD x) then e + y else y)

iBITWISE_def

|- iBITWISE = BITWISE

iLOG2_def

|- !n. iLOG2 n = LOG2 (n + 1)

Theorems

BIT_REVERSE_EVAL

|- !m n. BIT_REVERSE m n = BIT_REV m n 0

BIT_MODIFY_EVAL

|- !m f n. BIT_MODIFY m f n = BIT_MODF m f n 0 1 0

iBITWISE

|- (!opr a b. iBITWISE 0 opr a b = ZERO) /\
   (!x opr a b.
      iBITWISE (NUMERAL (BIT1 x)) opr a b =
      (let w = iBITWISE (NUMERAL (BIT1 x) - 1) opr (DIV2 a) (DIV2 b) in
         (if opr (ODD a) (ODD b) then BIT1 w else numeral$iDUB w))) /\
   !x opr a b.
     iBITWISE (NUMERAL (BIT2 x)) opr a b =
     (let w = iBITWISE (NUMERAL (BIT1 x)) opr (DIV2 a) (DIV2 b) in
        (if opr (ODD a) (ODD b) then BIT1 w else numeral$iDUB w))

NUMERAL_BITWISE

|- (!x f a. BITWISE x f 0 0 = NUMERAL (iBITWISE x f 0 0)) /\
   (!x f a.
      BITWISE x f (NUMERAL a) 0 = NUMERAL (iBITWISE x f (NUMERAL a) 0)) /\
   (!x f b.
      BITWISE x f 0 (NUMERAL b) = NUMERAL (iBITWISE x f 0 (NUMERAL b))) /\
   !x f a b.
     BITWISE x f (NUMERAL a) (NUMERAL b) =
     NUMERAL (iBITWISE x f (NUMERAL a) (NUMERAL b))

NUMERAL_BIT_REV

|- (!x y. BIT_REV 0 x y = y) /\
   (!n y.
      BIT_REV (NUMERAL (BIT1 n)) 0 y =
      BIT_REV (NUMERAL (BIT1 n) - 1) 0 (numeral$iDUB y)) /\
   (!n y.
      BIT_REV (NUMERAL (BIT2 n)) 0 y =
      BIT_REV (NUMERAL (BIT1 n)) 0 (numeral$iDUB y)) /\
   (!n x y.
      BIT_REV (NUMERAL (BIT1 n)) (NUMERAL x) y =
      BIT_REV (NUMERAL (BIT1 n) - 1) (DIV2 (NUMERAL x))
        (if ODD x then BIT1 y else numeral$iDUB y)) /\
   !n x y.
     BIT_REV (NUMERAL (BIT2 n)) (NUMERAL x) y =
     BIT_REV (NUMERAL (BIT1 n)) (DIV2 (NUMERAL x))
       (if ODD x then BIT1 y else numeral$iDUB y)

NUMERAL_BIT_REVERSE

|- (!m. BIT_REVERSE (NUMERAL m) 0 = NUMERAL (BIT_REV (NUMERAL m) 0 ZERO)) /\
   !n m.
     BIT_REVERSE (NUMERAL m) (NUMERAL n) =
     NUMERAL (BIT_REV (NUMERAL m) (NUMERAL n) ZERO)

NUMERAL_BIT_MODF

|- (!f x b e y. BIT_MODF 0 f x b e y = y) /\
   (!n f b e y.
      BIT_MODF (NUMERAL (BIT1 n)) f 0 b (NUMERAL e) y =
      BIT_MODF (NUMERAL (BIT1 n) - 1) f 0 (b + 1) (NUMERAL (numeral$iDUB e))
        (if f b F then NUMERAL e + y else y)) /\
   (!n f b e y.
      BIT_MODF (NUMERAL (BIT2 n)) f 0 b (NUMERAL e) y =
      BIT_MODF (NUMERAL (BIT1 n)) f 0 (b + 1) (NUMERAL (numeral$iDUB e))
        (if f b F then NUMERAL e + y else y)) /\
   (!n f x b e y.
      BIT_MODF (NUMERAL (BIT1 n)) f (NUMERAL x) b (NUMERAL e) y =
      BIT_MODF (NUMERAL (BIT1 n) - 1) f (DIV2 (NUMERAL x)) (b + 1)
        (NUMERAL (numeral$iDUB e))
        (if f b (ODD x) then NUMERAL e + y else y)) /\
   !n f x b e y.
     BIT_MODF (NUMERAL (BIT2 n)) f (NUMERAL x) b (NUMERAL e) y =
     BIT_MODF (NUMERAL (BIT1 n)) f (DIV2 (NUMERAL x)) (b + 1)
       (NUMERAL (numeral$iDUB e)) (if f b (ODD x) then NUMERAL e + y else y)

NUMERAL_BIT_MODIFY

|- (!m f. BIT_MODIFY (NUMERAL m) f 0 = BIT_MODF (NUMERAL m) f 0 0 1 0) /\
   !m f n.
     BIT_MODIFY (NUMERAL m) f (NUMERAL n) =
     BIT_MODF (NUMERAL m) f (NUMERAL n) 0 1 0

NUMERAL_TIMES_2EXP

|- (!n. TIMES_2EXP n 0 = 0) /\ (!x. TIMES_2EXP 0 x = x) /\
   !x n.
     TIMES_2EXP (NUMERAL x) (NUMERAL n) =
     NUMERAL n * NUMERAL (FUNPOW numeral$iDUB (NUMERAL x) (BIT1 ZERO))

NUMERAL_DIV_2EXP

|- (!n. DIV_2EXP 0 n = n) /\ (!x. DIV_2EXP x 0 = 0) /\
   (!x n.
      DIV_2EXP (NUMERAL (BIT1 x)) (NUMERAL n) =
      DIV_2EXP (NUMERAL (BIT1 x) - 1) (DIV2 (NUMERAL n))) /\
   !x n.
     DIV_2EXP (NUMERAL (BIT2 x)) (NUMERAL n) =
     DIV_2EXP (NUMERAL (BIT1 x)) (DIV2 (NUMERAL n))

numeral_ilog2

|- (iLOG2 ZERO = 0) /\ (!n. iLOG2 (BIT1 n) = 1 + iLOG2 n) /\
   !n. iLOG2 (BIT2 n) = 1 + iLOG2 n

numeral_log2

|- (!n. LOG2 (NUMERAL (BIT1 n)) = iLOG2 (numeral$iDUB n)) /\
   !n. LOG2 (NUMERAL (BIT2 n)) = iLOG2 (BIT1 n)