moved generic lemmas in Probability to HOL
authorhoelzl
Tue Aug 24 14:41:37 2010 +0200 (2010-08-24)
changeset 38705aaee86c0e237
parent 38656 d5d342611edb
child 38706 622a620a6474
moved generic lemmas in Probability to HOL
src/HOL/Complete_Lattice.thy
src/HOL/Orderings.thy
src/HOL/Probability/Borel.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Positive_Infinite_Real.thy
src/HOL/Probability/Product_Measure.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Aug 23 19:35:57 2010 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Tue Aug 24 14:41:37 2010 +0200
     1.3 @@ -88,6 +88,26 @@
     1.4  lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     1.5    by (auto intro: Inf_greatest dest: Inf_lower)
     1.6  
     1.7 +lemma Sup_mono:
     1.8 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
     1.9 +  shows "Sup A \<le> Sup B"
    1.10 +proof (rule Sup_least)
    1.11 +  fix a assume "a \<in> A"
    1.12 +  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
    1.13 +  from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
    1.14 +  with `a \<le> b` show "a \<le> Sup B" by auto
    1.15 +qed
    1.16 +
    1.17 +lemma Inf_mono:
    1.18 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
    1.19 +  shows "Inf A \<le> Inf B"
    1.20 +proof (rule Inf_greatest)
    1.21 +  fix b assume "b \<in> B"
    1.22 +  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
    1.23 +  from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
    1.24 +  with `a \<le> b` show "Inf A \<le> b" by auto
    1.25 +qed
    1.26 +
    1.27  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.28    "SUPR A f = \<Squnion> (f ` A)"
    1.29  
    1.30 @@ -144,8 +164,25 @@
    1.31  lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
    1.32    by (auto intro: antisym INF_leI le_INFI)
    1.33  
    1.34 +lemma SUP_mono:
    1.35 +  "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
    1.36 +  by (force intro!: Sup_mono simp: SUPR_def)
    1.37 +
    1.38 +lemma INF_mono:
    1.39 +  "(\<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.40 +  by (force intro!: Inf_mono simp: INFI_def)
    1.41 +
    1.42  end
    1.43  
    1.44 +lemma less_Sup_iff:
    1.45 +  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.46 +  shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
    1.47 +  unfolding not_le[symmetric] Sup_le_iff by auto
    1.48 +
    1.49 +lemma Inf_less_iff:
    1.50 +  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    1.51 +  shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
    1.52 +  unfolding not_le[symmetric] le_Inf_iff by auto
    1.53  
    1.54  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    1.55  
    1.56 @@ -204,6 +241,18 @@
    1.57  
    1.58  end
    1.59  
    1.60 +lemma SUPR_fun_expand:
    1.61 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
    1.62 +  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
    1.63 +  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
    1.64 +           simp: SUPR_def Sup_fun_def)
    1.65 +
    1.66 +lemma INFI_fun_expand:
    1.67 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
    1.68 +  shows "(INF y:A. f y) x = (INF y:A. f y x)"
    1.69 +  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
    1.70 +           simp: INFI_def Inf_fun_def)
    1.71 +
    1.72  lemma Inf_empty_fun:
    1.73    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
    1.74    by (simp add: Inf_fun_def)
     2.1 --- a/src/HOL/Orderings.thy	Mon Aug 23 19:35:57 2010 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Tue Aug 24 14:41:37 2010 +0200
     2.3 @@ -1154,7 +1154,7 @@
     2.4        have "\<And>y. P y \<Longrightarrow> x \<le> y"
     2.5        proof (rule classical)
     2.6          fix y
     2.7 -        assume "P y" and "\<not> x \<le> y" 
     2.8 +        assume "P y" and "\<not> x \<le> y"
     2.9          with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    2.10            by (auto simp add: not_le)
    2.11          with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
    2.12 @@ -1181,13 +1181,25 @@
    2.13    "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
    2.14    by (blast intro: LeastI_ex)
    2.15  
    2.16 +lemma LeastI2_wellorder:
    2.17 +  assumes "P a"
    2.18 +  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
    2.19 +  shows "Q (Least P)"
    2.20 +proof (rule LeastI2_order)
    2.21 +  show "P (Least P)" using `P a` by (rule LeastI)
    2.22 +next
    2.23 +  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
    2.24 +next
    2.25 +  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
    2.26 +qed
    2.27 +
    2.28  lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
    2.29  apply (simp (no_asm_use) add: not_le [symmetric])
    2.30  apply (erule contrapos_nn)
    2.31  apply (erule Least_le)
    2.32  done
    2.33  
    2.34 -end  
    2.35 +end
    2.36  
    2.37  
    2.38  subsection {* Order on bool *}
     3.1 --- a/src/HOL/Probability/Borel.thy	Mon Aug 23 19:35:57 2010 +0200
     3.2 +++ b/src/HOL/Probability/Borel.thy	Tue Aug 24 14:41:37 2010 +0200
     3.3 @@ -1238,7 +1238,7 @@
     3.4  proof safe
     3.5    fix a
     3.6    have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
     3.7 -    by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
     3.8 +    by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal])
     3.9    then show "{x\<in>space M. a < ?sup x} \<in> sets M"
    3.10      using assms by auto
    3.11  qed
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Aug 23 19:35:57 2010 +0200
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Aug 24 14:41:37 2010 +0200
     4.3 @@ -57,7 +57,7 @@
     4.4    shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
     4.5    (is "?l = ?r")
     4.6  proof -
     4.7 -  have "?r = (\<Sum>y \<in> f ` space M. 
     4.8 +  have "?r = (\<Sum>y \<in> f ` space M.
     4.9      (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
    4.10      by (auto intro!: setsum_cong2)
    4.11    also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
    4.12 @@ -222,19 +222,6 @@
    4.13      by (simp add: if_distrib setsum_cases[OF `finite P`])
    4.14  qed
    4.15  
    4.16 -lemma LeastI2_wellorder:
    4.17 -  fixes a :: "_ :: wellorder"
    4.18 -  assumes "P a"
    4.19 -  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
    4.20 -  shows "Q (Least P)"
    4.21 -proof (rule LeastI2_order)
    4.22 -  show "P (Least P)" using `P a` by (rule LeastI)
    4.23 -next
    4.24 -  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
    4.25 -next
    4.26 -  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
    4.27 -qed
    4.28 -
    4.29  lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
    4.30    fixes u :: "'a \<Rightarrow> pinfreal"
    4.31    assumes u: "u \<in> borel_measurable M"
    4.32 @@ -399,7 +386,8 @@
    4.33            let ?N = "max n (natfloor r + 1)"
    4.34            have "u t < of_nat ?N" "n \<le> ?N"
    4.35              using ge_natfloor_plus_one_imp_gt[of r n] preal
    4.36 -            by (auto simp: max_def real_Suc_natfloor)
    4.37 +            using real_natfloor_add_one_gt
    4.38 +            by (auto simp: max_def real_of_nat_Suc)
    4.39            from lower[OF this(1)]
    4.40            have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
    4.41              using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
    4.42 @@ -875,7 +863,7 @@
    4.43    moreover
    4.44    have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
    4.45      unfolding pinfreal_SUP_cmult[symmetric]
    4.46 -  proof (safe intro!: SUP_mono)
    4.47 +  proof (safe intro!: SUP_mono bexI)
    4.48      fix i
    4.49      have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
    4.50        using B `simple_function u`
    4.51 @@ -890,7 +878,7 @@
    4.52      qed
    4.53      finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
    4.54        by auto
    4.55 -  qed
    4.56 +  qed simp
    4.57    ultimately show "a * simple_integral u \<le> ?S" by simp
    4.58  qed
    4.59  
    4.60 @@ -1056,16 +1044,17 @@
    4.61      by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
    4.62  
    4.63    have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
    4.64 -  proof (unfold isoton_def, safe)
    4.65 -    fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
    4.66 -      by (rule INF_mono[where N=Suc]) simp
    4.67 -  qed
    4.68 +  proof (unfold isoton_def, safe intro!: INF_mono bexI)
    4.69 +    fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
    4.70 +  qed simp
    4.71    from positive_integral_isoton[OF this] assms
    4.72    have "positive_integral (SUP n. INF m. u (m + n)) =
    4.73      (SUP n. positive_integral (INF m. u (m + n)))"
    4.74      unfolding isoton_def by (simp add: borel_measurable_INF)
    4.75    also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
    4.76 -    by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
    4.77 +    apply (rule SUP_mono)
    4.78 +    apply (rule_tac x=n in bexI)
    4.79 +    by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
    4.80    finally show ?thesis .
    4.81  qed
    4.82  
    4.83 @@ -1123,10 +1112,10 @@
    4.84    have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
    4.85      unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
    4.86    also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
    4.87 -  proof (rule SUP_mono, rule positive_integral_mono)
    4.88 +  proof (rule SUP_mono, rule bexI, rule positive_integral_mono)
    4.89      fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
    4.90        by (cases "x \<in> N") auto
    4.91 -  qed
    4.92 +  qed simp
    4.93    also have "\<dots> = 0"
    4.94      using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
    4.95    finally show ?thesis by simp
    4.96 @@ -1967,46 +1956,37 @@
    4.97    unfolding finite_measure_space_def finite_measure_space_axioms_def
    4.98    using assms by simp
    4.99  
   4.100 -lemma (in finite_measure_space) borel_measurable_finite[intro, simp]:
   4.101 -  fixes f :: "'a \<Rightarrow> real"
   4.102 -  shows "f \<in> borel_measurable M"
   4.103 +lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
   4.104    unfolding measurable_def sets_eq_Pow by auto
   4.105  
   4.106 +lemma (in finite_measure_space) simple_function_finite: "simple_function f"
   4.107 +  unfolding simple_function_def sets_eq_Pow using finite_space by auto
   4.108 +
   4.109 +lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
   4.110 +  "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
   4.111 +proof -
   4.112 +  have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
   4.113 +    by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
   4.114 +  show ?thesis unfolding * using borel_measurable_finite[of f]
   4.115 +    by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
   4.116 +qed
   4.117 +
   4.118  lemma (in finite_measure_space) integral_finite_singleton:
   4.119    shows "integrable f"
   4.120    and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
   4.121  proof -
   4.122 -  have 1: "f \<in> borel_measurable M"
   4.123 -    unfolding measurable_def sets_eq_Pow by auto
   4.124 -
   4.125 -  have 2: "finite (f`space M)" using finite_space by simp
   4.126 -
   4.127 -  have 3: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
   4.128 -    using finite_measure[unfolded sets_eq_Pow] by simp
   4.129 -
   4.130 -  show "integrable f"
   4.131 -    by (rule integral_on_finite(1)[OF 1 2 3]) simp
   4.132 +  have [simp]:
   4.133 +    "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
   4.134 +    "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
   4.135 +    unfolding positive_integral_finite_eq_setsum by auto
   4.136  
   4.137 -  { fix r let ?x = "f -` {r} \<inter> space M"
   4.138 -    have "?x \<subseteq> space M" by auto
   4.139 -    with finite_space sets_eq_Pow finite_single_measure
   4.140 -    have "real (\<mu> ?x) = (\<Sum>i \<in> ?x. real (\<mu> {i}))"
   4.141 -      using real_measure_setsum_singleton[of ?x] by auto }
   4.142 -  note measure_eq_setsum = this
   4.143 +  show "integrable f" using finite_space finite_measure
   4.144 +    by (simp add: setsum_\<omega> integrable_def sets_eq_Pow)
   4.145  
   4.146 -  have "integral f = (\<Sum>r\<in>f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))"
   4.147 -    by (rule integral_on_finite(2)[OF 1 2 3]) simp
   4.148 -  also have "\<dots> = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))"
   4.149 -    unfolding measure_eq_setsum setsum_right_distrib
   4.150 -    apply (subst setsum_Sigma)
   4.151 -    apply (simp add: finite_space)
   4.152 -    apply (simp add: finite_space)
   4.153 -  proof (rule setsum_reindex_cong[symmetric])
   4.154 -    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
   4.155 -    thus "(\<lambda>(x, y). x * real (\<mu> {y})) a = f (snd a) * real (\<mu> {snd a})"
   4.156 -      by auto
   4.157 -  qed (auto intro!: image_eqI inj_onI)
   4.158 -  finally show ?I .
   4.159 +  show ?I using finite_measure
   4.160 +    apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric]
   4.161 +      real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric])
   4.162 +    by (rule setsum_cong) (simp_all split: split_if)
   4.163  qed
   4.164  
   4.165  end
     5.1 --- a/src/HOL/Probability/Positive_Infinite_Real.thy	Mon Aug 23 19:35:57 2010 +0200
     5.2 +++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Tue Aug 24 14:41:37 2010 +0200
     5.3 @@ -6,53 +6,20 @@
     5.4    imports Complex_Main Nat_Bijection Multivariate_Analysis
     5.5  begin
     5.6  
     5.7 -lemma less_Sup_iff:
     5.8 -  fixes a :: "'x\<Colon>{complete_lattice,linorder}"
     5.9 -  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
    5.10 -  unfolding not_le[symmetric] Sup_le_iff by auto
    5.11 -
    5.12 -lemma Inf_less_iff:
    5.13 -  fixes a :: "'x\<Colon>{complete_lattice,linorder}"
    5.14 -  shows "Inf S < a \<longleftrightarrow> (\<exists> x \<in> S. x < a)"
    5.15 -  unfolding not_le[symmetric] le_Inf_iff by auto
    5.16 -
    5.17 -lemma SUPR_fun_expand: "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
    5.18 -  unfolding SUPR_def expand_fun_eq Sup_fun_def
    5.19 -  by (auto intro!: arg_cong[where f=Sup])
    5.20 -
    5.21 -lemma real_Suc_natfloor: "r < real (Suc (natfloor r))"
    5.22 -proof cases
    5.23 -  assume "0 \<le> r"
    5.24 -  from floor_correct[of r]
    5.25 -  have "r < real (\<lfloor>r\<rfloor> + 1)" by auto
    5.26 -  also have "\<dots> = real (Suc (natfloor r))"
    5.27 -    using `0 \<le> r` by (auto simp: real_of_nat_Suc natfloor_def)
    5.28 -  finally show ?thesis .
    5.29 -next
    5.30 -  assume "\<not> 0 \<le> r"
    5.31 -  hence "r < 0" by auto
    5.32 -  also have "0 < real (Suc (natfloor r))" by auto
    5.33 -  finally show ?thesis .
    5.34 +lemma (in complete_lattice) Sup_start:
    5.35 +  assumes *: "\<And>x. f x \<le> f 0"
    5.36 +  shows "(SUP n. f n) = f 0"
    5.37 +proof (rule antisym)
    5.38 +  show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
    5.39 +  show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
    5.40  qed
    5.41  
    5.42 -lemma (in complete_lattice) Sup_mono:
    5.43 -  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
    5.44 -  shows "Sup A \<le> Sup B"
    5.45 -proof (rule Sup_least)
    5.46 -  fix a assume "a \<in> A"
    5.47 -  with assms obtain b where "b \<in> B" and "a \<le> b" by auto
    5.48 -  hence "b \<le> Sup B" by (auto intro: Sup_upper)
    5.49 -  with `a \<le> b` show "a \<le> Sup B" by auto
    5.50 -qed
    5.51 -
    5.52 -lemma (in complete_lattice) Inf_mono:
    5.53 -  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
    5.54 -  shows "Inf A \<le> Inf B"
    5.55 -proof (rule Inf_greatest)
    5.56 -  fix b assume "b \<in> B"
    5.57 -  with assms obtain a where "a \<in> A" and "a \<le> b" by auto
    5.58 -  hence "Inf A \<le> a" by (auto intro: Inf_lower)
    5.59 -  with `a \<le> b` show "Inf A \<le> b" by auto
    5.60 +lemma (in complete_lattice) Inf_start:
    5.61 +  assumes *: "\<And>x. f 0 \<le> f x"
    5.62 +  shows "(INF n. f n) = f 0"
    5.63 +proof (rule antisym)
    5.64 +  show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
    5.65 +  show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
    5.66  qed
    5.67  
    5.68  lemma (in complete_lattice) Sup_mono_offset:
    5.69 @@ -77,12 +44,18 @@
    5.70    apply (rule Sup_mono_offset)
    5.71    by (auto intro!: order.lift_Suc_mono_le[of "op \<le>" "op <" f, OF _ *]) default
    5.72  
    5.73 -lemma (in complete_lattice) Inf_start:
    5.74 -  assumes *: "\<And>x. f 0 \<le> f x"
    5.75 -  shows "(INF n. f n) = f 0"
    5.76 +lemma (in complete_lattice) Inf_mono_offset:
    5.77 +  fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
    5.78 +  assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
    5.79 +  shows "(INF n . f (k + n)) = (INF n. f n)"
    5.80  proof (rule antisym)
    5.81 -  show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
    5.82 -  show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
    5.83 +  show "(INF n. f n) \<le> (INF n. f (k + n))"
    5.84 +    by (auto intro!: Inf_mono simp: INFI_def)
    5.85 +  { fix n :: 'b
    5.86 +    have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
    5.87 +    with * have "f (k + n) \<le> f n" by simp }
    5.88 +  thus "(INF n. f (k + n)) \<le> (INF n. f n)"
    5.89 +    by (auto intro!: Inf_mono exI simp: INFI_def)
    5.90  qed
    5.91  
    5.92  lemma (in complete_lattice) isotone_converge:
    5.93 @@ -99,28 +72,6 @@
    5.94    ultimately show ?thesis by simp
    5.95  qed
    5.96  
    5.97 -lemma (in complete_lattice) Inf_mono_offset:
    5.98 -  fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
    5.99 -  assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
   5.100 -  shows "(INF n . f (k + n)) = (INF n. f n)"
   5.101 -proof (rule antisym)
   5.102 -  show "(INF n. f n) \<le> (INF n. f (k + n))"
   5.103 -    by (auto intro!: Inf_mono simp: INFI_def)
   5.104 -  { fix n :: 'b
   5.105 -    have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
   5.106 -    with * have "f (k + n) \<le> f n" by simp }
   5.107 -  thus "(INF n. f (k + n)) \<le> (INF n. f n)"
   5.108 -    by (auto intro!: Inf_mono exI simp: INFI_def)
   5.109 -qed
   5.110 -
   5.111 -lemma (in complete_lattice) Sup_start:
   5.112 -  assumes *: "\<And>x. f x \<le> f 0"
   5.113 -  shows "(SUP n. f n) = f 0"
   5.114 -proof (rule antisym)
   5.115 -  show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
   5.116 -  show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
   5.117 -qed
   5.118 -
   5.119  lemma (in complete_lattice) antitone_converges:
   5.120    fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
   5.121    shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
   5.122 @@ -1657,15 +1608,6 @@
   5.123    "1 \<le> Real p \<longleftrightarrow> 1 \<le> p"
   5.124    by (simp_all add: one_pinfreal_def del: Real_1)
   5.125  
   5.126 -lemma SUP_mono:
   5.127 -  assumes "\<And>n. f n \<le> g (N n)"
   5.128 -  shows "(SUP n. f n) \<le> (SUP n. g n)"
   5.129 -proof (safe intro!: SUPR_bound)
   5.130 -  fix n note assms[of n]
   5.131 -  also have "g (N n) \<le> (SUP n. g n)" by (auto intro!: le_SUPI)
   5.132 -  finally show "f n \<le> (SUP n. g n)" .
   5.133 -qed
   5.134 -
   5.135  lemma isoton_Sup:
   5.136    assumes "f \<up> u"
   5.137    shows "f i \<le> u"
   5.138 @@ -2563,20 +2505,6 @@
   5.139    shows "x \<le> (INF n. f n)"
   5.140    using assms by (simp add: INFI_def le_Inf_iff)
   5.141  
   5.142 -lemma INF_mono:
   5.143 -  assumes "\<And>n. f (N n) \<le> g n"
   5.144 -  shows "(INF n. f n) \<le> (INF n. g n)"
   5.145 -proof (safe intro!: INFI_bound)
   5.146 -  fix n
   5.147 -  have "(INF n. f n) \<le> f (N n)" by (auto intro!: INF_leI)
   5.148 -  also note assms[of n]
   5.149 -  finally show "(INF n. f n) \<le> g n" .
   5.150 -qed
   5.151 -
   5.152 -lemma INFI_fun_expand: "(INF y:A. f y) = (\<lambda>x. INF y:A. f y x)"
   5.153 -  unfolding INFI_def expand_fun_eq Inf_fun_def
   5.154 -  by (auto intro!: arg_cong[where f=Inf])
   5.155 -
   5.156  lemma LIMSEQ_imp_lim_INF:
   5.157    assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
   5.158    shows "(SUP n. INF m. Real (X (n + m))) = Real x"
   5.159 @@ -2596,11 +2524,11 @@
   5.160      proof safe
   5.161        fix x y :: nat assume "x \<le> y"
   5.162        have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
   5.163 -      proof (safe intro!: INF_mono)
   5.164 +      proof (safe intro!: INF_mono bexI)
   5.165          fix m have "x + (m + y - x) = y + m"
   5.166            using `x \<le> y` by auto
   5.167          thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
   5.168 -      qed
   5.169 +      qed simp
   5.170        thus "r x \<le> r y" using r by auto
   5.171      qed
   5.172      show "\<And>n. 0 \<le> r n" by fact
   5.173 @@ -2646,7 +2574,6 @@
   5.174    qed
   5.175  qed
   5.176  
   5.177 -
   5.178  lemma real_of_pinfreal_strict_mono_iff:
   5.179    "real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
   5.180  proof (cases a)
     6.1 --- a/src/HOL/Probability/Product_Measure.thy	Mon Aug 23 19:35:57 2010 +0200
     6.2 +++ b/src/HOL/Probability/Product_Measure.thy	Tue Aug 24 14:41:37 2010 +0200
     6.3 @@ -87,22 +87,6 @@
     6.4    shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
     6.5    oops
     6.6  
     6.7 -lemma (in finite_measure_space) simple_function_finite:
     6.8 -  "simple_function f"
     6.9 -  unfolding simple_function_def sets_eq_Pow using finite_space by auto
    6.10 -
    6.11 -lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
    6.12 -  unfolding measurable_def sets_eq_Pow by auto
    6.13 -
    6.14 -lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
    6.15 -  "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
    6.16 -proof -
    6.17 -  have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
    6.18 -    by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
    6.19 -  show ?thesis unfolding * using borel_measurable_finite[of f]
    6.20 -    by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
    6.21 -qed
    6.22 -
    6.23  lemma (in finite_measure_space) finite_prod_measure_times:
    6.24    assumes "finite_measure_space N \<nu>"
    6.25    and "A1 \<in> sets M" "A2 \<in> sets N"