*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] instance declaration problem with axiomatic classes*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 22 Aug 2007 08:31:09 -0700*In-reply-to*: <46CBDBFC.7030507@nicta.com.au>*References*: <46CBDBFC.7030507@nicta.com.au>*User-agent*: KMail/1.9.6

Hi Michael, Instead of using the type class mechanism here, you could accomplish what you want using predicates on types. I'll explain what I mean by this using an example: definition sizelimit :: "nat => 'a itself => bool" where "sizelimit n (t::'a itself) == ALL x::'a. size x <= n" Now you can use this predicate to represent sort constraints. For example, instead of proving "instance word32 :: sz4" you would prove a theorem that says "sizelimit 4 TYPE(word32)". This is basically what Isabelle's axclass system does internally (except that it doesn't allow you to parametrize a class by a natural number, of course). You could also prove an inference rule like this for tyop: [| sizelimit m TYPE('a); sizelimit n TYPE('b); m * n <= k|] ==> sizelimit k TYPE(('a,'b)tyop) This is much more flexible than any instance declaration in Isabelle could be. But the drawback is that you lose automation: Instead of sort annotations you will need to add explicit sizelimit assumptions to your theorems, which you will then have to discharge manually using inference rules like the one above. - Brian On Tuesday 21 August 2007, Michael Norrish wrote: > It seems that I cannot do the following > > instance tyop :: (class1, class2) myclass > <some proof> > > instance tyop :: (class3, class4) myclass > <some other proof> > > where there is no connection between the various class<n>. This is > despite the fact that the proofs themselves do work. > > My reading of the "Order-Sorted Unification" paper suggests to me that > I'm bumping my head against the "unnecessarily strong" co-regularity > condition. Is there any prospect of this being weakened? > > Failing that, how might I achieve the desired effect? The myclass > axclass has as one of its axioms that the "size" of its types not be > greater than a particular limit. In the binary type operator (array), > the "size" of the type is the product of the "size" of the first > argument to array, and the "number" of the second. > > At the moment, in order to get something like > > (word32, "10") array > > accepted as an instance of myclass, I first have to invent a class > into which I can put word32 (I call it sz4), and then a class for the > type "10", which I call count10. I can then use the definition of the > "size" calculation and the axioms for sz4 and count10 to prove that > the "size" of > > ('a::sz4, 'b::count10) array > > is 40, which is less than the limit in myclass. > > But if I'm interested in also showing > > (some_user_type, "13") array > > is in myclass, I'm now stuck. > > Thanks, > Michael.

**Follow-Ups**:**Re: [isabelle] instance declaration problem with axiomatic classes***From:*Michael Norrish

**References**:**[isabelle] instance declaration problem with axiomatic classes***From:*Michael Norrish

- Previous by Date: [isabelle] Research position in the area of types and verification at LMU Munich
- Next by Date: [isabelle] settings to start emacs?
- Previous by Thread: Re: [isabelle] instance declaration problem with axiomatic classes
- Next by Thread: Re: [isabelle] instance declaration problem with axiomatic classes
- Cl-isabelle-users August 2007 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