legacy/oldnonlinear/nonlinear/text_interface.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: nonlinear inequalities                                                             *)
   5 (* Author:  Thomas Hales     *)
   6 (* Date: 2011-04-29                                                    *)
   7 (* ========================================================================== *)
   8
   9 (*
  10
  11 This file translates the low-level nonlinear inequalities into the higher-level form
  12 in which they are used in the text part of the proof.
  13
  14 Make a constant for each computer calculation of the text.
  15 *)
  16
  17
  18 module Text_interface = struct
  19 1;;
  20
  21   let get_flypaper_filter s idv =
  22      mem s (Ineq.flypaper_ids idv);;
  23
  24   let get_flypaper s = List.filter (get_flypaper_filter s) (!Ineq.ineqs);;
  25
  26   let packing_chapter = ["TSKAJXY";"OXLZLEZ";"BIEFJHU";"WAZLDCD";"UKBRPFE"];;
  27
  28   let local_chapter = ["SDCCMGA";"UPONLFY";"OUCPLRI";"OMKYNLT";"2986512815";
  29    "JNTEFVP";"PQFYWHW";"GYQVFXJ";"ZHPXLTX"];;
  30
  31   let tame_chapter = ["TVAWGDR";"KCBLRQC"];;
  32
  33   let further_chapter = ["TNVWUGK";"ZVLLGZK"];;
  34
  35    Ineq.all_flypaper();;
  36
  37   let TSKAJXY_idvs = get_flypaper "TSKAJXY";;
  38
  39   let OXLZLEZ_idvs = get_flypaper "OXLZLEZ";;
  40
  41   let ineq_tm u = u.ineq;;
  42   let tms_of_ls = map ineq_tm o Ineq.getexact;;
  43
  44 let packing_TSKAJXY = list_mk_conj (map ineq_tm TSKAJXY_idvs);;
  45
  46 let TSKAJXY_HYPa = new_definition (mk_eq(`TSKAJXY_HYPa:bool`,packing_TSKAJXY));;
  47
  48
  49 let overlooked idv =
  50  List.length  (List.filter (function Flypaper _ -> true | Lp -> true | Lp_aux _ -> true | _ -> false) idv.tags) = 0;;
  51
  52 let ovv = List.filter overlooked (!Ineq.ineqs);;
  53
  54 map (fun r -> r.idv) ovv;;
  55
  56 end;;