(* ========================================================================== *)
(* 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;;