calc_num.ml

   1 (* ========================================================================= *)
   2 (* Calculation with naturals.                                                *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "wf.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Simple rule to get rid of NUMERAL constant.                               *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let DENUMERAL = GEN_REWRITE_RULE DEPTH_CONV [NUMERAL];;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* Big collection of rewrites to do trivial arithmetic.                      *)
  20 (*                                                                           *)
  21 (* Note that we have none for DIV and MOD, and that PRE and SUB are a bit    *)
  22 (* inefficient; log(n)^2 instead of log(n).                                  *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let ARITH_ZERO = prove
  26  (`(NUMERAL 0 = 0) /\
  27    (BIT0 _0 = _0)`,
  28   REWRITE_TAC[NUMERAL; BIT0; DENUMERAL ADD_CLAUSES]);;
  29
  30 let ARITH_SUC = prove
  31  (`(!n. SUC(NUMERAL n) = NUMERAL(SUC n)) /\
  32    (SUC _0 = BIT1 _0) /\
  33    (!n. SUC (BIT0 n) = BIT1 n) /\
  34    (!n. SUC (BIT1 n) = BIT0 (SUC n))`,
  35   REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES]);;
  36
  37 let ARITH_PRE = prove
  38  (`(!n. PRE(NUMERAL n) = NUMERAL(PRE n)) /\
  39    (PRE _0 = _0) /\
  40    (!n. PRE(BIT0 n) = if n = _0 then _0 else BIT1 (PRE n)) /\
  41    (!n. PRE(BIT1 n) = BIT0 n)`,
  42   REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL PRE] THEN INDUCT_TAC THEN
  43   REWRITE_TAC[NUMERAL; DENUMERAL PRE; DENUMERAL ADD_CLAUSES; DENUMERAL NOT_SUC;
  44               ARITH_ZERO]);;
  45
  46 let ARITH_ADD = prove
  47  (`(!m n. NUMERAL(m) + NUMERAL(n) = NUMERAL(m + n)) /\
  48    (_0 + _0 = _0) /\
  49    (!n. _0 + BIT0 n = BIT0 n) /\
  50    (!n.        _0 + BIT1 n = BIT1 n) /\
  51    (!n.   BIT0 n + _0 = BIT0 n) /\
  52    (!n.   BIT1 n + _0 = BIT1 n) /\
  53    (!m n. BIT0 m + BIT0 n = BIT0 (m + n)) /\
  54    (!m n. BIT0 m + BIT1 n = BIT1 (m + n)) /\
  55    (!m n. BIT1 m + BIT0 n = BIT1 (m + n)) /\
  56    (!m n. BIT1 m + BIT1 n = BIT0 (SUC(m + n)))`,
  57   PURE_REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES; SUC_INJ] THEN
  58   REWRITE_TAC[ADD_AC]);;
  59
  60 let ARITH_MULT = prove
  61  (`(!m n. NUMERAL(m) * NUMERAL(n) = NUMERAL(m * n)) /\
  62    (_0 * _0 = _0) /\
  63    (!n. _0 * BIT0 n = _0) /\
  64    (!n. _0 * BIT1 n = _0) /\
  65    (!n. BIT0 n * _0 = _0) /\
  66    (!n. BIT1 n * _0 = _0) /\
  67    (!m n. BIT0 m * BIT0 n = BIT0 (BIT0 (m * n))) /\
  68    (!m n. BIT0 m * BIT1 n = BIT0 m + BIT0 (BIT0 (m * n))) /\
  69    (!m n. BIT1 m * BIT0 n = BIT0 n + BIT0 (BIT0 (m * n))) /\
  70    (!m n. BIT1 m * BIT1 n = BIT1 m + BIT0 n + BIT0 (BIT0 (m * n)))`,
  71   PURE_REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL MULT_CLAUSES;
  72                    DENUMERAL ADD_CLAUSES; SUC_INJ] THEN
  73   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; ADD_AC]);;
  74
  75 let ARITH_EXP = prove
  76  (`(!m n. (NUMERAL m) EXP (NUMERAL n) = NUMERAL(m EXP n)) /\
  77    (_0 EXP _0 = BIT1 _0) /\
  78    (!m. (BIT0 m) EXP _0 = BIT1 _0) /\
  79    (!m. (BIT1 m) EXP _0 = BIT1 _0) /\
  80    (!n. _0 EXP (BIT0 n) = (_0 EXP n) * (_0 EXP n)) /\
  81    (!m n. (BIT0 m) EXP (BIT0 n) = ((BIT0 m) EXP n) * ((BIT0 m) EXP n)) /\
  82    (!m n. (BIT1 m) EXP (BIT0 n) = ((BIT1 m) EXP n) * ((BIT1 m) EXP n)) /\
  83    (!n. _0 EXP (BIT1 n) = _0) /\
  84    (!m n. (BIT0 m) EXP (BIT1 n) =
  85         BIT0 m * ((BIT0 m) EXP n) * ((BIT0 m) EXP n)) /\
  86    (!m n. (BIT1 m) EXP (BIT1 n) =
  87         BIT1 m * ((BIT1 m) EXP n) * ((BIT1 m) EXP n))`,
  88   REWRITE_TAC[NUMERAL] THEN REPEAT STRIP_TAC THEN
  89   TRY(GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [BIT0; BIT1]) THEN
  90   REWRITE_TAC[DENUMERAL EXP; DENUMERAL MULT_CLAUSES; EXP_ADD]);;
  91
  92 let ARITH_EVEN = prove
  93  (`(!n. EVEN(NUMERAL n) <=> EVEN n) /\
  94    (EVEN _0 <=> T) /\
  95    (!n. EVEN(BIT0 n) <=> T) /\
  96    (!n. EVEN(BIT1 n) <=> F)`,
  97   REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL EVEN; EVEN_ADD]);;
  98
  99 let ARITH_ODD = prove
 100  (`(!n. ODD(NUMERAL n) <=> ODD n) /\
 101    (ODD _0 <=> F) /\
 102    (!n. ODD(BIT0 n) <=> F) /\
 103    (!n. ODD(BIT1 n) <=> T)`,
 104   REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL ODD; ODD_ADD]);;
 105
 106 let ARITH_LE = prove
 107  (`(!m n. NUMERAL m <= NUMERAL n <=> m <= n) /\
 108    ((_0 <= _0) <=> T) /\
 109    (!n. (BIT0 n <= _0) <=> n <= _0) /\
 110    (!n. (BIT1 n <= _0) <=> F) /\
 111    (!n. (_0 <= BIT0 n) <=> T) /\
 112    (!n. (_0 <= BIT1 n) <=> T) /\
 113    (!m n. (BIT0 m <= BIT0 n) <=> m <= n) /\
 114    (!m n. (BIT0 m <= BIT1 n) <=> m <= n) /\
 115    (!m n. (BIT1 m <= BIT0 n) <=> m < n) /\
 116    (!m n. (BIT1 m <= BIT1 n) <=> m <= n)`,
 117   REWRITE_TAC[NUMERAL; BIT1; BIT0; DENUMERAL NOT_SUC;
 118       DENUMERAL(GSYM NOT_SUC); SUC_INJ] THEN
 119   REWRITE_TAC[DENUMERAL LE_0] THEN REWRITE_TAC[DENUMERAL LE; GSYM MULT_2] THEN
 120   REWRITE_TAC[LE_MULT_LCANCEL; SUC_INJ;
 121               DENUMERAL MULT_EQ_0; DENUMERAL NOT_SUC] THEN
 122   REWRITE_TAC[DENUMERAL NOT_SUC] THEN REWRITE_TAC[LE_SUC_LT] THEN
 123   REWRITE_TAC[LT_MULT_LCANCEL] THEN
 124   SUBGOAL_THEN `2 = SUC 1` (fun th -> REWRITE_TAC[th]) THENL
 125    [REWRITE_TAC[NUMERAL; BIT0; BIT1; DENUMERAL ADD_CLAUSES];
 126     REWRITE_TAC[DENUMERAL NOT_SUC; NOT_SUC; EQ_MULT_LCANCEL] THEN
 127     REWRITE_TAC[ONCE_REWRITE_RULE[DISJ_SYM] LE_LT] THEN
 128     MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
 129     SUBGOAL_THEN `~(SUC 1 * m = SUC (SUC 1 * n))`
 130       (fun th -> REWRITE_TAC[th]) THEN
 131     DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
 132     REWRITE_TAC[EVEN_MULT; EVEN_ADD; NUMERAL; BIT1; EVEN]]);;
 133
 134 let ARITH_LT = prove
 135  (`(!m n. NUMERAL m < NUMERAL n <=> m < n) /\
 136    ((_0 < _0) <=> F) /\
 137    (!n. (BIT0 n < _0) <=> F) /\
 138    (!n. (BIT1 n < _0) <=> F) /\
 139    (!n. (_0 < BIT0 n) <=> _0 < n) /\
 140    (!n. (_0 < BIT1 n) <=> T) /\
 141    (!m n. (BIT0 m < BIT0 n) <=> m < n) /\
 142    (!m n. (BIT0 m < BIT1 n) <=> m <= n) /\
 143    (!m n. (BIT1 m < BIT0 n) <=> m < n) /\
 144    (!m n. (BIT1 m < BIT1 n) <=> m < n)`,
 145   REWRITE_TAC[NUMERAL; GSYM NOT_LE; ARITH_LE] THEN
 146   REWRITE_TAC[DENUMERAL LE]);;
 147
 148 let ARITH_GE = REWRITE_RULE[GSYM GE; GSYM GT] ARITH_LE;;
 149
 150 let ARITH_GT = REWRITE_RULE[GSYM GE; GSYM GT] ARITH_LT;;
 151
 152 let ARITH_EQ = prove
 153  (`(!m n. (NUMERAL m = NUMERAL n) <=> (m = n)) /\
 154    ((_0 = _0) <=> T) /\
 155    (!n. (BIT0 n = _0) <=> (n = _0)) /\
 156    (!n. (BIT1 n = _0) <=> F) /\
 157    (!n. (_0 = BIT0 n) <=> (_0 = n)) /\
 158    (!n. (_0 = BIT1 n) <=> F) /\
 159    (!m n. (BIT0 m = BIT0 n) <=> (m = n)) /\
 160    (!m n. (BIT0 m = BIT1 n) <=> F) /\
 161    (!m n. (BIT1 m = BIT0 n) <=> F) /\
 162    (!m n. (BIT1 m = BIT1 n) <=> (m = n))`,
 163   REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; ARITH_LE] THEN
 164   REWRITE_TAC[LET_ANTISYM; LTE_ANTISYM; DENUMERAL LE_0]);;
 165
 166 let ARITH_SUB = prove
 167  (`(!m n. NUMERAL m - NUMERAL n = NUMERAL(m - n)) /\
 168    (_0 - _0 = _0) /\
 169    (!n. _0 - BIT0 n = _0) /\
 170    (!n. _0 - BIT1 n = _0) /\
 171    (!n. BIT0 n - _0 = BIT0 n) /\
 172    (!n. BIT1 n - _0 = BIT1 n) /\
 173    (!m n. BIT0 m - BIT0 n = BIT0 (m - n)) /\
 174    (!m n. BIT0 m - BIT1 n = PRE(BIT0 (m - n))) /\
 175    (!m n. BIT1 m - BIT0 n = if n <= m then BIT1 (m - n) else _0) /\
 176    (!m n. BIT1 m - BIT1 n = BIT0 (m - n))`,
 177   REWRITE_TAC[NUMERAL; DENUMERAL SUB_0] THEN PURE_REWRITE_TAC[BIT0; BIT1] THEN
 178   REWRITE_TAC[GSYM MULT_2; SUB_SUC; LEFT_SUB_DISTRIB] THEN
 179   REWRITE_TAC[SUB] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 180   REWRITE_TAC[DENUMERAL SUB_EQ_0] THEN
 181   RULE_ASSUM_TAC(REWRITE_RULE[NOT_LE]) THEN
 182   ASM_REWRITE_TAC[LE_SUC_LT; LT_MULT_LCANCEL; ARITH_EQ] THEN
 183   POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 184   REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB] THEN
 185   REWRITE_TAC[ADD_SUB2; GSYM ADD_ASSOC]);;
 186
 187 let ARITH = end_itlist CONJ
 188   [ARITH_ZERO; ARITH_SUC; ARITH_PRE;
 189    ARITH_ADD; ARITH_MULT; ARITH_EXP;
 190    ARITH_EVEN; ARITH_ODD;
 191    ARITH_EQ; ARITH_LE; ARITH_LT; ARITH_GE; ARITH_GT;
 192    ARITH_SUB];;
 193
 194 (* ------------------------------------------------------------------------- *)
 195 (* Now more delicate conversions for situations where efficiency matters.    *)
 196 (* ------------------------------------------------------------------------- *)
 197
 198 let NUM_EVEN_CONV =
 199   let tth,rths = CONJ_PAIR ARITH_EVEN in
 200   GEN_REWRITE_CONV I [tth] THENC GEN_REWRITE_CONV I [rths];;
 201
 202 let NUM_ODD_CONV =
 203   let tth,rths = CONJ_PAIR ARITH_ODD in
 204   GEN_REWRITE_CONV I [tth] THENC GEN_REWRITE_CONV I [rths];;
 205
 206 let NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV,
 207     NUM_LT_CONV,NUM_LE_CONV,NUM_EQ_CONV =
 208   let Comb(NUMERAL_tm,Comb(BIT0_tm,Comb(BIT1_tm,zero_tm))) =
 209     mk_small_numeral 2
 210   and suc_tm = rator(rand(concl TWO))
 211   and one_tm = rand(mk_small_numeral 1)
 212   and add_tm = rator(rator(lhand(snd(strip_forall(concl ADD_0)))))
 213   and mul_tm = rator(rator(rand(snd(strip_forall(concl EXP_2)))))
 214   and exp_tm = rator(rator(lhand(snd(strip_forall(concl EXP_2)))))
 215   and eq_tm = rator(rator(concl TWO)) in
 216   let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2 in
 217   let a_tm = `a:num`
 218   and b_tm = `b:num`
 219   and c_tm = `c:num`
 220   and d_tm = `d:num`
 221   and e_tm = `e:num`
 222   and h_tm = `h:num`
 223   and l_tm = `l:num`
 224   and m_tm = `m:num`
 225   and n_tm = `n:num`
 226   and p_tm = `p:num` in
 227   let STANDARDIZE =
 228     let ilist = [BIT0_tm,BIT0_tm; BIT1_tm,BIT1_tm; zero_tm,zero_tm;
 229                  suc_tm,suc_tm; add_tm,add_tm; mul_tm,mul_tm;
 230                  exp_tm,exp_tm; eq_tm,eq_tm; NUMERAL_tm,NUMERAL_tm;
 231                  a_tm,a_tm; b_tm,b_tm; c_tm,c_tm; d_tm,d_tm; e_tm,e_tm;
 232                  h_tm,h_tm; l_tm,l_tm; m_tm,m_tm; n_tm,n_tm; p_tm,p_tm] in
 233     let rec replace tm =
 234       match tm with
 235         Var(_,_) | Const(_,_) -> rev_assocd tm ilist tm
 236       | Comb(s,t) -> mk_comb(replace s,replace t)
 237       | Abs(_,_) -> failwith "replace" in
 238     fun th -> let tm' = replace (concl th) in EQ_MP (REFL tm') th in
 239   let REFL_bit0 = STANDARDIZE(REFL BIT0_tm)
 240   and REFL_bit1 = STANDARDIZE(REFL BIT1_tm) in
 241   let AP_BIT0 th = MK_COMB(REFL_bit0,th)
 242   and AP_BIT1 th = MK_COMB(REFL_bit1,th)
 243   and QUICK_PROVE_HYP ath bth = EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath in
 244   let rec dest_raw_numeral tm =
 245     match tm with
 246       Comb(Const("BIT1",_),t) -> num_2 */ dest_raw_numeral t +/ num_1
 247     | Comb(Const("BIT0",_),t) -> num_2 */ dest_raw_numeral t
 248     | Const("_0",_) -> num_0 in
 249   let bitcounts =
 250     let rec bctr w z tm =
 251       match tm with
 252         Const("_0",_) -> (w,z)
 253       | Comb(Const("BIT0",_),t) -> bctr w (z + 1) t
 254       | Comb(Const("BIT1",_),t) -> bctr (w + 1) z t
 255       | _ -> failwith "malformed numeral" in
 256     bctr 0 0 in
 257   let rec wellformed tm =
 258     match tm with
 259       Const("_0",_) -> true
 260     | Comb(Const("BIT0",_),t)|Comb(Const("BIT1",_),t) -> wellformed t
 261     | _ -> false in
 262   let rec orderrelation mtm ntm =
 263     if mtm == ntm then
 264       if wellformed mtm then 0 else failwith "orderrelation"
 265     else
 266       match (mtm,ntm) with
 267         Const("_0",_),Const("_0",_) -> 0
 268       | Const("_0",_),_ ->
 269            if wellformed ntm then -1 else failwith "orderrelation"
 270       | _, Const("_0",_) ->
 271            if wellformed ntm then 1 else failwith "orderrelation"
 272       | Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt)
 273       | Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt) ->
 274           orderrelation mt nt
 275       | Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt) ->
 276           if orderrelation mt nt > 0 then 1 else -1
 277       | Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt) ->
 278           if orderrelation mt nt < 0 then -1 else 1 in
 279   let doublebn tm = if tm = zero_tm then tm else mk_comb(BIT0_tm,tm) in
 280   let rec subbn mtm ntm =
 281     match (mtm,ntm) with
 282       (_,Const("_0",_)) -> mtm
 283     | (Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt)) ->
 284           doublebn (subbn mt nt)
 285     | (Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt)) ->
 286           doublebn (subbn mt nt)
 287     | (Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt)) ->
 288           mk_comb(BIT1_tm,subbn mt nt)
 289     | (Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt)) ->
 290           mk_comb(BIT1_tm,sbcbn mt nt)
 291     | _ -> failwith "malformed numeral or wrong relation"
 292   and sbcbn mtm ntm =
 293     match (mtm,ntm) with
 294     | (Comb(Const("BIT0",_),mt),Const("_0",_)) ->
 295           mk_comb(BIT1_tm,sbcbn mt ntm)
 296     | (Comb(Const("BIT1",_),mt),Const("_0",_)) ->
 297           doublebn mt
 298     | (Comb(Const("BIT0",_),mt),Comb(Const("BIT0",_),nt)) ->
 299           mk_comb(BIT1_tm,sbcbn mt nt)
 300     | (Comb(Const("BIT1",_),mt),Comb(Const("BIT1",_),nt)) ->
 301           mk_comb(BIT1_tm,sbcbn mt nt)
 302     | (Comb(Const("BIT1",_),mt),Comb(Const("BIT0",_),nt)) ->
 303           doublebn (subbn mt nt)
 304     | (Comb(Const("BIT0",_),mt),Comb(Const("BIT1",_),nt)) ->
 305           doublebn (sbcbn mt nt)
 306     | _ -> failwith "malformed numeral or wrong relation" in
 307   let topsplit tm =
 308     match tm with
 309      Const("_0",_) -> 0,zero_tm
 310    | Comb(Const("BIT1",_),Const("_0",_)) -> 1,zero_tm
 311    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_))) -> 2,zero_tm
 312    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_))) -> 3,zero_tm
 313    | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 4,zero_tm
 314    | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 5,zero_tm
 315    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 6,zero_tm
 316    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Const("_0",_)))) -> 7,zero_tm
 317    | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 0,n
 318    | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 1,n
 319    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 2,n
 320    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),n)))) -> 3,n
 321    | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 4,n
 322    | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 5,n
 323    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 6,n
 324    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),n)))) -> 7,n
 325    | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 8,n
 326    | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 9,n
 327    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 10,n
 328    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),n)))) -> 11,n
 329    | Comb(Const("BIT0",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 12,n
 330    | Comb(Const("BIT1",_),Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 13,n
 331    | Comb(Const("BIT0",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 14,n
 332    | Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),Comb(Const("BIT1",_),n)))) -> 15,n
 333    | _ -> failwith "malformed numeral" in
 334   let NUM_ADD_RULE,NUM_ADC_RULE =
 335     let rec mk_compnumeral k base =
 336       if k = 0 then base else
 337       let t = mk_compnumeral (k / 2) base in
 338       if k mod 2 = 1 then mk_comb(BIT1_tm,t) else mk_comb(BIT0_tm,t) in
 339     let bases v =
 340         let part2 = map (fun k -> mk_compnumeral k v) (8--15) in
 341         let part1 = map (subst[mk_comb(BIT0_tm,v),mk_comb(BIT1_tm,v)])
 342                         part2
 343         and part0 = map (fun k -> mk_compnumeral k zero_tm) (0--15) in
 344         part0 @ part1 @ part2 in
 345     let starts =
 346       allpairs (fun mtm ntm ->
 347         mk_comb(mk_comb(add_tm,mtm),ntm)) (bases m_tm) (bases n_tm) in
 348     let BITS_INJ = (STANDARDIZE o prove)
 349      (`(BIT0 m = BIT0 n <=> m = n) /\
 350        (BIT1 m = BIT1 n <=> m = n)`,
 351       REWRITE_TAC[BIT0; BIT1] THEN
 352       REWRITE_TAC[GSYM MULT_2] THEN
 353       REWRITE_TAC[SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ]) in
 354     let ARITH_0 = (STANDARDIZE o MESON[NUMERAL; ADD_CLAUSES])
 355       `m + _0 = m /\ _0 + n = n` in
 356     let patadj = subst[`SUC(m + _0)`,`SUC m`; `SUC(_0 + n)`,`SUC n`] in
 357     let mkclauses sucflag t =
 358       let tm = if sucflag then mk_comb(suc_tm,t) else t in
 359       let th1 = PURE_REWRITE_CONV[ARITH_ADD; ARITH_SUC; ARITH_0] tm in
 360       let tm1 = patadj(rand(concl th1)) in
 361       if not(free_in add_tm tm1) then th1,
 362          (if free_in m_tm tm1 then 0 else 1) else
 363       let ptm = rand(rand(rand(rand tm1))) in
 364       let tmc = mk_eq(mk_eq(ptm,p_tm),mk_eq(tm,subst[p_tm,ptm] tm1)) in
 365       EQT_ELIM(REWRITE_CONV[ARITH_ADD; ARITH_SUC; ARITH_0; BITS_INJ] tmc),
 366       (if free_in suc_tm tm1 then 3 else 2) in
 367     let add_clauses,add_flags =
 368       let l1,l2 = unzip(map (mkclauses false) starts) in
 369       Array.of_list(map STANDARDIZE l1),Array.of_list l2 in
 370     let adc_clauses,adc_flags =
 371       let l1,l2 = unzip(map (mkclauses true) starts) in
 372       Array.of_list(map STANDARDIZE l1),Array.of_list l2 in
 373     let rec NUM_ADD_RULE mtm ntm =
 374       let m_lo,m_hi = topsplit mtm
 375       and n_lo,n_hi = topsplit ntm in
 376       let m_ind = if m_hi = zero_tm then m_lo else m_lo + 16
 377       and n_ind = if n_hi = zero_tm then n_lo else n_lo + 16 in
 378       let ind = 32 * m_ind + n_ind in
 379       let th1 = Array.get add_clauses ind
 380       and fl = Array.get add_flags ind in
 381       match fl with
 382         0 -> INST [m_hi,m_tm] th1
 383       | 1 -> INST [n_hi,n_tm] th1
 384       | 2 -> let th2 = NUM_ADD_RULE m_hi n_hi in
 385              (match concl th2 with Comb(_,ptm) ->
 386               let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in
 387               EQ_MP th3 th2)
 388       | 3 -> let th2 = NUM_ADC_RULE m_hi n_hi in
 389              (match concl th2 with Comb(_,ptm) ->
 390               let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in
 391               EQ_MP th3 th2)
 392     and NUM_ADC_RULE mtm ntm =
 393       let m_lo,m_hi = topsplit mtm
 394       and n_lo,n_hi = topsplit ntm in
 395       let m_ind = if m_hi = zero_tm then m_lo else m_lo + 16
 396       and n_ind = if n_hi = zero_tm then n_lo else n_lo + 16 in
 397       let ind = 32 * m_ind + n_ind in
 398       let th1 = Array.get adc_clauses ind
 399       and fl = Array.get adc_flags ind in
 400       match fl with
 401         0 -> INST [m_hi,m_tm] th1
 402       | 1 -> INST [n_hi,n_tm] th1
 403       | 2 -> let th2 = NUM_ADD_RULE m_hi n_hi in
 404              (match concl th2 with Comb(_,ptm) ->
 405               let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in
 406               EQ_MP th3 th2)
 407       | 3 -> let th2 = NUM_ADC_RULE m_hi n_hi in
 408              (match concl th2 with Comb(_,ptm) ->
 409               let th3 = INST [m_hi,m_tm; n_hi,n_tm;ptm,p_tm] th1 in
 410               EQ_MP th3 th2) in
 411     NUM_ADD_RULE,NUM_ADC_RULE in
 412   let NUM_SHIFT_CONV =
 413     let pth_0 = (STANDARDIZE o prove)
 414      (`(n = a + p * b <=> BIT0 n = BIT0 a + BIT0 p * b)`,
 415       REWRITE_TAC[BIT0; BIT1] THEN
 416       REWRITE_TAC[GSYM MULT_2; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 417       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ])
 418     and pth_z = (STANDARDIZE o prove)
 419      (`n = _0 + p * b <=> BIT0 n = _0 + BIT0 p * b`,
 420       SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN
 421       REWRITE_TAC[BIT1; BIT0] THEN
 422       REWRITE_TAC[ADD_CLAUSES; GSYM MULT_2] THEN
 423       REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; ARITH_EQ])
 424     and pth_1 = (STANDARDIZE o prove)
 425      (`(n = a + p * b <=> BIT1 n = BIT1 a + BIT0 p * b)`,
 426       REWRITE_TAC[BIT0; BIT1] THEN
 427       REWRITE_TAC[GSYM MULT_2; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB;
 428                   ADD_CLAUSES; SUC_INJ] THEN
 429       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ])
 430     and pth_base = (STANDARDIZE o prove)
 431      (`n = _0 + BIT1 _0 * n`,
 432       MESON_TAC[ADD_CLAUSES; MULT_CLAUSES; NUMERAL])
 433     and pth_triv = (STANDARDIZE o prove)
 434      (`_0 = a + p * b <=> _0 = a + BIT0 p * b`,
 435       CONV_TAC(BINOP_CONV SYM_CONV) THEN
 436       SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN
 437       REWRITE_TAC[ADD_EQ_0; MULT_EQ_0; BIT0])
 438     and pths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
 439      (`(n = a + p * b <=>
 440         BIT0(BIT0(BIT0(BIT0 n))) =
 441         BIT0(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 442        (n = a + p * b <=>
 443         BIT1(BIT0(BIT0(BIT0 n))) =
 444         BIT1(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 445        (n = a + p * b <=>
 446         BIT0(BIT1(BIT0(BIT0 n))) =
 447         BIT0(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 448        (n = a + p * b <=>
 449         BIT1(BIT1(BIT0(BIT0 n))) =
 450         BIT1(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 451        (n = a + p * b <=>
 452         BIT0(BIT0(BIT1(BIT0 n))) =
 453         BIT0(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 454        (n = a + p * b <=>
 455         BIT1(BIT0(BIT1(BIT0 n))) =
 456         BIT1(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 457        (n = a + p * b <=>
 458         BIT0(BIT1(BIT1(BIT0 n))) =
 459         BIT0(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 460        (n = a + p * b <=>
 461         BIT1(BIT1(BIT1(BIT0 n))) =
 462         BIT1(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 463        (n = a + p * b <=>
 464         BIT0(BIT0(BIT0(BIT1 n))) =
 465         BIT0(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 466        (n = a + p * b <=>
 467         BIT1(BIT0(BIT0(BIT1 n))) =
 468         BIT1(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 469        (n = a + p * b <=>
 470         BIT0(BIT1(BIT0(BIT1 n))) =
 471         BIT0(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 472        (n = a + p * b <=>
 473         BIT1(BIT1(BIT0(BIT1 n))) =
 474         BIT1(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 475        (n = a + p * b <=>
 476         BIT0(BIT0(BIT1(BIT1 n))) =
 477         BIT0(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 478        (n = a + p * b <=>
 479         BIT1(BIT0(BIT1(BIT1 n))) =
 480         BIT1(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 481        (n = a + p * b <=>
 482         BIT0(BIT1(BIT1(BIT1 n))) =
 483         BIT0(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 484        (n = a + p * b <=>
 485         BIT1(BIT1(BIT1(BIT1 n))) =
 486         BIT1(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b)`,
 487       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN
 488       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN
 489       ABBREV_TAC `two = 2` THEN
 490       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 491       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 492       FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 493       REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ;
 494                   GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC])
 495     and pths_0 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
 496      (`(n = _0 + p * b <=>
 497         BIT0(BIT0(BIT0(BIT0 n))) =
 498         _0 + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 499        (n = _0 + p * b <=>
 500         BIT1(BIT0(BIT0(BIT0 n))) =
 501         BIT1 _0 + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 502        (n = _0 + p * b <=>
 503         BIT0(BIT1(BIT0(BIT0 n))) =
 504         BIT0(BIT1 _0) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 505        (n = _0 + p * b <=>
 506         BIT1(BIT1(BIT0(BIT0 n))) =
 507         BIT1(BIT1 _0) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 508        (n = _0 + p * b <=>
 509         BIT0(BIT0(BIT1(BIT0 n))) =
 510         BIT0(BIT0(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 511        (n = _0 + p * b <=>
 512         BIT1(BIT0(BIT1(BIT0 n))) =
 513         BIT1(BIT0(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 514        (n = _0 + p * b <=>
 515         BIT0(BIT1(BIT1(BIT0 n))) =
 516         BIT0(BIT1(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 517        (n = _0 + p * b <=>
 518         BIT1(BIT1(BIT1(BIT0 n))) =
 519         BIT1(BIT1(BIT1 _0)) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 520        (n = _0 + p * b <=>
 521         BIT0(BIT0(BIT0(BIT1 n))) =
 522         BIT0(BIT0(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 523        (n = _0 + p * b <=>
 524         BIT1(BIT0(BIT0(BIT1 n))) =
 525         BIT1(BIT0(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 526        (n = _0 + p * b <=>
 527         BIT0(BIT1(BIT0(BIT1 n))) =
 528         BIT0(BIT1(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 529        (n = _0 + p * b <=>
 530         BIT1(BIT1(BIT0(BIT1 n))) =
 531         BIT1(BIT1(BIT0(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 532        (n = _0 + p * b <=>
 533         BIT0(BIT0(BIT1(BIT1 n))) =
 534         BIT0(BIT0(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 535        (n = _0 + p * b <=>
 536         BIT1(BIT0(BIT1(BIT1 n))) =
 537         BIT1(BIT0(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 538        (n = _0 + p * b <=>
 539         BIT0(BIT1(BIT1(BIT1 n))) =
 540         BIT0(BIT1(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b) /\
 541        (n = _0 + p * b <=>
 542         BIT1(BIT1(BIT1(BIT1 n))) =
 543         BIT1(BIT1(BIT1(BIT1 _0))) + BIT0(BIT0(BIT0(BIT0 p))) * b)`,
 544       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
 545       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN
 546       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN
 547       ABBREV_TAC `two = 2` THEN
 548       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 549       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 550       FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 551       REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ;
 552                   GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC]) in
 553     let rec NUM_SHIFT_CONV k tm =
 554       if k <= 0 then INST [tm,n_tm] pth_base else
 555       match tm with
 556         Comb(_,Comb(_,Comb(_,Comb(_,_)))) when k >= 4 ->
 557           let i,ntm = topsplit tm in
 558           let th1 = NUM_SHIFT_CONV (k - 4) ntm in
 559           (match concl th1 with
 560                Comb(_,Comb(Comb(_,Const("_0",_)),Comb(Comb(_,ptm),btm))) ->
 561                   let th2 = Array.get pths_0 i in
 562                   let th3 = INST [ntm,n_tm; btm,b_tm; ptm,p_tm] th2 in
 563                   EQ_MP th3 th1
 564              | Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) ->
 565                   let th2 = Array.get pths_1 i in
 566                   let th3 = INST[ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] th2 in
 567                   EQ_MP th3 th1)
 568       | Comb(Const("BIT0",_),ntm) ->
 569             let th1 = NUM_SHIFT_CONV (k - 1) ntm in
 570             (match concl th1 with
 571                Comb(_,Comb(Comb(_,Const("_0",_)),Comb(Comb(_,ptm),btm))) ->
 572                  EQ_MP (INST [ntm,n_tm; btm,b_tm; ptm,p_tm] pth_z) th1
 573              | Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) ->
 574                  EQ_MP
 575                   (INST[ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] pth_0) th1)
 576       | Comb(Const("BIT1",_),ntm) ->
 577             let th1 = NUM_SHIFT_CONV (k - 1) ntm in
 578             (match concl th1 with
 579                Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) ->
 580                  EQ_MP
 581                   (INST [ntm,n_tm; atm,a_tm; btm,b_tm; ptm,p_tm] pth_1) th1)
 582       | Const("_0",_) ->
 583             let th1 = NUM_SHIFT_CONV (k - 1) tm in
 584             (match concl th1 with
 585                Comb(_,Comb(Comb(_,atm),Comb(Comb(_,ptm),btm))) ->
 586                  EQ_MP (INST [atm,a_tm; btm,b_tm; ptm,p_tm] pth_triv)
 587                        th1)
 588       | _ -> failwith "malformed numeral" in
 589     NUM_SHIFT_CONV in
 590   let NUM_UNSHIFT_CONV =
 591     let pth_triv = (STANDARDIZE o prove)
 592      (`a + p * _0 = a`,
 593       SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN
 594       REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES])
 595     and pth_base = (STANDARDIZE o prove)
 596      (`a + BIT1 _0 * b = a + b`,
 597       SUBST1_TAC(SYM(SPEC `BIT1 _0` NUMERAL)) THEN
 598       REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES])
 599     and pth_0 = (STANDARDIZE o prove)
 600      (`BIT0 a + BIT0 p * b = BIT0(a + p * b)`,
 601       REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN
 602       REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB])
 603     and pth_1 = (STANDARDIZE o prove)
 604      (`BIT1 a + BIT0 p * b = BIT1(a + p * b)`,
 605       REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2] THEN
 606       REWRITE_TAC[ADD_CLAUSES; SUC_INJ] THEN
 607       REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 608       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ])
 609     and pth_z = (STANDARDIZE o prove)
 610      (`_0 + BIT0 p * b = BIT0(_0 + p * b)`,
 611       SUBST1_TAC(SYM(SPEC `_0` NUMERAL)) THEN
 612       REWRITE_TAC[BIT1; BIT0] THEN REWRITE_TAC[ADD_CLAUSES] THEN
 613       REWRITE_TAC[RIGHT_ADD_DISTRIB])
 614     and puths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
 615        (`(a + p * b = n <=>
 616           BIT0(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 617           BIT0(BIT0(BIT0(BIT0 n)))) /\
 618          (a + p * b = n <=>
 619           BIT1(BIT0(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 620           BIT1(BIT0(BIT0(BIT0 n)))) /\
 621          (a + p * b = n <=>
 622           BIT0(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 623           BIT0(BIT1(BIT0(BIT0 n)))) /\
 624          (a + p * b = n <=>
 625           BIT1(BIT1(BIT0(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 626           BIT1(BIT1(BIT0(BIT0 n)))) /\
 627          (a + p * b = n <=>
 628           BIT0(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 629           BIT0(BIT0(BIT1(BIT0 n)))) /\
 630          (a + p * b = n <=>
 631           BIT1(BIT0(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 632           BIT1(BIT0(BIT1(BIT0 n)))) /\
 633          (a + p * b = n <=>
 634           BIT0(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 635           BIT0(BIT1(BIT1(BIT0 n)))) /\
 636          (a + p * b = n <=>
 637           BIT1(BIT1(BIT1(BIT0 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 638           BIT1(BIT1(BIT1(BIT0 n)))) /\
 639          (a + p * b = n <=>
 640           BIT0(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 641           BIT0(BIT0(BIT0(BIT1 n)))) /\
 642          (a + p * b = n <=>
 643           BIT1(BIT0(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 644           BIT1(BIT0(BIT0(BIT1 n)))) /\
 645          (a + p * b = n <=>
 646           BIT0(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 647           BIT0(BIT1(BIT0(BIT1 n)))) /\
 648          (a + p * b = n <=>
 649           BIT1(BIT1(BIT0(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 650           BIT1(BIT1(BIT0(BIT1 n)))) /\
 651          (a + p * b = n <=>
 652           BIT0(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 653           BIT0(BIT0(BIT1(BIT1 n)))) /\
 654          (a + p * b = n <=>
 655           BIT1(BIT0(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 656           BIT1(BIT0(BIT1(BIT1 n)))) /\
 657          (a + p * b = n <=>
 658           BIT0(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 659           BIT0(BIT1(BIT1(BIT1 n)))) /\
 660          (a + p * b = n <=>
 661           BIT1(BIT1(BIT1(BIT1 a))) + BIT0(BIT0(BIT0(BIT0 p))) * b =
 662           BIT1(BIT1(BIT1(BIT1 n))))`,
 663       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
 664       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT0) THEN
 665       MP_TAC(REWRITE_RULE[GSYM MULT_2] BIT1) THEN
 666       ABBREV_TAC `two = 2` THEN
 667       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 668       DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 669       FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 670       REWRITE_TAC[ADD_CLAUSES; SUC_INJ; EQ_MULT_LCANCEL; ARITH_EQ;
 671                   GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC]) in
 672     let puths_2 = Array.of_list
 673      (map (fun i -> let th1 = Array.get puths_1 (i mod 16)
 674                     and th2 = Array.get puths_1 (i / 16) in
 675                     let th3 = GEN_REWRITE_RULE RAND_CONV [th1] th2 in
 676                     STANDARDIZE th3) (0--255)) in
 677     let rec NUM_UNSHIFT_CONV tm =
 678       match tm with
 679         Comb(Comb(Const("+",_),atm),Comb(Comb(Const("*",_),ptm),btm)) ->
 680          (match (atm,ptm,btm) with
 681             (_,_,Const("_0",_)) ->
 682                 INST [atm,a_tm; ptm,p_tm] pth_triv
 683           | (_,Comb(Const("BIT1",_),Const("_0",_)),_) ->
 684                 let th1 = INST [atm,a_tm; btm,b_tm] pth_base in
 685                 let Comb(_,Comb(Comb(_,mtm),ntm)) = concl th1 in
 686                 TRANS th1 (NUM_ADD_RULE mtm ntm)
 687           | (Comb(_,Comb(_,Comb(_,Comb(_,atm')))),
 688               Comb(_,Comb(_,Comb(_,Comb(_,(Comb(_,_) as ptm'))))),_) ->
 689                 let i,_ = topsplit atm in
 690                 (match (atm',ptm') with
 691                    (Comb(_,Comb(_,Comb(_,Comb(_,atm'')))),
 692                       Comb(_,Comb(_,Comb(_,Comb(_,(Comb(_,_) as ptm'')))))) ->
 693                      let j,_ = topsplit atm' in
 694                      let tm' = mk_comb(mk_comb(add_tm,atm''),
 695                                        mk_comb(mk_comb(mul_tm,ptm''),btm)) in
 696                      let th1 = NUM_UNSHIFT_CONV tm' in
 697                      let th2 = INST [atm'',a_tm; ptm'',p_tm; btm,b_tm;
 698                                      rand(concl th1),n_tm]
 699                                     (Array.get puths_2 (16 * j + i)) in
 700                      EQ_MP th2 th1
 701                  | _ ->
 702                    let tm' = mk_comb(mk_comb(add_tm,atm'),
 703                                      mk_comb(mk_comb(mul_tm,ptm'),btm)) in
 704                    let th1 = NUM_UNSHIFT_CONV tm' in
 705                    let th2 = INST [atm',a_tm; ptm',p_tm; btm,b_tm;
 706                                    rand(concl th1),n_tm]
 707                                   (Array.get puths_1 i) in
 708                    EQ_MP th2 th1)
 709           | (Const("_0",_),Comb(Const("BIT0",_),qtm),_) ->
 710                 let th1 = INST [btm,b_tm; qtm,p_tm] pth_z in
 711                 CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1
 712           | (Comb(Const("BIT0",_),ctm),Comb(Const("BIT0",_),qtm),_) ->
 713                 let th1 = INST [ctm,a_tm; btm,b_tm; qtm,p_tm] pth_0 in
 714                 CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1
 715           | (Comb(Const("BIT1",_),ctm),Comb(Const("BIT0",_),qtm),_) ->
 716                 let th1 = INST [ctm,a_tm; btm,b_tm; qtm,p_tm] pth_1 in
 717                 CONV_RULE(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV)) th1
 718           | _ -> failwith "malformed numeral")
 719       | _ -> failwith "malformed numeral" in
 720     NUM_UNSHIFT_CONV in
 721   let NUM_SQUARE_RULE =
 722     let pth_0 = (STANDARDIZE o prove)
 723      (`_0 EXP 2 = _0`,
 724       MESON_TAC[NUMERAL; REWRITE_CONV[ARITH] `0 EXP 2`])
 725     and pth_1 = (STANDARDIZE o prove)
 726      (`(BIT1 _0) EXP 2 = BIT1 _0`,
 727       MESON_TAC[NUMERAL; REWRITE_CONV[ARITH] `1 EXP 2`])
 728     and pth_even = (STANDARDIZE o prove)
 729      (`m EXP 2 = n <=> (BIT0 m) EXP 2 = BIT0(BIT0 n)`,
 730       ABBREV_TAC `two = 2` THEN
 731       REWRITE_TAC[BIT0] THEN EXPAND_TAC "two" THEN
 732       REWRITE_TAC[GSYM MULT_2] THEN REWRITE_TAC[EXP_2] THEN
 733       REWRITE_TAC[AC MULT_AC `(2 * m) * (2 * n) = 2 * 2 * m * n`] THEN
 734       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ])
 735     and pth_odd = (STANDARDIZE o prove)
 736      (`m EXP 2 = n <=> (BIT1 m) EXP 2 = BIT1(BIT0(m + n))`,
 737       ABBREV_TAC `two = 2` THEN
 738       REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
 739       EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN
 740       REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
 741       REWRITE_TAC[SUC_INJ; GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 742       REWRITE_TAC[AC ADD_AC `(m + m * 2 * m) + m = m * 2 * m + m + m`] THEN
 743       REWRITE_TAC[GSYM MULT_2; AC MULT_AC `m * 2 * m = 2 * m * m`] THEN
 744       REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 745       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ] THEN
 746       GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ADD_SYM] THEN
 747       REWRITE_TAC[EQ_ADD_RCANCEL])
 748     and pth_qstep = (UNDISCH o STANDARDIZE o prove)
 749      (`n + BIT1 _0 = m /\
 750        m EXP 2 = p /\
 751        m + a = BIT0(BIT0 p)
 752        ==> (BIT1(BIT1(BIT1 n))) EXP 2 = BIT1(BIT0(BIT0(BIT0 a)))`,
 753       ABBREV_TAC `two = 2` THEN
 754       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
 755       REWRITE_TAC[BIT1; BIT0] THEN EXPAND_TAC "two" THEN
 756       REWRITE_TAC[GSYM MULT_2] THEN
 757       REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB; GSYM ADD_ASSOC] THEN
 758       REWRITE_TAC[MULT_ASSOC] THEN REWRITE_TAC[ARITH] THEN
 759       REWRITE_TAC[IMP_CONJ] THEN
 760       DISCH_THEN(SUBST1_TAC o SYM) THEN
 761       DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_TAC THEN
 762       MATCH_MP_TAC(MESON[EQ_ADD_LCANCEL]
 763        `!m:num. m + n = m + p ==> n = p`) THEN
 764       EXISTS_TAC `16 * (n + 1)` THEN
 765       ASM_REWRITE_TAC[ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 766       EXPAND_TAC "two" THEN REWRITE_TAC[EXP_2] THEN
 767       REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
 768       REWRITE_TAC[MULT_CLAUSES; MULT_ASSOC] THEN
 769       REWRITE_TAC[AC MULT_AC `(8 * n) * NUMERAL p = (8 * NUMERAL p) * n`] THEN
 770       REWRITE_TAC[ARITH] THEN
 771       REWRITE_TAC[AC ADD_AC
 772          `(n + 16) + p + q + 49 = (n + p + q) + (16 + 49)`] THEN
 773       REWRITE_TAC[GSYM ADD_ASSOC] THEN REWRITE_TAC[ARITH] THEN
 774       REWRITE_TAC[ADD_ASSOC; EQ_ADD_RCANCEL] THEN
 775       REWRITE_TAC[GSYM ADD_ASSOC; GSYM MULT_2; MULT_ASSOC] THEN
 776       ONCE_REWRITE_TAC[AC ADD_AC `a + b + c:num = b + a + c`] THEN
 777       REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
 778       REWRITE_TAC[ARITH])
 779     and pth_rec = (UNDISCH o STANDARDIZE o prove)
 780      (`n = l + p * h /\
 781        h + l = m /\
 782        h EXP 2 = a /\
 783        l EXP 2 = c /\
 784        m EXP 2 = d /\
 785        a + c = e /\
 786        e + b = d
 787        ==> n EXP 2 = c + p * (b + p * a)`,
 788       REWRITE_TAC[IMP_CONJ] THEN
 789       DISCH_THEN SUBST1_TAC THEN
 790       REPLICATE_TAC 5 (DISCH_THEN(SUBST1_TAC o SYM)) THEN
 791       REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
 792       REWRITE_TAC[MULT_AC] THEN CONV_TAC(BINOP_CONV NUM_CANCEL_CONV) THEN
 793       DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
 794       REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC])
 795     and pth_toom3 = (STANDARDIZE o prove)
 796      (`h EXP 2 = e /\
 797        l EXP 2 = a /\
 798        (l + BIT1 _0 * (m + BIT1 _0 * h)) EXP 2 =
 799        a +  BIT1 _0 * (b +  BIT1 _0 * (c +  BIT1 _0 * (d +  BIT1 _0 * e))) /\
 800        (l + BIT0(BIT1 _0) * (m + BIT0(BIT1 _0) * h)) EXP 2 =
 801        a + BIT0(BIT1 _0) * (b + BIT0(BIT1 _0) *
 802        (c + BIT0(BIT1 _0) * (d + BIT0(BIT1 _0) * e))) /\
 803        (h + BIT0(BIT1 _0) * (m + BIT0(BIT1 _0) * l)) EXP 2 =
 804        e + BIT0(BIT1 _0) * (d + BIT0(BIT1 _0) *
 805        (c + BIT0(BIT1 _0) * (b + BIT0(BIT1 _0) * a)))
 806        ==> (l + p * (m + p * h)) EXP 2 =
 807            a + p * (b + p * (c + p * (d + p * e)))`,
 808       ABBREV_TAC `two = 2` THEN
 809       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
 810       REWRITE_TAC[BIT1; BIT0] THEN
 811       EXPAND_TAC "two" THEN REWRITE_TAC[GSYM MULT_2] THEN
 812       REWRITE_TAC[ARITH] THEN
 813       SUBGOAL_THEN
 814        `!p x y z. (x + p * (y + p * z)) EXP 2 =
 815                   x * x + p * (2 * x * y + p * ((2 * x * z + y * y) +
 816                             p * (2 * y * z + p * z * z)))`
 817        (fun th -> REWRITE_TAC[th])
 818       THENL
 819        [REWRITE_TAC[EXP_2; MULT_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
 820         REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC];
 821         REWRITE_TAC[EXP_2]] THEN
 822       MAP_EVERY ABBREV_TAC
 823        [`a':num = l * l`;  `b' = 2 * l * m`; `c' = 2 * l * h + m * m`;
 824         `d' = 2 * m * h`; `e':num = h * h`] THEN
 825       SUBST1_TAC(AC MULT_AC `2 * m * l = 2 * l * m`) THEN
 826       SUBST1_TAC(AC MULT_AC `2 * h * l = 2 * l * h`) THEN
 827       SUBST1_TAC(AC MULT_AC `2 * h * m = 2 * m * h`) THEN
 828       ASM_REWRITE_TAC[] THEN EXPAND_TAC "two" THEN
 829       POP_ASSUM_LIST(K ALL_TAC) THEN
 830       ASM_CASES_TAC `a':num = a` THEN ASM_REWRITE_TAC[] THEN
 831       ASM_CASES_TAC `e':num = e` THEN ASM_REWRITE_TAC[] THEN
 832       POP_ASSUM_LIST(K ALL_TAC) THEN
 833       REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL] THEN
 834       REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN
 835       REWRITE_TAC[ARITH] THEN
 836       REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
 837       REWRITE_TAC[ADD_ASSOC; EQ_ADD_RCANCEL] THEN
 838       REWRITE_TAC[GSYM ADD_ASSOC] THEN DISCH_TAC THEN
 839       FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[]
 840        `b = b' /\ c = c' /\ d = d'
 841         ==> 5 * b + c' + d' = 5 * b' + c + d`)) THEN
 842       REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN
 843       REWRITE_TAC(map (fun k ->
 844           SYM(REWRITE_CONV[ARITH_SUC]
 845           (mk_comb(suc_tm,mk_small_numeral(k - 1)))))
 846          (1--5)) THEN
 847       REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 848       CONV_TAC(LAND_CONV NUM_CANCEL_CONV) THEN DISCH_THEN SUBST_ALL_TAC THEN
 849       FIRST_ASSUM(MP_TAC o MATCH_MP (MESON[]
 850        `b = b' /\ c = c' /\ d = d'
 851         ==> b + d':num = b' + d /\ 4 * b + d' = 4 * b' + d`)) THEN
 852       REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC] THEN
 853       REWRITE_TAC(map (fun k ->
 854           SYM(REWRITE_CONV[ARITH_SUC]
 855           (mk_comb(suc_tm,mk_small_numeral(k - 1)))))
 856          (1--4)) THEN
 857       REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 858       CONV_TAC(LAND_CONV(BINOP_CONV NUM_CANCEL_CONV)) THEN
 859       REWRITE_TAC[GSYM MULT_2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 860       REWRITE_TAC[GSYM(el 4 (CONJUNCTS MULT_CLAUSES))] THEN
 861       SIMP_TAC[EQ_MULT_LCANCEL; NOT_SUC])
 862     and pth_even3 = (STANDARDIZE o prove)
 863      (`m EXP 2 = n <=>
 864        (BIT0(BIT0(BIT0 m))) EXP 2 = BIT0(BIT0(BIT0(BIT0(BIT0(BIT0 n)))))`,
 865       ABBREV_TAC `two = 2` THEN
 866       REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN
 867       EXPAND_TAC "two" THEN REWRITE_TAC[EXP_2] THEN
 868       REWRITE_TAC[AC MULT_AC
 869        `(2 * 2 * 2 * m) * 2 * 2 * 2 * m = 2 * 2 * 2 * 2 * 2 * 2 * m * m`] THEN
 870       REWRITE_TAC[EQ_MULT_LCANCEL; ARITH_EQ]) in
 871     let NUM_UNSHIFT2_CONV =
 872       RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV) THENC NUM_UNSHIFT_CONV in
 873     let NUM_UNSHIFT3_CONV =
 874       RAND_CONV(RAND_CONV NUM_UNSHIFT2_CONV) THENC NUM_UNSHIFT_CONV in
 875     let NUM_UNSHIFT4_CONV =
 876       RAND_CONV(RAND_CONV NUM_UNSHIFT3_CONV) THENC NUM_UNSHIFT_CONV in
 877     let BINOP2_CONV conv1 conv2 = COMB2_CONV (RAND_CONV conv1) conv2 in
 878     let TOOM3_CONV = BINOP2_CONV
 879       (LAND_CONV NUM_UNSHIFT2_CONV) NUM_UNSHIFT4_CONV in
 880     let rec GEN_NUM_SQUARE_RULE w z tm =
 881       match tm with
 882         Const("_0",_) -> pth_0
 883       | Comb(Const("BIT0",_),mtm) ->
 884            (match mtm with
 885               Comb(Const("BIT0",_),Comb(Const("BIT0",_),ptm)) ->
 886                  let th1 = GEN_NUM_SQUARE_RULE w (z - 3) ptm in
 887                  let ntm = rand(concl th1) in
 888                  EQ_MP (INST [ptm,m_tm; ntm,n_tm] pth_even3) th1
 889             | _ ->
 890                  let th1 = GEN_NUM_SQUARE_RULE w (z - 1) mtm in
 891                  let ntm = rand(concl th1) in
 892                  EQ_MP (INST [mtm,m_tm; ntm,n_tm] pth_even) th1)
 893       | Comb(Const("BIT1",_),mtm) ->
 894             if mtm = zero_tm then pth_1 else
 895             if (w < 100 or z < 20) & w + z < 150 then
 896               match mtm with
 897                 Comb(Const("BIT1",_),Comb(Const("BIT1",_),ntm)) ->
 898                     let th1 = NUM_ADD_RULE ntm one_tm in
 899                     let mtm = rand(concl th1) in
 900                     let th2 = NUM_SQUARE_RULE mtm in
 901                     let ptm = rand(concl th2) in
 902                     let atm = subbn
 903                       (mk_comb(BIT0_tm,mk_comb(BIT0_tm,ptm))) mtm in
 904                     let th3 = NUM_ADD_RULE mtm atm in
 905                     let th4 = INST
 906                       [atm,a_tm; mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_qstep in
 907                     QUICK_PROVE_HYP (CONJ th1 (CONJ th2 th3)) th4
 908               | _ ->
 909                     let th1 = GEN_NUM_SQUARE_RULE (w - 1) z mtm in
 910                     let ntm = rand(concl th1) in
 911                     let th2 = EQ_MP (INST [mtm,m_tm; ntm,n_tm] pth_odd) th1 in
 912                     (match concl th2 with
 913                       Comb(_,Comb(_,Comb(_,Comb(Comb(_,ptm),qtm)))) ->
 914                         let th3 = NUM_ADD_RULE ptm qtm in
 915                         TRANS th2 (AP_BIT1 (AP_BIT0 th3)))
 916             else if w + z < 800 then
 917               let k2 = (w + z) / 2 in
 918               let th1 = NUM_SHIFT_CONV k2 tm in
 919               let Comb(Comb(_,ltm),Comb(Comb(_,ptm),htm)) = rand(concl th1) in
 920               let th2 = NUM_ADD_RULE htm ltm in
 921               let mtm = rand(concl th2) in
 922               let th3 = NUM_SQUARE_RULE htm
 923               and th4 = NUM_SQUARE_RULE ltm
 924               and th5 = NUM_SQUARE_RULE mtm in
 925               let atm = rand(concl th3)
 926               and ctm = rand(concl th4)
 927               and dtm = rand(concl th5) in
 928               let th6 = NUM_ADD_RULE atm ctm in
 929               let etm = rand(concl th6) in
 930               let btm = subbn dtm etm in
 931               let th7 = NUM_ADD_RULE etm btm in
 932               let dtm = rand(concl th7) in
 933               let th8 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; etm,e_tm;
 934                               htm,h_tm; ltm,l_tm; mtm,m_tm; tm,n_tm; ptm,p_tm]
 935                         pth_rec in
 936               let th9 = QUICK_PROVE_HYP (end_itlist CONJ
 937                    [th1;th2;th3;th4;th5;th6;th7]) th8 in
 938               CONV_RULE(RAND_CONV(RAND_CONV(RAND_CONV NUM_UNSHIFT_CONV) THENC
 939                                   NUM_UNSHIFT_CONV)) th9
 940             else
 941               let k3 = (w + z) / 3 in
 942               let th0 = (NUM_SHIFT_CONV k3 THENC
 943                          RAND_CONV(RAND_CONV(NUM_SHIFT_CONV k3))) tm in
 944               let Comb(Comb(_,ltm),Comb(Comb(_,ptm),
 945                    Comb(Comb(_,mtm),Comb(Comb(_,_),htm)))) = rand(concl th0) in
 946               let th1 = NUM_SQUARE_RULE htm
 947               and th2 = NUM_SQUARE_RULE ltm in
 948               let atm = rand(concl th2) and etm = rand(concl th1) in
 949               let lnum = dest_raw_numeral ltm
 950               and mnum = dest_raw_numeral mtm
 951               and hnum = dest_raw_numeral htm in
 952               let btm = rand(mk_numeral(num_2 */ lnum */ mnum))
 953               and ctm = rand(mk_numeral(mnum */ mnum +/ num_2 */ lnum */ hnum))
 954               and dtm = rand(mk_numeral(num_2 */ hnum */ mnum)) in
 955               let th = INST
 956                 [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm; etm,e_tm;
 957                  htm,h_tm; mtm,m_tm; ltm,l_tm; ptm,p_tm] pth_toom3 in
 958               let th' = CONV_RULE
 959                (BINOP2_CONV
 960                 (RAND_CONV(RAND_CONV
 961                  (BINOP2_CONV TOOM3_CONV (BINOP2_CONV TOOM3_CONV TOOM3_CONV))))
 962                 TOOM3_CONV) th in
 963               let [tm3;tm4;tm5] = conjuncts(rand(rand(lhand(concl th')))) in
 964               let th3 = NUM_SQUARE_RULE (lhand(lhand tm3))
 965               and th4 = NUM_SQUARE_RULE (lhand(lhand tm4))
 966               and th5 = NUM_SQUARE_RULE (lhand(lhand tm5)) in
 967               MP th' (end_itlist CONJ [th1;th2;th3;th4;th5])
 968     and NUM_SQUARE_RULE tm =
 969       let w,z = bitcounts tm in GEN_NUM_SQUARE_RULE w z tm in
 970     NUM_SQUARE_RULE in
 971   let NUM_MUL_RULE =
 972     let QUICK_PROVE_HYP ath bth =
 973       EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath
 974     and pth_0l,pth_0r = (CONJ_PAIR o STANDARDIZE o prove)
 975      (`_0 * n = _0 /\ m * _0 = _0`,
 976       MESON_TAC[NUMERAL; MULT_CLAUSES])
 977     and pth_1l,pth_1r = (CONJ_PAIR o STANDARDIZE o prove)
 978      (`(BIT1 _0) * n = n /\ m * (BIT1 _0) = m`,
 979       MESON_TAC[NUMERAL; MULT_CLAUSES])
 980     and pth_evenl,pth_evenr = (CONJ_PAIR o STANDARDIZE o prove)
 981      (`(m * n = p <=> (BIT0 m) * n = BIT0 p) /\
 982        (m * n = p <=> m * BIT0 n = BIT0 p)`,
 983       REWRITE_TAC[BIT0] THEN REWRITE_TAC[GSYM MULT_2] THEN
 984       REWRITE_TAC[AC MULT_AC `m * 2 * n = 2 * m * n`] THEN
 985       REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; ARITH_EQ])
 986     and pth_oddl,pth_oddr = (CONJ_PAIR o STANDARDIZE o prove)
 987      (`(m * n = p <=> BIT1 m * n = BIT0 p + n) /\
 988        (m * n = p <=> m * BIT1 n = BIT0 p + m)`,
 989       REWRITE_TAC[BIT0; BIT1] THEN REWRITE_TAC[GSYM MULT_2] THEN
 990       REWRITE_TAC[MULT_CLAUSES] THEN
 991       REWRITE_TAC[MESON[MULT_AC; ADD_SYM] `m + m * 2 * n = 2 * m * n + m`] THEN
 992       REWRITE_TAC[GSYM MULT_ASSOC; EQ_MULT_LCANCEL; EQ_ADD_RCANCEL] THEN
 993       REWRITE_TAC[ARITH_EQ]) in
 994     let pth_oo1 = (UNDISCH_ALL o STANDARDIZE o prove)
 995      (`n + p = m /\ SUC(m + n) = a /\ p EXP 2 = b /\ a EXP 2 = c /\ b + d = c
 996         ==> ((BIT1 m) * (BIT1 n) = d)`,
 997       ABBREV_TAC `two = 2` THEN REWRITE_TAC[BIT1; IMP_CONJ] THEN
 998       FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 999       REWRITE_TAC[EXP_2; GSYM MULT_2] THEN
1000       REPLICATE_TAC 4 (DISCH_THEN(SUBST1_TAC o SYM)) THEN
1001       REWRITE_TAC[ADD1; AC ADD_AC `((n + p) + n) + 1 = (p + (n + n)) + 1`] THEN
1002       REWRITE_TAC[GSYM MULT_2] THEN
1003       REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1004       REWRITE_TAC[GSYM ADD_ASSOC; MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
1005       DISCH_THEN SUBST1_TAC THEN
1006       REWRITE_TAC[MULT_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
1007       REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]) in
1008     let pth_oo2 = PURE_ONCE_REWRITE_RULE[MULT_SYM]
1009                    (INST [n_tm,m_tm; m_tm,n_tm] pth_oo1) in
1010     let pth_recodel = (UNDISCH_ALL o STANDARDIZE o prove)
1011      (`SUC(_0 + m) = p ==> (p * n = a + n <=> m * n = a)`,
1012       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
1013       DISCH_THEN(SUBST1_TAC o SYM) THEN
1014       REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; EQ_ADD_RCANCEL])
1015     and pth_recoder = (UNDISCH_ALL o STANDARDIZE o prove)
1016      (`SUC(_0 + n) = p ==> (m * p = a + m <=> m * n = a)`,
1017       ONCE_REWRITE_TAC[MULT_SYM] THEN
1018       SUBST1_TAC(MESON[NUMERAL] `_0 = 0`) THEN
1019       DISCH_THEN(SUBST1_TAC o SYM) THEN
1020       REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; EQ_ADD_RCANCEL]) in
1021     let rec NUM_MUL_RULE k l tm tm' =
1022       match (tm,tm') with
1023         (Const("_0",_),_) -> INST [tm',n_tm] pth_0l
1024       | (_,Const("_0",_)) -> INST [tm,m_tm] pth_0r
1025       | (Comb(Const("BIT1",_),Const("_0",_)),_) -> INST [tm',n_tm] pth_1l
1026       | (_,Comb(Const("BIT1",_),Const("_0",_))) -> INST [tm,m_tm] pth_1r
1027       | (Comb(Const("BIT0",_),mtm),_) ->
1028             let th0 = NUM_MUL_RULE (k - 1) l mtm tm' in
1029             let th1 = INST
1030              [mtm,m_tm; tm',n_tm; rand(concl th0),p_tm] pth_evenl in
1031             EQ_MP th1 th0
1032       | (_,Comb(Const("BIT0",_),ntm)) ->
1033             let th0 = NUM_MUL_RULE k (l - 1) tm ntm in
1034             let th1 = INST
1035              [tm,m_tm; ntm,n_tm; rand(concl th0),p_tm] pth_evenr in
1036             EQ_MP th1 th0
1037       | (Comb(Const("BIT1",_),mtm),Comb(Const("BIT1",_),ntm)) ->
1038           if k <= 50 or l <= 50 or
1039              Int k */ Int k <=/ Int l or
1040              Int l */ Int l <= Int k then
1041             match (mtm,ntm) with
1042               (Comb(Const("BIT1",_),Comb(Const("BIT1",_),_)),_) ->
1043                  let th1 = NUM_ADC_RULE zero_tm tm in
1044                  let ptm = rand(concl th1) in
1045                  let th2 = NUM_MUL_RULE k l ptm tm' in
1046                  let atm = subbn (rand(concl th2)) tm' in
1047                  let th3 = INST [tm,m_tm; tm',n_tm; ptm,p_tm; atm,a_tm]
1048                                 pth_recodel in
1049                  let th4 = PROVE_HYP th1 th3 in
1050                  EQ_MP th4 (TRANS th2 (SYM(NUM_ADD_RULE atm tm')))
1051             | (_,Comb(Const("BIT1",_),Comb(Const("BIT1",_),_))) ->
1052                  let th1 = NUM_ADC_RULE zero_tm tm' in
1053                  let ptm = rand(concl th1) in
1054                  let th2 = NUM_MUL_RULE k l tm ptm in
1055                  let atm = subbn (rand(concl th2)) tm in
1056                  let th3 = INST [tm,m_tm; tm',n_tm; ptm,p_tm; atm,a_tm]
1057                                 pth_recoder in
1058                  let th4 = PROVE_HYP th1 th3 in
1059                  EQ_MP th4 (TRANS th2 (SYM(NUM_ADD_RULE atm tm)))
1060             | _ ->
1061                  if k <= l then
1062                    let th0 = NUM_MUL_RULE (k - 1) l mtm tm' in
1063                    let ptm = rand(concl th0) in
1064                    let th1 =
1065                     EQ_MP (INST [mtm,m_tm; tm',n_tm; ptm,p_tm] pth_oddl) th0 in
1066                    let tm1 = lhand(rand(concl th1)) in
1067                    TRANS th1 (NUM_ADD_RULE tm1 tm')
1068                  else
1069                    let th0 = NUM_MUL_RULE k (l - 1) tm ntm in
1070                    let ptm = rand(concl th0) in
1071                    let th1 =
1072                      EQ_MP (INST [tm,m_tm; ntm,n_tm; ptm,p_tm] pth_oddr) th0 in
1073                    let tm1 = lhand(rand(concl th1)) in
1074                    TRANS th1 (NUM_ADD_RULE tm1 tm)
1075           else
1076              let mval = dest_raw_numeral mtm
1077              and nval = dest_raw_numeral ntm in
1078              if nval <=/ mval then
1079                let ptm = rand(mk_numeral(mval -/ nval)) in
1080                let th2 = NUM_ADD_RULE ntm ptm
1081                and th3 = NUM_ADC_RULE mtm ntm in
1082                let atm = rand(concl th3) in
1083                let th4 = NUM_SQUARE_RULE ptm in
1084                let btm = rand(concl th4) in
1085                let th5 = NUM_SQUARE_RULE atm in
1086                let ctm = rand(concl th5) in
1087                let dtm = subbn ctm btm in
1088                let th6 = NUM_ADD_RULE btm dtm in
1089                let th1 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm;
1090                                mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_oo1 in
1091                QUICK_PROVE_HYP  (end_itlist CONJ
1092                    [th2;th3;th4;th5;th6]) th1
1093              else
1094                let ptm = rand(mk_numeral(nval -/ mval)) in
1095                let th2 = NUM_ADD_RULE mtm ptm
1096                and th3 = NUM_ADC_RULE ntm mtm in
1097                let atm = rand(concl th3) in
1098                let th4 = NUM_SQUARE_RULE ptm in
1099                let btm = rand(concl th4) in
1100                let th5 = NUM_SQUARE_RULE atm in
1101                let ctm = rand(concl th5) in
1102                let dtm = subbn ctm btm in
1103                let th6 = NUM_ADD_RULE btm dtm in
1104                let th1 = INST [atm,a_tm; btm,b_tm; ctm,c_tm; dtm,d_tm;
1105                                mtm,m_tm; ntm,n_tm; ptm,p_tm] pth_oo2 in
1106                QUICK_PROVE_HYP  (end_itlist CONJ
1107                    [th2;th3;th4;th5;th6]) th1
1108       | _ -> failwith "NUM_MUL_RULE" in
1109     NUM_MUL_RULE in
1110   let NUM_MULT_CONV' =
1111     let pth_refl = (STANDARDIZE o MESON[EXP_2])
1112       `m EXP 2 = p <=> m * m = p` in
1113     fun tm ->
1114       match tm with
1115         Comb(Comb(Const("*",_),mtm),ntm) ->
1116             if Pervasives.compare mtm ntm = 0 then
1117               let th1 = NUM_SQUARE_RULE mtm in
1118               let ptm = rand(concl th1) in
1119               EQ_MP (INST [mtm,m_tm;ptm,p_tm] pth_refl) th1
1120             else
1121               let w1,z1 = bitcounts mtm and w2,z2 = bitcounts ntm in
1122               NUM_MUL_RULE (w1+z1) (w2+z2) mtm ntm
1123     | _ -> failwith "NUM_MULT_CONV'" in
1124   let NUM_SUC_CONV =
1125     let pth = (STANDARDIZE o prove)
1126      (`SUC(_0 + m) = n <=> SUC(NUMERAL m) = NUMERAL n`,
1127       BINOP_TAC THEN MESON_TAC[NUMERAL; ADD_CLAUSES]) in
1128     fun tm ->
1129       match tm with
1130         Comb(Const("SUC",_),Comb(Const("NUMERAL",_),mtm))
1131         when wellformed mtm ->
1132           let th1 = NUM_ADC_RULE zero_tm mtm in
1133           let ntm = rand(concl th1) in
1134           EQ_MP(INST [mtm,m_tm; ntm,n_tm] pth) th1
1135       | _ -> failwith "NUM_SUC_CONV" in
1136   let NUM_ADD_CONV =
1137     let topthm_add = (STANDARDIZE o MESON[NUMERAL])
1138       `m + n = p <=> NUMERAL m + NUMERAL n = NUMERAL p` in
1139     fun tm ->
1140       match tm with
1141         Comb(Comb(Const("+",_),Comb(Const("NUMERAL",_),mtm)),
1142           Comb(Const("NUMERAL",_),ntm))
1143         when wellformed mtm & wellformed ntm ->
1144         let th1 = NUM_ADD_RULE mtm ntm in
1145         let ptm = rand(concl th1) in
1146         let th2 = INST [mtm,m_tm; ntm,n_tm; ptm,p_tm] topthm_add in
1147         EQ_MP th2 th1
1148       | _ -> failwith "NUM_ADD_CONV" in
1149   let NUM_MULT_CONV =
1150     let topthm_mul = (STANDARDIZE o MESON[NUMERAL])
1151       `m * n = p <=> NUMERAL m * NUMERAL n = NUMERAL p`
1152     and pth_refl = (STANDARDIZE o MESON[NUMERAL; EXP_2])
1153       `m EXP 2 = p <=> NUMERAL m * NUMERAL m = NUMERAL p` in
1154     fun tm ->
1155       match tm with
1156         Comb(Comb(Const("*",_),Comb(Const("NUMERAL",_),mtm)),
1157           Comb(Const("NUMERAL",_),ntm)) ->
1158             if Pervasives.compare mtm ntm = 0 then
1159               let th1 = NUM_SQUARE_RULE mtm in
1160               let ptm = rand(concl th1) in
1161               EQ_MP (INST [mtm,m_tm;ptm,p_tm] pth_refl) th1
1162             else
1163               let w1,z1 = bitcounts mtm and w2,z2 = bitcounts ntm in
1164               let th1 = NUM_MUL_RULE (w1+z1) (w2+z2) mtm ntm in
1165               let ptm = rand(concl th1) in
1166               let th2 = INST [mtm,m_tm; ntm,n_tm; ptm,p_tm] topthm_mul in
1167               EQ_MP th2 th1
1168       | _ -> failwith "NUM_MULT_CONV" in
1169   let NUM_EXP_CONV =
1170     let pth0 = (STANDARDIZE o prove)
1171      (`(m EXP n = p) ==> (p * p = a) ==> (m EXP (BIT0 n) = a)`,
1172        REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
1173        REWRITE_TAC[BIT0; EXP_ADD])
1174     and pth1 = (STANDARDIZE o prove)
1175      (`(m EXP n = p) ==> (p * p = b) ==> (m * b = a) ==> (m EXP (BIT1 n) = a)`,
1176       REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
1177       REWRITE_TAC[BIT1; EXP_ADD; EXP])
1178     and pth = (STANDARDIZE o prove)
1179      (`m EXP _0 = BIT1 _0`,
1180       MP_TAC (CONJUNCT1 EXP) THEN REWRITE_TAC[NUMERAL; BIT1] THEN
1181       DISCH_THEN MATCH_ACCEPT_TAC)
1182     and tth = (STANDARDIZE o prove)
1183      (`(NUMERAL m) EXP (NUMERAL n) = m EXP n`,
1184       REWRITE_TAC[NUMERAL])
1185     and fth = (STANDARDIZE o prove)
1186      (`m = NUMERAL m`,
1187       REWRITE_TAC[NUMERAL]) in
1188     let tconv = GEN_REWRITE_CONV I [tth] in
1189     let rec NUM_EXP_CONV l r =
1190       if r = zero_tm then INST [l,m_tm] pth else
1191       let b,r' = dest_comb r in
1192       if b = BIT0_tm then
1193         let th1 = NUM_EXP_CONV l r' in
1194         let tm1 = rand(concl th1) in
1195         let th2 = NUM_MULT_CONV' (mk_binop mul_tm tm1 tm1) in
1196         let tm2 = rand(concl th2) in
1197         MP (MP (INST [l,m_tm; r',n_tm; tm1,p_tm; tm2,a_tm] pth0) th1) th2
1198       else
1199         let th1 = NUM_EXP_CONV l r' in
1200         let tm1 = rand(concl th1) in
1201         let th2 = NUM_MULT_CONV' (mk_binop mul_tm tm1 tm1) in
1202         let tm2 = rand(concl th2) in
1203         let th3 = NUM_MULT_CONV' (mk_binop mul_tm l tm2) in
1204         let tm3 = rand(concl th3) in
1205         MP (MP (MP (INST [l,m_tm; r',n_tm; tm1,p_tm; tm2,b_tm; tm3,a_tm]
1206                          pth1) th1) th2) th3 in
1207     fun tm -> try let th = tconv tm in
1208                   let lop,r = dest_comb (rand(concl th)) in
1209                   let _,l = dest_comb lop in
1210                   if not (wellformed l & wellformed r) then failwith "" else
1211                   let th' = NUM_EXP_CONV l r in
1212                   let tm' = rand(concl th') in
1213                   TRANS (TRANS th th') (INST [tm',m_tm] fth)
1214               with Failure _ -> failwith "NUM_EXP_CONV" in
1215   let NUM_LT_CONV =
1216     let pth = (UNDISCH o STANDARDIZE o prove)
1217      (`SUC(m + n) = p ==> ((NUMERAL n < NUMERAL p) <=> T)`,
1218       REWRITE_TAC[NUMERAL; LT_EXISTS; ADD_CLAUSES] THEN
1219       MESON_TAC[ADD_SYM])
1220     and qth = (UNDISCH o STANDARDIZE o prove)
1221      (`m + p = n ==> (NUMERAL n < NUMERAL p <=> F)`,
1222       DISCH_THEN(SUBST1_TAC o SYM) THEN
1223       REWRITE_TAC[NOT_LT; NUMERAL] THEN
1224       MESON_TAC[LE_ADD; ADD_SYM])
1225     and rth = (STANDARDIZE o prove)
1226      (`NUMERAL n < NUMERAL n <=> F`,
1227       MESON_TAC[LT_REFL]) in
1228     fun tm ->
1229       match tm with
1230         Comb(Comb(Const("<",_),Comb(Const("NUMERAL",_),mtm)),
1231              Comb(Const("NUMERAL",_),ntm)) ->
1232           let rel = orderrelation mtm ntm in
1233           if rel = 0 then INST[ntm,n_tm] rth
1234           else if rel < 0 then
1235             let dtm = sbcbn ntm mtm in
1236             let th = NUM_ADC_RULE dtm mtm in
1237             QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth)
1238           else
1239             let dtm = subbn mtm ntm in
1240             let th = NUM_ADD_RULE dtm ntm in
1241             QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth)
1242       | _ -> failwith "NUM_LT_CONV"
1243   and NUM_LE_CONV =
1244     let pth = (UNDISCH o STANDARDIZE o prove)
1245      (`m + n = p ==> ((NUMERAL n <= NUMERAL p) <=> T)`,
1246       DISCH_THEN(SUBST1_TAC o SYM) THEN
1247       REWRITE_TAC[NUMERAL] THEN
1248       MESON_TAC[LE_ADD; ADD_SYM])
1249     and qth = (UNDISCH o STANDARDIZE o prove)
1250      (`SUC(m + p) = n ==> (NUMERAL n <= NUMERAL p <=> F)`,
1251       DISCH_THEN(SUBST1_TAC o SYM) THEN
1252       REWRITE_TAC[NUMERAL; NOT_LE; ADD_CLAUSES; LT_EXISTS] THEN
1253       MESON_TAC[ADD_SYM])
1254     and rth = (STANDARDIZE o prove)
1255      (`NUMERAL n <= NUMERAL n <=> T`,
1256       REWRITE_TAC[LE_REFL]) in
1257     fun tm ->
1258       match tm with
1259         Comb(Comb(Const("<=",_),Comb(Const("NUMERAL",_),mtm)),
1260              Comb(Const("NUMERAL",_),ntm)) ->
1261           let rel = orderrelation mtm ntm in
1262           if rel = 0 then INST[ntm,n_tm] rth
1263           else if rel < 0 then
1264             let dtm = subbn ntm mtm in
1265             let th = NUM_ADD_RULE dtm mtm in
1266             QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth)
1267           else
1268             let dtm = sbcbn mtm ntm in
1269             let th = NUM_ADC_RULE dtm ntm in
1270             QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth)
1271       | _ -> failwith "NUM_LE_CONV"
1272   and NUM_EQ_CONV =
1273     let pth = (UNDISCH o STANDARDIZE o prove)
1274      (`SUC(m + n) = p ==> ((NUMERAL n = NUMERAL p) <=> F)`,
1275       DISCH_THEN(SUBST1_TAC o SYM) THEN
1276       REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; DE_MORGAN_THM] THEN
1277       REWRITE_TAC[NOT_LE; LT_EXISTS; ADD_CLAUSES] THEN
1278       MESON_TAC[ADD_SYM])
1279     and qth = (UNDISCH o STANDARDIZE o prove)
1280      (`SUC(m + p) = n ==> ((NUMERAL n = NUMERAL p) <=> F)`,
1281       DISCH_THEN(SUBST1_TAC o SYM) THEN
1282       REWRITE_TAC[NUMERAL; GSYM LE_ANTISYM; DE_MORGAN_THM] THEN
1283       REWRITE_TAC[NOT_LE; LT_EXISTS; ADD_CLAUSES] THEN
1284       MESON_TAC[ADD_SYM])
1285     and rth = (STANDARDIZE o prove)
1286      (`(NUMERAL n = NUMERAL n) <=> T`,
1287       REWRITE_TAC[]) in
1288     fun tm ->
1289       match tm with
1290         Comb(Comb(Const("=",_),Comb(Const("NUMERAL",_),mtm)),
1291              Comb(Const("NUMERAL",_),ntm)) ->
1292           let rel = orderrelation mtm ntm in
1293           if rel = 0 then INST [ntm,n_tm] rth
1294           else if rel < 0 then
1295              let dtm = sbcbn ntm mtm in
1296              let th = NUM_ADC_RULE dtm mtm in
1297              QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] pth)
1298           else
1299              let dtm = sbcbn mtm ntm in
1300              let th = NUM_ADC_RULE dtm ntm in
1301              QUICK_PROVE_HYP th (INST [dtm,m_tm; mtm,n_tm; ntm,p_tm] qth)
1302       | _ -> failwith "NUM_EQ_CONV" in
1303   NUM_SUC_CONV,NUM_ADD_CONV,NUM_MULT_CONV,NUM_EXP_CONV,
1304   NUM_LT_CONV,NUM_LE_CONV,NUM_EQ_CONV;;
1305
1306 let NUM_GT_CONV = GEN_REWRITE_CONV I [GT] THENC NUM_LT_CONV;;
1307
1308 let NUM_GE_CONV = GEN_REWRITE_CONV I [GE] THENC NUM_LE_CONV;;
1309
1310 let NUM_PRE_CONV =
1311   let tth = prove
1312    (`PRE 0 = 0`,
1313     REWRITE_TAC[PRE]) in
1314   let pth = prove
1315    (`(SUC m = n) ==> (PRE n = m)`,
1316     DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[PRE])
1317   and m = `m:num` and n = `n:num` in
1318   let suc = `SUC` in
1319   let pre = `PRE` in
1320   fun tm -> try let l,r = dest_comb tm in
1321                 if not (l = pre) then fail() else
1322                 let x = dest_numeral r in
1323                 if x =/ Int 0 then tth else
1324                 let tm' = mk_numeral (x -/ Int 1) in
1325                 let th1 = NUM_SUC_CONV (mk_comb(suc,tm')) in
1326                 MP (INST [tm',m; r,n] pth) th1
1327             with Failure _ -> failwith "NUM_PRE_CONV";;
1328
1329 let NUM_SUB_CONV =
1330   let pth0 = prove
1331    (`p <= n ==> (p - n = 0)`,
1332     REWRITE_TAC[SUB_EQ_0])
1333   and pth1 = prove
1334    (`(m + n = p) ==> (p - n = m)`,
1335     DISCH_THEN(SUBST1_TAC o SYM) THEN
1336     REWRITE_TAC[ADD_SUB])
1337   and m = `m:num` and n = `n:num` and p = `p:num`
1338   and minus = `(-)`
1339   and plus = `(+)`
1340   and le = `(<=)` in
1341   fun tm -> try let l,r = dest_binop minus tm in
1342                 let ln = dest_numeral l
1343                 and rn = dest_numeral r in
1344                 if  ln <=/ rn then
1345                   let pth = INST [l,p; r,n] pth0
1346                   and th0 = EQT_ELIM(NUM_LE_CONV (mk_binop le l r)) in
1347                   MP pth th0
1348                 else
1349                   let kn = ln -/ rn in
1350                   let k = mk_numeral kn in
1351                   let pth = INST [k,m; l,p; r,n] pth1
1352                   and th0 = NUM_ADD_CONV (mk_binop plus k r) in
1353                   MP pth th0
1354             with Failure _ -> failwith "NUM_SUB_CONV";;
1355
1356 let NUM_DIV_CONV,NUM_MOD_CONV =
1357   let pth = prove
1358    (`(q * n + r = m) ==> r < n ==> (m DIV n = q) /\ (m MOD n = r)`,
1359     MESON_TAC[DIVMOD_UNIQ])
1360   and m = `m:num` and n = `n:num` and q = `q:num` and r = `r:num`
1361   and dtm = `(DIV)` and mtm = `(MOD)` in
1362   let NUM_DIVMOD_CONV x y =
1363     let k = quo_num x y
1364     and l = mod_num x y in
1365     let th0 = INST [mk_numeral x,m; mk_numeral y,n;
1366                     mk_numeral k,q; mk_numeral l,r] pth in
1367     let tm0 = lhand(lhand(concl th0)) in
1368     let th1 = (LAND_CONV NUM_MULT_CONV THENC NUM_ADD_CONV) tm0 in
1369     let th2 = MP th0 th1 in
1370     let tm2 = lhand(concl th2) in
1371     MP th2 (EQT_ELIM(NUM_LT_CONV tm2)) in
1372   (fun tm -> try let xt,yt = dest_binop dtm tm in
1373                  CONJUNCT1(NUM_DIVMOD_CONV (dest_numeral xt) (dest_numeral yt))
1374              with Failure _ -> failwith "NUM_DIV_CONV"),
1375   (fun tm -> try let xt,yt = dest_binop mtm tm in
1376                  CONJUNCT2(NUM_DIVMOD_CONV (dest_numeral xt) (dest_numeral yt))
1377              with Failure _ -> failwith "NUM_MOD_CONV");;
1378
1379 let NUM_FACT_CONV =
1380   let suc = `SUC`
1381   and mul = `(*)` in
1382   let pth_0 = prove
1383    (`FACT 0 = 1`,
1384     REWRITE_TAC[FACT])
1385   and pth_suc = prove
1386    (`(SUC x = y) ==> (FACT x = w) ==> (y * w = z) ==> (FACT y = z)`,
1387     REPEAT (DISCH_THEN(SUBST1_TAC o SYM)) THEN
1388     REWRITE_TAC[FACT])
1389   and w = `w:num` and x = `x:num` and y = `y:num` and z = `z:num` in
1390   let mksuc n =
1391     let n' = n -/ (Int 1) in
1392     NUM_SUC_CONV (mk_comb(suc,mk_numeral n')) in
1393   let rec NUM_FACT_CONV n =
1394     if n =/ Int 0 then pth_0 else
1395     let th0 = mksuc n in
1396     let tmx = rand(lhand(concl th0)) in
1397     let tm0 = rand(concl th0) in
1398     let th1 = NUM_FACT_CONV (n -/ Int 1) in
1399     let tm1 = rand(concl th1) in
1400     let th2 = NUM_MULT_CONV (mk_binop mul tm0 tm1) in
1401     let tm2 = rand(concl th2) in
1402     let pth = INST [tmx,x; tm0, y; tm1,w; tm2,z] pth_suc in
1403     MP (MP (MP pth th0) th1) th2 in
1404   fun tm ->
1405     try let l,r = dest_comb tm in
1406         if fst(dest_const l) = "FACT"
1407         then NUM_FACT_CONV (dest_numeral r)
1408         else fail()
1409     with Failure _ -> failwith "NUM_FACT_CONV";;
1410
1411 let NUM_MAX_CONV =
1412   REWR_CONV MAX THENC
1413   RATOR_CONV(RATOR_CONV(RAND_CONV NUM_LE_CONV)) THENC
1414   GEN_REWRITE_CONV I [COND_CLAUSES];;
1415
1416 let NUM_MIN_CONV =
1417   REWR_CONV MIN THENC
1418   RATOR_CONV(RATOR_CONV(RAND_CONV NUM_LE_CONV)) THENC
1419   GEN_REWRITE_CONV I [COND_CLAUSES];;
1420
1421 (* ------------------------------------------------------------------------- *)
1422 (* Final hack-together.                                                      *)
1423 (* ------------------------------------------------------------------------- *)
1424
1425 let NUM_REL_CONV =
1426   let gconv_net = itlist (uncurry net_of_conv)
1427     [`NUMERAL m < NUMERAL n`,NUM_LT_CONV;
1428      `NUMERAL m <= NUMERAL n`,NUM_LE_CONV;
1429      `NUMERAL m > NUMERAL n`,NUM_GT_CONV;
1430      `NUMERAL m >= NUMERAL n`,NUM_GE_CONV;
1431      `NUMERAL m = NUMERAL n`,NUM_EQ_CONV]
1432     (basic_net()) in
1433   REWRITES_CONV gconv_net;;
1434
1435 let NUM_RED_CONV =
1436   let gconv_net = itlist (uncurry net_of_conv)
1437     [`SUC(NUMERAL n)`,NUM_SUC_CONV;
1438      `PRE(NUMERAL n)`,NUM_PRE_CONV;
1439      `FACT(NUMERAL n)`,NUM_FACT_CONV;
1440      `NUMERAL m < NUMERAL n`,NUM_LT_CONV;
1441      `NUMERAL m <= NUMERAL n`,NUM_LE_CONV;
1442      `NUMERAL m > NUMERAL n`,NUM_GT_CONV;
1443      `NUMERAL m >= NUMERAL n`,NUM_GE_CONV;
1444      `NUMERAL m = NUMERAL n`,NUM_EQ_CONV;
1445      `EVEN(NUMERAL n)`,NUM_EVEN_CONV;
1446      `ODD(NUMERAL n)`,NUM_ODD_CONV;
1447      `NUMERAL m + NUMERAL n`,NUM_ADD_CONV;
1448      `NUMERAL m - NUMERAL n`,NUM_SUB_CONV;
1449      `NUMERAL m * NUMERAL n`,NUM_MULT_CONV;
1450      `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV;
1451      `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV;
1452      `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV;
1453      `MAX (NUMERAL m) (NUMERAL n)`,NUM_MAX_CONV;
1454      `MIN (NUMERAL m) (NUMERAL n)`,NUM_MIN_CONV]
1455     (basic_net()) in
1456   REWRITES_CONV gconv_net;;
1457
1458 let NUM_REDUCE_CONV = DEPTH_CONV NUM_RED_CONV;;
1459
1460 let NUM_REDUCE_TAC = CONV_TAC NUM_REDUCE_CONV;;
1461
1462 (* ------------------------------------------------------------------------- *)
1463 (* I do like this after all...                                               *)
1464 (* ------------------------------------------------------------------------- *)
1465
1466 let num_CONV =
1467   let SUC_tm = `SUC` in
1468   fun tm ->
1469     let n = dest_numeral tm -/ Int 1 in
1470     if n </ Int 0 then failwith "num_CONV" else
1471     let tm' = mk_numeral n in
1472     SYM(NUM_SUC_CONV (mk_comb(SUC_tm,tm')));;
1473
1474 (* ------------------------------------------------------------------------- *)
1475 (* Expands "!n. n < numeral-constant ==> P(n)" into all the cases.           *)
1476 (* ------------------------------------------------------------------------- *)
1477
1478 let EXPAND_CASES_CONV =
1479   let pth_base = prove
1480    (`(!n. n < 0 ==> P n) <=> T`,
1481     REWRITE_TAC[LT])
1482   and pth_step = prove
1483    (`(!n. n < SUC k ==> P n) <=> (!n. n < k ==> P n) /\ P k`,
1484     REWRITE_TAC[LT] THEN MESON_TAC[]) in
1485   let base_CONV = GEN_REWRITE_CONV I [pth_base]
1486   and step_CONV =
1487     BINDER_CONV(LAND_CONV(RAND_CONV num_CONV)) THENC
1488     GEN_REWRITE_CONV I [pth_step] in
1489   let rec conv tm =
1490     (base_CONV ORELSEC (step_CONV THENC LAND_CONV conv)) tm in
1491   conv THENC (REWRITE_CONV[GSYM CONJ_ASSOC]);;