bitArithScript.sml

1(**
2  Translation from HOL4 numbers to bit strings
3
4  Used in inital attempt to speed up computations, used by evaluation of the
5  first phase
6**)
7Theory bitArith
8Ancestors
9  list arithmetic real
10Libs
11  BasicProvers
12
13val _ = numLib.temp_prefer_num();
14
15(** Code from Michael Norrish for translating to boolean vectors **)
16val tobl_def = new_specification(
17  "tobl_def", ["tobl"],
18  numeralTheory.bit_initiality
19    |> INST_TYPE [alpha |-> “:bool -> bool list”]
20    |> SPECL [“\b:bool. if b then [] else [T]”,
21              “\ (n:num) r b. b::(r b : bool list)”,
22              “\ (n:num) r b. ~b::r F”]
23    |> SIMP_RULE bool_ss [FUN_EQ_THM])
24
25val _ = computeLib.add_persistent_funs ["tobl_def"]
26
27Theorem tobl_NUMERAL[compute]: tobl (NUMERAL x) = tobl x
28Proof
29  simp[arithmeticTheory.NUMERAL_DEF]
30QED
31
32Theorem tobl0[compute]: tobl 0 b = tobl ZERO b
33Proof
34  simp[arithmeticTheory.ALT_ZERO]
35QED
36
37Definition bleval_def:
38  bleval [] = 0 /\
39  bleval (T::rest) = 2 * bleval rest + 1 /\
40  bleval (F::rest) = 2 * bleval rest
41End
42
43Theorem bleval_APPEND:
44  bleval (xs ++ ys) = bleval ys * 2 EXP (LENGTH xs) + bleval xs
45Proof
46  Induct_on ‘xs’ >> simp[FORALL_BOOL, bleval_def] >>
47  simp[arithmeticTheory.EXP]
48QED
49
50Theorem EVERYF_bleval0:
51  bleval bs = 0 <=> EVERY ((=) F) bs
52Proof
53  Induct_on ‘bs’ >> simp[bleval_def, FORALL_BOOL]
54QED
55
56Theorem EVERYF_suffix_bleval:
57  EVERY ((=) F) s ==> bleval (p ++ s) = bleval p
58Proof
59  simp[bleval_APPEND, EVERYF_bleval0]
60QED
61
62Theorem LASTbl_nonzero:
63  LAST (x::xs) ==> 0 < bleval (x::xs)
64Proof
65  qid_spec_tac ‘x’ >> Induct_on ‘xs’ >> simp[bleval_def] >> rpt gen_tac >>
66  rename [‘bleval (a::b::xs)’] >> Cases_on ‘a’ >> simp[bleval_def]
67QED
68
69Theorem tobl_correct:
70  bleval (tobl n T) = n /\
71  bleval (tobl n F) = n + 1
72Proof
73  Induct_on ‘n’ using numeralTheory.bit_induction >>
74  simp[tobl_def, bleval_def] >> rpt strip_tac
75  >- simp[arithmeticTheory.ALT_ZERO]
76  >- simp[arithmeticTheory.ALT_ZERO] >>
77  simp[SimpRHS, Once arithmeticTheory.BIT1] >>
78  simp[SimpRHS, Once arithmeticTheory.BIT2]
79QED
80
81Definition frombl_def:
82  frombl addedp [] = 0 /\
83  frombl T [T] = ZERO /\
84  frombl F [T] = BIT1 ZERO /\
85  frombl T (F::rest) = BIT1 (frombl T rest) /\
86  frombl F (F::rest) = BIT2 (frombl T rest) /\
87  frombl T (T::rest) = BIT2 (frombl T rest) /\
88  frombl F (T::rest) = BIT1 (frombl F rest)
89End
90
91Theorem frombl_correct:
92  bl <> [] /\ LAST bl ==>
93  frombl F bl = bleval bl /\
94  frombl T bl = bleval bl - 1
95Proof
96  Induct_on ‘bl’ >> simp[] >> Cases_on ‘bl’ >> gs[] >>
97  simp[frombl_def, bleval_def]
98  >- (simp[Once arithmeticTheory.BIT1, SimpLHS] >>
99      simp[arithmeticTheory.ALT_ZERO]) >>
100  rpt strip_tac >> gs[] >> rename [‘frombl _ (x::y::xs)’] >>
101  Cases_on ‘x’ >> simp[frombl_def, bleval_def]
102  >- simp[Once arithmeticTheory.BIT1, SimpLHS]
103  >- (simp[Once arithmeticTheory.BIT2, SimpLHS] >>
104      ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
105      simp[LASTbl_nonzero])
106  >- (simp[Once arithmeticTheory.BIT2, SimpLHS] >>
107      ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
108      simp[LASTbl_nonzero]) >>
109  simp[Once arithmeticTheory.BIT1, SimpLHS] >>
110  ‘0 < bleval (y::xs) ’ suffices_by simp[] >>
111  simp[LASTbl_nonzero]
112QED
113
114Definition fromBL_def:
115  fromBL bs =
116  if bs = [] then 0
117  else
118    let bs1 = REV bs []
119    in
120      case HD bs1 of
121        T => NUMERAL (frombl F bs)
122      | F =>
123          let
124            bs2 = dropWhile ((=) F) bs1 ;
125            bs3 = REV bs2 [] ;
126          in
127            if bs3 = [] then 0 else NUMERAL (frombl F bs3)
128End
129
130Theorem fromBL_correct:
131  fromBL bs = bleval bs
132Proof
133  rw[fromBL_def, bleval_def] >> gs[GSYM listTheory.REVERSE_REV]
134  >- (Cases_on ‘bs’ using listTheory.SNOC_CASES >>
135      gvs[listTheory.REVERSE_SNOC] >>
136      simp[arithmeticTheory.NUMERAL_DEF] >> irule (cj 1 frombl_correct) >>
137      simp[])
138  >- gs[listTheory.dropWhile_eq_nil, EVERYF_bleval0] >>
139  gs[listTheory.dropWhile_eq_nil, listTheory.EXISTS_MEM,
140     arithmeticTheory.NUMERAL_DEF] >>
141  pop_assum mp_tac >>
142  simp[Once listTheory.MEM_SPLIT_APPEND_last] >> rw[] >>
143  simp[listTheory.REVERSE_APPEND] >>
144  ‘EVERY ((=) F) (REVERSE sfx)’ by simp[listTheory.EVERY_MEM] >>
145  simp[listTheory.dropWhile_APPEND_EVERY, frombl_correct] >>
146  gs[EVERYF_suffix_bleval]
147QED
148
149(** Now use the code to develop bit list arithmetic and implement karatsuba
150    multiplication. The original idea is due to Magnus Myreen **)
151Definition add_aux_def:
152  add_aux [] bs F = bs /\
153  add_aux [] [] T = [T] /\
154  add_aux [] (F :: bs) T = T :: bs /\
155  add_aux [] (T :: bs) T = F :: (add_aux [] bs T) /\
156  add_aux bs [] F = bs /\
157  add_aux (F :: bs) [] T = T :: bs /\
158  add_aux (T :: bs) [] T = F :: (add_aux [] bs T) /\
159  add_aux (F :: bs1) (F :: bs2) T = T ::(add_aux bs1 bs2 F) /\
160  add_aux (F :: bs1) (F :: bs2) F = F :: (add_aux bs1 bs2 F) /\
161  add_aux (T :: bs1) (F :: bs2) F = T ::(add_aux bs1 bs2 F) /\
162  add_aux (T :: bs1) (F :: bs2) T = F :: (add_aux bs1 bs2 T) /\
163  add_aux (F :: bs1) (T :: bs2) T = F :: (add_aux bs1 bs2 T) /\
164  add_aux (F :: bs1) (T :: bs2) F = T ::(add_aux bs1 bs2 F) /\
165  add_aux (T :: bs1) (T :: bs2) T = T ::(add_aux bs1 bs2 T) /\
166  add_aux (T :: bs1) (T :: bs2) F = F :: (add_aux bs1 bs2 T)
167End
168
169Definition add_def:
170  add bs1 bs2 = add_aux bs1 bs2 F
171End
172
173Theorem add_aux_thm:
174  ! m n b.
175    bleval (add_aux m n b) = bleval m + bleval n + if b then 1 else 0
176Proof
177  ho_match_mp_tac add_aux_ind \\ fs [add_aux_def,bleval_def]
178QED
179
180Theorem add_thm:
181  bleval (add m n) = bleval m + bleval n
182Proof
183  fs [add_def,add_aux_thm]
184QED
185
186Definition divpow2_def:
187  divpow2 ([]:bool list) k = [] /\
188  divpow2 bs 0 = bs /\
189  divpow2 (b::bs) (SUC k) = divpow2 bs k
190End
191
192Theorem DIV_POW2:
193  ! x y. 0 < y ==> 2 * x DIV (2 * y) = x DIV y
194Proof
195  rpt strip_tac >> gs[GSYM DIV_DIV_DIV_MULT]
196  >> ‘2 * x = x * 2’ by gs[]
197  >> pop_assum $ rewrite_tac o single
198  >> gs[MULT_DIV]
199QED
200
201Theorem divpow2_thm:
202  ! x k. bleval (divpow2 x k) = bleval x DIV (2 ** k)
203Proof
204  ho_match_mp_tac divpow2_ind >> gs[divpow2_def, bleval_def, ZERO_DIV]
205  >> rpt strip_tac
206  >> reverse $ Cases_on ‘b’ >> gs[bleval_def]
207  >- (
208    ‘2 ** SUC k = 2 * 2 ** k’ by gs[EXP]
209    >> ‘2 * bleval x = bleval x * 2’ by gs[]
210    >> pop_assum $ rewrite_tac o single
211    >> gs[MULT_DIV, DIV_POW2])
212  >> ‘2 ** SUC k = 2 * 2 ** k’ by gs[EXP]
213  >> ‘2 * bleval x = bleval x * 2’ by gs[]
214  >> gs[GSYM DIV_DIV_DIV_MULT]
215  >> ‘2 * bleval x = bleval x * 2’ by gs[]
216  >> pop_assum $ rewrite_tac o single
217  >> gs[DIV_MULT]
218QED
219
220(** TODO: Try a tail recursive version that drops leading 0s **)
221Definition modpow2_def:
222  modpow2 ([]:bool list) k = [] /\
223  modpow2 bs 0 = [] /\
224  modpow2 (b::bs) (SUC k) = b :: (modpow2 bs k)
225End
226
227Theorem bleval_less:
228  ! bs. bleval bs < 2 ** (LENGTH bs)
229Proof
230  ho_match_mp_tac bleval_ind >> gs[bleval_def] >> rw[]
231  >> irule LESS_LESS_EQ_TRANS >> qexists_tac ‘2 * 2 ** LENGTH bs’
232  >> conj_tac >> gs[EXP]
233QED
234
235Theorem bleval_less_large:
236  LENGTH bs <= k ==> bleval bs < 2 ** k
237Proof
238  rpt strip_tac >> irule LESS_LESS_EQ_TRANS
239  >> qexists_tac ‘2 ** LENGTH bs’ >> gs[bleval_less]
240QED
241
242Theorem modpow2_thm:
243  ! x k. bleval (modpow2 x k) = bleval x MOD (2 ** k)
244Proof
245  ho_match_mp_tac modpow2_ind >> gs[modpow2_def, bleval_def, ZERO_MOD]
246  >> rpt strip_tac >> reverse $ Cases_on ‘b’ >> gs[bleval_def]
247  >- (
248    Cases_on ‘LENGTH x < k’ >> gs[NOT_LESS]
249    >- (
250      ‘bleval x MOD 2 ** k = bleval x’ by gs[LESS_MOD, bleval_less_large]
251      >> pop_assum $ rewrite_tac o single
252      >> ‘2 * bleval x = bleval (F :: x)’ by gs[bleval_def]
253      >> pop_assum $ rewrite_tac o single
254      >> ‘bleval (F::x) MOD 2 ** SUC k = bleval (F::x)’
255        by gs[LESS_MOD, bleval_less_large]
256      >> pop_assum $ rewrite_tac o single)
257    >> gs[quantHeuristicsTheory.LENGTH_LE_NUM, bleval_APPEND]
258    >> ‘bleval l1 MOD 2 ** k = bleval l1’
259        by (gs[LESS_MOD] >> rpt VAR_EQ_TAC >> gs[bleval_less])
260    >> first_assum $ once_rewrite_tac o single
261    >> gs[LEFT_ADD_DISTRIB]
262    >> ‘2 * (bleval l2 * 2 ** k) = bleval l2 * 2 ** SUC k’ by gs[EXP]
263    >> pop_assum $ once_rewrite_tac o single
264    >> gs[]
265    >> ‘2 * bleval l1 = bleval (F :: l1)’ by gs[bleval_def]
266    >> pop_assum $ rewrite_tac o single
267    >> gs[bleval_less_large])
268  >> Cases_on ‘LENGTH x < k’ >> gs[NOT_LESS]
269  >- (
270    ‘bleval x MOD 2 ** k = bleval x’ by gs[LESS_MOD, bleval_less_large]
271    >> pop_assum $ rewrite_tac o single
272    >> ‘2 * bleval x + 1 = bleval (T :: x)’ by gs[bleval_def]
273    >> pop_assum $ rewrite_tac o single
274    >> ‘bleval (T::x) MOD 2 ** SUC k = bleval (T::x)’
275        by gs[LESS_MOD, bleval_less_large]
276    >> pop_assum $ rewrite_tac o single)
277  >> gs[quantHeuristicsTheory.LENGTH_LE_NUM, bleval_APPEND]
278  >> ‘bleval l1 MOD 2 ** k = bleval l1’
279      by (gs[LESS_MOD] >> rpt VAR_EQ_TAC >> gs[bleval_less])
280  >> first_assum $ once_rewrite_tac o single
281  >> gs[LEFT_ADD_DISTRIB]
282  >> ‘2 * (bleval l2 * 2 ** k) = bleval l2 * 2 ** SUC k’ by gs[EXP]
283  >> pop_assum $ once_rewrite_tac o single
284  >> gs[]
285  >> ‘2 * bleval l1 + 1 = bleval (T :: l1)’ by gs[bleval_def]
286  >> pop_assum $ rewrite_tac o single
287  >> gs[bleval_less_large]
288QED
289
290Definition mul_def:
291  mul [] _ = [] /\
292  mul (T::bs) bs2 = add bs2 (mul bs (F::bs2)) /\
293  mul (F::bs) bs2 = mul bs (F::bs2)
294End
295
296Theorem mul_thm:
297  ! x y. bleval (mul x y) = bleval x * bleval y
298Proof
299  ho_match_mp_tac mul_ind >> gs[mul_def, bleval_def, add_thm]
300QED
301
302Definition mulpow2_def:
303  mulpow2 [] _ = [] /\
304  mulpow2 bs 0 = bs /\
305  mulpow2 bs (SUC k) = F::(mulpow2 bs k)
306End
307
308Theorem mulpow2_thm:
309  ! bs k. bleval (mulpow2 bs k) = bleval bs * 2 ** k
310Proof
311  ho_match_mp_tac mulpow2_ind >> gs[mulpow2_def, bleval_def, EXP]
312QED
313
314Definition lte_aux_def:
315  lte_aux [] [] = T /\
316  lte_aux (F::bs1) (T::bs2) = T /\
317  lte_aux (T::bs1) (F::bs2) = F /\
318  lte_aux (T::bs1) (T::bs2) = lte_aux bs1 bs2 /\
319  lte_aux (F::bs1) (F::bs2) = lte_aux bs1 bs2 /\
320  lte_aux _ _ = F
321End
322
323Theorem lte_aux_thm:
324  ! bs1 bs2.
325    LENGTH bs1 = LENGTH bs2 ==>
326    (lte_aux bs1 bs2 <=> bleval (REVERSE bs1) <= bleval (REVERSE bs2))
327Proof
328  ho_match_mp_tac lte_aux_ind >> rpt strip_tac
329  >> gs[lte_aux_def, bleval_def, bleval_APPEND]
330  >- (
331    ‘bleval (REVERSE bs1) <= 2 ** LENGTH (REVERSE bs1)’
332    by gs[LESS_OR_EQ, bleval_less]
333    >> ‘LENGTH (REVERSE bs1) = LENGTH bs2’ by gs[LENGTH_REVERSE]
334    >> irule LESS_EQ_TRANS
335    >> qexists_tac ‘2 ** LENGTH bs2’ >> gs[])
336  >> gs[NOT_LEQ]
337  >> ‘bleval (REVERSE bs2) < 2 ** LENGTH (REVERSE bs2)’
338    by gs[bleval_less]
339  >> ‘LENGTH (REVERSE bs2) = LENGTH bs2’ by gs[LENGTH_REVERSE]
340  >> ‘SUC (bleval (REVERSE bs2)) <= 2 ** LENGTH (REVERSE bs2)’
341    by gs[]
342  >> irule LESS_EQ_TRANS
343  >> qexists_tac ‘2 ** LENGTH bs2’ >> gs[]
344QED
345
346Definition zeroPad_def:
347  zeroPad [] [] = ([], []) /\
348  zeroPad (b::bs1) [] =
349    (let (bs1pad, bs2pad) = zeroPad bs1 [] in
350      (b::bs1pad, F::bs2pad)) /\
351  zeroPad [] (b::bs2) =
352    (let (bs1pad, bs2pad) = zeroPad [] bs2 in
353       (F::bs1pad, b::bs2pad)) /\
354  zeroPad (b1::bs1) (b2::bs2) =
355    (let (bs1pad, bs2pad) = zeroPad bs1 bs2 in
356       (b1::bs1pad, b2::bs2pad))
357End
358
359Theorem zeroPad_thm:
360  ! bs1 bs2 bs1pad bs2pad.
361    zeroPad bs1 bs2 = (bs1pad, bs2pad) ==>
362    bleval bs1 = bleval bs1pad /\ bleval bs2 = bleval bs2pad /\
363    LENGTH bs1pad = LENGTH bs2pad
364Proof
365  ho_match_mp_tac zeroPad_ind >> rpt strip_tac
366  >> gs[zeroPad_def, bleval_def, CaseEq"prod"]
367  >- (
368    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
369    >> Cases_on ‘b’ >> gs[bleval_def]
370    >> rpt VAR_EQ_TAC >> gs[bleval_def])
371  >- (
372    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
373    >> rpt VAR_EQ_TAC >> gs[bleval_def])
374  >- (
375    Cases_on ‘zeroPad bs1 []’ >> gs[zeroPad_def, bleval_def]
376    >> rpt VAR_EQ_TAC >> gs[])
377  >- (
378    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
379    >> Cases_on ‘b’ >> gs[bleval_def]
380    >> rpt VAR_EQ_TAC >> gs[bleval_def])
381  >- (
382    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
383    >> Cases_on ‘b’ >> gs[bleval_def]
384    >> rpt VAR_EQ_TAC >> gs[bleval_def])
385  >- (
386    Cases_on ‘zeroPad [] bs2’ >> gs[zeroPad_def, bleval_def]
387    >> rpt VAR_EQ_TAC >> gs[])
388  >- (
389    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
390    >> Cases_on ‘b1’ >> gs[bleval_def]
391    >> rpt VAR_EQ_TAC >> gs[bleval_def])
392  >- (
393    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
394    >> Cases_on ‘b2’ >> gs[bleval_def]
395    >> rpt VAR_EQ_TAC >> gs[bleval_def])
396  >- (
397    Cases_on ‘zeroPad bs1 bs2’ >> gs[zeroPad_def, bleval_def]
398    >> rpt VAR_EQ_TAC >> gs[])
399QED
400
401Definition lte_def:
402  lte bs1 bs2 =
403  let (bs1pad, bs2pad) = zeroPad bs1 bs2 in
404    lte_aux (REV bs1pad []) (REV bs2pad [])
405End
406
407Theorem lte_thm:
408  ! bs1 bs2. lte bs1 bs2 <=> bleval bs1 <= bleval bs2
409Proof
410  rpt strip_tac >> gs[lte_def]
411  >> Cases_on ‘zeroPad bs1 bs2’ >> imp_res_tac zeroPad_thm
412  >> ‘LENGTH (REVERSE q) = LENGTH (REVERSE r)’ by gs[LENGTH_REVERSE]
413  >> first_assum $ mp_then Any mp_tac lte_aux_thm
414  >> gs[GSYM REVERSE_REV, REVERSE_REVERSE]
415QED
416
417Definition sub_aux_def:
418  sub_aux [] _ _ = [] /\
419  sub_aux (F :: bs1) [] T = T :: (sub_aux bs1 [] T) /\
420  sub_aux (T :: bs1) [] T = F :: bs1 /\
421  sub_aux (F :: bs1) [] F = F :: bs1 /\
422  sub_aux (T :: bs1) [] F = T :: bs1 /\
423  sub_aux (F :: bs1) (F :: bs2) T = T :: (sub_aux bs1 bs2 T) /\
424  sub_aux (F :: bs1) (F :: bs2) F = F :: (sub_aux bs1 bs2 F) /\
425  sub_aux (F :: bs1) (T :: bs2) T = F :: (sub_aux bs1 bs2 T) /\
426  sub_aux (F :: bs1) (T :: bs2) F = T :: (sub_aux bs1 bs2 T) /\
427  sub_aux (T :: bs1) (F :: bs2) T = F :: (sub_aux bs1 bs2 F) /\
428  sub_aux (T :: bs1) (F :: bs2) F = T :: (sub_aux bs1 bs2 F) /\
429  sub_aux (T :: bs1) (T :: bs2) T = T :: (sub_aux bs1 bs2 T) /\
430  sub_aux (T :: bs1) (T :: bs2) F = F :: (sub_aux bs1 bs2 F)
431End
432
433Definition sub_def:
434  sub bs1 bs2 = if lte bs2 bs1 then sub_aux bs1 bs2 F else []
435End
436
437Theorem sub_aux_thm:
438  ! bs1 bs2 b.
439    (bleval bs2 + if b then 1 else 0) <= bleval bs1 ==>
440    bleval (sub_aux bs1 bs2 b) = bleval bs1 - (bleval bs2 + if b then 1 else 0)
441Proof
442  ho_match_mp_tac sub_aux_ind >> rpt conj_tac >> rpt strip_tac
443  >> gs[sub_aux_def, bleval_def, LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
444  >- (
445    TOP_CASE_TAC >> gs[]
446    >> ‘bleval bs1 = 1’ by (Cases_on ‘bleval bs1’ >> gs[])
447    >> gs[])
448  >- (
449    COND_CASES_TAC >> gs[]
450    >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
451    >> pop_assum $ once_rewrite_tac o single >> gs[])
452  >- (
453    COND_CASES_TAC >> gs[]
454    >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
455    >> pop_assum $ once_rewrite_tac o single >> gs[])
456  >- (
457    COND_CASES_TAC >> gs[]
458    >> ‘bleval bs2 <= bleval bs1’ by gs[]
459    >> ‘bleval bs2 = bleval bs1’ by gs[]
460    >> pop_assum $ once_rewrite_tac o single >> gs[])
461  >> COND_CASES_TAC >> gs[]
462  >> ‘bleval bs1 = bleval bs2 + 1’ by gs[]
463  >> pop_assum $ once_rewrite_tac o single >> gs[]
464QED
465
466Theorem sub_thm:
467  ! m n. bleval (sub m n) = bleval m - bleval n
468Proof
469  rw[sub_def, lte_thm, sub_aux_thm, bleval_def, SUB_EQ_0, NOT_LEQ]
470QED
471
472Theorem karatsuba_num:
473  ! d x y.
474    0 < d ==>
475    x * y =
476      let x1 = x DIV d in
477      let x0 = x MOD d in
478      let y1 = y DIV d in
479      let y0 = y MOD d in
480      let z0 = x0 * y0 in
481      let z2 = x1 * y1 in
482      let z1a = x1 + x0 in
483      let z1b = y1 + y0 in
484      let z1 = z1a * z1b in
485      let z1 = z1 - z2 - z0 in
486        (z2 * d + z1) * d + z0
487Proof
488  rpt strip_tac
489  \\ irule EQ_TRANS
490  \\ qexists_tac ‘(x DIV d * d + x MOD d) * (y DIV d * d + y MOD d)’
491  \\ conj_tac THEN1 metis_tac [DIVISION]
492  \\ fs [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB]
493QED
494
495Theorem karatsuba_bit:
496  ! x y.
497    bleval (mul x y) = bleval (
498    let d = (fromBL
499            (divpow2
500             (add (divpow2 (tobl (LENGTH x) F) 1)
501              (divpow2 (tobl (LENGTH y) F) 1)) 1)) + 1 in
502      let x1 = divpow2 x d in
503      let x0 = modpow2 x d in
504      let y1 = divpow2 y d in
505      let y0 = modpow2 y d in
506      let z0 = mul x0 y0 in
507      let z2 = mul x1 y1 in
508      let z1a = add x1 x0 in
509      let z1b = add y1 y0 in
510      let z1Mul = mul z1a z1b in
511      let z1 = sub (sub z1Mul z2) z0 in
512        add (mulpow2 (add (mulpow2 z2 d) z1) d) z0)
513Proof
514  rpt strip_tac >> rewrite_tac [mul_thm]
515  >> qmatch_goalsub_abbrev_tac ‘fromBL dVal’
516  >> qspecl_then [‘2 ** (fromBL dVal + 1)’, ‘bleval x’, ‘bleval y’] mp_tac karatsuba_num
517  >> impl_tac
518  >- (unabbrev_all_tac >> gs[fromBL_correct, divpow2_thm, add_thm])
519  >> disch_then $ rewrite_tac o single
520  >> unabbrev_all_tac
521  >> gs[divpow2_thm, modpow2_thm, add_thm, mul_thm, mulpow2_thm, sub_thm, fromBL_correct]
522QED
523
524(** Infrastructural Theorems for lib implementation **)
525Theorem mk_frac_thm[unlisted]:
526  !(x:real). x = x / 1
527Proof
528  gs[]
529QED
530
531Theorem id_thm[unlisted]:
532  ! (x:real). x = x
533Proof
534  gs[]
535QED
536
537Theorem mul_frac_thm[unlisted]:
538  ! a b c (d:real). (a / b) * (c / d) = (a * c) / (b * d)
539Proof
540  rpt gen_tac >> rewrite_tac [real_div, GSYM REAL_MUL_ASSOC]
541  >> ‘inv b * (c * inv d) = c * (inv b * inv d)’ by (gs[REAL_MUL_ASSOC] >> gs[REAL_MUL_COMM])
542  >> pop_assum $ once_rewrite_tac o single
543  >> gs[REAL_INV_MUL']
544QED
545