(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: nonlinear inequalities                                                             *)
(* Author:  Thomas Hales     *)
(* Date: 2011-04-29                                                    *)
(* ========================================================================== *)

(*

This file translates the low-level nonlinear inequalities into the higher-level form
in which they are used in the text part of the proof.

Make a constant for each computer calculation of the text.
*)


module Text_interface = struct
1;;

  let get_flypaper_filter s idv =
     mem s (Ineq.flypaper_ids idv);;
  
  let get_flypaper s = List.filter (get_flypaper_filter s) (!Ineq.ineqs);;

  let packing_chapter = ["TSKAJXY";"OXLZLEZ";"BIEFJHU";"WAZLDCD";"UKBRPFE"];;

  let local_chapter = ["SDCCMGA";"UPONLFY";"OUCPLRI";"OMKYNLT";"2986512815";
   "JNTEFVP";"PQFYWHW";"GYQVFXJ";"ZHPXLTX"];;

  let tame_chapter = ["TVAWGDR";"KCBLRQC"];;

  let further_chapter = ["TNVWUGK";"ZVLLGZK"];;

   Ineq.all_flypaper();;

  let TSKAJXY_idvs = get_flypaper "TSKAJXY";;

  let OXLZLEZ_idvs = get_flypaper "OXLZLEZ";;

  let ineq_tm u = u.ineq;;
  let tms_of_ls = map ineq_tm o Ineq.getexact;;
 
let packing_TSKAJXY = list_mk_conj (map ineq_tm TSKAJXY_idvs);;

let TSKAJXY_HYPa = new_definition (mk_eq(`TSKAJXY_HYPa:bool`,packing_TSKAJXY));;

let overlooked idv =
 List.length  (List.filter (function Flypaper _ -> true | Lp -> true | Lp_aux _ -> true | _ -> false) idv.tags) = 0;;

let ovv = List.filter overlooked (!Ineq.ineqs);;

map (fun r -> r.idv) ovv;;

end;;