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

[Tobias Nipkow]

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.

Tobias

On 02/07/2016 21:07, Florian Haftmann wrote:
> Hi all,
> 	
> 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.
> 	
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- 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/20160703/957a1b4f/attachment.bin>