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 *}