41973

1 
(* Title: Extended_Reals.thy


2 
Author: Johannes Hölzl, Robert Himmelmann, Armin Heller; TU München


3 
Author: Bogdan Grechuk; University of Edinburgh *)


4 


5 
header {* Extended real number line *}


6 


7 
theory Extended_Reals


8 
imports Topology_Euclidean_Space


9 
begin


10 


11 
subsection {* Definition and basic properties *}


12 


13 
datatype extreal = extreal real  PInfty  MInfty


14 


15 
notation (xsymbols)


16 
PInfty ("\<infinity>")


17 


18 
notation (HTML output)


19 
PInfty ("\<infinity>")


20 


21 
instantiation extreal :: uminus


22 
begin


23 
fun uminus_extreal where


24 
" (extreal r) = extreal ( r)"


25 
 " \<infinity> = MInfty"


26 
 " MInfty = \<infinity>"


27 
instance ..


28 
end


29 


30 
lemma MInfty_neq_PInfty[simp]:


31 
"\<infinity> \<noteq>  \<infinity>" " \<infinity> \<noteq> \<infinity>" by simp_all


32 


33 
lemma MInfty_neq_extreal[simp]:


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


35 


36 
lemma MInfinity_cases[simp]:


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


38 
by simp


39 


40 
lemma extreal_uminus_uminus[simp]:


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


42 
by (cases a) simp_all


43 


44 
lemma MInfty_eq[simp]:


45 
"MInfty =  \<infinity>" by simp


46 


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


48 


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


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


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


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


53 
shows P


54 
using assms by (cases x) auto


55 


56 
lemma extreal2_cases[case_names


57 
real_real real_PInf real_MInf


58 
PInf_real PInf_PInf PInf_MInf


59 
MInf_real MInf_PInf MInf_MInf]:


60 
assumes "\<And>r p. y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"


61 
assumes "\<And>p. y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


62 
assumes "\<And>p. y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


63 
assumes "\<And>r. y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


64 
assumes "y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


65 
assumes "y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


66 
assumes "\<And>r. y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


67 
assumes "y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


68 
assumes "y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


69 
shows P


70 
apply (cases x)


71 
apply (cases y) using assms apply simp_all


72 
apply (cases y) using assms apply simp_all


73 
apply (cases y) using assms apply simp_all


74 
done


75 


76 
lemma extreal3_cases[case_names


77 
real_real_real real_real_PInf real_real_MInf


78 
real_PInf_real real_PInf_PInf real_PInf_MInf


79 
real_MInf_real real_MInf_PInf real_MInf_MInf


80 
PInf_real_real PInf_real_PInf PInf_real_MInf


81 
PInf_PInf_real PInf_PInf_PInf PInf_PInf_MInf


82 
PInf_MInf_real PInf_MInf_PInf PInf_MInf_MInf


83 
MInf_real_real MInf_real_PInf MInf_real_MInf


84 
MInf_PInf_real MInf_PInf_PInf MInf_PInf_MInf


85 
MInf_MInf_real MInf_MInf_PInf MInf_MInf_MInf]:


86 
assumes "\<And>r p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"


87 
assumes "\<And>p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


88 
assumes "\<And>p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


89 
assumes "\<And>r q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


90 
assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


91 
assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


92 
assumes "\<And>q r. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


93 
assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


94 
assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


95 
assumes "\<And>r p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"


96 
assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


97 
assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


98 
assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


99 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


100 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


101 
assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


102 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


103 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


104 
assumes "\<And>r p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"


105 
assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


106 
assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


107 
assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


108 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


109 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


110 
assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"


111 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


112 
assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"


113 
shows P


114 
apply (cases x)


115 
apply (cases rule: extreal2_cases[of y z]) using assms apply simp_all


116 
apply (cases rule: extreal2_cases[of y z]) using assms apply simp_all


117 
apply (cases rule: extreal2_cases[of y z]) using assms apply simp_all


118 
done


119 


120 
lemma extreal_uminus_eq_iff[simp]:


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


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


123 


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


125 
"of_extreal (extreal r) = r" 


126 
"of_extreal \<infinity> = 0" 


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


128 
by (auto intro: extreal_cases)


129 
termination proof qed (rule wf_empty)


130 


131 
defs (overloaded)


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


133 


134 
lemma real_of_extreal[simp]:


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


136 
"real (extreal r) = r"


137 
"real \<infinity> = 0"


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


139 


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


141 
proof safe


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


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


144 
qed auto


145 


146 
instantiation extreal :: number


147 
begin


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


149 
instance proof qed


150 
end


151 


152 
subsubsection "Addition"


153 


154 
instantiation extreal :: comm_monoid_add


155 
begin


156 


157 
definition "0 = extreal 0"


158 


159 
function plus_extreal where


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


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


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


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


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


165 
"\<infinity> + \<infinity> = \<infinity>"


166 
proof 


167 
case (goal1 P x)


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


169 
ultimately show P


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


171 
qed auto


172 
termination proof qed (rule wf_empty)


173 


174 
lemma Infty_neq_0[simp]:


175 
"\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>"


176 
"\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>"


177 
by (simp_all add: zero_extreal_def)


178 


179 
lemma extreal_eq_0[simp]:


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


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


182 
unfolding zero_extreal_def by simp_all


183 


184 
instance


185 
proof


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


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


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


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


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


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


192 
qed


193 
end


194 


195 
lemma extreal_uminus_zero[simp]:


196 
" 0 = (0::extreal)"


197 
by (simp add: zero_extreal_def)


198 


199 
lemma extreal_uminus_zero_iff[simp]:


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


201 
by (cases a) simp_all


202 


203 
lemma extreal_plus_eq_PInfty[simp]:


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


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


206 


207 
lemma extreal_plus_eq_MInfty[simp]:


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


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


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


211 


212 
lemma extreal_add_cancel_left:


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


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


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


216 


217 
lemma extreal_add_cancel_right:


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


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


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


221 


222 
lemma extreal_real:


223 
"extreal (real x) = (if x = \<infinity> \<or> x = \<infinity> then 0 else x)"


224 
by (cases x) simp_all


225 


226 
subsubsection "Linear order on @{typ extreal}"


227 


228 
instantiation extreal :: linorder


229 
begin


230 


231 
function less_extreal where


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


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


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


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


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


237 
" \<infinity> < \<infinity> \<longleftrightarrow> True"


238 
proof 


239 
case (goal1 P x)


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


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


242 
qed simp_all


243 
termination by (relation "{}") simp


244 


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


246 


247 
lemma extreal_infty_less[simp]:


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


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


250 
by (cases x, simp_all) (cases x, simp_all)


251 


252 
lemma extreal_infty_less_eq[simp]:


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


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


255 
by (auto simp add: less_eq_extreal_def)


256 


257 
lemma extreal_less[simp]:


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


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


260 
"0 < \<infinity>"


261 
"\<infinity> < 0"


262 
by (simp_all add: zero_extreal_def)


263 


264 
lemma extreal_less_eq[simp]:


265 
"x \<le> \<infinity>"


266 
"\<infinity> \<le> x"


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


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


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


270 
by (auto simp add: less_eq_extreal_def zero_extreal_def)


271 


272 
lemma extreal_infty_less_eq2:


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


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


275 
by simp_all


276 


277 
instance


278 
proof


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


280 
by (cases x) simp_all


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


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


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


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


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


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


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


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


289 
qed


290 
end


291 


292 
lemma extreal_MInfty_lessI[intro, simp]:


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


294 
by (cases a) auto


295 


296 
lemma extreal_less_PInfty[intro, simp]:


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


298 
by (cases a) auto


299 


300 
lemma extreal_less_extreal_Ex:


301 
fixes a b :: extreal


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


303 
by (cases x) auto


304 


305 
lemma extreal_add_mono:


306 
fixes a b c d :: extreal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d"


307 
using assms


308 
apply (cases a)


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


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


311 
done


312 


313 
lemma extreal_minus_le_minus[simp]:


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


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


316 


317 
lemma extreal_minus_less_minus[simp]:


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


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


320 


321 
lemma extreal_le_real_iff:


322 
"x \<le> real y \<longleftrightarrow> ((y \<noteq> \<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> extreal x \<le> y) \<and> (y = \<infinity> \<or> y = \<infinity> \<longrightarrow> x \<le> 0))"


323 
by (cases y) auto


324 


325 
lemma real_le_extreal_iff:


326 
"real y \<le> x \<longleftrightarrow> ((y \<noteq> \<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> y \<le> extreal x) \<and> (y = \<infinity> \<or> y = \<infinity> \<longrightarrow> 0 \<le> x))"


327 
by (cases y) auto


328 


329 
lemma extreal_less_real_iff:


330 
"x < real y \<longleftrightarrow> ((y \<noteq> \<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> extreal x < y) \<and> (y = \<infinity> \<or> y = \<infinity> \<longrightarrow> x < 0))"


331 
by (cases y) auto


332 


333 
lemma real_less_extreal_iff:


334 
"real y < x \<longleftrightarrow> ((y \<noteq> \<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> y < extreal x) \<and> (y = \<infinity> \<or> y = \<infinity> \<longrightarrow> 0 < x))"


335 
by (cases y) auto


336 


337 
lemmas real_of_extreal_ord_simps =


338 
extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff


339 


340 
lemma extreal_dense:


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


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


343 
proof 


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


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


346 
moreover


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


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


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


350 
} ultimately have ?thesis by auto


351 
}


352 
moreover


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


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


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


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


357 
moreover


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


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


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


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


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


363 
} ultimately have ?thesis by auto


364 
} ultimately show ?thesis by auto


365 
qed


366 


367 
lemma extreal_dense2:


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


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


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


371 


372 
subsubsection "Multiplication"


373 


374 
instantiation extreal :: comm_monoid_mult


375 
begin


376 


377 
definition "1 = extreal 1"


378 


379 
function times_extreal where


380 
"extreal r * extreal p = extreal (r * p)" 


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


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


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


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


385 
"\<infinity> * \<infinity> = \<infinity>" 


386 
"\<infinity> * \<infinity> = \<infinity>" 


387 
"\<infinity> * \<infinity> = \<infinity>" 


388 
"\<infinity> * \<infinity> = \<infinity>"


389 
proof 


390 
case (goal1 P x)


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


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


393 
qed simp_all


394 
termination by (relation "{}") simp


395 


396 
instance


397 
proof


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


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


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


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


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


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


404 
(simp_all add: zero_extreal_def zero_less_mult_iff)


405 
qed


406 
end


407 


408 
lemma extreal_mult_zero[simp]:


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


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


411 


412 
lemma extreal_zero_mult[simp]:


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


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


415 


416 
lemma extreal_m1_less_0[simp]:


417 
"(1::extreal) < 0"


418 
by (simp add: zero_extreal_def one_extreal_def)


419 


420 
lemma extreal_zero_m1[simp]:


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


422 
by (simp add: zero_extreal_def one_extreal_def)


423 


424 
lemma extreal_times_0[simp]:


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


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


427 


428 
lemma extreal_times[simp]:


429 
"1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1"


430 
"1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1"


431 
by (auto simp add: times_extreal_def one_extreal_def)


432 


433 
lemma extreal_plus_1[simp]:


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


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


436 
unfolding one_extreal_def by auto


437 


438 
lemma extreal_zero_times[simp]:


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


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


441 


442 
lemma extreal_mult_eq_PInfty[simp]:


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


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


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


446 


447 
lemma extreal_mult_eq_MInfty[simp]:


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


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


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


451 


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


453 
by (simp_all add: zero_extreal_def one_extreal_def)


454 


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


456 
by (simp_all add: zero_extreal_def one_extreal_def)


457 


458 
lemma extreal_mult_minus_left[simp]:


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


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


461 


462 
lemma extreal_mult_minus_right[simp]:


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


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


465 


466 
lemma extreal_mult_infty[simp]:


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


468 
by (cases a) auto


469 


470 
lemma extreal_infty_mult[simp]:


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


472 
by (cases a) auto


473 


474 
lemma extreal_mult_strict_right_mono:


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


476 
shows "a * c < b * c"


477 
using assms


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


479 
(auto simp: zero_le_mult_iff extreal_less_PInfty)


480 


481 
lemma extreal_mult_strict_left_mono:


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


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


484 


485 
lemma extreal_mult_right_mono:


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


487 
using assms


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


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


490 
(auto simp: zero_le_mult_iff extreal_less_PInfty)


491 


492 
lemma extreal_mult_left_mono:


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


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


495 


496 
subsubsection {* Subtraction *}


497 


498 
lemma extreal_minus_minus_image[simp]:


499 
fixes S :: "extreal set"


500 
shows "uminus ` uminus ` S = S"


501 
by (auto simp: image_iff)


502 


503 
lemma extreal_uminus_lessThan[simp]:


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


505 
proof (safe intro!: image_eqI)


506 
fix x assume "a < x"


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


508 
then show " x < a" by simp


509 
qed auto


510 


511 
lemma extreal_uminus_greaterThan[simp]:


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


513 
by (metis extreal_uminus_lessThan extreal_uminus_uminus


514 
extreal_minus_minus_image)


515 


516 
instantiation extreal :: minus


517 
begin


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


519 
instance ..


520 
end


521 


522 
lemma extreal_minus[simp]:


523 
"extreal r  extreal p = extreal (r  p)"


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


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


526 
"\<infinity>  x = \<infinity>"


527 
"\<infinity>  \<infinity> = \<infinity>"


528 
"x  y = x + y"


529 
"x  0 = x"


530 
"0  x = x"


531 
by (simp_all add: minus_extreal_def)


532 


533 
lemma extreal_x_minus_x[simp]:


534 
"x  x = (if x = \<infinity> \<or> x = \<infinity> then \<infinity> else 0)"


535 
by (cases x) simp_all


536 


537 
lemma extreal_eq_minus_iff:


538 
fixes x y z :: extreal


539 
shows "x = z  y \<longleftrightarrow>


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


541 
(y = \<infinity> \<longrightarrow> x = \<infinity>) \<and>


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


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


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


545 


546 
lemma extreal_eq_minus:


547 
fixes x y z :: extreal


548 
shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> x = z  y \<longleftrightarrow> x + y = z"


549 
by (simp add: extreal_eq_minus_iff)


550 


551 
lemma extreal_less_minus_iff:


552 
fixes x y z :: extreal


553 
shows "x < z  y \<longleftrightarrow>


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


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


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


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


558 


559 
lemma extreal_less_minus:


560 
fixes x y z :: extreal


561 
shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> x < z  y \<longleftrightarrow> x + y < z"


562 
by (simp add: extreal_less_minus_iff)


563 


564 
lemma extreal_le_minus_iff:


565 
fixes x y z :: extreal


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


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


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


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


570 


571 
lemma extreal_le_minus:


572 
fixes x y z :: extreal


573 
shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> x \<le> z  y \<longleftrightarrow> x + y \<le> z"


574 
by (simp add: extreal_le_minus_iff)


575 


576 
lemma extreal_minus_less_iff:


577 
fixes x y z :: extreal


578 
shows "x  y < z \<longleftrightarrow>


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


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


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


582 


583 
lemma extreal_minus_less:


584 
fixes x y z :: extreal


585 
shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> x  y < z \<longleftrightarrow> x < z + y"


586 
by (simp add: extreal_minus_less_iff)


587 


588 
lemma extreal_minus_le_iff:


589 
fixes x y z :: extreal


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


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


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


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


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


595 


596 
lemma extreal_minus_le:


597 
fixes x y z :: extreal


598 
shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> x  y \<le> z \<longleftrightarrow> x \<le> z + y"


599 
by (simp add: extreal_minus_le_iff)


600 


601 
lemma extreal_minus_eq_minus_iff:


602 
fixes a b c :: extreal


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


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


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


606 


607 
lemma extreal_add_le_add_iff:


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


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


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


611 


612 
lemma extreal_mult_le_mult_iff:


613 
"c \<noteq> \<infinity> \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow>


614 
(0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"


615 
by (cases rule: extreal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)


616 


617 
lemma extreal_between:


618 
fixes x e :: extreal


619 
assumes "x \<noteq> \<infinity>" "x \<noteq> \<infinity>" "0 < e"


620 
shows "x  e < x" "x < x + e"


621 
using assms apply (cases x, cases e) apply auto


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


623 


624 
lemma extreal_distrib:


625 
fixes a b c :: extreal


626 
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" "c \<noteq> \<infinity>" "c \<noteq> \<infinity>"


627 
shows "(a + b) * c = a * c + b * c"


628 
using assms


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


630 


631 
subsubsection {* Division *}


632 


633 
instantiation extreal :: inverse


634 
begin


635 


636 
function inverse_extreal where


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


638 
"inverse \<infinity> = 0" 


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


640 
by (auto intro: extreal_cases)


641 
termination by (relation "{}") simp


642 


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


644 


645 
instance proof qed


646 
end


647 


648 
lemma extreal_inverse[simp]:


649 
"inverse 0 = \<infinity>"


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


651 
by (simp_all add: one_extreal_def zero_extreal_def)


652 


653 
lemma extreal_divide[simp]:


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


655 
unfolding divide_extreal_def by (auto simp: divide_real_def)


656 


657 
lemma extreal_divide_same[simp]:


658 
"x / x = (if x = \<infinity> \<or> x = \<infinity> \<or> x = 0 then 0 else 1)"


659 
by (cases x)


660 
(simp_all add: divide_real_def divide_extreal_def one_extreal_def)


661 


662 
lemma extreal_inv_inv[simp]:


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


664 
by (cases x) auto


665 


666 
lemma extreal_inverse_minus[simp]:


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


668 
by (cases x) simp_all


669 


670 
lemma extreal_uminus_divide[simp]:


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


672 
unfolding divide_extreal_def by simp


673 


674 
lemma extreal_divide_Infty[simp]:


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


676 
unfolding divide_extreal_def by simp_all


677 


678 
lemma extreal_divide_one[simp]:


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


680 
unfolding divide_extreal_def by simp


681 


682 
lemma extreal_divide_extreal[simp]:


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


684 
unfolding divide_extreal_def by simp


685 


686 
lemma extreal_mult_le_0_iff:


687 
fixes a b :: extreal


688 
shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)"


689 
by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_le_0_iff)


690 


691 
lemma extreal_zero_le_0_iff:


692 
fixes a b :: extreal


693 
shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)"


694 
by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_le_mult_iff)


695 


696 
lemma extreal_mult_less_0_iff:


697 
fixes a b :: extreal


698 
shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)"


699 
by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_less_0_iff)


700 


701 
lemma extreal_zero_less_0_iff:


702 
fixes a b :: extreal


703 
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"


704 
by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_less_mult_iff)


705 


706 
lemma extreal_le_divide_pos:


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


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


709 


710 
lemma extreal_divide_le_pos:


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


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


713 


714 
lemma extreal_le_divide_neg:


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


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


717 


718 
lemma extreal_divide_le_neg:


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


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


721 


722 
lemma extreal_inverse_antimono_strict:


723 
fixes x y :: extreal


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


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


726 


727 
lemma extreal_inverse_antimono:


728 
fixes x y :: extreal


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


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


731 


732 
lemma inverse_inverse_Pinfty_iff[simp]:


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


734 
by (cases x) auto


735 


736 
lemma extreal_inverse_eq_0:


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


738 
by (cases x) auto


739 


740 
lemma extreal_mult_less_right:


741 
assumes "b * a < c * a" "0 < a" "a < \<infinity>"


742 
shows "b < c"


743 
using assms


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


745 
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)


746 


747 
subsection "Complete lattice"


748 


749 
lemma extreal_bot:


750 
fixes x :: extreal assumes "\<And>B. x \<le> extreal B" shows "x =  \<infinity>"


751 
proof (cases x)


752 
case (real r) with assms[of "r  1"] show ?thesis by auto


753 
next case PInf with assms[of 0] show ?thesis by auto


754 
next case MInf then show ?thesis by simp


755 
qed


756 


757 
lemma extreal_top:


758 
fixes x :: extreal assumes "\<And>B. x \<ge> extreal B" shows "x = \<infinity>"


759 
proof (cases x)


760 
case (real r) with assms[of "r + 1"] show ?thesis by auto


761 
next case MInf with assms[of 0] show ?thesis by auto


762 
next case PInf then show ?thesis by simp


763 
qed


764 


765 
instantiation extreal :: lattice


766 
begin


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


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


769 
instance proof qed simp_all


770 
end


771 


772 
instantiation extreal :: complete_lattice


773 
begin


774 


775 
definition "bot = (\<infinity>)"


776 
definition "top = \<infinity>"


777 


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


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


780 


781 
lemma extreal_complete_Sup:


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


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


784 
proof cases


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


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


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


788 
show ?thesis


789 
proof cases


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


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


792 
next


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


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


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


796 
by (auto simp: real_of_extreal_ord_simps)


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


798 
obtain s where s:


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


800 
by auto


801 
show ?thesis


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


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


804 
proof (cases z)


805 
case (real r)


806 
then show ?thesis


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


808 
qed auto


809 
next


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


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


812 
proof (cases z)


813 
case (real u)


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


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


816 
then show ?thesis using real by simp


817 
qed auto


818 
qed


819 
qed


820 
next


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


822 
show ?thesis


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


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


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


826 
proof (cases y)


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


828 
qed auto


829 
qed simp


830 
qed


831 


832 
lemma extreal_complete_Inf:


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


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


835 
proof


836 
def S1 == "uminus ` S"


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


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


839 
using extreal_complete_Sup[of S1] by auto


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


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


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


843 
hence "z <= x"


844 
apply (subst extreal_uminus_uminus[symmetric])


845 
unfolding extreal_minus_le_minus . }


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


847 
using x_def unfolding S1_def


848 
apply simp


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


850 
unfolding extreal_minus_le_minus by simp


851 
ultimately show ?thesis by auto


852 
qed


853 


854 
lemma extreal_complete_uminus_eq:


855 
fixes S :: "extreal set"


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


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


858 
by simp (metis extreal_minus_le_minus extreal_uminus_uminus)


859 


860 
lemma extreal_Sup_uminus_image_eq:


861 
fixes S :: "extreal set"


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


863 
proof cases


864 
assume "S = {}"


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


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


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


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


869 
ultimately show ?thesis unfolding Inf_extreal_def Sup_extreal_def


870 
Least_def Greatest_def GreatestM_def by simp


871 
next


872 
assume "S \<noteq> {}"


873 
with extreal_complete_Sup[of "uminus`S"]


874 
obtain x where x: "(\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"


875 
unfolding extreal_complete_uminus_eq by auto


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


877 
unfolding Inf_extreal_def Greatest_def GreatestM_def


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


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


880 
using x .


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


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


883 
unfolding extreal_complete_uminus_eq by simp


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


885 
unfolding Sup_extreal_def extreal_uminus_eq_iff


886 
by (intro Least_equality) auto


887 
qed


888 
qed


889 


890 
instance


891 
proof


892 
{ fix x :: extreal and A


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


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


895 


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


897 
with extreal_complete_Sup[of A]


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


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


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


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


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


903 
note le_Sup = this


904 


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


906 
show "Sup A <= x"


907 
proof (cases "A = {}")


908 
case True


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


910 
by (auto intro!: Least_equality)


911 
thus "Sup A <= x" by simp


912 
next


913 
case False


914 
with extreal_complete_Sup[of A]


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


916 
hence "Sup A = s"


917 
unfolding Sup_extreal_def by (auto intro!: Least_equality)


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


919 
finally show "Sup A <= x" .


920 
qed }


921 
note Sup_le = this


922 


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


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


925 
unfolding extreal_Sup_uminus_image_eq by simp }


926 


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


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


929 
unfolding extreal_Sup_uminus_image_eq by force }


930 
qed


931 
end


932 


933 
lemma extreal_SUPR_uminus:


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


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


936 
unfolding SUPR_def INFI_def


937 
using extreal_Sup_uminus_image_eq[of "f`R"]


938 
by (simp add: image_image)


939 


940 
lemma extreal_INFI_uminus:


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


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


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


944 


945 
lemma extreal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: extreal set)"


946 
by (auto intro!: inj_onI)


947 


948 
lemma extreal_image_uminus_shift:


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


950 
proof


951 
assume "uminus ` X = Y"


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


953 
by (simp add: inj_image_eq_iff)


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


955 
qed (simp add: image_image)


956 


957 
lemma Inf_extreal_iff:


958 
fixes z :: extreal


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


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


961 
order_less_le_trans)


962 


963 
lemma Sup_eq_MInfty:


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


965 
proof


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


967 
with complete_lattice_class.Sup_upper[of _ S]


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


969 
next


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


971 
unfolding Sup_extreal_def by (auto intro!: Least_equality)


972 
qed


973 


974 
lemma Inf_eq_PInfty:


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


976 
using Sup_eq_MInfty[of "uminus`S"]


977 
unfolding extreal_Sup_uminus_image_eq extreal_image_uminus_shift by simp


978 


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


980 
unfolding Inf_extreal_def


981 
by (auto intro!: Greatest_equality)


982 


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


984 
unfolding Sup_extreal_def


985 
by (auto intro!: Least_equality)


986 


987 
lemma extreal_SUPI:


988 
fixes x :: extreal


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


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


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


992 
unfolding SUPR_def Sup_extreal_def


993 
using assms by (auto intro!: Least_equality)


994 


995 
lemma extreal_INFI:


996 
fixes x :: extreal


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


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


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


1000 
unfolding INFI_def Inf_extreal_def


1001 
using assms by (auto intro!: Greatest_equality)


1002 


1003 
lemma Sup_extreal_close:


1004 
fixes e :: extreal


1005 
assumes "0 < e" and S: "Sup S \<noteq> \<infinity>" "Sup S \<noteq> \<infinity>" "S \<noteq> {}"


1006 
shows "\<exists>x\<in>S. Sup S  e < x"


1007 
proof (rule less_Sup_iff[THEN iffD1])


1008 
show "Sup S  e < Sup S " using assms


1009 
by (cases "Sup S", cases e) auto


1010 
qed


1011 


1012 
lemma Inf_extreal_close:


1013 
fixes e :: extreal assumes "Inf X \<noteq> \<infinity>" "Inf X \<noteq> \<infinity>" "0 < e"


1014 
shows "\<exists>x\<in>X. x < Inf X + e"


1015 
proof (rule Inf_less_iff[THEN iffD1])


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


1017 
by (cases "Inf X", cases e) auto


1018 
qed


1019 


1020 
lemma (in complete_lattice) top_le:


1021 
"top \<le> x \<Longrightarrow> x = top"


1022 
by (rule antisym) auto


1023 


1024 
lemma Sup_eq_top_iff:


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


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


1027 
proof


1028 
assume *: "Sup A = top"


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


1030 
proof (intro allI impI)


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


1032 
unfolding less_Sup_iff by auto


1033 
qed


1034 
next


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


1036 
show "Sup A = top"


1037 
proof (rule ccontr)


1038 
assume "Sup A \<noteq> top"


1039 
with top_greatest[of "Sup A"]


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


1041 
then have "Sup A < Sup A"


1042 
using * unfolding less_Sup_iff by auto


1043 
then show False by auto


1044 
qed


1045 
qed


1046 


1047 
lemma SUP_eq_top_iff:


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


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


1050 
unfolding SUPR_def Sup_eq_top_iff by auto


1051 


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


1053 
proof 


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


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


1056 
proof (cases x)


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


1058 
next


1059 
case (real r)


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


1061 
using ex_less_of_nat by (auto simp: real_eq_of_nat)


1062 
ultimately show ?thesis by auto


1063 
qed simp }


1064 
then show ?thesis


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


1066 
by (auto simp: top_extreal_def)


1067 
qed


1068 


1069 
lemma infeal_le_Sup:


1070 
fixes x :: extreal


1071 
shows "(x <= (SUP i:A. f i)) <> (ALL y. y < x > (EX i. i : A & y <= f i))"


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


1073 
proof


1074 
{ assume "?rhs"


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


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


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


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


1079 
hence False using y_def by auto


1080 
} hence "?lhs" by auto


1081 
}


1082 
moreover


1083 
{ assume "?lhs" hence "?rhs"


1084 
by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff


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


1086 
} ultimately show ?thesis by auto


1087 
qed


1088 


1089 
lemma infeal_Inf_le:


1090 
fixes x :: extreal


1091 
shows "((INF i:A. f i) <= x) <> (ALL y. x < y > (EX i. i : A & f i <= y))"


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


1093 
proof


1094 
{ assume "?rhs"


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


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


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


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


1099 
hence False using y_def by auto


1100 
} hence "?lhs" by auto


1101 
}


1102 
moreover


1103 
{ assume "?lhs" hence "?rhs"


1104 
by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff


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


1106 
} ultimately show ?thesis by auto


1107 
qed


1108 


1109 
lemma Inf_less:


1110 
fixes x :: extreal


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


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


1113 
proof(rule ccontr)


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


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


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


1117 
thus False using assms by auto


1118 
qed


1119 


1120 
lemma same_INF:


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


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


1123 
proof


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


1125 
thus ?thesis unfolding INFI_def by auto


1126 
qed


1127 


1128 
lemma same_SUP:


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


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


1131 
proof


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


1133 
thus ?thesis unfolding SUPR_def by auto


1134 
qed


1135 


1136 
subsection "Limits on @{typ extreal}"


1137 


1138 
subsubsection "Topological space"


1139 


1140 
instantiation extreal :: topological_space


1141 
begin


1142 


1143 
definition "open A \<longleftrightarrow>


1144 
(\<exists>T. open T \<and> extreal ` T = A  {\<infinity>, \<infinity>})


1145 
\<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {extreal x <..} \<subseteq> A))


1146 
\<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<extreal x} \<subseteq> A))"


1147 


1148 
lemma open_PInfty: "open A ==> \<infinity> : A ==> (EX x. {extreal x<..} <= A)"


1149 
unfolding open_extreal_def by auto


1150 


1151 
lemma open_MInfty: "open A ==> (\<infinity>) : A ==> (EX x. {..<extreal x} <= A)"


1152 
unfolding open_extreal_def by auto


1153 


1154 
lemma open_PInfty2: assumes "open A" "\<infinity> : A" obtains x where "{extreal x<..} <= A"


1155 
using open_PInfty[OF assms] by auto


1156 


1157 
lemma open_MInfty2: assumes "open A" "(\<infinity>) : A" obtains x where "{..<extreal x} <= A"


1158 
using open_MInfty[OF assms] by auto


1159 


1160 
lemma extreal_openE: assumes "open A" obtains A' x y where


1161 
"open A'" "extreal ` A' = A  {\<infinity>, (\<infinity>)}"


1162 
"\<infinity> : A ==> {extreal x<..} <= A"


1163 
"(\<infinity>) : A ==> {..<extreal y} <= A"


1164 
using assms open_extreal_def by auto


1165 


1166 
instance


1167 
proof


1168 
let ?U = "UNIV::extreal set"


1169 
show "open ?U" unfolding open_extreal_def


1170 
by (auto intro!: exI[of _ "UNIV"] exI[of _ 0])


1171 
next


1172 
fix S T::"extreal set" assume "open S" and "open T"


1173 
from `open S`[THEN extreal_openE] guess S' xS yS . note S' = this


1174 
from `open T`[THEN extreal_openE] guess T' xT yT . note T' = this


1175 


1176 
have "extreal ` (S' Int T') = (extreal ` S') Int (extreal ` T')" by auto


1177 
also have "... = S Int T  {\<infinity>, (\<infinity>)}" using S' T' by auto


1178 
finally have "extreal ` (S' Int T') = S Int T  {\<infinity>, (\<infinity>)}" by auto


1179 
moreover have "open (S' Int T')" using S' T' by auto


1180 
moreover


1181 
{ assume a: "\<infinity> : S Int T"


1182 
hence "EX x. {extreal x<..} <= S Int T"


1183 
apply(rule_tac x="max xS xT" in exI)


1184 
proof


1185 
{ fix x assume *: "extreal (max xS xT) < x"


1186 
hence "x : S Int T" apply (cases x, auto simp: max_def split: split_if_asm)


1187 
using a S' T' by auto


1188 
} thus "{extreal (max xS xT)<..} <= S Int T" by auto


1189 
qed }


1190 
moreover


1191 
{ assume a: "(\<infinity>) : S Int T"


1192 
hence "EX x. {..<extreal x} <= S Int T"


1193 
apply(rule_tac x="min yS yT" in exI)


1194 
proof


1195 
{ fix x assume *: "extreal (min yS yT) > x"


1196 
hence "x<extreal yS & x<extreal yT" by (cases x) auto


1197 
hence "x : S Int T" using a S' T' by auto


1198 
} thus "{..<extreal (min yS yT)} <= S Int T" by auto


1199 
qed }


1200 
ultimately show "open (S Int T)" unfolding open_extreal_def by auto


1201 
next


1202 
fix K assume openK: "ALL S : K. open (S:: extreal set)"


1203 
hence "ALL S:K. EX T. open T & extreal ` T = S  {\<infinity>, (\<infinity>)}" by (auto simp: open_extreal_def)


1204 
from bchoice[OF this] guess T .. note T = this[rule_format]


1205 


1206 
show "open (Union K)" unfolding open_extreal_def


1207 
proof (safe intro!: exI[of _ "Union (T ` K)"])


1208 
fix x S assume "x : T S" "S : K"


1209 
with T[OF `S : K`] show "extreal x : Union K" by auto


1210 
next


1211 
fix x S assume x: "x ~: extreal ` (Union (T ` K))" "S : K" "x : S" "x ~= \<infinity>"


1212 
hence "x ~: extreal ` (T S)"


1213 
by (auto simp: image_UN UN_simps[symmetric] simp del: UN_simps)


1214 
thus "x=(\<infinity>)" using T[OF `S : K`] `x : S` `x ~= \<infinity>` by auto


1215 
next


1216 
fix S assume "\<infinity> : S" "S : K"


1217 
from openK[rule_format, OF `S : K`, THEN extreal_openE] guess S' x .


1218 
from this(3) `\<infinity> : S`


1219 
show "EX x. {extreal x<..} <= Union K"


1220 
by (auto intro!: exI[of _ x] bexI[OF _ `S : K`])


1221 
next


1222 
fix S assume "(\<infinity>) : S" "S : K"


1223 
from openK[rule_format, OF `S : K`, THEN extreal_openE] guess S' x y .


1224 
from this(4) `(\<infinity>) : S`


1225 
show "EX y. {..<extreal y} <= Union K"


1226 
by (auto intro!: exI[of _ y] bexI[OF _ `S : K`])


1227 
next


1228 
from T[THEN conjunct1] show "open (Union (T`K))" by auto


1229 
qed auto


1230 
qed


1231 
end


1232 


1233 
lemma open_extreal_lessThan[simp]:


1234 
"open {..< a :: extreal}"


1235 
proof (cases a)


1236 
case (real x)


1237 
then show ?thesis unfolding open_extreal_def


1238 
proof (safe intro!: exI[of _ "{..< x}"])


1239 
fix y assume "y < extreal x"


1240 
moreover assume "y ~: (extreal ` {..<x})"


1241 
ultimately have "y ~= extreal (real y)" using real by (cases y) auto


1242 
thus "y = (\<infinity>)" apply (cases y) using `y < extreal x` by auto


1243 
qed auto


1244 
qed (auto simp: open_extreal_def)


1245 


1246 
lemma open_extreal_greaterThan[simp]:


1247 
"open {a :: extreal <..}"


1248 
proof (cases a)


1249 
case (real x)


1250 
then show ?thesis unfolding open_extreal_def


1251 
proof (safe intro!: exI[of _ "{x<..}"])


1252 
fix y assume "extreal x < y"


1253 
moreover assume "y ~: (extreal ` {x<..})"


1254 
moreover assume "y ~= \<infinity>"


1255 
ultimately have "y ~= extreal (real y)" using real by (cases y) auto


1256 
hence False apply (cases y) using `extreal x < y` `y ~= \<infinity>` by auto


1257 
thus "y = (\<infinity>)" by auto


1258 
qed auto


1259 
qed (auto simp: open_extreal_def)


1260 


1261 
lemma extreal_open_greaterThanLessThan[simp]: "open {a::extreal <..< b}"


1262 
unfolding greaterThanLessThan_def by auto


1263 


1264 
lemma closed_extreal_atLeast[simp, intro]: "closed {a :: extreal ..}"


1265 
proof 


1266 
have " {a ..} = {..< a}" by auto


1267 
then show "closed {a ..}"


1268 
unfolding closed_def using open_extreal_lessThan by auto


1269 
qed


1270 


1271 
lemma closed_extreal_atMost[simp, intro]: "closed {.. b :: extreal}"


1272 
proof 


1273 
have " {.. b} = {b <..}" by auto


1274 
then show "closed {.. b}"


1275 
unfolding closed_def using open_extreal_greaterThan by auto


1276 
qed


1277 


1278 
lemma closed_extreal_atLeastAtMost[simp, intro]:


1279 
shows "closed {a :: extreal .. b}"


1280 
unfolding atLeastAtMost_def by auto


1281 


1282 
lemma closed_extreal_singleton:


1283 
"closed {a :: extreal}"


1284 
by (metis atLeastAtMost_singleton closed_extreal_atLeastAtMost)


1285 


1286 
lemma extreal_open_cont_interval:


1287 
assumes "open S" "x \<in> S" and "x \<noteq> \<infinity>" "x \<noteq>  \<infinity>"


1288 
obtains e where "e>0" "{xe <..< x+e} \<subseteq> S"


1289 
proof


1290 
obtain m where m_def: "x = extreal m" using assms by (cases x) auto


1291 
obtain A where "open A" and A_def: "extreal ` A = S  {\<infinity>,(\<infinity>)}"


1292 
using assms by (auto elim!: extreal_openE)


1293 
hence "m : A" using m_def assms by auto


1294 
from this obtain e where e_def: "e>0 & ball m e <= A"


1295 
using open_contains_ball[of A] `open A` by auto


1296 
moreover have "ball m e = {me <..< m+e}" unfolding ball_def dist_norm by auto


1297 
ultimately have *: "{me <..< m+e} <= A" using e_def by auto


1298 
{ fix y assume y_def: "y:{xextreal e <..< x+extreal e}"


1299 
from this obtain z where z_def: "y = extreal z" by (cases y) auto


1300 
hence "z:A" using y_def m_def * by auto


1301 
hence "y:S" using z_def A_def by auto


1302 
} hence "{xextreal e <..< x+extreal e} <= S" by auto


1303 
thus thesis apply apply(rule that[of "extreal e"]) using e_def by auto


1304 
qed


1305 


1306 
lemma extreal_open_cont_interval2:


1307 
assumes "open S" "x \<in> S" and x: "x \<noteq> \<infinity>" "x \<noteq> \<infinity>"


1308 
obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"


1309 
proof


1310 
guess e using extreal_open_cont_interval[OF assms] .


1311 
with that[of "xe" "x+e"] extreal_between[OF x, of e]


1312 
show thesis by auto


1313 
qed


1314 


1315 
lemma extreal_uminus_eq_reorder: " a = b \<longleftrightarrow> a = (b::extreal)" by auto


1316 


1317 
lemma extreal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::extreal)"


1318 
by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_less_minus)


1319 


1320 
lemma extreal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::extreal)"


1321 
by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_le_minus)


1322 


1323 
lemmas extreal_uminus_reorder =


1324 
extreal_uminus_eq_reorder extreal_uminus_less_reorder extreal_uminus_le_reorder


1325 


1326 
lemma extreal_open_uminus:


1327 
fixes S :: "extreal set"


1328 
assumes "open S"


1329 
shows "open (uminus ` S)"


1330 
proof


1331 
obtain T x y where T_def: "open T & extreal ` T = S  {\<infinity>, (\<infinity>)} &


1332 
(\<infinity> : S > {extreal x<..} <= S) & ((\<infinity>) : S > {..<extreal y} <= S)"


1333 
using assms extreal_openE[of S] by metis


1334 
have "extreal ` uminus ` T = uminus ` extreal ` T" apply auto


1335 
by (metis imageI extreal_uminus_uminus uminus_extreal.simps)


1336 
also have "...=uminus ` (S  {\<infinity>, (\<infinity>)})" using T_def by auto


1337 
finally have "extreal ` uminus ` T = uminus ` S  {\<infinity>, (\<infinity>)}" by (auto simp: extreal_uminus_reorder)


1338 
moreover have "open (uminus ` T)" using T_def open_negations[of T] by auto


1339 
ultimately have "EX T. open T & extreal ` T = uminus ` S  {\<infinity>, (\<infinity>)}" by auto


1340 
moreover


1341 
{ assume "\<infinity>: uminus ` S"


1342 
hence "(\<infinity>) : S" by (metis image_iff extreal_uminus_uminus)


1343 
hence "uminus ` {..<extreal y} <= uminus ` S" using T_def by (intro image_mono) auto


1344 
hence "EX x. {extreal x<..} <= uminus ` S" using extreal_uminus_lessThan by auto


1345 
} moreover


1346 
{ assume "(\<infinity>): uminus ` S"


1347 
hence "\<infinity> : S" by (metis image_iff extreal_uminus_uminus)


1348 
hence "uminus ` {extreal x<..} <= uminus ` S" using T_def by (intro image_mono) auto


1349 
hence "EX y. {..<extreal y} <= uminus ` S" using extreal_uminus_greaterThan by auto


1350 
}


1351 
ultimately show ?thesis unfolding open_extreal_def by auto


1352 
qed


1353 


1354 
lemma extreal_uminus_complement:


1355 
fixes S :: "extreal set"


1356 
shows "(uminus ` ( S)) = ( uminus ` S)"


1357 
proof


1358 
{ fix x


1359 
have "x:uminus ` ( S) <> x:( S)" by (metis image_iff extreal_uminus_uminus)


1360 
also have "... <> x:( uminus ` S)"


1361 
by (metis ComplI Compl_iff image_eqI extreal_uminus_uminus extreal_minus_minus_image)


1362 
finally have "x:uminus ` ( S) <> x:( uminus ` S)" by auto


1363 
} thus ?thesis by auto


1364 
qed


1365 


1366 
lemma extreal_closed_uminus:


1367 
fixes S :: "extreal set"


1368 
assumes "closed S"


1369 
shows "closed (uminus ` S)"


1370 
using assms unfolding closed_def


1371 
using extreal_open_uminus[of " S"] extreal_uminus_complement by auto


1372 


1373 


1374 
lemma not_open_extreal_singleton:


1375 
"~(open {a :: extreal})"


1376 
proof(rule ccontr)


1377 
assume "~ ~ open {a}" hence a: "open {a}" by auto


1378 
{ assume "a=(\<infinity>)"


1379 
then obtain y where "{..<extreal y} <= {a}" using a open_MInfty2[of "{a}"] by auto


1380 
hence "extreal(y  1):{a}" apply (subst subsetD[of "{..<extreal y}"]) by auto


1381 
hence False using `a=(\<infinity>)` by auto


1382 
} moreover


1383 
{ assume "a=\<infinity>"


1384 
then obtain y where "{extreal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto


1385 
hence "extreal(y+1):{a}" apply (subst subsetD[of "{extreal y<..}"]) by auto


1386 
hence False using `a=\<infinity>` by auto


1387 
} moreover


1388 
{ assume fin: "a~=(\<infinity>)" "a~=\<infinity>"


1389 
from extreal_open_cont_interval[OF a singletonI this(2,1)] guess e . note e = this


1390 
then obtain b where b_def: "a<b & b<a+e"


1391 
using fin extreal_between extreal_dense[of a "a+e"] by auto


1392 
then have "b: {ae <..< a+e}" using fin extreal_between[of a e] e by auto


1393 
then have False using b_def e by auto


1394 
} ultimately show False by auto


1395 
qed


1396 


1397 
lemma extreal_closed_contains_Inf:


1398 
fixes S :: "extreal set"


1399 
assumes "closed S" "S ~= {}"


1400 
shows "Inf S : S"


1401 
proof(rule ccontr)


1402 
assume "~(Inf S:S)" hence a: "open (S)" "Inf S:( S)" using assms by auto


1403 
{ assume minf: "Inf S=(\<infinity>)" hence "(\<infinity>) :  S" using a by auto


1404 
then obtain y where "{..<extreal y} <= (S)" using a open_MInfty2[of " S"] by auto


1405 
hence "extreal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff


1406 
complete_lattice_class.Inf_greatest double_complement set_rev_mp)


1407 
hence False using minf by auto


1408 
} moreover


1409 
{ assume pinf: "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))


1410 
hence False by (metis `Inf S ~: S` insert_code mem_def pinf)


1411 
} moreover


1412 
{ assume fin: "Inf S ~= \<infinity>" "Inf S ~= (\<infinity>)"


1413 
from extreal_open_cont_interval[OF a this] guess e . note e = this


1414 
{ fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower)


1415 
hence *: "x>Inf Se" using e by (metis fin extreal_between(1) order_less_le_trans)


1416 
{ assume "x<Inf S+e" hence "x:{Inf Se <..< Inf S+e}" using * by auto


1417 
hence False using e `x:S` by auto

15927c040731
add Extended_Reals from AFP/Lower_Semicontinuous
hoelzl
parents:
