(* ========================================================================= *)
(* Calculation with naturals.                                                *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "wf.ml";;

(* ------------------------------------------------------------------------- *)
(* Simple rule to get rid of NUMERAL constant.                               *)
(* ------------------------------------------------------------------------- *)

let DENUMERAL = GEN_REWRITE_RULE DEPTH_CONV [NUMERAL];;

(* ------------------------------------------------------------------------- *)
(* Big collection of rewrites to do trivial arithmetic.                      *)
(*                                                                           *)
(* Note that we have none for DIV and MOD, and that PRE and SUB are a bit    *)
(* inefficient; log(n)^2 instead of log(n).                                  *)
(* ------------------------------------------------------------------------- *)

let ARITH_ZERO = 
prove (`(NUMERAL 0 = 0) /\ (BIT0 _0 = _0)`,
REWRITE_TAC[NUMERAL; BIT0; DENUMERAL ADD_CLAUSES]);;
let ARITH_SUC = 
prove (`(!n. SUC(NUMERAL n) = NUMERAL(SUC n)) /\ (SUC _0 = BIT1 _0) /\ (!n. SUC (BIT0 n) = BIT1 n) /\ (!n. SUC (BIT1 n) = BIT0 (SUC n))`,
REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES]);;
let ARITH_PRE = 
prove (`(!n. PRE(NUMERAL n) = NUMERAL(PRE n)) /\ (PRE _0 = _0) /\ (!n. PRE(BIT0 n) = if n = _0 then _0 else BIT1 (PRE n)) /\ (!n. PRE(BIT1 n) = BIT0 n)`,
REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL PRE] THEN INDUCT_TAC THEN REWRITE_TAC[NUMERAL; DENUMERAL PRE; DENUMERAL ADD_CLAUSES; DENUMERAL NOT_SUC; ARITH_ZERO]);;
let ARITH_ADD = 
prove (`(!m n. NUMERAL(m) + NUMERAL(n) = NUMERAL(m + n)) /\ (_0 + _0 = _0) /\ (!n. _0 + BIT0 n = BIT0 n) /\ (!n. _0 + BIT1 n = BIT1 n) /\ (!n. BIT0 n + _0 = BIT0 n) /\ (!n. BIT1 n + _0 = BIT1 n) /\ (!m n. BIT0 m + BIT0 n = BIT0 (m + n)) /\ (!m n. BIT0 m + BIT1 n = BIT1 (m + n)) /\ (!m n. BIT1 m + BIT0 n = BIT1 (m + n)) /\ (!m n. BIT1 m + BIT1 n = BIT0 (SUC(m + n)))`,
PURE_REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES; SUC_INJ] THEN REWRITE_TAC[ADD_AC]);;
let ARITH_MULT = 
prove (`(!m n. NUMERAL(m) * NUMERAL(n) = NUMERAL(m * n)) /\ (_0 * _0 = _0) /\ (!n. _0 * BIT0 n = _0) /\ (!n. _0 * BIT1 n = _0) /\ (!n. BIT0 n * _0 = _0) /\ (!n. BIT1 n * _0 = _0) /\ (!m n. BIT0 m * BIT0 n = BIT0 (BIT0 (m * n))) /\ (!m n. BIT0 m * BIT1 n = BIT0 m + BIT0 (BIT0 (m * n))) /\ (!m n. BIT1 m * BIT0 n = BIT0 n + BIT0 (BIT0 (m * n))) /\ (!m n. BIT1 m * BIT1 n = BIT1 m + BIT0 n + BIT0 (BIT0 (m * n)))`,
PURE_REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL MULT_CLAUSES; DENUMERAL ADD_CLAUSES; SUC_INJ] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; ADD_AC]);;
let ARITH_EXP = 
prove (`(!m n. (NUMERAL m) EXP (NUMERAL n) = NUMERAL(m EXP n)) /\ (_0 EXP _0 = BIT1 _0) /\ (!m. (BIT0 m) EXP _0 = BIT1 _0) /\ (!m. (BIT1 m) EXP _0 = BIT1 _0) /\ (!n. _0 EXP (BIT0 n) = (_0 EXP n) * (_0 EXP n)) /\ (!m n. (BIT0 m) EXP (BIT0 n) = ((BIT0 m) EXP n) * ((BIT0 m) EXP n)) /\ (!m n. (BIT1 m) EXP (BIT0 n) = ((BIT1 m) EXP n) * ((BIT1 m) EXP n)) /\ (!n. _0 EXP (BIT1 n) = _0) /\ (!m n. (BIT0 m) EXP (BIT1 n) = BIT0 m * ((BIT0 m) EXP n) * ((BIT0 m) EXP n)) /\ (!m n. (BIT1 m) EXP (BIT1 n) = BIT1 m * ((BIT1 m) EXP n) * ((BIT1 m) EXP n))`,
REWRITE_TAC[NUMERAL] THEN REPEAT STRIP_TAC THEN TRY(GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [BIT0; BIT1]) THEN REWRITE_TAC[DENUMERAL EXP; DENUMERAL MULT_CLAUSES; EXP_ADD]);;
let ARITH_EVEN = 
prove (`(!n. EVEN(NUMERAL n) <=> EVEN n) /\ (EVEN _0 <=> T) /\ (!n. EVEN(BIT0 n) <=> T) /\ (!n. EVEN(BIT1 n) <=> F)`,
REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL EVEN; EVEN_ADD]);;
let ARITH_ODD = 
prove (`(!n. ODD(NUMERAL n) <=> ODD n) /\ (ODD _0 <=> F) /\ (!n. ODD(BIT0 n) <=> F) /\ (!n. ODD(BIT1 n) <=> T)`,
REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL ODD; ODD_ADD]);;
let ARITH_LE = 
prove (`(!m n. NUMERAL m <= NUMERAL n <=> m <= n) /\ ((_0 <= _0) <=> T) /\ (!n. (BIT0 n <= _0) <=> n <= _0) /\ (!n. (BIT1 n <= _0) <=> F) /\ (!n. (_0 <= BIT0 n) <=> T) /\ (!n. (_0 <= BIT1 n) <=> T) /\ (!m n. (BIT0 m <= BIT0 n) <=> m <= n) /\ (!m n. (BIT0 m <= BIT1 n) <=> m <= n) /\ (!m n. (BIT1 m <= BIT0 n) <=> m < n) /\ (!m n. (BIT1 m <= BIT1 n) <=> m <= n)`,
REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL NOT_SUC; DENUMERAL(GSYM NOT_SUC); SUC_INJ] THEN REWRITE_TAC[DENUMERAL LE_0] THEN REWRITE_TAC[DENUMERAL LE; GSYM MULT_2] THEN REWRITE_TAC[LE_MULT_LCANCEL; SUC_INJ; DENUMERAL MULT_EQ_0; DENUMERAL NOT_SUC] THEN REWRITE_TAC[DENUMERAL NOT_SUC] THEN REWRITE_TAC[LE_SUC_LT] THEN REWRITE_TAC[LT_MULT_LCANCEL] THEN SUBGOAL_THEN `2 = SUC 1` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES]; REWRITE_TAC[DENUMERAL NOT_SUC; NOT_SUC; EQ_MULT_LCANCEL] THEN REWRITE_TAC[ONCE_REWRITE_RULE[DISJ_SYM] LE_LT] THEN MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN SUBGOAL_THEN `~(SUC 1 * m = SUC (SUC 1 * n))` (fun th -> REWRITE_TAC[th]) THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN REWRITE_TAC[EVEN_MULT; EVEN_ADD; NUMERAL; BIT1; EVEN]]);;
let ARITH_LT = 
prove (`(!m n. NUMERAL m < NUMERAL n <=> m < n) /\ ((_0 < _0) <=> F) /\ (!n. (BIT0 n < _0) <=> F) /\ (!n. (BIT1 n < _0) <=> F) /\ (!n. (_0 < BIT0 n) <=> _0 < n) /\ (!n. (_0 < BIT1 n) <=> T) /\ (!m n. (BIT0 m < BIT0 n) <=> m < n) /\ (!m n. (BIT0 m < BIT1 n) <=> m <= n) /\ (!m n. (BIT1 m < BIT0 n) <=> m < n) /\ (!m n. (BIT1 m < BIT1 n) <=> m < n)`,
REWRITE_TAC[NUMERAL; GSYM NOT_LE; ARITH_LE] THEN REWRITE_TAC[DENUMERAL LE]);;
let ARITH_GE = REWRITE_RULE[GSYM GE; GSYM GT] ARITH_LE;; let ARITH_GT = REWRITE_RULE[GSYM GE; GSYM GT] ARITH_LT;;
let ARITH_EQ = 
prove (`(!m n. (NUMERAL m = NUMERAL n) <=> (m = n)) /\ ((_0 = _0) <=> T) /\ (!n. (BIT0 n = _0) <=> (n = _0)) /\ (!n. (BIT1 n = _0) <=> F) /\ (!n. (_0 = BIT0 n) <=> (_0 = n)) /\ (!n. (_0 = BIT1 n) <=> F) /\ (!m n. (BIT0 m = BIT0 n) <=> (m = n)) /\ (!m n. (BIT0 m = BIT1 n) <=> F) /\ (!m n. (BIT1 m = BIT0 n) <=> F) /\ (!m n. (BIT1 m = BIT1 n) <=> (m = n))`,
REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; ARITH_LE] THEN REWRITE_TAC[LET_ANTISYM; LTE_ANTISYM; DENUMERAL LE_0]);;
let ARITH_SUB = 
prove (`(!m n. NUMERAL m - NUMERAL n = NUMERAL(m - n)) /\ (_0 - _0 = _0) /\ (!n. _0 - BIT0 n = _0) /\ (!n. _0 - BIT1 n = _0) /\ (!n. BIT0 n - _0 = BIT0 n) /\ (!n. BIT1 n - _0 = BIT1 n) /\ (!m n. BIT0 m - BIT0 n = BIT0 (m - n)) /\ (!m n. BIT0 m - BIT1 n = PRE(BIT0 (m - n))) /\ (!m n. BIT1 m - BIT0 n = if n <= m then BIT1 (m - n) else _0) /\ (!m n. BIT1 m - BIT1 n = BIT0 (m - n))`,
REWRITE_TAC[NUMERAL; DENUMERAL SUB_0] THEN PURE_REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2; SUB_SUC; LEFT_SUB_DISTRIB] THEN REWRITE_TAC[SUB] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[DENUMERAL SUB_EQ_0] THEN RULE_ASSUM_TAC(REWRITE_RULE[NOT_LE]) THEN ASM_REWRITE_TAC[LE_SUC_LT; LT_MULT_LCANCEL; ARITH_EQ] THEN POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB] THEN REWRITE_TAC[ADD_SUB2; GSYM ADD_ASSOC]);;
let ARITH = end_itlist CONJ [ARITH_ZERO; ARITH_SUC; ARITH_PRE; ARITH_ADD; ARITH_MULT; ARITH_EXP; ARITH_EVEN; ARITH_ODD; ARITH_EQ; ARITH_LE; ARITH_LT; ARITH_GE; ARITH_GT; ARITH_SUB];; (* ------------------------------------------------------------------------- *) (* Now more delicate conversions for situations where efficiency matters. *) (* ------------------------------------------------------------------------- *) let NUM_EVEN_CONV = let tth,rths = CONJ_PAIR ARITH_EVEN in GEN_REWRITE_CONV I [tth] THENC GEN_REWRITE_CONV I [rths];; let NUM_ODD_CONV = let tth,rths = CONJ_PAIR ARITH_ODD in GEN_REWRITE_CONV I [tth] THENC GEN_REWRITE_CONV I [rths];; let NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV, NUM_LT_CONV,NUM_LE_CONV,NUM_EQ_CONV = let Comb(NUMERAL_tm,Comb(BIT0_tm,Comb(BIT1_tm,zero_tm))) = mk_small_numeral 2 and suc_tm = rator(rand(concl TWO)) and one_tm = rand(mk_small_numeral 1) and add_tm = rator(rator(lhand(snd(strip_forall(concl ADD_0))))) and mul_tm = rator(rator(rand(snd(strip_forall(concl EXP_2))))) and exp_tm = rator(rator(lhand(snd(strip_forall(concl EXP_2))))) and eq_tm = rator(rator(concl TWO)) in let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2 in let a_tm = `a:num` and b_tm = `b:num` and c_tm = `c:num` and d_tm = `d:num` and e_tm = `e:num` and h_tm = `h:num` and l_tm = `l:num` and m_tm = `m:num` and n_tm = `n:num` and p_tm = `p:num` in let STANDARDIZE = let ilist = [BIT0_tm,BIT0_tm; BIT1_tm,BIT1_tm; zero_tm,zero_tm; suc_tm,suc_tm; add_tm,add_tm; mul_tm,mul_tm; exp_tm,exp_tm; eq_tm,eq_tm; NUMERAL_tm,NUMERAL_tm; a_tm,a_tm; b_tm,b_tm; c_tm,c_tm; d_tm,d_tm; e_tm,e_tm; h_tm,h_tm; l_tm,l_tm; m_tm,m_tm; n_tm,n_tm; p_tm,p_tm] in let rec replace tm = match tm with Var(_,_) | Const(_,_) -> rev_assocd tm ilist tm | Comb(s,t) -> mk_comb(replace s,replace t) | Abs(_,_) -> failwith "replace" in fun th -> let tm' = replace (concl th) in EQ_MP (REFL tm') th in let REFL_bit0 = STANDARDIZE(REFL BIT0_tm) and REFL_bit1 = STANDARDIZE(REFL BIT1_tm) in let AP_BIT0 th = MK_COMB(REFL_bit0,th) and AP_BIT1 th = MK_COMB(REFL_bit1,th) and QUICK_PROVE_HYP ath bth = EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath in let rec dest_raw_numeral tm = match tm with Comb(Const("BIT1",_),t) -> num_2 */ dest_raw_numeral t +/ num_1 | Comb(Const("BIT0",_),t) -> num_2 */ dest_raw_numeral t | Const("_0",_) -> num_0 in let bitcounts = let rec bctr w z tm = match tm with Const("_0",_) -> (w,z) | Comb(Const("BIT0",_),t) -> bctr w (z + 1) t | Comb(Const("BIT1",_),t) -> bctr (w + 1) z t | _ -> failwith "malformed numeral" in bctr 0 0 in let rec wellformed tm = match tm with Const("_0",_) -> true | Comb(Const("BIT0",_),t)|Comb(Const("BIT1",_),t) -> wellformed t | _ -> false in let rec orderrelation mtm ntm = if mtm == ntm then if wellformed mtm then 0 else failwith "orderrelation" else match (mtm,ntm) with Const("_0",_),Const("_0",_) -> 0 | Const("_0",_),_ -> if wellformed ntm then -1 else failwith "orderrelation" | _, Const("_0",_) -> if wellformed ntm then 1 else failwith "orderrelation" | Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt) | Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt) -> orderrelation mt nt | Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt) -> if orderrelation mt nt > 0 then 1 else -1 | Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt) -> if orderrelation mt nt < 0 then -1 else 1 in let doublebn tm = if tm = zero_tm then tm else mk_comb(BIT0_tm,tm) in let rec subbn mtm ntm = match (mtm,ntm) with (_,Const("_0",_)) -> mtm | (Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt)) -> doublebn (subbn mt nt) | (Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt)) -> doublebn (subbn mt nt) | (Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt)) -> mk_comb(BIT1_tm,subbn mt nt) | (Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt)) -> mk_comb(BIT1_tm,sbcbn mt nt) | _ -> failwith "malformed numeral or wrong relation" and sbcbn mtm ntm = match (mtm,ntm) with | (Comb(Const("BIT0",_),mt),Const("_0",_)) -> mk_comb(BIT1_tm,sbcbn mt ntm) | (Comb(Const("BIT1",_),mt),Const("_0",_)) -> doublebn mt | (Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt)) -> mk_comb(BIT1_tm,sbcbn mt nt) | (Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt)) -> mk_comb(BIT1_tm,sbcbn mt nt) | (Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt)) -> doublebn (subbn mt nt) | (Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt)) -> doublebn (sbcbn mt nt) | _ -> failwith "malformed numeral or wrong relation" in let topsplit tm = match tm with Const("_0",_) -> 0,zero_tm | Comb(Const("BIT1",_),Const("_0",_)) -> 1,zero_tm | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_))) -> 2,zero_tm | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_))) -> 3,zero_tm | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 4,zero_tm | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 5,zero_tm | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 6,zero_tm | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 7,zero_tm | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 0,n | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 1,n | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 2,n | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 3,n | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 4,n | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 5,n | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 6,n | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 7,n | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 8,n | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 9,n | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 10,n | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 11,n | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 12,n | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 13,n | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 14,n | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 15,n | _ -> failwith "malformed numeral" in let NUM_ADD_RULE,NUM_ADC_RULE = let rec mk_compnumeral k base = if k = 0 then base else let t = mk_compnumeral (k / 2) base in if k mod 2 = 1 then mk_comb(BIT1_tm,t) else mk_comb(BIT0_tm,t) in let bases v = let part2 = map (fun k -> mk_compnumeral k v) (8--15) in let part1 = map (subst[mk_comb(BIT0_tm,v),mk_comb(BIT1_tm,v)]) part2 and part0 = map (fun k -> mk_compnumeral k zero_tm) (0--15) in part0 @ part1 @ part2 in let starts = allpairs (fun mtm ntm -> mk_comb(mk_comb(add_tm,mtm),ntm)) (bases m_tm) (bases n_tm) in let BITS_INJ = (STANDARDIZE o prove) (`(BIT0 m = BIT0 n <=> m = n) /\ (BIT1 m = BIT1 n <=> m = n)`, REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ]) in let ARITH_0 = (STANDARDIZE o MESON[NUMERAL; ADD_CLAUSES]) `m + _0 = m /\ _0 + n = n` in let patadj = subst[`SUC(m + _0)`,`SUC m`; `SUC(_0 + n)`,`SUC n`] in let mkclauses sucflag t = let tm = if sucflag then mk_comb(suc_tm,t) else t in let th1 = PURE_REWRITE_CONV[ARITH_ADD; ARITH_SUC; ARITH_0] tm in let tm1 = patadj(rand(concl th1)) in if not(free_in add_tm tm1) then th1, (if free_in m_tm tm1 then 0 else 1) else let ptm = rand(rand(rand(rand tm1))) in let tmc = mk_eq(mk_eq(ptm,p_tm),mk_eq(tm,subst[p_tm,ptm] tm1)) in EQT_ELIM(REWRITE_CONV[ARITH_ADD; ARITH_SUC; ARITH_0; BITS_INJ] tmc), (if free_in suc_tm tm1 then 3 else 2) in let add_clauses,add_flags = let l1,l2 = unzip(map (mkclauses false) starts) in Array.of_list(map STANDARDIZE l1),Array.of_list l2 in let adc_clauses,adc_flags = let l1,l2 = unzip(map (mkclauses true) starts) in Array.of_list(map STANDARDIZE l1),Array.of_list l2 in let rec NUM_ADD_RULE mtm ntm = let m_lo,m_hi = topsplit mtm and n_lo,n_hi = topsplit ntm in let m_ind = if m_hi = zero_tm then m_lo else m_lo + 16 and n_ind = if n_hi = zero_tm then n_lo else n_lo + 16 in let ind = 32 * m_ind + n_ind in let th1 = Array.get add_clauses ind and fl = Array.get add_flags ind in match fl with 0 -> INST [m_hi,m_tm] th1 | 1 -> INST [n_hi,n_tm] th1 | 2 -> let th2 = NUM_ADD_RULE m_hi n_hi in (match concl th2 with Comb(_,ptm) -> let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in EQ_MP th3 th2) | 3 -> let th2 = NUM_ADC_RULE m_hi n_hi in (match concl th2 with Comb(_,ptm) -> let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in EQ_MP th3 th2) and NUM_ADC_RULE mtm ntm = let m_lo,m_hi = topsplit mtm and n_lo,n_hi = topsplit ntm in let m_ind = if m_hi = zero_tm then m_lo else m_lo + 16 and n_ind = if n_hi = zero_tm then n_lo else n_lo + 16 in let ind = 32 * m_ind + n_ind in let th1 = Array.get adc_clauses ind and fl = Array.get adc_flags ind in match fl with 0 -> INST [m_hi,m_tm] th1 | 1 -> INST [n_hi,n_tm] th1 | 2 -> let th2 = NUM_ADD_RULE m_hi n_hi in (match concl th2 with Comb(_,ptm) -> let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in EQ_MP th3 th2) | 3 -> let th2 = NUM_ADC_RULE m_hi n_hi in (match concl th2 with Comb(_,ptm) -> let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in EQ_MP th3 th2) in NUM_ADD_RULE,NUM_ADC_RULE in let NUM_SHIFT_CONV = let pth_0 = (STANDARDIZE o prove) (`(n = a + p * b <=> BIT0 n = BIT0 a + BIT0 p * b)`, REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) and pth_z = (STANDARDIZE o prove) (`n = _0 + p * b <=> BIT0 n = _0 + BIT0 p * b`, SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN REWRITE_TAC[BIT1; BIT0] THEN REWRITE_TAC[ADD_CLAUSES; GSYM MULT_2] THEN REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; ARITH_EQ]) and pth_1 = (STANDARDIZE o prove) (`(n = a + p * b <=> BIT1 n = BIT1 a + BIT0 p * b)`, REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB; ADD_CLAUSES; SUC_INJ] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) and pth_base = (STANDARDIZE o prove) (`n = _0 + BIT1 _0 * n`, MESON_TAC[ADD_CLAUSES; MULT_CLAUSES; NUMERAL]) and pth_triv = (STANDARDIZE o prove) (`_0 = a + p * b <=> _0 = a + BIT0 p * b`, CONV_TAC(BINOP_CONV SYM_CONV) THEN SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN REWRITE_TAC[ADD_EQ_0; MULT_EQ_0; BIT0]) and pths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove) (`(n = a + p * b <=> BIT0(BIT0(BIT0(BIT0 n))) = BIT0(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT0(BIT0(BIT0 n))) = BIT1(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT1(BIT0(BIT0 n))) = BIT0(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT1(BIT0(BIT0 n))) = BIT1(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT0(BIT1(BIT0 n))) = BIT0(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT0(BIT1(BIT0 n))) = BIT1(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT1(BIT1(BIT0 n))) = BIT0(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT1(BIT1(BIT0 n))) = BIT1(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT0(BIT0(BIT1 n))) = BIT0(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT0(BIT0(BIT1 n))) = BIT1(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT1(BIT0(BIT1 n))) = BIT0(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT1(BIT0(BIT1 n))) = BIT1(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT0(BIT1(BIT1 n))) = BIT0(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT0(BIT1(BIT1 n))) = BIT1(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT0(BIT1(BIT1(BIT1 n))) = BIT0(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = a + p * b <=> BIT1(BIT1(BIT1(BIT1 n))) = BIT1(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b)`, MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN ABBREV_TAC `two = 2` THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ; GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC]) and pths_0 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove) (`(n = _0 + p * b <=> BIT0(BIT0(BIT0(BIT0 n))) = _0 + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT0(BIT0(BIT0 n))) = BIT1 _0 + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT1(BIT0(BIT0 n))) = BIT0(BIT1 _0) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT1(BIT0(BIT0 n))) = BIT1(BIT1 _0) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT0(BIT1(BIT0 n))) = BIT0(BIT0(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT0(BIT1(BIT0 n))) = BIT1(BIT0(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT1(BIT1(BIT0 n))) = BIT0(BIT1(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT1(BIT1(BIT0 n))) = BIT1(BIT1(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT0(BIT0(BIT1 n))) = BIT0(BIT0(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT0(BIT0(BIT1 n))) = BIT1(BIT0(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT1(BIT0(BIT1 n))) = BIT0(BIT1(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT1(BIT0(BIT1 n))) = BIT1(BIT1(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT0(BIT1(BIT1 n))) = BIT0(BIT0(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT0(BIT1(BIT1 n))) = BIT1(BIT0(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT0(BIT1(BIT1(BIT1 n))) = BIT0(BIT1(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\ (n = _0 + p * b <=> BIT1(BIT1(BIT1(BIT1 n))) = BIT1(BIT1(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b)`, SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN ABBREV_TAC `two = 2` THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ; GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC]) in let rec NUM_SHIFT_CONV k tm = if k <= 0 then INST [tm,n_tm] pth_base else match tm with Comb(_,Comb(_,Comb(_,Comb(_,_)))) when k >= 4 -> let i,ntm = topsplit tm in let th1 = NUM_SHIFT_CONV (k - 4) ntm in (match concl th1 with Comb(_,Comb(Comb(_,Const("_0",_)),Comb(Comb(_,ptm),btm))) -> let th2 = Array.get pths_0 i in let th3 = INST [ntm,n_tm; btm,b_tm; ptm,p_tm] th2 in EQ_MP th3 th1 | Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) -> let th2 = Array.get pths_1 i in let th3 = INST[ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] th2 in EQ_MP th3 th1) | Comb(Const("BIT0",_),ntm) -> let th1 = NUM_SHIFT_CONV (k - 1) ntm in (match concl th1 with Comb(_,Comb(Comb(_,Const("_0",_)),Comb(Comb(_,ptm),btm))) -> EQ_MP (INST [ntm,n_tm; btm,b_tm; ptm,p_tm] pth_z) th1 | Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) -> EQ_MP (INST[ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] pth_0) th1) | Comb(Const("BIT1",_),ntm) -> let th1 = NUM_SHIFT_CONV (k - 1) ntm in (match concl th1 with Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) -> EQ_MP (INST [ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] pth_1) th1) | Const("_0",_) -> let th1 = NUM_SHIFT_CONV (k - 1) tm in (match concl th1 with Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) -> EQ_MP (INST [atm,a_tm; btm,b_tm; ptm,p_tm] pth_triv) th1) | _ -> failwith "malformed numeral" in NUM_SHIFT_CONV in let NUM_UNSHIFT_CONV = let pth_triv = (STANDARDIZE o prove) (`a + p * _0 = a`, SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]) and pth_base = (STANDARDIZE o prove) (`a + BIT1 _0 * b = a + b`, SUBST1_TAC(SYM(SPEC `BIT1 _0` NUMERAL)) THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]) and pth_0 = (STANDARDIZE o prove) (`BIT0 a + BIT0 p * b = BIT0(a + p * b)`, REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB]) and pth_1 = (STANDARDIZE o prove) (`BIT1 a + BIT0 p * b = BIT1(a + p * b)`, REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ] THEN REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) and pth_z = (STANDARDIZE o prove) (`_0 + BIT0 p * b = BIT0(_0 + p * b)`, SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN REWRITE_TAC[BIT1; BIT0] THEN REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB]) and puths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove) (`(a + p * b = n <=> BIT0(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT0(BIT0(BIT0 n)))) /\ (a + p * b = n <=> BIT1(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT0(BIT0(BIT0 n)))) /\ (a + p * b = n <=> BIT0(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT1(BIT0(BIT0 n)))) /\ (a + p * b = n <=> BIT1(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT1(BIT0(BIT0 n)))) /\ (a + p * b = n <=> BIT0(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT0(BIT1(BIT0 n)))) /\ (a + p * b = n <=> BIT1(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT0(BIT1(BIT0 n)))) /\ (a + p * b = n <=> BIT0(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT1(BIT1(BIT0 n)))) /\ (a + p * b = n <=> BIT1(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT1(BIT1(BIT0 n)))) /\ (a + p * b = n <=> BIT0(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT0(BIT0(BIT1 n)))) /\ (a + p * b = n <=> BIT1(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT0(BIT0(BIT1 n)))) /\ (a + p * b = n <=> BIT0(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT1(BIT0(BIT1 n)))) /\ (a + p * b = n <=> BIT1(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT1(BIT0(BIT1 n)))) /\ (a + p * b = n <=> BIT0(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT0(BIT1(BIT1 n)))) /\ (a + p * b = n <=> BIT1(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT0(BIT1(BIT1 n)))) /\ (a + p * b = n <=> BIT0(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT0(BIT1(BIT1(BIT1 n)))) /\ (a + p * b = n <=> BIT1(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b = BIT1(BIT1(BIT1(BIT1 n))))`, SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN ABBREV_TAC `two = 2` THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ; GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC]) in let puths_2 = Array.of_list (map (fun i -> let th1 = Array.get puths_1 (i mod 16) and th2 = Array.get puths_1 (i / 16) in let th3 = GEN_REWRITE_RULE RAND_CONV [th1] th2 in STANDARDIZE th3) (0--255)) in let rec NUM_UNSHIFT_CONV tm = match tm with Comb(Comb(Const("+",_),atm),Comb(Comb(Const("*",_),ptm),btm)) -> (match (atm,ptm,btm) with (_,_,Const("_0",_)) -> INST [atm,a_tm; ptm,p_tm] pth_triv | (_,Comb(Const("BIT1",_),Const("_0",_)),_) -> let th1 = INST [atm,a_tm; btm,b_tm] pth_base in let Comb(_,Comb(Comb(_,mtm),ntm)) = concl th1 in TRANS th1 (NUM_ADD_RULE mtm ntm) | (Comb(_,Comb(_,Comb(_,Comb(_,atm')))), Comb(_,Comb(_,Comb(_,Comb(_,(Comb(_,_) as ptm'))))),_) -> let i,_ = topsplit atm in (match (atm',ptm') with (Comb(_,Comb(_,Comb(_,Comb(_,atm'')))), Comb(_,Comb(_,Comb(_,Comb(_,(Comb(_,_) as ptm'')))))) -> let j,_ = topsplit atm' in let tm' = mk_comb(mk_comb(add_tm,atm''), mk_comb(mk_comb(mul_tm,ptm''),btm)) in let th1 = NUM_UNSHIFT_CONV tm' in let th2 = INST [atm'',a_tm; ptm'',p_tm; btm,b_tm; rand(concl th1),n_tm] (Array.get puths_2 (16 * j + i)) in EQ_MP th2 th1 | _ -> let tm' = mk_comb(mk_comb(add_tm,atm'), mk_comb(mk_comb(mul_tm,ptm'),btm)) in let th1 = NUM_UNSHIFT_CONV tm' in let th2 = INST [atm',a_tm; ptm',p_tm; btm,b_tm; rand(concl th1),n_tm] (Array.get puths_1 i) in EQ_MP th2 th1) | (Const("_0",_),Comb(Const("BIT0",_),qtm),_) -> let th1 = INST [btm,b_tm; qtm,p_tm] pth_z in CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1 | (Comb(Const("BIT0",_),ctm),Comb(Const("BIT0",_),qtm),_) -> let th1 = INST [ctm,a_tm; btm,b_tm; qtm,p_tm] pth_0 in CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1 | (Comb(Const("BIT1",_),ctm),Comb(Const("BIT0",_),qtm),_) -> let th1 = INST [ctm,a_tm; btm,b_tm; qtm,p_tm] pth_1 in CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1 | _ -> failwith "malformed numeral") | _ -> failwith "malformed numeral" in NUM_UNSHIFT_CONV in let NUM_SQUARE_RULE = let pth_0 = (STANDARDIZE o prove) (`_0 EXP 2 = _0`, MESON_TAC[NUMERAL; REWRITE_CONV[ARITH] `0 EXP 2`]) and pth_1 = (STANDARDIZE o prove) (`(BIT1 _0) EXP 2 = BIT1 _0`, MESON_TAC[NUMERAL; REWRITE_CONV[ARITH] `1 EXP 2`]) and pth_even = (STANDARDIZE o prove) (`m EXP 2 = n <=> (BIT0 m) EXP 2 = BIT0(BIT0 n)`, ABBREV_TAC `two = 2` THEN REWRITE_TAC[BIT0] THEN EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[EXP_2] THEN REWRITE_TAC[AC MULT_AC `(2 * m) * (2 * n) = 2 * 2 * m * n`] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) and pth_odd = (STANDARDIZE o prove) (`m EXP 2 = n <=> (BIT1 m) EXP 2 = BIT1(BIT0(m + n))`, ABBREV_TAC `two = 2` THEN REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN REWRITE_TAC[SUC_INJ; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN REWRITE_TAC[AC ADD_AC `(m + m * 2 * m) + m = m * 2 * m + m + m`] THEN REWRITE_TAC[GSYM MULT_2; AC MULT_AC `m * 2 * m = 2 * m * m`] THEN REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ADD_SYM] THEN REWRITE_TAC[EQ_ADD_RCANCEL]) and pth_qstep = (UNDISCH o STANDARDIZE o prove) (`n + BIT1 _0 = m /\ m EXP 2 = p /\ m + a = BIT0(BIT0 p) ==> (BIT1(BIT1(BIT1 n))) EXP 2 = BIT1(BIT0(BIT0(BIT0 a)))`, ABBREV_TAC `two = 2` THEN SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN REWRITE_TAC[BIT1; BIT0] THEN EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB; GSYM ADD_ASSOC] THEN REWRITE_TAC[MULT_ASSOC] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_TAC THEN MATCH_MP_TAC(MESON[EQ_ADD_LCANCEL] `!m:num. m + n = m + p ==> n = p`) THEN EXISTS_TAC `16 * (n + 1)` THEN ASM_REWRITE_TAC[ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN EXPAND_TAC "two" THEN REWRITE_TAC[EXP_2] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_CLAUSES; MULT_ASSOC] THEN REWRITE_TAC[AC MULT_AC `(8 * n) * NUMERAL p = (8 * NUMERAL p) * n`] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[AC ADD_AC `(n + 16) + p + q + 49 = (n + p + q) + (16 + 49)`] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[ADD_ASSOC; EQ_ADD_RCANCEL] THEN REWRITE_TAC[GSYM ADD_ASSOC; GSYM MULT_2; MULT_ASSOC] THEN ONCE_REWRITE_TAC[AC ADD_AC `a + b + c:num = b + a + c`] THEN REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[ARITH]) and pth_rec = (UNDISCH o STANDARDIZE o prove) (`n = l + p * h /\ h + l = m /\ h EXP 2 = a /\ l EXP 2 = c /\ m EXP 2 = d /\ a + c = e /\ e + b = d ==> n EXP 2 = c + p * (b + p * a)`, REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN SUBST1_TAC THEN REPLICATE_TAC 5 (DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC] THEN CONV_TAC(BINOP_CONV NUM_CANCEL_CONV) THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]) and pth_toom3 = (STANDARDIZE o prove) (`h EXP 2 = e /\ l EXP 2 = a /\ (l + BIT1 _0 * (m + BIT1 _0 * h)) EXP 2 = a + BIT1 _0 * (b + BIT1 _0 * (c + BIT1 _0 * (d + BIT1 _0 * e))) /\ (l + BIT0(BIT1 _0) * (m + BIT0(BIT1 _0) * h)) EXP 2 = a + BIT0(BIT1 _0) * (b + BIT0(BIT1 _0) * (c + BIT0(BIT1 _0) * (d + BIT0(BIT1 _0) * e))) /\ (h + BIT0(BIT1 _0) * (m + BIT0(BIT1 _0) * l)) EXP 2 = e + BIT0(BIT1 _0) * (d + BIT0(BIT1 _0) * (c + BIT0(BIT1 _0) * (b + BIT0(BIT1 _0) * a))) ==> (l + p * (m + p * h)) EXP 2 = a + p * (b + p * (c + p * (d + p * e)))`, ABBREV_TAC `two = 2` THEN SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN REWRITE_TAC[BIT1; BIT0] THEN EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[ARITH] THEN SUBGOAL_THEN `!p x y z. (x + p * (y + p * z)) EXP 2 = x * x + p * (2 * x * y + p * ((2 * x * z + y * y) + p * (2 * y * z + p * z * z)))` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[EXP_2; MULT_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]; REWRITE_TAC[EXP_2]] THEN MAP_EVERY ABBREV_TAC [`a':num = l * l`; `b' = 2 * l * m`; `c' = 2 * l * h + m * m`; `d' = 2 * m * h`; `e':num = h * h`] THEN SUBST1_TAC(AC MULT_AC `2 * m * l = 2 * l * m`) THEN SUBST1_TAC(AC MULT_AC `2 * h * l = 2 * l * h`) THEN SUBST1_TAC(AC MULT_AC `2 * h * m = 2 * m * h`) THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "two" THEN POP_ASSUM_LIST(K ALL_TAC) THEN ASM_CASES_TAC `a':num = a` THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `e':num = e` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(K ALL_TAC) THEN REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN REWRITE_TAC[ADD_ASSOC; EQ_ADD_RCANCEL] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[] `b = b' /\ c = c' /\ d = d' ==> 5 * b + c' + d' = 5 * b' + c + d`)) THEN REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN REWRITE_TAC(map (fun k -> SYM(REWRITE_CONV[ARITH_SUC] (mk_comb(suc_tm,mk_small_numeral(k - 1))))) (1--5)) THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN CONV_TAC(LAND_CONV NUM_CANCEL_CONV) THEN DISCH_THEN SUBST_ALL_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[] `b = b' /\ c = c' /\ d = d' ==> b + d':num = b' + d /\ 4 * b + d' = 4 * b' + d`)) THEN REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN REWRITE_TAC(map (fun k -> SYM(REWRITE_CONV[ARITH_SUC] (mk_comb(suc_tm,mk_small_numeral(k - 1))))) (1--4)) THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN CONV_TAC(LAND_CONV(BINOP_CONV NUM_CANCEL_CONV)) THEN REWRITE_TAC[GSYM MULT_2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM(el 4 (CONJUNCTS MULT_CLAUSES))] THEN SIMP_TAC[EQ_MULT_LCANCEL; NOT_SUC]) and pth_even3 = (STANDARDIZE o prove) (`m EXP 2 = n <=> (BIT0(BIT0(BIT0 m))) EXP 2 = BIT0(BIT0(BIT0(BIT0(BIT0(BIT0 n)))))`, ABBREV_TAC `two = 2` THEN REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN EXPAND_TAC "two" THEN REWRITE_TAC[EXP_2] THEN REWRITE_TAC[AC MULT_AC `(2 * 2 * 2 * m) * 2 * 2 * 2 * m = 2 * 2 * 2 * 2 * 2 * 2 * m * m`] THEN REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) in let NUM_UNSHIFT2_CONV = RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV) THENC NUM_UNSHIFT_CONV in let NUM_UNSHIFT3_CONV = RAND_CONV(RAND_CONV NUM_UNSHIFT2_CONV) THENC NUM_UNSHIFT_CONV in let NUM_UNSHIFT4_CONV = RAND_CONV(RAND_CONV NUM_UNSHIFT3_CONV) THENC NUM_UNSHIFT_CONV in let BINOP2_CONV conv1 conv2 = COMB2_CONV (RAND_CONV conv1) conv2 in let TOOM3_CONV = BINOP2_CONV (LAND_CONV NUM_UNSHIFT2_CONV) NUM_UNSHIFT4_CONV in let rec GEN_NUM_SQUARE_RULE w z tm = match tm with Const("_0",_) -> pth_0 | Comb(Const("BIT0",_),mtm) -> (match mtm with Comb(Const("BIT0",_),Comb(Const("BIT0",_),ptm)) -> let th1 = GEN_NUM_SQUARE_RULE w (z - 3) ptm in let ntm = rand(concl th1) in EQ_MP (INST [ptm,m_tm; ntm,n_tm] pth_even3) th1 | _ -> let th1 = GEN_NUM_SQUARE_RULE w (z - 1) mtm in let ntm = rand(concl th1) in EQ_MP (INST [mtm,m_tm; ntm,n_tm] pth_even) th1) | Comb(Const("BIT1",_),mtm) -> if mtm = zero_tm then pth_1 else if (w < 100 or z < 20) & w + z < 150 then match mtm with Comb(Const("BIT1",_),Comb(Const("BIT1",_),ntm)) -> let th1 = NUM_ADD_RULE ntm one_tm in let mtm = rand(concl th1) in let th2 = NUM_SQUARE_RULE mtm in let ptm = rand(concl th2) in let atm = subbn (mk_comb(BIT0_tm,mk_comb(BIT0_tm,ptm))) mtm in let th3 = NUM_ADD_RULE mtm atm in let th4 = INST [atm,a_tm; mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_qstep in QUICK_PROVE_HYP (CONJ th1 (CONJ th2 th3)) th4 | _ -> let th1 = GEN_NUM_SQUARE_RULE (w - 1) z mtm in let ntm = rand(concl th1) in let th2 = EQ_MP (INST [mtm,m_tm; ntm,n_tm] pth_odd) th1 in (match concl th2 with Comb(_,Comb(_,Comb(_,Comb(Comb(_,ptm),qtm)))) -> let th3 = NUM_ADD_RULE ptm qtm in TRANS th2 (AP_BIT1 (AP_BIT0 th3))) else if w + z < 800 then let k2 = (w + z) / 2 in let th1 = NUM_SHIFT_CONV k2 tm in let Comb(Comb(_,ltm),Comb(Comb(_,ptm),htm)) = rand(concl th1) in let th2 = NUM_ADD_RULE htm ltm in let mtm = rand(concl th2) in let th3 = NUM_SQUARE_RULE htm and th4 = NUM_SQUARE_RULE ltm and th5 = NUM_SQUARE_RULE mtm in let atm = rand(concl th3) and ctm = rand(concl th4) and dtm = rand(concl th5) in let th6 = NUM_ADD_RULE atm ctm in let etm = rand(concl th6) in let btm = subbn dtm etm in let th7 = NUM_ADD_RULE etm btm in let dtm = rand(concl th7) in let th8 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; etm,e_tm; htm,h_tm; ltm,l_tm; mtm,m_tm; tm,n_tm; ptm,p_tm] pth_rec in let th9 = QUICK_PROVE_HYP (end_itlist CONJ [th1;th2;th3;th4;th5;th6;th7]) th8 in CONV_RULE(RAND_CONV(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV) THENC NUM_UNSHIFT_CONV)) th9 else let k3 = (w + z) / 3 in let th0 = (NUM_SHIFT_CONV k3 THENC RAND_CONV(RAND_CONV(NUM_SHIFT_CONV k3))) tm in let Comb(Comb(_,ltm),Comb(Comb(_,ptm), Comb(Comb(_,mtm),Comb(Comb(_,_),htm)))) = rand(concl th0) in let th1 = NUM_SQUARE_RULE htm and th2 = NUM_SQUARE_RULE ltm in let atm = rand(concl th2) and etm = rand(concl th1) in let lnum = dest_raw_numeral ltm and mnum = dest_raw_numeral mtm and hnum = dest_raw_numeral htm in let btm = rand(mk_numeral(num_2 */ lnum */ mnum)) and ctm = rand(mk_numeral(mnum */ mnum +/ num_2 */ lnum */ hnum)) and dtm = rand(mk_numeral(num_2 */ hnum */ mnum)) in let th = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; etm,e_tm; htm,h_tm; mtm,m_tm; ltm,l_tm; ptm,p_tm] pth_toom3 in let th' = CONV_RULE (BINOP2_CONV (RAND_CONV(RAND_CONV (BINOP2_CONV TOOM3_CONV (BINOP2_CONV TOOM3_CONV TOOM3_CONV)))) TOOM3_CONV) th in let [tm3;tm4;tm5] = conjuncts(rand(rand(lhand(concl th')))) in let th3 = NUM_SQUARE_RULE (lhand(lhand tm3)) and th4 = NUM_SQUARE_RULE (lhand(lhand tm4)) and th5 = NUM_SQUARE_RULE (lhand(lhand tm5)) in MP th' (end_itlist CONJ [th1;th2;th3;th4;th5]) and NUM_SQUARE_RULE tm = let w,z = bitcounts tm in GEN_NUM_SQUARE_RULE w z tm in NUM_SQUARE_RULE in let NUM_MUL_RULE = let QUICK_PROVE_HYP ath bth = EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath and pth_0l,pth_0r = (CONJ_PAIR o STANDARDIZE o prove) (`_0 * n = _0 /\ m * _0 = _0`, MESON_TAC[NUMERAL; MULT_CLAUSES]) and pth_1l,pth_1r = (CONJ_PAIR o STANDARDIZE o prove) (`(BIT1 _0) * n = n /\ m * (BIT1 _0) = m`, MESON_TAC[NUMERAL; MULT_CLAUSES]) and pth_evenl,pth_evenr = (CONJ_PAIR o STANDARDIZE o prove) (`(m * n = p <=> (BIT0 m) * n = BIT0 p) /\ (m * n = p <=> m * BIT0 n = BIT0 p)`, REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[AC MULT_AC `m * 2 * n = 2 * m * n`] THEN REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; ARITH_EQ]) and pth_oddl,pth_oddr = (CONJ_PAIR o STANDARDIZE o prove) (`(m * n = p <=> BIT1 m * n = BIT0 p + n) /\ (m * n = p <=> m * BIT1 n = BIT0 p + m)`, REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[MULT_CLAUSES] THEN REWRITE_TAC[MESON[MULT_AC; ADD_SYM] `m + m * 2 * n = 2 * m * n + m`] THEN REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; EQ_ADD_RCANCEL] THEN REWRITE_TAC[ARITH_EQ]) in let pth_oo1 = (UNDISCH_ALL o STANDARDIZE o prove) (`n + p = m /\ SUC(m + n) = a /\ p EXP 2 = b /\ a EXP 2 = c /\ b + d = c ==> ((BIT1 m) * (BIT1 n) = d)`, ABBREV_TAC `two = 2` THEN REWRITE_TAC[BIT1; IMP_CONJ] THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[EXP_2; GSYM MULT_2] THEN REPLICATE_TAC 4 (DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[ADD1; AC ADD_AC `((n + p) + n) + 1 = (p + (n + n)) + 1`] THEN REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[GSYM ADD_ASSOC; MULT_CLAUSES; EQ_ADD_LCANCEL] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[MULT_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]) in let pth_oo2 = PURE_ONCE_REWRITE_RULE[MULT_SYM] (INST [n_tm,m_tm; m_tm,n_tm] pth_oo1) in let pth_recodel = (UNDISCH_ALL o STANDARDIZE o prove) (`SUC(_0 + m) = p ==> (p * n = a + n <=> m * n = a)`, SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; EQ_ADD_RCANCEL]) and pth_recoder = (UNDISCH_ALL o STANDARDIZE o prove) (`SUC(_0 + n) = p ==> (m * p = a + m <=> m * n = a)`, ONCE_REWRITE_TAC[MULT_SYM] THEN SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; EQ_ADD_RCANCEL]) in let rec NUM_MUL_RULE k l tm tm' = match (tm,tm') with (Const("_0",_),_) -> INST [tm',n_tm] pth_0l | (_,Const("_0",_)) -> INST [tm,m_tm] pth_0r | (Comb(Const("BIT1",_),Const("_0",_)),_) -> INST [tm',n_tm] pth_1l | (_,Comb(Const("BIT1",_),Const("_0",_))) -> INST [tm,m_tm] pth_1r | (Comb(Const("BIT0",_),mtm),_) -> let th0 = NUM_MUL_RULE (k - 1) l mtm tm' in let th1 = INST [mtm,m_tm; tm',n_tm; rand(concl th0),p_tm] pth_evenl in EQ_MP th1 th0 | (_,Comb(Const("BIT0",_),ntm)) -> let th0 = NUM_MUL_RULE k (l - 1) tm ntm in let th1 = INST [tm,m_tm; ntm,n_tm; rand(concl th0),p_tm] pth_evenr in EQ_MP th1 th0 | (Comb(Const("BIT1",_),mtm),Comb(Const("BIT1",_),ntm)) -> if k <= 50 or l <= 50 or Int k */ Int k <=/ Int l or Int l */ Int l <= Int k then match (mtm,ntm) with (Comb(Const("BIT1",_),Comb(Const("BIT1",_),_)),_) -> let th1 = NUM_ADC_RULE zero_tm tm in let ptm = rand(concl th1) in let th2 = NUM_MUL_RULE k l ptm tm' in let atm = subbn (rand(concl th2)) tm' in let th3 = INST [tm,m_tm; tm',n_tm; ptm,p_tm; atm,a_tm] pth_recodel in let th4 = PROVE_HYP th1 th3 in EQ_MP th4 (TRANS th2 (SYM(NUM_ADD_RULE atm tm'))) | (_,Comb(Const("BIT1",_),Comb(Const("BIT1",_),_))) -> let th1 = NUM_ADC_RULE zero_tm tm' in let ptm = rand(concl th1) in let th2 = NUM_MUL_RULE k l tm ptm in let atm = subbn (rand(concl th2)) tm in let th3 = INST [tm,m_tm; tm',n_tm; ptm,p_tm; atm,a_tm] pth_recoder in let th4 = PROVE_HYP th1 th3 in EQ_MP th4 (TRANS th2 (SYM(NUM_ADD_RULE atm tm))) | _ -> if k <= l then let th0 = NUM_MUL_RULE (k - 1) l mtm tm' in let ptm = rand(concl th0) in let th1 = EQ_MP (INST [mtm,m_tm; tm',n_tm; ptm,p_tm] pth_oddl) th0 in let tm1 = lhand(rand(concl th1)) in TRANS th1 (NUM_ADD_RULE tm1 tm') else let th0 = NUM_MUL_RULE k (l - 1) tm ntm in let ptm = rand(concl th0) in let th1 = EQ_MP (INST [tm,m_tm; ntm,n_tm; ptm,p_tm] pth_oddr) th0 in let tm1 = lhand(rand(concl th1)) in TRANS th1 (NUM_ADD_RULE tm1 tm) else let mval = dest_raw_numeral mtm and nval = dest_raw_numeral ntm in if nval <=/ mval then let ptm = rand(mk_numeral(mval -/ nval)) in let th2 = NUM_ADD_RULE ntm ptm and th3 = NUM_ADC_RULE mtm ntm in let atm = rand(concl th3) in let th4 = NUM_SQUARE_RULE ptm in let btm = rand(concl th4) in let th5 = NUM_SQUARE_RULE atm in let ctm = rand(concl th5) in let dtm = subbn ctm btm in let th6 = NUM_ADD_RULE btm dtm in let th1 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_oo1 in QUICK_PROVE_HYP (end_itlist CONJ [th2;th3;th4;th5;th6]) th1 else let ptm = rand(mk_numeral(nval -/ mval)) in let th2 = NUM_ADD_RULE mtm ptm and th3 = NUM_ADC_RULE ntm mtm in let atm = rand(concl th3) in let th4 = NUM_SQUARE_RULE ptm in let btm = rand(concl th4) in let th5 = NUM_SQUARE_RULE atm in let ctm = rand(concl th5) in let dtm = subbn ctm btm in let th6 = NUM_ADD_RULE btm dtm in let th1 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_oo2 in QUICK_PROVE_HYP (end_itlist CONJ [th2;th3;th4;th5;th6]) th1 | _ -> failwith "NUM_MUL_RULE" in NUM_MUL_RULE in let NUM_MULT_CONV' = let pth_refl = (STANDARDIZE o MESON[EXP_2]) `m EXP 2 = p <=> m * m = p` in fun tm -> match tm with Comb(Comb(Const("*",_),mtm),ntm) -> if Pervasives.compare mtm ntm = 0 then let th1 = NUM_SQUARE_RULE mtm in let ptm = rand(concl th1) in EQ_MP (INST [mtm,m_tm;ptm,p_tm] pth_refl) th1 else let w1,z1 = bitcounts mtm and w2,z2 = bitcounts ntm in NUM_MUL_RULE (w1+z1) (w2+z2) mtm ntm | _ -> failwith "NUM_MULT_CONV'" in let NUM_SUC_CONV = let pth = (STANDARDIZE o prove) (`SUC(_0 + m) = n <=> SUC(NUMERAL m) = NUMERAL n`, BINOP_TAC THEN MESON_TAC[NUMERAL; ADD_CLAUSES]) in fun tm -> match tm with Comb(Const("SUC",_),Comb(Const("NUMERAL",_),mtm)) when wellformed mtm -> let th1 = NUM_ADC_RULE zero_tm mtm in let ntm = rand(concl th1) in EQ_MP(INST [mtm,m_tm; ntm,n_tm] pth) th1 | _ -> failwith "NUM_SUC_CONV" in let NUM_ADD_CONV = let topthm_add = (STANDARDIZE o MESON[NUMERAL]) `m + n = p <=> NUMERAL m + NUMERAL n = NUMERAL p` in fun tm -> match tm with Comb(Comb(Const("+",_),Comb(Const("NUMERAL",_),mtm)), Comb(Const("NUMERAL",_),ntm)) when wellformed mtm & wellformed ntm -> let th1 = NUM_ADD_RULE mtm ntm in let ptm = rand(concl th1) in let th2 = INST [mtm,m_tm; ntm,n_tm; ptm,p_tm] topthm_add in EQ_MP th2 th1 | _ -> failwith "NUM_ADD_CONV" in let NUM_MULT_CONV = let topthm_mul = (STANDARDIZE o MESON[NUMERAL]) `m * n = p <=> NUMERAL m * NUMERAL n = NUMERAL p` and pth_refl = (STANDARDIZE o MESON[NUMERAL; EXP_2]) `m EXP 2 = p <=> NUMERAL m * NUMERAL m = NUMERAL p` in fun tm -> match tm with Comb(Comb(Const("*",_),Comb(Const("NUMERAL",_),mtm)), Comb(Const("NUMERAL",_),ntm)) -> if Pervasives.compare mtm ntm = 0 then let th1 = NUM_SQUARE_RULE mtm in let ptm = rand(concl th1) in EQ_MP (INST [mtm,m_tm;ptm,p_tm] pth_refl) th1 else let w1,z1 = bitcounts mtm and w2,z2 = bitcounts ntm in let th1 = NUM_MUL_RULE (w1+z1) (w2+z2) mtm ntm in let ptm = rand(concl th1) in let th2 = INST [mtm,m_tm; ntm,n_tm; ptm,p_tm] topthm_mul in EQ_MP th2 th1 | _ -> failwith "NUM_MULT_CONV" in let NUM_EXP_CONV = let pth0 = (STANDARDIZE o prove) (`(m EXP n = p) ==> (p * p = a) ==> (m EXP (BIT0 n) = a)`, REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[BIT0; EXP_ADD]) and pth1 = (STANDARDIZE o prove) (`(m EXP n = p) ==> (p * p = b) ==> (m * b = a) ==> (m EXP (BIT1 n) = a)`, REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[BIT1; EXP_ADD; EXP]) and pth = (STANDARDIZE o prove) (`m EXP _0 = BIT1 _0`, MP_TAC (CONJUNCT1 EXP) THEN REWRITE_TAC[NUMERAL; BIT1] THEN DISCH_THEN MATCH_ACCEPT_TAC) and tth = (STANDARDIZE o prove) (`(NUMERAL m) EXP (NUMERAL n) = m EXP n`, REWRITE_TAC[NUMERAL]) and fth = (STANDARDIZE o prove) (`m = NUMERAL m`, REWRITE_TAC[NUMERAL]) in let tconv = GEN_REWRITE_CONV I [tth] in let rec NUM_EXP_CONV l r = if r = zero_tm then INST [l,m_tm] pth else let b,r' = dest_comb r in if b = BIT0_tm then let th1 = NUM_EXP_CONV l r' in let tm1 = rand(concl th1) in let th2 = NUM_MULT_CONV' (mk_binop mul_tm tm1 tm1) in let tm2 = rand(concl th2) in MP (MP (INST [l,m_tm; r',n_tm; tm1,p_tm; tm2,a_tm] pth0) th1) th2 else let th1 = NUM_EXP_CONV l r' in let tm1 = rand(concl th1) in let th2 = NUM_MULT_CONV' (mk_binop mul_tm tm1 tm1) in let tm2 = rand(concl th2) in let th3 = NUM_MULT_CONV' (mk_binop mul_tm l tm2) in let tm3 = rand(concl th3) in MP (MP (MP (INST [l,m_tm; r',n_tm; tm1,p_tm; tm2,b_tm; tm3,a_tm] pth1) th1) th2) th3 in fun tm -> try let th = tconv tm in let lop,r = dest_comb (rand(concl th)) in let _,l = dest_comb lop in if not (wellformed l & wellformed r) then failwith "" else let th' = NUM_EXP_CONV l r in let tm' = rand(concl th') in TRANS (TRANS th th') (INST [tm',m_tm] fth) with Failure _ -> failwith "NUM_EXP_CONV" in let NUM_LT_CONV = let pth = (UNDISCH o STANDARDIZE o prove) (`SUC(m + n) = p ==> ((NUMERAL n < NUMERAL p) <=> T)`, REWRITE_TAC[NUMERAL; LT_EXISTS; ADD_CLAUSES] THEN MESON_TAC[ADD_SYM]) and qth = (UNDISCH o STANDARDIZE o prove) (`m + p = n ==> (NUMERAL n < NUMERAL p <=> F)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[NOT_LT; NUMERAL] THEN MESON_TAC[LE_ADD; ADD_SYM]) and rth = (STANDARDIZE o prove) (`NUMERAL n < NUMERAL n <=> F`, MESON_TAC[LT_REFL]) in fun tm -> match tm with Comb(Comb(Const("<",_),Comb(Const("NUMERAL",_),mtm)), Comb(Const("NUMERAL",_),ntm)) -> let rel = orderrelation mtm ntm in if rel = 0 then INST[ntm,n_tm] rth else if rel < 0 then let dtm = sbcbn ntm mtm in let th = NUM_ADC_RULE dtm mtm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth) else let dtm = subbn mtm ntm in let th = NUM_ADD_RULE dtm ntm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth) | _ -> failwith "NUM_LT_CONV" and NUM_LE_CONV = let pth = (UNDISCH o STANDARDIZE o prove) (`m + n = p ==> ((NUMERAL n <= NUMERAL p) <=> T)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[NUMERAL] THEN MESON_TAC[LE_ADD; ADD_SYM]) and qth = (UNDISCH o STANDARDIZE o prove) (`SUC(m + p) = n ==> (NUMERAL n <= NUMERAL p <=> F)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[NUMERAL; NOT_LE; ADD_CLAUSES; LT_EXISTS] THEN MESON_TAC[ADD_SYM]) and rth = (STANDARDIZE o prove) (`NUMERAL n <= NUMERAL n <=> T`, REWRITE_TAC[LE_REFL]) in fun tm -> match tm with Comb(Comb(Const("<=",_),Comb(Const("NUMERAL",_),mtm)), Comb(Const("NUMERAL",_),ntm)) -> let rel = orderrelation mtm ntm in if rel = 0 then INST[ntm,n_tm] rth else if rel < 0 then let dtm = subbn ntm mtm in let th = NUM_ADD_RULE dtm mtm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth) else let dtm = sbcbn mtm ntm in let th = NUM_ADC_RULE dtm ntm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth) | _ -> failwith "NUM_LE_CONV" and NUM_EQ_CONV = let pth = (UNDISCH o STANDARDIZE o prove) (`SUC(m + n) = p ==> ((NUMERAL n = NUMERAL p) <=> F)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; DE_MORGAN_THM] THEN REWRITE_TAC[NOT_LE; LT_EXISTS; ADD_CLAUSES] THEN MESON_TAC[ADD_SYM]) and qth = (UNDISCH o STANDARDIZE o prove) (`SUC(m + p) = n ==> ((NUMERAL n = NUMERAL p) <=> F)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; DE_MORGAN_THM] THEN REWRITE_TAC[NOT_LE; LT_EXISTS; ADD_CLAUSES] THEN MESON_TAC[ADD_SYM]) and rth = (STANDARDIZE o prove) (`(NUMERAL n = NUMERAL n) <=> T`, REWRITE_TAC[]) in fun tm -> match tm with Comb(Comb(Const("=",_),Comb(Const("NUMERAL",_),mtm)), Comb(Const("NUMERAL",_),ntm)) -> let rel = orderrelation mtm ntm in if rel = 0 then INST [ntm,n_tm] rth else if rel < 0 then let dtm = sbcbn ntm mtm in let th = NUM_ADC_RULE dtm mtm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth) else let dtm = sbcbn mtm ntm in let th = NUM_ADC_RULE dtm ntm in QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth) | _ -> failwith "NUM_EQ_CONV" in NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV, NUM_LT_CONV,NUM_LE_CONV,NUM_EQ_CONV;; let NUM_GT_CONV = GEN_REWRITE_CONV I [GT] THENC NUM_LT_CONV;; let NUM_GE_CONV = GEN_REWRITE_CONV I [GE] THENC NUM_LE_CONV;; let NUM_PRE_CONV =
let tth = 
prove (`PRE 0 = 0`,
REWRITE_TAC[PRE]) in
let pth = prove
   (`(SUC m = n) ==> (PRE n = m)`,
    DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[PRE])
  and m = `m:num` and n = `n:num` in
  let suc = `SUC` in
  let pre = `PRE` in
  fun tm -> try let l,r = dest_comb tm in
                if not (l = pre) then fail() else
                let x = dest_numeral r in
                if x =/ Int 0 then tth else
                let tm' = mk_numeral (x -/ Int 1) in
                let th1 = NUM_SUC_CONV (mk_comb(suc,tm')) in
                MP (INST [tm',m; r,n] pth) th1
            with Failure _ -> failwith "NUM_PRE_CONV";
; let NUM_SUB_CONV =
let pth0 = 
prove (`p <= n ==> (p - n = 0)`,
REWRITE_TAC[SUB_EQ_0]) and pth1 = prove (`(m + n = p) ==> (p - n = m)`, DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[ADD_SUB]) and m = `m:num` and n = `n:num` and p = `p:num` and minus = `(-)` and plus = `(+)` and le = `(<=)` in fun tm -> try let l,r = dest_binop minus tm in let ln = dest_numeral l and rn = dest_numeral r in if ln <=/ rn then let pth = INST [l,p; r,n] pth0 and th0 = EQT_ELIM(NUM_LE_CONV (mk_binop le l r)) in MP pth th0 else let kn = ln -/ rn in let k = mk_numeral kn in let pth = INST [k,m; l,p; r,n] pth1 and th0 = NUM_ADD_CONV (mk_binop plus k r) in MP pth th0 with Failure _ -> failwith "NUM_SUB_CONV";
; let NUM_DIV_CONV,NUM_MOD_CONV =
let pth = 
prove (`(q * n + r = m) ==> r < n ==> (m DIV n = q) /\ (m MOD n = r)`,
MESON_TAC[DIVMOD_UNIQ]) and m = `m:num` and n = `n:num` and q = `q:num` and r = `r:num` and dtm = `(DIV)` and mtm = `(MOD)` in let NUM_DIVMOD_CONV x y = let k = quo_num x y and l = mod_num x y in let th0 = INST [mk_numeral x,m; mk_numeral y,n; mk_numeral k,q; mk_numeral l,r] pth in let tm0 = lhand(lhand(concl th0)) in let th1 = (LAND_CONV NUM_MULT_CONV THENC NUM_ADD_CONV) tm0 in let th2 = MP th0 th1 in let tm2 = lhand(concl th2) in MP th2 (EQT_ELIM(NUM_LT_CONV tm2)) in (fun tm -> try let xt,yt = dest_binop dtm tm in CONJUNCT1(NUM_DIVMOD_CONV (dest_numeral xt) (dest_numeral yt)) with Failure _ -> failwith "NUM_DIV_CONV"), (fun tm -> try let xt,yt = dest_binop mtm tm in CONJUNCT2(NUM_DIVMOD_CONV (dest_numeral xt) (dest_numeral yt)) with Failure _ -> failwith "NUM_MOD_CONV");;
let NUM_FACT_CONV = let suc = `SUC` and mul = `(*)` in let pth_0 = prove (`FACT 0 = 1`, REWRITE_TAC[FACT]) and pth_suc = prove (`(SUC x = y) ==> (FACT x = w) ==> (y * w = z) ==> (FACT y = z)`, REPEAT (DISCH_THEN(SUBST1_TAC o SYM)) THEN REWRITE_TAC[FACT]) and w = `w:num` and x = `x:num` and y = `y:num` and z = `z:num` in let mksuc n = let n' = n -/ (Int 1) in NUM_SUC_CONV (mk_comb(suc,mk_numeral n')) in let rec NUM_FACT_CONV n = if n =/ Int 0 then pth_0 else let th0 = mksuc n in let tmx = rand(lhand(concl th0)) in let tm0 = rand(concl th0) in let th1 = NUM_FACT_CONV (n -/ Int 1) in let tm1 = rand(concl th1) in let th2 = NUM_MULT_CONV (mk_binop mul tm0 tm1) in let tm2 = rand(concl th2) in let pth = INST [tmx,x; tm0, y; tm1,w; tm2,z] pth_suc in MP (MP (MP pth th0) th1) th2 in fun tm -> try let l,r = dest_comb tm in if fst(dest_const l) = "FACT" then NUM_FACT_CONV (dest_numeral r) else fail() with Failure _ -> failwith "NUM_FACT_CONV";; let NUM_MAX_CONV = REWR_CONV MAX THENC RATOR_CONV(RATOR_CONV(RAND_CONV NUM_LE_CONV)) THENC GEN_REWRITE_CONV I [COND_CLAUSES];; let NUM_MIN_CONV = REWR_CONV MIN THENC RATOR_CONV(RATOR_CONV(RAND_CONV NUM_LE_CONV)) THENC GEN_REWRITE_CONV I [COND_CLAUSES];; (* ------------------------------------------------------------------------- *) (* Final hack-together. *) (* ------------------------------------------------------------------------- *) let NUM_REL_CONV = let gconv_net = itlist (uncurry net_of_conv) [`NUMERAL m < NUMERAL n`,NUM_LT_CONV; `NUMERAL m <= NUMERAL n`,NUM_LE_CONV; `NUMERAL m > NUMERAL n`,NUM_GT_CONV; `NUMERAL m >= NUMERAL n`,NUM_GE_CONV; `NUMERAL m = NUMERAL n`,NUM_EQ_CONV] (basic_net()) in REWRITES_CONV gconv_net;; let NUM_RED_CONV = let gconv_net = itlist (uncurry net_of_conv) [`SUC(NUMERAL n)`,NUM_SUC_CONV; `PRE(NUMERAL n)`,NUM_PRE_CONV; `FACT(NUMERAL n)`,NUM_FACT_CONV; `NUMERAL m < NUMERAL n`,NUM_LT_CONV; `NUMERAL m <= NUMERAL n`,NUM_LE_CONV; `NUMERAL m > NUMERAL n`,NUM_GT_CONV; `NUMERAL m >= NUMERAL n`,NUM_GE_CONV; `NUMERAL m = NUMERAL n`,NUM_EQ_CONV; `EVEN(NUMERAL n)`,NUM_EVEN_CONV; `ODD(NUMERAL n)`,NUM_ODD_CONV; `NUMERAL m + NUMERAL n`,NUM_ADD_CONV; `NUMERAL m - NUMERAL n`,NUM_SUB_CONV; `NUMERAL m * NUMERAL n`,NUM_MULT_CONV; `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV; `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV; `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV; `MAX (NUMERAL m) (NUMERAL n)`,NUM_MAX_CONV; `MIN (NUMERAL m) (NUMERAL n)`,NUM_MIN_CONV] (basic_net()) in REWRITES_CONV gconv_net;; let NUM_REDUCE_CONV = DEPTH_CONV NUM_RED_CONV;; let NUM_REDUCE_TAC = CONV_TAC NUM_REDUCE_CONV;; (* ------------------------------------------------------------------------- *) (* I do like this after all... *) (* ------------------------------------------------------------------------- *) let num_CONV = let SUC_tm = `SUC` in fun tm -> let n = dest_numeral tm -/ Int 1 in if n </ Int 0 then failwith "num_CONV" else let tm' = mk_numeral n in SYM(NUM_SUC_CONV (mk_comb(SUC_tm,tm')));; (* ------------------------------------------------------------------------- *) (* Expands "!n. n < numeral-constant ==> P(n)" into all the cases. *) (* ------------------------------------------------------------------------- *) let EXPAND_CASES_CONV =
let pth_base = 
prove (`(!n. n < 0 ==> P n) <=> T`,
REWRITE_TAC[LT]) and pth_step = prove (`(!n. n < SUC k ==> P n) <=> (!n. n < k ==> P n) /\ P k`, REWRITE_TAC[LT] THEN MESON_TAC[]) in let base_CONV = GEN_REWRITE_CONV I [pth_base] and step_CONV = BINDER_CONV(LAND_CONV(RAND_CONV num_CONV)) THENC GEN_REWRITE_CONV I [pth_step] in let rec conv tm = (base_CONV ORELSEC (step_CONV THENC LAND_CONV conv)) tm in conv THENC (REWRITE_CONV[GSYM CONJ_ASSOC]);;