Re: [isabelle-dev] {0::nat..

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

Tobias

On 02/07/2016 21:07, Florian Haftmann wrote:

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.

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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev