[isabelle-dev] class recpower and other classes...
nipkow at in.tum.de
Tue Nov 6 15:37:56 CET 2007
Lest my meaning be lost or misconstrued: "in M" meant that if you are
not at TUM, please use email, but if you are, it is better to discuss
this complex topic in person.
Tobias Nipkow schrieb:
> 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
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev