[opentheory-users] importer for Isabelle

[Brian Huffman]

Hello,

I now have a working OpenTheory importer for Isabelle (tested with
Isabelle2011). The code is still kind of a mess, with a bunch of extra
debugging code sitting around, so I'll wait until I've cleaned it up a
bit before I share it. There are still a few improvements that need to
be made, but I think I have all the major bugs fixed now: It can
successfully import the parser-1.5 library (reading the article file
generated by "opentheory info --article parser-1.5").

The implementation adds three new tables to Isabelle's Theory_Data:
1) A set of theorems; there must be an entry here that matches each
"axiom" command.
2) A mapping of type names; there must be a matching entry for each
"typeOp" command.
3) A mapping of constant names; there must be a matching entry for
each "const" command.

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 other tables are extended using "setup" commands with "add_tyop"
and "add_const" ML functions, like this:

setup {*
  fold OpenTheory.add_tyop
  [("->", @{type_name "fun"}),
   ("bool", @{type_name "bool"}),
   ("Number.Natural.natural", @{type_name "nat"}),
   ("Data.Pair.*", @{type_name "prod"})]
*}

setup {*
  fold OpenTheory.add_const
  [("=", @{const_name "HOL.eq"}),
   ("Data.Bool.!", @{const_name "All"}),
   ("Data.Bool.==>", @{const_name "HOL.implies"}),
   ("Data.Bool.\\\\/", @{const_name "HOL.disj"}),
   ("Data.Bool./\\\\", @{const_name "HOL.conj"}),
   ("Data.Bool.cond", @{const_name "If"}),
   ("Data.Bool.select", @{const_name "Eps"})]
*}

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

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

- Brian