100/chords.ml

   1 (* ========================================================================= *)
   2 (* #55: Theorem on product of segments of chords.                            *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/convex.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Geometric concepts.                                                       *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let BETWEEN_THM = prove
  14  (`between x (a,b) <=>
  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);;
  21
  22 let length = new_definition
  23  `length(A:real^2,B:real^2) = norm(B - A)`;;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* One more special reduction theorem to avoid square roots.                 *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let lemma = prove
  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]);;
  35
  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]);;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* Now the main theorem.                                                     *)
  44 (* ------------------------------------------------------------------------- *)
  45
  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)`,
  52   REPEAT GEN_TAC THEN
  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
  65   CONV_TAC REAL_RING);;