[opentheory-users] importer for Isabelle

[Brian Huffman]

Hi Ramana,

I think it's great that you've revived my old opentheory importer; I
haven't worked on it for years and don't remember many details about
how it works. I don't plan on doing any more maintenance on my old
repo, so I'm happy to have all future development move to github.

If you are having problems with OpenTheory.thy, I can think of one
possible reason: Sometime around 2010-2012, Isabelle changed type 'a
set into an abbreviation for 'a => bool, and then later changed it
back into a separate type again. I'm not 100% sure, but I think the
importer was written during the 'a => bool time period. If opentheory
uses 'a => bool as its set type, you might need to map opentheory set
operations onto the corresponding Isabelle predicate operators
instead.

Another thing you might look into: Around 2012 Cezary Kaliszyk
implemented an Isabelle importer for HOL Light proofs; at the time I
remember looking at the code and noting that it was quite similar to
my OpenTheory importer. Browsing through his publication list, I just
found a paper about it:

http://cl-informatik.uibk.ac.at/users/cek/docs/13/ckak-itp13.pdf

If his importer has been maintained since then, it might be worth looking at.

- Brian


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