Re: [isabelle] Floor and ceiling
Ok, I just added the following two lemmas to Archimedean_Field.thy
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 ;-)
On Tue, Apr 3, 2012 at 1:57 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 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
> 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 .
This archive was generated by a fusion of
Pipermail (Mailman edition) and