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

needs "Multivariate/vectors.ml";;
needs "Library/transc.ml";;

(* ------------------------------------------------------------------------- *)
(* This gets overwritten by a theorem in transc load.                        *)
(* ------------------------------------------------------------------------- *)

let SUM_2 = 
prove (`!t. sum(1..2) t = t(1) + t(2)`,
REWRITE_TAC[num_CONV `2`; num_CONV `2`; SUM_CLAUSES_NUMSEG] THEN REWRITE_TAC[SUM_SING_NUMSEG; ARITH; REAL_ADD_ASSOC]);;
(* ------------------------------------------------------------------------- *) (* Some 2-vector special cases. *) (* ------------------------------------------------------------------------- *)
let DOT_VECTOR = 
prove (`(vector [x1;y1] :real^2) dot (vector [x2;y2]) = x1 * x2 + y1 * y2`,
REWRITE_TAC[dot; DIMINDEX_2; SUM_2; VECTOR_2]);;
(* ------------------------------------------------------------------------- *) (* Lemma about distance between points with polar coordinates. *) (* ------------------------------------------------------------------------- *)
let SIN_SUB = 
prove (`!x y. sin(x - y) = sin(x) * cos(y) - cos(x) * sin(y)`,
REWRITE_TAC[real_sub; SIN_ADD; COS_NEG; SIN_NEG] THEN CONV_TAC REAL_RING);;
let DIST_SEGMENT_LEMMA = 
prove (`!a1 a2. &0 <= a1 /\ a1 <= a2 /\ a2 <= &2 * pi /\ &0 <= radius ==> dist(centre + radius % vector [cos(a1);sin(a1)] :real^2, centre + radius % vector [cos(a2);sin(a2)]) = &2 * radius * sin((a2 - a1) / &2)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[dist; vector_norm] THEN MATCH_MP_TAC SQRT_POS_UNIQ THEN REWRITE_TAC[DOT_POS_LE] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SIN_POS_PI_LE THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[VECTOR_ARITH `(c + r % x) - (c + r % y) = r % (x - y)`] THEN REWRITE_TAC[VECTOR_ARITH `(r % x) dot (r % x) = (r pow 2) * (x dot x)`] THEN REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_VECTOR] THEN SUBST1_TAC(REAL_ARITH `a1 = &2 * a1 / &2`) THEN SUBST1_TAC(REAL_ARITH `a2 = &2 * a2 / &2`) THEN REWRITE_TAC[REAL_ARITH `(&2 * x - &2 * y) / &2 = x - y`] THEN REWRITE_TAC[SIN_SUB; SIN_DOUBLE; COS_DOUBLE] THEN MP_TAC(SPEC `a1 / &2` SIN_CIRCLE) THEN MP_TAC(SPEC `a2 / &2` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
(* ------------------------------------------------------------------------- *) (* Hence the overall theorem. *) (* ------------------------------------------------------------------------- *)
let PTOLEMY = 
prove (`!A B C D:real^2 a b c d centre radius. A = centre + radius % vector [cos(a);sin(a)] /\ B = centre + radius % vector [cos(b);sin(b)] /\ C = centre + radius % vector [cos(c);sin(c)] /\ D = centre + radius % vector [cos(d);sin(d)] /\ &0 <= radius /\ &0 <= a /\ a <= b /\ b <= c /\ c <= d /\ d <= &2 * pi ==> dist(A,C) * dist(B,D) = dist(A,B) * dist(C,D) + dist(A,D) * dist(B,C)`,
REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM(SUBST1_TAC o check (is_var o lhs o concl))) THEN REPEAT (W(fun (asl,w) -> let t = find_term (fun t -> can (PART_MATCH (lhs o rand) DIST_SEGMENT_LEMMA) t) w in MP_TAC (PART_MATCH (lhs o rand) DIST_SEGMENT_LEMMA t) THEN ANTS_TAC THENL [ASM_REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC])) THEN REWRITE_TAC[REAL_ARITH `(x - y) / &2 = x / &2 - y / &2`] THEN MAP_EVERY (fun t -> MP_TAC(SPEC t SIN_CIRCLE)) [`a / &2`; `b / &2`; `c / &2`; `d / &2`] THEN REWRITE_TAC[SIN_SUB; SIN_ADD; COS_ADD; SIN_PI; COS_PI] THEN CONV_TAC REAL_RING);;