src/HOL/Library/Extended_Nonnegative_Real.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67727 ce3e87a51488
child 68406 6beb45f6cf67
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/Extended_Nonnegative_Real.thy
     2     Author:     Johannes Hölzl
     3 *)
     4 
     5 subsection \<open>The type of non-negative extended real numbers\<close>
     6 
     7 theory Extended_Nonnegative_Real
     8   imports Extended_Real Indicator_Function
     9 begin
    10 
    11 lemma ereal_ineq_diff_add:
    12   assumes "b \<noteq> (-\<infinity>::ereal)" "a \<ge> b"
    13   shows "a = b + (a-b)"
    14 by (metis add.commute assms ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
    15 
    16 lemma Limsup_const_add:
    17   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
    18   shows "F \<noteq> bot \<Longrightarrow> Limsup F (\<lambda>x. c + f x) = c + Limsup F f"
    19   by (rule Limsup_compose_continuous_mono)
    20      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
    21 
    22 lemma Liminf_const_add:
    23   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
    24   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. c + f x) = c + Liminf F f"
    25   by (rule Liminf_compose_continuous_mono)
    26      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
    27 
    28 lemma Liminf_add_const:
    29   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
    30   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. f x + c) = Liminf F f + c"
    31   by (rule Liminf_compose_continuous_mono)
    32      (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
    33 
    34 lemma sums_offset:
    35   fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
    36   assumes "(\<lambda>n. f (n + i)) sums l" shows "f sums (l + (\<Sum>j<i. f j))"
    37 proof  -
    38   have "(\<lambda>k. (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
    39     using assms by (auto intro!: tendsto_add simp: sums_def)
    40   moreover
    41   { fix k :: nat
    42     have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
    43       by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
    44     also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
    45       unfolding image_add_atLeastLessThan by simp
    46     finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
    47       by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
    48   ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"
    49     by simp
    50   then show ?thesis
    51     unfolding sums_def by (rule LIMSEQ_offset)
    52 qed
    53 
    54 lemma suminf_offset:
    55   fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
    56   shows "summable (\<lambda>j. f (j + i)) \<Longrightarrow> suminf f = (\<Sum>j. f (j + i)) + (\<Sum>j<i. f j)"
    57   by (intro sums_unique[symmetric] sums_offset summable_sums)
    58 
    59 lemma eventually_at_left_1: "(\<And>z::real. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> P z) \<Longrightarrow> eventually P (at_left 1)"
    60   by (subst eventually_at_left[of 0]) (auto intro: exI[of _ 0])
    61 
    62 lemma mult_eq_1:
    63   fixes a b :: "'a :: {ordered_semiring, comm_monoid_mult}"
    64   shows "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b = 1 \<longleftrightarrow> (a = 1 \<and> b = 1)"
    65   by (metis mult.left_neutral eq_iff mult.commute mult_right_mono)
    66 
    67 lemma ereal_add_diff_cancel:
    68   fixes a b :: ereal
    69   shows "\<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
    70   by (cases a b rule: ereal2_cases) auto
    71 
    72 lemma add_top:
    73   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
    74   shows "0 \<le> x \<Longrightarrow> x + top = top"
    75   by (intro top_le add_increasing order_refl)
    76 
    77 lemma top_add:
    78   fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
    79   shows "0 \<le> x \<Longrightarrow> top + x = top"
    80   by (intro top_le add_increasing2 order_refl)
    81 
    82 lemma le_lfp: "mono f \<Longrightarrow> x \<le> lfp f \<Longrightarrow> f x \<le> lfp f"
    83   by (subst lfp_unfold) (auto dest: monoD)
    84 
    85 lemma lfp_transfer:
    86   assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and mg: "mono g"
    87   assumes bot: "\<alpha> bot \<le> lfp g" and eq: "\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
    88   shows "\<alpha> (lfp f) = lfp g"
    89 proof (rule antisym)
    90   note mf = sup_continuous_mono[OF f]
    91   have f_le_lfp: "(f ^^ i) bot \<le> lfp f" for i
    92     by (induction i) (auto intro: le_lfp mf)
    93 
    94   have "\<alpha> ((f ^^ i) bot) \<le> lfp g" for i
    95     by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
    96   then show "\<alpha> (lfp f) \<le> lfp g"
    97     unfolding sup_continuous_lfp[OF f]
    98     by (subst \<alpha>[THEN sup_continuousD])
    99        (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
   100 
   101   show "lfp g \<le> \<alpha> (lfp f)"
   102     by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
   103 qed
   104 
   105 lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"
   106   using sup_continuous_apply[THEN sup_continuous_compose] .
   107 
   108 lemma sup_continuous_SUP[order_continuous_intros]:
   109   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   110   assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
   111   shows  "sup_continuous (SUP i:I. M i)"
   112   unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
   113 
   114 lemma sup_continuous_apply_SUP[order_continuous_intros]:
   115   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   116   shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
   117   unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
   118 
   119 lemma sup_continuous_lfp'[order_continuous_intros]:
   120   assumes 1: "sup_continuous f"
   121   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (f g)"
   122   shows "sup_continuous (lfp f)"
   123 proof -
   124   have "sup_continuous ((f ^^ i) bot)" for i
   125   proof (induction i)
   126     case (Suc i) then show ?case
   127       by (auto intro!: 2)
   128   qed (simp add: bot_fun_def sup_continuous_const)
   129   then show ?thesis
   130     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
   131 qed
   132 
   133 lemma sup_continuous_lfp''[order_continuous_intros]:
   134   assumes 1: "\<And>s. sup_continuous (f s)"
   135   assumes 2: "\<And>g. sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>s. f s (g s))"
   136   shows "sup_continuous (\<lambda>x. lfp (f x))"
   137 proof -
   138   have "sup_continuous (\<lambda>x. (f x ^^ i) bot)" for i
   139   proof (induction i)
   140     case (Suc i) then show ?case
   141       by (auto intro!: 2)
   142   qed (simp add: bot_fun_def sup_continuous_const)
   143   then show ?thesis
   144     unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
   145 qed
   146 
   147 lemma mono_INF_fun:
   148     "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y : X x. F x y z :: 'a :: complete_lattice)"
   149   by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
   150 
   151 lemma continuous_on_max:
   152   fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
   153   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
   154   by (auto simp: continuous_on_def intro!: tendsto_max)
   155 
   156 lemma continuous_on_cmult_ereal:
   157   "\<bar>c::ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
   158   using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
   159   by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)
   160 
   161 lemma real_of_nat_Sup:
   162   assumes "A \<noteq> {}" "bdd_above A"
   163   shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
   164 proof (intro antisym)
   165   show "(SUP a:A. of_nat a::real) \<le> of_nat (Sup A)"
   166     using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
   167   have "Sup A \<in> A"
   168     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
   169   then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::real)"
   170     by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
   171 qed
   172 
   173 lemma (in complete_lattice) SUP_sup_const1:
   174   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
   175   using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
   176 
   177 lemma (in complete_lattice) SUP_sup_const2:
   178   "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
   179   using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
   180 
   181 lemma one_less_of_natD:
   182   "(1::'a::linordered_semidom) < of_nat n \<Longrightarrow> 1 < n"
   183   using zero_le_one[where 'a='a]
   184   apply (cases n)
   185   apply simp
   186   subgoal for n'
   187     apply (cases n')
   188     apply simp
   189     apply simp
   190     done
   191   done
   192 
   193 lemma sum_le_suminf:
   194   fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   195   shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
   196   by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
   197 
   198 lemma suminf_eq_SUP_real:
   199   assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
   200   by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
   201      (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
   202 
   203 subsection \<open>Defining the extended non-negative reals\<close>
   204 
   205 text \<open>Basic definitions and type class setup\<close>
   206 
   207 typedef ennreal = "{x :: ereal. 0 \<le> x}"
   208   morphisms enn2ereal e2ennreal'
   209   by auto
   210 
   211 definition "e2ennreal x = e2ennreal' (max 0 x)"
   212 
   213 lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
   214 proof -
   215   have "\<exists>y\<ge>0. x = e2ennreal y" for x
   216     by (cases x) (auto simp: e2ennreal_def max_absorb2)
   217   then show ?thesis
   218     by (auto simp: image_iff Bex_def)
   219 qed
   220 
   221 lemma type_definition_ennreal': "type_definition enn2ereal e2ennreal {x. 0 \<le> x}"
   222   using type_definition_ennreal
   223   by (auto simp: type_definition_def e2ennreal_def max_absorb2)
   224 
   225 setup_lifting type_definition_ennreal'
   226 
   227 declare [[coercion e2ennreal]]
   228 
   229 instantiation ennreal :: complete_linorder
   230 begin
   231 
   232 lift_definition top_ennreal :: ennreal is top by (rule top_greatest)
   233 lift_definition bot_ennreal :: ennreal is 0 by (rule order_refl)
   234 lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (rule le_supI1)
   235 lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (rule le_infI)
   236 
   237 lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
   238   by (rule Inf_greatest)
   239 
   240 lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
   241   by auto
   242 
   243 lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "(\<le>)" .
   244 lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "(<)" .
   245 
   246 instance
   247   by standard
   248      (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
   249 
   250 end
   251 
   252 lemma pcr_ennreal_enn2ereal[simp]: "pcr_ennreal (enn2ereal x) x"
   253   by (simp add: ennreal.pcr_cr_eq cr_ennreal_def)
   254 
   255 lemma rel_fun_eq_pcr_ennreal: "rel_fun (=) pcr_ennreal f g \<longleftrightarrow> f = enn2ereal \<circ> g"
   256   by (auto simp: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
   257 
   258 instantiation ennreal :: infinity
   259 begin
   260 
   261 definition infinity_ennreal :: ennreal
   262 where
   263   [simp]: "\<infinity> = (top::ennreal)"
   264 
   265 instance ..
   266 
   267 end
   268 
   269 instantiation ennreal :: "{semiring_1_no_zero_divisors, comm_semiring_1}"
   270 begin
   271 
   272 lift_definition one_ennreal :: ennreal is 1 by simp
   273 lift_definition zero_ennreal :: ennreal is 0 by simp
   274 lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(+)" by simp
   275 lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "( * )" by simp
   276 
   277 instance
   278   by standard (transfer; auto simp: field_simps ereal_right_distrib)+
   279 
   280 end
   281 
   282 instantiation ennreal :: minus
   283 begin
   284 
   285 lift_definition minus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "\<lambda>a b. max 0 (a - b)"
   286   by simp
   287 
   288 instance ..
   289 
   290 end
   291 
   292 instance ennreal :: numeral ..
   293 
   294 instantiation ennreal :: inverse
   295 begin
   296 
   297 lift_definition inverse_ennreal :: "ennreal \<Rightarrow> ennreal" is inverse
   298   by (rule inverse_ereal_ge0I)
   299 
   300 definition divide_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal"
   301   where "x div y = x * inverse (y :: ennreal)"
   302 
   303 instance ..
   304 
   305 end
   306 
   307 lemma ennreal_zero_less_one: "0 < (1::ennreal)" \<comment> \<open>TODO: remove\<close>
   308   by transfer auto
   309 
   310 instance ennreal :: dioid
   311 proof (standard; transfer)
   312   fix a b :: ereal assume "0 \<le> a" "0 \<le> b" then show "(a \<le> b) = (\<exists>c\<in>Collect ((\<le>) 0). b = a + c)"
   313     unfolding ereal_ex_split Bex_def
   314     by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
   315 qed
   316 
   317 instance ennreal :: ordered_comm_semiring
   318   by standard
   319      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
   320 
   321 instance ennreal :: linordered_nonzero_semiring
   322 proof
   323   fix a b::ennreal
   324   show "a < b \<Longrightarrow> a + 1 < b + 1"
   325     by transfer (simp add: add_right_mono ereal_add_cancel_right less_le)
   326 qed (transfer; simp)
   327 
   328 instance ennreal :: strict_ordered_ab_semigroup_add
   329 proof
   330   fix a b c d :: ennreal show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   331     by transfer (auto intro!: ereal_add_strict_mono)
   332 qed
   333 
   334 declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
   335 
   336 lemma e2ennreal_neg: "x \<le> 0 \<Longrightarrow> e2ennreal x = 0"
   337   unfolding zero_ennreal_def e2ennreal_def by (simp add: max_absorb1)
   338 
   339 lemma e2ennreal_mono: "x \<le> y \<Longrightarrow> e2ennreal x \<le> e2ennreal y"
   340   by (cases "0 \<le> x" "0 \<le> y" rule: bool.exhaust[case_product bool.exhaust])
   341      (auto simp: e2ennreal_neg less_eq_ennreal.abs_eq eq_onp_def)
   342 
   343 lemma enn2ereal_nonneg[simp]: "0 \<le> enn2ereal x"
   344   using ennreal.enn2ereal[of x] by simp
   345 
   346 lemma ereal_ennreal_cases:
   347   obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0"
   348   using e2ennreal'_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
   349 
   350 lemma rel_fun_liminf[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal liminf liminf"
   351 proof -
   352   have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
   353     unfolding liminf_SUP_INF[abs_def] by (transfer_prover_start, transfer_step+; simp)
   354   then show ?thesis
   355     apply (subst (asm) (2) rel_fun_def)
   356     apply (subst (2) rel_fun_def)
   357     apply (auto simp: comp_def max.absorb2 Liminf_bounded rel_fun_eq_pcr_ennreal)
   358     done
   359 qed
   360 
   361 lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
   362 proof -
   363   have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i:{n..}. x i)) limsup"
   364     unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
   365   then show ?thesis
   366     unfolding limsup_INF_SUP[abs_def]
   367     apply (subst (asm) (2) rel_fun_def)
   368     apply (subst (2) rel_fun_def)
   369     apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
   370     apply (subst (asm) max.absorb2)
   371     apply (rule SUP_upper2)
   372     apply auto
   373     done
   374 qed
   375 
   376 lemma sum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (sum f I)"
   377   by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg zero_ennreal.rep_eq plus_ennreal.rep_eq)
   378 
   379 lemma transfer_e2ennreal_sum [transfer_rule]:
   380   "rel_fun (rel_fun (=) pcr_ennreal) (rel_fun (=) pcr_ennreal) sum sum"
   381   by (auto intro!: rel_funI simp: rel_fun_eq_pcr_ennreal comp_def)
   382 
   383 lemma enn2ereal_of_nat[simp]: "enn2ereal (of_nat n) = ereal n"
   384   by (induction n) (auto simp: zero_ennreal.rep_eq one_ennreal.rep_eq plus_ennreal.rep_eq)
   385 
   386 lemma enn2ereal_numeral[simp]: "enn2ereal (numeral a) = numeral a"
   387   apply (subst of_nat_numeral[of a, symmetric])
   388   apply (subst enn2ereal_of_nat)
   389   apply simp
   390   done
   391 
   392 lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
   393   unfolding cr_ennreal_def pcr_ennreal_def by auto
   394 
   395 subsection \<open>Cancellation simprocs\<close>
   396 
   397 lemma ennreal_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b = c"
   398   unfolding infinity_ennreal_def by transfer (simp add: top_ereal_def ereal_add_cancel_left)
   399 
   400 lemma ennreal_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::ennreal) \<or> b \<le> c"
   401   unfolding infinity_ennreal_def by transfer (simp add: ereal_add_le_add_iff top_ereal_def disj_commute)
   402 
   403 lemma ereal_add_left_cancel_less:
   404   fixes a b c :: ereal
   405   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b < a + c \<longleftrightarrow> a \<noteq> \<infinity> \<and> b < c"
   406   by (cases a b c rule: ereal3_cases) auto
   407 
   408 lemma ennreal_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::ennreal) \<and> b < c"
   409   unfolding infinity_ennreal_def
   410   by transfer (simp add: top_ereal_def ereal_add_left_cancel_less)
   411 
   412 ML \<open>
   413 structure Cancel_Ennreal_Common =
   414 struct
   415   (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
   416   fun find_first_t _    _ []         = raise TERM("find_first_t", [])
   417     | find_first_t past u (t::terms) =
   418           if u aconv t then (rev past @ terms)
   419           else find_first_t (t::past) u terms
   420 
   421   fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
   422         dest_summing (t, dest_summing (u, ts))
   423     | dest_summing (t, ts) = t :: ts
   424 
   425   val mk_sum = Arith_Data.long_mk_sum
   426   fun dest_sum t = dest_summing (t, [])
   427   val find_first = find_first_t []
   428   val trans_tac = Numeral_Simprocs.trans_tac
   429   val norm_ss =
   430     simpset_of (put_simpset HOL_basic_ss @{context}
   431       addsimps @{thms ac_simps add_0_left add_0_right})
   432   fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   433   fun simplify_meta_eq ctxt cancel_th th =
   434     Arith_Data.simplify_meta_eq [] ctxt
   435       ([th, cancel_th] MRS trans)
   436   fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
   437 end
   438 
   439 structure Eq_Ennreal_Cancel = ExtractCommonTermFun
   440 (open Cancel_Ennreal_Common
   441   val mk_bal = HOLogic.mk_eq
   442   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ ennreal}
   443   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel}
   444 )
   445 
   446 structure Le_Ennreal_Cancel = ExtractCommonTermFun
   447 (open Cancel_Ennreal_Common
   448   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   449   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ ennreal}
   450   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_le}
   451 )
   452 
   453 structure Less_Ennreal_Cancel = ExtractCommonTermFun
   454 (open Cancel_Ennreal_Common
   455   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
   456   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ ennreal}
   457   fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_less}
   458 )
   459 \<close>
   460 
   461 simproc_setup ennreal_eq_cancel
   462   ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
   463   \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   464 
   465 simproc_setup ennreal_le_cancel
   466   ("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
   467   \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   468 
   469 simproc_setup ennreal_less_cancel
   470   ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
   471   \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
   472 
   473 
   474 subsection \<open>Order with top\<close>
   475 
   476 lemma ennreal_zero_less_top[simp]: "0 < (top::ennreal)"
   477   by transfer (simp add: top_ereal_def)
   478 
   479 lemma ennreal_one_less_top[simp]: "1 < (top::ennreal)"
   480   by transfer (simp add: top_ereal_def)
   481 
   482 lemma ennreal_zero_neq_top[simp]: "0 \<noteq> (top::ennreal)"
   483   by transfer (simp add: top_ereal_def)
   484 
   485 lemma ennreal_top_neq_zero[simp]: "(top::ennreal) \<noteq> 0"
   486   by transfer (simp add: top_ereal_def)
   487 
   488 lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
   489   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
   490 
   491 lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
   492   by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
   493 
   494 lemma ennreal_add_less_top[simp]:
   495   fixes a b :: ennreal
   496   shows "a + b < top \<longleftrightarrow> a < top \<and> b < top"
   497   by transfer (auto simp: top_ereal_def)
   498 
   499 lemma ennreal_add_eq_top[simp]:
   500   fixes a b :: ennreal
   501   shows "a + b = top \<longleftrightarrow> a = top \<or> b = top"
   502   by transfer (auto simp: top_ereal_def)
   503 
   504 lemma ennreal_sum_less_top[simp]:
   505   fixes f :: "'a \<Rightarrow> ennreal"
   506   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) < top \<longleftrightarrow> (\<forall>i\<in>I. f i < top)"
   507   by (induction I rule: finite_induct) auto
   508 
   509 lemma ennreal_sum_eq_top[simp]:
   510   fixes f :: "'a \<Rightarrow> ennreal"
   511   shows "finite I \<Longrightarrow> (\<Sum>i\<in>I. f i) = top \<longleftrightarrow> (\<exists>i\<in>I. f i = top)"
   512   by (induction I rule: finite_induct) auto
   513 
   514 lemma ennreal_mult_eq_top_iff:
   515   fixes a b :: ennreal
   516   shows "a * b = top \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
   517   by transfer (auto simp: top_ereal_def)
   518 
   519 lemma ennreal_top_eq_mult_iff:
   520   fixes a b :: ennreal
   521   shows "top = a * b \<longleftrightarrow> (a = top \<and> b \<noteq> 0) \<or> (b = top \<and> a \<noteq> 0)"
   522   using ennreal_mult_eq_top_iff[of a b] by auto
   523 
   524 lemma ennreal_mult_less_top:
   525   fixes a b :: ennreal
   526   shows "a * b < top \<longleftrightarrow> (a = 0 \<or> b = 0 \<or> (a < top \<and> b < top))"
   527   by transfer (auto simp add: top_ereal_def)
   528 
   529 lemma top_power_ennreal: "top ^ n = (if n = 0 then 1 else top :: ennreal)"
   530   by (induction n) (simp_all add: ennreal_mult_eq_top_iff)
   531 
   532 lemma ennreal_prod_eq_0[simp]:
   533   fixes f :: "'a \<Rightarrow> ennreal"
   534   shows "(prod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
   535   by (induction A rule: infinite_finite_induct) auto
   536 
   537 lemma ennreal_prod_eq_top:
   538   fixes f :: "'a \<Rightarrow> ennreal"
   539   shows "(\<Prod>i\<in>I. f i) = top \<longleftrightarrow> (finite I \<and> ((\<forall>i\<in>I. f i \<noteq> 0) \<and> (\<exists>i\<in>I. f i = top)))"
   540   by (induction I rule: infinite_finite_induct) (auto simp: ennreal_mult_eq_top_iff)
   541 
   542 lemma ennreal_top_mult: "top * a = (if a = 0 then 0 else top :: ennreal)"
   543   by (simp add: ennreal_mult_eq_top_iff)
   544 
   545 lemma ennreal_mult_top: "a * top = (if a = 0 then 0 else top :: ennreal)"
   546   by (simp add: ennreal_mult_eq_top_iff)
   547 
   548 lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \<infinity> \<longleftrightarrow> x = top"
   549   by transfer (simp add: top_ereal_def)
   550 
   551 lemma enn2ereal_top[simp]: "enn2ereal top = \<infinity>"
   552   by transfer (simp add: top_ereal_def)
   553 
   554 lemma e2ennreal_infty[simp]: "e2ennreal \<infinity> = top"
   555   by (simp add: top_ennreal.abs_eq top_ereal_def)
   556 
   557 lemma ennreal_top_minus[simp]: "top - x = (top::ennreal)"
   558   by transfer (auto simp: top_ereal_def max_def)
   559 
   560 lemma minus_top_ennreal: "x - top = (if x = top then top else 0:: ennreal)"
   561   apply transfer
   562   subgoal for x
   563     by (cases x) (auto simp: top_ereal_def max_def)
   564   done
   565 
   566 lemma bot_ennreal: "bot = (0::ennreal)"
   567   by transfer rule
   568 
   569 lemma ennreal_of_nat_neq_top[simp]: "of_nat i \<noteq> (top::ennreal)"
   570   by (induction i) auto
   571 
   572 lemma numeral_eq_of_nat: "(numeral a::ennreal) = of_nat (numeral a)"
   573   by simp
   574 
   575 lemma of_nat_less_top: "of_nat i < (top::ennreal)"
   576   using less_le_trans[of "of_nat i" "of_nat (Suc i)" "top::ennreal"]
   577   by simp
   578 
   579 lemma top_neq_numeral[simp]: "top \<noteq> (numeral i::ennreal)"
   580   using of_nat_less_top[of "numeral i"] by simp
   581 
   582 lemma ennreal_numeral_less_top[simp]: "numeral i < (top::ennreal)"
   583   using of_nat_less_top[of "numeral i"] by simp
   584 
   585 lemma ennreal_add_bot[simp]: "bot + x = (x::ennreal)"
   586   by transfer simp
   587 
   588 instance ennreal :: semiring_char_0
   589 proof (standard, safe intro!: linorder_injI)
   590   have *: "1 + of_nat k \<noteq> (0::ennreal)" for k
   591     using add_pos_nonneg[OF zero_less_one, of "of_nat k :: ennreal"] by auto
   592   fix x y :: nat assume "x < y" "of_nat x = (of_nat y::ennreal)" then show False
   593     by (auto simp add: less_iff_Suc_add *)
   594 qed
   595 
   596 subsection \<open>Arithmetic\<close>
   597 
   598 lemma ennreal_minus_zero[simp]: "a - (0::ennreal) = a"
   599   by transfer (auto simp: max_def)
   600 
   601 lemma ennreal_add_diff_cancel_right[simp]:
   602   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (x + y) - y = x"
   603   apply transfer
   604   subgoal for x y
   605     apply (cases x y rule: ereal2_cases)
   606     apply (auto split: split_max simp: top_ereal_def)
   607     done
   608   done
   609 
   610 lemma ennreal_add_diff_cancel_left[simp]:
   611   fixes x y z :: ennreal shows "y \<noteq> top \<Longrightarrow> (y + x) - y = x"
   612   by (simp add: add.commute)
   613 
   614 lemma
   615   fixes a b :: ennreal
   616   shows "a - b = 0 \<Longrightarrow> a \<le> b"
   617   apply transfer
   618   subgoal for a b
   619     apply (cases a b rule: ereal2_cases)
   620     apply (auto simp: not_le max_def split: if_splits)
   621     done
   622   done
   623 
   624 lemma ennreal_minus_cancel:
   625   fixes a b c :: ennreal
   626   shows "c \<noteq> top \<Longrightarrow> a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a = c - b \<Longrightarrow> a = b"
   627   apply transfer
   628   subgoal for a b c
   629     by (cases a b c rule: ereal3_cases)
   630        (auto simp: top_ereal_def max_def split: if_splits)
   631   done
   632 
   633 lemma sup_const_add_ennreal:
   634   fixes a b c :: "ennreal"
   635   shows "sup (c + a) (c + b) = c + sup a b"
   636   apply transfer
   637   subgoal for a b c
   638     apply (cases a b c rule: ereal3_cases)
   639     apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
   640     done
   641   done
   642 
   643 lemma ennreal_diff_add_assoc:
   644   fixes a b c :: ennreal
   645   shows "a \<le> b \<Longrightarrow> c + b - a = c + (b - a)"
   646   apply transfer
   647   subgoal for a b c
   648     by (cases a b c rule: ereal3_cases) (auto simp: field_simps max_absorb2)
   649   done
   650 
   651 lemma mult_divide_eq_ennreal:
   652   fixes a b :: ennreal
   653   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
   654   unfolding divide_ennreal_def
   655   apply transfer
   656   apply (subst mult.assoc)
   657   apply (simp add: top_ereal_def divide_ereal_def[symmetric])
   658   done
   659 
   660 lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
   661   unfolding divide_ennreal_def infinity_ennreal_def
   662   apply transfer
   663   subgoal for a b c
   664     apply (cases a b c rule: ereal3_cases)
   665     apply (auto simp: top_ereal_def)
   666     done
   667   done
   668 
   669 lemma ennreal_mult_divide_eq:
   670   fixes a b :: ennreal
   671   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
   672   unfolding divide_ennreal_def
   673   apply transfer
   674   apply (subst mult.assoc)
   675   apply (simp add: top_ereal_def divide_ereal_def[symmetric])
   676   done
   677 
   678 lemma ennreal_add_diff_cancel:
   679   fixes a b :: ennreal
   680   shows "b \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
   681   unfolding infinity_ennreal_def
   682   by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)
   683 
   684 lemma ennreal_minus_eq_0:
   685   "a - b = 0 \<Longrightarrow> a \<le> (b::ennreal)"
   686   apply transfer
   687   subgoal for a b
   688     apply (cases a b rule: ereal2_cases)
   689     apply (auto simp: zero_ereal_def ereal_max[symmetric] max.absorb2 simp del: ereal_max)
   690     done
   691   done
   692 
   693 lemma ennreal_mono_minus_cancel:
   694   fixes a b c :: ennreal
   695   shows "a - b \<le> a - c \<Longrightarrow> a < top \<Longrightarrow> b \<le> a \<Longrightarrow> c \<le> a \<Longrightarrow> c \<le> b"
   696   by transfer
   697      (auto simp add: max.absorb2 ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
   698 
   699 lemma ennreal_mono_minus:
   700   fixes a b c :: ennreal
   701   shows "c \<le> b \<Longrightarrow> a - b \<le> a - c"
   702   apply transfer
   703   apply (rule max.mono)
   704   apply simp
   705   subgoal for a b c
   706     by (cases a b c rule: ereal3_cases) auto
   707   done
   708 
   709 lemma ennreal_minus_pos_iff:
   710   fixes a b :: ennreal
   711   shows "a < top \<or> b < top \<Longrightarrow> 0 < a - b \<Longrightarrow> b < a"
   712   apply transfer
   713   subgoal for a b
   714     by (cases a b rule: ereal2_cases) (auto simp: less_max_iff_disj)
   715   done
   716 
   717 lemma ennreal_inverse_top[simp]: "inverse top = (0::ennreal)"
   718   by transfer (simp add: top_ereal_def ereal_inverse_eq_0)
   719 
   720 lemma ennreal_inverse_zero[simp]: "inverse 0 = (top::ennreal)"
   721   by transfer (simp add: top_ereal_def ereal_inverse_eq_0)
   722 
   723 lemma ennreal_top_divide: "top / (x::ennreal) = (if x = top then 0 else top)"
   724   unfolding divide_ennreal_def
   725   by transfer (simp add: top_ereal_def ereal_inverse_eq_0 ereal_0_gt_inverse)
   726 
   727 lemma ennreal_zero_divide[simp]: "0 / (x::ennreal) = 0"
   728   by (simp add: divide_ennreal_def)
   729 
   730 lemma ennreal_divide_zero[simp]: "x / (0::ennreal) = (if x = 0 then 0 else top)"
   731   by (simp add: divide_ennreal_def ennreal_mult_top)
   732 
   733 lemma ennreal_divide_top[simp]: "x / (top::ennreal) = 0"
   734   by (simp add: divide_ennreal_def ennreal_top_mult)
   735 
   736 lemma ennreal_times_divide: "a * (b / c) = a * b / (c::ennreal)"
   737   unfolding divide_ennreal_def
   738   by transfer (simp add: divide_ereal_def[symmetric] ereal_times_divide_eq)
   739 
   740 lemma ennreal_zero_less_divide: "0 < a / b \<longleftrightarrow> (0 < a \<and> b < (top::ennreal))"
   741   unfolding divide_ennreal_def
   742   by transfer (auto simp: ereal_zero_less_0_iff top_ereal_def ereal_0_gt_inverse)
   743 
   744 lemma divide_right_mono_ennreal:
   745   fixes a b c :: ennreal
   746   shows "a \<le> b \<Longrightarrow> a / c \<le> b / c"
   747   unfolding divide_ennreal_def by (intro mult_mono) auto
   748 
   749 lemma ennreal_mult_strict_right_mono: "(a::ennreal) < c \<Longrightarrow> 0 < b \<Longrightarrow> b < top \<Longrightarrow> a * b < c * b"
   750   by transfer (auto intro!: ereal_mult_strict_right_mono)
   751 
   752 lemma ennreal_indicator_less[simp]:
   753   "indicator A x \<le> (indicator B x::ennreal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
   754   by (simp add: indicator_def not_le)
   755 
   756 lemma ennreal_inverse_positive: "0 < inverse x \<longleftrightarrow> (x::ennreal) \<noteq> top"
   757   by transfer (simp add: ereal_0_gt_inverse top_ereal_def)
   758 
   759 lemma ennreal_inverse_mult': "((0 < b \<or> a < top) \<and> (0 < a \<or> b < top)) \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
   760   apply transfer
   761   subgoal for a b
   762     by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
   763   done
   764 
   765 lemma ennreal_inverse_mult: "a < top \<Longrightarrow> b < top \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
   766   apply transfer
   767   subgoal for a b
   768     by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
   769   done
   770 
   771 lemma ennreal_inverse_1[simp]: "inverse (1::ennreal) = 1"
   772   by transfer simp
   773 
   774 lemma ennreal_inverse_eq_0_iff[simp]: "inverse (a::ennreal) = 0 \<longleftrightarrow> a = top"
   775   by transfer (simp add: ereal_inverse_eq_0 top_ereal_def)
   776 
   777 lemma ennreal_inverse_eq_top_iff[simp]: "inverse (a::ennreal) = top \<longleftrightarrow> a = 0"
   778   by transfer (simp add: top_ereal_def)
   779 
   780 lemma ennreal_divide_eq_0_iff[simp]: "(a::ennreal) / b = 0 \<longleftrightarrow> (a = 0 \<or> b = top)"
   781   by (simp add: divide_ennreal_def)
   782 
   783 lemma ennreal_divide_eq_top_iff: "(a::ennreal) / b = top \<longleftrightarrow> ((a \<noteq> 0 \<and> b = 0) \<or> (a = top \<and> b \<noteq> top))"
   784   by (auto simp add: divide_ennreal_def ennreal_mult_eq_top_iff)
   785 
   786 lemma one_divide_one_divide_ennreal[simp]: "1 / (1 / c) = (c::ennreal)"
   787   including ennreal.lifting
   788   unfolding divide_ennreal_def
   789   by transfer auto
   790 
   791 lemma ennreal_mult_left_cong:
   792   "((a::ennreal) \<noteq> 0 \<Longrightarrow> b = c) \<Longrightarrow> a * b = a * c"
   793   by (cases "a = 0") simp_all
   794 
   795 lemma ennreal_mult_right_cong:
   796   "((a::ennreal) \<noteq> 0 \<Longrightarrow> b = c) \<Longrightarrow> b * a = c * a"
   797   by (cases "a = 0") simp_all
   798 
   799 lemma ennreal_zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < (b::ennreal)"
   800   by transfer (auto simp add: ereal_zero_less_0_iff le_less)
   801 
   802 lemma less_diff_eq_ennreal:
   803   fixes a b c :: ennreal
   804   shows "b < top \<or> c < top \<Longrightarrow> a < b - c \<longleftrightarrow> a + c < b"
   805   apply transfer
   806   subgoal for a b c
   807     by (cases a b c rule: ereal3_cases) (auto split: split_max)
   808   done
   809 
   810 lemma diff_add_cancel_ennreal:
   811   fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b - a + a = b"
   812   unfolding infinity_ennreal_def
   813   apply transfer
   814   subgoal for a b
   815     by (cases a b rule: ereal2_cases) (auto simp: max_absorb2)
   816   done
   817 
   818 lemma ennreal_diff_self[simp]: "a \<noteq> top \<Longrightarrow> a - a = (0::ennreal)"
   819   by transfer (simp add: top_ereal_def)
   820 
   821 lemma ennreal_minus_mono:
   822   fixes a b c :: ennreal
   823   shows "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> c - d"
   824   apply transfer
   825   apply (rule max.mono)
   826   apply simp
   827   subgoal for a b c d
   828     by (cases a b c d rule: ereal3_cases[case_product ereal_cases]) auto
   829   done
   830 
   831 lemma ennreal_minus_eq_top[simp]: "a - (b::ennreal) = top \<longleftrightarrow> a = top"
   832   by transfer (auto simp: top_ereal_def max.absorb2 ereal_minus_eq_PInfty_iff split: split_max)
   833 
   834 lemma ennreal_divide_self[simp]: "a \<noteq> 0 \<Longrightarrow> a < top \<Longrightarrow> a / a = (1::ennreal)"
   835   unfolding divide_ennreal_def
   836   apply transfer
   837   subgoal for a
   838     by (cases a) (auto simp: top_ereal_def)
   839   done
   840 
   841 subsection \<open>Coercion from @{typ real} to @{typ ennreal}\<close>
   842 
   843 lift_definition ennreal :: "real \<Rightarrow> ennreal" is "sup 0 \<circ> ereal"
   844   by simp
   845 
   846 declare [[coercion ennreal]]
   847 
   848 lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" by simp
   849 
   850 lemma ennreal_cases[cases type: ennreal]:
   851   fixes x :: ennreal
   852   obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
   853   apply transfer
   854   subgoal for x thesis
   855     by (cases x) (auto simp: max.absorb2 top_ereal_def)
   856   done
   857 
   858 lemmas ennreal2_cases = ennreal_cases[case_product ennreal_cases]
   859 lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]
   860 
   861 lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
   862   by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
   863 
   864 lemma top_neq_ennreal[simp]: "top \<noteq> ennreal r"
   865   using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)
   866 
   867 lemma ennreal_less_top[simp]: "ennreal x < top"
   868   by transfer (simp add: top_ereal_def max_def)
   869 
   870 lemma ennreal_neg: "x \<le> 0 \<Longrightarrow> ennreal x = 0"
   871   by transfer (simp add: max.absorb1)
   872 
   873 lemma ennreal_inj[simp]:
   874   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal a = ennreal b \<longleftrightarrow> a = b"
   875   by (transfer fixing: a b) (auto simp: max_absorb2)
   876 
   877 lemma ennreal_le_iff[simp]: "0 \<le> y \<Longrightarrow> ennreal x \<le> ennreal y \<longleftrightarrow> x \<le> y"
   878   by (auto simp: ennreal_def zero_ereal_def less_eq_ennreal.abs_eq eq_onp_def split: split_max)
   879 
   880 lemma le_ennreal_iff: "0 \<le> r \<Longrightarrow> x \<le> ennreal r \<longleftrightarrow> (\<exists>q\<ge>0. x = ennreal q \<and> q \<le> r)"
   881   by (cases x) (auto simp: top_unique)
   882 
   883 lemma ennreal_less_iff: "0 \<le> r \<Longrightarrow> ennreal r < ennreal q \<longleftrightarrow> r < q"
   884   unfolding not_le[symmetric] by auto
   885 
   886 lemma ennreal_eq_zero_iff[simp]: "0 \<le> x \<Longrightarrow> ennreal x = 0 \<longleftrightarrow> x = 0"
   887   by transfer (auto simp: max_absorb2)
   888 
   889 lemma ennreal_less_zero_iff[simp]: "0 < ennreal x \<longleftrightarrow> 0 < x"
   890   by transfer (auto simp: max_def)
   891 
   892 lemma ennreal_lessI: "0 < q \<Longrightarrow> r < q \<Longrightarrow> ennreal r < ennreal q"
   893   by (cases "0 \<le> r") (auto simp: ennreal_less_iff ennreal_neg)
   894 
   895 lemma ennreal_leI: "x \<le> y \<Longrightarrow> ennreal x \<le> ennreal y"
   896   by (cases "0 \<le> y") (auto simp: ennreal_neg)
   897 
   898 lemma enn2ereal_ennreal[simp]: "0 \<le> x \<Longrightarrow> enn2ereal (ennreal x) = x"
   899   by transfer (simp add: max_absorb2)
   900 
   901 lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
   902   by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
   903 
   904 lemma enn2ereal_e2ennreal: "x \<ge> 0 \<Longrightarrow> enn2ereal (e2ennreal x) = x"
   905 by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)
   906 
   907 lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
   908 by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
   909 
   910 lemma ennreal_0[simp]: "ennreal 0 = 0"
   911   by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
   912 
   913 lemma ennreal_1[simp]: "ennreal 1 = 1"
   914   by transfer (simp add: max_absorb2)
   915 
   916 lemma ennreal_eq_0_iff: "ennreal x = 0 \<longleftrightarrow> x \<le> 0"
   917   by (cases "0 \<le> x") (auto simp: ennreal_neg)
   918 
   919 lemma ennreal_le_iff2: "ennreal x \<le> ennreal y \<longleftrightarrow> ((0 \<le> y \<and> x \<le> y) \<or> (x \<le> 0 \<and> y \<le> 0))"
   920   by (cases "0 \<le> y") (auto simp: ennreal_eq_0_iff ennreal_neg)
   921 
   922 lemma ennreal_eq_1[simp]: "ennreal x = 1 \<longleftrightarrow> x = 1"
   923   by (cases "0 \<le> x")
   924      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
   925 
   926 lemma ennreal_le_1[simp]: "ennreal x \<le> 1 \<longleftrightarrow> x \<le> 1"
   927   by (cases "0 \<le> x")
   928      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
   929 
   930 lemma ennreal_ge_1[simp]: "ennreal x \<ge> 1 \<longleftrightarrow> x \<ge> 1"
   931   by (cases "0 \<le> x")
   932      (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
   933 
   934 lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
   935   by transfer (auto simp: max.absorb2 less_max_iff_disj)
   936 
   937 lemma ennreal_plus[simp]:
   938   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
   939   by (transfer fixing: a b) (auto simp: max_absorb2)
   940 
   941 lemma sum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (sum f I)"
   942   by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg)
   943 
   944 lemma sum_list_ennreal[simp]:
   945   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
   946   shows   "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
   947 using assms
   948 proof (induction xs)
   949   case (Cons x xs)
   950   from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
   951     by simp
   952   also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
   953     by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
   954   finally show ?case by simp
   955 qed simp_all
   956 
   957 lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
   958   by (induction i) simp_all
   959 
   960 lemma of_nat_le_ennreal_iff[simp]: "0 \<le> r \<Longrightarrow> of_nat i \<le> ennreal r \<longleftrightarrow> of_nat i \<le> r"
   961   by (simp add: ennreal_of_nat_eq_real_of_nat)
   962 
   963 lemma ennreal_le_of_nat_iff[simp]: "ennreal r \<le> of_nat i \<longleftrightarrow> r \<le> of_nat i"
   964   by (simp add: ennreal_of_nat_eq_real_of_nat)
   965 
   966 lemma ennreal_indicator: "ennreal (indicator A x) = indicator A x"
   967   by (auto split: split_indicator)
   968 
   969 lemma ennreal_numeral[simp]: "ennreal (numeral n) = numeral n"
   970   using ennreal_of_nat_eq_real_of_nat[of "numeral n"] by simp
   971 
   972 lemma min_ennreal: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> min (ennreal x) (ennreal y) = ennreal (min x y)"
   973   by (auto split: split_min)
   974 
   975 lemma ennreal_half[simp]: "ennreal (1/2) = inverse 2"
   976   by transfer (simp add: max.absorb2)
   977 
   978 lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
   979   by transfer
   980      (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
   981 
   982 lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
   983   by (simp add: minus_top_ennreal)
   984 
   985 lemma e2eenreal_enn2ereal_diff [simp]:
   986   "e2ennreal(enn2ereal x - enn2ereal y) = x - y" for x y
   987 by (cases x, cases y, auto simp add: ennreal_minus e2ennreal_neg)
   988 
   989 lemma ennreal_mult: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
   990   by transfer (simp add: max_absorb2)
   991 
   992 lemma ennreal_mult': "0 \<le> a \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
   993   by (cases "0 \<le> b") (auto simp: ennreal_mult ennreal_neg mult_nonneg_nonpos)
   994 
   995 lemma indicator_mult_ennreal: "indicator A x * ennreal r = ennreal (indicator A x * r)"
   996   by (simp split: split_indicator)
   997 
   998 lemma ennreal_mult'': "0 \<le> b \<Longrightarrow> ennreal (a * b) = ennreal a * ennreal b"
   999   by (cases "0 \<le> a") (auto simp: ennreal_mult ennreal_neg mult_nonpos_nonneg)
  1000 
  1001 lemma numeral_mult_ennreal: "0 \<le> x \<Longrightarrow> numeral b * ennreal x = ennreal (numeral b * x)"
  1002   by (simp add: ennreal_mult)
  1003 
  1004 lemma ennreal_power: "0 \<le> r \<Longrightarrow> ennreal r ^ n = ennreal (r ^ n)"
  1005   by (induction n) (auto simp: ennreal_mult)
  1006 
  1007 lemma power_eq_top_ennreal: "x ^ n = top \<longleftrightarrow> (n \<noteq> 0 \<and> (x::ennreal) = top)"
  1008   by (cases x rule: ennreal_cases)
  1009      (auto simp: ennreal_power top_power_ennreal)
  1010 
  1011 lemma inverse_ennreal: "0 < r \<Longrightarrow> inverse (ennreal r) = ennreal (inverse r)"
  1012   by transfer (simp add: max.absorb2)
  1013 
  1014 lemma divide_ennreal: "0 \<le> r \<Longrightarrow> 0 < q \<Longrightarrow> ennreal r / ennreal q = ennreal (r / q)"
  1015   by (simp add: divide_ennreal_def inverse_ennreal ennreal_mult[symmetric] inverse_eq_divide)
  1016 
  1017 lemma ennreal_inverse_power: "inverse (x ^ n :: ennreal) = inverse x ^ n"
  1018 proof (cases x rule: ennreal_cases)
  1019   case top with power_eq_top_ennreal[of x n] show ?thesis
  1020     by (cases "n = 0") auto
  1021 next
  1022   case (real r) then show ?thesis
  1023   proof cases
  1024     assume "x = 0" then show ?thesis
  1025       using power_eq_top_ennreal[of top "n - 1"]
  1026       by (cases n) (auto simp: ennreal_top_mult)
  1027   next
  1028     assume "x \<noteq> 0"
  1029     with real have "0 < r" by auto
  1030     with real show ?thesis
  1031       by (induction n)
  1032          (auto simp add: ennreal_power ennreal_mult[symmetric] inverse_ennreal)
  1033   qed
  1034 qed
  1035 
  1036 lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
  1037   by (subst divide_ennreal[symmetric]) auto
  1038 
  1039 lemma prod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (prod f A)"
  1040   by (induction A rule: infinite_finite_induct)
  1041      (auto simp: ennreal_mult prod_nonneg)
  1042 
  1043 lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
  1044   apply (cases "0 \<le> c")
  1045   apply (cases a b rule: ennreal2_cases)
  1046   apply (auto simp: ennreal_mult[symmetric] ennreal_neg ennreal_top_mult)
  1047   done
  1048 
  1049 lemma ennreal_le_epsilon:
  1050   "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
  1051   apply (cases y rule: ennreal_cases)
  1052   apply (cases x rule: ennreal_cases)
  1053   apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
  1054     intro: zero_less_one field_le_epsilon)
  1055   done
  1056 
  1057 lemma ennreal_rat_dense:
  1058   fixes x y :: ennreal
  1059   shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
  1060 proof transfer
  1061   fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
  1062   moreover
  1063   from ereal_dense3[OF \<open>x < y\<close>]
  1064   obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
  1065     by auto
  1066   then have "0 \<le> r"
  1067     using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
  1068   with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
  1069     by (intro exI[of _ r]) (auto simp: max_absorb2)
  1070 qed
  1071 
  1072 lemma ennreal_Ex_less_of_nat: "(x::ennreal) < top \<Longrightarrow> \<exists>n. x < of_nat n"
  1073   by (cases x rule: ennreal_cases)
  1074      (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_less_iff reals_Archimedean2)
  1075 
  1076 subsection \<open>Coercion from @{typ ennreal} to @{typ real}\<close>
  1077 
  1078 definition "enn2real x = real_of_ereal (enn2ereal x)"
  1079 
  1080 lemma enn2real_nonneg[simp]: "0 \<le> enn2real x"
  1081   by (auto simp: enn2real_def intro!: real_of_ereal_pos enn2ereal_nonneg)
  1082 
  1083 lemma enn2real_mono: "a \<le> b \<Longrightarrow> b < top \<Longrightarrow> enn2real a \<le> enn2real b"
  1084   by (auto simp add: enn2real_def less_eq_ennreal.rep_eq intro!: real_of_ereal_positive_mono enn2ereal_nonneg)
  1085 
  1086 lemma enn2real_of_nat[simp]: "enn2real (of_nat n) = n"
  1087   by (auto simp: enn2real_def)
  1088 
  1089 lemma enn2real_ennreal[simp]: "0 \<le> r \<Longrightarrow> enn2real (ennreal r) = r"
  1090   by (simp add: enn2real_def)
  1091 
  1092 lemma ennreal_enn2real[simp]: "r < top \<Longrightarrow> ennreal (enn2real r) = r"
  1093   by (cases r rule: ennreal_cases) auto
  1094 
  1095 lemma real_of_ereal_enn2ereal[simp]: "real_of_ereal (enn2ereal x) = enn2real x"
  1096   by (simp add: enn2real_def)
  1097 
  1098 lemma enn2real_top[simp]: "enn2real top = 0"
  1099   unfolding enn2real_def top_ennreal.rep_eq top_ereal_def by simp
  1100 
  1101 lemma enn2real_0[simp]: "enn2real 0 = 0"
  1102   unfolding enn2real_def zero_ennreal.rep_eq by simp
  1103 
  1104 lemma enn2real_1[simp]: "enn2real 1 = 1"
  1105   unfolding enn2real_def one_ennreal.rep_eq by simp
  1106 
  1107 lemma enn2real_numeral[simp]: "enn2real (numeral n) = (numeral n)"
  1108   unfolding enn2real_def by simp
  1109 
  1110 lemma enn2real_mult: "enn2real (a * b) = enn2real a * enn2real b"
  1111   unfolding enn2real_def
  1112   by (simp del: real_of_ereal_enn2ereal add: times_ennreal.rep_eq)
  1113 
  1114 lemma enn2real_leI: "0 \<le> B \<Longrightarrow> x \<le> ennreal B \<Longrightarrow> enn2real x \<le> B"
  1115   by (cases x rule: ennreal_cases) (auto simp: top_unique)
  1116 
  1117 lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
  1118   by (cases x rule: ennreal_cases) auto
  1119 
  1120 lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
  1121   by (cases x) auto
  1122 
  1123 subsection \<open>Coercion from @{typ enat} to @{typ ennreal}\<close>
  1124 
  1125 
  1126 definition ennreal_of_enat :: "enat \<Rightarrow> ennreal"
  1127 where
  1128   "ennreal_of_enat n = (case n of \<infinity> \<Rightarrow> top | enat n \<Rightarrow> of_nat n)"
  1129 
  1130 declare [[coercion ennreal_of_enat]]
  1131 declare [[coercion "of_nat :: nat \<Rightarrow> ennreal"]]
  1132 
  1133 lemma ennreal_of_enat_infty[simp]: "ennreal_of_enat \<infinity> = \<infinity>"
  1134   by (simp add: ennreal_of_enat_def)
  1135 
  1136 lemma ennreal_of_enat_enat[simp]: "ennreal_of_enat (enat n) = of_nat n"
  1137   by (simp add: ennreal_of_enat_def)
  1138 
  1139 lemma ennreal_of_enat_0[simp]: "ennreal_of_enat 0 = 0"
  1140   using ennreal_of_enat_enat[of 0] unfolding enat_0 by simp
  1141 
  1142 lemma ennreal_of_enat_1[simp]: "ennreal_of_enat 1 = 1"
  1143   using ennreal_of_enat_enat[of 1] unfolding enat_1 by simp
  1144 
  1145 lemma ennreal_top_neq_of_nat[simp]: "(top::ennreal) \<noteq> of_nat i"
  1146   using ennreal_of_nat_neq_top[of i] by metis
  1147 
  1148 lemma ennreal_of_enat_inj[simp]: "ennreal_of_enat i = ennreal_of_enat j \<longleftrightarrow> i = j"
  1149   by (cases i j rule: enat.exhaust[case_product enat.exhaust]) auto
  1150 
  1151 lemma ennreal_of_enat_le_iff[simp]: "ennreal_of_enat m \<le> ennreal_of_enat n \<longleftrightarrow> m \<le> n"
  1152   by (auto simp: ennreal_of_enat_def top_unique split: enat.split)
  1153 
  1154 lemma of_nat_less_ennreal_of_nat[simp]: "of_nat n \<le> ennreal_of_enat x \<longleftrightarrow> of_nat n \<le> x"
  1155   by (cases x) (auto simp: of_nat_eq_enat)
  1156 
  1157 lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x:X. ennreal_of_enat x)"
  1158 proof -
  1159   have "ennreal_of_enat (Sup X) \<le> (SUP x : X. ennreal_of_enat x)"
  1160     unfolding Sup_enat_def
  1161   proof (clarsimp, intro conjI impI)
  1162     fix x assume "finite X" "X \<noteq> {}"
  1163     then show "ennreal_of_enat (Max X) \<le> (SUP x : X. ennreal_of_enat x)"
  1164       by (intro SUP_upper Max_in)
  1165   next
  1166     assume "infinite X" "X \<noteq> {}"
  1167     have "\<exists>y\<in>X. r < ennreal_of_enat y" if r: "r < top" for r
  1168     proof -
  1169       from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
  1170       have "\<not> (X \<subseteq> enat ` {.. n})"
  1171         using \<open>infinite X\<close> by (auto dest: finite_subset)
  1172       then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
  1173         by blast
  1174       then have "of_nat n \<le> x"
  1175         by (cases x) (auto simp: of_nat_eq_enat)
  1176       with x show ?thesis
  1177         by (auto intro!: bexI[of _ x] less_le_trans[OF n])
  1178     qed
  1179     then have "(SUP x : X. ennreal_of_enat x) = top"
  1180       by simp
  1181     then show "top \<le> (SUP x : X. ennreal_of_enat x)"
  1182       unfolding top_unique by simp
  1183   qed
  1184   then show ?thesis
  1185     by (auto intro!: antisym Sup_least intro: Sup_upper)
  1186 qed
  1187 
  1188 lemma ennreal_of_enat_eSuc[simp]: "ennreal_of_enat (eSuc x) = 1 + ennreal_of_enat x"
  1189   by (cases x) (auto simp: eSuc_enat)
  1190 
  1191 subsection \<open>Topology on @{typ ennreal}\<close>
  1192 
  1193 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
  1194   using enn2ereal_nonneg
  1195   by (cases a rule: ereal_ennreal_cases)
  1196      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
  1197            simp del: enn2ereal_nonneg
  1198            intro: le_less_trans less_imp_le)
  1199 
  1200 lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
  1201   by (cases a rule: ereal_ennreal_cases)
  1202      (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
  1203            intro: less_le_trans)
  1204 
  1205 instantiation ennreal :: linear_continuum_topology
  1206 begin
  1207 
  1208 definition open_ennreal :: "ennreal set \<Rightarrow> bool"
  1209   where "(open :: ennreal set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
  1210 
  1211 instance
  1212 proof
  1213   show "\<exists>a b::ennreal. a \<noteq> b"
  1214     using zero_neq_one by (intro exI)
  1215   show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
  1216   proof transfer
  1217     fix x y :: ereal assume "0 \<le> x" and *: "x < y"
  1218     moreover from dense[OF *] guess z ..
  1219     ultimately show "\<exists>z\<in>Collect ((\<le>) 0). x < z \<and> z < y"
  1220       by (intro bexI[of _ z]) auto
  1221   qed
  1222 qed (rule open_ennreal_def)
  1223 
  1224 end
  1225 
  1226 lemma continuous_on_e2ennreal: "continuous_on A e2ennreal"
  1227 proof (rule continuous_on_subset)
  1228   show "continuous_on ({0..} \<union> {..0}) e2ennreal"
  1229   proof (rule continuous_on_closed_Un)
  1230     show "continuous_on {0 ..} e2ennreal"
  1231       by (rule continuous_onI_mono)
  1232          (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
  1233     show "continuous_on {.. 0} e2ennreal"
  1234       by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
  1235          (auto simp add: e2ennreal_neg continuous_on_const)
  1236   qed auto
  1237   show "A \<subseteq> {0..} \<union> {..0::ereal}"
  1238     by auto
  1239 qed
  1240 
  1241 lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
  1242   by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
  1243 
  1244 lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
  1245   by (rule continuous_on_generate_topology[OF open_generated_order])
  1246      (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
  1247 
  1248 lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
  1249   by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
  1250 
  1251 lemma sup_continuous_e2ennreal[order_continuous_intros]:
  1252   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
  1253   apply (rule sup_continuous_compose[OF _ f])
  1254   apply (rule continuous_at_left_imp_sup_continuous)
  1255   apply (auto simp: mono_def e2ennreal_mono continuous_at_e2ennreal)
  1256   done
  1257 
  1258 lemma sup_continuous_enn2ereal[order_continuous_intros]:
  1259   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. enn2ereal (f x))"
  1260   apply (rule sup_continuous_compose[OF _ f])
  1261   apply (rule continuous_at_left_imp_sup_continuous)
  1262   apply (simp_all add: mono_def less_eq_ennreal.rep_eq continuous_at_enn2ereal)
  1263   done
  1264 
  1265 lemma sup_continuous_mult_left_ennreal':
  1266   fixes c :: "ennreal"
  1267   shows "sup_continuous (\<lambda>x. c * x)"
  1268   unfolding sup_continuous_def
  1269   by transfer (auto simp: SUP_ereal_mult_left max.absorb2 SUP_upper2)
  1270 
  1271 lemma sup_continuous_mult_left_ennreal[order_continuous_intros]:
  1272   "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. c * f x :: ennreal)"
  1273   by (rule sup_continuous_compose[OF sup_continuous_mult_left_ennreal'])
  1274 
  1275 lemma sup_continuous_mult_right_ennreal[order_continuous_intros]:
  1276   "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x * c :: ennreal)"
  1277   using sup_continuous_mult_left_ennreal[of f c] by (simp add: mult.commute)
  1278 
  1279 lemma sup_continuous_divide_ennreal[order_continuous_intros]:
  1280   fixes f g :: "'a::complete_lattice \<Rightarrow> ennreal"
  1281   shows "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x / c)"
  1282   unfolding divide_ennreal_def by (rule sup_continuous_mult_right_ennreal)
  1283 
  1284 lemma transfer_enn2ereal_continuous_on [transfer_rule]:
  1285   "rel_fun (=) (rel_fun (rel_fun (=) pcr_ennreal) (=)) continuous_on continuous_on"
  1286 proof -
  1287   have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal"
  1288     using continuous_on_compose2[OF continuous_on_e2ennreal[of "{0..}"] that]
  1289     by (auto simp: ennreal.enn2ereal_inverse subset_eq e2ennreal_def max_absorb2)
  1290   moreover
  1291   have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal"
  1292     using continuous_on_compose2[OF continuous_on_enn2ereal that] by auto
  1293   ultimately
  1294   show ?thesis
  1295     by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
  1296 qed
  1297 
  1298 lemma transfer_sup_continuous[transfer_rule]:
  1299   "(rel_fun (rel_fun (=) pcr_ennreal) (=)) sup_continuous sup_continuous"
  1300 proof (safe intro!: rel_funI dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
  1301   show "sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f" for f :: "'a \<Rightarrow> _"
  1302     using sup_continuous_e2ennreal[of "enn2ereal \<circ> f"] by simp
  1303   show "sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)" for f :: "'a \<Rightarrow> _"
  1304     using sup_continuous_enn2ereal[of f] by (simp add: comp_def)
  1305 qed
  1306 
  1307 lemma continuous_on_ennreal[tendsto_intros]:
  1308   "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. ennreal (f x))"
  1309   by transfer (auto intro!: continuous_on_max continuous_on_const continuous_on_ereal)
  1310 
  1311 lemma tendsto_ennrealD:
  1312   assumes lim: "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
  1313   assumes *: "\<forall>\<^sub>F x in F. 0 \<le> f x" and x: "0 \<le> x"
  1314   shows "(f \<longlongrightarrow> x) F"
  1315   using continuous_on_tendsto_compose[OF continuous_on_enn2ereal lim]
  1316   apply simp
  1317   apply (subst (asm) tendsto_cong)
  1318   using *
  1319   apply eventually_elim
  1320   apply (auto simp: max_absorb2 \<open>0 \<le> x\<close>)
  1321   done
  1322 
  1323 lemma tendsto_ennreal_iff[simp]:
  1324   "\<forall>\<^sub>F x in F. 0 \<le> f x \<Longrightarrow> 0 \<le> x \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
  1325   by (auto dest: tendsto_ennrealD)
  1326      (auto simp: ennreal_def
  1327            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
  1328 
  1329 lemma tendsto_enn2ereal_iff[simp]: "((\<lambda>i. enn2ereal (f i)) \<longlongrightarrow> enn2ereal x) F \<longleftrightarrow> (f \<longlongrightarrow> x) F"
  1330   using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
  1331     continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\<lambda>x. enn2ereal (f x)" "enn2ereal x" F UNIV]
  1332   by auto
  1333 
  1334 lemma continuous_on_add_ennreal:
  1335   fixes f g :: "'a::topological_space \<Rightarrow> ennreal"
  1336   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)"
  1337   by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)
  1338 
  1339 lemma continuous_on_inverse_ennreal[continuous_intros]:
  1340   fixes f :: "'a::topological_space \<Rightarrow> ennreal"
  1341   shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
  1342 proof (transfer fixing: A)
  1343   show "pred_fun top  ((\<le>) 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
  1344     for f :: "'a \<Rightarrow> ereal"
  1345     using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
  1346 qed
  1347 
  1348 instance ennreal :: topological_comm_monoid_add
  1349 proof
  1350   show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" for a b :: ennreal
  1351     using continuous_on_add_ennreal[of UNIV fst snd]
  1352     using tendsto_at_iff_tendsto_nhds[symmetric, of "\<lambda>x::(ennreal \<times> ennreal). fst x + snd x"]
  1353     by (auto simp: continuous_on_eq_continuous_at)
  1354        (simp add: isCont_def nhds_prod[symmetric])
  1355 qed
  1356 
  1357 lemma sup_continuous_add_ennreal[order_continuous_intros]:
  1358   fixes f g :: "'a::complete_lattice \<Rightarrow> ennreal"
  1359   shows "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. f x + g x)"
  1360   by transfer (auto intro!: sup_continuous_add)
  1361 
  1362 lemma ennreal_suminf_lessD: "(\<Sum>i. f i :: ennreal) < x \<Longrightarrow> f i < x"
  1363   using le_less_trans[OF sum_le_suminf[OF summableI, of "{i}" f]] by simp
  1364 
  1365 lemma sums_ennreal[simp]: "(\<And>i. 0 \<le> f i) \<Longrightarrow> 0 \<le> x \<Longrightarrow> (\<lambda>i. ennreal (f i)) sums ennreal x \<longleftrightarrow> f sums x"
  1366   unfolding sums_def by (simp add: always_eventually sum_nonneg)
  1367 
  1368 lemma summable_suminf_not_top: "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> summable f"
  1369   using summable_sums[OF summableI, of "\<lambda>i. ennreal (f i)"]
  1370   by (cases "\<Sum>i. ennreal (f i)" rule: ennreal_cases)
  1371      (auto simp: summable_def)
  1372 
  1373 lemma suminf_ennreal[simp]:
  1374   "(\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
  1375   by (rule sums_unique[symmetric]) (simp add: summable_suminf_not_top suminf_nonneg summable_sums)
  1376 
  1377 lemma sums_enn2ereal[simp]: "(\<lambda>i. enn2ereal (f i)) sums enn2ereal x \<longleftrightarrow> f sums x"
  1378   unfolding sums_def by (simp add: always_eventually sum_nonneg)
  1379 
  1380 lemma suminf_enn2ereal[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
  1381   by (rule sums_unique[symmetric]) (simp add: summable_sums)
  1382 
  1383 lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal suminf suminf"
  1384   by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
  1385 
  1386 lemma ennreal_suminf_cmult[simp]: "(\<Sum>i. r * f i) = r * (\<Sum>i. f i::ennreal)"
  1387   by transfer (auto intro!: suminf_cmult_ereal)
  1388 
  1389 lemma ennreal_suminf_multc[simp]: "(\<Sum>i. f i * r) = (\<Sum>i. f i::ennreal) * r"
  1390   using ennreal_suminf_cmult[of r f] by (simp add: ac_simps)
  1391 
  1392 lemma ennreal_suminf_divide[simp]: "(\<Sum>i. f i / r) = (\<Sum>i. f i::ennreal) / r"
  1393   by (simp add: divide_ennreal_def)
  1394 
  1395 lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
  1396   using sums_ennreal[of f "suminf f"]
  1397   by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
  1398 
  1399 lemma suminf_ennreal_eq:
  1400   "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
  1401   using suminf_nonneg[of f] sums_unique[of f x]
  1402   by (intro sums_unique[symmetric]) (auto simp: summable_sums_iff)
  1403 
  1404 lemma ennreal_suminf_bound_add:
  1405   fixes f :: "nat \<Rightarrow> ennreal"
  1406   shows "(\<And>N. (\<Sum>n<N. f n) + y \<le> x) \<Longrightarrow> suminf f + y \<le> x"
  1407   by transfer (auto intro!: suminf_bound_add)
  1408 
  1409 lemma ennreal_suminf_SUP_eq_directed:
  1410   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
  1411   assumes *: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
  1412   shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
  1413 proof cases
  1414   assume "I \<noteq> {}"
  1415   then obtain i where "i \<in> I" by auto
  1416   from * show ?thesis
  1417     by (transfer fixing: I)
  1418        (auto simp: max_absorb2 SUP_upper2[OF \<open>i \<in> I\<close>] suminf_nonneg summable_ereal_pos \<open>I \<noteq> {}\<close>
  1419              intro!: suminf_SUP_eq_directed)
  1420 qed (simp add: bot_ennreal)
  1421 
  1422 lemma INF_ennreal_add_const:
  1423   fixes f g :: "nat \<Rightarrow> ennreal"
  1424   shows "(INF i. f i + c) = (INF i. f i) + c"
  1425   using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
  1426   using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
  1427   by (auto simp: mono_def)
  1428 
  1429 lemma INF_ennreal_const_add:
  1430   fixes f g :: "nat \<Rightarrow> ennreal"
  1431   shows "(INF i. c + f i) = c + (INF i. f i)"
  1432   using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
  1433 
  1434 lemma SUP_mult_left_ennreal: "c * (SUP i:I. f i) = (SUP i:I. c * f i ::ennreal)"
  1435 proof cases
  1436   assume "I \<noteq> {}" then show ?thesis
  1437     by transfer (auto simp add: SUP_ereal_mult_left max_absorb2 SUP_upper2)
  1438 qed (simp add: bot_ennreal)
  1439 
  1440 lemma SUP_mult_right_ennreal: "(SUP i:I. f i) * c = (SUP i:I. f i * c ::ennreal)"
  1441   using SUP_mult_left_ennreal by (simp add: mult.commute)
  1442 
  1443 lemma SUP_divide_ennreal: "(SUP i:I. f i) / c = (SUP i:I. f i / c ::ennreal)"
  1444   using SUP_mult_right_ennreal by (simp add: divide_ennreal_def)
  1445 
  1446 lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
  1447 proof (intro antisym top_greatest le_SUP_iff[THEN iffD2] allI impI)
  1448   fix y :: ennreal assume "y < top"
  1449   then obtain r where "y = ennreal r"
  1450     by (cases y rule: ennreal_cases) auto
  1451   then show "\<exists>i\<in>UNIV. y < of_nat i"
  1452     using reals_Archimedean2[of "max 1 r"] zero_less_one
  1453     by (simp add: ennreal_Ex_less_of_nat)
  1454 qed
  1455 
  1456 lemma ennreal_SUP_eq_top:
  1457   fixes f :: "'a \<Rightarrow> ennreal"
  1458   assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
  1459   shows "(SUP i : I. f i) = top"
  1460 proof -
  1461   have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
  1462     using assms by (auto intro!: SUP_least intro: SUP_upper2)
  1463   then show ?thesis
  1464     by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
  1465 qed
  1466 
  1467 lemma ennreal_INF_const_minus:
  1468   fixes f :: "'a \<Rightarrow> ennreal"
  1469   shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
  1470   by (transfer fixing: I)
  1471      (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
  1472 
  1473 lemma of_nat_Sup_ennreal:
  1474   assumes "A \<noteq> {}" "bdd_above A"
  1475   shows "of_nat (Sup A) = (SUP a:A. of_nat a :: ennreal)"
  1476 proof (intro antisym)
  1477   show "(SUP a:A. of_nat a::ennreal) \<le> of_nat (Sup A)"
  1478     by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
  1479   have "Sup A \<in> A"
  1480     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
  1481   then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::ennreal)"
  1482     by (intro SUP_upper)
  1483 qed
  1484 
  1485 lemma ennreal_tendsto_const_minus:
  1486   fixes g :: "'a \<Rightarrow> ennreal"
  1487   assumes ae: "\<forall>\<^sub>F x in F. g x \<le> c"
  1488   assumes g: "((\<lambda>x. c - g x) \<longlongrightarrow> 0) F"
  1489   shows "(g \<longlongrightarrow> c) F"
  1490 proof (cases c rule: ennreal_cases)
  1491   case top with tendsto_unique[OF _ g, of "top"] show ?thesis
  1492     by (cases "F = bot") auto
  1493 next
  1494   case (real r)
  1495   then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
  1496     by (auto simp: le_ennreal_iff)
  1497   then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
  1498     by metis
  1499   from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
  1500   proof eventually_elim
  1501     fix x assume "g x \<le> c" with *[of x] \<open>0 \<le> r\<close> show "c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
  1502       by (auto simp: real ennreal_minus)
  1503   qed
  1504   with g have "((\<lambda>x. ennreal (r - f x)) \<longlongrightarrow> ennreal 0) F"
  1505     by (auto simp add: tendsto_cong eventually_conj_iff)
  1506   with ae2 have "((\<lambda>x. r - f x) \<longlongrightarrow> 0) F"
  1507     by (subst (asm) tendsto_ennreal_iff) (auto elim: eventually_mono)
  1508   then have "(f \<longlongrightarrow> r) F"
  1509     by (rule Lim_transform2[OF tendsto_const])
  1510   with ae2 have "((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal r) F"
  1511     by (subst tendsto_ennreal_iff) (auto elim: eventually_mono simp: real)
  1512   with ae2 show ?thesis
  1513     by (auto simp: real tendsto_cong eventually_conj_iff)
  1514 qed
  1515 
  1516 lemma ennreal_SUP_add:
  1517   fixes f g :: "nat \<Rightarrow> ennreal"
  1518   shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
  1519   unfolding incseq_def le_fun_def
  1520   by transfer
  1521      (simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)
  1522 
  1523 lemma ennreal_SUP_sum:
  1524   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
  1525   shows "(\<And>i. i \<in> I \<Longrightarrow> incseq (f i)) \<Longrightarrow> (SUP n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. SUP n. f i n)"
  1526   unfolding incseq_def
  1527   by transfer
  1528      (simp add: SUP_ereal_sum incseq_def SUP_upper2 max_absorb2 sum_nonneg)
  1529 
  1530 lemma ennreal_liminf_minus:
  1531   fixes f :: "nat \<Rightarrow> ennreal"
  1532   shows "(\<And>n. f n \<le> c) \<Longrightarrow> liminf (\<lambda>n. c - f n) = c - limsup f"
  1533   apply transfer
  1534   apply (simp add: ereal_diff_positive max.absorb2 liminf_ereal_cminus)
  1535   apply (subst max.absorb2)
  1536   apply (rule ereal_diff_positive)
  1537   apply (rule Limsup_bounded)
  1538   apply auto
  1539   done
  1540 
  1541 lemma ennreal_continuous_on_cmult:
  1542   "(c::ennreal) < top \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
  1543   by (transfer fixing: A) (auto intro: continuous_on_cmult_ereal)
  1544 
  1545 lemma ennreal_tendsto_cmult:
  1546   "(c::ennreal) < top \<Longrightarrow> (f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. c * f x) \<longlongrightarrow> c * x) F"
  1547   by (rule continuous_on_tendsto_compose[where g=f, OF ennreal_continuous_on_cmult, where s=UNIV])
  1548      (auto simp: continuous_on_id)
  1549 
  1550 lemma tendsto_ennrealI[intro, simp, tendsto_intros]:
  1551   "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
  1552   by (auto simp: ennreal_def
  1553            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
  1554 
  1555 lemma tendsto_enn2erealI [tendsto_intros]:
  1556   assumes "(f \<longlongrightarrow> l) F"
  1557   shows "((\<lambda>i. enn2ereal(f i)) \<longlongrightarrow> enn2ereal l) F"
  1558 using tendsto_enn2ereal_iff assms by auto
  1559 
  1560 lemma tendsto_e2ennrealI [tendsto_intros]:
  1561   assumes "(f \<longlongrightarrow> l) F"
  1562   shows "((\<lambda>i. e2ennreal(f i)) \<longlongrightarrow> e2ennreal l) F"
  1563 proof -
  1564   have *: "e2ennreal (max x 0) = e2ennreal x" for x
  1565     by (simp add: e2ennreal_def max.commute)
  1566   have "((\<lambda>i. max (f i) 0) \<longlongrightarrow> max l 0) F"
  1567     apply (intro tendsto_intros) using assms by auto
  1568   then have "((\<lambda>i. enn2ereal(e2ennreal (max (f i) 0))) \<longlongrightarrow> enn2ereal (e2ennreal (max l 0))) F"
  1569     by (subst enn2ereal_e2ennreal, auto)+
  1570   then have "((\<lambda>i. e2ennreal (max (f i) 0)) \<longlongrightarrow> e2ennreal (max l 0)) F"
  1571     using tendsto_enn2ereal_iff by auto
  1572   then show ?thesis
  1573     unfolding * by auto
  1574 qed
  1575 
  1576 lemma ennreal_suminf_minus:
  1577   fixes f g :: "nat \<Rightarrow> ennreal"
  1578   shows "(\<And>i. g i \<le> f i) \<Longrightarrow> suminf f \<noteq> top \<Longrightarrow> suminf g \<noteq> top \<Longrightarrow> (\<Sum>i. f i - g i) = suminf f - suminf g"
  1579   by transfer
  1580      (auto simp add: max.absorb2 ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
  1581 
  1582 lemma ennreal_Sup_countable_SUP:
  1583   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
  1584   unfolding incseq_def
  1585   apply transfer
  1586   subgoal for A
  1587     using Sup_countable_SUP[of A]
  1588     apply (clarsimp simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
  1589     subgoal for f
  1590       by (intro exI[of _ f]) auto
  1591     done
  1592   done
  1593 
  1594 lemma ennreal_Inf_countable_INF:
  1595   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. decseq f \<and> range f \<subseteq> A \<and> Inf A = (INF i. f i)"
  1596   including ennreal.lifting
  1597   unfolding decseq_def
  1598   apply transfer
  1599   subgoal for A
  1600     using Inf_countable_INF[of A]
  1601     apply (clarsimp simp add: decseq_def[symmetric])
  1602     subgoal for f
  1603       by (intro exI[of _ f]) auto
  1604     done
  1605   done
  1606 
  1607 lemma ennreal_SUP_countable_SUP:
  1608   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
  1609   using ennreal_Sup_countable_SUP [of "g`A"] by auto
  1610 
  1611 lemma of_nat_tendsto_top_ennreal: "(\<lambda>n::nat. of_nat n :: ennreal) \<longlonglongrightarrow> top"
  1612   using LIMSEQ_SUP[of "of_nat :: nat \<Rightarrow> ennreal"]
  1613   by (simp add: ennreal_SUP_of_nat_eq_top incseq_def)
  1614 
  1615 lemma SUP_sup_continuous_ennreal:
  1616   fixes f :: "ennreal \<Rightarrow> 'a::complete_lattice"
  1617   assumes f: "sup_continuous f" and "I \<noteq> {}"
  1618   shows "(SUP i:I. f (g i)) = f (SUP i:I. g i)"
  1619 proof (rule antisym)
  1620   show "(SUP i:I. f (g i)) \<le> f (SUP i:I. g i)"
  1621     by (rule mono_SUP[OF sup_continuous_mono[OF f]])
  1622   from ennreal_Sup_countable_SUP[of "g`I"] \<open>I \<noteq> {}\<close>
  1623   obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i : I. g i) = (SUP i. M i)"
  1624     by auto
  1625   have "f (SUP i : I. g i) = (SUP i : range M. f i)"
  1626     unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
  1627   also have "\<dots> \<le> (SUP i : I. f (g i))"
  1628     by (insert M, drule SUP_subset_mono) auto
  1629   finally show "f (SUP i : I. g i) \<le> (SUP i : I. f (g i))" .
  1630 qed
  1631 
  1632 lemma ennreal_suminf_SUP_eq:
  1633   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ennreal"
  1634   shows "(\<And>i. incseq (\<lambda>n. f n i)) \<Longrightarrow> (\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
  1635   apply (rule ennreal_suminf_SUP_eq_directed)
  1636   subgoal for N n j
  1637     by (auto simp: incseq_def intro!:exI[of _ "max n j"])
  1638   done
  1639 
  1640 lemma ennreal_SUP_add_left:
  1641   fixes c :: ennreal
  1642   shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c"
  1643   apply transfer
  1644   apply (simp add: SUP_ereal_add_left)
  1645   apply (subst (1 2) max.absorb2)
  1646   apply (auto intro: SUP_upper2 ereal_add_nonneg_nonneg)
  1647   done
  1648 
  1649 lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *)
  1650   fixes f :: "'a \<Rightarrow> ennreal"
  1651   shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)"
  1652   apply (transfer fixing: I)
  1653   unfolding ex_in_conv[symmetric]
  1654   apply (auto simp add: sup_max[symmetric] SUP_upper2 sup_absorb2
  1655               simp del: sup_ereal_def)
  1656   apply (subst INF_ereal_minus_right[symmetric])
  1657   apply (auto simp del: sup_ereal_def simp add: sup_INF)
  1658   done
  1659 
  1660 subsection \<open>Approximation lemmas\<close>
  1661 
  1662 lemma INF_approx_ennreal:
  1663   fixes x::ennreal and e::real
  1664   assumes "e > 0"
  1665   assumes INF: "x = (INF i : A. f i)"
  1666   assumes "x \<noteq> \<infinity>"
  1667   shows "\<exists>i \<in> A. f i < x + e"
  1668 proof -
  1669   have "(INF i : A. f i) < x + e"
  1670     unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
  1671   then show ?thesis
  1672     unfolding INF_less_iff .
  1673 qed
  1674 
  1675 lemma SUP_approx_ennreal:
  1676   fixes x::ennreal and e::real
  1677   assumes "e > 0" "A \<noteq> {}"
  1678   assumes SUP: "x = (SUP i : A. f i)"
  1679   assumes "x \<noteq> \<infinity>"
  1680   shows "\<exists>i \<in> A. x < f i + e"
  1681 proof -
  1682   have "x < x + e"
  1683     using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
  1684   also have "x + e = (SUP i : A. f i + e)"
  1685     unfolding SUP ennreal_SUP_add_left[OF \<open>A \<noteq> {}\<close>] ..
  1686   finally show ?thesis
  1687     unfolding less_SUP_iff .
  1688 qed
  1689 
  1690 lemma ennreal_approx_SUP:
  1691   fixes x::ennreal
  1692   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
  1693   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
  1694   shows "x = (SUP i : A. f i)"
  1695 proof (rule antisym)
  1696   show "x \<le> (SUP i:A. f i)"
  1697   proof (rule ennreal_le_epsilon)
  1698     fix e :: real assume "0 < e"
  1699     from approx[OF this] guess i ..
  1700     then have "x \<le> f i + e"
  1701       by simp
  1702     also have "\<dots> \<le> (SUP i:A. f i) + e"
  1703       by (intro add_mono \<open>i \<in> A\<close> SUP_upper order_refl)
  1704     finally show "x \<le> (SUP i:A. f i) + e" .
  1705   qed
  1706 qed (intro SUP_least f_bound)
  1707 
  1708 lemma ennreal_approx_INF:
  1709   fixes x::ennreal
  1710   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
  1711   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
  1712   shows "x = (INF i : A. f i)"
  1713 proof (rule antisym)
  1714   show "(INF i:A. f i) \<le> x"
  1715   proof (rule ennreal_le_epsilon)
  1716     fix e :: real assume "0 < e"
  1717     from approx[OF this] guess i .. note i = this
  1718     then have "(INF i:A. f i) \<le> f i"
  1719       by (intro INF_lower)
  1720     also have "\<dots> \<le> x + e"
  1721       by fact
  1722     finally show "(INF i:A. f i) \<le> x + e" .
  1723   qed
  1724 qed (intro INF_greatest f_bound)
  1725 
  1726 lemma ennreal_approx_unit:
  1727   "(\<And>a::ennreal. 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * z \<le> y) \<Longrightarrow> z \<le> y"
  1728   apply (subst SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z, simplified])
  1729   apply (rule SUP_least)
  1730   apply auto
  1731   done
  1732 
  1733 lemma suminf_ennreal2:
  1734   "(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
  1735   using suminf_ennreal_eq by blast
  1736 
  1737 lemma less_top_ennreal: "x < top \<longleftrightarrow> (\<exists>r\<ge>0. x = ennreal r)"
  1738   by (cases x) auto
  1739 
  1740 lemma tendsto_top_iff_ennreal:
  1741   fixes f :: "'a \<Rightarrow> ennreal"
  1742   shows "(f \<longlongrightarrow> top) F \<longleftrightarrow> (\<forall>l\<ge>0. eventually (\<lambda>x. ennreal l < f x) F)"
  1743   by (auto simp: less_top_ennreal order_tendsto_iff )
  1744 
  1745 lemma ennreal_tendsto_top_eq_at_top:
  1746   "((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
  1747   unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
  1748   apply (auto simp: ennreal_less_iff)
  1749   subgoal for y
  1750     by (auto elim!: eventually_mono allE[of _ "max 0 y"])
  1751   done
  1752 
  1753 lemma tendsto_0_if_Limsup_eq_0_ennreal:
  1754   fixes f :: "_ \<Rightarrow> ennreal"
  1755   shows "Limsup F f = 0 \<Longrightarrow> (f \<longlongrightarrow> 0) F"
  1756   using Liminf_le_Limsup[of F f] tendsto_iff_Liminf_eq_Limsup[of F f 0]
  1757   by (cases "F = bot") auto
  1758 
  1759 lemma diff_le_self_ennreal[simp]: "a - b \<le> (a::ennreal)"
  1760   by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus)
  1761 
  1762 lemma ennreal_ineq_diff_add: "b \<le> a \<Longrightarrow> a = b + (a - b::ennreal)"
  1763   by transfer (auto simp: ereal_diff_positive max.absorb2 ereal_ineq_diff_add)
  1764 
  1765 lemma ennreal_mult_strict_left_mono: "(a::ennreal) < c \<Longrightarrow> 0 < b \<Longrightarrow> b < top \<Longrightarrow> b * a < b * c"
  1766   by transfer (auto intro!: ereal_mult_strict_left_mono)
  1767 
  1768 lemma ennreal_between: "0 < e \<Longrightarrow> 0 < x \<Longrightarrow> x < top \<Longrightarrow> x - e < (x::ennreal)"
  1769   by transfer (auto intro!: ereal_between)
  1770 
  1771 lemma minus_less_iff_ennreal: "b < top \<Longrightarrow> b \<le> a \<Longrightarrow> a - b < c \<longleftrightarrow> a < c + (b::ennreal)"
  1772   by transfer
  1773      (auto simp: top_ereal_def ereal_minus_less le_less)
  1774 
  1775 lemma tendsto_zero_ennreal:
  1776   assumes ev: "\<And>r. 0 < r \<Longrightarrow> \<forall>\<^sub>F x in F. f x < ennreal r"
  1777   shows "(f \<longlongrightarrow> 0) F"
  1778 proof (rule order_tendstoI)
  1779   fix e::ennreal assume "e > 0"
  1780   obtain e'::real where "e' > 0" "ennreal e' < e"
  1781     using \<open>0 < e\<close> dense[of 0 "if e = top then 1 else (enn2real e)"]
  1782     by (cases e) (auto simp: ennreal_less_iff)
  1783   from ev[OF \<open>e' > 0\<close>] show "\<forall>\<^sub>F x in F. f x < e"
  1784     by eventually_elim (insert \<open>ennreal e' < e\<close>, auto)
  1785 qed simp
  1786 
  1787 lifting_update ennreal.lifting
  1788 lifting_forget ennreal.lifting
  1789 
  1790 
  1791 subsection \<open>@{typ ennreal} theorems\<close>
  1792 
  1793 lemma neq_top_trans: fixes x y :: ennreal shows "\<lbrakk> y \<noteq> top; x \<le> y \<rbrakk> \<Longrightarrow> x \<noteq> top"
  1794 by (auto simp: top_unique)
  1795 
  1796 lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
  1797   by (cases a b rule: ennreal2_cases)
  1798      (auto simp: ennreal_minus top_unique)
  1799 
  1800 lemma ennreal_less_one_iff[simp]: "ennreal x < 1 \<longleftrightarrow> x < 1"
  1801   by (cases "0 \<le> x")
  1802      (auto simp: ennreal_neg ennreal_1[symmetric] ennreal_less_iff simp del: ennreal_1)
  1803 
  1804 lemma SUP_const_minus_ennreal:
  1805   fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
  1806   including ennreal.lifting
  1807   by (transfer fixing: I)
  1808      (simp add: sup_ereal_def[symmetric] SUP_sup_distrib[symmetric] SUP_ereal_minus_right
  1809            del: sup_ereal_def)
  1810 
  1811 lemma zero_minus_ennreal[simp]: "0 - (a::ennreal) = 0"
  1812   including ennreal.lifting
  1813   by transfer (simp split: split_max)
  1814 
  1815 lemma diff_diff_commute_ennreal:
  1816   fixes a b c :: ennreal shows "a - b - c = a - c - b"
  1817   by (cases a b c rule: ennreal3_cases) (simp_all add: ennreal_minus field_simps)
  1818 
  1819 lemma diff_gr0_ennreal: "b < (a::ennreal) \<Longrightarrow> 0 < a - b"
  1820   including ennreal.lifting by transfer (auto simp: ereal_diff_gr0 ereal_diff_positive split: split_max)
  1821 
  1822 lemma divide_le_posI_ennreal:
  1823   fixes x y z :: ennreal
  1824   shows "x > 0 \<Longrightarrow> z \<le> x * y \<Longrightarrow> z / x \<le> y"
  1825   by (cases x y z rule: ennreal3_cases)
  1826      (auto simp: divide_ennreal ennreal_mult[symmetric] field_simps top_unique)
  1827 
  1828 lemma add_diff_eq_ennreal:
  1829   fixes x y z :: ennreal
  1830   shows "z \<le> y \<Longrightarrow> x + (y - z) = x + y - z"
  1831   including ennreal.lifting
  1832   by transfer
  1833      (insert ereal_add_mono[of 0], auto simp add: ereal_diff_positive max.absorb2 add_diff_eq_ereal)
  1834 
  1835 lemma add_diff_inverse_ennreal:
  1836   fixes x y :: ennreal shows "x \<le> y \<Longrightarrow> x + (y - x) = y"
  1837   by (cases x) (simp_all add: top_unique add_diff_eq_ennreal)
  1838 
  1839 lemma add_diff_eq_iff_ennreal[simp]:
  1840   fixes x y :: ennreal shows "x + (y - x) = y \<longleftrightarrow> x \<le> y"
  1841 proof
  1842   assume *: "x + (y - x) = y" show "x \<le> y"
  1843     by (subst *[symmetric]) simp
  1844 qed (simp add: add_diff_inverse_ennreal)
  1845 
  1846 lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
  1847   apply (cases a b c rule: ennreal3_cases)
  1848   subgoal for a' b' c'
  1849     by (cases "0 \<le> b' - c'")
  1850        (simp_all add: ennreal_minus ennreal_plus[symmetric] top_add ennreal_neg
  1851                  del: ennreal_plus)
  1852   apply (simp_all add: top_add ennreal_plus[symmetric] del: ennreal_plus)
  1853   done
  1854 
  1855 lemma diff_eq_0_ennreal: "a < top \<Longrightarrow> a \<le> b \<Longrightarrow> a - b = (0::ennreal)"
  1856   using ennreal_minus_pos_iff gr_zeroI not_less by blast
  1857 
  1858 lemma diff_diff_ennreal': fixes x y z :: ennreal shows "z \<le> y \<Longrightarrow> y - z \<le> x \<Longrightarrow> x - (y - z) = x + z - y"
  1859   by (cases x; cases y; cases z)
  1860      (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique
  1861            simp del: ennreal_plus)
  1862 
  1863 lemma diff_diff_ennreal'': fixes x y z :: ennreal
  1864   shows "z \<le> y \<Longrightarrow> x - (y - z) = (if y - z \<le> x then x + z - y else 0)"
  1865   by (cases x; cases y; cases z)
  1866      (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique ennreal_neg
  1867            simp del: ennreal_plus)
  1868 
  1869 lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
  1870   using power_eq_top_ennreal[of x n] by (auto simp: less_top)
  1871 
  1872 lemma ennreal_divide_times: "(a / b) * c = a * (c / b :: ennreal)"
  1873   by (simp add: mult.commute ennreal_times_divide)
  1874 
  1875 lemma diff_less_top_ennreal: "a - b < top \<longleftrightarrow>  a < (top :: ennreal)"
  1876   by (cases a; cases b) (auto simp: ennreal_minus)
  1877 
  1878 lemma divide_less_ennreal: "b \<noteq> 0 \<Longrightarrow> b < top \<Longrightarrow> a / b < c \<longleftrightarrow> a < (c * b :: ennreal)"
  1879   by (cases a; cases b; cases c)
  1880      (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
  1881 
  1882 lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
  1883   by (simp del: ennreal_1 ennreal_numeral add: ennreal_1[symmetric] ennreal_numeral[symmetric] ennreal_less_iff)
  1884 
  1885 lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
  1886   by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
  1887 
  1888 lemma ennreal_mult_cancel_left: "(a * b = a * c) = (a = top \<and> b \<noteq> 0 \<and> c \<noteq> 0 \<or> a = 0 \<or> b = (c::ennreal))"
  1889   by (cases a; cases b; cases c) (auto simp: ennreal_mult[symmetric] ennreal_mult_top ennreal_top_mult)
  1890 
  1891 lemma ennreal_minus_if: "ennreal a - ennreal b = ennreal (if 0 \<le> b then (if b \<le> a then a - b else 0) else a)"
  1892   by (auto simp: ennreal_minus ennreal_neg)
  1893 
  1894 lemma ennreal_plus_if: "ennreal a + ennreal b = ennreal (if 0 \<le> a then (if 0 \<le> b then a + b else a) else b)"
  1895   by (auto simp: ennreal_neg)
  1896 
  1897 lemma power_le_one_iff: "0 \<le> (a::real) \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
  1898   by (metis (mono_tags, hide_lams) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
  1899 
  1900 lemma ennreal_diff_le_mono_left: "a \<le> b \<Longrightarrow> a - c \<le> (b::ennreal)"
  1901   using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp
  1902 
  1903 lemma ennreal_minus_le_iff: "a - b \<le> c \<longleftrightarrow> (a \<le> b + (c::ennreal) \<and> (a = top \<and> b = top \<longrightarrow> c = top))"
  1904   by (cases a; cases b; cases c)
  1905      (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric]
  1906            simp del: ennreal_plus)
  1907 
  1908 lemma ennreal_le_minus_iff: "a \<le> b - c \<longleftrightarrow> (a + c \<le> (b::ennreal) \<or> (a = 0 \<and> b \<le> c))"
  1909   by (cases a; cases b; cases c)
  1910      (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric] ennreal_le_iff2
  1911            simp del: ennreal_plus)
  1912 
  1913 lemma diff_add_eq_diff_diff_swap_ennreal: "x - (y + z :: ennreal) = x - y - z"
  1914   by (cases x; cases y; cases z)
  1915      (auto simp: ennreal_plus[symmetric] ennreal_minus_if add_top top_add simp del: ennreal_plus)
  1916 
  1917 lemma diff_add_assoc2_ennreal: "b \<le> a \<Longrightarrow> (a - b + c::ennreal) = a + c - b"
  1918   by (cases a; cases b; cases c)
  1919      (auto simp add: ennreal_minus_if ennreal_plus_if add_top top_add top_unique simp del: ennreal_plus)
  1920 
  1921 lemma diff_gt_0_iff_gt_ennreal: "0 < a - b \<longleftrightarrow> (a = top \<and> b = top \<or> b < (a::ennreal))"
  1922   by (cases a; cases b) (auto simp: ennreal_minus_if ennreal_less_iff)
  1923 
  1924 lemma diff_eq_0_iff_ennreal: "(a - b::ennreal) = 0 \<longleftrightarrow> (a < top \<and> a \<le> b)"
  1925   by (cases a) (auto simp: ennreal_minus_eq_0 diff_eq_0_ennreal)
  1926 
  1927 lemma add_diff_self_ennreal: "a + (b - a::ennreal) = (if a \<le> b then b else a)"
  1928   by (auto simp: diff_eq_0_iff_ennreal less_top)
  1929 
  1930 lemma diff_add_self_ennreal: "(b - a + a::ennreal) = (if a \<le> b then b else a)"
  1931   by (auto simp: diff_add_cancel_ennreal diff_eq_0_iff_ennreal less_top)
  1932 
  1933 lemma ennreal_minus_cancel_iff:
  1934   fixes a b c :: ennreal
  1935   shows "a - b = a - c \<longleftrightarrow> (b = c \<or> (a \<le> b \<and> a \<le> c) \<or> a = top)"
  1936   by (cases a; cases b; cases c) (auto simp: ennreal_minus_if)
  1937 
  1938 text \<open>The next lemma is wrong for $a = top$, for $b = c = 1$ for instance.\<close>
  1939 
  1940 lemma ennreal_right_diff_distrib:
  1941   fixes a b c::ennreal
  1942   assumes "a \<noteq> top"
  1943   shows "a * (b - c) = a * b - a * c"
  1944   apply (cases a, cases b, cases c, auto simp add: assms)
  1945   apply (metis (mono_tags, lifting) ennreal_minus ennreal_mult' linordered_field_class.sign_simps(38) split_mult_pos_le)
  1946   apply (metis ennreal_minus_zero ennreal_mult_cancel_left ennreal_top_eq_mult_iff minus_top_ennreal mult_eq_0_iff top_neq_ennreal)
  1947   apply (metis ennreal_minus_eq_top ennreal_minus_zero ennreal_mult_eq_top_iff mult_eq_0_iff)
  1948   done
  1949 
  1950 lemma SUP_diff_ennreal:
  1951   "c < top \<Longrightarrow> (SUP i:I. f i - c :: ennreal) = (SUP i:I. f i) - c"
  1952   by (auto intro!: SUP_eqI ennreal_minus_mono SUP_least intro: SUP_upper
  1953            simp: ennreal_minus_cancel_iff ennreal_minus_le_iff less_top[symmetric])
  1954 
  1955 lemma ennreal_SUP_add_right:
  1956   fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i:I. f i) = (SUP i:I. c + f i)"
  1957   using ennreal_SUP_add_left[of I f c] by (simp add: add.commute)
  1958 
  1959 lemma SUP_add_directed_ennreal:
  1960   fixes f g :: "_ \<Rightarrow> ennreal"
  1961   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
  1962   shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
  1963 proof cases
  1964   assume "I = {}" then show ?thesis
  1965     by (simp add: bot_ereal_def)
  1966 next
  1967   assume "I \<noteq> {}"
  1968   show ?thesis
  1969   proof (rule antisym)
  1970     show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
  1971       by (rule SUP_least; intro add_mono SUP_upper)
  1972   next
  1973     have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
  1974       by (intro ennreal_SUP_add_left[symmetric] \<open>I \<noteq> {}\<close>)
  1975     also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
  1976       by (intro SUP_cong refl ennreal_SUP_add_right \<open>I \<noteq> {}\<close>)
  1977     also have "\<dots> \<le> (SUP i:I. f i + g i)"
  1978       using directed by (intro SUP_least) (blast intro: SUP_upper2)
  1979     finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
  1980   qed
  1981 qed
  1982 
  1983 lemma enn2real_eq_0_iff: "enn2real x = 0 \<longleftrightarrow> x = 0 \<or> x = top"
  1984   by (cases x) auto
  1985 
  1986 lemma continuous_on_diff_ennreal:
  1987   "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> top) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<noteq> top) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ennreal)"
  1988   including ennreal.lifting
  1989 proof (transfer fixing: A, simp add: top_ereal_def)
  1990   fix f g :: "'a \<Rightarrow> ereal" assume "\<forall>x. 0 \<le> f x" "\<forall>x. 0 \<le> g x" "continuous_on A f" "continuous_on A g"
  1991   moreover assume "f x \<noteq> \<infinity>" "g x \<noteq> \<infinity>" if "x \<in> A" for x
  1992   ultimately show "continuous_on A (\<lambda>z. max 0 (f z - g z))"
  1993     by (intro continuous_on_max continuous_on_const continuous_on_diff_ereal) auto
  1994 qed
  1995 
  1996 lemma tendsto_diff_ennreal:
  1997   "(f \<longlongrightarrow> x) F \<Longrightarrow> (g \<longlongrightarrow> y) F \<Longrightarrow> x \<noteq> top \<Longrightarrow> y \<noteq> top \<Longrightarrow> ((\<lambda>z. f z - g z::ennreal) \<longlongrightarrow> x - y) F"
  1998   using continuous_on_tendsto_compose[where f="\<lambda>x. fst x - snd x::ennreal" and s="{(x, y). x \<noteq> top \<and> y \<noteq> top}" and g="\<lambda>x. (f x, g x)" and l="(x, y)" and F="F",
  1999     OF continuous_on_diff_ennreal]
  2000   by (auto simp: tendsto_Pair eventually_conj_iff less_top order_tendstoD continuous_on_fst continuous_on_snd continuous_on_id)
  2001 
  2002 declare lim_real_of_ereal [tendsto_intros]
  2003 
  2004 lemma tendsto_enn2real [tendsto_intros]:
  2005   assumes "(u \<longlongrightarrow> ennreal l) F" "l \<ge> 0"
  2006   shows "((\<lambda>n. enn2real (u n)) \<longlongrightarrow> l) F"
  2007   unfolding enn2real_def
  2008   apply (intro tendsto_intros)
  2009   apply (subst enn2ereal_ennreal[symmetric])
  2010   by (intro tendsto_intros assms)+
  2011 
  2012 end