*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] instance theorems*From*: Sean McLaughlin <seanmcl at cmu.edu>*Date*: Tue, 7 Mar 2006 08:58:34 -0500*In-reply-to*: <440D7CA0.9040400@informatik.tu-muenchen.de>*References*: <678ABD6F-FDBF-46DF-B357-59182A14D28D@cmu.edu> <440D7CA0.9040400@informatik.tu-muenchen.de>

Hello,

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

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

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.

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 relationsbetween 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 appropriatemanner, but in order to understand your issue exactly, we wouldneed more context - can you send a description what you want to doexactly 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>

**References**:**[isabelle] instance theorems***From:*Sean McLaughlin

**Re: [isabelle] instance theorems***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] instance theorems
- Next by Date: Re: [isabelle] some ESSLLI mailing list?
- Previous by Thread: Re: [isabelle] instance theorems
- Next by Thread: Re: [isabelle] instance theorems
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list