text_formalization/volume/vol1.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Volume                                                      *)\r
   5 (* Author: Nguyen Tat Thang                                                  *)\r
   6 (* Date: 2010-02-09                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 \r
  10 \r
  11 \r
  12 flyspeck_needs "general/prove_by_refinement.hl";;\r
  13 \r
  14 (* flyspeck_needs "trigonometry/trig2.hl";; *)\r
  15 \r
  16 \r
  17 \r
  18 \r
  19 module Vol1 = struct\r
  20 \r
  21 \r
  22   let prove_by_refinement = Prove_by_refinement.prove_by_refinement;;\r
  23 \r
  24   let BY = Hales_tactic.BY;;\r
  25 \r
  26 \r
  27 (* DEPRECATED 2013-05-25.\r
  28 let sphere= new_definition`sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;\r
  29 *)\r
  30 \r
  31 (* old definitions added by thales Nov 11, 2009 *)\r
  32 \r
  33 (*\r
  34 let radial_norm = new_definition `radial_norm r (x:real^A) C <=> (C SUBSET normball x r) /\ (!u. (x+u) IN C ==> (!t.(t> &0) /\ (t* norm u < r)==>(x+ t % u) IN C))`;;\r
  35 *)\r
  36 \r
  37 let radial_norm_deprecated = new_definition `(radial_norm:real->real^A->(real^A->bool)->bool) = radial`;;\r
  38 \r
  39 let radial_norm = prove_by_refinement(\r
  40   `!r x C. radial_norm r (x:real^A) C <=>\r
  41          C SUBSET normball x r /\\r
  42          (!u. x + u IN C\r
  43               ==> (!t. t > &0 /\ t * norm u < r ==> x + t % u IN C))`,\r
  44   (* {{{ proof *)\r
  45   [\r
  46     (REWRITE_TAC[radial_norm_deprecated;NORMBALL_BALL;Sphere.radial])\r
  47   ]);;\r
  48   (* }}} *)\r
  49 \r
  50 let RADIAL_VS_RADIAL_NORM = prove_by_refinement (\r
  51  `!(x:real^A) r C. radial r x C <=> radial_norm r x C`,\r
  52 [ \r
  53   (REWRITE_TAC[radial_norm_deprecated])\r
  54 ]);;\r
  55 \r
  56 (*\r
  57 let eventually_radial_norm = new_definition \r
  58   `eventually_radial_norm x C <=> (?r. (r> &0) /\ radial_norm r x (C INTER normball x r))`;;\r
  59 *)\r
  60 \r
  61   let eventually_radial_norm_deprecated =  new_definition\r
  62     `(eventually_radial_norm:real^A ->(real^A->bool)->bool) = eventually_radial`;;\r
  63 \r
  64 let eventually_radial_norm = prove_by_refinement(\r
  65   `!C (x:real^A). eventually_radial_norm x C <=>\r
  66          (?r. r > &0 /\ radial_norm r x (C INTER normball x r)) `,\r
  67   (* {{{ proof *)\r
  68   [\r
  69   REWRITE_TAC[eventually_radial_norm_deprecated;radial_norm_deprecated;Sphere.eventually_radial;NORMBALL_BALL]\r
  70   ]);;\r
  71   (* }}} *)\r
  72 \r
  73 let c_cone = new_definition `c_cone (v,w:real^3, r:real)={x:real^3 | ((x-v) dot w = norm (x-v)* norm w* r)}`;;\r
  74 \r
  75 let null_equiv = new_definition `null_equiv (s,t :real^3->bool)=(? (B:real^3-> bool). NULLSET B  /\\r
  76  ((s DIFF t) UNION (t DIFF s)) SUBSET B)`;;\r
  77 \r
  78 let VOLUME_PROPS_MEASURABLE = prove_by_refinement(\r
  79   `!C. measurable C ==> vol C >= &0`,\r
  80   (* {{{ proof *)\r
  81   [\r
  82   ASM_REWRITE_TAC[volume_props]\r
  83   ]);;\r
  84   (* }}} *)\r
  85 \r
  86 let VOLUME_PROPS_NULLSET = prove_by_refinement(\r
  87   `  (!Z. NULLSET Z ==> vol Z = &0)`,\r
  88   (* {{{ proof *)\r
  89   [\r
  90   ASM_REWRITE_TAC[volume_props]\r
  91   ]);;\r
  92   (* }}} *)\r
  93 \r
  94 let VOLUME_PROPS_SDIFF = prove_by_refinement(\r
  95   ` (!X Y.\r
  96           measurable X /\ measurable Y /\ NULLSET (SDIFF X Y)\r
  97           ==> vol X = vol Y)`,\r
  98   (* {{{ proof *)\r
  99   [\r
 100   ASM_REWRITE_TAC[volume_props]\r
 101   ]);;\r
 102   (* }}} *)\r
 103 \r
 104 \r
 105 let VOLUME_PROPS_SCALE = prove_by_refinement(\r
 106   `(!X t.\r
 107           measurable X /\ measurable (IMAGE (scale t) X)\r
 108           ==> vol (IMAGE (scale t) X) = abs (t$1 * t$2 * t$3) * vol X)`,\r
 109   (* {{{ proof *)\r
 110   [\r
 111   ASM_REWRITE_TAC[volume_props]\r
 112   ]);;\r
 113   (* }}} *)\r
 114 \r
 115 let VOLUME_PROPS_IMAGE = prove_by_refinement(\r
 116   `(!X v. measurable X ==> vol (IMAGE ((+) v) X) = vol X)`,\r
 117   (* {{{ proof *)\r
 118   [\r
 119   ASM_REWRITE_TAC[volume_props]\r
 120   ]);;\r
 121   (* }}} *)\r
 122 \r
 123 let VOLUME_PROPS_SOLID_TRIANGLE = prove_by_refinement(\r
 124   `(!v0 v1 v2 v3 r.\r
 125           r > &0 /\ ~coplanar {v0, v1, v2, v3}\r
 126           ==> vol (solid_triangle v0 {v1, v2, v3} r) =\r
 127               vol_solid_triangle v0 v1 v2 v3 r)`,\r
 128   (* {{{ proof *)\r
 129   [\r
 130   ASM_REWRITE_TAC[volume_props]\r
 131   ]);;\r
 132   (* }}} *)\r
 133 \r
 134 let VOLUME_PROPS_CONV0 = prove_by_refinement(\r
 135   ` (!v0 v1 v2 v3. vol (conv0 {v0, v1, v2, v3}) = vol_conv v0 v1 v2 v3)`,\r
 136   (* {{{ proof *)\r
 137   [\r
 138   ASM_REWRITE_TAC[volume_props]\r
 139   ]);;\r
 140   (* }}} *)\r
 141 \r
 142 let VOLUME_PROPS_FRUSTT = prove_by_refinement(\r
 143   ` (!v0 v1 v2 v3 h a.\r
 144           ~collinear {v0, v1, v2} /\\r
 145           ~collinear {v0, v1, v3} /\\r
 146           h >= &0 /\\r
 147           a > &0 /\\r
 148           a <= &1\r
 149           ==> vol (frustt v0 v1 h a INTER wedge v0 v1 v2 v3) =\r
 150               vol_frustt_wedge v0 v1 v2 v3 h a)`,\r
 151   (* {{{ proof *)\r
 152   [\r
 153   ASM_REWRITE_TAC[volume_props]\r
 154   ]);;\r
 155   (* }}} *)\r
 156 \r
 157 let VOLUME_PROPS_CONIC_CAP = prove_by_refinement(\r
 158   ` (!v0 v1 v2 v3 r c.\r
 159           ~collinear {v0, v1, v2} /\\r
 160           ~collinear {v0, v1, v3} /\\r
 161           r >= &0 /\\r
 162           c >= -- &1 /\\r
 163           c <= &1\r
 164           ==> vol (conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3) =\r
 165               vol_conic_cap_wedge v0 v1 v2 v3 r c)`,\r
 166   (* {{{ proof *)\r
 167   [\r
 168   ASM_REWRITE_TAC[volume_props]\r
 169   ]);;\r
 170   (* }}} *)\r
 171 \r
 172 let VOLUME_PROPS_RECT = prove_by_refinement(\r
 173   ` (!a b. vol (rect a b) = vol_rect a b) `,\r
 174   (* {{{ proof *)\r
 175   [\r
 176   ASM_REWRITE_TAC[volume_props]\r
 177   ]);;\r
 178   (* }}} *)\r
 179 \r
 180 let VOLUME_PROPS_NORMBALL = prove_by_refinement(\r
 181   ` (!v0 v1 v2 v3 r.\r
 182           ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3} /\ r >= &0\r
 183           ==> vol (normball v0 r INTER wedge v0 v1 v2 v3) =\r
 184               vol_ball_wedge v0 v1 v2 v3 r)`,\r
 185   (* {{{ proof *)\r
 186   [\r
 187   ASM_REWRITE_TAC[volume_props]\r
 188   ]);;\r
 189   (* }}} *)\r
 190 \r
 191 \r
 192 \r
 193 (*----------------------------------------------------------*)\r
 194 \r
 195 (*To prove Lemma 4.2*)\r
 196 \r
 197 \r
 198 \r
 199 let th1= prove(`!a b c. [a; b; c]= CONS a (CONS b [c])`,REPEAT GEN_TAC THEN MESON_TAC[]);;\r
 200 \r
 201 let dodai=prove(`!a b c. LENGTH [a; b; c] = 3`,REPEAT GEN_TAC THEN REWRITE_TAC[LENGTH;th1] THEN ARITH_TAC);;\r
 202 \r
 203 let th3=prove(`!i. (1<=i /\ i<= 3)==>(vec 1:real^3)$i= &1`,GEN_TAC THEN DISCH_TAC THEN (ASM_SIMP_TAC[VEC_COMPONENT;DIMINDEX_3]));;\r
 204 \r
 205 let identity_scale=prove(`scale (vec 1)= I`,REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN REWRITE_TAC[I_THM] THEN REWRITE_TAC[scale] THEN REWRITE_TAC[vector] THEN SIMP_TAC[dodai] THEN REWRITE_TAC[CART_EQ] THEN REWRITE_TAC[DIMINDEX_3] THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN MP_TAC (ARITH_RULE `(1 <= i /\ i <= 3) <=> ( i=1 \/ i=2 \/ i=3)`) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]] THENL [ASM_REWRITE_TAC[ARITH_RULE `1-1=0`];REWRITE_TAC[ARITH_RULE `2-1= SUC 0 `];REWRITE_TAC[ARITH_RULE `3-1= SUC 1 `]] THENL [REWRITE_TAC[EL];REWRITE_TAC[EL];REWRITE_TAC[EL]] THENL [REWRITE_TAC[HD];REWRITE_TAC[HD;TL];REWRITE_TAC[ARITH_RULE `1= SUC 0 `;EL]] THENL [SIMP_TAC[th3;ARITH_RULE `1<=1 /\ 1<=3`];SIMP_TAC[th3;ARITH_RULE `1<=2 /\ 2<=3`];REWRITE_TAC[HD;TL]] THENL [ARITH_TAC;ARITH_TAC;REWRITE_TAC[ARITH_RULE `SUC 0=1`]] THEN SIMP_TAC[th3;ARITH_RULE `1<=3 /\ 3<=3`] THEN ARITH_TAC);;\r
 206 \r
 207 let th4=prove(`!(S: A->bool). IMAGE I S= S`,GEN_TAC THEN REWRITE_TAC[IMAGE] THEN REWRITE_TAC[I_THM] THEN SET_TAC[]);;\r
 208 \r
 209 let SET_EQ=prove(`(A: real^3 -> bool) = B <=> (!a. a IN A ==> a IN B) /\ (!a. a IN B ==> a IN A)`,SET_TAC[]);;\r
 210 \r
 211 let scale_mul=prove(`!(s:real) t x. (scale (s%(t:real^3)) (x:real^3):real^3) = s% scale t x`,REPEAT GEN_TAC THEN REWRITE_TAC[scale] THEN REWRITE_TAC[vector] THEN SIMP_TAC[dodai] THEN REWRITE_TAC[CART_EQ] THEN REWRITE_TAC[DIMINDEX_3] THEN ASM_REWRITE_TAC[ARITH_RULE `(1 <= i /\ i <=3) <=> i =1 \/ i=2 \/ i=3`] THEN GEN_TAC THEN STRIP_TAC THENL [ASM_REWRITE_TAC[LAMBDA_BETA];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]] THENL [SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];SIMP_TAC[VECTOR_MUL_COMPONENT;LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`];SIMP_TAC[VECTOR_MUL_COMPONENT;LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`]] THENL [SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`\r
 212 ];REWRITE_TAC[EL;ARITH_RULE `2-1=SUC 0`];REWRITE_TAC[EL;ARITH_RULE `3-1=SUC 1`]] THENL [SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];REWRITE_TAC[HD;TL];REWRITE_TAC[EL;ARITH_RULE `1=SUC 0`]] THENL [REWRITE_TAC[ARITH_RULE `1-1=0`;EL];ARITH_TAC;REWRITE_TAC[HD;TL]] THENL[REWRITE_TAC[HD];ARITH_TAC] THEN ARITH_TAC);;\r
 213 \r
 214 let normball_ellip0=prove(`!r. normball (vec 0:real^3) r = ellipsoid (vec 1) r`,GEN_TAC THEN REWRITE_TAC[ellipsoid] THEN REWRITE_TAC[SET_EQ] THEN STRIP_TAC THENL [GEN_TAC;GEN_TAC] THENL [REWRITE_TAC[IN_IMAGE];REWRITE_TAC[IN_IMAGE]] THENL [DISCH_TAC;SIMP_TAC[identity_scale]] THENL [(EXISTS_TAC `a:real^3`);REWRITE_TAC[I_THM]] THENL [CONJ_TAC;REPEAT STRIP_TAC] THENL [SIMP_TAC[identity_scale];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]] THEN REWRITE_TAC[I_THM]);;\r
 215 \r
 216 let trans_normball=prove(`!(x:real^3) r. normball x r = IMAGE ((+) x) (normball (vec 0) r)`,REPEAT GEN_TAC THEN REWRITE_TAC[SET_EQ] THEN STRIP_TAC THENL [GEN_TAC;GEN_TAC] THENL [REWRITE_TAC[IN_IMAGE;normball];REWRITE_TAC[IN_IMAGE;normball]] THENL [REWRITE_TAC[IN_ELIM_THM];REWRITE_TAC[IN_ELIM_THM]] THENL [REWRITE_TAC[dist];REWRITE_TAC[dist]] THENL [DISCH_TAC;REWRITE_TAC[VECTOR_SUB_RZERO]] THENL [EXISTS_TAC `a-x:real^3`;REPEAT STRIP_TAC] THENL [REWRITE_TAC[VECTOR_ADD_SUB];ASM_REWRITE_TAC[]] THENL [CONJ_TAC;REWRITE_TAC[VECTOR_ADD_SUB]] THENL [REWRITE_TAC[VECTOR_SUB_ADD2];REWRITE_TAC[VECTOR_SUB_RZERO];ASM_REWRITE_TAC[]] THEN ASM_REWRITE_TAC[]);;\r
 217 \r
 218 let measurable_normball0=prove(`!r. measurable (normball (vec 0:real^3) r)`,GEN_TAC THEN MESON_TAC[primitive;MEASURABLE_RULES;normball_ellip0]);;\r
 219 \r
 220 let measurable_normball=prove(`!(x:real^3) r. measurable (normball x r)`,REPEAT GEN_TAC THEN MESON_TAC[MEASURABLE_RULES;trans_normball;measurable_normball0]);;\r
 221 \r
 222 let rsduong=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> r/s> &0`,REPEAT GEN_TAC THEN STRIP_TAC THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[ARITH_RULE `s> &0 <=> &0 <s`] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*s= &0`] THEN ASM_REAL_ARITH_TAC);;\r
 223 \r
 224 let rsnon_zero=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> ~(r/s= &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `r/s> &0` MP_TAC THENL[ASM_SIMP_TAC[rsduong];REAL_ARITH_TAC]);;\r
 225 \r
 226 let rduong=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> (r> &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool`THEN REAL_ARITH_TAC);;\r
 227 \r
 228 let rnon_zero=prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> ~(r= &0)`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `r> &0` MP_TAC THENL[UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];REAL_ARITH_TAC] THEN ASM_REWRITE_TAC[rduong]);;\r
 229 \r
 230 let rs_sr_unit= prove(`!(s:real) (r:real). (s> &0) /\ (s<r)==> (s / r * r / s= &1)`,\r
 231 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(r/s= &0)` MP_TAC\r
 232 THENL [UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];STRIP_TAC]\r
 233 THENL [ASM_REWRITE_TAC[rsnon_zero];SUBGOAL_THEN `r/s= inv(s/r)` MP_TAC] \r
 234 THENL [UNDISCH_TAC `~(r / s = &0):bool`;SIMP_TAC[]]\r
 235 THENL [ASM_SIMP_TAC[REAL_INV_DIV];DISCH_TAC]\r
 236 THEN SUBGOAL_THEN `~(s/r= &0)` MP_TAC\r
 237 THENL [MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`);SIMP_TAC[REAL_MUL_RINV]]\r
 238 THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[CONTRAPOS_THM]\r
 239 THEN DISCH_TAC THEN SUBGOAL_THEN `r*s/r = r* &0` MP_TAC\r
 240 THENL [REWRITE_TAC[ARITH_RULE `r * s / r = r * &0 <=> r * s / r - r * &0 = &0`];SUBGOAL_THEN `~(r= &0)` MP_TAC]\r
 241 THENL [REWRITE_TAC[ARITH_RULE `r * s / r - r * &0 = r*(s/r- &0)`];UNDISCH_TAC `(s<r):bool`THEN UNDISCH_TAC `(s> &0):bool`THEN REWRITE_TAC[TAUT `A==>B ==> C <=> A/\B==>C`];ASM_SIMP_TAC[REAL_DIV_LMUL]]\r
 242 THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[rnon_zero];REAL_ARITH_TAC]\r
 243 THEN ARITH_TAC);;\r
 244 \r
 245 \r
 246 let SQRT_MUL_POW_2= prove(`!(a:real) b. (a>= &0) /\ (b>= &0) ==> sqrt((a*a)*b)= a* sqrt(b)`,\r
 247 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `a*a>= &0` MP_TAC\r
 248 THENL [REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`];DISCH_TAC THEN UNDISCH_TAC `(b>= &0):bool`]\r
 249 THENL [SIMP_TAC[REAL_LE_SQUARE];REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`]]\r
 250 THEN UNDISCH_TAC `(a * a >= &0):bool` THEN REWRITE_TAC[ARITH_RULE `a*a>= &0 <=> &0 <= a*a`]\r
 251 THEN REWRITE_TAC[TAUT `A==>B ==>C <=> A/\ B ==> C`]\r
 252 THEN SIMP_TAC[SQRT_MUL] THEN SUBGOAL_THEN `sqrt(a*a)= a` MP_TAC\r
 253 THENL [UNDISCH_TAC `(a>= &0):bool`;MESON_TAC[]]\r
 254 THEN REWRITE_TAC[ARITH_RULE `s>= &0 <=> &0<= s`]\r
 255 THEN SIMP_TAC[SQRT_MUL] THEN SIMP_TAC[SQRT_POW_2] THEN MESON_TAC[REAL_POW_2;SQRT_POW_2]);;\r
 256 \r
 257 (*\r
 258 \r
 259 g `!r s (x:real^3) C. radial_norm r x C /\ (s > &0) /\ (s < r) ==> (C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r))))`;;\r
 260 \r
 261 e (REPEAT GEN_TAC THEN STRIP_TAC);;\r
 262 \r
 263 e (REWRITE_TAC[SET_EQ] THEN CONJ_TAC THEN GEN_TAC);;\r
 264 \r
 265 e (REWRITE_TAC[IN_INTER;IN_IMAGE]);;\r
 266 \r
 267 e (STRIP_TAC);;\r
 268 \r
 269 e (EXISTS_TAC `a-x:real^3`);;\r
 270 \r
 271 e (REWRITE_TAC[VECTOR_ARITH `(a:real^3)= x+a-x`]);;\r
 272 \r
 273 e (EXISTS_TAC `scale (r/s% vec 1)(a-x):real^3`);;\r
 274 \r
 275 e (SIMP_TAC[scale_mul] THEN SIMP_TAC[identity_scale] THEN REWRITE_TAC[I_THM]);;\r
 276 \r
 277 e (REWRITE_TAC[VECTOR_MUL_ASSOC]);;\r
 278 \r
 279 e (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 280 \r
 281 e (SIMP_TAC[rs_sr_unit]);;\r
 282 \r
 283 e (STRIP_TAC);;\r
 284 \r
 285 e (CONJ_TAC);;\r
 286 \r
 287 e (VECTOR_ARITH_TAC);;\r
 288 \r
 289 e (EXISTS_TAC `(x+r / s % (a - x)):real^3`);;\r
 290 \r
 291 e (CONJ_TAC);;\r
 292 \r
 293 e (VECTOR_ARITH_TAC);;\r
 294 \r
 295 e (CONJ_TAC);;\r
 296 \r
 297 e (SUBGOAL_THEN `(x:real^3)+(a-x) IN (C:real^3->bool)` MP_TAC);;\r
 298 \r
 299 e (UNDISCH_TAC `(a:real^3 IN (C:real^3->bool)):bool`);;\r
 300 \r
 301 e (MP_TAC(VECTOR_ARITH `(a:real^3)=x+(a-x)`));;\r
 302 \r
 303 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 304 \r
 305 e (SET_TAC[]);;\r
 306 \r
 307 e (DISCH_TAC);;\r
 308 \r
 309 e (SUBGOAL_THEN `(r/s)> &0 /\ (r/s) * (norm (a:real^3-x):real)< r` MP_TAC);;\r
 310 \r
 311 e (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 312 \r
 313 e (SIMP_TAC[rsduong]);;\r
 314 \r
 315 e (STRIP_TAC);;\r
 316 \r
 317 e (UNDISCH_TAC `(a:real^3 IN normball x s):bool`);;\r
 318 \r
 319 e (REWRITE_TAC[normball]);;\r
 320 \r
 321 e (REWRITE_TAC[IN_ELIM_THM;dist]);;\r
 322 \r
 323 e (ABBREV_TAC `c= norm(a:real^3 -x)`);;\r
 324 \r
 325 e (DISCH_TAC);;\r
 326 \r
 327 e (SUBGOAL_THEN `r/s> &0` MP_TAC);;\r
 328 \r
 329 e (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 330 \r
 331 e (SIMP_TAC[rsduong]);;\r
 332 \r
 333 e (REWRITE_TAC[ARITH_RULE `s> &0 <=> &0< s`]);;\r
 334 \r
 335 e (DISCH_TAC);;\r
 336 \r
 337 e (SUBGOAL_THEN `r/s*c < r/s*s` MP_TAC);;\r
 338 \r
 339 e (UNDISCH_TAC `(c < s):bool` THEN UNDISCH_TAC `(&0< r/s):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 340 \r
 341 e (REWRITE_TAC[TAUT `A/\B==>C <=> B/\A==>C`] THEN REWRITE_TAC[ARITH_RULE `r / s * c < r / s * s <=> c*r/s < s*r/s`]);;\r
 342 \r
 343 e (REWRITE_TAC[REAL_LT_RMUL]);;\r
 344 \r
 345 e (MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`));;\r
 346 \r
 347 e (ASM_REWRITE_TAC[]);;\r
 348 \r
 349 e (REWRITE_TAC[TAUT `A==>B==>C <=>A/\B==>C`]);;\r
 350 \r
 351 e (SIMP_TAC[]);;\r
 352 \r
 353 e (MESON_TAC[REAL_DIV_RMUL]);;\r
 354 \r
 355 e (ASM_MESON_TAC[radial_norm]);;\r
 356 \r
 357 e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;\r
 358 \r
 359 e (REWRITE_TAC[VECTOR_ARITH `((x:real^3) + r / s % (a - x)) - x= r / s % (a - x)`]);;\r
 360 \r
 361 e (REWRITE_TAC[vector_norm]);;\r
 362 \r
 363 e (REWRITE_TAC[VECTOR_ARITH `r / s % ((a:real^3) - x) dot r / s % (a - x)= (r/s *r/s) * (a-x) dot (a-x)`]);;\r
 364 \r
 365 e (SUBGOAL_THEN `r/s> &0` MP_TAC);;\r
 366 \r
 367 e (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 368 \r
 369 e (REWRITE_TAC[rsduong]);;\r
 370 \r
 371 e (DISCH_TAC);;\r
 372 \r
 373 e (UNDISCH_TAC `(a IN normball (x:real^3) s):bool`);;\r
 374 \r
 375 e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;\r
 376 \r
 377 e (REWRITE_TAC[vector_norm]);;\r
 378 \r
 379 e (ABBREV_TAC `q2= (a:real^3 - x) dot (a - x)`);;\r
 380 \r
 381 e (DISCH_TAC);;\r
 382 \r
 383 e (UNDISCH_TAC `(sqrt q2 < s):bool`);;\r
 384 \r
 385 e (DISCH_TAC);;\r
 386 \r
 387 e (SUBGOAL_THEN `q2>= &0` MP_TAC);;\r
 388 \r
 389 \r
 390 e (REWRITE_TAC[ARITH_RULE `q2>= &0 <=> &0<= q2`]);;\r
 391 \r
 392 e (ASM_MESON_TAC[DOT_POS_LE]);;\r
 393 \r
 394 e (MP_TAC(ARITH_RULE `r/s> &0 ==> r/s>= &0`));;\r
 395 \r
 396 e (ASM_REWRITE_TAC[]);;\r
 397 \r
 398 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 399 \r
 400 e (SIMP_TAC[SQRT_MUL_POW_2]);;\r
 401 \r
 402 e (STRIP_TAC);;\r
 403 \r
 404 e (SUBGOAL_THEN `r/s*sqrt q2<r/s * s` MP_TAC);;\r
 405 \r
 406 e (REWRITE_TAC[ARITH_RULE `r / s * sqrt q2 < r / s * s<=> sqrt q2* r/s< s* r/s`]);;\r
 407 \r
 408 e (UNDISCH_TAC `(r / s > &0):bool` THEN REWRITE_TAC[ARITH_RULE `r / s > &0<=> &0< r/s`] THEN UNDISCH_TAC `(sqrt q2 < s):bool`);;\r
 409 \r
 410 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 411 \r
 412 e (SIMP_TAC[REAL_LT_RMUL]);;\r
 413 \r
 414 e (MP_TAC(ARITH_RULE `s> &0==> ~(s= &0)`));;\r
 415 \r
 416 e (ASM_REWRITE_TAC[]);;\r
 417 \r
 418 e (MESON_TAC[REAL_DIV_RMUL]);;\r
 419 \r
 420 e (REWRITE_TAC[IN_IMAGE;IN_INTER]);;\r
 421 \r
 422 e (REWRITE_TAC[scale_mul;identity_scale;I_THM]);;\r
 423 \r
 424 e(STRIP_TAC THEN CONJ_TAC);;\r
 425 \r
 426 e (ASM_SIMP_TAC[]);;\r
 427 \r
 428 e (SUBGOAL_THEN `(x:real^3) + (--x + x''') IN C` MP_TAC);;\r
 429 \r
 430 e (MP_TAC(VECTOR_ARITH `x'''= (x:real^3)+ (--x + x''')`));;\r
 431 \r
 432 e (ABBREV_TAC `u1= (x:real^3) + --x + x'''`);;\r
 433 \r
 434 e (UNDISCH_TAC `(x''' IN (C:real^3->bool)):bool`);;\r
 435 \r
 436 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 437 \r
 438 e (SET_TAC[]);;\r
 439 \r
 440 e (SUBGOAL_THEN `s/r> &0 /\s/r* norm (--x+ x''':real^3)< r` MP_TAC);;\r
 441 \r
 442 \r
 443 e (CONJ_TAC);;\r
 444 \r
 445 e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));;\r
 446 \r
 447 e (ASM_REWRITE_TAC[]);;\r
 448 \r
 449 e (REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`]);;\r
 450 \r
 451 e (REWRITE_TAC[REAL_LT_LDIV_EQ]);;\r
 452 \r
 453 e (REWRITE_TAC[REAL_LT_RDIV_EQ]);;\r
 454 \r
 455 e (SIMP_TAC[REAL_LT_RDIV_EQ]);;\r
 456 \r
 457 e (REWRITE_TAC[ARITH_RULE `&0*r= &0`]);;\r
 458 \r
 459 e (DISCH_TAC);;\r
 460 \r
 461 e (ASM_REWRITE_TAC[]);;\r
 462 \r
 463 e (REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`]);;\r
 464 \r
 465 e (ASM_REWRITE_TAC[]);;\r
 466 \r
 467 e (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);;\r
 468 \r
 469 e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]);;\r
 470 \r
 471 e (SUBGOAL_THEN `s/r< &1` ASSUME_TAC);;\r
 472 \r
 473 e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));;\r
 474 \r
 475 e (ASM_REWRITE_TAC[]);;\r
 476 \r
 477 e (REWRITE_TAC[ARITH_RULE `r> &0 <=> &0 <r`]);;\r
 478 \r
 479 e (REWRITE_TAC[ARITH_RULE `&1 * r= r`]);;\r
 480 \r
 481 e (DISCH_TAC);;\r
 482 \r
 483 e (ASM_REWRITE_TAC[]);;\r
 484 \r
 485 e (UNDISCH_TAC `( &0<r):bool`);;\r
 486 \r
 487 e (SIMP_TAC[REAL_LT_LDIV_EQ]);;\r
 488 \r
 489 \r
 490 e (REWRITE_TAC[ARITH_RULE `&1*r=r`]);;\r
 491 \r
 492 e (DISCH_TAC);;\r
 493 \r
 494 e (ASM_REWRITE_TAC[]);;\r
 495 \r
 496 e (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);;\r
 497 \r
 498 e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;\r
 499 \r
 500 e (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);;\r
 501 \r
 502 e (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));;\r
 503 \r
 504 e (ABBREV_TAC `v1= x''':real^3 - x`);;\r
 505 \r
 506 e (MESON_TAC[]);;\r
 507 \r
 508 e (ASM_SIMP_TAC[]);;\r
 509 \r
 510 e (SUBGOAL_THEN `&0<= norm (--x + x''':real^3)` MP_TAC);;\r
 511 \r
 512 e (SIMP_TAC[NORM_POS_LE]);;\r
 513 \r
 514 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 515 \r
 516 e (MP_TAC(ARITH_RULE `s/r> &0 /\ s/r< &1==> &0<= s/r /\ s/r< &1`));;\r
 517 \r
 518 e (ASM_REWRITE_TAC[]);;\r
 519 \r
 520 e (REWRITE_TAC[TAUT `A==>B/\C==>D <=> A/\B/\C==>D`]);;\r
 521 \r
 522 e (ABBREV_TAC `y= norm (--x + x''':real^3)`);;\r
 523 \r
 524 e (UNDISCH_TAC `(s / r < &1):bool`);;\r
 525 \r
 526 e (REWRITE_TAC[TAUT `A==>B/\C/\D==>E <=> (B/\A/\C/\D==>E)`]);;\r
 527 \r
 528 e (DISCH_TAC);;\r
 529 \r
 530 e (SUBGOAL_THEN `s/r*y< &1*r` MP_TAC);;\r
 531 \r
 532 e (UNDISCH_TAC `(&0 <= s / r /\ s / r < &1 /\ &0 <= y /\ y < r):bool`);;\r
 533 \r
 534 e (MESON_TAC[REAL_LT_MUL2]);;\r
 535 \r
 536 e (MESON_TAC[ARITH_RULE `&1*r= r`]);;\r
 537 \r
 538 e (REWRITE_TAC[TAUT `A/\B==>C==>D <=> A/\B/\C==>D`]);;\r
 539 \r
 540 e (ASM_MESON_TAC[radial_norm]);;\r
 541 \r
 542 e (ASM_REWRITE_TAC[]);;\r
 543 \r
 544 e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;\r
 545 \r
 546 e (REWRITE_TAC[VECTOR_ARITH `(x + s / r % (--x + x''')) - x= s / r % (--x + x''')`]);;\r
 547 \r
 548 e (SIMP_TAC[NORM_MUL]);;\r
 549 \r
 550 e (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);;\r
 551 \r
 552 e (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]);;\r
 553 \r
 554 e (MP_TAC(ARITH_RULE `s/r> &0==> s/r>= &0`));;\r
 555 \r
 556 e (ASM_REWRITE_TAC[]);;\r
 557 \r
 558 e (REWRITE_TAC[ARITH_RULE `s/r>= &0 <=> &0<= s/r`]);;\r
 559 \r
 560 e (DISCH_TAC);;\r
 561 \r
 562 e (SUBGOAL_THEN `abs (s / r)= s/r` MP_TAC);;\r
 563 \r
 564 e (ASM_SIMP_TAC[REAL_ABS_REFL]);;\r
 565 \r
 566 e (SIMP_TAC[]);;\r
 567 \r
 568 e (DISCH_TAC);;\r
 569 \r
 570 e (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);;\r
 571 \r
 572 e (REWRITE_TAC[normball;IN_ELIM_THM;dist]);;\r
 573 \r
 574 e (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);;\r
 575 \r
 576 e (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));;\r
 577 \r
 578 \r
 579 e (ABBREV_TAC `v2= x''':real^3 - x`);;\r
 580 \r
 581 e (MESON_TAC[]);;\r
 582 \r
 583 e (ASM_SIMP_TAC[]);;\r
 584 \r
 585 e (ABBREV_TAC `p= norm (--x + x''':real^3)`);;\r
 586 \r
 587 e (DISCH_TAC);;\r
 588 \r
 589 e (SUBGOAL_THEN `p*s/r< r*s/r` MP_TAC);;\r
 590 \r
 591 e (MP_TAC(ARITH_RULE `s / r > &0 ==> &0< s/r`));;\r
 592 \r
 593 e (ASM_REWRITE_TAC[]);;\r
 594 \r
 595 e (UNDISCH_TAC `(p < r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 596 \r
 597 e (SIMP_TAC[REAL_LT_RMUL]);;\r
 598 \r
 599 e (REWRITE_TAC[ARITH_RULE `s/r*p<s <=> p*s/r< s`]);;\r
 600 \r
 601 e (MP_TAC(ARITH_RULE `s<r/\s> &0 ==> ~(r= &0)`));;\r
 602 \r
 603 e (ASM_REWRITE_TAC[]);;\r
 604 \r
 605 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
 606 \r
 607 e (MESON_TAC[REAL_DIV_LMUL]);;\r
 608 \r
 609 \r
 610 let trans_strech_trans_radial=top_thm();;\r
 611 \r
 612 *)\r
 613 \r
 614 let trans_strech_trans_radial = prove_by_refinement(\r
 615 `!r s (x:real^3) C. radial_norm r x C /\ (s > &0) /\ (s < r) ==> (C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r))))`,\r
 616   (* {{{ proof *)\r
 617   [\r
 618   (REPEAT GEN_TAC THEN STRIP_TAC);\r
 619   (REWRITE_TAC[SET_EQ] THEN CONJ_TAC THEN GEN_TAC);\r
 620     (REWRITE_TAC[IN_INTER;IN_IMAGE]);\r
 621     (STRIP_TAC);\r
 622     (EXISTS_TAC `a-x:real^3`);\r
 623     (REWRITE_TAC[VECTOR_ARITH `(a:real^3)= x+a-x`]);\r
 624     (EXISTS_TAC `scale (r/s% vec 1)(a-x):real^3`);\r
 625     (SIMP_TAC[scale_mul] THEN SIMP_TAC[identity_scale] THEN REWRITE_TAC[I_THM]);\r
 626     (REWRITE_TAC[VECTOR_MUL_ASSOC]);\r
 627     (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 628     (SIMP_TAC[rs_sr_unit]);\r
 629     (STRIP_TAC);\r
 630     (CONJ_TAC);\r
 631       BY((VECTOR_ARITH_TAC));\r
 632     (EXISTS_TAC `(x+r / s % (a - x)):real^3`);\r
 633     (CONJ_TAC);\r
 634       BY((VECTOR_ARITH_TAC));\r
 635     (CONJ_TAC);\r
 636       (SUBGOAL_THEN `(x:real^3)+(a-x) IN (C:real^3->bool)` MP_TAC);\r
 637         (UNDISCH_TAC `(a:real^3 IN (C:real^3->bool)):bool`);\r
 638         (MP_TAC(VECTOR_ARITH `(a:real^3)=x+(a-x)`));\r
 639         (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 640         BY((SET_TAC[]));\r
 641       (DISCH_TAC);\r
 642       (SUBGOAL_THEN `(r/s)> &0 /\ (r/s) * (norm (a:real^3-x):real)< r` MP_TAC);\r
 643         (UNDISCH_TAC `(s> &0):bool` THEN UNDISCH_TAC `(s<r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 644         (SIMP_TAC[rsduong]);\r
 645         (STRIP_TAC);\r
 646         (UNDISCH_TAC `(a:real^3 IN normball x s):bool`);\r
 647         (REWRITE_TAC[normball]);\r
 648         (REWRITE_TAC[IN_ELIM_THM;dist]);\r
 649         (ABBREV_TAC `c= norm(a:real^3 -x)`);\r
 650         (DISCH_TAC);\r
 651         (SUBGOAL_THEN `r/s> &0` MP_TAC);\r
 652           (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 653           BY((SIMP_TAC[rsduong]));\r
 654         (REWRITE_TAC[ARITH_RULE `s> &0 <=> &0< s`]);\r
 655         (DISCH_TAC);\r
 656         (SUBGOAL_THEN `r/s*c < r/s*s` MP_TAC);\r
 657           (UNDISCH_TAC `(c < s):bool` THEN UNDISCH_TAC `(&0< r/s):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 658           (REWRITE_TAC[TAUT `A/\B==>C <=> B/\A==>C`] THEN REWRITE_TAC[ARITH_RULE `r / s * c < r / s * s <=> c*r/s < s*r/s`]);\r
 659           BY((REWRITE_TAC[REAL_LT_RMUL]));\r
 660         (MP_TAC(ARITH_RULE `s> &0 ==> ~(s= &0)`));\r
 661         (ASM_REWRITE_TAC[]);\r
 662         (REWRITE_TAC[TAUT `A==>B==>C <=>A/\B==>C`]);\r
 663         (SIMP_TAC[]);\r
 664         BY((MESON_TAC[REAL_DIV_RMUL]));\r
 665       BY((ASM_MESON_TAC[radial_norm]));\r
 666     (REWRITE_TAC[normball;IN_ELIM_THM;dist]);\r
 667     (REWRITE_TAC[VECTOR_ARITH `((x:real^3) + r / s % (a - x)) - x= r / s % (a - x)`]);\r
 668     (REWRITE_TAC[vector_norm]);\r
 669     (REWRITE_TAC[VECTOR_ARITH `r / s % ((a:real^3) - x) dot r / s % (a - x)= (r/s *r/s) * (a-x) dot (a-x)`]);\r
 670     (SUBGOAL_THEN `r/s> &0` MP_TAC);\r
 671       (UNDISCH_TAC `(s<r):bool` THEN UNDISCH_TAC `(s> &0):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 672       BY((REWRITE_TAC[rsduong]));\r
 673     (DISCH_TAC);\r
 674     (UNDISCH_TAC `(a IN normball (x:real^3) s):bool`);\r
 675     (REWRITE_TAC[normball;IN_ELIM_THM;dist]);\r
 676     (REWRITE_TAC[vector_norm]);\r
 677     (ABBREV_TAC `q2= (a:real^3 - x) dot (a - x)`);\r
 678     (DISCH_TAC);\r
 679     (UNDISCH_TAC `(sqrt q2 < s):bool`);\r
 680     (DISCH_TAC);\r
 681     (SUBGOAL_THEN `q2>= &0` MP_TAC);\r
 682       (REWRITE_TAC[ARITH_RULE `q2>= &0 <=> &0<= q2`]);\r
 683       BY((ASM_MESON_TAC[DOT_POS_LE]));\r
 684     (MP_TAC(ARITH_RULE `r/s> &0 ==> r/s>= &0`));\r
 685     (ASM_REWRITE_TAC[]);\r
 686     (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 687     (SIMP_TAC[SQRT_MUL_POW_2]);\r
 688     (STRIP_TAC);\r
 689     (SUBGOAL_THEN `r/s*sqrt q2<r/s * s` MP_TAC);\r
 690       (REWRITE_TAC[ARITH_RULE `r / s * sqrt q2 < r / s * s<=> sqrt q2* r/s< s* r/s`]);\r
 691       (UNDISCH_TAC `(r / s > &0):bool` THEN REWRITE_TAC[ARITH_RULE `r / s > &0<=> &0< r/s`] THEN UNDISCH_TAC `(sqrt q2 < s):bool`);\r
 692       (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 693       BY((SIMP_TAC[REAL_LT_RMUL]));\r
 694     (MP_TAC(ARITH_RULE `s> &0==> ~(s= &0)`));\r
 695     (ASM_REWRITE_TAC[]);\r
 696     BY((MESON_TAC[REAL_DIV_RMUL]));\r
 697   (REWRITE_TAC[IN_IMAGE;IN_INTER]);\r
 698   (REWRITE_TAC[scale_mul;identity_scale;I_THM]);\r
 699   (STRIP_TAC THEN CONJ_TAC);\r
 700     (ASM_SIMP_TAC[]);\r
 701     (SUBGOAL_THEN `(x:real^3) + (--x + x''') IN C` MP_TAC);\r
 702       (MP_TAC(VECTOR_ARITH `x'''= (x:real^3)+ (--x + x''')`));\r
 703       (ABBREV_TAC `u1= (x:real^3) + --x + x'''`);\r
 704       (UNDISCH_TAC `(x''' IN (C:real^3->bool)):bool`);\r
 705       (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 706       BY((SET_TAC[]));\r
 707     (SUBGOAL_THEN `s/r> &0 /\s/r* norm (--x+ x''':real^3)< r` MP_TAC);\r
 708       (CONJ_TAC);\r
 709         (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));\r
 710         (ASM_REWRITE_TAC[]);\r
 711         (REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`]);\r
 712         (REWRITE_TAC[REAL_LT_LDIV_EQ]);\r
 713         (REWRITE_TAC[REAL_LT_RDIV_EQ]);\r
 714         (SIMP_TAC[REAL_LT_RDIV_EQ]);\r
 715         (REWRITE_TAC[ARITH_RULE `&0*r= &0`]);\r
 716         (DISCH_TAC);\r
 717         (ASM_REWRITE_TAC[]);\r
 718         (REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`]);\r
 719         BY((ASM_REWRITE_TAC[]));\r
 720       (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);\r
 721         BY((MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]));\r
 722       (SUBGOAL_THEN `s/r< &1` ASSUME_TAC);\r
 723         (MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`));\r
 724         (ASM_REWRITE_TAC[]);\r
 725         (REWRITE_TAC[ARITH_RULE `r> &0 <=> &0 <r`]);\r
 726         (REWRITE_TAC[ARITH_RULE `&1 * r= r`]);\r
 727         (DISCH_TAC);\r
 728         (ASM_REWRITE_TAC[]);\r
 729         (UNDISCH_TAC `( &0<r):bool`);\r
 730         (SIMP_TAC[REAL_LT_LDIV_EQ]);\r
 731         (REWRITE_TAC[ARITH_RULE `&1*r=r`]);\r
 732         (DISCH_TAC);\r
 733         BY((ASM_REWRITE_TAC[]));\r
 734       (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);\r
 735       (REWRITE_TAC[normball;IN_ELIM_THM;dist]);\r
 736       (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);\r
 737         (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));\r
 738         (ABBREV_TAC `v1= x''':real^3 - x`);\r
 739         BY((MESON_TAC[]));\r
 740       (ASM_SIMP_TAC[]);\r
 741       (SUBGOAL_THEN `&0<= norm (--x + x''':real^3)` MP_TAC);\r
 742         BY((SIMP_TAC[NORM_POS_LE]));\r
 743       (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 744       (MP_TAC(ARITH_RULE `s/r> &0 /\ s/r< &1==> &0<= s/r /\ s/r< &1`));\r
 745       (ASM_REWRITE_TAC[]);\r
 746       (REWRITE_TAC[TAUT `A==>B/\C==>D <=> A/\B/\C==>D`]);\r
 747       (ABBREV_TAC `y= norm (--x + x''':real^3)`);\r
 748       (UNDISCH_TAC `(s / r < &1):bool`);\r
 749       (REWRITE_TAC[TAUT `A==>B/\C/\D==>E <=> (B/\A/\C/\D==>E)`]);\r
 750       (DISCH_TAC);\r
 751       (SUBGOAL_THEN `s/r*y< &1*r` MP_TAC);\r
 752         (UNDISCH_TAC `(&0 <= s / r /\ s / r < &1 /\ &0 <= y /\ y < r):bool`);\r
 753         BY((MESON_TAC[REAL_LT_MUL2]));\r
 754       BY((MESON_TAC[ARITH_RULE `&1*r= r`]));\r
 755     (REWRITE_TAC[TAUT `A/\B==>C==>D <=> A/\B/\C==>D`]);\r
 756     BY((ASM_MESON_TAC[radial_norm]));\r
 757   (ASM_REWRITE_TAC[]);\r
 758   (REWRITE_TAC[normball;IN_ELIM_THM;dist]);\r
 759   (REWRITE_TAC[VECTOR_ARITH `(x + s / r % (--x + x''')) - x= s / r % (--x + x''')`]);\r
 760   (SIMP_TAC[NORM_MUL]);\r
 761   (SUBGOAL_THEN `s/r> &0` ASSUME_TAC);\r
 762     BY((MP_TAC(ARITH_RULE `s<r /\ s> &0 ==> r> &0`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `a> &0 <=> &0<a`] THEN REWRITE_TAC[REAL_LT_LDIV_EQ] THEN REWRITE_TAC[REAL_LT_RDIV_EQ] THEN SIMP_TAC[REAL_LT_RDIV_EQ] THEN REWRITE_TAC[ARITH_RULE `&0*r= &0`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE `&0< s <=> s> &0`] THEN ASM_REWRITE_TAC[]));\r
 763   (MP_TAC(ARITH_RULE `s/r> &0==> s/r>= &0`));\r
 764   (ASM_REWRITE_TAC[]);\r
 765   (REWRITE_TAC[ARITH_RULE `s/r>= &0 <=> &0<= s/r`]);\r
 766   (DISCH_TAC);\r
 767   (SUBGOAL_THEN `abs (s / r)= s/r` MP_TAC);\r
 768     BY((ASM_SIMP_TAC[REAL_ABS_REFL]));\r
 769   (SIMP_TAC[]);\r
 770   (DISCH_TAC);\r
 771   (UNDISCH_TAC `(x''':real^3 IN normball x r):bool`);\r
 772   (REWRITE_TAC[normball;IN_ELIM_THM;dist]);\r
 773   (SUBGOAL_THEN `norm (x''':real^3 - x)= norm (--x + x''')` ASSUME_TAC);\r
 774     (MP_TAC(VECTOR_ARITH `x''':real^3 - x = --x + x'''`));\r
 775     (ABBREV_TAC `v2= x''':real^3 - x`);\r
 776     BY((MESON_TAC[]));\r
 777   (ASM_SIMP_TAC[]);\r
 778   (ABBREV_TAC `p= norm (--x + x''':real^3)`);\r
 779   (DISCH_TAC);\r
 780   (SUBGOAL_THEN `p*s/r< r*s/r` MP_TAC);\r
 781     (MP_TAC(ARITH_RULE `s / r > &0 ==> &0< s/r`));\r
 782     (ASM_REWRITE_TAC[]);\r
 783     (UNDISCH_TAC `(p < r):bool` THEN REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 784     BY((SIMP_TAC[REAL_LT_RMUL]));\r
 785   (REWRITE_TAC[ARITH_RULE `s/r*p<s <=> p*s/r< s`]);\r
 786   (MP_TAC(ARITH_RULE `s<r/\s> &0 ==> ~(r= &0)`));\r
 787   (ASM_REWRITE_TAC[]);\r
 788   (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);\r
 789   BY((MESON_TAC[REAL_DIV_LMUL]))\r
 790   ]);;\r
 791   (* }}} *)\r
 792 \r
 793 \r
 794 \r
 795 (*----------------------------------------------*)\r
 796 \r
 797 (* Lemma 4.2*)\r
 798 \r
 799 (* changed volume_props to volume_prop in the rest of this file. volume_props uses ball in the definition and volume_prop \r
 800    uses normball in the definition*)\r
 801 \r
 802 (*\r
 803 let volume_prop = new_definition `volume_prop  (vol:(real^3->bool)->real) = \r
 804     ( (!C. vol C >= &0) /\\r
 805      (!Z. NULLSET Z ==> (vol Z = &0)) /\\r
 806      (!X Y. measurable X /\ measurable Y /\ NULLSET (SDIFF X Y) ==> (vol X = vol Y)) /\\r
 807      (!X t. (measurable X) /\ (measurable (IMAGE (scale t) X)) ==> (vol (IMAGE (scale t) X) = abs(t$1 * t$2 * t$3)*vol(X))) /\\r
 808      (!X v. measurable X ==> (vol (IMAGE ((+) v) X) = vol X)) /\\r
 809      (!v0 v1 v2 v3 r. (r > &0) /\ (~(collinear {v0,v1,v2})) /\ ~(collinear {v0,v1,v3}) ==> vol (solid_triangle v0 {v1,v2,v3} r) = vol_solid_triangle v0 v1 v2 v3 r) /\\r
 810      (!v0 v1 v2 v3. vol(conv0 {v0,v1,v2,v3}) = vol_conv v0 v1 v2 v3) /\\r
 811      (!v0 v1 v2 v3 h a. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (h >= &0) /\ (a > &0) /\ (a <= &1) ==> vol(frustt v0 v1 h a INTER wedge v0 v1 v2 v3) = vol_frustt_wedge v0 v1 v2 v3 h a) /\\r
 812      (!v0 v1 v2 v3 r c.  ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) /\ (c >= -- (&1)) /\ (c <= &1) ==> (vol(conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3) = vol_conic_cap_wedge v0 v1 v2 v3 r c)) /\ \r
 813      (!(a:real^3) (b:real^3). vol(rect a b) = vol_rect a b) /\\r
 814      (!v0 v1 v2 v3 r. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0)  ==> (vol(normball v0 r INTER wedge v0 v1 v2 v3) = vol_ball_wedge v0 v1 v2 v3 r)))`;;\r
 815 *)\r
 816 \r
 817 let volume_prop_fix = new_definition `volume_prop_fix  (vol:(real^3->bool)->real) = \r
 818     ( (!C. measurable C ==> vol C >= &0) /\\r
 819      (!Z. NULLSET Z ==> (vol Z = &0)) /\\r
 820      (!X Y. measurable X /\ measurable Y /\ NULLSET (SDIFF X Y) ==> (vol X = vol Y)) /\\r
 821      (!X t. (measurable X) /\ (measurable (IMAGE (scale t) X)) ==> (vol (IMAGE (scale t) X) = abs(t$1 * t$2 * t$3)*vol(X))) /\\r
 822      (!X v. measurable X ==> (vol (IMAGE ((+) v) X) = vol X)) /\\r
 823      (!v0 v1 v2 v3 r. (r > &0) /\ ~coplanar {v0, v1, v2, v3}  ==> vol (solid_triangle v0 {v1,v2,v3} r) = vol_solid_triangle v0 v1 v2 v3 r) /\\r
 824      (!v0 v1 v2 v3. vol(conv0 {v0,v1,v2,v3}) = vol_conv v0 v1 v2 v3) /\\r
 825      (!v0 v1 v2 v3 h a. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (h >= &0) /\ (a > &0) /\ (a <= &1) ==> vol(frustt v0 v1 h a INTER wedge v0 v1 v2 v3) = vol_frustt_wedge v0 v1 v2 v3 h a) /\\r
 826      (!v0 v1 v2 v3 r c.  ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0) /\ (c >= -- (&1)) /\ (c <= &1) ==> (vol(conic_cap v0 v1 r c INTER wedge v0 v1 v2 v3) = vol_conic_cap_wedge v0 v1 v2 v3 r c)) /\ \r
 827      (!(a:real^3) (b:real^3). vol(rect a b) = vol_rect a b) /\\r
 828      (!v0 v1 v2 v3 r. ~(collinear {v0,v1,v2}) /\ ~(collinear {v0,v1,v3}) /\ (r >= &0)  ==> (vol(normball v0 r INTER wedge v0 v1 v2 v3) = vol_ball_wedge v0 v1 v2 v3 r)))`;;\r
 829 \r
 830 let VOLUME_FIX = prove(`volume_prop_fix vol`,\r
 831   REWRITE_TAC[volume_prop_fix;volume_props];\r
 832      );;\r
 833 \r
 834 \r
 835 let lemma_r_r' = prove_by_refinement(`! (C:real^3->bool) (x:real^3) r s. measurable C /\ volume_prop_fix (vol) /\ radial_norm r x C /\ (s > &0) /\ (s < r) ==> measurable (C INTER normball x s) /\ vol (C INTER normball x s)= vol (C) *(s/r) pow 3`,\r
 836 [\r
 837 REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC;\r
 838 ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball];\r
 839 SUBGOAL_THEN `C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC;\r
 840 ASM_SIMP_TAC[trans_strech_trans_radial];\r
 841 ASM_REWRITE_TAC[];\r
 842 SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC;\r
 843 ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball];\r
 844 SUBGOAL_THEN `measurable (IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r))` ASSUME_TAC;\r
 845 ASM_MESON_TAC[MEASURABLE_RULES];\r
 846 SUBGOAL_THEN `measurable (IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC;\r
 847 ASM_MESON_TAC[MEASURABLE_RULES];\r
 848 SUBGOAL_THEN `measurable (IMAGE ((+) x)  (IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))))` ASSUME_TAC;\r
 849 ASM_MESON_TAC[MEASURABLE_RULES];\r
 850 ABBREV_TAC `A2:real^3->bool= (IMAGE (scale (s / r % vec 1))       (IMAGE ((+) (--x)) (C INTER normball x r)))`;\r
 851 SUBGOAL_THEN `vol (IMAGE ((+) x) A2)=vol (A2)` MP_TAC;\r
 852 UNDISCH_TAC `(volume_prop_fix vol):bool`;\r
 853 UNDISCH_TAC `(measurable (A2:real^3->bool)):bool`;\r
 854 REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];\r
 855 SIMP_TAC[volume_prop_fix];\r
 856 SIMP_TAC[];\r
 857 DISCH_TAC;\r
 858 UNDISCH_TAC `(IMAGE (scale (s / r % vec 1))      (IMAGE ((+) (--x)) (C INTER normball x r)):real^3->bool =      A2):bool`;\r
 859 REWRITE_TAC[SET_RULE `IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)) = A2:real^3->bool <=> A2= IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))`];\r
 860 SIMP_TAC[];\r
 861 DISCH_TAC;\r
 862 ABBREV_TAC `M1:real^3->bool= (IMAGE ((+) (--x)) (C INTER normball x r))`;\r
 863 ABBREV_TAC `w:real^3= s / r % vec 1`;\r
 864 SUBGOAL_THEN `vol (IMAGE (scale (w:real^3)) M1)= abs (w$1*w$2*w$3)*vol (M1)` MP_TAC;\r
 865 SUBGOAL_THEN `measurable (IMAGE (scale w) M1)` MP_TAC;\r
 866 UNDISCH_TAC `(A2 = IMAGE (scale w) M1:real^3->bool):bool`;\r
 867 REWRITE_TAC[SET_RULE `A2 = IMAGE (scale w) M1 <=> IMAGE (scale w) M1= A2`];\r
 868 SIMP_TAC[];\r
 869 ASM_MESON_TAC[];\r
 870 UNDISCH_TAC `(volume_prop_fix vol):bool`;\r
 871 UNDISCH_TAC `(measurable (M1:real^3->bool)):bool`;\r
 872 REWRITE_TAC[TAUT `P1 ==> P2 ==> P3 ==> P4 <=> P1 /\ P2 /\ P3 ==> P4`];\r
 873 SIMP_TAC[volume_prop_fix];\r
 874 SIMP_TAC[];\r
 875 DISCH_TAC;\r
 876 SUBGOAL_THEN `((w:real^3)$1 = s/r)/\ (w$2 = s/r) /\ (w$3 = s/r)` MP_TAC;\r
 877 REPEAT STRIP_TAC;\r
 878 UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`;\r
 879 REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`];\r
 880 SIMP_TAC[];\r
 881 DISCH_TAC;\r
 882 SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`];\r
 883 SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<= 3`];\r
 884 ARITH_TAC;\r
 885 UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`;\r
 886 REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`];\r
 887 SIMP_TAC[];\r
 888 DISCH_TAC;\r
 889 SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`];\r
 890 SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<= 3`];\r
 891 ARITH_TAC;\r
 892 UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`;\r
 893 REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`];\r
 894 SIMP_TAC[];\r
 895 DISCH_TAC;\r
 896 SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`];\r
 897 SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<= 3`];\r
 898 ARITH_TAC;\r
 899 SIMP_TAC[];\r
 900 REWRITE_TAC[ARITH_RULE `s / r * s / r * s / r= (s/r) pow 3`];\r
 901 DISCH_TAC;\r
 902 SUBGOAL_THEN `s/r > &0` MP_TAC;\r
 903 SUBGOAL_THEN `r> &0` MP_TAC;\r
 904 UNDISCH_TAC `(s < r):bool` THEN UNDISCH_TAC `(s > &0):bool`;\r
 905 REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];\r
 906 MESON_TAC[rduong];\r
 907 REWRITE_TAC[ARITH_RULE `(r> &0 <=> &0< r) /\ (s / r > &0 <=> &0 < s/r)`];\r
 908 SIMP_TAC[REAL_LT_RDIV_EQ];\r
 909 DISCH_TAC;\r
 910 REWRITE_TAC[ARITH_RULE `&0*r= &0`];\r
 911 ASM_REWRITE_TAC[ARITH_RULE `&0< s<=> s> &0`];\r
 912 DISCH_TAC;\r
 913 SUBGOAL_THEN `&0<= s/r` MP_TAC;\r
 914 REWRITE_TAC[ARITH_RULE `&0 <= s / r <=> s/r >= &0`];\r
 915 UNDISCH_TAC `(s / r > &0):bool`;\r
 916 ARITH_TAC;\r
 917 DISCH_TAC;\r
 918 SUBGOAL_THEN `&0<= (s / r) pow 3` MP_TAC;\r
 919 UNDISCH_TAC `(&0<=s / r):bool`;\r
 920 MP_TAC(ARITH_RULE `&0 <= &0`);\r
 921 REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`];\r
 922 DISCH_TAC;\r
 923 REWRITE_TAC[ARITH_RULE `&0<= (s/r) pow 3 <=> &0 pow 3<= (s/r) pow 3`];\r
 924 UNDISCH_TAC `(&0 <= &0 /\ &0 <= s / r):bool`;\r
 925 MP_TAC(ARITH_RULE `~(3= 0)`);\r
 926 REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`];\r
 927 SIMP_TAC[REAL_POW_LE2];\r
 928 DISCH_TAC;\r
 929 SUBGOAL_THEN `abs ((s / r) pow 3)=(s / r) pow 3` MP_TAC;\r
 930 SIMP_TAC[REAL_ABS_REFL];\r
 931 ASM_MESON_TAC[];\r
 932 SIMP_TAC[];\r
 933 DISCH_TAC;\r
 934 REWRITE_TAC[ARITH_RULE `(s / r) pow 3 * vol M1= vol M1 * (s / r) pow 3`];\r
 935 SUBGOAL_THEN `vol M1= vol C` MP_TAC;\r
 936 UNDISCH_TAC `(IMAGE ((+) (--x:real^3)) ((C:real^3->bool) INTER normball x r) = (M1:real^3->bool)):bool`;\r
 937 REWRITE_TAC[SET_RULE `IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r) = M1 <=> M1= IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r)`];\r
 938 SIMP_TAC[];\r
 939 DISCH_TAC;\r
 940 SUBGOAL_THEN `vol (IMAGE ((+) (--x)) (C INTER normball x r))= vol (C INTER normball (x:real^3) r)` MP_TAC;\r
 941 UNDISCH_TAC `(volume_prop_fix vol):bool`;\r
 942 UNDISCH_TAC `(measurable ((C:real^3->bool) INTER normball x r)):bool`;\r
 943 REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`];\r
 944 SIMP_TAC[volume_prop_fix];\r
 945 SIMP_TAC[];\r
 946 DISCH_TAC;\r
 947 SUBGOAL_THEN `C INTER normball (x:real^3) r= C` MP_TAC;\r
 948 UNDISCH_TAC `(radial_norm r (x:real^3) C):bool`;\r
 949 REWRITE_TAC[radial_norm];\r
 950 REPEAT STRIP_TAC;\r
 951 UNDISCH_TAC `((C:real^3->bool) SUBSET normball (x:real^3) r):bool`;\r
 952 SIMP_TAC[SUBSET_INTER_ABSORPTION];\r
 953 DISCH_TAC;\r
 954 ABBREV_TAC `(E:real^3->bool)= C INTER normball x r`;\r
 955 ASM_MESON_TAC[];\r
 956 ABBREV_TAC `a:real= (s / r) pow 3`;\r
 957 ABBREV_TAC `a1:real= vol M1` THEN ABBREV_TAC `a2:real= vol C`;\r
 958 SIMP_TAC[]\r
 959 ]);;\r
 960 \r
 961 let lemma_r_r'_fix = REWRITE_RULE[VOLUME_FIX] lemma_r_r';;\r
 962 \r
 963 \r
 964 (*\r
 965 (* start old lemma_r_r' here *)\r
 966 \r
 967 g `! (C:real^3->bool) (x:real^3) r s. measurable C /\ volume_prop (vol) /\ radial_norm r x C /\ (s > &0) /\ (s < r) ==> measurable (C INTER normball x s) /\ vol (C INTER normball x s)= vol (C) *(s/r) pow 3`;;\r
 968 \r
 969 e (REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC);;\r
 970 \r
 971 e (ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]);;\r
 972 \r
 973 e (SUBGOAL_THEN `C INTER normball x s = IMAGE ((+) x) (IMAGE (scale (s/r % (vec 1)))(IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC);;\r
 974 \r
 975 e (ASM_SIMP_TAC[trans_strech_trans_radial]);;\r
 976 \r
 977 e (ASM_REWRITE_TAC[]);;\r
 978 \r
 979 e (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC);;\r
 980 \r
 981 e (ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]);;\r
 982 \r
 983 e (SUBGOAL_THEN `measurable (IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r))` ASSUME_TAC);;\r
 984 \r
 985 e (ASM_MESON_TAC[MEASURABLE_RULES]);;\r
 986 \r
 987 e (SUBGOAL_THEN `measurable (IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)))` ASSUME_TAC);;\r
 988 \r
 989 e (ASM_MESON_TAC[MEASURABLE_RULES]);;\r
 990 \r
 991 e (SUBGOAL_THEN `measurable (IMAGE ((+) x)\r
 992  (IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))))` ASSUME_TAC);;\r
 993 \r
 994 e (ASM_MESON_TAC[MEASURABLE_RULES]);;\r
 995 \r
 996 e (ABBREV_TAC `A2:real^3->bool= (IMAGE (scale (s / r % vec 1))\r
 997       (IMAGE ((+) (--x)) (C INTER normball x r)))`);;\r
 998 \r
 999 e (SUBGOAL_THEN `vol (IMAGE ((+) x) A2)=vol (A2)` MP_TAC);;\r
1000 \r
1001 e (UNDISCH_TAC `(volume_prop vol):bool`);;\r
1002 \r
1003 e (UNDISCH_TAC `(measurable (A2:real^3->bool)):bool`);;\r
1004 \r
1005 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
1006 \r
1007 e (SIMP_TAC[volume_prop]);;\r
1008 \r
1009 e (SIMP_TAC[]);;\r
1010 \r
1011 e (DISCH_TAC);;\r
1012 \r
1013 e (UNDISCH_TAC `(IMAGE (scale (s / r % vec 1))\r
1014       (IMAGE ((+) (--x)) (C INTER normball x r)):real^3->bool =\r
1015       A2):bool`);;\r
1016 \r
1017 e (REWRITE_TAC[SET_RULE `IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r)) =\r
1018  A2:real^3->bool <=> A2= IMAGE (scale (s / r % vec 1)) (IMAGE ((+) (--x)) (C INTER normball x r))`]);;\r
1019 \r
1020 e (SIMP_TAC[]);;\r
1021 \r
1022 e (DISCH_TAC);;\r
1023 \r
1024 \r
1025 e (ABBREV_TAC `M1:real^3->bool= (IMAGE ((+) (--x)) (C INTER normball x r))`);;\r
1026 \r
1027 e (ABBREV_TAC `w:real^3= s / r % vec 1`);;\r
1028 \r
1029 e (SUBGOAL_THEN `vol (IMAGE (scale (w:real^3)) M1)= abs (w$1*w$2*w$3)*vol (M1)` MP_TAC);;\r
1030 \r
1031 e (SUBGOAL_THEN `measurable (IMAGE (scale w) M1)` MP_TAC);;\r
1032 \r
1033 e (UNDISCH_TAC `(A2 = IMAGE (scale w) M1:real^3->bool):bool`);;\r
1034 \r
1035 e (REWRITE_TAC[SET_RULE `A2 = IMAGE (scale w) M1 <=> IMAGE (scale w) M1= A2`]);;\r
1036 \r
1037 e (SIMP_TAC[]);;\r
1038 \r
1039 e (ASM_MESON_TAC[]);;\r
1040 \r
1041 e (UNDISCH_TAC `(volume_prop vol):bool`);;\r
1042 \r
1043 e (UNDISCH_TAC `(measurable (M1:real^3->bool)):bool`);;\r
1044 \r
1045 e (REWRITE_TAC[TAUT `P1 ==> P2 ==> P3 ==> P4 <=> P1 /\ P2 /\ P3 ==> P4`]);;\r
1046 \r
1047 e (SIMP_TAC[volume_prop]);;\r
1048 \r
1049 e (SIMP_TAC[]);;\r
1050 \r
1051 e (DISCH_TAC);;\r
1052 \r
1053 e (SUBGOAL_THEN `((w:real^3)$1 = s/r)/\ (w$2 = s/r) /\ (w$3 = s/r)` MP_TAC);;\r
1054 \r
1055 e (REPEAT STRIP_TAC);;\r
1056 \r
1057 e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;\r
1058 \r
1059 e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;\r
1060 \r
1061 e (SIMP_TAC[]);;\r
1062 \r
1063 e (DISCH_TAC);;\r
1064 \r
1065 e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<=3`]);;\r
1066 \r
1067 e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=1 /\ 1<= 3`]);;\r
1068 \r
1069 e (ARITH_TAC);;\r
1070 \r
1071 e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;\r
1072 \r
1073 e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;\r
1074 \r
1075 e (SIMP_TAC[]);;\r
1076 \r
1077 e (DISCH_TAC);;\r
1078 \r
1079 e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<=3`]);;\r
1080 \r
1081 e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=2 /\ 2<= 3`]);;\r
1082 \r
1083 e (ARITH_TAC);;\r
1084 \r
1085 e (UNDISCH_TAC `(s / r % vec 1 = w:real^3):bool`);;\r
1086 \r
1087 e (REWRITE_TAC[VECTOR_ARITH `s / r % vec 1 = w:real^3 <=> w= s / r % vec 1`]);;\r
1088 \r
1089 e (SIMP_TAC[]);;\r
1090 \r
1091 e (DISCH_TAC);;\r
1092 \r
1093 e (SIMP_TAC[VECTOR_MUL_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<=3`]);;\r
1094 \r
1095 e (SIMP_TAC[VEC_COMPONENT;DIMINDEX_3;ARITH_RULE `1<=3 /\ 3<= 3`]);;\r
1096 \r
1097 e (ARITH_TAC);;\r
1098 \r
1099 e (SIMP_TAC[]);;\r
1100 \r
1101 e (REWRITE_TAC[ARITH_RULE `s / r * s / r * s / r= (s/r) pow 3`]);;\r
1102 \r
1103 e (DISCH_TAC);;\r
1104 \r
1105 e (SUBGOAL_THEN `s/r > &0` MP_TAC);;\r
1106 \r
1107 e (SUBGOAL_THEN `r> &0` MP_TAC);;\r
1108 \r
1109 e (UNDISCH_TAC `(s < r):bool` THEN UNDISCH_TAC `(s > &0):bool`);;\r
1110 \r
1111 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
1112 \r
1113 e (MESON_TAC[rduong]);;\r
1114 \r
1115 e (REWRITE_TAC[ARITH_RULE `(r> &0 <=> &0< r) /\ (s / r > &0 <=> &0 < s/r)`]);;\r
1116 \r
1117 e (SIMP_TAC[REAL_LT_RDIV_EQ]);;\r
1118 \r
1119 e (DISCH_TAC);;\r
1120 \r
1121 e (REWRITE_TAC[ARITH_RULE `&0*r= &0`]);;\r
1122 \r
1123 e (ASM_REWRITE_TAC[ARITH_RULE `&0< s<=> s> &0`]);;\r
1124 \r
1125 e (DISCH_TAC);;\r
1126 \r
1127 e (SUBGOAL_THEN `&0<= s/r` MP_TAC);;\r
1128 \r
1129 e (REWRITE_TAC[ARITH_RULE `&0 <= s / r <=> s/r >= &0`]);;\r
1130 \r
1131 e (UNDISCH_TAC `(s / r > &0):bool`);;\r
1132 \r
1133 e (ARITH_TAC);;\r
1134 \r
1135 e (DISCH_TAC);;\r
1136 \r
1137 e (SUBGOAL_THEN `&0<= (s / r) pow 3` MP_TAC);;\r
1138 \r
1139 e (UNDISCH_TAC `(&0<=s / r):bool`);;\r
1140 \r
1141 e (MP_TAC(ARITH_RULE `&0 <= &0`));;\r
1142 \r
1143 e (REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`]);;\r
1144 \r
1145 e (DISCH_TAC);;\r
1146 \r
1147 e (REWRITE_TAC[ARITH_RULE `&0<= (s/r) pow 3 <=> &0 pow 3<= (s/r) pow 3`]);;\r
1148 \r
1149 e (UNDISCH_TAC `(&0 <= &0 /\ &0 <= s / r):bool`);;\r
1150 \r
1151 e (MP_TAC(ARITH_RULE `~(3= 0)`));;\r
1152 \r
1153 e (REWRITE_TAC[TAUT `a==>b==>c <=> a/\b==>c`]);;\r
1154 \r
1155 e (SIMP_TAC[REAL_POW_LE2]);;\r
1156 \r
1157 e (DISCH_TAC);;\r
1158 \r
1159 e (SUBGOAL_THEN `abs ((s / r) pow 3)=(s / r) pow 3` MP_TAC);;\r
1160 \r
1161 e (SIMP_TAC[REAL_ABS_REFL]);;\r
1162 \r
1163 e (ASM_MESON_TAC[]);;\r
1164 \r
1165 e (SIMP_TAC[]);;\r
1166 \r
1167 e (DISCH_TAC);;\r
1168 \r
1169 e (REWRITE_TAC[ARITH_RULE `(s / r) pow 3 * vol M1= vol M1 * (s / r) pow 3`]);;\r
1170 \r
1171 e (SUBGOAL_THEN `vol M1= vol C` MP_TAC);;\r
1172 \r
1173 e (UNDISCH_TAC `(IMAGE ((+) (--x:real^3)) ((C:real^3->bool) INTER normball x r) = (M1:real^3->bool)):bool`);;\r
1174 \r
1175 e (REWRITE_TAC[SET_RULE `IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r) = M1 <=> M1= IMAGE ((+) (--x)) ((C:real^3->bool) INTER normball x r)`]);;\r
1176 \r
1177 e (SIMP_TAC[]);;\r
1178 \r
1179 e (DISCH_TAC);;\r
1180 \r
1181 e (SUBGOAL_THEN `vol (IMAGE ((+) (--x)) (C INTER normball x r))= vol (C INTER normball (x:real^3) r)` MP_TAC);;\r
1182 \r
1183 e (UNDISCH_TAC `(volume_prop vol):bool`);;\r
1184 \r
1185 e (UNDISCH_TAC `(measurable ((C:real^3->bool) INTER normball x r)):bool`);;\r
1186 \r
1187 e (REWRITE_TAC[TAUT `A==>B==>C <=> A/\B==>C`]);;\r
1188 \r
1189 e (SIMP_TAC[volume_prop]);;\r
1190 \r
1191 e (SIMP_TAC[]);;\r
1192 \r
1193 e (DISCH_TAC);;\r
1194 \r
1195 e (SUBGOAL_THEN `C INTER normball (x:real^3) r= C` MP_TAC);;\r
1196 \r
1197 e (UNDISCH_TAC `(radial_norm r (x:real^3) C):bool`);;\r
1198 \r
1199 e (REWRITE_TAC[radial_norm]);;\r
1200 \r
1201 e (REPEAT STRIP_TAC);;\r
1202 \r
1203 e (UNDISCH_TAC `((C:real^3->bool) SUBSET normball (x:real^3) r):bool`);;\r
1204 \r
1205 e (SIMP_TAC[SUBSET_INTER_ABSORPTION]);;\r
1206 \r
1207 e (DISCH_TAC);;\r
1208 \r
1209 e (ABBREV_TAC `(E:real^3->bool)= C INTER normball x r`);;\r
1210 \r
1211 e (ASM_MESON_TAC[]);;\r
1212 \r
1213 e (ABBREV_TAC `a:real= (s / r) pow 3`);;\r
1214 \r
1215 e (ABBREV_TAC `a1:real= vol M1` THEN ABBREV_TAC `a2:real= vol C`);;\r
1216 \r
1217 e (SIMP_TAC[]);;\r
1218 \r
1219 let lemma_r_r'=top_thm();; \r
1220 \r
1221 *)\r
1222 \r
1223 (*------------------------   Definition of Solid angle  ---------------------------------------------------------*)\r
1224 \r
1225 \r
1226 let normball_subset= prove(`!(x:real^3) r r'. (r'> &0) /\ (r'<r)==> normball x r' SUBSET normball x r`, (REPEAT GEN_TAC THEN REPEAT STRIP_TAC) THEN REWRITE_TAC[SUBSET] THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[normball] THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[dist] THEN UNDISCH_TAC `(r' < r):bool` THEN REWRITE_TAC[TAUT `a==>b ==> c <=> a /\ b ==> c`] THEN ARITH_TAC);;\r
1227 let subset_inter=prove(`! (A:real^3->bool) (B:real^3->bool). A SUBSET B ==> A INTER B= A`,REPEAT GEN_TAC THEN SET_TAC[]);;\r
1228 let normball_eq=prove(`!(C:real^3->bool) x r r'. (r'> &0)/\ (r'< r)==> (C INTER normball x r) INTER normball x r' = C INTER normball x r'`,REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN (MP_TAC(SET_RULE `((C:real^3->bool) INTER normball x r) INTER normball x r'=(C INTER normball x r') INTER normball x r`)) THEN SIMP_TAC[] THEN DISCH_TAC THEN (SUBGOAL_THEN `(((C:real^3->bool) INTER normball x r') SUBSET normball x r)` MP_TAC) THENL[ASM_MESON_TAC[INTER_SUBSET;SUBSET_TRANS;normball_subset];MESON_TAC[subset_inter]]);;\r
1229 \r
1230 (* redone by thales below on 2010-06-06 :\r
1231 \r
1232 let pre_def1_4_3=prove(`!(C:real^3->bool)(x:real^3). volume_prop_fix (vol) /\ measurable C /\ eventually_radial_norm x C ==> (?s. ?c. (c > &0) /\ (!r. (r > &0) /\ (r < c) ==> (s= &3 * vol(C INTER normball x r)/(r pow 3)))) `,\r
1233  (REPEAT GEN_TAC) \r
1234  THEN (REWRITE_TAC[eventually_radial_norm]) \r
1235  THEN (REPEAT STRIP_TAC) \r
1236  THEN (EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`)  \r
1237  THEN (EXISTS_TAC `(r:real)`)\r
1238  THEN (ASM_REWRITE_TAC[])\r
1239  THEN (GEN_TAC)\r
1240  THEN (REPEAT STRIP_TAC)\r
1241  THEN (REWRITE_TAC[REAL_ARITH `&3 * vol (C INTER normball x r) / r pow 3 = &3 * vol (C INTER normball x r') / r' pow 3 <=> vol (C INTER normball x r) / r pow 3 = vol (C INTER normball x r') / r' pow 3`])\r
1242  THEN (SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC)\r
1243  THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]] \r
1244  THEN DISCH_TAC\r
1245  THEN (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC)\r
1246  THENL[ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball];(SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC)]\r
1247  THENL[ASM_MESON_TAC[lemma_r_r'];ABBREV_TAC `(a:real)=vol (C INTER normball x r)`]\r
1248  THEN ABBREV_TAC `(b:real)=vol ((C INTER normball x r) INTER normball x r')`\r
1249  THEN SIMP_TAC[] \r
1250  THEN DISCH_TAC \r
1251  THEN SIMP_TAC[REAL_POW_DIV] \r
1252  THEN MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`)\r
1253  THEN ASM_REWRITE_TAC[] \r
1254  THEN DISCH_TAC \r
1255  THEN MP_TAC(MESON[REAL_POW_NZ] `~(r'= &0)==> ~(r' pow 3= &0)`)\r
1256  THEN ASM_REWRITE_TAC[] \r
1257  THEN DISCH_TAC \r
1258  THEN REWRITE_TAC[REAL_ARITH `(a * r' pow 3 / r pow 3) / r' pow 3= (a * r' pow 3/ r' pow 3)/ r pow 3`]\r
1259  THEN MP_TAC(MESON[REAL_DIV_REFL] `~(r' pow 3 = &0)==> r' pow 3 / r' pow 3= &1`) \r
1260  THEN ASM_REWRITE_TAC[] \r
1261  THEN SIMP_TAC[] \r
1262  THEN DISCH_TAC \r
1263  THEN ARITH_TAC);;  \r
1264 \r
1265 let pre_def_4_3=REWRITE_RULE[VOLUME_FIX] (prove(`?(s:(real^3->bool)->real^3 -> real). !C x. volume_prop_fix vol /\ measurable C /\ eventually_radial_norm x C ==> (?r'.r' > &0 /\(!r. r > &0 /\ r < r' ==> s C x = &3 * vol (C INTER normball x r) / r pow 3))`,MESON_TAC[SKOLEM_THM;pre_def1_4_3]));;\r
1266 \r
1267 let sol= new_specification ["sol"] pre_def_4_3;;\r
1268 \r
1269 *)\r
1270 \r
1271 \r
1272 let radial_normball = prove_by_refinement( `!r x C. \r
1273   radial_norm r (x:real^A) C ==> radial_norm r x (C INTER normball x r)`,\r
1274 [\r
1275   REWRITE_TAC[radial_norm];\r
1276    STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC;\r
1277 \r
1278   SUBGOAL_THEN `C SUBSET normball (x:real^A) r ==> (C INTER normball x r =C)` MP_TAC;\r
1279   SET_TAC[];\r
1280   MESON_TAC[];\r
1281 ]);;\r
1282 \r
1283 \r
1284 (* \r
1285 A big part of the proof is devoted to this identity \r
1286  `(b = a * (r'/r) pow 3 ) /\ (r > &0) /\ (r' > &0) ==> a / r pow 3 = b / r' pow 3`;; *)\r
1287 \r
1288 (*\r
1289 let pre_def1_4_3=prove_by_refinement(\r
1290 ` !(C:real^3->bool) x.\r
1291          volume_prop_fix vol /\\r
1292          (?r. r > &0 /\\r
1293               measurable (C INTER normball x r) /\\r
1294               radial_norm r x (C INTER normball x r))\r
1295          ==> (?s c.\r
1296                   c > &0 /\\r
1297                   (!r. r > &0 /\ r < c\r
1298                        ==> s = &3 * vol (C INTER normball x r) / r pow 3))`,\r
1299 [\r
1300  (REPEAT STRIP_TAC)  ;\r
1301  (EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`)   ;\r
1302  (EXISTS_TAC `(r:real)`) ;\r
1303  (ASM_REWRITE_TAC[]) ;\r
1304  (REPEAT STRIP_TAC) ;\r
1305  (REWRITE_TAC[REAL_ARITH `(&3 * x = &3 *y) = (x = y)`]) ;\r
1306  (SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]]  ;\r
1307  DISCH_TAC ;\r
1308 (*  (SUBGOAL_THEN `measurable ((C:real^3->bool) INTER normball x r)` ASSUME_TAC) THENL[ASM_MESON_TAC[MEASURABLE_RULES;measurable_normball]; *)\r
1309 (SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC);\r
1310  ASM_MESON_TAC[lemma_r_r';radial_normball];\r
1311  ABBREV_TAC `(a:real)=vol (C INTER normball x r)`;\r
1312  ABBREV_TAC `(b:real)=vol ((C INTER normball x r) INTER normball x r')` ;\r
1313  SIMP_TAC[]  ;\r
1314  DISCH_TAC  ;\r
1315  SIMP_TAC[REAL_POW_DIV]  ;\r
1316  MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`) ;\r
1317  ASM_REWRITE_TAC[]  ;\r
1318  DISCH_TAC  ;\r
1319  MP_TAC(MESON[REAL_POW_NZ] `~(r'= &0)==> ~(r' pow 3= &0)`) ;\r
1320  ASM_REWRITE_TAC[]  ;\r
1321  DISCH_TAC  ;\r
1322  REWRITE_TAC[REAL_ARITH `(a * r' pow 3 / r pow 3) / r' pow 3= (a * r' pow 3/ r' pow 3)/ r pow 3`] ;\r
1323  MP_TAC(MESON[REAL_DIV_REFL] `~(r' pow 3 = &0)==> r' pow 3 / r' pow 3= &1`)  ;\r
1324  ASM_REWRITE_TAC[]  ;\r
1325  SIMP_TAC[]  ;\r
1326  DISCH_TAC  ;\r
1327  ARITH_TAC;\r
1328 ]);;  \r
1329 *)\r
1330 \r
1331 (* \r
1332 A big part of the proof of pre_def1_4_3 is devoted to this identity \r
1333 *)\r
1334 \r
1335 let pow3_identity = prove_by_refinement(\r
1336   `(b = a * (r'/r) pow 3 ) /\ (r > &0) /\ (r' > &0) ==> a / r pow 3 = b / r' pow 3`,\r
1337   [\r
1338  SIMP_TAC[REAL_POW_DIV]  ;\r
1339  MP_TAC(REAL_ARITH `r'> &0 ==> ~(r'= &0)`) ;\r
1340  MP_TAC(MESON[REAL_POW_NZ;REAL_DIV_REFL] `~(r'= &0)==> r' pow 3 / r' pow 3= &1`) ;\r
1341  REWRITE_TAC[REAL_ARITH `(a * b / c) / b= (a * b/ b)/ c`] ;\r
1342  SIMP_TAC[]  ;\r
1343  ARITH_TAC;\r
1344   ]);;\r
1345 (*\r
1346 let pre_def1_4_3=prove_by_refinement(\r
1347 ` !(C:real^3->bool) x.\r
1348          volume_prop_fix vol /\\r
1349          (?r. r > &0 /\\r
1350               measurable (C INTER normball x r) /\\r
1351               radial_norm r x (C INTER normball x r))\r
1352          ==> (?s c.\r
1353                   c > &0 /\\r
1354                   (!r. r > &0 /\ r < c\r
1355                        ==> s = &3 * vol (C INTER normball x r) / r pow 3))`,\r
1356 [\r
1357  (REPEAT STRIP_TAC)  ;\r
1358  (EXISTS_TAC `(&3* vol (C INTER normball x r) / r pow 3):real`)   ;\r
1359  (EXISTS_TAC `(r:real)`) ;\r
1360  (ASM_REWRITE_TAC[]) ;\r
1361  (REPEAT STRIP_TAC) ;\r
1362  (REWRITE_TAC[REAL_ARITH `(&3 * x = &3 *y) = (x = y)`]) ;\r
1363  (SUBGOAL_THEN `(C:real^3->bool) INTER normball x r'= (C INTER normball x r) INTER normball x r'` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]]  ;\r
1364  DISCH_TAC ;\r
1365  (SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x r')= vol (C INTER normball x r) * (r'/r) pow 3` MP_TAC);\r
1366  ASM_MESON_TAC[lemma_r_r';radial_normball];\r
1367   DISCH_TAC THEN ASM_REWRITE_TAC[];\r
1368 ASM_MESON_TAC[pow3_identity];\r
1369 ]);;\r
1370 *)\r
1371 \r
1372 let pre_def1_4_3b=prove_by_refinement(\r
1373 ` !x (C:real^3->bool). volume_prop_fix vol ==> ?s. !r. \r
1374          (( r > &0 /\\r
1375               measurable (C INTER normball x r) /\\r
1376               radial_norm r x (C INTER normball x r))\r
1377          ==> (s = &3 * vol (C INTER normball x r) / r pow 3))`,\r
1378 [\r
1379  (REPEAT STRIP_TAC)  ;\r
1380  (DISJ_CASES_TAC (ISPEC `?t. (t > &0) /\ measurable (C INTER normball (x:real^3) t) /\ (radial_norm t x (C INTER normball x t))`   (TAUT `!x. ~x \/ x`))); \r
1381   ASM_MESON_TAC[];\r
1382  (FIRST_X_ASSUM MP_TAC);\r
1383  STRIP_TAC;\r
1384  (EXISTS_TAC `(&3* vol (C INTER normball x t) / t pow 3):real`)   ;\r
1385  (REPEAT STRIP_TAC) ;\r
1386  (REWRITE_TAC[REAL_ARITH `(&3 * x = &3 *y) = (x = y)`]) ;\r
1387 (* to here *)\r
1388   DISJ_CASES_TAC (ARITH_RULE `(t < r) \/ (r < t) \/ (r = t)`);\r
1389  (SUBGOAL_THEN `(C:real^3->bool) INTER normball x t= (C INTER normball x r) INTER normball x t` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]]  ;\r
1390  DISCH_TAC ;\r
1391  (SUBGOAL_THEN `vol ((C INTER normball x r) INTER normball x t)= vol (C INTER normball x r) * (t/r) pow 3` MP_TAC);\r
1392  ASM_MESON_TAC[lemma_r_r';radial_normball];\r
1393   DISCH_TAC THEN ASM_REWRITE_TAC[];\r
1394 ASM_MESON_TAC[pow3_identity];\r
1395   FIRST_X_ASSUM DISJ_CASES_TAC;\r
1396  (SUBGOAL_THEN `(C:real^3->bool) INTER normball x r= (C INTER normball x t) INTER normball x r` MP_TAC) THENL[ASM_MESON_TAC[normball_eq];SIMP_TAC[]]  ;\r
1397  DISCH_TAC ;\r
1398  (SUBGOAL_THEN `vol ((C INTER normball x t) INTER normball x r)= vol (C INTER normball x t) * (r/t) pow 3` MP_TAC);\r
1399  ASM_MESON_TAC[lemma_r_r';radial_normball];\r
1400   DISCH_TAC THEN ASM_REWRITE_TAC[];\r
1401 ASM_MESON_TAC[pow3_identity];\r
1402  ASM_REWRITE_TAC[];\r
1403 ]);;\r
1404 \r
1405 (*\r
1406 let pre_def_4_3=REWRITE_RULE[VOLUME_FIX] (prove(`?(s:(real^3->bool)->real^3 -> real). !C x. (?r. (r > &0) /\  measurable (C INTER normball x r)  /\ radial_norm r x (C INTER normball x r)) ==> (?r'.r' > &0 /\(!r. r > &0 /\ r < r' ==> s C x = &3 * vol (C INTER normball x r) / r pow 3))`,MESON_TAC[VOLUME_FIX;SKOLEM_THM;pre_def1_4_3]));;\r
1407 *)\r
1408 \r
1409 let pre_def_4_3b=REWRITE_RULE[VOLUME_FIX;SKOLEM_THM]\r
1410  pre_def1_4_3b;;\r
1411 \r
1412 let pre_def_4_3b_alt = prove_by_refinement(\r
1413   `?s. !(x:real^3) C r.\r
1414              r > &0 /\\r
1415              measurable (C INTER ball (x, r)) /\\r
1416              radial r x (C INTER ball (x, r))\r
1417              ==> s x C = &3 * vol (C INTER ball(x,r)) / r pow 3`,\r
1418   (* {{{ proof *)\r
1419   [\r
1420   REWRITE_TAC[GSYM NORMBALL_BALL;GSYM radial_norm_deprecated;pre_def_4_3b]\r
1421   ]);;\r
1422   (* }}} *)\r
1423 \r
1424 (*\r
1425 let sol= new_specification ["sol"] pre_def_4_3b;;\r
1426 *)\r
1427 \r
1428 let sol_spec = new_specification ["sol"] pre_def_4_3b_alt;;\r
1429 \r
1430 let sol = prove_by_refinement(\r
1431   `!(x:real^3) C r.\r
1432          r > &0 /\\r
1433          measurable (C INTER normball x r) /\\r
1434          radial_norm r x (C INTER normball x r)\r
1435          ==> sol x C = &3 * vol (C INTER normball x r) / r pow 3`,\r
1436   (* {{{ proof *)\r
1437   [\r
1438   REWRITE_TAC[NORMBALL_BALL;radial_norm_deprecated];\r
1439   REPEAT STRIP_TAC;\r
1440   ASM_MESON_TAC[sol_spec]\r
1441   ]);;\r
1442   (* }}} *)\r
1443 \r
1444 let AFF_GT_1_3=prove(`!x u v w.\r
1445          DISJOINT {x} {u, v, w}\r
1446          ==> aff_gt {x} {u, v, w} =\r
1447              {y | ?t1 t2 t3 t4.\r
1448                       &0 < t2 /\ \r
1449                       &0 < t3 /\\r
1450                       &0 < t4 /\\r
1451                       t1 + t2 + t3 +t4= &1 /\\r
1452                       y = t1 % x + t2 %u + t3 % v + t4 % w}`,\r
1453 AFF_TAC);;\r
1454 \r
1455 \r
1456 \r
1457 let aff_normball =prove_by_refinement\r
1458 (`!t (x:real^B) u r.  (r > &0) /\ (t > &0) /\ (t  * norm u < r) /\ (x + u IN normball x r) ==> (x + t % u IN normball x r)`,\r
1459 [\r
1460 REWRITE_TAC[normball;IN_ELIM_THM;dist;\r
1461   VECTOR_ARITH `((x:real^B) + u ) - x = u`;NORM_MUL];\r
1462 REAL_ARITH_TAC;\r
1463 ]);;\r
1464 \r
1465 \r
1466 (* insert in vol1.hl after solid angle *)\r
1467 \r
1468 let aff_gt_radial = prove_by_refinement(`!x u v w r.\r
1469      (DISJOINT {(x:real^B)} {u,v,w} /\ (r > &0) ) ==>\r
1470      radial_norm r x (aff_gt {x} {u,v,w} INTER normball x r)`,\r
1471 [\r
1472 REWRITE_TAC[radial_norm];\r
1473 REPEAT STRIP_TAC;\r
1474 SET_TAC[];\r
1475 UNDISCH_TAC `(x:real^B) + u' IN aff_gt {x} {u, v, w} INTER normball x r`;\r
1476 ASM_SIMP_TAC[AFF_GT_1_3];\r
1477 REWRITE_TAC[IN_ELIM_THM;IN_INTER];\r
1478 REPEAT STRIP_TAC;\r
1479 EXISTS_TAC `&1 + (t:real) * t1 - t`;\r
1480 EXISTS_TAC `(t:real) * t2`;\r
1481 EXISTS_TAC `(t:real) * t3`;\r
1482 EXISTS_TAC `(t:real) * t4`;\r
1483 SUBGOAL_THEN `&0 < t * t2 /\ &0 < t * t3 /\ &0 < t * t4` (fun t -> REWRITE_TAC[t]);\r
1484 ASM_MESON_TAC[REAL_MUL_POS_LT;REAL_ARITH `r > &0 <=> &0 < r`];\r
1485 CONJ_TAC;\r
1486 SUBGOAL_THEN `(&1 + t * t1 - t) + t * t2 + t * t3 + t * t4 = &1 - t + t * (t1 + t2 + t3 + t4)` (fun t-> ASM_REWRITE_TAC[t]);\r
1487 REAL_ARITH_TAC;\r
1488 REAL_ARITH_TAC;\r
1489 ONCE_REWRITE_TAC[ VECTOR_ARITH `( &1 + t * t1 - t) % (x:real^B) + (t * t2) % u + (t * t3) % v + (t * t4) % w  = x - t % x + t % (t1 % x + t2 % u + t3 % v + t4 % w)`];\r
1490 UNDISCH_TAC `(x:real^B) + u' = t1 % x + t2 % u + t3 % v + t4 % w`;\r
1491 DISCH_THEN(fun thm -> ONCE_REWRITE_TAC[GSYM thm]);\r
1492 VECTOR_ARITH_TAC;\r
1493 MATCH_MP_TAC aff_normball;\r
1494 ASM_REWRITE_TAC[];\r
1495 ]);;\r
1496 \r
1497 \r
1498 (*---------------------------------------------------------------------------------------------------------------*)\r
1499 \r
1500 \r
1501 \r
1502 (*Lemma 4.3*)\r
1503 \r
1504 \r
1505 let tr5=prove(`!r v0 C C'.(radial_norm r v0 C /\ radial_norm r v0 C' ==> (!u. ((v0+u) IN (C INTER C')) ==> (!t.(t > &0) /\ (t * norm u < r)==> (v0+t % u IN (C INTER C')))))`, REPEAT GEN_TAC THEN REWRITE_TAC[IN_INTER] THEN MESON_TAC[radial_norm;IN_INTER]);;\r
1506 let tr6=prove(`!r v0 C C'.(radial_norm r v0 C /\ radial_norm r v0 C' ==> C INTER C' SUBSET normball v0 r)`, REPEAT GEN_TAC THEN MESON_TAC[radial_norm;INTER_SUBSET;SUBSET_TRANS]);;\r
1507 \r
1508 let inter_radial =prove(`!r v0 C C'.(radial_norm r v0 C /\ radial_norm r v0 C') ==> radial_norm r v0 (C INTER C')`, REPEAT GEN_TAC THEN MESON_TAC[radial_norm;tr5;tr6]);; \r
1509 \r
1510 \r
1511 (*4.2.11 combining solid angle and volume*)\r
1512 \r
1513 (* removed by thales, nov 11, 2008.  Conflicts with definition of phi already provided *)\r
1514 \r
1515 (*\r
1516 let phi=new_definition `phi(h:real,t:real,l:real^2)= l$1*t*h*(t+h)/ &6 + l$2`;;\r
1517 let A=new_definition `A(h:real,t:real,l:real^2)=(&1-h/t)*(phi (h,t,l)-phi (t,t,l))`;;\r
1518 \r
1519 *)\r
1520 \r
1521 \r
1522 (*-------------------------------------------------------------------------------------*)\r
1523 (*                                        Finiteness                                   *)\r
1524 (*-------------------------------------------------------------------------------------*)\r
1525 \r
1526 \r
1527 (*------------------------------------------------------*)\r
1528 (*            Useful definitions                        *)\r
1529 (*------------------------------------------------------*)\r
1530 \r
1531 let cube= new_definition `cube (x:real^3)= {y:real^3 | !i. (1<= i)/\ (i<= 3) ==> ( x$i < y$i ) /\ ( y$i < x$i + &1)}`;; \r
1532 \r
1533 \r
1534 \r
1535 (*\r
1536 let hinhcau=new_definition `hinhcau (x:real^3) (r:real)={y: real^3 | norm ( x - y ) < r } `;;\r
1537 *)\r
1538 \r
1539 let hinhcau_deprecated = new_definition `hinhcau (x:real^A) r = ball (x,r)`;;\r
1540 \r
1541 let hinhcau = prove_by_refinement(\r
1542   ` !(x:real^A) r. hinhcau x r = {y | norm (x - y) < r}`,\r
1543   (* {{{ proof *)\r
1544   [\r
1545   REWRITE_TAC[EXTENSION;IN_ELIM_THM;hinhcau_deprecated;ball;IN_ELIM_THM;dist]\r
1546   ]);;\r
1547   (* }}} *)\r
1548 \r
1549 \r
1550 let set_of_cube= new_definition`set_of_cube S= {cube x| x IN S}`;;\r
1551 \r
1552 let union_of_cube= new_definition `union_of_cube (x:real^3) (r:real)= UNIONS (set_of_cube (hinhcau x r))`;;\r
1553 \r
1554 let int_ball= new_definition `int_ball (x:real^3) r= { y :real^3 | !i. (1<= i) /\ (i<= 3) ==> integer (y$i)} INTER (hinhcau x r)`;;\r
1555 let union_of_int_cube=new_definition `union_of_int_cube (x:real^3) (r:real) = UNIONS (set_of_cube (int_ball x r))`;;\r
1556 \r
1557 (*\r
1558 let map0=new_definition `map0 = \(c:real^3). cube c`;;\r
1559 *)\r
1560 \r
1561 (*\r
1562 let map0 = new_definition `map0 = cube`;;\r
1563 *)\r
1564 \r
1565 (*-------------------------------------------------------*)\r
1566 (*                 Somes lemmas                          *)\r
1567 (*-------------------------------------------------------*)\r
1568 \r
1569 let COMPONENT_LE_NORM_3=prove(`!(x:real^3) i. (1<= i) /\ (i<= 3) ==> abs (x$i)<= norm x`,MESON_TAC[COMPONENT_LE_NORM;DIMINDEX_3]);;\r
1570 \r
1571 \r
1572 let component_hinhcau_bound=prove(`! (p:real^3) (r:real) x. x IN hinhcau p r ==> (!i. (1 <= i) /\ ( i <= 3 ) ==> ( p$i - r <= x$i ) /\ ( x$i <= p$i + r))`,REPEAT GEN_TAC THEN REWRITE_TAC[hinhcau] THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH `(p$i):real - r <= x$i <=> p$i - x$i <= r`; REAL_ARITH `a:real <= b+c <=> -- c <= b-a`] THEN REWRITE_TAC[MESON[] `C/\B <=> B/\ C`] THEN REWRITE_TAC[GSYM REAL_ABS_BOUNDS] THEN  REWRITE_TAC[MESON[] `C/\B <=> B/\ C`] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`p - x:real^3`; `i:num`] COMPONENT_LE_NORM_3) THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(norm (p:real^3 - x) < r):bool` THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN REAL_ARITH_TAC);;\r
1573 \r
1574 let int_interval= new_definition `int_interval (a:real) b = {x:real | integer x /\  (a<= x) /\ (x <= b)}`;;\r
1575 \r
1576 let finite_int_interval=prove(`! a:real b. FINITE (int_interval a b)`,REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[FINITE_INTSEG] THEN  REWRITE_TAC[int_interval] THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[FINITE_INTSEG]);;\r
1577 \r
1578 (*\r
1579 let finite_int_interval=prove(`! a:real b. FINITE (int_interval a b)`,REPEAT GEN_TAC THEN ASSUME_TAC (GSYM INTEGER_IS_INT) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[INTEGER_IS_INT;FINITE_INTSEG] THEN  REWRITE_TAC[int_interval] THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[FINITE_INTSEG]);;\r
1580 *)\r
1581 \r
1582 let vector_to_pair =new_definition`vector_to_pair (x:real^3) = x$1, x$2, x$3 `;;\r
1583 \r
1584 let lm1=prove(`!(x:real^3) (r:real) y. y IN int_ball x r ==> (!i. 1<=i /\i<= 3 ==> y$i IN int_interval (x$i - r) (x$i + r) )`,REPEAT GEN_TAC\r
1585                 THEN REWRITE_TAC[int_ball;IN_ELIM_THM] THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REWRITE_TAC[int_interval;IN_ELIM_THM] THEN MESON_TAC[component_hinhcau_bound]);;\r
1586 \r
1587 \r
1588 let lm2 =prove(`! (x:real^3) (r:real) y.   y IN (int_ball x r) ==> vector_to_pair y IN (int_interval (x$1 - r)  (x$1 + r) CROSS (int_interval (x$2 - r)  (x$2 + r)) CROSS (int_interval (x$3 - r)  (x$3 + r)))`,REPEAT GEN_TAC THEN REWRITE_TAC[IN_CROSS;vector_to_pair] THEN MESON_TAC[ARITH_RULE `1<=i /\ i<=3 <=> i=1\/ i=2 \/ i=3`;lm1]);;\r
1589 \r
1590 let vector_eq1=prove(`! (x:real^3) y. x= y <=> x - y= vec 0`,REPEAT GEN_TAC THEN VECTOR_ARITH_TAC);;\r
1591 \r
1592 let trip_eq=prove(`! (x:real^3) (y:real^3). x$1, x$2, x$3= y$1,y$2,y$3 <=> !i. 1<= i /\ i<=3 ==> x$i= y$i  `,REPEAT GEN_TAC THEN REWRITE_TAC[PAIR_EQ] THEN REWRITE_TAC[ARITH_RULE `1<=i /\ i<= 3 <=> i=1 \/ i=2 \/ i=3`] THEN MESON_TAC[]);;\r
1593 \r
1594 let int_ball_subset_CROSS=prove(`! (x:real^3) (r:real). INJ vector_to_pair (int_ball x r) (int_interval (x$1 - r)  (x$1 + r) CROSS (int_interval (x$2 - r)  (x$2 + r)) CROSS (int_interval (x$3 - r)  (x$3 + r)))`,REPEAT GEN_TAC THEN REWRITE_TAC[INJ] THEN REWRITE_TAC[lm2] THEN REWRITE_TAC[vector_to_pair] THEN REPEAT GEN_TAC THEN REWRITE_TAC[CART_EQ;DIMINDEX_3;trip_eq] THEN MESON_TAC[]);;\r
1595 \r
1596 \r
1597 let FINITE_IMAGE_INJ=prove(`! (h:real^3->B) (s:real^3 ->bool) t. (!(x:real^3). x IN s ==> h x IN t) /\ INJ h s t /\ FINITE t ==> FINITE s`,\r
1598 REPEAT GEN_TAC THEN REWRITE_TAC[INJ] THEN SIMP_TAC[MESON[] `p /\ (p /\ q) /\ w <=> p /\ q /\ w`] THEN STRIP_TAC\r
1599   THEN SUBGOAL_THEN `s= { x:real^3 | x IN s /\ (h:real^3->B) x IN t}` ASSUME_TAC\r
1600 THENL [REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];ASM_MESON_TAC[FINITE_IMAGE_INJ_GENERAL]]\r
1601        THEN REWRITE_TAC[SET_RULE `{x | x IN s /\ (h:real^3->B) x IN t} SUBSET s`] THEN REWRITE_TAC[SUBSET] THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_SIMP_TAC[]);;\r
1602 \r
1603 let finite_cross_int_interval=prove(`!(x:real^3) (r:real). FINITE (int_interval (x$1 - r)  (x$1 + r) CROSS (int_interval (x$2 - r)  (x$2 + r)) CROSS (int_interval (x$3 - r)  (x$3 + r)))`,REPEAT GEN_TAC THEN MESON_TAC[finite_int_interval;FINITE_CROSS]);;\r
1604 \r
1605 (*----------------------------------------------------------*)\r
1606 (*        Finiteness of integer points in a ball            *)\r
1607 (*----------------------------------------------------------*)\r
1608 \r
1609 \r
1610 let finite_int_ball=prove(`!(x:real^3) (r:real). FINITE (int_ball x r)`,REPEAT GEN_TAC THEN MATCH_MP_TAC(ISPECL [`vector_to_pair: real^3 -> real#real#real`; `(int_ball (x:real^3) (r:real)):real^3 -> bool`; `(int_interval ((x:real^3)$1 - r:real)  (x$1 + r) CROSS (int_interval (x$2 - r)  (x$2 + r)) CROSS (int_interval (x$3 - r)  (x$3 + r))):real#real#real -> bool`] FINITE_IMAGE_INJ) THEN SIMP_TAC[SPECL [`x:real^3`;`r:real`;`x':real^3`] lm2;finite_cross_int_interval;int_ball_subset_CROSS]);;\r
1611 \r
1612 (*----------------------------------------------------------*)\r
1613 (*                      Needed lemmas                       *)\r
1614 (*----------------------------------------------------------*)\r
1615 \r
1616 let disjoint_line_interval=prove(`!(x:real) (y:real). integer x /\ integer y /\ (? (z:real). x< z /\ z< x+ &1 /\ y<z /\ z< y+ &1) ==> x= y`,\r
1617 (*\r
1618 REPEAT GEN_TAC THEN SIMP_TAC[GSYM INTEGER_IS_INT] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`;`y:real`] REAL_LE_CASES_INTEGERS)\r
1619 -- 2/16/2011. *)\r
1620 REPEAT GEN_TAC THEN SIMP_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`;`y:real`] REAL_LE_CASES_INTEGERS)\r
1621   THEN ASM_SIMP_TAC[] THEN ASM_SIMP_TAC[SPECL [`x:real`;`y:real`] REAL_LE_INTEGERS] THEN SIMP_TAC[MESON[] `(((P\/Q)\/R ==> P) <=> (Q\/R ==> P))`]\r
1622   THEN STRIP_TAC\r
1623 THENL [UNDISCH_TAC `(y:real <z):bool` THEN UNDISCH_TAC `(z:real< x+ &1):bool`;UNDISCH_TAC `(x:real <z):bool` THEN UNDISCH_TAC `(z:real< y+ &1):bool`]\r
1624 THENL [REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P  ==> R`] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH ` (y:real) < z /\ (z:real) < x+ &1   ==> y< x+ &1 `);REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P  ==> R`] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH ` (x:real) < z /\ (z:real) < y+ &1   ==> x< y+ &1 `)]\r
1625 THENL [ASM_SIMP_TAC[];ASM_SIMP_TAC[]]\r
1626 THENL [UNDISCH_TAC `(x + &1 <= y:real):bool` THEN REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P  ==> R`];UNDISCH_TAC `(y + &1 <= x:real):bool` THEN REWRITE_TAC[MESON[] `P ==> Q ==> R <=> Q /\ P  ==> R`]]\r
1627 THENL [MESON_TAC[REAL_ARITH `a:real < b /\ b<= a ==> F`];MESON_TAC[REAL_ARITH `a:real < b /\ b<= a ==> F`]]);;\r
1628 \r
1629 let vector_eq2=prove(`!(x:real^3) (y:real^3). (!i. 1 <= i /\ i <= 3 ==> x$i = y$i) ==> x = y `,SIMP_TAC[CART_EQ;DIMINDEX_3]);;\r
1630 \r
1631 let nonempty_cube=prove(`!(x:real^3). ~ (cube x= {})`,GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]\r
1632                           THEN EXISTS_TAC `(lambda i. (x:real^3)$i + &1/ &2):real^3` \r
1633 THEN REWRITE_TAC[cube;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN REAL_ARITH_TAC);;\r
1634 \r
1635 \r
1636 let disjoint_cube=prove(`!(x:real^3) (y:real^3).(!i. 1<=i /\ i<=3 ==> integer (x$i) /\ integer (y$i))\r
1637  ==> ( ~(DISJOINT (cube x) (cube y)) <=> x = y)`, REPEAT STRIP_TAC THEN EQ_TAC\r
1638 THENL [REWRITE_TAC[DISJOINT;SET_RULE `~ ((B:real^3 -> bool)= {}) <=> ?(x:real^3). x IN B`];SIMP_TAC[]]\r
1639 THENL [DISCH_TAC THEN FIRST_X_ASSUM(CHOOSE_TAC);REWRITE_TAC[DISJOINT]]\r
1640 THENL [UNDISCH_TAC `(x' IN cube (x:real^3) INTER cube y):bool`;SIMP_TAC[INTER_ACI;nonempty_cube]]\r
1641        THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM;cube] THEN \r
1642 UNDISCH_TAC `(!i. 1 <= i /\ i <= 3 ==> integer ((x:real^3)$i) /\ integer ((y:real^3)$i)):bool`\r
1643          THEN SIMP_TAC[FORALL_3] THEN REWRITE_TAC[MESON[] `P ==> Q ==> R <=> P /\ Q  ==> R`]\r
1644          THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC (SPECL [`x:real^3`;`y:real^3`] vector_eq2)\r
1645          THEN REWRITE_TAC[FORALL_3] THEN ASM_MESON_TAC[disjoint_line_interval]);;\r
1646 \r
1647 \r
1648 (*-----------------------------------------------------------*)\r
1649 (*      Bijectivity of map from int_ball to set_of_cube      *)\r
1650 (*-----------------------------------------------------------*)\r
1651 \r
1652 \r
1653 let inj_cube= prove_by_refinement(\r
1654   `! (x:real^3) (r:real). INJ cube (int_ball x r) (set_of_cube (int_ball x r))`,\r
1655  [\r
1656                    REWRITE_TAC[INJ;set_of_cube];\r
1657                    SIMP_TAC[SET_RULE `(x':real^3) IN int_ball x r ==> cube x' IN {cube x' | x' IN int_ball x r}`];\r
1658                      REPEAT GEN_TAC;\r
1659                      REWRITE_TAC[int_ball];\r
1660                      REWRITE_TAC[IN_INTER;IN_ELIM_THM];\r
1661                      REPEAT STRIP_TAC;\r
1662                      ASM_SIMP_TAC[GSYM (SPECL [`x':real^3`;`y:real^3`] disjoint_cube)];\r
1663                      BY(ASM_REWRITE_TAC[DISJOINT;INTER_ACI;nonempty_cube]);\r
1664  ]);;\r
1665 \r
1666 let surj_cube= prove_by_refinement(\r
1667    `! (x:real^3) (r:real). SURJ cube (int_ball x r) (set_of_cube (int_ball x r))`,\r
1668    [\r
1669         REWRITE_TAC[SURJ]; \r
1670      REWRITE_TAC[set_of_cube] ;\r
1671      SIMP_TAC[SET_RULE `x' IN int_ball x r ==> cube x' IN {cube x' | x' IN int_ball x r}`]; \r
1672      REPEAT GEN_TAC; \r
1673      REWRITE_TAC[IN_ELIM_THM]; DISCH_TAC; FIRST_X_ASSUM CHOOSE_TAC\r
1674  ; EXISTS_TAC `x'':real^3`; ASM_MESON_TAC[]\r
1675    ]);;\r
1676 \r
1677 \r
1678 let bij_cube=prove(`! (x:real^3) (r:real). BIJ cube (int_ball x r) (set_of_cube (int_ball x r))`,\r
1679 MESON_TAC[BIJ;inj_cube;surj_cube]);;\r
1680 \r
1681 \r
1682 (*-----------------------------------------------------------*)\r
1683 \r
1684 let surj2_cube=  prove_by_refinement(\r
1685   `!(x:real^3) (r:real). IMAGE cube (int_ball x r) = set_of_cube (int_ball x r)`,\r
1686   [REWRITE_TAC[IMAGE] THEN REWRITE_TAC[] THEN REWRITE_TAC[set_of_cube] THEN SIMP_TAC[EXTENSION] \r
1687 THEN REWRITE_TAC[IN_ELIM_THM] THEN SIMP_TAC[GSYM EXTENSION]]);;\r
1688 \r
1689 \r
1690 \r
1691 let int_ball_card_eq=prove(`!(x:real^3) (r:real). CARD (int_ball x r)= CARD (set_of_cube (int_ball x r))`,\r
1692 REPEAT GEN_TAC THEN SIMP_TAC[GSYM (SPECL [`X:real^3`;`r:real` ] surj2_cube)]\r
1693   THEN MP_TAC(SPECL [`x:real^3`;`r:real`] finite_int_ball) THEN MP_TAC(SPECL [`x:real^3`;`r:real`] inj_cube)\r
1694   THEN REWRITE_TAC[MESON[] `a==>b==>c <=> a/\ b ==>c`;INJ] \r
1695   THEN SIMP_TAC[set_of_cube;cube;SET_RULE `x' IN int_ball x r ==> cube x' IN {cube x' | x' IN int_ball x r}`]\r
1696   THEN REWRITE_TAC[MESON[cube] `cube (x':real^3)= cube x'`;GSYM cube]\r
1697   THEN MESON_TAC[ISPECL [`cube:real^3 -> real^3 -> bool`;`(int_ball x r):real^3 -> bool`] CARD_IMAGE_INJ]);;\r
1698 \r
1699 \r
1700 \r
1701 let cube_eq_interval=prove(`!(x:real^3). cube x= interval(x,x+ lambda i. &1)`,\r
1702 GEN_TAC THEN REWRITE_TAC[EXTENSION;cube;interval;DIMINDEX_3] THEN SIMP_TAC[IN_ELIM_THM;LAMBDA_BETA;DIMINDEX_3]\r
1703   THEN SIMP_TAC[VECTOR_ADD_COMPONENT;LAMBDA_BETA;DIMINDEX_3]);;\r
1704 \r
1705 let measurable_cube=prove( `!(x:real^3). measurable (cube x)`,REWRITE_TAC[cube_eq_interval;MEASURABLE_INTERVAL]);;\r
1706 \r
1707 let finite_set_of_cube=prove(`!(x:real^3)(r:real). FINITE (set_of_cube (int_ball x r))`,\r
1708 MESON_TAC[ISPECL [`cube:real^3 -> real^3 -> bool`; `(int_ball x r):real^3 -> bool`] FINITE_IMAGE;finite_int_ball;surj2_cube]);;\r
1709 \r
1710 let MEASURABLE_UNIONS2 = prove\r
1711  (`!f:(real^N->bool)->bool.\r
1712         FINITE f /\ (!s. s IN f ==> measurable s)\r
1713         ==> measurable (UNIONS f)`,\r
1714 (*    GEN_TAC THEN *)REWRITE_TAC[IMP_CONJ] THEN\r
1715   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN\r
1716   SIMP_TAC[UNIONS_0; UNIONS_INSERT; MEASURABLE_EMPTY] THEN\r
1717   REWRITE_TAC[IN_INSERT] THEN REPEAT STRIP_TAC THEN\r
1718   MATCH_MP_TAC MEASURABLE_UNION THEN ASM_SIMP_TAC[]);;\r
1719 \r
1720 let measurable_unions_cube=prove( `!(x:real^3)(r:real). measurable (UNIONS (set_of_cube (int_ball x r)))`,\r
1721 REPEAT GEN_TAC THEN MATCH_MP_TAC(ISPEC `set_of_cube (int_ball x r):(real^3 -> bool) -> bool` MEASURABLE_UNIONS2) THEN REWRITE_TAC[finite_set_of_cube] THEN REWRITE_TAC[set_of_cube;IN_ELIM_THM] THEN MESON_TAC[measurable_cube]);;\r
1722 \r
1723 let non_empty_cinterval=prove(`!(x:real^3). ~ (interval[x,x+ (lambda i. &1)]= {})`,\r
1724 GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN EXISTS_TAC `(lambda i. ((x:real^3)$i+ &1/ &2)):real^3`\r
1725   THEN REWRITE_TAC[interval;IN_ELIM_THM;LAMBDA_BETA;DIMINDEX_3]\r
1726   THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[VECTOR_ADD_COMPONENT;LAMBDA_BETA;DIMINDEX_3]\r
1727   THEN REAL_ARITH_TAC);;\r
1728 \r
1729 (* in line 997 changed t to emoi, esusick 11/12 *)\r
1730 let product_3=prove(`!(f:num -> real). product (1..3) f= f 1 * f 2 * f 3 `, let emoi= CONJUNCT2 PRODUCT_CLAUSES in \r
1731 GEN_TAC THEN MP_TAC(GSYM (SPECL [`1:num`;`3:num`] NUMSEG_RREC)) \r
1732   THEN SIMP_TAC[ARITH_RULE `1<= 3`;ARITH_RULE `3-1 = 2`] \r
1733   THEN REPEAT DISCH_TAC\r
1734   THEN MP_TAC(ISPECL [`3:num`;`f:num -> real`;`((1..2)):num ->bool`] emoi)\r
1735   THEN SIMP_TAC[MESON[NUMSEG_RREC;FINITE_NUMSEG] `FINITE (1..2)`]\r
1736   THEN SIMP_TAC[MESON[IN_NUMSEG;ARITH_RULE `~ (3<=2)`] ` ~( 3 IN (1..2))`] \r
1737   THEN DISCH_TAC \r
1738   THEN MP_TAC(GSYM (SPECL [`1:num`;`2:num`] NUMSEG_RREC)) \r
1739   THEN SIMP_TAC[ARITH_RULE `1<=2`;ARITH_RULE `2-1=1`] \r
1740   THEN MP_TAC(ISPECL [`2:num`;`f:num -> real`;`((1..1)):num ->bool`] emoi) \r
1741   THEN SIMP_TAC[MESON[NUMSEG_RREC;FINITE_NUMSEG] `FINITE (1..1)`] \r
1742   THEN SIMP_TAC[MESON[IN_NUMSEG;ARITH_RULE `~ (2<=1)`] ` ~( 2 IN (1..1))`]\r
1743   THEN SIMP_TAC[SPECL [`f : num -> real`;`1:num`] PRODUCT_SING_NUMSEG] THEN REAL_ARITH_TAC);;\r
1744 \r
1745 \r
1746 (*------------------------------------------------------------------*)\r
1747 (*            Measures of cube and union of cubes                   *)\r
1748 (*------------------------------------------------------------------*)\r
1749 \r
1750 \r
1751 let interval_upper_lowerbound=prove(`!(x:real^3). (interval_upperbound (interval [x,x + (lambda i. &1)])= x + (lambda i. &1)) /\ ( interval_lowerbound (interval [x,x + (lambda i. &1)])= x)`,\r
1752 GEN_TAC \r
1753 THEN MP_TAC(ISPECL [`x:real^3`;`x + (lambda i. &1):real^3`] INTERVAL_UPPERBOUND) \r
1754 THEN MP_TAC(ISPECL [`x:real^3`;`x + (lambda i. &1):real^3`] INTERVAL_LOWERBOUND) \r
1755 THEN REWRITE_TAC[VECTOR_ADD_COMPONENT;DIMINDEX_3]\r
1756 THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] \r
1757 THEN SIMP_TAC[REAL_ARITH `a:real <= a+ &1`]);;\r
1758 \r
1759 \r
1760 let measure_cube=prove(`!(x:real^3). measure (cube x)= &1`,\r
1761 REWRITE_TAC[cube_eq_interval]\r
1762 THEN GEN_TAC \r
1763 THEN SIMP_TAC[MEASURE_INTERVAL] \r
1764 THEN REWRITE_TAC[content]\r
1765 THEN SIMP_TAC[MESON[] `(if P then a else b) = &1 <=> if P then a= &1 else b= &1`]\r
1766 THEN SIMP_TAC[COND_EXPAND] \r
1767 THEN SIMP_TAC[non_empty_cinterval;DIMINDEX_3]\r
1768 THEN REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT;PRODUCT_CLAUSES;LAMBDA_BETA;DIMINDEX_3]\r
1769 THEN SIMP_TAC[ISPEC `(\i. (interval_upperbound (interval [x,x + (lambda i. &1)]) - \r
1770 interval_lowerbound (interval [x,x + (lambda i. &1)]))$i):num -> real` product_3]\r
1771 THEN SIMP_TAC[SPEC `x:real^3` interval_upper_lowerbound]\r
1772 THEN SIMP_TAC[VECTOR_ARITH `((a:real^3) + b )- a = b`]\r
1773 THEN SIMP_TAC[product_3]\r
1774 THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<= 1 /\ 1<= 3/\ 1<= 2 /\ 2<= 3 /\ 1<= 3 /\ 3<=3`]\r
1775 THEN REAL_ARITH_TAC);;\r
1776 \r
1777 \r
1778 let has_measure_cube=prove(`!(x:real^3)(r:real) (s:real^3 -> bool). s IN set_of_cube (int_ball x r) ==> s has_measure &1`,\r
1779 REPEAT GEN_TAC THEN REWRITE_TAC[set_of_cube;IN_ELIM_THM] THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_MESON_TAC[measurable_cube;measure_cube;HAS_MEASURE_MEASURABLE_MEASURE]);;\r
1780 \r
1781 (*Negligiblity of intersection of cubes *)\r
1782 \r
1783 let negligible_cube=prove( `!(x:real^3)(r:real) (s:real^3 ->bool) (t:real^3 ->bool). s IN set_of_cube (int_ball x r) /\ t IN set_of_cube (int_ball x r) /\ ~(s = t) \r
1784 ==> negligible (s INTER t)`,REPEAT GEN_TAC THEN REWRITE_TAC[set_of_cube;IN_ELIM_THM]\r
1785   THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(~ ((s:real^3 -> bool) = t)):bool` THEN ASM_REWRITE_TAC[]\r
1786   THEN DISCH_TAC THEN MP_TAC(MESON[] ` (x':real^3 = x'') ==> (cube x'= cube x'')`)\r
1787   THEN ONCE_REWRITE_TAC[MESON[] `(A ==> B) <=> (~B ==> ~A)`] THEN ASM_REWRITE_TAC[]\r
1788   THEN MP_TAC(MESON[int_ball;IN_INTER;IN_ELIM_THM] `x' IN int_ball x r /\ x'' IN int_ball x r ==> !i. 1 <= i /\ i <= 3 ==> integer ((x')$i) /\ integer ((x'')$i)`) THEN ASM_REWRITE_TAC[]\r
1789   THEN DISCH_TAC THEN MP_TAC(SPECL [`x':real^3`;`x'':real^3`] disjoint_cube) THEN ASM_REWRITE_TAC[]\r
1790 THEN SIMP_TAC[DISJOINT;NEGLIGIBLE_EMPTY] THEN ONCE_REWRITE_TAC[MESON[] `( a<=>b ) <=> (b<=>a)`]\r
1791   THEN SIMP_TAC[NEGLIGIBLE_EMPTY;MESON[] `~ a ==> ~b <=> b==> a`]);;\r
1792 \r
1793 \r
1794 let SUM_CONST2 = prove\r
1795  (`!c s. FINITE s ==> (sum s (\n. c) = &(CARD s) * c)`,\r
1796   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN\r
1797   SIMP_TAC[SUM_CLAUSES; CARD_CLAUSES; GSYM REAL_OF_NUM_SUC] THEN\r
1798   REPEAT STRIP_TAC THEN REAL_ARITH_TAC);;\r
1799 \r
1800 (*There are two different theorems about SUM_CONST*)\r
1801 \r
1802 \r
1803 let measure_unions_of_cube=prove( `!(x:real^3) (r:real). measure (UNIONS (set_of_cube (int_ball x r)))=   & (CARD (set_of_cube (int_ball x r)))`,REPEAT GEN_TAC THEN MP_TAC(ISPECL [`(\s. &1):(real^3 ->bool) ->real`;`set_of_cube (int_ball x r):(real^3 -> bool) -> bool`] MEASURE_NEGLIGIBLE_UNIONS)\r
1804     THEN SIMP_TAC[SPECL [`x:real^3`;`r:real`] finite_set_of_cube;ABS_SIMP;has_measure_cube]\r
1805     THEN REWRITE_TAC[SPECL [`x:real^3`;`r:real`] has_measure_cube]\r
1806     THEN REWRITE_TAC[SPECL [`x:real^3`;`r:real`] negligible_cube]\r
1807     THEN SIMP_TAC[] THEN DISCH_TAC THEN MP_TAC(SPECL [`x:real^3`;`r:real`] finite_set_of_cube) THEN REWRITE_TAC[REAL_ARITH `&(CARD (set_of_cube (int_ball x r)))= &(CARD (set_of_cube (int_ball x r)))* &1`]\r
1808     THEN MESON_TAC[ISPECL [`&1:real`;`set_of_cube (int_ball x r):(real^3 ->bool)-> bool`] SUM_CONST2;REAL_ARITH `&(CARD (set_of_cube (int_ball x r)))= &(CARD (set_of_cube (int_ball x r)))* &1`]);;\r
1809 \r
1810 (*-----------------------------------------------------------------*)\r
1811 (*             Union of cubes is contained in ball                 *)\r
1812 (*-----------------------------------------------------------------*)\r
1813 \r
1814 \r
1815 let pow_lesthan_1=prove( `!(a:real). &0 < a /\ a < &1 ==> a*a < &1`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`a:real`;`a:real`;`&1:real`] REAL_LT_LMUL) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_ARITH `(x:real)* &1= x`;REAL_ARITH `a:real <b /\ b< c ==> a< c`]);;\r
1816 \r
1817 \r
1818 let cube_to_ball=prove(`!(x:real^3) (y:real^3). y IN cube x ==> norm (x-y)< sqrt(&3)`,\r
1819 REPEAT STRIP_TAC  THEN MP_TAC(ISPEC `(x-y):real^3` NORM_POS_LE)\r
1820   THEN MP_TAC (SPEC `&3:real` SQRT_POS_LE) THEN ASM_REWRITE_TAC[REAL_ARITH `&0<= &3`;REAL_ARITH `&0<A ==> A= abs (A)`]\r
1821   THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_REFL]\r
1822   THEN ONCE_REWRITE_TAC[MESON[] `a= b <=> b=a`]\r
1823   THEN REWRITE_TAC[MESON[] `((a:real) = b ==> (c:real) = d ==> c< a ) <=> ((a:real) = b ==> (c:real) = d ==> d< b )`]\r
1824   THEN REWRITE_TAC[REAL_LT_SQUARE_ABS] THEN SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0<= &3`]\r
1825   THEN SIMP_TAC[NORM_POW_2;DOT_3] THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN UNDISCH_TAC `(y IN cube (x:real^3)):bool`\r
1826   THEN REWRITE_TAC[cube;IN_ELIM_THM] THEN REWRITE_TAC[FORALL_3] \r
1827   THEN REWRITE_TAC[REAL_ARITH `(a:real) <b /\ b< a+ &1 <=> &0< b-a /\ b-a < &1`]\r
1828   THEN ONCE_REWRITE_TAC[REAL_FIELD `((x:real^3)$1 - (y:real^3)$1) * (x$1 - y$1) +\r
1829      (x$2 - y$2) * (x$2 - y$2) +\r
1830      (x$3 - y$3) * (x$3 - y$3)= (y$1 - x$1) * (y$1 - x$1) +\r
1831      (y$2 - x$2) * (y$2 - x$2) +\r
1832      (y$3 - x$3) * (y$3 - x$3)`]\r
1833   THEN REPEAT STRIP_TAC THEN MP_TAC(MESON[pow_lesthan_1] `&0 < (y:real^3)$1 - (x:real^3)$1 /\ y$1 - x$1 < &1 ==> (y$1 - x$1) * (y$1 - x$1)< &1`)\r
1834   THEN ASM_REWRITE_TAC[]\r
1835   THEN MP_TAC(MESON[pow_lesthan_1] `&0 < (y:real^3)$2 - (x:real^3)$2 /\ y$2 - x$2 < &1 ==> (y$2 - x$2) * (y$2 - x$2)< &1`) THEN ASM_REWRITE_TAC[]\r
1836   THEN MP_TAC(MESON[pow_lesthan_1] `&0 < (y:real^3)$3 - (x:real^3)$3 /\ y$3 - x$3 < &1 ==> (y$3 - x$3) * (y$3 - x$3)< &1`) THEN ASM_REWRITE_TAC[]\r
1837   THEN MESON_TAC[REAL_ARITH `(a:real)< &1 /\ b< &1 /\c < &1 ==> a+b+c < &3`]);;\r
1838 \r
1839 \r
1840 let unions_cube_subset_ball=prove(`!(x:real^3) (r:real). UNIONS (set_of_cube (int_ball x r)) SUBSET (hinhcau x (r+ sqrt (&3)))`,REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;UNIONS]\r
1841     THEN GEN_TAC THEN REWRITE_TAC[hinhcau;IN_ELIM_THM]\r
1842     THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC\r
1843     THEN UNDISCH_TAC `(u IN set_of_cube (int_ball x r) /\ (x':real^3) IN u):bool`\r
1844     THEN REWRITE_TAC[set_of_cube] THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC\r
1845     THEN UNDISCH_TAC `((x':real^3) IN u):bool` THEN ASM_REWRITE_TAC[]\r
1846     THEN DISCH_TAC THEN MP_TAC(SPECL [`x'':real^3`;`x':real^3`] cube_to_ball) THEN ASM_REWRITE_TAC[]\r
1847     THEN UNDISCH_TAC `(x'' IN int_ball (x:real^3) r):bool`\r
1848     THEN REWRITE_TAC[int_ball;IN_INTER] THEN STRIP_TAC\r
1849     THEN MP_TAC(MESON[hinhcau;IN_ELIM_THM] `(x'':real^3) IN (hinhcau x r) ==> norm (x - x'') < r`) THEN ASM_REWRITE_TAC[]\r
1850     THEN ONCE_REWRITE_TAC[MESON[VECTOR_ARITH `(x:real^3)- x' = (x - x'') + (x'' - x')`] `norm ((x:real^3) - x') < r + sqrt (&3) <=> norm ((x - x'') + (x'' - x')) < r + sqrt (&3)`]\r
1851     THEN MESON_TAC[ISPECL [`(x - x''):real^3`;`(x'' - x'):real^3`] NORM_TRIANGLE;REAL_ARITH `((e:real) <= (a + c)) /\a <b /\ c< d ==> e < b+ d`]);;\r
1852 \r
1853 (*-----------------------------------------------------------------*)\r
1854 \r
1855 \r
1856 let hinhcau_ball=prove(`!(x:real^3)(r:real). hinhcau x r= ball (x,r)`,REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]\r
1857                          THEN REWRITE_TAC[hinhcau;ball;IN_ELIM_THM;dist]);;\r
1858 \r
1859 let measure_unions_cube_less_ball=prove(`!(x:real^3)(r:real). measure (UNIONS (set_of_cube (int_ball x r))) \r
1860 <= measure (hinhcau x (r+ sqrt(&3)))`,REPEAT GEN_TAC THEN MP_TAC(SPECL [`x:real^3`;`r:real`] unions_cube_subset_ball) THEN MP_TAC(SPECL [`x:real^3`;`r:real`] measurable_unions_cube) THEN SIMP_TAC[SPECL [`x:real^3`;`r+ sqrt(&3):real`] hinhcau_ball]\r
1861   THEN MP_TAC(ISPECL [`x:real^3`;`r+ sqrt(&3):real`] MEASURABLE_BALL) THEN MESON_TAC[MEASURE_SUBSET]);;\r
1862 \r
1863 let measure_hinhcau=prove(`!(x:real^3)(r:real). &0<= r ==> measure (hinhcau x r) = &4 / &3 * pi * (r pow 3)`,MESON_TAC[hinhcau_ball;VOLUME_BALL]);;\r
1864 \r
1865 \r
1866 (*-----------------------------------------------------------------------*)\r
1867 (*Lemma 2.14 [WQZISRI]:Upperbound for number of integer points in a ball *)\r
1868 (*-----------------------------------------------------------------------*)\r
1869 \r
1870 let WQZISRI=prove(`!(p:real^3)(r:real). &0<= r ==> FINITE (int_ball p r) /\ (& (CARD(int_ball p r)) \r
1871 <= (&4/ &3) * pi * ((r+ sqrt (&3)) pow 3))`,REPEAT GEN_TAC THEN SIMP_TAC[finite_int_ball]\r
1872                     THEN DISCH_TAC THEN MP_TAC(GSYM(SPECL [`p:real^3`;`r + sqrt (&3):real`] measure_hinhcau))\r
1873                     THEN MP_TAC(MESON[REAL_LE_RADD;REAL_ARITH `&0+ a= a`] `&0<= r ==> sqrt(&3)<= r+ sqrt(&3)`)\r
1874                     THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPEC `&3:real` SQRT_POS_LE) THEN REWRITE_TAC[REAL_ARITH `&0<= &3`]\r
1875                     THEN ONCE_REWRITE_TAC[MESON[] `a ==> b==>c ==> d <=> a/\b ==>c==>d`]\r
1876                     THEN DISCH_TAC THEN MP_TAC(REAL_ARITH `&0 <= sqrt (&3) /\ sqrt (&3) <= r + sqrt (&3) ==> &0<= r+ sqrt(&3)`) THEN ASM_REWRITE_TAC[]\r
1877                     THEN SIMP_TAC[] THEN SIMP_TAC[int_ball_card_eq] THEN SIMP_TAC[GSYM measure_unions_of_cube] THEN SIMP_TAC[measure_unions_cube_less_ball]);;\r
1878 \r
1879 \r
1880 (*------------------------------------------------------------------------*)\r
1881 \r
1882 \r
1883 let ccube=new_definition`ccube (x:real^3)={y :real^3 | !i. 1<= i /\ i<= 3 ==> x$i<= y$i /\ y$i <= x$i + &1}`;;\r
1884 \r
1885 let set_of_ccube=new_definition`set_of_ccube(S:real^3 -> bool)= {ccube x| x IN S}`;;\r
1886 \r
1887 let close_hinhcau=new_definition`close_hinhcau (x:real^3)(r:real)={ y:real^3 | norm (y-x)<= r}`;;\r
1888 \r
1889 let map1=new_definition`map1 (x:real^3)= ccube x`;;\r
1890 \r
1891 \r
1892 let daumut_ccube=prove(`!(x:real^3). x IN ccube x /\ (x + lambda i. &1) IN ccube x`,REWRITE_TAC[ccube;IN_ELIM_THM]\r
1893                         THEN REWRITE_TAC[VECTOR_ADD_COMPONENT;LAMBDA_BETA;DIMINDEX_3]\r
1894                         THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN REAL_ARITH_TAC);;\r
1895 \r
1896 \r
1897 let different_ccube=prove( `!(x:real^3) (y:real^3).((ccube x) = (ccube y) ==> x = y)`,\r
1898 REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real^3` daumut_ccube) THEN ASM_REWRITE_TAC[]\r
1899   THEN REWRITE_TAC[ccube;VECTOR_ADD_COMPONENT;LAMBDA_BETA;DIMINDEX_3;IN_ELIM_THM]\r
1900   THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN SIMP_TAC[REAL_ARITH `(a:real) + &1 <= b+ &1 <=> a <= b `]\r
1901   THEN REWRITE_TAC[FORALL_3] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(SPECL [`x:real^3`;`y:real^3`] vector_eq2)\r
1902   THEN REWRITE_TAC[FORALL_3] THEN ASM_MESON_TAC[REAL_ARITH `(a:real)<= b /\ b<= a ==> a=b`]);;\r
1903 \r
1904 \r
1905 let inj_map1=prove(`! (x:real^3) (r:real). INJ map1 (int_ball x r) (set_of_ccube (int_ball x r))`,\r
1906 REWRITE_TAC[INJ;map1;set_of_ccube] THEN SIMP_TAC[SET_RULE `x' IN int_ball x r ==> ccube x' IN {ccube x' | x' IN int_ball x r}`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[int_ball] THEN MESON_TAC[different_ccube]);;                    \r
1907 \r
1908 let surj2_map1=prove(`!(x:real^3) (r:real). IMAGE map1 (int_ball x r) = set_of_ccube (int_ball x r)`,\r
1909 REWRITE_TAC[IMAGE] THEN REWRITE_TAC[map1] THEN REWRITE_TAC[set_of_ccube] THEN SIMP_TAC[EXTENSION] \r
1910 THEN REWRITE_TAC[IN_ELIM_THM] THEN SIMP_TAC[GSYM EXTENSION]);;\r
1911 \r
1912 let int_ball_card_eq_ccube=prove(`!(x:real^3) (r:real). CARD (int_ball x r)= CARD (set_of_ccube (int_ball x r))`,\r
1913 REPEAT GEN_TAC THEN SIMP_TAC[GSYM (SPECL [`X:real^3`;`r:real` ] surj2_map1)]\r
1914   THEN MP_TAC(SPECL [`x:real^3`;`r:real`] finite_int_ball) THEN MP_TAC(SPECL [`x:real^3`;`r:real`] inj_map1)\r
1915   THEN REWRITE_TAC[MESON[] `a==>b==>c <=> a/\ b ==>c`;INJ] \r
1916   THEN SIMP_TAC[set_of_ccube;map1;SET_RULE `x' IN int_ball x r ==> ccube x' IN {ccube x' | x' IN int_ball x r}`]\r
1917   THEN REWRITE_TAC[MESON[map1] `ccube (x':real^3)= map1 x'`;GSYM map1]\r
1918   THEN MESON_TAC[ISPECL [`map1:real^3 -> real^3 -> bool`;`(int_ball x r):real^3 -> bool`] CARD_IMAGE_INJ]);;\r
1919 \r
1920 let ccube_eq_interval=prove(`!(x:real^3). ccube x= interval[x,x+ lambda i. &1]`,\r
1921 GEN_TAC THEN REWRITE_TAC[EXTENSION;ccube;interval;DIMINDEX_3] THEN SIMP_TAC[IN_ELIM_THM;LAMBDA_BETA;DIMINDEX_3]\r
1922   THEN SIMP_TAC[VECTOR_ADD_COMPONENT;LAMBDA_BETA;DIMINDEX_3]);;\r
1923 \r
1924 \r
1925 let measurable_ccube=prove( `!(x:real^3). measurable (ccube x)`,REWRITE_TAC[ccube_eq_interval;MEASURABLE_INTERVAL]);;\r
1926 \r
1927 let finite_set_of_ccube=prove(`!(x:real^3)(r:real). FINITE (set_of_ccube (int_ball x r))`,\r
1928 MESON_TAC[ISPECL [`map1:real^3 -> real^3 -> bool`; `(int_ball x r):real^3 -> bool`] FINITE_IMAGE;finite_int_ball;surj2_map1]);;\r
1929 \r
1930 \r
1931 \r
1932 let measurable_unions_ccube=prove( `!(x:real^3)(r:real). measurable (UNIONS (set_of_ccube (int_ball x r)))`,\r
1933 REPEAT GEN_TAC THEN MATCH_MP_TAC(ISPEC `set_of_ccube (int_ball x r):(real^3 -> bool) -> bool` MEASURABLE_UNIONS2) \r
1934 THEN REWRITE_TAC[finite_set_of_ccube] THEN REWRITE_TAC[set_of_ccube;IN_ELIM_THM] THEN MESON_TAC[measurable_ccube]);;\r
1935 \r
1936 \r
1937 let measure_ccube=prove(`!(x:real^3). measure (ccube x)= &1`,REWRITE_TAC[ccube_eq_interval]\r
1938  THEN GEN_TAC THEN SIMP_TAC[MEASURE_INTERVAL] THEN REWRITE_TAC[content]\r
1939                          THEN SIMP_TAC[MESON[] `(if P then a else b) = &1 <=> if P then a= &1 else b= &1`]\r
1940  THEN SIMP_TAC[COND_EXPAND] THEN SIMP_TAC[non_empty_cinterval;DIMINDEX_3]\r
1941                          THEN REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT;PRODUCT_CLAUSES;LAMBDA_BETA;DIMINDEX_3]\r
1942  THEN SIMP_TAC[ISPEC `(\i. (interval_upperbound (interval [x,x + (lambda i. &1)]) - \r
1943 interval_lowerbound (interval [x,x + (lambda i. &1)]))$i):num -> real` product_3]\r
1944  THEN SIMP_TAC[SPEC `x:real^3` interval_upper_lowerbound]\r
1945                                          THEN SIMP_TAC[VECTOR_ARITH `((a:real^3) + b )- a = b`]\r
1946                                          THEN SIMP_TAC[product_3]\r
1947  THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<= 1 /\ 1<= 3/\ 1<= 2 /\ 2<= 3 /\ 1<= 3 /\ 3<=3`]\r
1948                                          THEN REAL_ARITH_TAC);;\r
1949 \r
1950 \r
1951 let has_measure_ccube=prove(`!(x:real^3)(r:real) (s:real^3 -> bool). s IN set_of_ccube (int_ball x r) ==> s has_measure &1`,\r
1952 REPEAT GEN_TAC THEN REWRITE_TAC[set_of_ccube;IN_ELIM_THM] THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_MESON_TAC[measurable_ccube;measure_ccube;HAS_MEASURE_MEASURABLE_MEASURE]);;\r
1953 \r
1954 \r
1955 let measure_element_set_ccube=prove( `! (S:real^3 -> bool) (t:real^3 -> bool). t IN (set_of_ccube S) ==> measure t= &1`,\r
1956 REPEAT GEN_TAC THEN REWRITE_TAC[set_of_ccube;IN_ELIM_THM]THEN MESON_TAC[measure_ccube]);;\r
1957 \r
1958 let sum_measure_ccube=prove(`!(p:real^3)(r:real). sum (set_of_ccube (int_ball p r)) (\s. measure s)= &(CARD (set_of_ccube (int_ball p r)))`,REPEAT GEN_TAC\r
1959                               THEN MP_TAC(ISPECL [`(\s. measure s):(real^3-> bool)-> real`;`(\s. &1):(real^3-> bool)-> real`;`set_of_ccube (int_ball p r):(real^3->bool) -> bool`] SUM_EQ)\r
1960                               THEN REWRITE_TAC[IN_ELIM_THM]\r
1961                               THEN REWRITE_TAC[measure_element_set_ccube]\r
1962                               THEN REWRITE_TAC[MESON[] `a=b ==> a=c <=> a=b ==> b=c`]\r
1963                               THEN MP_TAC(SPECL [`p:real^3`;`r:real`] finite_set_of_ccube)\r
1964                               THEN MESON_TAC[ISPECL [`&1:real`;`set_of_ccube (int_ball x r):(real^3 ->bool)-> bool`] SUM_CONST;REAL_ARITH `&(CARD (set_of_ccube (int_ball x r)))= &(CARD (set_of_ccube (int_ball x r)))* &1`]);;\r
1965 \r
1966 (* There are two different theorems about SUM_EQ and sum *)\r
1967 \r
1968 \r
1969 let mea_unions_ccube_le_card=prove(`!(x:real^3) (r:real). measure (UNIONS (set_of_ccube (int_ball x r)))<=   & (CARD (set_of_ccube (int_ball x r)))`,REPEAT GEN_TAC THEN MP_TAC(ISPEC  `set_of_ccube (int_ball x r):(real^3 -> bool) -> bool` MEASURE_UNIONS_LE) THEN SIMP_TAC[SPECL [`x:real^3`;`r:real`] finite_set_of_ccube;ABS_SIMP;has_measure_ccube]\r
1970                                      THEN REWRITE_TAC[set_of_ccube;IN_ELIM_THM]\r
1971                                      THEN REWRITE_TAC[MESON[measurable_ccube] `!s. (?x'. x' IN int_ball x r /\ s = ccube x') ==> measurable s`] THEN REWRITE_TAC[GSYM set_of_ccube] THEN MESON_TAC[SPECL [`x:real^3`;`r:real`] sum_measure_ccube]);;\r
1972 \r
1973 let in_ccube_floor=prove(`!(x:real^3). x IN ccube (lambda i. floor (x$i)) `,GEN_TAC THEN REWRITE_TAC[ccube;IN_ELIM_THM]\r
1974                            THEN GEN_TAC THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3]\r
1975                            THEN REWRITE_TAC[FLOOR] THEN MESON_TAC[FLOOR;REAL_ARITH `(a:real) < b ==> a<= b`]);;\r
1976 REAL_LE_SQUARE_ABS;;\r
1977 REAL_ABS_REFL;;\r
1978 \r
1979 let pow_lesthan_eq_1=prove( `!(a:real). &0 <= a /\ a <= &1 ==> a*a <= &1`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`a:real`;`a:real`;`&1:real`] REAL_LE_LMUL) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_ARITH `(x:real)* &1= x`;REAL_ARITH `a:real <=b /\ b<= c ==> a<= c`]);;\r
1980 \r
1981 let ccube_to_ball=prove(`!(x:real^3) (y:real^3). y IN ccube x ==> norm (x-y)<= sqrt(&3)`,\r
1982 REPEAT STRIP_TAC  THEN MP_TAC(ISPEC `((x:real^3)-y):real^3` NORM_POS_LE)\r
1983   THEN MP_TAC (SPEC `&3:real` SQRT_POS_LE) THEN ASM_REWRITE_TAC[REAL_ARITH `&0<= &3`;REAL_ARITH `&0<A ==> A= abs (A)`]\r
1984   THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_REFL]\r
1985   THEN ONCE_REWRITE_TAC[MESON[] `(a:real)= b <=> b=a`]\r
1986   THEN REWRITE_TAC[MESON[] `((a:real) = b ==> (c:real) = d ==> c<= a ) <=> ((a:real) = b ==> (c:real) = d ==> d<= b )`]\r
1987   THEN REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN SIMP_TAC[SQRT_POW_2; REAL_ARITH `&0<= &3`]\r
1988   THEN SIMP_TAC[NORM_POW_2;DOT_3] THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN UNDISCH_TAC `(y IN ccube (x:real^3)):bool`\r
1989   THEN REWRITE_TAC[ccube;IN_ELIM_THM] THEN REWRITE_TAC[FORALL_3]\r
1990   THEN REWRITE_TAC[REAL_ARITH `(a:real) <=b /\ b<= a+ &1 <=> &0<= b-a /\ b-a <= &1`]\r
1991   THEN ONCE_REWRITE_TAC[REAL_FIELD `((x:real^3)$1 - (y:real^3)$1) * (x$1 - y$1) +\r
1992      (x$2 - y$2) * (x$2 - y$2) +\r
1993      (x$3 - y$3) * (x$3 - y$3)= (y$1 - x$1) * (y$1 - x$1) +\r
1994      (y$2 - x$2) * (y$2 - x$2) +\r
1995      (y$3 - x$3) * (y$3 - x$3)`]\r
1996   THEN REPEAT STRIP_TAC THEN MP_TAC(MESON[pow_lesthan_eq_1] `&0 <= (y:real^3)$1 - (x:real^3)$1 /\ y$1 - x$1 <= &1 ==> (y$1 - x$1) * (y$1 - x$1)<= &1`)\r
1997   THEN ASM_REWRITE_TAC[]\r
1998   THEN MP_TAC(MESON[pow_lesthan_eq_1] `&0 <= (y:real^3)$2 - (x:real^3)$2 /\ y$2 - x$2 <= &1 ==> (y$2 - x$2) * (y$2 - x$2)<= &1`) THEN ASM_REWRITE_TAC[]\r
1999   THEN MP_TAC(MESON[pow_lesthan_eq_1] `&0 <= (y:real^3)$3 - (x:real^3)$3 /\ y$3 - x$3 <= &1 ==> (y$3 - x$3) * (y$3 - x$3)<= &1`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[REAL_ARITH `(a:real)<= &1 /\ b<= &1 /\c <= &1 ==> a+b+c <= &3`]);;\r
2000 \r
2001 \r
2002 let ball_subset_union_ccube=prove(`!(x:real^3) (r:real).ball(x,r- sqrt(&3)) SUBSET (UNIONS  (set_of_ccube (int_ball x r)))`,REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNIONS;set_of_ccube]\r
2003    THEN GEN_TAC THEN REWRITE_TAC[ball;IN_ELIM_THM]\r
2004    THEN REWRITE_TAC[dist] THEN DISCH_TAC THEN EXISTS_TAC `ccube (lambda i. (floor (((x':real^3))$i)):real):real^3 ->bool`\r
2005    THEN REWRITE_TAC[SPEC `x':real^3` in_ccube_floor]\r
2006                                    THEN EXISTS_TAC `(lambda i. (floor ((x':real^3)$i)):real):real^3`\r
2007                                    THEN SIMP_TAC[] THEN REWRITE_TAC[int_ball;IN_ELIM_THM]\r
2008                                    THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM]\r
2009                                    THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;hinhcau;IN_ELIM_THM;FLOOR]\r
2010                                    THEN REWRITE_TAC[FLOOR;(* GSYM INTEGER_IS_INT *)]\r
2011                                    THEN REWRITE_TAC[MESON[VECTOR_ARITH `(x:real^3) - (lambda i. floor ((x':real^3)$i))= (x- x') + (x' - (lambda i. floor (x'$i)))`] `(norm:real^3 ->real) ((x:real^3) - (lambda i. (floor ((x':real^3)$i)):real))= norm ((x- x') + (x' - (lambda i. floor (x'$i))))`]\r
2012                                    THEN MP_TAC(SPECL [`(lambda i. (floor ((x':real^3)$i)):real):real^3`;`x':real^3`] ccube_to_ball)\r
2013                                    THEN SIMP_TAC[SPEC `x':real^3` in_ccube_floor]\r
2014                                    THEN UNDISCH_TAC `((norm:real^3 ->real) ((x:real^3) - x') < (r:real) - sqrt (&3)):bool`\r
2015                                    THEN MP_TAC(ISPECL [`x - (x':real^3)`; ` x' - (lambda i. (floor ((x':real^3)$i):real)):real^3`] NORM_TRIANGLE)\r
2016                                    THEN ONCE_REWRITE_TAC[MESON[] `a ==>b ==> c ==> d <=> a/\b/\c ==>  d`]\r
2017                                    THEN MESON_TAC[NORM_SUB;REAL_ARITH `a:real <= b+ c /\ b< r- sqrt(&3) /\ c<= sqrt (&3) ==> a< r`]);;\r
2018 \r
2019 \r
2020 let volume_ball_gon=prove( `!(x:real^3)(r:real). sqrt(&3) <= r ==> measurable (ball(x,r- sqrt(&3))) /\ measure (ball(x,r- sqrt(&3)))= (&4/ &3)* pi* (r- sqrt (&3)) pow 3`,ONCE_REWRITE_TAC[REAL_ARITH `a:real <=b <=> &0<= b-a`] THEN MESON_TAC[MEASURABLE_BALL;VOLUME_BALL]);;\r
2021 \r
2022 let lower_bound_measure_unions_ccube=prove(`!(x:real^3)(r:real). (sqrt(&3)<= r) ==> (&4/ &3)* pi* (r- sqrt (&3)) pow 3 <= measure (UNIONS  (set_of_ccube (int_ball x r)))`,REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`ball(x,r- sqrt(&3)):real^3 -> bool`;`UNIONS  (set_of_ccube (int_ball x r)):real^3 -> bool`] MEASURE_SUBSET) THEN ASM_REWRITE_TAC[volume_ball_gon; measurable_unions_ccube;ball_subset_union_ccube] THEN ASM_SIMP_TAC[volume_ball_gon]);;\r
2023 \r
2024 \r
2025 (*-----------------------------------------------------------------------*)\r
2026 (* Lemma 2.15 [PWVIIOL] lower bound for number of integer points in ball *)\r
2027 (*-----------------------------------------------------------------------*)\r
2028 \r
2029 \r
2030 let PWVIIOL=prove(`!(x:real^3)(r:real). (sqrt(&3) <= r) ==> FINITE (int_ball x r) /\  (&4/ &3)* pi* (r- sqrt (&3)) pow 3 <= &(CARD(int_ball x r))`,REPEAT STRIP_TAC THEN SIMP_TAC[finite_int_ball] THEN ASM_MESON_TAC[ int_ball_card_eq_ccube;mea_unions_ccube_le_card;lower_bound_measure_unions_ccube;REAL_ARITH `a:real <= b /\ b<= c ==> a<= c`]);;\r
2031 \r
2032 \r
2033 (*-----------------------------------------------------------------------*)\r
2034 \r
2035 \r
2036 let integer_point= new_definition`integer_point (S:real^3 -> bool)= {x:real^3 | (!i. 1<= i /\ i<=3 ==> integer(x$i)) /\ x IN S}`;;\r
2037 \r
2038 let int_ball_subset=prove( `!(x:real^3)(r1:real)(r2:real). r1< r2 ==> (int_ball x r1) SUBSET (int_ball x r2)`,REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET;int_ball;IN_INTER;IN_ELIM_THM] THEN GEN_TAC THEN SIMP_TAC[]\r
2039                              THEN REWRITE_TAC[hinhcau;IN_ELIM_THM] THEN ASM_MESON_TAC[REAL_ARITH `a:real< b /\ b< c ==> a< c`]);;\r
2040 \r
2041 let card_int_ball_ineq=prove(`!(x:real^3)(r1:real)(r2:real). r1< r2 ==> CARD (int_ball x r1)<= CARD (int_ball x r2)`,MESON_TAC[int_ball_subset;finite_int_ball;CARD_SUBSET]);;\r
2042 \r
2043 \r
2044 let eq_def_intball=prove( `!(x:real^3)(k1:real)(k2:real)(r:real).(&0< k1 /\ &0< k2 /\ k2<= r) ==> integer_point (ball(x,r+ k1) DIFF ball(x,r- k2)) = (int_ball x (r+ k1)) DIFF (int_ball x (r- k2))`,REPEAT STRIP_TAC\r
2045                             THEN REWRITE_TAC[EXTENSION;integer_point;DIFF;ball;int_ball;IN_ELIM_THM]\r
2046                             THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[dist;IN_INTER;IN_ELIM_THM]\r
2047                             THEN REWRITE_TAC[hinhcau;IN_ELIM_THM;MESON[] `~ (A /\ B ) <=> ~A \/ ~B`]\r
2048                             THEN MESON_TAC[]);;\r
2049 \r
2050 let card_int_ball_le=prove( `!(x:real^3)(k1:real)(k2:real)(r:real).(&0<k1 /\ &0<k2 /\ k2+ sqrt(&3)<= r) ==> &(CARD (int_ball x (r + k1))) <=\r
2051      &4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r+ k1:real`] WQZISRI) THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0<k2 /\ k2+ sqrt(&3)<= r ==> sqrt(&3)< r+k1`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(MESON[SPEC `&3:real` SQRT_POS_LE;REAL_ARITH `&0 <= &3`] `&0<= sqrt(&3)`) THEN DISCH_TAC THEN MP_TAC(REAL_ARITH `&0 <= sqrt (&3) /\ (sqrt (&3) < r + k1) ==> &0<= r+ k1`) THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[]);;\r
2052 \r
2053 let card_int_ball_le2=prove( `!(x:real^3)(k1:real)(r:real).(&0<=k1 /\ &0<= r) ==> &(CARD (int_ball x (r + k1))) <=\r
2054      &4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r+ k1:real`] WQZISRI) THEN MP_TAC(REAL_ARITH `&0<=k1 /\ &0<= r ==> &0<= r+k1`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);;\r
2055 \r
2056 \r
2057 let card_int_ball_pos=prove(`!(x:real^3)(k1:real)(k2:real)(r:real).(&0<k1 /\ &0<k2 /\ k2+ sqrt(&3)<= r) ==> &4 / &3 * pi * ((r - k2) - sqrt (&3)) pow 3 <= &(CARD (int_ball x (r - k2)))`,REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real^3`;`r- k2:real`] PWVIIOL) THEN MP_TAC(REAL_ARITH `k2 + sqrt (&3) <= r ==> sqrt(&3)<= r- k2`) THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[]);;\r
2058 \r
2059 let bdt1_finiteness=prove(`!(r:real)(k:real). &0<r ==> &4*pi*r*k <= &4*pi*r* abs k`,REPEAT STRIP_TAC\r
2060                             THEN ASSUME_TAC PI_POS THEN MP_TAC(MESON[REAL_LT_LMUL;REAL_ARITH `&0* r= &0`;REAL_ARITH `pi* r= r* pi`;REAL_ARITH `&0< e ==> &0< &4* e`] `&0< r /\ &0< pi ==> &0< &4*pi*r`) THEN ASM_REWRITE_TAC[]\r
2061                             THEN REWRITE_TAC[REAL_ARITH `(a:real) *b*C*d= (a*b*C)*d`]\r
2062                             THEN MP_TAC(SPEC `k:real` REAL_ABS_LE) THEN MESON_TAC[REAL_ARITH `&0 < &4 * pi * r ==> &0<= &4 * pi * r`;REAL_LE_LMUL]);;\r
2063 \r
2064 \r
2065 let bdt2_finiteness=prove( `!(r:real)(k:real)(i:num).(&0< k /\ k<= r ==> &1 <= r pow i / k pow i)`,REPEAT STRIP_TAC\r
2066                              THEN MP_TAC(SPECL [`k:real`;`i:num`] REAL_POW_LT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC\r
2067                              THEN ASM_SIMP_TAC[GSYM (ISPECL [`&1:real`;`(r pow i/ k pow i):real`;`(k pow i):real`] REAL_LE_RMUL_EQ)] THEN MP_TAC(REAL_ARITH ` &0 < k pow i ==> ~ (&0= k pow i)`) THEN ASM_REWRITE_TAC[] \r
2068                              THEN SIMP_TAC[REAL_DIV_RMUL] THEN ASM_SIMP_TAC[REAL_ARITH ` &1 * a= a`;REAL_ARITH `a< b ==> a<= b`] THEN ASM_MESON_TAC[REAL_POW_LE2;REAL_ARITH `&0< k ==> &0 <= k`]);;\r
2069 \r
2070 \r
2071 let bdt3_finiteness=prove( `!(r:real)(k1:real)(k2:real) (k:real). ( &0 < r/\ &0 < k1 /\ &0< k2) ==>( &0<=  &4 * pi *r* (abs k) /\ &0 <= &4/ &3 *pi*( (k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3))`,\r
2072                            REPEAT STRIP_TAC THENL [ASM_MESON_TAC[REAL_ARITH `&0< A==> &0<= A`;PI_POS_LE;REAL_ABS_POS;REAL_LE_MUL;REAL_ARITH `&0<= &4`];MP_TAC(MESON[REAL_ARITH `&0< k1 ==> sqrt(&3)<= k1 + sqrt(&3)`;SQRT_POS_LE;REAL_ARITH `&0<= &3`;REAL_ARITH `a<= b /\ b<=c ==> a<= c`]  `&0< k1 ==> &0<= k1 + sqrt (&3)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(MESON[REAL_ARITH `&0< k2 ==> sqrt(&3)<= k2 + sqrt(&3)`;SQRT_POS_LE;REAL_ARITH `&0<= &3`;REAL_ARITH `a<= b /\ b<=c ==> a<= c`]  `&0< k2 ==> &0<= k2 + sqrt (&3)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(SPECL [`k1 + sqrt (&3):real`;` 3:num`] REAL_POW_LE) THEN ASM_REWRITE_TAC[]\r
2073                              THEN MP_TAC(SPECL [`k2 + sqrt (&3):real`;` 3:num`] REAL_POW_LE) THEN ASM_REWRITE_TAC[]\r
2074                              THEN REPEAT DISCH_TAC THEN MP_TAC(REAL_ARITH `&0 <= (k2 + sqrt (&3)) pow 3 /\ &0 <= (k1 + sqrt (&3)) pow 3 ==> &0<=  (k1 + sqrt (&3)) pow 3+ (k2 + sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[REAL_LE_MUL;REAL_ARITH `&0<= &4/ &3`;PI_POS_LE]]);;\r
2075 \r
2076 \r
2077 let bdt4_finiteness = prove(`!(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ k2 + sqrt (&3) <= r) ==> (&4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3)- (&4 / &3 * pi * (r - k2 - sqrt (&3)) pow 3)<= (&4/ &3* pi*( &3*(k1+ k2+ &2*sqrt(&3)) +((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) /((k2 + sqrt (&3)) pow 2) + &3 * abs(((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)) / (k2 + sqrt (&3)))) *r pow 2`, REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_FIELD `&4 / &3 * pi * ((r + k1) + sqrt (&3)) pow 3 -\r
2078  &4 / &3 * pi * (r - k2 - sqrt (&3)) pow 3= ( &4*pi*r pow 2 * (k1+k2+ &2*sqrt(&3)) + &4*pi*r* ((k1+ sqrt(&3))pow 2 - (k2+ sqrt(&3)) pow 2)+ &4/ &3*pi*((k1+ sqrt(&3))pow 3 + (k2+ sqrt(&3)) pow 3))`]\r
2079        THEN REWRITE_TAC[REAL_FIELD ` (&4/ &3 * pi*( &3* (k1+k2+ &2*sqrt(&3)) +\r
2080   ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2) +\r
2081   &3 *\r
2082   abs (((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)) / (k2 + sqrt (&3)))) *\r
2083  r pow 2=  (&4 * pi * r pow 2 * (k1 + k2 + &2 * sqrt (&3))+ &4*pi*r pow 2* abs (((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)) / (k2 + sqrt (&3))+ &4/ &3*pi* r pow 2* ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2))`]\r
2084  THEN REWRITE_TAC[REAL_ARITH `(a:real) + b+ c <= a + d + e <=> b+c <= d+ e`]\r
2085  THEN  MATCH_MP_TAC(REAL_ARITH `&4 * pi * r * ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)<=  &4 *\r
2086  pi *\r
2087  r pow 2 *\r
2088  abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)) /\  &4 / &3 * pi * ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3)<=  &4 / &3 *\r
2089  pi *\r
2090  r pow 2 *\r
2091  ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2) ==> &4 * pi * r * ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) +\r
2092  &4 / &3 * pi * ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) <=\r
2093  &4 *\r
2094  pi *\r
2095  r pow 2 *\r
2096  abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)) +\r
2097  &4 / &3 *\r
2098  pi *\r
2099  r pow 2 *\r
2100  ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2)`)\r
2101  THEN MATCH_MP_TAC(REAL_ARITH `&4 * pi * r * ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) <= &4*pi* r  * abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)  /\ &4*pi* r  * abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2)<=   &4 *\r
2102  pi *\r
2103  r pow 2 *\r
2104  abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)) /\ &4 / &3 * pi * ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) <=\r
2105  &4 / &3 *\r
2106  pi *\r
2107  r pow 2 *\r
2108  ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2) ==> &4 * pi * r * ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) <=\r
2109  &4 *\r
2110  pi *\r
2111  r pow 2 *\r
2112  abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)) /\\r
2113  &4 / &3 * pi * ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) <=\r
2114  &4 / &3 *\r
2115  pi *\r
2116  r pow 2 *\r
2117  ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / ((k2 + sqrt (&3)) pow 2) `)\r
2118  THEN MP_TAC(MESON[REAL_ARITH `&0 < k2 /\ k2 + sqrt (&3) <= r ==> sqrt(&3)< r`;MESON[SQRT_POS_LT;REAL_ARITH `&0< &3`] `&0< sqrt( &3)`;REAL_ARITH `a:real <b/\ b< c ==> a< c`] `&0 < k2 /\ k2 + sqrt (&3) <= r ==> &0< r`)\r
2119  THEN ASM_SIMP_TAC[bdt1_finiteness] THEN DISCH_TAC THEN REWRITE_TAC[bdt1_finiteness] THEN MP_TAC(REAL_ARITH `&0< k2 ==> &0 <=k2`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_FIELD `&4 *\r
2120      pi *\r
2121      r pow 2 *\r
2122      abs\r
2123      ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3))= ( &4*pi* r* abs\r
2124      ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2))*(r/ (k2+ sqrt(&3)))`] THEN REWRITE_TAC[REAL_FIELD `&4 / &3 *\r
2125      pi *\r
2126      r pow 2 *\r
2127      ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) /\r
2128      ((k2 + sqrt (&3)) pow 2) = (&4 / &3 *\r
2129      pi *((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3))*(r pow 2/ ((k2 + sqrt (&3)) pow 2))`]\r
2130      THEN DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k2+ sqrt(&3):real`;`1:num`] bdt2_finiteness)\r
2131      THEN MP_TAC(MESON[MESON[SQRT_POS_LT;REAL_ARITH `&0< &3`] `&0< sqrt( &3)`;REAL_ARITH `&0 < k2 \r
2132 ==> sqrt(&3)< k2 + sqrt(&3)`;REAL_ARITH `a:real <b/\ b< c ==> a< c`] `&0 < k2 \r
2133 ==> &0< k2 + sqrt(&3)`) THEN  ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ARITH `(x:real) pow 1= x`]\r
2134      THEN DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k2+ sqrt(&3):real`;`2:num`] bdt2_finiteness) THEN ASM_REWRITE_TAC[]\r
2135      THEN REPEAT DISCH_TAC THEN MP_TAC(SPECL [`r:real`;`k1:real`;`k2:real`;`((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2):real`] bdt3_finiteness) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_MESON_TAC[REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;\r
2136 \r
2137 \r
2138 \r
2139 let card_diff_ineq=prove( `!(x:real^3)(k1:real)(k2:real) (r:real). CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))) <= CARD (int_ball x (r+ k1))`,REPEAT GEN_TAC THEN ASSUME_TAC(SPECL [`x:real^3`;`r+ k1:real`] finite_int_ball) THEN ASM_MESON_TAC[CARD_SUBSET;SUBSET_DIFF]);;\r
2140 \r
2141 let bdt6_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0<r) ==> &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2)))) <= &4/ &3*pi*(r+k1+ sqrt(&3))pow 3`,REPEAT STRIP_TAC THEN MP_TAC(GSYM (SPECL [`CARD (int_ball x (r + k1) DIFF int_ball x (r - k2)):num`;`CARD (int_ball x (r+ k1)):num`] REAL_OF_NUM_LE)) THEN SIMP_TAC[card_diff_ineq]\r
2142             THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`r:real`] card_int_ball_le2) THEN ASM_SIMP_TAC[REAL_ARITH `&0< k1 /\ &0< r ==> &0<= k1 /\ &0<= r`] THEN ASM_SIMP_TAC[REAL_ARITH `&0< a ==> &0<= a`] THEN MESON_TAC[REAL_ARITH `a<= b /\ c<=a ==> c<= b`; REAL_ARITH `r + k1 + sqrt (&3)= (r + k1) + sqrt (&3)`]);;\r
2143 \r
2144 (*  Quantifiers corrected by thales below.\r
2145 let bdt5_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ k2 + sqrt (&3) <= r) ==> ?(C:real). &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,REPEAT STRIP_TAC THEN EXISTS_TAC `(&4 / &3 *\r
2146   pi *\r
2147   (&3 * (k1 + k2 + &2 * sqrt (&3)) +\r
2148    ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / (k2 + sqrt (&3)) pow 2 +\r
2149    &3 *\r
2150    abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)))):real`\r
2151                             THEN MP_TAC(ISPECL [`int_ball x (r + k1):real^3 -> bool`;`int_ball x (r - k2):real^3 -> bool`] CARD_DIFF)\r
2152   THEN REWRITE_TAC[finite_int_ball] THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0< k2 ==> r:real -k2 < r + k1`)\r
2153   THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[int_ball_subset]\r
2154   THEN DISCH_TAC THEN MP_TAC(SPECL [`x:real^3`;`r-k2:real`;`r+k1:real`] card_int_ball_ineq)\r
2155   THEN ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN REPEAT DISCH_TAC \r
2156   THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_le) THEN ASM_REWRITE_TAC[]\r
2157   THEN MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_pos) THEN ASM_REWRITE_TAC[]\r
2158   THEN MP_TAC(SPECL [`k1:real`;`k2:real`;`r:real`] bdt4_finiteness) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;\r
2159 *)\r
2160 \r
2161 let bdt5_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) . \r
2162      (&0< k1 /\ &0< k2) ==> ( ?(C:real).  !r.   ( k2 + sqrt (&3) <= r) ==> (&(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2))`,\r
2163   REPEAT STRIP_TAC THEN \r
2164  EXISTS_TAC `(&4 / &3 *  pi *  (&3 * (k1 + k2 + &2 * sqrt (&3)) +   ((k1 + sqrt (&3)) pow 3 + (k2 + sqrt (&3)) pow 3) / (k2 + sqrt (&3)) pow 2 +   &3 *   abs ((k1 + sqrt (&3)) pow 2 - (k2 + sqrt (&3)) pow 2) / (k2 + sqrt (&3)))):real`                          THEN \r
2165   STRIP_TAC THEN\r
2166  MP_TAC(ISPECL [`int_ball x (r + k1):real^3 -> bool`;`int_ball x (r - k2):real^3 -> bool`] CARD_DIFF)  THEN\r
2167  REWRITE_TAC[finite_int_ball] THEN MP_TAC(REAL_ARITH `&0<k1 /\ &0< k2 ==> r:real -k2 < r + k1`)  THEN\r
2168  ASM_REWRITE_TAC[] THEN SIMP_TAC[int_ball_subset]  THEN\r
2169  DISCH_TAC THEN MP_TAC(SPECL [`x:real^3`;`r-k2:real`;`r+k1:real`] card_int_ball_ineq)  THEN\r
2170  ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN REPEAT DISCH_TAC   THEN\r
2171  MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_le) THEN \r
2172 ASM_REWRITE_TAC[]  THEN\r
2173  MP_TAC(SPECL [`x:real^3`;`k1:real`;`k2:real`;`r:real`] card_int_ball_pos) THEN \r
2174 ASM_REWRITE_TAC[]  THEN\r
2175  MP_TAC(SPECL [`k1:real`;`k2:real`;`r:real`] bdt4_finiteness) THEN \r
2176 ASM_REWRITE_TAC[] THEN\r
2177  REAL_ARITH_TAC);;\r
2178 \r
2179 (* fixed quantifier order -thales \r
2180 let bdt7_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). (&0< k1 /\ &0< k2 /\ r< k2 + sqrt (&3) /\ k2 <= r) ==> ?(C:real). &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,\r
2181                   REPEAT STRIP_TAC THEN EXISTS_TAC `(&4/ &3*pi*(k2+k1+ &2*sqrt(&3)) pow 3/ (k2 pow 2)):real`\r
2182             THEN MATCH_MP_TAC(REAL_ARITH `&(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2)))\r
2183 <= &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 /\ &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 <= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2))) <= ( &4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`)             THEN MP_TAC(REAL_ARITH `&0< k2 /\ k2<= r ==> &0< r`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC\r
2184             THEN ASM_SIMP_TAC[SPECL [`x:real^3`;`k1:real`;`k2:real`; `r:real`] bdt6_finiteness]\r
2185             THEN MATCH_MP_TAC(REAL_ARITH `&4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3 \r
2186 <= &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3 /\ &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3 \r
2187 <= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3 <=\r
2188  (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`)\r
2189             THEN MP_TAC(MESON[REAL_ARITH `&0<k1 /\ &0< r ==> sqrt(&3)<= r+k1+ sqrt(&3)`;SPEC `&3:real` SQRT_POS_LE;\r
2190 REAL_ARITH `&0<= &3`;REAL_ARITH `a<=b /\ b<= c ==> a<= c`]  `&0<k1 /\ &0< r ==> &0<= r+k1+ sqrt(&3)`)\r
2191             THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH `r < k2 + sqrt (&3) ==> r+ k1+ sqrt(&3) <= k2+ k1+ &2* sqrt(&3)`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(MESON[PI_POS_LE;REAL_ARITH `&0<= &4/ &3`;REAL_LE_MUL] `&0<= &4/ &3*pi`)\r
2192             THEN REPEAT DISCH_TAC THEN MP_TAC(ISPECL [`3:num`;`r + k1 + sqrt (&3):real`;`k2 + k1 + &2 * sqrt (&3):real`] REAL_POW_LE2) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_ARITH `(a:real)*b*c = (a*b)*c`;REAL_LE_LMUL]\r
2193     THEN DISCH_TAC THEN REWRITE_TAC[REAL_FIELD `((&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2= ((&4 / &3 * pi)*((k2 + k1 + &2 * sqrt (&3)) pow 3))*(r pow 2/ k2 pow 2)`]\r
2194     THEN MP_TAC(MESON[MESON[REAL_POW_LE] `&0 <= r + k1 + sqrt (&3) ==> &0 <= (r + k1 + sqrt (&3)) pow 3`;REAL_ARITH `a<= b /\ b<= c ==> a<= c`] `&0 <= r + k1 + sqrt (&3) /\ (r + k1 + sqrt (&3)) pow 3 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[]   THEN MP_TAC(SPECL [`r:real`;`k2:real`;`2:num`] bdt2_finiteness) THEN ASM_REWRITE_TAC[]\r
2195           THEN REPEAT DISCH_TAC THEN MP_TAC(MESON[REAL_LE_MUL] `&0 <= &4 / &3 * pi /\ &0 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN ASM_REWRITE_TAC[] \r
2196 THEN ASM_MESON_TAC[REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;\r
2197 *)\r
2198 \r
2199 \r
2200 let bdt7_finiteness=prove(`!(x:real^3)(k1:real)(k2:real) (r:real). \r
2201    (&0< k1 /\ &0< k2)  ==>\r
2202    ?(C:real). !r. ( r< k2 + sqrt (&3) /\ k2 <= r) ==> &(CARD ((int_ball x (r+ k1)) DIFF (int_ball x (r- k2))))<= C* r pow 2`,\r
2203                   REPEAT STRIP_TAC THEN \r
2204 EXISTS_TAC `(&4/ &3*pi*(k2+k1+ &2*sqrt(&3)) pow 3/ (k2 pow 2)):real`        THEN \r
2205 REPEAT STRIP_TAC THEN\r
2206 MATCH_MP_TAC(REAL_ARITH `&(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2))) <= &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 /\ &4/ &3*pi*(r+k1+ sqrt(&3))pow 3 <= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &(CARD (int_ball x (r + k1) DIFF int_ball x (r - k2))) <= ( &4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`)             THEN \r
2207 MP_TAC(REAL_ARITH `&0< k2 /\ k2<= r ==> &0< r`) THEN \r
2208 ASM_REWRITE_TAC[] THEN \r
2209 DISCH_TAC           THEN \r
2210 ASM_SIMP_TAC[SPECL [`x:real^3`;`k1:real`;`k2:real`; `r:real`] bdt6_finiteness]      THEN \r
2211 MATCH_MP_TAC(REAL_ARITH `&4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3  <= &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3 /\ &4 / &3 * pi * (k2 + k1 + &2*sqrt (&3)) pow 3  <= (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2 ==> &4 / &3 * pi * (r + k1 + sqrt (&3)) pow 3 <=  (&4 / &3 * pi * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2`)         THEN \r
2212 MP_TAC(MESON[REAL_ARITH `&0<k1 /\ &0< r ==> sqrt(&3)<= r+k1+ sqrt(&3)`;SPEC `&3:real` SQRT_POS_LE; REAL_ARITH `&0<= &3`;REAL_ARITH `a<=b /\ b<= c ==> a<= c`]  `&0<k1 /\ &0< r ==> &0<= r+k1+ sqrt(&3)`)            THEN \r
2213 ASM_REWRITE_TAC[] THEN \r
2214 MP_TAC(REAL_ARITH `r < k2 + sqrt (&3) ==> r+ k1+ sqrt(&3) <= k2+ k1+ &2* sqrt(&3)`) THEN \r
2215 ASM_REWRITE_TAC[] THEN \r
2216 MP_TAC(MESON[PI_POS_LE;REAL_ARITH `&0<= &4/ &3`;REAL_LE_MUL] `&0<= &4/ &3*pi`)      THEN \r
2217 REPEAT DISCH_TAC THEN \r
2218 MP_TAC(ISPECL [`3:num`;`r + k1 + sqrt (&3):real`;`k2 + k1 + &2 * sqrt (&3):real`] REAL_POW_LE2) THEN \r
2219 ASM_REWRITE_TAC[] THEN \r
2220 ASM_SIMP_TAC[REAL_ARITH `(a:real)*b*c = (a*b)*c`;REAL_LE_LMUL]     THEN \r
2221 DISCH_TAC THEN \r
2222 REWRITE_TAC[REAL_FIELD `((&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3 / k2 pow 2) * r pow 2= ((&4 / &3 * pi)*((k2 + k1 + &2 * sqrt (&3)) pow 3))*(r pow 2/ k2 pow 2)`]     THEN \r
2223 MP_TAC(MESON[MESON[REAL_POW_LE] `&0 <= r + k1 + sqrt (&3) ==> &0 <= (r + k1 + sqrt (&3)) pow 3`;REAL_ARITH `a<= b /\ b<= c ==> a<= c`] `&0 <= r + k1 + sqrt (&3) /\ (r + k1 + sqrt (&3)) pow 3 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN \r
2224 ASM_REWRITE_TAC[]   THEN \r
2225 MP_TAC(SPECL [`r:real`;`k2:real`;`2:num`] bdt2_finiteness) THEN \r
2226 ASM_REWRITE_TAC[]         THEN \r
2227 REPEAT DISCH_TAC THEN \r
2228 MP_TAC(MESON[REAL_LE_MUL] `&0 <= &4 / &3 * pi /\ &0 <= (k2 + k1 + &2 * sqrt (&3)) pow 3 ==> &0<= (&4 / &3 * pi) * (k2 + k1 + &2 * sqrt (&3)) pow 3`) THEN \r
2229 ASM_REWRITE_TAC[]  THEN \r
2230 ASM_MESON_TAC[REAL_LE_LMUL;REAL_ARITH ` a* &1= a`]);;  \r
2231 \r
2232 let REAL_LE_SQUARE_POW =\r
2233 MESON[REAL_POW_2; REAL_LE_SQUARE]`! x. &0 <= x pow 2 `;;\r
2234 \r
2235 \r
2236 (*--------------------------------------------------------------------*)\r
2237 (*Lemma 2.16 [TXIWYHI] Bound of number of int points between two balls*)\r
2238 (*--------------------------------------------------------------------*)\r
2239 \r
2240 let TXIWYHI=prove( `!(x:real^3)(k1:real)(k2:real) (r:real). \r
2241     (&0< k1 /\ &0< k2) ==> ?(C:real). !r. (k2 <= r)  ==>\r
2242      &(CARD (integer_point (ball(x,r+ k1) DIFF ball(x,r- k2))))<= C* r pow 2`, \r
2243   REPEAT GEN_TAC THEN SIMP_TAC[eq_def_intball]  THEN \r
2244 REPEAT STRIP_TAC THEN \r
2245 SUBGOAL_THEN `?C. !r. k2+sqrt(&3) <= r ==> &(CARD   (int_ball x (r + k1) DIFF int_ball x (r - k2))) <=                  C * r pow 2` ASSUME_TAC THENL\r
2246  [ASM_MESON_TAC[bdt5_finiteness];ALL_TAC] THEN\r
2247 SUBGOAL_THEN `(?C. !r. r < k2 + sqrt (&3) /\ k2 <= r                      ==> &(CARD                           (int_ball x (r + k1) DIFF int_ball x (r - k2))) <=                          C * r pow 2)` ASSUME_TAC THENL\r
2248  [ASM_MESON_TAC[bdt7_finiteness];ALL_TAC] THEN\r
2249  FIRST_X_ASSUM CHOOSE_TAC THEN\r
2250  FIRST_X_ASSUM CHOOSE_TAC THEN\r
2251  EXISTS_TAC `(abs(C:real)+abs(C':real))` THEN\r
2252   GEN_TAC THEN\r
2253   STRIP_TAC THEN\r
2254   MATCH_MP_TAC (REAL_ARITH `(?b. (a<=b /\ b<=c) ) ==> (a <= c)`) THEN\r
2255 SUBGOAL_THEN `(C*r pow 2 <= (abs(C)+abs(C'))* r pow 2) /\ (C'*r pow 2 <= (abs(C)+abs(C')) * r pow 2)` MP_TAC  THENL\r
2256  [CONJ_TAC THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_LE_SQUARE_POW] THEN REAL_ARITH_TAC;ALL_TAC] THEN\r
2257  REPEAT STRIP_TAC THEN\r
2258 DISJ_CASES_TAC(REAL_ARITH `(r:real)< k2+ sqrt(&3) \/ (k2+ sqrt(&3)<= r)`)  THEN\r
2259 ASM_MESON_TAC[]\r
2260 );;\r
2261 \r
2262 (* old version with reversed quantifiers -thales\r
2263 let TXIWYHI=prove( `!(x:real^3)(k1:real)(k2:real) (r:real). \r
2264     (&0< k1 /\ &0< k2 /\ k2 <= r) ==> ?(C:real).\r
2265      &(CARD (integer_point (ball(x,r+ k1) DIFF ball(x,r- k2))))<= C* r pow 2`, \r
2266   REPEAT GEN_TAC THEN SIMP_TAC[eq_def_intball]\r
2267   THEN STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `(r:real)< k2+ sqrt(&3) \/ (k2+ sqrt(&3)<= r)`)\r
2268   THENL [ASM_MESON_TAC[bdt7_finiteness];ASM_MESON_TAC[bdt5_finiteness]]);;\r
2269 *)\r
2270 \r
2271 (*--------------------------------------------------------------------*)\r
2272 \r
2273 \r
2274 end;;\r