Re: [isabelle] instance declaration problem with axiomatic classes
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and