Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Floor and ceiling


view this post on Zulip Email Gateway (Aug 18 2022 at 19:27):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

I recently had to work with floor and ceiling where I was missing the following two monotonicity lemmas. Perhaps these are useful to someone else.

lemma floor_lesseq_add: "floor (x :: 'a :: floor_ceiling) + floor y \<le> floor (x + y)"
proof -
let ?f = floor
let ?i = of_int
let ?if = "\<lambda> x :: 'a. ?i (?f x)"
note fc = floor_correct
have "?f x + ?f y = ?if x + ?if y" by simp
also have "... \<le> ?f (x + y - ?if x - ?if y) + (?if x + ?if y)"
using fc[of x] fc[of y]
by (auto simp: field_simps)
also have "... = ?f (x + y)" unfolding floor_diff_of_int by simp
finally show ?thesis .
qed

lemma ceiling_lesseq_add: "ceiling (x + y) \<le> ceiling (x :: 'a :: floor_ceiling) + ceiling y" using floor_lesseq_add[of "- x" "- y"] unfolding floor_minus
using floor_minus[of "x + y"] by simp

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 19:28):

From: Tobias Nipkow <nipkow@in.tum.de>
René,

I appreciate the lemma, but the proof is really a bit pedestrian.
I prefer

by (metis add_le_cancel_left floor_add_of_int le_floor_iff order_eq_refl
order_trans)

;-)

Tobias

view this post on Zulip Email Gateway (Aug 18 2022 at 19:28):

From: Brian Huffman <huffman@in.tum.de>
Ok, I just added the following two lemmas to Archimedean_Field.thy
(rev 5e5ca36692b3).

lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)

lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)

Tobias' proof still seemed a bit overkill in my opinion ;-)

view this post on Zulip Email Gateway (Aug 18 2022 at 19:28):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 03/04/2012 14:17, schrieb Brian Huffman:

Ok, I just added the following two lemmas to Archimedean_Field.thy
(rev 5e5ca36692b3).

lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)

lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)

Tobias' proof still seemed a bit overkill in my opinion ;-)

But it took me fewer keystrokes to produce it ;-)

Tobias

On Tue, Apr 3, 2012 at 1:57 PM, Tobias Nipkow <nipkow@in.tum.de> wrote:

René,

I appreciate the lemma, but the proof is really a bit pedestrian.
I prefer

by (metis add_le_cancel_left floor_add_of_int le_floor_iff order_eq_refl
order_trans)

;-)

Tobias

Am 03/04/2012 12:59, schrieb René Thiemann:

lemma floor_lesseq_add: "floor (x :: 'a :: floor_ceiling) + floor y \<le> floor (x + y)"
proof -
let ?f = floor
let ?i = of_int
let ?if = "\<lambda> x :: 'a. ?i (?f x)"
note fc = floor_correct
have "?f x + ?f y = ?if x + ?if y" by simp
also have "... \<le> ?f (x + y - ?if x - ?if y) + (?if x + ?if y)"
using fc[of x] fc[of y]
by (auto simp: field_simps)
also have "... = ?f (x + y)" unfolding floor_diff_of_int by simp
finally show ?thesis .
qed

view this post on Zulip Email Gateway (Aug 18 2022 at 19:28):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Thanks for the addition and the shortening.
(I am quite sure that I tried sledgehammer first, but perhaps at that
time I stated the wrong lemma)

René

view this post on Zulip Email Gateway (Aug 18 2022 at 19:29):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 03/04/2012 14:55, schrieb René Thiemann:

Thanks for the addition and the shortening.
(I am quite sure that I tried sledgehammer first, but perhaps at that
time I stated the wrong lemma)

Disn't you have auto-quickcheck on? ;-)

Tobias

René

Am 03.04.2012 um 14:23 schrieb Tobias Nipkow:

>
>

Am 03/04/2012 14:17, schrieb Brian Huffman:

Ok, I just added the following two lemmas to Archimedean_Field.thy
(rev 5e5ca36692b3).

lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)

lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)

Tobias' proof still seemed a bit overkill in my opinion ;-)

But it took me fewer keystrokes to produce it ;-)

Tobias

  • Brian

On Tue, Apr 3, 2012 at 1:57 PM, Tobias Nipkow <nipkow@in.tum.de> wrote:

René,

I appreciate the lemma, but the proof is really a bit pedestrian.
I prefer

by (metis add_le_cancel_left floor_add_of_int le_floor_iff order_eq_refl
order_trans)

;-)

Tobias

Am 03/04/2012 12:59, schrieb René Thiemann:

lemma floor_lesseq_add: "floor (x :: 'a :: floor_ceiling) + floor y \<le> floor (x + y)"
proof -
let ?f = floor
let ?i = of_int
let ?if = "\<lambda> x :: 'a. ?i (?f x)"
note fc = floor_correct
have "?f x + ?f y = ?if x + ?if y" by simp
also have "... \<le> ?f (x + y - ?if x - ?if y) + (?if x + ?if y)"
using fc[of x] fc[of y]
by (auto simp: field_simps)
also have "... = ?f (x + y)" unfolding floor_diff_of_int by simp
finally show ?thesis .
qed

view this post on Zulip Email Gateway (Aug 19 2022 at 15:33):

From: "W. Douglas Maurer" <maurer@gwu.edu>
I am using Isabelle 2013-2. I was trying to use the floor symbols
from the Symbols window. Looking at \<lfloor> under Punctuation, I
see abbrev: [. Looking at \<rfloor>, I see abbrev: .] So the floor of
x, then, should be [. x .] But then I looked at the ceiling symbols.
Looking at \<lceil>, I see abbrev: [. Looking at \<rceil>, I see
abbrev: .] So the ceiling of x, then, should also be [. x .] This
can't be right. What is [. x .] ? Is it floor(x) or is it ceiling(x)?
Or has this already been fixed in the 2014 edition? Thanks! -Douglas

view this post on Zulip Email Gateway (Aug 19 2022 at 15:33):

From: Makarius <makarius@sketis.net>
There is nothing broken and nothing to be fixed here, merely a
misunderstanding of what symbol abbreviations are. See also the
Isabelle/jEdit manual page 16:

Note that the above abbreviations refer to the input method. The logical
notation provides ASCII alternatives that often coincide, but deviate
occasionally. This occasionally causes user confusion with very
old-fashioned Isabelle source that use ASCII replacement notation like !
or ALL directly in the text.

There is more text around it that talks about input methods for Isabelle
symbols. You don't write any ASCII abbreviations in the final text, and
[. x .] is invalid in the normal term syntax anyway.

In Isabelle2014 the Isabelle/jEdit manual is once again longer and more
thorough, and the input mechanisms have been refined as well.

Makarius


Last updated: Mar 29 2024 at 04:18 UTC