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