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

[Florian Haftmann]

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

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/20160704/f0bb11d1/attachment.sig>