Theory "int_bitwise"

Parents Omega int_arith bit

Signature

Constant	Type
bits_bitwise	:(β -> γ -> α) -> β list # β -> γ list # γ -> α list # α
bits_of_int	:int -> bool list # bool
bits_of_num	:num -> bool list
int_and	:int -> int -> int
int_bit	:num -> int -> bool
int_bitwise	:(bool -> bool -> bool) -> int -> int -> int
int_not	:int -> int
int_of_bits	:bool list # 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	:bool list -> num

Definitions

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_xor_def

⊢ int_xor = int_bitwise (λx y. x ⇎ y)

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

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_or_def

⊢ int_or = int_bitwise $\/

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

int_not_def

⊢ ∀i. int_not i = 0 − i − 1

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_bit_def

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

int_and_def

⊢ int_and = int_bitwise $/\

bits_of_num_primitive_def

⊢ bits_of_num =
  WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R (n DIV 2) n)
    (λbits_of_num a. I (if a = 0 then [] else ODD a::bits_of_num (a 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)

Theorems

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

int_of_bits_bits_of_int

⊢ ∀i. int_of_bits (bits_of_int i) = i

int_not_not

⊢ ∀i. int_not (int_not i) = i

int_not

⊢ int_not = int_bitwise (λx y. ¬y) 0

int_bit_xor

⊢ ∀j i n. int_bit n (int_xor i j) ⇔ (int_bit n i ⇎ int_bit n j)

int_bit_shift_right

⊢ ∀b n i. int_bit b (int_shift_right n i) ⇔ int_bit (b + n) i

int_bit_shift_left

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

int_bit_or

⊢ ∀j i n. int_bit n (int_or i j) ⇔ int_bit n i ∨ int_bit n j

int_bit_not

⊢ ∀b i. int_bit b (int_not i) ⇔ ¬int_bit b i

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_bit_equiv

⊢ ∀i j. (i = j) ⇔ ∀n. int_bit n i ⇔ int_bit n j

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

⊢ ∀j i n. int_bit n (int_and i j) ⇔ int_bit n i ∧ int_bit n j

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)

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