(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)



(*flyspeck_needs "general/sphere.hl";;*)


module Fan  = struct


(*
# use "/home/truong/Desktop/googlecode/hol_light/hol.ml";;
needs "/home/truong/Desktop/googlecode/hol_light/Multivariate/flyspeck.ml";;
needs "/home/truong/Desktop/googlecode/flyspeck/text_formalization/general/sphere.hl";;
*)

		
open Sphere;;
open Fan_defs;;
open Tactic_fan;;
open Lemma_fan;;		
open Hypermap;;


(* ========================================================================== *)
(*                                FAN                       *)
(* ========================================================================== *)



let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
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 ={}))`;;
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)`;;
let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
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})
==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
fan6(x,V,E)/\ fan7(x,V,E)`;;
(* ========================================================================== *) (* Invariance theorems *) (* ========================================================================== *)
let GRAPH = 
prove (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
REWRITE_TAC[graph; IN]);;
let CYCLIC_SET = 
prove (`cyclic_set W v w <=> ~(v = w) /\ FINITE W /\ (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\ W INTER affine hull {v, w} = {}`,
REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
let CYCLIC_SET_TRANSLATION_EQ = 
prove (`!a:real^N s x y. cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
let CYCLIC_SET_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s x y. linear f /\ (!x y. f x = f y ==> x = y) ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];; add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
let GRAPH_TRANSLATION_EQ = 
prove (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
let GRAPH_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N E. linear f /\ (!x y. f x = f y ==> x = y) ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
let FAN1_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan1(x,V,E)`,
REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
let FAN1_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
let FAN2_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan2(x,V,E)`,
REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
let FAN2_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
let FAN3_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan3(x,V,E)`,
REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
let FAN3_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s} =
     IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
let FAN4_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan4(x,V,E)`,
REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
let FAN4_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
let FAN5_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan5(x,V,E)`,
REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
let FAN5_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
let FAN6_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan6(x,V,E)`,
REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
let FAN6_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
let FAN7_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan7(x,V,E)`,
REWRITE_TAC[fan7] THEN REWRITE_TAC[SET_RULE `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN GEOM_TRANSLATE_TAC[]);;
let FAN7_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
REWRITE_TAC[fan7; IN_UNION] THEN REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [GRAPH_TRANSLATION_EQ; FAN1_TRANSLATION_EQ; FAN2_TRANSLATION_EQ; FAN3_TRANSLATION_EQ; FAN4_TRANSLATION_EQ; FAN5_TRANSLATION_EQ; FAN6_TRANSLATION_EQ; FAN7_TRANSLATION_EQ];; add_linear_invariants [GRAPH_LINEAR_IMAGE_EQ; FAN1_LINEAR_IMAGE_EQ; FAN2_LINEAR_IMAGE_EQ; FAN3_LINEAR_IMAGE_EQ; FAN4_LINEAR_IMAGE_EQ; FAN5_LINEAR_IMAGE_EQ; FAN6_LINEAR_IMAGE_EQ; FAN7_LINEAR_IMAGE_EQ];;
let FAN_TRANSLATION_EQ = 
prove (`!a:real^N x V E. FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> FAN(x,V,E)`,
REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
let FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [FAN_TRANSLATION_EQ];; add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
let BASE_POINT_FAN_TRANSLATION_EQ = 
prove (`!a x V E. base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) = a + base_point_fan(x,V,E)`,
REWRITE_TAC[base_point_fan]);;
let BASE_POINT_FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) = f(base_point_fan(x,V,E))`,
REWRITE_TAC[base_point_fan]);;
let SET_OF_EDGE_TRANSLATION_EQ = 
prove (`!a:real^N x V E. set_of_edge (a + x) (IMAGE (\x. a + x) V) (IMAGE (IMAGE (\x. a + x)) E) = IMAGE (\x. a + x) (set_of_edge x V E)`,
REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
let SET_OF_EDGE_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) = IMAGE f (set_of_edge x V E)`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
     {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[set_of_edge; lemma] THEN
  GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
add_translation_invariants [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];; add_linear_invariants [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];;
let CTVTAQA=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (E1:(real^3->bool)->bool). FAN(x,V,E) /\ E1 SUBSET E ==> FAN(x,V,E1)`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7;graph] THEN ASM_SET_TAC[]);;
(* ========================================================================== *) (* SET_OF_EDGE *) (* ========================================================================== *)
let set_of_edge_subset_edges=
prove(`!(V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). set_of_edge v V E SUBSET V`,
REWRITE_TAC[set_of_edge] THEN SET_TAC[]);;
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))`,
(
let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM]  THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
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)`,
REPEAT GEN_TAC THEN DISCH_TAC 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) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
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 ==> ({v,u} IN E <=> u IN set_of_edge v V E)`,
REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
let expand_edge_graph_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (e:real^3->bool). FAN(x,V,E) /\ e IN E ==> ?v:real^3 w:real^3. e={v,w}`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;IN] THEN STRIP_TAC THEN FIND_ASSUM MP_TAC `graph (E:(real^3->bool)->bool)` THEN REWRITE_TAC[graph] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`e:real^3->bool`th)) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC THEN SUBGOAL_THEN `~((e:real^3->bool)={})` ASSUME_TAC THENL[ STRIP_TAC THEN MP_TAC(ISPEC`(e:real^3->bool)`CARD_EQ_0) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(SET_RULE `~((e:real^3->bool)={})==> ?v:real^3. v IN e`) THEN RESA_TAC THEN SUBGOAL_THEN`~((e:real^3->bool) DELETE v={})` ASSUME_TAC THENL[ STRIP_TAC THEN MP_TAC(ISPECL[`v:real^3`;`(e:real^3->bool)`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(ISPECL[`(e:real^3->bool)`;`v:real^3`] FINITE_DELETE) THEN RESA_TAC THEN MP_TAC(ISPEC`(e:real^3->bool) DELETE v`CARD_EQ_0) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(SET_RULE `~((e:real^3->bool)DELETE v={})==> ?w:real^3. w IN (e:real^3->bool)DELETE v/\ w IN e`) THEN RESA_TAC THEN MP_TAC(SET_RULE `(v IN (e:real^3->bool))/\ (w IN (e:real^3->bool))==> {v,w} SUBSET e`) THEN RESA_TAC THEN MP_TAC(SET_RULE `(w IN (e:real^3->bool)DELETE v)==> ~(v=w)`) THEN RESA_TAC THEN MP_TAC(ISPECL [`{v:real^3,w:real^3}`;`(e:(real^3->bool))`] FINITE_SUBSET) THEN RESA_TAC THEN ASSUME_TAC(SET_RULE `v:real^3 IN {v:real^3,w:real^3} `) THEN MP_TAC(ISPECL[`v:real^3`;`{v:real^3,w:real^3}`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(SET_RULE `v IN {v,w}==>{v:real^3,w:real^3} DELETE v PSUBSET {v,w}`) THEN RESA_TAC THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v`;`{v:real^3,w:real^3}`]CARD_PSUBSET) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`FINITE {v:real^3,w:real^3}` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN DISCH_TAC THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v) < CARD {v, w}/\ CARD ({v, w} DELETE v) = CARD {v, w}-1 <=>CARD ({v, w} DELETE v) +1= CARD {v:real^3, w:real^3}`) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;]) THEN REWRITE_TAC[ARITH_RULE`A=A`] THEN DISCH_TAC THEN SUBGOAL_THEN `w:real^3 IN ({v:real^3,w:real^3} DELETE v)` ASSUME_TAC THENL[ ASM_SET_TAC[]; MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`v:real^3`] FINITE_DELETE) THEN RESA_TAC THEN MP_TAC(ISPECL[`w:real^3`;`{v:real^3,w:real^3} DELETE v`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(SET_RULE `w IN ({v,w} DELETE v)==>{v:real^3,w:real^3} DELETE v DELETE w PSUBSET {v,w} DELETE v`) THEN RESA_TAC THEN MP_TAC(ISPECL[`{v:real^3,w:real^3} DELETE v DELETE w`;`{v:real^3,w:real^3} DELETE v`]CARD_PSUBSET) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN FIND_ASSUM MP_TAC`FINITE ({v:real^3,w:real^3} DELETE v)` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN DISCH_TAC THEN MP_TAC(ARITH_RULE`CARD ({v, w} DELETE v DELETE w) < CARD ({v, w} DELETE v)/\ CARD ({v, w} DELETE v DELETE w) = CARD ({v, w} DELETE v)-1 <=>CARD ({v, w} DELETE v DELETE w) +1= CARD ({v:real^3, w:real^3} DELETE v)`) THEN POP_ASSUM (fun th->REWRITE_TAC[th]) THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th;]) THEN REWRITE_TAC[ARITH_RULE`A=A`] THEN DISCH_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[]) THEN POP_ASSUM (fun th->REWRITE_TAC[]) THEN ASSUME_TAC(SET_RULE `{v, w} DELETE v:real^3 DELETE w:real^3={}`) THEN POP_ASSUM (fun th->REWRITE_TAC[th;CARD_CLAUSES; ARITH_RULE `0+1=1`]) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"B") THEN DISCH_TAC THEN REMOVE_THEN "B" MP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th);ARITH_RULE` 1+1=2`]) THEN FIND_ASSUM MP_TAC`CARD (e:real^3->bool)=2` THEN DISCH_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN DISCH_TAC THEN MP_TAC(ISPECL[`{v:real^3,w:real^3}`;`e:real^3->bool`]CARD_SUBSET_EQ) THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)]) THEN RESA_TAC THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`w:real^3` THEN POP_ASSUM (fun th->REWRITE_TAC[SYM(th)])]]]);;
let add_edge_graph_fan=
prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A. v IN V /\ u IN V /\ E1=E UNION {{v,u}} /\ UNIONS E SUBSET V==> UNIONS E1 SUBSET V`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[UNIONS; SUBSET; UNION; IN_ELIM_THM;IN_SING] THEN DISCH_THEN(LABEL_TAC "YEU") THEN REPEAT STRIP_TAC THENL[SUBGOAL_THEN`(?u. u IN E /\ x IN (u:A->bool))`ASSUME_TAC THENL[ EXISTS_TAC`u':A->bool` THEN ASM_REWRITE_TAC[]; REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `x:A`)]; ASM_TAC THEN SET_TAC[]]);;
let garph_add_edge_is_garph=
prove(`!(V:A->bool) (E:(A->bool)->bool) v:A u:A. E1=E UNION {{v,u}} /\ ~(v=u) /\ graph E==> graph E1`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[GRAPH; UNION;IN_ELIM_THM;IN_SING] THEN DISCH_THEN(LABEL_TAC"YEU") THEN GEN_TAC THEN STRIP_TAC THENL[REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `e:A->bool`); ASM_REWRITE_TAC[HAS_SIZE] THEN STRIP_TAC THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`] THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY]]);;
let add_edge_into_collinear_fan=
prove(`!x:real^3 (E:(real^3->bool)->bool) v:real^3 u:real^3. ~collinear {x,v,u} /\ (!e. e IN E ==> ~collinear ({x} UNION e)) ==> (!e. e IN E UNION {{v, u}} ==> ~collinear ({x} UNION e))`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)[UNION;] THEN REWRITE_TAC[IN_ELIM_THM;IN_SING] THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU") THEN STRIP_TAC THENL[REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th `e:real^3->bool`); ASM_REWRITE_TAC[SET_RULE`{X} UNION {A,B}={X,A,B}`]]);;
let properties_edges_eq_fan=
prove(`!e:A-> bool v:A u:A. FINITE e /\ ~(e={v,u}) /\ ~(v=u) /\ CARD e=2 ==> ~(v IN e)\/ ~(u IN e)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "YEU") THEN ONCE_REWRITE_TAC[SET_RULE`~A \/ ~B<=> ~(A/\B)`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`v IN e /\ u IN e ==> {v:A,u} SUBSET e`) THEN RESA_TAC THEN MRESA_TAC CARD_2_FAN[`v:A`;`u:A`] THEN REMOVE_THEN "YEU" MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)]) THEN STRIP_TAC THEN MRESA_TAC CARD_SUBSET_EQ[`{v,u:A}`;`e:A->bool`]);;
(* ========================================================================== *) (* BASIC FAN *) (* ========================================================================== *)
let set_edges_is_finite_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> FINITE E`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1;graph] THEN STRIP_TAC THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET) THEN RESA_TAC THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`) THEN RESA_TAC THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET) THEN ASM_SET_TAC[]);;
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) ==> ({v,u} IN E <=> u IN set_of_edge v V E)`,
REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
let properties_of_graph=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==> v IN V`,
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 REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
let properties_of_graph1=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==> u IN V`,
ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SET_TAC[properties_of_graph]);;
let th4=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
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[]);;
let remark4_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). 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})`,
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]);;
let collinears_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
MESON_TAC[remark4_fan;collinear_fan]);;
let remark1_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) ==> FINITE (set_of_edge v V E) /\({v,u} IN E <=> u IN set_of_edge v V E)/\ ({v,u} IN E==> ~ collinear {x,v,u}/\ ~ (x=v) /\ ~(x=u)/\ ~(v=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v}) /\ v IN V /\ u IN V/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
(* ========================================================================== *) (* EXISTS SIGMA_FAN *) (* ========================================================================== *)
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)=  
(if (set_of_edge v V E = {u} ) then u 
    else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
(* This extends sigma to have a larger domain of R^3 rather than just V. It is the identity outside V (compare the definition of `permutes` ). *)
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)=  
(if ~(u IN set_of_edge v V E ) then u 
    else (sigma_fan x V E v u))`;;
let exists_sigma_fan=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`,
(
let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in


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
  
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)
ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)

DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[]](*4*);(*3*)
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
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)

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
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
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)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;
let SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> ((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\ (!(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)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan] 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[]);;
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). FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
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} )`) THENL[ MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN) THEN ASM_TAC THEN SET_TAC[]; ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
(* ========================================================================== *) (* CONDITION UNIQUE FOINT AND SIGMA_FAN *) (* ========================================================================== *)
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. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v}) ==> u=w`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th)) THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;] THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`) THENL [ 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[]; ASM_TAC THEN SET_TAC[]]);;
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. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u} ==> u=w`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN 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` THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (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 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC THENL (*1*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_10) THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*) SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC THENL (*2*)[ ASM_TAC THEN SET_TAC[];(*2*) POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`) THENL (*3*)[ SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*) SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC THENL (*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` 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*) ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*) SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))` THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)` 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 THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN 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 MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH` (inv t3 * --t1) % x + (inv t3 * --t2) % v + inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u ` ] THEN DISCH_TAC 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*) SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL (*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` 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*) ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;
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. 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) ==> w=w1`,
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 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_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 ASSUME_TAC(th)) THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) 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}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 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[] );;
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. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0) ==> u=w`,
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 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_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 ASSUME_TAC(th)) 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}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 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[] );;
let UNIQUE_SIGMA_FAN=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) /\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1) ==> sigma_fan x V E v u=w)`,
(
let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
) in

ASSUME_TAC(th) THEN
REPEAT GEN_TAC  THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN 
DISCH_TAC  THEN DISCH_THEN(LABEL_TAC "1") 
  THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4") 
  THEN DISCH_THEN(LABEL_TAC"a") 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN) 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  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)) 
  THEN ASM_REWRITE_TAC[]
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[] 
  THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
  THEN REPEAT DISCH_TAC
  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
THENL[
REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
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)) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
REMOVE_THEN"1" MP_TAC 
THEN  REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
  THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC 
  THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
  THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  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))
  THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC  
  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 )
  THEN ASM_REWRITE_TAC[]
  THEN ASM_MESON_TAC[]]));;
(* ========================================================================== *) (* CYCLIC SET FAN *) (* ========================================================================== *)
let CYCLIC_SET_EDGE_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) /\ v IN V ==> cyclic_set (set_of_edge v V E) x v`,
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; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*) STRIP_TAC THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*) STRIP_TAC THENL(*3*)[ ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b") THEN STRIP_TAC THEN STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] 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*) ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*) REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC 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})` ASSUME_TAC THENL(*4*)[ ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b") THEN STRIP_TAC THEN STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) ) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*) EQ_TAC THENL(*5*)[ 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*) ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
let XOHLED=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) /\ v IN V ==> cyclic_set (set_of_edge v V E) x v`,
MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
(* ========================================================================== *) (* SIGMA_FAN IS PERMUTES (^_^) *) (* ========================================================================== *)
let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
let exists_inverse_sigma_fan_alt=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <= azim1 x v u w1))) `,
(
let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in
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
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)

ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[](*4*)];

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
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
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
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
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)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;
let  SUR_SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). FAN(x,V,E) /\ ({v,u} IN E) ==> ?w. {v,w} IN E /\sigma_fan x V E v w= u `,
REPEAT GEN_TAC THEN STRIP_TAC 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)})`) THENL(*1*)[ EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*) 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 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 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[] 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) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC 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})`) THENL(*2*)[ 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*) ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN 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)`) THENL(*3*)[ ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC THENL(*4*)[ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*) SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC THENL(*5*)[ ASM_TAC THEN SET_TAC[];(*5*) 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 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 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 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) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 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[] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*) POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN 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)`) THENL(*7*)[ 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) THEN ASM_TAC THEN SET_TAC[];(*7*) 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)`) THENL(*8*)[ 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) THEN ASM_TAC THEN SET_TAC[];(*8*) MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3. w1 IN set_of_edge v V E /\ ~(w1 = u) ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1` THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`) THENL(*9*)[ 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)`) THENL(*10*)[ 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*) POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*) SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*) REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*); ASM_TAC THEN SET_TAC[]]]]);;
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). FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ (sigma_fan x V E v u= sigma_fan x V E v w) ==> u=w `,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") THEN 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 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}))`) THENL(*1*)[ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM] THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th)) THEN ASM_TAC THEN SET_TAC[];(*1*) 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}))`) THENL(*2*)[ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM] THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_TAC THEN SET_TAC[];(*2*) MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th)) THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th)) THEN ASM_REWRITE_TAC[] 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) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) 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)) THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`) THENL(*3*)[ 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 THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*) MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 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) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC 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 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)`) THENL(*5*)[ 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) THEN ASM_TAC THEN SET_TAC[];(*5*) 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)`) THENL(*6*)[ 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) THEN ASM_TAC THEN SET_TAC[];(*6*) 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)`) THENL(*7*)[ 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) THEN ASM_TAC THEN SET_TAC[];(*7*) 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) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`] 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 (*7*)](*6*)](*5*)](*4*)];(*3*) ASM_REWRITE_TAC[](*3*)]]]);;
let permutes_sigma_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). FAN(x,V,E) /\ ({v,u} IN E) ==> (extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
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 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 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) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL[ GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan]; STRIP_TAC THENL[ 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)})`) THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING]; ASM_MESON_TAC[SIGMA_FAN]]; REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;
(* ========================================================================== *) (* INVERSE OF SIGMA_FAN *) (* ========================================================================== *)
let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
let exists_function_inverse_sigma_fan_alt=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) ==> (?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E) /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w) /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)) `,
REPEAT STRIP_TAC THEN 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 ASM_REWRITE_TAC[] THEN DISCH_TAC 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) 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 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] SUR_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
(* This is the same as inverse_sigma_fan_alt, but easier to use. *)
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)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
/\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
let INVERSE1_SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) ==> ( (!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) /\ (!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) /\ (!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))`,
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) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
(* ========================================================================== *) (* PROPERTIES OF FAN *) (* ========================================================================== *)
let properties_of_fan7=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3 u1:real^3. FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1,u1} ==> v = v1 \/ v = u1`,
REPEAT STRIP_TAC THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)` THEN REWRITE_TAC[FAN; fan6; fan7] THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3),(u1:real^3)}`]th)) THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;] THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL(*1*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real` THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC; DISCH_TAC THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u} /\ v IN aff_ge {x} {v1, u1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1, u1:real^3}`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(SET_RULE`{v, u} INTER {v1, u1:real^3}={} \/ ~({v, u} INTER {v1, u1}={})`) THENL(*2*)[ ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC THENL(*3*)[ ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`) THEN AFF_TAC; ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC THEN ASM_REWRITE_TAC[]];(*2*) DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1, u1:real^3}) \/ (v IN {v, u} INTER {v1, u1})`) THENL(*3*)[ SUBGOAL_THEN`({v:real^3, u} INTER {v1, u1}={u})` ASSUME_TAC THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*) ASM_REWRITE_TAC[] THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC THENL(*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1) THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*5*) FIND_ASSUM MP_TAC`{v,u:real^3} IN E` THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN DISCH_TAC THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`u:real^3`] THEN ASM_TAC THEN SET_TAC[]]];(*3*) POP_ASSUM MP_TAC THEN SET_TAC[]]]]) ;;
let properties1_of_fan7=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 v1:real^3 u1:real^3. FAN(x,V,E)/\ {v,u} IN E /\ {v1,u1} IN E /\ v IN aff_ge {x} {v1} ==> v = v1`,
REPEAT STRIP_TAC THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)` THEN REWRITE_TAC[FAN; fan6; fan7] THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`v:real^3`] THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u1:real^3`;`v1:real^3`] THEN MP_TAC(SET_RULE`(v1:real^3) IN V==> (?v. v IN V /\ {v1} = {v})`) THEN REDA_TAC THEN STRIP_TAC THEN POP_ASSUM (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v1:real^3)}`]th)) THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;] THEN SUBGOAL_THEN `(v:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL(*1*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN EXISTS_TAC `&0:real` THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &1 % w + &0 % v `] THEN REAL_ARITH_TAC; DISCH_TAC THEN MP_TAC(SET_RULE`v IN aff_ge {x} {v, u:real^3} /\ v IN aff_ge {x} {v1} ==> v IN aff_ge {x} {v, u} INTER aff_ge {x:real^3} {v1}`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(SET_RULE`{v, u:real^3} INTER {v1}={} \/ ~({v, u} INTER {v1}={})`) THENL(*2*)[ ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`aff_ge {x:real^3} {}= {y| ?t1. t1= &1 /\ y= t1 %x}` ASSUME_TAC THENL(*3*)[ ASSUME_TAC(SET_RULE `DISJOINT {x:real^3} {}`) THEN AFF_TAC; ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REDUCE_VECTOR_TAC THEN ASM_REWRITE_TAC[]];(*2*) DISJ_CASES_TAC(SET_RULE`~(v IN {v, u} INTER {v1:real^3}) \/ (v IN {v, u} INTER {v1})`) THENL(*3*)[ SUBGOAL_THEN`({v:real^3, u} INTER {v1:real^3}={u})` ASSUME_TAC THENL(*4*)[ ASM_TAC THEN SET_TAC[]; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(u:real^3)} SUBSET aff {x,u}` ASSUME_TAC THENL(*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (u:real^3)`;]AFF_GE_1_1) THEN MP_TAC(SET_RULE`~((x:real^3) = (u:real^3))==> DISJOINT {x} {u}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[]; FIND_ASSUM MP_TAC`{v,u:real^3} IN E` THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN DISCH_TAC THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN ASM_TAC THEN SET_TAC[]]];(*3*) POP_ASSUM MP_TAC THEN SET_TAC[]]]]) ;;
let expand_elements_by_azim_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 x1:real x2:real x3:real. FAN(x,V,E)/\ {v,u} IN E /\ &0 < x1 /\ &0<= x2 /\ x2 < &2 * pi /\ &0< x3 /\ x3 < pi/ &2 ==> azim x v u (x + (x1 * cos (x2) * sin (x3)) % e1_fan x v u + (x1 * sin (x2) * sin (x3)) % e2_fan x v u + (x1 * cos (x3)) % e3_fan x v u) = x2`,
(
let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
 (let lem1=prove(`!x v u. {x,v,u}= {v,x,u}`,SET_TAC[]) in

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`]remark1_fan)
THEN RESA_TAC
THEN FIND_ASSUM MP_TAC`~collinear {(x:real^3),(v:real^3),(u:real^3)}`
THEN GEN_REWRITE_TAC( LAND_CONV  o ONCE_DEPTH_CONV)[lem1]
THEN ONCE_REWRITE_TAC[COLLINEAR_3]
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]orthonormal_e1_e2_e3_fan)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th))
THEN REWRITE_TAC[orthonormal]
THEN STRIP_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate)
THEN RESA_TAC
THEN MP_TAC(ISPEC`x3:real`SIN_POS_PI2)
THEN RESA_TAC
THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`(x +
  (x1 * cos (x2) * sin (x3)) % e1_fan x v u +
  (x1 * sin (x2) * sin (x3)) % e2_fan x v u +
  (x1 * cos (x3)) % e3_fan (x:real^3) (v:real^3) (u:real^3))`;
  `((u-x) dot (e3_fan (x:real^3) (v:real^3) (u:real^3))) *inv (norm((v:real^3)-(x:real^3)))`;
  `(x1 * cos (x3)) * (inv (norm((v:real^3)-(x:real^3))))`;
`((u-x) dot (e1_fan (x:real^3) (v:real^3) (u:real^3)))`;
`x1 * sin (x3:real)`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`&0`;`x2:real`]AZIM_UNIQUE)
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`&0+a=a`;]
THEN STRIP_TAC
THENL[
MATCH_MP_TAC REAL_LT_MUL
THEN REPEAT(POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

STRIP_TAC
THENL[

REWRITE_TAC[SIN_0;COS_0;VECTOR_ARITH`(A*B)%C=A%(B%C)`]
THEN REDUCE_ARITH_TAC
THEN REDUCE_VECTOR_TAC
THEN ONCE_REWRITE_TAC[GSYM e3_fan]
THEN MATCH_MP_TAC(ISPECL[`e3_fan (x:real^3) (v:real^3) (u:real^3)`;`(u:real^3)-(x:real^3)`;`
((u - x) dot e1_fan x v u) % (e1_fan (x:real^3) (v:real^3) (u:real^3)) +
 ((u - x) dot e3_fan x v u) % (e3_fan x v u)`]CROSS_DOT_CANCEL)
THEN ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_SYM]
THEN REDUCE_ARITH_TAC
THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_REFL]
THEN REDUCE_VECTOR_TAC
THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC[e1_fan]
THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;e2_fan]
THEN REWRITE_TAC[VECTOR_ARITH`A%(B%C)=(B*A)%C`]
THEN ONCE_REWRITE_TAC[DOT_SYM]
THEN ONCE_REWRITE_TAC[GSYM DOT_RMUL]
THEN ONCE_REWRITE_TAC[GSYM e2_fan]
THEN ASM_REWRITE_TAC[]
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`&0<(e1_fan x v u cross e2_fan x v u) dot e3_fan (x:real^3) (v:real^3) (u:real^3)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
THEN REWRITE_TAC[DOT_RZERO]
THEN REAL_ARITH_TAC;
REWRITE_TAC[e3_fan]
THEN VECTOR_ARITH_TAC]])));;
let one_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)/\ {v,u} IN E /\ ~(CARD (set_of_edge v V E) > 1) ==> set_of_edge v V E={u}`,
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`]remark1_fan) THEN RESA_TAC THEN MP_TAC(SET_RULE`(u:real^3) IN set_of_edge v V E==> ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={})/\ {(u:real^3)} SUBSET set_of_edge v V E`) THEN RESA_TAC THEN MP_TAC(ISPECL [`{(u:real^3)}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`] FINITE_SUBSET) THEN RESA_TAC THEN ASSUME_TAC(SET_RULE`u IN {(u:real^3)} /\ {(u:real^3)} DELETE u= {} /\ {} PSUBSET {(u:real^3)}`) THEN MP_TAC(ISPECL[`(u:real^3)`;`{(u:real^3)}`;]CARD_DELETE) THEN RESA_TAC THEN MP_TAC(ISPECL[`{}:real^3->bool`;`{(u:real^3)}`]CARD_PSUBSET) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[CARD_CLAUSES] THEN REPEAT DISCH_TAC THEN MP_TAC(ARITH_RULE` 0 = CARD ({(u:real^3)}) - 1 /\ 0 < CARD ({u}) <=> 1= CARD {u}`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`~(CARD (set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) > 1)==> CARD (set_of_edge v V E) <= 1`) THEN RESA_TAC THEN MP_TAC(ISPECL[`{u:real^3}`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]CARD_SUBSET_LE) THEN ASM_SET_TAC[]);;
end;;