(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: enclosed                                                       *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)




(*
The function of 9 variables defined on page 37 of the Kepler Conjecture, DCG vol 36(1), July 2006
It is generally typeset as a calligraphic E.

It is a quadratic with nonnegative leading coefficient.
*)



module type Enclosed_def_type = sig
  val enclosed : thm
  val quad_cross_diag2_x : thm
end;;


flyspeck_needs "leg/muR_def.hl";;

(*
flyspeck_needs "leg/abc_of_quadratic_def.hl";;
flyspeck_needs "leg/quadratic_root_plus_def.hl";;
*)


module Enclosed : Enclosed_def_type = struct

  let quadratic_root_plus = Sphere.quadratic_root_plus;;
  let abc_of_quadratic = Sphere.abc_of_quadratic;;
  let muR = Mur.muR;;

 
let enclosed = 
   new_definition `enclosed y1 y2 y3 y4 y5 y6 y7 y8 y9 = sqrt 
   (quadratic_root_plus (abc_of_quadratic (muR y1 y2 y3 y4 y5 y6 y7 y8 y9)))`;;
 
let quad_cross_diag2_x = new_definition 
  `quad_cross_diag2_x x1 x2 x3 x4 x5 x6 x7 x8 x9 = 
    enclosed (sqrt x1) (sqrt x5) (sqrt x6) (sqrt x4) (sqrt x2) (sqrt x3)  (sqrt x7)  (sqrt x8)  (sqrt x9)`;;
end;;