100/thales.ml

   1 (* ========================================================================= *)
   2 (* Thales's theorem.                                                         *)
   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_def = new_definition
  23  `length(A:real^2,B:real^2) = norm(B - A)`;;
  24
  25 let is_midpoint = new_definition
  26  `is_midpoint (m:real^2) (a,b) <=> m = (&1 / &2) % (a + b)`;;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* This formulation works.                                                   *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let THALES = prove
  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
  45   CONV_TAC REAL_RING);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* But for another natural version, we need to use the reals.                *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 needs "Examples/sos.ml";;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* The following, which we need as a lemma, needs the reals specifically.    *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 let MIDPOINT = prove
  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);;
  66
  67 (* ------------------------------------------------------------------------- *)
  68 (* Now we get a more natural formulation of Thales's theorem.                *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71 let THALES = prove
  72  (`!centre radius a b c:real^2.
  73         length(a,centre) = radius /\
  74         length(b,centre) = radius /\
  75         length(c,centre) = radius /\
  76         between centre (a,b)
  77         ==> orthogonal (c - a) (c - b)`,
  78   REPEAT STRIP_TAC THEN
  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
  87   CONV_TAC REAL_RING);;