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 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:
  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
    by (metis add.commute)
  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

subsubsection "Addition"

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

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

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

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

lemma real_of_ereal_add:
  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 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

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

lemma ereal_abs_add:
  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

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

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

lemma ereal_add_nonneg_eq_0_iff:
  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]: "(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"
      by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: sum_nonneg)
    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 = (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
    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

lemma ereal_add_le_add_iff:
  fixes a b c :: ereal
  shows "c + a  c + b 
    a  b  c =   (c = -  a    b  )"
  by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma ereal_add_le_add_iff2:
  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

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

lemma ereal_diff_add_assoc2:
  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 ::