1 (* ========================================================================= *)
2 (* #55: Theorem on product of segments of chords. *)
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 = new_definition
23 `length(A:real^2,B:real^2) = norm(B - A)`;;
25 (* ------------------------------------------------------------------------- *)
26 (* One more special reduction theorem to avoid square roots. *)
27 (* ------------------------------------------------------------------------- *)
30 (`!x y. &0 <= x /\ &0 <= y ==> (x pow 2 = y pow 2 <=> x = y)`,
31 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[REAL_POW_2] THEN
32 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
33 (SPECL [`x:real`; `y:real`] REAL_LT_TOTAL) THEN
34 ASM_MESON_TAC[REAL_LT_MUL2; REAL_LT_REFL]);;
36 let NORM_CROSS = prove
37 (`norm(a) * norm(b) = norm(c) * norm(d) <=>
38 (a dot a) * (b dot b) = (c dot c) * (d dot d)`,
39 REWRITE_TAC[GSYM NORM_POW_2; GSYM REAL_POW_MUL] THEN
40 MATCH_MP_TAC(GSYM lemma) THEN SIMP_TAC[NORM_POS_LE; REAL_LE_MUL]);;
42 (* ------------------------------------------------------------------------- *)
43 (* Now the main theorem. *)
44 (* ------------------------------------------------------------------------- *)
46 let SEGMENT_CHORDS = prove
47 (`!centre radius q r s t b.
48 between b (q,r) /\ between b (s,t) /\
49 length(q,centre) = radius /\ length(r,centre) = radius /\
50 length(s,centre) = radius /\ length(t,centre) = radius
51 ==> length(q,b) * length(b,r) = length(s,b) * length(b,t)`,
53 REWRITE_TAC[length; NORM_CROSS; BETWEEN_THM] THEN
54 DISCH_THEN(CONJUNCTS_THEN2
55 (X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) MP_TAC) THEN
56 FIRST_X_ASSUM SUBST_ALL_TAC THEN
57 DISCH_THEN(CONJUNCTS_THEN2
58 (X_CHOOSE_THEN `v:real` STRIP_ASSUME_TAC) MP_TAC) THEN
59 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN
60 (MP_TAC o AP_TERM `\x. x pow 2`)) THEN
61 FIRST_X_ASSUM(MP_TAC o SYM) THEN REWRITE_TAC[NORM_POW_2] THEN
62 ABBREV_TAC `rad = radius pow 2` THEN POP_ASSUM_LIST(K ALL_TAC) THEN
63 SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT;
64 CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN