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