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

[Tobias Nipkow]

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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160705/db8bbddd/attachment.bin>