# HG changeset patch
# User hoelzl
# Date 1306171265 -7200
# Node ID 6e5c2a3c69da902760669ca57d1e71edb5df0c4f
# Parent  618adb3584e513dc850e213f8c7cbf43ebca249a
move lemmas to Extended_Reals and Extended_Real_Limits

diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Library/Extended_Reals.thy
--- a/src/HOL/Library/Extended_Reals.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Library/Extended_Reals.thy	Mon May 23 19:21:05 2011 +0200
@@ -189,6 +189,9 @@
 qed
 end
 
+lemma real_of_extreal_0[simp]: "real (0::extreal) = 0"
+  unfolding real_of_extreal_def zero_extreal_def by simp
+
 lemma abs_extreal_zero[simp]: "\<bar>0\<bar> = (0::extreal)"
   unfolding zero_extreal_def abs_extreal.simps by simp
 
@@ -300,6 +303,10 @@
     by (cases rule: extreal3_cases[of a b c]) auto
 qed
 
+lemma real_of_extreal_positive_mono:
+  "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
+  by (cases rule: extreal2_cases[of x y]) auto
+
 lemma extreal_MInfty_lessI[intro, simp]:
   "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   by (cases a) auto
@@ -351,17 +358,38 @@
   "real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < extreal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"
   by (cases y) auto
 
-lemma real_of_extreal_positive_mono:
-  assumes "x \<noteq> \<infinity>" "y \<noteq> \<infinity>" "0 \<le> x" "x \<le> y"
-  shows "real x \<le> real y"
-  using assms by (cases rule: extreal2_cases[of x y]) auto
-
 lemma real_of_extreal_pos:
   fixes x :: extreal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
 
 lemmas real_of_extreal_ord_simps =
   extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff
 
+lemma abs_extreal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: extreal\<bar> = x"
+  by (cases x) auto
+
+lemma abs_extreal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: extreal\<bar> = -x"
+  by (cases x) auto
+
+lemma abs_extreal_pos[simp]: "0 \<le> \<bar>x :: extreal\<bar>"
+  by (cases x) auto
+
+lemma real_of_extreal_le_0[simp]: "real (X :: extreal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)"
+  by (cases X) auto
+
+lemma abs_real_of_extreal[simp]: "\<bar>real (X :: extreal)\<bar> = real \<bar>X\<bar>"
+  by (cases X) auto
+
+lemma zero_less_real_of_extreal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)"
+  by (cases X) auto
+
+lemma extreal_0_le_uminus_iff[simp]:
+  fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
+  by (cases rule: extreal2_cases[of a]) auto
+
+lemma extreal_uminus_le_0_iff[simp]:
+  fixes a :: extreal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
+  by (cases rule: extreal2_cases[of a]) auto
+
 lemma extreal_dense:
   fixes x y :: extreal assumes "x < y"
   shows "EX z. x < z & z < y"
@@ -444,6 +472,9 @@
   and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
   unfolding decseq_def incseq_def by auto
 
+lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
+  unfolding incseq_def by auto
+
 lemma extreal_add_nonneg_nonneg:
   fixes a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   using add_mono[of 0 a 0 b] by simp
@@ -511,6 +542,10 @@
 qed
 end
 
+lemma real_of_extreal_le_1:
+  fixes a :: extreal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
+  by (cases a) (auto simp: one_extreal_def)
+
 lemma abs_extreal_one[simp]: "\<bar>1\<bar> = (1::extreal)"
   unfolding one_extreal_def by simp
 
@@ -702,6 +737,44 @@
   shows "x >= y"
 by (metis assms extreal_dense leD linorder_le_less_linear)
 
+lemma setprod_extreal_0:
+  fixes f :: "'a \<Rightarrow> extreal"
+  shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
+proof cases
+  assume "finite A"
+  then show ?thesis by (induct A) auto
+qed auto
+
+lemma setprod_extreal_pos:
+  fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
+proof cases
+  assume "finite I" from this pos show ?thesis by induct auto
+qed simp
+
+lemma setprod_PInf:
+  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
+  assume "finite I" from this assms show ?thesis
+  proof (induct I)
+    case (insert i I)
+    then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
+    from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
+    also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
+      using setprod_extreal_pos[of I f] pos
+      by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
+    also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
+      using insert by (auto simp: setprod_extreal_0)
+    finally show ?case .
+  qed simp
+qed simp
+
+lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
+proof cases
+  assume "finite A" then show ?thesis
+    by induct (auto simp: one_extreal_def)
+qed (simp add: one_extreal_def)
+
 subsubsection {* Power *}
 
 instantiation extreal :: power
@@ -890,6 +963,11 @@
 instance proof qed
 end
 
+lemma real_of_extreal_inverse[simp]:
+  fixes a :: extreal
+  shows "real (inverse a) = 1 / real a"
+  by (cases a) (auto simp: inverse_eq_divide)
+
 lemma extreal_inverse[simp]:
   "inverse 0 = \<infinity>"
   "inverse (1::extreal) = 1"
@@ -1620,6 +1698,28 @@
   unfolding SUPR_def INFI_def image_image
   by auto
 
+lemma uminus_extreal_add_uminus_uminus:
+  fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
+  by (cases rule: extreal2_cases[of a b]) auto
+
+lemma INFI_extreal_add:
+  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 -
+  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+    using assms unfolding INF_less_iff by auto
+  { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
+      by (rule uminus_extreal_add_uminus_uminus) }
+  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+    by simp
+  also have "\<dots> = INFI UNIV f + INFI UNIV g"
+    unfolding extreal_INFI_uminus
+    using assms INF_less
+    by (subst SUPR_extreal_add)
+       (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
+  finally show ?thesis .
+qed
+
 subsection "Limits on @{typ extreal}"
 
 subsubsection "Topological space"
@@ -1936,9 +2036,6 @@
 } ultimately show ?thesis by blast
 qed
 
-lemma real_of_extreal_0[simp]: "real (0::extreal) = 0"
-  unfolding real_of_extreal_def zero_extreal_def by simp
-
 lemma real_of_extreal_mult[simp]:
   fixes a b :: extreal shows "real (a * b) = real a * real b"
   by (cases rule: extreal2_cases[of a b]) auto
@@ -2406,7 +2503,6 @@
 from this show ?thesis using ext by blast
 qed
 
-
 lemma open_image_extreal: "open(UNIV-{\<infinity>,(-\<infinity>)})"
 by (metis range_extreal open_extreal open_UNIV)
 
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon May 23 19:21:05 2011 +0200
@@ -805,6 +805,21 @@
 } ultimately show ?thesis by auto
 qed
 
+lemma liminf_extreal_cminus:
+  fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
+  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
+proof (cases c)
+  case PInf then show ?thesis by (simp add: Liminf_const)
+next
+  case (real r) then show ?thesis
+    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
+    apply (subst INFI_extreal_cminus)
+    apply auto
+    apply (subst SUPR_extreal_cminus)
+    apply auto
+    done
+qed (insert `c \<noteq> -\<infinity>`, simp)
+
 subsubsection {* Continuity *}
 
 lemma continuous_imp_tendsto:
@@ -1259,4 +1274,20 @@
   finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_extreal)
 qed
 
+lemma suminf_SUP_eq:
+  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> extreal"
+  assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
+  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
+proof -
+  { fix n :: nat
+    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
+      using assms by (auto intro!: SUPR_extreal_setsum[symmetric]) }
+  note * = this
+  show ?thesis using assms
+    apply (subst (1 2) suminf_extreal_eq_SUPR)
+    unfolding *
+    apply (auto intro!: le_SUPI2)
+    apply (subst SUP_commute) ..
+qed
+
 end
\ No newline at end of file
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -8,6 +8,9 @@
 imports Lebesgue_Integration
 begin
 
+lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
+  by auto
+
 lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
@@ -318,9 +321,6 @@
 sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
   by default
 
-lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
-  by auto
-
 lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
 proof
   fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Mon May 23 19:21:05 2011 +0200
@@ -1346,15 +1346,6 @@
     by induct auto
 qed (simp add: borel_measurable_const)
 
-lemma abs_extreal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: extreal\<bar> = x"
-  by (cases x) auto
-
-lemma abs_extreal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: extreal\<bar> = -x"
-  by (cases x) auto
-
-lemma abs_extreal_pos[simp]: "0 \<le> \<bar>x :: extreal\<bar>"
-  by (cases x) auto
-
 lemma (in sigma_algebra) borel_measurable_extreal_abs[intro, simp]:
   fixes f :: "'a \<Rightarrow> extreal" assumes "f \<in> borel_measurable M"
   shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Mon May 23 19:21:05 2011 +0200
@@ -9,6 +9,12 @@
   imports Sigma_Algebra Extended_Real_Limits
 begin
 
+lemma sums_def2:
+  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
+  unfolding sums_def
+  apply (subst LIMSEQ_Suc_iff[symmetric])
+  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
+
 text {*
   Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
 *}
@@ -853,12 +859,6 @@
 
 subsubsection {*Alternative instances of caratheodory*}
 
-lemma sums_def2:
-  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
-  unfolding sums_def
-  apply (subst LIMSEQ_Suc_iff[symmetric])
-  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
-
 lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
   assumes f: "positive M f" "additive M f"
   shows "countably_additive M f \<longleftrightarrow>
@@ -900,28 +900,6 @@
   show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
 qed
 
-lemma uminus_extreal_add_uminus_uminus:
-  fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
-  by (cases rule: extreal2_cases[of a b]) auto
-
-lemma INFI_extreal_add:
-  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 -
-  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
-    using assms unfolding INF_less_iff by auto
-  { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
-      by (rule uminus_extreal_add_uminus_uminus) }
-  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
-    by simp
-  also have "\<dots> = INFI UNIV f + INFI UNIV g"
-    unfolding extreal_INFI_uminus
-    using assms INF_less
-    by (subst SUPR_extreal_add)
-       (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
-  finally show ?thesis .
-qed
-
 lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
   assumes f: "positive M f" "additive M f"
   shows "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -495,44 +495,6 @@
 sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
   by default (fact finite_index')
 
-lemma setprod_extreal_0:
-  fixes f :: "'a \<Rightarrow> extreal"
-  shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
-proof cases
-  assume "finite A"
-  then show ?thesis by (induct A) auto
-qed auto
-
-lemma setprod_extreal_pos:
-  fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
-proof cases
-  assume "finite I" from this pos show ?thesis by induct auto
-qed simp
-
-lemma setprod_PInf:
-  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
-  assume "finite I" from this assms show ?thesis
-  proof (induct I)
-    case (insert i I)
-    then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
-    from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
-    also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
-      using setprod_extreal_pos[of I f] pos
-      by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
-    also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
-      using insert by (auto simp: setprod_extreal_0)
-    finally show ?case .
-  qed simp
-qed simp
-
-lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
-proof cases
-  assume "finite A" then show ?thesis
-    by induct (auto simp: one_extreal_def)
-qed (simp add: one_extreal_def)
-
 lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
   assumes "Pi\<^isub>E I F \<in> sets G"
   shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -223,11 +223,6 @@
     done
 qed
 
-lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
-  unfolding measure_space_1[symmetric]
-  using sets_into_space
-  by (intro measure_mono) auto
-
 definition (in product_prob_space)
   "\<mu>G A =
     (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = measure (Pi\<^isub>M J M) X))"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon May 23 19:21:05 2011 +0200
@@ -45,9 +45,6 @@
   then show ?thesis using assms by (auto intro: measurable_sets)
 qed
 
-lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
-  unfolding incseq_def by auto
-
 lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
 proof
   assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
@@ -2184,21 +2181,6 @@
   using assms unfolding lebesgue_integral_def
   by (subst (1 2) positive_integral_cong_AE) (auto simp add: extreal_real)
 
-lemma liminf_extreal_cminus:
-  fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
-  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
-proof (cases c)
-  case PInf then show ?thesis by (simp add: Liminf_const)
-next
-  case (real r) then show ?thesis
-    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
-    apply (subst INFI_extreal_cminus)
-    apply auto
-    apply (subst SUPR_extreal_cminus)
-    apply auto
-    done
-qed (insert `c \<noteq> -\<infinity>`, simp)
-
 lemma (in measure_space) integral_dominated_convergence:
   assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
   and w: "integrable M w"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -116,22 +116,6 @@
   qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
 qed simp
 
-lemma suminf_SUP_eq:
-  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> extreal"
-  assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
-  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
-proof -
-  { fix n :: nat
-    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
-      using assms by (auto intro!: SUPR_extreal_setsum[symmetric]) }
-  note * = this
-  show ?thesis using assms
-    apply (subst (1 2) suminf_extreal_eq_SUPR)
-    unfolding *
-    apply (auto intro!: le_SUPI2)
-    apply (subst SUP_commute) ..
-qed
-
 interpretation lebesgue: measure_space lebesgue
 proof
   have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
@@ -558,10 +542,6 @@
 
 subsection {* Lebesgue integrable implies Gauge integrable *}
 
-lemma positive_not_Inf:
-  "0 \<le> x \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> \<bar>x\<bar> \<noteq> \<infinity>"
-  by (cases x) auto
-
 lemma has_integral_cmult_real:
   fixes c :: real
   assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
@@ -648,10 +628,6 @@
   qed
 qed
 
-lemma real_of_extreal_positive_mono:
-  "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
-  by (cases rule: extreal2_cases[of x y]) auto
-
 lemma positive_integral_has_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> extreal"
   assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -1162,16 +1162,11 @@
     using finite_measure_of_space by auto
 qed
 
-lemma (in finite_measure) measure_not_inf:
-  assumes A: "A \<in> sets M"
-  shows "\<bar>\<mu> A\<bar> \<noteq> \<infinity>"
-  using finite_measure[OF A] positive_measure[OF A] by auto
-
 definition (in finite_measure)
   "\<mu>' A = (if A \<in> sets M then real (\<mu> A) else 0)"
 
 lemma (in finite_measure) finite_measure_eq: "A \<in> sets M \<Longrightarrow> \<mu> A = extreal (\<mu>' A)"
-  using measure_not_inf[of A] by (auto simp: \<mu>'_def)
+  by (auto simp: \<mu>'_def extreal_real)
 
 lemma (in finite_measure) positive_measure': "0 \<le> \<mu>' A"
   unfolding \<mu>'_def by (auto simp: real_of_extreal_pos)
@@ -1182,8 +1177,7 @@
   moreover then have "\<mu> A \<le> \<mu> (space M)"
     using sets_into_space by (auto intro!: measure_mono)
   ultimately show ?thesis
-    using measure_not_inf[of A] measure_not_inf[of "space M"]
-    by (auto simp: \<mu>'_def)
+    by (auto simp: \<mu>'_def intro!: real_of_extreal_positive_mono)
 qed (simp add: \<mu>'_def real_of_extreal_pos)
 
 lemma (in finite_measure) restricted_finite_measure:
diff -r 618adb3584e5 -r 6e5c2a3c69da src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Mon May 23 19:21:05 2011 +0200
@@ -9,23 +9,6 @@
 imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure Lebesgue_Measure
 begin
 
-lemma real_of_extreal_inverse[simp]:
-  fixes X :: extreal
-  shows "real (inverse X) = 1 / real X"
-  by (cases X) (auto simp: inverse_eq_divide)
-
-lemma real_of_extreal_le_0[simp]: "real (X :: extreal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)"
-  by (cases X) auto
-
-lemma abs_real_of_extreal[simp]: "\<bar>real (X :: extreal)\<bar> = real \<bar>X\<bar>"
-  by (cases X) auto
-
-lemma zero_less_real_of_extreal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)"
-  by (cases X) auto
-
-lemma real_of_extreal_le_1: fixes X :: extreal shows "X \<le> 1 \<Longrightarrow> real X \<le> 1"
-  by (cases X) (auto simp: one_extreal_def)
-
 locale prob_space = measure_space +
   assumes measure_space_1: "measure M (space M) = 1"
 
@@ -83,6 +66,11 @@
     "joint_distribution X X {(x, x)} = distribution X {x}"
   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
 
+lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
+  unfolding measure_space_1[symmetric]
+  using sets_into_space
+  by (intro measure_mono) auto
+
 lemma (in prob_space) distribution_1:
   "distribution X A \<le> 1"
   unfolding distribution_def by simp
@@ -1017,10 +1005,6 @@
   qed
 qed
 
-lemma extreal_0_le_iff_le_0[simp]:
-  fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
-  by (cases rule: extreal2_cases[of a]) auto
-
 lemma (in sigma_algebra) factorize_measurable_function:
   fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c"
   assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"