(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-06-17                                                           *)
(* ========================================================================== *)

(* General properties of a contravening packing   *)


flyspeck_needs "leg/collect_geom.hl";;
flyspeck_needs "trigonometry/trigonometry.hl";;
flyspeck_needs "nonlinear/ineq.hl";;

flyspeck_needs "fan/HypermapAndFan.hl";;
flyspeck_needs "tame/CKQOWSA.hl";;
flyspeck_needs "tame/tame_defs.hl";;


module Tame_general = struct

open Fan_defs;;
open Hypermap_and_fan;;
open Tame_defs;;



(* Non-linear inequalities *)
(* let tame_hypermap_calcs_concl = new_definition Tame_defs.tame_hypermap_calcs;; *)


(* tame ==> restricted *)
let RUNOQPQ = prove(`!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`,
    GEN_TAC THEN REWRITE_TAC[tame_hypermap; restricted_hypermap] THEN
      SIMP_TAC[tame_1; tame_2; tame_3; tame_5a; tame_9a] THEN
      REPEAT STRIP_TAC THENL
      [
        FIRST_X_ASSUM (MP_TAC o check (fun th -> (concl th) = `tame_8 (H:(A)hypermap)`)) THEN
          REWRITE_TAC[tame_8; Hypermap.number_of_faces; Hypermap.face_set; Hypermap.set_of_orbits] THEN
          SUBGOAL_THEN `{orbit_map (face_map (H:(A)hypermap)) x | x | x IN dart H} = {}` (fun th -> REWRITE_TAC[th]) THENL
          [
            ASM_REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
              X_GEN_TAC `ff:A->bool` THEN
              REWRITE_TAC[IN_ELIM_THM];
            ALL_TAC
          ] THEN
          REWRITE_TAC[CARD_CLAUSES; ARITH_RULE `~(0 >= 3)`];

        MP_TAC (SPEC `H:(A)hypermap` Hypermap.lemmaZHQCZLX) THEN
          ASM_SIMP_TAC[is_node_nondegenerate; GSYM GE];

        POP_ASSUM MP_TAC THEN
          REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits] THEN
          ONCE_REWRITE_TAC[GSYM Hypermap.face] THEN
          REWRITE_TAC[IN_ELIM_THM] THEN
          STRIP_TAC THEN
          ASM_SIMP_TAC[]
      ]);;


(* UBHDEUU1 = CKQOWSA *)
let UBHDEUU1 = Ckqowsa.CKQOWSA;;


(* (V,ECTC V) is a fan *)
let UBHDEUU2 = prove(`!V. packing V /\ V SUBSET ball_annulus /\ ~(V = {}) ==> FAN(vec 0, V, ECTC V)`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC Topology.CTVTAQA THEN
     EXISTS_TAC `ESTD V` THEN
     ASM_SIMP_TAC[UBHDEUU1] THEN
     REWRITE_TAC[ECTC; ESTD; SUBSET; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     MAP_EVERY EXISTS_TAC [`v:real^3`; `w:real^3`] THEN
     ASM_SIMP_TAC[Sphere.h0; REAL_ARITH `a = &2 ==> a <= &2 * #1.26`]);;
   


(*********************)
(* Numerical results *)
(*********************)

let COS_PI3 = prove(`cos (pi / &3) = &1 / &2`,
   REWRITE_TAC[COS_SIN] THEN
     REWRITE_TAC[REAL_ARITH `pi / &2 - pi / &3 = pi / &6`] THEN
     REWRITE_TAC[SIN_PI6]);;


let ACS_2 = prove(`acs (&1 / &2) = pi / &3`,
   REWRITE_TAC[SYM COS_PI3] THEN
     MATCH_MP_TAC ACS_COS THEN
     REWRITE_TAC[REAL_ARITH `(&0 <= a / &3 <=> &0 <= a) /\ (a / &3 <= a <=> &0 <= a)`] THEN
     MATCH_MP_TAC REAL_LT_IMP_LE THEN
     REWRITE_TAC[PI_POS]);;


let sol0_POS = prove(`&0 < sol0`,
   REWRITE_TAC[Pack_defs.sol0] THEN
     REWRITE_TAC[REAL_ARITH `&0 < &3 * a - pi <=> pi / &3 < a`] THEN
     REWRITE_TAC[SYM ACS_2] THEN
     MATCH_MP_TAC ACS_MONO_LT THEN
     REAL_ARITH_TAC);;

	 
(****************************************)	 



(*******************************************************************************************)
(* Connections between algebraic definitions in Sphere and geometric definitions elsewhere *)
(*******************************************************************************************)

(* ly = lmfun *)
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);;



(* sol0 = const1 * pi *)
let sol0_EQ_sol_y = prove(`sol0 = sol_y (&2) (&2) (&2) (&2) (&2) (&2)`,
    REWRITE_TAC[Pack_defs.sol0; Sphere.sol_y; Sphere.dih_y; Sphere.dih_x; Sphere.delta_x4; Sphere.delta_x] THEN
      CONV_TAC (DEPTH_CONV let_CONV) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      MP_TAC (SPEC `&1 / &3` Trigonometry2.acs_atn2) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
      REWRITE_TAC [REAL_ARITH `&3 * (a - b) - c = (a + d) + (a + d) + (a + d) - c <=> --b = d`] THEN
      MP_TAC (SPECL [`sqrt (&8 / &9)`; `&1 / &3`] Trigonometry1.ATN2_RNEG) THEN
      CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
      SUBGOAL_THEN `sqrt (&2048) = &48 * sqrt (&8 / &9) /\ -- &16 = &48 * (-- &1 / &3)` ASSUME_TAC THENL
      [
	MP_TAC (SPECL [`&48`; `&8 / &9`] Vol1.SQRT_MUL_POW_2) THEN
	  CONV_TAC (REAL_RAT_REDUCE_CONV);
	ALL_TAC
      ] THEN
      ASM_REWRITE_TAC[] THEN
      MATCH_MP_TAC (GSYM Trigonometry1.ATN2_LMUL_EQ) THEN
      REAL_ARITH_TAC);;


(* sol0 = const1 *)
let sol0_over_pi_EQ_const1 = prove(`sol0 / pi = const1`,
   REWRITE_TAC[sol0_EQ_sol_y; Sphere.const1]);;
	 

	 
(* Alternative form for ineq *)
let INEQ_ALT = prove(`!A bounds. ineq bounds A <=> (ALL (\(a,x,b). a <= x /\ x <= b) bounds ==> A)`,
  GEN_TAC THEN
    MATCH_MP_TAC list_INDUCT THEN REPEAT STRIP_TAC THENL
    [
      REWRITE_TAC[Sphere.ineq; ALL];
      ALL_TAC
    ] THEN
    MP_TAC (ISPEC `a0:real#real#real` PAIR_SURJECTIVE) THEN
    DISCH_THEN (X_CHOOSE_THEN `a:real` MP_TAC) THEN
    DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
    MP_TAC (ISPEC `y:real#real` PAIR_SURJECTIVE) THEN
    DISCH_THEN (X_CHOOSE_THEN `x:real` MP_TAC) THEN
    DISCH_THEN (X_CHOOSE_THEN `b:real` MP_TAC) THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    ASM_SIMP_TAC[Sphere.ineq; ALL; IMP_IMP]);;


(* delta = delta_x *)	
let DELTA_EQ_DELTA_X = prove(`!x1 x2 x3 x4 x5 x6. 
			       delta x1 x2 x3 x6 x5 x4 = delta_x x1 x2 x3 x4 x5 x6`,
  REPEAT GEN_TAC THEN
    REWRITE_TAC[Sphere.delta_x; Collect_geom.delta] THEN
    REAL_ARITH_TAC);;


(* Connection between delta_x and delta_x4 *)
let DELTA_X_AND_DELTA_X4 = prove(`!x1 x2 x3 x4 x5 x6.
				 (let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
				 let d = delta_x x1 x2 x3 x4 x5 x6 in
				 let v1 = ups_x x1 x2 x6 in
				 let v2 = ups_x x1 x3 x5 in
				 &4 * x1 * d = v1 * v2 - d4 * d4)`,
  REPEAT GEN_TAC THEN 
    REPEAT (CONV_TAC let_CONV) THEN
    REWRITE_TAC[Sphere.delta_x4; Sphere.delta_x; Sphere.ups_x] THEN
    REAL_ARITH_TAC);;




(* dihV = dih_y *)
let DIHV_EQ_DIH_Y = prove(`!v0:real^3 v1 v2 v3. ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3}
			    ==> (let v01 = dist (v0, v1) in
				 let v02 = dist (v0, v2) in
				 let v03 = dist (v0, v3) in
				 let v12 = dist (v1, v2) in
				 let v13 = dist (v1, v3) in
				 let v23 = dist (v2, v3) in
				   dihV v0 v1 v2 v3 = dih_y v01 v02 v03 v23 v13 v12)`,
  REPEAT GEN_TAC THEN
    DISCH_TAC THEN
    FIRST_ASSUM (MP_TAC o (fun th -> CONJUNCT2 (MATCH_MP (let_RULE Trigonometry.OJEKOJF) th))) THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
    REPEAT (CONV_TAC let_CONV) THEN
    MAP_EVERY ABBREV_TAC [`v01 = dist(v0:real^3,v1)`; `v02 = dist(v0:real^3,v2)`;
			  `v03 = dist(v0:real^3,v3)`; `v12 = dist(v1:real^3,v2)`;
			  `v13 = dist(v1:real^3,v3)`; `v23 = dist(v2:real^3,v3)`;
			  `d = delta_x (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`;
			  `d4 = delta_x4 (v01 pow 2) (v02 pow 2) (v03 pow 2) (v23 pow 2) (v13 pow 2) (v12 pow 2)`] THEN
    REWRITE_TAC[let_RULE Sphere.dih_y; let_RULE Sphere.dih_x; GSYM REAL_POW_2] THEN
    ASM_REWRITE_TAC[REAL_ARITH `a - b = a + c <=> c = --b`] THEN
    
    MATCH_MP_TAC Trigonometry1.ATN2_RNEG THEN
    DISJ_CASES_TAC (TAUT `~(d4 = &0) \/ d4 = &0`) THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC SQRT_POS_LT THEN

    MP_TAC (let_RULE (SPECL [`v01 pow 2`; `v02 pow 2`; `v03 pow 2`; `v23 pow 2`; `v13 pow 2`; `v12 pow 2`] DELTA_X_AND_DELTA_X4)) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ARITH `a - &0 * &0 = a`]) THEN
    
    MP_TAC (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT) THEN
    ASM_REWRITE_TAC[] THEN
    MP_TAC (INST [`v3:real^3`,`v2:real^3`] (let_RULE Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)) THEN
    ASM_REWRITE_TAC[] THEN
    REPEAT DISCH_TAC THEN
    MATCH_MP_TAC REAL_LT_MUL THEN
    ASM_REWRITE_TAC[]);;

	

    

(************************************************************************************)	


 (* Properties of a contravening packing *)
 
 (* LEMMA: aux *)
 let DIFF_LEMMA = prove(`!A B. A SUBSET B ==> (A = B DIFF (B DIFF A))`,
		       REWRITE_TAC[SUBSET; EXTENSION; IN_DIFF; DE_MORGAN_THM] THEN
			 REWRITE_TAC[TAUT `P /\ (~P \/ Q) <=> P /\ Q`] THEN
			 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[]);;



(* (V,ESTD V) is a fan for a contravening packing V *)
let CONTRAVENING_FAN = prove(`!V. contravening V ==> FAN (vec 0,V,ESTD V)`,
   REWRITE_TAC[contravening] THEN
     GEN_TAC THEN REWRITE_TAC[GSYM IMP_IMP] THEN
     REPLICATE_TAC 5 DISCH_TAC THEN
     REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
     MATCH_MP_TAC Ckqowsa.CKQOWSA THEN
     ASM_REWRITE_TAC[] THEN
     POP_ASSUM (LABEL_TAC "A") THEN DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN
     ASM_REWRITE_TAC[CARD_CLAUSES] THEN
     ARITH_TAC);;
     



(* LEMMA: aux *)
let CONTRAVENING_IMP_SURROUNDED = prove(`!V v. contravening V /\ v IN V ==> surrounded_node (V,ESTD V) v`,
					ASM_SIMP_TAC[contravening]);;


let CONTRAVENING_IMP_FULLY_SURROUNDED = prove(`!V. FAN (vec 0,V,ESTD V) /\ contravening V 
					      ==> fully_surrounded (V,ESTD V)`,
   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[FULLY_SURROUNDED] THEN
     REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[CONTRAVENING_IMP_SURROUNDED]);;
    


(* LEMMA: general *)
let CONTRAVENING_IMP_IN_DART1_OF_FAN = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
						 ==> x IN dart1_of_fan (V,ESTD V)`,
   REPEAT GEN_TAC THEN
     MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN
     ASSUME_TAC (SPEC `V:real^3->bool` CONTRAVENING_FAN) THEN
     MATCH_MP_TAC SURROUNDED_IMP_IN_DART1_OF_FAN THEN
     ASM_SIMP_TAC[] THEN
     MATCH_MP_TAC CONTRAVENING_IMP_SURROUNDED THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x':real^3`; `y:real^3`] PAIR_IN_DART_OF_FAN) THEN
     ASM_SIMP_TAC[]);;


(* LEMMA: general *)
let CONTRAVENING_IMP_DART_FST_NEQ_SND = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
						==> ~(FST x = SND x)`,
   REPEAT STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART1_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ THEN
     MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `ESTD V`] THEN
     ASM_REWRITE_TAC[]);;
     



(* LEMMA: general *)
let CONTRAVENING_DIST = prove(`!V v. contravening V /\ v IN V
			      ==> #2.0 <= dist(vec 0, v) /\ dist(vec 0,v) <= #2.52
			       /\ (!w. w IN V /\ ~(v = w) ==> #2.0 <= dist(v, w))`,
   REPEAT GEN_TAC THEN
     REWRITE_TAC[contravening] THEN
     DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
     DISCH_THEN (CONJUNCTS_THEN2 MP_TAC (MP_TAC o CONJUNCT1)) THEN
     REWRITE_TAC[Pack_defs.ball_annulus; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
     REWRITE_TAC[SUBSET; IN_DIFF; cball; ball; IN_ELIM_THM; REAL_NOT_LT] THEN
     DISCH_THEN (MP_TAC o SPEC `v:real^3`) THEN
     ASM_SIMP_TAC[REAL_ARITH `&2 = #2.0`] THEN
     DISCH_THEN (fun th -> ALL_TAC) THEN
     REWRITE_TAC[Sphere.packing; REAL_ARITH `#2.0 = &2`] THEN
     ASM SET_TAC[]);;
	 
	 
(* LEMMA: aux *)
let IN_ESTD = prove(`!V v w. {v,w} IN ESTD V <=> v IN V /\ w IN V /\ ~(v = w) /\ dist(v,w) <= #2.52`,
    REPEAT GEN_TAC THEN
      REWRITE_TAC[ESTD; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
      EQ_TAC THENL
      [
	REWRITE_TAC[IN_ELIM_THM] THEN
	  STRIP_TAC THEN
	  SUBGOAL_THEN `(v:real^3 = v' /\ w:real^3 = w') \/ (v = w' /\ w = v')` MP_TAC THENL
	  [
	    POP_ASSUM MP_TAC THEN SET_TAC[];
	    ALL_TAC
	  ] THEN
	  ASM_MESON_TAC[DIST_SYM];
	SET_TAC[]
      ]);;


(* LEMMA: general *)
let CONTRAVENING_ESTD_DIST = prove(`!V v w. contravening V /\ v IN V /\ w IN V /\ {v,w} IN ESTD V
				   ==> #2.0 <= dist(v,w) /\ dist(v,w) <= #2.52`,
   REPEAT GEN_TAC THEN
     REWRITE_TAC[contravening; IN_ESTD; Sphere.packing] THEN
     DISCH_THEN (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
     DISCH_THEN (MP_TAC o CONJUNCT1) THEN
     ASM_REWRITE_TAC[REAL_ARITH `#2.0 = &2`] THEN
     ASM SET_TAC[]);;



(* LEMMA: general *)
let CONTRAVENING_DART_DIST = prove(`!V x. contravening V /\ x IN dart_of_fan (V,ESTD V)
				     ==> #2.0 <= dist x /\ dist x <= #2.52`,
   REPEAT GEN_TAC THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC CONTRAVENING_ESTD_DIST THEN
     EXISTS_TAC `V:real^3->bool` THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_SURROUNDED) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[]);;
			

    

(* LEMMA: general *)
let CONTRAVENING_LMFUN_BOUND = prove(`!V v. contravening V /\ v IN V
				       ==> lmfun (norm v / &2) <= &1`,
   REPEAT GEN_TAC THEN 
     DISCH_THEN (MP_TAC o (fun th -> MATCH_MP CONTRAVENING_DIST th)) THEN
     REWRITE_TAC[DIST_SYM] THEN
     REWRITE_TAC[dist; VECTOR_SUB_RZERO; Pack_defs.lmfun; Pack_defs.h0] THEN
     REAL_ARITH_TAC);;





(* LEMMA: aux *)
let CONTRAVENING_IMP_AZIM_DART_EQ_AZIM = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
			==> azim_dart (V,ESTD V) (v,w) = azim (vec 0) v w (sigma_fan (vec 0) V (ESTD V) v w)`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_DART_FST_NEQ_SND) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`] SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_IMP_SURROUNDED) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
     ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[azim_dart; azim_fan; ARITH_RULE `a >= 3 ==> a > 1`]);;




(* 0, v, w, and sigma(v)(w) are not coplanar *)
let CONTRAVENING_IMP_NOT_COPLANAR = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
			    ==> ~coplanar {vec 0, v, w, sigma_fan (vec 0) V (ESTD V) v w}`,
   REPEAT GEN_TAC THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN  
     MP_TAC (SPECL [`V:real^3->bool`; `v:real^3,w:real^3`] CONTRAVENING_IMP_IN_DART1_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `sigma_fan (vec 0) V (ESTD V) v w`] AZIM_EQ_0_PI_EQ_COPLANAR) THEN
     ANTS_TAC THENL
     [
       MATCH_MP_TAC DART1_NOT_COLLINEAR_2 THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     REWRITE_TAC[DE_MORGAN_THM] THEN
     ASM_SIMP_TAC[GSYM CONTRAVENING_IMP_AZIM_DART_EQ_AZIM] THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`) THEN
	 MATCH_MP_TAC AZIM_DART_POS THEN
	 ASM_REWRITE_TAC[];
       MATCH_MP_TAC (REAL_ARITH `a < pi ==> ~(a = pi)`) THEN
	 MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
	 ASM_REWRITE_TAC[fully_surrounded] THEN
	 DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
	 ASM_SIMP_TAC[]
     ]);;
	 
	 

 

(* azim_dart = dih_y *)	 
let CONTRAVENING_AZIM_DART_EQ_DIH_Y = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V)
		==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
		    let y1 = norm v in
		    let y2 = norm w in
		    let y3 = norm w' in
		    let y4 = dist (w,w') in
		    let y5 = dist (v,w') in
		    let y6 = dist (v,w) in
		      azim_dart (V,ESTD V) (v,w) = dih_y y1 y2 y3 y4 y5 y6`,
   REPEAT STRIP_TAC THEN REPEAT (CONV_TAC let_CONV) THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_AZIM_DART_EQ_AZIM) THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_NOT_COPLANAR) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN

     SUBGOAL_THEN `~collinear {vec 0, v, w:real^3} /\ ~collinear {vec 0, v, w'}` ASSUME_TAC THENL
     [
       CONJ_TAC THEN MATCH_MP_TAC NOT_COPLANAR_NOT_COLLINEAR THENL
	 [
	   EXISTS_TAC `w':real^3` THEN ASM_REWRITE_TAC[];
	   EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[SET_RULE `{a:real^3,b,c,d} = {a,b,d,c}`]
	 ];
       ALL_TAC
     ] THEN
     
     MP_TAC ((let_RULE o SPECL [`vec 0:real^3`; `v:real^3`; `w:real^3`; `w':real^3`]) DIHV_EQ_DIH_Y) THEN
     ASM_REWRITE_TAC[DIST_0] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     MATCH_MP_TAC AZIM_DIHV_SAME THEN
     POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
     POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
     ASM_REWRITE_TAC[fully_surrounded] THEN
     DISCH_THEN (MP_TAC o SPEC `v:real^3,w:real^3`) THEN
     ASM_SIMP_TAC[]);;



      
(* Lower bound for CARD(face) in a contravening packing *)
let CONTRAVENING_IMP_CARD_FACE_GE_3 = prove(`!V. contravening V
		      ==> (!x. x IN dart_of_fan (V,ESTD V) ==> CARD (face (hypermap_of_fan (V,ESTD V)) x) >= 3)`,
			    MESON_TAC[CONTRAVENING_FAN; FULLY_SURROUNDED_IMP_CARD_FACE_GE_3; CONTRAVENING_IMP_FULLY_SURROUNDED]);;



(* Alternative form for type_of_node H x *)
let NODE_TYPE_lemma = prove(`!H (x:A). simple_hypermap H /\ x IN dart H
		    ==> type_of_node H x = CARD {y | y IN node H x /\ CARD (face H y) = 3},
			                   CARD {y | y IN node H x /\ CARD (face H y) = 4},
			                   CARD {y | y IN node H x /\ CARD (face H y) >= 5}`,
   REPEAT GEN_TAC THEN
     DISCH_THEN (MP_TAC o (fun th -> MATCH_MP SIMPLE_HYPERMAP_lemma th)) THEN
     REWRITE_TAC[type_of_node] THEN
     REWRITE_TAC[set_of_triangles_meeting_node; set_of_quadrilaterals_meeting_node; set_of_exceptional_meeting_node] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;


(* CARD (node) = p + q + r *)
let FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE = 
  prove(`!V E x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
	  fully_surrounded (V,E) /\ x IN dart_of_fan (V,E)
	==> (let p,q,r = type_of_node (hypermap_of_fan (V,E)) x in
	       CARD (node (hypermap_of_fan (V,E)) x) = p + q + r)`,
   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`hypermap_of_fan (V:real^3->bool,E)`; `x:real^3#real^3`] NODE_TYPE_lemma) THEN
     ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
     DISCH_THEN (fun th -> ALL_TAC) THEN
     CONV_TAC let_CONV THEN
     ABBREV_TAC `H = hypermap_of_fan (V:real^3->bool,E)` THEN
     ABBREV_TAC `A = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 3}` THEN
     ABBREV_TAC `B = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) = 4}` THEN
     ABBREV_TAC `C = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 5}` THEN
     MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `x:real^3#real^3`] FULLY_SURROUNDED_NODE_DECOMPOSITION) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (MP_TAC o let_RULE) THEN
     ABBREV_TAC `D = {y:real^3#real^3 | y IN node H x /\ CARD (face H y) >= 4}` THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN 

     SUBGOAL_THEN `CARD (B:real^3#real^3->bool) + CARD (C:real^3#real^3->bool) = CARD (D:real^3#real^3->bool)` MP_TAC THENL
     [
       MATCH_MP_TAC CARD_UNION_EQ THEN
	 ASM_SIMP_TAC[GSYM DISJOINT];
       ALL_TAC
     ] THEN

     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     MATCH_MP_TAC EQ_SYM THEN
     MATCH_MP_TAC CARD_UNION_EQ THEN
     ASM_SIMP_TAC[Hypermap.NODE_FINITE; GSYM DISJOINT]);;

	 
	 
(******************************************************************************)


(* tauVEF = taum for a triangular face *)
let tauVEF_EQ_taum = prove(`!V f. contravening V /\
			     f IN face_set_of_fan (V,ESTD V) /\
			     CARD (f) = 3 
        ==> (!v w. (v,w) IN f ==>
	     let w' = sigma_fan (vec 0) V (ESTD V) v w in
	     let y1 = norm v in
	     let y2 = norm w in
	     let y3 = norm w' in
	     let y4 = dist(w,w') in
	     let y5 = dist(v,w') in
	     let y6 = dist(v,w) in
	       tauVEF (V,ESTD V,f) = taum y1 y2 y3 y4 y5 y6)`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     UNDISCH_TAC `f IN face_set_of_fan (V,ESTD V)` THEN
     REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face; IN_ELIM_THM] THEN
     ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `face (hypermap_of_fan (V,ESTD V)) (v,w) = f` MP_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN
	 MATCH_MP_TAC (GSYM Hypermap.lemma_face_identity) THEN
	 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `(v,w) IN dart1_of_fan (V,ESTD V)` MP_TAC THENL
     [
       MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `f:real^3#real^3->bool` THEN
         ASM_REWRITE_TAC[] THEN
         MATCH_MP_TAC FACE_SUBSET_DART1_OF_FAN THEN
         ASM_SIMP_TAC[CONTRAVENING_IMP_IN_DART1_OF_FAN];
       ALL_TAC
     ] THEN
     REMOVE_ASSUM THEN REMOVE_ASSUM THEN
     REPEAT DISCH_TAC THEN
     REPEAT (CONV_TAC let_CONV) THEN
     ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
     REWRITE_TAC[tauVEF] THEN
     MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE)) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `(w,w') IN dart1_of_fan (V,ESTD V) /\ w',v IN dart1_of_fan (V,ESTD V)` ASSUME_TAC THENL
     [
       CONJ_TAC THEN MATCH_MP_TAC IN_FACE_IMP_IN_DART1_OF_FAN THEN EXISTS_TAC `v:real^3,w:real^3` THEN ASM_REWRITE_TAC[IN_INSERT];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     ASM_SIMP_TAC[Hypermap.FINITE_TWO_ELEMENTS; Hypermap.FINITE_SINGLETON; SUM_CLAUSES; SUM_SING] THEN
     SUBGOAL_THEN `~(v,w IN {(w,w'), (w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL
     [
       REWRITE_TAC[IN_INSERT; PAIR_EQ; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
	 MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `~(w,w' IN {(w':real^3,v:real^3)})` (fun th -> REWRITE_TAC[th]) THENL
     [
       REWRITE_TAC[IN_SING; PAIR_EQ] THEN
	 MP_TAC (ISPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN
     REWRITE_TAC[sol0_over_pi_EQ_const1] THEN
     ABBREV_TAC `a1 = azim_dart (V,ESTD V) (v,w)` THEN
     ABBREV_TAC `a2 = azim_dart (V,ESTD V) (w,w')` THEN
     ABBREV_TAC `a3 = azim_dart (V,ESTD V) (w',v)` THEN
     ABBREV_TAC `l1 = lmfun (h_dart (v:real^3,w:real^3))` THEN
     ABBREV_TAC `l2 = lmfun (h_dart (w:real^3,w':real^3))` THEN
     ABBREV_TAC `l3 = lmfun (h_dart (w':real^3,v:real^3))` THEN
     SUBGOAL_THEN `(pi + sol0) = pi * (&1 + const1)` (fun th -> REWRITE_TAC[th]) THENL
     [
       MP_TAC sol0_over_pi_EQ_const1 THEN
	 MP_TAC PI_POS THEN
	 CONV_TAC REAL_FIELD;
       ALL_TAC
     ] THEN
     
     REWRITE_TAC[Sphere.taum; Sphere.sol_y; Sphere.lnazim] THEN
     SUBGOAL_THEN `v,w IN dart_of_fan (V,ESTD V) /\ w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
     [
       REPEAT CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN EXISTS_TAC `dart1_of_fan (V,ESTD V)` THEN ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
       ALL_TAC
     ] THEN

     MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `v:real^3`; `w:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
     MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w:real^3`; `w':real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
     MP_TAC (let_RULE (SPECL [`V:real^3->bool`; `w':real^3`; `v:real^3`] CONTRAVENING_AZIM_DART_EQ_DIH_Y)) THEN
     ASM_REWRITE_TAC[DIST_SYM] THEN
     REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[SYM th])) THEN
     
     MP_TAC (SPEC `v:real^3,w:real^3` ly_EQ_lmfun) THEN
     MP_TAC (SPEC `w:real^3,w':real^3` ly_EQ_lmfun) THEN
     MP_TAC (SPEC `w':real^3,v:real^3` ly_EQ_lmfun) THEN

     MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN
     
     ASM_REWRITE_TAC[] THEN
     SUBGOAL_THEN `w' IN V /\ w IN V /\ v IN (V:real^3->bool)` (fun th -> REWRITE_TAC[th]) THENL
     [
       MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
	 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN
	 MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w':real^3`; `v:real^3`] PAIR_IN_DART_OF_FAN) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN
     SIMP_TAC[DIST_0; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
     REPEAT (DISCH_THEN (fun th -> ALL_TAC)) THEN
     REAL_ARITH_TAC);;


let CONTRAVENING_TAUVEF_EQ_TAUM = prove(`!V v w. contravening V /\ 
					       (v,w) IN dart_of_fan (V,ESTD V) /\
					       CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3
                                         ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
					     let y1 = norm v in
					     let y2 = norm w in
					     let y3 = norm w' in
					     let y4 = dist(w,w') in
					     let y5 = dist(v,w') in
					     let y6 = dist(v,w) in
					       tauVEF (V,ESTD V,face (hypermap_of_fan (V,ESTD V)) (v,w)) = taum y1 y2 y3 y4 y5 y6`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `face (hypermap_of_fan (V,ESTD V)) (v,w)`] tauVEF_EQ_taum) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[face_set_of_fan; Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
	 REWRITE_TAC[IN_ELIM_THM] THEN
	 EXISTS_TAC `v:real^3,w:real^3` THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN];
       ALL_TAC
     ] THEN
     DISCH_THEN MATCH_MP_TAC THEN
     REWRITE_TAC[Hypermap.face_refl]);;


(* Bounds for distances in a triangular face *)
	 
let CONTRAVENING_TRIANGULAR_FACE_DIST = prove(`!V v w. contravening V /\ (v,w) IN dart_of_fan (V,ESTD V) /\
						CARD (face (hypermap_of_fan (V,ESTD V)) (v,w)) = 3
    ==> let w' = sigma_fan (vec 0) V (ESTD V) v w in
        let y1 = norm v in
	let y2 = norm w in
	let y3 = norm w' in
	let y4 = dist(w,w') in
	let y5 = dist(v,w') in
	let y6 = dist(v,w) in
	  (&2 <= y1 /\ y1 <= #2.52) /\
	  (&2 <= y2 /\ y2 <= #2.52) /\
	  (&2 <= y3 /\ y3 <= #2.52) /\
	  (&2 <= y4 /\ y4 <= #2.52) /\
	  (&2 <= y5 /\ y5 <= #2.52) /\
	  (&2 <= y6 /\ y6 <= #2.52)`,
    REPEAT STRIP_TAC THEN CONV_TAC (DEPTH_CONV let_CONV) THEN
      MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
      ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
      MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] TRIANGULAR_FACE) THEN
      ASM_REWRITE_TAC[] THEN
      ANTS_TAC THENL
      [
	MATCH_MP_TAC CONTRAVENING_IMP_IN_DART1_OF_FAN THEN
	  ASM_REWRITE_TAC[];
	ALL_TAC
      ] THEN
      CONV_TAC (DEPTH_CONV let_CONV) THEN
      DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
      SUBGOAL_THEN `w,w' IN dart_of_fan (V,ESTD V) /\ w',v IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
      [
	CONJ_TAC THEN MATCH_MP_TAC Hypermap.lemma_in_subset THEN 
	  EXISTS_TAC `face (hypermap_of_fan (V,ESTD V)) (v,w)` THEN
	  ASM_SIMP_TAC[FACE_SUBSET_DART_OF_FAN; IN_INSERT];
	ALL_TAC
      ] THEN
      SUBGOAL_THEN `v IN V /\ w IN V /\ w' IN (V:real^3->bool)` ASSUME_TAC THENL
      [
	MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `v:real^3`; `w:real^3`] PAIR_IN_DART_OF_FAN) THEN
	  MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `w:real^3`; `w':real^3`] PAIR_IN_DART_OF_FAN) THEN
	  ASM_SIMP_TAC[];
	ALL_TAC
      ] THEN
      REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN
      MP_TAC (SPECL [`V:real^3->bool`; `v:real^3`] CONTRAVENING_DIST) THEN
      MP_TAC (SPECL [`V:real^3->bool`; `w:real^3`] CONTRAVENING_DIST) THEN
      MP_TAC (SPECL [`V:real^3->bool`; `w':real^3`] CONTRAVENING_DIST) THEN
      ASM_REWRITE_TAC[DIST_0] THEN
      REPEAT (DISCH_THEN (fun th -> REWRITE_TAC[th])) THEN
      MAP_EVERY (fun tm -> MP_TAC (SPECL [`V:real^3->bool`; tm] CONTRAVENING_DART_DIST)) [`v:real^3,w:real^3`; `w:real^3,w':real^3`; `w':real^3,v:real^3`] THEN
      ASM_SIMP_TAC[DIST_SYM]);;
	 

(* Bounds for azim_dart in a triangular face *)

let azim_dart_bounds_3_list = map (fun id -> (hd (Ineq.getexact id)).ineq) ["5735387903"; "5490182221"];;

let azim_dart_bounds_3 = list_mk_conj azim_dart_bounds_3_list;;

let TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl = mk_imp (azim_dart_bounds_3,
						     `!V x. contravening V /\
						       x IN dart_of_fan (V,ESTD V) /\
						       CARD (face (hypermap_of_fan (V,ESTD V)) x) = 3
                                                         ==> #0.852 < azim_dart (V,ESTD V) x /\ azim_dart (V,ESTD V) x < #1.893`);;

(* g(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl);; *)
let TRIANGULAR_FACE_AZIM_DART_BOUNDS = prove(TRIANGULAR_FACE_AZIM_DART_BOUNDS_concl,
   REWRITE_TAC[Ineq.dart_std3; INEQ_ALT; ALL; Pack_defs.h0; REAL_ARITH `&2 * #1.26 = #2.52`] THEN
     STRIP_TAC THEN

     REPEAT GEN_TAC THEN STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN

     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_AZIM_DART_EQ_DIH_Y) THEN
     ASM_REWRITE_TAC[] THEN CONV_TAC (DEPTH_CONV let_CONV) THEN
     ABBREV_TAC `w' = sigma_fan (vec 0) V (ESTD V) v w` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN

     MP_TAC (SPEC_ALL CONTRAVENING_TRIANGULAR_FACE_DIST) THEN
     ASM_REWRITE_TAC[] THEN
     CONV_TAC (DEPTH_CONV let_CONV) THEN
     REWRITE_TAC[REAL_ARITH `&2 = #2.0`] THEN
     DISCH_TAC THEN

     CONJ_TAC THENL
     [
       REWRITE_TAC[GSYM real_gt] THEN
	 FIRST_X_ASSUM MATCH_MP_TAC THEN
	 ASM_REWRITE_TAC[];
       FIRST_X_ASSUM MATCH_MP_TAC THEN
	 ASM_REWRITE_TAC[]
     ]);;



(******************************************************************************)	 
	 
(* Properties of rho_node (might be useful) *)
(*	 
let RHO_NODE_lemma = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
			     f IN face_set (hypermap_of_fan (V,E)) /\ x IN f
			   ==> ?!w. (FST x,w) IN f`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[EXISTS_UNIQUE] THEN
     EXISTS_TAC `SND (x:real^3#real^3)` THEN
     ASM_REWRITE_TAC[PAIR] THEN
     REPEAT STRIP_TAC THEN
     MP_TAC (INST [`FST (x:real^3#real^3),y:real^3`, `y:real^3#real^3`] (SPEC_ALL HYPERMAP_OF_FAN_FACE_NODE_INJ)) THEN
     ASM_REWRITE_TAC[] THEN
     ONCE_REWRITE_TAC[GSYM PAIR] THEN
     REWRITE_TAC[PAIR_EQ; EQ_SYM_EQ]);;




let RHO_NODE_LEMMA = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
			    f IN face_set (hypermap_of_fan (V,E)) /\ x IN f
			    ==> rho_node (V,E,f) (FST x) = SND x`,
   REPEAT GEN_TAC THEN
     DISCH_TAC THEN
     MP_TAC (SPEC_ALL RHO_NODE_lemma) THEN ASM_REWRITE_TAC[EXISTS_UNIQUE] THEN
     STRIP_TAC THEN
     SUBGOAL_THEN `w = SND (x:real^3#real^3)` ASSUME_TAC THENL
     [
       MATCH_MP_TAC EQ_SYM THEN
	 POP_ASSUM (fun th -> MATCH_MP_TAC th) THEN
	 ASM_REWRITE_TAC[PAIR];
       ALL_TAC
     ] THEN
     REWRITE_TAC[rho_node] THEN
     MATCH_MP_TAC SELECT_UNIQUE THEN
     GEN_TAC THEN BETA_TAC THEN
     EQ_TAC THENL
     [
       DISCH_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o SPEC `y:real^3`) THEN
	 ASM_REWRITE_TAC[];
       DISCH_THEN (fun th -> ASM_REWRITE_TAC[th])
     ]);;




let RHO_NODE_EQ_FACE_MAP = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
				   x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
				   ==> f_fan_pair_ext (V,E) x = (rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x))`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[Hypermap.POWER_2; o_THM] THEN
     ABBREV_TAC `w = rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST (x:real^3#real^3))` THEN
     MATCH_MP_TAC HYPERMAP_OF_FAN_FACE_NODE_INJ THEN
     MAP_EVERY EXISTS_TAC [`V:real^3->bool`; `E:(real^3->bool)->bool`; `f:real^3#real^3->bool`] THEN
     ASM_REWRITE_TAC[] THEN

     SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
     [
       ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
	 REWRITE_TAC[IN_ELIM_THM] THEN
	 EXISTS_TAC `x:real^3#real^3` THEN
	 REWRITE_TAC[] THEN
	 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
	 REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN

     SUBGOAL_THEN `f_fan_pair_ext (V,E) x IN f` MP_TAC THENL
     [
       ASM_REWRITE_TAC[Hypermap.face; Hypermap.face_map] THEN
	 ASM_SIMP_TAC[HYPERMAP_OF_FAN; Hypermap.in_orbit_map1];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN

     CONJ_TAC THENL
     [
       REWRITE_TAC[rho_node] THEN
	 MATCH_MP_TAC (BETA_RULE (ISPECL [`(\w':real^3. (w:real^3,w') IN face (hypermap_of_fan (V,E)) x)`] SELECT_AX)) THEN
	 POP_ASSUM MP_TAC THEN
	 MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
	 ASM_REWRITE_TAC[Hypermap.face_refl] THEN
	 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
	 STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 DISCH_TAC THEN
	 EXISTS_TAC `inverse_sigma_fan (vec 0) V E y x'` THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
     ASM_REWRITE_TAC[Hypermap.face_refl] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN ASM_REWRITE_TAC[f_fan_pair_ext; f_fan_pair]);;
   


let RHO_NODE_POWER_EQ_FACE_MAP_POWER = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
					       x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
                                               ==> !i. (f_fan_pair_ext (V,E) POWER i) x = 
						   ((\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) POWER i) x`,
   REPEAT STRIP_TAC THEN
     ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN
     SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
     [
       ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
	 REWRITE_TAC[IN_ELIM_THM] THEN
	 EXISTS_TAC `x:real^3#real^3` THEN
	 REWRITE_TAC[] THEN
	 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
	 REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
     
     SPEC_TAC (`i:num`,`i:num`) THEN
     INDUCT_TAC THENL
     [
       REWRITE_TAC[Hypermap.POWER];
       ALL_TAC
     ] THEN
     
     REWRITE_TAC[ARITH_RULE `SUC i = 1 + i`; Hypermap.addition_exponents; Hypermap.POWER_1; o_THM] THEN
     ABBREV_TAC `y = (f_fan_pair_ext (V,E) POWER i) x` THEN
     MP_TAC (SPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`; `y:real^3#real^3`; `f:real^3#real^3->bool`] RHO_NODE_EQ_FACE_MAP) THEN
     FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (rator (concl th)) = `y:real^3#real^3`)) THEN
     ASM_REWRITE_TAC[] THEN
     
     SUBGOAL_THEN `y IN face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL
     [
       POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
	 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
	 REWRITE_TAC[Hypermap.orbit_map; IN_ELIM_THM] THEN
	 EXISTS_TAC `i:num` THEN
	 REWRITE_TAC[GE; LE_0];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `face (hypermap_of_fan (V,E)) x = face (hypermap_of_fan (V,E)) y` ASSUME_TAC THENL
     [
       MATCH_MP_TAC Hypermap.lemma_face_identity THEN
	 ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `y IN dart1_of_fan (V:real^3->bool,E)` (fun th -> REWRITE_TAC[th]) THENL
     [
       MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN
	 ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     EXPAND_TAC "g" THEN BETA_TAC THEN
     ASM_REWRITE_TAC[]);;
     




let ORBIT_MAP_FUN_EQ_lemma = prove(`!(f:A->A) g x. (!y. y IN orbit_map f x ==> g y = f y) 
				   ==> orbit_map g x = orbit_map f x`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC Hypermap.lemma_orbit_eq THEN
     INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER] THEN
     REWRITE_TAC[GSYM Hypermap.POWER] THEN
     ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     REWRITE_TAC[Hypermap.lemma_in_orbit]);;
     



let RHO_NODE_face = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
			    x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
			    ==> f = orbit_map (\x. rho_node (V,E,f) (FST x), (rho_node (V,E,f) POWER 2) (FST x)) x`,
   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     SUBGOAL_THEN `orbit_map (f_fan_pair_ext (V,E)) x = face (hypermap_of_fan (V,E)) x` ASSUME_TAC THENL
     [
       ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN];
       ALL_TAC
     ] THEN
     FIRST_ASSUM (fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
     MATCH_MP_TAC EQ_SYM THEN
     MATCH_MP_TAC ORBIT_MAP_FUN_EQ_lemma THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC EQ_SYM THEN BETA_TAC THEN
     MATCH_MP_TAC RHO_NODE_EQ_FACE_MAP THEN
     ASM_REWRITE_TAC[] THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `face (hypermap_of_fan (V,E)) x` THEN
	 ASM_SIMP_TAC[FACE_SUBSET_DART1_OF_FAN];
       ALL_TAC
     ] THEN
     MATCH_MP_TAC Hypermap.lemma_face_identity THEN
     ASM_REWRITE_TAC[]);;



let RHO_NODE_POWER = prove(`!V E f x. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
			    x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
                            ==> !i. ((\x. rho_node (V,E,f) (FST x),(rho_node (V,E,f) POWER 2) (FST x)) POWER i) x
			         = (\x. (rho_node (V,E,f) POWER i) (FST x), (rho_node (V,E,f) POWER (i + 1)) (FST x)) x`,
   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `f IN face_set (hypermap_of_fan (V,E))` MP_TAC THENL
     [
       ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
	 REWRITE_TAC[IN_ELIM_THM] THEN
	 EXISTS_TAC `x:real^3#real^3` THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
	 MATCH_MP_TAC Hypermap.lemma_in_subset THEN
	 EXISTS_TAC `dart1_of_fan (V:real^3->bool,E)` THEN
	 ASM_REWRITE_TAC[DART1_OF_FAN_SUBSET_DART_OF_FAN];
       ALL_TAC
     ] THEN	
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN

     SPEC_TAC (`i:num`, `i:num`) THEN
     INDUCT_TAC THEN BETA_TAC THENL
     [
       REWRITE_TAC[Hypermap.POWER; ARITH_RULE `0 + 1 = 1`; Hypermap.POWER_1; I_THM] THEN
	 MP_TAC (SPEC_ALL RHO_NODE_LEMMA) THEN
	 ASM_REWRITE_TAC[Hypermap.face_refl] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM; PAIR_EQ] THEN
     REWRITE_TAC[ARITH_RULE `SUC i + 1 = 2 + i`] THEN
     REWRITE_TAC[Hypermap.addition_exponents; o_THM]);;

*)

(* Alternative definition of the perimeter of a face *)
(*
let PERIMETER_lemma = prove(`!V E x f. FAN (vec 0,V,E) /\ simple_hypermap (hypermap_of_fan (V,E)) /\
			      x IN dart1_of_fan (V,E) /\ f = face (hypermap_of_fan (V,E)) x
                              ==> per (V,E,f) (FST x) (CARD f) = sum f (\(v,w). arcV (vec 0) v w)`,
   REPEAT STRIP_TAC THEN
     REWRITE_TAC[per] THEN
     ABBREV_TAC `g = (\x:real^3#real^3. rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) (FST x), (rho_node (V,E,f) POWER 2) (FST x))` THEN
     ABBREV_TAC `orbit = orbit_map (f_fan_pair_ext (V,E)) x` THEN

     SUBGOAL_THEN `0 < CARD (orbit:real^3#real^3->bool)` ASSUME_TAC THENL
     [
       SUBGOAL_THEN `FINITE (orbit:real^3#real^3->bool)` ASSUME_TAC THENL
	 [
 	   EXPAND_TAC "orbit" THEN
	     MATCH_MP_TAC Hypermap.lemma_orbit_finite THEN
 	     EXISTS_TAC `dart_of_fan (V,E)` THEN
	     ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN];
	   ALL_TAC
	 ] THEN
	 DISJ_CASES_TAC (ARITH_RULE `0 < CARD (orbit:real^3#real^3->bool) \/ CARD orbit = 0`) THEN ASM_REWRITE_TAC[] THEN
	 POP_ASSUM MP_TAC THEN
	 POP_ASSUM (MP_TAC o (MATCH_MP CARD_EQ_0)) THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 DISCH_TAC THEN
	 MP_TAC (ISPECL [`f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.orbit_reflect) THEN
	 ASM_REWRITE_TAC[NOT_IN_EMPTY];
       ALL_TAC
     ] THEN

     SUBGOAL_THEN `!i. arcV (vec 0:real^3) ((rho_node (V:real^3->bool,E:(real^3->bool)->bool,f:real^3#real^3->bool) POWER i) (FST (x:real^3#real^3))) ((rho_node (V,E,f) POWER (i + 1)) (FST x)) = ((\(v,w). arcV (vec 0) v w) o (\i. (g POWER i) x)) i` MP_TAC THENL
     [
       REWRITE_TAC[LAMBDA_PAIR; o_THM] THEN BETA_TAC THEN
	 MP_TAC (SPEC_ALL RHO_NODE_POWER) THEN
	 ASM_REWRITE_TAC[] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     
     SUBGOAL_THEN `f:real^3#real^3->bool = IMAGE (\i. (g:real^3#real^3->real^3#real^3 POWER i) x) (0..CARD f - 1)` MP_TAC THENL
     [
       ASM_REWRITE_TAC[GSYM IMAGE_LEMMA; IN_NUMSEG; LE_0] THEN
	 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
	 MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`; `CARD (orbit_map (f_fan_pair_ext (V,E)) x)`] FINITE_ORBIT_MAP) THEN
	 ASM_SIMP_TAC[SPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
	 DISCH_THEN (fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
	 MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN
	 ASM_REWRITE_TAC[] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 POP_ASSUM MP_TAC THEN
	 SIMP_TAC[ARITH_RULE `0 < c ==> !i. i < c <=> i <= c - 1`];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
     REWRITE_TAC[ETA_AX] THEN

     MATCH_MP_TAC (GSYM SUM_IMAGE) THEN

     X_GEN_TAC `n:num` THEN X_GEN_TAC `m:num` THEN
     REWRITE_TAC[IN_NUMSEG; LE_0] THEN
     ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
     MP_TAC (SPEC_ALL RHO_NODE_POWER_EQ_FACE_MAP_POWER) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     
     STRIP_TAC THEN
     SUBGOAL_THEN `inj_orbit (f_fan_pair_ext (V,E)) x (CARD (f:real^3#real^3->bool) - 1)` MP_TAC THENL
     [
       MP_TAC (ISPECL [`dart_of_fan (V:real^3->bool,E)`; `f_fan_pair_ext (V,E)`; `x:real^3#real^3`] Hypermap.lemma_segment_orbit) THEN
	 ASM_SIMP_TAC[ISPEC `vec 0:real^3` FINITE_DART_OF_FAN; F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN] THEN
	 DISCH_THEN (MP_TAC o SPEC `CARD (f:real^3#real^3->bool) - 1`) THEN
	 ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN] THEN
	 ANTS_TAC THENL
	 [
	   REPLICATE_TAC 3 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
	     ARITH_TAC;
	   SIMP_TAC[]
	 ];
       ALL_TAC
     ] THEN

     REWRITE_TAC[Hypermap.lemma_inj_orbit] THEN
     DISCH_THEN MATCH_MP_TAC THEN
     ASM_SIMP_TAC[Hypermap.face; Hypermap.face_map; HYPERMAP_OF_FAN]);;
*)


end;;