[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

(Just replying to the bits of Joe's message that I can.)

On Fri, Aug 2, 2013 at 12:18 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Incidentally, how does your format encode lists (substituions or the
> list of types that are an argument to type operators)?
>

Their Subst and Inst commands take a variable-length list of arguments
(refs to terms or types).
So the substitution is given as part of the command itself, using a
"meta-level" list.


> > How does the HOL Light
> > exporter deal with sharing (between terms)?
>
> It adds every type, term and theorem to a dictionary, so each is only
> exported once (per theory, when the dictionaries are reset).
>
> > I assume for the HOL4 exporter
> > this is not an issue, since sharing can be observed directly. Is this
> > correct?
>
> That's a question for Ramana, who's the maintainer of the HOL4
> import/export infrastructure.
>

The HOL4 exporter doesn't do anything more sophisticated than what the HOL
Light exporter does, as far as sharing is concerned.
In particular, I do not make use of pointer equality directly.
I use HOL4's native Term.compare etc. functions, though, which may use
pointer equality internally.
I use a dictionary to save OpenTheory objects that I've already logged, and
reuse them (with the ref command) when possible.


>  > - If I want to play with the tools, i.e., export some small theorem
> from HOL
> > Light, apply some mapping (aka theory interpretation) and re-import into
> > HOL4... Are there any step by step instructions that I can follow?
>
> This FAQ describes the steps for exporting from HOL Light:
>
> http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light
>
> Ramana: I know I just asked you in another thread for some notes on
> exporting from HOL4, but if you also made notes for importing I'd
> create two new FAQs to put them in!
>

The importer is documented in the HOL4 sources, namely in this file:

  src/opentheory/Opentheory.sig

The main entry-point is Opentheory.read_article : string -> reader -> thm
net, which takes the path of an article file and a reader record (with
information about where to find constants and axioms the article might
need, and how to handle things the article might define, all documented in
the file above) and returns a net of theorems. (A "net" makes for efficient
lookup of theorems based on their conclusion; you can easily just extract a
list of the theorems if desired.)

Let me know if the documentation doesn't make sense, or if you want more
information for the FAQ. (I'll reply about the exporter in the other
thread, perhaps a bit later - it may be more complicated.)


>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130802/a5441a01/attachment.html>