(* ========================================================================= *)
(* Thales's theorem.                                                         *)
(* ========================================================================= *)

needs "Multivariate/convex.ml";;

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Geometric concepts.                                                       *)
(* ------------------------------------------------------------------------- *)

let BETWEEN_THM = 
prove (`between x (a,b) <=> ?u. &0 <= u /\ u <= &1 /\ x = u % a + (&1 - u) % b`,
REWRITE_TAC[BETWEEN_IN_CONVEX_HULL] THEN ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN REWRITE_TAC[CONVEX_HULL_2_ALT; IN_ELIM_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
let length_def = new_definition
 `length(A:real^2,B:real^2) = norm(B - A)`;;
let is_midpoint = new_definition
 `is_midpoint (m:real^2) (a,b) <=> m = (&1 / &2) % (a + b)`;;
(* ------------------------------------------------------------------------- *) (* This formulation works. *) (* ------------------------------------------------------------------------- *)
let THALES = 
prove (`!centre radius a b c. length(a,centre) = radius /\ length(b,centre) = radius /\ length(c,centre) = radius /\ is_midpoint centre (a,b) ==> orthogonal (c - a) (c - b)`,
REPEAT GEN_TAC THEN REWRITE_TAC[length_def; BETWEEN_THM; is_midpoint] THEN STRIP_TAC THEN REPEAT(FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x pow 2`)) THEN REWRITE_TAC[NORM_POW_2] THEN FIRST_ASSUM(MP_TAC o SYM) THEN ABBREV_TAC `rad = radius pow 2` THEN POP_ASSUM_LIST(K ALL_TAC) THEN SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT; orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN CONV_TAC REAL_RING);;
(* ------------------------------------------------------------------------- *) (* But for another natural version, we need to use the reals. *) (* ------------------------------------------------------------------------- *) needs "Examples/sos.ml";; (* ------------------------------------------------------------------------- *) (* The following, which we need as a lemma, needs the reals specifically. *) (* ------------------------------------------------------------------------- *)
let MIDPOINT = 
prove (`!m a b. between m (a,b) /\ length(a,m) = length(b,m) ==> is_midpoint m (a,b)`,
REPEAT GEN_TAC THEN REWRITE_TAC[length_def; BETWEEN_THM; is_midpoint; NORM_EQ] THEN SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT; orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_SOS);;
(* ------------------------------------------------------------------------- *) (* Now we get a more natural formulation of Thales's theorem. *) (* ------------------------------------------------------------------------- *)
let THALES = 
prove (`!centre radius a b c:real^2. length(a,centre) = radius /\ length(b,centre) = radius /\ length(c,centre) = radius /\ between centre (a,b) ==> orthogonal (c - a) (c - b)`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `is_midpoint centre (a,b)` MP_TAC THENL [MATCH_MP_TAC MIDPOINT THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN UNDISCH_THEN `between (centre:real^2) (a,b)` (K ALL_TAC) THEN REPEAT(FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x pow 2`)) THEN REWRITE_TAC[length_def; is_midpoint; orthogonal; NORM_POW_2] THEN ABBREV_TAC `rad = radius pow 2` THEN POP_ASSUM_LIST(K ALL_TAC) THEN SIMP_TAC[dot; SUM_2; VECTOR_SUB_COMPONENT; DIMINDEX_2; VECTOR_ADD_COMPONENT; orthogonal; CART_EQ; FORALL_2; VECTOR_MUL_COMPONENT; ARITH] THEN CONV_TAC REAL_RING);;