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-- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
