Theory "words"

Parents numeral_bit sum_num fcp

Signature

Constant	Type
word_xor	:'a word -> 'a word -> 'a word
word_sub	:'a word -> 'a word -> 'a word
word_slice	:num -> num -> 'a word -> 'a word
word_sdiv	:'a word -> 'a word -> 'a word
word_rrx	:bool # 'a word -> bool # 'a word
word_ror	:'a word -> num -> 'a word
word_rol	:'a word -> num -> 'a word
word_reverse	:'a word -> 'a word
word_or	:'a word -> 'a word -> 'a word
word_mul	:'a word -> 'a word -> 'a word
word_msb	:'a word -> bool
word_modify	:(num -> bool -> bool) -> 'a word -> 'a word
word_lt	:'a word -> 'a word -> bool
word_lsr	:'a word -> num -> 'a word
word_lsl	:'a word -> num -> 'a word
word_lsb	:'a word -> bool
word_ls	:'a word -> 'a word -> bool
word_log2	:'a word -> 'a word
word_lo	:'a word -> 'a word -> bool
word_len	:'a word -> num
word_le	:'a word -> 'a word -> bool
word_join	:'a word -> 'b word -> ('a + 'b) word
word_hs	:'a word -> 'a word -> bool
word_hi	:'a word -> 'a word -> bool
word_gt	:'a word -> 'a word -> bool
word_ge	:'a word -> 'a word -> bool
word_extract_itself	:'a itself -> num -> num -> 'b word -> 'a word
word_extract	:num -> num -> 'a word -> 'b word
word_eq	:'a word -> 'a word -> bool
word_div	:'a word -> 'a word -> 'a word
word_concat_itself	:'a itself -> 'b word -> 'c word -> 'a word
word_concat	:'a word -> 'b word -> 'c word
word_bits	:num -> num -> 'a word -> 'a word
word_bit	:num -> 'a word -> bool
word_asr	:'a word -> num -> 'a word
word_and	:'a word -> 'a word -> 'a word
word_add	:'a word -> 'a word -> 'a word
word_T	:'a word
word_L	:'a word
word_H	:'a word
word_2comp	:'a word -> 'a word
word_1comp	:'a word -> 'a word
w2w_itself	:'a itself -> 'b word -> 'a word
w2w	:'a word -> 'b word
w2n	:'a word -> num
sw2sw_itself	:'a itself -> 'b word -> 'a word
sw2sw	:'a word -> 'b word
nzcv	:'a word -> 'a word -> i16
n2w_itself	:num # 'a itself -> 'a word
n2w	:num -> 'a word
fromNum	:num # 'a itself -> 'a word
dimword	:'a itself -> num
UINT_MAX	:'a itself -> num
INT_MIN	:'a itself -> num
INT_MAX	:'a itself -> num

Definitions

dimword_def

|- dimword (:'a) = 2 ** dimindex (:'a)

INT_MIN_def

|- INT_MIN (:'a) = 2 ** (dimindex (:'a) - 1)

UINT_MAX_def

|- UINT_MAX (:'a) = dimword (:'a) - 1

INT_MAX_def

|- INT_MAX (:'a) = INT_MIN (:'a) - 1

w2n_def

|- !w. w2n w = SUM (dimindex (:'a)) (\i. SBIT (w %% i) i)

n2w_def

|- !n. n2w n = FCP i. BIT i n

w2w_def

|- !w. w2w w = n2w (w2n w)

sw2sw_def

|- !w. sw2sw w = n2w (SIGN_EXTEND (dimindex (:'a)) (dimindex (:'b)) (w2n w))

word_T_def

|- UINT_MAXw = n2w (UINT_MAX (:'a))

word_L_def

|- INT_MINw = n2w (INT_MIN (:'a))

word_H_def

|- INT_MAXw = n2w (INT_MAX (:'a))

word_1comp_def

|- !w. ~w = FCP i. ~(w %% i)

word_and_def

|- !v w. v && w = FCP i. v %% i /\ w %% i

word_or_def

|- !v w. v !! w = FCP i. v %% i \/ w %% i

word_xor_def

|- !v w. v ?? w = FCP i. ~(v %% i = w %% i)

word_lsb_def

|- !w. word_lsb w = w %% 0

word_msb_def

|- !w. word_msb w = w %% (dimindex (:'a) - 1)

word_slice_def

|- !h l.
     h <> l = (\w. FCP i. l <= i /\ i <= MIN h (dimindex (:'a) - 1) /\ w %% i)

word_bits_def

|- !h l.
     h -- l = (\w. FCP i. i + l <= MIN h (dimindex (:'a) - 1) /\ w %% (i + l))

word_extract_def

|- !h l. h >< l = w2w o (h -- l)

word_bit_def

|- !b w. word_bit b w = b <= dimindex (:'a) - 1 /\ w %% b

word_reverse_def

|- !w. word_reverse w = FCP i. w %% (dimindex (:'a) - 1 - i)

word_modify_def

|- !f w. word_modify f w = FCP i. f i (w %% i)

word_len_def

|- !w. word_len w = dimindex (:'a)

word_2comp_def

|- !w. $- w = n2w (dimword (:'a) - w2n w)

word_add_def

|- !v w. v + w = n2w (w2n v + w2n w)

word_mul_def

|- !v w. v * w = n2w (w2n v * w2n w)

word_log2_def

|- !w. word_log2 w = n2w (LOG2 (w2n w))

word_sub_def

|- !v w. v - w = v + $- w

word_div_def

|- !v w. v // w = n2w (w2n v DIV w2n w)

word_sdiv_def

|- !a b.
     a / b =
     (if word_msb a then
        (if word_msb b then $- a // $- b else $- ($- a // b))
      else
        (if word_msb b then $- (a // $- b) else a // b))

word_lsl_def

|- !w n. w << n = FCP i. i < dimindex (:'a) /\ n <= i /\ w %% (i - n)

word_lsr_def

|- !w n. w >>> n = FCP i. i + n < dimindex (:'a) /\ w %% (i + n)

word_asr_def

|- !w n.
     w >> n =
     FCP i. (if dimindex (:'a) <= i + n then word_msb w else w %% (i + n))

word_ror_def

|- !w n. w #>> n = FCP i. w %% (i + n) MOD dimindex (:'a)

word_rol_def

|- !w n. w #<< n = w #>> (dimindex (:'a) - n MOD dimindex (:'a))

word_rrx_def

|- !c w.
     word_rrx (c,w) =
     (word_lsb w,FCP i. (if i = dimindex (:'a) - 1 then c else w >>> 1 %% i))

word_join_def

|- !v w.
     word_join v w =
     (let cv = w2w v and cw = w2w w in cv << dimindex (:'b) !! cw)

word_concat_def

|- !v w. v @@ w = w2w (word_join v w)

nzcv_def

|- !a b.
     nzcv a b =
     (let q = w2n a + w2n ($- b) in
      let r = n2w q in
        (word_msb r,r = 0w,BIT (dimindex (:'a)) q \/ (b = 0w),
          ~(word_msb a = word_msb b) /\ ~(word_msb r = word_msb a)))

word_lt_def

|- !a b. a < b = (let (n,z,c,v) = nzcv a b in ~(n = v))

word_gt_def

|- !a b. a > b = (let (n,z,c,v) = nzcv a b in ~z /\ (n = v))

word_le_def

|- !a b. a <= b = (let (n,z,c,v) = nzcv a b in z \/ ~(n = v))

word_ge_def

|- !a b. a >= b = (let (n,z,c,v) = nzcv a b in n = v)

word_ls_def

|- !a b. a <=+ b = (let (n,z,c,v) = nzcv a b in ~c \/ z)

word_hi_def

|- !a b. a >+ b = (let (n,z,c,v) = nzcv a b in c /\ ~z)

word_lo_def

|- !a b. a <+ b = (let (n,z,c,v) = nzcv a b in ~c)

word_hs_def

|- !a b. a >=+ b = (let (n,z,c,v) = nzcv a b in c)

n2w_itself_primitive_def

|- n2w_itself =
   WFREC (@R. WF R) (\n2w_itself a. case a of (n,(:'a)) -> I (n2w n))

w2w_itself_def

|- !w. w2w_itself (:'a) w = w2w w

sw2sw_itself_def

|- !w. sw2sw_itself (:'a) w = sw2sw w

word_eq_def

|- !v w. word_eq v w = (v = w)

word_extract_itself_def

|- !h l w. word_extract_itself (:'a) h l w = (h >< l) w

word_concat_itself_def

|- !v w. word_concat_itself (:'a) v w = v @@ w

fromNum_primitive_def

|- fromNum =
   WFREC (@R. WF R)
     (\fromNum a.
        case a of (n,(:'a)) -> I (n2w_itself (n MOD dimword (:'a),(:'a))))

Theorems

ZERO_LT_dimword

|- 0 < dimword (:'a)

dimword_IS_TWICE_INT_MIN

|- dimword (:'a) = 2 * INT_MIN (:'a)

DIMINDEX_GT_0

|- 0 < dimindex (:'a)

ONE_LT_dimword

|- 1 < dimword (:'a)

EXISTS_HB

|- ?m. dimindex (:'a) = SUC m

MOD_DIMINDEX

|- !n. n MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 n

MOD_2EXP_DIMINDEX

|- !n. n MOD dimword (:'a) = MOD_2EXP (dimindex (:'a)) n

INT_MIN_SUM

|- INT_MIN (:'a + 'b) =
   (if FINITE UNIV /\ FINITE UNIV then
      dimword (:'a) * INT_MIN (:'b)
    else
      INT_MIN (:'a + 'b))

w2n_n2w

|- !n. w2n (n2w n) = n MOD dimword (:'a)

n2w_w2n

|- !w. n2w (w2n w) = w

word_nchotomy

|- !w. ?n. w = n2w n

n2w_mod

|- !n. n2w (n MOD dimword (:'a)) = n2w n

n2w_11

|- !m n. (n2w m = n2w n) = (m MOD dimword (:'a) = n MOD dimword (:'a))

ranged_word_nchotomy

|- !w. ?n. (w = n2w n) /\ n < dimword (:'a)

w2n_11

|- !v w. (w2n v = w2n w) = (v = w)

w2n_lt

|- !w. w2n w < dimword (:'a)

word_0_n2w

|- w2n 0w = 0

word_1_n2w

|- w2n 1w = 1

w2n_eq_0

|- (w2n w = 0) = (w = 0w)

word_add_n2w

|- !m n. n2w m + n2w n = n2w (m + n)

word_mul_n2w

|- !m n. n2w m * n2w n = n2w (m * n)

word_log2_n2w

|- !n. word_log2 (n2w n) = n2w (LOG2 (n MOD dimword (:'a)))

word_1comp_n2w

|- !n. ~n2w n = n2w (dimword (:'a) - 1 - n MOD dimword (:'a))

word_2comp_n2w

|- !n. $- (n2w n) = n2w (dimword (:'a) - n MOD dimword (:'a))

word_lsb_n2w

|- !n. word_lsb (n2w n) = BIT 0 n

word_msb_n2w

|- !n. word_msb (n2w n) = BIT (dimindex (:'a) - 1) n

word_msb_n2w_numeric

|- word_msb (n2w n) = INT_MIN (:'a) <= n MOD dimword (:'a)

word_and_n2w

|- !n m. n2w n && n2w m = n2w (BITWISE (dimindex (:'a)) $/\ n m)

word_or_n2w

|- !n m. n2w n !! n2w m = n2w (BITWISE (dimindex (:'a)) $\/ n m)

word_xor_n2w

|- !n m. n2w n ?? n2w m = n2w (BITWISE (dimindex (:'a)) (\x y. ~(x = y)) n m)

word_0

|- !i. i < dimindex (:'a) ==> ~(0w %% i)

word_T

|- !i. i < dimindex (:'a) ==> UINT_MAXw %% i

WORD_NOT_NOT

|- !a. ~ ~a = a

WORD_DE_MORGAN_THM

|- !a b. ~(a && b) = ~a !! ~b

WORD_AND_CLAUSES

|- !a.
     (UINT_MAXw && a = a) /\ (a && UINT_MAXw = a) /\ (0w && a = 0w) /\
     (a && 0w = 0w) /\ (a && a = a)

WORD_OR_CLAUSES

|- !a.
     (UINT_MAXw !! a = UINT_MAXw) /\ (a !! UINT_MAXw = UINT_MAXw) /\
     (0w !! a = a) /\ (a !! 0w = a) /\ (a !! a = a)

WORD_XOR_CLAUSES

|- !a.
     (UINT_MAXw ?? a = ~a) /\ (a ?? UINT_MAXw = ~a) /\ (0w ?? a = a) /\
     (a ?? 0w = a) /\ (a ?? a = 0w)

WORD_AND_ASSOC

|- !a b c. (a && b) && c = a && b && c

WORD_OR_ASSOC

|- !a b c. (a !! b) !! c = a !! b !! c

WORD_XOR_ASSOC

|- !a b c. (a ?? b) ?? c = a ?? b ?? c

WORD_AND_COMM

|- !a b. a && b = b && a

WORD_OR_COMM

|- !a b. a !! b = b !! a

WORD_XOR_COMM

|- !a b. a ?? b = b ?? a

WORD_AND_IDEM

|- !a. a && a = a

WORD_OR_IDEM

|- !a. a !! a = a

WORD_AND_ABSORD

|- !a b. a !! a && b = a

WORD_OR_ABSORB

|- !a b. a && (a !! b) = a

WORD_AND_COMP

|- !a. a && ~a = 0w

WORD_OR_COMP

|- !a. a !! ~a = UINT_MAXw

WORD_XOR_COMP

|- !a. a ?? ~a = UINT_MAXw

WORD_RIGHT_AND_OVER_OR

|- !a b c. (a !! b) && c = a && c !! b && c

WORD_RIGHT_OR_OVER_AND

|- !a b c. a && b !! c = (a !! c) && (b !! c)

WORD_XOR

|- !a b. a ?? b = a && ~b !! b && ~a

w2w

|- !w i. i < dimindex (:'b) ==> (w2w w %% i = i < dimindex (:'a) /\ w %% i)

w2w_id

|- !w. w2w w = w

w2w_w2w

|- !w. w2w (w2w w) = w2w ((dimindex (:'b) - 1 -- 0) w)

word_bit

|- !w b. b < dimindex (:'a) ==> (w %% b = word_bit b w)

word_slice_n2w

|- !h l n. (h <> l) (n2w n) = n2w (SLICE (MIN h (dimindex (:'a) - 1)) l n)

word_bits_n2w

|- !h l n. (h -- l) (n2w n) = n2w (BITS (MIN h (dimindex (:'a) - 1)) l n)

word_bit_n2w

|- !b n. word_bit b (n2w n) = b <= dimindex (:'a) - 1 /\ BIT b n

word_index_n2w

|- !n. n2w n %% i = (if i < dimindex (:'a) then BIT i n else n2w n %% i)

word_bits_w2w

|- !w. (h -- l) (w2w w) = w2w ((MIN h (dimindex (:'b) - 1) -- l) w)

word_reverse_n2w

|- !n. word_reverse (n2w n) = n2w (BIT_REVERSE (dimindex (:'a)) n)

word_modify_n2w

|- !f n. word_modify f (n2w n) = n2w (BIT_MODIFY (dimindex (:'a)) f n)

fcp_n2w

|- !f. $FCP f = word_modify (\i b. f i) 0w

w2n_w2w

|- !w.
     w2n (w2w w) =
     (if dimindex (:'a) <= dimindex (:'b) then
        w2n w
      else
        w2n ((dimindex (:'b) - 1 -- 0) w))

w2w_n2w

|- !n.
     w2w (n2w n) =
     (if dimindex (:'b) <= dimindex (:'a) then
        n2w n
      else
        n2w (BITS (dimindex (:'a) - 1) 0 n))

WORD_EQ

|- !v w. (!x. x < dimindex (:'a) ==> (word_bit x v = word_bit x w)) = (v = w)

WORD_BIT_BITS

|- !b w. word_bit b w = ((b -- b) w = 1w)

WORD_BITS_COMP_THM

|- !h1 l1 h2 l2 w. (h2 -- l2) ((h1 -- l1) w) = (MIN h1 (h2 + l1) -- l2 + l1) w

WORD_BITS_LSR

|- !h l w. (h -- l) w >>> n = (h -- l + n) w

WORD_BITS_ZERO

|- !h l w. h < l ==> ((h -- l) w = 0w)

WORD_BITS_LT

|- !h l w. w2n ((h -- l) w) < 2 ** (SUC h - l)

WORD_SLICE_THM

|- !h l w. (h <> l) w = (h -- l) w << l

WORD_SLICE_ZERO

|- !h l w. h < l ==> ((h <> l) w = 0w)

WORD_SLICE_BITS_THM

|- !h w. (h <> 0) w = (h -- 0) w

WORD_BITS_SLICE_THM

|- !h l w. (h -- l) ((h <> l) w) = (h -- l) w

WORD_SLICE_COMP_THM

|- !h m' m l w.
     l <= m /\ (m' = m + 1) /\ m < h ==>
     ((h <> m') w !! (m <> l) w = (h <> l) w)

WORD_EXTRACT_BITS_COMP

|- (j >< k) ((h -- l) n) = (MIN h (j + l) >< k + l) n

WORD_ALL_BITS

|- !w. (h = dimindex (:'a) - 1) ==> ((h -- 0) w = w)

WORD_FULL_EXTRACT

|- !w. (h = dimindex (:'a) - 1) ==> ((h >< 0) w = w)

CONCAT_EXTRACT

|- !h m l w.
     (h - m = dimindex (:'b)) /\ (m + 1 - l = dimindex (:'c)) /\
     (h + 1 - l = dimindex (:'d)) /\ ~(dimindex (:'b + 'c) = 1) ==>
     ((h >< m + 1) w @@ (m >< l) w = (h >< l) w)

WORD_SLICE_OVER_BITWISE

|- (!h l v w. (h <> l) v && (h <> l) w = (h <> l) (v && w)) /\
   (!h l v w. (h <> l) v !! (h <> l) w = (h <> l) (v !! w)) /\
   !h l v w. (h <> l) v ?? (h <> l) w = (h <> l) (v ?? w)

WORD_BITS_OVER_BITWISE

|- (!h l v w. (h -- l) v && (h -- l) w = (h -- l) (v && w)) /\
   (!h l v w. (h -- l) v !! (h -- l) w = (h -- l) (v !! w)) /\
   !h l v w. (h -- l) v ?? (h -- l) w = (h -- l) (v ?? w)

WORD_ADD_0

|- (!w. w + 0w = w) /\ !w. 0w + w = w

WORD_ADD_ASSOC

|- !v w x. v + (w + x) = v + w + x

WORD_MULT_ASSOC

|- !v w x. v * (w * x) = v * w * x

WORD_ADD_COMM

|- !v w. v + w = w + v

WORD_MULT_COMM

|- !v w. v * w = w * v

WORD_MULT_CLAUSES

|- !v w.
     (0w * v = 0w) /\ (v * 0w = 0w) /\ (1w * v = v) /\ (v * 1w = v) /\
     ((v + 1w) * w = v * w + w) /\ (v * (w + 1w) = v + v * w)

WORD_LEFT_ADD_DISTRIB

|- !v w x. v * (w + x) = v * w + v * x

WORD_RIGHT_ADD_DISTRIB

|- !v w x. (v + w) * x = v * x + w * x

WORD_ADD_SUB_ASSOC

|- !v w x. v + w - x = v + (w - x)

WORD_ADD_SUB_SYM

|- !v w x. v + w - x = v - x + w

WORD_ADD_LINV

|- !w. $- w + w = 0w

WORD_ADD_RINV

|- !w. w + $- w = 0w

WORD_SUB_REFL

|- !w. w - w = 0w

WORD_SUB_ADD2

|- !v w. v + (w - v) = w

WORD_ADD_SUB

|- !v w. v + w - w = v

WORD_SUB_ADD

|- !v w. v - w + w = v

WORD_ADD_EQ_SUB

|- !v w x. (v + w = x) = (v = x - w)

WORD_ADD_INV_0_EQ

|- !v w. (v + w = v) = (w = 0w)

WORD_EQ_ADD_LCANCEL

|- !v w x. (v + w = v + x) = (w = x)

WORD_EQ_ADD_RCANCEL

|- !v w x. (v + w = x + w) = (v = x)

WORD_NEG

|- !w. $- w = ~w + 1w

WORD_NOT

|- !w. ~w = $- w - 1w

WORD_NEG_0

|- $- 0w = 0w

WORD_NEG_ADD

|- !v w. $- (v + w) = $- v + $- w

WORD_NEG_NEG

|- !w. $- ($- w) = w

WORD_SUB_LNEG

|- !v w. $- v - w = $- (v + w)

WORD_SUB_RNEG

|- !v w. v - $- w = v + w

WORD_SUB_SUB

|- !v w x. v - (w - x) = v + x - w

WORD_SUB_SUB2

|- !v w. v - (v - w) = w

WORD_EQ_SUB_LADD

|- !v w x. (v = w - x) = (v + x = w)

WORD_EQ_SUB_RADD

|- !v w x. (v - w = x) = (v = x + w)

WORD_EQ_SUB_ZERO

|- !w v. (v - w = 0w) = (v = w)

WORD_LCANCEL_SUB

|- !v w x. (v - w = x - w) = (v = x)

WORD_RCANCEL_SUB

|- !v w x. (v - w = v - x) = (w = x)

WORD_SUB_PLUS

|- !v w x. v - (w + x) = v - w - x

WORD_SUB_LZERO

|- !w. 0w - w = $- w

WORD_SUB_RZERO

|- !w. w - 0w = w

WORD_ADD_LID_UNIQ

|- !v w. (v + w = w) = (v = 0w)

WORD_ADD_RID_UNIQ

|- !v w. (v + w = v) = (w = 0w)

WORD_ADD_SUB2

|- !v w. w + v - w = v

WORD_ADD_SUB3

|- !v x. v - (v + x) = $- x

WORD_SUB_SUB3

|- v - w - v = $- w

WORD_EQ_NEG

|- !v w. ($- v = $- w) = (v = w)

WORD_NEG_EQ

|- ($- v = w) = (v = $- w)

WORD_NEG_EQ_0

|- ($- v = 0w) = (v = 0w)

WORD_SUB

|- !v w. $- w + v = v - w

WORD_SUB_NEG

|- !v w. $- v - $- w = w - v

WORD_NEG_SUB

|- $- (v - w) = w - v

WORD_SUB_TRIANGLE

|- !v w x. v - w + (w - x) = v - x

WORD_NEG_1

|- $- 1w = UINT_MAXw

WORD_NOT_0

|- ~0w = UINT_MAXw

WORD_NOT_T

|- ~UINT_MAXw = 0w

WORD_NEG_T

|- $- UINT_MAXw = 1w

WORD_MULT_SUC

|- !v n. v * n2w (n + 1) = v * n2w n + v

WORD_NEG_LMUL

|- !v w. $- (v * w) = $- v * w

WORD_NEG_RMUL

|- !v w. $- (v * w) = v * $- w

WORD_LEFT_SUB_DISTRIB

|- !v w x. v * (w - x) = v * w - v * x

WORD_RIGHT_SUB_DISTRIB

|- !v w x. (w - x) * v = w * v - x * v

ASR_ADD

|- !w m n. w >> m >> n = w >> (m + n)

LSR_ADD

|- !w m n. w >>> m >>> n = w >>> (m + n)

ROR_ADD

|- !w m n. w #>> m #>> n = w #>> (m + n)

LSL_ADD

|- !w m n. w << m << n = w << (m + n)

ASR_LIMIT

|- !w n.
     dimindex (:'a) < n ==> (w >> n = (if word_msb w then UINT_MAXw else 0w))

ASR_UINT_MAX

|- !w n. UINT_MAXw >> n = UINT_MAXw

LSR_LIMIT

|- !w n. dimindex (:'a) < n ==> (w >>> n = 0w)

LSL_LIMIT

|- !w n. dimindex (:'a) <= n ==> (w << n = 0w)

ROR_CYCLE

|- !w n. w #>> (n * dimindex (:'a)) = w

ROR_MOD

|- !w n. w #>> (n MOD dimindex (:'a)) = w #>> n

LSL_ONE

|- !w. w << 1 = w + w

ROR_UINT_MAX

|- !n. UINT_MAXw #>> n = UINT_MAXw

ROR_ROL

|- !w n. (w #>> n #<< n = w) /\ (w #<< n #>> n = w)

ZERO_SHIFT

|- (!n. 0w << n = 0w) /\ (!n. 0w >> n = 0w) /\ (!n. 0w >>> n = 0w) /\
   !n. 0w #>> n = 0w

SHIFT_ZERO

|- (!a. a << 0 = a) /\ (!a. a >> 0 = a) /\ (!a. a >>> 0 = a) /\
   !a. a #>> 0 = a

LSR_BITWISE

|- (!n v w. w >>> n && v >>> n = (w && v) >>> n) /\
   (!n v w. w >>> n !! v >>> n = (w !! v) >>> n) /\
   !n v w. w >>> n ?? v >>> n = (w ?? v) >>> n

LSL_BITWISE

|- (!n v w. w << n && v << n = (w && v) << n) /\
   (!n v w. w << n !! v << n = (w !! v) << n) /\
   !n v w. w << n ?? v << n = (w ?? v) << n

ROR_BITWISE

|- (!n v w. w #>> n && v #>> n = (w && v) #>> n) /\
   (!n v w. w #>> n !! v #>> n = (w !! v) #>> n) /\
   !n v w. w #>> n ?? v #>> n = (w ?? v) #>> n

word_lsl_n2w

|- !n m.
     n2w m << n = (if dimindex (:'a) - 1 < n then 0w else n2w (m * 2 ** n))

word_lsr_n2w

|- !w n. w >>> n = (dimindex (:'a) - 1 -- n) w

LSL_UINT_MAX

|- !n. UINT_MAXw << n = n2w (dimword (:'a) - 2 ** n)

word_asr_n2w

|- !n w.
     w >> n =
     (if word_msb w then
        n2w
          (dimword (:'a) - 2 ** (dimindex (:'a) - MIN n (dimindex (:'a)))) !!
        w >>> n
      else
        w >>> n)

word_ror_n2w

|- !n a.
     n2w a #>> n =
     (let x = n MOD dimindex (:'a) in
        n2w
          (BITS (dimindex (:'a) - 1) x a +
           BITS (x - 1) 0 a * 2 ** (dimindex (:'a) - x)))

word_rrx_n2w

|- !c a.
     word_rrx (c,n2w a) =
     (ODD a,n2w (BITS (dimindex (:'a) - 1) 1 a + SBIT c (dimindex (:'a) - 1)))

WORD_NEG_L

|- $- INT_MINw = INT_MINw

TWO_COMP_POS

|- !a. ~word_msb a ==> (if a = 0w then ~word_msb ($- a) else word_msb ($- a))

TWO_COMP_NEG

|- !a.
     word_msb a ==>
     (if (dimindex (:'a) - 1 = 0) \/ (a = INT_MINw) then
        word_msb ($- a)
      else
        ~word_msb ($- a))

TWO_COMP_POS_NEG

|- !a.
     ~((dimindex (:'a) - 1 = 0) \/ (a = 0w) \/ (a = INT_MINw)) ==>
     (~word_msb a = word_msb ($- a))

WORD_0_POS

|- ~word_msb 0w

WORD_H_POS

|- ~word_msb INT_MAXw

WORD_L_NEG

|- word_msb INT_MINw

WORD_GREATER

|- !a b. a > b = b < a

WORD_GREATER_EQ

|- !a b. a >= b = b <= a

WORD_NOT_LESS

|- !a b. ~(a < b) = b <= a

WORD_LT

|- !a b.
     a < b =
     (word_msb a = word_msb b) /\ w2n a < w2n b \/ word_msb a /\ ~word_msb b

WORD_GT

|- !a b.
     a > b =
     (word_msb b = word_msb a) /\ w2n a > w2n b \/ word_msb b /\ ~word_msb a

WORD_LE

|- !a b.
     a <= b =
     (word_msb a = word_msb b) /\ w2n a <= w2n b \/ word_msb a /\ ~word_msb b

WORD_GE

|- !a b.
     a >= b =
     (word_msb b = word_msb a) /\ w2n a >= w2n b \/ word_msb b /\ ~word_msb a

WORD_LO

|- !a b. a <+ b = w2n a < w2n b

WORD_LS

|- !a b. a <=+ b = w2n a <= w2n b

WORD_HI

|- !a b. a >+ b = w2n a > w2n b

WORD_HS

|- !a b. a >=+ b = w2n a >= w2n b

WORD_NOT_LESS_EQUAL

|- !a b. ~(a <= b) = b < a

WORD_LESS_OR_EQ

|- !a b. a <= b = a < b \/ (a = b)

WORD_GREATER_OR_EQ

|- !a b. a >= b = a > b \/ (a = b)

WORD_LESS_TRANS

|- !a b c. a < b /\ b < c ==> a < c

WORD_LESS_EQ_TRANS

|- !a b c. a <= b /\ b <= c ==> a <= c

WORD_LESS_EQ_LESS_TRANS

|- !a b c. a <= b /\ b < c ==> a < c

WORD_LESS_LESS_EQ_TRANS

|- !a b c. a < b /\ b <= c ==> a < c

WORD_LESS_EQ_CASES

|- !a b. a <= b \/ b <= a

WORD_LESS_CASES

|- !a b. a < b \/ b <= a

WORD_LESS_CASES_IMP

|- !a b. ~(a < b) /\ ~(a = b) ==> b < a

WORD_LESS_ANTISYM

|- !a b. ~(a < b /\ b < a)

WORD_LESS_EQ_ANTISYM

|- !a b. ~(a < b /\ b <= a)

WORD_LESS_EQ_REFL

|- !a. a <= a

WORD_LESS_EQUAL_ANTISYM

|- !a b. a <= b /\ b <= a ==> (a = b)

WORD_LESS_IMP_LESS_OR_EQ

|- !a b. a < b ==> a <= b

WORD_LESS_REFL

|- !a. ~(a < a)

WORD_LESS_LESS_CASES

|- !a b. (a = b) \/ a < b \/ b < a

WORD_NOT_GREATER

|- !a b. ~(a > b) = a <= b

WORD_LESS_NOT_EQ

|- !a b. a < b ==> ~(a = b)

WORD_NOT_LESS_EQ

|- !a b. (a = b) ==> ~(a < b)

WORD_HIGHER

|- !a b. a >+ b = b <+ a

WORD_HIGHER_EQ

|- !a b. a >=+ b = b <=+ a

WORD_NOT_LOWER

|- !a b. ~(a <+ b) = b <=+ a

WORD_NOT_LOWER_EQUAL

|- !a b. ~(a <=+ b) = b <+ a

WORD_LOWER_OR_EQ

|- !a b. a <=+ b = a <+ b \/ (a = b)

WORD_HIGHER_OR_EQ

|- !a b. a >=+ b = a >+ b \/ (a = b)

WORD_LOWER_TRANS

|- !a b c. a <+ b /\ b <+ c ==> a <+ c

WORD_LOWER_EQ_TRANS

|- !a b c. a <=+ b /\ b <=+ c ==> a <=+ c

WORD_LOWER_EQ_LOWER_TRANS

|- !a b c. a <=+ b /\ b <+ c ==> a <+ c

WORD_LOWER_LOWER_EQ_TRANS

|- !a b c. a <+ b /\ b <=+ c ==> a <+ c

WORD_LOWER_EQ_CASES

|- !a b. a <=+ b \/ b <=+ a

WORD_LOWER_CASES

|- !a b. a <+ b \/ b <=+ a

WORD_LOWER_CASES_IMP

|- !a b. ~(a <+ b) /\ ~(a = b) ==> b <+ a

WORD_LOWER_ANTISYM

|- !a b. ~(a <+ b /\ b <+ a)

WORD_LOWER_EQ_ANTISYM

|- !a b. ~(a <+ b /\ b <=+ a)

WORD_LOWER_EQ_REFL

|- !a. a <=+ a

WORD_LOWER_EQUAL_ANTISYM

|- !a b. a <=+ b /\ b <=+ a ==> (a = b)

WORD_LOWER_IMP_LOWER_OR_EQ

|- !a b. a <+ b ==> a <=+ b

WORD_LOWER_REFL

|- !a. ~(a <+ a)

WORD_LOWER_LOWER_CASES

|- !a b. (a = b) \/ a <+ b \/ b <+ a

WORD_NOT_HIGHER

|- !a b. ~(a >+ b) = a <=+ b

WORD_LOWER_NOT_EQ

|- !a b. a <+ b ==> ~(a = b)

WORD_NOT_LOWER_EQ

|- !a b. (a = b) ==> ~(a <+ b)

WORD_L_PLUS_H

|- INT_MINw + INT_MAXw = UINT_MAXw

WORD_L_LESS_EQ

|- !a. INT_MINw <= a

WORD_LESS_EQ_H

|- !a. a <= INT_MAXw

WORD_L_LESS_H

|- INT_MINw < INT_MAXw

word_lt_n2w

|- !a b.
     n2w a < n2w b =
     (let sa = BIT (dimindex (:'a) - 1) a and sb = BIT (dimindex (:'a) - 1) b
      in
        (sa = sb) /\ a MOD dimword (:'a) < b MOD dimword (:'a) \/ sa /\ ~sb)

word_gt_n2w

|- !a b.
     n2w a > n2w b =
     (let sa = BIT (dimindex (:'a) - 1) a and sb = BIT (dimindex (:'a) - 1) b
      in
        (sa = sb) /\ a MOD dimword (:'a) > b MOD dimword (:'a) \/ ~sa /\ sb)

word_le_n2w

|- !a b.
     n2w a <= n2w b =
     (let sa = BIT (dimindex (:'a) - 1) a and sb = BIT (dimindex (:'a) - 1) b
      in
        (sa = sb) /\ a MOD dimword (:'a) <= b MOD dimword (:'a) \/ sa /\ ~sb)

word_ge_n2w

|- !a b.
     n2w a >= n2w b =
     (let sa = BIT (dimindex (:'a) - 1) a and sb = BIT (dimindex (:'a) - 1) b
      in
        (sa = sb) /\ a MOD dimword (:'a) >= b MOD dimword (:'a) \/ ~sa /\ sb)

word_ls_n2w

|- !a b. n2w a <=+ n2w b = a MOD dimword (:'a) <= b MOD dimword (:'a)

word_hi_n2w

|- !a b. n2w a >+ n2w b = a MOD dimword (:'a) > b MOD dimword (:'a)

word_lo_n2w

|- !a b. n2w a <+ n2w b = a MOD dimword (:'a) < b MOD dimword (:'a)

word_hs_n2w

|- !a b. n2w a >=+ n2w b = a MOD dimword (:'a) >= b MOD dimword (:'a)

SUC_WORD_PRED

|- !x. ~(x = 0w) ==> (SUC (w2n (x - 1w)) = w2n x)

WORD_PRED_THM

|- !m. ~(m = 0w) ==> w2n (m - 1w) < w2n m

word_sub_w2n

|- !x y. y <=+ x ==> (w2n (x - y) = w2n x - w2n y)

WORD_LE_EQ_LS

|- !x y. 0w <= x /\ 0w <= y ==> (x <= y = x <=+ y)

WORD_LT_EQ_LO

|- !x y. 0w <= x /\ 0w <= y ==> (x < y = x <+ y)

WORD_ZERO_LE

|- !w. 0w <= w = w2n w < INT_MIN (:'a)

WORD_SUB_LT

|- !x y. 0w < y /\ y < x ==> 0w < x - y /\ x - y < x

WORD_SUB_LE

|- !x y. 0w <= y /\ y <= x ==> 0w <= x - y /\ x - y <= x

dimindex_2

|- dimindex (:bool) = 2

finite_2

|- FINITE UNIV

size2

|- CARD UNIV = 2

INT_MIN_2

|- INT_MIN (:bool) = 2

dimword_2

|- dimword (:bool) = 4

dimindex_3

|- dimindex (:bool option) = 3

finite_3

|- FINITE UNIV

size3

|- CARD UNIV = 3

INT_MIN_3

|- INT_MIN (:bool option) = 4

dimword_3

|- dimword (:bool option) = 8

dimindex_4

|- dimindex (:bool # bool) = 4

finite_4

|- FINITE UNIV

size4

|- CARD UNIV = 4

INT_MIN_4

|- INT_MIN (:bool # bool) = 8

dimword_4

|- dimword (:bool # bool) = 16

dimindex_5

|- dimindex (:(bool # bool) option) = 5

finite_5

|- FINITE UNIV

size5

|- CARD UNIV = 5

INT_MIN_5

|- INT_MIN (:(bool # bool) option) = 16

dimword_5

|- dimword (:(bool # bool) option) = 32

dimindex_6

|- dimindex (:bool # bool option) = 6

finite_6

|- FINITE UNIV

size6

|- CARD UNIV = 6

INT_MIN_6

|- INT_MIN (:bool # bool option) = 32

dimword_6

|- dimword (:bool # bool option) = 64

dimindex_7

|- dimindex (:(bool # bool option) option) = 7

finite_7

|- FINITE UNIV

size7

|- CARD UNIV = 7

INT_MIN_7

|- INT_MIN (:(bool # bool option) option) = 64

dimword_7

|- dimword (:(bool # bool option) option) = 128

dimindex_8

|- dimindex (:bool # bool # bool) = 8

finite_8

|- FINITE UNIV

size8

|- CARD UNIV = 8

INT_MIN_8

|- INT_MIN (:bool # bool # bool) = 128

dimword_8

|- dimword (:bool # bool # bool) = 256

dimindex_12

|- dimindex (:i12) = 12

finite_12

|- FINITE UNIV

size12

|- CARD UNIV = 12

INT_MIN_12

|- INT_MIN (:i12) = 2048

dimword_12

|- dimword (:i12) = 4096

dimindex_16

|- dimindex (:i16) = 16

finite_16

|- FINITE UNIV

size16

|- CARD UNIV = 16

INT_MIN_16

|- INT_MIN (:i16) = 32768

dimword_16

|- dimword (:i16) = 65536

dimindex_20

|- dimindex (:i20) = 20

finite_20

|- FINITE UNIV

size20

|- CARD UNIV = 20

INT_MIN_20

|- INT_MIN (:i20) = 524288

dimword_20

|- dimword (:i20) = 1048576

dimindex_24

|- dimindex (:i24) = 24

finite_24

|- FINITE UNIV

size24

|- CARD UNIV = 24

INT_MIN_24

|- INT_MIN (:i24) = 8388608

dimword_24

|- dimword (:i24) = 16777216

dimindex_28

|- dimindex (:i28) = 28

finite_28

|- FINITE UNIV

size28

|- CARD UNIV = 28

INT_MIN_28

|- INT_MIN (:i28) = 134217728

dimword_28

|- dimword (:i28) = 268435456

dimindex_30

|- dimindex (:i30) = 30

finite_30

|- FINITE UNIV

size30

|- CARD UNIV = 30

INT_MIN_30

|- INT_MIN (:i30) = 536870912

dimword_30

|- dimword (:i30) = 1073741824

dimindex_32

|- dimindex (:i32) = 32

finite_32

|- FINITE UNIV

size32

|- CARD UNIV = 32

INT_MIN_32

|- INT_MIN (:i32) = 2147483648

dimword_32

|- dimword (:i32) = 4294967296

dimindex_64

|- dimindex (:i64) = 64

finite_64

|- FINITE UNIV

size64

|- CARD UNIV = 64

INT_MIN_64

|- INT_MIN (:i64) = 9223372036854775808

dimword_64

|- dimword (:i64) = 18446744073709551616

n2w_itself_ind

|- !P. (!n. P (n,(:'a))) ==> !v v1. P (v,v1)

n2w_itself_def

|- n2w_itself (n,(:'a)) = n2w n

fromNum_ind

|- !P. (!n. P (n,(:'a))) ==> !v v1. P (v,v1)

fromNum_def

|- fromNum (n,(:'a)) = n2w_itself (n MOD dimword (:'a),(:'a))