legacy/oldfan/JUTSTKG.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 module  Jutstkg = struct
  14
  15
  16
  17 open Sphere;;
  18 open Fan_defs;;
  19 open Hypermap_of_fan;;
  20 open Tactic_fan;;
  21 open Lemma_fan;;
  22 open Fan;;
  23 open Hypermap_of_fan;;
  24 open Node_fan;;
  25 open Azim_node;;
  26 open Sum_azim_node;;
  27 open Disjoint_fan;;
  28 open Lead_fan;;
  29 open Fan_misc;;
  30 open Leads_into_fan;;
  31 open Fully_surrounded;;
  32 open Sin_azim_cross_dot;;
  33 open Leads_intos;;
  34 open Hypermap;;
  35 open Dartset_leads_into;;
  36
  37
  38
  39
  40
  41
  42
  43 let exists_point_notx_in_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
  44 FAN(x,V,E) /\ ~(E={})
  45 ==> ?v. v IN xfan(x,V,E) /\ ~(v=x)`,
  46 REPEAT STRIP_TAC
  47 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
  48 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
  49 THEN STRIP_TAC
  50 THEN POP_ASSUM MP_TAC
  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
  54 THEN RESA_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[]);;
  62
  63
  64
  65 let x_in_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
  66 FAN(x,V,E) /\ ~(E={})
  67 ==> x IN xfan(x,V,E)`,
  68 REPEAT STRIP_TAC
  69 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
  70 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
  71 THEN STRIP_TAC
  72 THEN EXISTS_TAC `y:real^3->bool`
  73 THEN POP_ASSUM MP_TAC
  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
  77 THEN RESA_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[]);;
  81
  82
  83
  84 let xfan_notempty_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
  85 FAN(x,V,E) /\ ~(E={})
  86 ==> ~(xfan(x,V,E)={})`,
  87 REPEAT STRIP_TAC
  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`
  91 THEN ASM_TAC
  92 THEN SET_TAC[x_in_xfan]);;
  93
  94
  95
  96
  97
  98
  99
 100
 101 let xfan_closed_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 102 FAN(x,V,E)
 103 ==> closed (xfan(x,V,E))`,
 104
 105 REPEAT STRIP_TAC
 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`]);;
 116
 117
 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]);;
 124
 125
 126
 127
 128
 129
 130
 131
 132
 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))
 136 ==>
 137 aff_gt {x} {y,z} INTER aff_ge {x} {v,u}={}`,
 138
 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)`;
 145 ` (v: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]);;
 156
 157
 158
 159
 160
 161
 162
 163
 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)`,
 168
 169 REPEAT STRIP_TAC
 170 THEN
 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)] ));;
 179
 180
 181
 182
 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})`,
 186 REPEAT STRIP_TAC
 187 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]
 188 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;xfan;IN_ELIM_THM]
 189 THEN STRIP_TAC
 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
 194 THEN RESA_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})`)
 198 THENL[
 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`
 205 THEN STRIP_TAC
 206 THENL[
 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}`)
 213 THEN RESA_TAC
 214 THEN STRIP_TAC
 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}`)
 218 THEN RESA_TAC
 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]]]);;
 227
 228
 229
 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] ={})`,
 233 REPEAT STRIP_TAC
 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[]
 238 THEN EXISTS_TAC`&0`
 239 THEN REWRITE_TAC[REAL_ARITH`&1- &0= &1 /\ &0<= &0 /\ &0<= &1`]
 240 THEN REDUCE_VECTOR_TAC);;
 241
 242
 243
 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])`,
 246 REPEAT STRIP_TAC
 247 THEN MATCH_MP_TAC CLOSED_INTER
 248 THEN POP_ASSUM MP_TAC
 249 THEN REWRITE_TAC[CLOSED_SEGMENT;xfan_closed_fan]);;
 250
 251
 252
 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)
 256 /\ z IN U
 257 ==> ~(x=z)`,
 258 REPEAT STRIP_TAC
 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)`)
 262 THEN RESA_TAC
 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]
 267 THEN SET_TAC[]);;
 268
 269
 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)
 273 /\ z IN U
 274 ==> z IN yfan(x,V,E)`,
 275 REPEAT STRIP_TAC
 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)`)
 279 THEN RESA_TAC
 280 THEN SET_TAC[]);;
 281
 282
 283
 284
 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.
 286 FAN(x,V,E)
 287 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 288 /\ fan80(x,V,E)
 289 /\ U IN topological_component_yfan (x,V,E)
 290 /\ z IN U
 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))`,
 292 REPEAT STRIP_TAC
 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]`)
 304 THEN RESA_TAC
 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]
 308 THEN STRIP_TAC
 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)`)
 311 THEN RESA_TAC
 312 THEN STRIP_TAC
 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
 321 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`]
 326 THEN STRIP_TAC
 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]
 332 THEN SET_TAC[];
 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)`]
 336 THEN STRIP_TAC
 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]`)
 341 THEN RESA_TAC
 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]]);;
 345
 346
 347
 348
 349
 350
 351
 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)`,
 356 REPEAT STRIP_TAC
 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[]);;
 359
 360
 361
 362
 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)`,
 367
 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`)
 375 THEN RESA_TAC
 376 THENL[
 377 ASM_TAC THEN SET_TAC[];
 378 ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - &1) % w + &1 % z=z:real^3`]]);;
 379
 380
 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}`,
 383 REPEAT STRIP_TAC
 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 `
 386 THEN EXISTS_TAC`&0`
 387 THEN EXISTS_TAC`&1/ &2`
 388 THEN EXISTS_TAC`&1/ &2`
 389 THEN ASM_REWRITE_TAC[]
 390 THEN REAL_ARITH_TAC);;
 391
 392
 393
 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.
 395 FAN(x,V,E)
 396 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 397 /\ fan80(x,V,E)
 398 /\ U IN topological_component_yfan (x,V,E)
 399 /\ z IN U
 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`,
 403 REPEAT STRIP_TAC
 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`]);;
 426
 427
 428
 429
 430
 431
 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.
 433 FAN(x,V,E)
 434 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 435 /\ fan80(x,V,E)
 436 /\ U IN topological_component_yfan (x,V,E)
 437 /\ z IN U
 438 ==> ?y. ~(y=x) /\ y IN xfan(x,V,E) /\(!t. &0< t /\ t< &1==>   (&1-t)%y+t%z IN U)`,
 439
 440 REPEAT STRIP_TAC
 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}`)
 447 THEN RESA_TAC
 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]
 453 THEN EXISTS_TAC`&0`
 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);;
 458
 459
 460
 461
 462
 463
 464 let aff_ge_1_1_subset_xfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y:real^3.
 465 FAN(x,V,E)
 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)`,
 469
 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]
 475 THEN RESA_TAC
 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)`;
 483 ` (v: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))
 487 THEN STRIP_TAC
 488 THEN ASM_REWRITE_TAC[]
 489 THEN ASM_TAC THEN SET_TAC[]);;
 490
 491
 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.
 493 FAN(x,V,E)
 494 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 495 /\ fan80(x,V,E)
 496 /\ U IN topological_component_yfan (x,V,E)
 497 /\ z IN U
 498 /\ y IN xfan(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}`,
 501 REPEAT STRIP_TAC
 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)`]
 508 THEN STRIP_TAC
 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)`)
 512 THEN RESA_TAC
 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
 517 THEN SET_TAC[]);;
 518
 519
 520
 521
 522 (*CASE 1*)
 523
 524
 525
 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)
 529 ==>
 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))`,
 532
 533 (let lemma = prove
 534    (`!X:real->bool.
 535           FINITE X /\ ~(X = {})
 536           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 537     MESON_TAC[INF_FINITE]) in
 538
 539 REPEAT STRIP_TAC
 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)= {}) `)
 544 THEN RESA_TAC
 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))
 547 `
 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
 558 THENL[
 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)`)]));;
 562
 563
 564
 565
 566
 567
 568
 569
 570
 571
 572
 573
 574
 575
 576
 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.
 578 FAN(x,V,E)
 579 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 580 /\ fan80(x,V,E)
 581 /\ U IN topological_component_yfan (x,V,E)
 582 /\ z IN U
 583 /\ u IN V
 584 /\ y IN aff_ge {x} {u}
 585 /\ y IN xfan (x,V,E)
 586 /\ ~(y=x)
 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))`,
 589
 590 REPEAT STRIP_TAC
 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")
 595 THEN DISCH_TAC
 596 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w1:real^3)`;
 597 ` (u:real^3)`]
 598 THEN POP_ASSUM MP_TAC
 599 THEN RESA_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`]
 609 THEN STRIP_TAC
 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[]
 617 THEN STRIP_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}`)
 621 THEN RESA_TAC
 622 THEN SUBGOAL_THEN`aff_ge {x} {u,w1} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
 623 THENL[
 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)`)
 631 THEN RESA_TAC
 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]
 636 THEN SET_TAC[]]);;
 637
 638
 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.
 640 FAN(x,V,E)
 641 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 642 /\ fan80(x,V,E)
 643 /\ U IN topological_component_yfan (x,V,E)
 644 /\ z IN U
 645 /\ u IN V
 646 /\ y IN aff_ge {x} {u}
 647 /\ y IN xfan(x,V,E)
 648 /\ ~(y=x)
 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)`,
 651
 652 REPEAT STRIP_TAC
 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)`)
 658 THEN RESA_TAC
 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]
 662 THEN STRIP_TAC
 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[]
 669 THEN STRIP_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)`)
 673 THEN DISCH_TAC
 674 THEN  POP_ASSUM(fun th->  MP_TAC(ISPEC`u:real^3` th))
 675 THEN FIND_ASSUM MP_TAC(`(u:real^3) IN V`)
 676 THEN DISCH_TAC
 677 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
 678 THEN STRIP_TAC
 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)`)
 688 THEN RESA_TAC
 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
 692 THENL(*2*)[
 693 STRIP_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*)
 705
 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
 711 THEN RESA_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`)
 716 THEN RESA_TAC
 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
 725 THENL[ STRIP_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`];
 727
 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`]
 730 THEN STRIP_TAC
 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)`)
 733 THEN RESA_TAC
 734 THEN REMOVE_THEN"BE" MP_TAC
 735 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=B<=>A= &0`]]]]);;
 736
 737
 738
 739
 740
 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))
 744 /\ fan80(x,V,E)
 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)) `,
 747 REPEAT STRIP_TAC
 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]
 756 THEN DISCH_TAC
 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)`;
 760 ` (v:real^3)`]
 761 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 762 ` (u: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})`)
 765 THENL[
 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`;]]);;
 778
 779
 780
 781
 782
 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)
 787 /\ &0<h /\ h<= pi
 788 ==>
 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}={})`,
 790
 791 REPEAT STRIP_TAC
 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}`)
 799 THEN RESA_TAC
 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
 803 THEN SET_TAC[]);;
 804
 805
 806
 807
 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.
 809 FAN(x,V,E)
 810 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 811 /\ fan80(x,V,E)
 812 /\ U IN topological_component_yfan (x,V,E)
 813 /\ z IN U
 814 /\ u IN V
 815 /\ y IN aff_ge {x} {u}
 816 /\ y IN xfan(x,V,E)
 817 /\ ~(y=x)
 818 /\(!t. &0< t /\ t< &1==>   (&1-t)%y+t%z IN yfan (x,V,E))
 819 ==> ?w. {u,w} IN E /\
 820 (!h. &0<h /\ h<= pi
 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}={}))`,
 822
 823 REPEAT STRIP_TAC
 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`]);;
 834
 835
 836
 837
 838
 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.
 840 FAN(x,V,E)
 841 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 842 /\ fan80(x,V,E)
 843 /\ U IN topological_component_yfan (x,V,E)
 844 /\ z IN U
 845 /\ u IN V
 846 /\ y IN aff_ge {x} {u}
 847 /\ y IN xfan(x,V,E)
 848 /\ ~(y=x)
 849 /\(!t. &0< t /\ t< &1==>   (&1-t)%y+t%z IN yfan (x,V,E))
 850
 851 ==> ?w. {u,w} IN 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={}))`,
 854
 855 REPEAT STRIP_TAC
 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}`)
 859 THEN RESA_TAC
 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
 882 THEN STRIP_TAC
 883 THEN STRIP_TAC
 884 THEN MRESAL_TAC AFF_GE_1_1[`x:real^3`;`u:real^3`][IN_ELIM_THM]
 885 THEN STRIP_TAC
 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`)
 891 THEN RESA_TAC
 892 THEN REDUCE_ARITH_TAC
 893 THEN STRIP_TAC
 894 THEN ASM_REWRITE_TAC[]
 895 THEN REDUCE_VECTOR_TAC
 896 THEN ASM_REWRITE_TAC[]
 897 THEN VECTOR_ARITH_TAC);;
 898
 899
 900
 901
 902
 903
 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.
 905 FAN(x,V,E)
 906 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 907 /\ fan80(x,V,E)
 908 /\ U IN topological_component_yfan (x,V,E)
 909 /\ z IN U
 910 /\ u IN V
 911 /\ y IN aff_ge {x} {u}
 912 /\ y IN xfan(x,V,E)
 913 /\ ~(y=x)
 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`,
 916
 917 REPEAT STRIP_TAC
 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")
 944 THEN DISCH_TAC
 945 THEN REMOVE_THEN "EM" MP_TAC
 946 THEN POP_ASSUM(fun th -> REWRITE_TAC[SYM(th);])
 947 THEN DISCH_TAC
 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 =
 954         {})
 955 ==>
 956 ~(   connected_component (yfan (x,V,E)) y' INTER
 957         connected_component (yfan (x,V,E)) z =
 958         {})`)
 959 THEN ASM_REWRITE_TAC[]
 960 THEN REWRITE_TAC[CONNECTED_COMPONENT_OVERLAP]
 961 THEN SET_TAC[]);;
 962
 963
 964 (*CASE 2*)
 965
 966
 967
 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.
 969 FAN(x,V,E)
 970 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 971 /\ fan80(x,V,E)
 972 /\ U IN topological_component_yfan (x,V,E)
 973 /\ z IN U
 974 /\ {u,w} IN E
 975 /\ y IN aff_gt {x} {u,w}
 976 /\ y IN xfan (x,V,E)
 977 /\ ~(y=x)
 978  /\(!t. &0< t /\ t< &1==>   (&1-t)%y+t%z IN yfan (x,V,E))
 979 ==>  ~(azim x y z w= &0)`,
 980
 981 REPEAT STRIP_TAC
 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)`;
 986 ` (u: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}`;]
 995 THEN STRIP_TAC
 996 THEN MRESA_TAC AZIM_EQ_0_GE[`x:real^3`;`y:real^3`;`z:real^3`;`w:real^3`]
 997 THEN STRIP_TAC
 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])
1005 THEN RESA_TAC
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
1008 THENL[
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)`)
1016 THEN RESA_TAC
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]
1021 THEN SET_TAC[]]);;
1022
1023
1024
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.
1026 FAN(x,V,E)
1027 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1028 /\ fan80(x,V,E)
1029 /\ U IN topological_component_yfan (x,V,E)
1030 /\ z IN U
1031 /\ {u,w} IN E
1032 /\ y IN aff_gt {x} {u,w}
1033 /\ y IN xfan (x,V,E)
1034 /\ ~(y=x)
1035  /\(!t. &0< t /\ t< &1==>   (&1-t)%y+t%z IN yfan (x,V,E))
1036 ==>  ~(azim x y z u= &0)`,
1037
1038 REPEAT STRIP_TAC
1039 THEN POP_ASSUM MP_TAC
1040 THEN REWRITE_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[]);;
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
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.
1064 FAN(x,V,E)
1065 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1066 /\ fan80(x,V,E)
1067 /\ U IN topological_component_yfan (x,V,E)
1068 /\ z IN U
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}
1072 /\ y IN xfan(x,V,E)
1073 /\ ~(y=x)
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)
1076
1077 ==> dart_leads_into x V E v u = U`,
1078
1079
1080 REPEAT STRIP_TAC
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]
1084 THEN STRIP_TAC
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)`;
1111 ` (u:real^3)`]
1112 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
1113 ` (v: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
1117 THENL[
1118 POP_ASSUM MP_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`)
1127 THEN RESA_TAC
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]
1133 THEN RESA_TAC
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)
1137 THEN RESA_TAC
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`)
1142 THEN RESA_TAC
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]
1147 THEN RESA_TAC
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}`)
1152 THEN RESA_TAC
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]
1158 THEN RESA_TAC
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))`)
1164 THEN RESA_TAC
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]
1173 THEN DISCH_TAC
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`]
1177 ]);;
1178
1179
1180
1181
1182
1183 let JUTSTKG=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) U:real^3->bool.
1184 FAN(x,V,E)
1185 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1186 /\ fan80(x,V,E)
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`,
1189
1190 REPEAT STRIP_TAC
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]
1196 THEN STRIP_TAC
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]
1201 THEN RESA_TAC
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)`;
1205 ` (v: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]
1207 THEN STRIP_TAC
1208 THENL(*2*)[
1209 STRIP_TAC
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`)
1212 THENL(*3*)[
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[]
1223 THEN STRIP_TAC
1224 THEN STRIP_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}`]
1228 THEN RESA_TAC
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*)
1233
1234 POP_ASSUM MP_TAC
1235 THEN STRIP_TAC
1236 THENL(*4*)[
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)
1240 THEN RESA_TAC
1241 THEN POP_ASSUM MP_TAC
1242 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1243 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1244 THEN RESA_TAC
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`)
1250 THEN STRIP_TAC
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}`]
1254 THEN RESA_TAC
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*)
1260
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)
1264 THEN RESA_TAC
1265 THEN POP_ASSUM MP_TAC
1266 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1267 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1268 THEN RESA_TAC
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[]
1274 THEN STRIP_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]
1277 THEN STRIP_TAC
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}`]
1284 THEN STRIP_TAC
1285 THEN DISJ_CASES_TAC(REAL_ARITH`azim x y z (v:real^3)< pi \/ pi<= azim x y z (v:real^3)`)
1286 THENL(*5*)[
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]
1291 THEN RESA_TAC
1292 THEN POP_ASSUM MP_TAC
1293 THEN REAL_ARITH_TAC;(*5*)
1294
1295 POP_ASSUM MP_TAC
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[]
1300 THEN STRIP_TAC
1301 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC th)
1302 THEN STRIP_TAC
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
1307 `)
1308 THEN ASM_REWRITE_TAC[azim]
1309 THEN STRIP_TAC
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]
1314 THEN RESA_TAC
1315 THEN POP_ASSUM MP_TAC
1316 THEN REAL_ARITH_TAC](*5*)](*4*)](*3*);(*2*)
1317
1318
1319 STRIP_TAC
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[];
1324 STRIP_TAC
1325 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;
1326 ` (w:real^3)`]
1327 THEN POP_ASSUM MP_TAC
1328 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1329 THEN ASM_REWRITE_TAC[]
1330 THEN STRIP_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[]]]);;
1336
1337
1338
1339
1340 end;;
1341
1342