Florian,The whole setup has grown over time and initially I may have preferred {..<n} just like you did. I would welcome your proposed changes.
I agree, sums look nicer with {..<n}, but look at the bright side: {0..<n} clearly shows that the set/sum is bounded, something that is otherwise implicit in the type.
Tobias On 04/07/2016 21:00, Florian Haftmann wrote:
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, Florianobviously 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.
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
