(* ========================================================================= *)
(* Non-constructibility of irrational cubic equation solutions.              *)
(*                                                                           *)
(* This gives the two classic impossibility results: trisecting an angle or  *)
(* constructing the cube using traditional geometric constructions.          *)
(*                                                                           *)
(* This elementary proof (not using field extensions etc.) is taken from     *)
(* Dickson's "First Course in the Theory of Equations", chapter III.         *)
(* ========================================================================= *)

needs "Library/prime.ml";;
needs "Library/floor.ml";;
needs "Multivariate/transcendentals.ml";;

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* The critical lemma.                                                       *)
(* ------------------------------------------------------------------------- *)


let STEP_LEMMA = 
prove
 (`!P. (!n. P(&n)) /\
       (!x. P x ==> P(--x)) /\
       (!x. P x /\ ~(x = &0) ==> P(inv x)) /\
       (!x y. P x /\ P y ==> P(x + y)) /\
       (!x y. P x /\ P y ==> P(x * y))
       ==> !a b c z u v s.
               P a /\ P b /\ P c /\
               z pow 3 + a * z pow 2 + b * z + c = &0 /\
               P u /\ P v /\ P(s * s) /\ z = u + v * s
               ==> ?w. P w /\ w pow 3 + a * w pow 2 + b * w + c = &0`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
  ASM_CASES_TAC `v * s = &0` THENL
   [ASM_REWRITE_TAC[REAL_ADD_RID] THEN MESON_TAC[]; ALL_TAC] THEN
  STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
  MAP_EVERY ABBREV_TAC
   [`A = a * s pow 2 * v pow 2 + &3 * s pow 2 * u * v pow 2 +
         a * u pow 2 + u pow 3 +  b * u + c`;
    `B = s pow 2 * v pow 3 + &2 * a * u * v + &3 * u pow 2 * v + b * v`] THEN
  SUBGOAL_THEN `A + B * s = &0` ASSUME_TAC THENL
   [REPEAT(FIRST_X_ASSUM(MP_TAC o SYM)) THEN CONV_TAC REAL_RING; ALL_TAC] THEN
  ASM_CASES_TAC `(P:real->bool) s` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  SUBGOAL_THEN `B = &0` ASSUME_TAC THENL
   [UNDISCH_TAC `~P(s:real)` THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
    DISCH_TAC THEN REWRITE_TAC[] THEN
    FIRST_X_ASSUM(MP_TAC o MATCH_MP (REAL_FIELD
     `A + B * s = &0 ==> ~(B = &0) ==> s = --A / B`)) THEN
    ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
    REWRITE_TAC[real_div] THEN FIRST_ASSUM MATCH_MP_TAC THEN
    CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
    MAP_EVERY EXPAND_TAC ["A";
 "B"] THEN
    REWRITE_TAC[REAL_ARITH `x pow 3 = x * x * x`; REAL_POW_2] THEN
    REPEAT(FIRST_ASSUM MATCH_ACCEPT_TAC ORELSE
           (FIRST_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC));
    ALL_TAC] THEN
  EXISTS_TAC `--(a + &2 * u)` THEN ASM_SIMP_TAC[] THEN
  REPEAT(FIRST_X_ASSUM(MP_TAC o check ((not) o is_forall o concl))) THEN
  CONV_TAC REAL_RING);;

(* ------------------------------------------------------------------------- *)
(* Instantiate to square roots.                                              *)
(* ------------------------------------------------------------------------- *)


let STEP_LEMMA_SQRT = 
prove
 (`!P. (!n. P(&n)) /\
       (!x. P x ==> P(--x)) /\
       (!x. P x /\ ~(x = &0) ==> P(inv x)) /\
       (!x y. P x /\ P y ==> P(x + y)) /\
       (!x y. P x /\ P y ==> P(x * y))
       ==> !a b c z u v s.
               P a /\ P b /\ P c /\
               z pow 3 + a * z pow 2 + b * z + c = &0 /\
               P u /\ P v /\ P(s) /\ &0 <= s /\ z = u + v * sqrt(s)
               ==> ?w. P w /\ w pow 3 + a * w pow 2 + b * w + c = &0`,

  GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP STEP_LEMMA) THEN
  REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  ASM_MESON_TAC[SQRT_POW_2; REAL_POW_2]);;

(* ------------------------------------------------------------------------- *)
(* Numbers definable by radicals involving square roots only.                *)
(* ------------------------------------------------------------------------- *)

let radical_RULES,radical_INDUCT,radical_CASES = new_inductive_definition
 `(!x. rational x ==> radical x) /\
  (!x. radical x ==> radical (--x)) /\
  (!x. radical x /\ ~(x = &0) ==> radical (inv x)) /\
  (!x y. radical x /\ radical y ==> radical (x + y)) /\
  (!x y. radical x /\ radical y ==> radical (x * y)) /\
  (!x. radical x /\ &0 <= x ==> radical (sqrt x))`;;


let RADICAL_RULES = 
prove
 (`(!n. radical(&n)) /\
   (!x. rational x ==> radical x) /\
   (!x. radical x ==> radical (--x)) /\
   (!x. radical x /\ ~(x = &0) ==> radical (inv x)) /\
   (!x y. radical x /\ radical y ==> radical (x + y)) /\
   (!x y. radical x /\ radical y ==> radical (x - y)) /\
   (!x y. radical x /\ radical y ==> radical (x * y)) /\
   (!x y. radical x /\ radical y /\ ~(y = &0) ==> radical (x / y)) /\
   (!x n. radical x ==> radical(x pow n)) /\
   (!x. radical x /\ &0 <= x ==> radical (sqrt x))`,

  SIMP_TAC[real_div; real_sub; radical_RULES; RATIONAL_NUM] THEN
  GEN_TAC THEN INDUCT_TAC THEN
  ASM_SIMP_TAC[radical_RULES; real_pow; RATIONAL_NUM]);;

let RADICAL_TAC =
  REPEAT(MATCH_ACCEPT_TAC (CONJUNCT1 RADICAL_RULES) ORELSE
         (MAP_FIRST MATCH_MP_TAC(tl(tl(CONJUNCTS RADICAL_RULES))) THEN
          REPEAT CONJ_TAC));;

(* ------------------------------------------------------------------------- *)
(* Explicit "expressions" to support inductive proof.                        *)
(* ------------------------------------------------------------------------- *)


let expression_INDUCT,expression_RECURSION = define_type
 "expression = Constant real
             | Negation expression
             | Inverse expression
             | Addition expression expression
             | Multiplication expression expression
             | Sqrt expression";
;

(* ------------------------------------------------------------------------- *)
(* Interpretation.                                                           *)
(* ------------------------------------------------------------------------- *)


let value = define
 `(value(Constant x) = x) /\
  (value(Negation e) = --(value e)) /\
  (value(Inverse e) = inv(value e)) /\
  (value(Addition e1 e2) = value e1 + value e2) /\
  (value(Multiplication e1 e2) = value e1 * value e2) /\
  (value(Sqrt e) = sqrt(value e))`;;

(* ------------------------------------------------------------------------- *)
(* Wellformedness of an expression.                                          *)
(* ------------------------------------------------------------------------- *)


let wellformed = define
 `(wellformed(Constant x) <=> rational x) /\
  (wellformed(Negation e) <=> wellformed e) /\
  (wellformed(Inverse e) <=> ~(value e = &0) /\ wellformed e) /\
  (wellformed(Addition e1 e2) <=> wellformed e1 /\ wellformed e2) /\
  (wellformed(Multiplication e1 e2) <=> wellformed e1 /\ wellformed e2) /\
  (wellformed(Sqrt e) <=> &0 <= value e /\ wellformed e)`;;

(* ------------------------------------------------------------------------- *)
(* The set of radicals in an expression.                                     *)
(* ------------------------------------------------------------------------- *)


let radicals = define
 `(radicals(Constant x) = {}) /\
  (radicals(Negation e) = radicals e) /\
  (radicals(Inverse e) = radicals e) /\
  (radicals(Addition e1 e2) = (radicals e1) UNION (radicals e2)) /\
  (radicals(Multiplication e1 e2) = (radicals e1) UNION (radicals e2)) /\
  (radicals(Sqrt e) = e INSERT (radicals e))`;;


let FINITE_RADICALS = 
prove
 (`!e. FINITE(radicals e)`,

  MATCH_MP_TAC expression_INDUCT THEN
  SIMP_TAC[radicals; FINITE_RULES; FINITE_UNION]);;


let WELLFORMED_RADICALS = 
prove
 (`!e. wellformed e ==> !r. r IN radicals(e) ==> &0 <= value r`,

  MATCH_MP_TAC expression_INDUCT THEN
  REWRITE_TAC[radicals; wellformed; NOT_IN_EMPTY; IN_UNION; IN_INSERT] THEN
  MESON_TAC[]);;


let RADICALS_WELLFORMED = 
prove
 (`!e. wellformed e ==> !r. r IN radicals e ==> wellformed r`,

  MATCH_MP_TAC expression_INDUCT THEN
  REWRITE_TAC[radicals; wellformed; NOT_IN_EMPTY; IN_UNION; IN_INSERT] THEN
  MESON_TAC[]);;


let RADICALS_SUBSET = 
prove
 (`!e r. r IN radicals e ==> radicals(r) SUBSET radicals(e)`,

  MATCH_MP_TAC expression_INDUCT THEN
  REWRITE_TAC[radicals; IN_UNION; NOT_IN_EMPTY; IN_INSERT; SUBSET] THEN
  MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Show that every radical is the interpretation of a wellformed expresion.  *)
(* ------------------------------------------------------------------------- *)


let RADICAL_EXPRESSION = 
prove
 (`!x. radical x <=> ?e. wellformed e /\ x = value e`,

  GEN_TAC THEN EQ_TAC THEN SPEC_TAC(`x:real`,`x:real`) THENL
   [MATCH_MP_TAC radical_INDUCT THEN REPEAT STRIP_TAC THEN
    REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN ASM_MESON_TAC[value; wellformed];
    SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
    REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
    REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
    MATCH_MP_TAC expression_INDUCT THEN
    REWRITE_TAC[value; wellformed] THEN SIMP_TAC[radical_RULES]]);;

(* ------------------------------------------------------------------------- *)
(* Nesting depth of radicals in an expression.                               *)
(* ------------------------------------------------------------------------- *)


let LT_MAX = 
prove
 (`!a b c. a < MAX b c <=> a < b \/ a < c`,

  ARITH_TAC);;


let depth = define
 `(depth(Constant x) = 0) /\
  (depth(Negation e) = depth e) /\
  (depth(Inverse e) = depth e) /\
  (depth(Addition e1 e2) = MAX (depth e1) (depth e2)) /\
  (depth(Multiplication e1 e2) = MAX (depth e1) (depth e2)) /\
  (depth(Sqrt e) = 1 + depth e)`;;


let IN_RADICALS_SMALLER = 
prove
 (`!r s. s IN radicals(r) ==> depth(s) < depth(r)`,

  MATCH_MP_TAC expression_INDUCT THEN REWRITE_TAC[radicals; depth] THEN
  REWRITE_TAC[IN_UNION; NOT_IN_EMPTY; IN_INSERT; LT_MAX] THEN
  MESON_TAC[ARITH_RULE `s = a \/ s < a ==> s < 1 + a`]);;


let NOT_IN_OWN_RADICALS = 
prove
 (`!r. ~(r IN radicals r)`,


let RADICALS_EMPTY_RATIONAL = 
prove
 (`!e. wellformed e /\ radicals e = {} ==> rational(value e)`,

  MATCH_MP_TAC expression_INDUCT THEN
  REWRITE_TAC[wellformed; value; radicals; EMPTY_UNION; NOT_INSERT_EMPTY] THEN
  REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
  DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
  ASM_SIMP_TAC[RATIONAL_CLOSED]);;

(* ------------------------------------------------------------------------- *)
(* Crucial point about splitting off some "topmost" radical.                 *)
(* ------------------------------------------------------------------------- *)


let FINITE_MAX = 
prove
 (`!s. FINITE s ==> ~(s = {}) ==> ?b:num. b IN s /\ !a. a IN s ==> a <= b`,

  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  REWRITE_TAC[NOT_INSERT_EMPTY; IN_INSERT] THEN REPEAT GEN_TAC THEN
  ASM_CASES_TAC `s:num->bool = {}` THEN
  ASM_SIMP_TAC[NOT_IN_EMPTY; UNWIND_THM2; LE_REFL] THEN
  REWRITE_TAC[RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN
  MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;


let RADICAL_TOP = 
prove
 (`!e. ~(radicals e = {})
       ==> ?r. r IN radicals e /\
               !s. s IN radicals(e) ==> ~(r IN radicals s)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `IMAGE depth (radicals e)` FINITE_MAX) THEN
  ASM_SIMP_TAC[IMAGE_EQ_EMPTY; FINITE_IMAGE; FINITE_RADICALS] THEN
  REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE] THEN
  MESON_TAC[IN_RADICALS_SMALLER; NOT_LT]);;

(* ------------------------------------------------------------------------- *)
(* By rearranging the expression we can use it in a canonical way.           *)
(* ------------------------------------------------------------------------- *)


let RADICAL_CANONICAL_TRIVIAL = 
prove
 (`!e r.
     (r IN radicals e
            ==> (?a b.
                   wellformed a /\
                   wellformed b /\
                   value e = value a + value b * sqrt (value r) /\
                   radicals a SUBSET radicals e DELETE r /\
                   radicals b SUBSET radicals e DELETE r /\
                   radicals r SUBSET radicals e DELETE r))
     ==> wellformed e
         ==> ?a b. wellformed a /\
                   wellformed b /\
                   value e = value a + value b * sqrt (value r) /\
                   radicals a SUBSET (radicals e UNION radicals r) DELETE r /\
                   radicals b SUBSET (radicals e UNION radicals r) DELETE r /\
                   radicals r SUBSET (radicals e UNION radicals r) DELETE r`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `r IN radicals e` THEN ASM_SIMP_TAC[] THENL
   [DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
    REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN SET_TAC[];
    DISCH_TAC THEN
    MAP_EVERY EXISTS_TAC [`e:expression`; `Constant(&0)`] THEN
    ASM_REWRITE_TAC[wellformed; value; radicals] THEN
    REWRITE_TAC[RATIONAL_NUM; REAL_MUL_LZERO; REAL_ADD_RID] THEN
    UNDISCH_TAC `~(r IN radicals e)` THEN
    MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN SET_TAC[]]);;


let RADICAL_CANONICAL = 
prove
 (`!e. wellformed e /\ ~(radicals e = {})
       ==> ?r. r IN radicals(e) /\
               ?a b. wellformed(Addition a (Multiplication b (Sqrt r))) /\
                     value e = value(Addition a (Multiplication b (Sqrt r))) /\
                     (radicals a) SUBSET (radicals(e) DELETE r) /\
                     (radicals b) SUBSET (radicals(e) DELETE r) /\
                     (radicals r) SUBSET (radicals(e) DELETE r)`,

  REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP RADICAL_TOP) THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:expression` THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `&0 <= value r /\ wellformed r` STRIP_ASSUME_TAC THENL
   [ASM_MESON_TAC[WELLFORMED_RADICALS; RADICALS_WELLFORMED]; ALL_TAC] THEN
  MAP_EVERY UNDISCH_TAC [`wellformed e`; `r IN radicals e`] THEN
  ASM_REWRITE_TAC[IMP_IMP; wellformed; value; GSYM CONJ_ASSOC] THEN
  SPEC_TAC(`e:expression`,`e:expression`) THEN
  MATCH_MP_TAC expression_INDUCT THEN
  REWRITE_TAC[wellformed; radicals; value; NOT_IN_EMPTY] THEN
  REWRITE_TAC[IN_INSERT; IN_UNION] THEN REPEAT CONJ_TAC THEN
  X_GEN_TAC `e1:expression` THEN TRY(X_GEN_TAC `e2:expression`) THENL
   [DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
    ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`a:expression`; `b:expression`] THEN
    STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`Negation a`; `Negation b`] THEN
    ASM_REWRITE_TAC[value; wellformed; radicals] THEN REAL_ARITH_TAC;

    DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
    ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`a:expression`; `b:expression`] THEN
    ASM_CASES_TAC `value b * sqrt(value r) = value a` THENL
     [ASM_REWRITE_TAC[] THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
      MAP_EVERY EXISTS_TAC
       [`Inverse(Multiplication (Constant(&2)) a)`; `Constant(&0)`] THEN
      ASM_REWRITE_TAC[value; radicals; wellformed] THEN
      REWRITE_TAC[RATIONAL_NUM; EMPTY_SUBSET; CONJ_ASSOC] THEN CONJ_TAC THENL
       [UNDISCH_TAC `~(value a + value a = &0)` THEN CONV_TAC REAL_FIELD;
        REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]];
      ALL_TAC] THEN
    STRIP_TAC THEN MAP_EVERY EXISTS_TAC
     [`Multiplication a (Inverse
        (Addition (Multiplication a a)
                  (Multiplication (Multiplication b b) (Negation r))))`;
      `Multiplication (Negation b) (Inverse
        (Addition (Multiplication a a)
                  (Multiplication (Multiplication b b) (Negation r))))`] THEN
    ASM_REWRITE_TAC[value; wellformed; radicals; UNION_SUBSET] THEN
    UNDISCH_TAC `~(value b * sqrt (value r) = value a)` THEN
    UNDISCH_TAC `~(value e1 = &0)` THEN ASM_REWRITE_TAC[] THEN
    FIRST_ASSUM(MP_TAC o MATCH_MP SQRT_POW_2) THEN CONV_TAC REAL_FIELD;

    REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
    REWRITE_TAC[FORALL_AND_THM] THEN
    DISCH_THEN(fun th ->
      DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN MP_TAC th) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
      MATCH_MP RADICAL_CANONICAL_TRIVIAL)) THEN
    ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[IMP_IMP] THEN
    DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
    REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
    REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC
     [`a1:expression`; `b1:expression`; `a2:expression`; `b2:expression`] THEN
    STRIP_TAC THEN MAP_EVERY EXISTS_TAC
     [`Addition a1 a2`; `Addition b1 b2`] THEN
    ASM_REWRITE_TAC[value; wellformed; radicals] THEN
    CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
    MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN
    MP_TAC(SPECL [`e1:expression`; `r:expression`] RADICALS_SUBSET) THEN
    MP_TAC(SPECL [`e2:expression`; `r:expression`] RADICALS_SUBSET) THEN
    REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[];

    REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
    REWRITE_TAC[FORALL_AND_THM] THEN
    DISCH_THEN(fun th ->
      DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN MP_TAC th) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
      MATCH_MP RADICAL_CANONICAL_TRIVIAL)) THEN
    ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[IMP_IMP] THEN
    DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
    REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
    REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC
     [`a1:expression`; `b1:expression`; `a2:expression`; `b2:expression`] THEN
    STRIP_TAC THEN MAP_EVERY EXISTS_TAC
     [`Addition (Multiplication a1 a2)
                (Multiplication (Multiplication b1 b2) r)`;
      `Addition (Multiplication a1 b2) (Multiplication a2 b1)`] THEN
    ASM_REWRITE_TAC[value; wellformed; radicals] THEN CONJ_TAC THENL
     [FIRST_ASSUM(MP_TAC o MATCH_MP SQRT_POW_2) THEN CONV_TAC REAL_RING;
      ALL_TAC] THEN
    MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN
    MP_TAC(SPECL [`e1:expression`; `r:expression`] RADICALS_SUBSET) THEN
    MP_TAC(SPECL [`e2:expression`; `r:expression`] RADICALS_SUBSET) THEN
    REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[];

    REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
    REWRITE_TAC[FORALL_AND_THM] THEN
    DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
    REPEAT(DISCH_THEN(K ALL_TAC)) THEN
    MAP_EVERY EXISTS_TAC [`Constant(&0)`; `Constant(&1)`] THEN
    REWRITE_TAC[wellformed; value; REAL_ADD_LID; REAL_MUL_LID] THEN
    REWRITE_TAC[radicals; RATIONAL_NUM] THEN
    MP_TAC(SPEC `r:expression` NOT_IN_OWN_RADICALS) THEN ASM SET_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Now we quite easily get an inductive argument.                            *)
(* ------------------------------------------------------------------------- *)


let CUBIC_ROOT_STEP = 
prove
 (`!a b c. rational a /\ rational b /\ rational c
           ==> !e. wellformed e /\
                   ~(radicals e = {}) /\
                   (value e) pow 3 + a * (value e) pow 2 +
                                     b * (value e) + c = &0
                   ==> ?e'. wellformed e' /\
                            (radicals e') PSUBSET (radicals e) /\
                            (value e') pow 3 + a * (value e') pow 2 +
                                     b * (value e') + c = &0`,

  REPEAT STRIP_TAC THEN MP_TAC(SPEC `e:expression` RADICAL_CANONICAL) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN
   (X_CHOOSE_THEN `r:expression` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`eu:expression`; `ev:expression`] THEN
  STRIP_TAC THEN
  MP_TAC(SPEC `\x. ?ex. wellformed ex /\
                        radicals ex SUBSET (radicals(e) DELETE r) /\
                        value ex = x`
              STEP_LEMMA_SQRT) THEN
  REWRITE_TAC[] THEN ANTS_TAC THENL
   [REPEAT CONJ_TAC THENL
     [X_GEN_TAC `n:num` THEN EXISTS_TAC `Constant(&n)` THEN
      REWRITE_TAC[wellformed; radicals; RATIONAL_NUM; value; EMPTY_SUBSET];
      X_GEN_TAC `x:real` THEN
      DISCH_THEN(X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC) THEN
      EXISTS_TAC `Negation ex` THEN
      ASM_REWRITE_TAC[wellformed; radicals; value];
      X_GEN_TAC `x:real` THEN
      DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
      DISCH_THEN(X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC) THEN
      EXISTS_TAC `Inverse ex` THEN
      ASM_REWRITE_TAC[wellformed; radicals; value];
      MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN
      DISCH_THEN(CONJUNCTS_THEN2
       (X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC)
       (X_CHOOSE_THEN `ey:expression` STRIP_ASSUME_TAC)) THEN
      EXISTS_TAC `Addition ex ey` THEN
      ASM_REWRITE_TAC[wellformed; radicals; value; UNION_SUBSET];
      MAP_EVERY X_GEN_TAC [`x:real`; `y:real`] THEN
      DISCH_THEN(CONJUNCTS_THEN2
       (X_CHOOSE_THEN `ex:expression` STRIP_ASSUME_TAC)
       (X_CHOOSE_THEN `ey:expression` STRIP_ASSUME_TAC)) THEN
      EXISTS_TAC `Multiplication ex ey` THEN
      ASM_REWRITE_TAC[wellformed; radicals; value; UNION_SUBSET]];
    ALL_TAC] THEN
  DISCH_THEN(MP_TAC o SPECL
   [`a:real`; `b:real`; `c:real`;
    `value e`; `value eu`; `value ev`; `value r`]) THEN
  ANTS_TAC THENL
   [CONJ_TAC THENL
     [EXISTS_TAC `Constant a` THEN
      ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [EXISTS_TAC `Constant b` THEN
      ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [EXISTS_TAC `Constant c` THEN
      ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
      ALL_TAC] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[wellformed]) THEN
    ASM_REWRITE_TAC[value] THEN ASM_MESON_TAC[];
    ALL_TAC] THEN
  DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e':expression` THEN
  ASM_SIMP_TAC[] THEN ASM SET_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Hence the main result.                                                    *)
(* ------------------------------------------------------------------------- *)


let CUBIC_ROOT_RADICAL_INDUCT = 
prove
 (`!a b c. rational a /\ rational b /\ rational c
           ==> !n e. wellformed e /\ CARD (radicals e) = n /\
                     (value e) pow 3 + a * (value e) pow 2 +
                                b * (value e) + c = &0
                 ==> ?x. rational x /\
                         x pow 3 + a * x pow 2 + b * x + c = &0`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN
  X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `e:expression` THEN
  STRIP_TAC THEN ASM_CASES_TAC `radicals e = {}` THENL
   [ASM_MESON_TAC[RADICALS_EMPTY_RATIONAL]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_STEP) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `e:expression`) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `e':expression` STRIP_ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `CARD(radicals e')`) THEN ANTS_TAC THENL
   [REWRITE_TAC[SYM(ASSUME `CARD(radicals e) = n`)] THEN
    MATCH_MP_TAC CARD_PSUBSET THEN ASM_REWRITE_TAC[FINITE_RADICALS];
    DISCH_THEN MATCH_MP_TAC THEN EXISTS_TAC `e':expression` THEN
    ASM_REWRITE_TAC[]]);;


let CUBIC_ROOT_RATIONAL = 
prove
 (`!a b c. rational a /\ rational b /\ rational c /\
           (?x. radical x /\ x pow 3 + a * x pow 2 + b * x + c = &0)
           ==> (?x. rational x /\ x pow 3 + a * x pow 2 + b * x + c = &0)`,

  REWRITE_TAC[RADICAL_EXPRESSION] THEN REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_RADICAL_INDUCT) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
  MAP_EVERY EXISTS_TAC [`CARD(radicals e)`; `e:expression`] THEN
  ASM_MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Now go further to an *integer*, since the polynomial is monic.            *)
(* ------------------------------------------------------------------------- *)

prioritize_num();;


let RATIONAL_LOWEST_LEMMA = 
prove
 (`!p q. ~(q = 0) ==> ?p' q'. ~(q' = 0) /\ coprime(p',q') /\ p * q' = p' * q`,

  ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN MATCH_MP_TAC num_WF THEN
  X_GEN_TAC `q:num` THEN DISCH_TAC THEN X_GEN_TAC `p:num` THEN DISCH_TAC THEN
  ASM_CASES_TAC `coprime(p,q)` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [coprime]) THEN
  REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; GSYM CONJ_ASSOC] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` MP_TAC) THEN
  ASM_CASES_TAC `d = 0` THEN ASM_REWRITE_TAC[DIVIDES_ZERO] THEN
  REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `p':num` SUBST_ALL_TAC)
   (CONJUNCTS_THEN2 (X_CHOOSE_THEN `q':num` SUBST_ALL_TAC) ASSUME_TAC)) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `q':num`) THEN
  RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
  GEN_REWRITE_TAC (funpow 2 LAND_CONV) [ARITH_RULE `a < b <=> 1 * a < b`] THEN
  ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
  ASM_SIMP_TAC[ARITH_RULE `~(d = 0) /\ ~(d = 1) ==> 1 < d`] THEN
  DISCH_THEN(MP_TAC o SPEC `p':num`) THEN
  REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN SIMP_TAC[] THEN
  CONV_TAC NUM_RING);;

prioritize_real();;


let RATIONAL_LOWEST = 
prove
 (`!x. rational x <=> ?p q. ~(q = 0) /\ coprime(p,q) /\ abs(x) = &p / &q`,

  GEN_TAC THEN REWRITE_TAC[RATIONAL_ALT] THEN EQ_TAC THENL
   [ALL_TAC; MESON_TAC[]] THEN
  STRIP_TAC THEN MP_TAC(SPECL [`p:num`; `q:num`] RATIONAL_LOWEST_LEMMA) THEN
  ASM_REWRITE_TAC[] THEN REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
  UNDISCH_TAC `~(q = 0)` THEN SIMP_TAC[GSYM REAL_OF_NUM_EQ] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN CONV_TAC REAL_FIELD);;


let RATIONAL_ROOT_INTEGER = 
prove
 (`!a b c x. integer a /\ integer b /\ integer c /\ rational x /\
             x pow 3 + a * x pow 2 + b * x + c = &0
             ==> integer x`,

  REWRITE_TAC[RATIONAL_LOWEST; GSYM REAL_OF_NUM_EQ] THEN
  REPEAT STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP(REAL_ARITH
   `abs x = a ==> x = a \/ x = --a`)) THEN
  DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o check (is_eq o concl)) THEN
  ASM_SIMP_TAC[REAL_FIELD
   `~(q = &0)
     ==> ((p / q) pow 3 + a * (p / q) pow 2 + b * (p / q) + c = &0 <=>
          (p pow 3 = q * --(a * p pow 2 + b * p * q + c * q pow 2))) /\
         ((--(p / q)) pow 3 + a * (--(p / q)) pow 2 +
           b * (--(p / q)) + c = &0 <=>
          p pow 3 = q * (a * p pow 2 - b * p * q + c * q pow 2))`] THEN
  (W(fun(asl,w) ->
       SUBGOAL_THEN(mk_comb(`integer`,rand(rand(lhand w)))) MP_TAC THENL
    [REPEAT(MAP_FIRST MATCH_MP_TAC (tl(CONJUNCTS INTEGER_CLOSED)) THEN
            REPEAT CONJ_TAC) THEN
     ASM_REWRITE_TAC[INTEGER_CLOSED];
     ALL_TAC])) THEN
  REWRITE_TAC[integer] THEN DISCH_THEN(X_CHOOSE_TAC `i:num`) THEN
  DISCH_THEN(MP_TAC o AP_TERM `abs`) THEN
  ASM_REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NEG] THEN
  REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM; REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_EQ] THEN
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_SYM]) THEN
  DISCH_THEN(MP_TAC o SPEC `3` o MATCH_MP COPRIME_EXP) THEN
  REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `q:num`) THEN
  ASM_CASES_TAC `q = 1` THEN
  ASM_SIMP_TAC[REAL_DIV_1; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL] THEN
  MESON_TAC[divides; DIVIDES_REFL]);;

(* ------------------------------------------------------------------------- *)
(* Hence we have our big final theorem.                                      *)
(* ------------------------------------------------------------------------- *)


let CUBIC_ROOT_INTEGER = 
prove
 (`!a b c. integer a /\ integer b /\ integer c /\
           (?x. radical x /\ x pow 3 + a * x pow 2 + b * x + c = &0)
           ==> (?x. integer x /\ x pow 3 + a * x pow 2 + b * x + c = &0)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`a:real`; `b:real`; `c:real`] CUBIC_ROOT_RATIONAL) THEN
  ASM_SIMP_TAC[RATIONAL_INTEGER] THEN
  ASM_MESON_TAC[RATIONAL_ROOT_INTEGER]);;

(* ------------------------------------------------------------------------- *)
(* Geometrical definitions.                                                  *)
(* ------------------------------------------------------------------------- *)


let length = new_definition
  `length(a:real^2,b:real^2) = norm(b - a)`;;


let parallel = new_definition
 `parallel (a:real^2,b:real^2) (c:real^2,d:real^2) <=>
        (a$1 - b$1) * (c$2 - d$2) = (a$2 - b$2) * (c$1 - d$1)`;;


let collinear3 = new_definition
  `collinear3 (a:real^2) b c <=> parallel (a,b) (a,c)`;;


let is_intersection = new_definition
  `is_intersection p (a,b) (c,d) <=> collinear3 a p b /\ collinear3 c p d`;;


let on_circle = new_definition
 `on_circle x (centre,pt) <=> length(centre,x) = length(centre,pt)`;;

(* ------------------------------------------------------------------------- *)
(* A trivial lemma.                                                          *)
(* ------------------------------------------------------------------------- *)


let SQRT_CASES_LEMMA = 
prove
 (`!x y. y pow 2 = x ==> &0 <= x /\ (sqrt(x) = y \/ sqrt(x) = --y)`,

  REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
  MP_TAC(SPEC `y:real` (GEN_ALL POW_2_SQRT)) THEN
  MP_TAC(SPEC `--y` (GEN_ALL POW_2_SQRT)) THEN
  REWRITE_TAC[GSYM REAL_POW_2; REAL_POW_NEG; ARITH] THEN REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Show that solutions to certain classes of equations are radical.          *)
(* ------------------------------------------------------------------------- *)


let RADICAL_LINEAR_EQUATION = 
prove
 (`!a b x. radical a /\ radical b /\ ~(a = &0 /\ b = &0) /\ a * x + b = &0
           ==> radical x`,

  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `~(a = &0) /\ x = --b / a`
   (fun th -> ASM_SIMP_TAC[th; RADICAL_RULES]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD);;


let RADICAL_SIMULTANEOUS_LINEAR_EQUATION = 
prove
 (`!a b c d e f x.
        radical a /\ radical b /\ radical c /\
        radical d /\ radical e /\ radical f /\
        ~(a * e = b * d /\ a * f = c * d /\ e * c = b * f) /\
        a * x + b * y = c /\ d * x + e * y = f
        ==> radical(x) /\ radical(y)`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN
   `~(a * e - b * d = &0) /\
    x = (e * c - b * f) / (a * e - b * d) /\
    y = (a * f - d * c) / (a * e - b * d)`
  STRIP_ASSUME_TAC THENL
   [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;
    ASM_SIMP_TAC[RADICAL_RULES]]);;


let RADICAL_QUADRATIC_EQUATION = 
prove
 (`!a b c x. radical a /\ radical b /\ radical c /\
             a * x pow 2 + b * x + c = &0 /\
             ~(a = &0 /\ b = &0 /\ c = &0)
             ==> radical x`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `a = &0` THEN ASM_REWRITE_TAC[] THENL
   [ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
    MESON_TAC[RADICAL_LINEAR_EQUATION];
    ALL_TAC] THEN
  STRIP_TAC THEN MATCH_MP_TAC RADICAL_LINEAR_EQUATION THEN
  EXISTS_TAC `&2 * a` THEN
  ASM_SIMP_TAC[RADICAL_RULES; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN
  SUBGOAL_THEN `&0 <= b pow 2 - &4 * a * c /\
                ((&2 * a) * x + (b - sqrt(b pow 2 - &4 * a * c)) = &0 \/
                 (&2 * a) * x + (b + sqrt(b pow 2 - &4 * a * c)) = &0)`
  MP_TAC THENL
   [REWRITE_TAC[real_sub; REAL_ARITH `a + (b + c) = &0 <=> c = --(a + b)`] THEN
    REWRITE_TAC[REAL_EQ_NEG2] THEN MATCH_MP_TAC SQRT_CASES_LEMMA THEN
    FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC REAL_RING;
    STRIP_TAC THENL
     [EXISTS_TAC `b - sqrt(b pow 2 - &4 * a * c)`;
      EXISTS_TAC `b + sqrt(b pow 2 - &4 * a * c)`] THEN
    ASM_REWRITE_TAC[] THEN RADICAL_TAC THEN ASM_REWRITE_TAC[]]);;


let RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC = 
prove
 (`!a b c d e f x.
        radical a /\ radical b /\ radical c /\
        radical d /\ radical e /\ radical f /\
        ~(d = &0 /\ e = &0 /\ f = &0) /\
        (x - a) pow 2 + (y - b) pow 2 = c /\ d * x + e * y = f
        ==> radical x /\ radical y`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `d pow 2 + e pow 2` RADICAL_QUADRATIC_EQUATION) THEN
  DISCH_THEN MATCH_MP_TAC THENL
   [EXISTS_TAC `&2 * b * d * e - &2 * a * e pow 2 - &2 * d * f` THEN
    EXISTS_TAC `b pow 2 * e pow 2 + a pow 2 * e pow 2 +
                f pow 2 - c * e pow 2 - &2 * b * e * f`;
    EXISTS_TAC `&2 * a * d * e - &2 * b * d pow 2 - &2 * f * e` THEN
    EXISTS_TAC `a pow 2 * d pow 2 + b pow 2 * d pow 2 +
                f pow 2 - c * d pow 2 - &2 * a * d * f`] THEN
  (REPLICATE_TAC 3
    (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
   CONJ_TAC THENL
    [REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING; ALL_TAC] THEN
   REWRITE_TAC[REAL_SOS_EQ_0] THEN REPEAT(POP_ASSUM MP_TAC) THEN
   CONV_TAC REAL_RING));;


let RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC = 
prove
 (`!a b c d e f x.
        radical a /\ radical b /\ radical c /\
        radical d /\ radical e /\ radical f /\
        ~(a = d /\ b = e /\ c = f) /\
        (x - a) pow 2 + (y - b) pow 2 = c /\
        (x - d) pow 2 + (y - e) pow 2 = f
        ==> radical x /\ radical y`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN
  MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC THEN
  MAP_EVERY EXISTS_TAC
   [`a:real`; `b:real`; `c:real`; `&2 * (d - a)`; `&2 * (e - b)`;
    `(d pow 2 - a pow 2) + (e pow 2 - b pow 2) + (c - f)`] THEN
  ASM_REWRITE_TAC[] THEN
  REPLICATE_TAC 3
   (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;

(* ------------------------------------------------------------------------- *)
(* Analytic criterion for constructibility.                                  *)
(* ------------------------------------------------------------------------- *)

let constructible_RULES,constructible_INDUCT,constructible_CASES =
 new_inductive_definition
  `(!x:real^2. rational(x$1) /\ rational(x$2) ==> constructible x) /\
// Intersection of two non-parallel lines AB and CD
  (!a b c d x. constructible a /\ constructible b /\
               constructible c /\ constructible d /\
               ~parallel (a,b) (c,d) /\ is_intersection x (a,b) (c,d)
               ==> constructible x) /\
// Intersection of a nontrivial line AB and circle with centre C, radius DE
  (!a b c d e x. constructible a /\ constructible b /\
                 constructible c /\ constructible d /\
                 constructible e /\
                 ~(a = b) /\ collinear3 a x b /\ length (c,x) = length(d,e)
                 ==> constructible x) /\
// Intersection of distinct circles with centres A and D, radii BD and EF
  (!a b c d e f x. constructible a /\ constructible b /\
                   constructible c /\ constructible d /\
                   constructible e /\ constructible f /\
                   ~(a = d /\ length (b,c) = length (e,f)) /\
                   length (a,x) = length (b,c) /\ length (d,x) = length (e,f)
                   ==> constructible x)`;;

(* ------------------------------------------------------------------------- *)
(* Some "coordinate geometry" lemmas.                                        *)
(* ------------------------------------------------------------------------- *)


let RADICAL_LINE_LINE_INTERSECTION = 
prove
 (`!a b c d x.
        radical(a$1) /\ radical(a$2) /\
        radical(b$1) /\ radical(b$2) /\
        radical(c$1) /\ radical(c$2) /\
        radical(d$1) /\ radical(d$2) /\
        ~(parallel (a,b) (c,d)) /\ is_intersection x (a,b) (c,d)
        ==> radical(x$1) /\ radical(x$2)`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[parallel; collinear3; is_intersection] THEN STRIP_TAC THEN
  MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_EQUATION THEN
  MAP_EVERY EXISTS_TAC
   [`(b:real^2)$2 - (a:real^2)$2`; `(a:real^2)$1 - (b:real^2)$1`;
    `(a:real^2)$2 * (a$1 - (b:real^2)$1) - (a:real^2)$1 * (a$2 - b$2)`;
    `(d:real^2)$2 - (c:real^2)$2`; `(c:real^2)$1 - (d:real^2)$1`;
    `(c:real^2)$2 * (c$1 - (d:real^2)$1) - (c:real^2)$1 * (c$2 - d$2)`] THEN
  REPLICATE_TAC 6
   (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;


let RADICAL_LINE_CIRCLE_INTERSECTION = 
prove
 (`!a b c d e x.
        radical(a$1) /\ radical(a$2) /\
        radical(b$1) /\ radical(b$2) /\
        radical(c$1) /\ radical(c$2) /\
        radical(d$1) /\ radical(d$2) /\
        radical(e$1) /\ radical(e$2) /\
        ~(a = b) /\ collinear3 a x b /\ length(c,x) = length(d,e)
        ==> radical(x$1) /\ radical(x$2)`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[length; NORM_EQ; collinear3; parallel] THEN
  SIMP_TAC[CART_EQ; FORALL_2; dot; SUM_2; DIMINDEX_2; VECTOR_SUB_COMPONENT;
           GSYM REAL_POW_2] THEN
  STRIP_TAC THEN MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC THEN
  MAP_EVERY EXISTS_TAC
   [`(c:real^2)$1`; `(c:real^2)$2`;
    `((e:real^2)$1 - (d:real^2)$1) pow 2 + (e$2 - d$2) pow 2`;
    `(b:real^2)$2 - (a:real^2)$2`;
    `(a:real^2)$1 - (b:real^2)$1`;
    `a$2 * ((a:real^2)$1 - (b:real^2)$1) - a$1 * (a$2 - b$2)`] THEN
  REPLICATE_TAC 6
   (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;


let RADICAL_CIRCLE_CIRCLE_INTERSECTION = 
prove
 (`!a b c d e f x.
        radical(a$1) /\ radical(a$2) /\
        radical(b$1) /\ radical(b$2) /\
        radical(c$1) /\ radical(c$2) /\
        radical(d$1) /\ radical(d$2) /\
        radical(e$1) /\ radical(e$2) /\
        radical(f$1) /\ radical(f$2) /\
        length(a,x) = length(b,c) /\
        length(d,x) = length(e,f) /\
        ~(a = d /\ length(b,c) = length(e,f))
        ==> radical(x$1) /\ radical(x$2)`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[length; NORM_EQ; collinear3; parallel] THEN
  SIMP_TAC[CART_EQ; FORALL_2; dot; SUM_2; DIMINDEX_2; VECTOR_SUB_COMPONENT;
           GSYM REAL_POW_2] THEN
  STRIP_TAC THEN MATCH_MP_TAC RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC THEN
  MAP_EVERY EXISTS_TAC
   [`(a:real^2)$1`; `(a:real^2)$2`;
    `((c:real^2)$1 - (b:real^2)$1) pow 2 + (c$2 - b$2) pow 2`;
    `(d:real^2)$1`; `(d:real^2)$2`;
    `((f:real^2)$1 - (e:real^2)$1) pow 2 + (f$2 - e$2) pow 2`] THEN
  REPLICATE_TAC 6
   (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;

(* ------------------------------------------------------------------------- *)
(* So constructible points have radical coordinates.                         *)
(* ------------------------------------------------------------------------- *)


let CONSTRUCTIBLE_RADICAL = 
prove
 (`!x. constructible x ==> radical(x$1) /\ radical(x$2)`,

  MATCH_MP_TAC constructible_INDUCT THEN REPEAT CONJ_TAC THEN
  REPEAT GEN_TAC THEN STRIP_TAC THENL
   [ASM_SIMP_TAC[RADICAL_RULES];
    MATCH_MP_TAC RADICAL_LINE_LINE_INTERSECTION THEN ASM_MESON_TAC[];
    MATCH_MP_TAC RADICAL_LINE_CIRCLE_INTERSECTION THEN ASM_MESON_TAC[];
    MATCH_MP_TAC RADICAL_CIRCLE_CIRCLE_INTERSECTION THEN ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Impossibility of doubling the cube.                                       *)
(* ------------------------------------------------------------------------- *)


let DOUBLE_THE_CUBE_ALGEBRA = 
prove
 (`~(?x. radical x /\ x pow 3 = &2)`,

  STRIP_TAC THEN MP_TAC(SPECL [`&0`; `&0`; `-- &2`] CUBIC_ROOT_INTEGER) THEN
  SIMP_TAC[INTEGER_CLOSED; NOT_IMP] THEN
  REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
  REWRITE_TAC[GSYM real_sub; REAL_SUB_0] THEN
  CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o AP_TERM `abs`) THEN
  REWRITE_TAC[REAL_ABS_POW] THEN
  FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[integer]) THEN
  REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_POW; REAL_OF_NUM_EQ] THEN
  MATCH_MP_TAC(ARITH_RULE
   `n EXP 3 <= 1 EXP 3 \/ 2 EXP 3 <= n EXP 3 ==> ~(n EXP 3 = 2)`) THEN
  REWRITE_TAC[num_CONV `3`; EXP_MONO_LE_SUC] THEN ARITH_TAC);;


let DOUBLE_THE_CUBE = 
prove
 (`!x. x pow 3 = &2 ==> ~(constructible(vector[x; &0]))`,

  GEN_TAC THEN DISCH_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP CONSTRUCTIBLE_RADICAL) THEN
  REWRITE_TAC[VECTOR_2; RADICAL_RULES] THEN
  ASM_MESON_TAC[DOUBLE_THE_CUBE_ALGEBRA]);;

(* ------------------------------------------------------------------------- *)
(* Impossibility of trisecting                                               *)
(* ------------------------------------------------------------------------- *)


let COS_TRIPLE = 
prove
 (`!x. cos(&3 * x) = &4 * cos(x) pow 3 - &3 * cos(x)`,

  GEN_TAC THEN
  REWRITE_TAC[REAL_ARITH `&3 * x = x + x + x`; SIN_ADD; COS_ADD] THEN
  MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;


let COS_PI3 = 
prove
 (`cos(pi / &3) = &1 / &2`,

  MP_TAC(SPEC `pi / &3` COS_TRIPLE) THEN
  SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH; COS_PI] THEN
  REWRITE_TAC[REAL_RING
   `-- &1 = &4 * c pow 3 - &3 * c <=> c = &1 / &2 \/ c = -- &1`] THEN
  DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC MP_TAC) THEN
  MP_TAC(SPEC `pi / &3` COS_POS_PI) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);;


let TRISECT_60_DEGREES_ALGEBRA = 
prove
 (`~(?x. radical x /\ x pow 3 - &3 * x - &1 = &0)`,

  STRIP_TAC THEN MP_TAC(SPECL [`&0`; `-- &3`; `-- &1`] CUBIC_ROOT_INTEGER) THEN
  SIMP_TAC[INTEGER_CLOSED; NOT_IMP] THEN REWRITE_TAC[REAL_ADD_ASSOC] THEN
  REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; REAL_MUL_LNEG; GSYM real_sub] THEN
  CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH
   `x pow 3 - &3 * x - &1 = &0 <=> x * (x pow 2 - &3) = &1`] THEN
  POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o AP_TERM `abs`) THEN
  REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
  ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
  FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[integer]) THEN
  REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC (ARITH_RULE
   `n = 0 \/ n = 1 \/ n = 2 + (n - 2)`) THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
  REWRITE_TAC[REAL_ARITH `(&2 + m) pow 2 - &3 = m pow 2 + &4 * m + &1`] THEN
  REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_POW; REAL_ABS_NUM;
              REAL_OF_NUM_EQ; MULT_EQ_1] THEN
  ARITH_TAC);;


let TRISECT_60_DEGREES = 
prove
 (`!y. ~(constructible(vector[cos(pi / &9); y]))`,

  GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CONSTRUCTIBLE_RADICAL) THEN
  DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[VECTOR_2] THEN
  DISCH_TAC THEN MP_TAC(SPEC `pi / &9` COS_TRIPLE) THEN
  SIMP_TAC[REAL_ARITH `&3 * x / &9 = x / &3`; COS_PI3] THEN
  REWRITE_TAC[REAL_ARITH
   `&1 / &2 = &4 * c pow 3 - &3 * c <=>
    (&2 * c) pow 3 - &3 * (&2 * c) - &1 = &0`] THEN
  ASM_MESON_TAC[TRISECT_60_DEGREES_ALGEBRA; RADICAL_RULES]);;