[opentheory-users] importer for Isabelle

[Ramana Kumar]

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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150831/6bb808f8/attachment.html>