author  hoelzl 
Mon, 14 Mar 2011 14:37:46 +0100  
changeset 41979  b10ec1f5e9d5 
parent 41978  656298577a33 
child 41980  28b51effc5ed 
permissions  rwrr 
41978  1 
(* Title: Extended_Reals.thy 
41973  2 
Author: Johannes Hölzl, Robert Himmelmann, Armin Heller; TU München 
3 
Author: Bogdan Grechuk; University of Edinburgh *) 

4 

5 
header {* Extended real number line *} 

6 

7 
theory Extended_Reals 

8 
imports Topology_Euclidean_Space 

9 
begin 

10 

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

11 
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

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

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

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

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

16 
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

17 
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

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

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

20 

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

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

22 
"(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

24 

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

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

26 
"(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

28 

41973  29 
subsection {* Definition and basic properties *} 
30 

31 
datatype extreal = extreal real  PInfty  MInfty 

32 

33 
notation (xsymbols) 

34 
PInfty ("\<infinity>") 

35 

36 
notation (HTML output) 

37 
PInfty ("\<infinity>") 

38 

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

39 
declare [[coercion "extreal :: real \<Rightarrow> extreal"]] 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

40 

41973  41 
instantiation extreal :: uminus 
42 
begin 

43 
fun uminus_extreal where 

44 
" (extreal r) = extreal ( r)" 

45 
 " \<infinity> = MInfty" 

46 
 " MInfty = \<infinity>" 

47 
instance .. 

48 
end 

49 

41976  50 
lemma inj_extreal[simp]: "inj_on extreal A" 
51 
unfolding inj_on_def by auto 

52 

41973  53 
lemma MInfty_neq_PInfty[simp]: 
54 
"\<infinity> \<noteq>  \<infinity>" " \<infinity> \<noteq> \<infinity>" by simp_all 

55 

56 
lemma MInfty_neq_extreal[simp]: 

57 
"extreal r \<noteq>  \<infinity>" " \<infinity> \<noteq> extreal r" by simp_all 

58 

59 
lemma MInfinity_cases[simp]: 

60 
"(case  \<infinity> of extreal r \<Rightarrow> f r  \<infinity> \<Rightarrow> y  MInfinity \<Rightarrow> z) = z" 

61 
by simp 

62 

63 
lemma extreal_uminus_uminus[simp]: 

64 
fixes a :: extreal shows " ( a) = a" 

65 
by (cases a) simp_all 

66 

67 
lemma MInfty_eq[simp]: 

68 
"MInfty =  \<infinity>" by simp 

69 

70 
declare uminus_extreal.simps(2)[simp del] 

71 

72 
lemma extreal_cases[case_names real PInf MInf, cases type: extreal]: 

73 
assumes "\<And>r. x = extreal r \<Longrightarrow> P" 

74 
assumes "x = \<infinity> \<Longrightarrow> P" 

75 
assumes "x = \<infinity> \<Longrightarrow> P" 

76 
shows P 

77 
using assms by (cases x) auto 

78 

41974  79 
lemmas extreal2_cases = extreal_cases[case_product extreal_cases] 
80 
lemmas extreal3_cases = extreal2_cases[case_product extreal_cases] 

41973  81 

82 
lemma extreal_uminus_eq_iff[simp]: 

83 
fixes a b :: extreal shows "a = b \<longleftrightarrow> a = b" 

84 
by (cases rule: extreal2_cases[of a b]) simp_all 

85 

86 
function of_extreal :: "extreal \<Rightarrow> real" where 

87 
"of_extreal (extreal r) = r"  

88 
"of_extreal \<infinity> = 0"  

89 
"of_extreal (\<infinity>) = 0" 

90 
by (auto intro: extreal_cases) 

91 
termination proof qed (rule wf_empty) 

92 

93 
defs (overloaded) 

94 
real_of_extreal_def [code_unfold]: "real \<equiv> of_extreal" 

95 

96 
lemma real_of_extreal[simp]: 

97 
"real ( x :: extreal) =  (real x)" 

98 
"real (extreal r) = r" 

99 
"real \<infinity> = 0" 

100 
by (cases x) (simp_all add: real_of_extreal_def) 

101 

102 
lemma range_extreal[simp]: "range extreal = UNIV  {\<infinity>, \<infinity>}" 

103 
proof safe 

104 
fix x assume "x \<notin> range extreal" "x \<noteq> \<infinity>" 

105 
then show "x = \<infinity>" by (cases x) auto 

106 
qed auto 

107 

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

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

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

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

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

112 

41973  113 
instantiation extreal :: number 
114 
begin 

115 
definition [simp]: "number_of x = extreal (number_of x)" 

116 
instance proof qed 

117 
end 

118 

41976  119 
instantiation extreal :: abs 
120 
begin 

121 
function abs_extreal where 

122 
"\<bar>extreal r\<bar> = extreal \<bar>r\<bar>" 

123 
 "\<bar>\<infinity>\<bar> = \<infinity>" 

124 
 "\<bar>\<infinity>\<bar> = \<infinity>" 

125 
by (auto intro: extreal_cases) 

126 
termination proof qed (rule wf_empty) 

127 
instance .. 

128 
end 

129 

130 
lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = \<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 

131 
by (cases x) auto 

132 

133 
lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x\<bar> \<noteq> \<infinity> ; \<And>r. x = extreal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 

134 
by (cases x) auto 

135 

136 
lemma abs_extreal_uminus[simp]: "\<bar> x\<bar> = \<bar>x::extreal\<bar>" 

137 
by (cases x) auto 

138 

41973  139 
subsubsection "Addition" 
140 

141 
instantiation extreal :: comm_monoid_add 

142 
begin 

143 

144 
definition "0 = extreal 0" 

145 

146 
function plus_extreal where 

147 
"extreal r + extreal p = extreal (r + p)"  

148 
"\<infinity> + a = \<infinity>"  

149 
"a + \<infinity> = \<infinity>"  

150 
"extreal r + \<infinity> =  \<infinity>"  

151 
"\<infinity> + extreal p = \<infinity>"  

152 
"\<infinity> + \<infinity> = \<infinity>" 

153 
proof  

154 
case (goal1 P x) 

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

156 
ultimately show P 

157 
by (cases rule: extreal2_cases[of a b]) auto 

158 
qed auto 

159 
termination proof qed (rule wf_empty) 

160 

161 
lemma Infty_neq_0[simp]: 

162 
"\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>" 

163 
"\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>" 

164 
by (simp_all add: zero_extreal_def) 

165 

166 
lemma extreal_eq_0[simp]: 

167 
"extreal r = 0 \<longleftrightarrow> r = 0" 

168 
"0 = extreal r \<longleftrightarrow> r = 0" 

169 
unfolding zero_extreal_def by simp_all 

170 

171 
instance 

172 
proof 

173 
fix a :: extreal show "0 + a = a" 

174 
by (cases a) (simp_all add: zero_extreal_def) 

175 
fix b :: extreal show "a + b = b + a" 

176 
by (cases rule: extreal2_cases[of a b]) simp_all 

177 
fix c :: extreal show "a + b + c = a + (b + c)" 

178 
by (cases rule: extreal3_cases[of a b c]) simp_all 

179 
qed 

180 
end 

181 

41976  182 
lemma abs_extreal_zero[simp]: "\<bar>0\<bar> = (0::extreal)" 
183 
unfolding zero_extreal_def abs_extreal.simps by simp 

184 

41973  185 
lemma extreal_uminus_zero[simp]: 
186 
" 0 = (0::extreal)" 

187 
by (simp add: zero_extreal_def) 

188 

189 
lemma extreal_uminus_zero_iff[simp]: 

190 
fixes a :: extreal shows "a = 0 \<longleftrightarrow> a = 0" 

191 
by (cases a) simp_all 

192 

193 
lemma extreal_plus_eq_PInfty[simp]: 

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

195 
by (cases rule: extreal2_cases[of a b]) auto 

196 

197 
lemma extreal_plus_eq_MInfty[simp]: 

198 
shows "a + b = \<infinity> \<longleftrightarrow> 

199 
(a = \<infinity> \<or> b = \<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>" 

200 
by (cases rule: extreal2_cases[of a b]) auto 

201 

202 
lemma extreal_add_cancel_left: 

203 
assumes "a \<noteq> \<infinity>" 

204 
shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)" 

205 
using assms by (cases rule: extreal3_cases[of a b c]) auto 

206 

207 
lemma extreal_add_cancel_right: 

208 
assumes "a \<noteq> \<infinity>" 

209 
shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)" 

210 
using assms by (cases rule: extreal3_cases[of a b c]) auto 

211 

212 
lemma extreal_real: 

41976  213 
"extreal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)" 
41973  214 
by (cases x) simp_all 
215 

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

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

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

218 
shows "real (a + b) = (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

220 

41973  221 
subsubsection "Linear order on @{typ extreal}" 
222 

223 
instantiation extreal :: linorder 

224 
begin 

225 

226 
function less_extreal where 

227 
"extreal x < extreal y \<longleftrightarrow> x < y"  

228 
" \<infinity> < a \<longleftrightarrow> False"  

229 
" a < \<infinity> \<longleftrightarrow> False"  

230 
"extreal x < \<infinity> \<longleftrightarrow> True"  

231 
" \<infinity> < extreal r \<longleftrightarrow> True"  

232 
" \<infinity> < \<infinity> \<longleftrightarrow> True" 

233 
proof  

234 
case (goal1 P x) 

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

236 
ultimately show P by (cases rule: extreal2_cases[of a b]) auto 

237 
qed simp_all 

238 
termination by (relation "{}") simp 

239 

240 
definition "x \<le> (y::extreal) \<longleftrightarrow> x < y \<or> x = y" 

241 

242 
lemma extreal_infty_less[simp]: 

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

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

245 
by (cases x, simp_all) (cases x, simp_all) 

246 

247 
lemma extreal_infty_less_eq[simp]: 

248 
"\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>" 

249 
"x \<le> \<infinity> \<longleftrightarrow> x = \<infinity>" 

250 
by (auto simp add: less_eq_extreal_def) 

251 

252 
lemma extreal_less[simp]: 

253 
"extreal r < 0 \<longleftrightarrow> (r < 0)" 

254 
"0 < extreal r \<longleftrightarrow> (0 < r)" 

255 
"0 < \<infinity>" 

256 
"\<infinity> < 0" 

257 
by (simp_all add: zero_extreal_def) 

258 

259 
lemma extreal_less_eq[simp]: 

260 
"x \<le> \<infinity>" 

261 
"\<infinity> \<le> x" 

262 
"extreal r \<le> extreal p \<longleftrightarrow> r \<le> p" 

263 
"extreal r \<le> 0 \<longleftrightarrow> r \<le> 0" 

264 
"0 \<le> extreal r \<longleftrightarrow> 0 \<le> r" 

265 
by (auto simp add: less_eq_extreal_def zero_extreal_def) 

266 

267 
lemma extreal_infty_less_eq2: 

268 
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = \<infinity>" 

269 
"a \<le> b \<Longrightarrow> b = \<infinity> \<Longrightarrow> a = \<infinity>" 

270 
by simp_all 

271 

272 
instance 

273 
proof 

274 
fix x :: extreal show "x \<le> x" 

275 
by (cases x) simp_all 

276 
fix y :: extreal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 

277 
by (cases rule: extreal2_cases[of x y]) auto 

278 
show "x \<le> y \<or> y \<le> x " 

279 
by (cases rule: extreal2_cases[of x y]) auto 

280 
{ assume "x \<le> y" "y \<le> x" then show "x = y" 

281 
by (cases rule: extreal2_cases[of x y]) auto } 

282 
{ fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z" 

283 
by (cases rule: extreal3_cases[of x y z]) auto } 

284 
qed 

285 
end 

286 

41978  287 
instance extreal :: ordered_ab_semigroup_add 
288 
proof 

289 
fix a b c :: extreal assume "a \<le> b" then show "c + a \<le> c + b" 

290 
by (cases rule: extreal3_cases[of a b c]) auto 

291 
qed 

292 

41973  293 
lemma extreal_MInfty_lessI[intro, simp]: 
294 
"a \<noteq> \<infinity> \<Longrightarrow> \<infinity> < a" 

295 
by (cases a) auto 

296 

297 
lemma extreal_less_PInfty[intro, simp]: 

298 
"a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>" 

299 
by (cases a) auto 

300 

301 
lemma extreal_less_extreal_Ex: 

302 
fixes a b :: extreal 

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

304 
by (cases x) auto 

305 

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

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

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

308 
case (real r) then show ?thesis 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

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

311 

41973  312 
lemma extreal_add_mono: 
313 
fixes a b c d :: extreal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d" 

314 
using assms 

315 
apply (cases a) 

316 
apply (cases rule: extreal3_cases[of b c d], auto) 

317 
apply (cases rule: extreal3_cases[of b c d], auto) 

318 
done 

319 

320 
lemma extreal_minus_le_minus[simp]: 

321 
fixes a b :: extreal shows " a \<le>  b \<longleftrightarrow> b \<le> a" 

322 
by (cases rule: extreal2_cases[of a b]) auto 

323 

324 
lemma extreal_minus_less_minus[simp]: 

325 
fixes a b :: extreal shows " a <  b \<longleftrightarrow> b < a" 

326 
by (cases rule: extreal2_cases[of a b]) auto 

327 

328 
lemma extreal_le_real_iff: 

41976  329 
"x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> extreal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))" 
41973  330 
by (cases y) auto 
331 

332 
lemma real_le_extreal_iff: 

41976  333 
"real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> extreal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))" 
41973  334 
by (cases y) auto 
335 

336 
lemma extreal_less_real_iff: 

41976  337 
"x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> extreal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))" 
41973  338 
by (cases y) auto 
339 

340 
lemma real_less_extreal_iff: 

41976  341 
"real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < extreal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))" 
41973  342 
by (cases y) auto 
343 

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

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

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

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

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

348 

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

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

350 
fixes x :: extreal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

351 

41973  352 
lemmas real_of_extreal_ord_simps = 
353 
extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff 

354 

355 
lemma extreal_dense: 

356 
fixes x y :: extreal assumes "x < y" 

357 
shows "EX z. x < z & z < y" 

358 
proof  

359 
{ assume a: "x = (\<infinity>)" 

360 
{ assume "y = \<infinity>" hence ?thesis using a by (auto intro!: exI[of _ "0"]) } 

361 
moreover 

362 
{ assume "y ~= \<infinity>" 

363 
with `x < y` obtain r where r: "y = extreal r" by (cases y) auto 

364 
hence ?thesis using `x < y` a by (auto intro!: exI[of _ "extreal (r  1)"]) 

365 
} ultimately have ?thesis by auto 

366 
} 

367 
moreover 

368 
{ assume "x ~= (\<infinity>)" 

369 
with `x < y` obtain p where p: "x = extreal p" by (cases x) auto 

370 
{ assume "y = \<infinity>" hence ?thesis using `x < y` p 

371 
by (auto intro!: exI[of _ "extreal (p + 1)"]) } 

372 
moreover 

373 
{ assume "y ~= \<infinity>" 

374 
with `x < y` obtain r where r: "y = extreal r" by (cases y) auto 

375 
with p `x < y` have "p < r" by auto 

376 
with dense obtain z where "p < z" "z < r" by auto 

377 
hence ?thesis using r p by (auto intro!: exI[of _ "extreal z"]) 

378 
} ultimately have ?thesis by auto 

379 
} ultimately show ?thesis by auto 

380 
qed 

381 

382 
lemma extreal_dense2: 

383 
fixes x y :: extreal assumes "x < y" 

384 
shows "EX z. x < extreal z & extreal z < y" 

385 
by (metis extreal_dense[OF `x < y`] extreal_cases less_extreal.simps(2,3)) 

386 

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

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

388 
fixes a b c d :: extreal 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

389 
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

390 
shows "a + c < b + d" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

391 
using assms by (cases rule: extreal3_cases[case_product extreal_cases, of a b c d]) auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

392 

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

393 
lemma extreal_less_add: "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

395 

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

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

397 

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

398 
lemma extreal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::extreal)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

399 
by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_less_minus) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

400 

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

401 
lemma extreal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::extreal)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

402 
by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_le_minus) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

403 

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

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

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

406 

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

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

408 
fixes x :: extreal assumes "\<And>B. x \<le> extreal B" shows "x =  \<infinity>" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

410 
case (real r) with assms[of "r  1"] show ?thesis by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

411 
next case PInf with assms[of 0] show ?thesis by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

412 
next case MInf then show ?thesis by simp 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

414 

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

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

416 
fixes x :: extreal assumes "\<And>B. x \<ge> extreal B" shows "x = \<infinity>" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

418 
case (real r) with assms[of "r + 1"] show ?thesis by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

419 
next case MInf with assms[of 0] show ?thesis by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

420 
next case PInf then show ?thesis by simp 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

422 

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

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

424 
shows extreal_max[simp]: "extreal (max x y) = max (extreal x) (extreal y)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

425 
and extreal_min[simp]: "extreal (min x y) = min (extreal x) (extreal y)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

426 
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

427 

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

428 
lemma extreal_max_0: "max 0 (extreal r) = extreal (max 0 r)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

430 

41978  431 
lemma 
432 
fixes f :: "nat \<Rightarrow> extreal" 

433 
shows incseq_uminus[simp]: "incseq (\<lambda>x.  f x) \<longleftrightarrow> decseq f" 

434 
and decseq_uminus[simp]: "decseq (\<lambda>x.  f x) \<longleftrightarrow> incseq f" 

435 
unfolding decseq_def incseq_def by auto 

436 

437 
lemma extreal_add_nonneg_nonneg: 

438 
fixes a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 

439 
using add_mono[of 0 a 0 b] by simp 

440 

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

442 
by auto 

443 

444 
lemma incseq_setsumI: 

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

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

448 
proof (intro incseq_SucI) 

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

450 
using assms by (rule add_left_mono) 

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

452 
by auto 

453 
qed 

454 

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

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

456 
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

457 
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

458 
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

459 
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

460 

41973  461 
subsubsection "Multiplication" 
462 

41976  463 
instantiation extreal :: "{comm_monoid_mult, sgn}" 
41973  464 
begin 
465 

466 
definition "1 = extreal 1" 

467 

41976  468 
function sgn_extreal where 
469 
"sgn (extreal r) = extreal (sgn r)" 

470 
 "sgn \<infinity> = 1" 

471 
 "sgn (\<infinity>) = 1" 

472 
by (auto intro: extreal_cases) 

473 
termination proof qed (rule wf_empty) 

474 

41973  475 
function times_extreal where 
476 
"extreal r * extreal p = extreal (r * p)"  

477 
"extreal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)"  

478 
"\<infinity> * extreal r = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)"  

479 
"extreal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)"  

480 
"\<infinity> * extreal r = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)"  

481 
"\<infinity> * \<infinity> = \<infinity>"  

482 
"\<infinity> * \<infinity> = \<infinity>"  

483 
"\<infinity> * \<infinity> = \<infinity>"  

484 
"\<infinity> * \<infinity> = \<infinity>" 

485 
proof  

486 
case (goal1 P x) 

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

488 
ultimately show P by (cases rule: extreal2_cases[of a b]) auto 

489 
qed simp_all 

490 
termination by (relation "{}") simp 

491 

492 
instance 

493 
proof 

494 
fix a :: extreal show "1 * a = a" 

495 
by (cases a) (simp_all add: one_extreal_def) 

496 
fix b :: extreal show "a * b = b * a" 

497 
by (cases rule: extreal2_cases[of a b]) simp_all 

498 
fix c :: extreal show "a * b * c = a * (b * c)" 

499 
by (cases rule: extreal3_cases[of a b c]) 

500 
(simp_all add: zero_extreal_def zero_less_mult_iff) 

501 
qed 

502 
end 

503 

41976  504 
lemma abs_extreal_one[simp]: "\<bar>1\<bar> = (1::extreal)" 
505 
unfolding one_extreal_def by simp 

506 

41973  507 
lemma extreal_mult_zero[simp]: 
508 
fixes a :: extreal shows "a * 0 = 0" 

509 
by (cases a) (simp_all add: zero_extreal_def) 

510 

511 
lemma extreal_zero_mult[simp]: 

512 
fixes a :: extreal shows "0 * a = 0" 

513 
by (cases a) (simp_all add: zero_extreal_def) 

514 

515 
lemma extreal_m1_less_0[simp]: 

516 
"(1::extreal) < 0" 

517 
by (simp add: zero_extreal_def one_extreal_def) 

518 

519 
lemma extreal_zero_m1[simp]: 

520 
"1 \<noteq> (0::extreal)" 

521 
by (simp add: zero_extreal_def one_extreal_def) 

522 

523 
lemma extreal_times_0[simp]: 

524 
fixes x :: extreal shows "0 * x = 0" 

525 
by (cases x) (auto simp: zero_extreal_def) 

526 

527 
lemma extreal_times[simp]: 

528 
"1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1" 

529 
"1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1" 

530 
by (auto simp add: times_extreal_def one_extreal_def) 

531 

532 
lemma extreal_plus_1[simp]: 

533 
"1 + extreal r = extreal (r + 1)" "extreal r + 1 = extreal (r + 1)" 

534 
"1 + \<infinity> = \<infinity>" "\<infinity> + 1 = \<infinity>" 

535 
unfolding one_extreal_def by auto 

536 

537 
lemma extreal_zero_times[simp]: 

538 
fixes a b :: extreal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

539 
by (cases rule: extreal2_cases[of a b]) auto 

540 

541 
lemma extreal_mult_eq_PInfty[simp]: 

542 
shows "a * b = \<infinity> \<longleftrightarrow> 

543 
(a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>)" 

544 
by (cases rule: extreal2_cases[of a b]) auto 

545 

546 
lemma extreal_mult_eq_MInfty[simp]: 

547 
shows "a * b = \<infinity> \<longleftrightarrow> 

548 
(a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>)" 

549 
by (cases rule: extreal2_cases[of a b]) auto 

550 

551 
lemma extreal_0_less_1[simp]: "0 < (1::extreal)" 

552 
by (simp_all add: zero_extreal_def one_extreal_def) 

553 

554 
lemma extreal_zero_one[simp]: "0 \<noteq> (1::extreal)" 

555 
by (simp_all add: zero_extreal_def one_extreal_def) 

556 

557 
lemma extreal_mult_minus_left[simp]: 

558 
fixes a b :: extreal shows "a * b =  (a * b)" 

559 
by (cases rule: extreal2_cases[of a b]) auto 

560 

561 
lemma extreal_mult_minus_right[simp]: 

562 
fixes a b :: extreal shows "a * b =  (a * b)" 

563 
by (cases rule: extreal2_cases[of a b]) auto 

564 

565 
lemma extreal_mult_infty[simp]: 

566 
"a * \<infinity> = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 

567 
by (cases a) auto 

568 

569 
lemma extreal_infty_mult[simp]: 

570 
"\<infinity> * a = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 

571 
by (cases a) auto 

572 

573 
lemma extreal_mult_strict_right_mono: 

574 
assumes "a < b" and "0 < c" "c < \<infinity>" 

575 
shows "a * c < b * c" 

576 
using assms 

577 
by (cases rule: extreal3_cases[of a b c]) 

578 
(auto simp: zero_le_mult_iff extreal_less_PInfty) 

579 

580 
lemma extreal_mult_strict_left_mono: 

581 
"\<lbrakk> a < b ; 0 < c ; c < \<infinity>\<rbrakk> \<Longrightarrow> c * a < c * b" 

582 
using extreal_mult_strict_right_mono by (simp add: mult_commute[of c]) 

583 

584 
lemma extreal_mult_right_mono: 

585 
fixes a b c :: extreal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c" 

586 
using assms 

587 
apply (cases "c = 0") apply simp 

588 
by (cases rule: extreal3_cases[of a b c]) 

589 
(auto simp: zero_le_mult_iff extreal_less_PInfty) 

590 

591 
lemma extreal_mult_left_mono: 

592 
fixes a b c :: extreal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b" 

593 
using extreal_mult_right_mono by (simp add: mult_commute[of c]) 

594 

41978  595 
lemma zero_less_one_extreal[simp]: "0 \<le> (1::extreal)" 
596 
by (simp add: one_extreal_def zero_extreal_def) 

597 

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

598 
lemma extreal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: extreal)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

599 
by (cases rule: extreal2_cases[of a b]) (auto simp: mult_nonneg_nonneg) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

600 

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

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

602 
fixes r a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

603 
by (cases rule: extreal3_cases[of r a b]) (simp_all add: field_simps) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

604 

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

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

606 
fixes r a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

607 
by (cases rule: extreal3_cases[of r a b]) (simp_all add: field_simps) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

608 

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

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

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

611 
shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

612 
by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_le_0_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

613 

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

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

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

616 
shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

617 
by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_le_mult_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

618 

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

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

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

621 
shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

622 
by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_less_0_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

623 

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

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

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

626 
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

627 
by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_less_mult_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

628 

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

629 
lemma extreal_distrib: 
41978  630 
fixes a b c :: extreal 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

631 
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

632 
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

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

634 
by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

635 

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

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

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

638 
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

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

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

641 
{ assume a: "EX r. y = extreal r" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

642 
from this obtain r where r_def: "y = extreal r" by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

643 
{ 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

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

645 
{ assume "~(x=(\<infinity>))" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

646 
from this obtain p where p_def: "x = extreal p" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

647 
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

648 
{ fix e have "0 < e > p <= r + e" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

649 
using assms[rule_format, of "extreal e"] p_def r_def by auto } 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

650 
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

651 
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

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

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

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

655 
{ 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

656 
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

657 
} 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

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

659 

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

660 

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

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

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

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

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

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

666 
{ fix e :: extreal assume "e>0" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

667 
{ 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

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

669 
{ assume "e~=\<infinity>" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

670 
from this obtain r where "e = extreal r" using `e>0` apply (cases e) by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

671 
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

672 
} ultimately have "x<=y+e" by blast 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

673 
} from this show ?thesis using extreal_le_epsilon by auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

675 

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

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

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

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

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

680 
by (metis assms extreal.exhaust extreal_bot extreal_less_eq(1) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

681 
extreal_less_eq(2) order_refl uminus_extreal.simps(2)) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

682 

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

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

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

685 
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

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

687 
by (metis assms extreal_dense leD linorder_le_less_linear) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

688 

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

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

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

691 
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

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

693 
by (metis assms extreal_dense leD linorder_le_less_linear) 
41978  694 

695 
subsubsection {* Power *} 

696 

697 
instantiation extreal :: power 

698 
begin 

699 
primrec power_extreal where 

700 
"power_extreal x 0 = 1"  

701 
"power_extreal x (Suc n) = x * x ^ n" 

702 
instance .. 

703 
end 

704 

705 
lemma extreal_power[simp]: "(extreal x) ^ n = extreal (x^n)" 

706 
by (induct n) (auto simp: one_extreal_def) 

707 

708 
lemma extreal_power_PInf[simp]: "\<infinity> ^ n = (if n = 0 then 1 else \<infinity>)" 

709 
by (induct n) (auto simp: one_extreal_def) 

710 

711 
lemma extreal_power_uminus[simp]: 

712 
fixes x :: extreal 

713 
shows "( x) ^ n = (if even n then x ^ n else  (x^n))" 

714 
by (induct n) (auto simp: one_extreal_def) 

715 

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

716 
lemma extreal_power_number_of[simp]: 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

717 
"(number_of num :: extreal) ^ n = extreal (number_of num ^ n)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

718 
by (induct n) (auto simp: one_extreal_def) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

719 

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

720 
lemma zero_le_power_extreal[simp]: 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

721 
fixes a :: extreal assumes "0 \<le> a" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

722 
shows "0 \<le> a ^ n" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

723 
using assms by (induct n) (auto simp: extreal_zero_le_0_iff) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

724 

41973  725 
subsubsection {* Subtraction *} 
726 

727 
lemma extreal_minus_minus_image[simp]: 

728 
fixes S :: "extreal set" 

729 
shows "uminus ` uminus ` S = S" 

730 
by (auto simp: image_iff) 

731 

732 
lemma extreal_uminus_lessThan[simp]: 

733 
fixes a :: extreal shows "uminus ` {..<a} = {a<..}" 

734 
proof (safe intro!: image_eqI) 

735 
fix x assume "a < x" 

736 
then have " x <  ( a)" by (simp del: extreal_uminus_uminus) 

737 
then show " x < a" by simp 

738 
qed auto 

739 

740 
lemma extreal_uminus_greaterThan[simp]: 

741 
"uminus ` {(a::extreal)<..} = {..<a}" 

742 
by (metis extreal_uminus_lessThan extreal_uminus_uminus 

743 
extreal_minus_minus_image) 

744 

745 
instantiation extreal :: minus 

746 
begin 

747 
definition "x  y = x + (y::extreal)" 

748 
instance .. 

749 
end 

750 

751 
lemma extreal_minus[simp]: 

752 
"extreal r  extreal p = extreal (r  p)" 

753 
"\<infinity>  extreal r = \<infinity>" 

754 
"extreal r  \<infinity> = \<infinity>" 

755 
"\<infinity>  x = \<infinity>" 

756 
"\<infinity>  \<infinity> = \<infinity>" 

757 
"x  y = x + y" 

758 
"x  0 = x" 

759 
"0  x = x" 

760 
by (simp_all add: minus_extreal_def) 

761 

762 
lemma extreal_x_minus_x[simp]: 

41976  763 
"x  x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0)" 
41973  764 
by (cases x) simp_all 
765 

766 
lemma extreal_eq_minus_iff: 

767 
fixes x y z :: extreal 

768 
shows "x = z  y \<longleftrightarrow> 

41976  769 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y = z) \<and> 
41973  770 
(y = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 
771 
(y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and> 

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

773 
by (cases rule: extreal3_cases[of x y z]) auto 

774 

775 
lemma extreal_eq_minus: 

776 
fixes x y z :: extreal 

41976  777 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x = z  y \<longleftrightarrow> x + y = z" 
778 
by (auto simp: extreal_eq_minus_iff) 

41973  779 

780 
lemma extreal_less_minus_iff: 

781 
fixes x y z :: extreal 

782 
shows "x < z  y \<longleftrightarrow> 

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

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

41976  785 
(\<bar>y\<bar> \<noteq> \<infinity>\<longrightarrow> x + y < z)" 
41973  786 
by (cases rule: extreal3_cases[of x y z]) auto 
787 

788 
lemma extreal_less_minus: 

789 
fixes x y z :: extreal 

41976  790 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x < z  y \<longleftrightarrow> x + y < z" 
791 
by (auto simp: extreal_less_minus_iff) 

41973  792 

793 
lemma extreal_le_minus_iff: 

794 
fixes x y z :: extreal 

795 
shows "x \<le> z  y \<longleftrightarrow> 

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

41976  797 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)" 
41973  798 
by (cases rule: extreal3_cases[of x y z]) auto 
799 

800 
lemma extreal_le_minus: 

801 
fixes x y z :: extreal 

41976  802 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x \<le> z  y \<longleftrightarrow> x + y \<le> z" 
803 
by (auto simp: extreal_le_minus_iff) 

41973  804 

805 
lemma extreal_minus_less_iff: 

806 
fixes x y z :: extreal 

807 
shows "x  y < z \<longleftrightarrow> 

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

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

810 
by (cases rule: extreal3_cases[of x y z]) auto 

811 

812 
lemma extreal_minus_less: 

813 
fixes x y z :: extreal 

41976  814 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x  y < z \<longleftrightarrow> x < z + y" 
815 
by (auto simp: extreal_minus_less_iff) 

41973  816 

817 
lemma extreal_minus_le_iff: 

818 
fixes x y z :: extreal 

819 
shows "x  y \<le> z \<longleftrightarrow> 

820 
(y = \<infinity> \<longrightarrow> z = \<infinity>) \<and> 

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

41976  822 
(\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x \<le> z + y)" 
41973  823 
by (cases rule: extreal3_cases[of x y z]) auto 
824 

825 
lemma extreal_minus_le: 

826 
fixes x y z :: extreal 

41976  827 
shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x  y \<le> z \<longleftrightarrow> x \<le> z + y" 
828 
by (auto simp: extreal_minus_le_iff) 

41973  829 

830 
lemma extreal_minus_eq_minus_iff: 

831 
fixes a b c :: extreal 

832 
shows "a  b = a  c \<longleftrightarrow> 

833 
b = c \<or> a = \<infinity> \<or> (a = \<infinity> \<and> b \<noteq> \<infinity> \<and> c \<noteq> \<infinity>)" 

834 
by (cases rule: extreal3_cases[of a b c]) auto 

835 

836 
lemma extreal_add_le_add_iff: 

837 
"c + a \<le> c + b \<longleftrightarrow> 

838 
a \<le> b \<or> c = \<infinity> \<or> (c = \<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)" 

839 
by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps) 

840 

841 
lemma extreal_mult_le_mult_iff: 

41976  842 
"\<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)" 
41973  843 
by (cases rule: extreal3_cases[of a b c]) (simp_all add: mult_le_cancel_left) 
844 

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

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

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

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

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

849 
by (cases rule: extreal3_cases[case_product extreal_cases, of A B C D]) simp_all 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

850 

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

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

852 
"real (a  b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a  real b)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

854 

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

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

856 
fixes a b :: extreal shows "a \<le> b \<Longrightarrow> 0 \<le> b  a" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

858 

41973  859 
lemma extreal_between: 
860 
fixes x e :: extreal 

41976  861 
assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e" 
41973  862 
shows "x  e < x" "x < x + e" 
863 
using assms apply (cases x, cases e) apply auto 

864 
using assms by (cases x, cases e) auto 

865 

866 
subsubsection {* Division *} 

867 

868 
instantiation extreal :: inverse 

869 
begin 

870 

871 
function inverse_extreal where 

872 
"inverse (extreal r) = (if r = 0 then \<infinity> else extreal (inverse r))"  

873 
"inverse \<infinity> = 0"  

874 
"inverse (\<infinity>) = 0" 

875 
by (auto intro: extreal_cases) 

876 
termination by (relation "{}") simp 

877 

878 
definition "x / y = x * inverse (y :: extreal)" 

879 

880 
instance proof qed 

881 
end 

882 

883 
lemma extreal_inverse[simp]: 

884 
"inverse 0 = \<infinity>" 

885 
"inverse (1::extreal) = 1" 

886 
by (simp_all add: one_extreal_def zero_extreal_def) 

887 

888 
lemma extreal_divide[simp]: 

889 
"extreal r / extreal p = (if p = 0 then extreal r * \<infinity> else extreal (r / p))" 

890 
unfolding divide_extreal_def by (auto simp: divide_real_def) 

891 

892 
lemma extreal_divide_same[simp]: 

41976  893 
"x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)" 
41973  894 
by (cases x) 
895 
(simp_all add: divide_real_def divide_extreal_def one_extreal_def) 

896 

897 
lemma extreal_inv_inv[simp]: 

898 
"inverse (inverse x) = (if x \<noteq> \<infinity> then x else \<infinity>)" 

899 
by (cases x) auto 

900 

901 
lemma extreal_inverse_minus[simp]: 

902 
"inverse ( x) = (if x = 0 then \<infinity> else inverse x)" 

903 
by (cases x) simp_all 

904 

905 
lemma extreal_uminus_divide[simp]: 

906 
fixes x y :: extreal shows " x / y =  (x / y)" 

907 
unfolding divide_extreal_def by simp 

908 

909 
lemma extreal_divide_Infty[simp]: 

910 
"x / \<infinity> = 0" "x / \<infinity> = 0" 

911 
unfolding divide_extreal_def by simp_all 

912 

913 
lemma extreal_divide_one[simp]: 

914 
"x / 1 = (x::extreal)" 

915 
unfolding divide_extreal_def by simp 

916 

917 
lemma extreal_divide_extreal[simp]: 

918 
"\<infinity> / extreal r = (if 0 \<le> r then \<infinity> else \<infinity>)" 

919 
unfolding divide_extreal_def by simp 

920 

41978  921 
lemma zero_le_divide_extreal[simp]: 
922 
fixes a :: extreal assumes "0 \<le> a" "0 \<le> b" 

923 
shows "0 \<le> a / b" 

924 
using assms by (cases rule: extreal2_cases[of a b]) (auto simp: zero_le_divide_iff) 

925 

41973  926 
lemma extreal_le_divide_pos: 
927 
"x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z" 

928 
by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) 

929 

930 
lemma extreal_divide_le_pos: 

931 
"x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y" 

932 
by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) 

933 

934 
lemma extreal_le_divide_neg: 

935 
"x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y" 

936 
by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) 

937 

938 
lemma extreal_divide_le_neg: 

939 
"x < 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z" 

940 
by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) 

941 

942 
lemma extreal_inverse_antimono_strict: 

943 
fixes x y :: extreal 

944 
shows "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> inverse y < inverse x" 

945 
by (cases rule: extreal2_cases[of x y]) auto 

946 

947 
lemma extreal_inverse_antimono: 

948 
fixes x y :: extreal 

949 
shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x" 

950 
by (cases rule: extreal2_cases[of x y]) auto 

951 

952 
lemma inverse_inverse_Pinfty_iff[simp]: 

953 
"inverse x = \<infinity> \<longleftrightarrow> x = 0" 

954 
by (cases x) auto 

955 

956 
lemma extreal_inverse_eq_0: 

957 
"inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = \<infinity>" 

958 
by (cases x) auto 

959 

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

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

961 
fixes x :: extreal shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

963 

41973  964 
lemma extreal_mult_less_right: 
965 
assumes "b * a < c * a" "0 < a" "a < \<infinity>" 

966 
shows "b < c" 

967 
using assms 

968 
by (cases rule: extreal3_cases[of a b c]) 

969 
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff) 

970 

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

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

972 
"y \<noteq> 0 \<Longrightarrow> (x / y :: extreal) ^ n = x^n / y^n" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

973 
by (cases rule: extreal2_cases[of x y]) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

974 
(auto simp: one_extreal_def zero_extreal_def power_divide not_le 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

975 
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

976 

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

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

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

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

980 
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

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

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

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

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

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

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

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

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

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

990 
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

991 
fix z :: real assume "0 < z" and "z < 1" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

992 
with z[of "extreal z"] 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

993 
show "z * r \<le> p" using p r by (auto simp: zero_le_mult_iff one_extreal_def) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

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

995 
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

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

997 
qed simp 
41978  998 

41973  999 
subsection "Complete lattice" 
1000 

1001 
instantiation extreal :: lattice 

1002 
begin 

1003 
definition [simp]: "sup x y = (max x y :: extreal)" 

1004 
definition [simp]: "inf x y = (min x y :: extreal)" 

1005 
instance proof qed simp_all 

1006 
end 

1007 

1008 
instantiation extreal :: complete_lattice 

1009 
begin 

1010 

41976  1011 
definition "bot = \<infinity>" 
41973  1012 
definition "top = \<infinity>" 
1013 

1014 
definition "Sup S = (LEAST z. ALL x:S. x <= z :: extreal)" 

1015 
definition "Inf S = (GREATEST z. ALL x:S. z <= x :: extreal)" 

1016 

1017 
lemma extreal_complete_Sup: 

1018 
fixes S :: "extreal set" assumes "S \<noteq> {}" 

1019 
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)" 

1020 
proof cases 

1021 
assume "\<exists>x. \<forall>a\<in>S. a \<le> extreal x" 

1022 
then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> extreal y" by auto 

1023 
then have "\<infinity> \<notin> S" by force 

1024 
show ?thesis 

1025 
proof cases 

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

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

1028 
next 

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

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

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

1032 
by (auto simp: real_of_extreal_ord_simps) 

1033 
with reals_complete2[of "real ` (S  {\<infinity>})"] `x \<in> S  {\<infinity>}` 

1034 
obtain s where s: 

1035 
"\<forall>y\<in>S  {\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S  {\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z" 

1036 
by auto 

1037 
show ?thesis 

1038 
proof (safe intro!: exI[of _ "extreal s"]) 

1039 
fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> extreal s" 

1040 
proof (cases z) 

1041 
case (real r) 

1042 
then show ?thesis 

1043 
using s(1)[rule_format, of z] `z \<in> S` `z = extreal r` by auto 

1044 
qed auto 

1045 
next 

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

1047 
with `S \<noteq> {\<infinity>}` `S \<noteq> {}` show "extreal s \<le> z" 

1048 
proof (cases z) 

1049 
case (real u) 

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

1051 
by (intro s(2)[of u]) (auto simp: real_of_extreal_ord_simps) 

1052 
then show ?thesis using real by simp 

1053 
qed auto 

1054 
qed 

1055 
qed 

1056 
next 

1057 
assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> extreal x)" 

1058 
show ?thesis 

1059 
proof (safe intro!: exI[of _ \<infinity>]) 

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

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

1062 
proof (cases y) 

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

1064 
qed auto 

1065 
qed simp 

1066 
qed 

1067 

1068 
lemma extreal_complete_Inf: 

1069 
fixes S :: "extreal set" assumes "S ~= {}" 

1070 
shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) > z <= x)" 

1071 
proof 

1072 
def S1 == "uminus ` S" 

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

1074 
from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) > x <= z)" 

1075 
using extreal_complete_Sup[of S1] by auto 

1076 
{ fix z assume "ALL y:S. z <= y" 

1077 
hence "ALL y:S1. y <= z" unfolding S1_def by auto 

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

1079 
hence "z <= x" 

1080 
apply (subst extreal_uminus_uminus[symmetric]) 

1081 
unfolding extreal_minus_le_minus . } 

1082 
moreover have "(ALL y:S. x <= y)" 

1083 
using x_def unfolding S1_def 

1084 
apply simp 

1085 
apply (subst (3) extreal_uminus_uminus[symmetric]) 

1086 
unfolding extreal_minus_le_minus by simp 

1087 
ultimately show ?thesis by auto 

1088 
qed 

1089 

1090 
lemma extreal_complete_uminus_eq: 

1091 
fixes S :: "extreal set" 

1092 
shows "(\<forall>y\<in>uminus`S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>uminus`S. y \<le> z) \<longrightarrow> x \<le> z) 

1093 
\<longleftrightarrow> (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)" 

1094 
by simp (metis extreal_minus_le_minus extreal_uminus_uminus) 

1095 

1096 
lemma extreal_Sup_uminus_image_eq: 

1097 
fixes S :: "extreal set" 

1098 
shows "Sup (uminus ` S) =  Inf S" 

1099 
proof cases 

1100 
assume "S = {}" 

1101 
moreover have "(THE x. All (op \<le> x)) = (\<infinity>::extreal)" 

1102 
by (rule the_equality) (auto intro!: extreal_bot) 

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

1104 
by (rule some_equality) (auto intro!: extreal_top) 

1105 
ultimately show ?thesis unfolding Inf_extreal_def Sup_extreal_def 

1106 
Least_def Greatest_def GreatestM_def by simp 

1107 
next 

1108 
assume "S \<noteq> {}" 

1109 
with extreal_complete_Sup[of "uminus`S"] 

1110 
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)" 

1111 
unfolding extreal_complete_uminus_eq by auto 

1112 
show "Sup (uminus ` S) =  Inf S" 

1113 
unfolding Inf_extreal_def Greatest_def GreatestM_def 

1114 
proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) =  x"]) 

1115 
show "(\<forall>y\<in>S. x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x)" 

1116 
using x . 

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

1118 
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)" 

1119 
unfolding extreal_complete_uminus_eq by simp 

1120 
then show "Sup (uminus ` S) = x'" 

1121 
unfolding Sup_extreal_def extreal_uminus_eq_iff 

1122 
by (intro Least_equality) auto 

1123 
qed 

1124 
qed 

1125 

1126 
instance 

1127 
proof 

1128 
{ fix x :: extreal and A 

1129 
show "bot <= x" by (cases x) (simp_all add: bot_extreal_def) 

1130 
show "x <= top" by (simp add: top_extreal_def) } 

1131 

1132 
{ fix x :: extreal and A assume "x : A" 

1133 
with extreal_complete_Sup[of A] 

1134 
obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto 

1135 
hence "x <= s" using `x : A` by auto 

1136 
also have "... = Sup A" using s unfolding Sup_extreal_def 

1137 
by (auto intro!: Least_equality[symmetric]) 

1138 
finally show "x <= Sup A" . } 

1139 
note le_Sup = this 

1140 

1141 
{ fix x :: extreal and A assume *: "!!z. (z : A ==> z <= x)" 

1142 
show "Sup A <= x" 

1143 
proof (cases "A = {}") 

1144 
case True 

1145 
hence "Sup A = \<infinity>" unfolding Sup_extreal_def 

1146 
by (auto intro!: Least_equality) 

1147 
thus "Sup A <= x" by simp 

1148 
next 

1149 
case False 

1150 
with extreal_complete_Sup[of A] 

1151 
obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto 

1152 
hence "Sup A = s" 

1153 
unfolding Sup_extreal_def by (auto intro!: Least_equality) 

1154 
also have "s <= x" using * s by auto 

1155 
finally show "Sup A <= x" . 

1156 
qed } 

1157 
note Sup_le = this 

1158 

1159 
{ fix x :: extreal and A assume "x \<in> A" 

1160 
with le_Sup[of "x" "uminus`A"] show "Inf A \<le> x" 

1161 
unfolding extreal_Sup_uminus_image_eq by simp } 

1162 

1163 
{ fix x :: extreal and A assume *: "!!z. (z : A ==> x <= z)" 

1164 
with Sup_le[of "uminus`A" "x"] show "x \<le> Inf A" 

1165 
unfolding extreal_Sup_uminus_image_eq by force } 

1166 
qed 

1167 
end 

1168 

1169 
lemma extreal_SUPR_uminus: 

1170 
fixes f :: "'a => extreal" 

1171 
shows "(SUP i : R. (f i)) = (INF i : R. f i)" 

1172 
unfolding SUPR_def INFI_def 

1173 
using extreal_Sup_uminus_image_eq[of "f`R"] 

1174 
by (simp add: image_image) 

1175 

1176 
lemma extreal_INFI_uminus: 

1177 
fixes f :: "'a => extreal" 

1178 
shows "(INF i : R. (f i)) = (SUP i : R. f i)" 

1179 
using extreal_SUPR_uminus[of _ "\<lambda>x.  f x"] by simp 

1180 

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

1181 
lemma extreal_Inf_uminus_image_eq: "Inf (uminus ` S) =  Sup (S::extreal set)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1182 
using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1183 

41973  1184 
lemma extreal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: extreal set)" 
1185 
by (auto intro!: inj_onI) 

1186 

1187 
lemma extreal_image_uminus_shift: 

1188 
fixes X Y :: "extreal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y" 

1189 
proof 

1190 
assume "uminus ` X = Y" 

1191 
then have "uminus ` uminus ` X = uminus ` Y" 

1192 
by (simp add: inj_image_eq_iff) 

1193 
then show "X = uminus ` Y" by (simp add: image_image) 

1194 
qed (simp add: image_image) 

1195 

1196 
lemma Inf_extreal_iff: 

1197 
fixes z :: extreal 

1198 
shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x<y) <> Inf X < y" 

1199 
by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear 

1200 
order_less_le_trans) 

1201 

1202 
lemma Sup_eq_MInfty: 

1203 
fixes S :: "extreal set" shows "Sup S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}" 

1204 
proof 

1205 
assume a: "Sup S = \<infinity>" 

1206 
with complete_lattice_class.Sup_upper[of _ S] 

1207 
show "S={} \<or> S={\<infinity>}" by auto 

1208 
next 

1209 
assume "S={} \<or> S={\<infinity>}" then show "Sup S = \<infinity>" 

1210 
unfolding Sup_extreal_def by (auto intro!: Least_equality) 

1211 
qed 

1212 

1213 
lemma Inf_eq_PInfty: 

1214 
fixes S :: "extreal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}" 

1215 
using Sup_eq_MInfty[of "uminus`S"] 

1216 
unfolding extreal_Sup_uminus_image_eq extreal_image_uminus_shift by simp 

1217 

1218 
lemma Inf_eq_MInfty: "\<infinity> : S ==> Inf S = \<infinity>" 

1219 
unfolding Inf_extreal_def 

1220 
by (auto intro!: Greatest_equality) 

1221 

1222 
lemma Sup_eq_PInfty: "\<infinity> : S ==> Sup S = \<infinity>" 

1223 
unfolding Sup_extreal_def 

1224 
by (auto intro!: Least_equality) 

1225 

1226 
lemma extreal_SUPI: 

1227 
fixes x :: extreal 

1228 
assumes "!!i. i : A ==> f i <= x" 

1229 
assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y" 

1230 
shows "(SUP i:A. f i) = x" 

1231 
unfolding SUPR_def Sup_extreal_def 

1232 
using assms by (auto intro!: Least_equality) 

1233 

1234 
lemma extreal_INFI: 

1235 
fixes x :: extreal 

1236 
assumes "!!i. i : A ==> f i >= x" 

1237 
assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y" 

1238 
shows "(INF i:A. f i) = x" 

1239 
unfolding INFI_def Inf_extreal_def 

1240 
using assms by (auto intro!: Greatest_equality) 

1241 

1242 
lemma Sup_extreal_close: 

1243 
fixes e :: extreal 

41976  1244 
assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}" 
41973  1245 
shows "\<exists>x\<in>S. Sup S  e < x" 
41976  1246 
using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1]) 
41973  1247 

1248 
lemma Inf_extreal_close: 

41976  1249 
fixes e :: extreal assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>" "0 < e" 
41973  1250 
shows "\<exists>x\<in>X. x < Inf X + e" 
1251 
proof (rule Inf_less_iff[THEN iffD1]) 

1252 
show "Inf X < Inf X + e" using assms 

41976  1253 
by (cases e) auto 
41973  1254 
qed 
1255 

1256 
lemma Sup_eq_top_iff: 

1257 
fixes A :: "'a::{complete_lattice, linorder} set" 

1258 
shows "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)" 

1259 
proof 

1260 
assume *: "Sup A = top" 

1261 
show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding *[symmetric] 

1262 
proof (intro allI impI) 

1263 
fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i" 

1264 
unfolding less_Sup_iff by auto 

1265 
qed 

1266 
next 

1267 
assume *: "\<forall>x<top. \<exists>i\<in>A. x < i" 

1268 
show "Sup A = top" 

1269 
proof (rule ccontr) 

1270 
assume "Sup A \<noteq> top" 

1271 
with top_greatest[of "Sup A"] 

1272 
have "Sup A < top" unfolding le_less by auto 

1273 
then have "Sup A < Sup A" 

1274 
using * unfolding less_Sup_iff by auto 

1275 
then show False by auto 

1276 
qed 

1277 
qed 

1278 

1279 
lemma SUP_eq_top_iff: 

1280 
fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}" 

1281 
shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)" 

1282 
unfolding SUPR_def Sup_eq_top_iff by auto 

1283 

1284 
lemma SUP_nat_Infty: "(SUP i::nat. extreal (real i)) = \<infinity>" 

1285 
proof  

1286 
{ fix x assume "x \<noteq> \<infinity>" 

1287 
then have "\<exists>k::nat. x < extreal (real k)" 

1288 
proof (cases x) 

1289 
case MInf then show ?thesis by (intro exI[of _ 0]) auto 

1290 
next 

1291 
case (real r) 

1292 
moreover obtain k :: nat where "r < real k" 

1293 
using ex_less_of_nat by (auto simp: real_eq_of_nat) 

1294 
ultimately show ?thesis by auto 

1295 
qed simp } 

1296 
then show ?thesis 

1297 
using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. extreal (real n)"] 

1298 
by (auto simp: top_extreal_def) 

1299 
qed 

1300 

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

1301 
lemma extreal_le_Sup: 
41973  1302 
fixes x :: extreal 
1303 
shows "(x <= (SUP i:A. f i)) <> (ALL y. y < x > (EX i. i : A & y <= f i))" 

1304 
(is "?lhs <> ?rhs") 

1305 
proof 

1306 
{ assume "?rhs" 

1307 
{ assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le) 

1308 
from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using extreal_dense by auto 

1309 
from this obtain i where "i : A & y <= f i" using `?rhs` by auto 

1310 
hence "y <= (SUP i:A. f i)" using le_SUPI[of i A f] by auto 

1311 
hence False using y_def by auto 

1312 
} hence "?lhs" by auto 

1313 
} 

1314 
moreover 

1315 
{ assume "?lhs" hence "?rhs" 

1316 
by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff 

1317 
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8)) 

1318 
} ultimately show ?thesis by auto 

1319 
qed 

1320 

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

1321 
lemma extreal_Inf_le: 
41973  1322 
fixes x :: extreal 
1323 
shows "((INF i:A. f i) <= x) <> (ALL y. x < y > (EX i. i : A & f i <= y))" 

1324 
(is "?lhs <> ?rhs") 

1325 
proof 

1326 
{ assume "?rhs" 

1327 
{ assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le) 

1328 
from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using extreal_dense by auto 

1329 
from this obtain i where "i : A & f i <= y" using `?rhs` by auto 

1330 
hence "(INF i:A. f i) <= y" using INF_leI[of i A f] by auto 

1331 
hence False using y_def by auto 

1332 
} hence "?lhs" by auto 

1333 
} 

1334 
moreover 

1335 
{ assume "?lhs" hence "?rhs" 

1336 
by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff 

1337 
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8)) 

1338 
} ultimately show ?thesis by auto 

1339 
qed 

1340 

1341 
lemma Inf_less: 

1342 
fixes x :: extreal 

1343 
assumes "(INF i:A. f i) < x" 

1344 
shows "EX i. i : A & f i <= x" 

1345 
proof(rule ccontr) 

1346 
assume "~ (EX i. i : A & f i <= x)" 

1347 
hence "ALL i:A. f i > x" by auto 

1348 
hence "(INF i:A. f i) >= x" apply (subst le_INFI) by auto 

1349 
thus False using assms by auto 

1350 
qed 

1351 

1352 
lemma same_INF: 

1353 
assumes "ALL e:A. f e = g e" 

1354 
shows "(INF e:A. f e) = (INF e:A. g e)" 

1355 
proof 

1356 
have "f ` A = g ` A" unfolding image_def using assms by auto 

1357 
thus ?thesis unfolding INFI_def by auto 

1358 
qed 

1359 

1360 
lemma same_SUP: 

1361 
assumes "ALL e:A. f e = g e" 

1362 
shows "(SUP e:A. f e) = (SUP e:A. g e)" 

1363 
proof 

1364 
have "f ` A = g ` A" unfolding image_def using assms by auto 

1365 
thus ?thesis unfolding SUPR_def by auto 

1366 
qed 

1367 

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

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

1369 
assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<le> g j" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1370 
assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<le> f i" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelz 