(* ========================================================================== *) (* 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 *) (* 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 *)(* Origin *)let fan1 = new_definition `fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {})`;;(* Non-parallel *)let fan2 = new_definition `fan2(x,V,E):bool <=> ~(x IN V)`;;(* Intersection *)let fan6 = new_definition `fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;(* 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 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)))`;;(* E(v) *)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)`;;(* sigma *)let set_of_edge = new_definition `set_of_edge v V E = {w | {v,w} IN E /\ w IN V}`;;(* 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 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))`;;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)`;;(* Hypermap of Fan *)let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse (extension_sigma_fan x V E v)`;;let dart1_of_fan = new_definition `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) = { (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 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 }`;;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)`;;(* 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 contracted_dart = new_definition `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;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)`;;(* Restricted versions of e_fan_pair, n_fan_pair, f_fan_pair (for convenience) *)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))`;;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`;;(* Topological component and dart *) (* X(V,E) *)let HYPERMAP_OF_FAN_ALT =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))`,(* Y(V,E) *)let xfan = new_definition `xfan (x,V,E) = {v | ?e. (E e) /\ (v IN aff_ge {x} 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 yfan = new_definition `yfan (x,V,E) = (:real^3) DIFF xfan (x,V,E)`;;(* 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 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) else (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 {}))`;;(* azim(x) *)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`;;(* rcone^0(x,v,h) *)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`;;(* 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 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)}`;;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`;;(* 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 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) }`;;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)`;;(* node(x) not needed, use FST x *) (* compare fan80 and fan81, which define fully_surrounded *)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))`;;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`;;(* 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 fully_surrounded = new_definition `fully_surrounded (V,E) = (!x. x IN dart_of_fan (V,E) ==> azim_dart (V,E) x < pi)`;;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))`;;end;;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)`;;