[opentheory-users] importer for Isabelle

[Joe Hurd]

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?

> The set of theorems is extended using the [opentheory] attribute, like this:
>
> lemma [opentheory]: "ALL m::nat. m + 0 = m"
> by simp
>
> (I have lots of these kinds of proofs for natural numbers and booleans.)
>
> The importer also adds new theorems to the set whenever it processes a
> "thm" command. The complete list of theorems can be accessed using the
> name "opentheory", which is one of those new dynamic theorem
> references in Isabelle; it can be used in proof scripts or anywhere
> just like any other theorem name.

The [opentheory] attribute looks like a great scheme that could
perhaps be used in the HOL family of theorem provers to import
OpenTheory proofs.

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.

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

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

Thanks for having a go at this - I never thought you'd crank it out so quickly.

Cheers,

Joe