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