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