1 (* ========================================================================= *)
2 (* Thales's theorem. *)
3 (* ========================================================================= *)
5 needs "Multivariate/convex.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Geometric concepts. *)
11 (* ------------------------------------------------------------------------- *)
13 let BETWEEN_THM = prove
15 ?u. &0 <= u /\ u <= &1 /\ x = u % a + (&1 - u) % b`,
16 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL] THEN
17 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN
18 REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN
19 AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
20 AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
22 let length_def = new_definition
23 `length(A:real^2,B:real^2) = norm(B - A)`;;
25 let is_midpoint = new_definition
26 `is_midpoint (m:real^2) (a,b) <=> m = (&1 / &2) % (a + b)`;;
28 (* ------------------------------------------------------------------------- *)
29 (* This formulation works. *)
30 (* ------------------------------------------------------------------------- *)
33 (`!centre radius a b c.
34 length(a,centre) = radius /\
35 length(b,centre) = radius /\
36 length(c,centre) = radius /\
37 is_midpoint centre (a,b)
38 ==> orthogonal (c - a) (c - b)`,
39 REPEAT GEN_TAC THEN REWRITE_TAC[length_def; BETWEEN_THM; is_midpoint] THEN
40 STRIP_TAC THEN REPEAT(FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x pow 2`)) THEN
41 REWRITE_TAC[NORM_POW_2] THEN FIRST_ASSUM(MP_TAC o SYM) THEN
42 ABBREV_TAC `rad = radius pow 2` THEN POP_ASSUM_LIST(K ALL_TAC) THEN
43 SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT;
44 orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN
47 (* ------------------------------------------------------------------------- *)
48 (* But for another natural version, we need to use the reals. *)
49 (* ------------------------------------------------------------------------- *)
51 needs "Examples/sos.ml";;
53 (* ------------------------------------------------------------------------- *)
54 (* The following, which we need as a lemma, needs the reals specifically. *)
55 (* ------------------------------------------------------------------------- *)
58 (`!m a b. between m (a,b) /\ length(a,m) = length(b,m)
59 ==> is_midpoint m (a,b)`,
60 REPEAT GEN_TAC THEN REWRITE_TAC[length_def; BETWEEN_THM; is_midpoint; NORM_EQ] THEN
61 SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT;
62 orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN
63 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
64 REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN
65 REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_SOS);;
67 (* ------------------------------------------------------------------------- *)
68 (* Now we get a more natural formulation of Thales's theorem. *)
69 (* ------------------------------------------------------------------------- *)
72 (`!centre radius a b c:real^2.
73 length(a,centre) = radius /\
74 length(b,centre) = radius /\
75 length(c,centre) = radius /\
77 ==> orthogonal (c - a) (c - b)`,
79 SUBGOAL_THEN `is_midpoint centre (a,b)` MP_TAC THENL
80 [MATCH_MP_TAC MIDPOINT THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
81 UNDISCH_THEN `between (centre:real^2) (a,b)` (K ALL_TAC) THEN
82 REPEAT(FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x pow 2`)) THEN
83 REWRITE_TAC[length_def; is_midpoint; orthogonal; NORM_POW_2] THEN
84 ABBREV_TAC `rad = radius pow 2` THEN POP_ASSUM_LIST(K ALL_TAC) THEN
85 SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT;
86 orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN