Question: given the string of a theorem "IN_ELIM_THM", how can I access the theorem IN_ELIM_THM? Or given a string of a thm_list->tactic "MESON_TAC", how can I access MESON_TAC? This is a problem that Freek must have solved in miz3.ml, but I can't figure out how. John did not seem to solve it in mizar.ml, as his readable proof of the Knaster-Tarski fixpoint theorem is prefaced by
e(LABEL_TAC "IN_ELIM_THM" IN_ELIM_THM);; It seems to me that we should be able to do this with assoc "IN_ELIM_THM" env;; where env is some association list of pairs given by labels and theorems. Or maybe just an association list of the module Hol.thm. Something like this is explained in an example in the Ocaml manual: http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html#toc10 We first define a function to evaluate an expression given an environment that maps variable names to their values. For simplicity, the environment is represented as an association list. Another reason to think this can be done is that we can do it with term variables. As Konrad was explaining, if you have a string "x" and the type `:alpha` of a variable x, you can recover x with mk_var("x",`:alpha`). Isn't that correct? I don't see why something like this shouldn't work more generally than for term variables. My string/parser/readability project was going great until I ran into this problem. Below is the progress I made so far, which is mainly interesting as it shows I can use the str library, and that the parser can be easily used to get the math characters of HOL4 and Isabelle. Plus I finally threw and caught exceptions! -- Best, Bill #load "str.cma";;. let parse_qproof s = (String.sub s 1 (String.length s - 1));; let (make_env: goal -> (string * pretype) list) = fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var) (freesl (w::(map (concl o snd) asl)));; let parse_env_string env s = (term_of_preterm o retypecheck env) ((fst o parse_preterm o lex o explode) s);; let (exists_TAC: string -> tactic) = fun stm (asl,w) -> let env = make_env (asl,w) in EXISTS_TAC (parse_env_string env stm) (asl,w);; let ConvertToHOL s = try let len = Str.search_forward (Str.regexp "INTRO_TAC") s 0 in INTRO_TAC (String.sub s (len + 9) ((String.length s) - len - 9)) with Not_found -> try let len = Str.search_forward (Str.regexp "exists_TAC") s 0 in exists_TAC (String.sub s (len + 10) ((String.length s) - len - 10)) with Not_found -> ALL_TAC;; let rec OrganizeTHEN s = try let len = Str.search_forward (Str.regexp "THEN") s 0 in (ConvertToHOL (String.sub s 0 len)) THEN (OrganizeTHEN (String.sub s (len + 4) ((String.length s) - len - 4))) with Not_found -> ALL_TAC;; let StringToTac s = let s = Str.global_replace (Str.regexp "⇒") "==>" s in let s = Str.global_replace (Str.regexp "⇔") "<=>" s in let s = Str.global_replace (Str.regexp "∧ ") "/\\ " s in let s = Str.global_replace (Str.regexp "∨") "\\/" s in let s = Str.global_replace (Str.regexp "¬") "~" s in let s = Str.global_replace (Str.regexp "∀") "!" s in let s = Str.global_replace (Str.regexp "∃") "?" s in let s = Str.global_replace (Str.regexp "λ") "\\" s in OrganizeTHEN s;; g `!P. (!x. ?y. P x y) ==> ?f. !x. P x (f x)`;; e(StringToTac `;INTRO_TAC !P; H1 THEN exists_TAC \x. @y. P x y THEN HYP MESON_TAC "H1" []`);; ------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite It's a free troubleshooting tool designed for production Get down to code-level detail for bottlenecks, with <2% overhead. Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap2 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
