Am 2013-05-05 um 03:31 schrieb Ramana Kumar <ramana.ku...@cl.cam.ac.uk>:
> On Sun, May 5, 2013 at 5:45 AM, Vincent Aravantinos
> <vincent.aravanti...@gmail.com> wrote:
>> 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).
>
> In HOL4 you can get a named theorem with DB.fetch, which has type string ->
> string -> thm. (The first string is the name of the theory, the second is the
> name of the theorem.)
>
> In HOL Light I guess there's no database of theorems indexed by names? That
> would be one way to avoid having to use Obj.magic.
Indeed.
>> 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).
>
> I presume you mean "But OCaml terms are not OCaml values" there.
> Otherwise I'm confused by what you're saying.
Ha, yes, of course!
> (Side note: some languages are their own meta-languages, like Scheme, where a
> quoted expression is a value. Also there is a language like that for theorem
> proving called reFLect.)
>
>>
>>
>>
>> --
>> 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
>
------------------------------------------------------------------------------
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
