Re: [isabelle] Formalizations of Free Groups and Matrix Groups?

On Fri, May 7, 2010 at 2:27 PM, Joachim Breitner
<mail at joachim-breitner.de> wrote:
> I’m quite new to Isabelle and trying to get an overview of the
> mathematics already formalized. I found some basic group theory in the
> HOL/Algebra directory, but it seems to be relatively basic. It contains
> abstract definitions, but I’m missing some more concrete groups,
> especially the Free Group over a finite set of generators, matrix groups
> such as GL_r(ℤ) and permutation groups.
>
> Am I not looking in the right places? And if such theories really do not
> exist, is there some principal problem in implementing them, or is it
> something that just has not been done yet, but should not be
> particularly hard?

Hi Joachim,

Indeed, the Isabelle libraries contain a lot of more concrete
mathematical constructions, but they are spread over several different
places, and generally nobody has connected them up with HOL/Algebra to
show that they are instances of the more abstract notions.

Often these kind of constructions are formalized as type constructors.
For example, HOL/Matrix defines a type "'a matrix" of matrices with
elements of type 'a (it includes matrices of any finite size). You
could define GL_r(Z) as a subset of this type like this:

definition GL :: "nat => int matrix set"
where "GL n = {A::int matrix. nrows A = n & ncols A = n & (EX B.
inverse_matrix A B)}"

Then it would be straightforward to show that this set, together with
"op *" on type "int matrix", forms a group according to the
definitions defined in HOL/Algebra.

Some other constructions implemented as type constructors:
Library/Polynomial.thy defines the ring of univariate polynomials with
coefficients from type 'a as the type "'a poly". On the AFP
(afp.sourceforge.net) you will find a formalization of the Free
Boolean Algebra with generators from type 'a as the type "'a formula".
There is also a function "formulas :: 'a set => 'a formula set" which
can be used to reason about sub-algebras.

Also, the Isabelle library contains a very nice formalization of the
Free Monoid with generators from type 'a -- it can be found in
List.thy :) It also contains a function "lists :: 'a set => 'a list
set" that gives the lists generated by some subset of generators.
Similarly, a construction of the Free Commutative Monoid can be found
in Library/Multiset.thy, as type "'a multiset".

As far as I know, nobody has formalized Free Groups. I wouldn't expect
it to be difficult, but probably nobody has really needed them for
anything yet. You could define a type constructor for the free group
with generators over type 'a as a subset of type "(bool * 'a) list",
where you would have a function "normalize :: (bool * 'a) list =>
(bool * 'a) list" that removes adjacent copies of the same element
with opposite signs.

typedef 'a free_group = "{x :: (bool * 'a) list. normalize x = x}"

Then you could define a function analogous to "lists" with type "'a
set => 'a free_group set" that would pick out the values generated by
some smaller set. This would probably make a nice AFP entry, if you
wanted to formalize it.

As for permutations: There is a library Permutations.thy that
formalizes the set of permutations over a given set. (Currently it is
located in HOL/Multivariate_Analysis, since it is used by other
theories there; but in the next release of Isabelle it will be located
in HOL/Library.)

There are probably other examples that I can't think of right now.
Have fun exploring the Isabelle libraries!

- Brian

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