1 (* ========================================================================= *)
2 (* Non-constructibility of irrational cubic equation solutions. *)
4 (* This gives the two classic impossibility results: trisecting an angle or *)
5 (* constructing the cube using traditional geometric constructions. *)
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 (* ========================================================================= *)
11 needs "Library/prime.ml";;
12 needs "Library/floor.ml";;
13 needs "Multivariate/transcendentals.ml";;
17 (* ------------------------------------------------------------------------- *)
18 (* The critical lemma. *)
19 (* ------------------------------------------------------------------------- *)
21 let STEP_LEMMA = prove
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))
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
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));
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
60 (* ------------------------------------------------------------------------- *)
61 (* Instantiate to square roots. *)
62 (* ------------------------------------------------------------------------- *)
64 let STEP_LEMMA_SQRT = prove
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))
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]);;
79 (* ------------------------------------------------------------------------- *)
80 (* Numbers definable by radicals involving square roots only. *)
81 (* ------------------------------------------------------------------------- *)
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))`;;
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]);;
107 REPEAT(MATCH_ACCEPT_TAC (CONJUNCT1 RADICAL_RULES) ORELSE
108 (MAP_FIRST MATCH_MP_TAC(tl(tl(CONJUNCTS RADICAL_RULES))) THEN
111 (* ------------------------------------------------------------------------- *)
112 (* Explicit "expressions" to support inductive proof. *)
113 (* ------------------------------------------------------------------------- *)
115 let expression_INDUCT,expression_RECURSION = define_type
116 "expression = Constant real
117 | Negation expression
119 | Addition expression expression
120 | Multiplication expression expression
123 (* ------------------------------------------------------------------------- *)
124 (* Interpretation. *)
125 (* ------------------------------------------------------------------------- *)
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))`;;
135 (* ------------------------------------------------------------------------- *)
136 (* Wellformedness of an expression. *)
137 (* ------------------------------------------------------------------------- *)
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)`;;
147 (* ------------------------------------------------------------------------- *)
148 (* The set of radicals in an expression. *)
149 (* ------------------------------------------------------------------------- *)
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))`;;
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]);;
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
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
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
182 (* ------------------------------------------------------------------------- *)
183 (* Show that every radical is the interpretation of a wellformed expresion. *)
184 (* ------------------------------------------------------------------------- *)
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]]);;
197 (* ------------------------------------------------------------------------- *)
198 (* Nesting depth of radicals in an expression. *)
199 (* ------------------------------------------------------------------------- *)
202 (`!a b c. a < MAX b c <=> a < b \/ a < c`,
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)`;;
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`]);;
219 let NOT_IN_OWN_RADICALS = prove
220 (`!r. ~(r IN radicals r)`,
221 MESON_TAC[IN_RADICALS_SMALLER; LT_REFL]);;
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]);;
231 (* ------------------------------------------------------------------------- *)
232 (* Crucial point about splitting off some "topmost" radical. *)
233 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
254 (* ------------------------------------------------------------------------- *)
255 (* By rearranging the expression we can use it in a canonical way. *)
256 (* ------------------------------------------------------------------------- *)
258 let RADICAL_CANONICAL_TRIVIAL = prove
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))
269 ==> ?a b. wellformed a /\
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[];
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[]]);;
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;
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
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[]];
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;
335 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
336 REWRITE_TAC[FORALL_AND_THM] THEN
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
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[];
357 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
358 REWRITE_TAC[FORALL_AND_THM] THEN
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
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;
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[];
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[]]);;
391 (* ------------------------------------------------------------------------- *)
392 (* Now we quite easily get an inductive argument. *)
393 (* ------------------------------------------------------------------------- *)
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
411 MP_TAC(SPEC `\x. ?ex. wellformed ex /\
412 radicals ex SUBSET (radicals(e) DELETE r) /\
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]];
441 DISCH_THEN(MP_TAC o SPECL
442 [`a:real`; `b:real`; `c:real`;
443 `value e`; `value eu`; `value ev`; `value r`]) THEN
446 [EXISTS_TAC `Constant a` THEN
447 ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
450 [EXISTS_TAC `Constant b` THEN
451 ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
454 [EXISTS_TAC `Constant c` THEN
455 ASM_REWRITE_TAC[wellformed; radicals; EMPTY_SUBSET; value];
457 RULE_ASSUM_TAC(REWRITE_RULE[wellformed]) THEN
458 ASM_REWRITE_TAC[value] THEN ASM_MESON_TAC[];
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[]);;
464 (* ------------------------------------------------------------------------- *)
465 (* Hence the main result. *)
466 (* ------------------------------------------------------------------------- *)
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[]]);;
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
499 (* ------------------------------------------------------------------------- *)
500 (* Now go further to an *integer*, since the polynomial is monic. *)
501 (* ------------------------------------------------------------------------- *)
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
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);;
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
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
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
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];
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]);;
572 (* ------------------------------------------------------------------------- *)
573 (* Hence we have our big final theorem. *)
574 (* ------------------------------------------------------------------------- *)
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]);;
585 (* ------------------------------------------------------------------------- *)
586 (* Geometrical definitions. *)
587 (* ------------------------------------------------------------------------- *)
589 let length = new_definition
590 `length(a:real^2,b:real^2) = norm(b - a)`;;
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)`;;
596 let collinear3 = new_definition
597 `collinear3 (a:real^2) b c <=> parallel (a,b) (a,c)`;;
599 let is_intersection = new_definition
600 `is_intersection p (a,b) (c,d) <=> collinear3 a p b /\ collinear3 c p d`;;
602 let on_circle = new_definition
603 `on_circle x (centre,pt) <=> length(centre,x) = length(centre,pt)`;;
605 (* ------------------------------------------------------------------------- *)
606 (* A trivial lemma. *)
607 (* ------------------------------------------------------------------------- *)
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);;
617 (* ------------------------------------------------------------------------- *)
618 (* Show that solutions to certain classes of equations are radical. *)
619 (* ------------------------------------------------------------------------- *)
621 let RADICAL_LINEAR_EQUATION = prove
622 (`!a b x. radical a /\ radical b /\ ~(a = &0 /\ b = &0) /\ a * x + b = &0
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);;
629 let RADICAL_SIMULTANEOUS_LINEAR_EQUATION = prove
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]]);;
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)
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];
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)`
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;
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[]]);;
668 let RADICAL_SIMULTANEOUS_LINEAR_QUADRATIC = prove
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
685 (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
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));;
691 let RADICAL_SIMULTANEOUS_QUADRATIC_QUADRATIC = prove
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
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
706 (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
707 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
709 (* ------------------------------------------------------------------------- *)
710 (* Analytic criterion for constructibility. *)
711 (* ------------------------------------------------------------------------- *)
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 /\
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)`;;
735 (* ------------------------------------------------------------------------- *)
736 (* Some "coordinate geometry" lemmas. *)
737 (* ------------------------------------------------------------------------- *)
739 let RADICAL_LINE_LINE_INTERSECTION = prove
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)`,
748 REWRITE_TAC[parallel; collinear3; is_intersection] THEN STRIP_TAC THEN
749 MATCH_MP_TAC RADICAL_SIMULTANEOUS_LINEAR_EQUATION THEN
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
756 (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
757 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
759 let RADICAL_LINE_CIRCLE_INTERSECTION = prove
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)`,
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
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
780 (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
781 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
783 let RADICAL_CIRCLE_CIRCLE_INTERSECTION = prove
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)`,
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
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
806 (CONJ_TAC THENL [RADICAL_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]) THEN
807 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_RING);;
809 (* ------------------------------------------------------------------------- *)
810 (* So constructible points have radical coordinates. *)
811 (* ------------------------------------------------------------------------- *)
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[]]);;
822 (* ------------------------------------------------------------------------- *)
823 (* Impossibility of doubling the cube. *)
824 (* ------------------------------------------------------------------------- *)
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);;
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]);;
849 (* ------------------------------------------------------------------------- *)
850 (* Impossibility of trisecting *)
851 (* ------------------------------------------------------------------------- *)
853 let COS_TRIPLE = prove
854 (`!x. cos(&3 * x) = &4 * cos(x) pow 3 - &3 * cos(x)`,
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);;
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);;
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
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]);;