1.1 --- a/src/HOL/Library/Extended_Real.thy Wed Sep 25 11:12:59 2013 +0200
1.2 +++ b/src/HOL/Library/Extended_Real.thy Wed Sep 25 12:42:56 2013 +0200
1.3 @@ -24,23 +24,29 @@
1.4
1.5 instantiation ereal :: uminus
1.6 begin
1.7 - fun uminus_ereal where
1.8 - "- (ereal r) = ereal (- r)"
1.9 - | "- PInfty = MInfty"
1.10 - | "- MInfty = PInfty"
1.11 - instance ..
1.12 +
1.13 +fun uminus_ereal where
1.14 + "- (ereal r) = ereal (- r)"
1.15 +| "- PInfty = MInfty"
1.16 +| "- MInfty = PInfty"
1.17 +
1.18 +instance ..
1.19 +
1.20 end
1.21
1.22 instantiation ereal :: infinity
1.23 begin
1.24 - definition "(\<infinity>::ereal) = PInfty"
1.25 - instance ..
1.26 +
1.27 +definition "(\<infinity>::ereal) = PInfty"
1.28 +instance ..
1.29 +
1.30 end
1.31
1.32 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
1.33
1.34 lemma ereal_uminus_uminus[simp]:
1.35 - fixes a :: ereal shows "- (- a) = a"
1.36 + fixes a :: ereal
1.37 + shows "- (- a) = a"
1.38 by (cases a) simp_all
1.39
1.40 lemma
1.41 @@ -59,7 +65,7 @@
1.42
1.43 lemma [code_unfold]:
1.44 "\<infinity> = PInfty"
1.45 - "-PInfty = MInfty"
1.46 + "- PInfty = MInfty"
1.47 by simp_all
1.48
1.49 lemma inj_ereal[simp]: "inj_on ereal A"
1.50 @@ -76,77 +82,97 @@
1.51 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
1.52
1.53 lemma ereal_uminus_eq_iff[simp]:
1.54 - fixes a b :: ereal shows "-a = -b \<longleftrightarrow> a = b"
1.55 + fixes a b :: ereal
1.56 + shows "-a = -b \<longleftrightarrow> a = b"
1.57 by (cases rule: ereal2_cases[of a b]) simp_all
1.58
1.59 function of_ereal :: "ereal \<Rightarrow> real" where
1.60 -"of_ereal (ereal r) = r" |
1.61 -"of_ereal \<infinity> = 0" |
1.62 -"of_ereal (-\<infinity>) = 0"
1.63 + "of_ereal (ereal r) = r"
1.64 +| "of_ereal \<infinity> = 0"
1.65 +| "of_ereal (-\<infinity>) = 0"
1.66 by (auto intro: ereal_cases)
1.67 -termination proof qed (rule wf_empty)
1.68 +termination by default (rule wf_empty)
1.69
1.70 defs (overloaded)
1.71 real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"
1.72
1.73 lemma real_of_ereal[simp]:
1.74 - "real (- x :: ereal) = - (real x)"
1.75 - "real (ereal r) = r"
1.76 - "real (\<infinity>::ereal) = 0"
1.77 + "real (- x :: ereal) = - (real x)"
1.78 + "real (ereal r) = r"
1.79 + "real (\<infinity>::ereal) = 0"
1.80 by (cases x) (simp_all add: real_of_ereal_def)
1.81
1.82 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
1.83 proof safe
1.84 - fix x assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
1.85 - then show "x = -\<infinity>" by (cases x) auto
1.86 + fix x
1.87 + assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
1.88 + then show "x = -\<infinity>"
1.89 + by (cases x) auto
1.90 qed auto
1.91
1.92 lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"
1.93 proof safe
1.94 - fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
1.95 + fix x :: ereal
1.96 + show "x \<in> range uminus"
1.97 + by (intro image_eqI[of _ _ "-x"]) auto
1.98 qed auto
1.99
1.100 instantiation ereal :: abs
1.101 begin
1.102 - function abs_ereal where
1.103 - "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
1.104 - | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
1.105 - | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
1.106 - by (auto intro: ereal_cases)
1.107 - termination proof qed (rule wf_empty)
1.108 - instance ..
1.109 +
1.110 +function abs_ereal where
1.111 + "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
1.112 +| "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
1.113 +| "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
1.114 +by (auto intro: ereal_cases)
1.115 +termination proof qed (rule wf_empty)
1.116 +
1.117 +instance ..
1.118 +
1.119 end
1.120
1.121 -lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
1.122 +lemma abs_eq_infinity_cases[elim!]:
1.123 + fixes x :: ereal
1.124 + assumes "\<bar>x\<bar> = \<infinity>"
1.125 + obtains "x = \<infinity>" | "x = -\<infinity>"
1.126 + using assms by (cases x) auto
1.127 +
1.128 +lemma abs_neq_infinity_cases[elim!]:
1.129 + fixes x :: ereal
1.130 + assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.131 + obtains r where "x = ereal r"
1.132 + using assms by (cases x) auto
1.133 +
1.134 +lemma abs_ereal_uminus[simp]:
1.135 + fixes x :: ereal
1.136 + shows "\<bar>- x\<bar> = \<bar>x\<bar>"
1.137 by (cases x) auto
1.138
1.139 -lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
1.140 - by (cases x) auto
1.141 +lemma ereal_infinity_cases:
1.142 + fixes a :: ereal
1.143 + shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
1.144 + by auto
1.145
1.146 -lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
1.147 - by (cases x) auto
1.148 -
1.149 -lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
1.150 - by auto
1.151
1.152 subsubsection "Addition"
1.153
1.154 -instantiation ereal :: "{one, comm_monoid_add}"
1.155 +instantiation ereal :: "{one,comm_monoid_add}"
1.156 begin
1.157
1.158 definition "0 = ereal 0"
1.159 definition "1 = ereal 1"
1.160
1.161 function plus_ereal where
1.162 -"ereal r + ereal p = ereal (r + p)" |
1.163 -"\<infinity> + a = (\<infinity>::ereal)" |
1.164 -"a + \<infinity> = (\<infinity>::ereal)" |
1.165 -"ereal r + -\<infinity> = - \<infinity>" |
1.166 -"-\<infinity> + ereal p = -(\<infinity>::ereal)" |
1.167 -"-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
1.168 + "ereal r + ereal p = ereal (r + p)"
1.169 +| "\<infinity> + a = (\<infinity>::ereal)"
1.170 +| "a + \<infinity> = (\<infinity>::ereal)"
1.171 +| "ereal r + -\<infinity> = - \<infinity>"
1.172 +| "-\<infinity> + ereal p = -(\<infinity>::ereal)"
1.173 +| "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
1.174 proof -
1.175 case (goal1 P x)
1.176 - then obtain a b where "x = (a, b)" by (cases x) auto
1.177 + then obtain a b where "x = (a, b)"
1.178 + by (cases x) auto
1.179 with goal1 show P
1.180 by (cases rule: ereal2_cases[of a b]) auto
1.181 qed auto
1.182 @@ -172,6 +198,7 @@
1.183 show "a + b + c = a + (b + c)"
1.184 by (cases rule: ereal3_cases[of a b c]) simp_all
1.185 qed
1.186 +
1.187 end
1.188
1.189 instance ereal :: numeral ..
1.190 @@ -182,35 +209,37 @@
1.191 lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)"
1.192 unfolding zero_ereal_def abs_ereal.simps by simp
1.193
1.194 -lemma ereal_uminus_zero[simp]:
1.195 - "- 0 = (0::ereal)"
1.196 +lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)"
1.197 by (simp add: zero_ereal_def)
1.198
1.199 lemma ereal_uminus_zero_iff[simp]:
1.200 - fixes a :: ereal shows "-a = 0 \<longleftrightarrow> a = 0"
1.201 + fixes a :: ereal
1.202 + shows "-a = 0 \<longleftrightarrow> a = 0"
1.203 by (cases a) simp_all
1.204
1.205 lemma ereal_plus_eq_PInfty[simp]:
1.206 - fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
1.207 + fixes a b :: ereal
1.208 + shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
1.209 by (cases rule: ereal2_cases[of a b]) auto
1.210
1.211 lemma ereal_plus_eq_MInfty[simp]:
1.212 - fixes a b :: ereal shows "a + b = -\<infinity> \<longleftrightarrow>
1.213 - (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
1.214 + fixes a b :: ereal
1.215 + shows "a + b = -\<infinity> \<longleftrightarrow> (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
1.216 by (cases rule: ereal2_cases[of a b]) auto
1.217
1.218 lemma ereal_add_cancel_left:
1.219 - fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
1.220 - shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
1.221 + fixes a b :: ereal
1.222 + assumes "a \<noteq> -\<infinity>"
1.223 + shows "a + b = a + c \<longleftrightarrow> a = \<infinity> \<or> b = c"
1.224 using assms by (cases rule: ereal3_cases[of a b c]) auto
1.225
1.226 lemma ereal_add_cancel_right:
1.227 - fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
1.228 - shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
1.229 + fixes a b :: ereal
1.230 + assumes "a \<noteq> -\<infinity>"
1.231 + shows "b + a = c + a \<longleftrightarrow> a = \<infinity> \<or> b = c"
1.232 using assms by (cases rule: ereal3_cases[of a b c]) auto
1.233
1.234 -lemma ereal_real:
1.235 - "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
1.236 +lemma ereal_real: "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
1.237 by (cases x) simp_all
1.238
1.239 lemma real_of_ereal_add:
1.240 @@ -219,6 +248,7 @@
1.241 (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)"
1.242 by (cases rule: ereal2_cases[of a b]) auto
1.243
1.244 +
1.245 subsubsection "Linear order on @{typ ereal}"
1.246
1.247 instantiation ereal :: linorder
1.248 @@ -250,7 +280,7 @@
1.249 lemma ereal_infty_less_eq[simp]:
1.250 fixes x :: ereal
1.251 shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
1.252 - "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
1.253 + and "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
1.254 by (auto simp add: less_eq_ereal_def)
1.255
1.256 lemma ereal_less[simp]:
1.257 @@ -282,10 +312,16 @@
1.258 by (cases rule: ereal2_cases[of x y]) auto
1.259 show "x \<le> y \<or> y \<le> x "
1.260 by (cases rule: ereal2_cases[of x y]) auto
1.261 - { assume "x \<le> y" "y \<le> x" then show "x = y"
1.262 - by (cases rule: ereal2_cases[of x y]) auto }
1.263 - { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
1.264 - by (cases rule: ereal3_cases[of x y z]) auto }
1.265 + {
1.266 + assume "x \<le> y" "y \<le> x"
1.267 + then show "x = y"
1.268 + by (cases rule: ereal2_cases[of x y]) auto
1.269 + }
1.270 + {
1.271 + assume "x \<le> y" "y \<le> z"
1.272 + then show "x \<le> z"
1.273 + by (cases rule: ereal3_cases[of x y z]) auto
1.274 + }
1.275 qed
1.276
1.277 end
1.278 @@ -298,20 +334,25 @@
1.279
1.280 instance ereal :: ordered_ab_semigroup_add
1.281 proof
1.282 - fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
1.283 + fix a b c :: ereal
1.284 + assume "a \<le> b"
1.285 + then show "c + a \<le> c + b"
1.286 by (cases rule: ereal3_cases[of a b c]) auto
1.287 qed
1.288
1.289 lemma real_of_ereal_positive_mono:
1.290 - fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
1.291 + fixes x y :: ereal
1.292 + shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real x \<le> real y"
1.293 by (cases rule: ereal2_cases[of x y]) auto
1.294
1.295 lemma ereal_MInfty_lessI[intro, simp]:
1.296 - fixes a :: ereal shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
1.297 + fixes a :: ereal
1.298 + shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
1.299 by (cases a) auto
1.300
1.301 lemma ereal_less_PInfty[intro, simp]:
1.302 - fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
1.303 + fixes a :: ereal
1.304 + shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
1.305 by (cases a) auto
1.306
1.307 lemma ereal_less_ereal_Ex:
1.308 @@ -321,12 +362,16 @@
1.309
1.310 lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))"
1.311 proof (cases x)
1.312 - case (real r) then show ?thesis
1.313 + case (real r)
1.314 + then show ?thesis
1.315 using reals_Archimedean2[of r] by simp
1.316 qed simp_all
1.317
1.318 lemma ereal_add_mono:
1.319 - fixes a b c d :: ereal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d"
1.320 + fixes a b c d :: ereal
1.321 + assumes "a \<le> b"
1.322 + and "c \<le> d"
1.323 + shows "a + c \<le> b + d"
1.324 using assms
1.325 apply (cases a)
1.326 apply (cases rule: ereal3_cases[of b c d], auto)
1.327 @@ -334,31 +379,34 @@
1.328 done
1.329
1.330 lemma ereal_minus_le_minus[simp]:
1.331 - fixes a b :: ereal shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
1.332 + fixes a b :: ereal
1.333 + shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
1.334 by (cases rule: ereal2_cases[of a b]) auto
1.335
1.336 lemma ereal_minus_less_minus[simp]:
1.337 - fixes a b :: ereal shows "- a < - b \<longleftrightarrow> b < a"
1.338 + fixes a b :: ereal
1.339 + shows "- a < - b \<longleftrightarrow> b < a"
1.340 by (cases rule: ereal2_cases[of a b]) auto
1.341
1.342 lemma ereal_le_real_iff:
1.343 - "x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))"
1.344 + "x \<le> real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0)"
1.345 by (cases y) auto
1.346
1.347 lemma real_le_ereal_iff:
1.348 - "real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))"
1.349 + "real y \<le> x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x)"
1.350 by (cases y) auto
1.351
1.352 lemma ereal_less_real_iff:
1.353 - "x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))"
1.354 + "x < real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)"
1.355 by (cases y) auto
1.356
1.357 lemma real_less_ereal_iff:
1.358 - "real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"
1.359 + "real y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
1.360 by (cases y) auto
1.361
1.362 lemma real_of_ereal_pos:
1.363 - fixes x :: ereal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
1.364 + fixes x :: ereal
1.365 + shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
1.366
1.367 lemmas real_of_ereal_ord_simps =
1.368 ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff
1.369 @@ -372,35 +420,44 @@
1.370 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
1.371 by (cases x) auto
1.372
1.373 -lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)"
1.374 +lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
1.375 by (cases x) auto
1.376
1.377 lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"
1.378 by (cases x) auto
1.379
1.380 lemma zero_less_real_of_ereal:
1.381 - fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)"
1.382 + fixes x :: ereal
1.383 + shows "0 < real x \<longleftrightarrow> 0 < x \<and> x \<noteq> \<infinity>"
1.384 by (cases x) auto
1.385
1.386 lemma ereal_0_le_uminus_iff[simp]:
1.387 - fixes a :: ereal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
1.388 + fixes a :: ereal
1.389 + shows "0 \<le> - a \<longleftrightarrow> a \<le> 0"
1.390 by (cases rule: ereal2_cases[of a]) auto
1.391
1.392 lemma ereal_uminus_le_0_iff[simp]:
1.393 - fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
1.394 + fixes a :: ereal
1.395 + shows "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
1.396 by (cases rule: ereal2_cases[of a]) auto
1.397
1.398 lemma ereal_add_strict_mono:
1.399 fixes a b c d :: ereal
1.400 - assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
1.401 + assumes "a = b"
1.402 + and "0 \<le> a"
1.403 + and "a \<noteq> \<infinity>"
1.404 + and "c < d"
1.405 shows "a + c < b + d"
1.406 - using assms by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
1.407 + using assms
1.408 + by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
1.409
1.410 -lemma ereal_less_add:
1.411 - fixes a b c :: ereal shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
1.412 +lemma ereal_less_add:
1.413 + fixes a b c :: ereal
1.414 + shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
1.415 by (cases rule: ereal2_cases[of b c]) auto
1.416
1.417 -lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)" by auto
1.418 +lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)"
1.419 + by auto
1.420
1.421 lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
1.422 by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
1.423 @@ -412,23 +469,39 @@
1.424 ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder
1.425
1.426 lemma ereal_bot:
1.427 - fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"
1.428 + fixes x :: ereal
1.429 + assumes "\<And>B. x \<le> ereal B"
1.430 + shows "x = - \<infinity>"
1.431 proof (cases x)
1.432 - case (real r) with assms[of "r - 1"] show ?thesis by auto
1.433 + case (real r)
1.434 + with assms[of "r - 1"] show ?thesis
1.435 + by auto
1.436 next
1.437 - case PInf with assms[of 0] show ?thesis by auto
1.438 + case PInf
1.439 + with assms[of 0] show ?thesis
1.440 + by auto
1.441 next
1.442 - case MInf then show ?thesis by simp
1.443 + case MInf
1.444 + then show ?thesis
1.445 + by simp
1.446 qed
1.447
1.448 lemma ereal_top:
1.449 - fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"
1.450 + fixes x :: ereal
1.451 + assumes "\<And>B. x \<ge> ereal B"
1.452 + shows "x = \<infinity>"
1.453 proof (cases x)
1.454 - case (real r) with assms[of "r + 1"] show ?thesis by auto
1.455 + case (real r)
1.456 + with assms[of "r + 1"] show ?thesis
1.457 + by auto
1.458 next
1.459 - case MInf with assms[of 0] show ?thesis by auto
1.460 + case MInf
1.461 + with assms[of 0] show ?thesis
1.462 + by auto
1.463 next
1.464 - case PInf then show ?thesis by simp
1.465 + case PInf
1.466 + then show ?thesis
1.467 + by simp
1.468 qed
1.469
1.470 lemma
1.471 @@ -449,32 +522,36 @@
1.472 unfolding incseq_def by auto
1.473
1.474 lemma ereal_add_nonneg_nonneg:
1.475 - fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
1.476 + fixes a b :: ereal
1.477 + shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
1.478 using add_mono[of 0 a 0 b] by simp
1.479
1.480 -lemma image_eqD: "f ` A = B \<Longrightarrow> (\<forall>x\<in>A. f x \<in> B)"
1.481 +lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
1.482 by auto
1.483
1.484 lemma incseq_setsumI:
1.485 - fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
1.486 + fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
1.487 assumes "\<And>i. 0 \<le> f i"
1.488 shows "incseq (\<lambda>i. setsum f {..< i})"
1.489 proof (intro incseq_SucI)
1.490 - fix n have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
1.491 + fix n
1.492 + have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
1.493 using assms by (rule add_left_mono)
1.494 then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
1.495 by auto
1.496 qed
1.497
1.498 lemma incseq_setsumI2:
1.499 - fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
1.500 + fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
1.501 assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
1.502 shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
1.503 - using assms unfolding incseq_def by (auto intro: setsum_mono)
1.504 + using assms
1.505 + unfolding incseq_def by (auto intro: setsum_mono)
1.506 +
1.507
1.508 subsubsection "Multiplication"
1.509
1.510 -instantiation ereal :: "{comm_monoid_mult, sgn}"
1.511 +instantiation ereal :: "{comm_monoid_mult,sgn}"
1.512 begin
1.513
1.514 function sgn_ereal :: "ereal \<Rightarrow> ereal" where
1.515 @@ -482,28 +559,31 @@
1.516 | "sgn (\<infinity>::ereal) = 1"
1.517 | "sgn (-\<infinity>::ereal) = -1"
1.518 by (auto intro: ereal_cases)
1.519 -termination proof qed (rule wf_empty)
1.520 +termination by default (rule wf_empty)
1.521
1.522 function times_ereal where
1.523 -"ereal r * ereal p = ereal (r * p)" |
1.524 -"ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
1.525 -"\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
1.526 -"ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
1.527 -"-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
1.528 -"(\<infinity>::ereal) * \<infinity> = \<infinity>" |
1.529 -"-(\<infinity>::ereal) * \<infinity> = -\<infinity>" |
1.530 -"(\<infinity>::ereal) * -\<infinity> = -\<infinity>" |
1.531 -"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
1.532 + "ereal r * ereal p = ereal (r * p)"
1.533 +| "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
1.534 +| "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
1.535 +| "ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
1.536 +| "-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
1.537 +| "(\<infinity>::ereal) * \<infinity> = \<infinity>"
1.538 +| "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
1.539 +| "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
1.540 +| "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
1.541 proof -
1.542 case (goal1 P x)
1.543 - then obtain a b where "x = (a, b)" by (cases x) auto
1.544 - with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
1.545 + then obtain a b where "x = (a, b)"
1.546 + by (cases x) auto
1.547 + with goal1 show P
1.548 + by (cases rule: ereal2_cases[of a b]) auto
1.549 qed simp_all
1.550 termination by (relation "{}") simp
1.551
1.552 instance
1.553 proof
1.554 - fix a b c :: ereal show "1 * a = a"
1.555 + fix a b c :: ereal
1.556 + show "1 * a = a"
1.557 by (cases a) (simp_all add: one_ereal_def)
1.558 show "a * b = b * a"
1.559 by (cases rule: ereal2_cases[of a b]) simp_all
1.560 @@ -511,36 +591,39 @@
1.561 by (cases rule: ereal3_cases[of a b c])
1.562 (simp_all add: zero_ereal_def zero_less_mult_iff)
1.563 qed
1.564 +
1.565 end
1.566
1.567 lemma real_ereal_1[simp]: "real (1::ereal) = 1"
1.568 unfolding one_ereal_def by simp
1.569
1.570 lemma real_of_ereal_le_1:
1.571 - fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
1.572 + fixes a :: ereal
1.573 + shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
1.574 by (cases a) (auto simp: one_ereal_def)
1.575
1.576 lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)"
1.577 unfolding one_ereal_def by simp
1.578
1.579 lemma ereal_mult_zero[simp]:
1.580 - fixes a :: ereal shows "a * 0 = 0"
1.581 + fixes a :: ereal
1.582 + shows "a * 0 = 0"
1.583 by (cases a) (simp_all add: zero_ereal_def)
1.584
1.585 lemma ereal_zero_mult[simp]:
1.586 - fixes a :: ereal shows "0 * a = 0"
1.587 + fixes a :: ereal
1.588 + shows "0 * a = 0"
1.589 by (cases a) (simp_all add: zero_ereal_def)
1.590
1.591 -lemma ereal_m1_less_0[simp]:
1.592 - "-(1::ereal) < 0"
1.593 +lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
1.594 by (simp add: zero_ereal_def one_ereal_def)
1.595
1.596 -lemma ereal_zero_m1[simp]:
1.597 - "1 \<noteq> (0::ereal)"
1.598 +lemma ereal_zero_m1[simp]: "1 \<noteq> (0::ereal)"
1.599 by (simp add: zero_ereal_def one_ereal_def)
1.600
1.601 lemma ereal_times_0[simp]:
1.602 - fixes x :: ereal shows "0 * x = 0"
1.603 + fixes x :: ereal
1.604 + shows "0 * x = 0"
1.605 by (cases x) (auto simp: zero_ereal_def)
1.606
1.607 lemma ereal_times[simp]:
1.608 @@ -549,21 +632,24 @@
1.609 by (auto simp add: times_ereal_def one_ereal_def)
1.610
1.611 lemma ereal_plus_1[simp]:
1.612 - "1 + ereal r = ereal (r + 1)" "ereal r + 1 = ereal (r + 1)"
1.613 - "1 + -(\<infinity>::ereal) = -\<infinity>" "-(\<infinity>::ereal) + 1 = -\<infinity>"
1.614 + "1 + ereal r = ereal (r + 1)"
1.615 + "ereal r + 1 = ereal (r + 1)"
1.616 + "1 + -(\<infinity>::ereal) = -\<infinity>"
1.617 + "-(\<infinity>::ereal) + 1 = -\<infinity>"
1.618 unfolding one_ereal_def by auto
1.619
1.620 lemma ereal_zero_times[simp]:
1.621 - fixes a b :: ereal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.622 + fixes a b :: ereal
1.623 + shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.624 by (cases rule: ereal2_cases[of a b]) auto
1.625
1.626 lemma ereal_mult_eq_PInfty[simp]:
1.627 - shows "a * b = (\<infinity>::ereal) \<longleftrightarrow>
1.628 + "a * b = (\<infinity>::ereal) \<longleftrightarrow>
1.629 (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
1.630 by (cases rule: ereal2_cases[of a b]) auto
1.631
1.632 lemma ereal_mult_eq_MInfty[simp]:
1.633 - shows "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
1.634 + "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
1.635 (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
1.636 by (cases rule: ereal2_cases[of a b]) auto
1.637
1.638 @@ -574,11 +660,13 @@
1.639 by (simp_all add: zero_ereal_def one_ereal_def)
1.640
1.641 lemma ereal_mult_minus_left[simp]:
1.642 - fixes a b :: ereal shows "-a * b = - (a * b)"
1.643 + fixes a b :: ereal
1.644 + shows "-a * b = - (a * b)"
1.645 by (cases rule: ereal2_cases[of a b]) auto
1.646
1.647 lemma ereal_mult_minus_right[simp]:
1.648 - fixes a b :: ereal shows "a * -b = - (a * b)"
1.649 + fixes a b :: ereal
1.650 + shows "a * -b = - (a * b)"
1.651 by (cases rule: ereal2_cases[of a b]) auto
1.652
1.653 lemma ereal_mult_infty[simp]:
1.654 @@ -590,26 +678,33 @@
1.655 by (cases a) auto
1.656
1.657 lemma ereal_mult_strict_right_mono:
1.658 - assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)"
1.659 + assumes "a < b"
1.660 + and "0 < c"
1.661 + and "c < (\<infinity>::ereal)"
1.662 shows "a * c < b * c"
1.663 using assms
1.664 - by (cases rule: ereal3_cases[of a b c])
1.665 - (auto simp: zero_le_mult_iff)
1.666 + by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff)
1.667
1.668 lemma ereal_mult_strict_left_mono:
1.669 - "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
1.670 - using ereal_mult_strict_right_mono by (simp add: mult_commute[of c])
1.671 + "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c < (\<infinity>::ereal) \<Longrightarrow> c * a < c * b"
1.672 + using ereal_mult_strict_right_mono
1.673 + by (simp add: mult_commute[of c])
1.674
1.675 lemma ereal_mult_right_mono:
1.676 - fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c"
1.677 + fixes a b c :: ereal
1.678 + shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
1.679 using assms
1.680 - apply (cases "c = 0") apply simp
1.681 - by (cases rule: ereal3_cases[of a b c])
1.682 - (auto simp: zero_le_mult_iff)
1.683 + apply (cases "c = 0")
1.684 + apply simp
1.685 + apply (cases rule: ereal3_cases[of a b c])
1.686 + apply (auto simp: zero_le_mult_iff)
1.687 + done
1.688
1.689 lemma ereal_mult_left_mono:
1.690 - fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
1.691 - using ereal_mult_right_mono by (simp add: mult_commute[of c])
1.692 + fixes a b c :: ereal
1.693 + shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.694 + using ereal_mult_right_mono
1.695 + by (simp add: mult_commute[of c])
1.696
1.697 lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"
1.698 by (simp add: one_ereal_def zero_ereal_def)
1.699 @@ -618,11 +713,13 @@
1.700 by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)
1.701
1.702 lemma ereal_right_distrib:
1.703 - fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
1.704 + fixes r a b :: ereal
1.705 + shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
1.706 by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
1.707
1.708 lemma ereal_left_distrib:
1.709 - fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
1.710 + fixes r a b :: ereal
1.711 + shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
1.712 by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
1.713
1.714 lemma ereal_mult_le_0_iff:
1.715 @@ -657,7 +754,9 @@
1.716
1.717 lemma ereal_distrib:
1.718 fixes a b c :: ereal
1.719 - assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
1.720 + assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
1.721 + and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
1.722 + and "\<bar>c\<bar> \<noteq> \<infinity>"
1.723 shows "(a + b) * c = a * c + b * c"
1.724 using assms
1.725 by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
1.726 @@ -670,74 +769,119 @@
1.727
1.728 lemma ereal_le_epsilon:
1.729 fixes x y :: ereal
1.730 - assumes "ALL e. 0 < e --> x <= y + e"
1.731 - shows "x <= y"
1.732 -proof-
1.733 -{ assume a: "EX r. y = ereal r"
1.734 - then obtain r where r_def: "y = ereal r" by auto
1.735 - { assume "x=(-\<infinity>)" hence ?thesis by auto }
1.736 + assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
1.737 + shows "x \<le> y"
1.738 +proof -
1.739 + {
1.740 + assume a: "\<exists>r. y = ereal r"
1.741 + then obtain r where r_def: "y = ereal r"
1.742 + by auto
1.743 + {
1.744 + assume "x = -\<infinity>"
1.745 + then have ?thesis by auto
1.746 + }
1.747 + moreover
1.748 + {
1.749 + assume "x \<noteq> -\<infinity>"
1.750 + then obtain p where p_def: "x = ereal p"
1.751 + using a assms[rule_format, of 1]
1.752 + by (cases x) auto
1.753 + {
1.754 + fix e
1.755 + have "0 < e \<longrightarrow> p \<le> r + e"
1.756 + using assms[rule_format, of "ereal e"] p_def r_def by auto
1.757 + }
1.758 + then have "p \<le> r"
1.759 + apply (subst field_le_epsilon)
1.760 + apply auto
1.761 + done
1.762 + then have ?thesis
1.763 + using r_def p_def by auto
1.764 + }
1.765 + ultimately have ?thesis
1.766 + by blast
1.767 + }
1.768 moreover
1.769 - { assume "~(x=(-\<infinity>))"
1.770 - then obtain p where p_def: "x = ereal p"
1.771 - using a assms[rule_format, of 1] by (cases x) auto
1.772 - { fix e have "0 < e --> p <= r + e"
1.773 - using assms[rule_format, of "ereal e"] p_def r_def by auto }
1.774 - hence "p <= r" apply (subst field_le_epsilon) by auto
1.775 - hence ?thesis using r_def p_def by auto
1.776 - } ultimately have ?thesis by blast
1.777 -}
1.778 -moreover
1.779 -{ assume "y=(-\<infinity>) | y=\<infinity>" hence ?thesis
1.780 - using assms[rule_format, of 1] by (cases x) auto
1.781 -} ultimately show ?thesis by (cases y) auto
1.782 + {
1.783 + assume "y = -\<infinity> | y = \<infinity>"
1.784 + then have ?thesis
1.785 + using assms[rule_format, of 1] by (cases x) auto
1.786 + }
1.787 + ultimately show ?thesis
1.788 + by (cases y) auto
1.789 qed
1.790
1.791 -
1.792 lemma ereal_le_epsilon2:
1.793 fixes x y :: ereal
1.794 - assumes "ALL e. 0 < e --> x <= y + ereal e"
1.795 - shows "x <= y"
1.796 -proof-
1.797 -{ fix e :: ereal assume "e>0"
1.798 - { assume "e=\<infinity>" hence "x<=y+e" by auto }
1.799 - moreover
1.800 - { assume "e~=\<infinity>"
1.801 - then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
1.802 - hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
1.803 - } ultimately have "x<=y+e" by blast
1.804 -} then show ?thesis using ereal_le_epsilon by auto
1.805 + assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e"
1.806 + shows "x \<le> y"
1.807 +proof -
1.808 + {
1.809 + fix e :: ereal
1.810 + assume "e > 0"
1.811 + {
1.812 + assume "e = \<infinity>"
1.813 + then have "x \<le> y + e"
1.814 + by auto
1.815 + }
1.816 + moreover
1.817 + {
1.818 + assume "e \<noteq> \<infinity>"
1.819 + then obtain r where "e = ereal r"
1.820 + using `e > 0` by (cases e) auto
1.821 + then have "x \<le> y + e"
1.822 + using assms[rule_format, of r] `e>0` by auto
1.823 + }
1.824 + ultimately have "x \<le> y + e"
1.825 + by blast
1.826 + }
1.827 + then show ?thesis
1.828 + using ereal_le_epsilon by auto
1.829 qed
1.830
1.831 lemma ereal_le_real:
1.832 fixes x y :: ereal
1.833 - assumes "ALL z. x <= ereal z --> y <= ereal z"
1.834 - shows "y <= x"
1.835 -by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
1.836 + assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z"
1.837 + shows "y \<le> x"
1.838 + by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
1.839
1.840 lemma setprod_ereal_0:
1.841 fixes f :: "'a \<Rightarrow> ereal"
1.842 - shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
1.843 -proof cases
1.844 - assume "finite A"
1.845 + shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
1.846 +proof (cases "finite A")
1.847 + case True
1.848 then show ?thesis by (induct A) auto
1.849 -qed auto
1.850 +next
1.851 + case False
1.852 + then show ?thesis by auto
1.853 +qed
1.854
1.855 lemma setprod_ereal_pos:
1.856 - fixes f :: "'a \<Rightarrow> ereal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
1.857 -proof cases
1.858 - assume "finite I" from this pos show ?thesis by induct auto
1.859 -qed simp
1.860 + fixes f :: "'a \<Rightarrow> ereal"
1.861 + assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
1.862 + shows "0 \<le> (\<Prod>i\<in>I. f i)"
1.863 +proof (cases "finite I")
1.864 + case True
1.865 + from this pos show ?thesis
1.866 + by induct auto
1.867 +next
1.868 + case False
1.869 + then show ?thesis by simp
1.870 +qed
1.871
1.872 lemma setprod_PInf:
1.873 fixes f :: "'a \<Rightarrow> ereal"
1.874 assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
1.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)"
1.876 -proof cases
1.877 - assume "finite I" from this assms show ?thesis
1.878 +proof (cases "finite I")
1.879 + case True
1.880 + from this assms show ?thesis
1.881 proof (induct I)
1.882 case (insert i I)
1.883 - then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_ereal_pos)
1.884 - from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
1.885 + then have pos: "0 \<le> f i" "0 \<le> setprod f I"
1.886 + by (auto intro!: setprod_ereal_pos)
1.887 + from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>"
1.888 + by auto
1.889 also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
1.890 using setprod_ereal_pos[of I f] pos
1.891 by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
1.892 @@ -745,13 +889,22 @@
1.893 using insert by (auto simp: setprod_ereal_0)
1.894 finally show ?case .
1.895 qed simp
1.896 -qed simp
1.897 +next
1.898 + case False
1.899 + then show ?thesis by simp
1.900 +qed
1.901
1.902 lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
1.903 -proof cases
1.904 - assume "finite A" then show ?thesis
1.905 +proof (cases "finite A")
1.906 + case True
1.907 + then show ?thesis
1.908 by induct (auto simp: one_ereal_def)
1.909 -qed (simp add: one_ereal_def)
1.910 +next
1.911 + case False
1.912 + then show ?thesis
1.913 + by (simp add: one_ereal_def)
1.914 +qed
1.915 +
1.916
1.917 subsubsection {* Power *}
1.918
1.919 @@ -771,10 +924,12 @@
1.920 by (induct n) (auto simp: one_ereal_def)
1.921
1.922 lemma zero_le_power_ereal[simp]:
1.923 - fixes a :: ereal assumes "0 \<le> a"
1.924 + fixes a :: ereal
1.925 + assumes "0 \<le> a"
1.926 shows "0 \<le> a ^ n"
1.927 using assms by (induct n) (auto simp: ereal_zero_le_0_iff)
1.928
1.929 +
1.930 subsubsection {* Subtraction *}
1.931
1.932 lemma ereal_minus_minus_image[simp]:
1.933 @@ -783,25 +938,30 @@
1.934 by (auto simp: image_iff)
1.935
1.936 lemma ereal_uminus_lessThan[simp]:
1.937 - fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
1.938 + fixes a :: ereal
1.939 + shows "uminus ` {..<a} = {-a<..}"
1.940 proof -
1.941 {
1.942 - fix x assume "-a < x"
1.943 - then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
1.944 - then have "- x < a" by simp
1.945 + fix x
1.946 + assume "-a < x"
1.947 + then have "- x < - (- a)"
1.948 + by (simp del: ereal_uminus_uminus)
1.949 + then have "- x < a"
1.950 + by simp
1.951 }
1.952 - then show ?thesis by (auto intro!: image_eqI)
1.953 + then show ?thesis
1.954 + by (auto intro!: image_eqI)
1.955 qed
1.956
1.957 -lemma ereal_uminus_greaterThan[simp]:
1.958 - "uminus ` {(a::ereal)<..} = {..<-a}"
1.959 - by (metis ereal_uminus_lessThan ereal_uminus_uminus
1.960 - ereal_minus_minus_image)
1.961 +lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
1.962 + by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image)
1.963
1.964 instantiation ereal :: minus
1.965 begin
1.966 +
1.967 definition "x - y = x + -(y::ereal)"
1.968 instance ..
1.969 +
1.970 end
1.971
1.972 lemma ereal_minus[simp]:
1.973 @@ -815,8 +975,7 @@
1.974 "0 - x = -x"
1.975 by (simp_all add: minus_ereal_def)
1.976
1.977 -lemma ereal_x_minus_x[simp]:
1.978 - "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
1.979 +lemma ereal_x_minus_x[simp]: "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
1.980 by (cases x) simp_all
1.981
1.982 lemma ereal_eq_minus_iff:
1.983 @@ -848,9 +1007,7 @@
1.984
1.985 lemma ereal_le_minus_iff:
1.986 fixes x y z :: ereal
1.987 - shows "x \<le> z - y \<longleftrightarrow>
1.988 - (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and>
1.989 - (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"
1.990 + 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)"
1.991 by (cases rule: ereal3_cases[of x y z]) auto
1.992
1.993 lemma ereal_le_minus:
1.994 @@ -860,9 +1017,7 @@
1.995
1.996 lemma ereal_minus_less_iff:
1.997 fixes x y z :: ereal
1.998 - shows "x - y < z \<longleftrightarrow>
1.999 - y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and>
1.1000 - (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
1.1001 + 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)"
1.1002 by (cases rule: ereal3_cases[of x y z]) auto
1.1003
1.1004 lemma ereal_minus_less:
1.1005 @@ -917,31 +1072,40 @@
1.1006
1.1007 lemma ereal_between:
1.1008 fixes x e :: ereal
1.1009 - assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"
1.1010 - shows "x - e < x" "x < x + e"
1.1011 -using assms apply (cases x, cases e) apply auto
1.1012 -using assms apply (cases x, cases e) apply auto
1.1013 -done
1.1014 + assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.1015 + and "0 < e"
1.1016 + shows "x - e < x"
1.1017 + and "x < x + e"
1.1018 + using assms
1.1019 + apply (cases x, cases e)
1.1020 + apply auto
1.1021 + using assms
1.1022 + apply (cases x, cases e)
1.1023 + apply auto
1.1024 + done
1.1025
1.1026 lemma ereal_minus_eq_PInfty_iff:
1.1027 - fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
1.1028 + fixes x y :: ereal
1.1029 + shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
1.1030 by (cases x y rule: ereal2_cases) simp_all
1.1031
1.1032 +
1.1033 subsubsection {* Division *}
1.1034
1.1035 instantiation ereal :: inverse
1.1036 begin
1.1037
1.1038 function inverse_ereal where
1.1039 -"inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" |
1.1040 -"inverse (\<infinity>::ereal) = 0" |
1.1041 -"inverse (-\<infinity>::ereal) = 0"
1.1042 + "inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))"
1.1043 +| "inverse (\<infinity>::ereal) = 0"
1.1044 +| "inverse (-\<infinity>::ereal) = 0"
1.1045 by (auto intro: ereal_cases)
1.1046 termination by (relation "{}") simp
1.1047
1.1048 definition "x / y = x * inverse (y :: ereal)"
1.1049
1.1050 instance ..
1.1051 +
1.1052 end
1.1053
1.1054 lemma real_of_ereal_inverse[simp]:
1.1055 @@ -959,53 +1123,61 @@
1.1056 unfolding divide_ereal_def by (auto simp: divide_real_def)
1.1057
1.1058 lemma ereal_divide_same[simp]:
1.1059 - fixes x :: ereal shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
1.1060 - by (cases x)
1.1061 - (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
1.1062 + fixes x :: ereal
1.1063 + shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
1.1064 + by (cases x) (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
1.1065
1.1066 lemma ereal_inv_inv[simp]:
1.1067 - fixes x :: ereal shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
1.1068 + fixes x :: ereal
1.1069 + shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
1.1070 by (cases x) auto
1.1071
1.1072 lemma ereal_inverse_minus[simp]:
1.1073 - fixes x :: ereal shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
1.1074 + fixes x :: ereal
1.1075 + shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
1.1076 by (cases x) simp_all
1.1077
1.1078 lemma ereal_uminus_divide[simp]:
1.1079 - fixes x y :: ereal shows "- x / y = - (x / y)"
1.1080 + fixes x y :: ereal
1.1081 + shows "- x / y = - (x / y)"
1.1082 unfolding divide_ereal_def by simp
1.1083
1.1084 lemma ereal_divide_Infty[simp]:
1.1085 - fixes x :: ereal shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
1.1086 + fixes x :: ereal
1.1087 + shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
1.1088 unfolding divide_ereal_def by simp_all
1.1089
1.1090 -lemma ereal_divide_one[simp]:
1.1091 - "x / 1 = (x::ereal)"
1.1092 +lemma ereal_divide_one[simp]: "x / 1 = (x::ereal)"
1.1093 unfolding divide_ereal_def by simp
1.1094
1.1095 -lemma ereal_divide_ereal[simp]:
1.1096 - "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
1.1097 +lemma ereal_divide_ereal[simp]: "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
1.1098 unfolding divide_ereal_def by simp
1.1099
1.1100 lemma zero_le_divide_ereal[simp]:
1.1101 - fixes a :: ereal assumes "0 \<le> a" "0 \<le> b"
1.1102 + fixes a :: ereal
1.1103 + assumes "0 \<le> a"
1.1104 + and "0 \<le> b"
1.1105 shows "0 \<le> a / b"
1.1106 using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
1.1107
1.1108 lemma ereal_le_divide_pos:
1.1109 - fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
1.1110 + fixes x y z :: ereal
1.1111 + shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
1.1112 by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
1.1113
1.1114 lemma ereal_divide_le_pos:
1.1115 - fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
1.1116 + fixes x y z :: ereal
1.1117 + shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
1.1118 by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
1.1119
1.1120 lemma ereal_le_divide_neg:
1.1121 - fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
1.1122 + fixes x y z :: ereal
1.1123 + shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
1.1124 by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
1.1125
1.1126 lemma ereal_divide_le_neg:
1.1127 - fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
1.1128 + fixes x y z :: ereal
1.1129 + shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
1.1130 by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
1.1131
1.1132 lemma ereal_inverse_antimono_strict:
1.1133 @@ -1015,31 +1187,37 @@
1.1134
1.1135 lemma ereal_inverse_antimono:
1.1136 fixes x y :: ereal
1.1137 - shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x"
1.1138 + shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> inverse y \<le> inverse x"
1.1139 by (cases rule: ereal2_cases[of x y]) auto
1.1140
1.1141 lemma inverse_inverse_Pinfty_iff[simp]:
1.1142 - fixes x :: ereal shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
1.1143 + fixes x :: ereal
1.1144 + shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
1.1145 by (cases x) auto
1.1146
1.1147 lemma ereal_inverse_eq_0:
1.1148 - fixes x :: ereal shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
1.1149 + fixes x :: ereal
1.1150 + shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
1.1151 by (cases x) auto
1.1152
1.1153 lemma ereal_0_gt_inverse:
1.1154 - fixes x :: ereal shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
1.1155 + fixes x :: ereal
1.1156 + shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
1.1157 by (cases x) auto
1.1158
1.1159 lemma ereal_mult_less_right:
1.1160 fixes a b c :: ereal
1.1161 - assumes "b * a < c * a" "0 < a" "a < \<infinity>"
1.1162 + assumes "b * a < c * a"
1.1163 + and "0 < a"
1.1164 + and "a < \<infinity>"
1.1165 shows "b < c"
1.1166 using assms
1.1167 by (cases rule: ereal3_cases[of a b c])
1.1168 (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
1.1169
1.1170 lemma ereal_power_divide:
1.1171 - fixes x y :: ereal shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
1.1172 + fixes x y :: ereal
1.1173 + shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
1.1174 by (cases rule: ereal2_cases[of x y])
1.1175 (auto simp: one_ereal_def zero_ereal_def power_divide not_le
1.1176 power_less_zero_eq zero_le_power_iff)
1.1177 @@ -1047,36 +1225,47 @@
1.1178 lemma ereal_le_mult_one_interval:
1.1179 fixes x y :: ereal
1.1180 assumes y: "y \<noteq> -\<infinity>"
1.1181 - assumes z: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
1.1182 + assumes z: "\<And>z. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> z * x \<le> y"
1.1183 shows "x \<le> y"
1.1184 proof (cases x)
1.1185 - case PInf with z[of "1 / 2"] show "x \<le> y" by (simp add: one_ereal_def)
1.1186 + case PInf
1.1187 + with z[of "1 / 2"] show "x \<le> y"
1.1188 + by (simp add: one_ereal_def)
1.1189 next
1.1190 - case (real r) note r = this
1.1191 + case (real r)
1.1192 + note r = this
1.1193 show "x \<le> y"
1.1194 proof (cases y)
1.1195 - case (real p) note p = this
1.1196 + case (real p)
1.1197 + note p = this
1.1198 have "r \<le> p"
1.1199 proof (rule field_le_mult_one_interval)
1.1200 - fix z :: real assume "0 < z" and "z < 1"
1.1201 - with z[of "ereal z"]
1.1202 - show "z * r \<le> p" using p r by (auto simp: zero_le_mult_iff one_ereal_def)
1.1203 + fix z :: real
1.1204 + assume "0 < z" and "z < 1"
1.1205 + with z[of "ereal z"] show "z * r \<le> p"
1.1206 + using p r by (auto simp: zero_le_mult_iff one_ereal_def)
1.1207 qed
1.1208 - then show "x \<le> y" using p r by simp
1.1209 + then show "x \<le> y"
1.1210 + using p r by simp
1.1211 qed (insert y, simp_all)
1.1212 qed simp
1.1213
1.1214 lemma ereal_divide_right_mono[simp]:
1.1215 fixes x y z :: ereal
1.1216 - assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
1.1217 -using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
1.1218 + assumes "x \<le> y"
1.1219 + and "0 < z"
1.1220 + shows "x / z \<le> y / z"
1.1221 + using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
1.1222
1.1223 lemma ereal_divide_left_mono[simp]:
1.1224 fixes x y z :: ereal
1.1225 - assumes "y \<le> x" "0 < z" "0 < x * y"
1.1226 + assumes "y \<le> x"
1.1227 + and "0 < z"
1.1228 + and "0 < x * y"
1.1229 shows "z / x \<le> z / y"
1.1230 -using assms by (cases x y z rule: ereal3_cases)
1.1231 - (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
1.1232 + using assms
1.1233 + by (cases x y z rule: ereal3_cases)
1.1234 + (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
1.1235
1.1236 lemma ereal_divide_zero_left[simp]:
1.1237 fixes a :: ereal
1.1238 @@ -1088,13 +1277,16 @@
1.1239 shows "b / c * a = b * a / c"
1.1240 by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
1.1241
1.1242 +
1.1243 subsection "Complete lattice"
1.1244
1.1245 instantiation ereal :: lattice
1.1246 begin
1.1247 +
1.1248 definition [simp]: "sup x y = (max x y :: ereal)"
1.1249 definition [simp]: "inf x y = (min x y :: ereal)"
1.1250 instance by default simp_all
1.1251 +
1.1252 end
1.1253
1.1254 instantiation ereal :: complete_lattice
1.1255 @@ -1109,29 +1301,46 @@
1.1256 lemma ereal_complete_Sup:
1.1257 fixes S :: "ereal set"
1.1258 shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
1.1259 -proof cases
1.1260 - assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
1.1261 - then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y" by auto
1.1262 - then have "\<infinity> \<notin> S" by force
1.1263 +proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
1.1264 + case True
1.1265 + then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
1.1266 + by auto
1.1267 + then have "\<infinity> \<notin> S"
1.1268 + by force
1.1269 show ?thesis
1.1270 - proof cases
1.1271 - assume "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}"
1.1272 - with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>" by auto
1.1273 + proof (cases "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}")
1.1274 + case True
1.1275 + with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
1.1276 + by auto
1.1277 obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
1.1278 proof (atomize_elim, rule complete_real)
1.1279 - show "\<exists>x. x \<in> ereal -` S" using x by auto
1.1280 - show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z" by (auto dest: y intro!: exI[of _ y])
1.1281 + show "\<exists>x. x \<in> ereal -` S"
1.1282 + using x by auto
1.1283 + show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z"
1.1284 + by (auto dest: y intro!: exI[of _ y])
1.1285 qed
1.1286 show ?thesis
1.1287 proof (safe intro!: exI[of _ "ereal s"])
1.1288 - fix y assume "y \<in> S" with s `\<infinity> \<notin> S` show "y \<le> ereal s"
1.1289 + fix y
1.1290 + assume "y \<in> S"
1.1291 + with s `\<infinity> \<notin> S` show "y \<le> ereal s"
1.1292 by (cases y) auto
1.1293 next
1.1294 - fix z assume "\<forall>y\<in>S. y \<le> z" with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
1.1295 + fix z
1.1296 + assume "\<forall>y\<in>S. y \<le> z"
1.1297 + with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
1.1298 by (cases z) (auto intro!: s)
1.1299 qed
1.1300 - qed (auto intro!: exI[of _ "-\<infinity>"])
1.1301 -qed (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
1.1302 + next
1.1303 + case False
1.1304 + then show ?thesis
1.1305 + by (auto intro!: exI[of _ "-\<infinity>"])
1.1306 + qed
1.1307 +next
1.1308 + case False
1.1309 + then show ?thesis
1.1310 + by (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
1.1311 +qed
1.1312
1.1313 lemma ereal_complete_uminus_eq:
1.1314 fixes S :: "ereal set"
1.1315 @@ -1141,23 +1350,24 @@
1.1316
1.1317 lemma ereal_complete_Inf:
1.1318 "\<exists>x. (\<forall>y\<in>S::ereal set. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
1.1319 - using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
1.1320 + using ereal_complete_Sup[of "uminus ` S"]
1.1321 + unfolding ereal_complete_uminus_eq
1.1322 + by auto
1.1323
1.1324 instance
1.1325 proof
1.1326 show "Sup {} = (bot::ereal)"
1.1327 - apply (auto simp: bot_ereal_def Sup_ereal_def)
1.1328 - apply (rule some1_equality)
1.1329 - apply (metis ereal_bot ereal_less_eq(2))
1.1330 - apply (metis ereal_less_eq(2))
1.1331 - done
1.1332 -next
1.1333 + apply (auto simp: bot_ereal_def Sup_ereal_def)
1.1334 + apply (rule some1_equality)
1.1335 + apply (metis ereal_bot ereal_less_eq(2))
1.1336 + apply (metis ereal_less_eq(2))
1.1337 + done
1.1338 show "Inf {} = (top::ereal)"
1.1339 - apply (auto simp: top_ereal_def Inf_ereal_def)
1.1340 - apply (rule some1_equality)
1.1341 - apply (metis ereal_top ereal_less_eq(1))
1.1342 - apply (metis ereal_less_eq(1))
1.1343 - done
1.1344 + apply (auto simp: top_ereal_def Inf_ereal_def)
1.1345 + apply (rule some1_equality)
1.1346 + apply (metis ereal_top ereal_less_eq(1))
1.1347 + apply (metis ereal_less_eq(1))
1.1348 + done
1.1349 qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
1.1350 simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
1.1351
1.1352 @@ -1183,74 +1393,89 @@
1.1353 using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
1.1354
1.1355 lemma ereal_SUPR_uminus:
1.1356 - fixes f :: "'a => ereal"
1.1357 + fixes f :: "'a \<Rightarrow> ereal"
1.1358 shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
1.1359 using ereal_Sup_uminus_image_eq[of "f`R"]
1.1360 by (simp add: SUP_def INF_def image_image)
1.1361
1.1362 lemma ereal_INFI_uminus:
1.1363 - fixes f :: "'a => ereal"
1.1364 - shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
1.1365 + fixes f :: "'a \<Rightarrow> ereal"
1.1366 + shows "(INF i : R. - f i) = - (SUP i : R. f i)"
1.1367 using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
1.1368
1.1369 lemma ereal_image_uminus_shift:
1.1370 - fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
1.1371 + fixes X Y :: "ereal set"
1.1372 + shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
1.1373 proof
1.1374 assume "uminus ` X = Y"
1.1375 then have "uminus ` uminus ` X = uminus ` Y"
1.1376 by (simp add: inj_image_eq_iff)
1.1377 - then show "X = uminus ` Y" by (simp add: image_image)
1.1378 + then show "X = uminus ` Y"
1.1379 + by (simp add: image_image)
1.1380 qed (simp add: image_image)
1.1381
1.1382 lemma Inf_ereal_iff:
1.1383 fixes z :: ereal
1.1384 - shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x<y) <-> Inf X < y"
1.1385 - by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear
1.1386 - order_less_le_trans)
1.1387 + shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x < y) \<longleftrightarrow> Inf X < y"
1.1388 + by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
1.1389 + less_le_not_le linear order_less_le_trans)
1.1390
1.1391 lemma Sup_eq_MInfty:
1.1392 - fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
1.1393 + fixes S :: "ereal set"
1.1394 + shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
1.1395 unfolding bot_ereal_def[symmetric] by auto
1.1396
1.1397 lemma Inf_eq_PInfty:
1.1398 - fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
1.1399 + fixes S :: "ereal set"
1.1400 + shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
1.1401 using Sup_eq_MInfty[of "uminus`S"]
1.1402 unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp
1.1403
1.1404 -lemma Inf_eq_MInfty:
1.1405 - fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
1.1406 +lemma Inf_eq_MInfty:
1.1407 + fixes S :: "ereal set"
1.1408 + shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
1.1409 unfolding bot_ereal_def[symmetric] by auto
1.1410
1.1411 lemma Sup_eq_PInfty:
1.1412 - fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
1.1413 + fixes S :: "ereal set"
1.1414 + shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
1.1415 unfolding top_ereal_def[symmetric] by auto
1.1416
1.1417 lemma Sup_ereal_close:
1.1418 fixes e :: ereal
1.1419 - assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
1.1420 + assumes "0 < e"
1.1421 + and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
1.1422 shows "\<exists>x\<in>S. Sup S - e < x"
1.1423 using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1])
1.1424
1.1425 lemma Inf_ereal_close:
1.1426 - fixes e :: ereal assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>" "0 < e"
1.1427 + fixes e :: ereal
1.1428 + assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>"
1.1429 + and "0 < e"
1.1430 shows "\<exists>x\<in>X. x < Inf X + e"
1.1431 proof (rule Inf_less_iff[THEN iffD1])
1.1432 - show "Inf X < Inf X + e" using assms
1.1433 - by (cases e) auto
1.1434 + show "Inf X < Inf X + e"
1.1435 + using assms by (cases e) auto
1.1436 qed
1.1437
1.1438 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
1.1439 proof -
1.1440 - { fix x ::ereal assume "x \<noteq> \<infinity>"
1.1441 + {
1.1442 + fix x :: ereal
1.1443 + assume "x \<noteq> \<infinity>"
1.1444 then have "\<exists>k::nat. x < ereal (real k)"
1.1445 proof (cases x)
1.1446 - case MInf then show ?thesis by (intro exI[of _ 0]) auto
1.1447 + case MInf
1.1448 + then show ?thesis
1.1449 + by (intro exI[of _ 0]) auto
1.1450 next
1.1451 case (real r)
1.1452 moreover obtain k :: nat where "r < real k"
1.1453 using ex_less_of_nat by (auto simp: real_eq_of_nat)
1.1454 - ultimately show ?thesis by auto
1.1455 - qed simp }
1.1456 + ultimately show ?thesis
1.1457 + by auto
1.1458 + qed simp
1.1459 + }
1.1460 then show ?thesis
1.1461 using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
1.1462 by (auto simp: top_ereal_def)
1.1463 @@ -1259,96 +1484,136 @@
1.1464 lemma Inf_less:
1.1465 fixes x :: ereal
1.1466 assumes "(INF i:A. f i) < x"
1.1467 - shows "EX i. i : A & f i <= x"
1.1468 -proof(rule ccontr)
1.1469 - assume "~ (EX i. i : A & f i <= x)"
1.1470 - hence "ALL i:A. f i > x" by auto
1.1471 - hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto
1.1472 - thus False using assms by auto
1.1473 + shows "\<exists>i. i \<in> A \<and> f i \<le> x"
1.1474 +proof (rule ccontr)
1.1475 + assume "\<not> ?thesis"
1.1476 + then have "\<forall>i\<in>A. f i > x"
1.1477 + by auto
1.1478 + then have "(INF i:A. f i) \<ge> x"
1.1479 + by (subst INF_greatest) auto
1.1480 + then show False
1.1481 + using assms by auto
1.1482 qed
1.1483
1.1484 lemma SUP_ereal_le_addI:
1.1485 fixes f :: "'i \<Rightarrow> ereal"
1.1486 - assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
1.1487 + assumes "\<And>i. f i + y \<le> z"
1.1488 + and "y \<noteq> -\<infinity>"
1.1489 shows "SUPR UNIV f + y \<le> z"
1.1490 proof (cases y)
1.1491 case (real r)
1.1492 - then have "\<And>i. f i \<le> z - y" using assms by (simp add: ereal_le_minus_iff)
1.1493 - then have "SUPR UNIV f \<le> z - y" by (rule SUP_least)
1.1494 - then show ?thesis using real by (simp add: ereal_le_minus_iff)
1.1495 + then have "\<And>i. f i \<le> z - y"
1.1496 + using assms by (simp add: ereal_le_minus_iff)
1.1497 + then have "SUPR UNIV f \<le> z - y"
1.1498 + by (rule SUP_least)
1.1499 + then show ?thesis
1.1500 + using real by (simp add: ereal_le_minus_iff)
1.1501 qed (insert assms, auto)
1.1502
1.1503 lemma SUPR_ereal_add:
1.1504 fixes f g :: "nat \<Rightarrow> ereal"
1.1505 - assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
1.1506 + assumes "incseq f"
1.1507 + and "incseq g"
1.1508 + and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
1.1509 shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
1.1510 proof (rule SUP_eqI)
1.1511 - fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
1.1512 - have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
1.1513 - unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
1.1514 - { fix j
1.1515 - { fix i
1.1516 + fix y
1.1517 + assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
1.1518 + have f: "SUPR UNIV f \<noteq> -\<infinity>"
1.1519 + using pos
1.1520 + unfolding SUP_def Sup_eq_MInfty
1.1521 + by (auto dest: image_eqD)
1.1522 + {
1.1523 + fix j
1.1524 + {
1.1525 + fix i
1.1526 have "f i + g j \<le> f i + g (max i j)"
1.1527 - using `incseq g`[THEN incseqD] by (rule add_left_mono) auto
1.1528 + using `incseq g`[THEN incseqD]
1.1529 + by (rule add_left_mono) auto
1.1530 also have "\<dots> \<le> f (max i j) + g (max i j)"
1.1531 - using `incseq f`[THEN incseqD] by (rule add_right_mono) auto
1.1532 + using `incseq f`[THEN incseqD]
1.1533 + by (rule add_right_mono) auto
1.1534 also have "\<dots> \<le> y" using * by auto
1.1535 - finally have "f i + g j \<le> y" . }
1.1536 + finally have "f i + g j \<le> y" .
1.1537 + }
1.1538 then have "SUPR UNIV f + g j \<le> y"
1.1539 using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
1.1540 - then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps) }
1.1541 + then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps)
1.1542 + }
1.1543 then have "SUPR UNIV g + SUPR UNIV f \<le> y"
1.1544 using f by (rule SUP_ereal_le_addI)
1.1545 - then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
1.1546 + then show "SUPR UNIV f + SUPR UNIV g \<le> y"
1.1547 + by (simp add: ac_simps)
1.1548 qed (auto intro!: add_mono SUP_upper)
1.1549
1.1550 lemma SUPR_ereal_add_pos:
1.1551 fixes f g :: "nat \<Rightarrow> ereal"
1.1552 - assumes inc: "incseq f" "incseq g" and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
1.1553 + assumes inc: "incseq f" "incseq g"
1.1554 + and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
1.1555 shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
1.1556 proof (intro SUPR_ereal_add inc)
1.1557 - fix i show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>" using pos[of i] by auto
1.1558 + fix i
1.1559 + show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
1.1560 + using pos[of i] by auto
1.1561 qed
1.1562
1.1563 lemma SUPR_ereal_setsum:
1.1564 fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
1.1565 - assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)" and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
1.1566 + assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
1.1567 + and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
1.1568 shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPR UNIV (f n))"
1.1569 -proof cases
1.1570 - assume "finite A" then show ?thesis using assms
1.1571 +proof (cases "finite A")
1.1572 + case True
1.1573 + then show ?thesis using assms
1.1574 by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
1.1575 -qed simp
1.1576 +next
1.1577 + case False
1.1578 + then show ?thesis by simp
1.1579 +qed
1.1580
1.1581 lemma SUPR_ereal_cmult:
1.1582 - fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
1.1583 + fixes f :: "nat \<Rightarrow> ereal"
1.1584 + assumes "\<And>i. 0 \<le> f i"
1.1585 + and "0 \<le> c"
1.1586 shows "(SUP i. c * f i) = c * SUPR UNIV f"
1.1587 proof (rule SUP_eqI)
1.1588 - fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
1.1589 + fix i
1.1590 + have "f i \<le> SUPR UNIV f"
1.1591 + by (rule SUP_upper) auto
1.1592 then show "c * f i \<le> c * SUPR UNIV f"
1.1593 using `0 \<le> c` by (rule ereal_mult_left_mono)
1.1594 next
1.1595 - fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
1.1596 + fix y
1.1597 + assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
1.1598 show "c * SUPR UNIV f \<le> y"
1.1599 - proof cases
1.1600 - assume c: "0 < c \<and> c \<noteq> \<infinity>"
1.1601 + proof (cases "0 < c \<and> c \<noteq> \<infinity>")
1.1602 + case True
1.1603 with * have "SUPR UNIV f \<le> y / c"
1.1604 by (intro SUP_least) (auto simp: ereal_le_divide_pos)
1.1605 - with c show ?thesis
1.1606 + with True show ?thesis
1.1607 by (auto simp: ereal_le_divide_pos)
1.1608 next
1.1609 - { assume "c = \<infinity>" have ?thesis
1.1610 - proof cases
1.1611 - assume **: "\<forall>i. f i = 0"
1.1612 - then have "range f = {0}" by auto
1.1613 - with ** show "c * SUPR UNIV f \<le> y" using *
1.1614 - by (auto simp: SUP_def min_max.sup_absorb1)
1.1615 + case False
1.1616 + {
1.1617 + assume "c = \<infinity>"
1.1618 + have ?thesis
1.1619 + proof (cases "\<forall>i. f i = 0")
1.1620 + case True
1.1621 + then have "range f = {0}"
1.1622 + by auto
1.1623 + with True show "c * SUPR UNIV f \<le> y"
1.1624 + using * by (auto simp: SUP_def min_max.sup_absorb1)
1.1625 next
1.1626 - assume "\<not> (\<forall>i. f i = 0)"
1.1627 - then obtain i where "f i \<noteq> 0" by auto
1.1628 - with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis by (auto split: split_if_asm)
1.1629 - qed }
1.1630 - moreover assume "\<not> (0 < c \<and> c \<noteq> \<infinity>)"
1.1631 - ultimately show ?thesis using * `0 \<le> c` by auto
1.1632 + case False
1.1633 + then obtain i where "f i \<noteq> 0"
1.1634 + by auto
1.1635 + with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
1.1636 + by (auto split: split_if_asm)
1.1637 + qed
1.1638 + }
1.1639 + moreover note False
1.1640 + ultimately show ?thesis
1.1641 + using * `0 \<le> c` by auto
1.1642 qed
1.1643 qed
1.1644
1.1645 @@ -1359,15 +1624,21 @@
1.1646 unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
1.1647 apply simp
1.1648 proof safe
1.1649 - fix x :: ereal assume "x \<noteq> \<infinity>"
1.1650 + fix x :: ereal
1.1651 + assume "x \<noteq> \<infinity>"
1.1652 show "\<exists>i\<in>A. x < f i"
1.1653 proof (cases x)
1.1654 - case PInf with `x \<noteq> \<infinity>` show ?thesis by simp
1.1655 + case PInf
1.1656 + with `x \<noteq> \<infinity>` show ?thesis
1.1657 + by simp
1.1658 next
1.1659 - case MInf with assms[of "0"] show ?thesis by force
1.1660 + case MInf
1.1661 + with assms[of "0"] show ?thesis
1.1662 + by force
1.1663 next
1.1664 case (real r)
1.1665 - with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
1.1666 + with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
1.1667 + by auto
1.1668 moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
1.1669 using assms ..
1.1670 ultimately show ?thesis
1.1671 @@ -1382,7 +1653,8 @@
1.1672 case (real r)
1.1673 have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
1.1674 proof
1.1675 - fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
1.1676 + fix n :: nat
1.1677 + have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
1.1678 using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
1.1679 then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
1.1680 then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
1.1681 @@ -1392,48 +1664,63 @@
1.1682 where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
1.1683 have "SUPR UNIV f = Sup A"
1.1684 proof (rule SUP_eqI)
1.1685 - fix i show "f i \<le> Sup A" using f
1.1686 - by (auto intro!: complete_lattice_class.Sup_upper)
1.1687 + fix i
1.1688 + show "f i \<le> Sup A"
1.1689 + using f by (auto intro!: complete_lattice_class.Sup_upper)
1.1690 next
1.1691 - fix y assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
1.1692 + fix y
1.1693 + assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
1.1694 show "Sup A \<le> y"
1.1695 proof (rule ereal_le_epsilon, intro allI impI)
1.1696 - fix e :: ereal assume "0 < e"
1.1697 + fix e :: ereal
1.1698 + assume "0 < e"
1.1699 show "Sup A \<le> y + e"
1.1700 proof (cases e)
1.1701 case (real r)
1.1702 - hence "0 < r" using `0 < e` by auto
1.1703 - then obtain n ::nat where *: "1 / real n < r" "0 < n"
1.1704 - using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide)
1.1705 - have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n]
1.1706 + then have "0 < r"
1.1707 + using `0 < e` by auto
1.1708 + then obtain n :: nat where *: "1 / real n < r" "0 < n"
1.1709 + using ex_inverse_of_nat_less
1.1710 + by (auto simp: real_eq_of_nat inverse_eq_divide)
1.1711 + have "Sup A \<le> f n + 1 / ereal (real n)"
1.1712 + using f[THEN spec, of n]
1.1713 by auto
1.1714 - also have "1 / ereal (real n) \<le> e" using real * by (auto simp: one_ereal_def )
1.1715 - with bound have "f n + 1 / ereal (real n) \<le> y + e" by (rule add_mono) simp
1.1716 + also have "1 / ereal (real n) \<le> e"
1.1717 + using real *
1.1718 + by (auto simp: one_ereal_def )
1.1719 + with bound have "f n + 1 / ereal (real n) \<le> y + e"
1.1720 + by (rule add_mono) simp
1.1721 finally show "Sup A \<le> y + e" .
1.1722 qed (insert `0 < e`, auto)
1.1723 qed
1.1724 qed
1.1725 - with f show ?thesis by (auto intro!: exI[of _ f])
1.1726 + with f show ?thesis
1.1727 + by (auto intro!: exI[of _ f])
1.1728 next
1.1729 case PInf
1.1730 - from `A \<noteq> {}` obtain x where "x \<in> A" by auto
1.1731 + from `A \<noteq> {}` obtain x where "x \<in> A"
1.1732 + by auto
1.1733 show ?thesis
1.1734 - proof cases
1.1735 - assume *: "\<infinity> \<in> A"
1.1736 - then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
1.1737 - with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
1.1738 + proof (cases "\<infinity> \<in> A")
1.1739 + case True
1.1740 + then have "\<infinity> \<le> Sup A"
1.1741 + by (intro complete_lattice_class.Sup_upper)
1.1742 + with True show ?thesis
1.1743 + by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
1.1744 next
1.1745 - assume "\<infinity> \<notin> A"
1.1746 + case False
1.1747 have "\<exists>x\<in>A. 0 \<le> x"
1.1748 - by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least ereal_infty_less_eq2 linorder_linear)
1.1749 - then obtain x where "x \<in> A" "0 \<le> x" by auto
1.1750 + by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least
1.1751 + ereal_infty_less_eq2 linorder_linear)
1.1752 + then obtain x where "x \<in> A" and "0 \<le> x"
1.1753 + by auto
1.1754 have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
1.1755 proof (rule ccontr)
1.1756 assume "\<not> ?thesis"
1.1757 then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
1.1758 by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
1.1759 then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
1.1760 - by(cases x) auto
1.1761 + by (cases x) auto
1.1762 qed
1.1763 from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
1.1764 where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
1.1765 @@ -1444,20 +1731,26 @@
1.1766 using f[THEN spec, of n] `0 \<le> x`
1.1767 by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
1.1768 qed
1.1769 - then show ?thesis using f PInf by (auto intro!: exI[of _ f])
1.1770 + then show ?thesis
1.1771 + using f PInf by (auto intro!: exI[of _ f])
1.1772 qed
1.1773 next
1.1774 case MInf
1.1775 - with `A \<noteq> {}` have "A = {-\<infinity>}" by (auto simp: Sup_eq_MInfty)
1.1776 - then show ?thesis using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
1.1777 + with `A \<noteq> {}` have "A = {-\<infinity>}"
1.1778 + by (auto simp: Sup_eq_MInfty)
1.1779 + then show ?thesis
1.1780 + using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
1.1781 qed
1.1782
1.1783 lemma SUPR_countable_SUPR:
1.1784 "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
1.1785 - using Sup_countable_SUPR[of "g`A"] by (auto simp: SUP_def)
1.1786 + using Sup_countable_SUPR[of "g`A"]
1.1787 + by (auto simp: SUP_def)
1.1788
1.1789 lemma Sup_ereal_cadd:
1.1790 - fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
1.1791 + fixes A :: "ereal set"
1.1792 + assumes "A \<noteq> {}"
1.1793 + and "a \<noteq> -\<infinity>"
1.1794 shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
1.1795 proof (rule antisym)
1.1796 have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
1.1797 @@ -1465,37 +1758,46 @@
1.1798 then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
1.1799 show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
1.1800 proof (cases a)
1.1801 - case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1)
1.1802 + case PInf with `A \<noteq> {}`
1.1803 + show ?thesis
1.1804 + by (auto simp: image_constant min_max.sup_absorb1)
1.1805 next
1.1806 case (real r)
1.1807 then have **: "op + (- a) ` op + a ` A = A"
1.1808 by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
1.1809 - from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis unfolding **
1.1810 + from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
1.1811 + unfolding **
1.1812 by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
1.1813 qed (insert `a \<noteq> -\<infinity>`, auto)
1.1814 qed
1.1815
1.1816 lemma Sup_ereal_cminus:
1.1817 - fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
1.1818 + fixes A :: "ereal set"
1.1819 + assumes "A \<noteq> {}"
1.1820 + and "a \<noteq> -\<infinity>"
1.1821 shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
1.1822 using Sup_ereal_cadd[of "uminus ` A" a] assms
1.1823 - by (simp add: comp_def image_image minus_ereal_def
1.1824 - ereal_Sup_uminus_image_eq)
1.1825 + by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
1.1826
1.1827 lemma SUPR_ereal_cminus:
1.1828 fixes f :: "'i \<Rightarrow> ereal"
1.1829 - fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
1.1830 + fixes A
1.1831 + assumes "A \<noteq> {}"
1.1832 + and "a \<noteq> -\<infinity>"
1.1833 shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
1.1834 using Sup_ereal_cminus[of "f`A" a] assms
1.1835 unfolding SUP_def INF_def image_image by auto
1.1836
1.1837 lemma Inf_ereal_cminus:
1.1838 - fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
1.1839 + fixes A :: "ereal set"
1.1840 + assumes "A \<noteq> {}"
1.1841 + and "\<bar>a\<bar> \<noteq> \<infinity>"
1.1842 shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
1.1843 proof -
1.1844 {
1.1845 fix x
1.1846 - have "-a - -x = -(a - x)" using assms by (cases x) auto
1.1847 + have "-a - -x = -(a - x)"
1.1848 + using assms by (cases x) auto
1.1849 } note * = this
1.1850 then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
1.1851 by (auto simp: image_image)
1.1852 @@ -1505,25 +1807,32 @@
1.1853 qed
1.1854
1.1855 lemma INFI_ereal_cminus:
1.1856 - fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
1.1857 + fixes a :: ereal
1.1858 + assumes "A \<noteq> {}"
1.1859 + and "\<bar>a\<bar> \<noteq> \<infinity>"
1.1860 shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
1.1861 using Inf_ereal_cminus[of "f`A" a] assms
1.1862 unfolding SUP_def INF_def image_image
1.1863 by auto
1.1864
1.1865 lemma uminus_ereal_add_uminus_uminus:
1.1866 - fixes a b :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
1.1867 + fixes a b :: ereal
1.1868 + shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
1.1869 by (cases rule: ereal2_cases[of a b]) auto
1.1870
1.1871 lemma INFI_ereal_add:
1.1872 fixes f :: "nat \<Rightarrow> ereal"
1.1873 - assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
1.1874 + assumes "decseq f" "decseq g"
1.1875 + and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
1.1876 shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
1.1877 proof -
1.1878 have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
1.1879 using assms unfolding INF_less_iff by auto
1.1880 - { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
1.1881 - by (rule uminus_ereal_add_uminus_uminus) }
1.1882 + {
1.1883 + fix i
1.1884 + from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
1.1885 + by (rule uminus_ereal_add_uminus_uminus)
1.1886 + }
1.1887 then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
1.1888 by simp
1.1889 also have "\<dots> = INFI UNIV f + INFI UNIV g"
1.1890 @@ -1534,6 +1843,7 @@
1.1891 finally show ?thesis .
1.1892 qed
1.1893
1.1894 +
1.1895 subsection "Relation to @{typ enat}"
1.1896
1.1897 definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
1.1898 @@ -1546,50 +1856,41 @@
1.1899 "ereal_of_enat \<infinity> = \<infinity>"
1.1900 by (simp_all add: ereal_of_enat_def)
1.1901
1.1902 -lemma ereal_of_enat_le_iff[simp]:
1.1903 - "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
1.1904 -by (cases m n rule: enat2_cases) auto
1.1905 +lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
1.1906 + by (cases m n rule: enat2_cases) auto
1.1907
1.1908 -lemma ereal_of_enat_less_iff[simp]:
1.1909 - "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
1.1910 -by (cases m n rule: enat2_cases) auto
1.1911 +lemma ereal_of_enat_less_iff[simp]: "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
1.1912 + by (cases m n rule: enat2_cases) auto
1.1913
1.1914 -lemma numeral_le_ereal_of_enat_iff[simp]:
1.1915 - shows "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
1.1916 -by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
1.1917 +lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
1.1918 + by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
1.1919
1.1920 -lemma numeral_less_ereal_of_enat_iff[simp]:
1.1921 - shows "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
1.1922 -by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
1.1923 +lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
1.1924 + by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
1.1925
1.1926 -lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
1.1927 - "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
1.1928 -by (cases n) (auto simp: enat_0[symmetric])
1.1929 +lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
1.1930 + by (cases n) (auto simp: enat_0[symmetric])
1.1931
1.1932 -lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
1.1933 - "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
1.1934 -by (cases n) (auto simp: enat_0[symmetric])
1.1935 +lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
1.1936 + by (cases n) (auto simp: enat_0[symmetric])
1.1937
1.1938 -lemma ereal_of_enat_zero[simp]:
1.1939 - "ereal_of_enat 0 = 0"
1.1940 -by (auto simp: enat_0[symmetric])
1.1941 +lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
1.1942 + by (auto simp: enat_0[symmetric])
1.1943
1.1944 -lemma ereal_of_enat_inf[simp]:
1.1945 - "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
1.1946 +lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
1.1947 by (cases n) auto
1.1948
1.1949 -
1.1950 -lemma ereal_of_enat_add:
1.1951 - "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
1.1952 -by (cases m n rule: enat2_cases) auto
1.1953 +lemma ereal_of_enat_add: "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
1.1954 + by (cases m n rule: enat2_cases) auto
1.1955
1.1956 lemma ereal_of_enat_sub:
1.1957 - assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
1.1958 -using assms by (cases m n rule: enat2_cases) auto
1.1959 + assumes "n \<le> m"
1.1960 + shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
1.1961 + using assms by (cases m n rule: enat2_cases) auto
1.1962
1.1963 lemma ereal_of_enat_mult:
1.1964 "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
1.1965 -by (cases m n rule: enat2_cases) auto
1.1966 + by (cases m n rule: enat2_cases) auto
1.1967
1.1968 lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
1.1969 lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
1.1970 @@ -1607,6 +1908,7 @@
1.1971
1.1972 instance
1.1973 by default (simp add: open_ereal_generated)
1.1974 +
1.1975 end
1.1976
1.1977 lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
1.1978 @@ -1618,8 +1920,13 @@
1.1979 with Int show ?case
1.1980 by (intro exI[of _ "max x z"]) fastforce
1.1981 next
1.1982 - { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
1.1983 - moreover case (Basis S)
1.1984 + case (Basis S)
1.1985 + {
1.1986 + fix x
1.1987 + have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t"
1.1988 + by (cases x) auto
1.1989 + }
1.1990 + moreover note Basis
1.1991 ultimately show ?case
1.1992 by (auto split: ereal.split)
1.1993 qed (fastforce simp add: vimage_Union)+
1.1994 @@ -1633,8 +1940,13 @@
1.1995 with Int show ?case
1.1996 by (intro exI[of _ "min x z"]) fastforce
1.1997 next
1.1998 - { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
1.1999 - moreover case (Basis S)
1.2000 + case (Basis S)
1.2001 + {
1.2002 + fix x
1.2003 + have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x"
1.2004 + by (cases x) auto
1.2005 + }
1.2006 + moreover note Basis
1.2007 ultimately show ?case
1.2008 by (auto split: ereal.split)
1.2009 qed (fastforce simp add: vimage_Union)+
1.2010 @@ -1642,13 +1954,18 @@
1.2011 lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
1.2012 unfolding open_ereal_generated
1.2013 proof (induct rule: generate_topology.induct)
1.2014 - case (Int A B) then show ?case by auto
1.2015 + case (Int A B)
1.2016 + then show ?case
1.2017 + by auto
1.2018 next
1.2019 - { fix x have
1.2020 + case (Basis S)
1.2021 + {
1.2022 + fix x have
1.2023 "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
1.2024 "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
1.2025 - by (induct x) auto }
1.2026 - moreover case (Basis S)
1.2027 + by (induct x) auto
1.2028 + }
1.2029 + moreover note Basis
1.2030 ultimately show ?case
1.2031 by (auto split: ereal.split)
1.2032 qed (fastforce simp add: vimage_Union)+
1.2033 @@ -1657,16 +1974,32 @@
1.2034 unfolding open_generated_order[where 'a=real]
1.2035 proof (induct rule: generate_topology.induct)
1.2036 case (Basis S)
1.2037 - moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
1.2038 - moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
1.2039 + moreover {
1.2040 + fix x
1.2041 + have "ereal ` {..< x} = { -\<infinity> <..< ereal x }"
1.2042 + apply auto
1.2043 + apply (case_tac xa)
1.2044 + apply auto
1.2045 + done
1.2046 + }
1.2047 + moreover {
1.2048 + fix x
1.2049 + have "ereal ` {x <..} = { ereal x <..< \<infinity> }"
1.2050 + apply auto
1.2051 + apply (case_tac xa)
1.2052 + apply auto
1.2053 + done
1.2054 + }
1.2055 ultimately show ?case
1.2056 by auto
1.2057 qed (auto simp add: image_Union image_Int)
1.2058
1.2059 -lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
1.2060 +lemma open_ereal_def:
1.2061 + "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
1.2062 (is "open A \<longleftrightarrow> ?rhs")
1.2063 proof
1.2064 - assume "open A" then show ?rhs
1.2065 + assume "open A"
1.2066 + then show ?rhs
1.2067 using open_PInfty open_MInfty open_ereal_vimage by auto
1.2068 next
1.2069 assume "?rhs"
1.2070 @@ -1678,14 +2011,23 @@
1.2071 by (subst *) (auto simp: open_Un)
1.2072 qed
1.2073
1.2074 -lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
1.2075 +lemma open_PInfty2:
1.2076 + assumes "open A"
1.2077 + and "\<infinity> \<in> A"
1.2078 + obtains x where "{ereal x<..} \<subseteq> A"
1.2079 using open_PInfty[OF assms] by auto
1.2080
1.2081 -lemma open_MInfty2: assumes "open A" "-\<infinity> \<in> A" obtains x where "{..<ereal x} \<subseteq> A"
1.2082 +lemma open_MInfty2:
1.2083 + assumes "open A"
1.2084 + and "-\<infinity> \<in> A"
1.2085 + obtains x where "{..<ereal x} \<subseteq> A"
1.2086 using open_MInfty[OF assms] by auto
1.2087
1.2088 -lemma ereal_openE: assumes "open A" obtains x y where
1.2089 - "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
1.2090 +lemma ereal_openE:
1.2091 + assumes "open A"
1.2092 + obtains x y where "open (ereal -` A)"
1.2093 + and "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
1.2094 + and "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
1.2095 using assms open_ereal_def by auto
1.2096
1.2097 lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
1.2098 @@ -1695,60 +2037,76 @@
1.2099 lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
1.2100 lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
1.2101 lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
1.2102 -
1.2103 +
1.2104 lemma ereal_open_cont_interval:
1.2105 fixes S :: "ereal set"
1.2106 - assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
1.2107 - obtains e where "e>0" "{x-e <..< x+e} \<subseteq> S"
1.2108 -proof-
1.2109 - from `open S` have "open (ereal -` S)" by (rule ereal_openE)
1.2110 - then obtain e where "0 < e" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
1.2111 + assumes "open S"
1.2112 + and "x \<in> S"
1.2113 + and "\<bar>x\<bar> \<noteq> \<infinity>"
1.2114 + obtains e where "e > 0" and "{x-e <..< x+e} \<subseteq> S"
1.2115 +proof -
1.2116 + from `open S`
1.2117 + have "open (ereal -` S)"
1.2118 + by (rule ereal_openE)
1.2119 + then obtain e where "e > 0" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
1.2120 using assms unfolding open_dist by force
1.2121 show thesis
1.2122 proof (intro that subsetI)
1.2123 - show "0 < ereal e" using `0 < e` by auto
1.2124 - fix y assume "y \<in> {x - ereal e<..<x + ereal e}"
1.2125 + show "0 < ereal e"
1.2126 + using `0 < e` by auto
1.2127 + fix y
1.2128 + assume "y \<in> {x - ereal e<..<x + ereal e}"
1.2129 with assms obtain t where "y = ereal t" "dist t (real x) < e"
1.2130 - apply (cases y) by (auto simp: dist_real_def)
1.2131 - then show "y \<in> S" using e[of t] by auto
1.2132 + by (cases y) (auto simp: dist_real_def)
1.2133 + then show "y \<in> S"
1.2134 + using e[of t] by auto
1.2135 qed
1.2136 qed
1.2137
1.2138 lemma ereal_open_cont_interval2:
1.2139 fixes S :: "ereal set"
1.2140 - assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
1.2141 - obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
1.2142 + assumes "open S"
1.2143 + and "x \<in> S"
1.2144 + and x: "\<bar>x\<bar> \<noteq> \<infinity>"
1.2145 + obtains a b where "a < x" and "x < b" and "{a <..< b} \<subseteq> S"
1.2146 proof -
1.2147 obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
1.2148 using assms by (rule ereal_open_cont_interval)
1.2149 - with that[of "x-e" "x+e"] ereal_between[OF x, of e]
1.2150 - show thesis by auto
1.2151 + with that[of "x - e" "x + e"] ereal_between[OF x, of e]
1.2152 + show thesis
1.2153 + by auto
1.2154 qed
1.2155
1.2156 +
1.2157 subsubsection {* Convergent sequences *}
1.2158
1.2159 -lemma lim_ereal[simp]:
1.2160 - "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net" (is "?l = ?r")
1.2161 +lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
1.2162 + (is "?l = ?r")
1.2163 proof (intro iffI topological_tendstoI)
1.2164 - fix S assume "?l" "open S" "x \<in> S"
1.2165 + fix S
1.2166 + assume "?l" and "open S" and "x \<in> S"
1.2167 then show "eventually (\<lambda>x. f x \<in> S) net"
1.2168 using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
1.2169 by (simp add: inj_image_mem_iff)
1.2170 next
1.2171 - fix S assume "?r" "open S" "ereal x \<in> S"
1.2172 + fix S
1.2173 + assume "?r" and "open S" and "ereal x \<in> S"
1.2174 show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
1.2175 using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
1.2176 - using `ereal x \<in> S` by auto
1.2177 + using `ereal x \<in> S`
1.2178 + by auto
1.2179 qed
1.2180
1.2181 lemma lim_real_of_ereal[simp]:
1.2182 assumes lim: "(f ---> ereal x) net"
1.2183 shows "((\<lambda>x. real (f x)) ---> x) net"
1.2184 proof (intro topological_tendstoI)
1.2185 - fix S assume "open S" "x \<in> S"
1.2186 + fix S
1.2187 + assume "open S" and "x \<in> S"
1.2188 then have S: "open S" "ereal x \<in> ereal ` S"
1.2189 by (simp_all add: inj_image_mem_iff)
1.2190 - have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S" by auto
1.2191 + have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S"
1.2192 + by auto
1.2193 from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
1.2194 show "eventually (\<lambda>x. real (f x) \<in> S) net"
1.2195 by (rule eventually_mono)
1.2196 @@ -1756,10 +2114,12 @@
1.2197
1.2198 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
1.2199 proof -
1.2200 - { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
1.2201 - from this[THEN spec, of "real l"]
1.2202 - have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
1.2203 - by (cases l) (auto elim: eventually_elim1) }
1.2204 + {
1.2205 + fix l :: ereal
1.2206 + assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
1.2207 + from this[THEN spec, of "real l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
1.2208 + by (cases l) (auto elim: eventually_elim1)
1.2209 + }
1.2210 then show ?thesis
1.2211 by (auto simp: order_tendsto_iff)
1.2212 qed
1.2213 @@ -1772,20 +2132,26 @@
1.2214 from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
1.2215 moreover
1.2216 assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
1.2217 - then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
1.2218 - ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
1.2219 + then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
1.2220 + by auto
1.2221 + ultimately show "eventually (\<lambda>z. f z \<in> S) F"
1.2222 + by (auto elim!: eventually_elim1)
1.2223 next
1.2224 - fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
1.2225 - from this[rule_format, of "{..< ereal x}"]
1.2226 - show "eventually (\<lambda>y. f y < ereal x) F" by auto
1.2227 + fix x
1.2228 + assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
1.2229 + from this[rule_format, of "{..< ereal x}"] show "eventually (\<lambda>y. f y < ereal x) F"
1.2230 + by auto
1.2231 qed
1.2232
1.2233 lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
1.2234 unfolding tendsto_PInfty eventually_sequentially
1.2235 proof safe
1.2236 - fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
1.2237 - then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n" by blast
1.2238 - moreover have "ereal r < ereal (r + 1)" by auto
1.2239 + fix r
1.2240 + assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
1.2241 + then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n"
1.2242 + by blast
1.2243 + moreover have "ereal r < ereal (r + 1)"
1.2244 + by auto
1.2245 ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
1.2246 by (blast intro: less_le_trans)
1.2247 qed (blast intro: less_imp_le)
1.2248 @@ -1793,9 +2159,12 @@
1.2249 lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
1.2250 unfolding tendsto_MInfty eventually_sequentially
1.2251 proof safe
1.2252 - fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
1.2253 - then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)" by blast
1.2254 - moreover have "ereal (r - 1) < ereal r" by auto
1.2255 + fix r
1.2256 + assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
1.2257 + then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)"
1.2258 + by blast
1.2259 + moreover have "ereal (r - 1) < ereal r"
1.2260 + by auto
1.2261 ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
1.2262 by (blast intro: le_less_trans)
1.2263 qed (blast intro: less_imp_le)
1.2264 @@ -1807,38 +2176,43 @@
1.2265 using LIMSEQ_le_const[of f l "ereal B"] by auto
1.2266
1.2267 lemma tendsto_explicit:
1.2268 - "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
1.2269 + "f ----> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
1.2270 unfolding tendsto_def eventually_sequentially by auto
1.2271
1.2272 -lemma Lim_bounded_PInfty2:
1.2273 - "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
1.2274 +lemma Lim_bounded_PInfty2: "f ----> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
1.2275 using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
1.2276
1.2277 -lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
1.2278 +lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
1.2279 by (intro LIMSEQ_le_const2) auto
1.2280
1.2281 lemma Lim_bounded2_ereal:
1.2282 - assumes lim:"f ----> (l :: 'a::linorder_topology)" and ge: "ALL n>=N. f n >= C"
1.2283 - shows "l>=C"
1.2284 + assumes lim:"f ----> (l :: 'a::linorder_topology)"
1.2285 + and ge: "\<forall>n\<ge>N. f n \<ge> C"
1.2286 + shows "l \<ge> C"
1.2287 using ge
1.2288 by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
1.2289 (auto simp: eventually_sequentially)
1.2290
1.2291 lemma real_of_ereal_mult[simp]:
1.2292 - fixes a b :: ereal shows "real (a * b) = real a * real b"
1.2293 + fixes a b :: ereal
1.2294 + shows "real (a * b) = real a * real b"
1.2295 by (cases rule: ereal2_cases[of a b]) auto
1.2296
1.2297 lemma real_of_ereal_eq_0:
1.2298 - fixes x :: ereal shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
1.2299 + fixes x :: ereal
1.2300 + shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
1.2301 by (cases x) auto
1.2302
1.2303 lemma tendsto_ereal_realD:
1.2304 fixes f :: "'a \<Rightarrow> ereal"
1.2305 - assumes "x \<noteq> 0" and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
1.2306 + assumes "x \<noteq> 0"
1.2307 + and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
1.2308 shows "(f ---> x) net"
1.2309 proof (intro topological_tendstoI)
1.2310 - fix S assume S: "open S" "x \<in> S"
1.2311 - with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
1.2312 + fix S
1.2313 + assume S: "open S" "x \<in> S"
1.2314 + with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}"
1.2315 + by auto
1.2316 from tendsto[THEN topological_tendstoD, OF this]
1.2317 show "eventually (\<lambda>x. f x \<in> S) net"
1.2318 by (rule eventually_rev_mp) (auto simp: ereal_real)
1.2319 @@ -1849,22 +2223,25 @@
1.2320 assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
1.2321 shows "((\<lambda>x. ereal (real (f x))) ---> x) net"
1.2322 proof (intro topological_tendstoI)
1.2323 - fix S assume "open S" "x \<in> S"
1.2324 - with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}" by auto
1.2325 + fix S
1.2326 + assume "open S" and "x \<in> S"
1.2327 + with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}"
1.2328 + by auto
1.2329 from tendsto[THEN topological_tendstoD, OF this]
1.2330 show "eventually (\<lambda>x. ereal (real (f x)) \<in> S) net"
1.2331 by (elim eventually_elim1) (auto simp: ereal_real)
1.2332 qed
1.2333
1.2334 lemma ereal_mult_cancel_left:
1.2335 - fixes a b c :: ereal shows "a * b = a * c \<longleftrightarrow>
1.2336 - ((\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c)"
1.2337 - by (cases rule: ereal3_cases[of a b c])
1.2338 - (simp_all add: zero_less_mult_iff)
1.2339 + fixes a b c :: ereal
1.2340 + shows "a * b = a * c \<longleftrightarrow> (\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c"
1.2341 + by (cases rule: ereal3_cases[of a b c]) (simp_all add: zero_less_mult_iff)
1.2342
1.2343 lemma ereal_inj_affinity:
1.2344 fixes m t :: ereal
1.2345 - assumes "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" "\<bar>t\<bar> \<noteq> \<infinity>"
1.2346 + assumes "\<bar>m\<bar> \<noteq> \<infinity>"
1.2347 + and "m \<noteq> 0"
1.2348 + and "\<bar>t\<bar> \<noteq> \<infinity>"
1.2349 shows "inj_on (\<lambda>x. m * x + t) A"
1.2350 using assms
1.2351 by (cases rule: ereal2_cases[of m t])
1.2352 @@ -1902,108 +2279,136 @@
1.2353 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
1.2354 by (cases x) auto
1.2355
1.2356 -lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
1.2357 +lemma ereal_real':
1.2358 + assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.2359 + shows "ereal (real x) = x"
1.2360 using assms by auto
1.2361
1.2362 -lemma real_ereal_id: "real o ereal = id"
1.2363 -proof-
1.2364 - { fix x have "(real o ereal) x = id x" by auto }
1.2365 - then show ?thesis using ext by blast
1.2366 +lemma real_ereal_id: "real \<circ> ereal = id"
1.2367 +proof -
1.2368 + {
1.2369 + fix x
1.2370 + have "(real o ereal) x = id x"
1.2371 + by auto
1.2372 + }
1.2373 + then show ?thesis
1.2374 + using ext by blast
1.2375 qed
1.2376
1.2377 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
1.2378 -by (metis range_ereal open_ereal open_UNIV)
1.2379 + by (metis range_ereal open_ereal open_UNIV)
1.2380
1.2381 lemma ereal_le_distrib:
1.2382 - fixes a b c :: ereal shows "c * (a + b) \<le> c * a + c * b"
1.2383 + fixes a b c :: ereal
1.2384 + shows "c * (a + b) \<le> c * a + c * b"
1.2385 by (cases rule: ereal3_cases[of a b c])
1.2386 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
1.2387
1.2388 lemma ereal_pos_distrib:
1.2389 - fixes a b c :: ereal assumes "0 \<le> c" "c \<noteq> \<infinity>" shows "c * (a + b) = c * a + c * b"
1.2390 - using assms by (cases rule: ereal3_cases[of a b c])
1.2391 - (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
1.2392 + fixes a b c :: ereal
1.2393 + assumes "0 \<le> c"
1.2394 + and "c \<noteq> \<infinity>"
1.2395 + shows "c * (a + b) = c * a + c * b"
1.2396 + using assms
1.2397 + by (cases rule: ereal3_cases[of a b c])
1.2398 + (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
1.2399
1.2400 lemma ereal_pos_le_distrib:
1.2401 -fixes a b c :: ereal
1.2402 -assumes "c>=0"
1.2403 -shows "c * (a + b) <= c * a + c * b"
1.2404 - using assms by (cases rule: ereal3_cases[of a b c])
1.2405 - (auto simp add: field_simps)
1.2406 + fixes a b c :: ereal
1.2407 + assumes "c \<ge> 0"
1.2408 + shows "c * (a + b) \<le> c * a + c * b"
1.2409 + using assms
1.2410 + by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
1.2411
1.2412 -lemma ereal_max_mono:
1.2413 - "[| (a::ereal) <= b; c <= d |] ==> max a c <= max b d"
1.2414 +lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
1.2415 by (metis sup_ereal_def sup_mono)
1.2416
1.2417 -
1.2418 -lemma ereal_max_least:
1.2419 - "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
1.2420 +lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x"
1.2421 by (metis sup_ereal_def sup_least)
1.2422
1.2423 lemma ereal_LimI_finite:
1.2424 fixes x :: ereal
1.2425 assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.2426 - assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
1.2427 + and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
1.2428 shows "u ----> x"
1.2429 proof (rule topological_tendstoI, unfold eventually_sequentially)
1.2430 - obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
1.2431 - fix S assume "open S" "x : S"
1.2432 - then have "open (ereal -` S)" unfolding open_ereal_def by auto
1.2433 - with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
1.2434 - unfolding open_real_def rx_def by auto
1.2435 + obtain rx where rx: "x = ereal rx"
1.2436 + using assms by (cases x) auto
1.2437 + fix S
1.2438 + assume "open S" and "x \<in> S"
1.2439 + then have "open (ereal -` S)"
1.2440 + unfolding open_ereal_def by auto
1.2441 + with `x \<in> S` obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
1.2442 + unfolding open_real_def rx by auto
1.2443 then obtain n where
1.2444 - upper: "!!N. n <= N ==> u N < x + ereal r" and
1.2445 - lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
1.2446 - show "EX N. ALL n>=N. u n : S"
1.2447 + upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
1.2448 + lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
1.2449 + using assms(2)[of "ereal r"] by auto
1.2450 + show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
1.2451 proof (safe intro!: exI[of _ n])
1.2452 - fix N assume "n <= N"
1.2453 + fix N
1.2454 + assume "n \<le> N"
1.2455 from upper[OF this] lower[OF this] assms `0 < r`
1.2456 - have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
1.2457 - then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
1.2458 - hence "rx < ra + r" and "ra < rx + r"
1.2459 - using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
1.2460 - hence "dist (real (u N)) rx < r"
1.2461 - using rx_def ra_def
1.2462 + have "u N \<notin> {\<infinity>,(-\<infinity>)}"
1.2463 + by auto
1.2464 + then obtain ra where ra_def: "(u N) = ereal ra"
1.2465 + by (cases "u N") auto
1.2466 + then have "rx < ra + r" and "ra < rx + r"
1.2467 + using rx assms `0 < r` lower[OF `n \<le> N`] upper[OF `n \<le> N`]
1.2468 + by auto
1.2469 + then have "dist (real (u N)) rx < r"
1.2470 + using rx ra_def
1.2471 by (auto simp: dist_real_def abs_diff_less_iff field_simps)
1.2472 - from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
1.2473 + from dist[OF this] show "u N \<in> S"
1.2474 + using `u N \<notin> {\<infinity>, -\<infinity>}`
1.2475 by (auto simp: ereal_real split: split_if_asm)
1.2476 qed
1.2477 qed
1.2478
1.2479 lemma tendsto_obtains_N:
1.2480 assumes "f ----> f0"
1.2481 - assumes "open S" "f0 : S"
1.2482 - obtains N where "ALL n>=N. f n : S"
1.2483 + assumes "open S"
1.2484 + and "f0 \<in> S"
1.2485 + obtains N where "\<forall>n\<ge>N. f n \<in> S"
1.2486 using assms using tendsto_def
1.2487 using tendsto_explicit[of f f0] assms by auto
1.2488
1.2489 lemma ereal_LimI_finite_iff:
1.2490 fixes x :: ereal
1.2491 assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.2492 - shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
1.2493 - (is "?lhs <-> ?rhs")
1.2494 + shows "u ----> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
1.2495 + (is "?lhs \<longleftrightarrow> ?rhs")
1.2496 proof
1.2497 assume lim: "u ----> x"
1.2498 - { fix r assume "(r::ereal)>0"
1.2499 - then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
1.2500 + {
1.2501 + fix r :: ereal
1.2502 + assume "r > 0"
1.2503 + then obtain N where "\<forall>n\<ge>N. u n \<in> {x - r <..< x + r}"
1.2504 apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
1.2505 - using lim ereal_between[of x r] assms `r>0` by auto
1.2506 - hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
1.2507 - using ereal_minus_less[of r x] by (cases r) auto
1.2508 - } then show "?rhs" by auto
1.2509 + using lim ereal_between[of x r] assms `r > 0`
1.2510 + apply auto
1.2511 + done
1.2512 + then have "\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
1.2513 + using ereal_minus_less[of r x]
1.2514 + by (cases r) auto
1.2515 + }
1.2516 + then show ?rhs
1.2517 + by auto
1.2518 next
1.2519 - assume ?rhs then show "u ----> x"
1.2520 + assume ?rhs
1.2521 + then show "u ----> x"
1.2522 using ereal_LimI_finite[of x] assms by auto
1.2523 qed
1.2524
1.2525 lemma ereal_Limsup_uminus:
1.2526 - fixes f :: "'a => ereal"
1.2527 - shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
1.2528 + fixes f :: "'a \<Rightarrow> ereal"
1.2529 + shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
1.2530 unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
1.2531
1.2532 lemma liminf_bounded_iff:
1.2533 fixes x :: "nat \<Rightarrow> ereal"
1.2534 - shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
1.2535 + shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)"
1.2536 + (is "?lhs \<longleftrightarrow> ?rhs")
1.2537 unfolding le_Liminf_iff eventually_sequentially ..
1.2538
1.2539 lemma
1.2540 @@ -2012,6 +2417,7 @@
1.2541 and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
1.2542 unfolding incseq_def decseq_def by auto
1.2543
1.2544 +
1.2545 subsubsection {* Tests for code generator *}
1.2546
1.2547 (* A small list of simple arithmetic expressions *)