Freek Wiedijk answered a question: "string_of_term" and then "parse_term" take terms to strings and strings to terms. Using "parse_term", I made a start toward Freek's miz3 interface which doesn't use backquotes and require the extra type annotations. It also uses Marco Maggesi's new DESTRUCT_TAC:
let CONSIDER_TAC vars_string lab t_string prfs = match prfs with p::ps -> (warn (ps <> []) "CONSIDER_TAC: additional subproofs ignored"; let tm = parse_term ("?" ^ vars_string ^ "." ^ t_string) in SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars_string ^ "." ^ lab)) THENL [p; ALL_TAC]) | [] -> failwith "CONSIDER_TAC: no subproof given";; let CASES_TAC sDestruct sDisjlist tac = let rec list_mk_string_disj sDisjlist = match sDisjlist with [] -> "" | s::[] -> "(" ^ s ^ ")" | s::ls -> "(" ^ s ^ ") \\/ " ^ list_mk_string_disj ls in let disjthm = parse_term (list_mk_string_disj sDisjlist) in SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM (DESTRUCT_TAC sDestruct);; By using strings assembled by ^ and then transformed to terms by parse_term, I can avoid the extra type annotations that arise from typing each of the terms that would be assembled by term functions, in this case mk_exists and list_mk_disj. I'm not quite happy with CONSIDER_TAC. I'd prefer the usage to be consider "M such that M = transp(vector[v:real^2;w:real^2]):real^2^2" " Mexists" [MESON_TAC[]] and I bet this can be done with Ocaml string functions, which would remove the substring "such that" and then call the above version CONSIDER_TAC "M" "Mexists" "M = transp(vector[v:real^2;w:real^2]):real^2^2" [MESON_TAC[]] but I haven't learned how yet. Notice the improvement due to Freek's parse_term and Marco's DESTRUCT_TAC: the first M has no type annotation. -- Best, Bill ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_mar _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info