merged
authorpaulson
Wed Oct 28 11:43:06 2009 +0000 (2009-10-28)
changeset 3327273a0c804840f
parent 33268 02de0317f66f
parent 33271 7be66dee1a5a
child 33273 9290fbf0a30e
merged
src/HOL/IsaMakefile
     1.1 --- a/NEWS	Wed Oct 28 00:24:38 2009 +0100
     1.2 +++ b/NEWS	Wed Oct 28 11:43:06 2009 +0000
     1.3 @@ -65,6 +65,10 @@
     1.4  of finite and infinite sets. It is shown that they form a complete
     1.5  lattice.
     1.6  
     1.7 +* New theory SupInf of the supremum and infimum operators for sets of reals.
     1.8 +
     1.9 +* New theory Probability containing a development of measure theory, eventually leading to Lebesgue integration and probability.
    1.10 +
    1.11  * Split off prime number ingredients from theory GCD
    1.12  to theory Number_Theory/Primes;
    1.13  
     2.1 --- a/src/HOL/Complex_Main.thy	Wed Oct 28 00:24:38 2009 +0100
     2.2 +++ b/src/HOL/Complex_Main.thy	Wed Oct 28 11:43:06 2009 +0000
     2.3 @@ -4,6 +4,7 @@
     2.4  imports
     2.5    Main
     2.6    Real
     2.7 +  SupInf
     2.8    Complex
     2.9    Log
    2.10    Ln
     3.1 --- a/src/HOL/IsaMakefile	Wed Oct 28 00:24:38 2009 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Wed Oct 28 11:43:06 2009 +0000
     3.3 @@ -51,6 +51,7 @@
     3.4    HOL-Nominal-Examples \
     3.5    HOL-Number_Theory \
     3.6    HOL-Old_Number_Theory \
     3.7 +  HOL-Probability \
     3.8    HOL-Prolog \
     3.9    HOL-SET_Protocol \
    3.10    HOL-SMT-Examples \
    3.11 @@ -345,6 +346,7 @@
    3.12    RealVector.thy \
    3.13    SEQ.thy \
    3.14    Series.thy \
    3.15 +  SupInf.thy \
    3.16    Taylor.thy \
    3.17    Transcendental.thy \
    3.18    Tools/float_syntax.ML \
    3.19 @@ -1067,6 +1069,18 @@
    3.20    Multivariate_Analysis/Convex_Euclidean_Space.thy
    3.21  	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
    3.22  
    3.23 +## HOL-Probability
    3.24 +
    3.25 +HOL-Probability: HOL $(LOG)/HOL-Probability.gz
    3.26 +
    3.27 +$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
    3.28 +  Probability/Probability.thy \
    3.29 +  Probability/Sigma_Algebra.thy \
    3.30 +  Probability/SeriesPlus.thy \
    3.31 +  Probability/Caratheodory.thy \
    3.32 +  Probability/Measure.thy
    3.33 +	$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
    3.34 +
    3.35  ## HOL-Nominal
    3.36  
    3.37  HOL-Nominal: HOL $(OUT)/HOL-Nominal
     4.1 --- a/src/HOL/Library/FuncSet.thy	Wed Oct 28 00:24:38 2009 +0100
     4.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Oct 28 11:43:06 2009 +0000
     4.3 @@ -101,6 +101,19 @@
     4.4  lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
     4.5  by auto
     4.6  
     4.7 +lemma prod_final:
     4.8 +  assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
     4.9 +  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
    4.10 +proof (rule Pi_I) 
    4.11 +  fix z
    4.12 +  assume z: "z \<in> A" 
    4.13 +  have "f z = (fst (f z), snd (f z))" 
    4.14 +    by simp
    4.15 +  also have "...  \<in> B z \<times> C z"
    4.16 +    by (metis SigmaI PiE o_apply 1 2 z) 
    4.17 +  finally show "f z \<in> B z \<times> C z" .
    4.18 +qed
    4.19 +
    4.20  
    4.21  subsection{*Composition With a Restricted Domain: @{term compose}*}
    4.22  
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
     5.3 @@ -1133,7 +1133,7 @@
     5.4      hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
     5.5        apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
     5.6        apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
     5.7 -  thus ?thesis unfolding convex_def cone_def by blast
     5.8 +  thus ?thesis unfolding convex_def cone_def by auto
     5.9  qed
    5.10  
    5.11  lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
    5.12 @@ -1742,17 +1742,16 @@
    5.13      using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
    5.14      using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
    5.15    hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
    5.16 -  def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
    5.17 +  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
    5.18    show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
    5.19      apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
    5.20      from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
    5.21        apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
    5.22 -    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
    5.23 +    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
    5.24      fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
    5.25    next
    5.26      fix x assume "x\<in>s" 
    5.27 -    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
    5.28 -      unfolding setle_def
    5.29 +    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
    5.30        using ab[THEN bspec[where x=x]] by auto
    5.31      thus "k + b / 2 < inner a x" using `0 < b` by auto
    5.32    qed
    5.33 @@ -1794,11 +1793,20 @@
    5.34    assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
    5.35    shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
    5.36  proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
    5.37 -  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"  using assms(3-5) by auto 
    5.38 -  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
    5.39 -  thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
    5.40 -    apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
    5.41 -    prefer 4 using assms(3-5) by blast+ qed
    5.42 +  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" 
    5.43 +    using assms(3-5) by auto 
    5.44 +  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
    5.45 +    by (force simp add: inner_diff)
    5.46 +  thus ?thesis
    5.47 +    apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
    5.48 +    apply auto
    5.49 +    apply (rule Sup[THEN isLubD2]) 
    5.50 +    prefer 4
    5.51 +    apply (rule Sup_least) 
    5.52 +     using assms(3-5) apply (auto simp add: setle_def)
    5.53 +    apply (metis COMBC_def Collect_def Collect_mem_eq) 
    5.54 +    done
    5.55 +qed
    5.56  
    5.57  subsection {* More convexity generalities. *}
    5.58  
    5.59 @@ -2571,12 +2579,17 @@
    5.60      thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
    5.61        by(auto simp add: vector_component_simps) qed
    5.62    hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
    5.63 -    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
    5.64 -  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
    5.65 -
    5.66 -subsection {* Line segments, starlike sets etc.                                         *)
    5.67 -(* Use the same overloading tricks as for intervals, so that                 *)
    5.68 -(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *}
    5.69 +    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
    5.70 +    apply force
    5.71 +    done
    5.72 +  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
    5.73 +    using `d>0` by auto 
    5.74 +qed
    5.75 +
    5.76 +subsection {* Line segments, Starlike Sets, etc.*}
    5.77 +
    5.78 +(* Use the same overloading tricks as for intervals, so that 
    5.79 +   segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
    5.80  
    5.81  definition
    5.82    midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
     6.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
     6.3 @@ -2297,242 +2297,9 @@
     6.4    ultimately show ?thesis by metis
     6.5  qed
     6.6  
     6.7 -(* Supremum and infimum of real sets *)
     6.8 -
     6.9 -
    6.10 -definition rsup:: "real set \<Rightarrow> real" where
    6.11 -  "rsup S = (SOME a. isLub UNIV S a)"
    6.12 -
    6.13 -lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))"  by (auto simp  add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
    6.14 -
    6.15 -lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
    6.16 -  shows "isLub UNIV S (rsup S)"
    6.17 -using Se b
    6.18 -unfolding rsup_def
    6.19 -apply clarify
    6.20 -apply (rule someI_ex)
    6.21 -apply (rule reals_complete)
    6.22 -by (auto simp add: isUb_def setle_def)
    6.23 -
    6.24 -lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
    6.25 -proof-
    6.26 -  from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
    6.27 -  from rsup[OF Se] Sb have "isLub UNIV S (rsup S)"  by blast
    6.28 -  then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
    6.29 -qed
    6.30 -
    6.31 -lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.32 -  shows "rsup S = Max S"
    6.33 -using fS Se
    6.34 -proof-
    6.35 -  let ?m = "Max S"
    6.36 -  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
    6.37 -  with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
    6.38 -  from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
    6.39 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
    6.40 -  moreover
    6.41 -  have "rsup S \<le> ?m" using Sm lub
    6.42 -    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    6.43 -  ultimately  show ?thesis by arith
    6.44 -qed
    6.45 -
    6.46 -lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.47 -  shows "rsup S \<in> S"
    6.48 -  using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
    6.49 -
    6.50 -lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.51 -  shows "isUb S S (rsup S)"
    6.52 -  using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
    6.53 -  unfolding isUb_def setle_def by metis
    6.54 -
    6.55 -lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.56 -  shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
    6.57 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    6.58 -
    6.59 -lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.60 -  shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    6.61 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    6.62 -
    6.63 -lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.64 -  shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
    6.65 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    6.66 -
    6.67 -lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    6.68 -  shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
    6.69 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    6.70 -
    6.71 -lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
    6.72 -  shows "rsup S = b"
    6.73 -using b S
    6.74 -unfolding setle_def rsup_alt
    6.75 -apply -
    6.76 -apply (rule some_equality)
    6.77 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
    6.78 -done
    6.79 -
    6.80 -lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
    6.81 -  apply (rule rsup_le)
    6.82 -  apply simp
    6.83 -  using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
    6.84 -
    6.85 -lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
    6.86 -  apply (rule ext)
    6.87 -  by (metis isUb_def)
    6.88 -
    6.89 -lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
    6.90 -lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
    6.91 -  shows "a \<le> rsup S \<and> rsup S \<le> b"
    6.92 -proof-
    6.93 -  from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
    6.94 -  hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    6.95 -  from Se obtain y where y: "y \<in> S" by blast
    6.96 -  from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    6.97 -    apply (erule ballE[where x=y])
    6.98 -    apply (erule ballE[where x=y])
    6.99 -    apply arith
   6.100 -    using y apply auto
   6.101 -    done
   6.102 -  with b show ?thesis by blast
   6.103 -qed
   6.104 -
   6.105 -lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
   6.106 -  unfolding abs_le_interval_iff  using rsup_bounds[of S "-a" a]
   6.107 -  by (auto simp add: setge_def setle_def)
   6.108 -
   6.109 -lemma rsup_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
   6.110 -proof-
   6.111 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   6.112 -  show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
   6.113 -    by  (auto simp add: setge_def setle_def)
   6.114 -qed
   6.115 -
   6.116 -definition rinf:: "real set \<Rightarrow> real" where
   6.117 -  "rinf S = (SOME a. isGlb UNIV S a)"
   6.118 -
   6.119 -lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))"  by (auto simp  add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
   6.120 -
   6.121 -lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
   6.122 -  shows "\<exists>(t::real). isGlb UNIV S t"
   6.123 -proof-
   6.124 -  let ?M = "uminus ` S"
   6.125 -  from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
   6.126 -    by (rule_tac x="-y" in exI, auto)
   6.127 -  from Se have Me: "\<exists>x. x \<in> ?M" by blast
   6.128 -  from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
   6.129 -  have "isGlb UNIV S (- t)" using t
   6.130 -    apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
   6.131 -    apply (erule_tac x="-y" in allE)
   6.132 -    apply auto
   6.133 -    done
   6.134 -  then show ?thesis by metis
   6.135 -qed
   6.136 -
   6.137 -lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
   6.138 -  shows "isGlb UNIV S (rinf S)"
   6.139 -using Se b
   6.140 -unfolding rinf_def
   6.141 -apply clarify
   6.142 -apply (rule someI_ex)
   6.143 -apply (rule reals_complete_Glb)
   6.144 -apply (auto simp add: isLb_def setle_def setge_def)
   6.145 -done
   6.146 -
   6.147 -lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
   6.148 -proof-
   6.149 -  from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
   6.150 -  from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)"  by blast
   6.151 -  then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
   6.152 -qed
   6.153 -
   6.154 -lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.155 -  shows "rinf S = Min S"
   6.156 -using fS Se
   6.157 -proof-
   6.158 -  let ?m = "Min S"
   6.159 -  from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
   6.160 -  with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
   6.161 -  from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
   6.162 -    by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
   6.163 -  moreover
   6.164 -  have "rinf S \<ge> ?m" using Sm glb
   6.165 -    by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
   6.166 -  ultimately  show ?thesis by arith
   6.167 -qed
   6.168 -
   6.169 -lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.170 -  shows "rinf S \<in> S"
   6.171 -  using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   6.172 -
   6.173 -lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.174 -  shows "isLb S S (rinf S)"
   6.175 -  using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
   6.176 -  unfolding isLb_def setge_def by metis
   6.177 -
   6.178 -lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.179 -  shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   6.180 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   6.181 -
   6.182 -lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.183 -  shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   6.184 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   6.185 -
   6.186 -lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.187 -  shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   6.188 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   6.189 -
   6.190 -lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   6.191 -  shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   6.192 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   6.193 -
   6.194 -lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
   6.195 -  shows "rinf S = b"
   6.196 -using b S
   6.197 -unfolding setge_def rinf_alt
   6.198 -apply -
   6.199 -apply (rule some_equality)
   6.200 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
   6.201 -done
   6.202 -
   6.203 -lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
   6.204 -  apply (rule rinf_ge)
   6.205 -  apply simp
   6.206 -  using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
   6.207 -
   6.208 -lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
   6.209 -  apply (rule ext)
   6.210 -  by (metis isLb_def)
   6.211 -
   6.212 -lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   6.213 -  shows "a \<le> rinf S \<and> rinf S \<le> b"
   6.214 -proof-
   6.215 -  from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
   6.216 -  hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   6.217 -  from Se obtain y where y: "y \<in> S" by blast
   6.218 -  from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   6.219 -    apply (erule ballE[where x=y])
   6.220 -    apply (erule ballE[where x=y])
   6.221 -    apply arith
   6.222 -    using y apply auto
   6.223 -    done
   6.224 -  with b show ?thesis by blast
   6.225 -qed
   6.226 -
   6.227 -lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
   6.228 -  unfolding abs_le_interval_iff  using rinf_bounds[of S "-a" a]
   6.229 -  by (auto simp add: setge_def setle_def)
   6.230 -
   6.231 -lemma rinf_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
   6.232 -proof-
   6.233 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   6.234 -  show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
   6.235 -    by  (auto simp add: setge_def setle_def)
   6.236 -qed
   6.237 -
   6.238 -
   6.239 -
   6.240  subsection{* Operator norm. *}
   6.241  
   6.242 -definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
   6.243 +definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
   6.244  
   6.245  lemma norm_bound_generalize:
   6.246    fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
   6.247 @@ -2578,7 +2345,7 @@
   6.248      have Se: "?S \<noteq> {}" using  norm_basis by auto
   6.249      from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
   6.250        unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
   6.251 -    {from rsup[OF Se b, unfolded onorm_def[symmetric]]
   6.252 +    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
   6.253        show "norm (f x) <= onorm f * norm x"
   6.254          apply -
   6.255          apply (rule spec[where x = x])
   6.256 @@ -2586,7 +2353,7 @@
   6.257          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   6.258      {
   6.259        show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
   6.260 -        using rsup[OF Se b, unfolded onorm_def[symmetric]]
   6.261 +        using Sup[OF Se b, unfolded onorm_def[symmetric]]
   6.262          unfolding norm_bound_generalize[OF lf, symmetric]
   6.263          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   6.264    }
   6.265 @@ -2612,7 +2379,7 @@
   6.266      by(auto intro: vector_choose_size set_ext)
   6.267    show ?thesis
   6.268      unfolding onorm_def th
   6.269 -    apply (rule rsup_unique) by (simp_all  add: setle_def)
   6.270 +    apply (rule Sup_unique) by (simp_all  add: setle_def)
   6.271  qed
   6.272  
   6.273  lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
   6.274 @@ -3055,31 +2822,6 @@
   6.275  qed
   6.276  
   6.277  (* ------------------------------------------------------------------------- *)
   6.278 -(* Relate max and min to sup and inf.                                        *)
   6.279 -(* ------------------------------------------------------------------------- *)
   6.280 -
   6.281 -lemma real_max_rsup: "max x y = rsup {x,y}"
   6.282 -proof-
   6.283 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   6.284 -  from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
   6.285 -  moreover
   6.286 -  have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
   6.287 -    by (simp add: linorder_linear)
   6.288 -  ultimately show ?thesis by arith
   6.289 -qed
   6.290 -
   6.291 -lemma real_min_rinf: "min x y = rinf {x,y}"
   6.292 -proof-
   6.293 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   6.294 -  from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
   6.295 -    by (simp add: linorder_linear)
   6.296 -  moreover
   6.297 -  have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
   6.298 -    by simp
   6.299 -  ultimately show ?thesis by arith
   6.300 -qed
   6.301 -
   6.302 -(* ------------------------------------------------------------------------- *)
   6.303  (* Geometric progression.                                                    *)
   6.304  (* ------------------------------------------------------------------------- *)
   6.305  
   6.306 @@ -5048,7 +4790,7 @@
   6.307  
   6.308  (* Infinity norm.                                                            *)
   6.309  
   6.310 -definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   6.311 +definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   6.312  
   6.313  lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
   6.314    by auto
   6.315 @@ -5065,7 +4807,7 @@
   6.316  
   6.317  lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
   6.318    unfolding infnorm_def
   6.319 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   6.320 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   6.321    unfolding infnorm_set_image
   6.322    by auto
   6.323  
   6.324 @@ -5076,13 +4818,13 @@
   6.325    have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
   6.326    show ?thesis
   6.327    unfolding infnorm_def
   6.328 -  unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
   6.329 +  unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
   6.330    apply (subst diff_le_eq[symmetric])
   6.331 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   6.332 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   6.333    unfolding infnorm_set_image bex_simps
   6.334    apply (subst th)
   6.335    unfolding th1
   6.336 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   6.337 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   6.338  
   6.339    unfolding infnorm_set_image ball_simps bex_simps
   6.340    apply simp
   6.341 @@ -5094,7 +4836,7 @@
   6.342  proof-
   6.343    have "infnorm x <= 0 \<longleftrightarrow> x = 0"
   6.344      unfolding infnorm_def
   6.345 -    unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   6.346 +    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   6.347      unfolding infnorm_set_image ball_simps
   6.348      by vector
   6.349    then show ?thesis using infnorm_pos_le[of x] by simp
   6.350 @@ -5105,7 +4847,7 @@
   6.351  
   6.352  lemma infnorm_neg: "infnorm (- x) = infnorm x"
   6.353    unfolding infnorm_def
   6.354 -  apply (rule cong[of "rsup" "rsup"])
   6.355 +  apply (rule cong[of "Sup" "Sup"])
   6.356    apply blast
   6.357    apply (rule set_ext)
   6.358    apply auto
   6.359 @@ -5140,14 +4882,15 @@
   6.360      apply (rule finite_imageI) unfolding Collect_def mem_def by simp
   6.361    have S0: "?S \<noteq> {}" by blast
   6.362    have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
   6.363 -  from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
   6.364 -  show ?thesis unfolding infnorm_def isUb_def setle_def
   6.365 -    unfolding infnorm_set_image ball_simps by auto
   6.366 +  from Sup_finite_in[OF fS S0] 
   6.367 +  show ?thesis unfolding infnorm_def infnorm_set_image 
   6.368 +    by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
   6.369 +              rangeI real_le_refl)
   6.370  qed
   6.371  
   6.372  lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
   6.373    apply (subst infnorm_def)
   6.374 -  unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   6.375 +  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   6.376    unfolding infnorm_set_image ball_simps
   6.377    apply (simp add: abs_mult)
   6.378    apply (rule allI)
   6.379 @@ -5180,7 +4923,7 @@
   6.380  (* Prove that it differs only up to a bound from Euclidean norm.             *)
   6.381  
   6.382  lemma infnorm_le_norm: "infnorm x \<le> norm x"
   6.383 -  unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
   6.384 +  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
   6.385    unfolding infnorm_set_image  ball_simps
   6.386    by (metis component_le_norm)
   6.387  lemma card_enum: "card {1 .. n} = n" by auto
   6.388 @@ -5200,7 +4943,7 @@
   6.389      apply (rule setsum_bounded)
   6.390      apply (rule power_mono)
   6.391      unfolding abs_of_nonneg[OF infnorm_pos_le]
   6.392 -    unfolding infnorm_def  rsup_finite_ge_iff[OF infnorm_set_lemma]
   6.393 +    unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
   6.394      unfolding infnorm_set_image bex_simps
   6.395      apply blast
   6.396      by (rule abs_ge_zero)
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
     7.3 @@ -2100,59 +2100,54 @@
     7.4    shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
     7.5    by (simp add: bounded_iff)
     7.6  
     7.7 -lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
     7.8 -  shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
     7.9 +lemma bounded_has_Sup:
    7.10 +  fixes S :: "real set"
    7.11 +  assumes "bounded S" "S \<noteq> {}"
    7.12 +  shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
    7.13 +proof
    7.14 +  fix x assume "x\<in>S"
    7.15 +  thus "x \<le> Sup S"
    7.16 +    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
    7.17 +next
    7.18 +  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
    7.19 +    by (metis SupInf.Sup_least)
    7.20 +qed
    7.21 +
    7.22 +lemma Sup_insert:
    7.23 +  fixes S :: "real set"
    7.24 +  shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" 
    7.25 +by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) 
    7.26 +
    7.27 +lemma Sup_insert_finite:
    7.28 +  fixes S :: "real set"
    7.29 +  shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
    7.30 +  apply (rule Sup_insert)
    7.31 +  apply (rule finite_imp_bounded)
    7.32 +  by simp
    7.33 +
    7.34 +lemma bounded_has_Inf:
    7.35 +  fixes S :: "real set"
    7.36 +  assumes "bounded S"  "S \<noteq> {}"
    7.37 +  shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
    7.38  proof
    7.39    fix x assume "x\<in>S"
    7.40    from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
    7.41 -  hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
    7.42 -  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
    7.43 -next
    7.44 -  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
    7.45 -  using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
    7.46 -  apply (auto simp add: bounded_real)
    7.47 -  by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
    7.48 -qed
    7.49 -
    7.50 -lemma rsup_insert: assumes "bounded S"
    7.51 -  shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
    7.52 -proof(cases "S={}")
    7.53 -  case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
    7.54 +  thus "x \<ge> Inf S" using `x\<in>S`
    7.55 +    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
    7.56  next
    7.57 -  let ?S = "insert x S"
    7.58 -  case False
    7.59 -  hence *:"\<forall>x\<in>S. x \<le> rsup S" using bounded_has_rsup(1)[of S] using assms by auto
    7.60 -  hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto
    7.61 -  hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto
    7.62 -  moreover
    7.63 -  have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto
    7.64 -  { fix y assume as:"isUb UNIV (insert x S) y"
    7.65 -    hence "max x (rsup S) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
    7.66 -      unfolding setle_def by auto  }
    7.67 -  hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto
    7.68 -  hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto
    7.69 -  ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\<noteq>{}` by auto
    7.70 -qed
    7.71 -
    7.72 -lemma sup_insert_finite: "finite S \<Longrightarrow> rsup(insert x S) = (if S = {} then x else max x (rsup S))"
    7.73 -  apply (rule rsup_insert)
    7.74 -  apply (rule finite_imp_bounded)
    7.75 -  by simp
    7.76 -
    7.77 -lemma bounded_has_rinf:
    7.78 -  assumes "bounded S"  "S \<noteq> {}"
    7.79 -  shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
    7.80 -proof
    7.81 -  fix x assume "x\<in>S"
    7.82 -  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
    7.83 -  hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
    7.84 -  thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
    7.85 -next
    7.86 -  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
    7.87 -  using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
    7.88 -  apply (auto simp add: bounded_real)
    7.89 -  by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
    7.90 -qed
    7.91 +  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
    7.92 +    by (metis SupInf.Inf_greatest)
    7.93 +qed
    7.94 +
    7.95 +lemma Inf_insert:
    7.96 +  fixes S :: "real set"
    7.97 +  shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" 
    7.98 +by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) 
    7.99 +lemma Inf_insert_finite:
   7.100 +  fixes S :: "real set"
   7.101 +  shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
   7.102 +  by (rule Inf_insert, rule finite_imp_bounded, simp)
   7.103 +
   7.104  
   7.105  (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
   7.106  lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
   7.107 @@ -2161,29 +2156,6 @@
   7.108    apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   7.109    done
   7.110  
   7.111 -lemma rinf_insert: assumes "bounded S"
   7.112 -  shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
   7.113 -proof(cases "S={}")
   7.114 -  case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
   7.115 -next
   7.116 -  let ?S = "insert x S"
   7.117 -  case False
   7.118 -  hence *:"\<forall>x\<in>S. x \<ge> rinf S" using bounded_has_rinf(1)[of S] using assms by auto
   7.119 -  hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto
   7.120 -  hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto
   7.121 -  moreover
   7.122 -  have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto
   7.123 -  { fix y assume as:"isLb UNIV (insert x S) y"
   7.124 -    hence "min x (rinf S) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
   7.125 -      unfolding setge_def by auto  }
   7.126 -  hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto
   7.127 -  hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto
   7.128 -  ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\<noteq>{}` by auto
   7.129 -qed
   7.130 -
   7.131 -lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))"
   7.132 -  by (rule rinf_insert, rule finite_imp_bounded, simp)
   7.133 -
   7.134  subsection{* Compactness (the definition is the one based on convegent subsequences). *}
   7.135  
   7.136  definition
   7.137 @@ -4120,30 +4092,35 @@
   7.138    shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
   7.139  proof-
   7.140    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
   7.141 -  { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
   7.142 -    have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
   7.143 -    moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
   7.144 -    ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto  }
   7.145 -  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
   7.146 -    apply(rule_tac x="rsup s" in bexI) by auto
   7.147 -qed
   7.148 +  { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
   7.149 +    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
   7.150 +    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
   7.151 +    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
   7.152 +  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
   7.153 +    apply(rule_tac x="Sup s" in bexI) by auto
   7.154 +qed
   7.155 +
   7.156 +lemma Inf:
   7.157 +  fixes S :: "real set"
   7.158 +  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
   7.159 +by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
   7.160  
   7.161  lemma compact_attains_inf:
   7.162    fixes s :: "real set"
   7.163    assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
   7.164  proof-
   7.165    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
   7.166 -  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s"  "rinf s \<notin> s"  "0 < e"
   7.167 -      "\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
   7.168 -    have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
   7.169 +  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
   7.170 +      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
   7.171 +    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
   7.172      moreover
   7.173      { fix x assume "x \<in> s"
   7.174 -      hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
   7.175 -      have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
   7.176 -    hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
   7.177 -    ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto  }
   7.178 -  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
   7.179 -    apply(rule_tac x="rinf s" in bexI) by auto
   7.180 +      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
   7.181 +      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
   7.182 +    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
   7.183 +    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
   7.184 +  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
   7.185 +    apply(rule_tac x="Inf s" in bexI) by auto
   7.186  qed
   7.187  
   7.188  lemma continuous_attains_sup:
   7.189 @@ -4413,7 +4390,7 @@
   7.190  
   7.191  text{* We can state this in terms of diameter of a set.                          *}
   7.192  
   7.193 -definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   7.194 +definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   7.195    (* TODO: generalize to class metric_space *)
   7.196  
   7.197  lemma diameter_bounded:
   7.198 @@ -4427,12 +4404,22 @@
   7.199      hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
   7.200    note * = this
   7.201    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
   7.202 -    have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
   7.203 +    have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
   7.204 +      apply auto    (*FIXME: something horrible has happened here!*)
   7.205 +      apply atomize
   7.206 +      apply safe
   7.207 +      apply metis +
   7.208 +      done
   7.209      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto  }
   7.210    moreover
   7.211    { fix d::real assume "d>0" "d < diameter s"
   7.212      hence "s\<noteq>{}" unfolding diameter_def by auto
   7.213 -    hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto
   7.214 +    hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def 
   7.215 +      apply auto    (*FIXME: something horrible has happened here!*)
   7.216 +      apply atomize
   7.217 +      apply safe
   7.218 +      apply metis +
   7.219 +      done
   7.220      have "\<exists>d' \<in> ?D. d' > d"
   7.221      proof(rule ccontr)
   7.222        assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
   7.223 @@ -4456,8 +4443,8 @@
   7.224  proof-
   7.225    have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
   7.226    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
   7.227 -  hence "diameter s \<le> norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}" "norm (x - y)"]
   7.228 -    unfolding setle_def and diameter_def by auto
   7.229 +  hence "diameter s \<le> norm (x - y)" 
   7.230 +    by (force simp add: diameter_def intro!: Sup_least) 
   7.231    thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
   7.232  qed
   7.233  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Oct 28 11:43:06 2009 +0000
     8.3 @@ -0,0 +1,993 @@
     8.4 +header {*Caratheodory Extension Theorem*}
     8.5 +
     8.6 +theory Caratheodory
     8.7 +  imports Sigma_Algebra SupInf SeriesPlus
     8.8 +
     8.9 +begin
    8.10 +
    8.11 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    8.12 +
    8.13 +subsection {* Measure Spaces *}
    8.14 +
    8.15 +text {*A measure assigns a nonnegative real to every measurable set. 
    8.16 +       It is countably additive for disjoint sets.*}
    8.17 +
    8.18 +record 'a measure_space = "'a algebra" +
    8.19 +  measure:: "'a set \<Rightarrow> real"
    8.20 +
    8.21 +definition
    8.22 +  disjoint_family  where
    8.23 +  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
    8.24 +
    8.25 +definition
    8.26 +  positive  where
    8.27 +  "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
    8.28 +
    8.29 +definition
    8.30 +  additive  where
    8.31 +  "additive M f \<longleftrightarrow> 
    8.32 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
    8.33 +    \<longrightarrow> f (x \<union> y) = f x + f y)"
    8.34 +
    8.35 +definition
    8.36 +  countably_additive  where
    8.37 +  "countably_additive M f \<longleftrightarrow> 
    8.38 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> 
    8.39 +         disjoint_family A \<longrightarrow>
    8.40 +         (\<Union>i. A i) \<in> sets M \<longrightarrow> 
    8.41 +         (\<lambda>n. f (A n))  sums  f (\<Union>i. A i))"
    8.42 +
    8.43 +definition
    8.44 +  increasing  where
    8.45 +  "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
    8.46 +
    8.47 +definition
    8.48 +  subadditive  where
    8.49 +  "subadditive M f \<longleftrightarrow> 
    8.50 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
    8.51 +    \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    8.52 +
    8.53 +definition
    8.54 +  countably_subadditive  where
    8.55 +  "countably_subadditive M f \<longleftrightarrow> 
    8.56 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> 
    8.57 +         disjoint_family A \<longrightarrow>
    8.58 +         (\<Union>i. A i) \<in> sets M \<longrightarrow> 
    8.59 +         summable (f o A) \<longrightarrow>
    8.60 +         f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
    8.61 +
    8.62 +definition
    8.63 +  lambda_system where
    8.64 +  "lambda_system M f = 
    8.65 +    {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
    8.66 +
    8.67 +definition
    8.68 +  outer_measure_space where
    8.69 +  "outer_measure_space M f  \<longleftrightarrow> 
    8.70 +     positive M f & increasing M f & countably_subadditive M f"
    8.71 +
    8.72 +definition
    8.73 +  measure_set where
    8.74 +  "measure_set M f X =
    8.75 +     {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
    8.76 +
    8.77 +
    8.78 +locale measure_space = sigma_algebra +
    8.79 +  assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a"
    8.80 +      and empty_measure [simp]: "measure M {} = (0::real)"
    8.81 +      and ca: "countably_additive M (measure M)"
    8.82 +
    8.83 +subsection {* Basic Lemmas *}
    8.84 +
    8.85 +lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0"
    8.86 +  by (simp add: positive_def) 
    8.87 +
    8.88 +lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
    8.89 +  by (simp add: positive_def) 
    8.90 +
    8.91 +lemma increasingD:
    8.92 +     "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
    8.93 +  by (auto simp add: increasing_def)
    8.94 +
    8.95 +lemma subadditiveD:
    8.96 +     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
    8.97 +      \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    8.98 +  by (auto simp add: subadditive_def)
    8.99 +
   8.100 +lemma additiveD:
   8.101 +     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
   8.102 +      \<Longrightarrow> f (x \<union> y) = f x + f y"
   8.103 +  by (auto simp add: additive_def)
   8.104 +
   8.105 +lemma countably_additiveD:
   8.106 +  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A 
   8.107 +   \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
   8.108 +  by (simp add: countably_additive_def) 
   8.109 +
   8.110 +lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
   8.111 +  by blast
   8.112 +
   8.113 +lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
   8.114 +  by blast
   8.115 +
   8.116 +lemma disjoint_family_subset:
   8.117 +     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
   8.118 +  by (force simp add: disjoint_family_def) 
   8.119 +
   8.120 +subsection {* A Two-Element Series *}
   8.121 +
   8.122 +definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
   8.123 +  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
   8.124 +
   8.125 +lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
   8.126 +  apply (simp add: binaryset_def) 
   8.127 +  apply (rule set_ext) 
   8.128 +  apply (auto simp add: image_iff) 
   8.129 +  done
   8.130 +
   8.131 +lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
   8.132 +  by (simp add: UNION_eq_Union_image range_binaryset_eq) 
   8.133 +
   8.134 +lemma LIMSEQ_binaryset: 
   8.135 +  assumes f: "f {} = 0"
   8.136 +  shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
   8.137 +proof -
   8.138 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
   8.139 +    proof 
   8.140 +      fix n
   8.141 +      show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
   8.142 +	by (induct n)  (auto simp add: binaryset_def f) 
   8.143 +    qed
   8.144 +  moreover
   8.145 +  have "... ----> f A + f B" by (rule LIMSEQ_const) 
   8.146 +  ultimately
   8.147 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" 
   8.148 +    by metis
   8.149 +  hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
   8.150 +    by simp
   8.151 +  thus ?thesis by (rule LIMSEQ_offset [where k=2])
   8.152 +qed
   8.153 +
   8.154 +lemma binaryset_sums:
   8.155 +  assumes f: "f {} = 0"
   8.156 +  shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
   8.157 +    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) 
   8.158 +
   8.159 +lemma suminf_binaryset_eq:
   8.160 +     "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
   8.161 +  by (metis binaryset_sums sums_unique)
   8.162 +
   8.163 +
   8.164 +subsection {* Lambda Systems *}
   8.165 +
   8.166 +lemma (in algebra) lambda_system_eq:
   8.167 +    "lambda_system M f = 
   8.168 +        {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
   8.169 +proof -
   8.170 +  have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
   8.171 +    by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space)
   8.172 +  show ?thesis
   8.173 +    by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+
   8.174 +qed
   8.175 +
   8.176 +lemma (in algebra) lambda_system_empty:
   8.177 +    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
   8.178 +  by (auto simp add: positive_def lambda_system_eq) 
   8.179 +
   8.180 +lemma lambda_system_sets:
   8.181 +    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
   8.182 +  by (simp add:  lambda_system_def)
   8.183 +
   8.184 +lemma (in algebra) lambda_system_Compl:
   8.185 +  fixes f:: "'a set \<Rightarrow> real"
   8.186 +  assumes x: "x \<in> lambda_system M f"
   8.187 +  shows "space M - x \<in> lambda_system M f"
   8.188 +  proof -
   8.189 +    have "x \<subseteq> space M"
   8.190 +      by (metis sets_into_space lambda_system_sets x)
   8.191 +    hence "space M - (space M - x) = x"
   8.192 +      by (metis double_diff equalityE) 
   8.193 +    with x show ?thesis
   8.194 +      by (force simp add: lambda_system_def)
   8.195 +  qed
   8.196 +
   8.197 +lemma (in algebra) lambda_system_Int:
   8.198 +  fixes f:: "'a set \<Rightarrow> real"
   8.199 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   8.200 +  shows "x \<inter> y \<in> lambda_system M f"
   8.201 +  proof -
   8.202 +    from xl yl show ?thesis
   8.203 +      proof (auto simp add: positive_def lambda_system_eq Int)
   8.204 +	fix u
   8.205 +	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
   8.206 +           and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
   8.207 +           and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
   8.208 +	have "u - x \<inter> y \<in> sets M"
   8.209 +	  by (metis Diff Diff_Int Un u x y)
   8.210 +	moreover
   8.211 +	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
   8.212 +	moreover
   8.213 +	have "u - x \<inter> y - y = u - y" by blast
   8.214 +	ultimately
   8.215 +	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
   8.216 +	  by force
   8.217 +	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
   8.218 +              = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
   8.219 +	  by (simp add: ey) 
   8.220 +	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
   8.221 +	  by (simp add: Int_ac) 
   8.222 +	also have "... = f (u \<inter> y) + f (u - y)"
   8.223 +	  using fx [THEN bspec, of "u \<inter> y"] Int y u
   8.224 +	  by force
   8.225 +	also have "... = f u"
   8.226 +	  by (metis fy u) 
   8.227 +	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
   8.228 +      qed
   8.229 +  qed
   8.230 +
   8.231 +
   8.232 +lemma (in algebra) lambda_system_Un:
   8.233 +  fixes f:: "'a set \<Rightarrow> real"
   8.234 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   8.235 +  shows "x \<union> y \<in> lambda_system M f"
   8.236 +proof -
   8.237 +  have "(space M - x) \<inter> (space M - y) \<in> sets M"
   8.238 +    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) 
   8.239 +  moreover
   8.240 +  have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
   8.241 +    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
   8.242 +  ultimately show ?thesis
   8.243 +    by (metis lambda_system_Compl lambda_system_Int xl yl) 
   8.244 +qed
   8.245 +
   8.246 +lemma (in algebra) lambda_system_algebra:
   8.247 +    "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
   8.248 +  apply (auto simp add: algebra_def) 
   8.249 +  apply (metis lambda_system_sets set_mp sets_into_space)
   8.250 +  apply (metis lambda_system_empty)
   8.251 +  apply (metis lambda_system_Compl)
   8.252 +  apply (metis lambda_system_Un) 
   8.253 +  done
   8.254 +
   8.255 +lemma (in algebra) lambda_system_strong_additive:
   8.256 +  assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
   8.257 +      and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   8.258 +  shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
   8.259 +  proof -
   8.260 +    have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
   8.261 +    moreover
   8.262 +    have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
   8.263 +    moreover 
   8.264 +    have "(z \<inter> (x \<union> y)) \<in> sets M"
   8.265 +      by (metis Int Un lambda_system_sets xl yl z) 
   8.266 +    ultimately show ?thesis using xl yl
   8.267 +      by (simp add: lambda_system_eq)
   8.268 +  qed
   8.269 +
   8.270 +lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
   8.271 +  by (metis Int_absorb1 sets_into_space)
   8.272 +
   8.273 +lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
   8.274 +  by (metis Int_absorb2 sets_into_space)
   8.275 +
   8.276 +lemma (in algebra) lambda_system_additive:
   8.277 +     "additive (M (|sets := lambda_system M f|)) f"
   8.278 +  proof (auto simp add: additive_def)
   8.279 +    fix x and y
   8.280 +    assume disj: "x \<inter> y = {}"
   8.281 +       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   8.282 +    hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
   8.283 +    thus "f (x \<union> y) = f x + f y" 
   8.284 +      using lambda_system_strong_additive [OF top disj xl yl]
   8.285 +      by (simp add: Un)
   8.286 +  qed
   8.287 +
   8.288 +
   8.289 +lemma (in algebra) countably_subadditive_subadditive:
   8.290 +  assumes f: "positive M f" and cs: "countably_subadditive M f"
   8.291 +  shows  "subadditive M f"
   8.292 +proof (auto simp add: subadditive_def) 
   8.293 +  fix x y
   8.294 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   8.295 +  hence "disjoint_family (binaryset x y)"
   8.296 +    by (auto simp add: disjoint_family_def binaryset_def) 
   8.297 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
   8.298 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
   8.299 +         summable (f o (binaryset x y)) \<longrightarrow>
   8.300 +         f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
   8.301 +    using cs by (simp add: countably_subadditive_def) 
   8.302 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
   8.303 +         summable (f o (binaryset x y)) \<longrightarrow>
   8.304 +         f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
   8.305 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
   8.306 +  thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
   8.307 +    by (auto simp add: Un sums_iff positive_def o_def) 
   8.308 +qed 
   8.309 +
   8.310 +
   8.311 +definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
   8.312 +  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
   8.313 +
   8.314 +lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
   8.315 +proof (induct n)
   8.316 +  case 0 show ?case by simp
   8.317 +next
   8.318 +  case (Suc n)
   8.319 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 
   8.320 +qed
   8.321 +
   8.322 +lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   8.323 +  apply (rule UN_finite2_eq [where k=0]) 
   8.324 +  apply (simp add: finite_UN_disjointed_eq) 
   8.325 +  done
   8.326 +
   8.327 +lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   8.328 +  by (auto simp add: disjointed_def)
   8.329 +
   8.330 +lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   8.331 +  by (simp add: disjoint_family_def) 
   8.332 +     (metis neq_iff Int_commute less_disjoint_disjointed)
   8.333 +
   8.334 +lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   8.335 +  by (auto simp add: disjointed_def)
   8.336 +
   8.337 +
   8.338 +lemma (in algebra) UNION_in_sets:
   8.339 +  fixes A:: "nat \<Rightarrow> 'a set"
   8.340 +  assumes A: "range A \<subseteq> sets M "
   8.341 +  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   8.342 +proof (induct n)
   8.343 +  case 0 show ?case by simp
   8.344 +next
   8.345 +  case (Suc n) 
   8.346 +  thus ?case
   8.347 +    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
   8.348 +qed
   8.349 +
   8.350 +lemma (in algebra) range_disjointed_sets:
   8.351 +  assumes A: "range A \<subseteq> sets M "
   8.352 +  shows  "range (disjointed A) \<subseteq> sets M"
   8.353 +proof (auto simp add: disjointed_def) 
   8.354 +  fix n
   8.355 +  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
   8.356 +    by (metis A Diff UNIV_I disjointed_def image_subset_iff)
   8.357 +qed
   8.358 +
   8.359 +lemma sigma_algebra_disjoint_iff: 
   8.360 +     "sigma_algebra M \<longleftrightarrow> 
   8.361 +      algebra M &
   8.362 +      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> 
   8.363 +           (\<Union>i::nat. A i) \<in> sets M)"
   8.364 +proof (auto simp add: sigma_algebra_iff)
   8.365 +  fix A :: "nat \<Rightarrow> 'a set"
   8.366 +  assume M: "algebra M"
   8.367 +     and A: "range A \<subseteq> sets M"
   8.368 +     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
   8.369 +               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   8.370 +  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
   8.371 +         disjoint_family (disjointed A) \<longrightarrow>
   8.372 +         (\<Union>i. disjointed A i) \<in> sets M" by blast
   8.373 +  hence "(\<Union>i. disjointed A i) \<in> sets M"
   8.374 +    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) 
   8.375 +  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
   8.376 +qed
   8.377 +
   8.378 +
   8.379 +lemma (in algebra) additive_sum:
   8.380 +  fixes A:: "nat \<Rightarrow> 'a set"
   8.381 +  assumes f: "positive M f" and ad: "additive M f"
   8.382 +      and A: "range A \<subseteq> sets M"
   8.383 +      and disj: "disjoint_family A"
   8.384 +  shows  "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
   8.385 +proof (induct n)
   8.386 +  case 0 show ?case using f by (simp add: positive_def) 
   8.387 +next
   8.388 +  case (Suc n) 
   8.389 +  have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj 
   8.390 +    by (auto simp add: disjoint_family_def neq_iff) blast
   8.391 +  moreover 
   8.392 +  have "A n \<in> sets M" using A by blast 
   8.393 +  moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   8.394 +    by (metis A UNION_in_sets atLeast0LessThan)
   8.395 +  moreover 
   8.396 +  ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
   8.397 +    using ad UNION_in_sets A by (auto simp add: additive_def) 
   8.398 +  with Suc.hyps show ?case using ad
   8.399 +    by (auto simp add: atLeastLessThanSuc additive_def) 
   8.400 +qed
   8.401 +
   8.402 +
   8.403 +lemma countably_subadditiveD:
   8.404 +  "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
   8.405 +   (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)" 
   8.406 +  by (auto simp add: countably_subadditive_def o_def)
   8.407 +
   8.408 +lemma (in algebra) increasing_additive_summable:
   8.409 +  fixes A:: "nat \<Rightarrow> 'a set"
   8.410 +  assumes f: "positive M f" and ad: "additive M f"
   8.411 +      and inc: "increasing M f"
   8.412 +      and A: "range A \<subseteq> sets M"
   8.413 +      and disj: "disjoint_family A"
   8.414 +  shows  "summable (f o A)"
   8.415 +proof (rule pos_summable) 
   8.416 +  fix n
   8.417 +  show "0 \<le> (f \<circ> A) n" using f A
   8.418 +    by (force simp add: positive_def)
   8.419 +  next
   8.420 +  fix n
   8.421 +  have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
   8.422 +    by (rule additive_sum [OF f ad A disj]) 
   8.423 +  also have "... \<le> f (space M)" using space_closed A
   8.424 +    by (blast intro: increasingD [OF inc] UNION_in_sets top) 
   8.425 +  finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
   8.426 +qed
   8.427 +
   8.428 +lemma lambda_system_positive:
   8.429 +     "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
   8.430 +  by (simp add: positive_def lambda_system_def) 
   8.431 +
   8.432 +lemma lambda_system_increasing:
   8.433 +   "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
   8.434 +  by (simp add: increasing_def lambda_system_def) 
   8.435 +
   8.436 +lemma (in algebra) lambda_system_strong_sum:
   8.437 +  fixes A:: "nat \<Rightarrow> 'a set"
   8.438 +  assumes f: "positive M f" and a: "a \<in> sets M"
   8.439 +      and A: "range A \<subseteq> lambda_system M f"
   8.440 +      and disj: "disjoint_family A"
   8.441 +  shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
   8.442 +proof (induct n)
   8.443 +  case 0 show ?case using f by (simp add: positive_def) 
   8.444 +next
   8.445 +  case (Suc n) 
   8.446 +  have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
   8.447 +    by (force simp add: disjoint_family_def neq_iff) 
   8.448 +  have 3: "A n \<in> lambda_system M f" using A
   8.449 +    by blast
   8.450 +  have 4: "UNION {0..<n} A \<in> lambda_system M f"
   8.451 +    using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] 
   8.452 +    by simp
   8.453 +  from Suc.hyps show ?case
   8.454 +    by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
   8.455 +qed
   8.456 +
   8.457 +
   8.458 +lemma (in sigma_algebra) lambda_system_caratheodory:
   8.459 +  assumes oms: "outer_measure_space M f"
   8.460 +      and A: "range A \<subseteq> lambda_system M f"
   8.461 +      and disj: "disjoint_family A"
   8.462 +  shows  "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A)  sums  f (\<Union>i. A i)"
   8.463 +proof -
   8.464 +  have pos: "positive M f" and inc: "increasing M f" 
   8.465 +   and csa: "countably_subadditive M f" 
   8.466 +    by (metis oms outer_measure_space_def)+
   8.467 +  have sa: "subadditive M f"
   8.468 +    by (metis countably_subadditive_subadditive csa pos) 
   8.469 +  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A 
   8.470 +    by simp
   8.471 +  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
   8.472 +    by (rule lambda_system_algebra [OF pos]) 
   8.473 +  have A'': "range A \<subseteq> sets M"
   8.474 +     by (metis A image_subset_iff lambda_system_sets)
   8.475 +  have sumfA: "summable (f \<circ> A)" 
   8.476 +    by (metis algebra.increasing_additive_summable [OF alg_ls]
   8.477 +          lambda_system_positive lambda_system_additive lambda_system_increasing
   8.478 +          A' oms outer_measure_space_def disj)
   8.479 +  have U_in: "(\<Union>i. A i) \<in> sets M"
   8.480 +    by (metis A countable_UN image_subset_iff lambda_system_sets)
   8.481 +  have U_eq: "f (\<Union>i. A i) = suminf (f o A)" 
   8.482 +    proof (rule antisym)
   8.483 +      show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
   8.484 +	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
   8.485 +      show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
   8.486 +	by (rule suminf_le [OF sumfA]) 
   8.487 +           (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
   8.488 +	          lambda_system_positive lambda_system_additive 
   8.489 +                  subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) 
   8.490 +    qed
   8.491 +  {
   8.492 +    fix a 
   8.493 +    assume a [iff]: "a \<in> sets M" 
   8.494 +    have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
   8.495 +    proof -
   8.496 +      have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' 
   8.497 +	apply -
   8.498 +	apply (rule summable_comparison_test [OF _ sumfA]) 
   8.499 +	apply (rule_tac x="0" in exI) 
   8.500 +	apply (simp add: positive_def) 
   8.501 +	apply (auto simp add: )
   8.502 +	apply (subst abs_of_nonneg)
   8.503 +	apply (metis A'' Int UNIV_I a image_subset_iff)
   8.504 +	apply (blast intro:  increasingD [OF inc] a)   
   8.505 +	done
   8.506 +      show ?thesis
   8.507 +      proof (rule antisym)
   8.508 +	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
   8.509 +	  by blast
   8.510 +	moreover 
   8.511 +	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   8.512 +	  by (auto simp add: disjoint_family_def) 
   8.513 +	moreover 
   8.514 +	have "a \<inter> (\<Union>i. A i) \<in> sets M"
   8.515 +	  by (metis Int U_in a)
   8.516 +	ultimately 
   8.517 +	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
   8.518 +	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
   8.519 +	  by (simp add: o_def) 
   8.520 +	moreover 
   8.521 +	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
   8.522 +	  proof (rule suminf_le [OF summ])
   8.523 +	    fix n
   8.524 +	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   8.525 +	      by (metis A'' UNION_in_sets) 
   8.526 +	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   8.527 +	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
   8.528 +	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
   8.529 +	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
   8.530 +	      by (simp add: A) 
   8.531 +	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
   8.532 +	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
   8.533 +	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   8.534 +	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
   8.535 +                               UNION_in U_in a) 
   8.536 +	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
   8.537 +	      using eq_fa
   8.538 +	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
   8.539 +                            a A disj)
   8.540 +	  qed
   8.541 +	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
   8.542 +	  by arith
   8.543 +      next
   8.544 +	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
   8.545 +	  by (blast intro:  increasingD [OF inc] a U_in)
   8.546 +	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   8.547 +	  by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
   8.548 +	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   8.549 +        qed
   8.550 +     qed
   8.551 +  }
   8.552 +  thus  ?thesis
   8.553 +    by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA)
   8.554 +qed
   8.555 +
   8.556 +lemma (in sigma_algebra) caratheodory_lemma:
   8.557 +  assumes oms: "outer_measure_space M f"
   8.558 +  shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)"
   8.559 +proof -
   8.560 +  have pos: "positive M f" 
   8.561 +    by (metis oms outer_measure_space_def)
   8.562 +  have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)"
   8.563 +    using lambda_system_algebra [OF pos]
   8.564 +    by (simp add: algebra_def) 
   8.565 +  then moreover 
   8.566 +  have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)"
   8.567 +    using lambda_system_caratheodory [OF oms]
   8.568 +    by (simp add: sigma_algebra_disjoint_iff) 
   8.569 +  moreover 
   8.570 +  have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" 
   8.571 +    using pos lambda_system_caratheodory [OF oms]
   8.572 +    by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
   8.573 +                  countably_additive_def o_def) 
   8.574 +  ultimately 
   8.575 +  show ?thesis
   8.576 +    by intro_locales (auto simp add: sigma_algebra_def) 
   8.577 +qed
   8.578 +
   8.579 +
   8.580 +lemma (in algebra) inf_measure_nonempty:
   8.581 +  assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
   8.582 +  shows "f b \<in> measure_set M f a"
   8.583 +proof -
   8.584 +  have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}"
   8.585 +    by (rule series_zero)  (simp add: positive_imp_0 [OF f]) 
   8.586 +  also have "... = f b" 
   8.587 +    by simp
   8.588 +  finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
   8.589 +  thus ?thesis using a
   8.590 +    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] 
   8.591 +             simp add: measure_set_def disjoint_family_def b split_if_mem2) 
   8.592 +qed  
   8.593 +
   8.594 +lemma (in algebra) inf_measure_pos0:
   8.595 +     "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x"
   8.596 +apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero)
   8.597 +apply blast
   8.598 +done
   8.599 +
   8.600 +lemma (in algebra) inf_measure_pos:
   8.601 +  shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)"
   8.602 +apply (rule Inf_greatest)
   8.603 +apply (metis emptyE inf_measure_nonempty top)
   8.604 +apply (metis inf_measure_pos0) 
   8.605 +done
   8.606 +
   8.607 +lemma (in algebra) additive_increasing:
   8.608 +  assumes posf: "positive M f" and addf: "additive M f" 
   8.609 +  shows "increasing M f"
   8.610 +proof (auto simp add: increasing_def) 
   8.611 +  fix x y
   8.612 +  assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
   8.613 +  have "f x \<le> f x + f (y-x)" using posf
   8.614 +    by (simp add: positive_def) (metis Diff xy)
   8.615 +  also have "... = f (x \<union> (y-x))" using addf
   8.616 +    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) 
   8.617 +  also have "... = f y"
   8.618 +    by (metis Un_Diff_cancel Un_absorb1 xy)
   8.619 +  finally show "f x \<le> f y" .
   8.620 +qed
   8.621 +
   8.622 +lemma (in algebra) countably_additive_additive:
   8.623 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   8.624 +  shows "additive M f"
   8.625 +proof (auto simp add: additive_def) 
   8.626 +  fix x y
   8.627 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   8.628 +  hence "disjoint_family (binaryset x y)"
   8.629 +    by (auto simp add: disjoint_family_def binaryset_def) 
   8.630 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
   8.631 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
   8.632 +         f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
   8.633 +    using ca
   8.634 +    by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) 
   8.635 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
   8.636 +         f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
   8.637 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
   8.638 +  thus "f (x \<union> y) = f x + f y" using posf x y
   8.639 +    by (simp add: Un suminf_binaryset_eq positive_def)
   8.640 +qed 
   8.641 + 
   8.642 +lemma (in algebra) inf_measure_agrees:
   8.643 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   8.644 +      and s: "s \<in> sets M"  
   8.645 +  shows "Inf (measure_set M f s) = f s"
   8.646 +proof (rule Inf_eq) 
   8.647 +  fix z
   8.648 +  assume z: "z \<in> measure_set M f s"
   8.649 +  from this obtain A where 
   8.650 +    A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   8.651 +    and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
   8.652 +    and si: "suminf (f \<circ> A) = z"
   8.653 +    by (auto simp add: measure_set_def sums_iff) 
   8.654 +  hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
   8.655 +  have inc: "increasing M f"
   8.656 +    by (metis additive_increasing ca countably_additive_additive posf)
   8.657 +  have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
   8.658 +    proof (rule countably_additiveD [OF ca]) 
   8.659 +      show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   8.660 +	by blast
   8.661 +      show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   8.662 +	by (auto simp add: disjoint_family_def)
   8.663 +      show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   8.664 +	by (metis UN_extend_simps(4) s seq)
   8.665 +    qed
   8.666 +  hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
   8.667 +    by (metis Int_commute UN_simps(4) seq sums_iff) 
   8.668 +  also have "... \<le> suminf (f \<circ> A)" 
   8.669 +    proof (rule summable_le [OF _ _ sm]) 
   8.670 +      show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
   8.671 +	by (force intro: increasingD [OF inc]) 
   8.672 +      show "summable (\<lambda>i. f (A i \<inter> s))" using sums
   8.673 +	by (simp add: sums_iff) 
   8.674 +    qed
   8.675 +  also have "... = z" by (rule si) 
   8.676 +  finally show "f s \<le> z" .
   8.677 +next
   8.678 +  fix y
   8.679 +  assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
   8.680 +  thus "y \<le> f s"
   8.681 +    by (blast intro: inf_measure_nonempty [OF posf s subset_refl])
   8.682 +qed
   8.683 +
   8.684 +lemma (in algebra) inf_measure_empty:
   8.685 +  assumes posf: "positive M f"
   8.686 +  shows "Inf (measure_set M f {}) = 0"
   8.687 +proof (rule antisym)
   8.688 +  show "0 \<le> Inf (measure_set M f {})"
   8.689 +    by (metis empty_subsetI inf_measure_pos posf) 
   8.690 +  show "Inf (measure_set M f {}) \<le> 0"
   8.691 +    by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf
   8.692 +              positive_imp_0 subset_refl) 
   8.693 +qed
   8.694 +
   8.695 +lemma (in algebra) inf_measure_positive:
   8.696 +  "positive M f \<Longrightarrow> 
   8.697 +   positive (| space = space M, sets = Pow (space M) |)
   8.698 +                  (\<lambda>x. Inf (measure_set M f x))"
   8.699 +  by (simp add: positive_def inf_measure_empty inf_measure_pos) 
   8.700 +
   8.701 +lemma (in algebra) inf_measure_increasing:
   8.702 +  assumes posf: "positive M f"
   8.703 +  shows "increasing (| space = space M, sets = Pow (space M) |)
   8.704 +                    (\<lambda>x. Inf (measure_set M f x))"
   8.705 +apply (auto simp add: increasing_def) 
   8.706 +apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
   8.707 +apply (rule Inf_lower) 
   8.708 +apply (clarsimp simp add: measure_set_def, blast) 
   8.709 +apply (blast intro: inf_measure_pos0 posf)
   8.710 +done
   8.711 +
   8.712 +
   8.713 +lemma (in algebra) inf_measure_le:
   8.714 +  assumes posf: "positive M f" and inc: "increasing M f" 
   8.715 +      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
   8.716 +  shows "Inf (measure_set M f s) \<le> x"
   8.717 +proof -
   8.718 +  from x
   8.719 +  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" 
   8.720 +             and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
   8.721 +    by (auto simp add: sums_iff)
   8.722 +  have dA: "range (disjointed A) \<subseteq> sets M"
   8.723 +    by (metis A range_disjointed_sets)
   8.724 +  have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
   8.725 +    proof (auto)
   8.726 +      fix n
   8.727 +      have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
   8.728 +	by (auto simp add: positive_def image_subset_iff)
   8.729 +      also have "... \<le> f (A n)" 
   8.730 +	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   8.731 +      finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
   8.732 +    qed
   8.733 +  from Series.summable_le2 [OF this sm]
   8.734 +  have sda:  "summable (f o disjointed A)"  
   8.735 +             "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
   8.736 +    by blast+
   8.737 +  hence ley: "suminf (f o disjointed A) \<le> x"
   8.738 +    by (metis xeq) 
   8.739 +  from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
   8.740 +    by (simp add: sums_iff) 
   8.741 +  hence y: "suminf (f o disjointed A) \<in> measure_set M f s"
   8.742 +    apply (auto simp add: measure_set_def)
   8.743 +    apply (rule_tac x="disjointed A" in exI) 
   8.744 +    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
   8.745 +    done
   8.746 +  show ?thesis
   8.747 +    by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf)
   8.748 +qed
   8.749 +
   8.750 +lemma (in algebra) inf_measure_close:
   8.751 +  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
   8.752 +  shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) & 
   8.753 +               (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
   8.754 +proof -
   8.755 +  have " measure_set M f s \<noteq> {}" 
   8.756 +    by (metis emptyE ss inf_measure_nonempty [OF posf top])
   8.757 +  hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e" 
   8.758 +    by (rule Inf_close [OF _ e])
   8.759 +  thus ?thesis 
   8.760 +    by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto)
   8.761 +qed
   8.762 +
   8.763 +lemma (in algebra) inf_measure_countably_subadditive:
   8.764 +  assumes posf: "positive M f" and inc: "increasing M f" 
   8.765 +  shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
   8.766 +                  (\<lambda>x. Inf (measure_set M f x))"
   8.767 +proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
   8.768 +  fix A :: "nat \<Rightarrow> 'a set" and e :: real
   8.769 +    assume A: "range A \<subseteq> Pow (space M)"
   8.770 +       and disj: "disjoint_family A"
   8.771 +       and sb: "(\<Union>i. A i) \<subseteq> space M"
   8.772 +       and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
   8.773 +       and e: "0 < e"
   8.774 +    have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
   8.775 +                    (f o B) sums l \<and>
   8.776 +                    l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   8.777 +      apply (rule inf_measure_close [OF posf])
   8.778 +      apply (metis e half mult_pos_pos zero_less_power) 
   8.779 +      apply (metis UNIV_I UN_subset_iff sb)
   8.780 +      done
   8.781 +    hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   8.782 +                       A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
   8.783 +                       ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   8.784 +      by (rule choice2)
   8.785 +    then obtain BB ll
   8.786 +      where BB: "!!n. (range (BB n) \<subseteq> sets M)"
   8.787 +        and disjBB: "!!n. disjoint_family (BB n)" 
   8.788 +        and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
   8.789 +        and BBsums: "!!n. (f o BB n) sums ll n"
   8.790 +        and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   8.791 +      by auto blast
   8.792 +    have llpos: "!!n. 0 \<le> ll n"
   8.793 +	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
   8.794 +              range_subsetD BB) 
   8.795 +    have sll: "summable ll &
   8.796 +               suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
   8.797 +      proof -
   8.798 +	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
   8.799 +	  by (rule sums_mult [OF power_half_series]) 
   8.800 +	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
   8.801 +	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
   8.802 +	  by (auto simp add: sums_iff) 
   8.803 +	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
   8.804 +                 suminf (\<lambda>n. e * (1/2)^(Suc n)) =
   8.805 +                 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
   8.806 +	  by (rule suminf_add [OF sum1 sum0]) 
   8.807 +	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
   8.808 +	  by (metis ll llpos abs_of_nonneg)
   8.809 +	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
   8.810 +	  by (rule summable_add [OF sum1 sum0]) 
   8.811 +	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
   8.812 +	  using Series.summable_le2 [OF 1 2] by auto
   8.813 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
   8.814 +                         (\<Sum>n. e * (1 / 2) ^ Suc n)"
   8.815 +	  by (metis 0) 
   8.816 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
   8.817 +	  by (simp add: eqe) 
   8.818 +	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
   8.819 +      qed
   8.820 +    def C \<equiv> "(split BB) o nat_to_nat2"
   8.821 +    have C: "!!n. C n \<in> sets M"
   8.822 +      apply (rule_tac p="nat_to_nat2 n" in PairE)
   8.823 +      apply (simp add: C_def)
   8.824 +      apply (metis BB subsetD rangeI)  
   8.825 +      done
   8.826 +    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   8.827 +      proof (auto simp add: C_def)
   8.828 +	fix x i
   8.829 +	assume x: "x \<in> A i"
   8.830 +	with sbBB [of i] obtain j where "x \<in> BB i j"
   8.831 +	  by blast	  
   8.832 +	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
   8.833 +	  by (metis nat_to_nat2_surj internal_split_def prod.cases 
   8.834 +                prod_case_split surj_f_inv_f)
   8.835 +      qed 
   8.836 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
   8.837 +      by (rule ext)  (auto simp add: C_def) 
   8.838 +    also have "... sums suminf ll" 
   8.839 +      proof (rule suminf_2dimen)
   8.840 +	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
   8.841 +	  by (force simp add: positive_def)
   8.842 +	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
   8.843 +	  by (force simp add: o_def)
   8.844 +	show "summable ll" using sll
   8.845 +	  by auto
   8.846 +      qed
   8.847 +    finally have Csums: "(f \<circ> C) sums suminf ll" .
   8.848 +    have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
   8.849 +      apply (rule inf_measure_le [OF posf inc], auto)
   8.850 +      apply (rule_tac x="C" in exI)
   8.851 +      apply (auto simp add: C sbC Csums) 
   8.852 +      done
   8.853 +    also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
   8.854 +      by blast
   8.855 +    finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> 
   8.856 +          (\<Sum>n. Inf (measure_set M f (A n))) + e" .
   8.857 +qed
   8.858 +
   8.859 +lemma (in algebra) inf_measure_outer:
   8.860 +  "positive M f \<Longrightarrow> increasing M f 
   8.861 +   \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
   8.862 +                          (\<lambda>x. Inf (measure_set M f x))"
   8.863 +  by (simp add: outer_measure_space_def inf_measure_positive
   8.864 +                inf_measure_increasing inf_measure_countably_subadditive) 
   8.865 +
   8.866 +(*MOVE UP*)
   8.867 +
   8.868 +lemma (in algebra) algebra_subset_lambda_system:
   8.869 +  assumes posf: "positive M f" and inc: "increasing M f" 
   8.870 +      and add: "additive M f"
   8.871 +  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
   8.872 +                                (\<lambda>x. Inf (measure_set M f x))"
   8.873 +proof (auto dest: sets_into_space 
   8.874 +            simp add: algebra.lambda_system_eq [OF algebra_Pow]) 
   8.875 +  fix x s
   8.876 +  assume x: "x \<in> sets M"
   8.877 +     and s: "s \<subseteq> space M"
   8.878 +  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s 
   8.879 +    by blast
   8.880 +  have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   8.881 +        \<le> Inf (measure_set M f s)"
   8.882 +    proof (rule field_le_epsilon) 
   8.883 +      fix e :: real
   8.884 +      assume e: "0 < e"
   8.885 +      from inf_measure_close [OF posf e s]
   8.886 +      obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   8.887 +                   and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
   8.888 +	           and l: "l \<le> Inf (measure_set M f s) + e"
   8.889 +	by auto
   8.890 +      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   8.891 +                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   8.892 +	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   8.893 +      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   8.894 +	by (subst additiveD [OF add, symmetric])
   8.895 + 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   8.896 +      have fsumb: "summable (f \<circ> A)"
   8.897 +	by (metis fsums sums_iff) 
   8.898 +      { fix u
   8.899 +	assume u: "u \<in> sets M"
   8.900 +	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
   8.901 +	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
   8.902 +                        u Int  range_subsetD [OF A]) 
   8.903 +	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
   8.904 +          by (rule summable_comparison_test [OF _ fsumb]) simp
   8.905 +	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
   8.906 +          proof (rule Inf_lower) 
   8.907 +            show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
   8.908 +              apply (simp add: measure_set_def) 
   8.909 +              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) 
   8.910 +              apply (auto simp add: disjoint_family_subset [OF disj])
   8.911 +              apply (blast intro: u range_subsetD [OF A]) 
   8.912 +              apply (blast dest: subsetD [OF sUN])
   8.913 +              apply (metis 1 o_assoc sums_iff) 
   8.914 +              done
   8.915 +          next
   8.916 +            show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
   8.917 +              by (blast intro: inf_measure_pos0 [OF posf]) 
   8.918 +            qed
   8.919 +          note 1 2
   8.920 +      } note lesum = this
   8.921 +      have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
   8.922 +        and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
   8.923 +        and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   8.924 +        and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) 
   8.925 +                   \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   8.926 +	by (metis Diff lesum top x)+
   8.927 +      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   8.928 +           \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
   8.929 +	by (simp add: x)
   8.930 +      also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] 
   8.931 +	by (simp add: x) (simp add: o_def) 
   8.932 +      also have "... \<le> Inf (measure_set M f s) + e"
   8.933 +	by (metis fsums l sums_unique) 
   8.934 +      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   8.935 +        \<le> Inf (measure_set M f s) + e" .
   8.936 +    qed
   8.937 +  moreover 
   8.938 +  have "Inf (measure_set M f s)
   8.939 +       \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   8.940 +    proof -
   8.941 +    have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
   8.942 +      by (metis Un_Diff_Int Un_commute)
   8.943 +    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" 
   8.944 +      apply (rule subadditiveD) 
   8.945 +      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
   8.946 +	       inf_measure_positive inf_measure_countably_subadditive posf inc)
   8.947 +      apply (auto simp add: subsetD [OF s])  
   8.948 +      done
   8.949 +    finally show ?thesis .
   8.950 +    qed
   8.951 +  ultimately 
   8.952 +  show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   8.953 +        = Inf (measure_set M f s)"
   8.954 +    by (rule order_antisym)
   8.955 +qed
   8.956 +
   8.957 +lemma measure_down:
   8.958 +     "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
   8.959 +      (measure M = measure N) \<Longrightarrow> measure_space M"
   8.960 +  by (simp add: measure_space_def measure_space_axioms_def positive_def 
   8.961 +                countably_additive_def) 
   8.962 +     blast
   8.963 +
   8.964 +theorem (in algebra) caratheodory:
   8.965 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   8.966 +  shows "\<exists>MS :: 'a measure_space. 
   8.967 +             (\<forall>s \<in> sets M. measure MS s = f s) \<and>
   8.968 +             ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
   8.969 +             measure_space MS" 
   8.970 +  proof -
   8.971 +    have inc: "increasing M f"
   8.972 +      by (metis additive_increasing ca countably_additive_additive posf) 
   8.973 +    let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
   8.974 +    def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
   8.975 +    have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)"
   8.976 +      using sigma_algebra.caratheodory_lemma
   8.977 +              [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
   8.978 +      by (simp add: ls_def)
   8.979 +    hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)"
   8.980 +      by (simp add: measure_space_def) 
   8.981 +    have "sets M \<subseteq> ls" 
   8.982 +      by (simp add: ls_def)
   8.983 +         (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
   8.984 +    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" 
   8.985 +      using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
   8.986 +      by simp
   8.987 +    have "measure_space (|space = space M, 
   8.988 +                          sets = sigma_sets (space M) (sets M),
   8.989 +                          measure = ?infm|)"
   8.990 +      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) 
   8.991 +         (simp_all add: sgs_sb space_closed)
   8.992 +    thus ?thesis
   8.993 +      by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) 
   8.994 +qed
   8.995 +
   8.996 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Probability/Measure.thy	Wed Oct 28 11:43:06 2009 +0000
     9.3 @@ -0,0 +1,916 @@
     9.4 +header {*Measures*}
     9.5 +
     9.6 +theory Measure
     9.7 +  imports Caratheodory FuncSet
     9.8 +begin
     9.9 +
    9.10 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    9.11 +
    9.12 +definition prod_sets where
    9.13 +  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
    9.14 +
    9.15 +lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
    9.16 +  by (auto simp add: prod_sets_def) 
    9.17 +
    9.18 +definition
    9.19 +  closed_cdi  where
    9.20 +  "closed_cdi M \<longleftrightarrow>
    9.21 +   sets M \<subseteq> Pow (space M) &
    9.22 +   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
    9.23 +   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
    9.24 +        (\<Union>i. A i) \<in> sets M) &
    9.25 +   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
    9.26 +
    9.27 +
    9.28 +inductive_set
    9.29 +  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
    9.30 +  for M
    9.31 +  where
    9.32 +    Basic [intro]: 
    9.33 +      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
    9.34 +  | Compl [intro]:
    9.35 +      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
    9.36 +  | Inc:
    9.37 +      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
    9.38 +       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
    9.39 +  | Disj:
    9.40 +      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
    9.41 +       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
    9.42 +  monos Pow_mono
    9.43 +
    9.44 +
    9.45 +definition
    9.46 +  smallest_closed_cdi  where
    9.47 +  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
    9.48 +
    9.49 +definition
    9.50 +  measurable  where
    9.51 +  "measurable a b = {f . sigma_algebra a & sigma_algebra b &
    9.52 +			 f \<in> (space a -> space b) &
    9.53 +			 (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
    9.54 +
    9.55 +definition
    9.56 +  measure_preserving  where
    9.57 +  "measure_preserving m1 m2 =
    9.58 +     measurable m1 m2 \<inter> 
    9.59 +     {f . measure_space m1 & measure_space m2 &
    9.60 +          (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (space m1)) = measure m2 y)}"
    9.61 +
    9.62 +lemma space_smallest_closed_cdi [simp]:
    9.63 +     "space (smallest_closed_cdi M) = space M"
    9.64 +  by (simp add: smallest_closed_cdi_def)
    9.65 +
    9.66 +
    9.67 +lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
    9.68 +  by (auto simp add: smallest_closed_cdi_def) 
    9.69 +
    9.70 +lemma (in algebra) smallest_ccdi_sets:
    9.71 +     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
    9.72 +  apply (rule subsetI) 
    9.73 +  apply (erule smallest_ccdi_sets.induct) 
    9.74 +  apply (auto intro: range_subsetD dest: sets_into_space)
    9.75 +  done
    9.76 +
    9.77 +lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
    9.78 +  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
    9.79 +  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
    9.80 +  done
    9.81 +
    9.82 +lemma (in algebra) smallest_closed_cdi3:
    9.83 +     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
    9.84 +  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 
    9.85 +
    9.86 +lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
    9.87 +  by (simp add: closed_cdi_def) 
    9.88 +
    9.89 +lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
    9.90 +  by (simp add: closed_cdi_def) 
    9.91 +
    9.92 +lemma closed_cdi_Inc:
    9.93 +     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
    9.94 +        (\<Union>i. A i) \<in> sets M"
    9.95 +  by (simp add: closed_cdi_def) 
    9.96 +
    9.97 +lemma closed_cdi_Disj:
    9.98 +     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    9.99 +  by (simp add: closed_cdi_def) 
   9.100 +
   9.101 +lemma closed_cdi_Un:
   9.102 +  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
   9.103 +      and A: "A \<in> sets M" and B: "B \<in> sets M"
   9.104 +      and disj: "A \<inter> B = {}"
   9.105 +    shows "A \<union> B \<in> sets M"
   9.106 +proof -
   9.107 +  have ra: "range (binaryset A B) \<subseteq> sets M"
   9.108 +   by (simp add: range_binaryset_eq empty A B) 
   9.109 + have di:  "disjoint_family (binaryset A B)" using disj
   9.110 +   by (simp add: disjoint_family_def binaryset_def Int_commute) 
   9.111 + from closed_cdi_Disj [OF cdi ra di]
   9.112 + show ?thesis
   9.113 +   by (simp add: UN_binaryset_eq) 
   9.114 +qed
   9.115 +
   9.116 +lemma (in algebra) smallest_ccdi_sets_Un:
   9.117 +  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
   9.118 +      and disj: "A \<inter> B = {}"
   9.119 +    shows "A \<union> B \<in> smallest_ccdi_sets M"
   9.120 +proof -
   9.121 +  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
   9.122 +    by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
   9.123 +  have di:  "disjoint_family (binaryset A B)" using disj
   9.124 +    by (simp add: disjoint_family_def binaryset_def Int_commute) 
   9.125 +  from Disj [OF ra di]
   9.126 +  show ?thesis
   9.127 +    by (simp add: UN_binaryset_eq) 
   9.128 +qed
   9.129 +
   9.130 +
   9.131 +
   9.132 +lemma (in algebra) smallest_ccdi_sets_Int1:
   9.133 +  assumes a: "a \<in> sets M"
   9.134 +  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
   9.135 +proof (induct rule: smallest_ccdi_sets.induct)
   9.136 +  case (Basic x)
   9.137 +  thus ?case
   9.138 +    by (metis a Int smallest_ccdi_sets.Basic)
   9.139 +next
   9.140 +  case (Compl x)
   9.141 +  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
   9.142 +    by blast
   9.143 +  also have "... \<in> smallest_ccdi_sets M" 
   9.144 +    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
   9.145 +           Diff_disjoint Int_Diff Int_empty_right Un_commute
   9.146 +           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
   9.147 +           smallest_ccdi_sets_Un) 
   9.148 +  finally show ?case .
   9.149 +next
   9.150 +  case (Inc A)
   9.151 +  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
   9.152 +    by blast
   9.153 +  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
   9.154 +    by blast
   9.155 +  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
   9.156 +    by (simp add: Inc) 
   9.157 +  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
   9.158 +    by blast
   9.159 +  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
   9.160 +    by (rule smallest_ccdi_sets.Inc) 
   9.161 +  show ?case
   9.162 +    by (metis 1 2)
   9.163 +next
   9.164 +  case (Disj A)
   9.165 +  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
   9.166 +    by blast
   9.167 +  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
   9.168 +    by blast
   9.169 +  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
   9.170 +    by (auto simp add: disjoint_family_def) 
   9.171 +  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
   9.172 +    by (rule smallest_ccdi_sets.Disj) 
   9.173 +  show ?case
   9.174 +    by (metis 1 2)
   9.175 +qed
   9.176 +
   9.177 +
   9.178 +lemma (in algebra) smallest_ccdi_sets_Int:
   9.179 +  assumes b: "b \<in> smallest_ccdi_sets M"
   9.180 +  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
   9.181 +proof (induct rule: smallest_ccdi_sets.induct)
   9.182 +  case (Basic x)
   9.183 +  thus ?case
   9.184 +    by (metis b smallest_ccdi_sets_Int1)
   9.185 +next
   9.186 +  case (Compl x)
   9.187 +  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
   9.188 +    by blast
   9.189 +  also have "... \<in> smallest_ccdi_sets M"
   9.190 +    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b 
   9.191 +           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) 
   9.192 +  finally show ?case .
   9.193 +next
   9.194 +  case (Inc A)
   9.195 +  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
   9.196 +    by blast
   9.197 +  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
   9.198 +    by blast
   9.199 +  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
   9.200 +    by (simp add: Inc) 
   9.201 +  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
   9.202 +    by blast
   9.203 +  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
   9.204 +    by (rule smallest_ccdi_sets.Inc) 
   9.205 +  show ?case
   9.206 +    by (metis 1 2)
   9.207 +next
   9.208 +  case (Disj A)
   9.209 +  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
   9.210 +    by blast
   9.211 +  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
   9.212 +    by blast
   9.213 +  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
   9.214 +    by (auto simp add: disjoint_family_def) 
   9.215 +  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
   9.216 +    by (rule smallest_ccdi_sets.Disj) 
   9.217 +  show ?case
   9.218 +    by (metis 1 2)
   9.219 +qed
   9.220 +
   9.221 +lemma (in algebra) sets_smallest_closed_cdi_Int:
   9.222 +   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
   9.223 +    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
   9.224 +  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) 
   9.225 +
   9.226 +lemma algebra_iff_Int:
   9.227 +     "algebra M \<longleftrightarrow> 
   9.228 +       sets M \<subseteq> Pow (space M) & {} \<in> sets M & 
   9.229 +       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   9.230 +       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
   9.231 +proof (auto simp add: algebra.Int, auto simp add: algebra_def)
   9.232 +  fix a b
   9.233 +  assume ab: "sets M \<subseteq> Pow (space M)"
   9.234 +             "\<forall>a\<in>sets M. space M - a \<in> sets M" 
   9.235 +             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
   9.236 +             "a \<in> sets M" "b \<in> sets M"
   9.237 +  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
   9.238 +    by blast
   9.239 +  also have "... \<in> sets M"
   9.240 +    by (metis ab)
   9.241 +  finally show "a \<union> b \<in> sets M" .
   9.242 +qed
   9.243 +
   9.244 +lemma (in algebra) sigma_property_disjoint_lemma:
   9.245 +  assumes sbC: "sets M \<subseteq> C"
   9.246 +      and ccdi: "closed_cdi (|space = space M, sets = C|)"
   9.247 +  shows "sigma_sets (space M) (sets M) \<subseteq> C"
   9.248 +proof -
   9.249 +  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
   9.250 +    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int 
   9.251 +            smallest_ccdi_sets_Int)
   9.252 +    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) 
   9.253 +    apply (blast intro: smallest_ccdi_sets.Disj) 
   9.254 +    done
   9.255 +  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
   9.256 +    by auto 
   9.257 +       (metis sigma_algebra.sigma_sets_subset algebra.simps(1) 
   9.258 +          algebra.simps(2) subsetD) 
   9.259 +  also have "...  \<subseteq> C"
   9.260 +    proof
   9.261 +      fix x
   9.262 +      assume x: "x \<in> smallest_ccdi_sets M"
   9.263 +      thus "x \<in> C"
   9.264 +	proof (induct rule: smallest_ccdi_sets.induct)
   9.265 +	  case (Basic x)
   9.266 +	  thus ?case
   9.267 +	    by (metis Basic subsetD sbC)
   9.268 +	next
   9.269 +	  case (Compl x)
   9.270 +	  thus ?case
   9.271 +	    by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
   9.272 + 	next
   9.273 +	  case (Inc A)
   9.274 +	  thus ?case
   9.275 +	       by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
   9.276 +	next
   9.277 +	  case (Disj A)
   9.278 +	  thus ?case
   9.279 +	       by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
   9.280 +	qed
   9.281 +    qed
   9.282 +  finally show ?thesis .
   9.283 +qed
   9.284 +
   9.285 +lemma (in algebra) sigma_property_disjoint:
   9.286 +  assumes sbC: "sets M \<subseteq> C"
   9.287 +      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
   9.288 +      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
   9.289 +                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) 
   9.290 +                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
   9.291 +      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
   9.292 +                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
   9.293 +  shows "sigma_sets (space M) (sets M) \<subseteq> C"
   9.294 +proof -
   9.295 +  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 
   9.296 +    proof (rule sigma_property_disjoint_lemma) 
   9.297 +      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
   9.298 +	by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
   9.299 +    next
   9.300 +      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
   9.301 +	by (simp add: closed_cdi_def compl inc disj)
   9.302 +           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
   9.303 +	     IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
   9.304 +    qed
   9.305 +  thus ?thesis
   9.306 +    by blast
   9.307 +qed
   9.308 +
   9.309 +
   9.310 +(* or just countably_additiveD [OF measure_space.ca] *)
   9.311 +lemma (in measure_space) measure_countably_additive:
   9.312 +    "range A \<subseteq> sets M
   9.313 +     \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
   9.314 +     \<Longrightarrow> (measure M o A)  sums  measure M (\<Union>i. A i)"
   9.315 +  by (insert ca) (simp add: countably_additive_def o_def) 
   9.316 +
   9.317 +lemma (in measure_space) additive:
   9.318 +     "additive M (measure M)"
   9.319 +proof (rule algebra.countably_additive_additive [OF _ _ ca]) 
   9.320 +  show "algebra M"
   9.321 +    by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
   9.322 +  show "positive M (measure M)"
   9.323 +    by (simp add: positive_def empty_measure positive) 
   9.324 +qed
   9.325 + 
   9.326 +lemma (in measure_space) measure_additive:
   9.327 +     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} 
   9.328 +      \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
   9.329 +  by (metis additiveD additive)
   9.330 +
   9.331 +lemma (in measure_space) measure_compl:
   9.332 +  assumes s: "s \<in> sets M"
   9.333 +  shows "measure M (space M - s) = measure M (space M) - measure M s"
   9.334 +proof -
   9.335 +  have "measure M (space M) = measure M (s \<union> (space M - s))" using s
   9.336 +    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
   9.337 +  also have "... = measure M s + measure M (space M - s)"
   9.338 +    by (rule additiveD [OF additive]) (auto simp add: s) 
   9.339 +  finally have "measure M (space M) = measure M s + measure M (space M - s)" .
   9.340 +  thus ?thesis
   9.341 +    by arith
   9.342 +qed
   9.343 +
   9.344 +lemma disjoint_family_Suc:
   9.345 +  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
   9.346 +  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
   9.347 +proof -
   9.348 +  {
   9.349 +    fix m
   9.350 +    have "!!n. A n \<subseteq> A (m+n)" 
   9.351 +    proof (induct m)
   9.352 +      case 0 show ?case by simp
   9.353 +    next
   9.354 +      case (Suc m) thus ?case
   9.355 +	by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
   9.356 +    qed
   9.357 +  }
   9.358 +  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
   9.359 +    by (metis add_commute le_add_diff_inverse nat_less_le)
   9.360 +  thus ?thesis
   9.361 +    by (auto simp add: disjoint_family_def)
   9.362 +      (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) 
   9.363 +qed
   9.364 +
   9.365 +
   9.366 +lemma (in measure_space) measure_countable_increasing:
   9.367 +  assumes A: "range A \<subseteq> sets M"
   9.368 +      and A0: "A 0 = {}"
   9.369 +      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   9.370 +  shows "(measure M o A) ----> measure M (\<Union>i. A i)"
   9.371 +proof -
   9.372 +  {
   9.373 +    fix n
   9.374 +    have "(measure M \<circ> A) n =
   9.375 +          setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
   9.376 +      proof (induct n)
   9.377 +	case 0 thus ?case by (auto simp add: A0 empty_measure)
   9.378 +      next
   9.379 +	case (Suc m) 
   9.380 +	have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
   9.381 +	  by (metis ASuc Un_Diff_cancel Un_absorb1)
   9.382 +	hence "measure M (A (Suc m)) =
   9.383 +               measure M (A m) + measure M (A (Suc m) - A m)" 
   9.384 +	  by (subst measure_additive) 
   9.385 +             (auto simp add: measure_additive range_subsetD [OF A]) 
   9.386 +	with Suc show ?case
   9.387 +	  by simp
   9.388 +      qed
   9.389 +  }
   9.390 +  hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
   9.391 +    by (blast intro: ext) 
   9.392 +  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
   9.393 +    proof (rule UN_finite2_eq [where k=1], simp) 
   9.394 +      fix i
   9.395 +      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
   9.396 +	proof (induct i)
   9.397 +	  case 0 thus ?case by (simp add: A0)
   9.398 +	next
   9.399 +	  case (Suc i) 
   9.400 +	  thus ?case
   9.401 +	    by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
   9.402 +	qed
   9.403 +    qed
   9.404 +  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
   9.405 +    by (metis A Diff range_subsetD)
   9.406 +  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
   9.407 +    by (blast intro: countable_UN range_subsetD [OF A])  
   9.408 +  have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
   9.409 +    by (rule measure_countably_additive) 
   9.410 +       (auto simp add: disjoint_family_Suc ASuc A1 A2)
   9.411 +  also have "... =  measure M (\<Union>i. A i)"
   9.412 +    by (simp add: Aeq) 
   9.413 +  finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A i)" .
   9.414 +  thus ?thesis
   9.415 +    by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf) 
   9.416 +qed
   9.417 +
   9.418 +lemma (in measure_space) monotone_convergence:
   9.419 +  assumes A: "range A \<subseteq> sets M"
   9.420 +      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   9.421 +  shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
   9.422 +proof -
   9.423 +  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)" 
   9.424 +    by (auto simp add: split: nat.splits) 
   9.425 +  have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
   9.426 +    by (rule ext) simp
   9.427 +  have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)" 
   9.428 +    by (rule measure_countable_increasing) 
   9.429 +       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) 
   9.430 +  also have "... = measure M (\<Union>i. A i)" 
   9.431 +    by (simp add: ueq) 
   9.432 +  finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
   9.433 +  thus ?thesis using meq
   9.434 +    by (metis LIMSEQ_Suc)
   9.435 +qed
   9.436 +
   9.437 +lemma measurable_sigma_preimages:
   9.438 +  assumes a: "sigma_algebra a" and b: "sigma_algebra b"
   9.439 +      and f: "f \<in> space a -> space b"
   9.440 +      and ba: "!!y. y \<in> sets b ==> f -` y \<in> sets a"
   9.441 +  shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)"
   9.442 +proof (simp add: sigma_algebra_iff2, intro conjI) 
   9.443 +  show "op -` f ` sets b \<subseteq> Pow (space a)"
   9.444 +    by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI) 
   9.445 +next
   9.446 +  show "{} \<in> op -` f ` sets b"
   9.447 +    by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
   9.448 +next
   9.449 +  { fix y
   9.450 +    assume y: "y \<in> sets b"
   9.451 +    with a b f
   9.452 +    have "space a - f -` y = f -` (space b - y)"
   9.453 +      by (auto simp add: sigma_algebra_iff2) (blast intro: ba) 
   9.454 +    hence "space a - (f -` y) \<in> (vimage f) ` sets b"
   9.455 +      by auto
   9.456 +         (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
   9.457 +                sigma_sets.Compl) 
   9.458 +  } 
   9.459 +  thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
   9.460 +    by blast
   9.461 +next
   9.462 +  {
   9.463 +    fix A:: "nat \<Rightarrow> 'a set"
   9.464 +    assume A: "range A \<subseteq> (vimage f) ` (sets b)"
   9.465 +    have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
   9.466 +      proof -
   9.467 +	def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
   9.468 +	{ 
   9.469 +	  fix i
   9.470 +	  have "A i \<in> (vimage f) ` (sets b)" using A
   9.471 +	    by blast
   9.472 +	  hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
   9.473 +	    by blast
   9.474 +	  hence "B i \<in> sets b \<and> f -` B i = A i" 
   9.475 +	    by (simp add: B_def) (erule someI_ex)
   9.476 +	} note B = this
   9.477 +	show ?thesis
   9.478 +	  proof
   9.479 +	    show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
   9.480 +	      by (simp add: vimage_UN B) 
   9.481 +	   show "(\<Union>i. B i) \<in> sets b" using B
   9.482 +	     by (auto intro: sigma_algebra.countable_UN [OF b]) 
   9.483 +	  qed
   9.484 +      qed
   9.485 +  }
   9.486 +  thus "\<forall>A::nat \<Rightarrow> 'a set.
   9.487 +           range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
   9.488 +    by blast
   9.489 +qed
   9.490 +
   9.491 +lemma (in sigma_algebra) measurable_sigma:
   9.492 +  assumes B: "B \<subseteq> Pow X" 
   9.493 +      and f: "f \<in> space M -> X"
   9.494 +      and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
   9.495 +  shows "f \<in> measurable M (sigma X B)"
   9.496 +proof -
   9.497 +  have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
   9.498 +    proof clarify
   9.499 +      fix x
   9.500 +      assume "x \<in> sigma_sets X B"
   9.501 +      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
   9.502 +	proof induct
   9.503 +	  case (Basic a)
   9.504 +	  thus ?case
   9.505 +	    by (auto simp add: ba) (metis B subsetD PowD) 
   9.506 +        next
   9.507 +	  case Empty
   9.508 +	  thus ?case
   9.509 +	    by auto
   9.510 +        next
   9.511 +	  case (Compl a)
   9.512 +	  have [simp]: "f -` X \<inter> space M = space M"
   9.513 +	    by (auto simp add: funcset_mem [OF f]) 
   9.514 +	  thus ?case
   9.515 +	    by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
   9.516 +	next
   9.517 +	  case (Union a)
   9.518 +	  thus ?case
   9.519 +	    by (simp add: vimage_UN, simp only: UN_extend_simps(4))
   9.520 +	       (blast intro: countable_UN)
   9.521 +	qed
   9.522 +    qed
   9.523 +  thus ?thesis
   9.524 +    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 
   9.525 +       (auto simp add: sigma_def) 
   9.526 +qed
   9.527 +
   9.528 +lemma measurable_subset:
   9.529 +     "measurable a b \<subseteq> measurable a (sigma (space b) (sets b))"
   9.530 +  apply clarify
   9.531 +  apply (rule sigma_algebra.measurable_sigma) 
   9.532 +  apply (auto simp add: measurable_def)
   9.533 +  apply (metis algebra.sets_into_space subsetD sigma_algebra_iff) 
   9.534 +  done
   9.535 +
   9.536 +lemma measurable_eqI: 
   9.537 +     "space m1 = space m1' \<Longrightarrow> space m2 = space m2'
   9.538 +      \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
   9.539 +      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   9.540 +  by (simp add: measurable_def sigma_algebra_iff2) 
   9.541 +
   9.542 +lemma measure_preserving_lift:
   9.543 +  fixes f :: "'a1 \<Rightarrow> 'a2" 
   9.544 +    and m1 :: "('a1, 'b1) measure_space_scheme"
   9.545 +    and m2 :: "('a2, 'b2) measure_space_scheme"
   9.546 +  assumes m1: "measure_space m1" and m2: "measure_space m2" 
   9.547 +  defines "m x \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
   9.548 +  assumes setsm2: "sets m2 = sigma_sets (space m2) a"
   9.549 +      and fmp: "f \<in> measure_preserving m1 (m a)"
   9.550 +  shows "f \<in> measure_preserving m1 m2"
   9.551 +proof -
   9.552 +  have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2"
   9.553 +    by (simp add: m_def) 
   9.554 +  have sa1: "sigma_algebra m1" using m1 
   9.555 +    by (simp add: measure_space_def) 
   9.556 +  show ?thesis using fmp
   9.557 +    proof (clarsimp simp add: measure_preserving_def m1 m2) 
   9.558 +      assume fm: "f \<in> measurable m1 (m a)" 
   9.559 +	 and mam: "measure_space (m a)"
   9.560 +	 and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
   9.561 +      have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
   9.562 +	by (rule subsetD [OF measurable_subset fm]) 
   9.563 +      also have "... = measurable m1 m2"
   9.564 +	by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
   9.565 +      finally have f12: "f \<in> measurable m1 m2" .
   9.566 +      hence ffn: "f \<in> space m1 \<rightarrow> space m2"
   9.567 +	by (simp add: measurable_def) 
   9.568 +      have "space m1 \<subseteq> f -` (space m2)"
   9.569 +	by auto (metis PiE ffn)
   9.570 +      hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
   9.571 +	by blast
   9.572 +      {
   9.573 +	fix y
   9.574 +	assume y: "y \<in> sets m2" 
   9.575 +	have ama: "algebra (m a)"  using mam
   9.576 +	  by (simp add: measure_space_def sigma_algebra_iff) 
   9.577 +	have spa: "space m2 \<in> a" using algebra.top [OF ama]
   9.578 +	  by (simp add: m_def) 
   9.579 +	have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
   9.580 +	  by (simp add: m_def) 
   9.581 +	also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
   9.582 +	  proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
   9.583 +	    fix x
   9.584 +	    assume x: "x \<in> a"
   9.585 +	    thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
   9.586 +	      by (simp add: meq)
   9.587 +	  next
   9.588 +	    fix s
   9.589 +	    assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
   9.590 +	       and s: "s \<in> sigma_sets (space m2) a"
   9.591 +	    hence s2: "s \<in> sets m2"
   9.592 +	      by (simp add: setsm2) 
   9.593 +	    thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
   9.594 +                  measure m2 (space m2 - s)" using f12
   9.595 +	      by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
   9.596 +		    measure_space.measure_compl measurable_def)  
   9.597 +	         (metis fveq meq spa) 
   9.598 +	  next
   9.599 +	    fix A
   9.600 +	      assume A0: "A 0 = {}"
   9.601 +	 	 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   9.602 +		 and rA1: "range A \<subseteq> 
   9.603 +		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
   9.604 +		 and "range A \<subseteq> sigma_sets (space m2) a"
   9.605 +	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
   9.606 +	      have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
   9.607 +		using rA1 by blast
   9.608 +	      have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
   9.609 +		by (simp add: o_def eq1) 
   9.610 +	      also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
   9.611 +		proof (rule measure_space.measure_countable_increasing [OF m1])
   9.612 +		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
   9.613 +		    using f12 rA2 by (auto simp add: measurable_def)
   9.614 +		  show "f -` A 0 \<inter> space m1 = {}" using A0
   9.615 +		    by blast
   9.616 +		  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
   9.617 +		    using ASuc by auto
   9.618 +		qed
   9.619 +	      also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
   9.620 +		by (simp add: vimage_UN)
   9.621 +	      finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
   9.622 +	      moreover
   9.623 +	      have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
   9.624 +		by (rule measure_space.measure_countable_increasing 
   9.625 +		          [OF m2 rA2, OF A0 ASuc])
   9.626 +	      ultimately 
   9.627 +	      show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
   9.628 +                    measure m2 (\<Union>i. A i)"
   9.629 +		by (rule LIMSEQ_unique) 
   9.630 +	  next
   9.631 +	    fix A :: "nat => 'a2 set"
   9.632 +	      assume dA: "disjoint_family A"
   9.633 +		 and rA1: "range A \<subseteq> 
   9.634 +		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
   9.635 +		 and "range A \<subseteq> sigma_sets (space m2) a"
   9.636 +	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
   9.637 +	      hence Um2: "(\<Union>i. A i) \<in> sets m2"
   9.638 +		by (metis range_subsetD setsm2 sigma_sets.Union)
   9.639 +	      have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
   9.640 +		using rA1 by blast
   9.641 +	      hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
   9.642 +		by (simp add: o_def) 
   9.643 +	      also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
   9.644 +		proof (rule measure_space.measure_countably_additive [OF m1] )
   9.645 +		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
   9.646 +		    using f12 rA2 by (auto simp add: measurable_def)
   9.647 +		  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
   9.648 +		    by (auto simp add: disjoint_family_def) 
   9.649 +		  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
   9.650 +		    proof (rule sigma_algebra.countable_UN [OF sa1])
   9.651 +		      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
   9.652 +			by (auto simp add: measurable_def) 
   9.653 +		    qed
   9.654 + 		qed
   9.655 +	      finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
   9.656 +	      with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
   9.657 +	      have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
   9.658 +		by (metis sums_unique) 
   9.659 +
   9.660 +	      moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
   9.661 +		by (simp add: vimage_UN)
   9.662 +	      ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
   9.663 +                    measure m2 (\<Union>i. A i)" 
   9.664 +		by metis
   9.665 +	  qed
   9.666 +	finally have "sigma_sets (space m2) a 
   9.667 +              \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
   9.668 +	hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
   9.669 +	  by (force simp add: setsm2) 
   9.670 +      }
   9.671 +      thus "f \<in> measurable m1 m2 \<and>
   9.672 +       (\<forall>y\<in>sets m2.
   9.673 +           measure m1 (f -` y \<inter> space m1) = measure m2 y)"
   9.674 +	by (blast intro: f12) 
   9.675 +    qed
   9.676 +qed
   9.677 +
   9.678 +lemma measurable_ident:
   9.679 +     "sigma_algebra M ==> id \<in> measurable M M"
   9.680 +  apply (simp add: measurable_def)
   9.681 +  apply (auto simp add: sigma_algebra_def algebra.Int algebra.top)
   9.682 +  done
   9.683 +
   9.684 +lemma measurable_comp:
   9.685 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
   9.686 +  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
   9.687 +  apply (auto simp add: measurable_def vimage_compose) 
   9.688 +  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
   9.689 +  apply force+
   9.690 +  done
   9.691 +
   9.692 + lemma measurable_strong:
   9.693 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
   9.694 +  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
   9.695 +      and c: "sigma_algebra c"
   9.696 +      and t: "f ` (space a) \<subseteq> t"
   9.697 +      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
   9.698 +  shows "(g o f) \<in> measurable a c"
   9.699 +proof -
   9.700 +  have a: "sigma_algebra a" and b: "sigma_algebra b"
   9.701 +   and fab: "f \<in> (space a -> space b)"
   9.702 +   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
   9.703 +     by (auto simp add: measurable_def)
   9.704 +  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
   9.705 +    by force
   9.706 +  show ?thesis
   9.707 +    apply (auto simp add: measurable_def vimage_compose a c) 
   9.708 +    apply (metis funcset_mem fab g) 
   9.709 +    apply (subst eq, metis ba cb) 
   9.710 +    done
   9.711 +qed
   9.712 + 
   9.713 +lemma measurable_mono1:
   9.714 +     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
   9.715 +      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
   9.716 +  by (auto simp add: measurable_def) 
   9.717 +
   9.718 +lemma measurable_up_sigma:
   9.719 +   "measurable a b \<subseteq> measurable (sigma (space a) (sets a)) b"
   9.720 +  apply (auto simp add: measurable_def) 
   9.721 +  apply (metis sigma_algebra_iff2 sigma_algebra_sigma)
   9.722 +  apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def) 
   9.723 +  done
   9.724 +
   9.725 +lemma measure_preserving_up:
   9.726 +   "f \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
   9.727 +    measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1 
   9.728 +    \<Longrightarrow> f \<in> measure_preserving m1 m2"
   9.729 +  by (auto simp add: measure_preserving_def measurable_def) 
   9.730 +
   9.731 +lemma measure_preserving_up_sigma:
   9.732 +   "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
   9.733 +    \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 
   9.734 +        \<subseteq> measure_preserving m1 m2"
   9.735 +  apply (rule subsetI) 
   9.736 +  apply (rule measure_preserving_up) 
   9.737 +  apply (simp_all add: measure_space_def sigma_def) 
   9.738 +  apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic) 
   9.739 +  done
   9.740 +
   9.741 +lemma (in sigma_algebra) measurable_prod_sigma:
   9.742 +  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
   9.743 +  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2)) 
   9.744 +                          (prod_sets (sets a1) (sets a2)))"
   9.745 +proof -
   9.746 +  from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
   9.747 +     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
   9.748 +    by (auto simp add: measurable_def) 
   9.749 +  from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
   9.750 +     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
   9.751 +    by (auto simp add: measurable_def) 
   9.752 +  show ?thesis
   9.753 +    proof (rule measurable_sigma) 
   9.754 +      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
   9.755 +        by (force simp add: prod_sets_def sigma_algebra_iff algebra_def) 
   9.756 +    next
   9.757 +      show "f \<in> space M \<rightarrow> space a1 \<times> space a2" 
   9.758 +        by (rule prod_final [OF fn1 fn2])
   9.759 +    next
   9.760 +      fix z
   9.761 +      assume z: "z \<in> prod_sets (sets a1) (sets a2)" 
   9.762 +      thus "f -` z \<inter> space M \<in> sets M"
   9.763 +        proof (auto simp add: prod_sets_def vimage_Times) 
   9.764 +          fix x y
   9.765 +          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
   9.766 +          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M = 
   9.767 +                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
   9.768 +            by blast
   9.769 +          also have "...  \<in> sets M" using x y q1 q2
   9.770 +            by blast
   9.771 +          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
   9.772 +        qed
   9.773 +    qed
   9.774 +qed
   9.775 +
   9.776 +
   9.777 +lemma (in measure_space) measurable_range_reduce:
   9.778 +   "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
   9.779 +    s \<noteq> {} 
   9.780 +    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
   9.781 +  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
   9.782 +
   9.783 +lemma (in measure_space) measurable_Pow_to_Pow:
   9.784 +   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
   9.785 +  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
   9.786 +
   9.787 +lemma (in measure_space) measurable_Pow_to_Pow_image:
   9.788 +   "sets M = Pow (space M)
   9.789 +    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
   9.790 +  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
   9.791 +
   9.792 +lemma (in measure_space) measure_real_sum_image:
   9.793 +  assumes s: "s \<in> sets M"
   9.794 +      and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
   9.795 +      and fin: "finite s"
   9.796 +  shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
   9.797 +proof -
   9.798 +  {
   9.799 +    fix u
   9.800 +    assume u: "u \<subseteq> s & u \<in> sets M"
   9.801 +    hence "finite u"
   9.802 +      by (metis fin finite_subset) 
   9.803 +    hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
   9.804 +      proof (induct u)
   9.805 +        case empty
   9.806 +        thus ?case by simp
   9.807 +      next
   9.808 +        case (insert x t)
   9.809 +        hence x: "x \<in> s" and t: "t \<subseteq> s" 
   9.810 +          by (simp_all add: insert_subset) 
   9.811 +        hence ts: "t \<in> sets M"  using insert
   9.812 +          by (metis Diff_insert_absorb Diff ssets)
   9.813 +        have "measure M (insert x t) = measure M ({x} \<union> t)"
   9.814 +          by simp
   9.815 +        also have "... = measure M {x} + measure M t" 
   9.816 +          by (simp add: measure_additive insert insert_disjoint ssets x ts 
   9.817 +                  del: Un_insert_left)
   9.818 +        also have "... = (\<Sum>x\<in>insert x t. measure M {x})" 
   9.819 +          by (simp add: x t ts insert) 
   9.820 +        finally show ?case .
   9.821 +      qed
   9.822 +    }
   9.823 +  thus ?thesis
   9.824 +    by (metis subset_refl s)
   9.825 +qed
   9.826 +  
   9.827 +lemma (in sigma_algebra) sigma_algebra_extend:
   9.828 +     "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
   9.829 +proof -
   9.830 +  have 1: "sigma_algebra M \<Longrightarrow> ?thesis"
   9.831 +    by (simp add: sigma_algebra_def algebra_def sigma_algebra_axioms_def) 
   9.832 +  show ?thesis
   9.833 +    by (rule 1) intro_locales
   9.834 +qed
   9.835 +
   9.836 +
   9.837 +lemma (in sigma_algebra) finite_additivity_sufficient:
   9.838 +  assumes fin: "finite (space M)"
   9.839 +      and posf: "positive M f" and addf: "additive M f" 
   9.840 +  defines "Mf \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
   9.841 +  shows "measure_space Mf" 
   9.842 +proof -
   9.843 +  have [simp]: "f {} = 0" using posf
   9.844 +    by (simp add: positive_def) 
   9.845 +  have "countably_additive Mf f"
   9.846 +    proof (auto simp add: countably_additive_def positive_def) 
   9.847 +      fix A :: "nat \<Rightarrow> 'a set"
   9.848 +      assume A: "range A \<subseteq> sets Mf"
   9.849 +         and disj: "disjoint_family A"
   9.850 +         and UnA: "(\<Union>i. A i) \<in> sets Mf"
   9.851 +      def I \<equiv> "{i. A i \<noteq> {}}"
   9.852 +      have "Union (A ` I) \<subseteq> space M" using A
   9.853 +        by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space) 
   9.854 +      hence "finite (A ` I)"
   9.855 +        by (metis finite_UnionD finite_subset fin) 
   9.856 +      moreover have "inj_on A I" using disj
   9.857 +        by (auto simp add: I_def disjoint_family_def inj_on_def) 
   9.858 +      ultimately have finI: "finite I"
   9.859 +        by (metis finite_imageD)
   9.860 +      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
   9.861 +        proof (cases "I = {}")
   9.862 +          case True thus ?thesis by (simp add: I_def) 
   9.863 +        next
   9.864 +          case False
   9.865 +          hence "\<forall>i\<in>I. i < Suc(Max I)"
   9.866 +            by (simp add: Max_less_iff [symmetric] finI) 
   9.867 +          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
   9.868 +            by (simp add: I_def) (metis less_le_not_le) 
   9.869 +          thus ?thesis
   9.870 +            by blast
   9.871 +        qed
   9.872 +      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
   9.873 +      hence "\<forall>m\<ge>N. (f o A) m = 0"
   9.874 +        by simp 
   9.875 +      hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}" 
   9.876 +        by (simp add: series_zero o_def) 
   9.877 +      also have "... = f (\<Union>i<N. A i)"
   9.878 +        proof (induct N)
   9.879 +          case 0 thus ?case by simp
   9.880 +        next
   9.881 +          case (Suc n) 
   9.882 +          have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
   9.883 +            proof (rule Caratheodory.additiveD [OF addf])
   9.884 +              show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
   9.885 +                by (auto simp add: disjoint_family_def nat_less_le) blast
   9.886 +              show "A n \<in> sets M" using A 
   9.887 +                by (force simp add: Mf_def) 
   9.888 +              show "(\<Union>i<n. A i) \<in> sets M"
   9.889 +                proof (induct n)
   9.890 +                  case 0 thus ?case by simp
   9.891 +                next
   9.892 +                  case (Suc n) thus ?case using A
   9.893 +                    by (simp add: lessThan_Suc Mf_def Un range_subsetD) 
   9.894 +                qed
   9.895 +            qed
   9.896 +          thus ?case using Suc
   9.897 +            by (simp add: lessThan_Suc) 
   9.898 +        qed
   9.899 +      also have "... = f (\<Union>i. A i)" 
   9.900 +        proof -
   9.901 +          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
   9.902 +            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
   9.903 +          thus ?thesis by simp
   9.904 +        qed
   9.905 +      finally show "(\<lambda>n. f (A n)) sums f (\<Union>i. A i)" .
   9.906 +    qed
   9.907 +  thus ?thesis using posf 
   9.908 +    by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def) 
   9.909 +qed
   9.910 +
   9.911 +lemma finite_additivity_sufficient:
   9.912 +     "sigma_algebra M 
   9.913 +      \<Longrightarrow> finite (space M) 
   9.914 +      \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M) 
   9.915 +      \<Longrightarrow> measure_space M"
   9.916 +  by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
   9.917 +
   9.918 +end
   9.919 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Probability/Probability.thy	Wed Oct 28 11:43:06 2009 +0000
    10.3 @@ -0,0 +1,5 @@
    10.4 +theory Probability imports
    10.5 +	Measure
    10.6 +begin
    10.7 +
    10.8 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Probability/ROOT.ML	Wed Oct 28 11:43:06 2009 +0000
    11.3 @@ -0,0 +1,6 @@
    11.4 +(*
    11.5 +  no_document use_thy "ThisTheory";
    11.6 +  use_thy "ThatTheory";
    11.7 +*)
    11.8 +
    11.9 +use_thy "Probability";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Probability/SeriesPlus.thy	Wed Oct 28 11:43:06 2009 +0000
    12.3 @@ -0,0 +1,127 @@
    12.4 +theory SeriesPlus
    12.5 +  imports Complex_Main Nat_Int_Bij 
    12.6 +
    12.7 +begin
    12.8 +
    12.9 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
   12.10 +
   12.11 +lemma choice2: "(!!x. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)"
   12.12 +  by metis
   12.13 +
   12.14 +lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
   12.15 +  by blast
   12.16 +
   12.17 +
   12.18 +lemma suminf_2dimen:
   12.19 +  fixes f:: "nat * nat \<Rightarrow> real"
   12.20 +  assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
   12.21 +      and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
   12.22 +      and sumg: "summable g"
   12.23 +  shows "(f o nat_to_nat2) sums suminf g"
   12.24 +proof (simp add: sums_def)
   12.25 +  {
   12.26 +    fix x
   12.27 +    have "0 \<le> f x"
   12.28 +      by (cases x) (simp add: f_nneg) 
   12.29 +  } note [iff]  = this
   12.30 +  have g_nneg: "!!m. 0 \<le> g m"
   12.31 +    proof -
   12.32 +      fix m
   12.33 +      have "0 \<le> suminf (\<lambda>n. f (m,n))"
   12.34 +	by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
   12.35 +      thus "0 \<le> g m" using fsums [of m] 
   12.36 +	by (auto simp add: sums_iff) 
   12.37 +    qed
   12.38 +  show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
   12.39 +  proof (rule increasing_LIMSEQ, simp add: f_nneg)
   12.40 +    fix n
   12.41 +    def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
   12.42 +    def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
   12.43 +    have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})" 
   12.44 +      by (force simp add: i_def j_def 
   12.45 +                intro: finite_imageI Max_ge finite_Domain finite_Range)  
   12.46 +    have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})" 
   12.47 +      using setsum_reindex [of nat_to_nat2 "{0..<n}" f] 
   12.48 +      by (simp add: o_def)
   12.49 +         (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj) 
   12.50 +    also have "... \<le> setsum f ({0..i} \<times> {0..j})"
   12.51 +      by (rule setsum_mono2) (auto simp add: ij) 
   12.52 +    also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
   12.53 +      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
   12.54 +	        setsum_cartesian_product split_eta) 
   12.55 +    also have "... \<le> setsum g {0..<Suc i}" 
   12.56 +      proof (rule setsum_mono, simp add: less_Suc_eq_le) 
   12.57 +	fix m
   12.58 +	assume m: "m \<le> i"
   12.59 +	thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
   12.60 +	  by (auto simp add: sums_iff) 
   12.61 +	   (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
   12.62 +      qed
   12.63 +    finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
   12.64 +    also have "... \<le> suminf g" 
   12.65 +      by (rule series_pos_le [OF sumg]) (simp add: g_nneg) 
   12.66 +    finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
   12.67 +  next
   12.68 +    fix e :: real
   12.69 +    assume e: "0 < e"
   12.70 +    with summable_sums [OF sumg]
   12.71 +    obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < e/2" and nz: "N>0"
   12.72 +      by (simp add: sums_def LIMSEQ_iff_nz dist_real_def)
   12.73 +         (metis e half_gt_zero le_refl that)
   12.74 +    hence gless: "suminf g < setsum g {0..<N} + e/2" using series_pos_le [OF sumg]
   12.75 +      by (simp add: g_nneg)
   12.76 +    { fix m
   12.77 +      assume m: "m<N"
   12.78 +      hence enneg: "0 < e / (2 * real N)" using e
   12.79 +	by (simp add: zero_less_divide_iff) 
   12.80 +      hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
   12.81 +	using fsums [of m] m
   12.82 +        by (force simp add: sums_def LIMSEQ_def dist_real_def)
   12.83 +      hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" 
   12.84 +	using fsums [of m]
   12.85 +	by (auto simp add: sums_iff) 
   12.86 +           (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') 
   12.87 +    }
   12.88 +    hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
   12.89 +      by (force intro: choice) 
   12.90 +    then obtain jj where jj:
   12.91 +          "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
   12.92 +      by auto
   12.93 +    def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}"
   12.94 +    have "setsum g {0..<N} <
   12.95 +             (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))"
   12.96 +      by (auto simp add: nz jj intro: setsum_strict_mono) 
   12.97 +    also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz
   12.98 +      by (auto simp add: setsum_addf real_of_nat_def) 
   12.99 +    also have "... = setsum f IJ + e/2" 
  12.100 +      by (simp add: IJ_def setsum_Sigma) 
  12.101 +    finally have "setsum g {0..<N} < setsum f IJ + e/2" .
  12.102 +    hence glessf: "suminf g < setsum f IJ + e" using gless 
  12.103 +      by auto
  12.104 +    have finite_IJ: "finite IJ"
  12.105 +      by (simp add: IJ_def) 
  12.106 +    def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
  12.107 +    have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
  12.108 +      proof (auto simp add: NIJ_def)
  12.109 +	fix i j
  12.110 +	assume ij:"(i,j) \<in> IJ"
  12.111 +	hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
  12.112 +	  by (metis nat_to_nat2_surj surj_f_inv_f) 
  12.113 +	thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
  12.114 +	  by (rule image_eqI) 
  12.115 +	     (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
  12.116 +                    nat_to_nat2_surj surj_f_inv_f) 
  12.117 +      qed
  12.118 +    have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
  12.119 +      by (rule setsum_mono2) (auto simp add: IJsb) 
  12.120 +    also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
  12.121 +      by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV]) 
  12.122 +    also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
  12.123 +      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
  12.124 +    finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
  12.125 +    thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
  12.126 +      by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
  12.127 +  qed
  12.128 +qed
  12.129 +
  12.130 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 28 11:43:06 2009 +0000
    13.3 @@ -0,0 +1,229 @@
    13.4 +(*  Title:      Sigma_Algebra.thy
    13.5 +    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
    13.6 +    Plus material from the Hurd/Coble measure theory development, 
    13.7 +    translated by Lawrence Paulson.
    13.8 +*)
    13.9 +
   13.10 +header {* Sigma Algebras *}
   13.11 +
   13.12 +theory Sigma_Algebra imports Complex_Main begin
   13.13 +
   13.14 +text {* Sigma algebras are an elementary concept in measure
   13.15 +  theory. To measure --- that is to integrate --- functions, we first have
   13.16 +  to measure sets. Unfortunately, when dealing with a large universe,
   13.17 +  it is often not possible to consistently assign a measure to every
   13.18 +  subset. Therefore it is necessary to define the set of measurable
   13.19 +  subsets of the universe. A sigma algebra is such a set that has
   13.20 +  three very natural and desirable properties. *}
   13.21 +
   13.22 +subsection {* Algebras *}
   13.23 +
   13.24 +record 'a algebra = 
   13.25 +  space :: "'a set" 
   13.26 +  sets :: "'a set set"
   13.27 +
   13.28 +locale algebra =
   13.29 +  fixes M
   13.30 +  assumes space_closed: "sets M \<subseteq> Pow (space M)"
   13.31 +     and  empty_sets [iff]: "{} \<in> sets M"
   13.32 +     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
   13.33 +     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
   13.34 +
   13.35 +lemma (in algebra) top [iff]: "space M \<in> sets M"
   13.36 +  by (metis Diff_empty compl_sets empty_sets)
   13.37 +
   13.38 +lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
   13.39 +  by (metis PowD contra_subsetD space_closed)
   13.40 +
   13.41 +lemma (in algebra) Int [intro]: 
   13.42 +  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
   13.43 +proof -
   13.44 +  have "((space M - a) \<union> (space M - b)) \<in> sets M" 
   13.45 +    by (metis a b compl_sets Un)
   13.46 +  moreover
   13.47 +  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))" 
   13.48 +    using space_closed a b
   13.49 +    by blast
   13.50 +  ultimately show ?thesis
   13.51 +    by (metis compl_sets)
   13.52 +qed
   13.53 +
   13.54 +lemma (in algebra) Diff [intro]: 
   13.55 +  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
   13.56 +proof -
   13.57 +  have "(a \<inter> (space M - b)) \<in> sets M"
   13.58 +    by (metis a b compl_sets Int)
   13.59 +  moreover
   13.60 +  have "a - b = (a \<inter> (space M - b))"
   13.61 +    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
   13.62 +  ultimately show ?thesis
   13.63 +    by metis
   13.64 +qed
   13.65 +
   13.66 +lemma (in algebra) finite_union [intro]: 
   13.67 +  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
   13.68 +  by (induct set: finite) (auto simp add: Un) 
   13.69 +
   13.70 +
   13.71 +subsection {* Sigma Algebras *}
   13.72 +
   13.73 +locale sigma_algebra = algebra +
   13.74 +  assumes countable_UN [intro]:
   13.75 +         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   13.76 +
   13.77 +lemma (in sigma_algebra) countable_INT:
   13.78 +  assumes a: "range a \<subseteq> sets M"
   13.79 +  shows "(\<Inter>i::nat. a i) \<in> sets M"
   13.80 +proof -
   13.81 +  have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
   13.82 +    by (blast intro: countable_UN compl_sets a) 
   13.83 +  moreover
   13.84 +  have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a 
   13.85 +    by blast
   13.86 +  ultimately show ?thesis by metis
   13.87 +qed
   13.88 +
   13.89 +
   13.90 +lemma algebra_Pow:
   13.91 +     "algebra (| space = sp, sets = Pow sp |)"
   13.92 +  by (auto simp add: algebra_def) 
   13.93 +
   13.94 +lemma sigma_algebra_Pow:
   13.95 +     "sigma_algebra (| space = sp, sets = Pow sp |)"
   13.96 +  by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) 
   13.97 +
   13.98 +subsection {* Binary Unions *}
   13.99 +
  13.100 +definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
  13.101 +  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
  13.102 +
  13.103 +lemma range_binary_eq: "range(binary a b) = {a,b}" 
  13.104 +  by (auto simp add: binary_def)  
  13.105 +
  13.106 +lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
  13.107 +  by (simp add: UNION_eq_Union_image range_binary_eq) 
  13.108 +
  13.109 +lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
  13.110 +  by (simp add: INTER_eq_Inter_image range_binary_eq) 
  13.111 +
  13.112 +lemma sigma_algebra_iff: 
  13.113 +     "sigma_algebra M \<longleftrightarrow> 
  13.114 +      algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
  13.115 +  by (simp add: sigma_algebra_def sigma_algebra_axioms_def) 
  13.116 +
  13.117 +lemma sigma_algebra_iff2:
  13.118 +     "sigma_algebra M \<longleftrightarrow>
  13.119 +       sets M \<subseteq> Pow (space M) &
  13.120 +       {} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) &
  13.121 +       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
  13.122 +  by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
  13.123 +         algebra_def Un_range_binary) 
  13.124 +
  13.125 +
  13.126 +subsection {* Initial Sigma Algebra *}
  13.127 +
  13.128 +text {*Sigma algebras can naturally be created as the closure of any set of
  13.129 +  sets with regard to the properties just postulated.  *}
  13.130 +
  13.131 +inductive_set
  13.132 +  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
  13.133 +  for sp :: "'a set" and A :: "'a set set"
  13.134 +  where
  13.135 +    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
  13.136 +  | Empty: "{} \<in> sigma_sets sp A"
  13.137 +  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
  13.138 +  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
  13.139 +
  13.140 +
  13.141 +definition
  13.142 +  sigma  where
  13.143 +  "sigma sp A = (| space = sp, sets = sigma_sets sp A |)"
  13.144 +
  13.145 +
  13.146 +lemma space_sigma [simp]: "space (sigma X B) = X"
  13.147 +  by (simp add: sigma_def) 
  13.148 +
  13.149 +lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
  13.150 +  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
  13.151 +
  13.152 +lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
  13.153 +  by (erule sigma_sets.induct, auto) 
  13.154 +
  13.155 +lemma sigma_sets_Un: 
  13.156 +  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
  13.157 +apply (simp add: Un_range_binary range_binary_eq) 
  13.158 +apply (metis Union COMBK_def binary_def fun_upd_apply) 
  13.159 +done
  13.160 +
  13.161 +lemma sigma_sets_Inter:
  13.162 +  assumes Asb: "A \<subseteq> Pow sp"
  13.163 +  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
  13.164 +proof -
  13.165 +  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
  13.166 +  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A" 
  13.167 +    by (rule sigma_sets.Compl)
  13.168 +  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
  13.169 +    by (rule sigma_sets.Union)
  13.170 +  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
  13.171 +    by (rule sigma_sets.Compl)
  13.172 +  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)" 
  13.173 +    by auto
  13.174 +  also have "... = (\<Inter>i. a i)" using ai
  13.175 +    by (blast dest: sigma_sets_into_sp [OF Asb]) 
  13.176 +  finally show ?thesis . 
  13.177 +qed
  13.178 +
  13.179 +lemma sigma_sets_INTER:
  13.180 +  assumes Asb: "A \<subseteq> Pow sp" 
  13.181 +      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
  13.182 +  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
  13.183 +proof -
  13.184 +  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
  13.185 +    by (simp add: sigma_sets.intros sigma_sets_top)
  13.186 +  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
  13.187 +    by (rule sigma_sets_Inter [OF Asb])
  13.188 +  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
  13.189 +    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
  13.190 +  finally show ?thesis .
  13.191 +qed
  13.192 +
  13.193 +lemma (in sigma_algebra) sigma_sets_subset:
  13.194 +  assumes a: "a \<subseteq> sets M" 
  13.195 +  shows "sigma_sets (space M) a \<subseteq> sets M"
  13.196 +proof
  13.197 +  fix x
  13.198 +  assume "x \<in> sigma_sets (space M) a"
  13.199 +  from this show "x \<in> sets M"
  13.200 +    by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 
  13.201 +qed
  13.202 +
  13.203 +lemma (in sigma_algebra) sigma_sets_eq:
  13.204 +     "sigma_sets (space M) (sets M) = sets M"
  13.205 +proof
  13.206 +  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
  13.207 +    by (metis Set.subsetI sigma_sets.Basic space_closed)
  13.208 +  next
  13.209 +  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
  13.210 +    by (metis sigma_sets_subset subset_refl)
  13.211 +qed
  13.212 +
  13.213 +lemma sigma_algebra_sigma_sets:
  13.214 +     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
  13.215 +  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
  13.216 +      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) 
  13.217 +  apply (blast dest: sigma_sets_into_sp)
  13.218 +  apply (blast intro: sigma_sets.intros) 
  13.219 +  done
  13.220 +
  13.221 +lemma sigma_algebra_sigma:
  13.222 +     "a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)"
  13.223 +  apply (rule sigma_algebra_sigma_sets) 
  13.224 +  apply (auto simp add: sigma_def) 
  13.225 +  done
  13.226 +
  13.227 +lemma (in sigma_algebra) sigma_subset:
  13.228 +     "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
  13.229 +  by (simp add: sigma_def sigma_sets_subset)
  13.230 +
  13.231 +end
  13.232 +
    14.1 --- a/src/HOL/Product_Type.thy	Wed Oct 28 00:24:38 2009 +0100
    14.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 28 11:43:06 2009 +0000
    14.3 @@ -927,6 +927,9 @@
    14.4     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    14.5  by blast
    14.6  
    14.7 +lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
    14.8 +  by (auto, rule_tac p = "f x" in PairE, auto)
    14.9 +
   14.10  subsubsection {* Code generator setup *}
   14.11  
   14.12  instance * :: (eq, eq) eq ..
    15.1 --- a/src/HOL/SEQ.thy	Wed Oct 28 00:24:38 2009 +0100
    15.2 +++ b/src/HOL/SEQ.thy	Wed Oct 28 11:43:06 2009 +0000
    15.3 @@ -205,6 +205,9 @@
    15.4    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    15.5  unfolding LIMSEQ_def dist_norm ..
    15.6  
    15.7 +lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    15.8 +  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
    15.9 +
   15.10  lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
   15.11  by (simp only: LIMSEQ_iff Zseq_def)
   15.12  
    16.1 --- a/src/HOL/Series.thy	Wed Oct 28 00:24:38 2009 +0100
    16.2 +++ b/src/HOL/Series.thy	Wed Oct 28 11:43:06 2009 +0000
    16.3 @@ -10,7 +10,7 @@
    16.4  header{*Finite Summation and Infinite Series*}
    16.5  
    16.6  theory Series
    16.7 -imports SEQ
    16.8 +imports SEQ Deriv
    16.9  begin
   16.10  
   16.11  definition
   16.12 @@ -285,6 +285,26 @@
   16.13  text{*A summable series of positive terms has limit that is at least as
   16.14  great as any partial sum.*}
   16.15  
   16.16 +lemma pos_summable:
   16.17 +  fixes f:: "nat \<Rightarrow> real"
   16.18 +  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
   16.19 +  shows "summable f"
   16.20 +proof -
   16.21 +  have "convergent (\<lambda>n. setsum f {0..<n})" 
   16.22 +    proof (rule Bseq_mono_convergent)
   16.23 +      show "Bseq (\<lambda>n. setsum f {0..<n})"
   16.24 +	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
   16.25 +           (auto simp add: le pos)  
   16.26 +    next 
   16.27 +      show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
   16.28 +	by (auto intro: setsum_mono2 pos) 
   16.29 +    qed
   16.30 +  then obtain L where "(%n. setsum f {0..<n}) ----> L"
   16.31 +    by (blast dest: convergentD)
   16.32 +  thus ?thesis
   16.33 +    by (force simp add: summable_def sums_def) 
   16.34 +qed
   16.35 +
   16.36  lemma series_pos_le:
   16.37    fixes f :: "nat \<Rightarrow> real"
   16.38    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
   16.39 @@ -361,6 +381,19 @@
   16.40    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   16.41  by (rule geometric_sums [THEN sums_summable])
   16.42  
   16.43 +lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})"
   16.44 +  by arith 
   16.45 +
   16.46 +lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
   16.47 +proof -
   16.48 +  have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
   16.49 +    by auto
   16.50 +  have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
   16.51 +    by simp
   16.52 +  thus ?thesis using divide.sums [OF 2, of 2]
   16.53 +    by simp
   16.54 +qed
   16.55 +
   16.56  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   16.57  
   16.58  lemma summable_convergent_sumr_iff:
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/SupInf.thy	Wed Oct 28 11:43:06 2009 +0000
    17.3 @@ -0,0 +1,462 @@
    17.4 +(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
    17.5 +
    17.6 +header {*Sup and Inf Operators on Sets of Reals.*}
    17.7 +
    17.8 +theory SupInf
    17.9 +imports RComplete
   17.10 +begin
   17.11 +
   17.12 +lemma minus_max_eq_min:
   17.13 +  fixes x :: "'a::{lordered_ab_group_add, linorder}"
   17.14 +  shows "- (max x y) = min (-x) (-y)"
   17.15 +by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
   17.16 +
   17.17 +lemma minus_min_eq_max:
   17.18 +  fixes x :: "'a::{lordered_ab_group_add, linorder}"
   17.19 +  shows "- (min x y) = max (-x) (-y)"
   17.20 +by (metis minus_max_eq_min minus_minus)
   17.21 +
   17.22 +lemma minus_Max_eq_Min [simp]:
   17.23 +  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
   17.24 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
   17.25 +proof (induct S rule: finite_ne_induct)
   17.26 +  case (singleton x)
   17.27 +  thus ?case by simp
   17.28 +next
   17.29 +  case (insert x S)
   17.30 +  thus ?case by (simp add: minus_max_eq_min) 
   17.31 +qed
   17.32 +
   17.33 +lemma minus_Min_eq_Max [simp]:
   17.34 +  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
   17.35 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
   17.36 +proof (induct S rule: finite_ne_induct)
   17.37 +  case (singleton x)
   17.38 +  thus ?case by simp
   17.39 +next
   17.40 +  case (insert x S)
   17.41 +  thus ?case by (simp add: minus_min_eq_max) 
   17.42 +qed
   17.43 +
   17.44 +instantiation real :: Sup 
   17.45 +begin
   17.46 +definition
   17.47 +  Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
   17.48 +
   17.49 +instance ..
   17.50 +end
   17.51 +
   17.52 +instantiation real :: Inf 
   17.53 +begin
   17.54 +definition
   17.55 +  Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
   17.56 +
   17.57 +instance ..
   17.58 +end
   17.59 +
   17.60 +subsection{*Supremum of a set of reals*}
   17.61 +
   17.62 +lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
   17.63 +  fixes x :: real
   17.64 +  assumes x: "x \<in> X"
   17.65 +      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   17.66 +  shows "x \<le> Sup X"
   17.67 +proof (auto simp add: Sup_real_def) 
   17.68 +  from reals_complete2
   17.69 +  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   17.70 +    by (blast intro: x z)
   17.71 +  hence "x \<le> s"
   17.72 +    by (blast intro: x z)
   17.73 +  also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
   17.74 +    by (fast intro: Least_equality [symmetric])  
   17.75 +  finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
   17.76 +qed
   17.77 +
   17.78 +lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
   17.79 +  fixes z :: real
   17.80 +  assumes x: "X \<noteq> {}"
   17.81 +      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   17.82 +  shows "Sup X \<le> z"
   17.83 +proof (auto simp add: Sup_real_def) 
   17.84 +  from reals_complete2 x
   17.85 +  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   17.86 +    by (blast intro: z)
   17.87 +  hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
   17.88 +    by (best intro: Least_equality)  
   17.89 +  also with s z have "... \<le> z"
   17.90 +    by blast
   17.91 +  finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
   17.92 +qed
   17.93 +
   17.94 +lemma Sup_singleton [simp]: "Sup {x::real} = x"
   17.95 +  by (force intro: Least_equality simp add: Sup_real_def)
   17.96 + 
   17.97 +lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
   17.98 +  fixes z :: real
   17.99 +  assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
  17.100 +  shows  "Sup X = z"
  17.101 +  by (force intro: Least_equality X z simp add: Sup_real_def)
  17.102 + 
  17.103 +lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
  17.104 +  fixes x :: real
  17.105 +  shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
  17.106 +  by (metis Sup_upper real_le_trans)
  17.107 +
  17.108 +lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
  17.109 +  fixes z :: real
  17.110 +  shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
  17.111 +  by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
  17.112 +
  17.113 +lemma Sup_eq:
  17.114 +  fixes a :: real
  17.115 +  shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
  17.116 +        \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
  17.117 +  by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
  17.118 +        insert_not_empty real_le_anti_sym)
  17.119 +
  17.120 +lemma Sup_le:
  17.121 +  fixes S :: "real set"
  17.122 +  shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
  17.123 +by (metis SupInf.Sup_least setle_def)
  17.124 +
  17.125 +lemma Sup_upper_EX: 
  17.126 +  fixes x :: real
  17.127 +  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
  17.128 +  by blast
  17.129 +
  17.130 +lemma Sup_insert_nonempty: 
  17.131 +  fixes x :: real
  17.132 +  assumes x: "x \<in> X"
  17.133 +      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
  17.134 +  shows "Sup (insert a X) = max a (Sup X)"
  17.135 +proof (cases "Sup X \<le> a")
  17.136 +  case True
  17.137 +  thus ?thesis
  17.138 +    apply (simp add: max_def) 
  17.139 +    apply (rule Sup_eq_maximum)
  17.140 +    apply (metis insertCI)
  17.141 +    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
  17.142 +    done
  17.143 +next
  17.144 +  case False
  17.145 +  hence 1:"a < Sup X" by simp
  17.146 +  have "Sup X \<le> Sup (insert a X)"
  17.147 +    apply (rule Sup_least)
  17.148 +    apply (metis empty_psubset_nonempty psubset_eq x)
  17.149 +    apply (rule Sup_upper_EX) 
  17.150 +    apply blast
  17.151 +    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
  17.152 +    done
  17.153 +  moreover 
  17.154 +  have "Sup (insert a X) \<le> Sup X"
  17.155 +    apply (rule Sup_least)
  17.156 +    apply blast
  17.157 +    apply (metis False Sup_upper insertE real_le_linear z) 
  17.158 +    done
  17.159 +  ultimately have "Sup (insert a X) = Sup X"
  17.160 +    by (blast intro:  antisym )
  17.161 +  thus ?thesis
  17.162 +    by (metis 1 min_max.le_iff_sup real_less_def)
  17.163 +qed
  17.164 +
  17.165 +lemma Sup_insert_if: 
  17.166 +  fixes X :: "real set"
  17.167 +  assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
  17.168 +  shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
  17.169 +by auto (metis Sup_insert_nonempty z) 
  17.170 +
  17.171 +lemma Sup: 
  17.172 +  fixes S :: "real set"
  17.173 +  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
  17.174 +by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
  17.175 +
  17.176 +lemma Sup_finite_Max: 
  17.177 +  fixes S :: "real set"
  17.178 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.179 +  shows "Sup S = Max S"
  17.180 +using fS Se
  17.181 +proof-
  17.182 +  let ?m = "Max S"
  17.183 +  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
  17.184 +  with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
  17.185 +  from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
  17.186 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
  17.187 +  moreover
  17.188 +  have "Sup S \<le> ?m" using Sm lub
  17.189 +    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
  17.190 +  ultimately  show ?thesis by arith
  17.191 +qed
  17.192 +
  17.193 +lemma Sup_finite_in:
  17.194 +  fixes S :: "real set"
  17.195 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.196 +  shows "Sup S \<in> S"
  17.197 +  using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
  17.198 +
  17.199 +lemma Sup_finite_ge_iff: 
  17.200 +  fixes S :: "real set"
  17.201 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.202 +  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
  17.203 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
  17.204 +
  17.205 +lemma Sup_finite_le_iff: 
  17.206 +  fixes S :: "real set"
  17.207 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.208 +  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
  17.209 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
  17.210 +
  17.211 +lemma Sup_finite_gt_iff: 
  17.212 +  fixes S :: "real set"
  17.213 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.214 +  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
  17.215 +by (metis Se Sup_finite_le_iff fS linorder_not_less)
  17.216 +
  17.217 +lemma Sup_finite_lt_iff: 
  17.218 +  fixes S :: "real set"
  17.219 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.220 +  shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
  17.221 +by (metis Se Sup_finite_ge_iff fS linorder_not_less)
  17.222 +
  17.223 +lemma Sup_unique:
  17.224 +  fixes S :: "real set"
  17.225 +  shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
  17.226 +unfolding setle_def
  17.227 +apply (rule Sup_eq, auto) 
  17.228 +apply (metis linorder_not_less) 
  17.229 +done
  17.230 +
  17.231 +lemma Sup_abs_le:
  17.232 +  fixes S :: "real set"
  17.233 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
  17.234 +by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
  17.235 +
  17.236 +lemma Sup_bounds:
  17.237 +  fixes S :: "real set"
  17.238 +  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
  17.239 +  shows "a \<le> Sup S \<and> Sup S \<le> b"
  17.240 +proof-
  17.241 +  from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
  17.242 +  hence b: "Sup S \<le> b" using u 
  17.243 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
  17.244 +  from Se obtain y where y: "y \<in> S" by blast
  17.245 +  from lub l have "a \<le> Sup S"
  17.246 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
  17.247 +       (metis le_iff_sup le_sup_iff y)
  17.248 +  with b show ?thesis by blast
  17.249 +qed
  17.250 +
  17.251 +lemma Sup_asclose: 
  17.252 +  fixes S :: "real set"
  17.253 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
  17.254 +proof-
  17.255 +  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
  17.256 +  thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
  17.257 +    by  (auto simp add: setge_def setle_def)
  17.258 +qed
  17.259 +
  17.260 +
  17.261 +subsection{*Infimum of a set of reals*}
  17.262 +
  17.263 +lemma Inf_lower [intro]: 
  17.264 +  fixes z :: real
  17.265 +  assumes x: "x \<in> X"
  17.266 +      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
  17.267 +  shows "Inf X \<le> x"
  17.268 +proof -
  17.269 +  have "-x \<le> Sup (uminus ` X)"
  17.270 +    by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
  17.271 +  thus ?thesis 
  17.272 +    by (auto simp add: Inf_real_def)
  17.273 +qed
  17.274 +
  17.275 +lemma Inf_greatest [intro]: 
  17.276 +  fixes z :: real
  17.277 +  assumes x: "X \<noteq> {}"
  17.278 +      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
  17.279 +  shows "z \<le> Inf X"
  17.280 +proof -
  17.281 +  have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
  17.282 +  hence "z \<le> - Sup (uminus ` X)"
  17.283 +    by simp
  17.284 +  thus ?thesis 
  17.285 +    by (auto simp add: Inf_real_def)
  17.286 +qed
  17.287 +
  17.288 +lemma Inf_singleton [simp]: "Inf {x::real} = x"
  17.289 +  by (simp add: Inf_real_def) 
  17.290 + 
  17.291 +lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
  17.292 +  fixes z :: real
  17.293 +  assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
  17.294 +  shows  "Inf X = z"
  17.295 +proof -
  17.296 +  have "Sup (uminus ` X) = -z" using x z
  17.297 +    by (force intro: Sup_eq_maximum x z)
  17.298 +  thus ?thesis
  17.299 +    by (simp add: Inf_real_def) 
  17.300 +qed
  17.301 + 
  17.302 +lemma Inf_lower2:
  17.303 +  fixes x :: real
  17.304 +  shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
  17.305 +  by (metis Inf_lower real_le_trans)
  17.306 +
  17.307 +lemma Inf_real_iff:
  17.308 +  fixes z :: real
  17.309 +  shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
  17.310 +  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
  17.311 +            order_less_le_trans)
  17.312 +
  17.313 +lemma Inf_eq:
  17.314 +  fixes a :: real
  17.315 +  shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
  17.316 +  by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
  17.317 +        insert_absorb insert_not_empty real_le_anti_sym)
  17.318 +
  17.319 +lemma Inf_ge: 
  17.320 +  fixes S :: "real set"
  17.321 +  shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
  17.322 +by (metis SupInf.Inf_greatest setge_def)
  17.323 +
  17.324 +lemma Inf_lower_EX: 
  17.325 +  fixes x :: real
  17.326 +  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
  17.327 +  by blast
  17.328 +
  17.329 +lemma Inf_insert_nonempty: 
  17.330 +  fixes x :: real
  17.331 +  assumes x: "x \<in> X"
  17.332 +      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
  17.333 +  shows "Inf (insert a X) = min a (Inf X)"
  17.334 +proof (cases "a \<le> Inf X")
  17.335 +  case True
  17.336 +  thus ?thesis
  17.337 +    by (simp add: min_def)
  17.338 +       (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
  17.339 +next
  17.340 +  case False
  17.341 +  hence 1:"Inf X < a" by simp
  17.342 +  have "Inf (insert a X) \<le> Inf X"
  17.343 +    apply (rule Inf_greatest)
  17.344 +    apply (metis empty_psubset_nonempty psubset_eq x)
  17.345 +    apply (rule Inf_lower_EX) 
  17.346 +    apply (blast intro: elim:) 
  17.347 +    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
  17.348 +    done
  17.349 +  moreover 
  17.350 +  have "Inf X \<le> Inf (insert a X)"
  17.351 +    apply (rule Inf_greatest)
  17.352 +    apply blast
  17.353 +    apply (metis False Inf_lower insertE real_le_linear z) 
  17.354 +    done
  17.355 +  ultimately have "Inf (insert a X) = Inf X"
  17.356 +    by (blast intro:  antisym )
  17.357 +  thus ?thesis
  17.358 +    by (metis False min_max.inf_absorb2 real_le_linear)
  17.359 +qed
  17.360 +
  17.361 +lemma Inf_insert_if: 
  17.362 +  fixes X :: "real set"
  17.363 +  assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
  17.364 +  shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
  17.365 +by auto (metis Inf_insert_nonempty z) 
  17.366 +
  17.367 +lemma Inf_greater:
  17.368 +  fixes z :: real
  17.369 +  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
  17.370 +  by (metis Inf_real_iff mem_def not_leE)
  17.371 +
  17.372 +lemma Inf_close:
  17.373 +  fixes e :: real
  17.374 +  shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
  17.375 +  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
  17.376 +
  17.377 +lemma Inf_finite_Min:
  17.378 +  fixes S :: "real set"
  17.379 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
  17.380 +by (simp add: Inf_real_def Sup_finite_Max image_image) 
  17.381 +
  17.382 +lemma Inf_finite_in: 
  17.383 +  fixes S :: "real set"
  17.384 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
  17.385 +  shows "Inf S \<in> S"
  17.386 +  using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
  17.387 +
  17.388 +lemma Inf_finite_ge_iff: 
  17.389 +  fixes S :: "real set"
  17.390 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
  17.391 +by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
  17.392 +
  17.393 +lemma Inf_finite_le_iff:
  17.394 +  fixes S :: "real set"
  17.395 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
  17.396 +by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
  17.397 +          real_le_anti_sym real_le_linear)
  17.398 +
  17.399 +lemma Inf_finite_gt_iff: 
  17.400 +  fixes S :: "real set"
  17.401 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
  17.402 +by (metis Inf_finite_le_iff linorder_not_less)
  17.403 +
  17.404 +lemma Inf_finite_lt_iff: 
  17.405 +  fixes S :: "real set"
  17.406 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
  17.407 +by (metis Inf_finite_ge_iff linorder_not_less)
  17.408 +
  17.409 +lemma Inf_unique:
  17.410 +  fixes S :: "real set"
  17.411 +  shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
  17.412 +unfolding setge_def
  17.413 +apply (rule Inf_eq, auto) 
  17.414 +apply (metis less_le_not_le linorder_not_less) 
  17.415 +done
  17.416 +
  17.417 +lemma Inf_abs_ge:
  17.418 +  fixes S :: "real set"
  17.419 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
  17.420 +by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
  17.421 +
  17.422 +lemma Inf_asclose:
  17.423 +  fixes S :: "real set"
  17.424 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
  17.425 +proof -
  17.426 +  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
  17.427 +    by auto
  17.428 +  also have "... \<le> e" 
  17.429 +    apply (rule Sup_asclose) 
  17.430 +    apply (auto simp add: S)
  17.431 +    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
  17.432 +    done
  17.433 +  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
  17.434 +  thus ?thesis
  17.435 +    by (simp add: Inf_real_def)
  17.436 +qed
  17.437 +
  17.438 +subsection{*Relate max and min to Sup and Inf.*}
  17.439 +
  17.440 +lemma real_max_Sup:
  17.441 +  fixes x :: real
  17.442 +  shows "max x y = Sup {x,y}"
  17.443 +proof-
  17.444 +  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
  17.445 +  from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
  17.446 +  moreover
  17.447 +  have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
  17.448 +    by (simp add: linorder_linear)
  17.449 +  ultimately show ?thesis by arith
  17.450 +qed
  17.451 +
  17.452 +lemma real_min_Inf: 
  17.453 +  fixes x :: real
  17.454 +  shows "min x y = Inf {x,y}"
  17.455 +proof-
  17.456 +  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
  17.457 +  from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
  17.458 +    by (simp add: linorder_linear)
  17.459 +  moreover
  17.460 +  have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
  17.461 +    by simp
  17.462 +  ultimately show ?thesis by arith
  17.463 +qed
  17.464 +
  17.465 +end