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

[Tobias Nipkow]

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

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