Quelle  Extended_Real.thy   Sprache: Isabelle

(*  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 🍋‹HOL-Library.Extended_Nat› or 🍋‹HOL-Library.Order_Continuity›, but then the AFP-entry ‹Jinja_Thread› fails, as it does overload
  certain named from 🍋‹Complex_Main›.
›

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

lemma incseq_sumI:
  fixes f :: "nat \ 'a::ordered_comm_monoid_add"
  assumes "\i. 0 \ f i"
  shows "incseq (\i. sum f {..< i})"
proof (intro incseq_SucI)
  fix n
  have "sum f {..< n} + 0 \ sum f {..
    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 continuous_at_left_imp_sup_continuous sup_continuous_at_left sup_continuous_mono
  by blast

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"
    then have x_eq: "x = (INF i. S i)"
      using INF_Lim by blast
    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 continuous_at_right_imp_inf_continuous inf_continuous_at_right inf_continuous_mono
  by blast

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: 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: 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 
  have "\\<^sub>F x in INF m n. principal ({enat n..} \ {enat m..}). enat i \ fst x + snd x"
       "\\<^sub>F x in INF n. principal ({enat n..} \ {enat j}). enat i \ fst x + snd x" 
       "\\<^sub>F x in INF n. principal ({enat j} \ {enat n..}). enat i \ fst x + snd x" 
    for i j
    by (auto intro!: eventually_INF1[of i] simp: eventually_principal)
  then show "((\x. fst x + snd x) \ a + b) (nhds a \\<^sub>F nhds b)"
    by (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2
        filterlim_principal principal_prod_principal eventually_principal)
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

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

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

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

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 auto

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 auto


subsubsection "Linear order on \<^typ>\ereal\"

instantiation ereal :: linorder
begin

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

definition "x \ (y::ereal) \ x < y \ x = y"

lemma ereal_infty_less[simp]:
  fixes x :: ereal
  shows "x < \ \ (x \ \)"
       "-\ < x \ (x \ -\)"
  by (cases x, simp_all)+

lemma ereal_infty_less_eq[simp]:
  fixes x :: ereal
  shows "\ \ x \ x = \"
    and "x \ -\ \ x = -\"
  by (auto simp: 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: 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"
  then show "y \ x \ x = y"
    by (cases rule: ereal2_cases[of x y]) auto
  show "y \ z \ x \ z"
    using ‹x ≤ y›
    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 simp

lemma ereal_less_PInfty[intro, simp]:
  fixes a :: ereal
  shows "a \ \ \ a < \"
  by simp

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: 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 🍋‹a < ereal x ==> x < y ==> a < ereal y›,
  where x and y are real.
›

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

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

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

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

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

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

lemma real_of_ereal_pos:
  fixes x :: ereal
  shows "0 \ x \ 0 \ real_of_ereal x" 
  by (cases x) auto

lemmas real_of_ereal_ord_simps =
  ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff

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

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

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

lemma ereal_abs_leI:
  fixes x y :: ereal
  shows "\ x \ y; -x \ y \ \ \x\ \ y"
  by(cases x y rule: ereal2_cases)(simp_all)

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_uminus_eq_reorder: "- a = b \ a = (-b::ereal)"
  by auto

lemma ereal_uminus_less_reorder: "- a < b \ -b < a"
  and ereal_less_uminus_reorder: "a < - b \ b < - a"
  and ereal_uminus_le_reorder: "- a \ b \ -b \ a" for a::ereal
  using ereal_minus_le_minus ereal_minus_less_minus by fastforce+

lemmas ereal_uminus_reorder =
  ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder

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

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

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

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

lemma
  fixes f :: "nat \ ereal"
  shows ereal_incseq_uminus[simp]: "incseq (\x. - f x) \ decseq f"
    and ereal_decseq_uminus[simp]: "decseq (\x. - f x) \ incseq f"
  unfolding decseq_def incseq_def by auto

lemma incseq_ereal: "incseq f \ incseq (\x. ereal (f x))"
  unfolding incseq_def by auto

lemma sum_ereal[simp]: "(\x\A. ereal (f x)) = ereal (\x\A. f x)"
  by (induction A rule: infinite_finite_induct) auto

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

lemma sum_Pinfty:
  fixes f :: "'a \ ereal"
  shows "(\x\P. f x) = \ \ finite P \ (\i\P. f i = \)"
proof safe
  assume *: "sum f P = \"
  show "finite P"
    by (metis "*" Infty_neq_0(2) sum.infinite)
  show "\i\P. f i = \"
  proof (rule ccontr)
    assume "\ ?thesis"
    then have "\i. i \ P \ f i \ \"
      by auto
    with ‹finite P› have "sum f P \ \"
      by induct auto
    with * show False
      by auto
  qed
next
  fix i
  assume "finite P" and "i \ P" and "f i = \"
  then show "sum f P = \"
  proof induct
    case (insert x A)
    show ?case using insert by (cases "x = i") auto
  qed simp
qed

lemma sum_Inf:
  fixes f :: "'a \ ereal"
  shows "\sum f A\ = \ \ finite A \ (\i\A. \f i\ = \)"
proof
  assume *: "\sum f A\ = \"
  have "finite A"
    by (rule ccontr) (insert *, auto)
  moreover have "\i\A. \f i\ = \"
  proof (rule ccontr)
    assume "\ ?thesis"
    then have "\i\A. \r. f i = ereal r"
      by auto
    then obtain r where "\x\A. f x = ereal (r x)" 
      by metis
    with * show False
      by auto
  qed
  ultimately show "finite A \ (\i\A. \f i\ = \)"
    by auto
next
  assume "finite A \ (\i\A. \f i\ = \)"
  then obtain i where "finite A" "i \ A" and "\f i\ = \"
    by auto
  then show "\sum f A\ = \"
  proof induct
    case (insert j A)
    then show ?case
      by (cases rule: ereal3_cases[of "f i" "f j" "sum f A"]) auto
  qed simp
qed

lemma sum_real_of_ereal:
  fixes f :: "'i \ ereal"
  assumes "\x. x \ S \ \f x\ \ \"
  shows "(\x\S. real_of_ereal (f x)) = real_of_ereal (sum f S)"
proof -
  have "\x\S. \r. f x = ereal r"
    using assms by blast
  then obtain r where "\x\S. f x = ereal (r x)" 
    by metis
  then show ?thesis
    by simp
qed

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

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 (metis ereal_mult_zero mult.commute)

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 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"
  by (simp add: ereal_mult_right_mono mult.commute)

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(1,4) ereal_mult_left_mono by force 
  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 m1_ereal_less_iff [simp]:
  "((-1::ereal) < numeral a) \ ((-1::real) < numeral a)"
  by (simp add: one_ereal_def)

lemma m1_ereal_le_iff [simp]:
  "((-1::ereal) \ numeral a) \ ((-1::real) \ numeral a)"
  by (simp add: one_ereal_def)

lemma m1_ereal_eq_iff [simp]:
  "((-1::ereal) = numeral a) \ ((-1::real) = numeral a)"
  by (simp add: one_ereal_def)

lemma ereal_less_m1_iff [simp]:
  "(numeral a < (-1::ereal)) \ (numeral a < (-1::real))"
  by (simp add: one_ereal_def)

lemma ereal_le_m1_iff [simp]:
  "(numeral a \ (-1::ereal)) \ (numeral a \ (-1::real))"
  by (simp add: one_ereal_def)

lemma ereal_eq_m1_iff [simp]:
  "(numeral a = (-1::ereal)) \ (numeral a = (-1::real))"
  by (simp add: one_ereal_def)

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

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

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

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

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

lemma ereal_le_epsilon2:
  fixes x y :: ereal
  assumes "\e::real. 0 < e \ x \ y + ereal e"
  shows "x \ y"
proof (rule ereal_le_epsilon)
  show "\\::ereal. 0 < \ \ x \ y + \"
  using assms less_ereal.elims(2) zero_less_real_of_ereal by fastforce
qed

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

lemma prod_ereal_0:
  fixes f :: "'a \ ereal"
  shows "(\i\A. f i) = 0 \ finite A \ (\i\A. f i = 0)"
  by (induction A rule: infinite_finite_induct) auto

lemma prod_ereal_pos:
  fixes f :: "'a \ ereal"
  assumes "\i. i \ I \ 0 \ f i"
  shows "0 \ (\i\I. f i)"
  using assms
  by (induction I rule: infinite_finite_induct) auto

lemma prod_PInf:
  fixes f :: "'a \ ereal"
  assumes "\i. i \ I \ 0 \ f i"
  shows "(\i\I. f i) = \ \ finite I \ (\i\I. f i = \) \ (\i\I. f i \ 0)"
  using assms
proof (induction I rule: infinite_finite_induct)
  case (insert i I)
  then have pos: "0 \ f i" "0 \ prod f I"
    by (auto intro!: prod_ereal_pos)
  from insert have "(\j\insert i I. f j) = \ \ prod f I * f i = \"
    by auto
  also have "\ \ (prod f I = \ \ f i = \) \ f i \ 0 \ prod f I \ 0"
    using prod_ereal_pos[of I f] pos
    by (cases rule: ereal2_cases[of "f i" "prod f I"]) auto
  also have "\ \ finite (insert i I) \ (\j\insert i I. f j = \) \ (\j\insert i I. f j \ 0)"
    using insert by (auto simp: prod_ereal_0)
  finally show ?case .
qed auto

lemma prod_ereal: "(\i\A. ereal (f i)) = ereal (prod f A)"
  by (induction A rule: infinite_finite_induct) (auto simp: one_ereal_def)


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 ` {..
  by (force simp: ereal_uminus_less_reorder)

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 auto

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 (metis (no_types, lifting) add.commute ereal_add_le_add_iff)

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 (simp add: add.commute minus_ereal_def)

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 :: ereal
  shows "x / \ = 0" "x / -\ = 0"
  unfolding divide_ereal_def by simp_all

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

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

lemma ereal_inverse_nonneg_iff: "0 \ inverse (x :: ereal) \ 0 \ x \ x = -\"
  by (cases x) auto

lemma inverse_ereal_ge0I: "0 \ (x :: ereal) \ 0 \ inverse x"
by(cases x) simp_all

lemma zero_le_divide_ereal[simp]:
  fixes a :: ereal
  assumes "0 \ a" and "0 \ b"
  shows "0 \ a / b"
  by (simp add: assms divide_ereal_def ereal_inverse_nonneg_iff)

lemma ereal_le_divide_pos:
  fixes x y z :: ereal
  shows "x > 0 \ x \ \ \ y \ z / x \ x * y \ z"
  by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

lemma ereal_divide_le_pos:
  fixes x y z :: ereal
  shows "x > 0 \ x \ \ \ z / x \ y \ z \ x * y"
  by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)

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

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

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

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

lemma inverse_inverse_Pinfty_iff[simp]:
  fixes x :: ereal
  shows "inverse x = \ \ x = 0"
  by (cases x) auto

lemma ereal_inverse_eq_0:
  fixes x :: ereal
  shows "inverse x = 0 \ x = \ \ x = -\"
  by (cases x) auto

lemma ereal_0_gt_inverse:
  fixes x :: ereal
  shows "0 < inverse x \ x \ \ \ 0 \ x"
  by (cases x) auto

lemma ereal_inverse_le_0_iff:
  fixes x :: ereal
  shows "inverse x \ 0 \ x < 0 \ x = \"
  by(cases x) auto

lemma ereal_divide_eq_0_iff: "x / y = 0 \ x = 0 \ \y :: ereal\ = \"
by(cases x y rule: ereal2_cases) simp_all

lemma ereal_mult_less_right:
  fixes a b c :: ereal
  assumes "b * a < c * a" "0 < a" "a < \"
  shows "b < c"
  using assms
  by (metis order.asym ereal_mult_strict_left_mono linorder_neqE mult.commute)

lemma ereal_mult_divide: 
  fixes a b :: ereal 
  shows "0 < b \ b < \ \ b * (a / b) = a"
  by (cases a b rule: ereal2_cases) auto

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

lemma ereal_le_mult_one_interval:
  fixes x y :: ereal
  assumes y: "y \ -\"
  assumes z: "\z. 0 < z \ z < 1 \ z * x \ y"
  shows "x \ y"
proof (cases x)
  case PInf
  with z[of "1 / 2"] show "x \ y"
    by (simp add: one_ereal_def)
next
  case r: (real r)
  show "x \ y"
  proof (cases y)
    case p: (real p)
    have "r \ p"
    proof (rule field_le_mult_one_interval)
      fix z :: real
      assume "0 < z" and "z < 1"
      with z[of "ereal z"] show "z * r \ p"
        using p r by (auto simp: zero_le_mult_iff one_ereal_def)
    qed
    then show "x \ y"
      using p r by simp
  qed (use y in simp_all)
qed simp

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

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

lemma ereal_divide_zero_left[simp]:
  fixes a :: ereal
  shows "0 / a = 0"
  using ereal_divide_eq_0_iff by blast

lemma ereal_times_divide_eq_left[simp]:
  fixes a b c :: ereal
  shows "b / c * a = b * a / c"
  by (metis divide_ereal_def mult.assoc mult.commute)

lemma ereal_times_divide_eq: "a * (b / c :: ereal) = a * b / c"
  by (metis ereal_times_divide_eq_left mult.commute)

lemma ereal_inverse_real [simp]: "\z\ \ \ \ z \ 0 \ ereal (inverse (real_of_ereal z)) = inverse z"
  by auto

lemma ereal_inverse_mult:
  "a \ 0 \ b \ 0 \ inverse (a * (b::ereal)) = inverse a * inverse b"
  by (cases a; cases b) auto

lemma inverse_eq_infinity_iff_eq_zero [simp]:
  "1/(x::ereal) = \ \ x = 0"
by (simp add: divide_ereal_def)

lemma ereal_distrib_left:
  fixes a b c :: ereal
  assumes "a \ \ \ b \ -\"
      and "a \ -\ \ b \ \"
      and "\c\ \ \"
  shows "c * (a + b) = c * a + c * b"
  by (metis assms ereal_distrib mult.commute)

lemma ereal_distrib_minus_left:
  fixes a b c :: ereal
  assumes "a \ \ \ b \ \"
      and "a \ -\ \ b \ -\"
      and "\c\ \ \"
  shows "c * (a - b) = c * a - c * b"
  using assms ereal_distrib_left ereal_uminus_eq_reorder minus_ereal_def by auto

lemma ereal_distrib_minus_right:
  fixes a b c :: ereal
  assumes "a \ \ \ b \ \"
      and "a \ -\ \ b \ -\"
      and "\c\ \ \"
  shows "(a - b) * c = a * c - b * c"
  by (metis assms ereal_distrib_minus_left mult.commute)


subsection "Complete lattice"

instantiation ereal :: lattice
begin

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

end

instantiation ereal :: complete_lattice
begin

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

definition "Sup S = (SOME x :: ereal. (\y\S. y \ x) \ (\z. (\y\S. y \ z) \ x \ z))"
definition "Inf S = (SOME x :: ereal. (\y\S. x \ y) \ (\z. (\y\S. z \ y) \ z \ x))"

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

lemma ereal_complete_uminus_eq:
  fixes S :: "ereal set"
  shows "(\y\uminus`S. y \ x) \ (\z. (\y\uminus`S. y \ z) \ x \ z)
     ⟷ (∀y∈S. -x ≤ y) ∧ (∀z. (∀y∈S. z ≤ y) ⟶ z ≤ -x)"
  by simp (metis ereal_minus_le_minus ereal_uminus_uminus)

lemma ereal_complete_Inf:
  "\x. (\y\S::ereal set. x \ y) \ (\z. (\y\S. z \ y) \ z \ x)"
  using ereal_complete_Sup[of "uminus ` S"]
  unfolding ereal_complete_uminus_eq
  by auto

instance
proof
  show "Sup {} = (bot::ereal)"
    using ereal_bot by (auto simp: bot_ereal_def Sup_ereal_def)
  show "Inf {} = (top::ereal)"
    unfolding top_ereal_def Inf_ereal_def
    using ereal_infty_less_eq(1) ereal_less_eq(1) by blast
  show "\x::ereal. \A. x \ A \ Inf A \ x"
       "\A z. (\x::ereal. x \ A \ z \ x) \ z \ Inf A"
    by (auto intro: someI2_ex ereal_complete_Inf simp: Inf_ereal_def)
  show "\x::ereal. \A. x \ A \ x \ Sup A"
       "\A z. (\x::ereal. x \ A \ x \ z) \ Sup A \ z"
    by (auto intro: someI2_ex ereal_complete_Sup simp: Sup_ereal_def)
qed 

end

instance ereal :: complete_linorder ..

instance ereal :: linear_continuum
proof
  show "\a b::ereal. a \ b"
    using zero_neq_one by blast
qed

lemma min_PInf [simp]: "min (\::ereal) x = x"
  by (metis min_top top_ereal_def)

lemma min_PInf2 [simp]: "min x (\::ereal) = x"
  by (metis min_top2 top_ereal_def)

lemma max_PInf [simp]: "max (\::ereal) x = \"
  by (metis max_top top_ereal_def)

lemma max_PInf2 [simp]: "max x (\::ereal) = \"
  by (metis max_top2 top_ereal_def)

lemma min_MInf [simp]: "min (-\::ereal) x = -\"
  by (metis min_bot bot_ereal_def)

lemma min_MInf2 [simp]: "min x (-\::ereal) = -\"
  by (metis min_bot2 bot_ereal_def)

lemma max_MInf [simp]: "max (-\::ereal) x = x"
  by (metis max_bot bot_ereal_def)

lemma max_MInf2 [simp]: "max x (-\::ereal) = x"
  by (metis max_bot2 bot_ereal_def)

subsection ‹Extended real intervals›

lemma real_greaterThanLessThan_infinity_eq:
  "real_of_ereal ` {N::ereal<..<\} =
    (if N = ∞ then {} else if N = -∞ then UNIV else {real_of_ereal N<..})"
  by (force simp: real_less_ereal_iff intro!: image_eqI[where x="ereal _"] elim!: less_ereal.elims)

lemma real_greaterThanLessThan_minus_infinity_eq:
  "real_of_ereal ` {-\<..
    (if N = ∞ then UNIV else if N = -∞ then {} else {..<real_of_ereal N})"
proof -
  have "real_of_ereal ` {-\<..}"
    by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
  also note real_greaterThanLessThan_infinity_eq
  finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
qed

lemma real_greaterThanLessThan_inter:
  "real_of_ereal ` {N<..<.. real_of_ereal ` {N<..<\}"
  by (force elim!: less_ereal.elims)

lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..
   (if N = ∞ then {} else
   if N = -∞ then
    (if M = ∞ then UNIV
    else if M = -∞ then {}
    else {..< real_of_ereal M})
  else if M = -∞ then {}
  else if M = ∞ then {real_of_ereal N<..}
  else {real_of_ereal N <..< real_of_ereal M})"
proof (cases "M = -\ \ M = \ \ N = -\ \ N = \")
  case True
  then show ?thesis
    by (auto simp: real_greaterThanLessThan_minus_infinity_eq real_greaterThanLessThan_infinity_eq )
next
  case False
  then obtain p q where "M = ereal p" "N = ereal q"
    by (metis MInfty_eq_minfinity ereal.distinct(3) uminus_ereal.elims)
  moreover have "\x. \q < x; x < p\ \ x \ real_of_ereal ` {ereal q<..
    by (metis greaterThanLessThan_iff imageI less_ereal.simps(1) real_of_ereal.simps(1))
  ultimately show ?thesis
    by (auto elim!: less_ereal.elims)
qed

lemma real_image_ereal_ivl:
  fixes a b::ereal
  shows
  "real_of_ereal ` {a<..
  (if a < b then (if a = -∞ then if b = ∞ then UNIV else {..<real_of_ereal b}
  else if b = ∞ then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
  by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)

lemma fixes a b c::ereal
  shows not_inftyI: "a < b \ b < c \ abs b \ \"
  by force

context
  fixes r s t::real
begin

--> --------------------

--> maximum size reached

--> --------------------