legacy/oldfan/node_fan.hl

   1
   2 module Node_fan  = struct
   3
   4
   5 open Sphere;;
   6 open Fan_defs;;
   7 open Tactic_fan;;
   8 open Lemma_fan;;
   9 open Fan;;
  10 open Hypermap_of_fan;;
  11
  12
  13
  14 (* ========================================================================== *)
  15 (*                   NODE OF HYPERMAP OF FAN          (^_^)                 *)
  16 (* ========================================================================== *)
  17
  18
  19
  20 let CARD_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
  21 FAN(x,V,E) ==>
  22 CARD( IMAGE (sigma_fan x V E v) (set_of_edge v V E))= CARD(set_of_edge v V E)
  23 `,
  24
  25 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN STRIP_TAC
  26 THENL[
  27 REPEAT GEN_TAC THEN STRIP_TAC THEN
  28 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`x':real^3`]properties_of_set_of_edge_fan)
  29   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  30 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`y:real^3`]properties_of_set_of_edge_fan)
  31   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  32 ASM_MESON_TAC[MONO_SIGMA_FAN];
  33 POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN MESON_TAC[remark_finite_fan1]]);;
  34
  35 let MONO_AZIM_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
  36 FAN(x,V,E) /\ ({v,u} IN E)
  37 /\ ({v,w} IN E) /\ ~(sigma_fan x V E v w =u)
  38 ==> (azim x v u w <= azim x v u (sigma_fan x V E v w))`,
  39
  40 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1")
  41 THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6]
  42 THEN REPEAT STRIP_TAC
  43 THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN
  44 DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b")
  45   THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  46 THEN DISJ_CASES_TAC(SET_RULE`({(w:real^3)}=set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) \/ ~({(w:real^3)}=set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`)
  47 THENL(*1*)[
  48 ASM_REWRITE_TAC[sigma_fan] THEN REAL_ARITH_TAC;(*1*)
  49
  50 DISJ_CASES_TAC(SET_RULE`((u:real^3)=(w:real^3))\/ ~(u=w)`)
  51 THENL (*2*)[
  52
  53 ASM_REWRITE_TAC[AZIM_REFL] THEN MESON_TAC[azim];(*2*)
  54
  55 DISJ_CASES_TAC(SET_RULE`(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) <= azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) ) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) <= azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) )`)
  56   THENL (*3*)[
  57 ASM_REWRITE_TAC[];(*3*)
  58
  59 SUBGOAL_THEN`azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))
  60 <= azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) ` ASSUME_TAC
  61 THENL(*4*)[
  62 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
  63
  64 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
  65   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  66 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
  67   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  68   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
  69 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  70   THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "c") THEN
  71  SUBGOAL_THEN `{(u:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(w:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC
  72 THENL(*5*)[
  73 ASM_TAC THEN SET_TAC[];(*5*)
  74
  75 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
  76 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  77   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(u:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(w:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
  78                 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  79   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (w:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  80 THEN  SUBGOAL_THEN `azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (w:real^3)<= azim x v u w` ASSUME_TAC
  81
  82 THENL(*6*)[
  83 MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`]azim) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
  84
  85 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[])THEN  ASM_REWRITE_TAC[] THEN
  86 MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge)
  87 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
  88  THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  89   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  90   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))}`th) THEN ASSUME_TAC(th))
  91   THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
  92 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
  93   THEN
  94   DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
  95 THENL(*7*)[
  96 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN)
  97 THEN ASM_TAC THEN SET_TAC[];(*7*)
  98
  99 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (u:real^3) = &0)`)
 100
 101 THENL(*8*)[
 102 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
 103 THEN ASM_TAC THEN SET_TAC[];(*8*)
 104
 105 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`w:real^3`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]AZIM_COMPL)
 106 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 107 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL)
 108   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - a<= &2 * pi - (b:real) <=> b<= (a:real)`]
 109   THEN REMOVE_THEN "c" (fun th -> MP_TAC(ISPEC `u:real^3` th) ) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN STRIP_TAC
 110   THEN SUBGOAL_THEN `azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = azim x v  w u` ASSUME_TAC
 111
 112 THENL(*9*)[
 113 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN  REAL_ARITH_TAC;(*9*)
 114
 115 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;`u:real^3`]UNIQUE_AZIM_POINT_FAN)
 116   THEN ASM_REWRITE_TAC[]]]]]]]]]]);;
 117
 118
 119
 120
 121 let MONO_POWER_SIGMA_FAN=prove(`!(i:num) (j:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 122 FAN(x,V,E) /\ ({v,u} IN E)/\(j<i)/\
 123  (power_map_points sigma_fan x V E v u i)= (power_map_points sigma_fan x V E v u j)
 124 ==> u=power_map_points sigma_fan x V E v u (i-j)`,
 125 INDUCT_TAC THENL
 126 [ARITH_TAC;
 127
 128 INDUCT_TAC THENL
 129 [REWRITE_TAC[ARITH_RULE `SUC i- 0 =SUC (i:num)`;power_map_points] THEN ASM_TAC THEN SET_TAC[];
 130
 131 REWRITE_TAC[ARITH_RULE `SUC (i:num)-SUC (j:num)= i - j`; ARITH_RULE `SUC(j:num) < SUC (i) <=> j < i`;power_map_points]
 132   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC
 133   THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 134    MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]properties_of_set_of_edge_fan)
 135   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 136   THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
 137   THEN DISCH_TAC
 138   THEN MP_TAC(ISPECL[`(j:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
 139   THEN DISCH_TAC
 140   THEN  MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`]properties_of_set_of_edge_fan)
 141   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 142   THEN  MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (j:num)`]properties_of_set_of_edge_fan)
 143   THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 144   THEN MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (j:num)`]MONO_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
 145   THEN DISCH_TAC
 146   THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPECL[`(j:num) `;`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]th))
 147   THEN ASM_REWRITE_TAC[]]]);;
 148
 149
 150
 151
 152
 153
 154 let MONO_POWER_MAP_POINTS1_FAN=prove(`!(i:num)  (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 155 FAN(x,V,E) /\ (u IN set_of_edge v V E) /\ ~(set_of_edge v V E={u})
 156 ==> ~(power_map_points (sigma_fan) x V E v u i=power_map_points (sigma_fan) x V E v u (SUC i))
 157 `,
 158 INDUCT_TAC THENL[
 159 REWRITE_TAC[power_map_points] THEN REPEAT GEN_TAC THEN STRIP_TAC
 160 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN) THEN ASM_MESON_TAC[];
 161 REPEAT GEN_TAC THEN POP_ASSUM
 162  (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 REWRITE_TAC[power_map_points]
 163   THEN STRIP_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
 164 THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b")
 165 THEN USE_THEN "b" MP_TAC THEN REWRITE_TAC[FAN]
 166 THEN STRIP_TAC
 167 THEN  DISCH_TAC THEN DISCH_TAC
 168 THEN REMOVE_THEN "a" MP_TAC THEN MP_TAC(ARITH_RULE `SUC (i:num)< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> i < CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`)
 169 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 170 THEN MATCH_MP_TAC MONO_NOT THEN DISCH_TAC
 171   THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
 172   THEN DISCH_TAC
 173 THEN MP_TAC(ISPECL[`SUC (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
 174   THEN DISCH_TAC
 175   THEN MP_TAC(ISPECL[` (v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`] properties_of_set_of_edge)
 176   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 177 THEN MP_TAC(ISPECL[` (v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (SUC (i:num)))`] properties_of_set_of_edge)
 178   THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
 179   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`]MONO_SIGMA_FAN)
 180 THEN ASM_MESON_TAC[]]);;
 181
 182
 183
 184
 185
 186
 187
 188
 189
 190 let set_of_orbits_points_fan = new_definition `set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = {power_map_points sigma_fan x V E v u i| 0<=i }`;;
 191
 192 let number_of_orbits_fan = new_definition `number_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;;
 193
 194
 195
 196 let addition_sigma_fan = prove(`!(m:num) (n:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 197 power_map_points sigma_fan x V E v u (m + n) = (power_map_points sigma_fan x V E v (power_map_points sigma_fan x V E v u  n) m)  `,
 198 INDUCT_TAC
 199 THENL [
 200 REWRITE_TAC[power_map_points; ARITH_RULE`0 + n:num =n`];
 201 REWRITE_TAC[ARITH_RULE` SUC (m:num) + n= SUC(m+n)`; power_map_points] THEN REPEAT GEN_TAC
 202   THEN POP_ASSUM(ASSUME_TAC o GSYM o (ISPECL[`(n:num) `;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]))
 203                    THEN ASM_TAC THEN SET_TAC[]]);;
 204
 205
 206
 207
 208
 209
 210 let fix_point_sigma_fan=prove(`! (q:num) (i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 211 (power_map_points (sigma_fan) x V E v u i=u)
 212 ==>power_map_points sigma_fan x V E v u (q * i)=u
 213 `,
 214 INDUCT_TAC THENL[
 215 ASM_REWRITE_TAC[ARITH_RULE`0 * i:num = 0`;power_map_points];
 216 REWRITE_TAC[ARITH_RULE`SUC q * i:num= q * i + i`] THEN REPEAT GEN_TAC THEN
 217  POP_ASSUM(MP_TAC  o (ISPECL[`(i:num) `;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]))
 218   THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[addition_sigma_fan]]);;
 219
 220 let i_IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num).
 221  power_map_points (sigma_fan) x V E v u i IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
 222 REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN EXISTS_TAC`i:num` THEN REWRITE_TAC[power_map_points] THEN SIMP_TAC[] THEN ARITH_TAC);;
 223
 224 let u_IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 225  u IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
 226 REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN EXISTS_TAC`0` THEN REWRITE_TAC[power_map_points] THEN SIMP_TAC[] THEN ARITH_TAC);;
 227
 228
 229 let IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
 230  w IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
 231 ==> sigma_fan x V E v w IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
 232
 233 REPEAT GEN_TAC THEN REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`SUC i` THEN ASM_REWRITE_TAC[power_map_points] THEN ARITH_TAC);;
 234
 235
 236 let ORBITS_SUBSET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 237 FAN(x,V,E) /\ ({v,u} IN E)
 238 ==> set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
 239 SUBSET set_of_edge v V E`,
 240 REPEAT GEN_TAC THEN STRIP_TAC
 241   THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]properties_of_set_of_edge_fan)
 242 THEN  ASM_REWRITE_TAC[set_of_orbits_points_fan;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN GEN_TAC THEN STRIP_TAC
 243 THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]);;
 244
 245
 246 let CARD_ORBITS_EDGE_FAN_LE=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 247 FAN(x,V,E) /\ ({v,u} IN E)
 248 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) )
 249 <=CARD( set_of_edge v V E)`,
 250 REPEAT GEN_TAC THEN STRIP_TAC
 251   THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]ORBITS_SUBSET_EDGE_FAN)
 252   THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC)
 253 THEN REWRITE_TAC[FAN;fan1] THEN REPEAT STRIP_TAC
 254   THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`] remark_finite_fan1)
 255 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]CARD_SUBSET)
 256   THEN ASM_REWRITE_TAC[]);;
 257
 258
 259
 260
 261 let FINITE_ORBITS_SIGMA_FAN=prove( `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 262 FAN(x,V,E) /\ ({v,u} IN E)
 263 ==> FINITE(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) `,
 264
 265 REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`] ORBITS_SUBSET_EDGE_FAN)THEN ASM_REWRITE_TAC[]
 266   THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC
 267   THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`] remark_finite_fan1)
 268   THEN ASM_REWRITE_TAC[] THEN MESON_TAC[FINITE_SUBSET]);;
 269
 270
 271
 272 let ORBITS_SIGMA_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 273 FAN(x,V,E) /\ ({v,u} IN E)/\
 274 (power_map_points (sigma_fan) x V E v u i=u) /\ ~(i=0)
 275 ==> set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) =
 276 {power_map_points sigma_fan x V E v u j| j < i }
 277 `,
 278 REPEAT STRIP_TAC THEN REWRITE_TAC[set_of_orbits_points_fan; EXTENSION; IN_ELIM_THM]
 279 THEN GEN_TAC THEN EQ_TAC
 280 THENL [
 281 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 282 FIND_ASSUM (MP_TAC o (SPEC `i':num`) o MATCH_MP DIVMOD_EXIST) `~(i:num = 0)`
 283  THEN REPEAT STRIP_TAC
 284   THEN EXISTS_TAC`r:num` THEN ASM_REWRITE_TAC[ARITH_RULE`q * (i:num) + r = r+ q * i`;addition_sigma_fan]
 285   THEN MP_TAC  (SPECL [`(q:num)`;` (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`]fix_point_sigma_fan) THEN ASM_REWRITE_TAC[]
 286   THEN DISCH_TAC THEN ASM_REWRITE_TAC[];
 287
 288 STRIP_TAC THEN EXISTS_TAC `j:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC]);;
 289
 290 (***********lemmas in hypermap.ml***************)
 291
 292
 293 let IMAGE_SEG = prove(`!(n:num) (f:num->A). IMAGE f {i:num | i < n:num}  = {f (i:num) | i < n}`,
 294    REPEAT STRIP_TAC
 295    THEN REWRITE_TAC[IMAGE; IN_ELIM_THM] THEN ASM_SET_TAC[]);;
 296
 297 let FINITE_SERIES = prove(`!(n:num) (f:num->A). FINITE {f(i) | i < n}`,
 298    REPEAT GEN_TAC
 299    THEN ONCE_REWRITE_TAC[SYM(SPECL[`n:num`; `f:num->A`] IMAGE_SEG)]
 300    THEN MATCH_MP_TAC FINITE_IMAGE
 301    THEN REWRITE_TAC[FINITE_NUMSEG_LT]);;
 302
 303 let CARD_FINITE_SERIES_LE  = prove(`!(n:num) (f:num->A). CARD {f(i) | i < n} <= n`,
 304    REPEAT GEN_TAC
 305    THEN ONCE_REWRITE_TAC[SYM(SPECL[`n:num`; `f:num->A`] IMAGE_SEG)]
 306    THEN MP_TAC(ISPEC `f:num ->A` (MATCH_MP CARD_IMAGE_LE (SPEC `n:num` FINITE_NUMSEG_LT)))
 307    THEN REWRITE_TAC[CARD_NUMSEG_LT]);;
 308
 309 let LEMMA_INJ = prove(`!(n:num) (f:num->A).(!i:num j:num. i < n /\ j < i ==> ~(f i = f j)) ==> (!i:num j:num. i < n /\ j < n /\ f i = f j ==> i = j)`,
 310    REPEAT GEN_TAC
 311    THEN DISCH_TAC THEN MATCH_MP_TAC WLOG_LT
 312    THEN STRIP_TAC THENL[ARITH_TAC; ALL_TAC]
 313    THEN STRIP_TAC THENL[MESON_TAC[]; ALL_TAC]
 314    THEN ASM_MESON_TAC[]);;
 315
 316 let CARD_FINITE_SERIES_EQ  = prove(`!(n:num) (f:num->A). (!i:num j:num. i < n /\  j < i ==> ~(f i = f j)) ==> CARD {f(i) | i < n} = n`,
 317    REPEAT GEN_TAC
 318    THEN DISCH_THEN (LABEL_TAC "F1" o MATCH_MP LEMMA_INJ)
 319    THEN ONCE_REWRITE_TAC[GSYM IMAGE_SEG]
 320    THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV) [GSYM (SPEC `n:num` CARD_NUMSEG_LT)]
 321    THEN MATCH_MP_TAC CARD_IMAGE_INJ
 322    THEN REWRITE_TAC[FINITE_NUMSEG_LT]
 323    THEN REWRITE_TAC[IN_ELIM_THM]
 324    THEN ASM_REWRITE_TAC[]);;
 325
 326
 327
 328 (**************************************)
 329
 330
 331 let CARD_ORBITS_SIGMA_FAN_LE=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 332 FAN(x,V,E) /\ ({v,u} IN E)/\
 333 (power_map_points (sigma_fan) x V E v u i=u) /\ ~(i=0)
 334 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))<=i`,
 335
 336 REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 337 THEN MP_TAC(ISPECL[`i:num`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_LE) THEN ASM_TAC THEN SET_TAC[]);;
 338
 339
 340
 341
 342 let exists_inverse_in_orbits_sigma_fan=prove(`
 343 !(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (y:real^3).
 344  FAN(x,V,E) /\({v,u} IN E)/\ ~(y IN set_of_orbits_points_fan x V E v u)
 345 ==>
 346 (?(w:real^3). (w IN (set_of_orbits_points_fan x V E v u)) /\ ~(w=y) /\
 347 (!(w1:real^3). (w1 IN (set_of_orbits_points_fan x V E v u))/\ ~(w1=y) ==> azim1 x v y w <=  azim1 x v y w1))
 348 `,
 349
 350 (let lemma = prove
 351    (`!X:real->bool.
 352           FINITE X /\ ~(X = {})
 353           ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
 354     MESON_TAC[INF_FINITE]) in
 355
 356 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC
 357 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "ba")
 358 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan)
 359 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
 360 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 361 THEN
 362 SUBGOAL_THEN `FINITE ((set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) (v:real^3) (u:real^3) DELETE  (y:real^3))` ASSUME_TAC
 363 THENL[(*1*)
 364
 365 ASM_MESON_TAC[FINITE_DELETE_IMP];(*1*)
 366 DISJ_CASES_TAC(SET_RULE`(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE  (y:real^3)={})\/
 367  ~(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE  (y:real^3)={})`)
 368 THENL(*2*)[
 369 MP_TAC (ISPECL[`y:real^3`;`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]DELETE_NON_ELEMENT)
 370   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 371   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]u_IN_ORBITS_FAN)
 372   THEN ASM_TAC THEN SET_TAC[];(*2*)
 373 SUBGOAL_THEN`~(IMAGE ( azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE  (y:real^3))={})` ASSUME_TAC
 374 THENL(*3*)[
 375 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*3*)
 376
 377 SUBGOAL_THEN` FINITE (IMAGE (azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE  (y:real^3)))` ASSUME_TAC
 378 THENL(*4*)[
 379 ASM_MESON_TAC[FINITE_IMAGE];(*4*)
 380
 381 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE  (y:real^3)))` th))
 382  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
 383 THEN EXISTS_TAC`x':real^3`
 384   THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]]]]));;
 385
 386
 387
 388
 389
 390
 391
 392
 393 let key_lemma_cyclic_fan=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 394 FAN(x,V,E) /\ (0 < i) /\(i< CARD(set_of_edge v V E)) /\ ({v,u} IN E)
 395 ==> ~(power_map_points (sigma_fan) x V E v u i=u)
 396 `,
 397 INDUCT_TAC
 398 THENL(*1*)[ARITH_TAC;(*1*)
 399 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points] THEN
 400 MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]ORBITS_SUBSET_EDGE_FAN)
 401   THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 402   THEN DISJ_CASES_TAC(SET_RULE`(sigma_fan x V E v (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))= u)\/ ~(sigma_fan x V E v (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))= u)`)
 403 THENL(*2*)[
 404 ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`SUC (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_ORBITS_SIGMA_FAN_LE)
 405  THEN ASM_REWRITE_TAC[power_map_points; ARITH_RULE`~(SUC i = 0)`] THEN STRIP_TAC
 406   THEN SUBGOAL_THEN `CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) <CARD(set_of_edge v V E)` ASSUME_TAC
 407 THENL(*3*)[
 408 REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC;(*3*)
 409
 410 SUBGOAL_THEN `set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) PSUBSET set_of_edge v V E` ASSUME_TAC
 411 THENL(*4*)[
 412 ASM_REWRITE_TAC[PSUBSET] THEN DISJ_CASES_TAC(SET_RULE`(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = set_of_edge v V E)\/ ~(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = set_of_edge v V E)`)
 413 THENL(*5*)[
 414 SUBGOAL_THEN`CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) =CARD( set_of_edge v V E)`ASSUME_TAC
 415 THENL(*6*)[
 416 POP_ASSUM(fun th->REWRITE_TAC[th]);(*6*)
 417 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC](*6*);(*5*)
 418
 419 POP_ASSUM(fun th->REWRITE_TAC[th])](*5*);(*4*)
 420
 421
 422 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSUBSET_MEMBER] THEN STRIP_TAC
 423   THEN MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`y:real^3`]
 424 exists_inverse_in_orbits_sigma_fan)
 425   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)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`)
 426 THENL(*5*)[
 427 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
 428   THEN DISCH_THEN(LABEL_TAC "b") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN DISCH_TAC
 429   THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[u_IN_ORBITS_FAN];(*5*)
 430
 431 ASM_REWRITE_TAC[] THEN STRIP_TAC
 432 THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
 433 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:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})`)
 434 THENL(*6*)[
 435
 436 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
 437   THEN DISCH_THEN(LABEL_TAC "b") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN DISCH_TAC
 438   THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[];(*6*)
 439
 440 MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`u:real^3`;` (w:real^3)`]IN_ORBITS_FAN)
 441   THEN ASM_REWRITE_TAC[]
 442   THEN STRIP_TAC THEN STRIP_TAC
 443 THEN POP_ASSUM(fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)` th))
 444   THEN ASM_REWRITE_TAC[]
 445   THEN DISJ_CASES_TAC(SET_RULE`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)=(y:real^3) \/ ~(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)=(y:real^3))`)
 446 THENL(*7*)[
 447 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
 448   THEN ASM_REWRITE_TAC[];(*7*)
 449
 450 ASM_REWRITE_TAC[azim1;REAL_ARITH` (a:real) - b <= a - c <=> c<=b`] THEN STRIP_TAC
 451 THEN
 452 SUBGOAL_THEN `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) IN set_of_edge v V E` ASSUME_TAC
 453 THENL(*8*)[
 454  ASM_TAC THEN SET_TAC[];(*8*)
 455
 456 SUBGOAL_THEN `(w:real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ASSUME_TAC
 457 THENL(*9*)[
 458  ASM_TAC THEN SET_TAC[];(*9*)
 459
 460 SUBGOAL_THEN `{(y:real^3),sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3),(w:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
 461
 462 THENL(*10*)[
 463  ASM_TAC THEN SET_TAC[];(*10*)
 464
 465 FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN
 466 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 467 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
 468 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 469   THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(y:real^3),sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3),(w:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
 470                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 471 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`y:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`;`w:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[]
 472   THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`y:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`]azim)
 473 THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (w:real^3) <= azim (x:real^3) (v:real^3) (y:real^3) (w:real^3)`
 474 ASSUME_TAC
 475 THENL(*11*)[
 476 REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*11*)
 477
 478 POP_ASSUM MP_TAC THEN POP_ASSUM(fun th ->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[]  THEN
 479 MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (y:real^3)`]properties_of_set_of_edge_fan)
 480 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
 481   THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan)
 482 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
 483   THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge_fan)
 484 THEN  ASM_REWRITE_TAC[] THEN DISCH_TAC
 485 THEN
 486 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (y:real^3)= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (y:real^3) = &0)`)
 487 THENL(*12*)[
 488 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(y:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
 489 THEN ASM_REWRITE_TAC[];(*12*)
 490
 491 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3)  (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
 492 THENL(*13*)[
 493 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`; ` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ]UNIQUE_AZIM_0_POINT_FAN)
 494   THEN ASM_REWRITE_TAC[]
 495   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`] SIGMA_FAN)
 496   THEN ASM_REWRITE_TAC[] THEN  ASM_TAC THEN SET_TAC[];(*13*)
 497
 498  REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
 499   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(y:real^3)}`th) THEN ASSUME_TAC(th))
 500   THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))}`th) THEN ASSUME_TAC(th))
 501   THEN REWRITE_TAC[SET_RULE`{(a:real^3)} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
 502   THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
 503 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]AZIM_COMPL)
 504 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 505 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (y:real^3)`]AZIM_COMPL) THEN
 506 ASM_REWRITE_TAC[] THEN  DISCH_TAC
 507 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH`(a - (b:real) <= (a:real)- (c:real))<=> c <= b`]
 508    THEN STRIP_TAC
 509  THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`; `(w:real^3)`] SIGMA_FAN)
 510    THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(y:real^3)`th))
 511    THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
 512    THEN SUBGOAL_THEN`azim (x:real^3) (v:real^3) (w:real^3) (y:real^3) = azim x v w (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ASSUME_TAC
 513 THENL(*14*)[
 514 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC  THEN REAL_ARITH_TAC;(*14*)
 515
 516 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(w:real^3)`;` (y:real^3)`; ` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ]UNIQUE_AZIM_POINT_FAN)
 517   THEN ASM_REWRITE_TAC[]
 518
 519 ]]]]]]]]]]]];
 520 ASM_REWRITE_TAC[]]]);;
 521
 522
 523
 524
 525
 526 let cyclic_power_sigma_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) (j:num).
 527 FAN(x,V,E) /\ (i< CARD(set_of_edge v V E))  /\ (j<i) /\ ({v,u} IN E)
 528 ==> ~(power_map_points (sigma_fan) x V E v u i= power_map_points (sigma_fan) x V E v u j)
 529 `,
 530
 531 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
 532 MP_TAC(ISPECL[`(i:num)`;` (j:num)`;` (x:real^3)`;` (V:real^3->bool)`;
 533 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]MONO_POWER_SIGMA_FAN)
 534   THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE` j < i ==> 0 < (i:num)-(j:num)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 535   THEN MP_TAC(ARITH_RULE` (j:num) <(i:num)==> i-j <= i`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 536   THEN MP_TAC(ARITH_RULE` (i :num )-(j:num) <= i /\ i< CARD(set_of_edge (v:real^3)(V:real^3->bool) (E:(real^3->bool)->bool))==> i-j <CARD(set_of_edge (v:real^3)(V:real^3->bool) (E:(real^3->bool)->bool))`)  THEN ASM_REWRITE_TAC[]
 537   THEN DISCH_TAC
 538   THEN MP_TAC(ISPECL[`(i:num)-(j:num)`;` (x:real^3)`;` (V:real^3->bool)`;
 539 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]key_lemma_cyclic_fan)
 540   THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);;
 541
 542
 543
 544
 545
 546 let CARD_SET_OF_ORBITS_POINTS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 547 FAN(x,V,E) /\ ({v,u} IN E)
 548 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))= CARD(set_of_edge v V E)`,
 549
 550 REPEAT GEN_TAC THEN STRIP_TAC THEN
 551 SUBGOAL_THEN`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i|   (i< CARD(set_of_edge v V E))}
 552 SUBSET  set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
 553 `ASSUME_TAC
 554 THENL[ REWRITE_TAC[set_of_orbits_points_fan;SUBSET;IN_ELIM_THM]
 555  THEN GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
 556
 557 SUBGOAL_THEN`CARD {power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i|   (i< CARD(set_of_edge v V E))}
 558 <= CARD  (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`
 559 ASSUME_TAC
 560 THENL[
 561 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
 562 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`] FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
 563   THEN DISCH_TAC
 564   THEN MP_TAC(ISPECL[`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i|   (i< CARD(set_of_edge v V E))}`;`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_SUBSET) THEN ASM_REWRITE_TAC[];
 565
 566 MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
 567 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 568   THEN MP_TAC(ISPECL[`CARD(set_of_edge  (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_EQ)
 569                 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 570   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
 571 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_ORBITS_EDGE_FAN_LE)
 572   THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC]]);;
 573
 574
 575 let ORBITS_EQ_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 576 FAN(x,V,E) /\ ({v,u} IN E)
 577 ==>
 578 set_of_edge v V E
 579 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
 580
 581 REWRITE_TAC[SET_RULE`(set_of_edge v V E
 582 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))<=>  (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)= set_of_edge v V E) `] THEN
 583 REPEAT STRIP_TAC THEN  MATCH_MP_TAC CARD_SUBSET_EQ THEN
 584 STRIP_TAC THENL[REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan1] THEN MESON_TAC[remark_finite_fan1];
 585 ASM_MESON_TAC[ORBITS_SUBSET_EDGE_FAN;CARD_SET_OF_ORBITS_POINTS_FAN]]);;
 586
 587
 588 let SIMP_ORBITS_POINTS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
 589 FAN(x,V,E) /\ ({v,u} IN E)
 590 ==>
 591 {power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i|   (i< CARD(set_of_edge v V E))}
 592 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
 593 `,
 594
 595 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i|   (i< CARD(set_of_edge v V E))}
 596 SUBSET  set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
 597 `ASSUME_TAC
 598 THENL[
 599  REWRITE_TAC[set_of_orbits_points_fan;SUBSET;IN_ELIM_THM]
 600  THEN GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
 601
 602 POP_ASSUM MP_TAC THEN MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
 603 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 604   THEN MP_TAC(ISPECL[`CARD(set_of_edge  (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_EQ)
 605                 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"a")
 606   THEN MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
 607 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_SET_OF_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[SET_RULE`a=b<=> b=a`] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[]
 608   THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
 609 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`] FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
 610   THEN MESON_TAC[CARD_SUBSET_EQ]]);;
 611
 612
 613 let ORDER_POWER_SIGMA_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
 614 FAN(x,V,E) /\ (i=CARD(set_of_edge v V E)) /\ ({v,u} IN E)
 615 ==> power_map_points (sigma_fan) x V E v u i= u
 616 `,
 617 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) IN  set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` ASSUME_TAC
 618 THENL[
 619  REWRITE_TAC[ set_of_orbits_points_fan; IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
 620
 621 POP_ASSUM MP_TAC THEN  MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
 622 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIMP_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 623   THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th);]) THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
 624                 THEN ASM_REWRITE_TAC[] THEN
 625 MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`i':num`;`(x:real^3)`;` (V:real^3->bool)`;
 626 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]MONO_POWER_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
 627   THEN DISJ_CASES_TAC(ARITH_RULE`(0<(i':num))\/  i'=0`)
 628 THENL[
 629 DISCH_TAC THEN
 630 MP_TAC(ARITH_RULE`0 < (i':num)/\ i'< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) ==> (CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))- (i':num) < CARD (set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 631   THEN MP_TAC(ARITH_RULE`(i':num)< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> 0< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))-i'`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
 632                 THEN
 633 MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))-(i':num)`; `(x:real^3)`;` (V:real^3->bool)`;
 634 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]key_lemma_cyclic_fan)
 635   THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[];
 636
 637 ASM_REWRITE_TAC[power_map_points]]]);;
 638
 639
 640
 641
 642
 643
 644
 645 end;;