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
