# HG changeset patch
# User hoelzl
# Date 1311079109 -7200
# Node ID ab93d0190a5d9b5a3c6539332850846cc03cda09
# Parent  c6f35921056eb0325d9417ac3150fe130561a6ed
add ereal to typeclass infinity

diff -r c6f35921056e -r ab93d0190a5d src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -47,7 +47,6 @@
   qed
 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
 
-declare [[coercion_enabled]]
 declare [[coercion "Fin::nat\<Rightarrow>enat"]]
 
 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
diff -r c6f35921056e -r ab93d0190a5d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -8,7 +8,7 @@
 header {* Extended real number line *}
 
 theory Extended_Real
-  imports Complex_Main
+  imports Complex_Main Extended_Nat
 begin
 
 text {*
@@ -40,44 +40,43 @@
 
 datatype ereal = ereal real | PInfty | MInfty
 
-notation (xsymbols)
-  PInfty  ("\<infinity>")
-
-notation (HTML output)
-  PInfty  ("\<infinity>")
-
-declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
-
 instantiation ereal :: uminus
 begin
   fun uminus_ereal where
     "- (ereal r) = ereal (- r)"
-  | "- \<infinity> = MInfty"
-  | "- MInfty = \<infinity>"
+  | "- PInfty = MInfty"
+  | "- MInfty = PInfty"
   instance ..
 end
 
-lemma inj_ereal[simp]: "inj_on ereal A"
-  unfolding inj_on_def by auto
-
-lemma MInfty_neq_PInfty[simp]:
-  "\<infinity> \<noteq> - \<infinity>" "- \<infinity> \<noteq> \<infinity>" by simp_all
+instantiation ereal :: infinity
+begin
+  definition "(\<infinity>::ereal) = PInfty"
+  instance ..
+end
 
-lemma MInfty_neq_ereal[simp]:
-  "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r" by simp_all
+definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
 
-lemma MInfinity_cases[simp]:
-  "(case - \<infinity> of ereal r \<Rightarrow> f r | \<infinity> \<Rightarrow> y | MInfinity \<Rightarrow> z) = z"
-  by simp
+declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
+declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
+declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]]
 
 lemma ereal_uminus_uminus[simp]:
   fixes a :: ereal shows "- (- a) = a"
   by (cases a) simp_all
 
-lemma MInfty_eq[simp, code_post]:
-  "MInfty = - \<infinity>" by simp
+lemma
+  shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>"
+    and MInfty_eq_minfinity[simp]: "MInfty = - \<infinity>"
+    and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq> - (\<infinity>::ereal)" "- \<infinity> \<noteq> (\<infinity>::ereal)"
+    and MInfty_neq_ereal[simp]: "ereal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> ereal r"
+    and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r"
+    and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = y"
+    and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
+  by (simp_all add: infinity_ereal_def)
 
-declare uminus_ereal.simps(2)[code_inline, simp del]
+lemma inj_ereal[simp]: "inj_on ereal A"
+  unfolding inj_on_def by auto
 
 lemma ereal_cases[case_names real PInf MInf, cases type: ereal]:
   assumes "\<And>r. x = ereal r \<Longrightarrow> P"
@@ -106,7 +105,7 @@
 lemma real_of_ereal[simp]:
     "real (- x :: ereal) = - (real x)"
     "real (ereal r) = r"
-    "real \<infinity> = 0"
+    "real (\<infinity>::ereal) = 0"
   by (cases x) (simp_all add: real_of_ereal_def)
 
 lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
@@ -130,17 +129,17 @@
 begin
   function abs_ereal where
     "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
-  | "\<bar>-\<infinity>\<bar> = \<infinity>"
-  | "\<bar>\<infinity>\<bar> = \<infinity>"
+  | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
+  | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
   by (auto intro: ereal_cases)
   termination proof qed (rule wf_empty)
   instance ..
 end
 
-lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
+lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   by (cases x) auto
 
-lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
+lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   by (cases x) auto
 
 lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
@@ -155,11 +154,11 @@
 
 function plus_ereal where
 "ereal r + ereal p = ereal (r + p)" |
-"\<infinity> + a = \<infinity>" |
-"a + \<infinity> = \<infinity>" |
+"\<infinity> + a = (\<infinity>::ereal)" |
+"a + \<infinity> = (\<infinity>::ereal)" |
 "ereal r + -\<infinity> = - \<infinity>" |
-"-\<infinity> + ereal p = -\<infinity>" |
-"-\<infinity> + -\<infinity> = -\<infinity>"
+"-\<infinity> + ereal p = -(\<infinity>::ereal)" |
+"-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
 proof -
   case (goal1 P x)
   moreover then obtain a b where "x = (a, b)" by (cases x) auto
@@ -169,8 +168,8 @@
 termination proof qed (rule wf_empty)
 
 lemma Infty_neq_0[simp]:
-  "\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>"
-  "-\<infinity> \<noteq> 0" "0 \<noteq> -\<infinity>"
+  "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
+  "-(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> -(\<infinity>::ereal)"
   by (simp_all add: zero_ereal_def)
 
 lemma ereal_eq_0[simp]:
@@ -204,21 +203,21 @@
   by (cases a) simp_all
 
 lemma ereal_plus_eq_PInfty[simp]:
-  shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
+  fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_plus_eq_MInfty[simp]:
-  shows "a + b = -\<infinity> \<longleftrightarrow>
+  fixes a b :: ereal shows "a + b = -\<infinity> \<longleftrightarrow>
     (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_add_cancel_left:
-  assumes "a \<noteq> -\<infinity>"
+  fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
   shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   using assms by (cases rule: ereal3_cases[of a b c]) auto
 
 lemma ereal_add_cancel_right:
-  assumes "a \<noteq> -\<infinity>"
+  fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
   shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   using assms by (cases rule: ereal3_cases[of a b c]) auto
 
@@ -237,12 +236,12 @@
 begin
 
 function less_ereal where
-"ereal x < ereal y \<longleftrightarrow> x < y" |
-"        \<infinity> < a         \<longleftrightarrow> False" |
-"        a < -\<infinity>        \<longleftrightarrow> False" |
-"ereal x < \<infinity>         \<longleftrightarrow> True" |
-"       -\<infinity> < ereal r \<longleftrightarrow> True" |
-"       -\<infinity> < \<infinity>         \<longleftrightarrow> True"
+"   ereal x < ereal y     \<longleftrightarrow> x < y" |
+"(\<infinity>::ereal) < a           \<longleftrightarrow> False" |
+"         a < -(\<infinity>::ereal) \<longleftrightarrow> False" |
+"ereal x    < \<infinity>           \<longleftrightarrow> True" |
+"        -\<infinity> < ereal r     \<longleftrightarrow> True" |
+"        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
 proof -
   case (goal1 P x)
   moreover then obtain a b where "x = (a,b)" by (cases x) auto
@@ -253,33 +252,35 @@
 definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y"
 
 lemma ereal_infty_less[simp]:
-  "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
-  "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
+  fixes x :: ereal
+  shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
+    "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
   by (cases x, simp_all) (cases x, simp_all)
 
 lemma ereal_infty_less_eq[simp]:
-  "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
+  fixes x :: ereal
+  shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
   "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
   by (auto simp add: less_eq_ereal_def)
 
 lemma ereal_less[simp]:
   "ereal r < 0 \<longleftrightarrow> (r < 0)"
   "0 < ereal r \<longleftrightarrow> (0 < r)"
-  "0 < \<infinity>"
-  "-\<infinity> < 0"
+  "0 < (\<infinity>::ereal)"
+  "-(\<infinity>::ereal) < 0"
   by (simp_all add: zero_ereal_def)
 
 lemma ereal_less_eq[simp]:
-  "x \<le> \<infinity>"
-  "-\<infinity> \<le> x"
+  "x \<le> (\<infinity>::ereal)"
+  "-(\<infinity>::ereal) \<le> x"
   "ereal r \<le> ereal p \<longleftrightarrow> r \<le> p"
   "ereal r \<le> 0 \<longleftrightarrow> r \<le> 0"
   "0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"
   by (auto simp add: less_eq_ereal_def zero_ereal_def)
 
 lemma ereal_infty_less_eq2:
-  "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = \<infinity>"
-  "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -\<infinity>"
+  "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"
+  "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -(\<infinity>::ereal)"
   by simp_all
 
 instance
@@ -304,15 +305,15 @@
 qed
 
 lemma real_of_ereal_positive_mono:
-  "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
+  fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
   by (cases rule: ereal2_cases[of x y]) auto
 
 lemma ereal_MInfty_lessI[intro, simp]:
-  "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
+  fixes a :: ereal shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   by (cases a) auto
 
 lemma ereal_less_PInfty[intro, simp]:
-  "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
+  fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
   by (cases a) auto
 
 lemma ereal_less_ereal_Ex:
@@ -373,14 +374,15 @@
 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
   by (cases x) auto
 
-lemma real_of_ereal_le_0[simp]: "real (X :: ereal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)"
-  by (cases X) auto
+lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)"
+  by (cases x) auto
 
-lemma abs_real_of_ereal[simp]: "\<bar>real (X :: ereal)\<bar> = real \<bar>X\<bar>"
-  by (cases X) auto
+lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"
+  by (cases x) auto
 
-lemma zero_less_real_of_ereal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)"
-  by (cases X) auto
+lemma zero_less_real_of_ereal:
+  fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)"
+  by (cases x) auto
 
 lemma ereal_0_le_uminus_iff[simp]:
   fixes a :: ereal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
@@ -390,37 +392,13 @@
   fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   by (cases rule: ereal2_cases[of a]) auto
 
+lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
+  using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
+
 lemma ereal_dense:
   fixes x y :: ereal assumes "x < y"
-  shows "EX z. x < z & z < y"
-proof -
-{ assume a: "x = (-\<infinity>)"
-  { assume "y = \<infinity>" hence ?thesis using a by (auto intro!: exI[of _ "0"]) }
-  moreover
-  { assume "y ~= \<infinity>"
-    with `x < y` obtain r where r: "y = ereal r" by (cases y) auto
-    hence ?thesis using `x < y` a by (auto intro!: exI[of _ "ereal (r - 1)"])
-  } ultimately have ?thesis by auto
-}
-moreover
-{ assume "x ~= (-\<infinity>)"
-  with `x < y` obtain p where p: "x = ereal p" by (cases x) auto
-  { assume "y = \<infinity>" hence ?thesis using `x < y` p
-       by (auto intro!: exI[of _ "ereal (p + 1)"]) }
-  moreover
-  { assume "y ~= \<infinity>"
-    with `x < y` obtain r where r: "y = ereal r" by (cases y) auto
-    with p `x < y` have "p < r" by auto
-    with dense obtain z where "p < z" "z < r" by auto
-    hence ?thesis using r p by (auto intro!: exI[of _ "ereal z"])
-  } ultimately have ?thesis by auto
-} ultimately show ?thesis by auto
-qed
-
-lemma ereal_dense2:
-  fixes x y :: ereal assumes "x < y"
-  shows "EX z. x < ereal z & ereal z < y"
-  by (metis ereal_dense[OF `x < y`] ereal_cases less_ereal.simps(2,3))
+  shows "\<exists>z. x < z \<and> z < y"
+  using ereal_dense2[OF `x < y`] by blast
 
 lemma ereal_add_strict_mono:
   fixes a b c d :: ereal
@@ -428,7 +406,8 @@
   shows "a + c < b + d"
   using assms by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
 
-lemma ereal_less_add: "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
+lemma ereal_less_add: 
+  fixes a b c :: ereal shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
   by (cases rule: ereal2_cases[of b c]) auto
 
 lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)" by auto
@@ -508,8 +487,8 @@
 
 function sgn_ereal where
   "sgn (ereal r) = ereal (sgn r)"
-| "sgn \<infinity> = 1"
-| "sgn (-\<infinity>) = -1"
+| "sgn (\<infinity>::ereal) = 1"
+| "sgn (-\<infinity>::ereal) = -1"
 by (auto intro: ereal_cases)
 termination proof qed (rule wf_empty)
 
@@ -519,10 +498,10 @@
 "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
 "ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
 "-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
-"\<infinity> * \<infinity> = \<infinity>" |
-"-\<infinity> * \<infinity> = -\<infinity>" |
-"\<infinity> * -\<infinity> = -\<infinity>" |
-"-\<infinity> * -\<infinity> = \<infinity>"
+"(\<infinity>::ereal) * \<infinity> = \<infinity>" |
+"-(\<infinity>::ereal) * \<infinity> = -\<infinity>" |
+"(\<infinity>::ereal) * -\<infinity> = -\<infinity>" |
+"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
 proof -
   case (goal1 P x)
   moreover then obtain a b where "x = (a, b)" by (cases x) auto
@@ -570,13 +549,13 @@
   by (cases x) (auto simp: zero_ereal_def)
 
 lemma ereal_times[simp]:
-  "1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1"
-  "1 \<noteq> -\<infinity>" "-\<infinity> \<noteq> 1"
+  "1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"
+  "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 1"
   by (auto simp add: times_ereal_def one_ereal_def)
 
 lemma ereal_plus_1[simp]:
   "1 + ereal r = ereal (r + 1)" "ereal r + 1 = ereal (r + 1)"
-  "1 + -\<infinity> = -\<infinity>" "-\<infinity> + 1 = -\<infinity>"
+  "1 + -(\<infinity>::ereal) = -\<infinity>" "-(\<infinity>::ereal) + 1 = -\<infinity>"
   unfolding one_ereal_def by auto
 
 lemma ereal_zero_times[simp]:
@@ -584,12 +563,12 @@
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_mult_eq_PInfty[simp]:
-  shows "a * b = \<infinity> \<longleftrightarrow>
+  shows "a * b = (\<infinity>::ereal) \<longleftrightarrow>
     (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_mult_eq_MInfty[simp]:
-  shows "a * b = -\<infinity> \<longleftrightarrow>
+  shows "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
     (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
   by (cases rule: ereal2_cases[of a b]) auto
 
@@ -608,22 +587,22 @@
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_mult_infty[simp]:
-  "a * \<infinity> = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
+  "a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   by (cases a) auto
 
 lemma ereal_infty_mult[simp]:
-  "\<infinity> * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
+  "(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   by (cases a) auto
 
 lemma ereal_mult_strict_right_mono:
-  assumes "a < b" and "0 < c" "c < \<infinity>"
+  assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)"
   shows "a * c < b * c"
   using assms
   by (cases rule: ereal3_cases[of a b c])
      (auto simp: zero_le_mult_iff ereal_less_PInfty)
 
 lemma ereal_mult_strict_left_mono:
-  "\<lbrakk> a < b ; 0 < c ; c < \<infinity>\<rbrakk> \<Longrightarrow> c * a < c * b"
+  "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
   using ereal_mult_strict_right_mono by (simp add: mult_commute[of c])
 
 lemma ereal_mult_right_mono:
@@ -722,8 +701,7 @@
   fixes x y :: ereal
   assumes "ALL z. x <= ereal z --> y <= ereal z"
   shows "y <= x"
-by (metis assms ereal.exhaust ereal_bot ereal_less_eq(1)
-          ereal_less_eq(2) order_refl uminus_ereal.simps(2))
+by (metis assms ereal_bot ereal_cases ereal_infty_less_eq ereal_less_eq linorder_le_cases)
 
 lemma ereal_le_ereal:
   fixes x y :: ereal
@@ -752,6 +730,7 @@
 qed simp
 
 lemma setprod_PInf:
+  fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   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)"
 proof cases
@@ -788,7 +767,7 @@
 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)"
   by (induct n) (auto simp: one_ereal_def)
 
-lemma ereal_power_PInf[simp]: "\<infinity> ^ n = (if n = 0 then 1 else \<infinity>)"
+lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)"
   by (induct n) (auto simp: one_ereal_def)
 
 lemma ereal_power_uminus[simp]:
@@ -835,15 +814,15 @@
   "ereal r - ereal p = ereal (r - p)"
   "-\<infinity> - ereal r = -\<infinity>"
   "ereal r - \<infinity> = -\<infinity>"
-  "\<infinity> - x = \<infinity>"
-  "-\<infinity> - \<infinity> = -\<infinity>"
+  "(\<infinity>::ereal) - x = \<infinity>"
+  "-(\<infinity>::ereal) - \<infinity> = -\<infinity>"
   "x - -y = x + y"
   "x - 0 = x"
   "0 - x = -x"
   by (simp_all add: minus_ereal_def)
 
 lemma ereal_x_minus_x[simp]:
-  "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0)"
+  "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
   by (cases x) simp_all
 
 lemma ereal_eq_minus_iff:
@@ -917,12 +896,14 @@
   by (cases rule: ereal3_cases[of a b c]) auto
 
 lemma ereal_add_le_add_iff:
-  "c + a \<le> c + b \<longleftrightarrow>
+  fixes a b c :: ereal
+  shows "c + a \<le> c + b \<longleftrightarrow>
     a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
 
 lemma ereal_mult_le_mult_iff:
-  "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+  fixes a b c :: ereal
+  shows "\<bar>c\<bar> \<noteq> \<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   by (cases rule: ereal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)
 
 lemma ereal_minus_mono:
@@ -932,7 +913,8 @@
   by (cases rule: ereal3_cases[case_product ereal_cases, of A B C D]) simp_all
 
 lemma real_of_ereal_minus:
-  "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
+  fixes a b :: ereal
+  shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_diff_positive:
@@ -953,8 +935,8 @@
 
 function inverse_ereal where
 "inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" |
-"inverse \<infinity> = 0" |
-"inverse (-\<infinity>) = 0"
+"inverse (\<infinity>::ereal) = 0" |
+"inverse (-\<infinity>::ereal) = 0"
   by (auto intro: ereal_cases)
 termination by (relation "{}") simp
 
@@ -969,7 +951,7 @@
   by (cases a) (auto simp: inverse_eq_divide)
 
 lemma ereal_inverse[simp]:
-  "inverse 0 = \<infinity>"
+  "inverse (0::ereal) = \<infinity>"
   "inverse (1::ereal) = 1"
   by (simp_all add: one_ereal_def zero_ereal_def)
 
@@ -978,16 +960,16 @@
   unfolding divide_ereal_def by (auto simp: divide_real_def)
 
 lemma ereal_divide_same[simp]:
-  "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
+  fixes x :: ereal shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
   by (cases x)
      (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
 
 lemma ereal_inv_inv[simp]:
-  "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
+  fixes x :: ereal shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
   by (cases x) auto
 
 lemma ereal_inverse_minus[simp]:
-  "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
+  fixes x :: ereal shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
   by (cases x) simp_all
 
 lemma ereal_uminus_divide[simp]:
@@ -995,7 +977,7 @@
   unfolding divide_ereal_def by simp
 
 lemma ereal_divide_Infty[simp]:
-  "x / \<infinity> = 0" "x / -\<infinity> = 0"
+  fixes x :: ereal shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
   unfolding divide_ereal_def by simp_all
 
 lemma ereal_divide_one[simp]:
@@ -1012,19 +994,19 @@
   using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
 
 lemma ereal_le_divide_pos:
-  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
+  fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_divide_le_pos:
-  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
+  fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_le_divide_neg:
-  "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
+  fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_divide_le_neg:
-  "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
+  fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_inverse_antimono_strict:
@@ -1038,11 +1020,11 @@
   by (cases rule: ereal2_cases[of x y]) auto
 
 lemma inverse_inverse_Pinfty_iff[simp]:
-  "inverse x = \<infinity> \<longleftrightarrow> x = 0"
+  fixes x :: ereal shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
   by (cases x) auto
 
 lemma ereal_inverse_eq_0:
-  "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
+  fixes x :: ereal shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
   by (cases x) auto
 
 lemma ereal_0_gt_inverse:
@@ -1050,6 +1032,7 @@
   by (cases x) auto
 
 lemma ereal_mult_less_right:
+  fixes a b c :: ereal
   assumes "b * a < c * a" "0 < a" "a < \<infinity>"
   shows "b < c"
   using assms
@@ -1057,7 +1040,7 @@
      (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
 
 lemma ereal_power_divide:
-  "y \<noteq> 0 \<Longrightarrow> (x / y :: ereal) ^ n = x^n / y^n"
+  fixes x y :: ereal shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
   by (cases rule: ereal2_cases[of x y])
      (auto simp: one_ereal_def zero_ereal_def power_divide not_le
                  power_less_zero_eq zero_le_power_iff)
@@ -1096,11 +1079,11 @@
 instantiation ereal :: complete_lattice
 begin
 
-definition "bot = -\<infinity>"
-definition "top = \<infinity>"
+definition "bot = (-\<infinity>::ereal)"
+definition "top = (\<infinity>::ereal)"
 
-definition "Sup S = (LEAST z. ALL x:S. x <= z :: ereal)"
-definition "Inf S = (GREATEST z. ALL x:S. z <= x :: ereal)"
+definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: ereal)"
+definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: ereal)"
 
 lemma ereal_complete_Sup:
   fixes S :: "ereal set" assumes "S \<noteq> {}"
@@ -1303,11 +1286,13 @@
   using Sup_eq_MInfty[of "uminus`S"]
   unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp
 
-lemma Inf_eq_MInfty: "-\<infinity> : S ==> Inf S = -\<infinity>"
+lemma Inf_eq_MInfty: 
+  fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
   unfolding Inf_ereal_def
   by (auto intro!: Greatest_equality)
 
-lemma Sup_eq_PInfty: "\<infinity> : S ==> Sup S = \<infinity>"
+lemma Sup_eq_PInfty:
+  fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
   unfolding Sup_ereal_def
   by (auto intro!: Least_equality)
 
@@ -1371,7 +1356,7 @@
 
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
 proof -
-  { fix x assume "x \<noteq> \<infinity>"
+  { fix x ::ereal assume "x \<noteq> \<infinity>"
     then have "\<exists>k::nat. x < ereal (real k)"
     proof (cases x)
       case MInf then show ?thesis by (intro exI[of _ 0]) auto
@@ -1465,6 +1450,7 @@
 qed
 
 lemma SUP_ereal_le_addI:
+  fixes f :: "'i \<Rightarrow> ereal"
   assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
   shows "SUPR UNIV f + y \<le> z"
 proof (cases y)
@@ -1554,7 +1540,7 @@
   unfolding SUPR_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
   apply simp
 proof safe
-  fix x assume "x \<noteq> \<infinity>"
+  fix x :: ereal assume "x \<noteq> \<infinity>"
   show "\<exists>i\<in>A. x < f i"
   proof (cases x)
     case PInf with `x \<noteq> \<infinity>` show ?thesis by simp
@@ -1646,7 +1632,6 @@
   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
   using Sup_countable_SUPR[of "g`A"] by (auto simp: SUPR_def)
 
-
 lemma Sup_ereal_cadd:
   fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
   shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
@@ -1674,6 +1659,7 @@
                  ereal_Sup_uminus_image_eq)
 
 lemma SUPR_ereal_cminus:
+  fixes f :: "'i \<Rightarrow> ereal"
   fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
   shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
   using Sup_ereal_cminus[of "f`A" a] assms
@@ -1692,7 +1678,7 @@
 qed
 
 lemma INFI_ereal_cminus:
-  fixes A assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
+  fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
   shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
   using Inf_ereal_cminus[of "f`A" a] assms
   unfolding SUPR_def INFI_def image_image
@@ -1703,6 +1689,7 @@
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma INFI_ereal_add:
+  fixes f :: "nat \<Rightarrow> ereal"
   assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
 proof -
@@ -1824,6 +1811,7 @@
 by (metis atLeastAtMost_singleton closed_ereal_atLeastAtMost)
 
 lemma ereal_open_cont_interval:
+  fixes S :: "ereal set"
   assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
   obtains e where "e>0" "{x-e <..< x+e} \<subseteq> S"
 proof-
@@ -1841,6 +1829,7 @@
 qed
 
 lemma ereal_open_cont_interval2:
+  fixes S :: "ereal set"
   assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
   obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
 proof-
@@ -1901,9 +1890,13 @@
 qed
 
 lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= ereal B)" (is "?l = ?r")
-proof assume ?r show ?l apply(rule topological_tendstoI)
+proof
+  assume ?r
+  show ?l
+    apply(rule topological_tendstoI)
     unfolding eventually_sequentially
-  proof- fix S assume "open S" "\<infinity> : S"
+  proof-
+    fix S :: "ereal set" assume "open S" "\<infinity> : S"
     from open_PInfty[OF this] guess B .. note B=this
     from `?r`[rule_format,of "B+1"] guess N .. note N=this
     show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
@@ -1913,7 +1906,9 @@
       finally show ?case using B by fastsimp
     qed
   qed
-next assume ?l show ?r
+next
+  assume ?l
+  show ?r
   proof fix B::real have "open {ereal B<..}" "\<infinity> : {ereal B<..}" by auto
     from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
     guess N .. note N=this
@@ -1923,9 +1918,14 @@
 
 
 lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= ereal B)" (is "?l = ?r")
-proof assume ?r show ?l apply(rule topological_tendstoI)
+proof
+  assume ?r
+  show ?l
+    apply(rule topological_tendstoI)
     unfolding eventually_sequentially
-  proof- fix S assume "open S" "(-\<infinity>) : S"
+  proof-
+    fix S :: "ereal set"
+    assume "open S" "(-\<infinity>) : S"
     from open_MInfty[OF this] guess B .. note B=this
     from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
     show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
@@ -2041,7 +2041,7 @@
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma real_of_ereal_eq_0:
-  "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
+  fixes x :: ereal shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
   by (cases x) auto
 
 lemma tendsto_ereal_realD:
@@ -2075,6 +2075,7 @@
      (simp_all add: zero_less_mult_iff)
 
 lemma ereal_inj_affinity:
+  fixes m t :: ereal
   assumes "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" "\<bar>t\<bar> \<noteq> \<infinity>"
   shows "inj_on (\<lambda>x. m * x + t) A"
   using assms
@@ -2082,33 +2083,39 @@
      (auto intro!: inj_onI simp: ereal_add_cancel_right ereal_mult_cancel_left)
 
 lemma ereal_PInfty_eq_plus[simp]:
+  fixes a b :: ereal
   shows "\<infinity> = a + b \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_MInfty_eq_plus[simp]:
+  fixes a b :: ereal
   shows "-\<infinity> = a + b \<longleftrightarrow> (a = -\<infinity> \<and> b \<noteq> \<infinity>) \<or> (b = -\<infinity> \<and> a \<noteq> \<infinity>)"
   by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_less_divide_pos:
-  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
+  fixes x y :: ereal
+  shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_divide_less_pos:
-  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
+  fixes x y z :: ereal
+  shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
   by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
 
 lemma ereal_divide_eq:
-  "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
+  fixes a b c :: ereal
+  shows "b \<noteq> 0 \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
   by (cases rule: ereal3_cases[of a b c])
      (simp_all add: field_simps)
 
-lemma ereal_inverse_not_MInfty[simp]: "inverse a \<noteq> -\<infinity>"
+lemma ereal_inverse_not_MInfty[simp]: "inverse (a::ereal) \<noteq> -\<infinity>"
   by (cases a) auto
 
 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
   by (cases x) auto
 
 lemma ereal_LimI_finite:
+  fixes x :: ereal
   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
   shows "u ----> x"
@@ -2138,6 +2145,7 @@
 qed
 
 lemma ereal_LimI_finite_iff:
+  fixes x :: ereal
   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
   (is "?lhs <-> ?rhs")
@@ -2503,7 +2511,7 @@
 from this show ?thesis using ext by blast
 qed
 
-lemma open_image_ereal: "open(UNIV-{\<infinity>,(-\<infinity>)})"
+lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
 by (metis range_ereal open_ereal open_UNIV)
 
 lemma ereal_le_distrib:
diff -r c6f35921056e -r ab93d0190a5d src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -163,6 +163,7 @@
 qed
 
 lemma ereal_open_affinity_pos:
+  fixes S :: "ereal set"
   assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   shows "open ((\<lambda>x. m * x + t) ` S)"
 proof -
@@ -209,6 +210,7 @@
 qed
 
 lemma ereal_open_affinity:
+  fixes S :: "ereal set"
   assumes "open S" and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   shows "open ((\<lambda>x. m * x + t) ` S)"
 proof cases
@@ -268,7 +270,7 @@
 qed
 
 
-lemma ereal_open_atLeast: "open {x..} \<longleftrightarrow> x = -\<infinity>"
+lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
 proof
   assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
   then show "open {x..}" by auto
@@ -384,7 +386,7 @@
   shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
 proof (intro lim_imp_Liminf iffI assms)
   assume rhs: "Liminf net f = \<infinity>"
-  { fix S assume "open S & \<infinity> : S"
+  { fix S :: "ereal set" assume "open S & \<infinity> : S"
     then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
     moreover have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
       using rhs unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
@@ -893,7 +895,7 @@
    using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
 
 
-lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>)}) real"
+lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
    using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal by auto
 
 
@@ -1001,7 +1003,9 @@
   assume "finite A" then show ?thesis by induct auto
 qed simp
 
-lemma setsum_Pinfty: "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
+lemma setsum_Pinfty:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
 proof safe
   assume *: "setsum f P = \<infinity>"
   show "finite P"
@@ -1023,6 +1027,7 @@
 qed
 
 lemma setsum_Inf:
+  fixes f :: "'a \<Rightarrow> ereal"
   shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))"
 proof
   assume *: "\<bar>setsum f A\<bar> = \<infinity>"
@@ -1045,6 +1050,7 @@
 qed
 
 lemma setsum_real_of_ereal:
+  fixes f :: "'i \<Rightarrow> ereal"
   assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
 proof -
@@ -1186,6 +1192,7 @@
            intro!: SUPR_ereal_cmult )
 
 lemma suminf_PInfty:
+  fixes f :: "nat \<Rightarrow> ereal"
   assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
   shows "f i \<noteq> \<infinity>"
 proof -
@@ -1253,13 +1260,14 @@
 qed
 
 lemma suminf_ereal_PInf[simp]:
-  "(\<Sum>x. \<infinity>) = \<infinity>"
+  "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
 proof -
-  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>)" by (rule suminf_upper) auto
+  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)" by (rule suminf_upper) auto
   then show ?thesis by simp
 qed
 
 lemma summable_real_of_ereal:
+  fixes f :: "nat \<Rightarrow> ereal"
   assumes f: "\<And>i. 0 \<le> f i" and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
   shows "summable (\<lambda>i. real (f i))"
 proof (rule summable_def[THEN iffD2])
diff -r c6f35921056e -r ab93d0190a5d src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -1122,7 +1122,7 @@
   show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"
   proof cases
     assume "0 \<in> B"
-    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0}"
+    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"
       by (auto simp add: real_of_ereal_eq_0)
     then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
       using open_real by auto
@@ -1148,7 +1148,8 @@
 qed auto
 
 lemma (in sigma_algebra) borel_measurable_ereal_iff_real:
-  "f \<in> borel_measurable M \<longleftrightarrow>
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "f \<in> borel_measurable M \<longleftrightarrow>
     ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)"
 proof safe
   assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"
@@ -1208,7 +1209,8 @@
 qed auto
 
 lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal:
-  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
 proof (intro iffI allI)
   assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
   show "f \<in> borel_measurable M"
@@ -1226,7 +1228,7 @@
       by (auto simp: not_le)
     then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
     moreover
-    have "{-\<infinity>} = {..-\<infinity>}" by auto
+    have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
     then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
     moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
       using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)
diff -r c6f35921056e -r ab93d0190a5d src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Jul 19 14:37:49 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Jul 19 14:38:29 2011 +0200
@@ -951,15 +951,15 @@
   proof (rule AE_I')
     { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
         and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
-      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
+      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
       have "(\<Union>i. ?A i) \<in> null_sets"
       proof (rule null_sets_UN)
-        fix i have "?A i \<in> sets M"
+        fix i ::nat have "?A i \<in> sets M"
           using borel Q0(1) by auto
-        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x \<partial>M)"
+        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. (i::ereal) * indicator (?A i) x \<partial>M)"
           unfolding eq[OF `?A i \<in> sets M`]
           by (auto intro!: positive_integral_mono simp: indicator_def)
-        also have "\<dots> = of_nat i * \<mu> (?A i)"
+        also have "\<dots> = i * \<mu> (?A i)"
           using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
         also have "\<dots> < \<infinity>"
           using `?A i \<in> sets M`[THEN finite_measure] by auto
@@ -1067,7 +1067,7 @@
   interpret \<nu>: measure_space ?N
     where "borel_measurable ?N = borel_measurable M" and "measure ?N = \<nu>"
     and "sets ?N = sets M" and "space ?N = space M" using \<nu> by (auto simp: measurable_def)
-  def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M"
+  def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
   { fix i j have "A i \<inter> Q j \<in> sets M"
     unfolding A_def using f Q
     apply (rule_tac Int)
@@ -1095,7 +1095,7 @@
         case PInf with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0])
       next
         case (real r)
-        with less_PInf_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by (auto simp: real_eq_of_nat)
+        with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat)
         then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"])
       next
         case MInf with x show ?thesis
@@ -1115,9 +1115,9 @@
     next
       case (Suc n)
       then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
-        (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x \<partial>M)"
+        (\<integral>\<^isup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
         by (auto intro!: positive_integral_mono simp: indicator_def A_def)
-      also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
+      also have "\<dots> = Suc n * \<mu> (Q j)"
         using Q by (auto intro!: positive_integral_cmult_indicator)
       also have "\<dots> < \<infinity>"
         using Q by (auto simp: real_eq_of_nat[symmetric])