[isabelle-dev] class recpower and other classes...

[Amine Chaieb]

The class recpower is very unfortunate. I suggest to remove it and 
replace it by definitions inside the locale/class (The axioms *are* a 
recursive function definition).

The problem with the actual structure of classes is that many classes 
have been separated (which is nice for separation of concepts) but now 
we need to merge almost any two interesting classes into one in order to 
prove theorems in the locale and not on the axclass level, since it is 
not possible to do the following:

lemma (in ring + recpower) ...

as soon as you want a theorem about power in rings, where power is 
something very natural in terms of multiplication...

any suggestions, thoughts?

I also suggest the introduction of several "join" classes such as
(semi)ring/field + division_by_zero
ring + characteristic_zero
and many other useful classes, we use "almost daily". Is it thinkable to 
have such things in HOL or should I just rebuild the Ring_and_Field 
theory as I need it?

Amine.