Update from HH
[hl193./.git] / 100 / four_squares.ml
1 (* ========================================================================= *)
2 (* Theorems about representations as sums of 2 and 4 squares.                *)
3 (* ========================================================================= *)
4
5 needs "Library/prime.ml";;
6 needs "Library/analysis.ml";; (*** only for REAL_ARCH_LEAST! ***)
7
8 prioritize_num();;
9
10 (* ------------------------------------------------------------------------- *)
11 (* Definition of involution and various basic lemmas.                        *)
12 (* ------------------------------------------------------------------------- *)
13
14 let involution = new_definition
15   `involution f s = !x. x IN s ==> f(x) IN s /\ (f(f(x)) = x)`;;
16
17 let INVOLUTION_IMAGE = prove
18  (`!f s. involution f s ==> (IMAGE f s = s)`,
19   REWRITE_TAC[involution; EXTENSION; IN_IMAGE] THEN MESON_TAC[]);;
20
21 let INVOLUTION_DELETE = prove
22  (`involution f s /\ a IN s /\ (f a = a) ==> involution f (s DELETE a)`,
23   REWRITE_TAC[involution; IN_DELETE] THEN MESON_TAC[]);;
24
25 let INVOLUTION_STEPDOWN = prove
26  (`involution f s /\ a IN s ==> involution f (s DIFF {a, (f a)})`,
27   REWRITE_TAC[involution; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]);;
28
29 let INVOLUTION_NOFIXES = prove
30  (`involution f s ==> involution f {x | x IN s /\ ~(f x = x)}`,
31   REWRITE_TAC[involution; IN_ELIM_THM] THEN MESON_TAC[]);;
32
33 let INVOLUTION_SUBSET = prove
34  (`!f s t. involution f s /\ (!x. x IN t ==> f(x) IN t) /\ t SUBSET s
35            ==> involution f t`,
36   REWRITE_TAC[involution; SUBSET] THEN MESON_TAC[]);;
37
38 (* ------------------------------------------------------------------------- *)
39 (* Involution with no fixpoints can only occur on finite set of even card    *)
40 (* ------------------------------------------------------------------------- *)
41
42 let INVOLUTION_EVEN_STEP = prove
43  (`FINITE(s) /\
44    involution f s /\
45    (!x:A. x IN s ==> ~(f x = x)) /\
46    a IN s
47    ==> FINITE(s DIFF {a, (f a)}) /\
48        involution f (s DIFF {a, (f a)}) /\
49        (!x:A. x IN (s DIFF {a, (f a)}) ==> ~(f x = x)) /\
50        (CARD s = CARD(s DIFF {a, (f a)}) + 2)`,
51   SIMP_TAC[FINITE_DIFF; INVOLUTION_STEPDOWN; IN_DIFF] THEN STRIP_TAC THEN
52   SUBGOAL_THEN `s = (a:A) INSERT (f a) INSERT (s DIFF {a, (f a)})` MP_TAC THENL
53    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN
54     ASM_MESON_TAC[involution]; ALL_TAC] THEN
55   DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
56   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DIFF; FINITE_INSERT] THEN
57   ASM_SIMP_TAC[IN_INSERT; IN_DIFF; NOT_IN_EMPTY] THEN ARITH_TAC);;
58
59 let INVOLUTION_EVEN_INDUCT = prove
60  (`!n s. FINITE(s) /\ (CARD s = n) /\ involution f s /\
61          (!x:A. x IN s ==> ~(f x = x))
62          ==> EVEN(CARD s)`,
63   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
64   ASM_CASES_TAC `s:A->bool = {}` THEN
65   ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
66   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [EXTENSION]) THEN
67   REWRITE_TAC[NOT_IN_EMPTY; NOT_FORALL_THM] THEN
68   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN STRIP_TAC THEN
69   FIRST_X_ASSUM(MP_TAC o SPEC `CARD(s DIFF {a:A, (f a)})`) THEN
70   REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
71   DISCH_THEN(MP_TAC o SPEC `s DIFF {a:A, (f a)}`) THEN
72   MP_TAC INVOLUTION_EVEN_STEP THEN ASM_REWRITE_TAC[] THEN
73   STRIP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `n < n + 2`] THEN
74   SIMP_TAC[EVEN_ADD; ARITH]);;
75
76 let INVOLUTION_EVEN = prove
77  (`!s. FINITE(s) /\ involution f s /\ (!x:A. x IN s ==> ~(f x = x))
78        ==> EVEN(CARD s)`,
79   MESON_TAC[INVOLUTION_EVEN_INDUCT]);;
80
81 (* ------------------------------------------------------------------------- *)
82 (* So an involution with exactly one fixpoint has odd card domain.           *)
83 (* ------------------------------------------------------------------------- *)
84
85 let INVOLUTION_FIX_ODD = prove
86  (`FINITE(s) /\ involution f s /\ (?!a:A. a IN s /\ (f a = a))
87    ==> ODD(CARD s)`,
88   REWRITE_TAC[EXISTS_UNIQUE_DEF] THEN STRIP_TAC THEN
89   SUBGOAL_THEN `s = (a:A) INSERT (s DELETE a)` SUBST1_TAC THENL
90    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[];
91     ALL_TAC] THEN
92   ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; IN_DELETE; ODD; NOT_ODD] THEN
93   MATCH_MP_TAC INVOLUTION_EVEN THEN
94   ASM_SIMP_TAC[INVOLUTION_DELETE; FINITE_DELETE; IN_DELETE] THEN
95   ASM_MESON_TAC[]);;
96
97 (* ------------------------------------------------------------------------- *)
98 (* And an involution on a set of odd finite card must have a fixpoint.       *)
99 (* ------------------------------------------------------------------------- *)
100
101 let INVOLUTION_ODD = prove
102  (`!n s. FINITE(s) /\ involution f s /\ ODD(CARD s)
103          ==> ?a. a IN s /\ (f a = a)`,
104   REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[INVOLUTION_EVEN]);;
105
106 (* ------------------------------------------------------------------------- *)
107 (* Consequently, if one involution has a unique fixpoint, other has one.     *)
108 (* ------------------------------------------------------------------------- *)
109
110 let INVOLUTION_FIX_FIX = prove
111  (`!f g s. FINITE(s) /\ involution f s /\ involution g s /\
112            (?!x. x IN s /\ (f x = x)) ==> ?x. x IN s /\ (g x = x)`,
113   REPEAT STRIP_TAC THEN MATCH_MP_TAC INVOLUTION_ODD THEN
114   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INVOLUTION_FIX_ODD THEN
115   ASM_REWRITE_TAC[]);;
116
117 (* ------------------------------------------------------------------------- *)
118 (* Formalization of Zagier's "one-sentence" proof over the natural numbers.  *)
119 (* ------------------------------------------------------------------------- *)
120
121 let zset = new_definition
122   `zset(a) = {(x,y,z) | x EXP 2 + 4 * y * z = a}`;;
123
124 let zag = new_definition
125   `zag(x,y,z) =
126         if x + z < y then (x + 2 * z,z,y - (x + z))
127         else if x < 2 * y then (2 * y - x, y, (x + z) - y)
128         else (x - 2 * y,(x + z) - y, y)`;;
129
130 let tag = new_definition
131   `tag((x,y,z):num#num#num) = (x,z,y)`;;
132
133 let ZAG_INVOLUTION_GENERAL = prove
134  (`0 < x /\ 0 < y /\ 0 < z ==> (zag(zag(x,y,z)) = (x,y,z))`,
135   REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
136   REWRITE_TAC[zag] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
137   REWRITE_TAC[PAIR_EQ] THEN
138   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
139
140 let IN_TRIPLE = prove
141  (`(a,b,c) IN {(x,y,z) | P x y z} <=> P a b c`,
142   REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[]);;
143
144 let PRIME_SQUARE = prove
145  (`!n. ~prime(n * n)`,
146   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
147   ASM_REWRITE_TAC[PRIME_0; MULT_CLAUSES] THEN
148   REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
149   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[ARITH] THEN
150   DISJ2_TAC THEN EXISTS_TAC `n:num` THEN
151   ASM_SIMP_TAC[DIVIDES_LMUL; DIVIDES_REFL] THEN
152   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [ARITH_RULE `n = n * 1`] THEN
153   ASM_SIMP_TAC[EQ_MULT_LCANCEL]);;
154
155 let PRIME_4X = prove
156  (`!n. ~prime(4 * n)`,
157   GEN_TAC THEN REWRITE_TAC[prime; NOT_FORALL_THM; DE_MORGAN_THM] THEN
158   DISJ2_TAC THEN EXISTS_TAC `2` THEN
159   SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
160   ASM_SIMP_TAC[GSYM MULT_ASSOC; DIVIDES_RMUL; DIVIDES_REFL; ARITH_EQ] THEN
161   ASM_CASES_TAC `n = 0` THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
162
163 let PRIME_XYZ_NONZERO = prove
164  (`prime(x EXP 2 + 4 * y * z) ==> 0 < x /\ 0 < y /\ 0 < z`,
165   CONV_TAC CONTRAPOS_CONV THEN
166   REWRITE_TAC[DE_MORGAN_THM; ARITH_RULE `~(0 < x) = (x = 0)`] THEN
167   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
168   REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES; PRIME_SQUARE; PRIME_4X]);;
169
170 let ZAG_INVOLUTION = prove
171  (`!p. prime(p) ==> involution zag (zset(p))`,
172   REPEAT STRIP_TAC THEN REWRITE_TAC[involution; FORALL_PAIR_THM] THEN
173   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
174   REWRITE_TAC[zset; IN_TRIPLE] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
175   CONJ_TAC THENL
176    [REWRITE_TAC[zag] THEN REPEAT COND_CASES_TAC THEN
177     ASM_REWRITE_TAC[IN_TRIPLE] THEN
178     RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
179     ASM_SIMP_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_ADD; EXP_2;
180                  GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_SUB; LT_IMP_LE] THEN
181     INT_ARITH_TAC;
182     MATCH_MP_TAC ZAG_INVOLUTION_GENERAL THEN
183     ASM_MESON_TAC[PRIME_XYZ_NONZERO]]);;
184
185 let TAG_INVOLUTION = prove
186  (`!a. involution tag (zset a)`,
187   REWRITE_TAC[involution; tag; zset; FORALL_PAIR_THM] THEN
188   REWRITE_TAC[IN_TRIPLE] THEN REWRITE_TAC[MULT_AC]);;
189
190 let ZAG_LEMMA = prove
191  (`(zag(x,y,z) = (x,y,z)) ==> (y = x)`,
192   REWRITE_TAC[zag; INT_POW_2] THEN
193   REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[PAIR_EQ]) THEN
194   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC);;
195
196 let ZSET_BOUND = prove
197  (`0 < y /\ 0 < z /\ (x EXP 2 + 4 * y * z = p)
198    ==> x <= p /\ y <= p /\ z <= p`,
199   REPEAT GEN_TAC THEN STRIP_TAC THEN
200   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN CONJ_TAC THENL
201    [MESON_TAC[EXP_2; LE_SQUARE_REFL; ARITH_RULE `(a <= b ==> a <= b + c)`];
202     CONJ_TAC THEN MATCH_MP_TAC(ARITH_RULE `y <= z ==> y <= x + z`) THENL
203      [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM]; ALL_TAC] THEN
204     REWRITE_TAC[ARITH_RULE `y <= 4 * a * y <=> 1 * y <= (4 * a) * y`] THEN
205     ASM_REWRITE_TAC[LE_MULT_RCANCEL] THEN
206     ASM_SIMP_TAC[ARITH_RULE `0 < a ==> 1 <= 4 * a`]]);;
207
208 let ZSET_FINITE = prove
209  (`!p. prime(p) ==> FINITE(zset p)`,
210   GEN_TAC THEN DISCH_TAC THEN
211   MP_TAC(SPEC `p + 1` FINITE_NUMSEG_LT) THEN
212   DISCH_THEN(fun th ->
213     MP_TAC(funpow 2 (MATCH_MP FINITE_PRODUCT o CONJ th) th)) THEN
214   MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b ==> c <=> b ==> a ==> c`]
215     FINITE_SUBSET) THEN
216   REWRITE_TAC[zset; SUBSET; FORALL_PAIR_THM; IN_TRIPLE] THEN
217   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN
218   REWRITE_TAC[IN_ELIM_THM; EXISTS_PAIR_THM; PAIR_EQ] THEN
219   REWRITE_TAC[ARITH_RULE `x < p + 1 <=> x <= p`; PAIR_EQ] THEN
220   DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`x:num`; `y:num`; `z:num`] THEN
221   ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
222   MAP_EVERY EXISTS_TAC [`y:num`; `z:num`] THEN REWRITE_TAC[] THEN
223   ASM_MESON_TAC[ZSET_BOUND; PRIME_XYZ_NONZERO]);;
224
225 let SUM_OF_TWO_SQUARES = prove
226  (`!p k. prime(p) /\ (p = 4 * k + 1) ==> ?x y. p = x EXP 2 + y EXP 2`,
227   SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
228   SUBGOAL_THEN `?t. t IN zset(p) /\ (tag(t) = t)` MP_TAC THENL
229    [ALL_TAC;
230     REWRITE_TAC[LEFT_IMP_EXISTS_THM; FORALL_PAIR_THM; tag; PAIR_EQ] THEN
231     REWRITE_TAC[zset; IN_TRIPLE; EXP_2] THEN
232     ASM_MESON_TAC[ARITH_RULE `4 * x * y = (2 * x) * (2 * y)`]] THEN
233   MATCH_MP_TAC INVOLUTION_FIX_FIX THEN EXISTS_TAC `zag` THEN
234   ASM_SIMP_TAC[ZAG_INVOLUTION; TAG_INVOLUTION; ZSET_FINITE] THEN
235   REWRITE_TAC[EXISTS_UNIQUE_ALT] THEN EXISTS_TAC `1,1,k:num` THEN
236   REWRITE_TAC[FORALL_PAIR_THM] THEN
237   MAP_EVERY X_GEN_TAC [`x:num`; `y:num`; `z:num`] THEN EQ_TAC THENL
238    [ALL_TAC;
239     DISCH_THEN(SUBST1_TAC o SYM) THEN
240     REWRITE_TAC[zset; zag; IN_TRIPLE; ARITH] THEN
241     REWRITE_TAC[MULT_CLAUSES; ARITH_RULE `~(1 + k < 1)`; PAIR_EQ] THEN
242     ARITH_TAC] THEN
243   REWRITE_TAC[zset; IN_TRIPLE] THEN STRIP_TAC THEN
244   FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP ZAG_LEMMA) THEN
245   UNDISCH_TAC `x EXP 2 + 4 * x * z = 4 * k + 1` THEN
246   REWRITE_TAC[EXP_2; ARITH_RULE `x * x + 4 * x * z = x * (4 * z + x)`] THEN
247   DISCH_THEN(ASSUME_TAC o SYM) THEN UNDISCH_TAC `prime p` THEN
248   ASM_REWRITE_TAC[] THEN REWRITE_TAC[prime] THEN
249   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:num`)) THEN
250   SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN
251   DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THENL
252    [UNDISCH_TAC `4 * k + 1 = 1 * (4 * z + 1)` THEN
253     REWRITE_TAC[MULT_CLAUSES; PAIR_EQ] THEN ARITH_TAC;
254     ONCE_REWRITE_TAC[ARITH_RULE `(a = a * b) = (a * b = a * 1)`] THEN
255     ASM_SIMP_TAC[EQ_MULT_LCANCEL] THEN STRIP_TAC THENL
256      [UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
257       ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0; ARITH_EQ];
258       UNDISCH_TAC `4 * z + x = 1` THEN REWRITE_TAC[PAIR_EQ] THEN
259       ASM_CASES_TAC `z = 0` THENL
260        [ALL_TAC; UNDISCH_TAC `~(z = 0)` THEN ARITH_TAC] THEN
261       UNDISCH_TAC `4 * k + 1 = x * (4 * z + x)` THEN
262       ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
263       ASM_CASES_TAC `x = 1` THEN ASM_REWRITE_TAC[] THEN
264       REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC]]);;
265
266 (* ------------------------------------------------------------------------- *)
267 (* General pigeonhole lemma.                                                 *)
268 (* ------------------------------------------------------------------------- *)
269
270 let PIGEONHOLE_LEMMA = prove
271  (`!f:A->B g s t.
272         FINITE(s) /\ FINITE(t) /\
273         (!x. x IN s ==> f(x) IN t) /\
274         (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) /\
275         (!x. x IN s ==> g(x) IN t) /\
276         (!x y. x IN s /\ y IN s /\ (g x = g y) ==> (x = y)) /\
277         CARD(t) < 2 * CARD(s)
278         ==> ?x y. x IN s /\ y IN s /\ (f x = g y)`,
279   REPEAT STRIP_TAC THEN
280   MP_TAC(ISPECL [`IMAGE (f:A->B) s`; `IMAGE (g:A->B) s`] CARD_UNION) THEN
281   SUBGOAL_THEN `(CARD(IMAGE (f:A->B) s) = CARD s) /\
282                 (CARD(IMAGE (g:A->B) s) = CARD s)`
283   STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[CARD_IMAGE_INJ]; ALL_TAC] THEN
284   ASM_SIMP_TAC[FINITE_IMAGE] THEN
285   MATCH_MP_TAC(TAUT `(~a ==> c) /\ ~b ==> (a ==> b) ==> c`) THEN CONJ_TAC THENL
286    [REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; IN_IMAGE; NOT_IN_EMPTY] THEN
287     MESON_TAC[]; ALL_TAC] THEN
288   MATCH_MP_TAC(ARITH_RULE `!t. t < 2 * s /\ p <= t ==> ~(p = s + s)`) THEN
289   EXISTS_TAC `CARD(t:B->bool)` THEN ASM_REWRITE_TAC[] THEN
290   MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[SUBSET; IN_UNION; IN_IMAGE] THEN
291   ASM_MESON_TAC[]);;
292
293 (* ------------------------------------------------------------------------- *)
294 (* In particular, consider functions out of 0...(p-1)/2, mod p.              *)
295 (* ------------------------------------------------------------------------- *)
296
297 let PIGEONHOLE_LEMMA_P12 = prove
298  (`!f g p.
299         ODD(p) /\
300         (!x. 2 * x < p ==> f(x) < p) /\
301         (!x y. 2 * x < p /\ 2 * y < p /\ (f x = f y) ==> (x = y)) /\
302         (!x. 2 * x < p ==> g(x) < p) /\
303         (!x y. 2 * x < p /\ 2 * y < p /\ (g x = g y) ==> (x = y))
304         ==> ?x y. 2 * x < p /\ 2 * y < p /\ (f x = g y)`,
305   REPEAT GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
306   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
307   FIRST_X_ASSUM(X_CHOOSE_THEN `k:num` SUBST1_TAC) THEN
308   MP_TAC(ISPECL [`f:num->num`; `g:num->num`;
309                  `{x:num | 2 * x < 2 * k + 1}`; `{x:num | x < 2 * k + 1}`]
310          PIGEONHOLE_LEMMA) THEN
311   REWRITE_TAC[ADD1; ARITH_RULE `2 * x < 2 * k + 1 <=> x < k + 1`] THEN
312   REWRITE_TAC[FINITE_NUMSEG_LT; CARD_NUMSEG_LT] THEN
313   REWRITE_TAC[IN_ELIM_THM; ARITH_RULE `2 * k + 1 < 2 * (k + 1)`]);;
314
315 (* ------------------------------------------------------------------------- *)
316 (* Show that \x. x^2 + a (mod p) satisfies the conditions.                   *)
317 (* ------------------------------------------------------------------------- *)
318
319 let SQUAREMOD_INJ_LEMMA = prove
320  (`!p x d. prime(p) /\ 2 * (x + d) < p /\
321            ((x + d) * (x + d) + m * p = x * x + n * p)
322            ==> (d = 0)`,
323   REPEAT STRIP_TAC THEN
324   SUBGOAL_THEN `p divides d \/ p divides (2 * x + d)` MP_TAC THENL
325    [MATCH_MP_TAC PRIME_DIVPROD THEN ASM_REWRITE_TAC[divides] THEN
326     EXISTS_TAC `n - m:num` THEN REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
327     MATCH_MP_TAC(ARITH_RULE `!a:num. (a + b + d = a + c) ==> (b = c - d)`) THEN
328     EXISTS_TAC `x * x:num` THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
329     FIRST_ASSUM(SUBST1_TAC o SYM) THEN ARITH_TAC;
330     DISCH_THEN(DISJ_CASES_THEN(MP_TAC o MATCH_MP DIVIDES_LE)) THEN
331     SIMP_TAC[ADD_EQ_0] THEN UNDISCH_TAC `2 * (x + d) < p` THEN ARITH_TAC]);;
332
333 let SQUAREMOD_INJ = prove
334  (`!p. prime(p)
335    ==> (!x. 2 * x < p ==> (x EXP 2 + a) MOD p < p) /\
336        (!x y. 2 * x < p /\ 2 * y < p /\
337               ((x EXP 2 + a) MOD p = (y EXP 2 + a) MOD p)
338               ==> (x = y))`,
339   REPEAT STRIP_TAC THEN
340   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `x < a ==> ~(a = 0)`)) THEN
341   ASM_SIMP_TAC[DIVISION] THEN
342   SUBGOAL_THEN
343    `(x EXP 2 + a = (x EXP 2 + a) DIV p * p + (x EXP 2 + a) MOD p) /\
344     (y EXP 2 + a = (y EXP 2 + a) DIV p * p + (y EXP 2 + a) MOD p)`
345   MP_TAC THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
346   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
347    `(x2 + a = xp + b:num) /\ (y2 + a = yp + b)
348     ==> (x2 + yp = y2 + xp)`)) THEN
349   DISJ_CASES_THEN MP_TAC (SPECL [`x:num`; `y:num`] LE_CASES) THEN
350   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC o
351     REWRITE_RULE[LE_EXISTS])
352   THENL [ONCE_REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
353   REWRITE_TAC[EXP_2; ARITH_RULE `(x + d = x) = (d = 0)`] THEN
354   ASM_MESON_TAC[SQUAREMOD_INJ_LEMMA]);;
355
356 (* ------------------------------------------------------------------------- *)
357 (* Show that also a reflection mod p retains this property.                  *)
358 (* ------------------------------------------------------------------------- *)
359
360 let REFLECT_INJ = prove
361  (`(!x. 2 * x < p ==> f(x) < p) /\
362    (!x y. 2 * x < p /\ 2 * y < p /\ (f x = f y) ==> (x = y))
363    ==> (!x. 2 * x < p ==> p - 1 - f(x) < p) /\
364        (!x y. 2 * x < p /\ 2 * y < p /\ (p - 1 - f(x) = p - 1 - f(y))
365               ==> (x = y))`,
366   REPEAT GEN_TAC THEN STRIP_TAC THEN
367   REWRITE_TAC[ARITH_RULE `2 * x < p ==> p - 1 - y < p`] THEN
368   REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
369   MATCH_MP_TAC(ARITH_RULE
370    `x < p /\ y < p /\ (p - 1 - x = p - 1 - y) ==> (x = y)`) THEN
371   ASM_MESON_TAC[]);;
372
373 (* ------------------------------------------------------------------------- *)
374 (* Hence the main result.                                                    *)
375 (* ------------------------------------------------------------------------- *)
376
377 let LAGRANGE_LEMMA_ODD = prove
378  (`!a p. prime(p) /\ ODD(p)
379          ==> ?n x y. 2 * x < p /\ 2 * y < p /\
380                      (n * p = x EXP 2 + y EXP 2 + a + 1)`,
381   REPEAT STRIP_TAC THEN
382   SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL [ASM_MESON_TAC[ODD]; ALL_TAC] THEN
383   MP_TAC(ISPECL [`\x. (x EXP 2 + a) MOD p`;
384                  `\x. p - 1 - (x EXP 2 + 0) MOD p`; `p:num`]
385                 PIGEONHOLE_LEMMA_P12) THEN
386   REWRITE_TAC[] THEN ANTS_TAC THENL
387    [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT
388      `(a /\ b) /\ (c /\ d) ==> a /\ b /\ c /\ d`) THEN
389     CONJ_TAC THENL
390      [ALL_TAC; MATCH_MP_TAC REFLECT_INJ] THEN
391     ASM_MESON_TAC[SQUAREMOD_INJ]; ALL_TAC] THEN
392   STRIP_TAC THEN
393   FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
394    `(x = p - 1 - y) ==> y < p ==> (x + y + 1 = p)`)) THEN
395   ANTS_TAC THENL [ASM_MESON_TAC[DIVISION]; ALL_TAC] THEN
396   DISCH_THEN(MP_TAC o C AP_THM `p:num` o AP_TERM `(MOD)`) THEN
397   SUBGOAL_THEN
398    `((x EXP 2 + a) MOD p + (y EXP 2 + 0) MOD p + 1) MOD p =
399     (x EXP 2 + y EXP 2 + a + 1) MOD p`
400   SUBST1_TAC THENL
401    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN
402     EXISTS_TAC `(x EXP 2 + a) DIV p + (y EXP 2) DIV p` THEN
403     REWRITE_TAC[ADD_CLAUSES] THEN
404     MATCH_MP_TAC(ARITH_RULE
405       `(x2 + a = xd * p + xm) /\ (y2 = yd * p + ym)
406        ==> (x2 + y2 + a + 1 = (xm + ym + 1) + (xd + yd) * p)`) THEN
407     ASM_MESON_TAC[DIVISION]; ALL_TAC] THEN
408   SUBGOAL_THEN `p MOD p = 0` SUBST1_TAC THENL
409    [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN
410     UNDISCH_TAC `~(p = 0)` THEN ARITH_TAC; ALL_TAC] THEN
411   DISCH_TAC THEN MAP_EVERY EXISTS_TAC
412    [`(x EXP 2 + y EXP 2 + a + 1) DIV p`; `x:num`; `y:num`] THEN
413   ASM_REWRITE_TAC[] THEN
414   FIRST_ASSUM(MP_TAC o SPEC `x EXP 2 + y EXP 2 + a + 1` o
415     MATCH_MP DIVISION) THEN
416  ASM_REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN MESON_TAC[]);;
417
418 (* ------------------------------------------------------------------------- *)
419 (* Avoid the additional conditions.                                          *)
420 (* ------------------------------------------------------------------------- *)
421
422 let LAGRANGE_LEMMA = prove
423  (`!a p. prime(p)
424          ==> ?n x y. 2 * x <= p /\ 2 * y <= p /\
425                      (n * p = x EXP 2 + y EXP 2 + a)`,
426   REPEAT STRIP_TAC THEN ASM_CASES_TAC `EVEN(p)` THENL
427    [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [prime]) THEN
428     DISCH_THEN(MP_TAC o SPEC `2` o CONJUNCT2) THEN
429     ANTS_TAC THENL [ASM_MESON_TAC[EVEN_EXISTS; divides]; ALL_TAC] THEN
430     REWRITE_TAC[ARITH_EQ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
431     ASM_CASES_TAC `EVEN(a)` THENL
432      [UNDISCH_TAC `EVEN a` THEN REWRITE_TAC[EVEN_EXISTS] THEN
433       DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST_ALL_TAC) THEN
434       MAP_EVERY EXISTS_TAC [`k:num`; `0`; `0`] THEN
435       REWRITE_TAC[ARITH; ADD_CLAUSES] THEN ARITH_TAC;
436       UNDISCH_TAC `~(EVEN(a))` THEN REWRITE_TAC[NOT_EVEN; ODD_EXISTS] THEN
437       DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST_ALL_TAC) THEN
438       MAP_EVERY EXISTS_TAC [`k + 1`; `1`; `0`] THEN
439       REWRITE_TAC[ARITH; ADD_CLAUSES] THEN ARITH_TAC];
440     ASM_CASES_TAC `a = 0` THENL
441      [MAP_EVERY EXISTS_TAC [`0`; `0`; `0`] THEN
442       ASM_REWRITE_TAC[LE_0; ADD_CLAUSES; MULT_CLAUSES; EXP_2]; ALL_TAC] THEN
443     FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
444      `~(a = 0) ==> (a = (a - 1) + 1)`)) THEN
445     MP_TAC(SPECL [`a - 1`; `p:num`] LAGRANGE_LEMMA_ODD) THEN
446     ASM_REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[LT_IMP_LE]]);;
447
448 (* ------------------------------------------------------------------------- *)
449 (* Aubrey's lemma showing that rationals suffice for sums of 4 squares.      *)
450 (* ------------------------------------------------------------------------- *)
451
452 prioritize_real();;
453
454 let REAL_INTEGER_CLOSURES = prove
455  (`(!n. ?p. abs(&n) = &p) /\
456    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x + y) = &p) /\
457    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x - y) = &p) /\
458    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x * y) = &p) /\
459    (!x r. (?n. abs(x) = &n) ==> ?p. abs(x pow r) = &p) /\
460    (!x. (?n. abs(x) = &n) ==> ?p. abs(--x) = &p) /\
461    (!x. (?n. abs(x) = &n) ==> ?p. abs(abs x) = &p)`,
462   MATCH_MP_TAC(TAUT
463    `x /\ c /\ d /\ e /\ f /\ (a /\ e ==> b) /\ a
464     ==> x /\ a /\ b /\ c /\ d /\ e /\ f`) THEN
465   REPEAT CONJ_TAC THENL
466    [REWRITE_TAC[REAL_ABS_NUM] THEN MESON_TAC[];
467     REWRITE_TAC[REAL_ABS_MUL] THEN MESON_TAC[REAL_OF_NUM_MUL];
468     REWRITE_TAC[REAL_ABS_POW] THEN MESON_TAC[REAL_OF_NUM_POW];
469     REWRITE_TAC[REAL_ABS_NEG]; REWRITE_TAC[REAL_ABS_ABS];
470     REWRITE_TAC[real_sub] THEN MESON_TAC[]; ALL_TAC] THEN
471   SIMP_TAC[REAL_ARITH `&0 <= a ==> ((abs(x) = a) <=> (x = a) \/ (x = --a))`;
472            REAL_POS] THEN
473   REPEAT STRIP_TAC THEN
474   ASM_REWRITE_TAC[GSYM REAL_NEG_ADD; REAL_OF_NUM_ADD] THENL
475    [MESON_TAC[]; ALL_TAC; ALL_TAC; MESON_TAC[]] THEN
476   REWRITE_TAC[REAL_ARITH `(--a + b = c) <=> (a + c = b)`;
477               REAL_ARITH `(a + --b = c) <=> (b + c = a)`] THEN
478   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
479   MESON_TAC[LE_EXISTS; ADD_SYM; LE_CASES]);;
480
481 let REAL_NUM_ROUND = prove
482  (`!x. &0 <= x ==> ?n. abs(x - &n) <= &1 / &2`,
483   REPEAT STRIP_TAC THEN
484   FIRST_ASSUM(MP_TAC o MATCH_MP (MATCH_MP REAL_ARCH_LEAST REAL_LT_01)) THEN
485   REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_MUL_RID] THEN
486   DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
487   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
488     `a <= x /\ x < a + &1
489      ==> abs(x - a) * &2 <= &1 \/ abs(x - (a + &1)) * &2 <= &1`)) THEN
490   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
491   MESON_TAC[REAL_OF_NUM_ADD]);;
492
493 let REAL_POS_ABS_MIDDLE = prove
494  (`!x n. &0 <= x /\ (abs(x - &n) = &1 / &2)
495          ==> (x = &(n - 1) + &1 / &2) \/ (x = &n + &1 / &2)`,
496   REPEAT GEN_TAC THEN
497   MP_TAC(SPECL [`1`; `n:num`] REAL_OF_NUM_SUB) THEN
498   DISJ_CASES_TAC(ARITH_RULE `(n = 0) \/ 1 <= n`) THEN
499   ASM_REWRITE_TAC[ARITH] THENL
500    [MP_TAC(REAL_RAT_REDUCE_CONV `&0 <= &1 / &2`) THEN REAL_ARITH_TAC;
501     DISCH_THEN(SUBST1_TAC o SYM) THEN
502     REWRITE_TAC[REAL_ARITH `n - &1 + a = n - (&1 - a)`] THEN
503     CONV_TAC REAL_RAT_REDUCE_CONV THEN REAL_ARITH_TAC]);;
504
505 let REAL_RAT_ABS_MIDDLE = prove
506  (`!m n p. (abs(&m / &p - &n) = &1 / &2)
507          ==> (&m / &p = &(n - 1) + &1 / &2) \/ (&m / &p = &n + &1 / &2)`,
508   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_POS_ABS_MIDDLE THEN
509   ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS]);;
510
511 let AUBREY_LEMMA_4 = prove
512  (`!m n p q r.
513         ~(m = 0) /\ ~(m = 1) /\
514         ((&n / &m) pow 2 + (&p / &m) pow 2 +
515          (&q / &m) pow 2 + (&r / &m) pow 2 = &N)
516         ==> ?m' n' p' q' r'.
517                ~(m' = 0) /\ m' < m /\
518                ((&n' / &m') pow 2 + (&p' / &m') pow 2 +
519                 (&q' / &m') pow 2 + (&r' / &m') pow 2 = &N)`,
520   REPEAT STRIP_TAC THEN
521   MATCH_MP_TAC(TAUT `(~p ==> p) ==> p`) THEN
522   REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC THEN
523   SUBGOAL_THEN
524    `?n' p' q' r'.
525         (&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
526         (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 < &1 \/
527         (((&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
528           (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 = &1) /\
529          (m = 2) /\ (EVEN(n' + p' + q' + r') = EVEN(N)))`
530   MP_TAC THENL
531    [ASM_CASES_TAC
532      `?n' p' q' r'. (&n / &m = &n' + &1 / &2) /\
533                     (&p / &m = &p' + &1 / &2) /\
534                     (&q / &m = &q' + &1 / &2) /\
535                     (&r / &m = &r' + &1 / &2)` THENL
536      [FIRST_X_ASSUM(CHOOSE_THEN STRIP_ASSUME_TAC) THEN
537       MAP_EVERY EXISTS_TAC [`n':num`; `p':num`; `q':num`] THEN
538       SUBGOAL_THEN `m = 2` SUBST_ALL_TAC THENL
539        [FIRST_X_ASSUM(MP_TAC o SPECL
540          [`2`; `2 * n' + 1`; `2 * p' + 1`; `2 * q' + 1`; `2 * r' + 1`]) THEN
541         REWRITE_TAC[ARITH_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
542         REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
543         REWRITE_TAC[GSYM real_div] THEN
544         SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN
545         REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
546         REWRITE_TAC[] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
547         ARITH_TAC; ALL_TAC] THEN
548       SUBGOAL_THEN `(EVEN(n' + p' + q' + r') <=> EVEN(N)) \/
549                     (EVEN(n' + p' + q' + r' + 1) <=> EVEN(N))`
550       DISJ_CASES_TAC THENL
551        [REWRITE_TAC[EVEN_ADD; ARITH_EVEN] THEN CONV_TAC TAUT;
552         EXISTS_TAC `r':num` THEN DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
553         REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
554         CONV_TAC REAL_RAT_REDUCE_CONV;
555         EXISTS_TAC `r' + 1` THEN DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
556         REWRITE_TAC[REAL_ARITH `(a + b) - a = b`] THEN
557         REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
558         REWRITE_TAC[REAL_ARITH `(a + b) - (a + c) = b - c`] THEN
559         CONV_TAC REAL_RAT_REDUCE_CONV];
560       ALL_TAC] THEN
561     MAP_EVERY (fun t -> MP_TAC(SPEC t REAL_NUM_ROUND))
562      [`&n / &m`; `&p / &m`; `&q / &m`; `&r / &m`] THEN
563     SIMP_TAC[REAL_LE_DIV; REAL_POS] THEN
564     MAP_EVERY (fun t -> DISCH_THEN(X_CHOOSE_TAC t))
565      [`r':num`; `q':num`; `p':num`; `n':num`] THEN
566     MAP_EVERY EXISTS_TAC [`n':num`; `p':num`; `q':num`; `r':num`] THEN
567     DISJ1_TAC THEN
568     MATCH_MP_TAC(REAL_ARITH
569      `!m. a <= m /\ b <= m /\ c <= m /\ d <= m /\
570           ~((a = m) /\ (b = m) /\ (c = m) /\ (d = m)) /\
571           &4 * m <= &1
572           ==> a + b + c + d < &1`) THEN
573     EXISTS_TAC `(&1 / &2) pow 2` THEN
574     ONCE_REWRITE_TAC[SYM(SPEC `a - b` REAL_POW2_ABS)] THEN
575     ASM_SIMP_TAC[REAL_POW_LE2; REAL_ABS_POS; REAL_LE_DIV; REAL_POS] THEN
576     CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
577     REWRITE_TAC[REAL_POW_2; REAL_ARITH
578      `(a * a = b * b) <=> ((a + b) * (a - b) = &0)`] THEN
579     REWRITE_TAC[REAL_ENTIRE] THEN
580     SIMP_TAC[REAL_ARITH `&0 <= x /\ &0 < y ==> ~(x + y = &0)`;
581              REAL_ABS_POS; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
582     REWRITE_TAC[REAL_SUB_0] THEN
583     FIRST_ASSUM(MP_TAC o check (is_neg o concl)) THEN
584     REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN
585     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN
586      (MP_TAC o MATCH_MP REAL_RAT_ABS_MIDDLE)) THEN MESON_TAC[];
587     ALL_TAC] THEN
588   FIRST_X_ASSUM(K ALL_TAC o check (is_forall o concl)) THEN
589   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
590   MAP_EVERY X_GEN_TAC [`n':num`; `p':num`; `q':num`; `r':num`] THEN
591   DISCH_TAC THEN
592   ABBREV_TAC `s = &n - &m * &n'` THEN
593   ABBREV_TAC `t = &p - &m * &p'` THEN
594   ABBREV_TAC `u = &q - &m * &q'` THEN
595   ABBREV_TAC `v = &r - &m * &r'` THEN
596   ABBREV_TAC `N' = n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2` THEN
597   UNDISCH_TAC `n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2 = N'` THEN
598   DISCH_THEN(ASSUME_TAC o REWRITE_RULE
599    [GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW]) THEN
600   ABBREV_TAC `M = 2 * (n * n' + p * p' + q * q' + r * r')` THEN
601   UNDISCH_TAC `2 * (n * n' + p * p' + q * q' + r * r') = M` THEN
602   DISCH_THEN(ASSUME_TAC o REWRITE_RULE
603    [GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL;
604     GSYM REAL_OF_NUM_POW]) THEN
605   ASM_CASES_TAC `(&n / &m = &n') /\ (&p / &m = &p') /\
606                  (&q / &m = &q') /\ (&r / &m = &r')` THENL
607    [MAP_EVERY EXISTS_TAC [`1`; `n':num`; `p':num`; `q':num`; `r':num`] THEN
608     REWRITE_TAC[ARITH_EQ; REAL_DIV_1] THEN CONJ_TAC THENL
609      [UNDISCH_TAC `~(m = 0)` THEN UNDISCH_TAC `~(m = 1)` THEN ARITH_TAC;
610       UNDISCH_THEN
611         `(&n / &m) pow 2 + (&p / &m) pow 2 +
612          (&q / &m) pow 2 + (&r / &m) pow 2 = &N`
613         (SUBST1_TAC o SYM) THEN
614       ASM_REWRITE_TAC[]];
615     ALL_TAC] THEN
616   SUBGOAL_THEN `&0 < (&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
617                      (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2`
618   MP_TAC THENL
619    [MATCH_MP_TAC(REAL_ARITH
620      `&0 <= w /\ &0 <= x /\ &0 <= y /\ &0 <= z /\
621       ~((w = &0) /\ (x = &0) /\ (y = &0) /\ (z = &0))
622       ==> &0 < w + x + y + z`) THEN
623     REWRITE_TAC[REAL_POW_2; REAL_ENTIRE; REAL_LE_SQUARE] THEN
624     ASM_REWRITE_TAC[REAL_SUB_0];
625     ALL_TAC] THEN
626   FIRST_X_ASSUM(MP_TAC o check (is_disj o concl)) THEN
627   SUBGOAL_THEN
628    `(&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
629     (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 =
630     (s pow 2 + t pow 2 + u pow 2 + v pow 2) / &m pow 2`
631   MP_TAC THENL
632    [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&m pow 2` THEN
633     ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
634     REWRITE_TAC[REAL_ADD_RDISTRIB; GSYM REAL_POW_MUL; REAL_SUB_RDISTRIB] THEN
635     ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
636     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
637   SUBGOAL_THEN `(&n / &m - &n') pow 2 + (&p / &m - &p') pow 2 +
638                 (&q / &m - &q') pow 2 + (&r / &m - &r') pow 2 =
639                 (&N + &N') - &M / &m`
640   ASSUME_TAC THENL
641    [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&m pow 2` THEN
642     ASM_SIMP_TAC[REAL_POW_EQ_0; REAL_DIV_RMUL; REAL_OF_NUM_EQ] THEN
643     REWRITE_TAC[GSYM(ASSUME `(&n / &m) pow 2 + (&p / &m) pow 2 +
644                              (&q / &m) pow 2 + (&r / &m) pow 2 = &N`);
645            GSYM(ASSUME `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`);
646            GSYM(ASSUME
647             `&2 * (&n * &n' + &p * &p' + &q * &q' + &r * &r') = &M`)] THEN
648     REWRITE_TAC[REAL_ADD_RDISTRIB; GSYM REAL_POW_MUL; REAL_SUB_RDISTRIB] THEN
649     REWRITE_TAC[REAL_POW_2;  REAL_MUL_ASSOC] THEN
650     SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; ASSUME `~(m = 0)`] THEN
651     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
652     SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; ASSUME `~(m = 0)`] THEN
653     REAL_ARITH_TAC; ALL_TAC] THEN
654   ASM_REWRITE_TAC[] THEN
655   REWRITE_TAC[REAL_ARITH `(a + b) - c < &1 <=> (a + b) - &1 < c`;
656               REAL_ARITH `((a + b) - c = &1) <=> ((a + b) - &1 = c)`;
657               REAL_ARITH `&0 < a - b <=> b < a`] THEN
658   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_EQ_RDIV_EQ; REAL_OF_NUM_LT;
659            ARITH_RULE `0 < n <=> ~(n = 0)`; ASSUME `~(m = 0)`] THEN
660   REWRITE_TAC[REAL_ARITH `(a - &1) * m < M <=> a * m - M < m`;
661               REAL_ARITH `((a - &1) * m = M) <=> (a * m - M = m)`] THEN
662   REPEAT DISCH_TAC THEN
663   UNDISCH_TAC `(&N + &N') - &M / &m =
664                (s pow 2 + t pow 2 + u pow 2 + v pow 2) / &m pow 2` THEN
665   ASM_SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT;
666                ARITH_RULE `0 < a <=> ~(a = 0)`] THEN
667   REWRITE_TAC[REAL_POW_2; REAL_SUB_RDISTRIB; REAL_MUL_ASSOC] THEN
668   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_OF_NUM_EQ; GSYM REAL_POW_2] THEN
669   ABBREV_TAC `m':num = (N + N') * m - M` THEN
670   SUBGOAL_THEN `(&N + &N') * &m - &M = &m'`
671    (fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)
672   THENL
673    [EXPAND_TAC "m'" THEN
674     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] THEN
675     MATCH_MP_TAC REAL_OF_NUM_SUB THEN
676     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_ADD; GSYM
677                 REAL_OF_NUM_MUL] THEN
678     ASM_SIMP_TAC[REAL_LT_IMP_LE]; ALL_TAC] THEN
679   ASM_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
680   DISCH_THEN(ASSUME_TAC o GSYM) THEN
681   SUBGOAL_THEN `~(m' = 0)` ASSUME_TAC THENL
682    [REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN
683     REWRITE_TAC[GSYM(ASSUME `(&N + &N') * &m - &M = &m'`)] THEN
684     MATCH_MP_TAC(REAL_ARITH `b < a ==> ~(a - b = &0)`) THEN
685     ASM_REWRITE_TAC[]; ALL_TAC] THEN
686   SUBGOAL_THEN
687    `!z. (&n' + s * z) pow 2 + (&p' + t * z) pow 2 +
688         (&q' + u * z) pow 2 + (&r' + v * z) pow 2 - &N =
689         (&m * z - &1) * (&m' * z + &N - &N')`
690   ASSUME_TAC THENL
691    [GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
692     EXISTS_TAC `&m * &m' * z pow 2 + (&M - &2 * &m * &N') * z + &N' - &N` THEN
693     CONJ_TAC THENL
694      [REWRITE_TAC[REAL_POW_2; REAL_ARITH
695        `(n + s * z) * (n + s * z) + (p + t * z) * (p + t * z) +
696         (q + u * z) * (q + u * z) + (r + v * z) * (r + v * z) - N =
697         (s * s + t * t + u * u + v * v) * (z * z) +
698         (&2 * (n * s + p * t + q * u + r * v)) * z +
699         ((n * n + p * p + q * q + r * r) - N)`] THEN
700       ASM_REWRITE_TAC[GSYM REAL_POW_2] THEN
701       MATCH_MP_TAC(REAL_ARITH
702        `(a = c) /\ (b = d) ==> (a + b + n - m = c + d + n - m)`) THEN
703       CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN
704       AP_THM_TAC THEN AP_TERM_TAC THEN
705       REWRITE_TAC[GSYM(ASSUME
706        `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`);
707                   GSYM(ASSUME
708        `&2 * (&n * &n' + &p * &p' + &q * &q' + &r * &r') = &M`)] THEN
709       MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
710       REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC;
711       REWRITE_TAC[REAL_POW_2; REAL_ARITH
712         `(m * z - &1) * (m' * z + nn) = m * m' * z * z +
713                                         (m * z * nn - m' * z) - nn`] THEN
714       REWRITE_TAC[REAL_EQ_ADD_LCANCEL] THEN
715       REWRITE_TAC[REAL_ARITH `(a + n' - n = b - (n - n')) <=> (a = b)`] THEN
716       REWRITE_TAC[REAL_ARITH `a * z * b - c * z = (a * b - c) * z`] THEN
717       AP_THM_TAC THEN AP_TERM_TAC THEN
718       REWRITE_TAC[GSYM(ASSUME `(&N + &N') * &m - &M = &m'`)] THEN
719       REAL_ARITH_TAC];
720     ALL_TAC] THEN
721   ABBREV_TAC `w = &n' + s * (&N' - &N) / &m'` THEN
722   ABBREV_TAC `x = &p' + t * (&N' - &N) / &m'` THEN
723   ABBREV_TAC `y = &q' + u * (&N' - &N) / &m'` THEN
724   ABBREV_TAC `z = &r' + v * (&N' - &N) / &m'` THEN
725   SUBGOAL_THEN `w pow 2 + x pow 2 + y pow 2 + z pow 2 = &N`
726   (SUBST1_TAC o SYM) THENL
727    [MAP_EVERY EXPAND_TAC ["w"; "x"; "y"; "z"] THEN
728     ONCE_REWRITE_TAC[REAL_ARITH
729       `(a + b + c + d = e) <=> (a + b + c + d - e = &0)`] THEN
730     FIRST_ASSUM(SUBST1_TAC o SPEC `(&N' - &N) / &m'`) THEN
731     REWRITE_TAC[REAL_ENTIRE] THEN DISJ2_TAC THEN
732     ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ] THEN REAL_ARITH_TAC;
733     ALL_TAC] THEN
734   FIRST_X_ASSUM(DISJ_CASES_THEN2 ASSUME_TAC MP_TAC) THENL
735    [EXISTS_TAC `m':num` THEN
736     SUBGOAL_THEN
737      `?a b c d. (abs(&n' * &m' + s * (&N' - &N)) = &a) /\
738                 (abs(&p' * &m' + t * (&N' - &N)) = &b) /\
739                 (abs(&q' * &m' + u * (&N' - &N)) = &c) /\
740                 (abs(&r' * &m' + v * (&N' - &N)) = &d)`
741     MP_TAC THENL
742      [MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
743       REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
744       MESON_TAC[REAL_INTEGER_CLOSURES]; ALL_TAC] THEN
745     MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
746      [`a:num`; `b:num`; `c:num`; `d:num`] THEN
747     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
748     RULE_ASSUM_TAC(REWRITE_RULE[REAL_OF_NUM_LT]) THEN
749     REWRITE_TAC[REAL_POW_DIV; REAL_POW2_ABS] THEN
750     REWRITE_TAC[GSYM REAL_POW_DIV] THEN
751     REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
752     ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ] THEN
753     REWRITE_TAC[GSYM real_div; REAL_MUL_RID] THEN
754     ASM_REWRITE_TAC[]; ALL_TAC] THEN
755   REWRITE_TAC[REAL_OF_NUM_EQ] THEN
756   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC)) THEN
757   DISCH_TAC THEN
758   SUBGOAL_THEN `?n. abs((&N' - &N) / &2) = &n` ASSUME_TAC THENL
759    [REWRITE_TAC[GSYM(ASSUME
760      `&n' pow 2 + &p' pow 2 + &q' pow 2 + &r' pow 2 = &N'`)] THEN
761     REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD] THEN
762     SUBGOAL_THEN `EVEN(n' EXP 2 + p' EXP 2 + q' EXP 2 + r' EXP 2) =
763                   EVEN N`
764     MP_TAC THENL
765      [FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
766       REWRITE_TAC[EVEN_ADD; EVEN_EXP; ARITH_EQ];
767       ALL_TAC] THEN
768     DISJ_CASES_THEN MP_TAC (TAUT `EVEN(N) \/ ~EVEN(N)`) THEN SIMP_TAC[] THEN
769     REWRITE_TAC[NOT_EVEN; EVEN_EXISTS; ODD_EXISTS] THEN
770     REPEAT(DISCH_THEN(CHOOSE_THEN SUBST1_TAC)) THEN
771     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL] THEN
772     REWRITE_TAC[REAL_ARITH `(&2 * x + &1) - (&2 * y + &1) = &2 * (x - y)`] THEN
773     REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
774     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
775     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
776     CONV_TAC REAL_RAT_REDUCE_CONV THEN
777     REWRITE_TAC[REAL_MUL_RID] THEN MESON_TAC[REAL_INTEGER_CLOSURES];
778     ALL_TAC] THEN
779   EXISTS_TAC `1` THEN REWRITE_TAC[ARITH_EQ] THEN
780   SUBGOAL_THEN
781     `?a b c d. (abs(&n' + s * (&N' - &N) / &2) = &a) /\
782                (abs(&p' + t * (&N' - &N) / &2) = &b) /\
783                (abs(&q' + u * (&N' - &N) / &2) = &c) /\
784                (abs(&r' + v * (&N' - &N) / &2) = &d)`
785   MP_TAC THENL
786    [MAP_EVERY EXPAND_TAC ["s"; "t"; "u"; "v"] THEN
787     REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
788     UNDISCH_TAC `?n. abs ((&N' - &N) / &2) = &n` THEN
789     MESON_TAC[REAL_INTEGER_CLOSURES]; ALL_TAC] THEN
790   REWRITE_TAC[ARITH; REAL_DIV_1] THEN
791   MAP_EVERY (fun t -> MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC t)
792      [`a:num`; `b:num`; `c:num`; `d:num`] THEN
793   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
794   ASM_REWRITE_TAC[REAL_POW2_ABS]);;
795
796 (* ------------------------------------------------------------------------- *)
797 (* Hence the main result.                                                    *)
798 (* ------------------------------------------------------------------------- *)
799
800 let AUBREY_THM_4 = prove
801  (`(?q. ~(q = 0) /\
802        ?a b c d.
803             (&a / &q) pow 2 + (&b / &q) pow 2 +
804             (&c / &q) pow 2 + (&d / &q) pow 2 = &N)
805    ==> ?a b c d. &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2 = &N`,
806   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
807   DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
808   ASM_CASES_TAC `m = 1` THENL
809    [ASM_REWRITE_TAC[REAL_DIV_1; ARITH_EQ] THEN MESON_TAC[];
810     STRIP_TAC THEN MP_TAC(SPEC `m:num` AUBREY_LEMMA_4) THEN
811     ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;
812
813 (* ------------------------------------------------------------------------- *)
814 (* The algebraic lemma.                                                      *)
815 (* ------------------------------------------------------------------------- *)
816
817 let LAGRANGE_IDENTITY = REAL_ARITH
818   `(w1 pow 2 + x1 pow 2 + y1 pow 2 + z1 pow 2) *
819    (w2 pow 2 + x2 pow 2 + y2 pow 2 + z2 pow 2) =
820    (w1 * w2 - x1 * x2 - y1 * y2 - z1 * z2) pow 2 +
821    (w1 * x2 + x1 * w2 + y1 * z2 - z1 * y2) pow 2 +
822    (w1 * y2 - x1 * z2 + y1 * w2 + z1 * x2) pow 2 +
823    (w1 * z2 + x1 * y2 - y1 * x2 + z1 * w2) pow 2`;;
824
825 (* ------------------------------------------------------------------------- *)
826 (* Now sum of 4 squares.                                                     *)
827 (* ------------------------------------------------------------------------- *)
828
829 let LAGRANGE_REAL_NUM = prove
830  (`!n. ?w x y z. &n = &w pow 2 + &x pow 2 + &y pow 2 + &z pow 2`,
831   let lemma = prove
832    (`(?a. abs(w) = &a) /\ (?b. abs(x) = &b) /\
833      (?c. abs(y) = &c) /\ (?d. abs(z) = &d)
834      ==> ?a b c d. w pow 2 + x pow 2 + y pow 2 + z pow 2 =
835                    &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2`,
836     STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
837     ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ABS_NUM] THEN
838     MESON_TAC[]) in
839   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
840   ASM_CASES_TAC `n = 0` THENL
841    [REPEAT(EXISTS_TAC `0`) THEN ASM_REWRITE_TAC[] THEN
842     CONV_TAC REAL_RAT_REDUCE_CONV;
843     ALL_TAC] THEN
844   ASM_CASES_TAC `n = 1` THENL
845    [EXISTS_TAC `1` THEN REPEAT(EXISTS_TAC `0`) THEN
846     ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
847     ALL_TAC] THEN
848   FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
849   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
850   UNDISCH_TAC `p divides n` THEN REWRITE_TAC[divides] THEN
851   DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
852   ASM_CASES_TAC `m = 1` THENL
853    [ALL_TAC;
854     DISCH_THEN SUBST_ALL_TAC THEN
855     FIRST_X_ASSUM(fun th ->
856      MP_TAC(SPEC `p:num` th) THEN MP_TAC(SPEC `m:num` th)) THEN
857     ONCE_REWRITE_TAC[ARITH_RULE `m < p * m <=> 1 * m < p * m`] THEN
858     REWRITE_TAC[LT_MULT_RCANCEL] THEN
859     ONCE_REWRITE_TAC[ARITH_RULE `p < p * m <=> p * 1 < p * m`] THEN
860     REWRITE_TAC[LT_MULT_LCANCEL] THEN
861     UNDISCH_TAC `~(p * m = 0)` THEN REWRITE_TAC[MULT_EQ_0] THEN
862     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THEN
863     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
864     SUBGOAL_THEN `~(p = 1)` ASSUME_TAC THENL
865      [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
866     ASM_REWRITE_TAC[ARITH_RULE `1 < x <=> ~(x = 0) /\ ~(x = 1)`] THEN
867     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
868     MAP_EVERY X_GEN_TAC [`w1:num`; `x1:num`; `y1:num`; `z1:num`] THEN
869     DISCH_TAC THEN
870     MAP_EVERY X_GEN_TAC [`w2:num`; `x2:num`; `y2:num`; `z2:num`] THEN
871     DISCH_TAC THEN ASM_REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
872     REWRITE_TAC[LAGRANGE_IDENTITY] THEN
873     MATCH_MP_TAC lemma THEN REWRITE_TAC[REAL_OF_NUM_MUL] THEN
874     MESON_TAC[REAL_INTEGER_CLOSURES]] THEN
875   UNDISCH_TAC `m = 1` THEN DISCH_THEN SUBST_ALL_TAC THEN
876   REWRITE_TAC[MULT_CLAUSES] THEN DISCH_THEN SUBST_ALL_TAC THEN
877   FIRST_ASSUM(MP_TAC o MATCH_MP LAGRANGE_LEMMA) THEN
878   DISCH_THEN(MP_TAC o SPEC `1 EXP 2 + 0 EXP 2`) THEN
879   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
880   MAP_EVERY X_GEN_TAC [`q:num`; `x:num`; `y:num`] THEN STRIP_TAC THEN
881   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC AUBREY_THM_4 THEN
882   SUBGOAL_THEN `q * p < p EXP 2` MP_TAC THENL
883    [ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
884     MATCH_MP_TAC(ARITH_RULE
885      `(2 * x) * (2 * x) <= p * p /\ (2 * y) * (2 * y) <= p * p /\
886       2 * 2 <= p * p
887       ==> x * x + y * y + 1 < p * p`) THEN
888     REPEAT CONJ_TAC THEN MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[] THEN
889     MAP_EVERY UNDISCH_TAC [`~(p = 0)`; `~(p = 1)`] THEN ARITH_TAC;
890     ALL_TAC] THEN
891   REWRITE_TAC[EXP_2; LT_MULT_RCANCEL] THEN ASM_REWRITE_TAC[] THEN
892   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `q:num`) THEN
893   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
894   MAP_EVERY X_GEN_TAC [`a:num`; `b:num`; `c:num`; `d:num`] THEN DISCH_TAC THEN
895   SUBGOAL_THEN `~(q = 0)` ASSUME_TAC THENL
896    [DISCH_THEN SUBST_ALL_TAC THEN
897     UNDISCH_TAC `0 * p = x EXP 2 + y EXP 2 + 1 EXP 2 + 0 EXP 2` THEN
898     DISCH_THEN(MP_TAC o SYM) THEN REWRITE_TAC[MULT_CLAUSES; EXP_2] THEN
899     REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
900   SUBGOAL_THEN `&p = &q * &(q * p) / &q pow 2` SUBST1_TAC THENL
901    [REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_ASSOC; real_div] THEN
902     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
903     REWRITE_TAC[GSYM REAL_POW_2] THEN
904     SIMP_TAC[REAL_MUL_ASSOC; REAL_POW_EQ_0; REAL_MUL_LINV; REAL_MUL_LID;
905              ASSUME `~(q = 0)`; REAL_OF_NUM_EQ];
906     ALL_TAC] THEN
907   ASM_REWRITE_TAC[] THEN
908   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN
909   REWRITE_TAC[real_div; REAL_MUL_ASSOC; LAGRANGE_IDENTITY] THEN
910   SUBST1_TAC(SYM(ASSUME
911     `&q = &a pow 2 + &b pow 2 + &c pow 2 + &d pow 2`)) THEN
912   REWRITE_TAC[REAL_ADD_RDISTRIB] THEN
913   REWRITE_TAC[GSYM real_div; GSYM REAL_POW_DIV] THEN
914   EXISTS_TAC `q:num` THEN REWRITE_TAC[ASSUME `~(q = 0)`] THEN
915   REWRITE_TAC[REAL_POW_DIV] THEN
916   REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB] THEN
917   REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
918   REWRITE_TAC[REAL_INV_EQ_0; REAL_POW_EQ_0; REAL_OF_NUM_EQ;
919               ASSUME `~(q = 0)`] THEN
920   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN MATCH_MP_TAC lemma THEN
921   REWRITE_TAC[REAL_OF_NUM_MUL] THEN MESON_TAC[REAL_INTEGER_CLOSURES]);;
922
923 (* ------------------------------------------------------------------------- *)
924 (* Also prove it for the natural numbers.                                    *)
925 (* ------------------------------------------------------------------------- *)
926
927 let LAGRANGE_NUM = prove
928  (`!n. ?w x y z. n = w EXP 2 + x EXP 2 + y EXP 2 + z EXP 2`,
929   GEN_TAC THEN MP_TAC(SPEC `n:num` LAGRANGE_REAL_NUM) THEN
930   REWRITE_TAC[REAL_POS; REAL_OF_NUM_POW; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ]);;
931
932 (* ------------------------------------------------------------------------- *)
933 (* And for the integers.                                                     *)
934 (* ------------------------------------------------------------------------- *)
935
936 prioritize_int();;
937
938 let LAGRANGE_INT = prove
939  (`!a. &0 <= a <=> ?w x y z. a = w pow 2 + x pow 2 + y pow 2 + z pow 2`,
940   GEN_TAC THEN EQ_TAC THENL
941    [SPEC_TAC(`a:int`,`a:int`) THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN
942     X_GEN_TAC `n:num` THEN MP_TAC(SPEC `n:num` LAGRANGE_REAL_NUM) THEN
943     REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
944     SIMP_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_POW; GSYM INT_OF_NUM_ADD] THEN
945     MESON_TAC[];
946     STRIP_TAC THEN ASM_SIMP_TAC[INT_LE_SQUARE; INT_LE_ADD; INT_POW_2]]);;
947
948 prioritize_num();;