src/HOL/Library/Extended_Real.thy
author haftmann
Sat Mar 22 08:37:43 2014 +0100 (2014-03-22)
changeset 56248 67dc9549fa15
parent 56218 1c3f1f2431f9
child 56536 aefb4a8da31f
permissions -rw-r--r--
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
     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>SUPREMUM A f\<bar> \<noteq> \<infinity>"
  1415   using SUP_upper2[of _ A l f] SUP_least[of A f u]
  1416   by (cases "SUPREMUM 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>INFIMUM A f\<bar> \<noteq> \<infinity>"
  1421   using INF_lower2[of _ A f u] INF_greatest[of A l f]
  1422   by (cases "INFIMUM 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 "SUPREMUM 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 "SUPREMUM 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) = SUPREMUM UNIV f + SUPREMUM 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: "SUPREMUM 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 "SUPREMUM UNIV f + g j \<le> y"
  1569       using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
  1570     then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
  1571   }
  1572   then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
  1573     using f by (rule SUP_ereal_le_addI)
  1574   then show "SUPREMUM UNIV f + SUPREMUM 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) = SUPREMUM UNIV f + SUPREMUM 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. SUPREMUM 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 * SUPREMUM UNIV f"
  1608 proof (rule SUP_eqI)
  1609   fix i
  1610   have "f i \<le> SUPREMUM UNIV f"
  1611     by (rule SUP_upper) auto
  1612   then show "c * f i \<le> c * SUPREMUM 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   then have *: "\<And>i. c * f i \<le> y" by simp
  1618   show "c * SUPREMUM UNIV f \<le> y"
  1619   proof (cases "0 < c \<and> c \<noteq> \<infinity>")
  1620     case True
  1621     with * have "SUPREMUM UNIV f \<le> y / c"
  1622       by (intro SUP_least) (auto simp: ereal_le_divide_pos)
  1623     with True show ?thesis
  1624       by (auto simp: ereal_le_divide_pos)
  1625   next
  1626     case False
  1627     {
  1628       assume "c = \<infinity>"
  1629       have ?thesis
  1630       proof (cases "\<forall>i. f i = 0")
  1631         case True
  1632         then have "range f = {0}"
  1633           by auto
  1634         with True show "c * SUPREMUM UNIV f \<le> y"
  1635           using * by auto
  1636       next
  1637         case False
  1638         then obtain i where "f i \<noteq> 0"
  1639           by auto
  1640         with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
  1641           by (auto split: split_if_asm)
  1642       qed
  1643     }
  1644     moreover note False
  1645     ultimately show ?thesis
  1646       using * `0 \<le> c` by auto
  1647   qed
  1648 qed
  1649 
  1650 lemma SUP_PInfty:
  1651   fixes f :: "'a \<Rightarrow> ereal"
  1652   assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
  1653   shows "(SUP i:A. f i) = \<infinity>"
  1654   unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
  1655   apply simp
  1656 proof safe
  1657   fix x :: ereal
  1658   assume "x \<noteq> \<infinity>"
  1659   show "\<exists>i\<in>A. x < f i"
  1660   proof (cases x)
  1661     case PInf
  1662     with `x \<noteq> \<infinity>` show ?thesis
  1663       by simp
  1664   next
  1665     case MInf
  1666     with assms[of "0"] show ?thesis
  1667       by force
  1668   next
  1669     case (real r)
  1670     with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
  1671       by auto
  1672     moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
  1673       using assms ..
  1674     ultimately show ?thesis
  1675       by (auto intro!: bexI[of _ i])
  1676   qed
  1677 qed
  1678 
  1679 lemma Sup_countable_SUP:
  1680   assumes "A \<noteq> {}"
  1681   shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
  1682 proof (cases "Sup A")
  1683   case (real r)
  1684   have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
  1685   proof
  1686     fix n :: nat
  1687     have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
  1688       using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
  1689     then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
  1690     then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
  1691       by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
  1692   qed
  1693   from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
  1694     where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
  1695   have "SUPREMUM UNIV f = Sup A"
  1696   proof (rule SUP_eqI)
  1697     fix i
  1698     show "f i \<le> Sup A"
  1699       using f by (auto intro!: complete_lattice_class.Sup_upper)
  1700   next
  1701     fix y
  1702     assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
  1703     show "Sup A \<le> y"
  1704     proof (rule ereal_le_epsilon, intro allI impI)
  1705       fix e :: ereal
  1706       assume "0 < e"
  1707       show "Sup A \<le> y + e"
  1708       proof (cases e)
  1709         case (real r)
  1710         then have "0 < r"
  1711           using `0 < e` by auto
  1712         then obtain n :: nat where *: "1 / real n < r" "0 < n"
  1713           using ex_inverse_of_nat_less
  1714           by (auto simp: real_eq_of_nat inverse_eq_divide)
  1715         have "Sup A \<le> f n + 1 / ereal (real n)"
  1716           using f[THEN spec, of n]
  1717           by auto
  1718         also have "1 / ereal (real n) \<le> e"
  1719           using real *
  1720           by (auto simp: one_ereal_def )
  1721         with bound have "f n + 1 / ereal (real n) \<le> y + e"
  1722           by (rule add_mono) simp
  1723         finally show "Sup A \<le> y + e" .
  1724       qed (insert `0 < e`, auto)
  1725     qed
  1726   qed
  1727   with f show ?thesis
  1728     by (auto intro!: exI[of _ f])
  1729 next
  1730   case PInf
  1731   from `A \<noteq> {}` obtain x where "x \<in> A"
  1732     by auto
  1733   show ?thesis
  1734   proof (cases "\<infinity> \<in> A")
  1735     case True
  1736     then have "\<infinity> \<le> Sup A"
  1737       by (intro complete_lattice_class.Sup_upper)
  1738     with True show ?thesis
  1739       by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
  1740   next
  1741     case False
  1742     have "\<exists>x\<in>A. 0 \<le> x"
  1743       by (metis Infty_neq_0(2) PInf complete_lattice_class.Sup_least ereal_infty_less_eq2(1) linorder_linear)
  1744     then obtain x where "x \<in> A" and "0 \<le> x"
  1745       by auto
  1746     have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
  1747     proof (rule ccontr)
  1748       assume "\<not> ?thesis"
  1749       then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
  1750         by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
  1751       then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
  1752         by (cases x) auto
  1753     qed
  1754     from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
  1755       where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
  1756     have "SUPREMUM UNIV f = \<infinity>"
  1757     proof (rule SUP_PInfty)
  1758       fix n :: nat
  1759       show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
  1760         using f[THEN spec, of n] `0 \<le> x`
  1761         by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
  1762     qed
  1763     then show ?thesis
  1764       using f PInf by (auto intro!: exI[of _ f])
  1765   qed
  1766 next
  1767   case MInf
  1768   with `A \<noteq> {}` have "A = {-\<infinity>}"
  1769     by (auto simp: Sup_eq_MInfty)
  1770   then show ?thesis
  1771     using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
  1772 qed
  1773 
  1774 lemma SUP_countable_SUP:
  1775   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
  1776   using Sup_countable_SUP [of "g`A"]
  1777   by auto
  1778 
  1779 lemma Sup_ereal_cadd:
  1780   fixes A :: "ereal set"
  1781   assumes "A \<noteq> {}"
  1782     and "a \<noteq> -\<infinity>"
  1783   shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
  1784 proof (rule antisym)
  1785   have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
  1786     by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
  1787   then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
  1788   show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
  1789   proof (cases a)
  1790     case PInf with `A \<noteq> {}`
  1791     show ?thesis
  1792       by (auto simp: image_constant max.absorb1)
  1793   next
  1794     case (real r)
  1795     then have **: "op + (- a) ` op + a ` A = A"
  1796       by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
  1797     from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
  1798       unfolding **
  1799       by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
  1800   qed (insert `a \<noteq> -\<infinity>`, auto)
  1801 qed
  1802 
  1803 lemma Sup_ereal_cminus:
  1804   fixes A :: "ereal set"
  1805   assumes "A \<noteq> {}"
  1806     and "a \<noteq> -\<infinity>"
  1807   shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
  1808   using Sup_ereal_cadd [of "uminus ` A" a] assms
  1809   unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
  1810 
  1811 lemma SUP_ereal_cminus:
  1812   fixes f :: "'i \<Rightarrow> ereal"
  1813   fixes A
  1814   assumes "A \<noteq> {}"
  1815     and "a \<noteq> -\<infinity>"
  1816   shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
  1817   using Sup_ereal_cminus[of "f`A" a] assms
  1818   unfolding SUP_def INF_def image_image by auto
  1819 
  1820 lemma Inf_ereal_cminus:
  1821   fixes A :: "ereal set"
  1822   assumes "A \<noteq> {}"
  1823     and "\<bar>a\<bar> \<noteq> \<infinity>"
  1824   shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
  1825 proof -
  1826   {
  1827     fix x
  1828     have "-a - -x = -(a - x)"
  1829       using assms by (cases x) auto
  1830   } note * = this
  1831   then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
  1832     by (auto simp: image_image)
  1833   with * show ?thesis
  1834     using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
  1835     by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
  1836 qed
  1837 
  1838 lemma INF_ereal_cminus:
  1839   fixes a :: ereal
  1840   assumes "A \<noteq> {}"
  1841     and "\<bar>a\<bar> \<noteq> \<infinity>"
  1842   shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
  1843   using Inf_ereal_cminus[of "f`A" a] assms
  1844   unfolding SUP_def INF_def image_image
  1845   by auto
  1846 
  1847 lemma uminus_ereal_add_uminus_uminus:
  1848   fixes a b :: ereal
  1849   shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
  1850   by (cases rule: ereal2_cases[of a b]) auto
  1851 
  1852 lemma INF_ereal_add:
  1853   fixes f :: "nat \<Rightarrow> ereal"
  1854   assumes "decseq f" "decseq g"
  1855     and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
  1856   shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
  1857 proof -
  1858   have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
  1859     using assms unfolding INF_less_iff by auto
  1860   {
  1861     fix i
  1862     from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
  1863       by (rule uminus_ereal_add_uminus_uminus)
  1864   }
  1865   then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
  1866     by simp
  1867   also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
  1868     unfolding ereal_INF_uminus
  1869     using assms INF_less
  1870     by (subst SUP_ereal_add)
  1871        (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
  1872   finally show ?thesis .
  1873 qed
  1874 
  1875 subsection "Relation to @{typ enat}"
  1876 
  1877 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
  1878 
  1879 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
  1880 declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
  1881 
  1882 lemma ereal_of_enat_simps[simp]:
  1883   "ereal_of_enat (enat n) = ereal n"
  1884   "ereal_of_enat \<infinity> = \<infinity>"
  1885   by (simp_all add: ereal_of_enat_def)
  1886 
  1887 lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
  1888   by (cases m n rule: enat2_cases) auto
  1889 
  1890 lemma ereal_of_enat_less_iff[simp]: "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
  1891   by (cases m n rule: enat2_cases) auto
  1892 
  1893 lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
  1894   by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
  1895 
  1896 lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
  1897   by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
  1898 
  1899 lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
  1900   by (cases n) (auto simp: enat_0[symmetric])
  1901 
  1902 lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
  1903   by (cases n) (auto simp: enat_0[symmetric])
  1904 
  1905 lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
  1906   by (auto simp: enat_0[symmetric])
  1907 
  1908 lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
  1909   by (cases n) auto
  1910 
  1911 lemma ereal_of_enat_add: "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
  1912   by (cases m n rule: enat2_cases) auto
  1913 
  1914 lemma ereal_of_enat_sub:
  1915   assumes "n \<le> m"
  1916   shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
  1917   using assms by (cases m n rule: enat2_cases) auto
  1918 
  1919 lemma ereal_of_enat_mult:
  1920   "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
  1921   by (cases m n rule: enat2_cases) auto
  1922 
  1923 lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
  1924 lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
  1925 
  1926 
  1927 subsection "Limits on @{typ ereal}"
  1928 
  1929 subsubsection "Topological space"
  1930 
  1931 instantiation ereal :: linear_continuum_topology
  1932 begin
  1933 
  1934 definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
  1935   open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
  1936 
  1937 instance
  1938   by default (simp add: open_ereal_generated)
  1939 
  1940 end
  1941 
  1942 lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
  1943   unfolding open_ereal_generated
  1944 proof (induct rule: generate_topology.induct)
  1945   case (Int A B)
  1946   then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
  1947     by auto
  1948   with Int show ?case
  1949     by (intro exI[of _ "max x z"]) fastforce
  1950 next
  1951   case (Basis S)
  1952   {
  1953     fix x
  1954     have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t"
  1955       by (cases x) auto
  1956   }
  1957   moreover note Basis
  1958   ultimately show ?case
  1959     by (auto split: ereal.split)
  1960 qed (fastforce simp add: vimage_Union)+
  1961 
  1962 lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
  1963   unfolding open_ereal_generated
  1964 proof (induct rule: generate_topology.induct)
  1965   case (Int A B)
  1966   then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
  1967     by auto
  1968   with Int show ?case
  1969     by (intro exI[of _ "min x z"]) fastforce
  1970 next
  1971   case (Basis S)
  1972   {
  1973     fix x
  1974     have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x"
  1975       by (cases x) auto
  1976   }
  1977   moreover note Basis
  1978   ultimately show ?case
  1979     by (auto split: ereal.split)
  1980 qed (fastforce simp add: vimage_Union)+
  1981 
  1982 lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
  1983   unfolding open_ereal_generated
  1984 proof (induct rule: generate_topology.induct)
  1985   case (Int A B)
  1986   then show ?case
  1987     by auto
  1988 next
  1989   case (Basis S)
  1990   {
  1991     fix x have
  1992       "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
  1993       "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
  1994       by (induct x) auto
  1995   }
  1996   moreover note Basis
  1997   ultimately show ?case
  1998     by (auto split: ereal.split)
  1999 qed (fastforce simp add: vimage_Union)+
  2000 
  2001 lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
  2002   unfolding open_generated_order[where 'a=real]
  2003 proof (induct rule: generate_topology.induct)
  2004   case (Basis S)
  2005   moreover {
  2006     fix x
  2007     have "ereal ` {..< x} = { -\<infinity> <..< ereal x }"
  2008       apply auto
  2009       apply (case_tac xa)
  2010       apply auto
  2011       done
  2012   }
  2013   moreover {
  2014     fix x
  2015     have "ereal ` {x <..} = { ereal x <..< \<infinity> }"
  2016       apply auto
  2017       apply (case_tac xa)
  2018       apply auto
  2019       done
  2020   }
  2021   ultimately show ?case
  2022      by auto
  2023 qed (auto simp add: image_Union image_Int)
  2024 
  2025 lemma open_ereal_def:
  2026   "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))"
  2027   (is "open A \<longleftrightarrow> ?rhs")
  2028 proof
  2029   assume "open A"
  2030   then show ?rhs
  2031     using open_PInfty open_MInfty open_ereal_vimage by auto
  2032 next
  2033   assume "?rhs"
  2034   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"
  2035     by auto
  2036   have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
  2037     using A(2,3) by auto
  2038   from open_ereal[OF A(1)] show "open A"
  2039     by (subst *) (auto simp: open_Un)
  2040 qed
  2041 
  2042 lemma open_PInfty2:
  2043   assumes "open A"
  2044     and "\<infinity> \<in> A"
  2045   obtains x where "{ereal x<..} \<subseteq> A"
  2046   using open_PInfty[OF assms] by auto
  2047 
  2048 lemma open_MInfty2:
  2049   assumes "open A"
  2050     and "-\<infinity> \<in> A"
  2051   obtains x where "{..<ereal x} \<subseteq> A"
  2052   using open_MInfty[OF assms] by auto
  2053 
  2054 lemma ereal_openE:
  2055   assumes "open A"
  2056   obtains x y where "open (ereal -` A)"
  2057     and "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
  2058     and "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
  2059   using assms open_ereal_def by auto
  2060 
  2061 lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
  2062 lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
  2063 lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
  2064 lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
  2065 lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
  2066 lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
  2067 lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
  2068 
  2069 lemma ereal_open_cont_interval:
  2070   fixes S :: "ereal set"
  2071   assumes "open S"
  2072     and "x \<in> S"
  2073     and "\<bar>x\<bar> \<noteq> \<infinity>"
  2074   obtains e where "e > 0" and "{x-e <..< x+e} \<subseteq> S"
  2075 proof -
  2076   from `open S`
  2077   have "open (ereal -` S)"
  2078     by (rule ereal_openE)
  2079   then obtain e where "e > 0" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
  2080     using assms unfolding open_dist by force
  2081   show thesis
  2082   proof (intro that subsetI)
  2083     show "0 < ereal e"
  2084       using `0 < e` by auto
  2085     fix y
  2086     assume "y \<in> {x - ereal e<..<x + ereal e}"
  2087     with assms obtain t where "y = ereal t" "dist t (real x) < e"
  2088       by (cases y) (auto simp: dist_real_def)
  2089     then show "y \<in> S"
  2090       using e[of t] by auto
  2091   qed
  2092 qed
  2093 
  2094 lemma ereal_open_cont_interval2:
  2095   fixes S :: "ereal set"
  2096   assumes "open S"
  2097     and "x \<in> S"
  2098     and x: "\<bar>x\<bar> \<noteq> \<infinity>"
  2099   obtains a b where "a < x" and "x < b" and "{a <..< b} \<subseteq> S"
  2100 proof -
  2101   obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
  2102     using assms by (rule ereal_open_cont_interval)
  2103   with that[of "x - e" "x + e"] ereal_between[OF x, of e]
  2104   show thesis
  2105     by auto
  2106 qed
  2107 
  2108 
  2109 subsubsection {* Convergent sequences *}
  2110 
  2111 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
  2112   (is "?l = ?r")
  2113 proof (intro iffI topological_tendstoI)
  2114   fix S
  2115   assume "?l" and "open S" and "x \<in> S"
  2116   then show "eventually (\<lambda>x. f x \<in> S) net"
  2117     using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
  2118     by (simp add: inj_image_mem_iff)
  2119 next
  2120   fix S
  2121   assume "?r" and "open S" and "ereal x \<in> S"
  2122   show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
  2123     using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
  2124     using `ereal x \<in> S`
  2125     by auto
  2126 qed
  2127 
  2128 lemma lim_real_of_ereal[simp]:
  2129   assumes lim: "(f ---> ereal x) net"
  2130   shows "((\<lambda>x. real (f x)) ---> x) net"
  2131 proof (intro topological_tendstoI)
  2132   fix S
  2133   assume "open S" and "x \<in> S"
  2134   then have S: "open S" "ereal x \<in> ereal ` S"
  2135     by (simp_all add: inj_image_mem_iff)
  2136   have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S"
  2137     by auto
  2138   from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
  2139   show "eventually (\<lambda>x. real (f x) \<in> S) net"
  2140     by (rule eventually_mono)
  2141 qed
  2142 
  2143 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
  2144 proof -
  2145   {
  2146     fix l :: ereal
  2147     assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
  2148     from this[THEN spec, of "real l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
  2149       by (cases l) (auto elim: eventually_elim1)
  2150   }
  2151   then show ?thesis
  2152     by (auto simp: order_tendsto_iff)
  2153 qed
  2154 
  2155 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
  2156   unfolding tendsto_def
  2157 proof safe
  2158   fix S :: "ereal set"
  2159   assume "open S" "-\<infinity> \<in> S"
  2160   from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
  2161   moreover
  2162   assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
  2163   then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
  2164     by auto
  2165   ultimately show "eventually (\<lambda>z. f z \<in> S) F"
  2166     by (auto elim!: eventually_elim1)
  2167 next
  2168   fix x
  2169   assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
  2170   from this[rule_format, of "{..< ereal x}"] show "eventually (\<lambda>y. f y < ereal x) F"
  2171     by auto
  2172 qed
  2173 
  2174 lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
  2175   unfolding tendsto_PInfty eventually_sequentially
  2176 proof safe
  2177   fix r
  2178   assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
  2179   then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n"
  2180     by blast
  2181   moreover have "ereal r < ereal (r + 1)"
  2182     by auto
  2183   ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
  2184     by (blast intro: less_le_trans)
  2185 qed (blast intro: less_imp_le)
  2186 
  2187 lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
  2188   unfolding tendsto_MInfty eventually_sequentially
  2189 proof safe
  2190   fix r
  2191   assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
  2192   then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)"
  2193     by blast
  2194   moreover have "ereal (r - 1) < ereal r"
  2195     by auto
  2196   ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
  2197     by (blast intro: le_less_trans)
  2198 qed (blast intro: less_imp_le)
  2199 
  2200 lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
  2201   using LIMSEQ_le_const2[of f l "ereal B"] by auto
  2202 
  2203 lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
  2204   using LIMSEQ_le_const[of f l "ereal B"] by auto
  2205 
  2206 lemma tendsto_explicit:
  2207   "f ----> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
  2208   unfolding tendsto_def eventually_sequentially by auto
  2209 
  2210 lemma Lim_bounded_PInfty2: "f ----> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
  2211   using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
  2212 
  2213 lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
  2214   by (intro LIMSEQ_le_const2) auto
  2215 
  2216 lemma Lim_bounded2_ereal:
  2217   assumes lim:"f ----> (l :: 'a::linorder_topology)"
  2218     and ge: "\<forall>n\<ge>N. f n \<ge> C"
  2219   shows "l \<ge> C"
  2220   using ge
  2221   by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
  2222      (auto simp: eventually_sequentially)
  2223 
  2224 lemma real_of_ereal_mult[simp]:
  2225   fixes a b :: ereal
  2226   shows "real (a * b) = real a * real b"
  2227   by (cases rule: ereal2_cases[of a b]) auto
  2228 
  2229 lemma real_of_ereal_eq_0:
  2230   fixes x :: ereal
  2231   shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
  2232   by (cases x) auto
  2233 
  2234 lemma tendsto_ereal_realD:
  2235   fixes f :: "'a \<Rightarrow> ereal"
  2236   assumes "x \<noteq> 0"
  2237     and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2238   shows "(f ---> x) net"
  2239 proof (intro topological_tendstoI)
  2240   fix S
  2241   assume S: "open S" "x \<in> S"
  2242   with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}"
  2243     by auto
  2244   from tendsto[THEN topological_tendstoD, OF this]
  2245   show "eventually (\<lambda>x. f x \<in> S) net"
  2246     by (rule eventually_rev_mp) (auto simp: ereal_real)
  2247 qed
  2248 
  2249 lemma tendsto_ereal_realI:
  2250   fixes f :: "'a \<Rightarrow> ereal"
  2251   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
  2252   shows "((\<lambda>x. ereal (real (f x))) ---> x) net"
  2253 proof (intro topological_tendstoI)
  2254   fix S
  2255   assume "open S" and "x \<in> S"
  2256   with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}"
  2257     by auto
  2258   from tendsto[THEN topological_tendstoD, OF this]
  2259   show "eventually (\<lambda>x. ereal (real (f x)) \<in> S) net"
  2260     by (elim eventually_elim1) (auto simp: ereal_real)
  2261 qed
  2262 
  2263 lemma ereal_mult_cancel_left:
  2264   fixes a b c :: ereal
  2265   shows "a * b = a * c \<longleftrightarrow> (\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c"
  2266   by (cases rule: ereal3_cases[of a b c]) (simp_all add: zero_less_mult_iff)
  2267 
  2268 lemma ereal_inj_affinity:
  2269   fixes m t :: ereal
  2270   assumes "\<bar>m\<bar> \<noteq> \<infinity>"
  2271     and "m \<noteq> 0"
  2272     and "\<bar>t\<bar> \<noteq> \<infinity>"
  2273   shows "inj_on (\<lambda>x. m * x + t) A"
  2274   using assms
  2275   by (cases rule: ereal2_cases[of m t])
  2276      (auto intro!: inj_onI simp: ereal_add_cancel_right ereal_mult_cancel_left)
  2277 
  2278 lemma ereal_PInfty_eq_plus[simp]:
  2279   fixes a b :: ereal
  2280   shows "\<infinity> = a + b \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
  2281   by (cases rule: ereal2_cases[of a b]) auto
  2282 
  2283 lemma ereal_MInfty_eq_plus[simp]:
  2284   fixes a b :: ereal
  2285   shows "-\<infinity> = a + b \<longleftrightarrow> (a = -\<infinity> \<and> b \<noteq> \<infinity>) \<or> (b = -\<infinity> \<and> a \<noteq> \<infinity>)"
  2286   by (cases rule: ereal2_cases[of a b]) auto
  2287 
  2288 lemma ereal_less_divide_pos:
  2289   fixes x y :: ereal
  2290   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
  2291   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2292 
  2293 lemma ereal_divide_less_pos:
  2294   fixes x y z :: ereal
  2295   shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
  2296   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
  2297 
  2298 lemma ereal_divide_eq:
  2299   fixes a b c :: ereal
  2300   shows "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
  2301   by (cases rule: ereal3_cases[of a b c])
  2302      (simp_all add: field_simps)
  2303 
  2304 lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) \<noteq> -\<infinity>"
  2305   by (cases a) auto
  2306 
  2307 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
  2308   by (cases x) auto
  2309 
  2310 lemma ereal_real':
  2311   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2312   shows "ereal (real x) = x"
  2313   using assms by auto
  2314 
  2315 lemma real_ereal_id: "real \<circ> ereal = id"
  2316 proof -
  2317   {
  2318     fix x
  2319     have "(real o ereal) x = id x"
  2320       by auto
  2321   }
  2322   then show ?thesis
  2323     using ext by blast
  2324 qed
  2325 
  2326 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
  2327   by (metis range_ereal open_ereal open_UNIV)
  2328 
  2329 lemma ereal_le_distrib:
  2330   fixes a b c :: ereal
  2331   shows "c * (a + b) \<le> c * a + c * b"
  2332   by (cases rule: ereal3_cases[of a b c])
  2333      (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2334 
  2335 lemma ereal_pos_distrib:
  2336   fixes a b c :: ereal
  2337   assumes "0 \<le> c"
  2338     and "c \<noteq> \<infinity>"
  2339   shows "c * (a + b) = c * a + c * b"
  2340   using assms
  2341   by (cases rule: ereal3_cases[of a b c])
  2342     (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2343 
  2344 lemma ereal_pos_le_distrib:
  2345   fixes a b c :: ereal
  2346   assumes "c \<ge> 0"
  2347   shows "c * (a + b) \<le> c * a + c * b"
  2348   using assms
  2349   by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
  2350 
  2351 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
  2352   by (metis sup_ereal_def sup_mono)
  2353 
  2354 lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x"
  2355   by (metis sup_ereal_def sup_least)
  2356 
  2357 lemma ereal_LimI_finite:
  2358   fixes x :: ereal
  2359   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2360     and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2361   shows "u ----> x"
  2362 proof (rule topological_tendstoI, unfold eventually_sequentially)
  2363   obtain rx where rx: "x = ereal rx"
  2364     using assms by (cases x) auto
  2365   fix S
  2366   assume "open S" and "x \<in> S"
  2367   then have "open (ereal -` S)"
  2368     unfolding open_ereal_def by auto
  2369   with `x \<in> S` obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
  2370     unfolding open_real_def rx by auto
  2371   then obtain n where
  2372     upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
  2373     lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
  2374     using assms(2)[of "ereal r"] by auto
  2375   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
  2376   proof (safe intro!: exI[of _ n])
  2377     fix N
  2378     assume "n \<le> N"
  2379     from upper[OF this] lower[OF this] assms `0 < r`
  2380     have "u N \<notin> {\<infinity>,(-\<infinity>)}"
  2381       by auto
  2382     then obtain ra where ra_def: "(u N) = ereal ra"
  2383       by (cases "u N") auto
  2384     then have "rx < ra + r" and "ra < rx + r"
  2385       using rx assms `0 < r` lower[OF `n \<le> N`] upper[OF `n \<le> N`]
  2386       by auto
  2387     then have "dist (real (u N)) rx < r"
  2388       using rx ra_def
  2389       by (auto simp: dist_real_def abs_diff_less_iff field_simps)
  2390     from dist[OF this] show "u N \<in> S"
  2391       using `u N  \<notin> {\<infinity>, -\<infinity>}`
  2392       by (auto simp: ereal_real split: split_if_asm)
  2393   qed
  2394 qed
  2395 
  2396 lemma tendsto_obtains_N:
  2397   assumes "f ----> f0"
  2398   assumes "open S"
  2399     and "f0 \<in> S"
  2400   obtains N where "\<forall>n\<ge>N. f n \<in> S"
  2401   using assms using tendsto_def
  2402   using tendsto_explicit[of f f0] assms by auto
  2403 
  2404 lemma ereal_LimI_finite_iff:
  2405   fixes x :: ereal
  2406   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
  2407   shows "u ----> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
  2408   (is "?lhs \<longleftrightarrow> ?rhs")
  2409 proof
  2410   assume lim: "u ----> x"
  2411   {
  2412     fix r :: ereal
  2413     assume "r > 0"
  2414     then obtain N where "\<forall>n\<ge>N. u n \<in> {x - r <..< x + r}"
  2415        apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
  2416        using lim ereal_between[of x r] assms `r > 0`
  2417        apply auto
  2418        done
  2419     then have "\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2420       using ereal_minus_less[of r x]
  2421       by (cases r) auto
  2422   }
  2423   then show ?rhs
  2424     by auto
  2425 next
  2426   assume ?rhs
  2427   then show "u ----> x"
  2428     using ereal_LimI_finite[of x] assms by auto
  2429 qed
  2430 
  2431 lemma ereal_Limsup_uminus:
  2432   fixes f :: "'a \<Rightarrow> ereal"
  2433   shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
  2434   unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
  2435 
  2436 lemma liminf_bounded_iff:
  2437   fixes x :: "nat \<Rightarrow> ereal"
  2438   shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)"
  2439   (is "?lhs \<longleftrightarrow> ?rhs")
  2440   unfolding le_Liminf_iff eventually_sequentially ..
  2441 
  2442 
  2443 subsubsection {* Tests for code generator *}
  2444 
  2445 (* A small list of simple arithmetic expressions *)
  2446 
  2447 value [code] "- \<infinity> :: ereal"
  2448 value [code] "\<bar>-\<infinity>\<bar> :: ereal"
  2449 value [code] "4 + 5 / 4 - ereal 2 :: ereal"
  2450 value [code] "ereal 3 < \<infinity>"
  2451 value [code] "real (\<infinity>::ereal) = 0"
  2452 
  2453 end