*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 8 May 2010 09:40:41 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1273267675.11358.4.camel@kirk>*References*: <1273267675.11358.4.camel@kirk>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Joachim Breitner

**Re: [isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Timothy McKenzie

**References**:**[isabelle] Formalizations of Free Groups and Matrix Groups?***From:*Joachim Breitner

- Previous by Date: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Next by Date: Re: [isabelle] How to speed up locales
- Previous by Thread: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Next by Thread: Re: [isabelle] Formalizations of Free Groups and Matrix Groups?
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list