Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-05 16:01:58 -0800 (Wed, 05 Nov 2003)
Revision: 5074
Log message:
Finlay I added support for the record renaming.
I defined rename[a:t;b:t]{'r} operator.
I also defined as_additive{'r} operator that
renames "+"-> "*", "0"-> "1", "neg"->"inv"
One can prove that if 'r is a ring then as_additive{'r} in a group.
(This should be added to the typeinf resource).
I have also a bunch of tactics for renaming.
The main tactic is foldAdditiveT that replaces for example 'r^+ by as_additive{'r}^*, and so on.
There is also unfoldAdditiveT that opposite to foldAdditiveT.
These two tactics should be enough to apply group theorems to rings.
The tactic useAdditiveWithAutoT = foldAdditiveT thenT autoT thenT unfoldAdditiveT thenT autoT
should work in all simple cases.
I'm not sure if I pick up the right names for the tactics and the operations. Let me know what you think.
Now rings could be defined for example as
RingSig={car:univ; *: car->car; + : car -> car; 1: car; 0:car; inv: car -> car }
Ring={R:RingSig | isGroup{as_additive{'R}} and .... }
You can also define
isAdditiveGroup{'G} = isGroup{as_additive{'G}}
but then you need to add to the reduce resource two reductions:
isAdditiveGroup{rename_mul_add{'G}} <--> isGroup{'G}
isGroup{rename_add_mul{'G}} <--> isAdditiveGroup{'G}
Then foldAdditiveT will replace isAdditiveGroup{'R} by isGroup{as_additive{'R}}
See more details in Itt_record_renaming and itt_quickref.txt.
The documentation is not very good right now, let me know if you have any questions.
I will commit the proofs soon.