Email Gateway (Aug 19 2022 at 12:01): Email Gateway (Aug 19 2022 at 12:01):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Tobias,
2013-09-15 20:52 Tobias Nipkow:
Thanks, I'll import it into List as merge_eq.
let me use this occasion to ask what the general procedure is for
contributing functionality to the library. I said earlier that I have
some material ready for submitting to the AFP, and I will do so within
the next few weeks as soon as I find time.
However, some of my code is not "specialist" functionality, but
functionality I would actually have expected to find in the standard
library. Please see, at
https://github.com/formare/auctions/tree/master/isabelle/Auction, the
files *Utils.thy, which are named after their library counterparts.
None of them introduce new concepts (except for the notion of a
"trivial" set in SetUtils), but they merely add lemmas, which I found
useful in my work, to existing library concepts. Some of them may be
suitable as simp rules, but so far I have not yet gained sufficient
experience as to what lemmas I should reasonably make simp rules.
I had so far been thinking of submitting these *Utils.thy theories as a
separate AFP submission, on which my other, actual AFP submissions would
depend, and then suggesting that some of it may be merged into the
library. Our license is compatible anyway.
But now, if there is a faster track to the library, I'll be happy to
take it.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:02):From: Tobias Nipkow <nipkow@in.tum.de>
If you have a small theory of some types and/or functions, the AFP is the right
place. Such theories can be small to be reusable. Only in exceptional cases
should they go into Main. Manuel's function is borderline: the theory is tiny
and the functions is generic enough that I felt I would want it in List itself.
Theories that are merely collections of lemmas are not suitable as separate AFP
entries. If one of the lemmas is non-trivial, it could go into Main. Your Utils
theories however seem to consist mostly of variations and combinations of
existing lemmas, which may well be useful in certain situations but are not
clearly "needed" - a library can also become difficult to use if there is too
much in it. However, some of your lemmas should clearly go in Main, eg
"{}\<inverse> = {}"
I will look through your Utils for more such nuggets.
The question of when something should become a simp lemma is delicate unless it
is so obvious as in the above example. Usually there is no way around trying it
out and seeing if many proofs break.
Tobias
Last updated: Apr 26 2024 at 04:17 UTC