Tjark,
On Sat 4/22/2006 5:37 PM, Tjark Weber wrote:
 On Saturday 22 April 2006 04:07, Robert Lamar wrote:
 > I am attempting to develop ring theory in HOL,

 I would suggest to take one of the existing formalizations of ring theory that
 can be found in HOL/Ring_and_Field.thy or in HOL/HOLAlgebra as a starting
 point.

I have actually been working on this a while, and that didn't occur to me when
I started. I am considering porting my work to be based on one of these while
deleting repetitive results. But that is a decision that I am not going to make
right now. At the moment I am more focused on the equivalence question, which
is below.
 > and at the same time prove that these rings are categorically equivalent to
 > rings founded in ZermeloFraenkel set theory.

 Do you want to prove this on paper, or in Isabelle? In any case, what would
 be your theory for this proof?

My goal is a mathematical paperproof that shows that the ring theory in
Isabelle is equivalent to what has been developed in Abstract Algebra. I should
probably mention that I am an undergraduate: this is a project for my
bachelor's degree, and while I have learned much about rigorous ZermeloFraenkel
set theory and category theory, I am still not very confident.
The proof that I seek, upto my understanding of the discipline, is to declare
the category of rings based on ZF sets and the category of rings based on Isabelle
sets, and then to find a functor from one to the other which satisfies certain
requirements.
Does this make my goal clearer? I have seen some information about both HOLZF
and HOLST, but it is unclear whether they would serve my purpose.
Thanks for your thoughts,
Robert Lamar