(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Introduction                                                      *)
(* Chapter: Local Fan                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-02-18                                                           *)
(* ========================================================================== *)

(*
Various odds and ends from the first part of the Local fan chapter
*)

module Localization = struct

  open Hales_tactic;;

parse_as_infix("has_orders",(12,"right"));;
parse_as_infix("cyclic_on",(13,"right"));;

let has_orders = new_definition ` (f: A -> A) has_orders k <=>
(! i. 0 < i /\ i < k ==> ~( ITER i f = I )) /\
ITER k f = I `;;
let order = new_definition ` order f x y = (@n. ITER n f x =y /\ (!i. 0< i /\ i< n ==> ~(ITER i f x= y)))`;;
let cyclic_on = new_definition` f cyclic_on (S:A -> bool) <=>
(! x. x IN S ==> S = {z | ?n. z = ITER n f x }) `;;
let dih2k = new_definition` dih2k (H: (A) hypermap) k <=> 
CARD (dart H) = 2 * k
/\ (! x. x IN (dart H) ==> let S = face H x in 
         dart H = S UNION (IMAGE (node_map H) S ))
/\ (face_map H ) has_orders k /\
(edge_map H ) has_orders 2 /\
(node_map H) has_orders 2 `;;
let EE = new_definition` EE v S = {w | {v,w} IN S }`;;
let ord_pairs = new_definition` ord_pairs E = { a,b | {a,b} IN E } `;;
let self_pairs = new_definition` self_pairs E V = { (v,v) | v IN V /\
 EE v E = {} } `;;
let darts_of_hyp = new_definition` darts_of_hyp E V = ord_pairs E UNION 
self_pairs E V `;;
let ee_of_hyp = new_definition` ee_of_hyp (x,V,E) ((a:real^3),(b:real^3)) = 
if (a,b) IN darts_of_hyp E V then (b,a) else (a,b)`;;
let nn_of_hyp = new_definition` nn_of_hyp (x,V,E) (v,u) =
if (v,u) IN darts_of_hyp E V then
(v, azim_cycle (EE v E) x v u) else (v,u)`;;
let ivs_azim_cycle = new_definition`ivs_azim_cycle W v0 v w =
if W = {} then w else 
(@x. x IN W /\ azim_cycle W v0 v x = w ) `;;
let ff_of_hyp = new_definition` ff_of_hyp (x,V,E) (v,u) =
if (v,u) IN darts_of_hyp E V then
(u, ivs_azim_cycle (EE u E) x u  v) else (v,u)`;;
let HYP = new_definition` HYP (x,V,E) = (darts_of_hyp E V,
ee_of_hyp (x,V,E), nn_of_hyp (x,V,E), ff_of_hyp (x,V,E)) `;;
let local_fan = new_definition ` local_fan (V,E,FF ) <=>
 let H = hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) in
  FAN (vec 0, V, E) /\
  (?x. x IN ( dart H) /\ FF = face H x ) /\
dih2k H (CARD FF ) `;;
let rho_node1 = new_definition `!(v:real^3) FF. rho_node1 FF v = (@w. v,w IN FF)`;;
let azim_in_fan = new_definition` azim_in_fan (v:real^3,w:real^3) E = 
let d = (azim_cycle (EE v E) ( vec 0 ) v w) in
 if CARD ( EE v E ) > 1 then 
 azim (vec 0 ) v w d else &2 * pi `;;
let wedge_in_fan_gt = new_definition`wedge_in_fan_gt (v,w) E = 
  if CARD (EE v E) > 1 then
wedge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else if 
EE v E = {w} then { x | ~ ( x IN aff_ge {vec 0, v} {w} ) } else
{ x | ~ ( x IN aff {vec 0, v} )} `;;
let wedge_ge = new_definition `wedge_ge  v0 v1 w1 w2 = { z |
&0 <= azim v0 v1 w1 z /\ azim v0 v1 w1 z <= azim v0 v1 w1 w2 }`;;
let wedge_in_fan_ge = new_definition` wedge_in_fan_ge ((v:real^3),w) E = 
  if CARD (EE v E) > 1 then
wedge_ge (vec 0) v w (azim_cycle (EE v E) (vec 0 ) v w ) else { x:real^3 | T } `;;
let convex_local_fan = new_definition
  `convex_local_fan (V,E,FF) <=>
   local_fan (V,E,FF) /\
   (!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E)`;;
let v_prime = new_definition `v_prime V FF = {v| v IN V /\
 (?w. (v,w) IN FF )} `;;
let e_prime = new_definition ` e_prime E FF = {{v,w} | {v,w} IN E /\ 
(v,w) IN FF } `;;
let generic = new_definition` generic V E <=>
(! v w u. {v,w} IN E /\ u IN V ==> aff_ge { vec 0 } {v,w} INTER 
aff_lt {vec 0} {u} = {} )`;;
let circular = new_definition ` circular V E <=> 
(? v w u. {v,w} IN E /\ u IN V /\ ~(aff_gt { vec 0 } {v,w} INTER 
aff_lt {vec 0} {u} = {}) )`;;
let lunar = new_definition
` lunar (v,w) V E <=> ~(circular V E) /\ {v,w} SUBSET V /\
~( v = w ) /\ collinear {vec 0, v, w } `;;
let rho_node1 = new_definition ` rho_node1 (FF:real^3 # real^3 -> bool) v = (@w. (v,w) IN FF)`;;
let ivs_rho_node1 = new_definition ` ivs_rho_node1 (FF:real^3 # real^3 -> bool) v = (@a. a,v IN FF )`;;
let interior_angle1 = new_definition
` interior_angle1 x FF v = azim x v (rho_node1 FF v) (@a. a,v IN FF)`;;
let sol_local = new_definition ` sol_local E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
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)`;;
let deformation = new_definition 
` deformation ff V (a,b) <=> (&0) IN real_interval (a,b) /\
(! v r. v IN V /\ r IN real_interval (a,b) ==> (ff v) continuous atreal r) /\
(!v. v IN V ==> ff v (&0) = v )`;;
let localization = new_definition `localization (V, E) FF = (v_prime V FF, e_prime E FF) `;;
let a_ear0=new_definition`a_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 (if {i  MOD 3,j MOD 3} IN J then sqrt(&8) else &2)) `;;
let b_ear0=new_definition`b_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
 (if {i  MOD 3,j MOD 3} IN J then cstab else &2* h0)) `;;
let JNVXCRC = new_definition
 `polar_fan(V,(E:(real^3->bool)->bool),FF) =
        let r = rho_node1 FF in
        let prime = \v. v cross (r v) in
        ({ prime v | v IN V},
         { {prime v,prime(r v)} | v IN V},
         { (prime v,prime(r v)) | v IN V})`;;
(* deprecated: let v_slice = new_definition ` v_slice f (v,w) = { ITER i f v | ! j. j < i ==> ~( ITER j f v = w ) }`;; let e_slice = new_definition ` e_slice f (v,w) = {w,v} INSERT { {ITER i f v, ITER (i + 1) f v} | ! j. j < i + 1 ==> ~( ITER j f v = w)} `;; let f_slice = new_definition ` f_slice f (v,w) = (w,v) INSERT { (ITER i f v, ITER (i + 1) f v) | ! j. j < i + 1 ==> ~ (ITER j f v = w)} `;; *)
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}`;;
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}}`;;
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)}`;;
let FAN_EDGE_SUBSET_V = 
prove_by_refinement( `!V E e. FAN(vec 0, V, E) /\ e IN E ==> e SUBSET V`,
(* {{{ proof *) [ REWRITE_TAC[Fan_defs.FAN;UNIONS_SUBSET]; BY(MESON_TAC[]) ]);;
(* }}} *)
let FAN_EDGE_EL_V = 
prove_by_refinement( `!V E u v. FAN(vec 0,V,E) /\ {u,v} IN E ==> v IN V`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `v IN {u,v}` (C SUBGOAL_THEN ASSUME_TAC); BY(SET_TAC[]); BY(ASM_MESON_TAC[FAN_EDGE_SUBSET_V;SUBSET]) ]);;
(* }}} *) (* renamed from FAN_EE, EE_EQ_set_of_edge *)
let EE_elim = 
prove_by_refinement( `!V E (v:real^3). FAN(vec 0,V,E) ==> EE v E = set_of_edge v V E`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[EE;Fan_defs.set_of_edge]; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; BY(ASM_MESON_TAC[FAN_EDGE_EL_V]) ]);;
(* }}} *) (* renamed from darts_of_hyp_EQ_dart_of_fan *)
let darts_of_hyp_elim = 
prove_by_refinement( `!V E. FAN(vec 0,V,E) ==> darts_of_hyp E V = dart_of_fan (V,E)`,
(* {{{ proof *) [ REWRITE_TAC[darts_of_hyp;Fan_defs.dart_of_fan;ord_pairs;self_pairs;SUBSET]; REPEAT WEAKER_STRIP_TAC; ASM_SIMP_TAC[GSYM EE_elim]; BY(SET_TAC[]) ]);;
(* }}} *)
let dart_of_fan_eq = 
prove_by_refinement( `!V E. dart_of_fan (V,E) = dart1_of_fan (V,E) UNION {v,v | v IN V /\ set_of_edge v V E = {}}`,
(* {{{ proof *) [ REWRITE_TAC[Fan_defs.dart_of_fan;EXTENSION;IN_UNION;Fan_defs.dart1_of_fan]; BY(SET_TAC[]) ]);;
(* }}} *) (* renamed from ee_of_hyp_EQ_e_fan_pair_ext *)
let ee_of_hyp_elim = 
prove_by_refinement( `!V E (x:A). FAN(vec 0,V,E) ==> ee_of_hyp(x,V,E) = e_fan_pair_ext(V,E)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM]; REWRITE_TAC[ee_of_hyp;Fan_defs.e_fan_pair_ext;Fan_defs.e_fan_pair]; ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ]; REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; COND_CASES_TAC; BY(ASM_REWRITE_TAC[]); BY(REWRITE_TAC[]) ]);;
(* }}} *)
let AZIM_CYCLE_EQ_SIGMA_FAN_ALT = 
prove_by_refinement( `!V E u v. FAN (vec 0,V,E) /\ u IN set_of_edge v V E ==> azim_cycle (set_of_edge v V E) (vec 0) v u = sigma_fan (vec 0) V E v u`,
(* {{{ proof *) [ BY(ASM_MESON_TAC[EE_elim;Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN]) ]);;
(* }}} *) (* renamed from nn_of_hyp_EQ_n_fan_pair_ext : *)
let nn_of_hyp_elim = 
prove_by_refinement( `!V E. FAN(vec 0,V,E) ==> nn_of_hyp((vec 0),V,E) = n_fan_pair_ext(V,E)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM]; REWRITE_TAC[nn_of_hyp;Fan_defs.n_fan_pair_ext;Fan_defs.n_fan_pair]; ASM_SIMP_TAC[EE_elim;darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ]; REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC; (ASM_REWRITE_TAC[PAIR_EQ]); GMATCH_SIMP_TAC AZIM_CYCLE_EQ_SIGMA_FAN_ALT; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[Fan_defs.dart1_of_fan;Fan_defs.set_of_edge]; REWRITE_TAC[IN_ELIM_PAIR_THM]; REWRITE_TAC[IN_ELIM_THM]; BY(ASM_MESON_TAC[FAN_EDGE_EL_V]); ASM_REWRITE_TAC[]; TYPIFY`~(p1 = p2)` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM (ASSUME_TAC o (REWRITE_RULE[])); ASM_REWRITE_TAC[]; COND_CASES_TAC; ASM_REWRITE_TAC[PAIR_EQ]; INTRO_TAC Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE [`{}:real^3->bool`;`p2`]; ANTS_TAC; BY(SET_TAC[]); BY(MESON_TAC[]); BY(REWRITE_TAC[]) ]);;
(* }}} *) (* renamed from ivs_azim_cycle_EQ_inverse_sigma_fan *)
let ivs_azim_cycle_elim = 
prove_by_refinement( `!V E p1 p2. FAN(vec 0,V,E) /\ {p1,p2} IN E ==> ivs_azim_cycle (set_of_edge p1 V E) (vec 0) p1 p2 = inverse_sigma_fan (vec 0) V E p1 p2`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ASM_SIMP_TAC[GSYM Fan_misc.INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN]; ASM_SIMP_TAC[ (GSYM Wrgcvdr_cizmrrh.IVS_AZIM_EQ_INVERSE_SIGMA_FAN)]; BY(ASM_MESON_TAC[EE_elim]) ]);;
(* }}} *) (* renamed from ff_of_hyp_EQ_f_fan_pair_ext: *)
let ff_of_hyp_elim = 
prove_by_refinement( `!V E. FAN(vec 0,V,E) ==> ff_of_hyp(vec 0,V,E) = f_fan_pair_ext(V,E)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[FUN_EQ_THM;FORALL_PAIR_THM]; REWRITE_TAC[ff_of_hyp;Fan_defs.f_fan_pair_ext;Fan_defs.f_fan_pair]; ASM_SIMP_TAC[darts_of_hyp_elim;dart_of_fan_eq;IN_UNION;IN_ELIM_THM;PAIR_EQ]; REWRITE_TAC[TAUT `a /\ b /\ c <=> (a /\ b) /\ c`;Misc_defs_and_lemmas.GSPEC_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `p1,p2 IN dart1_of_fan(V,E)` ASM_CASES_TAC; (ASM_REWRITE_TAC[PAIR_EQ]); ASM_SIMP_TAC[EE_elim]; GMATCH_SIMP_TAC ivs_azim_cycle_elim; ASM_REWRITE_TAC[]; RULE_ASSUM_TAC (REWRITE_RULE[Fan_defs.dart1_of_fan;IN_ELIM_PAIR_THM]); BY(ASM_MESON_TAC[Collect_geom.PER_SET2]); ASM_REWRITE_TAC[]; COND_CASES_TAC THEN REWRITE_TAC[]; ASM_REWRITE_TAC[PAIR_EQ]; ASM_SIMP_TAC[EE_elim]; BY(REWRITE_TAC[Wrgcvdr_cizmrrh.IVS_AZIM_EMPTY_IDE]) ]);;
(* }}} *)
let HYP_elim = 
prove_by_refinement( `!V E. FAN (vec 0, V, E) ==> HYP ((vec 0),V,E) = (dart_of_fan (V,E), e_fan_pair_ext(V,E),n_fan_pair_ext(V,E),f_fan_pair_ext(V,E))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[HYP;darts_of_hyp_elim;ee_of_hyp_elim;nn_of_hyp_elim;ff_of_hyp_elim]) ]);;
(* }}} *)
let hypermap_HYP_elim = 
prove_by_refinement( `!V E. FAN(vec 0,V,E) ==> hypermap ( HYP (vec 0, (V: real^3 -> bool), E)) = hypermap_of_fan (V,E) `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; BY(ASM_SIMP_TAC[Fan_defs.HYPERMAP_OF_FAN_ALT;HYP_elim]) ]);;
(* }}} *)
let local_fan2 = 
prove_by_refinement( `!V E FF. local_fan (V,E,FF ) <=> let H = hypermap_of_fan (V,E) in FAN (vec 0, V, E) /\ FF IN face_set H /\ dih2k H (CARD FF ) `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[local_fan;LET_DEF;LET_END_DEF]; TYPIFY `FAN(vec 0,V,E)` ASM_CASES_TAC; ASM_SIMP_TAC[hypermap_HYP_elim]; BY(ASM_MESON_TAC[Hypermap.lemma_in_face_set;Hypermap.lemma_face_representation]); BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let WRGCVDR_BIJ = 
prove_by_refinement( `!V E FF. local_fan (V,E,FF) ==> BIJ FST FF V`,
(* {{{ proof *) [ BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.WRGCVDR;FUN_EQ_THM]) ]);;
(* }}} *)
let  WRGCVDR_ORBIT = 
prove_by_refinement( `!V E FF. local_fan (V,E,FF) ==> (!v. v IN V ==> orbit_map (rho_node1 FF) v = V) `,
(* {{{ proof *) [ BY(MESON_TAC[ Local_lemmas.LOCAL_FAN_ORBIT_MAP_V]) ]);;
(* }}} *)
let ALL_TO_THE_NONPARALLEL_PART_ALT = 
prove_by_refinement( `!a b V E phii. deformation phii V (a,b) /\ FAN (vec 0,V,E) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> UNIONS (IMAGE (IMAGE (\v. phii v t)) E) SUBSET IMAGE (\v. phii v t) V /\ graph (IMAGE (IMAGE (\v. phii v t)) E) /\ fan1 ((vec 0):real^3, IMAGE (\v. phii (v:real^3) t) V, IMAGE (IMAGE (\v. phii v t)) E) /\ fan2 ((vec 0):real^3, IMAGE (\v. phii v t) V, IMAGE (IMAGE (\v. phii v t)) E) /\ fan6 (vec 0, IMAGE (\v. phii v t) V, IMAGE (IMAGE (\v. phii v t)) E)))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Local_lemmas1.ALL_TO_THE_NONPARALLEL_PART; BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *) (* moved to deformation.hl let XRECQNS = prove_by_refinement( `!a b V E f. deformation f V (a,b) /\ FAN (vec 0,V,E) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> FAN(vec 0, IMAGE (\v. f (v:real^3) t) V, IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[Fan.FAN]; INTRO_TAC ALL_TO_THE_NONPARALLEL_PART_ALT [`a`;`b`;`V`;`E`;`f`]; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; INTRO_TAC Deformation.FAN7_SMALL_DEFORMATION [`V`;`E`;`a`;`b`;`f`]; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; TYPIFY `if (e < e') then e else e'` EXISTS_TAC; COND_CASES_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[arith `&0 < e /\ e < e' /\ -- e < t /\ t < e ==> -- e' < t /\ t < e'`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[arith `&0 < e' /\ ~(e < e') /\ -- e' < t /\ t < e' ==> -- e < t /\ t < e`]) ]);; (* }}} *) *)
let COMPATIBLE_BW_TWO_LEMMAS2_ALT = 
prove_by_refinement( `!V E FF HS fv fw v w. (convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v = w) /\ (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\ HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\ fv = face HS (v,rho_node1 FF v)) /\ fw = face HS (w,rho_node1 FF w) ==> (v_prime V fv = slicev E FF v w /\ e_prime (E UNION {{v, w}}) fv = slicee E FF v w /\ fv = slicef E FF v w) /\ v_prime V fw = slicev E FF w v /\ e_prime (E UNION {{w, v}}) fw = slicee E FF w v /\ fw = slicef E FF w v`,
(* {{{ proof *) [ MESON_TAC[Nkezbfc_local.COMPATIBLE_BW_TWO_LEMMAS2] ]);;
(* }}} *)
let EJRCFJD_ALT = 
prove_by_refinement( `!V E FF HS fv fw v w. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v = w) /\ (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\ HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\ fv = face HS (v,rho_node1 FF v) /\ fw = face HS (w,rho_node1 FF w) ==> convex_local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv) /\ convex_local_fan (v_prime V fw,e_prime (E UNION {{w, v}}) fw,fw) /\ (!ff. sum {i | i < CARD V} (\i. ff i * interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v)) = sum {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fv} (\i. ff i * interior_angle1 (vec 0) fv (ITER i (rho_node1 FF) v)) + sum {i | i < CARD V /\ ITER i (rho_node1 FF) v IN v_prime V fw} (\i. ff i * interior_angle1 (vec 0) fw (ITER i (rho_node1 FF) v)))`,
(* {{{ proof *) [ MESON_TAC[Local_lemmas1.EJRCFJD] ]);;
(* }}} *)
let WEDGE_VV = 
prove_by_refinement( `!a b c d. ~(b IN wedge a b c d) `,
(* {{{ proof *) [ REWRITE_TAC[wedge;IN_ELIM_THM]; REPEAT GEN_TAC; TYPIFY `{a,b,b} = {a,b}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); BY(REWRITE_TAC[COLLINEAR_2]) ]);;
(* }}} *)
let ejr_distinct = 
prove_by_refinement( `!V E FF v w. convex_local_fan (V,E,FF) /\ v IN V /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==> ~(w = v)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff_gt` MP_TAC; REWRITE_TAC[NOT_FORALL_THM]; TYPIFY `(v,rho_node1 FF v)` EXISTS_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); DISCH_THEN MP_TAC THEN ANTS_TAC; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]); ASM_REWRITE_TAC[]; TYPIFY `{v,v} = {v}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]); ASM_REWRITE_TAC[wedge_in_fan_gt]; TYPIFY `v IN aff_gt {vec 0} {v}` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC AFF_GT_1_1; REWRITE_TAC[DISJOINT;IN_ELIM_THM]; REWRITE_TAC[EXTENSION;IN_INTER;IN_SING;NOT_IN_EMPTY]; CONJ_TAC; RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN]); RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;LET_DEF;LET_END_DEF;Fan_defs.fan2]); BY(ASM_MESON_TAC[]); GEXISTL_TAC [`&0`;`&1`]; REWRITE_TAC[arith `&0 < &1`;arith `&0 + &1 = &1`]; BY(VECTOR_ARITH_TAC); REWRITE_TAC[SUBSET]; BY(ASM_MESON_TAC[WEDGE_VV]) ]);;
(* }}} *) (* TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]); FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC; *)
let WEDGE_EDGE_NOT_ADJ = 
prove_by_refinement( `!V E FF v . local_fan (V,E,FF) /\ v IN V ==> ~(aff_gt {vec 0} {v, rho_node1 FF v} SUBSET wedge_in_fan_gt (v,rho_node1 FF v) E) `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `CARD(EE v E) > 1` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOFA_CARD_EE_V_1;arith `2 > 1`]); FIRST_X_ASSUM_ST `wedge_in_fan_gt` MP_TAC; ASM_REWRITE_TAC[wedge_in_fan_gt]; REPEAT WEAKER_STRIP_TAC; 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)`]; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND; CONJ_TAC; BY(ASM_MESON_TAC[]); DISCH_THEN MP_TAC THEN ANTS_TAC; BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS;Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]); BY(REWRITE_TAC[wedge;IN_ELIM_THM;AZIM_REFL;arith `~(&0 < &0)`]) ]);;
(* }}} *)
let PERIODIC_RHO_NODE1 = 
prove_by_refinement( `!V E FF v. local_fan (V,E,FF) /\ v IN V ==> periodic (\i. ITER i (rho_node1 FF) v) (CARD V)`,
(* {{{ proof *) [ REWRITE_TAC[Oxl_def.periodic;GSYM ITER_ADD]; REPEAT WEAKER_STRIP_TAC; AP_TERM_TAC; MATCH_MP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2; BY(ASM_REWRITE_TAC[]) ]);;
(* }}} *)
let V_PRIME_SUBSET_V = 
prove_by_refinement( `!V f. v_prime (V:real^3->bool) (f:real^3 # real^3 -> bool) SUBSET V`,
(* {{{ proof *) [ REWRITE_TAC[v_prime;SUBSET;IN_ELIM_THM]; BY(MESON_TAC[]) ]);;
(* }}} *)
let SLICEV_IMAGE = 
prove_by_refinement( `!V E FF v w i. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\ (i < CARD V) /\ (w = ITER i (rho_node1 FF) v) ==> slicev E FF v w = IMAGE (\j. ITER j (rho_node1 FF) v) {j | j < i+1 } `,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]); COMMENT "remove a many lines here";
TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM); ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); COMMENT "v_prime as image"; TYPIFY `v_prime V fv = IMAGE (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE; GEXISTL_TAC [`w`;`FF`;`v`]; CONJ_TAC; GEXISTL_TAC [`E`;`HS`]; ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE]; X_GEN_TAC `u:real^3`; REWRITE_TAC[Geomdetail.EQ_EXPAND]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `n` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `x` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC); TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); BY(ASM_MESON_TAC[]) ]);; (* }}} *)
let LOCAL_FAN_ORBIT_MAP_EXPLICIT = 
prove (`!V E FF v w. local_fan(V,E,FF) /\ v IN V /\ w IN V ==> ?i. i < CARD V /\ w = ITER i (rho_node1 FF) v`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `v:real^3` o MATCH_MP Local_lemmas.LOCAL_FAN_ORBIT_MAP_V) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER; Hypermap.orbit_map] THEN ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN DISCH_THEN(MP_TAC o SPEC `w:real^3`) THEN ASM_REWRITE_TAC[GE; LE_0] THEN DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN EXISTS_TAC `n MOD (CARD(V:real^3->bool))` THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOCAL_FAN_FINITE_V) THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP Local_lemmas.LOFA_V_NOT_EMP) THEN MP_TAC(ISPECL [`n:num`; `CARD(V:real^3->bool)`] DIVISION) THEN ABBREV_TAC `i = n MOD (CARD(V:real^3->bool))` THEN ABBREV_TAC `m = n DIV (CARD(V:real^3->bool))` THEN ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN(K ALL_TAC) THEN SPEC_TAC(`m:num`,`p:num`) THEN INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ONCE_REWRITE_TAC[ARITH_RULE `(a + b) + c:num = (a + c) + b`] THEN ONCE_REWRITE_TAC[GSYM ITER_ADD] THEN FIRST_ASSUM(MP_TAC o MATCH_MP Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID) THEN ASM_SIMP_TAC[]);;
let SLICEW_IMAGE = 
prove_by_refinement( `!V E FF v w n. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\ (n < CARD V) /\ (w = ITER n (rho_node1 FF) v) ==> slicev E FF w v = IMAGE (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ (n <= j /\ j < CARD V) }`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]); 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); MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM2); ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); COMMENT "v_prime as image";
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); REWRITE_TAC[EXTENSION;IN_IMAGE]; X_GEN_TAC `u:real^3`; TYPIFY `u IN v_prime V fw` ASM_CASES_TAC; ASM_REWRITE_TAC[]; INTRO_TAC V_PRIME_SUBSET_V [`V`;`fw`]; REWRITE_TAC[SUBSET]; DISCH_THEN (C INTRO_TAC [`u`]); DISCH_TAC; INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`u`]; ANTS_TAC; BY(ASM_MESON_TAC[]); REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `i` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; REWRITE_TAC[NOT_EXISTS_THM;IN_ELIM_THM]; BY(ASM_MESON_TAC[]); BY(ASM_MESON_TAC[]) ]);; (* }}} *) (* Might extract things like the exact card of slicev, and the fact that 3 < CARD V *)
let CARD_SLICEV_LT = 
prove_by_refinement( `!V E FF v w. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==> CARD (slicev E FF v w) < CARD V`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `!i. ITER i (rho_node1 FF) v IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;]); INTRO_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT [`V`;`E`;`FF`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `1 < CARD V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas1.DIFFERENCE_IMP_LT_CARDV; ASM_REWRITE_TAC[arith `n < 1 <=> n = 0`]; BY(ASM_MESON_TAC[ITER]); TYPIFY `~(i = CARD V - 1)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; TYPIFY `w = ivs_rho_node1 FF v` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]); INTRO_TAC WEDGE_EDGE_NOT_ADJ [`V`;`E`;`FF`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[]; RULE_ASSUM_TAC (ONCE_REWRITE_RULE[Collect_geom.PER_SET2]); TYPIFY `w,rho_node1 FF w IN FF` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]); TYPIFY `rho_node1 FF w = v` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]); BY(ASM_MESON_TAC[]); TYPIFY `!j. j < CARD V /\ ITER j (rho_node1 FF) v IN v_prime V fv <=> j < i+1` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC (REWRITE_RULE[TAUT `(a ==> b ==> c) <=> (a /\ b ==> c)`] Local_lemmas1.CONDS_IN_V_PRIME_NUM); ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); COMMENT "v_prime as image";
TYPIFY `v_prime V fv = IMAGE (\j. ITER j (rho_node1 FF) v) {j | j < i+1 }` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC Local_lemmas1.POINTS_IN_HAFL_CIRCLE; GEXISTL_TAC [`w`;`FF`;`v`]; CONJ_TAC; GEXISTL_TAC [`E`;`HS`]; ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE]; X_GEN_TAC `u:real^3`; REWRITE_TAC[Geomdetail.EQ_EXPAND]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `n` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `n < i+1 <=> ~(i < n)`]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `x` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `m < CARD V` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); TYPIFY `m = i` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA]); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); COMMENT "now use IMAGE CARD"; FIRST_X_ASSUM (SUBST1_TAC); MATCH_MP_TAC LET_TRANS; TYPIFY `CARD {j | j < i + 1}` EXISTS_TAC; CONJ_TAC; MATCH_MP_TAC CARD_IMAGE_LE; BY(REWRITE_TAC[FINITE_NUMSEG_LT]); REWRITE_TAC[CARD_NUMSEG_LT]; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC) ]);; (* }}} *)
let SLICEW_BIJ = 
prove_by_refinement( `!V E FF v w n. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\ n < CARD V /\ w = ITER n (rho_node1 FF) v ==> BIJ (\j. ITER j (rho_node1 FF) v) {j | j = 0 \/ n <= j /\ j < CARD V} (slicev E FF w v)`,
(* {{{ proof *) [ REWRITE_TAC[BIJ]; REPEAT WEAKER_STRIP_TAC; SUBCONJ2_TAC; INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]); REWRITE_TAC[SURJ;INJ]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]); TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC); ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM]; BY(ASM_MESON_TAC[]); INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA []; ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let SLICEV_BIJ = 
prove_by_refinement( `!V E FF v w n. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\ n < CARD V /\ w = ITER n (rho_node1 FF) v ==> BIJ (\j. ITER j (rho_node1 FF) v) {j | j < n + 1} (slicev E FF v w)`,
(* {{{ proof *) [ REWRITE_TAC[BIJ]; REPEAT WEAKER_STRIP_TAC; SUBCONJ2_TAC; INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]); REWRITE_TAC[SURJ;INJ]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `FINITE V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]); TYPIFY `0 < CARD V` (C SUBGOAL_THEN ASSUME_TAC); ASM_SIMP_TAC[ arith `0 < x <=> ~(x = 0)`;CARD_EQ_0;EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM]; BY(ASM_MESON_TAC[]); INTRO_TAC Local_lemmas1.LT_CARD_MONO_LOFA []; ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(ASM_MESON_TAC[arith `x < n+1 /\ n < c==> x < c`]) ]);;
(* }}} *)
let CARD_SLICEV = 
prove_by_refinement( `!V E FF v w . convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==> CARD (slicev E FF v w) + CARD(slicev E FF w v) = CARD V + 2`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC); COMMENT "insert";
TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT; TYPIFY `E` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`]; ASM_REWRITE_TAC[]; DISCH_TAC; TYPED_ABBREV_TAC `f = (\j. ITER j (rho_node1 FF) v)` ; TYPIFY `CARD {j | j < n + 1} = CARD (slicev E FF v (ITER n (rho_node1 FF) v))` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD; ASM_REWRITE_TAC[FINITE_NUMSEG_LT]; BY(ASM_MESON_TAC[]); DISCH_THEN (SUBST1_TAC o GSYM); TYPIFY `CARD {j | j =0 \/ ( n <= j /\ j < CARD V)} = CARD (slicev E FF w v)` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC Misc_defs_and_lemmas.BIJ_CARD; TYPIFY `f` EXISTS_TAC; CONJ2_TAC; BY(ASM_REWRITE_TAC[]); MATCH_MP_TAC FINITE_SUBSET; TYPIFY `{0} UNION {j | j < CARD V}` EXISTS_TAC; CONJ_TAC; MATCH_MP_TAC FINITE_UNION_IMP; BY(ASM_REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY;FINITE_NUMSEG_LT]); BY(SET_TAC[]); ASM_REWRITE_TAC[]; DISCH_THEN (SUBST1_TAC o GSYM); REWRITE_TAC[CARD_NUMSEG_LT]; TYPIFY `{j | j = 0 \/ n <= j /\ j < CARD V } = {0} UNION {j | n <= j /\ j < CARD V}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); INTRO_TAC Geomdetail.CARD_EQUATION [`{0}`;`{j | n <= j /\ j < CARD V}`]; ANTS_TAC; REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]; MATCH_MP_TAC FINITE_SUBSET; TYPIFY ` {j | j < CARD V}` EXISTS_TAC; ASM_REWRITE_TAC[FINITE_NUMSEG_LT]; BY(SET_TAC[]); TYPIFY `({0} INTER {j | n <= j /\ j < CARD V}) = {}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;IN_SING;IN_ELIM_THM]; TYPIFY `~(n=0)` ENOUGH_TO_SHOW_TAC; BY(ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC; ASM_REWRITE_TAC[ITER]; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; DISCH_THEN MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[CARD_CLAUSES;arith `x + 0 = x`]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[Geomdetail.CARD_SING]; TYPIFY `{j | n <= j /\ j < CARD V} = (n.. (CARD V - 1))` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;IN_NUMSEG;IN_ELIM_THM]; BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC); REWRITE_TAC[CARD_NUMSEG]; BY(REPEAT (FIRST_X_ASSUM_ST `n < CARD V` MP_TAC) THEN ARITH_TAC) ]);; (* }}} *)
let HAFL_CIRCLE_FORM_LOCAL_FAN_ALT = 
prove_by_refinement( `!V E FF v w HS fv. (local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v = w) /\ (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\ (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\ HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\ fv = face HS (v,rho_node1 FF v) ==> local_fan (v_prime V fv,e_prime (E UNION {{v, w}}) fv,fv)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN) []; DISCH_THEN MATCH_MP_TAC; GEXISTL_TAC [`HS`;`FF`]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT = 
prove_by_refinement( `!V E FF v w HS fv. (local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v = w) /\ (!z t. z IN {v, w} /\ t IN V DIFF {z} ==> ~collinear {vec 0, z, t}) /\ (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E)) /\ HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\ fv = face HS (v,rho_node1 FF v) /\ fw = face HS (w,rho_node1 FF w) ==> 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)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL Local_lemmas1.HAFL_CIRCLE_FORM_LOCAL_FAN2) []; DISCH_THEN MATCH_MP_TAC; GEXISTL_TAC [`HS`;`FF`]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let CARD_SLICEF = 
prove_by_refinement( `!V E FF v w . convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==> CARD (slicef E FF v w) + CARD(slicef E FF w v) = CARD FF + 2`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); 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); MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT; GEXISTL_TAC [`FF`;`HS`]; ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `FINITE FF /\ FINITE fv /\ FINITE fw` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]); REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP Local_lemmas.LOFA_IMP_BIJ_FF_V))); INTRO_TAC CARD_SLICEV [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; BY(MESON_TAC[Local_lemmas.BIJ_IMP_CARD_EQ]) ]);;
(* }}} *)
let aff_ge_INTER_aff_lt = 
prove_by_refinement( `! (y:real^A). ~(y = vec 0) ==> aff_ge {vec 0} {y} INTER aff_lt {vec 0} {y} = {}`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; ASM_SIMP_TAC[AFF_GE_1_1_0]; GMATCH_SIMP_TAC AFF_LT_1_1; REWRITE_TAC[DISJOINT;IN_SING;EXTENSION;IN_INTER;IN_ELIM_THM;NOT_IN_EMPTY]; CONJ_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[VECTOR_MUL_RZERO]; REWRITE_TAC[varith `a % y = vec 0 + t2 % (y:real^A) <=> (a - t2) % y = vec 0`]; ASM_REWRITE_TAC[VECTOR_MUL_EQ_0]; BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC) ]);;
(* }}} *)
let ejr_generic = 
prove_by_refinement( `!V E FF v w. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) /\ generic V E ==> generic (slicev E FF v w) (slicee E FF v w)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[generic]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `e_prime (E UNION {{v,w}}) fv SUBSET (E UNION {{v,w}})` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.E_PRIME_SUBSET_E]); TYPIFY `{v',w'} IN E \/ {v',w'} = {v,w}` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `x IN slicee E FF v w` MP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[SUBSET;IN_UNION;IN_SING]; BY(MESON_TAC[]); FIRST_X_ASSUM (DISJ_CASES_TAC); FIRST_X_ASSUM_ST `generic` MP_TAC; REWRITE_TAC[generic]; DISCH_THEN MATCH_MP_TAC; BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]); FIRST_X_ASSUM (fun t -> REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[t]) THEN REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]); REWRITE_TAC[GSYM SUBSET_EMPTY]; MATCH_MP_TAC SUBSET_TRANS; 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; CONJ_TAC; BY(SET_TAC[]); REWRITE_TAC[UNION_SUBSET;SUBSET_EMPTY]; TYPIFY `u IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[V_PRIME_SUBSET_V;SUBSET]); TYPIFY `~(v = vec 0) /\ ~(w = vec 0) /\ ~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC (REWRITE_RULE[local_fan;Fan_defs.FAN;Fan_defs.fan2;LET_DEF;LET_END_DEF]); BY(ASM_MESON_TAC[]); CONJ2_TAC; CONJ_TAC; PROOF_BY_CONTR_TAC; TYPIFY `collinear {vec 0,u,v}` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]); TYPIFY `u = v` ASM_CASES_TAC; BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]); BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]); PROOF_BY_CONTR_TAC; TYPIFY `collinear {vec 0,u,w}` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL]); TYPIFY `u = w` ASM_CASES_TAC; BY(ASM_MESON_TAC[aff_ge_INTER_aff_lt]); BY(ASM_MESON_TAC[Collect_geom.PER_SET3;IN_INSERT]); 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; BY(SET_TAC[]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_RHO_NODE_PROS]); REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER]; GEN_TAC; GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_LOFA_DETER2; CONJ_TAC; BY(ASM_MESON_TAC[]); REWRITE_TAC[TAUT `~(a /\ b) <=> ( a ==> ~b)`]; ASM_SIMP_TAC[Nkezbfc_local.AFF_LT_1_1;IN_ELIM_THM;wedge]; REWRITE_TAC[VECTOR_MUL_RZERO;VECTOR_ADD_LID]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `collinear` MP_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[Local_lemmas.COLLINEAR_ONCE_VEC_0]; BY(MESON_TAC[]) ]);;
(* }}} *)
let LOFA_IMP_LT_CARD_SET_V_ALT = 
prove_by_refinement( `!V E FF v. local_fan (V,E,FF) /\ v IN V ==> {ITER n (rho_node1 FF) v | n < CARD V} = V`,
(* {{{ proof *) [ BY(MESON_TAC[Local_lemmas.LOFA_IMP_LT_CARD_SET_V]) ]);;
(* }}} *)
let ejr_sum = 
prove_by_refinement( `!V E FF HS v w f fv fw. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ hypermap (HYP (vec 0,V,E UNION {{v, w}})) = HS /\ face HS (v,rho_node1 FF v) = fv /\ face HS (w,rho_node1 FF w) = fw /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) // /\ ==> sum FF (\e. f (FST e) * azim_in_fan e E) = sum fv (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{v, w}}) fv)) + sum fw (\e. f (FST e) * azim_in_fan e (e_prime (E UNION {{w, v}}) fw))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[generic]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); TYPIFY `?n. n < CARD V /\ w = ITER n (rho_node1 FF) v` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC LOCAL_FAN_ORBIT_MAP_EXPLICIT; TYPIFY `E` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`(\i. f (ITER i (rho_node1 FF) v))`]); REWRITE_TAC[]; COMMENT "replace first index set";
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); INTRO_TAC SLICEV_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[IN_IMAGE;IN_ELIM_THM]; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; X_GEN_TAC `i:num`; REWRITE_TAC[Geomdetail.EQ_EXPAND]; CONJ2_TAC; REPEAT WEAKER_STRIP_TAC; SUBCONJ_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC); DISCH_TAC; TYPIFY `i` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC); BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA;arith `x' < n+1 /\ n < c ==> x' < c`]); COMMENT "n not 0"; TYPIFY `~(n=0)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `w = ITER n r v` MP_TAC; BY(ASM_REWRITE_TAC[ITER]); COMMENT "replace second index set"; 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); INTRO_TAC SLICEW_IMAGE [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[IN_IMAGE;IN_ELIM_THM]; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; X_GEN_TAC `i:num`; REWRITE_TAC[Geomdetail.EQ_EXPAND]; CONJ2_TAC; REPEAT WEAKER_STRIP_TAC; SUBCONJ_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); DISCH_TAC; TYPIFY `i` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `i = x'` ENOUGH_TO_SHOW_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `(a:num) < b` MP_TAC) THEN ARITH_TAC); TYPIFY `x' < CARD V` (C SUBGOAL_THEN MP_TAC); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]); MATCH_MP_TAC (arith `(a = a' /\ b = b' /\ c = c') ==> (a = b + c ==> a' = b' + c')`); COMMENT "match summands"; 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); BY(REWRITE_TAC[FUN_EQ_THM;o_THM]); COMMENT "first sum"; CONJ_TAC; TYPIFY `BIJ (\i. (ITER i (rho_node1 FF) v)) {i | i < CARD V} V` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[BIJ]; SUBCONJ2_TAC; TYPIFY `IMAGE (\i. (ITER i (rho_node1 FF) v)) {i | i < CARD V} = V` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[Misc_defs_and_lemmas.IMAGE_SURJ]); INTRO_TAC LOFA_IMP_LT_CARD_SET_V_ALT [`V`;`E`;`FF`;`v`]; ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_IMAGE]; BY(MESON_TAC[]); REWRITE_TAC[SURJ;INJ]; DISCH_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[IN_ELIM_THM]; BY(ASM_MESON_TAC[ Local_lemmas1.LT_CARD_MONO_LOFA]); FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) FF u`]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; TYPIFY `BIJ FST FF V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC WRGCVDR_BIJ; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) FF u`]); DISCH_THEN (SUBST1_TAC o GSYM); MATCH_MP_TAC SUM_EQ; REWRITE_TAC[o_THM]; GEN_TAC; DISCH_TAC; TYPIFY `FST x IN V` ENOUGH_TO_SHOW_TAC; DISCH_TAC; AP_TERM_TAC; BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]); COMMENT "prep for slice cases"; 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); MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT; GEXISTL_TAC [`FF`;`HS`]; ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); COMMENT "second sum"; CONJ_TAC; INTRO_TAC SLICEV_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fv u`]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; TYPIFY `BIJ FST fv (v_prime V fv)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC WRGCVDR_BIJ; BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]); FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fv u`]); DISCH_THEN (SUBST1_TAC o GSYM); MATCH_MP_TAC SUM_EQ; REWRITE_TAC[o_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `FST x IN v_prime V fv` ENOUGH_TO_SHOW_TAC; DISCH_TAC; AP_TERM_TAC; BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]); COMMENT "last case"; INTRO_TAC SLICEW_BIJ [`V`;`E`;`FF`;`v`;`w`;`n`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [`\u. f u * interior_angle1 (vec 0) fw u`]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; TYPIFY `BIJ FST fw (v_prime V fw)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC WRGCVDR_BIJ; BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]); FIRST_X_ASSUM (MP_TAC o (MATCH_MP Basics.BIJ_SUM)); DISCH_THEN (C INTRO_TAC [ `\u. f u * interior_angle1 (vec 0) fw u`]); DISCH_THEN (SUBST1_TAC o GSYM); MATCH_MP_TAC SUM_EQ; REWRITE_TAC[o_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `FST x IN v_prime V fw` ENOUGH_TO_SHOW_TAC; DISCH_TAC; AP_TERM_TAC; BY(ASM_MESON_TAC[Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM;Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2]); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V2]) ]);; (* }}} *)
let EJRCFJD_ALT2 = 
prove_by_refinement( `!V E FF v w. convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ (!u u1. u IN {v, w} /\ u1 IN V /\ ~(u = u1) ==> ~collinear {vec 0, u, u1}) /\ (!e. e IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt e E) ==> convex_local_fan (slicev E FF v w,slicee E FF v w,slicef E FF v w) /\ convex_local_fan (slicev E FF w v,slicee E FF w v,slicef E FF w v) /\ tau_fun V E FF >= tau_fun (slicev E FF v w) (slicee E FF v w) (slicef E FF v w) + tau_fun (slicev E FF w v) (slicee E FF w v) (slicef E FF w v) /\ sol_local E FF = sol_local (slicee E FF v w) (slicef E FF v w) + sol_local (slicee E FF w v) (slicef E FF w v) /\ CARD (slicev E FF v w) < CARD V /\ CARD (slicev E FF w v) < CARD V /\ (generic V E ==> generic (slicev E FF v w) (slicee E FF v w) /\ generic (slicev E FF w v) (slicee E FF w v))`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC ejr_distinct [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPED_ABBREV_TAC `HS = hypermap (HYP (vec 0,V,E UNION {{v, w}}))` ; TYPED_ABBREV_TAC `fv = face HS (v,rho_node1 FF v)` ; TYPED_ABBREV_TAC `fw = face HS (w,rho_node1 FF w)` ; INTRO_TAC EJRCFJD_ALT [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; INTRO_TAC (GSYM COMPATIBLE_BW_TWO_LEMMAS2_ALT) [`V`;`E`;`FF`;`HS`;`fv`;`fw`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `CARD (v_prime V fv) < CARD V /\ CARD (v_prime V fw) < CARD V` (C SUBGOAL_THEN (unlist REWRITE_TAC)); REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `v_prime` (SUBST1_TAC o GSYM)); CONJ_TAC; MATCH_MP_TAC CARD_SLICEV_LT; BY(ASM_REWRITE_TAC[]); MATCH_MP_TAC CARD_SLICEV_LT; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Collect_geom.PER_SET3]); 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)); DISCH_TAC; CONJ_TAC; INTRO_TAC ejr_generic [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); BY(ASM_MESON_TAC[]); INTRO_TAC ejr_generic [`V`;`E`;`FF`;`w`;`v`]; ANTS_TAC; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Collect_geom.PER_SET3]); BY(ASM_MESON_TAC[]); COMMENT "now tau and sol";
REWRITE_TAC[sol_local;tau_fun]; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.CVX_LO_IMP_LO]); 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); MATCH_MP_TAC HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT; GEXISTL_TAC [`FF`;`HS`]; ASM_REWRITE_TAC[IN_DIFF;IN_SING]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; COMMENT "insert"; TYPIFY ` CARD FF + 2 = CARD fv + CARD fw` (C SUBGOAL_THEN ASSUME_TAC); COMMENT "cut insert to here"; INTRO_TAC CARD_SLICEF [`V`;`E`;`FF`;`v`;`w`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; DISCH_THEN SUBST1_TAC; BY(REWRITE_TAC[]); COMMENT "tau sum"; INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`rho_fun o (norm: (real^3-> real))`;` fv`;` fw`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[o_THM]; DISCH_THEN SUBST1_TAC; CONJ_TAC; MATCH_MP_TAC (arith `c1 = c2 + c3 ==> ((a + b) - c1 >= a - c2 + b - c3)`); REWRITE_TAC[arith `a * b + a * c = a * (b + c)`]; AP_TERM_TAC; REWRITE_TAC[REAL_OF_NUM_ADD]; REWRITE_TAC[REAL_OF_NUM_EQ]; TYPIFY `(2 <= CARD FF /\ 2 <= CARD fv /\ 2 <= CARD fw) /\ CARD FF + 2 = CARD fv + CARD fw` ENOUGH_TO_SHOW_TAC; BY(ARITH_TAC); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ; TYPIFY`V` EXISTS_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); CONJ_TAC; MATCH_MP_TAC Hypermap.CARD_ATLEAST_2; GEXISTL_TAC [`v`;`w`]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]); REPEAT (GMATCH_SIMP_TAC (arith `2 < x ==> 2 <= x`)); REPEAT (GMATCH_SIMP_TAC (Local_lemmas1.LOFA_HYP_UNION_CARD_GT2)); REWRITE_TAC[IN_DIFF;IN_SING]; CONJ_TAC; GEXISTL_TAC [`V`;`E`;`w`;`HS`;`FF`;`v`]; BY(ASM_MESON_TAC[]); GEXISTL_TAC [`V`;`E`;`v`;`HS`;`FF`;`w`]; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[Collect_geom.PER_SET2]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Collect_geom.PER_SET3]); COMMENT "final sum"; INTRO_TAC ejr_sum [`V`;` E`;` FF`;` HS`;` v`;` w`;`\ (v:real^3). &1`;` fv`;` fw`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[o_THM;arith `&1 * x = x`]; TYPIFY `FINITE fv /\ FINITE fw /\ FINITE FF` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF]); ASM_SIMP_TAC[SUM_SUB]; ASM_SIMP_TAC[SUM_CONST]; DISCH_THEN kill; MATCH_MP_TAC (arith `cf + t2 = cv + c2 ==>t2 + (tv + tw) - cf = (t2 + tv - cv) + (t2 + tw - c2)`); MATCH_MP_TAC (arith `cf + &2 = cv + cw ==> cf * pi + &2 * pi = cv * pi + cw * pi`); REWRITE_TAC[REAL_OF_NUM_ADD]; REWRITE_TAC[REAL_OF_NUM_EQ]; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *)
let NKEZBFC = 
prove_by_refinement( `!V E FF. convex_local_fan(V,E,FF) /\ generic V E ==> &0 <= sol_local E FF`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MP_TAC Nkezbfc_local.NKEZBFC_PREP; ANTS_TAC; BY(REWRITE_TAC[EJRCFJD_ALT2 ]); BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let azim_dart_azim_in_fan = 
prove_by_refinement( `!V E x. FAN((vec 0),V,E) /\ ({FST x,SND x} IN E) ==> azim_dart (V,E) x = azim_in_fan x E`,
(* {{{ proof *) [ REWRITE_TAC[FORALL_PAIR_THM;FST;SND]; REWRITE_TAC[Fan_defs.azim_dart;(* L *)azim_in_fan;Fan_defs.azim_fan]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[LET_DEF;LET_END_DEF]; TYPIFY `~(p1 = p2)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; RULE_ASSUM_TAC (REWRITE_RULE[Fan.FAN;Fan.graph]); REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`{p1,p2}`]); REWRITE_TAC[Local_lemmas1.SET2_HAS_SIZE2]; BY(ASM_MESON_TAC[IN]); ASM_SIMP_TAC[GSYM (* L *)EE_elim]; COND_CASES_TAC THEN ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN; TYPIFY `V` EXISTS_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[GSYM (* L *)EE_elim]; BY(ASM_REWRITE_TAC[(* L *)EE;IN_ELIM_THM]) ]);;
(* }}} *)
let rho_fun = new_definition `rho_fun y =  &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
let rho_rho_fun = 
prove_by_refinement( `!y. rho_fun y = rho y`,
(* {{{ proof *) [ REWRITE_TAC[Sphere.rho;rho_fun;Sphere.const1;Sphere.ly;Sphere.interp]; REWRITE_TAC[GSYM Nonlinear_lemma.sol0_EQ_sol_y;Sphere.h0]; REWRITE_TAC[arith `a + b = a + c <=> c = b`]; GEN_TAC; MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`); AP_TERM_TAC; BY(REAL_ARITH_TAC) ]);;
(* }}} *)
let h_dart = new_definition `h_dart (x:real^3#B) = norm (FST x)  / &2`;;
let tauVEF = new_definition `tauVEF (V,E,f) = 
  sum f ( \ x. azim_dart (V,E) x * (&1 + (sol0/pi) * (&1 - lmfun (h_dart x))))   + (pi + sol0)*(&2 - &(CARD(f)))`;;
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)`;;
let ly_EQ_lmfun = 
prove(`!x:real^3#real^3. norm (FST x) <= &2 * h0 ==> lmfun (h_dart x) = ly (norm (FST x))`,
REWRITE_TAC[Pack_defs.lmfun; Sphere.ly; Sphere.interp; h_dart; Pack_defs.h0] THEN REAL_ARITH_TAC);;
let tauVEF_tau_fun = 
prove_by_refinement( `!V E f. FAN ((vec 0),V,E) /\ 2 <= CARD f /\ (!x. x IN f ==> norm(FST x) <= &2 * h0) /\ (!x. x IN f ==> {FST x,SND x} IN E) ==> tau_fun V E f = tauVEF (V,E,f)`,
(* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[tauVEF;tau_fun]; GMATCH_SIMP_TAC (GSYM REAL_OF_NUM_SUB); ASM_REWRITE_TAC[]; REWRITE_TAC[arith `x - u * (v - w) = x' + u * (w - v) <=> x = x'`]; MATCH_MP_TAC SUM_EQ; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[]; MATCH_MP_TAC (arith `x = x' /\ y = y' ==> x*y' = y*x'`); REWRITE_TAC[rho_rho_fun;Sphere.rho;Nonlinear_lemma.sol0_over_pi_EQ_const1]; CONJ_TAC; MATCH_MP_TAC (arith `(l = l') ==> &1 + c - c * l = &1 + c *(&1 - l')`); BY(ASM_SIMP_TAC[ly_EQ_lmfun]); GMATCH_SIMP_TAC azim_dart_azim_in_fan; BY(ASM_SIMP_TAC[]) ]);;
(* }}} *) end;;