Email Gateway (Aug 18 2022 at 13:28): Email Gateway (Aug 18 2022 at 13:28):From: Tobias Nipkow <nipkow@in.tum.de>
Many thanks, much appreciated, esp the inductive lemmas!
Tobias
Andreas Lochbihler schrieb:
Email Gateway (Aug 18 2022 at 13:34):From: Matthias Daum <md11@wjpserver.cs.uni-sb.de>
Dear list,
it seams as if the former list isabelle-lemmas@cl.cam.ac.uk has
vanished? If you are still interested in extending the basic
Isabelle/HOL theories by lemmata from their users, you might consider to
include the following lemmata, which I needed during my work with Isabelle:
lemma ex_ivl_less: (EX i:{..<n}. P i) = (EX i<n. P i)
and all_ivl_less: (ALL i:{..<n}. P i) = (ALL i<n. P i)
by auto
lemma distinct_takeWhile:
"distinct xs ==> distinct (takeWhile P xs)"
proof (induct xs)
case (Cons x xs)
thus ?case by clarsimp (frule set_take_whileD, clarsimp)
qed simp
Moreover, the two following lemmata could be incorporated into the
library's theory Nat_Infinity:
instance inat :: "{linorder}"
by intro_classes (auto simp add: inat_defs split: inat_splits)
lemma not_Infty_eq: "(x ~= Infty) = (EX i. x = Fin i)"
by (cases x) auto
Furthermore, I have enclosed a theory for the summation of a list of
values. I am not sure, whether you prefer to incorporate the definition
and proofs in the basic List theory or store it somewhere at the
libraries...
Unfortunately, the proofs are checked only in Isabelle/HOL 2005, I hope,
they still run through in the newest Isabelle release.
Best regards,
Matthias.
list_sum.thy
Email Gateway (Aug 18 2022 at 13:34):From: Tobias Nipkow <nipkow@in.tum.de>
Many thanks for your input, I have already moved half your lemmas into
the distribution. You seem to be the only one who provides new lemmas.
Hence we removed isabelle-lemmas@cl.cam.ac.uk - it may even have
attracted spam, I cannot remember. If other people suddenly feel
motivated to provide additional lemmas and there is too much of it on
this list, this would motivate us to think again about new ways of
integrating your contributions.
Tobias
PS I'll let you know separately what I added and how.
Matthias Daum schrieb:
Last updated: Nov 21 2024 at 12:39 UTC