1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: nonlinear inequalities *)
5 (* Author: Thomas Hales *)
7 (* ========================================================================== *)
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.
14 Make a constant for each computer calculation of the text.
18 module Text_interface = struct
21 let get_flypaper_filter s idv =
22 mem s (Ineq.flypaper_ids idv);;
24 let get_flypaper s = List.filter (get_flypaper_filter s) (!Ineq.ineqs);;
26 let packing_chapter = ["TSKAJXY";"OXLZLEZ";"BIEFJHU";"WAZLDCD";"UKBRPFE"];;
28 let local_chapter = ["SDCCMGA";"UPONLFY";"OUCPLRI";"OMKYNLT";"2986512815";
29 "JNTEFVP";"PQFYWHW";"GYQVFXJ";"ZHPXLTX"];;
31 let tame_chapter = ["TVAWGDR";"KCBLRQC"];;
33 let further_chapter = ["TNVWUGK";"ZVLLGZK"];;
37 let TSKAJXY_idvs = get_flypaper "TSKAJXY";;
39 let OXLZLEZ_idvs = get_flypaper "OXLZLEZ";;
41 let ineq_tm u = u.ineq;;
42 let tms_of_ls = map ineq_tm o Ineq.getexact;;
44 let packing_TSKAJXY = list_mk_conj (map ineq_tm TSKAJXY_idvs);;
46 let TSKAJXY_HYPa = new_definition (mk_eq(`TSKAJXY_HYPa:bool`,packing_TSKAJXY));;
50 List.length (List.filter (function Flypaper _ -> true | Lp -> true | Lp_aux _ -> true | _ -> false) idv.tags) = 0;;
52 let ovv = List.filter overlooked (!Ineq.ineqs);;
54 map (fun r -> r.idv) ovv;;