arith.ml

   1 (* ========================================================================= *)
   2 (* Natural number arithmetic.                                                *)
   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 "recursion.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Note: all the following proofs are intuitionistic and intensional, except *)
  14 (* for the least number principle num_WOP.                                   *)
  15 (* (And except the arith rewrites at the end; these could be done that way   *)
  16 (* but they use the conditional anyway.) In fact, one could very easily      *)
  17 (* write a "decider" returning P \/ ~P for quantifier-free P.                *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 parse_as_infix("<",(12,"right"));;
  21 parse_as_infix("<=",(12,"right"));;
  22 parse_as_infix(">",(12,"right"));;
  23 parse_as_infix(">=",(12,"right"));;
  24
  25 parse_as_infix("+",(16,"right"));;
  26 parse_as_infix("-",(18,"left"));;
  27 parse_as_infix("*",(20,"right"));;
  28 parse_as_infix("EXP",(24,"left"));;
  29
  30 parse_as_infix("DIV",(22,"left"));;
  31 parse_as_infix("MOD",(22,"left"));;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* The predecessor function.                                                 *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let PRE = new_recursive_definition num_RECURSION
  38  `(PRE 0 = 0) /\
  39   (!n. PRE (SUC n) = n)`;;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Addition.                                                                 *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 let ADD = new_recursive_definition num_RECURSION
  46  `(!n. 0 + n = n) /\
  47   (!m n. (SUC m) + n = SUC(m + n))`;;
  48
  49 let ADD_0 = prove
  50  (`!m. m + 0 = m`,
  51   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);;
  52
  53 let ADD_SUC = prove
  54  (`!m n. m + (SUC n) = SUC(m + n)`,
  55   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);;
  56
  57 let ADD_CLAUSES = prove
  58  (`(!n. 0 + n = n) /\
  59    (!m. m + 0 = m) /\
  60    (!m n. (SUC m) + n = SUC(m + n)) /\
  61    (!m n. m + (SUC n) = SUC(m + n))`,
  62   REWRITE_TAC[ADD; ADD_0; ADD_SUC]);;
  63
  64 let ADD_SYM = prove
  65  (`!m n. m + n = n + m`,
  66   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
  67
  68 let ADD_ASSOC = prove
  69  (`!m n p. m + (n + p) = (m + n) + p`,
  70   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]);;
  71
  72 let ADD_AC = prove
  73  (`(m + n = n + m) /\
  74    ((m + n) + p = m + (n + p)) /\
  75    (m + (n + p) = n + (m + p))`,
  76   MESON_TAC[ADD_ASSOC; ADD_SYM]);;
  77
  78 let ADD_EQ_0 = prove
  79  (`!m n. (m + n = 0) <=> (m = 0) /\ (n = 0)`,
  80   REPEAT INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; NOT_SUC]);;
  81
  82 let EQ_ADD_LCANCEL = prove
  83  (`!m n p. (m + n = m + p) <=> (n = p)`,
  84   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; SUC_INJ]);;
  85
  86 let EQ_ADD_RCANCEL = prove
  87  (`!m n p. (m + p = n + p) <=> (m = n)`,
  88   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC EQ_ADD_LCANCEL);;
  89
  90 let EQ_ADD_LCANCEL_0 = prove
  91  (`!m n. (m + n = m) <=> (n = 0)`,
  92   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; SUC_INJ]);;
  93
  94 let EQ_ADD_RCANCEL_0 = prove
  95  (`!m n. (m + n = n) <=> (m = 0)`,
  96   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC EQ_ADD_LCANCEL_0);;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Now define "bitwise" binary representation of numerals.                   *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 let BIT0 = prove
 103  (`!n. BIT0 n = n + n`,
 104   INDUCT_TAC THEN ASM_REWRITE_TAC[BIT0_DEF; ADD_CLAUSES]);;
 105
 106 let BIT1 = prove
 107  (`!n. BIT1 n = SUC(n + n)`,
 108   REWRITE_TAC[BIT1_DEF; BIT0]);;
 109
 110 let BIT0_THM = prove
 111  (`!n. NUMERAL (BIT0 n) = NUMERAL n + NUMERAL n`,
 112   REWRITE_TAC[NUMERAL; BIT0]);;
 113
 114 let BIT1_THM = prove
 115  (`!n. NUMERAL (BIT1 n) = SUC(NUMERAL n + NUMERAL n)`,
 116   REWRITE_TAC[NUMERAL; BIT1]);;
 117
 118 (* ------------------------------------------------------------------------- *)
 119 (* Following is handy before num_CONV arrives.                               *)
 120 (* ------------------------------------------------------------------------- *)
 121
 122 let ONE = prove
 123  (`1 = SUC 0`,
 124   REWRITE_TAC[BIT1; REWRITE_RULE[NUMERAL] ADD_CLAUSES; NUMERAL]);;
 125
 126 let TWO = prove
 127  (`2 = SUC 1`,
 128   REWRITE_TAC[BIT0; BIT1; REWRITE_RULE[NUMERAL] ADD_CLAUSES; NUMERAL]);;
 129
 130 (* ------------------------------------------------------------------------- *)
 131 (* One immediate consequence.                                                *)
 132 (* ------------------------------------------------------------------------- *)
 133
 134 let ADD1 = prove
 135  (`!m. SUC m = m + 1`,
 136   REWRITE_TAC[BIT1_THM; ADD_CLAUSES]);;
 137
 138 (* ------------------------------------------------------------------------- *)
 139 (* Multiplication.                                                           *)
 140 (* ------------------------------------------------------------------------- *)
 141
 142 let MULT = new_recursive_definition num_RECURSION
 143  `(!n. 0 * n = 0) /\
 144   (!m n. (SUC m) * n = (m * n) + n)`;;
 145
 146 let MULT_0 = prove
 147  (`!m. m * 0 = 0`,
 148   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES]);;
 149
 150 let MULT_SUC = prove
 151  (`!m n. m * (SUC n) = m + (m * n)`,
 152   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES; ADD_ASSOC]);;
 153
 154 let MULT_CLAUSES = prove
 155  (`(!n. 0 * n = 0) /\
 156    (!m. m * 0 = 0) /\
 157    (!n. 1 * n = n) /\
 158    (!m. m * 1 = m) /\
 159    (!m n. (SUC m) * n = (m * n) + n) /\
 160    (!m n. m * (SUC n) = m + (m * n))`,
 161   REWRITE_TAC[BIT1_THM; MULT; MULT_0; MULT_SUC; ADD_CLAUSES]);;
 162
 163 let MULT_SYM = prove
 164  (`!m n. m * n = n * m`,
 165   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; EQT_INTRO(SPEC_ALL ADD_SYM)]);;
 166
 167 let LEFT_ADD_DISTRIB = prove
 168  (`!m n p. m * (n + p) = (m * n) + (m * p)`,
 169   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD; MULT_CLAUSES; ADD_ASSOC]);;
 170
 171 let RIGHT_ADD_DISTRIB = prove
 172  (`!m n p. (m + n) * p = (m * p) + (n * p)`,
 173   ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_ACCEPT_TAC LEFT_ADD_DISTRIB);;
 174
 175 let MULT_ASSOC = prove
 176  (`!m n p. m * (n * p) = (m * n) * p`,
 177   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; RIGHT_ADD_DISTRIB]);;
 178
 179 let MULT_AC = prove
 180  (`(m * n = n * m) /\
 181    ((m * n) * p = m * (n * p)) /\
 182    (m * (n * p) = n * (m * p))`,
 183   MESON_TAC[MULT_ASSOC; MULT_SYM]);;
 184
 185 let MULT_EQ_0 = prove
 186  (`!m n. (m * n = 0) <=> (m = 0) \/ (n = 0)`,
 187   REPEAT INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; NOT_SUC]);;
 188
 189 let EQ_MULT_LCANCEL = prove
 190  (`!m n p. (m * n = m * p) <=> (m = 0) \/ (n = p)`,
 191   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
 192   REPEAT INDUCT_TAC THEN
 193   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; GSYM NOT_SUC; NOT_SUC] THEN
 194   ASM_REWRITE_TAC[SUC_INJ; GSYM ADD_ASSOC; EQ_ADD_LCANCEL]);;
 195
 196 let EQ_MULT_RCANCEL = prove
 197  (`!m n p. (m * p = n * p) <=> (m = n) \/ (p = 0)`,
 198   ONCE_REWRITE_TAC[MULT_SYM; DISJ_SYM] THEN MATCH_ACCEPT_TAC EQ_MULT_LCANCEL);;
 199
 200 let MULT_2 = prove
 201  (`!n. 2 * n = n + n`,
 202   GEN_TAC THEN REWRITE_TAC[BIT0_THM; MULT_CLAUSES; RIGHT_ADD_DISTRIB]);;
 203
 204 let MULT_EQ_1 = prove
 205  (`!m n. (m * n = 1) <=> (m = 1) /\ (n = 1)`,
 206   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC
 207     [MULT_CLAUSES; ADD_CLAUSES; BIT0_THM; BIT1_THM; GSYM NOT_SUC] THEN
 208   REWRITE_TAC[SUC_INJ; ADD_EQ_0; MULT_EQ_0] THEN
 209   CONV_TAC TAUT);;
 210
 211 (* ------------------------------------------------------------------------- *)
 212 (* Exponentiation.                                                           *)
 213 (* ------------------------------------------------------------------------- *)
 214
 215 let EXP = new_recursive_definition num_RECURSION
 216  `(!m. m EXP 0 = 1) /\
 217   (!m n. m EXP (SUC n) = m * (m EXP n))`;;
 218
 219 let EXP_EQ_0 = prove
 220  (`!m n. (m EXP n = 0) <=> (m = 0) /\ ~(n = 0)`,
 221   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC
 222     [BIT1_THM; NOT_SUC; NOT_SUC; EXP; MULT_CLAUSES; ADD_CLAUSES; ADD_EQ_0]);;
 223
 224 let EXP_EQ_1 = prove
 225  (`!x n. x EXP n = 1 <=> x = 1 \/ n = 0`,
 226   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[EXP; MULT_EQ_1; NOT_SUC] THEN
 227   CONV_TAC TAUT);;
 228
 229 let EXP_ZERO = prove
 230  (`!n. 0 EXP n = if n = 0 then 1 else 0`,
 231   GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[EXP_EQ_0; EXP_EQ_1]);;
 232
 233 let EXP_ADD = prove
 234  (`!m n p. m EXP (n + p) = (m EXP n) * (m EXP p)`,
 235   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 236   ASM_REWRITE_TAC[EXP; ADD_CLAUSES; MULT_CLAUSES; MULT_AC]);;
 237
 238 let EXP_ONE = prove
 239  (`!n. 1 EXP n = 1`,
 240   INDUCT_TAC THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES]);;
 241
 242 let EXP_1 = prove
 243  (`!n. n EXP 1 = n`,
 244   REWRITE_TAC[ONE; EXP; MULT_CLAUSES; ADD_CLAUSES]);;
 245
 246 let EXP_2 = prove
 247  (`!n. n EXP 2 = n * n`,
 248   REWRITE_TAC[BIT0_THM; BIT1_THM; EXP; EXP_ADD; MULT_CLAUSES; ADD_CLAUSES]);;
 249
 250 let MULT_EXP = prove
 251  (`!p m n. (m * n) EXP p = m EXP p * n EXP p`,
 252   INDUCT_TAC THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES; MULT_AC]);;
 253
 254 let EXP_MULT = prove
 255  (`!m n p. m EXP (n * p) = (m EXP n) EXP p`,
 256   GEN_TAC THEN INDUCT_TAC THEN
 257   ASM_REWRITE_TAC[EXP_ADD; EXP; MULT_CLAUSES] THENL
 258    [CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
 259     INDUCT_TAC THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES];
 260     REWRITE_TAC[MULT_EXP] THEN MATCH_ACCEPT_TAC MULT_SYM]);;
 261
 262 (* ------------------------------------------------------------------------- *)
 263 (* Define the orderings recursively too.                                     *)
 264 (* ------------------------------------------------------------------------- *)
 265
 266 let LE = new_recursive_definition num_RECURSION
 267  `(!m. (m <= 0) <=> (m = 0)) /\
 268   (!m n. (m <= SUC n) <=> (m = SUC n) \/ (m <= n))`;;
 269
 270 let LT = new_recursive_definition num_RECURSION
 271  `(!m. (m < 0) <=> F) /\
 272   (!m n. (m < SUC n) <=> (m = n) \/ (m < n))`;;
 273
 274 let GE = new_definition
 275   `m >= n <=> n <= m`;;
 276
 277 let GT = new_definition
 278   `m > n <=> n < m`;;
 279
 280 (* ------------------------------------------------------------------------- *)
 281 (* Maximum and minimum of natural numbers.                                   *)
 282 (* ------------------------------------------------------------------------- *)
 283
 284 let MAX = new_definition
 285   `!m n. MAX m n = if m <= n then n else m`;;
 286
 287 let MIN = new_definition
 288   `!m n. MIN m n = if m <= n then m else n`;;
 289
 290 (* ------------------------------------------------------------------------- *)
 291 (* Step cases.                                                               *)
 292 (* ------------------------------------------------------------------------- *)
 293
 294 let LE_SUC_LT = prove
 295  (`!m n. (SUC m <= n) <=> (m < n)`,
 296   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LE; LT; NOT_SUC; SUC_INJ]);;
 297
 298 let LT_SUC_LE = prove
 299  (`!m n. (m < SUC n) <=> (m <= n)`,
 300   GEN_TAC THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[LT; LE] THEN
 301   ASM_REWRITE_TAC[] THEN REWRITE_TAC[LT]);;
 302
 303 let LE_SUC = prove
 304  (`!m n. (SUC m <= SUC n) <=> (m <= n)`,
 305   REWRITE_TAC[LE_SUC_LT; LT_SUC_LE]);;
 306
 307 let LT_SUC = prove
 308  (`!m n. (SUC m < SUC n) <=> (m < n)`,
 309   REWRITE_TAC[LT_SUC_LE; LE_SUC_LT]);;
 310
 311 (* ------------------------------------------------------------------------- *)
 312 (* Base cases.                                                               *)
 313 (* ------------------------------------------------------------------------- *)
 314
 315 let LE_0 = prove
 316  (`!n. 0 <= n`,
 317   INDUCT_TAC THEN ASM_REWRITE_TAC[LE]);;
 318
 319 let LT_0 = prove
 320  (`!n. 0 < SUC n`,
 321   REWRITE_TAC[LT_SUC_LE; LE_0]);;
 322
 323 (* ------------------------------------------------------------------------- *)
 324 (* Reflexivity.                                                              *)
 325 (* ------------------------------------------------------------------------- *)
 326
 327 let LE_REFL = prove
 328  (`!n. n <= n`,
 329   INDUCT_TAC THEN REWRITE_TAC[LE]);;
 330
 331 let LT_REFL = prove
 332  (`!n. ~(n < n)`,
 333   INDUCT_TAC THEN ASM_REWRITE_TAC[LT_SUC] THEN REWRITE_TAC[LT]);;
 334
 335 (* ------------------------------------------------------------------------- *)
 336 (* Antisymmetry.                                                             *)
 337 (* ------------------------------------------------------------------------- *)
 338
 339 let LE_ANTISYM = prove
 340  (`!m n. (m <= n /\ n <= m) <=> (m = n)`,
 341   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_SUC; SUC_INJ] THEN
 342   REWRITE_TAC[LE; NOT_SUC; GSYM NOT_SUC]);;
 343
 344 let LT_ANTISYM = prove
 345  (`!m n. ~(m < n /\ n < m)`,
 346   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LT_SUC] THEN REWRITE_TAC[LT]);;
 347
 348 let LET_ANTISYM = prove
 349  (`!m n. ~(m <= n /\ n < m)`,
 350   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_SUC; LT_SUC] THEN
 351   REWRITE_TAC[LE; LT; NOT_SUC]);;
 352
 353 let LTE_ANTISYM = prove
 354  (`!m n. ~(m < n /\ n <= m)`,
 355   ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[LET_ANTISYM]);;
 356
 357 (* ------------------------------------------------------------------------- *)
 358 (* Transitivity.                                                             *)
 359 (* ------------------------------------------------------------------------- *)
 360
 361 let LE_TRANS = prove
 362  (`!m n p. m <= n /\ n <= p ==> m <= p`,
 363   REPEAT INDUCT_TAC THEN
 364   ASM_REWRITE_TAC[LE_SUC; LE_0] THEN REWRITE_TAC[LE; NOT_SUC]);;
 365
 366 let LT_TRANS = prove
 367  (`!m n p. m < n /\ n < p ==> m < p`,
 368   REPEAT INDUCT_TAC THEN
 369   ASM_REWRITE_TAC[LT_SUC; LT_0] THEN REWRITE_TAC[LT; NOT_SUC]);;
 370
 371 let LET_TRANS = prove
 372  (`!m n p. m <= n /\ n < p ==> m < p`,
 373   REPEAT INDUCT_TAC THEN
 374   ASM_REWRITE_TAC[LE_SUC; LT_SUC; LT_0] THEN REWRITE_TAC[LT; LE; NOT_SUC]);;
 375
 376 let LTE_TRANS = prove
 377  (`!m n p. m < n /\ n <= p ==> m < p`,
 378   REPEAT INDUCT_TAC THEN
 379   ASM_REWRITE_TAC[LE_SUC; LT_SUC; LT_0] THEN REWRITE_TAC[LT; LE; NOT_SUC]);;
 380
 381 (* ------------------------------------------------------------------------- *)
 382 (* Totality.                                                                 *)
 383 (* ------------------------------------------------------------------------- *)
 384
 385 let LE_CASES = prove
 386  (`!m n. m <= n \/ n <= m`,
 387   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_0; LE_SUC]);;
 388
 389 let LT_CASES = prove
 390  (`!m n. (m < n) \/ (n < m) \/ (m = n)`,
 391   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LT_SUC; SUC_INJ] THEN
 392   REWRITE_TAC[LT; NOT_SUC; GSYM NOT_SUC] THEN
 393   W(W (curry SPEC_TAC) o hd o frees o snd) THEN
 394   INDUCT_TAC THEN REWRITE_TAC[LT_0]);;
 395
 396 let LET_CASES = prove
 397  (`!m n. m <= n \/ n < m`,
 398   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_SUC_LT; LT_SUC_LE; LE_0]);;
 399
 400 let LTE_CASES = prove
 401  (`!m n. m < n \/ n <= m`,
 402   ONCE_REWRITE_TAC[DISJ_SYM] THEN MATCH_ACCEPT_TAC LET_CASES);;
 403
 404 (* ------------------------------------------------------------------------- *)
 405 (* Relationship between orderings.                                           *)
 406 (* ------------------------------------------------------------------------- *)
 407
 408 let LE_LT = prove
 409  (`!m n. (m <= n) <=> (m < n) \/ (m = n)`,
 410   REPEAT INDUCT_TAC THEN
 411   ASM_REWRITE_TAC[LE_SUC; LT_SUC; SUC_INJ; LE_0; LT_0] THEN
 412   REWRITE_TAC[LE; LT]);;
 413
 414 let LT_LE = prove
 415  (`!m n. (m < n) <=> (m <= n) /\ ~(m = n)`,
 416   REWRITE_TAC[LE_LT] THEN REPEAT GEN_TAC THEN EQ_TAC THENL
 417    [DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN
 418     POP_ASSUM MP_TAC THEN REWRITE_TAC[LT_REFL];
 419     DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
 420     ASM_REWRITE_TAC[]]);;
 421
 422 let NOT_LE = prove
 423  (`!m n. ~(m <= n) <=> (n < m)`,
 424   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_SUC; LT_SUC] THEN
 425   REWRITE_TAC[LE; LT; NOT_SUC; GSYM NOT_SUC; LE_0] THEN
 426   W(W (curry SPEC_TAC) o hd o frees o snd) THEN
 427   INDUCT_TAC THEN REWRITE_TAC[LT_0]);;
 428
 429 let NOT_LT = prove
 430  (`!m n. ~(m < n) <=> n <= m`,
 431   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[LE_SUC; LT_SUC] THEN
 432   REWRITE_TAC[LE; LT; NOT_SUC; GSYM NOT_SUC; LE_0] THEN
 433   W(W (curry SPEC_TAC) o hd o frees o snd) THEN
 434   INDUCT_TAC THEN REWRITE_TAC[LT_0]);;
 435
 436 let LT_IMP_LE = prove
 437  (`!m n. m < n ==> m <= n`,
 438   REWRITE_TAC[LT_LE] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 439
 440 let EQ_IMP_LE = prove
 441  (`!m n. (m = n) ==> m <= n`,
 442   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[LE_REFL]);;
 443
 444 (* ------------------------------------------------------------------------- *)
 445 (* Often useful to shuffle between different versions of "0 < n".            *)
 446 (* ------------------------------------------------------------------------- *)
 447
 448 let LT_NZ = prove
 449  (`!n. 0 < n <=> ~(n = 0)`,
 450   INDUCT_TAC THEN ASM_REWRITE_TAC[NOT_SUC; LT; EQ_SYM_EQ] THEN
 451   CONV_TAC TAUT);;
 452
 453 let LE_1 = prove
 454  (`(!n. ~(n = 0) ==> 0 < n) /\
 455    (!n. ~(n = 0) ==> 1 <= n) /\
 456    (!n. 0 < n ==> ~(n = 0)) /\
 457    (!n. 0 < n ==> 1 <= n) /\
 458    (!n. 1 <= n ==> 0 < n) /\
 459    (!n. 1 <= n ==> ~(n = 0))`,
 460   REWRITE_TAC[LT_NZ; GSYM NOT_LT; ONE; LT]);;
 461
 462 (* ------------------------------------------------------------------------- *)
 463 (* Relate the orderings to arithmetic operations.                            *)
 464 (* ------------------------------------------------------------------------- *)
 465
 466 let LE_EXISTS = prove
 467  (`!m n. (m <= n) <=> (?d. n = m + d)`,
 468   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LE] THENL
 469    [REWRITE_TAC[CONV_RULE(LAND_CONV SYM_CONV) (SPEC_ALL ADD_EQ_0)] THEN
 470     REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL];
 471     EQ_TAC THENL
 472      [DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC) THENL
 473        [EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES];
 474         DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 475         EXISTS_TAC `SUC d` THEN REWRITE_TAC[ADD_CLAUSES]];
 476       ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 477       INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ] THEN
 478       DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN DISJ2_TAC THEN
 479       REWRITE_TAC[EQ_ADD_LCANCEL; GSYM EXISTS_REFL]]]);;
 480
 481 let LT_EXISTS = prove
 482  (`!m n. (m < n) <=> (?d. n = m + SUC d)`,
 483   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[LT; ADD_CLAUSES; GSYM NOT_SUC] THEN
 484   ASM_REWRITE_TAC[SUC_INJ] THEN EQ_TAC THENL
 485    [DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC) THENL
 486      [EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES];
 487       DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 488       EXISTS_TAC `SUC d` THEN REWRITE_TAC[ADD_CLAUSES]];
 489     ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 490     INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; SUC_INJ] THEN
 491     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN DISJ2_TAC THEN
 492     REWRITE_TAC[SUC_INJ; EQ_ADD_LCANCEL; GSYM EXISTS_REFL]]);;
 493
 494 (* ------------------------------------------------------------------------- *)
 495 (* Interaction with addition.                                                *)
 496 (* ------------------------------------------------------------------------- *)
 497
 498 let LE_ADD = prove
 499  (`!m n. m <= m + n`,
 500   GEN_TAC THEN INDUCT_TAC THEN
 501   ASM_REWRITE_TAC[LE; ADD_CLAUSES; LE_REFL]);;
 502
 503 let LE_ADDR = prove
 504  (`!m n. n <= m + n`,
 505   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC LE_ADD);;
 506
 507 let LT_ADD = prove
 508  (`!m n. (m < m + n) <=> (0 < n)`,
 509   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; LT_SUC]);;
 510
 511 let LT_ADDR = prove
 512  (`!m n. (n < m + n) <=> (0 < m)`,
 513   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC LT_ADD);;
 514
 515 let LE_ADD_LCANCEL = prove
 516  (`!m n p. (m + n) <= (m + p) <=> n <= p`,
 517   REWRITE_TAC[LE_EXISTS; GSYM ADD_ASSOC; EQ_ADD_LCANCEL]);;
 518
 519 let LE_ADD_RCANCEL = prove
 520  (`!m n p. (m + p) <= (n + p) <=> (m <= n)`,
 521   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC LE_ADD_LCANCEL);;
 522
 523 let LT_ADD_LCANCEL = prove
 524  (`!m n p. (m + n) < (m + p) <=> n < p`,
 525   REWRITE_TAC[LT_EXISTS; GSYM ADD_ASSOC; EQ_ADD_LCANCEL; SUC_INJ]);;
 526
 527 let LT_ADD_RCANCEL = prove
 528  (`!m n p. (m + p) < (n + p) <=> (m < n)`,
 529   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC LT_ADD_LCANCEL);;
 530
 531 let LE_ADD2 = prove
 532  (`!m n p q. m <= p /\ n <= q ==> m + n <= p + q`,
 533   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
 534   DISCH_THEN(CONJUNCTS_THEN2
 535     (X_CHOOSE_TAC `a:num`) (X_CHOOSE_TAC `b:num`)) THEN
 536   EXISTS_TAC `a + b` THEN ASM_REWRITE_TAC[ADD_AC]);;
 537
 538 let LET_ADD2 = prove
 539  (`!m n p q. m <= p /\ n < q ==> m + n < p + q`,
 540   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS; LT_EXISTS] THEN
 541   DISCH_THEN(CONJUNCTS_THEN2
 542     (X_CHOOSE_TAC `a:num`) (X_CHOOSE_TAC `b:num`)) THEN
 543   EXISTS_TAC `a + b` THEN ASM_REWRITE_TAC[SUC_INJ; ADD_CLAUSES; ADD_AC]);;
 544
 545 let LTE_ADD2 = prove
 546  (`!m n p q. m < p /\ n <= q ==> m + n < p + q`,
 547   ONCE_REWRITE_TAC[ADD_SYM; CONJ_SYM] THEN
 548   MATCH_ACCEPT_TAC LET_ADD2);;
 549
 550 let LT_ADD2 = prove
 551  (`!m n p q. m < p /\ n < q ==> m + n < p + q`,
 552   REPEAT STRIP_TAC THEN MATCH_MP_TAC LTE_ADD2 THEN
 553   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LT_IMP_LE THEN
 554   ASM_REWRITE_TAC[]);;
 555
 556 (* ------------------------------------------------------------------------- *)
 557 (* And multiplication.                                                       *)
 558 (* ------------------------------------------------------------------------- *)
 559
 560 let LT_MULT = prove
 561  (`!m n. (0 < m * n) <=> (0 < m) /\ (0 < n)`,
 562   REPEAT INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LT_0]);;
 563
 564 let LE_MULT2 = prove
 565  (`!m n p q. m <= n /\ p <= q ==> m * p <= n * q`,
 566   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
 567   DISCH_THEN(CONJUNCTS_THEN2
 568     (X_CHOOSE_TAC `a:num`) (X_CHOOSE_TAC `b:num`)) THEN
 569   EXISTS_TAC `a * p + m * b + a * b` THEN
 570   ASM_REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
 571   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; ADD_ASSOC]);;
 572
 573 let LT_LMULT = prove
 574  (`!m n p. ~(m = 0) /\ n < p ==> m * n < m * p`,
 575   REPEAT GEN_TAC THEN REWRITE_TAC[LT_LE] THEN STRIP_TAC THEN CONJ_TAC THENL
 576    [MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[LE_REFL];
 577     ASM_REWRITE_TAC[EQ_MULT_LCANCEL]]);;
 578
 579 let LE_MULT_LCANCEL = prove
 580  (`!m n p. (m * n) <= (m * p) <=> (m = 0) \/ n <= p`,
 581   REPEAT INDUCT_TAC THEN
 582   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE_REFL; LE_0; NOT_SUC] THEN
 583   REWRITE_TAC[LE_SUC] THEN
 584   REWRITE_TAC[LE; LE_ADD_LCANCEL; GSYM ADD_ASSOC] THEN
 585   ASM_REWRITE_TAC[GSYM(el 4(CONJUNCTS MULT_CLAUSES)); NOT_SUC]);;
 586
 587 let LE_MULT_RCANCEL = prove
 588  (`!m n p. (m * p) <= (n * p) <=> (m <= n) \/ (p = 0)`,
 589   ONCE_REWRITE_TAC[MULT_SYM; DISJ_SYM] THEN
 590   MATCH_ACCEPT_TAC LE_MULT_LCANCEL);;
 591
 592 let LT_MULT_LCANCEL = prove
 593  (`!m n p. (m * n) < (m * p) <=> ~(m = 0) /\ n < p`,
 594   REPEAT INDUCT_TAC THEN
 595   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LT_REFL; LT_0; NOT_SUC] THEN
 596   REWRITE_TAC[LT_SUC] THEN
 597   REWRITE_TAC[LT; LT_ADD_LCANCEL; GSYM ADD_ASSOC] THEN
 598   ASM_REWRITE_TAC[GSYM(el 4(CONJUNCTS MULT_CLAUSES)); NOT_SUC]);;
 599
 600 let LT_MULT_RCANCEL = prove
 601  (`!m n p. (m * p) < (n * p) <=> (m < n) /\ ~(p = 0)`,
 602   ONCE_REWRITE_TAC[MULT_SYM; CONJ_SYM] THEN
 603   MATCH_ACCEPT_TAC LT_MULT_LCANCEL);;
 604
 605 let LT_MULT2 = prove
 606  (`!m n p q. m < n /\ p < q ==> m * p < n * q`,
 607   REPEAT STRIP_TAC THEN MATCH_MP_TAC LET_TRANS THEN
 608   EXISTS_TAC `n * p` THEN
 609   ASM_SIMP_TAC[LE_MULT_RCANCEL; LT_IMP_LE; LT_MULT_LCANCEL] THEN
 610   UNDISCH_TAC `m < n` THEN CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC[LT]);;
 611
 612 let LE_SQUARE_REFL = prove
 613  (`!n. n <= n * n`,
 614   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; LE_0; LE_ADDR]);;
 615
 616 let LT_POW2_REFL = prove
 617  (`!n. n < 2 EXP n`,
 618   INDUCT_TAC THEN REWRITE_TAC[EXP] THEN REWRITE_TAC[MULT_2; ADD1] THEN
 619   REWRITE_TAC[ONE; LT] THEN MATCH_MP_TAC LTE_ADD2 THEN
 620   ASM_REWRITE_TAC[LE_SUC_LT; TWO] THEN
 621   MESON_TAC[EXP_EQ_0; LE_1; NOT_SUC]);;
 622
 623 (* ------------------------------------------------------------------------- *)
 624 (* Useful "without loss of generality" lemmas.                               *)
 625 (* ------------------------------------------------------------------------- *)
 626
 627 let WLOG_LE = prove
 628  (`(!m n. P m n <=> P n m) /\ (!m n. m <= n ==> P m n) ==> !m n. P m n`,
 629   MESON_TAC[LE_CASES]);;
 630
 631 let WLOG_LT = prove
 632  (`(!m. P m m) /\ (!m n. P m n <=> P n m) /\ (!m n. m < n ==> P m n)
 633    ==> !m y. P m y`,
 634   MESON_TAC[LT_CASES]);;
 635
 636 (* ------------------------------------------------------------------------- *)
 637 (* Existence of least and greatest elements of (finite) set.                 *)
 638 (* ------------------------------------------------------------------------- *)
 639
 640 let num_WF = prove
 641  (`!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n`,
 642   GEN_TAC THEN MP_TAC(SPEC `\n. !m. m < n ==> P m` num_INDUCTION) THEN
 643   REWRITE_TAC[LT; BETA_THM] THEN MESON_TAC[LT]);;
 644
 645 let num_WOP = prove
 646  (`!P. (?n. P n) <=> (?n. P(n) /\ !m. m < n ==> ~P(m))`,
 647   GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 648   CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
 649   DISCH_TAC THEN MATCH_MP_TAC num_WF THEN ASM_MESON_TAC[]);;
 650
 651 let num_MAX = prove
 652  (`!P. (?x. P x) /\ (?M. !x. P x ==> x <= M) <=>
 653        ?m. P m /\ (!x. P x ==> x <= m)`,
 654   GEN_TAC THEN EQ_TAC THENL
 655    [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:num`) MP_TAC) THEN
 656     DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC o ONCE_REWRITE_RULE[num_WOP]) THEN
 657     DISCH_THEN(fun th -> EXISTS_TAC `m:num` THEN MP_TAC th) THEN
 658     REWRITE_TAC[TAUT `(a /\ b ==> c /\ a) <=> (a /\ b ==> c)`] THEN
 659     SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THENL
 660      [REWRITE_TAC[LE; LT] THEN DISCH_THEN(IMP_RES_THEN SUBST_ALL_TAC) THEN
 661       POP_ASSUM ACCEPT_TAC;
 662       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `m:num`)) THEN
 663       REWRITE_TAC[LT] THEN CONV_TAC CONTRAPOS_CONV THEN
 664       DISCH_TAC THEN REWRITE_TAC[] THEN X_GEN_TAC `p:num` THEN
 665       FIRST_ASSUM(MP_TAC o SPEC `p:num`) THEN REWRITE_TAC[LE] THEN
 666       ASM_CASES_TAC `p = SUC m` THEN ASM_REWRITE_TAC[]];
 667     REPEAT STRIP_TAC THEN EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[]]);;
 668
 669 (* ------------------------------------------------------------------------- *)
 670 (* Oddness and evenness (recursively rather than inductively!)               *)
 671 (* ------------------------------------------------------------------------- *)
 672
 673 let EVEN = new_recursive_definition num_RECURSION
 674   `(EVEN 0 <=> T) /\
 675    (!n. EVEN (SUC n) <=> ~(EVEN n))`;;
 676
 677 let ODD = new_recursive_definition num_RECURSION
 678   `(ODD 0 <=> F) /\
 679    (!n. ODD (SUC n) <=> ~(ODD n))`;;
 680
 681 let NOT_EVEN = prove
 682  (`!n. ~(EVEN n) <=> ODD n`,
 683   INDUCT_TAC THEN ASM_REWRITE_TAC[EVEN; ODD]);;
 684
 685 let NOT_ODD = prove
 686  (`!n. ~(ODD n) <=> EVEN n`,
 687   INDUCT_TAC THEN ASM_REWRITE_TAC[EVEN; ODD]);;
 688
 689 let EVEN_OR_ODD = prove
 690  (`!n. EVEN n \/ ODD n`,
 691   INDUCT_TAC THEN REWRITE_TAC[EVEN; ODD; NOT_EVEN; NOT_ODD] THEN
 692   ONCE_REWRITE_TAC[DISJ_SYM] THEN ASM_REWRITE_TAC[]);;
 693
 694 let EVEN_AND_ODD = prove
 695  (`!n. ~(EVEN n /\ ODD n)`,
 696   REWRITE_TAC[GSYM NOT_EVEN; ITAUT `~(p /\ ~p)`]);;
 697
 698 let EVEN_ADD = prove
 699  (`!m n. EVEN(m + n) <=> (EVEN m <=> EVEN n)`,
 700   INDUCT_TAC THEN ASM_REWRITE_TAC[EVEN; ADD_CLAUSES] THEN
 701   X_GEN_TAC `p:num` THEN
 702   DISJ_CASES_THEN MP_TAC (SPEC `n:num` EVEN_OR_ODD) THEN
 703   DISJ_CASES_THEN MP_TAC (SPEC `p:num` EVEN_OR_ODD) THEN
 704   REWRITE_TAC[GSYM NOT_EVEN] THEN DISCH_TAC THEN
 705   ASM_REWRITE_TAC[]);;
 706
 707 let EVEN_MULT = prove
 708  (`!m n. EVEN(m * n) <=> EVEN(m) \/ EVEN(n)`,
 709   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; EVEN_ADD; EVEN] THEN
 710   X_GEN_TAC `p:num` THEN
 711   DISJ_CASES_THEN MP_TAC (SPEC `n:num` EVEN_OR_ODD) THEN
 712   DISJ_CASES_THEN MP_TAC (SPEC `p:num` EVEN_OR_ODD) THEN
 713   REWRITE_TAC[GSYM NOT_EVEN] THEN DISCH_TAC THEN
 714   ASM_REWRITE_TAC[]);;
 715
 716 let EVEN_EXP = prove
 717  (`!m n. EVEN(m EXP n) <=> EVEN(m) /\ ~(n = 0)`,
 718   GEN_TAC THEN INDUCT_TAC THEN
 719   ASM_REWRITE_TAC[EVEN; EXP; ONE; EVEN_MULT; NOT_SUC] THEN
 720   CONV_TAC ITAUT);;
 721
 722 let ODD_ADD = prove
 723  (`!m n. ODD(m + n) <=> ~(ODD m <=> ODD n)`,
 724   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_EVEN; EVEN_ADD] THEN
 725   CONV_TAC ITAUT);;
 726
 727 let ODD_MULT = prove
 728  (`!m n. ODD(m * n) <=> ODD(m) /\ ODD(n)`,
 729   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_EVEN; EVEN_MULT] THEN
 730   CONV_TAC ITAUT);;
 731
 732 let ODD_EXP = prove
 733  (`!m n. ODD(m EXP n) <=> ODD(m) \/ (n = 0)`,
 734   GEN_TAC THEN INDUCT_TAC THEN
 735   ASM_REWRITE_TAC[ODD; EXP; ONE; ODD_MULT; NOT_SUC] THEN
 736   CONV_TAC ITAUT);;
 737
 738 let EVEN_DOUBLE = prove
 739  (`!n. EVEN(2 * n)`,
 740   GEN_TAC THEN REWRITE_TAC[EVEN_MULT] THEN DISJ1_TAC THEN
 741   PURE_REWRITE_TAC[BIT0_THM; BIT1_THM] THEN REWRITE_TAC[EVEN; EVEN_ADD]);;
 742
 743 let ODD_DOUBLE = prove
 744  (`!n. ODD(SUC(2 * n))`,
 745   REWRITE_TAC[ODD] THEN REWRITE_TAC[NOT_ODD; EVEN_DOUBLE]);;
 746
 747 let EVEN_EXISTS_LEMMA = prove
 748  (`!n. (EVEN n ==> ?m. n = 2 * m) /\
 749        (~EVEN n ==> ?m. n = SUC(2 * m))`,
 750   INDUCT_TAC THEN REWRITE_TAC[EVEN] THENL
 751    [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES];
 752     POP_ASSUM STRIP_ASSUME_TAC THEN CONJ_TAC THEN
 753     DISCH_THEN(ANTE_RES_THEN(X_CHOOSE_TAC `m:num`)) THENL
 754      [EXISTS_TAC `SUC m` THEN ASM_REWRITE_TAC[] THEN
 755       REWRITE_TAC[MULT_2] THEN REWRITE_TAC[ADD_CLAUSES];
 756       EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[]]]);;
 757
 758 let EVEN_EXISTS = prove
 759  (`!n. EVEN n <=> ?m. n = 2 * m`,
 760   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 761    [MATCH_MP_TAC(CONJUNCT1(SPEC_ALL EVEN_EXISTS_LEMMA)) THEN ASM_REWRITE_TAC[];
 762     POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[EVEN_DOUBLE]]);;
 763
 764 let ODD_EXISTS = prove
 765  (`!n. ODD n <=> ?m. n = SUC(2 * m)`,
 766   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 767    [MATCH_MP_TAC(CONJUNCT2(SPEC_ALL EVEN_EXISTS_LEMMA)) THEN
 768     ASM_REWRITE_TAC[NOT_EVEN];
 769     POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[ODD_DOUBLE]]);;
 770
 771 let EVEN_ODD_DECOMPOSITION = prove
 772  (`!n. (?k m. ODD m /\ (n = 2 EXP k * m)) <=> ~(n = 0)`,
 773   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 774   DISJ_CASES_TAC(SPEC `n:num` EVEN_OR_ODD) THENL
 775    [ALL_TAC; ASM_MESON_TAC[ODD; EXP; MULT_CLAUSES]] THEN
 776   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
 777   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
 778   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
 779   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_EQ_0] THENL
 780    [REWRITE_TAC[MULT_CLAUSES; LT] THEN
 781     CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
 782     REWRITE_TAC[EXP_EQ_0; MULT_EQ_0; TWO; NOT_SUC] THEN MESON_TAC[ODD];
 783     ALL_TAC] THEN
 784   ANTS_TAC THENL
 785    [GEN_REWRITE_TAC LAND_CONV [GSYM(el 2 (CONJUNCTS MULT_CLAUSES))] THEN
 786     ASM_REWRITE_TAC[LT_MULT_RCANCEL; TWO; LT];
 787     ALL_TAC] THEN
 788   REWRITE_TAC[TWO; NOT_SUC] THEN REWRITE_TAC[GSYM TWO] THEN
 789   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 790   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `p:num` THEN
 791   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 792   EXISTS_TAC `SUC k` THEN ASM_REWRITE_TAC[EXP; MULT_ASSOC]);;
 793
 794 (* ------------------------------------------------------------------------- *)
 795 (* Cutoff subtraction, also defined recursively. (Not the HOL88 defn.)       *)
 796 (* ------------------------------------------------------------------------- *)
 797
 798 let SUB = new_recursive_definition num_RECURSION
 799  `(!m. m - 0 = m) /\
 800   (!m n. m - (SUC n) = PRE(m - n))`;;
 801
 802 let SUB_0 = prove
 803  (`!m. (0 - m = 0) /\ (m - 0 = m)`,
 804   REWRITE_TAC[SUB] THEN INDUCT_TAC THEN ASM_REWRITE_TAC[SUB; PRE]);;
 805
 806 let SUB_PRESUC = prove
 807  (`!m n. PRE(SUC m - n) = m - n`,
 808   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[SUB; PRE]);;
 809
 810 let SUB_SUC = prove
 811  (`!m n. SUC m - SUC n = m - n`,
 812   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[SUB; PRE; SUB_PRESUC]);;
 813
 814 let SUB_REFL = prove
 815  (`!n. n - n = 0`,
 816   INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_SUC; SUB_0]);;
 817
 818 let ADD_SUB = prove
 819  (`!m n. (m + n) - n = m`,
 820   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; SUB_SUC; SUB_0]);;
 821
 822 let ADD_SUB2 = prove
 823  (`!m n. (m + n) - m = n`,
 824   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC ADD_SUB);;
 825
 826 let SUB_EQ_0 = prove
 827  (`!m n. (m - n = 0) <=> m <= n`,
 828   REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_SUC; LE_SUC; SUB_0] THEN
 829   REWRITE_TAC[LE; LE_0]);;
 830
 831 let ADD_SUBR2 = prove
 832  (`!m n. m - (m + n) = 0`,
 833   REWRITE_TAC[SUB_EQ_0; LE_ADD]);;
 834
 835 let ADD_SUBR = prove
 836  (`!m n. n - (m + n) = 0`,
 837   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC ADD_SUBR2);;
 838
 839 let SUB_ADD = prove
 840  (`!m n. n <= m ==> ((m - n) + n = m)`,
 841   REWRITE_TAC[LE_EXISTS] THEN REPEAT STRIP_TAC THEN
 842   ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
 843   MATCH_ACCEPT_TAC ADD_SYM);;
 844
 845 let SUB_ADD_LCANCEL = prove
 846  (`!m n p. (m + n) - (m + p) = n - p`,
 847   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; SUB_0; SUB_SUC]);;
 848
 849 let SUB_ADD_RCANCEL = prove
 850  (`!m n p. (m + p) - (n + p) = m - n`,
 851   ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC SUB_ADD_LCANCEL);;
 852
 853 let LEFT_SUB_DISTRIB = prove
 854  (`!m n p. m * (n - p) = m * n - m * p`,
 855   REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
 856   DISJ_CASES_TAC(SPECL [`n:num`; `p:num`] LE_CASES) THENL
 857    [FIRST_ASSUM(fun th -> REWRITE_TAC[REWRITE_RULE[GSYM SUB_EQ_0] th]) THEN
 858     ASM_REWRITE_TAC[MULT_CLAUSES; SUB_EQ_0; LE_MULT_LCANCEL];
 859     POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 860     REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
 861     REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB]]);;
 862
 863 let RIGHT_SUB_DISTRIB = prove
 864  (`!m n p. (m - n) * p = m * p - n * p`,
 865   ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_ACCEPT_TAC LEFT_SUB_DISTRIB);;
 866
 867 let SUC_SUB1 = prove
 868  (`!n. SUC n - 1 = n`,
 869   REWRITE_TAC[ONE; SUB_SUC; SUB_0]);;
 870
 871 let EVEN_SUB = prove
 872  (`!m n. EVEN(m - n) <=> m <= n \/ (EVEN(m) <=> EVEN(n))`,
 873   REPEAT GEN_TAC THEN ASM_CASES_TAC `m <= n:num` THENL
 874    [ASM_MESON_TAC[SUB_EQ_0; EVEN]; ALL_TAC] THEN
 875   DISJ_CASES_TAC(SPECL [`m:num`; `n:num`] LE_CASES) THEN ASM_SIMP_TAC[] THEN
 876   FIRST_ASSUM(MP_TAC o AP_TERM `EVEN` o MATCH_MP SUB_ADD) THEN
 877   ASM_MESON_TAC[EVEN_ADD]);;
 878
 879 let ODD_SUB = prove
 880  (`!m n. ODD(m - n) <=> n < m /\ ~(ODD m <=> ODD n)`,
 881   REWRITE_TAC[GSYM NOT_EVEN; EVEN_SUB; DE_MORGAN_THM; NOT_LE] THEN
 882   CONV_TAC TAUT);;
 883
 884 (* ------------------------------------------------------------------------- *)
 885 (* The factorial function.                                                   *)
 886 (* ------------------------------------------------------------------------- *)
 887
 888 let FACT = new_recursive_definition num_RECURSION
 889   `(FACT 0 = 1) /\
 890    (!n. FACT (SUC n) = (SUC n) * FACT(n))`;;
 891
 892 let FACT_LT = prove
 893  (`!n. 0 < FACT n`,
 894   INDUCT_TAC THEN ASM_REWRITE_TAC[FACT; LT_MULT] THEN
 895   REWRITE_TAC[ONE; LT_0]);;
 896
 897 let FACT_LE = prove
 898  (`!n. 1 <= FACT n`,
 899   REWRITE_TAC[ONE; LE_SUC_LT; FACT_LT]);;
 900
 901 let FACT_NZ = prove
 902  (`!n. ~(FACT n = 0)`,
 903   REWRITE_TAC[GSYM LT_NZ; FACT_LT]);;
 904
 905 let FACT_MONO = prove
 906  (`!m n. m <= n ==> FACT m <= FACT n`,
 907   REPEAT GEN_TAC THEN
 908   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 909   SPEC_TAC(`d:num`,`d:num`) THEN
 910   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
 911   REWRITE_TAC[FACT] THEN
 912   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `FACT(m + d)` THEN
 913   ASM_REWRITE_TAC[] THEN
 914   GEN_REWRITE_TAC LAND_CONV [GSYM(el 2 (CONJUNCTS MULT_CLAUSES))] THEN
 915   REWRITE_TAC[LE_MULT_RCANCEL] THEN
 916   REWRITE_TAC[ONE; LE_SUC; LE_0]);;
 917
 918 (* ------------------------------------------------------------------------- *)
 919 (* More complicated theorems about exponential.                              *)
 920 (* ------------------------------------------------------------------------- *)
 921
 922 let EXP_LT_0 = prove
 923  (`!n x. 0 < x EXP n <=> ~(x = 0) \/ (n = 0)`,
 924   REWRITE_TAC[GSYM NOT_LE; LE; EXP_EQ_0; DE_MORGAN_THM]);;
 925
 926 let LT_EXP = prove
 927  (`!x m n. x EXP m < x EXP n <=> 2 <= x /\ m < n \/
 928                                  (x = 0) /\ ~(m = 0) /\ (n = 0)`,
 929   REPEAT GEN_TAC THEN
 930   ASM_CASES_TAC `x = 0` THEN ASM_REWRITE_TAC[] THENL
 931    [REWRITE_TAC[GSYM NOT_LT; TWO; ONE; LT] THEN
 932     SPEC_TAC (`n:num`,`n:num`) THEN INDUCT_TAC THEN
 933     REWRITE_TAC[EXP; NOT_SUC; MULT_CLAUSES; LT] THEN
 934     SPEC_TAC (`m:num`,`m:num`) THEN INDUCT_TAC THEN
 935     REWRITE_TAC[EXP; MULT_CLAUSES; NOT_SUC; LT_REFL; LT] THEN
 936     REWRITE_TAC[ONE; LT_0]; ALL_TAC] THEN
 937   EQ_TAC THENL
 938    [CONV_TAC CONTRAPOS_CONV THEN
 939     REWRITE_TAC[NOT_LT; DE_MORGAN_THM; NOT_LE] THEN
 940     REWRITE_TAC[TWO; ONE; LT] THEN
 941     ASM_REWRITE_TAC[SYM ONE] THEN
 942     STRIP_TAC THEN ASM_REWRITE_TAC[EXP_ONE; LE_REFL] THEN
 943     FIRST_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o
 944       REWRITE_RULE[LE_EXISTS]) THEN
 945     SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
 946     REWRITE_TAC[ADD_CLAUSES; EXP; LE_REFL] THEN
 947     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `1 * x EXP (n + d)` THEN
 948     CONJ_TAC THENL
 949      [ASM_REWRITE_TAC[MULT_CLAUSES];
 950       REWRITE_TAC[LE_MULT_RCANCEL] THEN
 951       DISJ1_TAC THEN UNDISCH_TAC `~(x = 0)` THEN
 952       CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
 953       REWRITE_TAC[ONE; LT]];
 954     STRIP_TAC THEN
 955     FIRST_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o
 956       REWRITE_RULE[LT_EXISTS]) THEN
 957     SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
 958     REWRITE_TAC[ADD_CLAUSES; EXP] THENL
 959      [MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `2 * x EXP m` THEN
 960       CONJ_TAC THENL
 961        [ASM_REWRITE_TAC[MULT_2; LT_ADD; EXP_LT_0];
 962         ASM_REWRITE_TAC[LE_MULT_RCANCEL]];
 963       MATCH_MP_TAC LTE_TRANS THEN
 964       EXISTS_TAC `x EXP (m + SUC d)` THEN ASM_REWRITE_TAC[] THEN
 965       REWRITE_TAC[ADD_CLAUSES; EXP; MULT_ASSOC; LE_MULT_RCANCEL] THEN
 966       DISJ1_TAC THEN MATCH_MP_TAC LE_TRANS THEN
 967       EXISTS_TAC `x * 1` THEN CONJ_TAC THENL
 968        [REWRITE_TAC[MULT_CLAUSES; LE_REFL];
 969         REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
 970         UNDISCH_TAC `~(x = 0)` THEN
 971         CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
 972         REWRITE_TAC[ONE; LT]]]]);;
 973
 974 let LE_EXP = prove
 975  (`!x m n. x EXP m <= x EXP n <=>
 976            if x = 0 then (m = 0) ==> (n = 0)
 977            else (x = 1) \/ m <= n`,
 978   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_LT; LT_EXP; DE_MORGAN_THM] THEN
 979   COND_CASES_TAC THEN ASM_REWRITE_TAC[TWO; LT; ONE] THEN
 980   CONV_TAC(EQT_INTRO o TAUT));;
 981
 982 let EQ_EXP = prove
 983  (`!x m n. x EXP m = x EXP n <=>
 984            if x = 0 then (m = 0 <=> n = 0)
 985            else (x = 1) \/ m = n`,
 986   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM LE_ANTISYM; LE_EXP] THEN
 987   COND_CASES_TAC THEN ASM_REWRITE_TAC[LE_EXP] THEN
 988   REWRITE_TAC[GSYM LE_ANTISYM] THEN CONV_TAC TAUT);;
 989
 990 let EXP_MONO_LE_IMP = prove
 991  (`!x y n. x <= y ==> x EXP n <= y EXP n`,
 992   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
 993   REPEAT GEN_TAC THEN DISCH_TAC THEN
 994   INDUCT_TAC THEN ASM_SIMP_TAC[LE_MULT2; EXP; LE_REFL]);;
 995
 996 let EXP_MONO_LT_IMP = prove
 997  (`!x y n. x < y /\ ~(n = 0) ==> x EXP n < y EXP n`,
 998   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; EXP] THEN
 999   DISCH_TAC THEN MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `x * y EXP n` THEN
1000   ASM_SIMP_TAC[LT_IMP_LE; LE_MULT_LCANCEL; LT_MULT_RCANCEL; EXP_MONO_LE_IMP;
1001                EXP_EQ_0] THEN
1002   ASM_MESON_TAC[CONJUNCT1 LT]);;
1003
1004 let EXP_MONO_LE = prove
1005  (`!x y n. x EXP n <= y EXP n <=> x <= y \/ n = 0`,
1006   REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
1007   ASM_SIMP_TAC[EXP; LE_REFL; EXP_MONO_LE_IMP] THEN
1008   ASM_MESON_TAC[NOT_LE; EXP_MONO_LT_IMP]);;
1009
1010 let EXP_MONO_LT = prove
1011  (`!x y n. x EXP n < y EXP n <=> x < y /\ ~(n = 0)`,
1012   REWRITE_TAC[GSYM NOT_LE; EXP_MONO_LE; DE_MORGAN_THM]);;
1013
1014 let EXP_MONO_EQ = prove
1015  (`!x y n. x EXP n = y EXP n <=> x = y \/ n = 0`,
1016   REWRITE_TAC[GSYM LE_ANTISYM; EXP_MONO_LE] THEN CONV_TAC TAUT);;
1017
1018 (* ------------------------------------------------------------------------- *)
1019 (* Division and modulus, via existence proof of their basic property.        *)
1020 (* ------------------------------------------------------------------------- *)
1021
1022 let DIVMOD_EXIST = prove
1023  (`!m n. ~(n = 0) ==> ?q r. (m = q * n + r) /\ r < n`,
1024   REPEAT STRIP_TAC THEN MP_TAC(SPEC `\r. ?q. m = q * n + r` num_WOP) THEN
1025   BETA_TAC THEN DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN
1026   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
1027   DISCH_THEN(MP_TAC o SPECL [`m:num`; `0`]) THEN
1028   REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1029   DISCH_THEN(X_CHOOSE_THEN `r:num` MP_TAC) THEN
1030   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `q:num`) MP_TAC) THEN
1031   DISCH_THEN(fun th ->
1032     MAP_EVERY EXISTS_TAC [`q:num`; `r:num`] THEN MP_TAC th) THEN
1033   CONV_TAC CONTRAPOS_CONV THEN ASM_REWRITE_TAC[NOT_LT] THEN
1034   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC o
1035     REWRITE_RULE[LE_EXISTS]) THEN
1036   REWRITE_TAC[NOT_FORALL_THM] THEN EXISTS_TAC `d:num` THEN
1037   REWRITE_TAC[NOT_IMP; RIGHT_AND_EXISTS_THM] THEN
1038   EXISTS_TAC `q + 1` THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1039   REWRITE_TAC[MULT_CLAUSES; ADD_ASSOC; LT_ADDR] THEN
1040   ASM_REWRITE_TAC[GSYM NOT_LE; LE]);;
1041
1042 let DIVMOD_EXIST_0 = prove
1043  (`!m n. ?q r. if n = 0 then q = 0 /\ r = m
1044                else m = q * n + r /\ r < n`,
1045   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1046   ASM_SIMP_TAC[DIVMOD_EXIST; RIGHT_EXISTS_AND_THM; EXISTS_REFL]);;
1047
1048 let DIVISION_0 =  new_specification ["DIV"; "MOD"]
1049   (REWRITE_RULE[SKOLEM_THM] DIVMOD_EXIST_0);;
1050
1051 let DIVISION = prove
1052  (`!m n. ~(n = 0) ==> (m = m DIV n * n + m MOD n) /\ m MOD n < n`,
1053   MESON_TAC[DIVISION_0]);;
1054
1055 let DIVISION_SIMP = prove
1056  (`(!m n. ~(n = 0) ==> m DIV n * n + m MOD n = m) /\
1057    (!m n. ~(n = 0) ==> n * m DIV n + m MOD n = m)`,
1058   MESON_TAC[DIVISION; MULT_SYM]);;
1059
1060 let DIVMOD_UNIQ_LEMMA = prove
1061  (`!m n q1 r1 q2 r2. ((m = q1 * n + r1) /\ r1 < n) /\
1062                      ((m = q2 * n + r2) /\ r2 < n)
1063                      ==> (q1 = q2) /\ (r1 = r2)`,
1064   REPEAT GEN_TAC THEN STRIP_TAC THEN
1065   SUBGOAL_THEN `r1:num = r2` MP_TAC THENL
1066    [UNDISCH_TAC `m = q2 * n + r2` THEN
1067     ASM_REWRITE_TAC[] THEN
1068     DISJ_CASES_THEN MP_TAC (SPECL [`q1:num`; `q2:num`] LE_CASES) THEN
1069     DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
1070     REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; EQ_ADD_LCANCEL] THENL
1071      [DISCH_TAC THEN UNDISCH_TAC `r1 < n`;
1072       DISCH_THEN(ASSUME_TAC o SYM) THEN UNDISCH_TAC `r2 < n`] THEN
1073     ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
1074     SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
1075     REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES;
1076       GSYM NOT_LE; LE_ADD; GSYM ADD_ASSOC];
1077     DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[] THEN
1078     CONV_TAC SYM_CONV THEN
1079     UNDISCH_TAC `m = q1 * n + r2` THEN
1080     ASM_REWRITE_TAC[EQ_ADD_RCANCEL; EQ_MULT_RCANCEL] THEN
1081     REPEAT (UNDISCH_TAC `r2 < n`) THEN
1082     ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[GSYM NOT_LE; LE_0]]);;
1083
1084 let DIVMOD_UNIQ = prove
1085  (`!m n q r. (m = q * n + r) /\ r < n ==> (m DIV n = q) /\ (m MOD n = r)`,
1086   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC o GSYM) THEN
1087   MATCH_MP_TAC DIVMOD_UNIQ_LEMMA THEN
1088   MAP_EVERY EXISTS_TAC [`m:num`; `n:num`] THEN ASM_REWRITE_TAC[] THEN
1089   MATCH_MP_TAC DIVISION THEN
1090   DISCH_TAC THEN UNDISCH_TAC `r < n` THEN
1091   ASM_REWRITE_TAC[GSYM NOT_LE; LE_0]);;
1092
1093 let MOD_UNIQ = prove
1094  (`!m n q r. (m = q * n + r) /\ r < n ==> (m MOD n = r)`,
1095   REPEAT GEN_TAC THEN
1096   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP DIVMOD_UNIQ th]));;
1097
1098 let DIV_UNIQ = prove
1099  (`!m n q r. (m = q * n + r) /\ r < n ==> (m DIV n = q)`,
1100   REPEAT GEN_TAC THEN
1101   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP DIVMOD_UNIQ th]));;
1102
1103 let DIV_MULT,MOD_MULT = (CONJ_PAIR o prove)
1104  (`(!m n. ~(m = 0) ==> (m * n) DIV m = n) /\
1105    (!m n. ~(m = 0) ==> (m * n) MOD m = 0)`,
1106   SIMP_TAC[AND_FORALL_THM; TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
1107   REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC DIVMOD_UNIQ THEN
1108   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; MULT_AC; LT_NZ]);;
1109
1110 let MOD_LT = prove
1111  (`!m n. m < n ==> (m MOD n = m)`,
1112   REPEAT STRIP_TAC THEN MATCH_MP_TAC MOD_UNIQ THEN
1113   EXISTS_TAC `0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]);;
1114
1115 let MOD_EQ = prove
1116  (`!m n p q. (m = n + q * p) ==> (m MOD p = n MOD p)`,
1117   REPEAT GEN_TAC THEN ASM_CASES_TAC `p = 0` THENL
1118    [ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1119     DISCH_THEN SUBST1_TAC THEN REFL_TAC;
1120     DISCH_THEN SUBST1_TAC THEN
1121     MATCH_MP_TAC MOD_UNIQ THEN
1122     EXISTS_TAC `q + n DIV p` THEN
1123     POP_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
1124     DISCH_THEN(STRIP_ASSUME_TAC o GSYM o SPEC `n:num`) THEN
1125     ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC] THEN
1126     MATCH_ACCEPT_TAC ADD_SYM]);;
1127
1128 let DIV_LE = prove
1129  (`!m n. ~(n = 0) ==> m DIV n <= m`,
1130   REPEAT STRIP_TAC THEN
1131   FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [MATCH_MP DIVISION th]) THEN
1132   UNDISCH_TAC `~(n = 0)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
1133   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; GSYM ADD_ASSOC; LE_ADD]);;
1134
1135 let DIV_MUL_LE = prove
1136  (`!m n. n * (m DIV n) <= m`,
1137   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1138   ASM_REWRITE_TAC[MULT_CLAUSES; LE_0] THEN
1139   POP_ASSUM(MP_TAC o SPEC `m:num` o MATCH_MP DIVISION) THEN
1140   DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [CONJUNCT1 th]) THEN
1141   REWRITE_TAC[LE_ADD; MULT_AC]);;
1142
1143 let DIV_0,MOD_0 = (CONJ_PAIR o prove)
1144  (`(!n. ~(n = 0) ==> 0 DIV n = 0) /\
1145    (!n. ~(n = 0) ==> 0 MOD n = 0)`,
1146   SIMP_TAC[AND_FORALL_THM; TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
1147   GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC DIVMOD_UNIQ THEN
1148   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LT_NZ]);;
1149
1150 let DIV_1,MOD_1 = (CONJ_PAIR o prove)
1151  (`(!n. n DIV 1 = n) /\ (!n. n MOD 1 = 0)`,
1152   SIMP_TAC[AND_FORALL_THM] THEN GEN_TAC THEN MATCH_MP_TAC DIVMOD_UNIQ THEN
1153   REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN REWRITE_TAC[ONE; LT]);;
1154
1155 let DIV_LT = prove
1156  (`!m n. m < n ==> (m DIV n = 0)`,
1157   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `m:num` THEN
1158   ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]);;
1159
1160 let MOD_MOD = prove
1161  (`!m n p. ~(n * p = 0) ==> ((m MOD (n * p)) MOD n = m MOD n)`,
1162   REPEAT GEN_TAC THEN REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
1163   CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN
1164   EXISTS_TAC `m DIV (n * p) * p` THEN
1165   MP_TAC(SPECL [`m:num`; `n * p:num`] DIVISION) THEN
1166   ASM_REWRITE_TAC[MULT_EQ_0; MULT_AC; ADD_AC] THEN
1167   DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]));;
1168
1169 let MOD_MOD_REFL = prove
1170  (`!m n. ~(n = 0) ==> ((m MOD n) MOD n = m MOD n)`,
1171   REPEAT GEN_TAC THEN DISCH_TAC THEN
1172   MP_TAC(SPECL [`m:num`; `n:num`; `1`] MOD_MOD) THEN
1173   ASM_REWRITE_TAC[MULT_CLAUSES; MULT_EQ_0] THEN
1174   REWRITE_TAC[ONE; NOT_SUC]);;
1175
1176 let DIV_MULT2 = prove
1177  (`!m n p. ~(m * p = 0) ==> ((m * n) DIV (m * p) = n DIV p)`,
1178   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN
1179   MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `m * (n MOD p)` THEN
1180   ASM_SIMP_TAC[LT_MULT_LCANCEL; DIVISION] THEN
1181   ONCE_REWRITE_TAC[AC MULT_AC `a * b * c:num = b * a * c`] THEN
1182   REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; EQ_MULT_LCANCEL] THEN
1183   ASM_SIMP_TAC[GSYM DIVISION]);;
1184
1185 let MOD_MULT2 = prove
1186  (`!m n p. ~(m * p = 0) ==> ((m * n) MOD (m * p) = m * n MOD p)`,
1187   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN
1188   MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `n DIV p` THEN
1189   ASM_SIMP_TAC[LT_MULT_LCANCEL; DIVISION] THEN
1190   ONCE_REWRITE_TAC[AC MULT_AC `a * b * c:num = b * a * c`] THEN
1191   REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; EQ_MULT_LCANCEL] THEN
1192   ASM_SIMP_TAC[GSYM DIVISION]);;
1193
1194 let MOD_EXISTS = prove
1195  (`!m n. (?q. m = n * q) <=> if n = 0 then (m = 0) else (m MOD n = 0)`,
1196   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1197   EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[MOD_MULT] THEN
1198   EXISTS_TAC `m DIV n` THEN
1199   SUBGOAL_THEN `m = (m DIV n) * n + m MOD n`
1200    (fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THENL
1201    [ASM_MESON_TAC[DIVISION]; ASM_REWRITE_TAC[ADD_CLAUSES; MULT_AC]]);;
1202
1203 let LE_RDIV_EQ = prove
1204  (`!a b n. ~(a = 0) ==> (n <= b DIV a <=> a * n <= b)`,
1205   REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL
1206    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `a * (b DIV a)` THEN
1207     ASM_REWRITE_TAC[DIV_MUL_LE; LE_MULT_LCANCEL];
1208     SUBGOAL_THEN `a * n < a * (b DIV a + 1)` MP_TAC THENL
1209      [MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `(b DIV a) * a + b MOD a` THEN
1210       CONJ_TAC THENL [ASM_MESON_TAC[DIVISION]; ALL_TAC] THEN
1211       SIMP_TAC[LEFT_ADD_DISTRIB; MULT_SYM; MULT_CLAUSES; LT_ADD_LCANCEL] THEN
1212       ASM_MESON_TAC[DIVISION];
1213       ASM_REWRITE_TAC[LT_MULT_LCANCEL; GSYM ADD1; LT_SUC_LE]]]);;
1214
1215 let LE_LDIV_EQ = prove
1216  (`!a b n. ~(a = 0) ==> (b DIV a <= n <=> b < a * (n + 1))`,
1217   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM NOT_LT] THEN
1218   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM LE_SUC_LT] THEN
1219   ASM_SIMP_TAC[LE_RDIV_EQ] THEN REWRITE_TAC[NOT_LT; NOT_LE; ADD1]);;
1220
1221 let LE_LDIV = prove
1222  (`!a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n`,
1223   SIMP_TAC[LE_LDIV_EQ; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
1224   MESON_TAC[LT_ADD; LT_NZ; LET_TRANS]);;
1225
1226 let DIV_MONO = prove
1227  (`!m n p. ~(p = 0) /\ m <= n ==> m DIV p <= n DIV p`,
1228   REPEAT STRIP_TAC THEN
1229   MATCH_MP_TAC(MESON[LE_REFL] `(!k:num. k <= a ==> k <= b) ==> a <= b`) THEN
1230   ASM_SIMP_TAC[LE_RDIV_EQ] THEN ASM_MESON_TAC[LE_TRANS]);;
1231
1232 let DIV_MONO_LT = prove
1233  (`!m n p. ~(p = 0) /\ m + p <= n ==> m DIV p < n DIV p`,
1234   REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[ADD1; LE_SUC_LT; LE_REFL]
1235    `(!k:num. k <= a ==> k + 1 <= b) ==> a < b`) THEN
1236   ASM_SIMP_TAC[LE_RDIV_EQ; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
1237   ASM_MESON_TAC[LE_REFL; LE_TRANS; LE_ADD2; ADD_SYM]);;
1238
1239 let DIV_EQ_0 = prove
1240  (`!m n. ~(n = 0) ==> ((m DIV n = 0) <=> m < n)`,
1241   REPEAT(STRIP_TAC ORELSE EQ_TAC) THENL
1242    [FIRST_ASSUM(SUBST1_TAC o CONJUNCT1 o SPEC `m:num` o MATCH_MP DIVISION) THEN
1243     ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; DIVISION];
1244     MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `m:num` THEN
1245     ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]]);;
1246
1247 let MOD_EQ_0 = prove
1248  (`!m n. ~(n = 0) ==> ((m MOD n = 0) <=> (?q. m = q * n))`,
1249   REPEAT(STRIP_TAC ORELSE EQ_TAC) THENL
1250    [FIRST_ASSUM(SUBST1_TAC o CONJUNCT1 o SPEC `m:num` o MATCH_MP DIVISION) THEN
1251     ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; DIVISION] THEN MESON_TAC[];
1252     MATCH_MP_TAC MOD_UNIQ THEN ASM_SIMP_TAC[ADD_CLAUSES; MULT_AC] THEN
1253     ASM_MESON_TAC[NOT_LE; CONJUNCT1 LE]]);;
1254
1255 let MOD_REFL = prove
1256  (`!n. ~(n = 0) ==> n MOD n = 0`,
1257   SIMP_TAC[MOD_EQ_0] THEN MESON_TAC[MULT_CLAUSES]);;
1258
1259 let EVEN_MOD = prove
1260  (`!n. EVEN(n) <=> (n MOD 2 = 0)`,
1261   GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
1262   MATCH_MP_TAC(GSYM MOD_EQ_0) THEN REWRITE_TAC[TWO; NOT_SUC]);;
1263
1264 let ODD_MOD = prove
1265  (`!n. ODD(n) <=> (n MOD 2 = 1)`,
1266   GEN_TAC THEN REWRITE_TAC[GSYM NOT_EVEN; EVEN_MOD] THEN
1267   SUBGOAL_THEN `n MOD 2 < 2` MP_TAC THENL
1268    [SIMP_TAC[DIVISION; TWO; NOT_SUC]; ALL_TAC] THEN
1269   SPEC_TAC(`n MOD 2`,`n:num`) THEN
1270   REWRITE_TAC[TWO; ONE; LT] THEN MESON_TAC[NOT_SUC]);;
1271
1272 let MOD_MULT_RMOD = prove
1273  (`!m n p. ~(n = 0) ==> ((m * (p MOD n)) MOD n = (m * p) MOD n)`,
1274   REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN
1275   EXISTS_TAC `m * p DIV n` THEN
1276   REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
1277   REWRITE_TAC[EQ_MULT_LCANCEL] THEN DISJ2_TAC THEN
1278   ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_SIMP_TAC[DIVISION]);;
1279
1280 let MOD_MULT_LMOD = prove
1281  (`!m n p. ~(n = 0) ==> (((m MOD n) * p) MOD n = (m * p) MOD n)`,
1282   ONCE_REWRITE_TAC[MULT_SYM] THEN SIMP_TAC[MOD_MULT_RMOD]);;
1283
1284 let MOD_MULT_MOD2 = prove
1285  (`!m n p. ~(n = 0) ==> (((m MOD n) * (p MOD n)) MOD n = (m * p) MOD n)`,
1286   SIMP_TAC[MOD_MULT_RMOD; MOD_MULT_LMOD]);;
1287
1288 let MOD_EXP_MOD = prove
1289  (`!m n p. ~(n = 0) ==> (((m MOD n) EXP p) MOD n = (m EXP p) MOD n)`,
1290   REPEAT STRIP_TAC THEN SPEC_TAC(`p:num`,`p:num`) THEN
1291   INDUCT_TAC THEN ASM_REWRITE_TAC[EXP] THEN ASM_SIMP_TAC[MOD_MULT_LMOD] THEN
1292   MATCH_MP_TAC EQ_TRANS THEN
1293   EXISTS_TAC `(m * ((m MOD n) EXP p) MOD n) MOD n` THEN CONJ_TAC THENL
1294    [ALL_TAC; ASM_REWRITE_TAC[]] THEN
1295   ASM_SIMP_TAC[MOD_MULT_RMOD]);;
1296
1297 let MOD_MULT_ADD = prove
1298  (`!m n p. (m * n + p) MOD n = p MOD n`,
1299   REPEAT STRIP_TAC THEN
1300   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1301   MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `m + p DIV n` THEN
1302   ASM_SIMP_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; EQ_ADD_LCANCEL; DIVISION]);;
1303
1304 let DIV_MULT_ADD = prove
1305  (`!a b n. ~(n = 0) ==> (a * n + b) DIV n = a + b DIV n`,
1306   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN
1307   EXISTS_TAC `b MOD n` THEN
1308   REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC] THEN
1309   ASM_MESON_TAC[DIVISION]);;
1310
1311 let MOD_ADD_MOD = prove
1312  (`!a b n. ~(n = 0) ==> ((a MOD n + b MOD n) MOD n = (a + b) MOD n)`,
1313   REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN
1314   EXISTS_TAC `a DIV n + b DIV n` THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1315   ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + (c + d) = (c + a) + (d + b)`] THEN
1316   BINOP_TAC THEN ASM_SIMP_TAC[DIVISION]);;
1317
1318 let DIV_ADD_MOD = prove
1319  (`!a b n. ~(n = 0)
1320            ==> (((a + b) MOD n = a MOD n + b MOD n) <=>
1321                 ((a + b) DIV n = a DIV n + b DIV n))`,
1322   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
1323   DISCH_THEN(fun th -> MAP_EVERY (MP_TAC o CONJUNCT1 o C SPEC th)
1324     [`a + b:num`; `a:num`; `b:num`]) THEN
1325   DISCH_THEN(fun th1 -> DISCH_THEN(fun th2 ->
1326     MP_TAC(MK_COMB(AP_TERM `(+)` th2,th1)))) THEN
1327   DISCH_THEN(fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV) [th]) THEN
1328   ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + c + d = (a + c) + (b + d)`] THEN
1329   REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
1330   DISCH_THEN(fun th -> EQ_TAC THEN DISCH_TAC THEN MP_TAC th) THEN
1331   ASM_REWRITE_TAC[EQ_ADD_RCANCEL; EQ_ADD_LCANCEL; EQ_MULT_RCANCEL] THEN
1332   REWRITE_TAC[EQ_SYM_EQ]);;
1333
1334 let DIV_REFL = prove
1335  (`!n. ~(n = 0) ==> (n DIV n = 1)`,
1336   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN
1337   EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
1338   POP_ASSUM MP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN
1339   INDUCT_TAC THEN REWRITE_TAC[LT_0]);;
1340
1341 let MOD_LE = prove
1342  (`!m n. ~(n = 0) ==> m MOD n <= m`,
1343   REPEAT GEN_TAC THEN
1344   DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV
1345    [MATCH_MP DIVISION th]) THEN
1346   ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LE_ADD]);;
1347
1348 let DIV_MONO2 = prove
1349  (`!m n p. ~(p = 0) /\ p <= m ==> n DIV m <= n DIV p`,
1350   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LE_RDIV_EQ] THEN
1351   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `m * n DIV m` THEN
1352   ASM_REWRITE_TAC[LE_MULT_RCANCEL] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
1353   MP_TAC(SPECL [`n:num`; `m:num`] DIVISION) THEN ASM_MESON_TAC[LE_ADD; LE]);;
1354
1355 let DIV_LE_EXCLUSION = prove
1356  (`!a b c d. ~(b = 0) /\ b * c < (a + 1) * d ==> c DIV d <= a DIV b`,
1357   REPEAT GEN_TAC THEN ASM_CASES_TAC `d = 0` THEN
1358   ASM_REWRITE_TAC[MULT_CLAUSES; LT] THEN STRIP_TAC THEN
1359   MATCH_MP_TAC(MESON[LE_REFL] `(!k:num. k <= a ==> k <= b) ==> a <= b`) THEN
1360   X_GEN_TAC `k:num` THEN
1361   SUBGOAL_THEN `b * d * k <= b * c ==> (b * k) * d < (a + 1) * d` MP_TAC THENL
1362    [ASM_MESON_TAC[LET_TRANS; MULT_AC]; ALL_TAC] THEN
1363   MATCH_MP_TAC MONO_IMP THEN
1364   ASM_SIMP_TAC[LE_MULT_LCANCEL; LT_MULT_RCANCEL; LE_RDIV_EQ] THEN
1365   REWRITE_TAC[GSYM ADD1; LT_SUC_LE]);;
1366
1367 let DIV_EQ_EXCLUSION = prove
1368  (`b * c < (a + 1) * d /\ a * d < (c + 1) * b ==> (a DIV b = c DIV d)`,
1369   REPEAT GEN_TAC THEN
1370   ASM_CASES_TAC `b = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; LT] THEN
1371   ASM_CASES_TAC `d = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; LT] THEN
1372   ASM_MESON_TAC[MULT_SYM; LE_ANTISYM; DIV_LE_EXCLUSION]);;
1373
1374 let MULT_DIV_LE = prove
1375  (`!m n p. ~(p = 0) ==> m * (n DIV p) <= (m * n) DIV p`,
1376   REPEAT GEN_TAC THEN SIMP_TAC[LE_RDIV_EQ] THEN
1377   DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN
1378   DISCH_THEN(fun th ->
1379     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [CONJUNCT1 th]) THEN
1380   REWRITE_TAC[LEFT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC; LE_ADD]);;
1381
1382 let DIV_DIV = prove
1383  (`!m n p. ~(n * p = 0) ==> ((m DIV n) DIV p = m DIV (n * p))`,
1384   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN
1385   MATCH_MP_TAC(MESON[LE_ANTISYM] `(!k. k <= m <=> k <= n) ==> m = n`) THEN
1386   ASM_SIMP_TAC[LE_RDIV_EQ; MULT_EQ_0; MULT_ASSOC]);;
1387
1388 let DIV_MOD = prove
1389  (`!m n p. ~(n * p = 0) ==> ((m DIV n) MOD p = (m MOD (n * p)) DIV n)`,
1390   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN
1391   MATCH_MP_TAC(MESON[LE_ANTISYM] `(!k. k <= m <=> k <= n) ==> m = n`) THEN
1392   X_GEN_TAC `k:num` THEN MATCH_MP_TAC EQ_TRANS THEN
1393   EXISTS_TAC `k + p * ((m DIV n) DIV p) <= (m DIV n)` THEN CONJ_TAC THENL
1394    [MP_TAC(SPECL [`m DIV n`; `p:num`] DIVISION) THEN ASM_REWRITE_TAC[];
1395     MP_TAC(SPECL [`m:num`; `n * p:num`] DIVISION) THEN
1396     ASM_SIMP_TAC[LE_RDIV_EQ; MULT_EQ_0; DIV_DIV; LEFT_ADD_DISTRIB]] THEN
1397   REWRITE_TAC[MULT_AC] THEN MESON_TAC[ADD_SYM; MULT_SYM; LE_ADD_RCANCEL]);;
1398
1399 let MOD_MOD_EXP_MIN = prove
1400  (`!x p m n. ~(p = 0)
1401              ==> x MOD (p EXP m) MOD (p EXP n) = x MOD (p EXP (MIN m n))`,
1402   REPEAT STRIP_TAC THEN REWRITE_TAC[MIN] THEN
1403   ASM_CASES_TAC `m:num <= n` THEN ASM_REWRITE_TAC[] THENL
1404    [FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
1405     MATCH_MP_TAC MOD_LT THEN MATCH_MP_TAC LTE_TRANS THEN
1406     EXISTS_TAC `p EXP m` THEN
1407     ASM_SIMP_TAC[DIVISION; EXP_EQ_0; LE_EXP; LE_ADD];
1408     SUBGOAL_THEN `?d. m = n + d` (CHOOSE_THEN SUBST1_TAC) THENL
1409      [ASM_MESON_TAC[LE_CASES; LE_EXISTS];
1410       ASM_SIMP_TAC[EXP_ADD; MOD_MOD; MULT_EQ_0; EXP_EQ_0]]]);;
1411
1412 (* ------------------------------------------------------------------------- *)
1413 (* Theorems for eliminating cutoff subtraction, predecessor, DIV and MOD.    *)
1414 (* We have versions that introduce universal or existential quantifiers.     *)
1415 (* ------------------------------------------------------------------------- *)
1416
1417 let PRE_ELIM_THM = prove
1418  (`P(PRE n) <=> !m. n = SUC m \/ m = 0 /\ n = 0 ==> P m`,
1419   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
1420   REWRITE_TAC[NOT_SUC; SUC_INJ; PRE] THEN MESON_TAC[]);;
1421
1422 let PRE_ELIM_THM' = prove
1423  (`P(PRE n) <=> ?m. (n = SUC m \/ m = 0 /\ n = 0) /\ P m`,
1424   MP_TAC(INST [`\x:num. ~P x`,`P:num->bool`] PRE_ELIM_THM) THEN MESON_TAC[]);;
1425
1426 let SUB_ELIM_THM = prove
1427  (`P(a - b) <=> !d. a = b + d \/ a < b /\ d = 0 ==> P d`,
1428   DISJ_CASES_TAC(SPECL [`a:num`; `b:num`] LTE_CASES) THENL
1429    [ASM_MESON_TAC[NOT_LT; SUB_EQ_0; LT_IMP_LE; LE_ADD]; ALL_TAC] THEN
1430   FIRST_ASSUM(X_CHOOSE_THEN `e:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
1431   SIMP_TAC[ADD_SUB2; GSYM NOT_LE; LE_ADD; EQ_ADD_LCANCEL] THEN MESON_TAC[]);;
1432
1433 let SUB_ELIM_THM' = prove
1434  (`P(a - b) <=> ?d. (a = b + d \/ a < b /\ d = 0) /\ P d`,
1435   MP_TAC(INST [`\x:num. ~P x`,`P:num->bool`] SUB_ELIM_THM) THEN MESON_TAC[]);;
1436
1437 let DIVMOD_ELIM_THM = prove
1438  (`P (m DIV n) (m MOD n) <=>
1439         !q r. n = 0 /\ q = 0 /\ r = m \/ m = q * n + r /\ r < n ==> P q r`,
1440   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THENL
1441    [ASM_MESON_TAC[DIVISION_0; LT];
1442     FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN MESON_TAC[DIVMOD_UNIQ]]);;
1443
1444 let DIVMOD_ELIM_THM' = prove
1445  (`P (m DIV n) (m MOD n) <=>
1446         ?q r. (n = 0 /\ q = 0 /\ r = m \/ m = q * n + r /\ r < n) /\ P q r`,
1447   MP_TAC(INST [`\x:num y:num. ~P x y`,`P:num->num->bool`] DIVMOD_ELIM_THM) THEN
1448   MESON_TAC[]);;
1449
1450 (* ------------------------------------------------------------------------- *)
1451 (* Crude but useful conversion for cancelling down equations.                *)
1452 (* ------------------------------------------------------------------------- *)
1453
1454 let NUM_CANCEL_CONV =
1455   let rec minter i l1' l2' l1 l2 =
1456     if l1 = [] then (i,l1',l2'@l2)
1457     else if l2 = [] then (i,l1@l1',l2') else
1458     let h1 = hd l1 and h2 = hd l2 in
1459     if h1 = h2 then minter (h1::i) l1' l2' (tl l1) (tl l2)
1460     else if h1 < h2 then minter i (h1::l1') l2' (tl l1) l2
1461     else minter i l1' (h2::l2') l1 (tl l2) in
1462   let add_tm = `(+)` and eq_tm = `(=) :num->num->bool` in
1463   let EQ_ADD_LCANCEL_0' =
1464     GEN_REWRITE_RULE (funpow 2 BINDER_CONV o LAND_CONV) [EQ_SYM_EQ]
1465       EQ_ADD_LCANCEL_0 in
1466   let AC_RULE = AC ADD_AC in
1467   fun tm ->
1468     let l,r = dest_eq tm in
1469     let lats = sort (<=) (binops `(+)` l)
1470     and rats = sort (<=) (binops `(+)` r) in
1471     let i,lats',rats' = minter [] [] [] lats rats in
1472     let l' = list_mk_binop add_tm (i @ lats')
1473     and r' = list_mk_binop add_tm (i @ rats') in
1474     let lth = AC_RULE (mk_eq(l,l'))
1475     and rth = AC_RULE (mk_eq(r,r')) in
1476     let eth = MK_COMB(AP_TERM eq_tm lth,rth) in
1477     GEN_REWRITE_RULE (RAND_CONV o REPEATC)
1478       [EQ_ADD_LCANCEL; EQ_ADD_LCANCEL_0; EQ_ADD_LCANCEL_0'] eth;;
1479
1480 (* ------------------------------------------------------------------------- *)
1481 (* This is handy for easing MATCH_MP on inequalities.                        *)
1482 (* ------------------------------------------------------------------------- *)
1483
1484 let LE_IMP =
1485   let pth = PURE_ONCE_REWRITE_RULE[IMP_CONJ] LE_TRANS in
1486   fun th -> GEN_ALL(MATCH_MP pth (SPEC_ALL th));;
1487
1488 (* ------------------------------------------------------------------------- *)
1489 (* Binder for "the minimal n such that".                                     *)
1490 (* ------------------------------------------------------------------------- *)
1491
1492 parse_as_binder "minimal";;
1493
1494 let minimal = new_definition
1495   `(minimal) (P:num->bool) = @n. P n /\ !m. m < n ==> ~(P m)`;;
1496
1497 let MINIMAL = prove
1498  (`!P. (?n. P n) <=> P((minimal) P) /\ (!m. m < (minimal) P ==> ~(P m))`,
1499   GEN_TAC THEN REWRITE_TAC[minimal] THEN CONV_TAC(RAND_CONV SELECT_CONV) THEN
1500   REWRITE_TAC[GSYM num_WOP]);;
1501
1502 (* ------------------------------------------------------------------------- *)
1503 (* A common lemma for transitive relations.                                  *)
1504 (* ------------------------------------------------------------------------- *)
1505
1506 let TRANSITIVE_STEPWISE_LT_EQ = prove
1507  (`!R. (!x y z. R x y /\ R y z ==> R x z)
1508          ==> ((!m n. m < n ==> R m n) <=> (!n. R n (SUC n)))`,
1509   REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[LT] THEN
1510   DISCH_TAC THEN SIMP_TAC[LT_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1511   GEN_TAC THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1512   REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL; ADD_CLAUSES] THEN
1513   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN ASM_MESON_TAC[]);;
1514
1515 let TRANSITIVE_STEPWISE_LT = prove
1516  (`!R. (!x y z. R x y /\ R y z ==> R x z) /\ (!n. R n (SUC n))
1517        ==> !m n. m < n ==> R m n`,
1518   REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
1519    `(a ==> (c <=> b)) ==> a /\ b ==> c`) THEN
1520   MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LT_EQ);;
1521
1522 let TRANSITIVE_STEPWISE_LE_EQ = prove
1523  (`!R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z)
1524        ==> ((!m n. m <= n ==> R m n) <=> (!n. R n (SUC n)))`,
1525   REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[LE; LE_REFL] THEN
1526
1527   DISCH_TAC THEN SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1528   GEN_TAC THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1529   REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL; ADD_CLAUSES] THEN
1530   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN ASM_MESON_TAC[]);;
1531
1532 let TRANSITIVE_STEPWISE_LE = prove
1533  (`!R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z) /\
1534        (!n. R n (SUC n))
1535        ==> !m n. m <= n ==> R m n`,
1536   REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
1537    `(a /\ a' ==> (c <=> b)) ==> a /\ a' /\ b ==> c`) THEN
1538   MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LE_EQ);;
1539
1540 (* ------------------------------------------------------------------------- *)
1541 (* A couple of forms of Dependent Choice.                                    *)
1542 (* ------------------------------------------------------------------------- *)
1543
1544 let DEPENDENT_CHOICE_FIXED = prove
1545  (`!P R a:A.
1546         P 0 a /\ (!n x. P n x ==> ?y. P (SUC n) y /\ R n x y)
1547         ==> ?f. f 0 = a /\ (!n. P n (f n)) /\ (!n. R n (f n) (f(SUC n)))`,
1548   REPEAT STRIP_TAC THEN
1549   (MP_TAC o prove_recursive_functions_exist num_RECURSION)
1550     `f 0 = (a:A) /\ (!n. f(SUC n) = @y. P (SUC n) y /\ R n (f n) y)` THEN
1551   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN
1552   ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV
1553    [MESON[num_CASES] `(!n. P n) <=> P 0 /\ !n. P(SUC n)`] THEN
1554   ASM_REWRITE_TAC[AND_FORALL_THM] THEN INDUCT_TAC THEN ASM_MESON_TAC[]);;
1555
1556 let DEPENDENT_CHOICE = prove
1557  (`!P R:num->A->A->bool.
1558         (?a. P 0 a) /\ (!n x. P n x ==> ?y. P (SUC n) y /\ R n x y)
1559         ==> ?f. (!n. P n (f n)) /\ (!n. R n (f n) (f(SUC n)))`,
1560   MESON_TAC[DEPENDENT_CHOICE_FIXED]);;