(*

Volume files

Author: Thomas Hales

Date: 2010-02-08

*)

let RADIAL_NORM_RADIAL = prove(`radial_norm = radial`,
   REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;radial_norm;radial] 
				);;

let EVENTUALLY_RADIAL_UNNORM = prove(`eventually_radial_norm = eventually_radial`,
   REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;RADIAL_NORM_RADIAL;eventually_radial_norm;eventually_radial] 				    );;



(* LBWOPAH *)

let RADIAL_EVENTUALLY_RADIAL = prove(`!C x:real^N. (?r. (r> &0) /\ radial r x C) ==> eventually_radial x C`,
    REWRITE_TAC[radial;eventually_radial] THEN
    REPEAT STRIP_TAC THEN
    REWRITE_TAC[SET_RULE`x IN a INTER b <=> x IN a /\ x IN b`] THEN
    EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[] THEN
   CONJ_TAC THENL
   [
    (*1*) ASM_MESON_TAC[SET_RULE `a SUBSET b ==> a INTER b SUBSET b`];
    (*2*) ALL_TAC
    ] THEN
    REPEAT STRIP_TAC THENL
    [
    (*1*)ASM_MESON_TAC[];
     (*2*)ALL_TAC
    ] THEN
    REWRITE_TAC[IN_BALL;dist;VECTOR_ARITH `x:real^N -(x+y) = -- y`;NORM_MUL;NORM_NEG] THEN
    ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> (abs t =  t)`] 
			     );;

let LBWOPAH = RADIAL_EVENTUALLY_RADIAL;;


(* -- to here --
let VQFENMT1 = prove(`!r x C. volume_prop vol /\ measurable C /\ radial_norm r x C ==> 
  (vol C = sol C x * (r pow 3)/(&3))`,

  );;
*)

(* -- work in progres --
let VQFENMT2 = prove(`!x C. 
   volume_prop vol /\ measurable C /\ (?r. (r > &0) /\ (!y. y IN C ==> dist(x,y) >= r)) ==>
   eventually_radial_norm x C /\ (sol C (x:real^3) = &0)`,
   REWRITE_TAC[TAUT `(a ==> b /\ c) = ((a ==> b) /\ (a /\ b ==> c))`] THEN 
   STRIP_TAC THEN STRIP_TAC THEN
   CONJ_TAC THEN
   REWRITE_TAC[eventually_radial_norm;radial_norm] THEN
   REPEAT STRIP_TAC THEN
   REWRITE_TAC[NORMBALL_BALL] THEN
   EXISTS_TAC `r:real` THEN
   ASM_REWRITE_TAC[INTER_SUBSET] THEN
   GEN_TAC THEN
     SUBGOAL_THEN `C INTER ball((x:real^3),r) = EMPTY` ASSUME_TAC THEN
   (* branch 1 *)
   REWRITE_TAC[ball] THEN
   ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
   REWRITE_TAC[elimin NOT_IN_EMPTY;elimin IN_INTER;elimin IN_ELIM_THM] THEN
   ASM_MESON_TAC[IN;REAL_ARITH `!a b. a >= b ==> ~(a < b)`] THEN
   (* branch 2 *)
   ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
   (* branch 3 *)
   REPEAT STRIP_TAC THEN

*)