(* ========================================================================== *)
(* 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)`,
(* 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;;