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 raw_dest_hash : term -> num
13 val dest_numeral_hash : term -> num
14 val NUMERAL_TO_NUM_CONV : term -> thm
15 val NUM_TO_NUMERAL_CONV : term -> thm
16 val raw_suc_conv_hash : term -> thm
17 val NUM_SUC_HASH_CONV : term -> thm
18 val raw_eq0_hash_conv : term -> thm
19 val NUM_EQ0_HASH_CONV : term -> thm
20 val raw_pre_hash_conv : term -> thm
21 val NUM_PRE_HASH_CONV : term -> thm
22 val raw_gt0_hash_conv : term -> thm
23 val NUM_GT0_HASH_CONV : term -> thm
24 val raw_lt_hash_conv : term -> thm
25 val raw_le_hash_conv : term -> thm
26 val NUM_LT_HASH_CONV : term -> thm
27 val NUM_LE_HASH_CONV : term -> thm
28 val raw_add_conv_hash : term -> thm
29 val NUM_ADD_HASH_CONV : term -> thm
30 val raw_sub_hash_conv : term -> thm
31 val raw_sub_and_le_hash_conv : term -> term -> thm * thm
32 val NUM_SUB_HASH_CONV : term -> thm
33 val raw_mul_conv_hash : term -> thm
34 val NUM_MULT_HASH_CONV : term -> thm
35 val raw_div_hash_conv : term -> thm
36 val NUM_DIV_HASH_CONV : term -> thm
38 val raw_even_hash_conv : term -> thm
39 val raw_odd_hash_conv : term -> thm
40 val NUM_EVEN_HASH_CONV : term -> thm
41 val NUM_ODD_HASH_CONV : term -> thm
45 needs "../formal_lp/arith/misc.hl";;
46 needs "../formal_lp/arith/arith_options.hl";;
48 module Arith_hash : Arith_hash_sig = struct
57 (* Generate definitions and constants *)
59 let num_type = `:num`;;
60 let fnum_type = `:num->num`;;
62 let numeral_const = `NUMERAL` and
64 bit0_const = `BIT0` and
65 bit1_const = `BIT1` and
69 let m_var_num = `m:num` and
70 n_var_num = `n:num` and
71 t_var_num = `t:num` and
72 r_var_num = `r:num` and
73 p_var_num = `p:num` and
76 let suc_const = `SUC` and
77 plus_op_num = `(+):num->num->num` and
78 minus_op_num = `(-):num->num->num` and
79 mul_op_num = `( * ):num->num->num` and
80 div_op_num = `(DIV):num->num->num` and
81 le_op_num = `(<=):num->num->bool` and
82 lt_op_num = `(<):num->num->bool`;;
85 let plus_op_real = `(+):real->real->real` and
86 mul_op_real = `( * ):real->real->real`;;
90 let names_array = Array.init maximum (fun i -> "D"^(string_of_int i));;
95 let num_name = "NUM"^(string_of_int base);;
96 let num_def = new_basic_definition (mk_eq(mk_var(num_name, fnum_type), numeral_const));;
97 let num_const = mk_const(num_name, []);;
98 let num_def_sym = SYM num_def;;
99 let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
100 REWRITE_TAC[num_def; NUMERAL]);;
104 (* B_i(n) = i + B_0(n) *)
105 let mk_bit_definition i =
106 let lhs = mk_var (names_array.(i), fnum_type) in
107 let tm1 = mk_binop mul_op_num (mk_small_numeral base) n_var_num in
108 let tm2 = mk_binop plus_op_num tm1 (mk_small_numeral i) in
109 let rhs = mk_abs (n_var_num, tm2) in
110 new_basic_definition (mk_eq (lhs, rhs));;
114 let def_basic_array = Array.init maximum mk_bit_definition;;
115 let def_array = Array.init maximum (fun i ->
116 let basic = def_basic_array.(i) in
117 let th1 = AP_THM basic n_var_num in
118 TRANS th1 (BETA (rand (concl th1))));;
120 (* Index computation *)
123 let zero_index = int_of_char '0' in
124 let rec index str len i acc =
125 if i >= len then acc else
126 let ch = int_of_char (String.get str i) - zero_index in
127 index str len (i + 1) (acc * 10 + ch) in
129 let str = (fst o dest_const) tm in
130 index str (String.length str) 1 0;;
134 let def_table = Hashtbl.create maximum;;
135 let def_basic_table = Hashtbl.create maximum;;
137 for i = 0 to maximum - 1 do
138 let _ = Hashtbl.add def_table names_array.(i) def_array.(i) in
139 Hashtbl.add def_basic_table names_array.(i) def_basic_array.(i)
146 let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));;
148 let b0_def = def_array.(0);;
149 let b0_const = const_array.(0);;
150 let b0_name = names_array.(0);;
152 let max_const = mk_small_numeral maximum;;
156 (* Alternative definition of B_i *)
158 let ADD_0_n = prove(`_0 + n = n`,
159 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
160 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
161 let ADD_n_0 = prove(`n + _0 = n`,
162 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
163 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
165 let MUL_n_0 = prove(`n * _0 = 0`,
166 REWRITE_TAC[NUMERAL] THEN
167 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
168 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
172 (* B_i(n) = i + B_0(n) *)
174 let bin = mk_comb(const_array.(i), n_var_num) in
175 let bi0 = mk_comb(const_array.(i), zero_const) in
176 let b0n = mk_comb(const_array.(0), n_var_num) in
177 let rhs = mk_binop plus_op_num bi0 b0n in
178 prove(mk_eq(bin, rhs), REWRITE_TAC[def_array.(i); def_array.(0)] THEN
179 REWRITE_TAC[MUL_n_0; ADD_CLAUSES] THEN ARITH_TAC);;
182 let def_thm_array = Array.init maximum def_thm;;
185 let B0_0 = prove(mk_eq(mk_comb(b0_const, zero_const), zero_const),
186 REWRITE_TAC[b0_def; MUL_n_0; ADD_CLAUSES; NUMERAL]);;
190 let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num),
191 mk_binop mul_op_num max_const n_var_num),
192 REWRITE_TAC[b0_def; ADD_CLAUSES]);;
197 (******************************)
199 (* mk_numeral and dest_numeral *)
204 let mk_table = Hashtbl.create maximum;;
206 for i = 0 to maximum - 1 do
207 Hashtbl.add mk_table (Int i) const_array.(i)
212 let max_num = Int maximum;;
215 let mk_numeral_hash =
220 let m = mod_num n max_num in
221 let bit = Hashtbl.find mk_table m in
222 mk_comb(bit, mk_num(quo_num n max_num)) in
223 fun n -> if n </ num_0 then failwith "mk_numeral_hash: negative argument"
224 else mk_comb(num_const, mk_num n);;
227 let mk_numeral_array =
232 let m = Num.int_of_num (mod_num n max_num) in
233 let bit = const_array.(m) in
234 mk_comb(bit, mk_num(quo_num n max_num)) in
235 fun n -> if n </ num_0 then failwith "mk_numeral_array: negative argument"
236 else mk_comb(num_const, mk_num n);;
239 let mk_small_numeral_array =
241 if (n = 0) then zero_const
243 let m = n mod maximum in
244 let bit = const_array.(m) in
245 mk_comb(bit, mk_num(n / maximum)) in
246 fun n -> if n < 0 then failwith "mk_small_numeral_array: negative argument"
247 else mk_comb (num_const, mk_num n);;
253 test 10000 mk_numeral_hash (Int 65535);; (* 0.736 *)
255 test 10000 mk_numeral_array (Int 65535);; (* 0.728 *)
257 test 100000 mk_small_numeral_array 65535;; (* 0.216 *)
259 test 1000 mk_numeral_array (num_of_string "9111111111111111");; (* 0.288 *)
267 let dest_table_num = Hashtbl.create maximum;;
269 for i = 0 to maximum - 1 do
270 Hashtbl.add dest_table_num names_array.(i) (Int i)
273 let dest_array_num = Array.init maximum (fun i -> Num.num_of_int i);;
278 let max_num = Int maximum;;
281 let rec raw_dest_hash tm =
282 if tm = zero_const then
285 let l, r = dest_comb tm in
286 let n = max_num */ raw_dest_hash r in
287 let cn = fst(dest_const l) in
288 n +/ (Hashtbl.find dest_table_num cn);;
291 let rec raw_dest_array tm =
292 if tm = zero_const then
295 let l, r = dest_comb tm in
296 let n = max_num */ raw_dest_array r in
297 n +/ dest_array_num.(get_index l);;
300 let dest_numeral_hash tm = raw_dest_hash (rand tm);;
301 let dest_numeral_array tm = raw_dest_array (rand tm);;
303 let tm = mk_numeral_array (Int 11111111);;
305 dest_numeral_array tm;;
310 test 100000 dest_numeral_array (mk_numeral_array (Int 11111111));;
316 (******************************)
318 (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *)
321 let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));;
322 let mod_op_num = `MOD`;;
327 let h1 = mk_eq(mk_binop div_op_num m_var_num max_const, q_var_num) in
328 let h2 = mk_eq(mk_binop mod_op_num m_var_num max_const, r_var_num) in
329 let c = mk_eq(m_var_num, mk_binop plus_op_num (mk_binop mul_op_num max_const q_var_num) r_var_num) in
330 (UNDISCH_ALL o ARITH_RULE) (mk_imp(h1, mk_imp(h2, c)));;
333 let ZERO_EQ_ZERO = (EQT_ELIM o REWRITE_CONV[NUMERAL]) `0 = _0`;;
334 let SYM_ZERO_EQ_ZERO = SYM ZERO_EQ_ZERO;;
335 let SYM_NUM_THM = SYM NUM_THM;;
339 let NUMERAL_TO_NUM_CONV tm =
340 let rec raw_conv tm =
341 if (rand tm = zero_const) then
344 let th_div = NUM_DIV_CONV (mk_binop div_op_num tm max_const) in
345 let th_mod = NUM_MOD_CONV (mk_binop mod_op_num tm max_const) in
346 let q_tm = rand(concl th_div) in
347 let r_tm = rand(concl th_mod) in
348 let th0 = INST[tm, m_var_num; q_tm, q_var_num; r_tm, r_var_num] DIV_BASE in
349 let th1 = MY_PROVE_HYP th_mod (MY_PROVE_HYP th_div th0) in
350 let r = dest_small_numeral r_tm in
351 let th2 = INST[q_tm, n_var_num] th_num_conv.(r) in
352 let th = TRANS th1 th2 in
353 let ltm, rtm = dest_comb(rand(concl th)) in
354 let r_th = raw_conv rtm in
355 TRANS th (AP_TERM ltm r_th) in
357 if (fst o dest_const o rator) tm <> "NUMERAL" then
358 failwith "NUMERAL_TO_NUM_CONV"
360 let th0 = raw_conv tm in
361 let n_tm = rand(concl th0) in
362 TRANS th0 (INST[n_tm, n_var_num] SYM_NUM_THM);;
367 test 100 NUMERAL_TO_NUM_CONV `100034242430`;;
372 let replace_numerals = rand o concl o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
373 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;
377 (* NUM_TO_NUMERAL_CONV *)
380 let NUM_TO_NUMERAL_CONV tm =
381 let rec raw_conv tm =
382 if tm = zero_const then
385 let b_tm, n_tm = dest_comb tm in
386 let n_th = raw_conv n_tm in
387 let n_tm' = rand(concl n_th) in
388 let cb = (fst o dest_const) b_tm in
389 let th0 = Hashtbl.find def_table cb in
390 let th1 = AP_TERM b_tm n_th in
391 let th2 = TRANS th1 (INST[n_tm', n_var_num] th0) in
392 let ltm, rtm = dest_comb(rand(concl th2)) in
393 let mul_th = NUM_MULT_CONV (rand ltm) in
394 let add_th0 = AP_THM (AP_TERM plus_op_num mul_th) rtm in
395 let add_th = TRANS add_th0 (NUM_ADD_CONV (rand(concl add_th0))) in
397 let ltm, rtm = dest_comb tm in
398 if (fst o dest_const) ltm <> num_name then
399 failwith "NUM_TO_NUMERAL_CONV"
401 let num_th = INST[rtm, n_var_num] NUM_THM in
402 let th0 = raw_conv rtm in
409 (*************************)
413 let suc_const = `SUC`;;
417 let SUC_NUM = prove(mk_eq(mk_comb(suc_const, mk_comb (num_const, n_var_num)),
418 mk_comb(num_const, mk_comb (suc_const, n_var_num))),
419 REWRITE_TAC[num_def; NUMERAL]);;
421 let SUC_0 = prove(mk_eq(`SUC _0`, mk_comb (const_array.(1), zero_const)),
422 REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_SUC; NUMERAL; ARITH_ADD]);;
426 let cflag = (i + 1 >= maximum) in
427 let suc = if (cflag) then 0 else i + 1 in
428 let lhs = mk_comb(suc_const, (mk_comb (const_array.(i), n_var_num))) in
429 let rhs = mk_comb(const_array.(suc),
430 if (cflag) then mk_comb(suc_const, n_var_num) else n_var_num) in
431 let proof = REWRITE_TAC [def_array.(i); def_array.(suc)] THEN ARITH_TAC in
432 prove(mk_eq(lhs, rhs), proof);;
435 let th_suc_array = Array.init maximum suc_th;;
437 let th_suc_table = Hashtbl.create maximum;;
439 for i = 0 to maximum - 1 do
440 Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i)
443 let SUC_MAX = th_suc_array.(maximum - 1);;
444 let bit_max_name = names_array.(maximum - 1);;
449 let rec raw_suc_conv_hash tm =
451 if (otm = zero_const) then
454 let btm, ntm = dest_comb otm in
455 let cn = fst(dest_const btm) in
456 if (cn = bit_max_name) then
457 let th = INST [ntm, n_var_num] SUC_MAX in
458 let ltm, rtm = dest_comb(rand(concl th)) in
459 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm))
461 INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);;
464 let rec raw_suc_conv_array tm =
466 if (otm = zero_const) then
469 let btm, ntm = dest_comb otm in
470 let cn = fst(dest_const btm) in
471 if (cn = bit_max_name) then
472 let th = INST [ntm, n_var_num] SUC_MAX in
473 let ltm, rtm = dest_comb(rand(concl th)) in
474 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm))
476 INST [ntm, n_var_num] (th_suc_array.(get_index btm));;
480 let NUM_SUC_HASH_CONV tm =
481 let ntm = rand (rand tm) in
482 let th = INST [ntm, n_var_num] SUC_NUM in
483 let lhs, rhs = dest_eq(concl th) in
484 if (lhs <> tm) then failwith("NUM_SUC_HASH_CONV")
486 let ltm, rtm = dest_comb rhs in
487 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));;
494 let x = mk_comb(suc_const, mk_small_numeral_array 99999);;
495 NUM_SUC_HASH_CONV x;;
497 test 50000 NUM_SUC_HASH_CONV x;; (* 5: 0.980 *)
499 let x = mk_comb(suc_const, rand (mk_small_numeral_array 999999));;
501 test 50000 raw_suc_conv_hash x;;
503 test 50000 raw_suc_conv_array x;;
507 (**************************************)
511 let EQ_0_NUM = prove(mk_eq(mk_eq(mk_comb(num_const, n_var_num), `_0`), `n = _0`),
512 REWRITE_TAC[num_def; NUMERAL]);;
514 let EQ_B0_0 = prove(mk_eq(mk_eq(mk_comb(b0_const, n_var_num), `_0`), `n = _0`),
515 REWRITE_TAC[b0_def; ADD_CLAUSES; NUMERAL; REWRITE_RULE[NUMERAL] MULT_EQ_0; ARITH_EQ]);;
517 let EQ_0_0 = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH_EQ]);;
519 let eq_0_lemma = REWRITE_RULE[NUMERAL] (ARITH_RULE `a + b = 0 <=> a = 0 /\ b = 0`);;
522 let concl = mk_eq(mk_eq(mk_comb(const_array.(i), n_var_num), zero_const), false_const) in
523 prove(concl, REWRITE_TAC[def_array.(i); eq_0_lemma; NUMERAL; ARITH_EQ]);;
525 let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);;
527 let th_eq0_table = Hashtbl.create maximum;;
529 for i = 0 to maximum - 1 do
530 Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i)
535 let rec raw_eq0_hash_conv rtm =
536 if (rtm = zero_const) then
539 let b_tm, n_tm = dest_comb rtm in
540 let cn = (fst o dest_const) b_tm in
541 if (cn = b0_name) then
542 let th0 = INST[n_tm, n_var_num] EQ_B0_0 in
543 let th1 = raw_eq0_hash_conv n_tm in
546 INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);;
550 let NUM_EQ0_HASH_CONV rtm =
551 let n_tm = rand rtm in
552 let th = INST [n_tm, n_var_num] EQ_0_NUM in
553 TRANS th (raw_eq0_hash_conv n_tm);;
557 let x = mk_small_numeral_array 0;;
558 NUM_EQ0_HASH_CONV x;;
559 raw_eq0_hash_conv `B0 (B0 _0)`;;
563 (**************************************)
567 let pre_const = `PRE`;;
571 let PRE_NUM = prove(mk_eq(mk_comb(pre_const, mk_comb (num_const, n_var_num)),
572 mk_comb(num_const, mk_comb (pre_const, n_var_num))),
573 REWRITE_TAC[num_def; NUMERAL]);;
576 let PRE_0 = prove(`PRE _0 = _0`,
577 MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
579 let PRE_B1_0 = prove(mk_eq(mk_comb(`PRE`, mk_comb(const_array.(1), `_0`)), `_0`),
580 REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_ADD; NUMERAL; ARITH_PRE; ARITH_EQ]);;
583 let PRE_B0_n0 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> T`,
584 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), `_0`)),
585 REWRITE_TAC[B0_EXPLICIT] THEN
586 DISCH_THEN (fun th -> REWRITE_TAC[th; MUL_n_0]) THEN
587 REWRITE_TAC[NUMERAL; ARITH_PRE]);;
590 let PRE_B0_n1 = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o prove)(mk_imp(`n = 0 <=> F`,
591 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)),
592 mk_comb(const_array.(maximum - 1), `PRE n`))),
593 REWRITE_TAC[B0_EXPLICIT; def_array.(maximum - 1)] THEN ARITH_TAC);;
596 let PRE_lemma = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o ARITH_RULE) `((n = 0) <=> F) ==> (SUC m = n <=> PRE n = m)`;;
601 let pre_tm = mk_comb(const_array.(pre), n_var_num) in
602 let suc_tm = mk_comb(suc_const, pre_tm) in
603 let suc_th = raw_suc_conv_hash suc_tm in
604 let n_tm = rand(concl suc_th) in
605 let n0_th = raw_eq0_hash_conv n_tm in
606 let th0 = INST[pre_tm, m_var_num; n_tm, n_var_num] PRE_lemma in
607 MY_PROVE_HYP n0_th (EQ_MP th0 suc_th);;
612 let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);;
614 let th_pre_table = Hashtbl.create maximum;;
616 for i = 0 to maximum - 1 do
617 Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i)
622 let b1_name = names_array.(1);;
623 let b1_pre_thm = th_pre_array.(1);;
625 let rec raw_pre_hash_conv tm =
627 if (otm = zero_const) then
630 let btm, ntm = dest_comb otm in
631 let cn = fst(dest_const btm) in
632 if (cn = b0_name) then
633 let n_th = raw_eq0_hash_conv ntm in
634 if (rand(concl n_th) = false_const) then
635 let th0 = INST[ntm, n_var_num] PRE_B0_n1 in
636 let th1 = MY_PROVE_HYP n_th th0 in
637 let ltm, rtm = dest_comb(rand(concl th1)) in
638 let th2 = raw_pre_hash_conv rtm in
639 TRANS th1 (AP_TERM ltm th2)
641 let th = INST[ntm, n_var_num] PRE_B0_n0 in
644 if (cn = b1_name) then
645 if (ntm = zero_const) then
648 INST[ntm, n_var_num] b1_pre_thm
650 INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);;
654 let NUM_PRE_HASH_CONV tm =
655 let ntm = rand (rand tm) in
656 let th = INST [ntm, n_var_num] PRE_NUM in
657 let lhs, rhs = dest_eq(concl th) in
658 if (lhs <> tm) then failwith("NUM_PRE_HASH_CONV")
660 let ltm, rtm = dest_comb rhs in
661 TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));;
665 let x = mk_comb(pre_const, mk_small_numeral_array 100000);;
666 NUM_PRE_HASH_CONV x;;
667 (* 10: 0.488; 100: 0.200 *)
668 test 5000 NUM_PRE_HASH_CONV x;;
669 let x = mk_comb(pre_const, mk_small_numeral_array 65536);;
670 (* 10: 0.468; 100: 0.496 *)
671 test 50000 NUM_PRE_HASH_CONV x;;
677 (**************************************)
682 let gt0_table = Hashtbl.create maximum;;
684 let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
686 let gt0_0 = prove(`_0 < _0 <=> F`, REWRITE_TAC[ARITH_LT]);;
687 let gt0_b0 = (REWRITE_RULE[NUMERAL] o prove)(mk_eq (mk_binop lt_op_num `0` (mk_comb(b0_const, n_var_num)), `0 < n`),
688 REWRITE_TAC[b0_def] THEN ARITH_TAC);;
694 let bi = const_array.(i) in
695 let concl = mk_eq (mk_binop lt_op_num zero (mk_comb(bi, n_var_num)), truth_const) in
696 let proof = REWRITE_TAC[def_array.(i)] THEN ARITH_TAC in
697 (PURE_REWRITE_RULE[NUMERAL] o prove)(concl, proof);;
700 for i = 1 to maximum - 1 do
701 Hashtbl.add gt0_table names_array.(i) (gt0_th i)
705 let rec raw_gt0_hash_conv rtm =
706 if (rtm = zero_const) then
709 let b_tm, n_tm = dest_comb rtm in
710 let cn = (fst o dest_const) b_tm in
711 if (cn = b0_name) then
712 let th0 = INST[n_tm, n_var_num] gt0_b0 in
713 let th1 = raw_gt0_hash_conv n_tm in
716 INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);;
720 let NUM_GT0_HASH_CONV rtm =
721 let n_tm = rand rtm in
722 let th = INST [n_tm, n_var_num] GT0_NUM in
723 TRANS th (raw_gt0_hash_conv n_tm);;
729 let tm = mk_binop lt_op_num (mk_small_numeral_array 0) (mk_small_numeral_array 100000);;
730 NUM_GT0_HASH_CONV (rand tm);;
732 test 10000 NUM_GT0_HASH_CONV (rand tm);;
737 (*************************************)
741 let LT_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m < NUMERAL n <=> m < n`, REWRITE_TAC[NUMERAL]);;
742 let LE_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m <= NUMERAL n <=> m <= n`, REWRITE_TAC[NUMERAL]);;
744 let LT_n_0 = prove(`n < _0 <=> F`,
745 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
746 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
749 let LE_0_n = prove(`_0 <= n <=> T`,
750 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
751 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
754 let SUC_LT_THM = ARITH_RULE `SUC m < SUC n <=> m < n`;;
755 let SUC_LE_THM = ARITH_RULE `SUC m <= SUC n <=> m <= n`;;
761 (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *)
763 let bin = mk_comb (const_array.(i), n_var_num) in
764 let lt_tm = mk_binop lt_op_num zero bin in
766 (PURE_REWRITE_RULE[NUMERAL] o EQT_INTRO o prove)(lt_tm, REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
768 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `0 < n`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
771 let th_lt0_table = Hashtbl.create maximum;;
772 for i = 0 to maximum - 1 do
773 let th = gen_0_lt_bi i in
774 let name = names_array.(i) in
775 Hashtbl.add th_lt0_table name th
781 (* Generates the theorem |- bi(m) < bj(n) <=> m <= n (or m < n) *)
783 let gen_bi_lt_bj i j =
784 let bim = mk_comb (const_array.(i), m_var_num) in
785 let bjn = mk_comb (const_array.(j), n_var_num) in
786 let lt_tm = mk_binop lt_op_num bim bjn in
789 mk_binop lt_op_num m_var_num n_var_num
791 mk_binop le_op_num m_var_num n_var_num in
792 prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
796 (* Given a theorem |- bi(m) < bj(n) <=> P m n, generates the theorem
797 |- SUC(bi(m)) < SUC(bj(n)) <=> P m n *)
798 let gen_next_lt_thm th =
799 let ltm, n_tm = (dest_comb o lhand o concl) th in
800 let m_tm = rand ltm in
801 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LT_THM in
802 let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
803 let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
804 let th1 = SYM (MK_COMB ((AP_TERM lt_op_num suc_m), suc_n)) in
805 TRANS (TRANS th1 th0) th;;
808 let th_lt_table = Hashtbl.create (maximum * maximum);;
811 for i = 0 to maximum - 1 do
812 let th = ref (gen_bi_lt_bj 0 i) in
813 let name_left = names_array.(0) and
814 name_right = names_array.(i) in
815 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
817 for k = 1 to maximum - i - 1 do
818 let x = k and y = i + k in
819 let name_left = names_array.(x) and
820 name_right = names_array.(y) in
821 th := gen_next_lt_thm (!th);
822 Hashtbl.add th_lt_table (name_left ^ name_right) !th
827 for i = 1 to maximum - 1 do
828 let th = ref (gen_bi_lt_bj i 0) in
829 let name_left = names_array.(i) and
830 name_right = names_array.(0) in
831 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
833 for k = 1 to maximum - i - 1 do
834 let x = i + k and y = k in
835 let name_left = names_array.(x) and
836 name_right = names_array.(y) in
837 th := gen_next_lt_thm (!th);
838 Hashtbl.add th_lt_table (name_left ^ name_right) !th
847 (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *)
849 let bin = mk_comb (const_array.(i), n_var_num) in
850 let lt_tm = mk_binop le_op_num bin zero in
852 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, false_const), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
854 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `n <= 0`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
858 let th_le0_table = Hashtbl.create maximum;;
859 for i = 0 to maximum - 1 do
860 let th = gen_bi_le_0 i in
861 let name = names_array.(i) in
862 Hashtbl.add th_le0_table name th
868 (* Generates the theorem |- bi(m) <= bj(n) <=> m <= n (or m < n) *)
869 let gen_bi_le_bj i j =
870 let bim = mk_comb (const_array.(i), m_var_num) in
871 let bjn = mk_comb (const_array.(j), n_var_num) in
872 let lt_tm = mk_binop le_op_num bim bjn in
875 mk_binop lt_op_num m_var_num n_var_num
877 mk_binop le_op_num m_var_num n_var_num in
878 prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
882 (* Given a theorem |- bi(m) <= bj(n) <=> P m n, generates the theorem
883 |- SUC(bi(m)) <= SUC(bj(n)) <=> P m n *)
884 let gen_next_le_thm th =
885 let ltm, n_tm = (dest_comb o lhand o concl) th in
886 let m_tm = rand ltm in
887 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LE_THM in
888 let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
889 let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
890 let th1 = SYM (MK_COMB ((AP_TERM le_op_num suc_m), suc_n)) in
891 TRANS (TRANS th1 th0) th;;
895 let th_le_table = Hashtbl.create (maximum * maximum);;
898 for i = 0 to maximum - 1 do
899 let th = ref (gen_bi_le_bj 0 i) in
900 let name_left = names_array.(0) and
901 name_right = names_array.(i) in
902 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
904 for k = 1 to maximum - i - 1 do
905 let x = k and y = i + k in
906 let name_left = names_array.(x) and
907 name_right = names_array.(y) in
908 th := gen_next_le_thm (!th);
909 Hashtbl.add th_le_table (name_left ^ name_right) !th
914 for i = 1 to maximum - 1 do
915 let th = ref (gen_bi_le_bj i 0) in
916 let name_left = names_array.(i) and
917 name_right = names_array.(0) in
918 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
920 for k = 1 to maximum - i - 1 do
921 let x = i + k and y = k in
922 let name_left = names_array.(x) and
923 name_right = names_array.(y) in
924 th := gen_next_le_thm (!th);
925 Hashtbl.add th_le_table (name_left ^ name_right) !th
932 let rec raw_lt_hash_conv tm =
933 let ltm, rtm = dest_comb tm in
934 let ltm = rand ltm in
937 INST[ltm, n_var_num] LT_n_0
941 let bn_tm, n_tm = dest_comb rtm in
942 let cbn = (fst o dest_const) bn_tm in
943 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_lt0_table cbn) in
944 if cbn = b0_name then
945 let th1 = raw_lt_hash_conv (rand (concl th0)) in
951 let bm_tm, m_tm = dest_comb ltm in
952 let bn_tm, n_tm = dest_comb rtm in
953 let cbm = (fst o dest_const) bm_tm in
954 let cbn = (fst o dest_const) bn_tm in
955 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_lt_table (cbm^cbn)) in
956 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
959 raw_lt_hash_conv (rand (concl th0))
961 raw_le_hash_conv (rand (concl th0)) in
964 raw_le_hash_conv tm =
965 let ltm, rtm = dest_comb tm in
966 let ltm = rand ltm in
969 INST[rtm, n_var_num] LE_0_n
973 let bn_tm, n_tm = dest_comb ltm in
974 let cbn = (fst o dest_const) bn_tm in
975 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_le0_table cbn) in
976 if cbn = b0_name then
977 let th1 = raw_le_hash_conv (rand (concl th0)) in
983 let bm_tm, m_tm = dest_comb ltm in
984 let bn_tm, n_tm = dest_comb rtm in
985 let cbm = (fst o dest_const) bm_tm in
986 let cbn = (fst o dest_const) bn_tm in
987 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_le_table (cbm^cbn)) in
988 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
991 raw_lt_hash_conv (rand (concl th0))
993 raw_le_hash_conv (rand (concl th0)) in
998 let NUM_LT_HASH_CONV tm =
999 let atm, rtm = dest_comb tm in
1000 let ltm = rand atm in
1001 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LT_NUM in
1002 let rtm = rand(concl th) in
1003 TRANS th (raw_lt_hash_conv rtm);;
1007 let NUM_LE_HASH_CONV tm =
1008 let atm, rtm = dest_comb tm in
1009 let ltm = rand atm in
1010 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LE_NUM in
1011 let rtm = rand(concl th) in
1012 TRANS th (raw_le_hash_conv rtm);;
1017 let x = num_of_string "3543593547359325353535";;
1018 let y = num_of_string "9392392983247294924242";;
1020 let xx = mk_binop lt_op_num (mk_numeral_array x) (mk_numeral_array y);;
1021 let yy = mk_binop lt_op_num (mk_numeral x) (mk_numeral y);;
1025 test 1000 NUM_LT_CONV yy;;
1027 test 10000 NUM_LT_HASH_CONV xx;;
1033 (**************************************)
1040 let ADD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1041 (`NUMERAL m + NUMERAL n = NUMERAL (m + n)`, REWRITE_TAC[NUMERAL]);;
1044 let CADD_0_n = prove(`SUC (_0 + n) = SUC n`, REWRITE_TAC[ADD_0_n]);;
1045 let CADD_n_0 = prove(`SUC (n + _0) = SUC n`, REWRITE_TAC[ADD_n_0]);;
1047 (* B0 (SUC n) = B0 n + maximum *)
1048 let B0_SUC = prove(mk_eq(mk_comb(b0_const, mk_comb(suc_const, n_var_num)),
1049 mk_binop plus_op_num max_const (mk_comb(b0_const, n_var_num))),
1050 REWRITE_TAC [B0_EXPLICIT] THEN ARITH_TAC);;
1052 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)),
1053 mk_comb(b0_const, mk_binop plus_op_num m_var_num n_var_num)),
1054 REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
1056 let SUC_ADD_RIGHT = prove(`SUC(m + n) = m + SUC n`, ARITH_TAC);;
1059 (* Generate all theorems iteratively *)
1061 let th_add_right_next th =
1062 let lhs, rhs = dest_eq(concl th) in
1063 let ltm, rtm = dest_comb rhs in
1064 let cn = fst(dest_const ltm) in
1065 let suc_th = AP_TERM suc_const th in
1066 let th_rhs = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1067 let ltm, rarg = dest_comb lhs in
1068 let larg = rand ltm in
1069 let th1 = INST[larg, m_var_num; rarg, n_var_num] SUC_ADD_RIGHT in
1070 let cn = fst(dest_const(rator rarg)) in
1071 let th2 = Hashtbl.find th_suc_table cn in
1072 let th_lhs = TRANS th1 (AP_TERM ltm th2) in
1073 TRANS (TRANS (SYM th_lhs) suc_th) th_rhs;;
1076 let th_add_array = Array.make (maximum * maximum) (REFL zero_const);;
1078 for i = 0 to maximum - 1 do
1083 INST[n_var_num, m_var_num; m_var_num, n_var_num]
1084 (ONCE_REWRITE_RULE[ADD_AC] th_add_array.(i)) in
1085 let _ = th_add_array.(i * maximum) <- th0 in
1087 for j = 1 to maximum - 1 do
1088 th_add_array.(i * maximum + j) <- th_add_right_next th_add_array.(i * maximum + j - 1)
1093 (* SUC (B_i(m) + B_j(n)) = B_p(...) *)
1095 let add_th = th_add_array.(i * maximum + j) in
1096 let th0 = AP_TERM suc_const add_th in
1097 let ltm, rtm = dest_comb(rand(concl th0)) in
1098 let ltm, rtm = dest_comb rtm in
1099 let cn = fst(dest_const ltm) in
1100 let suc_th = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1104 let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);;
1106 for i = 0 to maximum - 1 do
1107 for j = 0 to maximum - 1 do
1108 th_cadd_array.(i * maximum + j) <- th_cadd i j
1114 let th_add_table = Hashtbl.create (maximum * maximum);;
1116 for i = 0 to maximum - 1 do
1117 for j = 0 to maximum - 1 do
1118 let name = names_array.(i) ^ names_array.(j) in
1119 let th = th_add_array.(i * maximum + j) in
1120 let cflag = (i + j >= maximum) in
1121 Hashtbl.add th_add_table name (th, cflag)
1127 let th_cadd_table = Hashtbl.create (maximum * maximum);;
1129 for i = 0 to maximum - 1 do
1130 for j = 0 to maximum - 1 do
1131 let name = names_array.(i) ^ names_array.(j) in
1132 let th = th_cadd_array.(i * maximum + j) in
1133 let cflag = (i + j + 1 >= maximum) in
1134 Hashtbl.add th_cadd_table name (th, cflag)
1140 (* ADD conversion *)
1143 let rec raw_add_conv_hash tm =
1144 let atm,rtm = dest_comb tm in
1145 let ltm = rand atm in
1146 if ltm = zero_const then
1147 INST [rtm,n_var_num] ADD_0_n
1148 else if rtm = zero_const then
1149 INST [ltm,n_var_num] ADD_n_0
1151 let lbit,larg = dest_comb ltm
1152 and rbit,rarg = dest_comb rtm in
1153 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1154 let th0, cflag = Hashtbl.find th_add_table name in
1155 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1156 let ltm, rtm = dest_comb(rand(concl th)) in
1158 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1160 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm))
1161 and raw_adc_conv_hash tm =
1162 let atm,rtm = dest_comb (rand tm) in
1163 let ltm = rand atm in
1164 if ltm = zero_const then
1165 let th = INST [rtm,n_var_num] CADD_0_n in
1166 TRANS th (raw_suc_conv_hash (rand(concl th)))
1167 else if rtm = zero_const then
1168 let th = INST [ltm,n_var_num] CADD_n_0 in
1169 TRANS th (raw_suc_conv_hash (rand(concl th)))
1171 let lbit,larg = dest_comb ltm
1172 and rbit,rarg = dest_comb rtm in
1173 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1174 let th0, cflag = Hashtbl.find th_cadd_table name in
1175 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1176 let ltm, rtm = dest_comb(rand(concl th)) in
1178 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1180 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1183 let NUM_ADD_HASH_CONV tm =
1184 let atm, rtm = dest_comb tm in
1185 let ltm = rand atm in
1186 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] ADD_NUM in
1187 let ltm, rtm = dest_comb(rand(concl th)) in
1188 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1192 let x = num_of_string "3543593547359325353535";;
1193 let y = num_of_string "9392392983247294924242";;
1195 let xx = mk_binop plus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1196 let yy = mk_binop plus_op_num (mk_numeral x) (mk_numeral y);;
1198 NUM_ADD_HASH_CONV xx;;
1200 test 10000 NUM_ADD_CONV yy;; (* 5.672 *)
1202 test 10000 NUM_ADD_HASH_CONV xx;;
1205 (********************************)
1209 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)),
1210 mk_comb(num_const, mk_binop minus_op_num m_var_num n_var_num)),
1211 REWRITE_TAC[num_def; NUMERAL]);;
1213 let SUB_lemma1 = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> m - n = t:num`;;
1214 let SUB_lemma2 = (UNDISCH_ALL o REWRITE_RULE[NUMERAL] o ARITH_RULE) `m + t = n ==> m - n = 0`;;
1215 let LE_lemma = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> n <= m:num`;;
1218 let raw_sub_hash_conv tm =
1219 let ltm, n_tm = dest_comb tm in
1220 let m_tm = rand ltm in
1221 let m = raw_dest_hash m_tm in
1222 let n = raw_dest_hash n_tm in
1225 let t_tm = rand (mk_numeral_array t) in
1226 let th0 = INST[n_tm, n_var_num; t_tm, t_var_num; m_tm, m_var_num] SUB_lemma1 in
1227 let th_add = raw_add_conv_hash (mk_binop plus_op_num n_tm t_tm) in
1228 MY_PROVE_HYP th_add th0
1230 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1231 let th0 = INST[m_tm, m_var_num; t_tm, t_var_num; n_tm, n_var_num] SUB_lemma2 in
1232 let th_add = raw_add_conv_hash (mk_binop plus_op_num m_tm t_tm) in
1233 MY_PROVE_HYP th_add th0;;
1237 (* Returns either (tm1 - tm2, tm2 <= tm1) or (tm2 - tm1, tm1 <= tm2) *)
1238 let raw_sub_and_le_hash_conv tm1 tm2 =
1239 let m = raw_dest_hash tm1 in
1240 let n = raw_dest_hash tm2 in
1243 let t_tm = rand (mk_numeral_array t) in
1244 let inst = INST[tm2, n_var_num; t_tm, t_var_num; tm1, m_var_num] in
1245 let th_sub = inst SUB_lemma1 in
1246 let th_le = inst LE_lemma in
1247 let th_add = raw_add_conv_hash (mk_binop plus_op_num tm2 t_tm) in
1248 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le)
1250 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1251 let inst = INST[tm2, m_var_num; t_tm, t_var_num; tm1, n_var_num] in
1252 let th_sub = inst SUB_lemma1 in
1253 let th_le = inst LE_lemma in
1254 let th_add = raw_add_conv_hash (mk_binop plus_op_num tm1 t_tm) in
1255 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le);;
1259 let NUM_SUB_HASH_CONV tm =
1260 let atm, rtm = dest_comb tm in
1261 let ltm = rand atm in
1262 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] SUB_NUM in
1263 let ltm, rtm = dest_comb(rand(concl th)) in
1264 TRANS th (AP_TERM ltm (raw_sub_hash_conv rtm));;
1268 let y = num_of_string "3543593547359325353535";;
1269 let x = num_of_string "9392392983247294924242";;
1271 let xx = mk_binop minus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1272 let yy = mk_binop minus_op_num (mk_numeral x) (mk_numeral y);;
1274 NUM_SUB_HASH_CONV xx;;
1276 test 1000 NUM_SUB_CONV yy;; (* 2.376 *)
1278 test 1000 NUM_SUB_HASH_CONV xx;;
1283 (********************************)
1285 (* Multiplication *)
1287 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)),
1288 mk_comb(num_const, mk_binop mul_op_num m_var_num n_var_num)),
1289 REWRITE_TAC[num_def; NUMERAL]);;
1291 let MUL_0_n = prove(`_0 * n = _0`, ONCE_REWRITE_TAC[GSYM NUM_THM] THEN
1292 ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN REWRITE_TAC[num_def] THEN
1293 REWRITE_TAC[MULT_CLAUSES]);;
1295 let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;;
1297 let MUL_1_n, MUL_n_1 =
1298 let one_const = mk_comb (const_array.(1), zero) in
1299 let cond = mk_eq(mk_binop mul_op_num one_const n_var_num, n_var_num) in
1300 let th = (REWRITE_RULE[NUMERAL] o prove)(cond, REWRITE_TAC[def_array.(1)] THEN ARITH_TAC) in
1301 th, ONCE_REWRITE_RULE[MULT_AC] th;;
1305 let MUL_B0_t = prove(mk_eq(mk_binop mul_op_num (mk_comb(b0_const, n_var_num)) t_var_num,
1306 mk_comb(b0_const, mk_binop mul_op_num n_var_num t_var_num)),
1307 REWRITE_TAC[def_array.(0)] THEN ARITH_TAC);;
1310 let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
1313 let MUL_SUC_RIGHT = prove(`m * SUC(n) = m * n + m`, ARITH_TAC);;
1316 (* Multiplication table *)
1318 let mul_th_next_right th =
1319 let ltm, rtm = dest_comb(rand(rator(concl th))) in
1320 let mtm = rand ltm in
1321 let th0 = INST[mtm, m_var_num; rtm, n_var_num] MUL_SUC_RIGHT in
1322 let th1 = AP_THM (AP_TERM plus_op_num th) mtm in
1323 let sum_th = raw_add_conv_hash (rand(concl th1)) in
1324 let th2 = TRANS (TRANS th0 th1) sum_th in
1325 let cn = fst(dest_const (rator rtm)) in
1326 let th_suc = INST[zero_const, n_var_num] (Hashtbl.find th_suc_table cn) in
1327 let th3 = AP_TERM (mk_comb (mul_op_num, mtm)) th_suc in
1328 TRANS (SYM th3) th2;;
1331 let mul_array = Array.make (maximum * maximum) (REFL zero_const);;
1332 for i = 1 to maximum - 1 do
1333 let th1 = INST[mk_comb(const_array.(i), zero_const), n_var_num] MUL_n_1 in
1334 let _ = mul_array.(i * maximum + 1) <- th1 in
1336 for j = 2 to maximum - 1 do
1337 mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1)
1343 let mul_table = Hashtbl.create (maximum * maximum);;
1344 for i = 1 to maximum - 1 do
1345 for j = 1 to maximum - 1 do
1346 Hashtbl.add mul_table (names_array.(i) ^ names_array.(j)) mul_array.(i * maximum + j)
1351 (* General multiplication theorem *)
1354 let mul (a,b) = mk_binop mul_op_num a b and
1355 add (a,b) = mk_binop plus_op_num a b in
1356 let lhs = mul(add(t_var_num, mk_comb(b0_const, m_var_num)),
1357 add(r_var_num, mk_comb(b0_const, n_var_num))) in
1358 let rhs = add(mul(t_var_num, r_var_num),
1359 mk_comb(b0_const, add(mk_comb(b0_const, mul(m_var_num, n_var_num)),
1360 add(mul(m_var_num, r_var_num),
1361 mul(n_var_num, t_var_num))))) in
1362 prove(mk_eq(lhs, rhs),
1363 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1364 REWRITE_TAC[MUL_B0_t; MUL_t_B0] THEN
1365 ONCE_REWRITE_TAC[GSYM ADD_ASSOC] THEN
1366 REWRITE_TAC[th_add_array.(0)] THEN
1367 REWRITE_TAC[ADD_AC; MULT_AC]);;
1369 let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;;
1372 let ltm, rtm = dest_comb tm in
1376 (* B_i(m) * B_j(n) = B_p(B_q(m * n) + m * B_j(0) + n * B_i(0))
1377 where B_p(B_q(0)) = i * j *)
1378 let gen_mul_thm i j =
1379 let bi0 = mk_comb(const_array.(i), zero_const) and
1380 bj0 = mk_comb(const_array.(j), zero_const) in
1381 let def_i = INST[m_var_num, n_var_num] def_thm_array.(i) in
1382 let def_j = def_thm_array.(j) in
1383 let th0 = MK_COMB(AP_TERM mul_op_num def_i, def_j) in
1384 let th1 = TRANS th0 (INST[bi0, t_var_num; bj0, r_var_num] prod_lemma) in
1385 let mul_th = mul_array.(i * maximum + j) in
1386 let larg, rarg = dest_op (rand (concl th1)) in
1387 let th2 = TRANS th1 (AP_THM (AP_TERM plus_op_num mul_th) rarg) in
1388 let larg = rand(concl mul_th) in
1389 let b_low, b_high = dest_comb larg in
1390 let rtm = rand(rarg) in
1391 let th_add = INST[b_high, m_var_num; rtm, n_var_num]
1392 (fst(Hashtbl.find th_add_table (fst(dest_const b_low)^b0_name))) in
1393 if i * j < maximum then
1394 let ltm, rtm = dest_op(rand(rand(concl th_add))) in
1395 let add_0 = AP_TERM b_low (INST[rtm, n_var_num] ADD_0_n) in
1396 TRANS th2 (TRANS th_add add_0)
1398 let larg, rtm = dest_op (rand(rand(concl th_add))) in
1399 let rarg, rtm = dest_op rtm in
1400 let th_assoc = INST[larg, m_var_num; rarg, n_var_num; rtm, p_var_num] ADD_ASSOC' in
1401 let mn = rand(rarg) in
1402 let b_high = rator b_high in
1403 let th_add2' = INST[zero_const, m_var_num; mn, n_var_num]
1404 (fst(Hashtbl.find th_add_table (fst(dest_const b_high)^b0_name))) in
1405 let add_0 = AP_TERM b_high (INST[mn, n_var_num] ADD_0_n) in
1406 let th_add2 = TRANS th_add2' add_0 in
1407 let th3 = TRANS th_assoc (AP_THM (AP_TERM plus_op_num th_add2) rtm) in
1408 let th4 = TRANS th_add (AP_TERM b_low th3) in
1412 let gen_mul_table = Hashtbl.create (maximum * maximum);;
1414 for i = 1 to maximum - 1 do
1415 for j = 1 to maximum - 1 do
1416 let name = names_array.(i) ^ names_array.(j) in
1417 Hashtbl.add gen_mul_table name (gen_mul_thm i j)
1422 (* B_i(m) * B_j(0) = B_p(B_q(0) + m * B_j(0))
1423 where i * j = B_p(B_q(0)) *)
1424 let mul1_right_th i j =
1425 let th0 = INST[zero_const, n_var_num]
1426 (Hashtbl.find gen_mul_table (names_array.(i)^names_array.(j))) in
1427 let b_low, rtm = dest_comb(rand(concl th0)) in
1428 let tm1, tm23 = dest_op rtm in
1429 let tm2p, tm3 = dest_comb tm23 in
1430 let tm3_th = INST[rand tm3, n_var_num] MUL_0_n in
1431 let tm2_th = INST[rand(tm2p), n_var_num] ADD_n_0 in
1432 let tm23_th = TRANS (AP_TERM tm2p tm3_th) tm2_th in
1433 let ltm, rtm = dest_comb tm1 in
1434 if (i * j < maximum) then
1435 let tm1_th = TRANS (AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0)) B0_0 in
1436 let tm123_th' = TRANS (INST[tm23, n_var_num] ADD_0_n) tm23_th in
1437 let tm123_th = TRANS (AP_THM (AP_TERM plus_op_num tm1_th) tm23) tm123_th' in
1438 TRANS th0 (AP_TERM b_low tm123_th)
1440 let tm1_th = AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0) in
1441 let tm123_th = MK_COMB(AP_TERM plus_op_num tm1_th, tm23_th) in
1442 TRANS th0 (AP_TERM b_low tm123_th);;
1445 (* B_j(0) * B_i(m) = B_p(B_q(0) + B_j(0) * B_i(m) *)
1447 let MULT_AC' = CONJUNCT1 MULT_AC;;
1449 let mul1_left_th th =
1450 let lhs, rhs = dest_eq(concl th) in
1451 let ltm, rtm = dest_op lhs in
1452 let th_lhs = INST[ltm, n_var_num; rtm, m_var_num] MULT_AC' in
1453 let btm, rtm = dest_comb rhs in
1454 let larg, rarg = dest_op rtm in
1455 if (is_comb larg) then
1456 let ltm, rtm = dest_op rarg in
1457 let th_rhs' = INST[ltm, m_var_num; rtm, n_var_num] MULT_AC' in
1458 let th_rhs = AP_TERM (mk_comb(plus_op_num, larg)) th_rhs' in
1459 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs))
1461 let th_rhs = INST[larg, m_var_num; rarg, n_var_num] MULT_AC' in
1462 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs));;
1467 let mul1_right_th_table = Hashtbl.create (maximum * maximum);;
1468 let mul1_left_th_table = Hashtbl.create (maximum * maximum);;
1470 for i = 1 to maximum - 1 do
1471 for j = 1 to maximum - 1 do
1472 let name_right = names_array.(i) ^ names_array.(j) in
1473 let name_left = names_array.(j) ^ names_array.(i) in
1474 let th = mul1_right_th i j in
1475 let add_flag = (i * j >= maximum) in
1476 let _ = Hashtbl.add mul1_right_th_table name_right (add_flag, th) in
1477 Hashtbl.add mul1_left_th_table name_left (add_flag, mul1_left_th th)
1483 (******************************************************)
1488 (* Multiplies arg and (tm = tmname(_0)) *)
1489 let rec raw_mul1_right_hash arg tm tmname =
1490 if arg = zero_const then
1491 INST [tm, n_var_num] MUL_0_n
1493 let btm, mtm = dest_comb arg in
1494 let cn = fst(dest_const btm) in
1495 if (cn = b0_name) then
1496 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_B0_t in
1497 TRANS th (AP_TERM b0_const (raw_mul1_right_hash mtm tm tmname))
1499 let name = cn ^ tmname in
1500 if (mtm = zero_const) then
1501 Hashtbl.find mul_table name
1503 let add_flag, th' = Hashtbl.find mul1_right_th_table name in
1504 let th = INST[mtm, m_var_num] th' in
1506 let ltm, rtm = dest_comb(rand(concl th)) in
1507 let lplus, rarg = dest_comb rtm in
1508 let th2 = AP_TERM lplus (raw_mul1_right_hash mtm tm tmname) in
1509 let th_add = raw_add_conv_hash (rand(concl th2)) in
1510 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1512 let ltm = rator(rand(concl th)) in
1513 let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in
1517 (* Multiplies (tm = tmname(_0)) and arg *)
1518 let rec raw_mul1_left_hash tm tmname arg =
1519 if arg = zero_const then
1520 INST [tm, n_var_num] MUL_n_0
1522 let btm, mtm = dest_comb arg in
1523 let cn = fst(dest_const btm) in
1524 if (cn = b0_name) then
1525 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_t_B0 in
1526 TRANS th (AP_TERM b0_const (raw_mul1_left_hash tm tmname mtm))
1528 let name = tmname ^ cn in
1529 if (mtm = zero_const) then
1530 Hashtbl.find mul_table name
1532 let add_flag, th' = Hashtbl.find mul1_left_th_table name in
1533 let th = INST[mtm, m_var_num] th' in
1535 let ltm, rtm = dest_comb(rand(concl th)) in
1536 let lplus, rarg = dest_comb rtm in
1537 let th2 = AP_TERM lplus (raw_mul1_left_hash tm tmname mtm) in
1538 let th_add = raw_add_conv_hash (rand(concl th2)) in
1539 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1541 let ltm = rator(rand(concl th)) in
1542 let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in
1546 (* Computes B_i(m) * B_j(n) *)
1547 let rec raw_mul_conv_hash tm =
1548 let larg, rarg = dest_comb tm in
1549 let larg = rand larg in
1550 if larg = zero_const then
1551 INST [rarg, n_var_num] MUL_0_n
1552 else if rarg = zero_const then
1553 INST [larg, n_var_num] MUL_n_0
1556 let lbtm, mtm = dest_comb larg in
1557 let lcn = fst(dest_const lbtm) in
1558 if (lcn = b0_name) then
1559 let th = INST[rarg, t_var_num; mtm, n_var_num] MUL_B0_t in
1560 let ltm, rtm = dest_comb(rand(concl th)) in
1561 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1563 let rbtm, ntm = dest_comb rarg in
1564 let rcn = fst(dest_const rbtm) in
1565 if (rcn = b0_name) then
1566 let th = INST[larg, t_var_num; ntm, n_var_num] MUL_t_B0 in
1567 let ltm, rtm = dest_comb(rand(concl th)) in
1568 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1571 if (ntm = zero_const) then
1572 if (mtm = zero_const) then
1573 Hashtbl.find mul_table (lcn ^ rcn)
1575 raw_mul1_right_hash larg (mk_comb(rbtm, zero_const)) rcn
1576 else if (mtm = zero_const) then
1577 raw_mul1_left_hash (mk_comb(lbtm, zero_const)) lcn rarg
1580 let th0 = INST[mtm, m_var_num; ntm, n_var_num]
1581 (Hashtbl.find gen_mul_table (lcn ^ rcn)) in
1582 let b_low, expr = dest_comb(rand(concl th0)) in
1583 let ltm, rsum = dest_comb expr in
1584 let b_high, mul0 = dest_comb (rand ltm) in
1585 let th_mul0 = raw_mul_conv_hash mul0 in
1586 let th_mul1 = raw_mul1_right_hash mtm (mk_comb(rbtm, zero_const)) rcn in
1587 let th_mul2 = raw_mul1_right_hash ntm (mk_comb(lbtm, zero_const)) lcn in
1588 let th_larg = AP_TERM plus_op_num (AP_TERM b_high th_mul0) in
1589 let th_rarg = MK_COMB(AP_TERM plus_op_num th_mul1, th_mul2) in
1591 let add_rarg = TRANS th_rarg (raw_add_conv_hash (rand(concl th_rarg))) in
1592 let add_th = MK_COMB (th_larg, add_rarg) in
1593 let add = TRANS add_th (raw_add_conv_hash (rand(concl add_th))) in
1595 TRANS th0 (AP_TERM b_low add);;
1599 (* The main multiplication conversion *)
1600 let NUM_MULT_HASH_CONV tm =
1601 let ltm, rtm = dest_comb tm in
1602 let larg, rarg = rand (rand ltm), rand rtm in
1603 let th0 = INST[larg, m_var_num; rarg, n_var_num] MUL_NUM in
1604 if (rand(rator(concl th0)) <> tm) then
1605 failwith "NUM_MULT_HASH_CONV"
1607 let rtm = rand(rand(concl th0)) in
1608 let th = raw_mul_conv_hash rtm in
1609 TRANS th0 (AP_TERM num_const th);;
1613 (**************************)
1618 let x = Int 325325353;;
1619 let y = Int 999434312;;
1621 let xx = mk_binop mul_op_num (mk_numeral_array x) (mk_numeral_array y);;
1622 let yy = mk_binop mul_op_num (mk_numeral x) (mk_numeral y);;
1623 let zz = rand(concl(REWRITE_CONV[NUM_THM] xx));;
1625 NUM_MULT_HASH_CONV xx;;
1627 test 1000 NUM_MULT_CONV yy;; (* 4.12 *)
1629 test 1000 NUM_MULT_HASH_CONV xx;; (* 4: 1.69; 6: 0.716(1), 0.608(2), 8: 0.328(3) *)
1631 test 1000 raw_mul_conv_hash zz;; (* 4: 2.45(1), 1.576(2), 8: 0.320 *)
1634 needs "example0.hl";;
1636 let x = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral t1) (mk_numeral t2)) example;;
1637 let h1 = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral_array t1) (mk_numeral_array t2)) example;;
1638 let h2 = map (fun t1, t2 -> mk_binop mul_op_num
1639 (rand (mk_numeral_array t1))
1640 (rand (mk_numeral_array t2))) example;;
1643 test 1 (map NUM_MULT_CONV) x;; (* 2.64 *)
1644 test 10 (map NUM_MULT_HASH_CONV) h1;; (* 4: 5.43; 6: 3.12; 8: 1.67 *)
1645 test 10 (map raw_mul_conv_hash) h2;; (* 5.42; 8: 1.576 *)
1650 (************************************)
1655 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)),
1656 mk_comb(num_const, mk_binop div_op_num m_var_num n_var_num)),
1657 REWRITE_TAC[num_def; NUMERAL]);;
1660 let DIV_UNIQ' = (UNDISCH_ALL o
1661 PURE_ONCE_REWRITE_RULE[ARITH_RULE `a < b <=> (a < b:num <=> T)`] o
1662 ONCE_REWRITE_RULE[ARITH_RULE `m = q * n + r <=> q * n + r = m:num`] o
1663 REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL) DIV_UNIQ;;
1665 (* Computes m DIV n *)
1666 let raw_div_hash_conv tm =
1667 let ltm, n_tm = dest_comb tm in
1668 let m_tm = rand ltm in
1669 let m = raw_dest_hash m_tm in
1670 let n = raw_dest_hash n_tm in
1671 let q = Num.quo_num m n and
1672 r = Num.mod_num m n in
1673 let q_tm = rand (mk_numeral_array q) and
1674 r_tm = rand (mk_numeral_array r) in
1676 let qn_th = raw_mul_conv_hash (mk_binop mul_op_num q_tm n_tm) in
1677 let qn_tm = rand (concl qn_th) in
1678 let qnr_th = raw_add_conv_hash (mk_binop plus_op_num qn_tm r_tm) in
1679 let th1 = TRANS (AP_THM (AP_TERM plus_op_num qn_th) r_tm) qnr_th in
1680 let th2 = raw_lt_hash_conv (mk_binop lt_op_num r_tm n_tm) in
1681 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
1682 MY_PROVE_HYP th1 (MY_PROVE_HYP th2 th0);;
1686 (* The main division conversion *)
1687 let NUM_DIV_HASH_CONV tm =
1688 let ltm, rtm = dest_comb tm in
1689 let larg, rarg = rand (rand ltm), rand rtm in
1690 let th0 = INST[larg, m_var_num; rarg, n_var_num] DIV_NUM in
1691 if (rand(rator(concl th0)) <> tm) then
1692 failwith "NUM_DIV_HASH_CONV"
1694 let rtm = rand(rand(concl th0)) in
1695 let th = raw_div_hash_conv rtm in
1696 TRANS th0 (AP_TERM num_const th);;
1700 let y = num_of_string "3543593547359";;
1701 let x = num_of_string "9392392983247294924242";;
1704 let xx = mk_binop div_op_num (mk_numeral_array x) (mk_numeral_array y);;
1705 let yy = mk_binop div_op_num (mk_numeral x) (mk_numeral y);;
1708 test 100 NUM_DIV_CONV yy;;
1710 test 100 NUM_DIV_HASH_CONV xx;;
1715 (*********************************************)
1717 (* EVEN_CONV, ODD_CONV *)
1719 let even_const = `EVEN` and
1720 odd_const = `ODD` and
1721 eq_const = `<=>` and
1727 let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1728 (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);;
1730 let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1731 (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
1733 let EVEN_ZERO = prove(`EVEN _0 <=> T`, REWRITE_TAC[ARITH_EVEN]);;
1734 let ODD_ZERO = prove(`ODD _0 <=> F`, REWRITE_TAC[ARITH_ODD]);;
1737 let EVEN_B0 = prove(mk_eq(mk_comb(`EVEN`, mk_comb(b0_const, `n:num`)), `T`),
1738 REWRITE_TAC[B0_EXPLICIT; EVEN_MULT] THEN
1739 DISJ1_TAC THEN CONV_TAC NUM_EVEN_CONV);;
1742 let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
1743 REWRITE_TAC[NOT_ODD; EVEN_B0]);;
1745 let EVEN_SUC_T = prove(`(EVEN (SUC n) <=> T) <=> (EVEN n <=> F)`, REWRITE_TAC[EVEN]);;
1746 let EVEN_SUC_F = prove(`(EVEN (SUC n) <=> F) <=> (EVEN n <=> T)`, REWRITE_TAC[EVEN]);;
1748 let ODD_SUC_T = prove(`(ODD (SUC n) <=> T) <=> (ODD n <=> F)`, REWRITE_TAC[ODD]);;
1749 let ODD_SUC_F = prove(`(ODD (SUC n) <=> F) <=> (ODD n <=> T)`, REWRITE_TAC[ODD]);;
1753 let next_even_th th =
1754 let ltm, rtm = dest_comb(concl th) in
1755 let b_tm = rand(rand ltm) in
1756 let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1757 let flag = (fst o dest_const) rtm = "T" in
1758 let th0 = SYM (AP_TERM even_const suc_b) in
1759 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1760 let th2 = INST[b_tm, n_var_num] (if flag then EVEN_SUC_F else EVEN_SUC_T) in
1761 EQ_MP (SYM (TRANS th1 th2)) th;;
1764 let next_odd_th th =
1765 let ltm, rtm = dest_comb(concl th) in
1766 let b_tm = rand(rand ltm) in
1767 let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1768 let flag = (fst o dest_const) rtm = "T" in
1769 let th0 = SYM (AP_TERM odd_const suc_b) in
1770 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1771 let th2 = INST[b_tm, n_var_num] (if flag then ODD_SUC_F else ODD_SUC_T) in
1772 EQ_MP (SYM (TRANS th1 th2)) th;;
1775 let even_thm_table = Hashtbl.create maximum;;
1778 Hashtbl.add even_thm_table names_array.(0) EVEN_B0;;
1781 for i = 1 to maximum - 1 do
1782 let th0 = next_even_th (Hashtbl.find even_thm_table names_array.(i - 1)) in
1783 Hashtbl.add even_thm_table names_array.(i) th0
1787 let odd_thm_table = Hashtbl.create maximum;;
1789 Hashtbl.add odd_thm_table names_array.(0) ODD_B0;;
1791 for i = 1 to maximum - 1 do
1792 let th0 = next_odd_th (Hashtbl.find odd_thm_table names_array.(i - 1)) in
1793 Hashtbl.add odd_thm_table names_array.(i) th0
1797 let raw_even_hash_conv tm =
1798 let ltm, rtm = dest_comb tm in
1799 if ((fst o dest_const) ltm <> "EVEN") then
1800 failwith "raw_even_hash_conv: no EVEN"
1802 if (is_const rtm) then
1805 let b_tm, n_tm = dest_comb rtm in
1806 let th0 = Hashtbl.find even_thm_table ((fst o dest_const) b_tm) in
1807 INST[n_tm, n_var_num] th0;;
1810 let raw_odd_hash_conv tm =
1811 let ltm, rtm = dest_comb tm in
1812 if ((fst o dest_const) ltm <> "ODD") then
1813 failwith "raw_odd_hash_conv: no ODD"
1815 if (is_const rtm) then
1818 let b_tm, n_tm = dest_comb rtm in
1819 let th0 = Hashtbl.find odd_thm_table ((fst o dest_const) b_tm) in
1820 INST[n_tm, n_var_num] th0;;
1824 let NUM_EVEN_HASH_CONV tm =
1825 let ltm, rtm = dest_comb tm in
1826 let th0 = INST[rand rtm, n_var_num] EVEN_NUM in
1827 let ltm, rtm = dest_comb(concl th0) in
1828 if (rand ltm <> tm) then
1829 failwith "NUM_EVEN_HASH_CONV"
1831 let th1 = raw_even_hash_conv rtm in
1835 let NUM_ODD_HASH_CONV tm =
1836 let ltm, rtm = dest_comb tm in
1837 let th0 = INST[rand rtm, n_var_num] ODD_NUM in
1838 let ltm, rtm = dest_comb(concl th0) in
1839 if (rand ltm <> tm) then
1840 failwith "NUM_ODD_HASH_CONV"
1842 let th1 = raw_odd_hash_conv rtm in