legacy/oldfan/hypermap_of_fan.hl

   1 module Hypermap_of_fan  = struct
   2
   3 open Sphere;;
   4 open Fan_defs;;
   5 open Tactic_fan;;
   6 open Lemma_fan;;
   7 open Hypermap;;
   8 open Fan;;
   9
  10 (* ========================================================================== *)
  11 (*                   DEFINITION OF HYPERMAP OF FAN                    *)
  12 (* ========================================================================== *)
  13
  14
  15
  16 let d1_fan =new_definition`
  17 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)}`;;
  18
  19
  20 let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
  21
  22 let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
  23
  24
  25 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`;;
  26
  27 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)))`;;
  28
  29
  30 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) )`;;
  31
  32 (* This is the same as f_fan,
  33    but easier to use *)
  34
  35 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) )`;;
  36
  37
  38
  39 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))))`;;
  40
  41 (* i_fan corrects the 4th coordinate to be
  42    the dart *)
  43
  44 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)))`;;
  45
  46 let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
  47
  48 let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
  49
  50 let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
  51
  52 let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
  53
  54 (* if f = sigma, the power_map_points gives
  55    iterates of sigma (for fixed x v) *)
  56
  57
  58 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))`;;
  59
  60 (* This is the composition operator (o),
  61    specialized to functions on 4-tuples *)
  62
  63
  64 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))))`;;
  65
  66 (* powers of permutations *)
  67
  68 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))`;;
  69
  70
  71 (* powers of node map *)
  72
  73
  74
  75
  76 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))))`;;
  77
  78
  79 (* the node of a dart, in a special form
  80    for fans *)
  81
  82
  83 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)}`;;
  84
  85
  86 (* The set X(V,E) *)
  87
  88 let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
  89
  90 (* See comment by AS in fan_defs.hl.  The correct definition is there. *)
  91 let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;
  92
  93
  94
  95
  96
  97
  98
  99 let hypermap_of_fanx = new_definition
 100   `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
 101     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
 102           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;
 103
 104
 105 let hypermap1_of_fanx = new_definition
 106   `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
 107     (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
 108           hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;
 109
 110
 111
 112
 113
 114 (*
 115 W^0_{dart}(x,v,w...)
 116 *)
 117
 118 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))=
 119 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
 120 else
 121 (if set_of_edge v  V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
 122 else (if set_of_edge v  V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
 123
 124
 125
 126
 127 (* ========================================================================== *)
 128 (*                   ORBITS NODE FAN                    *)
 129 (* ========================================================================== *)
 130
 131
 132
 133
 134
 135
 136 let image_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 137 FAN(x,V,E)  /\ (u IN set_of_edge v V E)
 138 ==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E`,
 139 INDUCT_TAC THEN
 140 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points]
 141 THENL[
 142 ASM_MESON_TAC[];
 143 REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
 144 THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`] th)) THEN
 145 ASM_REWRITE_TAC[] THEN DISCH_TAC
 146   THEN DISJ_CASES_TAC(SET_RULE `set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i}\/ ~(set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i})`)
 147 THENL[ASM_MESON_TAC[sigma_fan];
 148 ASM_MESON_TAC[SIGMA_FAN]]]);;
 149
 150
 151 let IN2_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 152 FAN(x,V,E)  /\ ({v,u} IN E)
 153 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
 154 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
 155
 156 let IN1_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 157 FAN(x,V,E)  /\ (u IN set_of_edge v V E)
 158 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
 159 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
 160
 161
 162 let remark_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 163 FAN(x,V,E)  /\ ({v,u} IN E)
 164 ==>
 165 power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E
 166 /\ {v,power_map_points sigma_fan x V E v u i} IN E
 167 /\
 168  ~(collinear {x,v,power_map_points sigma_fan x V E v u i})
 169 /\ ~(x = power_map_points (sigma_fan) x V E v u i) /\
 170              ~(v = power_map_points (sigma_fan) x V E v u i) /\
 171              DISJOINT {x, v} {power_map_points (sigma_fan) x V E v u i} /\
 172              ~((power_map_points (sigma_fan) x V E v u i) IN aff {x, v}) /\
 173              DISJOINT {x} {v, (power_map_points (sigma_fan) x V E v u i)} `,
 174 MESON_TAC[IN2_ORBITS_FAN;remark1_fan;image_power_map_points;properties_of_set_of_edge_fan]);;
 175
 176
 177
 178
 179
 180
 181
 182 (* ========================================================================== *)
 183 (*                  PERMUTES OF E_FAN N_FAN F1_FAN         (^_^)            *)
 184 (* ========================================================================== *)
 185
 186
 187
 188 (* Proof Lemma 6.1 [AAUHTVE] *)
 189
 190 let node_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) n:num. power_maps n_fan x V E n=power_n_fan x V E n`,
 191 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[power_maps; n_fan; power_n_fan; power_map_points] THEN INDUCT_TAC THEN REWRITE_TAC[power_maps; power_map_points;i_fan;] THEN REWRITE_TAC[power_map_points; power_maps] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[n_fan;o_funs; pr1; pr2; pr3; pr4]);;
 192
 193
 194
 195
 196
 197 let EQ_PAIR_4=prove(`!a:real^3 b:real^3 c:real^3 d:real^3 a1:real^3 b1:real^3 c1:real^3 d:real^3.
 198 (a,b,c,d)=(a1,b1,c1,d1) <=> a=a1 /\ b=b1 /\ c=c1 /\ d=d1`,
 199 REPEAT GEN_TAC THEN EQ_TAC
 200 THENL[
 201 DISCH_TAC THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr1(a,b,c,d)=pr1(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr1]
 202   THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr2(a,b,c,d)=pr2(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr2] THEN
 203 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr3(a,b,c,d)=pr3(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr3] THEN
 204 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr4(a,b,c,d)=pr4(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr4] THEN ASM_REWRITE_TAC[]
 205   THEN SET_TAC[];
 206 SET_TAC[]]);;
 207
 208
 209
 210 let MONO_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 211 FAN(x,V,E)
 212 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)`,
 213
 214 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;EQ_PAIR_4]
 215   THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> REWRITE_TAC[])
 216   THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
 217   THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3` ]remark1_fan)
 218   THEN ASM_REWRITE_TAC[]
 219   THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w':real^3`;`v:real^3` ]remark1_fan)
 220   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MONO_SIGMA_FAN;]);;
 221
 222
 223 let SUR_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 224 FAN(x,V,E)
 225 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,
 226
 227 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
 228   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`] SUR_SIGMA_FAN)
 229   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 230   THEN EXISTS_TAC`(x:real^3,v:real^3,w':real^3,w:real^3)`
 231   THEN ASM_REWRITE_TAC[n_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3`
 232   THEN EXISTS_TAC`w':real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
 233
 234
 235
 236 let simp_inverse_sigma_fan_alt=prove(`!x V E v w.
 237 inverse_sigma_fan_alt x V E v w= inverse (sigma_fan x V E v) w`,
 238 REWRITE_TAC[inverse] THEN MESON_TAC[inverse_sigma_fan_alt]);;
 239
 240
 241
 242 let SUR_F1_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 243 FAN(x,V,E)
 244 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))`,
 245 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
 246   THEN EXISTS_TAC`(x:real^3,sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w, v:real^3,sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v)`
 247   THEN ASM_REWRITE_TAC[f_fan;EQ_PAIR_4;]
 248  THEN STRIP_TAC
 249 THENL[
 250 EXISTS_TAC`x:real^3` THEN EXISTS_TAC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w`
 251   THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  v w) v`
 252 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ={w:real^3}) \/ ~(set_of_edge v V E ={w})`)
 253 THENL[
 254 REWRITE_TAC[sigma_fan;SET_RULE`{a,b}={b,a}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
 255 THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[])
 256 THEN POP_ASSUM (fun th-> REWRITE_TAC[th]);
 257
 258 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3`]remark1_fan)
 259   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 260 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`]SIGMA_FAN)
 261   THEN ASM_REWRITE_TAC[remark1_fan] THEN STRIP_TAC
 262   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`sigma_fan x V E v w:real^3`;`v:real^3`]remark1_fan)
 263   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 264   THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]];
 265
 266 REWRITE_TAC[f1_fan] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`]INVERSE1_SIGMA_FAN)
 267   THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC  THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th))
 268   THEN ASM_REWRITE_TAC[]]);;
 269
 270
 271
 272
 273
 274 let MONO_F1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 275 FAN(x,V,E)
 276 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)`,
 277 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;EQ_PAIR_4]
 278   THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 279
 280
 281 let MONO_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 282 FAN(x,V,E)
 283 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)`,
 284 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;EQ_PAIR_4]
 285   THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 286
 287
 288 let SUR_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 289 FAN(x,V,E)
 290 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,
 291
 292 REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN REPEAT STRIP_TAC
 293  THEN EXISTS_TAC`(x:real^3,w:real^3,v:real^3, sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v)`
 294 THEN ASM_REWRITE_TAC[e_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3`
 295   THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v`
 296 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]);;
 297
 298
 299
 300
 301
 302
 303 let permuters_of_enf_fan=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 304 FAN(x,V,E)
 305 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)
 306 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))
 307 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)
 308 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))
 309 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)
 310 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))
 311 `,MESON_TAC[MONO_N_FAN;SUR_N_FAN;MONO_F1_FAN;SUR_F1_FAN;MONO_E_FAN;SUR_E_FAN]);;
 312
 313
 314
 315
 316
 317
 318
 319 (* ========================================================================== *)
 320 (*                  PROPERTIES OF E_FAN N_FAN F1_FAN         (^_^)            *)
 321 (* ========================================================================== *)
 322
 323
 324 let condition_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 325 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> e_fan x V E((n_fan x V E) (f1_fan x V E a))=a)`,
 326 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[f1_fan;n_fan; e_fan; EQ_PAIR_4]
 327   THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`]INVERSE1_SIGMA_FAN)
 328   THEN ASM_REWRITE_TAC[]
 329   THEN STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[])
 330   THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`v:real^3`th))
 331   THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]
 332   THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
 333
 334
 335
 336 let plain_hypermap_fan=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 337 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==>
 338 (e_fan x V E)  (e_fan x V E a) =a)`,
 339 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]);;
 340
 341
 342 let e_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 343 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))`,
 344 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]
 345  THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
 346   THEN ASM_MESON_TAC[]);;
 347
 348 let f_fan_no_fix_point=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 349 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))`,
 350 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
 351 THEN ASM_REWRITE_TAC[f1_fan; EQ_PAIR_4]
 352 THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
 353   THEN ASM_MESON_TAC[]);;
 354
 355
 356
 357 (* from hypermap.hl *)
 358
 359 (******************************)
 360 parse_as_infix("POWER",(24,"right"));;
 361
 362 let POWER = new_recursive_definition num_RECURSION
 363  `(!(f:A->A). f POWER 0  = I) /\
 364   (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
 365
 366 let POWER_0 = prove(`!f:A->A. f POWER 0 = I`,
 367  REWRITE_TAC[POWER]);;
 368
 369 let POWER_1 = prove(`!f:A->A. f POWER 1 = f`,
 370  REWRITE_TAC[POWER; ONE; I_O_ID]);;
 371
 372 let POWER_2 = prove(`!f:A->A. f POWER 2 = f o f`,
 373  REWRITE_TAC[POWER; TWO; POWER_1]);;
 374
 375 let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;
 376 (**************************************************)
 377
 378 let POWER_RIGHT=prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
 379 INDUCT_TAC
 380 THENL[REWRITE_TAC[POWER;o_DEF; I_DEF];
 381 REWRITE_TAC[POWER;o_ASSOC] THEN GEN_TAC THEN POP_ASSUM(fun th -> MP_TAC(SPEC`f:A->A`th)) THEN DISCH_TAC
 382  THEN
 383 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;
 384
 385
 386
 387 let power_n_fan=prove(`!l:num x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 w:real^3.
 388 FAN(x,V,E)/\ ({v,w} IN E)==>
 389 (n_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) POWER l) (x,v,w,sigma_fan x V E v w)= (x,v, power_map_points sigma_fan x V E v w l, power_map_points sigma_fan x V E v w (SUC l) )`,
 390 INDUCT_TAC
 391 THENL[REWRITE_TAC[POWER; power_map_points;I_DEF];
 392 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT STRIP_TAC THEN
 393   REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;`(w:real^3)`]th))
 394 THEN ASM_REWRITE_TAC[POWER_RIGHT; o_DEF;]
 395 THEN DISCH_TAC THEN ASM_REWRITE_TAC[n_fan;power_map_points] ]);;
 396
 397
 398
 399 let distinct_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool) .
 400 FAN(x,V,E)==> (!k:num l:num a. a IN d1_fan(x,V,E) ==>
 401 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)`,
 402 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
 403 ASM_REWRITE_TAC[o_DEF;e_fan]  THEN
 404 MP_TAC(ISPECL[`l:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
 405   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 406   THEN MP_TAC(ISPECL[`k:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` w:real^3`;` v:real^3`]power_n_fan)
 407   THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC
 408   THEN POP_ASSUM(fun th-> REWRITE_TAC[])   THEN POP_ASSUM(fun th-> REWRITE_TAC[])
 409   THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th))
 410   THEN ASM_REWRITE_TAC[power_map_points] THEN  POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]));;
 411
 412
 413
 414
 415 let edge_lie_different_nodes=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 416 FAN(x,V,E)==> (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a)) `,
 417
 418 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC  THEN
 419 ASM_REWRITE_TAC[e_fan]  THEN
 420 MP_TAC(ISPECL[`n:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
 421   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4]
 422   THEN STRIP_TAC
 423 THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
 424   THEN ASM_MESON_TAC[]);;
 425
 426
 427
 428
 429 (* ========================================================================== *)
 430 (*             REPRESENTATION OF HYPERMAP OF FAN         (^_^)            *)
 431 (* ========================================================================== *)
 432
 433
 434
 435
 436 let finite_d1_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 437 FAN(x,V,E) ==> FINITE (d1_fan (x,V,E))`,
 438 REPEAT GEN_TAC
 439 THEN DISCH_THEN(LABEL_TAC"EM")
 440 THEN USE_THEN "EM" MP_TAC
 441 THEN REWRITE_TAC[FAN;fan1]
 442 THEN STRIP_TAC
 443 THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 444 THEN MRESA_TAC FINITE_PRODUCT[`V:real^3->bool`;`V:real^3->bool`]
 445 THEN MRESA_TAC FINITE_IMAGE[`(\(a,b:real^3). (x,a,b,sigma_fan x V E a b))`;`{x,y | x IN (V:real^3->bool) /\ y IN V}`]
 446 THEN MATCH_MP_TAC FINITE_SUBSET
 447 THEN EXISTS_TAC`(IMAGE (\(a,b). x,a,b,sigma_fan x V E a b) {x,y | x IN V /\ y IN (V:real^3->bool)})`
 448 THEN ASM_REWRITE_TAC[IMAGE;IN_ELIM_THM;d1_fan;SUBSET]
 449 THEN REPEAT STRIP_TAC
 450 THEN EXISTS_TAC`(v:real^3,w:real^3)`
 451 THEN ASM_REWRITE_TAC[]
 452 THEN EXISTS_TAC`v:real^3`
 453 THEN EXISTS_TAC`w:real^3`
 454 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
 455 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`w:real^3`]
 456 THEN POP_ASSUM MP_TAC
 457 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 458 THEN ASM_REWRITE_TAC[]
 459 THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
 460
 461
 462
 463 let finite_d20_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 464 FAN(x,V,E) ==> FINITE (d20_fan (x,V,E))`,
 465
 466 REPEAT GEN_TAC
 467 THEN DISCH_THEN(LABEL_TAC"EM")
 468 THEN USE_THEN "EM" MP_TAC
 469 THEN REWRITE_TAC[FAN;fan1]
 470 THEN STRIP_TAC
 471 THEN MRESA_TAC FINITE_IMAGE[`(\b:real^3. (x:real^3,b,b,b))`;`V:real^3->bool`]
 472 THEN MATCH_MP_TAC FINITE_SUBSET
 473 THEN EXISTS_TAC`(IMAGE (\b:real^3. (x:real^3,b,b,b))  (V:real^3->bool))`
 474 THEN ASM_REWRITE_TAC[d20_fan;SUBSET;IMAGE;IN_ELIM_THM]
 475 THEN REPEAT STRIP_TAC
 476 THEN EXISTS_TAC`v:real^3`
 477 THEN ASM_REWRITE_TAC[IN]);;
 478
 479
 480
 481 let finite_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 482 FAN(x,V,E)
 483 ==> FINITE (d_fan (x,V,E))`,
 484 REPEAT STRIP_TAC
 485 THEN REWRITE_TAC[d_fan;FINITE_UNION]
 486 THEN STRIP_TAC
 487 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
 488
 489 let subset_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 490 d1_fan (x,V,E) SUBSET d_fan (x,V,E) /\ d20_fan (x,V,E) SUBSET d_fan(x,V,E)`,
 491 REWRITE_TAC[d_fan] THEN SET_TAC[]);;
 492
 493
 494 let FACE_FAN_NOT_EMPTY=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
 495 FAN(x,V,E)
 496 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 497 ==> ~(ds={})`,
 498 REPEAT STRIP_TAC
 499 THEN POP_ASSUM MP_TAC
 500 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
 501 THEN MRESA_TAC FACE_FINITE[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
 502 THEN STRIP_TAC
 503 THEN MRESA1_TAC CARD_EQ_0`face (hypermap1_of_fanx (x:real^3,V,E)) x'`
 504 THEN MRESA_TAC FACE_NOT_EMPTY[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
 505 THEN POP_ASSUM MP_TAC
 506 THEN ARITH_TAC);;
 507
 508
 509
 510
 511
 512
 513
 514 let into_domain_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 515 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 516 ==> (!y. y IN d_fan (x,V,E)==> ((p e_fan ) y) IN (d_fan (x,V,E)))`,
 517 REPEAT STRIP_TAC
 518 THEN ASM_REWRITE_TAC[res;]
 519 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 520 THENL[
 521 ASM_REWRITE_TAC[];
 522
 523 ASM_REWRITE_TAC[]
 524 THEN POP_ASSUM MP_TAC
 525 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
 526 THEN STRIP_TAC
 527 THEN ASM_REWRITE_TAC[]
 528 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 529 THEN MATCH_MP_TAC(SET_RULE`x,w,v,sigma_fan x V E w v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
 530 ==>x,w,v,sigma_fan x V E w v IN  d_fan (x:real^3,V,E)`)
 531 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
 532 THEN EXISTS_TAC`x:real^3`
 533 THEN EXISTS_TAC`w:real^3`
 534 THEN EXISTS_TAC`v:real^3`
 535 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
 536 THEN ASM_REWRITE_TAC[]
 537 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 538 THEN ASM_REWRITE_TAC[]]);;
 539
 540
 541
 542
 543 let into_domain1_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 544 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (e_fan x V E y IN d1_fan (x,V,E)))`,
 545 REPEAT STRIP_TAC
 546 THEN POP_ASSUM MP_TAC
 547 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
 548 THEN STRIP_TAC
 549 THEN ASM_REWRITE_TAC[]
 550 THEN EXISTS_TAC`x:real^3`
 551 THEN EXISTS_TAC`w:real^3`
 552 THEN EXISTS_TAC`v:real^3`
 553 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
 554 THEN ASM_REWRITE_TAC[]
 555 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 556 THEN ASM_REWRITE_TAC[]);;
 557
 558
 559
 560
 561
 562 let e_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 563 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 564 ==> (p e_fan) permutes (d_fan (x,V,E))`,
 565 REPEAT STRIP_TAC
 566 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 567 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (e_fan x V E) (d1_fan (x:real^3,V,E))`]
 568 THEN STRIP_TAC
 569 THENL[
 570 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
 571 THEN REPEAT STRIP_TAC
 572 THEN ASM_REWRITE_TAC[];
 573
 574 MRESA_TAC into_domain_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 575 THEN REPEAT STRIP_TAC
 576 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 577 THENL[EXISTS_TAC`y:real^3#real^3#real^3#real^3`
 578 THEN ASM_REWRITE_TAC[res];
 579 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 580 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
 581 THEN REWRITE_TAC[res]
 582 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
 583 THEN ASM_REWRITE_TAC[]
 584 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 585 THEN ASM_TAC THEN SET_TAC[]]]);;
 586
 587 let into_domain_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 588 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 589 ==> (!y. y IN d_fan (x,V,E)==> ((p f1_fan ) y) IN (d_fan (x,V,E)))`,
 590 REPEAT STRIP_TAC
 591 THEN ASM_REWRITE_TAC[res;]
 592 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 593 THENL[
 594 ASM_REWRITE_TAC[];
 595 ASM_REWRITE_TAC[]
 596 THEN POP_ASSUM MP_TAC
 597 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
 598 THEN STRIP_TAC
 599 THEN ASM_REWRITE_TAC[]
 600 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 601 THEN MATCH_MP_TAC(SET_RULE`x,w,inverse1_sigma_fan x V E w v,v IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
 602 ==>x,w,inverse1_sigma_fan x V E w v,v IN  d_fan (x:real^3,V,E)`)
 603 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
 604 THEN EXISTS_TAC`x:real^3`
 605 THEN EXISTS_TAC`w:real^3`
 606 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
 607 THEN EXISTS_TAC`(v:real^3)`
 608 THEN ASM_REWRITE_TAC[]
 609 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
 610 THEN REMOVE_ASSUM_TAC
 611 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 612 THEN POP_ASSUM MP_TAC
 613 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 614 THEN RESA_TAC
 615 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 616 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 617 THEN POP_ASSUM MP_TAC
 618 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 619 THEN RESA_TAC
 620 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 621 THEN ASM_REWRITE_TAC[]]);;
 622
 623
 624
 625
 626 let into_domain1_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 627 FAN(x,V,E)==> (!y. y IN d1_fan (x,V,E)==> (f1_fan x V E y IN d1_fan (x,V,E)))`,
 628 REPEAT STRIP_TAC
 629 THEN ASM_REWRITE_TAC[]
 630 THEN POP_ASSUM MP_TAC
 631 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
 632 THEN STRIP_TAC
 633 THEN EXISTS_TAC`x:real^3`
 634 THEN EXISTS_TAC`w:real^3`
 635 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
 636 THEN EXISTS_TAC`(v:real^3)`
 637 THEN ASM_REWRITE_TAC[]
 638 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
 639 THEN REMOVE_ASSUM_TAC
 640 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 641 THEN POP_ASSUM MP_TAC
 642 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 643 THEN RESA_TAC
 644 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
 645 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 646 THEN POP_ASSUM MP_TAC
 647 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 648 THEN RESA_TAC
 649 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 650 THEN ASM_REWRITE_TAC[]);;
 651
 652
 653
 654
 655
 656 let f1_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 657 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 658 ==> (p f1_fan) permutes (d_fan (x,V,E))`,
 659
 660 REPEAT STRIP_TAC
 661 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 662 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (f1_fan x V E) (d1_fan (x:real^3,V,E))`]
 663 THEN STRIP_TAC
 664 THENL[
 665 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
 666 THEN REPEAT STRIP_TAC
 667 THEN ASM_REWRITE_TAC[];
 668 MRESA_TAC into_domain_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 669 THEN REPEAT STRIP_TAC
 670 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 671 THENL[
 672 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
 673 THEN ASM_REWRITE_TAC[res];
 674 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 675 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
 676 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
 677 THEN REWRITE_TAC[res]
 678 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
 679 THEN ASM_REWRITE_TAC[]
 680 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 681 THEN ASM_TAC THEN SET_TAC[]]]);;
 682
 683
 684
 685
 686
 687 let into_domain_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 688 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 689 ==> (!y. y IN d_fan (x,V,E)==> ((p n_fan ) y) IN (d_fan (x,V,E)))`,
 690 REPEAT STRIP_TAC
 691 THEN ASM_REWRITE_TAC[res;]
 692 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 693 THENL[
 694 ASM_REWRITE_TAC[];
 695 ASM_REWRITE_TAC[]
 696 THEN POP_ASSUM MP_TAC
 697 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
 698 THEN STRIP_TAC
 699 THEN ASM_REWRITE_TAC[]
 700 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 701 THEN MATCH_MP_TAC(SET_RULE`x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d1_fan (x,V,E) /\ d1_fan (x,V,E)  SUBSET d_fan (x,V,E)
 702 ==>x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN  d_fan (x:real^3,V,E)`)
 703 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
 704 THEN EXISTS_TAC`x:real^3`
 705 THEN EXISTS_TAC`v:real^3`
 706 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
 707 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
 708 THEN ASM_REWRITE_TAC[]
 709 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
 710 THEN POP_ASSUM MP_TAC
 711 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
 712 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]]);;
 713
 714
 715
 716 let into_domain1_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 717 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (n_fan x V E y IN d1_fan (x,V,E)))`,
 718 REPEAT STRIP_TAC
 719 THEN POP_ASSUM MP_TAC
 720 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
 721 THEN STRIP_TAC
 722 THEN ASM_REWRITE_TAC[]
 723 THEN EXISTS_TAC`x:real^3`
 724 THEN EXISTS_TAC`v:real^3`
 725 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
 726 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
 727 THEN ASM_REWRITE_TAC[]
 728 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
 729 THEN POP_ASSUM MP_TAC
 730 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
 731 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]);;
 732
 733
 734
 735 let n_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 736 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 737 ==> (p n_fan) permutes (d_fan (x,V,E))`,
 738
 739 REPEAT STRIP_TAC
 740 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 741 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (n_fan x V E) (d1_fan (x:real^3,V,E))`]
 742 THEN STRIP_TAC
 743 THENL[
 744 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
 745 THEN REPEAT STRIP_TAC
 746 THEN ASM_REWRITE_TAC[];
 747 MRESA_TAC into_domain_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 748 THEN REPEAT STRIP_TAC
 749 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
 750 THENL[
 751 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
 752 THEN ASM_REWRITE_TAC[res];
 753 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 754 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
 755 THEN POP_ASSUM  (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
 756 THEN REWRITE_TAC[res]
 757 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
 758 THEN ASM_REWRITE_TAC[]
 759 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 760 THEN ASM_TAC THEN SET_TAC[]]]);;
 761
 762
 763 let id_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3.
 764 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
 765 ==> (p e_fan) y=y /\ (p n_fan) y=y/\ (p f1_fan) y=y`,
 766 REPEAT STRIP_TAC
 767 THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
 768
 769 let id_power_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3 n:num p.
 770 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
 771 ==> ((p e_fan) POWER n) y=y /\ ((p n_fan) POWER n)y=y/\ ((p f1_fan) POWER n) y=y`,
 772 (let lem=prove(`!f:A->A x:A. f x = x ==> !m. (f POWER m) x = x`,
 773 MRESA_TAC power_map_fix_point[`1:num`]
 774 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[POWER_1;ARITH_RULE`m*1=m:num`]) in
 775 REPEAT STRIP_TAC
 776 THEN MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`y:real^3#real^3#real^3#real^3`]
 777 THEN MRESA_TAC lem[`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
 778 THEN MRESA_TAC lem[`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
 779 THEN MRESA_TAC lem[`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]));;
 780
 781
 782
 783
 784 let into_domain_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 785 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 786 ==> (!y. y IN d1_fan (x,V,E)==> (p e_fan ) y = e_fan x V E y)
 787 /\ (!y. y IN d1_fan (x,V,E)==> (p n_fan ) y = n_fan x V E y)
 788 /\(!y. y IN d1_fan (x,V,E)==> (p f1_fan ) y = f1_fan x V E y)
 789 `,
 790 REPEAT STRIP_TAC
 791 THEN ASM_REWRITE_TAC[res;]);;
 792
 793
 794
 795
 796 let power_map_fix_set = prove(`!n f:A->A g:A->A s:A->bool. (!x:A. x IN s ==>  f x= g x) /\ (!x:A. x IN s ==> g x IN s) ==> (!x. x IN s==>(f POWER n) x = (g POWER n) x)`,
 797  INDUCT_TAC THENL[REWRITE_TAC[MULT; POWER; I_THM];
 798     REWRITE_TAC[POWER; o_DEF] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
 799 THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
 800 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_THEN(LABEL_TAC"NHO")  THEN DISCH_TAC
 801 THEN REMOVE_THEN "YEU" (fun th -> MRESA_TAC th[`f:A->A`;`g:A->A`;`s:A->bool`])
 802 THEN POP_ASSUM (fun th-> MRESA1_TAC th `g (x:A):A`)
 803 THEN POP_ASSUM MP_TAC
 804 THEN REMOVE_THEN "EM"  (fun th -> MRESA1_TAC th `x:A`)
 805 THEN REMOVE_THEN "NHO"  (fun th -> MRESA1_TAC th `x:A`)]);;
 806
 807
 808
 809
 810
 811
 812 let into_domain_power_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num p.
 813 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
 814 ==> (!y. y IN d1_fan (x,V,E)==> ((p e_fan ) POWER n)y = ((e_fan x V E) POWER n) y)
 815 /\ (!y. y IN d1_fan (x,V,E)==> ((p n_fan ) POWER n) y = ((n_fan x V E) POWER n) y)
 816 /\(!y. y IN d1_fan (x,V,E)==> ((p f1_fan ) POWER n) y = ((f1_fan x V E) POWER n) y)`,
 817 REPEAT GEN_TAC THEN REPEAT DISCH_TAC
 818 THEN MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 819 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 820 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 821 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 822 THEN MRESA_TAC power_map_fix_set[`n:num`;
 823 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
 824 `(e_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
 825 THEN MRESA_TAC power_map_fix_set[`n:num`;
 826 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
 827 `(n_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
 828 THEN MRESA_TAC power_map_fix_set[`n:num`;
 829 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
 830 `(f1_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]);;
 831
 832
 833
 834
 835 let power_fun_in_domain=prove(`!n f:A->A s:A->bool.(!y. y IN s==> f y IN s)==> (!y. y IN s==> (f POWER n) y IN s)`,
 836  INDUCT_TAC THENL[REWRITE_TAC[POWER_0; I_THM];
 837 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
 838 THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`f:A->A`;`s:A->bool`])
 839 THEN REWRITE_TAC[COM_POWER;o_DEF]
 840 THEN POP_ASSUM  (fun th-> MRESA1_TAC th`y:A`)]);;
 841
 842
 843
 844 let into_domain1_power_efn_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num.
 845 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (((e_fan x V E) POWER n) y IN d1_fan (x,V,E)))
 846 /\ (!y. y IN d1_fan (x,V,E)==> (((n_fan x V E) POWER n) y IN d1_fan (x,V,E)))
 847 /\(!y. y IN d1_fan (x,V,E)==> (((f1_fan x V E) POWER n) y IN d1_fan (x,V,E)))`,
 848 REPEAT GEN_TAC THEN DISCH_TAC
 849 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
 850 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
 851 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
 852 THEN MRESA_TAC power_fun_in_domain[`n:num`;`e_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
 853 THEN MRESA_TAC power_fun_in_domain[`n:num`;`f1_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
 854 THEN MRESA_TAC power_fun_in_domain[`n:num`;`n_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]);;
 855
 856
 857
 858
 859
 860
 861 let lemma_hypermap1_of_fanx=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
 862 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
 863 (p e_fan) o (p n_fan) o (p f1_fan)= I`,
 864 REPEAT STRIP_TAC
 865 THEN MATCH_MP_TAC EQ_EXT
 866 THEN ASM_REWRITE_TAC[I_THM;o_DEF]
 867 THEN GEN_TAC
 868 THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
 869 THENL[
 870 MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x':real^3#real^3#real^3#real^3`];
 871 MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 872 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
 873 THEN REMOVE_ASSUM_TAC
 874 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
 875 THEN POP_ASSUM MP_TAC
 876 THEN POP_ASSUM MP_TAC
 877 THEN DISCH_THEN (LABEL_TAC"YEU")
 878 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 879 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
 880 THEN RESA_TAC
 881 THEN REMOVE_ASSUM_TAC
 882 THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `(n_fan x V E (f1_fan x V E x')):real^3#real^3#real^3#real^3` )
 883 THEN POP_ASSUM MP_TAC
 884 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 885 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
 886 THEN RESA_TAC
 887 THEN MRESA_TAC condition_hypermap_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
 888 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )]);;
 889
 890
 891
 892
 893
 894
 895
 896
 897
 898 let hypermap_of_fan_rep=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) p.
 899 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) )  ==>
 900 dart ( hypermap1_of_fanx (x,V,E)) =d_fan (x,V,E)  /\ edge_map (hypermap1_of_fanx (x,V,E)) = p e_fan  /\ node_map (hypermap1_of_fanx (x,V,E)) = p n_fan /\ face_map (hypermap1_of_fanx (x,V,E)) = p f1_fan `,
 901 REPEAT GEN_TAC THEN DISCH_TAC
 902 THEN REWRITE_TAC[hypermap1_of_fanx]
 903 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
 904 THEN ASM_REWRITE_TAC[]
 905 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
 906 THEN MRESA_TAC e_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
 907 THEN MRESA_TAC n_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
 908 THEN MRESA_TAC f1_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
 909 THEN MRESA_TAC lemma_hypermap1_of_fanx[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
 910 THEN MRESA_TAC lemma_hypermap_rep[`d_fan (x:real^3,V,E):real^3#real^3#real^3#real^3->bool`;
 911 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
 912 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
 913 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`]);;
 914
 915 let properties_of_f1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y y1.
 916 FAN(x,V,E) /\ y = f1_fan x V E y1 /\ y1 IN d1_fan (x,V,E)
 917 ==> pr3 y1 =pr2 y /\ {pr2 y1, pr3 y1} IN E /\ {pr2 y, pr3 y} IN E /\
 918 pr2 y1= sigma_fan x V E (pr2 y) (pr3 y)`,
 919 REPEAT GEN_TAC
 920 THEN STRIP_TAC
 921 THEN POP_ASSUM MP_TAC
 922 THEN REWRITE_TAC[d1_fan; IN_ELIM_THM]
 923 THEN STRIP_TAC
 924 THEN ASM_REWRITE_TAC[pr2;pr3;f1_fan]
 925 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`w:real^3`]
 926 THEN REMOVE_ASSUM_TAC
 927 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 928 THEN POP_ASSUM MP_TAC
 929 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 930 THEN RESA_TAC
 931 THEN REMOVE_ASSUM_TAC
 932 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
 933 THEN POP_ASSUM MP_TAC
 934 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 935 THEN RESA_TAC
 936 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 937 THEN ASM_REWRITE_TAC[]);;
 938
 939
 940
 941 (* ========================================================================== *)
 942 (*                 PROPERTIES OF HYPERMAP OF FAN          (^_^)            *)
 943 (* ========================================================================== *)
 944
 945
 946
 947 let face_subset_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
 948 FAN(x,V,E)
 949 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 950 ==> ds SUBSET d_fan (x,V,E)`,
 951 REPEAT GEN_TAC THEN STRIP_TAC
 952 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
 953 THEN MRESA_TAC hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
 954 THEN MRESA_TAC lemma_face_subset[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]);;
 955
 956
 957
 958
 959 let properties_of_elements_in_face_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
 960 FAN(x,V,E)
 961 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 962 /\ y IN ds
 963 ==> {pr2 y, pr3 y} IN E\/ pr2 y= pr3 y`,
 964 REPEAT GEN_TAC THEN STRIP_TAC
 965 THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
 966 THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
 967 THEN RESA_TAC
 968 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM]
 969 THEN STRIP_TAC
 970 THEN ASM_REWRITE_TAC[pr2;pr3]);;
 971
 972 let fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
 973 FAN(x,V,E)
 974 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 975 ==> d20_fan(x,V,E)={}`,
 976 REPEAT STRIP_TAC
 977 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
 978 THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`]
 979 THEN REWRITE_TAC[d20_fan;IN_ELIM_THM]
 980 THEN STRIP_TAC
 981 THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES])
 982 THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
 983
 984
 985
 986
 987
 988 let AAUHTVE=prove(`!x:real^3  (V:real^3->bool) (E:(real^3->bool)->bool).
 989 FAN(x,V,E)/\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==>
 990 FINITE (d_fan (x,V,E))
 991 /\ (p e_fan) permutes (d_fan (x,V,E))
 992 /\ (p n_fan) permutes (d_fan (x,V,E))
 993 /\ (p f1_fan) permutes (d_fan (x,V,E))
 994 /\(p e_fan) o (p n_fan) o (p f1_fan)= I
 995 /\ (!a. a IN d1_fan(x,V,E)==> (e_fan x V E)  (e_fan x V E a) =a)
 996 /\ (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))
 997 /\ (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))
 998 /\ (!k:num l:num a. a IN d1_fan(x,V,E) ==>
 999 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)
1000
1001 /\ (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a))`,
1002
1003 MESON_TAC[lemma_hypermap1_of_fanx;e_fan_permutes;n_fan_permutes;finite_d_fan;f1_fan_permutes;plain_hypermap_fan;e_fan_no_fix_point;f_fan_no_fix_point;distinct_nodes;edge_lie_different_nodes]);;
1004
1005 (********************************)
1006
1007
1008
1009
1010 end;;