[isabelle] instance declaration problem with axiomatic classes



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.