legacy/oldpacking/packing/development/Backup/KIZHLTL.hl

   1
   2
   3 g KIZHLTL1_concl;;
   4 e (GEN_TAC);;
   5 e (ASM_CASES_TAC `saturated V /\ packing (V:real^3->bool)`);;
   6 e (UP_ASM_TAC THEN STRIP_TAC);;
   7
   8
   9 e (NEW_GOAL `!r. &1 <= r
  10          ==> sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <=
  11              vol (ball (vec 0, r))`);;
  12 e (REPEAT STRIP_TAC);;
  13 e (ABBREV_TAC `S = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);;
  14 e (REWRITE_WITH `sum S vol = vol (UNIONS S)`);;
  15 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
  16 e (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS);;
  17 e (REPEAT STRIP_TAC);;
  18 e (EXPAND_TAC "S");;
  19 e (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);;
  20 e (REWRITE_TAC[GSYM HAS_MEASURE_MEASURE]);;
  21 e (UP_ASM_TAC THEN EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);;
  22 e (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);;
  23 e (ASM_REWRITE_TAC[]);;
  24 e (MATCH_MP_TAC MEASURABLE_MCELL);;
  25 e (ASM_REWRITE_TAC[]);;
  26 e (UP_ASM_TAC THEN REWRITE_TAC[IN]);;
  27
  28 e (ASM_CASES_TAC `~NULLSET (s INTER t)`);;
  29 e (NEW_GOAL `F`);;
  30 e (UNDISCH_TAC `s:real^3->bool IN S` THEN UNDISCH_TAC `t:real^3->bool IN S`);;
  31 e (EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);;
  32 e (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);;
  33 e (NEW_GOAL `s = t:real^3->bool`);;
  34 e (REWRITE_TAC[ASSUME `t = mcell i V ul`; ASSUME `s = mcell i' V ul'`]);;
  35 e (ABBREV_TAC `j = if i <= 4 then i else 4`);;
  36 e (ABBREV_TAC `j' = if i' <= 4 then i' else 4`);;
  37 e (REWRITE_WITH `mcell i V ul = mcell j V ul`);;
  38 e (EXPAND_TAC "j" THEN COND_CASES_TAC);;
  39 e (REFL_TAC);;
  40 e (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  41    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);;
  42 e (REWRITE_WITH `mcell i' V ul' = mcell j' V ul'`);;
  43 e (EXPAND_TAC "j'" THEN COND_CASES_TAC);;
  44 e (REFL_TAC);;
  45 e (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  46    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);;
  47 e (REWRITE_WITH `j' = j /\ mcell j' V ul' = mcell j V ul`);;
  48 e (MATCH_MP_TAC Ajripqn.AJRIPQN);;
  49
  50 e (REPEAT STRIP_TAC);;
  51 e (ASM_REWRITE_TAC[]);;
  52 e (ASM_REWRITE_TAC[]);;
  53 e (ASM_MESON_TAC[IN]);;
  54 e (ASM_MESON_TAC[IN]);;
  55 e (EXPAND_TAC "j'" THEN COND_CASES_TAC);;
  56 e (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
  57    THEN SET_TAC[]);;
  58 e (SET_TAC[]);;
  59 e (EXPAND_TAC "j" THEN COND_CASES_TAC);;
  60 e (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
  61    THEN SET_TAC[]);;
  62 e (SET_TAC[]);;
  63 e (UP_ASM_TAC);;
  64 e (REWRITE_WITH `mcell j V ul = mcell i V ul`);;
  65 e (EXPAND_TAC "j" THEN COND_CASES_TAC);;
  66 e (REFL_TAC);;
  67 e (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  68    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);;
  69 e (REWRITE_WITH `mcell j' V ul' = mcell i' V ul'`);;
  70 e (EXPAND_TAC "j'" THEN COND_CASES_TAC);;
  71 e (REFL_TAC);;
  72 e (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  73    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);;
  74 e (ASM_MESON_TAC[]);;
  75 e (ASM_MESON_TAC[]);;
  76 e (ASM_MESON_TAC[]);;
  77 e (ASM_MESON_TAC[]);;
  78
  79 e (MATCH_MP_TAC MEASURE_SUBSET);;
  80 e (REWRITE_TAC[MEASURABLE_BALL]);;
  81 e (REPEAT STRIP_TAC);;
  82 e (EXPAND_TAC "S" THEN MATCH_MP_TAC MEASURABLE_UNIONS);;
  83 e (REPEAT STRIP_TAC);;
  84 e (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);;
  85 e (UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM; mcell_set]);;
  86 e (REPEAT STRIP_TAC);;
  87 e (ASM_SIMP_TAC[MEASURABLE_MCELL]);;
  88 e (EXPAND_TAC "S" THEN SET_TAC[]);;
  89
  90 (* ----------------------------------------------------------------------- *)
  91
  92 e (NEW_GOAL `?c. !r. &1 <= r
  93          ==> vol (ball (vec 0, r)) + c * r pow 2 <=
  94             sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);;
  95 e (EXISTS_TAC `-- (&24 / &3) * pi`);;
  96 e (REPEAT STRIP_TAC);;
  97
  98 e (ASM_CASES_TAC `r < &6`);;
  99 e (NEW_GOAL `&0 <= sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);;
 100 e (MATCH_MP_TAC SUM_POS_LE);;
 101 e (ASM_SIMP_TAC[Packing3.KIUMVTC]);;
 102 e (REPEAT STRIP_TAC);;
 103 e (MATCH_MP_TAC MEASURE_POS_LE);;
 104 e (ASM_SIMP_TAC[Pack1.measurable_voronoi]);;
 105
 106 e (NEW_GOAL `vol (ball ((vec 0):real^3,r)) + (--(&24 / &3) * pi) * r pow 2 <= &0`);;
 107 e (REWRITE_TAC[REAL_ARITH `a + (--b * c) * d <= &0 <=> a <= b * c * d`]);;
 108 e (ASM_SIMP_TAC [VOLUME_BALL; REAL_ARITH `&1 <= r ==> &0 <= r`]);;
 109 e (REWRITE_TAC[REAL_ARITH `&4 / &3 * pi * r pow 3 <= &24 / &3 * pi * r pow 2
 110    <=> &0 <= &4 / &3 * pi * r pow 2 * (&6 - r)`]);;
 111 e (MATCH_MP_TAC REAL_LE_MUL);;
 112 e (STRIP_TAC);;
 113 e (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);;
 114 e (MATCH_MP_TAC REAL_LE_MUL);;
 115 e (REWRITE_TAC[PI_POS_LE]);;
 116 e (MATCH_MP_TAC REAL_LE_MUL);;
 117 e (REWRITE_TAC[REAL_LE_POW_2]);;
 118 e (ASM_REAL_ARITH_TAC);;
 119 e (ASM_REAL_ARITH_TAC);;
 120
 121
 122 e (NEW_GOAL `vol (ball (vec 0,r - &2)) <=
 123    sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);;
 124 e (REWRITE_WITH
 125    `sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u)) =
 126     sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_closed V u))`);;
 127 e (MATCH_MP_TAC SUM_EQ);;
 128 e (REPEAT STRIP_TAC);;
 129 e (REWRITE_TAC[BETA_THM]);;
 130 e (REWRITE_TAC[GSYM Pack2.MEASURE_VORONOI_CLOSED_OPEN]);;
 131
 132 e (ABBREV_TAC `S:real^3->bool = V INTER ball (vec 0, r)`);;
 133 e (ABBREV_TAC `g = (\t:real^3. voronoi_closed V t)`);;
 134
 135 e (REWRITE_WITH `sum S (\u:real^3. vol (voronoi_closed V u)) = sum S (\t. vol (g t))`);;
 136 e (EXPAND_TAC "g" THEN REWRITE_TAC[]);;
 137 e (REWRITE_WITH `sum S (\t:real^3. vol (g t)) = measure (UNIONS (IMAGE g S))`);;
 138 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
 139 e (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE);;
 140 e (ASM_REWRITE_TAC[] THEN EXPAND_TAC "g");;
 141 e (REPEAT STRIP_TAC);;
 142 e (EXPAND_TAC "S");;
 143 e (ASM_SIMP_TAC[Packing3.KIUMVTC]);;
 144 e (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);;
 145 e (ASM_REWRITE_TAC[]);;
 146 e (MATCH_MP_TAC Pack2.NEGLIGIBLE_INTER_VORONOI_CLOSED);;
 147 e (ASM_SET_TAC[]);;
 148 e (EXPAND_TAC "g" THEN REWRITE_TAC[IMAGE]);;
 149 e (MATCH_MP_TAC MEASURE_SUBSET);;
 150 e (REWRITE_TAC[MEASURABLE_BALL]);;
 151 e (REPEAT STRIP_TAC);;
 152 e (MATCH_MP_TAC MEASURABLE_UNIONS);;
 153 e (STRIP_TAC);;
 154 e (MATCH_MP_TAC FINITE_IMAGE_EXPAND);;
 155 e (EXPAND_TAC "S");;
 156 e (ASM_SIMP_TAC[Packing3.KIUMVTC]);;
 157
 158 e (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);;
 159 e (ASM_REWRITE_TAC[]);;
 160 e (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);;
 161 e (ASM_REWRITE_TAC[]);;
 162 e (REWRITE_TAC[SUBSET; IN_BALL; IN_UNIONS]);;
 163 e (REPEAT STRIP_TAC);;
 164 e (MP_TAC (ASSUME `saturated (V:real^3->bool)`));;
 165 e (REWRITE_TAC[saturated] THEN STRIP_TAC);;
 166 e (NEW_GOAL `?y. y IN V /\ dist (x:real^3,y) < &2`);;
 167 e (ASM_MESON_TAC[]);;
 168 e (UP_ASM_TAC THEN STRIP_TAC);;
 169 e (NEW_GOAL `?v:real^3. v IN V /\ x IN voronoi_closed V v`);;
 170 e (MATCH_MP_TAC Packing3.TIWWFYQ);;
 171 e (ASM_REWRITE_TAC[]);;
 172 e (UP_ASM_TAC THEN STRIP_TAC);;
 173
 174 e (EXISTS_TAC `voronoi_closed V (v:real^3)`);;
 175 e (ASM_REWRITE_TAC[]);;
 176
 177 e (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);;
 178 e (EXISTS_TAC `v:real^3`);;
 179 e (STRIP_TAC);;
 180 e (EXPAND_TAC "S" THEN REWRITE_TAC[IN_INTER]);;
 181 e (ASM_REWRITE_TAC[IN_BALL]);;
 182
 183 e (NEW_GOAL `dist (vec 0,v) <= dist (vec 0,x) + dist (x, v:real^3)`);;
 184 e (REWRITE_TAC[DIST_TRIANGLE]);;
 185 e (NEW_GOAL `dist (x, v:real^3) < &2`);;
 186 e (NEW_GOAL `dist (x, v) <= dist (x, y:real^3)`);;
 187 e (UNDISCH_TAC `x:real^3 IN voronoi_closed V v`);;
 188 e (REWRITE_TAC[IN; voronoi_closed; IN_ELIM_THM]);;
 189 e (STRIP_TAC);;
 190 e (FIRST_ASSUM MATCH_MP_TAC);;
 191 e (ASM_SET_TAC[]);;
 192 e (ASM_REAL_ARITH_TAC);;
 193 e (ASM_REAL_ARITH_TAC);;
 194 e (REFL_TAC);;
 195
 196 e (NEW_GOAL `vol (ball (vec 0,r)) + (--(&24 / &3) * pi) * r pow 2 <=
 197              vol (ball (vec 0,r - &2))`);;
 198 e (ASM_SIMP_TAC[VOLUME_BALL; REAL_ARITH `~(r < &6) ==> &0 <= r`;
 199    REAL_ARITH `~(r < &6) ==> &0 <= (r - &2)` ]);;
 200 e (REWRITE_TAC[REAL_ARITH
 201  `&4 / &3 * pi * r pow 3 + (--(&24 / &3) * pi) * r pow 2 <=
 202   &4 / &3 * pi * (r - &2) pow 3 <=>
 203   &0 <= &4 / &3 * pi * (&12 * r - &8)`]);;
 204 e (MATCH_MP_TAC REAL_LE_MUL);;
 205 e (STRIP_TAC);;
 206 e (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);;
 207 e (MATCH_MP_TAC REAL_LE_MUL);;
 208 e (STRIP_TAC);;
 209 e (REWRITE_TAC[PI_POS_LE]);;
 210 e (NEW_GOAL `&12 * r >= &72`);;
 211 e (ASM_REAL_ARITH_TAC);;
 212 e (ASM_REAL_ARITH_TAC);;
 213
 214 e (ASM_REAL_ARITH_TAC);;
 215 e (UP_ASM_TAC THEN STRIP_TAC);;
 216
 217 e (EXISTS_TAC `c:real`);;
 218 e (REPEAT STRIP_TAC);;
 219
 220 e (NEW_GOAL `sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <=
 221               vol (ball (vec 0,r))`);;
 222 e (ASM_SIMP_TAC[]);;
 223 e (NEW_GOAL `vol (ball (vec 0,r)) + c * r pow 2 <=
 224             sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);;
 225 e (ASM_SIMP_TAC[]);;
 226 e (ABBREV_TAC `a1 = sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol`);;
 227 e (ABBREV_TAC `a2 = vol (ball ((vec 0):real^3,r))`);;
 228 e (ABBREV_TAC `a3 = sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);;
 229 e (ASM_REAL_ARITH_TAC);;
 230
 231 e (EXISTS_TAC `&0`);;
 232 e (REPEAT STRIP_TAC);;
 233 e (NEW_GOAL `F`);;
 234 e (ASM_MESON_TAC[]);;
 235 e (ASM_MESON_TAC[]);;
 236
 237 let KIZHLTL1 = top_thm();;
 238
 239 (* ------------------------------------------------------------------------ *)
 240 (* ======================================================================== *)
 241
 242 g KIZHLTL2_concl;;
 243 e (REPEAT STRIP_TAC);;
 244 e (ASM_CASES_TAC `saturated V /\ packing V`);;
 245 e (NEW_GOAL
 246   `?C. !r. &1 <= r ==>
 247    &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
 248    C * r pow 2`);;
 249 e (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8)
 250     = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`);;
 251 e (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);;
 252 e (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);;
 253 e (TAKE_TAC);;
 254 e (EXISTS_TAC `(&2 * mm1 / pi) * (&4 * pi) * (--C)`);;
 255 e (REPEAT STRIP_TAC);;
 256 e (NEW_GOAL `&(CARD (V INTER ball ((vec 0):real^3,r) DIFF
 257                      V INTER ball (vec 0,r - &8))) <= C * r pow 2`);;
 258 e (ASM_SIMP_TAC[]);;
 259 e (NEW_GOAL `total_solid V = (\X. total_solid V X)`);;
 260 e (REWRITE_TAC[GSYM ETA_AX]);;
 261 e (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);;
 262 e (REWRITE_TAC[total_solid]);;
 263 e (ABBREV_TAC `B = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);;
 264 e (NEW_GOAL `FINITE (B:(real^3->bool) ->bool)`);;
 265 e (EXPAND_TAC "B" THEN MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);;
 266 e (ASM_REWRITE_TAC[]);;
 267 e (ABBREV_TAC `A1:real^3->bool = V INTER ball (vec 0,r)`);;
 268 e (ABBREV_TAC `A2:real^3->bool = V INTER ball (vec 0,r - &8)`);;
 269 e (NEW_GOAL `FINITE (A1:real^3->bool)`);;
 270 e (EXPAND_TAC "A1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);;
 271 e (ASM_REWRITE_TAC[]);;
 272 e (NEW_GOAL `FINITE (A2:real^3->bool)`);;
 273 e (EXPAND_TAC "A2" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);;
 274 e (ASM_REWRITE_TAC[]);;
 275
 276 e (NEW_GOAL `sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X))
 277           <= sum B (\X. sum (VX V X) (\x. sol x X))`);;
 278 e (MATCH_MP_TAC SUM_LE);;
 279 e (ASM_REWRITE_TAC[BETA_THM]);;
 280 e (REPEAT STRIP_TAC);;
 281 e (MATCH_MP_TAC SUM_SUBSET_SIMPLE);;
 282 e (REPEAT STRIP_TAC);;
 283 e (REWRITE_TAC[VX] THEN COND_CASES_TAC);;
 284 e (REWRITE_TAC[FINITE_EMPTY]);;
 285 e (LET_TAC);;
 286 e (COND_CASES_TAC);;
 287 e (REWRITE_TAC[FINITE_EMPTY]);;
 288 e (REWRITE_TAC[FINITE_SET_OF_LIST]);;
 289 e (SET_TAC[]);;
 290 e (REWRITE_TAC[BETA_THM]);;
 291
 292 e (UNDISCH_TAC `x:real^3->bool IN B`);;
 293 e (EXPAND_TAC "B" THEN REWRITE_TAC[IN; IN_ELIM_THM; mcell_set_2]);;
 294 e (REPEAT STRIP_TAC);;
 295 e (ASM_REWRITE_TAC[]);;
 296
 297 e (NEW_GOAL `eventually_radial x' (mcell i V ul)`);;
 298 e (MATCH_MP_TAC Urrphbz2.URRPHBZ2);;
 299 e (ASM_REWRITE_TAC[]);;
 300 e (SUBGOAL_THEN `x' IN (VX V x)` MP_TAC);;
 301 e (ASM_SET_TAC[]);;
 302 e (REWRITE_TAC[VX]);;
 303 e (COND_CASES_TAC);;
 304 e (SET_TAC[]);;
 305 e (LET_TAC);;
 306 e (COND_CASES_TAC);;
 307 e (SET_TAC[]);;
 308 e (STRIP_TAC);;
 309
 310 e (UNDISCH_TAC `cell_params V x = k,ul'`);;
 311 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
 312 e (REWRITE_TAC[cell_params]);;
 313 e (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ x = mcell k V ul)`);;
 314 e (DISCH_TAC);;
 315 e (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);;
 316 e (ASM_REWRITE_TAC[]);;
 317 e (MATCH_MP_TAC SELECT_AX);;
 318 e (EXISTS_TAC `(i:num,ul:(real^3)list)`);;
 319 e (EXPAND_TAC "P");;
 320 e (REWRITE_TAC[BETA_THM]);;
 321 e (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);;
 322 e (UP_ASM_TAC THEN EXPAND_TAC "P" THEN REWRITE_TAC[BETA_THM] THEN STRIP_TAC);;
 323 e (NEW_GOAL `set_of_list (truncate_simplex (k - 1) ul') SUBSET V:real^3->bool`);;
 324 e (MATCH_MP_TAC Packing3.BARV_SUBSET);;
 325 e (EXISTS_TAC `k - 1`);;
 326 e (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);;
 327 e (EXISTS_TAC `3`);;
 328 e (STRIP_TAC);;
 329 e (ASM_SET_TAC[]);;
 330 e (ASM_ARITH_TAC);;
 331 e (ASM_SET_TAC[]);;
 332
 333
 334 e (UP_ASM_TAC THEN REWRITE_TAC[eventually_radial]);;
 335 e (REPEAT STRIP_TAC);;
 336 e (REWRITE_WITH `sol x' (mcell i V ul) =
 337   &3 * vol ((mcell i V ul) INTER normball x' r') / r' pow 3`);;
 338 e (MATCH_MP_TAC sol);;
 339 e (ASM_REWRITE_TAC[GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM; NORMBALL_BALL]);;
 340 e (MATCH_MP_TAC MEASURABLE_INTER);;
 341 e (ASM_SIMP_TAC[MEASURABLE_BALL; MEASURABLE_MCELL]);;
 342 e (MATCH_MP_TAC REAL_LE_MUL);;
 343 e (REWRITE_TAC[REAL_ARITH `&0 <= &3`] THEN MATCH_MP_TAC REAL_LE_DIV);;
 344 e (STRIP_TAC);;
 345 e (MATCH_MP_TAC MEASURE_POS_LE);;
 346 e (MATCH_MP_TAC MEASURABLE_INTER);;
 347 e (ASM_SIMP_TAC[MEASURABLE_BALL; NORMBALL_BALL; MEASURABLE_MCELL]);;
 348 e (MATCH_MP_TAC REAL_POW_LE THEN ASM_REAL_ARITH_TAC);;
 349
 350 (* ------------------------------------------------------------------------- *)
 351
 352 e (NEW_GOAL `sum B  (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X)) =
 353              sum A2 (\u. sum  {X | X IN B /\ VX V X u} (\X. sol u X))`);;
 354 e (MATCH_MP_TAC SUM_SUM_RESTRICT);;
 355 e (ASM_REWRITE_TAC[]);;
 356
 357 e (NEW_GOAL `sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X)) =
 358              sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X}
 359                     (\X. sol u X))`);;
 360 e (MATCH_MP_TAC SUM_EQ);;
 361 e (EXPAND_TAC "A2" THEN REWRITE_TAC[IN_INTER; IN_DIFF] THEN
 362    REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);;
 363 e (REWRITE_WITH `{X | B X /\ VX V X x} =
 364                  {X | mcell_set V X /\ VX V X x}`);;
 365 e (REWRITE_TAC[SET_RULE `a = b <=> a SUBSET b /\ b SUBSET a`]);;
 366 e (STRIP_TAC);;
 367 e (EXPAND_TAC "B");;
 368 e (SET_TAC[]);;
 369 e (REWRITE_WITH `!x:real^3->bool. B x <=> x IN B`);;
 370 e (REWRITE_TAC[IN]);;
 371 e (EXPAND_TAC "B" THEN REWRITE_TAC[SUBSET; IN_INTER; IN_DIFF] THEN
 372    REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM]);;
 373 e (REWRITE_TAC[MESON[] `A /\ X /\ Y ==> (B /\ A) /\ X /\ Y <=> A /\ X /\ Y ==> B`]);;
 374 e (REPEAT STRIP_TAC);;
 375 e (NEW_GOAL `x IN VX V x'`);;
 376 e (ASM_REWRITE_TAC[IN]);;
 377 e (NEW_GOAL `~NULLSET x'`);;
 378 e (UNDISCH_TAC `x IN VX V x'` THEN REWRITE_TAC[VX] THEN COND_CASES_TAC);;
 379 e (SET_TAC[]);;
 380 e (MESON_TAC[]);;
 381
 382 e (NEW_GOAL `dist (vec 0, x'':real^3) <= dist (vec 0, x) + dist (x, x'')`);;
 383 e (REWRITE_TAC[DIST_TRIANGLE]);;
 384 e (NEW_GOAL `?p. x' SUBSET ball (p:real^3,&4)`);;
 385 e (MATCH_MP_TAC MCELL_SUBSET_BALL_4);;
 386 e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);;
 387 e (UP_ASM_TAC THEN REWRITE_TAC[SUBSET; IN_BALL] THEN STRIP_TAC);;
 388 e (NEW_GOAL `dist (x, x'':real^3) <= dist (x, p) + dist (p, x'')`);;
 389 e (REWRITE_TAC[DIST_TRIANGLE]);;
 390 e (NEW_GOAL `dist (x, p:real^3) < &4`);;
 391 e (ONCE_REWRITE_TAC[DIST_SYM]);;
 392 e (FIRST_ASSUM MATCH_MP_TAC);;
 393 e (NEW_GOAL `VX V x' = V INTER x'`);;
 394 e (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);;
 395 e (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN STRIP_TAC);;
 396 e (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);;
 397 e (ASM_REWRITE_TAC[]);;
 398 e (ASM_SET_TAC[]);;
 399 e (ASM_SET_TAC[]);;
 400 e (NEW_GOAL `dist (p:real^3,x'') < &4`);;
 401 e (FIRST_ASSUM MATCH_MP_TAC);;
 402 e (ASM_REWRITE_TAC[IN]);;
 403 e (ASM_REAL_ARITH_TAC);;
 404 e (ASM_REWRITE_TAC[]);;
 405 e (ASM_REWRITE_TAC[]);;
 406
 407 (* ------------------------------------------------------------------------ *)
 408
 409 e (UP_ASM_TAC);;
 410 e (REWRITE_WITH `sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X} (\X. sol u X)) = sum A2 (\u. &4 * pi)`);;
 411 e (MATCH_MP_TAC SUM_EQ);;
 412 e (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);;
 413 e (MATCH_MP_TAC Qzyzmjc.QZYZMJC);;
 414 e (ASM_REWRITE_TAC[]);;
 415 e (ASM_SET_TAC[]);;
 416 e (ASM_SIMP_TAC[SUM_CONST]);;
 417 e (STRIP_TAC);;
 418
 419 e (ABBREV_TAC `s1 = sum B (\X. sum (VX V X) (\x. sol x X))`);;
 420 e (NEW_GOAL `&(CARD (A2:real^3->bool)) * &4 * pi <= s1`);;
 421 e (ABBREV_TAC `s2 = sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X))`);;
 422 e (ABBREV_TAC `s3 = sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X))`);;
 423 e (ASM_REAL_ARITH_TAC);;
 424 e (NEW_GOAL `(&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi <= (&2 * mm1 / pi) * s1`);;
 425 e (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= (c - b) * a`]);;
 426 e (MATCH_MP_TAC REAL_LE_MUL);;
 427 e (STRIP_TAC);;
 428 e (ASM_REAL_ARITH_TAC);;
 429 e (MATCH_MP_TAC REAL_LE_MUL);;
 430 e (STRIP_TAC);;
 431 e (REAL_ARITH_TAC);;
 432 e (MATCH_MP_TAC REAL_LE_DIV);;
 433 e (REWRITE_TAC[PI_POS_LE]);;
 434 e (NEW_GOAL `#1.012080 < mm1`);;
 435 e (REWRITE_TAC[Flyspeck_constants.bounds]);;
 436 e (UP_ASM_TAC THEN REAL_ARITH_TAC);;
 437
 438 e (NEW_GOAL `&(CARD (A1:real^3->bool)) * &8 * mm1 +
 439              ((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 <=
 440              (&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi`);;
 441 e (REWRITE_TAC[REAL_ARITH `((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 =
 442   (--C * r pow 2) * (&8 * mm1) * (pi / pi)`]);;
 443 e (REWRITE_TAC[REAL_ARITH `(&2 * mm1 / pi) * &(CARD A2) * &4 * pi =
 444   &(CARD A2) * (&8 * mm1) * (pi / pi)`]);;
 445 e (REWRITE_WITH `pi / pi = &1`);;
 446 e (MATCH_MP_TAC REAL_DIV_REFL);;
 447 e (MP_TAC PI_POS THEN REAL_ARITH_TAC);;
 448 e (REWRITE_TAC[REAL_MUL_RID; REAL_ARITH `a * b + c * b <= d * b <=>
 449   &0 <= (d - a - c) * b `]);;
 450 e (MATCH_MP_TAC REAL_LE_MUL);;
 451 e (STRIP_TAC);;
 452 e (REWRITE_TAC[REAL_ARITH `&0 <= a - b - (--c * x) <=> b - a <= c * x`]);;
 453
 454 e (NEW_GOAL `A2 SUBSET A1:real^3->bool`);;
 455 e (EXPAND_TAC "A1" THEN EXPAND_TAC "A2");;
 456 e (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> V INTER A SUBSET V INTER B`));;
 457 e (MATCH_MP_TAC SUBSET_BALL);;
 458 e (REAL_ARITH_TAC);;
 459 e (REWRITE_WITH `&(CARD (A1:real^3->bool)) - &(CARD (A2:real^3->bool)) =
 460    &(CARD A1 - CARD A2)`);;
 461 e (MATCH_MP_TAC REAL_OF_NUM_SUB);;
 462 e (MATCH_MP_TAC CARD_SUBSET);;
 463 e (ASM_REWRITE_TAC[]);;
 464
 465 e (REWRITE_WITH `CARD (A1:real^3->bool) - CARD (A2:real^3->bool) =
 466    CARD (A1 DIFF A2)`);;
 467 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
 468 e (MATCH_MP_TAC CARD_DIFF);;
 469 e (ASM_REWRITE_TAC[]);;
 470 e (ASM_REWRITE_TAC[]);;
 471
 472 e (MATCH_MP_TAC REAL_LE_MUL);;
 473 e (NEW_GOAL `#1.012080 < mm1`);;
 474 e (REWRITE_TAC[Flyspeck_constants.bounds]);;
 475 e (UP_ASM_TAC THEN REAL_ARITH_TAC);;
 476
 477
 478 e (ASM_REAL_ARITH_TAC);;
 479 e (EXISTS_TAC `&0`);;
 480 e (REPEAT STRIP_TAC);;
 481 e (NEW_GOAL `F`);;
 482 e (ASM_MESON_TAC[]);;
 483 e (ASM_MESON_TAC[]);;
 484
 485 let KIZHLTL2 = top_thm();;
 486
 487 (* ========================================================================== *)
 488 open Flyspeck_constants;;
 489
 490 let SUM_PAIR_2_SET = prove
 491 (`!f s:real^N->bool d.
 492  FINITE s
 493 ==> sum {(m,n) | m IN s /\ n IN s /\ ~(m = n) /\ dist(m,n) <= d}
 494  (\(m,n). f {m, n}) = &2 *
 495  sum {{m, n} | m IN s /\ n IN s /\ ~(m = n) /\ dist(m,n) <= d} f`,
 496 REPEAT STRIP_TAC THEN MP_TAC(ISPECL
 497  [`\(m:real^N,n). {m,n}`;`(\(m,n). f {m,n}):real^N#real^N->real`;
 498   `{(m,n) | m IN s /\ n IN s /\ ~(m:real^N = n) /\ dist(m,n) <= d}`;
 499   `{{m,n} | m IN s /\ n IN s /\ ~(m:real^N = n) /\ dist(m,n) <= d}`]
 500   SUM_GROUP) THEN
 501   ANTS_TAC THENL
 502  [CONJ_TAC THENL
 503  [ONCE_REWRITE_TAC[SET_RULE
 504  `m IN s /\ n IN s /\ P m n <=>
 505   m IN s /\ n IN {n | n IN s /\ P m n}`] THEN
 506   MATCH_MP_TAC FINITE_PRODUCT_DEPENDENT THEN
 507   ASM_SIMP_TAC[FINITE_RESTRICT];
 508   REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN SET_TAC[]];
 509   DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM SUM_LMUL] THEN
 510   MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
 511   MAP_EVERY X_GEN_TAC [`m:real^N`; `n:real^N`] THEN STRIP_TAC THEN
 512   MATCH_MP_TAC EQ_TRANS THEN
 513   EXISTS_TAC `sum {(m:real^N,n), (n,m)} (\(m,n). f {m,n})` THEN
 514   CONJ_TAC THENL
 515   [AP_THM_TAC THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
 516   REWRITE_TAC[FORALL_PAIR_THM] THEN
 517   REWRITE_TAC[IN_ELIM_THM; PAIR_EQ; IN_INSERT; NOT_IN_EMPTY;
 518   SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`] THEN
 519   ASM_MESON_TAC[DIST_SYM];
 520   SIMP_TAC[SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
 521   ASM_REWRITE_TAC[IN_SING; NOT_IN_EMPTY; PAIR_EQ; REAL_ADD_RID] THEN
 522   REWRITE_TAC[INSERT_AC] THEN REAL_ARITH_TAC]]);;
 523
 524 (* ========================================================================== *)
 525
 526 let H0_LT_SQRT2 = prove_by_refinement (`h0 < sqrt (&2)`,
 527 [REWRITE_TAC[h0; GSYM sqrt2];
 528  NEW_GOAL `#1.414213 < sqrt2`;
 529  REWRITE_TAC[bounds];
 530  ASM_REAL_ARITH_TAC]);;
 531
 532 (* ========================================================================== *)
 533
 534 let gamma_y_pos_le = prove_by_refinement (
 535  `!V X e. packing V /\ saturated V /\ mcell_set V X /\ edgeX V X e
 536                         ==> &0 <= gammaY V X lmfun e`,
 537 [(REPEAT STRIP_TAC);
 538  (REWRITE_TAC[gammaY]);
 539  (NEW_GOAL `?u v. (VX V X u /\ VX V X v /\ ~(u = v)) /\ e = {u, v}`);
 540  (UP_ASM_TAC THEN REWRITE_TAC[edgeX; IN_ELIM_THM]);
 541  (UP_ASM_TAC THEN STRIP_TAC);
 542  (ASM_REWRITE_TAC[]);
 543  (ABBREV_TAC `f = (\u v. if {u, v} IN edgeX V X
 544              then dihX V X (u,v) * lmfun (hl [u; v])
 545              else &0)`);
 546  (REWRITE_WITH `(\({u, v}). if {u, v} IN edgeX V X
 547              then dihX V X (u,v) * lmfun (hl [u; v])
 548              else &0) = (\({u, v}). f u v)`);
 549  (EXPAND_TAC "f" THEN REWRITE_TAC[]);
 550  (REWRITE_WITH `(\({u:real^3, v}). f u v) {u, v} = (f:real^3->real^3->real) u v`);
 551  (MATCH_MP_TAC BETA_PAIR_THM);
 552  (EXPAND_TAC "f" THEN REPEAT STRIP_TAC);
 553  (REPEAT COND_CASES_TAC);
 554  (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 555  (REWRITE_WITH `dihX V X (u',v') = dihX V X (v',u')`);
 556  (MATCH_MP_TAC DIHX_SYM);
 557  (ASM_REWRITE_TAC[]);
 558  (NEW_GOAL `F`);
 559  (UP_ASM_TAC THEN REWRITE_TAC[]);
 560  (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN ASM_REWRITE_TAC[]);
 561  (ASM_MESON_TAC[]);
 562  (NEW_GOAL `F`);
 563  (UP_ASM_TAC THEN REWRITE_TAC[]);
 564  (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`] THEN ASM_REWRITE_TAC[]);
 565  (ASM_MESON_TAC[]);
 566  (REFL_TAC);
 567  (EXPAND_TAC "f");
 568  (COND_CASES_TAC);
 569  (MATCH_MP_TAC REAL_LE_MUL);
 570  (REWRITE_TAC[DIHX_POS;lmfun_pos_le]);
 571  (REAL_ARITH_TAC)]);;
 572
 573 (* ========================================================================== *)
 574
 575 let BETA_SET_2_THM = prove
 576  (`!g:(A->bool)->B u0 v0. (\({u, v}). g {u, v}) {u0, v0} = g {u0, v0}`,
 577  GEN_TAC THEN REWRITE_TAC[GABS_DEF;GEQ_DEF] THEN
 578  CONV_TAC SELECT_CONV THEN EXISTS_TAC `g:(A->bool)->B` THEN
 579  REWRITE_TAC[]);;
 580
 581 (* ========================================================================== *)
 582 (* Begin to prove KIZHLTL4 *)
 583 (* ========================================================================== *)
 584 (*                                                               *)
 585 (*    #use "/home/ky/flyspeck/working/marchal_cells_3.hl";;                   *)
 586 (*    #use "/home/ky/flyspeck/working/empty.hl";;                             *)
 587 (*                                                                            *)
 588 (* ========================================================================== *)
 589
 590
 591 (* ========================================================================== *)
 592
 593 let KIZHLTL4_concl =
 594   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r
 595                ==> (&8 * mm2 / pi) *
 596                    sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
 597                    (\X. sum (edgeX V X)
 598                         (\({u, v}). if {u, v} IN edgeX V X
 599                                     then dihX V X (u,v) * lmfun (hl [u; v])
 600                                     else &0)) +
 601                    c * r pow 2 <=
 602                    &8 *
 603                    mm2 *
 604                    sum (V INTER ball (vec 0,r))
 605                    (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 606                         (\v. lmfun (hl [u; v])))`;;
 607
 608 (* ========================================================================== *)
 609
 610 g KIZHLTL4_concl;;
 611 e (REPEAT STRIP_TAC);;
 612 e (ASM_CASES_TAC `saturated V /\ packing V`);;
 613 e (ABBREV_TAC `c = &8 * mm2 * (&0)`);;
 614 e (EXISTS_TAC `c:real`);;  (* choose d later *)
 615
 616 (* ------------------------------------------------------------------------- *)
 617
 618 e (REPEAT STRIP_TAC);;
 619 e (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);;
 620 e (ABBREV_TAC `V1:real^3->bool = V INTER ball (vec 0, r)`);;
 621 e (ABBREV_TAC `T1 = {{u,v:real^3} | u IN V1 /\ v IN V1}`);;
 622
 623 e (NEW_GOAL `FINITE (S1:(real^3->bool)->bool)`);;
 624 e (EXPAND_TAC "S1");;
 625 e (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);;
 626
 627 e (NEW_GOAL `FINITE (T1:(real^3->bool)->bool)`);;
 628 e (EXPAND_TAC "T1");;
 629 e (REWRITE_TAC[GSYM set_of_list]);;
 630 e (MATCH_MP_TAC FINITE_SUBSET);;
 631 e (EXISTS_TAC `IMAGE (set_of_list) {[u; v:real^3] | u IN V1 /\ v IN V1}`);;
 632 e (STRIP_TAC);;
 633 e (MATCH_MP_TAC FINITE_IMAGE);;
 634 e (REWRITE_TAC[SET_RULE `{[u;v] | u IN s /\ v IN s} =
 635                          {y | ?u0 u1. u0 IN s /\ u1 IN s /\ y = [u0; u1]}`]);;
 636 e (MATCH_MP_TAC FINITE_LIST_KY_LEMMA_2);;
 637 e (EXPAND_TAC "V1" THEN MATCH_MP_TAC Packing3.KIUMVTC);;
 638 e (ASM_REWRITE_TAC[]);;
 639 e (SET_TAC[]);;
 640
 641 e (ABBREV_TAC
 642    `S2 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~NULLSET X}`);;
 643 e (NEW_GOAL `FINITE (S2:(real^3->bool)->bool)`);;
 644 e (MATCH_MP_TAC FINITE_SUBSET);;
 645 e (EXISTS_TAC `S1:(real^3->bool)->bool`);;
 646 e (ASM_REWRITE_TAC[]);;
 647 e (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);;
 648
 649 e (ABBREV_TAC `g = (\X. (\({u, v}).
 650                             if {u, v} IN edgeX V X
 651                             then dihX V X (u,v) * lmfun (hl [u; v])
 652                             else &0))`);;
 653 e (REWRITE_WITH
 654 `sum S1  (\X. sum (edgeX V X)
 655                  (\({u, v}). if {u, v} IN edgeX V X
 656                              then dihX V X (u,v) * lmfun (hl [u; v])
 657                              else &0)) =
 658  sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u,v}))`);;
 659 e (MATCH_MP_TAC SUM_EQ);;
 660
 661 e (EXPAND_TAC "S1" THEN REWRITE_TAC[IN_ELIM_THM; IN; mcell_set_2]);;
 662 e (REPEAT STRIP_TAC);;
 663 e (MATCH_MP_TAC SUM_EQ);;
 664 e (REWRITE_WITH `!x'. x' IN edgeX V x <=>
 665                       ?u v. VX V x u /\ VX V x v /\ ~(u = v) /\ x' = {u, v}`);;
 666 e (REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);;
 667 e (MESON_TAC[]);;
 668 e (REPEAT STRIP_TAC);;
 669
 670 e (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
 671              then dihX V x (u,v) * lmfun (hl [u; v])
 672              else &0)`);;
 673 e (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);;
 674 e (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);;
 675 e (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);;
 676 e (REPEAT GEN_TAC THEN COND_CASES_TAC);;
 677 e (COND_CASES_TAC);;
 678 e (REWRITE_WITH `dihX V x (u',v') = dihX V x (v',u')`);;
 679 e (MATCH_MP_TAC DIHX_SYM);;
 680 e (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);;
 681 e (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list` THEN ASM_REWRITE_TAC[]);;
 682 e (UP_ASM_TAC THEN MESON_TAC[]);;
 683 e (COND_CASES_TAC);;
 684 e (UP_ASM_TAC THEN MESON_TAC[]);;
 685 e (REFL_TAC);;
 686
 687 e (REWRITE_WITH `(\({u, v}). if edgeX V x {u, v}
 688              then dihX V x (u,v) * lmfun (hl [u; v])
 689              else &0) = (\({u, v}). f_temp u v)`);;
 690 e (EXPAND_TAC "f_temp");;
 691 e (REWRITE_TAC[]);;
 692
 693 e (REWRITE_TAC[BETA_SET_2_THM; ASSUME `x' = {u,v:real^3}`]);;
 694 e (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} =
 695                              (f_temp:real^3->real^3->real) u v`);;
 696 e (MATCH_MP_TAC BETA_PAIR_THM);;
 697 e (ASM_REWRITE_TAC[]);;
 698
 699 e (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x =
 700                  (\({u, v}). f_temp u v)`);;
 701 e (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);;
 702 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
 703 e (MATCH_MP_TAC BETA_PAIR_THM);;
 704 e (ASM_REWRITE_TAC[]);;
 705
 706 (* ----------------------------------------------------------------------- *)
 707
 708 e (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u, v})) =
 709                  sum S1 (\X. sum (edgeX V X)  (g X))`);;
 710 e (MATCH_MP_TAC SUM_EQ);;
 711 e (REWRITE_TAC[] THEN REPEAT STRIP_TAC);;
 712 e (MATCH_MP_TAC SUM_EQ);;
 713 e (REWRITE_TAC[edgeX; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);;
 714 e (ASM_REWRITE_TAC[BETA_SET_2_THM]);;
 715
 716 e (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (g X)) =
 717                  sum S2 (\X. sum (edgeX V X) (g X))`);;
 718 e (MATCH_MP_TAC SUM_SUPERSET);;
 719 e (STRIP_TAC);;
 720 e (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);;
 721 e (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);;
 722 e (REPEAT STRIP_TAC);;
 723 e (MATCH_MP_TAC SUM_EQ_0);;
 724 e (REPEAT STRIP_TAC);;
 725
 726 e (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
 727              then dihX V x (u,v) * lmfun (hl [u; v])
 728              else &0)`);;
 729 e (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);;
 730 e (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);;
 731 e (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);;
 732 e (REPEAT GEN_TAC THEN COND_CASES_TAC);;
 733 e (COND_CASES_TAC);;
 734 e (REWRITE_WITH `dihX V x (u,v) = dihX V x (v,u)`);;
 735
 736 e (MATCH_MP_TAC DIHX_SYM);;
 737 e (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);;
 738 e (UP_ASM_TAC THEN MESON_TAC[]);;
 739 e (COND_CASES_TAC);;
 740 e (UP_ASM_TAC THEN MESON_TAC[]);;
 741 e (REFL_TAC);;
 742
 743 e (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x =
 744                  (\({u, v}). f_temp u v)`);;
 745 e (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);;
 746 e (UNDISCH_TAC `x' IN edgeX V x` THEN REWRITE_TAC[IN;IN_ELIM_THM; edgeX]);;
 747 e (STRIP_TAC);;
 748 e (ASM_SIMP_TAC[BETA_PAIR_THM]);;
 749 e (EXPAND_TAC "f_temp");;
 750 e (COND_CASES_TAC);;
 751 e (REWRITE_TAC[dihX]);;
 752 e (COND_CASES_TAC);;
 753 e (REAL_ARITH_TAC);;
 754 e (NEW_GOAL `F`);;
 755 e (ASM_MESON_TAC[]);;
 756 e (UP_ASM_TAC THEN MESON_TAC[]);;
 757 e (REFL_TAC);;
 758
 759 e (REWRITE_WITH
 760  `sum S2 (\X. sum (edgeX V X) (g X)) =
 761   sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X))`);;
 762 e (MATCH_MP_TAC SUM_EQ);;
 763 e (EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);;
 764 e (REPEAT STRIP_TAC);;
 765 e (AP_THM_TAC THEN AP_TERM_TAC);;
 766 e (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);;
 767 e (STRIP_TAC);;
 768 e (SET_TAC[]);;
 769 e (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]);;
 770 e (EXPAND_TAC "T1" THEN REWRITE_TAC[SUBSET; edgeX; IN; IN_ELIM_THM]);;
 771 e (REPEAT STRIP_TAC);;
 772 e (EXPAND_TAC "V1" THEN REWRITE_TAC[IN_ELIM_THM]);;
 773 e (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);;
 774 e (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; IN_INTER;
 775                MESON[IN] `V (x:real^3) <=> x IN V`]);;
 776 e (NEW_GOAL `VX V x = V INTER x`);;
 777 e (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);;
 778 e (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);;
 779 e (STRIP_TAC);;
 780 e (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);;
 781 e (ASM_REWRITE_TAC[]);;
 782 e (ASM_SET_TAC[]);;
 783
 784 e (REWRITE_WITH
 785   `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) =
 786    sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);;
 787 e (REWRITE_WITH
 788   `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) =
 789    sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (\x.g X x))`);;
 790 e (REWRITE_TAC[ETA_AX]);;
 791 e (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);;
 792
 793 (* May 09 - OK here *)
 794
 795 e (ABBREV_TAC
 796   `T2 = {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\ ~(u0 = u1) /\
 797                            hl[u0;u1] <= h0}`);;
 798 e (NEW_GOAL `sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x)) =
 799              sum T2 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);;
 800 e (MATCH_MP_TAC SUM_SUPERSET);;
 801 e (EXPAND_TAC "T1" THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN
 802    REPEAT STRIP_TAC);;
 803 e (SET_TAC[]);;
 804 e (MATCH_MP_TAC SUM_EQ_0);;
 805 e (EXPAND_TAC "g" THEN REPEAT STRIP_TAC);;
 806 e (ASM_REWRITE_TAC[]);;
 807
 808 e (ABBREV_TAC `f_temp = (\u v. if {u, v} IN edgeX V x'
 809              then dihX V x' (u,v) * lmfun (hl [u; v])
 810              else &0)`);;
 811 e (REWRITE_WITH `(\({u, v}). if {u, v} IN edgeX V x'
 812              then dihX V x' (u,v) * lmfun (hl [u; v])
 813              else &0) = (\({u, v}). f_temp u v)`);;
 814 e (EXPAND_TAC "f_temp");;
 815 e (REWRITE_TAC[]);;
 816 e (ASM_REWRITE_TAC[]);;
 817
 818 e (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} =
 819                              (f_temp:real^3->real^3->real) u v`);;
 820 e (MATCH_MP_TAC BETA_PAIR_THM);;
 821 e (ASM_REWRITE_TAC[]);;
 822 e (EXPAND_TAC "f_temp");;
 823 e (REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC);;
 824 e (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} ={b,a}`]);;
 825 e (REWRITE_WITH `dihX V x' (u',v') = dihX V x' (v',u')`);;
 826 e (MATCH_MP_TAC DIHX_SYM);;
 827 e (ASM_REWRITE_TAC[]);;
 828 e (UNDISCH_TAC `x' IN {X | S2 X /\ edgeX V X x}`);;
 829 e (EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);;
 830 e (MESON_TAC[]);;
 831 e (NEW_GOAL `F`);;
 832 e (UP_ASM_TAC THEN REWRITE_TAC[]);;
 833 e (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);;
 834 e (ASM_REWRITE_TAC[]);;
 835 e (UP_ASM_TAC THEN MESON_TAC[]);;
 836 e (NEW_GOAL `F`);;
 837 e (UP_ASM_TAC THEN REWRITE_TAC[]);;
 838 e (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);;
 839 e (ASM_REWRITE_TAC[]);;
 840 e (UP_ASM_TAC THEN MESON_TAC[]);;
 841 e (REFL_TAC);;
 842
 843 e (EXPAND_TAC "f_temp");;
 844 e (COND_CASES_TAC);;
 845
 846 e (ASM_CASES_TAC `hl [u; v:real^3] <= h0`);;
 847 e (NEW_GOAL `F`);;
 848 e (UNDISCH_TAC `~(?u0 u1.
 849             (V1 u0 /\ V1 u1 /\ ~(u0 = u1) /\ hl [u0; u1] <= h0) /\
 850             x = {u0, u1:real^3})` THEN REWRITE_TAC[]);;
 851 e (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);;
 852 e (ASM_REWRITE_TAC[]);;
 853 e (UNDISCH_TAC `{u, v} IN edgeX V x'` THEN REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);;
 854 e (REPEAT STRIP_TAC);;
 855 e (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 856 e (UP_ASM_TAC THEN MESON_TAC[]);;
 857 e (REWRITE_WITH `lmfun (hl [u; v:real^3]) = &0`);;
 858 e (ASM_REWRITE_TAC[lmfun]);;
 859 e (REAL_ARITH_TAC);;
 860 e (REFL_TAC);;
 861
 862 e (ASM_REWRITE_TAC[]);;
 863
 864 (* ==================================================================== *)
 865
 866 e (MATCH_MP_TAC (REAL_ARITH `(?b. a <= b /\ b + d <= e) ==> a + d <= e`));;
 867 e (EXISTS_TAC `(&8 * mm2 / pi) *
 868      sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x))`);;
 869 e (STRIP_TAC);;
 870 e (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= a * (c - b)`]);;
 871 e (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);;
 872 e (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);;
 873 e (REAL_ARITH_TAC);;
 874 e (MATCH_MP_TAC REAL_LE_DIV THEN SIMP_TAC[ZERO_LE_MM2_LEMMA; PI_POS_LE]);;
 875 e (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);;
 876 e (MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC);;
 877 e (MATCH_MP_TAC FINITE_SUBSET);;
 878 e (EXISTS_TAC `T1:(real^3->bool)->bool`);;
 879 e (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);;
 880 e (REWRITE_TAC[BETA_THM]);;
 881 e (MATCH_MP_TAC SUM_SUBSET_SIMPLE);;
 882
 883 e (STRIP_TAC);;
 884 e (REWRITE_TAC[IN] THEN MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);;
 885 e (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]
 886    THEN STRIP_TAC);;
 887 e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);;
 888 e (REPEAT STRIP_TAC);;
 889
 890 e (EXPAND_TAC "S2" THEN REWRITE_TAC[IN] THEN SET_TAC[]);;
 891 e (REWRITE_TAC[BETA_THM]);;
 892 e (REWRITE_WITH `g x' x = gammaY V x' lmfun x`);;
 893 e (EXPAND_TAC "g" THEN REWRITE_TAC[gammaY]);;
 894 e (MATCH_MP_TAC gamma_y_pos_le);;
 895
 896 e (UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_DIFF; IN; IN_ELIM_THM]);;
 897 e (MESON_TAC[]);;
 898 e (REWRITE_WITH
 899   `sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x)) =
 900    sum T2 (\x. &2 * pi * lmfun (radV x))`);;
 901 e (MATCH_MP_TAC SUM_EQ);;
 902 e (REPEAT STRIP_TAC);;
 903 e (REWRITE_TAC[BETA_THM]);;
 904 e (EXPAND_TAC "g");;
 905
 906 e (REWRITE_TAC[HL; BETA_THM; set_of_list]);;
 907 e (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);;
 908 e (STRIP_TAC);;
 909
 910 e (REWRITE_WITH `sum {X | mcell_set V X /\ edgeX V X x}
 911  (\X. (\({u, v}). if edgeX V X {u, v}
 912                   then dihX V X (u,v) * lmfun (radV {u, v}) else &0) x) =
 913                 sum {X | mcell_set V X /\ edgeX V X x}
 914  (\X. (if edgeX V X {u0, u1}
 915                   then dihX V X (u0,u1) * lmfun (radV {u0, u1}) else &0))`);;
 916 e (MATCH_MP_TAC SUM_EQ);;
 917 e (ASM_REWRITE_TAC[IN; IN_ELIM_THM; BETA_THM] THEN REPEAT STRIP_TAC);;
 918 e (ABBREV_TAC
 919   `f_temp = (\u v. if edgeX V x' {u, v}
 920                    then dihX V x' (u,v) * lmfun (radV {u, v}) else &0)`);;
 921 e (NEW_GOAL `!u:real^3 v:real^3.
 922             (f_temp:real^3->real^3->real) u v = f_temp v u`);;
 923 e (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);;
 924 e (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);;
 925 e (REPEAT GEN_TAC THEN COND_CASES_TAC);;
 926 e (COND_CASES_TAC);;
 927 e (REWRITE_WITH `dihX V x' (u,v) = dihX V x' (v,u)`);;
 928
 929 e (MATCH_MP_TAC DIHX_SYM);;
 930 e (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);;
 931 e (UP_ASM_TAC THEN MESON_TAC[]);;
 932 e (COND_CASES_TAC);;
 933 e (UP_ASM_TAC THEN MESON_TAC[]);;
 934 e (REFL_TAC);;
 935
 936 e (REWRITE_WITH
 937  `(\({u, v}). if edgeX V x' {u, v}
 938               then dihX V x' (u,v) * lmfun (radV {u, v})
 939               else &0)
 940     = (\({u, v}). f_temp u v)`);;
 941 e (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);;
 942 e (REWRITE_WITH
 943   `(if edgeX V x' {u0, u1}
 944    then dihX V x' (u0,u1) * lmfun (radV {u0, u1}) else &0) =
 945    f_temp u0 u1`);;
 946 e (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);;
 947 e (MATCH_MP_TAC BETA_PAIR_THM);;
 948 e (ASM_REWRITE_TAC[]);;
 949
 950 e (NEW_GOAL `FINITE {X | mcell_set V X /\ edgeX V X x}`);;
 951 e (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);;
 952 e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);;
 953 e (ASM_SIMP_TAC [SUM_CASES]);;
 954
 955 e (REWRITE_TAC[SET_RULE
 956  `{X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\ edgeX V X {u0, u1}} =
 957   {X | mcell_set V X /\ edgeX V X {u0, u1}} /\
 958   {X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\
 959       ~edgeX V X {u0, u1}} = {}`; SUM_CLAUSES; REAL_ARITH `a + &0 = a`]);;
 960 e (REWRITE_TAC[SUM_RMUL]);;
 961 e (REWRITE_WITH
 962   `sum {X | mcell_set V X /\ edgeX V X {u0, u1}} (\X. dihX V X (u0,u1)) =
 963    &2 * pi`);;
 964 e (REWRITE_WITH
 965   `{X | mcell_set V X /\ edgeX V X {u0, u1}} =
 966    {X | mcell_set V X /\ {u0, u1} IN edgeX V X}`);;
 967 e (REWRITE_TAC[IN]);;
 968 e (MATCH_MP_TAC GRUTOTI);;
 969 e (ASM_REWRITE_TAC[]);;
 970 e (REPEAT STRIP_TAC);;
 971 e (ASM_SET_TAC[]);;
 972 e (ASM_SET_TAC[]);;
 973 e (NEW_GOAL `h0 < sqrt (&2)`);;
 974 e (REWRITE_TAC[H0_LT_SQRT2]);;
 975 e (ASM_REAL_ARITH_TAC);;
 976 e (REAL_ARITH_TAC);;
 977 e (REWRITE_TAC[SUM_LMUL; REAL_ARITH `(&8 * mm2 / pi) * &2 * pi * a =
 978                                      (&8 * mm2) * (pi / pi) * (&2 * a)`]);;
 979 e (REWRITE_WITH `pi / pi = &1`);;
 980 e (MATCH_MP_TAC REAL_DIV_REFL);;
 981 e (REWRITE_TAC[PI_NZ]);;
 982 e (REWRITE_TAC[REAL_ARITH `&1 * a = a`]);;
 983 e (EXPAND_TAC "c");;
 984 e (REWRITE_TAC[REAL_ARITH
 985   `(&8 * mm2) * a + (&8 * mm2 * d) * b <= &8 * mm2 * c <=>
 986    &0 <= (&8 * mm2) * (c - a - d * b)`]);;
 987 e (MATCH_MP_TAC REAL_LE_MUL);;
 988 e (SIMP_TAC[REAL_LE_MUL; REAL_ARITH `&0 <= &8`; ZERO_LE_MM2_LEMMA]);;
 989 e (REWRITE_TAC[REAL_ARITH `&0 <= a - b - c <=> b + c <= a`]);;
 990
 991 e (EXPAND_TAC "T2");;
 992 e (REWRITE_TAC[Marchal_cells_3.HL_2;
 993    REAL_ARITH `inv (&2) * x <= y <=> x <= &2 * y`]);;
 994 e (REWRITE_WITH `&2 *
 995  sum
 996  {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\
 997                    ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
 998  (\x. lmfun (radV x)) =
 999  sum
1000  {u0:real^3,u1 | u0 IN V1 /\ u1 IN V1 /\
1001                 ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
1002  (\(u0,u1). (\x. lmfun (radV x)) {u0, u1})`);;
1003 e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
1004 e (MATCH_MP_TAC SUM_PAIR_2_SET);;
1005 e (EXPAND_TAC "V1");;
1006 e (ASM_SIMP_TAC [Packing3.KIUMVTC]);;
1007 e (REWRITE_TAC[GSYM Marchal_cells_3.HL_2; HL;set_of_list]);;
1008
1009 e (ABBREV_TAC
1010   `t = (\u:real^3. {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0})`);;
1011 e (ABBREV_TAC `f_temp = (\u v. lmfun (radV {u:real^3, v}))`);;
1012
1013 e (REWRITE_WITH
1014 `sum V1
1015  (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v:real^3) <= &2 * h0}
1016  (\v. lmfun (radV {u, v}))) =
1017  sum V1
1018  (\u:real^3. sum
1019  ((t:real^3->real^3->bool) u) ((f_temp:real^3->real^3->real) u))`);;
1020
1021 e (EXPAND_TAC "f_temp" THEN EXPAND_TAC "t");;
1022 e (REWRITE_TAC[]);;
1023
1024 e (REWRITE_WITH
1025  `sum V1 (\i. sum (t i) (f_temp i)) =
1026   sum {u0:real^3,u1:real^3 | u0 IN V1 /\ u1 IN t u0} (\(u0,u1). f_temp u0 u1)`);;
1027 e (MATCH_MP_TAC SUM_SUM_PRODUCT);;
1028 e (REPEAT STRIP_TAC);;
1029 e (EXPAND_TAC "V1");;
1030 e (ASM_SIMP_TAC [Packing3.KIUMVTC]);;
1031 e (EXPAND_TAC "t");;
1032 e (MATCH_MP_TAC FINITE_SUBSET);;
1033 e (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0, r + &2 * h0)`);;
1034 e (STRIP_TAC);;
1035 e (ASM_SIMP_TAC [Packing3.KIUMVTC]);;
1036 e (REWRITE_TAC[SUBSET; IN; IN_INTER; IN_BALL; IN_ELIM_THM]);;
1037 e (REPEAT STRIP_TAC);;
1038 e (ASM_REWRITE_TAC[]);;
1039 e (NEW_GOAL `dist (vec 0, x) <= dist (vec 0, u0) + dist (u0, x:real^3)`);;
1040 e (NORM_ARITH_TAC);;
1041 e (NEW_GOAL `dist (vec 0, u0:real^3) < r`);;
1042 e (REWRITE_TAC[GSYM IN_BALL]);;
1043 e (UNDISCH_TAC `u0:real^3 IN V1` THEN EXPAND_TAC "V1" THEN SET_TAC[]);;
1044 e (ASM_REAL_ARITH_TAC);;
1045 e (EXPAND_TAC "t" THEN EXPAND_TAC "f_temp");;
1046 e (REWRITE_TAC[IN; IN_ELIM_THM]);;
1047 e (REWRITE_TAC[REAL_ARITH `a + &0 * r pow 2 = a`]);;
1048 e (MATCH_MP_TAC SUM_SUBSET_SIMPLE);;
1049 e (REPEAT STRIP_TAC);;
1050
1051 e (MATCH_MP_TAC FINITE_SUBSET);;
1052 e (EXISTS_TAC
1053   `{u0:real^3,u1:real^3 |u0 IN V1 /\u1 IN V INTER ball (vec 0, r + &2 * h0)}`);;
1054 e (STRIP_TAC);;
1055 e (MATCH_MP_TAC FINITE_PRODUCT);;
1056 e (STRIP_TAC);;
1057 e (EXPAND_TAC "V1");;
1058 e (ASM_SIMP_TAC [Packing3.KIUMVTC]);;
1059 e (ASM_SIMP_TAC [Packing3.KIUMVTC]);;
1060 e (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);;
1061 e (REPEAT STRIP_TAC);;
1062 e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);;
1063 e (ASM_REWRITE_TAC[]);;
1064 e (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);;
1065 e (REWRITE_TAC[IN_BALL; IN_INTER; IN]);;
1066 e (ASM_REWRITE_TAC[]);;
1067
1068 e (NEW_GOAL `dist (vec 0, u1) <= dist (vec 0, u0) + dist (u0, u1:real^3)`);;
1069 e (NORM_ARITH_TAC);;
1070 e (NEW_GOAL `dist (vec 0, u0:real^3) < r`);;
1071 e (REWRITE_TAC[GSYM IN_BALL]);;
1072 e (UNDISCH_TAC `(V1:real^3->bool) u0` THEN EXPAND_TAC "V1");;
1073 e (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);;
1074 e (SET_TAC[]);;
1075 e (ASM_REAL_ARITH_TAC);;
1076 e (EXPAND_TAC "V1" THEN
1077    REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`; IN_INTER] THEN
1078    SET_TAC[]);;
1079 e (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN]);;
1080 e (REPEAT STRIP_TAC);;
1081 e (ASM_REWRITE_TAC[]);;
1082 e (REWRITE_TAC[lmfun_pos_le]);;
1083
1084 e (EXISTS_TAC `&0`);;
1085 e (REPEAT STRIP_TAC);;
1086 e (NEW_GOAL `F`);;
1087 e (ASM_MESON_TAC[]);;
1088 e (ASM_MESON_TAC[]);;
1089
1090 let KIZHLTL4 = top_thm();;