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

Florian Haftmann florian at haftmann-online.de
Sat Jul 2 21:07:50 CEST 2016

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160702/8629fe94/attachment.asc>

More information about the isabelle-dev mailing list