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.
> 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.
(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
