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/HOL-Algebra as a starting
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
| > and at the same time prove that these rings are categorically equivalent to
| > rings founded in Zermelo-Fraenkel 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 paper-proof 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 Zermelo-Fraenkel
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
Does this make my goal clearer? I have seen some information about both HOLZF
and HOL-ST, but it is unclear whether they would serve my purpose.
Thanks for your thoughts,