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




module  Leads_into_fan = 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;;


(****************************************************************************)
(****************************LEADS INTO**************************************)
(****************************************************************************)

let dart_leads_into=new_definition`dart_leads_into (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)= 
@(U:real^3->bool). ?h:real. &0<h /\
(!(s:real) (y:real^3). &0 <s /\ s<h
/\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s))
==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\  connected_component (yfan(x,V,E)) y=U))`;;
let exists_leads_into_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:real^3->bool). ?h:real. &0<h /\ (!(s:real) (y:real^3). &0 <s /\ s<h /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\ connected_component (yfan(x,V,E)) y=U))`,
REPEAT STRIP_TAC THEN MRESA_TAC JGIYDLE[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN ASM_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "BE") THEN DISCH_THEN (LABEL_TAC "YEU") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "EM") THEN DISCH_THEN (LABEL_TAC "NHIEU") THEN MP_TAC(REAL_ARITH`h> &0/\ &1>h ==> -- &1< (h:real)/\ -- &1<= (h:real) /\ h< &1 /\ &0 <h /\ h<= &1`) THEN RESA_TAC THEN MRESA1_TAC ACS_BOUNDS_LT`h:real` THEN REMOVE_ASSUM_TAC THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h:real`][ACS_0;REAL_ARITH`-- &1 <= &0`] THEN MRESA1_TAC COS_ACS `h:real` THEN REMOVE_THEN "BE" (fun th-> MRESA1_TAC th `acs(h:real)`) THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[EXTENSION] THEN REWRITE_TAC[EMPTY;IN;NOT_FORALL_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM FUN_EQ_THM] THEN EXISTS_TAC`(connected_component (yfan((x:real^3),(V:real^3->bool) ,(E:(real^3->bool)->bool))) (x':real^3)):real^3->bool` THEN EXISTS_TAC`acs(h:real)` THEN ASM_REWRITE_TAC[] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN DISCH_TAC THEN ASSUME_TAC(PI_WORKS) THEN MP_TAC(REAL_ARITH` &0< s /\ acs (h:real)< pi/ &2 /\ &0< pi ==> &0<= (s:real)/\ acs h<= pi`) THEN RESA_TAC THEN MRESAL_TAC COS_MONO_LT[`s:real`;`acs(h:real)`][] THEN MP_TAC(REAL_ARITH` h< cos(s:real)==>h<= cos(s:real)`) THEN RESA_TAC THEN REMOVE_THEN "NHIEU"(fun th-> MRESA1_TAC th `acs(h:real)`) THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`cos(s:real)`;`h:real`]) THEN MRESA_TAC CONNECTED_COMPONENT_MAXIMAL [`yfan(x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool))`;`rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (h:real)`;`x':real^3`] THEN STRIP_TAC THENL[ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; MATCH_MP_TAC CONNECTED_COMPONENT_EQ THEN ASM_TAC THEN SET_TAC[]]);;
let DART_LEADS_INTO=
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 ==> ?h:real. &0<h /\ (!(s:real) (y:real^3). &0 <s /\ s<h /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET dart_leads_into x V E v u /\ connected_component (yfan(x,V,E)) y=dart_leads_into x V E v u))`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[dart_leads_into] THEN MRESA_TAC exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`] THEN SELECT_ELIM_TAC THEN EXISTS_TAC`U:real^3->bool` THEN EXISTS_TAC`h:real` THEN ASM_REWRITE_TAC[]);;
let unique_dart_leads_into=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 (U:real^3->bool). FAN(x,V,E)/\ {v,u} IN E /\(?h:real. &0<h /\ (!(s:real) (y:real^3). &0 <s /\ s<h /\ y IN rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) ==> (rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),sigma_fan x V E v u) (cos(s)) SUBSET U /\ connected_component (yfan(x,V,E)) y=U))) ==> dart_leads_into x V E v u =U`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"A") THEN MRESA_TAC DART_LEADS_INTO [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "BE") THEN MRESA_TAC JGIYDLE[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_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 "YEU") THEN DISCH_THEN (LABEL_TAC "EM") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "MAI") THEN ASSUME_TAC(PI_WORKS) THEN MP_TAC(REAL_ARITH`&0<h /\ &0<h' /\ &0 <pi==> -- &1< (min (min (h:real) (h':real)/ &2) (pi/ &3)) /\ -- &1<= (min (min (h:real) (h':real)/ &2) (pi/ &3)) /\ (min (min (h:real) (h':real)/ &2) (pi/ &3))< pi/ &2 /\ &0 <(min (min (h:real) (h':real)/ &2) (pi/ &3)) /\ (min (min (h:real) (h':real)/ &2) (pi/ &3))<= pi/ &2 /\ (min (min (h:real) (h':real)/ &2) (pi/ &3))< h /\ (min (min (h:real) (h':real)/ &2) (pi/ &3))< h' `) THEN RESA_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th ` (min (min (h:real) (h':real)/ &2) (pi/ &3))`) THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[EXTENSION] THEN REWRITE_TAC[EMPTY;IN;NOT_FORALL_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM FUN_EQ_THM] THEN REMOVE_THEN "BE" (fun th-> MRESA_TAC th[`(min ((min (h:real) (h':real))/ &2) (pi/ &3))`;`x':real^3`]) THEN POP_ASSUM MP_TAC THEN REMOVE_THEN "A" (fun th-> MRESA_TAC th[`(min ((min (h:real) (h':real))/ &2) (pi/ &3))`;`x':real^3`]) THEN POP_ASSUM MP_TAC THEN SET_TAC[]);;
let dart_leads_into_fan_in_topological_component_yfan=
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 ==> dart_leads_into x V E v u IN topological_component_yfan (x,V,E)`,
REPEAT STRIP_TAC THEN MRESA_TAC not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN MRESA_TAC DART_LEADS_INTO[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`; `v:real^3`;`u:real^3`;] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN MRESA_TAC rw_dart_avoids_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"OI") THEN MP_TAC(REAL_ARITH`&1> h' /\ h' > &0==> -- &1 < h' /\ h'< &1 /\ -- &1 <= h' /\ h'<= &1/\ &0 < h' /\ h' <= &1`) THEN RESA_TAC THEN MRESA1_TAC ACS_BOUNDS_LT`h':real` THEN MRESAL_TAC ACS_MONO_LT[`&0`;`h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`] THEN MRESA1_TAC COS_ACS `h':real` THEN ABBREV_TAC`h1= min (h:real) (acs h')/ &2` THEN MP_TAC(REAL_ARITH`h1= min (h:real) (acs h')/ &2 /\ &0<h /\ &0< acs h' /\ acs h'< pi/ &2==> &0< h1 /\ h1< h /\ h1<pi/ &2/\ h1< acs h' /\ acs h' <= pi /\ &0<= h1`) THEN ASM_REWRITE_TAC[PI_WORKS] THEN STRIP_TAC THEN MRESAL_TAC COS_MONO_LT[`h1:real`;`acs h':real`][ACS_0;REAL_ARITH`-- &1 <= &0`] THEN MP_TAC(REAL_ARITH`h'< cos h1==> h'<= cos h1`) THEN RESA_TAC THEN REMOVE_THEN "EM"(fun th-> MRESAL1_TAC th `h1:real`[SET_RULE`~(A={})<=> ?y. y IN A`]) THEN REMOVE_THEN "YEU"(fun th-> MRESA_TAC th [`h1:real`;`y:real^3`]) THEN POP_ASSUM(fun th -> REWRITE_TAC[SYM(th);IN_ELIM_THM;topological_component_yfan;]) THEN EXISTS_TAC`y:real^3` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC continuous_set_fan[`(x:real^3)`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`(cos h1:real)`;`(h':real)`] THEN ASM_TAC THEN SET_TAC[]);;
let connected_dart_leads_into_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 ==> connected(dart_leads_into x V E v u )`,
REPEAT STRIP_TAC THEN MRESA_TAC dart_leads_into_fan_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`] THEN MATCH_MP_TAC in_topological_component_yfan_is_connected THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`V:real^3->bool` THEN EXISTS_TAC`E:(real^3->bool)->bool` THEN ASM_REWRITE_TAC[]);;
end;;