[isabelle-dev] {0::nat..<n} = {..<n}
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Mon Jul 4 21:00:55 CEST 2016
> 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.
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160704/f0bb11d1/attachment.sig>
More information about the isabelle-dev
mailing list