legacy/oldvolume/ch_volume/vol2.hl

   1 (*
   2
   3 Volume files
   4
   5 Author: Thomas Hales
   6
   7 Date: 2010-02-08
   8
   9 *)
  10
  11 let RADIAL_NORM_RADIAL = prove(`radial_norm = radial`,
  12    REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;radial_norm;radial]
  13                                 );;
  14
  15 let EVENTUALLY_RADIAL_UNNORM = prove(`eventually_radial_norm = eventually_radial`,
  16    REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;RADIAL_NORM_RADIAL;eventually_radial_norm;eventually_radial]                                );;
  17
  18
  19
  20 (* LBWOPAH *)
  21
  22 let RADIAL_EVENTUALLY_RADIAL = prove(`!C x:real^N. (?r. (r> &0) /\ radial r x C) ==> eventually_radial x C`,
  23     REWRITE_TAC[radial;eventually_radial] THEN
  24     REPEAT STRIP_TAC THEN
  25     REWRITE_TAC[SET_RULE`x IN a INTER b <=> x IN a /\ x IN b`] THEN
  26     EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[] THEN
  27    CONJ_TAC THENL
  28    [
  29     (*1*) ASM_MESON_TAC[SET_RULE `a SUBSET b ==> a INTER b SUBSET b`];
  30     (*2*) ALL_TAC
  31     ] THEN
  32     REPEAT STRIP_TAC THENL
  33     [
  34     (*1*)ASM_MESON_TAC[];
  35      (*2*)ALL_TAC
  36     ] THEN
  37     REWRITE_TAC[IN_BALL;dist;VECTOR_ARITH `x:real^N -(x+y) = -- y`;NORM_MUL;NORM_NEG] THEN
  38     ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> (abs t =  t)`]
  39                              );;
  40
  41 let LBWOPAH = RADIAL_EVENTUALLY_RADIAL;;
  42
  43
  44 (* -- to here --
  45 let VQFENMT1 = prove(`!r x C. volume_prop vol /\ measurable C /\ radial_norm r x C ==>
  46   (vol C = sol C x * (r pow 3)/(&3))`,
  47
  48   );;
  49 *)
  50
  51 (* -- work in progres --
  52 let VQFENMT2 = prove(`!x C.
  53    volume_prop vol /\ measurable C /\ (?r. (r > &0) /\ (!y. y IN C ==> dist(x,y) >= r)) ==>
  54    eventually_radial_norm x C /\ (sol C (x:real^3) = &0)`,
  55    REWRITE_TAC[TAUT `(a ==> b /\ c) = ((a ==> b) /\ (a /\ b ==> c))`] THEN
  56    STRIP_TAC THEN STRIP_TAC THEN
  57    CONJ_TAC THEN
  58    REWRITE_TAC[eventually_radial_norm;radial_norm] THEN
  59    REPEAT STRIP_TAC THEN
  60    REWRITE_TAC[NORMBALL_BALL] THEN
  61    EXISTS_TAC `r:real` THEN
  62    ASM_REWRITE_TAC[INTER_SUBSET] THEN
  63    GEN_TAC THEN
  64      SUBGOAL_THEN `C INTER ball((x:real^3),r) = EMPTY` ASSUME_TAC THEN
  65    (* branch 1 *)
  66    REWRITE_TAC[ball] THEN
  67    ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
  68    REWRITE_TAC[elimin NOT_IN_EMPTY;elimin IN_INTER;elimin IN_ELIM_THM] THEN
  69    ASM_MESON_TAC[IN;REAL_ARITH `!a b. a >= b ==> ~(a < b)`] THEN
  70    (* branch 2 *)
  71    ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
  72    (* branch 3 *)
  73    REPEAT STRIP_TAC THEN
  74
  75 *)