[isabelle-dev] {0::nat..<n} = {..<n}

Andreas Röhler andreas.roehler at easy-emacs.de
Tue Jul 5 08:58:23 CEST 2016

being beginner in Isabelle, you may safely ignore this post.

AFAIU {..<n} wouldn't protect against negative integers and might 
deliver wrong positive.
AFAIK the questionif 0 is part of natural numbers is disputed. Was there 
some solution in recent years?
Depending on that {1..<n} might be an option too in some cases.


On 05.07.2016 08:38, Tobias Nipkow wrote:
> Florian,
> The whole setup has grown over time and initially I may have preferred 
> {..<n} just like you did. I would welcome your proposed changes.
> I agree, sums look nicer with {..<n}, but look at the bright side: 
> {0..<n} clearly shows that the set/sum is bounded, something that is 
> otherwise implicit in the type.
> Tobias
> On 04/07/2016 21:00, Florian Haftmann wrote:
>>> The problem with {..<n} on nat is that you need multiple versions of
>>> every lemma involving {m..<n} on nat. Hence I discourage the use of
>>> {..<n} on nat. If you add ‹{0..<n} = {..<n}› it will solve many but not
>>> all problems: not all proof methods invoke simp all the time.
>>> I consider {..<n} on nat an anomaly that should be avoided because one
>>> gains very little by using it. One could even think aout replacing 
>>> it by
>>> {0..<n} upon parsing.
>> OK, then {0..<n} is the canonical representative.  And, as I did not
>> realize before, rules concerning {0..<?n} are obviously equally simple
>> to state as rules concerning {..<?n}, particulary induction on the upper
>> bound.
>> However then I suggest to add a few lemmas to emphasize that 
>> decision, e.g.
>> lemma lessThan_atLeast0:
>>   fixes n :: nat
>>   shows "{..<n} = {0..<n}"
>>   by (simp add: atLeast0LessThan)
>> lemma atMost_atLeast0:
>>   fixes n :: nat
>>   shows "{..n} = {0..n}"
>>   by (simp add: atLeast0AtMost)
>> Currently, only their symmetrics are present, but not these, which would
>> suggest that {..<n} is the canonical form.
>> Similarly for ‹{0..<Suc n} = insert n {0..n}› vs. ‹{..<Suc n} = insert n
>> {..n}›
>> What remains a little bit unsatisfactory is the printing of sums and
>> products:
>> term "setsum (\<lambda>n. n ^ 3) {0..<m::nat}" -- \<open>\<Sum>n =
>> 0..<m. n ^ 3\<close>
>> term "setsum (\<lambda>n. n ^ 3) {..<m::nat}" -- \<open>\<Sum>n<m. n ^
>> 3\<close>
>> term "setsum (\<lambda>n. n ^ 3) {0..m::nat}" -- \<open>\<Sum>n = 0..m.
>> n ^ 3\<close>
>> term "setsum (\<lambda>n. n ^ 3) {..m::nat}" -- \<open>\<Sum>n\<le>m. n
>> ^ 3\<close>
>> Here the non-canonical forms are superior to read, but I think we can
>> live with that.
>> Since I have currently laid hands-on on that matter, I would offer to
>> add lessThan_atLeast0, atMost_atLeast0 and ‹{0..<Suc n} = insert n
>> {0..n}› to the distribution.  I would also polish one or two definitions
>> in Binomial.thy which currently involve the non-canonical forms.
>> Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable candidates for
>> default simp rules also then.
>> Cheers,
>>     Florian
>>>> obviously on natural numbers ‹{0..<n} = {..<n}› holds, and the right
>>>> hand side is also more convenient to work with (no preconditions on m
>>>> being less or equal n etc.). But for historic reasons, ‹{0..<n}› is
>>>> still the preferred variant in many theorems, cf. ‹find_theorems
>>>> "{0::nat..<_}"›.
>>>> I'm tempted to say that these occurrences should be normalized to
>>>> ‹{..<n}› and ‹{0..<n} = {..<n}› be added as default simp rule, but I
>>>> leave it to experts on intervals to judge.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160705/37fd1eee/attachment-0002.html>

More information about the isabelle-dev mailing list