Re: [isabelle] Floor and ceiling



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 ;-)

- Brian

On Tue, Apr 3, 2012 at 1:57 PM, Tobias Nipkow <nipkow at 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
>>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.