[opentheory-users] importer for Isabelle

[Ramana Kumar]

On 2 October 2015 at 13:27, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana and Michael,
>
> Thank you for updating the Isabelle importer and moving it to a new
> home. I'll update the link on the OpenTheory project page
>
> http://www.gilith.com/research/opentheory/
>
> to point to the github repo, and should I also change the maintainer
> to you both?
>

I'm fine with that.


>
> Perhaps one day it will be possible to replace the "R" with an "R/W"
> too, to match the other interfaces :-)
>

That is the hope.


>
> Cheers,
>
> Joe
>
> On Thu, Oct 1, 2015 at 5:25 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Hello,
> >
> > Michael Norrish and I have taken Brian's importer and got it to at least
> > build on Isabelle2015. In the process we also converted to a git
> repository
> > and put it on GitHub. You can find it here:
> >
> > https://github.com/xrchz/isabelle-opentheory
> >
> > We haven't been able to get Brian's demo OpenTheory.thy to work yet, and
> > it's quite possible we made mistakes in updating opentheory.ML. I hope
> > further updates can happen in the above repository, where it's easy for
> me
> > to accept contributions (pull requests), although further coordination on
> > the original repository would also be fine as long as it's being actively
> > maintained.
> >
> > Cheers,
> > Ramana
> >
> > On 31 August 2015 at 15:24, Ramana Kumar <ramana at member.fsf.org> wrote:
> >>
> >> Hi Brian,
> >>
> >> Could I trouble you to look for a copy of your OpenTheory-related code
> for
> >> Isabelle? I'd like to see if I can get it working.
> >>
> >> Oh, actually I just found this link:
> >> http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory
> >>
> >> So, I can get started with that, but if you have any comments or ideas
> >> they could probably still be helpful :)
> >>
> >> Cheers,
> >> Ramana
> >>
> >> On 6 July 2015 at 20:54, Ramana Kumar <ramana at member.fsf.org> wrote:
> >>>
> >>> Yes, if it works (or is close to working) I would like to get it
> >>> incorporated into the Isabelle codebase. I'm not yet sure how to
> contribute
> >>> things to Isabelle, but I imagine I'll find out within the next few
> months.
> >>>
> >>> On 23 May 2015 at 15:52, Brian Huffman <brianh at cs.pdx.edu> wrote:
> >>>>
> >>>> I've hardly looked at it since I wrote it. It was never incorporated
> >>>> into the Isabelle codebase. I suppose it would probably work with the
> >>>> latest Isabelle, because it uses only the low-level proof kernel api,
> >>>> which doesn't change much any more.
> >>>>
> >>>> I'll have to look around to see where I have a copy of the source
> >>>> code; that was a couple of computers ago. Did you want to try to do
> >>>> something with it?
> >>>>
> >>>> - Brian
> >>>>
> >>>>
> >>>> On Sat, May 23, 2015 at 5:13 AM, Ramana Kumar <ramana at member.fsf.org>
> >>>> wrote:
> >>>> > Hi Brian,
> >>>> >
> >>>> > What's the status of your OpenTheory importer? Does it work with the
> >>>> > latest Isabelle? Was it incorporated into the main code base?
> >>>> >
> >>>> > Cheers,
> >>>> > Ramana
> >>>> >
> >>>> > On 15 April 2011 at 17:34, Brian Huffman <brianh at cs.pdx.edu> wrote:
> >>>> >> On Thu, Apr 14, 2011 at 7:03 PM, Joe Hurd <joe at gilith.com> wrote:
> >>>> >>> Hi Brian,
> >>>> >>>
> >>>> >>> That is really great work! Am I right in thinking you can import
> the
> >>>> >>> parser-1.5 article binding all the input symbols and axioms to
> >>>> >>> existing ones in Isabelle? I would have guessed that Isabelle type
> >>>> >>> classes would have managed to get in the way at some point, but
> >>>> >>> perhaps this would only be for converting Isabelle proofs to
> >>>> >>> OpenTheory format?
> >>>> >>
> >>>> >> Yes, each of the input constants of the article is mapped to a
> >>>> >> pre-existing Isabelle constant. Some of these existing Isabelle
> >>>> >> constants happen to be overloaded, but that doesn't cause any
> >>>> >> problems. This mapping of constant names does not even need to be
> >>>> >> one-to-one; for example, I imagine that "Number.Natural.+" and
> >>>> >> "Number.Integer.+" would map to the same overloaded "plus" constant
> >>>> >> in
> >>>> >> Isabelle.
> >>>> >>
> >>>> >> Of course, exporting proofs from Isabelle is a completely different
> >>>> >> story.
> >>>> >>
> >>>> >>> You mentioned that you prove a lot of theorems that the OpenTheory
> >>>> >>> article relies on, but it seems you could reduce this by
> processing
> >>>> >>> a
> >>>> >>> set of OpenTheory packages that don't make any definitions. When I
> >>>> >>> was
> >>>> >>> designing the standard theory library I tried to isolate packages
> >>>> >>> that
> >>>> >>> made definitions and have them export just a minimal theorem
> >>>> >>> interface
> >>>> >>> - most of the theorems are proved in packages that make no
> >>>> >>> definitions
> >>>> >>> and so can be safely run to populate the [opentheory] set of
> >>>> >>> theorems.
> >>>> >>
> >>>> >> Your idea of keeping definitions in separate, minimal modules is a
> >>>> >> good design. I'm sure I could have greatly reduced the number of
> >>>> >> [opentheory] lemmas that I needed by finding the right additional
> >>>> >> article files to import; I was just too lazy to figure out how the
> >>>> >> packages were organized.
> >>>> >>
> >>>> >>>> The importer should also extend these tables whenever it defines
> a
> >>>> >>>> new
> >>>> >>>> constant or type, but I haven't implemented this yet. Another
> nice
> >>>> >>>> feature would be a way for users to influence how the importer
> >>>> >>>> chooses
> >>>> >>>> names for newly-defined constants and types. Right now it takes
> the
> >>>> >>>> names directly from the strings in the article file, which isn't
> so
> >>>> >>>> nice for names like "HOLLight._dest_rec" (Isabelle's parser can't
> >>>> >>>> handle names that start with underscores).
> >>>> >>>
> >>>> >>> You should find that constants and type operators with names like
> >>>> >>> this
> >>>> >>> are never exported from a theory (i.e., never appear in exported
> >>>> >>> theorems), so it's perfectly safe to normalize their names to
> >>>> >>> something more acceptable to Isabelle. They are `local
> definitions'
> >>>> >>> that are used only in proofs.
> >>>> >>
> >>>> >> Actually, it seems like it would be safe to rename *any* constant
> >>>> >> (whether exported or not) to any name that I want in Isabelle, as
> >>>> >> long
> >>>> >> as the importer keeps track of the name mapping so that later
> imports
> >>>> >> can use the same names.
> >>>> >>
> >>>> >> I suppose I should write an "import_name" function that converts
> from
> >>>> >> OpenTheory names to Isabelle-friendly ones. It would be nice to
> >>>> >> parameterize this by a list of user-specified exceptions to the
> >>>> >> mapping, so you could say something like, "import this article, but
> >>>> >> when you define constant 'foo', call it 'bar' instead."
> >>>> >>
> >>>> >>>> Once I clean up the code, I'm not sure what I should do with
> it...
> >>>> >>>> I
> >>>> >>>> suppose I could add it to the Isabelle repo, but I'm not sure if
> I
> >>>> >>>> want to advertise to Munich crowd that I've been doing all this
> >>>> >>>> work
> >>>> >>>> that is unrelated to finishing my thesis :)
> >>>> >>>
> >>>> >>> I would very much like to see it live on in some fashion - my hope
> >>>> >>> is
> >>>> >>> that more and more theories will be converted to OpenTheory
> >>>> >>> packages,
> >>>> >>> and your code could be used to import them into Isabelle in a
> >>>> >>> principled way.
> >>>> >>
> >>>> >> I suppose I'll add it to the Isabelle distribution at some point,
> >>>> >> maybe after I finish writing my thesis. In the meantime, I guess I
> >>>> >> can
> >>>> >> post the code to the list, so it will be archived and people can
> try
> >>>> >> it out.
> >>>> >>
> >>>> >> - Brian
> >>>> >>
> >>>> >> _______________________________________________
> >>>> >> opentheory-users mailing list
> >>>> >> opentheory-users at gilith.com
> >>>> >> http://www.gilith.com/opentheory/mailing-list
> >>>
> >>>
> >>
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> 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/20151004/70073a4f/attachment-0001.html>