Theory Extended_Real

```(*  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
Author:     Manuel Eberl, TU München
*)

section ‹Extended real number line›

theory Extended_Real
imports Complex_Main Extended_Nat Liminf_Limsup
begin

text ‹
This should be part of \<^theory>‹HOL-Library.Extended_Nat› or \<^theory>‹HOL-Library.Order_Continuity›, but then the AFP-entry ‹Jinja_Thread› fails, as it does overload
certain named from \<^theory>‹Complex_Main›.
›

lemma incseq_sumI2:
fixes f :: "'i ⇒ nat ⇒ 'a::ordered_comm_monoid_add"
shows "(⋀n. n ∈ A ⟹ mono (f n)) ⟹ mono (λi. ∑n∈A. f n i)"
unfolding incseq_def by (auto intro: sum_mono)

lemma incseq_sumI:
fixes f :: "nat ⇒ 'a::ordered_comm_monoid_add"
assumes "⋀i. 0 ≤ f i"
shows "incseq (λi. sum f {..< i})"
proof (intro incseq_SucI)
fix n
have "sum f {..< n} + 0 ≤ sum f {..<n} + f n"
using assms by (rule add_left_mono)
then show "sum f {..< n} ≤ sum f {..< Suc n}"
by auto
qed

lemma continuous_at_left_imp_sup_continuous:
fixes f :: "'a::{complete_linorder, linorder_topology} ⇒ 'b::{complete_linorder, linorder_topology}"
assumes "mono f" "⋀x. continuous (at_left x) f"
shows "sup_continuous f"
unfolding sup_continuous_def
proof safe
fix M :: "nat ⇒ 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
using continuous_at_Sup_mono [OF assms, of "range M"] by (simp add: image_comp)
qed

lemma sup_continuous_at_left:
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} ⇒
'b::{complete_linorder, linorder_topology}"
assumes f: "sup_continuous f"
shows "continuous (at_left x) f"
proof cases
assume "x = bot" then show ?thesis
by (simp add: trivial_limit_at_left_bot)
next
assume x: "x ≠ bot"
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_left_sequentially[of bot])
fix S :: "nat ⇒ 'a" assume S: "incseq S" and S_x: "S ⇢ x"
from S_x have x_eq: "x = (SUP i. S i)"
by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S)
show "(λn. f (S n)) ⇢ f x"
unfolding x_eq sup_continuousD[OF f S]
using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def)
qed (insert x, auto simp: bot_less)
qed

lemma sup_continuous_iff_at_left:
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} ⇒
'b::{complete_linorder, linorder_topology}"
shows "sup_continuous f ⟷ (∀x. continuous (at_left x) f) ∧ mono f"
using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f]
sup_continuous_mono[of f] by auto

lemma continuous_at_right_imp_inf_continuous:
fixes f :: "'a::{complete_linorder, linorder_topology} ⇒ 'b::{complete_linorder, linorder_topology}"
assumes "mono f" "⋀x. continuous (at_right x) f"
shows "inf_continuous f"
unfolding inf_continuous_def
proof safe
fix M :: "nat ⇒ 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
using continuous_at_Inf_mono [OF assms, of "range M"] by (simp add: image_comp)
qed

lemma inf_continuous_at_right:
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} ⇒
'b::{complete_linorder, linorder_topology}"
assumes f: "inf_continuous f"
shows "continuous (at_right x) f"
proof cases
assume "x = top" then show ?thesis
by (simp add: trivial_limit_at_right_top)
next
assume x: "x ≠ top"
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_right_sequentially[of _ top])
fix S :: "nat ⇒ 'a" assume S: "decseq S" and S_x: "S ⇢ x"
from S_x have x_eq: "x = (INF i. S i)"
by (rule LIMSEQ_unique) (intro LIMSEQ_INF S)
show "(λn. f (S n)) ⇢ f x"
unfolding x_eq inf_continuousD[OF f S]
using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def)
qed (insert x, auto simp: less_top)
qed

lemma inf_continuous_iff_at_right:
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} ⇒
'b::{complete_linorder, linorder_topology}"
shows "inf_continuous f ⟷ (∀x. continuous (at_right x) f) ∧ mono f"
using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f]
inf_continuous_mono[of f] by auto

instantiation enat :: linorder_topology
begin

definition open_enat :: "enat set ⇒ bool" where
"open_enat = generate_topology (range lessThan ∪ range greaterThan)"

instance
proof qed (rule open_enat_def)

end

lemma open_enat: "open {enat n}"
proof (cases n)
case 0
then have "{enat n} = {..< eSuc 0}"
by (auto simp: enat_0)
then show ?thesis
by simp
next
case (Suc n')
then have "{enat n} = {enat n' <..< enat (Suc n)}"
using enat_iless by (fastforce simp: set_eq_iff)
then show ?thesis
by simp
qed

lemma open_enat_iff:
fixes A :: "enat set"
shows "open A ⟷ (∞ ∈ A ⟶ (∃n::nat. {n <..} ⊆ A))"
proof safe
assume "∞ ∉ A"
then have "A = (⋃n∈{n. enat n ∈ A}. {enat n})"
by (simp add: set_eq_iff) (metis not_enat_eq)
moreover have "open …"
by (auto intro: open_enat)
ultimately show "open A"
by simp
next
fix n assume "{enat n <..} ⊆ A"
then have "A = (⋃n∈{n. enat n ∈ A}. {enat n}) ∪ {enat n <..}"
using enat_ile leI by (simp add: set_eq_iff) blast
moreover have "open …"
by (intro open_Un open_UN ballI open_enat open_greaterThan)
ultimately show "open A"
by simp
next
assume "open A" "∞ ∈ A"
then have "generate_topology (range lessThan ∪ range greaterThan) A" "∞ ∈ A"
unfolding open_enat_def by auto
then show "∃n::nat. {n <..} ⊆ A"
proof induction
case (Int A B)
then obtain n m where "{enat n<..} ⊆ A" "{enat m<..} ⊆ B"
by auto
then have "{enat (max n m) <..} ⊆ A ∩ B"
by (auto simp add: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
then show ?case
by auto
next
case (UN K)
then obtain k where "k ∈ K" "∞ ∈ k"
by auto
with UN.IH[OF this] show ?case
by auto
qed auto
qed

lemma nhds_enat: "nhds x = (if x = ∞ then INF i. principal {enat i..} else principal {x})"
proof auto
show "nhds ∞ = (INF i. principal {enat i..})"
proof (rule antisym)
show "nhds ∞ ≤ (INF i. principal {enat i..})"
unfolding nhds_def
using Ioi_le_Ico by (intro INF_greatest INF_lower) (auto simp add: open_enat_iff)
show "(INF i. principal {enat i..}) ≤ nhds ∞"
unfolding nhds_def
by (intro INF_greatest) (force intro: INF_lower2[of "Suc _"] simp add: open_enat_iff Suc_ile_eq)
qed
show "nhds (enat i) = principal {enat i}" for i
by (simp add: nhds_discrete_open open_enat)
qed

instance enat :: topological_comm_monoid_add
proof
have [simp]: "enat i ≤ aa ⟹ enat i ≤ aa + ba" for aa ba i
by (rule order_trans[OF _ add_mono[of aa aa 0 ba]]) auto
then have [simp]: "enat i ≤ ba ⟹ enat i ≤ aa + ba" for aa ba i
fix a b :: enat show "((λx. fst x + snd x) ⤏ a + b) (nhds a ×⇩F nhds b)"
apply (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2
filterlim_principal principal_prod_principal eventually_principal)
subgoal for i
by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
subgoal for j i
by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
subgoal for j i
by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
done
qed

text ‹
For more lemmas about the extended real numbers see
🗏‹~~/src/HOL/Analysis/Extended_Real_Limits.thy›.
›

subsection ‹Definition and basic properties›

datatype ereal = ereal real | PInfty | MInfty

lemma ereal_cong: "x = y ⟹ ereal x = ereal y" by simp

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[cases type: ereal]:
obtains (real) r where "x = ereal r"
| (PInf) "x = ∞"
| (MInf) "x = -∞"
by (cases x) auto

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

lemma ereal_all_split: "⋀P. (∀x::ereal. P x) ⟷ P ∞ ∧ (∀x. P (ereal x)) ∧ P (-∞)"
by (metis ereal_cases)

lemma ereal_ex_split: "⋀P. (∃x::ereal. P x) ⟷ P ∞ ∨ (∃x. P (ereal x)) ∨ P (-∞)"
by (metis 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 real_of_ereal :: "ereal ⇒ real" where
"real_of_ereal (ereal r) = r"
| "real_of_ereal ∞ = 0"
| "real_of_ereal (-∞) = 0"
by (auto intro: ereal_cases)
termination by standard (rule wf_empty)

lemma real_of_ereal[simp]:
"real_of_ereal (- x :: ereal) = - (real_of_ereal x)"
by (cases x) simp_all

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

instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
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 goal_cases
case prems: (1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
termination by standard (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

lemma ereal_eq_1[simp]:
"ereal r = 1 ⟷ r = 1"
"1 = ereal r ⟷ r = 1"
unfolding one_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
show "0 ≠ (1::ereal)"
by (simp add: one_ereal_def zero_ereal_def)
qed

end

lemma ereal_0_plus [simp]: "ereal 0 + x = x"
and plus_ereal_0 [simp]: "x + ereal 0 = x"
by(simp_all flip: zero_ereal_def)

instance ereal :: numeral ..

lemma real_of_ereal_0[simp]: "real_of_ereal (0::ereal) = 0"
unfolding 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

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

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_of_ereal x) = (if ¦x¦ = ∞ then 0 else x)"
by (cases x) simp_all

fixes a b :: ereal
shows "real_of_ereal (a + b) =
(if (¦a¦ = ∞) ∧ (¦b¦ = ∞) ∨ (¦a¦ ≠ ∞) ∧ (¦b¦ ≠ ∞) then real_of_ereal a + real_of_ereal 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 goal_cases
case prems: (1 P x)
then obtain a b where "x = (a,b)" by (cases x) auto
with prems 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)"
"ereal r < 1 ⟷ (r < 1)"
"1 < ereal r ⟷ (1 < r)"
"0 < (∞::ereal)"
"-(∞::ereal) < 0"
by (simp_all add: zero_ereal_def one_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"
"ereal r ≤ 1 ⟷ r ≤ 1"
"1 ≤ ereal r ⟷ 1 ≤ r"
by (auto simp add: less_eq_ereal_def zero_ereal_def one_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 standard (blast dest: ereal_dense2)

instance ereal :: ordered_comm_monoid_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 ereal_one_not_less_zero_ereal[simp]: "¬ 1 < (0::ereal)"
by (simp add: zero_ereal_def)

lemma real_of_ereal_positive_mono:
fixes x y :: ereal
shows "0 ≤ x ⟹ x ≤ y ⟹ y ≠ ∞ ⟹ real_of_ereal x ≤ real_of_ereal 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

fixes a b c d :: ereal
assumes "a < b" and "c < d"
shows "a + c < b + d"
using assms
by (cases a; force simp add: elim: less_ereal.elims)

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_of_ereal y ⟷ (¦y¦ ≠ ∞ ⟶ ereal x ≤ y) ∧ (¦y¦ = ∞ ⟶ x ≤ 0)"
by (cases y) auto

lemma real_le_ereal_iff:
"real_of_ereal y ≤ x ⟷ (¦y¦ ≠ ∞ ⟶ y ≤ ereal x) ∧ (¦y¦ = ∞ ⟶ 0 ≤ x)"
by (cases y) auto

lemma ereal_less_real_iff:
"x < real_of_ereal y ⟷ (¦y¦ ≠ ∞ ⟶ ereal x < y) ∧ (¦y¦ = ∞ ⟶ x < 0)"
by (cases y) auto

lemma real_less_ereal_iff:
"real_of_ereal y < x ⟷ (¦y¦ ≠ ∞ ⟶ y < ereal x) ∧ (¦y¦ = ∞ ⟶ 0 < x)"
by (cases y) auto

text ‹
To help with inferences like \<^prop>‹a < ereal x ⟹ x < y ⟹ a < ereal y›,
where x and y are real.
›

lemma le_ereal_le: "a ≤ ereal x ⟹ x ≤ y ⟹ a ≤ ereal y"
using ereal_less_eq(3) order.trans by blast

lemma le_ereal_less: "a ≤ ereal x ⟹ x < y ⟹ a < ereal y"
by (simp add: le_less_trans)

lemma less_ereal_le: "a < ereal x ⟹ x ≤ y ⟹ a < ereal y"
using ereal_less_ereal_Ex by auto

lemma ereal_le_le: "ereal y ≤ a ⟹ x ≤ y ⟹ ereal x ≤ a"
by (simp add: order_subst2)

lemma ereal_le_less: "ereal y ≤ a ⟹ x < y ⟹ ereal x < a"
by (simp add: dual_order.strict_trans1)

lemma ereal_less_le: "ereal y < a ⟹ x ≤ y ⟹ ereal x < a"
using ereal_less_eq(3) le_less_trans by blast

lemma real_of_ereal_pos:
fixes x :: ereal
shows "0 ≤ x ⟹ 0 ≤ real_of_ereal 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 ereal_abs_leI:
fixes x y :: ereal
shows "⟦ x ≤ y; -x ≤ y ⟧ ⟹ ¦x¦ ≤ y"
by(cases x y rule: ereal2_cases)(simp_all)

fixes a b::ereal
shows "abs(a+b) ≤ abs a + abs b"
by (cases rule: ereal2_cases[of a b]) (auto)

lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) ≤ 0 ⟷ x ≤ 0 ∨ x = ∞"
by (cases x) auto

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

lemma zero_less_real_of_ereal:
fixes x :: ereal
shows "0 < real_of_ereal 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

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

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

fixes a b :: ereal
shows "0 ≤ a ⟹ 0 ≤ b ⟹ a + b = 0 ⟷ a = 0 ∧ b = 0"
by (cases a b rule: ereal2_cases) 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_less_uminus_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 ereal_incseq_uminus[simp]: "incseq (λx. - f x) ⟷ decseq f"
and ereal_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 sum_ereal[simp]: "(∑x∈A. ereal (f x)) = ereal (∑x∈A. f x)"
proof (cases "finite A")
case True
then show ?thesis by induct auto
next
case False
then show ?thesis by simp
qed

lemma sum_list_ereal [simp]: "sum_list (map (λx. ereal (f x)) xs) = ereal (sum_list (map f xs))"
by (induction xs) simp_all

lemma sum_Pinfty:
fixes f :: "'a ⇒ ereal"
shows "(∑x∈P. f x) = ∞ ⟷ finite P ∧ (∃i∈P. f i = ∞)"
proof safe
assume *: "sum f P = ∞"
show "finite P"
proof (rule ccontr)
assume "¬ finite P"
with * show False
by auto
qed
show "∃i∈P. f i = ∞"
proof (rule ccontr)
assume "¬ ?thesis"
then have "⋀i. i ∈ P ⟹ f i ≠ ∞"
by auto
with ‹finite P› have "sum f P ≠ ∞"
by induct auto
with * show False
by auto
qed
next
fix i
assume "finite P" and "i ∈ P" and "f i = ∞"
then show "sum f P = ∞"
proof induct
case (insert x A)
show ?case using insert by (cases "x = i") auto
qed simp
qed

lemma sum_Inf:
fixes f :: "'a ⇒ ereal"
shows "¦sum f A¦ = ∞ ⟷ finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
proof
assume *: "¦sum f A¦ = ∞"
have "finite A"
by (rule ccontr) (insert *, auto)
moreover have "∃i∈A. ¦f i¦ = ∞"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∀i∈A. ∃r. f i = ereal r"
by auto
from bchoice[OF this] obtain r where "∀x∈A. f x = ereal (r x)" ..
with * show False
by auto
qed
ultimately show "finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
by auto
next
assume "finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
then obtain i where "finite A" "i ∈ A" and "¦f i¦ = ∞"
by auto
then show "¦sum f A¦ = ∞"
proof induct
case (insert j A)
then show ?case
by (cases rule: ereal3_cases[of "f i" "f j" "sum f A"]) auto
qed simp
qed

lemma sum_real_of_ereal:
fixes f :: "'i ⇒ ereal"
assumes "⋀x. x ∈ S ⟹ ¦f x¦ ≠ ∞"
shows "(∑x∈S. real_of_ereal (f x)) = real_of_ereal (sum f S)"
proof -
have "∀x∈S. ∃r. f x = ereal r"
proof
fix x
assume "x ∈ S"
from assms[OF this] show "∃r. f x = ereal r"
by (cases "f x") auto
qed
from bchoice[OF this] obtain r where "∀x∈S. f x = ereal (r x)" ..
then show ?thesis
by simp
qed

lemma sum_ereal_0:
fixes f :: "'a ⇒ ereal"
assumes "finite A"
and "⋀i. i ∈ A ⟹ 0 ≤ f i"
shows "(∑x∈A. f x) = 0 ⟷ (∀i∈A. f i = 0)"
proof
assume "sum f A = 0" with assms show "∀i∈A. f i = 0"
proof (induction A)
case (insert a A)
then have "f a = 0 ∧ (∑a∈A. f a) = 0"
with insert show ?case
by simp
qed simp
qed auto

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 standard (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 goal_cases
case prems: (1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
with prems 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 [simp]:
shows ereal_1_times: "ereal 1 * x = x"
and times_ereal_1: "x * ereal 1 = x"
by(simp_all flip: one_ereal_def)

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

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

lemma real_of_ereal_le_1:
fixes a :: ereal
shows "a ≤ 1 ⟹ real_of_ereal 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_times[simp]:
"1 ≠ (∞::ereal)" "(∞::ereal) ≠ 1"
"1 ≠ -(∞::ereal)" "-(∞::ereal) ≠ 1"
by (auto simp: 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_abs_mult: "¦x * y :: ereal¦ = ¦x¦ * ¦y¦"
by (cases x y rule: ereal2_cases) (auto simp: abs_mult)

lemma ereal_0_less_1[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
assumes "a ≤ b" "0 ≤ c"
shows "a * c ≤ b * c"
proof (cases "c = 0")
case False
with assms show ?thesis
by (cases rule: ereal3_cases[of a b c]) auto
qed auto

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 ereal_mult_mono:
fixes a b c d::ereal
assumes "b ≥ 0" "c ≥ 0" "a ≤ b" "c ≤ d"
shows "a * c ≤ b * d"
by (metis ereal_mult_right_mono mult.commute order_trans assms)

lemma ereal_mult_mono':
fixes a b c d::ereal
assumes "a ≥ 0" "c ≥ 0" "a ≤ b" "c ≤ d"
shows "a * c ≤ b * d"
by (metis ereal_mult_right_mono mult.commute order_trans assms)

lemma ereal_mult_mono_strict:
fixes a b c d::ereal
assumes "b > 0" "c > 0" "a < b" "c < d"
shows "a * c < b * d"
proof -
have "c < ∞" using ‹c < d› by auto
then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
moreover have "b * c ≤ b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
ultimately show ?thesis by simp
qed

lemma ereal_mult_mono_strict':
fixes a b c d::ereal
assumes "a > 0" "c > 0" "a < b" "c < d"
shows "a * c < b * d"
using assms ereal_mult_mono_strict by auto

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

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 = d ⟹ (d ≠ 0 ⟹ a = b) ⟹ a * c = b * d"
by (cases "c = 0") simp_all

lemma ereal_right_mult_cong:
fixes a b c :: ereal
shows "c = d ⟹ (d ≠ 0 ⟹ a = b) ⟹ c * a = d * b"
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)"
proof (induct w rule: num_induct)
case One
then show ?case
by simp
next
case (inc x)
then show ?case
by (simp add: inc numeral_inc)
qed

lemma distrib_left_ereal_nn:
"c ≥ 0 ⟹ (x + y) * ereal c = x * ereal c + y * ereal c"
by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)

lemma sum_ereal_right_distrib:
fixes f :: "'a ⇒ ereal"
shows "(⋀i. i ∈ A ⟹ 0 ≤ f i) ⟹ r * sum f A = (∑n∈A. r * f n)"
by (induct A rule: infinite_finite_induct)  (auto simp: ereal_right_distrib sum_nonneg)

lemma sum_ereal_left_distrib:
"(⋀i. i ∈ A ⟹ 0 ≤ f i) ⟹ sum f A * r = (∑n∈A. f n * r :: ereal)"
using sum_ereal_right_distrib[of A f r] by (simp add: mult_ac)

lemma sum_distrib_right_ereal:
"c ≥ 0 ⟹ sum f A * ereal c = (∑x∈A. f x * c :: ereal)"
by(subst sum_comp_morphism[where h="λx. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn)

lemma ereal_le_epsilon:
fixes x y :: ereal
assumes "⋀e. 0 < e ⟹ x ≤ y + e"
shows "x ≤ y"
proof (cases "x = -∞ ∨ x = ∞ ∨ y = -∞ ∨ y = ∞")
case True
then show ?thesis
using assms[of 1] by auto
next
case False
then obtain p q where "x = ereal p" "y = ereal q"
by (metis MInfty_eq_minfinity ereal.distinct(3) uminus_ereal.elims)
then show ?thesis
by (metis assms field_le_epsilon ereal_less(2) ereal_less_eq(3) plus_ereal.simps(1))
qed

lemma ereal_le_epsilon2:
fixes x y :: ereal
assumes "⋀e::real. 0 < e ⟹ x ≤ y + ereal e"
shows "x ≤ y"
proof (rule ereal_le_epsilon)
show "⋀ε::ereal. 0 < ε ⟹ x ≤ y + ε"
using assms less_ereal.elims(2) zero_less_real_of_ereal by fastforce
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 prod_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
qed auto

lemma prod_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
qed auto

lemma prod_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 ≤ prod f I"
by (auto intro!: prod_ereal_pos)
from insert have "(∏j∈insert i I. f j) = ∞ ⟷ prod f I * f i = ∞"
by auto
also have "… ⟷ (prod f I = ∞ ∨ f i = ∞) ∧ f i ≠ 0 ∧ prod f I ≠ 0"
using prod_ereal_pos[of I f] pos
by (cases rule: ereal2_cases[of "f i" "prod 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: prod_ereal_0)
finally show ?case .
qed simp
qed auto

lemma prod_ereal: "(∏i∈A. ereal (f i)) = ereal (prod 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 force
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

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)

fixes a b c :: ereal
shows "a + c ≤ b + c ⟷ 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 ereal_mono_minus_cancel:
fixes a b c :: ereal
shows "c - a ≤ c - b ⟹ 0 ≤ c ⟹ c < ∞ ⟹ b ≤ a"
by (cases a b c rule: ereal3_cases) auto

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

lemma real_of_ereal_minus': "¦x¦ = ∞ ⟷ ¦y¦ = ∞ ⟹ real_of_ereal x - real_of_ereal y = real_of_ereal (x - y :: ereal)"
by(subst real_of_ereal_minus) 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  by (cases x, cases e, auto)+

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

fixes x y z :: ereal
shows "¦y¦ ≠ ∞ ⟹ x - (y + z) = x - y - z"
by(cases x y z rule: ereal3_cases) simp_all

fixes x y z :: ereal
shows "x + y - z = x - z + y"
by(cases x y z rule: ereal3_cases) simp_all

lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x"
by(cases x y rule: ereal2_cases) simp_all

lemma ereal_minus_diff_eq:
fixes x y :: ereal
shows "⟦ x = ∞ ⟶ y ≠ ∞; x = -∞ ⟶ y ≠ - ∞ ⟧ ⟹ - (x - y) = y - x"
by(cases x y rule: ereal2_cases) simp_all

lemma ediff_le_self [simp]: "x - y ≤ (x :: enat)"
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma ereal_abs_diff:
fixes a b::ereal
shows "abs(a-b) ≤ abs a + abs b"
by (cases rule: ereal2_cases[of a b]) (auto)

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 div y = x * inverse (y :: ereal)"

instance ..

end

lemma real_of_ereal_inverse[simp]:
fixes a :: ereal
shows "real_of_ereal (inverse a) = 1 / real_of_ereal 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 :: ```