Theory Extended_Real

theory Extended_Real
imports Extended_Nat Liminf_Limsup
(*  Title:      HOL/Library/Extended_Real.thy
Author: Johannes Hölzl, TU München
Author: Robert Himmelmann, TU München
Author: Armin Heller, TU München
Author: Bogdan Grechuk, University of Edinburgh
*)


header {* Extended real number line *}

theory Extended_Real
imports Complex_Main Extended_Nat Liminf_Limsup
begin

text {*

For more lemmas about the extended real numbers go to
@{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}

*}


subsection {* Definition and basic properties *}

datatype ereal = ereal real | PInfty | MInfty

instantiation ereal :: uminus
begin

fun uminus_ereal where
"- (ereal r) = ereal (- r)"
| "- PInfty = MInfty"
| "- MInfty = PInfty"

instance ..

end

instantiation ereal :: infinity
begin

definition "(∞::ereal) = PInfty"
instance ..

end

declare [[coercion "ereal :: real => ereal"]]

lemma ereal_uminus_uminus[simp]:
fixes a :: ereal
shows "- (- a) = a"
by (cases a) simp_all

lemma
shows PInfty_eq_infinity[simp]: "PInfty = ∞"
and MInfty_eq_minfinity[simp]: "MInfty = - ∞"
and MInfty_neq_PInfty[simp]: "∞ ≠ - (∞::ereal)" "- ∞ ≠ (∞::ereal)"
and MInfty_neq_ereal[simp]: "ereal r ≠ - ∞" "- ∞ ≠ ereal r"
and PInfty_neq_ereal[simp]: "ereal r ≠ ∞" "∞ ≠ ereal r"
and PInfty_cases[simp]: "(case ∞ of ereal r => f r | PInfty => y | MInfty => z) = y"
and MInfty_cases[simp]: "(case - ∞ of ereal r => f r | PInfty => y | MInfty => z) = z"
by (simp_all add: infinity_ereal_def)

declare
PInfty_eq_infinity[code_post]
MInfty_eq_minfinity[code_post]

lemma [code_unfold]:
"∞ = PInfty"
"- PInfty = MInfty"
by simp_all

lemma inj_ereal[simp]: "inj_on ereal A"
unfolding inj_on_def by auto

lemma ereal_cases[case_names real PInf MInf, cases type: ereal]:
assumes "!!r. x = ereal r ==> P"
assumes "x = ∞ ==> P"
assumes "x = -∞ ==> P"
shows P
using assms by (cases x) auto

lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]

lemma ereal_uminus_eq_iff[simp]:
fixes a b :: ereal
shows "-a = -b <-> a = b"
by (cases rule: ereal2_cases[of a b]) simp_all

function of_ereal :: "ereal => real" where
"of_ereal (ereal r) = r"
| "of_ereal ∞ = 0"
| "of_ereal (-∞) = 0"
by (auto intro: ereal_cases)
termination by default (rule wf_empty)

defs (overloaded)
real_of_ereal_def [code_unfold]: "real ≡ of_ereal"

lemma real_of_ereal[simp]:
"real (- x :: ereal) = - (real x)"
"real (ereal r) = r"
"real (∞::ereal) = 0"
by (cases x) (simp_all add: real_of_ereal_def)

lemma range_ereal[simp]: "range ereal = UNIV - {∞, -∞}"
proof safe
fix x
assume "x ∉ range ereal" "x ≠ ∞"
then show "x = -∞"
by (cases x) auto
qed auto

lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"
proof safe
fix x :: ereal
show "x ∈ range uminus"
by (intro image_eqI[of _ _ "-x"]) auto
qed auto

instantiation ereal :: abs
begin

function abs_ereal where
"¦ereal r¦ = ereal ¦r¦"
| "¦-∞¦ = (∞::ereal)"
| "¦∞¦ = (∞::ereal)"
by (auto intro: ereal_cases)
termination proof qed (rule wf_empty)

instance ..

end

lemma abs_eq_infinity_cases[elim!]:
fixes x :: ereal
assumes "¦x¦ = ∞"
obtains "x = ∞" | "x = -∞"
using assms by (cases x) auto

lemma abs_neq_infinity_cases[elim!]:
fixes x :: ereal
assumes "¦x¦ ≠ ∞"
obtains r where "x = ereal r"
using assms by (cases x) auto

lemma abs_ereal_uminus[simp]:
fixes x :: ereal
shows "¦- x¦ = ¦x¦"
by (cases x) auto

lemma ereal_infinity_cases:
fixes a :: ereal
shows "a ≠ ∞ ==> a ≠ -∞ ==> ¦a¦ ≠ ∞"
by auto


subsubsection "Addition"

instantiation ereal :: "{one,comm_monoid_add}"
begin

definition "0 = ereal 0"
definition "1 = ereal 1"

function plus_ereal where
"ereal r + ereal p = ereal (r + p)"
| "∞ + a = (∞::ereal)"
| "a + ∞ = (∞::ereal)"
| "ereal r + -∞ = - ∞"
| "-∞ + ereal p = -(∞::ereal)"
| "-∞ + -∞ = -(∞::ereal)"
proof -
case (goal1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
with goal1 show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
termination by default (rule wf_empty)

lemma Infty_neq_0[simp]:
"(∞::ereal) ≠ 0" "0 ≠ (∞::ereal)"
"-(∞::ereal) ≠ 0" "0 ≠ -(∞::ereal)"
by (simp_all add: zero_ereal_def)

lemma ereal_eq_0[simp]:
"ereal r = 0 <-> r = 0"
"0 = ereal r <-> r = 0"
unfolding zero_ereal_def by simp_all

instance
proof
fix a b c :: ereal
show "0 + a = a"
by (cases a) (simp_all add: zero_ereal_def)
show "a + b = b + a"
by (cases rule: ereal2_cases[of a b]) simp_all
show "a + b + c = a + (b + c)"
by (cases rule: ereal3_cases[of a b c]) simp_all
qed

end

instance ereal :: numeral ..

lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
unfolding real_of_ereal_def zero_ereal_def by simp

lemma abs_ereal_zero[simp]: "¦0¦ = (0::ereal)"
unfolding zero_ereal_def abs_ereal.simps by simp

lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)"
by (simp add: zero_ereal_def)

lemma ereal_uminus_zero_iff[simp]:
fixes a :: ereal
shows "-a = 0 <-> a = 0"
by (cases a) simp_all

lemma ereal_plus_eq_PInfty[simp]:
fixes a b :: ereal
shows "a + b = ∞ <-> a = ∞ ∨ b = ∞"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_plus_eq_MInfty[simp]:
fixes a b :: ereal
shows "a + b = -∞ <-> (a = -∞ ∨ b = -∞) ∧ a ≠ ∞ ∧ b ≠ ∞"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_add_cancel_left:
fixes a b :: ereal
assumes "a ≠ -∞"
shows "a + b = a + c <-> a = ∞ ∨ b = c"
using assms by (cases rule: ereal3_cases[of a b c]) auto

lemma ereal_add_cancel_right:
fixes a b :: ereal
assumes "a ≠ -∞"
shows "b + a = c + a <-> a = ∞ ∨ b = c"
using assms by (cases rule: ereal3_cases[of a b c]) auto

lemma ereal_real: "ereal (real x) = (if ¦x¦ = ∞ then 0 else x)"
by (cases x) simp_all

lemma real_of_ereal_add:
fixes a b :: ereal
shows "real (a + b) =
(if (¦a¦ = ∞) ∧ (¦b¦ = ∞) ∨ (¦a¦ ≠ ∞) ∧ (¦b¦ ≠ ∞) then real a + real b else 0)"

by (cases rule: ereal2_cases[of a b]) auto


subsubsection "Linear order on @{typ ereal}"

instantiation ereal :: linorder
begin

function less_ereal
where
" ereal x < ereal y <-> x < y"
| "(∞::ereal) < a <-> False"
| " a < -(∞::ereal) <-> False"
| "ereal x < ∞ <-> True"
| " -∞ < ereal r <-> True"
| " -∞ < (∞::ereal) <-> True"
proof -
case (goal1 P x)
then obtain a b where "x = (a,b)" by (cases x) auto
with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp

definition "x ≤ (y::ereal) <-> x < y ∨ x = y"

lemma ereal_infty_less[simp]:
fixes x :: ereal
shows "x < ∞ <-> (x ≠ ∞)"
"-∞ < x <-> (x ≠ -∞)"
by (cases x, simp_all) (cases x, simp_all)

lemma ereal_infty_less_eq[simp]:
fixes x :: ereal
shows "∞ ≤ x <-> x = ∞"
and "x ≤ -∞ <-> x = -∞"
by (auto simp add: less_eq_ereal_def)

lemma ereal_less[simp]:
"ereal r < 0 <-> (r < 0)"
"0 < ereal r <-> (0 < r)"
"0 < (∞::ereal)"
"-(∞::ereal) < 0"
by (simp_all add: zero_ereal_def)

lemma ereal_less_eq[simp]:
"x ≤ (∞::ereal)"
"-(∞::ereal) ≤ x"
"ereal r ≤ ereal p <-> r ≤ p"
"ereal r ≤ 0 <-> r ≤ 0"
"0 ≤ ereal r <-> 0 ≤ r"
by (auto simp add: less_eq_ereal_def zero_ereal_def)

lemma ereal_infty_less_eq2:
"a ≤ b ==> a = ∞ ==> b = (∞::ereal)"
"a ≤ b ==> b = -∞ ==> a = -(∞::ereal)"
by simp_all

instance
proof
fix x y z :: ereal
show "x ≤ x"
by (cases x) simp_all
show "x < y <-> x ≤ y ∧ ¬ y ≤ x"
by (cases rule: ereal2_cases[of x y]) auto
show "x ≤ y ∨ y ≤ x "
by (cases rule: ereal2_cases[of x y]) auto
{
assume "x ≤ y" "y ≤ x"
then show "x = y"
by (cases rule: ereal2_cases[of x y]) auto
}
{
assume "x ≤ y" "y ≤ z"
then show "x ≤ z"
by (cases rule: ereal3_cases[of x y z]) auto
}
qed

end

lemma ereal_dense2: "x < y ==> ∃z. x < ereal z ∧ ereal z < y"
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto

instance ereal :: dense_linorder
by default (blast dest: ereal_dense2)

instance ereal :: ordered_ab_semigroup_add
proof
fix a b c :: ereal
assume "a ≤ b"
then show "c + a ≤ c + b"
by (cases rule: ereal3_cases[of a b c]) auto
qed

lemma real_of_ereal_positive_mono:
fixes x y :: ereal
shows "0 ≤ x ==> x ≤ y ==> y ≠ ∞ ==> real x ≤ real y"
by (cases rule: ereal2_cases[of x y]) auto

lemma ereal_MInfty_lessI[intro, simp]:
fixes a :: ereal
shows "a ≠ -∞ ==> -∞ < a"
by (cases a) auto

lemma ereal_less_PInfty[intro, simp]:
fixes a :: ereal
shows "a ≠ ∞ ==> a < ∞"
by (cases a) auto

lemma ereal_less_ereal_Ex:
fixes a b :: ereal
shows "x < ereal r <-> x = -∞ ∨ (∃p. p < r ∧ x = ereal p)"
by (cases x) auto

lemma less_PInf_Ex_of_nat: "x ≠ ∞ <-> (∃n::nat. x < ereal (real n))"
proof (cases x)
case (real r)
then show ?thesis
using reals_Archimedean2[of r] by simp
qed simp_all

lemma ereal_add_mono:
fixes a b c d :: ereal
assumes "a ≤ b"
and "c ≤ d"
shows "a + c ≤ b + d"
using assms
apply (cases a)
apply (cases rule: ereal3_cases[of b c d], auto)
apply (cases rule: ereal3_cases[of b c d], auto)
done

lemma ereal_minus_le_minus[simp]:
fixes a b :: ereal
shows "- a ≤ - b <-> b ≤ a"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_minus_less_minus[simp]:
fixes a b :: ereal
shows "- a < - b <-> b < a"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_le_real_iff:
"x ≤ real y <-> (¦y¦ ≠ ∞ --> ereal x ≤ y) ∧ (¦y¦ = ∞ --> x ≤ 0)"
by (cases y) auto

lemma real_le_ereal_iff:
"real y ≤ x <-> (¦y¦ ≠ ∞ --> y ≤ ereal x) ∧ (¦y¦ = ∞ --> 0 ≤ x)"
by (cases y) auto

lemma ereal_less_real_iff:
"x < real y <-> (¦y¦ ≠ ∞ --> ereal x < y) ∧ (¦y¦ = ∞ --> x < 0)"
by (cases y) auto

lemma real_less_ereal_iff:
"real y < x <-> (¦y¦ ≠ ∞ --> y < ereal x) ∧ (¦y¦ = ∞ --> 0 < x)"
by (cases y) auto

lemma real_of_ereal_pos:
fixes x :: ereal
shows "0 ≤ x ==> 0 ≤ real x" by (cases x) auto

lemmas real_of_ereal_ord_simps =
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff

lemma abs_ereal_ge0[simp]: "0 ≤ x ==> ¦x :: ereal¦ = x"
by (cases x) auto

lemma abs_ereal_less0[simp]: "x < 0 ==> ¦x :: ereal¦ = -x"
by (cases x) auto

lemma abs_ereal_pos[simp]: "0 ≤ ¦x :: ereal¦"
by (cases x) auto

lemma real_of_ereal_le_0[simp]: "real (x :: ereal) ≤ 0 <-> x ≤ 0 ∨ x = ∞"
by (cases x) auto

lemma abs_real_of_ereal[simp]: "¦real (x :: ereal)¦ = real ¦x¦"
by (cases x) auto

lemma zero_less_real_of_ereal:
fixes x :: ereal
shows "0 < real x <-> 0 < x ∧ x ≠ ∞"
by (cases x) auto

lemma ereal_0_le_uminus_iff[simp]:
fixes a :: ereal
shows "0 ≤ - a <-> a ≤ 0"
by (cases rule: ereal2_cases[of a]) auto

lemma ereal_uminus_le_0_iff[simp]:
fixes a :: ereal
shows "- a ≤ 0 <-> 0 ≤ a"
by (cases rule: ereal2_cases[of a]) auto

lemma ereal_add_strict_mono:
fixes a b c d :: ereal
assumes "a = b"
and "0 ≤ a"
and "a ≠ ∞"
and "c < d"
shows "a + c < b + d"
using assms
by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto

lemma ereal_less_add:
fixes a b c :: ereal
shows "¦a¦ ≠ ∞ ==> c < b ==> a + c < a + b"
by (cases rule: ereal2_cases[of b c]) auto

lemma ereal_uminus_eq_reorder: "- a = b <-> a = (-b::ereal)"
by auto

lemma ereal_uminus_less_reorder: "- a < b <-> -b < (a::ereal)"
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)

lemma ereal_uminus_le_reorder: "- a ≤ b <-> -b ≤ (a::ereal)"
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)

lemmas ereal_uminus_reorder =
ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder

lemma ereal_bot:
fixes x :: ereal
assumes "!!B. x ≤ ereal B"
shows "x = - ∞"
proof (cases x)
case (real r)
with assms[of "r - 1"] show ?thesis
by auto
next
case PInf
with assms[of 0] show ?thesis
by auto
next
case MInf
then show ?thesis
by simp
qed

lemma ereal_top:
fixes x :: ereal
assumes "!!B. x ≥ ereal B"
shows "x = ∞"
proof (cases x)
case (real r)
with assms[of "r + 1"] show ?thesis
by auto
next
case MInf
with assms[of 0] show ?thesis
by auto
next
case PInf
then show ?thesis
by simp
qed

lemma
shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)"
and ereal_min[simp]: "ereal (min x y) = min (ereal x) (ereal y)"
by (simp_all add: min_def max_def)

lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)"
by (auto simp: zero_ereal_def)

lemma
fixes f :: "nat => ereal"
shows incseq_uminus[simp]: "incseq (λx. - f x) <-> decseq f"
and decseq_uminus[simp]: "decseq (λx. - f x) <-> incseq f"
unfolding decseq_def incseq_def by auto

lemma incseq_ereal: "incseq f ==> incseq (λx. ereal (f x))"
unfolding incseq_def by auto

lemma ereal_add_nonneg_nonneg:
fixes a b :: ereal
shows "0 ≤ a ==> 0 ≤ b ==> 0 ≤ a + b"
using add_mono[of 0 a 0 b] by simp

lemma image_eqD: "f ` A = B ==> ∀x∈A. f x ∈ B"
by auto

lemma incseq_setsumI:
fixes f :: "nat => 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
assumes "!!i. 0 ≤ f i"
shows "incseq (λi. setsum f {..< i})"
proof (intro incseq_SucI)
fix n
have "setsum f {..< n} + 0 ≤ setsum f {..<n} + f n"
using assms by (rule add_left_mono)
then show "setsum f {..< n} ≤ setsum f {..< Suc n}"
by auto
qed

lemma incseq_setsumI2:
fixes f :: "'i => nat => 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
assumes "!!n. n ∈ A ==> incseq (f n)"
shows "incseq (λi. ∑n∈A. f n i)"
using assms
unfolding incseq_def by (auto intro: setsum_mono)


subsubsection "Multiplication"

instantiation ereal :: "{comm_monoid_mult,sgn}"
begin

function sgn_ereal :: "ereal => ereal" where
"sgn (ereal r) = ereal (sgn r)"
| "sgn (∞::ereal) = 1"
| "sgn (-∞::ereal) = -1"
by (auto intro: ereal_cases)
termination by default (rule wf_empty)

function times_ereal where
"ereal r * ereal p = ereal (r * p)"
| "ereal r * ∞ = (if r = 0 then 0 else if r > 0 then ∞ else -∞)"
| "∞ * ereal r = (if r = 0 then 0 else if r > 0 then ∞ else -∞)"
| "ereal r * -∞ = (if r = 0 then 0 else if r > 0 then -∞ else ∞)"
| "-∞ * ereal r = (if r = 0 then 0 else if r > 0 then -∞ else ∞)"
| "(∞::ereal) * ∞ = ∞"
| "-(∞::ereal) * ∞ = -∞"
| "(∞::ereal) * -∞ = -∞"
| "-(∞::ereal) * -∞ = ∞"
proof -
case (goal1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
with goal1 show P
by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp

instance
proof
fix a b c :: ereal
show "1 * a = a"
by (cases a) (simp_all add: one_ereal_def)
show "a * b = b * a"
by (cases rule: ereal2_cases[of a b]) simp_all
show "a * b * c = a * (b * c)"
by (cases rule: ereal3_cases[of a b c])
(simp_all add: zero_ereal_def zero_less_mult_iff)
qed

end

lemma real_ereal_1[simp]: "real (1::ereal) = 1"
unfolding one_ereal_def by simp

lemma real_of_ereal_le_1:
fixes a :: ereal
shows "a ≤ 1 ==> real a ≤ 1"
by (cases a) (auto simp: one_ereal_def)

lemma abs_ereal_one[simp]: "¦1¦ = (1::ereal)"
unfolding one_ereal_def by simp

lemma ereal_mult_zero[simp]:
fixes a :: ereal
shows "a * 0 = 0"
by (cases a) (simp_all add: zero_ereal_def)

lemma ereal_zero_mult[simp]:
fixes a :: ereal
shows "0 * a = 0"
by (cases a) (simp_all add: zero_ereal_def)

lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
by (simp add: zero_ereal_def one_ereal_def)

lemma ereal_zero_m1[simp]: "1 ≠ (0::ereal)"
by (simp add: zero_ereal_def one_ereal_def)

lemma ereal_times_0[simp]:
fixes x :: ereal
shows "0 * x = 0"
by (cases x) (auto simp: zero_ereal_def)

lemma ereal_times[simp]:
"1 ≠ (∞::ereal)" "(∞::ereal) ≠ 1"
"1 ≠ -(∞::ereal)" "-(∞::ereal) ≠ 1"
by (auto simp add: times_ereal_def one_ereal_def)

lemma ereal_plus_1[simp]:
"1 + ereal r = ereal (r + 1)"
"ereal r + 1 = ereal (r + 1)"
"1 + -(∞::ereal) = -∞"
"-(∞::ereal) + 1 = -∞"
unfolding one_ereal_def by auto

lemma ereal_zero_times[simp]:
fixes a b :: ereal
shows "a * b = 0 <-> a = 0 ∨ b = 0"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_eq_PInfty[simp]:
"a * b = (∞::ereal) <->
(a = ∞ ∧ b > 0) ∨ (a > 0 ∧ b = ∞) ∨ (a = -∞ ∧ b < 0) ∨ (a < 0 ∧ b = -∞)"

by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_eq_MInfty[simp]:
"a * b = -(∞::ereal) <->
(a = ∞ ∧ b < 0) ∨ (a < 0 ∧ b = ∞) ∨ (a = -∞ ∧ b > 0) ∨ (a > 0 ∧ b = -∞)"

by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
by (simp_all add: zero_ereal_def one_ereal_def)

lemma ereal_zero_one[simp]: "0 ≠ (1::ereal)"
by (simp_all add: zero_ereal_def one_ereal_def)

lemma ereal_mult_minus_left[simp]:
fixes a b :: ereal
shows "-a * b = - (a * b)"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_minus_right[simp]:
fixes a b :: ereal
shows "a * -b = - (a * b)"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_infty[simp]:
"a * (∞::ereal) = (if a = 0 then 0 else if 0 < a then ∞ else - ∞)"
by (cases a) auto

lemma ereal_infty_mult[simp]:
"(∞::ereal) * a = (if a = 0 then 0 else if 0 < a then ∞ else - ∞)"
by (cases a) auto

lemma ereal_mult_strict_right_mono:
assumes "a < b"
and "0 < c"
and "c < (∞::ereal)"
shows "a * c < b * c"
using assms
by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff)

lemma ereal_mult_strict_left_mono:
"a < b ==> 0 < c ==> c < (∞::ereal) ==> c * a < c * b"
using ereal_mult_strict_right_mono
by (simp add: mult_commute[of c])

lemma ereal_mult_right_mono:
fixes a b c :: ereal
shows "a ≤ b ==> 0 ≤ c ==> a * c ≤ b * c"
using assms
apply (cases "c = 0")
apply simp
apply (cases rule: ereal3_cases[of a b c])
apply (auto simp: zero_le_mult_iff)
done

lemma ereal_mult_left_mono:
fixes a b c :: ereal
shows "a ≤ b ==> 0 ≤ c ==> c * a ≤ c * b"
using ereal_mult_right_mono
by (simp add: mult_commute[of c])

lemma zero_less_one_ereal[simp]: "0 ≤ (1::ereal)"
by (simp add: one_ereal_def zero_ereal_def)

lemma ereal_0_le_mult[simp]: "0 ≤ a ==> 0 ≤ b ==> 0 ≤ a * (b :: ereal)"
by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)

lemma ereal_right_distrib:
fixes r a b :: ereal
shows "0 ≤ a ==> 0 ≤ b ==> r * (a + b) = r * a + r * b"
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)

lemma ereal_left_distrib:
fixes r a b :: ereal
shows "0 ≤ a ==> 0 ≤ b ==> (a + b) * r = a * r + b * r"
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)

lemma ereal_mult_le_0_iff:
fixes a b :: ereal
shows "a * b ≤ 0 <-> (0 ≤ a ∧ b ≤ 0) ∨ (a ≤ 0 ∧ 0 ≤ b)"
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff)

lemma ereal_zero_le_0_iff:
fixes a b :: ereal
shows "0 ≤ a * b <-> (0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0)"
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff)

lemma ereal_mult_less_0_iff:
fixes a b :: ereal
shows "a * b < 0 <-> (0 < a ∧ b < 0) ∨ (a < 0 ∧ 0 < b)"
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff)

lemma ereal_zero_less_0_iff:
fixes a b :: ereal
shows "0 < a * b <-> (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0)"
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)

lemma ereal_left_mult_cong:
fixes a b c :: ereal
shows "(c ≠ 0 ==> a = b) ==> c * a = c * b"
by (cases "c = 0") simp_all

lemma ereal_right_mult_cong:
fixes a b c :: ereal
shows "(c ≠ 0 ==> a = b) ==> a * c = b * c"
by (cases "c = 0") simp_all

lemma ereal_distrib:
fixes a b c :: ereal
assumes "a ≠ ∞ ∨ b ≠ -∞"
and "a ≠ -∞ ∨ b ≠ ∞"
and "¦c¦ ≠ ∞"
shows "(a + b) * c = a * c + b * c"
using assms
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
apply (induct w rule: num_induct)
apply (simp only: numeral_One one_ereal_def)
apply (simp only: numeral_inc ereal_plus_1)
done

lemma ereal_le_epsilon:
fixes x y :: ereal
assumes "∀e. 0 < e --> x ≤ y + e"
shows "x ≤ y"
proof -
{
assume a: "∃r. y = ereal r"
then obtain r where r_def: "y = ereal r"
by auto
{
assume "x = -∞"
then have ?thesis by auto
}
moreover
{
assume "x ≠ -∞"
then obtain p where p_def: "x = ereal p"
using a assms[rule_format, of 1]
by (cases x) auto
{
fix e
have "0 < e --> p ≤ r + e"
using assms[rule_format, of "ereal e"] p_def r_def by auto
}
then have "p ≤ r"
apply (subst field_le_epsilon)
apply auto
done
then have ?thesis
using r_def p_def by auto
}
ultimately have ?thesis
by blast
}
moreover
{
assume "y = -∞ | y = ∞"
then have ?thesis
using assms[rule_format, of 1] by (cases x) auto
}
ultimately show ?thesis
by (cases y) auto
qed

lemma ereal_le_epsilon2:
fixes x y :: ereal
assumes "∀e. 0 < e --> x ≤ y + ereal e"
shows "x ≤ y"
proof -
{
fix e :: ereal
assume "e > 0"
{
assume "e = ∞"
then have "x ≤ y + e"
by auto
}
moreover
{
assume "e ≠ ∞"
then obtain r where "e = ereal r"
using `e > 0` by (cases e) auto
then have "x ≤ y + e"
using assms[rule_format, of r] `e>0` by auto
}
ultimately have "x ≤ y + e"
by blast
}
then show ?thesis
using ereal_le_epsilon by auto
qed

lemma ereal_le_real:
fixes x y :: ereal
assumes "∀z. x ≤ ereal z --> y ≤ ereal z"
shows "y ≤ x"
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)

lemma setprod_ereal_0:
fixes f :: "'a => ereal"
shows "(∏i∈A. f i) = 0 <-> finite A ∧ (∃i∈A. f i = 0)"
proof (cases "finite A")
case True
then show ?thesis by (induct A) auto
next
case False
then show ?thesis by auto
qed

lemma setprod_ereal_pos:
fixes f :: "'a => ereal"
assumes pos: "!!i. i ∈ I ==> 0 ≤ f i"
shows "0 ≤ (∏i∈I. f i)"
proof (cases "finite I")
case True
from this pos show ?thesis
by induct auto
next
case False
then show ?thesis by simp
qed

lemma setprod_PInf:
fixes f :: "'a => ereal"
assumes "!!i. i ∈ I ==> 0 ≤ f i"
shows "(∏i∈I. f i) = ∞ <-> finite I ∧ (∃i∈I. f i = ∞) ∧ (∀i∈I. f i ≠ 0)"
proof (cases "finite I")
case True
from this assms show ?thesis
proof (induct I)
case (insert i I)
then have pos: "0 ≤ f i" "0 ≤ setprod f I"
by (auto intro!: setprod_ereal_pos)
from insert have "(∏j∈insert i I. f j) = ∞ <-> setprod f I * f i = ∞"
by auto
also have "… <-> (setprod f I = ∞ ∨ f i = ∞) ∧ f i ≠ 0 ∧ setprod f I ≠ 0"
using setprod_ereal_pos[of I f] pos
by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
also have "… <-> finite (insert i I) ∧ (∃j∈insert i I. f j = ∞) ∧ (∀j∈insert i I. f j ≠ 0)"
using insert by (auto simp: setprod_ereal_0)
finally show ?case .
qed simp
next
case False
then show ?thesis by simp
qed

lemma setprod_ereal: "(∏i∈A. ereal (f i)) = ereal (setprod f A)"
proof (cases "finite A")
case True
then show ?thesis
by induct (auto simp: one_ereal_def)
next
case False
then show ?thesis
by (simp add: one_ereal_def)
qed


subsubsection {* Power *}

lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
by (induct n) (auto simp: one_ereal_def)

lemma ereal_power_PInf[simp]: "(∞::ereal) ^ n = (if n = 0 then 1 else ∞)"
by (induct n) (auto simp: one_ereal_def)

lemma ereal_power_uminus[simp]:
fixes x :: ereal
shows "(- x) ^ n = (if even n then x ^ n else - (x^n))"
by (induct n) (auto simp: one_ereal_def)

lemma ereal_power_numeral[simp]:
"(numeral num :: ereal) ^ n = ereal (numeral num ^ n)"
by (induct n) (auto simp: one_ereal_def)

lemma zero_le_power_ereal[simp]:
fixes a :: ereal
assumes "0 ≤ a"
shows "0 ≤ a ^ n"
using assms by (induct n) (auto simp: ereal_zero_le_0_iff)


subsubsection {* Subtraction *}

lemma ereal_minus_minus_image[simp]:
fixes S :: "ereal set"
shows "uminus ` uminus ` S = S"
by (auto simp: image_iff)

lemma ereal_uminus_lessThan[simp]:
fixes a :: ereal
shows "uminus ` {..<a} = {-a<..}"
proof -
{
fix x
assume "-a < x"
then have "- x < - (- a)"
by (simp del: ereal_uminus_uminus)
then have "- x < a"
by simp
}
then show ?thesis
by (auto intro!: image_eqI)
qed

lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image)

instantiation ereal :: minus
begin

definition "x - y = x + -(y::ereal)"
instance ..

end

lemma ereal_minus[simp]:
"ereal r - ereal p = ereal (r - p)"
"-∞ - ereal r = -∞"
"ereal r - ∞ = -∞"
"(∞::ereal) - x = ∞"
"-(∞::ereal) - ∞ = -∞"
"x - -y = x + y"
"x - 0 = x"
"0 - x = -x"
by (simp_all add: minus_ereal_def)

lemma ereal_x_minus_x[simp]: "x - x = (if ¦x¦ = ∞ then ∞ else 0::ereal)"
by (cases x) simp_all

lemma ereal_eq_minus_iff:
fixes x y z :: ereal
shows "x = z - y <->
(¦y¦ ≠ ∞ --> x + y = z) ∧
(y = -∞ --> x = ∞) ∧
(y = ∞ --> z = ∞ --> x = ∞) ∧
(y = ∞ --> z ≠ ∞ --> x = -∞)"

by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_eq_minus:
fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ==> x = z - y <-> x + y = z"
by (auto simp: ereal_eq_minus_iff)

lemma ereal_less_minus_iff:
fixes x y z :: ereal
shows "x < z - y <->
(y = ∞ --> z = ∞ ∧ x ≠ ∞) ∧
(y = -∞ --> x ≠ ∞) ∧
(¦y¦ ≠ ∞--> x + y < z)"

by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_less_minus:
fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ==> x < z - y <-> x + y < z"
by (auto simp: ereal_less_minus_iff)

lemma ereal_le_minus_iff:
fixes x y z :: ereal
shows "x ≤ z - y <-> (y = ∞ --> z ≠ ∞ --> x = -∞) ∧ (¦y¦ ≠ ∞ --> x + y ≤ z)"
by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_le_minus:
fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ==> x ≤ z - y <-> x + y ≤ z"
by (auto simp: ereal_le_minus_iff)

lemma ereal_minus_less_iff:
fixes x y z :: ereal
shows "x - y < z <-> y ≠ -∞ ∧ (y = ∞ --> x ≠ ∞ ∧ z ≠ -∞) ∧ (y ≠ ∞ --> x < z + y)"
by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_minus_less:
fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ==> x - y < z <-> x < z + y"
by (auto simp: ereal_minus_less_iff)

lemma ereal_minus_le_iff:
fixes x y z :: ereal
shows "x - y ≤ z <->
(y = -∞ --> z = ∞) ∧
(y = ∞ --> x = ∞ --> z = ∞) ∧
(¦y¦ ≠ ∞ --> x ≤ z + y)"

by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_minus_le:
fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ==> x - y ≤ z <-> x ≤ z + y"
by (auto simp: ereal_minus_le_iff)

lemma ereal_minus_eq_minus_iff:
fixes a b c :: ereal
shows "a - b = a - c <->
b = c ∨ a = ∞ ∨ (a = -∞ ∧ b ≠ -∞ ∧ c ≠ -∞)"

by (cases rule: ereal3_cases[of a b c]) auto

lemma ereal_add_le_add_iff:
fixes a b c :: ereal
shows "c + a ≤ c + b <->
a ≤ b ∨ c = ∞ ∨ (c = -∞ ∧ a ≠ ∞ ∧ b ≠ ∞)"

by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma ereal_mult_le_mult_iff:
fixes a b c :: ereal
shows "¦c¦ ≠ ∞ ==> c * a ≤ c * b <-> (0 < c --> a ≤ b) ∧ (c < 0 --> b ≤ a)"
by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)

lemma ereal_minus_mono:
fixes A B C D :: ereal assumes "A ≤ B" "D ≤ C"
shows "A - C ≤ B - D"
using assms
by (cases rule: ereal3_cases[case_product ereal_cases, of A B C D]) simp_all

lemma real_of_ereal_minus:
fixes a b :: ereal
shows "real (a - b) = (if ¦a¦ = ∞ ∨ ¦b¦ = ∞ then 0 else real a - real b)"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_diff_positive:
fixes a b :: ereal shows "a ≤ b ==> 0 ≤ b - a"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_between:
fixes x e :: ereal
assumes "¦x¦ ≠ ∞"
and "0 < e"
shows "x - e < x"
and "x < x + e"
using assms
apply (cases x, cases e)
apply auto
using assms
apply (cases x, cases e)
apply auto
done

lemma ereal_minus_eq_PInfty_iff:
fixes x y :: ereal
shows "x - y = ∞ <-> y = -∞ ∨ x = ∞"
by (cases x y rule: ereal2_cases) simp_all


subsubsection {* Division *}

instantiation ereal :: inverse
begin

function inverse_ereal where
"inverse (ereal r) = (if r = 0 then ∞ else ereal (inverse r))"
| "inverse (∞::ereal) = 0"
| "inverse (-∞::ereal) = 0"
by (auto intro: ereal_cases)
termination by (relation "{}") simp

definition "x / y = x * inverse (y :: ereal)"

instance ..

end

lemma real_of_ereal_inverse[simp]:
fixes a :: ereal
shows "real (inverse a) = 1 / real a"
by (cases a) (auto simp: inverse_eq_divide)

lemma ereal_inverse[simp]:
"inverse (0::ereal) = ∞"
"inverse (1::ereal) = 1"
by (simp_all add: one_ereal_def zero_ereal_def)

lemma ereal_divide[simp]:
"ereal r / ereal p = (if p = 0 then ereal r * ∞ else ereal (r / p))"
unfolding divide_ereal_def by (auto simp: divide_real_def)

lemma ereal_divide_same[simp]:
fixes x :: ereal
shows "x / x = (if ¦x¦ = ∞ ∨ x = 0 then 0 else 1)"
by (cases x) (simp_all add: divide_real_def divide_ereal_def one_ereal_def)

lemma ereal_inv_inv[simp]:
fixes x :: ereal
shows "inverse (inverse x) = (if x ≠ -∞ then x else ∞)"
by (cases x) auto

lemma ereal_inverse_minus[simp]:
fixes x :: ereal
shows "inverse (- x) = (if x = 0 then ∞ else -inverse x)"
by (cases x) simp_all

lemma ereal_uminus_divide[simp]:
fixes x y :: ereal
shows "- x / y = - (x / y)"
unfolding divide_ereal_def by simp

lemma ereal_divide_Infty[simp]:
fixes x :: ereal
shows "x / ∞ = 0" "x / -∞ = 0"
unfolding divide_ereal_def by simp_all

lemma ereal_divide_one[simp]: "x / 1 = (x::ereal)"
unfolding divide_ereal_def by simp

lemma ereal_divide_ereal[simp]: "∞ / ereal r = (if 0 ≤ r then ∞ else -∞)"
unfolding divide_ereal_def by simp

lemma zero_le_divide_ereal[simp]:
fixes a :: ereal
assumes "0 ≤ a"
and "0 ≤ b"
shows "0 ≤ a / b"
using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)

lemma ereal_le_divide_pos:
fixes x y z :: ereal
shows "x > 0 ==> x ≠ ∞ ==> y ≤ z / x <-> x * y ≤ z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_divide_le_pos:
fixes x y z :: ereal
shows "x > 0 ==> x ≠ ∞ ==> z / x ≤ y <-> z ≤ x * y"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_le_divide_neg:
fixes x y z :: ereal
shows "x < 0 ==> x ≠ -∞ ==> y ≤ z / x <-> z ≤ x * y"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_divide_le_neg:
fixes x y z :: ereal
shows "x < 0 ==> x ≠ -∞ ==> z / x ≤ y <-> x * y ≤ z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_inverse_antimono_strict:
fixes x y :: ereal
shows "0 ≤ x ==> x < y ==> inverse y < inverse x"
by (cases rule: ereal2_cases[of x y]) auto

lemma ereal_inverse_antimono:
fixes x y :: ereal
shows "0 ≤ x ==> x ≤ y ==> inverse y ≤ inverse x"
by (cases rule: ereal2_cases[of x y]) auto

lemma inverse_inverse_Pinfty_iff[simp]:
fixes x :: ereal
shows "inverse x = ∞ <-> x = 0"
by (cases x) auto

lemma ereal_inverse_eq_0:
fixes x :: ereal
shows "inverse x = 0 <-> x = ∞ ∨ x = -∞"
by (cases x) auto

lemma ereal_0_gt_inverse:
fixes x :: ereal
shows "0 < inverse x <-> x ≠ ∞ ∧ 0 ≤ x"
by (cases x) auto

lemma ereal_mult_less_right:
fixes a b c :: ereal
assumes "b * a < c * a"
and "0 < a"
and "a < ∞"
shows "b < c"
using assms
by (cases rule: ereal3_cases[of a b c])
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)

lemma ereal_power_divide:
fixes x y :: ereal
shows "y ≠ 0 ==> (x / y) ^ n = x^n / y^n"
by (cases rule: ereal2_cases[of x y])
(auto simp: one_ereal_def zero_ereal_def power_divide not_le
power_less_zero_eq zero_le_power_iff)

lemma ereal_le_mult_one_interval:
fixes x y :: ereal
assumes y: "y ≠ -∞"
assumes z: "!!z. 0 < z ==> z < 1 ==> z * x ≤ y"
shows "x ≤ y"
proof (cases x)
case PInf
with z[of "1 / 2"] show "x ≤ y"
by (simp add: one_ereal_def)
next
case (real r)
note r = this
show "x ≤ y"
proof (cases y)
case (real p)
note p = this
have "r ≤ p"
proof (rule field_le_mult_one_interval)
fix z :: real
assume "0 < z" and "z < 1"
with z[of "ereal z"] show "z * r ≤ p"
using p r by (auto simp: zero_le_mult_iff one_ereal_def)
qed
then show "x ≤ y"
using p r by simp
qed (insert y, simp_all)
qed simp

lemma ereal_divide_right_mono[simp]:
fixes x y z :: ereal
assumes "x ≤ y"
and "0 < z"
shows "x / z ≤ y / z"
using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)

lemma ereal_divide_left_mono[simp]:
fixes x y z :: ereal
assumes "y ≤ x"
and "0 < z"
and "0 < x * y"
shows "z / x ≤ z / y"
using assms
by (cases x y z rule: ereal3_cases)
(auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)

lemma ereal_divide_zero_left[simp]:
fixes a :: ereal
shows "0 / a = 0"
by (cases a) (auto simp: zero_ereal_def)

lemma ereal_times_divide_eq_left[simp]:
fixes a b c :: ereal
shows "b / c * a = b * a / c"
by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)


subsection "Complete lattice"

instantiation ereal :: lattice
begin

definition [simp]: "sup x y = (max x y :: ereal)"
definition [simp]: "inf x y = (min x y :: ereal)"
instance by default simp_all

end

instantiation ereal :: complete_lattice
begin

definition "bot = (-∞::ereal)"
definition "top = (∞::ereal)"

definition "Sup S = (SOME x :: ereal. (∀y∈S. y ≤ x) ∧ (∀z. (∀y∈S. y ≤ z) --> x ≤ z))"
definition "Inf S = (SOME x :: ereal. (∀y∈S. x ≤ y) ∧ (∀z. (∀y∈S. z ≤ y) --> z ≤ x))"

lemma ereal_complete_Sup:
fixes S :: "ereal set"
shows "∃x. (∀y∈S. y ≤ x) ∧ (∀z. (∀y∈S. y ≤ z) --> x ≤ z)"
proof (cases "∃x. ∀a∈S. a ≤ ereal x")
case True
then obtain y where y: "!!a. a∈S ==> a ≤ ereal y"
by auto
then have "∞ ∉ S"
by force
show ?thesis
proof (cases "S ≠ {-∞} ∧ S ≠ {}")
case True
with `∞ ∉ S` obtain x where x: "x ∈ S" "¦x¦ ≠ ∞"
by auto
obtain s where s: "∀x∈ereal -` S. x ≤ s" "!!z. (∀x∈ereal -` S. x ≤ z) ==> s ≤ z"
proof (atomize_elim, rule complete_real)
show "∃x. x ∈ ereal -` S"
using x by auto
show "∃z. ∀x∈ereal -` S. x ≤ z"
by (auto dest: y intro!: exI[of _ y])
qed
show ?thesis
proof (safe intro!: exI[of _ "ereal s"])
fix y
assume "y ∈ S"
with s `∞ ∉ S` show "y ≤ ereal s"
by (cases y) auto
next
fix z
assume "∀y∈S. y ≤ z"
with `S ≠ {-∞} ∧ S ≠ {}` show "ereal s ≤ z"
by (cases z) (auto intro!: s)
qed
next
case False
then show ?thesis
by (auto intro!: exI[of _ "-∞"])
qed
next
case False
then show ?thesis
by (fastforce intro!: exI[of _ ∞] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
qed

lemma ereal_complete_uminus_eq:
fixes S :: "ereal set"
shows "(∀y∈uminus`S. y ≤ x) ∧ (∀z. (∀y∈uminus`S. y ≤ z) --> x ≤ z)
<-> (∀y∈S. -x ≤ y) ∧ (∀z. (∀y∈S. z ≤ y) --> z ≤ -x)"

by simp (metis ereal_minus_le_minus ereal_uminus_uminus)

lemma ereal_complete_Inf:
"∃x. (∀y∈S::ereal set. x ≤ y) ∧ (∀z. (∀y∈S. z ≤ y) --> z ≤ x)"
using ereal_complete_Sup[of "uminus ` S"]
unfolding ereal_complete_uminus_eq
by auto

instance
proof
show "Sup {} = (bot::ereal)"
apply (auto simp: bot_ereal_def Sup_ereal_def)
apply (rule some1_equality)
apply (metis ereal_bot ereal_less_eq(2))
apply (metis ereal_less_eq(2))
done
show "Inf {} = (top::ereal)"
apply (auto simp: top_ereal_def Inf_ereal_def)
apply (rule some1_equality)
apply (metis ereal_top ereal_less_eq(1))
apply (metis ereal_less_eq(1))
done
qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)

end

instance ereal :: complete_linorder ..

instance ereal :: linear_continuum
proof
show "∃a b::ereal. a ≠ b"
using ereal_zero_one by blast
qed

lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
by (auto intro!: Sup_eqI
simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
intro!: complete_lattice_class.Inf_lower2)

lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
by (auto intro!: inj_onI)

lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp

lemma ereal_SUPR_uminus:
fixes f :: "'a => ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
using ereal_Sup_uminus_image_eq[of "f`R"]
by (simp add: SUP_def INF_def image_image)

lemma ereal_INFI_uminus:
fixes f :: "'a => ereal"
shows "(INF i : R. - f i) = - (SUP i : R. f i)"
using ereal_SUPR_uminus[of _ "λx. - f x"] by simp

lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set"
shows "uminus ` X = Y <-> X = uminus ` Y"
proof
assume "uminus ` X = Y"
then have "uminus ` uminus ` X = uminus ` Y"
by (simp add: inj_image_eq_iff)
then show "X = uminus ` Y"
by (simp add: image_image)
qed (simp add: image_image)

lemma Inf_ereal_iff:
fixes z :: ereal
shows "(!!x. x ∈ X ==> z ≤ x) ==> (∃x∈X. x < y) <-> Inf X < y"
by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
less_le_not_le linear order_less_le_trans)

lemma Sup_eq_MInfty:
fixes S :: "ereal set"
shows "Sup S = -∞ <-> S = {} ∨ S = {-∞}"
unfolding bot_ereal_def[symmetric] by auto

lemma Inf_eq_PInfty:
fixes S :: "ereal set"
shows "Inf S = ∞ <-> S = {} ∨ S = {∞}"
using Sup_eq_MInfty[of "uminus`S"]
unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp

lemma Inf_eq_MInfty:
fixes S :: "ereal set"
shows "-∞ ∈ S ==> Inf S = -∞"
unfolding bot_ereal_def[symmetric] by auto

lemma Sup_eq_PInfty:
fixes S :: "ereal set"
shows "∞ ∈ S ==> Sup S = ∞"
unfolding top_ereal_def[symmetric] by auto

lemma Sup_ereal_close:
fixes e :: ereal
assumes "0 < e"
and S: "¦Sup S¦ ≠ ∞" "S ≠ {}"
shows "∃x∈S. Sup S - e < x"
using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1])

lemma Inf_ereal_close:
fixes e :: ereal
assumes "¦Inf X¦ ≠ ∞"
and "0 < e"
shows "∃x∈X. x < Inf X + e"
proof (rule Inf_less_iff[THEN iffD1])
show "Inf X < Inf X + e"
using assms by (cases e) auto
qed

lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = ∞"
proof -
{
fix x :: ereal
assume "x ≠ ∞"
then have "∃k::nat. x < ereal (real k)"
proof (cases x)
case MInf
then show ?thesis
by (intro exI[of _ 0]) auto
next
case (real r)
moreover obtain k :: nat where "r < real k"
using ex_less_of_nat by (auto simp: real_eq_of_nat)
ultimately show ?thesis
by auto
qed simp
}
then show ?thesis
using SUP_eq_top_iff[of UNIV "λn::nat. ereal (real n)"]
by (auto simp: top_ereal_def)
qed

lemma Inf_less:
fixes x :: ereal
assumes "(INF i:A. f i) < x"
shows "∃i. i ∈ A ∧ f i ≤ x"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∀i∈A. f i > x"
by auto
then have "(INF i:A. f i) ≥ x"
by (subst INF_greatest) auto
then show False
using assms by auto
qed

lemma SUP_ereal_le_addI:
fixes f :: "'i => ereal"
assumes "!!i. f i + y ≤ z"
and "y ≠ -∞"
shows "SUPR UNIV f + y ≤ z"
proof (cases y)
case (real r)
then have "!!i. f i ≤ z - y"
using assms by (simp add: ereal_le_minus_iff)
then have "SUPR UNIV f ≤ z - y"
by (rule SUP_least)
then show ?thesis
using real by (simp add: ereal_le_minus_iff)
qed (insert assms, auto)

lemma SUPR_ereal_add:
fixes f g :: "nat => ereal"
assumes "incseq f"
and "incseq g"
and pos: "!!i. f i ≠ -∞" "!!i. g i ≠ -∞"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
proof (rule SUP_eqI)
fix y
assume *: "!!i. i ∈ UNIV ==> f i + g i ≤ y"
have f: "SUPR UNIV f ≠ -∞"
using pos
unfolding SUP_def Sup_eq_MInfty
by (auto dest: image_eqD)
{
fix j
{
fix i
have "f i + g j ≤ f i + g (max i j)"
using `incseq g`[THEN incseqD]
by (rule add_left_mono) auto
also have "… ≤ f (max i j) + g (max i j)"
using `incseq f`[THEN incseqD]
by (rule add_right_mono) auto
also have "… ≤ y" using * by auto
finally have "f i + g j ≤ y" .
}
then have "SUPR UNIV f + g j ≤ y"
using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
then have "g j + SUPR UNIV f ≤ y" by (simp add: ac_simps)
}
then have "SUPR UNIV g + SUPR UNIV f ≤ y"
using f by (rule SUP_ereal_le_addI)
then show "SUPR UNIV f + SUPR UNIV g ≤ y"
by (simp add: ac_simps)
qed (auto intro!: add_mono SUP_upper)

lemma SUPR_ereal_add_pos:
fixes f g :: "nat => ereal"
assumes inc: "incseq f" "incseq g"
and pos: "!!i. 0 ≤ f i" "!!i. 0 ≤ g i"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
proof (intro SUPR_ereal_add inc)
fix i
show "f i ≠ -∞" "g i ≠ -∞"
using pos[of i] by auto
qed

lemma SUPR_ereal_setsum:
fixes f g :: "'a => nat => ereal"
assumes "!!n. n ∈ A ==> incseq (f n)"
and pos: "!!n i. n ∈ A ==> 0 ≤ f n i"
shows "(SUP i. ∑n∈A. f n i) = (∑n∈A. SUPR UNIV (f n))"
proof (cases "finite A")
case True
then show ?thesis using assms
by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
next
case False
then show ?thesis by simp
qed

lemma SUPR_ereal_cmult:
fixes f :: "nat => ereal"
assumes "!!i. 0 ≤ f i"
and "0 ≤ c"
shows "(SUP i. c * f i) = c * SUPR UNIV f"
proof (rule SUP_eqI)
fix i
have "f i ≤ SUPR UNIV f"
by (rule SUP_upper) auto
then show "c * f i ≤ c * SUPR UNIV f"
using `0 ≤ c` by (rule ereal_mult_left_mono)
next
fix y
assume *: "!!i. i ∈ UNIV ==> c * f i ≤ y"
show "c * SUPR UNIV f ≤ y"
proof (cases "0 < c ∧ c ≠ ∞")
case True
with * have "SUPR UNIV f ≤ y / c"
by (intro SUP_least) (auto simp: ereal_le_divide_pos)
with True show ?thesis
by (auto simp: ereal_le_divide_pos)
next
case False
{
assume "c = ∞"
have ?thesis
proof (cases "∀i. f i = 0")
case True
then have "range f = {0}"
by auto
with True show "c * SUPR UNIV f ≤ y"
using * by (auto simp: SUP_def min_max.sup_absorb1)
next
case False
then obtain i where "f i ≠ 0"
by auto
with *[of i] `c = ∞` `0 ≤ f i` show ?thesis
by (auto split: split_if_asm)
qed
}
moreover note False
ultimately show ?thesis
using * `0 ≤ c` by auto
qed
qed

lemma SUP_PInfty:
fixes f :: "'a => ereal"
assumes "!!n::nat. ∃i∈A. ereal (real n) ≤ f i"
shows "(SUP i:A. f i) = ∞"
unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
apply simp
proof safe
fix x :: ereal
assume "x ≠ ∞"
show "∃i∈A. x < f i"
proof (cases x)
case PInf
with `x ≠ ∞` show ?thesis
by simp
next
case MInf
with assms[of "0"] show ?thesis
by force
next
case (real r)
with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
by auto
moreover obtain i where "i ∈ A" "ereal (real n) ≤ f i"
using assms ..
ultimately show ?thesis
by (auto intro!: bexI[of _ i])
qed
qed

lemma Sup_countable_SUPR:
assumes "A ≠ {}"
shows "∃f::nat => ereal. range f ⊆ A ∧ Sup A = SUPR UNIV f"
proof (cases "Sup A")
case (real r)
have "∀n::nat. ∃x. x ∈ A ∧ Sup A < x + 1 / ereal (real n)"
proof
fix n :: nat
have "∃x∈A. Sup A - 1 / ereal (real n) < x"
using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
then obtain x where "x ∈ A" "Sup A - 1 / ereal (real n) < x" ..
then show "∃x. x ∈ A ∧ Sup A < x + 1 / ereal (real n)"
by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
qed
from choice[OF this] obtain f :: "nat => ereal"
where f: "∀x. f x ∈ A ∧ Sup A < f x + 1 / ereal (real x)" ..
have "SUPR UNIV f = Sup A"
proof (rule SUP_eqI)
fix i
show "f i ≤ Sup A"
using f by (auto intro!: complete_lattice_class.Sup_upper)
next
fix y
assume bound: "!!i. i ∈ UNIV ==> f i ≤ y"
show "Sup A ≤ y"
proof (rule ereal_le_epsilon, intro allI impI)
fix e :: ereal
assume "0 < e"
show "Sup A ≤ y + e"
proof (cases e)
case (real r)
then have "0 < r"
using `0 < e` by auto
then obtain n :: nat where *: "1 / real n < r" "0 < n"
using ex_inverse_of_nat_less
by (auto simp: real_eq_of_nat inverse_eq_divide)
have "Sup A ≤ f n + 1 / ereal (real n)"
using f[THEN spec, of n]
by auto
also have "1 / ereal (real n) ≤ e"
using real *
by (auto simp: one_ereal_def )
with bound have "f n + 1 / ereal (real n) ≤ y + e"
by (rule add_mono) simp
finally show "Sup A ≤ y + e" .
qed (insert `0 < e`, auto)
qed
qed
with f show ?thesis
by (auto intro!: exI[of _ f])
next
case PInf
from `A ≠ {}` obtain x where "x ∈ A"
by auto
show ?thesis
proof (cases "∞ ∈ A")
case True
then have "∞ ≤ Sup A"
by (intro complete_lattice_class.Sup_upper)
with True show ?thesis
by (auto intro!: exI[of _ "λx. ∞"])
next
case False
have "∃x∈A. 0 ≤ x"
by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least
ereal_infty_less_eq2 linorder_linear)
then obtain x where "x ∈ A" and "0 ≤ x"
by auto
have "∀n::nat. ∃f. f ∈ A ∧ x + ereal (real n) ≤ f"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∃n::nat. Sup A ≤ x + ereal (real n)"
by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
then show False using `x ∈ A` `∞ ∉ A` PInf
by (cases x) auto
qed
from choice[OF this] obtain f :: "nat => ereal"
where f: "∀z. f z ∈ A ∧ x + ereal (real z) ≤ f z" ..
have "SUPR UNIV f = ∞"
proof (rule SUP_PInfty)
fix n :: nat
show "∃i∈UNIV. ereal (real n) ≤ f i"
using f[THEN spec, of n] `0 ≤ x`
by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
qed
then show ?thesis
using f PInf by (auto intro!: exI[of _ f])
qed
next
case MInf
with `A ≠ {}` have "A = {-∞}"
by (auto simp: Sup_eq_MInfty)
then show ?thesis
using MInf by (auto intro!: exI[of _ "λx. -∞"])
qed

lemma SUPR_countable_SUPR:
"A ≠ {} ==> ∃f::nat => ereal. range f ⊆ g`A ∧ SUPR A g = SUPR UNIV f"
using Sup_countable_SUPR[of "g`A"]
by (auto simp: SUP_def)

lemma Sup_ereal_cadd:
fixes A :: "ereal set"
assumes "A ≠ {}"
and "a ≠ -∞"
shows "Sup ((λx. a + x) ` A) = a + Sup A"
proof (rule antisym)
have *: "!!a::ereal. !!A. Sup ((λx. a + x) ` A) ≤ a + Sup A"
by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
then show "Sup ((λx. a + x) ` A) ≤ a + Sup A" .
show "a + Sup A ≤ Sup ((λx. a + x) ` A)"
proof (cases a)
case PInf with `A ≠ {}`
show ?thesis
by (auto simp: image_constant min_max.sup_absorb1)
next
case (real r)
then have **: "op + (- a) ` op + a ` A = A"
by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
from *[of "-a" "(λx. a + x) ` A"] real show ?thesis
unfolding **
by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
qed (insert `a ≠ -∞`, auto)
qed

lemma Sup_ereal_cminus:
fixes A :: "ereal set"
assumes "A ≠ {}"
and "a ≠ -∞"
shows "Sup ((λx. a - x) ` A) = a - Inf A"
using Sup_ereal_cadd[of "uminus ` A" a] assms
by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)

lemma SUPR_ereal_cminus:
fixes f :: "'i => ereal"
fixes A
assumes "A ≠ {}"
and "a ≠ -∞"
shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
using Sup_ereal_cminus[of "f`A" a] assms
unfolding SUP_def INF_def image_image by auto

lemma Inf_ereal_cminus:
fixes A :: "ereal set"
assumes "A ≠ {}"
and "¦a¦ ≠ ∞"
shows "Inf ((λx. a - x) ` A) = a - Sup A"
proof -
{
fix x
have "-a - -x = -(a - x)"
using assms by (cases x) auto
} note * = this
then have "(λx. -a - x)`uminus`A = uminus ` (λx. a - x) ` A"
by (auto simp: image_image)
with * show ?thesis
using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
qed

lemma INFI_ereal_cminus:
fixes a :: ereal
assumes "A ≠ {}"
and "¦a¦ ≠ ∞"
shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
using Inf_ereal_cminus[of "f`A" a] assms
unfolding SUP_def INF_def image_image
by auto

lemma uminus_ereal_add_uminus_uminus:
fixes a b :: ereal
shows "a ≠ ∞ ==> b ≠ ∞ ==> - (- a + - b) = a + b"
by (cases rule: ereal2_cases[of a b]) auto

lemma INFI_ereal_add:
fixes f :: "nat => ereal"
assumes "decseq f" "decseq g"
and fin: "!!i. f i ≠ ∞" "!!i. g i ≠ ∞"
shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
proof -
have INF_less: "(INF i. f i) < ∞" "(INF i. g i) < ∞"
using assms unfolding INF_less_iff by auto
{
fix i
from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
by (rule uminus_ereal_add_uminus_uminus)
}
then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
by simp
also have "… = INFI UNIV f + INFI UNIV g"
unfolding ereal_INFI_uminus
using assms INF_less
by (subst SUPR_ereal_add)
(auto simp: ereal_SUPR_uminus intro!: uminus_ereal_add_uminus_uminus)
finally show ?thesis .
qed


subsection "Relation to @{typ enat}"

definition "ereal_of_enat n = (case n of enat n => ereal (real n) | ∞ => ∞)"

declare [[coercion "ereal_of_enat :: enat => ereal"]]
declare [[coercion "(λn. ereal (real n)) :: nat => ereal"]]

lemma ereal_of_enat_simps[simp]:
"ereal_of_enat (enat n) = ereal n"
"ereal_of_enat ∞ = ∞"
by (simp_all add: ereal_of_enat_def)

lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m ≤ ereal_of_enat n <-> m ≤ n"
by (cases m n rule: enat2_cases) auto

lemma ereal_of_enat_less_iff[simp]: "ereal_of_enat m < ereal_of_enat n <-> m < n"
by (cases m n rule: enat2_cases) auto

lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m ≤ ereal_of_enat n <-> numeral m ≤ n"
by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])

lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n <-> numeral m < n"
by (cases n) (auto simp: real_of_nat_less_iff[symmetric])

lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 ≤ ereal_of_enat n <-> 0 ≤ n"
by (cases n) (auto simp: enat_0[symmetric])

lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n <-> 0 < n"
by (cases n) (auto simp: enat_0[symmetric])

lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
by (auto simp: enat_0[symmetric])

lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = ∞ <-> n = ∞"
by (cases n) auto

lemma ereal_of_enat_add: "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
by (cases m n rule: enat2_cases) auto

lemma ereal_of_enat_sub:
assumes "n ≤ m"
shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
using assms by (cases m n rule: enat2_cases) auto

lemma ereal_of_enat_mult:
"ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
by (cases m n rule: enat2_cases) auto

lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]


subsection "Limits on @{typ ereal}"

subsubsection "Topological space"

instantiation ereal :: linear_continuum_topology
begin

definition "open_ereal" :: "ereal set => bool" where
open_ereal_generated: "open_ereal = generate_topology (range lessThan ∪ range greaterThan)"

instance
by default (simp add: open_ereal_generated)

end

lemma open_PInfty: "open A ==> ∞ ∈ A ==> (∃x. {ereal x<..} ⊆ A)"
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
case (Int A B)
then obtain x z where "∞ ∈ A ==> {ereal x <..} ⊆ A" "∞ ∈ B ==> {ereal z <..} ⊆ B"
by auto
with Int show ?case
by (intro exI[of _ "max x z"]) fastforce
next
case (Basis S)
{
fix x
have "x ≠ ∞ ==> ∃t. x ≤ ereal t"
by (cases x) auto
}
moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+

lemma open_MInfty: "open A ==> -∞ ∈ A ==> (∃x. {..<ereal x} ⊆ A)"
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
case (Int A B)
then obtain x z where "-∞ ∈ A ==> {..< ereal x} ⊆ A" "-∞ ∈ B ==> {..< ereal z} ⊆ B"
by auto
with Int show ?case
by (intro exI[of _ "min x z"]) fastforce
next
case (Basis S)
{
fix x
have "x ≠ - ∞ ==> ∃t. ereal t ≤ x"
by (cases x) auto
}
moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+

lemma open_ereal_vimage: "open S ==> open (ereal -` S)"
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
case (Int A B)
then show ?case
by auto
next
case (Basis S)
{
fix x have
"ereal -` {..<x} = (case x of PInfty => UNIV | MInfty => {} | ereal r => {..<r})"
"ereal -` {x<..} = (case x of PInfty => {} | MInfty => UNIV | ereal r => {r<..})"
by (induct x) auto
}
moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+

lemma open_ereal: "open S ==> open (ereal ` S)"
unfolding open_generated_order[where 'a=real]
proof (induct rule: generate_topology.induct)
case (Basis S)
moreover {
fix x
have "ereal ` {..< x} = { -∞ <..< ereal x }"
apply auto
apply (case_tac xa)
apply auto
done
}
moreover {
fix x
have "ereal ` {x <..} = { ereal x <..< ∞ }"
apply auto
apply (case_tac xa)
apply auto
done
}
ultimately show ?case
by auto
qed (auto simp add: image_Union image_Int)

lemma open_ereal_def:
"open A <-> open (ereal -` A) ∧ (∞ ∈ A --> (∃x. {ereal x <..} ⊆ A)) ∧ (-∞ ∈ A --> (∃x. {..<ereal x} ⊆ A))"
(is "open A <-> ?rhs")
proof
assume "open A"
then show ?rhs
using open_PInfty open_MInfty open_ereal_vimage by auto
next
assume "?rhs"
then obtain x y where A: "open (ereal -` A)" "∞ ∈ A ==> {ereal x<..} ⊆ A" "-∞ ∈ A ==> {..< ereal y} ⊆ A"
by auto
have *: "A = ereal ` (ereal -` A) ∪ (if ∞ ∈ A then {ereal x<..} else {}) ∪ (if -∞ ∈ A then {..< ereal y} else {})"
using A(2,3) by auto
from open_ereal[OF A(1)] show "open A"
by (subst *) (auto simp: open_Un)
qed

lemma open_PInfty2:
assumes "open A"
and "∞ ∈ A"
obtains x where "{ereal x<..} ⊆ A"
using open_PInfty[OF assms] by auto

lemma open_MInfty2:
assumes "open A"
and "-∞ ∈ A"
obtains x where "{..<ereal x} ⊆ A"
using open_MInfty[OF assms] by auto

lemma ereal_openE:
assumes "open A"
obtains x y where "open (ereal -` A)"
and "∞ ∈ A ==> {ereal x<..} ⊆ A"
and "-∞ ∈ A ==> {..<ereal y} ⊆ A"
using assms open_ereal_def by auto

lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]

lemma ereal_open_cont_interval:
fixes S :: "ereal set"
assumes "open S"
and "x ∈ S"
and "¦x¦ ≠ ∞"
obtains e where "e > 0" and "{x-e <..< x+e} ⊆ S"
proof -
from `open S`
have "open (ereal -` S)"
by (rule ereal_openE)
then obtain e where "e > 0" and e: "!!y. dist y (real x) < e ==> ereal y ∈ S"
using assms unfolding open_dist by force
show thesis
proof (intro that subsetI)
show "0 < ereal e"
using `0 < e` by auto
fix y
assume "y ∈ {x - ereal e<..<x + ereal e}"
with assms obtain t where "y = ereal t" "dist t (real x) < e"
by (cases y) (auto simp: dist_real_def)
then show "y ∈ S"
using e[of t] by auto
qed
qed

lemma ereal_open_cont_interval2:
fixes S :: "ereal set"
assumes "open S"
and "x ∈ S"
and x: "¦x¦ ≠ ∞"
obtains a b where "a < x" and "x < b" and "{a <..< b} ⊆ S"
proof -
obtain e where "0 < e" "{x - e<..<x + e} ⊆ S"
using assms by (rule ereal_open_cont_interval)
with that[of "x - e" "x + e"] ereal_between[OF x, of e]
show thesis
by auto
qed


subsubsection {* Convergent sequences *}

lemma lim_ereal[simp]: "((λn. ereal (f n)) ---> ereal x) net <-> (f ---> x) net"
(is "?l = ?r")
proof (intro iffI topological_tendstoI)
fix S
assume "?l" and "open S" and "x ∈ S"
then show "eventually (λx. f x ∈ S) net"
using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
by (simp add: inj_image_mem_iff)
next
fix S
assume "?r" and "open S" and "ereal x ∈ S"
show "eventually (λx. ereal (f x) ∈ S) net"
using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
using `ereal x ∈ S`
by auto
qed

lemma lim_real_of_ereal[simp]:
assumes lim: "(f ---> ereal x) net"
shows "((λx. real (f x)) ---> x) net"
proof (intro topological_tendstoI)
fix S
assume "open S" and "x ∈ S"
then have S: "open S" "ereal x ∈ ereal ` S"
by (simp_all add: inj_image_mem_iff)
have "∀x. f x ∈ ereal ` S --> real (f x) ∈ S"
by auto
from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
show "eventually (λx. real (f x) ∈ S) net"
by (rule eventually_mono)
qed

lemma tendsto_PInfty: "(f ---> ∞) F <-> (∀r. eventually (λx. ereal r < f x) F)"
proof -
{
fix l :: ereal
assume "∀r. eventually (λx. ereal r < f x) F"
from this[THEN spec, of "real l"] have "l ≠ ∞ ==> eventually (λx. l < f x) F"
by (cases l) (auto elim: eventually_elim1)
}
then show ?thesis
by (auto simp: order_tendsto_iff)
qed

lemma tendsto_MInfty: "(f ---> -∞) F <-> (∀r. eventually (λx. f x < ereal r) F)"
unfolding tendsto_def
proof safe
fix S :: "ereal set"
assume "open S" "-∞ ∈ S"
from open_MInfty[OF this] obtain B where "{..<ereal B} ⊆ S" ..
moreover
assume "∀r::real. eventually (λz. f z < r) F"
then have "eventually (λz. f z ∈ {..< B}) F"
by auto
ultimately show "eventually (λz. f z ∈ S) F"
by (auto elim!: eventually_elim1)
next
fix x
assume "∀S. open S --> -∞ ∈ S --> eventually (λx. f x ∈ S) F"
from this[rule_format, of "{..< ereal x}"] show "eventually (λy. f y < ereal x) F"
by auto
qed

lemma Lim_PInfty: "f ----> ∞ <-> (∀B. ∃N. ∀n≥N. f n ≥ ereal B)"
unfolding tendsto_PInfty eventually_sequentially
proof safe
fix r
assume "∀r. ∃N. ∀n≥N. ereal r ≤ f n"
then obtain N where "∀n≥N. ereal (r + 1) ≤ f n"
by blast
moreover have "ereal r < ereal (r + 1)"
by auto
ultimately show "∃N. ∀n≥N. ereal r < f n"
by (blast intro: less_le_trans)
qed (blast intro: less_imp_le)

lemma Lim_MInfty: "f ----> -∞ <-> (∀B. ∃N. ∀n≥N. ereal B ≥ f n)"
unfolding tendsto_MInfty eventually_sequentially
proof safe
fix r
assume "∀r. ∃N. ∀n≥N. f n ≤ ereal r"
then obtain N where "∀n≥N. f n ≤ ereal (r - 1)"
by blast
moreover have "ereal (r - 1) < ereal r"
by auto
ultimately show "∃N. ∀n≥N. f n < ereal r"
by (blast intro: le_less_trans)
qed (blast intro: less_imp_le)

lemma Lim_bounded_PInfty: "f ----> l ==> (!!n. f n ≤ ereal B) ==> l ≠ ∞"
using LIMSEQ_le_const2[of f l "ereal B"] by auto

lemma Lim_bounded_MInfty: "f ----> l ==> (!!n. ereal B ≤ f n) ==> l ≠ -∞"
using LIMSEQ_le_const[of f l "ereal B"] by auto

lemma tendsto_explicit:
"f ----> f0 <-> (∀S. open S --> f0 ∈ S --> (∃N. ∀n≥N. f n ∈ S))"
unfolding tendsto_def eventually_sequentially by auto

lemma Lim_bounded_PInfty2: "f ----> l ==> ∀n≥N. f n ≤ ereal B ==> l ≠ ∞"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce

lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) ==> ∀n≥M. f n ≤ C ==> l ≤ C"
by (intro LIMSEQ_le_const2) auto

lemma Lim_bounded2_ereal:
assumes lim:"f ----> (l :: 'a::linorder_topology)"
and ge: "∀n≥N. f n ≥ C"
shows "l ≥ C"
using ge
by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
(auto simp: eventually_sequentially)

lemma real_of_ereal_mult[simp]:
fixes a b :: ereal
shows "real (a * b) = real a * real b"
by (cases rule: ereal2_cases[of a b]) auto

lemma real_of_ereal_eq_0:
fixes x :: ereal
shows "real x = 0 <-> x = ∞ ∨ x = -∞ ∨ x = 0"
by (cases x) auto

lemma tendsto_ereal_realD:
fixes f :: "'a => ereal"
assumes "x ≠ 0"
and tendsto: "((λx. ereal (real (f x))) ---> x) net"
shows "(f ---> x) net"
proof (intro topological_tendstoI)
fix S
assume S: "open S" "x ∈ S"
with `x ≠ 0` have "open (S - {0})" "x ∈ S - {0}"
by auto
from tendsto[THEN topological_tendstoD, OF this]
show "eventually (λx. f x ∈ S) net"
by (rule eventually_rev_mp) (auto simp: ereal_real)
qed

lemma tendsto_ereal_realI:
fixes f :: "'a => ereal"
assumes x: "¦x¦ ≠ ∞" and tendsto: "(f ---> x) net"
shows "((λx. ereal (real (f x))) ---> x) net"
proof (intro topological_tendstoI)
fix S
assume "open S" and "x ∈ S"
with x have "open (S - {∞, -∞})" "x ∈ S - {∞, -∞}"
by auto
from tendsto[THEN topological_tendstoD, OF this]
show "eventually (λx. ereal (real (f x)) ∈ S) net"
by (elim eventually_elim1) (auto simp: ereal_real)
qed

lemma ereal_mult_cancel_left:
fixes a b c :: ereal
shows "a * b = a * c <-> (¦a¦ = ∞ ∧ 0 < b * c) ∨ a = 0 ∨ b = c"
by (cases rule: ereal3_cases[of a b c]) (simp_all add: zero_less_mult_iff)

lemma ereal_inj_affinity:
fixes m t :: ereal
assumes "¦m¦ ≠ ∞"
and "m ≠ 0"
and "¦t¦ ≠ ∞"
shows "inj_on (λx. m * x + t) A"
using assms
by (cases rule: ereal2_cases[of m t])
(auto intro!: inj_onI simp: ereal_add_cancel_right ereal_mult_cancel_left)

lemma ereal_PInfty_eq_plus[simp]:
fixes a b :: ereal
shows "∞ = a + b <-> a = ∞ ∨ b = ∞"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_MInfty_eq_plus[simp]:
fixes a b :: ereal
shows "-∞ = a + b <-> (a = -∞ ∧ b ≠ ∞) ∨ (b = -∞ ∧ a ≠ ∞)"
by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_less_divide_pos:
fixes x y :: ereal
shows "x > 0 ==> x ≠ ∞ ==> y < z / x <-> x * y < z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_divide_less_pos:
fixes x y z :: ereal
shows "x > 0 ==> x ≠ ∞ ==> y / x < z <-> y < x * z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_divide_eq:
fixes a b c :: ereal
shows "b ≠ 0 ==> ¦b¦ ≠ ∞ ==> a / b = c <-> a = b * c"
by (cases rule: ereal3_cases[of a b c])
(simp_all add: field_simps)

lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) ≠ -∞"
by (cases a) auto

lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
by (cases x) auto

lemma ereal_real':
assumes "¦x¦ ≠ ∞"
shows "ereal (real x) = x"
using assms by auto

lemma real_ereal_id: "real o ereal = id"
proof -
{
fix x
have "(real o ereal) x = id x"
by auto
}
then show ?thesis
using ext by blast
qed

lemma open_image_ereal: "open(UNIV-{ ∞ , (-∞ :: ereal)})"
by (metis range_ereal open_ereal open_UNIV)

lemma ereal_le_distrib:
fixes a b c :: ereal
shows "c * (a + b) ≤ c * a + c * b"
by (cases rule: ereal3_cases[of a b c])
(auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)

lemma ereal_pos_distrib:
fixes a b c :: ereal
assumes "0 ≤ c"
and "c ≠ ∞"
shows "c * (a + b) = c * a + c * b"
using assms
by (cases rule: ereal3_cases[of a b c])
(auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)

lemma ereal_pos_le_distrib:
fixes a b c :: ereal
assumes "c ≥ 0"
shows "c * (a + b) ≤ c * a + c * b"
using assms
by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)

lemma ereal_max_mono: "(a::ereal) ≤ b ==> c ≤ d ==> max a c ≤ max b d"
by (metis sup_ereal_def sup_mono)

lemma ereal_max_least: "(a::ereal) ≤ x ==> c ≤ x ==> max a c ≤ x"
by (metis sup_ereal_def sup_least)

lemma ereal_LimI_finite:
fixes x :: ereal
assumes "¦x¦ ≠ ∞"
and "!!r. 0 < r ==> ∃N. ∀n≥N. u n < x + r ∧ x < u n + r"
shows "u ----> x"
proof (rule topological_tendstoI, unfold eventually_sequentially)
obtain rx where rx: "x = ereal rx"
using assms by (cases x) auto
fix S
assume "open S" and "x ∈ S"
then have "open (ereal -` S)"
unfolding open_ereal_def by auto
with `x ∈ S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y ∈ S"
unfolding open_real_def rx by auto
then obtain n where
upper: "!!N. n ≤ N ==> u N < x + ereal r" and
lower: "!!N. n ≤ N ==> x < u N + ereal r"
using assms(2)[of "ereal r"] by auto
show "∃N. ∀n≥N. u n ∈ S"
proof (safe intro!: exI[of _ n])
fix N
assume "n ≤ N"
from upper[OF this] lower[OF this] assms `0 < r`
have "u N ∉ {∞,(-∞)}"
by auto
then obtain ra where ra_def: "(u N) = ereal ra"
by (cases "u N") auto
then have "rx < ra + r" and "ra < rx + r"
using rx assms `0 < r` lower[OF `n ≤ N`] upper[OF `n ≤ N`]
by auto
then have "dist (real (u N)) rx < r"
using rx ra_def
by (auto simp: dist_real_def abs_diff_less_iff field_simps)
from dist[OF this] show "u N ∈ S"
using `u N ∉ {∞, -∞}`
by (auto simp: ereal_real split: split_if_asm)
qed
qed

lemma tendsto_obtains_N:
assumes "f ----> f0"
assumes "open S"
and "f0 ∈ S"
obtains N where "∀n≥N. f n ∈ S"
using assms using tendsto_def
using tendsto_explicit[of f f0] assms by auto

lemma ereal_LimI_finite_iff:
fixes x :: ereal
assumes "¦x¦ ≠ ∞"
shows "u ----> x <-> (∀r. 0 < r --> (∃N. ∀n≥N. u n < x + r ∧ x < u n + r))"
(is "?lhs <-> ?rhs")
proof
assume lim: "u ----> x"
{
fix r :: ereal
assume "r > 0"
then obtain N where "∀n≥N. u n ∈ {x - r <..< x + r}"
apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
using lim ereal_between[of x r] assms `r > 0`
apply auto
done
then have "∃N. ∀n≥N. u n < x + r ∧ x < u n + r"
using ereal_minus_less[of r x]
by (cases r) auto
}
then show ?rhs
by auto
next
assume ?rhs
then show "u ----> x"
using ereal_LimI_finite[of x] assms by auto
qed

lemma ereal_Limsup_uminus:
fixes f :: "'a => ereal"
shows "Limsup net (λx. - (f x)) = - Liminf net f"
unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..

lemma liminf_bounded_iff:
fixes x :: "nat => ereal"
shows "C ≤ liminf x <-> (∀B<C. ∃N. ∀n≥N. B < x n)"
(is "?lhs <-> ?rhs")
unfolding le_Liminf_iff eventually_sequentially ..

lemma
fixes X :: "nat => ereal"
shows ereal_incseq_uminus[simp]: "incseq (λi. - X i) = decseq X"
and ereal_decseq_uminus[simp]: "decseq (λi. - X i) = incseq X"
unfolding incseq_def decseq_def by auto


subsubsection {* Tests for code generator *}

(* A small list of simple arithmetic expressions *)

value [code] "- ∞ :: ereal"
value [code] "¦-∞¦ :: ereal"
value [code] "4 + 5 / 4 - ereal 2 :: ereal"
value [code] "ereal 3 < ∞"
value [code] "real (∞::ereal) = 0"

end