text_formalization/leg/enclosed_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: enclosed                                                       *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 The function of 9 variables defined on page 37 of the Kepler Conjecture, DCG vol 36(1), July 2006
  15 It is generally typeset as a calligraphic E.
  16
  17 It is a quadratic with nonnegative leading coefficient.
  18 *)
  19
  20
  21
  22 module type Enclosed_def_type = sig
  23   val enclosed : thm
  24   val quad_cross_diag2_x : thm
  25 end;;
  26
  27
  28 flyspeck_needs "leg/muR_def.hl";;
  29
  30 (*
  31 flyspeck_needs "leg/abc_of_quadratic_def.hl";;
  32 flyspeck_needs "leg/quadratic_root_plus_def.hl";;
  33 *)
  34
  35
  36 module Enclosed : Enclosed_def_type = struct
  37
  38   let quadratic_root_plus = Sphere.quadratic_root_plus;;
  39   let abc_of_quadratic = Sphere.abc_of_quadratic;;
  40   let muR = Mur.muR;;
  41
  42  let enclosed =
  43    new_definition `enclosed y1 y2 y3 y4 y5 y6 y7 y8 y9 = sqrt
  44    (quadratic_root_plus (abc_of_quadratic (muR y1 y2 y3 y4 y5 y6 y7 y8 y9)))`;;
  45
  46  let quad_cross_diag2_x = new_definition
  47   `quad_cross_diag2_x x1 x2 x3 x4 x5 x6 x7 x8 x9 =
  48     enclosed (sqrt x1) (sqrt x5) (sqrt x6) (sqrt x4) (sqrt x2) (sqrt x3)  (sqrt x7)  (sqrt x8)  (sqrt x9)`;;
  49
  50 end;;
  51