Re: [isabelle] instance declaration problem with axiomatic classes



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.





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