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

Reply via email to