Florian Haftmann wrote: > A) Archaic, hardly readable and fragile proof techniques: > * unfolding definitions of predicates over logical formulae instead of > proper intro/elim-rules
There was some discussion on this already, and I'd agree with Tobias and Amine that it's just a matter of taste. Having intro/elim rules can be more brittle than unfolding. > * long apply-Scripts with sometimes obscure tacticss Indeed, I don't like these either. Some of them go back to the time of ML scripts. I don't see the value in investing a lot of time into making them beautiful, though. No-one wants to read them. The only reason would be to make maintenance easier, but it didn't seem to be a problem so far. > B) Naive use of locales (instead of proper interpretation): > * somehow arbitrary mixed explicit locales and simple predicates > * free-floating use of uninterpreted global rules from locales > * use of "defines", where definition etc. would be appropriate Dude ;-) These things were written when locales didn't even fully exist yet. It is the first substantial use of the idea (hence the use of "open", which was the only kind of locale that existed at the time). Of course they're not using interpretations, we hadn't even thought of the concept yet (in fact, I believe that we started discussing them because of this application), and definition was something I'd very much have liked to have (and also suggested at the time) but it was still many years too early. In short: you're perfectly right, with modern locales this could be written a lot nicer. At the time it was as good as it got, though. I'm perfectly fine with someone going over these and making them into proper locales. I'm not volunteering, though ;-) > C) A lot of forked (but not shared) theories in MicroJava, Jinja, > JinjaThreads. > > Of course, all these are due to historic reasons, layers of increasing > state of the art built on top of each other. Anyway, concerning C), > IMHO in the future we should try harder to avoid such duplication by > distilling reasonable libraries out of large-sized projects. E.g. these > projects contain independent developments of semilattices, work which > would fit more appropriately in HOL-Algebra and then could simply be > re-used. Such shared libraries would greatly increase the motivation > and benefit for keeping them technically at the height of the day than > such (superficially) "specialized" and "adapted" theories scattered over > different projects. Quite right. The problem with that is that it costs considerable time and when your focus is the large project and not the distribution, you will just not care enough to do it. We should get into the habit of explicitly allocating time for activities like that. Cheers, Gerwin
