Email Gateway (Jan 10 2024 at 09:36): Email Gateway (Jan 10 2024 at 09:36):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Hi List,
I was about to prove the following lemma:
lemma finite_distinct: "finite s ⟹ finite {xs . set xs ⊆ s ∧ distinct
xs}"
when I realized that it occurs, multiple times in slightly different
variations, in the AFP (see below).
What's the process to get such lemmas into List.thy?
Email Gateway (Jan 10 2024 at 09:39):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks Peter, I'll deal with it.
Tobias
Email Gateway (Jan 10 2024 at 11:17):From: Lawrence Paulson <lp15@cam.ac.uk>
This sort of thing happens all the time. Many AFP entries are full of obviously useful results. From time to time I migrate some of these into the distribution, though maybe we need a systematic policy for doing this.
Larry
Email Gateway (Jan 10 2024 at 13:50):From: Tobias Nipkow <nipkow@in.tum.de>
Peter pointed out a number of places where (smalle) variations of the same thm
are proved. I am tempted to put only the most general version into List.thy -
s/h can prove the others, I checked. Let me know if you disagree strongly.
Tobias
Email Gateway (Jan 10 2024 at 14:24):From: Peter Lammich <lammich@in.tum.de>
I would argue that
finite_distinct: "finite s ⟹ finite {xs . set xs ⊆ s ∧ distinct xs}"
is the version we should have in List.thy. Maybe modulo conj_commute.
This lemma is simple to use, and general enough to easily derive more
general lemmas, like combinations with finite_subset, etc. It's also
what most of the AFP entries proved.
Email Gateway (Jan 11 2024 at 10:26):From: Tobias Nipkow <nipkow@in.tum.de>
Peter: Done, thanks.
Tobias
Last updated: Apr 29 2024 at 01:08 UTC