1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================== *)
12 module Lead_fan = struct
18 open Hypermap_of_fan;;
22 open Hypermap_of_fan;;
28 (* ========================================================================== *)
30 (* ========================================================================== *)
35 let exist_fan=prove(`(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
37 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
42 (!y1:real^3 y2:real^3. (y1 IN aff_ge {x} {v} INTER ballnorm_fan x) /\ y2 IN (aff_ge {x} {v1, w1} INTER ballnorm_fan x)
43 ==> h <= dist(y1,y2) ))`,
45 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
46 ` (v:real^3)`] remark1_fan)
48 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
49 ` (v1:real^3)`] remark1_fan)
51 THEN MATCH_MP_TAC( ISPECL [`aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x`;
52 `aff_ge {(x:real^3)} {(v1:real^3), (w1:real^3)} INTER ballnorm_fan x`] SEPARATE_CLOSED_COMPACT)
53 THEN MP_TAC(ISPECL[`(x:real^3) `;` (v:real^3)`;` (w:real^3)`]closed_point_fan)
55 THEN MP_TAC(ISPECL[`(x:real^3) `;` (v1:real^3)`;` (w1:real^3)`]compact_aff_ge_ballnorm_fan) THEN RESA_TAC
56 THEN FIND_ASSUM(MP_TAC)`FAN(x:real^3,V,E)`
57 THEN REWRITE_TAC[FAN;fan7] THEN STRIP_TAC
58 THEN POP_ASSUM(fun th-> MP_TAC(ISPECL[`{(v:real^3)}`;`{(v1:real^3),(w1:real^3)}`]th))
59 THEN ASM_REWRITE_TAC[UNION; IN_ELIM_THM;]
60 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[EXTENSION;]
61 THEN ASM_REWRITE_TAC[IN_SING; SET_RULE`(!x. x = v <=> x = v') <=> v =v'`;SET_RULE`(?v'. v' IN V /\ v = v')<=> v IN V`]
62 THEN SUBGOAL_THEN `{v:real^3} INTER {v1,w1} ={}` ASSUME_TAC
64 REWRITE_TAC[INTER;IN_SING; EXTENSION; EMPTY; IN_ELIM_THM] THEN ASM_SET_TAC[];
66 ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; SET_RULE`(A INTER C) INTER (B INTER C)= (A INTER B) INTER C`;]
67 THEN ASSUME_TAC(AFFINE_SING) THEN MP_TAC(ISPEC`{ (x:real^3) }` AFFINE_HULL_EQ )
68 THEN RESA_TAC THEN RESA_TAC THEN REWRITE_TAC[ballnorm_fan;INTER; IN_SING; EXTENSION;EMPTY;IN_ELIM_THM;
69 ] THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[DIST_REFL ] THEN REAL_ARITH_TAC]);;
74 let ballsets_fan=new_definition`ballsets_fan (s:real^3->bool) (h:real)= {y:real^3| ?x:real^3. dist(x,y) < h /\ x IN s} `;;
77 let exists_ballsets_fan =prove(
78 `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
79 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
83 /\ (ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h INTER (aff_ge {x} {v1, w1} INTER ballnorm_fan x) = {})
85 REPEAT GEN_TAC THEN DISCH_TAC THEN
86 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exist_fan) THEN RES_TAC
87 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ballsets_fan; INTER; IN_ELIM_THM]
88 THEN DISCH_TAC THEN EXISTS_TAC`h:real`
89 THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;] THEN GEN_TAC THEN EQ_TAC
92 THEN DISCH_THEN(LABEL_TAC"a")
93 THEN STRIP_TAC THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPECL[`x'':real^3`;`x':real^3`]th))
94 THEN ASM_REWRITE_TAC[EMPTY;IN_ELIM_THM] THEN REPEAT (POP_ASSUM MP_TAC)
96 REWRITE_TAC[EMPTY;IN_ELIM_THM]]);;
101 (*-------------------------------------------------------------------------------------------*)
102 (* cone_ge_fan_inter_aff_ge_is_empty *)
103 (*-------------------------------------------------------------------------------------------*)
107 let cone_ge_fan=new_definition`cone_ge_fan (x:real^3) (s:real^3->bool)= {y:real^3| ?a:real z:real^3. (&0 <= a)/\(z IN s) /\ (y =a % (z - x) + x)}`;;
113 let cone_ge_fan_inter_aff_ge_is_empty=prove(
114 `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
115 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
120 /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} = {x})
124 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
125 `(v:real^3)`] remark1_fan)
127 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
128 `(v1:real^3)`] remark1_fan)
130 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;
131 `(w:real^3)`;` (v1:real^3)`;` (w1:real^3)`] exists_ballsets_fan)
132 THEN ASM_REWRITE_TAC[]
133 THEN MATCH_MP_TAC MONO_EXISTS
134 THEN GEN_TAC THEN STRIP_TAC THEN STRIP_TAC
137 ASM_REWRITE_TAC[REAL_ARITH`a> &0 <=> &0< a`];(*1*)
138 REWRITE_TAC [cone_ge_fan; EXTENSION; IN_SING; INTER; IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC
140 ASM_CASES_TAC `(x':real^3)=(x:real^3)`
141 THENL(*3*)[ASM_REWRITE_TAC[];(*3*)
142 MP_TAC (ISPECL [`x':real^3`; `x:real^3`] imp_norm_not_zero_fan)
143 THEN RES_TAC THEN STRIP_TAC THEN
144 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a")
145 THEN REPEAT STRIP_TAC
146 THEN ASM_REWRITE_TAC[]
147 THEN ABBREV_TAC `(x1:real^3)= inv (norm ((x':real^3)-(x:real^3))) % (x'-x) + x`
148 THEN SUBGOAL_THEN `(x1:real^3) IN ballnorm_fan (x:real^3)` ASSUME_TAC
149 THENL(*4*)[ REWRITE_TAC[ballnorm_fan; IN_ELIM_THM]
151 THEN REWRITE_TAC[dist]
152 THEN REWRITE_TAC[VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --(a)`; VECTOR_ARITH `-- ((a:real)% (v:real^3))=(-- a) % v`; NORM_MUL;REAL_ABS_NEG; REAL_ABS_INV; REAL_ABS_NORM]
153 THEN USE_THEN "a" MP_TAC
154 THEN MP_TAC(ISPEC `norm ((x':real^3)-(x:real^3))` REAL_MUL_LINV)
155 THEN ASM_MESON_TAC[];(*4*)
156 SUBGOAL_THEN `(x1:real^3) IN aff_ge {(x:real^3)} {(v1:real^3),(w1:real^3)}` ASSUME_TAC
157 THENL(*5*)[REMOVE_THEN "a" MP_TAC THEN
158 MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC
159 THEN REWRITE_TAC[IN_ELIM_THM]
161 EXISTS_TAC `&1 - inv (norm((x':real^3)-(x:real^3))) + inv (norm (x' - x)) * (t1:real) `
162 THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t2:real) `
163 THEN EXISTS_TAC `inv (norm((x':real^3)-(x:real^3))) * (t3:real) `
165 THEN REWRITE_TAC[VECTOR_ARITH`((a:real)-(b:real)+(c:real))%(v:real^3)=(a:real) % v -(b:real)% v+(c:real) %(v:real^3)`;
166 VECTOR_ARITH `&1 % (x:real^3)=x`; VECTOR_ARITH `((a:real)*(b:real)) % (v:real^3)= (a % (b % v))`;
167 VECTOR_ARITH `(x - inv (norm (x' - x)) % x + inv (norm (x' - x)) % t1 % x) +
168 inv (norm (x' - x)) % t2 % v1 +
169 inv (norm (x' - x)) % t3 % w1 =(inv (norm ((x':real^3)- x))) % ( t1 % x + t2 % v1+ t3% w1 -x)+ (x:real^3)`
173 THENL(*6*)[SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC
174 THENL(*7*)[ MATCH_MP_TAC REAL_LE_INV
175 THEN MESON_TAC[NORM_POS_LE];(*7*)
176 ASM_MESON_TAC[REAL_LE_MUL]](*7*);(*6*)
179 THENL(*7*)[ SUBGOAL_THEN `&0 <= inv (norm ((x':real^3)-(x:real^3))) ` ASSUME_TAC
180 THENL(*8*)[ MATCH_MP_TAC REAL_LE_INV
181 THEN MESON_TAC[NORM_POS_LE];(*8*)
182 ASM_MESON_TAC[REAL_LE_MUL; REAL_ARITH `(a:real)>= &0 <=> &0 <= a`]](*8*);(*7*)
184 REWRITE_TAC[REAL_ARITH `(&1 - inv (norm (x' - x)) + inv (norm (x' - x)) * t1) +
185 inv (norm (x' - x)) * t2 +
186 inv (norm (x' - x)) * t3= &1 - inv (norm (x' - x)) + inv (norm (x' - x)) * (t1 + t2 + t3)`]
189 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `(a:real) * &1 = a`; REAL_ARITH `&1 - (a:real) +(a:real) = &1`];(*8*)
191 SUBGOAL_THEN `(x':real^3) -(x:real^3)= (t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3)` ASSUME_TAC
192 THENL(*9*)[ ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;(*9*)
193 SUBGOAL_THEN `inv (norm ((x':real^3) -(x:real^3)) ) % ((x':real^3) -(x:real^3)) = inv (norm ((x':real^3) -(x:real^3)) ) % ((t1:real) % (x:real^3) + (t2:real) % (v1:real^3) + (t3:real) % (w1:real^3) -(x:real^3))` ASSUME_TAC
194 THENL(*10*)[ASM_MESON_TAC[ VECTOR_MUL_LCANCEL ];(*10*)
195 ASM_MESON_TAC[]](*10*)](*9*)](*8*)](*7*)](*6*); (*5*)
197 SUBGOAL_THEN `(x1:real^3) IN ballsets_fan (aff_ge {(x:real^3)} {(v:real^3)} INTER ballnorm_fan x) (h:real)` ASSUME_TAC
199 SUBGOAL_THEN `norm ((z:real^3)-(x:real^3))= &1` ASSUME_TAC
200 THENL(*7*)[FIND_ASSUM(MP_TAC)`z IN ballnorm_fan (x:real^3)`
201 THEN REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; NORM_SUB];(*7*)
203 THEN DISCH_THEN (LABEL_TAC "k")
204 THEN SUBGOAL_THEN `(x':real^3)- (x:real^3)= (a:real) % ((z:real^3)-x )` ASSUME_TAC
205 THENL(*8*)[ FIND_ASSUM(MP_TAC)`x'=a %(z-x) +x:real^3` THEN VECTOR_ARITH_TAC;(*8*)
207 SUBGOAL_THEN `norm((x':real^3)- (x:real^3))= norm((a:real) % ((z:real^3)-x ))` ASSUME_TAC
208 THENL(*9*)[ASM_SET_TAC[];(*9*)
211 THEN REWRITE_TAC[NORM_MUL]
212 THEN POP_ASSUM MP_TAC
213 THEN USE_THEN "k" (fun th -> REWRITE_TAC[th])
214 THEN REDUCE_ARITH_TAC
215 THEN SUBGOAL_THEN `abs (a:real)=a`ASSUME_TAC
216 THENL(*10*)[FIND_ASSUM(MP_TAC)`&0 <= a:real` THEN REAL_ARITH_TAC;(*10*)
217 POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN DISCH_THEN(LABEL_TAC"l")
218 THEN DISCH_THEN (LABEL_TAC "n")
219 THEN REMOVE_THEN "l" MP_TAC THEN USE_THEN "n" (fun th-> REWRITE_TAC[SYM th])
220 THEN DISCH_THEN (LABEL_TAC "l")
221 THEN SUBGOAL_THEN `(inv (norm (x'- x))) % ((x':real^3)- (x:real^3)) = (inv (norm (x' - x))) % (norm (x' - x) % ((z:real^3)- x ))` ASSUME_TAC
222 THENL(*11*)[POP_ASSUM MP_TAC THEN MESON_TAC[];(*11*)
224 THEN REWRITE_TAC[VECTOR_ARITH `(a:real)%(b:real)%(v:real^3)=(a*b)%v`]
225 THEN MP_TAC(ISPEC`norm((x':real^3)-(x:real^3))`REAL_MUL_LINV)
226 THEN FIND_ASSUM(fun th ->REWRITE_TAC[th]) `~(norm((x':real^3)-(x:real^3))= &0)`
227 THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[th]) THEN REDUCE_VECTOR_TAC
228 THEN REWRITE_TAC[VECTOR_ARITH `((a:real^3)=(z:real^3)-(x:real^3))<=>(a+x=z)`]
229 THEN FIND_ASSUM(fun th-> REWRITE_TAC[th])`inv (norm (x' - x)) % (x' - x) + x = x1:real^3`
230 THEN DISCH_TAC THEN ASM_REWRITE_TAC[INTER]](*11*)](*10*)](*9*)](*8*)](*7*);(*6*)
231 ASM_SET_TAC[]](*6*)](*5*)](*4*)](*3*);(*2*)
233 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
234 THENL(*2*)[ EXISTS_TAC `&0` THEN EXISTS_TAC`inv (norm ((v:real^3)-(x:real^3))) % (v-x) + x` THEN REDUCE_VECTOR_TAC
236 THENL(*3*)[ REAL_ARITH_TAC;(*3*)
238 THENL(*4*)[ REWRITE_TAC[ballsets_fan; IN_ELIM_THM]
239 THEN EXISTS_TAC `inv(norm((v:real^3)-(x:real^3))) % (v-x)+x`
240 THEN REWRITE_TAC[dist; VECTOR_ARITH `(a)-a= vec 0`; NORM_0]
242 THENL(*5*)[ ASM_SET_TAC[];(*5*)
246 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC
247 THEN REWRITE_TAC[IN_ELIM_THM]
248 THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))`
249 THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))`
252 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*7*)
254 THENL(*8*)[ REAL_ARITH_TAC;(*8*)
255 VECTOR_ARITH_TAC](*8*)](*7*);(*6*)
257 REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
258 THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC
259 THENL(*7*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*7*)
261 SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC
262 THENL(*8*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*8*)
264 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
265 THENL(*9*)[MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*9*)
266 POP_ASSUM MP_TAC THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*9*)](*8*)](*7*)](*6*)](*5*);(*4*)
267 REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
268 THEN SUBGOAL_THEN `inv(norm((v:real^3)-(x:real^3))) > &0 ` ASSUME_TAC
269 THENL(*5*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_gl_zero_fan) THEN RESA_TAC;(*5*)
270 SUBGOAL_THEN `abs(inv(norm((v:real^3)-(x:real^3))))=inv(norm((v:real^3)-(x:real^3)))` ASSUME_TAC
271 THENL(*6*)[ASM_REWRITE_TAC[REAL_ABS_REFL] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*)
272 POP_ASSUM (fun th -> REWRITE_TAC[th])
273 THEN SUBGOAL_THEN `~ (norm ((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
274 THENL(*7*)[ MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_not_zero_fan) THEN RESA_TAC;(*7*)
275 POP_ASSUM MP_TAC THEN MESON_TAC[REAL_MUL_RINV;REAL_MUL_SYM]](*7*)](*6*)](*5*)](*4*)](*3*);(*2*)
277 MP_TAC(ISPECL[`x:real^3`;`v1:real^3`;`w1:real^3`]AFF_GE_1_2) THEN RESA_TAC THEN REWRITE_TAC[IN_ELIM_THM]
279 EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`
280 THEN STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; STRIP_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]]]]]]);;
283 let subset_by_inequality_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3) (h:real) (h1:real).
284 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E /\ h < h1
286 cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1}
289 THEN SUBGOAL_THEN` cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x) SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h1)INTER ballnorm_fan x ) ` ASSUME_TAC
291 REWRITE_TAC[cone_ge_fan; SUBSET;IN_ELIM_THM]
294 THEN EXISTS_TAC`a:real`
295 THEN EXISTS_TAC`z:real^3`
296 THEN ASM_REWRITE_TAC[]
297 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
298 THEN POP_ASSUM MP_TAC
299 THEN REWRITE_TAC[ballsets_fan;INTER; IN_ELIM_THM]
301 THEN EXISTS_TAC`x'':real^3`
302 THEN ASM_REWRITE_TAC[]
303 THEN REPEAT (POP_ASSUM MP_TAC)
309 let cone_ge_fan_inter_aff_ge_is_empty_fan=prove( `(!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
310 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
316 /\ (cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x ) INTER aff_ge {x} {v1, w1} SUBSET {x})
320 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;
321 `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty)
323 THEN DISJ_CASES_TAC(REAL_ARITH `(h >= &1) \/ (&1 > h)` )
325 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;
326 `(w:real^3) `;`(v1:real^3)`;` (w1:real^3)`; `&1/ &2`; `(h:real)`]subset_by_inequality_fan)
328 THEN POP_ASSUM MP_TAC
329 THEN MP_TAC(REAL_ARITH`h>= &1==> &1 / &2 <h`)
330 THEN ASM_REWRITE_TAC[]
332 THEN ASM_REWRITE_TAC[]
334 THEN EXISTS_TAC `&1/ &2`
335 THEN ASM_REWRITE_TAC[]
339 THEN ASM_REWRITE_TAC[]
340 THEN ASM_SET_TAC[]]);;
345 let rcone_subset_cone=prove(
346 `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) h:real.
347 FAN(x,V,E) /\ {v,w} IN E /\(&0< h) /\ (h< &1)
352 (rcone_fan x v h1) SUBSET cone_ge_fan x ((ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan x) h)INTER ballnorm_fan x )`,
354 REWRITE_TAC[rcone_fan;cone_ge_fan; SUBSET;IN_ELIM_THM;dist]
355 THEN REPEAT STRIP_TAC
356 THEN EXISTS_TAC`(&2 -(h:real) pow 2)/ &2`
359 REWRITE_TAC[REAL_ARITH`&1 > (&2 -(h:real) pow 2)/ &2 <=> h pow 2> &0`]
360 THEN MP_TAC (ISPECL[`h:real`;`2`]REAL_POW_LT)
361 THEN REPEAT(POP_ASSUM MP_TAC)
366 REWRITE_TAC[REAL_ARITH`(&2 -h pow 2)/ &2> &0<=> &2 > h pow 2`]
367 THEN MATCH_MP_TAC(REAL_ARITH` h pow 2<= &1 ==> &2 > h pow 2`)
368 THEN MATCH_MP_TAC (ISPECL[`2`;`h:real`;]REAL_POW_1_LE)
369 THEN POP_ASSUM MP_TAC
370 THEN POP_ASSUM MP_TAC
374 THEN EXISTS_TAC `norm ((x':real^3)-(x:real^3))`
375 THEN EXISTS_TAC `inv(norm ((x':real^3)-(x:real^3)))%(x'-x)+x`
376 THEN REWRITE_TAC[NORM_POS_LE]
377 THEN POP_ASSUM MP_TAC
378 THEN DISJ_CASES_TAC(SET_RULE`((x':real^3)-(x:real^3)= vec 0) \/ ~((x':real^3)-(x:real^3)= vec 0)`)
381 ASM_REWRITE_TAC[NORM_0;DOT_LZERO;] THEN REDUCE_ARITH_TAC THEN REAL_ARITH_TAC;(*1*)
383 REWRITE_TAC[VECTOR_ARITH`(A+B)-B=A:real^3`;VECTOR_MUL_ASSOC]
384 THEN MP_TAC(ISPEC`x':real^3- x`NORM_EQ_0)
386 THEN MP_TAC(ISPEC`norm(x':real^3- x)`REAL_MUL_LINV)
387 THEN ASM_REWRITE_TAC[REAL_MUL_SYM]
389 THEN REDUCE_VECTOR_TAC
390 THEN REWRITE_TAC[VECTOR_ARITH`A-B+B=A:real^3`]
391 THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC
393 REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
394 THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]imp_norm_ge_zero_fan)
395 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`]
397 THEN MP_TAC(ISPEC`inv(norm((x':real^3)-(x:real^3)))`REAL_ABS_REFL)
398 THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`]
402 THEN SUBGOAL_THEN` inv (norm (x' - x)) % (x' - x) + x IN ballsets_fan (aff_ge {x} {v} INTER ballnorm_fan (x:real^3)) (h:real)` ASSUME_TAC
405 REWRITE_TAC[ballsets_fan;IN_ELIM_THM;dist]
406 THEN EXISTS_TAC`inv (norm (v - x)) % (v - x) + (x:real^3)`
410 REWRITE_TAC[VECTOR_ARITH`((v:real^3)+b)-(u+b)= (v-u)`;]
411 THEN SUBGOAL_THEN`norm(inv(norm(v-x))%(v:real^3-x)-inv(norm(x'-x))%(x'-x)) pow 2< h pow 2` ASSUME_TAC
413 REWRITE_TAC[NORM_POW_2;DOT_LSUB;DOT_RSUB]
414 THEN REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_SQUARE_NORM; REAL_ARITH`a-b-(c-d)=a+d-b-c`;
415 REAL_ARITH`a*a*b pow 2=(a*b) pow 2`;DOT_SYM;REAL_ARITH`a+b-e*d*c-d*e*c=a+b- &2 * d*e *c`]
416 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`;
417 `(v:real^3)`;] remark1_fan)
419 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan)
420 THEN REWRITE_TAC[NORM_SUB]
422 THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV)
424 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 pow 2= &1`;
425 REAL_ARITH`&1+ &1 - &2 * a< h pow 2 <=> a > (&2- h pow 2)/ &2`]
426 THEN MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE)
428 THEN SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC
431 REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
433 MP_TAC (ISPEC `(x':real^3)-(x:real^3)` NORM_POS_LE)
435 THEN SUBGOAL_THEN ` norm((x:real^3)-(x':real^3))> &0 ` ASSUME_TAC
438 ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')> &0 <=> norm(x'-x)> &0`]
439 THEN REPEAT( POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*7*)
441 MP_TAC(ISPECL[`(&2 - (h:real) pow 2) / &2`;
442 `inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`;
443 `norm (x:real^3 - x')`]REAL_LT_LMUL_EQ)
444 THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`]
445 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
446 THEN POP_ASSUM(fun th->REWRITE_TAC[])
447 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`]
449 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
450 THEN MP_TAC(ISPECL[`norm (x:real^3 - x') * (&2 - (h:real) pow 2) / &2`;
451 `norm (x:real^3 - x')*inv (norm (x:real^3 - x')) * inv (norm (v - x)) * ((v - x) dot (x' - x))`;
452 `norm (v:real^3 - x)`]REAL_LT_LMUL_EQ)
453 THEN REWRITE_TAC[REAL_ARITH`a<b <=> b>a`]
454 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
455 THEN POP_ASSUM(fun th->REWRITE_TAC[])
456 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`(A<=>B)<=>(B<=>A)`]
458 THEN POP_ASSUM(fun th->REWRITE_TAC[th])
459 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C*D*E>a*b*c<=>(C*B)*(D*A)*E>b*c*a`]
460 THEN ONCE_REWRITE_TAC[NORM_ARITH`norm (x:real^3- x')= norm(x'-x)`]
461 THEN ASM_REWRITE_TAC[]
462 THEN REDUCE_ARITH_TAC
463 THEN GEN_REWRITE_TAC(RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[NORM_SUB]
464 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DOT_SYM]
465 THEN ASM_REWRITE_TAC[]](*7*)](*6*)(*5*);
467 ASM_REWRITE_TAC[NORM_LT_SQUARE;DOT_SQUARE_NORM]](*5*);(*4*)
470 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(w:real^3)`;
471 `(v:real^3)`;] remark1_fan)
474 SUBGOAL_THEN`inv(norm(v-x:real^3)) % (v-x) +x IN aff_ge {x} {v}` ASSUME_TAC
476 MP_TAC(ISPECL[`x:real^3`;`v:real^3`]AFF_GE_1_1) THEN RESA_TAC
477 THEN REWRITE_TAC[IN_ELIM_THM]
478 THEN EXISTS_TAC `&1 - inv (norm ((v:real^3)-(x:real^3)))`
479 THEN EXISTS_TAC `inv (norm ((v:real^3)-(x:real^3)))`
484 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan) THEN RES_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*6*)
488 VECTOR_ARITH_TAC]](*6*);(*5*)
490 SUBGOAL_THEN` inv (norm (v- x)) % (v - x) + x IN ballnorm_fan (x:real^3)` ASSUME_TAC
492 REWRITE_TAC[ballnorm_fan; IN_ELIM_THM; dist; VECTOR_ARITH `(x:real^3)-((a:real^3)+(x:real^3))= --a`; NORM_NEG; NORM_MUL ]
493 THEN MP_TAC(ISPECL[`v:real^3`;`x:real^3`]imp_norm_ge_zero_fan)
494 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> v=x`]
496 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`(a:real^3)=b <=> a - b = vec 0`]
498 THEN MP_TAC(ISPEC`inv(norm((v:real^3)-(x:real^3)))`REAL_ABS_REFL)
499 THEN GEN_REWRITE_TAC( LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[REAL_ARITH`&0<= (a:real) <=> a >= &0`]
501 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3)`;] imp_norm_not_zero_fan)
502 THEN REWRITE_TAC[NORM_SUB]
504 THEN MP_TAC(ISPEC`norm(v:real^3- x)`REAL_MUL_LINV)
506 THEN ASM_REWRITE_TAC[];(*6*)
507 ASM_SET_TAC[]](*6*)](*5*)](*4*);(*3*)
508 ASM_SET_TAC[]]]]]]);;
523 let inter_is_empty=prove(`
524 !(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
525 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
530 rcone_fan x v h1 INTER aff_ge {x} {v1, w1} = {}
533 THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3) `
534 ;`(w:real^3)`;` (v1:real^3) `;`(w1:real^3)`]cone_ge_fan_inter_aff_ge_is_empty_fan)
536 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`(v:real^3)`;
537 `(w:real^3)`;` h:real`]rcone_subset_cone)
539 THEN POP_ASSUM MP_TAC
540 THEN REWRITE_TAC[REAL_ARITH`&0<h<=> h> &0`; REAL_ARITH`h< &1 <=> &1 >h`]
542 THEN SUBGOAL_THEN`(rcone_fan x v h1 INTER aff_ge {x} {v1, w1}) SUBSET
543 {x:real^3}` ASSUME_TAC
546 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (h1:real)`]origin_not_in_rcone_fan)
547 THEN REPEAT STRIP_TAC
548 THEN EXISTS_TAC`h1:real`
549 THEN ASM_REWRITE_TAC[]
550 THEN POP_ASSUM MP_TAC
551 THEN POP_ASSUM MP_TAC
552 THEN REWRITE_TAC[SUBSET; IN_SING;EXTENSION;EMPTY]
553 THEN REPEAT STRIP_TAC
557 THEN POP_ASSUM MP_TAC
558 THEN DISCH_THEN(LABEL_TAC"a")
561 THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC`x':real^3`th))
562 THEN ASM_REWRITE_TAC[]
563 THEN POP_ASSUM MP_TAC
564 THEN DISCH_THEN(LABEL_TAC"a")
566 THEN REMOVE_THEN "a" MP_TAC
567 THEN ASM_REWRITE_TAC[]
569 THEN SUBGOAL_THEN`x:real^3 IN rcone_fan x v h1` ASSUME_TAC
574 let avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3)(w2:real^3).
575 FAN(x,V,E) /\ ~(v IN {v1,w1}) /\ {v1,w1} IN E /\ {v,w} IN E
580 /\ rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),(w2:real^3)) h INTER aff_ge {x} {v1, w1} = {}
584 THEN REWRITE_TAC[rw_dart_fan]
585 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (v1:real^3)` ;`(w1:real^3)`]inter_is_empty)
587 THEN EXISTS_TAC`h1:real`
593 let avoids1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (w1:real^3).
594 FAN(x,V,E) /\ {v,w} IN E /\ {v,w1} IN E
599 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v, w1} = {}`,
601 THEN REWRITE_TAC[rw_dart_fan]
602 THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3)`;
603 ` (w:real^3)`;`(w1:real^3)`]IBZWFFH)
605 THEN EXISTS_TAC`&1/ &2`
606 THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`]
607 THEN ASM_SET_TAC[]);;
610 let finish_avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (v1:real^3) (w1:real^3).
611 FAN(x,V,E) /\ {v,w} IN E /\ {v1,w1} IN E
616 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER aff_ge {x} {v1, w1} = {}`,
619 THEN DISJ_CASES_TAC(SET_RULE`~(v:real^3 IN {v1,w1})\/ (v=v1\/ v=w1)`)
621 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`(v1:real^3)`;`w1:real^3`;` (sigma_fan x V E v w:real^3)`]avoids_fan)
629 THEN POP_ASSUM MP_TAC
630 THEN DISCH_THEN(LABEL_TAC"A")
632 THEN REMOVE_THEN "A" MP_TAC
633 THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)])
635 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`w1:real^3`]avoids1_fan)
639 THEN POP_ASSUM MP_TAC
640 THEN DISCH_THEN(LABEL_TAC"A")
642 THEN REMOVE_THEN "A" MP_TAC
643 THEN POP_ASSUM( fun th-> REWRITE_TAC[SYM(th)])
644 THEN ONCE_REWRITE_TAC[SET_RULE`{X,Y}={Y,X}`]
646 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(w:real^3) `;`v1:real^3`]avoids1_fan)
649 let continuous_set_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) (h:real) (h1:real).
650 FAN(x,V,E) /\ {v,w} IN E /\ h1 <= h
652 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h1`,
655 THEN REWRITE_TAC[rw_dart_fan]
656 THEN SUBGOAL_THEN `rcone_fan x v h SUBSET rcone_fan x v h1` ASSUME_TAC
658 REWRITE_TAC[rcone_fan;SUBSET; IN_ELIM_THM]
659 THEN REPEAT STRIP_TAC
660 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
661 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
662 THEN MP_TAC(ISPECL[`dist((v:real^3),x)`;`h1:real`;`h:real`] REAL_LE_LMUL)
664 THEN MP_TAC(ISPECL[`dist((x':real^3),x)`;`dist((v:real^3),x)* (h1:real)`;`dist((v:real^3),x)* (h:real)`] REAL_LE_LMUL)
666 THEN REPEAT (POP_ASSUM MP_TAC)
675 let finish_avoids1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E':(real^3->bool)->bool) (v:real^3) (w:real^3).
676 FAN(x,V,E) /\ {v,w} IN E /\ E' SUBSET E
681 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h INTER {v | ?e. e IN E' /\ v IN aff_ge {x} e}={}`,
684 THEN REWRITE_TAC[xfan; IN_ELIM_THM]
685 THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]set_edges_is_finite_fan)
687 THEN MP_TAC(ISPECL [`(E':(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`] FINITE_SUBSET)
689 THEN ABBREV_TAC`n=CARD (E':(real^3->bool)->bool)`
690 THEN REPEAT(POP_ASSUM MP_TAC)
691 THEN SPEC_TAC (`(E':(real^3->bool)->bool)`,`(E':(real^3->bool)->bool)`)
692 THEN SPEC_TAC (`n:num`,`n:num`)
696 THEN MP_TAC(ISPECL[`E':(real^3->bool)->bool`]CARD_EQ_0)
698 THEN EXISTS_TAC`&1 / &2`
699 THEN REWRITE_TAC[REAL_ARITH`&1/ &2 > &0`;REAL_ARITH`&1 > &1/ &2`]
700 THEN ASM_SET_TAC[];(*1*)
703 THEN POP_ASSUM MP_TAC
704 THEN DISCH_THEN (LABEL_TAC "A")
705 THEN REPEAT STRIP_TAC
706 THEN MP_TAC(ISPEC`(E':(real^3->bool)->bool)` CHOOSE_SUBSET)
708 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`n:num `th))
709 THEN REWRITE_TAC[ARITH_RULE `n:num <= SUC n`; HAS_SIZE]
711 THEN MP_TAC(SET_RULE` t SUBSET E' /\ E' SUBSET E ==> (t:(real^3->bool)->bool) SUBSET E`)
713 THEN REMOVE_THEN "A" (fun th-> MP_TAC(ISPEC`(t:(real^3->bool)->bool)`th))
715 THEN SUBGOAL_THEN `~((E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)= {})` ASSUME_TAC
718 THEN MP_TAC(SET_RULE`(E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)={} /\ t SUBSET E' ==> t= E'`)
720 THEN FIND_ASSUM MP_TAC`CARD (t:(real^3->bool)->bool)=n`
721 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
722 THEN ASM_REWRITE_TAC[]
725 SUBGOAL_THEN`?e. e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)`
732 THEN MP_TAC(SET_RULE`e IN (E':(real^3->bool)->bool) DIFF (t:(real^3->bool)->bool)/\
733 (E':(real^3->bool)->bool) SUBSET (E:(real^3->bool)->bool) /\ t SUBSET E' ==> e IN E'/\ e IN E/\ ~(e IN t) /\ {e} UNION t SUBSET E'`)
735 THEN MP_TAC(ISPECL [`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`(E':(real^3->bool)->bool)`] FINITE_SUBSET)
737 THEN ASSUME_TAC(SET_RULE`e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`)
738 THEN MP_TAC(ISPECL[`e:real^3->bool`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;]CARD_DELETE)
740 THEN MP_TAC(SET_RULE `e IN {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)
741 ==> ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e PSUBSET {e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`)
743 THEN MP_TAC(ISPECL[`({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))DELETE e`;`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`]CARD_PSUBSET)
744 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
745 THEN FIND_ASSUM MP_TAC`FINITE ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool))`
747 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
749 THEN MP_TAC(ARITH_RULE`CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) < CARD ( {e:(real^3->bool)} UNION (t:(real^3->bool)->bool))
750 /\ CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) = CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))-1
751 <=>CARD (({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e) +1= CARD ({e:(real^3->bool)} UNION (t:(real^3->bool)->bool))`)
752 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
753 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
754 THEN REWRITE_TAC[ARITH_RULE`A=A`; ]
755 THEN MP_TAC(SET_RULE`~(e IN t)==>({e:(real^3->bool)} UNION (t:(real^3->bool)->bool)) DELETE e=t`)
757 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
758 THEN FIND_ASSUM MP_TAC`(CARD (E':(real^3->bool)->bool)=SUC n)`
759 THEN REWRITE_TAC[ARITH_RULE`SUC n=(n:num) +1`]
761 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
763 THEN MP_TAC(ISPECL[`{e:(real^3->bool)} UNION (t:(real^3->bool)->bool)`;`E':(real^3->bool)->bool`]CARD_SUBSET_EQ)
764 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
766 THEN POP_ASSUM MP_TAC
767 THEN DISCH_THEN(LABEL_TAC"MA")
768 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]expand_edge_graph_fan)
770 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;`(w:real^3)`; `(v':real^3)`;` (w':real^3)`]finish_avoids_fan)
772 THEN POP_ASSUM MP_TAC
773 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
774 THEN POP_ASSUM MP_TAC
777 THEN ABBREV_TAC`h1= max (h:real) (h':real)`
778 THEN EXISTS_TAC`h1:real`
781 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
782 THEN REPEAT(POP_ASSUM MP_TAC)
783 THEN REAL_ARITH_TAC;(*4*)
787 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
788 THEN REPEAT(POP_ASSUM MP_TAC)
789 THEN REAL_ARITH_TAC;(*5*)
791 REMOVE_THEN "MA" MP_TAC
793 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
794 THEN REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION; INTER;]
799 ASM_REWRITE_TAC[IN_SING]
803 THEN ASM_REWRITE_TAC[]
805 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h':real)`]continuous_set_fan)
807 THEN POP_ASSUM MP_TAC
809 THEN REWRITE_TAC[REAL_ARITH`h'<= max (h:real) (h':real)`]
814 THEN ASM_REWRITE_TAC[]
816 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)` ;`(h1:real)`;` (h:real)`]continuous_set_fan)
818 THEN POP_ASSUM MP_TAC
820 THEN REWRITE_TAC[REAL_ARITH`h<= max (h:real) (h':real)`]
824 ASM_SET_TAC[]]]]]]]);;
832 let rw_dart_avoids_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3).
833 FAN(x,V,E) /\ {v,w} IN E
838 rw_dart_fan x V E ((x:real^3),(v:real^3),(w:real^3),sigma_fan x V E v w) h SUBSET yfan(x,V,E) `,
841 THEN MP_TAC(ISPECL[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]finish_avoids1_fan)
843 THEN POP_ASSUM MP_TAC
844 THEN REWRITE_TAC[SET_RULE`A SUBSET A`;yfan;xfan]
846 THEN EXISTS_TAC`h:real`
847 THEN ASM_REWRITE_TAC[]
848 THEN ASM_SET_TAC[]);;
853 (*------------------------------------------------------------------------*)
854 (*------------------------------------------------------------------------*)
858 let r_fan=new_definition`r_fan (a:real) (b:real) (c:real) = { y:real^3 | y$1 > &0 /\ y$2 > a /\ y$2 < b /\ y$3 > &0 /\ y$3 < c}`;;
862 let r1_le_fan=new_definition`r1_le_fan (a:real)={ y:real^3 | y$1 > a}`;;
865 let r2_le_fan=new_definition`r2_le_fan (a:real)={ y:real^3 | y$2 > a}`;;
869 let r3_le_fan=new_definition`r3_le_fan (a:real)={ y:real^3 | y$3 > a}`;;
873 let r1_ge_fan=new_definition`r1_ge_fan (a:real)={ y:real^3 | y$1 < a}`;;
876 let r2_ge_fan=new_definition`r2_ge_fan (a:real)={ y:real^3 | y$2 < a}`;;
878 let r3_ge_fan=new_definition`r3_ge_fan (a:real)={ y:real^3 | y$3 < a}`;;
883 let r_fan_is_inter_halfspace=prove(`!a:real b:real c:real.
884 r_fan a b c = r1_le_fan (&0) INTER r2_le_fan a INTER r2_ge_fan b INTER r3_le_fan (&0) INTER r3_ge_fan c`,
885 REWRITE_TAC[r_fan; r1_le_fan; r2_le_fan; r2_ge_fan; r3_le_fan; r3_ge_fan; INTER; IN_ELIM_THM]);;
891 let r1_ge_is_convex_fan = prove(`!a:real. convex (r1_ge_fan a)/\ open (r1_ge_fan a) `,REWRITE_TAC[r1_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
894 let r2_ge_is_convex_fan = prove(`!a:real. convex (r2_ge_fan a)/\ open (r2_ge_fan a)`,
895 REWRITE_TAC[r2_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
897 let r3_ge_is_convex_fan = prove(`!a:real. convex (r3_ge_fan a) /\ open(r3_ge_fan a)`,
898 REWRITE_TAC[r3_ge_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_LT;OPEN_HALFSPACE_COMPONENT_LT]);;
900 let r1_le_is_convex_fan = prove(`!a:real. convex (r1_le_fan a)/\ open (r1_le_fan a) `,
901 REWRITE_TAC[r1_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
903 let r2_le_is_convex_fan = prove(`!a:real. convex (r2_le_fan a)/\ open (r2_le_fan a) `,
904 REWRITE_TAC[r2_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
906 let r3_le_is_convex_fan = prove(`!a:real. convex (r3_le_fan a)/\ open (r3_le_fan a) `,
907 REWRITE_TAC[r3_le_fan] THEN REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GT;OPEN_HALFSPACE_COMPONENT_GT]);;
909 let r_is_connected_fan=prove(`!a:real b:real c:real. connected (r_fan a b c)/\convex (r_fan a b c) /\ open (r_fan a b c)`,
910 (let lemma = prove(`!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c)`,
911 ASSUME_TAC (r_fan_is_inter_halfspace) THEN ASM_REWRITE_TAC[] THEN
912 ASSUME_TAC (r1_ge_is_convex_fan) THEN ASSUME_TAC ( r2_ge_is_convex_fan) THEN
913 ASSUME_TAC (r3_ge_is_convex_fan) THEN ASSUME_TAC(r1_le_is_convex_fan) THEN
914 ASSUME_TAC(r2_le_is_convex_fan) THEN ASSUME_TAC( r3_le_is_convex_fan) THEN
915 ASM_MESON_TAC[CONVEX_INTER;OPEN_INTER])
917 SUBGOAL_THEN `!a:real b:real c:real. convex (r_fan a b c)/\ open (r_fan a b c) ` ASSUME_TAC
918 THENL [MESON_TAC[lemma];
919 ASM_MESON_TAC[CONVEX_CONNECTED]]));;
925 let rw_dart_is_image_set_spherical_coordinate=prove(`(!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real.
926 FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\ h< pi/ &2
928 IMAGE (change_spherical_coordinate_fan x v u)
929 (r_fan (azim x v u u) (azim_fan x V E v u) h)=
930 rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))) `,
931 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,ASM_SET_TAC[]) in
932 ( let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in
934 REWRITE_TAC[azim_fan;r_fan; rw_dart_fan; change_spherical_coordinate_fan;IMAGE;INTER;
935 w_dart_fan;rcone_fan;EXTENSION;IN_ELIM_THM]
936 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
937 THEN REPEAT STRIP_TAC
938 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;
939 `(E:(real^3->bool)->bool)`;` u:real^3`;` v:real^3`]remark1_fan)
941 THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
942 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[lem1]
943 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
945 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
947 THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
948 THEN REWRITE_TAC[orthonormal]
950 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
955 THEN MP_TAC(ISPEC`(x'':real^3)$3`SIN_POS_PI2)
957 THEN ONCE_REWRITE_TAC[SET_RULE`A /\ B <=> B /\ A`]
964 REWRITE_TAC[dist;vector_norm;VECTOR_ARITH`(A+B)-A=(B:real^3)`; DOT_LADD;DOT_RADD;DOT_RMUL;DOT_LMUL;]
965 THEN ONCE_REWRITE_TAC[DOT_SYM]
966 THEN ASM_REWRITE_TAC[]
967 THEN REDUCE_ARITH_TAC
968 THEN ONCE_REWRITE_TAC[DOT_SYM]
969 THEN ASM_REWRITE_TAC[]
970 THEN REDUCE_ARITH_TAC
971 THEN REWRITE_TAC[REAL_ARITH`((x'':real^3)$1 * cos (x''$2) * sin (x''$3)) * x''$1 * cos (x''$2) * sin (x''$3) +
972 (x''$1 * sin (x''$2) * sin (x''$3)) * x''$1 * sin (x''$2) * sin (x''$3) +
973 (x''$1 * cos (x''$3)) * x''$1 * cos (x''$3)=(x''$1 * x''$1)* (( sin (x''$2) pow 2 +(cos (x''$2) pow 2)) * (sin (x''$3) pow 2)+ cos (x''$3) pow 2)`]
974 THEN ASSUME_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
975 THEN ASM_REWRITE_TAC[]
976 THEN REDUCE_ARITH_TAC
977 THEN ASSUME_TAC(ISPEC`(x'':real^3)$3`SIN_CIRCLE)
978 THEN ASM_REWRITE_TAC[]
979 THEN REDUCE_ARITH_TAC
980 THEN MP_TAC(ISPEC`(x'':real^3)$1`SQRT_POW_2)
981 THEN MP_TAC(REAL_ARITH`(x'':real^3)$1> &0==> &0 <= (x'':real^3)$1`)
984 THEN MP_TAC(ISPECL[`(x'':real^3)$1`;`(x'':real^3)$1`]SQRT_MUL)
986 THEN REWRITE_TAC[REAL_ARITH`A*(A:real)=A pow 2`]
987 THEN ASM_REWRITE_TAC[e3_fan;DOT_LMUL]
988 THEN ONCE_REWRITE_TAC[GSYM vector_norm;]
989 THEN ASSUME_TAC(ISPEC`(v:real^3)-(x:real^3)`DOT_SQUARE_NORM)
990 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
991 THEN REWRITE_TAC[REAL_ARITH`(A*B)*C *D pow 2=A*D*B *(C*D)`]
992 THEN SUBGOAL_THEN`~(norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
995 ASM_REWRITE_TAC[NORM_EQ_0;VECTOR_ARITH`v-x=vec 0<=> x=v`];(*3*)
997 MP_TAC(ISPEC`norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
999 THEN ASM_REWRITE_TAC[]
1000 THEN REDUCE_ARITH_TAC
1001 THEN MP_TAC(ISPEC`((v:real^3)-(x:real^3))`NORM_POS_LT)
1002 THEN ASM_REWRITE_TAC[VECTOR_ARITH`v-x=vec 0<=> x=v`;REAL_ARITH`A>B<=> B<A`]
1004 THEN MATCH_MP_TAC REAL_LT_LMUL
1005 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 < A<=> A> &0`]
1006 THEN MATCH_MP_TAC REAL_LT_LMUL
1007 THEN ASM_REWRITE_TAC[]
1008 THEN MATCH_MP_TAC COS_MONO_LT
1009 THEN REPEAT(POP_ASSUM MP_TAC)
1010 THEN REAL_ARITH_TAC];(*2*)
1014 SUBGOAL_THEN`azim (x:real^3) (v:real^3) (u:real^3)
1016 (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1017 (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1018 (x''$1 * cos (x''$3)) % e3_fan x v u)= (x'':real^3)$2 ` ASSUME_TAC
1021 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
1022 (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1023 (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
1024 (x''$1 * cos (x''$3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
1025 `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1026 `(x''$1 * cos ((x'':real^3)$3)) * (inv (norm((v:real^3)-(x:real^3))))`;
1027 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
1028 `x''$1 * sin ((x'':real^3)$3)`;
1029 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`(x'':real^3)$2`]AZIM_UNIQUE)
1031 THEN POP_ASSUM MATCH_MP_TAC
1032 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
1036 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
1037 THEN REPEAT(POP_ASSUM MP_TAC)
1038 THEN REAL_ARITH_TAC;(*4*)
1043 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`] azim)
1044 THEN REPEAT(POP_ASSUM MP_TAC)
1045 THEN REAL_ARITH_TAC;(*5*)
1050 MATCH_MP_TAC REAL_LT_MUL
1051 THEN REPEAT(POP_ASSUM MP_TAC)
1052 THEN REAL_ARITH_TAC;(*6*)
1057 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1058 THEN REDUCE_ARITH_TAC
1059 THEN REDUCE_VECTOR_TAC
1060 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1061 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1062 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1063 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1064 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1065 THEN REDUCE_ARITH_TAC
1066 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1067 THEN REDUCE_VECTOR_TAC
1068 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1070 THEN ASM_REWRITE_TAC[]
1071 THEN REWRITE_TAC[e1_fan]
1072 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1073 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1074 THEN ONCE_REWRITE_TAC[DOT_SYM]
1075 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1076 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1077 THEN ASM_REWRITE_TAC[]
1078 THEN REDUCE_VECTOR_TAC
1080 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1081 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1082 THEN REWRITE_TAC[DOT_RZERO]
1083 THEN REAL_ARITH_TAC;(*7*)
1086 THEN VECTOR_ARITH_TAC](*7*)](*6*)](*5*)](*4*);(*3*)
1091 SUBGOAL_THEN`~collinear
1092 {(x:real^3), (v:real^3), x +
1093 (x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v (u:real^3) +
1094 (x''$1 * sin (x''$2) * sin ((x'':real^3)$3)) % e2_fan x v u +
1095 (x''$1 * cos (x''$3)) % e3_fan x v u}`ASSUME_TAC
1098 ONCE_REWRITE_TAC[lem]
1099 THEN REWRITE_TAC[collinear1_fan]
1100 THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2; IN_ELIM_THM; REAL_ARITH`A+B= &1<=>A= &1-B`]
1102 THEN POP_ASSUM MP_TAC
1103 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1104 THEN REWRITE_TAC[VECTOR_ARITH`A+B=(&1-c) % A+ c % D<=>B=c%(D-A)`]
1106 THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1107 (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1108 (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e1_fan x v u =
1109 ((v':real) % ((v:real^3) - (x:real^3))) dot e1_fan x v u` ASSUME_TAC
1111 ASM_REWRITE_TAC[];(*5*)
1114 THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1115 THEN ASM_REWRITE_TAC[DOT_SYM]
1116 THEN REDUCE_ARITH_TAC
1117 THEN SUBGOAL_THEN`((x''$1 * cos (x''$2) * sin (x''$3)) % e1_fan x v u +
1118 (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1119 (x''$1 * cos ((x'':real^3)$3)) % e3_fan x v (u:real^3)) dot e2_fan x v u =
1120 ((v':real) % ((v:real^3) - (x:real^3))) dot e2_fan x v u` ASSUME_TAC
1122 ASM_REWRITE_TAC[];(*6*)
1125 THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1126 THEN ASM_REWRITE_TAC[DOT_SYM]
1127 THEN REDUCE_ARITH_TAC
1128 THEN REWRITE_TAC[REAL_ENTIRE]
1132 REPEAT (POP_ASSUM MP_TAC)
1133 THEN REAL_ARITH_TAC;(*7*)
1138 REPEAT (POP_ASSUM MP_TAC)
1139 THEN REAL_ARITH_TAC;(*8*)
1142 MP_TAC(ISPEC`(x'':real^3)$2`SIN_CIRCLE)
1143 THEN ASM_REWRITE_TAC[]
1144 THEN REAL_ARITH_TAC;
1146 REPEAT (POP_ASSUM MP_TAC)
1147 THEN REAL_ARITH_TAC];
1149 REPEAT (POP_ASSUM MP_TAC)
1150 THEN REAL_ARITH_TAC](*7*)](*6*)](*5*);(*4*)
1153 REPEAT(POP_ASSUM MP_TAC)
1154 THEN DISJ_CASES_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1
1155 \/ ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) >1)`)
1158 THEN REPEAT STRIP_TAC
1159 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
1160 THEN ASM_REWRITE_TAC[]
1161 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1162 THEN ASM_REWRITE_TAC[]
1163 THEN FIND_ASSUM MP_TAC`(x'':real^3)$2 > azim (x:real^3) (v:real^3) u (u:real^3)`
1164 THEN REWRITE_TAC[AZIM_REFL]
1165 THEN REAL_ARITH_TAC;(*5*)
1169 THEN REPEAT STRIP_TAC
1170 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1171 THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
1173 THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
1180 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x:real^3) +
1181 (x''$1 * cos (x''$2) * sin ((x'':real^3)$3)) % e1_fan x (v:real^3) (u:real^3) +
1182 (x''$1 * sin (x''$2) * sin (x''$3)) % e2_fan x v u +
1183 (x''$1 * cos (x''$3)) % e3_fan x v u`]AZIM_EQ_0_GE_ALT)
1185 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;]AZIM_REFL)
1186 THEN REPEAT(POP_ASSUM MP_TAC)
1187 THEN REAL_ARITH_TAC](*6*)](*5*)](*4*)](*3*)](*2*);(*1*)
1191 ONCE_REWRITE_TAC[GSYM EXTENSION]
1192 THEN DISJ_CASES_TAC(ARITH_RULE`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))>1
1193 \/ ~(CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) >1)`)
1195 ASM_REWRITE_TAC[wedge;IN_ELIM_THM]
1197 THEN POP_ASSUM MP_TAC
1198 THEN DISCH_THEN(LABEL_TAC"A")
1199 THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
1200 THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
1201 THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
1206 THEN REMOVE_THEN "A" MP_TAC
1207 THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
1208 THEN REDUCE_ARITH_TAC
1209 THEN REAL_ARITH_TAC;(*3*)
1212 MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
1214 THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
1215 THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
1217 THEN ASM_REWRITE_TAC[]
1223 REWRITE_TAC[ARCV_ANGLE; angle;]
1224 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
1226 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
1227 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
1228 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
1229 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
1231 THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
1232 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1233 THEN REWRITE_TAC[DE_MORGAN_THM]
1234 THEN REPEAT(POP_ASSUM MP_TAC)
1235 THEN REAL_ARITH_TAC;(*5*)
1237 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
1239 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
1240 THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
1242 THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
1244 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
1245 THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
1247 THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1249 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1250 THEN ASM_REWRITE_TAC[]
1251 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1252 THEN ASM_REWRITE_TAC[]
1253 THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
1254 THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
1255 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
1256 THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
1257 THEN ONCE_REWRITE_TAC[GSYM real_div;]
1258 THEN REWRITE_TAC[dist;arcV]
1260 THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
1262 THEN MP_TAC(ISPEC`h:real`ACS_COS)
1264 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
1266 THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
1267 THEN POP_ASSUM MATCH_MP_TAC
1268 THEN REWRITE_TAC[COS_BOUNDS]
1269 THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
1270 THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
1271 THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
1272 THEN REAL_ARITH_TAC](*5*);(*4*)
1275 MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1276 `e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
1277 THEN ASM_REWRITE_TAC[]
1278 THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
1281 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1282 `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1284 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
1285 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
1287 THEN POP_ASSUM MATCH_MP_TAC
1288 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
1292 THEN REAL_ARITH_TAC;(*6*)
1297 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1298 THEN REDUCE_ARITH_TAC
1299 THEN REDUCE_VECTOR_TAC
1300 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1301 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1302 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1303 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1304 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1305 THEN REDUCE_ARITH_TAC
1306 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1307 THEN REDUCE_VECTOR_TAC
1308 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1310 THEN ASM_REWRITE_TAC[]
1311 THEN REWRITE_TAC[e1_fan]
1312 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1313 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1314 THEN ONCE_REWRITE_TAC[DOT_SYM]
1315 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1316 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1317 THEN ASM_REWRITE_TAC[]
1318 THEN REDUCE_VECTOR_TAC
1320 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1321 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1322 THEN REWRITE_TAC[DOT_RZERO]
1323 THEN REAL_ARITH_TAC;(*7*)
1325 REWRITE_TAC[SIN_0;COS_0]
1326 THEN REDUCE_ARITH_TAC
1327 THEN REDUCE_VECTOR_TAC
1328 THEN VECTOR_ARITH_TAC](*7*)](*6*);(*5*)
1331 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
1333 THEN POP_ASSUM MATCH_MP_TAC
1334 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1335 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1336 THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
1337 THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
1338 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
1339 THEN REDUCE_ARITH_TAC
1340 THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*5*)](*4*)](*3*);(*2*)
1349 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1350 THEN MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]one_edge_fan)
1352 THEN REWRITE_TAC[DIFF;IN_ELIM_THM]
1354 THEN POP_ASSUM MP_TAC
1355 THEN DISCH_THEN(LABEL_TAC"A")
1356 THEN EXISTS_TAC`vector[(dist((x:real^3),(x':real^3)));(azim (x:real^3) (v:real^3) (u:real^3) (x':real^3));(arcV (x:real^3) (x':real^3) (v:real^3))]:real^3`
1357 THEN ASM_REWRITE_TAC[VECTOR_3;AZIM_REFL;REAL_ARITH`A> &0 <=> &0 <A`]
1358 THEN SUBGOAL_THEN `~((x:real^3)=(x':real^3))` ASSUME_TAC
1362 THEN REMOVE_THEN "A" MP_TAC
1363 THEN ASM_REWRITE_TAC[DIST_REFL;VECTOR_ARITH`A-A= vec 0`;DOT_LZERO]
1364 THEN REDUCE_ARITH_TAC
1365 THEN REAL_ARITH_TAC;(*3*)
1367 MP_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_EQ_0)
1369 THEN ASSUME_TAC(ISPECL[`x:real^3`;`x':real^3`]DIST_POS_LE)
1370 THEN MP_TAC(REAL_ARITH`~(dist((x:real^3),(x':real^3))= &0)/\ &0 <= dist((x:real^3),(x':real^3))==> &0 < dist((x:real^3),(x':real^3))`)
1372 THEN ASM_REWRITE_TAC[azim]
1373 THEN SUBGOAL_THEN`~collinear{(x:real^3),(v:real^3),(x':real^3)}` ASSUME_TAC
1376 POP_ASSUM (fun th-> REWRITE_TAC[])
1377 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1378 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1379 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1380 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
1381 THEN POP_ASSUM MP_TAC
1382 THEN DISCH_THEN(LABEL_TAC"MA")
1383 THEN ONCE_REWRITE_TAC[lem1]
1384 THEN ASM_REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA;VECTOR_ARITH`v-x=vec 0<=> v=x`]
1385 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]AFF_GE_2_1)
1390 REMOVE_THEN "MA" MP_TAC
1391 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1395 THEN REDUCE_ARITH_TAC
1396 THEN REDUCE_VECTOR_TAC
1397 THEN REAL_ARITH_TAC;(*5*)
1399 REMOVE_THEN "MA" MP_TAC
1400 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1401 THEN EXISTS_TAC`&1- (c:real)`
1402 THEN EXISTS_TAC`c:real`
1404 THEN REDUCE_ARITH_TAC
1405 THEN REDUCE_VECTOR_TAC
1406 THEN ASM_REWRITE_TAC[VECTOR_ARITH`(x':real^3)=(&1 - (c:real)) % (x:real^3)+ c % (v:real^3)<=>x'-x=c%(v-x)`]
1407 THEN REAL_ARITH_TAC](*5*);(*4*)
1416 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]AZIM_EQ_0_GE_ALT)
1417 THEN ASM_REWRITE_TAC[]
1418 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x':real^3`]azim)
1419 THEN REAL_ARITH_TAC;(*6*)
1425 REWRITE_TAC[ARCV_ANGLE; angle;]
1426 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]VECTOR_ANGLE_RANGE)
1428 THEN MP_TAC(ISPECL[`((x':real^3) - (x:real^3)) `;`((v:real^3) - (x:real^3))`]COLLINEAR_VECTOR_ANGLE)
1429 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-B= vec 0<=> B=A`;]
1430 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
1431 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
1433 THEN FIND_ASSUM MP_TAC `~collinear {(x:real^3),(v:real^3),(x':real^3)}`
1434 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1435 THEN REWRITE_TAC[DE_MORGAN_THM]
1436 THEN REPEAT(POP_ASSUM MP_TAC)
1437 THEN REAL_ARITH_TAC;(*7*)
1439 MP_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_EQ_0)
1441 THEN ASSUME_TAC(ISPECL[`v:real^3`;`x:real^3`]DIST_POS_LE)
1442 THEN MP_TAC(REAL_ARITH`~(dist((v:real^3),(x:real^3))= &0)/\ &0 <= dist((v:real^3),(x:real^3))==> &0 < dist((v:real^3),(x:real^3))`)
1444 THEN MP_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_EQ_0)
1446 THEN ASSUME_TAC(ISPECL[`x':real^3`;`x:real^3`]DIST_POS_LE)
1447 THEN MP_TAC(REAL_ARITH`~(dist((x':real^3),(x:real^3))= &0)/\ &0 <= dist((x':real^3),(x:real^3))==> &0 < dist((x':real^3),(x:real^3))`)
1449 THEN MP_TAC(ISPECL[`dist ((v:real^3),(x:real^3)) * cos (h:real)`;`((x':real^3) - x) dot ((v:real^3) - (x:real^3))`; `dist((x':real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1451 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3)) )/ dist ((x':real^3),(x:real^3)) `; `dist((v:real^3),(x:real^3))`]REAL_LT_RDIV_EQ)
1452 THEN ASM_REWRITE_TAC[]
1453 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
1454 THEN ASM_REWRITE_TAC[]
1455 THEN ONCE_REWRITE_TAC[REAL_ARITH`(A*B)*C =C* A*B`]
1456 THEN REWRITE_TAC[REAL_ARITH`A<B <=> B>A`;]
1457 THEN ASM_REWRITE_TAC[real_div;REAL_ARITH`(A*B)*C =A*(B *C)`]
1458 THEN ONCE_REWRITE_TAC[GSYM REAL_INV_MUL;]
1459 THEN ONCE_REWRITE_TAC[GSYM real_div;]
1460 THEN REWRITE_TAC[dist;arcV]
1462 THEN MP_TAC(REAL_ARITH`&0 < (h:real) /\ h< pi/ &2==> &0<= h /\ h<=pi`)
1464 THEN MP_TAC(ISPEC`h:real`ACS_COS)
1466 THEN MP_TAC(ISPECL[`cos (h:real)`;`(((x':real^3) - x) dot ((v:real^3) - (x:real^3))) / (norm (x' - x) * norm (v - x))` ;]ACS_MONO_LT)
1468 THEN REWRITE_TAC[REAL_ARITH`A>B<=> B<A`]
1469 THEN POP_ASSUM MATCH_MP_TAC
1470 THEN REWRITE_TAC[COS_BOUNDS]
1471 THEN ASM_REWRITE_TAC[REAL_ARITH`A<B<=> B>A`]
1472 THEN MP_TAC(ISPECL[`(x':real^3)-(x:real^3)`;`(v:real^3)-(x:real^3)`]NORM_CAUCHY_SCHWARZ_DIV)
1473 THEN MP_TAC(ISPEC`(((x':real^3)-(x:real^3)) dot ((v:real^3)-(x:real^3))) / (norm (x' - x) * norm (v - x))`REAL_ABS_LE)
1474 THEN REAL_ARITH_TAC](*7*)](*6*);(*5*)
1476 MATCH_MP_TAC(ISPECL[`u:real^3`;`x:real^3`;`v:real^3`;`x':real^3`;`e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1477 `e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`dist((x:real^3),(x':real^3))`;`arcV (x:real^3) (x':real^3) (v:real^3)`;`azim (x:real^3) (v:real^3) (u:real^3) (x':real^3)`]SPHERICAL_COORDINATES)
1478 THEN ASM_REWRITE_TAC[]
1479 THEN SUBGOAL_THEN`azim x v u (x+e1_fan (x:real^3) (v:real^3) (u:real^3))= &0` ASSUME_TAC
1482 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`;
1483 `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1485 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;`&1`;
1486 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`&0`]AZIM_UNIQUE)
1488 THEN POP_ASSUM MATCH_MP_TAC
1489 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;REAL_ARITH`&0<= &0/\ &0 < &1`]
1493 THEN REAL_ARITH_TAC;(*7*)
1498 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1499 THEN REDUCE_ARITH_TAC
1500 THEN REDUCE_VECTOR_TAC
1501 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1502 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1503 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1504 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1505 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1506 THEN REDUCE_ARITH_TAC
1507 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1508 THEN REDUCE_VECTOR_TAC
1509 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1511 THEN ASM_REWRITE_TAC[]
1512 THEN REWRITE_TAC[e1_fan]
1513 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1514 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1515 THEN ONCE_REWRITE_TAC[DOT_SYM]
1516 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1517 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1518 THEN ASM_REWRITE_TAC[]
1519 THEN REDUCE_VECTOR_TAC
1521 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1522 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1523 THEN REWRITE_TAC[DOT_RZERO]
1524 THEN REAL_ARITH_TAC;(*8*)
1526 REWRITE_TAC[SIN_0;COS_0]
1527 THEN REDUCE_ARITH_TAC
1528 THEN REDUCE_VECTOR_TAC
1529 THEN VECTOR_ARITH_TAC](*8*)](*7*);(*6*)
1532 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`x + e1_fan (x:real^3) (v:real^3) (u:real^3)`]AZIM_EQ_0_ALT)
1534 THEN POP_ASSUM MATCH_MP_TAC
1535 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
1536 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1537 THEN REWRITE_TAC[ VECTOR_ARITH`((A:real^3)+(B:real^3))-A=B`;]
1538 THEN ONCE_REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL]
1539 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2= &0`;REAL_ARITH `A=B:real <=> B=A`]
1540 THEN REDUCE_ARITH_TAC
1541 THEN ASM_REWRITE_TAC[DOT_EQ_0;VECTOR_ARITH`A-B=vec 0<=> A=B:real^3`]](*6*)](*5*)](*4*)](*3*)](*2*)](*1*))));;
1546 let connected_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 h:real.
1547 FAN(x,V,E)/\ {v,u} IN E/\ &0 <h /\ h< pi/ &2
1548 ==>connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h)))`,
1550 THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool) `;`v:real^3`;
1551 ` u:real^3` ;`h:real`]rw_dart_is_image_set_spherical_coordinate)
1553 THEN ASM_REWRITE_TAC[]
1554 THEN ASSUME_TAC(ISPECL[`(azim (x:real^3) (v:real^3) (u:real^3) u)`; `(azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) `;`h:real`] r_is_connected_fan)
1555 THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`]CONTINUOUS_ON_EQ_CONTINUOUS_AT)
1557 THEN MP_TAC(ISPECL[`change_spherical_coordinate_fan (x:real^3) (v:real^3) (u:real^3)`;`r_fan (azim x v u u) (azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) (h:real)`] CONNECTED_CONTINUOUS_IMAGE)
1559 THEN POP_ASSUM MATCH_MP_TAC
1562 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;
1563 `u:real^3`;`x':real^3`]continuous_change_spherical_coordinate_fan)
1564 THEN REWRITE_TAC[change_spherical_coordinate_fan]
1565 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1567 THEN MATCH_MP_TAC CONTINUOUS_ADD
1568 THEN ASM_REWRITE_TAC[]
1569 THEN SIMP_TAC[CONTINUOUS_CONST]);;
1572 let not_empty_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1573 FAN(x,V,E)/\ {v,u} IN E
1575 (!h:real. &0<h /\ h< pi/ &2
1577 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={}))`,
1579 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1580 THEN MRESA_TAC rw_dart_is_image_set_spherical_coordinate[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`h:real`]
1581 THEN POP_ASSUM MP_TAC
1582 THEN REWRITE_TAC[IMAGE_EQ_EMPTY;r_fan;EXTENSION;IN_ELIM_THM;IN;EMPTY;NOT_FORALL_THM;AZIM_REFL;azim_fan]
1583 THEN DISJ_CASES_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) V E) > 1)\/ CARD (set_of_edge v V E) > 1`)
1586 THEN EXISTS_TAC`vector[&1; pi; h/ &2]:real^3`
1587 THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1588 THEN MP_TAC PI_WORKS
1590 THEN REAL_ARITH_TAC;
1593 THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge v V E = {u:real^3})\/ ~(set_of_edge v V E = {u})`)
1595 MRESA_TAC CARD_SING[`u:real^3`; `(set_of_edge v V E):real^3->bool`]
1596 THEN FIND_ASSUM MP_TAC `CARD ((set_of_edge v V E):real^3->bool) >1`
1597 THEN POP_ASSUM MP_TAC
1598 THEN POP_ASSUM (fun TH-> REWRITE_TAC[TH])
1601 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = &0)`)
1603 MRESA_TAC SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(v:real^3)`;`(u:real^3)`]
1604 THEN MRESA_TAC UNIQUE_AZIM_0_POINT_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`]
1605 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`v:real^3`];
1607 MRESA_TAC azim[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`]
1608 THEN EXISTS_TAC`vector[&1; (azim x v u ((sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))))/ &2;h/ &2]:real^3`
1609 THEN SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]
1611 THEN REAL_ARITH_TAC]]]);;
1615 let JGIYDLE=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1616 FAN(x,V,E)/\ {v,u} IN E
1618 (!h:real. &0<h /\ h< pi/ &2
1620 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))={}))
1621 /\(!h:real h1:real. h1 <= h
1623 (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h SUBSET rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h1))
1629 rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) h SUBSET yfan(x,V,E))
1631 (!h:real. &0 <h /\ h< pi/ &2
1632 ==> connected(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(h))))`,
1633 MESON_TAC[not_empty_rw_dart_fan;continuous_set_fan;rw_dart_avoids_fan;connected_rw_dart_fan]);;