Re: [isabelle] instance theorems
In order to translate Isabelle/HOL to HOL Light, I create functors
out of the types, constants, axioms and theorems, and signatures out
of the classes.
An instance theorem corresponds to an extension of a type module with
For instance, say the real numbers are translated as, in SML syntax
(as I'm not
sure if Isabelle hackers are familiar with O'Caml)
signature TYPE =
val typ : hol_type
structure Real : TYPE =
val typ = `:real`
Where `:real` is the HOL Light real type.
An instance theorem, say, adds extra fields to this module
eg, if the constants were declared explicitly,
axclass ord < type [<= : 'a -> 'a -> bool]
instance Real ord [<=: real -> real -> bool]
would generate the following new modules
signature ORD =
val <= : hol_term
structure Real : ORD =
include Real (you can do this in O'Caml)
val <= = `real_le`
where the translator figures out that `real_le` is the HOL module
to <= on the Isabelle reals.
axclass order < ord =
refl : ...
trans : ...
signature ORDER =
val refl : hol_thm
instance real ord = *proof of (x:real) <= x /\ ...*
structure Real : ORDER =
val prethm = (translate the ideally supplied proof)
val refl = 1st conjuct prethm
val trans = 2nd conjunct prethm
So you can see, having the proof term is essential to my plan.
I've been surviving thus far by just throwing a bunch of stuff
into MESON_TAC, but this is starting to fail, especially on
nontrivial instances, eg
instance "*"(ord,ord) ord
instance "*"(order,order) order
(I realize that my method shown in the example wouldn't handle this
but I felt explaining the full rules would be needlessly complicated)
I hope this is sufficiently clear.
In my dreams, I would have the evidence for an instance declaration
be a list of constant maps and a list of separate theorems proving
each class proof obligation individually in a map from names
to the theorems, but I realize this is rather elaborate evidence.
I will be delighted if there is simply a straightforward algorithm to
the information I need from the proof term. For instance, if
you store the class axiom proofs as a big conjunction, a well defined
plan for the order of the conjuncts wrt the names of the axioms would
be nice, eg. alphabetical order.
I just sent a paper to IJCAR
with a precise description of the elaboration. I will post
it on my webpage by this evening.
On Mar 7, 2006, at 7:29 AM, Florian Haftmann wrote:
My guess is that they're in the system
somewhere, as they need the same kind of theorem proving as
an ordinary lemma.
Currently, they are not stored. Moreover, some instance relations
between type constructors and sorts are not proven but inferred,
proofs would have to be constructed manually.
It is not out of scope to enrich axclass.ML in an appropriate
manner, but in order to understand your issue exactly, we would
need more context - can you send a description what you want to do
exactly with classes or a piece of code?
This archive was generated by a fusion of
Pipermail (Mailman edition) and