legacy/oldfan/introduction1.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2010-02-09                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10
  11 (*flyspeck_needs "general/sphere.hl";;*)
  12
  13
  14 module Fan  = struct
  15
  16
  17 (*
  18 # use "/home/truong/Desktop/googlecode/hol_light/hol.ml";;
  19 needs "/home/truong/Desktop/googlecode/hol_light/Multivariate/flyspeck.ml";;
  20 needs "/home/truong/Desktop/googlecode/flyspeck/text_formalization/general/sphere.hl";;
  21 *)
  22
  23
  24 open Sphere;;
  25 open Fan_defs;;
  26 open Tactic_fan;;
  27 open Lemma_fan;;
  28 open Hypermap;;
  29
  30
  31 (* ========================================================================== *)
  32 (*                                FAN                       *)
  33 (* ========================================================================== *)
  34
  35
  36
  37 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
  38
  39 let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
  40
  41 let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
  42
  43 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
  44
  45 let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
  46
  47 let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
  48
  49 let fan = new_definition`fan(x,V,E)<=>  ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;;
  50
  51 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
  52
  53 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
  54
  55
  56 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
  57
  58 let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  59 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
  60
  61
  62
  63 let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
  64 fan6(x,V,E)/\ fan7(x,V,E)`;;
  65
  66
  67
  68 (* ========================================================================== *)
  69 (*                            Invariance theorems                  *)
  70 (* ========================================================================== *)
  71
  72
  73
  74 let GRAPH = prove
  75  (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
  76   REWRITE_TAC[graph; IN]);;
  77
  78 let CYCLIC_SET = prove
  79  (`cyclic_set W v w <=>
  80          ~(v = w) /\
  81          FINITE W /\
  82          (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\
  83          W INTER affine hull {v, w} = {}`,
  84   REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
  85
  86 let CYCLIC_SET_TRANSLATION_EQ = prove
  87  (`!a:real^N s x y.
  88     cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
  89   REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
  90
  91 let CYCLIC_SET_LINEAR_IMAGE = prove
  92  (`!f:real^M->real^N s x y.
  93         linear f /\ (!x y. f x = f y ==> x = y)
  94         ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
  95   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
  96    [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN
  97   GEOM_TRANSFORM_TAC[]);;
  98
  99 add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;
 100
 101 add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
 102
 103 let GRAPH_TRANSLATION_EQ = prove
 104  (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
 105   REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
 106
 107 let GRAPH_LINEAR_IMAGE_EQ = prove
 108  (`!f:real^M->real^N E.
 109     linear f /\ (!x y. f x = f y ==> x = y)
 110     ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
 111   REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
 112
 113 let FAN1_TRANSLATION_EQ = prove
 114  (`!a:real^N x V E.
 115         fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 116         fan1(x,V,E)`,
 117   REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
 118
 119 let FAN1_LINEAR_IMAGE_EQ = prove
 120  (`!f:real^M->real^N x V E.
 121     linear f /\ (!x y. f x = f y ==> x = y)
 122     ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
 123   REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
 124
 125 let FAN2_TRANSLATION_EQ = prove
 126  (`!a:real^N x V E.
 127         fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 128         fan2(x,V,E)`,
 129   REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
 130
 131 let FAN2_LINEAR_IMAGE_EQ = prove
 132  (`!f:real^M->real^N x V E.
 133     linear f /\ (!x y. f x = f y ==> x = y)
 134     ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
 135   REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
 136
 137 let FAN3_TRANSLATION_EQ = prove
 138  (`!a:real^N x V E.
 139         fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 140         fan3(x,V,E)`,
 141   REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
 142
 143 let FAN3_LINEAR_IMAGE_EQ = prove
 144  (`!f:real^M->real^N x V E.
 145     linear f /\ (!x y. f x = f y ==> x = y)
 146     ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
 147   let lemma = prove
 148    (`{w | {a,w} IN IMAGE (IMAGE f) s} =
 149      IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
 150     MATCH_MP_TAC(SET_RULE
 151      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
 152     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 153     MESON_TAC[]) in
 154   REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
 155
 156 let FAN4_TRANSLATION_EQ = prove
 157  (`!a:real^N x V E.
 158         fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 159         fan4(x,V,E)`,
 160   REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
 161
 162 let FAN4_LINEAR_IMAGE_EQ = prove
 163  (`!f:real^M->real^N x V E.
 164     linear f /\ (!x y. f x = f y ==> x = y)
 165     ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
 166   REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
 167
 168 let FAN5_TRANSLATION_EQ = prove
 169  (`!a:real^N x V E.
 170         fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 171         fan5(x,V,E)`,
 172   REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
 173
 174 let FAN5_LINEAR_IMAGE_EQ = prove
 175  (`!f:real^M->real^N x V E.
 176     linear f /\ (!x y. f x = f y ==> x = y)
 177     ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
 178   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 179    [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 180   GEOM_TRANSFORM_TAC[]);;
 181
 182 let FAN6_TRANSLATION_EQ = prove
 183  (`!a:real^N x V E.
 184         fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 185         fan6(x,V,E)`,
 186   REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
 187
 188 let FAN6_LINEAR_IMAGE_EQ = prove
 189  (`!f:real^M->real^N x V E.
 190     linear f /\ (!x y. f x = f y ==> x = y)
 191     ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
 192   REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
 193
 194 let FAN7_TRANSLATION_EQ = prove
 195  (`!a:real^N x V E.
 196         fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 197         fan7(x,V,E)`,
 198   REWRITE_TAC[fan7] THEN
 199   REWRITE_TAC[SET_RULE
 200    `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
 201   GEOM_TRANSLATE_TAC[]);;
 202
 203 let FAN7_LINEAR_IMAGE_EQ = prove
 204  (`!f:real^M->real^N x V E.
 205     linear f /\ (!x y. f x = f y ==> x = y)
 206     ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
 207   REWRITE_TAC[fan7; IN_UNION] THEN
 208   REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB;
 209               TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 210   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 211    [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 212   REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN
 213   GEOM_TRANSFORM_TAC[]);;
 214
 215 add_translation_invariants
 216  [GRAPH_TRANSLATION_EQ;
 217   FAN1_TRANSLATION_EQ;
 218   FAN2_TRANSLATION_EQ;
 219   FAN3_TRANSLATION_EQ;
 220   FAN4_TRANSLATION_EQ;
 221   FAN5_TRANSLATION_EQ;
 222   FAN6_TRANSLATION_EQ;
 223   FAN7_TRANSLATION_EQ];;
 224
 225 add_linear_invariants
 226  [GRAPH_LINEAR_IMAGE_EQ;
 227   FAN1_LINEAR_IMAGE_EQ;
 228   FAN2_LINEAR_IMAGE_EQ;
 229   FAN3_LINEAR_IMAGE_EQ;
 230   FAN4_LINEAR_IMAGE_EQ;
 231   FAN5_LINEAR_IMAGE_EQ;
 232   FAN6_LINEAR_IMAGE_EQ;
 233   FAN7_LINEAR_IMAGE_EQ];;
 234
 235 let FAN_TRANSLATION_EQ = prove
 236  (`!a:real^N x V E.
 237         FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 238         FAN(x,V,E)`,
 239   REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
 240
 241 let FAN_LINEAR_IMAGE_EQ = prove
 242  (`!f:real^M->real^N x V E.
 243     linear f /\ (!x y. f x = f y ==> x = y)
 244     ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
 245   REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
 246
 247 add_translation_invariants [FAN_TRANSLATION_EQ];;
 248 add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
 249
 250 let BASE_POINT_FAN_TRANSLATION_EQ = prove
 251  (`!a x V E.
 252     base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) =
 253     a + base_point_fan(x,V,E)`,
 254   REWRITE_TAC[base_point_fan]);;
 255
 256 let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
 257  (`!f:real^M->real^N x V E.
 258         linear f
 259         ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) =
 260             f(base_point_fan(x,V,E))`,
 261   REWRITE_TAC[base_point_fan]);;
 262
 263 let SET_OF_EDGE_TRANSLATION_EQ = prove
 264  (`!a:real^N x V E.
 265         set_of_edge (a + x) (IMAGE (\x. a + x) V)
 266                     (IMAGE (IMAGE (\x. a + x)) E) =
 267         IMAGE (\x. a + x) (set_of_edge x V E)`,
 268   REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
 269
 270 let SET_OF_EDGE_LINEAR_IMAGE_EQ = prove
 271  (`!f:real^M->real^N x V E.
 272         linear f /\ (!x y. f x = f y ==> x = y)
 273         ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) =
 274             IMAGE f (set_of_edge x V E)`,
 275   let lemma = prove
 276    (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
 277      {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
 278     MATCH_MP_TAC(SET_RULE
 279      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
 280     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 281     MESON_TAC[]) in
 282   REWRITE_TAC[set_of_edge; lemma] THEN
 283   GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
 284
 285 add_translation_invariants
 286  [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;
 287
 288 add_linear_invariants
 289  [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
 290
 291
 292
 293
 294
 295
 296
 297 let CTVTAQA=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E1:(real^3->bool)->bool).
 298 FAN(x,V,E) /\ E1 SUBSET E
 299 ==>
 300 FAN(x,V,E1)`,
 301 REPEAT GEN_TAC
 302 THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7;graph]
 303 THEN ASM_SET_TAC[]);;
 304
 305
 306
 307 (* ========================================================================== *)
 308 (*                        SET_OF_EDGE                     *)
 309 (* ========================================================================== *)
 310
 311
 312 let set_of_edge_subset_edges=prove(`!(V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
 313  set_of_edge v V E SUBSET V`,
 314 REWRITE_TAC[set_of_edge] THEN SET_TAC[]);;
 315
 316
 317
 318 let remark_fan1=prove(`!v w V E.
 319 (v IN V) /\ (w IN V) ==>
 320 ((w IN set_of_edge v V E)<=>(v IN set_of_edge w V E))`,
 321
 322 (let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
 323 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM]  THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
 324
 325 let remark_finite_fan1=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FINITE V ==> FINITE (set_of_edge v V E)`,
 326 REPEAT GEN_TAC THEN DISCH_TAC
 327   THEN MP_TAC(ISPECL [`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`; `V:real^3->bool`] FINITE_SUBSET)
 328   THEN ASM_REWRITE_TAC[]
 329   THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
 330
 331 let properties_of_set_of_edge=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3.
 332 UNIONS E SUBSET V
 333 ==>
 334 ({v,u} IN E <=> u IN set_of_edge v V E)`,
 335 REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
 336 THEN STRIP_TAC
 337  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
 338   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
 339
 340
 341
 342
 343 let expand_edge_graph_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (e:real^3->bool).
 344 FAN(x,V,E) /\ e IN E
 345 ==> ?v:real^3 w:real^3. e={v,w}`,
 346 REPEAT GEN_TAC
 347 THEN REWRITE_TAC[FAN;IN]
 348 THEN STRIP_TAC
 349 THEN FIND_ASSUM MP_TAC `graph (E:(real^3->bool)->bool)`
 350 THEN REWRITE_TAC[graph]
 351 THEN DISCH_TAC
 352 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`e:real^3->bool`th))
 353 THEN RESA_TAC
 354 THEN POP_ASSUM MP_TAC
 355 THEN REWRITE_TAC[HAS_SIZE]
 356 THEN STRIP_TAC
 357 THEN SUBGOAL_THEN `~((e:real^3->bool)={})` ASSUME_TAC
 358 THENL[
 359 STRIP_TAC
 360 THEN MP_TAC(ISPEC`(e:real^3->bool)`CARD_EQ_0)
 361 THEN RESA_TAC
 362 THEN POP_ASSUM MP_TAC
 363 THEN ARITH_TAC;
 364 MP_TAC(SET_RULE `~((e:real^3->bool)={})==> ?v:real^3. v IN e`)
 365 THEN RESA_TAC
 366 THEN SUBGOAL_THEN`~((e:real^3->bool) DELETE v={})` ASSUME_TAC
 367 THENL[
 368 STRIP_TAC
 369 THEN MP_TAC(ISPECL[`v:real^3`;`(e:real^3->bool)`;]CARD_DELETE)
 370 THEN RESA_TAC
 371 THEN MP_TAC(ISPECL[`(e:real^3->bool)`;`v:real^3`] FINITE_DELETE)
 372 THEN RESA_TAC
 373 THEN MP_TAC(ISPEC`(e:real^3->bool) DELETE v`CARD_EQ_0)
 374 THEN RESA_TAC
 375 THEN POP_ASSUM MP_TAC
 376 THEN ARITH_TAC;
 377 MP_TAC(SET_RULE `~((e:real^3->bool)DELETE v={})==> ?w:real^3. w IN (e:real^3->bool)DELETE v/\ w IN e`)
 378 THEN RESA_TAC
 379 THEN MP_TAC(SET_RULE `(v IN (e:real^3->bool))/\ (w IN (e:real^3->bool))==> {v,w} SUBSET e`)
 380 THEN RESA_TAC
 381 THEN MP_TAC(SET_RULE `(w IN (e:real^3->bool)DELETE v)==> ~(v=w)`)
 382 THEN RESA_TAC
 383 THEN MP_TAC(ISPECL [`{v:real^3,w:real^3}`;`(e:(real^3->bool))`] FINITE_SUBSET)
 384 THEN RESA_TAC
 385 THEN ASSUME_TAC(SET_RULE `v:real^3 IN {v:real^3,w:real^3} `)
 386 THEN MP_TAC(ISPECL[`v:real^3`;`{v:real^3,w:real^3}`;]CARD_DELETE)
 387 THEN RESA_TAC
 388 THEN MP_TAC(SET_RULE `v IN {v,w}==>{v:real^3,w:real^3} DELETE v PSUBSET {v,w}`)
 389 THEN RESA_TAC
 390 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v`;`{v:real^3,w:real^3}`]CARD_PSUBSET)
 391 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 392 THEN FIND_ASSUM MP_TAC`FINITE {v:real^3,w:real^3}`
 393 THEN DISCH_TAC
 394 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 395 THEN DISCH_TAC
 396 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v) < CARD {v, w}/\ CARD ({v, w} DELETE v) = CARD {v, w}-1
 397 <=>CARD ({v, w} DELETE v) +1= CARD {v:real^3, w:real^3}`)
 398 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 399 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
 400 THEN REWRITE_TAC[ARITH_RULE`A=A`]
 401 THEN DISCH_TAC
 402 THEN SUBGOAL_THEN `w:real^3 IN ({v:real^3,w:real^3} DELETE v)` ASSUME_TAC
 403 THENL[
 404 ASM_SET_TAC[];
 405 MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`v:real^3`] FINITE_DELETE)
 406 THEN RESA_TAC
 407 THEN MP_TAC(ISPECL[`w:real^3`;`{v:real^3,w:real^3} DELETE v`;]CARD_DELETE)
 408 THEN RESA_TAC
 409 THEN MP_TAC(SET_RULE `w IN ({v,w} DELETE v)==>{v:real^3,w:real^3} DELETE v DELETE w PSUBSET {v,w} DELETE v`)
 410 THEN RESA_TAC
 411 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v DELETE w`;`{v:real^3,w:real^3} DELETE v`]CARD_PSUBSET)
 412 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 413 THEN FIND_ASSUM MP_TAC`FINITE ({v:real^3,w:real^3} DELETE v)`
 414 THEN DISCH_TAC
 415 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 416 THEN DISCH_TAC
 417 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v DELETE w) < CARD ({v, w} DELETE v)/\ CARD ({v, w} DELETE v DELETE w) = CARD ({v, w} DELETE v)-1
 418 <=>CARD ({v, w} DELETE v DELETE w) +1= CARD ({v:real^3, w:real^3} DELETE v)`)
 419 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
 420 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
 421 THEN REWRITE_TAC[ARITH_RULE`A=A`]
 422 THEN DISCH_TAC
 423 THEN POP_ASSUM MP_TAC
 424 THEN POP_ASSUM (fun th->REWRITE_TAC[])
 425 THEN POP_ASSUM (fun th->REWRITE_TAC[])
 426 THEN ASSUME_TAC(SET_RULE `{v, w} DELETE v:real^3 DELETE w:real^3={}`)
 427 THEN POP_ASSUM (fun th->REWRITE_TAC[th;CARD_CLAUSES; ARITH_RULE `0+1=1`])
 428 THEN POP_ASSUM MP_TAC
 429 THEN DISCH_THEN(LABEL_TAC"B")
 430 THEN DISCH_TAC
 431 THEN REMOVE_THEN "B" MP_TAC
 432 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th);ARITH_RULE` 1+1=2`])
 433 THEN FIND_ASSUM MP_TAC`CARD (e:real^3->bool)=2`
 434 THEN DISCH_TAC
 435 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
 436 THEN DISCH_TAC
 437 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`e:real^3->bool`]CARD_SUBSET_EQ)
 438 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
 439 THEN RESA_TAC
 440 THEN EXISTS_TAC`v:real^3`
 441 THEN EXISTS_TAC`w:real^3`
 442 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])]]]);;
 443
 444
 445
 446
 447
 448 let add_edge_graph_fan=prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A.
 449  v IN V /\ u IN V /\ E1=E UNION {{v,u}} /\ UNIONS E SUBSET V==> UNIONS E1 SUBSET V`,
 450 REPEAT STRIP_TAC
 451 THEN POP_ASSUM MP_TAC
 452 THEN ASM_REWRITE_TAC[UNIONS; SUBSET; UNION; IN_ELIM_THM;IN_SING]
 453 THEN DISCH_THEN(LABEL_TAC "YEU")
 454 THEN REPEAT STRIP_TAC
 455 THENL[SUBGOAL_THEN`(?u. u IN E /\ x IN (u:A->bool))`ASSUME_TAC
 456 THENL[
 457 EXISTS_TAC`u':A->bool` THEN ASM_REWRITE_TAC[];
 458 REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `x:A`)];
 459 ASM_TAC THEN SET_TAC[]]);;
 460
 461
 462 let garph_add_edge_is_garph=prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A.
 463  E1=E UNION {{v,u}} /\ ~(v=u) /\ graph E==> graph E1`,
 464 REPEAT STRIP_TAC
 465 THEN POP_ASSUM MP_TAC
 466 THEN ASM_REWRITE_TAC[GRAPH; UNION;IN_ELIM_THM;IN_SING]
 467 THEN DISCH_THEN(LABEL_TAC"YEU")
 468 THEN GEN_TAC THEN STRIP_TAC
 469 THENL[REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `e:A->bool`);
 470 ASM_REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC
 471 THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`]
 472 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 473                  IN_INSERT; NOT_IN_EMPTY]]);;
 474
 475 let add_edge_into_collinear_fan=prove(`!x:real^3 (E:(real^3->bool)->bool) v:real^3 u:real^3.
 476 ~collinear {x,v,u} /\
 477 (!e. e IN E ==> ~collinear ({x} UNION e))
 478 ==>
 479 (!e. e IN E UNION {{v, u}} ==> ~collinear ({x} UNION e))`,
 480 REPEAT STRIP_TAC
 481 THEN POP_ASSUM MP_TAC
 482 THEN POP_ASSUM MP_TAC
 483 THEN ASM_REWRITE_TAC[]
 484 THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)[UNION;]
 485 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING]
 486 THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
 487 THEN STRIP_TAC
 488 THENL[REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th `e:real^3->bool`);
 489 ASM_REWRITE_TAC[SET_RULE`{X} UNION {A,B}={X,A,B}`]]);;
 490
 491
 492 let properties_edges_eq_fan=prove(`!e:A-> bool v:A u:A.
 493 FINITE e /\ ~(e={v,u}) /\ ~(v=u)  /\ CARD e=2  ==>  ~(v IN e)\/ ~(u IN e)`,
 494 REPEAT GEN_TAC THEN STRIP_TAC
 495 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "YEU")
 496 THEN ONCE_REWRITE_TAC[SET_RULE`~A \/ ~B<=> ~(A/\B)`]
 497 THEN STRIP_TAC
 498 THEN MP_TAC(SET_RULE`v IN e /\ u IN e ==> {v:A,u} SUBSET e`)
 499 THEN RESA_TAC
 500 THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`]
 501 THEN REMOVE_THEN "YEU" MP_TAC
 502 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 503 THEN STRIP_TAC
 504 THEN MRESA_TAC CARD_SUBSET_EQ[`{v,u:A}`;`e:A->bool`]);;
 505
 506
 507
 508
 509 (* ========================================================================== *)
 510 (*                        BASIC FAN                     *)
 511 (* ========================================================================== *)
 512
 513
 514 let set_edges_is_finite_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool).
 515 FAN(x,V,E)==> FINITE E`,
 516 REPEAT GEN_TAC
 517 THEN REWRITE_TAC[FAN;fan1;graph]
 518 THEN STRIP_TAC
 519 THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET)
 520 THEN RESA_TAC
 521 THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`)
 522 THEN RESA_TAC
 523   THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET)
 524 THEN ASM_SET_TAC[]);;
 525
 526
 527
 528 let properties_of_set_of_edge_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
 529 FAN(x,V,E)
 530 ==>
 531 ({v,u} IN E <=> u IN set_of_edge v V E)`,
 532 REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
 533 THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC
 534  THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
 535   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
 536
 537
 538
 539 let properties_of_graph=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 540 FAN(x,V,E) /\{v,u} IN E==> v IN V`,
 541
 542 REPEAT GEN_TAC THEN REWRITE_TAC[FAN] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN
 543 REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC
 544   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC
 545 THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
 546
 547
 548 let properties_of_graph1=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 549 FAN(x,V,E) /\{v,u} IN E==> u IN V`,
 550 ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[properties_of_graph]);;
 551
 552
 553 let th4=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 554 FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
 555 REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`; `(v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan2] THEN SET_TAC[]);;
 556
 557 let remark4_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 558 FAN(x,V,E) /\ {v,u} IN E==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\ DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,
 559
 560 REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN"a"(fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REWRITE_TAC[th3]);;
 561
 562
 563 let collinears_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 564 FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
 565 MESON_TAC[remark4_fan;collinear_fan]);;
 566
 567 let remark1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 568 FAN(x,V,E) ==>
 569 FINITE (set_of_edge v V E)
 570 /\({v,u} IN E <=> u IN set_of_edge v V E)/\
 571 ({v,u} IN E==>
 572 ~ collinear {x,v,u}/\
 573 ~ (x=v) /\ ~(x=u)/\ ~(v=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u}  /\ ~(u IN aff {x,v}) /\ v IN V /\ u IN V/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
 574 MESON_TAC[FAN;fan1;remark_finite_fan1;remark4_fan; properties_of_graph; SET_RULE`DISJOINT {x,v} {u} ==> ~(v=u)`;collinears_fan;properties_of_set_of_edge_fan;properties_of_graph1]);;
 575
 576
 577
 578
 579
 580
 581 (* ========================================================================== *)
 582 (*                       EXISTS  SIGMA_FAN                     *)
 583 (* ========================================================================== *)
 584
 585
 586
 587 let sigma_fan=new_definition`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
 588 (if (set_of_edge v V E = {u} ) then u
 589     else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 590 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
 591
 592
 593 (* This extends sigma to have a larger domain
 594    of R^3 rather than just V.  It is the
 595    identity outside V (compare the definition
 596    of `permutes` ).   *)
 597
 598
 599
 600
 601 let extension_sigma_fan=new_definition`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
 602 (if ~(u IN set_of_edge v V E ) then u
 603     else (sigma_fan x V E v u))`;;
 604
 605
 606
 607
 608
 609 let exists_sigma_fan=prove(`
 610 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 611 ~ (set_of_edge v V E= {u} )
 612 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 613 ==>
 614 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 615 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`,
 616 (let lemma = prove
 617    (`!X:real->bool.
 618           FINITE X /\ ~(X = {})
 619           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 620     MESON_TAC[INF_FINITE]) in
 621
 622
 623 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 624
 625 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
 626 THENL[(*2*)
 627 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
 628
 629 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 630  ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
 631 THENL[(*3*)
 632 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
 633   THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
 634 THENL[(*4*)
 635 ASM_TAC THEN SET_TAC[];(*4*)
 636 ASM_TAC THEN SET_TAC[]](*4*);(*3*)
 637 SUBGOAL_THEN`~(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
 638 THENL[(*4*)
 639 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
 640
 641 SUBGOAL_THEN` FINITE (IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
 642 THENL[(*5*)
 643 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
 644 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th))
 645   THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
 646   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
 647 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
 648
 649
 650
 651 let SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 652 ~ (set_of_edge v V E= {u} )
 653 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 654 ==>
 655 ((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\
 656 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u (sigma_fan x V E v u) <= azim x v u w1)`,
 657
 658 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan]
 659   THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]exists_sigma_fan)  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
 660
 661
 662
 663
 664
 665 let sigma_fan_in_set_of_edge=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 666 FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 667 ==>
 668 ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
 669
 670 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~ (set_of_edge v V E= {u:real^3} )\/ (set_of_edge v V E= {u} )`)
 671 THENL[
 672  MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
 673 THEN ASM_TAC
 674 THEN SET_TAC[];
 675 ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
 676
 677
 678
 679 (* ========================================================================== *)
 680 (*                   CONDITION UNIQUE FOINT AND SIGMA_FAN                     *)
 681 (* ========================================================================== *)
 682
 683
 684
 685
 686
 687 let UNIQUE_FOINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
 688 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\
 689  ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v})
 690 ==> u=w`,
 691 REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC
 692   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 693   THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC
 694   THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th))
 695   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
 696   THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`)
 697 THENL
 698 [  MP_TAC(SET_RULE`~((u:real^3)=(w:real^3))==> {(v:real^3),(u:real^3)} INTER {(v:real^3),(w:real^3)}={v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];
 699 ASM_TAC THEN SET_TAC[]]);;
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709 let UNIQUE1_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
 710 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u}
 711 ==> u=w`,
 712 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN
 713 EXISTS_TAC `x:real^3` THEN EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `E:(real^3->bool)->bool` THEN EXISTS_TAC `v:real^3`
 714            THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC)
 715            THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
 716            THEN DISCH_TAC THEN  DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
 717            THEN DISCH_THEN (LABEL_TAC "a")
 718            THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
 719 THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 720   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th))
 721   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
 722            THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c")
 723            THEN DISCH_TAC THEN DISCH_TAC
 724   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 725   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 726            THEN DISCH_TAC THEN DISCH_TAC
 727   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
 728            THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
 729            THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC
 730 THENL (*1*)[
 731 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_10)
 732 THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`)
 733   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 734   THEN ASM_REWRITE_TAC[]
 735   THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*)
 736
 737 SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC
 738 THENL (*2*)[
 739 ASM_TAC THEN SET_TAC[];(*2*)
 740
 741 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`)
 742 THENL (*3*)[
 743  SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
 744 THENL (*4*)[
 745  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
 746    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 747 THEN EXISTS_TAC `t1:real`
 748   THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[]
 749     THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*)
 750
 751  SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
 752 THENL (*5*)[
 753  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
 754    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 755 THEN EXISTS_TAC `&0:real`
 756   THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real`  THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &0 % v + &1 % w `] THEN REAL_ARITH_TAC;(*5*)
 757
 758 ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*)
 759
 760  SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
 761 THENL (*4*)[
 762  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
 763    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 764 THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))`
 765   THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)`
 766 THEN MP_TAC(ISPEC `t3:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0< inv(t3:real)==> (&0 <= inv(t3:real))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 767 THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 768 THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN
 769 MP_TAC(REAL_ARITH`(t1:real)+(t2:real)+(t3:real)= &1 ==> &1 - t1- t2=t3`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 770 MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH`
 771  (inv t3 * --t1) % x +
 772  (inv t3 * --t2) % v +
 773  inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u `
 774 ] THEN DISCH_TAC
 775 THEN MP_TAC(ISPEC `t3:real` REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH ` v= &1 % v`];(*4*)
 776
 777  SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
 778 THENL (*5*)[
 779  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
 780    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 781 THEN EXISTS_TAC `&0:real`
 782   THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real`  THEN REWRITE_TAC[VECTOR_ARITH`u= &0 % x+ &0 % v + &1 % u `] THEN REAL_ARITH_TAC;(*5*)
 783 ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;
 784
 785
 786 let UNIQUE_AZIM_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3 w1:real^3.
 787 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ { v, w1} IN E /\ (azim x v u w =azim x v u w1)
 788 ==> w=w1`,
 789
 790 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN  REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
 791   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
 792   THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 793   THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 794   THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w1:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
 795   THEN REPEAT STRIP_TAC
 796   THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) THEN
 797 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 798 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` w1:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[]      );;
 799
 800
 801 let UNIQUE_AZIM_0_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
 802 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0)
 803 ==> u=w`,
 804
 805 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN  REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
 806   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
 807   THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 808   THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
 809   THEN REPEAT STRIP_TAC
 810   THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) THEN
 811 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 812 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` w:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[]           );;
 813
 814
 815
 816
 817 let UNIQUE_SIGMA_FAN=prove(`
 818 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
 819 ~ (set_of_edge v V E= {u} )
 820 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 821 /\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 822 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)
 823 ==> sigma_fan x V E v u=w)`,
 824
 825         (   let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
 826 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
 827 ==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
 828 ) in
 829
 830 ASSUME_TAC(th) THEN
 831 REPEAT GEN_TAC  THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN
 832 DISCH_TAC  THEN DISCH_THEN(LABEL_TAC "1")
 833   THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4")
 834   THEN DISCH_THEN(LABEL_TAC"a")
 835   THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
 836   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 837   THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` th))
 838   THEN ASM_REWRITE_TAC[]
 839   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[]
 840   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
 841   THEN REPEAT DISCH_TAC
 842   THEN SUBGOAL_THEN `azim x v u (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = azim x v u (w:real^3)` ASSUME_TAC
 843 THENL[
 844 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 845 REMOVE_THEN "123" (fun th->MP_TAC (ISPECL[`(x:real^3)`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`; `(v:real^3)` ; `(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`(w:real^3)`]th))
 846 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 847 THEN
 848 REMOVE_THEN"1" MP_TAC
 849 THEN  REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
 850 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
 851   THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC
 852   THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
 853   THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
 854   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 855   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 856   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
 857   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
 858   THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)` ;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`; `(w:real^3)`]AZIM_EQ )
 859   THEN ASM_REWRITE_TAC[]
 860   THEN ASM_MESON_TAC[]]));;
 861
 862
 863
 864 (* ========================================================================== *)
 865 (*                   CYCLIC SET FAN                    *)
 866 (* ========================================================================== *)
 867
 868
 869
 870
 871
 872 let CYCLIC_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
 873 FAN(x,V,E) /\ v IN V
 874 ==> cyclic_set (set_of_edge v V E) x v`,
 875 REPEAT GEN_TAC
 876 THEN STRIP_TAC
 877 THEN REPEAT (POP_ASSUM MP_TAC)
 878 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th)
 879 THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC
 880   THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*)
 881 STRIP_TAC
 882   THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*)
 883  STRIP_TAC THENL(*3*)[
 884
 885 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
 886 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 887   DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
 888 THEN STRIP_TAC THEN STRIP_TAC THEN
 889 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th))
 890   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th))
 891   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
 892   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 893   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 894   THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 895   THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 896   THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
 897   THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC
 898
 899 THENL (*4*)[
 900  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
 901            THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 902    THEN EXISTS_TAC `--(h:real)` THEN EXISTS_TAC `(h:real)` THEN EXISTS_TAC `&1` THEN REWRITE_TAC[VECTOR_ARITH`q= (-- (h:real)) % x + (h:real) % v + &1 % (q+ h% (x-v))`] THEN REAL_ARITH_TAC;(*4*)
 903
 904 ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*)
 905
 906 REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC
 907 THEN SUBGOAL_THEN`(x':real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ==> ~(x' IN aff {x,v})`
 908 ASSUME_TAC
 909 THENL(*4*)[
 910 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
 911 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 912   DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
 913 THEN STRIP_TAC THEN STRIP_TAC THEN
 914 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) )
 915   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC
 916   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*)
 917
 918 EQ_TAC THENL(*5*)[
 919
 920 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN STRIP_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[aff];(*5*)
 921
 922 ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
 923
 924
 925 let XOHLED=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
 926 FAN(x,V,E) /\ v IN V
 927 ==> cyclic_set (set_of_edge v V E) x v`,
 928 MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
 929
 930
 931 (* ========================================================================== *)
 932 (*                   SIGMA_FAN IS PERMUTES     (^_^)                          *)
 933 (* ========================================================================== *)
 934
 935
 936 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
 937
 938
 939 let exists_inverse_sigma_fan_alt=prove(`
 940 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 941 ~ (set_of_edge v V E= {u} )
 942 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 943 ==>
 944 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 945 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <=  azim1 x v u w1)))
 946 `,
 947 (let lemma = prove
 948    (`!X:real->bool.
 949           FINITE X /\ ~(X = {})
 950           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 951     MESON_TAC[INF_FINITE]) in
 952 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 953 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
 954 THENL[(*2*)
 955
 956 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
 957 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 958  ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
 959 THENL[(*3*)
 960 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
 961   THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
 962 THENL[(*4*)
 963 ASM_TAC THEN SET_TAC[];(*4*)
 964 ASM_TAC THEN SET_TAC[](*4*)];
 965
 966 SUBGOAL_THEN`~(IMAGE ( azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
 967 THENL[(*4*)
 968 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
 969 SUBGOAL_THEN` FINITE (IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
 970 THENL[(*5*)
 971 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
 972 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th))
 973   THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
 974 THEN EXISTS_TAC`x':real^3`
 975   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
 976 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
 977
 978
 979
 980
 981 let  SUR_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 982 FAN(x,V,E) /\ ({v,u} IN E)
 983 ==> ?w.  {v,w} IN E /\sigma_fan x V E v w= u
 984 `,
 985 REPEAT GEN_TAC THEN STRIP_TAC
 986 THEN DISJ_CASES_TAC(SET_RULE `(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`)
 987 THENL(*1*)[
 988 EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*)
 989
 990 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 991 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]exists_inverse_sigma_fan_alt) THEN ASM_REWRITE_TAC[azim1;] THEN STRIP_TAC THEN
 992 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[]
 993   THEN MATCH_MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`] UNIQUE_SIGMA_FAN)
 994   THEN ASM_REWRITE_TAC[]
 995   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC
 996 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`)
 997 THENL(*2*)[
 998 FIND_ASSUM(MP_TAC)`u:real^3 IN set_of_edge v V E` THEN POP_ASSUM(fun th->REWRITE_TAC[th;IN_SING]) THEN ASM_TAC THEN SET_TAC[] ;(*2*)
 999
1000 ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN
1001 DISJ_CASES_TAC(SET_RULE`~(azim (x:real^3) v w u <= azim x v w w1)\/ (azim (x:real^3) v w u <= azim x v w w1)`)
1002 THENL(*3*)[
1003 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC
1004 THENL(*4*)[
1005 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
1006  SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
1007 THENL(*5*)[
1008 ASM_TAC THEN SET_TAC[];(*5*)
1009 FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN
1010 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1011 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
1012 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1013   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (w1:real^3),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
1014                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1015   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`;`u:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[]
1016   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC
1017   THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC
1018 THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
1019 POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN
1020 MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge)
1021 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
1022  THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
1023   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
1024   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th))
1025   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
1026   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
1027 THEN
1028   DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (u:real^3) (w1:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (u:real^3) (w1:real^3) = &0)`)
1029 THENL(*7*)[
1030 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w1:real^3`]UNIQUE_AZIM_0_POINT_FAN)
1031 THEN ASM_TAC THEN SET_TAC[];(*7*)
1032
1033   DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (u:real^3) (w:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (u:real^3) (w:real^3) = &0)`)
1034 THENL(*8*)[
1035 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w:real^3`]UNIQUE_AZIM_0_POINT_FAN)
1036 THEN ASM_TAC THEN SET_TAC[];(*8*)
1037  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1038    THEN  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1039    THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1040    THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3.  w1 IN set_of_edge v V E /\ ~(w1 = u)
1041            ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1`
1042  THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1043 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`)
1044 THENL(*9*)[
1045 ASM_REWRITE_TAC[REAL_ARITH`&2 * pi -(a:real)<= &2 *pi - b <=> b <= a`] THEN DISJ_CASES_TAC(SET_RULE `(azim(x:real^3) v u w =azim x v u w1)\/ ~(azim(x:real^3) v u w =azim x v u w1)`)
1046 THENL(*10*)[
1047 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`;`(w1:real^3)`]UNIQUE_AZIM_POINT_FAN) THEN ASM_REWRITE_TAC[];(*10*)
1048 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*)
1049 SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC
1050 THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*)
1051 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*);
1052 ASM_TAC THEN SET_TAC[]]]]);;
1053
1054
1055
1056
1057
1058
1059 let MONO_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
1060 FAN(x,V,E) /\ ({v,u} IN E)
1061 /\ ({v,w} IN E)/\
1062  (sigma_fan x V E v u= sigma_fan x V E v w)
1063 ==> u=w
1064 `,
1065 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1")
1066 THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6]
1067 THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN
1068 DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") THEN
1069 REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1070 THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~((set_of_edge v V E={u}))`)
1071 THENL(*1*)[
1072 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
1073 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[]
1074 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
1075 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th))
1076 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
1077 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th))
1078   THEN ASM_TAC THEN SET_TAC[];(*1*)
1079
1080 DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})\/ ~((set_of_edge v V E={w}))`)
1081 THENL(*2*)[
1082
1083 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
1084 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[]
1085 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
1086 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th))
1087 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
1088 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th))
1089   THEN ASM_TAC THEN SET_TAC[];(*2*)
1090
1091
1092 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
1093   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1094 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
1095   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1096   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN)
1097 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1098   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th))
1099 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
1100 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1101   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th))
1102   THEN ASM_REWRITE_TAC[]
1103 THEN MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge)
1104 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
1105  THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
1106   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
1107   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
1108   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
1109   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
1110 DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`)
1111
1112 THENL(*3*)[
1113 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{(w:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC
1114 THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*)
1115
1116 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
1117 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1118   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
1119                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
1120   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "c") THEN
1121   DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
1122
1123 THENL(*5*)[
1124 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN)
1125 THEN ASM_TAC THEN SET_TAC[];(*5*)
1126
1127 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3) = &0)`)
1128
1129 THENL(*6*)[
1130
1131 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
1132 THEN ASM_TAC THEN SET_TAC[];(*6*)
1133
1134   DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3)  (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3) = &0)`)
1135
1136 THENL(*7*)[
1137 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
1138 THEN ASM_TAC THEN SET_TAC[];(*7*)
1139
1140 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]AZIM_COMPL)
1141 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1142 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN
1143 ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC
1144 THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`]
1145   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`] azim)THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
1146 (*7*)](*6*)](*5*)](*4*)];(*3*)
1147
1148 ASM_REWRITE_TAC[](*3*)]]]);;
1149
1150
1151
1152
1153 let permutes_sigma_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
1154 FAN(x,V,E) /\ ({v,u} IN E)
1155 ==>
1156 (extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
1157 REPEAT GEN_TAC THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`FAN((x:real^3), V, E)` THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC
1158 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`]remark_finite_fan1)
1159   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1160   THEN MP_TAC(ISPECL[`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`;`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`]PERMUTES_FINITE_INJECTIVE)
1161   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1162 THENL[
1163 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan];
1164 STRIP_TAC
1165 THENL[
1166 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)}\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)})`)
1167 THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING];
1168 ASM_MESON_TAC[SIGMA_FAN]];
1169 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC
1170   THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge)
1171   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1172 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge)
1173   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1174 ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;
1175
1176
1177
1178
1179 (* ========================================================================== *)
1180 (*                   INVERSE OF SIGMA_FAN                   *)
1181 (* ========================================================================== *)
1182
1183
1184
1185
1186 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
1187
1188
1189
1190
1191
1192
1193 let exists_function_inverse_sigma_fan_alt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
1194 FAN(x,V,E) ==>
1195 (?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
1196 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
1197 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w))
1198 `,
1199 REPEAT STRIP_TAC THEN
1200 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] sigma_fan_in_set_of_edge) THEN
1201  ASM_REWRITE_TAC[] THEN DISCH_TAC
1202 THEN MP_TAC(ISPECL[`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`; `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]BIJECTIVE_ON_LEFT_RIGHT_INVERSE)
1203   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] properties_of_set_of_edge_fan) THEN
1204  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1205
1206 THEN
1207 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) THEN
1208  ASM_REWRITE_TAC[] THEN DISCH_TAC
1209 THEN
1210 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] SUR_SIGMA_FAN) THEN
1211  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
1212
1213 (*
1214 This is the same as inverse_sigma_fan_alt,
1215 but easier to use.
1216 *)
1217
1218
1219
1220 let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
1221 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
1222 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
1223
1224
1225
1226 let INVERSE1_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
1227 FAN(x,V,E) ==>
1228 ( (!w:real^3. {v,w} IN E==> {v, inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w} IN E)
1229 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w) =w)
1230 /\ (!w:real^3. {v,w} IN E==> inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (sigma_fan x V E v w) =w))`,
1231 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[inverse1_sigma_fan] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `]exists_function_inverse_sigma_fan_alt)
1232   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC  THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
1233
1234
1235
1236
1237
1238 (* ========================================================================== *)
1239 (*                   PROPERTIES OF FAN                   *)
1240 (* ========================================================================== *)
1241
1242
1243
1244
1245 let properties_of_fan7=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3  u1:real^3.
1246 FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1,u1}
1247 ==> v = v1 \/ v = u1`,
1248
1249 REPEAT STRIP_TAC
1250 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
1251 THEN REWRITE_TAC[FAN; fan6; fan7]
1252 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1253 THEN STRIP_TAC
1254   THEN POP_ASSUM  (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3),(u1:real^3)}`]th))
1255   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
1256 THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
1257 THENL(*1*)[
1258  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
1259    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1260 THEN EXISTS_TAC `&0:real`
1261   THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real`
1262 THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC;
1263
1264 DISCH_TAC
1265 THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u} /\ v IN aff_ge {x} {v1, u1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1, u1:real^3}`)
1266 THEN RESA_TAC
1267 THEN POP_ASSUM MP_TAC
1268 THEN DISJ_CASES_TAC(SET_RULE`{v, u} INTER {v1, u1:real^3}={} \/ ~({v, u} INTER {v1, u1}={})`)
1269 THENL(*2*)[
1270 ASM_REWRITE_TAC[]
1271 THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC
1272 THENL(*3*)[
1273 ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`)
1274 THEN AFF_TAC;
1275
1276 ASM_REWRITE_TAC[IN_ELIM_THM]
1277 THEN STRIP_TAC THEN POP_ASSUM MP_TAC
1278 THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC
1279 THEN ASM_REWRITE_TAC[]];(*2*)
1280
1281 DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1, u1:real^3}) \/ (v IN {v, u} INTER {v1, u1})`)
1282 THENL(*3*)[
1283 SUBGOAL_THEN`({v:real^3, u} INTER {v1, u1}={u})` ASSUME_TAC
1284 THENL(*4*)[
1285  ASM_TAC
1286 THEN SET_TAC[];(*4*)
1287
1288 ASM_REWRITE_TAC[]
1289 THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC
1290 THENL(*5*)[
1291 MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1)
1292 THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`)
1293   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1294   THEN ASM_REWRITE_TAC[]
1295   THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*5*)
1296
1297 FIND_ASSUM MP_TAC`{v,u:real^3} IN E`
1298 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1299 THEN DISCH_TAC
1300 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`u:real^3`]
1301 THEN ASM_TAC
1302 THEN SET_TAC[]]];(*3*)
1303
1304 POP_ASSUM MP_TAC
1305 THEN SET_TAC[]]]])  ;;
1306
1307
1308
1309
1310
1311
1312 let properties1_of_fan7=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3  u1:real^3.
1313 FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1}
1314 ==> v = v1`,
1315
1316 REPEAT STRIP_TAC
1317 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
1318 THEN REWRITE_TAC[FAN; fan6; fan7]
1319 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1320 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u1:real^3`;`v1:real^3`]
1321 THEN MP_TAC(SET_RULE`(v1:real^3) IN V==> (?v. v IN V /\ {v1} = {v})`)
1322 THEN REDA_TAC
1323 THEN STRIP_TAC
1324   THEN POP_ASSUM  (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3)}`]th))
1325   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
1326 THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
1327 THENL(*1*)[
1328  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
1329    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1330 THEN EXISTS_TAC `&0:real`
1331   THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real`
1332 THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC;
1333 DISCH_TAC
1334 THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u:real^3} /\ v IN aff_ge {x} {v1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1}`)
1335 THEN RESA_TAC
1336 THEN POP_ASSUM MP_TAC
1337 THEN DISJ_CASES_TAC(SET_RULE`{v, u:real^3} INTER {v1}={} \/ ~({v, u} INTER {v1}={})`)
1338 THENL(*2*)[
1339 ASM_REWRITE_TAC[]
1340 THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC
1341 THENL(*3*)[
1342 ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`)
1343 THEN AFF_TAC;
1344 ASM_REWRITE_TAC[IN_ELIM_THM]
1345 THEN STRIP_TAC THEN POP_ASSUM MP_TAC
1346 THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC
1347 THEN ASM_REWRITE_TAC[]];(*2*)
1348
1349 DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1:real^3}) \/ (v IN {v, u} INTER {v1})`)
1350 THENL(*3*)[
1351 SUBGOAL_THEN`({v:real^3, u} INTER {v1:real^3}={u})` ASSUME_TAC
1352 THENL(*4*)[
1353  ASM_TAC
1354 THEN SET_TAC[];
1355 ASM_REWRITE_TAC[]
1356 THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC
1357 THENL(*5*)[
1358 MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1)
1359 THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`)
1360   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1361   THEN ASM_REWRITE_TAC[]
1362   THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];
1363 FIND_ASSUM MP_TAC`{v,u:real^3} IN E`
1364 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1365 THEN DISCH_TAC
1366 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
1367 THEN ASM_TAC
1368 THEN SET_TAC[]]];(*3*)
1369
1370 POP_ASSUM MP_TAC
1371 THEN SET_TAC[]]]])  ;;
1372
1373
1374
1375
1376
1377 let expand_elements_by_azim_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 x1:real x2:real x3:real.
1378 FAN(x,V,E)/\ {v,u} IN E /\ &0 < x1 /\ &0<= x2
1379 /\ x2 < &2 * pi
1380 /\ &0< x3
1381 /\ x3 < pi/ &2
1382 ==>
1383 azim x v u
1384  (x +
1385   (x1 * cos (x2) * sin (x3)) % e1_fan x v u +
1386   (x1 * sin (x2) * sin (x3)) % e2_fan x v u +
1387   (x1 * cos (x3)) % e3_fan x v u) = x2`,
1388
1389 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
1390  (let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in
1391
1392 REPEAT STRIP_TAC
1393 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;
1394 `(E:(real^3->bool)->bool)`;` u:real^3`;` v:real^3`]remark1_fan)
1395 THEN RESA_TAC
1396 THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
1397 THEN GEN_REWRITE_TAC( LAND_CONV  o ONCE_DEPTH_CONV)[lem1]
1398 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1399 THEN RESA_TAC
1400 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
1401 THEN RESA_TAC
1402 THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
1403 THEN REWRITE_TAC[orthonormal]
1404 THEN STRIP_TAC
1405 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
1406 THEN RESA_TAC
1407 THEN MP_TAC(ISPEC`x3:real`SIN_POS_PI2)
1408 THEN RESA_TAC
1409 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
1410   (x1 * cos (x2) * sin (x3)) % e1_fan x v u +
1411   (x1 * sin (x2) * sin (x3)) % e2_fan x v u +
1412   (x1 * cos (x3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
1413   `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1414   `(x1 * cos (x3)) * (inv (norm((v:real^3)-(x:real^3))))`;
1415 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
1416 `x1 * sin (x3:real)`;
1417 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`x2:real`]AZIM_UNIQUE)
1418 THEN DISCH_TAC
1419 THEN POP_ASSUM MATCH_MP_TAC
1420 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
1421 THEN STRIP_TAC
1422 THENL[
1423 MATCH_MP_TAC REAL_LT_MUL
1424 THEN REPEAT(POP_ASSUM MP_TAC)
1425 THEN REAL_ARITH_TAC;
1426
1427 STRIP_TAC
1428 THENL[
1429
1430 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1431 THEN REDUCE_ARITH_TAC
1432 THEN REDUCE_VECTOR_TAC
1433 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1434 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1435 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1436  ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1437 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1438 THEN REDUCE_ARITH_TAC
1439 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1440 THEN REDUCE_VECTOR_TAC
1441 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1442 THEN RESA_TAC
1443 THEN ASM_REWRITE_TAC[]
1444 THEN REWRITE_TAC[e1_fan]
1445 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1446 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1447 THEN ONCE_REWRITE_TAC[DOT_SYM]
1448 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1449 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1450 THEN ASM_REWRITE_TAC[]
1451 THEN REDUCE_VECTOR_TAC
1452 THEN STRIP_TAC
1453 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1454 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1455 THEN REWRITE_TAC[DOT_RZERO]
1456 THEN REAL_ARITH_TAC;
1457 REWRITE_TAC[e3_fan]
1458 THEN VECTOR_ARITH_TAC]])));;
1459
1460
1461 let one_edge_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1462 FAN(x,V,E)/\ {v,u} IN E /\ ~(CARD (set_of_edge v V E) > 1)
1463 ==> set_of_edge v V E={u}`,
1464 REPEAT STRIP_TAC
1465 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool) `;`u:real^3 `;`v:real^3`]remark1_fan)
1466 THEN RESA_TAC
1467 THEN MP_TAC(SET_RULE`(u:real^3) IN set_of_edge v V E==> ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={})/\ {(u:real^3)} SUBSET set_of_edge v V E`)
1468 THEN RESA_TAC
1469 THEN MP_TAC(ISPECL [`{(u:real^3)}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`] FINITE_SUBSET)
1470 THEN RESA_TAC
1471 THEN ASSUME_TAC(SET_RULE`u IN {(u:real^3)} /\ {(u:real^3)} DELETE u= {} /\ {} PSUBSET {(u:real^3)}`)
1472 THEN MP_TAC(ISPECL[`(u:real^3)`;`{(u:real^3)}`;]CARD_DELETE)
1473 THEN RESA_TAC
1474 THEN MP_TAC(ISPECL[`{}:real^3->bool`;`{(u:real^3)}`]CARD_PSUBSET)
1475 THEN RESA_TAC
1476 THEN POP_ASSUM MP_TAC
1477 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
1478 THEN POP_ASSUM MP_TAC
1479 THEN REWRITE_TAC[CARD_CLAUSES]
1480 THEN REPEAT DISCH_TAC
1481 THEN MP_TAC(ARITH_RULE` 0 = CARD ({(u:real^3)}) - 1 /\  0 < CARD ({u}) <=>  1= CARD {u}`)
1482 THEN RESA_TAC
1483 THEN MP_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) > 1)==> CARD (set_of_edge v V E) <= 1`)
1484 THEN RESA_TAC
1485 THEN MP_TAC(ISPECL[`{u:real^3}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]CARD_SUBSET_LE)
1486 THEN ASM_SET_TAC[]);;
1487
1488
1489
1490
1491
1492
1493 end;;