author bulwahn Sat, 25 Feb 2012 09:07:41 +0100 changeset 46671 3a40ea076230 parent 46670 e9aa6d151329 child 46672 3fc49e6998da
removing unnecessary assumptions in RComplete; simplifying proof in Probability
 src/HOL/Probability/Lebesgue_Integration.thy file | annotate | diff | comparison | revisions src/HOL/RComplete.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Feb 25 09:07:39 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sat Feb 25 09:07:41 2012 +0100
@@ -366,7 +366,7 @@
also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
proof cases
assume "0 \<le> u x" then show ?thesis
-            by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
+            by (intro le_mult_natfloor)
next
assume "\<not> 0 \<le> u x" then show ?thesis
by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)```
```--- a/src/HOL/RComplete.thy	Sat Feb 25 09:07:39 2012 +0100
+++ b/src/HOL/RComplete.thy	Sat Feb 25 09:07:41 2012 +0100
@@ -415,10 +415,9 @@
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"

-lemma natfloor_subtract [simp]: "real a <= x ==>
-    natfloor(x - real a) = natfloor x - a"
-  unfolding natfloor_def
-  unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
+lemma natfloor_subtract [simp]:
+    "natfloor(x - real a) = natfloor x - a"
+  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
by simp

lemma natfloor_div_nat:
@@ -441,10 +440,9 @@
qed

lemma le_mult_natfloor:
-  assumes "0 \<le> (a :: real)" and "0 \<le> b"
shows "natfloor a * natfloor b \<le> natfloor (a * b)"
-  using assms
-  by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
+  by (cases "0 <= a & 0 <= b")
+    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)

lemma natceiling_zero [simp]: "natceiling 0 = 0"
by (unfold natceiling_def, simp)
@@ -505,10 +503,8 @@
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"