Theory bitArith

Parents

Contents

Type operators

(none)

Constants

Definitions

add_defbleval_def_primitivefromBL_deflte_defsub_deftobl_def

Theorems

DIV_POW2EVERYF_bleval0EVERYF_suffix_blevalLASTbl_nonzeroadd_aux_defadd_aux_indadd_aux_thmadd_thmbleval_APPENDbleval_defbleval_indbleval_lessbleval_less_largedivpow2_computedivpow2_defdivpow2_inddivpow2_thmfromBL_correctfrombl_correctfrombl_deffrombl_indkaratsuba_bitkaratsuba_numlte_aux_deflte_aux_indlte_aux_thmlte_thmmodpow2_computemodpow2_defmodpow2_indmodpow2_thmmul_defmul_indmul_thmmulpow2_computemulpow2_defmulpow2_indmulpow2_thmsub_aux_defsub_aux_indsub_aux_thmsub_thmtobl0tobl_NUMERALtobl_correctzeroPad_defzeroPad_indzeroPad_thm

Definitions

add_def
⊢ ∀bs1 bs2. add bs1 bs2 = add_aux bs1 bs2 F
bleval_def_primitive
⊢ bleval =
  WFREC (@R. WF R ∧ (∀rest. R rest (T::rest)) ∧ ∀rest. R rest (F::rest))
    (λbleval a.
         case a of
           [] => I 0
         | T::rest => I (2 * bleval rest + 1)
         | F::rest => I (2 * bleval rest))
fromBL_def
⊢ ∀bs.
    fromBL bs =
    if bs = [] then 0
    else
      (let
         bs1 = REV bs []
       in
         if HD bs1 then NUMERAL (frombl F bs)
         else
           (let
              bs2 = dropWhile ($<=> F) bs1;
              bs3 = REV bs2 []
            in
              if bs3 = [] then 0 else NUMERAL (frombl F bs3)))
lte_def
⊢ ∀bs1 bs2.
    lte bs1 bs2 ⇔
    (let
       (bs1pad,bs2pad) = zeroPad bs1 bs2
     in
       lte_aux (REV bs1pad []) (REV bs2pad []))
sub_def
⊢ ∀bs1 bs2. sub bs1 bs2 = if lte bs2 bs1 then sub_aux bs1 bs2 F else []
tobl_def
⊢ (∀b. tobl ZERO b = if b then [] else [T]) ∧
  (∀n x. tobl (BIT1 n) x = x::tobl n x) ∧
  ∀n x. tobl (BIT2 n) x = ¬x::tobl n F

Theorems

DIV_POW2
⊢ ∀x y. 0 < y ⇒ 2 * x DIV (2 * y) = x DIV y
EVERYF_bleval0
⊢ bleval bs = 0 ⇔ EVERY ($<=> F) bs
EVERYF_suffix_bleval
⊢ EVERY ($<=> F) s ⇒ bleval (p ⧺ s) = bleval p
LASTbl_nonzero
⊢ LAST (x::xs) ⇒ 0 < bleval (x::xs)
add_aux_def
⊢ (∀bs. add_aux [] bs F = bs) ∧ add_aux [] [] T = [T] ∧
  (∀bs. add_aux [] (F::bs) T = T::bs) ∧
  (∀bs. add_aux [] (T::bs) T = F::add_aux [] bs T) ∧
  (∀v5 v4. add_aux (v4::v5) [] F = v4::v5) ∧
  (∀bs. add_aux (F::bs) [] T = T::bs) ∧
  (∀bs. add_aux (T::bs) [] T = F::add_aux [] bs T) ∧
  (∀bs2 bs1. add_aux (F::bs1) (F::bs2) T = T::add_aux bs1 bs2 F) ∧
  (∀bs2 bs1. add_aux (F::bs1) (F::bs2) F = F::add_aux bs1 bs2 F) ∧
  (∀bs2 bs1. add_aux (T::bs1) (F::bs2) F = T::add_aux bs1 bs2 F) ∧
  (∀bs2 bs1. add_aux (T::bs1) (F::bs2) T = F::add_aux bs1 bs2 T) ∧
  (∀bs2 bs1. add_aux (F::bs1) (T::bs2) T = F::add_aux bs1 bs2 T) ∧
  (∀bs2 bs1. add_aux (F::bs1) (T::bs2) F = T::add_aux bs1 bs2 F) ∧
  (∀bs2 bs1. add_aux (T::bs1) (T::bs2) T = T::add_aux bs1 bs2 T) ∧
  ∀bs2 bs1. add_aux (T::bs1) (T::bs2) F = F::add_aux bs1 bs2 T
add_aux_ind
⊢ ∀P. (∀bs. P [] bs F) ∧ P [] [] T ∧ (∀bs. P [] (F::bs) T) ∧
      (∀bs. P [] bs T ⇒ P [] (T::bs) T) ∧ (∀v4 v5. P (v4::v5) [] F) ∧
      (∀bs. P (F::bs) [] T) ∧ (∀bs. P [] bs T ⇒ P (T::bs) [] T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (F::bs1) (F::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (F::bs1) (F::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (T::bs1) (F::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (T::bs1) (F::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (F::bs1) (T::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (F::bs1) (T::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (T::bs1) (T::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (T::bs1) (T::bs2) F) ⇒
      ∀v v1 v2. P v v1 v2
add_aux_thm
⊢ ∀m n b. bleval (add_aux m n b) = bleval m + bleval n + if b then 1 else 0
add_thm
⊢ bleval (add m n) = bleval m + bleval n
bleval_APPEND
⊢ bleval (xs ⧺ ys) = bleval ys * 2 ** LENGTH xs + bleval xs
bleval_def
⊢ bleval [] = 0 ∧ (∀rest. bleval (T::rest) = 2 * bleval rest + 1) ∧
  ∀rest. bleval (F::rest) = 2 * bleval rest
bleval_ind
⊢ ∀P. P [] ∧ (∀rest. P rest ⇒ P (T::rest)) ∧ (∀rest. P rest ⇒ P (F::rest)) ⇒
      ∀v. P v
bleval_less
⊢ ∀bs. bleval bs < 2 ** LENGTH bs
bleval_less_large
⊢ LENGTH bs ≤ k ⇒ bleval bs < 2 ** k
divpow2_compute
⊢ (∀k. divpow2 [] k = []) ∧ (∀v3 v2. divpow2 (v2::v3) 0 = v2::v3) ∧
  (∀k bs b.
     divpow2 (b::bs) (NUMERAL (BIT1 k)) = divpow2 bs (NUMERAL (BIT1 k) − 1)) ∧
  ∀k bs b.
    divpow2 (b::bs) (NUMERAL (BIT2 k)) = divpow2 bs (NUMERAL (BIT1 k))
divpow2_def
⊢ (∀k. divpow2 [] k = []) ∧ (∀v3 v2. divpow2 (v2::v3) 0 = v2::v3) ∧
  ∀k bs b. divpow2 (b::bs) (SUC k) = divpow2 bs k
divpow2_ind
⊢ ∀P. (∀k. P [] k) ∧ (∀v2 v3. P (v2::v3) 0) ∧
      (∀b bs k. P bs k ⇒ P (b::bs) (SUC k)) ⇒
      ∀v v1. P v v1
divpow2_thm
⊢ ∀x k. bleval (divpow2 x k) = bleval x DIV 2 ** k
fromBL_correct
⊢ fromBL bs = bleval bs
frombl_correct
⊢ bl ≠ [] ∧ LAST bl ⇒ frombl F bl = bleval bl ∧ frombl T bl = bleval bl − 1
frombl_def
⊢ (∀addedp. frombl addedp [] = 0) ∧ frombl T [T] = ZERO ∧
  frombl F [T] = BIT1 ZERO ∧
  (∀rest. frombl T (F::rest) = BIT1 (frombl T rest)) ∧
  (∀rest. frombl F (F::rest) = BIT2 (frombl T rest)) ∧
  (∀v5 v4. frombl T (T::v4::v5) = BIT2 (frombl T (v4::v5))) ∧
  ∀v7 v6. frombl F (T::v6::v7) = BIT1 (frombl F (v6::v7))
frombl_ind
⊢ ∀P. (∀addedp. P addedp []) ∧ P T [T] ∧ P F [T] ∧
      (∀rest. P T rest ⇒ P T (F::rest)) ∧
      (∀rest. P T rest ⇒ P F (F::rest)) ∧
      (∀v4 v5. P T (v4::v5) ⇒ P T (T::v4::v5)) ∧
      (∀v6 v7. P F (v6::v7) ⇒ P F (T::v6::v7)) ⇒
      ∀v v1. P v v1
karatsuba_bit
⊢ ∀x y.
    bleval (mul x y) =
    bleval
      (let
         d =
           fromBL
             (divpow2
                (add (divpow2 (tobl (LENGTH x) F) 1)
                   (divpow2 (tobl (LENGTH y) F) 1)) 1) + 1;
         x1 = divpow2 x d;
         x0 = modpow2 x d;
         y1 = divpow2 y d;
         y0 = modpow2 y d;
         z0 = mul x0 y0;
         z2 = mul x1 y1;
         z1a = add x1 x0;
         z1b = add y1 y0;
         z1Mul = mul z1a z1b;
         z1 = sub (sub z1Mul z2) z0
       in
         add (mulpow2 (add (mulpow2 z2 d) z1) d) z0)
karatsuba_num
⊢ ∀d x y.
    0 < d ⇒
    x * y =
    (let
       x1 = x DIV d;
       x0 = x MOD d;
       y1 = y DIV d;
       y0 = y MOD d;
       z0 = x0 * y0;
       z2 = x1 * y1;
       z1a = x1 + x0;
       z1b = y1 + y0;
       z1 = z1a * z1b;
       z1 = z1 − z2 − z0
     in
       (z2 * d + z1) * d + z0)
lte_aux_def
⊢ (lte_aux [] [] ⇔ T) ∧ (∀bs2 bs1. lte_aux (F::bs1) (T::bs2) ⇔ T) ∧
  (∀bs2 bs1. lte_aux (T::bs1) (F::bs2) ⇔ F) ∧
  (∀bs2 bs1. lte_aux (T::bs1) (T::bs2) ⇔ lte_aux bs1 bs2) ∧
  (∀bs2 bs1. lte_aux (F::bs1) (F::bs2) ⇔ lte_aux bs1 bs2) ∧
  (∀v8 v7. lte_aux [] (v7::v8) ⇔ F) ∧ ∀v4 v3. lte_aux (v3::v4) [] ⇔ F
lte_aux_ind
⊢ ∀P. P [] [] ∧ (∀bs1 bs2. P (F::bs1) (T::bs2)) ∧
      (∀bs1 bs2. P (T::bs1) (F::bs2)) ∧
      (∀bs1 bs2. P bs1 bs2 ⇒ P (T::bs1) (T::bs2)) ∧
      (∀bs1 bs2. P bs1 bs2 ⇒ P (F::bs1) (F::bs2)) ∧
      (∀v7 v8. P [] (v7::v8)) ∧ (∀v3 v4. P (v3::v4) []) ⇒
      ∀v v1. P v v1
lte_aux_thm
⊢ ∀bs1 bs2.
    LENGTH bs1 = LENGTH bs2 ⇒
    (lte_aux bs1 bs2 ⇔ bleval (REVERSE bs1) ≤ bleval (REVERSE bs2))
lte_thm
⊢ ∀bs1 bs2. lte bs1 bs2 ⇔ bleval bs1 ≤ bleval bs2
modpow2_compute
⊢ (∀k. modpow2 [] k = []) ∧ (∀v3 v2. modpow2 (v2::v3) 0 = []) ∧
  (∀k bs b.
     modpow2 (b::bs) (NUMERAL (BIT1 k)) =
     b::modpow2 bs (NUMERAL (BIT1 k) − 1)) ∧
  ∀k bs b.
    modpow2 (b::bs) (NUMERAL (BIT2 k)) = b::modpow2 bs (NUMERAL (BIT1 k))
modpow2_def
⊢ (∀k. modpow2 [] k = []) ∧ (∀v3 v2. modpow2 (v2::v3) 0 = []) ∧
  ∀k bs b. modpow2 (b::bs) (SUC k) = b::modpow2 bs k
modpow2_ind
⊢ ∀P. (∀k. P [] k) ∧ (∀v2 v3. P (v2::v3) 0) ∧
      (∀b bs k. P bs k ⇒ P (b::bs) (SUC k)) ⇒
      ∀v v1. P v v1
modpow2_thm
⊢ ∀x k. bleval (modpow2 x k) = bleval x MOD 2 ** k
mul_def
⊢ (∀v0. mul [] v0 = []) ∧
  (∀bs2 bs. mul (T::bs) bs2 = add bs2 (mul bs (F::bs2))) ∧
  ∀bs2 bs. mul (F::bs) bs2 = mul bs (F::bs2)
mul_ind
⊢ ∀P. (∀v0. P [] v0) ∧ (∀bs bs2. P bs (F::bs2) ⇒ P (T::bs) bs2) ∧
      (∀bs bs2. P bs (F::bs2) ⇒ P (F::bs) bs2) ⇒
      ∀v v1. P v v1
mul_thm
⊢ ∀x y. bleval (mul x y) = bleval x * bleval y
mulpow2_compute
⊢ (∀v0. mulpow2 [] v0 = []) ∧ (∀v3 v2. mulpow2 (v2::v3) 0 = v2::v3) ∧
  (∀v5 v4 k.
     mulpow2 (v4::v5) (NUMERAL (BIT1 k)) =
     F::mulpow2 (v4::v5) (NUMERAL (BIT1 k) − 1)) ∧
  ∀v5 v4 k.
    mulpow2 (v4::v5) (NUMERAL (BIT2 k)) =
    F::mulpow2 (v4::v5) (NUMERAL (BIT1 k))
mulpow2_def
⊢ (∀v0. mulpow2 [] v0 = []) ∧ (∀v3 v2. mulpow2 (v2::v3) 0 = v2::v3) ∧
  ∀v5 v4 k. mulpow2 (v4::v5) (SUC k) = F::mulpow2 (v4::v5) k
mulpow2_ind
⊢ ∀P. (∀v0. P [] v0) ∧ (∀v2 v3. P (v2::v3) 0) ∧
      (∀v4 v5 k. P (v4::v5) k ⇒ P (v4::v5) (SUC k)) ⇒
      ∀v v1. P v v1
mulpow2_thm
⊢ ∀bs k. bleval (mulpow2 bs k) = bleval bs * 2 ** k
sub_aux_def
⊢ (∀v1 v0. sub_aux [] v0 v1 = []) ∧
  (∀bs1. sub_aux (F::bs1) [] T = T::sub_aux bs1 [] T) ∧
  (∀bs1. sub_aux (T::bs1) [] T = F::bs1) ∧
  (∀bs1. sub_aux (F::bs1) [] F = F::bs1) ∧
  (∀bs1. sub_aux (T::bs1) [] F = T::bs1) ∧
  (∀bs2 bs1. sub_aux (F::bs1) (F::bs2) T = T::sub_aux bs1 bs2 T) ∧
  (∀bs2 bs1. sub_aux (F::bs1) (F::bs2) F = F::sub_aux bs1 bs2 F) ∧
  (∀bs2 bs1. sub_aux (F::bs1) (T::bs2) T = F::sub_aux bs1 bs2 T) ∧
  (∀bs2 bs1. sub_aux (F::bs1) (T::bs2) F = T::sub_aux bs1 bs2 T) ∧
  (∀bs2 bs1. sub_aux (T::bs1) (F::bs2) T = F::sub_aux bs1 bs2 F) ∧
  (∀bs2 bs1. sub_aux (T::bs1) (F::bs2) F = T::sub_aux bs1 bs2 F) ∧
  (∀bs2 bs1. sub_aux (T::bs1) (T::bs2) T = T::sub_aux bs1 bs2 T) ∧
  ∀bs2 bs1. sub_aux (T::bs1) (T::bs2) F = F::sub_aux bs1 bs2 F
sub_aux_ind
⊢ ∀P. (∀v0 v1. P [] v0 v1) ∧ (∀bs1. P bs1 [] T ⇒ P (F::bs1) [] T) ∧
      (∀bs1. P (T::bs1) [] T) ∧ (∀bs1. P (F::bs1) [] F) ∧
      (∀bs1. P (T::bs1) [] F) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (F::bs1) (F::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (F::bs1) (F::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (F::bs1) (T::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (F::bs1) (T::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (T::bs1) (F::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (T::bs1) (F::bs2) F) ∧
      (∀bs1 bs2. P bs1 bs2 T ⇒ P (T::bs1) (T::bs2) T) ∧
      (∀bs1 bs2. P bs1 bs2 F ⇒ P (T::bs1) (T::bs2) F) ⇒
      ∀v v1 v2. P v v1 v2
sub_aux_thm
⊢ ∀bs1 bs2 b.
    bleval bs2 + (if b then 1 else 0) ≤ bleval bs1 ⇒
    bleval (sub_aux bs1 bs2 b) =
    bleval bs1 − (bleval bs2 + if b then 1 else 0)
sub_thm
⊢ ∀m n. bleval (sub m n) = bleval m − bleval n
tobl0
⊢ tobl 0 b = tobl ZERO b
tobl_NUMERAL
⊢ tobl (NUMERAL x) = tobl x
tobl_correct
⊢ bleval (tobl n T) = n ∧ bleval (tobl n F) = n + 1
zeroPad_def
⊢ zeroPad [] [] = ([],[]) ∧
  (∀bs1 b.
     zeroPad (b::bs1) [] =
     (let (bs1pad,bs2pad) = zeroPad bs1 [] in (b::bs1pad,F::bs2pad))) ∧
  (∀bs2 b.
     zeroPad [] (b::bs2) =
     (let (bs1pad,bs2pad) = zeroPad [] bs2 in (F::bs1pad,b::bs2pad))) ∧
  ∀bs2 bs1 b2 b1.
    zeroPad (b1::bs1) (b2::bs2) =
    (let (bs1pad,bs2pad) = zeroPad bs1 bs2 in (b1::bs1pad,b2::bs2pad))
zeroPad_ind
⊢ ∀P. P [] [] ∧ (∀b bs1. P bs1 [] ⇒ P (b::bs1) []) ∧
      (∀b bs2. P [] bs2 ⇒ P [] (b::bs2)) ∧
      (∀b1 bs1 b2 bs2. P bs1 bs2 ⇒ P (b1::bs1) (b2::bs2)) ⇒
      ∀v v1. P v v1
zeroPad_thm
⊢ ∀bs1 bs2 bs1pad bs2pad.
    zeroPad bs1 bs2 = (bs1pad,bs2pad) ⇒
    bleval bs1 = bleval bs1pad ∧ bleval bs2 = bleval bs2pad ∧
    LENGTH bs1pad = LENGTH bs2pad