src/HOL/RComplete.thy
 changeset 46671 3a40ea076230 parent 45966 03ce2b2a29a2 child 47108 2a1953f0d20d
```     1.1 --- a/src/HOL/RComplete.thy	Sat Feb 25 09:07:39 2012 +0100
1.2 +++ b/src/HOL/RComplete.thy	Sat Feb 25 09:07:41 2012 +0100
1.3 @@ -415,10 +415,9 @@
1.4  lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
1.5    by (simp add: natfloor_add [symmetric] del: One_nat_def)
1.6
1.7 -lemma natfloor_subtract [simp]: "real a <= x ==>
1.8 -    natfloor(x - real a) = natfloor x - a"
1.9 -  unfolding natfloor_def
1.10 -  unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
1.11 +lemma natfloor_subtract [simp]:
1.12 +    "natfloor(x - real a) = natfloor x - a"
1.13 +  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
1.14    by simp
1.15
1.16  lemma natfloor_div_nat:
1.17 @@ -441,10 +440,9 @@
1.18  qed
1.19
1.20  lemma le_mult_natfloor:
1.21 -  assumes "0 \<le> (a :: real)" and "0 \<le> b"
1.22    shows "natfloor a * natfloor b \<le> natfloor (a * b)"
1.23 -  using assms
1.24 -  by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
1.25 +  by (cases "0 <= a & 0 <= b")
1.26 +    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
1.27
1.28  lemma natceiling_zero [simp]: "natceiling 0 = 0"
1.29    by (unfold natceiling_def, simp)
1.30 @@ -505,10 +503,8 @@
1.31  lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
1.32    by (simp add: natceiling_add [symmetric] del: One_nat_def)
1.33
1.34 -lemma natceiling_subtract [simp]: "real a <= x ==>
1.35 -    natceiling(x - real a) = natceiling x - a"
1.36 -  unfolding natceiling_def
1.37 -  unfolding real_of_int_of_nat_eq [symmetric] ceiling_subtract
1.38 +lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
1.39 +  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
1.40    by simp
1.41
1.42  subsection {* Exponentiation with floor *}
```