Hi Bill
2013/5/4 Bill Richter <rich...@math.northwestern.edu>
> 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?
# let get = Obj.magic o Toploop.getvalue;;
val get : string -> 'a = <fun>
# ((get "IN_ELIM_THM"):thm)
val it : thm =
|- (!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ x = t)) /\
(!p x. x IN {y | p y} <=> p x) /\
(!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ x = t)) /\
(!p x. {y | p y} x <=> p x) /\
(!p x. x IN (\y. p y) <=> p x)
# ((get "MESON_TAC"):thm list->tactic);;
val it : thm list -> tactic = <fun>
Note that you must explicitly provide the type of the value you want to
retrieve.
It makes use of some quite undocumented features of Ocaml (Obj.magic and
Toploop.getvalue).
Jon uses this somewhere (help.ml if I remember well).
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.
>
This is just a tutorial example on how to build such a mechanism in ocaml,
but not how to access this mechanism for ocaml itself. See below.
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?
It is correct but it does not solve your problem. The variable x belongs to
the language of HOL Light. You have all possible control, through ocaml,
over HOL Light terms, because HOL Light terms are just ocaml values. But
ocaml values are not ocaml values so it does not work in the same way.
That's precisely the difference between the object language (HOL) and the
meta language (ocaml): ocaml is the meta language of HOL Light so you can
control HOL Light through ocaml, but ocaml is not its own meta language
(that's why we have to go through tricky undocumented features to allow
such a behavior).
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
2013/5/4 Bill Richter <rich...@math.northwestern.edu>
> 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
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
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
