1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Tame Hypermap *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
11 Definitions file for Tame Hypermap
14 flyspeck_needs "hypermap/hypermap.hl";;
15 flyspeck_needs "fan/fan_defs.hl";;
16 flyspeck_needs "packing/pack_defs.hl";;
18 module Tame_defs = struct
24 let edge_nondegenerate = new_definition `edge_nondegenerate (H:(A)hypermap)
25 <=> !(x:A).(x IN dart H) ==> ~ (edge_map H x = x)`;;
28 let is_edge_nondegenerate = new_definition `is_edge_nondegenerate (H:(A)hypermap) <=>
29 (!x:A. x IN dart H ==> ~(edge_map H x = x))`;;
31 let is_node_nondegenerate = new_definition `is_node_nondegenerate (H:(A)hypermap) <=>
32 (!x:A. x IN dart H ==> ~(node_map H x = x))`;;
36 (* no_loops does not restrict x,y to be darts. But edge H is the
37 identitiy outside darts, so this is OK. *)
39 let no_loops = new_definition `no_loops (H:(A) hypermap) <=> ! (x:A) (y:A). x IN edge H y /\ x IN node H y ==> x = y`;;
41 (* this definition is more complicated than it needs to be. It is
42 better to use hypermap.hl is_no_double_joints *)
45 let hypermap_no_double_joins = new_definition
46 `hypermap_no_double_joins (H:(A) hypermap) <=>
47 ! (x:A) (y:A) (z:A) (t:A) (u:A) (v:A). x IN node H z /\ y IN (edge H x INTER node H t) /\ ~ (x = y)
48 /\ ~(z IN node H t) /\ u IN node H z /\ v IN (edge H u INTER node H t)
49 /\ ~(u = v) ==> x IN edge H u`;;
52 let is_no_double_joints = new_definition `is_no_double_joints (H:(A)hypermap)
53 <=> (!x y. x IN dart H /\ y IN node H x /\ edge_map H y IN node H (edge_map H x) ==> x = y)`;;
55 let exceptional_face = new_definition `exceptional_face (H:(A)hypermap) (x:A) <=> CARD (face H x) >= 5`;;
57 let set_of_triangles_meeting_node = new_definition
58 `set_of_triangles_meeting_node (H:(A)hypermap) (x:A) =
59 {face H (y:A) |y | y IN dart H /\ CARD (face H y) = 3 /\ y IN node H x }`;;
61 let set_of_quadrilaterals_meeting_node = new_definition
62 `set_of_quadrilaterals_meeting_node (H:(A)hypermap) (x:A) =
63 {face (H:(A)hypermap) (y:A)|y | y IN dart H /\ CARD (face H y) = 4 /\ y IN node H x}`;;
65 let set_of_exceptional_meeting_node = new_definition
66 `set_of_exceptional_meeting_node (H:(A)hypermap) (x:A) =
67 {face H (y:A) | y | (y IN (dart H)) /\ (CARD (face H y) >= 5) /\ (y IN node H x)}`;;
69 let set_of_face_meeting_node = new_definition
70 `set_of_face_meeting_node (H:(A)hypermap) (x:A) =
71 {face H (y:A)|y| y IN dart H /\ y IN node H x}`;;
73 let type_of_node = new_definition
74 `type_of_node (H:(A)hypermap) (x:A) =
75 (CARD (set_of_triangles_meeting_node H x),
76 CARD (set_of_quadrilaterals_meeting_node H x),
77 CARD (set_of_exceptional_meeting_node H x ))`;;
79 let node_type_exceptional_face = new_definition
80 `node_type_exceptional_face (H:(A)hypermap) (x:A) <=>
81 exceptional_face H x /\ (CARD (node H x) = 6) ==> type_of_node H x = (5,0,1)`;;
83 let node_exceptional_face = new_definition
84 `node_exceptional_face (H:(A)hypermap) (x:A) <=>
85 exceptional_face H x ==> CARD (node H x) <= 6`;;
88 let tgt = new_definition `tgt = #1.541`;;
90 (* b table constants corrected 2010-06-17 *)
92 let b_tame = new_definition
94 if p,q =0,3 then #0.618
95 else if p,q=0,4 then #0.97
96 else if p,q=1,2 then #0.656
97 else if p,q=1,3 then #0.618
98 else if p,q=2,1 then #0.797
99 else if p,q=2,2 then #0.412
100 else if p,q=2,3 then #1.2851
101 else if p,q=3,1 then #0.311
102 else if p,q=3,2 then #0.817
103 else if p,q=4,0 then #0.347
104 else if p,q=4,1 then #0.366
105 else if p,q=5,0 then #0.04
106 else if p,q=5,1 then #1.136
107 else if p,q=6,0 then #0.686
108 else if p,q=7,0 then #1.450
112 let d_tame = new_definition `d_tame n =
113 if n = 3 then &0 else
114 if n = 4 then #0.206 else
115 if n = 5 then #0.4819 else
116 if n = 6 then #0.712 else tgt`;;
118 (* tchales, changed n=6 case from 0.7578, 1/15/2012 to match May 2011
119 redo in main_estimate_ineq.hl and graph generator. *)
121 let a_tame = new_definition `a_tame = #0.63`;;
123 let total_weight = new_definition
124 `total_weight (H:(A)hypermap) (w:(A->bool)->real) = sum (face_set H) w`;;
126 let adm_1 = new_definition
127 `adm_1 (H:(A)hypermap) (w:(A->bool)->real) <=> (!x:A. x IN dart H ==> w (face H x) >= d_tame (CARD (face H x)))`;;
129 let adm_2 = new_definition
130 `adm_2 (H:(A)hypermap) (w:(A->bool)->real) <=>
131 (!x:A. x IN dart H /\ (CARD (set_of_exceptional_meeting_node H x) = 0) ==>
132 ((sum (set_of_face_meeting_node H x) w) >=
133 (b_tame (CARD (set_of_triangles_meeting_node H x)) (CARD (set_of_quadrilaterals_meeting_node H x)))))`;;
135 let adm_3 = new_definition
136 `adm_3 (H:(A)hypermap) (w:(A->bool)->real) <=>
137 (!x:A. x IN dart H /\ type_of_node H x = 5, 0, 1 ==>
138 (sum (set_of_triangles_meeting_node H x) w) >= a_tame)`;;
140 let admissible_weight = new_definition
141 `admissible_weight (H:(A)hypermap) (w:(A->bool)->real) <=>
142 adm_1 H w /\ adm_2 H w /\ adm_3 H w`;;
147 let tame_1 = new_definition
148 `tame_1 (H:(A)hypermap) <=>
149 plain_hypermap (H:(A)hypermap) /\ planar_hypermap (H:(A)hypermap)`;;
151 let tame_2 = new_definition
152 `tame_2 (H:(A)hypermap) <=>
153 connected_hypermap H /\ simple_hypermap H`;;
155 let tame_3 = new_definition
156 `tame_3 (H:(A)hypermap) <=> is_edge_nondegenerate H `;;
158 let tame_4 = new_definition
159 `tame_4 (H:(A)hypermap) <=> no_loops H`;;
161 let tame_5a = new_definition
162 `tame_5a (H:(A)hypermap) <=> is_no_double_joints H`;;
164 let tame_8 = new_definition
165 `tame_8 (H:(A)hypermap) <=> number_of_faces H >= 3`;;
167 let tame_9a = new_definition
168 `tame_9a (H:(A)hypermap) <=>
169 (!(x:A). x IN dart H ==> CARD (face H x) >= 3 /\ CARD (face H x) <= 6)`;;
171 let tame_10 = new_definition
172 `tame_10 (H:(A)hypermap) <=>
173 number_of_nodes H IN { 13, 14, 15 } `;;
175 let tame_11a = new_definition
176 `tame_11a (H:(A)hypermap) <=>
177 (!(x:A). x IN dart H ==> CARD (node H x) >= 3)`;;
179 let tame_11b = new_definition
180 `tame_11b (H:(A)hypermap) <=>
181 (!(x:A). x IN dart H ==> CARD (node H x) <= 7)`;;
183 let tame_12o = new_definition
184 `tame_12o (H:(A)hypermap) <=>
185 (! (x:A). node_type_exceptional_face H x /\ node_exceptional_face H x)`;;
187 let tame_13a = new_definition
188 `tame_13a (H:(A)hypermap) <=>
189 (?(w:(A->bool)->real). admissible_weight H w /\ total_weight H w < tgt)`;;
191 let tame_hypermap = new_definition
192 `tame_hypermap (H:(A)hypermap) <=>
193 tame_1 H /\ tame_2 H /\ tame_3 H /\ tame_4 H /\
194 tame_5a H /\ tame_8 H /\ tame_9a H /\
195 tame_10 H /\ tame_11a H /\ tame_11b H /\ tame_12o H /\ tame_13a H`;;
197 let opposite_hypermap = new_definition
198 `opposite_hypermap (H:(A)hypermap) =
199 hypermap ((dart H),face_map H o node_map H , inverse(node_map H),inverse(face_map H))`;;
202 let ESTD = new_definition
203 `ESTD (V:real^3->bool) = {{v,w}| v IN V /\ w IN V /\ ~(v = w) /\ dist(v,w) <= (&2)*h0}`;;
205 let ECTC = new_definition
206 `ECTC (V:real^3 -> bool) = {{v,w}| v IN V /\ w IN V /\ ~(v = w) /\ dist(v,w) = &2 }`;;
209 let isolated_node = new_definition
210 `isolated_node v V E = (set_of_edge v V E = {})`;;
213 let azim_dart = new_definition
214 `azim_dart (V,E) (v,w) = if (v=w) then &2 * pi else azim_fan (vec 0) V E v w`;;
216 let dart1_of_fan = new_definition
217 `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) = { (v,w) | {v,w} IN E }`;;
219 let dart_of_fan = new_definition
221 { (v,v) | v IN V /\ set_of_edge (v:real^3) V E = {} } UNION { (v,w) | {v,w} IN E }`;;
223 (* in fan/introduction.hl a dart is a 4-tuple. Here it is a pair. Here is the correspondence *)
225 let extended_dart = new_definition
226 `extended_dart (V,E) (v,w) = i_fan (vec 0) V E (vec 0, v, w, w)`;;
228 let contracted_dart = new_definition
229 `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;
231 (* e_fan, n_fan, f_fan of fan/introduction.hl, restricted to pairs *)
233 let e_fan_pair = new_definition `e_fan_pair (V,E) (v,w) = (w,v)`;;
235 let n_fan_pair = new_definition
236 `n_fan_pair (V,E) (v,w) = v,sigma_fan (vec 0) V E v w`;;
238 let f_fan_pair = new_definition
239 `f_fan_pair (V,E) (v,w) = w,(inverse_sigma_fan (vec 0) V E w v)`;;
241 let hypermap_of_fan = new_definition
242 `hypermap_of_fan (V,E) =
243 (let p = ( \ t. res (t (V,E) ) (dart1_of_fan (V,E)) ) in
244 hypermap( dart_of_fan (V,E) , p e_fan_pair, p n_fan_pair, p f_fan_pair))`;;
246 let face_set_of_fan = new_definition
247 `face_set_of_fan (V,E) = face_set (hypermap_of_fan (V,E))`;;
250 (* compare fan80 and fan81, which define fully_surrounded *)
252 let surrounded_node = new_definition
253 `surrounded_node (V,E) v =
254 !x. (x IN dart_of_fan (V,E)) /\ (FST x = v) ==> azim_dart (V,E) x < pi`;;
256 let scriptL = new_definition
257 `scriptL V = sum V ( \ (v:real^3) . lmfun (norm v / &2)) `;;
259 let contravening = new_definition
260 `contravening V <=> packing V /\ V SUBSET ball_annulus /\ scriptL V > &12 /\
261 (!W. packing W /\ W SUBSET ball_annulus ==> scriptL W <= scriptL V) /\
262 (CARD V = 13 \/ CARD V = 14 \/ CARD V = 15) /\
263 (!v. v IN V ==> surrounded_node (V, ESTD V) v) /\
264 (!v. v IN V ==> (surrounded_node (V, ECTC V) v \/ (norm v = &2) ))`;;
266 let topological_component_yfan = new_definition
267 `topological_component_yfan ((x:real^3),(V:real^3->bool),E) =
268 { connected_component (yfan (x,V,E)) y | y | y IN yfan (x,V,E) }`;;
270 (* there is a function dart_leads_into in fan/introduction.hl. This is a bit simpler. *)
272 let dart_leads_into1 = new_definition
273 `dart_leads_into1 (x,V,E) (v,u) = @s. s IN topological_component_yfan (x,V,E) /\
275 rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps SUBSET s)`;;
277 let dartset_leads_into = new_definition
278 `dartset_leads_into (x,V,E) ds =
279 @s. (!y. (y IN ds) ==> (s=dart_leads_into1 (x,V,E) y))`;;
281 (* node(x) not needed, use FST x *)
283 let h_dart = new_definition `h_dart (x:real^3#B) = norm (FST x) / &2`;;
285 let tauVEF = new_definition `tauVEF (V,E,f) =
286 sum f ( \ x. azim_dart (V,E) x * (&1 + (sol0/pi) * (&1 - lmfun (h_dart x)))) + (pi + sol0)*(&2 - &(CARD(f)))`;;
289 let restricted_hypermap = new_definition `restricted_hypermap (H:(A)hypermap) <=>
290 is_no_double_joints H /\ ~(dart H = {}) /\ planar_hypermap H /\ connected_hypermap H /\
291 plain_hypermap H /\ simple_hypermap H /\ is_edge_nondegenerate H /\ is_node_nondegenerate H /\
292 (!f. f IN face_set H ==> CARD(f) >= 3)`;;
294 (* deprecated 2013-2-22 : Use rho_node1 which has been developed further,
296 perimeterbound -> . They haven't been developed.
299 let rho_node = new_definition
300 `rho_node (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;;
302 let per = new_definition
303 `per(V,E,f) v k = sum (0..k-1)
304 ( \ i. arcV (vec 0) ((rho_node (V,E,f) POWER i) v) ((rho_node (V,E,f) POWER (i+1)) v))`;;
306 let perimeterbound = new_definition `perimeterbound (V,E) =
307 (!f. f IN face_set_of_fan (V,E) ==>
308 sum f (\ (v,w). arcV (vec 0) (v:real^3) w ) <= &2 * pi)`;;