legacy/oldlocal/ch_local/local_defs.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definitions                                                                  *)
   5 (* Chapter: Tame Hypermap                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-07                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11
  12 Definitions file for Local Fans
  13
  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.
  17
  18 This file is not currently part of the build.
  19 *)
  20
  21 flyspeck_needs "hypermap/hypermap.hl";;
  22 flyspeck_needs "fan/fan_defs.hl";;
  23 flyspeck_needs "packing/pack_defs.hl";;
  24
  25 module Local_fan_defs  = struct
  26
  27
  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}`;;
  31
  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)
  36 else (:real^3)`;;
  37
  38 let local_fan = new_definition `local_fan (V,E,f) <=>
  39    FAN (vec 0,V,E) /\
  40    f IN face_set_of_fan (V,E) /\
  41    (hypermap_of_fan (V,E)) iso (cyclic_hypermap I I (CARD f))`;;
  42
  43 let convex_local_fan = new_definition `convex_local_fan (V,E,f) <=>
  44     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)`;;
  47
  48 let rho_node1 = new_definition
  49   `rho_node1 (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;;
  50
  51 let order_permutation = new_definition
  52   `order_permutation (p:A->A) = (minimal) { m | (p POWER m = I) /\ (m > 0) }`;;
  53
  54 let is_cyclic_permutation = new_definition
  55   `is_cyclic_permutation rho s <=>
  56    rho permutes s /\ s HAS_SIZE (order_permutation rho)`;;
  57
  58 let interior_angle = new_definition
  59   `interior_angle (V,E,f) v = azim_dart (V,E) (v,(rho_node1 (V,E,f) v))`;;
  60
  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)`;;
  63
  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)`;;
  66
  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},
  70    f`;;
  71
  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 } = {})`;;
  75
  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 } = {}))`;;
  79
  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}`;;
  83
  84 let is_flat = new_definition `is_flat (V,E,f) v <=>
  85   interior_angle (V,E,f) v = pi`;;
  86
  87
  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)`;;
  90
  91 let node_deform = new_definition
  92   `node_deform phi V t = { phi v t | v IN V}`;;
  93
  94 let edge_deform = new_definition
  95   `edge_deform phi V E t = { {phi v t, phi w t} | {v,w} IN E}`;;
  96
  97 let face_deform = new_definition
  98   `face_deform phi V f t = { (phi v t, phi w t) | (v,w) IN f}`;;
  99
 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))`;;
 103
 104 let perimeter = new_definition
 105 `perimeter(V,E,f)  = per(V,E,f) (CHOICE V)  (CARD(f))`;;
 106
 107
 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)`;;
 111
 112
 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) /\
 115     S SUBSET E /\
 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))`;;
 119
 120 let r_special = new_definition
 121   `r_special (V,E,f,S) = CARD(E) - CARD(S)`;;
 122
 123 let s_special = new_definition
 124   `s_special (V,E,f,S) = CARD(S)`;;
 125
 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)
 129   else #0.0`;;
 130
 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 *)
 135
 136
 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))`;;
 139
 140 let vertex_datum = new_definition
 141   `vertex_datum p k = IMAGE p (0..(k-1))`;;
 142
 143 let edge_datum = new_definition
 144   `edge_datum p k  = { { p i, p ((i+1) MOD k) }  |i| i IN (0..(k-1)) }`;;
 145
 146 let face_datum = new_definition
 147   `face_datum p k = { (p i, p ((i+1) MOD k)) |i|  i IN (0..(k-1)) }`;;
 148
 149 let special_datum = new_definition
 150   `special_datum p k J = { (p i, (p((i+1) MOD k))) | i | i IN J }`;;
 151
 152 let fan_datum = new_definition
 153   `fan_datum p k J <=>
 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)) )`;;
 162
 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)  }`;;
 165
 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)) }`;;
 169
 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)) }`;;
 173
 174 let kmin = new_definition
 175   `kmin = (minimal)
 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) } )`;;
 179
 180 let taumin = new_definition
 181   `taumin = inf (
 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) })`;;
 184
 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))`;;
 188
 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 }) `;;
 191
 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) `;;
 194
 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))`;;
 197
 198
 199
 200
 201 end;;