1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Feb 25 09:07:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sat Feb 25 09:07:41 2012 +0100
     1.3 @@ -366,7 +366,7 @@
     1.4          also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
     1.5          proof cases
     1.6            assume "0 \<le> u x" then show ?thesis
     1.7 -            by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
     1.8 +            by (intro le_mult_natfloor) 
     1.9          next
    1.10            assume "\<not> 0 \<le> u x" then show ?thesis
    1.11              by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)

     2.1 --- a/src/HOL/RComplete.thy	Sat Feb 25 09:07:39 2012 +0100
     2.2 +++ b/src/HOL/RComplete.thy	Sat Feb 25 09:07:41 2012 +0100
     2.3 @@ -415,10 +415,9 @@
     2.4  lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
     2.5    by (simp add: natfloor_add [symmetric] del: One_nat_def)
     2.6  
     2.7 -lemma natfloor_subtract [simp]: "real a <= x ==>
     2.8 -    natfloor(x - real a) = natfloor x - a"
     2.9 -  unfolding natfloor_def
    2.10 -  unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
    2.11 +lemma natfloor_subtract [simp]:
    2.12 +    "natfloor(x - real a) = natfloor x - a"
    2.13 +  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
    2.14    by simp
    2.15  
    2.16  lemma natfloor_div_nat:
    2.17 @@ -441,10 +440,9 @@
    2.18  qed
    2.19  
    2.20  lemma le_mult_natfloor:
    2.21 -  assumes "0 \<le> (a :: real)" and "0 \<le> b"
    2.22    shows "natfloor a * natfloor b \<le> natfloor (a * b)"
    2.23 -  using assms
    2.24 -  by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
    2.25 +  by (cases "0 <= a & 0 <= b")
    2.26 +    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
    2.27  
    2.28  lemma natceiling_zero [simp]: "natceiling 0 = 0"
    2.29    by (unfold natceiling_def, simp)
    2.30 @@ -505,10 +503,8 @@
    2.31  lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
    2.32    by (simp add: natceiling_add [symmetric] del: One_nat_def)
    2.33  
    2.34 -lemma natceiling_subtract [simp]: "real a <= x ==>
    2.35 -    natceiling(x - real a) = natceiling x - a"
    2.36 -  unfolding natceiling_def
    2.37 -  unfolding real_of_int_of_nat_eq [symmetric] ceiling_subtract
    2.38 +lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
    2.39 +  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
    2.40    by simp
    2.41  
    2.42  subsection {* Exponentiation with floor *}