Email Gateway (Aug 18 2022 at 15:48): Email Gateway (Aug 18 2022 at 15:48):From: sudbrock@cs.tu-darmstadt.de
Hi all,
I am looking for a way to define algebraic structures
like, for instance, modules over rings or vector spaces
over fields in Isabelle/HOL. In particular, I want to
formulate statements like the following: "The product of
two vector spaces over a field K is a vector space over
the field K."
As far as I see, this is possible using 'typedef' to
define a type as follows (for vector spaces):
typedef ('K, 'V) vectorspace = "{
(zero :: 'V,
add :: 'V => 'V => 'V,
inverse :: 'V => 'V,
scalarmult :: 'K => 'V => 'V
(* ... *)
(ALL v. (add v zero) = v)
& (ALL v v'. (add v v') = (add v' v))
(* ... *)
}"
As working with typedef-ed types seems somewhat
cumbersome, and concepts like Haskell-style type classes
or locales seem to be useful for algebraic structures (as
algebraic structures are used in the running examples in
the documentation), I am wondering if I should rather use
one of those two concepts.
However, as far as I found out, type classes support only
one type parameter (while I need two, one for the
underlying ring/field, and one for the abelian group of
the module/vector space). Is there a reason for this
restriction of type classes?
Concerning locales, I found the vectorspace-locale of the
HahnBanach-theory within the Isabelle library. However, I
do not see how to define functions like "the product of
two vector spaces" (which would map two instantiations of
the locale to a third instantiation of the locale) for
such a locale. Is there any way to define such functions?
Or is there perhaps another "standard" or "recommended"
way to define such structures in Isabelle/HOL?
Best regards,
Henning
Email Gateway (Aug 18 2022 at 15:50):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Donnerstag, den 12.08.2010, 17:20 +0200 schrieb
sudbrock@cs.tu-darmstadt.de:
Hi all,
I am looking for a way to define algebraic structures
like, for instance, modules over rings or vector spaces
over fields in Isabelle/HOL. In particular, I want to
formulate statements like the following: "The product of
two vector spaces over a field K is a vector space over
the field K."
[..]
Concerning locales, I found the vectorspace-locale of the
HahnBanach-theory within the Isabelle library. However, I
do not see how to define functions like "the product of
two vector spaces" (which would map two instantiations of
the locale to a third instantiation of the locale) for
such a locale. Is there any way to define such functions?
When you use locales you get a predicate which describes your locale.
locale vector_space =
fixes zero, add, ...
assumes "..."
To prove that a product of two vector spaces is again a vector space,
you can use the predicates:
lemma vector_space_product:
assumes "vector_space z1 add1 ..."
assumes "vector_space z2 add2 ..."
shows "vector_space (z1, z2) ..."
proof -
(* Use interpret to get all you locale lemmas and definitions *)
interpret vs1: vector_space z1 add1 ... by fact
interpret vs2: vector_space z2 add2 ... by fact
...
show ?thesis ...
qed
Or is there perhaps another "standard" or "recommended"
way to define such structures in Isabelle/HOL?
The recommended way is to use locales. Even type classes are based on
locales.
Often the locale parameters for algebraic structures are packaged into a
record:
record 'v 'k vector_space = 'v monoid +
scalar :: "'k => 'v => 'v"
See also src/HOL/Algebra for application of locales to algebraic
structures.
Greetings,
Johannes
Best regards,
Henning
Last updated: Apr 18 2024 at 04:17 UTC