Email Gateway (Aug 18 2022 at 19:27): 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é
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
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 ;-)
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
- 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 preferby (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
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é
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 preferby (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
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
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: Nov 21 2024 at 12:39 UTC