int.ml

   1 (* ========================================================================= *)
   2 (* Theory of integers.                                                       *)
   3 (*                                                                           *)
   4 (* The integers are carved out of the real numbers; hence all the            *)
   5 (* universal theorems can be derived trivially from the real analog.         *)
   6 (*                                                                           *)
   7 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   8 (*                                                                           *)
   9 (*            (c) Copyright, University of Cambridge 1998                    *)
  10 (*              (c) Copyright, John Harrison 1998-2007                       *)
  11 (* ========================================================================= *)
  12
  13 needs "calc_rat.ml";;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Representing predicate. The "is_int" variant is useful for backwards      *)
  17 (* compatibility with former definition of "is_int" constant, now removed.   *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 let integer = new_definition
  21   `integer(x) <=> ?n. abs(x) = &n`;;
  22
  23 let is_int = prove
  24  (`integer(x) <=> ?n. x = &n \/ x = -- &n`,
  25   REWRITE_TAC[integer] THEN AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC);;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Type of integers.                                                         *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let int_tybij = new_type_definition "int" ("int_of_real","real_of_int")
  32  (prove(`?x. integer x`,
  33        EXISTS_TAC `&0` THEN
  34        REWRITE_TAC[is_int; REAL_OF_NUM_EQ; EXISTS_OR_THM; GSYM EXISTS_REFL]));;
  35
  36 let int_abstr,int_rep =
  37   SPEC_ALL(CONJUNCT1 int_tybij),SPEC_ALL(CONJUNCT2 int_tybij);;
  38
  39 let dest_int_rep = prove
  40  (`!i. ?n. (real_of_int i = &n) \/ (real_of_int i = --(&n))`,
  41   REWRITE_TAC[GSYM is_int; int_rep; int_abstr]);;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* We want the following too.                                                *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 let int_eq = prove
  48  (`!x y. (x = y) <=> (real_of_int x = real_of_int y)`,
  49   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  50   POP_ASSUM(MP_TAC o AP_TERM `int_of_real`) THEN
  51   REWRITE_TAC[int_abstr]);;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* Set up interface map.                                                     *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 do_list overload_interface
  58  ["+",`int_add:int->int->int`; "-",`int_sub:int->int->int`;
  59   "*",`int_mul:int->int->int`; "<",`int_lt:int->int->bool`;
  60   "<=",`int_le:int->int->bool`; ">",`int_gt:int->int->bool`;
  61   ">=",`int_ge:int->int->bool`; "--",`int_neg:int->int`;
  62   "pow",`int_pow:int->num->int`; "abs",`int_abs:int->int`;
  63   "max",`int_max:int->int->int`; "min",`int_min:int->int->int`;
  64   "&",`int_of_num:num->int`];;
  65
  66 let prioritize_int() = prioritize_overload(mk_type("int",[]));;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Definitions and closure derivations of all operations but "inv" and "/".  *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 let int_le = new_definition
  73   `x <= y <=> (real_of_int x) <= (real_of_int y)`;;
  74
  75 let int_lt = new_definition
  76   `x < y <=> (real_of_int x) < (real_of_int y)`;;
  77
  78 let int_ge = new_definition
  79   `x >= y <=> (real_of_int x) >= (real_of_int y)`;;
  80
  81 let int_gt = new_definition
  82   `x > y <=> (real_of_int x) > (real_of_int y)`;;
  83
  84 let int_of_num = new_definition
  85   `&n = int_of_real(real_of_num n)`;;
  86
  87 let int_of_num_th = prove
  88  (`!n. real_of_int(int_of_num n) = real_of_num n`,
  89   REWRITE_TAC[int_of_num; GSYM int_rep; is_int] THEN
  90   REWRITE_TAC[REAL_OF_NUM_EQ; EXISTS_OR_THM; GSYM EXISTS_REFL]);;
  91
  92 let int_neg = new_definition
  93  `--i = int_of_real(--(real_of_int i))`;;
  94
  95 let int_neg_th = prove
  96  (`!x. real_of_int(int_neg x) = --(real_of_int x)`,
  97   REWRITE_TAC[int_neg; GSYM int_rep; is_int] THEN
  98   GEN_TAC THEN STRIP_ASSUME_TAC(SPEC `x:int` dest_int_rep) THEN
  99   ASM_REWRITE_TAC[REAL_NEG_NEG; EXISTS_OR_THM; REAL_EQ_NEG2;
 100     REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
 101
 102 let int_add = new_definition
 103  `x + y = int_of_real((real_of_int x) + (real_of_int y))`;;
 104
 105 let int_add_th = prove
 106  (`!x y. real_of_int(x + y) = (real_of_int x) + (real_of_int y)`,
 107   REWRITE_TAC[int_add; GSYM int_rep; is_int] THEN REPEAT GEN_TAC THEN
 108   X_CHOOSE_THEN `m:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
 109   X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `y:int` dest_int_rep) THEN
 110   ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; EXISTS_OR_THM] THEN
 111   REWRITE_TAC[GSYM EXISTS_REFL] THEN
 112   DISJ_CASES_THEN MP_TAC (SPECL [`m:num`; `n:num`] LE_CASES) THEN
 113   REWRITE_TAC[LE_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 114   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; OR_EXISTS_THM; REAL_NEG_ADD] THEN
 115   TRY(EXISTS_TAC `d:num` THEN REAL_ARITH_TAC) THEN
 116   REWRITE_TAC[EXISTS_OR_THM; GSYM REAL_NEG_ADD; REAL_EQ_NEG2;
 117     REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
 118
 119 let int_sub = new_definition
 120   `x - y = int_of_real(real_of_int x - real_of_int y)`;;
 121
 122 let int_sub_th = prove
 123  (`!x y. real_of_int(x - y) = (real_of_int x) - (real_of_int y)`,
 124   REWRITE_TAC[int_sub; real_sub; GSYM int_neg_th; GSYM int_add_th] THEN
 125   REWRITE_TAC[int_abstr]);;
 126
 127 let int_mul = new_definition
 128   `x * y = int_of_real ((real_of_int x) * (real_of_int y))`;;
 129
 130 let int_mul_th = prove
 131  (`!x y. real_of_int(x * y) = (real_of_int x) * (real_of_int y)`,
 132   REPEAT GEN_TAC THEN REWRITE_TAC[int_mul; GSYM int_rep; is_int] THEN
 133   X_CHOOSE_THEN `m:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
 134   X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `y:int` dest_int_rep) THEN
 135   ASM_REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ; EXISTS_OR_THM] THEN
 136   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG; REAL_OF_NUM_MUL] THEN
 137   REWRITE_TAC[REAL_EQ_NEG2; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
 138
 139 let int_abs = new_definition
 140   `abs x = int_of_real(abs(real_of_int x))`;;
 141
 142 let int_abs_th = prove
 143  (`!x. real_of_int(abs x) = abs(real_of_int x)`,
 144   GEN_TAC THEN REWRITE_TAC[int_abs; real_abs] THEN COND_CASES_TAC THEN
 145   REWRITE_TAC[GSYM int_neg; int_neg_th; int_abstr]);;
 146
 147 let int_sgn = new_definition
 148   `int_sgn x = int_of_real(real_sgn(real_of_int x))`;;
 149
 150 let int_sgn_th = prove
 151  (`!x. real_of_int(int_sgn x) = real_sgn(real_of_int x)`,
 152   GEN_TAC THEN REWRITE_TAC[int_sgn; real_sgn; GSYM int_rep] THEN
 153   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 154   MESON_TAC[is_int]);;
 155
 156 let int_max = new_definition
 157   `int_max x y = int_of_real(max (real_of_int x) (real_of_int y))`;;
 158
 159 let int_max_th = prove
 160  (`!x y. real_of_int(max x y) = max (real_of_int x) (real_of_int y)`,
 161   REPEAT GEN_TAC THEN REWRITE_TAC[int_max; real_max] THEN
 162   COND_CASES_TAC THEN REWRITE_TAC[int_abstr]);;
 163
 164 let int_min = new_definition
 165   `int_min x y = int_of_real(min (real_of_int x) (real_of_int y))`;;
 166
 167 let int_min_th = prove
 168  (`!x y. real_of_int(min x y) = min (real_of_int x) (real_of_int y)`,
 169   REPEAT GEN_TAC THEN REWRITE_TAC[int_min; real_min] THEN
 170   COND_CASES_TAC THEN REWRITE_TAC[int_abstr]);;
 171
 172 let int_pow = new_definition
 173   `x pow n = int_of_real((real_of_int x) pow n)`;;
 174
 175 let int_pow_th = prove
 176  (`!x n. real_of_int(x pow n) = (real_of_int x) pow n`,
 177   GEN_TAC THEN REWRITE_TAC[int_pow] THEN INDUCT_TAC THEN
 178   REWRITE_TAC[real_pow] THENL
 179    [REWRITE_TAC[GSYM int_of_num; int_of_num_th];
 180     POP_ASSUM(SUBST1_TAC o SYM) THEN
 181     ASM_REWRITE_TAC[GSYM int_mul; int_mul_th]]);;
 182
 183 (* ------------------------------------------------------------------------- *)
 184 (* A couple of theorems peculiar to the integers.                            *)
 185 (* ------------------------------------------------------------------------- *)
 186
 187 let INT_IMAGE = prove
 188  (`!x. (?n. x = &n) \/ (?n. x = --(&n))`,
 189   GEN_TAC THEN
 190   X_CHOOSE_THEN `n:num` DISJ_CASES_TAC (SPEC `x:int` dest_int_rep) THEN
 191   POP_ASSUM(MP_TAC o AP_TERM `int_of_real`) THEN REWRITE_TAC[int_abstr] THEN
 192   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[int_of_num; int_neg] THENL
 193    [DISJ1_TAC; DISJ2_TAC] THEN
 194   EXISTS_TAC `n:num` THEN REWRITE_TAC[int_abstr] THEN
 195   REWRITE_TAC[GSYM int_of_num; int_of_num_th]);;
 196
 197 let INT_LT_DISCRETE = prove
 198  (`!x y. x < y <=> (x + &1) <= y`,
 199   REPEAT GEN_TAC THEN
 200   REWRITE_TAC[int_le; int_lt; int_add_th] THEN
 201   DISJ_CASES_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC )
 202    (SPEC `x:int` INT_IMAGE) THEN
 203   DISJ_CASES_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC )
 204    (SPEC `y:int` INT_IMAGE) THEN
 205   REWRITE_TAC[int_neg_th; int_of_num_th] THEN
 206   REWRITE_TAC[REAL_LE_NEG2; REAL_LT_NEG2] THEN
 207   REWRITE_TAC[REAL_LE_LNEG; REAL_LT_LNEG; REAL_LE_RNEG; REAL_LT_RNEG] THEN
 208   REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
 209   ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
 210   REWRITE_TAC[GSYM real_sub; REAL_LE_SUB_RADD] THEN
 211   REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_OF_NUM_ADD] THEN
 212   REWRITE_TAC[GSYM ADD1; ONCE_REWRITE_RULE[ADD_SYM] (GSYM ADD1)] THEN
 213   REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
 214   REWRITE_TAC[ADD_CLAUSES; LE_SUC_LT; LT_SUC_LE]);;
 215
 216 let INT_GT_DISCRETE = prove
 217  (`!x y. x > y <=> x >= (y + &1)`,
 218   REWRITE_TAC[int_gt; int_ge; real_ge; real_gt; GSYM int_le; GSYM int_lt] THEN
 219   MATCH_ACCEPT_TAC INT_LT_DISCRETE);;
 220
 221 (* ------------------------------------------------------------------------- *)
 222 (* Conversions of integer constants to and from OCaml numbers.               *)
 223 (* ------------------------------------------------------------------------- *)
 224
 225 let is_intconst tm =
 226   match tm with
 227     Comb(Const("int_of_num",_),n) -> is_numeral n
 228   | Comb(Const("int_neg",_),Comb(Const("int_of_num",_),n)) ->
 229       is_numeral n & not(dest_numeral n = num_0)
 230   | _ -> false;;
 231
 232 let dest_intconst tm =
 233   match tm with
 234     Comb(Const("int_of_num",_),n) -> dest_numeral n
 235   | Comb(Const("int_neg",_),Comb(Const("int_of_num",_),n)) ->
 236         let nn = dest_numeral n in
 237         if nn <>/ num_0 then minus_num(dest_numeral n)
 238         else failwith "dest_intconst"
 239   | _ -> failwith "dest_intconst";;
 240
 241 let mk_intconst =
 242   let cast_tm = `int_of_num` and neg_tm = `int_neg` in
 243   let mk_numconst n = mk_comb(cast_tm,mk_numeral n) in
 244   fun x -> if x </ num_0 then mk_comb(neg_tm,mk_numconst(minus_num x))
 245            else mk_numconst x;;
 246
 247 (* ------------------------------------------------------------------------- *)
 248 (* A simple procedure to lift most universal real theorems to integers.      *)
 249 (* For a more complete procedure, give required term to INT_ARITH (below).   *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let INT_OF_REAL_THM =
 253   let dest = `real_of_int`
 254   and real_ty = `:real`
 255   and int_ty = `:int`
 256   and cond_th = prove
 257    (`real_of_int(if b then x else y) =
 258        if b then real_of_int x else real_of_int y`,
 259     COND_CASES_TAC THEN REWRITE_TAC[]) in
 260   let thlist = map GSYM
 261    [int_eq; int_le; int_lt; int_ge; int_gt;
 262     int_of_num_th; int_neg_th; int_add_th; int_mul_th; int_sgn_th;
 263     int_sub_th; int_abs_th; int_max_th; int_min_th; int_pow_th; cond_th] in
 264   let REW_RULE = GEN_REWRITE_RULE DEPTH_CONV thlist in
 265   let int_tm_of_real_var v =
 266     let s,ty = dest_var v in
 267     if ty = real_ty then mk_comb(dest,mk_var(s,int_ty)) else v in
 268   let int_of_real_var v =
 269     let s,ty = dest_var v in
 270     if ty = real_ty then mk_var(s,int_ty) else v in
 271   let INT_OF_REAL_THM1 th =
 272     let newavs = subtract (frees (concl th)) (freesl (hyp th)) in
 273     let avs,bod = strip_forall(concl th) in
 274     let allavs = newavs@avs in
 275     let avs' = map int_tm_of_real_var allavs in
 276     let avs'' = map int_of_real_var avs in
 277     GENL avs'' (REW_RULE(SPECL avs' (GENL newavs th))) in
 278   let rec INT_OF_REAL_THM th =
 279     if is_conj(concl th) then CONJ (INT_OF_REAL_THM (CONJUNCT1 th))
 280                                    (INT_OF_REAL_THM (CONJUNCT2 th))
 281     else INT_OF_REAL_THM1 th in
 282   INT_OF_REAL_THM;;
 283
 284 (* ------------------------------------------------------------------------- *)
 285 (* Collect together all the theorems derived automatically.                  *)
 286 (* ------------------------------------------------------------------------- *)
 287
 288 let INT_ABS_0 = INT_OF_REAL_THM REAL_ABS_0;;
 289 let INT_ABS_1 = INT_OF_REAL_THM REAL_ABS_1;;
 290 let INT_ABS_ABS = INT_OF_REAL_THM REAL_ABS_ABS;;
 291 let INT_ABS_BETWEEN = INT_OF_REAL_THM REAL_ABS_BETWEEN;;
 292 let INT_ABS_BETWEEN1 = INT_OF_REAL_THM REAL_ABS_BETWEEN1;;
 293 let INT_ABS_BETWEEN2 = INT_OF_REAL_THM REAL_ABS_BETWEEN2;;
 294 let INT_ABS_BOUND = INT_OF_REAL_THM REAL_ABS_BOUND;;
 295 let INT_ABS_CASES = INT_OF_REAL_THM REAL_ABS_CASES;;
 296 let INT_ABS_CIRCLE = INT_OF_REAL_THM REAL_ABS_CIRCLE;;
 297 let INT_ABS_LE = INT_OF_REAL_THM REAL_ABS_LE;;
 298 let INT_ABS_MUL = INT_OF_REAL_THM REAL_ABS_MUL;;
 299 let INT_ABS_NEG = INT_OF_REAL_THM REAL_ABS_NEG;;
 300 let INT_ABS_NUM = INT_OF_REAL_THM REAL_ABS_NUM;;
 301 let INT_ABS_NZ = INT_OF_REAL_THM REAL_ABS_NZ;;
 302 let INT_ABS_POS = INT_OF_REAL_THM REAL_ABS_POS;;
 303 let INT_ABS_POW = INT_OF_REAL_THM REAL_ABS_POW;;
 304 let INT_ABS_REFL = INT_OF_REAL_THM REAL_ABS_REFL;;
 305 let INT_ABS_SGN = INT_OF_REAL_THM REAL_ABS_SGN;;
 306 let INT_ABS_SIGN = INT_OF_REAL_THM REAL_ABS_SIGN;;
 307 let INT_ABS_SIGN2 = INT_OF_REAL_THM REAL_ABS_SIGN2;;
 308 let INT_ABS_STILLNZ = INT_OF_REAL_THM REAL_ABS_STILLNZ;;
 309 let INT_ABS_SUB = INT_OF_REAL_THM REAL_ABS_SUB;;
 310 let INT_ABS_SUB_ABS = INT_OF_REAL_THM REAL_ABS_SUB_ABS;;
 311 let INT_ABS_TRIANGLE = INT_OF_REAL_THM REAL_ABS_TRIANGLE;;
 312 let INT_ABS_ZERO = INT_OF_REAL_THM REAL_ABS_ZERO;;
 313 let INT_ADD2_SUB2 = INT_OF_REAL_THM REAL_ADD2_SUB2;;
 314 let INT_ADD_AC = INT_OF_REAL_THM REAL_ADD_AC;;
 315 let INT_ADD_ASSOC = INT_OF_REAL_THM REAL_ADD_ASSOC;;
 316 let INT_ADD_LDISTRIB = INT_OF_REAL_THM REAL_ADD_LDISTRIB;;
 317 let INT_ADD_LID = INT_OF_REAL_THM REAL_ADD_LID;;
 318 let INT_ADD_LINV = INT_OF_REAL_THM REAL_ADD_LINV;;
 319 let INT_ADD_RDISTRIB = INT_OF_REAL_THM REAL_ADD_RDISTRIB;;
 320 let INT_ADD_RID = INT_OF_REAL_THM REAL_ADD_RID;;
 321 let INT_ADD_RINV = INT_OF_REAL_THM REAL_ADD_RINV;;
 322 let INT_ADD_SUB = INT_OF_REAL_THM REAL_ADD_SUB;;
 323 let INT_ADD_SUB2 = INT_OF_REAL_THM REAL_ADD_SUB2;;
 324 let INT_ADD_SYM = INT_OF_REAL_THM REAL_ADD_SYM;;
 325 let INT_BOUNDS_LE = INT_OF_REAL_THM REAL_BOUNDS_LE;;
 326 let INT_BOUNDS_LT = INT_OF_REAL_THM REAL_BOUNDS_LT;;
 327 let INT_DIFFSQ = INT_OF_REAL_THM REAL_DIFFSQ;;
 328 let INT_ENTIRE = INT_OF_REAL_THM REAL_ENTIRE;;
 329 let INT_EQ_ADD_LCANCEL = INT_OF_REAL_THM REAL_EQ_ADD_LCANCEL;;
 330 let INT_EQ_ADD_LCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_LCANCEL_0;;
 331 let INT_EQ_ADD_RCANCEL = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL;;
 332 let INT_EQ_ADD_RCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL_0;;
 333 let INT_EQ_IMP_LE = INT_OF_REAL_THM REAL_EQ_IMP_LE;;
 334 let INT_EQ_MUL_LCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_LCANCEL;;
 335 let INT_EQ_MUL_RCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_RCANCEL;;
 336 let INT_EQ_NEG2 = INT_OF_REAL_THM REAL_EQ_NEG2;;
 337 let INT_EQ_SGN_ABS = INT_OF_REAL_THM REAL_EQ_SGN_ABS;;
 338 let INT_EQ_SQUARE_ABS = INT_OF_REAL_THM REAL_EQ_SQUARE_ABS;;
 339 let INT_EQ_SUB_LADD = INT_OF_REAL_THM REAL_EQ_SUB_LADD;;
 340 let INT_EQ_SUB_RADD = INT_OF_REAL_THM REAL_EQ_SUB_RADD;;
 341 let INT_LET_ADD = INT_OF_REAL_THM REAL_LET_ADD;;
 342 let INT_LET_ADD2 = INT_OF_REAL_THM REAL_LET_ADD2;;
 343 let INT_LET_ANTISYM = INT_OF_REAL_THM REAL_LET_ANTISYM;;
 344 let INT_LET_TOTAL = INT_OF_REAL_THM REAL_LET_TOTAL;;
 345 let INT_LET_TRANS = INT_OF_REAL_THM REAL_LET_TRANS;;
 346 let INT_LE_01 = INT_OF_REAL_THM REAL_LE_01;;
 347 let INT_LE_ADD = INT_OF_REAL_THM REAL_LE_ADD;;
 348 let INT_LE_ADD2 = INT_OF_REAL_THM REAL_LE_ADD2;;
 349 let INT_LE_ADDL = INT_OF_REAL_THM REAL_LE_ADDL;;
 350 let INT_LE_ADDR = INT_OF_REAL_THM REAL_LE_ADDR;;
 351 let INT_LE_ANTISYM = INT_OF_REAL_THM REAL_LE_ANTISYM;;
 352 let INT_LE_DOUBLE = INT_OF_REAL_THM REAL_LE_DOUBLE;;
 353 let INT_LE_LADD = INT_OF_REAL_THM REAL_LE_LADD;;
 354 let INT_LE_LADD_IMP = INT_OF_REAL_THM REAL_LE_LADD_IMP;;
 355 let INT_LE_LMUL = INT_OF_REAL_THM REAL_LE_LMUL;;
 356 let INT_LE_LNEG = INT_OF_REAL_THM REAL_LE_LNEG;;
 357 let INT_LE_LT = INT_OF_REAL_THM REAL_LE_LT;;
 358 let INT_LE_MAX = INT_OF_REAL_THM REAL_LE_MAX;;
 359 let INT_LE_MIN = INT_OF_REAL_THM REAL_LE_MIN;;
 360 let INT_LE_MUL = INT_OF_REAL_THM REAL_LE_MUL;;
 361 let INT_LE_MUL_EQ = INT_OF_REAL_THM REAL_LE_MUL_EQ;;
 362 let INT_LE_NEG = INT_OF_REAL_THM REAL_LE_NEG;;
 363 let INT_LE_NEG2 = INT_OF_REAL_THM REAL_LE_NEG2;;
 364 let INT_LE_NEGL = INT_OF_REAL_THM REAL_LE_NEGL;;
 365 let INT_LE_NEGR = INT_OF_REAL_THM REAL_LE_NEGR;;
 366 let INT_LE_NEGTOTAL = INT_OF_REAL_THM REAL_LE_NEGTOTAL;;
 367 let INT_LE_POW2 = INT_OF_REAL_THM REAL_LE_POW2;;
 368 let INT_LE_RADD = INT_OF_REAL_THM REAL_LE_RADD;;
 369 let INT_LE_REFL = INT_OF_REAL_THM REAL_LE_REFL;;
 370 let INT_LE_RMUL = INT_OF_REAL_THM REAL_LE_RMUL;;
 371 let INT_LE_RNEG = INT_OF_REAL_THM REAL_LE_RNEG;;
 372 let INT_LE_SQUARE = INT_OF_REAL_THM REAL_LE_SQUARE;;
 373 let INT_LE_SQUARE_ABS = INT_OF_REAL_THM REAL_LE_SQUARE_ABS;;
 374 let INT_LE_SUB_LADD = INT_OF_REAL_THM REAL_LE_SUB_LADD;;
 375 let INT_LE_SUB_RADD = INT_OF_REAL_THM REAL_LE_SUB_RADD;;
 376 let INT_LE_TOTAL = INT_OF_REAL_THM REAL_LE_TOTAL;;
 377 let INT_LE_TRANS = INT_OF_REAL_THM REAL_LE_TRANS;;
 378 let INT_LNEG_UNIQ = INT_OF_REAL_THM REAL_LNEG_UNIQ;;
 379 let INT_LTE_ADD = INT_OF_REAL_THM REAL_LTE_ADD;;
 380 let INT_LTE_ADD2 = INT_OF_REAL_THM REAL_LTE_ADD2;;
 381 let INT_LTE_ANTISYM = INT_OF_REAL_THM REAL_LTE_ANTISYM;;
 382 let INT_LTE_TOTAL = INT_OF_REAL_THM REAL_LTE_TOTAL;;
 383 let INT_LTE_TRANS = INT_OF_REAL_THM REAL_LTE_TRANS;;
 384 let INT_LT_01 = INT_OF_REAL_THM REAL_LT_01;;
 385 let INT_LT_ADD = INT_OF_REAL_THM REAL_LT_ADD;;
 386 let INT_LT_ADD1 = INT_OF_REAL_THM REAL_LT_ADD1;;
 387 let INT_LT_ADD2 = INT_OF_REAL_THM REAL_LT_ADD2;;
 388 let INT_LT_ADDL = INT_OF_REAL_THM REAL_LT_ADDL;;
 389 let INT_LT_ADDNEG = INT_OF_REAL_THM REAL_LT_ADDNEG;;
 390 let INT_LT_ADDNEG2 = INT_OF_REAL_THM REAL_LT_ADDNEG2;;
 391 let INT_LT_ADDR = INT_OF_REAL_THM REAL_LT_ADDR;;
 392 let INT_LT_ADD_SUB = INT_OF_REAL_THM REAL_LT_ADD_SUB;;
 393 let INT_LT_ANTISYM = INT_OF_REAL_THM REAL_LT_ANTISYM;;
 394 let INT_LT_GT = INT_OF_REAL_THM REAL_LT_GT;;
 395 let INT_LT_IMP_LE = INT_OF_REAL_THM REAL_LT_IMP_LE;;
 396 let INT_LT_IMP_NE = INT_OF_REAL_THM REAL_LT_IMP_NE;;
 397 let INT_LT_LADD = INT_OF_REAL_THM REAL_LT_LADD;;
 398 let INT_LT_LE = INT_OF_REAL_THM REAL_LT_LE;;
 399 let INT_LT_LMUL_EQ = INT_OF_REAL_THM REAL_LT_LMUL_EQ;;
 400 let INT_LT_MAX = INT_OF_REAL_THM REAL_LT_MAX;;
 401 let INT_LT_MIN = INT_OF_REAL_THM REAL_LT_MIN;;
 402 let INT_LT_MUL = INT_OF_REAL_THM REAL_LT_MUL;;
 403 let INT_LT_MUL_EQ = INT_OF_REAL_THM REAL_LT_MUL_EQ;;
 404 let INT_LT_NEG = INT_OF_REAL_THM REAL_LT_NEG;;
 405 let INT_LT_NEG2 = INT_OF_REAL_THM REAL_LT_NEG2;;
 406 let INT_LT_NEGTOTAL = INT_OF_REAL_THM REAL_LT_NEGTOTAL;;
 407 let INT_LT_POW2 = INT_OF_REAL_THM REAL_LT_POW2;;
 408 let INT_LT_RADD = INT_OF_REAL_THM REAL_LT_RADD;;
 409 let INT_LT_REFL = INT_OF_REAL_THM REAL_LT_REFL;;
 410 let INT_LT_RMUL_EQ = INT_OF_REAL_THM REAL_LT_RMUL_EQ;;
 411 let INT_LT_SQUARE_ABS = INT_OF_REAL_THM REAL_LT_SQUARE_ABS;;
 412 let INT_LT_SUB_LADD = INT_OF_REAL_THM REAL_LT_SUB_LADD;;
 413 let INT_LT_SUB_RADD = INT_OF_REAL_THM REAL_LT_SUB_RADD;;
 414 let INT_LT_TOTAL = INT_OF_REAL_THM REAL_LT_TOTAL;;
 415 let INT_LT_TRANS = INT_OF_REAL_THM REAL_LT_TRANS;;
 416 let INT_MAX_ACI = INT_OF_REAL_THM REAL_MAX_ACI;;
 417 let INT_MAX_ASSOC = INT_OF_REAL_THM REAL_MAX_ASSOC;;
 418 let INT_MAX_LE = INT_OF_REAL_THM REAL_MAX_LE;;
 419 let INT_MAX_LT = INT_OF_REAL_THM REAL_MAX_LT;;
 420 let INT_MAX_MAX = INT_OF_REAL_THM REAL_MAX_MAX;;
 421 let INT_MAX_MIN = INT_OF_REAL_THM REAL_MAX_MIN;;
 422 let INT_MAX_SYM = INT_OF_REAL_THM REAL_MAX_SYM;;
 423 let INT_MIN_ACI = INT_OF_REAL_THM REAL_MIN_ACI;;
 424 let INT_MIN_ASSOC = INT_OF_REAL_THM REAL_MIN_ASSOC;;
 425 let INT_MIN_LE = INT_OF_REAL_THM REAL_MIN_LE;;
 426 let INT_MIN_LT = INT_OF_REAL_THM REAL_MIN_LT;;
 427 let INT_MIN_MAX = INT_OF_REAL_THM REAL_MIN_MAX;;
 428 let INT_MIN_MIN = INT_OF_REAL_THM REAL_MIN_MIN;;
 429 let INT_MIN_SYM = INT_OF_REAL_THM REAL_MIN_SYM;;
 430 let INT_MUL_AC = INT_OF_REAL_THM REAL_MUL_AC;;
 431 let INT_MUL_ASSOC = INT_OF_REAL_THM REAL_MUL_ASSOC;;
 432 let INT_MUL_LID = INT_OF_REAL_THM REAL_MUL_LID;;
 433 let INT_MUL_LNEG = INT_OF_REAL_THM REAL_MUL_LNEG;;
 434 let INT_MUL_LZERO = INT_OF_REAL_THM REAL_MUL_LZERO;;
 435 let INT_MUL_POS_LE = INT_OF_REAL_THM REAL_MUL_POS_LE;;
 436 let INT_MUL_POS_LT = INT_OF_REAL_THM REAL_MUL_POS_LT;;
 437 let INT_MUL_RID = INT_OF_REAL_THM REAL_MUL_RID;;
 438 let INT_MUL_RNEG = INT_OF_REAL_THM REAL_MUL_RNEG;;
 439 let INT_MUL_RZERO = INT_OF_REAL_THM REAL_MUL_RZERO;;
 440 let INT_MUL_SYM = INT_OF_REAL_THM REAL_MUL_SYM;;
 441 let INT_NEGNEG = INT_OF_REAL_THM REAL_NEGNEG;;
 442 let INT_NEG_0 = INT_OF_REAL_THM REAL_NEG_0;;
 443 let INT_NEG_ADD = INT_OF_REAL_THM REAL_NEG_ADD;;
 444 let INT_NEG_EQ = INT_OF_REAL_THM REAL_NEG_EQ;;
 445 let INT_NEG_EQ_0 = INT_OF_REAL_THM REAL_NEG_EQ_0;;
 446 let INT_NEG_GE0 = INT_OF_REAL_THM REAL_NEG_GE0;;
 447 let INT_NEG_GT0 = INT_OF_REAL_THM REAL_NEG_GT0;;
 448 let INT_NEG_LE0 = INT_OF_REAL_THM REAL_NEG_LE0;;
 449 let INT_NEG_LMUL = INT_OF_REAL_THM REAL_NEG_LMUL;;
 450 let INT_NEG_LT0 = INT_OF_REAL_THM REAL_NEG_LT0;;
 451 let INT_NEG_MINUS1 = INT_OF_REAL_THM REAL_NEG_MINUS1;;
 452 let INT_NEG_MUL2 = INT_OF_REAL_THM REAL_NEG_MUL2;;
 453 let INT_NEG_NEG = INT_OF_REAL_THM REAL_NEG_NEG;;
 454 let INT_NEG_RMUL = INT_OF_REAL_THM REAL_NEG_RMUL;;
 455 let INT_NEG_SUB = INT_OF_REAL_THM REAL_NEG_SUB;;
 456 let INT_NOT_EQ = INT_OF_REAL_THM REAL_NOT_EQ;;
 457 let INT_NOT_LE = INT_OF_REAL_THM REAL_NOT_LE;;
 458 let INT_NOT_LT = INT_OF_REAL_THM REAL_NOT_LT;;
 459 let INT_OF_NUM_ADD = INT_OF_REAL_THM REAL_OF_NUM_ADD;;
 460 let INT_OF_NUM_EQ = INT_OF_REAL_THM REAL_OF_NUM_EQ;;
 461 let INT_OF_NUM_GE = INT_OF_REAL_THM REAL_OF_NUM_GE;;
 462 let INT_OF_NUM_GT = INT_OF_REAL_THM REAL_OF_NUM_GT;;
 463 let INT_OF_NUM_LE = INT_OF_REAL_THM REAL_OF_NUM_LE;;
 464 let INT_OF_NUM_LT = INT_OF_REAL_THM REAL_OF_NUM_LT;;
 465 let INT_OF_NUM_MAX = INT_OF_REAL_THM REAL_OF_NUM_MAX;;
 466 let INT_OF_NUM_MIN = INT_OF_REAL_THM REAL_OF_NUM_MIN;;
 467 let INT_OF_NUM_MUL = INT_OF_REAL_THM REAL_OF_NUM_MUL;;
 468 let INT_OF_NUM_POW = INT_OF_REAL_THM REAL_OF_NUM_POW;;
 469 let INT_OF_NUM_SUB = INT_OF_REAL_THM REAL_OF_NUM_SUB;;
 470 let INT_OF_NUM_SUC = INT_OF_REAL_THM REAL_OF_NUM_SUC;;
 471 let INT_POS = INT_OF_REAL_THM REAL_POS;;
 472 let INT_POS_NZ = INT_OF_REAL_THM REAL_POS_NZ;;
 473 let INT_POW2_ABS = INT_OF_REAL_THM REAL_POW2_ABS;;
 474 let INT_POW_1 = INT_OF_REAL_THM REAL_POW_1;;
 475 let INT_POW_1_LE = INT_OF_REAL_THM REAL_POW_1_LE;;
 476 let INT_POW_1_LT = INT_OF_REAL_THM REAL_POW_1_LT;;
 477 let INT_POW_2 = INT_OF_REAL_THM REAL_POW_2;;
 478 let INT_POW_ADD = INT_OF_REAL_THM REAL_POW_ADD;;
 479 let INT_POW_EQ = INT_OF_REAL_THM REAL_POW_EQ;;
 480 let INT_POW_EQ_0 = INT_OF_REAL_THM REAL_POW_EQ_0;;
 481 let INT_POW_EQ_ABS = INT_OF_REAL_THM REAL_POW_EQ_ABS;;
 482 let INT_POW_LE = INT_OF_REAL_THM REAL_POW_LE;;
 483 let INT_POW_LE2 = INT_OF_REAL_THM REAL_POW_LE2;;
 484 let INT_POW_LE2_ODD = INT_OF_REAL_THM REAL_POW_LE2_ODD;;
 485 let INT_POW_LE2_REV = INT_OF_REAL_THM REAL_POW_LE2_REV;;
 486 let INT_POW_LE_1 = INT_OF_REAL_THM REAL_POW_LE_1;;
 487 let INT_POW_LT = INT_OF_REAL_THM REAL_POW_LT;;
 488 let INT_POW_LT2 = INT_OF_REAL_THM REAL_POW_LT2;;
 489 let INT_POW_LT2_REV = INT_OF_REAL_THM REAL_POW_LT2_REV;;
 490 let INT_POW_LT_1 = INT_OF_REAL_THM REAL_POW_LT_1;;
 491 let INT_POW_MONO = INT_OF_REAL_THM REAL_POW_MONO;;
 492 let INT_POW_MONO_LT = INT_OF_REAL_THM REAL_POW_MONO_LT;;
 493 let INT_POW_MUL = INT_OF_REAL_THM REAL_POW_MUL;;
 494 let INT_POW_NEG = INT_OF_REAL_THM REAL_POW_NEG;;
 495 let INT_POW_NZ = INT_OF_REAL_THM REAL_POW_NZ;;
 496 let INT_POW_ONE = INT_OF_REAL_THM REAL_POW_ONE;;
 497 let INT_POW_POW = INT_OF_REAL_THM REAL_POW_POW;;
 498 let INT_POW_ZERO = INT_OF_REAL_THM REAL_POW_ZERO;;
 499 let INT_RNEG_UNIQ = INT_OF_REAL_THM REAL_RNEG_UNIQ;;
 500 let INT_SGN = INT_OF_REAL_THM real_sgn;;
 501 let INT_SGN_0 = INT_OF_REAL_THM REAL_SGN_0;;
 502 let INT_SGN_ABS = INT_OF_REAL_THM REAL_SGN_ABS;;
 503 let INT_SGN_CASES = INT_OF_REAL_THM REAL_SGN_CASES;;
 504 let INT_SGN_EQ = INT_OF_REAL_THM REAL_SGN_EQ;;
 505 let INT_SGN_INEQS = INT_OF_REAL_THM REAL_SGN_INEQS;;
 506 let INT_SGN_MUL = INT_OF_REAL_THM REAL_SGN_MUL;;
 507 let INT_SGN_NEG = INT_OF_REAL_THM REAL_SGN_NEG;;
 508 let INT_SGN_POW = INT_OF_REAL_THM REAL_SGN_POW;;
 509 let INT_SGN_POW_2 = INT_OF_REAL_THM REAL_SGN_POW_2;;
 510 let INT_SGN_INT_SGN = INT_OF_REAL_THM REAL_SGN_REAL_SGN;;
 511 let INT_SOS_EQ_0 = INT_OF_REAL_THM REAL_SOS_EQ_0;;
 512 let INT_SUB_0 = INT_OF_REAL_THM REAL_SUB_0;;
 513 let INT_SUB_ABS = INT_OF_REAL_THM REAL_SUB_ABS;;
 514 let INT_SUB_ADD = INT_OF_REAL_THM REAL_SUB_ADD;;
 515 let INT_SUB_ADD2 = INT_OF_REAL_THM REAL_SUB_ADD2;;
 516 let INT_SUB_LDISTRIB = INT_OF_REAL_THM REAL_SUB_LDISTRIB;;
 517 let INT_SUB_LE = INT_OF_REAL_THM REAL_SUB_LE;;
 518 let INT_SUB_LNEG = INT_OF_REAL_THM REAL_SUB_LNEG;;
 519 let INT_SUB_LT = INT_OF_REAL_THM REAL_SUB_LT;;
 520 let INT_SUB_LZERO = INT_OF_REAL_THM REAL_SUB_LZERO;;
 521 let INT_SUB_NEG2 = INT_OF_REAL_THM REAL_SUB_NEG2;;
 522 let INT_SUB_RDISTRIB = INT_OF_REAL_THM REAL_SUB_RDISTRIB;;
 523 let INT_SUB_REFL = INT_OF_REAL_THM REAL_SUB_REFL;;
 524 let INT_SUB_RNEG = INT_OF_REAL_THM REAL_SUB_RNEG;;
 525 let INT_SUB_RZERO = INT_OF_REAL_THM REAL_SUB_RZERO;;
 526 let INT_SUB_SUB = INT_OF_REAL_THM REAL_SUB_SUB;;
 527 let INT_SUB_SUB2 = INT_OF_REAL_THM REAL_SUB_SUB2;;
 528 let INT_SUB_TRIANGLE = INT_OF_REAL_THM REAL_SUB_TRIANGLE;;
 529
 530 (* ------------------------------------------------------------------------- *)
 531 (* More useful "image" theorems.                                             *)
 532 (* ------------------------------------------------------------------------- *)
 533
 534 let INT_FORALL_POS = prove
 535  (`!P. (!n. P(&n)) <=> (!i:int. &0 <= i ==> P(i))`,
 536   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THENL
 537    [DISJ_CASES_THEN (CHOOSE_THEN SUBST1_TAC) (SPEC `i:int` INT_IMAGE) THEN
 538     ASM_REWRITE_TAC[INT_LE_RNEG; INT_ADD_LID; INT_OF_NUM_LE; LE] THEN
 539     DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[INT_NEG_0];
 540     FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INT_OF_NUM_LE; LE_0]]);;
 541
 542 let INT_EXISTS_POS = prove
 543  (`!P. (?n. P(&n)) <=> (?i:int. &0 <= i /\ P(i))`,
 544   GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN
 545   REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_POS] THEN MESON_TAC[]);;
 546
 547 let INT_FORALL_ABS = prove
 548  (`!P. (!n. P(&n)) <=> (!x:int. P(abs x))`,
 549   REWRITE_TAC[INT_FORALL_POS] THEN MESON_TAC[INT_ABS_POS; INT_ABS_REFL]);;
 550
 551 let INT_EXISTS_ABS = prove
 552  (`!P. (?n. P(&n)) <=> (?x:int. P(abs x))`,
 553   GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `(p <=> q) <=> (~p <=> ~q)`] THEN
 554   REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_ABS] THEN MESON_TAC[]);;
 555
 556 (* ------------------------------------------------------------------------- *)
 557 (* Sometimes handy in number-theoretic applications.                         *)
 558 (* ------------------------------------------------------------------------- *)
 559
 560 let INT_ABS_MUL_1 = prove
 561  (`!x y. (abs(x * y) = &1) <=> (abs(x) = &1) /\ (abs(y) = &1)`,
 562   REPEAT GEN_TAC THEN REWRITE_TAC[INT_ABS_MUL] THEN
 563   MP_TAC(SPEC `y:int` INT_ABS_POS) THEN SPEC_TAC(`abs(y)`,`b:int`) THEN
 564   MP_TAC(SPEC `x:int` INT_ABS_POS) THEN SPEC_TAC(`abs(x)`,`a:int`) THEN
 565   REWRITE_TAC[GSYM INT_FORALL_POS; INT_OF_NUM_MUL; INT_OF_NUM_EQ; MULT_EQ_1]);;
 566
 567 let INT_WOP = prove
 568  (`(?x. &0 <= x /\ P x) <=>
 569    (?x. &0 <= x /\ P x /\ !y. &0 <= y /\ P y ==> x <= y)`,
 570   ONCE_REWRITE_TAC[MESON[] `(?x. P x /\ Q x) <=> ~(!x. P x ==> ~Q x)`] THEN
 571   REWRITE_TAC[IMP_CONJ; GSYM INT_FORALL_POS; INT_OF_NUM_LE] THEN
 572   REWRITE_TAC[NOT_FORALL_THM] THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
 573   REWRITE_TAC[GSYM NOT_LE; CONTRAPOS_THM]);;
 574
 575 (* ------------------------------------------------------------------------- *)
 576 (* A few "pseudo definitions".                                               *)
 577 (* ------------------------------------------------------------------------- *)
 578
 579 let INT_POW = prove
 580  (`(x pow 0 = &1) /\
 581    (!n. x pow (SUC n) = x * x pow n)`,
 582   REWRITE_TAC(map INT_OF_REAL_THM (CONJUNCTS real_pow)));;
 583
 584 let INT_ABS = prove
 585  (`!x. abs(x) = if &0 <= x then x else --x`,
 586   GEN_TAC THEN MP_TAC(INT_OF_REAL_THM(SPEC `x:real` real_abs)) THEN
 587   COND_CASES_TAC THEN REWRITE_TAC[int_eq]);;
 588
 589 let INT_GE = prove
 590  (`!x y. x >= y <=> y <= x`,
 591   REWRITE_TAC[int_ge; int_le; real_ge]);;
 592
 593 let INT_GT = prove
 594  (`!x y. x > y <=> y < x`,
 595   REWRITE_TAC[int_gt; int_lt; real_gt]);;
 596
 597 let INT_LT = prove
 598  (`!x y. x < y <=> ~(y <= x)`,
 599   REWRITE_TAC[int_lt; int_le; real_lt]);;
 600
 601 (* ------------------------------------------------------------------------- *)
 602 (* Now a decision procedure for the integers.                                *)
 603 (* ------------------------------------------------------------------------- *)
 604
 605 let INT_ARITH =
 606   let atom_CONV =
 607     let pth = prove
 608       (`(~(x <= y) <=> y + &1 <= x) /\
 609         (~(x < y) <=> y <= x) /\
 610         (~(x = y) <=> x + &1 <= y \/ y + &1 <= x) /\
 611         (x < y <=> x + &1 <= y)`,
 612        REWRITE_TAC[INT_NOT_LE; INT_NOT_LT; INT_NOT_EQ; INT_LT_DISCRETE]) in
 613     GEN_REWRITE_CONV I [pth]
 614   and bub_CONV = GEN_REWRITE_CONV TOP_SWEEP_CONV
 615    [int_eq; int_le; int_lt; int_ge; int_gt;
 616     int_of_num_th; int_neg_th; int_add_th; int_mul_th;
 617     int_sub_th; int_pow_th; int_abs_th; int_max_th; int_min_th] in
 618   let base_CONV = TRY_CONV atom_CONV THENC bub_CONV in
 619   let NNF_NORM_CONV = GEN_NNF_CONV false
 620    (base_CONV,fun t -> base_CONV t,base_CONV(mk_neg t)) in
 621   let init_CONV =
 622     TOP_DEPTH_CONV BETA_CONV THENC
 623     PRESIMP_CONV THENC
 624     GEN_REWRITE_CONV DEPTH_CONV [INT_GT; INT_GE] THENC
 625     NNF_CONV THENC DEPTH_BINOP_CONV `(\/)` CONDS_ELIM_CONV THENC
 626     NNF_NORM_CONV in
 627   let p_tm = `p:bool`
 628   and not_tm = `(~)` in
 629   let pth = TAUT(mk_eq(mk_neg(mk_neg p_tm),p_tm)) in
 630   fun tm ->
 631     let th0 = INST [tm,p_tm] pth
 632     and th1 = init_CONV (mk_neg tm) in
 633     let th2 = REAL_ARITH(mk_neg(rand(concl th1))) in
 634     EQ_MP th0 (EQ_MP (AP_TERM not_tm (SYM th1)) th2);;
 635
 636 let INT_ARITH_TAC = CONV_TAC(EQT_INTRO o INT_ARITH);;
 637
 638 let ASM_INT_ARITH_TAC =
 639   REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
 640   INT_ARITH_TAC;;
 641
 642 (* ------------------------------------------------------------------------- *)
 643 (* Some pseudo-definitions.                                                  *)
 644 (* ------------------------------------------------------------------------- *)
 645
 646 let INT_SUB = INT_ARITH `!x y. x - y = x + --y`;;
 647
 648 let INT_MAX = INT_ARITH `!x y. max x y = if x <= y then y else x`;;
 649
 650 let INT_MIN = INT_ARITH `!x y. min x y = if x <= y then x else y`;;
 651
 652 (* ------------------------------------------------------------------------- *)
 653 (* Additional useful lemmas.                                                 *)
 654 (* ------------------------------------------------------------------------- *)
 655
 656 let INT_OF_NUM_EXISTS = prove
 657  (`!x:int. (?n. x = &n) <=> &0 <= x`,
 658   GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[INT_POS] THEN
 659   MP_TAC(ISPEC `x:int` INT_IMAGE) THEN
 660   REWRITE_TAC[OR_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
 661   ASM_INT_ARITH_TAC);;
 662
 663 let INT_LE_DISCRETE = INT_ARITH `!x y:int. x <= y <=> x < y + &1`;;
 664
 665 (* ------------------------------------------------------------------------- *)
 666 (* Archimedian property for the integers.                                    *)
 667 (* ------------------------------------------------------------------------- *)
 668
 669 let INT_ARCH = prove
 670  (`!x d. ~(d = &0) ==> ?c. x < c * d`,
 671   SUBGOAL_THEN `!x. &0 <= x ==> ?n. x <= &n` ASSUME_TAC THENL
 672    [REWRITE_TAC[GSYM INT_FORALL_POS; INT_OF_NUM_LE] THEN MESON_TAC[LE_REFL];
 673     ALL_TAC] THEN
 674   SUBGOAL_THEN `!x. ?n. x <= &n` ASSUME_TAC THENL
 675    [ASM_MESON_TAC[INT_LE_TOTAL]; ALL_TAC] THEN
 676   SUBGOAL_THEN `!x d. &0 < d ==> ?c. x < c * d` ASSUME_TAC THENL
 677    [REPEAT GEN_TAC THEN REWRITE_TAC[INT_LT_DISCRETE; INT_ADD_LID] THEN
 678     ASM_MESON_TAC[INT_POS; INT_LE_LMUL; INT_ARITH
 679         `x + &1 <= &n /\ &n * &1 <= &n * d ==> x + &1 <= &n * d`];
 680     ALL_TAC] THEN
 681   SUBGOAL_THEN `!x d. ~(d = &0) ==> ?c. x < c * d` ASSUME_TAC THENL
 682    [ASM_MESON_TAC[INT_ARITH `--x * y = x * --y`;
 683                   INT_ARITH `~(d = &0) ==> &0 < d \/ &0 < --d`];
 684     ALL_TAC] THEN
 685   ASM_MESON_TAC[INT_ARITH `--x * y = x * --y`;
 686                 INT_ARITH `~(d = &0) ==> &0 < d \/ &0 < --d`]);;
 687
 688 (* ------------------------------------------------------------------------- *)
 689 (* Definitions of ("Euclidean") integer division and remainder.              *)
 690 (* ------------------------------------------------------------------------- *)
 691
 692 let INT_DIVMOD_EXIST_0 = prove
 693  (`!m n:int. ?q r. if n = &0 then q = &0 /\ r = m
 694                    else &0 <= r /\ r < abs(n) /\ m = q * n + r`,
 695   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = &0` THEN
 696   ASM_REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
 697   GEN_REWRITE_TAC I [SWAP_EXISTS_THM] THEN
 698   SUBGOAL_THEN `?r. &0 <= r /\ ?q:int. m = n * q + r` MP_TAC THENL
 699    [FIRST_ASSUM(MP_TAC o SPEC `--m:int` o MATCH_MP INT_ARCH) THEN
 700     DISCH_THEN(X_CHOOSE_TAC `s:int`) THEN
 701     EXISTS_TAC `m + s * n:int` THEN CONJ_TAC THENL
 702      [ASM_INT_ARITH_TAC; EXISTS_TAC `--s:int` THEN INT_ARITH_TAC];
 703     GEN_REWRITE_TAC LAND_CONV [INT_WOP] THEN
 704     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:int` THEN
 705     REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
 706     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `q:int` THEN STRIP_TAC THEN
 707     ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC `r - abs n`) THEN
 708     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 709     DISCH_THEN(MP_TAC o SPEC `if &0 <= n then q + &1 else q - &1`) THEN
 710     ASM_INT_ARITH_TAC]);;
 711
 712 parse_as_infix("div",(22,"left"));;
 713 parse_as_infix("rem",(22,"left"));;
 714
 715 let INT_DIVISION_0 =  new_specification ["div"; "rem"]
 716   (REWRITE_RULE[SKOLEM_THM] INT_DIVMOD_EXIST_0);;
 717
 718 let INT_DIVISION = prove
 719  (`!m n. ~(n = &0)
 720          ==> m = m div n * n + m rem n /\ &0 <= m rem n /\ m rem n < abs n`,
 721   MESON_TAC[INT_DIVISION_0]);;
 722
 723 (* ------------------------------------------------------------------------- *)
 724 (* Arithmetic operations on integers. Essentially a clone of stuff for reals *)
 725 (* in the file "calc_int.ml", except for div and rem, which are more like N. *)
 726 (* ------------------------------------------------------------------------- *)
 727
 728 let INT_LE_CONV,INT_LT_CONV,INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV =
 729   let tth =
 730     TAUT `(F /\ F <=> F) /\ (F /\ T <=> F) /\
 731           (T /\ F <=> F) /\ (T /\ T <=> T)` in
 732   let nth = TAUT `(~T <=> F) /\ (~F <=> T)` in
 733   let NUM2_EQ_CONV = BINOP_CONV NUM_EQ_CONV THENC GEN_REWRITE_CONV I [tth] in
 734   let NUM2_NE_CONV =
 735     RAND_CONV NUM2_EQ_CONV THENC
 736     GEN_REWRITE_CONV I [nth] in
 737   let [pth_le1; pth_le2a; pth_le2b; pth_le3] = (CONJUNCTS o prove)
 738    (`(--(&m) <= &n <=> T) /\
 739      (&m <= &n <=> m <= n) /\
 740      (--(&m) <= --(&n) <=> n <= m) /\
 741      (&m <= --(&n) <=> (m = 0) /\ (n = 0))`,
 742     REWRITE_TAC[INT_LE_NEG2] THEN
 743     REWRITE_TAC[INT_LE_LNEG; INT_LE_RNEG] THEN
 744     REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_LE; LE_0] THEN
 745     REWRITE_TAC[LE; ADD_EQ_0]) in
 746   let INT_LE_CONV = FIRST_CONV
 747    [GEN_REWRITE_CONV I [pth_le1];
 748     GEN_REWRITE_CONV I [pth_le2a; pth_le2b] THENC NUM_LE_CONV;
 749     GEN_REWRITE_CONV I [pth_le3] THENC NUM2_EQ_CONV] in
 750   let [pth_lt1; pth_lt2a; pth_lt2b; pth_lt3] = (CONJUNCTS o prove)
 751    (`(&m < --(&n) <=> F) /\
 752      (&m < &n <=> m < n) /\
 753      (--(&m) < --(&n) <=> n < m) /\
 754      (--(&m) < &n <=> ~((m = 0) /\ (n = 0)))`,
 755     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3;
 756                 GSYM NOT_LE; INT_LT] THEN
 757     CONV_TAC TAUT) in
 758   let INT_LT_CONV = FIRST_CONV
 759    [GEN_REWRITE_CONV I [pth_lt1];
 760     GEN_REWRITE_CONV I [pth_lt2a; pth_lt2b] THENC NUM_LT_CONV;
 761     GEN_REWRITE_CONV I [pth_lt3] THENC NUM2_NE_CONV] in
 762   let [pth_ge1; pth_ge2a; pth_ge2b; pth_ge3] = (CONJUNCTS o prove)
 763    (`(&m >= --(&n) <=> T) /\
 764      (&m >= &n <=> n <= m) /\
 765      (--(&m) >= --(&n) <=> m <= n) /\
 766      (--(&m) >= &n <=> (m = 0) /\ (n = 0))`,
 767     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; INT_GE] THEN
 768     CONV_TAC TAUT) in
 769   let INT_GE_CONV = FIRST_CONV
 770    [GEN_REWRITE_CONV I [pth_ge1];
 771     GEN_REWRITE_CONV I [pth_ge2a; pth_ge2b] THENC NUM_LE_CONV;
 772     GEN_REWRITE_CONV I [pth_ge3] THENC NUM2_EQ_CONV] in
 773   let [pth_gt1; pth_gt2a; pth_gt2b; pth_gt3] = (CONJUNCTS o prove)
 774    (`(--(&m) > &n <=> F) /\
 775      (&m > &n <=> n < m) /\
 776      (--(&m) > --(&n) <=> m < n) /\
 777      (&m > --(&n) <=> ~((m = 0) /\ (n = 0)))`,
 778     REWRITE_TAC[pth_lt1; pth_lt2a; pth_lt2b; pth_lt3; INT_GT] THEN
 779     CONV_TAC TAUT) in
 780   let INT_GT_CONV = FIRST_CONV
 781    [GEN_REWRITE_CONV I [pth_gt1];
 782     GEN_REWRITE_CONV I [pth_gt2a; pth_gt2b] THENC NUM_LT_CONV;
 783     GEN_REWRITE_CONV I [pth_gt3] THENC NUM2_NE_CONV] in
 784   let [pth_eq1a; pth_eq1b; pth_eq2a; pth_eq2b] = (CONJUNCTS o prove)
 785    (`((&m = &n) <=> (m = n)) /\
 786      ((--(&m) = --(&n)) <=> (m = n)) /\
 787      ((--(&m) = &n) <=> (m = 0) /\ (n = 0)) /\
 788      ((&m = --(&n)) <=> (m = 0) /\ (n = 0))`,
 789     REWRITE_TAC[GSYM INT_LE_ANTISYM; GSYM LE_ANTISYM] THEN
 790     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; LE; LE_0] THEN
 791     CONV_TAC TAUT) in
 792   let INT_EQ_CONV = FIRST_CONV
 793    [GEN_REWRITE_CONV I [pth_eq1a; pth_eq1b] THENC NUM_EQ_CONV;
 794     GEN_REWRITE_CONV I [pth_eq2a; pth_eq2b] THENC NUM2_EQ_CONV] in
 795   INT_LE_CONV,INT_LT_CONV,
 796   INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV;;
 797
 798 let INT_NEG_CONV =
 799   let pth = prove
 800    (`(--(&0) = &0) /\
 801      (--(--(&x)) = &x)`,
 802     REWRITE_TAC[INT_NEG_NEG; INT_NEG_0]) in
 803   GEN_REWRITE_CONV I [pth];;
 804
 805 let INT_MUL_CONV =
 806   let pth0 = prove
 807    (`(&0 * &x = &0) /\
 808      (&0 * --(&x) = &0) /\
 809      (&x * &0 = &0) /\
 810      (--(&x) * &0 = &0)`,
 811     REWRITE_TAC[INT_MUL_LZERO; INT_MUL_RZERO])
 812   and pth1,pth2 = (CONJ_PAIR o prove)
 813    (`((&m * &n = &(m * n)) /\
 814       (--(&m) * --(&n) = &(m * n))) /\
 815      ((--(&m) * &n = --(&(m * n))) /\
 816       (&m * --(&n) = --(&(m * n))))`,
 817     REWRITE_TAC[INT_MUL_LNEG; INT_MUL_RNEG; INT_NEG_NEG] THEN
 818     REWRITE_TAC[INT_OF_NUM_MUL]) in
 819   FIRST_CONV
 820    [GEN_REWRITE_CONV I [pth0];
 821     GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_MULT_CONV;
 822     GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)];;
 823
 824 let INT_ADD_CONV =
 825   let neg_tm = `(--)` in
 826   let amp_tm = `&` in
 827   let add_tm = `(+)` in
 828   let dest = dest_binop `(+)` in
 829   let m_tm = `m:num` and n_tm = `n:num` in
 830   let pth0 = prove
 831    (`(--(&m) + &m = &0) /\
 832      (&m + --(&m) = &0)`,
 833     REWRITE_TAC[INT_ADD_LINV; INT_ADD_RINV]) in
 834   let [pth1; pth2; pth3; pth4; pth5; pth6] = (CONJUNCTS o prove)
 835    (`(--(&m) + --(&n) = --(&(m + n))) /\
 836      (--(&m) + &(m + n) = &n) /\
 837      (--(&(m + n)) + &m = --(&n)) /\
 838      (&(m + n) + --(&m) = &n) /\
 839      (&m + --(&(m + n)) = --(&n)) /\
 840      (&m + &n = &(m + n))`,
 841     REWRITE_TAC[GSYM INT_OF_NUM_ADD; INT_NEG_ADD] THEN
 842     REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
 843     REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID] THEN
 844     ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
 845     REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
 846     REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID]) in
 847   GEN_REWRITE_CONV I [pth0] ORELSEC
 848   (fun tm ->
 849     try let l,r = dest tm in
 850         if rator l = neg_tm then
 851           if rator r = neg_tm then
 852             let th1 = INST [rand(rand l),m_tm; rand(rand r),n_tm] pth1 in
 853             let tm1 = rand(rand(rand(concl th1))) in
 854             let th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) in
 855             TRANS th1 th2
 856           else
 857             let m = rand(rand l) and n = rand r in
 858             let m' = dest_numeral m and n' = dest_numeral n in
 859             if m' <=/ n' then
 860               let p = mk_numeral (n' -/ m') in
 861               let th1 = INST [m,m_tm; p,n_tm] pth2 in
 862               let th2 = NUM_ADD_CONV (rand(rand(lhand(concl th1)))) in
 863               let th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) in
 864               TRANS th3 th1
 865             else
 866               let p = mk_numeral (m' -/ n') in
 867               let th1 = INST [n,m_tm; p,n_tm] pth3 in
 868               let th2 = NUM_ADD_CONV (rand(rand(lhand(lhand(concl th1))))) in
 869               let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 870               let th4 = AP_THM (AP_TERM add_tm th3) (rand tm) in
 871               TRANS th4 th1
 872         else
 873           if rator r = neg_tm then
 874             let m = rand l and n = rand(rand r) in
 875             let m' = dest_numeral m and n' = dest_numeral n in
 876             if n' <=/ m' then
 877               let p = mk_numeral (m' -/ n') in
 878               let th1 = INST [n,m_tm; p,n_tm] pth4 in
 879               let th2 = NUM_ADD_CONV (rand(lhand(lhand(concl th1)))) in
 880               let th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) in
 881               let th4 = AP_THM th3 (rand tm) in
 882               TRANS th4 th1
 883             else
 884              let p = mk_numeral (n' -/ m') in
 885              let th1 = INST [m,m_tm; p,n_tm] pth5 in
 886              let th2 = NUM_ADD_CONV (rand(rand(rand(lhand(concl th1))))) in
 887              let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 888              let th4 = AP_TERM (rator tm) th3 in
 889              TRANS th4 th1
 890           else
 891             let th1 = INST [rand l,m_tm; rand r,n_tm] pth6 in
 892             let tm1 = rand(rand(concl th1)) in
 893             let th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) in
 894             TRANS th1 th2
 895     with Failure _ -> failwith "INT_ADD_CONV");;
 896
 897 let INT_SUB_CONV =
 898   GEN_REWRITE_CONV I [INT_SUB] THENC
 899   TRY_CONV(RAND_CONV INT_NEG_CONV) THENC
 900   INT_ADD_CONV;;
 901
 902 let INT_POW_CONV =
 903   let pth1,pth2 = (CONJ_PAIR o prove)
 904    (`(&x pow n = &(x EXP n)) /\
 905      ((--(&x)) pow n = if EVEN n then &(x EXP n) else --(&(x EXP n)))`,
 906     REWRITE_TAC[INT_OF_NUM_POW; INT_POW_NEG]) in
 907   let tth = prove
 908    (`((if T then x:int else y) = x) /\ ((if F then x:int else y) = y)`,
 909     REWRITE_TAC[]) in
 910   let neg_tm = `(--)` in
 911   (GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_EXP_CONV) ORELSEC
 912   (GEN_REWRITE_CONV I [pth2] THENC
 913    RATOR_CONV(RATOR_CONV(RAND_CONV NUM_EVEN_CONV)) THENC
 914    GEN_REWRITE_CONV I [tth] THENC
 915    (fun tm -> if rator tm = neg_tm then RAND_CONV(RAND_CONV NUM_EXP_CONV) tm
 916               else RAND_CONV NUM_EXP_CONV  tm));;
 917
 918 let INT_ABS_CONV =
 919   let pth = prove
 920    (`(abs(--(&x)) = &x) /\
 921      (abs(&x) = &x)`,
 922     REWRITE_TAC[INT_ABS_NEG; INT_ABS_NUM]) in
 923   GEN_REWRITE_CONV I [pth];;
 924
 925 let INT_MAX_CONV =
 926   REWR_CONV INT_MAX THENC
 927   RATOR_CONV(RATOR_CONV(RAND_CONV INT_LE_CONV)) THENC
 928   GEN_REWRITE_CONV I [COND_CLAUSES];;
 929
 930 let INT_MIN_CONV =
 931   REWR_CONV INT_MIN THENC
 932   RATOR_CONV(RATOR_CONV(RAND_CONV INT_LE_CONV)) THENC
 933   GEN_REWRITE_CONV I [COND_CLAUSES];;
 934
 935 (* ------------------------------------------------------------------------- *)
 936 (* Instantiate the normalizer.                                               *)
 937 (* ------------------------------------------------------------------------- *)
 938
 939 let INT_POLY_CONV =
 940   let sth = prove
 941    (`(!x y z. x + (y + z) = (x + y) + z) /\
 942      (!x y. x + y = y + x) /\
 943      (!x. &0 + x = x) /\
 944      (!x y z. x * (y * z) = (x * y) * z) /\
 945      (!x y. x * y = y * x) /\
 946      (!x. &1 * x = x) /\
 947      (!x. &0 * x = &0) /\
 948      (!x y z. x * (y + z) = x * y + x * z) /\
 949      (!x. x pow 0 = &1) /\
 950      (!x n. x pow (SUC n) = x * x pow n)`,
 951     REWRITE_TAC[INT_POW] THEN INT_ARITH_TAC)
 952   and rth = prove
 953    (`(!x. --x = --(&1) * x) /\
 954      (!x y. x - y = x + --(&1) * y)`,
 955     INT_ARITH_TAC)
 956   and is_semiring_constant = is_intconst
 957   and SEMIRING_ADD_CONV = INT_ADD_CONV
 958   and SEMIRING_MUL_CONV = INT_MUL_CONV
 959   and SEMIRING_POW_CONV = INT_POW_CONV in
 960   let _,_,_,_,_,INT_POLY_CONV =
 961     SEMIRING_NORMALIZERS_CONV sth rth
 962      (is_semiring_constant,
 963       SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV)
 964      (<) in
 965   INT_POLY_CONV;;
 966
 967 (* ------------------------------------------------------------------------- *)
 968 (* Instantiate the ring and ideal procedures.                                *)
 969 (* ------------------------------------------------------------------------- *)
 970
 971 let INT_RING,int_ideal_cofactors =
 972   let INT_INTEGRAL = prove
 973    (`(!x. &0 * x = &0) /\
 974      (!x y z. (x + y = x + z) <=> (y = z)) /\
 975      (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
 976     REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
 977     REWRITE_TAC[GSYM INT_OF_NUM_EQ;
 978                 GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_MUL] THEN
 979     ONCE_REWRITE_TAC[GSYM INT_SUB_0] THEN
 980     REWRITE_TAC[GSYM INT_ENTIRE] THEN INT_ARITH_TAC)
 981   and int_ty = `:int` in
 982   let pure,ideal =
 983   RING_AND_IDEAL_CONV
 984       (dest_intconst,mk_intconst,INT_EQ_CONV,
 985        `(--):int->int`,`(+):int->int->int`,`(-):int->int->int`,
 986        genvar bool_ty,`(*):int->int->int`,genvar bool_ty,
 987        `(pow):int->num->int`,
 988        INT_INTEGRAL,TRUTH,INT_POLY_CONV) in
 989   pure,
 990   (fun tms tm -> if forall (fun t -> type_of t = int_ty) (tm::tms)
 991                  then ideal tms tm
 992                  else failwith
 993                   "int_ideal_cofactors: not all terms have type :int");;
 994
 995 (* ------------------------------------------------------------------------- *)
 996 (* Arithmetic operations also on div and rem, hence the whole lot.           *)
 997 (* ------------------------------------------------------------------------- *)
 998
 999 let INT_DIVMOD_UNIQ = prove
1000  (`!m n q r:int. m = q * n + r /\ &0 <= r /\ r < abs n
1001                  ==> m div n = q /\ m rem n = r`,
1002   REPEAT GEN_TAC THEN STRIP_TAC THEN
1003   SUBGOAL_THEN `~(n = &0)` MP_TAC THENL [ASM_INT_ARITH_TAC; ALL_TAC] THEN
1004   DISCH_THEN(STRIP_ASSUME_TAC o SPEC `m:int` o MATCH_MP INT_DIVISION) THEN
1005   ASM_CASES_TAC `m div n = q` THENL
1006    [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC INT_RING; ALL_TAC] THEN
1007   SUBGOAL_THEN `abs(m rem n - r) < abs n` MP_TAC THENL
1008    [ASM_INT_ARITH_TAC; MATCH_MP_TAC(TAUT `~p ==> p ==> q`)] THEN
1009   MATCH_MP_TAC(INT_ARITH
1010    `&1 * abs n <= abs(q - m div n) * abs n /\
1011     abs(m rem n - r) = abs((q - m div n) * n)
1012     ==> ~(abs(m rem n - r) < abs n)`) THEN
1013   CONJ_TAC THENL
1014    [MATCH_MP_TAC INT_LE_RMUL THEN ASM_INT_ARITH_TAC;
1015     AP_TERM_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC INT_RING]);;
1016
1017 let INT_DIV_CONV,INT_REM_CONV =
1018   let pth = prove
1019    (`q * n + r = m ==> &0 <= r ==> r < abs n ==> m div n = q /\ m rem n = r`,
1020     MESON_TAC[INT_DIVMOD_UNIQ])
1021   and m = `m:int` and n = `n:int` and q = `q:int` and r = `r:int`
1022   and dtm = `(div)` and mtm = `(rem)` in
1023   let emod_num x y =
1024     let r = mod_num x y in
1025     if r </ Int 0 then r +/ abs_num y else r in
1026   let equo_num x y = quo_num (x -/ emod_num x y) y in
1027   let INT_DIVMOD_CONV x y =
1028     let k = equo_num x y
1029     and l = emod_num x y in
1030     let th0 = INST [mk_intconst x,m; mk_intconst y,n;
1031                     mk_intconst k,q; mk_intconst l,r] pth in
1032     let tm0 = lhand(lhand(concl th0)) in
1033     let th1 = (LAND_CONV INT_MUL_CONV THENC INT_ADD_CONV) tm0 in
1034     let th2 = MP th0 th1 in
1035     let tm2 = lhand(concl th2) in
1036     let th3 = MP th2 (EQT_ELIM(INT_LE_CONV tm2)) in
1037     let tm3 = lhand(concl th3) in
1038     MP th3 (EQT_ELIM((RAND_CONV INT_ABS_CONV THENC INT_LT_CONV) tm3)) in
1039   (fun tm -> try let l,r = dest_binop dtm tm in
1040                  CONJUNCT1(INT_DIVMOD_CONV (dest_intconst l) (dest_intconst r))
1041              with Failure _ -> failwith "INT_DIV_CONV"),
1042   (fun tm -> try let l,r = dest_binop mtm tm in
1043                  CONJUNCT2(INT_DIVMOD_CONV (dest_intconst l) (dest_intconst r))
1044              with Failure _ -> failwith "INT_MOD_CONV");;
1045
1046 let INT_RED_CONV =
1047   let gconv_net = itlist (uncurry net_of_conv)
1048     [`x <= y`,INT_LE_CONV;
1049      `x < y`,INT_LT_CONV;
1050      `x >= y`,INT_GE_CONV;
1051      `x > y`,INT_GT_CONV;
1052      `x:int = y`,INT_EQ_CONV;
1053      `--x`,CHANGED_CONV INT_NEG_CONV;
1054      `abs(x)`,INT_ABS_CONV;
1055      `x + y`,INT_ADD_CONV;
1056      `x - y`,INT_SUB_CONV;
1057      `x * y`,INT_MUL_CONV;
1058      `x div y`,INT_DIV_CONV;
1059      `x rem y`,INT_REM_CONV;
1060      `x pow n`,INT_POW_CONV;
1061      `max x y`,INT_MAX_CONV;
1062      `min x y`,INT_MIN_CONV]
1063     (basic_net()) in
1064   REWRITES_CONV gconv_net;;
1065
1066 let INT_REDUCE_CONV = DEPTH_CONV INT_RED_CONV;;
1067
1068 (* ------------------------------------------------------------------------- *)
1069 (* Set up overloading so we can use same symbols for N, Z and even R.        *)
1070 (* ------------------------------------------------------------------------- *)
1071
1072 make_overloadable "divides" `:A->A->bool`;;
1073 make_overloadable "mod" `:A->A->A->bool`;;
1074 make_overloadable "coprime" `:A#A->bool`;;
1075 make_overloadable "gcd" `:A#A->A`;;
1076
1077 (* ------------------------------------------------------------------------- *)
1078 (* The general notion of congruence: just syntax for equivalence relation.   *)
1079 (* ------------------------------------------------------------------------- *)
1080
1081 parse_as_infix("==",(10,"right"));;
1082
1083 let cong = new_definition
1084   `(x == y) (rel:A->A->bool) <=> rel x y`;;
1085
1086 (* ------------------------------------------------------------------------- *)
1087 (* Get real moduli defined and out of the way first.                         *)
1088 (* ------------------------------------------------------------------------- *)
1089
1090 let real_mod = new_definition
1091   `real_mod n (x:real) y = ?q. integer q /\ x - y = q * n`;;
1092
1093 overload_interface ("mod",`real_mod`);;
1094
1095 (* ------------------------------------------------------------------------- *)
1096 (* Integer divisibility.                                                     *)
1097 (* ------------------------------------------------------------------------- *)
1098
1099 parse_as_infix("divides",(12,"right"));;
1100 overload_interface("divides",`int_divides:int->int->bool`);;
1101
1102 let int_divides = new_definition
1103   `a divides b <=> ?x. b = a * x`;;
1104
1105 (* ------------------------------------------------------------------------- *)
1106 (* Integer congruences.                                                      *)
1107 (* ------------------------------------------------------------------------- *)
1108
1109 parse_as_prefix "mod";;
1110 overload_interface ("mod",`int_mod:int->int->int->bool`);;
1111
1112 let int_mod = new_definition
1113   `(mod n) x y = n divides (x - y)`;;
1114
1115 let int_congruent = prove
1116  (`!x y n. (x == y) (mod n) <=> ?d. x - y = n * d`,
1117   REWRITE_TAC[int_mod; cong; int_divides]);;
1118
1119 (* ------------------------------------------------------------------------- *)
1120 (* Integer coprimality.                                                      *)
1121 (* ------------------------------------------------------------------------- *)
1122
1123 overload_interface("coprime",`int_coprime:int#int->bool`);;
1124
1125 let int_coprime = new_definition
1126  `!a b. coprime(a,b) <=> ?x y. a * x + b * y = &1`;;
1127
1128 (* ------------------------------------------------------------------------- *)
1129 (* A tactic for simple divisibility/congruence/coprimality goals.            *)
1130 (* ------------------------------------------------------------------------- *)
1131
1132 let INTEGER_TAC =
1133   let int_ty = `:int` in
1134   let INT_POLYEQ_CONV =
1135     GEN_REWRITE_CONV I [GSYM INT_SUB_0] THENC LAND_CONV INT_POLY_CONV in
1136   let ISOLATE_VARIABLE =
1137     let pth = INT_ARITH `!a x. a = &0 <=> x = x + a` in
1138     let is_defined v t =
1139       let mons = striplist(dest_binary "int_add") t in
1140       mem v mons & forall (fun m -> v = m or not(free_in v m)) mons in
1141     fun vars tm ->
1142       let th = INT_POLYEQ_CONV tm
1143       and th' = (SYM_CONV THENC INT_POLYEQ_CONV) tm in
1144       let v,th1 =
1145           try find (fun v -> is_defined v (lhand(rand(concl th)))) vars,th'
1146           with Failure _ ->
1147               find (fun v -> is_defined v (lhand(rand(concl th')))) vars,th in
1148       let th2 = TRANS th1 (SPECL [lhs(rand(concl th1)); v] pth) in
1149       CONV_RULE(RAND_CONV(RAND_CONV INT_POLY_CONV)) th2 in
1150   let UNWIND_POLYS_CONV tm =
1151     let vars,bod = strip_exists tm in
1152     let cjs = conjuncts bod in
1153     let th1 = tryfind (ISOLATE_VARIABLE vars) cjs in
1154     let eq = lhand(concl th1) in
1155     let bod' = list_mk_conj(eq::(subtract cjs [eq])) in
1156     let th2 = CONJ_ACI_RULE(mk_eq(bod,bod')) in
1157     let th3 = TRANS th2 (MK_CONJ th1 (REFL(rand(rand(concl th2))))) in
1158     let v = lhs(lhand(rand(concl th3))) in
1159     let vars' = (subtract vars [v]) @ [v] in
1160     let th4 = CONV_RULE(RAND_CONV(REWR_CONV UNWIND_THM2)) (MK_EXISTS v th3) in
1161     let IMP_RULE v v' =
1162      DISCH_ALL(itlist SIMPLE_CHOOSE v (itlist SIMPLE_EXISTS v' (ASSUME bod))) in
1163     let th5 = IMP_ANTISYM_RULE (IMP_RULE vars vars') (IMP_RULE vars' vars) in
1164     TRANS th5 (itlist MK_EXISTS (subtract vars [v]) th4) in
1165   let zero_tm = `&0` and one_tm = `&1` in
1166   let isolate_monomials =
1167     let mul_tm = `(int_mul)` and add_tm = `(int_add)`
1168     and neg_tm = `(int_neg)` in
1169     let dest_mul = dest_binop mul_tm
1170     and dest_add = dest_binop add_tm
1171     and mk_mul = mk_binop mul_tm
1172     and mk_add = mk_binop add_tm in
1173     let scrub_var v m =
1174       let ps = striplist dest_mul m in
1175       let ps' = subtract ps [v] in
1176       if ps' = [] then one_tm else end_itlist mk_mul ps' in
1177     let find_multipliers v mons =
1178       let mons1 = filter (fun m -> free_in v m) mons in
1179       let mons2 = map (scrub_var v) mons1 in
1180       if mons2 = [] then zero_tm else end_itlist mk_add mons2 in
1181     fun vars tm ->
1182       let cmons,vmons =
1183          partition (fun m -> intersect (frees m) vars = [])
1184                    (striplist dest_add tm) in
1185       let cofactors = map (fun v -> find_multipliers v vmons) vars
1186       and cnc = if cmons = [] then zero_tm
1187                 else mk_comb(neg_tm,end_itlist mk_add cmons) in
1188       cofactors,cnc in
1189   let isolate_variables evs ps eq =
1190     let vars = filter (fun v -> vfree_in v eq) evs in
1191     let qs,p = isolate_monomials vars eq in
1192     let rs = filter (fun t -> type_of t = int_ty) (qs @ ps) in
1193     let rs = int_ideal_cofactors rs p in
1194     eq,zip (fst(chop_list(length qs) rs)) vars in
1195   let subst_in_poly i p = rhs(concl(INT_POLY_CONV (vsubst i p))) in
1196   let rec solve_idealism evs ps eqs =
1197     if evs = [] then [] else
1198     let eq,cfs = tryfind (isolate_variables evs ps) eqs in
1199     let evs' = subtract evs (map snd cfs)
1200     and eqs' = map (subst_in_poly cfs) (subtract eqs [eq]) in
1201     cfs @ solve_idealism evs' ps eqs' in
1202   let rec GENVAR_EXISTS_CONV tm =
1203     if not(is_exists tm) then REFL tm else
1204     let ev,bod = dest_exists tm in
1205     let gv = genvar(type_of ev) in
1206     (GEN_ALPHA_CONV gv THENC BINDER_CONV GENVAR_EXISTS_CONV) tm in
1207   let EXISTS_POLY_TAC (asl,w as gl) =
1208     let evs,bod = strip_exists w
1209     and ps = mapfilter (check (fun t -> type_of t = int_ty) o
1210                         lhs o concl o snd) asl in
1211     let cfs = solve_idealism evs ps (map lhs (conjuncts bod)) in
1212     (MAP_EVERY EXISTS_TAC(map (fun v -> rev_assocd v cfs zero_tm) evs) THEN
1213      REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC INT_RING) gl in
1214   let SCRUB_NEQ_TAC = MATCH_MP_TAC o MATCH_MP (MESON[]
1215     `~(x = y) ==> x = y \/ p ==> p`) in
1216   REWRITE_TAC[int_coprime; int_congruent; int_divides] THEN
1217   REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN
1218   REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM;
1219               LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM] THEN
1220   CONV_TAC(REPEATC UNWIND_POLYS_CONV) THEN
1221   REPEAT(FIRST_X_ASSUM SCRUB_NEQ_TAC) THEN
1222   REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM;
1223               LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM] THEN
1224   REPEAT(FIRST_X_ASSUM(MP_TAC o SYM)) THEN
1225   CONV_TAC(ONCE_DEPTH_CONV INT_POLYEQ_CONV) THEN
1226   REWRITE_TAC[GSYM INT_ENTIRE;
1227               TAUT `a \/ (b /\ c) <=> (a \/ b) /\ (a \/ c)`] THEN
1228   POP_ASSUM_LIST(K ALL_TAC) THEN
1229   REPEAT DISCH_TAC THEN CONV_TAC GENVAR_EXISTS_CONV THEN
1230   CONV_TAC(ONCE_DEPTH_CONV INT_POLYEQ_CONV) THEN EXISTS_POLY_TAC;;
1231
1232 let INTEGER_RULE tm = prove(tm,INTEGER_TAC);;
1233
1234 (* ------------------------------------------------------------------------- *)
1235 (* Existence of integer gcd, and the Bezout identity.                        *)
1236 (* ------------------------------------------------------------------------- *)
1237
1238 let WF_INT_MEASURE = prove
1239  (`!P m. (!x. &0 <= m(x)) /\ (!x. (!y. m(y) < m(x) ==> P(y)) ==> P(x))
1240          ==> !x:A. P(x)`,
1241   REPEAT STRIP_TAC THEN SUBGOAL_THEN `!n x:A. m(x) = &n ==> P(x)` MP_TAC THENL
1242    [MATCH_MP_TAC num_WF; ALL_TAC] THEN
1243   REWRITE_TAC[GSYM INT_OF_NUM_LT; INT_FORALL_POS] THEN ASM_MESON_TAC[]);;
1244
1245 let WF_INT_MEASURE_2 = prove
1246  (`!P m. (!x y. &0 <= m x y) /\
1247          (!x y. (!x' y'. m x' y' < m x y ==> P x' y') ==> P x y)
1248          ==> !x:A y:B. P x y`,
1249   REWRITE_TAC[FORALL_UNCURRY; GSYM FORALL_PAIR_THM; WF_INT_MEASURE]);;
1250
1251 let INT_GCD_EXISTS = prove
1252  (`!a b. ?d. d divides a /\ d divides b /\ ?x y. d = a * x + b * y`,
1253   let INT_GCD_EXISTS_CASES = INT_ARITH
1254    `(a = &0 \/ b = &0) \/
1255     abs(a - b) + abs b < abs a + abs b \/ abs(a + b) + abs b < abs a + abs b \/
1256     abs a + abs(b - a) < abs a + abs b \/ abs a + abs(b + a) < abs a + abs b` in
1257   MATCH_MP_TAC WF_INT_MEASURE_2 THEN EXISTS_TAC `\x y. abs(x) + abs(y)` THEN
1258   REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL [INT_ARITH_TAC; ALL_TAC] THEN
1259   DISJ_CASES_THEN MP_TAC INT_GCD_EXISTS_CASES THENL
1260    [STRIP_TAC THEN ASM_REWRITE_TAC[INTEGER_RULE `d divides &0`] THEN
1261     REWRITE_TAC[INT_MUL_LZERO; INT_ADD_LID; INT_ADD_RID] THEN
1262     MESON_TAC[INTEGER_RULE `d divides d`; INT_MUL_RID];
1263     DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (ANTE_RES_THEN MP_TAC)) THEN
1264     MATCH_MP_TAC MONO_EXISTS THEN INTEGER_TAC]);;
1265
1266 let INT_GCD_EXISTS_POS = prove
1267  (`!a b. ?d. &0 <= d /\ d divides a /\ d divides b /\ ?x y. d = a * x + b * y`,
1268   REPEAT GEN_TAC THEN
1269   X_CHOOSE_TAC `d:int` (SPECL [`a:int`; `b:int`] INT_GCD_EXISTS) THEN
1270   DISJ_CASES_TAC(SPEC `d:int` INT_LE_NEGTOTAL) THEN
1271   ASM_MESON_TAC[INTEGER_RULE `(--d) divides x <=> d divides x`;
1272                 INT_ARITH `a * --x + b * --y = --(a * x + b * y)`]);;
1273
1274 (* ------------------------------------------------------------------------- *)
1275 (* Hence define (positive) gcd function; add elimination to INTEGER_TAC.      *)
1276 (* ------------------------------------------------------------------------- *)
1277
1278 overload_interface("gcd",`int_gcd:int#int->int`);;
1279
1280 let int_gcd = new_specification ["int_gcd"]
1281  (REWRITE_RULE[EXISTS_UNCURRY; SKOLEM_THM] INT_GCD_EXISTS_POS);;
1282
1283 let INTEGER_TAC =
1284   let GCD_ELIM_TAC =
1285     let gcd_tm = `gcd` in
1286     let dest_gcd tm =
1287       let l,r = dest_comb tm in
1288       if l = gcd_tm then dest_pair r else failwith "dest_gcd" in
1289     REPEAT GEN_TAC THEN
1290     W(fun (asl,w) ->
1291           let gts = find_terms (can dest_gcd) w in
1292           let ths = map
1293            (fun tm -> let a,b = dest_gcd tm in SPECL [a;b] int_gcd) gts in
1294           MAP_EVERY MP_TAC ths THEN
1295           MAP_EVERY SPEC_TAC (zip gts (map (genvar o type_of) gts))) in
1296   REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN GCD_ELIM_TAC THEN INTEGER_TAC;;
1297
1298 let INTEGER_RULE tm = prove(tm,INTEGER_TAC);;
1299
1300 (* ------------------------------------------------------------------------- *)
1301 (* Mapping from nonnegative integers back to natural numbers.                *)
1302 (* ------------------------------------------------------------------------- *)
1303
1304 let num_of_int = new_definition
1305   `num_of_int x = @n. &n = x`;;
1306
1307 let NUM_OF_INT_OF_NUM = prove
1308  (`!n. num_of_int(&n) = n`,
1309   REWRITE_TAC[num_of_int; INT_OF_NUM_EQ; SELECT_UNIQUE]);;
1310
1311 let INT_OF_NUM_OF_INT = prove
1312  (`!x. &0 <= x ==> &(num_of_int x) = x`,
1313   REWRITE_TAC[GSYM INT_FORALL_POS; num_of_int] THEN
1314   GEN_TAC THEN CONV_TAC SELECT_CONV THEN MESON_TAC[]);;
1315
1316 let NUM_OF_INT = prove
1317  (`!x. &0 <= x <=> (&(num_of_int x) = x)`,
1318   MESON_TAC[INT_OF_NUM_OF_INT; INT_POS]);;
1319
1320 (* ------------------------------------------------------------------------- *)
1321 (* Now define similar notions over the natural numbers.                      *)
1322 (* ------------------------------------------------------------------------- *)
1323
1324 overload_interface("divides",`num_divides:num->num->bool`);;
1325 overload_interface ("mod",`num_mod:num->num->num->bool`);;
1326 overload_interface("coprime",`num_coprime:num#num->bool`);;
1327 overload_interface("gcd",`num_gcd:num#num->num`);;
1328
1329 let num_divides = new_definition
1330  `a divides b <=> &a divides &b`;;
1331
1332 let num_mod = new_definition
1333   `(mod n) x y <=> (mod &n) (&x) (&y)`;;
1334
1335 let num_congruent = prove
1336  (`!x y n. (x == y) (mod n) <=> (&x == &y) (mod &n)`,
1337   REWRITE_TAC[cong; num_mod]);;
1338
1339 let num_coprime = new_definition
1340  `coprime(a,b) <=> coprime(&a,&b)`;;
1341
1342 let num_gcd = new_definition
1343  `gcd(a,b) = num_of_int(gcd(&a,&b))`;;
1344
1345 (* ------------------------------------------------------------------------- *)
1346 (* Map an assertion over N to an integer equivalent.                         *)
1347 (* To make this work nicely, all variables of type num should be quantified. *)
1348 (* ------------------------------------------------------------------------- *)
1349
1350 let NUM_TO_INT_CONV =
1351   let pth_relativize = prove
1352    (`((!n. P(&n)) <=> (!i. ~(&0 <= i) \/ P i)) /\
1353      ((?n. P(&n)) <=> (?i. &0 <= i /\ P i))`,
1354     REWRITE_TAC[INT_EXISTS_POS; INT_FORALL_POS] THEN MESON_TAC[]) in
1355   let relation_conv = (GEN_REWRITE_CONV TOP_SWEEP_CONV o map GSYM)
1356    [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE; INT_OF_NUM_GT;
1357     INT_OF_NUM_SUC; INT_OF_NUM_ADD; INT_OF_NUM_MUL; INT_OF_NUM_POW]
1358   and quantifier_conv = GEN_REWRITE_CONV DEPTH_CONV [pth_relativize] in
1359   NUM_SIMPLIFY_CONV THENC relation_conv THENC quantifier_conv;;
1360
1361 (* ------------------------------------------------------------------------- *)
1362 (* Linear decision procedure for the naturals at last!                       *)
1363 (* ------------------------------------------------------------------------- *)
1364
1365 let ARITH_RULE =
1366   let init_conv =
1367     NUM_SIMPLIFY_CONV THENC
1368     GEN_REWRITE_CONV DEPTH_CONV [ADD1] THENC
1369     PROP_ATOM_CONV (BINOP_CONV NUM_NORMALIZE_CONV) THENC
1370     PRENEX_CONV THENC
1371     (GEN_REWRITE_CONV TOP_SWEEP_CONV o map GSYM)
1372       [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE;
1373        INT_OF_NUM_GT; INT_OF_NUM_ADD; SPEC `NUMERAL k` INT_OF_NUM_MUL;
1374        INT_OF_NUM_MAX; INT_OF_NUM_MIN]
1375   and is_numimage t =
1376     match t with
1377       Comb(Const("int_of_num",_),n) when not(is_numeral n) -> true
1378     | _ -> false in
1379   fun tm ->
1380     let th1 = init_conv tm in
1381     let tm1 = rand(concl th1) in
1382     let avs,bod = strip_forall tm1 in
1383     let nim = setify(find_terms is_numimage bod) in
1384     let gvs = map (genvar o type_of) nim in
1385     let pths = map (fun v -> SPEC (rand v) INT_POS) nim in
1386     let ibod = itlist (curry mk_imp o concl) pths bod in
1387     let gbod = subst (zip gvs nim) ibod in
1388     let th2 = INST (zip nim gvs) (INT_ARITH gbod) in
1389     let th3 = GENL avs (rev_itlist (C MP) pths th2) in
1390     EQ_MP (SYM th1) th3;;
1391
1392 let ARITH_TAC = CONV_TAC(EQT_INTRO o ARITH_RULE);;
1393
1394 let ASM_ARITH_TAC =
1395   REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
1396   ARITH_TAC;;
1397
1398 (* ------------------------------------------------------------------------- *)
1399 (* Also a similar divisibility procedure for natural numbers.                *)
1400 (* ------------------------------------------------------------------------- *)
1401
1402 let NUM_GCD = prove
1403  (`!a b. &(gcd(a,b)) = gcd(&a,&b)`,
1404   REWRITE_TAC[num_gcd; GSYM NUM_OF_INT; int_gcd]);;
1405
1406 let NUMBER_TAC =
1407   let pth_relativize = prove
1408    (`((!n. P(&n)) <=> (!i. &0 <= i ==> P i)) /\
1409      ((?n. P(&n)) <=> (?i. &0 <= i /\ P i))`,
1410     GEN_REWRITE_TAC RAND_CONV [TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
1411     REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_POS] THEN MESON_TAC[]) in
1412   let relation_conv =
1413    GEN_REWRITE_CONV TOP_SWEEP_CONV
1414     (num_divides::num_congruent::num_coprime::NUM_GCD::(map GSYM
1415     [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE; INT_OF_NUM_GT;
1416      INT_OF_NUM_SUC; INT_OF_NUM_ADD; INT_OF_NUM_MUL; INT_OF_NUM_POW]))
1417   and quantifier_conv = GEN_REWRITE_CONV DEPTH_CONV [pth_relativize] in
1418   W(fun (_,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
1419   CONV_TAC(relation_conv THENC quantifier_conv) THEN
1420   REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN REPEAT GEN_TAC THEN
1421   INTEGER_TAC;;
1422
1423 let NUMBER_RULE tm = prove(tm,NUMBER_TAC);;
1424
1425 let divides = prove
1426  (`a divides b <=> ?x. b = a * x`,
1427   EQ_TAC THENL [REWRITE_TAC[num_divides; int_divides]; NUMBER_TAC] THEN
1428   DISCH_THEN(X_CHOOSE_TAC `x:int`) THEN EXISTS_TAC `num_of_int(abs x)` THEN
1429   SIMP_TAC[GSYM INT_OF_NUM_EQ;
1430            INT_ARITH `&m:int = &n <=> abs(&m :int) = abs(&n)`] THEN
1431   ASM_REWRITE_TAC[GSYM INT_OF_NUM_MUL; INT_ABS_MUL] THEN
1432   SIMP_TAC[INT_OF_NUM_OF_INT; INT_ABS_POS; INT_ABS_ABS]);;
1433
1434 let DIVIDES_LE = prove
1435  (`!m n. m divides n ==> m <= n \/ n = 0`,
1436   SUBGOAL_THEN `!m n. m <= m * n \/ m * n = 0`
1437     (fun th -> MESON_TAC[divides; th]) THEN
1438   REWRITE_TAC[LE_MULT_LCANCEL; MULT_EQ_0; ARITH_RULE
1439    `m <= m * n <=> m * 1 <= m * n`] THEN
1440   ASM_ARITH_TAC);;
1441
1442 (* ------------------------------------------------------------------------- *)
1443 (* Make sure we give priority to N.                                          *)
1444 (* ------------------------------------------------------------------------- *)
1445
1446 prioritize_num();;