1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Tame Hypermap *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
12 Definitions file for Local Fans
14 This file was split off from tame/tame_defs.hl in July 2010
15 when it was discovered that there are many incompatible
16 definitions betwen the Local Fans chapter and the Tame chapter.
18 This file is not currently part of the build.
21 flyspeck_needs "hypermap/hypermap.hl";;
22 flyspeck_needs "fan/fan_defs.hl";;
23 flyspeck_needs "packing/pack_defs.hl";;
25 module Local_fan_defs = struct
28 let cwedge = new_definition `cwedge v0 v1 w1 w2 =
29 {y | &0 <= azim v0 v1 w1 y /\
30 azim v0 v1 w1 y <= azim v0 v1 w1 w2}`;;
32 let cw_dart_fan=new_definition
33 `cw_dart_fan (V:real^3->bool) (E:(real^3->bool)->bool) ((v:real^3),(w:real^3))=
34 if (CARD (set_of_edge v V E) > 1)
35 then cwedge (vec 0) v w (sigma_fan (vec 0) V E v w)
38 let local_fan = new_definition `local_fan (V,E,f) <=>
40 f IN face_set_of_fan (V,E) /\
41 (hypermap_of_fan (V,E)) iso (cyclic_hypermap I I (CARD f))`;;
43 let convex_local_fan = new_definition `convex_local_fan (V,E,f) <=>
45 (!x. (x IN f) ==> azim_dart (V,E) x <= pi) /\
46 (!x. (x IN f) ==> V SUBSET cw_dart_fan V E x)`;;
48 let rho_node1 = new_definition
49 `rho_node1 (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;;
51 let order_permutation = new_definition
52 `order_permutation (p:A->A) = (minimal) { m | (p POWER m = I) /\ (m > 0) }`;;
54 let is_cyclic_permutation = new_definition
55 `is_cyclic_permutation rho s <=>
56 rho permutes s /\ s HAS_SIZE (order_permutation rho)`;;
58 let interior_angle = new_definition
59 `interior_angle (V,E,f) v = azim_dart (V,E) (v,(rho_node1 (V,E,f) v))`;;
61 let cw_node_fan = new_definition
62 `cw_node_fan (V,E,f) v = cw_dart_fan V E (v,rho_node1(V,E,f) v)`;;
64 let w_node_fan = new_definition (* 4th component is ignored *)
65 `w_node_fan (V,E,f) v = w_dart_fan (vec 0) V E (vec 0,v,rho_node1(V,E,f) v,v)`;;
67 let localization = new_definition `localization (V,E,f) =
68 {v | v IN V /\ (?w. w IN V /\ (v,w) IN f)},
69 { {v,w} | {v,w} IN E /\ (v,w) IN f},
72 let is_generic_clf = new_definition `is_generic_clf (V,E,f:A) <=>
73 (! v w (u:real^3). (u IN V) /\ {v,w} IN E ==>
74 aff_ge { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {})`;;
76 let is_circular_clf = new_definition `is_circular_clf (V,E,f:A) <=>
77 (? v w (u:real^3). (u IN V) /\ {v,w} IN E /\
78 ~( aff_gt { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {}))`;;
80 let is_lunar_clf = new_definition `is_lunar_clf (V,E,f:A) (v,w) <=>
81 v IN V /\ w IN V /\ ~(is_circular_clf (V,E,f)) /\
82 collinear {(vec 0) , v, w}`;;
84 let is_flat = new_definition `is_flat (V,E,f) v <=>
85 interior_angle (V,E,f) v = pi`;;
88 let is_deformation_clf = new_definition
89 `is_deformation_clf phi V s = (!v x. v IN V ==> (phi v) continuous at x within s)`;;
91 let node_deform = new_definition
92 `node_deform phi V t = { phi v t | v IN V}`;;
94 let edge_deform = new_definition
95 `edge_deform phi V E t = { {phi v t, phi w t} | {v,w} IN E}`;;
97 let face_deform = new_definition
98 `face_deform phi V f t = { (phi v t, phi w t) | (v,w) IN f}`;;
100 let per = new_definition
101 `per(V,E,f) v k = sum (0..k-1)
102 ( \ i. arcV (vec 0) ((rho_node1 (V,E,f) POWER i) v) ((rho_node1 (V,E,f) POWER (i+1)) v))`;;
104 let perimeter = new_definition
105 `perimeter(V,E,f) = per(V,E,f) (CHOICE V) (CARD(f))`;;
108 let perimeterbound = new_definition `perimeterbound (V,E) =
109 (!f. f IN face_set_of_fan (V,E) ==>
110 sum f (\ (v,w). arcV (vec 0) (v:real^3) w ) <= &2 * pi)`;;
113 let special_fan = new_definition
114 `special_fan (V,E,f,S) <=> packing V /\ V SUBSET ball_annulus /\ convex_local_fan (V,E,f) /\
116 (! v w. {v,w} IN S ==>( dist(v,w) = &2 * h0)) /\
117 (! v w. {v,w} IN E ==> (dist(v,w) <= &2 * h0)) /\
118 (! v w. v IN V /\ w IN V /\ ~(v=w) /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))`;;
120 let r_special = new_definition
121 `r_special (V,E,f,S) = CARD(E) - CARD(S)`;;
123 let s_special = new_definition
124 `s_special (V,E,f,S) = CARD(S)`;;
126 let d2_tame = new_definition (* deprecate *)
127 `d2_tame r s = if (r + 2*s > 3)
128 then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4)
131 let tame_table_d = new_definition
132 `tame_table_d r s = if (r + 2*s > 3)
133 then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4)
134 else #0.0`;; (* preferred term *)
137 let d2_special = new_definition
138 `d2_special (V,E,f,S) = d2_tame (r_special (V,E,f,S)) (s_special (V,E,f,S))`;;
140 let vertex_datum = new_definition
141 `vertex_datum p k = IMAGE p (0..(k-1))`;;
143 let edge_datum = new_definition
144 `edge_datum p k = { { p i, p ((i+1) MOD k) } |i| i IN (0..(k-1)) }`;;
146 let face_datum = new_definition
147 `face_datum p k = { (p i, p ((i+1) MOD k)) |i| i IN (0..(k-1)) }`;;
149 let special_datum = new_definition
150 `special_datum p k J = { (p i, (p((i+1) MOD k))) | i | i IN J }`;;
152 let fan_datum = new_definition
154 IMAGE p (0..(k-1)) SUBSET ball_annulus /\
155 (!i j. (i < k) /\ (j < k) /\ dist(p i,p j) < &2 ==> (i=j)) /\
156 (!i. (i<k) /\ (i IN J) ==> dist(p i, p ((i+1) MOD k)) = &2 * h0) /\
157 (!i. (i<k) ==> dist(p i, p ((i+1) MOD k)) <= &2 * h0) /\
158 (!i j. (i+1<j) /\ (j<k) /\ (j +1 < i+k) ==> &2 * h0 <= dist(p i, p j)) /\
159 (CARD(J) <= 3) /\ (3 <= k) /\ (k + CARD(J) <= 6) /\
160 (!i. (i<k) ==> azim (vec 0) (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) <= pi) /\
161 (!i j. (i<k) /\ (j<k) ==> p j IN cwedge (vec 0) (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) )`;;
163 let vertex_slice = new_definition
164 `vertex_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER i) v | i IN (1..j) }`;;
166 let edge_slice = new_definition
167 `edge_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER j) v, v } INSERT
168 { {(rho_node1 (V,E,f) POWER i) v , (rho_node1 (V,E,f) POWER (i+1)) v } | i IN (1..(j-1)) }`;;
170 let face_slice = new_definition
171 `face_slice (V,E,f) v j = ( (rho_node1 (V,E,f) POWER j) v, v ) INSERT
172 { ((rho_node1 (V,E,f) POWER i) v , (rho_node1 (V,E,f) POWER (i+1)) v ) | i IN (1..(j-1)) }`;;
174 let kmin = new_definition
176 ({ k | (k=0) /\ (! V E f S. special_fan (V,E,f,S) ==>
177 tauVEF (V,E,f) >= d2_special (V,E,f,S) ) } UNION
178 { k | ? V E f S. (k= CARD(E)) /\ special_fan (V,E,f,S) /\ tauVEF(V,E,f) < d2_special (V,E,f,S) } )`;;
180 let taumin = new_definition
182 { tauVEF (V,E,f) - d2_special (V,E,f,S) | special_fan (V,E,f,S) /\ (kmin = CARD E) } UNION
183 { t | (t= &0) /\ (kmin = 0) })`;;
185 let minimal_fan = new_definition
186 `minimal_fan (V,E,f,S) <=> special_fan (V,E,f,S) /\ (kmin = CARD E) /\
187 (taumin = tauVEF (V,E,f) - d2_special (V,E,f,S))`;;
189 let s_extremal_edge = new_definition
190 `s_extremal_edge (V,E,f,S) (v,w) <=> (v,w ) IN S \/ (dist(v,w) IN {&2, &2 * h0 }) `;;
192 let s_minimal_edge = new_definition
193 `s_minimal_edge (V,E,f,S) (v,w) <=> (v,w) IN S \/ (dist(v,w) = &2) `;;
195 let special_feature_extreme_edge = new_definition
196 `special_feature_extreme_edge (V,E,f,S) = (!v w. {v,w} IN E ==> s_extremal_edge (V,E,f,S) (v,w))`;;