Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
JPackageCommand.java
Sprache: Unknown
(* 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.679 Sekunden
(vorverarbeitet)
]
|
|
