[Hol-info] Learning HOL: Commutative rings

[Michael N. <Mic...@cs...>]

Robert M. Solovay writes:
 
> 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.

The ring theory is set up so that there are functions

  RN, RM, RP, R0, and R1

from values of type ring to the various constituents of rings.  RM
returns the multiplicative operation, RP returns the additive one.
Your base equation would be 

  RM r (RP r a b) (RP r a b) = ...

because an expression 

  RM r

returns the multiplicative operation for ring r.  This does not look
particularly pretty, and there are probably better ways of setting
things up with the parsing and printing tools.  You could also write

  r.RM (r.RP a b) (r.RP a b)

if you prefer the dot notation for fields.  
 
You'll need to use is_ring to express the condition that the record
value is actually a ring, and then add more conditions to express that
it is a commutative ring. 

Michael.