Move SUP_commute, SUP_less_iff to HOL image;
Cleanup generic complete_lattice lemmas in Positive_Infinite_Real;
Cleanup lemma positive_integral_alt;

--- a/src/HOL/Complete_Lattice.thy	Wed Dec 01 21:03:02 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Thu Dec 02 14:34:58 2010 +0100
@@ -172,6 +172,18 @@
   "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
   by (force intro!: Inf_mono simp: INFI_def)
 
+lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
+  by (intro SUP_mono) auto
+
+lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
+  by (intro INF_mono) auto
+
+lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
+  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
+
+lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
+  by (iprover intro: INF_leI le_INFI order_trans antisym)
+
 end
 
 lemma less_Sup_iff:
@@ -184,6 +196,16 @@
   shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   unfolding not_le[symmetric] le_Inf_iff by auto
 
+lemma less_SUP_iff:
+  fixes a :: "'a::{complete_lattice,linorder}"
+  shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
+  unfolding SUPR_def less_Sup_iff by auto
+
+lemma INF_less_iff:
+  fixes a :: "'a::{complete_lattice,linorder}"
+  shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+  unfolding INFI_def Inf_less_iff by auto
+
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
 instantiation bool :: complete_lattice

--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 01 21:03:02 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 02 14:34:58 2010 +0100
@@ -849,7 +849,7 @@
 
 definition (in measure_space)
   "positive_integral f =
-    (SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)"
+    SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M} simple_integral"
 
 lemma (in measure_space) positive_integral_cong_measure:
   assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A"
@@ -883,74 +883,71 @@
     by auto
 qed
 
+lemma image_set_cong:
+  assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
+  assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x"
+  shows "f ` A = g ` B"
+  using assms by blast
+
 lemma (in measure_space) positive_integral_alt:
   "positive_integral f =
-    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)"
-  apply(rule order_class.antisym) unfolding positive_integral_def 
-  apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim)
-proof safe fix u assume u:"simple_function u" and uf:"u \<le> f"
-  let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x"
-  have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] .
-  show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and>
-    (\<lambda>n. simple_integral (b n)) ----> simple_integral u"
-    apply(rule_tac x="?u" in exI, safe) apply(rule su)
-  proof- fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto
-    also note uf finally show "?u n \<le> f" .
-    let ?s = "{x \<in> space M. u x = \<omega>}"
-    show "(\<lambda>n. simple_integral (?u n)) ----> simple_integral u"
-    proof(cases "\<mu> ?s = 0")
-      case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto 
-      have *:"\<And>n. simple_integral (?u n) = simple_integral u"
-        apply(rule simple_integral_cong'[OF su u]) unfolding * True ..
-      show ?thesis unfolding * by auto 
-    next case False note m0=this
-      have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u  by (auto simp: borel_measurable_simple_function)
-      have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)"
-        apply(subst simple_integral_mult) using s
-        unfolding simple_integral_indicator_only[OF s] using False by auto
-      also have "... \<le> simple_integral u"
-        apply (rule simple_integral_mono)
-        apply (rule simple_function_mult)
-        apply (rule simple_function_const)
-        apply(rule ) prefer 3 apply(subst indicator_def)
-        using s u by auto
-      finally have *:"simple_integral u = \<omega>" by auto
-      show ?thesis unfolding * Lim_omega_pos
-      proof safe case goal1
-        from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this
-        def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0"
-          unfolding N_def using N by auto
-        show ?case apply-apply(rule_tac x=N in exI,safe) 
-        proof- case goal1
-          have "Real B \<le> Real (real N) * \<mu> ?s"
-          proof(cases "\<mu> ?s = \<omega>")
-            case True thus ?thesis using `B>0` N by auto
-          next case False
-            have *:"B \<le> real N * real (\<mu> ?s)" 
-              using N(1) apply-apply(subst (asm) pos_divide_le_eq)
-              apply rule using m0 False by auto
-            show ?thesis apply(subst Real_real'[THEN sym,OF False])
-              apply(subst pinfreal_times,subst if_P) defer
-              apply(subst pinfreal_less_eq,subst if_P) defer
-              using * N `B>0` by(auto intro: mult_nonneg_nonneg)
-          qed
-          also have "... \<le> Real (real n) * \<mu> ?s"
-            apply(rule mult_right_mono) using goal1 by auto
-          also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)" 
-            apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s])
-            unfolding simple_integral_indicator_only[OF s] ..
-          also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)"
-            apply(rule simple_integral_mono) apply(rule simple_function_mult)
-            apply(rule simple_function_const)
-            apply(rule simple_function_indicator) apply(rule s su)+ by auto
-          finally show ?case .
-        qed qed qed
-    fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M"
-    hence "u x = \<omega>" apply-apply(rule ccontr) by auto
-    hence "\<omega> = Real (real n)" using x by auto
-    thus False by auto
+    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)" (is "_ = ?alt")
+proof (rule antisym SUP_leI)
+  show "?alt \<le> positive_integral f" unfolding positive_integral_def
+  proof (safe intro!: SUP_leI)
+    fix g assume g: "simple_function g" "g \<le> f"
+    let ?G = "g -` {\<omega>} \<inter> space M"
+    show "simple_integral g \<le>
+      SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} simple_integral"
+      (is "simple_integral g \<le> SUPR ?A simple_integral")
+    proof cases
+      let ?g = "\<lambda>x. indicator (space M - ?G) x * g x"
+      have g': "simple_function ?g"
+        using g by (auto intro: simple_functionD)
+      moreover
+      assume "\<mu> ?G = 0"
+      then have "AE x. g x = ?g x" using g
+        by (intro AE_I[where N="?G"])
+           (auto intro: simple_functionD simp: indicator_def)
+      with g(1) g' have "simple_integral g = simple_integral ?g"
+        by (rule simple_integral_cong_AE)
+      moreover have "?g \<le> g" by (auto simp: le_fun_def indicator_def)
+      from this `g \<le> f` have "?g \<le> f" by (rule order_trans)
+      moreover have "\<omega> \<notin> ?g ` space M"
+        by (auto simp: indicator_def split: split_if_asm)
+      ultimately show ?thesis by (auto intro!: le_SUPI)
+    next
+      assume "\<mu> ?G \<noteq> 0"
+      then have "?G \<noteq> {}" by auto
+      then have "\<omega> \<in> g`space M" by force
+      then have "space M \<noteq> {}" by auto
+      have "SUPR ?A simple_integral = \<omega>"
+      proof (intro SUP_\<omega>[THEN iffD2] allI impI)
+        fix x assume "x < \<omega>"
+        then guess n unfolding less_\<omega>_Ex_of_nat .. note n = this
+        then have "0 < n" by (intro neq0_conv[THEN iffD1] notI) simp
+        let ?g = "\<lambda>x. (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * indicator ?G x"
+        show "\<exists>i\<in>?A. x < simple_integral i"
+        proof (intro bexI impI CollectI conjI)
+          show "simple_function ?g" using g
+            by (auto intro!: simple_functionD simple_function_add)
+          have "?g \<le> g" by (auto simp: le_fun_def indicator_def)
+          from this g(2) show "?g \<le> f" by (rule order_trans)
+          show "\<omega> \<notin> ?g ` space M"
+            using `\<mu> ?G \<noteq> 0` by (auto simp: indicator_def split: split_if_asm)
+          have "x < (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * \<mu> ?G"
+            using n `\<mu> ?G \<noteq> 0` `0 < n`
+            by (auto simp: pinfreal_noteq_omega_Ex field_simps)
+          also have "\<dots> = simple_integral ?g" using g `space M \<noteq> {}`
+            by (subst simple_integral_indicator)
+               (auto simp: image_constant ac_simps dest: simple_functionD)
+          finally show "x < simple_integral ?g" .
+        qed
+      qed
+      then show ?thesis by simp
+    qed
   qed
-qed
+qed (auto intro!: SUP_subset simp: positive_integral_def)
 
 lemma (in measure_space) positive_integral_cong:
   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
@@ -1025,12 +1022,6 @@
   shows "positive_integral u \<le> positive_integral v"
   using mono by (auto intro!: AE_cong positive_integral_mono_AE)
 
-lemma image_set_cong:
-  assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
-  assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x"
-  shows "f ` A = g ` B"
-  using assms by blast
-
 lemma (in measure_space) positive_integral_vimage:
   fixes g :: "'a \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a"
   assumes f: "bij_betw f S (space M)"
@@ -1229,6 +1220,7 @@
       using assms by (simp cong: measurable_cong)
     moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
       unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
+      using SUP_const[OF UNIV_not_empty]
       by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
     ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
       unfolding positive_integral_def[of ru]

--- a/src/HOL/Probability/Positive_Infinite_Real.thy	Wed Dec 01 21:03:02 2010 +0100
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Thu Dec 02 14:34:58 2010 +0100
@@ -6,57 +6,6 @@
   imports Complex_Main Nat_Bijection Multivariate_Analysis
 begin
 
-lemma (in complete_lattice) SUPR_upper:
-  "x \<in> A \<Longrightarrow> f x \<le> SUPR A f"
-  unfolding SUPR_def apply(rule Sup_upper) by auto
-
-lemma (in complete_lattice) SUPR_subset:
-  assumes "A \<subseteq> B" shows "SUPR A f \<le> SUPR B f"
-  apply(rule SUP_leI) apply(rule SUPR_upper) using assms by auto
-
-lemma (in complete_lattice) SUPR_mono:
-  assumes "\<forall>a\<in>A. \<exists>b\<in>B. f b \<ge> f a"
-  shows "SUPR A f \<le> SUPR B f"
-  unfolding SUPR_def apply(rule Sup_mono)
-  using assms by auto
-
-lemma (in complete_lattice) SUP_pair:
-  "(SUP i:A. SUP j:B. f i j) = (SUP p:A\<times>B. (\<lambda> (i, j). f i j) p)" (is "?l = ?r")
-proof (intro antisym SUP_leI)
-  fix i j assume "i \<in> A" "j \<in> B"
-  then have "(case (i,j) of (i,j) \<Rightarrow> f i j) \<le> ?r"
-    by (intro SUPR_upper) auto
-  then show "f i j \<le> ?r" by auto
-next
-  fix p assume "p \<in> A \<times> B"
-  then obtain i j where "p = (i,j)" "i \<in> A" "j \<in> B" by auto
-  have "f i j \<le> (SUP j:B. f i j)" using `j \<in> B` by (intro SUPR_upper)
-  also have "(SUP j:B. f i j) \<le> ?l" using `i \<in> A` by (intro SUPR_upper)
-  finally show "(case p of (i, j) \<Rightarrow> f i j) \<le> ?l" using `p = (i,j)` by simp
-qed
-
-lemma (in complete_lattice) SUP_surj_compose:
-  assumes *: "f`A = B" shows "SUPR A (g \<circ> f) = SUPR B g"
-  unfolding SUPR_def unfolding *[symmetric]
-  by (simp add: image_compose)
-
-lemma (in complete_lattice) SUP_swap:
-  "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
-proof -
-  have *: "(\<lambda>(i,j). (j,i)) ` (B \<times> A) = A \<times> B" by auto
-  show ?thesis
-    unfolding SUP_pair SUP_surj_compose[symmetric, OF *]
-    by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def)
-qed
-
-lemma range_const[simp]: "range (\<lambda>x. c) = {c}" by auto
-
-lemma (in complete_lattice) SUPR_const[simp]: "(SUP i. c) = c"
-  unfolding SUPR_def by simp
-
-lemma (in complete_lattice) INFI_const[simp]: "(INF i. c) = c"
-  unfolding INFI_def by simp
-
 lemma (in complete_lattice) Sup_start:
   assumes *: "\<And>x. f x \<le> f 0"
   shows "(SUP n. f n) = f 0"
@@ -137,6 +86,26 @@
   ultimately show ?thesis by simp
 qed
 
+lemma (in complete_lattice) lim_INF_le_lim_SUP:
+  fixes f :: "nat \<Rightarrow> 'a"
+  shows "(SUP n. INF m. f (n + m)) \<le> (INF n. SUP m. f (n + m))"
+proof (rule SUP_leI, rule le_INFI)
+  fix i j show "(INF m. f (i + m)) \<le> (SUP m. f (j + m))"
+  proof (cases rule: le_cases)
+    assume "i \<le> j"
+    have "(INF m. f (i + m)) \<le> f (i + (j - i))" by (rule INF_leI) simp
+    also have "\<dots> = f (j + 0)" using `i \<le> j` by auto
+    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
+    finally show ?thesis .
+  next
+    assume "j \<le> i"
+    have "(INF m. f (i + m)) \<le> f (i + 0)" by (rule INF_leI) simp
+    also have "\<dots> = f (j + (i - j))" using `j \<le> i` by auto
+    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
+    finally show ?thesis .
+  qed
+qed
+
 text {*
 
 We introduce the the positive real numbers as needed for measure theory.
@@ -882,11 +851,6 @@
   qed simp
 qed simp
 
-lemma less_SUP_iff:
-  fixes a :: "'a::{complete_lattice,linorder}"
-  shows "(a < (SUP i:A. f i)) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
-  unfolding SUPR_def less_Sup_iff by auto
-
 lemma SUP_\<omega>: "(SUP i:A. f i) = \<omega> \<longleftrightarrow> (\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)"
 proof
   assume *: "(SUP i:A. f i) = \<omega>"
@@ -1320,7 +1284,6 @@
   have [intro, simp]: "\<And>A. inj_on f A" using `bij f` unfolding bij_def by (auto intro: subset_inj_on)
   have f[intro, simp]: "\<And>x. f (inv f x) = x"
     using `bij f` unfolding bij_def by (auto intro: surj_f_inv_f)
-
   show ?thesis
   proof (rule psuminf_equality)
     fix n
@@ -1345,49 +1308,6 @@
   qed
 qed
 
-lemma psuminf_2dimen:
-  fixes f:: "nat * nat \<Rightarrow> pinfreal"
-  assumes fsums: "\<And>m. g m = (\<Sum>\<^isub>\<infinity> n. f (m,n))"
-  shows "psuminf (f \<circ> prod_decode) = psuminf g"
-proof (rule psuminf_equality)
-  fix n :: nat
-  let ?P = "prod_decode ` {..<n}"
-  have "setsum (f \<circ> prod_decode) {..<n} = setsum f ?P"
-    by (auto simp: setsum_reindex inj_prod_decode)
-  also have "\<dots> \<le> setsum f ({..Max (fst ` ?P)} \<times> {..Max (snd ` ?P)})"
-  proof (safe intro!: setsum_mono3 Max_ge image_eqI)
-    fix a b x assume "(a, b) = prod_decode x"
-    from this[symmetric] show "a = fst (prod_decode x)" "b = snd (prod_decode x)"
-      by simp_all
-  qed simp_all
-  also have "\<dots> = (\<Sum>m\<le>Max (fst ` ?P). (\<Sum>n\<le>Max (snd ` ?P). f (m,n)))"
-    unfolding setsum_cartesian_product by simp
-  also have "\<dots> \<le> (\<Sum>m\<le>Max (fst ` ?P). g m)"
-    by (auto intro!: setsum_mono psuminf_upper simp del: setsum_lessThan_Suc
-        simp: fsums lessThan_Suc_atMost[symmetric])
-  also have "\<dots> \<le> psuminf g"
-    by (auto intro!: psuminf_upper simp del: setsum_lessThan_Suc
-        simp: lessThan_Suc_atMost[symmetric])
-  finally show "setsum (f \<circ> prod_decode) {..<n} \<le> psuminf g" .
-next
-  fix y assume *: "\<And>n. setsum (f \<circ> prod_decode) {..<n} \<le> y"
-  have g: "g = (\<lambda>m. \<Sum>\<^isub>\<infinity> n. f (m,n))" unfolding fsums[symmetric] ..
-  show "psuminf g \<le> y" unfolding g
-  proof (rule psuminf_bound, unfold setsum_pinfsum[symmetric], safe intro!: psuminf_bound)
-    fix N M :: nat
-    let ?P = "{..<N} \<times> {..<M}"
-    let ?M = "Max (prod_encode ` ?P)"
-    have "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> (\<Sum>(m, n)\<in>?P. f (m, n))"
-      unfolding setsum_commute[of _ _ "{..<M}"] unfolding setsum_cartesian_product ..
-    also have "\<dots> \<le> (\<Sum>(m,n)\<in>(prod_decode ` {..?M}). f (m, n))"
-      by (auto intro!: setsum_mono3 image_eqI[where f=prod_decode, OF prod_encode_inverse[symmetric]])
-    also have "\<dots> \<le> y" using *[of "Suc ?M"]
-      by (simp add: lessThan_Suc_atMost[symmetric] setsum_reindex
-               inj_prod_decode del: setsum_lessThan_Suc)
-    finally show "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> y" .
-  qed
-qed
-
 lemma pinfreal_mult_less_right:
   assumes "b * a < c * a" "0 < a" "a < \<omega>"
   shows "b < c"
@@ -1474,7 +1394,7 @@
   show ?thesis
     unfolding psuminf_def
     unfolding *
-    apply (subst SUP_swap) ..
+    apply (subst SUP_commute) ..
 qed
 
 lemma psuminf_commute:
@@ -1484,7 +1404,7 @@
     apply (subst SUPR_pinfreal_setsum)
     by auto
   also have "\<dots> = (SUP m n. \<Sum> j < m. \<Sum> i < n. f i j)"
-    apply (subst SUP_swap)
+    apply (subst SUP_commute)
     apply (subst setsum_commute)
     by auto
   also have "\<dots> = (SUP m. \<Sum> j < m. SUP n. \<Sum> i < n. f i j)"
@@ -1494,6 +1414,49 @@
     unfolding psuminf_def by auto
 qed
 
+lemma psuminf_2dimen:
+  fixes f:: "nat * nat \<Rightarrow> pinfreal"
+  assumes fsums: "\<And>m. g m = (\<Sum>\<^isub>\<infinity> n. f (m,n))"
+  shows "psuminf (f \<circ> prod_decode) = psuminf g"
+proof (rule psuminf_equality)
+  fix n :: nat
+  let ?P = "prod_decode ` {..<n}"
+  have "setsum (f \<circ> prod_decode) {..<n} = setsum f ?P"
+    by (auto simp: setsum_reindex inj_prod_decode)
+  also have "\<dots> \<le> setsum f ({..Max (fst ` ?P)} \<times> {..Max (snd ` ?P)})"
+  proof (safe intro!: setsum_mono3 Max_ge image_eqI)
+    fix a b x assume "(a, b) = prod_decode x"
+    from this[symmetric] show "a = fst (prod_decode x)" "b = snd (prod_decode x)"
+      by simp_all
+  qed simp_all
+  also have "\<dots> = (\<Sum>m\<le>Max (fst ` ?P). (\<Sum>n\<le>Max (snd ` ?P). f (m,n)))"
+    unfolding setsum_cartesian_product by simp
+  also have "\<dots> \<le> (\<Sum>m\<le>Max (fst ` ?P). g m)"
+    by (auto intro!: setsum_mono psuminf_upper simp del: setsum_lessThan_Suc
+        simp: fsums lessThan_Suc_atMost[symmetric])
+  also have "\<dots> \<le> psuminf g"
+    by (auto intro!: psuminf_upper simp del: setsum_lessThan_Suc
+        simp: lessThan_Suc_atMost[symmetric])
+  finally show "setsum (f \<circ> prod_decode) {..<n} \<le> psuminf g" .
+next
+  fix y assume *: "\<And>n. setsum (f \<circ> prod_decode) {..<n} \<le> y"
+  have g: "g = (\<lambda>m. \<Sum>\<^isub>\<infinity> n. f (m,n))" unfolding fsums[symmetric] ..
+  show "psuminf g \<le> y" unfolding g
+  proof (rule psuminf_bound, unfold setsum_pinfsum[symmetric], safe intro!: psuminf_bound)
+    fix N M :: nat
+    let ?P = "{..<N} \<times> {..<M}"
+    let ?M = "Max (prod_encode ` ?P)"
+    have "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> (\<Sum>(m, n)\<in>?P. f (m, n))"
+      unfolding setsum_commute[of _ _ "{..<M}"] unfolding setsum_cartesian_product ..
+    also have "\<dots> \<le> (\<Sum>(m,n)\<in>(prod_decode ` {..?M}). f (m, n))"
+      by (auto intro!: setsum_mono3 image_eqI[where f=prod_decode, OF prod_encode_inverse[symmetric]])
+    also have "\<dots> \<le> y" using *[of "Suc ?M"]
+      by (simp add: lessThan_Suc_atMost[symmetric] setsum_reindex
+               inj_prod_decode del: setsum_lessThan_Suc)
+    finally show "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> y" .
+  qed
+qed
+
 lemma Real_max:
   assumes "x \<ge> 0" "y \<ge> 0"
   shows "Real (max x y) = max (Real x) (Real y)"
@@ -2462,26 +2425,6 @@
   shows "a \<le> a - b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a \<noteq> \<omega> \<Longrightarrow> b = 0"
   by (cases a, cases b, auto split: split_if_asm)
 
-lemma lim_INF_le_lim_SUP:
-  fixes f :: "nat \<Rightarrow> pinfreal"
-  shows "(SUP n. INF m. f (n + m)) \<le> (INF n. SUP m. f (n + m))"
-proof (rule complete_lattice_class.SUP_leI, rule complete_lattice_class.le_INFI)
-  fix i j show "(INF m. f (i + m)) \<le> (SUP m. f (j + m))"
-  proof (cases rule: le_cases)
-    assume "i \<le> j"
-    have "(INF m. f (i + m)) \<le> f (i + (j - i))" by (rule INF_leI) simp
-    also have "\<dots> = f (j + 0)" using `i \<le> j` by auto
-    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
-    finally show ?thesis .
-  next
-    assume "j \<le> i"
-    have "(INF m. f (i + m)) \<le> f (i + 0)" by (rule INF_leI) simp
-    also have "\<dots> = f (j + (i - j))" using `j \<le> i` by auto
-    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
-    finally show ?thesis .
-  qed
-qed
-
 lemma lim_INF_eq_lim_SUP:
   fixes X :: "nat \<Rightarrow> real"
   assumes "\<And>i. 0 \<le> X i" and "0 \<le> x"

--- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 01 21:03:02 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Dec 02 14:34:58 2010 +0100
@@ -865,7 +865,7 @@
 
 lemma (in finite_product_sigma_algebra) P_empty:
   "I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
-  unfolding product_algebra_def by (simp add: sigma_def)
+  unfolding product_algebra_def by (simp add: sigma_def image_constant)
 
 lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
   "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
@@ -1258,7 +1258,7 @@
     by (auto intro!: exI[of _ "\<lambda>A. if A = {} then 0 else 1"] sigma_algebra_sigma
                      sigma_algebra.finite_additivity_sufficient
              simp add: positive_def additive_def sets_sigma sigma_finite_measure_def
-                       sigma_finite_measure_axioms_def)
+                       sigma_finite_measure_axioms_def image_constant)
 next
   case (insert i I)
   interpret finite_product_sigma_finite M \<mu> I by default fact

--- a/src/HOL/Set.thy	Wed Dec 01 21:03:02 2010 +0100
+++ b/src/HOL/Set.thy	Thu Dec 02 14:34:58 2010 +0100
@@ -882,7 +882,6 @@
 lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
   by blast
 
-
 subsubsection {* Some rules with @{text "if"} *}
 
 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}