# Theory HOL-Library.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 theoryHOL-Library.Extended_Nat or theoryHOL-Library.Order_Continuity, but then the AFP-entry Jinja_Thread› fails, as it does overload
certain named from theoryComplex_Main.
›

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

lemma incseq_sumI:
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"
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
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 ::
assumes f:
shows "continuous (at_left x) f"
proof cases
assume "x = bot" then show ?thesis
next
assume x: "x  bot"
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_left_sequentially[of ])
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 ::
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
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 ::
assumes f:
shows "continuous (at_right x) f"
proof cases
assume "x = top" then show ?thesis
next
assume x: "x  top"
show ?thesis
unfolding continuous_within
proof (intro tendsto_at_right_sequentially[of _ ])
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 ::
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  "  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
qed

proof
have [simp]: "enat i  aa  enat i  aa + ba" for aa ba i
by (rule order_trans[OF _ add_mono[of aa aa  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
.
›

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)"
|
|

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]:
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"

declare
PInfty_eq_infinity[code_post]
MInfty_eq_minfinity[code_post]

lemma [code_unfold]:
" = PInfty"

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 ::
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)"

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)"
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)"

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 typereal"

instantiation ereal :: linorder
begin

function less_ereal
where
"   ereal x < ereal y      x < y"
| "(::ereal) < a            False"
| "         a < -(::ereal)  False"
| "ereal x    <             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 = -"

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"

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)

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)"

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 propa < 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"

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"

lemma ereal_le_less: "ereal y  a  x < y  ereal x < a"

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]:
by (cases x) auto

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

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]: "(xA. ereal (f x)) = ereal (xA. 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 "(xP. f x) =   finite P  (iP. f i = )"
proof safe
assume *: "sum f P = "
show "finite P"
proof (rule ccontr)
assume "¬ finite P"
with * show False
by auto
qed
show "iP. 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  (iA. ¦f i¦ = )"
proof
assume *: "¦sum f A¦ = "
have "finite A"
by (rule ccontr) (insert *, auto)
moreover have "iA. ¦f i¦ = "
proof (rule ccontr)
assume "¬ ?thesis"
then have "iA. r. f i = ereal r"
by auto
from bchoice[OF this] obtain r where "xA. f x = ereal (r x)" ..
with * show False
by auto
qed
ultimately show "finite A  (iA. ¦f i¦ = )"
by auto
next
assume "finite A  (iA. ¦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 "(xS. real_of_ereal (f x)) = real_of_ereal (sum f S)"
proof -
have "xS. 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 "xS. 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 "(xA. f x) = 0  (iA. f i = 0)"
proof
assume "sum f A = 0" with assms show "iA. f i = 0"
proof (induction A)
case (insert a A)
then have "f a = 0  (aA. 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) *  = "
| "-(::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])
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))"

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"

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)"

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

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

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)"

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
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 = (nA. 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 = (nA. 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 = (xA. 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 "(iA. f i) = 0  finite A  (iA. 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  (iI. 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 "(iI. f i) =   finite I  (iI. f i = )  (iI. 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 "(jinsert 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)  (jinsert i I. f j = )  (jinsert i I. f j  0)"
using insert by (auto simp: prod_ereal_0)
finally show ?case .
qed simp
qed auto

lemma prod_ereal: "(iA. 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
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
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"

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
by (cases rule: ereal2_cases[of a b]) auto

lemma real_of_ereal_minus':
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
by (cases a) (auto simp: inverse_eq_divide)

lemma ereal_inverse[simp]:
"inverse (0::ereal) = "
"inverse (1::ereal) = 1"