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";;
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`];;
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;;
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;;
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;;
55 (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
59 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
61 let fan1 = new_definition`fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {}) `;;
63 let fan2 = new_definition`fan2(x,V,E):bool <=> ~(x IN V)`;;
65 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
67 let fan4 = new_definition`fan4(x,V,E):bool<=> (!e. (e IN E) ==> (aff_gt {x} e INTER V={}))`;;
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 ={}))`;;
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)`;;
75 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
77 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
80 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
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)))`;;
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)`;;
91 (* ************************************************* *)
92 (* Invariance theorems *)
95 (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
96 REWRITE_TAC[graph; IN]);;
98 let CYCLIC_SET = prove
99 (`cyclic_set W v 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`]);;
106 let CYCLIC_SET_TRANSLATION_EQ = prove
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[]);;
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[]);;
119 add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];;
121 add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
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[]);;
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[]);;
133 let FAN1_TRANSLATION_EQ = prove
135 fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
137 REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
145 let FAN2_TRANSLATION_EQ = prove
147 fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
149 REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
157 let FAN3_TRANSLATION_EQ = prove
159 fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
161 REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
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))`,
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
174 REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
176 let FAN4_TRANSLATION_EQ = prove
178 fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
180 REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
188 let FAN5_TRANSLATION_EQ = prove
190 fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
192 REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
202 let FAN6_TRANSLATION_EQ = prove
204 fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
206 REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
214 let FAN7_TRANSLATION_EQ = prove
216 fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
218 REWRITE_TAC[fan7] THEN
220 `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN
221 GEOM_TRANSLATE_TAC[]);;
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[]);;
235 add_translation_invariants
236 [GRAPH_TRANSLATION_EQ;
243 FAN7_TRANSLATION_EQ];;
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];;
255 let FAN_TRANSLATION_EQ = prove
257 FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=>
259 REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
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[]);;
267 add_translation_invariants [FAN_TRANSLATION_EQ];;
268 add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
270 let BASE_POINT_FAN_TRANSLATION_EQ = prove
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]);;
276 let BASE_POINT_FAN_LINEAR_IMAGE_EQ = prove
277 (`!f:real^M->real^N x V E.
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]);;
283 let SET_OF_EDGE_TRANSLATION_EQ = prove
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[]);;
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)`,
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
302 REWRITE_TAC[set_of_edge; lemma] THEN
303 GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
305 add_translation_invariants
306 [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];;
308 add_linear_invariants
309 [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
315 (*let hk=new_definition`hk((D:A->bool),(f:A->A),(n:A->A),(e:A->A),(k:num)) <=>
317 CARD D = 2 * k /\ (f permutes D) /\ (n permutes D) /\ (e permutes D )
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))`;;
328 (* ************************************************* *)
329 (* Proof remark rem:fan *)
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`,
334 THEN REWRITE_TAC[FAN;fan1;graph]
336 THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET)
338 THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`)
340 THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET)
341 THEN ASM_SET_TAC[]);;
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]));;
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[] );;
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
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]
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)
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[]);;
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`,
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[]);;
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[]));;
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]));;
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[]);;
409 let th3d=prove(`!x v u. ~(x=v)/\ ~(x=u) ==> DISJOINT {x} {v,u}`,
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]);;
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
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
426 STRIP_TAC THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1- (u':real)` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]));;
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]));;
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[]);;
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})`,
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]);;
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]);;
447 let remark1_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3).
449 FINITE (set_of_edge v V E)
450 /\({v,u} IN E <=> u IN set_of_edge v V 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]);;
458 (***************SIGMA_FAN*****************)
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)))`;;
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
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))`;;
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))
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)))
495 FINITE X /\ ~(X = {})
496 ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
497 MESON_TAC[INF_FINITE]) in
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
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
504 ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
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)={})`)
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
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
516 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
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
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*)));;
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`;;
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))
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)))
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
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)={})`)
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
554 ASM_TAC THEN SET_TAC[];(*4*)
555 ASM_TAC THEN SET_TAC[](*4*)];
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
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
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*)));;
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))
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)`,
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[]);;
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))
592 ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
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} )`)
596 MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN)
599 ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
604 let AFF_GE_2_1 = prove
607 ==> aff_ge {x,v} {w} =
611 y = t1 % x + t2 % v + t3 % w}`,
614 let AFF_GE_1_2 = prove
617 ==> aff_ge {x} {v,w} =
619 &0 <= t2 /\ &0 <= t3 /\
621 y = t1 % x + t2 % v + t3 % w}`,
623 let AFF_GE_1_1 = prove
630 y = t1 % x + t2 % v }`,
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})
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))`)
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[]]);;
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}
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
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*)
686 SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC
688 ASM_TAC THEN SET_TAC[];(*2*)
690 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`)
692 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
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*)
700 SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
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*)
707 ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*)
709 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC
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 `
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*)
726 SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC
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*));;
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)
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[] );;
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)
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[] );;
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)`,
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]
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
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
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[]]));;
812 let CYCLIC_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
814 ==> cyclic_set (set_of_edge v V E) x v`,
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*)
822 THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*)
823 STRIP_TAC THENL(*3*)[
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
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*)
844 ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*)
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})`
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*)
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*)
862 ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
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`,
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[]);;
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}`,
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
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`])
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
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[];
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[];
905 THEN POP_ASSUM MP_TAC
906 THEN POP_ASSUM MP_TAC
907 THEN DISCH_THEN(LABEL_TAC"a")
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`]
913 THEN SUBGOAL_THEN `(u:real^3) IN affine hull {(x:real^3),(v:real^3)}` ASSUME_TAC
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`;];
920 MP_TAC(ISPECL[`u:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`]th)
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}`,
930 (let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in
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]));;
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
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])));;
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
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]));;
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}`,
964 MESON_TAC[property_of_cyclic_set;property_of_cyclic_set2;property_of_cyclic_set1;property_of_cyclic_set3]);;
968 let XOHLED=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
970 ==> cyclic_set (set_of_edge v V E) x v`,
971 MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
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)}`;;
979 (* d2_fan not yet used *)
981 let d2_fan=new_definition`d2_fan (x,V,E)={ (x',v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
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`;;
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)))`;;
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) )`;;
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))))`;;
995 (* i_fan corrects the 4th coordinate to be
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)))`;;
1000 let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
1002 let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
1004 let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
1006 let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
1008 (* if f = sigma, the power_map_points gives
1009 iterates of sigma (for fixed x v) *)
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))`;;
1014 (* This is the composition operator (o),
1015 specialized to functions on 4-tuples *)
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))))`;;
1019 (* powers of permutations *)
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))`;;
1024 (* powers of node map *)
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))))`;;
1032 (* the node of a dart, in a special form
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)}`;;
1039 (* The set X(V,E) *)
1041 let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
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))}`;;
1048 W^0_{dart}(x,v,w...)
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)
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 {}))`;;
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`,
1069 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points]
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]]]);;
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]);;
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]);;
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)
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
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]);;
1111 (*-------------------------------------------------------------------------------------------*)
1112 (* the properties in normal vector *)
1113 (*-------------------------------------------------------------------------------------------*)
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[]]]);;
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]]);;
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
1136 [ASM_MESON_TAC[imp_norm_gl_zero_fan];
1137 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]);;
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]]);;
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[]]]]);;
1158 (*---------------------------------------------------------------------------------------*)
1159 (* the normal coordinate is the definiton of frame in flyspeck(above JBDNJJB) *)
1160 (*---------------------------------------------------------------------------------------*)
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))`;;
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))) `;;
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))`;;
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`]);;
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`]);;
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`]]);;
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
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 ];
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]]);;
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);;
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);;
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] );;
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] );;
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);;
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]);;
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);;
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);;
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})
1253 (v - x) cross (e3_fan x v u) = vec 0`,
1255 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e3_fan;CROSS_RMUL;CROSS_REFL] THEN VECTOR_ARITH_TAC);;
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
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]]);;
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);;
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
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]
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]));;
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))
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
1330 STRIP_TAC THEN SUBGOAL_THEN `((y:real) - (r:real))* (y + r) = &0` ASSUME_TAC
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[]
1339 [POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1340 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]];
1342 DISCH_TAC THEN ASM_REWRITE_TAC[]
1343 THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
1347 (****************************************************************************)
1348 (* some properties of azim in the orthonormal frame *)
1349 (****************************************************************************)
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}
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.
1360 (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (v - x) /\
1362 (r2 * cos (psi + y)) % e1 +
1363 (r2 * sin (psi + y)) % e2 +
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
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[]
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
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`]
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*)
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
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
1448 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*4*)
1449 POP_ASSUM MP_TAC THEN STRIP_TAC
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])
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
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`]
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
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*)]]]]]);;
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}))
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
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
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[]
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[]]]]);;
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]);;
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)
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`]
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);;
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)
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
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
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
1592 THENL[ASM_MESON_TAC[];
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[]
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]);;
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]);;
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`,
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}`]
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]
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`])
1638 (****************************************************************************)
1639 (* the conditions to add azim *)
1640 (****************************************************************************)
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
1649 azim x v u w2 = azim x v u w1+ azim x v w1 w2
1651 ( let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
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
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];
1666 MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim)
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
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
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];
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`]
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)
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)})
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
1710 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a")
1712 THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b")
1714 THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
1716 THEN USE_THEN "b" MP_TAC THEN
1717 GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
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)
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
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
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
1742 ASM_MESON_TAC[REAL_LE_ADD];
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`]])));;
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
1751 azim x v u w2 = azim x v u w1 + azim x v w1 w2
1754 (let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in
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
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)
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]));;
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)})
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
1811 REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
1813 REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a1")
1815 THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b1")
1817 THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC
1819 THEN USE_THEN "b1" MP_TAC THEN
1820 GEN_REWRITE_TAC ( LAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
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)
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)
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
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)})
1864 azim x v u w2 = azim x v u w1 + azim x v w1 w2
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)`)
1869 SUBGOAL_THEN`azim x v w1 w2 = &0` ASSUME_TAC
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;
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
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
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)`)
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]]
1899 (****************************************************************************)
1900 (* sigma_fan is permutes *)
1901 (****************************************************************************)
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
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)})`)
1911 EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*)
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})`)
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*)
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)`)
1926 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC
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
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
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)`)
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*)
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)`)
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)`)
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)`)
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[]]]]);;
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)
1985 (sigma_fan x V E v u= sigma_fan x V E v w)
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}))`)
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*)
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}))`)
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*)
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`)
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*)
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)`)
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*)
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)`)
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*)
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)`)
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*)
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*)
2071 ASM_REWRITE_TAC[](*3*)]]]);;
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)
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
2086 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan];
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]]]);;
2104 (****************************************************************************)
2105 (* inverse of sigma_fan *)
2106 (****************************************************************************)
2121 let exists_function_inverse_sigma_fan_alt=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
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))
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[]
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
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[]);;
2142 This is the same as inverse_sigma_fan_alt,
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)`;;
2154 let INVERSE1_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
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[]);;
2162 (* This is the same as f_fan,
2163 but easier to use *)
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) )`;;
2168 (* Proof Lemma 6.1 [AAUHTVE] *)
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]);;
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
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[]
2190 let MONO_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
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)`,
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;]);;
2203 let SUR_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2205 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,
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[]);;
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]);;
2222 let SUR_F1_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
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;]
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})`)
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]);
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}`]];
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[]]);;
2254 let MONO_F1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
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[]);;
2261 let MONO_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
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[]);;
2268 let SUR_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2270 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,
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}`]);;
2283 let permuters_of_enf_fan=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
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]);;
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[]);;
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]);;
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[]);;
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[]);;
2334 (* from hypermap.hl *)
2336 (******************************)
2337 parse_as_infix("POWER",(24,"right"));;
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)`;;
2343 let POWER_0 = prove(`!f:A->A. f POWER 0 = I`,
2344 REWRITE_TAC[POWER]);;
2346 let POWER_1 = prove(`!f:A->A. f POWER 1 = f`,
2347 REWRITE_TAC[POWER; ONE; I_O_ID]);;
2349 let POWER_2 = prove(`!f:A->A. f POWER 2 = f o f`,
2350 REWRITE_TAC[POWER; TWO; POWER_1]);;
2352 let orbit_map = new_definition `orbit_map (f:A->A) (x:A) = {(f POWER n) x | n >= 0}`;;
2353 (**************************************************)
2355 let POWER_RIGHT=prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
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
2360 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;
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) )`,
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] ]);;
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)]));;
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)) `,
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]
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[]);;
2406 (**********************)
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) ={})}`;;
2411 let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
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))`;;
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))`;;
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))`,
2430 THEN DISCH_THEN(LABEL_TAC"EM")
2431 THEN USE_THEN "EM" MP_TAC
2432 THEN REWRITE_TAC[FAN;fan1]
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[]);;
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))`,
2458 THEN DISCH_THEN(LABEL_TAC"EM")
2459 THEN USE_THEN "EM" MP_TAC
2460 THEN REWRITE_TAC[FAN;fan1]
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]);;
2472 let finite_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
2474 ==> FINITE (d_fan (x,V,E))`,
2476 THEN REWRITE_TAC[d_fan;FINITE_UNION]
2478 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
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[]);;
2485 let FACE_FAN_NOT_EMPTY=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
2487 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
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`]
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
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)))`,
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))`)
2515 THEN POP_ASSUM MP_TAC
2516 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
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[]]);;
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)))`,
2537 THEN POP_ASSUM MP_TAC
2538 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
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[]);;
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))`,
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))`]
2561 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
2562 THEN REPEAT STRIP_TAC
2563 THEN ASM_REWRITE_TAC[];
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[]]]);;
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)))`,
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))`)
2587 THEN POP_ASSUM MP_TAC
2588 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
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}`]
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}`]
2611 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2612 THEN ASM_REWRITE_TAC[]]);;
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)))`,
2620 THEN ASM_REWRITE_TAC[]
2621 THEN POP_ASSUM MP_TAC
2622 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
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}`]
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}`]
2640 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2641 THEN ASM_REWRITE_TAC[]);;
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))`,
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))`]
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))`)
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[]]]);;
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)))`,
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))`)
2687 THEN POP_ASSUM MP_TAC
2688 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
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`]]);;
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)))`,
2710 THEN POP_ASSUM MP_TAC
2711 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
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`]);;
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))`,
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))`]
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))`)
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[]]]);;
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`,
2758 THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
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
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`]));;
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)
2782 THEN ASM_REWRITE_TAC[res;]);;
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`)]);;
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)`;]);;
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`)]);;
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)`;]);;
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`,
2856 THEN MATCH_MP_TAC EQ_EXT
2857 THEN ASM_REWRITE_TAC[I_THM;o_DEF]
2859 THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
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` )
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` )
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` )]);;
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`]);;
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)`,
2912 THEN POP_ASSUM MP_TAC
2913 THEN REWRITE_TAC[d1_fan; IN_ELIM_THM]
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}`]
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}`]
2927 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2928 THEN ASM_REWRITE_TAC[]);;
2932 let face_subset_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
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`]);;
2944 let properties_of_elements_in_face_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
2946 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
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)`)
2953 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM]
2955 THEN ASM_REWRITE_TAC[pr2;pr3]);;
2957 let fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2959 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2960 ==> d20_fan(x,V,E)={}`,
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]
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);;
2972 let dartset_fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
2974 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2975 ==> d_fan(x,V,E)=d1_fan(x,V,E)`,
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;]
2982 let properties_of_elements_in_face_fully_surroundedfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
2984 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
2985 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
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)`)
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]
2996 THEN ASM_REWRITE_TAC[pr2;pr3]);;
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)
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))`,
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]);;
3017 (********************************)