Email Gateway (Aug 22 2022 at 15:49): Email Gateway (Aug 22 2022 at 15:49):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Johannes,
thanks! So I just have to wait for the next release ;)
What about the equivalent lemma for exists?
cheers
chris
Email Gateway (Aug 22 2022 at 15:50):From: Christian Sternagel <c.sternagel@gmail.com>
Sorry, my last reply was to fast ;)
The lemma you suggest separates the last number from the previous ones,
but I suggested a lemma that separates 0 from the remaining numbers
(since this is often useful for proving results that also talk about lists).
And the same is also useful for exists.
cheers
chris
Email Gateway (Aug 22 2022 at 15:50):From: Tobias Nipkow <nipkow@in.tum.de>
Christian,
I have added your lemmas:
http://isabelle.in.tum.de/repos/isabelle/diff/962c12353c67/src/HOL/Nat.thy
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:57):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I seem to reprove the following lemma a lot recently (which I then use
as a simp rule):
lemma all_Suc_conv: "(∀i<Suc n. P i) ⟷ P 0 ∧ (∀i<n. P (Suc i))"
using less_Suc_eq_0_disj by auto
Any chance that it might end up in the Isabelle distribution (at least I
did not find it in Isabelle2016-1)?
cheers
chris
Email Gateway (Aug 22 2022 at 15:58):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
All_less_Suc is in the distribution:
http://isabelle.in.tum.de/repos/isabelle/rev/e44f5c123f26
Best,
Last updated: Nov 21 2024 at 12:39 UTC