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();;