text_formalization/fan/introduction.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
  25 open Sphere;;
  26 open Fan_defs;;
  27 open Hypermap;;
  28
  29
  30 let ASM_TAC=REPEAT(POP_ASSUM MP_TAC);;
  31 let RED_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC;;
  32 let RES_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC;;
  33 let REDA_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];;
  34 let RESA_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[];;
  35 let REDAL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN DISCH_TAC THEN ASM_REWRITE_TAC th;;
  36 let RESAL_TAC (th: thm list) = ASM_REWRITE_TAC th THEN STRIP_TAC THEN ASM_REWRITE_TAC th;;
  37 let REMOVE_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[]);;
  38 let SYM_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);;
  39 let SYM_ASSUM1_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th));;
  40 let RESP_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]);;
  41 let RESPL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC [th]);;
  42 let REDUCE_ARITH_TAC=REWRITE_TAC[REAL_ARITH`&0 * a= &0`; REAL_ARITH`a * &0 = &0`; REAL_ARITH`a + &0 = a`;
  43 REAL_ARITH`a- &0 =a`;REAL_ARITH`&0 +a =a`;REAL_ARITH`&1 * a =a`;REAL_ARITH`a * &1 =a`;REAL_ARITH`(A+B)-B=A`];;
  44 let REDUCE_VECTOR_TAC=REWRITE_TAC[VECTOR_ARITH`&0 % a= vec 0`; VECTOR_ARITH`a % vec 0= vec 0`;VECTOR_ARITH`a + vec 0 = a`;
  45 VECTOR_ARITH`vec 0 +a =a`; VECTOR_ARITH`a- vec 0 =a`;VECTOR_ARITH`&1 % a =a`;VECTOR_ARITH`a- b =vec 0<=> a=b`];;
  46
  47 let MRESA_TAC th1 (th: term list) = MP_TAC(ISPECL th th1) THEN RESA_TAC;;
  48 let MRESA1_TAC th1 th = MP_TAC(ISPEC th th1) THEN RESA_TAC;;
  49
  50 let MRESAL_TAC th1 (th: term list) (th2: thm list) =MP_TAC(ISPECL th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;
  51
  52 let MRESAL1_TAC th1 th (th2: thm list) =MP_TAC(ISPEC th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;
  53
  54 let ASM_SET_TAC l =
  55     (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
  56
  57
  58
  59 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
  60
  61 let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
  62
  63 let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
  64
  65 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
  66
  67 let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
  68
  69 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 ={}))`;;
  70
  71 (* Deprecated, 2011-08-01, thales
  72 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)`;;
  73 *)
  74
  75 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
  76
  77 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
  78
  79
  80 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
  81
  82 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})
  83 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
  84
  85
  86
  87 let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
  88 fan6(x,V,E)/\ fan7(x,V,E)`;;
  89
  90
  91 (* ************************************************* *)
  92 (* Invariance theorems *)
  93
  94 let GRAPH = prove
  95  (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
  96   REWRITE_TAC[graph; IN]);;
  97
  98 let CYCLIC_SET = prove
  99  (`cyclic_set W v w <=>
 100          ~(v = w) /\
 101          FINITE W /\
 102          (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\
 103          W INTER affine hull {v, w} = {}`,
 104   REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
 105
 106 let CYCLIC_SET_TRANSLATION_EQ = prove
 107  (`!a:real^N s x y.
 108     cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
 109   REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
 110
 111 let CYCLIC_SET_LINEAR_IMAGE = prove
 112  (`!f:real^M->real^N s x y.
 113         linear f /\ (!x y. f x = f y ==> x = y)
 114         ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
 115   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 116    [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN
 117   GEOM_TRANSFORM_TAC[]);;
 118
 119 add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;
 120
 121 add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
 122
 123 let GRAPH_TRANSLATION_EQ = prove
 124  (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
 125   REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
 126
 127 let GRAPH_LINEAR_IMAGE_EQ = prove
 128  (`!f:real^M->real^N E.
 129     linear f /\ (!x y. f x = f y ==> x = y)
 130     ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
 131   REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
 132
 133 let FAN1_TRANSLATION_EQ = prove
 134  (`!a:real^N x V E.
 135         fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 136         fan1(x,V,E)`,
 137   REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
 138
 139 let FAN1_LINEAR_IMAGE_EQ = prove
 140  (`!f:real^M->real^N x V E.
 141     linear f /\ (!x y. f x = f y ==> x = y)
 142     ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
 143   REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
 144
 145 let FAN2_TRANSLATION_EQ = prove
 146  (`!a:real^N x V E.
 147         fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 148         fan2(x,V,E)`,
 149   REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
 150
 151 let FAN2_LINEAR_IMAGE_EQ = prove
 152  (`!f:real^M->real^N x V E.
 153     linear f /\ (!x y. f x = f y ==> x = y)
 154     ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
 155   REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
 156
 157 let FAN3_TRANSLATION_EQ = prove
 158  (`!a:real^N x V E.
 159         fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 160         fan3(x,V,E)`,
 161   REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
 162
 163 let FAN3_LINEAR_IMAGE_EQ = prove
 164  (`!f:real^M->real^N x V E.
 165     linear f /\ (!x y. f x = f y ==> x = y)
 166     ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
 167   let lemma = prove
 168    (`{w | {a,w} IN IMAGE (IMAGE f) s} =
 169      IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
 170     MATCH_MP_TAC(SET_RULE
 171      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
 172     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 173     MESON_TAC[]) in
 174   REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
 175
 176 let FAN4_TRANSLATION_EQ = prove
 177  (`!a:real^N x V E.
 178         fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 179         fan4(x,V,E)`,
 180   REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
 181
 182 let FAN4_LINEAR_IMAGE_EQ = prove
 183  (`!f:real^M->real^N x V E.
 184     linear f /\ (!x y. f x = f y ==> x = y)
 185     ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
 186   REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
 187
 188 let FAN5_TRANSLATION_EQ = prove
 189  (`!a:real^N x V E.
 190         fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 191         fan5(x,V,E)`,
 192   REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
 193
 194 let FAN5_LINEAR_IMAGE_EQ = prove
 195  (`!f:real^M->real^N x V E.
 196     linear f /\ (!x y. f x = f y ==> x = y)
 197     ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
 198   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 199    [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
 200   GEOM_TRANSFORM_TAC[]);;
 201
 202 let FAN6_TRANSLATION_EQ = prove
 203  (`!a:real^N x V E.
 204         fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 205         fan6(x,V,E)`,
 206   REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
 207
 208 let FAN6_LINEAR_IMAGE_EQ = prove
 209  (`!f:real^M->real^N x V E.
 210     linear f /\ (!x y. f x = f y ==> x = y)
 211     ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
 212   REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
 213
 214 let FAN7_TRANSLATION_EQ = prove
 215  (`!a:real^N x V E.
 216         fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 217         fan7(x,V,E)`,
 218   REWRITE_TAC[fan7] THEN
 219   REWRITE_TAC[SET_RULE
 220    `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
 221   GEOM_TRANSLATE_TAC[]);;
 222
 223 let FAN7_LINEAR_IMAGE_EQ = prove
 224  (`!f:real^M->real^N x V E.
 225     linear f /\ (!x y. f x = f y ==> x = y)
 226     ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
 227   REWRITE_TAC[fan7; IN_UNION] THEN
 228   REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB;
 229               TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 230   GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
 231    [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 232   REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN
 233   GEOM_TRANSFORM_TAC[]);;
 234
 235 add_translation_invariants
 236  [GRAPH_TRANSLATION_EQ;
 237   FAN1_TRANSLATION_EQ;
 238   FAN2_TRANSLATION_EQ;
 239   FAN3_TRANSLATION_EQ;
 240   FAN4_TRANSLATION_EQ;
 241   FAN5_TRANSLATION_EQ;
 242   FAN6_TRANSLATION_EQ;
 243   FAN7_TRANSLATION_EQ];;
 244
 245 add_linear_invariants
 246  [GRAPH_LINEAR_IMAGE_EQ;
 247   FAN1_LINEAR_IMAGE_EQ;
 248   FAN2_LINEAR_IMAGE_EQ;
 249   FAN3_LINEAR_IMAGE_EQ;
 250   FAN4_LINEAR_IMAGE_EQ;
 251   FAN5_LINEAR_IMAGE_EQ;
 252   FAN6_LINEAR_IMAGE_EQ;
 253   FAN7_LINEAR_IMAGE_EQ];;
 254
 255 let FAN_TRANSLATION_EQ = prove
 256  (`!a:real^N x V E.
 257         FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
 258         FAN(x,V,E)`,
 259   REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
 260
 261 let FAN_LINEAR_IMAGE_EQ = prove
 262  (`!f:real^M->real^N x V E.
 263     linear f /\ (!x y. f x = f y ==> x = y)
 264     ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
 265   REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
 266
 267 add_translation_invariants [FAN_TRANSLATION_EQ];;
 268 add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
 269
 270 let BASE_POINT_FAN_TRANSLATION_EQ = prove
 271  (`!a x V E.
 272     base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) =
 273     a + base_point_fan(x,V,E)`,
 274   REWRITE_TAC[base_point_fan]);;
 275
 276 let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
 277  (`!f:real^M->real^N x V E.
 278         linear f
 279         ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) =
 280             f(base_point_fan(x,V,E))`,
 281   REWRITE_TAC[base_point_fan]);;
 282
 283 let SET_OF_EDGE_TRANSLATION_EQ = prove
 284  (`!a:real^N x V E.
 285         set_of_edge (a + x) (IMAGE (\x. a + x) V)
 286                     (IMAGE (IMAGE (\x. a + x)) E) =
 287         IMAGE (\x. a + x) (set_of_edge x V E)`,
 288   REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
 289
 290 let SET_OF_EDGE_LINEAR_IMAGE_EQ = prove
 291  (`!f:real^M->real^N x V E.
 292         linear f /\ (!x y. f x = f y ==> x = y)
 293         ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) =
 294             IMAGE f (set_of_edge x V E)`,
 295   let lemma = prove
 296    (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
 297      {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
 298     MATCH_MP_TAC(SET_RULE
 299      `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
 300     REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
 301     MESON_TAC[]) in
 302   REWRITE_TAC[set_of_edge; lemma] THEN
 303   GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
 304
 305 add_translation_invariants
 306  [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;
 307
 308 add_linear_invariants
 309  [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
 310
 311
 312
 313
 314 (*H2k hypermap*)
 315 (*let hk=new_definition`hk((D:A->bool),(f:A->A),(n:A->A),(e:A->A),(k:num)) <=>
 316
 317 CARD D = 2 * k /\ (f permutes D) /\ (n permutes D) /\ (e permutes D )
 318 /\ (e o n o f= I)
 319 /\ (?x:A y:A. (x IN D) /\ (y IN D) /\ (orbit_map (f:A->A)  (x) INTER orbit_map (f)  (y)={})
 320    /\ (D = orbit_map (f:A->A)  (x) UNION orbit_map (f)  (y))
 321 /\ (IMAGE n (orbit_map (f:A->A)  (x)))= orbit_map (f)  (y))`;;
 322 *)
 323
 324
 325
 326
 327
 328 (* ************************************************* *)
 329 (* Proof remark rem:fan *)
 330
 331 let set_edges_is_finite_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool).
 332 FAN(x,V,E)==> FINITE E`,
 333 REPEAT GEN_TAC
 334 THEN REWRITE_TAC[FAN;fan1;graph]
 335 THEN STRIP_TAC
 336 THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET)
 337 THEN RESA_TAC
 338 THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`)
 339 THEN RESA_TAC
 340   THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET)
 341 THEN ASM_SET_TAC[]);;
 342
 343
 344 let remark_fan1=prove(`!v w V E. (v IN V) /\ (w IN V) ==>((w IN set_of_edge v V E)<=>(v IN set_of_edge w V E))`,
 345 (let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
 346 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM]  THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
 347
 348 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)`,
 349 REPEAT GEN_TAC THEN DISCH_TAC
 350   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)
 351   THEN ASM_REWRITE_TAC[]
 352   THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
 353
 354 let properties_of_set_of_edge=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3.  UNIONS E SUBSET V
 355 ==>
 356 ({v,u} IN E <=> u IN set_of_edge v V E)`,
 357 REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
 358 THEN STRIP_TAC
 359  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
 360   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
 361 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.  FAN(x,V,E)
 362 ==>
 363 ({v,u} IN E <=> u IN set_of_edge v V E)`,
 364 REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
 365 THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC
 366  THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
 367   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
 368
 369
 370
 371 let properties_of_graph=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 372 FAN(x,V,E) /\{v,u} IN E==> v IN V`,
 373
 374 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
 375 REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC
 376   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC
 377 THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
 378
 379
 380
 381 let th3a12=prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,u} {v})`,
 382    (let th=prove(`{x,v,u}={x,v,u}`, SET_TAC[]) in
 383 REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN
 384 REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC
 385   THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
 386 THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
 387
 388
 389 let th3a=prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,v} {u})`,
 390    (let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
 391 REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN
 392 REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC
 393   THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
 394 THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
 395    let th3b=prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=v) `,
 396 REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM] THEN SET_TAC[]);;
 397 let th3b1=prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=u) `,
 398 (let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
 399 REWRITE_TAC[th;th3b]));;
 400
 401    let th3c= prove(`!x v u. ~ collinear {x,v,u} ==> ~(u IN aff {x,v})`,
 402 REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_NOT
 403 THEN REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM;COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM]
 404 THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ARITH `u'+v'= &1 <=> v'= &1 -u'`]
 405   THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 406 THEN REWRITE_TAC[VECTOR_ARITH`(u = u' % x + (&1 - u') % v) <=> (u - v = u' % (x-v))`] THEN SET_TAC[]);;
 407
 408
 409 let th3d=prove(`!x v u. ~(x=v)/\ ~(x=u) ==> DISJOINT {x} {v,u}`,
 410 SET_TAC[]);;
 411
 412 let th3=prove(`!x v u. ~ collinear {x,v,u} ==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,
 413 MESON_TAC[th3a;th3b;th3b1;th3c;th3d;th3a12]);;
 414
 415
 416 let collinear1_fan=prove(`!x v u. ~ collinear {x,u,v} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
 417 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
 418 REPEAT GEN_TAC THEN EQ_TAC
 419 THENL[
 420 MESON_TAC[th3;lem];
 421 REWRITE_TAC[SET_RULE`~(t1) /\ ~ t2<=> ~(t2\/ t1)`;COLLINEAR_3_EXPAND;aff; AFFINE_HULL_2;IN_ELIM_THM]
 422 THEN MATCH_MP_TAC MONO_NOT  THEN MATCH_MP_TAC MONO_OR THEN STRIP_TAC
 423 THENL[
 424 REWRITE_TAC[];
 425
 426 STRIP_TAC THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1- (u':real)` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]));;
 427
 428
 429 let collinear_fan=prove(`!x v u. ~ collinear {x,v,u} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
 430 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
 431 MESON_TAC[collinear1_fan;lem]));;
 432
 433   let th4=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 434 FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
 435 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[]);;
 436
 437 let remark4_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 438 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})`,
 439
 440 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]);;
 441
 442
 443 let collinears_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 444 FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
 445 MESON_TAC[remark4_fan;collinear_fan]);;
 446
 447 let remark1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
 448 FAN(x,V,E) ==>
 449 FINITE (set_of_edge v V E)
 450 /\({v,u} IN E <=> u IN set_of_edge v V E)/\
 451 ({v,u} IN E==>
 452 ~ collinear {x,v,u}/\
 453 ~ (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/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
 454 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]);;
 455
 456
 457
 458 (***************SIGMA_FAN*****************)
 459
 460
 461
 462 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)=
 463 (if (set_of_edge v V E = {u} ) then u
 464     else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 465 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
 466
 467
 468 (* This extends sigma to have a larger domain
 469    of R^3 rather than just V.  It is the
 470    identity outside V (compare the definition
 471    of `permutes` ).   *)
 472
 473
 474
 475
 476 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)=
 477 (if ~(u IN set_of_edge v V E ) then u
 478     else (sigma_fan x V E v u))`;;
 479
 480
 481
 482
 483
 484 let exists_sigma_fan=prove(`
 485 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 486 ~ (set_of_edge v V E= {u} )
 487 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 488 ==>
 489 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 490 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))
 491 `,
 492
 493 (let lemma = prove
 494    (`!X:real->bool.
 495           FINITE X /\ ~(X = {})
 496           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 497     MESON_TAC[INF_FINITE]) in
 498
 499
 500 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
 501
 502 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
 503 THENL[(*2*)
 504 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
 505
 506 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 507  ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
 508 THENL[(*3*)
 509 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
 510   THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
 511 THENL[(*4*)
 512 ASM_TAC THEN SET_TAC[];(*4*)
 513 ASM_TAC THEN SET_TAC[]](*4*);(*3*)
 514 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
 515 THENL[(*4*)
 516 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
 517
 518 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
 519 THENL[(*5*)
 520 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
 521 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))
 522   THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
 523   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
 524 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
 525
 526
 527 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
 528
 529
 530 let exists_inverse_sigma_fan_alt=prove(`
 531 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 532 ~ (set_of_edge v V E= {u} )
 533 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 534 ==>
 535 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 536 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <=  azim1 x v u w1)))
 537 `,
 538 (let lemma = prove
 539    (`!X:real->bool.
 540           FINITE X /\ ~(X = {})
 541           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 542     MESON_TAC[INF_FINITE]) in
 543 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
 544 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
 545 THENL[(*2*)
 546
 547 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
 548 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 549  ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
 550 THENL[(*3*)
 551 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
 552   THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
 553 THENL[(*4*)
 554 ASM_TAC THEN SET_TAC[];(*4*)
 555 ASM_TAC THEN SET_TAC[](*4*)];
 556
 557 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
 558 THENL[(*4*)
 559 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
 560 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
 561 THENL[(*5*)
 562 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
 563 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))
 564   THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
 565 THEN EXISTS_TAC`x':real^3`
 566   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
 567 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
 568
 569
 570
 571
 572
 573
 574
 575
 576 let SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 577 ~ (set_of_edge v V E= {u} )
 578 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 579 ==>
 580 ((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\
 581 (!(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)`,
 582
 583 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan]
 584   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[]);;
 585
 586
 587
 588
 589 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).
 590 FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 591 ==>
 592 ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
 593
 594 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} )`)
 595 THENL[
 596  MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
 597 THEN ASM_TAC
 598 THEN SET_TAC[];
 599 ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
 600
 601
 602
 603
 604 let AFF_GE_2_1 = prove
 605  (`!x v w.
 606         DISJOINT {x,v} {w}
 607         ==> aff_ge {x,v} {w} =
 608              {y | ?t1 t2 t3.
 609                      &0 <= t3 /\
 610                      t1 + t2 + t3 = &1 /\
 611                      y = t1 % x + t2 % v + t3 % w}`,
 612   AFF_TAC);;
 613
 614 let AFF_GE_1_2 = prove
 615  (`!x v w.
 616         DISJOINT {x} {v,w}
 617         ==> aff_ge {x} {v,w} =
 618              {y | ?t1 t2 t3.
 619                      &0 <= t2 /\ &0 <= t3 /\
 620                      t1 + t2 + t3 = &1 /\
 621                      y = t1 % x + t2 % v + t3 % w}`,
 622   AFF_TAC);;
 623 let AFF_GE_1_1 = prove
 624  (`!x v w.
 625         DISJOINT {x} {v}
 626         ==> aff_ge {x} {v} =
 627              {y | ?t1 t2.
 628                      &0 <= t2 /\
 629                      t1 + t2 = &1 /\
 630                      y = t1 % x + t2 % v }`,
 631   AFF_TAC);;
 632
 633
 634
 635
 636 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.
 637 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\
 638  ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v})
 639 ==> u=w`,
 640 REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC
 641   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 642   THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC
 643   THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th))
 644   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
 645   THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`)
 646 THENL
 647 [  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[];
 648 ASM_TAC THEN SET_TAC[]]);;
 649
 650
 651
 652
 653
 654
 655
 656
 657
 658 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.
 659 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u}
 660 ==> u=w`,
 661 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN
 662 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`
 663            THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC)
 664            THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
 665            THEN DISCH_TAC THEN  DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
 666            THEN DISCH_THEN (LABEL_TAC "a")
 667            THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
 668 THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 669   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th))
 670   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
 671            THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c")
 672            THEN DISCH_TAC THEN DISCH_TAC
 673   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 674   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 675            THEN DISCH_TAC THEN DISCH_TAC
 676   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
 677            THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
 678            THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC
 679 THENL (*1*)[
 680 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_1)
 681 THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`)
 682   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 683   THEN ASM_REWRITE_TAC[]
 684   THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*)
 685
 686 SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC
 687 THENL (*2*)[
 688 ASM_TAC THEN SET_TAC[];(*2*)
 689
 690 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`)
 691 THENL (*3*)[
 692  SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
 693 THENL (*4*)[
 694  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
 695    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 696 THEN EXISTS_TAC `t1:real`
 697   THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[]
 698     THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*)
 699
 700  SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
 701 THENL (*5*)[
 702  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
 703    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 704 THEN EXISTS_TAC `&0:real`
 705   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*)
 706
 707 ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*)
 708
 709  SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
 710 THENL (*4*)[
 711  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
 712    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 713 THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))`
 714   THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)`
 715 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
 716 THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 717 THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN
 718 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
 719 MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH`
 720  (inv t3 * --t1) % x +
 721  (inv t3 * --t2) % v +
 722  inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u `
 723 ] THEN DISCH_TAC
 724 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*)
 725
 726  SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
 727 THENL (*5*)[
 728  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
 729    THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 730 THEN EXISTS_TAC `&0:real`
 731   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*)
 732 ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;
 733
 734
 735 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.
 736 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)
 737 ==> w=w1`,
 738
 739 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
 740   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
 741   THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 742   THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 743   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}`]
 744   THEN REPEAT STRIP_TAC
 745   THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) THEN
 746 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 747 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[]      );;
 748
 749
 750 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.
 751 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0)
 752 ==> u=w`,
 753
 754 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
 755   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
 756   THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 757   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}`]
 758   THEN REPEAT STRIP_TAC
 759   THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) THEN
 760 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 761 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[]           );;
 762
 763
 764
 765
 766 let UNIQUE_SIGMA_FAN=prove(`
 767 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
 768 ~ (set_of_edge v V E= {u} )
 769 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
 770 /\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\
 771 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)
 772 ==> sigma_fan x V E v u=w)`,
 773
 774         (   let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
 775 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
 776 ==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
 777 ) in
 778
 779 ASSUME_TAC(th) THEN
 780 REPEAT GEN_TAC  THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN
 781 DISCH_TAC  THEN DISCH_THEN(LABEL_TAC "1")
 782   THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4")
 783   THEN DISCH_THEN(LABEL_TAC"a")
 784   THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
 785   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 786   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))
 787   THEN ASM_REWRITE_TAC[]
 788   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[]
 789   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
 790   THEN REPEAT DISCH_TAC
 791   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
 792 THENL[
 793 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 794 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))
 795 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 796 THEN
 797 REMOVE_THEN"1" MP_TAC
 798 THEN  REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
 799 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
 800   THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC
 801   THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
 802   THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
 803   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 804   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
 805   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))
 806   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
 807   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 )
 808   THEN ASM_REWRITE_TAC[]
 809   THEN ASM_MESON_TAC[]]));;
 810
 811
 812 let CYCLIC_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
 813 FAN(x,V,E) /\ v IN V
 814 ==> cyclic_set (set_of_edge v V E) x v`,
 815 REPEAT GEN_TAC
 816 THEN STRIP_TAC
 817 THEN REPEAT (POP_ASSUM MP_TAC)
 818 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th)
 819 THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC
 820   THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*)
 821 STRIP_TAC
 822   THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*)
 823  STRIP_TAC THENL(*3*)[
 824
 825 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
 826 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 827   DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
 828 THEN STRIP_TAC THEN STRIP_TAC THEN
 829 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th))
 830   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th))
 831   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
 832   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 833   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[]
 834   THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 835   THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 836   THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
 837   THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC
 838
 839 THENL (*4*)[
 840  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
 841            THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
 842    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*)
 843
 844 ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*)
 845
 846 REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC
 847 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})`
 848 ASSUME_TAC
 849 THENL(*4*)[
 850 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
 851 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 852   DISCH_THEN(LABEL_TAC "a") THEN   DISCH_THEN(LABEL_TAC "b")
 853 THEN STRIP_TAC THEN STRIP_TAC THEN
 854 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) )
 855   THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC
 856   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*)
 857
 858 EQ_TAC THENL(*5*)[
 859
 860 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*)
 861
 862 ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
 863
 864
 865 let subset_cyclic_set_fan=prove(`!x:real^3 v:real^3 V:real^3->bool W:real^3->bool.
 866 V SUBSET W /\ cyclic_set W x v ==> cyclic_set V x v`,
 867
 868 REPEAT GEN_TAC THEN REWRITE_TAC[cyclic_set] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]
 869   THEN MP_TAC(ISPECL[`V:real^3->bool`;`W:real^3->bool`]FINITE_SUBSET) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN SET_TAC[]);;
 870
 871
 872
 873 let property_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 874  cyclic_set {u, w1, w2} x v
 875 ==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x}`,
 876
 877 (let th= prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 878 x IN {x,w1,w2}`, SET_TAC[]) in
 879
 880 (let th1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 881 x IN  affine hull {x,v}
 882 `,REPEAT GEN_TAC THEN REWRITE_TAC[AFFINE_HULL_2;INTER; IN_ELIM_THM] THEN EXISTS_TAC`&1` THEN EXISTS_TAC `&0` THEN
 883  MESON_TAC[REAL_ARITH`&1+ &0= &1`; VECTOR_ARITH`x= &1 % x + &0 % v`])
 884 in
 885
 886 (let th2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 887 x IN {x,w1,w2} INTER affine hull {x,v}
 888 `, REWRITE_TAC[INTER;IN_ELIM_THM] THEN REWRITE_TAC[th;th1]) in
 889
 890
 891 REPEAT GEN_TAC THEN
 892 REWRITE_TAC[COLLINEAR_LEMMA;DE_MORGAN_THM;VECTOR_ARITH`a-b=vec 0 <=> a=b`;cyclic_set;] THEN STRIP_TAC
 893   THEN ASM_REWRITE_TAC[VECTOR_ARITH`(v:real^3)=(x:real^3) <=> x=v`] THEN STRIP_TAC
 894 THENL[ STRIP_TAC  THEN
 895   POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")  THEN DISCH_TAC
 896 THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];
 897
 898 STRIP_TAC THENL[
 899
 900 STRIP_TAC  THEN
 901   POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")  THEN DISCH_TAC
 902 THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];
 903
 904 STRIP_TAC
 905 THEN POP_ASSUM MP_TAC
 906 THEN POP_ASSUM MP_TAC
 907 THEN DISCH_THEN(LABEL_TAC"a")
 908 THEN DISCH_TAC
 909 THEN REMOVE_THEN "a" MP_TAC
 910 THEN POP_ASSUM MP_TAC
 911 THEN REWRITE_TAC[VECTOR_ARITH`(c:real) % ((v:real^3)-(x:real^3))=(u:real^3)-x <=> u =  (&1 - c) % x+c % v`]
 912 THEN DISCH_TAC
 913 THEN SUBGOAL_THEN `(u:real^3) IN affine hull {(x:real^3),(v:real^3)}` ASSUME_TAC
 914 THENL[
 915 REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM]
 916 THEN EXISTS_TAC `&1 - (c:real)`
 917 THEN EXISTS_TAC`c:real`
 918 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - (c:real) +c= &1`;];
 919
 920 MP_TAC(ISPECL[`u:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`]th)
 921 THEN DISCH_TAC
 922 THEN ASM_TAC
 923 THEN SET_TAC[INTER]
 924 ]]]))));;
 925
 926
 927 let property_of_cyclic_set1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 928  cyclic_set {u, w1, w2} x v ==> ~collinear {x, v, w1}`,
 929
 930 (let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in
 931
 932 REPEAT GEN_TAC THEN DISCH_TAC
 933 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`;`u:real^3`; `w2:real^3`] property_of_cyclic_set) THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_3]));;
 934
 935 let property_of_cyclic_set2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 936  cyclic_set {u, w1, w2} x v
 937 ==> ~collinear {x, v, w2}`,
 938 ( let th=prove(`{u,w1,w2}={w2,w1,u}`,SET_TAC[]) in
 939 ( let th1=prove(`{u,w1,w2}={w1,w2,u}`,SET_TAC[]) in
 940
 941 REPEAT GEN_TAC THEN DISCH_TAC
 942 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w2:real^3`;`w1:real^3`; `u:real^3`] property_of_cyclic_set)
 943 THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[th1;COLLINEAR_3])));;
 944
 945 let property_of_cyclic_set3=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 946  cyclic_set {u, w1, w2} x v
 947 ==> ~ collinear {x, v, u}`,
 948 ( let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in
 949
 950 REPEAT GEN_TAC THEN DISCH_TAC
 951 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
 952 THEN ASM_REWRITE_TAC[]
 953 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_MESON_TAC[COLLINEAR_3;th]));;
 954
 955
 956
 957 let properties_of_cyclic_set=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
 958  cyclic_set {u, w1, w2} x v
 959 ==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x}
 960 /\ ~collinear {x, v, u}
 961 /\ ~collinear {x, v, w1}
 962 /\  ~collinear {x, v, w2}`,
 963
 964 MESON_TAC[property_of_cyclic_set;property_of_cyclic_set2;property_of_cyclic_set1;property_of_cyclic_set3]);;
 965
 966
 967
 968 let XOHLED=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
 969 FAN(x,V,E) /\ v IN V
 970 ==> cyclic_set (set_of_edge v V E) x v`,
 971 MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
 972
 973
 974
 975
 976 let d1_fan =new_definition`
 977 d1_fan (x,V,E) ={(x':real^3,v:real^3,w:real^3,w1:real^3)| (x'=x) /\ ({v,w} IN  E)/\ (w1 = sigma_fan x V E v w)}`;;
 978
 979 (* d2_fan not yet used *)
 980
 981 let d2_fan=new_definition`d2_fan (x,V,E)={ (x',v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
 982
 983
 984 let inverse_sigma_fan_alt=new_definition`inverse_sigma_fan_alt x V E v w = @a. sigma_fan x V E v a=w`;;
 985
 986 let e_fan=new_definition` e_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,v,(sigma_fan x V E w v)))`;;
 987
 988
 989 let f_fan=new_definition`f_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse_sigma_fan_alt x V E w v),v) )`;;
 990
 991
 992
 993 let n_fan=new_definition`n_fan (x:real^3) V E =(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,(sigma_fan x V E v w),(sigma_fan x V E v (sigma_fan x V E v w))))`;;
 994
 995 (* i_fan corrects the 4th coordinate to be
 996    the dart *)
 997
 998 let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
 999
1000 let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
1001
1002 let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
1003
1004 let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
1005
1006 let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
1007
1008 (* if f = sigma, the power_map_points gives
1009    iterates of sigma (for fixed x v) *)
1010
1011
1012 let power_map_points= new_recursive_definition num_RECURSION `(power_map_points f x V E v w 0 = w)/\(power_map_points f x V E v w  (SUC n)= f x V E v (power_map_points f x V E v w n))`;;
1013
1014 (* This is the composition operator (o),
1015    specialized to functions on 4-tuples *)
1016
1017 let o_funs=new_definition`!(f:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (g:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3). o_funs f g =(\(x:real^3,y:real^3,z:real^3,t:real^3).  f (pr1 (g(x,y,z,t)),pr2(g(x,y,z,t)),pr3(g(x,y,z,t)),pr4(g(x,y,z,t))))`;;
1018
1019 (* powers of permutations *)
1020
1021 let power_maps= new_recursive_definition num_RECURSION `(power_maps  (f:real^3->(real^3->bool)->((real^3->bool)->bool)->real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) 0 = i_fan (x:real^3) V E) /\ (power_maps f x V E (SUC n)= o_funs (f x V E)  (power_maps f x V E n))`;;
1022
1023
1024 (* powers of node map *)
1025
1026
1027
1028
1029 let power_n_fan= new_definition`power_n_fan x V E n=( \(x,v,w,w1). (x,v,(power_map_points sigma_fan x V E v w n),(power_map_points sigma_fan x V E v w (SUC n))))`;;
1030
1031
1032 (* the node of a dart, in a special form
1033    for fans *)
1034
1035
1036 let a_node_fan=new_definition`a_node_fan x V E (x,v,w,w1)={a | ?n. a=(power_maps  n_fan x V E n) (x,v,w,sigma_fan x V E v w)}`;;
1037
1038
1039 (* The set X(V,E) *)
1040
1041 let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
1042
1043 (* See comment by AS in fan_defs.hl.  The correct definition is there. *)
1044 let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;
1045
1046
1047 (*
1048 W^0_{dart}(x,v,w...)
1049 *)
1050
1051 let w_dart_fan=new_definition`w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3))=
1052 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
1053 else
1054 (if set_of_edge v  V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
1055 else (if set_of_edge v  V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065 let image_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
1066 FAN(x,V,E)  /\ (u IN set_of_edge v V E)
1067 ==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E`,
1068 INDUCT_TAC THEN
1069 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points]
1070 THENL[
1071 ASM_MESON_TAC[];
1072 REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
1073 THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`] th)) THEN
1074 ASM_REWRITE_TAC[] THEN DISCH_TAC
1075   THEN DISJ_CASES_TAC(SET_RULE `set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i}\/ ~(set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i})`)
1076 THENL[ASM_MESON_TAC[sigma_fan];
1077 ASM_MESON_TAC[SIGMA_FAN]]]);;
1078
1079
1080 let IN2_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
1081 FAN(x,V,E)  /\ ({v,u} IN E)
1082 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
1083 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
1084
1085 let IN1_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
1086 FAN(x,V,E)  /\ (u IN set_of_edge v V E)
1087 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
1088 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
1089
1090
1091 let remark_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
1092 FAN(x,V,E)  /\ ({v,u} IN E)
1093 ==>
1094 power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E
1095 /\ {v,power_map_points sigma_fan x V E v u i} IN E
1096 /\
1097  ~(collinear {x,v,power_map_points sigma_fan x V E v u i})
1098 /\ ~(x = power_map_points (sigma_fan) x V E v u i) /\
1099              ~(v = power_map_points (sigma_fan) x V E v u i) /\
1100              DISJOINT {x, v} {power_map_points (sigma_fan) x V E v u i} /\
1101              ~((power_map_points (sigma_fan) x V E v u i) IN aff {x, v}) /\
1102              DISJOINT {x} {v, (power_map_points (sigma_fan) x V E v u i)} `,
1103 MESON_TAC[IN2_ORBITS_FAN;remark1_fan;image_power_map_points;properties_of_set_of_edge_fan]);;
1104
1105
1106
1107
1108
1109
1110
1111 (*-------------------------------------------------------------------------------------------*)
1112 (*    the properties in normal vector                                                        *)
1113 (*-------------------------------------------------------------------------------------------*)
1114
1115 let imp_norm_not_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(norm ( v - x) = &0)`,
1116 REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(v:real^3)-(x:real^3)= vec 0` ASSUME_TAC THENL
1117                    [POP_ASSUM MP_TAC THEN MESON_TAC[NORM_EQ_0];
1118                     SUBGOAL_THEN `(v:real^3) = (x:real^3)` ASSUME_TAC THENL
1119                      [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;
1120                      ASM_TAC THEN SET_TAC[]]]);;
1121
1122
1123 let imp_norm_gl_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) > &0`,
1124 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
1125   [ASM_MESON_TAC[imp_norm_not_zero_fan];
1126    MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN
1127    SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL
1128      [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1129       MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC
1130 THEN REAL_ARITH_TAC]]);;
1131
1132
1133 let imp_inv_norm_not_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(inv(norm ( v - x)) = &0)`,
1134 REPEAT GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `inv(norm ((v:real^3) - (x:real^3))) > &0` ASSUME_TAC
1135 THENL
1136   [ASM_MESON_TAC[imp_norm_gl_zero_fan];
1137    POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]);;
1138
1139
1140 let imp_norm_ge_zero_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) >= &0`,
1141 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL
1142   [ASM_MESON_TAC[imp_norm_not_zero_fan];
1143    MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN
1144    SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL
1145      [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1146       MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
1147
1148 let norm_of_normal_vector_is_unit_fan=prove(`!v:real^3 x:real^3. ~(v = x) ==> norm(inv(norm ( v - x))% (v-x))= &1`,
1149 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[NORM_MUL] THEN SUBGOAL_THEN ` inv(norm ( (v:real^3) - (x:real^3))) >= &0` ASSUME_TAC THENL[ ASM_MESON_TAC[imp_norm_ge_zero_fan];
1150                 SUBGOAL_THEN ` ~(norm ( (v:real^3) - (x:real^3))= &0)` ASSUME_TAC THENL
1151                    [ASM_MESON_TAC[imp_norm_not_zero_fan];
1152                     SUBGOAL_THEN ` abs(inv(norm ( (v:real^3) - (x:real^3))))= inv(norm ( (v:real^3) - (x:real^3)))` ASSUME_TAC THENL
1153                        [ASM_MESON_TAC[REAL_ABS_REFL;REAL_ARITH `(a:real)>= &0 <=> &0 <= a`; ];
1154                         MP_TAC(ISPEC `norm ( (v:real^3) - (x:real^3))` REAL_MUL_LINV)THEN ASM_REWRITE_TAC[]]]]);;
1155
1156
1157
1158 (*---------------------------------------------------------------------------------------*)
1159 (* the normal coordinate is the definiton of frame in flyspeck(above JBDNJJB)              *)
1160 (*---------------------------------------------------------------------------------------*)
1161
1162
1163 let e3_fan=new_definition`e3_fan  (x:real^3) (v:real^3) (u:real^3) = inv(norm((v:real^3)-(x:real^3))) % ((v:real^3)-(x:real^3))`;;
1164
1165
1166
1167
1168   let e2_fan=new_definition`e2_fan (x:real^3) (v:real^3) (u:real^3) = inv(norm((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3)))) % ((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))) `;;
1169
1170 let e1_fan=new_definition`e1_fan (x:real^3) (v:real^3) (u:real^3)=(e2_fan (x:real^3) (v:real^3) (u:real^3)) cross (e3_fan (x:real^3) (v:real^3) (u:real^3))`;;
1171
1172
1173
1174   let e3_mul_dist_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> dist (v,x) % e3_fan x v u = v - x`,
1175 REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan; dist; VECTOR_ARITH `(a:real) % (b:real)% (v:real^3)=(a*b)%v`] THEN
1176 MESON_TAC[imp_norm_not_zero_fan; REAL_MUL_RINV; VECTOR_ARITH `&1 %(v:real^3)=v`]);;
1177
1178 let norm_dot_fan=prove(`!x:real^3. norm x = &1 ==> x dot x = &1`,
1179  ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]);;
1180
1181
1182   let e3_is_normal_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> e3_fan x v u dot e3_fan x v u = &1`,
1183 REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan]THEN DISCH_TAC
1184 THEN SUBGOAL_THEN `norm(inv(norm((v:real^3)-(x:real^3))) %(v-x)) pow 2= &1 pow 2` ASSUME_TAC THENL
1185  [ASM_MESON_TAC[norm_of_normal_vector_is_unit_fan] ;
1186 ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]]);;
1187
1188   let e2_is_normal_fan= prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e2_fan x v u dot e2_fan x v u = &1`,
1189 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC
1190 THENL[
1191 POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL]
1192 THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan)
1193 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1194 MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP)
1195 THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ];
1196
1197 MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`] norm_of_normal_vector_is_unit_fan) THEN
1198 ASM_REWRITE_TAC[] THEN REWRITE_TAC[e2_fan; VECTOR_ARITH`(v:real^3)- vec 0 = v`] THEN MESON_TAC[norm_dot_fan]]);;
1199
1200   let e2_orthogonal_e3_fan=prove(`!x:real^3 v:real^3 u:real^3.
1201 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (e2_fan x v u) dot (e3_fan x v u)= &0`,
1202 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;] THEN VEC3_TAC);;
1203
1204
1205
1206   let e1_is_normal_fan=prove(`!x:real^3 v:real^3 u:real^3.
1207 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e1_fan x v u dot e1_fan x v u = &1`,
1208 REPEAT GEN_TAC THEN STRIP_TAC THEN
1209 REWRITE_TAC[e1_fan;DOT_CROSS] THEN
1210 MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_orthogonal_e3_fan)
1211 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1212 MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_is_normal_fan)
1213 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1214 MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e3_is_normal_fan)
1215 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
1216
1217   let e1_orthogonal_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1218 ==> (e1_fan x v u) dot (e3_fan x v u)= &0`,
1219 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;
1220
1221
1222   let e1_orthogonal_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1223 ==> (e1_fan x v u) dot (e2_fan x v u)= &0`,
1224 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;
1225
1226
1227   let e1_cross_e2_dot_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==>
1228 &0 < (e1_fan x v u cross e2_fan x v u) dot e3_fan x v u`,
1229 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;CROSS_TRIPLE]
1230 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e1_is_normal_fan)
1231 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[e1_fan] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
1232
1233
1234
1235   let orthonormal_e1_e2_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==>
1236 (orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u))`,
1237 REPEAT GEN_TAC THEN REWRITE_TAC[orthonormal] THEN DISCH_TAC THEN
1238 ASM_MESON_TAC[e1_is_normal_fan;e2_is_normal_fan;e3_is_normal_fan;e1_orthogonal_e2_fan;
1239 e1_orthogonal_e3_fan;e2_orthogonal_e3_fan;e1_cross_e2_dot_e3_fan]);;
1240
1241
1242
1243   let dot_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1244 ==> (u-x) dot e2_fan x v u = &0`,
1245 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
1246
1247 let vdot_e2_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1248 ==> (v-x) dot e2_fan x v u = &0`,
1249 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
1250
1251 let vcross_e3_fan=prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1252 ==>
1253 (v - x) cross (e3_fan x v u) = vec 0`,
1254
1255 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e3_fan;CROSS_RMUL;CROSS_REFL] THEN VECTOR_ARITH_TAC);;
1256
1257 let udot_e1_fan=prove(`!x:real^3 v:real^3 u:real^3.
1258 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1259 ==> &0 < (u - x) dot e1_fan x v u `,
1260 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan; e2_fan;CROSS_LMUL;DOT_RMUL;DOT_SYM;DOT_LMUL;CROSS_TRIPLE]
1261 THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC
1262 THENL[
1263 POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL]
1264 THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan)
1265 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1266 MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP)
1267 THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ];
1268 MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`]imp_norm_gl_zero_fan) THEN
1269 ASM_REWRITE_TAC[REAL_ARITH`(a:real)> &0 <=> &0 < (a:real)`;VECTOR_ARITH `(a:real^3)- vec 0=a`] THEN DISCH_TAC
1270   THEN MP_TAC(ISPEC `e3_fan (x:real^3) (v:real^3) (u:real^3) cross (u-x)`DOT_POS_LT) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_LT_MUL]]);;
1271
1272 let udot_e1_fan1=prove(`!x:real^3 v:real^3 u:real^3.
1273 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1274 ==> &0 <= (u - x) dot e1_fan x v u `,
1275 REPEAT GEN_TAC THEN STRIP_TAC THEN
1276 MP_TAC(ISPECL[`x:real^3` ;`v:real^3` ;`u:real^3`]udot_e1_fan) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
1277
1278 let vdot_e1_fan=prove(`!x:real^3 v:real^3 u:real^3.
1279 ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1280 ==>  (v - x) dot e1_fan x v u = &0`,
1281 REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN RES_TAC THEN SYM_ASSUM_TAC THEN
1282 REWRITE_TAC[DOT_SYM;DOT_LMUL] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e1_orthogonal_e3_fan) THEN RESA_TAC THEN
1283 REAL_ARITH_TAC);;
1284
1285
1286
1287
1288
1289
1290 let properties_coordinate=prove(`!x:real^3 v:real^3 u:real^3.
1291 ~(collinear {x, v, u})
1292 ==> (orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u))
1293 /\ dist (v,x) % e3_fan x v u = v - x
1294 /\ ((v - x) cross (e3_fan x v u) = vec 0)
1295 /\  (v-x) dot e2_fan x v u = &0
1296 /\ ((u-x) dot e2_fan x v u = &0)
1297 /\  &0 <= (u - x) dot e1_fan x v u
1298 /\ &0 < (u - x) dot e1_fan x v u
1299 /\ (v - x) dot e1_fan x v u = &0`,
1300 (       let lem=prove(`!a b c. {a,b,c}={b,a,c}`,SET_TAC[]) in
1301 REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3)
1302   THEN RED_TAC THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[lem;] THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3]
1303 THEN
1304 ASM_MESON_TAC[orthonormal_e1_e2_e3_fan;e3_mul_dist_fan; dot_e2_fan;vdot_e2_fan;vcross_e3_fan;udot_e1_fan;udot_e1_fan1;vdot_e1_fan]));;
1305
1306
1307 let module_of_vector =prove(`!x:real^3 v:real^3 u:real^3 w:real^3 r:real psi:real h:real.
1308  ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x})
1309 /\ (&0 < r) /\ (w=(r * cos psi) % e1_fan x v u + (r * sin psi) % e2_fan x v u + h % (v-x))
1310 ==>
1311 sqrt(((w cross (e3_fan x v u)) dot e1_fan x v u) pow 2 + ((w cross (e3_fan x v u)) dot e2_fan x v u) pow 2) = r`,
1312 REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;] THEN
1313 MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[]
1314   THEN DISCH_THEN (LABEL_TAC "a") THEN
1315 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)`;
1316 `e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1317   THEN ASM_REWRITE_TAC[]
1318 THEN MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]vcross_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1319   THEN ASM_REWRITE_TAC[]
1320 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]CROSS_SKEW)
1321   THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1322   THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_LZERO;DOT_LNEG]
1323   THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[orthonormal] THEN  DISCH_TAC THEN ASM_REWRITE_TAC[DOT_SYM]
1324   THEN REWRITE_TAC[REAL_ARITH `-- &0 = &0`; REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH `(a:real) * &1 = a`;
1325 REAL_ARITH `(a:real) + &0 = a`;REAL_ARITH `&0 + (a:real) = a`;REAL_POW_MUL; REAL_ARITH `-- &1 pow 2 = &1`;
1326 REAL_ARITH `(d:real) * (b:real) + d * (c:real) = d * ( b + c)`;SIN_CIRCLE; sqrt] THEN MATCH_MP_TAC SELECT_UNIQUE
1327 THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC
1328
1329            THENL[
1330               STRIP_TAC THEN SUBGOAL_THEN `((y:real) - (r:real))* (y + r) = &0` ASSUME_TAC
1331                THENL[
1332                  REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ARITH `((a:real)- (b:real)) * (c:real)= a *c - b * c`;
1333 REAL_ARITH`(y:real) * (r:real)= r * y`; REAL_ARITH `((a:real) +(b:real)) - ((b:real) + (c:real))= a - c`;
1334 REAL_ARITH `(a:real)- (c:real)= &0 <=> a = c`]
1335                    THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1336                  MP_TAC (ISPECL [`(y:real)- (r:real)`; `(y:real)+(r:real)` ]REAL_ENTIRE) THEN ASM_REWRITE_TAC[]
1337                    THEN STRIP_TAC
1338                    THENL
1339                      [POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1340                      REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]];
1341
1342              DISCH_TAC THEN ASM_REWRITE_TAC[]
1343                THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
1344
1345
1346
1347 (****************************************************************************)
1348 (*        some properties of azim in the orthonormal frame                  *)
1349 (****************************************************************************)
1350
1351 let collinear_imp_azim_is_rezo_fan=prove(
1352 `!x:real^3 v:real^3 u:real^3 y:real h1:real h2:real.
1353 ~(v = x) /\ ~(u = x) /\ ~collinear {x, v, u}
1354 /\ &0 <= y /\
1355  y < &2 * pi /\
1356  ( !e1:real^3 e2:real^3 e3:real^3.
1357           orthonormal e1 e2 e3 /\ dist (v,x) % e3 = v - x
1358           ==> (?psi:real r1:real r2:real.
1359                    u - x =
1360                    (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (v - x) /\
1361                    u - x =
1362                    (r2 * cos (psi + y)) % e1 +
1363                    (r2 * sin (psi + y)) % e2 +
1364                    h2 % (v - x) /\
1365                    &0 < r1 /\
1366                    &0 < r2))
1367  ==> y = &0`,
1368 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1369   THEN REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~collinear {vec 0, (v:real^3)-(x:real^3), (u:real^3)-x}` ASSUME_TAC
1370   THENL (*1*)[
1371     POP_ASSUM MP_TAC
1372       THEN MATCH_MP_TAC MONO_NOT
1373       THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`; `u:real^3`] COLLINEAR_3)
1374       THEN SUBGOAL_THEN `{(v:real^3),(x:real^3),(u:real^3)}={x,v,u}` ASSUME_TAC
1375       THENL[SET_TAC[]; ASM_REWRITE_TAC[] THEN SET_TAC[]]; (*1*)
1376    REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1377      THEN DISCH_THEN (LABEL_TAC "1") THEN DISCH_THEN (LABEL_TAC "2") THEN REWRITE_TAC[LEFT_IMP_FORALL_THM]
1378      THEN EXISTS_TAC `e1_fan (x:real^3) (v:real^3) (u:real^3)`
1379      THEN EXISTS_TAC `e2_fan (x:real^3) (v:real^3) (u:real^3)`
1380      THEN EXISTS_TAC `e3_fan (x:real^3) (v:real^3) (u:real^3)`
1381      THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[]
1382      THEN DISCH_TAC
1383      THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`;`u:real^3`] e3_mul_dist_fan)THEN ASM_REWRITE_TAC[]
1384      THEN DISCH_THEN(LABEL_TAC "AB") THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1385      THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r1:real`; `psi:real`; `h1:real`] module_of_vector)
1386      THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1387      THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r2:real`; `(psi:real)+(y:real)`; `h2:real`] module_of_vector)
1388      THEN ASM_REWRITE_TAC[]
1389      THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1390      THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1391      THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
1392      THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1393      THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC
1394      THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC th)
1395      THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `sin (psi:real)= &0` ASSUME_TAC
1396       THENL (*2*)[
1397         MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)
1398           THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1399           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1400           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1401           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan)
1402           THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1403           THEN ASM_REWRITE_TAC[]
1404           THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`;
1405                REAL_ARITH`(a:real) * &1= a`]
1406           THEN DISCH_TAC
1407           THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP)  THEN ASM_REWRITE_TAC[]
1408           THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; (*2*)
1409
1410
1411         POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1412           THEN POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC
1413           THEN DISCH_THEN (LABEL_TAC "a")   THEN DISCH_THEN (LABEL_TAC "b")
1414           THEN REPEAT (DISCH_TAC) THEN REMOVE_THEN "a" MP_TAC THEN REMOVE_THEN "b" MP_TAC
1415           THEN REWRITE_TAC[COS_ADD;SIN_ADD] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1416           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)
1417           THEN ASM_REWRITE_TAC[] THEN  REWRITE_TAC[DOT_LADD;DOT_LMUL]
1418           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1419           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1420           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan)
1421           THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1422           THEN ASM_REWRITE_TAC[]
1423           THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`&0 * (a:real) = &0`;
1424               REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; REAL_ARITH`(a:real) * &1= a`;REAL_ENTIRE]
1425           THEN ASM_REWRITE_TAC[]
1426           THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
1427           THEN STRIP_TAC
1428              THENL(*3*)[
1429                REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*3*)
1430                MP_TAC(ISPEC `psi:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;(*3*)
1431                MP_TAC(ISPEC `y:real` SIN_EQ_0) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM MP_TAC
1432                  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_TAC THEN REMOVE_THEN "1" MP_TAC
1433                  THEN REMOVE_THEN "2" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(PI_WORKS) THEN REPEAT STRIP_TAC
1434                  THEN MP_TAC(ISPECL [ `n:real`;`&2`;`pi:real`]REAL_LT_RCANCEL_IMP)
1435                  THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "4")
1436                  THEN MP_TAC(ISPECL [ `&0`;`n:real`;`pi:real`]REAL_LE_RCANCEL_IMP)
1437                  THEN REWRITE_TAC[REAL_ARITH`&0 * (a:real) = &0`]
1438                  THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "5")
1439                  THEN MP_TAC(ISPECL [`n:real`; `pi:real`]REAL_ENTIRE) THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1440                  THEN REMOVE_THEN "3" MP_TAC THEN REWRITE_TAC[integer]
1441                  THEN MP_TAC(ISPEC `n:real` REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1442                  THEN STRIP_TAC THEN REMOVE_THEN "4" MP_TAC THEN REMOVE_THEN "5" MP_TAC
1443                  THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
1444                  THEN MP_TAC(ISPECL [`0`; `n':num`]REAL_OF_NUM_LE) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1445                  THEN MP_TAC(ISPECL [`n':num`; `2`]REAL_OF_NUM_LT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1446                  THEN SUBGOAL_THEN `(n':num)= 0 \/ n' = 1` ASSUME_TAC
1447                     THENL (*4*)[
1448                       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*4*)
1449                       POP_ASSUM MP_TAC THEN STRIP_TAC
1450                         THENL(*5*)[
1451                           ASM_MESON_TAC[REAL_OF_NUM_EQ];(*5*)
1452                           POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1453                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1454                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1455                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1456                             THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC
1457                             THEN REMOVE_THEN "A" MP_TAC
1458                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1459                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1460                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1461                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1462                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1463                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1464                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1465
1466                             THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC
1467                             THEN REMOVE_THEN "A" MP_TAC
1468                             THEN POP_ASSUM MP_TAC
1469                             THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC
1470                             THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[]
1471                             THEN REWRITE_TAC[REAL_ARITH `&1 * (a:real)=a`]
1472                             THEN POP_ASSUM MP_TAC
1473                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1474                             THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1475                             THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC
1476                             THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[]
1477                             THEN REWRITE_TAC[SIN_PI;COS_PI; REAL_ARITH `(a:real)- &0 = a`; REAL_ARITH `(a:real) * &0= &0`;
1478                                 REAL_ARITH `(a:real) * -- &1= -- a`;
1479                                 VECTOR_ARITH `&0 % (v:real^3)= vec 0`; VECTOR_ARITH `(v:real^3)+ vec 0 + (w:real^3)= v+w`]
1480                             THEN REMOVE_THEN "AB" MP_TAC THEN DISCH_TAC
1481                             THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th)]) THEN DISCH_TAC
1482                             THEN SUBGOAL_THEN `(((r2:real) * --cos (psi:real)) % e1_fan (x:real^3) (v:real^3) (u:real^3) + (h2:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u =(((r2:real) * cos psi) % e1_fan x v u + (h1:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u` ASSUME_TAC
1483                             THENL (*6*)[
1484                               ASM_REWRITE_TAC[]; (*6*)
1485                               POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;]
1486                                 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_is_normal_fan)
1487                                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1488                                 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e3_fan)
1489                                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1490                                 THEN ASM_REWRITE_TAC[]
1491                                 THEN REWRITE_TAC[REAL_ARITH `(a:real) * &0 = &0`; REAL_ARITH `(a:real)+ &0=a`;
1492                                                  REAL_ARITH `(a:real) * &1 =a`;
1493                                                  REAL_ARITH `(a:real) *(-- b)= a * b <=> &2 * a * b = &0`]
1494                                 THEN DISCH_TAC
1495                                 THEN MP_TAC(ISPECL [`&2 * (r2:real)`; `cos (psi:real)`]REAL_ENTIRE)
1496                                 THEN REWRITE_TAC[REAL_ARITH `((a:real)*(b:real))*(c:real)=a * b * c`]
1497                                 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1498                                  THENL(*7*)[
1499                                    REPEAT(POP_ASSUM MP_TAC ) THEN REAL_ARITH_TAC;(*7*)
1500                                    MP_TAC( ISPEC `psi:real` SIN_CIRCLE)
1501                                      THEN ASM_REWRITE_TAC[]
1502                                      THEN REWRITE_TAC[REAL_ARITH `&0 pow 2= &0`; REAL_ARITH `&0 + &0 = &0`]
1503                                      THEN SET_TAC[](*7*)](*6*)](*5*)]]]]]);;
1504
1505
1506
1507
1508 let azim_is_zero_fan=prove(`!x:real^3 v:real^3 u:real^3.
1509 ~(v=x) /\ ~(u=x) /\ (~(collinear {x, v, u}))
1510 ==>
1511 azim (x:real^3) (v:real^3) (u:real^3) (u:real^3) = &0`,
1512 REPEAT GEN_TAC THEN STRIP_TAC THEN
1513 REWRITE_TAC[azim_def] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SELECT_UNIQUE
1514 THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC
1515 THENL[
1516   REPEAT STRIP_TAC
1517     THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `y:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan)
1518     THEN ASM_REWRITE_TAC[];
1519   DISCH_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1520     THENL[
1521       REAL_ARITH_TAC;
1522       STRIP_TAC
1523         THENL[
1524           ASSUME_TAC(PI_WORKS) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1525           MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `u:real^3`] AZIM_EXISTS)
1526             THEN ASM_REWRITE_TAC[]
1527             THEN STRIP_TAC
1528             THEN EXISTS_TAC `h1:real`
1529             THEN EXISTS_TAC `h2:real`
1530             THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `theta:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan)
1531             THEN ASM_REWRITE_TAC[]
1532             THEN POP_ASSUM MP_TAC
1533             THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b")
1534             THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[]]]]);;
1535
1536
1537 let SINCOS_PRINCIPAL_VALUE_FAN = prove(
1538 `!x:real. ?y:real. (&0<= y /\ y < &2* pi) /\ (sin(y) = sin(x) /\ cos(y) = cos(x))`,
1539   GEN_TAC THEN MP_TAC(SPECL [`x:real`] SINCOS_PRINCIPAL_VALUE) THEN STRIP_TAC THEN
1540 DISJ_CASES_TAC(REAL_ARITH`((y:real) < &0)\/ (&0 <= y)`) THENL
1541 [ EXISTS_TAC `(y:real)+ &2 * pi` THEN ASSUME_TAC(PI_POS)
1542 THEN ASM_REWRITE_TAC[SIN_PERIODIC;COS_PERIODIC] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
1543  EXISTS_TAC `(y:real)` THEN ASSUME_TAC(PI_POS)
1544 THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
1545
1546 let sin_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
1547   ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1
1548 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
1549 ==> sin psi = &0`,
1550 REPEAT GEN_TAC THEN STRIP_TAC THEN  MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)
1551           THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL]
1552           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1553           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1554           THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan)
1555           THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1556           THEN ASM_REWRITE_TAC[]
1557           THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`;
1558                REAL_ARITH`(a:real) * &1= a`]
1559           THEN DISCH_TAC
1560           THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP)  THEN ASM_REWRITE_TAC[]
1561           THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
1562
1563 let cos_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
1564   ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1
1565 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
1566 ==> cos psi = &1`,
1567 REPEAT GEN_TAC THEN STRIP_TAC
1568 THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)-(x:real^3)`; `r1:real`; `psi:real`; `h1:real`]module_of_vector) THEN ASM_REWRITE_TAC[] THEN
1569  POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
1570 THEN POP_ASSUM MP_TAC
1571   THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e1_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1572 THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e2_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1573  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1574   THEN
1575 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 )THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN STRIP_TAC THEN
1576 POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN
1577 POP_ASSUM (fun th-> REWRITE_TAC[CROSS_SKEW;th])
1578   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)THEN ASM_REWRITE_TAC[]
1579 THEN DISCH_TAC THEN MP_TAC(ISPECL[ `e2_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2 +(a:real)=a`] THEN
1580 MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] udot_e1_fan1) THEN ASM_REWRITE_TAC[DOT_LNEG;] THEN DISCH_TAC
1581   THEN  MP_TAC(ISPECL[ `e1_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN
1582 POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN REWRITE_TAC[POW_2_SQRT_ABS;REAL_ABS_NEG] THEN
1583  MP_TAC(ISPECL[ `((u:real^3)-(x:real^3)) dot e1_fan (x:real^3) (v:real^3)(u:real^3)`]
1584   REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1585   THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_TAC
1586 THEN
1587  MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `r1:real`; `psi:real`; `h1:real`] sin_of_u_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`
1588  (r1 * cos psi) % e1_fan x v u + (r1 * &0) % e2_fan x v u + h1 % (v - x)=
1589  (r1 * cos psi) % e1_fan x v u + h1 % (v - x)`] THEN DISCH_TAC THEN
1590   SUBGOAL_THEN`((u:real^3) - (x:real^3)) dot e1_fan x (v:real^3) u = (((r1:real) * cos (psi:real)) % e1_fan x v u + (h1:real) % (v - x)) dot e1_fan x v u` ASSUME_TAC
1591
1592 THENL[ASM_MESON_TAC[];
1593
1594 POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN POP_ASSUM MP_TAC THEN  MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN ASM_REWRITE_TAC[]
1595   THEN DISCH_TAC
1596 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
1597 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
1598 e1_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[]
1599   THEN DISCH_TAC THEN ASM_REWRITE_TAC[DOT_LMUL;DOT_SYM]
1600 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]
1601 e1_is_normal_fan) THEN ASM_REWRITE_TAC[]
1602   THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)* &1+ (b:real)*(c:real)* &0= a`] THEN REPEAT DISCH_TAC
1603   THEN MP_TAC(ISPECL[`&1`;`cos (psi:real)`; `r1:real`]REAL_EQ_LCANCEL_IMP) THEN REWRITE_TAC[REAL_ARITH`(a:real)* &1=a`; REAL_ARITH`&1 = (a:real) <=> a= &1`] THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
1604
1605
1606
1607
1608 let sincos_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
1609   ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1
1610 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
1611 ==>  sin psi = &0 /\ cos psi = &1`,
1612 MESON_TAC[cos_of_u_fan;sin_of_u_fan]);;
1613
1614
1615
1616
1617 let sincos1_of_u_fan=prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real.
1618   ~collinear {x,v,u} /\ &0 < r1
1619 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x)
1620 ==>  sin psi = &0 /\ cos psi = &1`,
1621
1622 REPEAT STRIP_TAC
1623 THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
1624 THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={U,X,V}`]
1625 THEN DISCH_TAC
1626 THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}`
1627 THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={V,X,U}`]
1628 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1629 THEN DISCH_TAC
1630 THEN MRESA_TAC th3[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]
1631 THEN MRESA_TAC sincos_of_u_fan[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`;`r1:real`; `psi:real`; `h1:real`])
1632 ;;
1633
1634
1635
1636
1637
1638 (****************************************************************************)
1639 (*        the conditions to add azim                  *)
1640 (****************************************************************************)
1641
1642
1643
1644
1645
1646 let sum1_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
1647  cyclic_set {u, w1, w2} x v /\ (azim x v u w1 + azim x v w1 w2) < &2 * pi
1648 ==>
1649 azim x v u w2 = azim x v u w1+ azim x v w1 w2
1650 `,
1651 ( let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
1652
1653
1654 REPEAT GEN_TAC THEN STRIP_TAC
1655 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
1656 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1657 THEN
1658 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1)
1659 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1660   THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2)
1661 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1662   THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
1663 DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
1664 THENL[ASM_MESON_TAC[th];
1665
1666 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim)
1667   THEN STRIP_TAC
1668 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1669   THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
1670 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1671 MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1672   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1673   THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
1674 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC
1675 THEN
1676 POP_ASSUM (fun th-> 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)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1677 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
1678   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
1679   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1680
1681 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
1682 `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)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
1683   THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
1684 THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
1685 `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)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE)
1686 THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1687 THENL[ ASM_MESON_TAC[REAL_LE_ADD];
1688
1689
1690 ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
1691      ]]));;
1692
1693
1694
1695
1696
1697
1698
1699 let sum3_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
1700 ((azim x v u w1 + azim x v w1 w2) < &2 * pi)
1701 /\
1702 (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
1703 /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
1704 /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
1705 ==>
1706 azim x v u w2 = azim x v u w1+ azim x v w1 w2
1707 `, (let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
1708  (let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in
1709
1710 REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a")
1711
1712 THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b")
1713
1714 THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
1715
1716 THEN USE_THEN "b" MP_TAC THEN
1717 GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
1718 THEN
1719 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1720 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim)
1721   THEN STRIP_TAC
1722 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1723   THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
1724 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1725 MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1726   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1727   THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
1728 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC
1729 THEN
1730 POP_ASSUM (fun th-> 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)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1731 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
1732   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
1733   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1734
1735 THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
1736 `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)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
1737   THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
1738 THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
1739 `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)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE)
1740 THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1741 THENL[
1742  ASM_MESON_TAC[REAL_LE_ADD];
1743
1744 ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]])));;
1745
1746
1747
1748 let sum2_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
1749  cyclic_set {u, w1, w2} x v /\ azim x v u w1 <= azim x v u w2
1750 ==>
1751 azim x v u w2 = azim x v u w1 + azim x v w1 w2
1752 `,
1753
1754 (let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
1755
1756 REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
1757 REPEAT GEN_TAC THEN STRIP_TAC
1758 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
1759 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1760 THEN
1761 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1)
1762 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1763   THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2)
1764 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1765   THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
1766 DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
1767 THENL[ASM_MESON_TAC[th];
1768 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim)
1769   THEN STRIP_TAC
1770 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1771 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC
1772 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1773 THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
1774 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1775 MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1776   THEN ASM_REWRITE_TAC[]
1777 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1778   THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
1779 THEN REPEAT STRIP_TAC
1780    THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1781   THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC
1782   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
1783   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1784 THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
1785   THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
1786   THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
1787   THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
1788   THEN REPEAT STRIP_TAC
1789   THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
1790 `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)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE)
1791 THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC
1792 THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0)
1793 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1794 THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 )
1795 THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]));;
1796
1797
1798
1799
1800 let sum4_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
1801  azim x v u w1 <= azim x v u w2
1802 /\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
1803 /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
1804 /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
1805
1806 ==>
1807 azim x v u w2 = azim x v u w1 + azim x v w1 w2
1808 `,(let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
1809 (let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in
1810
1811 REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
1812
1813 REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a1")
1814
1815 THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b1")
1816
1817 THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
1818
1819 THEN USE_THEN "b1" MP_TAC THEN
1820 GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
1821 THEN
1822 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1823 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim)
1824   THEN STRIP_TAC
1825 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1826 THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC
1827 THEN POP_ASSUM(MP_TAC o SPECL [`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)`])
1828 THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan)
1829 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1830 MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1831   THEN ASM_REWRITE_TAC[]
1832 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1833   THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
1834 THEN REPEAT STRIP_TAC
1835    THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1836   THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC
1837   THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
1838   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1839 THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
1840   THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
1841   THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
1842   THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
1843   THEN REPEAT STRIP_TAC
1844   THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
1845 `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)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE)
1846 THEN DISCH_TAC
1847 THEN POP_ASSUM MATCH_MP_TAC
1848 THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0)
1849 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1850 THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 )
1851 THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC
1852 )));;
1853
1854
1855
1856
1857 let sum5_azim_fan=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
1858   azim x v  w1 w2 <= azim x v u w2
1859 /\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)})
1860 /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)})
1861 /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)})
1862
1863 ==>
1864 azim x v u w2 = azim x v u w1 + azim x v w1 w2
1865 `,
1866 REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC"1") THEN REPEAT STRIP_TAC
1867   THEN DISJ_CASES_TAC(REAL_ARITH`(azim x v u w2)= &0 \/ ~(azim x v u w2 = &0)`)
1868 THENL(*1*)[
1869 SUBGOAL_THEN`azim x v w1 w2 = &0` ASSUME_TAC
1870 THENL(*2*)[
1871 REPEAT(POP_ASSUM MP_TAC) THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]azim) THEN REAL_ARITH_TAC;
1872 (*2*)
1873 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1874 THEN
1875 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1876 THEN
1877 SUBGOAL_THEN`azim x v w2 w1 = azim x v w2 u` ASSUME_TAC
1878 THENL(*3*)[ASM_MESON_TAC[];(*3*)
1879 REWRITE_TAC[REAL_ARITH`&0 = a + &0 <=> a= &0`] THEN
1880 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w2:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1881   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_0) THEN ASM_REWRITE_TAC[]]];
1882  DISJ_CASES_TAC(REAL_ARITH`(azim x v w1 w2)= &0 \/ ~(azim x v w1 w2 = &0)`)
1883 THENL(*4*)[
1884 ASM_REWRITE_TAC[REAL_ARITH`b = a + &0 <=> b= a`] THEN
1885 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[]THEN ASM_MESON_TAC[AZIM_EQ_ALT]  ;(*4*)
1886 REMOVE_THEN"1" MP_TAC THEN
1887 MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_COMPL
1888 ) THEN ASM_REWRITE_TAC[]
1889   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_COMPL
1890 ) THEN ASM_REWRITE_TAC[REAL_ARITH`a=b-c <=> c= b-a`] THEN DISCH_TAC THEN DISCH_TAC
1891   THEN ASM_REWRITE_TAC[REAL_ARITH`a-b=c+a-d<=> d=b+c`;REAL_ARITH`a-b<=a-d<=> d<=b`] THEN ASM_MESON_TAC[sum4_azim_fan]]
1892 ]);;
1893
1894
1895
1896
1897
1898
1899 (****************************************************************************)
1900 (*        sigma_fan is permutes                                            *)
1901 (****************************************************************************)
1902
1903
1904 let  SUR_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
1905 FAN(x,V,E) /\ ({v,u} IN E)
1906 ==> ?w.  {v,w} IN E /\sigma_fan x V E v w= u
1907 `,
1908 REPEAT GEN_TAC THEN STRIP_TAC
1909 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)})`)
1910 THENL(*1*)[
1911 EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*)
1912
1913 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
1914 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
1915 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[]
1916   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)
1917   THEN ASM_REWRITE_TAC[]
1918   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC
1919 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})`)
1920 THENL(*2*)[
1921 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*)
1922
1923 ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN
1924 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)`)
1925 THENL(*3*)[
1926 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC
1927 THENL(*4*)[
1928 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
1929  SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
1930 THENL(*5*)[
1931 ASM_TAC THEN SET_TAC[];(*5*)
1932 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
1933 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
1934 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
1935 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1936   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)
1937                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1938   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[]
1939   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC
1940   THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC
1941 THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
1942 POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN
1943 MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge)
1944 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
1945  THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
1946   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
1947   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th))
1948   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
1949   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
1950 THEN
1951   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)`)
1952 THENL(*7*)[
1953 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)
1954 THEN ASM_TAC THEN SET_TAC[];(*7*)
1955
1956   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)`)
1957 THENL(*8*)[
1958 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)
1959 THEN ASM_TAC THEN SET_TAC[];(*8*)
1960  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1961    THEN  MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1962    THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1963    THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3.  w1 IN set_of_edge v V E /\ ~(w1 = u)
1964            ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1`
1965  THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1966 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`)
1967 THENL(*9*)[
1968 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)`)
1969 THENL(*10*)[
1970 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*)
1971 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*)
1972 SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC
1973 THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*)
1974 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*);
1975 ASM_TAC THEN SET_TAC[]]]]);;
1976
1977
1978
1979
1980
1981
1982 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).
1983 FAN(x,V,E) /\ ({v,u} IN E)
1984 /\ ({v,w} IN E)/\
1985  (sigma_fan x V E v u= sigma_fan x V E v w)
1986 ==> u=w
1987 `,
1988 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1")
1989 THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6]
1990 THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN
1991 DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") THEN
1992 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
1993 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}))`)
1994 THENL(*1*)[
1995 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
1996 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[]
1997 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
1998 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th))
1999 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
2000 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th))
2001   THEN ASM_TAC THEN SET_TAC[];(*1*)
2002
2003 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}))`)
2004 THENL(*2*)[
2005
2006 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
2007 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[]
2008 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
2009 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th))
2010 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
2011 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th))
2012   THEN ASM_TAC THEN SET_TAC[];(*2*)
2013
2014
2015 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
2016   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2017 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
2018   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2019   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN)
2020 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2021   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th))
2022 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
2023 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2024   THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th))
2025   THEN ASM_REWRITE_TAC[]
2026 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)
2027 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
2028  THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
2029   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
2030   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))
2031   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
2032   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
2033 DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`)
2034
2035 THENL(*3*)[
2036 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
2037 THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*)
2038
2039 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
2040 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2041   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)
2042                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
2043   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
2044   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)`)
2045
2046 THENL(*5*)[
2047 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)
2048 THEN ASM_TAC THEN SET_TAC[];(*5*)
2049
2050 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)`)
2051
2052 THENL(*6*)[
2053
2054 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)
2055 THEN ASM_TAC THEN SET_TAC[];(*6*)
2056
2057   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)`)
2058
2059 THENL(*7*)[
2060 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)
2061 THEN ASM_TAC THEN SET_TAC[];(*7*)
2062
2063 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)
2064 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2065 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN
2066 ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC
2067 THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`]
2068   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
2069 (*7*)](*6*)](*5*)](*4*)];(*3*)
2070
2071 ASM_REWRITE_TAC[](*3*)]]]);;
2072
2073
2074
2075
2076 let permutes_sigma_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
2077 FAN(x,V,E) /\ ({v,u} IN E)
2078 ==>
2079 (extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
2080 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
2081 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`]remark_finite_fan1)
2082   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2083   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)
2084   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2085 THENL[
2086 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan];
2087 STRIP_TAC
2088 THENL[
2089 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)})`)
2090 THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING];
2091 ASM_MESON_TAC[SIGMA_FAN]];
2092 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC
2093   THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge)
2094   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2095 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge)
2096   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2097 ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;
2098
2099
2100
2101
2102
2103
2104 (****************************************************************************)
2105 (*        inverse of sigma_fan                                             *)
2106 (****************************************************************************)
2107
2108
2109
2110
2111
2112
2113
2114
2115
2116
2117
2118
2119
2120
2121 let exists_function_inverse_sigma_fan_alt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
2122 FAN(x,V,E) ==>
2123 (?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
2124 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
2125 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w))
2126 `,
2127 REPEAT STRIP_TAC THEN
2128 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
2129  ASM_REWRITE_TAC[] THEN DISCH_TAC
2130 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)
2131   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
2132  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
2133
2134 THEN
2135 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) THEN
2136  ASM_REWRITE_TAC[] THEN DISCH_TAC
2137 THEN
2138 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] SUR_SIGMA_FAN) THEN
2139  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
2140
2141 (*
2142 This is the same as inverse_sigma_fan_alt,
2143 but easier to use.
2144 *)
2145
2146
2147
2148 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)
2149 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
2150 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
2151
2152
2153
2154 let INVERSE1_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
2155 FAN(x,V,E) ==>
2156 ( (!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)
2157 /\ (!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)
2158 /\ (!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))`,
2159 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)
2160   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC  THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
2161
2162 (* This is the same as f_fan,
2163    but easier to use *)
2164
2165 let f1_fan=new_definition`f1_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse1_sigma_fan x V E w v),v) )`;;
2166
2167
2168 (* Proof Lemma 6.1 [AAUHTVE] *)
2169
2170 let node_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) n:num. power_maps n_fan x V E n=power_n_fan x V E n`,
2171 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[power_maps; n_fan; power_n_fan; power_map_points] THEN INDUCT_TAC THEN REWRITE_TAC[power_maps; power_map_points;i_fan;] THEN REWRITE_TAC[power_map_points; power_maps] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[n_fan;o_funs; pr1; pr2; pr3; pr4]);;
2172
2173
2174
2175
2176
2177 let EQ_PAIR_4=prove(`!a:real^3 b:real^3 c:real^3 d:real^3 a1:real^3 b1:real^3 c1:real^3 d:real^3.
2178 (a,b,c,d)=(a1,b1,c1,d1) <=> a=a1 /\ b=b1 /\ c=c1 /\ d=d1`,
2179 REPEAT GEN_TAC THEN EQ_TAC
2180 THENL[
2181 DISCH_TAC THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr1(a,b,c,d)=pr1(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr1]
2182   THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr2(a,b,c,d)=pr2(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr2] THEN
2183 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr3(a,b,c,d)=pr3(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr3] THEN
2184 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr4(a,b,c,d)=pr4(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr4] THEN ASM_REWRITE_TAC[]
2185   THEN SET_TAC[];
2186 SET_TAC[]]);;
2187
2188
2189
2190 let MONO_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2191 FAN(x,V,E)
2192 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)`,
2193
2194 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;EQ_PAIR_4]
2195   THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> REWRITE_TAC[])
2196   THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
2197   THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3` ]remark1_fan)
2198   THEN ASM_REWRITE_TAC[]
2199   THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w':real^3`;`v:real^3` ]remark1_fan)
2200   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MONO_SIGMA_FAN;]);;
2201
2202
2203 let SUR_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2204 FAN(x,V,E)
2205 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,
2206
2207 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
2208   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`] SUR_SIGMA_FAN)
2209   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2210   THEN EXISTS_TAC`(x:real^3,v:real^3,w':real^3,w:real^3)`
2211   THEN ASM_REWRITE_TAC[n_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3`
2212   THEN EXISTS_TAC`w':real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
2213
2214
2215
2216 let simp_inverse_sigma_fan_alt=prove(`!x V E v w.
2217 inverse_sigma_fan_alt x V E v w= inverse (sigma_fan x V E v) w`,
2218 REWRITE_TAC[inverse] THEN MESON_TAC[inverse_sigma_fan_alt]);;
2219
2220
2221
2222 let SUR_F1_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2223 FAN(x,V,E)
2224 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))`,
2225 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
2226   THEN EXISTS_TAC`(x:real^3,sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w, v:real^3,sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v)`
2227   THEN ASM_REWRITE_TAC[f_fan;EQ_PAIR_4;]
2228  THEN STRIP_TAC
2229 THENL[
2230 EXISTS_TAC`x:real^3` THEN EXISTS_TAC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w`
2231   THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v`
2232 THEN ASM_REWRITE_TAC[] THEN 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})`)
2233 THENL[
2234 REWRITE_TAC[sigma_fan;SET_RULE`{a,b}={b,a}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
2235 THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[])
2236 THEN POP_ASSUM (fun th-> REWRITE_TAC[th]);
2237
2238 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3`]remark1_fan)
2239   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2240 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`]SIGMA_FAN)
2241   THEN ASM_REWRITE_TAC[remark1_fan] THEN STRIP_TAC
2242   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`sigma_fan x V E v w:real^3`;`v:real^3`]remark1_fan)
2243   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2244   THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]];
2245
2246 REWRITE_TAC[f1_fan] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`]INVERSE1_SIGMA_FAN)
2247   THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th))
2248   THEN ASM_REWRITE_TAC[]]);;
2249
2250
2251
2252
2253
2254 let MONO_F1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2255 FAN(x,V,E)
2256 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)`,
2257 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;EQ_PAIR_4]
2258   THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
2259
2260
2261 let MONO_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2262 FAN(x,V,E)
2263 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)`,
2264 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;EQ_PAIR_4]
2265   THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
2266
2267
2268 let SUR_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2269 FAN(x,V,E)
2270 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,
2271
2272 REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN REPEAT STRIP_TAC
2273  THEN EXISTS_TAC`(x:real^3,w:real^3,v:real^3, sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v)`
2274 THEN ASM_REWRITE_TAC[e_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3`
2275   THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v`
2276 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]);;
2277
2278
2279
2280
2281
2282
2283 let permuters_of_enf_fan=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2284 FAN(x,V,E)
2285 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)
2286 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))
2287 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)
2288 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))
2289 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)
2290 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))
2291 `,MESON_TAC[MONO_N_FAN;SUR_N_FAN;MONO_F1_FAN;SUR_F1_FAN;MONO_E_FAN;SUR_E_FAN]);;
2292
2293
2294
2295
2296
2297
2298
2299
2300
2301 let condition_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
2302 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> e_fan x V E((n_fan x V E) (f1_fan x V E a))=a)`,
2303 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[f1_fan;n_fan; e_fan; EQ_PAIR_4]
2304   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`]INVERSE1_SIGMA_FAN)
2305   THEN ASM_REWRITE_TAC[]
2306   THEN STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[])
2307   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`v:real^3`th))
2308   THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]
2309   THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
2310
2311
2312
2313 let plain_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
2314 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==>
2315 (e_fan x V E)  (e_fan x V E a) =a)`,
2316 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]);;
2317
2318
2319 let e_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
2320 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))`,
2321 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]
2322  THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
2323   THEN ASM_MESON_TAC[]);;
2324
2325 let f_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
2326 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))`,
2327 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
2328 THEN ASM_REWRITE_TAC[f1_fan; EQ_PAIR_4]
2329 THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
2330   THEN ASM_MESON_TAC[]);;
2331
2332
2333
2334 (* from hypermap.hl *)
2335
2336 (******************************)
2337 parse_as_infix("POWER",(24,"right"));;
2338
2339 let POWER = new_recursive_definition num_RECURSION
2340  `(!(f:A->A). f POWER 0  = I) /\
2341   (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
2342
2343 let POWER_0 = prove(`!f:A->A. f POWER 0 = I`,
2344  REWRITE_TAC[POWER]);;
2345
2346 let POWER_1 = prove(`!f:A->A. f POWER 1 = f`,
2347  REWRITE_TAC[POWER; ONE; I_O_ID]);;
2348
2349 let POWER_2 = prove(`!f:A->A. f POWER 2 = f o f`,
2350  REWRITE_TAC[POWER; TWO; POWER_1]);;
2351
2352 let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;
2353 (**************************************************)
2354
2355 let POWER_RIGHT=prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
2356 INDUCT_TAC
2357 THENL[REWRITE_TAC[POWER;o_DEF; I_DEF];
2358 REWRITE_TAC[POWER;o_ASSOC] THEN GEN_TAC THEN POP_ASSUM(fun th -> MP_TAC(SPEC`f:A->A`th)) THEN DISCH_TAC
2359  THEN
2360 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;
2361
2362
2363
2364 let power_n_fan=prove(`!l:num x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 w:real^3.
2365 FAN(x,V,E)/\ ({v,w} IN E)==>
2366 (n_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) POWER l) (x,v,w,sigma_fan x V E v w)= (x,v, power_map_points sigma_fan x V E v w l, power_map_points sigma_fan x V E v w (SUC l) )`,
2367 INDUCT_TAC
2368 THENL[REWRITE_TAC[POWER; power_map_points;I_DEF];
2369 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT STRIP_TAC THEN
2370   REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;`(w:real^3)`]th))
2371 THEN ASM_REWRITE_TAC[POWER_RIGHT; o_DEF;]
2372 THEN DISCH_TAC THEN ASM_REWRITE_TAC[n_fan;power_map_points] ]);;
2373
2374
2375
2376 let distinct_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) .
2377 FAN(x,V,E)==> (!k:num l:num a. a IN d1_fan(x,V,E) ==>
2378 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)`,
2379 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
2380 ASM_REWRITE_TAC[o_DEF;e_fan]  THEN
2381 MP_TAC(ISPECL[`l:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
2382   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2383   THEN MP_TAC(ISPECL[`k:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` w:real^3`;` v:real^3`]power_n_fan)
2384   THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC
2385   THEN POP_ASSUM(fun th-> REWRITE_TAC[])   THEN POP_ASSUM(fun th-> REWRITE_TAC[])
2386   THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th))
2387   THEN ASM_REWRITE_TAC[power_map_points] THEN  POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]));;
2388
2389
2390
2391
2392 let edge_lie_different_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
2393 FAN(x,V,E)==> (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a)) `,
2394
2395 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
2396 ASM_REWRITE_TAC[e_fan]  THEN
2397 MP_TAC(ISPECL[`n:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
2398   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4]
2399   THEN STRIP_TAC
2400 THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
2401   THEN ASM_MESON_TAC[]);;
2402
2403
2404
2405
2406 (**********************)
2407
2408
2409 let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
2410
2411 let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
2412
2413 let hypermap_of_fanx = new_definition
2414   `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
2415     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
2416           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;
2417
2418
2419 let hypermap1_of_fanx = new_definition
2420   `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
2421     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
2422           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;
2423
2424
2425
2426
2427 let finite_d1_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2428 FAN(x,V,E) ==> FINITE (d1_fan (x,V,E))`,
2429 REPEAT GEN_TAC
2430 THEN DISCH_THEN(LABEL_TAC"EM")
2431 THEN USE_THEN "EM" MP_TAC
2432 THEN REWRITE_TAC[FAN;fan1]
2433 THEN STRIP_TAC
2434 THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2435 THEN MRESA_TAC FINITE_PRODUCT[`V:real^3->bool`;`V:real^3->bool`]
2436 THEN MRESA_TAC FINITE_IMAGE[`(\(a,b:real^3). (x,a,b,sigma_fan x V E a b))`;`{x,y | x IN (V:real^3->bool) /\ y IN V}`]
2437 THEN MATCH_MP_TAC FINITE_SUBSET
2438 THEN EXISTS_TAC`(IMAGE (\(a,b). x,a,b,sigma_fan x V E a b) {x,y | x IN V /\ y IN (V:real^3->bool)})`
2439 THEN ASM_REWRITE_TAC[IMAGE;IN_ELIM_THM;d1_fan;SUBSET]
2440 THEN REPEAT STRIP_TAC
2441 THEN EXISTS_TAC`(v:real^3,w:real^3)`
2442 THEN ASM_REWRITE_TAC[]
2443 THEN EXISTS_TAC`v:real^3`
2444 THEN EXISTS_TAC`w:real^3`
2445 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
2446 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`w:real^3`]
2447 THEN POP_ASSUM MP_TAC
2448 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2449 THEN ASM_REWRITE_TAC[]
2450 THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
2451
2452
2453
2454 let finite_d20_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2455 FAN(x,V,E) ==> FINITE (d20_fan (x,V,E))`,
2456
2457 REPEAT GEN_TAC
2458 THEN DISCH_THEN(LABEL_TAC"EM")
2459 THEN USE_THEN "EM" MP_TAC
2460 THEN REWRITE_TAC[FAN;fan1]
2461 THEN STRIP_TAC
2462 THEN MRESA_TAC FINITE_IMAGE[`(\b:real^3. (x:real^3,b,b,b))`;`V:real^3->bool`]
2463 THEN MATCH_MP_TAC FINITE_SUBSET
2464 THEN EXISTS_TAC`(IMAGE (\b:real^3. (x:real^3,b,b,b))  (V:real^3->bool))`
2465 THEN ASM_REWRITE_TAC[d20_fan;SUBSET;IMAGE;IN_ELIM_THM]
2466 THEN REPEAT STRIP_TAC
2467 THEN EXISTS_TAC`v:real^3`
2468 THEN ASM_REWRITE_TAC[IN]);;
2469
2470
2471
2472 let finite_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2473 FAN(x,V,E)
2474 ==> FINITE (d_fan (x,V,E))`,
2475 REPEAT STRIP_TAC
2476 THEN REWRITE_TAC[d_fan;FINITE_UNION]
2477 THEN STRIP_TAC
2478 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
2479
2480 let subset_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2481 d1_fan (x,V,E) SUBSET d_fan (x,V,E) /\ d20_fan (x,V,E) SUBSET d_fan(x,V,E)`,
2482 REWRITE_TAC[d_fan] THEN SET_TAC[]);;
2483
2484
2485 let FACE_FAN_NOT_EMPTY=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
2486 FAN(x,V,E)
2487 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
2488 ==> ~(ds={})`,
2489 REPEAT STRIP_TAC
2490 THEN POP_ASSUM MP_TAC
2491 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
2492 THEN MRESA_TAC FACE_FINITE[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
2493 THEN STRIP_TAC
2494 THEN MRESA1_TAC CARD_EQ_0`face (hypermap1_of_fanx (x:real^3,V,E)) x'`
2495 THEN MRESA_TAC FACE_NOT_EMPTY[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
2496 THEN POP_ASSUM MP_TAC
2497 THEN ARITH_TAC);;
2498
2499
2500
2501
2502
2503
2504
2505 let into_domain_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2506 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2507 ==> (!y. y IN d_fan (x,V,E)==> ((p e_fan ) y) IN (d_fan (x,V,E)))`,
2508 REPEAT STRIP_TAC
2509 THEN ASM_REWRITE_TAC[res;]
2510 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2511 THENL[
2512 ASM_REWRITE_TAC[];
2513
2514 ASM_REWRITE_TAC[]
2515 THEN POP_ASSUM MP_TAC
2516 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
2517 THEN STRIP_TAC
2518 THEN ASM_REWRITE_TAC[]
2519 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2520 THEN MATCH_MP_TAC(SET_RULE`x,w,v,sigma_fan x V E w v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
2521 ==>x,w,v,sigma_fan x V E w v IN  d_fan (x:real^3,V,E)`)
2522 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
2523 THEN EXISTS_TAC`x:real^3`
2524 THEN EXISTS_TAC`w:real^3`
2525 THEN EXISTS_TAC`v:real^3`
2526 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
2527 THEN ASM_REWRITE_TAC[]
2528 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2529 THEN ASM_REWRITE_TAC[]]);;
2530
2531
2532
2533
2534 let into_domain1_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2535 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (e_fan x V E y IN d1_fan (x,V,E)))`,
2536 REPEAT STRIP_TAC
2537 THEN POP_ASSUM MP_TAC
2538 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
2539 THEN STRIP_TAC
2540 THEN ASM_REWRITE_TAC[]
2541 THEN EXISTS_TAC`x:real^3`
2542 THEN EXISTS_TAC`w:real^3`
2543 THEN EXISTS_TAC`v:real^3`
2544 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
2545 THEN ASM_REWRITE_TAC[]
2546 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2547 THEN ASM_REWRITE_TAC[]);;
2548
2549
2550
2551
2552
2553 let e_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2554 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2555 ==> (p e_fan) permutes (d_fan (x,V,E))`,
2556 REPEAT STRIP_TAC
2557 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2558 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (e_fan x V E) (d1_fan (x:real^3,V,E))`]
2559 THEN STRIP_TAC
2560 THENL[
2561 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
2562 THEN REPEAT STRIP_TAC
2563 THEN ASM_REWRITE_TAC[];
2564
2565 MRESA_TAC into_domain_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2566 THEN REPEAT STRIP_TAC
2567 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2568 THENL[EXISTS_TAC`y:real^3#real^3#real^3#real^3`
2569 THEN ASM_REWRITE_TAC[res];
2570 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2571 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
2572 THEN REWRITE_TAC[res]
2573 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
2574 THEN ASM_REWRITE_TAC[]
2575 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2576 THEN ASM_TAC THEN SET_TAC[]]]);;
2577
2578 let into_domain_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2579 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2580 ==> (!y. y IN d_fan (x,V,E)==> ((p f1_fan ) y) IN (d_fan (x,V,E)))`,
2581 REPEAT STRIP_TAC
2582 THEN ASM_REWRITE_TAC[res;]
2583 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2584 THENL[
2585 ASM_REWRITE_TAC[];
2586 ASM_REWRITE_TAC[]
2587 THEN POP_ASSUM MP_TAC
2588 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
2589 THEN STRIP_TAC
2590 THEN ASM_REWRITE_TAC[]
2591 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2592 THEN MATCH_MP_TAC(SET_RULE`x,w,inverse1_sigma_fan x V E w v,v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
2593 ==>x,w,inverse1_sigma_fan x V E w v,v IN  d_fan (x:real^3,V,E)`)
2594 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
2595 THEN EXISTS_TAC`x:real^3`
2596 THEN EXISTS_TAC`w:real^3`
2597 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
2598 THEN EXISTS_TAC`(v:real^3)`
2599 THEN ASM_REWRITE_TAC[]
2600 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
2601 THEN REMOVE_ASSUM_TAC
2602 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2603 THEN POP_ASSUM MP_TAC
2604 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2605 THEN RESA_TAC
2606 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
2607 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2608 THEN POP_ASSUM MP_TAC
2609 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2610 THEN RESA_TAC
2611 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2612 THEN ASM_REWRITE_TAC[]]);;
2613
2614
2615
2616
2617 let into_domain1_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2618 FAN(x,V,E)==> (!y. y IN d1_fan (x,V,E)==> (f1_fan x V E y IN d1_fan (x,V,E)))`,
2619 REPEAT STRIP_TAC
2620 THEN ASM_REWRITE_TAC[]
2621 THEN POP_ASSUM MP_TAC
2622 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
2623 THEN STRIP_TAC
2624 THEN EXISTS_TAC`x:real^3`
2625 THEN EXISTS_TAC`w:real^3`
2626 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
2627 THEN EXISTS_TAC`(v:real^3)`
2628 THEN ASM_REWRITE_TAC[]
2629 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
2630 THEN REMOVE_ASSUM_TAC
2631 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2632 THEN POP_ASSUM MP_TAC
2633 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2634 THEN RESA_TAC
2635 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
2636 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2637 THEN POP_ASSUM MP_TAC
2638 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2639 THEN RESA_TAC
2640 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2641 THEN ASM_REWRITE_TAC[]);;
2642
2643
2644
2645
2646
2647 let f1_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2648 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2649 ==> (p f1_fan) permutes (d_fan (x,V,E))`,
2650
2651 REPEAT STRIP_TAC
2652 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2653 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (f1_fan x V E) (d1_fan (x:real^3,V,E))`]
2654 THEN STRIP_TAC
2655 THENL[
2656 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
2657 THEN REPEAT STRIP_TAC
2658 THEN ASM_REWRITE_TAC[];
2659 MRESA_TAC into_domain_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2660 THEN REPEAT STRIP_TAC
2661 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2662 THENL[
2663 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
2664 THEN ASM_REWRITE_TAC[res];
2665 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2666 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
2667 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
2668 THEN REWRITE_TAC[res]
2669 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
2670 THEN ASM_REWRITE_TAC[]
2671 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2672 THEN ASM_TAC THEN SET_TAC[]]]);;
2673
2674
2675
2676
2677
2678 let into_domain_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2679 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2680 ==> (!y. y IN d_fan (x,V,E)==> ((p n_fan ) y) IN (d_fan (x,V,E)))`,
2681 REPEAT STRIP_TAC
2682 THEN ASM_REWRITE_TAC[res;]
2683 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2684 THENL[
2685 ASM_REWRITE_TAC[];
2686 ASM_REWRITE_TAC[]
2687 THEN POP_ASSUM MP_TAC
2688 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
2689 THEN STRIP_TAC
2690 THEN ASM_REWRITE_TAC[]
2691 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2692 THEN MATCH_MP_TAC(SET_RULE`x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
2693 ==>x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN  d_fan (x:real^3,V,E)`)
2694 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
2695 THEN EXISTS_TAC`x:real^3`
2696 THEN EXISTS_TAC`v:real^3`
2697 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
2698 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
2699 THEN ASM_REWRITE_TAC[]
2700 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
2701 THEN POP_ASSUM MP_TAC
2702 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
2703 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]]);;
2704
2705
2706
2707 let into_domain1_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2708 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (n_fan x V E y IN d1_fan (x,V,E)))`,
2709 REPEAT STRIP_TAC
2710 THEN POP_ASSUM MP_TAC
2711 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
2712 THEN STRIP_TAC
2713 THEN ASM_REWRITE_TAC[]
2714 THEN EXISTS_TAC`x:real^3`
2715 THEN EXISTS_TAC`v:real^3`
2716 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
2717 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
2718 THEN ASM_REWRITE_TAC[]
2719 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
2720 THEN POP_ASSUM MP_TAC
2721 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
2722 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]);;
2723
2724
2725
2726 let n_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2727 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2728 ==> (p n_fan) permutes (d_fan (x,V,E))`,
2729
2730 REPEAT STRIP_TAC
2731 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2732 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (n_fan x V E) (d1_fan (x:real^3,V,E))`]
2733 THEN STRIP_TAC
2734 THENL[
2735 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
2736 THEN REPEAT STRIP_TAC
2737 THEN ASM_REWRITE_TAC[];
2738 MRESA_TAC into_domain_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2739 THEN REPEAT STRIP_TAC
2740 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
2741 THENL[
2742 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
2743 THEN ASM_REWRITE_TAC[res];
2744 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2745 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
2746 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
2747 THEN REWRITE_TAC[res]
2748 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
2749 THEN ASM_REWRITE_TAC[]
2750 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2751 THEN ASM_TAC THEN SET_TAC[]]]);;
2752
2753
2754 let id_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3.
2755 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
2756 ==> (p e_fan) y=y /\ (p n_fan) y=y/\ (p f1_fan) y=y`,
2757 REPEAT STRIP_TAC
2758 THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
2759
2760 let id_power_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3 n:num p.
2761 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
2762 ==> ((p e_fan) POWER n) y=y /\ ((p n_fan) POWER n)y=y/\ ((p f1_fan) POWER n) y=y`,
2763 (let lem=prove(`!f:A->A x:A. f x = x ==> !m. (f POWER m) x = x`,
2764 MRESA_TAC power_map_fix_point[`1:num`]
2765 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[POWER_1;ARITH_RULE`m*1=m:num`]) in
2766 REPEAT STRIP_TAC
2767 THEN MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`y:real^3#real^3#real^3#real^3`]
2768 THEN MRESA_TAC lem[`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
2769 THEN MRESA_TAC lem[`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
2770 THEN MRESA_TAC lem[`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]));;
2771
2772
2773
2774
2775 let into_domain_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2776 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2777 ==> (!y. y IN d1_fan (x,V,E)==> (p e_fan ) y = e_fan x V E y)
2778 /\ (!y. y IN d1_fan (x,V,E)==> (p n_fan ) y = n_fan x V E y)
2779 /\(!y. y IN d1_fan (x,V,E)==> (p f1_fan ) y = f1_fan x V E y)
2780 `,
2781 REPEAT STRIP_TAC
2782 THEN ASM_REWRITE_TAC[res;]);;
2783
2784
2785
2786
2787 let power_map_fix_set = prove(`!n f:A->A g:A->A s:A->bool. (!x:A. x IN s ==>  f x= g x) /\ (!x:A. x IN s ==> g x IN s) ==> (!x. x IN s==>(f POWER n) x = (g POWER n) x)`,
2788  INDUCT_TAC THENL[REWRITE_TAC[MULT; POWER; I_THM];
2789     REWRITE_TAC[POWER; o_DEF] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
2790 THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
2791 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_THEN(LABEL_TAC"NHO")  THEN DISCH_TAC
2792 THEN REMOVE_THEN "YEU" (fun th -> MRESA_TAC th[`f:A->A`;`g:A->A`;`s:A->bool`])
2793 THEN POP_ASSUM (fun th-> MRESA1_TAC th `g (x:A):A`)
2794 THEN POP_ASSUM MP_TAC
2795 THEN REMOVE_THEN "EM"  (fun th -> MRESA1_TAC th `x:A`)
2796 THEN REMOVE_THEN "NHO"  (fun th -> MRESA1_TAC th `x:A`)]);;
2797
2798
2799
2800
2801
2802
2803 let into_domain_power_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num p.
2804 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
2805 ==> (!y. y IN d1_fan (x,V,E)==> ((p e_fan ) POWER n)y = ((e_fan x V E) POWER n) y)
2806 /\ (!y. y IN d1_fan (x,V,E)==> ((p n_fan ) POWER n) y = ((n_fan x V E) POWER n) y)
2807 /\(!y. y IN d1_fan (x,V,E)==> ((p f1_fan ) POWER n) y = ((f1_fan x V E) POWER n) y)`,
2808 REPEAT GEN_TAC THEN REPEAT DISCH_TAC
2809 THEN MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2810 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2811 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2812 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2813 THEN MRESA_TAC power_map_fix_set[`n:num`;
2814 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
2815 `(e_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
2816 THEN MRESA_TAC power_map_fix_set[`n:num`;
2817 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
2818 `(n_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
2819 THEN MRESA_TAC power_map_fix_set[`n:num`;
2820 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
2821 `(f1_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]);;
2822
2823
2824
2825
2826 let power_fun_in_domain=prove(`!n f:A->A s:A->bool.(!y. y IN s==> f y IN s)==> (!y. y IN s==> (f POWER n) y IN s)`,
2827  INDUCT_TAC THENL[REWRITE_TAC[POWER_0; I_THM];
2828 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
2829 THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`f:A->A`;`s:A->bool`])
2830 THEN REWRITE_TAC[COM_POWER;o_DEF]
2831 THEN POP_ASSUM  (fun th-> MRESA1_TAC th`y:A`)]);;
2832
2833
2834
2835 let into_domain1_power_efn_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num.
2836 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (((e_fan x V E) POWER n) y IN d1_fan (x,V,E)))
2837 /\ (!y. y IN d1_fan (x,V,E)==> (((n_fan x V E) POWER n) y IN d1_fan (x,V,E)))
2838 /\(!y. y IN d1_fan (x,V,E)==> (((f1_fan x V E) POWER n) y IN d1_fan (x,V,E)))`,
2839 REPEAT GEN_TAC THEN DISCH_TAC
2840 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
2841 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
2842 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
2843 THEN MRESA_TAC power_fun_in_domain[`n:num`;`e_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
2844 THEN MRESA_TAC power_fun_in_domain[`n:num`;`f1_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
2845 THEN MRESA_TAC power_fun_in_domain[`n:num`;`n_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]);;
2846
2847
2848
2849
2850
2851
2852 let lemma_hypermap1_of_fanx=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2853 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
2854 (p e_fan) o (p n_fan) o (p f1_fan)= I`,
2855 REPEAT STRIP_TAC
2856 THEN MATCH_MP_TAC EQ_EXT
2857 THEN ASM_REWRITE_TAC[I_THM;o_DEF]
2858 THEN GEN_TAC
2859 THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
2860 THENL[
2861 MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x':real^3#real^3#real^3#real^3`];
2862 MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2863 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
2864 THEN REMOVE_ASSUM_TAC
2865 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
2866 THEN POP_ASSUM MP_TAC
2867 THEN POP_ASSUM MP_TAC
2868 THEN DISCH_THEN (LABEL_TAC"YEU")
2869 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2870 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
2871 THEN RESA_TAC
2872 THEN REMOVE_ASSUM_TAC
2873 THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `(n_fan x V E (f1_fan x V E x')):real^3#real^3#real^3#real^3` )
2874 THEN POP_ASSUM MP_TAC
2875 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2876 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
2877 THEN RESA_TAC
2878 THEN MRESA_TAC condition_hypermap_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
2879 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )]);;
2880
2881
2882
2883
2884
2885
2886
2887
2888
2889 let hypermap_of_fan_rep=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) p.
2890 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
2891 dart ( hypermap1_of_fanx (x,V,E)) =d_fan (x,V,E)  /\ edge_map (hypermap1_of_fanx (x,V,E)) = p e_fan  /\ node_map (hypermap1_of_fanx (x,V,E)) = p n_fan /\ face_map (hypermap1_of_fanx (x,V,E)) = p f1_fan `,
2892 REPEAT GEN_TAC THEN DISCH_TAC
2893 THEN REWRITE_TAC[hypermap1_of_fanx]
2894 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
2895 THEN ASM_REWRITE_TAC[]
2896 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
2897 THEN MRESA_TAC e_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
2898 THEN MRESA_TAC n_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
2899 THEN MRESA_TAC f1_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
2900 THEN MRESA_TAC lemma_hypermap1_of_fanx[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
2901 THEN MRESA_TAC lemma_hypermap_rep[`d_fan (x:real^3,V,E):real^3#real^3#real^3#real^3->bool`;
2902 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
2903 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
2904 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`]);;
2905
2906 let properties_of_f1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y y1.
2907 FAN(x,V,E) /\ y = f1_fan x V E y1 /\ y1 IN d1_fan (x,V,E)
2908 ==> pr3 y1 =pr2 y /\ {pr2 y1, pr3 y1} IN E /\ {pr2 y, pr3 y} IN E /\
2909 pr2 y1= sigma_fan x V E (pr2 y) (pr3 y)`,
2910 REPEAT GEN_TAC
2911 THEN STRIP_TAC
2912 THEN POP_ASSUM MP_TAC
2913 THEN REWRITE_TAC[d1_fan; IN_ELIM_THM]
2914 THEN STRIP_TAC
2915 THEN ASM_REWRITE_TAC[pr2;pr3;f1_fan]
2916 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`w:real^3`]
2917 THEN REMOVE_ASSUM_TAC
2918 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2919 THEN POP_ASSUM MP_TAC
2920 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2921 THEN RESA_TAC
2922 THEN REMOVE_ASSUM_TAC
2923 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
2924 THEN POP_ASSUM MP_TAC
2925 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2926 THEN RESA_TAC
2927 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2928 THEN ASM_REWRITE_TAC[]);;
2929
2930
2931
2932 let face_subset_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
2933 FAN(x,V,E)
2934 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
2935 ==> ds SUBSET d_fan (x,V,E)`,
2936 REPEAT GEN_TAC THEN STRIP_TAC
2937 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
2938 THEN MRESA_TAC hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
2939 THEN MRESA_TAC lemma_face_subset[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]);;
2940
2941
2942
2943
2944 let properties_of_elements_in_face_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
2945 FAN(x,V,E)
2946 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
2947 /\ y IN ds
2948 ==> {pr2 y, pr3 y} IN E\/ pr2 y= pr3 y`,
2949 REPEAT GEN_TAC THEN STRIP_TAC
2950 THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
2951 THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
2952 THEN RESA_TAC
2953 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM]
2954 THEN STRIP_TAC
2955 THEN ASM_REWRITE_TAC[pr2;pr3]);;
2956
2957 let fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2958 FAN(x,V,E)
2959 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2960 ==> d20_fan(x,V,E)={}`,
2961 REPEAT STRIP_TAC
2962 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
2963 THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`]
2964 THEN REWRITE_TAC[d20_fan;IN_ELIM_THM]
2965 THEN STRIP_TAC
2966 THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES])
2967 THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
2968
2969
2970
2971
2972 let dartset_fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2973 FAN(x,V,E)
2974 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2975 ==> d_fan(x,V,E)=d1_fan(x,V,E)`,
2976 REPEAT STRIP_TAC
2977 THEN MRESA_TAC fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
2978 THEN ASM_REWRITE_TAC[d_fan;]
2979 THEN SET_TAC[]);;
2980
2981
2982 let properties_of_elements_in_face_fully_surroundedfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
2983 FAN(x,V,E)
2984 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2985 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
2986 /\ y IN ds
2987 ==> {pr2 y, pr3 y} IN E`,
2988 REPEAT GEN_TAC THEN STRIP_TAC
2989 THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
2990 THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
2991 THEN RESA_TAC
2992 THEN POP_ASSUM MP_TAC
2993 THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
2994 THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
2995 THEN STRIP_TAC
2996 THEN ASM_REWRITE_TAC[pr2;pr3]);;
2997
2998
2999
3000 let AAUHTVE=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) p.
3001 FAN(x,V,E)/\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==>
3002 FINITE (d_fan (x,V,E))
3003 /\ (p e_fan) permutes (d_fan (x,V,E))
3004 /\ (p n_fan) permutes (d_fan (x,V,E))
3005 /\ (p f1_fan) permutes (d_fan (x,V,E))
3006 /\(p e_fan) o (p n_fan) o (p f1_fan)= I
3007 /\ (!a. a IN d1_fan(x,V,E)==> (e_fan x V E)  (e_fan x V E a) =a)
3008 /\ (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))
3009 /\ (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))
3010 /\ (!k:num l:num a. a IN d1_fan(x,V,E) ==>
3011 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)
3012
3013 /\ (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a))`,
3014
3015 MESON_TAC[lemma_hypermap1_of_fanx;e_fan_permutes;n_fan_permutes;finite_d_fan;f1_fan_permutes;plain_hypermap_fan;e_fan_no_fix_point;f_fan_no_fix_point;distinct_nodes;edge_lie_different_nodes]);;
3016
3017 (********************************)
3018
3019
3020 end;;