(* summary of the volume chapter *)

(*
Known issues:

-- TXIWYHI has quantifiers in the wrong order. It should be ?C. !r.

-- JJFHOIW_t not formalized.

-- ATOAPUN missing the additivity of volumes

-- PUACSHX (Project Issue 5), mismatch between volume_prop vol and volume_props.
  This affects all theorems with assumption `volume_prop vol`

-- NULLSET and vol are pretty printed versions of negligible and measure, specialized to R^3,
    so searches don't show all the general theorems
*)



let OWCZKJR = NULLSET_RULES;;

(* more NULLSET props *)
let NULLSET_INTER = prove(`!s t. NULLSET s /\ NULLSET t ==>
   NULLSET (s INTER t)`,
  SIMP_TAC[NEGLIGIBLE_INTER]);;
 
let NULLSET_SUBSET = prove(`!s t. NULLSET s /\ t SUBSET s ==> NULLSET t`,
  MESON_TAC[NEGLIGIBLE_SUBSET]);;

let NULLSET_DIFF = prove(`!s t. NULLSET s ==> NULLSET(s DIFF t)`,
  SIMP_TAC[NEGLIGIBLE_DIFF]);;

let NUKRQDI = MEASURABLE_RULES;;

(* Background in Measure *)


let ATOAPUN = volume_props;;  

(* volume_props doesn't give additivity of measure.  Here it is. *)

let VOL_DISJOINT_UNION = prove(` !s t. 
           measurable s /\ measurable t /\ DISJOINT s t
           ==> vol (s UNION t) = vol s + vol t`,
	SIMP_TAC[MEASURE_DISJOINT_UNION]		      );;

let VOL_NULLSET_UNION= prove(` !s t.
           measurable s /\ measurable t /\ NULLSET (s INTER t)
           ==> vol (s UNION t) = vol s + vol t`,
      SIMP_TAC[MEASURE_NEGLIGIBLE_UNION]			       );;

let VOL_UNION_LE=prove(` !s t.
           measurable s /\ measurable t
           ==> vol (s UNION t) <= vol s + vol t`,
		SIMP_TAC[MEASURE_UNION_LE]      );;

(* unwedged versions *)

let ATOAPUN1 = VOLUME_CONIC_CAP;;
let ATOAPUN2 = VOLUME_CONIC_CAP_STRONG;;
let ATOAPUN3 = VOLUME_BALL;;
let ATOAPUN4 = VOLUME_FRUSTT;;
let ATOAPUN5 = VOLUME_FRUSTT_STRONG;;

(* Primitive Volume *)

(* radial set *)

let VSPMVNR1 = ball;;
let VSPMVNR2 = cball;;
let VSPMVNR = [VSPMVNR1;VSPMVNR2];;

(* duplicate definition : normball = ball *)

let QPHVSMZ1 = radial;;
let QPHVSMZ2 = eventually_radial;;
let QPHVSMZ3 = radial_norm;;
let QPHVSMZ4 = eventually_radial_norm;;
let QPHVSMZ5 = NORMBALL_BALL;;
let  QPHVSMZ = [ QPHVSMZ1; QPHVSMZ2; QPHVSMZ3;QPHVSMZ4;QPHVSMZ5];;

 let KODOBRF = inter_radial;;

 let LBWOPAH = "not found";;

let PUACSHX = lemma_r_r'_fix;;   

let MASYUQQ = sol;;  


(* to here *)
(* 2.2.1 wedge *)
let wedge = wedge;;

(* Lemma 2.4 [VICUATE] need to check - found in Multivariate/flyspeck.ml *)
let VICUATE = WEDGE_LUNE;;

(* Definition 2.4 Solid Triangle *)
let solid_triangle = solid_triangle;;

(* Definition 2.5 Conic Cap *)
let conic_cap = conic_cap;;

(* Definition 2.6 rcone label{def:p:rcone}
   - a collection of different rcones  label{def:p:rcone} *)
let rcone_gt = rcone_gt;;
let rcone_ge = rcone_ge;;
(* < version from the definition wasn't found in flyspeck.ml *)
let rcone_eq = rcone_eq;;

(* Definition 2.7 frustum *)
let frustum = frustum;;

(* Definition 2.8 tetrahedron *)
let tetrahedron = conv0;;

(* Definition 2.9 Primitive label{def:primitive} *)
let primitive = primitive;;

(* volume calculations *)

(* Lemma 2.5 [PAZNHPZ] label{lemma:prim-volume} - found in Multivariate/flyspeck.ml*)
(* 

VOLUME_SOLID_TRIANGLE, VOLUME_CONIC_CAP, VOLUME_FRUSTT, VOLUME_OF_TETRAHEDRON, vol_rect, VOLUME_BALL_WEDGE combine to 
 form the lemma *)

(* Lemma 2.6 [DFNVMFM] label{lemma:wedge-vol} need to check - found in Multivariate/flyspeck.ml *)
let DFNVMFM = VOLUME_BALL_WEDGE;;

(* Lemma 2.7 [FMSWMVO] label{lemma:wedge-sol}*)
(* not found *)

(* Lemma 2.8 [FUPXNLC] label{lemma:prim-sol} *)
(* not found *)

(* Lemma 2.9 [WFFVGVF] *)
(* not found *)
 
(* Lemma 2.10 [CZOQFNL] label{lemma:wedge:sol}  not sure if this one is correct...found in Multivariate/flyspeck.ml *)
let CZOQFNL = WEDGE_LUNE_GT;;

(* Lemma 2.11 [OXQZBJG] *)
(* not formalized *)

(* Definition 2.10 (orthosimplex, orth)  label{def:ortho} *)
(*found in sphere.hl *)
 let ortho0 = ortho0;;

(* Definition 2.11 (Rogers simplex, rog) label{def:rog} *)
(*both found in sphere.hl *)
(*
 let rogers0 = rogers0;;
 let rogers = rogers;;  
*)

(* Lemma 2.12 [XQBOVQF] *)
(* not formalized *)

(* Definition 2.12 (circumradius) label{def:etaV} *)
(* found in sphere.hl*)
 let radV = radV;;

(* Definition 2.13 (abc parameter) label{def:abc} *)
(*found in sphere.hl *)
 let abc_parameter = abc_param;; 


(* Lemma 2.13 [JJFHOIW] label{lemma:rog:abc} *)
(* didn't find an actual lemma for this, but I found the equations from the lemma in sphere.hl *)
 let JJFHOIW1 = volR;;
 let JJFHOIW2 = solR;;
 let JJFHOIW3 = dihR;;
 let JJFHOIW = "not found";;

 let orthosimplex = define `orthosimplex (v0:real^N) e1 e2 e3 a b c = 
   let v1 = v0 + a % e1 in
   let v2 = v1 + sqrt(b pow 2 - a pow 2) % e2 in
   let v3 = v2 + sqrt(c pow 2 - b pow 2) % e3 in
   conv0 {v0, v1, v2, v3}`;;

 let JJFHOIW_t = `!v0 e1 e2 e3 a b c.
   (orthonormal e1 e2 e3 /\ &0 < a /\ a <= b /\ b <= c) ==>

   (vol(orthosimplex v0 e1 e2 e3 a b c) = volR a b c)/\
   (sol (orthosimplex v0 e1 e2 e3 a b c) v0 = solR a b c) /\
   (dih(orthosimplex v0 e1 e2 e3 a b c) = dihR a b c)`;;

(* Finiteness and Volume *)
 type_of `orthosimplex`;;
 type_of `orthonormal`;;
 type_of `sol`;;

let  WQZISRI =  WQZISRI;;   

let PWVIIOL = PWVIIOL;;  

(* lattice shell *)
let TXIWYHI = TXIWYHI;;