1 (* ========================================================================= *)
2 (* Implementation of Cooper's algorithm via proforma theorems. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* Basic syntax on integer terms. *)
9 (* ------------------------------------------------------------------------- *)
11 let dest_mul = dest_binop `(*)`;;
12 let dest_add = dest_binop `(+)`;;
14 (* ------------------------------------------------------------------------- *)
16 (* ------------------------------------------------------------------------- *)
18 parse_as_infix("divides",(12,"right"));;
20 let divides = new_definition
21 `a divides b <=> ?x. b = a * x`;;
23 (* ------------------------------------------------------------------------- *)
24 (* Trivial lemmas about integers. *)
25 (* ------------------------------------------------------------------------- *)
28 (`!a b. ?c. !x. x < c ==> x < a /\ x < b`,
29 MESON_TAC[INT_LE_TOTAL; INT_LET_TRANS]);;
31 (* ------------------------------------------------------------------------- *)
32 (* Trivial lemmas about divisibility. *)
33 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
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`]);;
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`]);;
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`]);;
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]);;
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]);;
64 (* ------------------------------------------------------------------------- *)
65 (* More specialized lemmas (see footnotes on p4 and p5). *)
66 (* ------------------------------------------------------------------------- *)
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`]);;
73 let INT_MOD_LEMMA = prove
74 (`!d x. &0 < d ==> ?c. &1 <= x + c * d /\ x + c * d <= d`,
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]);;
99 (* ------------------------------------------------------------------------- *)
100 (* Shadow for restricted class of formulas. *)
101 (* ------------------------------------------------------------------------- *)
103 let cform_INDUCT,cform_RECURSION = define_type
114 (* ------------------------------------------------------------------------- *)
115 (* Interpretation of a cform. *)
116 (* ------------------------------------------------------------------------- *)
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)`;;
129 (* ------------------------------------------------------------------------- *)
130 (* The "minus infinity" and "plus infinity" variants. *)
131 (* ------------------------------------------------------------------------- *)
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)`;;
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)`;;
155 (* ------------------------------------------------------------------------- *)
156 (* All the "dividing" things divide the given constant (e.g. their LCM). *)
157 (* ------------------------------------------------------------------------- *)
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)`;;
170 (* ------------------------------------------------------------------------- *)
171 (* A-sets and B-sets. *)
172 (* ------------------------------------------------------------------------- *)
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) = {})`;;
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) = {})`;;
196 (* ------------------------------------------------------------------------- *)
197 (* The key minimality case analysis for the integers. *)
198 (* ------------------------------------------------------------------------- *)
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;
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
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
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)`]);;
219 (* ------------------------------------------------------------------------- *)
220 (* Lemmas towards the main theorems (following my book). *)
221 (* ------------------------------------------------------------------------- *)
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
228 `(a /\ b /\ c /\ d) /\ (e /\ f) ==> a /\ b /\ c /\ d /\ e /\ f`) THEN
230 [MESON_TAC[INT_ARITH `x < --a ==> x + a < &0`; INT_GT;
231 INT_LT_ANTISYM; INT_LT_REFL];
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[]);;
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]);;
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]);;
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
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
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);;
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
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];
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
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[]);;
309 (* ------------------------------------------------------------------------- *)
310 (* Deduce the other one by a symmetry argument rather than a similar proof. *)
311 (* ------------------------------------------------------------------------- *)
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)`;;
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);;
329 let INTERP_MIRROR = prove
330 (`!p x. interp x (mirror p) <=> interp (--x) p`,
331 MESON_TAC[INTERP_MIRROR_LEMMA; INT_NEG_NEG]);;
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);;
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]);;
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]);;
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]);;
352 let EXISTS_NEG = prove
353 (`(?x. P(--x)) <=> (?x. P(x))`,
354 MESON_TAC[INT_NEG_NEG]);;
356 let FORALL_NEG = prove
357 (`(!x. P(--x)) <=> (!x. P x)`,
358 MESON_TAC[INT_NEG_NEG]);;
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
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
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
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]);;
407 (* ------------------------------------------------------------------------- *)
408 (* Proforma for elimination of coefficient of main variable. *)
409 (* ------------------------------------------------------------------------- *)
411 let EXISTS_MULTIPLE_THM_1 = prove
412 (`(?x. P(&1 * x)) <=> ?x. P(x)`,
413 REWRITE_TAC[INT_MUL_LID]);;
415 let EXISTS_MULTIPLE_THM = prove
416 (`(?x. P(c * x)) <=> ?x. c divides x /\ P(x)`,
417 MESON_TAC[divides]);;
419 (* ------------------------------------------------------------------------- *)
420 (* Ordering of variables determined by a list, *with* trivial default. *)
421 (* ------------------------------------------------------------------------- *)
423 let rec earlier vars x y =
425 z::ovs -> if z = y then false
426 else if z = x then true
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 (* ------------------------------------------------------------------------- *)
437 fun tm -> try let l,r = dest_comb tm in
438 l = ptm & is_numeral r
439 with Failure _ -> false;;
441 let mk_num_const,dest_num_const =
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");;
452 try let l,r = dest_comb tm in
453 l = ptm & is_num_const r
454 with Failure _ -> false;;
456 let mk_int_const,dest_int_const =
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);;
464 (* ------------------------------------------------------------------------- *)
465 (* Similar tweaks of all the REAL_INT_..._CONV arith convs in real.ml *)
466 (* ------------------------------------------------------------------------- *)
468 let INT_LE_CONV,INT_LT_CONV,
469 INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV =
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
475 COMB2_CONV (RAND_CONV NUM_EQ_CONV) NUM_EQ_CONV THENC
476 GEN_REWRITE_CONV I [tth] in
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
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
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
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
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;;
545 REWRITE_TAC[INT_NEG_NEG; INT_NEG_0]) in
546 GEN_REWRITE_CONV I [pth];;
551 (&0 * --(&x) = &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
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)];;
568 let neg_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
574 (`(--(&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
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
600 let m = rand(rand l) and n = rand r in
601 let m' = dest_numeral m and n' = dest_numeral n in
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
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
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
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
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
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
638 with Failure _ -> failwith "INT_ADD_CONV");;
641 GEN_REWRITE_CONV I [INT_SUB] THENC
642 TRY_CONV(RAND_CONV INT_NEG_CONV) THENC
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
652 (`((if T then x:int else y) = x) /\ ((if F then x:int else y) = y)`,
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));;
662 (* ------------------------------------------------------------------------- *)
663 (* Handy utility functions for int arithmetic terms. *)
664 (* ------------------------------------------------------------------------- *)
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 `(-)`;;
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 `(-)`;;
676 (* ------------------------------------------------------------------------- *)
677 (* Instantiate the normalizer. *)
678 (* ------------------------------------------------------------------------- *)
680 let POLYNOMIAL_NORMALIZERS =
682 (`(!x y z. x + (y + z) = (x + y) + z) /\
683 (!x y. x + y = y + x) /\
685 (!x y z. x * (y * z) = (x * y) * z) /\
686 (!x y. x * y = y * x) /\
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)
694 (`(!x. --x = --(&1) * x) /\
695 (!x y. x - y = x + --(&1) * y)`,
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
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);;
707 let POLYNOMIAL_NEG_CONV vars =
708 let cnv,_,_,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
710 let POLYNOMIAL_ADD_CONV vars =
711 let _,cnv,_,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
713 let POLYNOMIAL_SUB_CONV vars =
714 let _,_,cnv,_,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
716 let POLYNOMIAL_MUL_CONV vars =
717 let _,_,_,cnv,_,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
719 let POLYNOMIAL_POW_CONV vars =
720 let _,_,_,_,cnv,_ = POLYNOMIAL_NORMALIZERS vars in cnv;;
722 let POLYNOMIAL_CONV vars =
723 let _,_,_,_,_,cnv = POLYNOMIAL_NORMALIZERS vars in cnv;;
725 (* ------------------------------------------------------------------------- *)
726 (* Slight variants of these functions for procedure below. *)
727 (* ------------------------------------------------------------------------- *)
730 let mul_tm = `(*)` in
732 POLYNOMIAL_MUL_CONV vars (mk_comb(mk_comb(mul_tm,mk_int_const n),tm));;
734 (* ------------------------------------------------------------------------- *)
735 (* Linearize a formula, dealing with non-strict inequalities. *)
736 (* ------------------------------------------------------------------------- *)
739 let rew_conv = GEN_REWRITE_CONV I
740 [CONJ (REFL `c divides e`)
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
764 (* ------------------------------------------------------------------------- *)
765 (* Get the coefficient of x, assumed to be first term, if there at all. *)
766 (* ------------------------------------------------------------------------- *)
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;;
778 (* ------------------------------------------------------------------------- *)
779 (* Find (always positive) LCM of all the multiples of x in formula tm. *)
780 (* ------------------------------------------------------------------------- *)
782 let lcm_num x y = abs_num((x */ y) // gcd_num x y);;
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;;
794 (* ------------------------------------------------------------------------- *)
795 (* Switch from "x [+ ...]" to "&1 * x [+ ...]" to suit later proforma. *)
796 (* ------------------------------------------------------------------------- *)
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
803 if tm = x then conv_0 tm
804 else if is_add tm & lhand tm = x then conv_1 tm
807 (* ------------------------------------------------------------------------- *)
808 (* Adjust all coefficients of x (head variable) to match l in formula tm. *)
809 (* ------------------------------------------------------------------------- *)
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`
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])
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
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
858 if c =/ l then REFL tm else
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
882 let tm2 = rator(rand(concl th3)) in
883 TRANS th3 (AP_TERM tm2 (LINEAR_CMUL vars m t)) in
885 CONV_RULE(funpow 2 RAND_CONV (MULTIPLY_1_CONV vars)) th1
889 (* ------------------------------------------------------------------------- *)
890 (* Now normalize all the x terms to have same coefficient and eliminate it. *)
891 (* ------------------------------------------------------------------------- *)
893 let NORMALIZE_COEFF_CONV =
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;;
907 (* ------------------------------------------------------------------------- *)
908 (* Convert to shadow syntax. *)
909 (* ------------------------------------------------------------------------- *)
912 let pth_trivial = prove
913 (`P = interp x (Nox P)`,
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))`,
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
949 let x,bod = dest_exists tm in
950 MK_EXISTS x (SHADOW_CONV x bod);;
952 (* ------------------------------------------------------------------------- *)
953 (* Get the LCM of the dividing things. *)
954 (* ------------------------------------------------------------------------- *)
957 let divides_tm = `Divides`
958 and ndivides_tm = `Ndivides`
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)
969 (* ------------------------------------------------------------------------- *)
970 (* Conversion for true formulas "(--) &m divides (--) &n". *)
971 (* ------------------------------------------------------------------------- *)
973 let PROVE_DIVIDES_CONV_POS =
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
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)))));;
987 let PROVE_DIVIDES_CONV =
988 GEN_REWRITE_CONV REPEATC [DIVIDES_LNEG; DIVIDES_RNEG] THENC
989 PROVE_DIVIDES_CONV_POS;;
991 (* ------------------------------------------------------------------------- *)
992 (* General version that works for positive and negative. *)
993 (* ------------------------------------------------------------------------- *)
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]]);;
1006 let INT_DIVIDES_POS_CONV =
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];
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;;
1017 let INT_DIVIDES_CONV =
1018 GEN_REWRITE_CONV REPEATC [DIVIDES_LNEG; DIVIDES_RNEG] THENC
1019 INT_DIVIDES_POS_CONV;;
1021 (* ------------------------------------------------------------------------- *)
1022 (* Conversion for "alldivide d p" (which should be true!) *)
1023 (* ------------------------------------------------------------------------- *)
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])
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
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
1055 (* ------------------------------------------------------------------------- *)
1056 (* Conversion for "?b. b IN bset p /\ P b";; *)
1057 (* ------------------------------------------------------------------------- *)
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])
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])
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
1083 LAND_CONV(LAND_CONV(POLYNOMIAL_NEG_CONV 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
1089 itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
1090 (CONJUNCTS pth_false) empty_net in
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
1096 enter [] (lhand(concl pth_add),
1097 let cnv = K (REWR_CONV pth_add) in fun v -> cnv v THENC conv_add v)
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
1103 GEN_REWRITE_CONV DEPTH_CONV [taut] THENC
1104 PURE_REWRITE_CONV [DISJ_ACI] in
1105 fun vars tm -> (baseconv vars THENC finconv) tm;;
1107 (* ------------------------------------------------------------------------- *)
1108 (* Naive conversion for "minusinf p". *)
1109 (* ------------------------------------------------------------------------- *)
1111 let MINUSINF_CONV = GEN_REWRITE_CONV TOP_SWEEP_CONV [minusinf];;
1113 (* ------------------------------------------------------------------------- *)
1114 (* Conversion for "interp s p" where s is a canonical linear form. *)
1115 (* ------------------------------------------------------------------------- *)
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
1137 itlist (fun th -> enter [] (lhand(concl th),K (REWR_CONV th)))
1138 (CONJUNCTS pth_trivial) empty_net in
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
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
1152 (* ------------------------------------------------------------------------- *)
1153 (* Expand `?j. &1 <= j /\ j <= &[n] /\ P[j]` cases. *)
1154 (* ------------------------------------------------------------------------- *)
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
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
1173 try base_conv tm with Failure _ ->
1174 (step_conv THENC LAND_CONV conv) tm in
1177 (* ------------------------------------------------------------------------- *)
1178 (* Canonicalize "t + c" in all "interp (t + c) P"s assuming t is canonical. *)
1179 (* ------------------------------------------------------------------------- *)
1181 let CANON_INTERP_ADD =
1182 let pat = `interp (t + c) P` in
1184 let net = net_of_conv pat (LAND_CONV(POLYNOMIAL_ADD_CONV vars))
1186 ONCE_DEPTH_CONV(REWRITES_CONV net);;
1188 (* ------------------------------------------------------------------------- *)
1189 (* Conversion to evaluate constant expressions. *)
1190 (* ------------------------------------------------------------------------- *)
1192 let EVAL_CONSTANT_CONV =
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`])
1203 DEPTH_CONV(REWRITES_CONV net);;
1205 (* ------------------------------------------------------------------------- *)
1206 (* Basic quantifier elimination conversion. *)
1207 (* ------------------------------------------------------------------------- *)
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
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
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;;
1231 (* ------------------------------------------------------------------------- *)
1232 (* NNF transformation that also eliminates negated inequalities. *)
1233 (* ------------------------------------------------------------------------- *)
1235 let NNF_POSINEQ_CONV =
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
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
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');;
1255 (* ------------------------------------------------------------------------- *)
1256 (* Overall function. *)
1257 (* ------------------------------------------------------------------------- *)
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
1287 GEN_REWRITE_CONV ONCE_DEPTH_CONV
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
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)));;
1298 (* ------------------------------------------------------------------------- *)
1299 (* Examples from the book. *)
1300 (* ------------------------------------------------------------------------- *)
1302 time COOPER_CONV `!x y. x < y ==> &2 * x + &1 < &2 * y`;;
1304 time COOPER_CONV `!x y. ~(&2 * x + &1 = &2 * y)`;;
1307 `?x y. x > &0 /\ y >= &0 /\ (&3 * x - &5 * y = &1)`;;
1309 time COOPER_CONV `?x y z. &4 * x - &6 * y = &1`;;
1311 time COOPER_CONV `!x. b < x ==> a <= x`;;
1313 time COOPER_CONV `!x. a < &3 * x ==> b < &3 * x`;;
1315 time COOPER_CONV `!x y. x <= y ==> &2 * x + &1 < &2 * y`;;
1317 time COOPER_CONV `(?d. y = &65 * d) ==> (?d. y = &5 * d)`;;
1319 time COOPER_CONV `!y. (?d. y = &65 * d) ==> (?d. y = &5 * d)`;;
1321 time COOPER_CONV `!x y. ~(&2 * x + &1 = &2 * y)`;;
1323 time COOPER_CONV `!x y z. (&2 * x + &1 = &2 * y) ==> x + y + z > &129`;;
1325 time COOPER_CONV `!x. a < x ==> b < x`;;
1327 time COOPER_CONV `!x. a <= x ==> b < x`;;
1329 (* ------------------------------------------------------------------------- *)
1330 (* Formula examples from Cooper's paper. *)
1331 (* ------------------------------------------------------------------------- *)
1333 time COOPER_CONV `!a b. ?x. a < &20 * x /\ &20 * x < b`;;
1335 time COOPER_CONV `?x. a < &20 * x /\ &20 * x < b`;;
1337 time COOPER_CONV `!b. ?x. a < &20 * x /\ &20 * x < b`;;
1339 time COOPER_CONV `!a. ?b. a < &4 * b + &3 * a \/ (~(a < b) /\ a > b + &1)`;;
1341 time COOPER_CONV `?y. !x. x + &5 * y > &1 /\ &13 * x - y > &1 /\ x + &2 < &0`;;
1343 (* ------------------------------------------------------------------------- *)
1344 (* More of my own. *)
1345 (* ------------------------------------------------------------------------- *)
1347 time COOPER_CONV `!x y. x >= &0 /\ y >= &0
1348 ==> &12 * x - &8 * y < &0 \/ &12 * x - &8 * y > &2`;;
1350 time COOPER_CONV `?x y. &5 * x + &3 * y = &1`;;
1352 time COOPER_CONV `?x y. &5 * x + &10 * y = &1`;;
1354 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&5 * x - &6 * y = &1)`;;
1356 time COOPER_CONV `?w x y z. &2 * w + &3 * x + &4 * y + &5 * z = &1`;;
1358 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&5 * x - &3 * y = &1)`;;
1360 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&3 * x - &5 * y = &1)`;;
1362 time COOPER_CONV `?x y. x >= &0 /\ y >= &0 /\ (&6 * x - &3 * y = &1)`;;
1364 time COOPER_CONV `!x y. ~(x = &0) ==> &5 * y < &6 * x \/ &5 * y > &6 * x`;;
1367 `!x y. ~(&5 divides x) /\ ~(&6 divides y) ==> ~(&6 * x = &5 * y)`;;
1369 time COOPER_CONV `!x y. ~(&5 divides x) ==> ~(&6 * x = &5 * y)`;;
1371 time COOPER_CONV `!x y. ~(&6 * x = &5 * y)`;;
1373 time COOPER_CONV `!x y. (&6 * x = &5 * y) ==> (?d. y = &3 * d)`;;
1375 time COOPER_CONV `(&6 * x = &5 * y) ==> (?d. y = &3 * d)`;;
1377 (* ------------------------------------------------------------------------- *)
1378 (* Positive variant of the Bezout theorem (see the exercise). *)
1379 (* ------------------------------------------------------------------------- *)
1382 `!z. z > &7 ==> ?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = z)`;;
1385 `!z. z > &2 ==> ?x y. x >= &0 /\ y >= &0 /\ (&3 * x + &5 * y = z)`;;
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)))`;;
1391 (* ------------------------------------------------------------------------- *)
1392 (* Basic result about congruences. *)
1393 (* ------------------------------------------------------------------------- *)
1395 time COOPER_CONV `!x. ~(&2 divides x) /\ &3 divides (x - &1) <=>
1396 &12 divides (x - &1) \/ &12 divides (x - &7)`;;
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)`;;
1401 (* ------------------------------------------------------------------------- *)
1402 (* Something else. *)
1403 (* ------------------------------------------------------------------------- *)
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)`;;
1417 (* ------------------------------------------------------------------------- *)
1418 (* Testing fix for an earlier version with negative result from formlcm. *)
1419 (* ------------------------------------------------------------------------- *)
1423 (a + &2 = b) /\ (v_3 = b - a + &1) /\ (v_2 = b - &2) /\ (v_1 = &3) ==> F`;;
1425 (* ------------------------------------------------------------------------- *)
1426 (* Inspired by the Collatz conjecture. *)
1427 (* ------------------------------------------------------------------------- *)
1430 `?a b. ~(a = &1) /\ ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1434 `?a b. a > &1 /\ b > &1 /\
1435 ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1439 `?b. a > &1 /\ b > &1 /\
1440 ((&2 * b = a) \/ (&2 * b = &3 * a + &1)) /\
1441 ((&2 * a = b) \/ (&2 * a = &3 * b + &1))`;;
1443 (*************** These seem to take a long time
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))`;;
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)) /\
1459 map (itlist (fun x p -> Exists(x,And(Atom(R(`>`,[Var x; Fn(`1`,[])])),p)))
1460 [`b`; `c`; `d`; `e`; `f`])
1463 let fm = el &15 fms;;
1468 (* ------------------------------------------------------------------------- *)
1469 (* More old examples. *)
1470 (* ------------------------------------------------------------------------- *)
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)`;;
1478 `?x. &5 * x + x + x < x \/
1482 &3 divides (&4 * x + z) /\
1483 (x + y + z = &7 * z)`;;
1486 `?x. &5 * x + x + x < x \/
1490 &3 divides (&4 * x + z) /\
1491 (x + y + z = &7 * z)`;;
1493 (**** This also seems very slow; one quantifier less maybe?
1496 `?z y x. &5 * x + x + x < x \/
1500 &3 divides (&4 * x + z) /\
1501 (x + y + z = &7 * z)`;;
1504 `?y x. &5 * x + x + x < x \/
1508 &3 divides (&4 * x + z) /\
1509 (x + y + z = &7 * z)`;;
1514 `?x. x + &1 < &2 * y /\
1515 &3 divides (&4 * x + z) /\
1516 (&6 * x + y + z = &7 * z)`;;
1519 `?x. &5 * x + x + x < x \/
1523 &3 divides (&4 * x + z) /\
1524 (x + y + z = &7 * z)`;;
1526 (* ------------------------------------------------------------------------- *)
1527 (* Stamp problem. *)
1528 (* ------------------------------------------------------------------------- *)
1530 time COOPER_CONV `!x. x >= &8 ==> ?u v. u >= &0 /\ v >= &0 /\
1531 (x = &3 * u + &5 * v)`;;
1533 time COOPER_CONV `!x. x >= &10 ==> ?u v. u >= &0 /\ v >= &0 /\
1534 (x = &3 * u + &7 * v)`;;
1536 time COOPER_CONV `!x. x >= &30 ==> ?u v. u >= &0 /\ v >= &0 /\
1537 (x = &3 * u + &7 * v)`;;
1539 (* ------------------------------------------------------------------------- *)
1540 (* Decision procedures in the style of INT_ARITH and ARITH_RULE. *)
1542 (* Really I should locate the free alien subterms. *)
1543 (* ------------------------------------------------------------------------- *)
1546 let fvs = frees tm in
1547 let tm' = list_mk_forall(fvs,tm) in
1548 SPECL fvs (EQT_ELIM(COOPER_CONV tm'));;
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);;
1556 (* ------------------------------------------------------------------------- *)
1558 (* ------------------------------------------------------------------------- *)
1560 time INT_COOPER `abs(x) < &1 ==> (x = &0)`;;
1562 time COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
1564 time COOPER_RULE `!n. EVEN(n) ==> (2 * n DIV 2 = n)`;;
1566 time COOPER_RULE `!n. ODD n <=> 2 * n DIV 2 < n`;;
1568 (**** This seems quite slow (maybe not very) as well
1569 time COOPER_RULE `n DIV 3 <= n DIV 2`;;
1573 time COOPER_RULE `!x. ?y. if EVEN x then x = 2 * y else x = 2 * (y - 1) + 1`;;
1576 time COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;