Structure bitArithTheory
signature bitArithTheory =
sig
type thm = Thm.thm
(* Definitions *)
val add_def : thm
val bleval_def_primitive : thm
val fromBL_def : thm
val lte_def : thm
val sub_def : thm
val tobl_def : thm
(* Theorems *)
val DIV_POW2 : thm
val EVERYF_bleval0 : thm
val EVERYF_suffix_bleval : thm
val LASTbl_nonzero : thm
val add_aux_def : thm
val add_aux_ind : thm
val add_aux_thm : thm
val add_thm : thm
val bleval_APPEND : thm
val bleval_def : thm
val bleval_ind : thm
val bleval_less : thm
val bleval_less_large : thm
val divpow2_compute : thm
val divpow2_def : thm
val divpow2_ind : thm
val divpow2_thm : thm
val fromBL_correct : thm
val frombl_correct : thm
val frombl_def : thm
val frombl_ind : thm
val karatsuba_bit : thm
val karatsuba_num : thm
val lte_aux_def : thm
val lte_aux_ind : thm
val lte_aux_thm : thm
val lte_thm : thm
val modpow2_compute : thm
val modpow2_def : thm
val modpow2_ind : thm
val modpow2_thm : thm
val mul_def : thm
val mul_ind : thm
val mul_thm : thm
val mulpow2_compute : thm
val mulpow2_def : thm
val mulpow2_ind : thm
val mulpow2_thm : thm
val sub_aux_def : thm
val sub_aux_ind : thm
val sub_aux_thm : thm
val sub_thm : thm
val tobl0 : thm
val tobl_NUMERAL : thm
val tobl_correct : thm
val zeroPad_def : thm
val zeroPad_ind : thm
val zeroPad_thm : thm
val bitArith_grammars : type_grammar.grammar * term_grammar.grammar
(*
[real] Parent theory of "bitArith"
[add_def] Definition
⊢ ∀bs1 bs2. add bs1 bs2 = add_aux bs1 bs2 F
[bleval_def_primitive] Definition
⊢ 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] Definition
⊢ ∀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] Definition
⊢ ∀bs1 bs2.
lte bs1 bs2 ⇔
(let
(bs1pad,bs2pad) = zeroPad bs1 bs2
in
lte_aux (REV bs1pad []) (REV bs2pad []))
[sub_def] Definition
⊢ ∀bs1 bs2.
sub bs1 bs2 = if lte bs2 bs1 then sub_aux bs1 bs2 F else []
[tobl_def] Definition
⊢ (∀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
[DIV_POW2] Theorem
⊢ ∀x y. 0 < y ⇒ 2 * x DIV (2 * y) = x DIV y
[EVERYF_bleval0] Theorem
⊢ bleval bs = 0 ⇔ EVERY ($<=> F) bs
[EVERYF_suffix_bleval] Theorem
⊢ EVERY ($<=> F) s ⇒ bleval (p ⧺ s) = bleval p
[LASTbl_nonzero] Theorem
⊢ LAST (x::xs) ⇒ 0 < bleval (x::xs)
[add_aux_def] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀m n b.
bleval (add_aux m n b) = bleval m + bleval n + if b then 1 else 0
[add_thm] Theorem
⊢ bleval (add m n) = bleval m + bleval n
[bleval_APPEND] Theorem
⊢ bleval (xs ⧺ ys) = bleval ys * 2 ** LENGTH xs + bleval xs
[bleval_def] Theorem
⊢ bleval [] = 0 ∧ (∀rest. bleval (T::rest) = 2 * bleval rest + 1) ∧
∀rest. bleval (F::rest) = 2 * bleval rest
[bleval_ind] Theorem
⊢ ∀P. P [] ∧ (∀rest. P rest ⇒ P (T::rest)) ∧
(∀rest. P rest ⇒ P (F::rest)) ⇒
∀v. P v
[bleval_less] Theorem
⊢ ∀bs. bleval bs < 2 ** LENGTH bs
[bleval_less_large] Theorem
⊢ LENGTH bs ≤ k ⇒ bleval bs < 2 ** k
[divpow2_compute] Theorem
⊢ (∀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] Theorem
⊢ (∀k. divpow2 [] k = []) ∧ (∀v3 v2. divpow2 (v2::v3) 0 = v2::v3) ∧
∀k bs b. divpow2 (b::bs) (SUC k) = divpow2 bs k
[divpow2_ind] Theorem
⊢ ∀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] Theorem
⊢ ∀x k. bleval (divpow2 x k) = bleval x DIV 2 ** k
[fromBL_correct] Theorem
⊢ fromBL bs = bleval bs
[frombl_correct] Theorem
⊢ bl ≠ [] ∧ LAST bl ⇒
frombl F bl = bleval bl ∧ frombl T bl = bleval bl − 1
[frombl_def] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ (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] Theorem
⊢ ∀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] Theorem
⊢ ∀bs1 bs2.
LENGTH bs1 = LENGTH bs2 ⇒
(lte_aux bs1 bs2 ⇔ bleval (REVERSE bs1) ≤ bleval (REVERSE bs2))
[lte_thm] Theorem
⊢ ∀bs1 bs2. lte bs1 bs2 ⇔ bleval bs1 ≤ bleval bs2
[modpow2_compute] Theorem
⊢ (∀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] Theorem
⊢ (∀k. modpow2 [] k = []) ∧ (∀v3 v2. modpow2 (v2::v3) 0 = []) ∧
∀k bs b. modpow2 (b::bs) (SUC k) = b::modpow2 bs k
[modpow2_ind] Theorem
⊢ ∀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] Theorem
⊢ ∀x k. bleval (modpow2 x k) = bleval x MOD 2 ** k
[mul_def] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀x y. bleval (mul x y) = bleval x * bleval y
[mulpow2_compute] Theorem
⊢ (∀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] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀bs k. bleval (mulpow2 bs k) = bleval bs * 2 ** k
[sub_aux_def] Theorem
⊢ (∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀m n. bleval (sub m n) = bleval m − bleval n
[tobl0] Theorem
⊢ tobl 0 b = tobl ZERO b
[tobl_NUMERAL] Theorem
⊢ tobl (NUMERAL x) = tobl x
[tobl_correct] Theorem
⊢ bleval (tobl n T) = n ∧ bleval (tobl n F) = n + 1
[zeroPad_def] Theorem
⊢ 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] Theorem
⊢ ∀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] Theorem
⊢ ∀bs1 bs2 bs1pad bs2pad.
zeroPad bs1 bs2 = (bs1pad,bs2pad) ⇒
bleval bs1 = bleval bs1pad ∧ bleval bs2 = bleval bs2pad ∧
LENGTH bs1pad = LENGTH bs2pad
*)
end
HOL 4, Trindemossen-1