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