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

[Florian Haftmann]

> The whole setup has grown over time and initially I may have preferred
> {..<n} just like you did. I would welcome your proposed changes.

See now c184ec919c70.

The core addition are substantial theorems concerning indexed sums and
products, using locale comm_monoid_set to provide them uniformly for
setsum and setprod.

I still hesitated to add suitable default simp rules.  Let's see…

Cheers,
	Florian

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160711/6f8f3f2d/attachment.sig>