Theory "bit"

Parents logroot

Signature

Constant	Type
BIT	:num reln
BITS	:num -> num -> num -> num
BITV	:num -> num -> num
BITWISE	:num -> bool reln -> num -> num -> num
BIT_MODIFY	:num -> (num -> bool -> bool) -> num -> num
BIT_REVERSE	:num -> num -> num
DIVMOD_2EXP	:num -> num -> num # num
DIV_2EXP	:num -> num -> num
LOG2	:num -> num
LOWEST_SET_BIT	:num -> num
MOD_2EXP	:num -> num -> num
MOD_2EXP_EQ	:num -> num reln
MOD_2EXP_MAX	:num reln
SBIT	:bool -> num -> num
SIGN_EXTEND	:num -> num -> num -> num
SLICE	:num -> num -> num -> num
TIMES_2EXP	:num -> num -> num

Definitions

MOD_2EXP_def

⊢ ∀x n. MOD_2EXP x n = n MOD 2 ** x

DIV_2EXP_def

⊢ ∀x n. DIV_2EXP x n = n DIV 2 ** x

TIMES_2EXP_def

⊢ ∀x n. TIMES_2EXP x n = n * 2 ** x

DIVMOD_2EXP_def

⊢ ∀x n. DIVMOD_2EXP x n = (n DIV 2 ** x,n MOD 2 ** x)

SBIT_def

⊢ ∀b n. SBIT b n = if b then 2 ** n else 0

BITS_def

⊢ ∀h l n. BITS h l n = MOD_2EXP (SUC h − l) (DIV_2EXP l n)

BITV_def

⊢ ∀n b. BITV n b = BITS b b n

BIT_def

⊢ ∀b n. BIT b n ⇔ BITS b b n = 1

SLICE_def

⊢ ∀h l n. SLICE h l n = MOD_2EXP (SUC h) n − MOD_2EXP l n

LOG2_def

⊢ LOG2 = LOG 2

LOWEST_SET_BIT_def

⊢ ∀n. LOWEST_SET_BIT n = LEAST i. BIT i n

BIT_REVERSE_def

⊢ (∀x. BIT_REVERSE 0 x = 0) ∧
  ∀n x. BIT_REVERSE (SUC n) x = BIT_REVERSE n x * 2 + SBIT (BIT n x) 0

BITWISE_def

⊢ (∀op x y. BITWISE 0 op x y = 0) ∧
  ∀n op x y.
      BITWISE (SUC n) op x y =
      BITWISE n op x y + SBIT (op (BIT n x) (BIT n y)) n

BIT_MODIFY_def

⊢ (∀f x. BIT_MODIFY 0 f x = 0) ∧
  ∀n f x. BIT_MODIFY (SUC n) f x = BIT_MODIFY n f x + SBIT (f n (BIT n x)) n

SIGN_EXTEND_def

⊢ ∀l h n.
      SIGN_EXTEND l h n =
      (let
         m = n MOD 2 ** l
       in
         if BIT (l − 1) n then 2 ** h − 2 ** l + m else m)

MOD_2EXP_EQ_def

⊢ ∀n a b. MOD_2EXP_EQ n a b ⇔ MOD_2EXP n a = MOD_2EXP n b

MOD_2EXP_MAX_def

⊢ ∀n a. MOD_2EXP_MAX n a ⇔ MOD_2EXP n a = 2 ** n − 1

Theorems

LESS_MULT_MONO2

⊢ ∀a b x y. a < x ∧ b < y ⇒ a * b < x * y

LOG2_UNIQUE

⊢ ∀n p. 2 ** p ≤ n ∧ n < 2 ** SUC p ⇒ LOG2 n = p

LOG2_TWOEXP

⊢ ∀n. LOG2 (2 ** n) = n

DIVMOD_2EXP

⊢ ∀x n. DIVMOD_2EXP x n = (DIV_2EXP x n,MOD_2EXP x n)

SUC_SUB

⊢ ∀a. SUC a − a = 1

DIV_MULT_1

⊢ ∀r n. r < n ⇒ (n + r) DIV n = 1

NOT_ZERO_ADD1

⊢ ∀m. m ≠ 0 ⇒ ∃p. m = SUC p

ZERO_LT_TWOEXP

⊢ ∀n. 0 < 2 ** n

ONE_LE_TWOEXP

⊢ ∀n. 1 ≤ 2 ** n

TWOEXP_NOT_ZERO

⊢ ∀n. 2 ** n ≠ 0

MOD_2EXP_LT

⊢ ∀n k. k MOD 2 ** n < 2 ** n

TWOEXP_DIVISION

⊢ ∀n k. k = k DIV 2 ** n * 2 ** n + k MOD 2 ** n

TWOEXP_MONO

⊢ ∀a b. a < b ⇒ 2 ** a < 2 ** b

TWOEXP_MONO2

⊢ ∀a b. a ≤ b ⇒ 2 ** a ≤ 2 ** b

EXP_SUB_LESS_EQ

⊢ ∀a b. 2 ** (a − b) ≤ 2 ** a

MOD_LEQ

⊢ ∀a b. 0 < b ⇒ a MOD b ≤ a

BITS_THM

⊢ ∀h l n. BITS h l n = (n DIV 2 ** l) MOD 2 ** (SUC h − l)

BITSLT_THM

⊢ ∀h l n. BITS h l n < 2 ** (SUC h − l)

BITSLT_THM2

⊢ ∀h l n. BITS h l n < 2 ** SUC h

BITS_THM2

⊢ ∀h l n. BITS h l n = n MOD 2 ** SUC h DIV 2 ** l

BITS_LEQ

⊢ ∀h l n. BITS h l n ≤ n

BITS_COMP_THM

⊢ ∀h1 l1 h2 l2 n.
      h2 + l1 ≤ h1 ⇒ BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n

BITS_DIV_THM

⊢ ∀h l x n. BITS h l x DIV 2 ** n = BITS h (l + n) x

BITS_LT_HIGH

⊢ ∀h l n. n < 2 ** SUC h ⇒ BITS h l n = n DIV 2 ** l

BITS_ZERO

⊢ ∀h l n. h < l ⇒ BITS h l n = 0

BITS_ZERO2

⊢ ∀h l. BITS h l 0 = 0

BITS_ZERO3

⊢ ∀h n. BITS h 0 n = n MOD 2 ** SUC h

BITS_ZERO4

⊢ ∀h l a. l ≤ h ⇒ BITS h l (a * 2 ** l) = BITS (h − l) 0 a

BITS_ZEROL

⊢ ∀h a. a < 2 ** SUC h ⇒ BITS h 0 a = a

BITS_LOG2_ZERO_ID

⊢ ∀n. 0 < n ⇒ BITS (LOG2 n) 0 n = n

BITS_LT_LOW

⊢ ∀h l n. n < 2 ** l ⇒ BITS h l n = 0

BIT_ZERO

⊢ ∀b. ¬BIT b 0

BIT_B

⊢ ∀b. BIT b (2 ** b)

BIT_TWO_POW

⊢ ∀n m. BIT n (2 ** m) ⇔ m = n

BIT_B_NEQ

⊢ ∀a b. a ≠ b ⇒ ¬BIT a (2 ** b)

BITS_COMP_THM2

⊢ ∀h1 l1 h2 l2 n.
      BITS h2 l2 (BITS h1 l1 n) = BITS (MIN h1 (h2 + l1)) (l2 + l1) n

NOT_MOD2_LEM

⊢ ∀n. n MOD 2 ≠ 0 ⇔ n MOD 2 = 1

NOT_MOD2_LEM2

⊢ ∀n. n MOD 2 ≠ 1 ⇔ n MOD 2 = 0

ODD_MOD2_LEM

⊢ ∀n. ODD n ⇔ n MOD 2 = 1

DIV_MULT_THM

⊢ ∀x n. n DIV 2 ** x * 2 ** x = n − n MOD 2 ** x

DIV_MULT_THM2

⊢ ∀n. 2 * (n DIV 2) = n − n MOD 2

LESS_EQ_EXP_MULT

⊢ ∀a b. a ≤ b ⇒ ∃p. 2 ** b = p * 2 ** a

SLICE_THM

⊢ ∀n h l. SLICE h l n = BITS h l n * 2 ** l

SLICELT_THM

⊢ ∀h l n. SLICE h l n < 2 ** SUC h

BITS_SLICE_THM

⊢ ∀h l n. BITS h l (SLICE h l n) = BITS h l n

BITS_SLICE_THM2

⊢ ∀h h2 l n. h ≤ h2 ⇒ BITS h2 l (SLICE h l n) = BITS h l n

SLICE_ZERO_THM

⊢ ∀n h. SLICE h 0 n = BITS h 0 n

MOD_2EXP_MONO

⊢ ∀n h l. l ≤ h ⇒ n MOD 2 ** l ≤ n MOD 2 ** SUC h

SLICE_COMP_THM

⊢ ∀h m l n. SUC m ≤ h ∧ l ≤ m ⇒ SLICE h (SUC m) n + SLICE m l n = SLICE h l n

SLICE_COMP_RWT

⊢ ∀h m' m l n.
      l ≤ m ∧ m' = m + 1 ∧ m < h ⇒ SLICE h m' n + SLICE m l n = SLICE h l n

SLICE_ZERO

⊢ ∀h l n. h < l ⇒ SLICE h l n = 0

SLICE_ZERO2

⊢ ∀l h. SLICE h l 0 = 0

BITS_SUM

⊢ ∀h l a b. b < 2 ** l ⇒ BITS h l (a * 2 ** l + b) = BITS h l (a * 2 ** l)

BITS_SUM2

⊢ ∀h l a b. BITS h l (a * 2 ** SUC h + b) = BITS h l b

SLICE_COMP_THM2

⊢ ∀h l x y n. h ≤ x ∧ y ≤ l ⇒ SLICE h l (SLICE x y n) = SLICE h l n

BITS_SUM3

⊢ ∀h a b. BITS h 0 (BITS h 0 a + BITS h 0 b) = BITS h 0 (a + b)

BITS_MUL

⊢ ∀h a b. BITS h 0 (BITS h 0 a * BITS h 0 b) = BITS h 0 (a * b)

BIT_COMP_THM3

⊢ ∀h m l n.
      SUC m ≤ h ∧ l ≤ m ⇒
      BITS h (SUC m) n * 2 ** (SUC m − l) + BITS m l n = BITS h l n

NOT_BIT

⊢ ∀n a. ¬BIT n a ⇔ BITS n n a = 0

NOT_BITS

⊢ ∀n a. BITS n n a ≠ 0 ⇔ BITS n n a = 1

NOT_BITS2

⊢ ∀n a. BITS n n a ≠ 1 ⇔ BITS n n a = 0

BIT_SLICE

⊢ ∀n a b. (BIT n a ⇔ BIT n b) ⇔ SLICE n n a = SLICE n n b

BIT_SLICE_LEM

⊢ ∀y x n. SBIT (BIT x n) (x + y) = SLICE x x n * 2 ** y

BIT_SLICE_THM

⊢ ∀x n. SBIT (BIT x n) x = SLICE x x n

BIT_SLICE_THM2

⊢ ∀b n. BIT b n ⇔ SLICE b b n = 2 ** b

BIT_SLICE_THM3

⊢ ∀b n. ¬BIT b n ⇔ SLICE b b n = 0

BIT_SLICE_THM4

⊢ ∀b h l n. BIT b (SLICE h l n) ⇔ l ≤ b ∧ b ≤ h ∧ BIT b n

SBIT_DIV

⊢ ∀b m n. n < m ⇒ SBIT b (m − n) = SBIT b m DIV 2 ** n

BITS_SUC

⊢ ∀h l n.
      l ≤ SUC h ⇒
      SBIT (BIT (SUC h) n) (SUC h − l) + BITS h l n = BITS (SUC h) l n

BITS_SUC_THM

⊢ ∀h l n.
      BITS (SUC h) l n = if SUC h < l then 0
      else SBIT (BIT (SUC h) n) (SUC h − l) + BITS h l n

BIT_BITS_THM

⊢ ∀h l a b.
      (∀x. l ≤ x ∧ x ≤ h ⇒ (BIT x a ⇔ BIT x b)) ⇔ BITS h l a = BITS h l b

BITS_ZERO5

⊢ ∀n m. (∀i. i ≤ n ⇒ ¬BIT i m) ⇒ BITS n 0 m = 0

BIT0_ODD

⊢ BIT 0 = ODD

BITV_THM

⊢ ∀b n. BITV n b = SBIT (BIT b n) 0

ADD_BIT0

⊢ ∀m n. BIT 0 (m + n) ⇔ (BIT 0 m ⇎ BIT 0 n)

ADD_BITS_SUC

⊢ ∀n a b.
      BITS (SUC n) (SUC n) (a + b) =
      (BITS (SUC n) (SUC n) a + BITS (SUC n) (SUC n) b +
       BITS (SUC n) (SUC n) (BITS n 0 a + BITS n 0 b)) MOD 2

ADD_BIT_SUC

⊢ ∀n a b.
      BIT (SUC n) (a + b) ⇔
      if BIT (SUC n) (BITS n 0 a + BITS n 0 b) then
        BIT (SUC n) a ⇔ BIT (SUC n) b else BIT (SUC n) a ⇎ BIT (SUC n) b

BITWISE_LT_2EXP

⊢ ∀n op a b. BITWISE n op a b < 2 ** n

BITWISE_THM

⊢ ∀x n op a b. x < n ⇒ (BIT x (BITWISE n op a b) ⇔ op (BIT x a) (BIT x b))

BITWISE_COR

⊢ ∀x n op a b.
      x < n ⇒ op (BIT x a) (BIT x b) ⇒ (BITWISE n op a b DIV 2 ** x) MOD 2 = 1

BITWISE_NOT_COR

⊢ ∀x n op a b.
      x < n ⇒
      ¬op (BIT x a) (BIT x b) ⇒
      (BITWISE n op a b DIV 2 ** x) MOD 2 = 0

BITWISE_BITS

⊢ ∀wl op a b.
      BITWISE (SUC wl) op (BITS wl 0 a) (BITS wl 0 b) =
      BITWISE (SUC wl) op a b

NOT_BIT_GT_TWOEXP

⊢ ∀i n. n < 2 ** i ⇒ ¬BIT i n

BIT_IMP_GE_TWOEXP

⊢ ∀i n. BIT i n ⇒ 2 ** i ≤ n

BITWISE_ONE_COMP_LEM

⊢ ∀n a b. BITWISE (SUC n) (λx y. ¬x) a b = 2 ** SUC n − 1 − BITS n 0 a

BIT_COMPLEMENT

⊢ ∀n i a.
      BIT i (2 ** n − a MOD 2 ** n) ⇔
      a MOD 2 ** n = 0 ∧ i = n ∨
      a MOD 2 ** n ≠ 0 ∧ i < n ∧ ¬BIT i (a MOD 2 ** n − 1)

BIT_OF_BITS_THM

⊢ ∀n h l a. l + n ≤ h ⇒ (BIT n (BITS h l a) ⇔ BIT (l + n) a)

BIT_SHIFT_THM

⊢ ∀n a s. BIT (n + s) (a * 2 ** s) ⇔ BIT n a

BIT_SHIFT_THM2

⊢ ∀n a s. s ≤ n ⇒ (BIT n (a * 2 ** s) ⇔ BIT (n − s) a)

BIT_SHIFT_THM3

⊢ ∀n a s. n < s ⇒ ¬BIT n (a * 2 ** s)

BIT_OF_BITS_THM2

⊢ ∀h l x n. h < l + x ⇒ ¬BIT x (BITS h l n)

BIT_DIV2

⊢ ∀n i. BIT n (i DIV 2) ⇔ BIT (SUC n) i

BIT_SHIFT_THM4

⊢ ∀n i a. BIT i (a DIV 2 ** n) ⇔ BIT (i + n) a

DIV_LT

⊢ ∀n m a. n < m ∧ a < 2 ** m ⇒ a DIV 2 ** n < 2 ** m

MOD_ZERO_GT

⊢ ∀n a. a ≠ 0 ∧ a MOD 2 ** n = 0 ⇒ 2 ** n ≤ a

DIV_GT0

⊢ ∀a b. b ≤ a ∧ 0 < b ⇒ 0 < a DIV b

DIV_SUB1

⊢ ∀a b. 2 ** b ≤ a ∧ a MOD 2 ** b = 0 ⇒ a DIV 2 ** b − 1 = (a − 1) DIV 2 ** b

BIT_EXP_SUB1

⊢ ∀b n. BIT b (2 ** n − 1) ⇔ b < n

BIT_SHIFT_THM5

⊢ ∀n m i a.
      i + n < m ∧ a < 2 ** m ⇒
      (BIT i
         (2 ** m −
          (a DIV 2 ** n + if a MOD 2 ** n = 0 then 0 else 1) MOD 2 ** m) ⇔
       BIT (i + n) (2 ** m − a MOD 2 ** m))

SBIT_MULT

⊢ ∀b m n. SBIT b n * 2 ** m = SBIT b (n + m)

BITWISE_EVAL

⊢ ∀n op a b.
      BITWISE (SUC n) op a b =
      2 * BITWISE n op (a DIV 2) (b DIV 2) + SBIT (op (ODD a) (ODD b)) 0

MOD_PLUS_RIGHT

⊢ ∀n. 0 < n ⇒ ∀j k. (j + k MOD n) MOD n = (j + k) MOD n

MOD_PLUS_LEFT

⊢ ∀n. 0 < n ⇒ ∀j k. (k MOD n + j) MOD n = (k + j) MOD n

MOD_PLUS_1

⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n = 0 ⇔ x MOD n + 1 = n

MOD_ADD_1

⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n ≠ 0 ⇒ (x + 1) MOD n = x MOD n + 1

BIT_REVERSE_THM

⊢ ∀x n a. x < n ⇒ (BIT x (BIT_REVERSE n a) ⇔ BIT (n − 1 − x) a)

LOG2_LE_MONO

⊢ ∀x y. 0 < x ⇒ x ≤ y ⇒ LOG2 x ≤ LOG2 y

TWOEXP_LE_IMP_LE_LOG2

⊢ (∀x y. 2 ** x ≤ y ⇒ x ≤ LOG2 y) ∧ ∀y x. 0 < x ⇒ x ≤ 2 ** y ⇒ LOG2 x ≤ y

NOT_BIT_GT_LOG2

⊢ ∀i n. LOG2 n < i ⇒ ¬BIT i n

NOT_BIT_GT_BITWISE

⊢ ∀i n op a b. n ≤ i ⇒ ¬BIT i (BITWISE n op a b)

LT_TWOEXP

⊢ ∀x n. x < 2 ** n ⇔ x = 0 ∨ LOG2 x < n

BIT_MODIFY_THM

⊢ ∀x n f a. x < n ⇒ (BIT x (BIT_MODIFY n f a) ⇔ f x (BIT x a))

BIT_SIGN_EXTEND

⊢ ∀l h n i.
      l ≠ 0 ⇒
      (BIT i (SIGN_EXTEND l h n) ⇔ if l ≤ h ⇒ i < l then BIT i (n MOD 2 ** l)
       else i < h ∧ BIT (l − 1) n)

BIT_LOG2

⊢ ∀n. n ≠ 0 ⇒ BIT (LOG2 n) n

EXISTS_BIT_IN_RANGE

⊢ ∀a b n. n ≠ 0 ∧ 2 ** a ≤ n ∧ n < 2 ** b ⇒ ∃i. a ≤ i ∧ i < b ∧ BIT i n

EXISTS_BIT_LT

⊢ ∀b n. n ≠ 0 ∧ n < 2 ** b ⇒ ∃i. i < b ∧ BIT i n

LEAST_THM

⊢ ∀n P. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ $LEAST P = n