(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definitions                                                                *)
(* Chapter: Fan                                                               *)
(* Authors: Thomas C. Hales, Hoang Le Truong, Alexey Solovyev                 *)
(* Date: 2010-05-11                                                           *)
(* ========================================================================== *)

Definitions file for Fan 

flyspeck_needs "general/sphere.hl";;
flyspeck_needs "volume/vol1.hl";;
flyspeck_needs "hypermap/hypermap.hl";;

module Fan_defs  = struct

(* General definitions *)

let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
(* AS: Maybe it is better to change names to something like fan_card, fan_origin, fan_non_parallel, fan_intersection, because names like fan1, fan2, fan6, fan7 are not descriptive at all. If the names are changed, then it will be required to modify fan/*.hl as well. I think, it is quite easy and fast: search for all occurrences of fan1 and change it to fan_card, etc. This procedure should take at most 10-20 minutes. *) (* Cardinality *)
let fan1 = new_definition `fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {})`;;
(* Origin *)
let fan2 = new_definition `fan2(x,V,E):bool <=> ~(x IN V)`;;
(* Non-parallel *)
let fan6 = new_definition `fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
(* Intersection *)
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)))`;;
(* Fan *) (* AS: In my opinion, the name `fan` is better because it follows the general convention of naming objects in HOL Light. The file fan/introduction.hl already contains the definition of the constant `fan`. Probably, it is an earlier definition of fan. Now, it should be deprecated. Again, I think it will be not difficult to make corresponding changes in fan/*.hl *)
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)`;;
(* E(v) *)
let set_of_edge = new_definition `set_of_edge v V E = {w | {v,w} IN E /\ w IN V}`;;
(* sigma *)
let sigma_fan = new_definition `sigma_fan x (V:real^3->bool) E v u =  
					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))`;;
(* AS: This definition is not very important (there is only one result involving this definition which proves that extension_sigma_fan permutes set_of_edge). But I decided that it is simpler to have this definition rather than modify the definition of sigma_fan *) (* THALES: It appears that there are three definitions of inverse_sigma_fan from the files introduction.hl, fan_misc.hl, and fan_defs.hl I am renaming the one in fan/introduction.hl inverse_sigma_fan_alt and the one in fan_misc.hl as inverse_sigma_fan_bis. I take the one in fan_defs.hl to be the primary definition. *)
let extension_sigma_fan = new_definition `extension_sigma_fan x (V:real^3->bool) E v u =  
					if ~(u IN set_of_edge v V E ) then u 
						else (sigma_fan x V E v u)`;;
let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse (extension_sigma_fan x V E v)`;;
(* Hypermap of Fan *)
let dart1_of_fan = new_definition
  `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  { (v,w) | {v,w} IN E }`;;
let dart_of_fan = new_definition
  `dart_of_fan (V,E) =
   { (v,v) | v IN V /\ set_of_edge (v:real^3) V E = {} } UNION { (v,w) | {v,w} IN E }`;;
(* in fan/introduction.hl a dart is a 4-tuple. Here it is a pair. Here is the correspondence *) (* AS: Do we need this correspondence? Right now, there are no results involving `extended_dart` or `contracted_dart`. Ultimately, it is better to use new definition of darts as pairs everywhere. *)
let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
let extended_dart = new_definition
  `extended_dart (V,E) (v,w) = i_fan (vec 0) V E (vec 0, v, w, w)`;;
let contracted_dart = new_definition
  `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;
(* e_fan, n_fan, f_fan of fan/introduction.hl, restricted to pairs *) (* AS: In my opinion, it is better to change the names e_fan_pair, n_fan_pair, f_fan_pair to e_fan, n_fan, f_fan. It will require some modifications in fan/introduction.hl, but it is not a problem *)
let e_fan_pair = new_definition `e_fan_pair (V,E) (v,w) = (w,v)`;;
let n_fan_pair = new_definition 
  `n_fan_pair (V,E) (v,w) = v,sigma_fan (vec 0) V E v w`;;
let f_fan_pair = new_definition 
  `f_fan_pair (V,E) (v,w) = w,(inverse_sigma_fan (vec 0) V E w v)`;;
let hypermap_of_fan  = new_definition
  `hypermap_of_fan (V,E) = 
    (let p = ( \ t. res (t (V,E) ) (dart1_of_fan (V,E)) ) in 
          hypermap( dart_of_fan (V,E) , p e_fan_pair, p n_fan_pair, p f_fan_pair))`;;
(* Restricted versions of e_fan_pair, n_fan_pair, f_fan_pair (for convenience) *)
let e_fan_pair_ext = new_definition `e_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then e_fan_pair (V,E) x else x`;;
let n_fan_pair_ext = new_definition `n_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then n_fan_pair (V,E) x else x`;;
let f_fan_pair_ext = new_definition `f_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then f_fan_pair (V,E) x else x`;;
prove(`!V E. e_fan_pair_ext (V,E) = res (e_fan_pair (V,E)) (dart1_of_fan (V,E))`,
REWRITE_TAC[FUN_EQ_THM; e_fan_pair_ext; Sphere.res]);;
prove(`!V E. f_fan_pair_ext (V,E) = res (f_fan_pair (V,E)) (dart1_of_fan (V,E))`,
REWRITE_TAC[FUN_EQ_THM; f_fan_pair_ext; Sphere.res]);;
prove(`!V E. n_fan_pair_ext (V,E) = res (n_fan_pair (V,E)) (dart1_of_fan (V,E))`,
REWRITE_TAC[FUN_EQ_THM; n_fan_pair_ext; Sphere.res]);;
prove(`!V E. hypermap_of_fan (V,E) = hypermap (dart_of_fan (V,E), e_fan_pair_ext (V,E), n_fan_pair_ext (V,E), f_fan_pair_ext (V,E))`,
(* Topological component and dart *) (* X(V,E) *)
let xfan = new_definition `xfan (x,V,E) = {v | ?e. (E e) /\ (v IN aff_ge {x} e)}`;;
(* Y(V,E) *)
let yfan = new_definition `yfan (x,V,E) = (:real^3) DIFF xfan (x,V,E)`;;
(* AS: The original definition of yfan (renamed yfan_deprecated in fan/introduction.hl) is the following: let yfan_deprecated = new_definition `yfan_deprecated (x,V,E) = {v:real^3 | ?e. (E e) /\ (~(v IN aff_ge {x} e))}`;; It seems to be wrong since the negation of (?e. (E e) /\ (v IN aff_ge {x} e)) is (!e. (E e) /\ ~(v IN aff_ge {x} e)). *) (* W^0_{dart}(x) *) (* AS: It is better to have w_dart_fan x V E (v,w), or even w_dart_fan V E (v,w) *)
let w_dart_fan = new_definition `w_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3)=  
 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
   (if set_of_edge v V E = {w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
    else (if set_of_edge v V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
(* DEPRECATED, 2011-08-01, --> wedge_ge let cwedge = new_definition `cwedge v0 v1 w1 w2 = {y | &0 <= azim v0 v1 w1 y /\ azim v0 v1 w1 y <= azim v0 v1 w1 w2}`;; *) (* W_{dart}(x) *) (* DEPRECATED, 2011-08-01 let cw_dart_fan=new_definition `cw_dart_fan (V:real^3->bool) E (v,w)= if (CARD (set_of_edge v V E) > 1) then cwedge (vec 0) v w (sigma_fan (vec 0) V E v w) else (:real^3)`;; *)
let azim_fan = new_definition `azim_fan x (V:real^3->bool) E v w = 
  if (CARD (set_of_edge v V E) > 1) 
  then azim x v w (sigma_fan x V E v w) 
  else &2 * pi`;;
(* azim(x) *)
let azim_dart = new_definition 
  `azim_dart (V,E) (v,w) = 
  if (v=w) then &2 * pi else azim_fan (vec 0) V E v w`;;
(* rcone^0(x,v,h) *)
let rcone_fan = new_definition `rcone_fan  (x:real^3) (v:real^3) (h:real) = 
			{y:real^3 | (y-x) dot (v-x) > (dist(y,x)*dist(v,x)*h)}`;;
(* W^0_{dart}(x,epsilon) *) (* AS: It is better to have rw_dart_fan V E (v,w) In the book, it is defined as ... INTER rcone_fan x v (cos h), in fan/introduction.hl, it is used as rw_dart_fan x V E (...) (cos s) instead (not always but only when necessary). This can lead to confusions. In my opinion, it is simpler to follow the book definition. In this case, some changes in fan/introduction.hl are required. *)
let rw_dart_fan = new_definition 
  `rw_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3) h = 
		w_dart_fan x V E (y,v,w,w1) INTER rcone_fan x v h`;;
let topological_component_yfan = new_definition 
  `topological_component_yfan ((x:real^3),(V:real^3->bool),E) =
      {  connected_component (yfan (x,V,E)) y  | y | y IN yfan (x,V,E) }`;;
(* there is a function dart_leads_into in fan/introduction.hl. This is a bit simpler. *) (* AS: It is better to change name to `dart_leads_into`. For the current definition of rw_dart_fan, should be: rw_dart_fan ... (cos eps), but I prefer to change the definition of rw_dart_fan instead. *)
let dart_leads_into1 = new_definition 
    `dart_leads_into1 (x,V,E) (v,u) = @s.  s IN topological_component_yfan (x,V,E) /\
	(?eps. (eps < &1) /\ 
	   rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps  SUBSET s)`;;
let dartset_leads_into = new_definition
  `dartset_leads_into (x,V,E) ds = 
    @s. (!y. (y IN ds) ==> (s = dart_leads_into1 (x,V,E) y))`;;
(* node(x) not needed, use FST x *) (* compare fan80 and fan81, which define fully_surrounded *)
let surrounded_node = new_definition
  `surrounded_node (V,E) v = 
  !x. (x IN dart_of_fan (V,E)) /\ (FST x = v) ==> azim_dart (V,E) x < pi`;;
let fully_surrounded = new_definition
	`fully_surrounded (V,E) = (!x. x IN dart_of_fan (V,E) ==> azim_dart (V,E) x < pi)`;;
(* AS: the definitions from fan/introduction.hl are below: let fan81=new_definition`fan81 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> azim_fan x V E v u <pi)`;; let fan80=new_definition`fan80 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> &0< azim x v u (sigma_fan x V E v u) /\ azim x v u (sigma_fan x V E v u) <pi)`;; *) (* Conformance *)
let conforming_bijection = new_definition `conforming_bijection (V,E) <=>
  !s. s IN topological_component_yfan (vec 0,V,E) ==> (?!f. f IN face_set (hypermap_of_fan (V,E)) /\ 
							 s = dartset_leads_into (vec 0,V,E) f)`;;
let conforming_half_space = new_definition `conforming_half_space (V,E) <=>
	!f. f IN face_set (hypermap_of_fan (V,E)) ==> 
		dartset_leads_into (vec 0,V,E) f = 
			INTERS {aff_gt {vec 0, FST x, FST (f_fan_pair (V,E) x)} {FST (inverse (f_fan_pair (V,E)) x)} | x IN f}`;;
let conforming_solid_angle = new_definition `conforming_solid_angle (V,E) <=>
  !f. f IN face_set (hypermap_of_fan (V,E)) ==>
  (let U = dartset_leads_into (vec 0,V,E) f in
     (!r. measurable (ball (vec 0,r) INTER U)) /\
       eventually_radial (vec 0) U /\
       sol (vec 0) U = &2 * pi + sum (f) (\x. azim_dart (V,E) x - pi))`;;
let conforming_diagonal = new_definition `conforming_diagonal (V,E) <=>
	(!f x y. f IN face_set (hypermap_of_fan (V,E)) /\ x IN f /\ y IN f /\ ~(x = y) ==> 
		~collinear {vec 0, FST x, FST y} /\
		(y = f_fan_pair (V,E) x \/ x = f_fan_pair (V,E) y \/ 
			aff_gt {vec 0} {FST x, FST y} SUBSET dartset_leads_into (vec 0,V,E) f))`;;
let conforming = new_definition `conforming (V,E) <=>
	fully_surrounded (V,E) /\
	conforming_bijection (V,E) /\
	conforming_half_space (V,E) /\
	conforming_solid_angle (V,E) /\
	conforming_diagonal (V,E)`;;