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




module  Dwwutkw = struct



open Sphere;;
open Fan_defs;;
open Hypermap_of_fan;;
open Tactic_fan;;
open Lemma_fan;;		
open Fan;;
open Hypermap_of_fan;;
open Node_fan;;
open Azim_node;;
open Sum_azim_node;;
open Disjoint_fan;;
open Lead_fan;;
open Fan_misc;;
open Leads_into_fan;;
open Fully_surrounded;;
open Sin_azim_cross_dot;;
open Leads_intos;;
open Hypermap;;
open Dartset_leads_into;;






let condition_not_edge_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ e1 IN E /\ e2 = {v, u}
/\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
==> ~(e1=e2)`,



REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN STRIP_TAC
THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
THEN DISCH_TAC
THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
THENL[REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC `e1:real^3->bool`
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC(`(e1:real^3->bool) IN E`)
THEN REWRITE_TAC[IN]
THEN ASM_REWRITE_TAC[];
ASSUME_TAC(SET_RULE`aff_gt {x} {v, u} INTER
      (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
=aff_gt {x} {v, u} `)
THEN MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC 
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
THEN MATCH_MP_TAC exists_in_aff_gt
THEN ASM_REWRITE_TAC[]]);;


let condition_not_intersection_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds e1:real^3->bool e2:real^3->bool.
FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
/\ e1 IN E /\ e2 = {v, u}
==>aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,

REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
THEN DISCH_TAC
THEN SUBGOAL_THEN`aff_ge {x} e1 SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
THENL[
REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC `e1:real^3->bool`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC THEN SET_TAC[IN];
MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} e1 SUBSET xfan (x,V,E)
==> aff_gt {x} {v, u} INTER aff_ge {x} e1={}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`
aff_gt {x:real^3} {v, u} INTER aff_ge {x} e1={}==>
aff_ge {x} e1 INTER (aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u})
= (aff_ge {x} e1 INTER aff_ge {x} {v}) UNION (aff_ge {x} e1 INTER aff_ge {x} {u})`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`e1 IN E==> e1 IN E UNION {{v:real^3} | v IN V}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
THEN RESA_TAC
THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
THEN POP_ASSUM(fun th-> MRESA_TAC th [`e1:real^3->bool`;`{u:real^3}`])
THEN MRESA_TAC condition_not_edge_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`ds:real^3#real^3#real^3#real^3->bool`]
THEN FIND_ASSUM MP_TAC (`graph (E:(real^3->bool)->bool)`)
THEN REWRITE_TAC[GRAPH]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESAL1_TAC th `e1:real^3->bool`[HAS_SIZE])
THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MRESA_TAC properties_edges_eq_fan[`e1:real^3->bool`; `v:real^3`;`u:real^3`]
THENL[MP_TAC(SET_RULE`~(v IN e1)==> e1 INTER {v:real^3}={} /\ e1 INTER {v, u}=e1 INTER {u}`)
THEN RESA_TAC
THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {u}:real^3->bool`)
THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {u})`)
THEN RESA_TAC
THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {u}:real^3->bool`]
THEN POP_ASSUM MP_TAC THEN SET_TAC[];
MP_TAC(SET_RULE`~(u IN e1)==> e1 INTER {u:real^3}={} /\ e1 INTER {v, u}=e1 INTER {v}`)
THEN RESA_TAC
THEN ASSUME_TAC(SET_RULE`{} SUBSET e1 INTER {v}:real^3->bool`)
THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} (e1 INTER {v})`)
THEN RESA_TAC
THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`e1 INTER {v}:real^3->bool`]
THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;




let condition_not_intersection_point_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds:real^3#real^3#real^3#real^3->bool e1:real^3->bool w:real^3.
FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
/\ w IN V /\ e1 = {v, u}
==>aff_ge {x} e1 INTER aff_ge {x} {w} = aff_ge {x} (e1 INTER {w})`,

REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`]
THEN MRESA_TAC dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` ds:real^3#real^3#real^3#real^3->bool`]
THEN MP_TAC(SET_RULE`dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)/\ aff_gt {x} {v, u} SUBSET dartset_leads_into_fan x V E ds==> aff_gt {x} {v, u} SUBSET yfan (x:real^3,V,E)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[yfan; SET_RULE`A SUBSET (:real^3) DIFF B <=> A INTER B={}`;]
THEN DISCH_TAC
THEN SUBGOAL_THEN`aff_ge {x} {w} SUBSET xfan(x:real^3,V:real^3->bool,E)` ASSUME_TAC
THENL[
REWRITE_TAC[xfan;SUBSET;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC exists_edge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` w:real^3`]
THEN EXISTS_TAC `{w,v'}:real^3->bool`
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v':real^3)`;
` (w:real^3)`]
THEN MRESA_TAC aff_ge_eq_aff_gt_union_aff_ge[`(x:real^3)`;`(w:real^3)`;` (v':real^3)`]
THEN ASM_TAC THEN SET_TAC[IN];
MP_TAC(SET_RULE`aff_gt {x:real^3} {v, u} INTER xfan (x,V:real^3->bool,E) = {}/\aff_ge {x} {w} SUBSET xfan (x,V,E)
==> aff_gt {x} {v, u} INTER aff_ge {x} {w}={}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`
aff_gt {x:real^3} {v, u} INTER aff_ge {x} {w}={}==>
(aff_gt {x} {v, u} UNION aff_ge {x} {v} UNION aff_ge {x} {u}) INTER aff_ge {x} {w} 
= (aff_ge {x} {w} INTER aff_ge {x} {v}) UNION (aff_ge {x} {w} INTER aff_ge {x} {u})`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`w IN V==> {w} IN E UNION {{v:real^3} | v IN V}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`v:real^3 IN V==> {v} IN E UNION {{v} | v IN V}`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`u:real^3 IN V==> {u} IN E UNION {{v} | v IN V}`)
THEN RESA_TAC
THEN FIND_ASSUM MP_TAC(`FAN(x:real^3,V,E)`)
THEN REWRITE_TAC[FAN;fan7]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{v:real^3}`]THEN ASSUME_TAC th)
THEN POP_ASSUM(fun th-> MRESA_TAC th [`{w}:real^3->bool`;`{u:real^3}`])
THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(v=u:real^3)==> ({v, u} INTER {w}= {w} INTER {v} /\ {w} INTER {u}={}) \/ ({v, u} INTER {w}= {w} INTER {u} /\ {w} INTER {v}={})`)
THEN RESA_TAC
THENL[ ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {v}:real^3->bool`)
THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {v})`)
THEN RESA_TAC
THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {v}:real^3->bool`]
THEN POP_ASSUM MP_TAC THEN SET_TAC[];
ASSUME_TAC(SET_RULE`{} SUBSET {w} INTER {u}:real^3->bool`)
THEN MP_TAC(SET_RULE`DISJOINT {v, u} {x:real^3}==> DISJOINT {x} ({w} INTER {u})`)
THEN RESA_TAC
THEN MRESA_TAC AFF_GE_MONO_RIGHT[`{x:real^3}`;`{}:real^3->bool`;`{w} INTER {u}:real^3->bool`]
THEN POP_ASSUM MP_TAC THEN SET_TAC[]]]);;


let DWWUTKW=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 ds.
FAN(x,V,E) /\ v IN V /\ u IN V /\ ~collinear {x,v,u}
/\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
/\ fan80(x,V,E)
/\ ds IN face_set(hypermap1_of_fanx (x,V,E))
/\ aff_gt {x} {v,u} SUBSET dartset_leads_into_fan x V E ds
/\ E1=E UNION {{v,u}}
==> FAN (x,V,E1)`,

REPEAT STRIP_TAC
THEN FIND_ASSUM MP_TAC`FAN(x:real^3,V,E)`
THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
THEN MRESA_TAC th3[`v:real^3`;`u:real^3`;`x:real^3`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
THEN RESA_TAC
THEN MRESA_TAC add_edge_graph_fan[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
THEN MRESA_TAC garph_add_edge_is_garph[`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
THEN MRESA_TAC add_edge_into_collinear_fan[`x:real^3`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`]
THEN REWRITE_TAC[UNION;IN_ELIM_THM;IN_SING]
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THENL[ REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
THEN POP_ASSUM MATCH_MP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];

MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`e2:real^3->bool`];

REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
THEN POP_ASSUM MATCH_MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];

MRESA_TAC condition_not_intersection_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`e1:real^3->bool`]
THEN ASM_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`];

ASM_REWRITE_TAC[SET_RULE`A INTER A=A`];

MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e1:real^3->bool`;`v':real^3`];

REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e2:real^3->bool`;`e1:real^3->bool`])
THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`]
THEN POP_ASSUM MATCH_MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[];

MRESA_TAC condition_not_intersection_point_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `ds:real^3#real^3#real^3#real^3->bool`;`e2:real^3->bool`;`v':real^3`]
THEN ASM_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`];

REMOVE_THEN"YEU" (fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`])
THEN POP_ASSUM MATCH_MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);;



end;;