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

[Tobias Nipkow]

I suggest that those of us in M do not start an email discussion but 
meet in person to discuss this.

Tobias

Amine Chaieb schrieb:
> 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.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev