1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA *)
5 (* EULER TRIANGLE LEMMA *)
7 (* Authour : VU KHAC KY *)
8 (* Date : 2010-04-02 *)
9 (* Books name: JLPSDHF *)
10 (* ========================================================================= *)
13 (* =========================================================================*)
15 (* BEGIN THE MAIN THEORM ABOUT EULER ANGLE SUM *)
17 (*==========================================================================*)
20 flyspeck_needs "general/sphere.hl";;
22 flyspeck_needs "general/prove_by_refinement.hl";;
24 flyspeck_needs "trigonometry/trig1.hl";;
25 flyspeck_needs "trigonometry/trig2.hl";;
26 flyspeck_needs "trigonometry/delta_x.hl";;
27 flyspeck_needs "trigonometry/euler_complement.hl";;
28 flyspeck_needs "trigonometry/euler_multivariate.hl";;
32 module Euler_main_theorem = struct
37 open Prove_by_refinement;;
39 open Euler_complement;;
40 open Euler_multivariate;;
42 let euler_angle_sum_rescale =
43 ` !v0:real^3 v1 v2 v3 p x1 x2 x3 x4 x5 x6 alpha1 alpha2 alpha3 d w1 w2 w3.
44 p = euler_p v0 v1 v2 v3 /\
45 x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
46 alpha1 = dihV v0 v1 v2 v3 /\
47 alpha2 = dihV v0 v2 v3 v1 /\
48 alpha3 = dihV v0 v3 v1 v2 /\
49 d = delta_x x1 x2 x3 x4 x5 x6 /\
57 ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p)`;;
59 let EULER_ANGLE_SUM_rescal = prove_by_refinement (euler_angle_sum_rescale ,
63 (REPLICATE_TAC 11 UP_ASM_TAC);
64 (FIRST_ASSUM MP_TAC THEN SWITCH_TAC THEN FIRST_ASSUM MP_TAC);
65 (REWRITE_TAC[euler_p;xlist;ylist]);
67 (REPEAT UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC);
69 (* ==========================================================================*)
70 (* 3 FIRST SUBGOALS: *)
71 (* ==========================================================================*)
74 ` ~collinear {(v0:real^3), v1, v2} /\
75 ~collinear {v0, v1, v3} /\
76 ~collinear {v0, v3, v2}`
78 (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
80 (SUBGOAL_THEN `y1 = &1 /\ y2 = &1 /\ y3 = &1` ASSUME_TAC);
81 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
82 (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
83 (PURE_ONCE_REWRITE_TAC[dist]);
85 (UP_ASM_TAC THEN STRIP_TAC);
87 (SUBGOAL_THEN `x1 = &1 /\ x2 = &1 /\ x3 = &1` ASSUME_TAC);
89 (ONCE_ASM_REWRITE_TAC[REAL_POW_2]);
91 (UP_ASM_TAC THEN STRIP_TAC);
93 (* ==========================================================================*)
94 (* Subgoal 4: Comput p and delta *)
95 (* ==========================================================================*)
98 `&2 * p = &8 - x4 - x5 - x6 /\ d = ups_x x4 x5 x6 - x4 * x5 * x6`
102 `x4 = (v2 - v3) dot (v2 - v3:real^3) /\
103 x5 = (v1 - v3) dot (v1 - v3) /\
104 x6 = (v1 - v2) dot (v1 - v2)`
108 (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
109 (ONCE_REWRITE_TAC[dist]);
110 (REWRITE_TAC[NORM_POW_2]);
112 CONJ_TAC; (* Break into 2 subgoals *)
114 (REPEAT UP_ASM_TAC THEN DISCH_TAC THEN DISCH_TAC);
115 (DEL_TAC THEN REPEAT DISCH_TAC);
116 (ONCE_ASM_REWRITE_TAC[]);
117 (ONCE_ASM_REWRITE_TAC[]);
118 (REWRITE_TAC [REAL_MUL_LID]);
119 (EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'");
120 (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
122 (REWRITE_TAC[NORM_POW_2]);
123 (ASM_MESON_TAC[LEMMA_FOR_EULER_AFTER_RESCALE]);
126 (REWRITE_TAC[ups_x;delta_x]);
127 (ONCE_ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
129 (* ========================================================================= *)
130 (* Re-comput alpha1, alpha2, alpha3 . *)
131 (* ========================================================================= *)
133 (* ------------------------------------------------------------------------- *)
134 (* Subgoal 5: alpha1 *)
135 (* ------------------------------------------------------------------------- *)
141 atn2 (sqrt (&4 * x1 * delta_x x1 x2 x3 x4 x5 x6),delta_x4 x1 x2 x3 x4 x5 x6)`
144 (REPLICATE_TAC 7 DEL_TAC THEN UP_ASM_TAC THEN DISCH_TAC);
145 (MP_TAC COMPUTE_DIHV_ATN2);
146 (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
148 (* ------------------------------------------------------------------------- *)
149 (* Subgoal 6: alpha2 *)
150 (* ------------------------------------------------------------------------- *)
155 atn2 (sqrt (&4 * x2 * delta_x x2 x3 x1 x5 x6 x4),delta_x4 x2 x3 x1 x5 x6 x4)`
158 (REPLICATE_TAC 8 DEL_TAC);
161 `x4 = dist (v2:real^3,v3) pow 2 /\
162 x5 = dist (v3,v1) pow 2 /\
163 x6 = dist (v2,v1) pow 2 /\
164 ~collinear {v0, v2, v3} /\
165 ~collinear {v0, v2, v1}`
167 (ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
169 (REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
171 (ONCE_ASM_REWRITE_TAC[]);
172 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
173 (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
175 (* ------------------------------------------------------------------------- *)
176 (* Subgoal 7: alpha3 *)
177 (* ------------------------------------------------------------------------- *)
183 atn2 (sqrt (&4 * x3 * delta_x x3 x1 x2 x6 x4 x5),delta_x4 x3 x1 x2 x6 x4 x5)`
186 (REPLICATE_TAC 9 DEL_TAC);
189 `x5 = dist (v3:real^3,v1) pow 2 /\
190 x4 = dist (v3,v2) pow 2 /\
191 x6 = dist (v1,v2) pow 2 /\
192 ~collinear {v0, v3, v1} /\
193 ~collinear {v0, v3, v2}`
195 (ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
197 (REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
199 (ONCE_ASM_REWRITE_TAC[]);
200 (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
201 (ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
203 (* ------------------------------------------------------------------------- *)
204 (* Subgoal 8: delta_x is symmetry *)
205 (* ------------------------------------------------------------------------- *)
208 `delta_x x2 x3 x1 x5 x6 x4 = d /\ delta_x x3 x1 x2 x6 x4 x5 = d`
212 `x2, x3, x1, x5, x6, x4 = xlist (v0:real^3) v2 v3 v1`
214 (REWRITE_TAC[xlist;ylist]);
216 (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
217 (ASM_MESON_TAC[DIST_SYM]);
220 `x3, x1, x2, x6, x4, x5 = xlist (v0:real^3) v3 v1 v2`
222 (REWRITE_TAC[xlist;ylist]);
224 (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
225 (ASM_MESON_TAC[DIST_SYM]);
228 (REWRITE_TAC[delta_x]);
231 (* ------------------------------------------------------------------------- *)
232 (* Subgoal 9: Th simplest form of alpha1,2,3 *)
233 (* ------------------------------------------------------------------------- *)
237 pi / &2 - atn ((-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) / sqrt (&4 * d)) /\
239 pi / &2 - atn ((-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) / sqrt (&4 * d)) /\
241 pi / &2 - atn ((-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5) / sqrt (&4 * d))`
244 (ABBREV_TAC `4D = &4 * d`);
245 (REPLICATE_TAC 21 UP_ASM_TAC THEN REPLICATE_TAC 9 DEL_TAC);
247 (ONCE_ASM_REWRITE_TAC[]);
248 (REWRITE_TAC[REAL_ARITH `a - x = a - y <=> x = y`]);
250 (REWRITE_TAC[GSYM (ASSUME `d = delta_x x1 x2 x3 x4 x5 x6`)]);
251 (REWRITE_TAC[ASSUME `delta_x x2 x3 x1 x5 x6 x4 = d /\
252 delta_x x3 x1 x2 x6 x4 x5 = d`]);
254 (REWRITE_TAC[delta_x4]);
255 (REWRITE_TAC[ASSUME `x1 = &1`]);
256 (REWRITE_TAC[ASSUME `x2 = &1`]);
257 (REWRITE_TAC[ASSUME `x3 = &1`]);
258 (REWRITE_TAC[REAL_MUL_LID;REAL_MUL_RID]);
260 (REWRITE_TAC[REAL_ARITH
261 `-- &1 - x4 + x5 + x6 - x5 * x6 + -- &1 + &1 + &1 - x4 + x5 + x6
262 = (-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) /\
263 -- &1 - x5 + x6 + x4 - x6 * x4 + -- &1 + &1 + &1 - x5 + x6 + x4
264 = (-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) /\
265 -- &1 - x6 + x4 + x5 - x4 * x5 + -- &1 + &1 + &1 - x6 + x4 + x5
266 = (-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5)`]);
269 (SUBGOAL_THEN `&0 < sqrt (&4 * d)` ASSUME_TAC);
270 (MATCH_MP_TAC SQRT_POS_LT);
271 (ASM_MESON_TAC[REAL_ARITH `&0 < &4`;REAL_LT_MUL]);
273 (ASM_MESON_TAC[ATN2_BREAKDOWN]);
275 (* ------------------------------------------------------------------------- *)
276 (* Subgoal 10, 11: Something remains *)
277 (* ------------------------------------------------------------------------- *)
279 (ABBREV_TAC `a = (x4:real)`);
280 (ABBREV_TAC `b = (x5:real)`);
281 (ABBREV_TAC `c = (x6:real)`);
284 `atn2 (sqrt d,&2 * p) = atn ((&8 - a - b - c) / sqrt d)`
286 (SUBGOAL_THEN `&0 < sqrt d ` ASSUME_TAC);
287 (MATCH_MP_TAC SQRT_POS_LT THEN ASM_MESON_TAC[]);
289 (ASM_MESON_TAC[ATN2_BREAKDOWN]);
292 (SUBGOAL_THEN `sqrt (&4 * d) = &2 * sqrt d` ASSUME_TAC);
293 (SUBGOAL_THEN `sqrt (&4 * d) = sqrt (&4) * sqrt d` ASSUME_TAC);
294 (MATCH_MP_TAC SQRT_MUL);
297 (AP_THM_TAC THEN AP_TERM_TAC);
298 (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2 `]);
299 (REWRITE_TAC[MESON[SQRT_MUL;REAL_ARITH `&0 <= &2`]
300 `sqrt (&2 * &2) = sqrt (&2) * sqrt (&2)`]);
301 (REWRITE_TAC[GSYM POW_2]);
302 (MATCH_MP_TAC SQRT_POW_2);
305 (REPLICATE_TAC 7 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
306 (REPLICATE_TAC 16 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
308 (ONCE_ASM_REWRITE_TAC[]);
310 (* ------------------------------------------------------------------------- *)
311 (* Subgoal 12: &0 < a, b , c < &4 *)
312 (* ------------------------------------------------------------------------- *)
314 (SUBGOAL_THEN `a < &4 /\ b < &4 /\ c < &4` ASSUME_TAC);
315 (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
316 (ASM_REWRITE_TAC[REAL_ARITH `&4 = &2 pow 2`]);
319 (MATCH_MP_TAC REAL_POW_LT2);
321 (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
322 (MATCH_MP_TAC (REAL_ARITH
323 `dist (v0:real^3,v2) = &1 /\ dist (v0,v3) = &1 /\
324 dist (v2,v3) < dist (v0:real^3,v2) + dist (v0,v3)
325 ==> dist (v2,v3) < &2`));
330 (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
331 (REWRITE_TAC[DIST_TRIANGLE_ALT]);
333 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
334 (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
335 (REWRITE_TAC[NORM_POW_2]);
336 (ABBREV_TAC `m = v0:real^3 - v2`);
337 (ABBREV_TAC `n = v0:real^3 - v3`);
338 (SUBGOAL_THEN `v2:real^3 - v3 = n - m` ASSUME_TAC);
339 (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
340 (ONCE_ASM_REWRITE_TAC[]);
341 (REWRITE_TAC[NORM_POW_2]);
342 (REWRITE_TAC[VECTOR_ARITH
343 `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
344 (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
345 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
346 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
347 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
348 (REWRITE_TAC [NORM_POW_2]);
349 (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
351 (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
352 (EXPAND_TAC "n" THEN EXPAND_TAC "m");
353 (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
354 (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
355 (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, a, c}`]);
360 (MATCH_MP_TAC REAL_POW_LT2);
362 (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
363 (MATCH_MP_TAC (REAL_ARITH
364 `dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
365 dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
366 ==> dist (v1,v3) < &2`));
371 (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
372 (REWRITE_TAC[DIST_TRIANGLE_ALT]);
374 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
375 (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
376 (REWRITE_TAC[NORM_POW_2]);
377 (ABBREV_TAC `m = v0:real^3 - v1`);
378 (ABBREV_TAC `n = v0:real^3 - v3`);
379 (SUBGOAL_THEN `v1:real^3 - v3 = n - m` ASSUME_TAC);
380 (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
381 (ONCE_ASM_REWRITE_TAC[]);
382 (REWRITE_TAC[NORM_POW_2]);
383 (REWRITE_TAC[VECTOR_ARITH
384 `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
385 (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
386 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
387 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
388 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
389 (REWRITE_TAC [NORM_POW_2]);
390 (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
392 (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
393 (EXPAND_TAC "n" THEN EXPAND_TAC "m");
394 (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
395 (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
396 (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
401 (MATCH_MP_TAC REAL_POW_LT2);
403 (REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
404 (MATCH_MP_TAC (REAL_ARITH
405 `dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
406 dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
407 ==> dist (v1,v3) < &2`));
412 (MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
413 (REWRITE_TAC[DIST_TRIANGLE_ALT]);
415 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
416 (REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
417 (REWRITE_TAC[NORM_POW_2]);
418 (ABBREV_TAC `m = v0:real^3 - v1`);
419 (ABBREV_TAC `n = v0:real^3 - v2`);
420 (SUBGOAL_THEN `v1:real^3 - v2 = n - m` ASSUME_TAC);
421 (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
422 (ONCE_ASM_REWRITE_TAC[]);
423 (REWRITE_TAC[NORM_POW_2]);
424 (REWRITE_TAC[VECTOR_ARITH
425 `(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
426 (REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
427 (MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
428 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
429 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
430 (REWRITE_TAC [NORM_POW_2]);
431 (ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
433 (REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
434 (EXPAND_TAC "n" THEN EXPAND_TAC "m");
435 (ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
436 (ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
437 (PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
442 (SUBGOAL_THEN `&0 < a /\ &0 < b /\ &0 < c` ASSUME_TAC);
443 (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
448 (MATCH_MP_TAC REAL_POW_LT);
451 (MATCH_MP_TAC (NORM_ARITH `~(v2 = v3) ==> &0 < norm (v2 - v3)`));
453 (MATCH_MP_TAC (MESON[]
454 ` collinear {v0:real^3, v2, v3} /\ ~ collinear {v0, v2, v3} ==> F`));
458 (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
459 (ASM_MESON_TAC[COLLINEAR_2]);
463 (MATCH_MP_TAC REAL_POW_LT);
466 (MATCH_MP_TAC (NORM_ARITH `~(v1 = v3) ==> &0 < norm (v1 - v3)`));
468 (MATCH_MP_TAC (MESON[]
469 ` collinear {v0:real^3, v3, v1} /\ ~ collinear {v0, v3, v1} ==> F`));
473 (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
474 (ASM_MESON_TAC[COLLINEAR_2]);
478 (MATCH_MP_TAC REAL_POW_LT);
481 (MATCH_MP_TAC (NORM_ARITH `~(v1 = v2) ==> &0 < norm (v1 - v2)`));
483 (MATCH_MP_TAC (MESON[]
484 ` collinear {v0:real^3, v1, v2} /\ ~ collinear {v0, v1, v2} ==> F`));
487 (REWRITE_TAC[ASSUME `v1 :real^3 = v2`]);
488 (REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
489 (ASM_MESON_TAC[COLLINEAR_2]);
492 (* ------------------------------------------------------------------------- *)
493 (* FINISH the EULER LEMMA *)
494 (* ------------------------------------------------------------------------- *)
496 (REPLICATE_TAC 3 UP_ASM_TAC);
497 (REPLICATE_TAC 9 DEL_TAC);
498 (UP_ASM_TAC THEN REPLICATE_TAC 13 DEL_TAC THEN UP_ASM_TAC);
499 (REPEAT DEL_TAC THEN REPEAT DISCH_TAC);
501 (MP_TAC DERIVATIVE_WRT_A_Euler_lemma THEN LET_TAC);
502 (ASM_MESON_TAC[])]);;
505 let euler_triangle_t = `!v0 v1 v2 v3:real^3.
506 let p = euler_p v0 v1 v2 v3 in
507 let (x1,x2,x3,x4,x5,x6) = xlist v0 v1 v2 v3 in
508 let alpha1 = dihV v0 v1 v2 v3 in
509 let alpha2 = dihV v0 v2 v3 v1 in
510 let alpha3 = dihV v0 v3 v1 v2 in
511 let d = delta_x x1 x2 x3 x4 x5 x6 in
513 (alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2(sqrt(d), (&2 * p))))`;;
515 let EULER_TRIANGLE = prove_by_refinement (euler_triangle_t ,
516 [MATCH_MP_TAC EULER_FORMULA_RESCALE;
517 MP_TAC EULER_ANGLE_SUM_rescal;