products/Sources/formale Sprachen/Isabelle/HOL/Library/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Cardinal_Order_Relation.thy   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/Library/Extended_Nonnegative_Real.thy
    Author:     Johannes Hölzl
*)

subsection \<open>The type of non-negative extended real numbers\<close>

theory Extended_Nonnegative_Real
  imports Extended_Real Indicator_Function
begin

lemma ereal_ineq_diff_add:
  assumes "b \ (-\::ereal)" "a \ b"
  shows "a = b + (a-b)"
by (metis add.commute assms ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)

lemma Limsup_const_add:
  fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
  shows "F \ bot \ Limsup F (\x. c + f x) = c + Limsup F f"
  by (rule Limsup_compose_continuous_mono)
     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)

lemma Liminf_const_add:
  fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
  shows "F \ bot \ Liminf F (\x. c + f x) = c + Liminf F f"
  by (rule Liminf_compose_continuous_mono)
     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)

lemma Liminf_add_const:
  fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
  shows "F \ bot \ Liminf F (\x. f x + c) = Liminf F f + c"
  by (rule Liminf_compose_continuous_mono)
     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)

lemma sums_offset:
  fixes f g :: "nat \ 'a :: {t2_space, topological_comm_monoid_add}"
  assumes "(\n. f (n + i)) sums l" shows "f sums (l + (\j
proof  -
  have "(\k. (\nj l + (\j
    using assms by (auto intro!: tendsto_add simp: sums_def)
  moreover
  { fix k :: nat
    have "(\jj=i..j=0..
      by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
    also have "(\j=i..j\(\n. n + i)`{0..
      unfolding image_add_atLeastLessThan by simp
    finally have "(\jnj
      by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
  ultimately have "(\k. (\n l + (\j
    by simp
  then show ?thesis
    unfolding sums_def by (rule LIMSEQ_offset)
qed

lemma suminf_offset:
  fixes f g :: "nat \ 'a :: {t2_space, topological_comm_monoid_add}"
  shows "summable (\j. f (j + i)) \ suminf f = (\j. f (j + i)) + (\j
  by (intro sums_unique[symmetric] sums_offset summable_sums)

lemma eventually_at_left_1: "(\z::real. 0 < z \ z < 1 \ P z) \ eventually P (at_left 1)"
  by (subst eventually_at_left[of 0]) (auto intro: exI[of _ 0])

lemma mult_eq_1:
  fixes a b :: "'a :: {ordered_semiring, comm_monoid_mult}"
  shows "0 \ a \ a \ 1 \ b \ 1 \ a * b = 1 \ (a = 1 \ b = 1)"
  by (metis mult.left_neutral eq_iff mult.commute mult_right_mono)

lemma ereal_add_diff_cancel:
  fixes a b :: ereal
  shows "\b\ \ \ \ (a + b) - b = a"
  by (cases a b rule: ereal2_cases) auto

lemma add_top:
  fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
  shows "0 \ x \ x + top = top"
  by (intro top_le add_increasing order_refl)

lemma top_add:
  fixes x :: "'a::{order_top, ordered_comm_monoid_add}"
  shows "0 \ x \ top + x = top"
  by (intro top_le add_increasing2 order_refl)

lemma le_lfp: "mono f \ x \ lfp f \ f x \ lfp f"
  by (subst lfp_unfold) (auto dest: monoD)

lemma lfp_transfer:
  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and mg: "mono g"
  assumes bot: "\ bot \ lfp g" and eq: "\x. x \ lfp f \ \ (f x) = g (\ x)"
  shows "\ (lfp f) = lfp g"
proof (rule antisym)
  note mf = sup_continuous_mono[OF f]
  have f_le_lfp: "(f ^^ i) bot \ lfp f" for i
    by (induction i) (auto intro: le_lfp mf)

  have "\ ((f ^^ i) bot) \ lfp g" for i
    by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
  then show "\ (lfp f) \ lfp g"
    unfolding sup_continuous_lfp[OF f]
    by (subst \<alpha>[THEN sup_continuousD])
       (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)

  show "lfp g \ \ (lfp f)"
    by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
qed

lemma sup_continuous_applyD: "sup_continuous f \ sup_continuous (\x. f x h)"
  using sup_continuous_apply[THEN sup_continuous_compose] .

lemma sup_continuous_SUP[order_continuous_intros]:
  fixes M :: "_ \ _ \ 'a::complete_lattice"
  assumes M: "\i. i \ I \ sup_continuous (M i)"
  shows  "sup_continuous (SUP i\I. M i)"
  unfolding sup_continuous_def by (auto simp add: sup_continuousD [OF M] image_comp intro: SUP_commute)

lemma sup_continuous_apply_SUP[order_continuous_intros]:
  fixes M :: "_ \ _ \ 'a::complete_lattice"
  shows "(\i. i \ I \ sup_continuous (M i)) \ sup_continuous (\x. SUP i\I. M i x)"
  unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)

lemma sup_continuous_lfp'[order_continuous_intros]:
  assumes 1: "sup_continuous f"
  assumes 2: "\g. sup_continuous g \ sup_continuous (f g)"
  shows "sup_continuous (lfp f)"
proof -
  have "sup_continuous ((f ^^ i) bot)" for i
  proof (induction i)
    case (Suc i) then show ?case
      by (auto intro!: 2)
  qed (simp add: bot_fun_def sup_continuous_const)
  then show ?thesis
    unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
qed

lemma sup_continuous_lfp''[order_continuous_intros]:
  assumes 1: "\s. sup_continuous (f s)"
  assumes 2: "\g. sup_continuous g \ sup_continuous (\s. f s (g s))"
  shows "sup_continuous (\x. lfp (f x))"
proof -
  have "sup_continuous (\x. (f x ^^ i) bot)" for i
  proof (induction i)
    case (Suc i) then show ?case
      by (auto intro!: 2)
  qed (simp add: bot_fun_def sup_continuous_const)
  then show ?thesis
    unfolding sup_continuous_lfp[OF 1] by (intro order_continuous_intros)
qed

lemma mono_INF_fun:
    "(\x y. mono (F x y)) \ mono (\z x. INF y \ X x. F x y z :: 'a :: complete_lattice)"
  by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)

lemma continuous_on_cmult_ereal:
  "\c::ereal\ \ \ \ continuous_on A f \ continuous_on A (\x. c * f x)"
  using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
  by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)

lemma real_of_nat_Sup:
  assumes "A \ {}" "bdd_above A"
  shows "of_nat (Sup A) = (SUP a\A. of_nat a :: real)"
proof (intro antisym)
  show "(SUP a\A. of_nat a::real) \ of_nat (Sup A)"
    using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
  have "Sup A \ A"
    using assms by (auto simp: Sup_nat_def bdd_above_nat)
  then show "of_nat (Sup A) \ (SUP a\A. of_nat a::real)"
    by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
qed

lemma (in complete_lattice) SUP_sup_const1:
  "I \ {} \ (SUP i\I. sup c (f i)) = sup c (SUP i\I. f i)"
  using SUP_sup_distrib[of "\_. c" I f] by simp

lemma (in complete_lattice) SUP_sup_const2:
  "I \ {} \ (SUP i\I. sup (f i) c) = sup (SUP i\I. f i) c"
  using SUP_sup_distrib[of f I "\_. c"] by simp

lemma one_less_of_natD:
  assumes "(1::'a::linordered_semidom) < of_nat n" shows "1 < n"
  by (cases n) (use assms in auto)

subsection \<open>Defining the extended non-negative reals\<close>

text \<open>Basic definitions and type class setup\<close>

typedef ennreal = "{x :: ereal. 0 \ x}"
  morphisms enn2ereal e2ennreal'
  by auto

definition "e2ennreal x = e2ennreal' (max 0 x)"

lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
proof -
  have "\y\0. x = e2ennreal y" for x
    by (cases x) (auto simp: e2ennreal_def max_absorb2)
  then show ?thesis
    by (auto simp: image_iff Bex_def)
qed

lemma type_definition_ennreal': "type_definition enn2ereal e2ennreal {x. 0 \ x}"
  using type_definition_ennreal
  by (auto simp: type_definition_def e2ennreal_def max_absorb2)

setup_lifting type_definition_ennreal'

declare [[coercion e2ennreal]]

instantiation ennreal :: complete_linorder
begin

lift_definition top_ennreal :: ennreal is top by (rule top_greatest)
lift_definition bot_ennreal :: ennreal is 0 by (rule order_refl)
lift_definition sup_ennreal :: "ennreal \ ennreal \ ennreal" is sup by (rule le_supI1)
lift_definition inf_ennreal :: "ennreal \ ennreal \ ennreal" is inf by (rule le_infI)

lift_definition Inf_ennreal :: "ennreal set \ ennreal" is "Inf"
  by (rule Inf_greatest)

lift_definition Sup_ennreal :: "ennreal set \ ennreal" is "sup 0 \ Sup"
  by auto

lift_definition less_eq_ennreal :: "ennreal \ ennreal \ bool" is "(\)" .
lift_definition less_ennreal :: "ennreal \ ennreal \ bool" is "(<)" .

instance
  by standard
     (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+

end

lemma pcr_ennreal_enn2ereal[simp]: "pcr_ennreal (enn2ereal x) x"
  by (simp add: ennreal.pcr_cr_eq cr_ennreal_def)

lemma rel_fun_eq_pcr_ennreal: "rel_fun (=) pcr_ennreal f g \ f = enn2ereal \ g"
  by (auto simp: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)

instantiation ennreal :: infinity
begin

definition infinity_ennreal :: ennreal
where
  [simp]: "\ = (top::ennreal)"

instance ..

end

instantiation ennreal :: "{semiring_1_no_zero_divisors, comm_semiring_1}"
begin

lift_definition one_ennreal :: ennreal is 1 by simp
lift_definition zero_ennreal :: ennreal is 0 by simp
lift_definition plus_ennreal :: "ennreal \ ennreal \ ennreal" is "(+)" by simp
lift_definition times_ennreal :: "ennreal \ ennreal \ ennreal" is "(*)" by simp

instance
  by standard (transfer; auto simp: field_simps ereal_right_distrib)+

end

instantiation ennreal :: minus
begin

lift_definition minus_ennreal :: "ennreal \ ennreal \ ennreal" is "\a b. max 0 (a - b)"
  by simp

instance ..

end

instance ennreal :: numeral ..

instantiation ennreal :: inverse
begin

lift_definition inverse_ennreal :: "ennreal \ ennreal" is inverse
  by (rule inverse_ereal_ge0I)

definition divide_ennreal :: "ennreal \ ennreal \ ennreal"
  where "x div y = x * inverse (y :: ennreal)"

instance ..

end

lemma ennreal_zero_less_one: "0 < (1::ennreal)" \<comment> \<open>TODO: remove\<close>
  by transfer auto

instance ennreal :: dioid
proof (standard; transfer)
  fix a b :: ereal assume "0 \ a" "0 \ b" then show "(a \ b) = (\c\Collect ((\) 0). b = a + c)"
    unfolding ereal_ex_split Bex_def
    by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"])
qed

instance ennreal :: ordered_comm_semiring
  by standard
     (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+

instance ennreal :: linordered_nonzero_semiring
proof
  fix a b::ennreal
  show "a < b \ a + 1 < b + 1"
    by transfer (simp add: add_right_mono ereal_add_cancel_right less_le)
qed (transfer; simp)

instance ennreal :: strict_ordered_ab_semigroup_add
proof
  fix a b c d :: ennreal show "a < b \ c < d \ a + c < b + d"
    by transfer (auto intro!: ereal_add_strict_mono)
qed

declare [[coercion "of_nat :: nat \ ennreal"]]

lemma e2ennreal_neg: "x \ 0 \ e2ennreal x = 0"
  unfolding zero_ennreal_def e2ennreal_def by (simp add: max_absorb1)

lemma e2ennreal_mono: "x \ y \ e2ennreal x \ e2ennreal y"
  by (cases "0 \ x" "0 \ y" rule: bool.exhaust[case_product bool.exhaust])
     (auto simp: e2ennreal_neg less_eq_ennreal.abs_eq eq_onp_def)

lemma enn2ereal_nonneg[simp]: "0 \ enn2ereal x"
  using ennreal.enn2ereal[of x] by simp

lemma ereal_ennreal_cases:
  obtains b where "0 \ a" "a = enn2ereal b" | "a < 0"
  using e2ennreal'_inverse[of a, symmetric] by (cases "0 \ a") (auto intro: enn2ereal_nonneg)

lemma rel_fun_liminf[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal liminf liminf"
proof -
  have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\x. sup 0 (liminf x)) liminf"
    unfolding liminf_SUP_INF[abs_def] by (transfer_prover_start, transfer_step+; simp)
  then show ?thesis
    apply (subst (asm) (2) rel_fun_def)
    apply (subst (2) rel_fun_def)
    apply (auto simp: comp_def max.absorb2 Liminf_bounded rel_fun_eq_pcr_ennreal)
    done
qed

lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
proof -
  have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\x. INF n. sup 0 (SUP i\{n..}. x i)) limsup"
    unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
  then show ?thesis
    unfolding limsup_INF_SUP[abs_def]
    apply (subst (asm) (2) rel_fun_def)
    apply (subst (2) rel_fun_def)
    apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
    apply (subst (asm) max.absorb2)
    apply (auto intro: SUP_upper2)
    done
qed

lemma sum_enn2ereal[simp]: "(\i. i \ I \ 0 \ f i) \ (\i\I. enn2ereal (f i)) = enn2ereal (sum f I)"
  by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg zero_ennreal.rep_eq plus_ennreal.rep_eq)

lemma transfer_e2ennreal_sum [transfer_rule]:
  "rel_fun (rel_fun (=) pcr_ennreal) (rel_fun (=) pcr_ennreal) sum sum"
  by (auto intro!: rel_funI simp: rel_fun_eq_pcr_ennreal comp_def)

lemma enn2ereal_of_nat[simp]: "enn2ereal (of_nat n) = ereal n"
  by (induction n) (auto simp: zero_ennreal.rep_eq one_ennreal.rep_eq plus_ennreal.rep_eq)

lemma enn2ereal_numeral[simp]: "enn2ereal (numeral a) = numeral a"
  by (metis enn2ereal_of_nat numeral_eq_ereal of_nat_numeral)

lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
  unfolding cr_ennreal_def pcr_ennreal_def by auto

subsection \<open>Cancellation simprocs\<close>

lemma ennreal_add_left_cancel: "a + b = a + c \ a = (\::ennreal) \ b = c"
  unfolding infinity_ennreal_def by transfer (simp add: top_ereal_def ereal_add_cancel_left)

lemma ennreal_add_left_cancel_le: "a + b \ a + c \ a = (\::ennreal) \ b \ c"
  unfolding infinity_ennreal_def by transfer (simp add: ereal_add_le_add_iff top_ereal_def disj_commute)

lemma ereal_add_left_cancel_less:
  fixes a b c :: ereal
  shows "0 \ a \ 0 \ b \ a + b < a + c \ a \ \ \ b < c"
  by (cases a b c rule: ereal3_cases) auto

lemma ennreal_add_left_cancel_less: "a + b < a + c \ a \ (\::ennreal) \ b < c"
  unfolding infinity_ennreal_def
  by transfer (simp add: top_ereal_def ereal_add_left_cancel_less)

ML \<open>
structure Cancel_Ennreal_Common =
struct
  (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
  fun find_first_t _    _ []         = raise TERM("find_first_t", [])
    | find_first_t past u (t::terms) =
          if u aconv t then (rev past @ terms)
          else find_first_t (t::past) u terms

  fun dest_summing (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t $ u, ts) =
        dest_summing (t, dest_summing (u, ts))
    | dest_summing (t, ts) = t :: ts

  val mk_sum = Arith_Data.long_mk_sum
  fun dest_sum t = dest_summing (t, [])
  val find_first = find_first_t []
  val trans_tac = Numeral_Simprocs.trans_tac
  val norm_ss =
    simpset_of (put_simpset HOL_basic_ss \<^context>
      addsimps @{thms ac_simps add_0_left add_0_right})
  fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
  fun simplify_meta_eq ctxt cancel_th th =
    Arith_Data.simplify_meta_eq [] ctxt
      ([th, cancel_th] MRS trans)
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end

structure Eq_Ennreal_Cancel = ExtractCommonTermFun
(open Cancel_Ennreal_Common
  val mk_bal = HOLogic.mk_eq
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>HOL.eq\<close> \<^typ>\<open>ennreal\<close>
  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel}
)

structure Le_Ennreal_Cancel = ExtractCommonTermFun
(open Cancel_Ennreal_Common
  val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> \<^typ>\<open>ennreal\<close>
  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_le}
)

structure Less_Ennreal_Cancel = ExtractCommonTermFun
(open Cancel_Ennreal_Common
  val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> \<^typ>\<open>ennreal\<close>
  fun simp_conv _ _ = SOME @{thm ennreal_add_left_cancel_less}
)
\<close>

simproc_setup ennreal_eq_cancel
  ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
  \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>

simproc_setup ennreal_le_cancel
  ("(l::ennreal) + m \ n" | "(l::ennreal) \ m + n") =
  \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>

simproc_setup ennreal_less_cancel
  ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
  \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>


subsection \<open>Order with top\<close>

lemma ennreal_zero_less_top[simp]: "0 < (top::ennreal)"
  by transfer (simp add: top_ereal_def)

lemma ennreal_one_less_top[simp]: "1 < (top::ennreal)"
  by transfer (simp add: top_ereal_def)

lemma ennreal_zero_neq_top[simp]: "0 \ (top::ennreal)"
  by transfer (simp add: top_ereal_def)

lemma ennreal_top_neq_zero[simp]: "(top::ennreal) \ 0"
  by transfer (simp add: top_ereal_def)

lemma ennreal_top_neq_one[simp]: "top \ (1::ennreal)"
  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)

lemma ennreal_one_neq_top[simp]: "1 \ (top::ennreal)"
  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)

lemma ennreal_add_less_top[simp]:
  fixes a b :: ennreal
  shows "a + b < top \ a < top \ b < top"
  by transfer (auto simp: top_ereal_def)

lemma ennreal_add_eq_top[simp]:
  fixes a b :: ennreal
  shows "a + b = top \ a = top \ b = top"
  by transfer (auto simp: top_ereal_def)

lemma ennreal_sum_less_top[simp]:
  fixes f :: "'a \ ennreal"
  shows "finite I \ (\i\I. f i) < top \ (\i\I. f i < top)"
  by (induction I rule: finite_induct) auto

lemma ennreal_sum_eq_top[simp]:
  fixes f :: "'a \ ennreal"
  shows "finite I \ (\i\I. f i) = top \ (\i\I. f i = top)"
  by (induction I rule: finite_induct) auto

lemma ennreal_mult_eq_top_iff:
  fixes a b :: ennreal
  shows "a * b = top \ (a = top \ b \ 0) \ (b = top \ a \ 0)"
  by transfer (auto simp: top_ereal_def)

lemma ennreal_top_eq_mult_iff:
  fixes a b :: ennreal
  shows "top = a * b \ (a = top \ b \ 0) \ (b = top \ a \ 0)"
  using ennreal_mult_eq_top_iff[of a b] by auto

lemma ennreal_mult_less_top:
  fixes a b :: ennreal
  shows "a * b < top \ (a = 0 \ b = 0 \ (a < top \ b < top))"
  by transfer (auto simp add: top_ereal_def)

lemma top_power_ennreal: "top ^ n = (if n = 0 then 1 else top :: ennreal)"
  by (induction n) (simp_all add: ennreal_mult_eq_top_iff)

lemma ennreal_prod_eq_0[simp]:
  fixes f :: "'a \ ennreal"
  shows "(prod f A = 0) = (finite A \ (\i\A. f i = 0))"
  by (induction A rule: infinite_finite_induct) auto

lemma ennreal_prod_eq_top:
  fixes f :: "'a \ ennreal"
  shows "(\i\I. f i) = top \ (finite I \ ((\i\I. f i \ 0) \ (\i\I. f i = top)))"
  by (induction I rule: infinite_finite_induct) (auto simp: ennreal_mult_eq_top_iff)

lemma ennreal_top_mult: "top * a = (if a = 0 then 0 else top :: ennreal)"
  by (simp add: ennreal_mult_eq_top_iff)

lemma ennreal_mult_top: "a * top = (if a = 0 then 0 else top :: ennreal)"
  by (simp add: ennreal_mult_eq_top_iff)

lemma enn2ereal_eq_top_iff[simp]: "enn2ereal x = \ \ x = top"
  by transfer (simp add: top_ereal_def)

lemma enn2ereal_top[simp]: "enn2ereal top = \"
  by transfer (simp add: top_ereal_def)

lemma e2ennreal_infty[simp]: "e2ennreal \ = top"
  by (simp add: top_ennreal.abs_eq top_ereal_def)

lemma ennreal_top_minus[simp]: "top - x = (top::ennreal)"
  by transfer (auto simp: top_ereal_def max_def)

lemma minus_top_ennreal: "x - top = (if x = top then top else 0:: ennreal)"
  by transfer (use ereal_eq_minus_iff top_ereal_def in force)

lemma bot_ennreal: "bot = (0::ennreal)"
  by transfer rule

lemma ennreal_of_nat_neq_top[simp]: "of_nat i \ (top::ennreal)"
  by (induction i) auto

lemma numeral_eq_of_nat: "(numeral a::ennreal) = of_nat (numeral a)"
  by simp

lemma of_nat_less_top: "of_nat i < (top::ennreal)"
  using less_le_trans[of "of_nat i" "of_nat (Suc i)" "top::ennreal"]
  by simp

lemma top_neq_numeral[simp]: "top \ (numeral i::ennreal)"
  using of_nat_less_top[of "numeral i"] by simp

lemma ennreal_numeral_less_top[simp]: "numeral i < (top::ennreal)"
  using of_nat_less_top[of "numeral i"] by simp

lemma ennreal_add_bot[simp]: "bot + x = (x::ennreal)"
  by transfer simp

instance ennreal :: semiring_char_0
proof (standard, safe intro!: linorder_injI)
  have *: "1 + of_nat k \ (0::ennreal)" for k
    using add_pos_nonneg[OF zero_less_one, of "of_nat k :: ennreal"] by auto
  fix x y :: nat assume "x < y" "of_nat x = (of_nat y::ennreal)" then show False
    by (auto simp add: less_iff_Suc_add *)
qed

subsection \<open>Arithmetic\<close>

lemma ennreal_minus_zero[simp]: "a - (0::ennreal) = a"
  by transfer (auto simp: max_def)

lemma ennreal_add_diff_cancel_right[simp]:
  fixes x y z :: ennreal shows "y \ top \ (x + y) - y = x"
  by transfer (metis ereal_eq_minus_iff max_absorb2 not_MInfty_nonneg top_ereal_def)

lemma ennreal_add_diff_cancel_left[simp]:
  fixes x y z :: ennreal shows "y \ top \ (y + x) - y = x"
  by (simp add: add.commute)

lemma
  fixes a b :: ennreal
  shows "a - b = 0 \ a \ b"
  by transfer (metis ereal_diff_gr0 le_cases max.absorb2 not_less)

lemma ennreal_minus_cancel:
  fixes a b c :: ennreal
  shows "c \ top \ a \ c \ b \ c \ c - a = c - b \ a = b"
  apply transfer
  subgoal for a b c
    by (cases a b c rule: ereal3_cases)
       (auto simp: top_ereal_def max_def split: if_splits)
  done

lemma sup_const_add_ennreal:
  fixes a b c :: "ennreal"
  shows "sup (c + a) (c + b) = c + sup a b"
  by transfer (metis add_left_mono le_cases sup.absorb2 sup.orderE)

lemma ennreal_diff_add_assoc:
  fixes a b c :: ennreal
  shows "a \ b \ c + b - a = c + (b - a)"
  apply transfer
  subgoal for a b c
    by (cases a b c rule: ereal3_cases) (auto simp: field_simps max_absorb2)
  done

lemma mult_divide_eq_ennreal:
  fixes a b :: ennreal
  shows "b \ 0 \ b \ top \ (a * b) / b = a"
  unfolding divide_ennreal_def
  apply transfer
  apply (subst mult.assoc)
  apply (simp add: top_ereal_def flip: divide_ereal_def)
  done

lemma divide_mult_eq: "a \ 0 \ a \ \ \ x * a / (b * a) = x / (b::ennreal)"
  unfolding divide_ennreal_def infinity_ennreal_def
  apply transfer
  subgoal for a b c
    apply (cases a b c rule: ereal3_cases)
    apply (auto simp: top_ereal_def)
    done
  done

lemma ennreal_mult_divide_eq:
  fixes a b :: ennreal
  shows "b \ 0 \ b \ top \ (a * b) / b = a"
  unfolding divide_ennreal_def
  apply transfer
  apply (subst mult.assoc)
  apply (simp add: top_ereal_def flip: divide_ereal_def)
  done

lemma ennreal_add_diff_cancel:
  fixes a b :: ennreal
  shows "b \ \ \ (a + b) - b = a"
  unfolding infinity_ennreal_def
  by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)

lemma ennreal_minus_eq_0:
  "a - b = 0 \ a \ (b::ennreal)"
  by transfer (metis ereal_diff_gr0 le_cases max.absorb2 not_less)

lemma ennreal_mono_minus_cancel:
  fixes a b c :: ennreal
  shows "a - b \ a - c \ a < top \ b \ a \ c \ a \ c \ b"
  by transfer
     (auto simp add: max.absorb2 ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)

lemma ennreal_mono_minus:
  fixes a b c :: ennreal
  shows "c \ b \ a - b \ a - c"
  by transfer (meson ereal_minus_mono max.mono order_refl)

lemma ennreal_minus_pos_iff:
  fixes a b :: ennreal
  shows "a < top \ b < top \ 0 < a - b \ b < a"
  by transfer (use add.left_neutral ereal_minus_le_iff less_irrefl not_less in fastforce)

lemma ennreal_inverse_top[simp]: "inverse top = (0::ennreal)"
  by transfer (simp add: top_ereal_def ereal_inverse_eq_0)

lemma ennreal_inverse_zero[simp]: "inverse 0 = (top::ennreal)"
  by transfer (simp add: top_ereal_def ereal_inverse_eq_0)

lemma ennreal_top_divide: "top / (x::ennreal) = (if x = top then 0 else top)"
  unfolding divide_ennreal_def
  by transfer (simp add: top_ereal_def ereal_inverse_eq_0 ereal_0_gt_inverse)

lemma ennreal_zero_divide[simp]: "0 / (x::ennreal) = 0"
  by (simp add: divide_ennreal_def)

lemma ennreal_divide_zero[simp]: "x / (0::ennreal) = (if x = 0 then 0 else top)"
  by (simp add: divide_ennreal_def ennreal_mult_top)

lemma ennreal_divide_top[simp]: "x / (top::ennreal) = 0"
  by (simp add: divide_ennreal_def ennreal_top_mult)

lemma ennreal_times_divide: "a * (b / c) = a * b / (c::ennreal)"
  unfolding divide_ennreal_def
  by transfer (simp add: divide_ereal_def[symmetric] ereal_times_divide_eq)

lemma ennreal_zero_less_divide: "0 < a / b \ (0 < a \ b < (top::ennreal))"
  unfolding divide_ennreal_def
  by transfer (auto simp: ereal_zero_less_0_iff top_ereal_def ereal_0_gt_inverse)

lemma divide_right_mono_ennreal:
  fixes a b c :: ennreal
  shows "a \ b \ a / c \ b / c"
  unfolding divide_ennreal_def by (intro mult_mono) auto

lemma ennreal_mult_strict_right_mono: "(a::ennreal) < c \ 0 < b \ b < top \ a * b < c * b"
  by transfer (auto intro!: ereal_mult_strict_right_mono)

lemma ennreal_indicator_less[simp]:
  "indicator A x \ (indicator B x::ennreal) \ (x \ A \ x \ B)"
  by (simp add: indicator_def not_le)

lemma ennreal_inverse_positive: "0 < inverse x \ (x::ennreal) \ top"
  by transfer (simp add: ereal_0_gt_inverse top_ereal_def)

lemma ennreal_inverse_mult': "((0 < b \ a < top) \ (0 < a \ b < top)) \ inverse (a * b::ennreal) = inverse a * inverse b"
  apply transfer
  subgoal for a b
    by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
  done

lemma ennreal_inverse_mult: "a < top \ b < top \ inverse (a * b::ennreal) = inverse a * inverse b"
  apply transfer
  subgoal for a b
    by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
  done

lemma ennreal_inverse_1[simp]: "inverse (1::ennreal) = 1"
  by transfer simp

lemma ennreal_inverse_eq_0_iff[simp]: "inverse (a::ennreal) = 0 \ a = top"
  by transfer (simp add: ereal_inverse_eq_0 top_ereal_def)

lemma ennreal_inverse_eq_top_iff[simp]: "inverse (a::ennreal) = top \ a = 0"
  by transfer (simp add: top_ereal_def)

lemma ennreal_divide_eq_0_iff[simp]: "(a::ennreal) / b = 0 \ (a = 0 \ b = top)"
  by (simp add: divide_ennreal_def)

lemma ennreal_divide_eq_top_iff: "(a::ennreal) / b = top \ ((a \ 0 \ b = 0) \ (a = top \ b \ top))"
  by (auto simp add: divide_ennreal_def ennreal_mult_eq_top_iff)

lemma one_divide_one_divide_ennreal[simp]: "1 / (1 / c) = (c::ennreal)"
  including ennreal.lifting
  unfolding divide_ennreal_def
  by transfer auto

lemma ennreal_mult_left_cong:
  "((a::ennreal) \ 0 \ b = c) \ a * b = a * c"
  by (cases "a = 0") simp_all

lemma ennreal_mult_right_cong:
  "((a::ennreal) \ 0 \ b = c) \ b * a = c * a"
  by (cases "a = 0") simp_all

lemma ennreal_zero_less_mult_iff: "0 < a * b \ 0 < a \ 0 < (b::ennreal)"
  by transfer (auto simp add: ereal_zero_less_0_iff le_less)

lemma less_diff_eq_ennreal:
  fixes a b c :: ennreal
  shows "b < top \ c < top \ a < b - c \ a + c < b"
  apply transfer
  subgoal for a b c
    by (cases a b c rule: ereal3_cases) (auto split: split_max)
  done

lemma diff_add_cancel_ennreal:
  fixes a b :: ennreal shows "a \ b \ b - a + a = b"
  unfolding infinity_ennreal_def
  by transfer (metis (no_types) add.commute ereal_diff_positive ereal_ineq_diff_add max_def not_MInfty_nonneg)

lemma ennreal_diff_self[simp]: "a \ top \ a - a = (0::ennreal)"
  by transfer (simp add: top_ereal_def)

lemma ennreal_minus_mono:
  fixes a b c :: ennreal
  shows "a \ c \ d \ b \ a - b \ c - d"
  by transfer (meson ereal_minus_mono max.mono order_refl)

lemma ennreal_minus_eq_top[simp]: "a - (b::ennreal) = top \ a = top"
  by transfer (auto simp: top_ereal_def max.absorb2 ereal_minus_eq_PInfty_iff split: split_max)

lemma ennreal_divide_self[simp]: "a \ 0 \ a < top \ a / a = (1::ennreal)"
  unfolding divide_ennreal_def
  apply transfer
  subgoal for a
    by (cases a) (auto simp: top_ereal_def)
  done

subsection \<open>Coercion from \<^typ>\<open>real\<close> to \<^typ>\<open>ennreal\<close>\<close>

lift_definition ennreal :: "real \ ennreal" is "sup 0 \ ereal"
  by simp

declare [[coercion ennreal]]

lemma ennreal_cong: "x = y \ ennreal x = ennreal y" by simp

lemma ennreal_cases[cases type: ennreal]:
  fixes x :: ennreal
  obtains (real) r :: real where "0 \ r" "x = ennreal r" | (top) "x = top"
  apply transfer
  subgoal for x thesis
    by (cases x) (auto simp: max.absorb2 top_ereal_def)
  done

lemmas ennreal2_cases = ennreal_cases[case_product ennreal_cases]
lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]

lemma ennreal_neq_top[simp]: "ennreal r \ top"
  by transfer (simp add: top_ereal_def zero_ereal_def flip: ereal_max)

lemma top_neq_ennreal[simp]: "top \ ennreal r"
  using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)

lemma ennreal_less_top[simp]: "ennreal x < top"
  by transfer (simp add: top_ereal_def max_def)

lemma ennreal_neg: "x \ 0 \ ennreal x = 0"
  by transfer (simp add: max.absorb1)

lemma ennreal_inj[simp]:
  "0 \ a \ 0 \ b \ ennreal a = ennreal b \ a = b"
  by (transfer fixing: a b) (auto simp: max_absorb2)

lemma ennreal_le_iff[simp]: "0 \ y \ ennreal x \ ennreal y \ x \ y"
  by (auto simp: ennreal_def zero_ereal_def less_eq_ennreal.abs_eq eq_onp_def split: split_max)

lemma le_ennreal_iff: "0 \ r \ x \ ennreal r \ (\q\0. x = ennreal q \ q \ r)"
  by (cases x) (auto simp: top_unique)

lemma ennreal_less_iff: "0 \ r \ ennreal r < ennreal q \ r < q"
  unfolding not_le[symmetric] by auto

lemma ennreal_eq_zero_iff[simp]: "0 \ x \ ennreal x = 0 \ x = 0"
  by transfer (auto simp: max_absorb2)

lemma ennreal_less_zero_iff[simp]: "0 < ennreal x \ 0 < x"
  by transfer (auto simp: max_def)

lemma ennreal_lessI: "0 < q \ r < q \ ennreal r < ennreal q"
  by (cases "0 \ r") (auto simp: ennreal_less_iff ennreal_neg)

lemma ennreal_leI: "x \ y \ ennreal x \ ennreal y"
  by (cases "0 \ y") (auto simp: ennreal_neg)

lemma enn2ereal_ennreal[simp]: "0 \ x \ enn2ereal (ennreal x) = x"
  by transfer (simp add: max_absorb2)

lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
  by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)

lemma enn2ereal_e2ennreal: "x \ 0 \ enn2ereal (e2ennreal x) = x"
by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)

lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)

lemma ennreal_0[simp]: "ennreal 0 = 0"
  by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)

lemma ennreal_1[simp]: "ennreal 1 = 1"
  by transfer (simp add: max_absorb2)

lemma ennreal_eq_0_iff: "ennreal x = 0 \ x \ 0"
  by (cases "0 \ x") (auto simp: ennreal_neg)

lemma ennreal_le_iff2: "ennreal x \ ennreal y \ ((0 \ y \ x \ y) \ (x \ 0 \ y \ 0))"
  by (cases "0 \ y") (auto simp: ennreal_eq_0_iff ennreal_neg)

lemma ennreal_eq_1[simp]: "ennreal x = 1 \ x = 1"
  by (cases "0 \ x") (auto simp: ennreal_neg simp flip: ennreal_1)

lemma ennreal_le_1[simp]: "ennreal x \ 1 \ x \ 1"
  by (cases "0 \ x") (auto simp: ennreal_neg simp flip: ennreal_1)

lemma ennreal_ge_1[simp]: "ennreal x \ 1 \ x \ 1"
  by (cases "0 \ x") (auto simp: ennreal_neg simp flip: ennreal_1)

lemma one_less_ennreal[simp]: "1 < ennreal x \ 1 < x"
  by transfer (auto simp: max.absorb2 less_max_iff_disj)

lemma ennreal_plus[simp]:
  "0 \ a \ 0 \ b \ ennreal (a + b) = ennreal a + ennreal b"
  by (transfer fixing: a b) (auto simp: max_absorb2)

lemma add_mono_ennreal: "x < ennreal y \ x' < ennreal y' \ x + x' < ennreal (y + y')"
  by (metis (full_types) add_strict_mono ennreal_less_zero_iff ennreal_plus less_le not_less zero_le)

lemma sum_ennreal[simp]: "(\i. i \ I \ 0 \ f i) \ (\i\I. ennreal (f i)) = ennreal (sum f I)"
  by (induction I rule: infinite_finite_induct) (auto simp: sum_nonneg)

lemma sum_list_ennreal[simp]:
  assumes "\x. x \ set xs \ f x \ 0"
  shows   "sum_list (map (\x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
using assms
proof (induction xs)
  case (Cons x xs)
  from Cons have "(\x\x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
    by simp
  also from Cons.prems have "\ = ennreal (f x + sum_list (map f xs))"
    by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
  finally show ?case by simp
qed simp_all

lemma ennreal_of_nat_eq_real_of_nat: "of_nat i = ennreal (of_nat i)"
  by (induction i) simp_all

lemma of_nat_le_ennreal_iff[simp]: "0 \ r \ of_nat i \ ennreal r \ of_nat i \ r"
  by (simp add: ennreal_of_nat_eq_real_of_nat)

lemma ennreal_le_of_nat_iff[simp]: "ennreal r \ of_nat i \ r \ of_nat i"
  by (simp add: ennreal_of_nat_eq_real_of_nat)

lemma ennreal_indicator: "ennreal (indicator A x) = indicator A x"
  by (auto split: split_indicator)

lemma ennreal_numeral[simp]: "ennreal (numeral n) = numeral n"
  using ennreal_of_nat_eq_real_of_nat[of "numeral n"] by simp

lemma ennreal_less_numeral_iff [simp]: "ennreal n < numeral w \ n < numeral w"
  by (metis ennreal_less_iff ennreal_numeral less_le not_less zero_less_numeral)

lemma numeral_less_ennreal_iff [simp]: "numeral w < ennreal n \ numeral w < n"
  using ennreal_less_iff zero_le_numeral by fastforce

lemma numeral_le_ennreal_iff [simp]: "numeral n \ ennreal m \ numeral n \ m"
  by (metis not_le ennreal_less_numeral_iff)

lemma min_ennreal: "0 \ x \ 0 \ y \ min (ennreal x) (ennreal y) = ennreal (min x y)"
  by (auto split: split_min)

lemma ennreal_half[simp]: "ennreal (1/2) = inverse 2"
  by transfer (simp add: max.absorb2)

lemma ennreal_minus: "0 \ q \ ennreal r - ennreal q = ennreal (r - q)"
  by transfer
     (simp add: max.absorb2 zero_ereal_def flip: ereal_max)

lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
  by (simp add: minus_top_ennreal)

lemma e2eenreal_enn2ereal_diff [simp]:
  "e2ennreal(enn2ereal x - enn2ereal y) = x - y" for x y
by (cases x, cases y, auto simp add: ennreal_minus e2ennreal_neg)

lemma ennreal_mult: "0 \ a \ 0 \ b \ ennreal (a * b) = ennreal a * ennreal b"
  by transfer (simp add: max_absorb2)

lemma ennreal_mult': "0 \ a \ ennreal (a * b) = ennreal a * ennreal b"
  by (cases "0 \ b") (auto simp: ennreal_mult ennreal_neg mult_nonneg_nonpos)

lemma indicator_mult_ennreal: "indicator A x * ennreal r = ennreal (indicator A x * r)"
  by (simp split: split_indicator)

lemma ennreal_mult'': "0 \ b \ ennreal (a * b) = ennreal a * ennreal b"
  by (cases "0 \ a") (auto simp: ennreal_mult ennreal_neg mult_nonpos_nonneg)

lemma numeral_mult_ennreal: "0 \ x \ numeral b * ennreal x = ennreal (numeral b * x)"
  by (simp add: ennreal_mult)

lemma ennreal_power: "0 \ r \ ennreal r ^ n = ennreal (r ^ n)"
  by (induction n) (auto simp: ennreal_mult)

lemma power_eq_top_ennreal: "x ^ n = top \ (n \ 0 \ (x::ennreal) = top)"
  by (cases x rule: ennreal_cases)
     (auto simp: ennreal_power top_power_ennreal)

lemma inverse_ennreal: "0 < r \ inverse (ennreal r) = ennreal (inverse r)"
  by transfer (simp add: max.absorb2)

lemma divide_ennreal: "0 \ r \ 0 < q \ ennreal r / ennreal q = ennreal (r / q)"
  by (simp add: divide_ennreal_def inverse_ennreal ennreal_mult[symmetric] inverse_eq_divide)

lemma ennreal_inverse_power: "inverse (x ^ n :: ennreal) = inverse x ^ n"
proof (cases x rule: ennreal_cases)
  case top with power_eq_top_ennreal[of x n] show ?thesis
    by (cases "n = 0") auto
next
  case (real r) then show ?thesis
  proof cases
    assume "x = 0" then show ?thesis
      using power_eq_top_ennreal[of top "n - 1"]
      by (cases n) (auto simp: ennreal_top_mult)
  next
    assume "x \ 0"
    with real have "0 < r" by auto
    with real show ?thesis
      by (induction n)
         (auto simp add: ennreal_power ennreal_mult[symmetric] inverse_ennreal)
  qed
qed

lemma ennreal_divide_numeral: "0 \ x \ ennreal x / numeral b = ennreal (x / numeral b)"
  by (subst divide_ennreal[symmetric]) auto

lemma prod_ennreal: "(\i. i \ A \ 0 \ f i) \ (\i\A. ennreal (f i)) = ennreal (prod f A)"
  by (induction A rule: infinite_finite_induct)
     (auto simp: ennreal_mult prod_nonneg)

lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \ (a = b \ c \ 0)"
proof (cases "0 \ c")
  case True
  then show ?thesis
    by (metis ennreal_eq_0_iff ennreal_mult_right_cong ennreal_neq_top mult_divide_eq_ennreal)
qed (use ennreal_neg in auto)

lemma ennreal_le_epsilon:
  "(\e::real. y < top \ 0 < e \ x \ y + ennreal e) \ x \ y"
  apply (cases y rule: ennreal_cases)
  apply (cases x rule: ennreal_cases)
  apply (auto simp flip: ennreal_plus simp add: top_unique intro: zero_less_one field_le_epsilon)
  done

lemma ennreal_rat_dense:
  fixes x y :: ennreal
  shows "x < y \ \r::rat. x < real_of_rat r \ real_of_rat r < y"
proof transfer
  fix x y :: ereal assume xy: "0 \ x" "0 \ y" "x < y"
  moreover
  from ereal_dense3[OF \<open>x < y\<close>]
  obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
    by auto
  then have "0 \ r"
    using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
  with r show "\r. x < (sup 0 \ ereal) (real_of_rat r) \ (sup 0 \ ereal) (real_of_rat r) < y"
    by (intro exI[of _ r]) (auto simp: max_absorb2)
qed

lemma ennreal_Ex_less_of_nat: "(x::ennreal) < top \ \n. x < of_nat n"
  by (cases x rule: ennreal_cases)
     (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_less_iff reals_Archimedean2)

subsection \<open>Coercion from \<^typ>\<open>ennreal\<close> to \<^typ>\<open>real\<close>\<close>

definition "enn2real x = real_of_ereal (enn2ereal x)"

lemma enn2real_nonneg[simp]: "0 \ enn2real x"
  by (auto simp: enn2real_def intro!: real_of_ereal_pos enn2ereal_nonneg)

lemma enn2real_mono: "a \ b \ b < top \ enn2real a \ enn2real b"
  by (auto simp add: enn2real_def less_eq_ennreal.rep_eq intro!: real_of_ereal_positive_mono enn2ereal_nonneg)

lemma enn2real_of_nat[simp]: "enn2real (of_nat n) = n"
  by (auto simp: enn2real_def)

lemma enn2real_ennreal[simp]: "0 \ r \ enn2real (ennreal r) = r"
  by (simp add: enn2real_def)

lemma ennreal_enn2real[simp]: "r < top \ ennreal (enn2real r) = r"
  by (cases r rule: ennreal_cases) auto

lemma real_of_ereal_enn2ereal[simp]: "real_of_ereal (enn2ereal x) = enn2real x"
  by (simp add: enn2real_def)

lemma enn2real_top[simp]: "enn2real top = 0"
  unfolding enn2real_def top_ennreal.rep_eq top_ereal_def by simp

lemma enn2real_0[simp]: "enn2real 0 = 0"
  unfolding enn2real_def zero_ennreal.rep_eq by simp

lemma enn2real_1[simp]: "enn2real 1 = 1"
  unfolding enn2real_def one_ennreal.rep_eq by simp

lemma enn2real_numeral[simp]: "enn2real (numeral n) = (numeral n)"
  unfolding enn2real_def by simp

lemma enn2real_mult: "enn2real (a * b) = enn2real a * enn2real b"
  unfolding enn2real_def
  by (simp del: real_of_ereal_enn2ereal add: times_ennreal.rep_eq)

lemma enn2real_leI: "0 \ B \ x \ ennreal B \ enn2real x \ B"
  by (cases x rule: ennreal_cases) (auto simp: top_unique)

lemma enn2real_positive_iff: "0 < enn2real x \ (0 < x \ x < top)"
  by (cases x rule: ennreal_cases) auto

lemma enn2real_eq_posreal_iff[simp]: "c > 0 \ enn2real x = c \ x = c"
  by (cases x) auto

lemma ennreal_enn2real_if: "ennreal (enn2real r) = (if r = top then 0 else r)"
  by(auto intro!: ennreal_enn2real simp add: less_top)

subsection \<open>Coercion from \<^typ>\<open>enat\<close> to \<^typ>\<open>ennreal\<close>\<close>


definition ennreal_of_enat :: "enat \ ennreal"
where
  "ennreal_of_enat n = (case n of \ \ top | enat n \ of_nat n)"

declare [[coercion ennreal_of_enat]]
declare [[coercion "of_nat :: nat \ ennreal"]]

lemma ennreal_of_enat_infty[simp]: "ennreal_of_enat \ = \"
  by (simp add: ennreal_of_enat_def)

lemma ennreal_of_enat_enat[simp]: "ennreal_of_enat (enat n) = of_nat n"
  by (simp add: ennreal_of_enat_def)

lemma ennreal_of_enat_0[simp]: "ennreal_of_enat 0 = 0"
  using ennreal_of_enat_enat[of 0] unfolding enat_0 by simp

lemma ennreal_of_enat_1[simp]: "ennreal_of_enat 1 = 1"
  using ennreal_of_enat_enat[of 1] unfolding enat_1 by simp

lemma ennreal_top_neq_of_nat[simp]: "(top::ennreal) \ of_nat i"
  using ennreal_of_nat_neq_top[of i] by metis

lemma ennreal_of_enat_inj[simp]: "ennreal_of_enat i = ennreal_of_enat j \ i = j"
  by (cases i j rule: enat.exhaust[case_product enat.exhaust]) auto

lemma ennreal_of_enat_le_iff[simp]: "ennreal_of_enat m \ ennreal_of_enat n \ m \ n"
  by (auto simp: ennreal_of_enat_def top_unique split: enat.split)

lemma of_nat_less_ennreal_of_nat[simp]: "of_nat n \ ennreal_of_enat x \ of_nat n \ x"
  by (cases x) (auto simp: of_nat_eq_enat)

lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x\X. ennreal_of_enat x)"
proof -
  have "ennreal_of_enat (Sup X) \ (SUP x \ X. ennreal_of_enat x)"
    unfolding Sup_enat_def
  proof (clarsimp, intro conjI impI)
    fix x assume "finite X" "X \ {}"
    then show "ennreal_of_enat (Max X) \ (SUP x \ X. ennreal_of_enat x)"
      by (intro SUP_upper Max_in)
  next
    assume "infinite X" "X \ {}"
    have "\y\X. r < ennreal_of_enat y" if r: "r < top" for r
    proof -
      from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
      have "\ (X \ enat ` {.. n})"
        using \<open>infinite X\<close> by (auto dest: finite_subset)
      then obtain x where x: "x \ X" "x \ enat ` {..n}"
        by blast
      then have "of_nat n \ x"
        by (cases x) (auto simp: of_nat_eq_enat)
      with x show ?thesis
        by (auto intro!: bexI[of _ x] less_le_trans[OF n])
    qed
    then have "(SUP x \ X. ennreal_of_enat x) = top"
      by simp
    then show "top \ (SUP x \ X. ennreal_of_enat x)"
      unfolding top_unique by simp
  qed
  then show ?thesis
    by (auto intro!: antisym Sup_least intro: Sup_upper)
qed

lemma ennreal_of_enat_eSuc[simp]: "ennreal_of_enat (eSuc x) = 1 + ennreal_of_enat x"
  by (cases x) (auto simp: eSuc_enat)

subsection \<open>Topology on \<^typ>\<open>ennreal\<close>\<close>

lemma enn2ereal_Iio: "enn2ereal -` {.. a then {..< e2ennreal a} else {})"
  using enn2ereal_nonneg
  by (cases a rule: ereal_ennreal_cases)
     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
           simp del: enn2ereal_nonneg
           intro: le_less_trans less_imp_le)

lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \ a then {e2ennreal a <..} else UNIV)"
  by (cases a rule: ereal_ennreal_cases)
     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
           intro: less_le_trans)

instantiation ennreal :: linear_continuum_topology
begin

definition open_ennreal :: "ennreal set \ bool"
  where "(open :: ennreal set \ bool) = generate_topology (range lessThan \ range greaterThan)"

instance
proof
  show "\a b::ennreal. a \ b"
    using zero_neq_one by (intro exI)
  show "\x y::ennreal. x < y \ \z>x. z < y"
  proof transfer
    fix x y :: ereal assume "0 \ x" and *: "x < y"
    moreover from dense[OF *] guess z ..
    ultimately show "\z\Collect ((\) 0). x < z \ z < y"
      by (intro bexI[of _ z]) auto
  qed
qed (rule open_ennreal_def)

end

lemma continuous_on_e2ennreal: "continuous_on A e2ennreal"
proof (rule continuous_on_subset)
  show "continuous_on ({0..} \ {..0}) e2ennreal"
  proof (rule continuous_on_closed_Un)
    show "continuous_on {0 ..} e2ennreal"
      by (rule continuous_onI_mono)
         (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
    show "continuous_on {.. 0} e2ennreal"
      by (subst continuous_on_cong[OF refl, of _ _ "\_. 0"])
         (auto simp add: e2ennreal_neg continuous_on_const)
  qed auto
  show "A \ {0..} \ {..0::ereal}"
    by auto
qed

lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
  by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto

lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
  by (rule continuous_on_generate_topology[OF open_generated_order])
     (auto simp add: enn2ereal_Iio enn2ereal_Ioi)

lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
  by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto

lemma sup_continuous_e2ennreal[order_continuous_intros]:
  assumes f: "sup_continuous f" shows "sup_continuous (\x. e2ennreal (f x))"
proof (rule sup_continuous_compose[OF _ f])
  show "sup_continuous e2ennreal"
    by (simp add: continuous_at_e2ennreal continuous_at_left_imp_sup_continuous e2ennreal_mono mono_def)
qed

lemma sup_continuous_enn2ereal[order_continuous_intros]:
  assumes f: "sup_continuous f" shows "sup_continuous (\x. enn2ereal (f x))"
proof (rule sup_continuous_compose[OF _ f])
  show "sup_continuous enn2ereal"
  by (simp add: continuous_at_enn2ereal continuous_at_left_imp_sup_continuous less_eq_ennreal.rep_eq mono_def)
qed

lemma sup_continuous_mult_left_ennreal':
  fixes c :: "ennreal"
  shows "sup_continuous (\x. c * x)"
  unfolding sup_continuous_def
  by transfer (auto simp: SUP_ereal_mult_left max.absorb2 SUP_upper2)

lemma sup_continuous_mult_left_ennreal[order_continuous_intros]:
  "sup_continuous f \ sup_continuous (\x. c * f x :: ennreal)"
  by (rule sup_continuous_compose[OF sup_continuous_mult_left_ennreal'])

lemma sup_continuous_mult_right_ennreal[order_continuous_intros]:
  "sup_continuous f \ sup_continuous (\x. f x * c :: ennreal)"
  using sup_continuous_mult_left_ennreal[of f c] by (simp add: mult.commute)

lemma sup_continuous_divide_ennreal[order_continuous_intros]:
  fixes f g :: "'a::complete_lattice \ ennreal"
  shows "sup_continuous f \ sup_continuous (\x. f x / c)"
  unfolding divide_ennreal_def by (rule sup_continuous_mult_right_ennreal)

lemma transfer_enn2ereal_continuous_on [transfer_rule]:
  "rel_fun (=) (rel_fun (rel_fun (=) pcr_ennreal) (=)) continuous_on continuous_on"
proof -
  have "continuous_on A f" if "continuous_on A (\x. enn2ereal (f x))" for A and f :: "'a \ ennreal"
    using continuous_on_compose2[OF continuous_on_e2ennreal[of "{0..}"] that]
    by (auto simp: ennreal.enn2ereal_inverse subset_eq e2ennreal_def max_absorb2)
  moreover
  have "continuous_on A (\x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \ ennreal"
    using continuous_on_compose2[OF continuous_on_enn2ereal that] by auto
  ultimately
  show ?thesis
    by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
qed

lemma transfer_sup_continuous[transfer_rule]:
  "(rel_fun (rel_fun (=) pcr_ennreal) (=)) sup_continuous sup_continuous"
proof (safe intro!: rel_funI dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
  show "sup_continuous (enn2ereal \ f) \ sup_continuous f" for f :: "'a \ _"
    using sup_continuous_e2ennreal[of "enn2ereal \ f"] by simp
  show "sup_continuous f \ sup_continuous (enn2ereal \ f)" for f :: "'a \ _"
    using sup_continuous_enn2ereal[of f] by (simp add: comp_def)
qed

lemma continuous_on_ennreal[tendsto_intros]:
  "continuous_on A f \ continuous_on A (\x. ennreal (f x))"
  by transfer (auto intro!: continuous_on_max continuous_on_const continuous_on_ereal)

lemma tendsto_ennrealD:
  assumes lim: "((\x. ennreal (f x)) \ ennreal x) F"
  assumes *: "\\<^sub>F x in F. 0 \ f x" and x: "0 \ x"
  shows "(f \ x) F"
proof -
  have "((\x. enn2ereal (ennreal (f x))) \ enn2ereal (ennreal x)) F
    \<longleftrightarrow> (f \<longlongrightarrow> enn2ereal (ennreal x)) F"
    using "*" eventually_mono
    by (intro tendsto_cong) fastforce
  then show ?thesis
    using assms(1) continuous_at_enn2ereal isCont_tendsto_compose x by fastforce
qed

lemma tendsto_ennreal_iff[simp]:
  "\\<^sub>F x in F. 0 \ f x \ 0 \ x \ ((\x. ennreal (f x)) \ ennreal x) F \ (f \ x) F"
  by (auto dest: tendsto_ennrealD)
     (auto simp: ennreal_def
           intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)

lemma tendsto_enn2ereal_iff[simp]: "((\i. enn2ereal (f i)) \ enn2ereal x) F \ (f \ x) F"
  using continuous_on_enn2ereal[THEN continuous_on_tendsto_compose, of f x F]
    continuous_on_e2ennreal[THEN continuous_on_tendsto_compose, of "\x. enn2ereal (f x)" "enn2ereal x" F UNIV]
  by auto

lemma ennreal_tendsto_0_iff: "(\n. f n \ 0) \ ((\n. ennreal (f n)) \ 0) \ (f \ 0)"
  by (metis (mono_tags) ennreal_0 eventuallyI order_refl tendsto_ennreal_iff)
    
lemma continuous_on_add_ennreal:
  fixes f g :: "'a::topological_space \ ennreal"
  shows "continuous_on A f \ continuous_on A g \ continuous_on A (\x. f x + g x)"
  by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)

lemma continuous_on_inverse_ennreal[continuous_intros]:
  fixes f :: "'a::topological_space \ ennreal"
  shows "continuous_on A f \ continuous_on A (\x. inverse (f x))"
proof (transfer fixing: A)
  show "pred_fun top ((\) 0) f \ continuous_on A (\x. inverse (f x))" if "continuous_on A f"
    for f :: "'a \ ereal"
    using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
qed

instance ennreal :: topological_comm_monoid_add
proof
  show "((\x. fst x + snd x) \ a + b) (nhds a \\<^sub>F nhds b)" for a b :: ennreal
    using continuous_on_add_ennreal[of UNIV fst snd]
    using tendsto_at_iff_tendsto_nhds[symmetric, of "\x::(ennreal \ ennreal). fst x + snd x"]
    by (auto simp: continuous_on_eq_continuous_at)
       (simp add: isCont_def nhds_prod[symmetric])
qed

lemma sup_continuous_add_ennreal[order_continuous_intros]:
  fixes f g :: "'a::complete_lattice \ ennreal"
  shows "sup_continuous f \ sup_continuous g \ sup_continuous (\x. f x + g x)"
  by transfer (auto intro!: sup_continuous_add)

lemma ennreal_suminf_lessD: "(\i. f i :: ennreal) < x \ f i < x"
  using le_less_trans[OF sum_le_suminf[OF summableI, of "{i}" f]] by simp

lemma sums_ennreal[simp]: "(\i. 0 \ f i) \ 0 \ x \ (\i. ennreal (f i)) sums ennreal x \ f sums x"
  unfolding sums_def by (simp add: always_eventually sum_nonneg)

lemma summable_suminf_not_top: "(\i. 0 \ f i) \ (\i. ennreal (f i)) \ top \ summable f"
  using summable_sums[OF summableI, of "\i. ennreal (f i)"]
  by (cases "\i. ennreal (f i)" rule: ennreal_cases)
     (auto simp: summable_def)

lemma suminf_ennreal[simp]:
  "(\i. 0 \ f i) \ (\i. ennreal (f i)) \ top \ (\i. ennreal (f i)) = ennreal (\i. f i)"
  by (rule sums_unique[symmetric]) (simp add: summable_suminf_not_top suminf_nonneg summable_sums)

lemma sums_enn2ereal[simp]: "(\i. enn2ereal (f i)) sums enn2ereal x \ f sums x"
  unfolding sums_def by (simp add: always_eventually sum_nonneg)

lemma suminf_enn2ereal[simp]: "(\i. enn2ereal (f i)) = enn2ereal (suminf f)"
  by (rule sums_unique[symmetric]) (simp add: summable_sums)

lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal suminf suminf"
  by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)

lemma ennreal_suminf_cmult[simp]: "(\i. r * f i) = r * (\i. f i::ennreal)"
  by transfer (auto intro!: suminf_cmult_ereal)

lemma ennreal_suminf_multc[simp]: "(\i. f i * r) = (\i. f i::ennreal) * r"
  using ennreal_suminf_cmult[of r f] by (simp add: ac_simps)

lemma ennreal_suminf_divide[simp]: "(\i. f i / r) = (\i. f i::ennreal) / r"
  by (simp add: divide_ennreal_def)

lemma ennreal_suminf_neq_top: "summable f \ (\i. 0 \ f i) \ (\i. ennreal (f i)) \ top"
  using sums_ennreal[of f "suminf f"]
  by (simp add: suminf_nonneg flip: sums_unique summable_sums_iff del: sums_ennreal)

lemma suminf_ennreal_eq:
  "(\i. 0 \ f i) \ f sums x \ (\i. ennreal (f i)) = ennreal x"
  using suminf_nonneg[of f] sums_unique[of f x]
  by (intro sums_unique[symmetric]) (auto simp: summable_sums_iff)

lemma ennreal_suminf_bound_add:
  fixes f :: "nat \ ennreal"
  shows "(\N. (\n x) \ suminf f + y \ x"
  by transfer (auto intro!: suminf_bound_add)

lemma ennreal_suminf_SUP_eq_directed:
  fixes f :: "'a \ nat \ ennreal"
  assumes *: "\N i j. i \ I \ j \ I \ finite N \ \k\I. \n\N. f i n \ f k n \ f j n \ f k n"
  shows "(\n. SUP i\I. f i n) = (SUP i\I. \n. f i n)"
proof cases
  assume "I \ {}"
  then obtain i where "i \ I" by auto
  from * show ?thesis
    by (transfer fixing: I)
       (auto simp: max_absorb2 SUP_upper2[OF \<open>i \<in> I\<close>] suminf_nonneg summable_ereal_pos \<open>I \<noteq> {}\<close>
             intro!: suminf_SUP_eq_directed)
qed (simp add: bot_ennreal)

lemma INF_ennreal_add_const:
  fixes f g :: "nat \ ennreal"
  shows "(INF i. f i + c) = (INF i. f i) + c"
  using continuous_at_Inf_mono[of "\x. x + c" "f`UNIV"]
  using continuous_add[of "at_right (Inf (range f))", of "\x. x" "\x. c"]
  by (auto simp: mono_def image_comp)

lemma INF_ennreal_const_add:
  fixes f g :: "nat \ ennreal"
  shows "(INF i. c + f i) = c + (INF i. f i)"
  using INF_ennreal_add_const[of f c] by (simp add: ac_simps)

lemma SUP_mult_left_ennreal: "c * (SUP i\I. f i) = (SUP i\I. c * f i ::ennreal)"
proof cases
  assume "I \ {}" then show ?thesis
    by transfer (auto simp add: SUP_ereal_mult_left max_absorb2 SUP_upper2)
qed (simp add: bot_ennreal)

lemma SUP_mult_right_ennreal: "(SUP i\I. f i) * c = (SUP i\I. f i * c ::ennreal)"
  using SUP_mult_left_ennreal by (simp add: mult.commute)

lemma SUP_divide_ennreal: "(SUP i\I. f i) / c = (SUP i\I. f i / c ::ennreal)"
  using SUP_mult_right_ennreal by (simp add: divide_ennreal_def)

lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
proof (intro antisym top_greatest le_SUP_iff[THEN iffD2] allI impI)
  fix y :: ennreal assume "y < top"
  then obtain r where "y = ennreal r"
    by (cases y rule: ennreal_cases) auto
  then show "\i\UNIV. y < of_nat i"
    using reals_Archimedean2[of "max 1 r"] zero_less_one
    by (simp add: ennreal_Ex_less_of_nat)
qed

lemma ennreal_SUP_eq_top:
  fixes f :: "'a \ ennreal"
  assumes "\n. \i\I. of_nat n \ f i"
  shows "(SUP i \ I. f i) = top"
proof -
  have "(SUP x. of_nat x :: ennreal) \ (SUP i \ I. f i)"
    using assms by (auto intro!: SUP_least intro: SUP_upper2)
  then show ?thesis
    by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
qed

lemma ennreal_INF_const_minus:
  fixes f :: "'a \ ennreal"
  shows "I \ {} \ (SUP x\I. c - f x) = c - (INF x\I. f x)"
  by (transfer fixing: I)
     (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)

lemma of_nat_Sup_ennreal:
  assumes "A \ {}" "bdd_above A"
  shows "of_nat (Sup A) = (SUP a\A. of_nat a :: ennreal)"
proof (intro antisym)
  show "(SUP a\A. of_nat a::ennreal) \ of_nat (Sup A)"
    by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
  have "Sup A \ A"
    using assms by (auto simp: Sup_nat_def bdd_above_nat)
  then show "of_nat (Sup A) \ (SUP a\A. of_nat a::ennreal)"
    by (intro SUP_upper)
qed

lemma ennreal_tendsto_const_minus:
  fixes g :: "'a \ ennreal"
  assumes ae: "\\<^sub>F x in F. g x \ c"
  assumes g: "((\x. c - g x) \ 0) F"
  shows "(g \ c) F"
proof (cases c rule: ennreal_cases)
  case top with tendsto_unique[OF _ g, of "top"] show ?thesis
    by (cases "F = bot") auto
next
  case (real r)
  then have "\x. \q\0. g x \ c \ (g x = ennreal q \ q \ r)"
    by (auto simp: le_ennreal_iff)
  then obtain f where *: "0 \ f x" "g x = ennreal (f x)" "f x \ r" if "g x \ c" for x
    by metis
  from ae have ae2: "\\<^sub>F x in F. c - g x = ennreal (r - f x) \ f x \ r \ g x = ennreal (f x) \ 0 \ f x"
  proof eventually_elim
    fix x assume "g x \ c" with *[of x] \0 \ r\ show "c - g x = ennreal (r - f x) \ f x \ r \ g x = ennreal (f x) \ 0 \ f x"
      by (auto simp: real ennreal_minus)
  qed
  with g have "((\x. ennreal (r - f x)) \ ennreal 0) F"
    by (auto simp add: tendsto_cong eventually_conj_iff)
  with ae2 have "((\x. r - f x) \ 0) F"
    by (subst (asm) tendsto_ennreal_iff) (auto elim: eventually_mono)
  then have "(f \ r) F"
    by (rule Lim_transform2[OF tendsto_const])
  with ae2 have "((\x. ennreal (f x)) \ ennreal r) F"
    by (subst tendsto_ennreal_iff) (auto elim: eventually_mono simp: real)
  with ae2 show ?thesis
    by (auto simp: real tendsto_cong eventually_conj_iff)
qed

lemma ennreal_SUP_add:
  fixes f g :: "nat \ ennreal"
  shows "incseq f \ incseq g \ (SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
  unfolding incseq_def le_fun_def
  by transfer
     (simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)

lemma ennreal_SUP_sum:
  fixes f :: "'a \ nat \ ennreal"
  shows "(\i. i \ I \ incseq (f i)) \ (SUP n. \i\I. f i n) = (\i\I. SUP n. f i n)"
  unfolding incseq_def
  by transfer
     (simp add: SUP_ereal_sum incseq_def SUP_upper2 max_absorb2 sum_nonneg)

lemma ennreal_liminf_minus:
  fixes f :: "nat \ ennreal"
  shows "(\n. f n \ c) \ liminf (\n. c - f n) = c - limsup f"
  apply transfer
  apply (simp add: ereal_diff_positive max.absorb2 liminf_ereal_cminus)
  apply (subst max.absorb2)
  apply (rule ereal_diff_positive)
  apply (rule Limsup_bounded)
  apply auto
  done

lemma ennreal_continuous_on_cmult:
  "(c::ennreal) < top \ continuous_on A f \ continuous_on A (\x. c * f x)"
  by (transfer fixing: A) (auto intro: continuous_on_cmult_ereal)

lemma ennreal_tendsto_cmult:
  "(c::ennreal) < top \ (f \ x) F \ ((\x. c * f x) \ c * x) F"
  by (rule continuous_on_tendsto_compose[where g=f, OF ennreal_continuous_on_cmult, where s=UNIV])
     (auto simp: continuous_on_id)

lemma tendsto_ennrealI[intro, simp, tendsto_intros]:
  "(f \ x) F \ ((\x. ennreal (f x)) \ ennreal x) F"
  by (auto simp: ennreal_def
           intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)

lemma tendsto_enn2erealI [tendsto_intros]:
  assumes "(f \ l) F"
  shows "((\i. enn2ereal(f i)) \ enn2ereal l) F"
using tendsto_enn2ereal_iff assms by auto

lemma tendsto_e2ennrealI [tendsto_intros]:
  assumes "(f \ l) F"
  shows "((\i. e2ennreal(f i)) \ e2ennreal l) F"
proof -
  have *: "e2ennreal (max x 0) = e2ennreal x" for x
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.63Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff