Re: [isabelle] instance theorems



Hello,

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 new fields. 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 =
sig
  val typ : hol_type
end

structure Real : TYPE =
struct
  val typ = `:real`
end

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  =
sig
  include TYPE
  val <= : hol_term
end

structure Real : ORD =
struct
   include Real (you can do this in O'Caml)
   val <= = `real_le`
end

where the translator figures out that `real_le` is the HOL module corresponding
to <= on the Isabelle reals.

now,

axclass order < ord =
  refl : ...
  trans : ...
  etc...

becomes

signature ORDER =
sig
  include TYPE
  include ORDER
  val refl : hol_thm
  ...
end

and the

instance real ord = *proof of (x:real) <=  x /\ ...*
becomes

structure Real : ORDER =
struct
  include Real
  val prethm = (translate the ideally supplied proof)
  val refl = 1st conjuct prethm
  val trans = 2nd conjunct prethm
 ...
end

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
and worse
instance "*"(order,order) order

(I realize that my method shown in the example wouldn't handle this case,
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 extract
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.

Thanks,

Sean



On Mar 7, 2006, at 7:29 AM, Florian Haftmann wrote:

Dear Sean,

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?

Rgds.
Florian

--

PGP available:
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/ florian_haftmann_at_informatik_tu_muenchen_de.pgp
<florian.haftmann.vcf>






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.