Move SUP_commute, SUP_less_iff to HOL image;
authorhoelzl
Thu Dec 02 14:34:58 2010 +0100 (2010-12-02)
changeset 408727c556a9240de
parent 40871 688f6ff859e1
child 40873 1ef85f4e7097
Move SUP_commute, SUP_less_iff to HOL image;
Cleanup generic complete_lattice lemmas in Positive_Infinite_Real;
Cleanup lemma positive_integral_alt;
src/HOL/Complete_Lattice.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Positive_Infinite_Real.thy
src/HOL/Probability/Product_Measure.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Dec 01 21:03:02 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Dec 02 14:34:58 2010 +0100
     1.3 @@ -172,6 +172,18 @@
     1.4    "(\<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)"
     1.5    by (force intro!: Inf_mono simp: INFI_def)
     1.6  
     1.7 +lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f"
     1.8 +  by (intro SUP_mono) auto
     1.9 +
    1.10 +lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f"
    1.11 +  by (intro INF_mono) auto
    1.12 +
    1.13 +lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
    1.14 +  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
    1.15 +
    1.16 +lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
    1.17 +  by (iprover intro: INF_leI le_INFI order_trans antisym)
    1.18 +
    1.19  end
    1.20  
    1.21  lemma less_Sup_iff:
    1.22 @@ -184,6 +196,16 @@
    1.23    shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
    1.24    unfolding not_le[symmetric] le_Inf_iff by auto
    1.25  
    1.26 +lemma less_SUP_iff:
    1.27 +  fixes a :: "'a::{complete_lattice,linorder}"
    1.28 +  shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    1.29 +  unfolding SUPR_def less_Sup_iff by auto
    1.30 +
    1.31 +lemma INF_less_iff:
    1.32 +  fixes a :: "'a::{complete_lattice,linorder}"
    1.33 +  shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
    1.34 +  unfolding INFI_def Inf_less_iff by auto
    1.35 +
    1.36  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    1.37  
    1.38  instantiation bool :: complete_lattice
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 01 21:03:02 2010 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 02 14:34:58 2010 +0100
     2.3 @@ -849,7 +849,7 @@
     2.4  
     2.5  definition (in measure_space)
     2.6    "positive_integral f =
     2.7 -    (SUP g : {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. simple_integral g)"
     2.8 +    SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M} simple_integral"
     2.9  
    2.10  lemma (in measure_space) positive_integral_cong_measure:
    2.11    assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A"
    2.12 @@ -883,74 +883,71 @@
    2.13      by auto
    2.14  qed
    2.15  
    2.16 +lemma image_set_cong:
    2.17 +  assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
    2.18 +  assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x"
    2.19 +  shows "f ` A = g ` B"
    2.20 +  using assms by blast
    2.21 +
    2.22  lemma (in measure_space) positive_integral_alt:
    2.23    "positive_integral f =
    2.24 -    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)"
    2.25 -  apply(rule order_class.antisym) unfolding positive_integral_def 
    2.26 -  apply(rule SUPR_subset) apply blast apply(rule SUPR_mono_lim)
    2.27 -proof safe fix u assume u:"simple_function u" and uf:"u \<le> f"
    2.28 -  let ?u = "\<lambda>n x. if u x = \<omega> then Real (real (n::nat)) else u x"
    2.29 -  have su:"\<And>n. simple_function (?u n)" using simple_function_compose1[OF u] .
    2.30 -  show "\<exists>b. \<forall>n. b n \<in> {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} \<and>
    2.31 -    (\<lambda>n. simple_integral (b n)) ----> simple_integral u"
    2.32 -    apply(rule_tac x="?u" in exI, safe) apply(rule su)
    2.33 -  proof- fix n::nat have "?u n \<le> u" unfolding le_fun_def by auto
    2.34 -    also note uf finally show "?u n \<le> f" .
    2.35 -    let ?s = "{x \<in> space M. u x = \<omega>}"
    2.36 -    show "(\<lambda>n. simple_integral (?u n)) ----> simple_integral u"
    2.37 -    proof(cases "\<mu> ?s = 0")
    2.38 -      case True have *:"\<And>n. {x\<in>space M. ?u n x \<noteq> u x} = {x\<in>space M. u x = \<omega>}" by auto 
    2.39 -      have *:"\<And>n. simple_integral (?u n) = simple_integral u"
    2.40 -        apply(rule simple_integral_cong'[OF su u]) unfolding * True ..
    2.41 -      show ?thesis unfolding * by auto 
    2.42 -    next case False note m0=this
    2.43 -      have s:"{x \<in> space M. u x = \<omega>} \<in> sets M" using u  by (auto simp: borel_measurable_simple_function)
    2.44 -      have "\<omega> = simple_integral (\<lambda>x. \<omega> * indicator {x\<in>space M. u x = \<omega>} x)"
    2.45 -        apply(subst simple_integral_mult) using s
    2.46 -        unfolding simple_integral_indicator_only[OF s] using False by auto
    2.47 -      also have "... \<le> simple_integral u"
    2.48 -        apply (rule simple_integral_mono)
    2.49 -        apply (rule simple_function_mult)
    2.50 -        apply (rule simple_function_const)
    2.51 -        apply(rule ) prefer 3 apply(subst indicator_def)
    2.52 -        using s u by auto
    2.53 -      finally have *:"simple_integral u = \<omega>" by auto
    2.54 -      show ?thesis unfolding * Lim_omega_pos
    2.55 -      proof safe case goal1
    2.56 -        from real_arch_simple[of "B / real (\<mu> ?s)"] guess N0 .. note N=this
    2.57 -        def N \<equiv> "Suc N0" have N:"real N \<ge> B / real (\<mu> ?s)" "N > 0"
    2.58 -          unfolding N_def using N by auto
    2.59 -        show ?case apply-apply(rule_tac x=N in exI,safe) 
    2.60 -        proof- case goal1
    2.61 -          have "Real B \<le> Real (real N) * \<mu> ?s"
    2.62 -          proof(cases "\<mu> ?s = \<omega>")
    2.63 -            case True thus ?thesis using `B>0` N by auto
    2.64 -          next case False
    2.65 -            have *:"B \<le> real N * real (\<mu> ?s)" 
    2.66 -              using N(1) apply-apply(subst (asm) pos_divide_le_eq)
    2.67 -              apply rule using m0 False by auto
    2.68 -            show ?thesis apply(subst Real_real'[THEN sym,OF False])
    2.69 -              apply(subst pinfreal_times,subst if_P) defer
    2.70 -              apply(subst pinfreal_less_eq,subst if_P) defer
    2.71 -              using * N `B>0` by(auto intro: mult_nonneg_nonneg)
    2.72 -          qed
    2.73 -          also have "... \<le> Real (real n) * \<mu> ?s"
    2.74 -            apply(rule mult_right_mono) using goal1 by auto
    2.75 -          also have "... = simple_integral (\<lambda>x. Real (real n) * indicator ?s x)" 
    2.76 -            apply(subst simple_integral_mult) apply(rule simple_function_indicator[OF s])
    2.77 -            unfolding simple_integral_indicator_only[OF s] ..
    2.78 -          also have "... \<le> simple_integral (\<lambda>x. if u x = \<omega> then Real (real n) else u x)"
    2.79 -            apply(rule simple_integral_mono) apply(rule simple_function_mult)
    2.80 -            apply(rule simple_function_const)
    2.81 -            apply(rule simple_function_indicator) apply(rule s su)+ by auto
    2.82 -          finally show ?case .
    2.83 -        qed qed qed
    2.84 -    fix x assume x:"\<omega> = (if u x = \<omega> then Real (real n) else u x)" "x \<in> space M"
    2.85 -    hence "u x = \<omega>" apply-apply(rule ccontr) by auto
    2.86 -    hence "\<omega> = Real (real n)" using x by auto
    2.87 -    thus False by auto
    2.88 +    (SUP g : {g. simple_function g \<and> g \<le> f}. simple_integral g)" (is "_ = ?alt")
    2.89 +proof (rule antisym SUP_leI)
    2.90 +  show "?alt \<le> positive_integral f" unfolding positive_integral_def
    2.91 +  proof (safe intro!: SUP_leI)
    2.92 +    fix g assume g: "simple_function g" "g \<le> f"
    2.93 +    let ?G = "g -` {\<omega>} \<inter> space M"
    2.94 +    show "simple_integral g \<le>
    2.95 +      SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} simple_integral"
    2.96 +      (is "simple_integral g \<le> SUPR ?A simple_integral")
    2.97 +    proof cases
    2.98 +      let ?g = "\<lambda>x. indicator (space M - ?G) x * g x"
    2.99 +      have g': "simple_function ?g"
   2.100 +        using g by (auto intro: simple_functionD)
   2.101 +      moreover
   2.102 +      assume "\<mu> ?G = 0"
   2.103 +      then have "AE x. g x = ?g x" using g
   2.104 +        by (intro AE_I[where N="?G"])
   2.105 +           (auto intro: simple_functionD simp: indicator_def)
   2.106 +      with g(1) g' have "simple_integral g = simple_integral ?g"
   2.107 +        by (rule simple_integral_cong_AE)
   2.108 +      moreover have "?g \<le> g" by (auto simp: le_fun_def indicator_def)
   2.109 +      from this `g \<le> f` have "?g \<le> f" by (rule order_trans)
   2.110 +      moreover have "\<omega> \<notin> ?g ` space M"
   2.111 +        by (auto simp: indicator_def split: split_if_asm)
   2.112 +      ultimately show ?thesis by (auto intro!: le_SUPI)
   2.113 +    next
   2.114 +      assume "\<mu> ?G \<noteq> 0"
   2.115 +      then have "?G \<noteq> {}" by auto
   2.116 +      then have "\<omega> \<in> g`space M" by force
   2.117 +      then have "space M \<noteq> {}" by auto
   2.118 +      have "SUPR ?A simple_integral = \<omega>"
   2.119 +      proof (intro SUP_\<omega>[THEN iffD2] allI impI)
   2.120 +        fix x assume "x < \<omega>"
   2.121 +        then guess n unfolding less_\<omega>_Ex_of_nat .. note n = this
   2.122 +        then have "0 < n" by (intro neq0_conv[THEN iffD1] notI) simp
   2.123 +        let ?g = "\<lambda>x. (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * indicator ?G x"
   2.124 +        show "\<exists>i\<in>?A. x < simple_integral i"
   2.125 +        proof (intro bexI impI CollectI conjI)
   2.126 +          show "simple_function ?g" using g
   2.127 +            by (auto intro!: simple_functionD simple_function_add)
   2.128 +          have "?g \<le> g" by (auto simp: le_fun_def indicator_def)
   2.129 +          from this g(2) show "?g \<le> f" by (rule order_trans)
   2.130 +          show "\<omega> \<notin> ?g ` space M"
   2.131 +            using `\<mu> ?G \<noteq> 0` by (auto simp: indicator_def split: split_if_asm)
   2.132 +          have "x < (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * \<mu> ?G"
   2.133 +            using n `\<mu> ?G \<noteq> 0` `0 < n`
   2.134 +            by (auto simp: pinfreal_noteq_omega_Ex field_simps)
   2.135 +          also have "\<dots> = simple_integral ?g" using g `space M \<noteq> {}`
   2.136 +            by (subst simple_integral_indicator)
   2.137 +               (auto simp: image_constant ac_simps dest: simple_functionD)
   2.138 +          finally show "x < simple_integral ?g" .
   2.139 +        qed
   2.140 +      qed
   2.141 +      then show ?thesis by simp
   2.142 +    qed
   2.143    qed
   2.144 -qed
   2.145 +qed (auto intro!: SUP_subset simp: positive_integral_def)
   2.146  
   2.147  lemma (in measure_space) positive_integral_cong:
   2.148    assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
   2.149 @@ -1025,12 +1022,6 @@
   2.150    shows "positive_integral u \<le> positive_integral v"
   2.151    using mono by (auto intro!: AE_cong positive_integral_mono_AE)
   2.152  
   2.153 -lemma image_set_cong:
   2.154 -  assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
   2.155 -  assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x"
   2.156 -  shows "f ` A = g ` B"
   2.157 -  using assms by blast
   2.158 -
   2.159  lemma (in measure_space) positive_integral_vimage:
   2.160    fixes g :: "'a \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a"
   2.161    assumes f: "bij_betw f S (space M)"
   2.162 @@ -1229,6 +1220,7 @@
   2.163        using assms by (simp cong: measurable_cong)
   2.164      moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
   2.165        unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
   2.166 +      using SUP_const[OF UNIV_not_empty]
   2.167        by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
   2.168      ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
   2.169        unfolding positive_integral_def[of ru]
     3.1 --- a/src/HOL/Probability/Positive_Infinite_Real.thy	Wed Dec 01 21:03:02 2010 +0100
     3.2 +++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Thu Dec 02 14:34:58 2010 +0100
     3.3 @@ -6,57 +6,6 @@
     3.4    imports Complex_Main Nat_Bijection Multivariate_Analysis
     3.5  begin
     3.6  
     3.7 -lemma (in complete_lattice) SUPR_upper:
     3.8 -  "x \<in> A \<Longrightarrow> f x \<le> SUPR A f"
     3.9 -  unfolding SUPR_def apply(rule Sup_upper) by auto
    3.10 -
    3.11 -lemma (in complete_lattice) SUPR_subset:
    3.12 -  assumes "A \<subseteq> B" shows "SUPR A f \<le> SUPR B f"
    3.13 -  apply(rule SUP_leI) apply(rule SUPR_upper) using assms by auto
    3.14 -
    3.15 -lemma (in complete_lattice) SUPR_mono:
    3.16 -  assumes "\<forall>a\<in>A. \<exists>b\<in>B. f b \<ge> f a"
    3.17 -  shows "SUPR A f \<le> SUPR B f"
    3.18 -  unfolding SUPR_def apply(rule Sup_mono)
    3.19 -  using assms by auto
    3.20 -
    3.21 -lemma (in complete_lattice) SUP_pair:
    3.22 -  "(SUP i:A. SUP j:B. f i j) = (SUP p:A\<times>B. (\<lambda> (i, j). f i j) p)" (is "?l = ?r")
    3.23 -proof (intro antisym SUP_leI)
    3.24 -  fix i j assume "i \<in> A" "j \<in> B"
    3.25 -  then have "(case (i,j) of (i,j) \<Rightarrow> f i j) \<le> ?r"
    3.26 -    by (intro SUPR_upper) auto
    3.27 -  then show "f i j \<le> ?r" by auto
    3.28 -next
    3.29 -  fix p assume "p \<in> A \<times> B"
    3.30 -  then obtain i j where "p = (i,j)" "i \<in> A" "j \<in> B" by auto
    3.31 -  have "f i j \<le> (SUP j:B. f i j)" using `j \<in> B` by (intro SUPR_upper)
    3.32 -  also have "(SUP j:B. f i j) \<le> ?l" using `i \<in> A` by (intro SUPR_upper)
    3.33 -  finally show "(case p of (i, j) \<Rightarrow> f i j) \<le> ?l" using `p = (i,j)` by simp
    3.34 -qed
    3.35 -
    3.36 -lemma (in complete_lattice) SUP_surj_compose:
    3.37 -  assumes *: "f`A = B" shows "SUPR A (g \<circ> f) = SUPR B g"
    3.38 -  unfolding SUPR_def unfolding *[symmetric]
    3.39 -  by (simp add: image_compose)
    3.40 -
    3.41 -lemma (in complete_lattice) SUP_swap:
    3.42 -  "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
    3.43 -proof -
    3.44 -  have *: "(\<lambda>(i,j). (j,i)) ` (B \<times> A) = A \<times> B" by auto
    3.45 -  show ?thesis
    3.46 -    unfolding SUP_pair SUP_surj_compose[symmetric, OF *]
    3.47 -    by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def)
    3.48 -qed
    3.49 -
    3.50 -lemma range_const[simp]: "range (\<lambda>x. c) = {c}" by auto
    3.51 -
    3.52 -lemma (in complete_lattice) SUPR_const[simp]: "(SUP i. c) = c"
    3.53 -  unfolding SUPR_def by simp
    3.54 -
    3.55 -lemma (in complete_lattice) INFI_const[simp]: "(INF i. c) = c"
    3.56 -  unfolding INFI_def by simp
    3.57 -
    3.58  lemma (in complete_lattice) Sup_start:
    3.59    assumes *: "\<And>x. f x \<le> f 0"
    3.60    shows "(SUP n. f n) = f 0"
    3.61 @@ -137,6 +86,26 @@
    3.62    ultimately show ?thesis by simp
    3.63  qed
    3.64  
    3.65 +lemma (in complete_lattice) lim_INF_le_lim_SUP:
    3.66 +  fixes f :: "nat \<Rightarrow> 'a"
    3.67 +  shows "(SUP n. INF m. f (n + m)) \<le> (INF n. SUP m. f (n + m))"
    3.68 +proof (rule SUP_leI, rule le_INFI)
    3.69 +  fix i j show "(INF m. f (i + m)) \<le> (SUP m. f (j + m))"
    3.70 +  proof (cases rule: le_cases)
    3.71 +    assume "i \<le> j"
    3.72 +    have "(INF m. f (i + m)) \<le> f (i + (j - i))" by (rule INF_leI) simp
    3.73 +    also have "\<dots> = f (j + 0)" using `i \<le> j` by auto
    3.74 +    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
    3.75 +    finally show ?thesis .
    3.76 +  next
    3.77 +    assume "j \<le> i"
    3.78 +    have "(INF m. f (i + m)) \<le> f (i + 0)" by (rule INF_leI) simp
    3.79 +    also have "\<dots> = f (j + (i - j))" using `j \<le> i` by auto
    3.80 +    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
    3.81 +    finally show ?thesis .
    3.82 +  qed
    3.83 +qed
    3.84 +
    3.85  text {*
    3.86  
    3.87  We introduce the the positive real numbers as needed for measure theory.
    3.88 @@ -882,11 +851,6 @@
    3.89    qed simp
    3.90  qed simp
    3.91  
    3.92 -lemma less_SUP_iff:
    3.93 -  fixes a :: "'a::{complete_lattice,linorder}"
    3.94 -  shows "(a < (SUP i:A. f i)) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
    3.95 -  unfolding SUPR_def less_Sup_iff by auto
    3.96 -
    3.97  lemma SUP_\<omega>: "(SUP i:A. f i) = \<omega> \<longleftrightarrow> (\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)"
    3.98  proof
    3.99    assume *: "(SUP i:A. f i) = \<omega>"
   3.100 @@ -1320,7 +1284,6 @@
   3.101    have [intro, simp]: "\<And>A. inj_on f A" using `bij f` unfolding bij_def by (auto intro: subset_inj_on)
   3.102    have f[intro, simp]: "\<And>x. f (inv f x) = x"
   3.103      using `bij f` unfolding bij_def by (auto intro: surj_f_inv_f)
   3.104 -
   3.105    show ?thesis
   3.106    proof (rule psuminf_equality)
   3.107      fix n
   3.108 @@ -1345,49 +1308,6 @@
   3.109    qed
   3.110  qed
   3.111  
   3.112 -lemma psuminf_2dimen:
   3.113 -  fixes f:: "nat * nat \<Rightarrow> pinfreal"
   3.114 -  assumes fsums: "\<And>m. g m = (\<Sum>\<^isub>\<infinity> n. f (m,n))"
   3.115 -  shows "psuminf (f \<circ> prod_decode) = psuminf g"
   3.116 -proof (rule psuminf_equality)
   3.117 -  fix n :: nat
   3.118 -  let ?P = "prod_decode ` {..<n}"
   3.119 -  have "setsum (f \<circ> prod_decode) {..<n} = setsum f ?P"
   3.120 -    by (auto simp: setsum_reindex inj_prod_decode)
   3.121 -  also have "\<dots> \<le> setsum f ({..Max (fst ` ?P)} \<times> {..Max (snd ` ?P)})"
   3.122 -  proof (safe intro!: setsum_mono3 Max_ge image_eqI)
   3.123 -    fix a b x assume "(a, b) = prod_decode x"
   3.124 -    from this[symmetric] show "a = fst (prod_decode x)" "b = snd (prod_decode x)"
   3.125 -      by simp_all
   3.126 -  qed simp_all
   3.127 -  also have "\<dots> = (\<Sum>m\<le>Max (fst ` ?P). (\<Sum>n\<le>Max (snd ` ?P). f (m,n)))"
   3.128 -    unfolding setsum_cartesian_product by simp
   3.129 -  also have "\<dots> \<le> (\<Sum>m\<le>Max (fst ` ?P). g m)"
   3.130 -    by (auto intro!: setsum_mono psuminf_upper simp del: setsum_lessThan_Suc
   3.131 -        simp: fsums lessThan_Suc_atMost[symmetric])
   3.132 -  also have "\<dots> \<le> psuminf g"
   3.133 -    by (auto intro!: psuminf_upper simp del: setsum_lessThan_Suc
   3.134 -        simp: lessThan_Suc_atMost[symmetric])
   3.135 -  finally show "setsum (f \<circ> prod_decode) {..<n} \<le> psuminf g" .
   3.136 -next
   3.137 -  fix y assume *: "\<And>n. setsum (f \<circ> prod_decode) {..<n} \<le> y"
   3.138 -  have g: "g = (\<lambda>m. \<Sum>\<^isub>\<infinity> n. f (m,n))" unfolding fsums[symmetric] ..
   3.139 -  show "psuminf g \<le> y" unfolding g
   3.140 -  proof (rule psuminf_bound, unfold setsum_pinfsum[symmetric], safe intro!: psuminf_bound)
   3.141 -    fix N M :: nat
   3.142 -    let ?P = "{..<N} \<times> {..<M}"
   3.143 -    let ?M = "Max (prod_encode ` ?P)"
   3.144 -    have "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> (\<Sum>(m, n)\<in>?P. f (m, n))"
   3.145 -      unfolding setsum_commute[of _ _ "{..<M}"] unfolding setsum_cartesian_product ..
   3.146 -    also have "\<dots> \<le> (\<Sum>(m,n)\<in>(prod_decode ` {..?M}). f (m, n))"
   3.147 -      by (auto intro!: setsum_mono3 image_eqI[where f=prod_decode, OF prod_encode_inverse[symmetric]])
   3.148 -    also have "\<dots> \<le> y" using *[of "Suc ?M"]
   3.149 -      by (simp add: lessThan_Suc_atMost[symmetric] setsum_reindex
   3.150 -               inj_prod_decode del: setsum_lessThan_Suc)
   3.151 -    finally show "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> y" .
   3.152 -  qed
   3.153 -qed
   3.154 -
   3.155  lemma pinfreal_mult_less_right:
   3.156    assumes "b * a < c * a" "0 < a" "a < \<omega>"
   3.157    shows "b < c"
   3.158 @@ -1474,7 +1394,7 @@
   3.159    show ?thesis
   3.160      unfolding psuminf_def
   3.161      unfolding *
   3.162 -    apply (subst SUP_swap) ..
   3.163 +    apply (subst SUP_commute) ..
   3.164  qed
   3.165  
   3.166  lemma psuminf_commute:
   3.167 @@ -1484,7 +1404,7 @@
   3.168      apply (subst SUPR_pinfreal_setsum)
   3.169      by auto
   3.170    also have "\<dots> = (SUP m n. \<Sum> j < m. \<Sum> i < n. f i j)"
   3.171 -    apply (subst SUP_swap)
   3.172 +    apply (subst SUP_commute)
   3.173      apply (subst setsum_commute)
   3.174      by auto
   3.175    also have "\<dots> = (SUP m. \<Sum> j < m. SUP n. \<Sum> i < n. f i j)"
   3.176 @@ -1494,6 +1414,49 @@
   3.177      unfolding psuminf_def by auto
   3.178  qed
   3.179  
   3.180 +lemma psuminf_2dimen:
   3.181 +  fixes f:: "nat * nat \<Rightarrow> pinfreal"
   3.182 +  assumes fsums: "\<And>m. g m = (\<Sum>\<^isub>\<infinity> n. f (m,n))"
   3.183 +  shows "psuminf (f \<circ> prod_decode) = psuminf g"
   3.184 +proof (rule psuminf_equality)
   3.185 +  fix n :: nat
   3.186 +  let ?P = "prod_decode ` {..<n}"
   3.187 +  have "setsum (f \<circ> prod_decode) {..<n} = setsum f ?P"
   3.188 +    by (auto simp: setsum_reindex inj_prod_decode)
   3.189 +  also have "\<dots> \<le> setsum f ({..Max (fst ` ?P)} \<times> {..Max (snd ` ?P)})"
   3.190 +  proof (safe intro!: setsum_mono3 Max_ge image_eqI)
   3.191 +    fix a b x assume "(a, b) = prod_decode x"
   3.192 +    from this[symmetric] show "a = fst (prod_decode x)" "b = snd (prod_decode x)"
   3.193 +      by simp_all
   3.194 +  qed simp_all
   3.195 +  also have "\<dots> = (\<Sum>m\<le>Max (fst ` ?P). (\<Sum>n\<le>Max (snd ` ?P). f (m,n)))"
   3.196 +    unfolding setsum_cartesian_product by simp
   3.197 +  also have "\<dots> \<le> (\<Sum>m\<le>Max (fst ` ?P). g m)"
   3.198 +    by (auto intro!: setsum_mono psuminf_upper simp del: setsum_lessThan_Suc
   3.199 +        simp: fsums lessThan_Suc_atMost[symmetric])
   3.200 +  also have "\<dots> \<le> psuminf g"
   3.201 +    by (auto intro!: psuminf_upper simp del: setsum_lessThan_Suc
   3.202 +        simp: lessThan_Suc_atMost[symmetric])
   3.203 +  finally show "setsum (f \<circ> prod_decode) {..<n} \<le> psuminf g" .
   3.204 +next
   3.205 +  fix y assume *: "\<And>n. setsum (f \<circ> prod_decode) {..<n} \<le> y"
   3.206 +  have g: "g = (\<lambda>m. \<Sum>\<^isub>\<infinity> n. f (m,n))" unfolding fsums[symmetric] ..
   3.207 +  show "psuminf g \<le> y" unfolding g
   3.208 +  proof (rule psuminf_bound, unfold setsum_pinfsum[symmetric], safe intro!: psuminf_bound)
   3.209 +    fix N M :: nat
   3.210 +    let ?P = "{..<N} \<times> {..<M}"
   3.211 +    let ?M = "Max (prod_encode ` ?P)"
   3.212 +    have "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> (\<Sum>(m, n)\<in>?P. f (m, n))"
   3.213 +      unfolding setsum_commute[of _ _ "{..<M}"] unfolding setsum_cartesian_product ..
   3.214 +    also have "\<dots> \<le> (\<Sum>(m,n)\<in>(prod_decode ` {..?M}). f (m, n))"
   3.215 +      by (auto intro!: setsum_mono3 image_eqI[where f=prod_decode, OF prod_encode_inverse[symmetric]])
   3.216 +    also have "\<dots> \<le> y" using *[of "Suc ?M"]
   3.217 +      by (simp add: lessThan_Suc_atMost[symmetric] setsum_reindex
   3.218 +               inj_prod_decode del: setsum_lessThan_Suc)
   3.219 +    finally show "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> y" .
   3.220 +  qed
   3.221 +qed
   3.222 +
   3.223  lemma Real_max:
   3.224    assumes "x \<ge> 0" "y \<ge> 0"
   3.225    shows "Real (max x y) = max (Real x) (Real y)"
   3.226 @@ -2462,26 +2425,6 @@
   3.227    shows "a \<le> a - b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a \<noteq> \<omega> \<Longrightarrow> b = 0"
   3.228    by (cases a, cases b, auto split: split_if_asm)
   3.229  
   3.230 -lemma lim_INF_le_lim_SUP:
   3.231 -  fixes f :: "nat \<Rightarrow> pinfreal"
   3.232 -  shows "(SUP n. INF m. f (n + m)) \<le> (INF n. SUP m. f (n + m))"
   3.233 -proof (rule complete_lattice_class.SUP_leI, rule complete_lattice_class.le_INFI)
   3.234 -  fix i j show "(INF m. f (i + m)) \<le> (SUP m. f (j + m))"
   3.235 -  proof (cases rule: le_cases)
   3.236 -    assume "i \<le> j"
   3.237 -    have "(INF m. f (i + m)) \<le> f (i + (j - i))" by (rule INF_leI) simp
   3.238 -    also have "\<dots> = f (j + 0)" using `i \<le> j` by auto
   3.239 -    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
   3.240 -    finally show ?thesis .
   3.241 -  next
   3.242 -    assume "j \<le> i"
   3.243 -    have "(INF m. f (i + m)) \<le> f (i + 0)" by (rule INF_leI) simp
   3.244 -    also have "\<dots> = f (j + (i - j))" using `j \<le> i` by auto
   3.245 -    also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
   3.246 -    finally show ?thesis .
   3.247 -  qed
   3.248 -qed
   3.249 -
   3.250  lemma lim_INF_eq_lim_SUP:
   3.251    fixes X :: "nat \<Rightarrow> real"
   3.252    assumes "\<And>i. 0 \<le> X i" and "0 \<le> x"
     4.1 --- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 01 21:03:02 2010 +0100
     4.2 +++ b/src/HOL/Probability/Product_Measure.thy	Thu Dec 02 14:34:58 2010 +0100
     4.3 @@ -865,7 +865,7 @@
     4.4  
     4.5  lemma (in finite_product_sigma_algebra) P_empty:
     4.6    "I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
     4.7 -  unfolding product_algebra_def by (simp add: sigma_def)
     4.8 +  unfolding product_algebra_def by (simp add: sigma_def image_constant)
     4.9  
    4.10  lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
    4.11    "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
    4.12 @@ -1258,7 +1258,7 @@
    4.13      by (auto intro!: exI[of _ "\<lambda>A. if A = {} then 0 else 1"] sigma_algebra_sigma
    4.14                       sigma_algebra.finite_additivity_sufficient
    4.15               simp add: positive_def additive_def sets_sigma sigma_finite_measure_def
    4.16 -                       sigma_finite_measure_axioms_def)
    4.17 +                       sigma_finite_measure_axioms_def image_constant)
    4.18  next
    4.19    case (insert i I)
    4.20    interpret finite_product_sigma_finite M \<mu> I by default fact
     5.1 --- a/src/HOL/Set.thy	Wed Dec 01 21:03:02 2010 +0100
     5.2 +++ b/src/HOL/Set.thy	Thu Dec 02 14:34:58 2010 +0100
     5.3 @@ -882,7 +882,6 @@
     5.4  lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
     5.5    by blast
     5.6  
     5.7 -
     5.8  subsubsection {* Some rules with @{text "if"} *}
     5.9  
    5.10  text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}