summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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"