legacy/oldfan/definition_fan.hl

   1 module Definition_fan  = struct
   2
   3
   4 open Sphere;;
   5 open Fan_defs;;
   6
   7
   8 (* ========================================================================== *)
   9 (*                                FAN                       *)
  10 (* ========================================================================== *)
  11
  12
  13
  14 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
  15
  16 let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
  17
  18 let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
  19
  20 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
  21
  22 let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
  23
  24 let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
  25
  26 let fan = new_definition`fan(x,V,E)<=>  ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;;
  27
  28 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
  29
  30 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
  31
  32
  33 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
  34
  35 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})
  36 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
  37
  38
  39
  40 let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
  41 fan6(x,V,E)/\ fan7(x,V,E)`;;
  42
  43 (* ========================================================================== *)
  44 (*                   DEFINITION OF SIGMA_FAN AND INVERSE1_SIGMA_FAN (^_^)                    *)
  45 (* ========================================================================== *)
  46
  47
  48 let sigma_fan=new_definition`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
  49 (if (set_of_edge v V E = {u} ) then u
  50     else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
  51 (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
  52
  53
  54 (* This extends sigma to have a larger domain
  55    of R^3 rather than just V.  It is the
  56    identity outside V (compare the definition
  57    of `permutes` ).   *)
  58
  59
  60
  61
  62 let extension_sigma_fan=new_definition`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=
  63 (if ~(u IN set_of_edge v V E ) then u
  64     else (sigma_fan x V E v u))`;;
  65
  66
  67
  68 let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
  69
  70
  71
  72 let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
  73 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
  74 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
  75
  76
  77
  78 (* ========================================================================== *)
  79 (*                   DEFINITION OF HYPERMAP OF FAN                    *)
  80 (* ========================================================================== *)
  81
  82
  83
  84 let d1_fan =new_definition`
  85 d1_fan (x,V,E) ={(x':real^3,v:real^3,w:real^3,w1:real^3)| (x'=x) /\ ({v,w} IN  E)/\ (w1 = sigma_fan x V E v w)}`;;
  86
  87
  88 let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
  89
  90 let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
  91
  92
  93 let inverse_sigma_fan_alt=new_definition`inverse_sigma_fan_alt x V E v w = @a. sigma_fan x V E v a=w`;;
  94
  95 let e_fan=new_definition` e_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,v,(sigma_fan x V E w v)))`;;
  96
  97
  98 let f_fan=new_definition`f_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse_sigma_fan_alt x V E w v),v) )`;;
  99
 100 (* This is the same as f_fan,
 101    but easier to use *)
 102
 103 let f1_fan=new_definition`f1_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse1_sigma_fan x V E w v),v) )`;;
 104
 105
 106
 107 let n_fan=new_definition`n_fan (x:real^3) V E =(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,(sigma_fan x V E v w),(sigma_fan x V E v (sigma_fan x V E v w))))`;;
 108
 109 (* i_fan corrects the 4th coordinate to be
 110    the dart *)
 111
 112 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)))`;;
 113
 114 let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
 115
 116 let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
 117
 118 let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
 119
 120 let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
 121
 122 (* if f = sigma, the power_map_points gives
 123    iterates of sigma (for fixed x v) *)
 124
 125
 126 let power_map_points= new_recursive_definition num_RECURSION `(power_map_points f x V E v w 0 = w)/\(power_map_points f x V E v w  (SUC n)= f x V E v (power_map_points f x V E v w n))`;;
 127
 128 (* This is the composition operator (o),
 129    specialized to functions on 4-tuples *)
 130
 131 let o_funs=new_definition`!(f:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (g:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3). o_funs f g =(\(x:real^3,y:real^3,z:real^3,t:real^3).  f (pr1 (g(x,y,z,t)),pr2(g(x,y,z,t)),pr3(g(x,y,z,t)),pr4(g(x,y,z,t))))`;;
 132
 133 (* powers of permutations *)
 134
 135 let power_maps= new_recursive_definition num_RECURSION `(power_maps  (f:real^3->(real^3->bool)->((real^3->bool)->bool)->real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) 0 = i_fan (x:real^3) V E) /\ (power_maps f x V E (SUC n)= o_funs (f x V E)  (power_maps f x V E n))`;;
 136
 137
 138 (* powers of node map *)
 139
 140
 141
 142
 143 let power_n_fan= new_definition`power_n_fan x V E n=( \(x,v,w,w1). (x,v,(power_map_points sigma_fan x V E v w n),(power_map_points sigma_fan x V E v w (SUC n))))`;;
 144
 145
 146 (* the node of a dart, in a special form
 147    for fans *)
 148
 149
 150 let a_node_fan=new_definition`a_node_fan x V E (x,v,w,w1)={a | ?n. a=(power_maps  n_fan x V E n) (x,v,w,sigma_fan x V E v w)}`;;
 151
 152
 153 (* The set X(V,E) *)
 154
 155 let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
 156
 157 (* See comment by AS in fan_defs.hl.  The correct definition is there. *)
 158 let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;
 159
 160
 161
 162
 163
 164
 165
 166 let hypermap_of_fanx = new_definition
 167   `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
 168     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
 169           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;
 170
 171
 172 let hypermap1_of_fanx = new_definition
 173   `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
 174     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
 175           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;
 176
 177
 178
 179
 180
 181 (*
 182 W^0_{dart}(x,v,w...)
 183 *)
 184
 185 let w_dart_fan=new_definition`w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3))=
 186 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
 187 else
 188 (if set_of_edge v  V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
 189 else (if set_of_edge v  V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
 190
 191
 192
 193
 194 let if_azims_fan= new_definition`
 195 if_azims_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)
 196     = if i = CARD(set_of_edge v V E)
 197         then &2 * pi
 198          else azim x v u (power_map_points sigma_fan x V E v u i)`;;
 199
 200
 201
 202 (* rcone^0(x,v,h) *)
 203
 204 let rcone_fan = new_definition `rcone_fan  (x:real^3) (v:real^3) (h:real) = {y:real^3 | (y-x) dot (v-x) >(dist(y,x)*dist(v,x)*h)}`;;
 205
 206
 207 (*
 208 W^0_{dart}(x,epsilon)
 209 *)
 210
 211 let rw_dart_fan= new_definition`rw_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3)) (h:real)= w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3)) INTER rcone_fan x v h`;;
 212
 213
 214 (*
 215 azim(x), x dart.
 216 *)
 217
 218
 219 let azim_fan=new_definition`azim_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)
 220 = if (CARD (set_of_edge v V E) > 1) then azim x v w (sigma_fan x V E v w) else &2* pi`;;
 221
 222
 223
 224
 225 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)`;;
 226
 227 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)`;;
 228
 229
 230
 231 end;;