Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lizenz.pas.~25~ Sprache: Isabelle

Original von: 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 \<open>Extended real number line\<close>

theory Extended_Real
imports Complex_Main Extended_Nat Liminf_Limsup
begin

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

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 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 \\<^sub>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 \<open>
  For more lemmas about the extended real numbers see
  \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>.
\<close>

subsection \<open>Definition and basic properties\<close>

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 (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real_of_ereal a + real_of_ereal b else 0)"
  by (cases rule: ereal2_cases[of a b]) auto

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

instantiation ereal :: linorder
begin

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

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

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

lemma ereal_infty_less_eq[simp]:
  fixes x :: ereal
  shows "\ \ x \ x = \"
    and "x \ -\ \ x = -\"
  by (auto simp add: less_eq_ereal_def)

lemma ereal_less[simp]:
  "ereal r < 0 \ (r < 0)"
  "0 < ereal r \ (0 < r)"
  "ereal r < 1 \ (r < 1)"
  "1 < ereal r \ (1 < r)"
  "0 < (\::ereal)"
  "-(\::ereal) < 0"
  by (simp_all add: zero_ereal_def one_ereal_def)

lemma ereal_less_eq[simp]:
  "x \ (\::ereal)"
  "-(\::ereal) \ x"
  "ereal r \ ereal p \ r \ p"
  "ereal r \ 0 \ r \ 0"
  "0 \ ereal r \ 0 \ r"
  "ereal r \ 1 \ r \ 1"
  "1 \ ereal r \ 1 \ r"
  by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def)

lemma ereal_infty_less_eq2:
  "a \ b \ a = \ \ b = (\::ereal)"
  "a \ b \ b = -\ \ a = -(\::ereal)"
  by simp_all

instance
proof
  fix x y z :: ereal
  show "x \ x"
    by (cases x) simp_all
  show "x < y \ x \ y \ \ y \ x"
    by (cases rule: ereal2_cases[of x y]) auto
  show "x \ y \ y \ x "
    by (cases rule: ereal2_cases[of x y]) auto
  {
    assume "x \ y" "y \ x"
    then show "x = y"
      by (cases rule: ereal2_cases[of x y]) auto
  }
  {
    assume "x \ y" "y \ z"
    then show "x \ z"
      by (cases rule: ereal3_cases[of x y z]) auto
  }
qed

end

lemma ereal_dense2: "x < y \ \z. x < ereal z \ ereal z < y"
  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto

instance ereal :: dense_linorder
  by standard (blast dest: ereal_dense2)

instance ereal :: ordered_comm_monoid_add
proof
  fix a b c :: ereal
  assume "a \ b"
  then show "c + a \ c + b"
    by (cases rule: ereal3_cases[of a b c]) auto
qed

lemma ereal_one_not_less_zero_ereal[simp]: "\ 1 < (0::ereal)"
  by (simp add: zero_ereal_def)

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

lemma ereal_MInfty_lessI[intro, simp]:
  fixes a :: ereal
  shows "a \ -\ \ -\ < a"
  by (cases a) auto

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

lemma ereal_less_ereal_Ex:
  fixes a b :: ereal
  shows "x < ereal r \ x = -\ \ (\p. p < r \ x = ereal p)"
  by (cases x) auto

lemma less_PInf_Ex_of_nat: "x \ \ \ (\n::nat. x < ereal (real n))"
proof (cases x)
  case (real r)
  then show ?thesis
    using reals_Archimedean2[of r] by simp
qed simp_all

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 \<open>
  To help with inferences like \<^prop>\<open>a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y\<close>,
  where x and y are real.
\<close>

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]: "(\x\A. ereal (f x)) = ereal (\x\A. f x)"
proof (cases "finite A")
  case True
  then show ?thesis by induct auto
next
  case False
  then show ?thesis by simp
qed

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

lemma sum_Pinfty:
  fixes f :: "'a \ ereal"
  shows "(\x\P. f x) = \ \ finite P \ (\i\P. f i = \)"
proof safe
  assume *: "sum f P = \"
  show "finite P"
  proof (rule ccontr)
    assume "\ finite P"
    with * show False
      by auto
  qed
  show "\i\P. f i = \"
  proof (rule ccontr)
    assume "\ ?thesis"
    then have "\i. i \ P \ f i \ \"
      by auto
    with \<open>finite P\<close> have "sum f P \<noteq> \<infinity>"
      by induct auto
    with * show False
      by auto
  qed
next
  fix i
  assume "finite P" and "i \ P" and "f i = \"
  then show "sum f P = \"
  proof induct
    case (insert x A)
    show ?case using insert by (cases "x = i") auto
  qed simp
qed

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

lemma sum_real_of_ereal:
  fixes f :: "'i \ ereal"
  assumes "\x. x \ S \ \f x\ \ \"
  shows "(\x\S. real_of_ereal (f x)) = real_of_ereal (sum f S)"
proof -
  have "\x\S. \r. f x = ereal r"
  proof
    fix x
    assume "x \ S"
    from assms[OF this] show "\r. f x = ereal r"
      by (cases "f x") auto
  qed
  from bchoice[OF this] obtain r where "\x\S. f x = ereal (r x)" ..
  then show ?thesis
    by simp
qed

lemma sum_ereal_0:
  fixes f :: "'a \ ereal"
  assumes "finite A"
    and "\i. i \ A \ 0 \ f i"
  shows "(\x\A. f x) = 0 \ (\i\A. f i = 0)"
proof
  assume "sum f A = 0" with assms show "\i\A. f i = 0"
  proof (induction A)
    case (insert a A)
    then have "f a = 0 \ (\a\A. f a) = 0"
      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 = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
  by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_eq_MInfty[simp]:
  "a * b = -(\::ereal) \
    (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
  by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_abs_mult: "\x * y :: ereal\ = \x\ * \y\"
  by (cases x y rule: ereal2_cases) (auto simp: abs_mult)

lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
  by (simp_all add: zero_ereal_def one_ereal_def)

lemma ereal_mult_minus_left[simp]:
  fixes a b :: ereal
  shows "-a * b = - (a * b)"
  by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_minus_right[simp]:
  fixes a b :: ereal
  shows "a * -b = - (a * b)"
  by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_mult_infty[simp]:
  "a * (\::ereal) = (if a = 0 then 0 else if 0 < a then \ else - \)"
  by (cases a) auto

lemma ereal_infty_mult[simp]:
  "(\::ereal) * a = (if a = 0 then 0 else if 0 < a then \ else - \)"
  by (cases a) auto

lemma ereal_mult_strict_right_mono:
  assumes "a < b"
    and "0 < c"
    and "c < (\::ereal)"
  shows "a * c < b * c"
  using assms
  by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff)

lemma ereal_mult_strict_left_mono:
  "a < b \ 0 < c \ c < (\::ereal) \ c * a < c * b"
  using ereal_mult_strict_right_mono
  by (simp add: mult.commute[of c])

lemma ereal_mult_right_mono:
  fixes a b c :: ereal
  assumes "a \ b" "0 \ c"
  shows "a * c \ b * c"
proof (cases "c = 0")
  case False
  with assms show ?thesis
    by (cases rule: ereal3_cases[of a b c]) auto
qed auto

lemma ereal_mult_left_mono:
  fixes a b c :: ereal
  shows "a \ b \ 0 \ c \ c * a \ c * b"
  using ereal_mult_right_mono
  by (simp add: mult.commute[of c])

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

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

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

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

lemma zero_less_one_ereal[simp]: "0 \ (1::ereal)"
  by (simp add: one_ereal_def zero_ereal_def)

lemma ereal_0_le_mult[simp]: "0 \ a \ 0 \ b \ 0 \ a * (b :: ereal)"
  by (cases rule: ereal2_cases[of a b]) auto

lemma ereal_right_distrib:
  fixes r a b :: ereal
  shows "0 \ a \ 0 \ b \ r * (a + b) = r * a + r * b"
  by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)

lemma ereal_left_distrib:
  fixes r a b :: ereal
  shows "0 \ a \ 0 \ b \ (a + b) * r = a * r + b * r"
  by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)

lemma ereal_mult_le_0_iff:
  fixes a b :: ereal
  shows "a * b \ 0 \ (0 \ a \ b \ 0) \ (a \ 0 \ 0 \ b)"
  by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff)

lemma ereal_zero_le_0_iff:
  fixes a b :: ereal
  shows "0 \ a * b \ (0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0)"
  by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff)

lemma ereal_mult_less_0_iff:
  fixes a b :: ereal
  shows "a * b < 0 \ (0 < a \ b < 0) \ (a < 0 \ 0 < b)"
  by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff)

lemma ereal_zero_less_0_iff:
  fixes a b :: ereal
  shows "0 < a * b \ (0 < a \ 0 < b) \ (a < 0 \ b < 0)"
  by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)

lemma ereal_left_mult_cong:
  fixes a b c :: ereal
  shows  "c = d \ (d \ 0 \ a = b) \ a * c = b * d"
  by (cases "c = 0") simp_all

lemma ereal_right_mult_cong:
  fixes a b c :: ereal
  shows "c = d \ (d \ 0 \ a = b) \ c * a = d * b"
  by (cases "c = 0") simp_all

lemma ereal_distrib:
  fixes a b c :: ereal
  assumes "a \ \ \ b \ -\"
    and "a \ -\ \ b \ \"
    and "\c\ \ \"
  shows "(a + b) * c = a * c + b * c"
  using assms
  by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
proof (induct w rule: num_induct)
  case One
  then show ?case
    by simp
next
  case (inc x)
  then show ?case
    by (simp add: inc numeral_inc)
qed

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

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

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

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

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

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

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

lemma prod_ereal_0:
  fixes f :: "'a \ ereal"
  shows "(\i\A. f i) = 0 \ finite A \ (\i\A. f i = 0)"
proof (cases "finite A")
  case True
  then show ?thesis by (induct A) auto
qed auto

lemma prod_ereal_pos:
  fixes f :: "'a \ ereal"
  assumes pos: "\i. i \ I \ 0 \ f i"
  shows "0 \ (\i\I. f i)"
proof (cases "finite I")
  case True
  from this pos show ?thesis
    by induct auto
qed auto

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

lemma prod_ereal: "(\i\A. ereal (f i)) = ereal (prod f A)"
proof (cases "finite A")
  case True
  then show ?thesis
    by induct (auto simp: one_ereal_def)
next
  case False
  then show ?thesis
    by (simp add: one_ereal_def)
qed

subsubsection \<open>Power\<close>

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 \<open>Subtraction\<close>

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 ` {..
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 \
    (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and>
    (y = -\<infinity> \<longrightarrow> x = \<infinity>) \<and>
    (y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and>
    (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>)"
  by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_eq_minus:
  fixes x y z :: ereal
  shows "\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 = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and>
    (y = -\<infinity> \<longrightarrow> x \<noteq> \<infinity>) \<and>
    (\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)"
  by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_less_minus:
  fixes x y z :: ereal
  shows "\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 = -\<infinity> \<longrightarrow> z = \<infinity>) \<and>
    (y = \<infinity> \<longrightarrow> x = \<infinity> \<longrightarrow> z = \<infinity>) \<and>
    (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)"
  by (cases rule: ereal3_cases[of x y z]) auto

lemma ereal_minus_le:
  fixes x y z :: ereal
  shows "\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 \<or> a = \<infinity> \<or> (a = -\<infinity> \<and> b \<noteq> -\<infinity> \<and> c \<noteq> -\<infinity>)"
  by (cases rule: ereal3_cases[of a b c]) auto

lemma ereal_add_le_add_iff:
  fixes a b c :: ereal
  shows "c + a \ c + b \
    a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
  by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

lemma ereal_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 \<open>Division\<close>

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"
  using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_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"
    and "0 < a"
    and "a < \"
  shows "b < c"
  using assms
  by (cases rule: ereal3_cases[of a b c])
     (auto split: if_split_asm simp: zero_less_mult_iff zero_le_mult_iff)

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 (real r)
  note r = this
  show "x \ y"
  proof (cases y)
    case (real p)
    note p = this
    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 (insert y, 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"
  by (cases a) (auto simp: zero_ereal_def)

lemma ereal_times_divide_eq_left[simp]:
  fixes a b c :: ereal
  shows "b / c * a = b * a / c"
  by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff mult_less_0_iff)

lemma ereal_times_divide_eq: "a * (b / c :: ereal) = a * b / c"
  by (cases a b c rule: ereal3_cases)
     (auto simp: field_simps zero_less_mult_iff)

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"
using assms
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

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
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

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"
using assms
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)

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 \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
      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 \<open>\<infinity> \<notin> S\<close> show "y \<le> ereal s"
        by (cases y) auto
    next
      fix z
      assume "\y\S. y \ z"
      with \<open>S \<noteq> {-\<infinity>} \<and> S \<noteq> {}\<close> show "ereal s \<le> 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 _ \<infinity>] 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)
     \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -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
qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
  simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)

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 \<open>Extended real intervals\<close>

lemma real_greaterThanLessThan_infinity_eq:
  "real_of_ereal ` {N::ereal<..<\} =
    (if N = \<infinity> then {} else if N = -\<infinity> 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 = \<infinity> then UNIV else if N = -\<infinity> 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 = \<infinity> then {} else
   if N = -\<infinity> then
    (if M = \<infinity> then UNIV
    else if M = -\<infinity> then {}
    else {..< real_of_ereal M})
  else if M = - \<infinity> then {}
  else if M = \<infinity> 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<..
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.65 Sekunden (vorverarbeitet) ¤

vermutete Sprache: Sekunden
vermutete Sprache: sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.