<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<tt>Hallo,</tt><tt><br>
</tt><tt>being beginner in I</tt><tt>sabell</tt><tt>e, you may </tt><tt>sa</tt><tt>f</tt><tt>ely
ignore </tt><tt>this post.</tt><tt><br>
<br>
</tt><tt>AFAIU {..<n} wouldn't protect against negative integers
and might deliver wrong positive. </tt><tt><br>
</tt><tt>AFAIK the question</tt><tt> if </tt><tt>0 is part of
natural numbers is disputed. </tt><tt>Was there some solution in
recent years?</tt><tt><br>
</tt><tt>Depending on that {1..<n} might be an option too in some
cases.</tt><tt><br>
<br>
</tt><tt>Cheers,</tt><tt><br>
</tt><tt>Andreas</tt><br>
<br>
<div class="moz-cite-prefix">On 05.07.2016 08:38, Tobias Nipkow
wrote:<br>
</div>
<blockquote
cite="mid:79e2e6cf-972e-f005-86d1-022596fa5846@in.tum.de"
type="cite">Florian,
<br>
<br>
The whole setup has grown over time and initially I may have
preferred {..<n} just like you did. I would welcome your
proposed changes.
<br>
<br>
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.
<br>
<br>
Tobias
<br>
<br>
On 04/07/2016 21:00, Florian Haftmann wrote:
<br>
<blockquote type="cite">
<blockquote type="cite">The problem with {..<n} on nat is
that you need multiple versions of
<br>
every lemma involving {m..<n} on nat. Hence I discourage
the use of
<br>
{..<n} on nat. If you add {0..<n} = {..<n} it will
solve many but not
<br>
all problems: not all proof methods invoke simp all the time.
<br>
<br>
I consider {..<n} on nat an anomaly that should be avoided
because one
<br>
gains very little by using it. One could even think aout
replacing it by
<br>
{0..<n} upon parsing.
<br>
</blockquote>
<br>
OK, then {0..<n} is the canonical representative. And, as I
did not
<br>
realize before, rules concerning {0..<?n} are obviously
equally simple
<br>
to state as rules concerning {..<?n}, particulary induction
on the upper
<br>
bound.
<br>
<br>
However then I suggest to add a few lemmas to emphasize that
decision, e.g.
<br>
<br>
lemma lessThan_atLeast0:
<br>
fixes n :: nat
<br>
shows "{..<n} = {0..<n}"
<br>
by (simp add: atLeast0LessThan)
<br>
<br>
lemma atMost_atLeast0:
<br>
fixes n :: nat
<br>
shows "{..n} = {0..n}"
<br>
by (simp add: atLeast0AtMost)
<br>
<br>
Currently, only their symmetrics are present, but not these,
which would
<br>
suggest that {..<n} is the canonical form.
<br>
<br>
Similarly for {0..<Suc n} = insert n {0..n} vs. {..<Suc
n} = insert n
<br>
{..n}
<br>
<br>
What remains a little bit unsatisfactory is the printing of sums
and
<br>
products:
<br>
<br>
term "setsum (\<lambda>n. n ^ 3) {0..<m::nat}" --
\<open>\<Sum>n =
<br>
0..<m. n ^ 3\<close>
<br>
term "setsum (\<lambda>n. n ^ 3) {..<m::nat}" --
\<open>\<Sum>n<m. n ^
<br>
3\<close>
<br>
term "setsum (\<lambda>n. n ^ 3) {0..m::nat}" --
\<open>\<Sum>n = 0..m.
<br>
n ^ 3\<close>
<br>
term "setsum (\<lambda>n. n ^ 3) {..m::nat}" --
\<open>\<Sum>n\<le>m. n
<br>
^ 3\<close>
<br>
<br>
Here the non-canonical forms are superior to read, but I think
we can
<br>
live with that.
<br>
<br>
Since I have currently laid hands-on on that matter, I would
offer to
<br>
add lessThan_atLeast0, atMost_atLeast0 and {0..<Suc n} =
insert n
<br>
{0..n} to the distribution. I would also polish one or two
definitions
<br>
in Binomial.thy which currently involve the non-canonical forms.
<br>
<br>
Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable
candidates for
<br>
default simp rules also then.
<br>
<br>
Cheers,
<br>
Florian
<br>
<br>
<blockquote type="cite">
<blockquote type="cite">obviously on natural numbers
{0..<n} = {..<n} holds, and the right
<br>
hand side is also more convenient to work with (no
preconditions on m
<br>
being less or equal n etc.). But for historic reasons,
{0..<n} is
<br>
still the preferred variant in many theorems, cf.
find_theorems
<br>
"{0::nat..<_}".
<br>
<br>
I'm tempted to say that these occurrences should be
normalized to
<br>
{..<n} and {0..<n} = {..<n} be added as default
simp rule, but I
<br>
leave it to experts on intervals to judge.
<br>
</blockquote>
</blockquote>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>