1 module type Arith_hash_sig =
6 val const_array : term array
7 val def_array: thm array
8 val def_thm_array: thm array
9 val mk_numeral_hash : num -> term
10 val mk_numeral_array : num -> term
11 val mk_small_numeral_array : int -> term
12 val mk_int64_numeral_array : int64 -> term
13 val raw_dest_hash : term -> num
14 val dest_numeral_hash : term -> num
15 val dest_numeral64_hash : term -> int64
16 val NUMERAL_TO_NUM_CONV : term -> thm
17 val NUM_TO_NUMERAL_CONV : term -> thm
19 val raw_suc_conv_hash : term -> thm
20 val NUM_SUC_HASH_CONV : term -> thm
22 val raw_eq0_hash_conv : term -> thm
23 val NUM_EQ0_HASH_CONV : term -> thm
25 val raw_pre_hash_conv : term -> thm
26 val NUM_PRE_HASH_CONV : term -> thm
28 val raw_gt0_hash_conv : term -> thm
29 val NUM_GT0_HASH_CONV : term -> thm
31 val raw_lt_hash_conv : term -> thm
32 val raw_le_hash_conv : term -> thm
33 val NUM_LT_HASH_CONV : term -> thm
34 val NUM_LE_HASH_CONV : term -> thm
36 val raw_add_conv_hash : term -> thm
37 val NUM_ADD_HASH_CONV : term -> thm
39 val raw_sub_hash_conv : term -> thm
40 val raw_sub_and_le_hash_conv : term -> term -> thm * thm
41 val NUM_SUB_HASH_CONV : term -> thm
43 val raw_mul_conv_hash : term -> thm
44 val NUM_MULT_HASH_CONV : term -> thm
46 val raw_div_hash_conv : term -> thm
47 val NUM_DIV_HASH_CONV : term -> thm
49 val raw_even_hash_conv : term -> thm
50 val raw_odd_hash_conv : term -> thm
51 val NUM_EVEN_HASH_CONV : term -> thm
52 val NUM_ODD_HASH_CONV : term -> thm
56 needs "../formal_lp/arith/misc.hl";;
57 needs "../formal_lp/arith/arith_options.hl";;
59 module Arith_hash : Arith_hash_sig = struct
70 if n > 1 then log2b (n lsr 1) + 1 else 0;;
73 let bits = log2b base;;
78 let maximum = 1 lsl bits;;
79 let mask = maximum - 1;;
81 (* Check that the base is correct *)
82 if maximum <> base then
83 failwith "arith_hash: base is not a power of 2"
88 (* Generate definitions and constants *)
90 let num_type = `:num`;;
91 let fnum_type = `:num->num`;;
93 let numeral_const = `NUMERAL` and
95 bit0_const = `BIT0` and
96 bit1_const = `BIT1` and
100 let m_var_num = `m:num` and
101 n_var_num = `n:num` and
102 t_var_num = `t:num` and
103 r_var_num = `r:num` and
104 p_var_num = `p:num` and
105 q_var_num = `q:num`;;
107 let suc_const = `SUC` and
108 plus_op_num = `(+):num->num->num` and
109 minus_op_num = `(-):num->num->num` and
110 mul_op_num = `( * ):num->num->num` and
111 div_op_num = `(DIV):num->num->num` and
112 le_op_num = `(<=):num->num->bool` and
113 lt_op_num = `(<):num->num->bool`;;
116 let plus_op_real = `(+):real->real->real` and
117 mul_op_real = `( * ):real->real->real`;;
122 let rec decode n level =
123 if (level >= k) then ""
124 else if (n land 1 = 1) then "1"^decode (n lsr 1) (level + 1)
125 else "0"^decode (n lsr 1) (level + 1) in
129 let rec create_bit_term n k =
130 if (k <= 0) then n_var_num
132 if (n land 1 = 1) then bit1_const else bit0_const in
133 mk_comb (bit, create_bit_term (n lsr 1) (k - 1));;
137 let names_array = Array.init maximum (fun i -> "B"^(string_of_int i));;
142 let num_name = "NUM"^(string_of_int bits);;
143 let num_def = new_basic_definition (mk_eq(mk_var(num_name, fnum_type), numeral_const));;
144 let num_const = mk_const(num_name, []);;
145 let num_def_sym = SYM num_def;;
146 let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
147 REWRITE_TAC[num_def; NUMERAL]);;
150 let mk_bit_definition i =
151 let lhs = mk_var (names_array.(i), fnum_type) in
152 let rhs = mk_abs (n_var_num, create_bit_term i bits) in
153 new_basic_definition (mk_eq(lhs, rhs));;
156 let def_basic_array = Array.init maximum mk_bit_definition;;
157 let def_array = Array.init maximum (fun i ->
158 let basic = def_basic_array.(i) in
159 let th1 = AP_THM basic n_var_num in
160 TRANS th1 (BETA (rand (concl th1))));;
161 let def_table = Hashtbl.create maximum;;
162 let def_basic_table = Hashtbl.create maximum;;
164 for i = 0 to maximum - 1 do
165 let _ = Hashtbl.add def_table names_array.(i) def_array.(i) in
166 Hashtbl.add def_basic_table names_array.(i) def_basic_array.(i)
173 let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));;
175 let b0_def = def_array.(0);;
176 let b0_const = const_array.(0);;
177 let b0_name = names_array.(0);;
179 let max_const = mk_small_numeral maximum;;
183 (* Alternative definition of B_i *)
185 let ADD_0_n = prove(`_0 + n = n`,
186 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
187 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
188 let ADD_n_0 = prove(`n + _0 = n`,
189 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
190 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
192 (* B_i(n) = i + B_0(n) *)
194 let bin = mk_comb(const_array.(i), n_var_num) in
195 let bi0 = mk_comb(const_array.(i), zero_const) in
196 let b0n = mk_comb(const_array.(0), n_var_num) in
197 let rhs = mk_binop plus_op_num bi0 b0n in
198 prove(mk_eq(bin, rhs), REWRITE_TAC[def_array.(i); def_array.(0)] THEN
199 REWRITE_TAC[ARITH_ZERO; ARITH_ADD; ADD_0_n; ADD_n_0]);;
201 let def_thm_array = Array.init maximum def_thm;;
204 let B0_0 = prove(mk_eq(mk_comb(b0_const, zero_const), zero_const),
205 REWRITE_TAC[b0_def; ARITH_ZERO]);;
207 let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num),
208 mk_binop mul_op_num max_const n_var_num),
209 REWRITE_TAC[b0_def] THEN
210 GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [BIT0] THEN
217 (******************************)
219 (* mk_numeral and dest_numeral *)
224 let mk_table = Hashtbl.create maximum;;
226 for i = 0 to maximum - 1 do
227 Hashtbl.add mk_table (Int i) const_array.(i)
232 let max_num = Int maximum;;
233 let mask64 = Int64.of_int mask;;
235 let mk_numeral_hash =
240 let m = mod_num n max_num in
241 let bit = Hashtbl.find mk_table m in
242 mk_comb(bit, mk_num(quo_num n max_num)) in
243 fun n -> if n </ num_0 then failwith "mk_numeral_hash: negative argument"
244 else mk_comb(num_const, mk_num n);;
247 let mk_numeral_array =
252 let m = Num.int_of_num (mod_num n max_num) in
253 let bit = const_array.(m) in
254 mk_comb(bit, mk_num(quo_num n max_num)) in
255 fun n -> if n </ num_0 then failwith "mk_numeral_array: negative argument"
256 else mk_comb(num_const, mk_num n);;
259 let mk_small_numeral_array =
261 if (n = 0) then zero_const
263 let m = n land mask in
264 let bit = const_array.(m) in
265 mk_comb(bit, mk_num(n lsr bits)) in
266 fun n -> if n < 0 then failwith "mk_small_numeral_array: negative argument"
267 else mk_comb (num_const, mk_num n);;
270 let mk_int64_numeral_array =
272 if (n = 0L) then zero_const
274 let m = Int64.to_int (Int64.logand n mask64) in
275 let bit = const_array.(m) in
276 mk_comb(bit, mk_num(Int64.shift_right n bits)) in
277 fun n -> if n < 0L then failwith "mk_int64_numeral_array: negative argument"
278 else mk_comb (num_const, mk_num n);;
283 test 10000 mk_numeral_hash (Int 65535);; (* 0.736 *)
284 test 10000 mk_numeral_array (Int 65535);; (* 0.728 *)
285 test 100000 mk_small_numeral_array 65535;; (* 0.216 *)
286 test 100000 mk_int64_numeral_array 65535L;; (* 0.264 *)
288 test 1000 mk_numeral_array (num_of_string "9111111111111111");; (* 0.288 *)
289 test 1000 mk_int64_numeral_array 9111111111111111L;; (* 0.012 *)
296 let dest_table_num = Hashtbl.create maximum;;
298 for i = 0 to maximum - 1 do
299 Hashtbl.add dest_table_num names_array.(i) (Int i)
303 let dest_table_int64 = Hashtbl.create maximum;;
305 for i = 0 to maximum - 1 do
306 Hashtbl.add dest_table_int64 names_array.(i) (Int64.of_int i)
313 let max_num = Int maximum;;
316 let rec raw_dest_hash tm =
317 if tm = zero_const then
320 let l, r = dest_comb tm in
321 let n = max_num */ raw_dest_hash r in
322 let cn = fst(dest_const l) in
323 n +/ (Hashtbl.find dest_table_num cn);;
326 let dest_numeral_hash tm = raw_dest_hash (rand tm);;
329 let dest_numeral64_hash tm =
330 let rec dest_num tm =
331 if (tm = zero_const) then
334 let l, r = dest_comb tm in
335 let n = Int64.shift_left (dest_num r) bits in
336 let cn = fst(dest_const l) in
337 Int64.add n (Hashtbl.find dest_table_int64 cn) in
343 test 100000 dest_numeral_hash (mk_numeral_array (Int 11111111));; (* 5: 0.572 *)
344 test 100000 dest_numeral64_hash (mk_numeral_array (Int 11111111));; (* 5: 0.264 *)
349 (******************************)
351 (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *)
354 let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));;
356 let th_part_num_conv = Array.init maximum
357 (fun i -> REWRITE_RULE[ARITH_ZERO] (INST [zero_const, n_var_num] th_num_conv.(i)));;
359 th_part_num_conv.(0) <- REFL zero_const;;
363 let NUMERAL_TO_NUM_CONV tm =
364 let rec find_match tm i level =
365 if (level >= bits) then
366 if (tm = zero_const) then
367 INST [zero_const, n_var_num] th_num_conv.(i)
369 let th = INST[tm, n_var_num] th_num_conv.(i) in
370 let ltm, rtm = dest_comb (rand (concl th)) in
371 TRANS th (AP_TERM ltm (find_match rtm 0 0))
372 else if (tm = zero_const) then
373 INST [zero_const, n_var_num] th_part_num_conv.(i)
375 let btm, ntm = dest_comb tm in
376 let cn = fst(dest_const btm) in
377 if (cn = "BIT0") then
378 find_match ntm i (level + 1)
379 else if (cn = "BIT1") then
380 find_match ntm (i lor (1 lsl level)) (level + 1)
381 else failwith("NUMERAL_TO_NUM_CONV") in
382 let ltm, rtm = dest_comb tm in
383 if (ltm = numeral_const) then
384 MK_COMB (num_def_sym, find_match rtm 0 0)
385 else failwith("NUMERAL_TO_NUM_CONV");;
388 let replace_numerals = rand o concl o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
389 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;
390 (* NUM_TO_NUMERAL_CONV *)
393 let th_part_num_table = Hashtbl.create maximum;;
395 for i = 1 to maximum - 1 do
396 Hashtbl.add th_part_num_table names_array.(i) (SYM th_part_num_conv.(i))
401 let NUM_TO_NUMERAL_CONV tm =
402 let rec bits_to_num tm =
403 if (tm = zero_const) then
406 let btm, ntm = dest_comb tm in
407 let cn = fst(dest_const btm) in
408 if ntm = zero_const then
409 Hashtbl.find th_part_num_table cn
411 let th0 = Hashtbl.find def_basic_table cn in
412 let th1 = bits_to_num ntm in
413 let th = MK_COMB(th0, th1) in
414 TRANS th (BETA_CONV (rand(concl th))) in
415 let ltm, rtm = dest_comb tm in
416 if (ltm = num_const) then
417 MK_COMB(num_def, bits_to_num rtm)
419 failwith("NUM_TO_NUMERAL_CONV");;
423 (*************************)
427 let suc_const = `SUC`;;
431 let SUC_NUM = prove(mk_eq(mk_comb(suc_const, mk_comb (num_const, n_var_num)),
432 mk_comb(num_const, mk_comb (suc_const, n_var_num))),
433 REWRITE_TAC[num_def; NUMERAL]);;
435 let SUC_0 = prove(mk_eq(`SUC _0`, mk_comb (const_array.(1), zero_const)),
436 REWRITE_TAC[def_array.(1); ARITH_SUC; ARITH_ZERO]);;
440 let cflag = (i + 1 >= maximum) in
441 let suc = if (cflag) then 0 else i + 1 in
442 let lhs = mk_comb(suc_const, (mk_comb (const_array.(i), n_var_num))) in
443 let rhs = mk_comb(const_array.(suc),
444 if (cflag) then mk_comb(suc_const, n_var_num) else n_var_num) in
445 let proof = REWRITE_TAC [def_array.(i); def_array.(suc); ARITH_SUC] in
446 prove(mk_eq(lhs, rhs), proof);;
449 let th_suc_array = Array.init maximum suc_th;;
451 let th_suc_table = Hashtbl.create maximum;;
453 for i = 0 to maximum - 1 do
454 Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i)
457 let SUC_MAX = th_suc_array.(maximum - 1);;
458 let bit_max_name = names_array.(maximum - 1);;
463 let rec raw_suc_conv_hash tm =
465 if (otm = zero_const) then
468 let btm, ntm = dest_comb otm in
469 let cn = fst(dest_const btm) in
470 if (cn = bit_max_name) then
471 let th = INST [ntm, n_var_num] SUC_MAX in
472 let ltm, rtm = dest_comb(rand(concl th)) in
473 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm))
475 INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);;
479 let NUM_SUC_HASH_CONV tm =
480 let ntm = rand (rand tm) in
481 let th = INST [ntm, n_var_num] SUC_NUM in
482 let lhs, rhs = dest_eq(concl th) in
483 if (lhs <> tm) then failwith("NUM_SUC_HASH_CONV")
485 let ltm, rtm = dest_comb rhs in
486 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));;
493 let x = mk_comb(suc_const, mk_small_numeral_array 65535);;
494 test 50000 NUM_SUC_HASH_CONV x;; (* 5: 0.980 *)
498 (**************************************)
502 let EQ_0_NUM = prove(mk_eq(mk_eq(mk_comb(num_const, n_var_num), `_0`), `n = _0`),
503 REWRITE_TAC[num_def; NUMERAL]);;
505 let EQ_B0_0 = prove(mk_eq(mk_eq(mk_comb(b0_const, n_var_num), `_0`), `n = _0`),
506 REWRITE_TAC[b0_def; ARITH_EQ]);;
508 let EQ_0_0 = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH_EQ]);;
511 let concl = mk_eq(mk_eq(mk_comb(const_array.(i), n_var_num), zero_const), false_const) in
512 prove(concl, REWRITE_TAC[def_array.(i); ARITH_EQ]);;
516 let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);;
518 let th_eq0_table = Hashtbl.create maximum;;
520 for i = 0 to maximum - 1 do
521 Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i)
526 let rec raw_eq0_hash_conv rtm =
527 if (rtm = zero_const) then
530 let b_tm, n_tm = dest_comb rtm in
531 let cn = (fst o dest_const) b_tm in
532 if (cn = b0_name) then
533 let th0 = INST[n_tm, n_var_num] EQ_B0_0 in
534 let th1 = raw_eq0_hash_conv n_tm in
537 INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);;
541 let NUM_EQ0_HASH_CONV rtm =
542 let n_tm = rand rtm in
543 let th = INST [n_tm, n_var_num] EQ_0_NUM in
544 TRANS th (raw_eq0_hash_conv n_tm);;
548 (**************************************)
552 let pre_const = `PRE`;;
556 let PRE_NUM = prove(mk_eq(mk_comb(pre_const, mk_comb (num_const, n_var_num)),
557 mk_comb(num_const, mk_comb (pre_const, n_var_num))),
558 REWRITE_TAC[num_def; NUMERAL]);;
561 let PRE_0 = prove(`PRE _0 = _0`,
562 MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
564 let PRE_B1_0 = prove(mk_eq(mk_comb(`PRE`, mk_comb(const_array.(1), `_0`)), `_0`),
565 REWRITE_TAC[def_array.(1); ARITH_PRE; ARITH_EQ]);;
567 let PRE_B0_n0 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> T`,
568 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), `_0`)),
569 REWRITE_TAC[def_array.(0); ARITH_PRE; ARITH_EQ] THEN SIMP_TAC[]);;
572 let PRE_B0_n1 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> F`,
573 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)),
574 mk_comb(const_array.(maximum - 1), `PRE n`))),
575 REWRITE_TAC[def_array.(0); def_array.(maximum - 1); ARITH_PRE; ARITH_EQ] THEN SIMP_TAC[]);;
581 let lhs = mk_comb(pre_const, (mk_comb (const_array.(i), n_var_num))) in
582 let rhs = mk_comb(const_array.(pre), n_var_num) in
583 let proof = REWRITE_TAC [def_array.(i); def_array.(pre); ARITH_PRE; ARITH_EQ] in
584 prove(mk_eq(lhs, rhs), proof);;
587 let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);;
589 let th_pre_table = Hashtbl.create maximum;;
591 for i = 0 to maximum - 1 do
592 Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i)
597 let b1_name = names_array.(1);;
598 let b1_pre_thm = th_pre_array.(1);;
600 let rec raw_pre_hash_conv tm =
602 if (otm = zero_const) then
605 let btm, ntm = dest_comb otm in
606 let cn = fst(dest_const btm) in
607 if (cn = b0_name) then
608 let n_th = raw_eq0_hash_conv ntm in
609 if (rand(concl n_th) = false_const) then
610 let th0 = INST[ntm, n_var_num] PRE_B0_n1 in
611 let th1 = MY_PROVE_HYP n_th th0 in
612 let ltm, rtm = dest_comb(rand(concl th1)) in
613 let th2 = raw_pre_hash_conv rtm in
614 TRANS th1 (AP_TERM ltm th2)
616 let th = INST[ntm, n_var_num] PRE_B0_n0 in
619 if (cn = b1_name) then
620 if (ntm = zero_const) then
623 INST[ntm, n_var_num] b1_pre_thm
625 INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);;
629 let NUM_PRE_HASH_CONV tm =
630 let ntm = rand (rand tm) in
631 let th = INST [ntm, n_var_num] PRE_NUM in
632 let lhs, rhs = dest_eq(concl th) in
633 if (lhs <> tm) then failwith("NUM_PRE_HASH_CONV")
635 let ltm, rtm = dest_comb rhs in
636 TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));;
640 let x = mk_comb(pre_const, mk_small_numeral_array 65535);;
642 test 50000 NUM_PRE_HASH_CONV x;;
643 let x = mk_comb(pre_const, mk_small_numeral_array 65536);;
645 test 50000 NUM_PRE_HASH_CONV x;;
651 (**************************************)
656 let gt0_table = Hashtbl.create maximum;;
658 let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
660 let gt0_0 = prove(`_0 < _0 <=> F`, REWRITE_TAC[ARITH_LT]);;
661 let gt0_b0 = prove(mk_eq (mk_binop lt_op_num zero_const (mk_comb(b0_const, n_var_num)), `_0 < n`),
662 REWRITE_TAC[b0_def; ARITH_LT]);;
667 let bi = const_array.(i) in
668 let concl = mk_eq (mk_binop lt_op_num zero_const (mk_comb(bi, n_var_num)), truth_const) in
669 let proof = REWRITE_TAC[def_array.(i); ARITH_LT] in
670 prove(concl, proof);;
673 for i = 1 to maximum - 1 do
674 Hashtbl.add gt0_table names_array.(i) (gt0_th i)
678 let rec raw_gt0_hash_conv rtm =
679 if (rtm = zero_const) then
682 let b_tm, n_tm = dest_comb rtm in
683 let cn = (fst o dest_const) b_tm in
684 if (cn = b0_name) then
685 let th0 = INST[n_tm, n_var_num] gt0_b0 in
686 let th1 = raw_gt0_hash_conv n_tm in
689 INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);;
693 let NUM_GT0_HASH_CONV rtm =
694 let n_tm = rand rtm in
695 let th = INST [n_tm, n_var_num] GT0_NUM in
696 TRANS th (raw_gt0_hash_conv n_tm);;
701 let tm = `0 < 65536`;;
702 let tm' = rand (replace_numerals tm);;
705 test 10000 NUM_LT_CONV tm;;
707 test 10000 NUM_GT0_HASH_CONV tm';;
712 (*************************************)
716 let LT_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m < NUMERAL n <=> m < n`, REWRITE_TAC[NUMERAL]);;
717 let LE_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m <= NUMERAL n <=> m <= n`, REWRITE_TAC[NUMERAL]);;
719 let LT_n_0 = prove(`n < _0 <=> F`,
720 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
721 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
724 let LE_0_n = prove(`_0 <= n <=> T`,
725 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
726 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
729 let SUC_LT_THM = ARITH_RULE `SUC m < SUC n <=> m < n`;;
730 let SUC_LE_THM = ARITH_RULE `SUC m <= SUC n <=> m <= n`;;
736 (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *)
738 let bin = mk_comb (const_array.(i), n_var_num) in
739 let lt_tm = mk_binop lt_op_num zero_const bin in
740 REWRITE_CONV[def_array.(i); ARITH_LT; ARITH_LE] lt_tm;;
743 let th_lt0_table = Hashtbl.create maximum;;
744 for i = 0 to maximum - 1 do
745 let th = gen_0_lt_bi i in
746 let name = names_array.(i) in
747 Hashtbl.add th_lt0_table name th
753 (* Generates the theorem |- bi(m) < bj(n) <=> m <= n (or m < n) *)
754 let gen_bi_lt_bj i j =
755 let bim = mk_comb (const_array.(i), m_var_num) in
756 let bjn = mk_comb (const_array.(j), n_var_num) in
757 let lt_tm = mk_binop lt_op_num bim bjn in
758 REWRITE_CONV[def_array.(i); def_array.(j); ARITH_LT; ARITH_LE] lt_tm;;
761 (* Given a theorem |- bi(m) < bj(n) <=> P m n, generates the theorem
762 |- SUC(bi(m)) < SUC(bj(n)) <=> P m n *)
763 let gen_next_lt_thm th =
764 let ltm, n_tm = (dest_comb o lhand o concl) th in
765 let m_tm = rand ltm in
766 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LT_THM in
767 let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
768 let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
769 let th1 = SYM (MK_COMB ((AP_TERM lt_op_num suc_m), suc_n)) in
770 TRANS (TRANS th1 th0) th;;
775 let th_lt_table = Hashtbl.create (maximum * maximum);;
778 for i = 0 to maximum - 1 do
779 let th = ref (gen_bi_lt_bj 0 i) in
780 let name_left = names_array.(0) and
781 name_right = names_array.(i) in
782 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
784 for k = 1 to maximum - i - 1 do
785 let x = k and y = i + k in
786 let name_left = names_array.(x) and
787 name_right = names_array.(y) in
788 th := gen_next_lt_thm (!th);
789 Hashtbl.add th_lt_table (name_left ^ name_right) !th
794 for i = 1 to maximum - 1 do
795 let th = ref (gen_bi_lt_bj i 0) in
796 let name_left = names_array.(i) and
797 name_right = names_array.(0) in
798 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
800 for k = 1 to maximum - i - 1 do
801 let x = i + k and y = k in
802 let name_left = names_array.(x) and
803 name_right = names_array.(y) in
804 th := gen_next_lt_thm (!th);
805 Hashtbl.add th_lt_table (name_left ^ name_right) !th
815 (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *)
817 let bin = mk_comb (const_array.(i), n_var_num) in
818 let lt_tm = mk_binop le_op_num bin zero_const in
819 REWRITE_CONV[def_array.(i); ARITH_LT; ARITH_LE] lt_tm;;
822 let th_le0_table = Hashtbl.create maximum;;
823 for i = 0 to maximum - 1 do
824 let th = gen_bi_le_0 i in
825 let name = names_array.(i) in
826 Hashtbl.add th_le0_table name th
832 (* Generates the theorem |- bi(m) <= bj(n) <=> m <= n (or m < n) *)
833 let gen_bi_le_bj i j =
834 let bim = mk_comb (const_array.(i), m_var_num) in
835 let bjn = mk_comb (const_array.(j), n_var_num) in
836 let lt_tm = mk_binop le_op_num bim bjn in
837 REWRITE_CONV[def_array.(i); def_array.(j); ARITH_LT; ARITH_LE] lt_tm;;
840 (* Given a theorem |- bi(m) <= bj(n) <=> P m n, generates the theorem
841 |- SUC(bi(m)) <= SUC(bj(n)) <=> P m n *)
842 let gen_next_le_thm th =
843 let ltm, n_tm = (dest_comb o lhand o concl) th in
844 let m_tm = rand ltm in
845 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LE_THM in
846 let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
847 let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
848 let th1 = SYM (MK_COMB ((AP_TERM le_op_num suc_m), suc_n)) in
849 TRANS (TRANS th1 th0) th;;
853 let th_le_table = Hashtbl.create (maximum * maximum);;
856 for i = 0 to maximum - 1 do
857 let th = ref (gen_bi_le_bj 0 i) in
858 let name_left = names_array.(0) and
859 name_right = names_array.(i) in
860 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
862 for k = 1 to maximum - i - 1 do
863 let x = k and y = i + k in
864 let name_left = names_array.(x) and
865 name_right = names_array.(y) in
866 th := gen_next_le_thm (!th);
867 Hashtbl.add th_le_table (name_left ^ name_right) !th
872 for i = 1 to maximum - 1 do
873 let th = ref (gen_bi_le_bj i 0) in
874 let name_left = names_array.(i) and
875 name_right = names_array.(0) in
876 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
878 for k = 1 to maximum - i - 1 do
879 let x = i + k and y = k in
880 let name_left = names_array.(x) and
881 name_right = names_array.(y) in
882 th := gen_next_le_thm (!th);
883 Hashtbl.add th_le_table (name_left ^ name_right) !th
890 let rec raw_lt_hash_conv tm =
891 let ltm, rtm = dest_comb tm in
892 let ltm = rand ltm in
895 INST[ltm, n_var_num] LT_n_0
899 let bn_tm, n_tm = dest_comb rtm in
900 let cbn = (fst o dest_const) bn_tm in
901 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_lt0_table cbn) in
902 if cbn = b0_name then
903 let th1 = raw_lt_hash_conv (rand (concl th0)) in
909 let bm_tm, m_tm = dest_comb ltm in
910 let bn_tm, n_tm = dest_comb rtm in
911 let cbm = (fst o dest_const) bm_tm in
912 let cbn = (fst o dest_const) bn_tm in
913 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_lt_table (cbm^cbn)) in
914 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
917 raw_lt_hash_conv (rand (concl th0))
919 raw_le_hash_conv (rand (concl th0)) in
922 raw_le_hash_conv tm =
923 let ltm, rtm = dest_comb tm in
924 let ltm = rand ltm in
927 INST[rtm, n_var_num] LE_0_n
931 let bn_tm, n_tm = dest_comb ltm in
932 let cbn = (fst o dest_const) bn_tm in
933 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_le0_table cbn) in
934 if cbn = b0_name then
935 let th1 = raw_le_hash_conv (rand (concl th0)) in
941 let bm_tm, m_tm = dest_comb ltm in
942 let bn_tm, n_tm = dest_comb rtm in
943 let cbm = (fst o dest_const) bm_tm in
944 let cbn = (fst o dest_const) bn_tm in
945 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_le_table (cbm^cbn)) in
946 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
949 raw_lt_hash_conv (rand (concl th0))
951 raw_le_hash_conv (rand (concl th0)) in
956 let NUM_LT_HASH_CONV tm =
957 let atm, rtm = dest_comb tm in
958 let ltm = rand atm in
959 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LT_NUM in
960 let rtm = rand(concl th) in
961 TRANS th (raw_lt_hash_conv rtm);;
965 let NUM_LE_HASH_CONV tm =
966 let atm, rtm = dest_comb tm in
967 let ltm = rand atm in
968 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LE_NUM in
969 let rtm = rand(concl th) in
970 TRANS th (raw_le_hash_conv rtm);;
975 let x = num_of_string "3543593547359325353535";;
976 let y = num_of_string "9392392983247294924242";;
978 let xx = mk_binop lt_op_num (mk_numeral_array x) (mk_numeral_array y);;
979 let yy = mk_binop lt_op_num (mk_numeral x) (mk_numeral y);;
983 test 1000 NUM_LT_CONV yy;;
985 test 10000 NUM_LT_HASH_CONV xx;;
991 (**************************************)
998 let ADD_NUM = prove(mk_eq(mk_binop plus_op_num (mk_comb (num_const, m_var_num)) (mk_comb (num_const, n_var_num)),
999 mk_comb(num_const, mk_binop plus_op_num m_var_num n_var_num)),
1000 REWRITE_TAC[num_def; NUMERAL]);;
1002 let CADD_0_n = prove(`SUC (_0 + n) = SUC n`, REWRITE_TAC[ADD_0_n]);;
1003 let CADD_n_0 = prove(`SUC (n + _0) = SUC n`, REWRITE_TAC[ADD_n_0]);;
1005 (* B0 (SUC n) = B0 n + maximum *)
1006 let B0_SUC = prove(mk_eq(mk_comb(b0_const, mk_comb(suc_const, n_var_num)),
1007 mk_binop plus_op_num max_const (mk_comb(b0_const, n_var_num))),
1008 REWRITE_TAC [B0_EXPLICIT] THEN ARITH_TAC);;
1010 let B0_ADD = prove(mk_eq(mk_binop plus_op_num (mk_comb(b0_const, m_var_num)) (mk_comb(b0_const, n_var_num)),
1011 mk_comb(b0_const, mk_binop plus_op_num m_var_num n_var_num)),
1012 REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
1014 let SUC_ADD_RIGHT = prove(`SUC(m + n) = m + SUC n`, ARITH_TAC);;
1017 (* Generate all theorems iteratively *)
1019 let th_add_right_next th =
1020 let lhs, rhs = dest_eq(concl th) in
1021 let ltm, rtm = dest_comb rhs in
1022 let cn = fst(dest_const ltm) in
1023 let suc_th = AP_TERM suc_const th in
1024 let th_rhs = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1025 let ltm, rarg = dest_comb lhs in
1026 let larg = rand ltm in
1027 let th1 = INST[larg, m_var_num; rarg, n_var_num] SUC_ADD_RIGHT in
1028 let cn = fst(dest_const(rator rarg)) in
1029 let th2 = Hashtbl.find th_suc_table cn in
1030 let th_lhs = TRANS th1 (AP_TERM ltm th2) in
1031 TRANS (TRANS (SYM th_lhs) suc_th) th_rhs;;
1034 let th_add_array = Array.make (maximum * maximum) (REFL zero_const);;
1036 for i = 0 to maximum - 1 do
1041 INST[n_var_num, m_var_num; m_var_num, n_var_num]
1042 (ONCE_REWRITE_RULE[ADD_AC] th_add_array.(i)) in
1043 let _ = th_add_array.(i * maximum) <- th0 in
1045 for j = 1 to maximum - 1 do
1046 th_add_array.(i * maximum + j) <- th_add_right_next th_add_array.(i * maximum + j - 1)
1052 (* SUC (B_i(m) + B_j(n)) = B_p(...) *)
1054 let add_th = th_add_array.(i * maximum + j) in
1055 let th0 = AP_TERM suc_const add_th in
1056 let ltm, rtm = dest_comb(rand(concl th0)) in
1057 let ltm, rtm = dest_comb rtm in
1058 let cn = fst(dest_const ltm) in
1059 let suc_th = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1063 let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);;
1065 for i = 0 to maximum - 1 do
1066 for j = 0 to maximum - 1 do
1067 th_cadd_array.(i * maximum + j) <- th_cadd i j
1073 let th_add_table = Hashtbl.create (maximum * maximum);;
1075 for i = 0 to maximum - 1 do
1076 for j = 0 to maximum - 1 do
1077 let name = names_array.(i) ^ names_array.(j) in
1078 let th = th_add_array.(i * maximum + j) in
1079 let cflag = (i + j >= maximum) in
1080 Hashtbl.add th_add_table name (th, cflag)
1086 let th_cadd_table = Hashtbl.create (maximum * maximum);;
1088 for i = 0 to maximum - 1 do
1089 for j = 0 to maximum - 1 do
1090 let name = names_array.(i) ^ names_array.(j) in
1091 let th = th_cadd_array.(i * maximum + j) in
1092 let cflag = (i + j + 1 >= maximum) in
1093 Hashtbl.add th_cadd_table name (th, cflag)
1099 (* ADD conversion *)
1102 let rec raw_add_conv_hash tm =
1103 let atm,rtm = dest_comb tm in
1104 let ltm = rand atm in
1105 if ltm = zero_const then
1106 INST [rtm,n_var_num] ADD_0_n
1107 else if rtm = zero_const then
1108 INST [ltm,n_var_num] ADD_n_0
1110 let lbit,larg = dest_comb ltm
1111 and rbit,rarg = dest_comb rtm in
1112 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1113 let th0, cflag = Hashtbl.find th_add_table name in
1114 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1115 let ltm, rtm = dest_comb(rand(concl th)) in
1117 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1119 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm))
1120 and raw_adc_conv_hash tm =
1121 let atm,rtm = dest_comb (rand tm) in
1122 let ltm = rand atm in
1123 if ltm = zero_const then
1124 let th = INST [rtm,n_var_num] CADD_0_n in
1125 TRANS th (raw_suc_conv_hash (rand(concl th)))
1126 else if rtm = zero_const then
1127 let th = INST [ltm,n_var_num] CADD_n_0 in
1128 TRANS th (raw_suc_conv_hash (rand(concl th)))
1130 let lbit,larg = dest_comb ltm
1131 and rbit,rarg = dest_comb rtm in
1132 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1133 let th0, cflag = Hashtbl.find th_cadd_table name in
1134 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1135 let ltm, rtm = dest_comb(rand(concl th)) in
1137 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1139 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1142 let NUM_ADD_HASH_CONV tm =
1143 let atm, rtm = dest_comb tm in
1144 let ltm = rand atm in
1145 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] ADD_NUM in
1146 let ltm, rtm = dest_comb(rand(concl th)) in
1147 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1151 let x = num_of_string "3543593547359325353535";;
1152 let y = num_of_string "9392392983247294924242";;
1154 let xx = mk_binop plus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1155 let yy = mk_binop plus_op_num (mk_numeral x) (mk_numeral y);;
1157 test 10000 NUM_ADD_CONV yy;; (* 5.672 *)
1158 test 10000 NUM_ADD_HASH_CONV xx;; (* 8: 0.728 *)
1161 (********************************)
1165 let SUB_NUM = prove(mk_eq(mk_binop minus_op_num (mk_comb (num_const, m_var_num)) (mk_comb (num_const, n_var_num)),
1166 mk_comb(num_const, mk_binop minus_op_num m_var_num n_var_num)),
1167 REWRITE_TAC[num_def; NUMERAL]);;
1169 let SUB_lemma1 = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> m - n = t:num`;;
1170 let SUB_lemma2 = (UNDISCH_ALL o REWRITE_RULE[NUMERAL] o ARITH_RULE) `m + t = n ==> m - n = 0`;;
1171 let LE_lemma = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> n <= m:num`;;
1174 let raw_sub_hash_conv tm =
1175 let ltm, n_tm = dest_comb tm in
1176 let m_tm = rand ltm in
1177 let m = raw_dest_hash m_tm in
1178 let n = raw_dest_hash n_tm in
1181 let t_tm = rand (mk_numeral_array t) in
1182 let th0 = INST[n_tm, n_var_num; t_tm, t_var_num; m_tm, m_var_num] SUB_lemma1 in
1183 let th_add = raw_add_conv_hash (mk_binop plus_op_num n_tm t_tm) in
1184 MY_PROVE_HYP th_add th0
1186 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1187 let th0 = INST[m_tm, m_var_num; t_tm, t_var_num; n_tm, n_var_num] SUB_lemma2 in
1188 let th_add = raw_add_conv_hash (mk_binop plus_op_num m_tm t_tm) in
1189 MY_PROVE_HYP th_add th0;;
1193 (* Returns either (tm1 - tm2, tm2 <= tm1) or (tm2 - tm1, tm1 <= tm2) *)
1194 let raw_sub_and_le_hash_conv tm1 tm2 =
1195 let m = raw_dest_hash tm1 in
1196 let n = raw_dest_hash tm2 in
1199 let t_tm = rand (mk_numeral_array t) in
1200 let inst = INST[tm2, n_var_num; t_tm, t_var_num; tm1, m_var_num] in
1201 let th_sub = inst SUB_lemma1 in
1202 let th_le = inst LE_lemma in
1203 let th_add = raw_add_conv_hash (mk_binop plus_op_num tm2 t_tm) in
1204 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le)
1206 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1207 let inst = INST[tm2, m_var_num; t_tm, t_var_num; tm1, n_var_num] in
1208 let th_sub = inst SUB_lemma1 in
1209 let th_le = inst LE_lemma in
1210 let th_add = raw_add_conv_hash (mk_binop plus_op_num tm1 t_tm) in
1211 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le);;
1215 let NUM_SUB_HASH_CONV tm =
1216 let atm, rtm = dest_comb tm in
1217 let ltm = rand atm in
1218 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] SUB_NUM in
1219 let ltm, rtm = dest_comb(rand(concl th)) in
1220 TRANS th (AP_TERM ltm (raw_sub_hash_conv rtm));;
1224 let y = num_of_string "3543593547359325353535";;
1225 let x = num_of_string "9392392983247294924242";;
1227 let xx = mk_binop minus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1228 let yy = mk_binop minus_op_num (mk_numeral x) (mk_numeral y);;
1230 test 1000 NUM_SUB_CONV yy;; (* 2.376 *)
1231 test 1000 NUM_SUB_HASH_CONV xx;; (* 4: 0.692 *)
1236 (********************************)
1238 (* Multiplication *)
1240 let MUL_NUM = prove(mk_eq(mk_binop mul_op_num (mk_comb(num_const, m_var_num)) (mk_comb(num_const, n_var_num)),
1241 mk_comb(num_const, mk_binop mul_op_num m_var_num n_var_num)),
1242 REWRITE_TAC[num_def; NUMERAL]);;
1244 let MUL_0_n = prove(`_0 * n = _0`, ONCE_REWRITE_TAC[GSYM NUM_THM] THEN
1245 ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN REWRITE_TAC[num_def] THEN
1246 REWRITE_TAC[MULT_CLAUSES]);;
1248 let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;;
1250 let MUL_1_n, MUL_n_1 =
1251 let one_const = mk_comb (const_array.(1), zero_const) in
1252 let cond = mk_eq(mk_binop mul_op_num one_const n_var_num, n_var_num) in
1253 let th = prove(cond, REWRITE_TAC[def_array.(1); ARITH_ZERO] THEN
1254 ONCE_REWRITE_TAC[GSYM NUM_THM] THEN
1255 ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN
1256 REWRITE_TAC[num_def] THEN
1257 REWRITE_TAC[MULT_CLAUSES]) in
1258 th, ONCE_REWRITE_RULE[MULT_AC] th;;
1261 let MUL_BIT0_t = prove(`BIT0 n * t = BIT0 (n * t)`, REWRITE_TAC[BIT0; RIGHT_ADD_DISTRIB]);;
1263 let MUL_B0_t = prove(mk_eq(mk_binop mul_op_num (mk_comb(b0_const, n_var_num)) t_var_num,
1264 mk_comb(b0_const, mk_binop mul_op_num n_var_num t_var_num)),
1265 REWRITE_TAC[def_array.(0)] THEN REWRITE_TAC[MUL_BIT0_t]);;
1267 let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
1270 let MUL_SUC_RIGHT = prove(`m * SUC(n) = m * n + m`, ARITH_TAC);;
1273 (* Multiplication table *)
1275 let mul_th_next_right th =
1276 let ltm, rtm = dest_comb(rand(rator(concl th))) in
1277 let mtm = rand ltm in
1278 let th0 = INST[mtm, m_var_num; rtm, n_var_num] MUL_SUC_RIGHT in
1279 let th1 = AP_THM (AP_TERM plus_op_num th) mtm in
1280 let sum_th = raw_add_conv_hash (rand(concl th1)) in
1281 let th2 = TRANS (TRANS th0 th1) sum_th in
1282 let cn = fst(dest_const (rator rtm)) in
1283 let th_suc = INST[zero_const, n_var_num] (Hashtbl.find th_suc_table cn) in
1284 let th3 = AP_TERM (mk_comb (mul_op_num, mtm)) th_suc in
1285 TRANS (SYM th3) th2;;
1288 let mul_array = Array.make (maximum * maximum) (REFL zero_const);;
1289 for i = 1 to maximum - 1 do
1290 let th1 = INST[mk_comb(const_array.(i), zero_const), n_var_num] MUL_n_1 in
1291 let _ = mul_array.(i * maximum + 1) <- th1 in
1293 for j = 2 to maximum - 1 do
1294 mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1)
1299 let mul_table = Hashtbl.create (maximum * maximum);;
1300 for i = 1 to maximum - 1 do
1301 for j = 1 to maximum - 1 do
1302 Hashtbl.add mul_table (names_array.(i) ^ names_array.(j)) mul_array.(i * maximum + j)
1307 (* General multiplication theorem *)
1310 let mul (a,b) = mk_binop mul_op_num a b and
1311 add (a,b) = mk_binop plus_op_num a b in
1312 let lhs = mul(add(t_var_num, mk_comb(b0_const, m_var_num)),
1313 add(r_var_num, mk_comb(b0_const, n_var_num))) in
1314 let rhs = add(mul(t_var_num, r_var_num),
1315 mk_comb(b0_const, add(mk_comb(b0_const, mul(m_var_num, n_var_num)),
1316 add(mul(m_var_num, r_var_num),
1317 mul(n_var_num, t_var_num))))) in
1318 prove(mk_eq(lhs, rhs),
1319 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1320 REWRITE_TAC[MUL_B0_t; MUL_t_B0] THEN
1321 ONCE_REWRITE_TAC[GSYM ADD_ASSOC] THEN
1322 REWRITE_TAC[th_add_array.(0)] THEN
1323 REWRITE_TAC[ADD_AC; MULT_AC]);;
1325 let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;;
1328 let ltm, rtm = dest_comb tm in
1332 (* B_i(m) * B_j(n) = B_p(B_q(m * n) + m * B_j(0) + n * B_i(0))
1333 where B_p(B_q(0)) = i * j *)
1334 let gen_mul_thm i j =
1335 let bi0 = mk_comb(const_array.(i), zero_const) and
1336 bj0 = mk_comb(const_array.(j), zero_const) in
1337 let def_i = INST[m_var_num, n_var_num] def_thm_array.(i) in
1338 let def_j = def_thm_array.(j) in
1339 let th0 = MK_COMB(AP_TERM mul_op_num def_i, def_j) in
1340 let th1 = TRANS th0 (INST[bi0, t_var_num; bj0, r_var_num] prod_lemma) in
1341 let mul_th = mul_array.(i * maximum + j) in
1342 let larg, rarg = dest_op (rand (concl th1)) in
1343 let th2 = TRANS th1 (AP_THM (AP_TERM plus_op_num mul_th) rarg) in
1344 let larg = rand(concl mul_th) in
1345 let b_low, b_high = dest_comb larg in
1346 let rtm = rand(rarg) in
1347 let th_add = INST[b_high, m_var_num; rtm, n_var_num]
1348 (fst(Hashtbl.find th_add_table (fst(dest_const b_low)^b0_name))) in
1349 if i * j < maximum then
1350 let ltm, rtm = dest_op(rand(rand(concl th_add))) in
1351 let add_0 = AP_TERM b_low (INST[rtm, n_var_num] ADD_0_n) in
1352 TRANS th2 (TRANS th_add add_0)
1354 let larg, rtm = dest_op (rand(rand(concl th_add))) in
1355 let rarg, rtm = dest_op rtm in
1356 let th_assoc = INST[larg, m_var_num; rarg, n_var_num; rtm, p_var_num] ADD_ASSOC' in
1357 let mn = rand(rarg) in
1358 let b_high = rator b_high in
1359 let th_add2' = INST[zero_const, m_var_num; mn, n_var_num]
1360 (fst(Hashtbl.find th_add_table (fst(dest_const b_high)^b0_name))) in
1361 let add_0 = AP_TERM b_high (INST[mn, n_var_num] ADD_0_n) in
1362 let th_add2 = TRANS th_add2' add_0 in
1363 let th3 = TRANS th_assoc (AP_THM (AP_TERM plus_op_num th_add2) rtm) in
1364 let th4 = TRANS th_add (AP_TERM b_low th3) in
1368 let gen_mul_table = Hashtbl.create (maximum * maximum);;
1370 for i = 1 to maximum - 1 do
1371 for j = 1 to maximum - 1 do
1372 let name = names_array.(i) ^ names_array.(j) in
1373 Hashtbl.add gen_mul_table name (gen_mul_thm i j)
1378 (* B_i(m) * B_j(0) = B_p(B_q(0) + m * B_j(0))
1379 where i * j = B_p(B_q(0)) *)
1380 let mul1_right_th i j =
1381 let th0 = INST[zero_const, n_var_num]
1382 (Hashtbl.find gen_mul_table (names_array.(i)^names_array.(j))) in
1383 let b_low, rtm = dest_comb(rand(concl th0)) in
1384 let tm1, tm23 = dest_op rtm in
1385 let tm2p, tm3 = dest_comb tm23 in
1386 let tm3_th = INST[rand tm3, n_var_num] MUL_0_n in
1387 let tm2_th = INST[rand(tm2p), n_var_num] ADD_n_0 in
1388 let tm23_th = TRANS (AP_TERM tm2p tm3_th) tm2_th in
1389 let ltm, rtm = dest_comb tm1 in
1390 if (i * j < maximum) then
1391 let tm1_th = TRANS (AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0)) B0_0 in
1392 let tm123_th' = TRANS (INST[tm23, n_var_num] ADD_0_n) tm23_th in
1393 let tm123_th = TRANS (AP_THM (AP_TERM plus_op_num tm1_th) tm23) tm123_th' in
1394 TRANS th0 (AP_TERM b_low tm123_th)
1396 let tm1_th = AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0) in
1397 let tm123_th = MK_COMB(AP_TERM plus_op_num tm1_th, tm23_th) in
1398 TRANS th0 (AP_TERM b_low tm123_th);;
1401 (* B_j(0) * B_i(m) = B_p(B_q(0) + B_j(0) * B_i(m) *)
1403 let MULT_AC' = CONJUNCT1 MULT_AC;;
1405 let mul1_left_th th =
1406 let lhs, rhs = dest_eq(concl th) in
1407 let ltm, rtm = dest_op lhs in
1408 let th_lhs = INST[ltm, n_var_num; rtm, m_var_num] MULT_AC' in
1409 let btm, rtm = dest_comb rhs in
1410 let larg, rarg = dest_op rtm in
1411 if (is_comb larg) then
1412 let ltm, rtm = dest_op rarg in
1413 let th_rhs' = INST[ltm, m_var_num; rtm, n_var_num] MULT_AC' in
1414 let th_rhs = AP_TERM (mk_comb(plus_op_num, larg)) th_rhs' in
1415 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs))
1417 let th_rhs = INST[larg, m_var_num; rarg, n_var_num] MULT_AC' in
1418 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs));;
1423 let mul1_right_th_table = Hashtbl.create (maximum * maximum);;
1424 let mul1_left_th_table = Hashtbl.create (maximum * maximum);;
1426 for i = 1 to maximum - 1 do
1427 for j = 1 to maximum - 1 do
1428 let name_right = names_array.(i) ^ names_array.(j) in
1429 let name_left = names_array.(j) ^ names_array.(i) in
1430 let th = mul1_right_th i j in
1431 let add_flag = (i * j >= maximum) in
1432 let _ = Hashtbl.add mul1_right_th_table name_right (add_flag, th) in
1433 Hashtbl.add mul1_left_th_table name_left (add_flag, mul1_left_th th)
1439 (******************************************************)
1444 (* Multiplies arg and (tm = tmname(_0)) *)
1445 let rec raw_mul1_right_hash arg tm tmname =
1446 if arg = zero_const then
1447 INST [tm, n_var_num] MUL_0_n
1449 let btm, mtm = dest_comb arg in
1450 let cn = fst(dest_const btm) in
1451 if (cn = b0_name) then
1452 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_B0_t in
1453 TRANS th (AP_TERM b0_const (raw_mul1_right_hash mtm tm tmname))
1455 let name = cn ^ tmname in
1456 if (mtm = zero_const) then
1457 Hashtbl.find mul_table name
1459 let add_flag, th' = Hashtbl.find mul1_right_th_table name in
1460 let th = INST[mtm, m_var_num] th' in
1462 let ltm, rtm = dest_comb(rand(concl th)) in
1463 let lplus, rarg = dest_comb rtm in
1464 let th2 = AP_TERM lplus (raw_mul1_right_hash mtm tm tmname) in
1465 let th_add = raw_add_conv_hash (rand(concl th2)) in
1466 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1468 let ltm = rator(rand(concl th)) in
1469 let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in
1473 (* Multiplies (tm = tmname(_0)) and arg *)
1474 let rec raw_mul1_left_hash tm tmname arg =
1475 if arg = zero_const then
1476 INST [tm, n_var_num] MUL_n_0
1478 let btm, mtm = dest_comb arg in
1479 let cn = fst(dest_const btm) in
1480 if (cn = b0_name) then
1481 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_t_B0 in
1482 TRANS th (AP_TERM b0_const (raw_mul1_left_hash tm tmname mtm))
1484 let name = tmname ^ cn in
1485 if (mtm = zero_const) then
1486 Hashtbl.find mul_table name
1488 let add_flag, th' = Hashtbl.find mul1_left_th_table name in
1489 let th = INST[mtm, m_var_num] th' in
1491 let ltm, rtm = dest_comb(rand(concl th)) in
1492 let lplus, rarg = dest_comb rtm in
1493 let th2 = AP_TERM lplus (raw_mul1_left_hash tm tmname mtm) in
1494 let th_add = raw_add_conv_hash (rand(concl th2)) in
1495 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1497 let ltm = rator(rand(concl th)) in
1498 let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in
1502 (* Computes B_i(m) * B_j(n) *)
1503 let rec raw_mul_conv_hash tm =
1504 let larg, rarg = dest_comb tm in
1505 let larg = rand larg in
1506 if larg = zero_const then
1507 INST [rarg, n_var_num] MUL_0_n
1508 else if rarg = zero_const then
1509 INST [larg, n_var_num] MUL_n_0
1512 let lbtm, mtm = dest_comb larg in
1513 let lcn = fst(dest_const lbtm) in
1514 if (lcn = b0_name) then
1515 let th = INST[rarg, t_var_num; mtm, n_var_num] MUL_B0_t in
1516 let ltm, rtm = dest_comb(rand(concl th)) in
1517 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1519 let rbtm, ntm = dest_comb rarg in
1520 let rcn = fst(dest_const rbtm) in
1521 if (rcn = b0_name) then
1522 let th = INST[larg, t_var_num; ntm, n_var_num] MUL_t_B0 in
1523 let ltm, rtm = dest_comb(rand(concl th)) in
1524 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1527 if (ntm = zero_const) then
1528 if (mtm = zero_const) then
1529 Hashtbl.find mul_table (lcn ^ rcn)
1531 raw_mul1_right_hash larg (mk_comb(rbtm, zero_const)) rcn
1532 else if (mtm = zero_const) then
1533 raw_mul1_left_hash (mk_comb(lbtm, zero_const)) lcn rarg
1536 let th0 = INST[mtm, m_var_num; ntm, n_var_num]
1537 (Hashtbl.find gen_mul_table (lcn ^ rcn)) in
1538 let b_low, expr = dest_comb(rand(concl th0)) in
1539 let ltm, rsum = dest_comb expr in
1540 let b_high, mul0 = dest_comb (rand ltm) in
1541 let th_mul0 = raw_mul_conv_hash mul0 in
1542 let th_mul1 = raw_mul1_right_hash mtm (mk_comb(rbtm, zero_const)) rcn in
1543 let th_mul2 = raw_mul1_right_hash ntm (mk_comb(lbtm, zero_const)) lcn in
1544 let th_larg = AP_TERM plus_op_num (AP_TERM b_high th_mul0) in
1545 let th_rarg = MK_COMB(AP_TERM plus_op_num th_mul1, th_mul2) in
1547 let add_rarg = TRANS th_rarg (raw_add_conv_hash (rand(concl th_rarg))) in
1548 let add_th = MK_COMB (th_larg, add_rarg) in
1549 let add = TRANS add_th (raw_add_conv_hash (rand(concl add_th))) in
1551 TRANS th0 (AP_TERM b_low add);;
1555 (* The main multiplication conversion *)
1556 let NUM_MULT_HASH_CONV tm =
1557 let ltm, rtm = dest_comb tm in
1558 let larg, rarg = rand (rand ltm), rand rtm in
1559 let th0 = INST[larg, m_var_num; rarg, n_var_num] MUL_NUM in
1560 if (rand(rator(concl th0)) <> tm) then
1561 failwith "NUM_MULT_HASH_CONV"
1563 let rtm = rand(rand(concl th0)) in
1564 let th = raw_mul_conv_hash rtm in
1565 TRANS th0 (AP_TERM num_const th);;
1569 (**************************)
1574 let x = Int 325325353;;
1575 let y = Int 999434312;;
1577 let xx = mk_binop mul_op_num (mk_numeral_array x) (mk_numeral_array y);;
1578 let yy = mk_binop mul_op_num (mk_numeral x) (mk_numeral y);;
1579 let zz = rand(concl(REWRITE_CONV[NUMERAL] xx));;
1581 NUM_MULT_HASH_CONV xx;;
1583 test 1000 NUM_MULT_CONV yy;; (* 4.12 *)
1584 test 1000 NUM_MULT_HASH_CONV xx;; (* 4: 1.69; 6: 0.716(1), 0.608(2), 8: 0.328(3) *)
1585 test 1000 raw_mul_conv_hash zz;; (* 4: 2.45(1), 1.576(2), 8: 0.320 *)
1588 needs "example0.hl";;
1590 let x = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral t1) (mk_numeral t2)) example;;
1591 let h1 = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral_array t1) (mk_numeral_array t2)) example;;
1592 let h2 = map (fun t1, t2 -> mk_binop mul_op_num
1593 (rand (mk_numeral_array t1))
1594 (rand (mk_numeral_array t2))) example;;
1597 test 1 (map NUM_MULT_CONV) x;; (* 2.64 *)
1598 test 10 (map NUM_MULT_HASH_CONV) h1;; (* 4: 5.43; 6: 3.12; 8: 1.67 *)
1599 test 10 (map raw_mul_conv_hash) h2;; (* 5.42; 8: 1.576 *)
1604 (************************************)
1609 let DIV_NUM = prove(mk_eq(mk_binop div_op_num (mk_comb(num_const, m_var_num)) (mk_comb(num_const, n_var_num)),
1610 mk_comb(num_const, mk_binop div_op_num m_var_num n_var_num)),
1611 REWRITE_TAC[num_def; NUMERAL]);;
1614 let DIV_UNIQ' = (UNDISCH_ALL o
1615 PURE_ONCE_REWRITE_RULE[ARITH_RULE `a < b <=> (a < b:num <=> T)`] o
1616 ONCE_REWRITE_RULE[ARITH_RULE `m = q * n + r <=> q * n + r = m:num`] o
1617 REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL) DIV_UNIQ;;
1619 (* Computes m DIV n *)
1620 let raw_div_hash_conv tm =
1621 let ltm, n_tm = dest_comb tm in
1622 let m_tm = rand ltm in
1623 let m = raw_dest_hash m_tm in
1624 let n = raw_dest_hash n_tm in
1625 let q = Num.quo_num m n and
1626 r = Num.mod_num m n in
1627 let q_tm = rand (mk_numeral_array q) and
1628 r_tm = rand (mk_numeral_array r) in
1630 let qn_th = raw_mul_conv_hash (mk_binop mul_op_num q_tm n_tm) in
1631 let qn_tm = rand (concl qn_th) in
1632 let qnr_th = raw_add_conv_hash (mk_binop plus_op_num qn_tm r_tm) in
1633 let th1 = TRANS (AP_THM (AP_TERM plus_op_num qn_th) r_tm) qnr_th in
1634 let th2 = raw_lt_hash_conv (mk_binop lt_op_num r_tm n_tm) in
1635 let th0 = INST[r_tm, r_var_num; n_tm, n_var_num; m_tm, m_var_num; q_tm, q_var_num] DIV_UNIQ' in
1636 MY_PROVE_HYP th1 (MY_PROVE_HYP th2 th0);;
1640 (* The main division conversion *)
1641 let NUM_DIV_HASH_CONV tm =
1642 let ltm, rtm = dest_comb tm in
1643 let larg, rarg = rand (rand ltm), rand rtm in
1644 let th0 = INST[larg, m_var_num; rarg, n_var_num] DIV_NUM in
1645 if (rand(rator(concl th0)) <> tm) then
1646 failwith "NUM_DIV_HASH_CONV"
1648 let rtm = rand(rand(concl th0)) in
1649 let th = raw_div_hash_conv rtm in
1650 TRANS th0 (AP_TERM num_const th);;
1654 let y = num_of_string "3543593547359";;
1655 let x = num_of_string "9392392983247294924242";;
1658 let xx = mk_binop div_op_num (mk_numeral_array x) (mk_numeral_array y);;
1659 let yy = mk_binop div_op_num (mk_numeral x) (mk_numeral y);;
1662 test 100 NUM_DIV_CONV yy;;
1664 test 1000 NUM_DIV_HASH_CONV xx;;
1668 (*********************************************)
1670 (* EVEN_CONV, ODD_CONV *)
1672 let even_const = `EVEN` and
1673 odd_const = `ODD` and
1674 eq_const = `<=>` and
1680 let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1681 (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);;
1683 let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1684 (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
1686 let EVEN_ZERO = prove(`EVEN _0 <=> T`, REWRITE_TAC[ARITH_EVEN]);;
1687 let ODD_ZERO = prove(`ODD _0 <=> F`, REWRITE_TAC[ARITH_ODD]);;
1690 let EVEN_B0 = prove(mk_eq(mk_comb(`EVEN`, mk_comb(b0_const, `n:num`)), `T`),
1691 REWRITE_TAC[B0_EXPLICIT; EVEN_MULT] THEN
1692 DISJ1_TAC THEN CONV_TAC NUM_EVEN_CONV);;
1695 let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
1696 REWRITE_TAC[NOT_ODD; EVEN_B0]);;
1698 let EVEN_SUC_T = prove(`(EVEN (SUC n) <=> T) <=> (EVEN n <=> F)`, REWRITE_TAC[EVEN]);;
1699 let EVEN_SUC_F = prove(`(EVEN (SUC n) <=> F) <=> (EVEN n <=> T)`, REWRITE_TAC[EVEN]);;
1701 let ODD_SUC_T = prove(`(ODD (SUC n) <=> T) <=> (ODD n <=> F)`, REWRITE_TAC[ODD]);;
1702 let ODD_SUC_F = prove(`(ODD (SUC n) <=> F) <=> (ODD n <=> T)`, REWRITE_TAC[ODD]);;
1706 let next_even_th th =
1707 let ltm, rtm = dest_comb(concl th) in
1708 let b_tm = rand(rand ltm) in
1709 let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1710 let flag = (fst o dest_const) rtm = "T" in
1711 let th0 = SYM (AP_TERM even_const suc_b) in
1712 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1713 let th2 = INST[b_tm, n_var_num] (if flag then EVEN_SUC_F else EVEN_SUC_T) in
1714 EQ_MP (SYM (TRANS th1 th2)) th;;
1717 let next_odd_th th =
1718 let ltm, rtm = dest_comb(concl th) in
1719 let b_tm = rand(rand ltm) in
1720 let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1721 let flag = (fst o dest_const) rtm = "T" in
1722 let th0 = SYM (AP_TERM odd_const suc_b) in
1723 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1724 let th2 = INST[b_tm, n_var_num] (if flag then ODD_SUC_F else ODD_SUC_T) in
1725 EQ_MP (SYM (TRANS th1 th2)) th;;
1728 let even_thm_table = Hashtbl.create maximum;;
1731 Hashtbl.add even_thm_table names_array.(0) EVEN_B0;;
1734 for i = 1 to maximum - 1 do
1735 let th0 = next_even_th (Hashtbl.find even_thm_table names_array.(i - 1)) in
1736 Hashtbl.add even_thm_table names_array.(i) th0
1740 let odd_thm_table = Hashtbl.create maximum;;
1742 Hashtbl.add odd_thm_table names_array.(0) ODD_B0;;
1744 for i = 1 to maximum - 1 do
1745 let th0 = next_odd_th (Hashtbl.find odd_thm_table names_array.(i - 1)) in
1746 Hashtbl.add odd_thm_table names_array.(i) th0
1750 let raw_even_hash_conv tm =
1751 let ltm, rtm = dest_comb tm in
1752 if ((fst o dest_const) ltm <> "EVEN") then
1753 failwith "raw_even_hash_conv: no EVEN"
1755 if (is_const rtm) then
1758 let b_tm, n_tm = dest_comb rtm in
1759 let th0 = Hashtbl.find even_thm_table ((fst o dest_const) b_tm) in
1760 INST[n_tm, n_var_num] th0;;
1763 let raw_odd_hash_conv tm =
1764 let ltm, rtm = dest_comb tm in
1765 if ((fst o dest_const) ltm <> "ODD") then
1766 failwith "raw_odd_hash_conv: no ODD"
1768 if (is_const rtm) then
1771 let b_tm, n_tm = dest_comb rtm in
1772 let th0 = Hashtbl.find odd_thm_table ((fst o dest_const) b_tm) in
1773 INST[n_tm, n_var_num] th0;;
1777 let NUM_EVEN_HASH_CONV tm =
1778 let ltm, rtm = dest_comb tm in
1779 let th0 = INST[rand rtm, n_var_num] EVEN_NUM in
1780 let ltm, rtm = dest_comb(concl th0) in
1781 if (rand ltm <> tm) then
1782 failwith "NUM_EVEN_HASH_CONV"
1784 let th1 = raw_even_hash_conv rtm in
1788 let NUM_ODD_HASH_CONV tm =
1789 let ltm, rtm = dest_comb tm in
1790 let th0 = INST[rand rtm, n_var_num] ODD_NUM in
1791 let ltm, rtm = dest_comb(concl th0) in
1792 if (rand ltm <> tm) then
1793 failwith "NUM_ODD_HASH_CONV"
1795 let th1 = raw_odd_hash_conv rtm in