100/constructible.ml

   1 (* ========================================================================= *)
   2 (* Non-constructibility of irrational cubic equation solutions.              *)
   3 (*                                                                           *)
   4 (* This gives the two classic impossibility results: trisecting an angle or  *)
   5 (* constructing the cube using traditional geometric constructions.          *)
   6 (*                                                                           *)
   7 (* This elementary proof (not using field extensions etc.) is taken from     *)
   8 (* Dickson's "First Course in the Theory of Equations", chapter III.         *)
   9 (* ========================================================================= *)
  10
  11 needs "Library/prime.ml";;
  12 needs "Library/floor.ml";;
  13 needs "Multivariate/transcendentals.ml";;
  14
  15 prioritize_real();;
  16
  17 (* ------------------------------------------------------------------------- *)
  18 (* The critical lemma.                                                       *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 let STEP_LEMMA = prove
  22  (`!P. (!n. P(&n)) /\
  23        (!x. P x ==> P(--x)) /\
  24        (!x. P x /\ ~(x = &0) ==> P(inv x)) /\
  25        (!x y. P x /\ P y ==> P(x + y)) /\
  26        (!x y. P x /\ P y ==> P(x * y))
  27        ==> !a b c z u v s.
  28                P a /\ P b /\ P c /\
  29                z pow 3 + a * z pow 2 + b * z + c = &0 /\
  30                P u /\ P v /\ P(s * s) /\ z = u + v * s
  31                ==> ?w. P w /\ w pow 3 + a * w pow 2 + b * w + c = &0`,
  32   REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
  33   ASM_CASES_TAC `v * s = &0` THENL
  34    [ASM_REWRITE_TAC[REAL_ADD_RID] THEN MESON_TAC[]; ALL_TAC] THEN
  35   STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
  36   MAP_EVERY ABBREV_TAC
  37    [`A = a * s pow 2 * v pow 2 + &3 * s pow 2 * u * v pow 2 +
  38          a * u pow 2 + u pow 3 +  b * u + c`;
  39     `B = s pow 2 * v pow 3 + &2 * a * u * v + &3 * u pow 2 * v + b * v`] THEN
  40   SUBGOAL_THEN `A + B * s = &0` ASSUME_TAC THENL
  41    [REPEAT(FIRST_X_ASSUM(MP_TAC o SYM)) THEN CONV_TAC REAL_RING; ALL_TAC] THEN
  42   ASM_CASES_TAC `(P:real->bool) s` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  43   SUBGOAL_THEN `B = &0` ASSUME_TAC THENL
  44    [UNDISCH_TAC `~P(s:real)` THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  45     DISCH_TAC THEN REWRITE_TAC[] THEN
  46     FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_FIELD
  47      `A + B * s = &0 ==> ~(B = &0) ==> s = --A / B`)) THEN
  48     ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
  49     REWRITE_TAC[real_div] THEN FIRST_ASSUM MATCH_MP_TAC THEN
  50     CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
  51     MAP_EVERY EXPAND_TAC ["A"; "B"] THEN
  52     REWRITE_TAC[REAL_ARITH `x pow 3 = x * x * x`; REAL_POW_2] THEN
  53     REPEAT(FIRST_ASSUM MATCH_ACCEPT_TAC ORELSE
  54            (FIRST_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC));
  55     ALL_TAC] THEN
  56   EXISTS_TAC `--(a + &2 * u)` THEN ASM_SIMP_TAC[] THEN
  57   REPEAT(FIRST_X_ASSUM(MP_TAC o check ((not) o is_forall o concl))) THEN
  58   CONV_TAC REAL_RING);;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* Instantiate to square roots.                                              *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 let STEP_LEMMA_SQRT = prove
  65  (`!P. (!n. P(&n)) /\
  66        (!x. P x ==> P(--x)) /\
  67        (!x. P x /\ ~(x = &0) ==> P(inv x)) /\
  68        (!x y. P x /\ P y ==> P(x + y)) /\
  69        (!x y. P x /\ P y ==> P(x * y))
  70        ==> !a b c z u v s.
  71                P a /\ P b /\ P c /\
  72                z pow 3 + a * z pow 2 + b * z + c = &0 /\
  73                P u /\ P v /\ P(s) /\ &0 <= s /\ z = u + v * sqrt(s)
  74                ==> ?w. P w /\ w pow 3 + a * w pow 2 + b * w + c = &0`,
  75   GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP STEP_LEMMA) THEN
  76   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  77   ASM_MESON_TAC[SQRT_POW_2; REAL_POW_2]);;
  78
  79 (* ------------------------------------------------------------------------- *)
  80 (* Numbers definable by radicals involving square roots only.                *)
  81 (* ------------------------------------------------------------------------- *)
  82
  83 let radical_RULES,radical_INDUCT,radical_CASES = new_inductive_definition
  84  `(!x. rational x ==> radical x) /\
  85   (!x. radical x ==> radical (--x)) /\
  86   (!x. radical x /\ ~(x = &0) ==> radical (inv x)) /\
  87   (!x y. radical x /\ radical y ==> radical (x + y)) /\
  88   (!x y. radical x /\ radical y ==> radical (x * y)) /\
  89   (!x. radical x /\ &0 <= x ==> radical (sqrt x))`;;
  90
  91 let RADICAL_RULES = prove
  92  (`(!n. radical(&n)) /\
  93    (!x. rational x ==> radical x) /\
  94    (!x. radical x ==> radical (--x)) /\
  95    (!x. radical x /\ ~(x = &0) ==> radical (inv x)) /\
  96    (!x y. radical x /\ radical y ==> radical (x + y)) /\
  97    (!x y. radical x /\ radical y ==> radical (x - y)) /\
  98    (!x y. radical x /\ radical y ==> radical (x * y)) /\
  99    (!x y. radical x /\ radical y /\ ~(y = &0) ==> radical (x / y)) /\
 100    (!x n. radical x ==> radical(x pow n)) /\
 101    (!x. radical x /\ &0 <= x ==> radical (sqrt x))`,
 102   SIMP_TAC[real_div; real_sub; radical_RULES; RATIONAL_NUM] THEN
 103   GEN_TAC THEN INDUCT_TAC THEN
 104   ASM_SIMP_TAC[radical_RULES; real_pow; RATIONAL_NUM]);;
 105
 106 let RADICAL_TAC =
 107   REPEAT(MATCH_ACCEPT_TAC (CONJUNCT1 RADICAL_RULES) ORELSE
 108          (MAP_FIRST MATCH_MP_TAC(tl(tl(CONJUNCTS RADICAL_RULES))) THEN
 109           REPEAT CONJ_TAC));;
 110
 111 (* ------------------------------------------------------------------------- *)
 112 (* Explicit "expressions" to support inductive proof.                        *)
 113 (* ------------------------------------------------------------------------- *)
 114
 115 let expression_INDUCT,expression_RECURSION = define_type
 116  "expression = Constant real
 117              | Negation expression
 118              | Inverse expression
 119              | Addition expression expression
 120              | Multiplication expression expression
 121              | Sqrt expression";;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Interpretation.                                                           *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let value = define
 128  `(value(Constant x) = x) /\
 129   (value(Negation e) = --(value e)) /\
 130   (value(Inverse e) = inv(value e)) /\
 131   (value(Addition e1 e2) = value e1 + value e2) /\
 132   (value(Multiplication e1 e2) = value e1 * value e2) /\
 133   (value(Sqrt e) = sqrt(value e))`;;
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* Wellformedness of an expression.                                          *)
 137 (* ------------------------------------------------------------------------- *)
 138
 139 let wellformed = define
 140  `(wellformed(Constant x) <=> rational x) /\
 141   (wellformed(Negation e) <=> wellformed e) /\
 142   (wellformed(Inverse e) <=> ~(value e = &0) /\ wellformed e) /\
 143   (wellformed(Addition e1 e2) <=> wellformed e1 /\ wellformed e2) /\
 144   (wellformed(Multiplication e1 e2) <=> wellformed e1 /\ wellformed e2) /\
 145   (wellformed(Sqrt e) <=> &0 <= value e /\ wellformed e)`;;
 146
 147 (* ------------------------------------------------------------------------- *)
 148 (* The set of radicals in an expression.                                     *)
 149 (* ------------------------------------------------------------------------- *)
 150
 151 let radicals = define
 152  `(radicals(Constant x) = {}) /\
 153   (radicals(Negation e) = radicals e) /\
 154   (radicals(Inverse e) = radicals e) /\
 155   (radicals(Addition e1 e2) = (radicals e1) UNION (radicals e2)) /\
 156   (radicals(Multiplication e1 e2) = (radicals e1) UNION (radicals e2)) /\
 157   (radicals(Sqrt e) = e INSERT (radicals e))`;;
 158
 159 let FINITE_RADICALS = prove
 160  (`!e. FINITE(radicals e)`,
 161   MATCH_MP_TAC expression_INDUCT THEN
 162   SIMP_TAC[radicals; FINITE_RULES; FINITE_UNION]);;
 163
 164 let WELLFORMED_RADICALS = prove
 165  (`!e. wellformed e ==> !r. r IN radicals(e) ==> &0 <= value r`,
 166   MATCH_MP_TAC expression_INDUCT THEN
 167   REWRITE_TAC[radicals; wellformed; NOT_IN_EMPTY; IN_UNION; IN_INSERT] THEN
 168   MESON_TAC[]);;
 169
 170 let RADICALS_WELLFORMED = prove
 171  (`!e. wellformed e ==> !r. r IN radicals e ==> wellformed r`,
 172   MATCH_MP_TAC expression_INDUCT THEN
 173   REWRITE_TAC[radicals; wellformed; NOT_IN_EMPTY; IN_UNION; IN_INSERT] THEN
 174   MESON_TAC[]);;
 175
 176 let RADICALS_SUBSET = prove
 177  (`!e r. r IN radicals e ==> radicals(r) SUBSET radicals(e)`,
 178   MATCH_MP_TAC expression_INDUCT THEN
 179   REWRITE_TAC[radicals; IN_UNION; NOT_IN_EMPTY; IN_INSERT; SUBSET] THEN
 180   MESON_TAC[]);;
 181
 182 (* ------------------------------------------------------------------------- *)
 183 (* Show that every radical is the interpretation of a wellformed expresion.  *)
 184 (* ------------------------------------------------------------------------- *)
 185
 186 let RADICAL_EXPRESSION = prove
 187  (`!x. radical x <=> ?e. wellformed e /\ x = value e`,
 188   GEN_TAC THEN EQ_TAC THEN SPEC_TAC(`x:real`,`x:real`) THENL
 189    [MATCH_MP_TAC radical_INDUCT THEN REPEAT STRIP_TAC THEN
 190     REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN ASM_MESON_TAC[value; wellformed];
 191     SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 192     REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 193     REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
 194     MATCH_MP_TAC expression_INDUCT THEN
 195     REWRITE_TAC[value; wellformed] THEN SIMP_TAC[radical_RULES]]);;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Nesting depth of radicals in an expression.                               *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let LT_MAX = prove
 202  (`!a b c. a < MAX b c <=> a < b \/ a < c`,
 203   ARITH_TAC);;
 204
 205 let depth = define
 206  `(depth(Constant x) = 0) /\
 207   (depth(Negation e) = depth e) /\
 208   (depth(Inverse e) = depth e) /\
 209   (depth(Addition e1 e2) = MAX (depth e1) (depth e2)) /\
 210   (depth(Multiplication e1 e2) = MAX (depth e1) (depth e2)) /\
 211   (depth(Sqrt e) = 1 + depth e)`;;
 212
 213 let IN_RADICALS_SMALLER = prove
 214  (`!r s. s IN radicals(r) ==> depth(s) < depth(r)`,
 215   MATCH_MP_TAC expression_INDUCT THEN REWRITE_TAC[radicals; depth] THEN
 216   REWRITE_TAC[IN_UNION; NOT_IN_EMPTY; IN_INSERT; LT_MAX] THEN
 217   MESON_TAC[ARITH_RULE `s = a \/ s < a ==> s < 1 + a`]);;
 218
 219 let NOT_IN_OWN_RADICALS = prove
 220  (`!r. ~(r IN radicals r)`,
 221   MESON_TAC[IN_RADICALS_SMALLER; LT_REFL]);;
 222
 223 let RADICALS_EMPTY_RATIONAL = prove
 224  (`!e. wellformed e /\ radicals e = {} ==> rational(value e)`,
 225   MATCH_MP_TAC expression_INDUCT THEN
 226   REWRITE_TAC[wellformed; value; radicals; EMPTY_UNION; NOT_INSERT_EMPTY] THEN
 227   REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
 228   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 229   ASM_SIMP_TAC[RATIONAL_CLOSED]);;
 230
 231 (* ------------------------------------------------------------------------- *)
 232 (* Crucial point about splitting off some "topmost" radical.                 *)
 233 (* ------------------------------------------------------------------------- *)
 234
 235 let FINITE_MAX = prove
 236  (`!s. FINITE s ==> ~(s = {}) ==> ?b:num. b IN s /\ !a. a IN s ==> a <= b`,
 237   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 238   REWRITE_TAC[NOT_INSERT_EMPTY; IN_INSERT] THEN REPEAT GEN_TAC THEN
 239   ASM_CASES_TAC `s:num->bool = {}` THEN
 240   ASM_SIMP_TAC[NOT_IN_EMPTY; UNWIND_THM2; LE_REFL] THEN
 241   REWRITE_TAC[RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN
 242   MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;
 243
 244 let RADICAL_TOP = prove
 245  (`!e. ~(radicals e = {})
 246        ==> ?r. r IN radicals e /\
 247                !s. s IN radicals(e) ==> ~(r IN radicals s)`,
 248   REPEAT STRIP_TAC THEN
 249   MP_TAC(SPEC `IMAGE depth (radicals e)` FINITE_MAX) THEN
 250   ASM_SIMP_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE; FINITE_RADICALS] THEN
 251   REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE] THEN
 252   MESON_TAC[IN_RADICALS_SMALLER; NOT_LT]);;
 253
 254 (* ------------------------------------------------------------------------- *)
 255 (* By rearranging the expression we can use it in a canonical way.           *)
 256 (* ------------------------------------------------------------------------- *)
 257
 258 let RADICAL_CANONICAL_TRIVIAL = prove
 259  (`!e r.
 260      (r IN radicals e
 261             ==> (?a b.
 262                    wellformed a /\
 263                    wellformed b /\
 264                    value e = value a + value b * sqrt (value r) /\
 265                    radicals a SUBSET radicals e DELETE r /\
 266                    radicals b SUBSET radicals e DELETE r /\
 267                    radicals r SUBSET radicals e DELETE r))
 268      ==> wellformed e
 269          ==> ?a b. wellformed a /\
 270                    wellformed b /\
 271                    value e = value a + value b * sqrt (value r) /\
 272                    radicals a SUBSET (radicals e UNION radicals r) DELETE r /\
 273                    radicals b SUBSET (radicals e UNION radicals r) DELETE r /\
 274                    radicals r SUBSET (radicals e UNION radicals r) DELETE r`,
 275   REPEAT GEN_TAC THEN ASM_CASES_TAC `r IN radicals e` THEN ASM_SIMP_TAC[] THENL
 276    [DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 277     REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN SET_TAC[];
 278     DISCH_TAC THEN
 279     MAP_EVERY EXISTS_TAC [`e:expression`; `Constant(&0)`] THEN
 280     ASM_REWRITE_TAC[wellformed; value; radicals] THEN
 281     REWRITE_TAC[RATIONAL_NUM; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 282     UNDISCH_TAC `~(r IN radicals e)` THEN
 283     MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN SET_TAC[]]);;
 284
 285 let RADICAL_CANONICAL = prove
 286  (`!e. wellformed e /\ ~(radicals e = {})
 287        ==> ?r. r IN radicals(e) /\
 288                ?a b. wellformed(Addition a (Multiplication b (Sqrt r))) /\
 289                      value e = value(Addition a (Multiplication b (Sqrt r))) /\
 290                      (radicals a) SUBSET (radicals(e) DELETE r) /\
 291                      (radicals b) SUBSET (radicals(e) DELETE r) /\
 292                      (radicals r) SUBSET (radicals(e) DELETE r)`,
 293   REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP RADICAL_TOP) THEN
 294   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:expression` THEN
 295   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[] THEN
 296   SUBGOAL_THEN `&0 <= value r /\ wellformed r` STRIP_ASSUME_TAC THENL
 297    [ASM_MESON_TAC[WELLFORMED_RADICALS; RADICALS_WELLFORMED]; ALL_TAC] THEN
 298   MAP_EVERY UNDISCH_TAC [`wellformed e`; `r IN radicals e`] THEN
 299   ASM_REWRITE_TAC[IMP_IMP; wellformed; value; GSYM CONJ_ASSOC] THEN
 300   SPEC_TAC(`e:expression`,`e:expression`) THEN
 301   MATCH_MP_TAC expression_INDUCT THEN
 302   REWRITE_TAC[wellformed; radicals; value; NOT_IN_EMPTY] THEN
 303   REWRITE_TAC[IN_INSERT; IN_UNION] THEN REPEAT CONJ_TAC THEN
 304   X_GEN_TAC `e1:expression` THEN TRY(X_GEN_TAC `e2:expression`) THENL
 305    [DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 306     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 307     MAP_EVERY X_GEN_TAC [`a:expression`; `b:expression`] THEN
 308     STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`Negation a`; `Negation b`] THEN
 309     ASM_REWRITE_TAC[value; wellformed; radicals] THEN REAL_ARITH_TAC;
 310
 311     DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 312     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 313     MAP_EVERY X_GEN_TAC [`a:expression`; `b:expression`] THEN
 314     ASM_CASES_TAC `value b * sqrt(value r) = value a` THENL
 315      [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 316       MAP_EVERY EXISTS_TAC
 317        [`Inverse(Multiplication (Constant(&2)) a)`; `Constant(&0)`] THEN
 318       ASM_REWRITE_TAC[value; radicals; wellformed] THEN
 319       REWRITE_TAC[RATIONAL_NUM; EMPTY_SUBSET; CONJ_ASSOC] THEN CONJ_TAC THENL
 320        [UNDISCH_TAC `~(value a + value a = &0)` THEN CONV_TAC REAL_FIELD;
 321         REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]];
 322       ALL_TAC] THEN
 323     STRIP_TAC THEN MAP_EVERY EXISTS_TAC
 324      [`Multiplication a (Inverse
 325         (Addition (Multiplication a a)
 326                   (Multiplication (Multiplication b b) (Negation r))))`;
 327       `Multiplication (Negation b) (Inverse
 328         (Addition (Multiplication a a)
 329                   (Multiplication (Multiplication b b) (Negation r))))`] THEN
 330     ASM_REWRITE_TAC[value; wellformed; radicals; UNION_SUBSET] THEN
 331     UNDISCH_TAC `~(value b * sqrt (value r) = value a)` THEN
 332     UNDISCH_TAC `~(value e1 = &0)` THEN ASM_REWRITE_TAC[] THEN
 333     FIRST_ASSUM(MP_TAC o MATCH_MP SQRT_POW_2) THEN CONV_TAC REAL_FIELD;
 334
 335     REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 336     REWRITE_TAC[FORALL_AND_THM] THEN
 337     DISCH_THEN(fun th ->
 338       DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN MP_TAC th) THEN
 339     ASM_REWRITE_TAC[] THEN
 340     DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
 341       MATCH_MP RADICAL_CANONICAL_TRIVIAL)) THEN
 342     ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[IMP_IMP] THEN
 343     DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 344     REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 345     REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 346     MAP_EVERY X_GEN_TAC
 347      [`a1:expression`; `b1:expression`; `a2:expression`; `b2:expression`] THEN
 348     STRIP_TAC THEN MAP_EVERY EXISTS_TAC
 349      [`Addition a1 a2`; `Addition b1 b2`] THEN
 350     ASM_REWRITE_TAC[value; wellformed; radicals] THEN
 351     CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 352     MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN
 353     MP_TAC(SPECL [`e1:expression`; `r:expression`] RADICALS_SUBSET) THEN
 354     MP_TAC(SPECL [`e2:expression`; `r:expression`] RADICALS_SUBSET) THEN
 355     REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[];
 356
 357     REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 358     REWRITE_TAC[FORALL_AND_THM] THEN
 359     DISCH_THEN(fun th ->
 360       DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN MP_TAC th) THEN
 361     ASM_REWRITE_TAC[] THEN
 362     DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
 363       MATCH_MP RADICAL_CANONICAL_TRIVIAL)) THEN
 364     ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[IMP_IMP] THEN
 365     DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 366     REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 367     REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 368     MAP_EVERY X_GEN_TAC
 369      [`a1:expression`; `b1:expression`; `a2:expression`; `b2:expression`] THEN
 370     STRIP_TAC THEN MAP_EVERY EXISTS_TAC
 371      [`Addition (Multiplication a1 a2)
 372                 (Multiplication (Multiplication b1 b2) r)`;
 373       `Addition (Multiplication a1 b2) (Multiplication a2 b1)`] THEN
 374     ASM_REWRITE_TAC[value; wellformed; radicals] THEN CONJ_TAC THENL
 375      [FIRST_ASSUM(MP_TAC o MATCH_MP SQRT_POW_2) THEN CONV_TAC REAL_RING;
 376       ALL_TAC] THEN
 377     MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN
 378     MP_TAC(SPECL [`e1:expression`; `r:expression`] RADICALS_SUBSET) THEN
 379     MP_TAC(SPECL [`e2:expression`; `r:expression`] RADICALS_SUBSET) THEN
 380     REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[];
 381
 382     REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 383     REWRITE_TAC[FORALL_AND_THM] THEN
 384     DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 385     REPEAT(DISCH_THEN(K ALL_TAC)) THEN
 386     MAP_EVERY EXISTS_TAC [`Constant(&0)`; `Constant(&1)`] THEN
 387     REWRITE_TAC[wellformed; value; REAL_ADD_LID; REAL_MUL_LID] THEN
 388     REWRITE_TAC[radicals; RATIONAL_NUM] THEN
 389     MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN ASM SET_TAC[]]);;
 390
 391 (* ------------------------------------------------------------------------- *)
 392 (* Now we quite easily get an inductive argument.                            *)
 393 (* ------------------------------------------------------------------------- *)
 394
 395 let CUBIC_ROOT_STEP = prove
 396  (`!a b c. rational a /\ rational b /\ rational c
 397            ==> !e. wellformed e /\
 398                    ~(radicals e = {}) /\
 399                    (value e) pow 3 + a * (value e) pow 2 +
 400                                      b * (value e) + c = &0
 401                    ==> ?e'. wellformed e' /\
 402                             (radicals e') PSUBSET (radicals e) /\
 403                             (value e') pow 3 + a * (value e') pow 2 +
 404                                      b * (value e') + c = &0`,
 405   REPEAT STRIP_TAC THEN MP_TAC(SPEC `e:expression` RADICAL_CANONICAL) THEN
 406   ASM_REWRITE_TAC[] THEN DISCH_THEN
 407    (X_CHOOSE_THEN `r:expression` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 408   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 409   MAP_EVERY X_GEN_TAC [`eu:expression`; `ev:expression`] THEN
 410   STRIP_TAC THEN
 411   MP_TAC(SPEC `\x. ?ex. wellformed ex /\
 412                         radicals ex SUBSET (radicals(e) DELETE r) /\
 413                         value ex = x`
 414               STEP_LEMMA_SQRT) THEN
 415   REWRITE_TAC[] THEN ANTS_TAC THENL
 416    [REPEAT CONJ_TAC THENL
 417      [X_GEN_TAC `n:num` THEN EXISTS_TAC `Constant(&n)` THEN
 418       REWRITE_TAC[wellformed; radicals; RATIONAL_NUM; value; EMPTY_SUBSET];
 419       X_GEN_TAC `x:real` THEN
 420       DISCH_THEN(X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC) THEN
 421       EXISTS_TAC `Negation ex` THEN
 422       ASM_REWRITE_TAC[wellformed; radicals; value];
 423       X_GEN_TAC `x:real` THEN
 424       DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 425       DISCH_THEN(X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC) THEN
 426       EXISTS_TAC `Inverse ex` THEN
 427       ASM_REWRITE_TAC[wellformed; radicals; value];
 428       MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN
 429       DISCH_THEN(CONJUNCTS_THEN2
 430        (X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC)
 431        (X_CHOOSE_THEN `ey:expression` STRIP_ASSUME_TAC)) THEN
 432       EXISTS_TAC `Addition ex ey` THEN
 433       ASM_REWRITE_TAC[wellformed; radicals; value; UNION_SUBSET];
 434       MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN
 435       DISCH_THEN(CONJUNCTS_THEN2
 436        (X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC)
 437        (X_CHOOSE_THEN `ey:expression` STRIP_ASSUME_TAC)) THEN
 438       EXISTS_TAC `Multiplication ex ey` THEN
 439       ASM_REWRITE_TAC[wellformed; radicals; value; UNION_SUBSET]];
 440     ALL_TAC] THEN
 441   DISCH_THEN(MP_TAC o SPECL
 442    [`a:real`; `b:real`; `c:real`;
 443     `value e`; `value eu`; `value ev`; `value r`]) THEN
 444   ANTS_TAC THENL
 445    [CONJ_TAC THENL
 446      [EXISTS_TAC `Constant a` THEN
 447       ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
 448       ALL_TAC] THEN
 449     CONJ_TAC THENL
 450      [EXISTS_TAC `Constant b` THEN
 451       ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
 452       ALL_TAC] THEN
 453     CONJ_TAC THENL
 454      [EXISTS_TAC `Constant c` THEN
 455       ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
 456       ALL_TAC] THEN
 457     RULE_ASSUM_TAC(REWRITE_RULE[wellformed]) THEN
 458     ASM_REWRITE_TAC[value] THEN ASM_MESON_TAC[];
 459     ALL_TAC] THEN
 460   DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
 461   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e':expression` THEN
 462   ASM_SIMP_TAC[] THEN ASM SET_TAC[]);;
 463
 464 (* ------------------------------------------------------------------------- *)
 465 (* Hence the main result.                                                    *)
 466 (* ------------------------------------------------------------------------- *)
 467
 468 let CUBIC_ROOT_RADICAL_INDUCT = prove
 469  (`!a b c. rational a /\ rational b /\ rational c
 470            ==> !n e. wellformed e /\ CARD (radicals e) = n /\
 471                      (value e) pow 3 + a * (value e) pow 2 +
 472                                 b * (value e) + c = &0
 473                  ==> ?x. rational x /\
 474                          x pow 3 + a * x pow 2 + b * x + c = &0`,
 475   REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN
 476   X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `e:expression` THEN
 477   STRIP_TAC THEN ASM_CASES_TAC `radicals e = {}` THENL
 478    [ASM_MESON_TAC[RADICALS_EMPTY_RATIONAL]; ALL_TAC] THEN
 479   MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_STEP) THEN
 480   ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `e:expression`) THEN
 481   ASM_REWRITE_TAC[] THEN
 482   DISCH_THEN(X_CHOOSE_THEN `e':expression` STRIP_ASSUME_TAC) THEN
 483   FIRST_X_ASSUM(MP_TAC o SPEC `CARD(radicals e')`) THEN ANTS_TAC THENL
 484    [REWRITE_TAC[SYM(ASSUME `CARD(radicals e) = n`)] THEN
 485     MATCH_MP_TAC CARD_PSUBSET THEN ASM_REWRITE_TAC[FINITE_RADICALS];
 486     DISCH_THEN MATCH_MP_TAC THEN EXISTS_TAC `e':expression` THEN
 487     ASM_REWRITE_TAC[]]);;
 488
 489 let CUBIC_ROOT_RATIONAL = prove
 490  (`!a b c. rational a /\ rational b /\ rational c /\
 491            (?x. radical x /\ x pow 3 + a * x pow 2 + b * x + c = &0)
 492            ==> (?x. rational x /\ x pow 3 + a * x pow 2 + b * x + c = &0)`,
 493   REWRITE_TAC[RADICAL_EXPRESSION] THEN REPEAT STRIP_TAC THEN
 494   MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_RADICAL_INDUCT) THEN
 495   ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
 496   MAP_EVERY EXISTS_TAC [`CARD(radicals e)`; `e:expression`] THEN
 497   ASM_MESON_TAC[]);;
 498
 499 (* ------------------------------------------------------------------------- *)
 500 (* Now go further to an *integer*, since the polynomial is monic.            *)
 501 (* ------------------------------------------------------------------------- *)
 502
 503 prioritize_num();;
 504
 505 let RATIONAL_LOWEST_LEMMA = prove
 506  (`!p q. ~(q = 0) ==> ?p' q'. ~(q' = 0) /\ coprime(p',q') /\ p * q' = p' * q`,
 507   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN MATCH_MP_TAC num_WF THEN
 508   X_GEN_TAC `q:num` THEN DISCH_TAC THEN X_GEN_TAC `p:num` THEN DISCH_TAC THEN
 509   ASM_CASES_TAC `coprime(p,q)` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 510   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [coprime]) THEN
 511   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; GSYM CONJ_ASSOC] THEN
 512   DISCH_THEN(X_CHOOSE_THEN `d:num` MP_TAC) THEN
 513   ASM_CASES_TAC `d = 0` THEN ASM_REWRITE_TAC[DIVIDES_ZERO] THEN
 514   REWRITE_TAC[divides] THEN
 515   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `p':num` SUBST_ALL_TAC)
 516    (CONJUNCTS_THEN2 (X_CHOOSE_THEN `q':num` SUBST_ALL_TAC) ASSUME_TAC)) THEN
 517   FIRST_X_ASSUM(MP_TAC o SPEC `q':num`) THEN
 518   RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
 519   GEN_REWRITE_TAC (funpow 2 LAND_CONV) [ARITH_RULE `a < b <=> 1 * a < b`] THEN
 520   ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
 521   ASM_SIMP_TAC[ARITH_RULE `~(d = 0) /\ ~(d = 1) ==> 1 < d`] THEN
 522   DISCH_THEN(MP_TAC o SPEC `p':num`) THEN
 523   REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN SIMP_TAC[] THEN
 524   CONV_TAC NUM_RING);;
 525
 526 prioritize_real();;
 527
 528 let RATIONAL_LOWEST = prove
 529  (`!x. rational x <=> ?p q. ~(q = 0) /\ coprime(p,q) /\ abs(x) = &p / &q`,
 530   GEN_TAC THEN REWRITE_TAC[RATIONAL_ALT] THEN EQ_TAC THENL
 531    [ALL_TAC; MESON_TAC[]] THEN
 532   STRIP_TAC THEN MP_TAC(SPECL [`p:num`; `q:num`] RATIONAL_LOWEST_LEMMA) THEN
 533   ASM_REWRITE_TAC[] THEN REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
 534   UNDISCH_TAC `~(q = 0)` THEN SIMP_TAC[GSYM REAL_OF_NUM_EQ] THEN
 535   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN CONV_TAC REAL_FIELD);;
 536
 537 let RATIONAL_ROOT_INTEGER = prove
 538  (`!a b c x. integer a /\ integer b /\ integer c /\ rational x /\
 539              x pow 3 + a * x pow 2 + b * x + c = &0
 540              ==> integer x`,
 541   REWRITE_TAC[RATIONAL_LOWEST; GSYM REAL_OF_NUM_EQ] THEN
 542   REPEAT STRIP_TAC THEN
 543   FIRST_X_ASSUM(MP_TAC o MATCH_MP(REAL_ARITH
 544    `abs x = a ==> x = a \/ x = --a`)) THEN
 545   DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
 546   FIRST_X_ASSUM(MP_TAC o check (is_eq o concl)) THEN
 547   ASM_SIMP_TAC[REAL_FIELD
 548    `~(q = &0)
 549      ==> ((p / q) pow 3 + a * (p / q) pow 2 + b * (p / q) + c = &0 <=>
 550           (p pow 3 = q * --(a * p pow 2 + b * p * q + c * q pow 2))) /\
 551          ((--(p / q)) pow 3 + a * (--(p / q)) pow 2 +
 552            b * (--(p / q)) + c = &0 <=>
 553           p pow 3 = q * (a * p pow 2 - b * p * q + c * q pow 2))`] THEN
 554   (W(fun(asl,w) ->
 555        SUBGOAL_THEN(mk_comb(`integer`,rand(rand(lhand w)))) MP_TAC THENL
 556     [REPEAT(MAP_FIRST MATCH_MP_TAC (tl(CONJUNCTS INTEGER_CLOSED)) THEN
 557             REPEAT CONJ_TAC) THEN
 558      ASM_REWRITE_TAC[INTEGER_CLOSED];
 559      ALL_TAC])) THEN
 560   REWRITE_TAC[integer] THEN DISCH_THEN(X_CHOOSE_TAC `i:num`) THEN
 561   DISCH_THEN(MP_TAC o AP_TERM `abs`) THEN
 562   ASM_REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NEG] THEN
 563   REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM; REAL_OF_NUM_MUL] THEN
 564   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_EQ] THEN
 565   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_SYM]) THEN
 566   DISCH_THEN(MP_TAC o SPEC `3` o MATCH_MP COPRIME_EXP) THEN
 567   REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `q:num`) THEN
 568   ASM_CASES_TAC `q = 1` THEN
 569   ASM_SIMP_TAC[REAL_DIV_1; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL] THEN
 570   MESON_TAC[divides; DIVIDES_REFL]);;
 571
 572 (* ------------------------------------------------------------------------- *)
 573 (* Hence we have our big final theorem.                                      *)
 574 (* ------------------------------------------------------------------------- *)
 575
 576 let CUBIC_ROOT_INTEGER = prove
 577  (`!a b c. integer a /\ integer b /\ integer c /\
 578            (?x. radical x /\ x pow 3 + a * x pow 2 + b * x + c = &0)
 579            ==> (?x. integer x /\ x pow 3 + a * x pow 2 + b * x + c = &0)`,
 580   REPEAT STRIP_TAC THEN
 581   MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_RATIONAL) THEN
 582   ASM_SIMP_TAC[RATIONAL_INTEGER] THEN
 583   ASM_MESON_TAC[RATIONAL_ROOT_INTEGER]);;
 584
 585 (* ------------------------------------------------------------------------- *)
 586 (* Geometrical definitions.                                                  *)
 587 (* ------------------------------------------------------------------------- *)
 588
 589 let length = new_definition
 590   `length(a:real^2,b:real^2) = norm(b - a)`;;
 591
 592 let parallel = new_definition
 593  `parallel (a:real^2,b:real^2) (c:real^2,d:real^2) <=>
 594         (a$1 - b$1) * (c$2 - d$2) = (a$2 - b$2) * (c$1 - d$1)`;;
 595
 596 let collinear3 = new_definition
 597   `collinear3 (a:real^2) b c <=> parallel (a,b) (a,c)`;;
 598
 599 let is_intersection = new_definition
 600   `is_intersection p (a,b) (c,d) <=> collinear3 a p b /\ collinear3 c p d`;;
 601
 602 let on_circle = new_definition
 603  `on_circle x (centre,pt) <=> length(centre,x) = length(centre,pt)`;;
 604
 605 (* ------------------------------------------------------------------------- *)
 606 (* A trivial lemma.                                                          *)
 607 (* ------------------------------------------------------------------------- *)
 608
 609 let SQRT_CASES_LEMMA = prove
 610  (`!x y. y pow 2 = x ==> &0 <= x /\ (sqrt(x) = y \/ sqrt(x) = --y)`,
 611   REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
 612   REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
 613   MP_TAC(SPEC `y:real` (GEN_ALL POW_2_SQRT)) THEN
 614   MP_TAC(SPEC `--y` (GEN_ALL POW_2_SQRT)) THEN
 615   REWRITE_TAC[GSYM REAL_POW_2; REAL_POW_NEG; ARITH] THEN REAL_ARITH_TAC);;
 616
 617 (* ------------------------------------------------------------------------- *)
 618 (* Show that solutions to certain classes of equations are radical.          *)
 619 (* ------------------------------------------------------------------------- *)
 620
 621 let RADICAL_LINEAR_EQUATION = prove
 622  (`!a b x. radical a /\ radical b /\ ~(a = &0 /\ b = &0) /\ a * x + b = &0
 623            ==> radical x`,
 624   REPEAT STRIP_TAC THEN
 625   SUBGOAL_THEN `~(a = &0) /\ x = --b / a`
 626    (fun th -> ASM_SIMP_TAC[th; RADICAL_RULES]) THEN
 627   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;
 628
 629 let RADICAL_SIMULTANEOUS_LINEAR_EQUATION = prove
 630  (`!a b c d e f x.
 631         radical a /\ radical b /\ radical c /\
 632         radical d /\ radical e /\ radical f /\
 633         ~(a * e = b * d /\ a * f = c * d /\ e * c = b * f) /\
 634         a * x + b * y = c /\ d * x + e * y = f
 635         ==> radical(x) /\ radical(y)`,
 636   REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN
 637    `~(a * e - b * d = &0) /\
 638     x = (e * c - b * f) / (a * e - b * d) /\
 639     y = (a * f - d * c) / (a * e - b * d)`
 640   STRIP_ASSUME_TAC THENL
 641    [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
 642     ASM_SIMP_TAC[RADICAL_RULES]]);;
 643
 644 let RADICAL_QUADRATIC_EQUATION = prove
 645  (`!a b c x. radical a /\ radical b /\ radical c /\
 646              a * x pow 2 + b * x + c = &0 /\
 647              ~(a = &0 /\ b = &0 /\ c = &0)
 648              ==> radical x`,
 649   REPEAT GEN_TAC THEN ASM_CASES_TAC `a = &0` THEN ASM_REWRITE_TAC[] THENL
 650    [ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
 651     MESON_TAC[RADICAL_LINEAR_EQUATION];
 652     ALL_TAC] THEN
 653   STRIP_TAC THEN MATCH_MP_TAC RADICAL_LINEAR_EQUATION THEN
 654   EXISTS_TAC `&2 * a` THEN
 655   ASM_SIMP_TAC[RADICAL_RULES; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 656   SUBGOAL_THEN `&0 <= b pow 2 - &4 * a * c /\
 657                 ((&2 * a) * x + (b - sqrt(b pow 2 - &4 * a * c)) = &0 \/
 658                  (&2 * a) * x + (b + sqrt(b pow 2 - &4 * a * c)) = &0)`
 659   MP_TAC THENL
 660    [REWRITE_TAC[real_sub; REAL_ARITH `a + (b + c) = &0 <=> c = --(a + b)`] THEN
 661     REWRITE_TAC[REAL_EQ_NEG2] THEN MATCH_MP_TAC SQRT_CASES_LEMMA THEN
 662     FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC REAL_RING;
 663     STRIP_TAC THENL
 664      [EXISTS_TAC `b - sqrt(b pow 2 - &4 * a * c)`;
 665       EXISTS_TAC `b + sqrt(b pow 2 - &4 * a * c)`] THEN
 666     ASM_REWRITE_TAC[] THEN RADICAL_TAC THEN ASM_REWRITE_TAC[]]);;
 667
 668 let RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC = prove
 669  (`!a b c d e f x.
 670         radical a /\ radical b /\ radical c /\
 671         radical d /\ radical e /\ radical f /\
 672         ~(d = &0 /\ e = &0 /\ f = &0) /\
 673         (x - a) pow 2 + (y - b) pow 2 = c /\ d * x + e * y = f
 674         ==> radical x /\ radical y`,
 675   REPEAT STRIP_TAC THEN
 676   MP_TAC(SPEC `d pow 2 + e pow 2` RADICAL_QUADRATIC_EQUATION) THEN
 677   DISCH_THEN MATCH_MP_TAC THENL
 678    [EXISTS_TAC `&2 * b * d * e - &2 * a * e pow 2 - &2 * d * f` THEN
 679     EXISTS_TAC `b pow 2 * e pow 2 + a pow 2 * e pow 2 +
 680                 f pow 2 - c * e pow 2 - &2 * b * e * f`;
 681     EXISTS_TAC `&2 * a * d * e - &2 * b * d pow 2 - &2 * f * e` THEN
 682     EXISTS_TAC `a pow 2 * d pow 2 + b pow 2 * d pow 2 +
 683                 f pow 2 - c * d pow 2 - &2 * a * d * f`] THEN
 684   (REPLICATE_TAC 3
 685     (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
 686    CONJ_TAC THENL
 687     [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING; ALL_TAC] THEN
 688    REWRITE_TAC[REAL_SOS_EQ_0] THEN REPEAT(POP_ASSUM MP_TAC) THEN
 689    CONV_TAC REAL_RING));;
 690
 691 let RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC = prove
 692  (`!a b c d e f x.
 693         radical a /\ radical b /\ radical c /\
 694         radical d /\ radical e /\ radical f /\
 695         ~(a = d /\ b = e /\ c = f) /\
 696         (x - a) pow 2 + (y - b) pow 2 = c /\
 697         (x - d) pow 2 + (y - e) pow 2 = f
 698         ==> radical x /\ radical y`,
 699   REPEAT GEN_TAC THEN STRIP_TAC THEN
 700   MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC THEN
 701   MAP_EVERY EXISTS_TAC
 702    [`a:real`; `b:real`; `c:real`; `&2 * (d - a)`; `&2 * (e - b)`;
 703     `(d pow 2 - a pow 2) + (e pow 2 - b pow 2) + (c - f)`] THEN
 704   ASM_REWRITE_TAC[] THEN
 705   REPLICATE_TAC 3
 706    (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
 707   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
 708
 709 (* ------------------------------------------------------------------------- *)
 710 (* Analytic criterion for constructibility.                                  *)
 711 (* ------------------------------------------------------------------------- *)
 712
 713 let constructible_RULES,constructible_INDUCT,constructible_CASES =
 714  new_inductive_definition
 715   `(!x:real^2. rational(x$1) /\ rational(x$2) ==> constructible x) /\
 716 // Intersection of two non-parallel lines AB and CD
 717   (!a b c d x. constructible a /\ constructible b /\
 718                constructible c /\ constructible d /\
 719                ~parallel (a,b) (c,d) /\ is_intersection x (a,b) (c,d)
 720                ==> constructible x) /\
 721 // Intersection of a nontrivial line AB and circle with centre C, radius DE
 722   (!a b c d e x. constructible a /\ constructible b /\
 723                  constructible c /\ constructible d /\
 724                  constructible e /\
 725                  ~(a = b) /\ collinear3 a x b /\ length (c,x) = length(d,e)
 726                  ==> constructible x) /\
 727 // Intersection of distinct circles with centres A and D, radii BD and EF
 728   (!a b c d e f x. constructible a /\ constructible b /\
 729                    constructible c /\ constructible d /\
 730                    constructible e /\ constructible f /\
 731                    ~(a = d /\ length (b,c) = length (e,f)) /\
 732                    length (a,x) = length (b,c) /\ length (d,x) = length (e,f)
 733                    ==> constructible x)`;;
 734
 735 (* ------------------------------------------------------------------------- *)
 736 (* Some "coordinate geometry" lemmas.                                        *)
 737 (* ------------------------------------------------------------------------- *)
 738
 739 let RADICAL_LINE_LINE_INTERSECTION = prove
 740  (`!a b c d x.
 741         radical(a$1) /\ radical(a$2) /\
 742         radical(b$1) /\ radical(b$2) /\
 743         radical(c$1) /\ radical(c$2) /\
 744         radical(d$1) /\ radical(d$2) /\
 745         ~(parallel (a,b) (c,d)) /\ is_intersection x (a,b) (c,d)
 746         ==> radical(x$1) /\ radical(x$2)`,
 747   REPEAT GEN_TAC THEN
 748   REWRITE_TAC[parallel; collinear3; is_intersection] THEN STRIP_TAC THEN
 749   MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_EQUATION THEN
 750   MAP_EVERY EXISTS_TAC
 751    [`(b:real^2)$2 - (a:real^2)$2`; `(a:real^2)$1 - (b:real^2)$1`;
 752     `(a:real^2)$2 * (a$1 - (b:real^2)$1) - (a:real^2)$1 * (a$2 - b$2)`;
 753     `(d:real^2)$2 - (c:real^2)$2`; `(c:real^2)$1 - (d:real^2)$1`;
 754     `(c:real^2)$2 * (c$1 - (d:real^2)$1) - (c:real^2)$1 * (c$2 - d$2)`] THEN
 755   REPLICATE_TAC 6
 756    (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
 757   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
 758
 759 let RADICAL_LINE_CIRCLE_INTERSECTION = prove
 760  (`!a b c d e x.
 761         radical(a$1) /\ radical(a$2) /\
 762         radical(b$1) /\ radical(b$2) /\
 763         radical(c$1) /\ radical(c$2) /\
 764         radical(d$1) /\ radical(d$2) /\
 765         radical(e$1) /\ radical(e$2) /\
 766         ~(a = b) /\ collinear3 a x b /\ length(c,x) = length(d,e)
 767         ==> radical(x$1) /\ radical(x$2)`,
 768   REPEAT GEN_TAC THEN
 769   REWRITE_TAC[length; NORM_EQ; collinear3; parallel] THEN
 770   SIMP_TAC[CART_EQ; FORALL_2; dot; SUM_2; DIMINDEX_2; VECTOR_SUB_COMPONENT;
 771            GSYM REAL_POW_2] THEN
 772   STRIP_TAC THEN MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC THEN
 773   MAP_EVERY EXISTS_TAC
 774    [`(c:real^2)$1`; `(c:real^2)$2`;
 775     `((e:real^2)$1 - (d:real^2)$1) pow 2 + (e$2 - d$2) pow 2`;
 776     `(b:real^2)$2 - (a:real^2)$2`;
 777     `(a:real^2)$1 - (b:real^2)$1`;
 778     `a$2 * ((a:real^2)$1 - (b:real^2)$1) - a$1 * (a$2 - b$2)`] THEN
 779   REPLICATE_TAC 6
 780    (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
 781   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
 782
 783 let RADICAL_CIRCLE_CIRCLE_INTERSECTION = prove
 784  (`!a b c d e f x.
 785         radical(a$1) /\ radical(a$2) /\
 786         radical(b$1) /\ radical(b$2) /\
 787         radical(c$1) /\ radical(c$2) /\
 788         radical(d$1) /\ radical(d$2) /\
 789         radical(e$1) /\ radical(e$2) /\
 790         radical(f$1) /\ radical(f$2) /\
 791         length(a,x) = length(b,c) /\
 792         length(d,x) = length(e,f) /\
 793         ~(a = d /\ length(b,c) = length(e,f))
 794         ==> radical(x$1) /\ radical(x$2)`,
 795   REPEAT GEN_TAC THEN
 796   REWRITE_TAC[length; NORM_EQ; collinear3; parallel] THEN
 797   SIMP_TAC[CART_EQ; FORALL_2; dot; SUM_2; DIMINDEX_2; VECTOR_SUB_COMPONENT;
 798            GSYM REAL_POW_2] THEN
 799   STRIP_TAC THEN MATCH_MP_TAC RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC THEN
 800   MAP_EVERY EXISTS_TAC
 801    [`(a:real^2)$1`; `(a:real^2)$2`;
 802     `((c:real^2)$1 - (b:real^2)$1) pow 2 + (c$2 - b$2) pow 2`;
 803     `(d:real^2)$1`; `(d:real^2)$2`;
 804     `((f:real^2)$1 - (e:real^2)$1) pow 2 + (f$2 - e$2) pow 2`] THEN
 805   REPLICATE_TAC 6
 806    (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
 807   REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
 808
 809 (* ------------------------------------------------------------------------- *)
 810 (* So constructible points have radical coordinates.                         *)
 811 (* ------------------------------------------------------------------------- *)
 812
 813 let CONSTRUCTIBLE_RADICAL = prove
 814  (`!x. constructible x ==> radical(x$1) /\ radical(x$2)`,
 815   MATCH_MP_TAC constructible_INDUCT THEN REPEAT CONJ_TAC THEN
 816   REPEAT GEN_TAC THEN STRIP_TAC THENL
 817    [ASM_SIMP_TAC[RADICAL_RULES];
 818     MATCH_MP_TAC RADICAL_LINE_LINE_INTERSECTION THEN ASM_MESON_TAC[];
 819     MATCH_MP_TAC RADICAL_LINE_CIRCLE_INTERSECTION THEN ASM_MESON_TAC[];
 820     MATCH_MP_TAC RADICAL_CIRCLE_CIRCLE_INTERSECTION THEN ASM_MESON_TAC[]]);;
 821
 822 (* ------------------------------------------------------------------------- *)
 823 (* Impossibility of doubling the cube.                                       *)
 824 (* ------------------------------------------------------------------------- *)
 825
 826 let DOUBLE_THE_CUBE_ALGEBRA = prove
 827  (`~(?x. radical x /\ x pow 3 = &2)`,
 828   STRIP_TAC THEN MP_TAC(SPECL [`&0`; `&0`; `-- &2`] CUBIC_ROOT_INTEGER) THEN
 829   SIMP_TAC[INTEGER_CLOSED; NOT_IMP] THEN
 830   REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
 831   REWRITE_TAC[GSYM real_sub; REAL_SUB_0] THEN
 832   CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 833   POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC THEN
 834   FIRST_X_ASSUM(MP_TAC o AP_TERM `abs`) THEN
 835   REWRITE_TAC[REAL_ABS_POW] THEN
 836   FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[integer]) THEN
 837   REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_POW; REAL_OF_NUM_EQ] THEN
 838   MATCH_MP_TAC(ARITH_RULE
 839    `n EXP 3 <= 1 EXP 3 \/ 2 EXP 3 <= n EXP 3 ==> ~(n EXP 3 = 2)`) THEN
 840   REWRITE_TAC[num_CONV `3`; EXP_MONO_LE_SUC] THEN ARITH_TAC);;
 841
 842 let DOUBLE_THE_CUBE = prove
 843  (`!x. x pow 3 = &2 ==> ~(constructible(vector[x; &0]))`,
 844   GEN_TAC THEN DISCH_TAC THEN
 845   DISCH_THEN(MP_TAC o MATCH_MP CONSTRUCTIBLE_RADICAL) THEN
 846   REWRITE_TAC[VECTOR_2; RADICAL_RULES] THEN
 847   ASM_MESON_TAC[DOUBLE_THE_CUBE_ALGEBRA]);;
 848
 849 (* ------------------------------------------------------------------------- *)
 850 (* Impossibility of trisecting                                               *)
 851 (* ------------------------------------------------------------------------- *)
 852
 853 let COS_TRIPLE = prove
 854  (`!x. cos(&3 * x) = &4 * cos(x) pow 3 - &3 * cos(x)`,
 855   GEN_TAC THEN
 856   REWRITE_TAC[REAL_ARITH `&3 * x = x + x + x`; SIN_ADD; COS_ADD] THEN
 857   MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
 858
 859 let COS_PI3 = prove
 860  (`cos(pi / &3) = &1 / &2`,
 861   MP_TAC(SPEC `pi / &3` COS_TRIPLE) THEN
 862   SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH; COS_PI] THEN
 863   REWRITE_TAC[REAL_RING
 864    `-- &1 = &4 * c pow 3 - &3 * c <=> c = &1 / &2 \/ c = -- &1`] THEN
 865   DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC MP_TAC) THEN
 866   MP_TAC(SPEC `pi / &3` COS_POS_PI) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);;
 867
 868 let TRISECT_60_DEGREES_ALGEBRA = prove
 869  (`~(?x. radical x /\ x pow 3 - &3 * x - &1 = &0)`,
 870   STRIP_TAC THEN MP_TAC(SPECL [`&0`; `-- &3`; `-- &1`] CUBIC_ROOT_INTEGER) THEN
 871   SIMP_TAC[INTEGER_CLOSED; NOT_IMP] THEN REWRITE_TAC[REAL_ADD_ASSOC] THEN
 872   REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; REAL_MUL_LNEG; GSYM real_sub] THEN
 873   CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 874   REWRITE_TAC[REAL_ARITH
 875    `x pow 3 - &3 * x - &1 = &0 <=> x * (x pow 2 - &3) = &1`] THEN
 876   POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC THEN
 877   FIRST_X_ASSUM(MP_TAC o AP_TERM `abs`) THEN
 878   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
 879   ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
 880   FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[integer]) THEN
 881   REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC (ARITH_RULE
 882    `n = 0 \/ n = 1 \/ n = 2 + (n - 2)`) THEN
 883   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
 884   REWRITE_TAC[REAL_ARITH `(&2 + m) pow 2 - &3 = m pow 2 + &4 * m + &1`] THEN
 885   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_POW; REAL_ABS_NUM;
 886               REAL_OF_NUM_EQ; MULT_EQ_1] THEN
 887   ARITH_TAC);;
 888
 889 let TRISECT_60_DEGREES = prove
 890  (`!y. ~(constructible(vector[cos(pi / &9); y]))`,
 891   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CONSTRUCTIBLE_RADICAL) THEN
 892   DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[VECTOR_2] THEN
 893   DISCH_TAC THEN MP_TAC(SPEC `pi / &9` COS_TRIPLE) THEN
 894   SIMP_TAC[REAL_ARITH `&3 * x / &9 = x / &3`; COS_PI3] THEN
 895   REWRITE_TAC[REAL_ARITH
 896    `&1 / &2 = &4 * c pow 3 - &3 * c <=>
 897     (&2 * c) pow 3 - &3 * (&2 * c) - &1 = &0`] THEN
 898   ASM_MESON_TAC[TRISECT_60_DEGREES_ALGEBRA; RADICAL_RULES]);;