Re: [isabelle] lemma on Suc-bounded allquantification



Christian,

I have added your lemmas:

http://isabelle.in.tum.de/repos/isabelle/diff/962c12353c67/src/HOL/Nat.thy

Tobias

On 09/08/2017 10:56, Christian Sternagel wrote:
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

On 08/08/2017 04:38 PM, Johannes HÃlzl wrote:
All_less_Suc is in the distribution:

   http://isabelle.in.tum.de/repos/isabelle/rev/e44f5c123f26

Best,
  - Johannes



On Tue, 2017-08-08 at 12:37 +0200, Christian Sternagel wrote:
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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.