author bulwahn Sat Feb 25 09:07:41 2012 +0100 (2012-02-25) changeset 46671 3a40ea076230 parent 46670 e9aa6d151329 child 46672 3fc49e6998da
removing unnecessary assumptions in RComplete;
simplifying proof in Probability
```     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.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.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 *}
```