[isabelle-dev] class recpower and other classes...
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?
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev