(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Eyypqdw = struct



open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Appendix;;

let SGIN_POW_EQ=
prove(`a IN {-- &1, &1} ==> a pow 2= &1`,
REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC THEN REAL_ARITH_TAC);;
let EYYPQDW_COPLANAR=
prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 /\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3 ==> coplanar{vec 0, v1, v2, v3}`,
[STRIP_TAC; REWRITE_TAC[coplanar] THEN EXISTS_TAC`vec 0:real^3` THEN EXISTS_TAC`v1:real^3` THEN EXISTS_TAC`v2:real^3` THEN ASM_REWRITE_TAC[SET_RULE`{A,B,C,D} SUBSET E<=> A IN E/\ B IN E/\ C IN E/\ D IN E`;Collect_geom2.AFFINE_HULL_3;IN_ELIM_THM] THEN REPEAT STRIP_TAC; EXISTS_TAC`&1` THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&0` THEN ASM_REWRITE_TAC[REAL_ARITH`&1+ &0+ &0= &1`] THEN VECTOR_ARITH_TAC; EXISTS_TAC`&0` THEN EXISTS_TAC`&1` THEN EXISTS_TAC`&0` THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &1+ &0= &1`] THEN VECTOR_ARITH_TAC; EXISTS_TAC`&0` THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&1` THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &0+ &1= &1`] THEN VECTOR_ARITH_TAC; EXPAND_TAC"v3" THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`a%v+b%(c%v-d%w)=(a+ b*c)%v+(--b*d)%w`] THEN EXISTS_TAC`&1- (inv (&2 * x1) * (x1 + x3 - x5) + (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) * (v1 dot (v2:real^3))) - (--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) * (v1 dot v1))` THEN EXISTS_TAC`(inv (&2 * x1) * (x1 + x3 - x5) + (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) * (v1 dot (v2:real^3)))` THEN EXISTS_TAC`(--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) * (v1 dot (v1:real^3)))` THEN ASM_REWRITE_TAC[REAL_ARITH`(&1-A-B)+A+B= &1`] THEN VECTOR_ARITH_TAC]);;
let EYYPQDW_NORMV3=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 /\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3 ==> norm(v3) pow 2= x3`,
STRIP_TAC THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM] THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`] THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG] THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG] THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`) THEN RESA_TAC THEN EXPAND_TAC"v3" THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS] THEN ASM_TAC THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_RSUB;DOT_LSUB] THEN REPEAT RESA_TAC THEN MRESA_TAC DOT_SYM[`v2:real^3`;`v1:real^3`] THEN REPLICATE_TAC (23-9)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[REAL_ARITH`x1 - v1 dot v2 - (v1 dot v2 - x2) = x6 <=> v1 dot v2 = (x1 + x2 - x6)/ &2`;REAL_ARITH`a*a *b=a pow 2 *b/\ A- &0=A/\ (a*b) pow 2=a pow 2 * b pow 2`;REAL_INV_MUL] THEN RESA_TAC THEN ASM_SIMP_TAC[SGIN_POW_EQ] THEN MRESA_TAC REAL_MUL_LINV[`x1:real`] THEN ASM_REWRITE_TAC[REAL_ARITH`((inv (&2) pow 2 * inv x1 pow 2) * (x1 + x3 - x5) pow 2) * x1 = ((inv (&2) pow 2 * inv x1 ) * (x1 + x3 - x5) pow 2) * (inv x1 *x1) /\ A * &1 =A `] THEN ASM_SIMP_TAC[SGIN_POW_EQ] THEN MP_TAC(REAL_ARITH`&0< ups_x x1 x3 x5==> &0<=ups_x x1 x3 x5/\ ~(ups_x x1 x3 x5 = &0)`) THEN RESA_TAC THEN MRESA_TAC REAL_LE_INV[`ups_x x1 x2 x6`] THEN MRESA_TAC REAL_LE_MUL[`inv(ups_x x1 x2 x6)`;`ups_x x1 x3 x5`] THEN MRESA_TAC SQRT_POW2[`inv (ups_x x1 x2 x6) * ups_x x1 x3 x5`] THEN ASM_REWRITE_TAC[REAL_ARITH`(inv x1 pow 2 * &1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5) * x1 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2) = (inv x1 *x1) * inv x1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`] THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`ups_x x1 x2 x6`;`(inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 + &1 * inv x1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`;`x3:real`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC REAL_MUL_LINV[`ups_x x1 x2 x6`] THEN ASM_REWRITE_TAC[REAL_ARITH`ups_x x1 x2 x6 * ((inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 + &1 * inv x1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)) = inv x1 *( ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2/ &4 + (inv (ups_x x1 x2 x6) * ups_x x1 x2 x6 ) * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`] THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`x1:real`;`inv x1 * (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 + &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`;`ups_x x1 x2 x6 * x3`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_REWRITE_TAC[REAL_ARITH`x1 * inv x1 * (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 + &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)) = (inv x1 *x1) * (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 + ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))/\ a pow 2=a*a`;ups_x] THEN REAL_ARITH_TAC);;
let EYYPQDW_NORM_V3_V1=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 /\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3 ==> norm (v3-v1) pow 2= x5`,
STRIP_TAC THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_LSUB;DOT_RSUB] THEN MP_TAC EYYPQDW_NORMV3 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[GSYM DOT_SQUARE_NORM;] THEN REPEAT RESA_TAC THEN MRESA_TAC DOT_SYM[`v3:real^3`;`v1:real^3`] THEN REWRITE_TAC[REAL_ARITH`x3 - v1 dot v3 - (v1 dot v3 - x1) = x5 <=> v1 dot v3 = (x1+x3-x5)/ &2`] THEN EXPAND_TAC"v3" THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL] THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`) THEN RESA_TAC THEN MRESA_TAC REAL_MUL_LINV[`x1:real`] THEN ASM_REWRITE_TAC[REAL_ARITH`((inv (&2) * inv x1) * (x1 + x3 - x5)) * x1 = (inv x1 * x1) * (x1 + x3 - x5)/ &2 `] THEN REAL_ARITH_TAC);;
let EYYPQDW_SCALAR_POS=
prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 /\ (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))=v3 ==> (?t. &0<t/\ v3 cross v1= (a*t)%(v1 cross v2))`,
STRIP_TAC THEN EXPAND_TAC"v3" THEN REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH`A-B=A+(--B):real^3/\ a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM] THEN MRESA_TAC CROSS_SKEW[`v2:real^3`;`v1:real^3`] THEN REWRITE_TAC[VECTOR_ARITH`(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) % --(x1 % --(v1 cross v2)) = ((inv x1 *x1) * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) % (v1 cross v2)`] THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`) THEN RESA_TAC THEN MRESAL_TAC REAL_MUL_LINV[`x1:real`][REAL_ARITH`&1*a=a`] THEN EXISTS_TAC`sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SQRT_POS_LT THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`) THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`] THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG] THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]);;
let v3_defor_v1=new_definition`v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3= (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))`;;
let v3_defor_v2=new_definition`v3_defor_v2 a  x1 x2 x3 x5 x6 v1 v2= (inv(&2 * x1) *(x1 + x3 - x5))% v1 + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%(v1 cross (v1 cross v2))`;;
let LIFT_CONTINUOUS_ATREAL=
prove(`!x. lift continuous atreal x`,
REWRITE_TAC[continuous_atreal;DIST_LIFT] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`e:real` THEN ASM_REWRITE_TAC[]);;
let LIFT_CONTINUOUS_ATREAL_I=
prove(`!x. lift o(\x. x) continuous atreal x`,
REWRITE_TAC[continuous_atreal;DIST_LIFT;o_DEF] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`e:real` THEN ASM_REWRITE_TAC[]);;
let EYYPQDW_CONTINUOUS_AT_X=
prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 ==> (\x3. v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3) continuous atreal (x3)`,
[ STRIP_TAC THEN REWRITE_TAC[v3_defor_v1;CROSS_LAGRANGE] THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH`A-B=A+(--B):real^3/\ a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM;o_DEF] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN STRIP_TAC; MATCH_MP_TAC CONTINUOUS_VMUL THEN REWRITE_TAC[o_DEF;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[o_DEF;LIFT_ADD] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN REWRITE_TAC[LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_LIFT_NORM_COMPOSE;LIFT_CONTINUOUS_ATREAL]; MATCH_MP_TAC CONTINUOUS_VMUL THEN REWRITE_TAC[o_DEF;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MRESAL_TAC CONTINUOUS_ATREAL_COMPOSE[`(\x. lift (inv (ups_x x1 x2 x6) * ups_x x1 x x5))`;`lift o sqrt o drop`;`x3:real`][o_DEF;LIFT_DROP] THEN POP_ASSUM MATCH_MP_TAC THEN STRIP_TAC; REWRITE_TAC[LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[ups_x;LIFT_ADD;] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN STRIP_TAC; REWRITE_TAC[LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN ONCE_REWRITE_TAC[GSYM o_DEF;] THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;] THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I]; MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN STRIP_TAC; REWRITE_TAC[o_DEF;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]; ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`] THEN REWRITE_TAC[o_DEF;LIFT_CMUL;] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]; ONCE_REWRITE_TAC[GSYM o_DEF] THEN ONCE_REWRITE_TAC[GSYM o_DEF] THEN MATCH_MP_TAC CONTINUOUS_AT_WITHIN THEN MATCH_MP_TAC CONTINUOUS_AT_SQRT THEN REWRITE_TAC[LIFT_DROP] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`) THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`] THEN MRESAL_TAC (GEN_ALL Trigonometry1.DIST_UPS_X_POS)[`vec 0:real^3`;`v1:real^3`;`v2:real^3`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG] THEN MRESAL_TAC Collect_geom.FHFMKIY[`vec 0:real^3`;`v1:real^3`;`v2:real^3`;`x1:real`;`x2:real`;`x6:real`][dist;VECTOR_ARITH`vec 0- A= --A/\ A- vec 0=A:real^3`;GSYM DOT_SQUARE_NORM;NORM_NEG]]);;
let EYYPQDW_CONTINUOUS_AT_V=
prove(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\ ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 /\ a IN {-- &1, &1} /\ &0< ups_x x1 x3 x5 ==> (\v2. v3_defor_v2 a x1 x2 x3 x5 x6 v1 v2) continuous at (v2)`,
STRIP_TAC THEN REWRITE_TAC[v3_defor_v2;CROSS_LAGRANGE] THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A/\ &0 +A=A`;DOT_CROSS;REAL_INV_MUL;CROSS_LAGRANGE;CROSS_LADD;VECTOR_ARITH` a % vec 0= vec 0 /\ vec 0 +A=A`;CROSS_LMUL;CROSS_REFL;CROSS_LADD;CROSS_LNEG;DOT_SQUARE_NORM;o_DEF] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST;VECTOR_ARITH`a%(v-w)=a%v- a%w`] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN STRIP_TAC THENL[ MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_VMUL THEN ASM_SIMP_TAC[CONTINUOUS_AT_LIFT_DOT]; MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN ASM_SIMP_TAC[CONTINUOUS_AT_ID]]);;
let V3_DEFOR_V1_EQV3_DEFOR_V2=
prove(`v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3=v3_defor_v2 a x1 x2 x3 x5 x6 v1 v2`,
REWRITE_TAC[v3_defor_v1;v3_defor_v2]);;
let LIFT_UPS_CONTINUOUS=
prove_by_refinement(`~(collinear{vec 0,v1,v2:real^3}) /\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6 ==> lift o(\x2. ups_x x1 x2 x6) continuous atreal (x2)`,
[STRIP_TAC THEN REWRITE_TAC[ups_x;LIFT_ADD;o_DEF] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN STRIP_TAC; REWRITE_TAC[LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN ONCE_REWRITE_TAC[GSYM o_DEF;] THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;] THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I]; MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST] THEN STRIP_TAC; REWRITE_TAC[o_DEF;LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]; ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`] THEN REWRITE_TAC[o_DEF;LIFT_CMUL;] THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN MATCH_MP_TAC CONTINUOUS_CMUL THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]]);;
let MK_PLANAR_REP=
prove(`mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 a - v0= (inv(&2 * x1) *(x1 + x3 - x5))% (v1-v0) + ((inv x1)* a * sqrt(inv(ups_x x1 x2 x6) * (ups_x x1 x3 x5)))%((v1-v0) cross ((v1-v0) cross (v2-v0:real^3)))`,
REWRITE_TAC[mk_planar2;LET_DEF;LET_END_DEF;real_div;VECTOR_ARITH`(a+b)-a=b:real^3`;] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`] THEN MATCH_MP_TAC(VECTOR_ARITH`a=b==> c+a=c+b:real^3`) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`] THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> a%v=b %v:real^3`) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`(a*b)*c=b*a*c`] THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`) THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`) THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> sqrt(a)=sqrt(b:real)`) THEN REAL_ARITH_TAC);;
let EYYPQDW = 
prove_by_refinement(`!v0 v1 v2 v3 x1 x2 x3 x5 x6 s. &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\ ~collinear {v0,v1,v2} /\ x1 = dist(v1,v0) pow 2 /\ x2 = dist(v2,v0) pow 2 /\ x6 = dist(v1,v2) pow 2 /\ &0 < ups_x x1 x3 x5 /\ (s = &1 \/ s = -- &1) /\ v3 = mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s ==> (coplanar {v0,v1,v2,v3} /\ x3 = dist(v3,v0) pow 2 /\ x5 = dist(v3,v1) pow 2 /\ ?t. &0 < t /\ t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`,
[ REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`] THEN REPEAT STRIP_TAC; MRESAL_TAC(GEN_ALL EYYPQDW_COPLANAR)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`x5:real`;`v1-v0:real^3`;`v2-v0:real^3`;`v3-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT] THEN REDUCE_VECTOR_TAC; MRESAL_TAC(GEN_ALL EYYPQDW_NORMV3)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x5:real`;`v1-v0:real^3`;`v2-v0:real^3`;`v3-v0:real^3`;`x3:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]; MRESAL_TAC(GEN_ALL EYYPQDW_NORM_V3_V1)[`x3:real`;`s:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`v2-v0:real^3`;`v3-v0:real^3`;`v1-v0:real^3`;`x5:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE]; MRESAL_TAC(GEN_ALL EYYPQDW_SCALAR_POS)[`x3:real`;`x2:real`;`x6:real` ;`x1:real`;`x3:real`;`x5:real`;`v3-v0:real^3`;`s:real`;`v1-v0:real^3`;`v2-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE] THEN EXISTS_TAC`inv t` THEN STRIP_TAC; MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[]; MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`) THEN RESA_TAC THEN MRESA_TAC REAL_MUL_LINV[`t:real`] THEN ASM_REWRITE_TAC[VECTOR_ARITH`a%b%v=(a*b)%v`;REAL_ARITH`inv t * s * t= (inv t * t)*s`] THEN VECTOR_ARITH_TAC]);;
let MK_PLANAR_V3_DEFOR_V1=
prove(`mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 a - v0 = v3_defor_v1 a (v1-v0) (v2-v0) x1 x2 x5 x6 x3`,
REWRITE_TAC[v3_defor_v1;MK_PLANAR_REP]);;
let MK_PLANAR_V3_DEFOR_V1_FUN=
prove(`(\q. mk_planar2 v0 v1 v2 x1 x2 q x5 x6 s)= (\x3. v3_defor_v1 s (v1-v0) (v2-v0) x1 x2 x5 x6 x3+ v0)`,
REWRITE_TAC[FUN_EQ_THM;] THEN GEN_TAC THEN REWRITE_TAC[GSYM MK_PLANAR_V3_DEFOR_V1] THEN VECTOR_ARITH_TAC);;
let EYYPQDW2 = 
prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s. &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\ ~collinear {v0,v1,v2} /\ x1 = dist(v1,v0) pow 2 /\ x2 = dist(v2,v0) pow 2 /\ x6 = dist(v1,v2) pow 2 /\ (s = &1 \/ s = -- &1)/\ &0 < ups_x x1 x3 x5 ==> (\q. mk_planar2 v0 v1 v2 x1 x2 q x5 x6 s) continuous atreal x3`,
REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V1_FUN] THEN MRESAL_TAC(GEN_ALL EYYPQDW_CONTINUOUS_AT_X)[`x3:real`;`s:real`;`v1-v0:real^3`;`v2-v0:real^3`;`x1:real`;`x2:real` ;`x5:real`;`x6:real`;`x3:real`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST]);;
let MK_PLANAR_V3_DEFOR_V2_FUN=
prove(`(\q. mk_planar2 v0 v1 q x1 x2 x3 x5 x6 s)= (\v2. v3_defor_v2 s x1 x2 x3 x5 x6 (v1-v0) (v2-v0) + v0)`,
REWRITE_TAC[FUN_EQ_THM;] THEN GEN_TAC THEN REWRITE_TAC[v3_defor_v2;GSYM MK_PLANAR_REP] THEN VECTOR_ARITH_TAC);;
let lemma30000=
prove(`(\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5 (norm (v1 - v2) pow 2) (v1 - v0) (v2' - v0)) = (\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5 (norm (v1 - v2) pow 2) (v1 - v0) (v2'))o(\v2. v2- v0)`,
REWRITE_TAC[o_DEF]) ;;
let EYYPQDW3 =
prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s. &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\ ~collinear {v0,v1,v2} /\ x1 = dist(v1,v0) pow 2 /\ x2 = dist(v2,v0) pow 2 /\ x6 = dist(v1,v2) pow 2 /\ (s = &1 \/ s = -- &1)/\ &0 < ups_x x1 x3 x5 ==> (\q. mk_planar2 v0 v1 q x1 x2 x3 x5 x6 s) continuous at v2`,
REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V2_FUN] THEN MRESAL_TAC(GEN_ALL EYYPQDW_CONTINUOUS_AT_V)[`x3:real`;`s:real`;`x1:real`;`x2:real` ;`x3:real`;`x5:real`;`x6:real`;`v1-v0:real^3`;`v2-v0:real^3`][VECTOR_ARITH`v1 - v0 - (v2 - v0)= v1-v2:real^3`;GSYM MK_PLANAR_REP;GSYM Trigonometry2.COLLINEAR_TRANSABLE] THEN MATCH_MP_TAC CONTINUOUS_ADD THEN ASM_SIMP_TAC[CONTINUOUS_CONST;lemma30000] THEN MATCH_MP_TAC CONTINUOUS_AT_COMPOSE THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CONTINUOUS_SUB THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_AT_ID]);;
end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)