# Re: [isabelle] matrix constructions

Take a look at src/HOL/Matrix/Matrix.thy in the Isabelle repository.
It defines the type matrix based on "nat => nat => 'a" which are only
non-zero on finitely many positions. It forms a semiring, ring,
ordered_ring when 'a is respectively a semiring, ring, ordered_ring.
There are alternatives like using a type to encode the dimensionality
like the finite cartesian products in Multivariate_Analysis.
- Johannes
Am Donnerstag, den 31.03.2011, 17:56 +0300 schrieb Viorel Preoteasa:
> Hello,
>
> I have a class that has the binary operations * and +, and I would like
> to define
> an instantiation of this class for matrices with the usual operations
> for matrices.
>
> (A * B) i j = Sum_k (A i k) * (B k j).
>
> The dimension of the matrices must be finite because the plus operation
> is binary.
>
> Is there a way of defining this structure with the instantiation
> mechanism of Isabelle?
>
> Best regards,
>
> Viorel
>

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