legacy/glpk/glpk/glpk_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma:  Main Linear Programs                                                      *)
   5 (* Chapter:                                                                *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-06-14                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 (*
  12 This file contains definitions related to the main linear programming model.
  13 *)
  14
  15 (*
  16 changes
  17 delta0 -> sol0
  18
  19 *)
  20
  21 let sol0 = new_definition `sol0 = &3 * acs (&1 / &3)  - pi`;;
  22 let rhom = new_definition `rhom y = &1 + sol0 / pi - lfun (y/ &2) * sol0/pi`;;
  23 let rho218 = new_definition `rho218 = rhom (#2.18)`;;
  24 let tgt_exact = new_definition `tgt_exact = &4 * pi - &20 * sol0`;;
  25
  26 (* The model has a hypermap (D,e,n,f) with
  27     set of nodes V, edges E, faces F,
  28
  29    std_faces_not_super : set of faces.
  30    super8 : set of faces.
  31    superduperq : set of faces.
  32    ....
  33
  34    declare a type for decorated hypermaps.
  35
  36
  37    Each standard fan gives a decorated hypermap.
  38
  39  *)