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