Re: [isabelle] reasoning about classes of many-sorted structures

Dear Andrei,

It might not be the most elegant way. In the recent snapshot development there is theory in HOL/Library/Finite_Cartesian_Product.thy which introduces a new type constructor "'a ^ 'n" which represents 'a * ... 'a and this as many times as 'n has inhabitants. This is true only if 'n has finitely many inhabitants.

Of course this is more restrictive that an abstract view, but better than nothing. You can also look at an other new theory in HOL/Library/Euclidean_Space.thy, where it is shown that e.g is 'a is a group, then so is 'a^'n etc. for several interesting algebraic classes. So you get implicitly that it is a vector space (there is scalar multiplication) but this is not a class.

On the other hand, if you want to have thing really general and nice, you could use locales.

Best wishes,

Andrei Popescu wrote:
As far as I see, type classes do not allow multiple type
variables.  Concretely, say I
want to reason about vector spaces (K,V,+,*,...) without having either of K and V fixed. Is there any elegant way around this? Thank you in advance for any hint, Andrei Popescu

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