text_formalization/packing/TARJJUW.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Lemma: TARJJUW                                                             *)
   4 (* Chapter: packing                                                           *)
   5 (* Author: Dang Tat Dat                                                       *)
   6 (* Date: 2010-02-13                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* edits by thales:
  10     wrapped in a module.
  11    Moved into the project on August 2, 2010.
  12 *)
  13
  14 module Tarjjuw  = struct
  15
  16 (*
  17 needs "/home/nyx/flyspeck/working/flyspeck_needs.hl";;
  18
  19 flyspeck_needs "general/prove_by_refinement.hl";;
  20 flyspeck_needs "general/sphere.hl";;
  21 *)
  22 open Sphere;;
  23 open Prove_by_refinement;;
  24 (*-----------Definition------------------------------------------------------*)
  25 let weakly_saturated =
  26     new_definition
  27      `weakly_saturated (V:real^3 ->bool) (r:real) (r':real) <=>
  28         (!(v:real^3).(&2 <= dist(vec 0,v) ) /\ (dist(vec 0, v) <= r') ==>
  29             (?(u:real^3). (u IN V) /\ (~((vec 0) = u)) /\ (dist(u,v) < r)))`;;
  30
  31 let half_spaces =
  32     new_definition
  33     `half_spaces (a:real^3) (b:real) =
  34      {x:real^3| (a dot x) <= b}`;;
  35
  36 (*----------------------------------------------------------------------------*)
  37 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
  38 SUBGOAL_THEN `norm (v:real^3) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL
  39 [REWRITE_TAC [] THEN
  40 ASM_MESON_TAC [];SUBGOAL_THEN `&0 < norm (p:real^3)` ASSUME_TAC THENL
  41 [REWRITE_TAC[] THEN
  42 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]]]]]]]]);;
  43
  44 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
  45 [ASM_MESON_TAC [CHANGE_TARJJUW_1];
  46 SUBGOAL_THEN `norm (v:real^3) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL
  47 [ASM_MESON_TAC[];
  48 SUBGOAL_THEN `(r':real) = norm (((r':real)/(norm (p:real^3)))%p)` ASSUME_TAC THENL
  49 [ASM_ARITH_TAC;ASM_MESON_TAC [EQ_SYM_EQ]]]]);;
  50
  51 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
  52 SUBGOAL_THEN `&0 < norm (p:real^3)` ASSUME_TAC THENL
  53 [REWRITE_TAC[] THEN
  54 ASM_REWRITE_TAC [NORM_POS_LT];
  55 SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))%p) = (abs (r'/norm p))*(norm p)` ASSUME_TAC THENL
  56 [REWRITE_TAC[] THEN
  57 REWRITE_TAC [NORM_MUL];
  58 SUBGOAL_THEN `&0 < ((r':real)/(norm (p:real^3)))` ASSUME_TAC THENL
  59 [REWRITE_TAC[] THEN
  60 ASM_MESON_TAC [REAL_LT_DIV];
  61 SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) = r'/(norm p)` ASSUME_TAC THENL
  62 [REWRITE_TAC[] THEN
  63 ASM_REWRITE_TAC [REAL_ABS_REFL] THEN ASM_ARITH_TAC;
  64 SUBGOAL_THEN `abs ((r':real) / norm (p:real^3)) * norm p = ((r':real) / norm (p:real^3)) * norm p` ASSUME_TAC THENL
  65 [ASM_ARITH_TAC;
  66 SUBGOAL_THEN `~(norm (p:real^3) = &0)` ASSUME_TAC THENL
  67 [ASM_ARITH_TAC;
  68 SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))%p) =  ((r':real) / norm (p:real^3)) * norm p` ASSUME_TAC THENL
  69 [REWRITE_TAC[] THEN ASM_ARITH_TAC;
  70 ASM_MESON_TAC [REAL_DIV_RMUL]]]]]]]]);;
  71
  72 (*-------------------------------------------------------------------*)
  73 let CHANGE_TARJJUW_2 = prove (`!(v:real^3) (r':real) (p:real^3).(~(p = vec 0)) /\ (v = (r'/(norm p))% p) ==>
  74 (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[]]]]]]);;
  75
  76 (*-------------------------------------------------------------------*)
  77
  78 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`,
  79 [
  80  (REPEAT GEN_TAC THEN REWRITE_TAC [ball; DIFF;SUBSET]);
  81  (STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC));
  82  (DISCH_TAC);
  83  (DISCH_THEN (LABEL_TAC "F1"));
  84  (REWRITE_TAC [IN] THEN REPEAT STRIP_TAC);
  85  (REMOVE_THEN "F1" (MP_TAC o SPEC `u:real^3`));
  86  (ASM_REWRITE_TAC [IN;IN_ELIM_THM]);
  87  (STRIP_TAC);
  88  (POP_ASSUM MP_TAC);
  89  (REWRITE_TAC [DIST_0]);
  90  (ARITH_TAC);
  91
  92 ]);;
  93
  94
  95
  96 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)`,
  97 [
  98  (REPEAT GEN_TAC);
  99  (STRIP_TAC);
 100  (SUBGOAL_THEN `&2 <= norm (u:real^3)` ASSUME_TAC);
 101  (ASM_MESON_TAC [CHANGE_TARJJUW_3]);
 102  (MP_TAC (ISPECL [`&0`;`&2`;`norm (u:real^3)`]REAL_LTE_TRANS));
 103  (ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
 104  (REWRITE_TAC[NORM_POS_LT]);
 105
 106 ]);;
 107
 108
 109 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`,
 110 [
 111  (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);
 112  (ASM_CASES_TAC `&2 <= norm (u:real^3)` THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN REWRITE_TAC [GSYM DIST_0]]);
 113  (STRIP_TAC THEN REMOVE_THEN "F1" (MP_TAC o SPECL [`(vec 0):real^3`;`u:real^3`]));
 114  (ASM_REWRITE_TAC[]);
 115
 116 ]);;
 117 (*------------------------------------------------------------------------*)
 118
 119 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]]]]]]);;
 120
 121 (*-------------------------------------------------------------------------*)
 122
 123 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)`,
 124 REPEAT GEN_TAC
 125 THEN STRIP_TAC
 126 THEN MP_TAC (ISPECL [`v:real^3`;`r':real`]CHANGE_TARJJUW_1)
 127 THEN DISCH_THEN (MP_TAC o SPEC `p:real^3`)
 128 THEN MP_TAC (ISPECL [`&2`;`r:real`;`r':real`]REAL_LE_TRANS)
 129 THEN ASM_REWRITE_TAC[]
 130 THEN STRIP_TAC
 131 THEN MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS)
 132 THEN ASM_REWRITE_TAC[ARITH_RULE `&0 < &2`]
 133 THEN STRIP_TAC
 134 THEN ASM_REWRITE_TAC[]
 135 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(v:real^3) = (r':real) / norm p % (p:real^3)`
 136 THEN STRIP_TAC
 137 THEN MP_TAC (ISPECL [`v:real^3`]NORM_POS_LE)
 138 THEN STRIP_TAC
 139 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)
 140 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `((u:real^3) dot (p:real^3)) <= ((g:real^3->real)(u:real^3))`
 141 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= norm (v:real^3)`
 142 THEN STRIP_TAC
 143 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))
 144 THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
 145 THEN STRIP_TAC
 146 (*Sub 1*)
 147 THEN SUBGOAL_THEN `((u dot p) * norm (v:real^3)) / &2 <= (((g:real^3->real)(u:real^3)) * norm v) / &2` ASSUME_TAC
 148 THENL [ASM_ARITH_TAC;MP_TAC (ISPECL [`((u:real^3) dot (p:real^3))`;`(r':real)`]REAL_MUL_SYM)
 149 THEN STRIP_TAC
 150 THEN MP_TAC (ISPECL [`r':real`;`u:real^3`;`p:real^3`]DOT_RMUL)
 151 THEN STRIP_TAC
 152 THEN MP_TAC (ISPECL [`v:real^3`;`r':real`;`p:real^3`]CHANGE_TARJJUW_2)
 153 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `~(p:real^3 = vec 0)`
 154 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `v:real^3 = (r':real) / norm p % (p:real^3)`
 155 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `v:real^3 = (r':real) / norm p % (p:real^3)`
 156 THEN STRIP_TAC
 157 THEN
 158 (*Sub 1.1 ]]*)
 159 SUBGOAL_THEN `(u:real^3) dot ((r':real)% (p:real^3)) = u dot ((norm p)%v)` ASSUME_TAC
 160 THENL [ASM_MESON_TAC[];MP_TAC (ISPECL [`(norm (p:real^3))`;`(u:real^3)`;`(v:real^3)`]DOT_RMUL)
 161 THEN STRIP_TAC (*]]);;*)
 162 (*Sub 1.1.1]]]*)
 163 THEN SUBGOAL_THEN `((u:real^3) dot (p:real^3)) * (r':real) = norm p * (u dot (v:real^3))` ASSUME_TAC
 164 THENL [FIND_ASSUM (fun th -> REWRITE_TAC [th]) `((u:real^3) dot (p:real^3)) * (r':real) = r' * (u dot p)`
 165 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(u:real^3) dot (r':real) % (p:real^3)= r' * (u dot p)`
 166 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(u:real^3) dot (r':real) % (p:real^3)= r' * (u dot p)`
 167 THEN POP_ASSUM MP_TAC
 168 THEN POP_ASSUM MP_TAC
 169 THEN MESON_TAC[EQ_TRANS];
 170 MP_TAC (ISPECL [`(u:real^3)`;`(v:real^3)`]DOT_NORM_NEG)
 171 THEN STRIP_TAC (*]]]);;*)
 172 (*Sub 1.1.1.1 ]]]]*)
 173 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
 174 THENL [POP_ASSUM MP_TAC
 175 THEN MESON_TAC[];
 176 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM dist] THEN STRIP_TAC
 177 THEN MP_TAC (ISPECL [`V:real^3->bool`;`u:real^3`]CHANGE_TARJJUW_3)
 178 THEN ASM_REWRITE_TAC[]
 179 THEN STRIP_TAC
 180 THEN MP_TAC (ISPECL [`&2`]REAL_ABS_REFL)
 181 THEN REWRITE_TAC [ARITH_RULE `&0 <= &2`]
 182 THEN STRIP_TAC
 183 THEN MP_TAC (ISPECL [`u:real^3`]REAL_ABS_NORM) THEN STRIP_TAC (*]]]]);;*)
 184 THEN
 185 (*Sub 1.1.1.1.1 ]]]]]*)
 186 SUBGOAL_THEN `abs (&2) <= abs (norm (u:real^3))` ASSUME_TAC
 187 THENL [ASM_ARITH_TAC;
 188 MP_TAC (ISPECL [`&2`;`norm (u:real^3)`]REAL_LE_SQUARE_ABS)
 189 THEN POP_ASSUM (fun th -> REWRITE_TAC [th])
 190 THEN REWRITE_TAC [ARITH_RULE `&2 pow 2 = &4`]
 191 THEN STRIP_TAC
 192 THEN MP_TAC (ISPECL [`u:real^3`;`v:real^3`;`r:real`]CHANGE_TARJJUW_4)
 193 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `dist (u:real^3,v:real^3) < r:real`
 194 THEN STRIP_TAC
 195 THEN MP_TAC (ISPECL [`((r:real) pow 2)`;`dist (u:real^3,v:real^3) pow 2`]REAL_LT_NEG)
 196 THEN FIRST_ASSUM (fun th -> REWRITE_TAC [th])
 197 THEN STRIP_TAC (*]]]]]);;*)
 198 (*Sub 1.1.1.1.1.1 ]]]]]]*)
 199 THEN SUBGOAL_THEN `(norm (v:real^3)) pow 2 = (r':real) pow 2`ASSUME_TAC
 200 THENL [UNDISCH_TAC `r':real = norm (v:real^3)`
 201 THEN MESON_TAC[];
 202 (*Sub 1.1.1.1.1.1.2*)
 203 SUBGOAL_THEN `((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) =
 204  (norm (u:real^3)) pow 2 + (r':real) pow 2` ASSUME_TAC
 205 THENL [ASM_ARITH_TAC;
 206 (*Sub 1.1.1.1.1.1.2.2*)
 207 SUBGOAL_THEN `&4 + (norm (v:real^3)) pow 2 <= ((norm (u:real^3)) pow 2 + (norm v) pow 2 )` ASSUME_TAC
 208 THENL [ASM_ARITH_TAC;
 209 (*Sub 1.1.1.1.1.1.2.2.2*)
 210 SUBGOAL_THEN `(((u:real^3) dot (p:real^3)) * (r':real)) / &2 < (norm (p))` ASSUME_TAC
 211 THENL [UNDISCH_TAC `(((u:real^3) dot (p:real^3)) * norm (v:real^3)) / &2 <= ((g:real^3->real) u * norm v) / &2`
 212 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `r':real = norm (v:real^3)`
 213 THEN UNDISCH_TAC `((g:real^3->real) (u:real^3) * (r':real)) / &2 < norm (p:real^3)`
 214 THEN ARITH_TAC;
 215 (*Sub 1.1.1.1.1.1.2.2.2.2*)
 216 SUBGOAL_THEN `((norm (p:real^3)) * ((u:real^3) dot (v:real^3))) / &2 < (norm (p))`ASSUME_TAC
 217 THENL [ASM_ARITH_TAC;
 218 (*Sub 1.1.1.1.1.1.2.2.2.2*)
 219 SUBGOAL_THEN `&4 + (r':real) pow 2 <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2 )` ASSUME_TAC
 220 THENL [ASM_ARITH_TAC;
 221 (*Sub 1.1.1.1.1.1.2.2.2.2*)
 222 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
 223 THENL [ASM_ARITH_TAC;
 224 (*Sub 1.1.1.1.1.1.2.2.2.2*)
 225 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
 226 THENL [ASM_ARITH_TAC;
 227 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
 228 THENL [ASM_ARITH_TAC;
 229 MP_TAC (ISPECL [`&0`;`&2`;`r:real`]REAL_LE_TRANS)
 230 THEN ASM_REWRITE_TAC[ARITH_RULE `&0 <= &2`]
 231 THEN STRIP_TAC
 232 THEN MP_TAC (ISPECL [`&0`;`r:real`;`r':real`]REAL_LE_TRANS)
 233 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `&0 <= r:real`
 234 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `r:real <= r':real`
 235 THEN STRIP_TAC
 236 THEN MP_TAC (ISPECL [`r':real`]REAL_ABS_REFL)
 237 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= r':real`
 238 THEN STRIP_TAC
 239 THEN MP_TAC (ISPECL [`r:real`]REAL_ABS_REFL)
 240 THEN FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `&0 <= r:real`
 241 THEN STRIP_TAC(*]]]]]]]]]]]]]]);;*)
 242
 243 THEN SUBGOAL_THEN `abs (r:real) <= abs(r':real)` ASSUME_TAC
 244 THENL [POP_ASSUM (fun th -> REWRITE_TAC[th])
 245 THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
 246 THEN ASM_REWRITE_TAC[];
 247 MP_TAC (ISPECL [`r:real`;`r':real`]REAL_LE_SQUARE_ABS)
 248 THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
 249 THEN STRIP_TAC
 250 THEN MP_TAC (ISPECL [`r':real`;`r:real`]REAL_SUB_LE)
 251 THEN UNDISCH_TAC `r:real <= r':real`
 252 THEN STRIP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
 253 THEN STRIP_TAC
 254 THEN MP_TAC (ISPECL [`(r':real) pow 2`;`(r:real) pow 2 `]REAL_SUB_LE)
 255 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(r:real) pow 2 <= (r':real) pow 2`
 256 THEN STRIP_TAC(*]]]]]]]]]]]]]]]);;*)
 257
 258 THEN SUBGOAL_THEN `&4 <= &4 + (r':real) pow 2 - (r:real) pow 2` ASSUME_TAC
 259 THENL [MP_TAC (ISPECL [`&4`;`&0`;`(r':real) pow 2 - (r:real) pow 2`]REAL_LE_LADD)
 260 THEN POP_ASSUM (fun th -> REWRITE_TAC[th])
 261 THEN REWRITE_TAC [ARITH_RULE `&4 + &0 = &4`];
 262 MP_TAC (ISPECL [`&4 + ((r':real) pow 2)`;`((r:real) pow 2)`]real_sub)
 263 THEN STRIP_TAC(*]]]]]]]]]]]]]]]]);;*)
 264
 265 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
 266 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
 267 THENL [ASM_ARITH_TAC;
 268 MP_TAC (ISPECL [`(((norm (p:real^3)) * ((u:real^3) dot (v:real^3)))/ &2)`;`(norm (p:real^3))`;`&2`]REAL_LT_RMUL)
 269 THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
 270 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(norm (p:real^3) * ((u:real^3) dot (v:real^3))) / &2 < norm p`
 271 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)))`]
 272 THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]);;*)
 273
 274
 275 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
 276 THENL [ASM_ARITH_TAC;
 277 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)
 278 THEN REWRITE_TAC [ARITH_RULE `&0 < &2`]
 279 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`
 280 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))`]
 281 THEN STRIP_TAC
 282 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)
 283 THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]]);;*)
 284
 285
 286
 287 THEN SUBGOAL_THEN `&4 <= ((norm (u:real^3)) pow 2 + (norm (v:real^3)) pow 2) - (dist (u,v) pow 2)` ASSUME_TAC
 288 THENL [ASM_ARITH_TAC;
 289 MP_TAC (ISPECL [`p:real^3`]NORM_POS_LE) THEN STRIP_TAC
 290 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)
 291 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`
 292 THEN FIND_ASSUM (fun th -> REWRITE_TAC [th]) `&0 <= norm (p:real^3)`
 293 THEN STRIP_TAC(*]]]]]]]]]]]]]]]]]]]]);; *)
 294 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)
 295 THEN POP_ASSUM (fun th -> REWRITE_TAC [th])
 296 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) <
 297   (norm p * &2) * &2`
 298 THEN ARITH_TAC]]]]]]]]]]]]]]]]]]]]);;
 299
 300
 301 (*----------------------------------------------------------------*)
 302 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') /\
 303  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))`,
 304
 305 [
 306 (REPEAT GEN_TAC );
 307 (STRIP_TAC);
 308 (REWRITE_TAC [INTERS;IN_ELIM_THM] THEN STRIP_TAC);
 309 (POP_ASSUM MP_TAC);
 310 (ASM_REWRITE_TAC[IN_ELIM_THM]);
 311 (REPEAT STRIP_TAC);
 312 (SUBGOAL_THEN `INTERS {half_spaces u (g u) | u IN V} SUBSET half_spaces (u:real^3) ((g:real^3->real) u)` ASSUME_TAC);
 313 (REWRITE_TAC [SUBSET;IN_INTERS]);
 314 (GEN_TAC);
 315 (DISCH_THEN (LABEL_TAC "F1"));
 316 (REMOVE_THEN "F1" (MP_TAC o SPEC `half_spaces (u:real^3) ((g:real^3 -> real) u)`));
 317 (STRIP_TAC);
 318 (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);
 319 (REWRITE_TAC [half_spaces]);
 320 (REWRITE_TAC [IN_ELIM_THM]);
 321 (EXISTS_TAC `u:real^3`);
 322 (ASM_REWRITE_TAC[]);
 323 (POP_ASSUM MP_TAC);
 324 (ASM_REWRITE_TAC[]);
 325 (POP_ASSUM MP_TAC);
 326 (REWRITE_TAC [SUBSET]);
 327 (DISCH_THEN (MP_TAC o SPEC `p:real^3`));
 328 (ASM_REWRITE_TAC[]);
 329
 330 ]);;
 331
 332
 333 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') /\
 334  P = INTERS {half_spaces u (g u)| u IN V} /\ u IN V   ==> (!p:real^3. p IN P ==> (u dot p) <= (g u))`,
 335 [
 336 (REPEAT GEN_TAC THEN STRIP_TAC);
 337 (GEN_TAC);
 338 (STRIP_TAC);
 339 (SUBGOAL_THEN `(!u:real^3. u IN (V:real^3->bool) ==> p IN half_spaces u ((g:real^3->real) u))` ASSUME_TAC);
 340 (ASM_MESON_TAC[CHANGE_TARJJUW_6]);
 341 (POP_ASSUM MP_TAC);
 342 (REWRITE_TAC [half_spaces;IN_ELIM_THM]);
 343 (DISCH_THEN (MP_TAC o SPEC `u:real^3`));
 344 (ASM_REWRITE_TAC[]);
 345
 346 ]);;
 347
 348
 349 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') /\
 350  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))`,
 351 [
 352 (REPEAT GEN_TAC);
 353 (STRIP_TAC);
 354 (REPEAT GEN_TAC);
 355 (STRIP_TAC);
 356 (SUBGOAL_THEN `!p:real^3. p IN (P:real^3->bool) ==> (u dot p) <= ((g:real^3->real)(u:real^3))` ASSUME_TAC);
 357 (ASM_MESON_TAC [CHANGE_TARJJUW_7]);
 358 (POP_ASSUM (MP_TAC o SPEC `p:real^3`));
 359 (ASM_REWRITE_TAC[]);
 360 ]);;
 361
 362
 363 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`,
 364
 365 [
 366  (REPEAT GEN_TAC THEN STRIP_TAC);
 367  (SUBGOAL_THEN `&2 <= (r':real)` ASSUME_TAC);
 368  (ASM_ARITH_TAC);
 369  (SUBGOAL_THEN `&0 <= (r':real)` ASSUME_TAC);
 370  (POP_ASSUM MP_TAC);
 371  (MP_TAC (ARITH_RULE `&0 <= &2`));
 372  (MESON_TAC[REAL_LE_TRANS]);
 373  (MP_TAC (ISPECL [`(g:real^3->real) (u:real^3)`;`r':real`]REAL_LE_MUL));
 374  (ASM_REWRITE_TAC[]);
 375 (STRIP_TAC);
 376  (MP_TAC (ISPECL [`(((g:real^3->real) (u:real^3)) * (r':real))`;`(&2)`]REAL_LE_DIV));
 377  (ASM_REWRITE_TAC[ARITH_RULE `&0 <= &2`]);
 378 ]);;
 379
 380
 381 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} = {})`,
 382 [
 383  (REPEAT GEN_TAC);
 384  (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);
 385  (REWRITE_TAC [IMAGE;EXTENSION]);
 386  (GEN_TAC);
 387  (EQ_TAC);
 388  (REWRITE_TAC [IN_ELIM_THM]);
 389  (REWRITE_TAC [IN_ELIM_THM]);
 390  (REPEAT STRIP_TAC);
 391  (MP_TAC (ISPECL [`\u. (((g:real^3->real)(u:real^3)) * (r':real)) / (&2)`;`V:real^3->bool`]FINITE_IMAGE));
 392  (ASM_REWRITE_TAC[]);
 393  (MP_TAC (ISPECL [`\u. (((g:real^3->real)(u:real^3)) * (r':real)) / (&2)`;`V:real^3->bool`]IMAGE_EQ_EMPTY));
 394  (ASM_REWRITE_TAC[]);
 395
 396 ]);;
 397
 398
 399 (*----------------------------------------------------------------------------*)
 400 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') /\
 401  P = INTERS {half_spaces u (g u)| u IN V} ==> polyhedron P`,
 402 [
 403 (REPEAT GEN_TAC);
 404 (STRIP_TAC);
 405 (ASM_REWRITE_TAC [polyhedron]);
 406 (EXISTS_TAC `{half_spaces (u:real^3) ((g:real^3->real) u)| u IN (V:real^3->bool)}`);
 407 (REWRITE_TAC[]);
 408 (STRIP_TAC);
 409 (MP_TAC (ISPECL [`\u. half_spaces (u:real^3) ((g:real^3->real) u) `;`V:real^3->bool`]FINITE_IMAGE));
 410 (ASM_REWRITE_TAC[]);
 411 (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);
 412 (REWRITE_TAC [IMAGE;EXTENSION]);
 413 (STRIP_TAC);
 414 (REWRITE_TAC [IN_ELIM_THM]);
 415 (EQ_TAC);
 416 (STRIP_TAC);
 417 (EXISTS_TAC `x':real^3`);
 418 (ASM_REWRITE_TAC[]);
 419 (REWRITE_TAC [EXTENSION]);
 420 (STRIP_TAC);
 421 (POP_ASSUM (MP_TAC o SPEC `x'':real^3`));
 422 (ARITH_TAC);
 423 (STRIP_TAC);
 424 (EXISTS_TAC `u:real^3`);
 425 (ASM_REWRITE_TAC []);
 426 (ASM_REWRITE_TAC[]);
 427 (ASM_REWRITE_TAC[half_spaces;IN_ELIM_THM]);
 428 (GEN_TAC THEN STRIP_TAC);
 429 (EXISTS_TAC `u:real^3`);
 430 (EXISTS_TAC `((g:real^3->real)(u:real^3))`);
 431 (MP_TAC (ISPECL [`V:real^3->bool`;`u:real^3`]CHANGE_TARJJUW_31));
 432 (ASM_REWRITE_TAC[]);
 433
 434 ]);;
 435
 436 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') /\
 437  P = INTERS {half_spaces u (g u)| u IN V} /\ polyhedron P /\ u IN V ==>
 438 (bounded P)`,
 439 [
 440 (REPEAT GEN_TAC);
 441 (STRIP_TAC);
 442 (SUBGOAL_THEN `!p:real^3 u:real^3. p IN P /\ u IN V ==> (u dot p) <= ((g:real^3->real) u)` ASSUME_TAC);
 443 (ASM_MESON_TAC[CHANGE_TARJJUW_71]);
 444 (REPEAT (POP_ASSUM MP_TAC));
 445 (REWRITE_TAC [weakly_saturated;polyhedron;half_spaces] THEN STRIP_TAC);
 446 (DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC);
 447 (STRIP_TAC);
 448 (DISCH_THEN (LABEL_TAC "F1"));
 449 (DISCH_TAC);
 450 (DISCH_THEN (LABEL_TAC "F2"));
 451 (DISCH_TAC);
 452 (DISCH_THEN (LABEL_TAC "F3"));
 453 (*
 454 (ASM_CASES_TAC `(V:real^3->bool) = {}`);
 455 (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);
 456 (REWRITE_TAC[IMAGE;EXTENSION]);
 457 (GEN_TAC);
 458 (EQ_TAC);
 459 (REWRITE_TAC [IN_ELIM_THM]);
 460 (STRIP_TAC);
 461 (EXISTS_TAC `x':real^3`);
 462 (ASM_REWRITE_TAC[]);
 463 (POP_ASSUM (LABEL_TAC "B1"));
 464 (REWRITE_TAC [EXTENSION]);
 465 (STRIP_TAC);
 466 (REWRITE_TAC[IN_ELIM_THM]);
 467 (REMOVE_THEN "B1" (MP_TAC o SPEC `x'':real^3`));
 468 (ASM_REWRITE_TAC[]);
 469 (REWRITE_TAC [IN_ELIM_THM]);
 470 (STRIP_TAC);
 471 (EXISTS_TAC `u':real^3`);
 472 (ASM_REWRITE_TAC[]);
 473 (STRIP_TAC);
 474 (REWRITE_TAC [IN_ELIM_THM]);
 475 (MP_TAC (ISPECL [`(\(u:real^3). {x:real^3 | u dot x <= g u})`;`V:real^3->bool`]IMAGE_EQ_EMPTY));
 476 (FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(V:real^3->bool) = {}`);
 477 (POP_ASSUM MP_TAC);
 478 (ASM_REWRITE_TAC[]);
 479 (DISCH_TAC);
 480 (POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
 481 (DISCH_TAC);
 482 ( POP_ASSUM (fun th -> REWRITE_TAC [th]));
 483 (REWRITE_TAC [INTERS_0]);
 484 *)
 485
 486 (MP_TAC (ISPECL [`V:real^3->bool`;`(g:real^3->real)`;`r':real`]FININTE_GFUN));
 487 (FIND_ASSUM (fun th -> REWRITE_TAC [th]) `~ ((V:real^3->bool) = {})`);
 488 (FIND_ASSUM (fun th -> REWRITE_TAC [th]) `FINITE (V:real^3->bool) `);
 489 (STRIP_TAC);
 490 (ASM_CASES_TAC `bounded (P:real^3->bool)`);
 491 (ASM_REWRITE_TAC[]);
 492 (POP_ASSUM MP_TAC);
 493 (REWRITE_TAC [bounded]);
 494 (REWRITE_TAC [NOT_EXISTS_THM;NOT_FORALL_THM]);
 495 (REWRITE_TAC [NOT_IMP;REAL_NOT_LE]);
 496 (DISCH_THEN (LABEL_TAC "F4"));
 497 (REWRITE_TAC [GSYM bounded]);
 498 (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);
 499 (REPEAT STRIP_TAC);
 500 (REMOVE_THEN "F4" (MP_TAC o SPEC `sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`));
 501 (DISCH_THEN (X_CHOOSE_TAC `p:real^3`));
 502 (POP_ASSUM MP_TAC THEN STRIP_TAC);
 503 (EXISTS_TAC `p:real^3`);
 504 (ASM_REWRITE_TAC[]);
 505 (MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
 506 (ASM_REWRITE_TAC[]);
 507 (STRIP_TAC);
 508 (POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u':real^3) * (r':real)) / &2 `));
 509 (REWRITE_TAC [IN_ELIM_THM]);
 510 (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);
 511 (EXISTS_TAC `u':real^3`);
 512 (ASM_REWRITE_TAC[]);
 513 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 514 (STRIP_TAC);
 515 (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));
 516 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 517 (POP_ASSUM MP_TAC);
 518 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 519 (POP_ASSUM (LABEL_TAC "F5"));
 520 (REMOVE_THEN "F4" (MP_TAC o SPEC `sup {((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`));
 521 (DISCH_THEN (X_CHOOSE_TAC `p:real^3`));
 522 (POP_ASSUM MP_TAC THEN STRIP_TAC);
 523 (REMOVE_THEN "F5" (MP_TAC o SPEC `u:real^3`));
 524 (FIND_ASSUM (fun th ->REWRITE_TAC [th]) `(u:real^3) IN (V:real^3 -> bool)`);
 525 (STRIP_TAC);
 526 (USE_THEN "F3" (MP_TAC o SPECL [`p:real^3`;`u:real^3`]));
 527 (FIND_ASSUM (fun th -> REWRITE_TAC [th])`(p:real^3) IN (P:real^3->bool)`);
 528 (FIND_ASSUM (fun th -> REWRITE_TAC [th])`(u:real^3) IN (V:real^3->bool)`);
 529 (DISCH_TAC);
 530 (MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
 531 (ASM_REWRITE_TAC[]);
 532 (STRIP_TAC);
 533 (POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u:real^3) * (r':real)) / &2`));
 534 (REWRITE_TAC [IN_ELIM_THM]);
 535 (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);
 536 (EXISTS_TAC `u:real^3`);
 537 (ASM_REWRITE_TAC[]);
 538 (POP_ASSUM (fun th -> REWRITE_TAC[th]));
 539 (STRIP_TAC);
 540 (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));
 541 (ASM_REWRITE_TAC[]);
 542 (STRIP_TAC);
 543 (ASM_CASES_TAC `(p:real^3) = vec 0`);
 544 (SUBGOAL_THEN `((r':real)/(norm (p:real^3)))% p = vec 0` ASSUME_TAC);
 545 (POP_ASSUM (fun th -> REWRITE_TAC [th]));
 546 (MESON_TAC [VECTOR_MUL_RZERO]);
 547 (SUBGOAL_THEN `norm (((r':real)/(norm (p:real^3)))% p) = &0` ASSUME_TAC );
 548 (ASM_REWRITE_TAC[]);
 549 (REWRITE_TAC [NORM_EQ_0]);
 550 (MP_TAC (ISPECL [`p:real^3`]NORM_EQ_0));
 551 (ASM_REWRITE_TAC[]);
 552 (STRIP_TAC);
 553 (UNDISCH_TAC `((g:real^3->real)(u:real^3) * (r':real)) / (&2) < norm (p:real^3)`);
 554 (ASM_REWRITE_TAC[]);
 555 (STRIP_TAC);
 556 (USE_THEN "F3" (MP_TAC o SPECL [`(vec 0):real^3`;`u:real^3`]));
 557 (UNDISCH_TAC `(p:real^3) IN (P:real^3->bool)`);
 558 (UNDISCH_TAC `p:real^3 = vec 0`);
 559 (DISCH_TAC THEN POP_ASSUM (fun th ->REWRITE_TAC [th]));
 560 (DISCH_TAC THEN POP_ASSUM (fun th ->REWRITE_TAC [th]));
 561 (FIND_ASSUM (fun th -> REWRITE_TAC [th]) `(u:real^3) IN (V:real^3->bool)`);
 562 (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)}`);
 563 (DISCH_TAC);
 564 (POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
 565 (REWRITE_TAC [DOT_RZERO]);
 566 (SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
 567 (ASM_ARITH_TAC);
 568 (MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS));
 569 (ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
 570 (STRIP_TAC);
 571 (MP_TAC (ARITH_RULE `(((g:real^3->real))(u:real^3) * (r':real)) / &2 < &0 <=> g u * r' < &0`));
 572 (POP_ASSUM MP_TAC);
 573 (POP_ASSUM MP_TAC);
 574 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 575 (REPEAT STRIP_TAC);
 576 (MP_TAC (ISPECL [`((g:real^3->real))(u:real^3)`;`&0`;`r':real`]REAL_LT_RDIV_EQ));
 577 (POP_ASSUM MP_TAC);
 578 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 579 (POP_ASSUM (fun th ->REWRITE_TAC [th]));
 580 (REWRITE_TAC [ARITH_RULE `&0 / (r':real) = &0`]);
 581 (ARITH_TAC);
 582 (SUBGOAL_THEN `~(u:real^3 = vec 0)` ASSUME_TAC);
 583 (ASM_MESON_TAC[CHANGE_TARJJUW_31]);
 584
 585 (SUBGOAL_THEN `!v:real^3.(v = ((r':real)/(norm p))% (p:real^3)) ==> (r' = norm v)` ASSUME_TAC);
 586 (GEN_TAC);
 587 (STRIP_TAC);
 588 (SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
 589 (ASM_ARITH_TAC);
 590 (MP_TAC (ISPECL [`&0`;`&2`;`r':real`]REAL_LTE_TRANS));
 591 (ASM_REWRITE_TAC [ARITH_RULE `&0 < &2`]);
 592 (STRIP_TAC);
 593 (FIND_ASSUM (fun th -> REWRITE_TAC [GSYM th]) `(v:real^3) = (r':real) / norm p % (p:real^3)`);
 594 (ASM_MESON_TAC [CHANGE_TARJJUW_1]);
 595 (POP_ASSUM (LABEL_TAC "F7"));
 596 (USE_THEN "F1" (MP_TAC o SPEC `((r':real)/(norm (p:real^3)))% p`));
 597 (REWRITE_TAC [dist;NORM_SUB;VECTOR_SUB_RZERO]);
 598 (ABBREV_TAC `v = (r':real) / norm p % (p:real^3)`);
 599 (ASM_REWRITE_TAC[]);
 600 (REMOVE_THEN "F7" (MP_TAC o SPEC `v:real^3`));
 601 (REWRITE_TAC[]);
 602 (STRIP_TAC);
 603 (SUBGOAL_THEN `&2 <= r':real` ASSUME_TAC);
 604 (ASM_ARITH_TAC);
 605 (POP_ASSUM MP_TAC);
 606 (ASM_REWRITE_TAC[]);
 607 (STRIP_TAC);
 608 (ASM_REWRITE_TAC[ARITH_RULE `norm (v:real^3) <= norm v`]);
 609 (STRIP_TAC);
 610 (POP_ASSUM MP_TAC);
 611 (REWRITE_TAC [GSYM dist]);
 612 (STRIP_TAC);
 613 (REMOVE_THEN "F3" (MP_TAC o SPECL [`p:real^3`;`u':real^3`]));
 614 (ASM_REWRITE_TAC[]);
 615 (STRIP_TAC);
 616 (MP_TAC (ISPECL [`{((g:real^3->real)(u:real^3) * (r':real)) / &2 | u IN (V:real^3->bool)}`]SUP_FINITE));
 617 (ASM_REWRITE_TAC[]);
 618 (UNDISCH_TAC `(r':real) = norm (v:real^3)`);
 619 (STRIP_TAC);
 620 (POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]));
 621 (STRIP_TAC);
 622 (POP_ASSUM (MP_TAC o SPEC `((g:real^3->real)(u':real^3) * (r':real)) / &2`));
 623 (REWRITE_TAC [IN_ELIM_THM]);
 624 (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);
 625 (EXISTS_TAC `u':real^3`);
 626 (ASM_REWRITE_TAC[]);
 627 (POP_ASSUM (fun th -> REWRITE_TAC[th]));
 628 (STRIP_TAC);
 629 (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));
 630 (ASM_REWRITE_TAC[]);
 631 (STRIP_TAC);
 632 (UNDISCH_TAC `(r':real) / norm (p:real^3) % p = v:real^3`);
 633 (REWRITE_TAC [EQ_SYM_EQ]);
 634 (STRIP_TAC);
 635 (SUBGOAL_THEN `norm (p:real^3) < norm p` ASSUME_TAC);
 636 (ASM_MESON_TAC[CHANGE_TARJJUW_5]);
 637 (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)}`);
 638 (STRIP_TAC);
 639 (POP_ASSUM (fun th -> REWRITE_TAC [GSYM th]));
 640 (ASM_ARITH_TAC);
 641 ]);;
 642
 643
 644 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') /\
 645  P = INTERS {half_spaces u (g u)| u IN V} ==>
 646 (bounded P)`,
 647 REPEAT GEN_TAC
 648 THEN STRIP_TAC
 649 THEN MP_TAC (ISPECL [`V:real^3->bool`]MEMBER_NOT_EMPTY)
 650 THEN POP_ASSUM MP_TAC
 651 THEN POP_ASSUM MP_TAC
 652 THEN FIRST_ASSUM (fun th -> REWRITE_TAC [th])
 653 THEN STRIP_TAC
 654 THEN STRIP_TAC
 655 THEN DISCH_THEN (X_CHOOSE_TAC `u:real^3`)
 656 THEN MP_TAC (ISPECL [`(V:real^3 -> bool)`;`(P:real^3->bool)`;`(g:real^3->real)`;` r:real`;`r':real`] CHANGE_TARJJUW_9)
 657 THEN ASM_REWRITE_TAC[]
 658 THEN FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th])
 659 THEN POP_ASSUM MP_TAC
 660 THEN FIRST_ASSUM (fun th -> REWRITE_TAC [GSYM th])
 661 THEN REPEAT STRIP_TAC
 662 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)
 663 THEN ASM_REWRITE_TAC[]);;
 664
 665
 666 end;;