Re: [isabelle-dev] {0::nat..<n} = {..<n}
> The whole setup has grown over time and initially I may have preferred
> {..
> I agree, sums look nicer with {.. {0.. otherwise implicit in the type.
>
> Tobias
>
> On 04/07/2016 21:00, Florian Haftmann wrote:
>>> The problem with {..>> every lemma involving {m..>> {..>> all problems: not all proof methods invoke simp all the time.
>>>
>>> I consider {..>> gains very little by using it. One could even think aout replacing it by
>>> {0..>
>> OK, then {0..> realize before, rules concerning {0..> to state as rules concerning {..> bound.
>>
>> However then I suggest to add a few lemmas to emphasize that decision,
>> e.g.
>>
>> lemma lessThan_atLeast0:
>> fixes n :: nat
>> shows "{..> 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 {..>
>> Similarly for ‹{0..> {..n}›
>>
>> What remains a little bit unsatisfactory is the printing of sums and
>> products:
>>
>> term "setsum (\n. n ^ 3) {0..> 0..
>> term "setsum (\n. n ^ 3) {.. 3\
>> term "setsum (\n. n ^ 3) {0..m::nat}" -- \\n = 0..m.
>> n ^ 3\
>> term "setsum (\n. n ^ 3) {..m::nat}" -- \\n\m. n
>> ^ 3\
>>
>> 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..> {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..
>
>
> ___
> 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
Re: [isabelle-dev] {0::nat..<n} = {..<n}
Hello Andreas,
> AFAIU {.. deliver wrong positive.
> AFAIK the questionif 0 is part of natural numbers is disputed. Was there
> some solution in recent years?
> Depending on that {1..
> Cheers,
> Andreas
>
> On 05.07.2016 08:38, Tobias Nipkow wrote:
>> Florian,
>>
>> The whole setup has grown over time and initially I may have preferred
>> {..>
>> I agree, sums look nicer with {..> {0..> otherwise implicit in the type.
>>
>> Tobias
>>
>> On 04/07/2016 21:00, Florian Haftmann wrote:
The problem with {..>>
>>> OK, then {0..>> realize before, rules concerning {0..>> to state as rules concerning {..>> bound.
>>>
>>> However then I suggest to add a few lemmas to emphasize that
>>> decision, e.g.
>>>
>>> lemma lessThan_atLeast0:
>>> fixes n :: nat
>>> shows "{..>> 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 {..>>
>>> Similarly for ‹{0..>> {..n}›
>>>
>>> What remains a little bit unsatisfactory is the printing of sums and
>>> products:
>>>
>>> term "setsum (\n. n ^ 3) {0..>> 0..
>>> term "setsum (\n. n ^ 3) {..> 3\
>>> term "setsum (\n. n ^ 3) {0..m::nat}" -- \\n = 0..m.
>>> n ^ 3\
>>> term "setsum (\n. n ^ 3) {..m::nat}" -- \\n\m. n
>>> ^ 3\
>>>
>>> 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..>> {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.. hand side is also more convenient to work with (no preconditions on m
> being less or equal n etc.). But for historic reasons, ‹{0.. still the preferred variant in many theorems, cf. ‹find_theorems
> "{0::nat..<_}"›.
>
> I'm tempted to say that these occurrences should be normalized to
> ‹{.. 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
>
>
>
> ___
> 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
Re: [isabelle-dev] {0::nat..<n} = {..<n}
Hallo,
being beginner in Isabelle, you may safely ignore this post.
AFAIU {..
Re: [isabelle-dev] {0::nat..<n} = {..<n}
Florian,
The whole setup has grown over time and initially I may have preferred {..
Re: [isabelle-dev] {0::nat..<n} = {..<n}
> The problem with {.. every lemma involving {m.. {.. all problems: not all proof methods invoke simp all the time.
>
> I consider {.. gains very little by using it. One could even think aout replacing it by
> {0.. obviously on natural numbers ‹{0..> hand side is also more convenient to work with (no preconditions on m
>> being less or equal n etc.). But for historic reasons, ‹{0..> still the preferred variant in many theorems, cf. ‹find_theorems
>> "{0::nat..<_}"›.
>>
>> I'm tempted to say that these occurrences should be normalized to
>> ‹{..> leave it to experts on intervals to judge.
--
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
Re: [isabelle-dev] {0::nat..<n} = {..<n}
The problem with {..
[isabelle-dev] {0::nat..<n} = {..<n}
Hi all,
obviously on natural numbers ‹{0..
