(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Lemma: TARJJUW                                                             *)
(* Chapter: packing                                                           *)
(* Author: Dang Tat Dat                                                       *)
(* Date: 2010-02-13                                                           *)
(* ========================================================================== *)

(* edits by thales:
    wrapped in a module.
   Moved into the project on August 2, 2010.
*)

module Tarjjuw  = struct

(*
needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;

flyspeck_needs "general/prove_by_refinement.hl";;
flyspeck_needs "general/sphere.hl";;
*)
open Sphere;;
open Prove_by_refinement;;
(*-----------Definition------------------------------------------------------*)
let weakly_saturated = 
    new_definition 
     `weakly_saturated (V:real^3 ->bool) (r:real) (r':real) <=>
        (!(v:real^3).(&2 <= dist(vec 0,v) ) /\ (dist(vec 0, v) <= r') ==>
            (?(u:real^3). (u IN V) /\ (~((vec 0) = u)) /\ (dist(u,v) < r)))`;;
let half_spaces =
    new_definition 
    `half_spaces (a:real^3) (b:real) =
     {x:real^3| (a dot x) <= b}`;;
(*----------------------------------------------------------------------------*)
let CHANGE_TARJJUW_1 = 
prove (`!(v:real^3) (r':real) (p:real^3).(&0 < r') /\ (~(p = vec 0)) /\ (v = (r'/(norm p))% p) ==> (r' = norm v)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN 
SUBGOAL_THEN `norm (v:real^3) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL 
[REWRITE_TAC [] THEN
ASM_MESON_TAC [];SUBGOAL_THEN `&0 < norm (p:real^3)` ASSUME_TAC THENL
[REWRITE_TAC[] THEN 
ASM_REWRITE_TAC [NORM_POS_LT];SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))%p) = (abs (r'/norm p))*(norm p)` ASSUME_TAC THENL [REWRITE_TAC[] THEN REWRITE_TAC [NORM_MUL];SUBGOAL_THEN `&0 < ((r':real)/(norm (p:real^3)))` ASSUME_TAC THENL [REWRITE_TAC[] THEN ASM_MESON_TAC [REAL_LT_DIV];SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) = r'/(norm p)` ASSUME_TAC THENL [REWRITE_TAC[] THEN ASM_REWRITE_TAC [REAL_ABS_REFL] THEN ASM_ARITH_TAC;SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) * norm p = ((r':real) / norm (p:real^3)) * norm p` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `~(norm (p:real^3) = &0)` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_MESON_TAC [REAL_DIV_RMUL]]]]]]]]);;
let CHANGE_TARJJUW_11 = 
prove (`!(v:real^3) (r':real) (p:real^3). (&0 < r') /\ (~(p = vec 0)) /\ (v = (r'/(norm p))% p) ==> norm (((r')/(norm (p)))%p) = r'`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `(r':real) = norm (v:real^3)` ASSUME_TAC THENL
[ASM_MESON_TAC [CHANGE_TARJJUW_1];
SUBGOAL_THEN `norm (v:real^3) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL
[ASM_MESON_TAC[];
SUBGOAL_THEN `(r':real) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL
[ASM_ARITH_TAC;ASM_MESON_TAC [EQ_SYM_EQ]]]]);;
let CHANGE_TARJJUW_12 = 
prove (`!(v:real^3) (r':real) (p:real^3). (&0 < r') /\ (~(p = vec 0)) ==> norm (((r')/(norm (p)))%p) = r'`,
REPEAT GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `&0 < norm (p:real^3)` ASSUME_TAC THENL 
[REWRITE_TAC[] THEN
ASM_REWRITE_TAC [NORM_POS_LT];
SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))%p) = (abs (r'/norm p))*(norm p)` ASSUME_TAC THENL 
[REWRITE_TAC[] THEN
REWRITE_TAC [NORM_MUL];
SUBGOAL_THEN `&0 < ((r':real)/(norm (p:real^3)))` ASSUME_TAC THENL
[REWRITE_TAC[] THEN
ASM_MESON_TAC [REAL_LT_DIV];
SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) = r'/(norm p)` ASSUME_TAC THENL
[REWRITE_TAC[] THEN
ASM_REWRITE_TAC [REAL_ABS_REFL] THEN ASM_ARITH_TAC;
SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) * norm p = ((r':real) / norm (p:real^3)) * norm p` ASSUME_TAC THENL
[ASM_ARITH_TAC;
SUBGOAL_THEN `~(norm (p:real^3) = &0)` ASSUME_TAC THENL 
[ASM_ARITH_TAC;
SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))%p) =  ((r':real) / norm (p:real^3)) * norm p` ASSUME_TAC THENL 
[REWRITE_TAC[] THEN ASM_ARITH_TAC;
ASM_MESON_TAC [REAL_DIV_RMUL]]]]]]]]);;
(*-------------------------------------------------------------------*)
let CHANGE_TARJJUW_2 = 
prove (`!(v:real^3) (r':real) (p:real^3).(~(p = vec 0)) /\ (v = (r'/(norm p))% p) ==>
(r'% p = (norm p)%v)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `(norm (p:real^3)) % (v:real^3) =(norm (p:real^3)) % ((r'/(norm p))% p) ` ASSUME_TAC THENL [REWRITE_TAC [] THEN ASM_MESON_TAC [VECTOR_MUL_LCANCEL];SUBGOAL_THEN `(norm (p:real^3)) % (((r':real)/(norm p))% p) = ((norm p) * (r'/norm p))%p` ASSUME_TAC THENL [REWRITE_TAC[] THEN MESON_TAC[VECTOR_MUL_ASSOC];SUBGOAL_THEN `~(norm (p:real^3) = &0)` ASSUME_TAC THENL [REWRITE_TAC[] THEN REWRITE_TAC[NORM_EQ_0] THEN ASM_MESON_TAC[];SUBGOAL_THEN `(norm (p:real^3)) * ((r':real)/norm p) = r'` ASSUME_TAC THENL [REWRITE_TAC[] THEN ASM_MESON_TAC [REAL_DIV_LMUL];SUBGOAL_THEN `((norm (p:real^3)) * ((r':real)/norm p))%p = r' % p` ASSUME_TAC THENL [REWRITE_TAC[] THEN ASM_MESON_TAC[];ASM_MESON_TAC[]]]]]]);;
(*-------------------------------------------------------------------*)

let CHANGE_TARJJUW_3 = 
prove_by_refinement(`!(V:real^3 -> bool)(u:real^3).(packing V)  /\ (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (u IN V) ==> &2 <= norm u`,

[
 (REPEAT GEN_TAC THEN REWRITE_TAC [ball; DIFF;SUBSET]);
 (STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC));
 (DISCH_TAC);
 (DISCH_THEN (LABEL_TAC "F1"));
 (REWRITE_TAC [IN] THEN REPEAT STRIP_TAC);
 (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));
 (ASM_REWRITE_TAC [IN;IN_ELIM_THM]);
 (STRIP_TAC);
 (POP_ASSUM MP_TAC);
 (REWRITE_TAC [DIST_0]);
 (ARITH_TAC);

]);;


let CHANGE_TARJJUW_31 = 
prove_by_refinement( `!(V:real^3 -> bool)(u:real^3).(packing V)  /\ (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (u IN V) ==> ~(u = vec 0)`,

[
 (REPEAT GEN_TAC);
 (STRIP_TAC);
 (SUBGOAL_THEN `&2 <= norm (u:real^3)` ASSUME_TAC);
 (ASM_MESON_TAC [CHANGE_TARJJUW_3]);
 (MP_TAC (ISPECL [`&0`;`&2`;`norm (u:real^3)`]REAL_LTE_TRANS));
 (ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
 (REWRITE_TAC[NORM_POS_LT]);

]);;

let CHANGE_TARJJUW_32 = 
prove_by_refinement(`!(V:real^3 -> bool)(u:real^3)(v:real^3).(packing V) /\ (vec 0 IN V) /\ (u IN V) /\ (~(vec 0 = u)) ==> &2 <= norm u`,

[
 (REPEAT GEN_TAC THEN REWRITE_TAC [packing;IN] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "F1") THEN REPEAT STRIP_TAC);
 (ASM_CASES_TAC `&2 <= norm (u:real^3)` THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN REWRITE_TAC [GSYM DIST_0]]);
 (STRIP_TAC THEN REMOVE_THEN "F1" (MP_TAC o SPECL [`(vec 0):real^3`;`u:real^3`]));
 (ASM_REWRITE_TAC[]);

]);;
(*------------------------------------------------------------------------*)

let CHANGE_TARJJUW_4 =
prove (`!(u:real^3) (v:real^3) (r:real).dist (u,v) < r ==> (dist (u,v)) pow 2 < r pow 2`,
REPEAT GEN_TAC THEN REWRITE_TAC [dist] THEN STRIP_TAC THEN SUBGOAL_THEN `&0 <= norm ((u:real^3) - (v:real^3))` ASSUME_TAC THENL [REWRITE_TAC [NORM_POS_LE];SUBGOAL_THEN `&0 <= r` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `abs (norm ((u:real^3) - (v:real^3))) = norm (u - v)` ASSUME_TAC THENL [REWRITE_TAC [REAL_ABS_NORM];SUBGOAL_THEN `abs (r:real) = r` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `abs (norm ((u:real^3) - (v:real^3))) < abs(r:real)` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_MESON_TAC [REAL_LT_SQUARE_ABS]]]]]]);;
(*-------------------------------------------------------------------------*)

let CHANGE_TARJJUW_5 =
prove (`!(V:real^3 -> bool)(g:real^3->real) (r:real) (r':real) (u:real^3) (v:real^3) (p:real^3).(packing V) /\ V SUBSET (:real^3) DIFF ball (vec 0,&2) /\ (&2 <= r) /\ (r <= r') /\  (~(p = vec 0)) /\ ((((g u) * r')/ &2) < norm p) /\ (v = (r'/(norm p))% p) /\ ((u dot p) <= (g u)) /\ (~(vec 0 = u)) /\ (dist (u,v) < r) /\ (u IN V)  ==> (norm p < norm p)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`v:real^3`;`r':real`]CHANGE_TARJJUW_1)
THEN DISCH_THEN (MP_TAC o SPEC `p:real^3`)
THEN MP_TAC (ISPECL [`&2`;`r:real`;`r':real`]REAL_LE_TRANS) 
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS) 
THEN ASM_REWRITE_TAC[ARITH_RULE `&0 < &2`]
THEN STRIP_TAC 
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(v:real^3) = (r':real) / norm p % (p:real^3)`
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`v:real^3`]NORM_POS_LE) 
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`((u:real^3) dot (p:real^3))`;`((g:real^3->real)(u:real^3))`;`(norm (v:real^3))`]REAL_LE_RMUL)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `((u:real^3) dot (p:real^3)) <= ((g:real^3->real)(u:real^3))`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= norm (v:real^3)`
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`(((u:real^3) dot (p:real^3)) * (norm (v:real^3)))`;`(((g:real^3->real)(u:real^3)) * norm v)`;`&2`](GSYM REAL_LE_DIV2_EQ))
THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
THEN STRIP_TAC
(*Sub 1*)
THEN SUBGOAL_THEN `((u dot p) * norm (v:real^3)) / &2 <= (((g:real^3->real)(u:real^3)) * norm v) / &2` ASSUME_TAC
THENL [ASM_ARITH_TAC;MP_TAC (ISPECL [`((u:real^3) dot (p:real^3))`;`(r':real)`]REAL_MUL_SYM)
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`r':real`;`u:real^3`;`p:real^3`]DOT_RMUL)
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`v:real^3`;`r':real`;`p:real^3`]CHANGE_TARJJUW_2)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `~(p:real^3 = vec 0)`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `v:real^3 = (r':real) / norm p % (p:real^3)`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `v:real^3 = (r':real) / norm p % (p:real^3)`
THEN STRIP_TAC
THEN 
(*Sub 1.1 ]]*)
SUBGOAL_THEN `(u:real^3) dot ((r':real)% (p:real^3)) = u dot ((norm p)%v)` ASSUME_TAC
THENL [ASM_MESON_TAC[];MP_TAC (ISPECL [`(norm (p:real^3))`;`(u:real^3)`;`(v:real^3)`]DOT_RMUL)
THEN STRIP_TAC (*]]);;*)
(*Sub 1.1.1]]]*)
THEN SUBGOAL_THEN `((u:real^3) dot (p:real^3)) * (r':real) = norm p * (u dot (v:real^3))` ASSUME_TAC
THENL [FIND_ASSUM (fun th -> REWRITE_TAC [th]) `((u:real^3) dot (p:real^3)) * (r':real) = r' * (u dot p)`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(u:real^3) dot (r':real) % (p:real^3)= r' * (u dot p)`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(u:real^3) dot (r':real) % (p:real^3)= r' * (u dot p)`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MESON_TAC[EQ_TRANS];
MP_TAC (ISPECL [`(u:real^3)`;`(v:real^3)`]DOT_NORM_NEG)
THEN STRIP_TAC (*]]]);;*)
(*Sub 1.1.1.1 ]]]]*)
THEN SUBGOAL_THEN `((norm (p:real^3)) * ((u:real^3) dot (v:real^3))) = (((norm p) *(((norm u pow 2 + norm v pow 2) - (norm (u - v)) pow 2)) / &2))` ASSUME_TAC
THENL [POP_ASSUM MP_TAC
THEN MESON_TAC[];
POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM dist] THEN STRIP_TAC
THEN MP_TAC (ISPECL [`V:real^3->bool`;`u:real^3`]CHANGE_TARJJUW_3)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`&2`]REAL_ABS_REFL)
THEN REWRITE_TAC [ARITH_RULE `&0 <= &2`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`u:real^3`]REAL_ABS_NORM) THEN STRIP_TAC (*]]]]);;*)
THEN 
(*Sub 1.1.1.1.1 ]]]]]*)
SUBGOAL_THEN `abs (&2) <= abs (norm (u:real^3))` ASSUME_TAC
THENL [ASM_ARITH_TAC;
MP_TAC (ISPECL [`&2`;`norm (u:real^3)`]REAL_LE_SQUARE_ABS)
THEN POP_ASSUM (fun th -> REWRITE_TAC [th])
THEN REWRITE_TAC [ARITH_RULE `&2 pow 2 = &4`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`u:real^3`;`v:real^3`;`r:real`]CHANGE_TARJJUW_4)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `dist (u:real^3,v:real^3) < r:real`
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`((r:real) pow 2)`;`dist (u:real^3,v:real^3) pow 2`]REAL_LT_NEG)
THEN FIRST_ASSUM (fun th -> REWRITE_TAC [th])
THEN STRIP_TAC (*]]]]]);;*)
(*Sub 1.1.1.1.1.1 ]]]]]]*)
THEN SUBGOAL_THEN `(norm (v:real^3)) pow 2 = (r':real) pow 2`ASSUME_TAC
THENL [UNDISCH_TAC `r':real = norm (v:real^3)`
THEN MESON_TAC[];
(*Sub 1.1.1.1.1.1.2*)
SUBGOAL_THEN `((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) =
 (norm (u:real^3)) pow 2 + (r':real) pow 2` ASSUME_TAC
THENL [ASM_ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2*)
SUBGOAL_THEN `&4 + (norm (v:real^3)) pow 2 <= ((norm (u:real^3)) pow 2 + (norm v) pow 2 )` ASSUME_TAC
THENL [ASM_ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2.2*)
SUBGOAL_THEN `(((u:real^3) dot (p:real^3)) * (r':real)) / &2 < (norm (p))` ASSUME_TAC
THENL [UNDISCH_TAC `(((u:real^3) dot (p:real^3)) * norm (v:real^3)) / &2 <= ((g:real^3->real) u * norm v) / &2`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `r':real = norm (v:real^3)`
THEN UNDISCH_TAC `((g:real^3->real) (u:real^3) * (r':real)) / &2 < norm (p:real^3)`
THEN ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2.2.2*)
SUBGOAL_THEN `((norm (p:real^3)) * ((u:real^3) dot (v:real^3))) / &2 < (norm (p))`ASSUME_TAC
THENL [ASM_ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2.2.2*)
SUBGOAL_THEN `&4 + (r':real) pow 2 <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2 )` ASSUME_TAC
THENL [ASM_ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2.2.2*)
SUBGOAL_THEN `&4 + (r':real) pow 2 + --(dist ((u:real^3),(v:real^3)) pow 2) <= ((norm (u)) pow 2 + (norm (v)) pow 2 + --(dist (u,v) pow 2) )` ASSUME_TAC 
THENL [ASM_ARITH_TAC;
(*Sub 1.1.1.1.1.1.2.2.2.2*)
SUBGOAL_THEN `&4 + (r':real) pow 2 + --((r:real) pow 2)  <= &4 + (r':real) pow 2 + --(dist ((u:real^3),(v:real^3)) pow 2)` ASSUME_TAC
THENL [ASM_ARITH_TAC;
SUBGOAL_THEN `&4 + (r':real) pow 2 + --((r:real) pow 2) <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2 + --(dist (u,v) pow 2))` ASSUME_TAC 
THENL [ASM_ARITH_TAC;
MP_TAC (ISPECL [`&0`;`&2`;`r:real`]REAL_LE_TRANS)
THEN ASM_REWRITE_TAC[ARITH_RULE `&0 <= &2`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`&0`;`r:real`;`r':real`]REAL_LE_TRANS)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `&0 <= r:real`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `r:real <= r':real`
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`r':real`]REAL_ABS_REFL)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= r':real`
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`r:real`]REAL_ABS_REFL)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= r:real`
THEN STRIP_TAC(*]]]]]]]]]]]]]]);;*)

THEN SUBGOAL_THEN `abs (r:real) <= abs(r':real)` ASSUME_TAC
THENL [POP_ASSUM (fun th -> REWRITE_TAC[th])
THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
THEN ASM_REWRITE_TAC[];
MP_TAC (ISPECL [`r:real`;`r':real`]REAL_LE_SQUARE_ABS)
THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`r':real`;`r:real`]REAL_SUB_LE)
THEN UNDISCH_TAC `r:real <= r':real`
THEN STRIP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`(r':real) pow 2`;`(r:real) pow 2 `]REAL_SUB_LE)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(r:real) pow 2 <= (r':real) pow 2`
THEN STRIP_TAC(*]]]]]]]]]]]]]]]);;*)

THEN SUBGOAL_THEN `&4 <= &4 + (r':real) pow 2 - (r:real) pow 2` ASSUME_TAC
THENL [MP_TAC (ISPECL [`&4`;`&0`;`(r':real) pow 2 - (r:real) pow 2`]REAL_LE_LADD)
THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
THEN REWRITE_TAC [ARITH_RULE `&4 + &0 = &4`];
MP_TAC (ISPECL [`&4 + ((r':real) pow 2)`;`((r:real) pow 2)`]real_sub)
THEN STRIP_TAC(*]]]]]]]]]]]]]]]]);;*)

THEN SUBGOAL_THEN `&4 + ((r':real) pow 2) - ((r:real) pow 2) <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) + --(dist (u,v) pow 2)` ASSUME_TAC
THENL [ASM_ARITH_TAC;SUBGOAL_THEN `&4 <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) + --(dist (u,v) pow 2)` ASSUME_TAC 
THENL [ASM_ARITH_TAC;
MP_TAC (ISPECL [`(((norm (p:real^3)) * ((u:real^3) dot (v:real^3)))/ &2)`;`(norm (p:real^3))`;`&2`]REAL_LT_RMUL)
THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(norm (p:real^3) * ((u:real^3) dot (v:real^3))) / &2 < norm p`
THEN REWRITE_TAC [ARITH_RULE `(((norm (p:real^3)) * ((u:real^3) dot (v:real^3)))/ &2) * (&2) = ((norm (p:real^3)) * ((u:real^3) dot (v:real^3)))`]
THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]);;*)


THEN SUBGOAL_THEN `(((norm (p:real^3)) * (((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - dist (u,v) pow 2)) / &2) < (norm p) * (&2) ` ASSUME_TAC
THENL [ASM_ARITH_TAC;
MP_TAC (ISPECL [`((((norm (p:real^3)) * (((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - dist (u,v) pow 2)) / &2))`;`(norm (p:real^3)) * (&2)`;`&2`]REAL_LT_RMUL)
THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(norm (p:real^3) * ((norm (u:real^3) pow 2 + norm (v:real^3) pow 2) - dist (u,v) pow 2)) / &2 < norm p * &2`
THEN REWRITE_TAC [ARITH_RULE `((((norm (p:real^3)) * (((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - dist (u,v) pow 2)) / &2))*(&2) = ((norm (p:real^3)) * (((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - dist (u,v) pow 2))`]
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2)`;`(dist (u:real^3,v:real^3) pow 2)`]real_sub)
THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]]);;*)



THEN SUBGOAL_THEN `&4 <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - (dist (u,v) pow 2)` ASSUME_TAC
THENL [ASM_ARITH_TAC;
MP_TAC (ISPECL [`p:real^3`]NORM_POS_LE) THEN STRIP_TAC
THEN MP_TAC (ISPECL [`(norm (p:real^3))`;`&4`;`(((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - dist (u,v) pow 2)`]REAL_LE_LMUL)
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `&4 <= (norm (u:real^3) pow 2 + norm (v:real^3) pow 2) - dist (u,v) pow 2`
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `&0 <= norm (p:real^3)`
THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]]]);; *)
THEN MP_TAC (ISPECL [`(norm (p:real^3)) * (&4)`;`norm (p:real^3) * ((norm (u:real^3) pow 2 + norm v pow 2) - dist (u,v) pow 2)`;`(norm (p:real^3) * &2) * &2`]REAL_LET_TRANS)
THEN POP_ASSUM (fun th -> REWRITE_TAC [th])
THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `norm (p:real^3) * ((norm (u:real^3) pow 2 + norm v pow 2) - dist (u,v) pow 2) <
  (norm p * &2) * &2`
THEN ARITH_TAC]]]]]]]]]]]]]]]]]]]]);;

(*----------------------------------------------------------------*)
let CHANGE_TARJJUW_6 = 
prove_by_refinement(`!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) p:real^3 r r':real. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} /\ (p IN P)  ==>(!u:real^3. u IN V ==> p IN half_spaces u (g u))`,


[
(REPEAT GEN_TAC );
(STRIP_TAC);
(REWRITE_TAC [INTERS;IN_ELIM_THM] THEN STRIP_TAC);
(POP_ASSUM MP_TAC);
(ASM_REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(SUBGOAL_THEN `INTERS {half_spaces u (g u) | u IN V} SUBSET half_spaces (u:real^3) ((g:real^3->real) u)` ASSUME_TAC);
(REWRITE_TAC [SUBSET;IN_INTERS]);
(GEN_TAC);
(DISCH_THEN (LABEL_TAC "F1"));
(REMOVE_THEN "F1" (MP_TAC o SPEC `half_spaces (u:real^3) ((g:real^3 -> real) u)`));
(STRIP_TAC);
(SUBGOAL_THEN `half_spaces (u:real^3) ((g:real^3 -> real) u) IN {half_spaces u (g u) | u IN (V:real^3->bool)}` ASSUME_TAC);
(REWRITE_TAC [half_spaces]);
(REWRITE_TAC [IN_ELIM_THM]);
(EXISTS_TAC `u:real^3`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM MP_TAC);
(ASM_REWRITE_TAC[]);
(POP_ASSUM MP_TAC);
(REWRITE_TAC [SUBSET]);
(DISCH_THEN (MP_TAC o SPEC `p:real^3`));
(ASM_REWRITE_TAC[]);

]);;

let CHANGE_TARJJUW_7 = 
prove_by_refinement( `!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) u:real^3 r r':real. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} /\ u IN V   ==> (!p:real^3. p IN P ==> (u dot p) <= (g u))`,

[
(REPEAT GEN_TAC THEN STRIP_TAC);
(GEN_TAC);
(STRIP_TAC);
(SUBGOAL_THEN `(!u:real^3. u IN (V:real^3->bool) ==> p IN half_spaces u ((g:real^3->real) u))` ASSUME_TAC);
(ASM_MESON_TAC[CHANGE_TARJJUW_6]);
(POP_ASSUM MP_TAC);
(REWRITE_TAC [half_spaces;IN_ELIM_THM]);
(DISCH_THEN (MP_TAC o SPEC `u:real^3`));
(ASM_REWRITE_TAC[]);

]);;

let CHANGE_TARJJUW_71 = 
prove_by_refinement( `!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) r r':real. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} ==> (!p:real^3 u:real^3. p IN P /\ u IN V ==> (u dot p) <= ((g:real^3->real) u))`,

[
(REPEAT GEN_TAC);
(STRIP_TAC);
(REPEAT GEN_TAC);
(STRIP_TAC);
(SUBGOAL_THEN `!p:real^3. p IN (P:real^3->bool) ==> (u dot p) <= ((g:real^3->real)(u:real^3))` ASSUME_TAC);
(ASM_MESON_TAC [CHANGE_TARJJUW_7]);
(POP_ASSUM (MP_TAC o SPEC `p:real^3`));
(ASM_REWRITE_TAC[]);
]);;

let CHANGE_TARJJUW_8 = 
prove_by_refinement( `!(g:real^3->real)(r':real)(u:real^3).(&2 <= r) /\ (r <= r') /\ (&0 <= g u) ==> &0 <= ((g u) * r')/ &2`,


[
 (REPEAT GEN_TAC THEN STRIP_TAC);
 (SUBGOAL_THEN `&2 <= (r':real)` ASSUME_TAC);
 (ASM_ARITH_TAC);
 (SUBGOAL_THEN `&0 <= (r':real)` ASSUME_TAC);
 (POP_ASSUM MP_TAC);
 (MP_TAC (ARITH_RULE `&0 <= &2`));
 (MESON_TAC[REAL_LE_TRANS]);
 (MP_TAC (ISPECL [`(g:real^3->real) (u:real^3)`;`r':real`]REAL_LE_MUL));
 (ASM_REWRITE_TAC[]);
(STRIP_TAC);
 (MP_TAC (ISPECL [`(((g:real^3->real) (u:real^3)) * (r':real))`;`(&2)`]REAL_LE_DIV));
 (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &2`]);
]);;

let FININTE_GFUN = 
prove_by_refinement(`!(V:real^3 -> bool)(g:real^3->real) r':real.(FINITE V) /\ ~(V = {}) ==> FINITE {(g(u:real^3)*r')/(&2)|u IN V} /\ ~({(g(u:real^3)*r')/(&2)|u IN V} = {})`,

[
 (REPEAT GEN_TAC);
 (SUBGOAL_THEN `IMAGE (\u. ((g:real^3->real)(u:real^3) * (r':real)) / &2) (V:real^3->bool) = {(g u * r') / &2 | u IN V}` ASSUME_TAC);
 (REWRITE_TAC [IMAGE;EXTENSION]);
 (GEN_TAC);
 (EQ_TAC);
 (REWRITE_TAC [IN_ELIM_THM]);
 (REWRITE_TAC [IN_ELIM_THM]);
 (REPEAT STRIP_TAC);
 (MP_TAC (ISPECL [`\u. (((g:real^3->real)(u:real^3)) * (r':real)) / (&2)`;`V:real^3->bool`]FINITE_IMAGE));
 (ASM_REWRITE_TAC[]);
 (MP_TAC (ISPECL [`\u. (((g:real^3->real)(u:real^3)) * (r':real)) / (&2)`;`V:real^3->bool`]IMAGE_EQ_EMPTY));
 (ASM_REWRITE_TAC[]);

]);;

(*----------------------------------------------------------------------------*)
let CHANGE_TARJJUW_9 = 
prove_by_refinement(`!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) r r':real. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V/\ ~(V = {}) /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} ==> polyhedron P`,

[
(REPEAT GEN_TAC);
(STRIP_TAC);
(ASM_REWRITE_TAC [polyhedron]);
(EXISTS_TAC `{half_spaces (u:real^3) ((g:real^3->real) u)| u IN (V:real^3->bool)}`);
(REWRITE_TAC[]);
(STRIP_TAC);
(MP_TAC (ISPECL [`\u. half_spaces (u:real^3) ((g:real^3->real) u) `;`V:real^3->bool`]FINITE_IMAGE));
(ASM_REWRITE_TAC[]);
(SUBGOAL_THEN `IMAGE (\u. half_spaces (u:real^3) ((g:real^3->real)(u))) (V:real^3->bool) = {half_spaces u (g u) | u IN V}` ASSUME_TAC);
(REWRITE_TAC [IMAGE;EXTENSION]);
(STRIP_TAC);
(REWRITE_TAC [IN_ELIM_THM]);
(EQ_TAC);
(STRIP_TAC);
(EXISTS_TAC `x':real^3`);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC [EXTENSION]);
(STRIP_TAC);
(POP_ASSUM (MP_TAC o SPEC `x'':real^3`));
(ARITH_TAC);
(STRIP_TAC);
(EXISTS_TAC `u:real^3`);
(ASM_REWRITE_TAC []);
(ASM_REWRITE_TAC[]);
(ASM_REWRITE_TAC[half_spaces;IN_ELIM_THM]);
(GEN_TAC THEN STRIP_TAC);
(EXISTS_TAC `u:real^3`);
(EXISTS_TAC `((g:real^3->real)(u:real^3))`);
(MP_TAC (ISPECL [`V:real^3->bool`;`u:real^3`]CHANGE_TARJJUW_31));
(ASM_REWRITE_TAC[]);

]);;
let CHANGE_TARJJUW_10 = 
prove_by_refinement( `!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) r r':real u:real^3. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V/\ ~(V = {}) /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} /\ polyhedron P /\ u IN V ==>
(bounded P)`,

[
(REPEAT GEN_TAC);
(STRIP_TAC);
(SUBGOAL_THEN `!p:real^3 u:real^3. p IN P /\ u IN V ==> (u dot p) <= ((g:real^3->real) u)` ASSUME_TAC);
(ASM_MESON_TAC[CHANGE_TARJJUW_71]);
(REPEAT (POP_ASSUM MP_TAC));
(REWRITE_TAC [weakly_saturated;polyhedron;half_spaces] THEN STRIP_TAC);
(DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC);
(STRIP_TAC);
(DISCH_THEN (LABEL_TAC "F1"));
(DISCH_TAC);
(DISCH_THEN (LABEL_TAC "F2"));
(DISCH_TAC);
(DISCH_THEN (LABEL_TAC "F3")); 
(*
(ASM_CASES_TAC `(V:real^3->bool) = {}`);
(SUBGOAL_THEN `IMAGE (\(u:real^3). {x:real^3 | u dot x <= g u}) (V:real^3->bool) = {{x | u dot x <= g u} | u IN V}` ASSUME_TAC);
(REWRITE_TAC[IMAGE;EXTENSION]);
(GEN_TAC);
(EQ_TAC);
(REWRITE_TAC [IN_ELIM_THM]);
(STRIP_TAC);
(EXISTS_TAC `x':real^3`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM (LABEL_TAC "B1"));
(REWRITE_TAC [EXTENSION]);
(STRIP_TAC);
(REWRITE_TAC[IN_ELIM_THM]);
(REMOVE_THEN "B1" (MP_TAC o SPEC `x'':real^3`));
(ASM_REWRITE_TAC[]);
(REWRITE_TAC [IN_ELIM_THM]);
(STRIP_TAC);
(EXISTS_TAC `u':real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(REWRITE_TAC [IN_ELIM_THM]);
(MP_TAC (ISPECL [`(\(u:real^3). {x:real^3 | u dot x <= g u})`;`V:real^3->bool`]IMAGE_EQ_EMPTY));
(FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(V:real^3->bool) = {}`);
(POP_ASSUM MP_TAC);
(ASM_REWRITE_TAC[]);
(DISCH_TAC);
(POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
(DISCH_TAC);
( POP_ASSUM (fun th -> REWRITE_TAC [th]));
(REWRITE_TAC [INTERS_0]);
*)

(MP_TAC (ISPECL [`V:real^3->bool`;`(g:real^3->real)`;`r':real`]FININTE_GFUN));
(FIND_ASSUM (fun th -> REWRITE_TAC [th]) `~ ((V:real^3->bool) = {})`);
(FIND_ASSUM (fun th -> REWRITE_TAC [th]) `FINITE (V:real^3->bool) `);
(STRIP_TAC);
(ASM_CASES_TAC `bounded (P:real^3->bool)`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM MP_TAC);
(REWRITE_TAC [bounded]);
(REWRITE_TAC [NOT_EXISTS_THM;NOT_FORALL_THM]);
(REWRITE_TAC [NOT_IMP;REAL_NOT_LE]);
(DISCH_THEN (LABEL_TAC "F4"));
(REWRITE_TAC [GSYM bounded]);
(SUBGOAL_THEN `!u:real^3 . u IN (V:real^3->bool) ==> (?p:real^3. p IN (P:real^3->bool) /\ (((g:real^3->real)(u:real^3)) * (r':real)) / (&2) < norm p)` ASSUME_TAC);
(REPEAT STRIP_TAC);
(REMOVE_THEN "F4" (MP_TAC o SPEC `sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`));
(DISCH_THEN (X_CHOOSE_TAC `p:real^3`));
(POP_ASSUM MP_TAC THEN STRIP_TAC);
(EXISTS_TAC `p:real^3`);
(ASM_REWRITE_TAC[]);
(MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u':real^3) * (r':real)) / &2 `));
(REWRITE_TAC [IN_ELIM_THM]);
(SUBGOAL_THEN `(?u:real^3. u IN (V:real^3->bool) /\ ((g:real^3->real)(u':real^3) * (r':real)) / &2 = (g u * r') / &2)` ASSUME_TAC);
(EXISTS_TAC `u':real^3`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(STRIP_TAC);
(MP_TAC (ISPECL [`((g:real^3->real)(u':real^3) * (r':real)) / &2`;`sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`;`norm (p:real^3)`]REAL_LET_TRANS));
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(POP_ASSUM MP_TAC);
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(POP_ASSUM (LABEL_TAC "F5"));
(REMOVE_THEN "F4" (MP_TAC o SPEC `sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`));
(DISCH_THEN (X_CHOOSE_TAC `p:real^3`));
(POP_ASSUM MP_TAC THEN STRIP_TAC);
(REMOVE_THEN "F5" (MP_TAC o SPEC `u:real^3`));
(FIND_ASSUM (fun th ->REWRITE_TAC [th]) `(u:real^3) IN (V:real^3 -> bool)`);
(STRIP_TAC);
(USE_THEN "F3" (MP_TAC o SPECL [`p:real^3`;`u:real^3`]));
(FIND_ASSUM (fun th -> REWRITE_TAC [th])`(p:real^3) IN (P:real^3->bool)`);
(FIND_ASSUM (fun th -> REWRITE_TAC [th])`(u:real^3) IN (V:real^3->bool)`);
(DISCH_TAC);
(MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u:real^3) * (r':real)) / &2`));
(REWRITE_TAC [IN_ELIM_THM]);
(SUBGOAL_THEN `(?(u':real^3). u' IN (V:real^3->bool) /\ ((g:real^3->real)(u:real^3) * (r':real)) / &2 = (g u' * r') / &2)` ASSUME_TAC);
(EXISTS_TAC `u:real^3`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM (fun th -> REWRITE_TAC[th]));
(STRIP_TAC);
(MP_TAC (ISPECL [`((g:real^3->real)(u:real^3) * (r':real)) / &2`;`sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`;`norm (p:real^3)`]REAL_LET_TRANS));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(ASM_CASES_TAC `(p:real^3) = vec 0`);
(SUBGOAL_THEN `((r':real)/(norm (p:real^3)))% p = vec 0` ASSUME_TAC);
(POP_ASSUM (fun th -> REWRITE_TAC [th]));
(MESON_TAC [VECTOR_MUL_RZERO]);
(SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))% p) = &0` ASSUME_TAC );
(ASM_REWRITE_TAC[]);
(REWRITE_TAC [NORM_EQ_0]);
(MP_TAC (ISPECL [`p:real^3`]NORM_EQ_0));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(UNDISCH_TAC `((g:real^3->real)(u:real^3) * (r':real)) / (&2) < norm (p:real^3)`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(USE_THEN "F3" (MP_TAC o SPECL [`(vec 0):real^3`;`u:real^3`]));
(UNDISCH_TAC `(p:real^3) IN (P:real^3->bool)`);
(UNDISCH_TAC `p:real^3 = vec 0`);
(DISCH_TAC THEN POP_ASSUM (fun th ->REWRITE_TAC [th]));
(DISCH_TAC THEN POP_ASSUM (fun th ->REWRITE_TAC [th]));
(FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(u:real^3) IN (V:real^3->bool)`);
(UNDISCH_TAC `(P:real^3->bool) = INTERS {{x:real^3 | u dot x <= (g:real^3->real)(u)} | (u:real^3) IN (V:real^3->bool)}`);
(DISCH_TAC);
(POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
(REWRITE_TAC [DOT_RZERO]);
(SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
(ASM_ARITH_TAC);
(MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS));
(ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
(STRIP_TAC);
(MP_TAC (ARITH_RULE `(((g:real^3->real))(u:real^3) * (r':real)) / &2 < &0 <=> g u * r' < &0`));
(POP_ASSUM MP_TAC);
(POP_ASSUM MP_TAC);
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(REPEAT STRIP_TAC);
(MP_TAC (ISPECL [`((g:real^3->real))(u:real^3)`;`&0`;`r':real`]REAL_LT_RDIV_EQ));
(POP_ASSUM MP_TAC);
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(POP_ASSUM (fun th ->REWRITE_TAC [th]));
(REWRITE_TAC [ARITH_RULE `&0 / (r':real) = &0`]);
(ARITH_TAC);
(SUBGOAL_THEN `~(u:real^3 = vec 0)` ASSUME_TAC);
(ASM_MESON_TAC[CHANGE_TARJJUW_31]);

(SUBGOAL_THEN `!v:real^3.(v = ((r':real)/(norm p))% (p:real^3)) ==> (r' = norm v)` ASSUME_TAC);
(GEN_TAC);
(STRIP_TAC);
(SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
(ASM_ARITH_TAC);
(MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS));
(ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
(STRIP_TAC);
(FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(v:real^3) = (r':real) / norm p % (p:real^3)`);
(ASM_MESON_TAC [CHANGE_TARJJUW_1]);
(POP_ASSUM (LABEL_TAC "F7"));
(USE_THEN "F1" (MP_TAC o SPEC `((r':real)/(norm (p:real^3)))% p`));
(REWRITE_TAC [dist;NORM_SUB;VECTOR_SUB_RZERO]);
(ABBREV_TAC `v = (r':real) / norm p % (p:real^3)`);
(ASM_REWRITE_TAC[]);
(REMOVE_THEN "F7" (MP_TAC o SPEC `v:real^3`));
(REWRITE_TAC[]);
(STRIP_TAC);
(SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
(ASM_ARITH_TAC);
(POP_ASSUM MP_TAC);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(ASM_REWRITE_TAC[ARITH_RULE `norm (v:real^3) <= norm v`]);
(STRIP_TAC);
(POP_ASSUM MP_TAC);
(REWRITE_TAC [GSYM dist]);
(STRIP_TAC);
(REMOVE_THEN "F3" (MP_TAC o SPECL [`p:real^3`;`u':real^3`]));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
(ASM_REWRITE_TAC[]);
(UNDISCH_TAC `(r':real) = norm (v:real^3)`);
(STRIP_TAC);
(POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]));
(STRIP_TAC);
(POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u':real^3) * (r':real)) / &2`));
(REWRITE_TAC [IN_ELIM_THM]);
(SUBGOAL_THEN `(?(u:real^3). u IN (V:real^3->bool) /\ ((g:real^3->real)(u':real^3) * (r':real)) / &2 = (g u * r') / &2)` ASSUME_TAC);
(EXISTS_TAC `u':real^3`);
(ASM_REWRITE_TAC[]);
(POP_ASSUM (fun th -> REWRITE_TAC[th]));
(STRIP_TAC);
(MP_TAC (ISPECL [`((g:real^3->real)(u':real^3) * (r':real)) / &2`;`sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`;`norm (p:real^3)`]REAL_LET_TRANS));
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
(UNDISCH_TAC `(r':real) / norm (p:real^3) % p = v:real^3`);
(REWRITE_TAC [EQ_SYM_EQ]);
(STRIP_TAC);
(SUBGOAL_THEN `norm (p:real^3) < norm p` ASSUME_TAC);
(ASM_MESON_TAC[CHANGE_TARJJUW_5]);
(UNDISCH_TAC `(P:real^3->bool) = INTERS {{x:real^3 | u dot x <= (g:real^3->real)(u:real^3)} | u IN (V:real^3->bool)}`);
(STRIP_TAC);
(POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
(ASM_ARITH_TAC);
]);;

let TARJJUW = 
prove( `!(V:real^3 -> bool)(P:real^3->bool) (g:real^3->real) r r':real. (&2 <= r) /\ (r <= r') /\  (V SUBSET (:real^3) DIFF ball (vec 0,&2)) /\ (FINITE V) /\ packing V /\ ~(V = {}) /\ (weakly_saturated V r r') /\
 P = INTERS {half_spaces u (g u)| u IN V} ==>
(bounded P)`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC (ISPECL [`V:real^3->bool`]MEMBER_NOT_EMPTY)
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN FIRST_ASSUM (fun th -> REWRITE_TAC [th])
THEN STRIP_TAC
THEN STRIP_TAC
THEN DISCH_THEN (X_CHOOSE_TAC `u:real^3`)
THEN MP_TAC (ISPECL [`(V:real^3 -> bool)`;`(P:real^3->bool)`;`(g:real^3->real)`;` r:real`;`r':real`] CHANGE_TARJJUW_9)
THEN ASM_REWRITE_TAC[]
THEN FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th])
THEN POP_ASSUM MP_TAC
THEN FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th])
THEN REPEAT STRIP_TAC
THEN MP_TAC (ISPECL [`V:real^3 -> bool`;`P:real^3->bool`;`g:real^3 -> real`;`r:real`;`r':real`;`u:real^3`]CHANGE_TARJJUW_10)
THEN ASM_REWRITE_TAC[]);;

end;;