formal_lp/old/arith/arith_hash2.hl

   1 module type Arith_hash_sig =
   2   sig
   3     val num_def : thm
   4     val NUM_THM : thm
   5     val num_const : term
   6     val const_array : term array
   7     val def_array: thm array
   8     val def_thm_array: thm array
   9     val mk_numeral_hash : num -> term
  10     val mk_numeral_array : num -> term
  11     val mk_small_numeral_array : int -> term
  12     val raw_dest_hash : term -> num
  13     val dest_numeral_hash : term -> num
  14     val NUMERAL_TO_NUM_CONV : term -> thm
  15     val NUM_TO_NUMERAL_CONV : term -> thm
  16     val raw_suc_conv_hash : term -> thm
  17     val NUM_SUC_HASH_CONV : term -> thm
  18     val raw_eq0_hash_conv : term -> thm
  19     val NUM_EQ0_HASH_CONV : term -> thm
  20     val raw_pre_hash_conv : term -> thm
  21     val NUM_PRE_HASH_CONV : term -> thm
  22     val raw_gt0_hash_conv : term -> thm
  23     val NUM_GT0_HASH_CONV : term -> thm
  24     val raw_lt_hash_conv : term -> thm
  25     val raw_le_hash_conv : term -> thm
  26     val NUM_LT_HASH_CONV : term -> thm
  27     val NUM_LE_HASH_CONV : term -> thm
  28     val raw_add_conv_hash : term -> thm
  29     val NUM_ADD_HASH_CONV : term -> thm
  30     val raw_sub_hash_conv : term -> thm
  31     val raw_sub_and_le_hash_conv : term -> term -> thm * thm
  32     val NUM_SUB_HASH_CONV : term -> thm
  33     val raw_mul_conv_hash : term -> thm
  34     val NUM_MULT_HASH_CONV : term -> thm
  35     val raw_div_hash_conv : term -> thm
  36     val NUM_DIV_HASH_CONV : term -> thm
  37
  38     val raw_even_hash_conv : term -> thm
  39     val raw_odd_hash_conv : term -> thm
  40     val NUM_EVEN_HASH_CONV : term -> thm
  41     val NUM_ODD_HASH_CONV : term -> thm
  42 end;;
  43
  44 (* Dependencies *)
  45 needs "../formal_lp/arith/misc.hl";;
  46 needs "../formal_lp/arith/arith_options.hl";;
  47
  48 module Arith_hash : Arith_hash_sig = struct
  49
  50 open Arith_misc;;
  51 open Arith_options;;
  52
  53 let maximum = base;;
  54
  55 (******************)
  56
  57 (* Generate definitions and constants *)
  58
  59 let num_type = `:num`;;
  60 let fnum_type = `:num->num`;;
  61
  62 let numeral_const = `NUMERAL` and
  63     zero_const = `_0` and
  64     bit0_const = `BIT0` and
  65     bit1_const = `BIT1` and
  66     truth_const = `T` and
  67     false_const = `F`;;
  68
  69 let m_var_num = `m:num` and
  70     n_var_num = `n:num` and
  71     t_var_num = `t:num` and
  72     r_var_num = `r:num` and
  73     p_var_num = `p:num` and
  74     q_var_num = `q:num`;;
  75
  76 let suc_const = `SUC` and
  77     plus_op_num = `(+):num->num->num` and
  78     minus_op_num = `(-):num->num->num` and
  79     mul_op_num = `( * ):num->num->num` and
  80     div_op_num = `(DIV):num->num->num` and
  81     le_op_num = `(<=):num->num->bool` and
  82     lt_op_num = `(<):num->num->bool`;;
  83
  84
  85 let plus_op_real = `(+):real->real->real` and
  86     mul_op_real = `( * ):real->real->real`;;
  87
  88
  89
  90 let names_array = Array.init maximum (fun i -> "D"^(string_of_int i));;
  91
  92
  93 (* Definitions *)
  94
  95 let num_name = "NUM"^(string_of_int base);;
  96 let num_def = new_basic_definition (mk_eq(mk_var(num_name, fnum_type), numeral_const));;
  97 let num_const = mk_const(num_name, []);;
  98 let num_def_sym = SYM num_def;;
  99 let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
 100                     REWRITE_TAC[num_def; NUMERAL]);;
 101
 102
 103
 104 (* B_i(n) = i + B_0(n) *)
 105 let mk_bit_definition i =
 106   let lhs = mk_var (names_array.(i), fnum_type) in
 107   let tm1 = mk_binop mul_op_num (mk_small_numeral base) n_var_num in
 108   let tm2 = mk_binop plus_op_num tm1 (mk_small_numeral i) in
 109   let rhs = mk_abs (n_var_num, tm2) in
 110     new_basic_definition (mk_eq (lhs, rhs));;
 111
 112
 113
 114 let def_basic_array = Array.init maximum mk_bit_definition;;
 115 let def_array = Array.init maximum (fun i ->
 116                                       let basic = def_basic_array.(i) in
 117                                       let th1 = AP_THM basic n_var_num in
 118                                         TRANS th1 (BETA (rand (concl th1))));;
 119 let def_table = Hashtbl.create maximum;;
 120 let def_basic_table = Hashtbl.create maximum;;
 121
 122 for i = 0 to maximum - 1 do
 123   let _ = Hashtbl.add def_table names_array.(i) def_array.(i) in
 124     Hashtbl.add def_basic_table names_array.(i) def_basic_array.(i)
 125 done;;
 126
 127
 128 (* Constants *)
 129
 130
 131 let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));;
 132
 133 let b0_def = def_array.(0);;
 134 let b0_const = const_array.(0);;
 135 let b0_name = names_array.(0);;
 136
 137 let max_const = mk_small_numeral maximum;;
 138
 139
 140
 141 (* Alternative definition of B_i *)
 142
 143 let ADD_0_n = prove(`_0 + n = n`,
 144                     ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
 145                       REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
 146 let ADD_n_0 = prove(`n + _0 = n`,
 147                     ONCE_REWRITE_TAC[GSYM NUMERAL] THEN
 148                       REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
 149
 150 let MUL_n_0 = prove(`n * _0 = 0`,
 151                     REWRITE_TAC[NUMERAL] THEN
 152                       SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
 153                       DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
 154                       ARITH_TAC);;
 155
 156
 157 (* B_i(n) = i + B_0(n) *)
 158 let def_thm i =
 159   let bin = mk_comb(const_array.(i), n_var_num) in
 160   let bi0 = mk_comb(const_array.(i), zero_const) in
 161   let b0n = mk_comb(const_array.(0), n_var_num) in
 162   let rhs = mk_binop plus_op_num bi0 b0n in
 163     prove(mk_eq(bin, rhs), REWRITE_TAC[def_array.(i); def_array.(0)] THEN
 164             REWRITE_TAC[MUL_n_0; ADD_CLAUSES] THEN ARITH_TAC);;
 165
 166
 167 let def_thm_array = Array.init maximum def_thm;;
 168
 169
 170 let B0_0 = prove(mk_eq(mk_comb(b0_const, zero_const), zero_const),
 171                  REWRITE_TAC[b0_def; MUL_n_0; ADD_CLAUSES; NUMERAL]);;
 172
 173
 174
 175 let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num),
 176                               mk_binop mul_op_num max_const n_var_num),
 177                         REWRITE_TAC[b0_def; ADD_CLAUSES]);;
 178
 179
 180
 181
 182 (******************************)
 183
 184 (* mk_numeral and dest_numeral *)
 185
 186
 187 (* mk_table *)
 188
 189 let mk_table = Hashtbl.create maximum;;
 190
 191 for i = 0 to maximum - 1 do
 192   Hashtbl.add mk_table (Int i) const_array.(i)
 193 done;;
 194
 195
 196 (* mk_numeral *)
 197 let max_num = Int maximum;;
 198
 199
 200 let mk_numeral_hash =
 201   let rec mk_num n =
 202     if (n =/ num_0) then
 203       zero_const
 204     else
 205       let m = mod_num n max_num in
 206       let bit = Hashtbl.find mk_table m in
 207         mk_comb(bit, mk_num(quo_num n max_num)) in
 208   fun n -> if n </ num_0 then failwith "mk_numeral_hash: negative argument"
 209   else mk_comb(num_const, mk_num n);;
 210
 211
 212 let mk_numeral_array =
 213   let rec mk_num n =
 214     if (n =/ num_0) then
 215       zero_const
 216     else
 217       let m = Num.int_of_num (mod_num n max_num) in
 218       let bit = const_array.(m) in
 219         mk_comb(bit, mk_num(quo_num n max_num)) in
 220     fun n -> if n </ num_0 then failwith "mk_numeral_array: negative argument"
 221     else mk_comb(num_const, mk_num n);;
 222
 223
 224 let mk_small_numeral_array =
 225   let rec mk_num n =
 226     if (n = 0) then zero_const
 227     else
 228       let m = n mod maximum in
 229       let bit = const_array.(m) in
 230         mk_comb(bit, mk_num(n / maximum)) in
 231     fun n -> if n < 0 then failwith "mk_small_numeral_array: negative argument"
 232     else mk_comb (num_const, mk_num n);;
 233
 234
 235
 236 (*
 237 (* 10: 1.232 *)
 238 test 10000 mk_numeral_hash (Int 65535);; (* 0.736 *)
 239 (* 10: 1.216 *)
 240 test 10000 mk_numeral_array (Int 65535);; (* 0.728 *)
 241 (* 10: 0.272 *)
 242 test 100000 mk_small_numeral_array 65535;; (* 0.216 *)
 243 (* 10: 0.316 *)
 244 test 1000 mk_numeral_array (num_of_string "9111111111111111");; (* 0.288 *)
 245 *)
 246
 247
 248
 249
 250 (* dest_table *)
 251
 252 let dest_table_num = Hashtbl.create maximum;;
 253
 254 for i = 0 to maximum - 1 do
 255   Hashtbl.add dest_table_num names_array.(i) (Int i)
 256 done;;
 257
 258
 259
 260 (* dest_numeral *)
 261
 262 let max_num = Int maximum;;
 263
 264
 265 let rec raw_dest_hash tm =
 266   if tm = zero_const then
 267     num_0
 268   else
 269     let l, r = dest_comb tm in
 270     let n = max_num */ raw_dest_hash r in
 271     let cn = fst(dest_const l) in
 272       n +/ (Hashtbl.find dest_table_num cn);;
 273
 274
 275 let dest_numeral_hash tm = raw_dest_hash (rand tm);;
 276
 277
 278
 279
 280 (*
 281 (* 10: 0.852 *)
 282 test 100000 dest_numeral_hash (mk_numeral_array (Int 11111111));;
 283 *)
 284
 285
 286
 287
 288 (******************************)
 289
 290 (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *)
 291
 292
 293 let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));;
 294 let mod_op_num = `MOD`;;
 295 let zero = `0`;;
 296
 297
 298 let DIV_BASE =
 299   let h1 = mk_eq(mk_binop div_op_num m_var_num max_const, q_var_num) in
 300   let h2 = mk_eq(mk_binop mod_op_num m_var_num max_const, r_var_num) in
 301   let c = mk_eq(m_var_num, mk_binop plus_op_num (mk_binop mul_op_num max_const q_var_num) r_var_num) in
 302     (UNDISCH_ALL o ARITH_RULE) (mk_imp(h1, mk_imp(h2, c)));;
 303
 304
 305 let ZERO_EQ_ZERO = (EQT_ELIM o REWRITE_CONV[NUMERAL]) `0 = _0`;;
 306 let SYM_ZERO_EQ_ZERO = SYM ZERO_EQ_ZERO;;
 307 let SYM_NUM_THM = SYM NUM_THM;;
 308
 309
 310
 311 let NUMERAL_TO_NUM_CONV tm =
 312   let rec raw_conv tm =
 313     if (rand tm = zero_const) then
 314       ZERO_EQ_ZERO
 315     else
 316       let th_div = NUM_DIV_CONV (mk_binop div_op_num tm max_const) in
 317       let th_mod = NUM_MOD_CONV (mk_binop mod_op_num tm max_const) in
 318       let q_tm = rand(concl th_div) in
 319       let r_tm = rand(concl th_mod) in
 320       let th0 = INST[tm, m_var_num; q_tm, q_var_num; r_tm, r_var_num] DIV_BASE in
 321       let th1 = MY_PROVE_HYP th_mod (MY_PROVE_HYP th_div th0) in
 322       let r = dest_small_numeral r_tm in
 323       let th2 = INST[q_tm, n_var_num] th_num_conv.(r) in
 324       let th = TRANS th1 th2 in
 325       let ltm, rtm = dest_comb(rand(concl th)) in
 326       let r_th = raw_conv rtm in
 327         TRANS th (AP_TERM ltm r_th) in
 328
 329     if (fst o dest_const o rator) tm <> "NUMERAL" then
 330       failwith "NUMERAL_TO_NUM_CONV"
 331     else
 332       let th0 = raw_conv tm in
 333       let n_tm = rand(concl th0) in
 334         TRANS th0 (INST[n_tm, n_var_num] SYM_NUM_THM);;
 335
 336
 337 (*
 338 (* 100: 2.588 *)
 339 test 100 NUMERAL_TO_NUM_CONV `100034242430`;;
 340 *)
 341
 342
 343
 344 let replace_numerals = rand o concl o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
 345 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;
 346
 347
 348
 349 (* NUM_TO_NUMERAL_CONV *)
 350
 351
 352 let NUM_TO_NUMERAL_CONV tm =
 353   let rec raw_conv tm =
 354     if tm = zero_const then
 355       SYM_ZERO_EQ_ZERO
 356     else
 357       let b_tm, n_tm = dest_comb tm in
 358       let n_th = raw_conv n_tm in
 359       let n_tm' = rand(concl n_th) in
 360       let cb = (fst o dest_const) b_tm in
 361       let th0 = Hashtbl.find def_table cb in
 362       let th1 = AP_TERM b_tm n_th in
 363       let th2 = TRANS th1 (INST[n_tm', n_var_num] th0) in
 364       let ltm, rtm = dest_comb(rand(concl th2)) in
 365       let mul_th = NUM_MULT_CONV (rand ltm) in
 366       let add_th0 = AP_THM (AP_TERM plus_op_num mul_th) rtm in
 367       let add_th = TRANS add_th0 (NUM_ADD_CONV (rand(concl add_th0))) in
 368         TRANS th2 add_th in
 369   let ltm, rtm = dest_comb tm in
 370     if (fst o dest_const) ltm <> num_name then
 371       failwith "NUM_TO_NUMERAL_CONV"
 372     else
 373       let num_th = INST[rtm, n_var_num] NUM_THM in
 374       let th0 = raw_conv rtm in
 375         TRANS num_th th0;;
 376
 377
 378
 379
 380
 381 (*************************)
 382
 383 (* SUC_CONV *)
 384
 385 let suc_const = `SUC`;;
 386
 387 (* Theorems *)
 388
 389 let SUC_NUM = prove(mk_eq(mk_comb(suc_const, mk_comb (num_const, n_var_num)),
 390                           mk_comb(num_const, mk_comb (suc_const, n_var_num))),
 391                     REWRITE_TAC[num_def; NUMERAL]);;
 392
 393 let SUC_0 = prove(mk_eq(`SUC _0`, mk_comb (const_array.(1), zero_const)),
 394                   REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_SUC; NUMERAL; ARITH_ADD]);;
 395
 396
 397 let suc_th i =
 398   let cflag = (i + 1 >= maximum) in
 399   let suc = if (cflag) then 0 else i + 1 in
 400   let lhs = mk_comb(suc_const, (mk_comb (const_array.(i), n_var_num))) in
 401   let rhs = mk_comb(const_array.(suc),
 402                     if (cflag) then mk_comb(suc_const, n_var_num) else n_var_num) in
 403   let proof = REWRITE_TAC [def_array.(i); def_array.(suc)] THEN ARITH_TAC in
 404     prove(mk_eq(lhs, rhs), proof);;
 405
 406
 407 let th_suc_array = Array.init maximum suc_th;;
 408
 409 let th_suc_table = Hashtbl.create maximum;;
 410
 411 for i = 0 to maximum - 1 do
 412   Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i)
 413 done;;
 414
 415 let SUC_MAX = th_suc_array.(maximum - 1);;
 416 let bit_max_name = names_array.(maximum - 1);;
 417
 418
 419 (* Conversion *)
 420
 421 let rec raw_suc_conv_hash tm =
 422   let otm = rand tm in
 423     if (otm = zero_const) then
 424       SUC_0
 425     else
 426       let btm, ntm = dest_comb otm in
 427       let cn = fst(dest_const btm) in
 428         if (cn = bit_max_name) then
 429           let th = INST [ntm, n_var_num] SUC_MAX in
 430           let ltm, rtm = dest_comb(rand(concl th)) in
 431             TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm))
 432         else
 433           INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);;
 434
 435
 436
 437 let NUM_SUC_HASH_CONV tm =
 438   let ntm = rand (rand tm) in
 439   let th = INST [ntm, n_var_num] SUC_NUM in
 440   let lhs, rhs = dest_eq(concl th) in
 441     if (lhs <> tm) then failwith("NUM_SUC_HASH_CONV")
 442     else
 443       let ltm, rtm = dest_comb rhs in
 444         TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));;
 445
 446
 447
 448
 449
 450 (*
 451 let x = mk_comb(suc_const, mk_small_numeral_array 99999);;
 452 NUM_SUC_HASH_CONV x;;
 453 (* 10: 1.488 *)
 454 test 50000 NUM_SUC_HASH_CONV x;; (* 5: 0.980 *)
 455 *)
 456
 457
 458 (**************************************)
 459
 460 (* EQ_0_CONV *)
 461
 462 let EQ_0_NUM = prove(mk_eq(mk_eq(mk_comb(num_const, n_var_num), `_0`), `n = _0`),
 463                      REWRITE_TAC[num_def; NUMERAL]);;
 464
 465 let EQ_B0_0 = prove(mk_eq(mk_eq(mk_comb(b0_const, n_var_num), `_0`), `n = _0`),
 466                     REWRITE_TAC[b0_def; ADD_CLAUSES; NUMERAL; REWRITE_RULE[NUMERAL] MULT_EQ_0; ARITH_EQ]);;
 467
 468 let EQ_0_0 = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH_EQ]);;
 469
 470 let eq_0_lemma = REWRITE_RULE[NUMERAL] (ARITH_RULE `a + b = 0 <=> a = 0 /\ b = 0`);;
 471
 472 let eq_0_i i =
 473   let concl = mk_eq(mk_eq(mk_comb(const_array.(i), n_var_num), zero_const), false_const) in
 474     prove(concl, REWRITE_TAC[def_array.(i); eq_0_lemma; NUMERAL; ARITH_EQ]);;
 475
 476 let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);;
 477
 478 let th_eq0_table = Hashtbl.create maximum;;
 479
 480 for i = 0 to maximum - 1 do
 481   Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i)
 482 done;;
 483
 484
 485
 486 let rec raw_eq0_hash_conv rtm =
 487   if (rtm = zero_const) then
 488     EQ_0_0
 489   else
 490     let b_tm, n_tm = dest_comb rtm in
 491     let cn = (fst o dest_const) b_tm in
 492       if (cn = b0_name) then
 493         let th0 = INST[n_tm, n_var_num] EQ_B0_0 in
 494         let th1 = raw_eq0_hash_conv n_tm in
 495           TRANS th0 th1
 496       else
 497         INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);;
 498
 499
 500
 501 let NUM_EQ0_HASH_CONV rtm =
 502   let n_tm = rand rtm in
 503   let th = INST [n_tm, n_var_num] EQ_0_NUM in
 504     TRANS th (raw_eq0_hash_conv n_tm);;
 505
 506
 507 (*
 508 let x = mk_small_numeral_array 0;;
 509 NUM_EQ0_HASH_CONV x;;
 510 raw_eq0_hash_conv `B0 (B0 _0)`;;
 511 *)
 512
 513
 514 (**************************************)
 515
 516 (* PRE_CONV *)
 517
 518 let pre_const = `PRE`;;
 519
 520 (* Theorems *)
 521
 522 let PRE_NUM = prove(mk_eq(mk_comb(pre_const, mk_comb (num_const, n_var_num)),
 523                           mk_comb(num_const, mk_comb (pre_const, n_var_num))),
 524                     REWRITE_TAC[num_def; NUMERAL]);;
 525
 526
 527 let PRE_0 = prove(`PRE _0 = _0`,
 528                   MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
 529
 530 let PRE_B1_0 = prove(mk_eq(mk_comb(`PRE`, mk_comb(const_array.(1), `_0`)), `_0`),
 531                      REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_ADD; NUMERAL; ARITH_PRE; ARITH_EQ]);;
 532
 533
 534 let PRE_B0_n0 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> T`,
 535                      mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), `_0`)),
 536                                       REWRITE_TAC[B0_EXPLICIT] THEN
 537                                         DISCH_THEN (fun th -> REWRITE_TAC[th; MUL_n_0]) THEN
 538                                         REWRITE_TAC[NUMERAL; ARITH_PRE]);;
 539
 540
 541 let PRE_B0_n1 = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o prove)(mk_imp(`n = 0 <=> F`,
 542                      mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)),
 543                            mk_comb(const_array.(maximum - 1), `PRE n`))),
 544                         REWRITE_TAC[B0_EXPLICIT; def_array.(maximum - 1)] THEN ARITH_TAC);;
 545
 546
 547 let PRE_lemma = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o ARITH_RULE) `((n = 0) <=> F) ==> (SUC m = n <=> PRE n = m)`;;
 548
 549
 550 let pre_th i =
 551   let pre = i - 1 in
 552   let pre_tm = mk_comb(const_array.(pre), n_var_num) in
 553   let suc_tm = mk_comb(suc_const, pre_tm) in
 554   let suc_th = raw_suc_conv_hash suc_tm in
 555   let n_tm = rand(concl suc_th) in
 556   let n0_th = raw_eq0_hash_conv n_tm in
 557   let th0 = INST[pre_tm, m_var_num; n_tm, n_var_num] PRE_lemma in
 558     MY_PROVE_HYP n0_th (EQ_MP th0 suc_th);;
 559
 560
 561
 562
 563 let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);;
 564
 565 let th_pre_table = Hashtbl.create maximum;;
 566
 567 for i = 0 to maximum - 1 do
 568   Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i)
 569 done;;
 570
 571
 572 (* Conversion *)
 573 let b1_name = names_array.(1);;
 574 let b1_pre_thm = th_pre_array.(1);;
 575
 576 let rec raw_pre_hash_conv tm =
 577   let otm = rand tm in
 578     if (otm = zero_const) then
 579       PRE_0
 580     else
 581       let btm, ntm = dest_comb otm in
 582       let cn = fst(dest_const btm) in
 583         if (cn = b0_name) then
 584           let n_th = raw_eq0_hash_conv ntm in
 585             if (rand(concl n_th) = false_const) then
 586               let th0 = INST[ntm, n_var_num] PRE_B0_n1 in
 587               let th1 = MY_PROVE_HYP n_th th0 in
 588               let ltm, rtm = dest_comb(rand(concl th1)) in
 589               let th2 = raw_pre_hash_conv rtm in
 590                 TRANS th1 (AP_TERM ltm th2)
 591             else
 592               let th = INST[ntm, n_var_num] PRE_B0_n0 in
 593                 MY_PROVE_HYP n_th th
 594         else
 595           if (cn = b1_name) then
 596             if (ntm = zero_const) then
 597               PRE_B1_0
 598             else
 599               INST[ntm, n_var_num] b1_pre_thm
 600           else
 601             INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);;
 602
 603
 604
 605 let NUM_PRE_HASH_CONV tm =
 606   let ntm = rand (rand tm) in
 607   let th = INST [ntm, n_var_num] PRE_NUM in
 608   let lhs, rhs = dest_eq(concl th) in
 609     if (lhs <> tm) then failwith("NUM_PRE_HASH_CONV")
 610     else
 611       let ltm, rtm = dest_comb rhs in
 612         TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));;
 613
 614
 615 (*
 616 let x = mk_comb(pre_const, mk_small_numeral_array 100000);;
 617 NUM_PRE_HASH_CONV x;;
 618 (* 10: 0.488; 100: 0.200 *)
 619 test 5000 NUM_PRE_HASH_CONV x;;
 620 let x = mk_comb(pre_const, mk_small_numeral_array 65536);;
 621 (* 10: 0.468; 100: 0.496 *)
 622 test 50000 NUM_PRE_HASH_CONV x;;
 623 *)
 624
 625
 626
 627
 628 (**************************************)
 629
 630 (* GT0_CONV *)
 631
 632
 633 let gt0_table = Hashtbl.create maximum;;
 634
 635 let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
 636
 637 let gt0_0 = prove(`_0 < _0 <=> F`, REWRITE_TAC[ARITH_LT]);;
 638 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`),
 639                    REWRITE_TAC[b0_def] THEN ARITH_TAC);;
 640
 641
 642 let zero = `0`;;
 643
 644 let gt0_th i =
 645   let bi = const_array.(i) in
 646   let concl = mk_eq (mk_binop lt_op_num zero (mk_comb(bi, n_var_num)), truth_const) in
 647   let proof = REWRITE_TAC[def_array.(i)] THEN ARITH_TAC in
 648     (PURE_REWRITE_RULE[NUMERAL] o prove)(concl, proof);;
 649
 650
 651 for i = 1 to maximum - 1 do
 652   Hashtbl.add gt0_table names_array.(i) (gt0_th i)
 653 done;;
 654
 655
 656 let rec raw_gt0_hash_conv rtm =
 657   if (rtm = zero_const) then
 658     gt0_0
 659   else
 660     let b_tm, n_tm = dest_comb rtm in
 661     let cn = (fst o dest_const) b_tm in
 662       if (cn = b0_name) then
 663         let th0 = INST[n_tm, n_var_num] gt0_b0 in
 664         let th1 = raw_gt0_hash_conv n_tm in
 665           TRANS th0 th1
 666       else
 667         INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);;
 668
 669
 670
 671 let NUM_GT0_HASH_CONV rtm =
 672   let n_tm = rand rtm in
 673   let th = INST [n_tm, n_var_num] GT0_NUM in
 674     TRANS th (raw_gt0_hash_conv n_tm);;
 675
 676
 677
 678
 679 (*
 680 let tm = mk_binop lt_op_num (mk_small_numeral_array 0) (mk_small_numeral_array 100000);;
 681 NUM_GT0_HASH_CONV (rand tm);;
 682 (* 10: 0.232 *)
 683 test 10000 NUM_GT0_HASH_CONV (rand tm);;
 684 *)
 685
 686
 687
 688 (*************************************)
 689
 690 (* LT and LE *)
 691
 692 let LT_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m < NUMERAL n <=> m < n`, REWRITE_TAC[NUMERAL]);;
 693 let LE_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m <= NUMERAL n <=> m <= n`, REWRITE_TAC[NUMERAL]);;
 694
 695 let LT_n_0 = prove(`n < _0 <=> F`,
 696                    SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
 697                        DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
 698                        ARITH_TAC);;
 699
 700 let LE_0_n = prove(`_0 <= n <=> T`,
 701                    SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN
 702                        DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
 703                        ARITH_TAC);;
 704
 705 let SUC_LT_THM = ARITH_RULE `SUC m < SUC n <=> m < n`;;
 706 let SUC_LE_THM = ARITH_RULE `SUC m <= SUC n <=> m <= n`;;
 707
 708
 709
 710 (* LT tables *)
 711
 712 (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *)
 713 let gen_0_lt_bi i =
 714   let bin = mk_comb (const_array.(i), n_var_num) in
 715   let lt_tm = mk_binop lt_op_num zero bin in
 716     if i > 0 then
 717       (PURE_REWRITE_RULE[NUMERAL] o EQT_INTRO o prove)(lt_tm, REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
 718     else
 719       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `0 < n`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
 720
 721
 722 let th_lt0_table = Hashtbl.create maximum;;
 723 for i = 0 to maximum - 1 do
 724   let th = gen_0_lt_bi i in
 725   let name = names_array.(i) in
 726     Hashtbl.add th_lt0_table name th
 727 done;;
 728
 729
 730
 731
 732 (* Generates the theorem |- bi(m) < bj(n) <=> m <= n (or m < n) *)
 733
 734 let gen_bi_lt_bj i j =
 735   let bim = mk_comb (const_array.(i), m_var_num) in
 736   let bjn = mk_comb (const_array.(j), n_var_num) in
 737   let lt_tm = mk_binop lt_op_num bim bjn in
 738   let rhs =
 739     if i >= j then
 740       mk_binop lt_op_num m_var_num n_var_num
 741     else
 742       mk_binop le_op_num m_var_num n_var_num in
 743     prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
 744
 745
 746
 747 (* Given a theorem |- bi(m) < bj(n) <=> P m n, generates the theorem
 748    |- SUC(bi(m)) < SUC(bj(n)) <=> P m n *)
 749 let gen_next_lt_thm th =
 750   let ltm, n_tm = (dest_comb o lhand o concl) th in
 751   let m_tm = rand ltm in
 752   let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LT_THM in
 753   let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
 754   let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
 755   let th1 = SYM (MK_COMB ((AP_TERM lt_op_num suc_m), suc_n)) in
 756     TRANS (TRANS th1 th0) th;;
 757
 758
 759 let th_lt_table = Hashtbl.create (maximum * maximum);;
 760
 761
 762 for i = 0 to maximum - 1 do
 763   let th = ref (gen_bi_lt_bj 0 i) in
 764   let name_left = names_array.(0) and
 765       name_right = names_array.(i) in
 766   let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
 767
 768     for k = 1 to maximum - i - 1 do
 769       let x = k and y = i + k in
 770       let name_left = names_array.(x) and
 771           name_right = names_array.(y) in
 772         th := gen_next_lt_thm (!th);
 773         Hashtbl.add th_lt_table (name_left ^ name_right) !th
 774     done;
 775 done;;
 776
 777
 778 for i = 1 to maximum - 1 do
 779   let th = ref (gen_bi_lt_bj i 0) in
 780   let name_left = names_array.(i) and
 781       name_right = names_array.(0) in
 782   let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in
 783
 784     for k = 1 to maximum - i - 1 do
 785       let x = i + k and y = k in
 786       let name_left = names_array.(x) and
 787           name_right = names_array.(y) in
 788         th := gen_next_lt_thm (!th);
 789         Hashtbl.add th_lt_table (name_left ^ name_right) !th
 790     done;
 791 done;;
 792
 793
 794
 795
 796 (* LE tables *)
 797
 798 (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *)
 799 let gen_bi_le_0 i =
 800   let bin = mk_comb (const_array.(i), n_var_num) in
 801   let lt_tm = mk_binop le_op_num bin zero in
 802     if i > 0 then
 803       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, false_const), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC)
 804     else
 805       (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `n <= 0`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
 806
 807
 808
 809 let th_le0_table = Hashtbl.create maximum;;
 810 for i = 0 to maximum - 1 do
 811   let th = gen_bi_le_0 i in
 812   let name = names_array.(i) in
 813     Hashtbl.add th_le0_table name th
 814 done;;
 815
 816
 817
 818
 819 (* Generates the theorem |- bi(m) <= bj(n) <=> m <= n (or m < n) *)
 820 let gen_bi_le_bj i j =
 821   let bim = mk_comb (const_array.(i), m_var_num) in
 822   let bjn = mk_comb (const_array.(j), n_var_num) in
 823   let lt_tm = mk_binop le_op_num bim bjn in
 824   let rhs =
 825     if i > j then
 826       mk_binop lt_op_num m_var_num n_var_num
 827     else
 828       mk_binop le_op_num m_var_num n_var_num in
 829     prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);;
 830
 831
 832
 833 (* Given a theorem |- bi(m) <= bj(n) <=> P m n, generates the theorem
 834    |- SUC(bi(m)) <= SUC(bj(n)) <=> P m n *)
 835 let gen_next_le_thm th =
 836   let ltm, n_tm = (dest_comb o lhand o concl) th in
 837   let m_tm = rand ltm in
 838   let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LE_THM in
 839   let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in
 840   let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in
 841   let th1 = SYM (MK_COMB ((AP_TERM le_op_num suc_m), suc_n)) in
 842     TRANS (TRANS th1 th0) th;;
 843
 844
 845
 846 let th_le_table = Hashtbl.create (maximum * maximum);;
 847
 848
 849 for i = 0 to maximum - 1 do
 850   let th = ref (gen_bi_le_bj 0 i) in
 851   let name_left = names_array.(0) and
 852       name_right = names_array.(i) in
 853   let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
 854
 855     for k = 1 to maximum - i - 1 do
 856       let x = k and y = i + k in
 857       let name_left = names_array.(x) and
 858           name_right = names_array.(y) in
 859         th := gen_next_le_thm (!th);
 860         Hashtbl.add th_le_table (name_left ^ name_right) !th
 861     done;
 862 done;;
 863
 864
 865 for i = 1 to maximum - 1 do
 866   let th = ref (gen_bi_le_bj i 0) in
 867   let name_left = names_array.(i) and
 868       name_right = names_array.(0) in
 869   let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in
 870
 871     for k = 1 to maximum - i - 1 do
 872       let x = i + k and y = k in
 873       let name_left = names_array.(x) and
 874           name_right = names_array.(y) in
 875         th := gen_next_le_thm (!th);
 876         Hashtbl.add th_le_table (name_left ^ name_right) !th
 877     done;
 878 done;;
 879
 880
 881 (* Conversions *)
 882
 883 let rec raw_lt_hash_conv tm =
 884   let ltm, rtm = dest_comb tm in
 885   let ltm = rand ltm in
 886     if is_const rtm then
 887       (* n < _0 <=> F *)
 888       INST[ltm, n_var_num] LT_n_0
 889     else
 890       if is_const ltm then
 891         (* _0 < Bi(n) *)
 892         let bn_tm, n_tm = dest_comb rtm in
 893         let cbn = (fst o dest_const) bn_tm in
 894         let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_lt0_table cbn) in
 895           if cbn = b0_name then
 896             let th1 = raw_lt_hash_conv (rand (concl th0)) in
 897               TRANS th0 th1
 898           else
 899             th0
 900       else
 901         (* Bi(n) < Bj(m) *)
 902         let bm_tm, m_tm = dest_comb ltm in
 903         let bn_tm, n_tm = dest_comb rtm in
 904         let cbm = (fst o dest_const) bm_tm in
 905         let cbn = (fst o dest_const) bn_tm in
 906         let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_lt_table (cbm^cbn)) in
 907         let op = (fst o dest_const o rator o rator o rand o concl) th0 in
 908         let th1 =
 909           if op = "<" then
 910             raw_lt_hash_conv (rand (concl th0))
 911           else
 912             raw_le_hash_conv (rand (concl th0)) in
 913           TRANS th0 th1 and
 914
 915     raw_le_hash_conv tm =
 916   let ltm, rtm = dest_comb tm in
 917   let ltm = rand ltm in
 918     if is_const ltm then
 919       (* _0 <= n <=> T *)
 920       INST[rtm, n_var_num] LE_0_n
 921     else
 922       if is_const rtm then
 923         (* Bi(n) <= _0 *)
 924         let bn_tm, n_tm = dest_comb ltm in
 925         let cbn = (fst o dest_const) bn_tm in
 926         let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_le0_table cbn) in
 927           if cbn = b0_name then
 928             let th1 = raw_le_hash_conv (rand (concl th0)) in
 929               TRANS th0 th1
 930           else
 931             th0
 932       else
 933         (* Bi(n) <= Bj(m) *)
 934         let bm_tm, m_tm = dest_comb ltm in
 935         let bn_tm, n_tm = dest_comb rtm in
 936         let cbm = (fst o dest_const) bm_tm in
 937         let cbn = (fst o dest_const) bn_tm in
 938         let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_le_table (cbm^cbn)) in
 939         let op = (fst o dest_const o rator o rator o rand o concl) th0 in
 940         let th1 =
 941           if op = "<" then
 942             raw_lt_hash_conv (rand (concl th0))
 943           else
 944             raw_le_hash_conv (rand (concl th0)) in
 945           TRANS th0 th1;;
 946
 947
 948
 949 let NUM_LT_HASH_CONV tm =
 950   let atm, rtm = dest_comb tm in
 951   let ltm = rand atm in
 952   let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LT_NUM in
 953   let rtm = rand(concl th) in
 954     TRANS th (raw_lt_hash_conv rtm);;
 955
 956
 957
 958 let NUM_LE_HASH_CONV tm =
 959   let atm, rtm = dest_comb tm in
 960   let ltm = rand atm in
 961   let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LE_NUM in
 962   let rtm = rand(concl th) in
 963     TRANS th (raw_le_hash_conv rtm);;
 964
 965
 966
 967 (*
 968 let x = num_of_string "3543593547359325353535";;
 969 let y = num_of_string "9392392983247294924242";;
 970
 971 let xx = mk_binop lt_op_num (mk_numeral_array x) (mk_numeral_array y);;
 972 let yy = mk_binop lt_op_num (mk_numeral x) (mk_numeral y);;
 973
 974
 975 (* 2.38 *)
 976 test 1000 NUM_LT_CONV yy;;
 977 (* 10: 1.248 *)
 978 test 10000 NUM_LT_HASH_CONV xx;;
 979 *)
 980
 981
 982
 983
 984 (**************************************)
 985
 986 (* ADD_CONV *)
 987
 988
 989 (* ADD theorems *)
 990
 991 let ADD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
 992   (`NUMERAL m + NUMERAL n = NUMERAL (m + n)`, REWRITE_TAC[NUMERAL]);;
 993
 994
 995 let CADD_0_n = prove(`SUC (_0 + n) = SUC n`, REWRITE_TAC[ADD_0_n]);;
 996 let CADD_n_0 = prove(`SUC (n + _0) = SUC n`, REWRITE_TAC[ADD_n_0]);;
 997
 998 (* B0 (SUC n) = B0 n + maximum *)
 999 let B0_SUC = prove(mk_eq(mk_comb(b0_const, mk_comb(suc_const, n_var_num)),
1000                          mk_binop plus_op_num max_const (mk_comb(b0_const, n_var_num))),
1001                    REWRITE_TAC [B0_EXPLICIT] THEN ARITH_TAC);;
1002
1003 let B0_ADD = prove(mk_eq(mk_binop plus_op_num (mk_comb(b0_const, m_var_num)) (mk_comb(b0_const, n_var_num)),
1004                          mk_comb(b0_const, mk_binop plus_op_num m_var_num n_var_num)),
1005                    REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
1006
1007 let SUC_ADD_RIGHT = prove(`SUC(m + n) = m + SUC n`, ARITH_TAC);;
1008
1009
1010 (* Generate all theorems iteratively *)
1011
1012 let th_add_right_next th =
1013   let lhs, rhs = dest_eq(concl th) in
1014   let ltm, rtm = dest_comb rhs in
1015   let cn = fst(dest_const ltm) in
1016   let suc_th = AP_TERM suc_const th in
1017   let th_rhs = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1018   let ltm, rarg = dest_comb lhs in
1019   let larg = rand ltm in
1020   let th1 = INST[larg, m_var_num; rarg, n_var_num] SUC_ADD_RIGHT in
1021   let cn = fst(dest_const(rator rarg)) in
1022   let th2 = Hashtbl.find th_suc_table cn in
1023   let th_lhs = TRANS th1 (AP_TERM ltm th2) in
1024     TRANS (TRANS (SYM th_lhs) suc_th) th_rhs;;
1025
1026
1027 let th_add_array = Array.make (maximum * maximum) (REFL zero_const);;
1028
1029 for i = 0 to maximum - 1 do
1030   let th0 =
1031     if i = 0 then
1032       B0_ADD
1033     else
1034       INST[n_var_num, m_var_num; m_var_num, n_var_num]
1035         (ONCE_REWRITE_RULE[ADD_AC] th_add_array.(i)) in
1036   let _ = th_add_array.(i * maximum) <- th0 in
1037
1038     for j = 1 to maximum - 1 do
1039       th_add_array.(i * maximum + j) <- th_add_right_next th_add_array.(i * maximum + j - 1)
1040     done;
1041 done;;
1042
1043
1044 (* SUC (B_i(m) + B_j(n)) = B_p(...) *)
1045 let th_cadd i j =
1046   let add_th = th_add_array.(i * maximum + j) in
1047   let th0 = AP_TERM suc_const add_th in
1048   let ltm, rtm = dest_comb(rand(concl th0)) in
1049   let ltm, rtm = dest_comb rtm in
1050   let cn = fst(dest_const ltm) in
1051   let suc_th = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in
1052     TRANS th0 suc_th;;
1053
1054
1055 let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);;
1056
1057 for i = 0 to maximum - 1 do
1058   for j = 0 to maximum - 1 do
1059     th_cadd_array.(i * maximum + j) <- th_cadd i j
1060   done;
1061 done;;
1062
1063
1064
1065 let th_add_table = Hashtbl.create (maximum * maximum);;
1066
1067 for i = 0 to maximum - 1 do
1068   for j = 0 to maximum - 1 do
1069     let name = names_array.(i) ^ names_array.(j) in
1070     let th = th_add_array.(i * maximum + j) in
1071     let cflag = (i + j >= maximum) in
1072       Hashtbl.add th_add_table name (th, cflag)
1073   done;
1074 done;;
1075
1076
1077
1078 let th_cadd_table = Hashtbl.create (maximum * maximum);;
1079
1080 for i = 0 to maximum - 1 do
1081   for j = 0 to maximum - 1 do
1082     let name = names_array.(i) ^ names_array.(j) in
1083     let th = th_cadd_array.(i * maximum + j) in
1084     let cflag = (i + j + 1 >= maximum) in
1085       Hashtbl.add th_cadd_table name (th, cflag)
1086   done;
1087 done;;
1088
1089
1090
1091 (* ADD conversion *)
1092
1093
1094 let rec raw_add_conv_hash tm =
1095   let atm,rtm = dest_comb tm in
1096   let ltm = rand atm in
1097     if ltm = zero_const then
1098       INST [rtm,n_var_num] ADD_0_n
1099     else if rtm = zero_const then
1100       INST [ltm,n_var_num] ADD_n_0
1101     else
1102       let lbit,larg = dest_comb ltm
1103       and rbit,rarg = dest_comb rtm in
1104       let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1105       let th0, cflag = Hashtbl.find th_add_table name in
1106       let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1107       let ltm, rtm = dest_comb(rand(concl th)) in
1108         if cflag then
1109           TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1110         else
1111           TRANS th (AP_TERM ltm (raw_add_conv_hash rtm))
1112 and raw_adc_conv_hash tm =
1113   let atm,rtm = dest_comb (rand tm) in
1114   let ltm = rand atm in
1115     if ltm = zero_const then
1116       let th = INST [rtm,n_var_num] CADD_0_n in
1117         TRANS th (raw_suc_conv_hash (rand(concl th)))
1118     else if rtm = zero_const then
1119       let th = INST [ltm,n_var_num] CADD_n_0 in
1120         TRANS th (raw_suc_conv_hash (rand(concl th)))
1121     else
1122       let lbit,larg = dest_comb ltm
1123       and rbit,rarg = dest_comb rtm in
1124       let name = fst(dest_const lbit) ^ fst(dest_const rbit) in
1125       let th0, cflag = Hashtbl.find th_cadd_table name in
1126       let th = INST [larg, m_var_num; rarg, n_var_num] th0 in
1127       let ltm, rtm = dest_comb(rand(concl th)) in
1128         if cflag then
1129           TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm))
1130         else
1131           TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1132
1133
1134 let NUM_ADD_HASH_CONV tm =
1135   let atm, rtm = dest_comb tm in
1136   let ltm = rand atm in
1137   let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] ADD_NUM in
1138   let ltm, rtm = dest_comb(rand(concl th)) in
1139     TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));;
1140
1141
1142 (*
1143 let x = num_of_string "3543593547359325353535";;
1144 let y = num_of_string "9392392983247294924242";;
1145
1146 let xx = mk_binop plus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1147 let yy = mk_binop plus_op_num (mk_numeral x) (mk_numeral y);;
1148
1149 NUM_ADD_HASH_CONV xx;;
1150
1151 test 10000 NUM_ADD_CONV yy;; (* 5.672 *)
1152 (* 10: 1.672 *)
1153 test 10000 NUM_ADD_HASH_CONV xx;;
1154 *)
1155
1156 (********************************)
1157
1158 (* Subtraction *)
1159
1160 let SUB_NUM = prove(mk_eq(mk_binop minus_op_num (mk_comb (num_const, m_var_num)) (mk_comb (num_const, n_var_num)),
1161                           mk_comb(num_const, mk_binop minus_op_num m_var_num n_var_num)),
1162                     REWRITE_TAC[num_def; NUMERAL]);;
1163
1164 let SUB_lemma1 = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> m - n = t:num`;;
1165 let SUB_lemma2 = (UNDISCH_ALL o REWRITE_RULE[NUMERAL] o ARITH_RULE) `m + t = n ==> m - n = 0`;;
1166 let LE_lemma = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> n <= m:num`;;
1167
1168
1169 let raw_sub_hash_conv tm =
1170   let ltm, n_tm = dest_comb tm in
1171   let m_tm = rand ltm in
1172   let m = raw_dest_hash m_tm in
1173   let n = raw_dest_hash n_tm in
1174   let t = m -/ n in
1175     if t >=/ num_0 then
1176       let t_tm = rand (mk_numeral_array t) in
1177       let th0 = INST[n_tm, n_var_num; t_tm, t_var_num; m_tm, m_var_num] SUB_lemma1 in
1178       let th_add = raw_add_conv_hash (mk_binop plus_op_num n_tm t_tm) in
1179         MY_PROVE_HYP th_add th0
1180     else
1181       let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1182       let th0 = INST[m_tm, m_var_num; t_tm, t_var_num; n_tm, n_var_num] SUB_lemma2 in
1183       let th_add = raw_add_conv_hash (mk_binop plus_op_num m_tm t_tm) in
1184         MY_PROVE_HYP th_add th0;;
1185
1186
1187
1188 (* Returns either (tm1 - tm2, tm2 <= tm1) or (tm2 - tm1, tm1 <= tm2) *)
1189 let raw_sub_and_le_hash_conv tm1 tm2 =
1190   let m = raw_dest_hash tm1 in
1191   let n = raw_dest_hash tm2 in
1192   let t = m -/ n in
1193     if t >=/ num_0 then
1194       let t_tm = rand (mk_numeral_array t) in
1195       let inst = INST[tm2, n_var_num; t_tm, t_var_num; tm1, m_var_num] in
1196       let th_sub = inst SUB_lemma1 in
1197       let th_le = inst LE_lemma in
1198       let th_add = raw_add_conv_hash (mk_binop plus_op_num tm2 t_tm) in
1199         (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le)
1200     else
1201       let t_tm = rand (mk_numeral_array (Num.abs_num t)) in
1202       let inst = INST[tm2, m_var_num; t_tm, t_var_num; tm1, n_var_num] in
1203       let th_sub = inst SUB_lemma1 in
1204       let th_le = inst LE_lemma in
1205       let th_add = raw_add_conv_hash (mk_binop plus_op_num tm1 t_tm) in
1206         (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le);;
1207
1208
1209
1210 let NUM_SUB_HASH_CONV tm =
1211   let atm, rtm = dest_comb tm in
1212   let ltm = rand atm in
1213   let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] SUB_NUM in
1214   let ltm, rtm = dest_comb(rand(concl th)) in
1215     TRANS th (AP_TERM ltm (raw_sub_hash_conv rtm));;
1216
1217
1218 (*
1219 let y = num_of_string "3543593547359325353535";;
1220 let x = num_of_string "9392392983247294924242";;
1221
1222 let xx = mk_binop minus_op_num (mk_numeral_array x) (mk_numeral_array y);;
1223 let yy = mk_binop minus_op_num (mk_numeral x) (mk_numeral y);;
1224
1225 NUM_SUB_HASH_CONV xx;;
1226
1227 test 1000 NUM_SUB_CONV yy;; (* 2.376 *)
1228 (* 10: 0.872 *)
1229 test 1000 NUM_SUB_HASH_CONV xx;;
1230 *)
1231
1232
1233
1234 (********************************)
1235
1236 (* Multiplication *)
1237
1238 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)),
1239                           mk_comb(num_const, mk_binop mul_op_num m_var_num n_var_num)),
1240                     REWRITE_TAC[num_def; NUMERAL]);;
1241
1242 let MUL_0_n = prove(`_0 * n = _0`, ONCE_REWRITE_TAC[GSYM NUM_THM] THEN
1243                       ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN REWRITE_TAC[num_def] THEN
1244                       REWRITE_TAC[MULT_CLAUSES]);;
1245
1246 let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;;
1247
1248 let MUL_1_n, MUL_n_1 =
1249   let one_const = mk_comb (const_array.(1), zero) in
1250   let cond = mk_eq(mk_binop mul_op_num one_const n_var_num, n_var_num) in
1251   let th = (REWRITE_RULE[NUMERAL] o prove)(cond, REWRITE_TAC[def_array.(1)] THEN ARITH_TAC) in
1252     th, ONCE_REWRITE_RULE[MULT_AC] th;;
1253
1254
1255
1256 let MUL_B0_t = prove(mk_eq(mk_binop mul_op_num (mk_comb(b0_const, n_var_num)) t_var_num,
1257                            mk_comb(b0_const, mk_binop mul_op_num n_var_num t_var_num)),
1258                      REWRITE_TAC[def_array.(0)] THEN ARITH_TAC);;
1259
1260
1261 let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
1262
1263
1264 let MUL_SUC_RIGHT = prove(`m * SUC(n) = m * n + m`, ARITH_TAC);;
1265
1266
1267 (* Multiplication table *)
1268
1269 let mul_th_next_right th =
1270   let ltm, rtm = dest_comb(rand(rator(concl th))) in
1271   let mtm = rand ltm in
1272   let th0 = INST[mtm, m_var_num; rtm, n_var_num] MUL_SUC_RIGHT in
1273   let th1 = AP_THM (AP_TERM plus_op_num th) mtm in
1274   let sum_th = raw_add_conv_hash (rand(concl th1)) in
1275   let th2 = TRANS (TRANS th0 th1) sum_th in
1276   let cn = fst(dest_const (rator rtm)) in
1277   let th_suc = INST[zero_const, n_var_num] (Hashtbl.find th_suc_table cn) in
1278   let th3 = AP_TERM (mk_comb (mul_op_num, mtm)) th_suc in
1279     TRANS (SYM th3) th2;;
1280
1281
1282 let mul_array = Array.make (maximum * maximum) (REFL zero_const);;
1283 for i = 1 to maximum - 1 do
1284   let th1 = INST[mk_comb(const_array.(i), zero_const), n_var_num] MUL_n_1 in
1285   let _ = mul_array.(i * maximum + 1) <- th1 in
1286
1287     for j = 2 to maximum - 1 do
1288       mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1)
1289     done;
1290 done;;
1291
1292
1293
1294 let mul_table = Hashtbl.create (maximum * maximum);;
1295 for i = 1 to maximum - 1 do
1296   for j = 1 to maximum - 1 do
1297     Hashtbl.add mul_table (names_array.(i) ^ names_array.(j)) mul_array.(i * maximum + j)
1298   done;
1299 done;;
1300
1301
1302 (* General multiplication theorem *)
1303
1304 let prod_lemma =
1305   let mul (a,b) = mk_binop mul_op_num a b and
1306       add (a,b) = mk_binop plus_op_num a b in
1307   let lhs = mul(add(t_var_num, mk_comb(b0_const, m_var_num)),
1308                 add(r_var_num, mk_comb(b0_const, n_var_num))) in
1309   let rhs = add(mul(t_var_num, r_var_num),
1310                 mk_comb(b0_const, add(mk_comb(b0_const, mul(m_var_num, n_var_num)),
1311                                       add(mul(m_var_num, r_var_num),
1312                                           mul(n_var_num, t_var_num))))) in
1313     prove(mk_eq(lhs, rhs),
1314           REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1315             REWRITE_TAC[MUL_B0_t; MUL_t_B0] THEN
1316             ONCE_REWRITE_TAC[GSYM ADD_ASSOC] THEN
1317             REWRITE_TAC[th_add_array.(0)] THEN
1318             REWRITE_TAC[ADD_AC; MULT_AC]);;
1319
1320 let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;;
1321
1322 let dest_op tm =
1323   let ltm, rtm = dest_comb tm in
1324     rand ltm, rtm;;
1325
1326
1327 (* B_i(m) * B_j(n) = B_p(B_q(m * n) + m * B_j(0) + n * B_i(0))
1328    where B_p(B_q(0)) = i * j *)
1329 let gen_mul_thm i j =
1330   let bi0 = mk_comb(const_array.(i), zero_const) and
1331       bj0 = mk_comb(const_array.(j), zero_const) in
1332   let def_i = INST[m_var_num, n_var_num] def_thm_array.(i) in
1333   let def_j = def_thm_array.(j) in
1334   let th0 = MK_COMB(AP_TERM mul_op_num def_i, def_j) in
1335   let th1 = TRANS th0 (INST[bi0, t_var_num; bj0, r_var_num] prod_lemma) in
1336   let mul_th = mul_array.(i * maximum + j) in
1337   let larg, rarg = dest_op (rand (concl th1)) in
1338   let th2 = TRANS th1 (AP_THM (AP_TERM plus_op_num mul_th) rarg) in
1339   let larg = rand(concl mul_th) in
1340   let b_low, b_high = dest_comb larg in
1341   let rtm = rand(rarg) in
1342   let th_add = INST[b_high, m_var_num; rtm, n_var_num]
1343     (fst(Hashtbl.find th_add_table (fst(dest_const b_low)^b0_name))) in
1344     if i * j < maximum then
1345       let ltm, rtm = dest_op(rand(rand(concl th_add))) in
1346       let add_0 = AP_TERM b_low (INST[rtm, n_var_num] ADD_0_n) in
1347         TRANS th2 (TRANS th_add add_0)
1348     else
1349       let larg, rtm = dest_op (rand(rand(concl th_add))) in
1350       let rarg, rtm = dest_op rtm in
1351       let th_assoc = INST[larg, m_var_num; rarg, n_var_num; rtm, p_var_num] ADD_ASSOC' in
1352       let mn = rand(rarg) in
1353       let b_high = rator b_high in
1354       let th_add2' = INST[zero_const, m_var_num; mn, n_var_num]
1355         (fst(Hashtbl.find th_add_table (fst(dest_const b_high)^b0_name))) in
1356       let add_0 = AP_TERM b_high (INST[mn, n_var_num] ADD_0_n) in
1357       let th_add2 = TRANS th_add2' add_0 in
1358       let th3 = TRANS th_assoc (AP_THM (AP_TERM plus_op_num th_add2) rtm) in
1359       let th4 = TRANS th_add (AP_TERM b_low th3) in
1360         TRANS th2 th4;;
1361
1362
1363 let gen_mul_table = Hashtbl.create (maximum * maximum);;
1364
1365 for i = 1 to maximum - 1 do
1366   for j = 1 to maximum - 1 do
1367     let name = names_array.(i) ^ names_array.(j) in
1368       Hashtbl.add gen_mul_table name (gen_mul_thm i j)
1369   done;
1370 done;;
1371
1372
1373 (* B_i(m) * B_j(0) = B_p(B_q(0) + m * B_j(0))
1374    where i * j = B_p(B_q(0)) *)
1375 let mul1_right_th i j =
1376   let th0 = INST[zero_const, n_var_num]
1377     (Hashtbl.find gen_mul_table (names_array.(i)^names_array.(j))) in
1378   let b_low, rtm = dest_comb(rand(concl th0)) in
1379   let tm1, tm23 = dest_op rtm in
1380   let tm2p, tm3 = dest_comb tm23 in
1381   let tm3_th = INST[rand tm3, n_var_num] MUL_0_n in
1382   let tm2_th = INST[rand(tm2p), n_var_num] ADD_n_0 in
1383   let tm23_th = TRANS (AP_TERM tm2p tm3_th) tm2_th in
1384   let ltm, rtm = dest_comb tm1 in
1385     if (i * j < maximum) then
1386       let tm1_th = TRANS (AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0)) B0_0 in
1387       let tm123_th' = TRANS (INST[tm23, n_var_num] ADD_0_n) tm23_th in
1388       let tm123_th = TRANS (AP_THM (AP_TERM plus_op_num tm1_th) tm23) tm123_th' in
1389         TRANS th0 (AP_TERM b_low tm123_th)
1390     else
1391       let tm1_th = AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0) in
1392       let tm123_th = MK_COMB(AP_TERM plus_op_num tm1_th, tm23_th) in
1393         TRANS th0 (AP_TERM b_low tm123_th);;
1394
1395
1396 (* B_j(0) * B_i(m) = B_p(B_q(0) + B_j(0) * B_i(m) *)
1397
1398 let MULT_AC' = CONJUNCT1 MULT_AC;;
1399
1400 let mul1_left_th th =
1401   let lhs, rhs = dest_eq(concl th) in
1402   let ltm, rtm = dest_op lhs in
1403   let th_lhs = INST[ltm, n_var_num; rtm, m_var_num] MULT_AC' in
1404   let btm, rtm = dest_comb rhs in
1405   let larg, rarg = dest_op rtm in
1406     if (is_comb larg) then
1407       let ltm, rtm = dest_op rarg in
1408       let th_rhs' = INST[ltm, m_var_num; rtm, n_var_num] MULT_AC' in
1409       let th_rhs = AP_TERM (mk_comb(plus_op_num, larg)) th_rhs' in
1410         TRANS th_lhs (TRANS th (AP_TERM btm th_rhs))
1411     else
1412       let th_rhs = INST[larg, m_var_num; rarg, n_var_num] MULT_AC' in
1413         TRANS th_lhs (TRANS th (AP_TERM btm th_rhs));;
1414
1415
1416
1417
1418 let mul1_right_th_table = Hashtbl.create (maximum * maximum);;
1419 let mul1_left_th_table = Hashtbl.create (maximum * maximum);;
1420
1421 for i = 1 to maximum - 1 do
1422   for j = 1 to maximum - 1 do
1423     let name_right = names_array.(i) ^ names_array.(j) in
1424     let name_left = names_array.(j) ^ names_array.(i) in
1425     let th = mul1_right_th i j in
1426     let add_flag = (i * j >= maximum) in
1427     let _ = Hashtbl.add mul1_right_th_table name_right (add_flag, th) in
1428       Hashtbl.add mul1_left_th_table name_left (add_flag, mul1_left_th th)
1429   done;
1430 done;;
1431
1432
1433
1434 (******************************************************)
1435
1436 (* Conversions *)
1437
1438
1439 (* Multiplies arg and (tm = tmname(_0)) *)
1440 let rec raw_mul1_right_hash arg tm tmname =
1441   if arg = zero_const then
1442     INST [tm, n_var_num] MUL_0_n
1443   else
1444     let btm, mtm = dest_comb arg in
1445     let cn = fst(dest_const btm) in
1446       if (cn = b0_name) then
1447         let th = INST[mtm, n_var_num; tm, t_var_num] MUL_B0_t in
1448           TRANS th (AP_TERM b0_const (raw_mul1_right_hash mtm tm tmname))
1449       else
1450         let name = cn ^ tmname in
1451           if (mtm = zero_const) then
1452             Hashtbl.find mul_table name
1453           else
1454             let add_flag, th' = Hashtbl.find mul1_right_th_table name in
1455             let th = INST[mtm, m_var_num] th' in
1456               if add_flag then
1457                 let ltm, rtm = dest_comb(rand(concl th)) in
1458                 let lplus, rarg = dest_comb rtm in
1459                 let th2 = AP_TERM lplus (raw_mul1_right_hash mtm tm tmname) in
1460                 let th_add = raw_add_conv_hash (rand(concl th2)) in
1461                   TRANS th (AP_TERM ltm (TRANS th2 th_add))
1462               else
1463                 let ltm = rator(rand(concl th)) in
1464                 let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in
1465                   TRANS th th2;;
1466
1467
1468 (* Multiplies (tm = tmname(_0)) and arg *)
1469 let rec raw_mul1_left_hash tm tmname arg =
1470   if arg = zero_const then
1471     INST [tm, n_var_num] MUL_n_0
1472   else
1473     let btm, mtm = dest_comb arg in
1474     let cn = fst(dest_const btm) in
1475       if (cn = b0_name) then
1476         let th = INST[mtm, n_var_num; tm, t_var_num] MUL_t_B0 in
1477           TRANS th (AP_TERM b0_const (raw_mul1_left_hash tm tmname mtm))
1478       else
1479         let name = tmname ^ cn in
1480           if (mtm = zero_const) then
1481             Hashtbl.find mul_table name
1482           else
1483             let add_flag, th' = Hashtbl.find mul1_left_th_table name in
1484             let th = INST[mtm, m_var_num] th' in
1485               if add_flag then
1486                 let ltm, rtm = dest_comb(rand(concl th)) in
1487                 let lplus, rarg = dest_comb rtm in
1488                 let th2 = AP_TERM lplus (raw_mul1_left_hash tm tmname mtm) in
1489                 let th_add = raw_add_conv_hash (rand(concl th2)) in
1490                   TRANS th (AP_TERM ltm (TRANS th2 th_add))
1491               else
1492                 let ltm = rator(rand(concl th)) in
1493                 let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in
1494                   TRANS th th2;;
1495
1496
1497 (* Computes B_i(m) * B_j(n) *)
1498 let rec raw_mul_conv_hash tm =
1499   let larg, rarg = dest_comb tm in
1500   let larg = rand larg in
1501     if larg = zero_const then
1502       INST [rarg, n_var_num] MUL_0_n
1503     else if rarg = zero_const then
1504       INST [larg, n_var_num] MUL_n_0
1505     else
1506
1507       let lbtm, mtm = dest_comb larg in
1508       let lcn = fst(dest_const lbtm) in
1509         if (lcn = b0_name) then
1510           let th = INST[rarg, t_var_num; mtm, n_var_num] MUL_B0_t in
1511           let ltm, rtm = dest_comb(rand(concl th)) in
1512             TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1513         else
1514           let rbtm, ntm = dest_comb rarg in
1515           let rcn = fst(dest_const rbtm) in
1516             if (rcn = b0_name) then
1517               let th = INST[larg, t_var_num; ntm, n_var_num] MUL_t_B0 in
1518               let ltm, rtm = dest_comb(rand(concl th)) in
1519                 TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm))
1520             else
1521
1522               if (ntm = zero_const) then
1523                 if (mtm = zero_const) then
1524                   Hashtbl.find mul_table (lcn ^ rcn)
1525                 else
1526                   raw_mul1_right_hash larg (mk_comb(rbtm, zero_const)) rcn
1527               else if (mtm = zero_const) then
1528                 raw_mul1_left_hash (mk_comb(lbtm, zero_const)) lcn rarg
1529               else
1530
1531                 let th0 = INST[mtm, m_var_num; ntm, n_var_num]
1532                   (Hashtbl.find gen_mul_table (lcn ^ rcn)) in
1533                 let b_low, expr = dest_comb(rand(concl th0)) in
1534                 let ltm, rsum = dest_comb expr in
1535                 let b_high, mul0 = dest_comb (rand ltm) in
1536                 let th_mul0 = raw_mul_conv_hash mul0 in
1537                 let th_mul1 = raw_mul1_right_hash mtm (mk_comb(rbtm, zero_const)) rcn in
1538                 let th_mul2 = raw_mul1_right_hash ntm (mk_comb(lbtm, zero_const)) lcn in
1539                 let th_larg = AP_TERM plus_op_num (AP_TERM b_high th_mul0) in
1540                 let th_rarg = MK_COMB(AP_TERM plus_op_num th_mul1, th_mul2) in
1541
1542                 let add_rarg = TRANS th_rarg (raw_add_conv_hash (rand(concl th_rarg))) in
1543                 let add_th = MK_COMB (th_larg, add_rarg) in
1544                 let add = TRANS add_th (raw_add_conv_hash (rand(concl add_th))) in
1545
1546                   TRANS th0 (AP_TERM b_low add);;
1547
1548
1549
1550 (* The main multiplication conversion *)
1551 let NUM_MULT_HASH_CONV tm =
1552   let ltm, rtm = dest_comb tm in
1553   let larg, rarg = rand (rand ltm), rand rtm in
1554   let th0 = INST[larg, m_var_num; rarg, n_var_num] MUL_NUM in
1555     if (rand(rator(concl th0)) <> tm) then
1556       failwith "NUM_MULT_HASH_CONV"
1557     else
1558       let rtm = rand(rand(concl th0)) in
1559       let th = raw_mul_conv_hash rtm in
1560         TRANS th0 (AP_TERM num_const th);;
1561
1562
1563
1564 (**************************)
1565
1566 (* Tests *)
1567
1568 (*
1569 let x = Int 325325353;;
1570 let y = Int 999434312;;
1571
1572 let xx = mk_binop mul_op_num (mk_numeral_array x) (mk_numeral_array y);;
1573 let yy = mk_binop mul_op_num (mk_numeral x) (mk_numeral y);;
1574 let zz = rand(concl(REWRITE_CONV[NUM_THM] xx));;
1575
1576 NUM_MULT_HASH_CONV xx;;
1577
1578 test 1000 NUM_MULT_CONV yy;; (* 4.12 *)
1579 (* 10: 1.896 *)
1580 test 1000 NUM_MULT_HASH_CONV xx;; (* 4: 1.69; 6: 0.716(1), 0.608(2), 8: 0.328(3) *)
1581 (* 10: 1.864 *)
1582 test 1000 raw_mul_conv_hash zz;; (* 4: 2.45(1), 1.576(2), 8: 0.320 *)
1583
1584
1585 needs "example0.hl";;
1586
1587 let x = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral t1) (mk_numeral t2)) example;;
1588 let h1 = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral_array t1) (mk_numeral_array t2)) example;;
1589 let h2 = map (fun t1, t2 -> mk_binop mul_op_num
1590                (rand (mk_numeral_array t1))
1591                (rand (mk_numeral_array t2))) example;;
1592
1593
1594 test 1 (map NUM_MULT_CONV) x;; (* 2.64 *)
1595 test 10 (map NUM_MULT_HASH_CONV) h1;; (* 4: 5.43; 6: 3.12; 8: 1.67 *)
1596 test 10 (map raw_mul_conv_hash) h2;; (* 5.42; 8: 1.576 *)
1597 *)
1598
1599
1600
1601 (************************************)
1602
1603 (* DIV *)
1604
1605
1606 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)),
1607                           mk_comb(num_const, mk_binop div_op_num m_var_num n_var_num)),
1608                     REWRITE_TAC[num_def; NUMERAL]);;
1609
1610
1611 let DIV_UNIQ' = (UNDISCH_ALL o
1612                    PURE_ONCE_REWRITE_RULE[ARITH_RULE `a < b <=> (a < b:num <=> T)`] o
1613                    ONCE_REWRITE_RULE[ARITH_RULE `m = q * n + r <=> q * n + r = m:num`] o
1614                    REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL) DIV_UNIQ;;
1615
1616 (* Computes m DIV n *)
1617 let raw_div_hash_conv tm =
1618   let ltm, n_tm = dest_comb tm in
1619   let m_tm = rand ltm in
1620   let m = raw_dest_hash m_tm in
1621   let n = raw_dest_hash n_tm in
1622   let q = Num.quo_num m n and
1623       r = Num.mod_num m n in
1624   let q_tm = rand (mk_numeral_array q) and
1625       r_tm = rand (mk_numeral_array r) in
1626
1627   let qn_th = raw_mul_conv_hash (mk_binop mul_op_num q_tm n_tm) in
1628   let qn_tm = rand (concl qn_th) in
1629   let qnr_th = raw_add_conv_hash (mk_binop plus_op_num qn_tm r_tm) in
1630   let th1 = TRANS (AP_THM (AP_TERM plus_op_num qn_th) r_tm) qnr_th in
1631   let th2 = raw_lt_hash_conv (mk_binop lt_op_num r_tm n_tm) in
1632   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
1633     MY_PROVE_HYP th1 (MY_PROVE_HYP th2 th0);;
1634
1635
1636
1637 (* The main division conversion *)
1638 let NUM_DIV_HASH_CONV tm =
1639   let ltm, rtm = dest_comb tm in
1640   let larg, rarg = rand (rand ltm), rand rtm in
1641   let th0 = INST[larg, m_var_num; rarg, n_var_num] DIV_NUM in
1642     if (rand(rator(concl th0)) <> tm) then
1643       failwith "NUM_DIV_HASH_CONV"
1644     else
1645       let rtm = rand(rand(concl th0)) in
1646       let th = raw_div_hash_conv rtm in
1647         TRANS th0 (AP_TERM num_const th);;
1648
1649
1650 (*
1651 let y = num_of_string "3543593547359";;
1652 let x = num_of_string "9392392983247294924242";;
1653
1654
1655 let xx = mk_binop div_op_num (mk_numeral_array x) (mk_numeral_array y);;
1656 let yy = mk_binop div_op_num (mk_numeral x) (mk_numeral y);;
1657
1658 (* 1.844 *)
1659 test 100 NUM_DIV_CONV yy;;
1660 (* 10: 0.428 *)
1661 test 100 NUM_DIV_HASH_CONV xx;;
1662 *)
1663
1664
1665
1666 (*********************************************)
1667
1668 (* EVEN_CONV, ODD_CONV *)
1669
1670 let even_const = `EVEN` and
1671     odd_const = `ODD` and
1672     eq_const = `<=>` and
1673     f_const = `F` and
1674     t_const = `T`;;
1675
1676
1677
1678 let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1679   (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);;
1680
1681 let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove)
1682   (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
1683
1684 let EVEN_ZERO = prove(`EVEN _0 <=> T`, REWRITE_TAC[ARITH_EVEN]);;
1685 let ODD_ZERO = prove(`ODD _0 <=> F`, REWRITE_TAC[ARITH_ODD]);;
1686
1687
1688 let EVEN_B0 = prove(mk_eq(mk_comb(`EVEN`, mk_comb(b0_const, `n:num`)), `T`),
1689                     REWRITE_TAC[B0_EXPLICIT; EVEN_MULT] THEN
1690                       DISJ1_TAC THEN CONV_TAC NUM_EVEN_CONV);;
1691
1692
1693 let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
1694                    REWRITE_TAC[NOT_ODD; EVEN_B0]);;
1695
1696 let EVEN_SUC_T = prove(`(EVEN (SUC n) <=> T) <=> (EVEN n <=> F)`, REWRITE_TAC[EVEN]);;
1697 let EVEN_SUC_F = prove(`(EVEN (SUC n) <=> F) <=> (EVEN n <=> T)`, REWRITE_TAC[EVEN]);;
1698
1699 let ODD_SUC_T = prove(`(ODD (SUC n) <=> T) <=> (ODD n <=> F)`, REWRITE_TAC[ODD]);;
1700 let ODD_SUC_F = prove(`(ODD (SUC n) <=> F) <=> (ODD n <=> T)`, REWRITE_TAC[ODD]);;
1701
1702
1703
1704 let next_even_th th =
1705   let ltm, rtm = dest_comb(concl th) in
1706   let b_tm = rand(rand ltm) in
1707   let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1708   let flag = (fst o dest_const) rtm = "T" in
1709   let th0 = SYM (AP_TERM even_const suc_b) in
1710   let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1711   let th2 = INST[b_tm, n_var_num] (if flag then EVEN_SUC_F else EVEN_SUC_T) in
1712     EQ_MP (SYM (TRANS th1 th2)) th;;
1713
1714
1715 let next_odd_th th =
1716   let ltm, rtm = dest_comb(concl th) in
1717   let b_tm = rand(rand ltm) in
1718   let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in
1719   let flag = (fst o dest_const) rtm = "T" in
1720   let th0 = SYM (AP_TERM odd_const suc_b) in
1721   let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in
1722   let th2 = INST[b_tm, n_var_num] (if flag then ODD_SUC_F else ODD_SUC_T) in
1723     EQ_MP (SYM (TRANS th1 th2)) th;;
1724
1725
1726 let even_thm_table = Hashtbl.create maximum;;
1727
1728
1729 Hashtbl.add even_thm_table names_array.(0) EVEN_B0;;
1730
1731
1732 for i = 1 to maximum - 1 do
1733   let th0 = next_even_th (Hashtbl.find even_thm_table names_array.(i - 1)) in
1734     Hashtbl.add even_thm_table names_array.(i) th0
1735 done;;
1736
1737
1738 let odd_thm_table = Hashtbl.create maximum;;
1739
1740 Hashtbl.add odd_thm_table names_array.(0) ODD_B0;;
1741
1742 for i = 1 to maximum - 1 do
1743   let th0 = next_odd_th (Hashtbl.find odd_thm_table names_array.(i - 1)) in
1744     Hashtbl.add odd_thm_table names_array.(i) th0
1745 done;;
1746
1747
1748 let raw_even_hash_conv tm =
1749   let ltm, rtm = dest_comb tm in
1750     if ((fst o dest_const) ltm <> "EVEN") then
1751       failwith "raw_even_hash_conv: no EVEN"
1752     else
1753       if (is_const rtm) then
1754         EVEN_ZERO
1755       else
1756         let b_tm, n_tm = dest_comb rtm in
1757         let th0 = Hashtbl.find even_thm_table ((fst o dest_const) b_tm) in
1758           INST[n_tm, n_var_num] th0;;
1759
1760
1761 let raw_odd_hash_conv tm =
1762   let ltm, rtm = dest_comb tm in
1763     if ((fst o dest_const) ltm <> "ODD") then
1764       failwith "raw_odd_hash_conv: no ODD"
1765     else
1766       if (is_const rtm) then
1767         ODD_ZERO
1768       else
1769         let b_tm, n_tm = dest_comb rtm in
1770         let th0 = Hashtbl.find odd_thm_table ((fst o dest_const) b_tm) in
1771           INST[n_tm, n_var_num] th0;;
1772
1773
1774
1775 let NUM_EVEN_HASH_CONV tm =
1776   let ltm, rtm = dest_comb tm in
1777   let th0 = INST[rand rtm, n_var_num] EVEN_NUM in
1778   let ltm, rtm = dest_comb(concl th0) in
1779     if (rand ltm <> tm) then
1780       failwith "NUM_EVEN_HASH_CONV"
1781     else
1782       let th1 = raw_even_hash_conv rtm in
1783         TRANS th0 th1;;
1784
1785
1786 let NUM_ODD_HASH_CONV tm =
1787   let ltm, rtm = dest_comb tm in
1788   let th0 = INST[rand rtm, n_var_num] ODD_NUM in
1789   let ltm, rtm = dest_comb(concl th0) in
1790     if (rand ltm <> tm) then
1791       failwith "NUM_ODD_HASH_CONV"
1792     else
1793       let th1 = raw_odd_hash_conv rtm in
1794         TRANS th0 th1;;
1795
1796
1797
1798 end;;
1799
1800