author  wenzelm 
Wed, 25 Sep 2013 12:42:56 +0200  
changeset 53873  08594daabcd9 
parent 53381  355a4cac5440 
child 54408  67dec4ccaabd 
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 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
51329
diff
changeset

11 
imports Complex_Main Extended_Nat Liminf_Limsup 
41973  12 
begin 
13 

51022
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

14 
text {* 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

15 

78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

16 
For more lemmas about the extended real numbers go to 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

17 
@{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

18 

78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

19 
*} 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

20 

41973  21 
subsection {* Definition and basic properties *} 
22 

43920  23 
datatype ereal = ereal real  PInfty  MInfty 
41973  24 

43920  25 
instantiation ereal :: uminus 
41973  26 
begin 
53873  27 

28 
fun uminus_ereal where 

29 
" (ereal r) = ereal ( r)" 

30 
 " PInfty = MInfty" 

31 
 " MInfty = PInfty" 

32 

33 
instance .. 

34 

41973  35 
end 
36 

43923  37 
instantiation ereal :: infinity 
38 
begin 

53873  39 

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

41 
instance .. 

42 

43923  43 
end 
41973  44 

43923  45 
declare [[coercion "ereal :: real \<Rightarrow> ereal"]] 
41973  46 

43920  47 
lemma ereal_uminus_uminus[simp]: 
53873  48 
fixes a :: ereal 
49 
shows " ( a) = a" 

41973  50 
by (cases a) simp_all 
51 

43923  52 
lemma 
53 
shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>" 

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

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

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

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

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

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

60 
by (simp_all add: infinity_ereal_def) 

41973  61 

43933  62 
declare 
63 
PInfty_eq_infinity[code_post] 

64 
MInfty_eq_minfinity[code_post] 

65 

66 
lemma [code_unfold]: 

67 
"\<infinity> = PInfty" 

53873  68 
" PInfty = MInfty" 
43933  69 
by simp_all 
70 

43923  71 
lemma inj_ereal[simp]: "inj_on ereal A" 
72 
unfolding inj_on_def by auto 

41973  73 

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

41973  76 
assumes "x = \<infinity> \<Longrightarrow> P" 
77 
assumes "x = \<infinity> \<Longrightarrow> P" 

78 
shows P 

79 
using assms by (cases x) auto 

80 

43920  81 
lemmas ereal2_cases = ereal_cases[case_product ereal_cases] 
82 
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases] 

41973  83 

43920  84 
lemma ereal_uminus_eq_iff[simp]: 
53873  85 
fixes a b :: ereal 
86 
shows "a = b \<longleftrightarrow> a = b" 

43920  87 
by (cases rule: ereal2_cases[of a b]) simp_all 
41973  88 

43920  89 
function of_ereal :: "ereal \<Rightarrow> real" where 
53873  90 
"of_ereal (ereal r) = r" 
91 
 "of_ereal \<infinity> = 0" 

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

43920  93 
by (auto intro: ereal_cases) 
53873  94 
termination by default (rule wf_empty) 
41973  95 

96 
defs (overloaded) 

43920  97 
real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal" 
41973  98 

43920  99 
lemma real_of_ereal[simp]: 
53873  100 
"real ( x :: ereal) =  (real x)" 
101 
"real (ereal r) = r" 

102 
"real (\<infinity>::ereal) = 0" 

43920  103 
by (cases x) (simp_all add: real_of_ereal_def) 
41973  104 

43920  105 
lemma range_ereal[simp]: "range ereal = UNIV  {\<infinity>, \<infinity>}" 
41973  106 
proof safe 
53873  107 
fix x 
108 
assume "x \<notin> range ereal" "x \<noteq> \<infinity>" 

109 
then show "x = \<infinity>" 

110 
by (cases x) auto 

41973  111 
qed auto 
112 

43920  113 
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

114 
proof safe 
53873  115 
fix x :: ereal 
116 
show "x \<in> range uminus" 

117 
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

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

119 

43920  120 
instantiation ereal :: abs 
41976  121 
begin 
53873  122 

123 
function abs_ereal where 

124 
"\<bar>ereal r\<bar> = ereal \<bar>r\<bar>" 

125 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 

126 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 

127 
by (auto intro: ereal_cases) 

128 
termination proof qed (rule wf_empty) 

129 

130 
instance .. 

131 

41976  132 
end 
133 

53873  134 
lemma abs_eq_infinity_cases[elim!]: 
135 
fixes x :: ereal 

136 
assumes "\<bar>x\<bar> = \<infinity>" 

137 
obtains "x = \<infinity>"  "x = \<infinity>" 

138 
using assms by (cases x) auto 

41976  139 

53873  140 
lemma abs_neq_infinity_cases[elim!]: 
141 
fixes x :: ereal 

142 
assumes "\<bar>x\<bar> \<noteq> \<infinity>" 

143 
obtains r where "x = ereal r" 

144 
using assms by (cases x) auto 

145 

146 
lemma abs_ereal_uminus[simp]: 

147 
fixes x :: ereal 

148 
shows "\<bar> x\<bar> = \<bar>x\<bar>" 

41976  149 
by (cases x) auto 
150 

53873  151 
lemma ereal_infinity_cases: 
152 
fixes a :: ereal 

153 
shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>" 

154 
by auto 

41976  155 

50104  156 

41973  157 
subsubsection "Addition" 
158 

53873  159 
instantiation ereal :: "{one,comm_monoid_add}" 
41973  160 
begin 
161 

43920  162 
definition "0 = ereal 0" 
51351  163 
definition "1 = ereal 1" 
41973  164 

43920  165 
function plus_ereal where 
53873  166 
"ereal r + ereal p = ereal (r + p)" 
167 
 "\<infinity> + a = (\<infinity>::ereal)" 

168 
 "a + \<infinity> = (\<infinity>::ereal)" 

169 
 "ereal r + \<infinity> =  \<infinity>" 

170 
 "\<infinity> + ereal p = (\<infinity>::ereal)" 

171 
 "\<infinity> + \<infinity> = (\<infinity>::ereal)" 

41973  172 
proof  
173 
case (goal1 P x) 

53873  174 
then obtain a b where "x = (a, b)" 
175 
by (cases x) auto 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

176 
with goal1 show P 
43920  177 
by (cases rule: ereal2_cases[of a b]) auto 
41973  178 
qed auto 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

179 
termination by default (rule wf_empty) 
41973  180 

181 
lemma Infty_neq_0[simp]: 

43923  182 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 
183 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 

43920  184 
by (simp_all add: zero_ereal_def) 
41973  185 

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

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

189 
unfolding zero_ereal_def by simp_all 

41973  190 

191 
instance 

192 
proof 

47082  193 
fix a b c :: ereal 
194 
show "0 + a = a" 

43920  195 
by (cases a) (simp_all add: zero_ereal_def) 
47082  196 
show "a + b = b + a" 
43920  197 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  198 
show "a + b + c = a + (b + c)" 
43920  199 
by (cases rule: ereal3_cases[of a b c]) simp_all 
41973  200 
qed 
53873  201 

41973  202 
end 
203 

51351  204 
instance ereal :: numeral .. 
205 

43920  206 
lemma real_of_ereal_0[simp]: "real (0::ereal) = 0" 
207 
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

208 

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

41976  211 

53873  212 
lemma ereal_uminus_zero[simp]: " 0 = (0::ereal)" 
43920  213 
by (simp add: zero_ereal_def) 
41973  214 

43920  215 
lemma ereal_uminus_zero_iff[simp]: 
53873  216 
fixes a :: ereal 
217 
shows "a = 0 \<longleftrightarrow> a = 0" 

41973  218 
by (cases a) simp_all 
219 

43920  220 
lemma ereal_plus_eq_PInfty[simp]: 
53873  221 
fixes a b :: ereal 
222 
shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>" 

43920  223 
by (cases rule: ereal2_cases[of a b]) auto 
41973  224 

43920  225 
lemma ereal_plus_eq_MInfty[simp]: 
53873  226 
fixes a b :: ereal 
227 
shows "a + b = \<infinity> \<longleftrightarrow> (a = \<infinity> \<or> b = \<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>" 

43920  228 
by (cases rule: ereal2_cases[of a b]) auto 
41973  229 

43920  230 
lemma ereal_add_cancel_left: 
53873  231 
fixes a b :: ereal 
232 
assumes "a \<noteq> \<infinity>" 

233 
shows "a + b = a + c \<longleftrightarrow> a = \<infinity> \<or> b = c" 

43920  234 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  235 

43920  236 
lemma ereal_add_cancel_right: 
53873  237 
fixes a b :: ereal 
238 
assumes "a \<noteq> \<infinity>" 

239 
shows "b + a = c + a \<longleftrightarrow> a = \<infinity> \<or> b = c" 

43920  240 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  241 

53873  242 
lemma ereal_real: "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)" 
41973  243 
by (cases x) simp_all 
244 

43920  245 
lemma real_of_ereal_add: 
246 
fixes a b :: ereal 

47082  247 
shows "real (a + b) = 
248 
(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  249 
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

250 

53873  251 

43920  252 
subsubsection "Linear order on @{typ ereal}" 
41973  253 

43920  254 
instantiation ereal :: linorder 
41973  255 
begin 
256 

47082  257 
function less_ereal 
258 
where 

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

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

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

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

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

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

41973  265 
proof  
266 
case (goal1 P x) 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

267 
then obtain a b where "x = (a,b)" by (cases x) auto 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

268 
with goal1 show P by (cases rule: ereal2_cases[of a b]) auto 
41973  269 
qed simp_all 
270 
termination by (relation "{}") simp 

271 

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

43920  274 
lemma ereal_infty_less[simp]: 
43923  275 
fixes x :: ereal 
276 
shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)" 

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

41973  278 
by (cases x, simp_all) (cases x, simp_all) 
279 

43920  280 
lemma ereal_infty_less_eq[simp]: 
43923  281 
fixes x :: ereal 
282 
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>" 

53873  283 
and "x \<le> \<infinity> \<longleftrightarrow> x = \<infinity>" 
43920  284 
by (auto simp add: less_eq_ereal_def) 
41973  285 

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

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

43923  289 
"0 < (\<infinity>::ereal)" 
290 
"(\<infinity>::ereal) < 0" 

43920  291 
by (simp_all add: zero_ereal_def) 
41973  292 

43920  293 
lemma ereal_less_eq[simp]: 
43923  294 
"x \<le> (\<infinity>::ereal)" 
295 
"(\<infinity>::ereal) \<le> x" 

43920  296 
"ereal r \<le> ereal p \<longleftrightarrow> r \<le> p" 
297 
"ereal r \<le> 0 \<longleftrightarrow> r \<le> 0" 

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

299 
by (auto simp add: less_eq_ereal_def zero_ereal_def) 

41973  300 

43920  301 
lemma ereal_infty_less_eq2: 
43923  302 
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)" 
303 
"a \<le> b \<Longrightarrow> b = \<infinity> \<Longrightarrow> a = (\<infinity>::ereal)" 

41973  304 
by simp_all 
305 

306 
instance 

307 
proof 

47082  308 
fix x y z :: ereal 
309 
show "x \<le> x" 

41973  310 
by (cases x) simp_all 
47082  311 
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 
43920  312 
by (cases rule: ereal2_cases[of x y]) auto 
41973  313 
show "x \<le> y \<or> y \<le> x " 
43920  314 
by (cases rule: ereal2_cases[of x y]) auto 
53873  315 
{ 
316 
assume "x \<le> y" "y \<le> x" 

317 
then show "x = y" 

318 
by (cases rule: ereal2_cases[of x y]) auto 

319 
} 

320 
{ 

321 
assume "x \<le> y" "y \<le> z" 

322 
then show "x \<le> z" 

323 
by (cases rule: ereal3_cases[of x y z]) auto 

324 
} 

41973  325 
qed 
47082  326 

41973  327 
end 
328 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

329 
lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

330 
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

331 

53216  332 
instance ereal :: dense_linorder 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

333 
by default (blast dest: ereal_dense2) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

334 

43920  335 
instance ereal :: ordered_ab_semigroup_add 
41978  336 
proof 
53873  337 
fix a b c :: ereal 
338 
assume "a \<le> b" 

339 
then show "c + a \<le> c + b" 

43920  340 
by (cases rule: ereal3_cases[of a b c]) auto 
41978  341 
qed 
342 

43920  343 
lemma real_of_ereal_positive_mono: 
53873  344 
fixes x y :: ereal 
345 
shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real x \<le> real y" 

43920  346 
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

347 

43920  348 
lemma ereal_MInfty_lessI[intro, simp]: 
53873  349 
fixes a :: ereal 
350 
shows "a \<noteq> \<infinity> \<Longrightarrow> \<infinity> < a" 

41973  351 
by (cases a) auto 
352 

43920  353 
lemma ereal_less_PInfty[intro, simp]: 
53873  354 
fixes a :: ereal 
355 
shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>" 

41973  356 
by (cases a) auto 
357 

43920  358 
lemma ereal_less_ereal_Ex: 
359 
fixes a b :: ereal 

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

41973  361 
by (cases x) auto 
362 

43920  363 
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

364 
proof (cases x) 
53873  365 
case (real r) 
366 
then show ?thesis 

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

367 
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

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

369 

43920  370 
lemma ereal_add_mono: 
53873  371 
fixes a b c d :: ereal 
372 
assumes "a \<le> b" 

373 
and "c \<le> d" 

374 
shows "a + c \<le> b + d" 

41973  375 
using assms 
376 
apply (cases a) 

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

41973  379 
done 
380 

43920  381 
lemma ereal_minus_le_minus[simp]: 
53873  382 
fixes a b :: ereal 
383 
shows " a \<le>  b \<longleftrightarrow> b \<le> a" 

43920  384 
by (cases rule: ereal2_cases[of a b]) auto 
41973  385 

43920  386 
lemma ereal_minus_less_minus[simp]: 
53873  387 
fixes a b :: ereal 
388 
shows " a <  b \<longleftrightarrow> b < a" 

43920  389 
by (cases rule: ereal2_cases[of a b]) auto 
41973  390 

43920  391 
lemma ereal_le_real_iff: 
53873  392 
"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  393 
by (cases y) auto 
394 

43920  395 
lemma real_le_ereal_iff: 
53873  396 
"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  397 
by (cases y) auto 
398 

43920  399 
lemma ereal_less_real_iff: 
53873  400 
"x < real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)" 
41973  401 
by (cases y) auto 
402 

43920  403 
lemma real_less_ereal_iff: 
53873  404 
"real y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)" 
41973  405 
by (cases y) auto 
406 

43920  407 
lemma real_of_ereal_pos: 
53873  408 
fixes x :: ereal 
409 
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

410 

43920  411 
lemmas real_of_ereal_ord_simps = 
412 
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff 

41973  413 

43920  414 
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

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

416 

43920  417 
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

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

419 

43920  420 
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

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

422 

53873  423 
lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" 
43923  424 
by (cases x) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

425 

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

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

428 

43923  429 
lemma zero_less_real_of_ereal: 
53873  430 
fixes x :: ereal 
431 
shows "0 < real x \<longleftrightarrow> 0 < x \<and> x \<noteq> \<infinity>" 

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

433 

43920  434 
lemma ereal_0_le_uminus_iff[simp]: 
53873  435 
fixes a :: ereal 
436 
shows "0 \<le>  a \<longleftrightarrow> a \<le> 0" 

43920  437 
by (cases rule: ereal2_cases[of a]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

438 

43920  439 
lemma ereal_uminus_le_0_iff[simp]: 
53873  440 
fixes a :: ereal 
441 
shows " a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

43920  442 
by (cases rule: ereal2_cases[of a]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

443 

43920  444 
lemma ereal_add_strict_mono: 
445 
fixes a b c d :: ereal 

53873  446 
assumes "a = b" 
447 
and "0 \<le> a" 

448 
and "a \<noteq> \<infinity>" 

449 
and "c < d" 

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

450 
shows "a + c < b + d" 
53873  451 
using assms 
452 
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

453 

53873  454 
lemma ereal_less_add: 
455 
fixes a b c :: ereal 

456 
shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b" 

43920  457 
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

458 

53873  459 
lemma ereal_uminus_eq_reorder: " a = b \<longleftrightarrow> a = (b::ereal)" 
460 
by auto 

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

461 

43920  462 
lemma ereal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::ereal)" 
463 
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

464 

43920  465 
lemma ereal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::ereal)" 
466 
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

467 

43920  468 
lemmas ereal_uminus_reorder = 
469 
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

470 

43920  471 
lemma ereal_bot: 
53873  472 
fixes x :: ereal 
473 
assumes "\<And>B. x \<le> ereal B" 

474 
shows "x =  \<infinity>" 

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

475 
proof (cases x) 
53873  476 
case (real r) 
477 
with assms[of "r  1"] show ?thesis 

478 
by auto 

47082  479 
next 
53873  480 
case PInf 
481 
with assms[of 0] show ?thesis 

482 
by auto 

47082  483 
next 
53873  484 
case MInf 
485 
then show ?thesis 

486 
by simp 

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

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

488 

43920  489 
lemma ereal_top: 
53873  490 
fixes x :: ereal 
491 
assumes "\<And>B. x \<ge> ereal B" 

492 
shows "x = \<infinity>" 

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

493 
proof (cases x) 
53873  494 
case (real r) 
495 
with assms[of "r + 1"] show ?thesis 

496 
by auto 

47082  497 
next 
53873  498 
case MInf 
499 
with assms[of 0] show ?thesis 

500 
by auto 

47082  501 
next 
53873  502 
case PInf 
503 
then show ?thesis 

504 
by simp 

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

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

506 

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

507 
lemma 
43920  508 
shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)" 
509 
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

510 
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

511 

43920  512 
lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)" 
513 
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

514 

41978  515 
lemma 
43920  516 
fixes f :: "nat \<Rightarrow> ereal" 
41978  517 
shows incseq_uminus[simp]: "incseq (\<lambda>x.  f x) \<longleftrightarrow> decseq f" 
518 
and decseq_uminus[simp]: "decseq (\<lambda>x.  f x) \<longleftrightarrow> incseq f" 

519 
unfolding decseq_def incseq_def by auto 

520 

43920  521 
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

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

523 

43920  524 
lemma ereal_add_nonneg_nonneg: 
53873  525 
fixes a b :: ereal 
526 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 

41978  527 
using add_mono[of 0 a 0 b] by simp 
528 

53873  529 
lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B" 
41978  530 
by auto 
531 

532 
lemma incseq_setsumI: 

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

536 
proof (intro incseq_SucI) 

53873  537 
fix n 
538 
have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n" 

41978  539 
using assms by (rule add_left_mono) 
540 
then show "setsum f {..< n} \<le> setsum f {..< Suc n}" 

541 
by auto 

542 
qed 

543 

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

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

546 
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

547 
shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)" 
53873  548 
using assms 
549 
unfolding incseq_def by (auto intro: setsum_mono) 

550 

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

551 

41973  552 
subsubsection "Multiplication" 
553 

53873  554 
instantiation ereal :: "{comm_monoid_mult,sgn}" 
41973  555 
begin 
556 

51351  557 
function sgn_ereal :: "ereal \<Rightarrow> ereal" where 
43920  558 
"sgn (ereal r) = ereal (sgn r)" 
43923  559 
 "sgn (\<infinity>::ereal) = 1" 
560 
 "sgn (\<infinity>::ereal) = 1" 

43920  561 
by (auto intro: ereal_cases) 
53873  562 
termination by default (rule wf_empty) 
41976  563 

43920  564 
function times_ereal where 
53873  565 
"ereal r * ereal p = ereal (r * p)" 
566 
 "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)" 

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

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

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

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

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

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

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

41973  574 
proof  
575 
case (goal1 P x) 

53873  576 
then obtain a b where "x = (a, b)" 
577 
by (cases x) auto 

578 
with goal1 show P 

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

41973  580 
qed simp_all 
581 
termination by (relation "{}") simp 

582 

583 
instance 

584 
proof 

53873  585 
fix a b c :: ereal 
586 
show "1 * a = a" 

43920  587 
by (cases a) (simp_all add: one_ereal_def) 
47082  588 
show "a * b = b * a" 
43920  589 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  590 
show "a * b * c = a * (b * c)" 
43920  591 
by (cases rule: ereal3_cases[of a b c]) 
592 
(simp_all add: zero_ereal_def zero_less_mult_iff) 

41973  593 
qed 
53873  594 

41973  595 
end 
596 

50104  597 
lemma real_ereal_1[simp]: "real (1::ereal) = 1" 
598 
unfolding one_ereal_def by simp 

599 

43920  600 
lemma real_of_ereal_le_1: 
53873  601 
fixes a :: ereal 
602 
shows "a \<le> 1 \<Longrightarrow> real a \<le> 1" 

43920  603 
by (cases a) (auto simp: one_ereal_def) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

604 

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

41976  607 

43920  608 
lemma ereal_mult_zero[simp]: 
53873  609 
fixes a :: ereal 
610 
shows "a * 0 = 0" 

43920  611 
by (cases a) (simp_all add: zero_ereal_def) 
41973  612 

43920  613 
lemma ereal_zero_mult[simp]: 
53873  614 
fixes a :: ereal 
615 
shows "0 * a = 0" 

43920  616 
by (cases a) (simp_all add: zero_ereal_def) 
41973  617 

53873  618 
lemma ereal_m1_less_0[simp]: "(1::ereal) < 0" 
43920  619 
by (simp add: zero_ereal_def one_ereal_def) 
41973  620 

53873  621 
lemma ereal_zero_m1[simp]: "1 \<noteq> (0::ereal)" 
43920  622 
by (simp add: zero_ereal_def one_ereal_def) 
41973  623 

43920  624 
lemma ereal_times_0[simp]: 
53873  625 
fixes x :: ereal 
626 
shows "0 * x = 0" 

43920  627 
by (cases x) (auto simp: zero_ereal_def) 
41973  628 

43920  629 
lemma ereal_times[simp]: 
43923  630 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 
631 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 

43920  632 
by (auto simp add: times_ereal_def one_ereal_def) 
41973  633 

43920  634 
lemma ereal_plus_1[simp]: 
53873  635 
"1 + ereal r = ereal (r + 1)" 
636 
"ereal r + 1 = ereal (r + 1)" 

637 
"1 + (\<infinity>::ereal) = \<infinity>" 

638 
"(\<infinity>::ereal) + 1 = \<infinity>" 

43920  639 
unfolding one_ereal_def by auto 
41973  640 

43920  641 
lemma ereal_zero_times[simp]: 
53873  642 
fixes a b :: ereal 
643 
shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

43920  644 
by (cases rule: ereal2_cases[of a b]) auto 
41973  645 

43920  646 
lemma ereal_mult_eq_PInfty[simp]: 
53873  647 
"a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  648 
(a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>)" 
43920  649 
by (cases rule: ereal2_cases[of a b]) auto 
41973  650 

43920  651 
lemma ereal_mult_eq_MInfty[simp]: 
53873  652 
"a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  653 
(a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>)" 
43920  654 
by (cases rule: ereal2_cases[of a b]) auto 
41973  655 

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

41973  658 

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

41973  661 

43920  662 
lemma ereal_mult_minus_left[simp]: 
53873  663 
fixes a b :: ereal 
664 
shows "a * b =  (a * b)" 

43920  665 
by (cases rule: ereal2_cases[of a b]) auto 
41973  666 

43920  667 
lemma ereal_mult_minus_right[simp]: 
53873  668 
fixes a b :: ereal 
669 
shows "a * b =  (a * b)" 

43920  670 
by (cases rule: ereal2_cases[of a b]) auto 
41973  671 

43920  672 
lemma ereal_mult_infty[simp]: 
43923  673 
"a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  674 
by (cases a) auto 
675 

43920  676 
lemma ereal_infty_mult[simp]: 
43923  677 
"(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  678 
by (cases a) auto 
679 

43920  680 
lemma ereal_mult_strict_right_mono: 
53873  681 
assumes "a < b" 
682 
and "0 < c" 

683 
and "c < (\<infinity>::ereal)" 

41973  684 
shows "a * c < b * c" 
685 
using assms 

53873  686 
by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff) 
41973  687 

43920  688 
lemma ereal_mult_strict_left_mono: 
53873  689 
"a < b \<Longrightarrow> 0 < c \<Longrightarrow> c < (\<infinity>::ereal) \<Longrightarrow> c * a < c * b" 
690 
using ereal_mult_strict_right_mono 

691 
by (simp add: mult_commute[of c]) 

41973  692 

43920  693 
lemma ereal_mult_right_mono: 
53873  694 
fixes a b c :: ereal 
695 
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 

41973  696 
using assms 
53873  697 
apply (cases "c = 0") 
698 
apply simp 

699 
apply (cases rule: ereal3_cases[of a b c]) 

700 
apply (auto simp: zero_le_mult_iff) 

701 
done 

41973  702 

43920  703 
lemma ereal_mult_left_mono: 
53873  704 
fixes a b c :: ereal 
705 
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 

706 
using ereal_mult_right_mono 

707 
by (simp add: mult_commute[of c]) 

41973  708 

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

41978  711 

43920  712 
lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)" 
713 
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

714 

43920  715 
lemma ereal_right_distrib: 
53873  716 
fixes r a b :: ereal 
717 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b" 

43920  718 
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

719 

43920  720 
lemma ereal_left_distrib: 
53873  721 
fixes r a b :: ereal 
722 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r" 

43920  723 
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

724 

43920  725 
lemma ereal_mult_le_0_iff: 
726 
fixes a b :: ereal 

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

727 
shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)" 
43920  728 
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

729 

43920  730 
lemma ereal_zero_le_0_iff: 
731 
fixes a b :: ereal 

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

732 
shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)" 
43920  733 
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

734 

43920  735 
lemma ereal_mult_less_0_iff: 
736 
fixes a b :: ereal 

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

737 
shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)" 
43920  738 
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

739 

43920  740 
lemma ereal_zero_less_0_iff: 
741 
fixes a b :: ereal 

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

742 
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)" 
43920  743 
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

744 

50104  745 
lemma ereal_left_mult_cong: 
746 
fixes a b c :: ereal 

747 
shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b" 

748 
by (cases "c = 0") simp_all 

749 

750 
lemma ereal_right_mult_cong: 

751 
fixes a b c :: ereal 

752 
shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c" 

753 
by (cases "c = 0") simp_all 

754 

43920  755 
lemma ereal_distrib: 
756 
fixes a b c :: ereal 

53873  757 
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" 
758 
and "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" 

759 
and "\<bar>c\<bar> \<noteq> \<infinity>" 

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

760 
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

761 
using assms 
43920  762 
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

763 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

764 
lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

765 
apply (induct w rule: num_induct) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

766 
apply (simp only: numeral_One one_ereal_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

767 
apply (simp only: numeral_inc ereal_plus_1) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

768 
done 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

769 

43920  770 
lemma ereal_le_epsilon: 
771 
fixes x y :: ereal 

53873  772 
assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e" 
773 
shows "x \<le> y" 

774 
proof  

775 
{ 

776 
assume a: "\<exists>r. y = ereal r" 

777 
then obtain r where r_def: "y = ereal r" 

778 
by auto 

779 
{ 

780 
assume "x = \<infinity>" 

781 
then have ?thesis by auto 

782 
} 

783 
moreover 

784 
{ 

785 
assume "x \<noteq> \<infinity>" 

786 
then obtain p where p_def: "x = ereal p" 

787 
using a assms[rule_format, of 1] 

788 
by (cases x) auto 

789 
{ 

790 
fix e 

791 
have "0 < e \<longrightarrow> p \<le> r + e" 

792 
using assms[rule_format, of "ereal e"] p_def r_def by auto 

793 
} 

794 
then have "p \<le> r" 

795 
apply (subst field_le_epsilon) 

796 
apply auto 

797 
done 

798 
then have ?thesis 

799 
using r_def p_def by auto 

800 
} 

801 
ultimately have ?thesis 

802 
by blast 

803 
} 

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

804 
moreover 
53873  805 
{ 
806 
assume "y = \<infinity>  y = \<infinity>" 

807 
then have ?thesis 

808 
using assms[rule_format, of 1] by (cases x) auto 

809 
} 

810 
ultimately show ?thesis 

811 
by (cases y) auto 

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

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

813 

43920  814 
lemma ereal_le_epsilon2: 
815 
fixes x y :: ereal 

53873  816 
assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e" 
817 
shows "x \<le> y" 

818 
proof  

819 
{ 

820 
fix e :: ereal 

821 
assume "e > 0" 

822 
{ 

823 
assume "e = \<infinity>" 

824 
then have "x \<le> y + e" 

825 
by auto 

826 
} 

827 
moreover 

828 
{ 

829 
assume "e \<noteq> \<infinity>" 

830 
then obtain r where "e = ereal r" 

831 
using `e > 0` by (cases e) auto 

832 
then have "x \<le> y + e" 

833 
using assms[rule_format, of r] `e>0` by auto 

834 
} 

835 
ultimately have "x \<le> y + e" 

836 
by blast 

837 
} 

838 
then show ?thesis 

839 
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

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

841 

43920  842 
lemma ereal_le_real: 
843 
fixes x y :: ereal 

53873  844 
assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z" 
845 
shows "y \<le> x" 

846 
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

847 

43920  848 
lemma setprod_ereal_0: 
849 
fixes f :: "'a \<Rightarrow> ereal" 

53873  850 
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)" 
851 
proof (cases "finite A") 

852 
case True 

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

853 
then show ?thesis by (induct A) auto 
53873  854 
next 
855 
case False 

856 
then show ?thesis by auto 

857 
qed 

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

858 

43920  859 
lemma setprod_ereal_pos: 
53873  860 
fixes f :: "'a \<Rightarrow> ereal" 
861 
assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" 

862 
shows "0 \<le> (\<Prod>i\<in>I. f i)" 

863 
proof (cases "finite I") 

864 
case True 

865 
from this pos show ?thesis 

866 
by induct auto 

867 
next 

868 
case False 

869 
then show ?thesis by simp 

870 
qed 

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

871 

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

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

874 
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

875 
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)" 
53873  876 
proof (cases "finite I") 
877 
case True 

878 
from this assms show ?thesis 

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

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

880 
case (insert i I) 
53873  881 
then have pos: "0 \<le> f i" "0 \<le> setprod f I" 
882 
by (auto intro!: setprod_ereal_pos) 

883 
from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" 

884 
by auto 

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

885 
also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0" 
43920  886 
using setprod_ereal_pos[of I f] pos 
887 
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

888 
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  889 
using insert by (auto simp: setprod_ereal_0) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

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

891 
qed simp 
53873  892 
next 
893 
case False 

894 
then show ?thesis by simp 

895 
qed 

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

896 

43920  897 
lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)" 
53873  898 
proof (cases "finite A") 
899 
case True 

900 
then show ?thesis 

43920  901 
by induct (auto simp: one_ereal_def) 
53873  902 
next 
903 
case False 

904 
then show ?thesis 

905 
by (simp add: one_ereal_def) 

906 
qed 

907 

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

908 

41978  909 
subsubsection {* Power *} 
910 

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

41978  913 

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

43920  917 
lemma ereal_power_uminus[simp]: 
918 
fixes x :: ereal 

41978  919 
shows "( x) ^ n = (if even n then x ^ n else  (x^n))" 
43920  920 
by (induct n) (auto simp: one_ereal_def) 
41978  921 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

922 
lemma ereal_power_numeral[simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

923 
"(numeral num :: ereal) ^ n = ereal (numeral num ^ n)" 
43920  924 
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

925 

43920  926 
lemma zero_le_power_ereal[simp]: 
53873  927 
fixes a :: ereal 
928 
assumes "0 \<le> a" 

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

929 
shows "0 \<le> a ^ n" 
43920  930 
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

931 

53873  932 

41973  933 
subsubsection {* Subtraction *} 
934 

43920  935 
lemma ereal_minus_minus_image[simp]: 
936 
fixes S :: "ereal set" 

41973  937 
shows "uminus ` uminus ` S = S" 
938 
by (auto simp: image_iff) 

939 

43920  940 
lemma ereal_uminus_lessThan[simp]: 
53873  941 
fixes a :: ereal 
942 
shows "uminus ` {..<a} = {a<..}" 

47082  943 
proof  
944 
{ 

53873  945 
fix x 
946 
assume "a < x" 

947 
then have " x <  ( a)" 

948 
by (simp del: ereal_uminus_uminus) 

949 
then have " x < a" 

950 
by simp 

47082  951 
} 
53873  952 
then show ?thesis 
953 
by (auto intro!: image_eqI) 

47082  954 
qed 
41973  955 

53873  956 
lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<a}" 
957 
by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image) 

41973  958 

43920  959 
instantiation ereal :: minus 
41973  960 
begin 
53873  961 

43920  962 
definition "x  y = x + (y::ereal)" 
41973  963 
instance .. 
53873  964 

41973  965 
end 
966 

43920  967 
lemma ereal_minus[simp]: 
968 
"ereal r  ereal p = ereal (r  p)" 

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

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

43923  971 
"(\<infinity>::ereal)  x = \<infinity>" 
972 
"(\<infinity>::ereal)  \<infinity> = \<infinity>" 

41973  973 
"x  y = x + y" 
974 
"x  0 = x" 

975 
"0  x = x" 

43920  976 
by (simp_all add: minus_ereal_def) 
41973  977 

53873  978 
lemma ereal_x_minus_x[simp]: "x  x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)" 
41973  979 
by (cases x) simp_all 
980 

43920  981 
lemma ereal_eq_minus_iff: 
982 
fixes x y z :: ereal 

41973  983 
shows "x = z  y \<longleftrightarrow> 
41976  984 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and> 
41973  985 
(y = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 
986 
(y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 

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

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

43920  990 
lemma ereal_eq_minus: 
991 
fixes x y z :: ereal 

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

43920  995 
lemma ereal_less_minus_iff: 
996 
fixes x y z :: ereal 

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

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

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

43920  1003 
lemma ereal_less_minus: 
1004 
fixes x y z :: ereal 

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

43920  1008 
lemma ereal_le_minus_iff: 
1009 
fixes x y z :: ereal 

53873  1010 
shows "x \<le> z  y \<longleftrightarrow> (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = \<infinity>) \<and> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)" 
43920  1011 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  1012 

43920  1013 
lemma ereal_le_minus: 
1014 
fixes x y z :: ereal 

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

43920  1018 
lemma ereal_minus_less_iff: 
1019 
fixes x y z :: ereal 

53873  1020 
shows "x  y < z \<longleftrightarrow> y \<noteq> \<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> \<infinity>) \<and> (y \<noteq> \<infinity> \<longrightarrow> x < z + y)" 
43920  1021 
by (cases rule: ereal3_cases[of x y z]) auto 
41973  1022 

43920  1023 
lemma ereal_minus_less: 
1024 
fixes x y z :: ereal 

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

43920  1028 
lemma ereal_minus_le_iff: 
1029 
fixes x y z :: ereal 

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

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

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

43920  1036 
lemma ereal_minus_le: 
1037 
fixes x y z :: ereal 

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

43920  1041 
lemma ereal_minus_eq_minus_iff: 
1042 
fixes a b c :: ereal 

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

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

43920  1047 
lemma ereal_add_le_add_iff: 
43923  1048 
fixes a b c :: ereal 
1049 
shows "c + a \<le> c + b \<longleftrightarrow> 

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

43920  1053 
lemma ereal_mult_le_mult_iff: 
43923  1054 
fixes a b c :: ereal 
1055 
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  1056 
by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left) 
41973  1057 

43920  1058 
lemma ereal_minus_mono: 
1059 
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

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

1061 
using assms 
43920  1062 
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

1063 

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

43920  1067 
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

1068 

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

1071 
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

1072 

43920  1073 
lemma ereal_between: 
1074 
fixes x e :: ereal 

53873  1075 
assumes "\<bar>x\<bar> \<noteq> \<infinity>" 
1076 
and "0 < e" 

1077 
shows "x  e < x" 

1078 
and "x < x + e" 

1079 
using assms 

1080 
apply (cases x, cases e) 

1081 
apply auto 

1082 
using assms 

1083 
apply (cases x, cases e) 

1084 
apply auto 

1085 
done 

41973  1086 

50104  1087 
lemma ereal_minus_eq_PInfty_iff: 
53873  1088 
fixes x y :: ereal 
1089 
shows "x  y = \<infinity> \<longleftrightarrow> y = \<infinity> \<or> x = \<infinity>" 

50104  1090 
by (cases x y rule: ereal2_cases) simp_all 
1091 

53873  1092 

41973  1093 
subsubsection {* Division *} 
1094 

43920  1095 
instantiation ereal :: inverse 
41973  1096 
begin 
1097 

43920  1098 
function inverse_ereal where 
53873  1099 
"inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" 
1100 
 "inverse (\<infinity>::ereal) = 0" 

1101 
 "inverse (\<infinity>::ereal) = 0" 

43920  1102 
by (auto intro: ereal_cases) 
41973  1103 
termination by (relation "{}") simp 
1104 

43920  1105 
definition "x / y = x * inverse (y :: ereal)" 
41973  1106 

47082  1107 
instance .. 
53873  1108 

41973  1109 
end 
1110 

43920  1111 
lemma real_of_ereal_inverse[simp]: 
1112 
fixes a :: ereal 

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

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

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

1115 

43920  1116 
lemma ereal_inverse[simp]: 
43923  1117 
"inverse (0::ereal) = \<infinity>" 
43920  1118 
"inverse (1::ereal) = 1" 
1119 
by (simp_all add: one_ereal_def zero_ereal_def) 

41973  1120 

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

1123 
unfolding divide_ereal_def by (auto simp: divide_real_def) 

41973  1124 

43920  1125 
lemma ereal_divide_same[simp]: 
53873  1126 
fixes x :: ereal 
1127 
shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)" 

1128 
by (cases x) (simp_all add: divide_real_def divide_ereal_def one_ereal_def) 

41973  1129 

43920  1130 
lemma ereal_inv_inv[simp]: 
53873  1131 
fixes x :: ereal 
1132 
shows "inverse (inverse x) = (if x \<noteq> \<infinity> then x else \<infinity>)" 

41973  1133 
by (cases x) auto 
1134 

43920  1135 
lemma ereal_inverse_minus[simp]: 
53873  1136 
fixes x :: ereal 
1137 
shows "inverse ( x) = (if x = 0 then \<infinity> else inverse x)" 

41973  1138 
by (cases x) simp_all 
1139 

43920  1140 
lemma ereal_uminus_divide[simp]: 
53873  1141 
fixes x y :: ereal 
1142 
shows " x / y =  (x / y)" 

43920  1143 
unfolding divide_ereal_def by simp 
41973  1144 

43920  1145 
lemma ereal_divide_Infty[simp]: 
53873  1146 
fixes x :: ereal 
1147 
shows "x / \<infinity> = 0" "x / \<infinity> = 0" 

43920  1148 
unfolding divide_ereal_def by simp_all 
41973  1149 

53873  1150 
lemma ereal_divide_one[simp]: "x / 1 = (x::ereal)" 
43920  1151 
unfolding divide_ereal_def by simp 
41973  1152 

53873  1153 
lemma ereal_divide_ereal[simp]: "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else \<infinity>)" 
43920  1154 
unfolding divide_ereal_def by simp 
41973  1155 

43920  1156 
lemma zero_le_divide_ereal[simp]: 
53873  1157 
fixes a :: ereal 
1158 
assumes "0 \<le> a" 

1159 
and "0 \<le> b" 

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

43920  1163 
lemma ereal_le_divide_pos: 
53873  1164 
fixes x y z :: ereal 
1165 
shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z" 

43920  1166 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1167 

43920  1168 
lemma ereal_divide_le_pos: 
53873  1169 
fixes x y z :: ereal 
1170 
shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y" 

43920  1171 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1172 

43920  1173 
lemma ereal_le_divide_neg: 
53873  1174 
fixes x y z :: ereal 
1175 
shows "x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y" 

43920  1176 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1177 

43920  1178 
lemma ereal_divide_le_neg: 
53873  1179 
fixes x y z :: ereal 
1180 
shows "x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z" 

43920  1181 
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps) 
41973  1182 

43920  1183 
lemma ereal_inverse_antimono_strict: 
1184 
fixes x y :: ereal 

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

43920  1188 
lemma ereal_inverse_antimono: 
1189 
fixes x y :: ereal 

53873  1190 
shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> inverse y \<le> inverse x" 
43920  1191 
by (cases rule: ereal2_cases[of x y]) auto 
41973  1192 

1193 
lemma inverse_inverse_Pinfty_iff[simp]: 

53873  1194 
fixes x :: ereal 
1195 
shows "inverse x = \<infinity> \<longleftrightarrow> x = 0" 

41973  1196 
by (cases x) auto 
1197 

43920  1198 
lemma ereal_inverse_eq_0: 
53873  1199 
fixes x :: ereal 
1200 
shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = \<infinity>" 

41973  1201 
by (cases x) auto 
1202 

43920  1203 
lemma ereal_0_gt_inverse: 
53873  1204 
fixes x :: ereal 
1205 
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

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

1207 

43920  1208 
lemma ereal_mult_less_right: 
43923  1209 
fixes a b c :: ereal 
53873  1210 
assumes "b * a < c * a" 
1211 
and "0 < a" 

1212 
and "a < \<infinity>" 

41973  1213 
shows "b < c" 
1214 
using assms 

43920  1215 
by (cases rule: ereal3_cases[of a b c]) 
41973  1216 
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff) 
1217 

43920  1218 
lemma ereal_power_divide: 
53873  1219 
fixes x y :: ereal 
1220 
shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n" 

43920  1221 
by (cases rule: ereal2_cases[of x y]) 
1222 
(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

1223 
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

1224 

43920  1225 
lemma ereal_le_mult_one_interval: 
1226 
fixes x y :: ereal 

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

1227 
assumes y: "y \<noteq> \<infinity>" 
53873  1228 
assumes z: "\<And>z. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> z * x \<le> y" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

1230 
proof (cases x) 
53873  1231 
case PInf 
1232 
with z[of "1 / 2"] show "x \<le> y" 

1233 
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

1234 
next 
53873  1235 
case (real r) 
1236 
note r = this 

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

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

1238 
proof (cases y) 
53873  1239 
case (real p) 
1240 
note p = this 

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

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

1242 
proof (rule field_le_mult_one_interval) 
53873  1243 
fix z :: real 
1244 
assume "0 < z" and "z < 1" 

1245 
with z[of "ereal z"] show "z * r \<le> p" 

1246 
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

1247 
qed 
53873  1248 
then show "x \<le> y" 
1249 
using p r by simp 

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

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