text_formalization/local/localization.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Introduction                                                      *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2013-02-18                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 Various odds and ends from the first part of the Local fan chapter
  11 *)
  12
  13 module Localization = struct
  14
  15   open Hales_tactic;;
  16
  17 parse_as_infix("has_orders",(12,"right"));;
  18 parse_as_infix("cyclic_on",(13,"right"));;
  19
  20 let has_orders = new_definition ` (f: A -> A) has_orders k <=>
  21 (! i. 0 < i /\ i < k ==> ~( ITER i f = I )) /\
  22 ITER k f = I `;;
  23
  24 let order = new_definition ` order f x y = (@n. ITER n f x =y /\ (!i. 0< i /\ i< n ==> ~(ITER i f x= y)))`;;
  25
  26
  27 let cyclic_on = new_definition` f cyclic_on (S:A -> bool) <=>
  28 (! x. x IN S ==> S = {z | ?n. z = ITER n f x }) `;;
  29
  30 let dih2k = new_definition` dih2k (H: (A) hypermap) k <=>
  31 CARD (dart H) = 2 * k
  32 /\ (! x. x IN (dart H) ==> let S = face H x in
  33          dart H = S UNION (IMAGE (node_map H) S ))
  34 /\ (face_map H ) has_orders k /\
  35 (edge_map H ) has_orders 2 /\
  36 (node_map H) has_orders 2 `;;
  37
  38 let EE = new_definition` EE v S = {w | {v,w} IN S }`;;
  39
  40 let ord_pairs = new_definition` ord_pairs E = { a,b | {a,b} IN E } `;;
  41
  42 let self_pairs = new_definition` self_pairs E V = { (v,v) | v IN V /\
  43  EE v E = {} } `;;
  44
  45 let darts_of_hyp = new_definition` darts_of_hyp E V = ord_pairs E UNION
  46 self_pairs E V `;;
  47
  48 let ee_of_hyp = new_definition` ee_of_hyp (x,V,E) ((a:real^3),(b:real^3)) =
  49 if (a,b) IN darts_of_hyp E V then (b,a) else (a,b)`;;
  50
  51 let nn_of_hyp = new_definition` nn_of_hyp (x,V,E) (v,u) =
  52 if (v,u) IN darts_of_hyp E V then
  53 (v, azim_cycle (EE v E) x v u) else (v,u)`;;
  54
  55 let ivs_azim_cycle = new_definition`ivs_azim_cycle W v0 v w =
  56 if W = {} then w else
  57 (@x. x IN W /\ azim_cycle W v0 v x = w ) `;;
  58
  59 let ff_of_hyp = new_definition` ff_of_hyp (x,V,E) (v,u) =
  60 if (v,u) IN darts_of_hyp E V then
  61 (u, ivs_azim_cycle (EE u E) x u  v) else (v,u)`;;
  62
  63 let HYP = new_definition` HYP (x,V,E) = (darts_of_hyp E V,
  64 ee_of_hyp (x,V,E), nn_of_hyp (x,V,E), ff_of_hyp (x,V,E)) `;;
  65
  66 let local_fan = new_definition ` local_fan (V,E,FF ) <=>
  67  let H = hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) in
  68   FAN (vec 0, V, E) /\
  69   (?x. x IN ( dart H) /\ FF = face H x ) /\
  70 dih2k H (CARD FF ) `;;
  71
  72 let rho_node1 = new_definition `!(v:real^3) FF. rho_node1 FF v = (@w. v,w IN FF)`;;
  73
  74 let azim_in_fan = new_definition` azim_in_fan (v:real^3,w:real^3) E =
  75 let d = (azim_cycle (EE v E) ( vec 0 ) v w) in
  76  if CARD ( EE v E ) > 1 then
  77  azim (vec 0 ) v w d else &2 * pi `;;
  78
  79 let wedge_in_fan_gt = new_definition`wedge_in_fan_gt (v,w) E =
  80   if CARD (EE v E) > 1 then
  81 wedge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else if
  82 EE v E = {w} then { x | ~ ( x IN aff_ge {vec 0, v} {w} ) } else
  83 { x | ~ ( x IN aff {vec 0, v} )} `;;
  84
  85 let wedge_ge = new_definition `wedge_ge  v0 v1 w1 w2 = { z |
  86 &0 <= azim v0 v1 w1 z /\ azim v0 v1 w1 z <= azim v0 v1 w1 w2 }`;;
  87
  88 let wedge_in_fan_ge = new_definition` wedge_in_fan_ge ((v:real^3),w) E =
  89   if CARD (EE v E) > 1 then
  90 wedge_ge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else { x:real^3 | T } `;;
  91
  92 let convex_local_fan = new_definition
  93   `convex_local_fan (V,E,FF) <=>
  94    local_fan (V,E,FF) /\
  95    (!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E)`;;
  96
  97 let v_prime = new_definition `v_prime V FF = {v| v IN V /\
  98  (?w. (v,w) IN FF )} `;;
  99
 100 let e_prime = new_definition ` e_prime E FF = {{v,w} | {v,w} IN E /\
 101 (v,w) IN FF } `;;
 102
 103 let generic = new_definition` generic V E <=>
 104 (! v w u. {v,w} IN E /\ u IN V ==> aff_ge { vec 0 } {v,w} INTER
 105 aff_lt {vec 0} {u} = {} )`;;
 106
 107 let circular = new_definition ` circular V E <=>
 108 (? v w u. {v,w} IN E /\ u IN V /\ ~(aff_gt { vec 0 } {v,w} INTER
 109 aff_lt {vec 0} {u} = {}) )`;;
 110
 111 let lunar = new_definition
 112 ` lunar (v,w) V E <=> ~(circular V E) /\ {v,w} SUBSET V /\
 113 ~( v = w ) /\ collinear {vec 0, v, w } `;;
 114
 115 let rho_node1 = new_definition ` rho_node1 (FF:real^3 # real^3 -> bool) v = (@w. (v,w) IN FF)`;;
 116
 117 let ivs_rho_node1 = new_definition ` ivs_rho_node1 (FF:real^3 # real^3 -> bool) v = (@a. a,v IN FF )`;;
 118
 119 let interior_angle1 = new_definition
 120 ` interior_angle1 x FF v = azim x v (rho_node1 FF v) (@a. a,v IN FF)`;;
 121
 122 let sol_local = new_definition ` sol_local E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
 123
 124 let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
 125
 126 let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
 127
 128 let deformation = new_definition
 129 ` deformation ff V (a,b) <=> (&0) IN real_interval (a,b) /\
 130 (! v r. v IN V /\ r IN real_interval (a,b) ==> (ff v) continuous atreal r) /\
 131 (!v. v IN V ==> ff v (&0) = v )`;;
 132
 133 let localization = new_definition `localization (V, E) FF = (v_prime V FF, e_prime E FF) `;;
 134
 135 let a_ear0=new_definition`a_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 136  (if {i  MOD 3,j MOD 3} IN J then sqrt(&8) else &2)) `;;
 137
 138 let b_ear0=new_definition`b_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 139  (if {i  MOD 3,j MOD 3} IN J then cstab else &2* h0)) `;;
 140
 141 let JNVXCRC = new_definition
 142  `polar_fan(V,(E:(real^3->bool)->bool),FF) =
 143         let r = rho_node1 FF in
 144         let prime = \v. v cross (r v) in
 145         ({ prime v | v IN V},
 146          { {prime v,prime(r v)} | v IN V},
 147          { (prime v,prime(r v)) | v IN V})`;;
 148
 149
 150
 151
 152 (* deprecated:
 153 let v_slice = new_definition ` v_slice f (v,w) =
 154 { ITER i f v | ! j. j < i ==> ~( ITER j f v = w ) }`;;
 155
 156
 157 let e_slice = new_definition ` e_slice f (v,w) =
 158 {w,v} INSERT
 159 { {ITER i f v, ITER (i + 1) f v} | ! j. j < i + 1 ==> ~( ITER j f v = w)} `;;
 160
 161
 162 let f_slice = new_definition ` f_slice f (v,w) =
 163 (w,v) INSERT
 164 { (ITER i f v, ITER (i + 1) f v) | ! j. j < i + 1 ==> ~ (ITER j f v = w)} `;;
 165 *)
 166
 167
 168 let slicev = new_definition ` slicev E FF v w = {u| ?n. 0<= n /\ n<= order (rho_node1 FF) v w /\ u= ITER n (rho_node1 FF) v}`;;
 169
 170 let slicee = new_definition ` slicee E FF v w = {e| ?u. u IN (slicev E FF v w) DELETE w /\ e={u,rho_node1 FF u} } UNION {{w,v}}`;;
 171
 172 let slicef = new_definition ` slicef E FF v w = {f| ?u. u IN (slicev E FF v w) DELETE w /\ f=(u,rho_node1 FF u) } UNION {(w,v)}`;;
 173
 174 let FAN_EDGE_SUBSET_V = prove_by_refinement(
 175   `!V E e. FAN(vec 0, V, E) /\ e IN E ==> e SUBSET V`,
 176   (* {{{ proof *)
 177   [
 178   REWRITE_TAC[Fan_defs.FAN;UNIONS_SUBSET];
 179   BY(MESON_TAC[])
 180   ]);;
 181   (* }}} *)
 182
 183 let FAN_EDGE_EL_V = prove_by_refinement(
 184   `!V E u v. FAN(vec 0,V,E) /\ {u,v} IN E ==> v IN V`,
 185   (* {{{ proof *)
 186   [
 187   REPEAT WEAKER_STRIP_TAC;
 188   TYPIFY `v IN {u,v}` (C SUBGOAL_THEN ASSUME_TAC);
 189     BY(SET_TAC[]);
 190   BY(ASM_MESON_TAC[FAN_EDGE_SUBSET_V;SUBSET])
 191   ]);;
 192   (* }}} *)
 193
 194 (* renamed from FAN_EE, EE_EQ_set_of_edge *)
 195
 196 let EE_elim = prove_by_refinement(
 197   `!V E (v:real^3). FAN(vec 0,V,E) ==> EE v E = set_of_edge v V E`,
 198   (* {{{ proof *)
 199   [
 200   REPEAT WEAKER_STRIP_TAC;
 201   REWRITE_TAC[EE;Fan_defs.set_of_edge];
 202   REWRITE_TAC[EXTENSION;IN_ELIM_THM];
 203   BY(ASM_MESON_TAC[FAN_EDGE_EL_V])
 204   ]);;
 205   (* }}} *)
 206
 207 (* renamed from darts_of_hyp_EQ_dart_of_fan *)
 208
 209 let darts_of_hyp_elim = prove_by_refinement(
 210   `!V E. FAN(vec 0,V,E) ==> darts_of_hyp E V = dart_of_fan (V,E)`,
 211   (* {{{ proof *)
 212   [
 213   REWRITE_TAC[darts_of_hyp;Fan_defs.dart_of_fan;ord_pairs;self_pairs;SUBSET];
 214   REPEAT WEAKER_STRIP_TAC;
 215   ASM_SIMP_TAC[GSYM EE_elim];
 216   BY(SET_TAC[])
 217   ]);;
 218   (* }}} *)
 219
 220 let dart_of_fan_eq = prove_by_refinement(
 221  `!V E.
 222          dart_of_fan (V,E) =
 223          dart1_of_fan (V,E) UNION {v,v | v IN V /\ set_of_edge v V E = {}}`,
 224   (* {{{ proof *)
 225   [
 226   REWRITE_TAC[Fan_defs.dart_of_fan;EXTENSION;IN_UNION;Fan_defs.dart1_of_fan];
 227   BY(SET_TAC[])
 228   ]);;
 229   (* }}} *)
 230
 231
 232 (* renamed from ee_of_hyp_EQ_e_fan_pair_ext *)
 233
 234 let ee_of_hyp_elim = prove_by_refinement(
 235   `!V E (x:A).  FAN(vec 0,V,E)  ==> ee_of_hyp(x,V,E) = e_fan_pair_ext(V,E)`,
 236   (* {{{ proof *)
 237   [
 238   REPEAT WEAKER_STRIP_TAC;
 239   REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
 240   REWRITE_TAC[ee_of_hyp;Fan_defs.e_fan_pair_ext;Fan_defs.e_fan_pair];
 241   ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
 242   REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
 243   REPEAT WEAKER_STRIP_TAC;
 244   TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
 245     BY(ASM_REWRITE_TAC[]);
 246   ASM_REWRITE_TAC[];
 247   COND_CASES_TAC;
 248     BY(ASM_REWRITE_TAC[]);
 249   BY(REWRITE_TAC[])
 250   ]);;
 251   (* }}} *)
 252
 253 let AZIM_CYCLE_EQ_SIGMA_FAN_ALT = prove_by_refinement(
 254   `!V E u v. FAN (vec 0,V,E) /\ u IN set_of_edge v V E
 255         ==> azim_cycle (set_of_edge v V E) (vec 0) v u = sigma_fan (vec 0) V E v u`,
 256   (* {{{ proof *)
 257   [
 258   BY(ASM_MESON_TAC[EE_elim;Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN])
 259   ]);;
 260   (* }}} *)
 261
 262 (* renamed from nn_of_hyp_EQ_n_fan_pair_ext : *)
 263
 264 let nn_of_hyp_elim = prove_by_refinement(
 265   `!V E.  FAN(vec 0,V,E)  ==> nn_of_hyp((vec 0),V,E) = n_fan_pair_ext(V,E)`,
 266   (* {{{ proof *)
 267   [
 268   REPEAT WEAKER_STRIP_TAC;
 269   REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
 270   REWRITE_TAC[nn_of_hyp;Fan_defs.n_fan_pair_ext;Fan_defs.n_fan_pair];
 271   ASM_SIMP_TAC[EE_elim;darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
 272   REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
 273   REPEAT WEAKER_STRIP_TAC;
 274   TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
 275     (ASM_REWRITE_TAC[PAIR_EQ]);
 276     GMATCH_SIMP_TAC AZIM_CYCLE_EQ_SIGMA_FAN_ALT;
 277     ASM_REWRITE_TAC[];
 278     FIRST_X_ASSUM MP_TAC;
 279     REWRITE_TAC[Fan_defs.dart1_of_fan;Fan_defs.set_of_edge];
 280     REWRITE_TAC[IN_ELIM_PAIR_THM];
 281     REWRITE_TAC[IN_ELIM_THM];
 282     BY(ASM_MESON_TAC[FAN_EDGE_EL_V]);
 283   ASM_REWRITE_TAC[];
 284   TYPIFY`~(p1 = p2)` ASM_CASES_TAC;
 285     BY(ASM_REWRITE_TAC[]);
 286   FIRST_X_ASSUM (ASSUME_TAC o (REWRITE_RULE[]));
 287   ASM_REWRITE_TAC[];
 288   COND_CASES_TAC;
 289     ASM_REWRITE_TAC[PAIR_EQ];
 290     INTRO_TAC Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE [`{}:real^3->bool`;`p2`];
 291     ANTS_TAC;
 292       BY(SET_TAC[]);
 293     BY(MESON_TAC[]);
 294   BY(REWRITE_TAC[])
 295   ]);;
 296   (* }}} *)
 297
 298 (* renamed from ivs_azim_cycle_EQ_inverse_sigma_fan *)
 299
 300 let ivs_azim_cycle_elim = prove_by_refinement(
 301   `!V E p1 p2. FAN(vec 0,V,E)   /\ {p1,p2} IN E
 302   ==> ivs_azim_cycle (set_of_edge p1 V E) (vec 0) p1 p2 = inverse_sigma_fan (vec 0) V E p1 p2`,
 303   (* {{{ proof *)
 304   [
 305   REPEAT WEAKER_STRIP_TAC;
 306   ASM_SIMP_TAC[GSYM Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN];
 307   ASM_SIMP_TAC[ (GSYM Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN)];
 308   BY(ASM_MESON_TAC[EE_elim])
 309   ]);;
 310   (* }}} *)
 311
 312 (* renamed from ff_of_hyp_EQ_f_fan_pair_ext: *)
 313
 314 let ff_of_hyp_elim = prove_by_refinement(
 315   `!V E.  FAN(vec 0,V,E)  ==> ff_of_hyp(vec 0,V,E) = f_fan_pair_ext(V,E)`,
 316   (* {{{ proof *)
 317   [
 318   REPEAT WEAKER_STRIP_TAC;
 319   REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM];
 320   REWRITE_TAC[ff_of_hyp;Fan_defs.f_fan_pair_ext;Fan_defs.f_fan_pair];
 321   ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ];
 322   REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM];
 323   REPEAT WEAKER_STRIP_TAC;
 324   TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC;
 325     (ASM_REWRITE_TAC[PAIR_EQ]);
 326     ASM_SIMP_TAC[EE_elim];
 327     GMATCH_SIMP_TAC ivs_azim_cycle_elim;
 328     ASM_REWRITE_TAC[];
 329     RULE_ASSUM_TAC (REWRITE_RULE[Fan_defs.dart1_of_fan;IN_ELIM_PAIR_THM]);
 330     BY(ASM_MESON_TAC[Collect_geom.PER_SET2]);
 331   ASM_REWRITE_TAC[];
 332   COND_CASES_TAC THEN REWRITE_TAC[];
 333   ASM_REWRITE_TAC[PAIR_EQ];
 334   ASM_SIMP_TAC[EE_elim];
 335   BY(REWRITE_TAC[Wrgcvdr_cizmrrh.IVS_AZIM_EMPTY_IDE])
 336   ]);;
 337   (* }}} *)
 338
 339 let HYP_elim = prove_by_refinement(
 340   `!V E. FAN (vec 0, V, E) ==> HYP ((vec 0),V,E) = (dart_of_fan (V,E),
 341   e_fan_pair_ext(V,E),n_fan_pair_ext(V,E),f_fan_pair_ext(V,E))`,
 342   (* {{{ proof *)
 343   [
 344   REPEAT WEAKER_STRIP_TAC;
 345   BY(ASM_SIMP_TAC[HYP;darts_of_hyp_elim;ee_of_hyp_elim;nn_of_hyp_elim;ff_of_hyp_elim])
 346   ]);;
 347   (* }}} *)
 348
 349 let hypermap_HYP_elim = prove_by_refinement(
 350   `!V E.  FAN(vec 0,V,E) ==> hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) = hypermap_of_fan (V,E) `,
 351   (* {{{ proof *)
 352   [
 353   REPEAT WEAKER_STRIP_TAC;
 354   BY(ASM_SIMP_TAC[Fan_defs.HYPERMAP_OF_FAN_ALT;HYP_elim])
 355   ]);;
 356   (* }}} *)
 357
 358 let local_fan2 = prove_by_refinement(
 359   `!V E FF. local_fan (V,E,FF ) <=>
 360  let H = hypermap_of_fan (V,E) in
 361   FAN (vec 0, V, E) /\
 362   FF IN face_set H /\
 363   dih2k H (CARD FF ) `,
 364   (* {{{ proof *)
 365   [
 366   REPEAT WEAKER_STRIP_TAC;
 367   REWRITE_TAC[local_fan;LET_DEF;LET_END_DEF];
 368   TYPIFY `FAN(vec 0,V,E)` ASM_CASES_TAC;
 369     ASM_SIMP_TAC[hypermap_HYP_elim];
 370     BY(ASM_MESON_TAC[Hypermap.lemma_in_face_set;Hypermap.lemma_face_representation]);
 371   BY(ASM_REWRITE_TAC[])
 372   ]);;
 373   (* }}} *)
 374
 375 let WRGCVDR_BIJ = prove_by_refinement(
 376   `!V E FF. local_fan (V,E,FF)
 377         ==> BIJ FST FF V`,
 378   (* {{{ proof *)
 379   [
 380     BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.WRGCVDR;FUN_EQ_THM])
 381   ]);;
 382   (* }}} *)
 383
 384 let  WRGCVDR_ORBIT = prove_by_refinement(
 385   `!V E FF. local_fan (V,E,FF) ==>
 386       (!v. v IN V ==> orbit_map (rho_node1 FF) v = V) `,
 387   (* {{{ proof *)
 388   [
 389     BY(MESON_TAC[ Local_lemmas.LOCAL_FAN_ORBIT_MAP_V])
 390   ]);;
 391   (* }}} *)
 392
 393 let ALL_TO_THE_NONPARALLEL_PART_ALT = prove_by_refinement(
 394   `!a b V E phii. deformation phii V (a,b) /\ FAN (vec 0,V,E)
 395         ==> (?e. &0 < e /\
 396                  (!t. --e < t /\ t < e
 397                       ==> UNIONS (IMAGE (IMAGE (\v. phii v t)) E) SUBSET
 398                           IMAGE (\v. phii v t) V /\
 399                           graph (IMAGE (IMAGE (\v. phii v t)) E) /\
 400                           fan1
 401                           ((vec 0):real^3,
 402                            IMAGE (\v. phii (v:real^3) t) V,
 403                            IMAGE (IMAGE (\v. phii v t)) E) /\
 404                           fan2
 405                           ((vec 0):real^3,
 406                            IMAGE (\v. phii v t) V,
 407                            IMAGE (IMAGE (\v. phii v t)) E) /\
 408                           fan6
 409                           (vec 0,
 410                            IMAGE (\v. phii v t) V,
 411                            IMAGE (IMAGE (\v. phii v t)) E)))`,
 412   (* {{{ proof *)
 413   [
 414   REPEAT WEAKER_STRIP_TAC;
 415   MATCH_MP_TAC Local_lemmas1.ALL_TO_THE_NONPARALLEL_PART;
 416   BY(ASM_REWRITE_TAC[])
 417   ]);;
 418   (* }}} *)
 419
 420 (* moved to deformation.hl
 421 let XRECQNS = prove_by_refinement(
 422   `!a b V E f.
 423     deformation f V (a,b) /\ FAN (vec 0,V,E) ==>
 424      (?e. &0 < e /\ (!t. --e < t /\ t < e ==>
 425         FAN(vec 0,
 426             IMAGE (\v. f (v:real^3) t) V,
 427                                IMAGE (IMAGE (\v. f v t)) E)))`,
 428   (* {{{ proof *)
 429   [
 430   REPEAT STRIP_TAC;
 431   REWRITE_TAC[Fan.FAN];
 432   INTRO_TAC ALL_TO_THE_NONPARALLEL_PART_ALT [`a`;`b`;`V`;`E`;`f`];
 433   ASM_REWRITE_TAC[];
 434   REPEAT STRIP_TAC;
 435   INTRO_TAC Deformation.FAN7_SMALL_DEFORMATION [`V`;`E`;`a`;`b`;`f`];
 436   ASM_REWRITE_TAC[];
 437   REPEAT STRIP_TAC;
 438   TYPIFY `if (e < e') then e else e'` EXISTS_TAC;
 439   COND_CASES_TAC;
 440     ASM_REWRITE_TAC[];
 441     REPEAT WEAKER_STRIP_TAC;
 442     BY(ASM_MESON_TAC[arith `&0 < e /\ e < e' /\ -- e < t /\ t < e ==> -- e' < t /\ t < e'`]);
 443   ASM_REWRITE_TAC[];
 444   REPEAT WEAKER_STRIP_TAC;
 445   BY(ASM_MESON_TAC[arith `&0 < e' /\ ~(e < e') /\ -- e' < t /\ t < e' ==> -- e < t /\ t < e`])
 446   ]);;
 447   (* }}} *)
 448 *)
 449
 450 let COMPATIBLE_BW_TWO_LEMMAS2_ALT = prove_by_refinement(
 451   `!V E FF HS fv fw v w. (convex_local_fan (V,E,FF) /\
 452          v IN V /\
 453          w IN V /\
 454          ~(v = w) /\
 455          (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
 456          HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
 457          fv = face HS (v,rho_node1 FF v)) /\
 458         fw = face HS (w,rho_node1 FF w)
 459         ==> (v_prime V fv = slicev E FF v w /\
 460              e_prime (E UNION {{v, w}}) fv = slicee E FF v w /\
 461              fv = slicef E FF v w) /\
 462             v_prime V fw = slicev E FF w v /\
 463             e_prime (E UNION {{w, v}}) fw = slicee E FF w v /\
 464             fw = slicef E FF w v`,
 465   (* {{{ proof *)
 466   [
 467   MESON_TAC[Nkezbfc_local.COMPATIBLE_BW_TWO_LEMMAS2]
 468   ]);;
 469   (* }}} *)
 470
 471 let EJRCFJD_ALT = prove_by_refinement(
 472   `!V E FF HS fv fw v w. convex_local_fan (V,E,FF) /\
 473         v IN V /\
 474         w IN V /\
 475         ~(v = w) /\
 476         (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
 477         HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
 478         fv = face HS (v,rho_node1 FF v) /\
 479         fw = face HS (w,rho_node1 FF w)
 480         ==> convex_local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\
 481             convex_local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw) /\
 482             (!ff. sum {i | i < CARD V}
 483                   (\i. ff i *
 484                        interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v)) =
 485                   sum
 486                   {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fv}
 487                   (\i. ff i *
 488                        interior_angle1 (vec 0) fv (ITER i (rho_node1 FF) v)) +
 489                   sum
 490                   {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fw}
 491                   (\i. ff i *
 492                        interior_angle1 (vec 0) fw (ITER i (rho_node1 FF) v)))`,
 493   (* {{{ proof *)
 494   [
 495   MESON_TAC[Local_lemmas1.EJRCFJD]
 496   ]);;
 497   (* }}} *)
 498
 499 let WEDGE_VV = prove_by_refinement(
 500   `!a b c d. ~(b IN wedge a b c d) `,
 501   (* {{{ proof *)
 502   [
 503   REWRITE_TAC[wedge;IN_ELIM_THM];
 504   REPEAT GEN_TAC;
 505   TYPIFY `{a,b,b} = {a,b}` (C SUBGOAL_THEN SUBST1_TAC);
 506     BY(SET_TAC[]);
 507   BY(REWRITE_TAC[COLLINEAR_2])
 508   ]);;
 509   (* }}} *)
 510
 511 let ejr_distinct = prove_by_refinement(
 512   `!V E FF v w. convex_local_fan (V,E,FF) /\
 513     v IN V /\
 514   (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==>
 515     ~(w = v)`,
 516   (* {{{ proof *)
 517   [
 518   REPEAT WEAKER_STRIP_TAC;
 519   FIRST_X_ASSUM_ST `aff_gt` MP_TAC;
 520   REWRITE_TAC[NOT_FORALL_THM];
 521   TYPIFY `(v,rho_node1 FF v)` EXISTS_TAC;
 522   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 523     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 524   DISCH_THEN MP_TAC THEN ANTS_TAC;
 525     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
 526   ASM_REWRITE_TAC[];
 527   TYPIFY `{v,v} = {v}` (C SUBGOAL_THEN SUBST1_TAC);
 528     BY(SET_TAC[]);
 529   TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
 530     BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
 531   ASM_REWRITE_TAC[wedge_in_fan_gt];
 532   TYPIFY `v IN aff_gt {vec 0} {v}` (C SUBGOAL_THEN ASSUME_TAC);
 533     GMATCH_SIMP_TAC AFF_GT_1_1;
 534     REWRITE_TAC[DISJOINT;IN_ELIM_THM];
 535     REWRITE_TAC[EXTENSION;IN_INTER;IN_SING;NOT_IN_EMPTY];
 536     CONJ_TAC;
 537       RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN]);
 538       RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;LET_DEF;LET_END_DEF;Fan_defs.fan2]);
 539       BY(ASM_MESON_TAC[]);
 540     GEXISTL_TAC [`&0`;`&1`];
 541     REWRITE_TAC[arith `&0 < &1`;arith `&0 + &1 = &1`];
 542     BY(VECTOR_ARITH_TAC);
 543   REWRITE_TAC[SUBSET];
 544   BY(ASM_MESON_TAC[WEDGE_VV])
 545   ]);;
 546   (* }}} *)
 547
 548 (*
 549   TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
 550     BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
 551   FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC;
 552 *)
 553
 554 let WEDGE_EDGE_NOT_ADJ = prove_by_refinement(
 555   `!V E FF v .  local_fan (V,E,FF) /\
 556          v IN V ==>
 557            ~(aff_gt {vec 0} {v, rho_node1 FF v} SUBSET wedge_in_fan_gt (v,rho_node1 FF v) E) `,
 558   (* {{{ proof *)
 559   [
 560   REPEAT WEAKER_STRIP_TAC;
 561   TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC);
 562     BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]);
 563   FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC;
 564   ASM_REWRITE_TAC[wedge_in_fan_gt];
 565   REPEAT WEAKER_STRIP_TAC;
 566   INTRO_TAC Nkezbfc_local.AFF_GT_SUBSET_WEDGE_IMP_VERTEX [`(vec 0):real^3`;`v`;`rho_node1 FF v`;`rho_node1 FF v`;`azim_cycle (EE v E) (vec 0) v (rho_node1 FF v)`];
 567   ASM_REWRITE_TAC[];
 568   GMATCH_SIMP_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND;
 569   CONJ_TAC;
 570     BY(ASM_MESON_TAC[]);
 571   DISCH_THEN MP_TAC THEN ANTS_TAC;
 572     BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS;Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
 573   BY(REWRITE_TAC[wedge;IN_ELIM_THM;AZIM_REFL;arith `~(&0 < &0)`])
 574   ]);;
 575   (* }}} *)
 576
 577 let PERIODIC_RHO_NODE1 = prove_by_refinement(
 578   `!V E FF v.  local_fan (V,E,FF) /\ v IN V ==> periodic (\i. ITER i (rho_node1 FF) v) (CARD V)`,
 579   (* {{{ proof *)
 580   [
 581   REWRITE_TAC[Oxl_def.periodic;GSYM ITER_ADD];
 582   REPEAT WEAKER_STRIP_TAC;
 583   AP_TERM_TAC;
 584   MATCH_MP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2;
 585   BY(ASM_REWRITE_TAC[])
 586   ]);;
 587   (* }}} *)
 588
 589 let V_PRIME_SUBSET_V = prove_by_refinement(
 590   `!V f.  v_prime (V:real^3->bool) (f:real^3 # real^3 -> bool) SUBSET V`,
 591   (* {{{ proof *)
 592   [
 593   REWRITE_TAC[v_prime;SUBSET;IN_ELIM_THM];
 594   BY(MESON_TAC[])
 595   ]);;
 596   (* }}} *)
 597
 598 let SLICEV_IMAGE = prove_by_refinement(
 599   `!V E FF v w i.
 600      convex_local_fan (V,E,FF) /\
 601      v IN V /\
 602      w IN V /\
 603      (!u u1.
 604           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
 605      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
 606      (i < CARD V) /\
 607      (w = ITER i (rho_node1 FF) v)
 608      ==>
 609        slicev E FF v w = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 } `,
 610   (* {{{ proof *)
 611   [
 612   REPEAT WEAKER_STRIP_TAC;
 613   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
 614   ANTS_TAC;
 615     BY(ASM_REWRITE_TAC[]);
 616   DISCH_TAC;
 617   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
 618   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
 619   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
 620   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 621   ASM_REWRITE_TAC[];
 622   REPEAT WEAKER_STRIP_TAC;
 623   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 624   ANTS_TAC;
 625     BY(ASM_REWRITE_TAC[]);
 626   REPEAT WEAKER_STRIP_TAC;
 627   ASM_REWRITE_TAC[];
 628   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 629     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 630   TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
 631     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
 632   COMMENT "remove a many lines here";
 633   TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC);
 634     MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM);
 635     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
 636     BY(ASM_MESON_TAC[]);
 637   COMMENT "v_prime as image";
 638   TYPIFY `v_prime V fv = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC);
 639     GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE;
 640     GEXISTL_TAC [`w`;`FF`;`v`];
 641     CONJ_TAC;
 642       GEXISTL_TAC [`E`;`HS`];
 643       ASM_REWRITE_TAC[IN_DIFF;IN_SING];
 644       BY(ASM_MESON_TAC[]);
 645     REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
 646     X_GEN_TAC `u:real^3`;
 647     REWRITE_TAC[Geomdetail.EQ_EXPAND];
 648     CONJ_TAC;
 649       REPEAT WEAKER_STRIP_TAC;
 650       TYPIFY `n` EXISTS_TAC;
 651       ASM_REWRITE_TAC[];
 652       REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`];
 653       BY(ASM_MESON_TAC[]);
 654     REPEAT WEAKER_STRIP_TAC;
 655     TYPIFY `x` EXISTS_TAC;
 656     ASM_REWRITE_TAC[];
 657     REPEAT WEAKER_STRIP_TAC;
 658     TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
 659       BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
 660     TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC);
 661       BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]);
 662     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 663   BY(ASM_MESON_TAC[])
 664   ]);;
 665   (* }}} *)
 666
 667 let LOCAL_FAN_ORBIT_MAP_EXPLICIT = prove
 668  (`!V E FF v w.
 669         local_fan(V,E,FF) /\ v IN V /\ w IN V
 670         ==> ?i. i < CARD V /\ w = ITER i (rho_node1 FF) v`,
 671   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o
 672     MATCH_MP Local_lemmas.LOCAL_FAN_ORBIT_MAP_V) THEN
 673   REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER; Hypermap.orbit_map] THEN
 674   ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 675   DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN ASM_REWRITE_TAC[GE; LE_0] THEN
 676   DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
 677   EXISTS_TAC `n MOD (CARD(V:real^3->bool))` THEN
 678   FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN
 679   FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN
 680   MP_TAC(ISPECL [`n:num`; `CARD(V:real^3->bool)`] DIVISION) THEN
 681   ABBREV_TAC `i = n MOD (CARD(V:real^3->bool))` THEN
 682   ABBREV_TAC `m = n DIV (CARD(V:real^3->bool))` THEN
 683   ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN(K ALL_TAC) THEN
 684   SPEC_TAC(`m:num`,`p:num`) THEN
 685   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 686   ONCE_REWRITE_TAC[ARITH_RULE `(a + b) + c:num = (a + c) + b`] THEN
 687   ONCE_REWRITE_TAC[GSYM ITER_ADD] THEN
 688   FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID) THEN
 689   ASM_SIMP_TAC[]);;
 690
 691 let SLICEW_IMAGE = prove_by_refinement(
 692   `!V E FF v w n.
 693      convex_local_fan (V,E,FF) /\
 694      v IN V /\
 695      w IN V /\
 696      (!u u1.
 697           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
 698      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
 699      (n < CARD V) /\
 700      (w = ITER n (rho_node1 FF) v)
 701      ==>
 702        slicev E FF w v = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ (n <= j /\ j < CARD V) }`,
 703   (* {{{ proof *)
 704   [
 705   REPEAT WEAKER_STRIP_TAC;
 706   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
 707   ANTS_TAC;
 708     BY(ASM_REWRITE_TAC[]);
 709   DISCH_TAC;
 710   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
 711   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
 712   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
 713   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 714   ASM_REWRITE_TAC[];
 715   REPEAT WEAKER_STRIP_TAC;
 716   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 717   ANTS_TAC;
 718     BY(ASM_REWRITE_TAC[]);
 719   REPEAT WEAKER_STRIP_TAC;
 720   ASM_REWRITE_TAC[];
 721   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 722     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 723   TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
 724     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
 725   TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fw <=> (j =0) \/ (n <= j /\ j < CARD V)` (C SUBGOAL_THEN ASSUME_TAC);
 726     MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM2);
 727     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
 728     BY(ASM_MESON_TAC[]);
 729   COMMENT "v_prime as image";
 730   TYPIFY `v_prime V fw = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ (n <= j /\ j < CARD V) }` (C SUBGOAL_THEN ASSUME_TAC);
 731     REWRITE_TAC[EXTENSION;IN_IMAGE];
 732     X_GEN_TAC `u:real^3`;
 733     TYPIFY `u IN v_prime V fw` ASM_CASES_TAC;
 734       ASM_REWRITE_TAC[];
 735       INTRO_TAC V_PRIME_SUBSET_V [`V`;`fw`];
 736       REWRITE_TAC[SUBSET];
 737       DISCH_THEN (C INTRO_TAC [`u`]);
 738       DISCH_TAC;
 739       INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`u`];
 740       ANTS_TAC;
 741         BY(ASM_MESON_TAC[]);
 742       REWRITE_TAC[IN_ELIM_THM];
 743       REPEAT WEAKER_STRIP_TAC;
 744       TYPIFY `i` EXISTS_TAC;
 745       ASM_REWRITE_TAC[];
 746       BY(ASM_MESON_TAC[]);
 747     ASM_REWRITE_TAC[];
 748     REWRITE_TAC[NOT_EXISTS_THM;IN_ELIM_THM];
 749     BY(ASM_MESON_TAC[]);
 750   BY(ASM_MESON_TAC[])
 751   ]);;
 752   (* }}} *)
 753
 754 (* Might extract things like the exact card of slicev, and the fact that 3 < CARD V *)
 755
 756 let CARD_SLICEV_LT = prove_by_refinement(
 757   `!V E FF v w.
 758      convex_local_fan (V,E,FF) /\
 759      v IN V /\
 760      w IN V /\
 761      (!u u1.
 762           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
 763      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==>
 764       CARD (slicev E FF v w) < CARD V`,
 765   (* {{{ proof *)
 766   [
 767   REPEAT WEAKER_STRIP_TAC;
 768   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
 769   ANTS_TAC;
 770     BY(ASM_REWRITE_TAC[]);
 771   DISCH_TAC;
 772   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
 773   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
 774   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
 775   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 776   ASM_REWRITE_TAC[];
 777   REPEAT WEAKER_STRIP_TAC;
 778   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
 779   ANTS_TAC;
 780     BY(ASM_REWRITE_TAC[]);
 781   REPEAT WEAKER_STRIP_TAC;
 782   ASM_REWRITE_TAC[];
 783   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 784     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 785   TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC);
 786     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]);
 787   INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`w`];
 788   ASM_REWRITE_TAC[];
 789   REPEAT WEAKER_STRIP_TAC;
 790   TYPIFY `1 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
 791     MATCH_MP_TAC Local_lemmas1.DIFFERENCE_IMP_LT_CARDV;
 792     ASM_REWRITE_TAC[arith `n < 1 <=> n = 0`];
 793     BY(ASM_MESON_TAC[ITER]);
 794   TYPIFY `~(i = CARD V - 1)` (C SUBGOAL_THEN ASSUME_TAC);
 795     DISCH_TAC;
 796     TYPIFY `w = ivs_rho_node1 FF v` (C SUBGOAL_THEN ASSUME_TAC);
 797       BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
 798     INTRO_TAC WEDGE_EDGE_NOT_ADJ [`V`;`E`;`FF`;`w`];
 799     ANTS_TAC;
 800       BY(ASM_REWRITE_TAC[]);
 801     REWRITE_TAC[];
 802     RULE_ASSUM_TAC (ONCE_REWRITE_RULE[Collect_geom.PER_SET2]);
 803     TYPIFY `w,rho_node1 FF w IN FF` (C SUBGOAL_THEN ASSUME_TAC);
 804       BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
 805     TYPIFY `rho_node1 FF w = v` (C SUBGOAL_THEN ASSUME_TAC);
 806       BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]);
 807     BY(ASM_MESON_TAC[]);
 808   TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC);
 809     MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM);
 810     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
 811     BY(ASM_MESON_TAC[]);
 812   COMMENT "v_prime as image";
 813   TYPIFY `v_prime V fv = IMAGE  (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC);
 814     GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE;
 815     GEXISTL_TAC [`w`;`FF`;`v`];
 816     CONJ_TAC;
 817       GEXISTL_TAC [`E`;`HS`];
 818       ASM_REWRITE_TAC[IN_DIFF;IN_SING];
 819       BY(ASM_MESON_TAC[]);
 820     REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
 821     X_GEN_TAC `u:real^3`;
 822     REWRITE_TAC[Geomdetail.EQ_EXPAND];
 823     CONJ_TAC;
 824       REPEAT WEAKER_STRIP_TAC;
 825       TYPIFY `n` EXISTS_TAC;
 826       ASM_REWRITE_TAC[];
 827       REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`];
 828       BY(ASM_MESON_TAC[]);
 829     REPEAT WEAKER_STRIP_TAC;
 830     TYPIFY `x` EXISTS_TAC;
 831     ASM_REWRITE_TAC[];
 832     REPEAT WEAKER_STRIP_TAC;
 833     TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
 834       BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 835     TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC);
 836       BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]);
 837     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
 838   COMMENT "now use IMAGE CARD";
 839   FIRST_X_ASSUM (SUBST1_TAC);
 840   MATCH_MP_TAC LET_TRANS;
 841   TYPIFY `CARD {j | j < i + 1}` EXISTS_TAC;
 842   CONJ_TAC;
 843     MATCH_MP_TAC CARD_IMAGE_LE;
 844     BY(REWRITE_TAC[FINITE_NUMSEG_LT]);
 845   REWRITE_TAC[CARD_NUMSEG_LT];
 846   BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)
 847   ]);;
 848   (* }}} *)
 849
 850 let SLICEW_BIJ = prove_by_refinement(
 851   `!V E FF v w n.
 852          convex_local_fan (V,E,FF) /\
 853          v IN V /\
 854          w IN V /\
 855          (!u u1.
 856               u IN {v, w} /\ u1 IN V /\ ~(u = u1)
 857               ==> ~collinear {vec 0, u, u1}) /\
 858          (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
 859          n < CARD V /\
 860          w = ITER n (rho_node1 FF) v
 861          ==>
 862              BIJ (\j. ITER j (rho_node1 FF) v)
 863              {j | j = 0 \/ n <= j /\ j < CARD V} (slicev E FF w v)`,
 864   (* {{{ proof *)
 865   [
 866   REWRITE_TAC[BIJ];
 867   REPEAT WEAKER_STRIP_TAC;
 868   SUBCONJ2_TAC;
 869     INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
 870     ANTS_TAC;
 871       BY(ASM_REWRITE_TAC[]);
 872     DISCH_THEN SUBST1_TAC;
 873     BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
 874   REWRITE_TAC[SURJ;INJ];
 875   REPEAT WEAKER_STRIP_TAC;
 876   ASM_REWRITE_TAC[];
 877   REWRITE_TAC[IN_ELIM_THM];
 878   REPEAT WEAKER_STRIP_TAC;
 879   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 880     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 881   TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC);
 882     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
 883   TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
 884     ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM];
 885     BY(ASM_MESON_TAC[]);
 886   INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA [];
 887   ASM_REWRITE_TAC[];
 888   DISCH_THEN MATCH_MP_TAC;
 889   BY(ASM_MESON_TAC[])
 890  ]);;
 891   (* }}} *)
 892
 893 let SLICEV_BIJ = prove_by_refinement(
 894   `!V E FF v w n.
 895          convex_local_fan (V,E,FF) /\
 896          v IN V /\
 897          w IN V /\
 898          (!u u1.
 899               u IN {v, w} /\ u1 IN V /\ ~(u = u1)
 900               ==> ~collinear {vec 0, u, u1}) /\
 901          (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
 902          n < CARD V /\
 903          w = ITER n (rho_node1 FF) v
 904          ==>
 905              BIJ (\j. ITER j (rho_node1 FF) v)
 906              {j | j < n + 1} (slicev E FF v w)`,
 907   (* {{{ proof *)
 908   [
 909   REWRITE_TAC[BIJ];
 910   REPEAT WEAKER_STRIP_TAC;
 911   SUBCONJ2_TAC;
 912     INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
 913     ANTS_TAC;
 914       BY(ASM_REWRITE_TAC[]);
 915     DISCH_THEN SUBST1_TAC;
 916     BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
 917   REWRITE_TAC[SURJ;INJ];
 918   REPEAT WEAKER_STRIP_TAC;
 919   ASM_REWRITE_TAC[];
 920   REWRITE_TAC[IN_ELIM_THM];
 921   REPEAT WEAKER_STRIP_TAC;
 922   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 923     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 924   TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC);
 925     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
 926   TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC);
 927     ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM];
 928     BY(ASM_MESON_TAC[]);
 929   INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA [];
 930   ASM_REWRITE_TAC[];
 931   DISCH_THEN MATCH_MP_TAC;
 932   BY(ASM_MESON_TAC[arith `x < n+1 /\ n < c==> x < c`])
 933  ]);;
 934   (* }}} *)
 935
 936 let CARD_SLICEV = prove_by_refinement(
 937   `!V E FF v w .
 938          convex_local_fan (V,E,FF) /\
 939          v IN V /\
 940          w IN V /\
 941          (!u u1.
 942               u IN {v, w} /\ u1 IN V /\ ~(u = u1)
 943               ==> ~collinear {vec 0, u, u1}) /\
 944          (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)
 945          ==> CARD (slicev E FF v w) + CARD(slicev E FF w v) = CARD V + 2`,
 946   (* {{{ proof *)
 947   [
 948   REPEAT WEAKER_STRIP_TAC;
 949   TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC);
 950     COMMENT "insert";
 951     TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
 952       BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
 953     MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT;
 954     TYPIFY `E` EXISTS_TAC;
 955     BY(ASM_REWRITE_TAC[]);
 956   REPEAT WEAKER_STRIP_TAC;
 957   INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
 958   ASM_REWRITE_TAC[];
 959   DISCH_TAC;
 960   INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
 961   ASM_REWRITE_TAC[];
 962   DISCH_TAC;
 963   TYPED_ABBREV_TAC  `f = (\j. ITER j (rho_node1 FF) v)` ;
 964   TYPIFY `CARD {j | j < n + 1} =  CARD (slicev E FF v (ITER n (rho_node1 FF) v))` (C SUBGOAL_THEN MP_TAC);
 965     MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD;
 966     ASM_REWRITE_TAC[FINITE_NUMSEG_LT];
 967     BY(ASM_MESON_TAC[]);
 968   DISCH_THEN (SUBST1_TAC o GSYM);
 969   TYPIFY `CARD {j | j =0 \/ ( n <= j /\ j < CARD V)} =  CARD (slicev E FF w v)` (C SUBGOAL_THEN MP_TAC);
 970     MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD;
 971     TYPIFY `f` EXISTS_TAC;
 972     CONJ2_TAC;
 973       BY(ASM_REWRITE_TAC[]);
 974     MATCH_MP_TAC FINITE_SUBSET;
 975     TYPIFY `{0} UNION {j | j < CARD V}` EXISTS_TAC;
 976     CONJ_TAC;
 977       MATCH_MP_TAC FINITE_UNION_IMP;
 978       BY(ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY;FINITE_NUMSEG_LT]);
 979     BY(SET_TAC[]);
 980   ASM_REWRITE_TAC[];
 981   DISCH_THEN (SUBST1_TAC o GSYM);
 982   REWRITE_TAC[CARD_NUMSEG_LT];
 983   TYPIFY `{j | j  = 0 \/ n <= j /\ j < CARD V } = {0} UNION {j | n <= j /\ j < CARD V}` (C SUBGOAL_THEN SUBST1_TAC);
 984     BY(SET_TAC[]);
 985   INTRO_TAC Geomdetail.CARD_EQUATION [`{0}`;`{j | n <= j /\ j < CARD V}`];
 986   ANTS_TAC;
 987     REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
 988     MATCH_MP_TAC FINITE_SUBSET;
 989     TYPIFY ` {j | j < CARD V}` EXISTS_TAC;
 990     ASM_REWRITE_TAC[FINITE_NUMSEG_LT];
 991     BY(SET_TAC[]);
 992   TYPIFY `({0} INTER {j | n <= j /\ j < CARD V}) = {}` (C SUBGOAL_THEN SUBST1_TAC);
 993     REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_SING;IN_ELIM_THM];
 994     TYPIFY `~(n=0)` ENOUGH_TO_SHOW_TAC;
 995       BY(ARITH_TAC);
 996     DISCH_TAC;
 997     FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC;
 998     ASM_REWRITE_TAC[ITER];
 999     INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
1000     DISCH_THEN MATCH_MP_TAC;
1001     BY(ASM_REWRITE_TAC[]);
1002   REWRITE_TAC[CARD_CLAUSES;arith `x + 0 = x`];
1003   DISCH_THEN SUBST1_TAC;
1004   REWRITE_TAC[Geomdetail.CARD_SING];
1005   TYPIFY `{j | n <= j /\  j < CARD V} = (n.. (CARD V - 1))` (C SUBGOAL_THEN SUBST1_TAC);
1006     REWRITE_TAC[EXTENSION;IN_NUMSEG;IN_ELIM_THM];
1007     BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC);
1008   REWRITE_TAC[CARD_NUMSEG];
1009   BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC)
1010   ]);;
1011   (* }}} *)
1012
1013 let HAFL_CIRCLE_FORM_LOCAL_FAN_ALT = prove_by_refinement(
1014   `!V E FF v w HS fv. (local_fan (V,E,FF) /\
1015       v IN V /\
1016       w IN V /\
1017       ~(v = w) /\
1018       (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\
1019       (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\
1020      HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1021      fv = face HS (v,rho_node1 FF v)
1022      ==> local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv)`,
1023   (* {{{ proof *)
1024   [
1025   REPEAT WEAKER_STRIP_TAC;
1026   INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN) [];
1027   DISCH_THEN MATCH_MP_TAC;
1028   GEXISTL_TAC [`HS`;`FF`];
1029   BY(ASM_MESON_TAC[])
1030   ]);;
1031   (* }}} *)
1032
1033 let HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT = prove_by_refinement(
1034   `!V E FF v w HS fv. (local_fan (V,E,FF) /\
1035       v IN V /\
1036       w IN V /\
1037       ~(v = w) /\
1038       (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\
1039       (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\
1040      HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1041      fv = face HS (v,rho_node1 FF v) /\
1042      fw = face HS (w,rho_node1 FF w)
1043      ==> local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\
1044          local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)`,
1045   (* {{{ proof *)
1046   [
1047   REPEAT WEAKER_STRIP_TAC;
1048   INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN2) [];
1049   DISCH_THEN MATCH_MP_TAC;
1050   GEXISTL_TAC [`HS`;`FF`];
1051   BY(ASM_MESON_TAC[])
1052   ]);;
1053   (* }}} *)
1054
1055 let CARD_SLICEF = prove_by_refinement(
1056   `!V E FF v w .
1057          convex_local_fan (V,E,FF) /\
1058          v IN V /\
1059          w IN V /\
1060          (!u u1.
1061               u IN {v, w} /\ u1 IN V /\ ~(u = u1)
1062               ==> ~collinear {vec 0, u, u1}) /\
1063          (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)
1064          ==> CARD (slicef E FF v w) + CARD(slicef E FF w v) = CARD FF + 2`,
1065   (* {{{ proof *)
1066   [
1067   REPEAT WEAKER_STRIP_TAC;
1068   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
1069   ANTS_TAC;
1070     BY(ASM_REWRITE_TAC[]);
1071   DISCH_TAC;
1072   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
1073   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
1074   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
1075   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1076   ASM_REWRITE_TAC[];
1077   REPEAT WEAKER_STRIP_TAC;
1078   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1079   ANTS_TAC;
1080     BY(ASM_REWRITE_TAC[]);
1081   REPEAT WEAKER_STRIP_TAC;
1082   ASM_REWRITE_TAC[];
1083   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
1084     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
1085   TYPIFY` local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\          local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN MP_TAC);
1086     MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
1087     GEXISTL_TAC [`FF`;`HS`];
1088     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
1089     BY(ASM_MESON_TAC[]);
1090   REPEAT WEAKER_STRIP_TAC;
1091   TYPIFY `FINITE FF /\ FINITE fv /\ FINITE fw` (C SUBGOAL_THEN ASSUME_TAC);
1092     BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]);
1093   REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP Local_lemmas.LOFA_IMP_BIJ_FF_V)));
1094   INTRO_TAC CARD_SLICEV [`V`;`E`;`FF`;`v`;`w`];
1095   ANTS_TAC;
1096     BY(ASM_REWRITE_TAC[]);
1097   ASM_REWRITE_TAC[];
1098   FIRST_X_ASSUM MP_TAC;
1099   BY(MESON_TAC[Local_lemmas.BIJ_IMP_CARD_EQ])
1100   ]);;
1101   (* }}} *)
1102
1103 let aff_ge_INTER_aff_lt = prove_by_refinement(
1104   `! (y:real^A). ~(y = vec 0) ==> aff_ge {vec 0} {y} INTER aff_lt {vec 0} {y} = {}`,
1105   (* {{{ proof *)
1106   [
1107   REPEAT WEAKER_STRIP_TAC;
1108   ASM_SIMP_TAC[AFF_GE_1_1_0];
1109   GMATCH_SIMP_TAC AFF_LT_1_1;
1110   REWRITE_TAC[DISJOINT;IN_SING;EXTENSION;IN_INTER;IN_ELIM_THM;NOT_IN_EMPTY];
1111   CONJ_TAC;
1112     BY(ASM_MESON_TAC[]);
1113   REPEAT WEAKER_STRIP_TAC;
1114   FIRST_X_ASSUM MP_TAC;
1115   ASM_REWRITE_TAC[];
1116   REWRITE_TAC[VECTOR_MUL_RZERO];
1117   REWRITE_TAC[varith `a % y = vec 0 + t2 % (y:real^A) <=> (a - t2) % y = vec 0`];
1118   ASM_REWRITE_TAC[VECTOR_MUL_EQ_0];
1119   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1120   ]);;
1121   (* }}} *)
1122
1123 let ejr_generic = prove_by_refinement(
1124   `!V E FF v w.
1125      convex_local_fan (V,E,FF) /\
1126      v IN V /\
1127      w IN V /\
1128      (!u u1.
1129           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
1130      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\
1131     generic V E
1132   ==> generic (slicev E FF v w) (slicee E FF v w)`,
1133   (* {{{ proof *)
1134   [
1135   REPEAT WEAKER_STRIP_TAC;
1136   REWRITE_TAC[generic];
1137   REPEAT WEAKER_STRIP_TAC;
1138   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
1139   ANTS_TAC;
1140     BY(ASM_REWRITE_TAC[]);
1141   DISCH_TAC;
1142   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
1143   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
1144   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
1145   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1146   ASM_REWRITE_TAC[];
1147   REPEAT WEAKER_STRIP_TAC;
1148   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1149   ANTS_TAC;
1150     BY(ASM_REWRITE_TAC[]);
1151   REPEAT WEAKER_STRIP_TAC;
1152   ASM_REWRITE_TAC[];
1153   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
1154     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
1155   TYPIFY `e_prime (E UNION {{v,w}}) fv SUBSET (E UNION {{v,w}})` (C SUBGOAL_THEN ASSUME_TAC);
1156     BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E]);
1157   TYPIFY `{v',w'} IN E \/ {v',w'} = {v,w}` (C SUBGOAL_THEN ASSUME_TAC);
1158     FIRST_X_ASSUM_ST `x IN slicee E FF v w` MP_TAC;
1159     ASM_REWRITE_TAC[];
1160     FIRST_X_ASSUM MP_TAC;
1161     REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
1162     BY(MESON_TAC[]);
1163   FIRST_X_ASSUM (DISJ_CASES_TAC);
1164     FIRST_X_ASSUM_ST `generic` MP_TAC;
1165     REWRITE_TAC[generic];
1166     DISCH_THEN MATCH_MP_TAC;
1167     BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]);
1168   FIRST_X_ASSUM (fun t -> REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[t]) THEN REPEAT WEAKER_STRIP_TAC;
1169   GMATCH_SIMP_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge;
1170   CONJ_TAC;
1171     FIRST_X_ASSUM MATCH_MP_TAC;
1172     BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
1173   REWRITE_TAC[GSYM SUBSET_EMPTY];
1174   MATCH_MP_TAC SUBSET_TRANS;
1175   TYPIFY `(aff_gt {vec 0} {v,w} INTER aff_lt {vec 0} {u}) UNION (aff_ge {vec 0} {v} INTER aff_lt {vec 0} {u}) UNION (aff_ge {vec 0} {w} INTER aff_lt {vec 0} {u})` EXISTS_TAC;
1176   CONJ_TAC;
1177     BY(SET_TAC[]);
1178   REWRITE_TAC[UNION_SUBSET;SUBSET_EMPTY];
1179   TYPIFY `u IN V` (C SUBGOAL_THEN ASSUME_TAC);
1180     BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]);
1181   TYPIFY `~(v = vec 0) /\ ~(w = vec 0) /\ ~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
1182     RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;Fan_defs.fan2;LET_DEF;LET_END_DEF]);
1183     BY(ASM_MESON_TAC[]);
1184   CONJ2_TAC;
1185     CONJ_TAC;
1186       PROOF_BY_CONTR_TAC;
1187       TYPIFY `collinear {vec 0,u,v}` (C SUBGOAL_THEN ASSUME_TAC);
1188         BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]);
1189       TYPIFY `u = v` ASM_CASES_TAC;
1190         BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]);
1191       BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]);
1192     PROOF_BY_CONTR_TAC;
1193     TYPIFY `collinear {vec 0,u,w}` (C SUBGOAL_THEN ASSUME_TAC);
1194       BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]);
1195     TYPIFY `u = w` ASM_CASES_TAC;
1196       BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]);
1197     BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]);
1198   TYPIFY `aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt (u,rho_node1 FF u) E /\ aff_lt {vec 0} {u} INTER wedge_in_fan_gt (u,rho_node1 FF u) E = {}` ENOUGH_TO_SHOW_TAC;
1199     BY(SET_TAC[]);
1200   CONJ_TAC;
1201     FIRST_X_ASSUM MATCH_MP_TAC;
1202     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]);
1203   REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
1204   GEN_TAC;
1205   GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_LOFA_DETER2;
1206   CONJ_TAC;
1207     BY(ASM_MESON_TAC[]);
1208   REWRITE_TAC[TAUT `~(a /\ b) <=> ( a ==> ~b)`];
1209   ASM_SIMP_TAC[Nkezbfc_local.AFF_LT_1_1;IN_ELIM_THM;wedge];
1210   REWRITE_TAC[VECTOR_MUL_RZERO;VECTOR_ADD_LID];
1211   REPEAT WEAKER_STRIP_TAC;
1212   ASM_REWRITE_TAC[];
1213   FIRST_X_ASSUM_ST `collinear` MP_TAC;
1214   ASM_REWRITE_TAC[];
1215   ASM_SIMP_TAC[Local_lemmas.COLLINEAR_ONCE_VEC_0];
1216   BY(MESON_TAC[])
1217   ]);;
1218   (* }}} *)
1219
1220 let LOFA_IMP_LT_CARD_SET_V_ALT = prove_by_refinement(
1221   `!V E FF v. local_fan (V,E,FF) /\ v IN V
1222          ==> {ITER n (rho_node1 FF) v | n < CARD V} = V`,
1223   (* {{{ proof *)
1224   [
1225     BY(MESON_TAC[Local_lemmas.LOFA_IMP_LT_CARD_SET_V])
1226   ]);;
1227   (* }}} *)
1228
1229 let ejr_sum = prove_by_refinement(
1230   `!V E FF HS v w f fv fw.
1231      convex_local_fan (V,E,FF) /\
1232      v IN V /\
1233      w IN V /\
1234      hypermap (HYP (vec 0,V,E UNION {{v, w}})) = HS /\
1235      face HS (v,rho_node1 FF v) = fv /\
1236      face HS (w,rho_node1 FF w) = fw /\
1237       (!u u1.
1238           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
1239      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)  // /\
1240      ==> sum FF (\e. f (FST e) * azim_in_fan e E) =
1241          sum fv
1242          (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{v, w}}) fv)) +
1243          sum fw
1244          (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{w, v}}) fw))`,
1245   (* {{{ proof *)
1246   [
1247   REPEAT WEAKER_STRIP_TAC;
1248   REWRITE_TAC[generic];
1249   REPEAT WEAKER_STRIP_TAC;
1250   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
1251   ANTS_TAC;
1252     BY(ASM_REWRITE_TAC[]);
1253   DISCH_TAC;
1254   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1255   ASM_REWRITE_TAC[];
1256   REPEAT WEAKER_STRIP_TAC;
1257   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1258   ANTS_TAC;
1259     BY(ASM_REWRITE_TAC[]);
1260   REPEAT WEAKER_STRIP_TAC;
1261   ASM_REWRITE_TAC[];
1262   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
1263     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
1264   TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC);
1265     MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT;
1266     TYPIFY `E` EXISTS_TAC;
1267     BY(ASM_REWRITE_TAC[]);
1268   REPEAT WEAKER_STRIP_TAC;
1269   FIRST_X_ASSUM (C INTRO_TAC [`(\i. f (ITER i (rho_node1 FF) v))`]);
1270   REWRITE_TAC[];
1271   COMMENT "replace first index set";
1272   TYPIFY `{i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fv } = {i | i < n + 1}` (C SUBGOAL_THEN SUBST1_TAC);
1273     INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
1274     ANTS_TAC;
1275       BY(ASM_MESON_TAC[]);
1276     ASM_REWRITE_TAC[];
1277     DISCH_THEN SUBST1_TAC;
1278     REWRITE_TAC[IN_IMAGE;IN_ELIM_THM];
1279     REWRITE_TAC[EXTENSION;IN_ELIM_THM];
1280     X_GEN_TAC `i:num`;
1281     REWRITE_TAC[Geomdetail.EQ_EXPAND];
1282     CONJ2_TAC;
1283       REPEAT WEAKER_STRIP_TAC;
1284       SUBCONJ_TAC;
1285         BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
1286       DISCH_TAC;
1287       TYPIFY `i` EXISTS_TAC;
1288       BY(ASM_REWRITE_TAC[]);
1289     REPEAT WEAKER_STRIP_TAC;
1290     TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC;
1291       BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
1292     BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA;arith `x' < n+1 /\ n < c ==> x' < c`]);
1293   COMMENT "n not 0";
1294   TYPIFY `~(n=0)` (C SUBGOAL_THEN ASSUME_TAC);
1295     DISCH_TAC;
1296     FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC;
1297     BY(ASM_REWRITE_TAC[ITER]);
1298   COMMENT "replace second index set";
1299   TYPIFY `{i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fw } = {i | i = 0 \/ n <= i /\ i < CARD V}` (C SUBGOAL_THEN SUBST1_TAC);
1300     INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`];
1301     ANTS_TAC;
1302       BY(ASM_MESON_TAC[]);
1303     ASM_REWRITE_TAC[];
1304     DISCH_THEN SUBST1_TAC;
1305     REWRITE_TAC[IN_IMAGE;IN_ELIM_THM];
1306     REWRITE_TAC[EXTENSION;IN_ELIM_THM];
1307     X_GEN_TAC `i:num`;
1308     REWRITE_TAC[Geomdetail.EQ_EXPAND];
1309     CONJ2_TAC;
1310       REPEAT WEAKER_STRIP_TAC;
1311       SUBCONJ_TAC;
1312         BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
1313       DISCH_TAC;
1314       TYPIFY `i` EXISTS_TAC;
1315       BY(ASM_REWRITE_TAC[]);
1316     REPEAT WEAKER_STRIP_TAC;
1317     TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC;
1318       BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC);
1319     TYPIFY `x' < CARD V` (C SUBGOAL_THEN MP_TAC);
1320       BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
1321     BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]);
1322   MATCH_MP_TAC (arith `(a = a' /\ b = b' /\ c = c') ==> (a = b + c ==> a' = b' + c')`);
1323   COMMENT "match summands";
1324   TYPIFY `!fu. ((\u. f u * interior_angle1 (vec 0) fu u) o (\i. ITER i (rho_node1 FF) v)) = (\i. f (ITER i (rho_node1 FF) v) *           interior_angle1 (vec 0) fu (ITER i (rho_node1 FF) v))` (C SUBGOAL_THEN ASSUME_TAC);
1325     BY(REWRITE_TAC[FUN_EQ_THM;o_THM]);
1326   COMMENT "first sum";
1327   CONJ_TAC;
1328     TYPIFY `BIJ (\i. (ITER i (rho_node1 FF) v)) {i | i < CARD V} V` (C SUBGOAL_THEN ASSUME_TAC);
1329       REWRITE_TAC[BIJ];
1330       SUBCONJ2_TAC;
1331         TYPIFY `IMAGE (\i.  (ITER i (rho_node1 FF) v)) {i | i < CARD V} = V` ENOUGH_TO_SHOW_TAC;
1332           BY(MESON_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]);
1333         INTRO_TAC LOFA_IMP_LT_CARD_SET_V_ALT [`V`;`E`;`FF`;`v`];
1334         ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE];
1335         BY(MESON_TAC[]);
1336       REWRITE_TAC[SURJ;INJ];
1337       DISCH_TAC;
1338       ASM_REWRITE_TAC[];
1339       ASM_REWRITE_TAC[IN_ELIM_THM];
1340       BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]);
1341     FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1342     DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) FF u`]);
1343     ASM_REWRITE_TAC[];
1344     DISCH_THEN SUBST1_TAC;
1345     TYPIFY `BIJ FST FF V` (C SUBGOAL_THEN ASSUME_TAC);
1346       MATCH_MP_TAC WRGCVDR_BIJ;
1347       BY(ASM_MESON_TAC[]);
1348     FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1349     DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) FF u`]);
1350     DISCH_THEN (SUBST1_TAC o GSYM);
1351     MATCH_MP_TAC SUM_EQ;
1352     REWRITE_TAC[o_THM];
1353     GEN_TAC;
1354     DISCH_TAC;
1355     TYPIFY `FST x IN V` ENOUGH_TO_SHOW_TAC;
1356       DISCH_TAC;
1357       AP_TERM_TAC;
1358       BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
1359     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]);
1360   COMMENT "prep for slice cases";
1361   TYPIFY `local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\ local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN ASSUME_TAC);
1362     MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
1363     GEXISTL_TAC [`FF`;`HS`];
1364     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
1365     BY(ASM_MESON_TAC[]);
1366   COMMENT "second sum";
1367   CONJ_TAC;
1368     INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
1369     ANTS_TAC;
1370       BY(ASM_REWRITE_TAC[]);
1371     DISCH_TAC;
1372     FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1373     DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fv u`]);
1374     ASM_REWRITE_TAC[];
1375     DISCH_THEN SUBST1_TAC;
1376     TYPIFY `BIJ FST fv (v_prime V fv)` (C SUBGOAL_THEN ASSUME_TAC);
1377       MATCH_MP_TAC WRGCVDR_BIJ;
1378       BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1379     FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1380     DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fv u`]);
1381     DISCH_THEN (SUBST1_TAC o GSYM);
1382     MATCH_MP_TAC SUM_EQ;
1383     REWRITE_TAC[o_THM];
1384     REPEAT WEAKER_STRIP_TAC;
1385     TYPIFY `FST x IN v_prime V fv` ENOUGH_TO_SHOW_TAC;
1386       DISCH_TAC;
1387       AP_TERM_TAC;
1388       BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
1389     BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]);
1390   COMMENT "last case";
1391   INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`];
1392   ANTS_TAC;
1393     BY(ASM_REWRITE_TAC[]);
1394   DISCH_TAC;
1395   FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1396   DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fw u`]);
1397   ASM_REWRITE_TAC[];
1398   DISCH_THEN SUBST1_TAC;
1399   TYPIFY `BIJ FST fw (v_prime V fw)` (C SUBGOAL_THEN ASSUME_TAC);
1400     MATCH_MP_TAC WRGCVDR_BIJ;
1401     BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1402   FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM));
1403   DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fw u`]);
1404   DISCH_THEN (SUBST1_TAC o GSYM);
1405   MATCH_MP_TAC SUM_EQ;
1406   REWRITE_TAC[o_THM];
1407   REPEAT WEAKER_STRIP_TAC;
1408   TYPIFY `FST x IN v_prime V fw` ENOUGH_TO_SHOW_TAC;
1409     DISCH_TAC;
1410     AP_TERM_TAC;
1411     BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]);
1412   BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2])
1413   ]);;
1414   (* }}} *)
1415
1416 let EJRCFJD_ALT2 = prove_by_refinement(
1417  `!V E FF v w.
1418      convex_local_fan (V,E,FF) /\
1419      v IN V /\
1420      w IN V /\
1421      (!u u1.
1422           u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\
1423      (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E)
1424      ==> convex_local_fan (slicev E FF v w,slicee E FF v w,slicef E FF v w) /\
1425          convex_local_fan (slicev E FF w v,slicee E FF w v,slicef E FF w v) /\
1426          tau_fun V E FF >=
1427          tau_fun (slicev E FF v w) (slicee E FF v w) (slicef E FF v w) +
1428          tau_fun (slicev E FF w v) (slicee E FF w v) (slicef E FF w v) /\
1429          sol_local E FF =
1430          sol_local (slicee E FF v w) (slicef E FF v w) +
1431          sol_local (slicee E FF w v) (slicef E FF w v) /\
1432          CARD (slicev E FF v w) < CARD V /\
1433          CARD (slicev E FF w v) < CARD V /\
1434          (generic V E
1435           ==> generic (slicev E FF v w) (slicee E FF v w) /\
1436               generic (slicev E FF w v) (slicee E FF w v))`,
1437   (* {{{ proof *)
1438   [
1439   REPEAT WEAKER_STRIP_TAC;
1440   INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`];
1441   ANTS_TAC;
1442     BY(ASM_REWRITE_TAC[]);
1443   DISCH_TAC;
1444   TYPED_ABBREV_TAC  `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ;
1445   TYPED_ABBREV_TAC  `fv = face HS (v,rho_node1 FF v)` ;
1446   TYPED_ABBREV_TAC  `fw = face HS (w,rho_node1 FF w)` ;
1447   INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1448   ASM_REWRITE_TAC[];
1449   REPEAT WEAKER_STRIP_TAC;
1450   ASM_REWRITE_TAC[];
1451   INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`];
1452   ANTS_TAC;
1453     BY(ASM_REWRITE_TAC[]);
1454   REPEAT WEAKER_STRIP_TAC;
1455   ASM_REWRITE_TAC[];
1456   TYPIFY `CARD (v_prime V fv) < CARD V /\ CARD (v_prime V fw) < CARD V` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1457     REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `v_prime` (SUBST1_TAC o GSYM));
1458     CONJ_TAC;
1459       MATCH_MP_TAC CARD_SLICEV_LT;
1460       BY(ASM_REWRITE_TAC[]);
1461     MATCH_MP_TAC CARD_SLICEV_LT;
1462     ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
1463     ASM_REWRITE_TAC[];
1464     BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
1465   TYPIFY `(generic V E  ==> generic (v_prime V fv) (e_prime (E UNION {{v, w}}) fv) /\      generic (v_prime V fw) (e_prime (E UNION {{w, v}}) fw))` (C SUBGOAL_THEN (unlist REWRITE_TAC));
1466     DISCH_TAC;
1467     CONJ_TAC;
1468       INTRO_TAC ejr_generic [`V`;`E`;`FF`;`v`;`w`];
1469       ANTS_TAC;
1470         BY(ASM_REWRITE_TAC[]);
1471       BY(ASM_MESON_TAC[]);
1472     INTRO_TAC ejr_generic [`V`;`E`;`FF`;`w`;`v`];
1473     ANTS_TAC;
1474       ASM_REWRITE_TAC[];
1475       ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
1476       ASM_REWRITE_TAC[];
1477       BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
1478     BY(ASM_MESON_TAC[]);
1479   COMMENT "now tau and sol";
1480   REWRITE_TAC[sol_local;tau_fun];
1481   TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
1482     BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]);
1483   TYPIFY` local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\          local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw)` (C SUBGOAL_THEN MP_TAC);
1484     MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT;
1485     GEXISTL_TAC [`FF`;`HS`];
1486     ASM_REWRITE_TAC[IN_DIFF;IN_SING];
1487     BY(ASM_MESON_TAC[]);
1488   REPEAT WEAKER_STRIP_TAC;
1489   COMMENT "insert";
1490   TYPIFY ` CARD FF + 2 = CARD fv + CARD fw` (C SUBGOAL_THEN ASSUME_TAC);
1491     COMMENT "cut insert to here";
1492     INTRO_TAC CARD_SLICEF [`V`;`E`;`FF`;`v`;`w`];
1493     ANTS_TAC;
1494       BY(ASM_REWRITE_TAC[]);
1495     ASM_REWRITE_TAC[];
1496     DISCH_THEN SUBST1_TAC;
1497     BY(REWRITE_TAC[]);
1498   COMMENT "tau sum";
1499   INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`rho_fun o (norm: (real^3-> real))`;` fv`;` fw`];
1500   ANTS_TAC;
1501     BY(ASM_REWRITE_TAC[]);
1502   REWRITE_TAC[o_THM];
1503   DISCH_THEN SUBST1_TAC;
1504   CONJ_TAC;
1505     MATCH_MP_TAC (arith `c1 = c2 + c3 ==> ((a + b) - c1 >= a - c2 + b - c3)`);
1506     REWRITE_TAC[arith `a * b + a * c = a * (b + c)`];
1507     AP_TERM_TAC;
1508     REWRITE_TAC[REAL_OF_NUM_ADD];
1509     REWRITE_TAC[REAL_OF_NUM_EQ];
1510     TYPIFY `(2 <= CARD FF /\ 2 <= CARD fv /\ 2 <= CARD fw) /\ CARD FF + 2 = CARD fv + CARD fw` ENOUGH_TO_SHOW_TAC;
1511       BY(ARITH_TAC);
1512     ASM_REWRITE_TAC[];
1513     GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ;
1514     TYPIFY`V` EXISTS_TAC;
1515     CONJ_TAC;
1516       BY(ASM_MESON_TAC[]);
1517     CONJ_TAC;
1518       MATCH_MP_TAC Hypermap.CARD_ATLEAST_2;
1519       GEXISTL_TAC [`v`;`w`];
1520       ASM_REWRITE_TAC[];
1521       BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
1522     REPEAT (GMATCH_SIMP_TAC (arith `2 < x ==> 2 <= x`));
1523     REPEAT (GMATCH_SIMP_TAC (Local_lemmas1.LOFA_HYP_UNION_CARD_GT2));
1524     REWRITE_TAC[IN_DIFF;IN_SING];
1525     CONJ_TAC;
1526       GEXISTL_TAC [`V`;`E`;`w`;`HS`;`FF`;`v`];
1527       BY(ASM_MESON_TAC[]);
1528     GEXISTL_TAC [`V`;`E`;`v`;`HS`;`FF`;`w`];
1529     ASM_REWRITE_TAC[];
1530     ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
1531     ASM_REWRITE_TAC[];
1532     BY(ASM_MESON_TAC[Collect_geom.PER_SET3]);
1533   COMMENT "final sum";
1534   INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`\ (v:real^3). &1`;` fv`;` fw`];
1535   ANTS_TAC;
1536     BY(ASM_REWRITE_TAC[]);
1537   REWRITE_TAC[o_THM;arith `&1 * x = x`];
1538   TYPIFY `FINITE fv /\ FINITE fw /\ FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
1539     BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]);
1540   ASM_SIMP_TAC[SUM_SUB];
1541   ASM_SIMP_TAC[SUM_CONST];
1542   DISCH_THEN kill;
1543   MATCH_MP_TAC (arith `cf + t2 = cv + c2 ==>t2 + (tv + tw) - cf = (t2 + tv - cv) + (t2 + tw - c2)`);
1544   MATCH_MP_TAC (arith `cf + &2 = cv + cw ==> cf * pi + &2 * pi = cv * pi + cw * pi`);
1545   REWRITE_TAC[REAL_OF_NUM_ADD];
1546   REWRITE_TAC[REAL_OF_NUM_EQ];
1547   BY(ASM_REWRITE_TAC[])
1548   ]);;
1549   (* }}} *)
1550
1551 let NKEZBFC = prove_by_refinement(
1552   `!V E FF. convex_local_fan(V,E,FF) /\ generic V E
1553   ==> &0 <= sol_local E FF`,
1554   (* {{{ proof *)
1555   [
1556   REPEAT WEAKER_STRIP_TAC;
1557   MP_TAC Nkezbfc_local.NKEZBFC_PREP;
1558   ANTS_TAC;
1559     BY(REWRITE_TAC[EJRCFJD_ALT2 ]);
1560   BY(ASM_MESON_TAC[])
1561   ]);;
1562   (* }}} *)
1563
1564 let azim_dart_azim_in_fan = prove_by_refinement(
1565   `!V E x. FAN((vec 0),V,E) /\ ({FST x,SND x} IN E)
1566     ==> azim_dart (V,E) x = azim_in_fan x E`,
1567   (* {{{ proof *)
1568   [
1569   REWRITE_TAC[FORALL_PAIR_THM;FST;SND];
1570   REWRITE_TAC[Fan_defs.azim_dart;(* L *)azim_in_fan;Fan_defs.azim_fan];
1571   REPEAT WEAKER_STRIP_TAC;
1572   ASM_REWRITE_TAC[LET_DEF;LET_END_DEF];
1573   TYPIFY `~(p1 = p2)` (C SUBGOAL_THEN ASSUME_TAC);
1574     DISCH_TAC;
1575     RULE_ASSUM_TAC (REWRITE_RULE[Fan.FAN;Fan.graph]);
1576     REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
1577     FIRST_X_ASSUM (C INTRO_TAC [`{p1,p2}`]);
1578     REWRITE_TAC[Local_lemmas1.SET2_HAS_SIZE2];
1579     BY(ASM_MESON_TAC[IN]);
1580   ASM_SIMP_TAC[GSYM (* L *)EE_elim];
1581   COND_CASES_TAC THEN ASM_REWRITE_TAC[];
1582   GMATCH_SIMP_TAC Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN;
1583   TYPIFY `V` EXISTS_TAC;
1584   ASM_REWRITE_TAC[];
1585   ASM_SIMP_TAC[GSYM (* L *)EE_elim];
1586   BY(ASM_REWRITE_TAC[(* L *)EE;IN_ELIM_THM])
1587   ]);;
1588   (* }}} *)
1589
1590 let rho_fun = new_definition `rho_fun y =  &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
1591
1592 let rho_rho_fun = prove_by_refinement(
1593   `!y. rho_fun y = rho y`,
1594   (* {{{ proof *)
1595   [
1596   REWRITE_TAC[Sphere.rho;rho_fun;Sphere.const1;Sphere.ly;Sphere.interp];
1597   REWRITE_TAC[GSYM Nonlinear_lemma.sol0_EQ_sol_y;Sphere.h0];
1598   REWRITE_TAC[arith `a + b = a + c <=> c = b`];
1599   GEN_TAC;
1600   MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`);
1601   AP_TERM_TAC;
1602   BY(REAL_ARITH_TAC)
1603   ]);;
1604   (* }}} *)
1605
1606 let h_dart = new_definition `h_dart (x:real^3#B) = norm (FST x)  / &2`;;
1607
1608 let tauVEF = new_definition `tauVEF (V,E,f) =
1609   sum f ( \ x. azim_dart (V,E) x * (&1 + (sol0/pi) * (&1 - lmfun (h_dart x))))   + (pi + sol0)*(&2 - &(CARD(f)))`;;
1610
1611 let tau_fun = new_definition `tau_fun V E f =  sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
1612
1613 let ly_EQ_lmfun = prove(`!x:real^3#real^3. norm (FST x) <= &2 * h0 ==> lmfun (h_dart x) = ly (norm (FST x))`,
1614    REWRITE_TAC[Pack_defs.lmfun; Sphere.ly; Sphere.interp; h_dart; Pack_defs.h0] THEN
1615      REAL_ARITH_TAC);;
1616
1617 let tauVEF_tau_fun = prove_by_refinement(
1618   `!V E f. FAN ((vec 0),V,E) /\
1619     2 <= CARD f /\
1620     (!x. x IN f ==> norm(FST x) <= &2 * h0) /\
1621     (!x. x IN f ==> {FST x,SND x} IN E)
1622   ==> tau_fun V E f = tauVEF (V,E,f)`,
1623   (* {{{ proof *)
1624   [
1625   REPEAT WEAKER_STRIP_TAC;
1626   REWRITE_TAC[tauVEF;tau_fun];
1627   GMATCH_SIMP_TAC (GSYM REAL_OF_NUM_SUB);
1628   ASM_REWRITE_TAC[];
1629   REWRITE_TAC[arith `x - u * (v - w) = x' + u * (w - v) <=> x = x'`];
1630   MATCH_MP_TAC SUM_EQ;
1631   REPEAT WEAKER_STRIP_TAC;
1632   REWRITE_TAC[];
1633   MATCH_MP_TAC (arith `x = x' /\ y = y' ==> x*y' = y*x'`);
1634   REWRITE_TAC[rho_rho_fun;Sphere.rho;Nonlinear_lemma.sol0_over_pi_EQ_const1];
1635   CONJ_TAC;
1636     MATCH_MP_TAC (arith `(l = l') ==> &1 + c - c * l = &1 + c *(&1 - l')`);
1637     BY(ASM_SIMP_TAC[ly_EQ_lmfun]);
1638   GMATCH_SIMP_TAC azim_dart_azim_in_fan;
1639   BY(ASM_SIMP_TAC[])
1640   ]);;
1641   (* }}} *)
1642
1643
1644  end;;