[isabelle-dev] {0::nat..<n} = {..<n}
Andreas Röhler
andreas.roehler at easy-emacs.de
Tue Jul 5 08:58:23 CEST 2016
Hallo,
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.
Cheers,
Andreas
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