src/HOL/Library/Liminf_Limsup.thy
changeset 61810 3c5040d5694a
parent 61806 d2e62ae01cd8
child 61880 ff4d33058566
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -100,7 +100,7 @@
 lemma Liminf_eq:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
 
 lemma Limsup_mono:
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
 lemma Limsup_eq:
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
 
 lemma Liminf_le_Limsup:
   assumes ntriv: "\<not> trivial_limit F"
@@ -167,7 +167,7 @@
 proof -
   have "eventually (\<lambda>x. y < X x) F"
     if "eventually P F" "y < INFIMUM (Collect P) X" for y P
-    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
+    using that by (auto elim!: eventually_mono dest: less_INF_D)
   moreover
   have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
@@ -218,7 +218,7 @@
       then have "eventually (\<lambda>x. y < f x) F"
         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
       then have "eventually (\<lambda>x. f0 \<le> f x) F"
-        using discrete by (auto elim!: eventually_elim1)
+        using discrete by (auto elim!: eventually_mono)
       then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
         by (rule upper)
       moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
@@ -257,7 +257,7 @@
       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 False by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_mono simp: not_less)
       then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
         by (rule lower)
       moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
@@ -278,14 +278,14 @@
   then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
     unfolding Limsup_def INF_less_iff by auto
   then show "eventually (\<lambda>x. f x < a) F"
-    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+    by (auto elim!: eventually_mono dest: SUP_lessD)
 next
   fix a assume "a < f0"
   with assms have "a < Liminf F f" by simp
   then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
     unfolding Liminf_def less_SUP_iff by auto
   then show "eventually (\<lambda>x. a < f x) F"
-    by (auto elim!: eventually_elim1 dest: less_INF_D)
+    by (auto elim!: eventually_mono dest: less_INF_D)
 qed
 
 lemma tendsto_iff_Liminf_eq_Limsup: