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