(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma:  EMNWUUS                                                 *)
(*      Chaper    : Packing (Marchal Cells)                                  *)
(*      Date      : October 3, 2010                                          *)
(*                                                                           *)
(* ========================================================================= *)
(*
#use "/usr/programs/hollight/hollight-svn75/hol.ml";; 
loads "Multivariate/flyspeck.ml";;
#use "/home/ky/flyspeck/working/boot.hl";; 
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "trigonometry/trig2.hl";;
flyspeck_needs "trigonometry/trigonometry.hl";;

(* =================  Loaded files   ======================================== *)

flyspeck_needs "leg/collect_geom.hl";;
flyspeck_needs "fan/fan_defs.hl";;
flyspeck_needs "fan/introduction.hl";; 
flyspeck_needs "fan/topology.hl";;
flyspeck_needs "fan/fan_misc.hl";; 
flyspeck_needs "fan/HypermapAndFan.hl";; 
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "packing/pack_concl.hl";; 
flyspeck_needs "packing/pack1.hl";;
flyspeck_needs "packing/pack2.hl";;
flyspeck_needs "packing/pack3.hl";;
flyspeck_needs "packing/Rogers.hl";; 
flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
*)
(* ====================== Open appropriate files ============================ *)
flyspeck_needs "packing/marchal_cells.hl";;

module Emnwuus = struct

open Rogers;;
open Prove_by_refinement;;
open Vukhacky_tactics;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Sphere;; 
open Marchal_cells;;

let seans_fn () =
let (tms,tm) = top_goal () in
let vss = map frees (tm::tms) in
let vs = setify (flat vss) in
map dest_var vs;;

(* ======================= Begin working ==================================== *) 
(* ========================================================================= *)

let EMNWUUS1 = prove_by_refinement ( EMNWUUS1_concl,
[ (REWRITE_TAC[mcell4] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN COND_CASES_TAC);   
 (REPEAT STRIP_TAC);
 (NEW_GOAL `set_of_list (ul:(real^3)list) = {}`);
 (ASM_MESON_TAC[CONVEX_HULL_EQ_EMPTY]);
 (NEW_GOAL `ul:(real^3)list = []`);
 (NEW_GOAL `~(?h t. ul:(real^3)list = CONS h t)`);
 STRIP_TAC;
 (NEW_GOAL `(h:real^3) IN set_of_list ul`);
 (REWRITE_TAC [ASSUME `ul = CONS (h:real^3) t`; IN_SET_OF_LIST;MEM]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[list_CASES]);
 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
 (REWRITE_TAC[BARV]);
 STRIP_TAC;
 (NEW_GOAL `LENGTH (ul:(real^3)list) = 0`);
 (ASM_MESON_TAC[ASSUME `ul:(real^3)list =[]`;LENGTH]);
 (ASM_ARITH_TAC);
 (MESON_TAC[]);
 (MESON_TAC[]);
 (MESON_TAC[]) ]);;

(* ========================================================================= *)

let EMNWUUS2 = prove_by_refinement (EMNWUUS2_concl,
[ (REPEAT GEN_TAC THEN STRIP_TAC); 
(EQ_TAC); 

(REPEAT STRIP_TAC); 
(* Break into 4 cases *)

(* =============== Case 1 ================================ *) 

(REWRITE_TAC[mcell0]); 
(REWRITE_TAC[SET_RULE `x DIFF y = {} <=> (!a. a IN x ==> a IN y)`]); 
(REWRITE_TAC[ROGERS;IMAGE;IN;ball;SUBSET;IN_ELIM_THM]); 
 GEN_TAC; 
(MATCH_MP_TAC BALL_CONVEX_HULL_LEMMA); 

(GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]); 
(STRIP_TAC); 

 (* New_subgoal 1.1 *)
(NEW_GOAL `hl (truncate_simplex x' (ul:(real^3)list)) 
          <= hl (truncate_simplex (LENGTH ul - 1) ul)`); 
(ASM_CASES_TAC `x' < LENGTH (ul:(real^3)list) - 1`); 
(MATCH_MP_TAC (REAL_ARITH `a < b ==> a <= b`)); 
(NEW_GOAL `x' < (LENGTH (ul:(real^3)list) - 1) /\ LENGTH ul - 1 <= 3`); 
(ASM_REWRITE_TAC[] THEN UNDISCH_TAC `barV V 3 ul`); 
(REWRITE_TAC[BARV] THEN ARITH_TAC); 
(UP_ASM_TAC); 
(NEW_GOAL `ul IN barV V 3`); 
(ASM_MESON_TAC[IN]); 
(ASM_MESON_TAC[XNHPWAB4; ARITH_RULE `3 <= 3`]); 
(MATCH_MP_TAC (REAL_ARITH `a = b ==> a <= b`)); 
(REWRITE_WITH `LENGTH (ul:(real^3)list) - 1 = x'`); 
(ASM_ARITH_TAC); 
  (* End subgoal 1.1 *)

  (* New subgoal 1.2 *)
(NEW_GOAL `hl (truncate_simplex (LENGTH ul - 1) ul) = hl (ul:(real^3)list)`); 
(AP_TERM_TAC); 
(REWRITE_TAC[TRUNCATE_SIMPLEX]); 
(MATCH_MP_TAC SELECT_UNIQUE); 
(GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;INITIAL_SUBLIST] THEN EQ_TAC); 
STRIP_TAC; 
(NEW_GOAL `LENGTH (ul:(real^3)list) = 
             LENGTH (y:(real^3)list) + LENGTH (yl:(real^3)list)`); 
(ASM_MESON_TAC[LENGTH_APPEND]); 
(NEW_GOAL `LENGTH (yl:(real^3)list) = 0`); 
(ASM_ARITH_TAC); 
(NEW_GOAL `(yl:(real^3)list) = []`); 
(ASM_MESON_TAC[LENGTH_EQ_NIL]); 
(ASM_MESON_TAC[APPEND_NIL]); 
(REPEAT STRIP_TAC); 
(ASM_REWRITE_TAC[]); 
(ASM_ARITH_TAC); 
(EXISTS_TAC `[]:(real^3)list`); 
(ASM_MESON_TAC[APPEND_NIL]); 
  (* End subgoal 1.2 *)

  (* New subgoal 1.3 *)

(NEW_GOAL `?u0 u1 u2 u3:real^3. ul = [u0;u1;u2;u3]`); 
(ASM_MESON_TAC[BARV_3_EXPLICIT]); 
(REPEAT (FIRST_X_ASSUM CHOOSE_TAC)); 
(REWRITE_TAC[ASSUME `ul = [u0:real^3; u1; u2; u3]`; HD]); 

  (* ---------------------------------------------- *)
  (* Consider case x' = 0 *)

(ASM_CASES_TAC `x' = 0`); 
(REWRITE_WITH `x:real^3 = u0`); 
(MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`)); 
(ASM_MESON_TAC[OMEGA_LIST_0_EXPLICIT; GSYM IN]); 
(ASM_REWRITE_TAC[DIST_REFL]); 
(MESON_TAC[SQRT_LT_0;REAL_ARITH `&0 <= &2 /\ &0 < &2`]); 

  (* ---------------------------------------------- *)
  (* Consider case x' = 1 *)

(ASM_CASES_TAC `x' = 1`); 
(REWRITE_WITH `x:real^3 = circumcenter {u0, u1}`); 
(MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`)); 
(ASM_MESON_TAC[OMEGA_LIST_1_EXPLICIT; GSYM IN]); 
(ONCE_REWRITE_TAC[DIST_SYM]); 
(REWRITE_WITH `dist (circumcenter {u0:real^3, u1},u0) 
               = hl (truncate_simplex x' (ul:(real^3)list))`); 
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;HL;radV]); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(MATCH_MP_TAC SELECT_UNIQUE); 
(GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list] 
   `set_of_list [u0:real^3;u1] = {u0, u1}`] THEN EQ_TAC); 
(DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC)); 
(SUBGOAL_THEN `(u0:real^3) IN {u0, u1}` ASSUME_TAC); 
(SET_TAC[]); 
(ASM_MESON_TAC[IN]); 
(REPEAT STRIP_TAC); 
(NEW_GOAL `w IN {u0,u1:real^3}`); 
(UP_ASM_TAC THEN MESON_TAC[IN]); 
(NEW_GOAL 
 `(!w. w IN {u0,u1:real^3} ==> radV {u0,u1} = dist (circumcenter {u0,u1},w))`); 
(MATCH_MP_TAC OAPVION2); 
(REWRITE_TAC[AFFINE_INDEPENDENT_2]); 
(ASM_REWRITE_TAC[]); 
(NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},w))`); 
(ASM_SIMP_TAC[]); 
(NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},u0))`); 
(FIRST_ASSUM MATCH_MP_TAC); 
(SET_TAC[]); 
(ASM_MESON_TAC[]); 
(ASM_REAL_ARITH_TAC); 

  (* ---------------------------------------------- *)
  (* Consider case x' = 2 *)

(ASM_CASES_TAC `x' = 2`); 
(REWRITE_WITH `x:real^3 = circumcenter {u0, u1, u2}`); 
(MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`)); 
(ASM_MESON_TAC[OMEGA_LIST_2_EXPLICIT; GSYM IN]); 
(ONCE_REWRITE_TAC[DIST_SYM]); 
(REWRITE_WITH `dist (circumcenter {u0:real^3, u1, u2},u0) 
               = hl (truncate_simplex x' (ul:(real^3)list))`); 
(ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;HL;radV]); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(MATCH_MP_TAC SELECT_UNIQUE); 
(GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list] 
   `set_of_list [u0:real^3;u1;u2] = {u0, u1, u2}`] THEN EQ_TAC); 
(DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC)); 
(SUBGOAL_THEN `(u0:real^3) IN {u0, u1, u2}` ASSUME_TAC); 
(SET_TAC[]); 
(ASM_MESON_TAC[IN]); 
(REPEAT STRIP_TAC); 
(NEW_GOAL `w IN {u0,u1:real^3,u2}`); 
(UP_ASM_TAC THEN MESON_TAC[IN]); 
(NEW_GOAL `(!w. w IN {u0,u1:real^3, u2} ==> 
             radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w))`); 
(MATCH_MP_TAC OAPVION2); 
(MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET); 
(EXISTS_TAC `{u0, u1, u2, u3:real^3}`); 
(REWRITE_TAC[SET_RULE `{a, b:A, c} SUBSET {a, b , c, d:A}`]); 
(REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]); 
STRIP_TAC; 
(REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]); 
(NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`); 
(REWRITE_TAC[MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]); 
(MATCH_MP_TAC MHFTTZN1); 
(EXISTS_TAC `V:real^3->bool`); 
(ASM_MESON_TAC[ARITH_RULE `3 <= 3`]); 
(ONCE_ASM_REWRITE_TAC[]); 
(NEW_GOAL `FINITE {u1, u2, u3:real^3}`); 
(REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]); 
(MATCH_MP_TAC (ARITH_RULE 
  `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`)); 
(MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`)); 
(NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
            (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}  
             else SUC (CARD {u1, u2, u3} ))`); 
(UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]); 
(UP_ASM_TAC THEN COND_CASES_TAC); 
(DISCH_TAC); 
(NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`); 
(REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=> 
            {u1, u2, u3:real^3} = {u0, u1, u2, u3}`); 
(MATCH_MP_TAC SUBSET_CARD_EQ); 
(STRIP_TAC); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(SET_TAC[]); 
(ASM_MESON_TAC[]); 

(REWRITE_TAC[MESON[set_of_list] 
  `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]); 
(MATCH_MP_TAC AFF_DIM_LE_LENGTH); 
(REWRITE_TAC[LENGTH]); 
(ARITH_TAC); 
(NEW_GOAL `F`); 
(ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]); 
(ASM_MESON_TAC[]); 
 STRIP_TAC; 
(NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`); 
(NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`); 
(MATCH_MP_TAC (ARITH_RULE 
 `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`)); 
 STRIP_TAC; 
(REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]); 
(REWRITE_TAC[LENGTH] THEN ARITH_TAC); 
(ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`); 
(NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`); 
(NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
  (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`); 
(NEW_GOAL `FINITE {u1,u2,u3:real^3}`); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(ASM_REWRITE_TAC[CARD_CLAUSES]); 
(UP_ASM_TAC THEN COND_CASES_TAC); 
(ASM_ARITH_TAC); 
(ASM_ARITH_TAC); 
(ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`); 


(NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} 
           < int_of_num (CARD {u0, u1, u2, u3})`); 
(REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`); 
(EXPAND_TAC "xl"); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(MATCH_MP_TAC SET_OF_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(MATCH_MP_TAC AFF_DIM_LE_LENGTH); 
(REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`); 
(EXPAND_TAC "xl"); 
(MATCH_MP_TAC SET_OF_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(EXPAND_TAC "xl"); 
(MATCH_MP_TAC LENGTH_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(NEW_GOAL `F`); 
(ASM_ARITH_TAC); 
(ASM_MESON_TAC[]); 
(ASM_ARITH_TAC); 
 ASM_ARITH_TAC; 
(MATCH_MP_TAC (REAL_ARITH 
  `radV {u0,u1,u2:real^3} = a /\ radV {u0,u1,u2} = b ==> a = b`)); 
 STRIP_TAC; 
(ASM_REWRITE_TAC[]); 
(FIRST_ASSUM MATCH_MP_TAC); 
(SET_TAC[]); 
(FIRST_ASSUM MATCH_MP_TAC); 
(ASM_REWRITE_TAC[]); 
(ASM_REAL_ARITH_TAC); 

  (* ---------------------------------------------- *)
  (* Consider case x' = 3 *)

(ASM_CASES_TAC `x' = 3`); 
(REWRITE_WITH `x = circumcenter {u0,u1,u2,u3:real^3}`); 
(ASM_REWRITE_TAC[]); 
(MATCH_MP_TAC OMEGA_LIST_3_EXPLICIT); 
(ASM_MESON_TAC[GSYM IN]); 
(NEW_GOAL `dist (u0,circumcenter {u0:real^3, u1, u2, u3}) 
           = hl (ul:(real^3)list)`); 
(ASM_REWRITE_TAC[HL]); 
(REWRITE_WITH `set_of_list [u0:real^3; u1; u2; u3] = {u0,u1,u2,u3}`); 
(MESON_TAC[set_of_list]); 

(NEW_GOAL `(!w. w IN {u0,u1:real^3, u2,u3} ==> 
             radV {u0,u1,u2,u3} = dist (circumcenter {u0,u1,u2,u3},w))`); 
(MATCH_MP_TAC OAPVION2); 
(REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]); 
 STRIP_TAC; 
(REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]); 
(NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`); 
(REWRITE_TAC[MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]); 
(MATCH_MP_TAC MHFTTZN1); 
(EXISTS_TAC `V:real^3->bool`); 
(ASM_MESON_TAC[ARITH_RULE `3 <= 3`]); 
(ONCE_ASM_REWRITE_TAC[]); 
(MATCH_MP_TAC (ARITH_RULE 
  `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`)); 
(MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`)); 

(NEW_GOAL `FINITE {u1, u2, u3:real^3}`); 
(REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]); 
(NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
            (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}  
             else SUC (CARD {u1, u2, u3} ))`); 
(UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]); 
(UP_ASM_TAC THEN COND_CASES_TAC); 
(DISCH_TAC); 
(NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`); 
(REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=> 
            {u1, u2, u3:real^3} = {u0, u1, u2, u3}`); 
(MATCH_MP_TAC SUBSET_CARD_EQ); 
(STRIP_TAC); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(SET_TAC[]); (* check *)
(ASM_MESON_TAC[]); 

(REWRITE_TAC[MESON[set_of_list] 
  `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]); 
(MATCH_MP_TAC AFF_DIM_LE_LENGTH); 
(REWRITE_TAC[LENGTH]); 
(ARITH_TAC); 
(NEW_GOAL `F`); 
(ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]); 
(ASM_MESON_TAC[]); 
 STRIP_TAC; 
(NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`); 
(NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`); 
(MATCH_MP_TAC (ARITH_RULE 
 `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`)); 
 STRIP_TAC; 
(REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]); 
(REWRITE_TAC[LENGTH] THEN ARITH_TAC); 
(ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`); 
(NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`); 
(NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
  (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`); 
(NEW_GOAL `FINITE {u1,u2,u3:real^3}`); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(ASM_REWRITE_TAC[CARD_CLAUSES]); 
(UP_ASM_TAC THEN COND_CASES_TAC); 
(ASM_ARITH_TAC); 
(ASM_ARITH_TAC); 
(ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`); 


(NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} 
           < int_of_num (CARD {u0, u1, u2, u3})`); 
(REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`); 
(EXPAND_TAC "xl"); 
(ONCE_REWRITE_TAC[EQ_SYM_EQ]); 
(MATCH_MP_TAC SET_OF_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(MATCH_MP_TAC AFF_DIM_LE_LENGTH); 
(REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`); 
(EXPAND_TAC "xl"); 
(MATCH_MP_TAC SET_OF_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(EXPAND_TAC "xl"); 
(MATCH_MP_TAC LENGTH_LIST_OF_SET); 
(REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]); 
(NEW_GOAL `F`); 
(ASM_ARITH_TAC); 
(ASM_MESON_TAC[]); 
(ASM_ARITH_TAC); 
 ASM_ARITH_TAC; 
(MATCH_MP_TAC (REAL_ARITH 
  `radV {u0,u1,u2:real^3,u3} = a /\ radV {u0,u1,u2,u3} = b ==> a = b`)); 
 STRIP_TAC; 
(ONCE_REWRITE_TAC[DIST_SYM] THEN FIRST_ASSUM MATCH_MP_TAC); 
(SET_TAC[]); 
(MESON_TAC[]); 

(ASM_MESON_TAC[]); 

(* --------------------------------------------- *)

(UNDISCH_TAC `barV V 3 (ul:(real^3)list)`); 
(REWRITE_TAC[BARV]); 
(STRIP_TAC); 
(NEW_GOAL `F`); 
(ASM_ARITH_TAC); 
(ASM_MESON_TAC[]); 

(* 
Here we have finished the first part `mcell0 V ul = {}`;there are 3 parts left:
mcell1 V ul = {}
mcell2 V ul = {}
mcell3 V ul = {}
*)

(* =============== Case 2 =================================== *)

(REWRITE_TAC[mcell1]); 
(COND_CASES_TAC); 
(NEW_GOAL `F`); 
(UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC); 
(UP_ASM_TAC THEN MESON_TAC[]); 
(REWRITE_TAC[]); 

(* =============== Case 3 =================================== *) 
(REWRITE_TAC[mcell2]); 
(COND_CASES_TAC); 
(NEW_GOAL `F`); 
(UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC); 
(UP_ASM_TAC THEN MESON_TAC[]); 
(REWRITE_TAC[]); 

(* =============== Case 4 =================================== *) 

(REWRITE_TAC[mcell3]); 
(COND_CASES_TAC); 
(NEW_GOAL `F`); 
(ASM_REAL_ARITH_TAC); 
(ASM_MESON_TAC[]); 
(MESON_TAC[]); 


(* =============== Reverse part =============================== *)

(REPEAT STRIP_TAC); 
(ASM_CASES_TAC `hl (ul:(real^3)list) >= sqrt (&2)`); 
(NEW_GOAL `omega_list V (ul:(real^3)list) IN mcell0 V ul`); 
(REWRITE_TAC[mcell0; IN_DIFF;ROGERS]); 
(STRIP_TAC); 
(NEW_GOAL`LENGTH (ul:(real^3)list) = 4`); 
(NEW_GOAL `?u0 u1 u2 u3:real^3. ul = [u0; u1; u2; u3]`); 
(MATCH_MP_TAC BARV_3_EXPLICIT); 
(EXISTS_TAC `V:real^3->bool`); 
(ASM_REWRITE_TAC[]); 
(FIRST_X_ASSUM CHOOSE_TAC); 
(FIRST_X_ASSUM CHOOSE_TAC); 
(FIRST_X_ASSUM CHOOSE_TAC); 
(FIRST_X_ASSUM CHOOSE_TAC); 
(ASM_REWRITE_TAC[LENGTH]); 
(ARITH_TAC); 
(ASM_REWRITE_TAC[OMEGA_LIST; ARITH_RULE `4 - 1 = 3`]); 
(REWRITE_TAC[IMAGE; CONVEX_HULL_EXPLICIT; IN; IN_ELIM_THM]); 
(EXISTS_TAC `{omega_list_n V (ul:(real^3)list) 3}`); 
(ABBREV_TAC `u = (\x:real^3. &1 )`); 

(EXISTS_TAC `(\x:real^3. &1)`); 
(REPEAT STRIP_TAC); 
(MESON_TAC[FINITE_SING]); 
(REWRITE_TAC[SUBSET;IN;IN_ELIM_THM; Geomdetail.IN_ACT_SING]); 
(GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]); 
(EXISTS_TAC `3`); 
(ASM_REWRITE_TAC[ARITH_RULE `3 < 4`]); 
(REWRITE_TAC[BETA_THM]); 
(REAL_ARITH_TAC); 
(REWRITE_TAC[SUM_SING]); 
(REWRITE_TAC[VSUM_SING]); 
(VECTOR_ARITH_TAC); 
(REWRITE_TAC[IN; ball; IN_ELIM_THM]); 
(ONCE_REWRITE_TAC[DIST_SYM]); 
(MATCH_MP_TAC (REAL_ARITH `x <= y ==> ~(y < x)`)); 
(MATCH_MP_TAC (REAL_ARITH `hl (ul:(real^3)list) >= x /\ hl ul <= z ==> x <= z`)); 
(ASM_REWRITE_TAC[]); 
(MATCH_MP_TAC WAUFCHE1); 
(EXISTS_TAC `3`); 
(ASM_REWRITE_TAC[IN]); 
(NEW_GOAL `F`); 
(UP_ASM_TAC THEN UNDISCH_TAC `mcell0 V (ul:(real^3)list) = {}`); 
(SET_TAC[]); 
(UP_ASM_TAC THEN MESON_TAC[]); 
(UP_ASM_TAC THEN REAL_ARITH_TAC)]);;
 

end;;