author wenzelm Tue, 03 Sep 2013 00:51:08 +0200 changeset 53373 3ca9e79ac926 parent 53372 f5a6313c7fe4 child 53374 a14d2a854c02
proper imports; tuned proofs;
```--- a/src/HOL/ex/Dedekind_Real.thy	Mon Sep 02 23:35:58 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Sep 03 00:51:08 2013 +0200
@@ -8,7 +8,7 @@
*)

theory Dedekind_Real
-imports Rat Lubs
+imports Complex_Main
begin

section {* Positive real numbers *}
@@ -782,7 +782,7 @@
have "r + ?d < r*x"
proof -
have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
-      also with ypos have "... = (r/y) * (y + ?d)"
+      also from ypos have "... = (r/y) * (y + ?d)"
by (simp only: algebra_simps divide_inverse, simp)
also have "... = r*x" using ypos
by simp
@@ -1785,10 +1785,10 @@
proof
fix pa
assume "pa \<in> ?pS"
-    then obtain a where "a \<in> S" and "a = real_of_preal pa"
+    then obtain a where a: "a \<in> S" "a = real_of_preal pa"
by simp
-    moreover hence "a \<le> u" using sup by simp
-    ultimately show "pa \<le> pu"
+    then have "a \<le> u" using sup by simp
+    with a show "pa \<le> pu"
using sup and u_is_pu by (simp add: real_of_preal_le_iff)
qed

@@ -1864,9 +1864,9 @@
fix s
assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
hence "\<exists> x \<in> S. s = x + -X + 1" ..
-      then obtain x1 where "x1 \<in> S" and "s = x1 + (-X) + 1" ..
-      moreover hence "x1 \<le> x" using S_le_x by simp
-      ultimately have "s \<le> x + - X + 1" by arith
+      then obtain x1 where x1: "x1 \<in> S" "s = x1 + (-X) + 1" ..
+      then have "x1 \<le> x" using S_le_x by simp
+      with x1 have "s \<le> x + - X + 1" by arith
}
then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
by (auto simp add: isUb_def setle_def)```