src/HOL/Library/Extended_Real.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 51022 78de6c7e8a58
child 51301 6822aa82aafa
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
     1 (*  Title:      HOL/Library/Extended_Real.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Robert Himmelmann, TU München
     4     Author:     Armin Heller, TU München
     5     Author:     Bogdan Grechuk, University of Edinburgh
     6 *)
     7 
     8 header {* Extended real number line *}
     9 
    10 theory Extended_Real
    11 imports "~~/src/HOL/Complex_Main" Extended_Nat
    12 begin
    13 
    14 text {*
    15 
    16 For more lemmas about the extended real numbers go to
    17   @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
    18 
    19 *}
    20 
    21 lemma LIMSEQ_SUP:
    22   fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
    23   assumes "incseq X"
    24   shows "X ----> (SUP i. X i)"
    25   using `incseq X`
    26   by (intro increasing_tendsto)
    27      (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
    28 
    29 lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
    30   by (cases P) (simp_all add: eventually_False)
    31 
    32 lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
    33   by (metis Sup_upper2 Inf_lower ex_in_conv)
    34 
    35 lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
    36   unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
    37 
    38 lemma (in complete_linorder) le_Sup_iff:
    39   "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
    40 proof safe
    41   fix y assume "x \<le> Sup A" "y < x"
    42   then have "y < Sup A" by auto
    43   then show "\<exists>a\<in>A. y < a"
    44     unfolding less_Sup_iff .
    45 qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
    46 
    47 lemma (in complete_linorder) le_SUP_iff:
    48   "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
    49   unfolding le_Sup_iff SUP_def by simp
    50 
    51 lemma (in complete_linorder) Inf_le_iff:
    52   "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
    53 proof safe
    54   fix y assume "x \<ge> Inf A" "y > x"
    55   then have "y > Inf A" by auto
    56   then show "\<exists>a\<in>A. y > a"
    57     unfolding Inf_less_iff .
    58 qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
    59 
    60 lemma (in complete_linorder) le_INF_iff:
    61   "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
    62   unfolding Inf_le_iff INF_def by simp
    63 
    64 lemma (in complete_lattice) Sup_eqI:
    65   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
    66   assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
    67   shows "Sup A = x"
    68   by (metis antisym Sup_least Sup_upper assms)
    69 
    70 lemma (in complete_lattice) Inf_eqI:
    71   assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
    72   assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
    73   shows "Inf A = x"
    74   by (metis antisym Inf_greatest Inf_lower assms)
    75 
    76 lemma (in complete_lattice) SUP_eqI:
    77   "(\<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"
    78   unfolding SUP_def by (rule Sup_eqI) auto
    79 
    80 lemma (in complete_lattice) INF_eqI:
    81   "(\<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"
    82   unfolding INF_def by (rule Inf_eqI) auto
    83 
    84 lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
    85 proof
    86   assume "{x..} = UNIV"
    87   show "x = bot"
    88   proof (rule ccontr)
    89     assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less)
    90     then show False using `{x..} = UNIV` by simp
    91   qed
    92 qed auto
    93 
    94 lemma SUPR_pair:
    95   "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    96   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    97 
    98 lemma INFI_pair:
    99   "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   100   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
   101 
   102 subsection {* Definition and basic properties *}
   103 
   104 datatype ereal = ereal real | PInfty | MInfty
   105 
   106 instantiation ereal :: uminus
   107 begin
   108   fun uminus_ereal where
   109     "- (ereal r) = ereal (- r)"
   110   | "- PInfty = MInfty"
   111   | "- MInfty = PInfty"
   112   instance ..
   113 end
   114 
   115 instantiation ereal :: infinity
   116 begin
   117   definition "(\<infinity>::ereal) = PInfty"
   118   instance ..
   119 end
   120 
   121 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
   122 
   123 lemma ereal_uminus_uminus[simp]:
   124   fixes a :: ereal shows "- (- a) = a"
   125   by (cases a) simp_all
   126 
   127 lemma
   128   shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>"
   129     and MInfty_eq_minfinity[simp]: "MInfty = - \<infinity>"
   130     and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "- \<infinity> \<noteq> (\<infinity>::ereal)"
   131     and MInfty_neq_ereal[simp]: "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r"
   132     and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r"
   133     and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = y"
   134     and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
   135   by (simp_all add: infinity_ereal_def)
   136 
   137 declare
   138   PInfty_eq_infinity[code_post]
   139   MInfty_eq_minfinity[code_post]
   140 
   141 lemma [code_unfold]:
   142   "\<infinity> = PInfty"
   143   "-PInfty = MInfty"
   144   by simp_all
   145 
   146 lemma inj_ereal[simp]: "inj_on ereal A"
   147   unfolding inj_on_def by auto
   148 
   149 lemma ereal_cases[case_names real PInf MInf, cases type: ereal]:
   150   assumes "\<And>r. x = ereal r \<Longrightarrow> P"
   151   assumes "x = \<infinity> \<Longrightarrow> P"
   152   assumes "x = -\<infinity> \<Longrightarrow> P"
   153   shows P
   154   using assms by (cases x) auto
   155 
   156 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
   157 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
   158 
   159 lemma ereal_uminus_eq_iff[simp]:
   160   fixes a b :: ereal shows "-a = -b \<longleftrightarrow> a = b"
   161   by (cases rule: ereal2_cases[of a b]) simp_all
   162 
   163 function of_ereal :: "ereal \<Rightarrow> real" where
   164 "of_ereal (ereal r) = r" |
   165 "of_ereal \<infinity> = 0" |
   166 "of_ereal (-\<infinity>) = 0"
   167   by (auto intro: ereal_cases)
   168 termination proof qed (rule wf_empty)
   169 
   170 defs (overloaded)
   171   real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"
   172 
   173 lemma real_of_ereal[simp]:
   174     "real (- x :: ereal) = - (real x)"
   175     "real (ereal r) = r"
   176     "real (\<infinity>::ereal) = 0"
   177   by (cases x) (simp_all add: real_of_ereal_def)
   178 
   179 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
   180 proof safe
   181   fix x assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
   182   then show "x = -\<infinity>" by (cases x) auto
   183 qed auto
   184 
   185 lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"
   186 proof safe
   187   fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
   188 qed auto
   189 
   190 instantiation ereal :: abs
   191 begin
   192   function abs_ereal where
   193     "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
   194   | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
   195   | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
   196   by (auto intro: ereal_cases)
   197   termination proof qed (rule wf_empty)
   198   instance ..
   199 end
   200 
   201 lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   202   by (cases x) auto
   203 
   204 lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   205   by (cases x) auto
   206 
   207 lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
   208   by (cases x) auto
   209 
   210 lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
   211   by auto
   212 
   213 subsubsection "Addition"
   214 
   215 instantiation ereal :: comm_monoid_add
   216 begin
   217 
   218 definition "0 = ereal 0"
   219 
   220 function plus_ereal where
   221 "ereal r + ereal p = ereal (r + p)" |
   222 "\<infinity> + a = (\<infinity>::ereal)" |
   223 "a + \<infinity> = (\<infinity>::ereal)" |
   224 "ereal r + -\<infinity> = - \<infinity>" |
   225 "-\<infinity> + ereal p = -(\<infinity>::ereal)" |
   226 "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
   227 proof -
   228   case (goal1 P x)
   229   moreover then obtain a b where "x = (a, b)" by (cases x) auto
   230   ultimately show P
   231    by (cases rule: ereal2_cases[of a b]) auto
   232 qed auto
   233 termination proof qed (rule wf_empty)
   234 
   235 lemma Infty_neq_0[simp]:
   236   "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
   237   "-(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> -(\<infinity>::ereal)"
   238   by (simp_all add: zero_ereal_def)
   239 
   240 lemma ereal_eq_0[simp]:
   241   "ereal r = 0 \<longleftrightarrow> r = 0"
   242   "0 = ereal r \<longleftrightarrow> r = 0"
   243   unfolding zero_ereal_def by simp_all
   244 
   245 instance
   246 proof
   247   fix a b c :: ereal
   248   show "0 + a = a"
   249     by (cases a) (simp_all add: zero_ereal_def)
   250   show "a + b = b + a"
   251     by (cases rule: ereal2_cases[of a b]) simp_all
   252   show "a + b + c = a + (b + c)"
   253     by (cases rule: ereal3_cases[of a b c]) simp_all
   254 qed
   255 end
   256 
   257 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
   258   unfolding real_of_ereal_def zero_ereal_def by simp
   259 
   260 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)"
   261   unfolding zero_ereal_def abs_ereal.simps by simp
   262 
   263 lemma ereal_uminus_zero[simp]:
   264   "- 0 = (0::ereal)"
   265   by (simp add: zero_ereal_def)
   266 
   267 lemma ereal_uminus_zero_iff[simp]:
   268   fixes a :: ereal shows "-a = 0 \<longleftrightarrow> a = 0"
   269   by (cases a) simp_all
   270 
   271 lemma ereal_plus_eq_PInfty[simp]:
   272   fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
   273   by (cases rule: ereal2_cases[of a b]) auto
   274 
   275 lemma ereal_plus_eq_MInfty[simp]:
   276   fixes a b :: ereal shows "a + b = -\<infinity> \<longleftrightarrow>
   277     (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
   278   by (cases rule: ereal2_cases[of a b]) auto
   279 
   280 lemma ereal_add_cancel_left:
   281   fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
   282   shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   283   using assms by (cases rule: ereal3_cases[of a b c]) auto
   284 
   285 lemma ereal_add_cancel_right:
   286   fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
   287   shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   288   using assms by (cases rule: ereal3_cases[of a b c]) auto
   289 
   290 lemma ereal_real:
   291   "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
   292   by (cases x) simp_all
   293 
   294 lemma real_of_ereal_add:
   295   fixes a b :: ereal
   296   shows "real (a + b) =
   297     (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
   298   by (cases rule: ereal2_cases[of a b]) auto
   299 
   300 subsubsection "Linear order on @{typ ereal}"
   301 
   302 instantiation ereal :: linorder
   303 begin
   304 
   305 function less_ereal
   306 where
   307   "   ereal x < ereal y     \<longleftrightarrow> x < y"
   308 | "(\<infinity>::ereal) < a           \<longleftrightarrow> False"
   309 | "         a < -(\<infinity>::ereal) \<longleftrightarrow> False"
   310 | "ereal x    < \<infinity>           \<longleftrightarrow> True"
   311 | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
   312 | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
   313 proof -
   314   case (goal1 P x)
   315   moreover then obtain a b where "x = (a,b)" by (cases x) auto
   316   ultimately show P by (cases rule: ereal2_cases[of a b]) auto
   317 qed simp_all
   318 termination by (relation "{}") simp
   319 
   320 definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y"
   321 
   322 lemma ereal_infty_less[simp]:
   323   fixes x :: ereal
   324   shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
   325     "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
   326   by (cases x, simp_all) (cases x, simp_all)
   327 
   328 lemma ereal_infty_less_eq[simp]:
   329   fixes x :: ereal
   330   shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
   331   "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
   332   by (auto simp add: less_eq_ereal_def)
   333 
   334 lemma ereal_less[simp]:
   335   "ereal r < 0 \<longleftrightarrow> (r < 0)"
   336   "0 < ereal r \<longleftrightarrow> (0 < r)"
   337   "0 < (\<infinity>::ereal)"
   338   "-(\<infinity>::ereal) < 0"
   339   by (simp_all add: zero_ereal_def)
   340 
   341 lemma ereal_less_eq[simp]:
   342   "x \<le> (\<infinity>::ereal)"
   343   "-(\<infinity>::ereal) \<le> x"
   344   "ereal r \<le> ereal p \<longleftrightarrow> r \<le> p"
   345   "ereal r \<le> 0 \<longleftrightarrow> r \<le> 0"
   346   "0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"
   347   by (auto simp add: less_eq_ereal_def zero_ereal_def)
   348 
   349 lemma ereal_infty_less_eq2:
   350   "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"
   351   "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -(\<infinity>::ereal)"
   352   by simp_all
   353 
   354 instance
   355 proof
   356   fix x y z :: ereal
   357   show "x \<le> x"
   358     by (cases x) simp_all
   359   show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   360     by (cases rule: ereal2_cases[of x y]) auto
   361   show "x \<le> y \<or> y \<le> x "
   362     by (cases rule: ereal2_cases[of x y]) auto
   363   { assume "x \<le> y" "y \<le> x" then show "x = y"
   364     by (cases rule: ereal2_cases[of x y]) auto }
   365   { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
   366     by (cases rule: ereal3_cases[of x y z]) auto }
   367 qed
   368 
   369 end
   370 
   371 instance ereal :: ordered_ab_semigroup_add
   372 proof
   373   fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
   374     by (cases rule: ereal3_cases[of a b c]) auto
   375 qed
   376 
   377 lemma real_of_ereal_positive_mono:
   378   fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
   379   by (cases rule: ereal2_cases[of x y]) auto
   380 
   381 lemma ereal_MInfty_lessI[intro, simp]:
   382   fixes a :: ereal shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   383   by (cases a) auto
   384 
   385 lemma ereal_less_PInfty[intro, simp]:
   386   fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
   387   by (cases a) auto
   388 
   389 lemma ereal_less_ereal_Ex:
   390   fixes a b :: ereal
   391   shows "x < ereal r \<longleftrightarrow> x = -\<infinity> \<or> (\<exists>p. p < r \<and> x = ereal p)"
   392   by (cases x) auto
   393 
   394 lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))"
   395 proof (cases x)
   396   case (real r) then show ?thesis
   397     using reals_Archimedean2[of r] by simp
   398 qed simp_all
   399 
   400 lemma ereal_add_mono:
   401   fixes a b c d :: ereal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d"
   402   using assms
   403   apply (cases a)
   404   apply (cases rule: ereal3_cases[of b c d], auto)
   405   apply (cases rule: ereal3_cases[of b c d], auto)
   406   done
   407 
   408 lemma ereal_minus_le_minus[simp]:
   409   fixes a b :: ereal shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
   410   by (cases rule: ereal2_cases[of a b]) auto
   411 
   412 lemma ereal_minus_less_minus[simp]:
   413   fixes a b :: ereal shows "- a < - b \<longleftrightarrow> b < a"
   414   by (cases rule: ereal2_cases[of a b]) auto
   415 
   416 lemma ereal_le_real_iff:
   417   "x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))"
   418   by (cases y) auto
   419 
   420 lemma real_le_ereal_iff:
   421   "real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))"
   422   by (cases y) auto
   423 
   424 lemma ereal_less_real_iff:
   425   "x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))"
   426   by (cases y) auto
   427 
   428 lemma real_less_ereal_iff:
   429   "real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"
   430   by (cases y) auto
   431 
   432 lemma real_of_ereal_pos:
   433   fixes x :: ereal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
   434 
   435 lemmas real_of_ereal_ord_simps =
   436   ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff
   437 
   438 lemma abs_ereal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: ereal\<bar> = x"
   439   by (cases x) auto
   440 
   441 lemma abs_ereal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: ereal\<bar> = -x"
   442   by (cases x) auto
   443 
   444 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
   445   by (cases x) auto
   446 
   447 lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)"
   448   by (cases x) auto
   449 
   450 lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"
   451   by (cases x) auto
   452 
   453 lemma zero_less_real_of_ereal:
   454   fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)"
   455   by (cases x) auto
   456 
   457 lemma ereal_0_le_uminus_iff[simp]:
   458   fixes a :: ereal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
   459   by (cases rule: ereal2_cases[of a]) auto
   460 
   461 lemma ereal_uminus_le_0_iff[simp]:
   462   fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   463   by (cases rule: ereal2_cases[of a]) auto
   464 
   465 lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
   466   using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
   467 
   468 lemma ereal_dense:
   469   fixes x y :: ereal assumes "x < y"
   470   shows "\<exists>z. x < z \<and> z < y"
   471   using ereal_dense2[OF `x < y`] by blast
   472 
   473 lemma ereal_add_strict_mono:
   474   fixes a b c d :: ereal
   475   assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
   476   shows "a + c < b + d"
   477   using assms by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
   478 
   479 lemma ereal_less_add: 
   480   fixes a b c :: ereal shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
   481   by (cases rule: ereal2_cases[of b c]) auto
   482 
   483 lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)" by auto
   484 
   485 lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
   486   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
   487 
   488 lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
   489   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
   490 
   491 lemmas ereal_uminus_reorder =
   492   ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder
   493 
   494 lemma ereal_bot:
   495   fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"
   496 proof (cases x)
   497   case (real r) with assms[of "r - 1"] show ?thesis by auto
   498 next
   499   case PInf with assms[of 0] show ?thesis by auto
   500 next
   501   case MInf then show ?thesis by simp
   502 qed
   503 
   504 lemma ereal_top:
   505   fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"
   506 proof (cases x)
   507   case (real r) with assms[of "r + 1"] show ?thesis by auto
   508 next
   509   case MInf with assms[of 0] show ?thesis by auto
   510 next
   511   case PInf then show ?thesis by simp
   512 qed
   513 
   514 lemma
   515   shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)"
   516     and ereal_min[simp]: "ereal (min x y) = min (ereal x) (ereal y)"
   517   by (simp_all add: min_def max_def)
   518 
   519 lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)"
   520   by (auto simp: zero_ereal_def)
   521 
   522 lemma
   523   fixes f :: "nat \<Rightarrow> ereal"
   524   shows incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"
   525   and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
   526   unfolding decseq_def incseq_def by auto
   527 
   528 lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"
   529   unfolding incseq_def by auto
   530 
   531 lemma ereal_add_nonneg_nonneg:
   532   fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   533   using add_mono[of 0 a 0 b] by simp
   534 
   535 lemma image_eqD: "f ` A = B \<Longrightarrow> (\<forall>x\<in>A. f x \<in> B)"
   536   by auto
   537 
   538 lemma incseq_setsumI:
   539   fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
   540   assumes "\<And>i. 0 \<le> f i"
   541   shows "incseq (\<lambda>i. setsum f {..< i})"
   542 proof (intro incseq_SucI)
   543   fix n have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
   544     using assms by (rule add_left_mono)
   545   then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
   546     by auto
   547 qed
   548 
   549 lemma incseq_setsumI2:
   550   fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
   551   assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
   552   shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
   553   using assms unfolding incseq_def by (auto intro: setsum_mono)
   554 
   555 subsubsection "Multiplication"
   556 
   557 instantiation ereal :: "{comm_monoid_mult, sgn}"
   558 begin
   559 
   560 definition "1 = ereal 1"
   561 
   562 function sgn_ereal where
   563   "sgn (ereal r) = ereal (sgn r)"
   564 | "sgn (\<infinity>::ereal) = 1"
   565 | "sgn (-\<infinity>::ereal) = -1"
   566 by (auto intro: ereal_cases)
   567 termination proof qed (rule wf_empty)
   568 
   569 function times_ereal where
   570 "ereal r * ereal p = ereal (r * p)" |
   571 "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
   572 "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
   573 "ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
   574 "-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
   575 "(\<infinity>::ereal) * \<infinity> = \<infinity>" |
   576 "-(\<infinity>::ereal) * \<infinity> = -\<infinity>" |
   577 "(\<infinity>::ereal) * -\<infinity> = -\<infinity>" |
   578 "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
   579 proof -
   580   case (goal1 P x)
   581   moreover then obtain a b where "x = (a, b)" by (cases x) auto
   582   ultimately show P by (cases rule: ereal2_cases[of a b]) auto
   583 qed simp_all
   584 termination by (relation "{}") simp
   585 
   586 instance
   587 proof
   588   fix a b c :: ereal show "1 * a = a"
   589     by (cases a) (simp_all add: one_ereal_def)
   590   show "a * b = b * a"
   591     by (cases rule: ereal2_cases[of a b]) simp_all
   592   show "a * b * c = a * (b * c)"
   593     by (cases rule: ereal3_cases[of a b c])
   594        (simp_all add: zero_ereal_def zero_less_mult_iff)
   595 qed
   596 end
   597 
   598 lemma real_ereal_1[simp]: "real (1::ereal) = 1"
   599   unfolding one_ereal_def by simp
   600 
   601 lemma real_of_ereal_le_1:
   602   fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
   603   by (cases a) (auto simp: one_ereal_def)
   604 
   605 lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)"
   606   unfolding one_ereal_def by simp
   607 
   608 lemma ereal_mult_zero[simp]:
   609   fixes a :: ereal shows "a * 0 = 0"
   610   by (cases a) (simp_all add: zero_ereal_def)
   611 
   612 lemma ereal_zero_mult[simp]:
   613   fixes a :: ereal shows "0 * a = 0"
   614   by (cases a) (simp_all add: zero_ereal_def)
   615 
   616 lemma ereal_m1_less_0[simp]:
   617   "-(1::ereal) < 0"
   618   by (simp add: zero_ereal_def one_ereal_def)
   619 
   620 lemma ereal_zero_m1[simp]:
   621   "1 \<noteq> (0::ereal)"
   622   by (simp add: zero_ereal_def one_ereal_def)
   623 
   624 lemma ereal_times_0[simp]:
   625   fixes x :: ereal shows "0 * x = 0"
   626   by (cases x) (auto simp: zero_ereal_def)
   627 
   628 lemma ereal_times[simp]:
   629   "1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"
   630   "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 1"
   631   by (auto simp add: times_ereal_def one_ereal_def)
   632 
   633 lemma ereal_plus_1[simp]:
   634   "1 + ereal r = ereal (r + 1)" "ereal r + 1 = ereal (r + 1)"
   635   "1 + -(\<infinity>::ereal) = -\<infinity>" "-(\<infinity>::ereal) + 1 = -\<infinity>"
   636   unfolding one_ereal_def by auto
   637 
   638 lemma ereal_zero_times[simp]:
   639   fixes a b :: ereal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   640   by (cases rule: ereal2_cases[of a b]) auto
   641 
   642 lemma ereal_mult_eq_PInfty[simp]:
   643   shows "a * b = (\<infinity>::ereal) \<longleftrightarrow>
   644     (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
   645   by (cases rule: ereal2_cases[of a b]) auto
   646 
   647 lemma ereal_mult_eq_MInfty[simp]:
   648   shows "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
   649     (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
   650   by (cases rule: ereal2_cases[of a b]) auto
   651 
   652 lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
   653   by (simp_all add: zero_ereal_def one_ereal_def)
   654 
   655 lemma ereal_zero_one[simp]: "0 \<noteq> (1::ereal)"
   656   by (simp_all add: zero_ereal_def one_ereal_def)
   657 
   658 lemma ereal_mult_minus_left[simp]:
   659   fixes a b :: ereal shows "-a * b = - (a * b)"
   660   by (cases rule: ereal2_cases[of a b]) auto
   661 
   662 lemma ereal_mult_minus_right[simp]:
   663   fixes a b :: ereal shows "a * -b = - (a * b)"
   664   by (cases rule: ereal2_cases[of a b]) auto
   665 
   666 lemma ereal_mult_infty[simp]:
   667   "a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   668   by (cases a) auto
   669 
   670 lemma ereal_infty_mult[simp]:
   671   "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   672   by (cases a) auto
   673 
   674 lemma ereal_mult_strict_right_mono:
   675   assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)"
   676   shows "a * c < b * c"
   677   using assms
   678   by (cases rule: ereal3_cases[of a b c])
   679      (auto simp: zero_le_mult_iff)
   680 
   681 lemma ereal_mult_strict_left_mono:
   682   "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
   683   using ereal_mult_strict_right_mono by (simp add: mult_commute[of c])
   684 
   685 lemma ereal_mult_right_mono:
   686   fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c"
   687   using assms
   688   apply (cases "c = 0") apply simp
   689   by (cases rule: ereal3_cases[of a b c])
   690      (auto simp: zero_le_mult_iff)
   691 
   692 lemma ereal_mult_left_mono:
   693   fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
   694   using ereal_mult_right_mono by (simp add: mult_commute[of c])
   695 
   696 lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"
   697   by (simp add: one_ereal_def zero_ereal_def)
   698 
   699 lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)"
   700   by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)
   701 
   702 lemma ereal_right_distrib:
   703   fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
   704   by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
   705 
   706 lemma ereal_left_distrib:
   707   fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
   708   by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
   709 
   710 lemma ereal_mult_le_0_iff:
   711   fixes a b :: ereal
   712   shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)"
   713   by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff)
   714 
   715 lemma ereal_zero_le_0_iff:
   716   fixes a b :: ereal
   717   shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)"
   718   by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff)
   719 
   720 lemma ereal_mult_less_0_iff:
   721   fixes a b :: ereal
   722   shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)"
   723   by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff)
   724 
   725 lemma ereal_zero_less_0_iff:
   726   fixes a b :: ereal
   727   shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
   728   by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
   729 
   730 lemma ereal_left_mult_cong:
   731   fixes a b c :: ereal
   732   shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
   733   by (cases "c = 0") simp_all
   734 
   735 lemma ereal_right_mult_cong:
   736   fixes a b c :: ereal
   737   shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
   738   by (cases "c = 0") simp_all
   739 
   740 lemma ereal_distrib:
   741   fixes a b c :: ereal
   742   assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
   743   shows "(a + b) * c = a * c + b * c"
   744   using assms
   745   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
   746 
   747 instance ereal :: numeral ..
   748 
   749 lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
   750   apply (induct w rule: num_induct)
   751   apply (simp only: numeral_One one_ereal_def)
   752   apply (simp only: numeral_inc ereal_plus_1)
   753   done
   754 
   755 lemma ereal_le_epsilon:
   756   fixes x y :: ereal
   757   assumes "ALL e. 0 < e --> x <= y + e"
   758   shows "x <= y"
   759 proof-
   760 { assume a: "EX r. y = ereal r"
   761   then obtain r where r_def: "y = ereal r" by auto
   762   { assume "x=(-\<infinity>)" hence ?thesis by auto }
   763   moreover
   764   { assume "~(x=(-\<infinity>))"
   765     then obtain p where p_def: "x = ereal p"
   766     using a assms[rule_format, of 1] by (cases x) auto
   767     { fix e have "0 < e --> p <= r + e"
   768       using assms[rule_format, of "ereal e"] p_def r_def by auto }
   769     hence "p <= r" apply (subst field_le_epsilon) by auto
   770     hence ?thesis using r_def p_def by auto
   771   } ultimately have ?thesis by blast
   772 }
   773 moreover
   774 { assume "y=(-\<infinity>) | y=\<infinity>" hence ?thesis
   775     using assms[rule_format, of 1] by (cases x) auto
   776 } ultimately show ?thesis by (cases y) auto
   777 qed
   778 
   779 
   780 lemma ereal_le_epsilon2:
   781   fixes x y :: ereal
   782   assumes "ALL e. 0 < e --> x <= y + ereal e"
   783   shows "x <= y"
   784 proof-
   785 { fix e :: ereal assume "e>0"
   786   { assume "e=\<infinity>" hence "x<=y+e" by auto }
   787   moreover
   788   { assume "e~=\<infinity>"
   789     then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
   790     hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
   791   } ultimately have "x<=y+e" by blast
   792 } then show ?thesis using ereal_le_epsilon by auto
   793 qed
   794 
   795 lemma ereal_le_real:
   796   fixes x y :: ereal
   797   assumes "ALL z. x <= ereal z --> y <= ereal z"
   798   shows "y <= x"
   799 by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
   800 
   801 lemma ereal_le_ereal:
   802   fixes x y :: ereal
   803   assumes "\<And>B. B < x \<Longrightarrow> B <= y"
   804   shows "x <= y"
   805 by (metis assms ereal_dense leD linorder_le_less_linear)
   806 
   807 lemma ereal_ge_ereal:
   808   fixes x y :: ereal
   809   assumes "ALL B. B>x --> B >= y"
   810   shows "x >= y"
   811 by (metis assms ereal_dense leD linorder_le_less_linear)
   812 
   813 lemma setprod_ereal_0:
   814   fixes f :: "'a \<Rightarrow> ereal"
   815   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
   816 proof cases
   817   assume "finite A"
   818   then show ?thesis by (induct A) auto
   819 qed auto
   820 
   821 lemma setprod_ereal_pos:
   822   fixes f :: "'a \<Rightarrow> ereal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
   823 proof cases
   824   assume "finite I" from this pos show ?thesis by induct auto
   825 qed simp
   826 
   827 lemma setprod_PInf:
   828   fixes f :: "'a \<Rightarrow> ereal"
   829   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   830   shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
   831 proof cases
   832   assume "finite I" from this assms show ?thesis
   833   proof (induct I)
   834     case (insert i I)
   835     then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_ereal_pos)
   836     from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
   837     also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
   838       using setprod_ereal_pos[of I f] pos
   839       by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
   840     also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
   841       using insert by (auto simp: setprod_ereal_0)
   842     finally show ?case .
   843   qed simp
   844 qed simp
   845 
   846 lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
   847 proof cases
   848   assume "finite A" then show ?thesis
   849     by induct (auto simp: one_ereal_def)
   850 qed (simp add: one_ereal_def)
   851 
   852 subsubsection {* Power *}
   853 
   854 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
   855   by (induct n) (auto simp: one_ereal_def)
   856 
   857 lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)"
   858   by (induct n) (auto simp: one_ereal_def)
   859 
   860 lemma ereal_power_uminus[simp]:
   861   fixes x :: ereal
   862   shows "(- x) ^ n = (if even n then x ^ n else - (x^n))"
   863   by (induct n) (auto simp: one_ereal_def)
   864 
   865 lemma ereal_power_numeral[simp]:
   866   "(numeral num :: ereal) ^ n = ereal (numeral num ^ n)"
   867   by (induct n) (auto simp: one_ereal_def)
   868 
   869 lemma zero_le_power_ereal[simp]:
   870   fixes a :: ereal assumes "0 \<le> a"
   871   shows "0 \<le> a ^ n"
   872   using assms by (induct n) (auto simp: ereal_zero_le_0_iff)
   873 
   874 subsubsection {* Subtraction *}
   875 
   876 lemma ereal_minus_minus_image[simp]:
   877   fixes S :: "ereal set"
   878   shows "uminus ` uminus ` S = S"
   879   by (auto simp: image_iff)
   880 
   881 lemma ereal_uminus_lessThan[simp]:
   882   fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
   883 proof -
   884   {
   885     fix x assume "-a < x"
   886     then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
   887     then have "- x < a" by simp
   888   }
   889   then show ?thesis by (auto intro!: image_eqI)
   890 qed
   891 
   892 lemma ereal_uminus_greaterThan[simp]:
   893   "uminus ` {(a::ereal)<..} = {..<-a}"
   894   by (metis ereal_uminus_lessThan ereal_uminus_uminus
   895             ereal_minus_minus_image)
   896 
   897 instantiation ereal :: minus
   898 begin
   899 definition "x - y = x + -(y::ereal)"
   900 instance ..
   901 end
   902 
   903 lemma ereal_minus[simp]:
   904   "ereal r - ereal p = ereal (r - p)"
   905   "-\<infinity> - ereal r = -\<infinity>"
   906   "ereal r - \<infinity> = -\<infinity>"
   907   "(\<infinity>::ereal) - x = \<infinity>"
   908   "-(\<infinity>::ereal) - \<infinity> = -\<infinity>"
   909   "x - -y = x + y"
   910   "x - 0 = x"
   911   "0 - x = -x"
   912   by (simp_all add: minus_ereal_def)
   913 
   914 lemma ereal_x_minus_x[simp]:
   915   "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
   916   by (cases x) simp_all
   917 
   918 lemma ereal_eq_minus_iff:
   919   fixes x y z :: ereal
   920   shows "x = z - y \<longleftrightarrow>
   921     (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and>
   922     (y = -\<infinity> \<longrightarrow> x = \<infinity>) \<and>
   923     (y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and>
   924     (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>)"
   925   by (cases rule: ereal3_cases[of x y z]) auto
   926 
   927 lemma ereal_eq_minus:
   928   fixes x y z :: ereal
   929   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x = z - y \<longleftrightarrow> x + y = z"
   930   by (auto simp: ereal_eq_minus_iff)
   931 
   932 lemma ereal_less_minus_iff:
   933   fixes x y z :: ereal
   934   shows "x < z - y \<longleftrightarrow>
   935     (y = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and>
   936     (y = -\<infinity> \<longrightarrow> x \<noteq> \<infinity>) \<and>
   937     (\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)"
   938   by (cases rule: ereal3_cases[of x y z]) auto
   939 
   940 lemma ereal_less_minus:
   941   fixes x y z :: ereal
   942   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x < z - y \<longleftrightarrow> x + y < z"
   943   by (auto simp: ereal_less_minus_iff)
   944 
   945 lemma ereal_le_minus_iff:
   946   fixes x y z :: ereal
   947   shows "x \<le> z - y \<longleftrightarrow>
   948     (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and>
   949     (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"
   950   by (cases rule: ereal3_cases[of x y z]) auto
   951 
   952 lemma ereal_le_minus:
   953   fixes x y z :: ereal
   954   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x \<le> z - y \<longleftrightarrow> x + y \<le> z"
   955   by (auto simp: ereal_le_minus_iff)
   956 
   957 lemma ereal_minus_less_iff:
   958   fixes x y z :: ereal
   959   shows "x - y < z \<longleftrightarrow>
   960     y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and>
   961     (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
   962   by (cases rule: ereal3_cases[of x y z]) auto
   963 
   964 lemma ereal_minus_less:
   965   fixes x y z :: ereal
   966   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y < z \<longleftrightarrow> x < z + y"
   967   by (auto simp: ereal_minus_less_iff)
   968 
   969 lemma ereal_minus_le_iff:
   970   fixes x y z :: ereal
   971   shows "x - y \<le> z \<longleftrightarrow>
   972     (y = -\<infinity> \<longrightarrow> z = \<infinity>) \<and>
   973     (y = \<infinity> \<longrightarrow> x = \<infinity> \<longrightarrow> z = \<infinity>) \<and>
   974     (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)"
   975   by (cases rule: ereal3_cases[of x y z]) auto
   976 
   977 lemma ereal_minus_le:
   978   fixes x y z :: ereal
   979   shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y \<le> z \<longleftrightarrow> x \<le> z + y"
   980   by (auto simp: ereal_minus_le_iff)
   981 
   982 lemma ereal_minus_eq_minus_iff:
   983   fixes a b c :: ereal
   984   shows "a - b = a - c \<longleftrightarrow>
   985     b = c \<or> a = \<infinity> \<or> (a = -\<infinity> \<and> b \<noteq> -\<infinity> \<and> c \<noteq> -\<infinity>)"
   986   by (cases rule: ereal3_cases[of a b c]) auto
   987 
   988 lemma ereal_add_le_add_iff:
   989   fixes a b c :: ereal
   990   shows "c + a \<le> c + b \<longleftrightarrow>
   991     a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
   992   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
   993 
   994 lemma ereal_mult_le_mult_iff:
   995   fixes a b c :: ereal
   996   shows "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   997   by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)
   998 
   999 lemma ereal_minus_mono:
  1000   fixes A B C D :: ereal assumes "A \<le> B" "D \<le> C"
  1001   shows "A - C \<le> B - D"
  1002   using assms
  1003   by (cases rule: ereal3_cases[case_product ereal_cases, of A B C D]) simp_all
  1004 
  1005 lemma real_of_ereal_minus:
  1006   fixes a b :: ereal
  1007   shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
  1008   by (cases rule: ereal2_cases[of a b]) auto
  1009 
  1010 lemma ereal_diff_positive:
  1011   fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b - a"
  1012   by (cases rule: ereal2_cases[of a b]) auto
  1013 
  1014 lemma ereal_between:
  1015   fixes x e :: ereal
  1016   assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"
  1017   shows "x - e < x" "x < x + e"
  1018 using assms apply (cases x, cases e) apply auto
  1019 using assms apply (cases x, cases e) apply auto
  1020 done
  1021 
  1022 lemma ereal_minus_eq_PInfty_iff:
  1023   fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
  1024   by (cases x y rule: ereal2_cases) simp_all
  1025 
  1026 subsubsection {* Division *}
  1027 
  1028 instantiation ereal :: inverse
  1029 begin
  1030 
  1031 function inverse_ereal where
  1032 "inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" |
  1033 "inverse (\<infinity>::ereal) = 0" |
  1034 "inverse (-\<infinity>::ereal) = 0"
  1035   by (auto intro: ereal_cases)
  1036 termination by (relation "{}") simp
  1037 
  1038 definition "x / y = x * inverse (y :: ereal)"
  1039 
  1040 instance ..
  1041 end
  1042 
  1043 lemma real_of_ereal_inverse[simp]:
  1044   fixes a :: ereal
  1045   shows "real (inverse a) = 1 / real a"
  1046   by (cases a) (auto simp: inverse_eq_divide)
  1047 
  1048 lemma ereal_inverse[simp]:
  1049   "inverse (0::ereal) = \<infinity>"
  1050   "inverse (1::ereal) = 1"
  1051   by (simp_all add: one_ereal_def zero_ereal_def)
  1052 
  1053 lemma ereal_divide[simp]:
  1054   "ereal r / ereal p = (if p = 0 then ereal r * \<infinity> else ereal (r / p))"
  1055   unfolding divide_ereal_def by (auto simp: divide_real_def)
  1056 
  1057 lemma ereal_divide_same[simp]:
  1058   fixes x :: ereal shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
  1059   by (cases x)
  1060      (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
  1061 
  1062 lemma ereal_inv_inv[simp]:
  1063   fixes x :: ereal shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
  1064   by (cases x) auto
  1065 
  1066 lemma ereal_inverse_minus[simp]:
  1067   fixes x :: ereal shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
  1068   by (cases x) simp_all
  1069 
  1070 lemma ereal_uminus_divide[simp]:
  1071   fixes x y :: ereal shows "- x / y = - (x / y)"
  1072   unfolding divide_ereal_def by simp
  1073 
  1074 lemma ereal_divide_Infty[simp]:
  1075   fixes x :: ereal shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
  1076   unfolding divide_ereal_def by simp_all
  1077 
  1078 lemma ereal_divide_one[simp]:
  1079   "x / 1 = (x::ereal)"
  1080   unfolding divide_ereal_def by simp
  1081 
  1082 lemma ereal_divide_ereal[simp]:
  1083   "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
  1084   unfolding divide_ereal_def by simp
  1085 
  1086 lemma zero_le_divide_ereal[simp]:
  1087   fixes a :: ereal assumes "0 \<le> a" "0 \<le> b"
  1088   shows "0 \<le> a / b"
  1089   using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
  1090 
  1091 lemma ereal_le_divide_pos:
  1092   fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
  1093   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1094 
  1095 lemma ereal_divide_le_pos:
  1096   fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
  1097   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1098 
  1099 lemma ereal_le_divide_neg:
  1100   fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
  1101   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1102 
  1103 lemma ereal_divide_le_neg:
  1104   fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
  1105   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  1106 
  1107 lemma ereal_inverse_antimono_strict:
  1108   fixes x y :: ereal
  1109   shows "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> inverse y < inverse x"
  1110   by (cases rule: ereal2_cases[of x y]) auto
  1111 
  1112 lemma ereal_inverse_antimono:
  1113   fixes x y :: ereal
  1114   shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x"
  1115   by (cases rule: ereal2_cases[of x y]) auto
  1116 
  1117 lemma inverse_inverse_Pinfty_iff[simp]:
  1118   fixes x :: ereal shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
  1119   by (cases x) auto
  1120 
  1121 lemma ereal_inverse_eq_0:
  1122   fixes x :: ereal shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
  1123   by (cases x) auto
  1124 
  1125 lemma ereal_0_gt_inverse:
  1126   fixes x :: ereal shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
  1127   by (cases x) auto
  1128 
  1129 lemma ereal_mult_less_right:
  1130   fixes a b c :: ereal
  1131   assumes "b * a < c * a" "0 < a" "a < \<infinity>"
  1132   shows "b < c"
  1133   using assms
  1134   by (cases rule: ereal3_cases[of a b c])
  1135      (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
  1136 
  1137 lemma ereal_power_divide:
  1138   fixes x y :: ereal shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
  1139   by (cases rule: ereal2_cases[of x y])
  1140      (auto simp: one_ereal_def zero_ereal_def power_divide not_le
  1141                  power_less_zero_eq zero_le_power_iff)
  1142 
  1143 lemma ereal_le_mult_one_interval:
  1144   fixes x y :: ereal
  1145   assumes y: "y \<noteq> -\<infinity>"
  1146   assumes z: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
  1147   shows "x \<le> y"
  1148 proof (cases x)
  1149   case PInf with z[of "1 / 2"] show "x \<le> y" by (simp add: one_ereal_def)
  1150 next
  1151   case (real r) note r = this
  1152   show "x \<le> y"
  1153   proof (cases y)
  1154     case (real p) note p = this
  1155     have "r \<le> p"
  1156     proof (rule field_le_mult_one_interval)
  1157       fix z :: real assume "0 < z" and "z < 1"
  1158       with z[of "ereal z"]
  1159       show "z * r \<le> p" using p r by (auto simp: zero_le_mult_iff one_ereal_def)
  1160     qed
  1161     then show "x \<le> y" using p r by simp
  1162   qed (insert y, simp_all)
  1163 qed simp
  1164 
  1165 lemma ereal_divide_right_mono[simp]:
  1166   fixes x y z :: ereal
  1167   assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
  1168 using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
  1169 
  1170 lemma ereal_divide_left_mono[simp]:
  1171   fixes x y z :: ereal
  1172   assumes "y \<le> x" "0 < z" "0 < x * y"
  1173   shows "z / x \<le> z / y"
  1174 using assms by (cases x y z rule: ereal3_cases)
  1175   (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
  1176 
  1177 lemma ereal_divide_zero_left[simp]:
  1178   fixes a :: ereal
  1179   shows "0 / a = 0"
  1180   by (cases a) (auto simp: zero_ereal_def)
  1181 
  1182 lemma ereal_times_divide_eq_left[simp]:
  1183   fixes a b c :: ereal
  1184   shows "b / c * a = b * a / c"
  1185   by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
  1186 
  1187 subsection "Complete lattice"
  1188 
  1189 instantiation ereal :: lattice
  1190 begin
  1191 definition [simp]: "sup x y = (max x y :: ereal)"
  1192 definition [simp]: "inf x y = (min x y :: ereal)"
  1193 instance by default simp_all
  1194 end
  1195 
  1196 instantiation ereal :: complete_lattice
  1197 begin
  1198 
  1199 definition "bot = (-\<infinity>::ereal)"
  1200 definition "top = (\<infinity>::ereal)"
  1201 
  1202 definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)"
  1203 definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)"
  1204 
  1205 lemma ereal_complete_Sup:
  1206   fixes S :: "ereal set" assumes "S \<noteq> {}"
  1207   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
  1208 proof cases
  1209   assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
  1210   then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y" by auto
  1211   then have "\<infinity> \<notin> S" by force
  1212   show ?thesis
  1213   proof cases
  1214     assume "S = {-\<infinity>}"
  1215     then show ?thesis by (auto intro!: exI[of _ "-\<infinity>"])
  1216   next
  1217     assume "S \<noteq> {-\<infinity>}"
  1218     with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
  1219     with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
  1220       by (auto simp: real_of_ereal_ord_simps)
  1221     with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
  1222     obtain s where s:
  1223        "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
  1224        by auto
  1225     show ?thesis
  1226     proof (safe intro!: exI[of _ "ereal s"])
  1227       fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> ereal s"
  1228       proof (cases z)
  1229         case (real r)
  1230         then show ?thesis
  1231           using s(1)[rule_format, of z] `z \<in> S` `z = ereal r` by auto
  1232       qed auto
  1233     next
  1234       fix z assume *: "\<forall>y\<in>S. y \<le> z"
  1235       with `S \<noteq> {-\<infinity>}` `S \<noteq> {}` show "ereal s \<le> z"
  1236       proof (cases z)
  1237         case (real u)
  1238         with * have "s \<le> u"
  1239           by (intro s(2)[of u]) (auto simp: real_of_ereal_ord_simps)
  1240         then show ?thesis using real by simp
  1241       qed auto
  1242     qed
  1243   qed
  1244 next
  1245   assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> ereal x)"
  1246   show ?thesis
  1247   proof (safe intro!: exI[of _ \<infinity>])
  1248     fix y assume **: "\<forall>z\<in>S. z \<le> y"
  1249     with * show "\<infinity> \<le> y"
  1250     proof (cases y)
  1251       case MInf with * ** show ?thesis by (force simp: not_le)
  1252     qed auto
  1253   qed simp
  1254 qed
  1255 
  1256 lemma ereal_complete_Inf:
  1257   fixes S :: "ereal set" assumes "S ~= {}"
  1258   shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)"
  1259 proof-
  1260 def S1 == "uminus ` S"
  1261 hence "S1 ~= {}" using assms by auto
  1262 then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
  1263    using ereal_complete_Sup[of S1] by auto
  1264 { fix z assume "ALL y:S. z <= y"
  1265   hence "ALL y:S1. y <= -z" unfolding S1_def by auto
  1266   hence "x <= -z" using x_def by auto
  1267   hence "z <= -x"
  1268     apply (subst ereal_uminus_uminus[symmetric])
  1269     unfolding ereal_minus_le_minus . }
  1270 moreover have "(ALL y:S. -x <= y)"
  1271    using x_def unfolding S1_def
  1272    apply simp
  1273    apply (subst (3) ereal_uminus_uminus[symmetric])
  1274    unfolding ereal_minus_le_minus by simp
  1275 ultimately show ?thesis by auto
  1276 qed
  1277 
  1278 lemma ereal_complete_uminus_eq:
  1279   fixes S :: "ereal set"
  1280   shows "(\<forall>y\<in>uminus`S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>uminus`S. y \<le> z) \<longrightarrow> x \<le> z)
  1281      \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
  1282   by simp (metis ereal_minus_le_minus ereal_uminus_uminus)
  1283 
  1284 lemma ereal_Sup_uminus_image_eq:
  1285   fixes S :: "ereal set"
  1286   shows "Sup (uminus ` S) = - Inf S"
  1287 proof cases
  1288   assume "S = {}"
  1289   moreover have "(THE x. All (op \<le> x)) = (-\<infinity>::ereal)"
  1290     by (rule the_equality) (auto intro!: ereal_bot)
  1291   moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::ereal)"
  1292     by (rule some_equality) (auto intro!: ereal_top)
  1293   ultimately show ?thesis unfolding Inf_ereal_def Sup_ereal_def
  1294     Least_def Greatest_def GreatestM_def by simp
  1295 next
  1296   assume "S \<noteq> {}"
  1297   with ereal_complete_Sup[of "uminus`S"]
  1298   obtain x where x: "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
  1299     unfolding ereal_complete_uminus_eq by auto
  1300   show "Sup (uminus ` S) = - Inf S"
  1301     unfolding Inf_ereal_def Greatest_def GreatestM_def
  1302   proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) = - x"])
  1303     show "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> -x)"
  1304       using x .
  1305     fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')"
  1306     then have "(\<forall>y\<in>uminus`S. y \<le> - x') \<and> (\<forall>y. (\<forall>z\<in>uminus`S. z \<le> y) \<longrightarrow> - x' \<le> y)"
  1307       unfolding ereal_complete_uminus_eq by simp
  1308     then show "Sup (uminus ` S) = -x'"
  1309       unfolding Sup_ereal_def ereal_uminus_eq_iff
  1310       by (intro Least_equality) auto
  1311   qed
  1312 qed
  1313 
  1314 instance
  1315 proof
  1316   { fix x :: ereal and A
  1317     show "bot <= x" by (cases x) (simp_all add: bot_ereal_def)
  1318     show "x <= top" by (simp add: top_ereal_def) }
  1319 
  1320   { fix x :: ereal and A assume "x : A"
  1321     with ereal_complete_Sup[of A]
  1322     obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
  1323     hence "x <= s" using `x : A` by auto
  1324     also have "... = Sup A" using s unfolding Sup_ereal_def
  1325       by (auto intro!: Least_equality[symmetric])
  1326     finally show "x <= Sup A" . }
  1327   note le_Sup = this
  1328 
  1329   { fix x :: ereal and A assume *: "!!z. (z : A ==> z <= x)"
  1330     show "Sup A <= x"
  1331     proof (cases "A = {}")
  1332       case True
  1333       hence "Sup A = -\<infinity>" unfolding Sup_ereal_def
  1334         by (auto intro!: Least_equality)
  1335       thus "Sup A <= x" by simp
  1336     next
  1337       case False
  1338       with ereal_complete_Sup[of A]
  1339       obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
  1340       hence "Sup A = s"
  1341         unfolding Sup_ereal_def by (auto intro!: Least_equality)
  1342       also have "s <= x" using * s by auto
  1343       finally show "Sup A <= x" .
  1344     qed }
  1345   note Sup_le = this
  1346 
  1347   { fix x :: ereal and A assume "x \<in> A"
  1348     with le_Sup[of "-x" "uminus`A"] show "Inf A \<le> x"
  1349       unfolding ereal_Sup_uminus_image_eq by simp }
  1350 
  1351   { fix x :: ereal and A assume *: "!!z. (z : A ==> x <= z)"
  1352     with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
  1353       unfolding ereal_Sup_uminus_image_eq by force }
  1354 qed
  1355 
  1356 end
  1357 
  1358 instance ereal :: complete_linorder ..
  1359 
  1360 lemma ereal_SUPR_uminus:
  1361   fixes f :: "'a => ereal"
  1362   shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
  1363   unfolding SUP_def INF_def
  1364   using ereal_Sup_uminus_image_eq[of "f`R"]
  1365   by (simp add: image_image)
  1366 
  1367 lemma ereal_INFI_uminus:
  1368   fixes f :: "'a => ereal"
  1369   shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
  1370   using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
  1371 
  1372 lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::ereal set)"
  1373   using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image)
  1374 
  1375 lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
  1376   by (auto intro!: inj_onI)
  1377 
  1378 lemma ereal_image_uminus_shift:
  1379   fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
  1380 proof
  1381   assume "uminus ` X = Y"
  1382   then have "uminus ` uminus ` X = uminus ` Y"
  1383     by (simp add: inj_image_eq_iff)
  1384   then show "X = uminus ` Y" by (simp add: image_image)
  1385 qed (simp add: image_image)
  1386 
  1387 lemma Inf_ereal_iff:
  1388   fixes z :: ereal
  1389   shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x<y) <-> Inf X < y"
  1390   by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear
  1391             order_less_le_trans)
  1392 
  1393 lemma Sup_eq_MInfty:
  1394   fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
  1395 proof
  1396   assume a: "Sup S = -\<infinity>"
  1397   with complete_lattice_class.Sup_upper[of _ S]
  1398   show "S={} \<or> S={-\<infinity>}" by auto
  1399 next
  1400   assume "S={} \<or> S={-\<infinity>}" then show "Sup S = -\<infinity>"
  1401     unfolding Sup_ereal_def by (auto intro!: Least_equality)
  1402 qed
  1403 
  1404 lemma Inf_eq_PInfty:
  1405   fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
  1406   using Sup_eq_MInfty[of "uminus`S"]
  1407   unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp
  1408 
  1409 lemma Inf_eq_MInfty: 
  1410   fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
  1411   unfolding Inf_ereal_def
  1412   by (auto intro!: Greatest_equality)
  1413 
  1414 lemma Sup_eq_PInfty:
  1415   fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
  1416   unfolding Sup_ereal_def
  1417   by (auto intro!: Least_equality)
  1418 
  1419 lemma Sup_ereal_close:
  1420   fixes e :: ereal
  1421   assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
  1422   shows "\<exists>x\<in>S. Sup S - e < x"
  1423   using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1])
  1424 
  1425 lemma Inf_ereal_close:
  1426   fixes e :: ereal assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>" "0 < e"
  1427   shows "\<exists>x\<in>X. x < Inf X + e"
  1428 proof (rule Inf_less_iff[THEN iffD1])
  1429   show "Inf X < Inf X + e" using assms
  1430     by (cases e) auto
  1431 qed
  1432 
  1433 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
  1434 proof -
  1435   { fix x ::ereal assume "x \<noteq> \<infinity>"
  1436     then have "\<exists>k::nat. x < ereal (real k)"
  1437     proof (cases x)
  1438       case MInf then show ?thesis by (intro exI[of _ 0]) auto
  1439     next
  1440       case (real r)
  1441       moreover obtain k :: nat where "r < real k"
  1442         using ex_less_of_nat by (auto simp: real_eq_of_nat)
  1443       ultimately show ?thesis by auto
  1444     qed simp }
  1445   then show ?thesis
  1446     using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
  1447     by (auto simp: top_ereal_def)
  1448 qed
  1449 
  1450 lemma ereal_le_Sup:
  1451   fixes x :: ereal
  1452   shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
  1453 proof-
  1454 { assume "?rhs"
  1455   { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
  1456     then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
  1457     then obtain i where "i : A & y <= f i" using `?rhs` by auto
  1458     hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
  1459     hence False using y_def by auto
  1460   } hence "?lhs" by auto
  1461 }
  1462 moreover
  1463 { assume "?lhs" hence "?rhs"
  1464   by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
  1465 } ultimately show ?thesis by auto
  1466 qed
  1467 
  1468 lemma ereal_Inf_le:
  1469   fixes x :: ereal
  1470   shows "((INF i:A. f i) <= x) <-> (ALL y. x < y --> (EX i. i : A & f i <= y))"
  1471 (is "?lhs <-> ?rhs")
  1472 proof-
  1473 { assume "?rhs"
  1474   { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
  1475     then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
  1476     then obtain i where "i : A & f i <= y" using `?rhs` by auto
  1477     hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
  1478     hence False using y_def by auto
  1479   } hence "?lhs" by auto
  1480 }
  1481 moreover
  1482 { assume "?lhs" hence "?rhs"
  1483   by (metis INF_less_iff order_le_less order_less_le_trans)
  1484 } ultimately show ?thesis by auto
  1485 qed
  1486 
  1487 lemma Inf_less:
  1488   fixes x :: ereal
  1489   assumes "(INF i:A. f i) < x"
  1490   shows "EX i. i : A & f i <= x"
  1491 proof(rule ccontr)
  1492   assume "~ (EX i. i : A & f i <= x)"
  1493   hence "ALL i:A. f i > x" by auto
  1494   hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto
  1495   thus False using assms by auto
  1496 qed
  1497 
  1498 lemma same_INF:
  1499   assumes "ALL e:A. f e = g e"
  1500   shows "(INF e:A. f e) = (INF e:A. g e)"
  1501 proof-
  1502 have "f ` A = g ` A" unfolding image_def using assms by auto
  1503 thus ?thesis unfolding INF_def by auto
  1504 qed
  1505 
  1506 lemma same_SUP:
  1507   assumes "ALL e:A. f e = g e"
  1508   shows "(SUP e:A. f e) = (SUP e:A. g e)"
  1509 proof-
  1510 have "f ` A = g ` A" unfolding image_def using assms by auto
  1511 thus ?thesis unfolding SUP_def by auto
  1512 qed
  1513 
  1514 lemma SUPR_eq:
  1515   assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<le> g j"
  1516   assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<le> f i"
  1517   shows "(SUP i:A. f i) = (SUP j:B. g j)"
  1518 proof (intro antisym)
  1519   show "(SUP i:A. f i) \<le> (SUP j:B. g j)"
  1520     using assms by (metis SUP_least SUP_upper2)
  1521   show "(SUP i:B. g i) \<le> (SUP j:A. f j)"
  1522     using assms by (metis SUP_least SUP_upper2)
  1523 qed
  1524 
  1525 lemma INFI_eq:
  1526   assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
  1527   assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
  1528   shows "(INF i:A. f i) = (INF j:B. g j)"
  1529 proof (intro antisym)
  1530   show "(INF i:A. f i) \<le> (INF j:B. g j)"
  1531     using assms by (metis INF_greatest INF_lower2)
  1532   show "(INF i:B. g i) \<le> (INF j:A. f j)"
  1533     using assms by (metis INF_greatest INF_lower2)
  1534 qed
  1535 
  1536 lemma SUP_ereal_le_addI:
  1537   fixes f :: "'i \<Rightarrow> ereal"
  1538   assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
  1539   shows "SUPR UNIV f + y \<le> z"
  1540 proof (cases y)
  1541   case (real r)
  1542   then have "\<And>i. f i \<le> z - y" using assms by (simp add: ereal_le_minus_iff)
  1543   then have "SUPR UNIV f \<le> z - y" by (rule SUP_least)
  1544   then show ?thesis using real by (simp add: ereal_le_minus_iff)
  1545 qed (insert assms, auto)
  1546 
  1547 lemma SUPR_ereal_add:
  1548   fixes f g :: "nat \<Rightarrow> ereal"
  1549   assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
  1550   shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
  1551 proof (rule SUP_eqI)
  1552   fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
  1553   have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
  1554     unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
  1555   { fix j
  1556     { fix i
  1557       have "f i + g j \<le> f i + g (max i j)"
  1558         using `incseq g`[THEN incseqD] by (rule add_left_mono) auto
  1559       also have "\<dots> \<le> f (max i j) + g (max i j)"
  1560         using `incseq f`[THEN incseqD] by (rule add_right_mono) auto
  1561       also have "\<dots> \<le> y" using * by auto
  1562       finally have "f i + g j \<le> y" . }
  1563     then have "SUPR UNIV f + g j \<le> y"
  1564       using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
  1565     then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps) }
  1566   then have "SUPR UNIV g + SUPR UNIV f \<le> y"
  1567     using f by (rule SUP_ereal_le_addI)
  1568   then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
  1569 qed (auto intro!: add_mono SUP_upper)
  1570 
  1571 lemma SUPR_ereal_add_pos:
  1572   fixes f g :: "nat \<Rightarrow> ereal"
  1573   assumes inc: "incseq f" "incseq g" and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
  1574   shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
  1575 proof (intro SUPR_ereal_add inc)
  1576   fix i show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>" using pos[of i] by auto
  1577 qed
  1578 
  1579 lemma SUPR_ereal_setsum:
  1580   fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
  1581   assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)" and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
  1582   shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPR UNIV (f n))"
  1583 proof cases
  1584   assume "finite A" then show ?thesis using assms
  1585     by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
  1586 qed simp
  1587 
  1588 lemma SUPR_ereal_cmult:
  1589   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
  1590   shows "(SUP i. c * f i) = c * SUPR UNIV f"
  1591 proof (rule SUP_eqI)
  1592   fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
  1593   then show "c * f i \<le> c * SUPR UNIV f"
  1594     using `0 \<le> c` by (rule ereal_mult_left_mono)
  1595 next
  1596   fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
  1597   show "c * SUPR UNIV f \<le> y"
  1598   proof cases
  1599     assume c: "0 < c \<and> c \<noteq> \<infinity>"
  1600     with * have "SUPR UNIV f \<le> y / c"
  1601       by (intro SUP_least) (auto simp: ereal_le_divide_pos)
  1602     with c show ?thesis
  1603       by (auto simp: ereal_le_divide_pos)
  1604   next
  1605     { assume "c = \<infinity>" have ?thesis
  1606       proof cases
  1607         assume "\<forall>i. f i = 0"
  1608         moreover then have "range f = {0}" by auto
  1609         ultimately show "c * SUPR UNIV f \<le> y" using *
  1610           by (auto simp: SUP_def min_max.sup_absorb1)
  1611       next
  1612         assume "\<not> (\<forall>i. f i = 0)"
  1613         then obtain i where "f i \<noteq> 0" by auto
  1614         with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis by (auto split: split_if_asm)
  1615       qed }
  1616     moreover assume "\<not> (0 < c \<and> c \<noteq> \<infinity>)"
  1617     ultimately show ?thesis using * `0 \<le> c` by auto
  1618   qed
  1619 qed
  1620 
  1621 lemma SUP_PInfty:
  1622   fixes f :: "'a \<Rightarrow> ereal"
  1623   assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
  1624   shows "(SUP i:A. f i) = \<infinity>"
  1625   unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
  1626   apply simp
  1627 proof safe
  1628   fix x :: ereal assume "x \<noteq> \<infinity>"
  1629   show "\<exists>i\<in>A. x < f i"
  1630   proof (cases x)
  1631     case PInf with `x \<noteq> \<infinity>` show ?thesis by simp
  1632   next
  1633     case MInf with assms[of "0"] show ?thesis by force
  1634   next
  1635     case (real r)
  1636     with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
  1637     moreover from assms[of n] guess i ..
  1638     ultimately show ?thesis
  1639       by (auto intro!: bexI[of _ i])
  1640   qed
  1641 qed
  1642 
  1643 lemma Sup_countable_SUPR:
  1644   assumes "A \<noteq> {}"
  1645   shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
  1646 proof (cases "Sup A")
  1647   case (real r)
  1648   have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
  1649   proof
  1650     fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
  1651       using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
  1652     then guess x ..
  1653     then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
  1654       by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
  1655   qed
  1656   from choice[OF this] guess f .. note f = this
  1657   have "SUPR UNIV f = Sup A"
  1658   proof (rule SUP_eqI)
  1659     fix i show "f i \<le> Sup A" using f
  1660       by (auto intro!: complete_lattice_class.Sup_upper)
  1661   next
  1662     fix y assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
  1663     show "Sup A \<le> y"
  1664     proof (rule ereal_le_epsilon, intro allI impI)
  1665       fix e :: ereal assume "0 < e"
  1666       show "Sup A \<le> y + e"
  1667       proof (cases e)
  1668         case (real r)
  1669         hence "0 < r" using `0 < e` by auto
  1670         then obtain n ::nat where *: "1 / real n < r" "0 < n"
  1671           using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide)
  1672         have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n]
  1673           by auto
  1674         also have "1 / ereal (real n) \<le> e" using real * by (auto simp: one_ereal_def )
  1675         with bound have "f n + 1 / ereal (real n) \<le> y + e" by (rule add_mono) simp
  1676         finally show "Sup A \<le> y + e" .
  1677       qed (insert `0 < e`, auto)
  1678     qed
  1679   qed
  1680   with f show ?thesis by (auto intro!: exI[of _ f])
  1681 next
  1682   case PInf
  1683   from `A \<noteq> {}` obtain x where "x \<in> A" by auto
  1684   show ?thesis
  1685   proof cases
  1686     assume "\<infinity> \<in> A"
  1687     moreover then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
  1688     ultimately show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
  1689   next
  1690     assume "\<infinity> \<notin> A"
  1691     have "\<exists>x\<in>A. 0 \<le> x"
  1692       by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least ereal_infty_less_eq2 linorder_linear)
  1693     then obtain x where "x \<in> A" "0 \<le> x" by auto
  1694     have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
  1695     proof (rule ccontr)
  1696       assume "\<not> ?thesis"
  1697       then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
  1698         by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
  1699       then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
  1700         by(cases x) auto
  1701     qed
  1702     from choice[OF this] guess f .. note f = this
  1703     have "SUPR UNIV f = \<infinity>"
  1704     proof (rule SUP_PInfty)
  1705       fix n :: nat show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
  1706         using f[THEN spec, of n] `0 \<le> x`
  1707         by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
  1708     qed
  1709     then show ?thesis using f PInf by (auto intro!: exI[of _ f])
  1710   qed
  1711 next
  1712   case MInf
  1713   with `A \<noteq> {}` have "A = {-\<infinity>}" by (auto simp: Sup_eq_MInfty)
  1714   then show ?thesis using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
  1715 qed
  1716 
  1717 lemma SUPR_countable_SUPR:
  1718   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
  1719   using Sup_countable_SUPR[of "g`A"] by (auto simp: SUP_def)
  1720 
  1721 lemma Sup_ereal_cadd:
  1722   fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
  1723   shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
  1724 proof (rule antisym)
  1725   have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
  1726     by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
  1727   then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
  1728   show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
  1729   proof (cases a)
  1730     case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1)
  1731   next
  1732     case (real r)
  1733     then have **: "op + (- a) ` op + a ` A = A"
  1734       by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
  1735     from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis unfolding **
  1736       by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
  1737   qed (insert `a \<noteq> -\<infinity>`, auto)
  1738 qed
  1739 
  1740 lemma Sup_ereal_cminus:
  1741   fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
  1742   shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
  1743   using Sup_ereal_cadd[of "uminus ` A" a] assms
  1744   by (simp add: comp_def image_image minus_ereal_def
  1745                  ereal_Sup_uminus_image_eq)
  1746 
  1747 lemma SUPR_ereal_cminus:
  1748   fixes f :: "'i \<Rightarrow> ereal"
  1749   fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
  1750   shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
  1751   using Sup_ereal_cminus[of "f`A" a] assms
  1752   unfolding SUP_def INF_def image_image by auto
  1753 
  1754 lemma Inf_ereal_cminus:
  1755   fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
  1756   shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
  1757 proof -
  1758   { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto }
  1759   moreover then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
  1760     by (auto simp: image_image)
  1761   ultimately show ?thesis
  1762     using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
  1763     by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
  1764 qed
  1765 
  1766 lemma INFI_ereal_cminus:
  1767   fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
  1768   shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
  1769   using Inf_ereal_cminus[of "f`A" a] assms
  1770   unfolding SUP_def INF_def image_image
  1771   by auto
  1772 
  1773 lemma uminus_ereal_add_uminus_uminus:
  1774   fixes a b :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
  1775   by (cases rule: ereal2_cases[of a b]) auto
  1776 
  1777 lemma INFI_ereal_add:
  1778   fixes f :: "nat \<Rightarrow> ereal"
  1779   assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
  1780   shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
  1781 proof -
  1782   have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
  1783     using assms unfolding INF_less_iff by auto
  1784   { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
  1785       by (rule uminus_ereal_add_uminus_uminus) }
  1786   then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
  1787     by simp
  1788   also have "\<dots> = INFI UNIV f + INFI UNIV g"
  1789     unfolding ereal_INFI_uminus
  1790     using assms INF_less
  1791     by (subst SUPR_ereal_add)
  1792        (auto simp: ereal_SUPR_uminus intro!: uminus_ereal_add_uminus_uminus)
  1793   finally show ?thesis .
  1794 qed
  1795 
  1796 subsection "Relation to @{typ enat}"
  1797 
  1798 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
  1799 
  1800 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
  1801 declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
  1802 
  1803 lemma ereal_of_enat_simps[simp]:
  1804   "ereal_of_enat (enat n) = ereal n"
  1805   "ereal_of_enat \<infinity> = \<infinity>"
  1806   by (simp_all add: ereal_of_enat_def)
  1807 
  1808 lemma ereal_of_enat_le_iff[simp]:
  1809   "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
  1810 by (cases m n rule: enat2_cases) auto
  1811 
  1812 lemma ereal_of_enat_less_iff[simp]:
  1813   "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
  1814 by (cases m n rule: enat2_cases) auto
  1815 
  1816 lemma numeral_le_ereal_of_enat_iff[simp]:
  1817   shows "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
  1818 by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
  1819 
  1820 lemma numeral_less_ereal_of_enat_iff[simp]:
  1821   shows "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
  1822 by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
  1823 
  1824 lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
  1825   "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
  1826 by (cases n) (auto simp: enat_0[symmetric])
  1827 
  1828 lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
  1829   "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
  1830 by (cases n) (auto simp: enat_0[symmetric])
  1831 
  1832 lemma ereal_of_enat_zero[simp]:
  1833   "ereal_of_enat 0 = 0"
  1834 by (auto simp: enat_0[symmetric])
  1835 
  1836 lemma ereal_of_enat_inf[simp]:
  1837   "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
  1838   by (cases n) auto
  1839 
  1840 
  1841 lemma ereal_of_enat_add:
  1842   "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
  1843 by (cases m n rule: enat2_cases) auto
  1844 
  1845 lemma ereal_of_enat_sub:
  1846   assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
  1847 using assms by (cases m n rule: enat2_cases) auto
  1848 
  1849 lemma ereal_of_enat_mult:
  1850   "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
  1851 by (cases m n rule: enat2_cases) auto
  1852 
  1853 lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
  1854 lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
  1855 
  1856 
  1857 subsection "Limits on @{typ ereal}"
  1858 
  1859 subsubsection "Topological space"
  1860 
  1861 instantiation ereal :: linorder_topology
  1862 begin
  1863 
  1864 definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
  1865   open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
  1866 
  1867 instance
  1868   by default (simp add: open_ereal_generated)
  1869 end
  1870 
  1871 lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
  1872   unfolding open_ereal_generated
  1873 proof (induct rule: generate_topology.induct)
  1874   case (Int A B)
  1875   moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
  1876       by auto
  1877   ultimately show ?case
  1878     by (intro exI[of _ "max x z"]) fastforce
  1879 next
  1880   { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
  1881   moreover case (Basis S)
  1882   ultimately show ?case
  1883     by (auto split: ereal.split)
  1884 qed (fastforce simp add: vimage_Union)+
  1885 
  1886 lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
  1887   unfolding open_ereal_generated
  1888 proof (induct rule: generate_topology.induct)
  1889   case (Int A B)
  1890   moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
  1891       by auto
  1892   ultimately show ?case
  1893     by (intro exI[of _ "min x z"]) fastforce
  1894 next
  1895   { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
  1896   moreover case (Basis S)
  1897   ultimately show ?case
  1898     by (auto split: ereal.split)
  1899 qed (fastforce simp add: vimage_Union)+
  1900 
  1901 lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
  1902   unfolding open_ereal_generated
  1903 proof (induct rule: generate_topology.induct)
  1904   case (Int A B) then show ?case by auto
  1905 next
  1906   { fix x have
  1907       "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
  1908       "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
  1909       by (induct x) auto }
  1910   moreover case (Basis S)
  1911   ultimately show ?case
  1912     by (auto split: ereal.split)
  1913 qed (fastforce simp add: vimage_Union)+
  1914 
  1915 lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
  1916   unfolding open_generated_order[where 'a=real]
  1917 proof (induct rule: generate_topology.induct)
  1918   case (Basis S)
  1919   moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
  1920   moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
  1921   ultimately show ?case
  1922      by auto
  1923 qed (auto simp add: image_Union image_Int)
  1924 
  1925 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))"
  1926   (is "open A \<longleftrightarrow> ?rhs")
  1927 proof
  1928   assume "open A" then show ?rhs
  1929     using open_PInfty open_MInfty open_ereal_vimage by auto
  1930 next
  1931   assume "?rhs"
  1932   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"
  1933     by auto
  1934   have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
  1935     using A(2,3) by auto
  1936   from open_ereal[OF A(1)] show "open A"
  1937     by (subst *) (auto simp: open_Un)
  1938 qed
  1939 
  1940 lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
  1941   using open_PInfty[OF assms] by auto
  1942 
  1943 lemma open_MInfty2: assumes "open A" "-\<infinity> \<in> A" obtains x where "{..<ereal x} \<subseteq> A"
  1944   using open_MInfty[OF assms] by auto
  1945 
  1946 lemma ereal_openE: assumes "open A" obtains x y where
  1947   "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
  1948   using assms open_ereal_def by auto
  1949 
  1950 lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
  1951 lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
  1952 lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
  1953 lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
  1954 lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
  1955 lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
  1956 lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
  1957   
  1958 lemma ereal_open_cont_interval:
  1959   fixes S :: "ereal set"
  1960   assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
  1961   obtains e where "e>0" "{x-e <..< x+e} \<subseteq> S"
  1962 proof-
  1963   from `open S` have "open (ereal -` S)" by (rule ereal_openE)
  1964   then obtain e where "0 < e" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
  1965     using assms unfolding open_dist by force
  1966   show thesis
  1967   proof (intro that subsetI)
  1968     show "0 < ereal e" using `0 < e` by auto
  1969     fix y assume "y \<in> {x - ereal e<..<x + ereal e}"
  1970     with assms obtain t where "y = ereal t" "dist t (real x) < e"
  1971       apply (cases y) by (auto simp: dist_real_def)
  1972     then show "y \<in> S" using e[of t] by auto
  1973   qed
  1974 qed
  1975 
  1976 lemma ereal_open_cont_interval2:
  1977   fixes S :: "ereal set"
  1978   assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
  1979   obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
  1980 proof-
  1981   guess e using ereal_open_cont_interval[OF assms] .
  1982   with that[of "x-e" "x+e"] ereal_between[OF x, of e]
  1983   show thesis by auto
  1984 qed
  1985 
  1986 subsubsection {* Convergent sequences *}
  1987 
  1988 lemma lim_ereal[simp]:
  1989   "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net" (is "?l = ?r")
  1990 proof (intro iffI topological_tendstoI)
  1991   fix S assume "?l" "open S" "x \<in> S"
  1992   then show "eventually (\<lambda>x. f x \<in> S) net"
  1993     using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
  1994     by (simp add: inj_image_mem_iff)
  1995 next
  1996   fix S assume "?r" "open S" "ereal x \<in> S"
  1997   show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
  1998     using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
  1999     using `ereal x \<in> S` by auto
  2000 qed
  2001 
  2002 lemma lim_real_of_ereal[simp]:
  2003   assumes lim: "(f ---> ereal x) net"
  2004   shows "((\<lambda>x. real (f x)) ---> x) net"
  2005 proof (intro topological_tendstoI)
  2006   fix S assume "open S" "x \<in> S"
  2007   then have S: "open S" "ereal x \<in> ereal ` S"
  2008     by (simp_all add: inj_image_mem_iff)
  2009   have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S" by auto
  2010   from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
  2011   show "eventually (\<lambda>x. real (f x) \<in> S) net"
  2012     by (rule eventually_mono)
  2013 qed
  2014 
  2015 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
  2016 proof -
  2017   { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
  2018     from this[THEN spec, of "real l"]
  2019     have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
  2020       by (cases l) (auto elim: eventually_elim1) }
  2021   then show ?thesis
  2022     by (auto simp: order_tendsto_iff)
  2023 qed
  2024 
  2025 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
  2026   unfolding tendsto_def
  2027 proof safe
  2028   fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
  2029   from open_MInfty[OF this] guess B .. note B = this
  2030   moreover
  2031   assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
  2032   then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
  2033   ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
  2034 next
  2035   fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
  2036   from this[rule_format, of "{..< ereal x}"]
  2037   show "eventually (\<lambda>y. f y < ereal x) F" by auto
  2038 qed
  2039 
  2040 lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
  2041   unfolding tendsto_PInfty eventually_sequentially
  2042 proof safe
  2043   fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
  2044   from this[rule_format, of "r+1"] guess N ..
  2045   moreover have "ereal r < ereal (r + 1)" by auto
  2046   ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
  2047     by (blast intro: less_le_trans)
  2048 qed (blast intro: less_imp_le)
  2049 
  2050 lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
  2051   unfolding tendsto_MInfty eventually_sequentially
  2052 proof safe
  2053   fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
  2054   from this[rule_format, of "r - 1"] guess N ..
  2055   moreover have "ereal (r - 1) < ereal r" by auto
  2056   ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
  2057     by (blast intro: le_less_trans)
  2058 qed (blast intro: less_imp_le)
  2059 
  2060 lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
  2061   using LIMSEQ_le_const2[of f l "ereal B"] by auto
  2062 
  2063 lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
  2064   using LIMSEQ_le_const[of f l "ereal B"] by auto
  2065 
  2066 lemma tendsto_explicit:
  2067   "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
  2068   unfolding tendsto_def eventually_sequentially by auto
  2069 
  2070 lemma Lim_bounded_PInfty2:
  2071   "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
  2072   using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
  2073 
  2074 lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
  2075   by (intro LIMSEQ_le_const2) auto
  2076 
  2077 lemma real_of_ereal_mult[simp]:
  2078   fixes a b :: ereal shows "real (a * b) = real a * real b"
  2079   by (cases rule: ereal2_cases[of a b]) auto
  2080 
  2081 lemma real_of_ereal_eq_0:
  2082   fixes x :: ereal shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
  2083   by (cases x) auto
  2084 
  2085 lemma tendsto_ereal_realD:
  2086   fixes f :: "'a \<Rightarrow> ereal"
  2087   assumes "x \<noteq> 0" and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2088   shows "(f ---> x) net"
  2089 proof (intro topological_tendstoI)
  2090   fix S assume S: "open S" "x \<in> S"
  2091   with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
  2092   from tendsto[THEN topological_tendstoD, OF this]
  2093   show "eventually (\<lambda>x. f x \<in> S) net"
  2094     by (rule eventually_rev_mp) (auto simp: ereal_real)
  2095 qed
  2096 
  2097 lemma tendsto_ereal_realI:
  2098   fixes f :: "'a \<Rightarrow> ereal"
  2099   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
  2100   shows "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2101 proof (intro topological_tendstoI)
  2102   fix S assume "open S" "x \<in> S"
  2103   with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}" by auto
  2104   from tendsto[THEN topological_tendstoD, OF this]
  2105   show "eventually (\<lambda>x. ereal (real (f x)) \<in> S) net"
  2106     by (elim eventually_elim1) (auto simp: ereal_real)
  2107 qed
  2108 
  2109 lemma ereal_mult_cancel_left:
  2110   fixes a b c :: ereal shows "a * b = a * c \<longleftrightarrow>
  2111     ((\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c)"
  2112   by (cases rule: ereal3_cases[of a b c])
  2113      (simp_all add: zero_less_mult_iff)
  2114 
  2115 lemma ereal_inj_affinity:
  2116   fixes m t :: ereal
  2117   assumes "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" "\<bar>t\<bar> \<noteq> \<infinity>"
  2118   shows "inj_on (\<lambda>x. m * x + t) A"
  2119   using assms
  2120   by (cases rule: ereal2_cases[of m t])
  2121      (auto intro!: inj_onI simp: ereal_add_cancel_right ereal_mult_cancel_left)
  2122 
  2123 lemma ereal_PInfty_eq_plus[simp]:
  2124   fixes a b :: ereal
  2125   shows "\<infinity> = a + b \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
  2126   by (cases rule: ereal2_cases[of a b]) auto
  2127 
  2128 lemma ereal_MInfty_eq_plus[simp]:
  2129   fixes a b :: ereal
  2130   shows "-\<infinity> = a + b \<longleftrightarrow> (a = -\<infinity> \<and> b \<noteq> \<infinity>) \<or> (b = -\<infinity> \<and> a \<noteq> \<infinity>)"
  2131   by (cases rule: ereal2_cases[of a b]) auto
  2132 
  2133 lemma ereal_less_divide_pos:
  2134   fixes x y :: ereal
  2135   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
  2136   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2137 
  2138 lemma ereal_divide_less_pos:
  2139   fixes x y z :: ereal
  2140   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
  2141   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2142 
  2143 lemma ereal_divide_eq:
  2144   fixes a b c :: ereal
  2145   shows "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
  2146   by (cases rule: ereal3_cases[of a b c])
  2147      (simp_all add: field_simps)
  2148 
  2149 lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) \<noteq> -\<infinity>"
  2150   by (cases a) auto
  2151 
  2152 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
  2153   by (cases x) auto
  2154 
  2155 lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
  2156   using assms by auto
  2157 
  2158 lemma ereal_le_ereal_bounded:
  2159   fixes x y z :: ereal
  2160   assumes "z \<le> y"
  2161   assumes *: "\<And>B. z < B \<Longrightarrow> B < x \<Longrightarrow> B \<le> y"
  2162   shows "x \<le> y"
  2163 proof (rule ereal_le_ereal)
  2164   fix B assume "B < x"
  2165   show "B \<le> y"
  2166   proof cases
  2167     assume "z < B" from *[OF this `B < x`] show "B \<le> y" .
  2168   next
  2169     assume "\<not> z < B" with `z \<le> y` show "B \<le> y" by auto
  2170   qed
  2171 qed
  2172 
  2173 lemma fixes x y :: ereal
  2174   shows Sup_atMost[simp]: "Sup {.. y} = y"
  2175     and Sup_lessThan[simp]: "Sup {..< y} = y"
  2176     and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y"
  2177     and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y"
  2178     and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
  2179   by (auto simp: Sup_ereal_def intro!: Least_equality
  2180            intro: ereal_le_ereal ereal_le_ereal_bounded[of x])
  2181 
  2182 lemma Sup_greaterThanlessThan[simp]:
  2183   fixes x y :: ereal assumes "x < y" shows "Sup { x <..< y} = y"
  2184   unfolding Sup_ereal_def
  2185 proof (intro Least_equality ereal_le_ereal_bounded[of _ _ y])
  2186   fix z assume z: "\<forall>u\<in>{x<..<y}. u \<le> z"
  2187   from ereal_dense[OF `x < y`] guess w .. note w = this
  2188   with z[THEN bspec, of w] show "x \<le> z" by auto
  2189 qed auto
  2190 
  2191 lemma real_ereal_id: "real o ereal = id"
  2192 proof-
  2193   { fix x have "(real o ereal) x = id x" by auto }
  2194   then show ?thesis using ext by blast
  2195 qed
  2196 
  2197 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
  2198 by (metis range_ereal open_ereal open_UNIV)
  2199 
  2200 lemma ereal_le_distrib:
  2201   fixes a b c :: ereal shows "c * (a + b) \<le> c * a + c * b"
  2202   by (cases rule: ereal3_cases[of a b c])
  2203      (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2204 
  2205 lemma ereal_pos_distrib:
  2206   fixes a b c :: ereal assumes "0 \<le> c" "c \<noteq> \<infinity>" shows "c * (a + b) = c * a + c * b"
  2207   using assms by (cases rule: ereal3_cases[of a b c])
  2208                  (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2209 
  2210 lemma ereal_pos_le_distrib:
  2211 fixes a b c :: ereal
  2212 assumes "c>=0"
  2213 shows "c * (a + b) <= c * a + c * b"
  2214   using assms by (cases rule: ereal3_cases[of a b c])
  2215                  (auto simp add: field_simps)
  2216 
  2217 lemma ereal_max_mono:
  2218   "[| (a::ereal) <= b; c <= d |] ==> max a c <= max b d"
  2219   by (metis sup_ereal_def sup_mono)
  2220 
  2221 
  2222 lemma ereal_max_least:
  2223   "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
  2224   by (metis sup_ereal_def sup_least)
  2225 
  2226 lemma ereal_LimI_finite:
  2227   fixes x :: ereal
  2228   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2229   assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
  2230   shows "u ----> x"
  2231 proof (rule topological_tendstoI, unfold eventually_sequentially)
  2232   obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
  2233   fix S assume "open S" "x : S"
  2234   then have "open (ereal -` S)" unfolding open_ereal_def by auto
  2235   with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
  2236     unfolding open_real_def rx_def by auto
  2237   then obtain n where
  2238     upper: "!!N. n <= N ==> u N < x + ereal r" and
  2239     lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
  2240   show "EX N. ALL n>=N. u n : S"
  2241   proof (safe intro!: exI[of _ n])
  2242     fix N assume "n <= N"
  2243     from upper[OF this] lower[OF this] assms `0 < r`
  2244     have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
  2245     then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
  2246     hence "rx < ra + r" and "ra < rx + r"
  2247        using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
  2248     hence "dist (real (u N)) rx < r"
  2249       using rx_def ra_def
  2250       by (auto simp: dist_real_def abs_diff_less_iff field_simps)
  2251     from dist[OF this] show "u N : S" using `u N  ~: {\<infinity>, -\<infinity>}`
  2252       by (auto simp: ereal_real split: split_if_asm)
  2253   qed
  2254 qed
  2255 
  2256 lemma tendsto_obtains_N:
  2257   assumes "f ----> f0"
  2258   assumes "open S" "f0 : S"
  2259   obtains N where "ALL n>=N. f n : S"
  2260   using tendsto_explicit[of f f0] assms by auto
  2261 
  2262 lemma ereal_LimI_finite_iff:
  2263   fixes x :: ereal
  2264   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2265   shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
  2266   (is "?lhs <-> ?rhs")
  2267 proof
  2268   assume lim: "u ----> x"
  2269   { fix r assume "(r::ereal)>0"
  2270     then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
  2271        apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
  2272        using lim ereal_between[of x r] assms `r>0` by auto
  2273     hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
  2274       using ereal_minus_less[of r x] by (cases r) auto
  2275   } then show "?rhs" by auto
  2276 next
  2277   assume ?rhs then show "u ----> x"
  2278     using ereal_LimI_finite[of x] assms by auto
  2279 qed
  2280 
  2281 
  2282 subsubsection {* @{text Liminf} and @{text Limsup} *}
  2283 
  2284 definition
  2285   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
  2286 
  2287 definition
  2288   "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
  2289 
  2290 abbreviation "liminf \<equiv> Liminf sequentially"
  2291 
  2292 abbreviation "limsup \<equiv> Limsup sequentially"
  2293 
  2294 lemma Liminf_eqI:
  2295   "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
  2296     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
  2297   unfolding Liminf_def by (auto intro!: SUP_eqI)
  2298 
  2299 lemma Limsup_eqI:
  2300   "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
  2301     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
  2302   unfolding Limsup_def by (auto intro!: INF_eqI)
  2303 
  2304 lemma liminf_SUPR_INFI:
  2305   fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
  2306   shows "liminf f = (SUP n. INF m:{n..}. f m)"
  2307   unfolding Liminf_def eventually_sequentially
  2308   by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
  2309 
  2310 lemma limsup_INFI_SUPR:
  2311   fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
  2312   shows "limsup f = (INF n. SUP m:{n..}. f m)"
  2313   unfolding Limsup_def eventually_sequentially
  2314   by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
  2315 
  2316 lemma Limsup_const: 
  2317   assumes ntriv: "\<not> trivial_limit F"
  2318   shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
  2319 proof -
  2320   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
  2321   have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
  2322     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
  2323   then show ?thesis
  2324     unfolding Limsup_def using eventually_True
  2325     by (subst INF_cong[where D="\<lambda>x. c"])
  2326        (auto intro!: INF_const simp del: eventually_True)
  2327 qed
  2328 
  2329 lemma Liminf_const:
  2330   assumes ntriv: "\<not> trivial_limit F"
  2331   shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
  2332 proof -
  2333   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
  2334   have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
  2335     using ntriv by (intro INF_const) (auto simp: eventually_False *)
  2336   then show ?thesis
  2337     unfolding Liminf_def using eventually_True
  2338     by (subst SUP_cong[where D="\<lambda>x. c"])
  2339        (auto intro!: SUP_const simp del: eventually_True)
  2340 qed
  2341 
  2342 lemma Liminf_mono:
  2343   fixes f g :: "'a => 'b :: complete_lattice"
  2344   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
  2345   shows "Liminf F f \<le> Liminf F g"
  2346   unfolding Liminf_def
  2347 proof (safe intro!: SUP_mono)
  2348   fix P assume "eventually P F"
  2349   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
  2350   then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
  2351     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
  2352 qed
  2353 
  2354 lemma Liminf_eq:
  2355   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2356   assumes "eventually (\<lambda>x. f x = g x) F"
  2357   shows "Liminf F f = Liminf F g"
  2358   by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
  2359 
  2360 lemma Limsup_mono:
  2361   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2362   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
  2363   shows "Limsup F f \<le> Limsup F g"
  2364   unfolding Limsup_def
  2365 proof (safe intro!: INF_mono)
  2366   fix P assume "eventually P F"
  2367   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
  2368   then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
  2369     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
  2370 qed
  2371 
  2372 lemma Limsup_eq:
  2373   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
  2374   assumes "eventually (\<lambda>x. f x = g x) net"
  2375   shows "Limsup net f = Limsup net g"
  2376   by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
  2377 
  2378 lemma Liminf_le_Limsup:
  2379   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
  2380   assumes ntriv: "\<not> trivial_limit F"
  2381   shows "Liminf F f \<le> Limsup F f"
  2382   unfolding Limsup_def Liminf_def
  2383   apply (rule complete_lattice_class.SUP_least)
  2384   apply (rule complete_lattice_class.INF_greatest)
  2385 proof safe
  2386   fix P Q assume "eventually P F" "eventually Q F"
  2387   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
  2388   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
  2389     using ntriv by (auto simp add: eventually_False)
  2390   have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
  2391     by (rule INF_mono) auto
  2392   also have "\<dots> \<le> SUPR (Collect ?C) f"
  2393     using not_False by (intro INF_le_SUP) auto
  2394   also have "\<dots> \<le> SUPR (Collect Q) f"
  2395     by (rule SUP_mono) auto
  2396   finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
  2397 qed
  2398 
  2399 lemma
  2400   fixes X :: "nat \<Rightarrow> ereal"
  2401   shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
  2402     and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
  2403   unfolding incseq_def decseq_def by auto
  2404 
  2405 lemma Liminf_bounded:
  2406   fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
  2407   assumes ntriv: "\<not> trivial_limit F"
  2408   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
  2409   shows "C \<le> Liminf F X"
  2410   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
  2411 
  2412 lemma Limsup_bounded:
  2413   fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
  2414   assumes ntriv: "\<not> trivial_limit F"
  2415   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
  2416   shows "Limsup F X \<le> C"
  2417   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
  2418 
  2419 lemma le_Liminf_iff:
  2420   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
  2421   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
  2422 proof -
  2423   { fix y P assume "eventually P F" "y < INFI (Collect P) X"
  2424     then have "eventually (\<lambda>x. y < X x) F"
  2425       by (auto elim!: eventually_elim1 dest: less_INF_D) }
  2426   moreover
  2427   { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
  2428     have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
  2429     proof cases
  2430       assume "\<exists>z. y < z \<and> z < C"
  2431       then guess z ..
  2432       moreover then have "z \<le> INFI {x. z < X x} X"
  2433         by (auto intro!: INF_greatest)
  2434       ultimately show ?thesis
  2435         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
  2436     next
  2437       assume "\<not> (\<exists>z. y < z \<and> z < C)"
  2438       then have "C \<le> INFI {x. y < X x} X"
  2439         by (intro INF_greatest) auto
  2440       with `y < C` show ?thesis
  2441         using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
  2442     qed }
  2443   ultimately show ?thesis
  2444     unfolding Liminf_def le_SUP_iff by auto
  2445 qed
  2446 
  2447 lemma lim_imp_Liminf:
  2448   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
  2449   assumes ntriv: "\<not> trivial_limit F"
  2450   assumes lim: "(f ---> f0) F"
  2451   shows "Liminf F f = f0"
  2452 proof (intro Liminf_eqI)
  2453   fix P assume P: "eventually P F"
  2454   then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
  2455     by eventually_elim (auto intro!: INF_lower)
  2456   then show "INFI (Collect P) f \<le> f0"
  2457     by (rule tendsto_le[OF ntriv lim tendsto_const])
  2458 next
  2459   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
  2460   show "f0 \<le> y"
  2461   proof cases
  2462     assume "\<exists>z. y < z \<and> z < f0"
  2463     then guess z ..
  2464     moreover have "z \<le> INFI {x. z < f x} f"
  2465       by (rule INF_greatest) simp
  2466     ultimately show ?thesis
  2467       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
  2468   next
  2469     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
  2470     show ?thesis
  2471     proof (rule classical)
  2472       assume "\<not> f0 \<le> y"
  2473       then have "eventually (\<lambda>x. y < f x) F"
  2474         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
  2475       then have "eventually (\<lambda>x. f0 \<le> f x) F"
  2476         using discrete by (auto elim!: eventually_elim1)
  2477       then have "INFI {x. f0 \<le> f x} f \<le> y"
  2478         by (rule upper)
  2479       moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
  2480         by (intro INF_greatest) simp
  2481       ultimately show "f0 \<le> y" by simp
  2482     qed
  2483   qed
  2484 qed
  2485 
  2486 lemma lim_imp_Limsup:
  2487   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
  2488   assumes ntriv: "\<not> trivial_limit F"
  2489   assumes lim: "(f ---> f0) F"
  2490   shows "Limsup F f = f0"
  2491 proof (intro Limsup_eqI)
  2492   fix P assume P: "eventually P F"
  2493   then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
  2494     by eventually_elim (auto intro!: SUP_upper)
  2495   then show "f0 \<le> SUPR (Collect P) f"
  2496     by (rule tendsto_le[OF ntriv tendsto_const lim])
  2497 next
  2498   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
  2499   show "y \<le> f0"
  2500   proof cases
  2501     assume "\<exists>z. f0 < z \<and> z < y"
  2502     then guess z ..
  2503     moreover have "SUPR {x. f x < z} f \<le> z"
  2504       by (rule SUP_least) simp
  2505     ultimately show ?thesis
  2506       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
  2507   next
  2508     assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
  2509     show ?thesis
  2510     proof (rule classical)
  2511       assume "\<not> y \<le> f0"
  2512       then have "eventually (\<lambda>x. f x < y) F"
  2513         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
  2514       then have "eventually (\<lambda>x. f x \<le> f0) F"
  2515         using discrete by (auto elim!: eventually_elim1 simp: not_less)
  2516       then have "y \<le> SUPR {x. f x \<le> f0} f"
  2517         by (rule lower)
  2518       moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
  2519         by (intro SUP_least) simp
  2520       ultimately show "y \<le> f0" by simp
  2521     qed
  2522   qed
  2523 qed
  2524 
  2525 lemma Liminf_eq_Limsup:
  2526   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
  2527   assumes ntriv: "\<not> trivial_limit F"
  2528     and lim: "Liminf F f = f0" "Limsup F f = f0"
  2529   shows "(f ---> f0) F"
  2530 proof (rule order_tendstoI)
  2531   fix a assume "f0 < a"
  2532   with assms have "Limsup F f < a" by simp
  2533   then obtain P where "eventually P F" "SUPR (Collect P) f < a"
  2534     unfolding Limsup_def INF_less_iff by auto
  2535   then show "eventually (\<lambda>x. f x < a) F"
  2536     by (auto elim!: eventually_elim1 dest: SUP_lessD)
  2537 next
  2538   fix a assume "a < f0"
  2539   with assms have "a < Liminf F f" by simp
  2540   then obtain P where "eventually P F" "a < INFI (Collect P) f"
  2541     unfolding Liminf_def less_SUP_iff by auto
  2542   then show "eventually (\<lambda>x. a < f x) F"
  2543     by (auto elim!: eventually_elim1 dest: less_INF_D)
  2544 qed
  2545 
  2546 lemma tendsto_iff_Liminf_eq_Limsup:
  2547   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
  2548   shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
  2549   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
  2550 
  2551 lemma liminf_bounded_iff:
  2552   fixes x :: "nat \<Rightarrow> ereal"
  2553   shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
  2554   unfolding le_Liminf_iff eventually_sequentially ..
  2555 
  2556 lemma liminf_subseq_mono:
  2557   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
  2558   assumes "subseq r"
  2559   shows "liminf X \<le> liminf (X \<circ> r) "
  2560 proof-
  2561   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
  2562   proof (safe intro!: INF_mono)
  2563     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
  2564       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
  2565   qed
  2566   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
  2567 qed
  2568 
  2569 lemma limsup_subseq_mono:
  2570   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
  2571   assumes "subseq r"
  2572   shows "limsup (X \<circ> r) \<le> limsup X"
  2573 proof-
  2574   have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
  2575   proof (safe intro!: SUP_mono)
  2576     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
  2577       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
  2578   qed
  2579   then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
  2580 qed
  2581 
  2582 definition (in order) mono_set:
  2583   "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
  2584 
  2585 lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
  2586 lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
  2587 lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
  2588 lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
  2589 
  2590 lemma (in complete_linorder) mono_set_iff:
  2591   fixes S :: "'a set"
  2592   defines "a \<equiv> Inf S"
  2593   shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
  2594 proof
  2595   assume "mono_set S"
  2596   then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
  2597   show ?c
  2598   proof cases
  2599     assume "a \<in> S"
  2600     show ?c
  2601       using mono[OF _ `a \<in> S`]
  2602       by (auto intro: Inf_lower simp: a_def)
  2603   next
  2604     assume "a \<notin> S"
  2605     have "S = {a <..}"
  2606     proof safe
  2607       fix x assume "x \<in> S"
  2608       then have "a \<le> x" unfolding a_def by (rule Inf_lower)
  2609       then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
  2610     next
  2611       fix x assume "a < x"
  2612       then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
  2613       with mono[of y x] show "x \<in> S" by auto
  2614     qed
  2615     then show ?c ..
  2616   qed
  2617 qed auto
  2618 
  2619 subsubsection {* Tests for code generator *}
  2620 
  2621 (* A small list of simple arithmetic expressions *)
  2622 
  2623 value [code] "- \<infinity> :: ereal"
  2624 value [code] "\<bar>-\<infinity>\<bar> :: ereal"
  2625 value [code] "4 + 5 / 4 - ereal 2 :: ereal"
  2626 value [code] "ereal 3 < \<infinity>"
  2627 value [code] "real (\<infinity>::ereal) = 0"
  2628 
  2629 end