(* ========================================================================= *)
(* Theory of elementary Euclidean geometry.                                  *)
(* ========================================================================= *)

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Basic definitions of what circles and lines are.                          *)
(* ------------------------------------------------------------------------- *)

let is_circle = new_definition
  `is_circle c =
     ?x0 y0 r. c = {(x,y) | (x - x0) pow 2 + (y - y0) pow 2 = r}`;;

let is_line = new_definition
  `is_line l =
     ?a b c d. l = {(x,y) | ?u. (x = a * u + c) /\ (y = b * u + d)}`;;

(* ------------------------------------------------------------------------- *)
(* A trivial rephrasing to sound more geometrical.                           *)
(* ------------------------------------------------------------------------- *)

parse_as_infix("on",(11,"right"));;

let on = new_definition
  `p on s = p IN s`;;

(* ------------------------------------------------------------------------- *)
(* Line defined by two points.                                               *)
(* ------------------------------------------------------------------------- *)

let line = new_definition
  `line A B = @L. is_line L /\ A on L /\ B on L`;;

let LINE = prove
 (`!A B. is_line(line A B) /\ A on (line A B) /\ B on (line A B)`,
  REWRITE_TAC[FORALL_PAIR_THM] THEN
  MAP_EVERY X_GEN_TAC [`a1:real`; `a2:real`; `b1:real`; `b2:real`] THEN
  REWRITE_TAC[line] THEN CONV_TAC SELECT_CONV THEN REWRITE_TAC[is_line] THEN
  REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
  REWRITE_TAC[REWR_CONV SWAP_EXISTS_THM `?L:(A->bool) m. P L m`] THEN
  REWRITE_TAC[UNWIND_THM2; on; IN_ELIM_THM] THEN
  SUBGOAL_THEN
    `?a b c d u v.
        (a1 = a * u + c) /\ (a2 = b * u + d) /\
        (b1 = a * v + c) /\ (b2 = b * v + d)`
    (fun th -> MESON_TAC[th]) THEN
  MAP_EVERY EXISTS_TAC
   [`b1 - a1`; `b2 - a2`; `a1:real`; `a2:real`; `&0`; `&1`] THEN
  REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Intersection of two lines.                                                *)
(* ------------------------------------------------------------------------- *)

let intersection = new_definition
  `intersection L1 L2 = @p:real#real. p on L1 /\ p on L2`;;

(* ------------------------------------------------------------------------- *)
(* Collinearity.                                                             *)
(* ------------------------------------------------------------------------- *)

let collinear = new_definition
  `collinear pts = ?L. is_line(L) /\ ALL (\p. p on L) pts`;;

let COLLINEAR_3 = prove
 (`collinear [a1,a2; b1,b2; c1,c2] =
        ((a1 - b1) * (b2 - c2) - (a2 - b2) * (b1 - c1) = &0)`,
  REWRITE_TAC[collinear; is_line; ALL] THEN EQ_TAC THENL
   [DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
    DISCH_THEN(REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC) THEN
    POP_ASSUM MP_TAC THEN  REWRITE_TAC[on; IN_ELIM_THM] THEN
    GEN_REWRITE_TAC (LAND_CONV o DEPTH_BINOP_CONV `(/\)` o ONCE_DEPTH_CONV) 
                    [CONJ_SYM] THEN
    REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC] THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;

    REWRITE_TAC[REAL_SUB_0] THEN DISCH_TAC THEN
    EXISTS_TAC `{(x,y) | ?u. (x = (c1 - a1) * u + a1) /\ 
                             (y = (c2 - a2) * u + a2)}` THEN
    CONJ_TAC THENL
     [MAP_EVERY EXISTS_TAC [`c1 - a1`; `c2 - a2`; `a1:real`; `a2:real`] THEN
      REWRITE_TAC[]; ALL_TAC] THEN
    REWRITE_TAC[on; IN_ELIM_THM] THEN
    GEN_REWRITE_TAC (DEPTH_BINOP_CONV `(/\)` o ONCE_DEPTH_CONV) 
                    [CONJ_SYM] THEN                                
    REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC] THEN
    REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN REPEAT CONJ_TAC THENL
     [EXISTS_TAC `&0` THEN REAL_ARITH_TAC;
      ALL_TAC;
      EXISTS_TAC `&1` THEN REAL_ARITH_TAC] THEN
    POP_ASSUM MP_TAC THEN
    ASM_CASES_TAC `c1:real = a1` THEN ASM_REWRITE_TAC[] THENL
     [ASM_CASES_TAC `c2:real = a2` THEN ASM_REWRITE_TAC[] THENL
       [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
        



    POP_ASSUM MP_TAC THEN ASM_CASES_TAC `b1:real = a1` THENL
     [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_LZERO] THEN
      DISCH_THEN(MP_TAC o SYM) THEN ASM_CASES_TAC `c1:real = a1` THENL
       [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_LZERO; REAL_ADD_LID] THEN
        DISCH_TAC THEN EXISTS_TAC `



 

CONJ_TAC THENL 
     [MAP_EVERY EXISTS_TAC `
    
    


  


(* ------------------------------------------------------------------------- *) 
(* Parallelism.                                                              *)
(* ------------------------------------------------------------------------- *)

let parallel = new_definition
  `parallel L1 L2 = (L1 = L2) \/ ~(?p. p on intersection L1 L2)`;;

let PARALLEL = prove
 (`parallel (line (a1,a2) (b1,b2)) (line (c1,c2) (d1,d2)) =
        ((a1 - b1) * (c2 - d2) - (a2 - b2) * (c1 - d1) = &0)`,

