[Hol-info] Learning HOL: Commutative rings

[Robert M. S. <so...@Ma...>]

I'm trying to learn how to formalize mathematics in HOL. So far, I've
worked through Chapter 7 in the tutorial.

For the next warmup project, I'd like to port the proof of the binomial
theorem in the HOL book from HOL 88 to HOL 4. As a warm up, I'd like to
prove the [trivial special case] of (a + b) * (a + b) = ...

But I don't even know how to state it. What I want to formalize is:

If R is a commutative ring and a, b are elments of R then ...

Clearly the files in HOL4/src/ring/src are relevant but I'm not sure in
what order to tackle them.

I'm not yet asking how HOL4 represents specific rings. I just want to know
how to formulate general statements about commutative rings. {Of course, I
could "reinvent the wheel" and define rings on my own. But I want to know
how it's done in the libraries.}

	Many thanks for any assistance.

	--Bob Solovay