(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Calculate Numeric constants                                                                  *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-27                                                           *)
(* ========================================================================== *)


module Flyspeck_constants = struct

  open Sphere;;

  let conv_of (s,t) = (s,PURE_ONCE_REWRITE_CONV[t]);;
  
  let convl = [
  conv_of ("sqrt2",sqrt2);
  conv_of ("sqrt3",sqrt3);
  conv_of ("sqrt8",sqrt8);
  conv_of ("sol0",sol0);
  conv_of("tau0",tau0);
  conv_of("mm1",mm1);
  conv_of("mm2",mm2);
  conv_of("pi_rt18",pi_rt18);
  conv_of("hplus",hplus);
  ];;

  let calc = snd o  (Float.REAL_INEQUALITY_CALCULATOR convl)  ;;

  let bounds = calc `#1.414213 < sqrt2 /\ sqrt2 < #1.414214 /\
   #2.828427 < sqrt8 /\ sqrt8 < #2.828428 /\
   #1.732  < sqrt3 /\ sqrt3 < #1.7321 /\
   #3.14159 < pi /\ pi < #3.1416 /\
   #0.551285 < sol0 /\ sol0 < #0.551286 /\
   #1.54065 < tau0 /\ tau0 < #1.54066 /\
   #0.740480 < pi_rt18 /\ pi_rt18 < #0.740481 /\
   #1.012080 < mm1 /\ mm1 < #1.012081 /\
   #0.02541 < mm2 /\ mm2 < #0.02542 /\
   &0 < ((sqrt (&2) - &1) * &5 * (hplus - &1)) /\
   &0 < sqrt(&2) - hplus /\
   &0 < hplus - &1 `;;


end;;