2 (* ========================================================================== *)
3 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Hoang Le Truong *)
8 (* ========================================================================== *)
13 module Jutstkg = struct
19 open Hypermap_of_fan;;
23 open Hypermap_of_fan;;
31 open Fully_surrounded;;
32 open Sin_azim_cross_dot;;
35 open Dartset_leads_into;;
43 let exists_point_notx_in_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
45 ==> ?v. v IN xfan(x,V,E) /\ ~(v=x)`,
47 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
48 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
51 THEN DISCH_THEN (LABEL_TAC"YEU")
52 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(y:real^3->bool)`]
53 THEN REMOVE_THEN "YEU" MP_TAC
55 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
56 THEN MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w:real^3)`]
57 THEN EXISTS_TAC `v:real^3`
58 THEN ASM_REWRITE_TAC[]
59 THEN EXISTS_TAC `y:real^3->bool`
60 THEN ASM_REWRITE_TAC[]
61 THEN ASM_TAC THEN SET_TAC[]);;
65 let x_in_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
67 ==> x IN xfan(x,V,E)`,
69 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
70 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
72 THEN EXISTS_TAC `y:real^3->bool`
74 THEN DISCH_THEN (LABEL_TAC"YEU")
75 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(y:real^3->bool)`]
76 THEN REMOVE_THEN "YEU" MP_TAC
78 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
79 THEN MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w:real^3)`]
80 THEN ASM_TAC THEN SET_TAC[]);;
84 let xfan_notempty_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
86 ==> ~(xfan(x,V,E)={})`,
88 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
89 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
90 THEN EXISTS_TAC `x:real^3`
92 THEN SET_TAC[x_in_xfan]);;
101 let xfan_closed_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
103 ==> closed (xfan(x,V,E))`,
106 THEN REWRITE_TAC[xfan;SET_RULE`{v | ?e. E e /\ v IN aff_ge {x} e}= UNIONS{y | ?x'. x' IN E /\ y = aff_ge {x} x'}`]
107 THEN MATCH_MP_TAC CLOSED_UNIONS
108 THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
109 THEN MRESAL_TAC FINITE_IMAGE[`(\e:real^3->bool. aff_ge {x:real^3} e)`;`E:(real^3->bool)->bool`][IMAGE;IN_ELIM_THM]
110 THEN REPEAT STRIP_TAC
111 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN DISCH_TAC
112 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(x':real^3->bool)`]
113 THEN REMOVE_THEN "YEU"MP_TAC THEN RESA_TAC
114 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
115 THEN MRESA_TAC closed_aff_ge_1_2[`x:real^3`;`v:real^3`;`w:real^3`]);;
118 let topological_component_subset_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool.
119 U IN topological_component_yfan (x,V,E)
120 ==> U SUBSET yfan(x,V,E)`,
121 REWRITE_TAC[topological_component_yfan;IN_ELIM_THM;]
122 THEN REPEAT STRIP_TAC
123 THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_SUBSET]);;
133 let aff_gt_connect_bound_not_inter_edges_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 y:real^3 z:real^3.
134 FAN(x,V,E)/\ {v,u} IN E /\ DISJOINT {x} {y,z}
135 /\ (!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
137 aff_gt {x} {y,z} INTER aff_ge {x} {v,u}={}`,
139 REWRITE_TAC[SET_RULE`A={}<=> ~(?w. w IN A)`;INTER;IN_ELIM_THM]
140 THEN REPEAT STRIP_TAC
141 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
142 THEN REPEAT STRIP_TAC
143 THEN MRESA_TAC scale_in_edges_fan[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`]
144 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
146 THEN MP_TAC(REAL_ARITH`&0<a==> &0 <= a`) THEN RESA_TAC
147 THEN MRESA_TAC scale_aff_ge_fan[`x:real^3`;`v:real^3`;`u:real^3`]
148 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`w:real^3`;`a:real`][VECTOR_ARITH`(A+B-C)+C=A+B:real^3`])
149 THEN MRESA_TAC in_aff_gt_1_2[`x:real^3`;`y:real^3`;`z:real^3 `;`t:real`]
150 THEN REMOVE_THEN "YEU" (fun th-> MRESAL1_TAC th`t:real`[yfan])
151 THEN POP_ASSUM MP_TAC
152 THEN ASM_REWRITE_TAC[SET_RULE`~((&1 - t) % y + t % z IN (:real^3) DIFF xfan (x,V,E))<=>(&1 - t) % y + t % z IN xfan (x,V,E)`;xfan;IN_ELIM_THM]
153 THEN EXISTS_TAC`{v,u}:real^3->bool`
154 THEN ASM_REWRITE_TAC[]
155 THEN ASM_TAC THEN SET_TAC[IN]);;
164 let aff_gt_connect_bound_subset_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3 z:real^3.
165 FAN(x,V,E) /\ DISJOINT {x} {y,z}
166 /\ (!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
167 ==> aff_gt {x} {y,z} SUBSET yfan (x,V,E)`,
171 REWRITE_TAC[yfan;xfan;SET_RULE`aff_gt {x} {y, z} SUBSET
172 (:real^3) DIFF {v | ?e. E e /\ v IN aff_ge {x} e}
173 <=> (!e. e IN E ==> aff_gt {x} {y,z} INTER aff_ge {x} e={})`]
174 THEN REPEAT STRIP_TAC
175 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]
176 THEN MRESA_TAC aff_gt_connect_bound_not_inter_edges_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` w:real^3`;`y:real^3`;`z:real^3`]
177 THEN POP_ASSUM MATCH_MP_TAC
178 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM(th)] ));;
183 let exists_point_notxin_convex_in_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) z:real^3.
184 FAN(x,V,E) /\ ~(x=z) /\ ~(E={})
185 ==> ?v. v IN xfan(x,V,E) /\ ~(x IN convex hull{v,z})`,
187 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
188 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
190 THEN POP_ASSUM MP_TAC
191 THEN DISCH_THEN (LABEL_TAC"YEU")
192 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(y:real^3->bool)`]
193 THEN REMOVE_THEN "YEU" MP_TAC
195 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
196 THEN MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w:real^3)`]
197 THEN DISJ_CASES_TAC(SET_RULE`~(x IN convex hull{v,z:real^3})\/ (x IN convex hull{v,z})`)
199 EXISTS_TAC `v:real^3`
200 THEN ASM_REWRITE_TAC[]
201 THEN EXISTS_TAC `y:real^3->bool`
202 THEN ASM_REWRITE_TAC[]
203 THEN ASM_TAC THEN SET_TAC[];
204 EXISTS_TAC `w:real^3`
207 EXISTS_TAC `y:real^3->bool`
208 THEN ASM_REWRITE_TAC[]
209 THEN ASM_TAC THEN SET_TAC[];
210 MRESA1_TAC CONVEX_HULL_SUBSET_AFFINE_HULL`{v,z:real^3}`
211 THEN MP_TAC(SET_RULE`x IN convex hull {v, z:real^3}/\ convex hull {v, z} SUBSET affine hull {v, z}
212 ==> x IN affine hull {v, z}`)
215 THEN MRESA1_TAC CONVEX_HULL_SUBSET_AFFINE_HULL`{w,z:real^3}`
216 THEN MP_TAC(SET_RULE`x IN convex hull {w, z:real^3}/\ convex hull {w, z} SUBSET affine hull {w, z}
217 ==> x IN affine hull {w, z}`)
219 THEN MP_TAC(SET_RULE`~(x=z) /\ ~(x=v) /\ ~(x=w)==> DISJOINT {x:real^3} {v,z} /\ DISJOINT{x} {w,z}`) THEN RESA_TAC
220 THEN MRESAL_TAC sym_line_fan[`x:real^3`;`v:real^3`;`z:real^3`][aff]
221 THEN MRESAL_TAC sym_line_fan[`x:real^3`;`w:real^3`;`z:real^3`][aff]
222 THEN MRESA_TAC POINT_IN_LINE1[`x:real^3` ;`w:real^3`]
223 THEN POP_ASSUM MP_TAC
224 THEN REWRITE_TAC[aff]
225 THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th)])
226 THEN ASM_REWRITE_TAC[SYM aff]]]);;
230 let notempty_xfan_inter_segment_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) z:real^3 v:real^3.
231 FAN(x,V,E) /\ v IN xfan(x,V,E)
232 ==> ~(xfan(x,V,E) INTER segment[v,z] ={})`,
234 THEN POP_ASSUM MP_TAC
235 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;IN_ELIM_THM;INTER;segment]
236 THEN EXISTS_TAC`v:real^3`
237 THEN ASM_REWRITE_TAC[]
239 THEN REWRITE_TAC[REAL_ARITH`&1- &0= &1 /\ &0<= &0 /\ &0<= &1`]
240 THEN REDUCE_VECTOR_TAC);;
244 let xfan_inter_segment_closed_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) z:real^3 v:real^3.
245 FAN(x,V,E) ==> closed(xfan(x,V,E) INTER segment[v,z])`,
247 THEN MATCH_MP_TAC CLOSED_INTER
248 THEN POP_ASSUM MP_TAC
249 THEN REWRITE_TAC[CLOSED_SEGMENT;xfan_closed_fan]);;
253 let point_in_yfan_not_x_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool z:real^3.
254 FAN(x,V,E) /\ ~(E={})
255 /\ U IN topological_component_yfan (x,V,E)
259 THEN POP_ASSUM MP_TAC
260 THEN MRESA_TAC topological_component_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` U:real^3->bool`]
261 THEN MP_TAC(SET_RULE`U SUBSET yfan (x:real^3,V:real^3->bool,E)/\ z IN U ==> z IN yfan(x,V,E)`)
263 THEN MRESA_TAC x_in_xfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
264 THEN POP_ASSUM MP_TAC
265 THEN POP_ASSUM MP_TAC
266 THEN REWRITE_TAC[yfan]
270 let zpoint_in_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool z:real^3.
271 FAN(x,V,E) /\ ~(E={})
272 /\ U IN topological_component_yfan (x,V,E)
274 ==> z IN yfan(x,V,E)`,
276 THEN POP_ASSUM MP_TAC
277 THEN MRESA_TAC topological_component_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` U:real^3->bool`]
278 THEN MP_TAC(SET_RULE`U SUBSET yfan (x:real^3,V:real^3->bool,E)/\ z IN U ==> z IN yfan(x,V,E)`)
285 let connect_insidepoint_to_bound_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool z:real^3.
287 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
289 /\ U IN topological_component_yfan (x,V,E)
291 ==> ?y. ~(y=x)/\ y IN xfan(x,V,E) /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan(x,V,E))`,
293 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
294 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
295 THEN MRESA_TAC exists_point_notxin_convex_in_xfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` z:real^3`]
296 THEN EXISTS_TAC`closest_point (xfan (x:real^3,V:real^3->bool,E) INTER segment[v,z]) (z:real^3)`
297 THEN MRESA_TAC xfan_inter_segment_closed_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` z:real^3`;`v:real^3`]
298 THEN MRESA_TAC notempty_xfan_inter_segment_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` z:real^3`;`v:real^3`]
299 THEN MRESA_TAC CLOSEST_POINT_EXISTS[`xfan (x:real^3,V:real^3->bool,E) INTER segment[v,z]`;`(z:real^3)`]
300 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
301 THEN MP_TAC (SET_RULE`closest_point (xfan (x:real^3,V:real^3->bool,E) INTER segment [v,z:real^3]) z IN
302 xfan (x,V,E) INTER segment [v,z]==> closest_point (xfan (x,V,E) INTER segment [v,z]) z IN
303 xfan (x,V,E)/\ closest_point (xfan (x,V,E) INTER segment [v,z]) z IN segment [v,z]`)
305 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_TAC
306 THEN POP_ASSUM (fun th-> MP_TAC th THEN ASSUME_TAC(th))
307 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SEGMENT_CONVEX_HULL]
309 THEN MP_TAC(SET_RULE`closest_point (xfan (x:real^3,V:real^3->bool,E) INTER convex hull {v, z}) z IN
310 convex hull {v, z} /\ ~(x IN convex hull {v, z})==> ~(closest_point (xfan (x,V,E) INTER convex hull {v, z} ) z = x)`)
313 THENL[ASM_REWRITE_TAC[SEGMENT_CONVEX_HULL];
314 ABBREV_TAC`y1=closest_point (xfan (x:real^3,V:real^3->bool,E) INTER segment [v,z]) z`
315 THEN SUBGOAL_THEN`!t. &0< t /\ t< &1==>dist (z,(&1 - t) % y1 + t % z)<dist (z,y1:real^3)` ASSUME_TAC
316 THENL[ REPEAT STRIP_TAC
317 THEN REWRITE_TAC[dist;VECTOR_ARITH`z - ((&1 - t) % y1 + t % z)=(&1 - t)%(z-y1)`]
318 THEN MP_TAC(ISPEC`&1- t:real`REAL_ABS_REFL)
319 THEN REWRITE_TAC[REAL_ARITH`&0<= &1-t <=> t<= &1`;NORM_MUL]
320 THEN MP_TAC(REAL_ARITH`t< &1==> t<= &1`) THEN RESA_TAC
322 THEN MRESAL_TAC REAL_LT_RMUL[`&1-t:real`;`&1:real`;`norm (z - y1:real^3)`][REAL_ARITH`&1*A=A`;REAL_ARITH`&1-t< &1<=> &0< t`]
323 THEN POP_ASSUM MATCH_MP_TAC
324 THEN MATCH_MP_TAC(REAL_ARITH`&0<= A /\ ~(A= &0) ==> &0 < A`)
325 THEN REWRITE_TAC[NORM_POS_LE;NORM_EQ_0;VECTOR_ARITH`A-B= vec 0<=>A=B`]
327 THEN REMOVE_THEN "EM" MP_TAC
328 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
329 THEN MRESA_TAC topological_component_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`]
330 THEN MP_TAC(SET_RULE`z:real^3 IN U /\ U SUBSET yfan(x,V,E) ==> z IN yfan(x:real^3,V:real^3->bool,E)`)
331 THEN ASM_REWRITE_TAC[yfan]
333 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"NHIEU")
334 THEN REPEAT STRIP_TAC
335 THEN ASM_REWRITE_TAC[yfan;DIFF;IN_ELIM_THM;SET_RULE`(&1 - t) % y1 + t % z IN (:real^3)`]
337 THEN MP_TAC (REAL_ARITH`&0<t /\ t< &1==> &0<= t /\ t:real<= &1`) THEN RESA_TAC
338 THEN MRESA_TAC segment_in_segment[`v:real^3`;`z:real^3`;`y1:real^3`]
339 THEN POP_ASSUM (fun th-> MRESA1_TAC th`t:real`)
340 THEN MP_TAC(SET_RULE`(&1 - t) % y1 + t % z IN xfan (x:real^3,V:real^3->bool,E) /\ (&1 - t) % y1 + t % z IN segment [v,z]==> (&1 - t) % y1 + t % z IN xfan (x,V,E) INTER segment [v,z]`)
342 THEN REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th`(&1 - t) % y1 + t % z:real^3`)
343 THEN REMOVE_THEN "NHIEU"(fun th-> MRESA1_TAC th`t:real`)
344 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
352 let point_in_aff_gt_in_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3 z:real^3 w:real^3.
353 FAN(x,V,E) /\ DISJOINT {x} {y,z} /\ w IN aff_gt {x} {y,z}
354 /\ (!t. &0 < t /\ t < &1 ==> (&1 - t) % y + t % z IN yfan (x,V,E))
355 ==> w IN yfan(x,V,E)`,
357 THEN MRESA_TAC aff_gt_connect_bound_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`y:real^3`;`z:real^3`]
358 THEN ASM_TAC THEN SET_TAC[]);;
363 let segment_subset_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3 z:real^3 w:real^3.
364 FAN(x,V,E) /\ DISJOINT {x} {y,z} /\ z IN yfan(x,V,E) /\ w IN aff_gt {x} {y,z}
365 /\ (!t. &0 < t /\ t < &1 ==> (&1 - t) % y + t % z IN yfan (x,V,E))
366 ==> segment[w,z] SUBSET yfan(x,V,E)`,
368 REWRITE_TAC[segment;SUBSET;IN_ELIM_THM]
369 THEN REPEAT STRIP_TAC
370 THEN MRESA_TAC aff_gt_connect_bound_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`y:real^3`;`z:real^3`]
371 THEN MRESA_TAC segmentsubset_aff_gt[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`]
372 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real`)
373 THEN POP_ASSUM MP_TAC
374 THEN MP_TAC(REAL_ARITH`u<= &1==> u< &1\/ u= &1`)
377 ASM_TAC THEN SET_TAC[];
378 ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - &1) % w + &1 % z=z:real^3`]]);;
381 let exists_in_aff_gt_disjoint=prove(`!x:real^3 v:real^3 u:real^3.
382 DISJOINT {x} {v,u} ==> ?y:real^3. y IN aff_gt {x} {v, u}`,
384 THEN MRESAL_TAC AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
385 THEN EXISTS_TAC`&0 % x+ &1 / &2 % v+ &1/ &2 %u:real^3 `
387 THEN EXISTS_TAC`&1/ &2`
388 THEN EXISTS_TAC`&1/ &2`
389 THEN ASM_REWRITE_TAC[]
390 THEN REAL_ARITH_TAC);;
394 let aff_gt_subset_component_y_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3.
396 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
398 /\ U IN topological_component_yfan (x,V,E)
400 /\ DISJOINT {x} {y,z}
401 /\ (!t. &0 < t /\ t < &1 ==> (&1 - t) % y + t % z IN yfan (x,V,E))
402 ==> aff_gt {x} {y,z} SUBSET U`,
404 THEN MRESA_TAC expand_element_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`z:real^3`]
405 THEN MRESA_TAC exists_in_aff_gt_disjoint[`x:real^3`;`y:real^3`;`z:real^3`]
406 THEN MRESA_TAC CONVEX_AFF_GT[`{x:real^3}`;`{y,z:real^3}`]
407 THEN MRESA1_TAC CONVEX_CONNECTED`aff_gt {x:real^3} {y,z:real^3}`
408 THEN MRESA_TAC aff_gt_connect_bound_subset_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`y:real^3`;`z:real^3`]
409 THEN MRESA_TAC CONNECTED_COMPONENT_MAXIMAL[`yfan(x:real^3, (V:real^3->bool) ,E)`;`aff_gt {x:real^3} {y,z}`;`y':real^3`;]
410 THEN MATCH_MP_TAC(SET_RULE`aff_gt {x} {y, z} SUBSET connected_component (yfan (x,V,E)) y'/\ connected_component (yfan (x:real^3, (V:real^3->bool),E)) y'= connected_component (yfan (x,V,E)) z==> aff_gt {x} {y, z} SUBSET connected_component (yfan (x,V,E)) z`)
411 THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_EQ_EQ;]
412 THEN MRESA_TAC point_in_aff_gt_in_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`y:real^3`;`z:real^3`;`y':real^3`]
413 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
414 THEN MRESA_TAC zpoint_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`z:real^3`]
415 THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET [`segment [y',z:real^3]`;`yfan(x:real^3, (V:real^3->bool) ,E)`;`y':real^3`;`z:real^3`]
416 THEN POP_ASSUM MATCH_MP_TAC
417 THEN MRESA_TAC segment_subset_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`y:real^3`;`z:real^3`;`y':real^3`]
418 THEN REWRITE_TAC[SEGMENT_CONVEX_HULL]
419 THEN MRESA1_TAC CONVEX_CONVEX_HULL`{y',z:real^3}`
420 THEN MRESA1_TAC CONVEX_CONNECTED `convex hull {y', z:real^3}`
421 THEN MRESA1_TAC CONNECTED_IFF_CONNECTED_COMPONENT`convex hull {y', z:real^3}`
422 THEN POP_ASSUM(fun th-> MRESA_TAC th[`y':real^3`;`z:real^3`])
423 THEN POP_ASSUM MATCH_MP_TAC
424 THEN MRESAL_TAC expansion1_convex_fan[`y':real^3`;`z:real^3`;`&0`][REAL_ARITH`&0<= &0 /\ &0<= &1`;VECTOR_ARITH`(&1- &0)%v+ &0 % u=v`]
425 THEN MRESAL_TAC expansion1_convex_fan[`y':real^3`;`z:real^3`;`&1`][REAL_ARITH`&0<= &1 /\ &1 <= &1`;VECTOR_ARITH`(&1- &1)%v+ &1 % u=u`]);;
432 let exists_connect_point_in_xfanto_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool z:real^3.
434 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
436 /\ U IN topological_component_yfan (x,V,E)
438 ==> ?y. ~(y=x) /\ y IN xfan(x,V,E) /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN U)`,
441 THEN MRESA_TAC connect_insidepoint_to_bound_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`; `U:real^3->bool`;`z:real^3`]
442 THEN EXISTS_TAC `y:real^3`
443 THEN ASM_REWRITE_TAC[]
444 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
445 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
446 THEN MP_TAC(SET_RULE`~(x=z) /\ ~(y=x)==> DISJOINT {x} {y,z:real^3}`)
448 THEN MRESA_TAC aff_gt_subset_component_y_fan [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`]
449 THEN REPEAT STRIP_TAC
450 THEN MATCH_MP_TAC(SET_RULE`aff_gt {x:real^3} {y, z} SUBSET U /\ (&1 - t) % y + t % z IN aff_gt {x} {y, z}==> (&1 - t) % y + t % z IN U`)
451 THEN ASM_REWRITE_TAC[]
452 THEN MRESAL_TAC AFF_GT_1_2[`(x:real^3)` ;` (y:real^3)`;`(z:real^3) `;][IN_ELIM_THM]
454 THEN EXISTS_TAC `&1- t:real`
455 THEN EXISTS_TAC `t:real`
456 THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1- t<=> t< &1`;REAL_ARITH`&0 + &1 - t + t = &1`]
457 THEN VECTOR_ARITH_TAC);;
464 let aff_ge_1_1_subset_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3.
466 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
467 /\ y IN xfan(x,V,E) /\ ~(x=y)
468 ==> aff_ge {x} {y} SUBSET xfan(x,V,E)`,
470 REWRITE_TAC[xfan;IN_ELIM_THM;SUBSET]
471 THEN REPEAT STRIP_TAC
472 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]
473 THEN POP_ASSUM MP_TAC
474 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN]
476 THEN EXISTS_TAC`e:real^3->bool`
477 THEN ASM_REWRITE_TAC[]
478 THEN MRESA_TAC aff_ge_1_1_subset_aff_ge_fan[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`]
479 THEN POP_ASSUM MP_TAC
480 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(th))
481 THEN ASM_REWRITE_TAC[]
482 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
484 THEN POP_ASSUM MP_TAC
485 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
486 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN]THEN ASM_REWRITE_TAC[] THEN ASSUME_TAC(th))
488 THEN ASM_REWRITE_TAC[]
489 THEN ASM_TAC THEN SET_TAC[]);;
492 let point_in_yfan_and_point_in_xfan_indepent_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3.
494 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
496 /\ U IN topological_component_yfan (x,V,E)
499 /\ ~(y=x) /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
500 ==> ~collinear {x,y,z}`,
502 THEN POP_ASSUM MP_TAC
503 THEN POP_ASSUM MP_TAC
504 THEN DISCH_THEN(LABEL_TAC"EM")
505 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
506 THEN MRESA_TAC zpoint_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`z:real^3`]
507 THEN ASM_REWRITE_TAC[collinear_fan;SET_RULE`~(y=x)<=> ~(x=y)`]
509 THEN MRESA_TAC place_there_point_line_fan[`x:real^3`;`y:real^3`;`z:real^3`]
510 THEN MRESA_TAC aff_ge_1_1_subset_xfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`y:real^3`]
511 THEN MP_TAC(SET_RULE`(&1 - t) % y + t % z IN aff_ge {x:real^3} {y}/\ aff_ge {x} {y} SUBSET xfan (x,V:real^3->bool,E) ==> (&1 - t) % y + t % z IN xfan (x,V,E)`)
513 THEN REMOVE_THEN "EM"(fun th-> MRESA1_TAC th`t:real`)
514 THEN POP_ASSUM MP_TAC
515 THEN ASM_REWRITE_TAC[yfan]
516 THEN POP_ASSUM MP_TAC
526 let exists_edge_component_yfan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (y:real^3).
527 FAN(x,V,E) /\ (!v. v IN V==>CARD (set_of_edge v V E) >1) /\ v IN V
528 /\ ~(y IN set_of_edge v V E)
530 (?(w:real^3). (w IN (set_of_edge v V E)) /\
531 (!(w1:real^3). (w1 IN (set_of_edge v V E)) ==> azim1 x v y w <= azim1 x v y w1))`,
535 FINITE X /\ ~(X = {})
536 ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
537 MESON_TAC[INF_FINITE]) in
540 THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`]
541 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v':real^3`;`v:real^3`]
542 THEN MRESA_TAC FINITE_IMAGE [`azim1 (x:real^3) v y`;`(set_of_edge v (V:real^3->bool) (E:(real^3->bool)->bool))`]
543 THEN MP_TAC(SET_RULE`v' IN set_of_edge v V E==> ~(set_of_edge v (V:real^3->bool) (E:(real^3->bool)->bool)= {}) `)
545 THEN MRESA_TAC IMAGE_EQ_EMPTY[`azim1 (x:real^3) v y`;`(set_of_edge v (V:real^3->bool) (E:(real^3->bool)->bool))`]
546 THEN MRESA1_TAC lemma`IMAGE (azim1 (x:real^3) v y) (set_of_edge v (V:real^3->bool) (E:(real^3->bool)->bool))
548 THEN POP_ASSUM MP_TAC
549 THEN POP_ASSUM MP_TAC
550 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
551 THEN REPEAT STRIP_TAC
552 THEN EXISTS_TAC`x':real^3`
553 THEN ASM_REWRITE_TAC[]
554 THEN POP_ASSUM MP_TAC
555 THEN DISCH_THEN(LABEL_TAC"YEU")
556 THEN REPEAT STRIP_TAC
557 THEN SUBGOAL_THEN`(?x'. x' IN set_of_edge v V E /\ azim1 x v y w1 = azim1 x v y (x':real^3))`ASSUME_TAC
559 EXISTS_TAC`w1:real^3`
560 THEN ASM_REWRITE_TAC[];
561 REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th`azim1 x v y (w1:real^3)`)]));;
577 let not_azim_points_in_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3.
579 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
581 /\ U IN topological_component_yfan (x,V,E)
584 /\ y IN aff_ge {x} {u}
587 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
588 ==>(!(w1:real^3). (w1 IN (set_of_edge u V E)) ==> ~(azim x u z w1= &0))`,
591 THEN POP_ASSUM MP_TAC
592 THEN POP_ASSUM MP_TAC
593 THEN POP_ASSUM MP_TAC
594 THEN DISCH_THEN (LABEL_TAC"YEU")
596 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
598 THEN POP_ASSUM MP_TAC
600 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
601 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
602 THEN MRESA_TAC no_origin_aff_ge_is_aff_gt[`x:real^3`;`u:real^3`;`y:real^3`]
603 THEN MRESA_TAC in_aff_gt_eq_azim[`x:real^3`;`y:real^3`;`u:real^3`;`z:real^3`;`w1:real^3`]
604 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(SYM(th)))
605 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
606 THEN MRESA_TAC aff_ge_1_1_subset_aff_fan[`y:real^3`;`x:real^3`;`u:real^3`]
607 THEN MRESA_TAC permutes_4points_collinear1[`x:real^3`;`y:real^3`;`u:real^3`;`w1:real^3`]
608 THEN MRESA_TAC th3[`x:real^3`;`y:real^3`;`w1:real^3`]
610 THEN MRESA_TAC AZIM_EQ_0_GE[`x:real^3`;`y:real^3`;`z:real^3`;`w1:real^3`]
611 THEN MRESA_TAC aff_ge_2_1_is_exists_point_inaff_ge_1_2[`x:real^3`;`y:real^3`;`z:real^3`;`w1:real^3`]
612 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`x:real^3`;`u:real^3`;`w1:real^3`]
613 THEN MP_TAC(SET_RULE`y IN aff_ge {x} {u}/\ aff_ge {x} {u, w1} =
614 aff_gt {x} {u, w1} UNION aff_ge {x} {u} UNION aff_ge {x} {w1}==> y IN aff_ge {x} {u, w1:real^3}`)
615 THEN POP_ASSUM(fun th -> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
616 THEN ASM_REWRITE_TAC[]
618 THEN MRESA_TAC aff_ge1_subset_aff_ge[`x:real^3`;`u:real^3`;`w1:real^3`;`y:real^3`]
619 THEN MP_TAC(SET_RULE`(&1 - t) % y + t % z IN aff_ge {x} {y, w1}
620 /\ aff_ge {x} {y, w1:real^3} SUBSET aff_ge {x} {u, w1}==> (&1 - t) % y + t % z IN aff_ge {x} {u, w1}`)
622 THEN SUBGOAL_THEN`aff_ge {x} {u,w1} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
624 ASM_REWRITE_TAC[xfan; SUBSET;IN_ELIM_THM]
625 THEN REPEAT STRIP_TAC
626 THEN EXISTS_TAC`{u,w1:real^3}`
627 THEN ASM_REWRITE_TAC[]
628 THEN ASM_TAC THEN SET_TAC[IN];
629 MP_TAC(SET_RULE`(&1 - t) % y + t % z IN aff_ge {x:real^3} {u, w1}/\ aff_ge {x} {u, w1} SUBSET xfan (x,V:real^3->bool,E)
630 ==> (&1 - t) % y + t % z IN xfan (x,V,E)`)
632 THEN REMOVE_THEN "YEU"(fun th -> MRESA1_TAC th`t:real` )
633 THEN POP_ASSUM MP_TAC
634 THEN POP_ASSUM MP_TAC
635 THEN REWRITE_TAC[yfan]
639 let exists_edge_bounded_topological_component_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3.
641 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
643 /\ U IN topological_component_yfan (x,V,E)
646 /\ y IN aff_ge {x} {u}
649 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
650 ==> ?w. {u,w} IN E /\ z IN w_dart_fan x V E (x,u,w,sigma_fan x V E u w)`,
653 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
654 THEN MRESA_TAC zpoint_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`z:real^3`]
655 THEN MRESA_TAC v_subset_xfan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
656 THEN MRESA_TAC set_of_edge_subset_edges[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`]
657 THEN MP_TAC (SET_RULE`V SUBSET xfan (x,(V:real^3->bool),(E:(real^3->bool)->bool)) /\ set_of_edge u V E SUBSET V==> set_of_edge u V E SUBSET xfan (x,V,E)`)
659 THEN MP_TAC(SET_RULE` z IN yfan (x,(V:real^3->bool),(E:(real^3->bool)->bool)) /\ set_of_edge u V E SUBSET xfan (x,V,E)/\ yfan (x,V,E)= (:real^3) DIFF xfan (x,V,E)
660 ==> ~(z IN set_of_edge u V E)`)
661 THEN ASM_REWRITE_TAC[yfan]
663 THEN MRESA_TAC exists_edge_component_yfan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (u:real^3)`; `(z:real^3)`]
664 THEN POP_ASSUM MP_TAC
665 THEN DISCH_THEN(LABEL_TAC"YEU")
666 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`u:real^3`]
667 THEN POP_ASSUM MP_TAC
668 THEN ASM_REWRITE_TAC[]
670 THEN EXISTS_TAC`w:real^3`
671 THEN ASM_REWRITE_TAC[w_dart_fan]
672 THEN FIND_ASSUM MP_TAC(`(!v:real^3. v IN V==>CARD (set_of_edge v V E) >1)`)
674 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3` th))
675 THEN FIND_ASSUM MP_TAC(`(u:real^3) IN V`)
677 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
679 THEN ASM_REWRITE_TAC[wedge;IN_ELIM_THM]
680 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
681 THEN MRESA_TAC aff_ge_1_1_subset_aff_fan[`y:real^3`;`x:real^3`;`u:real^3`]
682 THEN MRESA_TAC permutes_4points_collinear[`x:real^3`;`y:real^3`;`u:real^3`;`z:real^3`]
683 THEN MRESA_TAC not_azim_points_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` U:real^3->bool`;`y:real^3`;`z:real^3`;`u:real^3`]
684 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
685 THEN MRESA_TAC azim[`x:real^3`;`u:real^3`;`w:real^3`;`z:real^3`]
686 THEN REMOVE_ASSUM_TAC
687 THEN MP_TAC(REAL_ARITH`&0<= azim x u w z ==> azim x u w z = &0 \/ &0< azim x u w (z:real^3)`)
689 THENL(*1*)[ MRESA_TAC AZIM_COMPL_EQ_0[`x:real^3`;`u:real^3`;`w:real^3`;`z:real^3`];(*1*)
690 ABBREV_TAC`w1=sigma_fan x V E u w:real^3`
691 THEN SUBGOAL_THEN`~(set_of_edge u V E = {w:real^3})`ASSUME_TAC
694 THEN FIND_ASSUM (MP_TAC)`CARD (set_of_edge (u:real^3) V E) > 1`
695 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
696 THEN SUBGOAL_THEN `FINITE {(w:real^3)}` ASSUME_TAC
697 THENL (*3*)[SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
698 IN_INSERT; NOT_IN_EMPTY];
699 MRESAL_TAC CARD_PSUBSET[`{}:real^3->bool`;`{w:real^3}`][SET_RULE`{} PSUBSET {w}`]
700 THEN MRESAL_TAC CARD_DELETE[`w:real^3`;`{w:real^3}`][SET_RULE`w IN {w}/\ {w} DELETE w= {}`]
701 THEN POP_ASSUM MP_TAC
702 THEN POP_ASSUM MP_TAC
703 THEN REWRITE_TAC[CARD_CLAUSES]
704 THEN ARITH_TAC];(*2*)
706 MRESA_TAC SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`w:real^3`]
707 THEN POP_ASSUM MP_TAC
708 THEN DISCH_THEN(LABEL_TAC"LINH")
709 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w1:real^3`;`u:real^3`]
710 THEN POP_ASSUM MP_TAC
712 THEN MRESA_TAC not_azim_points_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` U:real^3->bool`;`y:real^3`;`z:real^3`;`u:real^3`]
713 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w1:real^3`)
714 THEN REMOVE_THEN "YEU" (fun th-> MRESAL1_TAC th`w1:real^3`[azim1])
715 THEN MP_TAC(REAL_ARITH`&2 * pi - azim x u z w <= &2 * pi - azim x u z w1==> azim x u z (w1:real^3) <= azim x u z w`)
717 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`u:real^3`;`z:real^3`;`w1:real^3`;` w:real^3`]
718 THEN MP_TAC(REAL_ARITH` azim x u z w = azim x u z w1 + azim x u w1 w /\ &0<= azim x u z w1
719 ==> &2 * pi - azim x u z w <= &2 * pi - azim x u w1 (w:real^3)`)
720 THEN ASM_REWRITE_TAC[azim]
721 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(SYM(th)))
722 THEN POP_ASSUM MP_TAC
723 THEN DISCH_THEN(LABEL_TAC"BE")
724 THEN SUBGOAL_THEN`~(azim x u w1 (w:real^3)= &0)` ASSUME_TAC
726 THEN MRESA_TAC UNIQUE_AZIM_0_POINT_FAN[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(u:real^3)`;`(w1:real^3)`;`w:real^3`];
728 MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`z:real^3`;`w:real^3`]
729 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
731 THEN MP_TAC(REAL_ARITH`&2 * pi - azim x u z w <= &2 * pi - azim x u w1 w
732 ==> &2 * pi - azim x u z w < &2 * pi - azim x u w1 w \/ azim x u z w = azim x u w1 (w:real^3)`)
734 THEN REMOVE_THEN"BE" MP_TAC
735 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=B<=>A= &0`]]]]);;
741 let aff_gt_in_w_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3 w:real^3 y:real^3.
742 FAN(x,V,E) /\ {u,w} IN E
743 /\ y IN w_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(sigma_fan x V E u w:real^3))
745 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
746 ==> aff_gt {x} {u,y} SUBSET w_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(sigma_fan x V E u w:real^3)) `,
748 THEN POP_ASSUM MP_TAC
749 THEN POP_ASSUM MP_TAC
750 THEN POP_ASSUM MP_TAC
751 THEN DISCH_THEN(LABEL_TAC "CON")
752 THEN DISCH_THEN(LABEL_TAC "BE")
753 THEN DISCH_THEN(LABEL_TAC"EM")
754 THEN USE_THEN "BE" MP_TAC
755 THEN REWRITE_TAC[fan80]
757 THEN POP_ASSUM (fun th-> MRESA_TAC th [`u:real^3`;`w:real^3`]
758 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
759 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
761 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
763 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
764 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge u V E = {w} \/ ~(set_of_edge u V E = {w:real^3})`)
766 MRESA_TAC CARD_SING[`w:real^3`; `(set_of_edge u V E):real^3->bool`]
767 THEN POP_ASSUM MP_TAC
768 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
769 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
770 REMOVE_THEN "CON" MP_TAC
771 THEN ASM_REWRITE_TAC[SUBSET; w_dart_fan;wedge;IN_ELIM_THM;]
772 THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC
773 THEN MRESA_TAC aff_gt_inter_aff_gt [`(x:real^3)`;`(u:real^3)`;`(y:real^3)`]
774 THEN MP_TAC(SET_RULE`aff_gt {x} {u, y} = aff_gt {x, u} {y} INTER aff_gt {x, y} {u}
775 /\ x' IN aff_gt {x} {u, y:real^3} ==> x' IN aff_gt {x,u} {y}`) THEN RESA_TAC
776 THEN MRESA_TAC aff_gt_imp_not_collinear[`x:real^3`;`y:real^3`;`u:real^3`; `x':real^3`]
777 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`w:real^3`;`x':real^3`;`y:real^3`;]]);;
783 let condition_rw_dart_fan_inter_aff_gt_is_not_empty=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 z:real^3 h:real.
784 FAN(x,V,E)/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
785 /\ fan80(x,V,E) /\ ~collinear {x,v,z}
786 /\ {v,u} IN E /\ z IN w_dart_fan x V E (x,v,u,sigma_fan x V E v u)
789 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u ) (cos(h)) INTER aff_gt {x} {v,z}={})`,
792 THEN POP_ASSUM MP_TAC
793 THEN MRESA_TAC aff_gt_in_w_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`z:real^3`]
794 THEN MP_TAC(SET_RULE`aff_gt {x} {v, z} SUBSET w_dart_fan x V E (x,v,u,sigma_fan x V E v u) ==>
795 (w_dart_fan x V E (x,v,u,sigma_fan x V E v u) INTER
796 rcone_fan x v (cos h)) INTER
797 aff_gt {x} {v, z}= rcone_fan x v (cos h) INTER
798 aff_gt {x} {v, z:real^3}`)
800 THEN ASM_REWRITE_TAC[rw_dart_fan;SET_RULE`~(A={})<=> ?y. y IN A`]
801 THEN MRESA_TAC not_empty_rcone_fan_inter_aff_gt[`x:real^3`;`v:real^3`;`z:real^3`;`h:real`]
802 THEN POP_ASSUM MP_TAC
808 let exists_edge_rw_dart_fan_inter_aff_gt_not_empty_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3.
810 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
812 /\ U IN topological_component_yfan (x,V,E)
815 /\ y IN aff_ge {x} {u}
818 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
819 ==> ?w. {u,w} IN E /\
821 ==> ~((rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h)) INTER aff_gt {x} {u,z}={}))`,
824 THEN MRESA_TAC exists_edge_bounded_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`u:real^3`]
825 THEN EXISTS_TAC`w:real^3`
826 THEN ASM_REWRITE_TAC[]
827 THEN GEN_TAC THEN STRIP_TAC
828 THEN MATCH_MP_TAC condition_rw_dart_fan_inter_aff_gt_is_not_empty
829 THEN ASM_REWRITE_TAC[]
830 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`u:real^3`]
831 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
832 THEN MRESA_TAC aff_ge_1_1_subset_aff_fan[`y:real^3`;`x:real^3`;`u:real^3`]
833 THEN MRESA_TAC permutes_4points_collinear[`x:real^3`;`y:real^3`;`u:real^3`;`z:real^3`]);;
839 let exists_edge_rw_dart_fan_inter_topological_component_not_empty_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3.
841 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
843 /\ U IN topological_component_yfan (x,V,E)
846 /\ y IN aff_ge {x} {u}
849 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
852 /\(!h. &0<h /\ h<= pi
853 ==> ~((rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h)) INTER U={}))`,
856 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
857 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
858 THEN MP_TAC(SET_RULE`~(x=z) /\ ~(y=x)==> DISJOINT {x} {y,z:real^3}`)
860 THEN MRESA_TAC aff_gt_subset_component_y_fan [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`]
861 THEN MRESA_TAC exists_edge_rw_dart_fan_inter_aff_gt_not_empty_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`u:real^3`]
862 THEN POP_ASSUM MP_TAC
863 THEN DISCH_THEN(LABEL_TAC"YEU")
864 THEN EXISTS_TAC `w:real^3`
865 THEN ASM_REWRITE_TAC[]
866 THEN GEN_TAC THEN STRIP_TAC
867 THEN REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th`h:real`)
868 THEN MATCH_MP_TAC(SET_RULE`~(rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h) INTER aff_gt {x} {u, z} = {})
869 /\ aff_gt {x:real^3} {y, z} SUBSET U /\ aff_gt {x} {u, z} =aff_gt {x} {y, z}
870 ==> ~(rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h) INTER U = {})`)
871 THEN ASM_REWRITE_TAC[]
872 THEN MATCH_MP_TAC aff_gt_1_2_scale_fan
873 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`u:real^3`]
874 THEN MRESA_TAC aff_ge_1_1_subset_aff_fan[`y:real^3`;`x:real^3`;`u:real^3`]
875 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
876 THEN MRESA_TAC permutes_4points_collinear[`x:real^3`;`y:real^3`;`u:real^3`;`z:real^3`]
877 THEN ASM_REWRITE_TAC[]
878 THEN FIND_ASSUM MP_TAC `y IN aff_ge {x} {u:real^3}`
879 THEN FIND_ASSUM MP_TAC ` ~(x=u:real^3)`
880 THEN FIND_ASSUM MP_TAC ` ~(y=x:real^3)`
881 THEN REPEAT REMOVE_ASSUM_TAC
884 THEN MRESAL_TAC AFF_GE_1_1[`x:real^3`;`u:real^3`][IN_ELIM_THM]
886 THEN EXISTS_TAC`t2:real`
887 THEN ASM_REWRITE_TAC[VECTOR_ARITH` (t1 % x + t2 % u) - x= ((t1+t2)- &1) %x+ t2%(u-x)`;]
888 THEN POP_ASSUM MP_TAC
889 THEN POP_ASSUM MP_TAC
890 THEN MP_TAC(REAL_ARITH`&0<= t2==> t2= &0 \/ &0< t2`)
892 THEN REDUCE_ARITH_TAC
894 THEN ASM_REWRITE_TAC[]
895 THEN REDUCE_VECTOR_TAC
896 THEN ASM_REWRITE_TAC[]
897 THEN VECTOR_ARITH_TAC);;
904 let exists_dart_leads_into_edge_eq_topological_component_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3.
906 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
908 /\ U IN topological_component_yfan (x,V,E)
911 /\ y IN aff_ge {x} {u}
914 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan(x,V,E))
915 ==> ?w. {u,w} IN E /\ dart_leads_into x V E u w = U`,
918 THEN MRESA_TAC exists_edge_rw_dart_fan_inter_topological_component_not_empty_fan[`x:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`u:real^3`;]
919 THEN POP_ASSUM MP_TAC
920 THEN DISCH_THEN(LABEL_TAC"MA")
921 THEN MRESA_TAC not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;`w:real^3`]
922 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM")
923 THEN MRESA_TAC DART_LEADS_INTO[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
924 `u:real^3`;`w:real^3`;]
925 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
926 THEN MRESA_TAC rw_dart_avoids_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;`w:real^3`]
927 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"OI")
928 THEN MP_TAC(REAL_ARITH`&1> h' /\ h' > &0==> -- &1 < h' /\ h'< &1 /\ -- &1 <= h' /\ h'<= &1/\ &0 < h' /\ h' <= &1`) THEN RESA_TAC
929 THEN MRESA1_TAC ACS_BOUNDS_LT`h':real`
930 THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
931 THEN MRESA1_TAC COS_ACS `h':real`
932 THEN ABBREV_TAC`h1= min (h:real) (acs h')/ &2`
933 THEN MP_TAC(REAL_ARITH`h1= min (h:real) (acs h')/ &2 /\ &0<h /\ &0< acs h' /\ acs h'< pi/ &2==> &0< h1 /\ h1< h /\ h1<pi/ &2/\ h1< acs h' /\ acs h' <= pi /\ &0<= h1/\ h1<= pi`)
934 THEN ASM_REWRITE_TAC[PI_WORKS] THEN STRIP_TAC
935 THEN MRESAL_TAC COS_MONO_LT[`h1:real`;`acs h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
936 THEN MP_TAC(REAL_ARITH`h'< cos h1==> h'<= cos h1`) THEN RESA_TAC
937 THEN REMOVE_THEN "EM"(fun th-> MRESAL1_TAC th `h1:real`[SET_RULE`~(A={})<=> ?y. y IN A`])
938 THEN REMOVE_THEN "YEU"(fun th-> MRESA_TAC th [`h1:real`;`y':real^3`])
939 THEN EXISTS_TAC `w:real^3`
940 THEN ASM_REWRITE_TAC[]
941 THEN POP_ASSUM MP_TAC
942 THEN POP_ASSUM MP_TAC
943 THEN DISCH_THEN(LABEL_TAC "EM")
945 THEN REMOVE_THEN "EM" MP_TAC
946 THEN POP_ASSUM(fun th -> REWRITE_TAC[SYM(th);])
948 THEN MRESA_TAC expand_element_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`z:real^3`]
949 THEN REMOVE_THEN "MA"(fun th-> MRESA1_TAC th `h1:real`)
950 THEN MP_TAC(SET_RULE`rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h1) SUBSET
951 connected_component (yfan (x,V,E)) y'/\
952 ~(rw_dart_fan x V E (x,u,w,sigma_fan x V E u w) (cos h1) INTER
953 connected_component (yfan (x,V,E)) z =
956 ~( connected_component (yfan (x,V,E)) y' INTER
957 connected_component (yfan (x,V,E)) z =
959 THEN ASM_REWRITE_TAC[]
960 THEN REWRITE_TAC[CONNECTED_COMPONENT_OVERLAP]
968 let not_azim_points1_in_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3 w:real^3.
970 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
972 /\ U IN topological_component_yfan (x,V,E)
975 /\ y IN aff_gt {x} {u,w}
978 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
979 ==> ~(azim x y z w= &0)`,
982 THEN POP_ASSUM MP_TAC
983 THEN POP_ASSUM MP_TAC
984 THEN DISCH_THEN (LABEL_TAC"YEU")
985 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
987 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
988 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
989 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
990 THEN MRESA_TAC properties_of_collinear4_points_fan[`x:real^3`;`w:real^3`;`u:real^3`;`y:real^3`]
991 THEN POP_ASSUM MP_TAC
992 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;SET_RULE`{A,B}={B,A}`]
993 THEN ASM_REWRITE_TAC[]
994 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
996 THEN MRESA_TAC AZIM_EQ_0_GE[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`]
998 THEN MRESA_TAC th3[`x:real^3`;`y:real^3`;`w:real^3`]
999 THEN MRESA_TAC aff_ge_2_1_is_exists_point_inaff_ge_1_2[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`]
1000 THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`x:real^3`;`u:real^3`;`w:real^3`]
1001 THEN MP_TAC(SET_RULE`aff_ge {x} {u, w} =
1002 aff_gt {x} {u, w} UNION aff_ge {x} {u} UNION aff_ge {x} {w}
1003 /\ y IN aff_gt {x} {u,w}==> y IN aff_ge {x:real^3} {u,w}`)
1004 THEN POP_ASSUM(fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
1006 THEN MRESA_TAC aff_ge1_subset_aff_ge[`x:real^3`;`u:real^3`; `w:real^3`;`y:real^3`]
1007 THEN SUBGOAL_THEN`aff_ge {x} {u,w} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
1009 ASM_REWRITE_TAC[xfan; SUBSET;IN_ELIM_THM]
1010 THEN REPEAT STRIP_TAC
1011 THEN EXISTS_TAC`{u,w:real^3}`
1012 THEN ASM_REWRITE_TAC[]
1013 THEN ASM_TAC THEN SET_TAC[IN];
1014 MP_TAC(SET_RULE`(&1 - t) % y + t % z IN aff_ge {x:real^3} {y, w}/\ aff_ge {x} {y, w} SUBSET aff_ge {x} {u, w} /\aff_ge {x} {u, w} SUBSET xfan (x,V:real^3->bool,E)
1015 ==> (&1 - t) % y + t % z IN xfan (x,V,E)`)
1017 THEN REMOVE_THEN "YEU"(fun th -> MRESA1_TAC th`t:real` )
1018 THEN POP_ASSUM MP_TAC
1019 THEN POP_ASSUM MP_TAC
1020 THEN ASM_REWRITE_TAC[yfan]
1025 let not_azim_points2_in_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 u:real^3 w:real^3.
1027 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1029 /\ U IN topological_component_yfan (x,V,E)
1032 /\ y IN aff_gt {x} {u,w}
1033 /\ y IN xfan (x,V,E)
1035 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan (x,V,E))
1036 ==> ~(azim x y z u= &0)`,
1039 THEN POP_ASSUM MP_TAC
1041 THEN MATCH_MP_TAC not_azim_points1_in_yfan
1042 THEN EXISTS_TAC`V:real^3->bool`
1043 THEN EXISTS_TAC`E:(real^3->bool)->bool`
1044 THEN EXISTS_TAC`U:real^3->bool`
1045 THEN EXISTS_TAC`w:real^3`
1046 THEN ASM_REWRITE_TAC[]
1047 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1048 THEN ASM_REWRITE_TAC[]);;
1063 let exists_dart_leads_into_edge_eq_topological1_component_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool y:real^3 z:real^3 v:real^3 u:real^3 w:real^3.
1065 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1067 /\ U IN topological_component_yfan (x,V,E)
1069 /\ {v,u} IN E /\ {u,w} IN E
1070 /\ sigma_fan x V E u w = v
1071 /\ y IN aff_gt {x} {v,u}
1074 /\(!t. &0< t /\ t< &1==> (&1-t)%y+t%z IN yfan(x,V,E))
1075 /\ &0<((v-x) cross (y-x)) dot (z-x)
1077 ==> dart_leads_into x V E v u = U`,
1081 THEN MRESA_TAC connected_component_of_faces_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `w:real^3`]
1082 THEN FIND_ASSUM MP_TAC`fan80 (x:real^3,V,E)`
1083 THEN REWRITE_TAC[fan80]
1085 THEN POP_ASSUM (fun th-> MRESA_TAC th[`u:real^3`;`w:real^3`])
1086 THEN MRESA_TAC fan_run_in_small_is_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1087 THEN POP_ASSUM MP_TAC
1088 THEN DISCH_THEN (LABEL_TAC"HA")
1089 THEN MRESA_TAC not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;`w:real^3`]
1090 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM")
1091 THEN MRESA_TAC DART_LEADS_INTO[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1092 `u:real^3`;`w:real^3`;]
1093 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
1094 THEN MRESA_TAC rw_dart_avoids_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;`w:real^3`]
1095 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"OI")
1096 THEN MP_TAC(REAL_ARITH`&1> h'' /\ h'' > &0==> -- &1 < h'' /\ h''< &1 /\ -- &1 <= h'' /\ h''<= &1/\ &0 < h'' /\ h'' <= &1`) THEN RESA_TAC
1097 THEN MRESA1_TAC ACS_BOUNDS_LT`h'':real`
1098 THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h'':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
1099 THEN MRESA1_TAC COS_ACS `h'':real`
1100 THEN ABBREV_TAC`h1= min h (min (h':real) (acs h''))/ &2`
1101 THEN MP_TAC(REAL_ARITH`h1= min h (min (h':real) (acs h''))/ &2 /\ &0< h /\ &0<h' /\ &0< acs h'' /\ acs h''< pi/ &2==> &0< h1 /\ h1< h /\ h1<h' /\ h1<pi/ &2/\ h1< acs h'' /\ acs h'' <= pi /\ &0<= h1`)
1102 THEN ASM_REWRITE_TAC[PI_WORKS] THEN STRIP_TAC
1103 THEN MRESAL_TAC COS_MONO_LT[`h1:real`;`acs h'':real`][ACS_0;REAL_ARITH`-- &1 <= &0`]
1104 THEN MP_TAC(REAL_ARITH`h''< cos h1==> h''<= cos h1`) THEN RESA_TAC
1105 THEN REMOVE_THEN "EM"(fun th-> MRESAL1_TAC th `h1:real`[SET_RULE`~(A={})<=> ?y. y IN A`])
1106 THEN REMOVE_THEN "YEU"(fun th-> MRESA_TAC th [`h1:real`;`y':real^3`])
1107 THEN MRESA_TAC exists_rw_dart_inter_aff_gt1_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;` w:real^3`;`h1:real`]
1108 THEN POP_ASSUM MP_TAC
1109 THEN DISCH_THEN(LABEL_TAC"MA1")
1110 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
1112 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
1114 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
1115 THEN MRESA_TAC exists_open_not_collinear[`(x:real^3)` ;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` (v:real^3)`;`(u:real^3)`;`(w:real^3)`]
1116 THEN SUBGOAL_THEN`(!h. &0 < h /\ h < t1 / &2 ==> ~collinear {x, v, (&1 - h) % u + h % w:real^3})`ASSUME_TAC
1119 THEN DISCH_THEN(LABEL_TAC"CHANGE")
1120 THEN GEN_TAC THEN STRIP_TAC
1121 THEN REMOVE_THEN "CHANGE"(fun th-> MRESA1_TAC th`h'''':real`)
1122 THEN POP_ASSUM MATCH_MP_TAC
1123 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1124 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1125 THEN REAL_ARITH_TAC;
1126 MP_TAC(REAL_ARITH`&0< t1 /\ t1<= &1==> &0< t1/ &2 /\ t1/ &2 < &1`)
1128 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`; `u:real^3`;`v:real^3`;`w:real^3`]
1129 THEN POP_ASSUM MP_TAC
1130 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1131 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1132 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1134 THEN MRESA_TAC condition_4point_aff_gt_1_2inter_aff_gt_1_2[`x:real^3`;`y:real^3`;`z:real^3`;`v:real^3`;` u:real^3`;`w:real^3`;`t1/ &2:real`]
1135 THEN POP_ASSUM MP_TAC
1136 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1138 THEN POP_ASSUM MP_TAC
1139 THEN DISCH_THEN(LABEL_TAC"MA2")
1140 THEN ABBREV_TAC`t2=min h ( min h''' t) / &2:real`
1141 THEN MP_TAC(REAL_ARITH`t2=min h ( min h''' t) / &2:real /\ &0<h /\ &0<t /\ &0< h'''==> t2< h''' /\ t2< t /\ &0< t2/\ t2< h`)
1143 THEN REMOVE_THEN "MA1"(fun th-> MRESA1_TAC th `t2:real`)
1144 THEN POP_ASSUM MP_TAC
1145 THEN ASM_REWRITE_TAC[]
1146 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y1. y1 IN A`;INTER;IN_ELIM_THM]
1148 THEN REMOVE_THEN "MA2"(fun th-> MRESA1_TAC th `t2:real`)
1149 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
1150 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;` z:real^3`]
1151 THEN MP_TAC(SET_RULE`~(x=z) /\ ~(y=x)==> DISJOINT {x} {y,z:real^3}`)
1153 THEN MRESA_TAC aff_gt_subset_component_y_fan [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`]
1154 THEN MP_TAC(SET_RULE`~(aff_gt {x} {y, z} INTER aff_gt {x} {v, (&1 - t2) % u + t2 % w} = {})/\
1155 aff_gt {x} {y, z} SUBSET U==> ~(U INTER aff_gt {x:real^3} {v, (&1 - t2) % u + t2 % w} = {})`)
1156 THEN ASM_REWRITE_TAC[]
1157 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y2. y2 IN A`;INTER;IN_ELIM_THM]
1159 THEN MRESA_TAC expand_element_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y2:real^3`]
1160 THEN MRESA_TAC dart_leads_into_fan_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
1161 THEN MP_TAC(SET_RULE`y1 IN rw_dart_fan x V E (x,u,w,v) (cos h1)
1162 /\ rw_dart_fan x V E (x,u,w,v) (cos h1) SUBSET (dart_leads_into x V E u w)
1163 ==> y1 IN (dart_leads_into x V E u (w:real^3))`)
1165 THEN MRESA_TAC expand_element_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(dart_leads_into x V E u w):real^3->bool`;`y1:real^3`]
1166 THEN MRESA_TAC zpoint_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y2:real^3`]
1167 THEN MRESA_TAC zpoint_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(dart_leads_into x V E u w):real^3->bool`;`y1:real^3`]
1168 THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_EQ_EQ]
1169 THEN MRESA_TAC CONVEX_AFF_GT[`{x:real^3}`;`{v, (&1 - t2) % u + t2 % w:real^3}`]
1170 THEN MRESA_TAC CONVEX_CONNECTED[`aff_gt {x} {v, (&1 - t2) % u + t2 % w}:real^3->bool`]
1171 THEN POP_ASSUM MP_TAC
1172 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT]
1174 THEN POP_ASSUM (fun th-> MRESA_TAC th [`y1:real^3`;`y2:real^3`])
1175 THEN REMOVE_THEN "HA" (fun th-> MRESA1_TAC th `t2:real`)
1176 THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`aff_gt {x} {v, (&1 - t2) % u + t2 % w:real^3}:real^3-> bool`;`yfan (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):real^3->bool`;`y1:real^3`;`y2:real^3`]
1183 let JUTSTKG=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool.
1185 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1187 /\ U IN topological_component_yfan (x,V,E)
1188 ==> ?v u. {v,u} IN E /\ dart_leads_into x V E v u = U`,
1191 THEN MRESA_TAC exists_point_in_component_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)` ;`U:real^3->bool`]
1192 THEN MRESA_TAC connect_insidepoint_to_bound_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)` ;`U:real^3->bool`;`z:real^3`]
1193 THEN POP_ASSUM MP_TAC
1194 THEN POP_ASSUM (fun th-> MP_TAC th THEN ASSUME_TAC th)
1195 THEN REWRITE_TAC[xfan;IN_ELIM_THM]
1197 THEN POP_ASSUM MP_TAC
1198 THEN MRESA_TAC expand_edge_graph_fan [`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(e:real^3->bool)`]
1199 THEN POP_ASSUM MP_TAC
1200 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[IN]
1202 THEN SUBGOAL_THEN `{v,w:real^3} IN E`ASSUME_TAC
1203 THENL(*1*)[POP_ASSUM (fun th-> ASM_REWRITE_TAC[SYM(th);IN]);(*1*)
1204 MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
1206 THEN MRESAL_TAC aff_ge_eq_aff_gt_union_aff_ge[`x:real^3`;`v:real^3`;`w:real^3`][UNION;IN_ELIM_THM]
1210 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;` z:real^3`]
1211 THEN DISJ_CASES_TAC(REAL_ARITH`&0 < ((v - x) cross (y - x)) dot (z - x) \/ &0< --(((v - x) cross (y - x)) dot (z - x)) \/ ((v - x:real^3) cross (y - x)) dot (z - x)= &0`)
1213 MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
1214 THEN REMOVE_ASSUM_TAC
1215 THEN POP_ASSUM (fun th-> MRESA1_TAC th `v:real^3`)
1216 THEN POP_ASSUM MP_TAC
1217 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1218 THEN ASM_REWRITE_TAC[]
1219 THEN POP_ASSUM (fun th-> MRESA1_TAC th `v:real^3`)
1220 THEN POP_ASSUM MP_TAC
1221 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1222 THEN ASM_REWRITE_TAC[]
1225 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`v:real^3`;`w:real^3`;`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (w:real^3) (v:real^3)`]
1226 THEN POP_ASSUM MP_TAC
1227 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1229 THEN EXISTS_TAC`v:real^3`
1230 THEN EXISTS_TAC`w:real^3`
1231 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1232 THEN ASM_REWRITE_TAC[];(*3*)
1237 MRESA_TAC aff_gt_1_2_cross_dotr_4point_neg[`x:real^3`;`y:real^3`;`z:real^3`;`v:real^3`;`w:real^3`;]
1238 THEN POP_ASSUM MP_TAC
1239 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1241 THEN POP_ASSUM MP_TAC
1242 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1243 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1245 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`]
1246 THEN REMOVE_ASSUM_TAC
1247 THEN POP_ASSUM (fun th-> MRESA1_TAC th `w:real^3`)
1248 THEN POP_ASSUM MP_TAC
1249 THEN POP_ASSUM (fun th-> MRESA1_TAC th `w:real^3`)
1251 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`w:real^3`;`v:real^3`;`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`]
1252 THEN POP_ASSUM MP_TAC
1253 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1255 THEN EXISTS_TAC`w:real^3`
1256 THEN EXISTS_TAC`v:real^3`
1257 THEN ASM_REWRITE_TAC[]
1258 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1259 THEN ASM_REWRITE_TAC[];(*4*)
1261 MRESA_TAC aff_gt_1_2_cross_dotr_4point_zero[`x:real^3`;`y:real^3`;`z:real^3`;`v:real^3`;`w:real^3`;]
1262 THEN POP_ASSUM MP_TAC
1263 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1265 THEN POP_ASSUM MP_TAC
1266 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1267 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1269 THEN MRESA_TAC not_azim_points1_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`v:real^3`;`w:real^3`]
1270 THEN MRESA_TAC not_azim_points1_in_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`w:real^3`;`v:real^3`]
1271 THEN POP_ASSUM MP_TAC
1272 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1273 THEN ASM_REWRITE_TAC[]
1275 THEN MP_TAC(REAL_ARITH`~(azim x y z v = &0) /\ &0<= azim x y z v==> &0< azim x y z (v:real^3) `)
1276 THEN ASM_REWRITE_TAC[azim]
1278 THEN MRESA_TAC properties_of_collinear4_points_fan[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`]
1279 THEN MRESA_TAC properties_of_collinear4_points_fan[`x:real^3`;`w:real^3`;`v:real^3`;`y:real^3`]
1280 THEN POP_ASSUM MP_TAC
1281 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1282 THEN ASM_REWRITE_TAC[]
1283 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1285 THEN DISJ_CASES_TAC(REAL_ARITH`azim x y z (v:real^3)< pi \/ pi<= azim x y z (v:real^3)`)
1287 MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`y:real^3`; `v:real^3`;`z:real^3`]
1288 THEN POP_ASSUM MP_TAC
1289 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1290 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1292 THEN POP_ASSUM MP_TAC
1293 THEN REAL_ARITH_TAC;(*5*)
1296 THEN MRESA_TAC aff_gt2_subset_aff_ge [`x:real^3`;`w:real^3`; `v:real^3`;`y:real^3`]
1297 THEN POP_ASSUM MP_TAC
1298 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1299 THEN ASM_REWRITE_TAC[]
1301 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC th)
1303 THEN MRESA_TAC sum5_azim_fan[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`;`v:real^3`]
1304 THEN MP_TAC(REAL_ARITH`azim x y z v = azim x y z w + pi/\
1305 azim x y z v < &2 * pi/\ ~(azim x y z w = &0) /\ &0 <= azim x y z w
1306 ==> &0< azim x y z w /\ azim x y z w < pi
1308 THEN ASM_REWRITE_TAC[azim]
1310 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`y:real^3`; `w:real^3`;`z:real^3`]
1311 THEN POP_ASSUM MP_TAC
1312 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1313 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1315 THEN POP_ASSUM MP_TAC
1316 THEN REAL_ARITH_TAC](*5*)](*4*)](*3*);(*2*)
1320 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological_component_fan[`x:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`v:real^3`]
1321 THEN EXISTS_TAC `v:real^3`
1322 THEN EXISTS_TAC `w':real^3`
1323 THEN ASM_REWRITE_TAC[];
1325 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;
1327 THEN POP_ASSUM MP_TAC
1328 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1329 THEN ASM_REWRITE_TAC[]
1331 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological_component_fan[`x:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`y:real^3`;`z:real^3`;`w:real^3`]
1332 THEN EXISTS_TAC `w:real^3`
1333 THEN EXISTS_TAC `w':real^3`
1334 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1335 THEN ASM_REWRITE_TAC[]]]);;