(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Definitions *) (* Chapter: Tame Hypermap *) (* Author: Thomas C. Hales *) (* Date: 2010-07-07 *) (* ========================================================================== *) (* Definitions file for Local Fans This file was split off from tame/tame_defs.hl in July 2010 when it was discovered that there are many incompatible definitions betwen the Local Fans chapter and the Tame chapter. This file is not currently part of the build. *) flyspeck_needs "hypermap/hypermap.hl";; flyspeck_needs "fan/fan_defs.hl";; flyspeck_needs "packing/pack_defs.hl";; module Local_fan_defs = struct 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}`;; let cw_dart_fan=new_definition `cw_dart_fan (V:real^3->bool) (E:(real^3->bool)->bool) ((v:real^3),(w:real^3))= 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 local_fan = new_definition `local_fan (V,E,f) <=> FAN (vec 0,V,E) /\ f IN face_set_of_fan (V,E) /\ (hypermap_of_fan (V,E)) iso (cyclic_hypermap I I (CARD f))`;; let convex_local_fan = new_definition `convex_local_fan (V,E,f) <=> local_fan (V,E,f) /\ (!x. (x IN f) ==> azim_dart (V,E) x <= pi) /\ (!x. (x IN f) ==> V SUBSET cw_dart_fan V E x)`;; let rho_node1 = new_definition `rho_node1 (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;; let order_permutation = new_definition `order_permutation (p:A->A) = (minimal) { m | (p POWER m = I) /\ (m > 0) }`;; let is_cyclic_permutation = new_definition `is_cyclic_permutation rho s <=> rho permutes s /\ s HAS_SIZE (order_permutation rho)`;; let interior_angle = new_definition `interior_angle (V,E,f) v = azim_dart (V,E) (v,(rho_node1 (V,E,f) v))`;; let cw_node_fan = new_definition `cw_node_fan (V,E,f) v = cw_dart_fan V E (v,rho_node1(V,E,f) v)`;; let w_node_fan = new_definition (* 4th component is ignored *) `w_node_fan (V,E,f) v = w_dart_fan (vec 0) V E (vec 0,v,rho_node1(V,E,f) v,v)`;; let localization = new_definition `localization (V,E,f) = {v | v IN V /\ (?w. w IN V /\ (v,w) IN f)}, { {v,w} | {v,w} IN E /\ (v,w) IN f}, f`;; let is_generic_clf = new_definition `is_generic_clf (V,E,f:A) <=> (! v w (u:real^3). (u IN V) /\ {v,w} IN E ==> aff_ge { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {})`;; let is_circular_clf = new_definition `is_circular_clf (V,E,f:A) <=> (? v w (u:real^3). (u IN V) /\ {v,w} IN E /\ ~( aff_gt { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {}))`;; let is_lunar_clf = new_definition `is_lunar_clf (V,E,f:A) (v,w) <=> v IN V /\ w IN V /\ ~(is_circular_clf (V,E,f)) /\ collinear {(vec 0) , v, w}`;; let is_flat = new_definition `is_flat (V,E,f) v <=> interior_angle (V,E,f) v = pi`;; let is_deformation_clf = new_definition `is_deformation_clf phi V s = (!v x. v IN V ==> (phi v) continuous at x within s)`;; let node_deform = new_definition `node_deform phi V t = { phi v t | v IN V}`;; let edge_deform = new_definition `edge_deform phi V E t = { {phi v t, phi w t} | {v,w} IN E}`;; let face_deform = new_definition `face_deform phi V f t = { (phi v t, phi w t) | (v,w) IN f}`;; let per = new_definition `per(V,E,f) v k = sum (0..k-1) ( \ i. arcV (vec 0) ((rho_node1 (V,E,f) POWER i) v) ((rho_node1 (V,E,f) POWER (i+1)) v))`;; let perimeter = new_definition `perimeter(V,E,f) = per(V,E,f) (CHOICE V) (CARD(f))`;; let perimeterbound = new_definition `perimeterbound (V,E) = (!f. f IN face_set_of_fan (V,E) ==> sum f (\ (v,w). arcV (vec 0) (v:real^3) w ) <= &2 * pi)`;; let special_fan = new_definition `special_fan (V,E,f,S) <=> packing V /\ V SUBSET ball_annulus /\ convex_local_fan (V,E,f) /\ S SUBSET E /\ (! v w. {v,w} IN S ==>( dist(v,w) = &2 * h0)) /\ (! v w. {v,w} IN E ==> (dist(v,w) <= &2 * h0)) /\ (! v w. v IN V /\ w IN V /\ ~(v=w) /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))`;; let r_special = new_definition `r_special (V,E,f,S) = CARD(E) - CARD(S)`;; let s_special = new_definition `s_special (V,E,f,S) = CARD(S)`;; let d2_tame = new_definition (* deprecate *) `d2_tame r s = if (r + 2*s > 3) then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4) else #0.0`;; let tame_table_d = new_definition `tame_table_d r s = if (r + 2*s > 3) then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4) else #0.0`;; (* preferred term *) let d2_special = new_definition `d2_special (V,E,f,S) = d2_tame (r_special (V,E,f,S)) (s_special (V,E,f,S))`;; let vertex_datum = new_definition `vertex_datum p k = IMAGE p (0..(k-1))`;; let edge_datum = new_definition `edge_datum p k = { { p i, p ((i+1) MOD k) } |i| i IN (0..(k-1)) }`;; let face_datum = new_definition `face_datum p k = { (p i, p ((i+1) MOD k)) |i| i IN (0..(k-1)) }`;; let special_datum = new_definition `special_datum p k J = { (p i, (p((i+1) MOD k))) | i | i IN J }`;; let fan_datum = new_definition `fan_datum p k J <=> IMAGE p (0..(k-1)) SUBSET ball_annulus /\ (!i j. (i < k) /\ (j < k) /\ dist(p i,p j) < &2 ==> (i=j)) /\ (!i. (i dist(p i, p ((i+1) MOD k)) = &2 * h0) /\ (!i. (i dist(p i, p ((i+1) MOD k)) <= &2 * h0) /\ (!i j. (i+1 &2 * h0 <= dist(p i, p j)) /\ (CARD(J) <= 3) /\ (3 <= k) /\ (k + CARD(J) <= 6) /\ (!i. (i azim (vec 0) (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) <= pi) /\ (!i j. (i p j IN cwedge (vec 0) (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) )`;; let vertex_slice = new_definition `vertex_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER i) v | i IN (1..j) }`;; let edge_slice = new_definition `edge_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER j) v, v } INSERT { {(rho_node1 (V,E,f) POWER i) v , (rho_node1 (V,E,f) POWER (i+1)) v } | i IN (1..(j-1)) }`;; let face_slice = new_definition `face_slice (V,E,f) v j = ( (rho_node1 (V,E,f) POWER j) v, v ) INSERT { ((rho_node1 (V,E,f) POWER i) v , (rho_node1 (V,E,f) POWER (i+1)) v ) | i IN (1..(j-1)) }`;; let kmin = new_definition `kmin = (minimal) ({ k | (k=0) /\ (! V E f S. special_fan (V,E,f,S) ==> tauVEF (V,E,f) >= d2_special (V,E,f,S) ) } UNION { k | ? V E f S. (k= CARD(E)) /\ special_fan (V,E,f,S) /\ tauVEF(V,E,f) < d2_special (V,E,f,S) } )`;; let taumin = new_definition `taumin = inf ( { tauVEF (V,E,f) - d2_special (V,E,f,S) | special_fan (V,E,f,S) /\ (kmin = CARD E) } UNION { t | (t= &0) /\ (kmin = 0) })`;; let minimal_fan = new_definition `minimal_fan (V,E,f,S) <=> special_fan (V,E,f,S) /\ (kmin = CARD E) /\ (taumin = tauVEF (V,E,f) - d2_special (V,E,f,S))`;; let s_extremal_edge = new_definition `s_extremal_edge (V,E,f,S) (v,w) <=> (v,w ) IN S \/ (dist(v,w) IN {&2, &2 * h0 }) `;; let s_minimal_edge = new_definition `s_minimal_edge (V,E,f,S) (v,w) <=> (v,w) IN S \/ (dist(v,w) = &2) `;; let special_feature_extreme_edge = new_definition `special_feature_extreme_edge (V,E,f,S) = (!v w. {v,w} IN E ==> s_extremal_edge (V,E,f,S) (v,w))`;; end;;