Email Gateway (Aug 18 2022 at 17:18): Email Gateway (Aug 18 2022 at 17:18):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 17:19):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Last updated: Apr 19 2024 at 20:15 UTC