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