[opentheory-users] importer for Isabelle

[Ramana Kumar]

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