formal_ineqs/arith/arith_num.hl

   1 (* =========================================================== *)
   2 (* Formal natural arithmetic with an arbitrary base            *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 module type Arith_hash_sig =
   8   sig
   9         val arith_base : int
  10     val num_def : thm
  11     val NUM_THM : thm
  12     val num_const : term
  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
  23         (* SUC *)
  24     val raw_suc_conv_hash : term -> thm
  25     val NUM_SUC_HASH_CONV : term -> thm
  26         (* eq0 *)
  27     val raw_eq0_hash_conv : term -> thm
  28     val NUM_EQ0_HASH_CONV : term -> thm
  29         (* PRE *)
  30     val raw_pre_hash_conv : term -> thm
  31     val NUM_PRE_HASH_CONV : term -> thm
  32         (* gt0 *)
  33     val raw_gt0_hash_conv : term -> thm
  34     val NUM_GT0_HASH_CONV : term -> thm
  35         (* eq *)
  36         val raw_eq_hash_conv : term -> thm
  37         val NUM_EQ_HASH_CONV : term -> thm
  38         (* lt, le *)
  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
  43         (* add *)
  44     val raw_add_conv_hash : term -> thm
  45     val NUM_ADD_HASH_CONV : term -> thm
  46         (* sub *)
  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
  50         (* mul *)
  51     val raw_mul_conv_hash : term -> thm
  52     val NUM_MULT_HASH_CONV : term -> thm
  53         (* DIV *)
  54     val raw_div_hash_conv : term -> thm
  55     val NUM_DIV_HASH_CONV : term -> thm
  56         (* EVEN, ODD *)
  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
  61 end;;
  62
  63 (* Dependencies *)
  64 needs "misc/misc.hl";;
  65 needs "misc/vars.hl";;
  66 needs "arith_options.hl";;
  67
  68 module Arith_hash : Arith_hash_sig = struct
  69
  70 open Arith_misc;;
  71 open Misc_vars;;
  72
  73 let arith_base = !Arith_options.base;;
  74 let maximum = arith_base;;
  75
  76 (******************)
  77
  78 (* Generate definitions and constants *)
  79
  80 let fnum_type = `:num->num` and
  81     numeral_const = `NUMERAL` and
  82     bit0_const = `BIT0` and
  83     bit1_const = `BIT1`;;
  84
  85 (* Names of constants which define "digits" *)
  86 let names_array = Array.init maximum (fun i -> "D"^(string_of_int i));;
  87
  88 (* Definitions *)
  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;;
  93
  94 (* |- NUM n = n *)
  95 let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
  96                     REWRITE_TAC[num_def; NUMERAL]);;
  97
  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));;
 105
 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;;
 113
 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)
 117 done;;
 118
 119
 120 (* Constants *)
 121 let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));;
 122
 123 let b0_def = def_array.(0);;
 124 let b0_const = const_array.(0);;
 125 let b0_name = names_array.(0);;
 126
 127 let max_const = mk_small_numeral maximum;;
 128
 129
 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]);;
 137
 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
 142                       ARITH_TAC);;
 143
 144 (* D_i(n) = i + D_0(n) *)
 145 let def_thm i =
 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);;
 152
 153 let def_thm_array = Array.init maximum def_thm;;
 154
 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]);;
 157
 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]);;
 161
 162 (******************************)
 163 (* mk_numeral and dest_numeral *)
 164
 165 (* mk_table *)
 166
 167 let mk_table = Hashtbl.create maximum;;
 168
 169 for i = 0 to maximum - 1 do
 170   Hashtbl.add mk_table (Int i) const_array.(i)
 171 done;;
 172
 173 (* mk_numeral *)
 174 let max_num = Int maximum;;
 175
 176 let mk_numeral_hash =
 177   let rec mk_num n =
 178     if (n =/ num_0) then
 179       zero_const
 180     else
 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);;
 186
 187 let mk_numeral_array =
 188   let rec mk_num n =
 189     if (n =/ num_0) then
 190       zero_const
 191     else
 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);;
 197
 198 let mk_small_numeral_array =
 199   let rec mk_num n =
 200     if (n = 0) then zero_const
 201     else
 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);;
 207
 208 (* dest_table *)
 209 let dest_table_num = Hashtbl.create maximum;;
 210
 211 for i = 0 to maximum - 1 do
 212   Hashtbl.add dest_table_num names_array.(i) (Int i)
 213 done;;
 214
 215
 216 (* dest_numeral *)
 217 let max_num = Int maximum;;
 218
 219 let rec raw_dest_hash tm =
 220   if tm = zero_const then
 221     num_0
 222   else
 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);;
 227
 228
 229 let dest_numeral_hash tm = raw_dest_hash (rand tm);;
 230
 231
 232 (******************************)
 233 (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *)
 234
 235 let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));;
 236 let mod_op_num = `MOD`;;
 237
 238 let DIV_BASE =
 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)));;
 243
 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;;
 247
 248 let NUMERAL_TO_NUM_CONV tm =
 249   let rec raw_conv tm =
 250     if (rand tm = zero_const) then
 251       ZERO_EQ_ZERO
 252     else
 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
 265
 266     if (fst o dest_const o rator) tm <> "NUMERAL" then
 267       failwith "NUMERAL_TO_NUM_CONV"
 268     else
 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);;
 272
 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);;
 275
 276 (* NUM_TO_NUMERAL_CONV *)
 277 let NUM_TO_NUMERAL_CONV tm =
 278   let rec raw_conv tm =
 279     if tm = zero_const then
 280       SYM_ZERO_EQ_ZERO
 281     else
 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
 293         TRANS th2 add_th 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"
 297     else
 298       let num_th = INST[rtm, n_var_num] NUM_THM in
 299       let th0 = raw_conv rtm in
 300         TRANS num_th th0;;
 301
 302 (*************************)
 303 (* SUC_CONV *)
 304
 305 (* Theorems *)
 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]);;
 309
 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]);;
 312
 313 let suc_th i =
 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);;
 321
 322 let th_suc_array = Array.init maximum suc_th;;
 323 let th_suc_table = Hashtbl.create maximum;;
 324
 325 for i = 0 to maximum - 1 do
 326   Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i)
 327 done;;
 328
 329 let SUC_MAX = th_suc_array.(maximum - 1);;
 330 let bit_max_name = names_array.(maximum - 1);;
 331
 332 (* Conversion *)
 333 let rec raw_suc_conv_hash tm =
 334   let otm = rand tm in
 335     if (otm = zero_const) then
 336       SUC_0
 337     else
 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))
 344         else
 345           INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);;
 346
 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")
 352     else
 353       let ltm, rtm = dest_comb rhs in
 354         TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));;
 355
 356
 357 (**************************************)
 358 (* EQ_0_CONV *)
 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]);;
 361
 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]);;
 364
 365 let EQ_0_0 = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH_EQ]);;
 366
 367 let eq_0_lemma = REWRITE_RULE[NUMERAL] (ARITH_RULE `a + b = 0 <=> a = 0 /\ b = 0`);;
 368
 369 let eq_0_i i =
 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]);;
 372
 373 let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);;
 374
 375 let th_eq0_table = Hashtbl.create maximum;;
 376
 377 for i = 0 to maximum - 1 do
 378   Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i)
 379 done;;
 380
 381 let rec raw_eq0_hash_conv rtm =
 382   if (rtm = zero_const) then
 383     EQ_0_0
 384   else
 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
 390           TRANS th0 th1
 391       else
 392         INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);;
 393
 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);;
 398
 399 (**************************************)
 400 (* PRE_CONV *)
 401
 402 (* Theorems *)
 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]);;
 406
 407 let PRE_0 = prove(`PRE _0 = _0`,
 408                   MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
 409
 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]);;
 412
 413
 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]);;
 419
 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);;
 424
 425 let PRE_lemma = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o ARITH_RULE) `((n = 0) <=> F) ==> (SUC m = n <=> PRE n = m)`;;
 426
 427 let pre_th i =
 428   let pre = i - 1 in
 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);;
 436
 437
 438 let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);;
 439
 440 let th_pre_table = Hashtbl.create maximum;;
 441
 442 for i = 0 to maximum - 1 do
 443   Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i)
 444 done;;
 445
 446 (* Conversion *)
 447 let b1_name = names_array.(1);;
 448 let b1_pre_thm = th_pre_array.(1);;
 449
 450 let rec raw_pre_hash_conv tm =
 451   let otm = rand tm in
 452     if (otm = zero_const) then
 453       PRE_0
 454     else
 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)
 465             else
 466               let th = INST[ntm, n_var_num] PRE_B0_n0 in
 467                 MY_PROVE_HYP n_th th
 468         else
 469           if (cn = b1_name) then
 470             if (ntm = zero_const) then
 471               PRE_B1_0
 472             else
 473               INST[ntm, n_var_num] b1_pre_thm
 474           else
 475             INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);;
 476
 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")
 482     else
 483       let ltm, rtm = dest_comb rhs in
 484         TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));;
 485
 486 (**************************************)
 487 (* GT0_CONV *)
 488
 489 let gt0_table = Hashtbl.create maximum;;
 490
 491 let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
 492
 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);;
 496
 497 let gt0_th i =
 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);;
 502
 503 for i = 1 to maximum - 1 do
 504   Hashtbl.add gt0_table names_array.(i) (gt0_th i)
 505 done;;
 506
 507 let rec raw_gt0_hash_conv rtm =
 508   if (rtm = zero_const) then
 509     gt0_0
 510   else
 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
 516           TRANS th0 th1
 517       else
 518         INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);;
 519
 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);;
 524
 525 (*************************************)
 526 (* EQ *)
 527
 528 let EQ_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m = NUMERAL n <=> m = n`, REWRITE_TAC[NUMERAL]);;
 529
 530
 531 (* EQ tables *)
 532
 533 (* Generates the theorem |- D_i(m) = D_j(n) <=> F if i <> j and D_i(m) = D_i(n) <=> m = n *)
 534 let gen_bi_eq_bj =
 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
 544                          [
 545                            FIRST_ASSUM (ASSUME_TAC o MATCH_MP DIV_EQ_0) THEN ASM_REWRITE_TAC[];
 546                            ALL_TAC
 547                          ] THEN
 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
 551     fun i j ->
 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
 555         if i = j then
 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)
 557         else
 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);;
 560
 561
 562 let gen_next_eq_thm =
 563   let suc_eq_th = ARITH_RULE `SUC m = SUC n <=> m = n` in
 564     fun th ->
 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;;
 572
 573
 574 let th_eq_table = Hashtbl.create (maximum * maximum);;
 575
 576
 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)
 585   else () in
 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
 592         if y > x then
 593           Hashtbl.add th_eq_table (name_right ^ name_left) (sym !th)
 594         else
 595           ()
 596     done;
 597 done;;
 598
 599
 600 (* Conversion *)
 601
 602 let eq_0_sym = (REWRITE_RULE[NUMERAL] o prove)(`0 = n <=> n = 0`, REWRITE_TAC[EQ_SYM_EQ]);;
 603
 604 let rec raw_eq_hash_conv tm =
 605   let ltm, rtm = dest_comb tm in
 606   let ltm = rand ltm in
 607     if is_const rtm then
 608       (* n = _0 *)
 609       raw_eq0_hash_conv ltm
 610     else
 611       (* n <> _0 *)
 612       if is_const ltm then
 613         (* m = _0 *)
 614         let th0 = raw_eq0_hash_conv rtm in
 615         let th1 = INST[rtm, n_var_num] eq_0_sym in
 616           TRANS th1 th0
 617       else
 618         (* m <> _0 *)
 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
 624           if cbm <> cbn then
 625             th0
 626           else
 627             let th1 = raw_eq_hash_conv (rand (concl th0)) in
 628               TRANS th0 th1;;
 629
 630
 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);;
 637
 638
 639
 640 (*************************************)
 641 (* LT and LE *)
 642
 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]);;
 645
 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
 649                        ARITH_TAC);;
 650
 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
 654                        ARITH_TAC);;
 655
 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`;;
 658
 659 (* LT tables *)
 660
 661 (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *)
 662 let gen_0_lt_bi i =
 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
 665     if i > 0 then
 666       (PURE_REWRITE_RULE[NUMERAL] o EQT_INTRO o prove)(lt_tm, REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
 667     else
 668       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `0 < n`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
 669
 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
 675 done;;
 676
 677
 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
 683   let rhs =
 684     if i >= j then
 685       mk_binop lt_op_num m_var_num n_var_num
 686     else
 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);;
 689
 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;;
 700
 701 let th_lt_table = Hashtbl.create (maximum * maximum);;
 702
 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
 708
 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
 715     done;
 716 done;;
 717
 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
 723
 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
 730     done;
 731 done;;
 732
 733 (* LE tables *)
 734
 735 (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *)
 736 let gen_bi_le_0 i =
 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
 739     if i > 0 then
 740       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, f_const), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
 741     else
 742       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `n <= 0`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
 743
 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
 749 done;;
 750
 751
 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
 757   let rhs =
 758     if i > j then
 759       mk_binop lt_op_num m_var_num n_var_num
 760     else
 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);;
 763
 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;;
 774
 775 let th_le_table = Hashtbl.create (maximum * maximum);;
 776
 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
 782
 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
 789     done;
 790 done;;
 791
 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
 797
 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
 804     done;
 805 done;;
 806
 807 (* Conversions *)
 808
 809 let rec raw_lt_hash_conv tm =
 810   let ltm, rtm = dest_comb tm in
 811   let ltm = rand ltm in
 812     if is_const rtm then
 813       (* n < _0 <=> F *)
 814       INST[ltm, n_var_num] LT_n_0
 815     else
 816       if is_const ltm then
 817         (* _0 < Bi(n) *)
 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
 823               TRANS th0 th1
 824           else
 825             th0
 826       else
 827         (* Bi(n) < Bj(m) *)
 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
 834         let th1 =
 835           if op = "<" then
 836             raw_lt_hash_conv (rand (concl th0))
 837           else
 838             raw_le_hash_conv (rand (concl th0)) in
 839           TRANS th0 th1 and
 840
 841     raw_le_hash_conv tm =
 842   let ltm, rtm = dest_comb tm in
 843   let ltm = rand ltm in
 844     if is_const ltm then
 845       (* _0 <= n <=> T *)
 846       INST[rtm, n_var_num] LE_0_n
 847     else
 848       if is_const rtm then
 849         (* Bi(n) <= _0 *)
 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
 855               TRANS th0 th1
 856           else
 857             th0
 858       else
 859         (* Bi(n) <= Bj(m) *)
 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
 866         let th1 =
 867           if op = "<" then
 868             raw_lt_hash_conv (rand (concl th0))
 869           else
 870             raw_le_hash_conv (rand (concl th0)) in
 871           TRANS th0 th1;;
 872
 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);;
 879
 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);;
 886
 887
 888 (**************************************)
 889 (* ADD_CONV *)
 890
 891 (* ADD theorems *)
 892
 893 let ADD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
 894   (`NUMERAL m + NUMERAL n = NUMERAL (m + n)`, REWRITE_TAC[NUMERAL]);;
 895
 896
 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]);;
 899
 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);;
 904
 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);;
 908
 909 let SUC_ADD_RIGHT = prove(`SUC(m + n) = m + SUC n`, ARITH_TAC);;
 910
 911
 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;;
 926
 927 let th_add_array = Array.make (maximum * maximum) (REFL zero_const);;
 928
 929 for i = 0 to maximum - 1 do
 930   let th0 =
 931     if i = 0 then
 932       B0_ADD
 933     else
 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
 937
 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)
 940     done;
 941 done;;
 942
 943 (* SUC (B_i(m) + B_j(n)) = B_p(...) *)
 944 let th_cadd i j =
 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
 951     TRANS th0 suc_th;;
 952
 953 let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);;
 954
 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
 958   done;
 959 done;;
 960
 961 let th_add_table = Hashtbl.create (maximum * maximum);;
 962
 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)
 969   done;
 970 done;;
 971
 972 let th_cadd_table = Hashtbl.create (maximum * maximum);;
 973
 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)
 980   done;
 981 done;;
 982
 983 (* ADD conversion *)
 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
 991     else
 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
 998         if cflag then
 999           TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1000         else
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)))
1011     else
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
1018         if cflag then
1019           TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1020         else
1021           TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1022
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));;
1029
1030 (********************************)
1031 (* Subtraction *)
1032
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]);;
1036
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`;;
1040
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
1046   let t = m -/ n in
1047     if t >=/ num_0 then
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
1052     else
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;;
1057
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
1062   let t = m -/ n in
1063     if t >=/ num_0 then
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)
1070     else
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);;
1077
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));;
1084
1085
1086 (********************************)
1087 (* Multiplication *)
1088
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]);;
1092
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]);;
1096
1097 let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;;
1098
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;;
1104
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);;
1108
1109 let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
1110
1111 let MUL_SUC_RIGHT = prove(`m * SUC(n) = m * n + m`, ARITH_TAC);;
1112
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;;
1125
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
1130
1131     for j = 2 to maximum - 1 do
1132       mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1)
1133     done;
1134 done;;
1135
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)
1140   done;
1141 done;;
1142
1143 (* General multiplication theorem *)
1144 let prod_lemma =
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]);;
1159
1160 let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;;
1161
1162 let dest_op tm =
1163   let ltm, rtm = dest_comb tm in
1164     rand ltm, rtm;;
1165
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)
1187     else
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
1199         TRANS th2 th4;;
1200
1201 let gen_mul_table = Hashtbl.create (maximum * maximum);;
1202
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)
1207   done;
1208 done;;
1209
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)
1227     else
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);;
1231
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;;
1234
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))
1246     else
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));;
1249
1250 let mul1_right_th_table = Hashtbl.create (maximum * maximum);;
1251 let mul1_left_th_table = Hashtbl.create (maximum * maximum);;
1252
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)
1261   done;
1262 done;;
1263
1264
1265 (******************************************************)
1266 (* Conversions *)
1267
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
1272   else
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))
1278       else
1279         let name = cn ^ tmname in
1280           if (mtm = zero_const) then
1281             Hashtbl.find mul_table name
1282           else
1283             let add_flag, th' = Hashtbl.find mul1_right_th_table name in
1284             let th = INST[mtm, m_var_num] th' in
1285               if add_flag then
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))
1291               else
1292                 let ltm = rator(rand(concl th)) in
1293                 let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in
1294                   TRANS th th2;;
1295
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
1300   else
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))
1306       else
1307         let name = tmname ^ cn in
1308           if (mtm = zero_const) then
1309             Hashtbl.find mul_table name
1310           else
1311             let add_flag, th' = Hashtbl.find mul1_left_th_table name in
1312             let th = INST[mtm, m_var_num] th' in
1313               if add_flag then
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))
1319               else
1320                 let ltm = rator(rand(concl th)) in
1321                 let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in
1322                   TRANS th th2;;
1323
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
1332     else
1333
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))
1340         else
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))
1347             else
1348
1349               if (ntm = zero_const) then
1350                 if (mtm = zero_const) then
1351                   Hashtbl.find mul_table (lcn ^ rcn)
1352                 else
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
1356               else
1357
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
1368
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
1372
1373                   TRANS th0 (AP_TERM b_low add);;
1374
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"
1382     else
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);;
1386
1387
1388 (************************************)
1389 (* DIV *)
1390
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]);;
1394
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;;
1399
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
1410
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);;
1418
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"
1426     else
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);;
1430
1431
1432 (*********************************************)
1433 (* EVEN_CONV, ODD_CONV *)
1434
1435 let even_const = `EVEN` and
1436     odd_const = `ODD` and
1437     eq_const = `<=>`;;
1438
1439 let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1440   (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);;
1441
1442 let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1443   (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
1444
1445 let EVEN_ZERO = prove(`EVEN _0 <=> T`, REWRITE_TAC[ARITH_EVEN]);;
1446 let ODD_ZERO = prove(`ODD _0 <=> F`, REWRITE_TAC[ARITH_ODD]);;
1447
1448
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);;
1452
1453
1454 let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
1455                    REWRITE_TAC[NOT_ODD; EVEN_B0]);;
1456
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]);;
1459
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]);;
1462
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;;
1472
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;;
1482
1483 let even_thm_table = Hashtbl.create maximum;;
1484
1485 Hashtbl.add even_thm_table names_array.(0) EVEN_B0;;
1486
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
1490 done;;
1491
1492 let odd_thm_table = Hashtbl.create maximum;;
1493 Hashtbl.add odd_thm_table names_array.(0) ODD_B0;;
1494
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
1498 done;;
1499
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"
1504     else
1505       if (is_const rtm) then
1506         EVEN_ZERO
1507       else
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;;
1511
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"
1516     else
1517       if (is_const rtm) then
1518         ODD_ZERO
1519       else
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;;
1523
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"
1530     else
1531       let th1 = raw_even_hash_conv rtm in
1532         TRANS th0 th1;;
1533
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"
1540     else
1541       let th1 = raw_odd_hash_conv rtm in
1542         TRANS th0 th1;;
1543
1544 end;;