(*  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

begin

text {*

For more lemmas about the extended real numbers go to

  @{text "src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}

*}

lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"

proof

  assume "{x..} = UNIV"

  show "x = bot"

  proof (rule ccontr)

    assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less)

    then show False using `{x..} = UNIV` by simp

  qed

qed auto

lemma SUPR_pair:

  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"

  by (rule antisym) (auto intro!: SUP_leI le_SUPI2)

lemma INFI_pair:

  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"

  by (rule antisym) (auto intro!: le_INFI INF_leI2)

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 "(\<infinity>::ereal) = PInfty"

  instance ..

end

definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"

declare [[coercion "ereal :: real \<Rightarrow> ereal"]]

declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]

declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]]

lemma ereal_uminus_uminus[simp]:

  fixes a :: ereal shows "- (- a) = a"

  by (cases a) simp_all

lemma

  shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>"

    and MInfty_eq_minfinity[simp]: "MInfty = - \<infinity>"

    and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "- \<infinity> \<noteq> (\<infinity>::ereal)"

    and MInfty_neq_ereal[simp]: "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r"

    and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r"

    and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = y"

    and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"

  by (simp_all add: infinity_ereal_def)

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 "\<And>r. x = ereal r \<Longrightarrow> P"

  assumes "x = \<infinity> \<Longrightarrow> P"

  assumes "x = -\<infinity> \<Longrightarrow> 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 \<longleftrightarrow> a = b"

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

function of_ereal :: "ereal \<Rightarrow> real" where

"of_ereal (ereal r) = r" |

"of_ereal \<infinity> = 0" |

"of_ereal (-\<infinity>) = 0"

  by (auto intro: ereal_cases)

termination proof qed (rule wf_empty)

defs (overloaded)

  real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"

lemma real_of_ereal[simp]:

    "real (- x :: ereal) = - (real x)"

    "real (ereal r) = r"

    "real (\<infinity>::ereal) = 0"

  by (cases x) (simp_all add: real_of_ereal_def)

lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"

proof safe

  fix x assume "x \<notin> range ereal" "x \<noteq> \<infinity>"

  then show "x = -\<infinity>" by (cases x) auto

qed auto

lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"

proof safe

  fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto

qed auto

instantiation ereal :: number

begin

definition [simp]: "number_of x = ereal (number_of x)"

instance proof qed

end

instantiation ereal :: abs

begin

  function abs_ereal where

    "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"

  | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"

  | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"

  by (auto intro: ereal_cases)

  termination proof qed (rule wf_empty)

  instance ..

end

lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"

  by (cases x) auto

lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"

  by (cases x) auto

lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"

  by (cases x) auto

subsubsection "Addition"

instantiation ereal :: comm_monoid_add

begin

definition "0 = ereal 0"

function plus_ereal where

"ereal r + ereal p = ereal (r + p)" |

"\<infinity> + a = (\<infinity>::ereal)" |

"a + \<infinity> = (\<infinity>::ereal)" |

"ereal r + -\<infinity> = - \<infinity>" |

"-\<infinity> + ereal p = -(\<infinity>::ereal)" |

"-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"

proof -

  case (goal1 P x)

  moreover then obtain a b where "x = (a, b)" by (cases x) auto

  ultimately show P

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

qed auto

termination proof qed (rule wf_empty)

lemma Infty_neq_0[simp]:

  "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"

  "-(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> -(\<infinity>::ereal)"

  by (simp_all add: zero_ereal_def)

lemma ereal_eq_0[simp]:

  "ereal r = 0 \<longleftrightarrow> r = 0"

  "0 = ereal r \<longleftrightarrow> r = 0"

  unfolding zero_ereal_def by simp_all

instance

proof

  fix a :: ereal show "0 + a = a"

    by (cases a) (simp_all add: zero_ereal_def)

  fix b :: ereal show "a + b = b + a"

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

  fix c :: ereal show "a + b + c = a + (b + c)"

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

qed

end

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]: "\<bar>0\<bar> = (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 \<longleftrightarrow> a = 0"

  by (cases a) simp_all

lemma ereal_plus_eq_PInfty[simp]:

  fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"

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

lemma ereal_plus_eq_MInfty[simp]:

  fixes a b :: ereal shows "a + b = -\<infinity> \<longleftrightarrow>

    (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"

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

lemma ereal_add_cancel_left:

  fixes a b :: ereal assumes "a \<noteq> -\<infinity>"

  shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> 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 \<noteq> -\<infinity>"

  shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"

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

lemma ereal_real:

  "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"

  by (cases x) simp_all

lemma real_of_ereal_add:

  fixes a b :: ereal

  shows "real (a + b) = (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) 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     \<longleftrightarrow> x < y" |

"(\<infinity>::ereal) < a           \<longleftrightarrow> False" |

"         a < -(\<infinity>::ereal) \<longleftrightarrow> False" |

"ereal x    < \<infinity>           \<longleftrightarrow> True" |

"        -\<infinity> < ereal r     \<longleftrightarrow> True" |

"        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"

proof -

  case (goal1 P x)

  moreover then obtain a b where "x = (a,b)" by (cases x) auto

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

qed simp_all

termination by (relation "{}") simp

definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y"

lemma ereal_infty_less[simp]:

  fixes x :: ereal

  shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"

    "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"

  by (cases x, simp_all) (cases x, simp_all)

lemma ereal_infty_less_eq[simp]:

  fixes x :: ereal

  shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"

  "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"

  by (auto simp add: less_eq_ereal_def)

lemma ereal_less[simp]:

  "ereal r < 0 \<longleftrightarrow> (r < 0)"

  "0 < ereal r \<longleftrightarrow> (0 < r)"

  "0 < (\<infinity>::ereal)"

  "-(\<infinity>::ereal) < 0"

  by (simp_all add: zero_ereal_def)

lemma ereal_less_eq[simp]:

  "x \<le> (\<infinity>::ereal)"

  "-(\<infinity>::ereal) \<le> x"

  "ereal r \<le> ereal p \<longleftrightarrow> r \<le> p"

  "ereal r \<le> 0 \<longleftrightarrow> r \<le> 0"

  "0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"

  by (auto simp add: less_eq_ereal_def zero_ereal_def)

lemma ereal_infty_less_eq2:

  "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"

  "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -(\<infinity>::ereal)"

  by simp_all

instance

proof

  fix x :: ereal show "x \<le> x"

    by (cases x) simp_all

  fix y :: ereal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"

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

  show "x \<le> y \<or> y \<le> x "

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

  { assume "x \<le> y" "y \<le> x" then show "x = y"

    by (cases rule: ereal2_cases[of x y]) auto }

  { fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z"

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

qed

end

instance ereal :: ordered_ab_semigroup_add

proof

  fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"

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

qed

lemma real_of_ereal_positive_mono:

  fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"

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

lemma ereal_MInfty_lessI[intro, simp]:

  fixes a :: ereal shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"

  by (cases a) auto

lemma ereal_less_PInfty[intro, simp]:

  fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"

  by (cases a) auto

lemma ereal_less_ereal_Ex:

  fixes a b :: ereal

  shows "x < ereal r \<longleftrightarrow> x = -\<infinity> \<or> (\<exists>p. p < r \<and> x = ereal p)"

  by (cases x) auto

lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>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 \<le> b" "c \<le> d" shows "a + c \<le> 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 \<le> - b \<longleftrightarrow> b \<le> a"

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

lemma ereal_minus_less_minus[simp]:

  fixes a b :: ereal shows "- a < - b \<longleftrightarrow> b < a"

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

lemma ereal_le_real_iff:

  "x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))"

  by (cases y) auto

lemma real_le_ereal_iff:

  "real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))"

  by (cases y) auto

lemma ereal_less_real_iff:

  "x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))"

  by (cases y) auto

lemma real_less_ereal_iff:

  "real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"

  by (cases y) auto

lemma real_of_ereal_pos:

  fixes x :: ereal shows "0 \<le> x \<Longrightarrow> 0 \<le> 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 \<le> x \<Longrightarrow> \<bar>x :: ereal\<bar> = x"

  by (cases x) auto

lemma abs_ereal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: ereal\<bar> = -x"

  by (cases x) auto

lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"

  by (cases x) auto

lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)"

  by (cases x) auto

lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"

  by (cases x) auto

lemma zero_less_real_of_ereal:

  fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)"

  by (cases x) auto

lemma ereal_0_le_uminus_iff[simp]:

  fixes a :: ereal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"

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

lemma ereal_uminus_le_0_iff[simp]:

  fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"

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

lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"

  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto

lemma ereal_dense:

  fixes x y :: ereal assumes "x < y"

  shows "\<exists>z. x < z \<and> z < y"

  using ereal_dense2[OF `x < y`] by blast

lemma ereal_add_strict_mono:

  fixes a b c d :: ereal

  assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "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 "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"

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

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

lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"

  by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)

lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (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 "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"

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 "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"

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 \<Rightarrow> ereal"

  shows incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"

  and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"

  unfolding decseq_def incseq_def by auto

lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"

  unfolding incseq_def by auto

lemma ereal_add_nonneg_nonneg:

  fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"

  using add_mono[of 0 a 0 b] by simp

lemma image_eqD: "f ` A = B \<Longrightarrow> (\<forall>x\<in>A. f x \<in> B)"

  by auto

lemma incseq_setsumI:

  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"

  assumes "\<And>i. 0 \<le> f i"

  shows "incseq (\<lambda>i. setsum f {..< i})"

proof (intro incseq_SucI)

  fix n have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"

    using assms by (rule add_left_mono)

  then show "setsum f {..< n} \<le> setsum f {..< Suc n}"

    by auto

qed

lemma incseq_setsumI2:

  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"

  assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"

  shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"

  using assms unfolding incseq_def by (auto intro: setsum_mono)

subsubsection "Multiplication"

instantiation ereal :: "{comm_monoid_mult, sgn}"

begin

definition "1 = ereal 1"

function sgn_ereal where

  "sgn (ereal r) = ereal (sgn r)"

| "sgn (\<infinity>::ereal) = 1"

| "sgn (-\<infinity>::ereal) = -1"

by (auto intro: ereal_cases)

termination proof qed (rule wf_empty)

function times_ereal where

"ereal r * ereal p = ereal (r * p)" |

"ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |

"\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |

"ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |

"-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |

"(\<infinity>::ereal) * \<infinity> = \<infinity>" |

"-(\<infinity>::ereal) * \<infinity> = -\<infinity>" |

"(\<infinity>::ereal) * -\<infinity> = -\<infinity>" |

"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"

proof -

  case (goal1 P x)

  moreover then obtain a b where "x = (a, b)" by (cases x) auto

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

qed simp_all

termination by (relation "{}") simp

instance

proof

  fix a :: ereal show "1 * a = a"

    by (cases a) (simp_all add: one_ereal_def)

  fix b :: ereal show "a * b = b * a"

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

  fix c :: ereal 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_of_ereal_le_1:

  fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"

  by (cases a) (auto simp: one_ereal_def)

lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (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 \<noteq> (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 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"

  "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 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 + -(\<infinity>::ereal) = -\<infinity>" "-(\<infinity>::ereal) + 1 = -\<infinity>"

  unfolding one_ereal_def by auto

lemma ereal_zero_times[simp]:

  fixes a b :: ereal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"

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

lemma ereal_mult_eq_PInfty[simp]:

  shows "a * b = (\<infinity>::ereal) \<longleftrightarrow>

    (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"

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

lemma ereal_mult_eq_MInfty[simp]:

  shows "a * b = -(\<infinity>::ereal) \<longleftrightarrow>

    (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"

  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 \<noteq> (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 * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"

  by (cases a) auto

lemma ereal_infty_mult[simp]:

  "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"

  by (cases a) auto

lemma ereal_mult_strict_right_mono:

  assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)"

  shows "a * c < b * c"

  using assms

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

     (auto simp: zero_le_mult_iff ereal_less_PInfty)

lemma ereal_mult_strict_left_mono:

  "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c"

  using assms

  apply (cases "c = 0") apply simp

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

     (auto simp: zero_le_mult_iff ereal_less_PInfty)

lemma ereal_mult_left_mono:

  fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"

  using ereal_mult_right_mono by (simp add: mult_commute[of c])

lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"

  by (simp add: one_ereal_def zero_ereal_def)

lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> 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 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 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 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (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 \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> 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 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 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 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 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 \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"

  by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)

lemma ereal_distrib:

  fixes a b c :: ereal

  assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"

  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 ereal_le_epsilon:

  fixes x y :: ereal

  assumes "ALL e. 0 < e --> x <= y + e"

  shows "x <= y"

proof-

{ assume a: "EX r. y = ereal r"

  from this obtain r where r_def: "y = ereal r" by auto

  { assume "x=(-\<infinity>)" hence ?thesis by auto }

  moreover

  { assume "~(x=(-\<infinity>))"

    from this 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 }

    hence "p <= r" apply (subst field_le_epsilon) by auto

    hence ?thesis using r_def p_def by auto

  } ultimately have ?thesis by blast

}

moreover

{ assume "y=(-\<infinity>) | y=\<infinity>" hence ?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 "ALL e. 0 < e --> x <= y + ereal e"

  shows "x <= y"

proof-

{ fix e :: ereal assume "e>0"

  { assume "e=\<infinity>" hence "x<=y+e" by auto }

  moreover

  { assume "e~=\<infinity>"

    from this obtain r where "e = ereal r" using `e>0` apply (cases e) by auto

    hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto

  } ultimately have "x<=y+e" by blast

} from this show ?thesis using ereal_le_epsilon by auto

qed

lemma ereal_le_real:

  fixes x y :: ereal

  assumes "ALL z. x <= ereal z --> y <= ereal z"

  shows "y <= x"

by (metis assms ereal_bot ereal_cases ereal_infty_less_eq ereal_less_eq linorder_le_cases)

lemma ereal_le_ereal:

  fixes x y :: ereal

  assumes "\<And>B. B < x \<Longrightarrow> B <= y"

  shows "x <= y"

by (metis assms ereal_dense leD linorder_le_less_linear)

lemma ereal_ge_ereal:

  fixes x y :: ereal

  assumes "ALL B. B>x --> B >= y"

  shows "x >= y"

by (metis assms ereal_dense leD linorder_le_less_linear)

lemma setprod_ereal_0:

  fixes f :: "'a \<Rightarrow> ereal"

  shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"

proof cases

  assume "finite A"

  then show ?thesis by (induct A) auto

qed auto

lemma setprod_ereal_pos:

  fixes f :: "'a \<Rightarrow> ereal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"

proof cases

  assume "finite I" from this pos show ?thesis by induct auto

qed simp

lemma setprod_PInf:

  fixes f :: "'a \<Rightarrow> ereal"

  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"

  shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"

proof cases

  assume "finite I" from this assms show ?thesis

  proof (induct I)

    case (insert i I)

    then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_ereal_pos)

    from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto

    also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"

      using setprod_ereal_pos[of I f] pos

      by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto

    also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"

      using insert by (auto simp: setprod_ereal_0)

    finally show ?case .

  qed simp

qed simp

lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"

proof cases

  assume "finite A" then show ?thesis

    by induct (auto simp: one_ereal_def)

qed (simp add: one_ereal_def)

subsubsection {* Power *}

instantiation ereal :: power

begin

primrec power_ereal where

  "power_ereal x 0 = 1" |

  "power_ereal x (Suc n) = x * x ^ n"

instance ..

end

lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"

  by (induct n) (auto simp: one_ereal_def)

lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)"

  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_number_of[simp]:

  "(number_of num :: ereal) ^ n = ereal (number_of num ^ n)"

  by (induct n) (auto simp: one_ereal_def)

lemma zero_le_power_ereal[simp]:

  fixes a :: ereal assumes "0 \<le> a"

  shows "0 \<le> 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 (safe intro!: image_eqI)

  fix x assume "-a < x"

  then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)

  then show "- x < a" by simp

qed auto

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

  "-\<infinity> - ereal r = -\<infinity>"

  "ereal r - \<infinity> = -\<infinity>"

  "(\<infinity>::ereal) - x = \<infinity>"

  "-(\<infinity>::ereal) - \<infinity> = -\<infinity>"

  "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 \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"

  by (cases x) simp_all

lemma ereal_eq_minus_iff:

  fixes x y z :: ereal

  shows "x = z - y \<longleftrightarrow>

    (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and>

    (y = -\<infinity> \<longrightarrow> x = \<infinity>) \<and>

    (y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and>

    (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>)"

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

lemma ereal_eq_minus:

  fixes x y z :: ereal

  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x = z - y \<longleftrightarrow> x + y = z"

  by (auto simp: ereal_eq_minus_iff)

lemma ereal_less_minus_iff:

  fixes x y z :: ereal

  shows "x < z - y \<longleftrightarrow>

    (y = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and>

    (y = -\<infinity> \<longrightarrow> x \<noteq> \<infinity>) \<and>

    (\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)"

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

lemma ereal_less_minus:

  fixes x y z :: ereal

  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x < z - y \<longleftrightarrow> x + y < z"

  by (auto simp: ereal_less_minus_iff)

lemma ereal_le_minus_iff:

  fixes x y z :: ereal

  shows "x \<le> z - y \<longleftrightarrow>

    (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and>

    (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"

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

lemma ereal_le_minus:

  fixes x y z :: ereal

  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x \<le> z - y \<longleftrightarrow> x + y \<le> z"

  by (auto simp: ereal_le_minus_iff)

lemma ereal_minus_less_iff:

  fixes x y z :: ereal

  shows "x - y < z \<longleftrightarrow>

    y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and>

    (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"

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

lemma ereal_minus_less:

  fixes x y z :: ereal

  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y < z \<longleftrightarrow> x < z + y"

  by (auto simp: ereal_minus_less_iff)

lemma ereal_minus_le_iff:

  fixes x y z :: ereal

  shows "x - y \<le> z \<longleftrightarrow>

    (y = -\<infinity> \<longrightarrow> z = \<infinity>) \<and>

    (y = \<infinity> \<longrightarrow> x = \<infinity> \<longrightarrow> z = \<infinity>) \<and>

    (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)"

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

lemma ereal_minus_le:

  fixes x y z :: ereal

  shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - y \<le> z \<longleftrightarrow> x \<le> 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 \<longleftrightarrow>

    b = c \<or> a = \<infinity> \<or> (a = -\<infinity> \<and> b \<noteq> -\<infinity> \<and> c \<noteq> -\<infinity>)"

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

lemma ereal_add_le_add_iff:

  fixes a b c :: ereal

  shows "c + a \<le> c + b \<longleftrightarrow>

    a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"

  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 "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 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 \<le> B" "D \<le> C"

  shows "A - C \<le> 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 \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> 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 \<le> b \<Longrightarrow> 0 \<le> b - a"

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

lemma ereal_between:

  fixes x e :: ereal

  assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"

  shows "x - e < x" "x < x + e"

using assms apply (cases x, cases e) apply auto

using assms by (cases x, cases e) auto

subsubsection {* Division *}

instantiation ereal :: inverse

begin

function inverse_ereal where

"inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" |

"inverse (\<infinity>::ereal) = 0" |

"inverse (-\<infinity>::ereal) = 0"

  by (auto intro: ereal_cases)

termination by (relation "{}") simp

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

instance proof qed

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) = \<infinity>"

  "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 * \<infinity> 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 \<bar>x\<bar> = \<infinity> \<or> 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 \<noteq> -\<infinity> then x else \<infinity>)"

  by (cases x) auto

lemma ereal_inverse_minus[simp]:

  fixes x :: ereal shows "inverse (- x) = (if x = 0 then \<infinity> 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 / \<infinity> = 0" "x / -\<infinity> = 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]:

  "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"

  unfolding divide_ereal_def by simp

lemma zero_le_divide_ereal[simp]:

  fixes a :: ereal assumes "0 \<le> a" "0 \<le> b"

  shows "0 \<le> a / b"