Equality of integral and infinite sum.
authorhoelzl
Fri Mar 12 15:35:41 2010 +0100 (2010-03-12)
changeset 357485f35613d9a65
parent 35747 c910fe606829
child 35750 41267aebfa5f
Equality of integral and infinite sum.
src/HOL/Probability/Borel.thy
src/HOL/Probability/Lebesgue.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Probability/Borel.thy	Fri Mar 12 12:02:22 2010 +0100
     1.2 +++ b/src/HOL/Probability/Borel.thy	Fri Mar 12 15:35:41 2010 +0100
     1.3 @@ -434,6 +434,14 @@
     1.4    unfolding field_divide_inverse
     1.5    by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
     1.6  
     1.7 +lemma (in measure_space) borel_measurable_vimage:
     1.8 +  assumes borel: "f \<in> borel_measurable M"
     1.9 +  shows "f -` {X} \<inter> space M \<in> sets M"
    1.10 +proof -
    1.11 +  have "{w \<in> space M. f w = X} = {w. f w = X} \<inter> space M" by auto
    1.12 +  with borel_measurable_eq_borel_measurable[OF borel borel_measurable_const, of X]
    1.13 +  show ?thesis unfolding vimage_def by simp
    1.14 +qed
    1.15  
    1.16  section "Monotone convergence"
    1.17  
     2.1 --- a/src/HOL/Probability/Lebesgue.thy	Fri Mar 12 12:02:22 2010 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue.thy	Fri Mar 12 15:35:41 2010 +0100
     2.3 @@ -673,6 +673,9 @@
     2.4    unfolding nnfis_def mono_convergent_def incseq_def
     2.5    by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
     2.6  
     2.7 +lemma nnfis_0: "0 \<in> nnfis (\<lambda> x. 0)"
     2.8 +  by (rule psfis_nnfis[OF psfis_0])
     2.9 +
    2.10  lemma nnfis_times:
    2.11    assumes "a \<in> nnfis f" and "0 \<le> z"
    2.12    shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
    2.13 @@ -836,7 +839,7 @@
    2.14  using assms
    2.15  proof -
    2.16    from assms[unfolded nnfis_def] guess u y by auto note uy = this
    2.17 -  hence "\<And> n. 0 \<le> u n x" 
    2.18 +  hence "\<And> n. 0 \<le> u n x"
    2.19      unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
    2.20      by auto
    2.21    thus "0 \<le> f x" using uy[rule_format]
    2.22 @@ -1307,6 +1310,190 @@
    2.23      by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
    2.24  qed
    2.25  
    2.26 +section "Lebesgue integration on countable spaces"
    2.27 +
    2.28 +lemma nnfis_on_countable:
    2.29 +  assumes borel: "f \<in> borel_measurable M"
    2.30 +  and bij: "bij_betw enum S (f ` space M - {0})"
    2.31 +  and enum_zero: "enum ` (-S) \<subseteq> {0}"
    2.32 +  and nn_enum: "\<And>n. 0 \<le> enum n"
    2.33 +  and sums: "(\<lambda>r. enum r * measure M (f -` {enum r} \<inter> space M)) sums x" (is "?sum sums x")
    2.34 +  shows "x \<in> nnfis f"
    2.35 +proof -
    2.36 +  have inj_enum: "inj_on enum S"
    2.37 +    and range_enum: "enum ` S = f ` space M - {0}"
    2.38 +    using bij by (auto simp: bij_betw_def)
    2.39 +
    2.40 +  let "?x n z" = "\<Sum>i = 0..<n. enum i * indicator_fn (f -` {enum i} \<inter> space M) z"
    2.41 +
    2.42 +  show ?thesis
    2.43 +  proof (rule nnfis_mon_conv)
    2.44 +    show "(\<lambda>n. \<Sum>i = 0..<n. ?sum i) ----> x" using sums unfolding sums_def .
    2.45 +  next
    2.46 +    fix n
    2.47 +    show "(\<Sum>i = 0..<n. ?sum i) \<in> nnfis (?x n)"
    2.48 +    proof (induct n)
    2.49 +      case 0 thus ?case by (simp add: nnfis_0)
    2.50 +    next
    2.51 +      case (Suc n) thus ?case using nn_enum
    2.52 +        by (auto intro!: nnfis_add nnfis_times psfis_nnfis[OF psfis_indicator] borel_measurable_vimage[OF borel])
    2.53 +    qed
    2.54 +  next
    2.55 +    show "mono_convergent ?x f (space M)"
    2.56 +    proof (rule mono_convergentI)
    2.57 +      fix x
    2.58 +      show "incseq (\<lambda>n. ?x n x)"
    2.59 +        by (rule incseq_SucI, auto simp: indicator_fn_def nn_enum)
    2.60 +
    2.61 +      have fin: "\<And>n. finite (enum ` ({0..<n} \<inter> S))" by auto
    2.62 +
    2.63 +      assume "x \<in> space M"
    2.64 +      hence "f x \<in> enum ` S \<or> f x = 0" using range_enum by auto
    2.65 +      thus "(\<lambda>n. ?x n x) ----> f x"
    2.66 +      proof (rule disjE)
    2.67 +        assume "f x \<in> enum ` S"
    2.68 +        then obtain i where "i \<in> S" and "f x = enum i" by auto
    2.69 +
    2.70 +        { fix n
    2.71 +          have sum_ranges:
    2.72 +            "i < n \<Longrightarrow> enum`({0..<n} \<inter> S) \<inter> {z. enum i = z \<and> x\<in>space M} = {enum i}"
    2.73 +            "\<not> i < n \<Longrightarrow> enum`({0..<n} \<inter> S) \<inter> {z. enum i = z \<and> x\<in>space M} = {}"
    2.74 +            using `x \<in> space M` `i \<in> S` inj_enum[THEN inj_on_iff] by auto
    2.75 +          have "?x n x =
    2.76 +            (\<Sum>i \<in> {0..<n} \<inter> S. enum i * indicator_fn (f -` {enum i} \<inter> space M) x)"
    2.77 +            using enum_zero by (auto intro!: setsum_mono_zero_cong_right)
    2.78 +          also have "... =
    2.79 +            (\<Sum>z \<in> enum`({0..<n} \<inter> S). z * indicator_fn (f -` {z} \<inter> space M) x)"
    2.80 +            using inj_enum[THEN subset_inj_on] by (auto simp: setsum_reindex)
    2.81 +          also have "... = (if i < n then f x else 0)"
    2.82 +            unfolding indicator_fn_def if_distrib[where x=1 and y=0]
    2.83 +              setsum_cases[OF fin]
    2.84 +            using sum_ranges `f x = enum i`
    2.85 +            by auto
    2.86 +          finally have "?x n x = (if i < n then f x else 0)" . }
    2.87 +        note sum_equals_if = this
    2.88 +
    2.89 +        show ?thesis unfolding sum_equals_if
    2.90 +          by (rule LIMSEQ_offset[where k="i + 1"]) (auto intro!: LIMSEQ_const)
    2.91 +      next
    2.92 +        assume "f x = 0"
    2.93 +        { fix n have "?x n x = 0"
    2.94 +            unfolding indicator_fn_def if_distrib[where x=1 and y=0]
    2.95 +              setsum_cases[OF finite_atLeastLessThan]
    2.96 +            using `f x = 0` `x \<in> space M`
    2.97 +            by (auto split: split_if) }
    2.98 +        thus ?thesis using `f x = 0` by (auto intro!: LIMSEQ_const)
    2.99 +      qed
   2.100 +    qed
   2.101 +  qed
   2.102 +qed
   2.103 +
   2.104 +lemma integral_on_countable:
   2.105 +  assumes borel: "f \<in> borel_measurable M"
   2.106 +  and bij: "bij_betw enum S (f ` space M)"
   2.107 +  and enum_zero: "enum ` (-S) \<subseteq> {0}"
   2.108 +  and abs_summable: "summable (\<lambda>r. \<bar>enum r * measure M (f -` {enum r} \<inter> space M)\<bar>)"
   2.109 +  shows "integrable f"
   2.110 +  and "integral f = (\<Sum>r. enum r * measure M (f -` {enum r} \<inter> space M))" (is "_ = suminf (?sum f enum)")
   2.111 +proof -
   2.112 +  { fix f enum
   2.113 +    assume borel: "f \<in> borel_measurable M"
   2.114 +      and bij: "bij_betw enum S (f ` space M)"
   2.115 +      and enum_zero: "enum ` (-S) \<subseteq> {0}"
   2.116 +      and abs_summable: "summable (\<lambda>r. \<bar>enum r * measure M (f -` {enum r} \<inter> space M)\<bar>)"
   2.117 +    have inj_enum: "inj_on enum S" and range_enum: "f ` space M = enum ` S"
   2.118 +      using bij unfolding bij_betw_def by auto
   2.119 +
   2.120 +    have [simp, intro]: "\<And>X. 0 \<le> measure M (f -` {X} \<inter> space M)"
   2.121 +      by (rule positive, rule borel_measurable_vimage[OF borel])
   2.122 +
   2.123 +    have "(\<Sum>r. ?sum (pos_part f) (pos_part enum) r) \<in> nnfis (pos_part f) \<and>
   2.124 +          summable (\<lambda>r. ?sum (pos_part f) (pos_part enum) r)"
   2.125 +    proof (rule conjI, rule nnfis_on_countable)
   2.126 +      have pos_f_image: "pos_part f ` space M - {0} = f ` space M \<inter> {0<..}"
   2.127 +        unfolding pos_part_def max_def by auto
   2.128 +
   2.129 +      show "bij_betw (pos_part enum) {x \<in> S. 0 < enum x} (pos_part f ` space M - {0})"
   2.130 +        unfolding bij_betw_def pos_f_image
   2.131 +        unfolding pos_part_def max_def range_enum
   2.132 +        by (auto intro!: inj_onI simp: inj_enum[THEN inj_on_eq_iff])
   2.133 +
   2.134 +      show "\<And>n. 0 \<le> pos_part enum n" unfolding pos_part_def max_def by auto
   2.135 +
   2.136 +      show "pos_part f \<in> borel_measurable M"
   2.137 +        by (rule pos_part_borel_measurable[OF borel])
   2.138 +
   2.139 +      show "pos_part enum ` (- {x \<in> S. 0 < enum x}) \<subseteq> {0}"
   2.140 +        unfolding pos_part_def max_def using enum_zero by auto
   2.141 +
   2.142 +      show "summable (\<lambda>r. ?sum (pos_part f) (pos_part enum) r)"
   2.143 +      proof (rule summable_comparison_test[OF _ abs_summable], safe intro!: exI[of _ 0])
   2.144 +        fix n :: nat
   2.145 +        have "pos_part enum n \<noteq> 0 \<Longrightarrow> (pos_part f -` {enum n} \<inter> space M) =
   2.146 +          (if 0 < enum n then (f -` {enum n} \<inter> space M) else {})"
   2.147 +          unfolding pos_part_def max_def by (auto split: split_if_asm)
   2.148 +        thus "norm (?sum (pos_part f) (pos_part enum) n) \<le> \<bar>?sum f enum n \<bar>"
   2.149 +          by (cases "pos_part enum n = 0",
   2.150 +            auto simp: pos_part_def max_def abs_mult not_le split: split_if_asm intro!: mult_nonpos_nonneg)
   2.151 +      qed
   2.152 +      thus "(\<lambda>r. ?sum (pos_part f) (pos_part enum) r) sums (\<Sum>r. ?sum (pos_part f) (pos_part enum) r)"
   2.153 +        by (rule summable_sums)
   2.154 +    qed }
   2.155 +  note pos = this
   2.156 +
   2.157 +  note pos_part = pos[OF assms(1-4)]
   2.158 +  moreover
   2.159 +  have neg_part_to_pos_part:
   2.160 +    "\<And>f :: _ \<Rightarrow> real. neg_part f = pos_part (uminus \<circ> f)"
   2.161 +    by (auto simp: pos_part_def neg_part_def min_def max_def expand_fun_eq)
   2.162 +
   2.163 +  have neg_part: "(\<Sum>r. ?sum (neg_part f) (neg_part enum) r) \<in> nnfis (neg_part f) \<and>
   2.164 +    summable (\<lambda>r. ?sum (neg_part f) (neg_part enum) r)"
   2.165 +    unfolding neg_part_to_pos_part
   2.166 +  proof (rule pos)
   2.167 +    show "uminus \<circ> f \<in> borel_measurable M" unfolding comp_def
   2.168 +      by (rule borel_measurable_uminus_borel_measurable[OF borel])
   2.169 +
   2.170 +    show "bij_betw (uminus \<circ> enum) S ((uminus \<circ> f) ` space M)"
   2.171 +      using bij unfolding bij_betw_def
   2.172 +      by (auto intro!: comp_inj_on simp: image_compose)
   2.173 +
   2.174 +    show "(uminus \<circ> enum) ` (- S) \<subseteq> {0}"
   2.175 +      using enum_zero by auto
   2.176 +
   2.177 +    have minus_image: "\<And>r. (uminus \<circ> f) -` {(uminus \<circ> enum) r} \<inter> space M = f -` {enum r} \<inter> space M"
   2.178 +      by auto
   2.179 +    show "summable (\<lambda>r. \<bar>(uminus \<circ> enum) r * measure_space.measure M ((uminus \<circ> f) -` {(uminus \<circ> enum) r} \<inter> space M)\<bar>)"
   2.180 +      unfolding minus_image using abs_summable by simp
   2.181 +  qed
   2.182 +  ultimately show "integrable f" unfolding integrable_def by auto
   2.183 +
   2.184 +  { fix r
   2.185 +    have "?sum (pos_part f) (pos_part enum) r - ?sum (neg_part f) (neg_part enum) r = ?sum f enum r"
   2.186 +    proof (cases rule: linorder_cases)
   2.187 +      assume "0 < enum r"
   2.188 +      hence "pos_part f -` {enum r} \<inter> space M = f -` {enum r} \<inter> space M"
   2.189 +        unfolding pos_part_def max_def by (auto split: split_if_asm)
   2.190 +      with `0 < enum r` show ?thesis unfolding pos_part_def neg_part_def min_def max_def expand_fun_eq
   2.191 +        by auto
   2.192 +    next
   2.193 +      assume "enum r < 0"
   2.194 +      hence "neg_part f -` {- enum r} \<inter> space M = f -` {enum r} \<inter> space M"
   2.195 +        unfolding neg_part_def min_def by (auto split: split_if_asm)
   2.196 +      with `enum r < 0` show ?thesis unfolding pos_part_def neg_part_def min_def max_def expand_fun_eq
   2.197 +        by auto
   2.198 +    qed (simp add: neg_part_def pos_part_def) }
   2.199 +  note sum_diff_eq_sum = this
   2.200 +
   2.201 +  have "(\<Sum>r. ?sum (pos_part f) (pos_part enum) r) - (\<Sum>r. ?sum (neg_part f) (neg_part enum) r)
   2.202 +    = (\<Sum>r. ?sum (pos_part f) (pos_part enum) r - ?sum (neg_part f) (neg_part enum) r)"
   2.203 +    using neg_part pos_part by (auto intro: suminf_diff)
   2.204 +  also have "... = (\<Sum>r. ?sum f enum r)" unfolding sum_diff_eq_sum ..
   2.205 +  finally show "integral f = suminf (?sum f enum)"
   2.206 +    unfolding integral_def using pos_part neg_part
   2.207 +    by (auto dest: the_nnfis)
   2.208 +qed
   2.209 +
   2.210  section "Lebesgue integration on finite space"
   2.211  
   2.212  lemma integral_finite_on_sets:
   2.213 @@ -1428,219 +1615,6 @@
   2.214      using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
   2.215  qed fact
   2.216  
   2.217 -section "Lebesgue integration on countable spaces"
   2.218 -
   2.219 -definition
   2.220 -  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
   2.221 -
   2.222 -lemma countable_space_integral_reduce:
   2.223 -  assumes "positive M (measure M)" and "f \<in> borel_measurable M"
   2.224 -  and "countable (f ` space M)"
   2.225 -  and "\<not> finite (pos_part f ` space M)"
   2.226 -  and "\<not> finite (neg_part f ` space M)"
   2.227 -  and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
   2.228 -  and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
   2.229 -  shows "integral f = p - n"
   2.230 -oops
   2.231 -
   2.232 -(*
   2.233 -val countable_space_integral_reduce = store_thm
   2.234 -  ("countable_space_integral_reduce",
   2.235 -   "\<forall>m f p n. measure_space m \<and>
   2.236 -	     positive m \<and>
   2.237 -	     f \<in> borel_measurable (space m, sets m) \<and>
   2.238 -	     countable (IMAGE f (space m)) \<and>
   2.239 -	     ~(FINITE (IMAGE (pos_part f) (space m))) \<and>
   2.240 -	     ~(FINITE (IMAGE (neg_part f) (space m))) \<and>
   2.241 -	     (\<lambda>r. r *
   2.242 -		  measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
   2.243 -		enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
   2.244 -	     (\<lambda>r. r *
   2.245 -		  measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
   2.246 -		enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
   2.247 -	     (integral m f = p - n)",
   2.248 -   RW_TAC std_ss [integral_def]
   2.249 -   ++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
   2.250 -   >> RW_TAC std_ss []
   2.251 -   ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
   2.252 -   >> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
   2.253 -       ++ MATCH_MP_TAC nnfis_mon_conv
   2.254 -       ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
   2.255 -		by (`countable (IMAGE (pos_part f) (space m))`
   2.256 -			by (MATCH_MP_TAC COUNTABLE_SUBSET
   2.257 -			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
   2.258 -			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
   2.259 -			    ++ METIS_TAC [])
   2.260 -		     ++ METIS_TAC [COUNTABLE_ALT])
   2.261 -       ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
   2.262 -       ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
   2.263 -			(pred_set$count n) then pos_part f t else 0)`
   2.264 -       ++ Q.EXISTS_TAC `(\<lambda>n.
   2.265 -         sum (0,n)
   2.266 -           ((\<lambda>r.
   2.267 -               r *
   2.268 -               measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
   2.269 -            enumerate (IMAGE (pos_part f) (space m))))`
   2.270 -       ++ ASM_SIMP_TAC std_ss []
   2.271 -       ++ CONJ_TAC
   2.272 -       >> (RW_TAC std_ss [mono_convergent_def]
   2.273 -	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
   2.274 -	   ++ RW_TAC std_ss [SEQ]
   2.275 -	   ++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
   2.276 -		by METIS_TAC [IN_IMAGE]
   2.277 -	   ++ Q.EXISTS_TAC `SUC N`
   2.278 -	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
   2.279 -	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
   2.280 -	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
   2.281 -       ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
   2.282 -	   ++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
   2.283 -      			then pos_part f t else  0)) =
   2.284 -		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
   2.285 -			indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
   2.286 -					   \<inter> (space m)) i) t)
   2.287 -		     (pred_set$count n'))`
   2.288 -		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
   2.289 -		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
   2.290 -				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
   2.291 -			++ POP_ORW
   2.292 -			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
   2.293 -			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
   2.294 -				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
   2.295 -			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
   2.296 -			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
   2.297 -				enumerate (IMAGE (pos_part f) (space m)) x' *
   2.298 -				(if enumerate (IMAGE (pos_part f) (space m)) x =
   2.299 -				enumerate (IMAGE (pos_part f) (space m)) x'
   2.300 -				then 1 else 0) else 0)) = (\<lambda>x. 0)`
   2.301 -				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
   2.302 -			++ POP_ORW
   2.303 -			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
   2.304 -		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
   2.305 -		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
   2.306 -		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
   2.307 -			REAL_SUM_IMAGE_IN_IF]
   2.308 -		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
   2.309 -			(\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
   2.310 -           		(if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
   2.311 -             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
   2.312 -			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
   2.313 -		    ++ POP_ORW
   2.314 -		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
   2.315 -	   ++ POP_ORW
   2.316 -	   ++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
   2.317 -		enumerate (IMAGE (pos_part f) (space m))) =
   2.318 -		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
   2.319 -			measure m ((\<lambda>i.
   2.320 -                PREIMAGE (pos_part f)
   2.321 -                  {enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
   2.322 -                space m) i))`
   2.323 -		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
   2.324 -	   ++ POP_ORW
   2.325 -	   ++ MATCH_MP_TAC psfis_intro
   2.326 -	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
   2.327 -	   ++ REVERSE CONJ_TAC
   2.328 -	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
   2.329 -	       ++ METIS_TAC [REAL_LE_REFL])
   2.330 -	   ++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
   2.331 -		by METIS_TAC [pos_part_neg_part_borel_measurable]
   2.332 -	   ++ REPEAT STRIP_TAC
   2.333 -	   ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
   2.334 -		{w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
   2.335 -		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
   2.336 -		    ++ DECIDE_TAC)
   2.337 -	   ++ POP_ORW
   2.338 -	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
   2.339 -	   ++ METIS_TAC [borel_measurable_const, measure_space_def])
   2.340 -   ++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
   2.341 -   ++ MATCH_MP_TAC nnfis_mon_conv
   2.342 -   ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
   2.343 -		by (`countable (IMAGE (neg_part f) (space m))`
   2.344 -			by (MATCH_MP_TAC COUNTABLE_SUBSET
   2.345 -			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
   2.346 -			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
   2.347 -			    ++ METIS_TAC [])
   2.348 -		     ++ METIS_TAC [COUNTABLE_ALT])
   2.349 -   ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
   2.350 -   ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
   2.351 -			(pred_set$count n) then neg_part f t else 0)`
   2.352 -   ++ Q.EXISTS_TAC `(\<lambda>n.
   2.353 -         sum (0,n)
   2.354 -           ((\<lambda>r.
   2.355 -               r *
   2.356 -               measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
   2.357 -            enumerate (IMAGE (neg_part f) (space m))))`
   2.358 -   ++ ASM_SIMP_TAC std_ss []
   2.359 -   ++ CONJ_TAC
   2.360 -   >> (RW_TAC std_ss [mono_convergent_def]
   2.361 -	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
   2.362 -	   ++ RW_TAC std_ss [SEQ]
   2.363 -	   ++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
   2.364 -		by METIS_TAC [IN_IMAGE]
   2.365 -	   ++ Q.EXISTS_TAC `SUC N`
   2.366 -	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
   2.367 -	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
   2.368 -	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
   2.369 -   ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
   2.370 -	   ++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
   2.371 -      			then neg_part f t else  0)) =
   2.372 -		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
   2.373 -			indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
   2.374 -					   \<inter> (space m)) i) t)
   2.375 -		     (pred_set$count n'))`
   2.376 -		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
   2.377 -		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
   2.378 -				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
   2.379 -			++ POP_ORW
   2.380 -			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
   2.381 -			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
   2.382 -				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
   2.383 -			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
   2.384 -			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
   2.385 -				enumerate (IMAGE (neg_part f) (space m)) x' *
   2.386 -				(if enumerate (IMAGE (neg_part f) (space m)) x =
   2.387 -				enumerate (IMAGE (neg_part f) (space m)) x'
   2.388 -				then 1 else 0) else 0)) = (\<lambda>x. 0)`
   2.389 -				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
   2.390 -			++ POP_ORW
   2.391 -			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
   2.392 -		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
   2.393 -		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
   2.394 -		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
   2.395 -			REAL_SUM_IMAGE_IN_IF]
   2.396 -		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
   2.397 -			(\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
   2.398 -           		(if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
   2.399 -             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
   2.400 -			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
   2.401 -		    ++ POP_ORW
   2.402 -		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
   2.403 -	   ++ POP_ORW
   2.404 -	   ++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
   2.405 -		enumerate (IMAGE (neg_part f) (space m))) =
   2.406 -		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
   2.407 -			measure m ((\<lambda>i.
   2.408 -                PREIMAGE (neg_part f)
   2.409 -                  {enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
   2.410 -                space m) i))`
   2.411 -		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
   2.412 -	   ++ POP_ORW
   2.413 -	   ++ MATCH_MP_TAC psfis_intro
   2.414 -	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
   2.415 -	   ++ REVERSE CONJ_TAC
   2.416 -	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
   2.417 -	       ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
   2.418 -	   ++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
   2.419 -		by METIS_TAC [pos_part_neg_part_borel_measurable]
   2.420 -	   ++ REPEAT STRIP_TAC
   2.421 -	   ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
   2.422 -		{w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
   2.423 -		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
   2.424 -		    ++ DECIDE_TAC)
   2.425 -	   ++ POP_ORW
   2.426 -	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
   2.427 -	   ++ METIS_TAC [borel_measurable_const, measure_space_def]);
   2.428 -*)
   2.429 +end
   2.430  
   2.431  end
   2.432 -
   2.433 -end
   2.434 \ No newline at end of file
     3.1 --- a/src/HOL/SEQ.thy	Fri Mar 12 12:02:22 2010 +0100
     3.2 +++ b/src/HOL/SEQ.thy	Fri Mar 12 15:35:41 2010 +0100
     3.3 @@ -981,6 +981,24 @@
     3.4      by (blast intro: eq_refl X)
     3.5  qed
     3.6  
     3.7 +lemma incseq_SucI:
     3.8 +  assumes "\<And>n. X n \<le> X (Suc n)"
     3.9 +  shows "incseq X" unfolding incseq_def
    3.10 +proof safe
    3.11 +  fix m n :: nat
    3.12 +  { fix d m :: nat
    3.13 +    have "X m \<le> X (m + d)"
    3.14 +    proof (induct d)
    3.15 +      case (Suc d)
    3.16 +      also have "X (m + d) \<le> X (m + Suc d)"
    3.17 +        using assms by simp
    3.18 +      finally show ?case .
    3.19 +    qed simp }
    3.20 +  note this[of m "n - m"]
    3.21 +  moreover assume "m \<le> n"
    3.22 +  ultimately show "X m \<le> X n" by simp
    3.23 +qed
    3.24 +
    3.25  lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
    3.26    by (simp add: decseq_def monoseq_def)
    3.27