Theory "integer_word"

Parents     Omega   int_arith   words

Signature

Constant Type
w2i :'a word -> int
i2w :int -> 'a word
UINT_MAX :'a itself -> int
INT_MIN :'a itself -> int
INT_MAX :'a itself -> int

Definitions

i2w_def 
|- !i. i2w i = (if i < 0 then $- (n2w (Num ~i)) else n2w (Num i))
w2i_def 
|- !w. w2i w = (if word_msb w then ~ & (w2n ($- w)) else & (w2n w))
UINT_MAX_def 
|- UINT_MAX (:'a) = & (dimword (:'a)) - 1
INT_MAX_def 
|- INT_MAX (:'a) = & (INT_MIN (:'a)) - 1
INT_MIN_def 
|- INT_MIN (:'a) = ~INT_MAX (:'a) - 1

Theorems

INT_MAX_32 
|- INT_MAX (:i32) = 2147483647
INT_MIN_32 
|- INT_MIN (:i32) = ~2147483648
UINT_MAX_32 
|- UINT_MAX (:i32) = 4294967295
ONE_LE_TWOEXP 
|- 1 <= 2 ** m
w2i_n2w_pos 
|- n < INT_MIN (:'a) ==> (w2i (n2w n) = & n)
w2i_n2w_neg 
|- INT_MIN (:'a) <= n /\ n < dimword (:'a) ==>
   (w2i (n2w n) = ~ & (dimword (:'a) - n))
i2w_w2i 
|- i2w (w2i w) = w
w2i_i2w 
|- INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a) ==> (w2i (i2w i) = i)
word_msb_i2w 
|- word_msb (i2w i) = & (INT_MIN (:'a)) <= i % & (dimword (:'a))