module type Arith_hash_sig =
  sig
    val num_def : thm
    val NUM_THM : thm
    val num_const : term
    val const_array : term array
    val def_array: thm array
    val def_thm_array: thm array
    val mk_numeral_hash : num -> term
    val mk_numeral_array : num -> term
    val mk_small_numeral_array : int -> term
    val raw_dest_hash : term -> num
    val dest_numeral_hash : term -> num
    val NUMERAL_TO_NUM_CONV : term -> thm
    val NUM_TO_NUMERAL_CONV : term -> thm
    val raw_suc_conv_hash : term -> thm
    val NUM_SUC_HASH_CONV : term -> thm
    val raw_eq0_hash_conv : term -> thm
    val NUM_EQ0_HASH_CONV : term -> thm
    val raw_pre_hash_conv : term -> thm
    val NUM_PRE_HASH_CONV : term -> thm
    val raw_gt0_hash_conv : term -> thm
    val NUM_GT0_HASH_CONV : term -> thm
    val raw_lt_hash_conv : term -> thm
    val raw_le_hash_conv : term -> thm
    val NUM_LT_HASH_CONV : term -> thm
    val NUM_LE_HASH_CONV : term -> thm
    val raw_add_conv_hash : term -> thm
    val NUM_ADD_HASH_CONV : term -> thm
    val raw_sub_hash_conv : term -> thm
    val raw_sub_and_le_hash_conv : term -> term -> thm * thm
    val NUM_SUB_HASH_CONV : term -> thm
    val raw_mul_conv_hash : term -> thm
    val NUM_MULT_HASH_CONV : term -> thm
    val raw_div_hash_conv : term -> thm
    val NUM_DIV_HASH_CONV : term -> thm

    val raw_even_hash_conv : term -> thm
    val raw_odd_hash_conv : term -> thm
    val NUM_EVEN_HASH_CONV : term -> thm
    val NUM_ODD_HASH_CONV : term -> thm
end;;

(* Dependencies *)
needs "../formal_lp/arith/misc.hl";;
needs "../formal_lp/arith/arith_options.hl";;

module Arith_hash : Arith_hash_sig = struct

open Arith_misc;;
open Arith_options;;

let maximum = base;;

(******************)

(* Generate definitions and constants *)

let num_type = `:num`;;
let fnum_type = `:num->num`;;

let numeral_const = `NUMERAL` and
    zero_const = `_0` and
    bit0_const = `BIT0` and
    bit1_const = `BIT1` and
    truth_const = `T` and
    false_const = `F`;;

let m_var_num = `m:num` and
    n_var_num = `n:num` and
    t_var_num = `t:num` and
    r_var_num = `r:num` and
    p_var_num = `p:num` and
    q_var_num = `q:num`;;

let suc_const = `SUC` and
    plus_op_num = `(+):num->num->num` and
    minus_op_num = `(-):num->num->num` and
    mul_op_num = `( * ):num->num->num` and
    div_op_num = `(DIV):num->num->num` and
    le_op_num = `(<=):num->num->bool` and
    lt_op_num = `(<):num->num->bool`;;


let plus_op_real = `(+):real->real->real` and
    mul_op_real = `( * ):real->real->real`;;



let names_array = Array.init maximum (fun i -> "D"^(string_of_int i));;


(* Definitions *)

let num_name = "NUM"^(string_of_int base);;
let num_def = new_basic_definition (mk_eq(mk_var(num_name, fnum_type), numeral_const));;
let num_const = mk_const(num_name, []);;
let num_def_sym = SYM num_def;;
let NUM_THM = prove(mk_eq(mk_comb(num_const, n_var_num), n_var_num),
                    REWRITE_TAC[num_def; NUMERAL]);;
(* B_i(n) = i + B_0(n) *) let mk_bit_definition i = let lhs = mk_var (names_array.(i), fnum_type) in let tm1 = mk_binop mul_op_num (mk_small_numeral base) n_var_num in let tm2 = mk_binop plus_op_num tm1 (mk_small_numeral i) in let rhs = mk_abs (n_var_num, tm2) in new_basic_definition (mk_eq (lhs, rhs));; let def_basic_array = Array.init maximum mk_bit_definition;; let def_array = Array.init maximum (fun i -> let basic = def_basic_array.(i) in let th1 = AP_THM basic n_var_num in TRANS th1 (BETA (rand (concl th1))));; let def_table = Hashtbl.create maximum;; let def_basic_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do let _ = Hashtbl.add def_table names_array.(i) def_array.(i) in Hashtbl.add def_basic_table names_array.(i) def_basic_array.(i) done;; (* Constants *) let const_array = Array.init maximum (fun i -> mk_const(names_array.(i),[]));; let b0_def = def_array.(0);; let b0_const = const_array.(0);; let b0_name = names_array.(0);; let max_const = mk_small_numeral maximum;; (* Alternative definition of B_i *)
let ADD_0_n = 
prove(`_0 + n = n`,
ONCE_REWRITE_TAC[GSYM NUMERAL] THEN REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
let ADD_n_0 = 
prove(`n + _0 = n`,
ONCE_REWRITE_TAC[GSYM NUMERAL] THEN REWRITE_TAC[GSYM ARITH_ADD; ADD_CLAUSES]);;
let MUL_n_0 = 
prove(`n * _0 = 0`,
REWRITE_TAC[NUMERAL] THEN SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN ARITH_TAC);;
(* B_i(n) = i + B_0(n) *) let def_thm i = let bin = mk_comb(const_array.(i), n_var_num) in let bi0 = mk_comb(const_array.(i), zero_const) in let b0n = mk_comb(const_array.(0), n_var_num) in let rhs = mk_binop plus_op_num bi0 b0n in prove(mk_eq(bin, rhs), REWRITE_TAC[def_array.(i); def_array.(0)] THEN REWRITE_TAC[MUL_n_0; ADD_CLAUSES] THEN ARITH_TAC);; let def_thm_array = Array.init maximum def_thm;;
let B0_0 = prove(mk_eq(mk_comb(b0_const, zero_const), zero_const),
                 REWRITE_TAC[b0_def; MUL_n_0; ADD_CLAUSES; NUMERAL]);;
let B0_EXPLICIT = prove(mk_eq(mk_comb(b0_const, n_var_num),
                              mk_binop mul_op_num max_const n_var_num),
                        REWRITE_TAC[b0_def; ADD_CLAUSES]);;
(******************************) (* mk_numeral and dest_numeral *) (* mk_table *) let mk_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do Hashtbl.add mk_table (Int i) const_array.(i) done;; (* mk_numeral *) let max_num = Int maximum;; let mk_numeral_hash = let rec mk_num n = if (n =/ num_0) then zero_const else let m = mod_num n max_num in let bit = Hashtbl.find mk_table m in mk_comb(bit, mk_num(quo_num n max_num)) in fun n -> if n </ num_0 then failwith "mk_numeral_hash: negative argument" else mk_comb(num_const, mk_num n);; let mk_numeral_array = let rec mk_num n = if (n =/ num_0) then zero_const else let m = Num.int_of_num (mod_num n max_num) in let bit = const_array.(m) in mk_comb(bit, mk_num(quo_num n max_num)) in fun n -> if n </ num_0 then failwith "mk_numeral_array: negative argument" else mk_comb(num_const, mk_num n);; let mk_small_numeral_array = let rec mk_num n = if (n = 0) then zero_const else let m = n mod maximum in let bit = const_array.(m) in mk_comb(bit, mk_num(n / maximum)) in fun n -> if n < 0 then failwith "mk_small_numeral_array: negative argument" else mk_comb (num_const, mk_num n);; (* (* 10: 1.232 *) test 10000 mk_numeral_hash (Int 65535);; (* 0.736 *) (* 10: 1.216 *) test 10000 mk_numeral_array (Int 65535);; (* 0.728 *) (* 10: 0.272 *) test 100000 mk_small_numeral_array 65535;; (* 0.216 *) (* 10: 0.316 *) test 1000 mk_numeral_array (num_of_string "9111111111111111");; (* 0.288 *) *) (* dest_table *) let dest_table_num = Hashtbl.create maximum;; for i = 0 to maximum - 1 do Hashtbl.add dest_table_num names_array.(i) (Int i) done;; (* dest_numeral *) let max_num = Int maximum;; let rec raw_dest_hash tm = if tm = zero_const then num_0 else let l, r = dest_comb tm in let n = max_num */ raw_dest_hash r in let cn = fst(dest_const l) in n +/ (Hashtbl.find dest_table_num cn);; let dest_numeral_hash tm = raw_dest_hash (rand tm);; (* (* 10: 0.852 *) test 100000 dest_numeral_hash (mk_numeral_array (Int 11111111));; *) (******************************) (* NUMERAL_TO_NUM_CONV: coverts usual HOL numerals into k-bit numerals *) let th_num_conv = Array.init maximum (fun i -> (SYM o SPEC_ALL) def_array.(i));; let mod_op_num = `MOD`;; let zero = `0`;; let DIV_BASE = let h1 = mk_eq(mk_binop div_op_num m_var_num max_const, q_var_num) in let h2 = mk_eq(mk_binop mod_op_num m_var_num max_const, r_var_num) in 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 (UNDISCH_ALL o ARITH_RULE) (mk_imp(h1, mk_imp(h2, c)));; let ZERO_EQ_ZERO = (EQT_ELIM o REWRITE_CONV[NUMERAL]) `0 = _0`;; let SYM_ZERO_EQ_ZERO = SYM ZERO_EQ_ZERO;; let SYM_NUM_THM = SYM NUM_THM;; let NUMERAL_TO_NUM_CONV tm = let rec raw_conv tm = if (rand tm = zero_const) then ZERO_EQ_ZERO else let th_div = NUM_DIV_CONV (mk_binop div_op_num tm max_const) in let th_mod = NUM_MOD_CONV (mk_binop mod_op_num tm max_const) in let q_tm = rand(concl th_div) in let r_tm = rand(concl th_mod) in let th0 = INST[tm, m_var_num; q_tm, q_var_num; r_tm, r_var_num] DIV_BASE in let th1 = MY_PROVE_HYP th_mod (MY_PROVE_HYP th_div th0) in let r = dest_small_numeral r_tm in let th2 = INST[q_tm, n_var_num] th_num_conv.(r) in let th = TRANS th1 th2 in let ltm, rtm = dest_comb(rand(concl th)) in let r_th = raw_conv rtm in TRANS th (AP_TERM ltm r_th) in if (fst o dest_const o rator) tm <> "NUMERAL" then failwith "NUMERAL_TO_NUM_CONV" else let th0 = raw_conv tm in let n_tm = rand(concl th0) in TRANS th0 (INST[n_tm, n_var_num] SYM_NUM_THM);; (* (* 100: 2.588 *) test 100 NUMERAL_TO_NUM_CONV `100034242430`;; *) let replace_numerals = rand o concl o DEPTH_CONV NUMERAL_TO_NUM_CONV;; let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);; (* NUM_TO_NUMERAL_CONV *) let NUM_TO_NUMERAL_CONV tm = let rec raw_conv tm = if tm = zero_const then SYM_ZERO_EQ_ZERO else let b_tm, n_tm = dest_comb tm in let n_th = raw_conv n_tm in let n_tm' = rand(concl n_th) in let cb = (fst o dest_const) b_tm in let th0 = Hashtbl.find def_table cb in let th1 = AP_TERM b_tm n_th in let th2 = TRANS th1 (INST[n_tm', n_var_num] th0) in let ltm, rtm = dest_comb(rand(concl th2)) in let mul_th = NUM_MULT_CONV (rand ltm) in let add_th0 = AP_THM (AP_TERM plus_op_num mul_th) rtm in let add_th = TRANS add_th0 (NUM_ADD_CONV (rand(concl add_th0))) in TRANS th2 add_th in let ltm, rtm = dest_comb tm in if (fst o dest_const) ltm <> num_name then failwith "NUM_TO_NUMERAL_CONV" else let num_th = INST[rtm, n_var_num] NUM_THM in let th0 = raw_conv rtm in TRANS num_th th0;; (*************************) (* SUC_CONV *) let suc_const = `SUC`;; (* Theorems *)
let SUC_NUM = prove(mk_eq(mk_comb(suc_const, mk_comb (num_const, n_var_num)),
                          mk_comb(num_const, mk_comb (suc_const, n_var_num))),
                    REWRITE_TAC[num_def; NUMERAL]);;
let SUC_0 = prove(mk_eq(`SUC _0`, mk_comb (const_array.(1), zero_const)),
                  REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_SUC; NUMERAL; ARITH_ADD]);;
let suc_th i = let cflag = (i + 1 >= maximum) in let suc = if (cflag) then 0 else i + 1 in let lhs = mk_comb(suc_const, (mk_comb (const_array.(i), n_var_num))) in let rhs = mk_comb(const_array.(suc), if (cflag) then mk_comb(suc_const, n_var_num) else n_var_num) in let proof = REWRITE_TAC [def_array.(i); def_array.(suc)] THEN ARITH_TAC in prove(mk_eq(lhs, rhs), proof);; let th_suc_array = Array.init maximum suc_th;; let th_suc_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do Hashtbl.add th_suc_table names_array.(i) th_suc_array.(i) done;; let SUC_MAX = th_suc_array.(maximum - 1);; let bit_max_name = names_array.(maximum - 1);; (* Conversion *) let rec raw_suc_conv_hash tm = let otm = rand tm in if (otm = zero_const) then SUC_0 else let btm, ntm = dest_comb otm in let cn = fst(dest_const btm) in if (cn = bit_max_name) then let th = INST [ntm, n_var_num] SUC_MAX in let ltm, rtm = dest_comb(rand(concl th)) in TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm)) else INST [ntm, n_var_num] (Hashtbl.find th_suc_table cn);; let NUM_SUC_HASH_CONV tm = let ntm = rand (rand tm) in let th = INST [ntm, n_var_num] SUC_NUM in let lhs, rhs = dest_eq(concl th) in if (lhs <> tm) then failwith("NUM_SUC_HASH_CONV") else let ltm, rtm = dest_comb rhs in TRANS th (AP_TERM ltm (raw_suc_conv_hash rtm));; (* let x = mk_comb(suc_const, mk_small_numeral_array 99999);; NUM_SUC_HASH_CONV x;; (* 10: 1.488 *) test 50000 NUM_SUC_HASH_CONV x;; (* 5: 0.980 *) *) (**************************************) (* EQ_0_CONV *)
let EQ_0_NUM = prove(mk_eq(mk_eq(mk_comb(num_const, n_var_num), `_0`), `n = _0`),
		     REWRITE_TAC[num_def; NUMERAL]);;
let EQ_B0_0 = prove(mk_eq(mk_eq(mk_comb(b0_const, n_var_num), `_0`), `n = _0`),
		    REWRITE_TAC[b0_def; ADD_CLAUSES; NUMERAL; REWRITE_RULE[NUMERAL] MULT_EQ_0; ARITH_EQ]);;
let EQ_0_0 = 
prove(`_0 = _0 <=> T`,
REWRITE_TAC[ARITH_EQ]);;
let eq_0_lemma = REWRITE_RULE[NUMERAL] (ARITH_RULE `a + b = 0 <=> a = 0 /\ b = 0`);; let eq_0_i i = let concl = mk_eq(mk_eq(mk_comb(const_array.(i), n_var_num), zero_const), false_const) in prove(concl, REWRITE_TAC[def_array.(i); eq_0_lemma; NUMERAL; ARITH_EQ]);; let th_eq0_array = Array.init maximum (fun i -> if (i = 0) then EQ_0_0 else eq_0_i i);; let th_eq0_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do Hashtbl.add th_eq0_table names_array.(i) th_eq0_array.(i) done;; let rec raw_eq0_hash_conv rtm = if (rtm = zero_const) then EQ_0_0 else let b_tm, n_tm = dest_comb rtm in let cn = (fst o dest_const) b_tm in if (cn = b0_name) then let th0 = INST[n_tm, n_var_num] EQ_B0_0 in let th1 = raw_eq0_hash_conv n_tm in TRANS th0 th1 else INST[n_tm, n_var_num] (Hashtbl.find th_eq0_table cn);; let NUM_EQ0_HASH_CONV rtm = let n_tm = rand rtm in let th = INST [n_tm, n_var_num] EQ_0_NUM in TRANS th (raw_eq0_hash_conv n_tm);; (* let x = mk_small_numeral_array 0;; NUM_EQ0_HASH_CONV x;; raw_eq0_hash_conv `B0 (B0 _0)`;; *) (**************************************) (* PRE_CONV *) let pre_const = `PRE`;; (* Theorems *)
let PRE_NUM = prove(mk_eq(mk_comb(pre_const, mk_comb (num_const, n_var_num)),
                          mk_comb(num_const, mk_comb (pre_const, n_var_num))),
                    REWRITE_TAC[num_def; NUMERAL]);;
let PRE_0 = 
prove(`PRE _0 = _0`,
MP_TAC (CONJUNCT1 PRE) THEN SIMP_TAC[NUMERAL]);;
let PRE_B1_0 = prove(mk_eq(mk_comb(`PRE`, mk_comb(const_array.(1), `_0`)), `_0`),
		     REWRITE_TAC[def_array.(1); MUL_n_0; ARITH_ADD; NUMERAL; ARITH_PRE; ARITH_EQ]);;
let PRE_B0_n0 = (UNDISCH_ALL o prove)(mk_imp(`n = _0 <=> T`, mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), `_0`)), REWRITE_TAC[B0_EXPLICIT] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; MUL_n_0]) THEN REWRITE_TAC[NUMERAL; ARITH_PRE]);; let PRE_B0_n1 = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o prove)(mk_imp(`n = 0 <=> F`, mk_eq(mk_comb(`PRE`, mk_comb(b0_const, `n:num`)), mk_comb(const_array.(maximum - 1), `PRE n`))), REWRITE_TAC[B0_EXPLICIT; def_array.(maximum - 1)] THEN ARITH_TAC);; let PRE_lemma = (UNDISCH_ALL o PURE_REWRITE_RULE[NUMERAL] o ARITH_RULE) `((n = 0) <=> F) ==> (SUC m = n <=> PRE n = m)`;; let pre_th i = let pre = i - 1 in let pre_tm = mk_comb(const_array.(pre), n_var_num) in let suc_tm = mk_comb(suc_const, pre_tm) in let suc_th = raw_suc_conv_hash suc_tm in let n_tm = rand(concl suc_th) in let n0_th = raw_eq0_hash_conv n_tm in let th0 = INST[pre_tm, m_var_num; n_tm, n_var_num] PRE_lemma in MY_PROVE_HYP n0_th (EQ_MP th0 suc_th);; let th_pre_array = Array.init maximum (fun i -> if i = 0 then REFL `_0` else pre_th i);; let th_pre_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do Hashtbl.add th_pre_table names_array.(i) th_pre_array.(i) done;; (* Conversion *) let b1_name = names_array.(1);; let b1_pre_thm = th_pre_array.(1);; let rec raw_pre_hash_conv tm = let otm = rand tm in if (otm = zero_const) then PRE_0 else let btm, ntm = dest_comb otm in let cn = fst(dest_const btm) in if (cn = b0_name) then let n_th = raw_eq0_hash_conv ntm in if (rand(concl n_th) = false_const) then let th0 = INST[ntm, n_var_num] PRE_B0_n1 in let th1 = MY_PROVE_HYP n_th th0 in let ltm, rtm = dest_comb(rand(concl th1)) in let th2 = raw_pre_hash_conv rtm in TRANS th1 (AP_TERM ltm th2) else let th = INST[ntm, n_var_num] PRE_B0_n0 in MY_PROVE_HYP n_th th else if (cn = b1_name) then if (ntm = zero_const) then PRE_B1_0 else INST[ntm, n_var_num] b1_pre_thm else INST [ntm, n_var_num] (Hashtbl.find th_pre_table cn);; let NUM_PRE_HASH_CONV tm = let ntm = rand (rand tm) in let th = INST [ntm, n_var_num] PRE_NUM in let lhs, rhs = dest_eq(concl th) in if (lhs <> tm) then failwith("NUM_PRE_HASH_CONV") else let ltm, rtm = dest_comb rhs in TRANS th (AP_TERM ltm (raw_pre_hash_conv rtm));; (* let x = mk_comb(pre_const, mk_small_numeral_array 100000);; NUM_PRE_HASH_CONV x;; (* 10: 0.488; 100: 0.200 *) test 5000 NUM_PRE_HASH_CONV x;; let x = mk_comb(pre_const, mk_small_numeral_array 65536);; (* 10: 0.468; 100: 0.496 *) test 50000 NUM_PRE_HASH_CONV x;; *) (**************************************) (* GT0_CONV *) let gt0_table = Hashtbl.create maximum;; let GT0_NUM = (REWRITE_RULE[GSYM num_def] o prove)(`0 < NUMERAL n <=> _0 < n`, REWRITE_TAC[NUMERAL]);;
let gt0_0 = 
prove(`_0 < _0 <=> F`,
REWRITE_TAC[ARITH_LT]);;
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`), REWRITE_TAC[b0_def] THEN ARITH_TAC);; let zero = `0`;; let gt0_th i = let bi = const_array.(i) in let concl = mk_eq (mk_binop lt_op_num zero (mk_comb(bi, n_var_num)), truth_const) in let proof = REWRITE_TAC[def_array.(i)] THEN ARITH_TAC in (PURE_REWRITE_RULE[NUMERAL] o prove)(concl, proof);; for i = 1 to maximum - 1 do Hashtbl.add gt0_table names_array.(i) (gt0_th i) done;; let rec raw_gt0_hash_conv rtm = if (rtm = zero_const) then gt0_0 else let b_tm, n_tm = dest_comb rtm in let cn = (fst o dest_const) b_tm in if (cn = b0_name) then let th0 = INST[n_tm, n_var_num] gt0_b0 in let th1 = raw_gt0_hash_conv n_tm in TRANS th0 th1 else INST[n_tm, n_var_num] (Hashtbl.find gt0_table cn);; let NUM_GT0_HASH_CONV rtm = let n_tm = rand rtm in let th = INST [n_tm, n_var_num] GT0_NUM in TRANS th (raw_gt0_hash_conv n_tm);; (* let tm = mk_binop lt_op_num (mk_small_numeral_array 0) (mk_small_numeral_array 100000);; NUM_GT0_HASH_CONV (rand tm);; (* 10: 0.232 *) test 10000 NUM_GT0_HASH_CONV (rand tm);; *) (*************************************) (* LT and LE *) let LT_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m < NUMERAL n <=> m < n`, REWRITE_TAC[NUMERAL]);; let LE_NUM = (REWRITE_RULE[SYM num_def] o prove)(`NUMERAL m <= NUMERAL n <=> m <= n`, REWRITE_TAC[NUMERAL]);;
let LT_n_0 = 
prove(`n < _0 <=> F`,
SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN ARITH_TAC);;
let LE_0_n = 
prove(`_0 <= n <=> T`,
SUBGOAL_THEN `_0 = 0` MP_TAC THENL [ REWRITE_TAC[NUMERAL]; ALL_TAC ] THEN DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN ARITH_TAC);;
let SUC_LT_THM = ARITH_RULE `SUC m < SUC n <=> m < n`;;
let SUC_LE_THM = ARITH_RULE `SUC m <= SUC n <=> m <= n`;;
(* LT tables *) (* Generates the theorem |- _0 < bi(n) <=> T (or |- _0 < b0(n) <=> _0 < n) *) let gen_0_lt_bi i = let bin = mk_comb (const_array.(i), n_var_num) in let lt_tm = mk_binop lt_op_num zero bin in if i > 0 then (PURE_REWRITE_RULE[NUMERAL] o EQT_INTRO o prove)(lt_tm, REWRITE_TAC[def_array.(i)] THEN ARITH_TAC) else (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `0 < n`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);; let th_lt0_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do let th = gen_0_lt_bi i in let name = names_array.(i) in Hashtbl.add th_lt0_table name th done;; (* Generates the theorem |- bi(m) < bj(n) <=> m <= n (or m < n) *) let gen_bi_lt_bj i j = let bim = mk_comb (const_array.(i), m_var_num) in let bjn = mk_comb (const_array.(j), n_var_num) in let lt_tm = mk_binop lt_op_num bim bjn in let rhs = if i >= j then mk_binop lt_op_num m_var_num n_var_num else mk_binop le_op_num m_var_num n_var_num in prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);; (* Given a theorem |- bi(m) < bj(n) <=> P m n, generates the theorem |- SUC(bi(m)) < SUC(bj(n)) <=> P m n *) let gen_next_lt_thm th = let ltm, n_tm = (dest_comb o lhand o concl) th in let m_tm = rand ltm in let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LT_THM in let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in let th1 = SYM (MK_COMB ((AP_TERM lt_op_num suc_m), suc_n)) in TRANS (TRANS th1 th0) th;; let th_lt_table = Hashtbl.create (maximum * maximum);; for i = 0 to maximum - 1 do let th = ref (gen_bi_lt_bj 0 i) in let name_left = names_array.(0) and name_right = names_array.(i) in let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in for k = 1 to maximum - i - 1 do let x = k and y = i + k in let name_left = names_array.(x) and name_right = names_array.(y) in th := gen_next_lt_thm (!th); Hashtbl.add th_lt_table (name_left ^ name_right) !th done; done;; for i = 1 to maximum - 1 do let th = ref (gen_bi_lt_bj i 0) in let name_left = names_array.(i) and name_right = names_array.(0) in let _ = Hashtbl.add th_lt_table (name_left ^ name_right) !th in for k = 1 to maximum - i - 1 do let x = i + k and y = k in let name_left = names_array.(x) and name_right = names_array.(y) in th := gen_next_lt_thm (!th); Hashtbl.add th_lt_table (name_left ^ name_right) !th done; done;; (* LE tables *) (* Generates the theorem |- bi(n) <= _0 <=> F (or |- b0(n) <= _0 <=> n <= _0) *) let gen_bi_le_0 i = let bin = mk_comb (const_array.(i), n_var_num) in let lt_tm = mk_binop le_op_num bin zero in if i > 0 then (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, false_const), REWRITE_TAC[def_array.(i)] THEN ARITH_TAC) else (PURE_REWRITE_RULE[NUMERAL] o prove)(mk_eq(lt_tm, `n <= 0`), REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);; let th_le0_table = Hashtbl.create maximum;; for i = 0 to maximum - 1 do let th = gen_bi_le_0 i in let name = names_array.(i) in Hashtbl.add th_le0_table name th done;; (* Generates the theorem |- bi(m) <= bj(n) <=> m <= n (or m < n) *) let gen_bi_le_bj i j = let bim = mk_comb (const_array.(i), m_var_num) in let bjn = mk_comb (const_array.(j), n_var_num) in let lt_tm = mk_binop le_op_num bim bjn in let rhs = if i > j then mk_binop lt_op_num m_var_num n_var_num else mk_binop le_op_num m_var_num n_var_num in prove(mk_eq(lt_tm, rhs), REWRITE_TAC[def_array.(i); def_array.(j)] THEN ARITH_TAC);; (* Given a theorem |- bi(m) <= bj(n) <=> P m n, generates the theorem |- SUC(bi(m)) <= SUC(bj(n)) <=> P m n *) let gen_next_le_thm th = let ltm, n_tm = (dest_comb o lhand o concl) th in let m_tm = rand ltm in let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] SUC_LE_THM in let suc_m = raw_suc_conv_hash (mk_comb (suc_const, m_tm)) in let suc_n = raw_suc_conv_hash (mk_comb (suc_const, n_tm)) in let th1 = SYM (MK_COMB ((AP_TERM le_op_num suc_m), suc_n)) in TRANS (TRANS th1 th0) th;; let th_le_table = Hashtbl.create (maximum * maximum);; for i = 0 to maximum - 1 do let th = ref (gen_bi_le_bj 0 i) in let name_left = names_array.(0) and name_right = names_array.(i) in let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in for k = 1 to maximum - i - 1 do let x = k and y = i + k in let name_left = names_array.(x) and name_right = names_array.(y) in th := gen_next_le_thm (!th); Hashtbl.add th_le_table (name_left ^ name_right) !th done; done;; for i = 1 to maximum - 1 do let th = ref (gen_bi_le_bj i 0) in let name_left = names_array.(i) and name_right = names_array.(0) in let _ = Hashtbl.add th_le_table (name_left ^ name_right) !th in for k = 1 to maximum - i - 1 do let x = i + k and y = k in let name_left = names_array.(x) and name_right = names_array.(y) in th := gen_next_le_thm (!th); Hashtbl.add th_le_table (name_left ^ name_right) !th done; done;; (* Conversions *) let rec raw_lt_hash_conv tm = let ltm, rtm = dest_comb tm in let ltm = rand ltm in if is_const rtm then (* n < _0 <=> F *) INST[ltm, n_var_num] LT_n_0 else if is_const ltm then (* _0 < Bi(n) *) let bn_tm, n_tm = dest_comb rtm in let cbn = (fst o dest_const) bn_tm in let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_lt0_table cbn) in if cbn = b0_name then let th1 = raw_lt_hash_conv (rand (concl th0)) in TRANS th0 th1 else th0 else (* Bi(n) < Bj(m) *) let bm_tm, m_tm = dest_comb ltm in let bn_tm, n_tm = dest_comb rtm in let cbm = (fst o dest_const) bm_tm in let cbn = (fst o dest_const) bn_tm in let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_lt_table (cbm^cbn)) in let op = (fst o dest_const o rator o rator o rand o concl) th0 in let th1 = if op = "<" then raw_lt_hash_conv (rand (concl th0)) else raw_le_hash_conv (rand (concl th0)) in TRANS th0 th1 and raw_le_hash_conv tm = let ltm, rtm = dest_comb tm in let ltm = rand ltm in if is_const ltm then (* _0 <= n <=> T *) INST[rtm, n_var_num] LE_0_n else if is_const rtm then (* Bi(n) <= _0 *) let bn_tm, n_tm = dest_comb ltm in let cbn = (fst o dest_const) bn_tm in let th0 = INST[n_tm, n_var_num] (Hashtbl.find th_le0_table cbn) in if cbn = b0_name then let th1 = raw_le_hash_conv (rand (concl th0)) in TRANS th0 th1 else th0 else (* Bi(n) <= Bj(m) *) let bm_tm, m_tm = dest_comb ltm in let bn_tm, n_tm = dest_comb rtm in let cbm = (fst o dest_const) bm_tm in let cbn = (fst o dest_const) bn_tm in let th0 = INST[m_tm, m_var_num; n_tm, n_var_num] (Hashtbl.find th_le_table (cbm^cbn)) in let op = (fst o dest_const o rator o rator o rand o concl) th0 in let th1 = if op = "<" then raw_lt_hash_conv (rand (concl th0)) else raw_le_hash_conv (rand (concl th0)) in TRANS th0 th1;; let NUM_LT_HASH_CONV tm = let atm, rtm = dest_comb tm in let ltm = rand atm in let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LT_NUM in let rtm = rand(concl th) in TRANS th (raw_lt_hash_conv rtm);; let NUM_LE_HASH_CONV tm = let atm, rtm = dest_comb tm in let ltm = rand atm in let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] LE_NUM in let rtm = rand(concl th) in TRANS th (raw_le_hash_conv rtm);; (* let x = num_of_string "3543593547359325353535";; let y = num_of_string "9392392983247294924242";; let xx = mk_binop lt_op_num (mk_numeral_array x) (mk_numeral_array y);; let yy = mk_binop lt_op_num (mk_numeral x) (mk_numeral y);; (* 2.38 *) test 1000 NUM_LT_CONV yy;; (* 10: 1.248 *) test 10000 NUM_LT_HASH_CONV xx;; *) (**************************************) (* ADD_CONV *) (* ADD theorems *) let ADD_NUM = (REWRITE_RULE[GSYM num_def] o prove) (`NUMERAL m + NUMERAL n = NUMERAL (m + n)`, REWRITE_TAC[NUMERAL]);;
let CADD_0_n = 
prove(`SUC (_0 + n) = SUC n`,
REWRITE_TAC[ADD_0_n]);;
let CADD_n_0 = 
prove(`SUC (n + _0) = SUC n`,
REWRITE_TAC[ADD_n_0]);;
(* B0 (SUC n) = B0 n + maximum *)
let B0_SUC = prove(mk_eq(mk_comb(b0_const, mk_comb(suc_const, n_var_num)),
                         mk_binop plus_op_num max_const (mk_comb(b0_const, n_var_num))),
                   REWRITE_TAC [B0_EXPLICIT] THEN ARITH_TAC);;
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)),
                         mk_comb(b0_const, mk_binop plus_op_num m_var_num n_var_num)),
                   REWRITE_TAC[B0_EXPLICIT] THEN ARITH_TAC);;
let SUC_ADD_RIGHT = 
prove(`SUC(m + n) = m + SUC n`,
ARITH_TAC);;
(* Generate all theorems iteratively *) let th_add_right_next th = let lhs, rhs = dest_eq(concl th) in let ltm, rtm = dest_comb rhs in let cn = fst(dest_const ltm) in let suc_th = AP_TERM suc_const th in let th_rhs = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in let ltm, rarg = dest_comb lhs in let larg = rand ltm in let th1 = INST[larg, m_var_num; rarg, n_var_num] SUC_ADD_RIGHT in let cn = fst(dest_const(rator rarg)) in let th2 = Hashtbl.find th_suc_table cn in let th_lhs = TRANS th1 (AP_TERM ltm th2) in TRANS (TRANS (SYM th_lhs) suc_th) th_rhs;; let th_add_array = Array.make (maximum * maximum) (REFL zero_const);; for i = 0 to maximum - 1 do let th0 = if i = 0 then B0_ADD else INST[n_var_num, m_var_num; m_var_num, n_var_num] (ONCE_REWRITE_RULE[ADD_AC] th_add_array.(i)) in let _ = th_add_array.(i * maximum) <- th0 in for j = 1 to maximum - 1 do th_add_array.(i * maximum + j) <- th_add_right_next th_add_array.(i * maximum + j - 1) done; done;; (* SUC (B_i(m) + B_j(n)) = B_p(...) *) let th_cadd i j = let add_th = th_add_array.(i * maximum + j) in let th0 = AP_TERM suc_const add_th in let ltm, rtm = dest_comb(rand(concl th0)) in let ltm, rtm = dest_comb rtm in let cn = fst(dest_const ltm) in let suc_th = INST[rtm, n_var_num] (Hashtbl.find th_suc_table cn) in TRANS th0 suc_th;; let th_cadd_array = Array.make (maximum * maximum) (REFL zero_const);; for i = 0 to maximum - 1 do for j = 0 to maximum - 1 do th_cadd_array.(i * maximum + j) <- th_cadd i j done; done;; let th_add_table = Hashtbl.create (maximum * maximum);; for i = 0 to maximum - 1 do for j = 0 to maximum - 1 do let name = names_array.(i) ^ names_array.(j) in let th = th_add_array.(i * maximum + j) in let cflag = (i + j >= maximum) in Hashtbl.add th_add_table name (th, cflag) done; done;; let th_cadd_table = Hashtbl.create (maximum * maximum);; for i = 0 to maximum - 1 do for j = 0 to maximum - 1 do let name = names_array.(i) ^ names_array.(j) in let th = th_cadd_array.(i * maximum + j) in let cflag = (i + j + 1 >= maximum) in Hashtbl.add th_cadd_table name (th, cflag) done; done;; (* ADD conversion *) let rec raw_add_conv_hash tm = let atm,rtm = dest_comb tm in let ltm = rand atm in if ltm = zero_const then INST [rtm,n_var_num] ADD_0_n else if rtm = zero_const then INST [ltm,n_var_num] ADD_n_0 else let lbit,larg = dest_comb ltm and rbit,rarg = dest_comb rtm in let name = fst(dest_const lbit) ^ fst(dest_const rbit) in let th0, cflag = Hashtbl.find th_add_table name in let th = INST [larg, m_var_num; rarg, n_var_num] th0 in let ltm, rtm = dest_comb(rand(concl th)) in if cflag then TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm)) else TRANS th (AP_TERM ltm (raw_add_conv_hash rtm)) and raw_adc_conv_hash tm = let atm,rtm = dest_comb (rand tm) in let ltm = rand atm in if ltm = zero_const then let th = INST [rtm,n_var_num] CADD_0_n in TRANS th (raw_suc_conv_hash (rand(concl th))) else if rtm = zero_const then let th = INST [ltm,n_var_num] CADD_n_0 in TRANS th (raw_suc_conv_hash (rand(concl th))) else let lbit,larg = dest_comb ltm and rbit,rarg = dest_comb rtm in let name = fst(dest_const lbit) ^ fst(dest_const rbit) in let th0, cflag = Hashtbl.find th_cadd_table name in let th = INST [larg, m_var_num; rarg, n_var_num] th0 in let ltm, rtm = dest_comb(rand(concl th)) in if cflag then TRANS th (AP_TERM ltm (raw_adc_conv_hash rtm)) else TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));; let NUM_ADD_HASH_CONV tm = let atm, rtm = dest_comb tm in let ltm = rand atm in let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] ADD_NUM in let ltm, rtm = dest_comb(rand(concl th)) in TRANS th (AP_TERM ltm (raw_add_conv_hash rtm));; (* let x = num_of_string "3543593547359325353535";; let y = num_of_string "9392392983247294924242";; let xx = mk_binop plus_op_num (mk_numeral_array x) (mk_numeral_array y);; let yy = mk_binop plus_op_num (mk_numeral x) (mk_numeral y);; NUM_ADD_HASH_CONV xx;; test 10000 NUM_ADD_CONV yy;; (* 5.672 *) (* 10: 1.672 *) test 10000 NUM_ADD_HASH_CONV xx;; *) (********************************) (* Subtraction *)
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)),
                          mk_comb(num_const, mk_binop minus_op_num m_var_num n_var_num)),
                    REWRITE_TAC[num_def; NUMERAL]);;
let SUB_lemma1 = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> m - n = t:num`;; let SUB_lemma2 = (UNDISCH_ALL o REWRITE_RULE[NUMERAL] o ARITH_RULE) `m + t = n ==> m - n = 0`;; let LE_lemma = (UNDISCH_ALL o ARITH_RULE) `n + t = m ==> n <= m:num`;; let raw_sub_hash_conv tm = let ltm, n_tm = dest_comb tm in let m_tm = rand ltm in let m = raw_dest_hash m_tm in let n = raw_dest_hash n_tm in let t = m -/ n in if t >=/ num_0 then let t_tm = rand (mk_numeral_array t) in let th0 = INST[n_tm, n_var_num; t_tm, t_var_num; m_tm, m_var_num] SUB_lemma1 in let th_add = raw_add_conv_hash (mk_binop plus_op_num n_tm t_tm) in MY_PROVE_HYP th_add th0 else let t_tm = rand (mk_numeral_array (Num.abs_num t)) in let th0 = INST[m_tm, m_var_num; t_tm, t_var_num; n_tm, n_var_num] SUB_lemma2 in let th_add = raw_add_conv_hash (mk_binop plus_op_num m_tm t_tm) in MY_PROVE_HYP th_add th0;; (* Returns either (tm1 - tm2, tm2 <= tm1) or (tm2 - tm1, tm1 <= tm2) *) let raw_sub_and_le_hash_conv tm1 tm2 = let m = raw_dest_hash tm1 in let n = raw_dest_hash tm2 in let t = m -/ n in if t >=/ num_0 then let t_tm = rand (mk_numeral_array t) in let inst = INST[tm2, n_var_num; t_tm, t_var_num; tm1, m_var_num] in let th_sub = inst SUB_lemma1 in let th_le = inst LE_lemma in let th_add = raw_add_conv_hash (mk_binop plus_op_num tm2 t_tm) in (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le) else let t_tm = rand (mk_numeral_array (Num.abs_num t)) in let inst = INST[tm2, m_var_num; t_tm, t_var_num; tm1, n_var_num] in let th_sub = inst SUB_lemma1 in let th_le = inst LE_lemma in let th_add = raw_add_conv_hash (mk_binop plus_op_num tm1 t_tm) in (MY_PROVE_HYP th_add th_sub, MY_PROVE_HYP th_add th_le);; let NUM_SUB_HASH_CONV tm = let atm, rtm = dest_comb tm in let ltm = rand atm in let th = INST [rand ltm, m_var_num; rand rtm, n_var_num] SUB_NUM in let ltm, rtm = dest_comb(rand(concl th)) in TRANS th (AP_TERM ltm (raw_sub_hash_conv rtm));; (* let y = num_of_string "3543593547359325353535";; let x = num_of_string "9392392983247294924242";; let xx = mk_binop minus_op_num (mk_numeral_array x) (mk_numeral_array y);; let yy = mk_binop minus_op_num (mk_numeral x) (mk_numeral y);; NUM_SUB_HASH_CONV xx;; test 1000 NUM_SUB_CONV yy;; (* 2.376 *) (* 10: 0.872 *) test 1000 NUM_SUB_HASH_CONV xx;; *) (********************************) (* Multiplication *)
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)),
                          mk_comb(num_const, mk_binop mul_op_num m_var_num n_var_num)),
                    REWRITE_TAC[num_def; NUMERAL]);;
let MUL_0_n = 
prove(`_0 * n = _0`,
ONCE_REWRITE_TAC[GSYM NUM_THM] THEN ONCE_REWRITE_TAC[GSYM MUL_NUM] THEN REWRITE_TAC[num_def] THEN REWRITE_TAC[MULT_CLAUSES]);;
let MUL_n_0 = ONCE_REWRITE_RULE[MULT_AC] MUL_0_n;; let MUL_1_n, MUL_n_1 = let one_const = mk_comb (const_array.(1), zero) in let cond = mk_eq(mk_binop mul_op_num one_const n_var_num, n_var_num) in let th = (REWRITE_RULE[NUMERAL] o prove)(cond, REWRITE_TAC[def_array.(1)] THEN ARITH_TAC) in th, ONCE_REWRITE_RULE[MULT_AC] th;;
let MUL_B0_t = prove(mk_eq(mk_binop mul_op_num (mk_comb(b0_const, n_var_num)) t_var_num,
                           mk_comb(b0_const, mk_binop mul_op_num n_var_num t_var_num)),
                     REWRITE_TAC[def_array.(0)] THEN ARITH_TAC);;
let MUL_t_B0 = ONCE_REWRITE_RULE[MULT_AC] MUL_B0_t;;
let MUL_SUC_RIGHT = 
prove(`m * SUC(n) = m * n + m`,
ARITH_TAC);;
(* Multiplication table *) let mul_th_next_right th = let ltm, rtm = dest_comb(rand(rator(concl th))) in let mtm = rand ltm in let th0 = INST[mtm, m_var_num; rtm, n_var_num] MUL_SUC_RIGHT in let th1 = AP_THM (AP_TERM plus_op_num th) mtm in let sum_th = raw_add_conv_hash (rand(concl th1)) in let th2 = TRANS (TRANS th0 th1) sum_th in let cn = fst(dest_const (rator rtm)) in let th_suc = INST[zero_const, n_var_num] (Hashtbl.find th_suc_table cn) in let th3 = AP_TERM (mk_comb (mul_op_num, mtm)) th_suc in TRANS (SYM th3) th2;; let mul_array = Array.make (maximum * maximum) (REFL zero_const);; for i = 1 to maximum - 1 do let th1 = INST[mk_comb(const_array.(i), zero_const), n_var_num] MUL_n_1 in let _ = mul_array.(i * maximum + 1) <- th1 in for j = 2 to maximum - 1 do mul_array.(i * maximum + j) <- mul_th_next_right mul_array.(i * maximum + j - 1) done; done;; let mul_table = Hashtbl.create (maximum * maximum);; for i = 1 to maximum - 1 do for j = 1 to maximum - 1 do Hashtbl.add mul_table (names_array.(i) ^ names_array.(j)) mul_array.(i * maximum + j) done; done;; (* General multiplication theorem *) let prod_lemma = let mul (a,b) = mk_binop mul_op_num a b and add (a,b) = mk_binop plus_op_num a b in let lhs = mul(add(t_var_num, mk_comb(b0_const, m_var_num)), add(r_var_num, mk_comb(b0_const, n_var_num))) in let rhs = add(mul(t_var_num, r_var_num), mk_comb(b0_const, add(mk_comb(b0_const, mul(m_var_num, n_var_num)), add(mul(m_var_num, r_var_num), mul(n_var_num, t_var_num))))) in prove(mk_eq(lhs, rhs), REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MUL_B0_t; MUL_t_B0] THEN ONCE_REWRITE_TAC[GSYM ADD_ASSOC] THEN REWRITE_TAC[th_add_array.(0)] THEN REWRITE_TAC[ADD_AC; MULT_AC]);; let ADD_ASSOC' = SPEC_ALL ADD_ASSOC;; let dest_op tm = let ltm, rtm = dest_comb tm in rand ltm, rtm;; (* B_i(m) * B_j(n) = B_p(B_q(m * n) + m * B_j(0) + n * B_i(0)) where B_p(B_q(0)) = i * j *) let gen_mul_thm i j = let bi0 = mk_comb(const_array.(i), zero_const) and bj0 = mk_comb(const_array.(j), zero_const) in let def_i = INST[m_var_num, n_var_num] def_thm_array.(i) in let def_j = def_thm_array.(j) in let th0 = MK_COMB(AP_TERM mul_op_num def_i, def_j) in let th1 = TRANS th0 (INST[bi0, t_var_num; bj0, r_var_num] prod_lemma) in let mul_th = mul_array.(i * maximum + j) in let larg, rarg = dest_op (rand (concl th1)) in let th2 = TRANS th1 (AP_THM (AP_TERM plus_op_num mul_th) rarg) in let larg = rand(concl mul_th) in let b_low, b_high = dest_comb larg in let rtm = rand(rarg) in let th_add = INST[b_high, m_var_num; rtm, n_var_num] (fst(Hashtbl.find th_add_table (fst(dest_const b_low)^b0_name))) in if i * j < maximum then let ltm, rtm = dest_op(rand(rand(concl th_add))) in let add_0 = AP_TERM b_low (INST[rtm, n_var_num] ADD_0_n) in TRANS th2 (TRANS th_add add_0) else let larg, rtm = dest_op (rand(rand(concl th_add))) in let rarg, rtm = dest_op rtm in let th_assoc = INST[larg, m_var_num; rarg, n_var_num; rtm, p_var_num] ADD_ASSOC' in let mn = rand(rarg) in let b_high = rator b_high in let th_add2' = INST[zero_const, m_var_num; mn, n_var_num] (fst(Hashtbl.find th_add_table (fst(dest_const b_high)^b0_name))) in let add_0 = AP_TERM b_high (INST[mn, n_var_num] ADD_0_n) in let th_add2 = TRANS th_add2' add_0 in let th3 = TRANS th_assoc (AP_THM (AP_TERM plus_op_num th_add2) rtm) in let th4 = TRANS th_add (AP_TERM b_low th3) in TRANS th2 th4;; let gen_mul_table = Hashtbl.create (maximum * maximum);; for i = 1 to maximum - 1 do for j = 1 to maximum - 1 do let name = names_array.(i) ^ names_array.(j) in Hashtbl.add gen_mul_table name (gen_mul_thm i j) done; done;; (* B_i(m) * B_j(0) = B_p(B_q(0) + m * B_j(0)) where i * j = B_p(B_q(0)) *) let mul1_right_th i j = let th0 = INST[zero_const, n_var_num] (Hashtbl.find gen_mul_table (names_array.(i)^names_array.(j))) in let b_low, rtm = dest_comb(rand(concl th0)) in let tm1, tm23 = dest_op rtm in let tm2p, tm3 = dest_comb tm23 in let tm3_th = INST[rand tm3, n_var_num] MUL_0_n in let tm2_th = INST[rand(tm2p), n_var_num] ADD_n_0 in let tm23_th = TRANS (AP_TERM tm2p tm3_th) tm2_th in let ltm, rtm = dest_comb tm1 in if (i * j < maximum) then let tm1_th = TRANS (AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0)) B0_0 in let tm123_th' = TRANS (INST[tm23, n_var_num] ADD_0_n) tm23_th in let tm123_th = TRANS (AP_THM (AP_TERM plus_op_num tm1_th) tm23) tm123_th' in TRANS th0 (AP_TERM b_low tm123_th) else let tm1_th = AP_TERM ltm (INST[m_var_num, n_var_num] MUL_n_0) in let tm123_th = MK_COMB(AP_TERM plus_op_num tm1_th, tm23_th) in TRANS th0 (AP_TERM b_low tm123_th);; (* B_j(0) * B_i(m) = B_p(B_q(0) + B_j(0) * B_i(m) *) let MULT_AC' = CONJUNCT1 MULT_AC;; let mul1_left_th th = let lhs, rhs = dest_eq(concl th) in let ltm, rtm = dest_op lhs in let th_lhs = INST[ltm, n_var_num; rtm, m_var_num] MULT_AC' in let btm, rtm = dest_comb rhs in let larg, rarg = dest_op rtm in if (is_comb larg) then let ltm, rtm = dest_op rarg in let th_rhs' = INST[ltm, m_var_num; rtm, n_var_num] MULT_AC' in let th_rhs = AP_TERM (mk_comb(plus_op_num, larg)) th_rhs' in TRANS th_lhs (TRANS th (AP_TERM btm th_rhs)) else let th_rhs = INST[larg, m_var_num; rarg, n_var_num] MULT_AC' in TRANS th_lhs (TRANS th (AP_TERM btm th_rhs));; let mul1_right_th_table = Hashtbl.create (maximum * maximum);; let mul1_left_th_table = Hashtbl.create (maximum * maximum);; for i = 1 to maximum - 1 do for j = 1 to maximum - 1 do let name_right = names_array.(i) ^ names_array.(j) in let name_left = names_array.(j) ^ names_array.(i) in let th = mul1_right_th i j in let add_flag = (i * j >= maximum) in let _ = Hashtbl.add mul1_right_th_table name_right (add_flag, th) in Hashtbl.add mul1_left_th_table name_left (add_flag, mul1_left_th th) done; done;; (******************************************************) (* Conversions *) (* Multiplies arg and (tm = tmname(_0)) *) let rec raw_mul1_right_hash arg tm tmname = if arg = zero_const then INST [tm, n_var_num] MUL_0_n else let btm, mtm = dest_comb arg in let cn = fst(dest_const btm) in if (cn = b0_name) then let th = INST[mtm, n_var_num; tm, t_var_num] MUL_B0_t in TRANS th (AP_TERM b0_const (raw_mul1_right_hash mtm tm tmname)) else let name = cn ^ tmname in if (mtm = zero_const) then Hashtbl.find mul_table name else let add_flag, th' = Hashtbl.find mul1_right_th_table name in let th = INST[mtm, m_var_num] th' in if add_flag then let ltm, rtm = dest_comb(rand(concl th)) in let lplus, rarg = dest_comb rtm in let th2 = AP_TERM lplus (raw_mul1_right_hash mtm tm tmname) in let th_add = raw_add_conv_hash (rand(concl th2)) in TRANS th (AP_TERM ltm (TRANS th2 th_add)) else let ltm = rator(rand(concl th)) in let th2 = AP_TERM ltm (raw_mul1_right_hash mtm tm tmname) in TRANS th th2;; (* Multiplies (tm = tmname(_0)) and arg *) let rec raw_mul1_left_hash tm tmname arg = if arg = zero_const then INST [tm, n_var_num] MUL_n_0 else let btm, mtm = dest_comb arg in let cn = fst(dest_const btm) in if (cn = b0_name) then let th = INST[mtm, n_var_num; tm, t_var_num] MUL_t_B0 in TRANS th (AP_TERM b0_const (raw_mul1_left_hash tm tmname mtm)) else let name = tmname ^ cn in if (mtm = zero_const) then Hashtbl.find mul_table name else let add_flag, th' = Hashtbl.find mul1_left_th_table name in let th = INST[mtm, m_var_num] th' in if add_flag then let ltm, rtm = dest_comb(rand(concl th)) in let lplus, rarg = dest_comb rtm in let th2 = AP_TERM lplus (raw_mul1_left_hash tm tmname mtm) in let th_add = raw_add_conv_hash (rand(concl th2)) in TRANS th (AP_TERM ltm (TRANS th2 th_add)) else let ltm = rator(rand(concl th)) in let th2 = AP_TERM ltm (raw_mul1_left_hash tm tmname mtm) in TRANS th th2;; (* Computes B_i(m) * B_j(n) *) let rec raw_mul_conv_hash tm = let larg, rarg = dest_comb tm in let larg = rand larg in if larg = zero_const then INST [rarg, n_var_num] MUL_0_n else if rarg = zero_const then INST [larg, n_var_num] MUL_n_0 else let lbtm, mtm = dest_comb larg in let lcn = fst(dest_const lbtm) in if (lcn = b0_name) then let th = INST[rarg, t_var_num; mtm, n_var_num] MUL_B0_t in let ltm, rtm = dest_comb(rand(concl th)) in TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm)) else let rbtm, ntm = dest_comb rarg in let rcn = fst(dest_const rbtm) in if (rcn = b0_name) then let th = INST[larg, t_var_num; ntm, n_var_num] MUL_t_B0 in let ltm, rtm = dest_comb(rand(concl th)) in TRANS th (AP_TERM ltm (raw_mul_conv_hash rtm)) else if (ntm = zero_const) then if (mtm = zero_const) then Hashtbl.find mul_table (lcn ^ rcn) else raw_mul1_right_hash larg (mk_comb(rbtm, zero_const)) rcn else if (mtm = zero_const) then raw_mul1_left_hash (mk_comb(lbtm, zero_const)) lcn rarg else let th0 = INST[mtm, m_var_num; ntm, n_var_num] (Hashtbl.find gen_mul_table (lcn ^ rcn)) in let b_low, expr = dest_comb(rand(concl th0)) in let ltm, rsum = dest_comb expr in let b_high, mul0 = dest_comb (rand ltm) in let th_mul0 = raw_mul_conv_hash mul0 in let th_mul1 = raw_mul1_right_hash mtm (mk_comb(rbtm, zero_const)) rcn in let th_mul2 = raw_mul1_right_hash ntm (mk_comb(lbtm, zero_const)) lcn in let th_larg = AP_TERM plus_op_num (AP_TERM b_high th_mul0) in let th_rarg = MK_COMB(AP_TERM plus_op_num th_mul1, th_mul2) in let add_rarg = TRANS th_rarg (raw_add_conv_hash (rand(concl th_rarg))) in let add_th = MK_COMB (th_larg, add_rarg) in let add = TRANS add_th (raw_add_conv_hash (rand(concl add_th))) in TRANS th0 (AP_TERM b_low add);; (* The main multiplication conversion *) let NUM_MULT_HASH_CONV tm = let ltm, rtm = dest_comb tm in let larg, rarg = rand (rand ltm), rand rtm in let th0 = INST[larg, m_var_num; rarg, n_var_num] MUL_NUM in if (rand(rator(concl th0)) <> tm) then failwith "NUM_MULT_HASH_CONV" else let rtm = rand(rand(concl th0)) in let th = raw_mul_conv_hash rtm in TRANS th0 (AP_TERM num_const th);; (**************************) (* Tests *) (* let x = Int 325325353;; let y = Int 999434312;; let xx = mk_binop mul_op_num (mk_numeral_array x) (mk_numeral_array y);; let yy = mk_binop mul_op_num (mk_numeral x) (mk_numeral y);; let zz = rand(concl(REWRITE_CONV[NUM_THM] xx));; NUM_MULT_HASH_CONV xx;; test 1000 NUM_MULT_CONV yy;; (* 4.12 *) (* 10: 1.896 *) test 1000 NUM_MULT_HASH_CONV xx;; (* 4: 1.69; 6: 0.716(1), 0.608(2), 8: 0.328(3) *) (* 10: 1.864 *) test 1000 raw_mul_conv_hash zz;; (* 4: 2.45(1), 1.576(2), 8: 0.320 *) needs "example0.hl";; let x = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral t1) (mk_numeral t2)) example;; let h1 = map (fun t1, t2 -> mk_binop mul_op_num (mk_numeral_array t1) (mk_numeral_array t2)) example;; let h2 = map (fun t1, t2 -> mk_binop mul_op_num (rand (mk_numeral_array t1)) (rand (mk_numeral_array t2))) example;; test 1 (map NUM_MULT_CONV) x;; (* 2.64 *) test 10 (map NUM_MULT_HASH_CONV) h1;; (* 4: 5.43; 6: 3.12; 8: 1.67 *) test 10 (map raw_mul_conv_hash) h2;; (* 5.42; 8: 1.576 *) *) (************************************) (* DIV *)
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)),
                          mk_comb(num_const, mk_binop div_op_num m_var_num n_var_num)),
                    REWRITE_TAC[num_def; NUMERAL]);;
let DIV_UNIQ' = (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[ARITH_RULE `a < b <=> (a < b:num <=> T)`] o ONCE_REWRITE_RULE[ARITH_RULE `m = q * n + r <=> q * n + r = m:num`] o REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL) DIV_UNIQ;; (* Computes m DIV n *) let raw_div_hash_conv tm = let ltm, n_tm = dest_comb tm in let m_tm = rand ltm in let m = raw_dest_hash m_tm in let n = raw_dest_hash n_tm in let q = Num.quo_num m n and r = Num.mod_num m n in let q_tm = rand (mk_numeral_array q) and r_tm = rand (mk_numeral_array r) in let qn_th = raw_mul_conv_hash (mk_binop mul_op_num q_tm n_tm) in let qn_tm = rand (concl qn_th) in let qnr_th = raw_add_conv_hash (mk_binop plus_op_num qn_tm r_tm) in let th1 = TRANS (AP_THM (AP_TERM plus_op_num qn_th) r_tm) qnr_th in let th2 = raw_lt_hash_conv (mk_binop lt_op_num r_tm n_tm) in 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 MY_PROVE_HYP th1 (MY_PROVE_HYP th2 th0);; (* The main division conversion *) let NUM_DIV_HASH_CONV tm = let ltm, rtm = dest_comb tm in let larg, rarg = rand (rand ltm), rand rtm in let th0 = INST[larg, m_var_num; rarg, n_var_num] DIV_NUM in if (rand(rator(concl th0)) <> tm) then failwith "NUM_DIV_HASH_CONV" else let rtm = rand(rand(concl th0)) in let th = raw_div_hash_conv rtm in TRANS th0 (AP_TERM num_const th);; (* let y = num_of_string "3543593547359";; let x = num_of_string "9392392983247294924242";; let xx = mk_binop div_op_num (mk_numeral_array x) (mk_numeral_array y);; let yy = mk_binop div_op_num (mk_numeral x) (mk_numeral y);; (* 1.844 *) test 100 NUM_DIV_CONV yy;; (* 10: 0.428 *) test 100 NUM_DIV_HASH_CONV xx;; *) (*********************************************) (* EVEN_CONV, ODD_CONV *) let even_const = `EVEN` and odd_const = `ODD` and eq_const = `<=>` and f_const = `F` and t_const = `T`;; let EVEN_NUM = (REWRITE_RULE[GSYM num_def] o prove) (`EVEN (NUMERAL n) <=> EVEN n`, REWRITE_TAC[NUMERAL]);; let ODD_NUM = (REWRITE_RULE[GSYM num_def] o prove) (`ODD (NUMERAL n) <=> ODD n`, REWRITE_TAC[NUMERAL]);;
let EVEN_ZERO = 
prove(`EVEN _0 <=> T`,
REWRITE_TAC[ARITH_EVEN]);;
let ODD_ZERO = 
prove(`ODD _0 <=> F`,
REWRITE_TAC[ARITH_ODD]);;
let EVEN_B0 = prove(mk_eq(mk_comb(`EVEN`, mk_comb(b0_const, `n:num`)), `T`),
		    REWRITE_TAC[B0_EXPLICIT; EVEN_MULT] THEN
		      DISJ1_TAC THEN CONV_TAC NUM_EVEN_CONV);;
let ODD_B0 = prove(mk_eq(mk_comb(`ODD`, mk_comb(b0_const, `n:num`)), `F`),
		   REWRITE_TAC[NOT_ODD; EVEN_B0]);;
let EVEN_SUC_T = 
prove(`(EVEN (SUC n) <=> T) <=> (EVEN n <=> F)`,
REWRITE_TAC[EVEN]);;
let EVEN_SUC_F = 
prove(`(EVEN (SUC n) <=> F) <=> (EVEN n <=> T)`,
REWRITE_TAC[EVEN]);;
let ODD_SUC_T = 
prove(`(ODD (SUC n) <=> T) <=> (ODD n <=> F)`,
REWRITE_TAC[ODD]);;
let ODD_SUC_F = 
prove(`(ODD (SUC n) <=> F) <=> (ODD n <=> T)`,
REWRITE_TAC[ODD]);;
let next_even_th th = let ltm, rtm = dest_comb(concl th) in let b_tm = rand(rand ltm) in let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in let flag = (fst o dest_const) rtm = "T" in let th0 = SYM (AP_TERM even_const suc_b) in let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in let th2 = INST[b_tm, n_var_num] (if flag then EVEN_SUC_F else EVEN_SUC_T) in EQ_MP (SYM (TRANS th1 th2)) th;; let next_odd_th th = let ltm, rtm = dest_comb(concl th) in let b_tm = rand(rand ltm) in let suc_b = raw_suc_conv_hash (mk_comb (suc_const, b_tm)) in let flag = (fst o dest_const) rtm = "T" in let th0 = SYM (AP_TERM odd_const suc_b) in let th1 = AP_THM (AP_TERM eq_const th0) (if flag then f_const else t_const) in let th2 = INST[b_tm, n_var_num] (if flag then ODD_SUC_F else ODD_SUC_T) in EQ_MP (SYM (TRANS th1 th2)) th;; let even_thm_table = Hashtbl.create maximum;; Hashtbl.add even_thm_table names_array.(0) EVEN_B0;; for i = 1 to maximum - 1 do let th0 = next_even_th (Hashtbl.find even_thm_table names_array.(i - 1)) in Hashtbl.add even_thm_table names_array.(i) th0 done;; let odd_thm_table = Hashtbl.create maximum;; Hashtbl.add odd_thm_table names_array.(0) ODD_B0;; for i = 1 to maximum - 1 do let th0 = next_odd_th (Hashtbl.find odd_thm_table names_array.(i - 1)) in Hashtbl.add odd_thm_table names_array.(i) th0 done;; let raw_even_hash_conv tm = let ltm, rtm = dest_comb tm in if ((fst o dest_const) ltm <> "EVEN") then failwith "raw_even_hash_conv: no EVEN" else if (is_const rtm) then EVEN_ZERO else let b_tm, n_tm = dest_comb rtm in let th0 = Hashtbl.find even_thm_table ((fst o dest_const) b_tm) in INST[n_tm, n_var_num] th0;; let raw_odd_hash_conv tm = let ltm, rtm = dest_comb tm in if ((fst o dest_const) ltm <> "ODD") then failwith "raw_odd_hash_conv: no ODD" else if (is_const rtm) then ODD_ZERO else let b_tm, n_tm = dest_comb rtm in let th0 = Hashtbl.find odd_thm_table ((fst o dest_const) b_tm) in INST[n_tm, n_var_num] th0;; let NUM_EVEN_HASH_CONV tm = let ltm, rtm = dest_comb tm in let th0 = INST[rand rtm, n_var_num] EVEN_NUM in let ltm, rtm = dest_comb(concl th0) in if (rand ltm <> tm) then failwith "NUM_EVEN_HASH_CONV" else let th1 = raw_even_hash_conv rtm in TRANS th0 th1;; let NUM_ODD_HASH_CONV tm = let ltm, rtm = dest_comb tm in let th0 = INST[rand rtm, n_var_num] ODD_NUM in let ltm, rtm = dest_comb(concl th0) in if (rand ltm <> tm) then failwith "NUM_ODD_HASH_CONV" else let th1 = raw_odd_hash_conv rtm in TRANS th0 th1;; end;;