[ProofPower] Equivalence Relations and Group Theory [Apologies to HOL-info readers who will see this twice.]

[Rob Arthan]

Dear All,

Inspired by Larry Paulson's recent discussion on the HOL-info on equivalence 
relations, I have done some work on the basics of group theory in 
ProofPower-HOL. The initial results are in the paper wrk068.pdf at:

	http://www.lemma-one.com/ProofPower/examples/examples.html

This includes my take on Larry's lemma-library approach to equivalence 
relations. It then gives my take on traditional abstract group theory as far 
as the construction of quotient groups and the proof of their characterising 
properties (i.e., not very far at all, but I've only been at it for a few 
days).

There are some quite interesting questions about how to formalise this 
material. There are some points at which you get into deep trouble formally 
if you mindlessly follow the traditional explications of pure mathematics in 
set theory. I've discussed this in the paper. I would welcome any comments on 
this. I'd also be very interested in pointers to similar work with other 
systems.

Regards,

Rob.