Re: [isabelle] lemma on Suc-bounded allquantification


I have added your lemmas:


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.



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

  - 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
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)?



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

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