1 (* =========================================================== *)
2 (* Formal natural arithmetic with an arbitrary base *)
3 (* Author: Alexey Solovyev *)
5 (* =========================================================== *)
7 module type Arith_hash_sig =
13 val const_array : term array
14 val def_array: thm array
15 val def_thm_array: thm array
16 val mk_numeral_hash : num -> term
17 val mk_numeral_array : num -> term
18 val mk_small_numeral_array : int -> term
19 val raw_dest_hash : term -> num
20 val dest_numeral_hash : term -> num
21 val NUMERAL_TO_NUM_CONV : term -> thm
22 val NUM_TO_NUMERAL_CONV : term -> thm
24 val raw_suc_conv_hash : term -> thm
25 val NUM_SUC_HASH_CONV : term -> thm
27 val raw_eq0_hash_conv : term -> thm
28 val NUM_EQ0_HASH_CONV : term -> thm
30 val raw_pre_hash_conv : term -> thm
31 val NUM_PRE_HASH_CONV : term -> thm
33 val raw_gt0_hash_conv : term -> thm
34 val NUM_GT0_HASH_CONV : term -> thm
36 val raw_eq_hash_conv : term -> thm
37 val NUM_EQ_HASH_CONV : term -> thm
39 val raw_lt_hash_conv : term -> thm
40 val raw_le_hash_conv : term -> thm
41 val NUM_LT_HASH_CONV : term -> thm
42 val NUM_LE_HASH_CONV : term -> thm
44 val raw_add_conv_hash : term -> thm
45 val NUM_ADD_HASH_CONV : term -> thm
47 val raw_sub_hash_conv : term -> thm
48 val raw_sub_and_le_hash_conv : term -> term -> thm * thm
49 val NUM_SUB_HASH_CONV : term -> thm
51 val raw_mul_conv_hash : term -> thm
52 val NUM_MULT_HASH_CONV : term -> thm
54 val raw_div_hash_conv : term -> thm
55 val NUM_DIV_HASH_CONV : term -> thm
57 val raw_even_hash_conv : term -> thm
58 val raw_odd_hash_conv : term -> thm
59 val NUM_EVEN_HASH_CONV : term -> thm
60 val NUM_ODD_HASH_CONV : term -> thm
64 needs "misc/misc.hl";;
65 needs "misc/vars.hl";;
66 needs "arith_options.hl";;
68 module Arith_hash : Arith_hash_sig = struct
73 let arith_base = !Arith_options.base;;
74 let maximum = arith_base;;
78 (* Generate definitions and constants *)
80 let fnum_type = `:num->num` and
81 numeral_const = `NUMERAL` and
82 bit0_const = `BIT0` and
85 (* Names of constants which define "digits" *)
86 let names_array = Array.init maximum (fun i -> "D"^(string_of_int i));;
89 let num_name = "NUM"^(string_of_int arith_base);;
90 let num_def = new_basic_definition (mk_eq(mk_var(num_name, fnum_type), numeral_const));;
91 let num_const = mk_const(num_name, []);;
92 let num_def_sym = SYM num_def;;
95 let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
96 REWRITE_TAC[num_def; NUMERAL]);;
98 (* |- D_i(n) = i + D_0(n) *)
99 let mk_bit_definition i =
100 let lhs = mk_var (names_array.(i), fnum_type) in
101 let tm1 = mk_binop mul_op_num (mk_small_numeral arith_base) n_var_num in
102 let tm2 = mk_binop add_op_num tm1 (mk_small_numeral i) in
103 let rhs = mk_abs (n_var_num, tm2) in
104 new_basic_definition (mk_eq (lhs, rhs));;
106 let def_basic_array = Array.init maximum mk_bit_definition;;
107 let def_array = Array.init maximum (fun i ->
108 let basic = def_basic_array.(i) in
109 let th1 = AP_THM basic n_var_num in
110 TRANS th1 (BETA (rand (concl th1))));;
111 let def_table = Hashtbl.create maximum;;
112 let def_basic_table = Hashtbl.create maximum;;
114 for i = 0 to maximum - 1 do
115 let _ = Hashtbl.add def_table names_array.(i) def_array.(i) in
116 Hashtbl.add def_basic_table names_array.(i) def_basic_array.(i)
121 let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));;
123 let b0_def = def_array.(0);;
124 let b0_const = const_array.(0);;
125 let b0_name = names_array.(0);;
127 let max_const = mk_small_numeral maximum;;
130 (* Alternative definition of D_i *)
131 let ADD_0_n = prove(`_0 + n = n`,
132 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
133 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
134 let ADD_n_0 = prove(`n + _0 = n`,
135 ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
136 REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
138 let MUL_n_0 = prove(`n * _0 = 0`,
139 REWRITE_TAC[NUMERAL] THEN
140 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
141 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
144 (* D_i(n) = i + D_0(n) *)
146 let bin = mk_comb(const_array.(i), n_var_num) in
147 let bi0 = mk_comb(const_array.(i), zero_const) in
148 let b0n = mk_comb(const_array.(0), n_var_num) in
149 let rhs = mk_binop add_op_num bi0 b0n in
150 prove(mk_eq(bin, rhs), REWRITE_TAC[def_array.(i); def_array.(0)] THEN
151 REWRITE_TAC[MUL_n_0; ADD_CLAUSES] THEN ARITH_TAC);;
153 let def_thm_array = Array.init maximum def_thm;;
155 let B0_0 = prove(mk_eq(mk_comb(b0_const, zero_const), zero_const),
156 REWRITE_TAC[b0_def; MUL_n_0; ADD_CLAUSES; NUMERAL]);;
158 let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num),
159 mk_binop mul_op_num max_const n_var_num),
160 REWRITE_TAC[b0_def; ADD_CLAUSES]);;
162 (******************************)
163 (* mk_numeral and dest_numeral *)
167 let mk_table = Hashtbl.create maximum;;
169 for i = 0 to maximum - 1 do
170 Hashtbl.add mk_table (Int i) const_array.(i)
174 let max_num = Int maximum;;
176 let mk_numeral_hash =
181 let m = mod_num n max_num in
182 let bit = Hashtbl.find mk_table m in
183 mk_comb(bit, mk_num(quo_num n max_num)) in
184 fun n -> if n </ num_0 then failwith "mk_numeral_hash: negative argument"
185 else mk_comb(num_const, mk_num n);;
187 let mk_numeral_array =
192 let m = Num.int_of_num (mod_num n max_num) in
193 let bit = const_array.(m) in
194 mk_comb(bit, mk_num(quo_num n max_num)) in
195 fun n -> if n </ num_0 then failwith "mk_numeral_array: negative argument"
196 else mk_comb(num_const, mk_num n);;
198 let mk_small_numeral_array =
200 if (n = 0) then zero_const
202 let m = n mod maximum in
203 let bit = const_array.(m) in
204 mk_comb(bit, mk_num(n / maximum)) in
205 fun n -> if n < 0 then failwith "mk_small_numeral_array: negative argument"
206 else mk_comb (num_const, mk_num n);;
209 let dest_table_num = Hashtbl.create maximum;;
211 for i = 0 to maximum - 1 do
212 Hashtbl.add dest_table_num names_array.(i) (Int i)
217 let max_num = Int maximum;;
219 let rec raw_dest_hash tm =
220 if tm = zero_const then
223 let l, r = dest_comb tm in
224 let n = max_num */ raw_dest_hash r in
225 let cn = fst(dest_const l) in
226 n +/ (Hashtbl.find dest_table_num cn);;
229 let dest_numeral_hash tm = raw_dest_hash (rand tm);;
232 (******************************)
233 (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *)
235 let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));;
236 let mod_op_num = `MOD`;;
239 let h1 = mk_eq(mk_binop div_op_num m_var_num max_const, q_var_num) in
240 let h2 = mk_eq(mk_binop mod_op_num m_var_num max_const, r_var_num) in
241 let c = mk_eq(m_var_num, mk_binop add_op_num (mk_binop mul_op_num max_const q_var_num) r_var_num) in
242 (UNDISCH_ALL o ARITH_RULE) (mk_imp(h1, mk_imp(h2, c)));;
244 let ZERO_EQ_ZERO = (EQT_ELIM o REWRITE_CONV[NUMERAL]) `0 = _0`;;
245 let SYM_ZERO_EQ_ZERO = SYM ZERO_EQ_ZERO;;
246 let SYM_NUM_THM = SYM NUM_THM;;
248 let NUMERAL_TO_NUM_CONV tm =
249 let rec raw_conv tm =
250 if (rand tm = zero_const) then
253 let th_div = NUM_DIV_CONV (mk_binop div_op_num tm max_const) in
254 let th_mod = NUM_MOD_CONV (mk_binop mod_op_num tm max_const) in
255 let q_tm = rand(concl th_div) in
256 let r_tm = rand(concl th_mod) in
257 let th0 = INST[tm, m_var_num; q_tm, q_var_num; r_tm, r_var_num] DIV_BASE in
258 let th1 = MY_PROVE_HYP th_mod (MY_PROVE_HYP th_div th0) in
259 let r = dest_small_numeral r_tm in
260 let th2 = INST[q_tm, n_var_num] th_num_conv.(r) in
261 let th = TRANS th1 th2 in
262 let ltm, rtm = dest_comb(rand(concl th)) in
263 let r_th = raw_conv rtm in
264 TRANS th (AP_TERM ltm r_th) in
266 if (fst o dest_const o rator) tm <> "NUMERAL" then
267 failwith "NUMERAL_TO_NUM_CONV"
269 let th0 = raw_conv tm in
270 let n_tm = rand(concl th0) in
271 TRANS th0 (INST[n_tm, n_var_num] SYM_NUM_THM);;
273 let replace_numerals = rand o concl o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
274 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;
276 (* NUM_TO_NUMERAL_CONV *)
277 let NUM_TO_NUMERAL_CONV tm =
278 let rec raw_conv tm =
279 if tm = zero_const then
282 let b_tm, n_tm = dest_comb tm in
283 let n_th = raw_conv n_tm in
284 let n_tm' = rand(concl n_th) in
285 let cb = (fst o dest_const) b_tm in
286 let th0 = Hashtbl.find def_table cb in
287 let th1 = AP_TERM b_tm n_th in
288 let th2 = TRANS th1 (INST[n_tm', n_var_num] th0) in
289 let ltm, rtm = dest_comb(rand(concl th2)) in
290 let mul_th = NUM_MULT_CONV (rand ltm) in
291 let add_th0 = AP_THM (AP_TERM add_op_num mul_th) rtm in
292 let add_th = TRANS add_th0 (NUM_ADD_CONV (rand(concl add_th0))) in
294 let ltm, rtm = dest_comb tm in
295 if (fst o dest_const) ltm <> num_name then
296 failwith "NUM_TO_NUMERAL_CONV"
298 let num_th = INST[rtm, n_var_num] NUM_THM in
299 let th0 = raw_conv rtm in
302 (*************************)
306 let SUC_NUM = prove(mk_eq(mk_comb(suc_op_num, mk_comb (num_const, n_var_num)),
307 mk_comb(num_const, mk_comb (suc_op_num, n_var_num))),
308 REWRITE_TAC[num_def; NUMERAL]);;
310 let SUC_0 = prove(mk_eq(`SUC _0`, mk_comb (const_array.(1), zero_const)),
311 REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_SUC; NUMERAL; ARITH_ADD]);;
314 let cflag = (i + 1 >= maximum) in
315 let suc = if (cflag) then 0 else i + 1 in
316 let lhs = mk_comb(suc_op_num, (mk_comb (const_array.(i), n_var_num))) in
317 let rhs = mk_comb(const_array.(suc),
318 if (cflag) then mk_comb(suc_op_num, n_var_num) else n_var_num) in
319 let proof = REWRITE_TAC [def_array.(i); def_array.(suc)] THEN ARITH_TAC in
320 prove(mk_eq(lhs, rhs), proof);;
322 let th_suc_array = Array.init maximum suc_th;;
323 let th_suc_table = Hashtbl.create maximum;;
325 for i = 0 to maximum - 1 do
326 Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i)
329 let SUC_MAX = th_suc_array.(maximum - 1);;
330 let bit_max_name = names_array.(maximum - 1);;
333 let rec raw_suc_conv_hash tm =
335 if (otm = zero_const) then
338 let btm, ntm = dest_comb otm in
339 let cn = fst(dest_const btm) in
340 if (cn = bit_max_name) then
341 let th = INST [ntm, n_var_num] SUC_MAX in
342 let ltm, rtm = dest_comb(rand(concl th)) in
343 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm))
345 INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);;
347 let NUM_SUC_HASH_CONV tm =
348 let ntm = rand (rand tm) in
349 let th = INST [ntm, n_var_num] SUC_NUM in
350 let lhs, rhs = dest_eq(concl th) in
351 if (lhs <> tm) then failwith("NUM_SUC_HASH_CONV")
353 let ltm, rtm = dest_comb rhs in
354 TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));;
357 (**************************************)
359 let EQ_0_NUM = prove(mk_eq(mk_eq(mk_comb(num_const, n_var_num), `_0`), `n = _0`),
360 REWRITE_TAC[num_def; NUMERAL]);;
362 let EQ_B0_0 = prove(mk_eq(mk_eq(mk_comb(b0_const, n_var_num), `_0`), `n = _0`),
363 REWRITE_TAC[b0_def; ADD_CLAUSES; NUMERAL; REWRITE_RULE[NUMERAL] MULT_EQ_0; ARITH_EQ]);;
365 let EQ_0_0 = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH_EQ]);;
367 let eq_0_lemma = REWRITE_RULE[NUMERAL] (ARITH_RULE `a + b = 0 <=> a = 0 /\ b = 0`);;
370 let concl = mk_eq(mk_eq(mk_comb(const_array.(i), n_var_num), zero_const), f_const) in
371 prove(concl, REWRITE_TAC[def_array.(i); eq_0_lemma; NUMERAL; ARITH_EQ]);;
373 let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);;
375 let th_eq0_table = Hashtbl.create maximum;;
377 for i = 0 to maximum - 1 do
378 Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i)
381 let rec raw_eq0_hash_conv rtm =
382 if (rtm = zero_const) then
385 let b_tm, n_tm = dest_comb rtm in
386 let cn = (fst o dest_const) b_tm in
387 if (cn = b0_name) then
388 let th0 = INST[n_tm, n_var_num] EQ_B0_0 in
389 let th1 = raw_eq0_hash_conv n_tm in
392 INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);;
394 let NUM_EQ0_HASH_CONV rtm =
395 let n_tm = rand rtm in
396 let th = INST [n_tm, n_var_num] EQ_0_NUM in
397 TRANS th (raw_eq0_hash_conv n_tm);;
399 (**************************************)
403 let PRE_NUM = prove(mk_eq(mk_comb(pre_op_num, mk_comb (num_const, n_var_num)),
404 mk_comb(num_const, mk_comb (pre_op_num, n_var_num))),
405 REWRITE_TAC[num_def; NUMERAL]);;
407 let PRE_0 = prove(`PRE _0 = _0`,
408 MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
410 let PRE_B1_0 = prove(mk_eq(mk_comb(`PRE`, mk_comb(const_array.(1), `_0`)), `_0`),
411 REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_ADD; NUMERAL; ARITH_PRE; ARITH_EQ]);;
414 let PRE_B0_n0 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> T`,
415 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), `_0`)),
416 REWRITE_TAC[B0_EXPLICIT] THEN
417 DISCH_THEN (fun th -> REWRITE_TAC[th; MUL_n_0]) THEN
418 REWRITE_TAC[NUMERAL; ARITH_PRE]);;
420 let PRE_B0_n1 = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o prove)(mk_imp(`n = 0 <=> F`,
421 mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)),
422 mk_comb(const_array.(maximum - 1), `PRE n`))),
423 REWRITE_TAC[B0_EXPLICIT; def_array.(maximum - 1)] THEN ARITH_TAC);;
425 let PRE_lemma = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o ARITH_RULE) `((n = 0) <=> F) ==> (SUC m = n <=> PRE n = m)`;;
429 let pre_tm = mk_comb(const_array.(pre), n_var_num) in
430 let suc_tm = mk_comb(suc_op_num, pre_tm) in
431 let suc_th = raw_suc_conv_hash suc_tm in
432 let n_tm = rand(concl suc_th) in
433 let n0_th = raw_eq0_hash_conv n_tm in
434 let th0 = INST[pre_tm, m_var_num; n_tm, n_var_num] PRE_lemma in
435 MY_PROVE_HYP n0_th (EQ_MP th0 suc_th);;
438 let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);;
440 let th_pre_table = Hashtbl.create maximum;;
442 for i = 0 to maximum - 1 do
443 Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i)
447 let b1_name = names_array.(1);;
448 let b1_pre_thm = th_pre_array.(1);;
450 let rec raw_pre_hash_conv tm =
452 if (otm = zero_const) then
455 let btm, ntm = dest_comb otm in
456 let cn = fst(dest_const btm) in
457 if (cn = b0_name) then
458 let n_th = raw_eq0_hash_conv ntm in
459 if (rand(concl n_th) = f_const) then
460 let th0 = INST[ntm, n_var_num] PRE_B0_n1 in
461 let th1 = MY_PROVE_HYP n_th th0 in
462 let ltm, rtm = dest_comb(rand(concl th1)) in
463 let th2 = raw_pre_hash_conv rtm in
464 TRANS th1 (AP_TERM ltm th2)
466 let th = INST[ntm, n_var_num] PRE_B0_n0 in
469 if (cn = b1_name) then
470 if (ntm = zero_const) then
473 INST[ntm, n_var_num] b1_pre_thm
475 INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);;
477 let NUM_PRE_HASH_CONV tm =
478 let ntm = rand (rand tm) in
479 let th = INST [ntm, n_var_num] PRE_NUM in
480 let lhs, rhs = dest_eq(concl th) in
481 if (lhs <> tm) then failwith("NUM_PRE_HASH_CONV")
483 let ltm, rtm = dest_comb rhs in
484 TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));;
486 (**************************************)
489 let gt0_table = Hashtbl.create maximum;;
491 let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
493 let gt0_0 = prove(`_0 < _0 <=> F`, REWRITE_TAC[ARITH_LT]);;
494 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`),
495 REWRITE_TAC[b0_def] THEN ARITH_TAC);;
498 let bi = const_array.(i) in
499 let concl = mk_eq (mk_binop lt_op_num zero_num (mk_comb(bi, n_var_num)), t_const) in
500 let proof = REWRITE_TAC[def_array.(i)] THEN ARITH_TAC in
501 (PURE_REWRITE_RULE[NUMERAL] o prove)(concl, proof);;
503 for i = 1 to maximum - 1 do
504 Hashtbl.add gt0_table names_array.(i) (gt0_th i)
507 let rec raw_gt0_hash_conv rtm =
508 if (rtm = zero_const) then
511 let b_tm, n_tm = dest_comb rtm in
512 let cn = (fst o dest_const) b_tm in
513 if (cn = b0_name) then
514 let th0 = INST[n_tm, n_var_num] gt0_b0 in
515 let th1 = raw_gt0_hash_conv n_tm in
518 INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);;
520 let NUM_GT0_HASH_CONV rtm =
521 let n_tm = rand rtm in
522 let th = INST [n_tm, n_var_num] GT0_NUM in
523 TRANS th (raw_gt0_hash_conv n_tm);;
525 (*************************************)
528 let EQ_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m = NUMERAL n <=> m = n`, REWRITE_TAC[NUMERAL]);;
533 (* Generates the theorem |- D_i(m) = D_j(n) <=> F if i <> j and D_i(m) = D_i(n) <=> m = n *)
535 let aux_th = prove(`i < b /\ j < b /\ ~(i = j) ==> ~(b * m + i = b * n + j:num)`,
536 ONCE_REWRITE_TAC[ARITH_RULE `b * m + i = b * n + j <=> m * b + i = n * b + j:num`] THEN
537 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
538 SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN ARITH_TAC; ALL_TAC] THEN
539 REWRITE_TAC[CONTRAPOS_THM] THEN
540 DISCH_TAC THEN FIRST_ASSUM (MP_TAC o AP_TERM `\x. x DIV b`) THEN REWRITE_TAC[] THEN
541 FIRST_ASSUM (MP_TAC o MATCH_MP DIV_MULT_ADD) THEN
542 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
543 SUBGOAL_THEN `i DIV b = 0 /\ j DIV b = 0` (fun th -> REWRITE_TAC[th]) THENL
545 FIRST_ASSUM (ASSUME_TAC o MATCH_MP DIV_EQ_0) THEN ASM_REWRITE_TAC[];
548 REWRITE_TAC[ADD_0] THEN DISCH_TAC THEN
549 UNDISCH_TAC `m * b + i = n * b + j:num` THEN
550 ASM_REWRITE_TAC[] THEN ARITH_TAC) in
552 let bi_m = mk_comb (const_array.(i), m_var_num) in
553 let bj_n = mk_comb (const_array.(j), n_var_num) in
554 let eq_tm = mk_binop eq_op_num bi_m bj_n in
556 prove (mk_eq (eq_tm, mk_binop eq_op_num m_var_num n_var_num), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
558 prove (mk_eq (eq_tm, f_const), REWRITE_TAC[def_array.(i); def_array.(j)] THEN
559 MATCH_MP_TAC aux_th THEN CONV_TAC NUM_REDUCE_CONV);;
562 let gen_next_eq_thm =
563 let suc_eq_th = ARITH_RULE `SUC m = SUC n <=> m = n` in
565 let ltm, n_tm = (dest_comb o lhand o concl) th in
566 let m_tm = rand ltm in
567 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] suc_eq_th in
568 let suc_m = raw_suc_conv_hash (mk_comb (suc_op_num, m_tm)) in
569 let suc_n = raw_suc_conv_hash (mk_comb (suc_op_num, n_tm)) in
570 let th1 = SYM (MK_COMB ((AP_TERM eq_op_num suc_m), suc_n)) in
571 TRANS (TRANS th1 th0) th;;
574 let th_eq_table = Hashtbl.create (maximum * maximum);;
577 for i = 0 to maximum - 1 do
578 let sym = INST[n_var_num, m_var_num; m_var_num, n_var_num] o CONV_RULE (LAND_CONV SYM_CONV) in
579 let th = ref (gen_bi_eq_bj 0 i) in
580 let name_left = names_array.(0) and
581 name_right = names_array.(i) in
582 let _ = Hashtbl.add th_eq_table (name_left ^ name_right) !th in
583 let _ = if i > 0 then
584 Hashtbl.add th_eq_table (name_right ^ name_left) (sym !th)
586 for k = 1 to maximum - i - 1 do
587 let x = k and y = i + k in
588 let name_left = names_array.(x) and
589 name_right = names_array.(y) in
590 let _ = th := gen_next_eq_thm (!th) in
591 let _ = Hashtbl.add th_eq_table (name_left ^ name_right) !th in
593 Hashtbl.add th_eq_table (name_right ^ name_left) (sym !th)
602 let eq_0_sym = (REWRITE_RULE[NUMERAL] o prove)(`0 = n <=> n = 0`, REWRITE_TAC[EQ_SYM_EQ]);;
604 let rec raw_eq_hash_conv tm =
605 let ltm, rtm = dest_comb tm in
606 let ltm = rand ltm in
609 raw_eq0_hash_conv ltm
614 let th0 = raw_eq0_hash_conv rtm in
615 let th1 = INST[rtm, n_var_num] eq_0_sym in
619 let bm_tm, m_tm = dest_comb ltm in
620 let bn_tm, n_tm = dest_comb rtm in
621 let cbm = (fst o dest_const) bm_tm in
622 let cbn = (fst o dest_const) bn_tm in
623 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_eq_table (cbm^cbn)) in
627 let th1 = raw_eq_hash_conv (rand (concl th0)) in
631 let NUM_EQ_HASH_CONV tm =
632 let atm, rtm = dest_comb tm in
633 let ltm = rand atm in
634 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] EQ_NUM in
635 let rtm = rand(concl th) in
636 TRANS th (raw_eq_hash_conv rtm);;
640 (*************************************)
643 let LT_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m < NUMERAL n <=> m < n`, REWRITE_TAC[NUMERAL]);;
644 let LE_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m <= NUMERAL n <=> m <= n`, REWRITE_TAC[NUMERAL]);;
646 let LT_n_0 = prove(`n < _0 <=> F`,
647 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
648 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
651 let LE_0_n = prove(`_0 <= n <=> T`,
652 SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
653 DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
656 let SUC_LT_THM = ARITH_RULE `SUC m < SUC n <=> m < n`;;
657 let SUC_LE_THM = ARITH_RULE `SUC m <= SUC n <=> m <= n`;;
661 (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *)
663 let bin = mk_comb (const_array.(i), n_var_num) in
664 let lt_tm = mk_binop lt_op_num zero_num bin in
666 (PURE_REWRITE_RULE[NUMERAL] o EQT_INTRO o prove)(lt_tm, REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
668 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `0 < n`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
670 let th_lt0_table = Hashtbl.create maximum;;
671 for i = 0 to maximum - 1 do
672 let th = gen_0_lt_bi i in
673 let name = names_array.(i) in
674 Hashtbl.add th_lt0_table name th
678 (* Generates the theorem |- bi(m) < bj(n) <=> m <= n (or m < n) *)
679 let gen_bi_lt_bj i j =
680 let bim = mk_comb (const_array.(i), m_var_num) in
681 let bjn = mk_comb (const_array.(j), n_var_num) in
682 let lt_tm = mk_binop lt_op_num bim bjn in
685 mk_binop lt_op_num m_var_num n_var_num
687 mk_binop le_op_num m_var_num n_var_num in
688 prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
690 (* Given a theorem |- bi(m) < bj(n) <=> P m n, generates the theorem
691 |- SUC(bi(m)) < SUC(bj(n)) <=> P m n *)
692 let gen_next_lt_thm th =
693 let ltm, n_tm = (dest_comb o lhand o concl) th in
694 let m_tm = rand ltm in
695 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LT_THM in
696 let suc_m = raw_suc_conv_hash (mk_comb (suc_op_num, m_tm)) in
697 let suc_n = raw_suc_conv_hash (mk_comb (suc_op_num, n_tm)) in
698 let th1 = SYM (MK_COMB ((AP_TERM lt_op_num suc_m), suc_n)) in
699 TRANS (TRANS th1 th0) th;;
701 let th_lt_table = Hashtbl.create (maximum * maximum);;
703 for i = 0 to maximum - 1 do
704 let th = ref (gen_bi_lt_bj 0 i) in
705 let name_left = names_array.(0) and
706 name_right = names_array.(i) in
707 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
709 for k = 1 to maximum - i - 1 do
710 let x = k and y = i + k in
711 let name_left = names_array.(x) and
712 name_right = names_array.(y) in
713 th := gen_next_lt_thm (!th);
714 Hashtbl.add th_lt_table (name_left ^ name_right) !th
718 for i = 1 to maximum - 1 do
719 let th = ref (gen_bi_lt_bj i 0) in
720 let name_left = names_array.(i) and
721 name_right = names_array.(0) in
722 let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
724 for k = 1 to maximum - i - 1 do
725 let x = i + k and y = k in
726 let name_left = names_array.(x) and
727 name_right = names_array.(y) in
728 th := gen_next_lt_thm (!th);
729 Hashtbl.add th_lt_table (name_left ^ name_right) !th
735 (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *)
737 let bin = mk_comb (const_array.(i), n_var_num) in
738 let lt_tm = mk_binop le_op_num bin zero_num in
740 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, f_const), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
742 (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `n <= 0`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
744 let th_le0_table = Hashtbl.create maximum;;
745 for i = 0 to maximum - 1 do
746 let th = gen_bi_le_0 i in
747 let name = names_array.(i) in
748 Hashtbl.add th_le0_table name th
752 (* Generates the theorem |- bi(m) <= bj(n) <=> m <= n (or m < n) *)
753 let gen_bi_le_bj i j =
754 let bim = mk_comb (const_array.(i), m_var_num) in
755 let bjn = mk_comb (const_array.(j), n_var_num) in
756 let lt_tm = mk_binop le_op_num bim bjn in
759 mk_binop lt_op_num m_var_num n_var_num
761 mk_binop le_op_num m_var_num n_var_num in
762 prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
764 (* Given the theorem |- bi(m) <= bj(n) <=> P m n, generates the theorem
765 |- SUC(bi(m)) <= SUC(bj(n)) <=> P m n *)
766 let gen_next_le_thm th =
767 let ltm, n_tm = (dest_comb o lhand o concl) th in
768 let m_tm = rand ltm in
769 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LE_THM in
770 let suc_m = raw_suc_conv_hash (mk_comb (suc_op_num, m_tm)) in
771 let suc_n = raw_suc_conv_hash (mk_comb (suc_op_num, n_tm)) in
772 let th1 = SYM (MK_COMB ((AP_TERM le_op_num suc_m), suc_n)) in
773 TRANS (TRANS th1 th0) th;;
775 let th_le_table = Hashtbl.create (maximum * maximum);;
777 for i = 0 to maximum - 1 do
778 let th = ref (gen_bi_le_bj 0 i) in
779 let name_left = names_array.(0) and
780 name_right = names_array.(i) in
781 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
783 for k = 1 to maximum - i - 1 do
784 let x = k and y = i + k in
785 let name_left = names_array.(x) and
786 name_right = names_array.(y) in
787 th := gen_next_le_thm (!th);
788 Hashtbl.add th_le_table (name_left ^ name_right) !th
792 for i = 1 to maximum - 1 do
793 let th = ref (gen_bi_le_bj i 0) in
794 let name_left = names_array.(i) and
795 name_right = names_array.(0) in
796 let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
798 for k = 1 to maximum - i - 1 do
799 let x = i + k and y = k in
800 let name_left = names_array.(x) and
801 name_right = names_array.(y) in
802 th := gen_next_le_thm (!th);
803 Hashtbl.add th_le_table (name_left ^ name_right) !th
809 let rec raw_lt_hash_conv tm =
810 let ltm, rtm = dest_comb tm in
811 let ltm = rand ltm in
814 INST[ltm, n_var_num] LT_n_0
818 let bn_tm, n_tm = dest_comb rtm in
819 let cbn = (fst o dest_const) bn_tm in
820 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_lt0_table cbn) in
821 if cbn = b0_name then
822 let th1 = raw_lt_hash_conv (rand (concl th0)) in
828 let bm_tm, m_tm = dest_comb ltm in
829 let bn_tm, n_tm = dest_comb rtm in
830 let cbm = (fst o dest_const) bm_tm in
831 let cbn = (fst o dest_const) bn_tm in
832 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_lt_table (cbm^cbn)) in
833 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
836 raw_lt_hash_conv (rand (concl th0))
838 raw_le_hash_conv (rand (concl th0)) in
841 raw_le_hash_conv tm =
842 let ltm, rtm = dest_comb tm in
843 let ltm = rand ltm in
846 INST[rtm, n_var_num] LE_0_n
850 let bn_tm, n_tm = dest_comb ltm in
851 let cbn = (fst o dest_const) bn_tm in
852 let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_le0_table cbn) in
853 if cbn = b0_name then
854 let th1 = raw_le_hash_conv (rand (concl th0)) in
860 let bm_tm, m_tm = dest_comb ltm in
861 let bn_tm, n_tm = dest_comb rtm in
862 let cbm = (fst o dest_const) bm_tm in
863 let cbn = (fst o dest_const) bn_tm in
864 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_le_table (cbm^cbn)) in
865 let op = (fst o dest_const o rator o rator o rand o concl) th0 in
868 raw_lt_hash_conv (rand (concl th0))
870 raw_le_hash_conv (rand (concl th0)) in
873 let NUM_LT_HASH_CONV tm =
874 let atm, rtm = dest_comb tm in
875 let ltm = rand atm in
876 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LT_NUM in
877 let rtm = rand(concl th) in
878 TRANS th (raw_lt_hash_conv rtm);;
880 let NUM_LE_HASH_CONV tm =
881 let atm, rtm = dest_comb tm in
882 let ltm = rand atm in
883 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LE_NUM in
884 let rtm = rand(concl th) in
885 TRANS th (raw_le_hash_conv rtm);;
888 (**************************************)
893 let ADD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
894 (`NUMERAL m + NUMERAL n = NUMERAL (m + n)`, REWRITE_TAC[NUMERAL]);;
897 let CADD_0_n = prove(`SUC (_0 + n) = SUC n`, REWRITE_TAC[ADD_0_n]);;
898 let CADD_n_0 = prove(`SUC (n + _0) = SUC n`, REWRITE_TAC[ADD_n_0]);;
900 (* B0 (SUC n) = B0 n + maximum *)
901 let B0_SUC = prove(mk_eq(mk_comb(b0_const, mk_comb(suc_op_num, n_var_num)),
902 mk_binop add_op_num max_const (mk_comb(b0_const, n_var_num))),
903 REWRITE_TAC [B0_EXPLICIT] THEN ARITH_TAC);;
905 let B0_ADD = prove(mk_eq(mk_binop add_op_num (mk_comb(b0_const, m_var_num)) (mk_comb(b0_const, n_var_num)),
906 mk_comb(b0_const, mk_binop add_op_num m_var_num n_var_num)),
907 REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
909 let SUC_ADD_RIGHT = prove(`SUC(m + n) = m + SUC n`, ARITH_TAC);;
912 (* Generate all theorems iteratively *)
913 let th_add_right_next th =
914 let lhs, rhs = dest_eq(concl th) in
915 let ltm, rtm = dest_comb rhs in
916 let cn = fst(dest_const ltm) in
917 let suc_th = AP_TERM suc_op_num th in
918 let th_rhs = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
919 let ltm, rarg = dest_comb lhs in
920 let larg = rand ltm in
921 let th1 = INST[larg, m_var_num; rarg, n_var_num] SUC_ADD_RIGHT in
922 let cn = fst(dest_const(rator rarg)) in
923 let th2 = Hashtbl.find th_suc_table cn in
924 let th_lhs = TRANS th1 (AP_TERM ltm th2) in
925 TRANS (TRANS (SYM th_lhs) suc_th) th_rhs;;
927 let th_add_array = Array.make (maximum * maximum) (REFL zero_const);;
929 for i = 0 to maximum - 1 do
934 INST[n_var_num, m_var_num; m_var_num, n_var_num]
935 (ONCE_REWRITE_RULE[ADD_AC] th_add_array.(i)) in
936 let _ = th_add_array.(i * maximum) <- th0 in
938 for j = 1 to maximum - 1 do
939 th_add_array.(i * maximum + j) <- th_add_right_next th_add_array.(i * maximum + j - 1)
943 (* SUC (B_i(m) + B_j(n)) = B_p(...) *)
945 let add_th = th_add_array.(i * maximum + j) in
946 let th0 = AP_TERM suc_op_num add_th in
947 let ltm, rtm = dest_comb(rand(concl th0)) in
948 let ltm, rtm = dest_comb rtm in
949 let cn = fst(dest_const ltm) in
950 let suc_th = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
953 let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);;
955 for i = 0 to maximum - 1 do
956 for j = 0 to maximum - 1 do
957 th_cadd_array.(i * maximum + j) <- th_cadd i j
961 let th_add_table = Hashtbl.create (maximum * maximum);;
963 for i = 0 to maximum - 1 do
964 for j = 0 to maximum - 1 do
965 let name = names_array.(i) ^ names_array.(j) in
966 let th = th_add_array.(i * maximum + j) in
967 let cflag = (i + j >= maximum) in
968 Hashtbl.add th_add_table name (th, cflag)
972 let th_cadd_table = Hashtbl.create (maximum * maximum);;
974 for i = 0 to maximum - 1 do
975 for j = 0 to maximum - 1 do
976 let name = names_array.(i) ^ names_array.(j) in
977 let th = th_cadd_array.(i * maximum + j) in
978 let cflag = (i + j + 1 >= maximum) in
979 Hashtbl.add th_cadd_table name (th, cflag)
984 let rec raw_add_conv_hash tm =
985 let atm,rtm = dest_comb tm in
986 let ltm = rand atm in
987 if ltm = zero_const then
988 INST [rtm,n_var_num] ADD_0_n
989 else if rtm = zero_const then
990 INST [ltm,n_var_num] ADD_n_0
992 let lbit,larg = dest_comb ltm
993 and rbit,rarg = dest_comb rtm in
994 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
995 let th0, cflag = Hashtbl.find th_add_table name in
996 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
997 let ltm, rtm = dest_comb(rand(concl th)) in
999 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1001 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm))
1002 and raw_adc_conv_hash tm =
1003 let atm,rtm = dest_comb (rand tm) in
1004 let ltm = rand atm in
1005 if ltm = zero_const then
1006 let th = INST [rtm,n_var_num] CADD_0_n in
1007 TRANS th (raw_suc_conv_hash (rand(concl th)))
1008 else if rtm = zero_const then
1009 let th = INST [ltm,n_var_num] CADD_n_0 in
1010 TRANS th (raw_suc_conv_hash (rand(concl th)))
1012 let lbit,larg = dest_comb ltm
1013 and rbit,rarg = dest_comb rtm in
1014 let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1015 let th0, cflag = Hashtbl.find th_cadd_table name in
1016 let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1017 let ltm, rtm = dest_comb(rand(concl th)) in
1019 TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1021 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1023 let NUM_ADD_HASH_CONV tm =
1024 let atm, rtm = dest_comb tm in
1025 let ltm = rand atm in
1026 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] ADD_NUM in
1027 let ltm, rtm = dest_comb(rand(concl th)) in
1028 TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1030 (********************************)
1033 let SUB_NUM = prove(mk_eq(mk_binop sub_op_num (mk_comb (num_const, m_var_num)) (mk_comb (num_const, n_var_num)),
1034 mk_comb(num_const, mk_binop sub_op_num m_var_num n_var_num)),
1035 REWRITE_TAC[num_def; NUMERAL]);;
1037 let SUB_lemma1 = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> m - n = t:num`;;
1038 let SUB_lemma2 = (UNDISCH_ALL o REWRITE_RULE[NUMERAL] o ARITH_RULE) `m + t = n ==> m - n = 0`;;
1039 let LE_lemma = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> n <= m:num`;;
1041 let raw_sub_hash_conv tm =
1042 let ltm, n_tm = dest_comb tm in
1043 let m_tm = rand ltm in
1044 let m = raw_dest_hash m_tm in
1045 let n = raw_dest_hash n_tm in
1048 let t_tm = rand (mk_numeral_array t) in
1049 let th0 = INST[n_tm, n_var_num; t_tm, t_var_num; m_tm, m_var_num] SUB_lemma1 in
1050 let th_add = raw_add_conv_hash (mk_binop add_op_num n_tm t_tm) in
1051 MY_PROVE_HYP th_add th0
1053 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1054 let th0 = INST[m_tm, m_var_num; t_tm, t_var_num; n_tm, n_var_num] SUB_lemma2 in
1055 let th_add = raw_add_conv_hash (mk_binop add_op_num m_tm t_tm) in
1056 MY_PROVE_HYP th_add th0;;
1058 (* Returns either (tm1 - tm2, tm2 <= tm1) or (tm2 - tm1, tm1 <= tm2) *)
1059 let raw_sub_and_le_hash_conv tm1 tm2 =
1060 let m = raw_dest_hash tm1 in
1061 let n = raw_dest_hash tm2 in
1064 let t_tm = rand (mk_numeral_array t) in
1065 let inst = INST[tm2, n_var_num; t_tm, t_var_num; tm1, m_var_num] in
1066 let th_sub = inst SUB_lemma1 in
1067 let th_le = inst LE_lemma in
1068 let th_add = raw_add_conv_hash (mk_binop add_op_num tm2 t_tm) in
1069 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le)
1071 let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1072 let inst = INST[tm2, m_var_num; t_tm, t_var_num; tm1, n_var_num] in
1073 let th_sub = inst SUB_lemma1 in
1074 let th_le = inst LE_lemma in
1075 let th_add = raw_add_conv_hash (mk_binop add_op_num tm1 t_tm) in
1076 (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le);;
1078 let NUM_SUB_HASH_CONV tm =
1079 let atm, rtm = dest_comb tm in
1080 let ltm = rand atm in
1081 let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] SUB_NUM in
1082 let ltm, rtm = dest_comb(rand(concl th)) in
1083 TRANS th (AP_TERM ltm (raw_sub_hash_conv rtm));;
1086 (********************************)
1087 (* Multiplication *)
1089 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)),
1090 mk_comb(num_const, mk_binop mul_op_num m_var_num n_var_num)),
1091 REWRITE_TAC[num_def; NUMERAL]);;
1093 let MUL_0_n = prove(`_0 * n = _0`, ONCE_REWRITE_TAC[GSYM NUM_THM] THEN
1094 ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN REWRITE_TAC[num_def] THEN
1095 REWRITE_TAC[MULT_CLAUSES]);;
1097 let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;;
1099 let MUL_1_n, MUL_n_1 =
1100 let one_const = mk_comb (const_array.(1), zero_num) in
1101 let cond = mk_eq(mk_binop mul_op_num one_const n_var_num, n_var_num) in
1102 let th = (REWRITE_RULE[NUMERAL] o prove)(cond, REWRITE_TAC[def_array.(1)] THEN ARITH_TAC) in
1103 th, ONCE_REWRITE_RULE[MULT_AC] th;;
1105 let MUL_B0_t = prove(mk_eq(mk_binop mul_op_num (mk_comb(b0_const, n_var_num)) t_var_num,
1106 mk_comb(b0_const, mk_binop mul_op_num n_var_num t_var_num)),
1107 REWRITE_TAC[def_array.(0)] THEN ARITH_TAC);;
1109 let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
1111 let MUL_SUC_RIGHT = prove(`m * SUC(n) = m * n + m`, ARITH_TAC);;
1113 (* Multiplication table *)
1114 let mul_th_next_right th =
1115 let ltm, rtm = dest_comb(rand(rator(concl th))) in
1116 let mtm = rand ltm in
1117 let th0 = INST[mtm, m_var_num; rtm, n_var_num] MUL_SUC_RIGHT in
1118 let th1 = AP_THM (AP_TERM add_op_num th) mtm in
1119 let sum_th = raw_add_conv_hash (rand(concl th1)) in
1120 let th2 = TRANS (TRANS th0 th1) sum_th in
1121 let cn = fst(dest_const (rator rtm)) in
1122 let th_suc = INST[zero_const, n_var_num] (Hashtbl.find th_suc_table cn) in
1123 let th3 = AP_TERM (mk_comb (mul_op_num, mtm)) th_suc in
1124 TRANS (SYM th3) th2;;
1126 let mul_array = Array.make (maximum * maximum) (REFL zero_const);;
1127 for i = 1 to maximum - 1 do
1128 let th1 = INST[mk_comb(const_array.(i), zero_const), n_var_num] MUL_n_1 in
1129 let _ = mul_array.(i * maximum + 1) <- th1 in
1131 for j = 2 to maximum - 1 do
1132 mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1)
1136 let mul_table = Hashtbl.create (maximum * maximum);;
1137 for i = 1 to maximum - 1 do
1138 for j = 1 to maximum - 1 do
1139 Hashtbl.add mul_table (names_array.(i) ^ names_array.(j)) mul_array.(i * maximum + j)
1143 (* General multiplication theorem *)
1145 let mul (a,b) = mk_binop mul_op_num a b and
1146 add (a,b) = mk_binop add_op_num a b in
1147 let lhs = mul(add(t_var_num, mk_comb(b0_const, m_var_num)),
1148 add(r_var_num, mk_comb(b0_const, n_var_num))) in
1149 let rhs = add(mul(t_var_num, r_var_num),
1150 mk_comb(b0_const, add(mk_comb(b0_const, mul(m_var_num, n_var_num)),
1151 add(mul(m_var_num, r_var_num),
1152 mul(n_var_num, t_var_num))))) in
1153 prove(mk_eq(lhs, rhs),
1154 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1155 REWRITE_TAC[MUL_B0_t; MUL_t_B0] THEN
1156 ONCE_REWRITE_TAC[GSYM ADD_ASSOC] THEN
1157 REWRITE_TAC[th_add_array.(0)] THEN
1158 REWRITE_TAC[ADD_AC; MULT_AC]);;
1160 let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;;
1163 let ltm, rtm = dest_comb tm in
1166 (* B_i(m) * B_j(n) = B_p(B_q(m * n) + m * B_j(0) + n * B_i(0))
1167 where B_p(B_q(0)) = i * j *)
1168 let gen_mul_thm i j =
1169 let bi0 = mk_comb(const_array.(i), zero_const) and
1170 bj0 = mk_comb(const_array.(j), zero_const) in
1171 let def_i = INST[m_var_num, n_var_num] def_thm_array.(i) in
1172 let def_j = def_thm_array.(j) in
1173 let th0 = MK_COMB(AP_TERM mul_op_num def_i, def_j) in
1174 let th1 = TRANS th0 (INST[bi0, t_var_num; bj0, r_var_num] prod_lemma) in
1175 let mul_th = mul_array.(i * maximum + j) in
1176 let larg, rarg = dest_op (rand (concl th1)) in
1177 let th2 = TRANS th1 (AP_THM (AP_TERM add_op_num mul_th) rarg) in
1178 let larg = rand(concl mul_th) in
1179 let b_low, b_high = dest_comb larg in
1180 let rtm = rand(rarg) in
1181 let th_add = INST[b_high, m_var_num; rtm, n_var_num]
1182 (fst(Hashtbl.find th_add_table (fst(dest_const b_low)^b0_name))) in
1183 if i * j < maximum then
1184 let ltm, rtm = dest_op(rand(rand(concl th_add))) in
1185 let add_0 = AP_TERM b_low (INST[rtm, n_var_num] ADD_0_n) in
1186 TRANS th2 (TRANS th_add add_0)
1188 let larg, rtm = dest_op (rand(rand(concl th_add))) in
1189 let rarg, rtm = dest_op rtm in
1190 let th_assoc = INST[larg, m_var_num; rarg, n_var_num; rtm, p_var_num] ADD_ASSOC' in
1191 let mn = rand(rarg) in
1192 let b_high = rator b_high in
1193 let th_add2' = INST[zero_const, m_var_num; mn, n_var_num]
1194 (fst(Hashtbl.find th_add_table (fst(dest_const b_high)^b0_name))) in
1195 let add_0 = AP_TERM b_high (INST[mn, n_var_num] ADD_0_n) in
1196 let th_add2 = TRANS th_add2' add_0 in
1197 let th3 = TRANS th_assoc (AP_THM (AP_TERM add_op_num th_add2) rtm) in
1198 let th4 = TRANS th_add (AP_TERM b_low th3) in
1201 let gen_mul_table = Hashtbl.create (maximum * maximum);;
1203 for i = 1 to maximum - 1 do
1204 for j = 1 to maximum - 1 do
1205 let name = names_array.(i) ^ names_array.(j) in
1206 Hashtbl.add gen_mul_table name (gen_mul_thm i j)
1210 (* B_i(m) * B_j(0) = B_p(B_q(0) + m * B_j(0))
1211 where i * j = B_p(B_q(0)) *)
1212 let mul1_right_th i j =
1213 let th0 = INST[zero_const, n_var_num]
1214 (Hashtbl.find gen_mul_table (names_array.(i)^names_array.(j))) in
1215 let b_low, rtm = dest_comb(rand(concl th0)) in
1216 let tm1, tm23 = dest_op rtm in
1217 let tm2p, tm3 = dest_comb tm23 in
1218 let tm3_th = INST[rand tm3, n_var_num] MUL_0_n in
1219 let tm2_th = INST[rand(tm2p), n_var_num] ADD_n_0 in
1220 let tm23_th = TRANS (AP_TERM tm2p tm3_th) tm2_th in
1221 let ltm, rtm = dest_comb tm1 in
1222 if (i * j < maximum) then
1223 let tm1_th = TRANS (AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0)) B0_0 in
1224 let tm123_th' = TRANS (INST[tm23, n_var_num] ADD_0_n) tm23_th in
1225 let tm123_th = TRANS (AP_THM (AP_TERM add_op_num tm1_th) tm23) tm123_th' in
1226 TRANS th0 (AP_TERM b_low tm123_th)
1228 let tm1_th = AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0) in
1229 let tm123_th = MK_COMB(AP_TERM add_op_num tm1_th, tm23_th) in
1230 TRANS th0 (AP_TERM b_low tm123_th);;
1232 (* B_j(0) * B_i(m) = B_p(B_q(0) + B_j(0) * B_i(m) *)
1233 let MULT_AC' = CONJUNCT1 MULT_AC;;
1235 let mul1_left_th th =
1236 let lhs, rhs = dest_eq(concl th) in
1237 let ltm, rtm = dest_op lhs in
1238 let th_lhs = INST[ltm, n_var_num; rtm, m_var_num] MULT_AC' in
1239 let btm, rtm = dest_comb rhs in
1240 let larg, rarg = dest_op rtm in
1241 if (is_comb larg) then
1242 let ltm, rtm = dest_op rarg in
1243 let th_rhs' = INST[ltm, m_var_num; rtm, n_var_num] MULT_AC' in
1244 let th_rhs = AP_TERM (mk_comb(add_op_num, larg)) th_rhs' in
1245 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs))
1247 let th_rhs = INST[larg, m_var_num; rarg, n_var_num] MULT_AC' in
1248 TRANS th_lhs (TRANS th (AP_TERM btm th_rhs));;
1250 let mul1_right_th_table = Hashtbl.create (maximum * maximum);;
1251 let mul1_left_th_table = Hashtbl.create (maximum * maximum);;
1253 for i = 1 to maximum - 1 do
1254 for j = 1 to maximum - 1 do
1255 let name_right = names_array.(i) ^ names_array.(j) in
1256 let name_left = names_array.(j) ^ names_array.(i) in
1257 let th = mul1_right_th i j in
1258 let add_flag = (i * j >= maximum) in
1259 let _ = Hashtbl.add mul1_right_th_table name_right (add_flag, th) in
1260 Hashtbl.add mul1_left_th_table name_left (add_flag, mul1_left_th th)
1265 (******************************************************)
1268 (* Multiplies arg and (tm = tmname(_0)) *)
1269 let rec raw_mul1_right_hash arg tm tmname =
1270 if arg = zero_const then
1271 INST [tm, n_var_num] MUL_0_n
1273 let btm, mtm = dest_comb arg in
1274 let cn = fst(dest_const btm) in
1275 if (cn = b0_name) then
1276 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_B0_t in
1277 TRANS th (AP_TERM b0_const (raw_mul1_right_hash mtm tm tmname))
1279 let name = cn ^ tmname in
1280 if (mtm = zero_const) then
1281 Hashtbl.find mul_table name
1283 let add_flag, th' = Hashtbl.find mul1_right_th_table name in
1284 let th = INST[mtm, m_var_num] th' in
1286 let ltm, rtm = dest_comb(rand(concl th)) in
1287 let lplus, rarg = dest_comb rtm in
1288 let th2 = AP_TERM lplus (raw_mul1_right_hash mtm tm tmname) in
1289 let th_add = raw_add_conv_hash (rand(concl th2)) in
1290 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1292 let ltm = rator(rand(concl th)) in
1293 let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in
1296 (* Multiplies (tm = tmname(_0)) and arg *)
1297 let rec raw_mul1_left_hash tm tmname arg =
1298 if arg = zero_const then
1299 INST [tm, n_var_num] MUL_n_0
1301 let btm, mtm = dest_comb arg in
1302 let cn = fst(dest_const btm) in
1303 if (cn = b0_name) then
1304 let th = INST[mtm, n_var_num; tm, t_var_num] MUL_t_B0 in
1305 TRANS th (AP_TERM b0_const (raw_mul1_left_hash tm tmname mtm))
1307 let name = tmname ^ cn in
1308 if (mtm = zero_const) then
1309 Hashtbl.find mul_table name
1311 let add_flag, th' = Hashtbl.find mul1_left_th_table name in
1312 let th = INST[mtm, m_var_num] th' in
1314 let ltm, rtm = dest_comb(rand(concl th)) in
1315 let lplus, rarg = dest_comb rtm in
1316 let th2 = AP_TERM lplus (raw_mul1_left_hash tm tmname mtm) in
1317 let th_add = raw_add_conv_hash (rand(concl th2)) in
1318 TRANS th (AP_TERM ltm (TRANS th2 th_add))
1320 let ltm = rator(rand(concl th)) in
1321 let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in
1324 (* Computes B_i(m) * B_j(n) *)
1325 let rec raw_mul_conv_hash tm =
1326 let larg, rarg = dest_comb tm in
1327 let larg = rand larg in
1328 if larg = zero_const then
1329 INST [rarg, n_var_num] MUL_0_n
1330 else if rarg = zero_const then
1331 INST [larg, n_var_num] MUL_n_0
1334 let lbtm, mtm = dest_comb larg in
1335 let lcn = fst(dest_const lbtm) in
1336 if (lcn = b0_name) then
1337 let th = INST[rarg, t_var_num; mtm, n_var_num] MUL_B0_t in
1338 let ltm, rtm = dest_comb(rand(concl th)) in
1339 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1341 let rbtm, ntm = dest_comb rarg in
1342 let rcn = fst(dest_const rbtm) in
1343 if (rcn = b0_name) then
1344 let th = INST[larg, t_var_num; ntm, n_var_num] MUL_t_B0 in
1345 let ltm, rtm = dest_comb(rand(concl th)) in
1346 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1349 if (ntm = zero_const) then
1350 if (mtm = zero_const) then
1351 Hashtbl.find mul_table (lcn ^ rcn)
1353 raw_mul1_right_hash larg (mk_comb(rbtm, zero_const)) rcn
1354 else if (mtm = zero_const) then
1355 raw_mul1_left_hash (mk_comb(lbtm, zero_const)) lcn rarg
1358 let th0 = INST[mtm, m_var_num; ntm, n_var_num]
1359 (Hashtbl.find gen_mul_table (lcn ^ rcn)) in
1360 let b_low, expr = dest_comb(rand(concl th0)) in
1361 let ltm, rsum = dest_comb expr in
1362 let b_high, mul0 = dest_comb (rand ltm) in
1363 let th_mul0 = raw_mul_conv_hash mul0 in
1364 let th_mul1 = raw_mul1_right_hash mtm (mk_comb(rbtm, zero_const)) rcn in
1365 let th_mul2 = raw_mul1_right_hash ntm (mk_comb(lbtm, zero_const)) lcn in
1366 let th_larg = AP_TERM add_op_num (AP_TERM b_high th_mul0) in
1367 let th_rarg = MK_COMB(AP_TERM add_op_num th_mul1, th_mul2) in
1369 let add_rarg = TRANS th_rarg (raw_add_conv_hash (rand(concl th_rarg))) in
1370 let add_th = MK_COMB (th_larg, add_rarg) in
1371 let add = TRANS add_th (raw_add_conv_hash (rand(concl add_th))) in
1373 TRANS th0 (AP_TERM b_low add);;
1375 (* The main multiplication conversion *)
1376 let NUM_MULT_HASH_CONV tm =
1377 let ltm, rtm = dest_comb tm in
1378 let larg, rarg = rand (rand ltm), rand rtm in
1379 let th0 = INST[larg, m_var_num; rarg, n_var_num] MUL_NUM in
1380 if (rand(rator(concl th0)) <> tm) then
1381 failwith "NUM_MULT_HASH_CONV"
1383 let rtm = rand(rand(concl th0)) in
1384 let th = raw_mul_conv_hash rtm in
1385 TRANS th0 (AP_TERM num_const th);;
1388 (************************************)
1391 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)),
1392 mk_comb(num_const, mk_binop div_op_num m_var_num n_var_num)),
1393 REWRITE_TAC[num_def; NUMERAL]);;
1395 let DIV_UNIQ' = (UNDISCH_ALL o
1396 PURE_ONCE_REWRITE_RULE[ARITH_RULE `a < b <=> (a < b:num <=> T)`] o
1397 ONCE_REWRITE_RULE[ARITH_RULE `m = q * n + r <=> q * n + r = m:num`] o
1398 REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL) DIV_UNIQ;;
1400 (* Computes m DIV n *)
1401 let raw_div_hash_conv tm =
1402 let ltm, n_tm = dest_comb tm in
1403 let m_tm = rand ltm in
1404 let m = raw_dest_hash m_tm in
1405 let n = raw_dest_hash n_tm in
1406 let q = Num.quo_num m n and
1407 r = Num.mod_num m n in
1408 let q_tm = rand (mk_numeral_array q) and
1409 r_tm = rand (mk_numeral_array r) in
1411 let qn_th = raw_mul_conv_hash (mk_binop mul_op_num q_tm n_tm) in
1412 let qn_tm = rand (concl qn_th) in
1413 let qnr_th = raw_add_conv_hash (mk_binop add_op_num qn_tm r_tm) in
1414 let th1 = TRANS (AP_THM (AP_TERM add_op_num qn_th) r_tm) qnr_th in
1415 let th2 = raw_lt_hash_conv (mk_binop lt_op_num r_tm n_tm) in
1416 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
1417 MY_PROVE_HYP th1 (MY_PROVE_HYP th2 th0);;
1419 (* The main division conversion *)
1420 let NUM_DIV_HASH_CONV tm =
1421 let ltm, rtm = dest_comb tm in
1422 let larg, rarg = rand (rand ltm), rand rtm in
1423 let th0 = INST[larg, m_var_num; rarg, n_var_num] DIV_NUM in
1424 if (rand(rator(concl th0)) <> tm) then
1425 failwith "NUM_DIV_HASH_CONV"
1427 let rtm = rand(rand(concl th0)) in
1428 let th = raw_div_hash_conv rtm in
1429 TRANS th0 (AP_TERM num_const th);;
1432 (*********************************************)
1433 (* EVEN_CONV, ODD_CONV *)
1435 let even_const = `EVEN` and
1436 odd_const = `ODD` and
1439 let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1440 (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);;
1442 let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1443 (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
1445 let EVEN_ZERO = prove(`EVEN _0 <=> T`, REWRITE_TAC[ARITH_EVEN]);;
1446 let ODD_ZERO = prove(`ODD _0 <=> F`, REWRITE_TAC[ARITH_ODD]);;
1449 let EVEN_B0 = prove(mk_eq(mk_comb(`EVEN`, mk_comb(b0_const, `n:num`)), `T`),
1450 REWRITE_TAC[B0_EXPLICIT; EVEN_MULT] THEN
1451 DISJ1_TAC THEN CONV_TAC NUM_EVEN_CONV);;
1454 let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
1455 REWRITE_TAC[NOT_ODD; EVEN_B0]);;
1457 let EVEN_SUC_T = prove(`(EVEN (SUC n) <=> T) <=> (EVEN n <=> F)`, REWRITE_TAC[EVEN]);;
1458 let EVEN_SUC_F = prove(`(EVEN (SUC n) <=> F) <=> (EVEN n <=> T)`, REWRITE_TAC[EVEN]);;
1460 let ODD_SUC_T = prove(`(ODD (SUC n) <=> T) <=> (ODD n <=> F)`, REWRITE_TAC[ODD]);;
1461 let ODD_SUC_F = prove(`(ODD (SUC n) <=> F) <=> (ODD n <=> T)`, REWRITE_TAC[ODD]);;
1463 let next_even_th th =
1464 let ltm, rtm = dest_comb(concl th) in
1465 let b_tm = rand(rand ltm) in
1466 let suc_b = raw_suc_conv_hash (mk_comb (suc_op_num, b_tm)) in
1467 let flag = (fst o dest_const) rtm = "T" in
1468 let th0 = SYM (AP_TERM even_const suc_b) in
1469 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1470 let th2 = INST[b_tm, n_var_num] (if flag then EVEN_SUC_F else EVEN_SUC_T) in
1471 EQ_MP (SYM (TRANS th1 th2)) th;;
1473 let next_odd_th th =
1474 let ltm, rtm = dest_comb(concl th) in
1475 let b_tm = rand(rand ltm) in
1476 let suc_b = raw_suc_conv_hash (mk_comb (suc_op_num, b_tm)) in
1477 let flag = (fst o dest_const) rtm = "T" in
1478 let th0 = SYM (AP_TERM odd_const suc_b) in
1479 let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1480 let th2 = INST[b_tm, n_var_num] (if flag then ODD_SUC_F else ODD_SUC_T) in
1481 EQ_MP (SYM (TRANS th1 th2)) th;;
1483 let even_thm_table = Hashtbl.create maximum;;
1485 Hashtbl.add even_thm_table names_array.(0) EVEN_B0;;
1487 for i = 1 to maximum - 1 do
1488 let th0 = next_even_th (Hashtbl.find even_thm_table names_array.(i - 1)) in
1489 Hashtbl.add even_thm_table names_array.(i) th0
1492 let odd_thm_table = Hashtbl.create maximum;;
1493 Hashtbl.add odd_thm_table names_array.(0) ODD_B0;;
1495 for i = 1 to maximum - 1 do
1496 let th0 = next_odd_th (Hashtbl.find odd_thm_table names_array.(i - 1)) in
1497 Hashtbl.add odd_thm_table names_array.(i) th0
1500 let raw_even_hash_conv tm =
1501 let ltm, rtm = dest_comb tm in
1502 if ((fst o dest_const) ltm <> "EVEN") then
1503 failwith "raw_even_hash_conv: no EVEN"
1505 if (is_const rtm) then
1508 let b_tm, n_tm = dest_comb rtm in
1509 let th0 = Hashtbl.find even_thm_table ((fst o dest_const) b_tm) in
1510 INST[n_tm, n_var_num] th0;;
1512 let raw_odd_hash_conv tm =
1513 let ltm, rtm = dest_comb tm in
1514 if ((fst o dest_const) ltm <> "ODD") then
1515 failwith "raw_odd_hash_conv: no ODD"
1517 if (is_const rtm) then
1520 let b_tm, n_tm = dest_comb rtm in
1521 let th0 = Hashtbl.find odd_thm_table ((fst o dest_const) b_tm) in
1522 INST[n_tm, n_var_num] th0;;
1524 let NUM_EVEN_HASH_CONV tm =
1525 let ltm, rtm = dest_comb tm in
1526 let th0 = INST[rand rtm, n_var_num] EVEN_NUM in
1527 let ltm, rtm = dest_comb(concl th0) in
1528 if (rand ltm <> tm) then
1529 failwith "NUM_EVEN_HASH_CONV"
1531 let th1 = raw_even_hash_conv rtm in
1534 let NUM_ODD_HASH_CONV tm =
1535 let ltm, rtm = dest_comb tm in
1536 let th0 = INST[rand rtm, n_var_num] ODD_NUM in
1537 let ltm, rtm = dest_comb(concl th0) in
1538 if (rand ltm <> tm) then
1539 failwith "NUM_ODD_HASH_CONV"
1541 let th1 = raw_odd_hash_conv rtm in