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.