1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================== *)
11 (*flyspeck_needs "general/sphere.hl";;*)
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";;
31 (* ========================================================================== *)
33 (* ========================================================================== *)
37 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
39 let fan1 = new_definition`fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {}) `;;
41 let fan2 = new_definition`fan2(x,V,E):bool <=> ~(x IN V)`;;
43 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
45 let fan4 = new_definition`fan4(x,V,E):bool<=> (!e. (e IN E) ==> (aff_gt {x} e INTER V={}))`;;
47 let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
49 let fan = new_definition`fan(x,V,E)<=> ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;;
51 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
53 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
56 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
58 let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
59 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
63 let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
64 fan6(x,V,E)/\ fan7(x,V,E)`;;
68 (* ========================================================================== *)
69 (* Invariance theorems *)
70 (* ========================================================================== *)
75 (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
76 REWRITE_TAC[graph; IN]);;
78 let CYCLIC_SET = prove
79 (`cyclic_set W v w <=>
82 (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\
83 W INTER affine hull {v, w} = {}`,
84 REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
86 let CYCLIC_SET_TRANSLATION_EQ = prove
88 cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
89 REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
91 let CYCLIC_SET_LINEAR_IMAGE = prove
92 (`!f:real^M->real^N s x y.
93 linear f /\ (!x y. f x = f y ==> x = y)
94 ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
95 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
96 [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN
97 GEOM_TRANSFORM_TAC[]);;
99 add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;
101 add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
103 let GRAPH_TRANSLATION_EQ = prove
104 (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
105 REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
107 let GRAPH_LINEAR_IMAGE_EQ = prove
108 (`!f:real^M->real^N E.
109 linear f /\ (!x y. f x = f y ==> x = y)
110 ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
111 REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
113 let FAN1_TRANSLATION_EQ = prove
115 fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
117 REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
119 let FAN1_LINEAR_IMAGE_EQ = prove
120 (`!f:real^M->real^N x V E.
121 linear f /\ (!x y. f x = f y ==> x = y)
122 ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
123 REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
125 let FAN2_TRANSLATION_EQ = prove
127 fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
129 REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
131 let FAN2_LINEAR_IMAGE_EQ = prove
132 (`!f:real^M->real^N x V E.
133 linear f /\ (!x y. f x = f y ==> x = y)
134 ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
135 REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
137 let FAN3_TRANSLATION_EQ = prove
139 fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
141 REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
143 let FAN3_LINEAR_IMAGE_EQ = prove
144 (`!f:real^M->real^N x V E.
145 linear f /\ (!x y. f x = f y ==> x = y)
146 ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
148 (`{w | {a,w} IN IMAGE (IMAGE f) s} =
149 IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
150 MATCH_MP_TAC(SET_RULE
151 `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
152 REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
154 REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
156 let FAN4_TRANSLATION_EQ = prove
158 fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
160 REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
162 let FAN4_LINEAR_IMAGE_EQ = prove
163 (`!f:real^M->real^N x V E.
164 linear f /\ (!x y. f x = f y ==> x = y)
165 ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
166 REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
168 let FAN5_TRANSLATION_EQ = prove
170 fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
172 REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
174 let FAN5_LINEAR_IMAGE_EQ = prove
175 (`!f:real^M->real^N x V E.
176 linear f /\ (!x y. f x = f y ==> x = y)
177 ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
178 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
179 [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
180 GEOM_TRANSFORM_TAC[]);;
182 let FAN6_TRANSLATION_EQ = prove
184 fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
186 REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
188 let FAN6_LINEAR_IMAGE_EQ = prove
189 (`!f:real^M->real^N x V E.
190 linear f /\ (!x y. f x = f y ==> x = y)
191 ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
192 REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
194 let FAN7_TRANSLATION_EQ = prove
196 fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
198 REWRITE_TAC[fan7] THEN
200 `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
201 GEOM_TRANSLATE_TAC[]);;
203 let FAN7_LINEAR_IMAGE_EQ = prove
204 (`!f:real^M->real^N x V E.
205 linear f /\ (!x y. f x = f y ==> x = y)
206 ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
207 REWRITE_TAC[fan7; IN_UNION] THEN
208 REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB;
209 TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
210 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV)
211 [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
212 REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN
213 GEOM_TRANSFORM_TAC[]);;
215 add_translation_invariants
216 [GRAPH_TRANSLATION_EQ;
223 FAN7_TRANSLATION_EQ];;
225 add_linear_invariants
226 [GRAPH_LINEAR_IMAGE_EQ;
227 FAN1_LINEAR_IMAGE_EQ;
228 FAN2_LINEAR_IMAGE_EQ;
229 FAN3_LINEAR_IMAGE_EQ;
230 FAN4_LINEAR_IMAGE_EQ;
231 FAN5_LINEAR_IMAGE_EQ;
232 FAN6_LINEAR_IMAGE_EQ;
233 FAN7_LINEAR_IMAGE_EQ];;
235 let FAN_TRANSLATION_EQ = prove
237 FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
239 REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
241 let FAN_LINEAR_IMAGE_EQ = prove
242 (`!f:real^M->real^N x V E.
243 linear f /\ (!x y. f x = f y ==> x = y)
244 ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
245 REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
247 add_translation_invariants [FAN_TRANSLATION_EQ];;
248 add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
250 let BASE_POINT_FAN_TRANSLATION_EQ = prove
252 base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) =
253 a + base_point_fan(x,V,E)`,
254 REWRITE_TAC[base_point_fan]);;
256 let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
257 (`!f:real^M->real^N x V E.
259 ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) =
260 f(base_point_fan(x,V,E))`,
261 REWRITE_TAC[base_point_fan]);;
263 let SET_OF_EDGE_TRANSLATION_EQ = prove
265 set_of_edge (a + x) (IMAGE (\x. a + x) V)
266 (IMAGE (IMAGE (\x. a + x)) E) =
267 IMAGE (\x. a + x) (set_of_edge x V E)`,
268 REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
270 let SET_OF_EDGE_LINEAR_IMAGE_EQ = prove
271 (`!f:real^M->real^N x V E.
272 linear f /\ (!x y. f x = f y ==> x = y)
273 ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) =
274 IMAGE f (set_of_edge x V E)`,
276 (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
277 {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
278 MATCH_MP_TAC(SET_RULE
279 `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
280 REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
282 REWRITE_TAC[set_of_edge; lemma] THEN
283 GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
285 add_translation_invariants
286 [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;
288 add_linear_invariants
289 [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
297 let CTVTAQA=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E1:(real^3->bool)->bool).
298 FAN(x,V,E) /\ E1 SUBSET E
302 THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7;graph]
303 THEN ASM_SET_TAC[]);;
307 (* ========================================================================== *)
309 (* ========================================================================== *)
312 let set_of_edge_subset_edges=prove(`!(V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
313 set_of_edge v V E SUBSET V`,
314 REWRITE_TAC[set_of_edge] THEN SET_TAC[]);;
318 let remark_fan1=prove(`!v w V E.
319 (v IN V) /\ (w IN V) ==>
320 ((w IN set_of_edge v V E)<=>(v IN set_of_edge w V E))`,
322 (let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
323 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
325 let remark_finite_fan1=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FINITE V ==> FINITE (set_of_edge v V E)`,
326 REPEAT GEN_TAC THEN DISCH_TAC
327 THEN MP_TAC(ISPECL [`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`; `V:real^3->bool`] FINITE_SUBSET)
328 THEN ASM_REWRITE_TAC[]
329 THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
331 let properties_of_set_of_edge=prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3.
334 ({v,u} IN E <=> u IN set_of_edge v V E)`,
335 REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
337 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
338 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
343 let expand_edge_graph_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (e:real^3->bool).
345 ==> ?v:real^3 w:real^3. e={v,w}`,
347 THEN REWRITE_TAC[FAN;IN]
349 THEN FIND_ASSUM MP_TAC `graph (E:(real^3->bool)->bool)`
350 THEN REWRITE_TAC[graph]
352 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`e:real^3->bool`th))
354 THEN POP_ASSUM MP_TAC
355 THEN REWRITE_TAC[HAS_SIZE]
357 THEN SUBGOAL_THEN `~((e:real^3->bool)={})` ASSUME_TAC
360 THEN MP_TAC(ISPEC`(e:real^3->bool)`CARD_EQ_0)
362 THEN POP_ASSUM MP_TAC
364 MP_TAC(SET_RULE `~((e:real^3->bool)={})==> ?v:real^3. v IN e`)
366 THEN SUBGOAL_THEN`~((e:real^3->bool) DELETE v={})` ASSUME_TAC
369 THEN MP_TAC(ISPECL[`v:real^3`;`(e:real^3->bool)`;]CARD_DELETE)
371 THEN MP_TAC(ISPECL[`(e:real^3->bool)`;`v:real^3`] FINITE_DELETE)
373 THEN MP_TAC(ISPEC`(e:real^3->bool) DELETE v`CARD_EQ_0)
375 THEN POP_ASSUM MP_TAC
377 MP_TAC(SET_RULE `~((e:real^3->bool)DELETE v={})==> ?w:real^3. w IN (e:real^3->bool)DELETE v/\ w IN e`)
379 THEN MP_TAC(SET_RULE `(v IN (e:real^3->bool))/\ (w IN (e:real^3->bool))==> {v,w} SUBSET e`)
381 THEN MP_TAC(SET_RULE `(w IN (e:real^3->bool)DELETE v)==> ~(v=w)`)
383 THEN MP_TAC(ISPECL [`{v:real^3,w:real^3}`;`(e:(real^3->bool))`] FINITE_SUBSET)
385 THEN ASSUME_TAC(SET_RULE `v:real^3 IN {v:real^3,w:real^3} `)
386 THEN MP_TAC(ISPECL[`v:real^3`;`{v:real^3,w:real^3}`;]CARD_DELETE)
388 THEN MP_TAC(SET_RULE `v IN {v,w}==>{v:real^3,w:real^3} DELETE v PSUBSET {v,w}`)
390 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v`;`{v:real^3,w:real^3}`]CARD_PSUBSET)
391 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
392 THEN FIND_ASSUM MP_TAC`FINITE {v:real^3,w:real^3}`
394 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
396 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v) < CARD {v, w}/\ CARD ({v, w} DELETE v) = CARD {v, w}-1
397 <=>CARD ({v, w} DELETE v) +1= CARD {v:real^3, w:real^3}`)
398 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
399 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
400 THEN REWRITE_TAC[ARITH_RULE`A=A`]
402 THEN SUBGOAL_THEN `w:real^3 IN ({v:real^3,w:real^3} DELETE v)` ASSUME_TAC
405 MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`v:real^3`] FINITE_DELETE)
407 THEN MP_TAC(ISPECL[`w:real^3`;`{v:real^3,w:real^3} DELETE v`;]CARD_DELETE)
409 THEN MP_TAC(SET_RULE `w IN ({v,w} DELETE v)==>{v:real^3,w:real^3} DELETE v DELETE w PSUBSET {v,w} DELETE v`)
411 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v DELETE w`;`{v:real^3,w:real^3} DELETE v`]CARD_PSUBSET)
412 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
413 THEN FIND_ASSUM MP_TAC`FINITE ({v:real^3,w:real^3} DELETE v)`
415 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
417 THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v DELETE w) < CARD ({v, w} DELETE v)/\ CARD ({v, w} DELETE v DELETE w) = CARD ({v, w} DELETE v)-1
418 <=>CARD ({v, w} DELETE v DELETE w) +1= CARD ({v:real^3, w:real^3} DELETE v)`)
419 THEN POP_ASSUM (fun th->REWRITE_TAC[th])
420 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;])
421 THEN REWRITE_TAC[ARITH_RULE`A=A`]
423 THEN POP_ASSUM MP_TAC
424 THEN POP_ASSUM (fun th->REWRITE_TAC[])
425 THEN POP_ASSUM (fun th->REWRITE_TAC[])
426 THEN ASSUME_TAC(SET_RULE `{v, w} DELETE v:real^3 DELETE w:real^3={}`)
427 THEN POP_ASSUM (fun th->REWRITE_TAC[th;CARD_CLAUSES; ARITH_RULE `0+1=1`])
428 THEN POP_ASSUM MP_TAC
429 THEN DISCH_THEN(LABEL_TAC"B")
431 THEN REMOVE_THEN "B" MP_TAC
432 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th);ARITH_RULE` 1+1=2`])
433 THEN FIND_ASSUM MP_TAC`CARD (e:real^3->bool)=2`
435 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
437 THEN MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`e:real^3->bool`]CARD_SUBSET_EQ)
438 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])
440 THEN EXISTS_TAC`v:real^3`
441 THEN EXISTS_TAC`w:real^3`
442 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])]]]);;
448 let add_edge_graph_fan=prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A.
449 v IN V /\ u IN V /\ E1=E UNION {{v,u}} /\ UNIONS E SUBSET V==> UNIONS E1 SUBSET V`,
451 THEN POP_ASSUM MP_TAC
452 THEN ASM_REWRITE_TAC[UNIONS; SUBSET; UNION; IN_ELIM_THM;IN_SING]
453 THEN DISCH_THEN(LABEL_TAC "YEU")
454 THEN REPEAT STRIP_TAC
455 THENL[SUBGOAL_THEN`(?u. u IN E /\ x IN (u:A->bool))`ASSUME_TAC
457 EXISTS_TAC`u':A->bool` THEN ASM_REWRITE_TAC[];
458 REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `x:A`)];
459 ASM_TAC THEN SET_TAC[]]);;
462 let garph_add_edge_is_garph=prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A.
463 E1=E UNION {{v,u}} /\ ~(v=u) /\ graph E==> graph E1`,
465 THEN POP_ASSUM MP_TAC
466 THEN ASM_REWRITE_TAC[GRAPH; UNION;IN_ELIM_THM;IN_SING]
467 THEN DISCH_THEN(LABEL_TAC"YEU")
468 THEN GEN_TAC THEN STRIP_TAC
469 THENL[REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `e:A->bool`);
470 ASM_REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC
471 THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`]
472 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
473 IN_INSERT; NOT_IN_EMPTY]]);;
475 let add_edge_into_collinear_fan=prove(`!x:real^3 (E:(real^3->bool)->bool) v:real^3 u:real^3.
476 ~collinear {x,v,u} /\
477 (!e. e IN E ==> ~collinear ({x} UNION e))
479 (!e. e IN E UNION {{v, u}} ==> ~collinear ({x} UNION e))`,
481 THEN POP_ASSUM MP_TAC
482 THEN POP_ASSUM MP_TAC
483 THEN ASM_REWRITE_TAC[]
484 THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)[UNION;]
485 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING]
486 THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
488 THENL[REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th `e:real^3->bool`);
489 ASM_REWRITE_TAC[SET_RULE`{X} UNION {A,B}={X,A,B}`]]);;
492 let properties_edges_eq_fan=prove(`!e:A-> bool v:A u:A.
493 FINITE e /\ ~(e={v,u}) /\ ~(v=u) /\ CARD e=2 ==> ~(v IN e)\/ ~(u IN e)`,
494 REPEAT GEN_TAC THEN STRIP_TAC
495 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "YEU")
496 THEN ONCE_REWRITE_TAC[SET_RULE`~A \/ ~B<=> ~(A/\B)`]
498 THEN MP_TAC(SET_RULE`v IN e /\ u IN e ==> {v:A,u} SUBSET e`)
500 THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`]
501 THEN REMOVE_THEN "YEU" MP_TAC
502 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
504 THEN MRESA_TAC CARD_SUBSET_EQ[`{v,u:A}`;`e:A->bool`]);;
509 (* ========================================================================== *)
511 (* ========================================================================== *)
514 let set_edges_is_finite_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool).
515 FAN(x,V,E)==> FINITE E`,
517 THEN REWRITE_TAC[FAN;fan1;graph]
519 THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET)
521 THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`)
523 THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET)
524 THEN ASM_SET_TAC[]);;
528 let properties_of_set_of_edge_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
531 ({v,u} IN E <=> u IN set_of_edge v V E)`,
532 REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM]
533 THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC
534 THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC
535 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
539 let properties_of_graph=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
540 FAN(x,V,E) /\{v,u} IN E==> v IN V`,
542 REPEAT GEN_TAC THEN REWRITE_TAC[FAN] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN
543 REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC
544 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC
545 THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
548 let properties_of_graph1=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
549 FAN(x,V,E) /\{v,u} IN E==> u IN V`,
550 ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[properties_of_graph]);;
553 let th4=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
554 FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
555 REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`; `(v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan2] THEN SET_TAC[]);;
557 let remark4_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
558 FAN(x,V,E) /\ {v,u} IN E==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\ DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,
560 REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN"a"(fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REWRITE_TAC[th3]);;
563 let collinears_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
564 FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
565 MESON_TAC[remark4_fan;collinear_fan]);;
567 let remark1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
569 FINITE (set_of_edge v V E)
570 /\({v,u} IN E <=> u IN set_of_edge v V E)/\
572 ~ collinear {x,v,u}/\
573 ~ (x=v) /\ ~(x=u)/\ ~(v=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v}) /\ v IN V /\ u IN V/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
574 MESON_TAC[FAN;fan1;remark_finite_fan1;remark4_fan; properties_of_graph; SET_RULE`DISJOINT {x,v} {u} ==> ~(v=u)`;collinears_fan;properties_of_set_of_edge_fan;properties_of_graph1]);;
581 (* ========================================================================== *)
582 (* EXISTS SIGMA_FAN *)
583 (* ========================================================================== *)
587 let sigma_fan=new_definition`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
588 (if (set_of_edge v V E = {u} ) then u
589 else (@(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
590 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
593 (* This extends sigma to have a larger domain
594 of R^3 rather than just V. It is the
595 identity outside V (compare the definition
601 let extension_sigma_fan=new_definition`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
602 (if ~(u IN set_of_edge v V E ) then u
603 else (sigma_fan x V E v u))`;;
609 let exists_sigma_fan=prove(`
610 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
611 ~ (set_of_edge v V E= {u} )
612 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
614 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
615 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`,
618 FINITE X /\ ~(X = {})
619 ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
620 MESON_TAC[INF_FINITE]) in
623 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
625 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3))` ASSUME_TAC
627 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
629 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)={})\/
630 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)={})`)
632 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
633 THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
635 ASM_TAC THEN SET_TAC[];(*4*)
636 ASM_TAC THEN SET_TAC[]](*4*);(*3*)
637 SUBGOAL_THEN`~(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3))={})` ASSUME_TAC
639 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
641 SUBGOAL_THEN` FINITE (IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)))` ASSUME_TAC
643 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
644 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)))` th))
645 THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
646 THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
647 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
651 let SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
652 ~ (set_of_edge v V E= {u} )
653 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
655 ((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\
656 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u (sigma_fan x V E v u) <= azim x v u w1)`,
658 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan]
659 THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]exists_sigma_fan) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
665 let sigma_fan_in_set_of_edge=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
666 FAN(x,V,E) /\ (u IN (set_of_edge v V E))
668 ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
670 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~ (set_of_edge v V E= {u:real^3} )\/ (set_of_edge v V E= {u} )`)
672 MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
675 ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
679 (* ========================================================================== *)
680 (* CONDITION UNIQUE FOINT AND SIGMA_FAN *)
681 (* ========================================================================== *)
687 let UNIQUE_FOINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
688 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\
689 ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v})
691 REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC
692 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
693 THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC
694 THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th))
695 THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
696 THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`)
698 [ MP_TAC(SET_RULE`~((u:real^3)=(w:real^3))==> {(v:real^3),(u:real^3)} INTER {(v:real^3),(w:real^3)}={v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];
699 ASM_TAC THEN SET_TAC[]]);;
709 let UNIQUE1_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
710 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u}
712 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN
713 EXISTS_TAC `x:real^3` THEN EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `E:(real^3->bool)->bool` THEN EXISTS_TAC `v:real^3`
714 THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC)
715 THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
716 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
717 THEN DISCH_THEN (LABEL_TAC "a")
718 THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
719 THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
720 THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th))
721 THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
722 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c")
723 THEN DISCH_TAC THEN DISCH_TAC
724 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[]
725 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[]
726 THEN DISCH_TAC THEN DISCH_TAC
727 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
728 THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
729 THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC
731 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_10)
732 THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`)
733 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
734 THEN ASM_REWRITE_TAC[]
735 THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*)
737 SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC
739 ASM_TAC THEN SET_TAC[];(*2*)
741 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`)
743 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
745 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
746 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
747 THEN EXISTS_TAC `t1:real`
748 THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[]
749 THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*)
751 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
753 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
754 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
755 THEN EXISTS_TAC `&0:real`
756 THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &0 % v + &1 % w `] THEN REAL_ARITH_TAC;(*5*)
758 ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*)
760 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
762 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2)
763 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
764 THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))`
765 THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)`
766 THEN MP_TAC(ISPEC `t3:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0< inv(t3:real)==> (&0 <= inv(t3:real))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
767 THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
768 THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN
769 MP_TAC(REAL_ARITH`(t1:real)+(t2:real)+(t3:real)= &1 ==> &1 - t1- t2=t3`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
770 MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH`
771 (inv t3 * --t1) % x +
772 (inv t3 * --t2) % v +
773 inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u `
775 THEN MP_TAC(ISPEC `t3:real` REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH ` v= &1 % v`];(*4*)
777 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
779 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
780 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
781 THEN EXISTS_TAC `&0:real`
782 THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN REWRITE_TAC[VECTOR_ARITH`u= &0 % x+ &0 % v + &1 % u `] THEN REAL_ARITH_TAC;(*5*)
783 ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;
786 let UNIQUE_AZIM_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3 w1:real^3.
787 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ { v, w1} IN E /\ (azim x v u w =azim x v u w1)
790 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
791 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
792 THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
793 THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
794 THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w1:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
795 THEN REPEAT STRIP_TAC
796 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) THEN
797 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
798 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` w1:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[] );;
801 let UNIQUE_AZIM_0_POINT_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
802 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0)
805 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC
806 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
807 THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
808 THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
809 THEN REPEAT STRIP_TAC
810 THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) THEN
811 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
812 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` w:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[] );;
817 let UNIQUE_SIGMA_FAN=prove(`
818 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
819 ~ (set_of_edge v V E= {u} )
820 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
821 /\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\
822 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)
823 ==> sigma_fan x V E v u=w)`,
825 ( let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
826 FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
827 ==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
831 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN
832 DISCH_TAC THEN DISCH_THEN(LABEL_TAC "1")
833 THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4")
834 THEN DISCH_THEN(LABEL_TAC"a")
835 THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
836 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
837 THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` th))
838 THEN ASM_REWRITE_TAC[]
839 THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[]
840 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
841 THEN REPEAT DISCH_TAC
842 THEN SUBGOAL_THEN `azim x v u (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = azim x v u (w:real^3)` ASSUME_TAC
844 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
845 REMOVE_THEN "123" (fun th->MP_TAC (ISPECL[`(x:real^3)`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`; `(v:real^3)` ; `(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`(w:real^3)`]th))
846 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
848 REMOVE_THEN"1" MP_TAC
849 THEN REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
850 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
851 THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC
852 THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
853 THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
854 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
855 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
856 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
857 THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
858 THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)` ;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`; `(w:real^3)`]AZIM_EQ )
859 THEN ASM_REWRITE_TAC[]
860 THEN ASM_MESON_TAC[]]));;
864 (* ========================================================================== *)
866 (* ========================================================================== *)
872 let CYCLIC_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
874 ==> cyclic_set (set_of_edge v V E) x v`,
877 THEN REPEAT (POP_ASSUM MP_TAC)
878 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th)
879 THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC
880 THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*)
882 THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*)
883 STRIP_TAC THENL(*3*)[
885 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
886 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
887 DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b")
888 THEN STRIP_TAC THEN STRIP_TAC THEN
889 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th))
890 THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th))
891 THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC
892 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[]
893 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[]
894 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
895 THEN POP_ASSUM (fun th-> REWRITE_TAC[])
896 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
897 THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC
900 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[]
901 THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
902 THEN EXISTS_TAC `--(h:real)` THEN EXISTS_TAC `(h:real)` THEN EXISTS_TAC `&1` THEN REWRITE_TAC[VECTOR_ARITH`q= (-- (h:real)) % x + (h:real) % v + &1 % (q+ h% (x-v))`] THEN REAL_ARITH_TAC;(*4*)
904 ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*)
906 REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC
907 THEN SUBGOAL_THEN`(x':real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ==> ~(x' IN aff {x,v})`
910 ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN
911 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
912 DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b")
913 THEN STRIP_TAC THEN STRIP_TAC THEN
914 REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) )
915 THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC
916 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*)
920 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN STRIP_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[aff];(*5*)
922 ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
925 let XOHLED=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
927 ==> cyclic_set (set_of_edge v V E) x v`,
928 MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
931 (* ========================================================================== *)
932 (* SIGMA_FAN IS PERMUTES (^_^) *)
933 (* ========================================================================== *)
936 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
939 let exists_inverse_sigma_fan_alt=prove(`
940 (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
941 ~ (set_of_edge v V E= {u} )
942 /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E))
944 (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\
945 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <= azim1 x v u w1)))
949 FINITE X /\ ~(X = {})
950 ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
951 MESON_TAC[INF_FINITE]) in
952 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
953 SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3))` ASSUME_TAC
956 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
957 DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)={})\/
958 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)={})`)
960 POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
961 THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
963 ASM_TAC THEN SET_TAC[];(*4*)
964 ASM_TAC THEN SET_TAC[](*4*)];
966 SUBGOAL_THEN`~(IMAGE ( azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3))={})` ASSUME_TAC
968 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
969 SUBGOAL_THEN` FINITE (IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)))` ASSUME_TAC
971 ASM_MESON_TAC[FINITE_IMAGE];(*5*)
972 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE (u:real^3)))` th))
973 THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
974 THEN EXISTS_TAC`x':real^3`
975 THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
976 ](*5*)](*4*)](*3*)](*2*)(*1*)));;
981 let SUR_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
982 FAN(x,V,E) /\ ({v,u} IN E)
983 ==> ?w. {v,w} IN E /\sigma_fan x V E v w= u
985 REPEAT GEN_TAC THEN STRIP_TAC
986 THEN DISJ_CASES_TAC(SET_RULE `(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`)
988 EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*)
990 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
991 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]exists_inverse_sigma_fan_alt) THEN ASM_REWRITE_TAC[azim1;] THEN STRIP_TAC THEN
992 MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[]
993 THEN MATCH_MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`] UNIQUE_SIGMA_FAN)
994 THEN ASM_REWRITE_TAC[]
995 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC
996 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`)
998 FIND_ASSUM(MP_TAC)`u:real^3 IN set_of_edge v V E` THEN POP_ASSUM(fun th->REWRITE_TAC[th;IN_SING]) THEN ASM_TAC THEN SET_TAC[] ;(*2*)
1000 ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN
1001 DISJ_CASES_TAC(SET_RULE`~(azim (x:real^3) v w u <= azim x v w w1)\/ (azim (x:real^3) v w u <= azim x v w w1)`)
1003 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC
1005 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
1006 SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
1008 ASM_TAC THEN SET_TAC[];(*5*)
1009 FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN
1010 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1011 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
1012 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1013 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (w1:real^3),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
1014 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1015 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`;`u:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[]
1016 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC
1017 THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC
1018 THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
1019 POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN
1020 MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge)
1021 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1022 THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
1023 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
1024 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th))
1025 THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
1026 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC
1028 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) = &0)`)
1030 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w1:real^3`]UNIQUE_AZIM_0_POINT_FAN)
1031 THEN ASM_TAC THEN SET_TAC[];(*7*)
1033 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) = &0)`)
1035 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w:real^3`]UNIQUE_AZIM_0_POINT_FAN)
1036 THEN ASM_TAC THEN SET_TAC[];(*8*)
1037 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1038 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[]
1039 THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1040 THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3. w1 IN set_of_edge v V E /\ ~(w1 = u)
1041 ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1`
1042 THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1043 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`)
1045 ASM_REWRITE_TAC[REAL_ARITH`&2 * pi -(a:real)<= &2 *pi - b <=> b <= a`] THEN DISJ_CASES_TAC(SET_RULE `(azim(x:real^3) v u w =azim x v u w1)\/ ~(azim(x:real^3) v u w =azim x v u w1)`)
1047 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`;`(w1:real^3)`]UNIQUE_AZIM_POINT_FAN) THEN ASM_REWRITE_TAC[];(*10*)
1048 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*)
1049 SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC
1050 THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*)
1051 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*);
1052 ASM_TAC THEN SET_TAC[]]]]);;
1059 let MONO_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
1060 FAN(x,V,E) /\ ({v,u} IN E)
1062 (sigma_fan x V E v u= sigma_fan x V E v w)
1065 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1")
1066 THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6]
1067 THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN
1068 DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") THEN
1069 REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1070 THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~((set_of_edge v V E={u}))`)
1072 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
1073 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[]
1074 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
1075 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th))
1076 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
1077 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th))
1078 THEN ASM_TAC THEN SET_TAC[];(*1*)
1080 DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})\/ ~((set_of_edge v V E={w}))`)
1083 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM]
1084 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[]
1085 THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM]
1086 THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th))
1087 THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM]
1088 THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th))
1089 THEN ASM_TAC THEN SET_TAC[];(*2*)
1092 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
1093 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1094 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
1095 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1096 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN)
1097 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1098 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th))
1099 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
1100 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1101 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th))
1102 THEN ASM_REWRITE_TAC[]
1103 THEN MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge)
1104 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1105 THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
1106 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
1107 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
1108 THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
1109 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
1110 DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`)
1113 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{(w:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC
1114 THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*)
1116 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
1117 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1118 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
1119 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
1120 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "c") THEN
1121 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
1124 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN)
1125 THEN ASM_TAC THEN SET_TAC[];(*5*)
1127 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3) = &0)`)
1131 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
1132 THEN ASM_TAC THEN SET_TAC[];(*6*)
1134 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3) = &0)`)
1137 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
1138 THEN ASM_TAC THEN SET_TAC[];(*7*)
1140 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]AZIM_COMPL)
1141 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1142 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN
1143 ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC
1144 THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`]
1145 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`] azim)THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
1146 (*7*)](*6*)](*5*)](*4*)];(*3*)
1148 ASM_REWRITE_TAC[](*3*)]]]);;
1153 let permutes_sigma_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
1154 FAN(x,V,E) /\ ({v,u} IN E)
1156 (extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
1157 REPEAT GEN_TAC THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`FAN((x:real^3), V, E)` THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC
1158 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`]remark_finite_fan1)
1159 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1160 THEN MP_TAC(ISPECL[`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`;`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`]PERMUTES_FINITE_INJECTIVE)
1161 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1163 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan];
1166 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)}\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)})`)
1167 THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING];
1168 ASM_MESON_TAC[SIGMA_FAN]];
1169 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC
1170 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge)
1171 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1172 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge)
1173 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1174 ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;
1179 (* ========================================================================== *)
1180 (* INVERSE OF SIGMA_FAN *)
1181 (* ========================================================================== *)
1186 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
1193 let exists_function_inverse_sigma_fan_alt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
1195 (?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
1196 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
1197 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w))
1199 REPEAT STRIP_TAC THEN
1200 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] sigma_fan_in_set_of_edge) THEN
1201 ASM_REWRITE_TAC[] THEN DISCH_TAC
1202 THEN MP_TAC(ISPECL[`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`; `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]BIJECTIVE_ON_LEFT_RIGHT_INVERSE)
1203 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] properties_of_set_of_edge_fan) THEN
1204 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
1207 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) THEN
1208 ASM_REWRITE_TAC[] THEN DISCH_TAC
1210 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] SUR_SIGMA_FAN) THEN
1211 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
1214 This is the same as inverse_sigma_fan_alt,
1220 let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
1221 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
1222 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
1226 let INVERSE1_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
1228 ( (!w:real^3. {v,w} IN E==> {v, inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w} IN E)
1229 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w) =w)
1230 /\ (!w:real^3. {v,w} IN E==> inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (sigma_fan x V E v w) =w))`,
1231 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[inverse1_sigma_fan] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `]exists_function_inverse_sigma_fan_alt)
1232 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
1238 (* ========================================================================== *)
1239 (* PROPERTIES OF FAN *)
1240 (* ========================================================================== *)
1245 let properties_of_fan7=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3 u1:real^3.
1246 FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1,u1}
1247 ==> v = v1 \/ v = u1`,
1250 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
1251 THEN REWRITE_TAC[FAN; fan6; fan7]
1252 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1254 THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3),(u1:real^3)}`]th))
1255 THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
1256 THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
1258 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
1259 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1260 THEN EXISTS_TAC `&0:real`
1261 THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real`
1262 THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC;
1265 THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u} /\ v IN aff_ge {x} {v1, u1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1, u1:real^3}`)
1267 THEN POP_ASSUM MP_TAC
1268 THEN DISJ_CASES_TAC(SET_RULE`{v, u} INTER {v1, u1:real^3}={} \/ ~({v, u} INTER {v1, u1}={})`)
1271 THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC
1273 ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`)
1276 ASM_REWRITE_TAC[IN_ELIM_THM]
1277 THEN STRIP_TAC THEN POP_ASSUM MP_TAC
1278 THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC
1279 THEN ASM_REWRITE_TAC[]];(*2*)
1281 DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1, u1:real^3}) \/ (v IN {v, u} INTER {v1, u1})`)
1283 SUBGOAL_THEN`({v:real^3, u} INTER {v1, u1}={u})` ASSUME_TAC
1286 THEN SET_TAC[];(*4*)
1289 THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC
1291 MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1)
1292 THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`)
1293 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1294 THEN ASM_REWRITE_TAC[]
1295 THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*5*)
1297 FIND_ASSUM MP_TAC`{v,u:real^3} IN E`
1298 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1300 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`u:real^3`]
1302 THEN SET_TAC[]]];(*3*)
1305 THEN SET_TAC[]]]]) ;;
1312 let properties1_of_fan7=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3 u1:real^3.
1313 FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1}
1317 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
1318 THEN REWRITE_TAC[FAN; fan6; fan7]
1319 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`]
1320 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u1:real^3`;`v1:real^3`]
1321 THEN MP_TAC(SET_RULE`(v1:real^3) IN V==> (?v. v IN V /\ {v1} = {v})`)
1324 THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3)}`]th))
1325 THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
1326 THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
1328 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2)
1329 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1330 THEN EXISTS_TAC `&0:real`
1331 THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real`
1332 THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC;
1334 THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u:real^3} /\ v IN aff_ge {x} {v1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1}`)
1336 THEN POP_ASSUM MP_TAC
1337 THEN DISJ_CASES_TAC(SET_RULE`{v, u:real^3} INTER {v1}={} \/ ~({v, u} INTER {v1}={})`)
1340 THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC
1342 ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`)
1344 ASM_REWRITE_TAC[IN_ELIM_THM]
1345 THEN STRIP_TAC THEN POP_ASSUM MP_TAC
1346 THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC
1347 THEN ASM_REWRITE_TAC[]];(*2*)
1349 DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1:real^3}) \/ (v IN {v, u} INTER {v1})`)
1351 SUBGOAL_THEN`({v:real^3, u} INTER {v1:real^3}={u})` ASSUME_TAC
1356 THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC
1358 MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1)
1359 THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`)
1360 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1361 THEN ASM_REWRITE_TAC[]
1362 THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];
1363 FIND_ASSUM MP_TAC`{v,u:real^3} IN E`
1364 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1366 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
1368 THEN SET_TAC[]]];(*3*)
1371 THEN SET_TAC[]]]]) ;;
1377 let expand_elements_by_azim_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 x1:real x2:real x3:real.
1378 FAN(x,V,E)/\ {v,u} IN E /\ &0 < x1 /\ &0<= x2
1385 (x1 * cos (x2) * sin (x3)) % e1_fan x v u +
1386 (x1 * sin (x2) * sin (x3)) % e2_fan x v u +
1387 (x1 * cos (x3)) % e3_fan x v u) = x2`,
1389 (let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
1390 (let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in
1393 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;
1394 `(E:(real^3->bool)->bool)`;` u:real^3`;` v:real^3`]remark1_fan)
1396 THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
1397 THEN GEN_REWRITE_TAC( LAND_CONV o ONCE_DEPTH_CONV)[lem1]
1398 THEN ONCE_REWRITE_TAC[COLLINEAR_3]
1400 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
1402 THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
1403 THEN REWRITE_TAC[orthonormal]
1405 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
1407 THEN MP_TAC(ISPEC`x3:real`SIN_POS_PI2)
1409 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
1410 (x1 * cos (x2) * sin (x3)) % e1_fan x v u +
1411 (x1 * sin (x2) * sin (x3)) % e2_fan x v u +
1412 (x1 * cos (x3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
1413 `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
1414 `(x1 * cos (x3)) * (inv (norm((v:real^3)-(x:real^3))))`;
1415 `((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
1416 `x1 * sin (x3:real)`;
1417 `e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`x2:real`]AZIM_UNIQUE)
1419 THEN POP_ASSUM MATCH_MP_TAC
1420 THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
1423 MATCH_MP_TAC REAL_LT_MUL
1424 THEN REPEAT(POP_ASSUM MP_TAC)
1425 THEN REAL_ARITH_TAC;
1430 REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
1431 THEN REDUCE_ARITH_TAC
1432 THEN REDUCE_VECTOR_TAC
1433 THEN ONCE_REWRITE_TAC[GSYM e3_fan]
1434 THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
1435 ((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
1436 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
1437 THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
1438 THEN REDUCE_ARITH_TAC
1439 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
1440 THEN REDUCE_VECTOR_TAC
1441 THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
1443 THEN ASM_REWRITE_TAC[]
1444 THEN REWRITE_TAC[e1_fan]
1445 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
1446 THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
1447 THEN ONCE_REWRITE_TAC[DOT_SYM]
1448 THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
1449 THEN ONCE_REWRITE_TAC[GSYM e2_fan]
1450 THEN ASM_REWRITE_TAC[]
1451 THEN REDUCE_VECTOR_TAC
1453 THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
1454 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1455 THEN REWRITE_TAC[DOT_RZERO]
1456 THEN REAL_ARITH_TAC;
1458 THEN VECTOR_ARITH_TAC]])));;
1461 let one_edge_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3.
1462 FAN(x,V,E)/\ {v,u} IN E /\ ~(CARD (set_of_edge v V E) > 1)
1463 ==> set_of_edge v V E={u}`,
1465 THEN MP_TAC(ISPECL[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool) `;`u:real^3 `;`v:real^3`]remark1_fan)
1467 THEN MP_TAC(SET_RULE`(u:real^3) IN set_of_edge v V E==> ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={})/\ {(u:real^3)} SUBSET set_of_edge v V E`)
1469 THEN MP_TAC(ISPECL [`{(u:real^3)}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`] FINITE_SUBSET)
1471 THEN ASSUME_TAC(SET_RULE`u IN {(u:real^3)} /\ {(u:real^3)} DELETE u= {} /\ {} PSUBSET {(u:real^3)}`)
1472 THEN MP_TAC(ISPECL[`(u:real^3)`;`{(u:real^3)}`;]CARD_DELETE)
1474 THEN MP_TAC(ISPECL[`{}:real^3->bool`;`{(u:real^3)}`]CARD_PSUBSET)
1476 THEN POP_ASSUM MP_TAC
1477 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th))
1478 THEN POP_ASSUM MP_TAC
1479 THEN REWRITE_TAC[CARD_CLAUSES]
1480 THEN REPEAT DISCH_TAC
1481 THEN MP_TAC(ARITH_RULE` 0 = CARD ({(u:real^3)}) - 1 /\ 0 < CARD ({u}) <=> 1= CARD {u}`)
1483 THEN MP_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) > 1)==> CARD (set_of_edge v V E) <= 1`)
1485 THEN MP_TAC(ISPECL[`{u:real^3}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]CARD_SUBSET_LE)
1486 THEN ASM_SET_TAC[]);;