src/HOL/Library/Liminf_Limsup.thy
 changeset 53381 355a4cac5440 parent 53374 a14d2a854c02 child 54257 5c7a3b6b05a9
```--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -169,15 +169,15 @@
moreover
{ fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
-    proof cases
-      assume "\<exists>z. y < z \<and> z < C"
-      then guess z .. note z = this
+    proof (cases "\<exists>z. y < z \<and> z < C")
+      case True
+      then obtain z where z: "y < z \<and> z < C" ..
moreover from z have "z \<le> INFI {x. z < X x} X"
by (auto intro!: INF_greatest)
ultimately show ?thesis
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
next
-      assume "\<not> (\<exists>z. y < z \<and> z < C)"
+      case False
then have "C \<le> INFI {x. y < X x} X"
by (intro INF_greatest) auto
with `y < C` show ?thesis
@@ -240,22 +240,22 @@
next
fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
show "y \<le> f0"
-  proof cases
-    assume "\<exists>z. f0 < z \<and> z < y"
-    then guess z ..
+  proof (cases "\<exists>z. f0 < z \<and> z < y")
+    case True
+    then obtain z where "f0 < z \<and> z < y" ..
moreover have "SUPR {x. f x < z} f \<le> z"
by (rule SUP_least) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
next
-    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+    case False
show ?thesis
proof (rule classical)
assume "\<not> y \<le> f0"
then have "eventually (\<lambda>x. f x < y) F"
using lim[THEN topological_tendstoD, of "{..< y}"] by auto
then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using discrete by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_elim1 simp: not_less)
then have "y \<le> SUPR {x. f x \<le> f0} f"
by (rule lower)
moreover have "SUPR {x. f x \<le> f0} f \<le> f0"```