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