text_formalization/fan/fan_defs.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definitions                                                                *)
   5 (* Chapter: Fan                                                               *)
   6 (* Authors: Thomas C. Hales, Hoang Le Truong, Alexey Solovyev                 *)
   7 (* Date: 2010-05-11                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 Definitions file for Fan
  12 *)
  13
  14 flyspeck_needs "general/sphere.hl";;
  15 flyspeck_needs "volume/vol1.hl";;
  16 flyspeck_needs "hypermap/hypermap.hl";;
  17
  18 module Fan_defs  = struct
  19
  20
  21
  22 (* General definitions *)
  23
  24 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
  25
  26 (* AS:
  27         Maybe it is better to change names to something like fan_card, fan_origin, fan_non_parallel, fan_intersection,
  28         because names like fan1, fan2, fan6, fan7 are not descriptive at all.
  29
  30         If the names are changed, then it will be required to modify fan/*.hl as well. I think,
  31         it is quite easy and fast: search for all occurrences of fan1 and change it to fan_card, etc.
  32         This procedure should take at most 10-20 minutes.
  33 *)
  34
  35 (* Cardinality *)
  36 let fan1 = new_definition `fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {})`;;
  37 (* Origin *)
  38 let fan2 = new_definition `fan2(x,V,E):bool <=> ~(x IN V)`;;
  39 (* Non-parallel *)
  40 let fan6 = new_definition `fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
  41 (* Intersection *)
  42 let fan7 = new_definition `fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  43 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
  44
  45 (* Fan *)
  46
  47 (* AS:
  48         In my opinion, the name `fan` is better because it follows the general convention of naming objects
  49         in HOL Light.
  50
  51         The file fan/introduction.hl already contains the definition of the constant `fan`. Probably, it is an earlier definition
  52         of fan. Now, it should be deprecated. Again, I think it will be not difficult to make corresponding
  53         changes in fan/*.hl
  54 *)
  55 let FAN = new_definition `FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
  56 fan6(x,V,E)/\ fan7(x,V,E)`;;
  57
  58 (* E(v) *)
  59 let set_of_edge = new_definition `set_of_edge v V E = {w | {v,w} IN E /\ w IN V}`;;
  60
  61 (* sigma *)
  62 let sigma_fan = new_definition `sigma_fan x (V:real^3->bool) E v u =
  63                                         if (set_of_edge v V E = {u}) then u
  64                                         else (@(w:real^3). w IN (set_of_edge v V E) /\ ~(w = u) /\
  65                                                 (!(w1:real^3). w1 IN (set_of_edge v V E) /\ ~(w1=u) ==> azim x v u w <= azim x v u w1))`;;
  66
  67 (* AS:
  68         This definition is not very important (there is only one result involving this definition
  69         which proves that extension_sigma_fan permutes set_of_edge). But I decided that it is simpler
  70         to have this definition rather than modify the definition of sigma_fan
  71 *)
  72
  73 (* THALES:
  74    It appears that there are three definitions of inverse_sigma_fan from the files introduction.hl, fan_misc.hl, and fan_defs.hl
  75    I am renaming the one in fan/introduction.hl inverse_sigma_fan_alt and the one in fan_misc.hl as inverse_sigma_fan_bis.
  76    I take the one in fan_defs.hl to be the primary definition.
  77 *)
  78
  79 let extension_sigma_fan = new_definition `extension_sigma_fan x (V:real^3->bool) E v u =
  80                                         if ~(u IN set_of_edge v V E ) then u
  81                                                 else (sigma_fan x V E v u)`;;
  82
  83 let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse (extension_sigma_fan x V E v)`;;
  84
  85
  86 (* Hypermap of Fan *)
  87
  88 let dart1_of_fan = new_definition
  89   `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  { (v,w) | {v,w} IN E }`;;
  90
  91
  92 let dart_of_fan = new_definition
  93   `dart_of_fan (V,E) =
  94    { (v,v) | v IN V /\ set_of_edge (v:real^3) V E = {} } UNION { (v,w) | {v,w} IN E }`;;
  95
  96
  97 (* in fan/introduction.hl a dart is a 4-tuple.  Here it is a pair.  Here is the correspondence *)
  98 (* AS:
  99         Do we need this correspondence?
 100         Right now, there are no results involving `extended_dart` or `contracted_dart`.
 101         Ultimately, it is better to use new definition of darts as pairs everywhere.
 102 *)
 103 let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
 104
 105 let extended_dart = new_definition
 106   `extended_dart (V,E) (v,w) = i_fan (vec 0) V E (vec 0, v, w, w)`;;
 107
 108 let contracted_dart = new_definition
 109   `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;
 110
 111 (* e_fan, n_fan, f_fan of fan/introduction.hl, restricted to pairs *)
 112
 113 (* AS:
 114         In my opinion, it is better to change the names e_fan_pair, n_fan_pair, f_fan_pair
 115         to e_fan, n_fan, f_fan.
 116         It will require some modifications in fan/introduction.hl, but it is not a problem
 117 *)
 118
 119 let e_fan_pair = new_definition `e_fan_pair (V,E) (v,w) = (w,v)`;;
 120
 121 let n_fan_pair = new_definition
 122   `n_fan_pair (V,E) (v,w) = v,sigma_fan (vec 0) V E v w`;;
 123
 124 let f_fan_pair = new_definition
 125   `f_fan_pair (V,E) (v,w) = w,(inverse_sigma_fan (vec 0) V E w v)`;;
 126
 127
 128 let hypermap_of_fan  = new_definition
 129   `hypermap_of_fan (V,E) =
 130     (let p = ( \ t. res (t (V,E) ) (dart1_of_fan (V,E)) ) in
 131           hypermap( dart_of_fan (V,E) , p e_fan_pair, p n_fan_pair, p f_fan_pair))`;;
 132
 133 (* Restricted versions of e_fan_pair, n_fan_pair, f_fan_pair (for convenience) *)
 134 let e_fan_pair_ext = new_definition `e_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then e_fan_pair (V,E) x else x`;;
 135
 136 let n_fan_pair_ext = new_definition `n_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then n_fan_pair (V,E) x else x`;;
 137
 138 let f_fan_pair_ext = new_definition `f_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then f_fan_pair (V,E) x else x`;;
 139
 140
 141 let E_FAN_PAIR_EXT = prove(`!V E. e_fan_pair_ext (V,E) = res (e_fan_pair (V,E)) (dart1_of_fan (V,E))`,
 142                                   REWRITE_TAC[FUN_EQ_THM; e_fan_pair_ext; Sphere.res]);;
 143
 144 let F_FAN_PAIR_EXT = prove(`!V E. f_fan_pair_ext (V,E) = res (f_fan_pair (V,E)) (dart1_of_fan (V,E))`,
 145                                   REWRITE_TAC[FUN_EQ_THM; f_fan_pair_ext; Sphere.res]);;
 146
 147 let N_FAN_PAIR_EXT = prove(`!V E. n_fan_pair_ext (V,E) = res (n_fan_pair (V,E)) (dart1_of_fan (V,E))`,
 148                                   REWRITE_TAC[FUN_EQ_THM; n_fan_pair_ext; Sphere.res]);;
 149
 150 let HYPERMAP_OF_FAN_ALT = prove(`!V E. hypermap_of_fan (V,E) =
 151                 hypermap (dart_of_fan (V,E), e_fan_pair_ext (V,E), n_fan_pair_ext (V,E), f_fan_pair_ext (V,E))`,
 152         REPEAT GEN_TAC THEN
 153         REWRITE_TAC[CONV_RULE (DEPTH_CONV let_CONV) hypermap_of_fan] THEN
 154         REWRITE_TAC[E_FAN_PAIR_EXT; F_FAN_PAIR_EXT; N_FAN_PAIR_EXT]);;
 155
 156
 157 (* Topological component and dart *)
 158
 159 (* X(V,E) *)
 160 let xfan = new_definition `xfan (x,V,E) = {v | ?e. (E e) /\ (v IN aff_ge {x} e)}`;;
 161
 162 (* Y(V,E) *)
 163 let yfan = new_definition `yfan (x,V,E) = (:real^3) DIFF xfan (x,V,E)`;;
 164
 165 (* AS:
 166         The original definition of yfan (renamed yfan_deprecated in fan/introduction.hl) is the following:
 167 let yfan_deprecated = new_definition `yfan_deprecated (x,V,E) = {v:real^3 | ?e. (E e) /\ (~(v IN aff_ge {x} e))}`;;
 168         It seems to be wrong since the negation of (?e. (E e) /\ (v IN aff_ge {x} e)) is
 169         (!e. (E e) /\ ~(v IN aff_ge {x} e)).
 170 *)
 171
 172
 173 (* W^0_{dart}(x) *)
 174
 175 (* AS:
 176         It is better to have
 177         w_dart_fan x V E (v,w),
 178         or even
 179         w_dart_fan V E (v,w)
 180 *)
 181 let w_dart_fan = new_definition `w_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3)=
 182  if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
 183  else
 184    (if set_of_edge v V E = {w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
 185     else (if set_of_edge v V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
 186
 187
 188 (* DEPRECATED, 2011-08-01, --> wedge_ge
 189 let cwedge = new_definition `cwedge v0 v1 w1 w2 =
 190          {y |  &0 <= azim v0 v1 w1 y /\
 191               azim v0 v1 w1 y <= azim v0 v1 w1 w2}`;;
 192 *)
 193
 194 (* W_{dart}(x) *)
 195
 196 (* DEPRECATED, 2011-08-01
 197 let cw_dart_fan=new_definition `cw_dart_fan (V:real^3->bool) E (v,w)=
 198   if (CARD (set_of_edge v V E) > 1)
 199   then cwedge (vec 0) v w (sigma_fan (vec 0) V E v w)
 200   else (:real^3)`;;
 201 *)
 202
 203 let azim_fan = new_definition `azim_fan x (V:real^3->bool) E v w =
 204   if (CARD (set_of_edge v V E) > 1)
 205   then azim x v w (sigma_fan x V E v w)
 206   else &2 * pi`;;
 207
 208 (* azim(x) *)
 209 let azim_dart = new_definition
 210   `azim_dart (V,E) (v,w) =
 211   if (v=w) then &2 * pi else azim_fan (vec 0) V E v w`;;
 212
 213 (* rcone^0(x,v,h) *)
 214 let rcone_fan = new_definition `rcone_fan  (x:real^3) (v:real^3) (h:real) =
 215                         {y:real^3 | (y-x) dot (v-x) > (dist(y,x)*dist(v,x)*h)}`;;
 216
 217 (* W^0_{dart}(x,epsilon) *)
 218 (* AS:
 219         It is better to have rw_dart_fan V E (v,w)
 220
 221         In the book, it is defined as ... INTER rcone_fan x v (cos h),
 222     in fan/introduction.hl, it is used as rw_dart_fan x V E (...) (cos s) instead (not always but only when necessary).
 223         This can lead to confusions. In my opinion, it is simpler to follow the book definition. In this case,
 224         some changes in fan/introduction.hl are required.
 225 *)
 226 let rw_dart_fan = new_definition
 227   `rw_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3) h =
 228                 w_dart_fan x V E (y,v,w,w1) INTER rcone_fan x v h`;;
 229
 230 let topological_component_yfan = new_definition
 231   `topological_component_yfan ((x:real^3),(V:real^3->bool),E) =
 232       {  connected_component (yfan (x,V,E)) y  | y | y IN yfan (x,V,E) }`;;
 233
 234 (* there is a function dart_leads_into in fan/introduction.hl.  This is a bit simpler. *)
 235
 236 (* AS:
 237         It is better to change name to `dart_leads_into`.
 238
 239         For the current definition of rw_dart_fan, should be: rw_dart_fan ... (cos eps),
 240         but I prefer to change the definition of rw_dart_fan instead.
 241 *)
 242 let dart_leads_into1 = new_definition
 243     `dart_leads_into1 (x,V,E) (v,u) = @s.  s IN topological_component_yfan (x,V,E) /\
 244         (?eps. (eps < &1) /\
 245            rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps  SUBSET s)`;;
 246
 247 let dartset_leads_into = new_definition
 248   `dartset_leads_into (x,V,E) ds =
 249     @s. (!y. (y IN ds) ==> (s = dart_leads_into1 (x,V,E) y))`;;
 250
 251 (* node(x) not needed, use FST x *)
 252
 253
 254 (* compare fan80 and fan81, which define fully_surrounded *)
 255 let surrounded_node = new_definition
 256   `surrounded_node (V,E) v =
 257   !x. (x IN dart_of_fan (V,E)) /\ (FST x = v) ==> azim_dart (V,E) x < pi`;;
 258
 259
 260 let fully_surrounded = new_definition
 261         `fully_surrounded (V,E) = (!x. x IN dart_of_fan (V,E) ==> azim_dart (V,E) x < pi)`;;
 262
 263 (* AS: the definitions from fan/introduction.hl are below:
 264 let fan81=new_definition`fan81 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> azim_fan x V E v u <pi)`;;
 265
 266 let fan80=new_definition`fan80 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> &0< azim x v u (sigma_fan x V E v u) /\ azim x v u (sigma_fan x V E v u) <pi)`;;
 267 *)
 268
 269 (* Conformance *)
 270 let conforming_bijection = new_definition `conforming_bijection (V,E) <=>
 271   !s. s IN topological_component_yfan (vec 0,V,E) ==> (?!f. f IN face_set (hypermap_of_fan (V,E)) /\
 272                                                          s = dartset_leads_into (vec 0,V,E) f)`;;
 273
 274
 275 let conforming_half_space = new_definition `conforming_half_space (V,E) <=>
 276         !f. f IN face_set (hypermap_of_fan (V,E)) ==>
 277                 dartset_leads_into (vec 0,V,E) f =
 278                         INTERS {aff_gt {vec 0, FST x, FST (f_fan_pair (V,E) x)} {FST (inverse (f_fan_pair (V,E)) x)} | x IN f}`;;
 279
 280
 281 let conforming_solid_angle = new_definition `conforming_solid_angle (V,E) <=>
 282   !f. f IN face_set (hypermap_of_fan (V,E)) ==>
 283   (let U = dartset_leads_into (vec 0,V,E) f in
 284      (!r. measurable (ball (vec 0,r) INTER U)) /\
 285        eventually_radial (vec 0) U /\
 286        sol (vec 0) U = &2 * pi + sum (f) (\x. azim_dart (V,E) x - pi))`;;
 287
 288
 289 let conforming_diagonal = new_definition `conforming_diagonal (V,E) <=>
 290         (!f x y. f IN face_set (hypermap_of_fan (V,E)) /\ x IN f /\ y IN f /\ ~(x = y) ==>
 291                 ~collinear {vec 0, FST x, FST y} /\
 292                 (y = f_fan_pair (V,E) x \/ x = f_fan_pair (V,E) y \/
 293                         aff_gt {vec 0} {FST x, FST y} SUBSET dartset_leads_into (vec 0,V,E) f))`;;
 294
 295
 296 let conforming = new_definition `conforming (V,E) <=>
 297         fully_surrounded (V,E) /\
 298         conforming_bijection (V,E) /\
 299         conforming_half_space (V,E) /\
 300         conforming_solid_angle (V,E) /\
 301         conforming_diagonal (V,E)`;;
 302
 303 end;;
 304