Theory "bit"

Signature

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_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)