Re: [isabelle] reasoning about classes of many-sorted structures
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.
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and