Examples/cooper.ml

   1 (* ========================================================================= *)
   2 (* Implementation of Cooper's algorithm via proforma theorems.               *)
   3 (* ========================================================================= *)
   4
   5 prioritize_int();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Basic syntax on integer terms.                                            *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let dest_mul = dest_binop `(*)`;;
  12 let dest_add = dest_binop `(+)`;;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* Divisibility.                                                             *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 parse_as_infix("divides",(12,"right"));;
  19
  20 let divides = new_definition
  21   `a divides b <=> ?x. b = a * x`;;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Trivial lemmas about integers.                                            *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let INT_DOWN2 = prove
  28  (`!a b. ?c. !x. x < c ==> x < a /\ x < b`,
  29   MESON_TAC[INT_LE_TOTAL; INT_LET_TRANS]);;
  30
  31 (* ------------------------------------------------------------------------- *)
  32 (* Trivial lemmas about divisibility.                                        *)
  33 (* ------------------------------------------------------------------------- *)
  34
  35 let DIVIDES_ADD = prove
  36  (`!d a b. d divides a /\ d divides b ==> d divides (a + b)`,
  37   MESON_TAC[divides; INT_ADD_LDISTRIB]);;
  38
  39 let DIVIDES_SUB = prove
  40  (`!d a b. d divides a /\ d divides b ==> d divides (a - b)`,
  41   MESON_TAC[divides; INT_SUB_LDISTRIB]);;
  42
  43 let DIVIDES_ADD_REVR = prove
  44  (`!d a b. d divides a /\ d divides (a + b) ==> d divides b`,
  45   MESON_TAC[DIVIDES_SUB; INT_ARITH `(a + b) - a = b`]);;
  46
  47 let DIVIDES_ADD_REVL = prove
  48  (`!d a b. d divides b /\ d divides (a + b) ==> d divides a`,
  49   MESON_TAC[DIVIDES_SUB; INT_ARITH `(a + b) - b = a`]);;
  50
  51 let DIVIDES_LMUL = prove
  52  (`!d a x. d divides a ==> d divides (x * a)`,
  53   ASM_MESON_TAC[divides; INT_ARITH `a * b * c = b * a * c`]);;
  54
  55 let DIVIDES_RNEG = prove
  56  (`!d a. d divides (--a) <=> d divides a`,
  57   REWRITE_TAC[divides] THEN MESON_TAC[INT_MUL_RNEG; INT_NEG_NEG]);;
  58
  59 let DIVIDES_LNEG = prove
  60  (`!d a. (--d) divides a <=> d divides a`,
  61   REWRITE_TAC[divides] THEN
  62   MESON_TAC[INT_MUL_RNEG; INT_MUL_LNEG; INT_NEG_NEG]);;
  63
  64 (* ------------------------------------------------------------------------- *)
  65 (* More specialized lemmas (see footnotes on p4 and p5).                     *)
  66 (* ------------------------------------------------------------------------- *)
  67
  68 let INT_DOWN_MUL_LT = prove
  69  (`!x y d. &0 < d ==> ?c. x + c * d < y`,
  70   MESON_TAC[INT_ARCH; INT_LT_REFL;
  71             INT_ARITH `x - y < c * d <=> x + --c * d < y`]);;
  72
  73 let INT_MOD_LEMMA = prove
  74  (`!d x. &0 < d ==> ?c. &1 <= x + c * d /\ x + c * d <= d`,
  75   REPEAT STRIP_TAC THEN
  76   FIRST_ASSUM(MP_TAC o SPECL [`x:int`; `&0`] o MATCH_MP INT_DOWN_MUL_LT) THEN
  77   DISCH_THEN(X_CHOOSE_TAC `c0:int`) THEN
  78   SUBGOAL_THEN `?c1. &0 <= c1 /\ --(x + c0 * d) < c1 * d` MP_TAC THENL
  79    [SUBGOAL_THEN `?c1. --(x + c0 * d) < c1 * d` MP_TAC THENL
  80      [ASM_MESON_TAC[INT_ARCH; INT_ARITH `&0 < d ==> ~(d = &0)`]; ALL_TAC] THEN
  81     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN
  82     MATCH_MP_TAC(INT_ARITH
  83       `(&0 < --c1 ==> &0 < --cd) /\ xcod < &0
  84        ==> --xcod < cd ==> &0 <= c1`) THEN
  85     ASM_SIMP_TAC[GSYM INT_MUL_LNEG; INT_LT_MUL]; ALL_TAC] THEN
  86   REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`; GSYM NOT_FORALL_THM] THEN
  87   REWRITE_TAC[GSYM INT_FORALL_POS] THEN
  88   REWRITE_TAC[NOT_FORALL_THM] THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
  89   REWRITE_TAC[INT_ARITH `--(x + a * d) < b * d <=> &1 <= x + (a + b) * d`] THEN
  90   DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
  91   EXISTS_TAC `c0 + &n` THEN ASM_REWRITE_TAC[] THEN
  92   FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
  93   UNDISCH_TAC `&1 <= x + (c0 + &n) * d` THEN SPEC_TAC(`n:num`,`n:num`) THEN
  94   INDUCT_TAC THEN REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THENL
  95    [REWRITE_TAC[SUB_0; LT_REFL; INT_ADD_RID] THEN
  96     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN INT_ARITH_TAC;
  97     REWRITE_TAC[GSYM INT_OF_NUM_SUC; LT] THEN INT_ARITH_TAC]);;
  98
  99 (* ------------------------------------------------------------------------- *)
 100 (* Shadow for restricted class of formulas.                                  *)
 101 (* ------------------------------------------------------------------------- *)
 102
 103 let cform_INDUCT,cform_RECURSION = define_type
 104   "cform = Lt int
 105          | Gt int
 106          | Eq int
 107          | Ne int
 108          | Divides int int
 109          | Ndivides int int
 110          | And cform cform
 111          | Or cform cform
 112          | Nox bool";;
 113
 114 (* ------------------------------------------------------------------------- *)
 115 (* Interpretation of a cform.                                                *)
 116 (* ------------------------------------------------------------------------- *)
 117
 118 let interp = new_recursive_definition cform_RECURSION
 119   `(interp x (Lt e) <=> x + e < &0) /\
 120    (interp x (Gt e) <=> x + e > &0) /\
 121    (interp x (Eq e) <=> (x + e = &0)) /\
 122    (interp x (Ne e) <=> ~(x + e = &0)) /\
 123    (interp x (Divides c e) <=> c divides (x + e)) /\
 124    (interp x (Ndivides c e) <=> ~(c divides (x + e))) /\
 125    (interp x (And p q) <=> interp x p /\ interp x q) /\
 126    (interp x (Or p q) <=> interp x p \/ interp x q) /\
 127    (interp x (Nox P) <=> P)`;;
 128
 129 (* ------------------------------------------------------------------------- *)
 130 (* The "minus infinity" and "plus infinity" variants.                        *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let minusinf = new_recursive_definition cform_RECURSION
 134  `(minusinf (Lt e) = Nox T) /\
 135   (minusinf (Gt e) = Nox F) /\
 136   (minusinf (Eq e) = Nox F) /\
 137   (minusinf (Ne e) = Nox T) /\
 138   (minusinf (Divides c e) = Divides c e) /\
 139   (minusinf (Ndivides c e) = Ndivides c e) /\
 140   (minusinf (And p q) = And (minusinf p) (minusinf q)) /\
 141   (minusinf (Or p q) = Or (minusinf p) (minusinf q)) /\
 142   (minusinf (Nox P) = Nox P)`;;
 143
 144 let plusinf = new_recursive_definition cform_RECURSION
 145  `(plusinf (Lt e) = Nox F) /\
 146   (plusinf (Gt e) = Nox T) /\
 147   (plusinf (Eq e) = Nox F) /\
 148   (plusinf (Ne e) = Nox T) /\
 149   (plusinf (Divides c e) = Divides c e) /\
 150   (plusinf (Ndivides c e) = Ndivides c e) /\
 151   (plusinf (And p q) = And (plusinf p) (plusinf q)) /\
 152   (plusinf (Or p q) = Or (plusinf p) (plusinf q)) /\
 153   (plusinf (Nox P) = Nox P)`;;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* All the "dividing" things divide the given constant (e.g. their LCM).     *)
 157 (* ------------------------------------------------------------------------- *)
 158
 159 let alldivide = new_recursive_definition cform_RECURSION
 160  `(alldivide d (Lt e) <=> T) /\
 161   (alldivide d (Gt e) <=> T) /\
 162   (alldivide d (Eq e) <=> T) /\
 163   (alldivide d (Ne e) <=> T) /\
 164   (alldivide d (Divides c e) <=> c divides d) /\
 165   (alldivide d (Ndivides c e) <=> c divides d) /\
 166   (alldivide d (And p q) <=> alldivide d p /\ alldivide d q) /\
 167   (alldivide d (Or p q) <=> alldivide d p /\ alldivide d q) /\
 168   (alldivide d (Nox P) <=> T)`;;
 169
 170 (* ------------------------------------------------------------------------- *)
 171 (* A-sets and B-sets.                                                        *)
 172 (* ------------------------------------------------------------------------- *)
 173
 174 let aset = new_recursive_definition cform_RECURSION
 175  `(aset (Lt e) = {(--e)}) /\
 176   (aset (Gt e) = {}) /\
 177   (aset (Eq e) = {(--e + &1)}) /\
 178   (aset (Ne e) = {(--e)}) /\
 179   (aset (Divides c e) = {}) /\
 180   (aset (Ndivides c e) = {}) /\
 181   (aset (And p q) = (aset p) UNION (aset q)) /\
 182   (aset (Or p q) = (aset p) UNION (aset q)) /\
 183   (aset (Nox P) = {})`;;
 184
 185 let bset = new_recursive_definition cform_RECURSION
 186  `(bset (Lt e) = {}) /\
 187   (bset (Gt e) = {(--e)}) /\
 188   (bset (Eq e) = {(--(e + &1))}) /\
 189   (bset (Ne e) = {(--e)}) /\
 190   (bset (Divides c e) = {}) /\
 191   (bset (Ndivides c e) = {}) /\
 192   (bset (And p q) = (bset p) UNION (bset q)) /\
 193   (bset (Or p q) = (bset p) UNION (bset q)) /\
 194   (bset (Nox P) = {})`;;
 195
 196 (* ------------------------------------------------------------------------- *)
 197 (* The key minimality case analysis for the integers.                        *)
 198 (* ------------------------------------------------------------------------- *)
 199
 200 let INT_EXISTS_CASES = prove
 201  (`(?x. P x) <=> (!y. ?x. x < y /\ P x) \/ (?x. P x /\ !y. y < x ==> ~P y)`,
 202   EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 203   DISCH_THEN(X_CHOOSE_TAC `x:int`) THEN
 204   MATCH_MP_TAC(TAUT `(~b ==> a) ==> a \/ b`) THEN
 205   REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(p /\ q) <=> p ==> ~q`; NOT_FORALL_THM;
 206               NOT_IMP] THEN
 207   STRIP_TAC THEN X_GEN_TAC `y:int` THEN
 208   DISJ_CASES_TAC(INT_ARITH `x < y \/ &0 <= x - y`) THENL
 209    [ASM_MESON_TAC[]; ALL_TAC] THEN
 210   SUBGOAL_THEN `!n. ?y. y < x - &n /\ P y` MP_TAC THENL
 211    [ALL_TAC;
 212     REWRITE_TAC[INT_FORALL_POS] THEN
 213     DISCH_THEN(MP_TAC o SPEC `x - y`) THEN
 214     ASM_REWRITE_TAC[INT_ARITH `x - (x - y) = y`]] THEN
 215   INDUCT_TAC THEN
 216   REWRITE_TAC[INT_SUB_RZERO; GSYM INT_OF_NUM_SUC] THEN
 217   ASM_MESON_TAC[INT_ARITH `z < y /\ y < x - &n ==> z < x - (&n + &1)`]);;
 218
 219 (* ------------------------------------------------------------------------- *)
 220 (* Lemmas towards the main theorems (following my book).                     *)
 221 (* ------------------------------------------------------------------------- *)
 222
 223 let MINUSINF_LEMMA = prove
 224  (`!p. ?y. !x. x < y ==> (interp x p <=> interp x (minusinf p))`,
 225   MATCH_MP_TAC cform_INDUCT THEN
 226   REWRITE_TAC[interp; minusinf] THEN
 227   MATCH_MP_TAC(TAUT
 228    `(a /\ b /\ c /\ d) /\ (e /\ f) ==> a /\ b /\ c /\ d /\ e /\ f`) THEN
 229   CONJ_TAC THENL
 230    [MESON_TAC[INT_ARITH `x < --a ==> x + a < &0`; INT_GT;
 231               INT_LT_ANTISYM; INT_LT_REFL];
 232     ALL_TAC] THEN
 233   CONJ_TAC THEN REPEAT GEN_TAC THEN
 234   REWRITE_TAC[LEFT_AND_EXISTS_THM;
 235      RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 236   MAP_EVERY X_GEN_TAC [`a:int`; `b:int`] THEN STRIP_TAC THEN
 237   MP_TAC(SPECL [`a:int`; `b:int`] INT_DOWN2) THEN
 238   MATCH_MP_TAC MONO_EXISTS THEN ASM_SIMP_TAC[]);;
 239
 240 let MINUSINF_REPEATS = prove
 241  (`!p c d x. alldivide d p
 242              ==> (interp x (minusinf p) <=> interp (x + c * d) (minusinf p))`,
 243   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC cform_INDUCT THEN
 244   SIMP_TAC[interp; minusinf; alldivide] THEN
 245   ONCE_REWRITE_TAC[INT_ARITH `(x + d) + y = (x + y) + d`] THEN
 246   MESON_TAC[DIVIDES_LMUL; DIVIDES_ADD_REVL; DIVIDES_ADD]);;
 247
 248 let NOMINIMAL_EQUIV = prove
 249  (`alldivide d p /\ &0 < d
 250    ==> ((!y. ?x. x < y /\ interp x p) <=>
 251         ?j. &1 <= j /\ j <= d /\ interp j (minusinf p))`,
 252   ASM_MESON_TAC[MINUSINF_LEMMA; MINUSINF_REPEATS; INT_DOWN_MUL_LT;
 253                 INT_DOWN2; INT_MOD_LEMMA]);;
 254
 255 let BDISJ_REPEATS_LEMMA = prove
 256  (`!d p. alldivide d p /\ &0 < d
 257          ==> !x. interp x p /\ ~(interp (x - d) p)
 258                  ==> ?j b. &1 <= j /\ j <= d /\ b IN bset p /\ (x = b + j)`,
 259   GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `a /\ b ==> c <=> b ==> a ==> c`] THEN
 260   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 261   MATCH_MP_TAC cform_INDUCT THEN
 262   REWRITE_TAC[interp; alldivide; bset; NOT_IN_EMPTY] THEN
 263   MATCH_MP_TAC(TAUT `(a /\ b /\ c /\ d /\ e /\ f) /\ g /\ h
 264                      ==> a /\ b /\ c /\ d /\ e /\ f /\ g /\ h`) THEN
 265   CONJ_TAC THENL
 266    [ALL_TAC;
 267     SIMP_TAC[TAUT `~a \/ a`;
 268              TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`;
 269              TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`;
 270              TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`;
 271              DE_MORGAN_THM; IN_UNION; EXISTS_OR_THM; FORALL_AND_THM]] THEN
 272   REPEAT STRIP_TAC THENL
 273    [ALL_TAC;
 274     MAP_EVERY EXISTS_TAC [`x + a`; `--a`];
 275     MAP_EVERY EXISTS_TAC [`&1`; `--a - &1`];
 276     MAP_EVERY EXISTS_TAC [`d:int`; `--a`];
 277     ASM_MESON_TAC[INT_ARITH `(x - y) + z = (x + z) - y`; DIVIDES_SUB];
 278     ASM_MESON_TAC[INT_ARITH `(x - y) + z = (x + z) - y`;
 279                   INT_ARITH `(x - y) + y = x`; DIVIDES_ADD]] THEN
 280   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 281   REWRITE_TAC[IN_SING] THEN INT_ARITH_TAC);;
 282
 283 let MAINTHM_B = prove
 284  (`!p d. alldivide d p /\ &0 < d
 285          ==> ((?x. interp x p) <=>
 286               ?j. &1 <= j /\ j <= d /\
 287                   (interp j (minusinf p) \/
 288                    ?b. b IN bset p /\ interp (b + j) p))`,
 289   REPEAT GEN_TAC THEN DISCH_TAC THEN
 290   REWRITE_TAC[TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`; EXISTS_OR_THM] THEN
 291   MATCH_MP_TAC(TAUT
 292    `!a1 a2. (a <=> a1 \/ a2) /\ (a1 <=> b) /\ (a2 ==> c) /\ (c ==> a)
 293             ==> (a <=> b \/ c)`) THEN
 294   EXISTS_TAC `!y. ?x. x < y /\ interp x p` THEN
 295   EXISTS_TAC `?x. interp x p /\ !y. y < x ==> ~(interp y p)` THEN
 296   REPEAT CONJ_TAC THENL
 297    [REWRITE_TAC[GSYM INT_EXISTS_CASES];
 298     ASM_MESON_TAC[NOMINIMAL_EQUIV];
 299     ALL_TAC;
 300     MESON_TAC[]] THEN
 301   DISCH_THEN(X_CHOOSE_THEN `x:int`
 302    (CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x - d`))) THEN
 303   ASM_SIMP_TAC[INT_ARITH `&0 < d ==> x - d < x`] THEN
 304   DISCH_TAC THEN
 305   MP_TAC(SPECL [`d:int`; `p:cform`] BDISJ_REPEATS_LEMMA) THEN
 306   ASM_REWRITE_TAC[] THEN
 307   DISCH_THEN(MP_TAC o SPEC `x:int`) THEN ASM_MESON_TAC[]);;
 308
 309 (* ------------------------------------------------------------------------- *)
 310 (* Deduce the other one by a symmetry argument rather than a similar proof.  *)
 311 (* ------------------------------------------------------------------------- *)
 312
 313 let mirror = new_recursive_definition cform_RECURSION
 314  `(mirror (Lt e) = Gt(--e)) /\
 315   (mirror (Gt e) = Lt(--e)) /\
 316   (mirror (Eq e) = Eq(--e)) /\
 317   (mirror (Ne e) = Ne(--e)) /\
 318   (mirror (Divides c e) = Divides c (--e)) /\
 319   (mirror (Ndivides c e) = Ndivides c (--e)) /\
 320   (mirror (And p q) = And (mirror p) (mirror q)) /\
 321   (mirror (Or p q) = Or (mirror p) (mirror q)) /\
 322   (mirror (Nox P) = Nox P)`;;
 323
 324 let INTERP_MIRROR_LEMMA = prove
 325  (`!p x. interp (--x) (mirror p) <=> interp x p`,
 326   MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[mirror; interp] THEN
 327   REWRITE_TAC[GSYM INT_NEG_ADD; DIVIDES_RNEG] THEN INT_ARITH_TAC);;
 328
 329 let INTERP_MIRROR = prove
 330  (`!p x. interp x (mirror p) <=> interp (--x) p`,
 331   MESON_TAC[INTERP_MIRROR_LEMMA; INT_NEG_NEG]);;
 332
 333 let BSET_MIRROR = prove
 334  (`!p. bset(mirror p) = IMAGE (--) (aset p)`,
 335   MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[mirror; aset; bset] THEN
 336   REWRITE_TAC[IMAGE_CLAUSES; IMAGE_UNION] THEN
 337   REWRITE_TAC[EXTENSION; IN_SING] THEN INT_ARITH_TAC);;
 338
 339 let MINUSINF_MIRROR = prove
 340  (`!p. minusinf (mirror p) = mirror (plusinf p)`,
 341   MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[plusinf; minusinf; mirror]);;
 342
 343 let PLUSINF_MIRROR = prove
 344  (`!p. plusinf p = mirror(minusinf (mirror p))`,
 345   MATCH_MP_TAC cform_INDUCT THEN
 346   SIMP_TAC[plusinf; minusinf; mirror; INT_NEG_NEG]);;
 347
 348 let ALLDIVIDE_MIRROR = prove
 349  (`!p d. alldivide d (mirror p) = alldivide d p`,
 350   MATCH_MP_TAC cform_INDUCT THEN SIMP_TAC[mirror; alldivide]);;
 351
 352 let EXISTS_NEG = prove
 353  (`(?x. P(--x)) <=> (?x. P(x))`,
 354   MESON_TAC[INT_NEG_NEG]);;
 355
 356 let FORALL_NEG = prove
 357  (`(!x. P(--x)) <=> (!x. P x)`,
 358   MESON_TAC[INT_NEG_NEG]);;
 359
 360 let EXISTS_MOD_IMP = prove
 361  (`!P d. (!c x. P(x + c * d) <=> P(x)) /\ (?j. &1 <= j /\ j <= d /\ P(--j))
 362          ==> ?j. &1 <= j /\ j <= d /\ P(j)`,
 363   REPEAT STRIP_TAC THEN ASM_CASES_TAC `d:int = j` THENL
 364    [FIRST_X_ASSUM(MP_TAC o SPECL [`--(&2)`; `d:int`]) THEN
 365     ASM_REWRITE_TAC[INT_ARITH `d + --(&2) * d = --d`] THEN
 366     ASM_MESON_TAC[INT_LE_REFL];
 367     FIRST_X_ASSUM(MP_TAC o SPECL [`&1`; `--j`]) THEN
 368     ASM_REWRITE_TAC[INT_ARITH `--j + &1 * d = d - j`] THEN
 369     DISCH_TAC THEN EXISTS_TAC `d - j` THEN ASM_REWRITE_TAC[] THEN
 370     MAP_EVERY UNDISCH_TAC [`&1 <= j`; `j <= d`; `~(d:int = j)`] THEN
 371     INT_ARITH_TAC]);;
 372
 373 let EXISTS_MOD_EQ = prove
 374  (`!P d. (!c x. P(x + c * d) <=> P(x))
 375          ==> ((?j. &1 <= j /\ j <= d /\ P(--j)) <=>
 376               (?j. &1 <= j /\ j <= d /\ P(j)))`,
 377   REPEAT STRIP_TAC THEN EQ_TAC THENL
 378    [MP_TAC(SPEC `P:int->bool` EXISTS_MOD_IMP);
 379     MP_TAC(SPEC `\x. P(--x):bool` EXISTS_MOD_IMP)] THEN
 380   DISCH_THEN(MP_TAC o SPEC `d:int`) THEN ASM_REWRITE_TAC[INT_NEG_NEG] THEN
 381   ASM_REWRITE_TAC[INT_ARITH `--(x + c * d) = --x + --c * d`; FORALL_NEG] THEN
 382   MESON_TAC[]);;
 383
 384 let MAINTHM_A = prove
 385  (`!p d. alldivide d p /\ &0 < d
 386          ==> ((?x. interp x p) <=>
 387               ?j. &1 <= j /\ j <= d /\
 388                   (interp j (plusinf p) \/
 389                    ?a. a IN aset p /\ interp (a - j) p))`,
 390   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM EXISTS_NEG] THEN
 391   REWRITE_TAC[GSYM INTERP_MIRROR] THEN
 392   MP_TAC(SPECL [`mirror p`; `d:int`] MAINTHM_B) THEN
 393   ASM_REWRITE_TAC[ALLDIVIDE_MIRROR] THEN DISCH_THEN SUBST1_TAC THEN
 394   REWRITE_TAC[TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`;
 395               TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`; EXISTS_OR_THM] THEN
 396   BINOP_TAC THENL
 397    [ALL_TAC;
 398     REWRITE_TAC[INTERP_MIRROR; MINUSINF_MIRROR; BSET_MIRROR] THEN
 399     REWRITE_TAC[INT_ARITH `--(b + j) = --b - j`; IN_IMAGE] THEN
 400     MESON_TAC[INT_NEG_NEG]] THEN
 401   REWRITE_TAC[PLUSINF_MIRROR] THEN
 402   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM ALLDIVIDE_MIRROR]) THEN
 403   SPEC_TAC(`mirror p`,`q:cform`) THEN REWRITE_TAC[INTERP_MIRROR] THEN
 404   REPEAT STRIP_TAC THEN MATCH_MP_TAC(GSYM EXISTS_MOD_EQ) THEN
 405   ASM_SIMP_TAC[GSYM MINUSINF_REPEATS]);;
 406
 407 (* ------------------------------------------------------------------------- *)
 408 (* Proforma for elimination of coefficient of main variable.                 *)
 409 (* ------------------------------------------------------------------------- *)
 410
 411 let EXISTS_MULTIPLE_THM_1 = prove
 412  (`(?x. P(&1 * x)) <=> ?x. P(x)`,
 413   REWRITE_TAC[INT_MUL_LID]);;
 414
 415 let EXISTS_MULTIPLE_THM = prove
 416  (`(?x. P(c * x)) <=> ?x. c divides x /\ P(x)`,
 417   MESON_TAC[divides]);;
 418
 419 (* ------------------------------------------------------------------------- *)
 420 (* Ordering of variables determined by a list, *with* trivial default.       *)
 421 (* ------------------------------------------------------------------------- *)
 422
 423 let rec earlier vars x y =
 424   match vars with
 425     z::ovs -> if z = y then false
 426               else if z = x then true
 427               else earlier ovs x y
 428   | [] -> x < y;;
 429
 430 (* ------------------------------------------------------------------------- *)
 431 (* Conversion of integer constant to ML rational number.                     *)
 432 (* This is a tweaked copy of the real-type versions in "real.ml".            *)
 433 (* ------------------------------------------------------------------------- *)
 434
 435 let is_num_const =
 436   let ptm = `&` in
 437   fun tm -> try let l,r = dest_comb tm in
 438                 l = ptm & is_numeral r
 439             with Failure _ -> false;;
 440
 441 let mk_num_const,dest_num_const =
 442   let ptm = `&` in
 443   (fun n -> mk_comb(ptm,mk_numeral n)),
 444   (fun tm -> let l,r = dest_comb tm in
 445              if l = ptm then dest_numeral r
 446              else failwith "dest_num_const");;
 447
 448 let is_int_const =
 449   let ptm = `(--)` in
 450   fun tm ->
 451     is_num_const tm or
 452     try let l,r = dest_comb tm in
 453         l = ptm & is_num_const r
 454     with Failure _ -> false;;
 455
 456 let mk_int_const,dest_int_const =
 457   let ptm = `(--)` in
 458   (fun n -> if n </ Int 0 then mk_comb(ptm,mk_num_const(minus_num n))
 459             else mk_num_const n),
 460   (fun tm -> if try rator tm = ptm with Failure _ -> false then
 461                minus_num (dest_num_const(rand tm))
 462              else dest_num_const tm);;
 463
 464 (* ------------------------------------------------------------------------- *)
 465 (* Similar tweaks of all the REAL_INT_..._CONV arith convs in real.ml        *)
 466 (* ------------------------------------------------------------------------- *)
 467
 468 let INT_LE_CONV,INT_LT_CONV,
 469     INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV =
 470   let tth =
 471     TAUT `(F /\ F <=> F) /\ (F /\ T <=> F) /\
 472           (T /\ F <=> F) /\ (T /\ T <=> T)` in
 473   let nth = TAUT `(~T <=> F) /\ (~F <=> T)` in
 474   let NUM2_EQ_CONV =
 475     COMB2_CONV (RAND_CONV NUM_EQ_CONV) NUM_EQ_CONV THENC
 476     GEN_REWRITE_CONV I [tth] in
 477   let NUM2_NE_CONV =
 478     RAND_CONV NUM2_EQ_CONV THENC
 479     GEN_REWRITE_CONV I [nth] in
 480   let [pth_le1; pth_le2a; pth_le2b; pth_le3] = (CONJUNCTS o prove)
 481    (`(--(&m) <= &n <=> T) /\
 482      (&m <= &n <=> m <= n) /\
 483      (--(&m) <= --(&n) <=> n <= m) /\
 484      (&m <= --(&n) <=> (m = 0) /\ (n = 0))`,
 485     REWRITE_TAC[INT_LE_NEG2] THEN
 486     REWRITE_TAC[INT_LE_LNEG; INT_LE_RNEG] THEN
 487     REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_LE; LE_0] THEN
 488     REWRITE_TAC[LE; ADD_EQ_0]) in
 489   let INT_LE_CONV = FIRST_CONV
 490    [GEN_REWRITE_CONV I [pth_le1];
 491     GEN_REWRITE_CONV I [pth_le2a; pth_le2b] THENC NUM_LE_CONV;
 492     GEN_REWRITE_CONV I [pth_le3] THENC NUM2_EQ_CONV] in
 493   let [pth_lt1; pth_lt2a; pth_lt2b; pth_lt3] = (CONJUNCTS o prove)
 494    (`(&m < --(&n) <=> F) /\
 495      (&m < &n <=> m < n) /\
 496      (--(&m) < --(&n) <=> n < m) /\
 497      (--(&m) < &n <=> ~((m = 0) /\ (n = 0)))`,
 498     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3;
 499                 GSYM NOT_LE; GSYM INT_NOT_LE] THEN
 500     CONV_TAC TAUT) in
 501   let INT_LT_CONV = FIRST_CONV
 502    [GEN_REWRITE_CONV I [pth_lt1];
 503     GEN_REWRITE_CONV I [pth_lt2a; pth_lt2b] THENC NUM_LT_CONV;
 504     GEN_REWRITE_CONV I [pth_lt3] THENC NUM2_NE_CONV] in
 505   let [pth_ge1; pth_ge2a; pth_ge2b; pth_ge3] = (CONJUNCTS o prove)
 506    (`(&m >= --(&n) <=> T) /\
 507      (&m >= &n <=> n <= m) /\
 508      (--(&m) >= --(&n) <=> m <= n) /\
 509      (--(&m) >= &n <=> (m = 0) /\ (n = 0))`,
 510     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; INT_GE] THEN
 511     CONV_TAC TAUT) in
 512   let INT_GE_CONV = FIRST_CONV
 513    [GEN_REWRITE_CONV I [pth_ge1];
 514     GEN_REWRITE_CONV I [pth_ge2a; pth_ge2b] THENC NUM_LE_CONV;
 515     GEN_REWRITE_CONV I [pth_ge3] THENC NUM2_EQ_CONV] in
 516   let [pth_gt1; pth_gt2a; pth_gt2b; pth_gt3] = (CONJUNCTS o prove)
 517    (`(--(&m) > &n <=> F) /\
 518      (&m > &n <=> n < m) /\
 519      (--(&m) > --(&n) <=> m < n) /\
 520      (&m > --(&n) <=> ~((m = 0) /\ (n = 0)))`,
 521     REWRITE_TAC[pth_lt1; pth_lt2a; pth_lt2b; pth_lt3; INT_GT] THEN
 522     CONV_TAC TAUT) in
 523   let INT_GT_CONV = FIRST_CONV
 524    [GEN_REWRITE_CONV I [pth_gt1];
 525     GEN_REWRITE_CONV I [pth_gt2a; pth_gt2b] THENC NUM_LT_CONV;
 526     GEN_REWRITE_CONV I [pth_gt3] THENC NUM2_NE_CONV] in
 527   let [pth_eq1a; pth_eq1b; pth_eq2a; pth_eq2b] = (CONJUNCTS o prove)
 528    (`((&m = &n) <=> (m = n)) /\
 529      ((--(&m) = --(&n)) <=> (m = n)) /\
 530      ((--(&m) = &n) <=> (m = 0) /\ (n = 0)) /\
 531      ((&m = --(&n)) <=> (m = 0) /\ (n = 0))`,
 532     REWRITE_TAC[GSYM INT_LE_ANTISYM; GSYM LE_ANTISYM] THEN
 533     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; LE; LE_0] THEN
 534     CONV_TAC TAUT) in
 535   let INT_EQ_CONV = FIRST_CONV
 536    [GEN_REWRITE_CONV I [pth_eq1a; pth_eq1b] THENC NUM_EQ_CONV;
 537     GEN_REWRITE_CONV I [pth_eq2a; pth_eq2b] THENC NUM2_EQ_CONV] in
 538   INT_LE_CONV,INT_LT_CONV,
 539   INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV;;
 540
 541 let INT_NEG_CONV =
 542   let pth = prove
 543    (`(--(&0) = &0) /\
 544      (--(--(&x)) = &x)`,
 545     REWRITE_TAC[INT_NEG_NEG; INT_NEG_0]) in
 546   GEN_REWRITE_CONV I [pth];;
 547
 548 let INT_MUL_CONV =
 549   let pth0 = prove
 550    (`(&0 * &x = &0) /\
 551      (&0 * --(&x) = &0) /\
 552      (&x * &0 = &0) /\
 553      (--(&x) * &0 = &0)`,
 554     REWRITE_TAC[INT_MUL_LZERO; INT_MUL_RZERO])
 555   and pth1,pth2 = (CONJ_PAIR o prove)
 556    (`((&m * &n = &(m * n)) /\
 557       (--(&m) * --(&n) = &(m * n))) /\
 558      ((--(&m) * &n = --(&(m * n))) /\
 559       (&m * --(&n) = --(&(m * n))))`,
 560     REWRITE_TAC[INT_MUL_LNEG; INT_MUL_RNEG; INT_NEG_NEG] THEN
 561     REWRITE_TAC[INT_OF_NUM_MUL]) in
 562   FIRST_CONV
 563    [GEN_REWRITE_CONV I [pth0];
 564     GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_MULT_CONV;
 565     GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)];;
 566
 567 let INT_ADD_CONV =
 568   let neg_tm = `(--)` in
 569   let amp_tm = `&` in
 570   let add_tm = `(+)` in
 571   let dest = dest_binop `(+)` in
 572   let m_tm = `m:num` and n_tm = `n:num` in
 573   let pth0 = prove
 574    (`(--(&m) + &m = &0) /\
 575      (&m + --(&m) = &0)`,
 576     REWRITE_TAC[INT_ADD_LINV; INT_ADD_RINV]) in
 577   let [pth1; pth2; pth3; pth4; pth5; pth6] = (CONJUNCTS o prove)
 578    (`(--(&m) + --(&n) = --(&(m + n))) /\
 579      (--(&m) + &(m + n) = &n) /\
 580      (--(&(m + n)) + &m = --(&n)) /\
 581      (&(m + n) + --(&m) = &n) /\
 582      (&m + --(&(m + n)) = --(&n)) /\
 583      (&m + &n = &(m + n))`,
 584     REWRITE_TAC[GSYM INT_OF_NUM_ADD; INT_NEG_ADD] THEN
 585     REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
 586     REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID] THEN
 587     ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
 588     REWRITE_TAC[INT_ADD_ASSOC; INT_ADD_LINV; INT_ADD_LID] THEN
 589     REWRITE_TAC[INT_ADD_RINV; INT_ADD_LID]) in
 590   GEN_REWRITE_CONV I [pth0] ORELSEC
 591   (fun tm ->
 592     try let l,r = dest tm in
 593         if rator l = neg_tm then
 594           if rator r = neg_tm then
 595             let th1 = INST [rand(rand l),m_tm; rand(rand r),n_tm] pth1 in
 596             let tm1 = rand(rand(rand(concl th1))) in
 597             let th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) in
 598             TRANS th1 th2
 599           else
 600             let m = rand(rand l) and n = rand r in
 601             let m' = dest_numeral m and n' = dest_numeral n in
 602             if m' <=/ n' then
 603               let p = mk_numeral (n' -/ m') in
 604               let th1 = INST [m,m_tm; p,n_tm] pth2 in
 605               let th2 = NUM_ADD_CONV (rand(rand(lhand(concl th1)))) in
 606               let th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) in
 607               TRANS th3 th1
 608             else
 609               let p = mk_numeral (m' -/ n') in
 610               let th1 = INST [n,m_tm; p,n_tm] pth3 in
 611               let th2 = NUM_ADD_CONV (rand(rand(lhand(lhand(concl th1))))) in
 612               let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 613               let th4 = AP_THM (AP_TERM add_tm th3) (rand tm) in
 614               TRANS th4 th1
 615         else
 616           if rator r = neg_tm then
 617             let m = rand l and n = rand(rand r) in
 618             let m' = dest_numeral m and n' = dest_numeral n in
 619             if n' <=/ m' then
 620               let p = mk_numeral (m' -/ n') in
 621               let th1 = INST [n,m_tm; p,n_tm] pth4 in
 622               let th2 = NUM_ADD_CONV (rand(lhand(lhand(concl th1)))) in
 623               let th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) in
 624               let th4 = AP_THM th3 (rand tm) in
 625               TRANS th4 th1
 626             else
 627              let p = mk_numeral (n' -/ m') in
 628              let th1 = INST [m,m_tm; p,n_tm] pth5 in
 629              let th2 = NUM_ADD_CONV (rand(rand(rand(lhand(concl th1))))) in
 630              let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 631              let th4 = AP_TERM (rator tm) th3 in
 632              TRANS th4 th1
 633           else
 634             let th1 = INST [rand l,m_tm; rand r,n_tm] pth6 in
 635             let tm1 = rand(rand(concl th1)) in
 636             let th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) in
 637             TRANS th1 th2
 638     with Failure _ -> failwith "INT_ADD_CONV");;
 639
 640 let INT_SUB_CONV =
 641   GEN_REWRITE_CONV I [INT_SUB] THENC
 642   TRY_CONV(RAND_CONV INT_NEG_CONV) THENC
 643   INT_ADD_CONV;;
 644
 645 let INT_POW_CONV =
 646   let n = `n:num` and x = `x:num` in
 647   let pth1,pth2 = (CONJ_PAIR o prove)
 648    (`(&x pow n = &(x EXP n)) /\
 649      ((--(&x)) pow n = if EVEN n then &(x EXP n) else --(&(x EXP n)))`,
 650     REWRITE_TAC[INT_OF_NUM_POW; INT_POW_NEG]) in
 651   let tth = prove
 652    (`((if T then x:int else y) = x) /\ ((if F then x:int else y) = y)`,
 653     REWRITE_TAC[]) in
 654   let neg_tm = `(--)` in
 655   (GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_EXP_CONV) ORELSEC
 656   (GEN_REWRITE_CONV I [pth2] THENC
 657    RATOR_CONV(RATOR_CONV(RAND_CONV NUM_EVEN_CONV)) THENC
 658    GEN_REWRITE_CONV I [tth] THENC
 659    (fun tm -> if rator tm = neg_tm then RAND_CONV(RAND_CONV NUM_EXP_CONV) tm
 660               else RAND_CONV NUM_EXP_CONV  tm));;
 661
 662 (* ------------------------------------------------------------------------- *)
 663 (* Handy utility functions for int arithmetic terms.                         *)
 664 (* ------------------------------------------------------------------------- *)
 665
 666 let dest_add = dest_binop `(+)`;;
 667 let dest_mul = dest_binop `(*)`;;
 668 let dest_pow = dest_binop `(pow)`;;
 669 let dest_sub = dest_binop `(-)`;;
 670
 671 let is_add = is_binop `(+)`;;
 672 let is_mul = is_binop `(*)`;;
 673 let is_pow = is_binop `(pow)`;;
 674 let is_sub = is_binop `(-)`;;
 675
 676 (* ------------------------------------------------------------------------- *)
 677 (* Instantiate the normalizer.                                               *)
 678 (* ------------------------------------------------------------------------- *)
 679
 680 let POLYNOMIAL_NORMALIZERS =
 681   let sth = prove
 682    (`(!x y z. x + (y + z) = (x + y) + z) /\
 683      (!x y. x + y = y + x) /\
 684      (!x. &0 + x = x) /\
 685      (!x y z. x * (y * z) = (x * y) * z) /\
 686      (!x y. x * y = y * x) /\
 687      (!x. &1 * x = x) /\
 688      (!x. &0 * x = &0) /\
 689      (!x y z. x * (y + z) = x * y + x * z) /\
 690      (!x. x pow 0 = &1) /\
 691      (!x n. x pow (SUC n) = x * x pow n)`,
 692     REWRITE_TAC[INT_POW] THEN INT_ARITH_TAC)
 693   and rth = prove
 694    (`(!x. --x = --(&1) * x) /\
 695      (!x y. x - y = x + --(&1) * y)`,
 696     INT_ARITH_TAC)
 697   and is_semiring_constant = is_int_const
 698   and SEMIRING_ADD_CONV = INT_ADD_CONV
 699   and SEMIRING_MUL_CONV = INT_MUL_CONV
 700   and SEMIRING_POW_CONV = INT_POW_CONV in
 701   let NORMALIZERS =
 702    SEMIRING_NORMALIZERS_CONV sth rth
 703     (is_semiring_constant,
 704      SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV) in
 705   fun vars -> NORMALIZERS(earlier vars);;
 706
 707 let POLYNOMIAL_NEG_CONV vars =
 708   let cnv,_,_,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
 709
 710 let POLYNOMIAL_ADD_CONV vars =
 711   let _,cnv,_,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
 712
 713 let POLYNOMIAL_SUB_CONV vars =
 714   let _,_,cnv,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
 715
 716 let POLYNOMIAL_MUL_CONV vars =
 717   let _,_,_,cnv,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
 718
 719 let POLYNOMIAL_POW_CONV vars =
 720   let _,_,_,_,cnv,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
 721
 722 let POLYNOMIAL_CONV vars =
 723   let _,_,_,_,_,cnv = POLYNOMIAL_NORMALIZERS vars in cnv;;
 724
 725 (* ------------------------------------------------------------------------- *)
 726 (* Slight variants of these functions for procedure below.                   *)
 727 (* ------------------------------------------------------------------------- *)
 728
 729 let LINEAR_CMUL =
 730   let mul_tm = `(*)` in
 731   fun vars n tm ->
 732     POLYNOMIAL_MUL_CONV vars (mk_comb(mk_comb(mul_tm,mk_int_const n),tm));;
 733
 734 (* ------------------------------------------------------------------------- *)
 735 (* Linearize a formula, dealing with non-strict inequalities.                *)
 736 (* ------------------------------------------------------------------------- *)
 737
 738 let LINEARIZE_CONV =
 739   let rew_conv = GEN_REWRITE_CONV I
 740     [CONJ (REFL `c divides e`)
 741           (INT_ARITH
 742               `(s < t <=> &0 < t - s) /\
 743                (~(s < t) <=> &0 < (s + &1) - t) /\
 744                (s > t <=> &0 < s - t) /\
 745                (~(s > t) <=> &0 < (t + &1) - s) /\
 746                (s <= t <=> &0 < (t + &1) - s) /\
 747                (~(s <= t) <=> &0 < s - t) /\
 748                (s >= t <=> &0 < (s + &1) - t) /\
 749                (~(s >= t) <=> &0 < t - s) /\
 750                ((s = t) <=> (&0 = s - t))`)]
 751   and true_tm = `T` and false_tm = `F` in
 752   let rec conv vars tm =
 753     try (rew_conv THENC RAND_CONV(POLYNOMIAL_CONV vars)) tm with Failure _ ->
 754     if is_exists tm or is_forall tm then
 755       let x = bndvar(rand tm) in BINDER_CONV (conv (x::vars)) tm
 756     else if is_neg tm then
 757       RAND_CONV (conv vars) tm
 758     else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
 759       BINOP_CONV (conv vars) tm
 760     else if tm = true_tm or tm = false_tm then REFL tm
 761     else failwith "LINEARIZE_CONV: Unexpected term type" in
 762   conv;;
 763
 764 (* ------------------------------------------------------------------------- *)
 765 (* Get the coefficient of x, assumed to be first term, if there at all.      *)
 766 (* ------------------------------------------------------------------------- *)
 767
 768 let coefficient x tm =
 769   try let l,r = dest_add tm in
 770       if l = x then Int 1 else
 771       let c,y = dest_mul l in
 772       if y = x then dest_int_const c else Int 0
 773   with Failure _ -> try
 774       let c,y = dest_mul tm in
 775       if y = x then dest_int_const c else Int 0
 776   with Failure _ -> Int 1;;
 777
 778 (* ------------------------------------------------------------------------- *)
 779 (* Find (always positive) LCM of all the multiples of x in formula tm.       *)
 780 (* ------------------------------------------------------------------------- *)
 781
 782 let lcm_num x y = abs_num((x */ y) // gcd_num x y);;
 783
 784 let rec formlcm x tm =
 785   if is_neg tm then formlcm x (rand tm)
 786   else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
 787      lcm_num (formlcm x (lhand tm)) (formlcm x (rand tm))
 788   else if is_forall tm or is_exists tm then
 789      formlcm x (body(rand tm))
 790   else if not(mem x (frees tm)) then Int 1
 791   else let c = coefficient x (rand tm) in
 792        if c =/ Int 0 then Int 1 else c;;
 793
 794 (* ------------------------------------------------------------------------- *)
 795 (* Switch from "x [+ ...]" to "&1 * x [+ ...]" to suit later proforma.       *)
 796 (* ------------------------------------------------------------------------- *)
 797
 798 let MULTIPLY_1_CONV =
 799   let conv_0 = REWR_CONV(INT_ARITH `x = &1 * x`)
 800   and conv_1 = REWR_CONV(INT_ARITH `x + a = &1 * x + a`) in
 801   fun vars tm ->
 802     let x = hd vars in
 803     if tm = x then conv_0 tm
 804     else if is_add tm & lhand tm = x then conv_1 tm
 805     else REFL tm;;
 806
 807 (* ------------------------------------------------------------------------- *)
 808 (* Adjust all coefficients of x (head variable) to match l in formula tm.    *)
 809 (* ------------------------------------------------------------------------- *)
 810
 811 let ADJUSTCOEFF_CONV =
 812   let op_eq = `(=):int->int->bool`
 813   and op_lt = `(<):int->int->bool`
 814   and op_gt = `(>):int->int->bool`
 815   and op_divides = `(divides):int->int->bool`
 816   and c_tm = `c:int`
 817   and d_tm = `d:int`
 818   and e_tm = `e:int` in
 819   let pth_divides = prove
 820    (`~(d = &0) ==> (c divides e <=> (d * c) divides (d * e))`,
 821     SIMP_TAC[divides; GSYM INT_MUL_ASSOC; INT_EQ_MUL_LCANCEL])
 822   and pth_eq = prove
 823    (`~(d = &0) ==> ((&0 = e) <=> (&0 = d * e))`,
 824     DISCH_TAC THEN CONV_TAC(BINOP_CONV SYM_CONV) THEN
 825     ASM_REWRITE_TAC[INT_ENTIRE])
 826   and pth_lt_pos = prove
 827    (`&0 < d ==> (&0 < e <=> &0 < d * e)`,
 828     DISCH_TAC THEN SUBGOAL_THEN `&0 < e <=> d * &0 < d * e` SUBST1_TAC THENL
 829      [ASM_SIMP_TAC[INT_LT_LMUL_EQ]; REWRITE_TAC[INT_MUL_RZERO]])
 830   and pth_gt_pos = prove
 831    (`&0 < d ==> (&0 > e <=> &0 > d * e)`,
 832     DISCH_TAC THEN REWRITE_TAC[INT_GT] THEN
 833     SUBGOAL_THEN `e < &0 <=> d * e < d * &0` SUBST1_TAC THENL
 834      [ASM_SIMP_TAC[INT_LT_LMUL_EQ]; REWRITE_TAC[INT_MUL_RZERO]])
 835   and true_tm = `T` and false_tm = `F` in
 836   let pth_lt_neg = prove
 837    (`d < &0 ==> (&0 < e <=> &0 > d * e)`,
 838     REWRITE_TAC[INT_ARITH `&0 > d * e <=> &0 < --d * e`;
 839                 INT_ARITH `d < &0 <=> &0 < --d`; pth_lt_pos])
 840   and pth_gt_neg = prove
 841    (`d < &0 ==> (&0 > e <=> &0 < d * e)`,
 842     REWRITE_TAC[INT_ARITH `&0 < d * e <=> &0 > --d * e`;
 843                 INT_ARITH `d < &0 <=> &0 < --d`; pth_gt_pos]) in
 844   let rec ADJUSTCOEFF_CONV vars l tm =
 845     if tm = true_tm or tm = false_tm then REFL tm
 846     else if is_exists tm or is_forall tm then
 847       BINDER_CONV (ADJUSTCOEFF_CONV vars l) tm
 848     else if is_neg tm then
 849       RAND_CONV (ADJUSTCOEFF_CONV vars l) tm
 850     else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
 851       BINOP_CONV (ADJUSTCOEFF_CONV vars l) tm
 852     else
 853       let lop,t = dest_comb tm in
 854       let op,z = dest_comb lop in
 855       let c = coefficient (hd vars) t in
 856       if c =/ Int 0 then REFL tm else
 857       let th1 =
 858         if c =/ l then REFL tm else
 859         let m = l // c in
 860         let th0 = if op = op_eq then pth_eq
 861                   else if op = op_divides then pth_divides
 862                   else if op = op_lt then
 863                     if m >/ Int 0 then pth_lt_pos else pth_lt_neg
 864                   else if op = op_gt then
 865                     if m >/ Int 0 then pth_gt_pos else pth_gt_neg
 866                   else failwith "ADJUSTCOEFF_CONV: unknown predicate" in
 867         let th1 = INST [mk_int_const m,d_tm; z,c_tm; t,e_tm] th0 in
 868         let tm1 = lhand(concl th1) in
 869         let th2 = if is_neg tm1 then EQF_ELIM(INT_EQ_CONV(rand tm1))
 870                   else EQT_ELIM(INT_LT_CONV tm1) in
 871         let th3 = MP th1 th2 in
 872         if op = op_divides then
 873           let th3 = MP th1 th2 in
 874           let tm2 = rand(concl th3) in
 875           let l,r = dest_comb tm2 in
 876           let th4 = AP_TERM (rator l) (INT_MUL_CONV (rand l)) in
 877           let th5 = AP_THM th4 r in
 878           let tm3 = rator(rand(concl th5)) in
 879           let th6 = TRANS th5 (AP_TERM tm3 (LINEAR_CMUL vars m t)) in
 880           TRANS th3 th6
 881         else
 882           let tm2 = rator(rand(concl th3)) in
 883           TRANS th3 (AP_TERM tm2 (LINEAR_CMUL vars m t)) in
 884       if l =/ Int 1 then
 885         CONV_RULE(funpow 2 RAND_CONV (MULTIPLY_1_CONV vars)) th1
 886       else th1 in
 887   ADJUSTCOEFF_CONV;;
 888
 889 (* ------------------------------------------------------------------------- *)
 890 (* Now normalize all the x terms to have same coefficient and eliminate it.  *)
 891 (* ------------------------------------------------------------------------- *)
 892
 893 let NORMALIZE_COEFF_CONV =
 894   let c_tm = `c:int`
 895   and pth = prove
 896    (`(?x. P(c * x)) <=> (?x. c divides x /\ P x)`,
 897     REWRITE_TAC[GSYM EXISTS_MULTIPLE_THM]) in
 898   let NORMALIZE_COEFF_CONV vars tm =
 899     let x,bod = dest_exists tm in
 900     let l = formlcm x tm in
 901     let th1 = ADJUSTCOEFF_CONV (x::vars) l tm in
 902     let th2 = if l =/ Int 1 then EXISTS_MULTIPLE_THM_1
 903               else INST [mk_int_const l,c_tm] pth in
 904     TRANS th1 (REWR_CONV th2 (rand(concl th1))) in
 905   NORMALIZE_COEFF_CONV;;
 906
 907 (* ------------------------------------------------------------------------- *)
 908 (* Convert to shadow syntax.                                                 *)
 909 (* ------------------------------------------------------------------------- *)
 910
 911 let SHADOW_CONV =
 912   let pth_trivial = prove
 913    (`P = interp x (Nox P)`,
 914     REWRITE_TAC[interp])
 915   and pth_composite = prove
 916    (`(interp x p /\ interp x q <=> interp x (And p q)) /\
 917      (interp x p \/ interp x q <=> interp x (Or p q))`,
 918     REWRITE_TAC[interp])
 919   and pth_literal_nontrivial = prove
 920    (`(&0 > x + e <=> interp x (Lt e)) /\
 921      (&0 < x + e <=> interp x (Gt e)) /\
 922      ((&0 = x + e) <=> interp x (Eq e)) /\
 923      (~(&0 = x + e) <=> interp x (Ne e)) /\
 924      (c divides (x + e) <=> interp x (Divides c e)) /\
 925      (~(c divides (x + e)) <=> interp x (Ndivides c e))`,
 926     REWRITE_TAC[interp; INT_ADD_RID] THEN INT_ARITH_TAC)
 927   and  pth_literal_trivial = prove
 928    (`(&0 > x <=> interp x (Lt(&0))) /\
 929      (&0 < x <=> interp x (Gt(&0))) /\
 930      ((&0 = x) <=> interp x (Eq(&0))) /\
 931      (~(&0 = x) <=> interp x (Ne(&0))) /\
 932      (c divides x <=> interp x (Divides c (&0))) /\
 933      (~(c divides x) <=> interp x (Ndivides c (&0)))`,
 934     REWRITE_TAC[interp; INT_ADD_RID] THEN INT_ARITH_TAC) in
 935   let rewr_composite = GEN_REWRITE_CONV I [pth_composite]
 936   and rewr_literal = GEN_REWRITE_CONV I [pth_literal_nontrivial] ORELSEC
 937                      GEN_REWRITE_CONV I [pth_literal_trivial]
 938   and x_tm = `x:int` and p_tm = `P:bool` in
 939   let rec SHADOW_CONV x tm =
 940     if not (mem x (frees tm)) then
 941        INST [tm,p_tm; x,x_tm] pth_trivial
 942     else if is_conj tm or is_disj tm then
 943       let l,r = try dest_conj tm with Failure _ -> dest_disj tm in
 944       let thl = SHADOW_CONV x l and thr = SHADOW_CONV x r in
 945       let th1 = MK_COMB(AP_TERM (rator(rator tm)) thl,thr) in
 946       TRANS th1 (rewr_composite(rand(concl th1)))
 947     else rewr_literal tm in
 948   fun tm ->
 949     let x,bod = dest_exists tm in
 950     MK_EXISTS x (SHADOW_CONV x bod);;
 951
 952 (* ------------------------------------------------------------------------- *)
 953 (* Get the LCM of the dividing things.                                       *)
 954 (* ------------------------------------------------------------------------- *)
 955
 956 let dplcm =
 957   let divides_tm = `Divides`
 958   and ndivides_tm = `Ndivides`
 959   and and_tm = `And`
 960   and or_tm = `Or` in
 961   let rec dplcm tm =
 962     let hop,args = strip_comb tm in
 963     if hop = divides_tm or hop = ndivides_tm then dest_int_const (hd args)
 964     else if hop = and_tm or hop = or_tm
 965     then end_itlist lcm_num (map dplcm args)
 966     else Int 1 in
 967   dplcm;;
 968
 969 (* ------------------------------------------------------------------------- *)
 970 (* Conversion for true formulas "(--) &m divides (--) &n".                   *)
 971 (* ------------------------------------------------------------------------- *)
 972
 973 let PROVE_DIVIDES_CONV_POS =
 974   let pth = prove
 975    (`(p * m = n) ==> &p divides &n`,
 976     DISCH_THEN(SUBST1_TAC o SYM) THEN
 977     REWRITE_TAC[divides] THEN EXISTS_TAC `&m` THEN
 978     REWRITE_TAC[INT_OF_NUM_MUL])
 979   and m_tm = `m:num` and n_tm = `n:num` and p_tm = `p:num` in
 980   fun tm ->
 981     let n = rand(rand tm)
 982     and p = rand(lhand tm) in
 983     let m = mk_numeral(dest_numeral n // dest_numeral p) in
 984     let th1 = INST [m,m_tm; n,n_tm; p,p_tm] pth in
 985     EQT_INTRO(MP th1 (NUM_MULT_CONV (lhand(lhand(concl th1)))));;
 986
 987 let PROVE_DIVIDES_CONV =
 988   GEN_REWRITE_CONV REPEATC [DIVIDES_LNEG; DIVIDES_RNEG] THENC
 989   PROVE_DIVIDES_CONV_POS;;
 990
 991 (* ------------------------------------------------------------------------- *)
 992 (* General version that works for positive and negative.                     *)
 993 (* ------------------------------------------------------------------------- *)
 994
 995 let INT_DIVIDES_NUM = prove
 996  (`&p divides &n <=> ?m. (n = p * m)`,
 997   REWRITE_TAC[divides] THEN EQ_TAC THENL
 998    [DISCH_THEN(X_CHOOSE_THEN `x:int` MP_TAC) THEN
 999     DISJ_CASES_THEN(X_CHOOSE_THEN `q:num` SUBST1_TAC)
1000      (SPEC `x:int` INT_IMAGE) THEN
1001     DISCH_THEN(MP_TAC o AP_TERM `abs:int->int`) THEN
1002     REWRITE_TAC[INT_ABS_MUL; INT_ABS_NUM; INT_ABS_NEG] THEN
1003     REWRITE_TAC[INT_OF_NUM_MUL; INT_OF_NUM_EQ] THEN MESON_TAC[];
1004     MESON_TAC[INT_OF_NUM_MUL]]);;
1005
1006 let INT_DIVIDES_POS_CONV =
1007   let pth = prove
1008    (`(&p divides &n) <=> (p = 0) /\ (n = 0) \/ ~(p = 0) /\ (n MOD p = 0)`,
1009     REWRITE_TAC[INT_DIVIDES_NUM] THEN
1010     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN EQ_TAC THENL
1011      [ASM_MESON_TAC[MOD_MULT];
1012       DISCH_TAC THEN
1013       FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN
1014       ASM_REWRITE_TAC[ADD_CLAUSES] THEN MESON_TAC[MULT_SYM]]) in
1015   GEN_REWRITE_CONV I [pth] THENC NUM_REDUCE_CONV;;
1016
1017 let INT_DIVIDES_CONV =
1018   GEN_REWRITE_CONV REPEATC [DIVIDES_LNEG; DIVIDES_RNEG] THENC
1019   INT_DIVIDES_POS_CONV;;
1020
1021 (* ------------------------------------------------------------------------- *)
1022 (* Conversion for "alldivide d p" (which should be true!)                    *)
1023 (* ------------------------------------------------------------------------- *)
1024
1025 let ALLDIVIDE_CONV =
1026   let pth_atom = prove
1027    (`(alldivide d (Lt e) <=> T) /\
1028      (alldivide d (Gt e) <=> T) /\
1029      (alldivide d (Eq e) <=> T) /\
1030      (alldivide d (Ne e) <=> T) /\
1031      (alldivide d (Nox P) <=> T)`,
1032     REWRITE_TAC[alldivide])
1033   and pth_div = prove
1034     (`(alldivide d (Divides c e) <=> c divides d) /\
1035       (alldivide d (Ndivides c e) <=> c divides d)`,
1036      REWRITE_TAC[alldivide])
1037   and pth_comp = prove
1038    (`(alldivide d (And p q) <=> alldivide d p /\ alldivide d q) /\
1039      (alldivide d (Or p q) <=> alldivide d p /\ alldivide d q)`,
1040     REWRITE_TAC[alldivide])
1041   and pth_taut = TAUT `(T /\ T <=> T)` in
1042   let basnet =
1043     itlist (fun th -> enter [] (lhand(concl th),REWR_CONV th))
1044            (CONJUNCTS pth_atom)
1045            (itlist (fun th -> enter [] (lhand(concl th),
1046                                         REWR_CONV th THENC PROVE_DIVIDES_CONV))
1047                    (CONJUNCTS pth_div) empty_net)
1048   and comp_rewr = GEN_REWRITE_CONV I [pth_comp] in
1049   let rec alldivide_conv tm =
1050     try tryfind (fun f -> f tm) (lookup tm basnet) with Failure _ ->
1051     let th = (comp_rewr THENC BINOP_CONV alldivide_conv) tm in
1052     TRANS th pth_taut in
1053   alldivide_conv;;
1054
1055 (* ------------------------------------------------------------------------- *)
1056 (* Conversion for "?b. b IN bset p /\ P b";;                                 *)
1057 (* ------------------------------------------------------------------------- *)
1058
1059 let EXISTS_IN_BSET_CONV =
1060   let pth_false = prove
1061    (`((?b. b IN bset (Lt e) /\ P b) <=> F) /\
1062      ((?b. b IN bset (Divides c e) /\ P b) <=> F) /\
1063      ((?b. b IN bset (Ndivides c e) /\ P b) <=> F) /\
1064      ((?b. b IN bset(Nox Q) /\ P b) <=> F)`,
1065     REWRITE_TAC[bset; NOT_IN_EMPTY])
1066   and pth_neg = prove
1067    (`((?b. b IN bset (Gt e) /\ P b) <=> P(--e)) /\
1068      ((?b. b IN bset (Ne e) /\ P b) <=> P(--e))`,
1069     REWRITE_TAC[bset; IN_SING; INT_MUL_LID; UNWIND_THM2])
1070   and pth_add = prove
1071    (`(?b. b IN bset (Eq e) /\ P b) <=> P(--(e + &1))`,
1072     REWRITE_TAC[bset; IN_SING; INT_MUL_LID; UNWIND_THM2])
1073   and pth_comp = prove
1074    (`((?b. b IN bset (And p q) /\ P b) <=>
1075               (?b. b IN bset p /\ P b) \/
1076               (?b. b IN bset q /\ P b)) /\
1077      ((?b. b IN bset (Or p q) /\ P b) <=>
1078               (?b. b IN bset p /\ P b) \/
1079                    (?b. b IN bset q /\ P b))`,
1080     REWRITE_TAC[bset; IN_UNION] THEN MESON_TAC[])
1081   and taut = TAUT `(F \/ P <=> P) /\ (P \/ F <=> P)` in
1082   let conv_neg vars =
1083     LAND_CONV(LAND_CONV(POLYNOMIAL_NEG_CONV vars))
1084   and conv_add vars =
1085     LAND_CONV(LAND_CONV(RAND_CONV(POLYNOMIAL_ADD_CONV vars) THENC
1086                         POLYNOMIAL_NEG_CONV vars))
1087   and conv_comp = GEN_REWRITE_CONV I [pth_comp] in
1088   let net1 =
1089     itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
1090            (CONJUNCTS pth_false) empty_net in
1091   let net2 =
1092     itlist (fun th -> enter [] (lhand(concl th),
1093         let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_neg v))
1094            (CONJUNCTS pth_neg) net1 in
1095   let basnet =
1096     enter [] (lhand(concl pth_add),
1097         let cnv = K (REWR_CONV pth_add) in fun v -> cnv v THENC conv_add v)
1098             net2 in
1099   let rec baseconv vars tm =
1100     try tryfind (fun f -> f vars tm) (lookup tm basnet) with Failure _ ->
1101     (conv_comp THENC BINOP_CONV (baseconv vars)) tm in
1102   let finconv =
1103     GEN_REWRITE_CONV DEPTH_CONV [taut] THENC
1104     PURE_REWRITE_CONV [DISJ_ACI] in
1105   fun vars tm -> (baseconv vars THENC finconv) tm;;
1106
1107 (* ------------------------------------------------------------------------- *)
1108 (* Naive conversion for "minusinf p".                                        *)
1109 (* ------------------------------------------------------------------------- *)
1110
1111 let MINUSINF_CONV = GEN_REWRITE_CONV TOP_SWEEP_CONV [minusinf];;
1112
1113 (* ------------------------------------------------------------------------- *)
1114 (* Conversion for "interp s p" where s is a canonical linear form.           *)
1115 (* ------------------------------------------------------------------------- *)
1116
1117 let INTERP_CONV =
1118   let pth_trivial = prove
1119    (`interp x (Nox P) <=> P`,
1120     REWRITE_TAC[interp])
1121   and pth_comp = prove
1122    (`(interp x (And p q) <=> interp x p /\ interp x q) /\
1123      (interp x (Or p q) <=> interp x p \/ interp x q)`,
1124     REWRITE_TAC[interp])
1125   and pth_pos,pth_neg = (CONJ_PAIR o prove)
1126    (`((interp x (Lt e)         <=> &0 > x + e) /\
1127       (interp x (Gt e)         <=> &0 < x + e) /\
1128       (interp x (Eq e)         <=> (&0 = x + e)) /\
1129       (interp x (Divides c e)  <=> c divides (x + e))) /\
1130      ((interp x (Ne e)         <=> ~(&0 = x + e)) /\
1131       (interp x (Ndivides c e) <=> ~(c divides (x + e))))`,
1132     REWRITE_TAC[interp] THEN INT_ARITH_TAC) in
1133   let conv_pos vars = RAND_CONV(POLYNOMIAL_ADD_CONV vars)
1134   and conv_neg vars = RAND_CONV(RAND_CONV(POLYNOMIAL_ADD_CONV vars))
1135   and conv_comp = GEN_REWRITE_CONV I [pth_comp] in
1136   let net1 =
1137     itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
1138            (CONJUNCTS pth_trivial) empty_net in
1139   let net2 =
1140     itlist (fun th -> enter [] (lhand(concl th),
1141         let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_pos v))
1142            (CONJUNCTS pth_pos) net1 in
1143   let basnet =
1144     itlist (fun th -> enter [] (lhand(concl th),
1145         let cnv = K (REWR_CONV th) in fun v -> cnv v THENC conv_neg v))
1146            (CONJUNCTS pth_neg) net2 in
1147   let rec baseconv vars tm =
1148     try tryfind (fun f -> f vars tm) (lookup tm basnet) with Failure _ ->
1149     (conv_comp THENC BINOP_CONV (baseconv vars)) tm in
1150   baseconv;;
1151
1152 (* ------------------------------------------------------------------------- *)
1153 (* Expand `?j. &1 <= j /\ j <= &[n] /\ P[j]` cases.                          *)
1154 (* ------------------------------------------------------------------------- *)
1155
1156 let EXPAND_INT_CASES_CONV =
1157   let pth_base = prove
1158    (`(?j. n <= j /\ j <= n /\ P(j)) <=> P(n)`,
1159     MESON_TAC[INT_LE_ANTISYM])
1160   and pth_step = prove
1161    (`(?j. &1 <= j /\ j <= &(SUC n) /\ P(j)) <=>
1162      (?j. &1 <= j /\ j <= &n /\ P(j)) \/ P(&(SUC n))`,
1163     REWRITE_TAC[GSYM INT_OF_NUM_SUC] THEN
1164     REWRITE_TAC[INT_ARITH `x <= y + &1 <=> (x = y + &1) \/ x < y + &1`] THEN
1165     REWRITE_TAC[INT_LT_DISCRETE; INT_LE_RADD] THEN
1166     MESON_TAC[INT_ARITH `&0 <= x ==> &1 <= x + &1`; INT_POS; INT_LE_REFL]) in
1167   let base_conv = REWR_CONV pth_base
1168   and step_conv =
1169    BINDER_CONV(RAND_CONV(LAND_CONV(funpow 2 RAND_CONV num_CONV))) THENC
1170    REWR_CONV pth_step THENC
1171    RAND_CONV(ONCE_DEPTH_CONV NUM_SUC_CONV) in
1172   let rec conv tm =
1173     try base_conv tm with Failure _ ->
1174     (step_conv THENC LAND_CONV conv) tm in
1175   conv;;
1176
1177 (* ------------------------------------------------------------------------- *)
1178 (* Canonicalize "t + c" in all "interp (t + c) P"s assuming t is canonical.  *)
1179 (* ------------------------------------------------------------------------- *)
1180
1181 let CANON_INTERP_ADD =
1182   let pat = `interp (t + c) P` in
1183   fun vars ->
1184     let net = net_of_conv pat (LAND_CONV(POLYNOMIAL_ADD_CONV vars))
1185               empty_net in
1186     ONCE_DEPTH_CONV(REWRITES_CONV net);;
1187
1188 (* ------------------------------------------------------------------------- *)
1189 (* Conversion to evaluate constant expressions.                              *)
1190 (* ------------------------------------------------------------------------- *)
1191
1192 let EVAL_CONSTANT_CONV =
1193   let net =
1194       itlist (uncurry net_of_conv)
1195        ([`x < y`,INT_LT_CONV;
1196          `x > y`,INT_GT_CONV;
1197          `x:int = y`,INT_EQ_CONV;
1198          `x divides y`,INT_DIVIDES_CONV] @
1199         map (fun t -> t,REWR_CONV(REWRITE_CONV[] t))
1200             [`~F`; `~T`; `a /\ T`; `T /\ a`; `a /\ F`; `F /\ a`;
1201              `a \/ T`; `T \/ a`; `a \/ F`; `F \/ a`])
1202       empty_net in
1203     DEPTH_CONV(REWRITES_CONV net);;
1204
1205 (* ------------------------------------------------------------------------- *)
1206 (* Basic quantifier elimination conversion.                                  *)
1207 (* ------------------------------------------------------------------------- *)
1208
1209 let BASIC_COOPER_CONV =
1210   let p_tm = `p:cform`
1211   and d_tm = `d:int` in
1212   let pth_B = SPECL [p_tm; d_tm] MAINTHM_B in
1213   fun vars tm ->
1214     let x,bod = dest_exists tm in
1215     let th1 = (NORMALIZE_COEFF_CONV vars THENC SHADOW_CONV) tm in
1216     let p = rand(snd(dest_exists(rand(concl th1)))) in
1217     let th2 = INST [p,p_tm; mk_int_const(dplcm p),d_tm] pth_B in
1218     let tm2a,tm2b = dest_conj(lhand(concl th2)) in
1219     let th3 =
1220       CONJ (EQT_ELIM(ALLDIVIDE_CONV tm2a)) (EQT_ELIM(INT_LT_CONV tm2b)) in
1221     let th4 = TRANS th1 (MP th2 th3) in
1222     let th5 = CONV_RULE(RAND_CONV(BINDER_CONV(funpow 2 RAND_CONV(LAND_CONV
1223                         MINUSINF_CONV)))) th4 in
1224     let th6 = CONV_RULE(RAND_CONV(BINDER_CONV(funpow 3 RAND_CONV
1225                         (EXISTS_IN_BSET_CONV vars)))) th5 in
1226     let th7 = CONV_RULE(RAND_CONV EXPAND_INT_CASES_CONV) th6 in
1227     let th8 = CONV_RULE(RAND_CONV(CANON_INTERP_ADD vars)) th7 in
1228     let th9 = CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV(INTERP_CONV vars))) th8 in
1229     CONV_RULE(RAND_CONV EVAL_CONSTANT_CONV) th9;;
1230
1231 (* ------------------------------------------------------------------------- *)
1232 (* NNF transformation that also eliminates negated inequalities.             *)
1233 (* ------------------------------------------------------------------------- *)
1234
1235 let NNF_POSINEQ_CONV =
1236   let pth = prove
1237    (`(~(&0 < x) <=> &0 < &1 - x) /\
1238      (~(&0 > x) <=> &0 < &1 + x)`,
1239     REWRITE_TAC[INT_NOT_LT; INT_GT] THEN
1240     REWRITE_TAC[INT_LT_DISCRETE; INT_GT_DISCRETE] THEN
1241     INT_ARITH_TAC) in
1242   let conv1 vars = REWR_CONV(CONJUNCT1 pth) THENC
1243                    RAND_CONV (POLYNOMIAL_SUB_CONV vars)
1244   and conv2 vars = REWR_CONV(CONJUNCT2 pth) THENC
1245                    RAND_CONV (POLYNOMIAL_ADD_CONV vars)
1246   and pat1 = `~(&0 < x)` and pat2 = `~(&0 > x)`
1247   and net = itlist (fun t -> net_of_conv (lhand t) (REWR_CONV(TAUT t)))
1248                    [`~(~ p) <=> p`; `~(p /\ q) <=> ~p \/ ~q`;
1249                     `~(p \/ q) <=> ~p /\ ~q`] empty_net in
1250   fun vars ->
1251    let net' = net_of_conv pat1 (conv1 vars)
1252                (net_of_conv pat2 (conv2 vars) net) in
1253    TOP_SWEEP_CONV(REWRITES_CONV net');;
1254
1255 (* ------------------------------------------------------------------------- *)
1256 (* Overall function.                                                         *)
1257 (* ------------------------------------------------------------------------- *)
1258
1259 let COOPER_CONV =
1260   let FORALL_ELIM_CONV = GEN_REWRITE_CONV I
1261    [prove(`(!x. P x) <=> ~(?x. ~(P x))`,MESON_TAC[])]
1262   and not_tm = `(~)` in
1263   let rec conv vars tm =
1264     if is_conj tm or is_disj tm then
1265       let lop,r = dest_comb tm in
1266       let op,l = dest_comb lop in
1267       MK_COMB(AP_TERM op (conv vars l),conv vars r)
1268     else if is_neg tm then
1269       let l,r = dest_comb tm in
1270       AP_TERM l (conv vars r)
1271     else if is_exists tm then
1272       let x,bod = dest_exists tm in
1273       let th1 = MK_EXISTS x (conv (x::vars) bod) in
1274       TRANS th1 (BASIC_COOPER_CONV vars (rand(concl th1)))
1275     else if is_forall tm then
1276       let x,bod = dest_forall tm in
1277       let th1 = AP_TERM not_tm (conv (x::vars) bod) in
1278       let th2 = CONV_RULE(RAND_CONV (NNF_POSINEQ_CONV (x::vars))) th1 in
1279       let th3 = MK_EXISTS x th2 in
1280       let th4 = CONV_RULE(RAND_CONV (BASIC_COOPER_CONV vars)) th3 in
1281       let th5 = CONV_RULE(RAND_CONV (NNF_POSINEQ_CONV (x::vars)))
1282           (AP_TERM not_tm th4) in
1283       TRANS (FORALL_ELIM_CONV tm) th5
1284     else REFL tm in
1285   let init_CONV =
1286     PRESIMP_CONV THENC
1287     GEN_REWRITE_CONV ONCE_DEPTH_CONV
1288      [INT_ABS;
1289       INT_ARITH `max m n = if m <= n then n else m`;
1290       INT_ARITH `min m n = if m <= n then m else n`] THENC
1291     CONDS_ELIM_CONV THENC NNF_CONV in
1292   fun tm ->
1293     let vars = frees tm in
1294     let th1 = (init_CONV THENC LINEARIZE_CONV vars) tm in
1295     let th2 = TRANS th1 (conv vars (rand(concl th1))) in
1296     TRANS th2 (EVAL_CONSTANT_CONV(rand(concl th2)));;
1297
1298 (* ------------------------------------------------------------------------- *)
1299 (* Examples from the book.                                                   *)
1300 (* ------------------------------------------------------------------------- *)
1301
1302 time COOPER_CONV `!x y. x < y ==> &2 * x + &1 < &2 * y`;;
1303
1304 time COOPER_CONV `!x y. ~(&2 * x + &1 = &2 * y)`;;
1305
1306 time COOPER_CONV
1307    `?x y. x > &0 /\ y >= &0 /\ (&3 * x - &5 * y = &1)`;;
1308
1309 time COOPER_CONV `?x y z. &4 * x - &6 * y = &1`;;
1310
1311 time COOPER_CONV `!x. b < x ==> a <= x`;;
1312
1313 time COOPER_CONV `!x. a < &3 * x ==> b < &3 * x`;;
1314
1315 time COOPER_CONV `!x y. x <= y ==> &2 * x + &1 < &2 * y`;;
1316
1317 time COOPER_CONV `(?d. y = &65 * d) ==> (?d. y = &5 * d)`;;
1318
1319 time COOPER_CONV `!y. (?d. y = &65 * d) ==> (?d. y = &5 * d)`;;
1320
1321 time COOPER_CONV `!x y. ~(&2 * x + &1 = &2 * y)`;;
1322
1323 time COOPER_CONV `!x y z. (&2 * x + &1 = &2 * y) ==> x + y + z > &129`;;
1324
1325 time COOPER_CONV `!x. a < x ==> b < x`;;
1326
1327 time COOPER_CONV `!x. a <= x ==> b < x`;;
1328
1329 (* ------------------------------------------------------------------------- *)
1330 (* Formula examples from Cooper's paper.                                     *)
1331 (* ------------------------------------------------------------------------- *)
1332
1333 time COOPER_CONV `!a b. ?x. a < &20 * x /\ &20 * x < b`;;
1334
1335 time COOPER_CONV `?x. a < &20 * x /\ &20 * x < b`;;
1336
1337 time COOPER_CONV `!b. ?x. a < &20 * x /\ &20 * x < b`;;
1338
1339 time COOPER_CONV `!a. ?b. a < &4 * b + &3 * a \/ (~(a < b) /\ a > b + &1)`;;
1340
1341 time COOPER_CONV `?y. !x. x + &5 * y > &1 /\ &13 * x - y > &1 /\ x + &2 < &0`;;
1342
1343 (* ------------------------------------------------------------------------- *)
1344 (* More of my own.                                                           *)
1345 (* ------------------------------------------------------------------------- *)
1346
1347 time COOPER_CONV `!x y. x >= &0 /\ y >= &0
1348                   ==> &12 * x - &8 * y < &0 \/ &12 * x - &8 * y > &2`;;
1349
1350 time COOPER_CONV `?x y. &5 * x + &3 * y = &1`;;
1351
1352 time COOPER_CONV `?x y. &5 * x + &10 * y = &1`;;
1353
1354 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&5 * x - &6 * y = &1)`;;
1355
1356 time COOPER_CONV `?w x y z. &2 * w + &3 * x + &4 * y + &5 * z = &1`;;
1357
1358 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&5 * x - &3 * y = &1)`;;
1359
1360 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&3 * x - &5 * y = &1)`;;
1361
1362 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&6 * x - &3 * y = &1)`;;
1363
1364 time COOPER_CONV `!x y. ~(x = &0) ==> &5 * y < &6 * x \/ &5 * y > &6 * x`;;
1365
1366 time COOPER_CONV
1367   `!x y. ~(&5 divides x) /\ ~(&6 divides y) ==> ~(&6 * x = &5 * y)`;;
1368
1369 time COOPER_CONV `!x y. ~(&5 divides x) ==> ~(&6 * x = &5 * y)`;;
1370
1371 time COOPER_CONV `!x y. ~(&6 * x = &5 * y)`;;
1372
1373 time COOPER_CONV `!x y. (&6 * x = &5 * y) ==> (?d. y = &3 * d)`;;
1374
1375 time COOPER_CONV `(&6 * x = &5 * y) ==> (?d. y = &3 * d)`;;
1376
1377 (* ------------------------------------------------------------------------- *)
1378 (* Positive variant of the Bezout theorem (see the exercise).                *)
1379 (* ------------------------------------------------------------------------- *)
1380
1381 time COOPER_CONV
1382   `!z. z > &7 ==> ?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = z)`;;
1383
1384 time COOPER_CONV
1385   `!z. z > &2 ==> ?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = z)`;;
1386
1387 time COOPER_CONV `!z. z <= &7 ==>
1388          ((?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = z)) <=>
1389           ~(?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = &7 - z)))`;;
1390
1391 (* ------------------------------------------------------------------------- *)
1392 (* Basic result about congruences.                                           *)
1393 (* ------------------------------------------------------------------------- *)
1394
1395 time COOPER_CONV `!x. ~(&2 divides x) /\ &3 divides (x - &1) <=>
1396                       &12 divides (x - &1) \/ &12 divides (x - &7)`;;
1397
1398 time COOPER_CONV `!x. ~(?m. x = &2 * m) /\ (?m. x = &3 * m + &1) <=>
1399                      (?m. x = &12 * m + &1) \/ (?m. x = &12 * m + &7)`;;
1400
1401 (* ------------------------------------------------------------------------- *)
1402 (* Something else.                                                           *)
1403 (* ------------------------------------------------------------------------- *)
1404
1405 time COOPER_CONV
1406  `!x. ~(&2 divides x)
1407       ==> &4 divides (x - &1) \/
1408           &8 divides (x - &1) \/
1409           &8 divides (x - &3) \/
1410           &6 divides (x - &1) \/
1411           &14 divides (x - &1) \/
1412           &14 divides (x - &9) \/
1413           &14 divides (x - &11) \/
1414           &24 divides (x - &5) \/
1415           &24 divides (x - &11)`;;
1416
1417 (* ------------------------------------------------------------------------- *)
1418 (* Testing fix for an earlier version with negative result from formlcm.     *)
1419 (* ------------------------------------------------------------------------- *)
1420
1421 time COOPER_CONV
1422  `!a b v_1 v_2 v_3.
1423     (a + &2 = b) /\ (v_3 = b - a + &1) /\ (v_2 = b - &2) /\ (v_1 = &3) ==> F`;;
1424
1425 (* ------------------------------------------------------------------------- *)
1426 (* Inspired by the Collatz conjecture.                                       *)
1427 (* ------------------------------------------------------------------------- *)
1428
1429 time COOPER_CONV
1430  `?a b. ~(a = &1) /\ ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1431               (a = b)`;;
1432
1433 time COOPER_CONV
1434  `?a b. a > &1 /\ b > &1 /\
1435              ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1436              (a = b)`;;
1437
1438 time COOPER_CONV
1439  `?b. a > &1 /\ b > &1 /\
1440       ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1441       ((&2 * a = b) \/ (&2 * a = &3 * b + &1))`;;
1442
1443 (*************** These seem to take a long time
1444
1445 time COOPER_CONV
1446  `?a b. a > &1 /\ b > &1 /\
1447              ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1448              ((&2 * a = b) \/ (&2 * a = &3 * b + &1))`;;
1449
1450 let fm = (dnf ** parse)
1451  `((2 * b = a) \/ (2 * b = &3 * a + 1)) /\
1452   ((2 * c = b) \/ (2 * c = &3 * b + 1)) /\
1453   ((2 * d = c) \/ (2 * d = &3 * c + 1)) /\
1454   ((2 * e = d) \/ (2 * e = &3 * d + 1)) /\
1455   ((2 * f = e) \/ (2 * f = &3 * e + 1)) /\
1456   (f = a)`;;
1457
1458 let fms =
1459   map (itlist (fun x p -> Exists(x,And(Atom(R(`>`,[Var x; Fn(`1`,[])])),p)))
1460               [`b`; `c`; `d`; `e`; `f`])
1461       (disjuncts fm);;
1462
1463 let fm = el &15 fms;;
1464 integer_qelim fm;;
1465
1466 ******************)
1467
1468 (* ------------------------------------------------------------------------- *)
1469 (* More old examples.                                                        *)
1470 (* ------------------------------------------------------------------------- *)
1471
1472 time COOPER_CONV
1473  `?x. &5 * x + x + x < x \/
1474       (y = &7 - x) /\ &33 + z < x /\ x + &1 <= &2 * y \/
1475       &3 divides &4 * x + z /\ (x + y + z = &7 * z)`;;
1476
1477 time COOPER_CONV
1478  `?x. &5 * x + x + x < x \/
1479       (y = &7 - x) /\
1480       &33 + z < x /\
1481       x + &1 <= &2 * y \/
1482       &3 divides (&4 * x + z) /\
1483       (x + y + z = &7 * z)`;;
1484
1485 time COOPER_CONV
1486  `?x. &5 * x + x + x < x \/
1487       (y = &7 - x) /\
1488       &33 + z < x /\
1489       x + &1 <= &2 * y \/
1490       &3 divides (&4 * x + z) /\
1491       (x + y + z = &7 * z)`;;
1492
1493 (**** This also seems very slow; one quantifier less maybe?
1494
1495 time COOPER_CONV
1496  `?z y x. &5 * x + x + x < x \/
1497           (y = &7 - x) /\
1498           &33 + z < x /\
1499           x + &1 <= &2 * y \/
1500           &3 divides (&4 * x + z) /\
1501           (x + y + z = &7 * z)`;;
1502
1503 time COOPER_CONV
1504  `?y x. &5 * x + x + x < x \/
1505         (y = &7 - x) /\
1506         &33 + z < x /\
1507         x + &1 <= &2 * y \/
1508         &3 divides (&4 * x + z) /\
1509         (x + y + z = &7 * z)`;;
1510
1511 *****)
1512
1513 time COOPER_CONV
1514      `?x. x + &1 < &2 * y /\
1515           &3 divides (&4 * x + z) /\
1516           (&6 * x + y + z = &7 * z)`;;
1517
1518 time COOPER_CONV
1519      `?x. &5 * x + x + x < x \/
1520           (y = &7 - x) /\
1521           &33 + z < x /\
1522           x + &1 < &2 * y \/
1523           &3 divides (&4 * x + z) /\
1524           (x + y + z = &7 * z)`;;
1525
1526 (* ------------------------------------------------------------------------- *)
1527 (* Stamp problem.                                                            *)
1528 (* ------------------------------------------------------------------------- *)
1529
1530 time COOPER_CONV `!x. x >= &8 ==> ?u v. u >= &0 /\ v >= &0 /\
1531                                          (x = &3 * u + &5 * v)`;;
1532
1533 time COOPER_CONV `!x. x >= &10 ==> ?u v. u >= &0 /\ v >= &0 /\
1534                                          (x = &3 * u + &7 * v)`;;
1535
1536 time COOPER_CONV `!x. x >= &30 ==> ?u v. u >= &0 /\ v >= &0 /\
1537                                          (x = &3 * u + &7 * v)`;;
1538
1539 (* ------------------------------------------------------------------------- *)
1540 (* Decision procedures in the style of INT_ARITH and ARITH_RULE.             *)
1541 (*                                                                           *)
1542 (* Really I should locate the free alien subterms.                           *)
1543 (* ------------------------------------------------------------------------- *)
1544
1545 let INT_COOPER tm =
1546   let fvs = frees tm in
1547   let tm' = list_mk_forall(fvs,tm) in
1548   SPECL fvs (EQT_ELIM(COOPER_CONV tm'));;
1549
1550 let COOPER_RULE tm =
1551   let fvs = frees tm in
1552   let tm' = list_mk_forall(fvs,tm) in
1553   let th = (NUM_TO_INT_CONV THENC COOPER_CONV) tm' in
1554   SPECL fvs (EQT_ELIM th);;
1555
1556 (* ------------------------------------------------------------------------- *)
1557 (* Examples.                                                                 *)
1558 (* ------------------------------------------------------------------------- *)
1559
1560 time INT_COOPER `abs(x) < &1 ==> (x = &0)`;;
1561
1562 time COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
1563
1564 time COOPER_RULE `!n. EVEN(n) ==> (2 * n DIV 2 = n)`;;
1565
1566 time COOPER_RULE `!n. ODD n <=> 2 * n DIV 2 < n`;;
1567
1568 (**** This seems quite slow (maybe not very) as well
1569 time COOPER_RULE `n DIV 3 <= n DIV 2`;;
1570  ****)
1571
1572 (*** This one too?
1573 time COOPER_RULE `!x. ?y. if EVEN x then x = 2 * y else x = 2 * (y - 1) + 1`;;
1574  ***)
1575
1576 time COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;