Theory "int_bitwise"

Parents bit Omega int_arith

Signature

Constant	Type
bits_bitwise	:(β -> γ -> α) -> β list # β -> γ list # γ -> α list # α
bits_bitwise_tupled	:(β -> γ -> α) # (β list # β) # γ list # γ -> α list # α
bits_of_int	:int -> bitstring # bool
bits_of_num	:num -> bitstring
int_and	:int -> int -> int
int_bit	:num -> int -> bool
int_bitwise	:bool reln -> int -> int -> int
int_not	:int -> int
int_of_bits	:bitstring # bool -> int
int_or	:int -> int -> int
int_shift_left	:num -> int -> int
int_shift_right	:num -> int -> int
int_xor	:int -> int -> int
num_of_bits	:bitstring -> num

Definitions

int_not_def

|- ∀i. int_not i = 0 − i − 1

int_bit_def

|- ∀b i.
     int_bit b i ⇔ if i < 0 then ¬BIT b (Num (int_not i)) else BIT b (Num i)

bits_of_num_primitive_def

|- bits_of_num =
   WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R (n DIV 2) n)
     (λbits_of_num n. I (if n = 0 then [] else ODD n::bits_of_num (n DIV 2)))

bits_of_int_def

|- ∀i.
     bits_of_int i =
     if i < 0 then (MAP $~ (bits_of_num (Num (int_not i))),T)
     else (bits_of_num (Num i),F)

num_of_bits_primitive_def

|- num_of_bits =
   WFREC (@R. WF R ∧ (∀bs. R bs (F::bs)) ∧ ∀bs. R bs (T::bs))
     (λnum_of_bits a.
        case a of
          [] => I 0
        | T::bs => I (1 + 2 * num_of_bits bs)
        | F::bs => I (2 * num_of_bits bs))

int_of_bits_def

|- ∀bs rest.
     int_of_bits (bs,rest) =
     if rest then int_not (&num_of_bits (MAP $~ bs)) else &num_of_bits bs

bits_bitwise_tupled_primitive_def

|- bits_bitwise_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀b2 r2 bs2 r1 f. R (f,([],r1),bs2,r2) (f,([],r1),b2::bs2,r2)) ∧
        (∀b1 r2 r1 bs1 f. R (f,(bs1,r1),[],r2) (f,(b1::bs1,r1),[],r2)) ∧
        ∀b2 b1 r2 bs2 r1 bs1 f.
          R (f,(bs1,r1),bs2,r2) (f,(b1::bs1,r1),b2::bs2,r2))
     (λbits_bitwise_tupled a.
        case a of
          (f,([],r1),[],r2) => I ([],f r1 r2)
        | (f,(b1::bs1,r1),[],r2) =>
            I
              (let (bs,r) = bits_bitwise_tupled (f,(bs1,r1),[],r2)
               in
                 (f b1 r2::bs,r))
        | (f,([],r1),b2::bs2,r2) =>
            I
              (let (bs,r) = bits_bitwise_tupled (f,([],r1),bs2,r2)
               in
                 (f r1 b2::bs,r))
        | (f,(b1'::bs1',r1),b2::bs2,r2) =>
            I
              (let (bs,r) = bits_bitwise_tupled (f,(bs1',r1),bs2,r2)
               in
                 (f b1' b2::bs,r)))

bits_bitwise_curried_def

|- ∀x x1 x2. bits_bitwise x x1 x2 = bits_bitwise_tupled (x,x1,x2)

int_bitwise_def

|- ∀f i j.
     int_bitwise f i j =
     int_of_bits (bits_bitwise f (bits_of_int i) (bits_of_int j))

int_and_def

|- int_and = int_bitwise $/\

int_or_def

|- int_or = int_bitwise $\/

int_xor_def

|- int_xor = int_bitwise (λx y. x ⇎ y)

int_shift_left_def

|- ∀n i.
     int_shift_left n i =
     (let (bs,r) = bits_of_int i in int_of_bits (GENLIST (K F) n ++ bs,r))

int_shift_right_def

|- ∀n i.
     int_shift_right n i =
     (let (bs,r) = bits_of_int i in int_of_bits (DROP n bs,r))

Theorems

int_not_not

|- ∀i. int_not (int_not i) = i

int_bit_not

|- ∀b i. int_bit b (int_not i) ⇔ ¬int_bit b i

bits_of_num_ind

|- ∀P. (∀n. (n ≠ 0 ⇒ P (n DIV 2)) ⇒ P n) ⇒ ∀v. P v

bits_of_num_def

|- ∀n. bits_of_num n = if n = 0 then [] else ODD n::bits_of_num (n DIV 2)

num_of_bits_ind

|- ∀P. P [] ∧ (∀bs. P bs ⇒ P (F::bs)) ∧ (∀bs. P bs ⇒ P (T::bs)) ⇒ ∀v. P v

num_of_bits_def

|- (num_of_bits [] = 0) ∧ (∀bs. num_of_bits (F::bs) = 2 * num_of_bits bs) ∧
   ∀bs. num_of_bits (T::bs) = 1 + 2 * num_of_bits bs

bits_bitwise_ind

|- ∀P.
     (∀f r1 r2. P f ([],r1) ([],r2)) ∧
     (∀f r1 b2 bs2 r2. P f ([],r1) (bs2,r2) ⇒ P f ([],r1) (b2::bs2,r2)) ∧
     (∀f b1 bs1 r1 r2. P f (bs1,r1) ([],r2) ⇒ P f (b1::bs1,r1) ([],r2)) ∧
     (∀f b1 bs1 r1 b2 bs2 r2.
        P f (bs1,r1) (bs2,r2) ⇒ P f (b1::bs1,r1) (b2::bs2,r2)) ⇒
     ∀v v1 v2 v3 v4. P v (v1,v2) (v3,v4)

bits_bitwise_def

|- (∀r2 r1 f. bits_bitwise f ([],r1) ([],r2) = ([],f r1 r2)) ∧
   (∀r2 r1 f bs2 b2.
      bits_bitwise f ([],r1) (b2::bs2,r2) =
      (let (bs,r) = bits_bitwise f ([],r1) (bs2,r2) in (f r1 b2::bs,r))) ∧
   (∀r2 r1 f bs1 b1.
      bits_bitwise f (b1::bs1,r1) ([],r2) =
      (let (bs,r) = bits_bitwise f (bs1,r1) ([],r2) in (f b1 r2::bs,r))) ∧
   ∀r2 r1 f bs2 bs1 b2 b1.
     bits_bitwise f (b1::bs1,r1) (b2::bs2,r2) =
     (let (bs,r) = bits_bitwise f (bs1,r1) (bs2,r2) in (f b1 b2::bs,r))

int_not

|- int_not = int_bitwise (λx y. ¬y) 0

int_bit_int_of_bits

|- int_bit n (int_of_bits b) ⇔
   if n < LENGTH (FST b) then EL n (FST b) else SND b

int_of_bits_bits_of_int

|- ∀i. int_of_bits (bits_of_int i) = i

int_bit_bitwise

|- ∀n f i j. int_bit n (int_bitwise f i j) ⇔ f (int_bit n i) (int_bit n j)

int_bit_and

|- ∀n i j. int_bit n (int_and i j) ⇔ int_bit n i ∧ int_bit n j

int_bit_or

|- ∀n i j. int_bit n (int_or i j) ⇔ int_bit n i ∨ int_bit n j

int_bit_xor

|- ∀n i j. int_bit n (int_xor i j) ⇔ (int_bit n i ⇎ int_bit n j)

int_bit_equiv

|- ∀i j. (i = j) ⇔ ∀n. int_bit n i ⇔ int_bit n j

int_bit_shift_left

|- ∀b n i. int_bit b (int_shift_left n i) ⇔ n ≤ b ∧ int_bit (b − n) i

int_bit_shift_right

|- ∀b n i. int_bit b (int_shift_right n i) ⇔ int_bit (b + n) i