use order topology for extended reals
authorhoelzl
Thu Jan 31 11:31:30 2013 +0100 (2013-01-31)
changeset 51000c9adb50f74ad
parent 50999 3de230ed0547
child 51001 461fdbbdb912
use order topology for extended reals
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Discrete_Topology.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Regularity.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports Main
     1.8 +imports "~~/src/HOL/Main"
     1.9  begin
    1.10  
    1.11  class infinity =
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jan 31 11:31:27 2013 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jan 31 11:31:30 2013 +0100
     2.3 @@ -8,9 +8,32 @@
     2.4  header {* Extended real number line *}
     2.5  
     2.6  theory Extended_Real
     2.7 -imports Complex_Main Extended_Nat
     2.8 +imports "~~/src/HOL/Complex_Main" Extended_Nat
     2.9  begin
    2.10  
    2.11 +lemma LIMSEQ_SUP:
    2.12 +  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
    2.13 +  assumes "incseq X"
    2.14 +  shows "X ----> (SUP i. X i)"
    2.15 +  using `incseq X`
    2.16 +  by (intro increasing_tendsto)
    2.17 +     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
    2.18 +
    2.19 +lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
    2.20 +  by (cases P) (simp_all add: eventually_False)
    2.21 +
    2.22 +lemma (in complete_lattice) Inf_le_Sup:
    2.23 +  assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
    2.24 +proof -
    2.25 +  from `A \<noteq> {}` obtain x where "x \<in> A" by auto
    2.26 +  then show ?thesis
    2.27 +    by (metis Sup_upper2 Inf_lower)
    2.28 +qed
    2.29 +
    2.30 +lemma (in complete_lattice) INF_le_SUP:
    2.31 +  "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
    2.32 +  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
    2.33 +
    2.34  text {*
    2.35  
    2.36  For more lemmas about the extended real numbers go to
    2.37 @@ -18,6 +41,26 @@
    2.38  
    2.39  *}
    2.40  
    2.41 +lemma (in complete_lattice) Sup_eqI:
    2.42 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
    2.43 +  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
    2.44 +  shows "Sup A = x"
    2.45 +  by (metis antisym Sup_least Sup_upper assms)
    2.46 +
    2.47 +lemma (in complete_lattice) Inf_eqI:
    2.48 +  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
    2.49 +  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
    2.50 +  shows "Inf A = x"
    2.51 +  by (metis antisym Inf_greatest Inf_lower assms)
    2.52 +
    2.53 +lemma (in complete_lattice) SUP_eqI:
    2.54 +  "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x"
    2.55 +  unfolding SUP_def by (rule Sup_eqI) auto
    2.56 +
    2.57 +lemma (in complete_lattice) INF_eqI:
    2.58 +  "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x"
    2.59 +  unfolding INF_def by (rule Inf_eqI) auto
    2.60 +
    2.61  lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
    2.62  proof
    2.63    assume "{x..} = UNIV"
    2.64 @@ -1353,22 +1396,6 @@
    2.65    unfolding Sup_ereal_def
    2.66    by (auto intro!: Least_equality)
    2.67  
    2.68 -lemma ereal_SUPI:
    2.69 -  fixes x :: ereal
    2.70 -  assumes "!!i. i : A ==> f i <= x"
    2.71 -  assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
    2.72 -  shows "(SUP i:A. f i) = x"
    2.73 -  unfolding SUP_def Sup_ereal_def
    2.74 -  using assms by (auto intro!: Least_equality)
    2.75 -
    2.76 -lemma ereal_INFI:
    2.77 -  fixes x :: ereal
    2.78 -  assumes "!!i. i : A ==> f i >= x"
    2.79 -  assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
    2.80 -  shows "(INF i:A. f i) = x"
    2.81 -  unfolding INF_def Inf_ereal_def
    2.82 -  using assms by (auto intro!: Greatest_equality)
    2.83 -
    2.84  lemma Sup_ereal_close:
    2.85    fixes e :: ereal
    2.86    assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
    2.87 @@ -1476,6 +1503,17 @@
    2.88      using assms by (metis SUP_least SUP_upper2)
    2.89  qed
    2.90  
    2.91 +lemma INFI_eq:
    2.92 +  assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
    2.93 +  assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
    2.94 +  shows "(INF i:A. f i) = (INF j:B. g j)"
    2.95 +proof (intro antisym)
    2.96 +  show "(INF i:A. f i) \<le> (INF j:B. g j)"
    2.97 +    using assms by (metis INF_greatest INF_lower2)
    2.98 +  show "(INF i:B. g i) \<le> (INF j:A. f j)"
    2.99 +    using assms by (metis INF_greatest INF_lower2)
   2.100 +qed
   2.101 +
   2.102  lemma SUP_ereal_le_addI:
   2.103    fixes f :: "'i \<Rightarrow> ereal"
   2.104    assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
   2.105 @@ -1491,7 +1529,7 @@
   2.106    fixes f g :: "nat \<Rightarrow> ereal"
   2.107    assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
   2.108    shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
   2.109 -proof (rule ereal_SUPI)
   2.110 +proof (rule SUP_eqI)
   2.111    fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
   2.112    have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
   2.113      unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
   2.114 @@ -1531,7 +1569,7 @@
   2.115  lemma SUPR_ereal_cmult:
   2.116    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
   2.117    shows "(SUP i. c * f i) = c * SUPR UNIV f"
   2.118 -proof (rule ereal_SUPI)
   2.119 +proof (rule SUP_eqI)
   2.120    fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
   2.121    then show "c * f i \<le> c * SUPR UNIV f"
   2.122      using `0 \<le> c` by (rule ereal_mult_left_mono)
   2.123 @@ -1598,7 +1636,7 @@
   2.124    qed
   2.125    from choice[OF this] guess f .. note f = this
   2.126    have "SUPR UNIV f = Sup A"
   2.127 -  proof (rule ereal_SUPI)
   2.128 +  proof (rule SUP_eqI)
   2.129      fix i show "f i \<le> Sup A" using f
   2.130        by (auto intro!: complete_lattice_class.Sup_upper)
   2.131    next
   2.132 @@ -1801,18 +1839,84 @@
   2.133  
   2.134  subsubsection "Topological space"
   2.135  
   2.136 -instantiation ereal :: topological_space
   2.137 +instantiation ereal :: linorder_topology
   2.138  begin
   2.139  
   2.140 -definition "open A \<longleftrightarrow> open (ereal -` A)
   2.141 -       \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A))
   2.142 -       \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
   2.143 +definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
   2.144 +  open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
   2.145 +
   2.146 +instance
   2.147 +  by default (simp add: open_ereal_generated)
   2.148 +end
   2.149  
   2.150  lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
   2.151 -  unfolding open_ereal_def by auto
   2.152 +  unfolding open_ereal_generated
   2.153 +proof (induct rule: generate_topology.induct)
   2.154 +  case (Int A B)
   2.155 +  moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
   2.156 +      by auto
   2.157 +  ultimately show ?case
   2.158 +    by (intro exI[of _ "max x z"]) fastforce
   2.159 +next
   2.160 +  { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
   2.161 +  moreover case (Basis S)
   2.162 +  ultimately show ?case
   2.163 +    by (auto split: ereal.split)
   2.164 +qed (fastforce simp add: vimage_Union)+
   2.165  
   2.166  lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
   2.167 -  unfolding open_ereal_def by auto
   2.168 +  unfolding open_ereal_generated
   2.169 +proof (induct rule: generate_topology.induct)
   2.170 +  case (Int A B)
   2.171 +  moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
   2.172 +      by auto
   2.173 +  ultimately show ?case
   2.174 +    by (intro exI[of _ "min x z"]) fastforce
   2.175 +next
   2.176 +  { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
   2.177 +  moreover case (Basis S)
   2.178 +  ultimately show ?case
   2.179 +    by (auto split: ereal.split)
   2.180 +qed (fastforce simp add: vimage_Union)+
   2.181 +
   2.182 +lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
   2.183 +  unfolding open_ereal_generated
   2.184 +proof (induct rule: generate_topology.induct)
   2.185 +  case (Int A B) then show ?case by auto
   2.186 +next
   2.187 +  { fix x have
   2.188 +      "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
   2.189 +      "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
   2.190 +      by (induct x) auto }
   2.191 +  moreover case (Basis S)
   2.192 +  ultimately show ?case
   2.193 +    by (auto split: ereal.split)
   2.194 +qed (fastforce simp add: vimage_Union)+
   2.195 +
   2.196 +lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
   2.197 +  unfolding open_generated_order[where 'a=real]
   2.198 +proof (induct rule: generate_topology.induct)
   2.199 +  case (Basis S)
   2.200 +  moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
   2.201 +  moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
   2.202 +  ultimately show ?case
   2.203 +     by auto
   2.204 +qed (auto simp add: image_Union image_Int)
   2.205 +
   2.206 +lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
   2.207 +  (is "open A \<longleftrightarrow> ?rhs")
   2.208 +proof
   2.209 +  assume "open A" then show ?rhs
   2.210 +    using open_PInfty open_MInfty open_ereal_vimage by auto
   2.211 +next
   2.212 +  assume "?rhs"
   2.213 +  then obtain x y where A: "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..< ereal y} \<subseteq> A"
   2.214 +    by auto
   2.215 +  have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
   2.216 +    using A(2,3) by auto
   2.217 +  from open_ereal[OF A(1)] show "open A"
   2.218 +    by (subst *) (auto simp: open_Un)
   2.219 +qed
   2.220  
   2.221  lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
   2.222    using open_PInfty[OF assms] by auto
   2.223 @@ -1821,85 +1925,17 @@
   2.224    using open_MInfty[OF assms] by auto
   2.225  
   2.226  lemma ereal_openE: assumes "open A" obtains x y where
   2.227 -  "open (ereal -` A)"
   2.228 -  "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
   2.229 -  "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
   2.230 +  "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
   2.231    using assms open_ereal_def by auto
   2.232  
   2.233 -instance
   2.234 -proof
   2.235 -  let ?U = "UNIV::ereal set"
   2.236 -  show "open ?U" unfolding open_ereal_def
   2.237 -    by (auto intro!: exI[of _ 0])
   2.238 -next
   2.239 -  fix S T::"ereal set" assume "open S" and "open T"
   2.240 -  from `open S`[THEN ereal_openE] guess xS yS .
   2.241 -  moreover from `open T`[THEN ereal_openE] guess xT yT .
   2.242 -  ultimately have
   2.243 -    "open (ereal -` (S \<inter> T))"
   2.244 -    "\<infinity> \<in> S \<inter> T \<Longrightarrow> {ereal (max xS xT) <..} \<subseteq> S \<inter> T"
   2.245 -    "-\<infinity> \<in> S \<inter> T \<Longrightarrow> {..< ereal (min yS yT)} \<subseteq> S \<inter> T"
   2.246 -    by auto
   2.247 -  then show "open (S Int T)" unfolding open_ereal_def by blast
   2.248 -next
   2.249 -  fix K :: "ereal set set" assume "\<forall>S\<in>K. open S"
   2.250 -  then have *: "\<forall>S. \<exists>x y. S \<in> K \<longrightarrow> open (ereal -` S) \<and>
   2.251 -    (\<infinity> \<in> S \<longrightarrow> {ereal x <..} \<subseteq> S) \<and> (-\<infinity> \<in> S \<longrightarrow> {..< ereal y} \<subseteq> S)"
   2.252 -    by (auto simp: open_ereal_def)
   2.253 -  then show "open (Union K)" unfolding open_ereal_def
   2.254 -  proof (intro conjI impI)
   2.255 -    show "open (ereal -` \<Union>K)"
   2.256 -      using *[THEN choice] by (auto simp: vimage_Union)
   2.257 -  qed ((metis UnionE Union_upper subset_trans *)+)
   2.258 -qed
   2.259 -end
   2.260 -
   2.261 -lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
   2.262 -  by (auto simp: inj_vimage_image_eq open_ereal_def)
   2.263 -
   2.264 -lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
   2.265 -  unfolding open_ereal_def by auto
   2.266 -
   2.267 -lemma open_ereal_lessThan[intro, simp]: "open {..< a :: ereal}"
   2.268 -proof -
   2.269 -  have "\<And>x. ereal -` {..<ereal x} = {..< x}"
   2.270 -    "ereal -` {..< \<infinity>} = UNIV" "ereal -` {..< -\<infinity>} = {}" by auto
   2.271 -  then show ?thesis by (cases a) (auto simp: open_ereal_def)
   2.272 -qed
   2.273 -
   2.274 -lemma open_ereal_greaterThan[intro, simp]:
   2.275 -  "open {a :: ereal <..}"
   2.276 -proof -
   2.277 -  have "\<And>x. ereal -` {ereal x<..} = {x<..}"
   2.278 -    "ereal -` {\<infinity><..} = {}" "ereal -` {-\<infinity><..} = UNIV" by auto
   2.279 -  then show ?thesis by (cases a) (auto simp: open_ereal_def)
   2.280 -qed
   2.281 -
   2.282 -lemma ereal_open_greaterThanLessThan[intro, simp]: "open {a::ereal <..< b}"
   2.283 -  unfolding greaterThanLessThan_def by auto
   2.284 -
   2.285 -lemma closed_ereal_atLeast[simp, intro]: "closed {a :: ereal ..}"
   2.286 -proof -
   2.287 -  have "- {a ..} = {..< a}" by auto
   2.288 -  then show "closed {a ..}"
   2.289 -    unfolding closed_def using open_ereal_lessThan by auto
   2.290 -qed
   2.291 -
   2.292 -lemma closed_ereal_atMost[simp, intro]: "closed {.. b :: ereal}"
   2.293 -proof -
   2.294 -  have "- {.. b} = {b <..}" by auto
   2.295 -  then show "closed {.. b}"
   2.296 -    unfolding closed_def using open_ereal_greaterThan by auto
   2.297 -qed
   2.298 -
   2.299 -lemma closed_ereal_atLeastAtMost[simp, intro]:
   2.300 -  shows "closed {a :: ereal .. b}"
   2.301 -  unfolding atLeastAtMost_def by auto
   2.302 -
   2.303 -lemma closed_ereal_singleton:
   2.304 -  "closed {a :: ereal}"
   2.305 -by (metis atLeastAtMost_singleton closed_ereal_atLeastAtMost)
   2.306 -
   2.307 +lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
   2.308 +lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
   2.309 +lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
   2.310 +lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
   2.311 +lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
   2.312 +lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
   2.313 +lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
   2.314 +  
   2.315  lemma ereal_open_cont_interval:
   2.316    fixes S :: "ereal set"
   2.317    assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
   2.318 @@ -1928,28 +1964,6 @@
   2.319    show thesis by auto
   2.320  qed
   2.321  
   2.322 -instance ereal :: t2_space
   2.323 -proof
   2.324 -  fix x y :: ereal assume "x ~= y"
   2.325 -  let "?P x (y::ereal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}"
   2.326 -
   2.327 -  { fix x y :: ereal assume "x < y"
   2.328 -    from ereal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
   2.329 -    have "?P x y"
   2.330 -      apply (rule exI[of _ "{..<z}"])
   2.331 -      apply (rule exI[of _ "{z<..}"])
   2.332 -      using z by auto }
   2.333 -  note * = this
   2.334 -
   2.335 -  from `x ~= y`
   2.336 -  show "EX U V. open U & open V & x : U & y : V & U Int V = {}"
   2.337 -  proof (cases rule: linorder_cases)
   2.338 -    assume "x = y" with `x ~= y` show ?thesis by simp
   2.339 -  next assume "x < y" from *[OF this] show ?thesis by auto
   2.340 -  next assume "y < x" from *[OF this] show ?thesis by auto
   2.341 -  qed
   2.342 -qed
   2.343 -
   2.344  subsubsection {* Convergent sequences *}
   2.345  
   2.346  lemma lim_ereal[simp]:
   2.347 @@ -1979,152 +1993,72 @@
   2.348      by (rule eventually_mono)
   2.349  qed
   2.350  
   2.351 -lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= ereal B)" (is "?l = ?r")
   2.352 -proof
   2.353 -  assume ?r
   2.354 -  show ?l
   2.355 -    apply(rule topological_tendstoI)
   2.356 -    unfolding eventually_sequentially
   2.357 -  proof-
   2.358 -    fix S :: "ereal set" assume "open S" "\<infinity> : S"
   2.359 -    from open_PInfty[OF this] guess B .. note B=this
   2.360 -    from `?r`[rule_format,of "B+1"] guess N .. note N=this
   2.361 -    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
   2.362 -    proof safe case goal1
   2.363 -      have "ereal B < ereal (B + 1)" by auto
   2.364 -      also have "... <= f n" using goal1 N by auto
   2.365 -      finally show ?case using B by fastforce
   2.366 -    qed
   2.367 -  qed
   2.368 +lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
   2.369 +  unfolding tendsto_def
   2.370 +proof safe
   2.371 +  fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
   2.372 +  from open_PInfty[OF this] guess B .. note B = this
   2.373 +  moreover
   2.374 +  assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
   2.375 +  then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
   2.376 +  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
   2.377  next
   2.378 -  assume ?l
   2.379 -  show ?r
   2.380 -  proof fix B::real have "open {ereal B<..}" "\<infinity> : {ereal B<..}" by auto
   2.381 -    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
   2.382 -    guess N .. note N=this
   2.383 -    show "EX N. ALL n>=N. ereal B <= f n" apply(rule_tac x=N in exI) using N by auto
   2.384 -  qed
   2.385 +  fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   2.386 +  from this[rule_format, of "{ereal x <..}"]
   2.387 +  show "eventually (\<lambda>y. ereal x < f y) F" by auto
   2.388  qed
   2.389  
   2.390 -
   2.391 -lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= ereal B)" (is "?l = ?r")
   2.392 -proof
   2.393 -  assume ?r
   2.394 -  show ?l
   2.395 -    apply(rule topological_tendstoI)
   2.396 -    unfolding eventually_sequentially
   2.397 -  proof-
   2.398 -    fix S :: "ereal set"
   2.399 -    assume "open S" "(-\<infinity>) : S"
   2.400 -    from open_MInfty[OF this] guess B .. note B=this
   2.401 -    from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
   2.402 -    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
   2.403 -    proof safe case goal1
   2.404 -      have "ereal (B - 1) >= f n" using goal1 N by auto
   2.405 -      also have "... < ereal B" by auto
   2.406 -      finally show ?case using B by fastforce
   2.407 -    qed
   2.408 -  qed
   2.409 -next assume ?l show ?r
   2.410 -  proof fix B::real have "open {..<ereal B}" "(-\<infinity>) : {..<ereal B}" by auto
   2.411 -    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
   2.412 -    guess N .. note N=this
   2.413 -    show "EX N. ALL n>=N. ereal B >= f n" apply(rule_tac x=N in exI) using N by auto
   2.414 -  qed
   2.415 +lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
   2.416 +  unfolding tendsto_def
   2.417 +proof safe
   2.418 +  fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
   2.419 +  from open_MInfty[OF this] guess B .. note B = this
   2.420 +  moreover
   2.421 +  assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
   2.422 +  then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
   2.423 +  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
   2.424 +next
   2.425 +  fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   2.426 +  from this[rule_format, of "{..< ereal x}"]
   2.427 +  show "eventually (\<lambda>y. f y < ereal x) F" by auto
   2.428  qed
   2.429  
   2.430 -
   2.431 -lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= ereal B" shows "l ~= \<infinity>"
   2.432 -proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\<infinity>"
   2.433 -  from lim[unfolded this Lim_PInfty,rule_format,of "?B"]
   2.434 -  guess N .. note N=this[rule_format,OF le_refl]
   2.435 -  hence "ereal ?B <= ereal B" using assms(2)[of N] by(rule order_trans)
   2.436 -  hence "ereal ?B < ereal ?B" apply (rule le_less_trans) by auto
   2.437 -  thus False by auto
   2.438 -qed
   2.439 +lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
   2.440 +  unfolding tendsto_PInfty eventually_sequentially
   2.441 +proof safe
   2.442 +  fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
   2.443 +  from this[rule_format, of "r+1"] guess N ..
   2.444 +  moreover have "ereal r < ereal (r + 1)" by auto
   2.445 +  ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
   2.446 +    by (blast intro: less_le_trans)
   2.447 +qed (blast intro: less_imp_le)
   2.448  
   2.449 +lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
   2.450 +  unfolding tendsto_MInfty eventually_sequentially
   2.451 +proof safe
   2.452 +  fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
   2.453 +  from this[rule_format, of "r - 1"] guess N ..
   2.454 +  moreover have "ereal (r - 1) < ereal r" by auto
   2.455 +  ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
   2.456 +    by (blast intro: le_less_trans)
   2.457 +qed (blast intro: less_imp_le)
   2.458  
   2.459 -lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= ereal B" shows "l ~= (-\<infinity>)"
   2.460 -proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\<infinity>)"
   2.461 -  from lim[unfolded this Lim_MInfty,rule_format,of "?B"]
   2.462 -  guess N .. note N=this[rule_format,OF le_refl]
   2.463 -  hence "ereal B <= ereal ?B" using assms(2)[of N] order_trans[of "ereal B" "f N" "ereal(B - 1)"] by blast
   2.464 -  thus False by auto
   2.465 -qed
   2.466 +lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
   2.467 +  using LIMSEQ_le_const2[of f l "ereal B"] by auto
   2.468  
   2.469 +lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
   2.470 +  using LIMSEQ_le_const[of f l "ereal B"] by auto
   2.471  
   2.472  lemma tendsto_explicit:
   2.473    "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
   2.474    unfolding tendsto_def eventually_sequentially by auto
   2.475  
   2.476 -
   2.477 -lemma tendsto_obtains_N:
   2.478 -  assumes "f ----> f0"
   2.479 -  assumes "open S" "f0 : S"
   2.480 -  obtains N where "ALL n>=N. f n : S"
   2.481 -  using tendsto_explicit[of f f0] assms by auto
   2.482 -
   2.483 -
   2.484 -lemma tail_same_limit:
   2.485 -  fixes X Y N
   2.486 -  assumes "X ----> L" "ALL n>=N. X n = Y n"
   2.487 -  shows "Y ----> L"
   2.488 -proof-
   2.489 -{ fix S assume "open S" and "L:S"
   2.490 -  then obtain N1 where "ALL n>=N1. X n : S"
   2.491 -     using assms unfolding tendsto_def eventually_sequentially by auto
   2.492 -  hence "ALL n>=max N N1. Y n : S" using assms by auto
   2.493 -  hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
   2.494 -}
   2.495 -thus ?thesis using tendsto_explicit by auto
   2.496 -qed
   2.497 -
   2.498 -
   2.499  lemma Lim_bounded_PInfty2:
   2.500 -assumes lim:"f ----> l" and "ALL n>=N. f n <= ereal B"
   2.501 -shows "l ~= \<infinity>"
   2.502 -proof-
   2.503 -  def g == "(%n. if n>=N then f n else ereal B)"
   2.504 -  hence "g ----> l" using tail_same_limit[of f l N g] lim by auto
   2.505 -  moreover have "!!n. g n <= ereal B" using g_def assms by auto
   2.506 -  ultimately show ?thesis using  Lim_bounded_PInfty by auto
   2.507 -qed
   2.508 +  "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
   2.509 +  using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
   2.510  
   2.511 -lemma Lim_bounded_ereal:
   2.512 -  assumes lim:"f ----> (l :: ereal)"
   2.513 -  and "ALL n>=M. f n <= C"
   2.514 -  shows "l<=C"
   2.515 -proof-
   2.516 -{ assume "l=(-\<infinity>)" hence ?thesis by auto }
   2.517 -moreover
   2.518 -{ assume "~(l=(-\<infinity>))"
   2.519 -  { assume "C=\<infinity>" hence ?thesis by auto }
   2.520 -  moreover
   2.521 -  { assume "C=(-\<infinity>)" hence "ALL n>=M. f n = (-\<infinity>)" using assms by auto
   2.522 -    hence "l=(-\<infinity>)" using assms
   2.523 -       tendsto_unique[OF trivial_limit_sequentially] tail_same_limit[of "\<lambda>n. -\<infinity>" "-\<infinity>" M f, OF tendsto_const] by auto
   2.524 -    hence ?thesis by auto }
   2.525 -  moreover
   2.526 -  { assume "EX B. C = ereal B"
   2.527 -    then obtain B where B_def: "C=ereal B" by auto
   2.528 -    hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
   2.529 -    then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
   2.530 -    then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
   2.531 -       apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
   2.532 -    { fix n assume "n>=N"
   2.533 -      hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
   2.534 -    } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
   2.535 -    hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
   2.536 -    hence *: "(%n. g n) ----> m" using m_def by auto
   2.537 -    { fix n assume "n>=max N M"
   2.538 -      hence "ereal (g n) <= ereal B" using assms g_def B_def by auto
   2.539 -      hence "g n <= B" by auto
   2.540 -    } hence "EX N. ALL n>=N. g n <= B" by blast
   2.541 -    hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto
   2.542 -    hence ?thesis using m_def B_def by auto
   2.543 -  } ultimately have ?thesis by (cases C) auto
   2.544 -} ultimately show ?thesis by blast
   2.545 -qed
   2.546 +lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
   2.547 +  by (intro LIMSEQ_le_const2) auto
   2.548  
   2.549  lemma real_of_ereal_mult[simp]:
   2.550    fixes a b :: ereal shows "real (a * b) = real a * real b"
   2.551 @@ -2204,349 +2138,6 @@
   2.552  lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
   2.553    by (cases x) auto
   2.554  
   2.555 -lemma ereal_LimI_finite:
   2.556 -  fixes x :: ereal
   2.557 -  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   2.558 -  assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
   2.559 -  shows "u ----> x"
   2.560 -proof (rule topological_tendstoI, unfold eventually_sequentially)
   2.561 -  obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
   2.562 -  fix S assume "open S" "x : S"
   2.563 -  then have "open (ereal -` S)" unfolding open_ereal_def by auto
   2.564 -  with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
   2.565 -    unfolding open_real_def rx_def by auto
   2.566 -  then obtain n where
   2.567 -    upper: "!!N. n <= N ==> u N < x + ereal r" and
   2.568 -    lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
   2.569 -  show "EX N. ALL n>=N. u n : S"
   2.570 -  proof (safe intro!: exI[of _ n])
   2.571 -    fix N assume "n <= N"
   2.572 -    from upper[OF this] lower[OF this] assms `0 < r`
   2.573 -    have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
   2.574 -    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
   2.575 -    hence "rx < ra + r" and "ra < rx + r"
   2.576 -       using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
   2.577 -    hence "dist (real (u N)) rx < r"
   2.578 -      using rx_def ra_def
   2.579 -      by (auto simp: dist_real_def abs_diff_less_iff field_simps)
   2.580 -    from dist[OF this] show "u N : S" using `u N  ~: {\<infinity>, -\<infinity>}`
   2.581 -      by (auto simp: ereal_real split: split_if_asm)
   2.582 -  qed
   2.583 -qed
   2.584 -
   2.585 -lemma ereal_LimI_finite_iff:
   2.586 -  fixes x :: ereal
   2.587 -  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   2.588 -  shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
   2.589 -  (is "?lhs <-> ?rhs")
   2.590 -proof
   2.591 -  assume lim: "u ----> x"
   2.592 -  { fix r assume "(r::ereal)>0"
   2.593 -    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
   2.594 -       apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
   2.595 -       using lim ereal_between[of x r] assms `r>0` by auto
   2.596 -    hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
   2.597 -      using ereal_minus_less[of r x] by (cases r) auto
   2.598 -  } then show "?rhs" by auto
   2.599 -next
   2.600 -  assume ?rhs then show "u ----> x"
   2.601 -    using ereal_LimI_finite[of x] assms by auto
   2.602 -qed
   2.603 -
   2.604 -
   2.605 -subsubsection {* @{text Liminf} and @{text Limsup} *}
   2.606 -
   2.607 -definition
   2.608 -  "Liminf net f = (GREATEST l. \<forall>y<l. eventually (\<lambda>x. y < f x) net)"
   2.609 -
   2.610 -definition
   2.611 -  "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
   2.612 -
   2.613 -lemma Liminf_Sup:
   2.614 -  fixes f :: "'a => 'b::complete_linorder"
   2.615 -  shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
   2.616 -  by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
   2.617 -
   2.618 -lemma Limsup_Inf:
   2.619 -  fixes f :: "'a => 'b::complete_linorder"
   2.620 -  shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
   2.621 -  by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
   2.622 -
   2.623 -lemma ereal_SupI:
   2.624 -  fixes x :: ereal
   2.625 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   2.626 -  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
   2.627 -  shows "Sup A = x"
   2.628 -  unfolding Sup_ereal_def
   2.629 -  using assms by (auto intro!: Least_equality)
   2.630 -
   2.631 -lemma ereal_InfI:
   2.632 -  fixes x :: ereal
   2.633 -  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
   2.634 -  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
   2.635 -  shows "Inf A = x"
   2.636 -  unfolding Inf_ereal_def
   2.637 -  using assms by (auto intro!: Greatest_equality)
   2.638 -
   2.639 -lemma Limsup_const:
   2.640 -  fixes c :: "'a::complete_linorder"
   2.641 -  assumes ntriv: "\<not> trivial_limit net"
   2.642 -  shows "Limsup net (\<lambda>x. c) = c"
   2.643 -  unfolding Limsup_Inf
   2.644 -proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower)
   2.645 -  fix x assume *: "\<forall>y>x. eventually (\<lambda>_. c < y) net"
   2.646 -  show "c \<le> x"
   2.647 -  proof (rule ccontr)
   2.648 -    assume "\<not> c \<le> x" then have "x < c" by auto
   2.649 -    then show False using ntriv * by (auto simp: trivial_limit_def)
   2.650 -  qed
   2.651 -qed auto
   2.652 -
   2.653 -lemma Liminf_const:
   2.654 -  fixes c :: "'a::complete_linorder"
   2.655 -  assumes ntriv: "\<not> trivial_limit net"
   2.656 -  shows "Liminf net (\<lambda>x. c) = c"
   2.657 -  unfolding Liminf_Sup
   2.658 -proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
   2.659 -  fix x assume *: "\<forall>y<x. eventually (\<lambda>_. y < c) net"
   2.660 -  show "x \<le> c"
   2.661 -  proof (rule ccontr)
   2.662 -    assume "\<not> x \<le> c" then have "c < x" by auto
   2.663 -    then show False using ntriv * by (auto simp: trivial_limit_def)
   2.664 -  qed
   2.665 -qed auto
   2.666 -
   2.667 -definition (in order) mono_set:
   2.668 -  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   2.669 -
   2.670 -lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
   2.671 -lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
   2.672 -lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
   2.673 -lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
   2.674 -
   2.675 -lemma (in complete_linorder) mono_set_iff:
   2.676 -  fixes S :: "'a set"
   2.677 -  defines "a \<equiv> Inf S"
   2.678 -  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
   2.679 -proof
   2.680 -  assume "mono_set S"
   2.681 -  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
   2.682 -  show ?c
   2.683 -  proof cases
   2.684 -    assume "a \<in> S"
   2.685 -    show ?c
   2.686 -      using mono[OF _ `a \<in> S`]
   2.687 -      by (auto intro: Inf_lower simp: a_def)
   2.688 -  next
   2.689 -    assume "a \<notin> S"
   2.690 -    have "S = {a <..}"
   2.691 -    proof safe
   2.692 -      fix x assume "x \<in> S"
   2.693 -      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
   2.694 -      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
   2.695 -    next
   2.696 -      fix x assume "a < x"
   2.697 -      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
   2.698 -      with mono[of y x] show "x \<in> S" by auto
   2.699 -    qed
   2.700 -    then show ?c ..
   2.701 -  qed
   2.702 -qed auto
   2.703 -
   2.704 -lemma lim_imp_Liminf:
   2.705 -  fixes f :: "'a \<Rightarrow> ereal"
   2.706 -  assumes ntriv: "\<not> trivial_limit net"
   2.707 -  assumes lim: "(f ---> f0) net"
   2.708 -  shows "Liminf net f = f0"
   2.709 -  unfolding Liminf_Sup
   2.710 -proof (safe intro!: ereal_SupI)
   2.711 -  fix y assume *: "\<forall>y'<y. eventually (\<lambda>x. y' < f x) net"
   2.712 -  show "y \<le> f0"
   2.713 -  proof (rule ereal_le_ereal)
   2.714 -    fix B assume "B < y"
   2.715 -    { assume "f0 < B"
   2.716 -      then have "eventually (\<lambda>x. f x < B \<and> B < f x) net"
   2.717 -         using topological_tendstoD[OF lim, of "{..<B}"] *[rule_format, OF `B < y`]
   2.718 -         by (auto intro: eventually_conj)
   2.719 -      also have "(\<lambda>x. f x < B \<and> B < f x) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
   2.720 -      finally have False using ntriv[unfolded trivial_limit_def] by auto
   2.721 -    } then show "B \<le> f0" by (metis linorder_le_less_linear)
   2.722 -  qed
   2.723 -next
   2.724 -  fix y assume *: "\<forall>z. z \<in> {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net} \<longrightarrow> z \<le> y"
   2.725 -  show "f0 \<le> y"
   2.726 -  proof (safe intro!: *[rule_format])
   2.727 -    fix y assume "y < f0" then show "eventually (\<lambda>x. y < f x) net"
   2.728 -      using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   2.729 -  qed
   2.730 -qed
   2.731 -
   2.732 -lemma ereal_Liminf_le_Limsup:
   2.733 -  fixes f :: "'a \<Rightarrow> ereal"
   2.734 -  assumes ntriv: "\<not> trivial_limit net"
   2.735 -  shows "Liminf net f \<le> Limsup net f"
   2.736 -  unfolding Limsup_Inf Liminf_Sup
   2.737 -proof (safe intro!: complete_lattice_class.Inf_greatest  complete_lattice_class.Sup_least)
   2.738 -  fix u v assume *: "\<forall>y<u. eventually (\<lambda>x. y < f x) net" "\<forall>y>v. eventually (\<lambda>x. f x < y) net"
   2.739 -  show "u \<le> v"
   2.740 -  proof (rule ccontr)
   2.741 -    assume "\<not> u \<le> v"
   2.742 -    then obtain t where "t < u" "v < t"
   2.743 -      using ereal_dense[of v u] by (auto simp: not_le)
   2.744 -    then have "eventually (\<lambda>x. t < f x \<and> f x < t) net"
   2.745 -      using * by (auto intro: eventually_conj)
   2.746 -    also have "(\<lambda>x. t < f x \<and> f x < t) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
   2.747 -    finally show False using ntriv by (auto simp: trivial_limit_def)
   2.748 -  qed
   2.749 -qed
   2.750 -
   2.751 -lemma Liminf_mono:
   2.752 -  fixes f g :: "'a => ereal"
   2.753 -  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
   2.754 -  shows "Liminf net f \<le> Liminf net g"
   2.755 -  unfolding Liminf_Sup
   2.756 -proof (safe intro!: Sup_mono bexI)
   2.757 -  fix a y assume "\<forall>y<a. eventually (\<lambda>x. y < f x) net" and "y < a"
   2.758 -  then have "eventually (\<lambda>x. y < f x) net" by auto
   2.759 -  then show "eventually (\<lambda>x. y < g x) net"
   2.760 -    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
   2.761 -qed simp
   2.762 -
   2.763 -lemma Liminf_eq:
   2.764 -  fixes f g :: "'a \<Rightarrow> ereal"
   2.765 -  assumes "eventually (\<lambda>x. f x = g x) net"
   2.766 -  shows "Liminf net f = Liminf net g"
   2.767 -  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
   2.768 -
   2.769 -lemma Liminf_mono_all:
   2.770 -  fixes f g :: "'a \<Rightarrow> ereal"
   2.771 -  assumes "\<And>x. f x \<le> g x"
   2.772 -  shows "Liminf net f \<le> Liminf net g"
   2.773 -  using assms by (intro Liminf_mono always_eventually) auto
   2.774 -
   2.775 -lemma Limsup_mono:
   2.776 -  fixes f g :: "'a \<Rightarrow> ereal"
   2.777 -  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
   2.778 -  shows "Limsup net f \<le> Limsup net g"
   2.779 -  unfolding Limsup_Inf
   2.780 -proof (safe intro!: Inf_mono bexI)
   2.781 -  fix a y assume "\<forall>y>a. eventually (\<lambda>x. g x < y) net" and "a < y"
   2.782 -  then have "eventually (\<lambda>x. g x < y) net" by auto
   2.783 -  then show "eventually (\<lambda>x. f x < y) net"
   2.784 -    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
   2.785 -qed simp
   2.786 -
   2.787 -lemma Limsup_mono_all:
   2.788 -  fixes f g :: "'a \<Rightarrow> ereal"
   2.789 -  assumes "\<And>x. f x \<le> g x"
   2.790 -  shows "Limsup net f \<le> Limsup net g"
   2.791 -  using assms by (intro Limsup_mono always_eventually) auto
   2.792 -
   2.793 -lemma Limsup_eq:
   2.794 -  fixes f g :: "'a \<Rightarrow> ereal"
   2.795 -  assumes "eventually (\<lambda>x. f x = g x) net"
   2.796 -  shows "Limsup net f = Limsup net g"
   2.797 -  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
   2.798 -
   2.799 -abbreviation "liminf \<equiv> Liminf sequentially"
   2.800 -
   2.801 -abbreviation "limsup \<equiv> Limsup sequentially"
   2.802 -
   2.803 -lemma liminf_SUPR_INFI:
   2.804 -  fixes f :: "nat \<Rightarrow> ereal"
   2.805 -  shows "liminf f = (SUP n. INF m:{n..}. f m)"
   2.806 -  unfolding Liminf_Sup eventually_sequentially
   2.807 -proof (safe intro!: antisym complete_lattice_class.Sup_least)
   2.808 -  fix x assume *: "\<forall>y<x. \<exists>N. \<forall>n\<ge>N. y < f n" show "x \<le> (SUP n. INF m:{n..}. f m)"
   2.809 -  proof (rule ereal_le_ereal)
   2.810 -    fix y assume "y < x"
   2.811 -    with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
   2.812 -    then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
   2.813 -    also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
   2.814 -    finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
   2.815 -  qed
   2.816 -next
   2.817 -  show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
   2.818 -  proof (unfold SUP_def, safe intro!: Sup_mono bexI)
   2.819 -    fix y n assume "y < INFI {n..} f"
   2.820 -    from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
   2.821 -  qed (rule order_refl)
   2.822 -qed
   2.823 -
   2.824 -lemma tail_same_limsup:
   2.825 -  fixes X Y :: "nat => ereal"
   2.826 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
   2.827 -  shows "limsup X = limsup Y"
   2.828 -  using Limsup_eq[of X Y sequentially] eventually_sequentially assms by auto
   2.829 -
   2.830 -lemma tail_same_liminf:
   2.831 -  fixes X Y :: "nat => ereal"
   2.832 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
   2.833 -  shows "liminf X = liminf Y"
   2.834 -  using Liminf_eq[of X Y sequentially] eventually_sequentially assms by auto
   2.835 -
   2.836 -lemma liminf_mono:
   2.837 -  fixes X Y :: "nat \<Rightarrow> ereal"
   2.838 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   2.839 -  shows "liminf X \<le> liminf Y"
   2.840 -  using Liminf_mono[of X Y sequentially] eventually_sequentially assms by auto
   2.841 -
   2.842 -lemma limsup_mono:
   2.843 -  fixes X Y :: "nat => ereal"
   2.844 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   2.845 -  shows "limsup X \<le> limsup Y"
   2.846 -  using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
   2.847 -
   2.848 -lemma
   2.849 -  fixes X :: "nat \<Rightarrow> ereal"
   2.850 -  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
   2.851 -    and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
   2.852 -  unfolding incseq_def decseq_def by auto
   2.853 -
   2.854 -lemma liminf_bounded:
   2.855 -  fixes X Y :: "nat \<Rightarrow> ereal"
   2.856 -  assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
   2.857 -  shows "C \<le> liminf X"
   2.858 -  using liminf_mono[of N "\<lambda>n. C" X] assms Liminf_const[of sequentially C] by simp
   2.859 -
   2.860 -lemma limsup_bounded:
   2.861 -  fixes X Y :: "nat => ereal"
   2.862 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= C"
   2.863 -  shows "limsup X \<le> C"
   2.864 -  using limsup_mono[of N X "\<lambda>n. C"] assms Limsup_const[of sequentially C] by simp
   2.865 -
   2.866 -lemma liminf_bounded_iff:
   2.867 -  fixes x :: "nat \<Rightarrow> ereal"
   2.868 -  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
   2.869 -proof safe
   2.870 -  fix B assume "B < C" "C \<le> liminf x"
   2.871 -  then have "B < liminf x" by auto
   2.872 -  then obtain N where "B < (INF m:{N..}. x m)"
   2.873 -    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
   2.874 -  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
   2.875 -next
   2.876 -  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
   2.877 -  { fix B assume "B<C"
   2.878 -    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
   2.879 -    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
   2.880 -    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
   2.881 -    finally have "B \<le> liminf x" .
   2.882 -  } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
   2.883 -qed
   2.884 -
   2.885 -lemma liminf_subseq_mono:
   2.886 -  fixes X :: "nat \<Rightarrow> ereal"
   2.887 -  assumes "subseq r"
   2.888 -  shows "liminf X \<le> liminf (X \<circ> r) "
   2.889 -proof-
   2.890 -  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   2.891 -  proof (safe intro!: INF_mono)
   2.892 -    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   2.893 -      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
   2.894 -  qed
   2.895 -  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
   2.896 -qed
   2.897 -
   2.898  lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
   2.899    using assms by auto
   2.900  
   2.901 @@ -2618,6 +2209,333 @@
   2.902    "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   2.903    by (metis sup_ereal_def sup_least)
   2.904  
   2.905 +
   2.906 +lemma ereal_LimI_finite:
   2.907 +  fixes x :: ereal
   2.908 +  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   2.909 +  assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
   2.910 +  shows "u ----> x"
   2.911 +proof (rule topological_tendstoI, unfold eventually_sequentially)
   2.912 +  obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
   2.913 +  fix S assume "open S" "x : S"
   2.914 +  then have "open (ereal -` S)" unfolding open_ereal_def by auto
   2.915 +  with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
   2.916 +    unfolding open_real_def rx_def by auto
   2.917 +  then obtain n where
   2.918 +    upper: "!!N. n <= N ==> u N < x + ereal r" and
   2.919 +    lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
   2.920 +  show "EX N. ALL n>=N. u n : S"
   2.921 +  proof (safe intro!: exI[of _ n])
   2.922 +    fix N assume "n <= N"
   2.923 +    from upper[OF this] lower[OF this] assms `0 < r`
   2.924 +    have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
   2.925 +    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
   2.926 +    hence "rx < ra + r" and "ra < rx + r"
   2.927 +       using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
   2.928 +    hence "dist (real (u N)) rx < r"
   2.929 +      using rx_def ra_def
   2.930 +      by (auto simp: dist_real_def abs_diff_less_iff field_simps)
   2.931 +    from dist[OF this] show "u N : S" using `u N  ~: {\<infinity>, -\<infinity>}`
   2.932 +      by (auto simp: ereal_real split: split_if_asm)
   2.933 +  qed
   2.934 +qed
   2.935 +
   2.936 +lemma tendsto_obtains_N:
   2.937 +  assumes "f ----> f0"
   2.938 +  assumes "open S" "f0 : S"
   2.939 +  obtains N where "ALL n>=N. f n : S"
   2.940 +  using tendsto_explicit[of f f0] assms by auto
   2.941 +
   2.942 +lemma ereal_LimI_finite_iff:
   2.943 +  fixes x :: ereal
   2.944 +  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   2.945 +  shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
   2.946 +  (is "?lhs <-> ?rhs")
   2.947 +proof
   2.948 +  assume lim: "u ----> x"
   2.949 +  { fix r assume "(r::ereal)>0"
   2.950 +    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
   2.951 +       apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
   2.952 +       using lim ereal_between[of x r] assms `r>0` by auto
   2.953 +    hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
   2.954 +      using ereal_minus_less[of r x] by (cases r) auto
   2.955 +  } then show "?rhs" by auto
   2.956 +next
   2.957 +  assume ?rhs then show "u ----> x"
   2.958 +    using ereal_LimI_finite[of x] assms by auto
   2.959 +qed
   2.960 +
   2.961 +
   2.962 +subsubsection {* @{text Liminf} and @{text Limsup} *}
   2.963 +
   2.964 +definition
   2.965 +  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
   2.966 +
   2.967 +definition
   2.968 +  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
   2.969 +
   2.970 +abbreviation "liminf \<equiv> Liminf sequentially"
   2.971 +
   2.972 +abbreviation "limsup \<equiv> Limsup sequentially"
   2.973 +
   2.974 +lemma Liminf_eqI:
   2.975 +  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
   2.976 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   2.977 +  unfolding Liminf_def by (auto intro!: SUP_eqI)
   2.978 +
   2.979 +lemma Limsup_eqI:
   2.980 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
   2.981 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   2.982 +  unfolding Limsup_def by (auto intro!: INF_eqI)
   2.983 +
   2.984 +lemma liminf_SUPR_INFI:
   2.985 +  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
   2.986 +  shows "liminf f = (SUP n. INF m:{n..}. f m)"
   2.987 +  unfolding Liminf_def eventually_sequentially
   2.988 +  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
   2.989 +
   2.990 +lemma limsup_INFI_SUPR:
   2.991 +  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
   2.992 +  shows "limsup f = (INF n. SUP m:{n..}. f m)"
   2.993 +  unfolding Limsup_def eventually_sequentially
   2.994 +  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
   2.995 +
   2.996 +lemma Limsup_const: 
   2.997 +  assumes ntriv: "\<not> trivial_limit F"
   2.998 +  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
   2.999 +proof -
  2.1000 +  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
  2.1001 +  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
  2.1002 +    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
  2.1003 +  then show ?thesis
  2.1004 +    unfolding Limsup_def using eventually_True
  2.1005 +    by (subst INF_cong[where D="\<lambda>x. c"])
  2.1006 +       (auto intro!: INF_const simp del: eventually_True)
  2.1007 +qed
  2.1008 +
  2.1009 +lemma Liminf_const:
  2.1010 +  assumes ntriv: "\<not> trivial_limit F"
  2.1011 +  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
  2.1012 +proof -
  2.1013 +  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
  2.1014 +  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
  2.1015 +    using ntriv by (intro INF_const) (auto simp: eventually_False *)
  2.1016 +  then show ?thesis
  2.1017 +    unfolding Liminf_def using eventually_True
  2.1018 +    by (subst SUP_cong[where D="\<lambda>x. c"])
  2.1019 +       (auto intro!: SUP_const simp del: eventually_True)
  2.1020 +qed
  2.1021 +
  2.1022 +lemma Liminf_mono:
  2.1023 +  fixes f g :: "'a => 'b :: complete_lattice"
  2.1024 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
  2.1025 +  shows "Liminf F f \<le> Liminf F g"
  2.1026 +  unfolding Liminf_def
  2.1027 +proof (safe intro!: SUP_mono)
  2.1028 +  fix P assume "eventually P F"
  2.1029 +  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
  2.1030 +  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
  2.1031 +    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
  2.1032 +qed
  2.1033 +
  2.1034 +lemma Liminf_eq:
  2.1035 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2.1036 +  assumes "eventually (\<lambda>x. f x = g x) F"
  2.1037 +  shows "Liminf F f = Liminf F g"
  2.1038 +  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
  2.1039 +
  2.1040 +lemma Limsup_mono:
  2.1041 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2.1042 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
  2.1043 +  shows "Limsup F f \<le> Limsup F g"
  2.1044 +  unfolding Limsup_def
  2.1045 +proof (safe intro!: INF_mono)
  2.1046 +  fix P assume "eventually P F"
  2.1047 +  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
  2.1048 +  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
  2.1049 +    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
  2.1050 +qed
  2.1051 +
  2.1052 +lemma Limsup_eq:
  2.1053 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2.1054 +  assumes "eventually (\<lambda>x. f x = g x) net"
  2.1055 +  shows "Limsup net f = Limsup net g"
  2.1056 +  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
  2.1057 +
  2.1058 +lemma Liminf_le_Limsup:
  2.1059 +  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
  2.1060 +  assumes ntriv: "\<not> trivial_limit F"
  2.1061 +  shows "Liminf F f \<le> Limsup F f"
  2.1062 +  unfolding Limsup_def Liminf_def
  2.1063 +  apply (rule complete_lattice_class.SUP_least)
  2.1064 +  apply (rule complete_lattice_class.INF_greatest)
  2.1065 +proof safe
  2.1066 +  fix P Q assume "eventually P F" "eventually Q F"
  2.1067 +  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
  2.1068 +  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
  2.1069 +    using ntriv by (auto simp add: eventually_False)
  2.1070 +  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
  2.1071 +    by (rule INF_mono) auto
  2.1072 +  also have "\<dots> \<le> SUPR (Collect ?C) f"
  2.1073 +    using not_False by (intro INF_le_SUP) auto
  2.1074 +  also have "\<dots> \<le> SUPR (Collect Q) f"
  2.1075 +    by (rule SUP_mono) auto
  2.1076 +  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
  2.1077 +qed
  2.1078 +
  2.1079 +lemma
  2.1080 +  fixes X :: "nat \<Rightarrow> ereal"
  2.1081 +  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
  2.1082 +    and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
  2.1083 +  unfolding incseq_def decseq_def by auto
  2.1084 +
  2.1085 +lemma Liminf_bounded:
  2.1086 +  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
  2.1087 +  assumes ntriv: "\<not> trivial_limit F"
  2.1088 +  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
  2.1089 +  shows "C \<le> Liminf F X"
  2.1090 +  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
  2.1091 +
  2.1092 +lemma Limsup_bounded:
  2.1093 +  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
  2.1094 +  assumes ntriv: "\<not> trivial_limit F"
  2.1095 +  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
  2.1096 +  shows "Limsup F X \<le> C"
  2.1097 +  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
  2.1098 +
  2.1099 +lemma liminf_bounded_iff:
  2.1100 +  fixes x :: "nat \<Rightarrow> ereal"
  2.1101 +  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
  2.1102 +proof safe
  2.1103 +  fix B assume "B < C" "C \<le> liminf x"
  2.1104 +  then have "B < liminf x" by auto
  2.1105 +  then obtain N where "B < (INF m:{N..}. x m)"
  2.1106 +    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
  2.1107 +  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
  2.1108 +next
  2.1109 +  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
  2.1110 +  { fix B assume "B<C"
  2.1111 +    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
  2.1112 +    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
  2.1113 +    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
  2.1114 +    finally have "B \<le> liminf x" .
  2.1115 +  } then show "?lhs"
  2.1116 +    by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
  2.1117 +qed
  2.1118 +
  2.1119 +lemma liminf_subseq_mono:
  2.1120 +  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
  2.1121 +  assumes "subseq r"
  2.1122 +  shows "liminf X \<le> liminf (X \<circ> r) "
  2.1123 +proof-
  2.1124 +  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
  2.1125 +  proof (safe intro!: INF_mono)
  2.1126 +    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
  2.1127 +      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
  2.1128 +  qed
  2.1129 +  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
  2.1130 +qed
  2.1131 +
  2.1132 +lemma limsup_subseq_mono:
  2.1133 +  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
  2.1134 +  assumes "subseq r"
  2.1135 +  shows "limsup (X \<circ> r) \<le> limsup X"
  2.1136 +proof-
  2.1137 +  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
  2.1138 +  proof (safe intro!: SUP_mono)
  2.1139 +    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
  2.1140 +      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
  2.1141 +  qed
  2.1142 +  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
  2.1143 +qed
  2.1144 +
  2.1145 +lemma lim_imp_Liminf:
  2.1146 +  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
  2.1147 +  assumes ntriv: "\<not> trivial_limit F"
  2.1148 +  assumes lim: "(f ---> f0) F"
  2.1149 +  shows "Liminf F f = f0"
  2.1150 +proof (rule Liminf_eqI)
  2.1151 +  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
  2.1152 +  show "f0 \<le> y"
  2.1153 +  proof (rule ereal_le_ereal)
  2.1154 +    fix B
  2.1155 +    assume "B < f0"
  2.1156 +    have "B \<le> INFI {x. B < f x} f"
  2.1157 +      by (rule INF_greatest) simp
  2.1158 +    also have "INFI {x. B < f x} f \<le> y"
  2.1159 +      using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
  2.1160 +    finally show "B \<le> y" .
  2.1161 +  qed
  2.1162 +next
  2.1163 +  fix P assume P: "eventually P F"
  2.1164 +  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
  2.1165 +    by eventually_elim (auto intro!: INF_lower)
  2.1166 +  then show "INFI (Collect P) f \<le> f0"
  2.1167 +    by (rule tendsto_le[OF ntriv lim tendsto_const])
  2.1168 +qed
  2.1169 +
  2.1170 +lemma lim_imp_Limsup:
  2.1171 +  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
  2.1172 +  assumes ntriv: "\<not> trivial_limit F"
  2.1173 +  assumes lim: "(f ---> f0) F"
  2.1174 +  shows "Limsup F f = f0"
  2.1175 +proof (rule Limsup_eqI)
  2.1176 +  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
  2.1177 +  show "y \<le> f0"
  2.1178 +  proof (rule ereal_ge_ereal, safe)
  2.1179 +    fix B
  2.1180 +    assume "f0 < B"
  2.1181 +    have "y \<le> SUPR {x. f x < B} f"
  2.1182 +      using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
  2.1183 +    also have "SUPR {x. f x < B} f \<le> B"
  2.1184 +      by (rule SUP_least) simp
  2.1185 +    finally show "y \<le> B" .
  2.1186 +  qed
  2.1187 +next
  2.1188 +  fix P assume P: "eventually P F"
  2.1189 +  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
  2.1190 +    by eventually_elim (auto intro!: SUP_upper)
  2.1191 +  then show "f0 \<le> SUPR (Collect P) f"
  2.1192 +    by (rule tendsto_le[OF ntriv tendsto_const lim])
  2.1193 +qed
  2.1194 +
  2.1195 +definition (in order) mono_set:
  2.1196 +  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
  2.1197 +
  2.1198 +lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
  2.1199 +lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
  2.1200 +lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
  2.1201 +lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
  2.1202 +
  2.1203 +lemma (in complete_linorder) mono_set_iff:
  2.1204 +  fixes S :: "'a set"
  2.1205 +  defines "a \<equiv> Inf S"
  2.1206 +  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
  2.1207 +proof
  2.1208 +  assume "mono_set S"
  2.1209 +  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
  2.1210 +  show ?c
  2.1211 +  proof cases
  2.1212 +    assume "a \<in> S"
  2.1213 +    show ?c
  2.1214 +      using mono[OF _ `a \<in> S`]
  2.1215 +      by (auto intro: Inf_lower simp: a_def)
  2.1216 +  next
  2.1217 +    assume "a \<notin> S"
  2.1218 +    have "S = {a <..}"
  2.1219 +    proof safe
  2.1220 +      fix x assume "x \<in> S"
  2.1221 +      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
  2.1222 +      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
  2.1223 +    next
  2.1224 +      fix x assume "a < x"
  2.1225 +      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
  2.1226 +      with mono[of y x] show "x \<in> S" by auto
  2.1227 +    qed
  2.1228 +    then show ?c ..
  2.1229 +  qed
  2.1230 +qed auto
  2.1231 +
  2.1232  subsubsection {* Tests for code generator *}
  2.1233  
  2.1234  (* A small list of simple arithmetic expressions *)
     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:27 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:30 2013 +0100
     3.3 @@ -288,16 +288,9 @@
     3.4    assumes lim:"f ----> (l :: ereal)"
     3.5      and ge: "ALL n>=N. f n >= C"
     3.6    shows "l>=C"
     3.7 -proof -
     3.8 -  def g == "(%i. -(f i))"
     3.9 -  { fix n
    3.10 -    assume "n>=N"
    3.11 -    then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
    3.12 -  then have "ALL n>=N. g n <= -C" by auto
    3.13 -  moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
    3.14 -  ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
    3.15 -  then show ?thesis using ereal_minus_le_minus by auto
    3.16 -qed
    3.17 +  using ge
    3.18 +  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
    3.19 +     (auto simp: eventually_sequentially)
    3.20  
    3.21  lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
    3.22  proof
    3.23 @@ -326,54 +319,69 @@
    3.24    fixes f :: "'a => ereal"
    3.25    shows "Liminf net f =
    3.26      Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    3.27 -  unfolding Liminf_Sup
    3.28 -proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
    3.29 -  fix l S
    3.30 -  assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
    3.31 -  then have "S = UNIV \<or> S = {Inf S <..}"
    3.32 -    using ereal_open_mono_set[of S] by auto
    3.33 -  then show "eventually (\<lambda>x. f x \<in> S) net"
    3.34 -  proof
    3.35 -    assume S: "S = {Inf S<..}"
    3.36 -    then have "Inf S < l" using `l \<in> S` by auto
    3.37 -    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
    3.38 -    then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
    3.39 -  qed auto
    3.40 +    (is "_ = Sup ?A")
    3.41 +proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
    3.42 +  fix P assume P: "eventually P net"
    3.43 +  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
    3.44 +  { fix x assume "P x"
    3.45 +    then have "INFI (Collect P) f \<le> f x"
    3.46 +      by (intro complete_lattice_class.INF_lower) simp
    3.47 +    with S have "f x \<in> S"
    3.48 +      by (simp add: mono_set) }
    3.49 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
    3.50 +    by (auto elim: eventually_elim1)
    3.51  next
    3.52 -  fix l y
    3.53 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
    3.54 -  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
    3.55 -    using `y < l` by (intro S[rule_format]) auto
    3.56 -  then show "eventually (\<lambda>x. y < f x) net" by auto
    3.57 +  fix y l
    3.58 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
    3.59 +  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
    3.60 +  show "l \<le> y"
    3.61 +  proof (rule ereal_le_ereal)
    3.62 +    fix B assume "B < l"
    3.63 +    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
    3.64 +      by (intro S[rule_format]) auto
    3.65 +    then have "INFI {x. B < f x} f \<le> y"
    3.66 +      using P by auto
    3.67 +    moreover have "B \<le> INFI {x. B < f x} f"
    3.68 +      by (intro INF_greatest) auto
    3.69 +    ultimately show "B \<le> y"
    3.70 +      by simp
    3.71 +  qed
    3.72  qed
    3.73  
    3.74  lemma ereal_Limsup_Inf_monoset:
    3.75    fixes f :: "'a => ereal"
    3.76    shows "Limsup net f =
    3.77      Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    3.78 -  unfolding Limsup_Inf
    3.79 -proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
    3.80 -  fix l S
    3.81 -  assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
    3.82 -  then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
    3.83 -  then have "S = UNIV \<or> S = {..< Sup S}"
    3.84 -    unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
    3.85 -  then show "eventually (\<lambda>x. f x \<in> S) net"
    3.86 -  proof
    3.87 -    assume S: "S = {..< Sup S}"
    3.88 -    then have "l < Sup S" using `l \<in> S` by auto
    3.89 -    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
    3.90 -    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
    3.91 -  qed auto
    3.92 +    (is "_ = Inf ?A")
    3.93 +proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
    3.94 +  fix P assume P: "eventually P net"
    3.95 +  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
    3.96 +  { fix x assume "P x"
    3.97 +    then have "f x \<le> SUPR (Collect P) f"
    3.98 +      by (intro complete_lattice_class.SUP_upper) simp
    3.99 +    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   3.100 +    have "f x \<in> S"
   3.101 +      by (simp add: inj_image_mem_iff) }
   3.102 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
   3.103 +    by (auto elim: eventually_elim1)
   3.104  next
   3.105 -  fix l y
   3.106 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
   3.107 -  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
   3.108 -    using `l < y` by (intro S[rule_format]) auto
   3.109 -  then show "eventually (\<lambda>x. f x < y) net" by auto
   3.110 +  fix y l
   3.111 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   3.112 +  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   3.113 +  show "y \<le> l"
   3.114 +  proof (rule ereal_ge_ereal, safe)
   3.115 +    fix B assume "l < B"
   3.116 +    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   3.117 +      by (intro S[rule_format]) auto
   3.118 +    then have "y \<le> SUPR {x. f x < B} f"
   3.119 +      using P by auto
   3.120 +    moreover have "SUPR {x. f x < B} f \<le> B"
   3.121 +      by (intro SUP_least) auto
   3.122 +    ultimately show "y \<le> B"
   3.123 +      by simp
   3.124 +  qed
   3.125  qed
   3.126  
   3.127 -
   3.128  lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   3.129    using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
   3.130  
   3.131 @@ -434,21 +442,16 @@
   3.132    shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   3.133  proof (intro lim_imp_Liminf iffI assms)
   3.134    assume rhs: "Liminf net f = \<infinity>"
   3.135 -  { fix S :: "ereal set"
   3.136 -    assume "open S & \<infinity> : S"
   3.137 -    then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
   3.138 -    moreover
   3.139 -    have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
   3.140 -      using rhs
   3.141 -      unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
   3.142 -      by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
   3.143 -    ultimately
   3.144 -    have "eventually (%x. f x : S) net"
   3.145 -      apply (subst eventually_mono)
   3.146 -      apply auto
   3.147 -      done
   3.148 -  }
   3.149 -  then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
   3.150 +  show "(f ---> \<infinity>) net"
   3.151 +    unfolding tendsto_PInfty
   3.152 +  proof
   3.153 +    fix r :: real
   3.154 +    have "ereal r < top" unfolding top_ereal_def by simp
   3.155 +    with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
   3.156 +      unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
   3.157 +    then show "eventually (\<lambda>x. ereal r < f x) net"
   3.158 +      by (auto elim!: eventually_elim1 dest: less_INF_D)
   3.159 +  qed
   3.160  qed
   3.161  
   3.162  lemma Limsup_MInfty:
   3.163 @@ -474,12 +477,12 @@
   3.164    show "(f ---> f0) net"
   3.165    proof (rule topological_tendstoI)
   3.166      fix S
   3.167 -    assume "open S""f0 \<in> S"
   3.168 +    assume "open S" "f0 \<in> S"
   3.169      then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
   3.170        using ereal_open_cont_interval2[of S f0] real lim by auto
   3.171      then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
   3.172 -      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
   3.173 -      by (auto intro!: eventually_conj)
   3.174 +      unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
   3.175 +      by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
   3.176      with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
   3.177        by (rule_tac eventually_mono) auto
   3.178    qed
   3.179 @@ -518,7 +521,7 @@
   3.180    assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   3.181      and "X ----> x" "Y ----> y"
   3.182    shows "x <= y"
   3.183 -  by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
   3.184 +  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   3.185  
   3.186  lemma incseq_le_ereal:
   3.187    fixes X :: "nat \<Rightarrow> ereal"
   3.188 @@ -577,114 +580,24 @@
   3.189    by (metis abs_less_iff assms leI le_max_iff_disj
   3.190      less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   3.191  
   3.192 -lemma bounded_increasing_convergent2:
   3.193 -  fixes f::"nat => real"
   3.194 -  assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"
   3.195 -  shows "EX l. (f ---> l) sequentially"
   3.196 -proof -
   3.197 -  def N == "max (abs (f 0)) (abs B)"
   3.198 -  { fix n
   3.199 -    have "abs (f n) <= N"
   3.200 -      unfolding N_def
   3.201 -      apply (subst bounded_abs)
   3.202 -      using assms apply auto
   3.203 -      done }
   3.204 -  then have "bounded {f n| n::nat. True}"
   3.205 -    unfolding bounded_real by auto
   3.206 -  then show ?thesis
   3.207 -    apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)
   3.208 -    using assms apply auto
   3.209 -    done
   3.210 -qed
   3.211 -
   3.212  lemma lim_ereal_increasing:
   3.213 -  assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
   3.214 -  obtains l where "f ----> (l::ereal)"
   3.215 -proof (cases "f = (\<lambda>x. - \<infinity>)")
   3.216 -  case True
   3.217 -  then show thesis
   3.218 -    using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
   3.219 -next
   3.220 -  case False
   3.221 -  then obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
   3.222 -  have "ALL n>=N. f n >= f N" using assms by auto
   3.223 -  then have minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
   3.224 -  def Y == "(%n. (if n>=N then f n else f N))"
   3.225 -  then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
   3.226 -  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
   3.227 -  show thesis
   3.228 -  proof (cases "EX B. ALL n. f n < ereal B")
   3.229 -    case False
   3.230 -    then show thesis
   3.231 -      apply -
   3.232 -      apply (rule that[of \<infinity>])
   3.233 -      unfolding Lim_PInfty not_ex not_all
   3.234 -      apply safe
   3.235 -      apply (erule_tac x=B in allE, safe)
   3.236 -      apply (rule_tac x=x in exI, safe)
   3.237 -      apply (rule order_trans[OF _ assms[rule_format]])
   3.238 -      apply auto
   3.239 -      done
   3.240 -  next
   3.241 -    case True
   3.242 -    then guess B ..
   3.243 -    then have "ALL n. Y n < ereal B" using Y_def by auto
   3.244 -    note B = this[rule_format]
   3.245 -    { fix n
   3.246 -      have "Y n < \<infinity>"
   3.247 -        using B[of n]
   3.248 -        apply (subst less_le_trans)
   3.249 -        apply auto
   3.250 -        done
   3.251 -      then have "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
   3.252 -    }
   3.253 -    then have *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
   3.254 -    { fix n
   3.255 -      have "real (Y n) < B"
   3.256 -      proof -
   3.257 -        case goal1
   3.258 -        then show ?case
   3.259 -          using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
   3.260 -          unfolding ereal_less using * by auto
   3.261 -      qed
   3.262 -    }
   3.263 -    then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
   3.264 -    have "EX l. (%n. real (Y n)) ----> l"
   3.265 -      apply (rule bounded_increasing_convergent2)
   3.266 -    proof safe
   3.267 -      show "\<And>n. real (Y n) <= B" using B' by auto
   3.268 -      fix n m :: nat
   3.269 -      assume "n<=m"
   3.270 -      then have "ereal (real (Y n)) <= ereal (real (Y m))"
   3.271 -        using incy[rule_format,of n m] apply(subst ereal_real)+
   3.272 -        using *[rule_format, of n] *[rule_format, of m] by auto
   3.273 -      then show "real (Y n) <= real (Y m)" by auto
   3.274 -    qed
   3.275 -    then guess l .. note l=this
   3.276 -    have "Y ----> ereal l"
   3.277 -      using l
   3.278 -      apply -
   3.279 -      apply (subst(asm) lim_ereal[THEN sym])
   3.280 -      unfolding ereal_real
   3.281 -      using * apply auto
   3.282 -      done
   3.283 -    then show thesis
   3.284 -      apply -
   3.285 -      apply (rule that[of "ereal l"])
   3.286 -      apply (subst tail_same_limit[of Y _ N])
   3.287 -      using Y_def apply auto
   3.288 -      done
   3.289 -  qed
   3.290 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   3.291 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   3.292 +proof
   3.293 +  show "f ----> (SUP n. f n)"
   3.294 +    using assms
   3.295 +    by (intro increasing_tendsto)
   3.296 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   3.297  qed
   3.298  
   3.299  lemma lim_ereal_decreasing:
   3.300 -  assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
   3.301 -  obtains l where "f ----> (l::ereal)"
   3.302 -proof -
   3.303 -  from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
   3.304 -  obtain l where "(\<lambda>x. - f x) ----> l" by auto
   3.305 -  from ereal_lim_mult[OF this, of "- 1"] show thesis
   3.306 -    by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
   3.307 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   3.308 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   3.309 +proof
   3.310 +  show "f ----> (INF n. f n)"
   3.311 +    using assms
   3.312 +    by (intro decreasing_tendsto)
   3.313 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   3.314  qed
   3.315  
   3.316  lemma compact_ereal:
   3.317 @@ -711,37 +624,17 @@
   3.318    by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   3.319  
   3.320  lemma SUP_Lim_ereal:
   3.321 -  fixes X :: "nat \<Rightarrow> ereal"
   3.322 -  assumes "incseq X" "X ----> l"
   3.323 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   3.324 +  assumes inc: "incseq X" and l: "X ----> l"
   3.325    shows "(SUP n. X n) = l"
   3.326 -proof (rule ereal_SUPI)
   3.327 -  fix n from assms show "X n \<le> l"
   3.328 -    by (intro incseq_le_ereal) (simp add: incseq_def)
   3.329 -next
   3.330 -  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
   3.331 -  with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l \<le> y" by auto
   3.332 -qed
   3.333 -
   3.334 -lemma LIMSEQ_ereal_SUPR:
   3.335 -  fixes X :: "nat \<Rightarrow> ereal"
   3.336 -  assumes "incseq X"
   3.337 -  shows "X ----> (SUP n. X n)"
   3.338 -proof (rule lim_ereal_increasing)
   3.339 -  fix n m :: nat
   3.340 -  assume "m \<le> n"
   3.341 -  then show "X m \<le> X n" using `incseq X` by (simp add: incseq_def)
   3.342 -next
   3.343 -  fix l
   3.344 -  assume "X ----> l"
   3.345 -  with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
   3.346 -qed
   3.347 +  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
   3.348  
   3.349  lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
   3.350    using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
   3.351    by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   3.352  
   3.353  lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
   3.354 -  using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
   3.355 +  using LIMSEQ_SUP[of "\<lambda>i. - X i"]
   3.356    by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   3.357  
   3.358  lemma SUP_eq_LIMSEQ:
   3.359 @@ -755,165 +648,66 @@
   3.360      from SUP_Lim_ereal[OF inc this]
   3.361      show "(SUP n. ereal (f n)) = ereal x" . }
   3.362    { assume "(SUP n. ereal (f n)) = ereal x"
   3.363 -    with LIMSEQ_ereal_SUPR[OF inc]
   3.364 +    with LIMSEQ_SUP[OF inc]
   3.365      show "f ----> x" by auto }
   3.366  qed
   3.367  
   3.368  lemma Liminf_within:
   3.369 -  fixes f :: "'a::metric_space => ereal"
   3.370 -  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
   3.371 -proof -
   3.372 -  let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
   3.373 -  { fix T
   3.374 -    assume T_def: "open T & mono_set T & ?l:T"
   3.375 -    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
   3.376 -    proof -
   3.377 -      { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }
   3.378 -      moreover
   3.379 -      { assume "~(T=UNIV)"
   3.380 -        then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
   3.381 -        then have "B<?l" using T_def by auto
   3.382 -        then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
   3.383 -          unfolding less_SUP_iff by auto
   3.384 -        { fix y assume "y:S & 0 < dist y x & dist y x < d"
   3.385 -          then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
   3.386 -          then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
   3.387 -        } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   3.388 -      }
   3.389 -      ultimately show ?thesis by auto
   3.390 -    qed
   3.391 -  }
   3.392 -  moreover
   3.393 -  { fix z
   3.394 -    assume a: "ALL T. open T --> mono_set T --> z : T -->
   3.395 -       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   3.396 -    { fix B
   3.397 -      assume "B<z"
   3.398 -      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
   3.399 -         using a[rule_format, of "{B<..}"] mono_greaterThan by auto
   3.400 -      { fix y
   3.401 -        assume "y:(S Int ball x d - {x})"
   3.402 -        then have "y:S & 0 < dist y x & dist y x < d"
   3.403 -          unfolding ball_def
   3.404 -          apply (simp add: dist_commute)
   3.405 -          apply (metis dist_eq_0_iff less_le zero_le_dist)
   3.406 -          done
   3.407 -        then have "B <= f y" using d_def by auto
   3.408 -      }
   3.409 -      then have "B <= INFI (S Int ball x d - {x}) f"
   3.410 -        apply (subst INF_greatest)
   3.411 -        apply auto
   3.412 -        done
   3.413 -      also have "...<=?l"
   3.414 -        apply (subst SUP_upper)
   3.415 -        using d_def apply auto
   3.416 -        done
   3.417 -      finally have "B<=?l" by auto
   3.418 -    }
   3.419 -    then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
   3.420 -  }
   3.421 -  ultimately show ?thesis
   3.422 -    unfolding ereal_Liminf_Sup_monoset eventually_within
   3.423 -    apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])
   3.424 -    apply auto
   3.425 -    done
   3.426 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   3.427 +  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   3.428 +  unfolding Liminf_def eventually_within
   3.429 +proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
   3.430 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.431 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.432 +    by (auto simp: zero_less_dist_iff dist_commute)
   3.433 +  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
   3.434 +    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   3.435 +next
   3.436 +  fix d :: real assume "0 < d"
   3.437 +  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>
   3.438 +    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   3.439 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.440 +       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   3.441  qed
   3.442  
   3.443  lemma Limsup_within:
   3.444 -  fixes f :: "'a::metric_space => ereal"
   3.445 -  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   3.446 -proof -
   3.447 -  let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   3.448 -  { fix T
   3.449 -    assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
   3.450 -    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
   3.451 -    proof -
   3.452 -      { assume "T = UNIV"
   3.453 -        then have ?thesis by (simp add: gt_ex) }
   3.454 -      moreover
   3.455 -      { assume "T \<noteq> UNIV"
   3.456 -        then have "~(uminus ` T = UNIV)"
   3.457 -          by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
   3.458 -        then have "uminus ` T = {Inf (uminus ` T)<..}"
   3.459 -          using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto
   3.460 -        then obtain B where "T={..<B}"
   3.461 -          unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
   3.462 -          unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
   3.463 -        then have "?l<B" using T_def by auto
   3.464 -        then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
   3.465 -          unfolding INF_less_iff by auto
   3.466 -        { fix y
   3.467 -          assume "y:S & 0 < dist y x & dist y x < d"
   3.468 -          then have "y:(S Int ball x d - {x})"
   3.469 -            unfolding ball_def by (auto simp add: dist_commute)
   3.470 -          then have "f y:T"
   3.471 -            using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
   3.472 -        }
   3.473 -        then have ?thesis
   3.474 -          apply (rule_tac x="d" in exI)
   3.475 -          using d_def apply auto
   3.476 -          done
   3.477 -      }
   3.478 -      ultimately show ?thesis by auto
   3.479 -    qed
   3.480 -  }
   3.481 -  moreover
   3.482 -  { fix z
   3.483 -    assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
   3.484 -       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   3.485 -    { fix B
   3.486 -      assume "z<B"
   3.487 -      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
   3.488 -         using a[rule_format, of "{..<B}"] by auto
   3.489 -      { fix y
   3.490 -        assume "y:(S Int ball x d - {x})"
   3.491 -        then have "y:S & 0 < dist y x & dist y x < d"
   3.492 -          unfolding ball_def
   3.493 -          apply (simp add: dist_commute)
   3.494 -          apply (metis dist_eq_0_iff less_le zero_le_dist)
   3.495 -          done
   3.496 -        then have "f y <= B" using d_def by auto
   3.497 -      }
   3.498 -      then have "SUPR (S Int ball x d - {x}) f <= B"
   3.499 -        apply (subst SUP_least)
   3.500 -        apply auto
   3.501 -        done
   3.502 -      moreover
   3.503 -      have "?l<=SUPR (S Int ball x d - {x}) f"
   3.504 -        apply (subst INF_lower)
   3.505 -        using d_def apply auto
   3.506 -        done
   3.507 -      ultimately have "?l<=B" by auto
   3.508 -    } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
   3.509 -  }
   3.510 -  ultimately show ?thesis
   3.511 -    unfolding ereal_Limsup_Inf_monoset eventually_within
   3.512 -    apply (subst ereal_InfI)
   3.513 -    apply auto
   3.514 -    done
   3.515 +  fixes f :: "'a::metric_space => 'b::complete_lattice"
   3.516 +  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   3.517 +  unfolding Limsup_def eventually_within
   3.518 +proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
   3.519 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.520 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.521 +    by (auto simp: zero_less_dist_iff dist_commute)
   3.522 +  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   3.523 +    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   3.524 +next
   3.525 +  fix d :: real assume "0 < d"
   3.526 +  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>
   3.527 +    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   3.528 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.529 +       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   3.530  qed
   3.531  
   3.532 -
   3.533  lemma Liminf_within_UNIV:
   3.534 -  fixes f :: "'a::metric_space => ereal"
   3.535 +  fixes f :: "'a::metric_space => _"
   3.536    shows "Liminf (at x) f = Liminf (at x within UNIV) f"
   3.537    by simp (* TODO: delete *)
   3.538  
   3.539  
   3.540  lemma Liminf_at:
   3.541 -  fixes f :: "'a::metric_space => ereal"
   3.542 +  fixes f :: "'a::metric_space => _"
   3.543    shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   3.544    using Liminf_within[of x UNIV f] by simp
   3.545  
   3.546  
   3.547  lemma Limsup_within_UNIV:
   3.548 -  fixes f :: "'a::metric_space => ereal"
   3.549 +  fixes f :: "'a::metric_space => _"
   3.550    shows "Limsup (at x) f = Limsup (at x within UNIV) f"
   3.551    by simp (* TODO: delete *)
   3.552  
   3.553  
   3.554  lemma Limsup_at:
   3.555 -  fixes f :: "'a::metric_space => ereal"
   3.556 +  fixes f :: "'a::metric_space => _"
   3.557    shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   3.558    using Limsup_within[of x UNIV f] by simp
   3.559  
   3.560 @@ -1295,7 +1089,7 @@
   3.561  proof -
   3.562    have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
   3.563      using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
   3.564 -  from LIMSEQ_ereal_SUPR[OF this]
   3.565 +  from LIMSEQ_SUP[OF this]
   3.566    show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
   3.567  qed
   3.568  
     4.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:27 2013 +0100
     4.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:30 2013 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4  *)
     4.5  
     4.6  theory Discrete_Topology
     4.7 -imports Multivariate_Analysis
     4.8 +imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
     4.9  begin
    4.10  
    4.11  text {* Copy of discrete types with discrete topology. This space is polish. *}
     5.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:27 2013 +0100
     5.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:30 2013 +0100
     5.3 @@ -297,7 +297,7 @@
     5.4      qed
     5.5    next
     5.6      fix x show "(SUP i. ?g i x) = max 0 (u x)"
     5.7 -    proof (rule ereal_SUPI)
     5.8 +    proof (rule SUP_eqI)
     5.9        fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
    5.10          by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
    5.11                                       mult_nonpos_nonneg mult_nonneg_nonneg)
    5.12 @@ -2147,7 +2147,7 @@
    5.13      assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
    5.14      have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
    5.15      also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
    5.16 -      by (intro limsup_mono positive_integral_positive)
    5.17 +      by (simp add: Limsup_mono  positive_integral_positive)
    5.18      finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
    5.19      have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
    5.20        using u'
    5.21 @@ -2178,11 +2178,11 @@
    5.22    qed
    5.23  
    5.24    have "liminf ?f \<le> limsup ?f"
    5.25 -    by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
    5.26 +    by (intro Liminf_le_Limsup trivial_limit_sequentially)
    5.27    moreover
    5.28    { have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
    5.29      also have "\<dots> \<le> liminf ?f"
    5.30 -      by (intro liminf_mono positive_integral_positive)
    5.31 +      by (simp add: Liminf_mono positive_integral_positive)
    5.32      finally have "0 \<le> liminf ?f" . }
    5.33    ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
    5.34      using `limsup ?f = 0` by auto
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 31 11:31:27 2013 +0100
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 31 11:31:30 2013 +0100
     6.3 @@ -698,7 +698,7 @@
     6.4    have "integral\<^isup>P lebesgue f = ereal (integral UNIV f')"
     6.5    proof (rule tendsto_unique[OF trivial_limit_sequentially])
     6.6      have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) ----> (SUP i. integral\<^isup>P lebesgue (u i))"
     6.7 -      unfolding u_eq by (intro LIMSEQ_ereal_SUPR incseq_positive_integral u)
     6.8 +      unfolding u_eq by (intro LIMSEQ_SUP incseq_positive_integral u)
     6.9      also note positive_integral_monotone_convergence_SUP
    6.10        [OF u(2)  borel_measurable_simple_function[OF u(1)] u(5), symmetric]
    6.11      finally show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) ----> integral\<^isup>P lebesgue f"
     7.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:27 2013 +0100
     7.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:30 2013 +0100
     7.3 @@ -50,7 +50,7 @@
     7.4    then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
     7.5      by (auto simp: setsum_cases)
     7.6    moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
     7.7 -  proof (rule ereal_SUPI)
     7.8 +  proof (rule SUP_eqI)
     7.9      fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
    7.10      from this[of "Suc i"] show "f i \<le> y" by auto
    7.11    qed (insert assms, simp)
    7.12 @@ -523,7 +523,7 @@
    7.13  lemma SUP_emeasure_incseq:
    7.14    assumes A: "range A \<subseteq> sets M" "incseq A"
    7.15    shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
    7.16 -  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
    7.17 +  using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
    7.18    by (simp add: LIMSEQ_unique)
    7.19  
    7.20  lemma decseq_emeasure:
    7.21 @@ -1570,7 +1570,7 @@
    7.22        have "incseq (\<lambda>i. ?M (F i))"
    7.23          using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
    7.24        then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
    7.25 -        by (rule LIMSEQ_ereal_SUPR)
    7.26 +        by (rule LIMSEQ_SUP)
    7.27  
    7.28        moreover have "(SUP n. ?M (F n)) = \<infinity>"
    7.29        proof (rule SUP_PInfty)
     8.1 --- a/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:27 2013 +0100
     8.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:30 2013 +0100
     8.3 @@ -16,7 +16,7 @@
     8.4    assumes f_nonneg: "\<And>i. 0 \<le> f i"
     8.5    assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
     8.6    shows "x = (SUP i : A. f i)"
     8.7 -proof (subst eq_commute, rule ereal_SUPI)
     8.8 +proof (subst eq_commute, rule SUP_eqI)
     8.9    show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
    8.10  next
    8.11    fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
    8.12 @@ -45,7 +45,7 @@
    8.13    assumes f_nonneg: "\<And>i. 0 \<le> f i"
    8.14    assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
    8.15    shows "x = (INF i : A. f i)"
    8.16 -proof (subst eq_commute, rule ereal_INFI)
    8.17 +proof (subst eq_commute, rule INF_eqI)
    8.18    show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
    8.19  next
    8.20    fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
    8.21 @@ -79,7 +79,7 @@
    8.22    from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
    8.23    ultimately
    8.24    have "(INF i : A. f i) = x + e" using `e > 0`
    8.25 -    by (intro ereal_INFI)
    8.26 +    by (intro INF_eqI)
    8.27        (force, metis add.comm_neutral add_left_mono ereal_less(1)
    8.28          linorder_not_le not_less_iff_gr_or_eq)
    8.29    thus False using assms by auto
    8.30 @@ -97,7 +97,7 @@
    8.31    from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
    8.32    ultimately
    8.33    have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
    8.34 -    by (intro ereal_SUPI)
    8.35 +    by (intro SUP_eqI)
    8.36         (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
    8.37          metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
    8.38    thus False using assms by auto
    8.39 @@ -290,7 +290,7 @@
    8.40        have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
    8.41          by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
    8.42        ultimately show ?thesis by simp
    8.43 -    qed (auto intro!: ereal_INFI)
    8.44 +    qed (auto intro!: INF_eqI)
    8.45      note `?inner A` `?outer A` }
    8.46    note closed_in_D = this
    8.47    from `B \<in> sets borel`
    8.48 @@ -299,8 +299,8 @@
    8.49    then show "?inner B" "?outer B"
    8.50    proof (induct B rule: sigma_sets_induct_disjoint)
    8.51      case empty
    8.52 -    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
    8.53 -    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
    8.54 +    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
    8.55 +    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
    8.56    next
    8.57      case (basic B)
    8.58      { case 1 from basic closed_in_D show ?case by auto }