> The whole setup has grown over time and initially I may have preferred > {..<n} just like you did. I would welcome your proposed changes.
See now c184ec919c70. The core addition are substantial theorems concerning indexed sums and products, using locale comm_monoid_set to provide them uniformly for setsum and setprod. I still hesitated to add suitable default simp rules. Let's see… Cheers, Florian > > 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, >> Florian >> >>>> 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. > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev