Re: [isabelle] lemma on Suc-bounded allquantification
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)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and