# HG changeset patch
# User hoelzl
# Date 1362494588 -3600
# Node ID 5e6296afe08d6804a3dbdb929f0174569f61795e
# Parent  04ebef4ee84474ee39f3e87494f0c9359fc8cc6d
move Liminf / Limsup lemmas on complete_lattices to its own file

diff -r 04ebef4ee844 -r 5e6296afe08d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:43:08 2013 +0100
@@ -8,7 +8,7 @@
 header {* Extended real number line *}
 
 theory Extended_Real
-imports Complex_Main Extended_Nat
+imports Complex_Main Extended_Nat Liminf_Limsup
 begin
 
 text {*
@@ -18,26 +18,6 @@
 
 *}
 
-lemma SUPR_pair:
-  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
-  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
-
-lemma INFI_pair:
-  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
-  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
-
-lemma le_Sup_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
-  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
-  unfolding le_SUP_iff
-  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
-
-lemma Inf_le_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
-  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
-  unfolding INF_le_iff
-  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
-
 subsection {* Definition and basic properties *}
 
 datatype ereal = ereal real | PInfty | MInfty
@@ -1718,6 +1698,31 @@
   show thesis by auto
 qed
 
+instance ereal :: perfect_space
+proof (default, rule)
+  fix a :: ereal assume a: "open {a}"
+  show False
+  proof (cases a)
+    case MInf
+    then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
+    then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
+    then show False using `a = -\<infinity>` by auto
+  next
+    case PInf
+    then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
+    then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
+    then show False using `a = \<infinity>` by auto
+  next
+    case (real r)
+    then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
+    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
+    then obtain b where b_def: "a<b \<and> b<a+e"
+      using fin ereal_between dense[of a "a+e"] by auto
+    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
+    then show False using b_def e by auto
+  qed
+qed
+
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]:
@@ -1981,123 +1986,15 @@
     using ereal_LimI_finite[of x] assms by auto
 qed
 
-
-subsubsection {* @{text Liminf} and @{text Limsup} *}
-
-definition
-  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
-
-definition
-  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
-
-abbreviation "liminf \<equiv> Liminf sequentially"
-
-abbreviation "limsup \<equiv> Limsup sequentially"
-
-lemma Liminf_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
-    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
-  unfolding Liminf_def by (auto intro!: SUP_eqI)
-
-lemma Limsup_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
-    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
-  unfolding Limsup_def by (auto intro!: INF_eqI)
-
-lemma liminf_SUPR_INFI:
-  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
-  shows "liminf f = (SUP n. INF m:{n..}. f m)"
-  unfolding Liminf_def eventually_sequentially
-  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
-
-lemma limsup_INFI_SUPR:
-  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
-  shows "limsup f = (INF n. SUP m:{n..}. f m)"
-  unfolding Limsup_def eventually_sequentially
-  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
-
-lemma Limsup_const: 
-  assumes ntriv: "\<not> trivial_limit F"
-  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
-proof -
-  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
-  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
-    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
-  then show ?thesis
-    unfolding Limsup_def using eventually_True
-    by (subst INF_cong[where D="\<lambda>x. c"])
-       (auto intro!: INF_const simp del: eventually_True)
-qed
+lemma ereal_Limsup_uminus:
+  fixes f :: "'a => ereal"
+  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
+  unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
 
-lemma Liminf_const:
-  assumes ntriv: "\<not> trivial_limit F"
-  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
-proof -
-  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
-  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
-    using ntriv by (intro INF_const) (auto simp: eventually_False *)
-  then show ?thesis
-    unfolding Liminf_def using eventually_True
-    by (subst SUP_cong[where D="\<lambda>x. c"])
-       (auto intro!: SUP_const simp del: eventually_True)
-qed
-
-lemma Liminf_mono:
-  fixes f g :: "'a => 'b :: complete_lattice"
-  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
-  shows "Liminf F f \<le> Liminf F g"
-  unfolding Liminf_def
-proof (safe intro!: SUP_mono)
-  fix P assume "eventually P F"
-  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
-  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
-    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
-qed
-
-lemma Liminf_eq:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
-  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
-
-lemma Limsup_mono:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
-  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
-  shows "Limsup F f \<le> Limsup F g"
-  unfolding Limsup_def
-proof (safe intro!: INF_mono)
-  fix P assume "eventually P F"
-  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
-  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
-    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
-qed
-
-lemma Limsup_eq:
-  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
-  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
-
-lemma Liminf_le_Limsup:
-  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
-  assumes ntriv: "\<not> trivial_limit F"
-  shows "Liminf F f \<le> Limsup F f"
-  unfolding Limsup_def Liminf_def
-  apply (rule complete_lattice_class.SUP_least)
-  apply (rule complete_lattice_class.INF_greatest)
-proof safe
-  fix P Q assume "eventually P F" "eventually Q F"
-  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
-  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
-    using ntriv by (auto simp add: eventually_False)
-  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
-    by (rule INF_mono) auto
-  also have "\<dots> \<le> SUPR (Collect ?C) f"
-    using not_False by (intro INF_le_SUP) auto
-  also have "\<dots> \<le> SUPR (Collect Q) f"
-    by (rule SUP_mono) auto
-  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
-qed
+lemma liminf_bounded_iff:
+  fixes x :: "nat \<Rightarrow> ereal"
+  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
+  unfolding le_Liminf_iff eventually_sequentially ..
 
 lemma
   fixes X :: "nat \<Rightarrow> ereal"
@@ -2105,220 +2002,6 @@
     and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
   unfolding incseq_def decseq_def by auto
 
-lemma Liminf_bounded:
-  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
-  shows "C \<le> Liminf F X"
-  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
-
-lemma Limsup_bounded:
-  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
-  shows "Limsup F X \<le> C"
-  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
-
-lemma le_Liminf_iff:
-  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
-  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
-proof -
-  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
-    then have "eventually (\<lambda>x. y < X x) F"
-      by (auto elim!: eventually_elim1 dest: less_INF_D) }
-  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 ..
-      moreover then 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)"
-      then have "C \<le> INFI {x. y < X x} X"
-        by (intro INF_greatest) auto
-      with `y < C` show ?thesis
-        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
-    qed }
-  ultimately show ?thesis
-    unfolding Liminf_def le_SUP_iff by auto
-qed
-
-lemma lim_imp_Liminf:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Liminf F f = f0"
-proof (intro Liminf_eqI)
-  fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
-    by eventually_elim (auto intro!: INF_lower)
-  then show "INFI (Collect P) f \<le> f0"
-    by (rule tendsto_le[OF ntriv lim tendsto_const])
-next
-  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
-  show "f0 \<le> y"
-  proof cases
-    assume "\<exists>z. y < z \<and> z < f0"
-    then guess z ..
-    moreover have "z \<le> INFI {x. z < f x} f"
-      by (rule INF_greatest) simp
-    ultimately show ?thesis
-      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
-  next
-    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
-    show ?thesis
-    proof (rule classical)
-      assume "\<not> f0 \<le> y"
-      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)
-      then have "INFI {x. f0 \<le> f x} f \<le> y"
-        by (rule upper)
-      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
-        by (intro INF_greatest) simp
-      ultimately show "f0 \<le> y" by simp
-    qed
-  qed
-qed
-
-lemma lim_imp_Limsup:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Limsup F f = f0"
-proof (intro Limsup_eqI)
-  fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
-    by eventually_elim (auto intro!: SUP_upper)
-  then show "f0 \<le> SUPR (Collect P) f"
-    by (rule tendsto_le[OF ntriv tendsto_const lim])
-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 ..
-    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)"
-    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)
-      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"
-        by (intro SUP_least) simp
-      ultimately show "y \<le> f0" by simp
-    qed
-  qed
-qed
-
-lemma Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-    and lim: "Liminf F f = f0" "Limsup F f = f0"
-  shows "(f ---> f0) F"
-proof (rule order_tendstoI)
-  fix a assume "f0 < a"
-  with assms have "Limsup F f < a" by simp
-  then obtain P where "eventually P F" "SUPR (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)
-next
-  fix a assume "a < f0"
-  with assms have "a < Liminf F f" by simp
-  then obtain P where "eventually P F" "a < INFI (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)
-qed
-
-lemma tendsto_iff_Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
-  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
-  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
-
-lemma liminf_bounded_iff:
-  fixes x :: "nat \<Rightarrow> ereal"
-  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
-  unfolding le_Liminf_iff eventually_sequentially ..
-
-lemma liminf_subseq_mono:
-  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
-  shows "liminf X \<le> liminf (X \<circ> r) "
-proof-
-  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
-  proof (safe intro!: INF_mono)
-    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
-      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
-  qed
-  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
-qed
-
-lemma limsup_subseq_mono:
-  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
-  shows "limsup (X \<circ> r) \<le> limsup X"
-proof-
-  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
-  proof (safe intro!: SUP_mono)
-    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
-      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
-  qed
-  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
-qed
-
-definition (in order) mono_set:
-  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
-
-lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
-lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
-lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
-lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
-
-lemma (in complete_linorder) mono_set_iff:
-  fixes S :: "'a set"
-  defines "a \<equiv> Inf S"
-  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
-proof
-  assume "mono_set S"
-  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
-  show ?c
-  proof cases
-    assume "a \<in> S"
-    show ?c
-      using mono[OF _ `a \<in> S`]
-      by (auto intro: Inf_lower simp: a_def)
-  next
-    assume "a \<notin> S"
-    have "S = {a <..}"
-    proof safe
-      fix x assume "x \<in> S"
-      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
-      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
-    next
-      fix x assume "a < x"
-      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
-      with mono[of y x] show "x \<in> S" by auto
-    qed
-    then show ?c ..
-  qed
-qed auto
-
 subsubsection {* Tests for code generator *}
 
 (* A small list of simple arithmetic expressions *)
diff -r 04ebef4ee844 -r 5e6296afe08d src/HOL/Library/Liminf_Limsup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 05 15:43:08 2013 +0100
@@ -0,0 +1,320 @@
+(*  Title:      HOL/Library/Liminf_Limsup.thy
+    Author:     Johannes Hölzl, TU München
+*)
+
+header {* Liminf and Limsup on complete lattices *}
+
+theory Liminf_Limsup
+imports "~~/src/HOL/Complex_Main"
+begin
+
+lemma le_Sup_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+  unfolding le_SUP_iff
+  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
+lemma Inf_le_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  unfolding INF_le_iff
+  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
+lemma SUPR_pair:
+  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
+
+lemma INFI_pair:
+  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
+
+subsubsection {* @{text Liminf} and @{text Limsup} *}
+
+definition
+  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+
+definition
+  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+
+abbreviation "liminf \<equiv> Liminf sequentially"
+
+abbreviation "limsup \<equiv> Limsup sequentially"
+
+lemma Liminf_eqI:
+  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
+    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
+  unfolding Liminf_def by (auto intro!: SUP_eqI)
+
+lemma Limsup_eqI:
+  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
+    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
+  unfolding Limsup_def by (auto intro!: INF_eqI)
+
+lemma liminf_SUPR_INFI:
+  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+  shows "liminf f = (SUP n. INF m:{n..}. f m)"
+  unfolding Liminf_def eventually_sequentially
+  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
+
+lemma limsup_INFI_SUPR:
+  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+  shows "limsup f = (INF n. SUP m:{n..}. f m)"
+  unfolding Limsup_def eventually_sequentially
+  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
+
+lemma Limsup_const: 
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
+  then show ?thesis
+    unfolding Limsup_def using eventually_True
+    by (subst INF_cong[where D="\<lambda>x. c"])
+       (auto intro!: INF_const simp del: eventually_True)
+qed
+
+lemma Liminf_const:
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+    using ntriv by (intro INF_const) (auto simp: eventually_False *)
+  then show ?thesis
+    unfolding Liminf_def using eventually_True
+    by (subst SUP_cong[where D="\<lambda>x. c"])
+       (auto intro!: SUP_const simp del: eventually_True)
+qed
+
+lemma Liminf_mono:
+  fixes f g :: "'a => 'b :: complete_lattice"
+  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+  shows "Liminf F f \<le> Liminf F g"
+  unfolding Liminf_def
+proof (safe intro!: SUP_mono)
+  fix P assume "eventually P F"
+  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
+    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
+qed
+
+lemma Liminf_eq:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  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
+
+lemma Limsup_mono:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+  shows "Limsup F f \<le> Limsup F g"
+  unfolding Limsup_def
+proof (safe intro!: INF_mono)
+  fix P assume "eventually P F"
+  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
+    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
+qed
+
+lemma Limsup_eq:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  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
+
+lemma Liminf_le_Limsup:
+  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Liminf F f \<le> Limsup F f"
+  unfolding Limsup_def Liminf_def
+  apply (rule complete_lattice_class.SUP_least)
+  apply (rule complete_lattice_class.INF_greatest)
+proof safe
+  fix P Q assume "eventually P F" "eventually Q F"
+  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
+  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
+    using ntriv by (auto simp add: eventually_False)
+  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
+    by (rule INF_mono) auto
+  also have "\<dots> \<le> SUPR (Collect ?C) f"
+    using not_False by (intro INF_le_SUP) auto
+  also have "\<dots> \<le> SUPR (Collect Q) f"
+    by (rule SUP_mono) auto
+  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
+qed
+
+lemma Liminf_bounded:
+  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
+  shows "C \<le> Liminf F X"
+  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
+
+lemma Limsup_bounded:
+  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
+  shows "Limsup F X \<le> C"
+  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+
+lemma le_Liminf_iff:
+  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
+  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
+proof -
+  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+    then have "eventually (\<lambda>x. y < X x) F"
+      by (auto elim!: eventually_elim1 dest: less_INF_D) }
+  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 ..
+      moreover then 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)"
+      then have "C \<le> INFI {x. y < X x} X"
+        by (intro INF_greatest) auto
+      with `y < C` show ?thesis
+        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+    qed }
+  ultimately show ?thesis
+    unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Liminf F f = f0"
+proof (intro Liminf_eqI)
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+    by eventually_elim (auto intro!: INF_lower)
+  then show "INFI (Collect P) f \<le> f0"
+    by (rule tendsto_le[OF ntriv lim tendsto_const])
+next
+  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+  show "f0 \<le> y"
+  proof cases
+    assume "\<exists>z. y < z \<and> z < f0"
+    then guess z ..
+    moreover have "z \<le> INFI {x. z < f x} f"
+      by (rule INF_greatest) simp
+    ultimately show ?thesis
+      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+  next
+    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+    show ?thesis
+    proof (rule classical)
+      assume "\<not> f0 \<le> y"
+      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)
+      then have "INFI {x. f0 \<le> f x} f \<le> y"
+        by (rule upper)
+      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+        by (intro INF_greatest) simp
+      ultimately show "f0 \<le> y" by simp
+    qed
+  qed
+qed
+
+lemma lim_imp_Limsup:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Limsup F f = f0"
+proof (intro Limsup_eqI)
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+    by eventually_elim (auto intro!: SUP_upper)
+  then show "f0 \<le> SUPR (Collect P) f"
+    by (rule tendsto_le[OF ntriv tendsto_const lim])
+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 ..
+    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)"
+    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)
+      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"
+        by (intro SUP_least) simp
+      ultimately show "y \<le> f0" by simp
+    qed
+  qed
+qed
+
+lemma Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+    and lim: "Liminf F f = f0" "Limsup F f = f0"
+  shows "(f ---> f0) F"
+proof (rule order_tendstoI)
+  fix a assume "f0 < a"
+  with assms have "Limsup F f < a" by simp
+  then obtain P where "eventually P F" "SUPR (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)
+next
+  fix a assume "a < f0"
+  with assms have "a < Liminf F f" by simp
+  then obtain P where "eventually P F" "a < INFI (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)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
+lemma liminf_subseq_mono:
+  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+  assumes "subseq r"
+  shows "liminf X \<le> liminf (X \<circ> r) "
+proof-
+  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+  proof (safe intro!: INF_mono)
+    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
+      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+  qed
+  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
+qed
+
+lemma limsup_subseq_mono:
+  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+  assumes "subseq r"
+  shows "limsup (X \<circ> r) \<le> limsup X"
+proof-
+  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
+  proof (safe intro!: SUP_mono)
+    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
+      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+  qed
+  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
+qed
+
+end
diff -r 04ebef4ee844 -r 5e6296afe08d src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:43:08 2013 +0100
@@ -22,35 +22,13 @@
 
 lemma ereal_open_uminus:
   fixes S :: "ereal set"
-  assumes "open S"
-  shows "open (uminus ` S)"
-  unfolding open_ereal_def
-proof (intro conjI impI)
-  obtain x y where
-    S: "open (ereal -` S)" "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
-    using `open S` unfolding open_ereal_def by auto
-  have "ereal -` uminus ` S = uminus ` (ereal -` S)"
-  proof safe
-    fix x y
-    assume "ereal x = - y" "y \<in> S"
-    then show "x \<in> uminus ` ereal -` S" by (cases y) auto
-  next
-    fix x
-    assume "ereal x \<in> S"
-    then show "- x \<in> ereal -` uminus ` S"
-      by (auto intro: image_eqI[of _ _ "ereal x"])
-  qed
-  then show "open (ereal -` uminus ` S)"
-    using S by (auto intro: open_negations)
-  { assume "\<infinity> \<in> uminus ` S"
-    then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
-    then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
-    then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
-  { assume "-\<infinity> \<in> uminus ` S"
-    then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
-    then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
-    then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
-qed
+  assumes "open S" shows "open (uminus ` S)"
+  using `open S`[unfolded open_generated_order]
+proof induct
+  have "range uminus = (UNIV :: ereal set)"
+    by (auto simp: image_iff ereal_uminus_eq_reorder)
+  then show "open (range uminus :: ereal set)" by simp
+qed (auto simp add: image_Union image_Int)
 
 lemma ereal_uminus_complement:
   fixes S :: "ereal set"
@@ -61,32 +39,7 @@
   fixes S :: "ereal set"
   assumes "closed S"
   shows "closed (uminus ` S)"
-  using assms unfolding closed_def
-  using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
-
-instance ereal :: perfect_space
-proof (default, rule)
-  fix a :: ereal assume a: "open {a}"
-  show False
-  proof (cases a)
-    case MInf
-    then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
-    then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
-    then show False using `a=(-\<infinity>)` by auto
-  next
-    case PInf
-    then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
-    then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
-    then show False using `a=\<infinity>` by auto
-  next
-    case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
-    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
-    then obtain b where b_def: "a<b & b<a+e"
-      using fin ereal_between dense[of a "a+e"] by auto
-    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
-    then show False using b_def e by auto
-  qed
-qed
+  using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
 
 lemma ereal_closed_contains_Inf:
   fixes S :: "ereal set"
@@ -303,113 +256,9 @@
   then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
 qed
 
-lemma ereal_open_mono_set:
-  fixes S :: "ereal set"
-  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
-  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
-    ereal_open_closed mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_closed_mono_set:
-  fixes S :: "ereal set"
-  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
-  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
-    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_Liminf_Sup_monoset:
-  fixes f :: "'a => ereal"
-  shows "Liminf net f =
-    Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
-    (is "_ = Sup ?A")
-proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
-  fix P assume P: "eventually P net"
-  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
-  { fix x assume "P x"
-    then have "INFI (Collect P) f \<le> f x"
-      by (intro complete_lattice_class.INF_lower) simp
-    with S have "f x \<in> S"
-      by (simp add: mono_set) }
-  with P show "eventually (\<lambda>x. f x \<in> S) net"
-    by (auto elim: eventually_elim1)
-next
-  fix y l
-  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
-  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
-  show "l \<le> y"
-  proof (rule dense_le)
-    fix B assume "B < l"
-    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
-      by (intro S[rule_format]) auto
-    then have "INFI {x. B < f x} f \<le> y"
-      using P by auto
-    moreover have "B \<le> INFI {x. B < f x} f"
-      by (intro INF_greatest) auto
-    ultimately show "B \<le> y"
-      by simp
-  qed
-qed
-
-lemma ereal_Limsup_Inf_monoset:
-  fixes f :: "'a => ereal"
-  shows "Limsup net f =
-    Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
-    (is "_ = Inf ?A")
-proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
-  fix P assume P: "eventually P net"
-  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
-  { fix x assume "P x"
-    then have "f x \<le> SUPR (Collect P) f"
-      by (intro complete_lattice_class.SUP_upper) simp
-    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
-    have "f x \<in> S"
-      by (simp add: inj_image_mem_iff) }
-  with P show "eventually (\<lambda>x. f x \<in> S) net"
-    by (auto elim: eventually_elim1)
-next
-  fix y l
-  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
-  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
-  show "y \<le> l"
-  proof (rule dense_ge)
-    fix B assume "l < B"
-    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
-      by (intro S[rule_format]) auto
-    then have "y \<le> SUPR {x. f x < B} f"
-      using P by auto
-    moreover have "SUPR {x. f x < B} f \<le> B"
-      by (intro SUP_least) auto
-    ultimately show "y \<le> B"
-      by simp
-  qed
-qed
-
 lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
 
-lemma ereal_Limsup_uminus:
-  fixes f :: "'a => ereal"
-  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
-proof -
-  { fix P l
-    have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)"
-      by (auto intro!: exI[of _ "-l"]) }
-  note Ex_cancel = this
-  { fix P :: "ereal set \<Rightarrow> bool"
-    have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
-      apply auto
-      apply (erule_tac x="uminus`S" in allE)
-      apply (auto simp: image_image)
-      done }
-  note add_uminus_image = this
-  { fix x S
-    have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S"
-      by (auto intro!: image_eqI[of _ _ "-x"]) }
-  note remove_uminus_image = this
-  show ?thesis
-    unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
-    unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
-    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
-qed
-
 lemma ereal_Liminf_uminus:
   fixes f :: "'a => ereal"
   shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
@@ -423,14 +272,6 @@
     ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   by (auto simp: ereal_uminus_reorder)
 
-lemma lim_imp_Limsup:
-  fixes f :: "'a => ereal"
-  assumes "\<not> trivial_limit net"
-    and lim: "(f ---> f0) net"
-  shows "Limsup net f = f0"
-  using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
-     ereal_Liminf_uminus[of net f] assms by simp
-
 lemma convergent_ereal_limsup:
   fixes X :: "nat \<Rightarrow> ereal"
   shows "convergent X \<Longrightarrow> limsup X = lim X"
@@ -461,43 +302,10 @@
   using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
         ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
 
-lemma ereal_Liminf_eq_Limsup:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes ntriv: "\<not> trivial_limit net"
-    and lim: "Liminf net f = f0" "Limsup net f = f0"
-  shows "(f ---> f0) net"
-proof (cases f0)
-  case PInf
-  then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
-next
-  case MInf
-  then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
-next
-  case (real r)
-  show "(f ---> f0) net"
-  proof (rule topological_tendstoI)
-    fix S
-    assume "open S" "f0 \<in> S"
-    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
-      using ereal_open_cont_interval2[of S f0] real lim by auto
-    then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
-      unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
-      by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
-    with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
-      by (rule_tac eventually_mono) auto
-  qed
-qed
-
-lemma ereal_Liminf_eq_Limsup_iff:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<not> trivial_limit net"
-  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
-  by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
-
 lemma convergent_ereal:
   fixes X :: "nat \<Rightarrow> ereal"
   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
-  using ereal_Liminf_eq_Limsup_iff[of sequentially]
+  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   by (auto simp: convergent_def)
 
 lemma limsup_INFI_SUPR:
@@ -535,45 +343,6 @@
   shows "X N >= L"
   using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
 
-lemma liminf_bounded_open:
-  fixes x :: "nat \<Rightarrow> ereal"
-  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
-  (is "_ \<longleftrightarrow> ?P x0")
-proof
-  assume "?P x0"
-  then show "x0 \<le> liminf x"
-    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
-    by (intro complete_lattice_class.Sup_upper) auto
-next
-  assume "x0 \<le> liminf x"
-  { fix S :: "ereal set"
-    assume om: "open S & mono_set S & x0:S"
-    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
-    moreover
-    { assume "~(S=UNIV)"
-      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
-      then have "B<x0" using om by auto
-      then have "EX N. ALL n>=N. x n : S"
-        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
-    }
-    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
-  }
-  then show "?P x0" by auto
-qed
-
-lemma limsup_subseq_mono:
-  fixes X :: "nat \<Rightarrow> ereal"
-  assumes "subseq r"
-  shows "limsup (X \<circ> r) \<le> limsup X"
-proof -
-  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
-  then have "- limsup X \<le> - limsup (X \<circ> r)"
-     using liminf_subseq_mono[of r "(%n. - X n)"]
-       ereal_Liminf_uminus[of sequentially X]
-       ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
-  then show ?thesis by auto
-qed
-
 lemma bounded_abs:
   assumes "(a::real)<=x" "x<=b"
   shows "abs x <= max (abs a) (abs b)"
@@ -652,85 +421,6 @@
     show "f ----> x" by auto }
 qed
 
-lemma Liminf_within:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
-  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
-  unfolding Liminf_def eventually_within
-proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
-  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
-  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
-  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
-    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
-next
-  fix d :: real assume "0 < d"
-  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
-    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
-    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
-       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
-qed
-
-lemma Limsup_within:
-  fixes f :: "'a::metric_space => 'b::complete_lattice"
-  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
-  unfolding Limsup_def eventually_within
-proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
-  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
-  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
-  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
-    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
-next
-  fix d :: real assume "0 < d"
-  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
-    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
-    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
-       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
-qed
-
-lemma Liminf_within_UNIV:
-  fixes f :: "'a::metric_space => _"
-  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
-  by simp (* TODO: delete *)
-
-
-lemma Liminf_at:
-  fixes f :: "'a::metric_space => _"
-  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
-  using Liminf_within[of x UNIV f] by simp
-
-
-lemma Limsup_within_UNIV:
-  fixes f :: "'a::metric_space => _"
-  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
-  by simp (* TODO: delete *)
-
-
-lemma Limsup_at:
-  fixes f :: "'a::metric_space => _"
-  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
-  using Limsup_within[of x UNIV f] by simp
-
-lemma Lim_within_constant:
-  assumes "ALL y:S. f y = C"
-  shows "(f ---> C) (at x within S)"
-  unfolding tendsto_def Limits.eventually_within eventually_at_topological
-  using assms by simp (metis open_UNIV UNIV_I)
-
-lemma Liminf_within_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> ereal"
-  assumes "ALL y:S. f y = C"
-    and "~trivial_limit (at x within S)"
-  shows "Liminf (at x within S) f = C"
-  by (metis Lim_within_constant assms lim_imp_Liminf)
-
-lemma Limsup_within_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> ereal"
-  assumes "ALL y:S. f y = C"
-    and "~trivial_limit (at x within S)"
-  shows "Limsup (at x within S) f = C"
-  by (metis Lim_within_constant assms lim_imp_Limsup)
-
 lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
   unfolding islimpt_def by blast
 
@@ -1317,4 +1007,205 @@
   then show "\<forall>i. f i = 0" by auto
 qed simp
 
+lemma Liminf_within:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
+  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+  unfolding Liminf_def eventually_within
+proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
+  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+    by (auto simp: zero_less_dist_iff dist_commute)
+  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
+    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
+next
+  fix d :: real assume "0 < d"
+  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
+    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
+qed
+
+lemma Limsup_within:
+  fixes f :: "'a::metric_space => 'b::complete_lattice"
+  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+  unfolding Limsup_def eventually_within
+proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
+  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+    by (auto simp: zero_less_dist_iff dist_commute)
+  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
+    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
+next
+  fix d :: real assume "0 < d"
+  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
+    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
+qed
+
+lemma Liminf_at:
+  fixes f :: "'a::metric_space => _"
+  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
+  using Liminf_within[of x UNIV f] by simp
+
+lemma Limsup_at:
+  fixes f :: "'a::metric_space => _"
+  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
+  using Limsup_within[of x UNIV f] by simp
+
+lemma min_Liminf_at:
+  fixes f :: "'a::metric_space => 'b::complete_linorder"
+  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
+  unfolding inf_min[symmetric] Liminf_at
+  apply (subst inf_commute)
+  apply (subst SUP_inf)
+  apply (intro SUP_cong[OF refl])
+  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
+  apply (simp add: INF_def del: inf_ereal_def)
+  done
+
+subsection {* monoset *}
+
+definition (in order) mono_set:
+  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
+
+lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
+
+lemma (in complete_linorder) mono_set_iff:
+  fixes S :: "'a set"
+  defines "a \<equiv> Inf S"
+  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
+proof
+  assume "mono_set S"
+  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
+  show ?c
+  proof cases
+    assume "a \<in> S"
+    show ?c
+      using mono[OF _ `a \<in> S`]
+      by (auto intro: Inf_lower simp: a_def)
+  next
+    assume "a \<notin> S"
+    have "S = {a <..}"
+    proof safe
+      fix x assume "x \<in> S"
+      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
+      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
+    next
+      fix x assume "a < x"
+      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
+      with mono[of y x] show "x \<in> S" by auto
+    qed
+    then show ?c ..
+  qed
+qed auto
+
+lemma ereal_open_mono_set:
+  fixes S :: "ereal set"
+  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
+  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
+    ereal_open_closed mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_closed_mono_set:
+  fixes S :: "ereal set"
+  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
+  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
+    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_Liminf_Sup_monoset:
+  fixes f :: "'a => ereal"
+  shows "Liminf net f =
+    Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+    (is "_ = Sup ?A")
+proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
+  fix P assume P: "eventually P net"
+  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
+  { fix x assume "P x"
+    then have "INFI (Collect P) f \<le> f x"
+      by (intro complete_lattice_class.INF_lower) simp
+    with S have "f x \<in> S"
+      by (simp add: mono_set) }
+  with P show "eventually (\<lambda>x. f x \<in> S) net"
+    by (auto elim: eventually_elim1)
+next
+  fix y l
+  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
+  show "l \<le> y"
+  proof (rule dense_le)
+    fix B assume "B < l"
+    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
+      by (intro S[rule_format]) auto
+    then have "INFI {x. B < f x} f \<le> y"
+      using P by auto
+    moreover have "B \<le> INFI {x. B < f x} f"
+      by (intro INF_greatest) auto
+    ultimately show "B \<le> y"
+      by simp
+  qed
+qed
+
+lemma ereal_Limsup_Inf_monoset:
+  fixes f :: "'a => ereal"
+  shows "Limsup net f =
+    Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+    (is "_ = Inf ?A")
+proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
+  fix P assume P: "eventually P net"
+  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
+  { fix x assume "P x"
+    then have "f x \<le> SUPR (Collect P) f"
+      by (intro complete_lattice_class.SUP_upper) simp
+    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
+    have "f x \<in> S"
+      by (simp add: inj_image_mem_iff) }
+  with P show "eventually (\<lambda>x. f x \<in> S) net"
+    by (auto elim: eventually_elim1)
+next
+  fix y l
+  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
+  show "y \<le> l"
+  proof (rule dense_ge)
+    fix B assume "l < B"
+    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
+      by (intro S[rule_format]) auto
+    then have "y \<le> SUPR {x. f x < B} f"
+      using P by auto
+    moreover have "SUPR {x. f x < B} f \<le> B"
+      by (intro SUP_least) auto
+    ultimately show "y \<le> B"
+      by simp
+  qed
+qed
+
+lemma liminf_bounded_open:
+  fixes x :: "nat \<Rightarrow> ereal"
+  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
+  (is "_ \<longleftrightarrow> ?P x0")
+proof
+  assume "?P x0"
+  then show "x0 \<le> liminf x"
+    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
+    by (intro complete_lattice_class.Sup_upper) auto
+next
+  assume "x0 \<le> liminf x"
+  { fix S :: "ereal set"
+    assume om: "open S & mono_set S & x0:S"
+    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
+    moreover
+    { assume "~(S=UNIV)"
+      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
+      then have "B<x0" using om by auto
+      then have "EX N. ALL n>=N. x n : S"
+        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
+    }
+    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
+  }
+  then show "?P x0" by auto
+qed
+
 end
diff -r 04ebef4ee844 -r 5e6296afe08d src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 15:27:08 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 15:43:08 2013 +0100
@@ -2190,7 +2190,7 @@
     using diff positive_integral_positive[of M]
     by (subst integral_eq_positive_integral[of _ M]) (auto simp: ereal_real integrable_def)
   then show ?lim_diff
-    using ereal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
+    using Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
     by simp
 
   show ?lim