text_formalization/tame/tame_defs.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definitions                                                                *)
   5 (* Chapter: Tame Hypermap                                                     *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-27                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 Definitions file for Tame Hypermap
  12 *)
  13
  14 flyspeck_needs "hypermap/hypermap.hl";;
  15 flyspeck_needs "fan/fan_defs.hl";;
  16 flyspeck_needs "packing/pack_defs.hl";;
  17
  18 module Tame_defs  = struct
  19
  20
  21
  22
  23 (*
  24 let edge_nondegenerate = new_definition `edge_nondegenerate (H:(A)hypermap)
  25    <=> !(x:A).(x IN dart H) ==> ~ (edge_map H x = x)`;;
  26 *)
  27
  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))`;;
  30
  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))`;;
  33
  34
  35
  36 (* no_loops does not restrict x,y to be darts.  But edge H is the
  37    identitiy outside darts, so this is OK. *)
  38
  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`;;
  40
  41 (* this definition is more complicated than it needs to be.  It is
  42    better to use hypermap.hl is_no_double_joints *)
  43
  44 (*
  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`;;
  50 *)
  51
  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)`;;
  54
  55 let exceptional_face = new_definition `exceptional_face (H:(A)hypermap) (x:A) <=> CARD (face H x) >= 5`;;
  56
  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 }`;;
  60
  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}`;;
  64
  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)}`;;
  68
  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}`;;
  72
  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 ))`;;
  78
  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)`;;
  82
  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`;;
  86
  87
  88 let tgt = new_definition `tgt = #1.541`;;
  89
  90 (* b table constants corrected 2010-06-17 *)
  91
  92     let b_tame = new_definition
  93   `b_tame p q=
  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
 109     else tgt`;;
 110
 111
 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`;;
 117
 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.  *)
 120
 121 let a_tame = new_definition `a_tame = #0.63`;;
 122
 123 let total_weight = new_definition
 124   `total_weight (H:(A)hypermap) (w:(A->bool)->real) = sum (face_set H) w`;;
 125
 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)))`;;
 128
 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)))))`;;
 134
 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)`;;
 139
 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`;;
 143
 144
 145 (* def of tame *)
 146
 147 let tame_1 = new_definition
 148   `tame_1 (H:(A)hypermap) <=>
 149   plain_hypermap (H:(A)hypermap) /\ planar_hypermap (H:(A)hypermap)`;;
 150
 151 let tame_2 = new_definition
 152   `tame_2 (H:(A)hypermap) <=>
 153   connected_hypermap H /\ simple_hypermap H`;;
 154
 155 let tame_3 = new_definition
 156   `tame_3 (H:(A)hypermap)  <=>  is_edge_nondegenerate H `;;
 157
 158 let tame_4 = new_definition
 159   `tame_4 (H:(A)hypermap)  <=> no_loops H`;;
 160
 161 let tame_5a = new_definition
 162   `tame_5a (H:(A)hypermap)  <=> is_no_double_joints H`;;
 163
 164 let tame_8 = new_definition
 165   `tame_8 (H:(A)hypermap)  <=> number_of_faces H >= 3`;;
 166
 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)`;;
 170
 171 let tame_10 = new_definition
 172   `tame_10 (H:(A)hypermap) <=>
 173    number_of_nodes H  IN { 13, 14, 15 } `;;
 174
 175 let tame_11a = new_definition
 176   `tame_11a (H:(A)hypermap) <=>
 177    (!(x:A). x IN dart H ==>  CARD (node H x) >= 3)`;;
 178
 179 let tame_11b = new_definition
 180   `tame_11b (H:(A)hypermap) <=>
 181    (!(x:A). x IN dart H ==> CARD (node H x) <= 7)`;;
 182
 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)`;;
 186
 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)`;;
 190
 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`;;
 196
 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))`;;
 200
 201
 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}`;;
 204
 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 }`;;
 207
 208 (*
 209 let isolated_node = new_definition
 210   `isolated_node v V E = (set_of_edge v V E = {})`;;
 211 *)
 212
 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`;;
 215
 216 let dart1_of_fan = new_definition
 217   `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  { (v,w) | {v,w} IN E }`;;
 218
 219 let dart_of_fan = new_definition
 220   `dart_of_fan (V,E) =
 221    { (v,v) | v IN V /\ set_of_edge (v:real^3) V E = {} } UNION { (v,w) | {v,w} IN E }`;;
 222
 223  (* in fan/introduction.hl a dart is a 4-tuple.  Here it is a pair.  Here is the correspondence *)
 224
 225 let extended_dart = new_definition
 226   `extended_dart (V,E) (v,w) = i_fan (vec 0) V E (vec 0, v, w, w)`;;
 227
 228 let contracted_dart = new_definition
 229   `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;
 230
 231 (* e_fan, n_fan, f_fan of fan/introduction.hl, restricted to pairs *)
 232
 233 let e_fan_pair = new_definition `e_fan_pair (V,E) (v,w) = (w,v)`;;
 234
 235 let n_fan_pair = new_definition
 236   `n_fan_pair (V,E) (v,w) = v,sigma_fan (vec 0) V E v w`;;
 237
 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)`;;
 240
 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))`;;
 245
 246 let face_set_of_fan = new_definition
 247   `face_set_of_fan (V,E) = face_set (hypermap_of_fan (V,E))`;;
 248
 249
 250 (* compare fan80 and fan81, which define fully_surrounded *)
 251
 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`;;
 255
 256 let scriptL = new_definition
 257   `scriptL V = sum V ( \ (v:real^3) . lmfun (norm v  /  &2)) `;;
 258
 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) ))`;;
 265
 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) }`;;
 269
 270 (* there is a function dart_leads_into in fan/introduction.hl.  This is a bit simpler. *)
 271
 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) /\
 274         (?eps. (eps < &1) /\
 275            rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps  SUBSET s)`;;
 276
 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))`;;
 280
 281 (* node(x) not needed, use FST x *)
 282
 283 let h_dart = new_definition `h_dart (x:real^3#B) = norm (FST x)  / &2`;;
 284
 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)))`;;
 287
 288
 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)`;;
 293
 294 (* deprecated 2013-2-22 : Use rho_node1 which has been developed further,
 295    per -> .
 296    perimeterbound -> .  They haven't been developed.
 297  *)
 298
 299 let rho_node = new_definition
 300   `rho_node (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;;
 301
 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))`;;
 305
 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)`;;
 309
 310
 311 end;;
 312