(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALISATION                                              *)
(*                                                                            *)
(* Lemma: FATUGPD                                                             *)
(* Chapter: Tame                                                              *)
(* Author: Vuong Anh Quyen                                                    *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)


flyspeck_needs "hypermap/hypermap.hl";;
flyspeck_needs "fan/fan_defs.hl";;
flyspeck_needs "fan/planarity.hl";;
flyspeck_needs "leg/geomdetail.hl";;
flyspeck_needs "packing/pack2.hl";; (* for KIUMVTC  *)
flyspeck_needs "packing/pack_defs.hl";; (* for h0 def and others *)
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "general/prove_by_refinement.hl";;
flyspeck_needs "tame/tame_concl.hl";;
flyspeck_needs "tame/tame_defs.hl";;  (* was commented out *)

module Fatugpd = struct

open Hypermap;;
open Fan_defs;;
open Fan;;
open Planarity;;
open Pack_defs;;
open Pack1;;
open Pack2;;
open Tame_defs;;
open Trigonometry1;;
open Tame_defs;;
open Prove_by_refinement;;

let JBDNJJB = Planarity.JBDNJJB;;

(* my assumptions *)

  let UBHDEUU2_concl =  Tame_concl.UBHDEUU2_concl;;

  let UBHDEUU2_hypothesis = new_definition (mk_eq(`UBHDEUU2_hypothesis:bool`,UBHDEUU2_concl));;

  let UBHDEUU2_quasi = UNDISCH(MATCH_MP (TAUT `(x = y) ==> (x ==> y)`) UBHDEUU2_hypothesis);;


 (* my tatics *)

let Q_LABEL_TAC term phr = UNDISCH_THEN term (LABEL_TAC phr);;

let Q_ABBREV_TAC term str = (ABBREV_TAC term) THEN 
   FIRST_X_ASSUM (LABEL_TAC str);;

let Q_EXPAND_TAC str = (USE_THEN str (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));;

(* some of my lemmas that may help others *)
let NOT_EMPTY_IMAGE = prove
( ` !(S:A -> bool) (f:A->B). ~( S = {}) ==> ~( IMAGE f S = {})`, SET_TAC[]);;

(* lemma about sup of function on finite set *)
let finite_num_func_attain_max = 
prove_by_refinement(
`! (S:A->bool) (f:A->num). FINITE S /\ ~ (S = {}) 
     ==> (? x. x IN S /\ (! y. y IN S ==> f y <= f x))`,
[
  (REPEAT STRIP_TAC);

(* subgoal 1 *)
  (SUBGOAL_THEN 
` FINITE (IMAGE (& o(f:A->num)) (S:A->bool)) /\ ~ (IMAGE (& o f) S = {})`
ASSUME_TAC);
  CONJ_TAC;
(* subgoal 1.1 *)
  (ASM_SIMP_TAC[FINITE_IMAGE]);
(* subgoal 2.1 *)
  (ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);

  (FIRST_ASSUM(MP_TAC o (MATCH_MP SUP_FINITE)));
  (CONV_TAC(PAT_CONV `\k. _ IN k /\ _ ==> _` (REWRITE_CONV[IMAGE])));
  (PURE_REWRITE_TAC[IN_ELIM_THM]);
  STRIP_TAC;
  (EXISTS_TAC `x:A`);
  (ASM_SIMP_TAC[]);
  (REPEAT STRIP_TAC);
  (FIRST_X_ASSUM(MP_TAC o SPEC ` (& o (f:A->num)) y`));

(* subgoal 2 *)
  (SUBGOAL_THEN ` (& o (f:A->num)) y IN IMAGE (& o f) S` ASSUME_TAC);
  (PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
  (EXISTS_TAC `y:A` THEN ASM_SIMP_TAC[]);

    (ASM_SIMP_TAC[o_THM; REAL_OF_NUM_LE]);
]);;


(* lemma about property of sup *)
let sup_property1 = prove_by_refinement( 
`! (S:real->bool). ~(S = {}) /\(?b. !x. x IN S ==> x <= b) ==>
      (! epsilon. epsilon > &0 ==> ?x. x IN S /\ x > sup S - epsilon)`,
[
(GEN_TAC THEN DISCH_THEN  (MP_TAC o (MATCH_MP SUP)));
(STRIP_TAC THEN GEN_TAC);
(DISCH_THEN (ASSUME_TAC o (MATCH_MP (ARITH_RULE 
` epsilon > &0 ==> ~ ( sup (S:real->bool) <= sup S - epsilon)`))));
(MATCH_MP_TAC (MESON[] 
`! (P:A->bool) (Q:A->bool). ~(!(x:A). P x ==> ~ (Q x)) 
              ==> (?(x:A). P x /\ Q x)`));
(PURE_REWRITE_TAC[ARITH_RULE 
`~(x > sup S - epsilon) <=> x <= sup S - epsilon`]);
(ASM_MESON_TAC[]);]);;
 

(* lemma about maximal of num bounded function *)

let bdd_num_func_attain_max = prove_by_refinement(
`! (S:A ->bool) (f:A-> num). ~(S = {})/\(?m. !x. x IN S ==> f x <= m) 
      ==> (?x. x IN S /\ (!y. y IN S ==> f y  <= f x))`,
[
(REPEAT STRIP_TAC);
(* subgoal 1 *)
(SUBGOAL_THEN `~( IMAGE (& o (f:A->num)) (S:A->bool) = {}) 
  /\ (? b. ! y. y IN (IMAGE (& o f) S) ==> y <= b)` ASSUME_TAC);
(CONJ_TAC);

(* subgoal 1.1 *)
(ASM_SET_TAC[]);

(* subgoal 1.2 *)
(EXISTS_TAC `& (m:num)`);
(PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM]);
(REPEAT STRIP_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[REAL_OF_NUM_LE]);

(FIRST_ASSUM (MP_TAC o MATCH_MP SUP));
(ABBREV_TAC `p = sup (IMAGE (& o (f:A->num)) (S:A->bool))` THEN STRIP_TAC);
(* subgoal 2 *)
(SUBGOAL_THEN 
`?z. z IN (IMAGE (& o (f:A->num)) (S:A->bool)) /\ z > p - &1` MP_TAC);
(EXPAND_TAC "p");
(FIRST_ASSUM (MP_TAC o (SPEC `&1`) o (MATCH_MP sup_property1)));
(SIMP_TAC[ARITH_RULE `&1 > &0`]);

(PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE;o_THM] THEN STRIP_TAC );
(EXISTS_TAC `x:A`);
(ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);
(MATCH_MP_TAC (ARITH_RULE ` n < (m:num) + 1 ==> n <= m`));
(* subgoal 3 *)
(SUBGOAL_THEN 
`&((f:A->num) y) IN (IMAGE (& o f) (S:A->bool))` ASSUME_TAC);
(ASM_SIMP_TAC[IN_ELIM_THM;o_THM;IMAGE]);
(EXISTS_TAC `y:A`);
(ASM_SIMP_TAC[]);

(* subgoal 4 *)
(SUBGOAL_THEN `&((f:A->num) y) <= p` ASSUME_TAC);
(ASM_SIMP_TAC[]);

(MATCH_MP_TAC 
  (fst(EQ_IMP_RULE (SPECL [`(f:A->num) y`;`f x + 1`] REAL_OF_NUM_LT))));
(PURE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD]);
(ASM_ARITH_TAC);
]);;


let BIJ_CARD_EQ = prove
( `! (V:A->bool) (U:B->bool) (f:A->B). FINITE V /\ BIJ f V U 
            ==> CARD U = CARD V`,
REPEAT GEN_TAC THEN REWRITE_TAC[BIJ;INJ;SURJ] THEN STRIP_TAC THEN
MATCH_MP_TAC CARD_EQ_CARD_IMP THEN ASM_SIMP_TAC[] THEN
ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c] 
THEN EXISTS_TAC `f:A->B` THEN ASM_MESON_TAC[]);;


(* another property of sup *)
let SUP_lt = prove_by_refinement(
`! (S:real -> bool) (b:real). 
~(S = {}) /\ FINITE S /\ (!x. x IN S ==> x < b)   ==> sup S < b`,
[
(REPEAT STRIP_TAC);
(FIRST_ASSUM (fun thm -> (MATCH_MP_TAC thm)));
(ASM_SIMP_TAC[SUP_FINITE]);
]);;


(* epsilon lemma *)
let epsilon_lemma = prove_by_refinement(
 `! (a:real) b. a < b ==> ? epsilon. epsilon > &0 /\ b > a + epsilon`,
[
(REPEAT STRIP_TAC);
(EXISTS_TAC `(b - a) / &2`);
ASM_ARITH_TAC;
]);;

let normalize = new_definition `!(v:real^N). normalize v = inv (norm v) % v`;;

let norm_normalize = prove_by_refinement(
 `! (v:real^3). ~(v = vec 0) ==> norm (normalize v) = &1 `,
[
(GEN_TAC THEN STRIP_TAC);
(PURE_REWRITE_TAC[normalize;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM]);
(MATCH_MP_TAC REAL_MUL_LINV);
(ASM_MESON_TAC[NORM_EQ_0]);
]);;
 

let normalize_vec_0 = prove_by_refinement(
 `normalize (vec 0:real^N) = (vec 0:real^N)`,
[(PURE_REWRITE_TAC[normalize;REAL_INV_0;NORM_0;VECTOR_MUL_LZERO]);
VECTOR_ARITH_TAC;]);;


let norm_mul_normalize = prove_by_refinement(
`! (v:real^3).(norm v) % (normalize v) = v`,
[
(GEN_TAC);
(ASM_CASES_TAC `v:real^3 = vec 0`);

(* subgoal 1 *)
(ASM_SIMP_TAC[normalize_vec_0; VECTOR_MUL_RZERO]);

(* subgoal 2 *)
(PURE_REWRITE_TAC[normalize;VECTOR_MUL_ASSOC]);
(SUBGOAL_THEN `~(norm (v:real^3) = &0)` (ASSUME_TAC o MATCH_MP REAL_MUL_RINV));
(ASM_MESON_TAC[NORM_EQ_0]);
(ASM_SIMP_TAC[VECTOR_MUL_LID]);]);;
 

let dot_normalize = prove_by_refinement(
 `! v:real^3. v dot (normalize v) = norm v`,
[
(GEN_TAC);
(ASM_CASES_TAC `v:real^3 = vec 0`);

(* subgoal 1 *)
(ASM_SIMP_TAC[NORM_0;DOT_LZERO]);

(* subgoal 2 *)
(SUBGOAL_THEN ` norm (v:real^3) * (v dot normalize v) = norm v pow 2` MP_TAC);
(ONCE_REWRITE_TAC[GSYM DOT_RMUL]);
(ASM_SIMP_TAC[norm_mul_normalize;DOT_SQUARE_NORM]);

(ONCE_REWRITE_TAC[REAL_POW_2]);
(MATCH_MP_TAC (REWRITE_RULE [TAUT `A /\ B ==> C <=> A ==> (B ==> C)`] REAL_EQ_LCANCEL_IMP));
(ASM_SIMP_TAC[NORM_EQ_0]);]);;


let fourier = prove_by_refinement(
 ` ! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3
==> v = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`,
[
(REPEAT STRIP_TAC);
(FIRST_ASSUM  (ASSUME_TAC o (MATCH_MP ORTHONORMAL_IMP_SPANNING)));
(UNDISCH_TAC `orthonormal (e1:real^3) e2 e3`);
(ONCE_REWRITE_TAC[orthonormal]);
(REPEAT STRIP_TAC);
(ABBREV_TAC `(u:real^3) = (v dot e1) % e1 + (v dot e2) % e2 + (v dot e3) % e3`);
(* subgoal 1 *)
(SUBGOAL_THEN ` (v:real^3) dot e1 =  u dot e1 `  ASSUME_TAC);
(EXPAND_TAC "u");
(ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
REAL_ADD_RID;REAL_MUL_RID]);

(* subgoal 2 *)
(SUBGOAL_THEN ` (v:real^3) dot e2 =  u dot e2 `  ASSUME_TAC);
(EXPAND_TAC "u");
(ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);

(* subgoal 3 *)
(SUBGOAL_THEN ` (v:real^3) dot e3 =  u dot e3 `  ASSUME_TAC);
(EXPAND_TAC "u");
(ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;REAL_MUL_RZERO;
REAL_ADD_RID;REAL_MUL_RID;REAL_ADD_LID]);

(* subgoal 4 *)
(SUBGOAL_THEN `(v:real^3) - u IN span {e1:real^3, e2, e3}` MP_TAC);
(ASM_SET_TAC[]);

(SIMP_TAC[SPAN_3;IN_ELIM_THM;IN_UNIV]);
(STRIP_TAC);

(* subgoal 5 *) 
(SUBGOAL_THEN `((v:real^3) - u) dot (v - u) = &0` MP_TAC);
(PURE_REWRITE_TAC[DOT_LSUB]);
(ASM_SIMP_TAC[DOT_RMUL;DOT_RADD;REAL_SUB_REFL]);

(ASM_SIMP_TAC[DOT_EQ_0;VECTOR_SUB_EQ]);]);;


let norm_lemma1 = prove_by_refinement(
`! (v:real^3) (e1:real^3) e2 e3. orthonormal e1 e2 e3 ==>
  norm v = sqrt ((v dot e1) pow 2 + (v dot e2) pow 2 + (v dot e3) pow 2)`,
[
(REPEAT STRIP_TAC);
(PURE_REWRITE_TAC[vector_norm]);
(FIRST_ASSUM (ASSUME_TAC o MATCH_MP fourier));
(FIRST_ASSUM (fun thm -> CONV_TAC (PAT_CONV `\x. sqrt (x dot x) = _` (ONCE_REWRITE_CONV[thm]))));
(PURE_REWRITE_TAC[DOT_RADD;DOT_LADD;DOT_RMUL;DOT_LMUL;
REAL_ADD_RDISTRIB;REAL_ADD_LDISTRIB]);
(ONCE_REWRITE_TAC[REAL_MUL_ASSOC]);
(ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
(FIRST_ASSUM (MP_TAC o MATCH_MP
(fst (EQ_IMP_RULE (SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`] orthonormal)))));
STRIP_TAC;
(ASM_SIMP_TAC[DOT_SYM;REAL_MUL_RZERO;REAL_ADD_RID;
REAL_ADD_LID;REAL_MUL_RID]);]);;


let coordinates_lemma = prove_by_refinement(
 `! (v:real^3) (e1:real^3) e2 e3 (x:real) y z. orthonormal e1 e2 e3 /\
  v = x % e1 + y % e2 + z % e3 ==>
     x = v dot e1 /\ y = v dot e2 /\ z = v dot e3`,
[
(REPEAT GEN_TAC);
(STRIP_TAC);
(FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` (MATCH_MP fourier thm))));
(ASM_MESON_TAC[ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT]);]);;


let dot_coordinates = prove_by_refinement(
 `! v:real^3 u e1 e2 e3. orthonormal e1 e2 e3
   ==> v dot u = (v dot e1) * (u dot e1) + (v dot e2) * (u dot e2)
                + (v dot e3) * (u dot e3)`,
[
(REPEAT STRIP_TAC);
(FIRST_ASSUM((LABEL_TAC "a") o (MATCH_MP (SPEC `u:real^3` fourier))));
(USE_THEN "a" (fun thm -> (CONV_TAC (PAT_CONV `\x. A dot x = B` 
    (ONCE_REWRITE_CONV[thm])))));
(ONCE_REWRITE_TAC[VECTOR_ARITH `(v:real^3) dot (a % e1 + b % e2 + c % e3) = 
   (v dot e1) * a + (v dot e2 ) * b + (v dot e3) * c`]);
(SIMP_TAC[]);]);;


let dot_coordinates_2 = prove_by_refinement(
 `! (v:real^3) u e1 e2 e3 x y z a b c. orthonormal e1 e2 e3 /\
   v = x % e1 + y % e2 + z % e3 /\ u = a % e1 + b % e2 + c % e3
 ==> v dot u = x * a + y * b + z * c`,
[(ONCE_REWRITE_TAC[orthonormal]);
(REPEAT STRIP_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[DOT_SYM;DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL]);
ARITH_TAC;]);;
 

let norm_lemma2 = prove_by_refinement(
 `! (v:real^3) e1 e2 e3 x y z. orthonormal e1 e2 e3 /\
   v = x % e1 + y % e2 + z % e3 ==>
   norm v = sqrt (x pow 2 + y pow 2 + z pow 2)`,
[
(REPEAT GEN_TAC);
(DISCH_TAC);
(FIRST_ASSUM (fun thm -> ONCE_REWRITE_TAC [ MATCH_MP norm_lemma1 (CONJUNCT1 thm)]));
(FIRST_ASSUM (fun thm -> SIMP_TAC[ MATCH_MP coordinates_lemma thm]));]);;
 

let dot_gt_0 = prove_by_refinement(
 `! v:real^3 u. &0 < v dot u <=> &0 < v dot normalize u `,
[
(REPEAT GEN_TAC);
(ASM_CASES_TAC `u:real^3 = vec 0`);

(* subgoal 1 *)
(ASM_SIMP_TAC[normalize_vec_0]);

(* subgoal 2 *)
( CONV_TAC(PAT_CONV `\x. &0 < A dot x <=> B`(ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
(PURE_REWRITE_TAC[DOT_RMUL]);
(MATCH_MP_TAC (CONJUNCT1 REAL_LT_MUL_EQ));
(MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ ~(x = &0) ==> &0 < x`));
(ASM_SIMP_TAC[NORM_POS_LE;NORM_EQ_0]);]);;


let dot_eq_0 = prove_by_refinement(
`! v:real^3 u. v dot u = &0 <=> (normalize v) dot u = &0`,
[
(REPEAT GEN_TAC);
(ASM_CASES_TAC `v:real^3 = vec 0`);

(* subgoal 1 *)
(ASM_SIMP_TAC[normalize_vec_0]);

(* subgoal 2 *)
(CONV_TAC(PAT_CONV `\x. x dot y = &0 <=> A` 
(ONCE_REWRITE_CONV[GSYM norm_mul_normalize])));
(ONCE_REWRITE_TAC[DOT_LMUL]);
(CONV_TAC(PAT_CONV `\x. x <=> A` (ONCE_REWRITE_CONV
[ARITH_RULE `&0 = norm (v:real^3) * &0`])));
(ONCE_REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);
(ASM_SIMP_TAC[NORM_EQ_0]);]);;


let azim_ge_azim_dart = prove_by_refinement(
 `! (V:real^3->bool) E w u v. FAN (vec 0, V, E) /\ w IN V /\ 
u IN set_of_edge w V E /\ v IN set_of_edge w V E /\ ~(w = u) /\ ~(v = u)
   ==> azim (vec 0) w u v >= azim_dart (V,E) (w,u)`,
[
(REPEAT STRIP_TAC);
(ASM_SIMP_TAC[azim_dart]);
(PURE_REWRITE_TAC[azim_fan]);

(* subgoal 1 *)
(SUBGOAL_THEN `CARD (set_of_edge (w:real^3) V E) > 1` ASSUME_TAC);
(MP_TAC (SPECL [`vec 0:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;
`u:real^3`;`w:real^3`] Fan.remark1_fan));
(ASM_SIMP_TAC[]);
(STRIP_TAC);
(MP_TAC(ISPECL [`v:real^3`;`u:real^3`] Hypermap.CARD_TWO_ELEMENTS));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (ARITH_RULE `(a:num) <= b ==> a = 2 ==> b > 1`));
(MATCH_MP_TAC CARD_SUBSET);
(ASM_SET_TAC[]);

(ASM_SIMP_TAC[]);
(* subgoal 2 *)
(SUBGOAL_THEN `~(set_of_edge (w:real^3) V E = {u})` ASSUME_TAC);
(ONCE_REWRITE_TAC[TAUT ` ~A <=> A ==> F`]);
(DISCH_THEN (MP_TAC o (AP_TERM `(\(S:real^3->bool). CARD S)`)));
(SIMP_TAC[BETA_THM;Geomdetail.CARD_SING]);
(ASM_ARITH_TAC);
(MP_TAC (SPECL [`vec 0 :real^3`;`V:real^3 -> bool`;
`E:(real^3->bool)->bool`;`w:real^3`;`u:real^3`] Fan.SIGMA_FAN));
(ASM_SIMP_TAC[]);
STRIP_TAC;
(ASM_SIMP_TAC[ARITH_RULE `a >= b <=> b <= a`]);]);;


(* FATUGPD *)

(* definitions in the proof *)

let set_of_iso = new_definition 
` set_of_iso W = {w| w IN W /\ set_of_edge w W (ECTC W) = {}}`;;


(* lemmas prepared for the proof *)
let lemma1 = prove_by_refinement(
 `! (S:real^3->bool). packing S /\ S SUBSET ball_annulus ==> FINITE S`,
[
(REPEAT STRIP_TAC);

(* subgoal 1 *)
(SUBGOAL_THEN ` (S:real^3->bool) = S INTER ball (vec 0,&3 * h0)` ASSUME_TAC);

(MATCH_MP_TAC (SET_RULE `! U V. U SUBSET ball_annulus /\ ball_annulus SUBSET V ==> (U = U INTER V)`));
(ASM_SIMP_TAC[ball_annulus;ball;cball;IN_DIFF;SUBSET;IN_ELIM_THM;h0]);
(REPEAT STRIP_TAC );
(MATCH_MP_TAC (ARITH_RULE ` u <= &2 * #1.26 ==> u < &3 * #1.26`));
(ASM_SIMP_TAC[]);

(ONCE_ASM_REWRITE_TAC[]);
(ASM_SIMP_TAC[KIUMVTC]);]);;


let lemma2 = prove_by_refinement(
 `! (V:real^3 -> bool) v. packing V /\ FINITE V /\ v IN V
==> ? epsilon. epsilon > &0 /\
  (! w. w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V)) 
          ==> dist (v,w) > &2 + epsilon )`,
[
(REPEAT STRIP_TAC);
(ABBREV_TAC `(S:real^3->bool) = {w|w IN V /\ ~(w = v) /\ ~(w IN set_of_edge v V (ECTC V))}`);

(ASM_CASES_TAC `(S:real^3 ->bool) = {}`);

(* subgoal 1 *)
(EXISTS_TAC `&1`);
(SIMP_TAC[ARITH_RULE `&1 > &0`]);
(REPEAT STRIP_TAC);
(* subgoal 1.1 *)
(SUBGOAL_THEN `~((S:real^3->bool) = {})` ASSUME_TAC);
(ASM_SET_TAC[]);

(ASM_MESON_TAC[]);

(* subgoal 2 *)

(* subgoal 2.1 *)
(SUBGOAL_THEN `FINITE (S:real^3 -> bool)` ASSUME_TAC);
(MATCH_MP_TAC 
  (ISPECL [`(S:real^3-> bool)`;`(V:real^3 ->bool)`] FINITE_SUBSET));
(ASM_SET_TAC[]);

(ABBREV_TAC `(f:real^3 -> real) = (\w. dist (v,w))`);
(* subgoal 2.2 *)
(SUBGOAL_THEN `&2 < inf (IMAGE (f:real^3 -> real) (S:real^3 ->bool))`         ASSUME_TAC);
(* subgoal 2.2.1 *)
(SUBGOAL_THEN 
  `FINITE (IMAGE (f:real^3 ->real) S) /\ ~ (IMAGE f S = {})` ASSUME_TAC);
(ASM_SIMP_TAC[FINITE_IMAGE;NOT_EMPTY_IMAGE]);

(ASM_SIMP_TAC[REAL_LT_INF_FINITE]);
(EXPAND_TAC "S");
(PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
(REPEAT STRIP_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(EXPAND_TAC "f");
(MATCH_MP_TAC (ARITH_RULE `! (a:real). &2 <= a /\ ~(&2 = a) ==> &2 < a`));
CONJ_TAC;
(* subgoal 2.2.3 *)
(UNDISCH_TAC `packing (V:real^3 -> bool)`);
(PURE_REWRITE_TAC[packing]);
(DISCH_THEN (fun thm -> MATCH_MP_TAC (ISPECL [`x':real^3`;`v:real^3`] thm)));
(ASM_MESON_TAC[IN]);

(* subgoal 2.2.4 *)
(SUBGOAL_THEN `&2 = dist (v,x') ==> (x' IN set_of_edge v V (ECTC V))` ASSUME_TAC);
(STRIP_TAC);
(PURE_REWRITE_TAC[set_of_edge]);
(ASM_SIMP_TAC[ECTC;IN_ELIM_THM]);
(EXISTS_TAC `v:real^3`);
(EXISTS_TAC `x':real^3`);
(ASM_SIMP_TAC[]);

(ASM_MESON_TAC[]);

(FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP epsilon_lemma)));
(FIRST_X_ASSUM CHOOSE_TAC);
(EXISTS_TAC `epsilon:real`);
(ASM_SIMP_TAC[]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC (ARITH_RULE `! u:real v w. u >= v /\ v > w ==> u > w`));
(EXISTS_TAC `inf (IMAGE (f:real^3 -> real) (S:real^3 -> bool))`);
(ASM_SIMP_TAC[]);

(* subgoal 2.3 *)
(SUBGOAL_THEN `dist (v,w:real^3) IN (IMAGE (f:real^3 -> real) S)` ASSUME_TAC);
(PURE_REWRITE_TAC[IMAGE;IN_ELIM_THM]);
(EXISTS_TAC `w:real^3`);
(CONJ_TAC);

(* subgoal 2.3.1 *)
(EXPAND_TAC "S");
(ASM_SIMP_TAC[IN_ELIM_THM]);

(* subgoal 2.3.2 *)
(EXPAND_TAC "f");
(SIMP_TAC[]);

(* subgoal 2.3.3 *)
(SUBGOAL_THEN `~(IMAGE (f:real^3 -> real) S = {}) 
  /\ (? b:real. !x. x IN (IMAGE f S) ==> b <= x )` ASSUME_TAC);
(ASM_SIMP_TAC[NOT_EMPTY_IMAGE]);
(EXISTS_TAC `&2`);
STRIP_TAC;
(EXPAND_TAC "f");
(PURE_REWRITE_TAC[IN_ELIM_THM;IMAGE]);
(REPEAT STRIP_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(SIMP_TAC[]);
(UNDISCH_TAC `packing (V:real^3 -> bool)`);
(PURE_REWRITE_TAC[packing]);
(DISCH_THEN (fun thm -> MP_TAC  (ISPECL [`v:real^3`;`x':real^3`] thm)));
(MATCH_MP_TAC (TAUT `U ==> ((U ==> V)==> V) `));

(CONV_TAC (PAT_CONV `\x y. x /\ y /\ _ ` (ONCE_REWRITE_CONV[GSYM IN])));
(ASM_SIMP_TAC[]);
(UNDISCH_TAC `(x':real^3) IN S`);
(EXPAND_TAC "S");
(PURE_REWRITE_TAC[IN_ELIM_THM]);
(SIMP_TAC[]);

(FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP INF)));
(ONCE_REWRITE_TAC[ARITH_RULE `a >= b <=> b <= a`]);
(FIRST_X_ASSUM (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
(ASM_SIMP_TAC[]); ]);;
 

let lemma3 = prove_by_refinement(
 `! (w:real^3) (W:real^3 -> bool). packing W /\ w IN W /\ 
~(set_of_edge w W (ECTC W) = {}) /\ ~(surrounded_node (W,(ECTC W)) w) 
==> ?u. (u IN set_of_edge w W (ECTC W)) /\ (azim_dart (W, (ECTC W)) (w,u) >= pi)`,
[
(PURE_REWRITE_TAC[surrounded_node]);
(PURE_REWRITE_TAC[GSYM EXISTS_NOT_THM]);
(PURE_REWRITE_TAC[TAUT `~(A ==> B) <=> A /\ ~B`]);
(PURE_REWRITE_TAC[ARITH_RULE `~ (a < pi) <=> a >= pi`]);
(PURE_REWRITE_TAC[dart_of_fan]);
(PURE_REWRITE_TAC[SET_RULE `x IN A UNION B <=> x IN A \/ x IN B`]);
(SIMP_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);

(* subgoal 1 *)
(SUBGOAL_THEN `set_of_edge (w:real^3) (W:real^3 ->bool) (ECTC W) = {}` ASSUME_TAC);
(FIRST_X_ASSUM (fun thm -> ALL_TAC));
(FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(ASM_SIMP_TAC[]);
(ASM_MESON_TAC[]);

(* subgoal 2 *)
(EXISTS_TAC `SND (x:real^3 # real^3)`);
(Q_LABEL_TAC `FST (x:real^3 # real^3) = w` "a");
(USE_THEN "a" (fun thm -> SIMP_TAC[PAIR; GSYM thm]));
(ASM_SIMP_TAC[]);
(PURE_REWRITE_TAC[IN_ELIM_THM;set_of_edge]);

(* subgoal 2.1 *)
(SUBGOAL_THEN `w:real^3 = v` (LABEL_TAC "b"));
(REMOVE_THEN "a" (fun thm -> PURE_REWRITE_TAC[GSYM thm]));
(ASM_SIMP_TAC[]);
(ASM_SIMP_TAC[]);
(UNDISCH_TAC `{v:real^3,w':real^3} IN ECTC (W:real^3 -> bool)`);
(REWRITE_TAC[ECTC;IN_ELIM_THM;Geomdetail.PAIR_EQ_EXPAND]);
(STRIP_TAC);

(* subgoal 2.2 *)
(ASM_SIMP_TAC[]);

(* subgoal 2.3 *)
(ASM_SIMP_TAC[]);]);;



let lemma4 = prove_by_refinement(
 `! w:real^3 u v. 
         ~collinear {vec 0, w, u} /\ ~collinear {vec 0, w, v} /\
         azim (vec 0) w u v >= pi
  ==> (w cross u) dot v <= &0`,
[
(REPEAT STRIP_TAC);
(MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] JBDNJJB));
(ASM_SIMP_TAC[]);
STRIP_TAC;
(ABBREV_TAC `(a:real) = ((w:real^3) cross u) dot v`);
(MATCH_MP_TAC (SPECL [`t:real`;`a:real`;`&0`] REAL_LE_LCANCEL_IMP));
(ASM_SIMP_TAC[]);
(Q_LABEL_TAC `sin (azim (vec 0) w u v ) = t * a` "b");
(USE_THEN "b" (fun thm -> (ONCE_REWRITE_TAC[GSYM thm; REAL_MUL_RZERO])));

(* subgoal 1 *)
(SUBGOAL_THEN `azim (vec 0 :real^3) w u v < &2 * pi` ASSUME_TAC);
(SIMP_TAC[SPECL [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`] azim]);

(ABBREV_TAC `b:real = azim (vec 0:real^3) w u v`);
(ONCE_REWRITE_TAC[ARITH_RULE `m <= &0 <=> &0 <= -- m `]);
(ONCE_REWRITE_TAC[GSYM SIN_NEG]);
(ONCE_REWRITE_TAC[GSYM SIN_PERIODIC]);

(* subgoal 2 *)
(SUBGOAL_THEN `-- pi < --b + &2 * pi /\ --b + &2 * pi <= pi` ASSUME_TAC); 
ASM_ARITH_TAC;

(ABBREV_TAC `c:real = --b + &2 * pi`);
(FIRST_ASSUM (ASSUME_TAC o (MATCH_MP SIN_NEGPOS_PI)));
(ONCE_REWRITE_TAC[ARITH_RULE `&0 <= x <=> x = &0 \/ &0 < x`]);
(ONCE_ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (ARITH_RULE ` (&0 <= c /\ c <= pi) ==> ((c = &0 \/ c = pi) \/ &0 <  c /\ c < pi)`));
(ASM_SIMP_TAC[]);
(EXPAND_TAC "c");
(MATCH_MP_TAC (ARITH_RULE `b < a ==> &0 <= --b + a`));
(ASM_SIMP_TAC[]);]);;


let lemma5 = prove_by_refinement(
 `! (V:real^3 -> bool) v. packing V /\ V SUBSET ball_annulus /\ v IN V
  ==> ! u. (u IN set_of_edge v V (ECTC V)) ==> v dot u > &0`,
[
(REPEAT STRIP_TAC);
(* subgoal 1 *)
(SUBGOAL_THEN `!(w:real^3). w IN V ==> w dot w >= &4` (LABEL_TAC "a"));
(REPEAT STRIP_TAC);
(MP_TAC (SET_RULE `(w:real^3) IN V /\ V SUBSET ball_annulus ==> w IN ball_annulus`));
(ASM_SIMP_TAC[]);
(PURE_REWRITE_TAC[ball_annulus]);
(PURE_REWRITE_TAC[DIFF;ball;IN_ELIM_THM]);
(PURE_REWRITE_TAC[REAL_ARITH `~(a < &2) <=> a >= &2`]);
(PURE_REWRITE_TAC[dist; DIST_SYM;VECTOR_SUB_RZERO]);
(PURE_REWRITE_TAC[NORM_GE_SQUARE]);

(SIMP_TAC[ARITH_RULE `~(&2 <= &0) /\ &2 pow 2 = &4`]);
(MATCH_MP_TAC (ARITH_RULE `&2 * a > &0 ==> a > &0`));
(ONCE_REWRITE_TAC[VECTOR_ARITH `&2 * (v dot u) = v dot v + u dot u - (v - u) dot (v - u)`]);

(* subgoal 2 *)
(SUBGOAL_THEN `(v:real^3 - u) dot (v - u) = &4 /\ u IN V` MP_TAC);
(UNDISCH_TAC `u:real^3 IN set_of_edge v V (ECTC V)`);
(SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
STRIP_TAC;
(ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
(ONCE_REWRITE_TAC[GSYM dist]);
(FIRST_ASSUM (MP_TAC o (MATCH_MP (fst (EQ_IMP_RULE Geomdetail.PAIR_EQ_EXPAND)))));
(REPEAT STRIP_TAC);

(* subgoal 2.1 *)
(ASM_SIMP_TAC[]);
ARITH_TAC;
(* subgoal 2.2 *)
(ONCE_REWRITE_TAC[DIST_SYM]);
(ASM_SIMP_TAC[]);
ARITH_TAC;

(STRIP_TAC);
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (ARITH_RULE `a >= &4 /\ b >= &4 ==> a + b - &4 > &0`));
(USE_THEN "a" (fun thm -> MP_TAC( SPEC `v:real^3` thm)));
(USE_THEN "a" (fun thm -> MP_TAC( SPEC `u:real^3` thm)));
(ASM_SIMP_TAC[]);]);;


let lemma6 = prove_by_refinement(
 `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\ 
 orthonormal e1 e2 e3 /\ 
 u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
==> norm u = norm v`,
[
(REPEAT STRIP_TAC);
(* subgoal 1 *)
(SUBGOAL_THEN `orthonormal e1 e2 e3 /\
 u:real^3 = (cos (phi:real) * norm (v:real^3)) % e1 + (sin phi * norm v) % e2 + &0 % e3` ASSUME_TAC);
(ASM_SIMP_TAC[]);
VECTOR_ARITH_TAC;

(FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP (SPECL [`u:real^3`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
` cos (phi:real) * norm (v:real^3)`;`sin (phi:real) * norm (v:real^3)`;`&0`]
norm_lemma2)));
(ONCE_ASM_REWRITE_TAC[]);
(ONCE_REWRITE_TAC[ARITH_RULE `( a * m) pow 2 + (b * m) pow 2 + &0 pow 2 
= (b pow 2 + a pow 2) * m pow 2`]);
(SIMP_TAC[SIN_CIRCLE;REAL_MUL_LID]);
(MATCH_MP_TAC POW_2_SQRT);
(SIMP_TAC[NORM_POS_LE]);]);;


let lemma7 = prove_by_refinement(
 `! v:real^3 u (phi:real) e1 e2 e3. e1 = normalize v /\ 
 orthonormal e1 e2 e3 /\ &0 < phi /\ phi < pi /\ &0 < norm v  /\
 u = (cos phi * norm v) % e1 + (sin phi * norm v) % e2
==> (! w:real^3. &0 < w dot e1  /\ w dot e2 <= &0
     ==> dist (v,w) < dist (u,w))`,
[
(REPEAT STRIP_TAC);
(PURE_REWRITE_TAC[dist;NORM_LT]);
(ONCE_REWRITE_TAC[ARITH_RULE `a < b <=> &0 < b - a `]);
(ONCE_REWRITE_TAC[VECTOR_ARITH `(u - w) dot (u - w) - (v - w) dot (v - w) =
 u dot u - v dot v - &2 * ((u - v) dot w )`]);
(ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);

(* subgoal 1 *)
(SUBGOAL_THEN `norm (u:real^3) = norm (v:real^3)` ASSUME_TAC);
(MATCH_MP_TAC (SPECL [`v:real^3`;`u:real^3`;`phi:real`; `e1:real^3`;
`e2:real^3`;`e3:real^3`] lemma6));
(ASM_SIMP_TAC[]);

(FIRST_ASSUM (fun thm -> SIMP_TAC[thm; ARITH_RULE `a - a - b = --b`]));
(ONCE_REWRITE_TAC[ARITH_RULE `&0 < --(&2 * a) <=> a < &0`]);

(* subgoal 2 *)
(SUBGOAL_THEN `v:real^3 = (norm v) % e1` (LABEL_TAC "v_coordinate"));
(ASM_SIMP_TAC[norm_mul_normalize]);

(Q_LABEL_TAC `orthonormal e1 e2 e3` "base");
(USE_THEN "base" (ASSUME_TAC o MATCH_MP (SPECL [`(u - v):real^3`;`w:real^3`;
`e1:real^3`;`e2:real^3`;`e3:real^3`] dot_coordinates)));
(ONCE_ASM_REWRITE_TAC[]);

(* subgoal 3 *)
(SUBGOAL_THEN `(u:real^3 - v) dot e1 = (cos phi - &1) * norm v /\
(u - v) dot e2 = sin phi * norm v /\ (u - v) dot e3 = &0` MP_TAC);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(MATCH_MP_TAC (SPECL [`u:real^3 - v`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
`(cos phi - &1) * norm v`;`sin phi * norm v`;`&0`] coordinates_lemma));
(USE_THEN "base" (fun thm -> SIMP_TAC[thm]));
(USE_THEN "v_coordinate" (fun thm -> CONV_TAC( PAT_CONV
`\x. U - x = _` (ONCE_REWRITE_CONV[thm]))));
(Q_LABEL_TAC `u:real^3 = (cos phi * norm (v:real^3)) % e1 + (sin phi * norm v) % e2` "u");
(USE_THEN "u" (fun thm -> ONCE_REWRITE_TAC[thm]));
(VECTOR_ARITH_TAC);
(DISCH_THEN (LABEL_TAC "c"));
(USE_THEN "c" (fun thm -> ONCE_REWRITE_TAC[thm]));
(PURE_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_RID]);
(MATCH_MP_TAC (REAL_ARITH `a < &0 /\ b <= &0 ==> a + b < &0`));
CONJ_TAC;

(* subgoal 4 *)
(ONCE_REWRITE_TAC[REAL_ARITH 
`((a - &1) * b) * c < &0 <=> &0 < ((&1 - a) * b) * c`]);
(MATCH_MP_TAC REAL_LT_MUL);
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC REAL_LT_MUL);
(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[REAL_ARITH 
`&0 < &1 - a <=> (a <= &1 /\ ~(a = &1))`]);
(SIMP_TAC[COS_BOUNDS;COS_ONE_2PI]); 
(ONCE_REWRITE_TAC[ TAUT `~(A \/ B) <=> ~A /\ ~B`]);
(STRIP_TAC);

(* subgoal 4.1 *)
(ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
(STRIP_TAC);
(FIRST_X_ASSUM(LABEL_TAC "phi"));


(* subgoal 4.1.1 *)
(SUBGOAL_THEN `0 < n:num` ASSUME_TAC);
(ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
(MATCH_MP_TAC (SPECL [`&0`;`&(n:num)`;`&2 * pi`]
REAL_LT_RCANCEL_IMP));
(SIMP_TAC[ARITH_RULE `&0 * &2 * pi = &0`;
ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
(USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(ASM_SIMP_TAC[PI_POS]);

(* subgoal 4.1.2 *)
(SUBGOAL_THEN `n:num < 1` ASSUME_TAC);
(ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_LT]);
(MATCH_MP_TAC (SPECL [`&(n:num)`;`&1`;`&2 * pi`]
REAL_LT_RCANCEL_IMP));
(SIMP_TAC[ARITH_RULE `&1 * &2 * pi = &2 * pi`;
ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
(USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(SIMP_TAC[PI_POS]);
(MATCH_MP_TAC(ARITH_RULE `a < pi /\ pi < b ==> a < b`));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC(ARITH_RULE `&0 < a ==> a < &2 * a`));
(SIMP_TAC[PI_POS]);
(ASM_MESON_TAC[ARITH_RULE `~(0 < n:num /\ n < 1)`]);

(* subgoal 4.2 *)
(ONCE_REWRITE_TAC[TAUT `~A <=> A ==> F`]);
(STRIP_TAC);
(FIRST_X_ASSUM(LABEL_TAC "phi"));
(* subgoal 4.2.1 *)
(SUBGOAL_THEN `~(&0 < phi:real)` ASSUME_TAC);
(USE_THEN "phi" (fun thm -> ONCE_REWRITE_TAC[thm]));
(ONCE_REWRITE_TAC[ARITH_RULE `~(&0 < -- a) <=> &0 <= a`]);
(MATCH_MP_TAC REAL_LE_MUL);
(SIMP_TAC[REAL_POS]);
(MATCH_MP_TAC (ARITH_RULE `&0 < a ==> &0 <= a`));
(MATCH_MP_TAC REAL_LT_MUL);
(SIMP_TAC[PI_POS]);
ARITH_TAC;
(ASM_MESON_TAC[]);

(* subgoal 5 *)
(ONCE_REWRITE_TAC[ARITH_RULE `a * b <= &0 <=> &0 <= a * (--b)`]);
(MATCH_MP_TAC REAL_LE_MUL);
(ONCE_REWRITE_TAC[ARITH_RULE `&0 <= -- a <=> a <= &0`]);
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC REAL_LE_MUL);
(SIMP_TAC[NORM_POS_LE]);
(MATCH_MP_TAC SIN_POS_PI_LE);
(ASM_ARITH_TAC);]);;


let lemma8 = prove_by_refinement(
`! w:real^3 W:real^3->bool. w IN W 
==> set_of_edge w W (ECTC W) = {v| v IN W /\ dist (w,v) = &2}`,
[
(REPEAT STRIP_TAC);
(MATCH_MP_TAC SUBSET_ANTISYM);
CONJ_TAC;

(* subgoal 1 *)
(PURE_REWRITE_TAC[SUBSET]);
(GEN_TAC);
(SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
(STRIP_TAC);
(SUBGOAL_THEN `dist (w:real^3,x) = dist (v:real^3,w'')` ASSUME_TAC);
(MATCH_MP_TAC Geomdetail.DIST_PAIR_LEMMA);
(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);

(* subgoal 2 *)
(PURE_REWRITE_TAC[SUBSET]);
(GEN_TAC);
(SIMP_TAC[set_of_edge;ECTC;IN_ELIM_THM]);
(STRIP_TAC);
(EXISTS_TAC `w:real^3`);
(EXISTS_TAC `x:real^3`);
(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[DIST_NZ]);
(ASM_ARITH_TAC);]);;


(* main proof *)

let FATUGPD_quasi =  prove_by_refinement( ` UBHDEUU2_hypothesis ==> (!V. packing V /\ V SUBSET ball_annulus 
==> (?W phi.  BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\ 
        (!w. w IN W ==>  (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w))))`,
[
DISCH_TAC;
GEN_TAC;
STRIP_TAC;
(ABBREV_TAC 
   `S = {(U:real^3->bool)| FINITE U /\ packing U /\ 
         (?phi. BIJ phi (V:real^3->bool) U /\ 
                   (! v. v IN V ==> norm v = norm (phi v)))}`);
(ABBREV_TAC 
   `(f:(real^3 ->bool)->num) = 
     (\U. CARD (set_of_iso U))`);

(* subgoal 1 *)
(SUBGOAL_THEN `FINITE (V:real^3->bool)` (LABEL_TAC "finite_v"));
(ASM_SIMP_TAC[lemma1]);

(* subgoal 2 *)
(SUBGOAL_THEN `! (U:real^3 ->bool). U IN S ==> FINITE U` (LABEL_TAC "finite_u"));
(EXPAND_TAC "S");
(SIMP_TAC[IN_ELIM_THM]);

(* subgoal 3 *)
(SUBGOAL_THEN 
 `~ ((S:(real^3->bool)->bool) = {}) /\ 
    (?m. !U. U IN S ==> (f:(real^3->bool)->num) U <= m)` (LABEL_TAC "asm1"));
CONJ_TAC;

(* subgoal 3.1 *)
(PURE_REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]);
(EXISTS_TAC `V:real^3->bool`);
(EXPAND_TAC "S");
(ASM_SIMP_TAC[IN_ELIM_THM]);
(EXISTS_TAC `(I:real^3->real^3)`);
CONJ_TAC;

(* subgoal 3.1.1 *)
(SIMP_TAC[BIJ;INJ;SURJ;I_THM]);
(SET_TAC[]);

(* subgoal 3.1.2 *)
(SIMP_TAC[I_THM]);

(* subgoal 3.2 *)
(EXISTS_TAC `CARD (V:real^3->bool)`);
(GEN_TAC);

(* subgoal 3.2.1 *)
(SUBGOAL_THEN `! (U:real^3->bool). U IN S ==> CARD U = CARD (V:real^3->bool)` MP_TAC);
(GEN_TAC);
(EXPAND_TAC "S");
(PURE_REWRITE_TAC[IN_ELIM_THM]);
STRIP_TAC;
(MATCH_MP_TAC BIJ_CARD_EQ);
(EXISTS_TAC `phi:real^3->real^3`);
(ASM_SIMP_TAC[]);

(DISCH_THEN (MP_TAC o (fun thm -> (SPEC `U:real^3 ->bool` thm))));
(MATCH_MP_TAC (TAUT ` (p ==> (q ==> r)) ==> ((p ==> q) ==> (p ==> r))`));
(REPEAT STRIP_TAC);

(* subgoal 3.2.2 *)
(SUBGOAL_THEN  `(f:(real^3->bool) -> num) U <= CARD U` ASSUME_TAC);
(EXPAND_TAC "f");
(MATCH_MP_TAC CARD_SUBSET);
CONJ_TAC;

(* subgoal 3.2.2.1 *)
(SET_TAC[set_of_iso]);

(* subgoal 3.2.2.2 *)
(UNDISCH_TAC `(U:real^3->bool) IN (S:(real^3->bool)->bool)`);  
(ASM_SIMP_TAC[]);

ASM_ARITH_TAC;

(REMOVE_THEN "asm1" (ASSUME_TAC o (MATCH_MP bdd_num_func_attain_max)));
(FIRST_X_ASSUM CHOOSE_TAC);
(EXISTS_TAC `U:real^3->bool`);

(FIRST_X_ASSUM MP_TAC);
(STRIP_TAC);
(UNDISCH_TAC `U:real^3 -> bool IN S`);
(EXPAND_TAC "S");
(SIMP_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `phi:real^3 ->real^3`);
(ASM_SIMP_TAC[]);
(REPEAT STRIP_TAC);

(* subgoal 4 *)
(SUBGOAL_THEN `! v:real^3. v IN U ==> norm v <= &2 * h0 /\ ~(norm v < &2)`
(LABEL_TAC "norm_bdd"));
GEN_TAC;
(UNDISCH_TAC `BIJ phi (V:real^3->bool) (U:real^3->bool)`);
(PURE_REWRITE_TAC[BIJ;SURJ]);
( STRIP_TAC);
(STRIP_TAC);
(FIRST_ASSUM (fun thm -> MP_TAC (SPEC `v:real^3` thm)));
(FIRST_ASSUM (fun thm -> SIMP_TAC[thm]));
STRIP_TAC;
(UNDISCH_TAC `! v:real^3. v IN V ==> norm v = norm ((phi:real^3 -> real^3) v)`);
(DISCH_THEN (fun thm -> MP_TAC (SPEC `y:real^3` thm)));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (ARITH_RULE 
`a <= &2 * h0 /\ ~(a < &2) ==> a = b ==> b <= &2 * h0 /\ ~(b < &2)`));

(* subgoal 4.1 *)
(SUBGOAL_THEN `y:real^3 IN ball_annulus` MP_TAC);
(MATCH_MP_TAC (SET_RULE `y:real^3 IN V /\ V SUBSET ball_annulus ==> y IN ball_annulus`));
(ASM_SIMP_TAC[]);

(PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
(SIMP_TAC[DIST_0]);

(* subgoal 5 *)
(SUBGOAL_THEN `(U:real^3 -> bool) SUBSET ball_annulus` (LABEL_TAC "u_annu"));
(PURE_REWRITE_TAC[SUBSET]);
GEN_TAC;
STRIP_TAC;
(PURE_REWRITE_TAC[IN_ELIM_THM;ball_annulus;DIFF;cball;ball]);
(SIMP_TAC[DIST_0]);
(ASM_SIMP_TAC[]);
 
(* subgoal 6 *)
(SUBGOAL_THEN `! v:real^3. v IN U ==> ~(v = vec 0)` (LABEL_TAC "not_0"));
(GEN_TAC);
STRIP_TAC;
(ONCE_REWRITE_TAC[GSYM NORM_POS_LT]);
(MATCH_MP_TAC (ARITH_RULE `~(norm (v:real^3) < &2) ==> &0 < norm v`));
(ASM_SIMP_TAC[]);

(* subgoal 7 *)
(SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U) 
  ==> ~(collinear {vec 0, w, v})` (LABEL_TAC "not_li"));
(GEN_TAC);
(MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
(ASM_SIMP_TAC[]);
(SIMP_TAC[IN_ELIM_THM;ECTC]);
(MATCH_MP_TAC (TAUT `(B ==> C) ==> (A ==> B ==> C)`));
STRIP_TAC;
(ONCE_REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);
(ONCE_REWRITE_TAC[TAUT `~(A \/ B \/ C) <=> ~A /\ ~B /\ ~C`]);
(ONCE_REWRITE_TAC[between]);
(ONCE_REWRITE_TAC[DIST_0]);
(CONV_TAC (PAT_CONV `\x. A /\ ~( _ = x + _ ) /\ ~( _ = _ + x)`
(ONCE_REWRITE_CONV[DIST_SYM])));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (ARITH_RULE 
`(a <= &2 * #1.26) /\ ~(a < &2) /\ (b <= &2 * #1.26) /\ ~(b < &2)
==> ~(&2 = a + b) /\ ~(b = &2 + a) /\ ~(a = b + &2)`));
(ONCE_REWRITE_TAC[GSYM h0]);
(ASM_SIMP_TAC[]);

(ASM_CASES_TAC `~(set_of_edge (w:real^3) (U:real^3->bool) (ECTC U) = {}) /\
  ~(surrounded_node (U,ECTC U) w)`);

(ABBREV_TAC `result:bool = (set_of_edge w U (ECTC U) = {} \/ surrounded_node (U,ECTC U) w)`);
(MP_TAC (SPECL [`U:real^3 -> bool`;`w:real^3`] lemma2));
(ASM_SIMP_TAC[]);
(STRIP_TAC);
(MP_TAC (SPECL[`w:real^3`;`U:real^3->bool`] lemma3));
(ASM_SIMP_TAC[]);
(STRIP_TAC);
(Q_ABBREV_TAC `e1:real^3 = normalize w` "e1");
(Q_ABBREV_TAC `y:real^3 = w cross u` "y_axis");
(Q_ABBREV_TAC `e2:real^3 = normalize y` "e2");
(Q_ABBREV_TAC `e3:real^3 = e1 cross e2` "e3");

(* subgoal 8 *)
(SUBGOAL_THEN `orthonormal (e1:real^3) e2 e3` ASSUME_TAC);
(PURE_REWRITE_TAC[orthonormal]);
(ONCE_REWRITE_TAC[GSYM NORM_EQ_1]);
(* subgoal 8.1 *)
(SUBGOAL_THEN `norm (e1:real^3) = &1` ASSUME_TAC);
(Q_EXPAND_TAC "e1");
(MATCH_MP_TAC norm_normalize);
(ASM_SIMP_TAC[]);

(* subgoal 8.2 *)
(SUBGOAL_THEN `norm (e2:real^3) = &1` ASSUME_TAC);
(Q_EXPAND_TAC "e2");
(MATCH_MP_TAC norm_normalize);
(Q_EXPAND_TAC "y_axis");
(ONCE_REWRITE_TAC[CROSS_EQ_0]);
(ASM_SIMP_TAC[]);

(* subgoal 8.3 *)
(SUBGOAL_THEN `(e1:real^3) dot e2 = &0` ASSUME_TAC);
(Q_EXPAND_TAC "e1");
(ONCE_REWRITE_TAC[GSYM dot_eq_0]);
(Q_EXPAND_TAC "e2");
(ONCE_REWRITE_TAC[DOT_SYM]);
(ONCE_REWRITE_TAC[GSYM dot_eq_0]);
(Q_EXPAND_TAC "y_axis");
(SIMP_TAC[DOT_CROSS_SELF]);

(* subgoal 8.4 *)
(SUBGOAL_THEN `(e1:real^3) dot e3 = &0 /\ e2 dot e3 = &0` ASSUME_TAC);
(Q_EXPAND_TAC "e3");
(SIMP_TAC[DOT_CROSS_SELF]);

(* subgoal 8.5 *)
(SUBGOAL_THEN `norm (e3:real^3) = &1` ASSUME_TAC);
(Q_EXPAND_TAC "e3");
(MP_TAC(ISPECL [`e1:real^3`;`e2:real^3`] NORM_CROSS_DOT));
(ASM_SIMP_TAC[REAL_POW_2;REAL_MUL_RZERO;REAL_ADD_RID;REAL_MUL_RID]);
(ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
(STRIP_TAC);
(MP_TAC(SPECL [`norm (e3:real^3)`;`2`] REAL_POW_EQ_1_IMP));
(ASM_SIMP_TAC[ARITH_RULE `~(2 = 0)`]);
(STRIP_TAC);
(MATCH_MP_TAC (ARITH_RULE `abs x = &1 /\ &0 <= x  ==> x = &1`));
(ASM_SIMP_TAC[NORM_POS_LE]);

(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[DOT_SQUARE_NORM]);
(ASM_SIMP_TAC[REAL_POW_2]);
ARITH_TAC;

(* subgoal 9 *)
(SUBGOAL_THEN `!v:real^3. v IN set_of_edge w U (ECTC U)
  ==> v dot e2 <= &0` ASSUME_TAC);
(GEN_TAC);
(STRIP_TAC);
(ONCE_REWRITE_TAC[DOT_SYM]);
(ONCE_REWRITE_TAC[ARITH_RULE `a <= &0 <=> &0 < --a \/ a = &0`]);
(ONCE_REWRITE_TAC[VECTOR_ARITH `--((e2:real^3) dot v) = (--v) dot e2`]);
(Q_EXPAND_TAC "e2");
(ONCE_REWRITE_TAC[GSYM dot_gt_0]);
(ONCE_REWRITE_TAC[GSYM dot_eq_0]);
(ONCE_REWRITE_TAC[VECTOR_ARITH ` --(v:real^3) dot y = -- (y dot v)`]);
(ONCE_REWRITE_TAC[ARITH_RULE ` (&0 < --a \/ a = &0 )<=> a <= &0`]);
(Q_EXPAND_TAC "y_axis");
(ASM_CASES_TAC `v:real^3 = u`);

(* subgoal 9.1 *)
(FIRST_ASSUM(fun thm -> SIMP_TAC[thm;DOT_CROSS_SELF]));
 ARITH_TAC;

(* subgoal 9.2 *)
(MP_TAC (SPECL [`w:real^3`;`u:real^3`;`v:real^3`] lemma4));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `A ==> (A ==>B) ==> B`));
(MP_TAC (SPEC `U:real^3 -> bool` UBHDEUU2_quasi));
(ASM_SIMP_TAC[]);
(DISCH_TAC);
(MP_TAC (SPECL [`U:real^3->bool`;`(ECTC U):(real^3->bool)->bool`;`w:real^3`;
`u:real^3`;`v:real^3`] azim_ge_azim_dart));
(ASM_SIMP_TAC[]);

(* subgoal 9.2.1 *)
(SUBGOAL_THEN `~(w:real^3 = u)` ASSUME_TAC);
(UNDISCH_TAC `u:real^3 IN set_of_edge w U (ECTC U)`);
(MP_TAC(SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
(ASM_SIMP_TAC[IN_ELIM_THM]);
(STRIP_TAC);
(STRIP_TAC);
(ONCE_REWRITE_TAC[GSYM DIST_EQ_0]);
(ASM_ARITH_TAC);

(ASM_SIMP_TAC[]);
(ASM_ARITH_TAC);

(* subgoal 10 *)
(SUBGOAL_THEN `?(a:real). &0 < a /\ a < pi /\
 (&2 - &2 * cos a ) * ( norm (w:real^3) pow 2) < epsilon pow 2` ASSUME_TAC);
(MP_TAC (SPEC `&0` REAL_CONTINUOUS_AT_COS));
(ONCE_REWRITE_TAC[real_continuous_atreal]);
(DISCH_THEN (MP_TAC o (SPEC 
`epsilon pow 2 / (&2 * norm(w:real^3) pow 2)`)));

(* subgoal 10.1 *)
(SUBGOAL_THEN 
`&0 < epsilon pow 2/ (&2 * norm (w:real^3) pow 2)` ASSUME_TAC);
(MATCH_MP_TAC REAL_LT_DIV);
(CONJ_TAC);

(* subgoal 10.1.1 *)
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);

(* subgoal 10.1.2 *)
(MATCH_MP_TAC (ARITH_RULE ` &0 < a ==> &0 < &2 * a`));
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[NORM_POS_LT]);

(ASM_SIMP_TAC[COS_0;REAL_MUL_RID;REAL_SUB_RZERO]);
(DISCH_THEN CHOOSE_TAC); 
(FIRST_X_ASSUM MP_TAC);
STRIP_TAC;
(Q_ABBREV_TAC `m:real = min (d / &2) (pi / &2)` "phi");
(EXISTS_TAC `m:real`);
 (* subgoal 10.2 *)
(SUBGOAL_THEN `&0 < m:real` ASSUME_TAC);
(Q_EXPAND_TAC "phi");
(SIMP_TAC[REAL_LT_MIN;PI2_BOUNDS]);
(MATCH_MP_TAC REAL_LT_DIV);
(ASM_ARITH_TAC);

(* subgoal 10.3 *)
(SUBGOAL_THEN `m < pi` ASSUME_TAC);
(Q_EXPAND_TAC "phi");
(ONCE_REWRITE_TAC[REAL_MIN_LT]);
(DISJ2_TAC);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> a / &2 < a`));
(SIMP_TAC[PI_POS]);

(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC [REAL_ARITH `(&2 - &2 * a) * b = (&1 - a) * (&2 * b)`]);
(MP_TAC (SPECL [`&1 - cos (m:real)`;`epsilon:real pow 2`;
`&2 * norm (w:real^3) pow 2`] REAL_LT_RDIV_EQ));

(* subgoal 10.4 *)
(SUBGOAL_THEN `&0 < &2 * norm (w:real^3) pow 2` ASSUME_TAC);
(ONCE_REWRITE_TAC[ARITH_RULE `&0 < &2 * a <=> &0 < a`]);
(MATCH_MP_TAC REAL_POW_LT);
(ASM_SIMP_TAC[NORM_POS_LT]);

(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `A ==> (A <=> B ) ==> B`));
(MATCH_MP_TAC (REAL_ARITH `abs a < b ==> a < b`));
(ONCE_REWRITE_TAC[REAL_ARITH `abs (a - b) = abs (b - a)`]);
(FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));

(* subgoal 10.5 *)
(SUBGOAL_THEN `abs (m:real) = m` ASSUME_TAC);
(ONCE_REWRITE_TAC[REAL_ABS_REFL]);
(ASM_ARITH_TAC);
(ASM_SIMP_TAC[]);
(Q_EXPAND_TAC "phi");
(ONCE_REWRITE_TAC[REAL_MIN_LT]);
(DISJ1_TAC);
 ASM_ARITH_TAC;

(FIRST_X_ASSUM CHOOSE_TAC);
(Q_ABBREV_TAC `s:real^3 = 
  (cos a * norm (w:real^3)) % e1 + (sin a * norm w) % e2` "subs_point");
(Q_ABBREV_TAC `U':real^3 -> bool = s INSERT (U DELETE w)` "new_set");

(* subgoal 11 *)
(SUBGOAL_THEN `!(v:real^3). v IN U /\ ~(v = w) ==> &2 < dist (s,v)` 
(LABEL_TAC "dist_gt_2"));
(GEN_TAC);
(STRIP_TAC);
(ASM_CASES_TAC  `(v:real^3) IN set_of_edge w U (ECTC U)`);

(* subgoal 11.1 *)
(SUBGOAL_THEN `dist ((w:real^3),v) = &2` ASSUME_TAC);
(FIRST_X_ASSUM MP_TAC);
(MP_TAC (SPECL [`w:real^3`;`U:real^3->bool`] lemma8));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
(SIMP_TAC[IN_ELIM_THM]);

(FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
`e1:real^3`;`e2:real^3`;`e3:real^3`] lemma7));
(ASM_SIMP_TAC[NORM_POS_LT]);
(DISCH_THEN (fun thm -> MATCH_MP_TAC (SPEC `v:real^3` thm)));
(ASM_SIMP_TAC[]);
(Q_EXPAND_TAC "e1");
(ONCE_REWRITE_TAC[GSYM dot_gt_0]);
(ONCE_REWRITE_TAC[ARITH_RULE `&0 < a <=> a > &0`]);
(ONCE_REWRITE_TAC[DOT_SYM]);
(MP_TAC (SPECL [`U:real^3->bool`;`w:real^3`] lemma5));
(ASM_SIMP_TAC[]);

(* subgoal 11.2 *)
(ONCE_REWRITE_TAC[DIST_SYM]);
(MATCH_MP_TAC (REAL_ARITH `&2 < dist (v:real^3,w) - dist (s,w) /\ 
dist (v,w) - dist (s,w) <= a ==> &2 < a`));
(SIMP_TAC[Pack1.real_sub_norm]);
(MATCH_MP_TAC (REAL_ARITH 
`a > &2 + (epsilon:real) /\ b < epsilon ==>  &2 < a - b`));
(ONCE_REWRITE_TAC[DIST_SYM]);
(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(PURE_REWRITE_TAC[dist]);
(ONCE_REWRITE_TAC[NORM_LT_SQUARE]);
(ASM_SIMP_TAC[ARITH_RULE `&0 < a <=> a > &0`]);

(* subgoal 11.2.1 *)
(SUBGOAL_THEN `s:real^3 - w = ((cos (a:real) - &1) * norm (w:real^3)) % e1 +
(sin a * norm w) % e2 + &0 % e3` ASSUME_TAC);
(* subgoal 11.2.1.1 *)
(SUBGOAL_THEN `w:real^3 = norm w % e1` ASSUME_TAC);
(Q_EXPAND_TAC "e1");
(SIMP_TAC[norm_mul_normalize]);

(FIRST_X_ASSUM(fun thm -> CONV_TAC(PAT_CONV `\x. s - x = A`
(ONCE_REWRITE_CONV[thm]))));
(Q_EXPAND_TAC "subs_point");
(SIMP_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_RID]);
(ONCE_REWRITE_TAC[VECTOR_ARITH 
`(a % (e1:real^3) + b % e2) - c % e1 = (a - c) % e1 + b % e2`]);
(SIMP_TAC[ARITH_RULE `a * b - b = (a - &1) * b`]);
(MP_TAC (SPECL 
[`s:real^3 - w`;`s:real^3 - w`;`e1:real^3`;`e2:real^3`;`e3:real^3`;
`(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
`(cos a - &1) * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`] 
dot_coordinates_2));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `B ==> A ==> B`));
(ONCE_REWRITE_TAC [REAL_ARITH 
`(a * b) * a * b + (c * b) * c * b + &0 * &0 = (a * a + c * c) * b pow 2`]);
(ONCE_REWRITE_TAC [REAL_ARITH 
`(a - &1) * (a - &1) + b * b = &1 - &2 * a + b pow 2 + a pow 2`]);
(SIMP_TAC[SIN_CIRCLE]);
(ASM_SIMP_TAC[REAL_ARITH `&1 - b + &1 = &2 - b`]);

(* subgoal 12 *)
(SUBGOAL_THEN `!(v:real^3). v IN U' /\ ~(v = s) ==> &2 < dist (s,v)` 
(LABEL_TAC "iso"));
(GEN_TAC);
(Q_EXPAND_TAC "new_set");
(SIMP_TAC[IN_INSERT; TAUT ` ((A \/ B) /\ ~A) <=> (~A /\ B)`]);
(SIMP_TAC[IN_DELETE]);
(ASM_SIMP_TAC[]);

(* subgoal 13 *)
(SUBGOAL_THEN `~(s:real^3 IN U)` ASSUME_TAC);
(ONCE_REWRITE_TAC[SET_RULE `~(x IN S) <=> (!y. y IN S ==> ~(x = y))`]);
GEN_TAC;
STRIP_TAC;
(ASM_CASES_TAC `y':real^3 = w`);

(* subgoal 13.1 *)
(ASM_SIMP_TAC[]);
(* subgoal 13.1.1 *)
(SUBGOAL_THEN `w:real^3 = norm w % e1 + &0 % e2 + &0 % e3` ASSUME_TAC);
(SIMP_TAC[ VECTOR_ARITH `a % e1 + &0 % e2 + &0 % e3 = a % e1`]);
(Q_EXPAND_TAC "e1");
(SIMP_TAC[norm_mul_normalize]);

(FIRST_X_ASSUM (fun thm -> ONCE_REWRITE_TAC[thm]));
(USE_THEN "subs_point" (fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(CONV_TAC(PAT_CONV `\x. ~(x = A)` (ONCE_REWRITE_CONV[
VECTOR_ARITH `a % e1 + b % e2 = a % e1 + b % e2 + &0 % e3`])));
(MP_TAC ( SPECL [`e1:real^3`;`e2:real^3`;`e3:real^3`;
`cos a * norm (w:real^3)`;`sin a * norm (w:real^3)`;`&0`;
`norm (w:real^3)`;`&0`;`&0`] ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT ));
(MATCH_MP_TAC(TAUT `(A /\ ~C) ==> ((A ==> ( B <=> C)) ==> ~B) `));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `~B ==> ~ (A /\ B)`));
(SIMP_TAC[REAL_ENTIRE]);
(SIMP_TAC[TAUT `~(A \/ B) <=> ~A /\ ~B`]);
CONJ_TAC;

(* subgoal 13.1.2 *)
(ASM_SIMP_TAC[PI_WORKS]);
(* subgoal 13.1.3 *)
(MATCH_MP_TAC(ARITH_RULE `&0 < x ==> ~(x = &0)`));
(ASM_SIMP_TAC[NORM_POS_LT]);

(* subgoal 13.2 *)
(ONCE_REWRITE_TAC[DIST_NZ]);
(MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &0 < a`));
(USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
(ASM_SIMP_TAC[]);


(* subgoal 14 *)
(SUBGOAL_THEN `U':real^3 -> bool IN S` ASSUME_TAC);
(EXPAND_TAC "S");
(SIMP_TAC[IN_ELIM_THM]);

(* subgoal 14.1 *)
(SUBGOAL_THEN `norm (s:real^3) = norm (w:real^3)` ASSUME_TAC);
(MP_TAC (SPECL [`w:real^3`;`s:real^3`;`a:real`;
`e1:real^3`;`e2:real^3`;`e3:real^3`] lemma6));
(ASM_SIMP_TAC[]);

(* subgoal 14.2 *)
(SUBGOAL_THEN `FINITE (U':real^3->bool)` ASSUME_TAC);
(Q_EXPAND_TAC "new_set");
(ONCE_REWRITE_TAC[FINITE_INSERT]);
(ASM_SIMP_TAC[FINITE_DELETE]);

(* subgoal 14.3 *)
(SUBGOAL_THEN `packing (U':real^3 -> bool)` ASSUME_TAC);
(PURE_REWRITE_TAC[packing]);
(REPEAT GEN_TAC);
(CONV_TAC(PAT_CONV `\x. x /\ x /\ A ==> B`
(ONCE_REWRITE_CONV[GSYM IN])));
(STRIP_TAC);
(ASM_CASES_TAC `u':real^3 = s`);

(* subgoal 14.3.1 *)
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
(FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
(ASM_SIMP_TAC[]);
(FIRST_X_ASSUM(fun thm-> ONCE_REWRITE_TAC[GSYM thm]));
(ASM_SIMP_TAC[EQ_SYM_EQ]);

(ASM_CASES_TAC `v:real^3 = s`);

(* subgoal 14.3.2.1 *)
(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(MATCH_MP_TAC (ARITH_RULE `&2 < a ==> &2 <= a`));
(FIRST_ASSUM (fun thm -> MATCH_MP_TAC thm));
(ASM_SIMP_TAC[]);

(* subgoal 14.3.2.2 *) 
(UNDISCH_TAC `u':real^3 IN U'`);
(Q_EXPAND_TAC "new_set");
(ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
(STRIP_TAC);
(UNDISCH_TAC `v:real^3 IN U'`);
(Q_EXPAND_TAC "new_set");
(ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
(STRIP_TAC);
(UNDISCH_TAC `packing (U:real^3->bool)`);
(PURE_REWRITE_TAC[packing]);
(DISCH_THEN (fun thm -> MATCH_MP_TAC (SPECL [`u':real^3`;`v:real^3`] thm)));
(CONV_TAC(PAT_CONV `\x. x /\ x /\ A` (ONCE_REWRITE_CONV[GSYM IN])));
(ASM_SIMP_TAC[]);

(ASM_SIMP_TAC[]);
(Q_ABBREV_TAC `(h:real^3->real^3) = (\v. if  v = w then s else v)` "h");
(EXISTS_TAC `(h:real^3->real^3) o (phi:real^3->real^3)`);
(CONJ_TAC);

(* subgoal 14.4 *)
(MATCH_MP_TAC Hypermap.COMPOSE_BIJ);
(EXISTS_TAC `U:real^3->bool`);
(ASM_SIMP_TAC[]);
(* subgoal 14.4.1 *)
(SUBGOAL_THEN `!v:real^3. v IN U ==> (h:real^3->real^3) v IN U'` ASSUME_TAC);
(REPEAT STRIP_TAC);
(Q_EXPAND_TAC "h");
(SIMP_TAC[BETA_THM]);
(COND_CASES_TAC);
(* subgoal 14.4.1.1 *)
(Q_EXPAND_TAC "new_set");
(SET_TAC[]);
(* subgoal 14.5.1.2 *)
(Q_EXPAND_TAC "new_set");
(SIMP_TAC[IN_INSERT]);
(DISJ2_TAC);
(ASM_SIMP_TAC[IN_DELETE]);

(ASM_SIMP_TAC[BIJ;INJ;SURJ]);
(CONJ_TAC);

(* subgoal 14.5.2 *)
(REPEAT STRIP_TAC);
(UNDISCH_TAC `(h:real^3->real^3) x = h y'`);
(Q_EXPAND_TAC "h");
(SIMP_TAC[BETA_THM]);
(COND_CASES_TAC);

(* subgoal 14.5.2.1 *)
(COND_CASES_TAC);
(* subgoal 14.5.2.1.1 *)
(ASM_SIMP_TAC[]);
(* subgoal 14.5.2.1.2 *)
(ASM_MESON_TAC[]);

(* subgoal 14.5.2.2 *)
(COND_CASES_TAC);

(* subgoal 14.5.2.2.1 *)
(ASM_MESON_TAC[]);

(* subgoal 14.5.2.2.2 *)
(SIMP_TAC []);

(* subgoal 14.5.3 *)
(REPEAT STRIP_TAC);
(ASM_CASES_TAC `x:real^3 = s`);

(* subgoal 14.5.3.1 *)
(EXISTS_TAC `w:real^3`);
(ASM_SIMP_TAC[]);
(Q_EXPAND_TAC "h");
(SIMP_TAC[BETA_THM]);

(* subgoal 14.5.3.2 *)
(EXISTS_TAC `x:real^3`);
(UNDISCH_TAC `x:real^3 IN U'`);
(Q_EXPAND_TAC "new_set");
(ASM_SIMP_TAC[IN_INSERT;IN_DELETE]);
(STRIP_TAC);
(Q_EXPAND_TAC "h");
(ASM_SIMP_TAC[BETA_THM]);

(REPEAT STRIP_TAC);
(SIMP_TAC[o_THM]);

(* subgoal 14.6 *)
(SUBGOAL_THEN `! x:real^3. x IN U ==> norm x = norm ((h:real^3->real^3) x)` MATCH_MP_TAC);
(REPEAT STRIP_TAC);
(Q_EXPAND_TAC "h");
(SIMP_TAC[BETA_THM]);
(COND_CASES_TAC);
(* subgoal 14.6.1 *)
(ASM_SIMP_TAC[]);

(* subgoal 14.6.2 *)
(SIMP_TAC[]);

(UNDISCH_TAC `BIJ (phi:real^3->real^3) V U`);
(SIMP_TAC[BIJ]);
(DISCH_THEN (fun thm -> MP_TAC (CONJUNCT1 thm)));
(SIMP_TAC[INJ]);
(DISCH_THEN (fun thm -> MATCH_MP_TAC (CONJUNCT1 thm)));
(ASM_SIMP_TAC[]);

(* subgoal 15 *)
(SUBGOAL_THEN `~((f:(real^3->bool)->num) U' <= f U)` ASSUME_TAC);
(ONCE_REWRITE_TAC[ ARITH_RULE `~((a:num) <= b) <=> (b < a)`]);
(EXPAND_TAC "f");
(MATCH_MP_TAC CARD_PSUBSET);
(CONJ_TAC);

(* subgoal 15.1 *)
(ONCE_REWRITE_TAC[PSUBSET_ALT]);
(CONJ_TAC);

(* subgoal 15.1.1 *)
(ONCE_REWRITE_TAC[SUBSET]);
GEN_TAC;
(ONCE_REWRITE_TAC[set_of_iso]);
(SIMP_TAC[IN_ELIM_THM]);
(STRIP_TAC);

(* subgoal 15.1.1.1 *)
(SUBGOAL_THEN `x:real^3 IN U'` ASSUME_TAC);
(Q_EXPAND_TAC "new_set");
(SIMP_TAC[IN_INSERT]);
DISJ2_TAC;
(SIMP_TAC[IN_DELETE]);
(ASM_SIMP_TAC[]);
(ASM_MESON_TAC[]);

(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[GSYM SUBSET_EMPTY]);
(UNDISCH_TAC `set_of_edge x U (ECTC U) = {}`);
(DISCH_THEN(fun thm -> ONCE_REWRITE_TAC[GSYM thm]));
(MP_TAC (SPECL [`x:real^3`;`U:real^3->bool`] lemma8));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
(MP_TAC (SPECL [`x:real^3`;`U':real^3->bool`] lemma8));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT `B ==> (A ==> B)`));
(SIMP_TAC[SUBSET;IN_ELIM_THM]);
GEN_TAC;
(Q_EXPAND_TAC "new_set");
(SIMP_TAC[IN_INSERT;IN_DELETE]);
(MATCH_MP_TAC (TAUT `(D ==> ~A) ==> (A \/ B /\ C) /\ D ==> B`));
(MATCH_MP_TAC (TAUT `(B ==> ~A) ==> (A ==> ~B)`));
STRIP_TAC;
(ASM_SIMP_TAC[]);
(ONCE_REWRITE_TAC[DIST_SYM]);
(MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~(a = &2)`));
(USE_THEN "dist_gt_2" (fun thm -> MATCH_MP_TAC thm));
(ASM_SIMP_TAC[]);
(ASM_SET_TAC[]);

(* subgoal 15.2 *)
(EXISTS_TAC `s:real^3`);
(CONJ_TAC);
(* subgoal 15.2.1 *)
(SIMP_TAC[set_of_iso;IN_ELIM_THM]);
(* subgoal 15.2.1.1 *)
(SUBGOAL_THEN `s:real^3 IN U'` ASSUME_TAC);
(Q_EXPAND_TAC "new_set");
(SET_TAC[]);

(ASM_SIMP_TAC[]);
(MP_TAC (SPECL [`s:real^3`;`U':real^3->bool`] lemma8));
(ASM_SIMP_TAC[]);
(MATCH_MP_TAC (TAUT ` B ==> A ==> B`));
(ONCE_REWRITE_TAC[SET_RULE `{x| P x} = {} <=> !x. ~(P x)`]); 
(GEN_TAC);
(MATCH_MP_TAC (TAUT ` (A ==> ~B) ==> ~(A /\ B)`));
(STRIP_TAC);
(ASM_CASES_TAC `v:real^3 = s`);

(* subgoal 15.2.1.2 *)
(ASM_SIMP_TAC[DIST_REFL]);
ARITH_TAC;
(* subgoal 15.2.1.3 *)
(MATCH_MP_TAC (ARITH_RULE `&2 < a ==> ~ (a = &2)`));
(USE_THEN "iso" (fun thm -> MATCH_MP_TAC thm));
(ASM_SIMP_TAC[]);

(* subgoal 15.2.2 *)
(ASM_SIMP_TAC[set_of_iso;IN_ELIM_THM]);
(MATCH_MP_TAC ( ISPECL [`set_of_iso (U':real^3->bool)`;
`U':real^3->bool`] FINITE_SUBSET));
(ASM_SIMP_TAC[set_of_iso]);
(SET_TAC[]);

(ASM_MESON_TAC[]);
(ASM_MESON_TAC[]);
]);;

end;;