text_formalization/local/EYYPQDW.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Eyypqdw = struct
  16
  17
  18
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Topology;;
  22 open Fan_misc;;
  23 open Planarity;;
  24 open Conforming;;
  25 open Hypermap;;
  26 open Fan;;
  27 open Appendix;;
  28
  29 let SGIN_POW_EQ=prove(`a IN {-- &1, &1} ==> a pow 2= &1`,
  30 REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`]
  31 THEN RESA_TAC
  32 THEN REAL_ARITH_TAC);;
  33
  34
  35 let EYYPQDW_COPLANAR=prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
  36 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
  37 /\ a IN {-- &1, &1}
  38 /\ &0< ups_x x1 x3 x5
  39 /\ (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
  40 ==>
  41  coplanar{vec 0, v1, v2, v3}`,
  42 [STRIP_TAC;
  43
  44 REWRITE_TAC[coplanar]
  45 THEN EXISTS_TAC`vec 0:real^3`
  46 THEN EXISTS_TAC`v1:real^3`
  47 THEN EXISTS_TAC`v2:real^3`
  48 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]
  49 THEN REPEAT STRIP_TAC;
  50
  51 EXISTS_TAC`&1`
  52 THEN EXISTS_TAC`&0`
  53 THEN EXISTS_TAC`&0`
  54 THEN ASM_REWRITE_TAC[REAL_ARITH`&1+ &0+ &0= &1`]
  55 THEN VECTOR_ARITH_TAC;
  56
  57 EXISTS_TAC`&0`
  58 THEN EXISTS_TAC`&1`
  59 THEN EXISTS_TAC`&0`
  60 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &1+ &0= &1`]
  61 THEN VECTOR_ARITH_TAC;
  62
  63 EXISTS_TAC`&0`
  64 THEN EXISTS_TAC`&0`
  65 THEN EXISTS_TAC`&1`
  66 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+ &0+ &1= &1`]
  67 THEN VECTOR_ARITH_TAC;
  68
  69 EXPAND_TAC"v3"
  70 THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`a%v+b%(c%v-d%w)=(a+ b*c)%v+(--b*d)%w`]
  71 THEN EXISTS_TAC`&1- (inv (&2 * x1) * (x1 + x3 - x5) +
  72       (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
  73       (v1 dot (v2:real^3))) - (--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
  74       (v1 dot v1))`
  75 THEN EXISTS_TAC`(inv (&2 * x1) * (x1 + x3 - x5) +
  76       (inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
  77       (v1 dot (v2:real^3)))`
  78 THEN EXISTS_TAC`(--(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) *
  79       (v1 dot (v1:real^3)))`
  80 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1-A-B)+A+B= &1`]
  81 THEN VECTOR_ARITH_TAC]);;
  82
  83
  84
  85 let EYYPQDW_NORMV3=prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
  86 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
  87 /\ a IN {-- &1, &1}
  88 /\ &0< ups_x x1 x3 x5
  89 /\ (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
  90 ==>
  91  norm(v3)  pow 2= x3`,
  92 STRIP_TAC
  93 THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM]
  94 THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
  95 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]
  96 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]
  97 THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
  98 THEN RESA_TAC
  99 THEN EXPAND_TAC"v3"
 100 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]
 101 THEN ASM_TAC
 102 THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_RSUB;DOT_LSUB]
 103 THEN REPEAT RESA_TAC
 104 THEN MRESA_TAC DOT_SYM[`v2:real^3`;`v1:real^3`]
 105 THEN REPLICATE_TAC (23-9)(POP_ASSUM MP_TAC)
 106 THEN POP_ASSUM(fun th->
 107 REPEAT STRIP_TAC
 108 THEN MP_TAC th)
 109 THEN ASM_REWRITE_TAC[REAL_ARITH`x1 - v1 dot v2 - (v1 dot v2 - x2) = x6
 110 <=>  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]
 111 THEN RESA_TAC
 112 THEN ASM_SIMP_TAC[SGIN_POW_EQ]
 113 THEN MRESA_TAC REAL_MUL_LINV[`x1:real`]
 114 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)
 115 /\ A * &1 =A `]
 116 THEN ASM_SIMP_TAC[SGIN_POW_EQ]
 117 THEN MP_TAC(REAL_ARITH`&0< ups_x x1 x3 x5==> &0<=ups_x x1 x3 x5/\ ~(ups_x x1 x3 x5 = &0)`)
 118 THEN RESA_TAC
 119 THEN MRESA_TAC REAL_LE_INV[`ups_x x1 x2 x6`]
 120 THEN MRESA_TAC REAL_LE_MUL[`inv(ups_x x1 x2 x6)`;`ups_x x1 x3 x5`]
 121 THEN MRESA_TAC SQRT_POW2[`inv (ups_x x1 x2 x6) * ups_x x1 x3 x5`]
 122 THEN ASM_REWRITE_TAC[REAL_ARITH`(inv x1 pow 2 * &1 * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5) *
 123  x1 *
 124  (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)
 125 = (inv x1 *x1) * inv x1  * inv (ups_x x1 x2 x6) * ups_x x1 x3 x5 *
 126  (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`]
 127 THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`ups_x x1 x2 x6`;`(inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 +
 128  &1 *
 129  inv x1 *
 130  inv (ups_x x1 x2 x6) *
 131  ups_x x1 x3 x5 *
 132  (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2)`;`x3:real`]
 133 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 134 THEN MRESA_TAC REAL_MUL_LINV[`ups_x x1 x2 x6`]
 135 THEN ASM_REWRITE_TAC[REAL_ARITH`ups_x x1 x2 x6 *
 136  ((inv (&2) pow 2 * inv x1) * (x1 + x3 - x5) pow 2 +
 137   &1 *
 138   inv x1 *
 139   inv (ups_x x1 x2 x6) *
 140   ups_x x1 x3 x5 *
 141   (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))
 142 = inv x1 *( ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2/ &4 +
 143     (inv (ups_x x1 x2 x6) * ups_x x1 x2 x6 ) *
 144   ups_x x1 x3 x5 *
 145   (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`]
 146 THEN MRESA_TAC REAL_EQ_MUL_LCANCEL[`x1:real`;`inv x1 *
 147  (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
 148   &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))`;`ups_x x1 x2 x6 * x3`]
 149 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 150 THEN ASM_REWRITE_TAC[REAL_ARITH`x1 *
 151  inv x1 *
 152  (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
 153   &1 * ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))
 154 = (inv x1 *x1) *
 155  (ups_x x1 x2 x6 * (x1 + x3 - x5) pow 2 / &4 +
 156    ups_x x1 x3 x5 * (x1 * x2 - (x1 + x2 - x6) / &2 * (x1 + x2 - x6) / &2))/\ a pow 2=a*a`;ups_x]
 157 THEN REAL_ARITH_TAC);;
 158
 159
 160 let EYYPQDW_NORM_V3_V1=prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
 161 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
 162 /\ a IN {-- &1, &1}
 163 /\ &0< ups_x x1 x3 x5
 164 /\ (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
 165 ==>
 166  norm (v3-v1)  pow 2= x5`,
 167 STRIP_TAC
 168 THEN ASM_REWRITE_TAC[GSYM DOT_SQUARE_NORM;DOT_LSUB;DOT_RSUB]
 169 THEN MP_TAC EYYPQDW_NORMV3
 170 THEN RESA_TAC
 171 THEN ASM_TAC
 172 THEN REWRITE_TAC[GSYM DOT_SQUARE_NORM;]
 173 THEN REPEAT RESA_TAC
 174 THEN MRESA_TAC DOT_SYM[`v3:real^3`;`v1:real^3`]
 175 THEN REWRITE_TAC[REAL_ARITH`x3 - v1 dot v3 - (v1 dot v3 - x1) = x5
 176 <=> v1 dot v3 = (x1+x3-x5)/ &2`]
 177 THEN EXPAND_TAC"v3"
 178 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]
 179 THEN ASM_REWRITE_TAC[]
 180 THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
 181 THEN RESA_TAC
 182 THEN MRESA_TAC REAL_MUL_LINV[`x1:real`]
 183 THEN ASM_REWRITE_TAC[REAL_ARITH`((inv (&2) * inv x1) * (x1 + x3 - x5)) * x1
 184 = (inv x1 * x1) * (x1 + x3 - x5)/ &2 `]
 185 THEN REAL_ARITH_TAC);;
 186
 187
 188 let EYYPQDW_SCALAR_POS=prove(`&0< x1 /\ &0<x2 /\ &0<x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
 189 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
 190 /\ a IN {-- &1, &1}
 191 /\ &0< ups_x x1 x3 x5
 192 /\ (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
 193 ==>
 194  (?t. &0<t/\ v3 cross v1= (a*t)%(v1 cross v2))`,
 195 STRIP_TAC
 196 THEN EXPAND_TAC"v3"
 197 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]
 198 THEN MRESA_TAC CROSS_SKEW[`v2:real^3`;`v1:real^3`]
 199 THEN REWRITE_TAC[VECTOR_ARITH`(inv x1 * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) %
 200      --(x1 % --(v1 cross v2))
 201 = ((inv x1 *x1) * a * sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)) %
 202      (v1 cross v2)`]
 203 THEN MP_TAC(REAL_ARITH`&0< x3/\ &0< x1==> &0<= x3/\ ~(x1= &0)`)
 204 THEN RESA_TAC
 205 THEN MRESAL_TAC REAL_MUL_LINV[`x1:real`][REAL_ARITH`&1*a=a`]
 206 THEN EXISTS_TAC`sqrt (inv (ups_x x1 x2 x6) * ups_x x1 x3 x5)`
 207 THEN ASM_REWRITE_TAC[]
 208 THEN MATCH_MP_TAC SQRT_POS_LT
 209 THEN MATCH_MP_TAC REAL_LT_MUL
 210 THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ]
 211 THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`)
 212 THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
 213 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]
 214 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]);;
 215
 216
 217
 218
 219
 220 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))`;;
 221
 222 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))`;;
 223
 224
 225 let LIFT_CONTINUOUS_ATREAL=prove(`!x. lift continuous atreal x`,
 226 REWRITE_TAC[continuous_atreal;DIST_LIFT]
 227 THEN REPEAT STRIP_TAC
 228 THEN EXISTS_TAC`e:real`
 229 THEN ASM_REWRITE_TAC[]);;
 230
 231
 232
 233 let LIFT_CONTINUOUS_ATREAL_I=prove(`!x. lift o(\x. x) continuous atreal x`,
 234 REWRITE_TAC[continuous_atreal;DIST_LIFT;o_DEF]
 235 THEN REPEAT STRIP_TAC
 236 THEN EXISTS_TAC`e:real`
 237 THEN ASM_REWRITE_TAC[]);;
 238
 239
 240
 241 let EYYPQDW_CONTINUOUS_AT_X=prove_by_refinement(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
 242 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
 243 /\ a IN {-- &1, &1}
 244  /\ &0< ups_x x1 x3 x5
 245 ==>
 246  (\x3. v3_defor_v1 a v1 v2 x1 x2 x5 x6 x3)  continuous atreal (x3)`,
 247 [
 248 STRIP_TAC
 249 THEN REWRITE_TAC[v3_defor_v1;CROSS_LAGRANGE]
 250 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]
 251 THEN MATCH_MP_TAC CONTINUOUS_ADD
 252 THEN STRIP_TAC;
 253
 254 MATCH_MP_TAC CONTINUOUS_VMUL
 255 THEN REWRITE_TAC[o_DEF;LIFT_CMUL]
 256 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 257 THEN REWRITE_TAC[o_DEF;LIFT_ADD]
 258 THEN MATCH_MP_TAC CONTINUOUS_ADD
 259 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 260 THEN REWRITE_TAC[LIFT_SUB]
 261 THEN MATCH_MP_TAC CONTINUOUS_SUB
 262 THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_LIFT_NORM_COMPOSE;LIFT_CONTINUOUS_ATREAL];
 263
 264 MATCH_MP_TAC CONTINUOUS_VMUL
 265 THEN REWRITE_TAC[o_DEF;LIFT_CMUL]
 266 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 267 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 268 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]
 269 THEN POP_ASSUM MATCH_MP_TAC
 270 THEN STRIP_TAC;
 271
 272 REWRITE_TAC[LIFT_CMUL]
 273 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 274 THEN REWRITE_TAC[ups_x;LIFT_ADD;]
 275 THEN MATCH_MP_TAC CONTINUOUS_ADD
 276 THEN STRIP_TAC;
 277
 278 REWRITE_TAC[LIFT_SUB]
 279 THEN MATCH_MP_TAC CONTINUOUS_SUB
 280 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 281 THEN MATCH_MP_TAC CONTINUOUS_SUB
 282 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 283 THEN ONCE_REWRITE_TAC[GSYM o_DEF;]
 284 THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;]
 285 THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL
 286 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I];
 287
 288 MATCH_MP_TAC CONTINUOUS_ADD
 289 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 290 THEN MATCH_MP_TAC CONTINUOUS_ADD
 291 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 292 THEN STRIP_TAC;
 293
 294 REWRITE_TAC[o_DEF;LIFT_CMUL]
 295 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 296 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 297 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];
 298
 299 ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`]
 300 THEN REWRITE_TAC[o_DEF;LIFT_CMUL;]
 301 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 302 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 303 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];
 304
 305 ONCE_REWRITE_TAC[GSYM o_DEF]
 306 THEN ONCE_REWRITE_TAC[GSYM o_DEF]
 307 THEN MATCH_MP_TAC CONTINUOUS_AT_WITHIN
 308 THEN MATCH_MP_TAC CONTINUOUS_AT_SQRT
 309 THEN REWRITE_TAC[LIFT_DROP]
 310 THEN MATCH_MP_TAC REAL_LT_MUL
 311 THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ]
 312 THEN MATCH_MP_TAC (REAL_ARITH`&0<=a /\ ~(a= &0)==> &0< a`)
 313 THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`v2:real^3`]
 314 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]
 315 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]]);;
 316
 317
 318 let EYYPQDW_CONTINUOUS_AT_V=prove(`&0< x1 /\ &0<x2 /\ &0< x3 /\ &0<x4 /\ &0<x5 /\ &0< x6 /\
 319 ~(collinear{vec 0,v1,v2:real^3})/\ norm v1 pow 2 = x1/\ norm v2 pow 2 =x2/\ norm(v1-v2) pow 2=x6
 320 /\ a IN {-- &1, &1}
 321  /\ &0< ups_x x1 x3 x5
 322 ==> (\v2. v3_defor_v2 a x1 x2 x3 x5 x6 v1 v2)  continuous at (v2)`,
 323 STRIP_TAC
 324 THEN REWRITE_TAC[v3_defor_v2;CROSS_LAGRANGE]
 325 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]
 326 THEN MATCH_MP_TAC CONTINUOUS_ADD
 327 THEN ASM_SIMP_TAC[CONTINUOUS_CONST;VECTOR_ARITH`a%(v-w)=a%v- a%w`]
 328 THEN MATCH_MP_TAC CONTINUOUS_SUB
 329 THEN STRIP_TAC
 330 THENL[
 331
 332 MATCH_MP_TAC CONTINUOUS_CMUL
 333 THEN MATCH_MP_TAC CONTINUOUS_VMUL
 334 THEN ASM_SIMP_TAC[CONTINUOUS_AT_LIFT_DOT];
 335
 336 MATCH_MP_TAC CONTINUOUS_CMUL
 337 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 338 THEN ASM_SIMP_TAC[CONTINUOUS_AT_ID]]);;
 339
 340
 341 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`,
 342 REWRITE_TAC[v3_defor_v1;v3_defor_v2]);;
 343
 344
 345 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
 346 ==> lift o(\x2. ups_x x1 x2 x6) continuous atreal (x2)`,
 347 [STRIP_TAC
 348 THEN REWRITE_TAC[ups_x;LIFT_ADD;o_DEF]
 349 THEN MATCH_MP_TAC CONTINUOUS_ADD
 350 THEN STRIP_TAC;
 351
 352 REWRITE_TAC[LIFT_SUB]
 353 THEN MATCH_MP_TAC CONTINUOUS_SUB
 354 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 355 THEN MATCH_MP_TAC CONTINUOUS_SUB
 356 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 357 THEN ONCE_REWRITE_TAC[GSYM o_DEF;]
 358 THEN REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS1;]
 359 THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL
 360 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL_I];
 361
 362 MATCH_MP_TAC CONTINUOUS_ADD
 363 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 364 THEN MATCH_MP_TAC CONTINUOUS_ADD
 365 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]
 366 THEN STRIP_TAC;
 367
 368 REWRITE_TAC[o_DEF;LIFT_CMUL]
 369 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 370 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 371 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL];
 372
 373 ONCE_REWRITE_TAC[REAL_ARITH`&2 * x * x5= &2 * x5 * x`]
 374 THEN REWRITE_TAC[o_DEF;LIFT_CMUL;]
 375 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 376 THEN MATCH_MP_TAC CONTINUOUS_CMUL
 377 THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1;LIFT_CONTINUOUS_ATREAL]]);;
 378
 379
 380
 381 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)))`,
 382 REWRITE_TAC[mk_planar2;LET_DEF;LET_END_DEF;real_div;VECTOR_ARITH`(a+b)-a=b:real^3`;]
 383 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`]
 384 THEN MATCH_MP_TAC(VECTOR_ARITH`a=b==> c+a=c+b:real^3`)
 385 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`a*b=b*a`]
 386 THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> a%v=b %v:real^3`)
 387 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`(a*b)*c=b*a*c`]
 388 THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`)
 389 THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> c*a=c*b:real`)
 390 THEN MATCH_MP_TAC(SET_RULE`a=b:real ==> sqrt(a)=sqrt(b:real)`)
 391 THEN REAL_ARITH_TAC);;
 392
 393
 394
 395
 396
 397 let EYYPQDW = prove_by_refinement(`!v0 v1 v2 v3 x1 x2 x3 x5 x6 s.
 398     &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
 399     ~collinear {v0,v1,v2} /\
 400   x1 = dist(v1,v0) pow 2 /\
 401   x2 = dist(v2,v0) pow 2 /\
 402   x6 = dist(v1,v2) pow 2 /\
 403   &0 < ups_x x1 x3 x5 /\
 404   (s = &1 \/ s = -- &1) /\
 405   v3 = mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s ==>
 406     (coplanar {v0,v1,v2,v3} /\
 407        x3 = dist(v3,v0) pow 2 /\
 408         x5 = dist(v3,v1) pow 2 /\
 409         ?t. &0 < t /\
 410          t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`,
 411 [
 412 REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
 413 THEN REPEAT STRIP_TAC;
 414
 415 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]
 416 THEN POP_ASSUM MP_TAC
 417 THEN REWRITE_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT]
 418 THEN REDUCE_VECTOR_TAC;
 419
 420 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];
 421
 422 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];
 423
 424 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]
 425 THEN EXISTS_TAC`inv t`
 426 THEN STRIP_TAC;
 427
 428 MATCH_MP_TAC REAL_LT_INV
 429 THEN ASM_REWRITE_TAC[];
 430
 431 MP_TAC(REAL_ARITH`&0< t==> ~(t= &0)`)
 432 THEN RESA_TAC
 433 THEN MRESA_TAC REAL_MUL_LINV[`t:real`]
 434 THEN ASM_REWRITE_TAC[VECTOR_ARITH`a%b%v=(a*b)%v`;REAL_ARITH`inv t * s * t= (inv t * t)*s`]
 435 THEN VECTOR_ARITH_TAC]);;
 436
 437
 438
 439
 440 let MK_PLANAR_V3_DEFOR_V1=prove(`mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 a  - v0
 441 = v3_defor_v1 a (v1-v0) (v2-v0) x1 x2 x5 x6 x3`,
 442 REWRITE_TAC[v3_defor_v1;MK_PLANAR_REP]);;
 443
 444 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)`,
 445 REWRITE_TAC[FUN_EQ_THM;]
 446 THEN GEN_TAC
 447 THEN REWRITE_TAC[GSYM MK_PLANAR_V3_DEFOR_V1]
 448 THEN VECTOR_ARITH_TAC);;
 449
 450
 451
 452 let EYYPQDW2 =  prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
 453     &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
 454     ~collinear {v0,v1,v2} /\
 455   x1 = dist(v1,v0) pow 2 /\
 456   x2 = dist(v2,v0) pow 2 /\
 457   x6 = dist(v1,v2) pow 2 /\
 458   (s = &1 \/ s = -- &1)/\
 459   &0 < ups_x x1 x3 x5 ==>
 460    (\q. mk_planar2 v0 v1 v2 x1 x2 q x5 x6 s) continuous atreal x3`,
 461 REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
 462 THEN REPEAT STRIP_TAC
 463 THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V1_FUN]
 464 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]
 465 THEN MATCH_MP_TAC CONTINUOUS_ADD
 466 THEN ASM_SIMP_TAC[CONTINUOUS_CONST]);;
 467
 468
 469 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)`,
 470 REWRITE_TAC[FUN_EQ_THM;]
 471 THEN GEN_TAC
 472 THEN REWRITE_TAC[v3_defor_v2;GSYM MK_PLANAR_REP]
 473 THEN VECTOR_ARITH_TAC);;
 474
 475 let lemma30000=prove(`(\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5
 476         (norm (v1 - v2) pow 2)
 477         (v1 - v0)
 478         (v2' - v0))
 479 = (\v2'. v3_defor_v2 s (norm (v1 - v0) pow 2) (norm (v2 - v0) pow 2) x3 x5
 480         (norm (v1 - v2) pow 2)
 481         (v1 - v0)
 482         (v2'))o(\v2. v2- v0)`,
 483 REWRITE_TAC[o_DEF])
 484 ;;
 485
 486
 487 let EYYPQDW3 =prove(`!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
 488     &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
 489     ~collinear {v0,v1,v2} /\
 490   x1 = dist(v1,v0) pow 2 /\
 491   x2 = dist(v2,v0) pow 2 /\
 492   x6 = dist(v1,v2) pow 2 /\
 493   (s = &1 \/ s = -- &1)/\
 494   &0 < ups_x x1 x3 x5 ==>
 495    (\q. mk_planar2 v0 v1 q x1 x2 x3 x5 x6 s) continuous at v2`,
 496 REWRITE_TAC[dist;SET_RULE`(s = &1 \/ s = -- &1)<=> s IN { -- &1, &1}`]
 497 THEN REPEAT STRIP_TAC
 498 THEN ASM_SIMP_TAC[MK_PLANAR_V3_DEFOR_V2_FUN]
 499 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]
 500 THEN MATCH_MP_TAC CONTINUOUS_ADD
 501 THEN ASM_SIMP_TAC[CONTINUOUS_CONST;lemma30000]
 502 THEN MATCH_MP_TAC CONTINUOUS_AT_COMPOSE
 503 THEN ASM_REWRITE_TAC[]
 504 THEN MATCH_MP_TAC CONTINUOUS_SUB
 505 THEN ASM_SIMP_TAC[CONTINUOUS_CONST;CONTINUOUS_AT_ID]);;
 506
 507  end;;
 508
 509
 510 (*
 511 let check_completeness_claimA_concl =
 512   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 513 *)
 514
 515
 516
 517