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

Tobias Nipkow nipkow at in.tum.de
Tue Nov 6 15:14:10 CET 2007

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


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

More information about the isabelle-dev mailing list