author  wenzelm 
Thu, 22 Mar 2012 16:44:19 +0100  
changeset 47082  737d7bc8e50f 
parent 45934  9321cd2572fe 
child 47108  2a1953f0d20d 
permissions  rwrr 
43920  1 
(* Title: HOL/Library/Extended_Real.thy 
41983  2 
Author: Johannes Hölzl, TU München 
3 
Author: Robert Himmelmann, TU München 

4 
Author: Armin Heller, TU München 

5 
Author: Bogdan Grechuk, University of Edinburgh 

6 
*) 

41973  7 

8 
header {* Extended real number line *} 

9 

43920  10 
theory Extended_Real 
43941  11 
imports Complex_Main Extended_Nat 
41973  12 
begin 
13 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

14 
text {* 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

15 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

16 
For more lemmas about the extended real numbers go to 
47082  17 
@{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

18 

28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

19 
*} 
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

20 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

21 
lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

22 
proof 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

23 
assume "{x..} = UNIV" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

24 
show "x = bot" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

25 
proof (rule ccontr) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

26 
assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

27 
then show False using `{x..} = UNIV` by simp 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

28 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

29 
qed auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

30 

b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

31 
lemma SUPR_pair: 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

32 
"(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

33 
by (rule antisym) (auto intro!: SUP_least SUP_upper2) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

34 

b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

35 
lemma INFI_pair: 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

36 
"(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

37 
by (rule antisym) (auto intro!: INF_greatest INF_lower2) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

38 

41973  39 
subsection {* Definition and basic properties *} 
40 

43920  41 
datatype ereal = ereal real  PInfty  MInfty 
41973  42 

43920  43 
instantiation ereal :: uminus 
41973  44 
begin 
43920  45 
fun uminus_ereal where 
46 
" (ereal r) = ereal ( r)" 

43923  47 
 " PInfty = MInfty" 
48 
 " MInfty = PInfty" 

41973  49 
instance .. 
50 
end 

51 

43923  52 
instantiation ereal :: infinity 
53 
begin 

54 
definition "(\<infinity>::ereal) = PInfty" 

55 
instance .. 

56 
end 

41973  57 

43923  58 
declare [[coercion "ereal :: real \<Rightarrow> ereal"]] 
41973  59 

43920  60 
lemma ereal_uminus_uminus[simp]: 
61 
fixes a :: ereal shows " ( a) = a" 

41973  62 
by (cases a) simp_all 
63 

43923  64 
lemma 
65 
shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>" 

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

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

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

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

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

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

72 
by (simp_all add: infinity_ereal_def) 

41973  73 

43933  74 
declare 
75 
PInfty_eq_infinity[code_post] 

76 
MInfty_eq_minfinity[code_post] 

77 

78 
lemma [code_unfold]: 

79 
"\<infinity> = PInfty" 

80 
"PInfty = MInfty" 

81 
by simp_all 

82 

43923  83 
lemma inj_ereal[simp]: "inj_on ereal A" 
84 
unfolding inj_on_def by auto 

41973  85 

43920  86 
lemma ereal_cases[case_names real PInf MInf, cases type: ereal]: 
87 
assumes "\<And>r. x = ereal r \<Longrightarrow> P" 

41973  88 
assumes "x = \<infinity> \<Longrightarrow> P" 
89 
assumes "x = \<infinity> \<Longrightarrow> P" 

90 
shows P 

91 
using assms by (cases x) auto 

92 

43920  93 
lemmas ereal2_cases = ereal_cases[case_product ereal_cases] 
94 
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases] 

41973  95 

43920  96 
lemma ereal_uminus_eq_iff[simp]: 
97 
fixes a b :: ereal shows "a = b \<longleftrightarrow> a = b" 

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

41973  99 

43920  100 
function of_ereal :: "ereal \<Rightarrow> real" where 
101 
"of_ereal (ereal r) = r"  

102 
"of_ereal \<infinity> = 0"  

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

104 
by (auto intro: ereal_cases) 

41973  105 
termination proof qed (rule wf_empty) 
106 

107 
defs (overloaded) 

43920  108 
real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal" 
41973  109 

43920  110 
lemma real_of_ereal[simp]: 
111 
"real ( x :: ereal) =  (real x)" 

112 
"real (ereal r) = r" 

43923  113 
"real (\<infinity>::ereal) = 0" 
43920  114 
by (cases x) (simp_all add: real_of_ereal_def) 
41973  115 

43920  116 
lemma range_ereal[simp]: "range ereal = UNIV  {\<infinity>, \<infinity>}" 
41973  117 
proof safe 
43920  118 
fix x assume "x \<notin> range ereal" "x \<noteq> \<infinity>" 
41973  119 
then show "x = \<infinity>" by (cases x) auto 
120 
qed auto 

121 

43920  122 
lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

123 
proof safe 
43920  124 
fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "x"]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

125 
qed auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

126 

43920  127 
instantiation ereal :: number 
41973  128 
begin 
43920  129 
definition [simp]: "number_of x = ereal (number_of x)" 
47082  130 
instance .. 
41973  131 
end 
132 

43920  133 
instantiation ereal :: abs 
41976  134 
begin 
43920  135 
function abs_ereal where 
136 
"\<bar>ereal r\<bar> = ereal \<bar>r\<bar>" 

43923  137 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 
138 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 

43920  139 
by (auto intro: ereal_cases) 
41976  140 
termination proof qed (rule wf_empty) 
141 
instance .. 

142 
end 

143 

43923  144 
lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = \<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 
41976  145 
by (cases x) auto 
146 

43923  147 
lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 
41976  148 
by (cases x) auto 
149 

43920  150 
lemma abs_ereal_uminus[simp]: "\<bar> x\<bar> = \<bar>x::ereal\<bar>" 
41976  151 
by (cases x) auto 
152 

41973  153 
subsubsection "Addition" 
154 

43920  155 
instantiation ereal :: comm_monoid_add 
41973  156 
begin 
157 

43920  158 
definition "0 = ereal 0" 
41973  159 

43920  160 
function plus_ereal where 
161 
"ereal r + ereal p = ereal (r + p)"  

43923  162 
"\<infinity> + a = (\<infinity>::ereal)"  
163 
"a + \<infinity> = (\<infinity>::ereal)"  

43920  164 
"ereal r + \<infinity> =  \<infinity>"  
43923  165 
"\<infinity> + ereal p = (\<infinity>::ereal)"  
166 
"\<infinity> + \<infinity> = (\<infinity>::ereal)" 

41973  167 
proof  
168 
case (goal1 P x) 

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

170 
ultimately show P 

43920  171 
by (cases rule: ereal2_cases[of a b]) auto 
41973  172 
qed auto 
173 
termination proof qed (rule wf_empty) 

174 

175 
lemma Infty_neq_0[simp]: 

43923  176 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 
177 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 

43920  178 
by (simp_all add: zero_ereal_def) 
41973  179 

43920  180 
lemma ereal_eq_0[simp]: 
181 
"ereal r = 0 \<longleftrightarrow> r = 0" 

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

183 
unfolding zero_ereal_def by simp_all 

41973  184 

185 
instance 

186 
proof 

47082  187 
fix a b c :: ereal 
188 
show "0 + a = a" 

43920  189 
by (cases a) (simp_all add: zero_ereal_def) 
47082  190 
show "a + b = b + a" 
43920  191 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  192 
show "a + b + c = a + (b + c)" 
43920  193 
by (cases rule: ereal3_cases[of a b c]) simp_all 
41973  194 
qed 
195 
end 

196 

43920  197 
lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" 
198 
unfolding real_of_ereal_def zero_ereal_def by simp 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

199 

43920  200 
lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)" 
201 
unfolding zero_ereal_def abs_ereal.simps by simp 

41976  202 

43920  203 
lemma ereal_uminus_zero[simp]: 
204 
" 0 = (0::ereal)" 

205 
by (simp add: zero_ereal_def) 

41973  206 

43920  207 
lemma ereal_uminus_zero_iff[simp]: 
208 
fixes a :: ereal shows "a = 0 \<longleftrightarrow> a = 0" 

41973  209 
by (cases a) simp_all 
210 

43920  211 
lemma ereal_plus_eq_PInfty[simp]: 
43923  212 
fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>" 
43920  213 
by (cases rule: ereal2_cases[of a b]) auto 
41973  214 

43920  215 
lemma ereal_plus_eq_MInfty[simp]: 
43923  216 
fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> 
41973  217 
(a = \<infinity> \<or> b = \<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>" 
43920  218 
by (cases rule: ereal2_cases[of a b]) auto 
41973  219 

43920  220 
lemma ereal_add_cancel_left: 
43923  221 
fixes a b :: ereal assumes "a \<noteq> \<infinity>" 
41973  222 
shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)" 
43920  223 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  224 

43920  225 
lemma ereal_add_cancel_right: 
43923  226 
fixes a b :: ereal assumes "a \<noteq> \<infinity>" 
41973  227 
shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)" 
43920  228 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  229 

43920  230 
lemma ereal_real: 
231 
"ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)" 

41973  232 
by (cases x) simp_all 
233 

43920  234 
lemma real_of_ereal_add: 
235 
fixes a b :: ereal 

47082  236 
shows "real (a + b) = 
237 
(if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)" 

43920  238 
by (cases rule: ereal2_cases[of a b]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

239 

43920  240 
subsubsection "Linear order on @{typ ereal}" 
41973  241 

43920  242 
instantiation ereal :: linorder 
41973  243 
begin 
244 

47082  245 
function less_ereal 
246 
where 

247 
" ereal x < ereal y \<longleftrightarrow> x < y" 

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

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

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

251 
 " \<infinity> < ereal r \<longleftrightarrow> True" 

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

41973  253 
proof  
254 
case (goal1 P x) 

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

43920  256 
ultimately show P by (cases rule: ereal2_cases[of a b]) auto 
41973  257 
qed simp_all 
258 
termination by (relation "{}") simp 

259 

43920  260 
definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y" 
41973  261 

43920  262 
lemma ereal_infty_less[simp]: 
43923  263 
fixes x :: ereal 
264 
shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)" 

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

41973  266 
by (cases x, simp_all) (cases x, simp_all) 
267 

43920  268 
lemma ereal_infty_less_eq[simp]: 
43923  269 
fixes x :: ereal 
270 
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>" 

41973  271 
"x \<le> \<infinity> \<longleftrightarrow> x = \<infinity>" 
43920  272 
by (auto simp add: less_eq_ereal_def) 
41973  273 

43920  274 
lemma ereal_less[simp]: 
275 
"ereal r < 0 \<longleftrightarrow> (r < 0)" 

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

43923  277 
"0 < (\<infinity>::ereal)" 
278 
"(\<infinity>::ereal) < 0" 

43920  279 
by (simp_all add: zero_ereal_def) 
41973  280 

43920  281 
lemma ereal_less_eq[simp]: 
43923  282 
"x \<le> (\<infinity>::ereal)" 
283 
"(\<infinity>::ereal) \<le> x" 

43920  284 
"ereal r \<le> ereal p \<longleftrightarrow> r \<le> p" 
285 
"ereal r \<le> 0 \<longleftrightarrow> r \<le> 0" 

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

287 
by (auto simp add: less_eq_ereal_def zero_ereal_def) 

41973  288 

43920  289 
lemma ereal_infty_less_eq2: 
43923  290 
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)" 
291 
"a \<le> b \<Longrightarrow> b = \<infinity> \<Longrightarrow> a = (\<infinity>::ereal)" 

41973  292 
by simp_all 
293 

294 
instance 

295 
proof 

47082  296 
fix x y z :: ereal 
297 
show "x \<le> x" 

41973  298 
by (cases x) simp_all 
47082  299 
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 
43920  300 
by (cases rule: ereal2_cases[of x y]) auto 
41973  301 
show "x \<le> y \<or> y \<le> x " 
43920  302 
by (cases rule: ereal2_cases[of x y]) auto 
41973  303 
{ assume "x \<le> y" "y \<le> x" then show "x = y" 
43920  304 
by (cases rule: ereal2_cases[of x y]) auto } 
47082  305 
{ assume "x \<le> y" "y \<le> z" then show "x \<le> z" 
43920  306 
by (cases rule: ereal3_cases[of x y z]) auto } 
41973  307 
qed 
47082  308 

41973  309 
end 
310 

43920  311 
instance ereal :: ordered_ab_semigroup_add 
41978  312 
proof 
43920  313 
fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b" 
314 
by (cases rule: ereal3_cases[of a b c]) auto 

41978  315 
qed 
316 

43920  317 
lemma real_of_ereal_positive_mono: 
43923  318 
fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y" 
43920  319 
by (cases rule: ereal2_cases[of x y]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

320 

43920  321 
lemma ereal_MInfty_lessI[intro, simp]: 
43923  322 
fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> \<infinity> < a" 
41973  323 
by (cases a) auto 
324 

43920  325 
lemma ereal_less_PInfty[intro, simp]: 
43923  326 
fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>" 
41973  327 
by (cases a) auto 
328 

43920  329 
lemma ereal_less_ereal_Ex: 
330 
fixes a b :: ereal 

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

41973  332 
by (cases x) auto 
333 

43920  334 
lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

335 
proof (cases x) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

336 
case (real r) then show ?thesis 
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

337 
using reals_Archimedean2[of r] by simp 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

338 
qed simp_all 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

339 

43920  340 
lemma ereal_add_mono: 
341 
fixes a b c d :: ereal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d" 

41973  342 
using assms 
343 
apply (cases a) 

43920  344 
apply (cases rule: ereal3_cases[of b c d], auto) 
345 
apply (cases rule: ereal3_cases[of b c d], auto) 

41973  346 
done 
347 

43920  348 
lemma ereal_minus_le_minus[simp]: 
349 
fixes a b :: ereal shows " a \<le>  b \<longleftrightarrow> b \<le> a" 

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

41973  351 

43920  352 
lemma ereal_minus_less_minus[simp]: 
353 
fixes a b :: ereal shows " a <  b \<longleftrightarrow> b < a" 

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

41973  355 

43920  356 
lemma ereal_le_real_iff: 
357 
"x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))" 

41973  358 
by (cases y) auto 
359 

43920  360 
lemma real_le_ereal_iff: 
361 
"real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))" 

41973  362 
by (cases y) auto 
363 

43920  364 
lemma ereal_less_real_iff: 
365 
"x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))" 

41973  366 
by (cases y) auto 
367 

43920  368 
lemma real_less_ereal_iff: 
369 
"real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))" 

41973  370 
by (cases y) auto 
371 

43920  372 
lemma real_of_ereal_pos: 
373 
fixes x :: ereal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

374 

43920  375 
lemmas real_of_ereal_ord_simps = 
376 
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff 

41973  377 

43920  378 
lemma abs_ereal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: ereal\<bar> = x" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

379 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

380 

43920  381 
lemma abs_ereal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: ereal\<bar> = x" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

382 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

383 

43920  384 
lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

385 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

386 

43923  387 
lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)" 
388 
by (cases x) auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

389 

43923  390 
lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>" 
391 
by (cases x) auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

392 

43923  393 
lemma zero_less_real_of_ereal: 
394 
fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)" 

395 
by (cases x) auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

396 

43920  397 
lemma ereal_0_le_uminus_iff[simp]: 
398 
fixes a :: ereal shows "0 \<le> a \<longleftrightarrow> a \<le> 0" 

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

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

400 

43920  401 
lemma ereal_uminus_le_0_iff[simp]: 
402 
fixes a :: ereal shows "a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

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

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

404 

43923  405 
lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y" 
406 
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto 

407 

43920  408 
lemma ereal_dense: 
409 
fixes x y :: ereal assumes "x < y" 

43923  410 
shows "\<exists>z. x < z \<and> z < y" 
411 
using ereal_dense2[OF `x < y`] by blast 

41973  412 

43920  413 
lemma ereal_add_strict_mono: 
414 
fixes a b c d :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

415 
assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

416 
shows "a + c < b + d" 
43920  417 
using assms by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

418 

43923  419 
lemma ereal_less_add: 
420 
fixes a b c :: ereal shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b" 

43920  421 
by (cases rule: ereal2_cases[of b c]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

422 

43920  423 
lemma ereal_uminus_eq_reorder: " a = b \<longleftrightarrow> a = (b::ereal)" by auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

424 

43920  425 
lemma ereal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::ereal)" 
426 
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

427 

43920  428 
lemma ereal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::ereal)" 
429 
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

430 

43920  431 
lemmas ereal_uminus_reorder = 
432 
ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

433 

43920  434 
lemma ereal_bot: 
435 
fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x =  \<infinity>" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

436 
proof (cases x) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

437 
case (real r) with assms[of "r  1"] show ?thesis by auto 
47082  438 
next 
439 
case PInf with assms[of 0] show ?thesis by auto 

440 
next 

441 
case MInf then show ?thesis by simp 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

442 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

443 

43920  444 
lemma ereal_top: 
445 
fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

446 
proof (cases x) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

447 
case (real r) with assms[of "r + 1"] show ?thesis by auto 
47082  448 
next 
449 
case MInf with assms[of 0] show ?thesis by auto 

450 
next 

451 
case PInf then show ?thesis by simp 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

452 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

453 

b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

454 
lemma 
43920  455 
shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)" 
456 
and ereal_min[simp]: "ereal (min x y) = min (ereal x) (ereal y)" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

457 
by (simp_all add: min_def max_def) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

458 

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

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

461 

41978  462 
lemma 
43920  463 
fixes f :: "nat \<Rightarrow> ereal" 
41978  464 
shows incseq_uminus[simp]: "incseq (\<lambda>x.  f x) \<longleftrightarrow> decseq f" 
465 
and decseq_uminus[simp]: "decseq (\<lambda>x.  f x) \<longleftrightarrow> incseq f" 

466 
unfolding decseq_def incseq_def by auto 

467 

43920  468 
lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

469 
unfolding incseq_def by auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

470 

43920  471 
lemma ereal_add_nonneg_nonneg: 
472 
fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 

41978  473 
using add_mono[of 0 a 0 b] by simp 
474 

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

476 
by auto 

477 

478 
lemma incseq_setsumI: 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

479 
fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}" 
41978  480 
assumes "\<And>i. 0 \<le> f i" 
481 
shows "incseq (\<lambda>i. setsum f {..< i})" 

482 
proof (intro incseq_SucI) 

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

484 
using assms by (rule add_left_mono) 

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

486 
by auto 

487 
qed 

488 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

489 
lemma incseq_setsumI2: 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

490 
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

491 
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

492 
shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

493 
using assms unfolding incseq_def by (auto intro: setsum_mono) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

494 

41973  495 
subsubsection "Multiplication" 
496 

43920  497 
instantiation ereal :: "{comm_monoid_mult, sgn}" 
41973  498 
begin 
499 

43920  500 
definition "1 = ereal 1" 
41973  501 

43920  502 
function sgn_ereal where 
503 
"sgn (ereal r) = ereal (sgn r)" 

43923  504 
 "sgn (\<infinity>::ereal) = 1" 
505 
 "sgn (\<infinity>::ereal) = 1" 

43920  506 
by (auto intro: ereal_cases) 
41976  507 
termination proof qed (rule wf_empty) 
508 

43920  509 
function times_ereal where 
510 
"ereal r * ereal p = ereal (r * p)"  

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

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

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

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

43923  515 
"(\<infinity>::ereal) * \<infinity> = \<infinity>"  
516 
"(\<infinity>::ereal) * \<infinity> = \<infinity>"  

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

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

41973  519 
proof  
520 
case (goal1 P x) 

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

43920  522 
ultimately show P by (cases rule: ereal2_cases[of a b]) auto 
41973  523 
qed simp_all 
524 
termination by (relation "{}") simp 

525 

526 
instance 

527 
proof 

47082  528 
fix a b c :: ereal show "1 * a = a" 
43920  529 
by (cases a) (simp_all add: one_ereal_def) 
47082  530 
show "a * b = b * a" 
43920  531 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  532 
show "a * b * c = a * (b * c)" 
43920  533 
by (cases rule: ereal3_cases[of a b c]) 
534 
(simp_all add: zero_ereal_def zero_less_mult_iff) 

41973  535 
qed 
536 
end 

537 

43920  538 
lemma real_of_ereal_le_1: 
539 
fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1" 

540 
by (cases a) (auto simp: one_ereal_def) 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

541 

43920  542 
lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)" 
543 
unfolding one_ereal_def by simp 

41976  544 

43920  545 
lemma ereal_mult_zero[simp]: 
546 
fixes a :: ereal shows "a * 0 = 0" 

547 
by (cases a) (simp_all add: zero_ereal_def) 

41973  548 

43920  549 
lemma ereal_zero_mult[simp]: 
550 
fixes a :: ereal shows "0 * a = 0" 

551 
by (cases a) (simp_all add: zero_ereal_def) 

41973  552 

43920  553 
lemma ereal_m1_less_0[simp]: 
554 
"(1::ereal) < 0" 

555 
by (simp add: zero_ereal_def one_ereal_def) 

41973  556 

43920  557 
lemma ereal_zero_m1[simp]: 
558 
"1 \<noteq> (0::ereal)" 

559 
by (simp add: zero_ereal_def one_ereal_def) 

41973  560 

43920  561 
lemma ereal_times_0[simp]: 
562 
fixes x :: ereal shows "0 * x = 0" 

563 
by (cases x) (auto simp: zero_ereal_def) 

41973  564 

43920  565 
lemma ereal_times[simp]: 
43923  566 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 
567 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 

43920  568 
by (auto simp add: times_ereal_def one_ereal_def) 
41973  569 

43920  570 
lemma ereal_plus_1[simp]: 
571 
"1 + ereal r = ereal (r + 1)" "ereal r + 1 = ereal (r + 1)" 

43923  572 
"1 + (\<infinity>::ereal) = \<infinity>" "(\<infinity>::ereal) + 1 = \<infinity>" 
43920  573 
unfolding one_ereal_def by auto 
41973  574 

43920  575 
lemma ereal_zero_times[simp]: 
576 
fixes a b :: ereal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

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

41973  578 

43920  579 
lemma ereal_mult_eq_PInfty[simp]: 
43923  580 
shows "a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  581 
(a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>)" 
43920  582 
by (cases rule: ereal2_cases[of a b]) auto 
41973  583 

43920  584 
lemma ereal_mult_eq_MInfty[simp]: 
43923  585 
shows "a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  586 
(a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>)" 
43920  587 
by (cases rule: ereal2_cases[of a b]) auto 
41973  588 

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

41973  591 

43920  592 
lemma ereal_zero_one[simp]: "0 \<noteq> (1::ereal)" 
593 
by (simp_all add: zero_ereal_def one_ereal_def) 

41973  594 

43920  595 
lemma ereal_mult_minus_left[simp]: 
596 
fixes a b :: ereal shows "a * b =  (a * b)" 

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

41973  598 

43920  599 
lemma ereal_mult_minus_right[simp]: 
600 
fixes a b :: ereal shows "a * b =  (a * b)" 

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

41973  602 

43920  603 
lemma ereal_mult_infty[simp]: 
43923  604 
"a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  605 
by (cases a) auto 
606 

43920  607 
lemma ereal_infty_mult[simp]: 
43923  608 
"(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  609 
by (cases a) auto 
610 

43920  611 
lemma ereal_mult_strict_right_mono: 
43923  612 
assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)" 
41973  613 
shows "a * c < b * c" 
614 
using assms 

43920  615 
by (cases rule: ereal3_cases[of a b c]) 
44142  616 
(auto simp: zero_le_mult_iff) 
41973  617 

43920  618 
lemma ereal_mult_strict_left_mono: 
43923  619 
"\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b" 
43920  620 
using ereal_mult_strict_right_mono by (simp add: mult_commute[of c]) 
41973  621 

43920  622 
lemma ereal_mult_right_mono: 
623 
fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c" 

41973  624 
using assms 
625 
apply (cases "c = 0") apply simp 

43920  626 
by (cases rule: ereal3_cases[of a b c]) 
44142  627 
(auto simp: zero_le_mult_iff) 
41973  628 

43920  629 
lemma ereal_mult_left_mono: 
630 
fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b" 

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

41973  632 

43920  633 
lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)" 
634 
by (simp add: one_ereal_def zero_ereal_def) 

41978  635 

43920  636 
lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)" 
637 
by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

638 

43920  639 
lemma ereal_right_distrib: 
640 
fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b" 

641 
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

642 

43920  643 
lemma ereal_left_distrib: 
644 
fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r" 

645 
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

646 

43920  647 
lemma ereal_mult_le_0_iff: 
648 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

649 
shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)" 
43920  650 
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

651 

43920  652 
lemma ereal_zero_le_0_iff: 
653 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

654 
shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)" 
43920  655 
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

656 

43920  657 
lemma ereal_mult_less_0_iff: 
658 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

659 
shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)" 
43920  660 
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

661 

43920  662 
lemma ereal_zero_less_0_iff: 
663 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

664 
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)" 
43920  665 
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

666 

43920  667 
lemma ereal_distrib: 
668 
fixes a b c :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

669 
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

670 
shows "(a + b) * c = a * c + b * c" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

671 
using assms 
43920  672 
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

673 

43920  674 
lemma ereal_le_epsilon: 
675 
fixes x y :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

676 
assumes "ALL e. 0 < e > x <= y + e" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

677 
shows "x <= y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

678 
proof 
43920  679 
{ assume a: "EX r. y = ereal r" 
47082  680 
then obtain r where r_def: "y = ereal r" by auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

681 
{ assume "x=(\<infinity>)" hence ?thesis by auto } 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

682 
moreover 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

683 
{ assume "~(x=(\<infinity>))" 
47082  684 
then obtain p where p_def: "x = ereal p" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

685 
using a assms[rule_format, of 1] by (cases x) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

686 
{ fix e have "0 < e > p <= r + e" 
43920  687 
using assms[rule_format, of "ereal e"] p_def r_def by auto } 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

688 
hence "p <= r" apply (subst field_le_epsilon) by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

689 
hence ?thesis using r_def p_def by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

690 
} ultimately have ?thesis by blast 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

691 
} 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

692 
moreover 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

693 
{ assume "y=(\<infinity>)  y=\<infinity>" hence ?thesis 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

694 
using assms[rule_format, of 1] by (cases x) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

695 
} ultimately show ?thesis by (cases y) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

696 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

697 

b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

698 

43920  699 
lemma ereal_le_epsilon2: 
700 
fixes x y :: ereal 

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

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

702 
shows "x <= y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

703 
proof 
43920  704 
{ fix e :: ereal assume "e>0" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

705 
{ assume "e=\<infinity>" hence "x<=y+e" by auto } 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

706 
moreover 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

707 
{ assume "e~=\<infinity>" 
47082  708 
then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

709 
hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

710 
} ultimately have "x<=y+e" by blast 
47082  711 
} then show ?thesis using ereal_le_epsilon by auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

712 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

713 

43920  714 
lemma ereal_le_real: 
715 
fixes x y :: ereal 

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

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

717 
shows "y <= x" 
44142  718 
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

719 

43920  720 
lemma ereal_le_ereal: 
721 
fixes x y :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

722 
assumes "\<And>B. B < x \<Longrightarrow> B <= y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

723 
shows "x <= y" 
43920  724 
by (metis assms ereal_dense leD linorder_le_less_linear) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

725 

43920  726 
lemma ereal_ge_ereal: 
727 
fixes x y :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

728 
assumes "ALL B. B>x > B >= y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

729 
shows "x >= y" 
43920  730 
by (metis assms ereal_dense leD linorder_le_less_linear) 
41978  731 

43920  732 
lemma setprod_ereal_0: 
733 
fixes f :: "'a \<Rightarrow> ereal" 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

734 
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

735 
proof cases 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

736 
assume "finite A" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

737 
then show ?thesis by (induct A) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

738 
qed auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

739 

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

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

742 
proof cases 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

743 
assume "finite I" from this pos show ?thesis by induct auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

744 
qed simp 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

745 

6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

746 
lemma setprod_PInf: 
43923  747 
fixes f :: "'a \<Rightarrow> ereal" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

748 
assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

749 
shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

750 
proof cases 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

751 
assume "finite I" from this assms show ?thesis 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

752 
proof (induct I) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

753 
case (insert i I) 
43920  754 
then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_ereal_pos) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

755 
from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

756 
also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0" 
43920  757 
using setprod_ereal_pos[of I f] pos 
758 
by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

759 
also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)" 
43920  760 
using insert by (auto simp: setprod_ereal_0) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

761 
finally show ?case . 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

762 
qed simp 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

763 
qed simp 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

764 

43920  765 
lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

766 
proof cases 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

767 
assume "finite A" then show ?thesis 
43920  768 
by induct (auto simp: one_ereal_def) 
769 
qed (simp add: one_ereal_def) 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

770 

41978  771 
subsubsection {* Power *} 
772 

43920  773 
lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)" 
774 
by (induct n) (auto simp: one_ereal_def) 

41978  775 

43923  776 
lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)" 
43920  777 
by (induct n) (auto simp: one_ereal_def) 
41978  778 

43920  779 
lemma ereal_power_uminus[simp]: 
780 
fixes x :: ereal 

41978  781 
shows "( x) ^ n = (if even n then x ^ n else  (x^n))" 
43920  782 
by (induct n) (auto simp: one_ereal_def) 
41978  783 

43920  784 
lemma ereal_power_number_of[simp]: 
785 
"(number_of num :: ereal) ^ n = ereal (number_of num ^ n)" 

786 
by (induct n) (auto simp: one_ereal_def) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

787 

43920  788 
lemma zero_le_power_ereal[simp]: 
789 
fixes a :: ereal assumes "0 \<le> a" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

790 
shows "0 \<le> a ^ n" 
43920  791 
using assms by (induct n) (auto simp: ereal_zero_le_0_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

792 

41973  793 
subsubsection {* Subtraction *} 
794 

43920  795 
lemma ereal_minus_minus_image[simp]: 
796 
fixes S :: "ereal set" 

41973  797 
shows "uminus ` uminus ` S = S" 
798 
by (auto simp: image_iff) 

799 

43920  800 
lemma ereal_uminus_lessThan[simp]: 
801 
fixes a :: ereal shows "uminus ` {..<a} = {a<..}" 

47082  802 
proof  
803 
{ 

804 
fix x assume "a < x" 

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

806 
then have " x < a" by simp 

807 
} 

808 
then show ?thesis by (auto intro!: image_eqI) 

809 
qed 

41973  810 

43920  811 
lemma ereal_uminus_greaterThan[simp]: 
812 
"uminus ` {(a::ereal)<..} = {..<a}" 

813 
by (metis ereal_uminus_lessThan ereal_uminus_uminus 

814 
ereal_minus_minus_image) 

41973  815 

43920  816 
instantiation ereal :: minus 
41973  817 
begin 
43920  818 
definition "x  y = x + (y::ereal)" 
41973  819 
instance .. 
820 
end 

821 

43920  822 
lemma ereal_minus[simp]: 
823 
"ereal r  ereal p = ereal (r  p)" 

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

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

43923  826 
"(\<infinity>::ereal)  x = \<infinity>" 
827 
"(\<infinity>::ereal)  \<infinity> = \<infinity>" 

41973  828 
"x  y = x + y" 
829 
"x  0 = x" 

830 
"0  x = x" 

43920  831 
by (simp_all add: minus_ereal_def) 
41973  832 

43920  833 
lemma ereal_x_minus_x[simp]: 
43923  834 
"x  x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)" 
41973  835 
by (cases x) simp_all 
836 

43920  837 
lemma ereal_eq_minus_iff: 
838 
fixes x y z :: ereal 

41973  839 
shows "x = z  y \<longleftrightarrow> 
41976  840 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and> 
41973  841 
(y = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 
842 
(y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 

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

43920  844 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  845 

43920  846 
lemma ereal_eq_minus: 
847 
fixes x y z :: ereal 

41976  848 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x = z  y \<longleftrightarrow> x + y = z" 
43920  849 
by (auto simp: ereal_eq_minus_iff) 
41973  850 

43920  851 
lemma ereal_less_minus_iff: 
852 
fixes x y z :: ereal 

41973  853 
shows "x < z  y \<longleftrightarrow> 
854 
(y = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and> 

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

41976  856 
(\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)" 
43920  857 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  858 

43920  859 
lemma ereal_less_minus: 
860 
fixes x y z :: ereal 

41976  861 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x < z  y \<longleftrightarrow> x + y < z" 
43920  862 
by (auto simp: ereal_less_minus_iff) 
41973  863 

43920  864 
lemma ereal_le_minus_iff: 
865 
fixes x y z :: ereal 

41973  866 
shows "x \<le> z  y \<longleftrightarrow> 
867 
(y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = \<infinity>) \<and> 

41976  868 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)" 
43920  869 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  870 

43920  871 
lemma ereal_le_minus: 
872 
fixes x y z :: ereal 

41976  873 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x \<le> z  y \<longleftrightarrow> x + y \<le> z" 
43920  874 
by (auto simp: ereal_le_minus_iff) 
41973  875 

43920  876 
lemma ereal_minus_less_iff: 
877 
fixes x y z :: ereal 

41973  878 
shows "x  y < z \<longleftrightarrow> 
879 
y \<noteq> \<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> \<infinity>) \<and> 

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

43920  881 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  882 

43920  883 
lemma ereal_minus_less: 
884 
fixes x y z :: ereal 

41976  885 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x  y < z \<longleftrightarrow> x < z + y" 
43920  886 
by (auto simp: ereal_minus_less_iff) 
41973  887 

43920  888 
lemma ereal_minus_le_iff: 
889 
fixes x y z :: ereal 

41973  890 
shows "x  y \<le> z \<longleftrightarrow> 
891 
(y = \<infinity> \<longrightarrow> z = \<infinity>) \<and> 

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

41976  893 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)" 
43920  894 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  895 

43920  896 
lemma ereal_minus_le: 
897 
fixes x y z :: ereal 

41976  898 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x  y \<le> z \<longleftrightarrow> x \<le> z + y" 
43920  899 
by (auto simp: ereal_minus_le_iff) 
41973  900 

43920  901 
lemma ereal_minus_eq_minus_iff: 
902 
fixes a b c :: ereal 

41973  903 
shows "a  b = a  c \<longleftrightarrow> 
904 
b = c \<or> a = \<infinity> \<or> (a = \<infinity> \<and> b \<noteq> \<infinity> \<and> c \<noteq> \<infinity>)" 

43920  905 
by (cases rule: ereal3_cases[of a b c]) auto 
41973  906 

43920  907 
lemma ereal_add_le_add_iff: 
43923  908 
fixes a b c :: ereal 
909 
shows "c + a \<le> c + b \<longleftrightarrow> 

41973  910 
a \<le> b \<or> c = \<infinity> \<or> (c = \<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)" 
43920  911 
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) 
41973  912 

43920  913 
lemma ereal_mult_le_mult_iff: 
43923  914 
fixes a b c :: ereal 
915 
shows "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 

43920  916 
by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left) 
41973  917 

43920  918 
lemma ereal_minus_mono: 
919 
fixes A B C D :: ereal assumes "A \<le> B" "D \<le> C" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

920 
shows "A  C \<le> B  D" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

921 
using assms 
43920  922 
by (cases rule: ereal3_cases[case_product ereal_cases, of A B C D]) simp_all 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

923 

43920  924 
lemma real_of_ereal_minus: 
43923  925 
fixes a b :: ereal 
926 
shows "real (a  b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a  real b)" 

43920  927 
by (cases rule: ereal2_cases[of a b]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

928 

43920  929 
lemma ereal_diff_positive: 
930 
fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b  a" 

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

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

932 

43920  933 
lemma ereal_between: 
934 
fixes x e :: ereal 

41976  935 
assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e" 
41973  936 
shows "x  e < x" "x < x + e" 
937 
using assms apply (cases x, cases e) apply auto 

47082  938 
using assms apply (cases x, cases e) apply auto 
939 
done 

41973  940 

941 
subsubsection {* Division *} 

942 

43920  943 
instantiation ereal :: inverse 
41973  944 
begin 
945 

43920  946 
function inverse_ereal where 
947 
"inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))"  

43923  948 
"inverse (\<infinity>::ereal) = 0"  
949 
"inverse (\<infinity>::ereal) = 0" 

43920  950 
by (auto intro: ereal_cases) 
41973  951 
termination by (relation "{}") simp 
952 

43920  953 
definition "x / y = x * inverse (y :: ereal)" 
41973  954 

47082  955 
instance .. 
41973  956 
end 
957 

43920  958 
lemma real_of_ereal_inverse[simp]: 
959 
fixes a :: ereal 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

960 
shows "real (inverse a) = 1 / real a" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

961 
by (cases a) (auto simp: inverse_eq_divide) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

962 

43920  963 
lemma ereal_inverse[simp]: 
43923  964 
"inverse (0::ereal) = \<infinity>" 
43920  965 
"inverse (1::ereal) = 1" 
966 
by (simp_all add: one_ereal_def zero_ereal_def) 

41973  967 

43920  968 
lemma ereal_divide[simp]: 
969 
"ereal r / ereal p = (if p = 0 then ereal r * \<infinity> else ereal (r / p))" 

970 
unfolding divide_ereal_def by (auto simp: divide_real_def) 

41973  971 

43920  972 
lemma ereal_divide_same[simp]: 
43923  973 
fixes x :: ereal shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)" 
41973  974 
by (cases x) 
43920  975 
(simp_all add: divide_real_def divide_ereal_def one_ereal_def) 
41973  976 

43920  977 
lemma ereal_inv_inv[simp]: 
43923  978 
fixes x :: ereal shows "inverse (inverse x) = (if x \<noteq> \<infinity> then x else \<infinity>)" 
41973  979 
by (cases x) auto 
980 

43920  981 
lemma ereal_inverse_minus[simp]: 
43923  982 
fixes x :: ereal shows "inverse ( x) = (if x = 0 then \<infinity> else inverse x)" 
41973  983 
by (cases x) simp_all 
984 

43920  985 
lemma ereal_uminus_divide[simp]: 
986 
fixes x y :: ereal shows " x / y =  (x / y)" 

987 
unfolding divide_ereal_def by simp 

41973  988 

43920  989 
lemma ereal_divide_Infty[simp]: 
43923  990 
fixes x :: ereal shows "x / \<infinity> = 0" "x / \<infinity> = 0" 
43920  991 
unfolding divide_ereal_def by simp_all 
41973  992 

43920  993 
lemma ereal_divide_one[simp]: 
994 
"x / 1 = (x::ereal)" 

995 
unfolding divide_ereal_def by simp 

41973  996 

43920  997 
lemma ereal_divide_ereal[simp]: 
998 
"\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else \<infinity>)" 

999 
unfolding divide_ereal_def by simp 

41973  1000 

43920  1001 
lemma zero_le_divide_ereal[simp]: 
1002 
fixes a :: ereal assumes "0 \<le> a" "0 \<le> b" 

41978  1003 
shows "0 \<le> a / b" 
43920  1004 
using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff) 
41978  1005 

43920  1006 
lemma ereal_le_divide_pos: 
43923  1007 
fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z" 
43920  1008 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1009 

43920  1010 
lemma ereal_divide_le_pos: 
43923  1011 
fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y" 
43920  1012 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1013 

43920  1014 
lemma ereal_le_divide_neg: 
43923  1015 
fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y" 
43920  1016 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1017 

43920  1018 
lemma ereal_divide_le_neg: 
43923  1019 
fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z" 
43920  1020 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1021 

43920  1022 
lemma ereal_inverse_antimono_strict: 
1023 
fixes x y :: ereal 

41973  1024 
shows "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> inverse y < inverse x" 
43920  1025 
by (cases rule: ereal2_cases[of x y]) auto 
41973  1026 

43920  1027 
lemma ereal_inverse_antimono: 
1028 
fixes x y :: ereal 

41973  1029 
shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x" 
43920  1030 
by (cases rule: ereal2_cases[of x y]) auto 
41973  1031 

1032 
lemma inverse_inverse_Pinfty_iff[simp]: 

43923  1033 
fixes x :: ereal shows "inverse x = \<infinity> \<longleftrightarrow> x = 0" 
41973  1034 
by (cases x) auto 
1035 

43920  1036 
lemma ereal_inverse_eq_0: 
43923  1037 
fixes x :: ereal shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = \<infinity>" 
41973  1038 
by (cases x) auto 
1039 

43920  1040 
lemma ereal_0_gt_inverse: 
1041 
fixes x :: ereal shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1042 
by (cases x) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1043 

43920  1044 
lemma ereal_mult_less_right: 
43923  1045 
fixes a b c :: ereal 
41973  1046 
assumes "b * a < c * a" "0 < a" "a < \<infinity>" 
1047 
shows "b < c" 

1048 
using assms 

43920  1049 
by (cases rule: ereal3_cases[of a b c]) 
41973  1050 
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff) 
1051 

43920  1052 
lemma ereal_power_divide: 
43923  1053 
fixes x y :: ereal shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n" 
43920  1054 
by (cases rule: ereal2_cases[of x y]) 
1055 
(auto simp: one_ereal_def zero_ereal_def power_divide not_le 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1056 
power_less_zero_eq zero_le_power_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1057 

43920  1058 
lemma ereal_le_mult_one_interval: 
1059 
fixes x y :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1060 
assumes y: "y \<noteq> \<infinity>" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1061 
assumes z: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1062 
shows "x \<le> y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1063 
proof (cases x) 
43920  1064 
case PInf with z[of "1 / 2"] show "x \<le> y" by (simp add: one_ereal_def) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1065 
next 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1066 
case (real r) note r = this 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1067 
show "x \<le> y" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1068 
proof (cases y) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1069 
case (real p) note p = this 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1070 
have "r \<le> p" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1071 
proof (rule field_le_mult_one_interval) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1072 
fix z :: real assume "0 < z" and "z < 1" 
43920  1073 
with z[of "ereal z"] 
1074 
show "z * r \<le> p" using p r by (auto simp: zero_le_mult_iff one_ereal_def) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1075 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1076 
then show "x \<le> y" using p r by simp 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1077 
qed (insert y, simp_all) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1078 
qed simp 
41978  1079 

45934  1080 
lemma ereal_divide_right_mono[simp]: 
1081 
fixes x y z :: ereal 

1082 
assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z" 

1083 
using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono) 

1084 

1085 
lemma ereal_divide_left_mono[simp]: 

1086 
fixes x y z :: ereal 

1087 
assumes "y \<le> x" "0 < z" "0 < x * y" 

1088 
shows "z / x \<le> z / y" 

1089 
using assms by (cases x y z rule: ereal3_cases) 

1090 
(auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm) 

1091 

1092 
lemma ereal_divide_zero_left[simp]: 

1093 
fixes a :: ereal 

1094 
shows "0 / a = 0" 

1095 
by (cases a) (auto simp: zero_ereal_def) 

1096 

1097 
lemma ereal_times_divide_eq_left[simp]: 

1098 
fixes a b c :: ereal 

1099 
shows "b / c * a = b * a / c" 

1100 
by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps) 

1101 

41973  1102 
subsection "Complete lattice" 
1103 

43920  1104 
instantiation ereal :: lattice 
41973  1105 
begin 
43920  1106 
definition [simp]: "sup x y = (max x y :: ereal)" 
1107 
definition [simp]: "inf x y = (min x y :: ereal)" 

47082  1108 
instance by default simp_all 
41973  1109 
end 
1110 

43920  1111 
instantiation ereal :: complete_lattice 
41973  1112 
begin 
1113 

43923  1114 
definition "bot = (\<infinity>::ereal)" 
1115 
definition "top = (\<infinity>::ereal)" 

41973  1116 

43923  1117 
definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)" 
1118 
definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)" 

41973  1119 

43920  1120 
lemma ereal_complete_Sup: 
1121 
fixes S :: "ereal set" assumes "S \<noteq> {}" 

41973  1122 
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)" 
1123 
proof cases 

43920  1124 
assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x" 
1125 
then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y" by auto 

41973  1126 
then have "\<infinity> \<notin> S" by force 
1127 
show ?thesis 

1128 
proof cases 

1129 
assume "S = {\<infinity>}" 

1130 
then show ?thesis by (auto intro!: exI[of _ "\<infinity>"]) 

1131 
next 

1132 
assume "S \<noteq> {\<infinity>}" 

1133 
with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S  {\<infinity>}" "x \<noteq> \<infinity>" by auto 

1134 
with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S  {\<infinity>}). z \<le> y" 

43920  1135 
by (auto simp: real_of_ereal_ord_simps) 
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
44520
diff
changeset

1136 
with complete_real[of "real ` (S  {\<infinity>})"] `x \<in> S  {\<infinity>}` 
41973  1137 
obtain s where s: 
1138 
"\<forall>y\<in>S  {\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S  {\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z" 

1139 
by auto 

1140 
show ?thesis 

43920  1141 
proof (safe intro!: exI[of _ "ereal s"]) 
1142 
fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> ereal s" 

41973  1143 
proof (cases z) 
1144 
case (real r) 

1145 
then show ?thesis 

43920  1146 
using s(1)[rule_format, of z] `z \<in> S` `z = ereal r` by auto 
41973  1147 
qed auto 
1148 
next 

1149 
fix z assume *: "\<forall>y\<in>S. y \<le> z" 

43920  1150 
with `S \<noteq> {\<infinity>}` `S \<noteq> {}` show "ereal s \<le> z" 
41973  1151 
proof (cases z) 
1152 
case (real u) 

1153 
with * have "s \<le> u" 

43920  1154 
by (intro s(2)[of u]) (auto simp: real_of_ereal_ord_simps) 
41973  1155 
then show ?thesis using real by simp 
1156 
qed auto 

1157 
qed 

1158 
qed 

1159 
next 

43920  1160 
assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> ereal x)" 
41973  1161 
show ?thesis 
1162 
proof (safe intro!: exI[of _ \<infinity>]) 

1163 
fix y assume **: "\<forall>z\<in>S. z \<le> y" 

1164 
with * show "\<infinity> \<le> y" 

1165 
proof (cases y) 

1166 
case MInf with * ** show ?thesis by (force simp: not_le) 

1167 
qed auto 

1168 
qed simp 

1169 
qed 

1170 

43920  1171 
lemma ereal_complete_Inf: 
1172 
fixes S :: "ereal set" assumes "S ~= {}" 

41973  1173 
shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) > z <= x)" 
1174 
proof 

1175 
def S1 == "uminus ` S" 

1176 
hence "S1 ~= {}" using assms by auto 

47082  1177 
then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) > x <= z)" 
43920  1178 
using ereal_complete_Sup[of S1] by auto 
41973  1179 
{ fix z assume "ALL y:S. z <= y" 
1180 
hence "ALL y:S1. y <= z" unfolding S1_def by auto 

1181 
hence "x <= z" using x_def by auto 

1182 
hence "z <= x" 

43920  1183 
apply (subst ereal_uminus_uminus[symmetric]) 
1184 
unfolding ereal_minus_le_minus . } 

41973  1185 
moreover have "(ALL y:S. x <= y)" 
1186 
using x_def unfolding S1_def 

1187 
apply simp 

43920  1188 
apply (subst (3) ereal_uminus_uminus[symmetric]) 
1189 
unfolding ereal_minus_le_minus by simp 

41973  1190 
ultimately show ?thesis by auto 
1191 
qed 

1192 

43920  1193 
lemma ereal_complete_uminus_eq: 
1194 
fixes S :: "ereal set" 

41973  1195 
shows "(\<forall>y\<in>uminus`S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>uminus`S. y \<le> z) \<longrightarrow> x \<le> z) 
1196 
\<longleftrightarrow> (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)" 

43920  1197 
by simp (metis ereal_minus_le_minus ereal_uminus_uminus) 
41973  1198 

43920  1199 
lemma ereal_Sup_uminus_image_eq: 
1200 
fixes S :: "ereal set" 

41973  1201 
shows "Sup (uminus ` S) =  Inf S" 
1202 
proof cases 

1203 
assume "S = {}" 

43920  1204 
moreover have "(THE x. All (op \<le> x)) = (\<infinity>::ereal)" 
1205 
by (rule the_equality) (auto intro!: ereal_bot) 

1206 
moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::ereal)" 

1207 
by (rule some_equality) (auto intro!: ereal_top) 

1208 
ultimately show ?thesis unfolding Inf_ereal_def Sup_ereal_def 

41973  1209 
Least_def Greatest_def GreatestM_def by simp 
1210 
next 

1211 
assume "S \<noteq> {}" 

43920  1212 
with ereal_complete_Sup[of "uminus`S"] 
41973  1213 
obtain x where x: "(\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)" 
43920  1214 
unfolding ereal_complete_uminus_eq by auto 
41973  1215 
show "Sup (uminus ` S) =  Inf S" 
43920  1216 
unfolding Inf_ereal_def Greatest_def GreatestM_def 
41973  1217 
proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) =  x"]) 
1218 
show "(\<forall>y\<in>S. x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x)" 

1219 
using x . 

1220 
fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')" 

1221 
then have "(\<forall>y\<in>uminus`S. y \<le>  x') \<and> (\<forall>y. (\<forall>z\<in>uminus`S. z \<le> y) \<longrightarrow>  x' \<le> y)" 

43920  1222 
unfolding ereal_complete_uminus_eq by simp 
41973  1223 
then show "Sup (uminus ` S) = x'" 
43920  1224 
unfolding Sup_ereal_def ereal_uminus_eq_iff 
41973  1225 
by (intro Least_equality) auto 
1226 
qed 

1227 
qed 

1228 

1229 
instance 

1230 
proof 

43920  1231 
{ fix x :: ereal and A 
1232 
show "bot <= x" by (cases x) (simp_all add: bot_ereal_def) 

1233 
show "x <= top" by (simp add: top_ereal_def) } 

41973  1234 

43920  1235 
{ fix x :: ereal and A assume "x : A" 
1236 
with ereal_complete_Sup[of A] 

41973  1237 
obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto 
1238 
hence "x <= s" using `x : A` by auto 

43920  1239 
also have "... = Sup A" using s unfolding Sup_ereal_def 
41973  1240 
by (auto intro!: Least_equality[symmetric]) 
1241 
finally show "x <= Sup A" . } 

1242 
note le_Sup = this 

1243 

43920  1244 
{ fix x :: ereal and A assume *: "!!z. (z : A ==> z <= x)" 
41973  1245 
show "Sup A <= x" 
1246 
proof (cases "A = {}") 

1247 
case True 

43920  1248 
hence "Sup A = \<infinity>" unfolding Sup_ereal_def 
41973  1249 
by (auto intro!: Least_equality) 