author hoelzl Fri Nov 16 18:45:57 2012 +0100 (2012-11-16) changeset 50104 de19856feb54 parent 50103 3d89c38408cd child 50105 65d5b18e1626
move theorems to be more generally useable
```     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Nov 16 18:49:46 2012 +0100
1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Nov 16 18:45:57 2012 +0100
1.3 @@ -124,7 +124,6 @@
1.4    fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
1.5  qed auto
1.6
1.7 -
1.8  instantiation ereal :: abs
1.9  begin
1.10    function abs_ereal where
1.11 @@ -145,6 +144,9 @@
1.12  lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
1.13    by (cases x) auto
1.14
1.15 +lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
1.16 +  by auto
1.17 +
1.19
1.21 @@ -530,6 +532,9 @@
1.22  qed
1.23  end
1.24
1.25 +lemma real_ereal_1[simp]: "real (1::ereal) = 1"
1.26 +  unfolding one_ereal_def by simp
1.27 +
1.28  lemma real_of_ereal_le_1:
1.29    fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
1.30    by (cases a) (auto simp: one_ereal_def)
1.31 @@ -659,6 +664,16 @@
1.32    shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
1.33    by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
1.34
1.35 +lemma ereal_left_mult_cong:
1.36 +  fixes a b c :: ereal
1.37 +  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
1.38 +  by (cases "c = 0") simp_all
1.39 +
1.40 +lemma ereal_right_mult_cong:
1.41 +  fixes a b c :: ereal
1.42 +  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
1.43 +  by (cases "c = 0") simp_all
1.44 +
1.45  lemma ereal_distrib:
1.46    fixes a b c :: ereal
1.47    assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
1.48 @@ -941,6 +956,10 @@
1.49  using assms apply (cases x, cases e) apply auto
1.50  done
1.51
1.52 +lemma ereal_minus_eq_PInfty_iff:
1.53 +  fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
1.54 +  by (cases x y rule: ereal2_cases) simp_all
1.55 +
1.56  subsubsection {* Division *}
1.57
1.58  instantiation ereal :: inverse
```
```     2.1 --- a/src/HOL/Library/FuncSet.thy	Fri Nov 16 18:49:46 2012 +0100
2.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Nov 16 18:45:57 2012 +0100
2.3 @@ -81,7 +81,10 @@
2.5
2.6  lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
2.7 -by auto
2.8 +  by auto
2.9 +
2.10 +lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
2.11 +  by auto
2.12
2.13  lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
2.14  apply (simp add: Pi_def, auto)
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 16 18:49:46 2012 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
3.3 @@ -5914,4 +5914,71 @@
3.4  } ultimately show ?thesis by blast
3.5  qed
3.6
3.7 +
3.8 +lemma convex_le_Inf_differential:
3.9 +  fixes f :: "real \<Rightarrow> real"
3.10 +  assumes "convex_on I f"
3.11 +  assumes "x \<in> interior I" "y \<in> I"
3.12 +  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
3.13 +    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
3.14 +proof (cases rule: linorder_cases)
3.15 +  assume "x < y"
3.16 +  moreover
3.17 +  have "open (interior I)" by auto
3.18 +  from openE[OF this `x \<in> interior I`] guess e . note e = this
3.19 +  moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
3.20 +  ultimately have "x < t" "t < y" "t \<in> ball x e"
3.21 +    by (auto simp: dist_real_def field_simps split: split_min)
3.22 +  with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
3.23 +
3.24 +  have "open (interior I)" by auto
3.25 +  from openE[OF this `x \<in> interior I`] guess e .
3.26 +  moreover def K \<equiv> "x - e / 2"
3.27 +  with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
3.28 +  ultimately have "K \<in> I" "K < x" "x \<in> I"
3.29 +    using interior_subset[of I] `x \<in> interior I` by auto
3.30 +
3.31 +  have "Inf (?F x) \<le> (f x - f y) / (x - y)"
3.32 +  proof (rule Inf_lower2)
3.33 +    show "(f x - f t) / (x - t) \<in> ?F x"
3.34 +      using `t \<in> I` `x < t` by auto
3.35 +    show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
3.36 +      using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
3.37 +  next
3.38 +    fix y assume "y \<in> ?F x"
3.39 +    with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
3.40 +    show "(f K - f x) / (K - x) \<le> y" by auto
3.41 +  qed
3.42 +  then show ?thesis
3.43 +    using `x < y` by (simp add: field_simps)
3.44 +next
3.45 +  assume "y < x"
3.46 +  moreover
3.47 +  have "open (interior I)" by auto
3.48 +  from openE[OF this `x \<in> interior I`] guess e . note e = this
3.49 +  moreover def t \<equiv> "x + e / 2"
3.50 +  ultimately have "x < t" "t \<in> ball x e"
3.51 +    by (auto simp: dist_real_def field_simps)
3.52 +  with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
3.53 +
3.54 +  have "(f x - f y) / (x - y) \<le> Inf (?F x)"
3.55 +  proof (rule Inf_greatest)
3.56 +    have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
3.57 +      using `y < x` by (auto simp: field_simps)
3.58 +    also
3.59 +    fix z  assume "z \<in> ?F x"
3.60 +    with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
3.61 +    have "(f y - f x) / (y - x) \<le> z" by auto
3.62 +    finally show "(f x - f y) / (x - y) \<le> z" .
3.63 +  next
3.64 +    have "open (interior I)" by auto
3.65 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
3.66 +    then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
3.67 +    with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
3.68 +    then show "?F x \<noteq> {}" by blast
3.69 +  qed
3.70 +  then show ?thesis
3.71 +    using `y < x` by (simp add: field_simps)
3.72 +qed simp
3.73 +
3.74  end
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Nov 16 18:49:46 2012 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Nov 16 18:45:57 2012 +0100
4.3 @@ -423,6 +423,11 @@
4.4    using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
4.5       ereal_Liminf_uminus[of net f] assms by simp
4.6
4.7 +lemma convergent_ereal_limsup:
4.8 +  fixes X :: "nat \<Rightarrow> ereal"
4.9 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
4.10 +  by (auto simp: convergent_def limI lim_imp_Limsup)
4.11 +
4.12  lemma Liminf_PInfty:
4.13    fixes f :: "'a \<Rightarrow> ereal"
4.14    assumes "\<not> trivial_limit net"
4.15 @@ -486,6 +491,12 @@
4.16    shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
4.17    by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
4.18
4.19 +lemma convergent_ereal:
4.20 +  fixes X :: "nat \<Rightarrow> ereal"
4.21 +  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
4.22 +  using ereal_Liminf_eq_Limsup_iff[of sequentially]
4.23 +  by (auto simp: convergent_def)
4.24 +
4.25  lemma limsup_INFI_SUPR:
4.26    fixes f :: "nat \<Rightarrow> ereal"
4.27    shows "limsup f = (INF n. SUP m:{n..}. f m)"
4.28 @@ -1496,4 +1507,20 @@
4.30  qed simp
4.31
4.32 +lemma suminf_ereal_eq_0:
4.33 +  fixes f :: "nat \<Rightarrow> ereal"
4.34 +  assumes nneg: "\<And>i. 0 \<le> f i"
4.35 +  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
4.36 +proof
4.37 +  assume "(\<Sum>i. f i) = 0"
4.38 +  { fix i assume "f i \<noteq> 0"
4.39 +    with nneg have "0 < f i" by (auto simp: less_le)
4.40 +    also have "f i = (\<Sum>j. if j = i then f i else 0)"
4.41 +      by (subst suminf_finite[where N="{i}"]) auto
4.42 +    also have "\<dots> \<le> (\<Sum>i. f i)"
4.43 +      using nneg by (auto intro!: suminf_le_pos)
4.44 +    finally have False using `(\<Sum>i. f i) = 0` by auto }
4.45 +  then show "\<forall>i. f i = 0" by auto
4.46 +qed simp
4.47 +
4.48  end
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:49:46 2012 +0100
5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:45:57 2012 +0100
5.3 @@ -483,6 +483,13 @@
5.4    show ?thesis unfolding content_def using assms by (auto simp: *)
5.5  qed
5.6
5.7 +lemma content_singleton[simp]: "content {a} = 0"
5.8 +proof -
5.9 +  have "content {a .. a} = 0"
5.10 +    by (subst content_closed_interval) auto
5.11 +  then show ?thesis by simp
5.12 +qed
5.13 +
5.14  lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1"
5.15  proof -
5.16    have *: "\<forall>i<DIM('a). (0::'a)\$\$i \<le> (One::'a)\$\$i" by auto
5.17 @@ -1665,6 +1672,16 @@
5.18    unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
5.19    by(rule bounded_linear_scaleR_right)
5.20
5.21 +lemma has_integral_cmult_real:
5.22 +  fixes c :: real
5.23 +  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
5.24 +  shows "((\<lambda>x. c * f x) has_integral c * x) A"
5.25 +proof cases
5.26 +  assume "c \<noteq> 0"
5.27 +  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
5.28 +    unfolding real_scaleR_def .
5.29 +qed simp
5.30 +
5.31  lemma has_integral_neg:
5.32    shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
5.33    apply(drule_tac c="-1" in has_integral_cmul) by auto
5.34 @@ -1746,6 +1763,12 @@
5.35    shows "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
5.36    unfolding integrable_on_def by(auto intro: has_integral_cmul)
5.37
5.38 +lemma integrable_on_cmult_iff:
5.39 +  fixes c :: real assumes "c \<noteq> 0"
5.40 +  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
5.41 +  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
5.42 +  by auto
5.43 +
5.44  lemma integrable_neg:
5.45    shows "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
5.46    unfolding integrable_on_def by(auto intro: has_integral_neg)
5.47 @@ -2669,6 +2692,11 @@
5.48    unfolding split_def apply(subst scaleR_left.setsum[THEN sym, unfolded o_def])
5.49    defer apply(subst additive_content_tagged_division[unfolded split_def]) apply assumption by auto
5.50
5.51 +lemma integral_const[simp]:
5.52 +  fixes a b :: "'a::ordered_euclidean_space"
5.53 +  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
5.54 +  by (rule integral_unique) (rule has_integral_const)
5.55 +
5.56  subsection {* Bounds on the norm of Riemann sums and the integral itself. *}
5.57
5.58  lemma dsum_bound: assumes "p division_of {a..b}" "norm(c) \<le> e"
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:49:46 2012 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:45:57 2012 +0100
6.3 @@ -2891,6 +2891,10 @@
6.4    by (fast intro: less_trans, fast intro: le_less_trans,
6.5      fast intro: order_trans)
6.6
6.7 +lemma atLeastAtMost_singleton_euclidean[simp]:
6.8 +  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
6.9 +  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
6.10 +
6.11  lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
6.12
6.13  instance real::ordered_euclidean_space
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:49:46 2012 +0100
7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
7.3 @@ -2044,6 +2044,10 @@
7.4  unfolding bounded_any_center [where a=0]
7.6
7.7 +lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
7.8 +  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
7.9 +  using assms by auto
7.10 +
7.11  lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
7.12  lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
7.13    by (metis bounded_def subset_eq)
```
```     8.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
8.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
8.3 @@ -8,24 +8,12 @@
8.4  imports Lebesgue_Integration
8.5  begin
8.6
8.7 -lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
8.8 -  by auto
8.9 -
8.10 -lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
8.11 -  by auto
8.12 -
8.13 -lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
8.14 +lemma Pair_vimage_times[simp]: "Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
8.15    by auto
8.16
8.17 -lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
8.18 +lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
8.19    by auto
8.20
8.21 -lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
8.22 -  by (cases x) simp
8.23 -
8.24 -lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
8.25 -  by (auto simp: fun_eq_iff)
8.26 -
8.27  section "Binary products"
8.28
8.29  definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where
8.30 @@ -787,4 +775,39 @@
8.31               intro!: positive_integral_cong arg_cong[where f="emeasure N"])
8.32  qed simp
8.33
8.34 +lemma pair_measure_eqI:
8.35 +  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
8.36 +  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
8.37 +  assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
8.38 +  shows "M1 \<Otimes>\<^isub>M M2 = M"
8.39 +proof -
8.40 +  interpret M1: sigma_finite_measure M1 by fact
8.41 +  interpret M2: sigma_finite_measure M2 by fact
8.42 +  interpret pair_sigma_finite M1 M2 by default
8.43 +  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
8.44 +  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
8.45 +  let ?P = "M1 \<Otimes>\<^isub>M M2"
8.46 +  show ?thesis
8.47 +  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
8.48 +    show "?E \<subseteq> Pow (space ?P)"
8.49 +      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
8.50 +    show "sets ?P = sigma_sets (space ?P) ?E"
8.51 +      by (simp add: sets_pair_measure space_pair_measure)
8.52 +    then show "sets M = sigma_sets (space ?P) ?E"
8.53 +      using sets[symmetric] by simp
8.54 +  next
8.55 +    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
8.56 +      using F by (auto simp: space_pair_measure)
8.57 +  next
8.58 +    fix X assume "X \<in> ?E"
8.59 +    then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
8.60 +    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
8.61 +       by (simp add: M2.emeasure_pair_measure_Times)
8.62 +    also have "\<dots> = emeasure M (A \<times> B)"
8.63 +      using A B emeasure by auto
8.64 +    finally show "emeasure ?P X = emeasure M X"
8.65 +      by simp
8.66 +  qed
8.67 +qed
8.68 +
8.69  end
8.70 \ No newline at end of file
```
```     9.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:49:46 2012 +0100
9.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:45:57 2012 +0100
9.3 @@ -1114,21 +1114,10 @@
9.4      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
9.5    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
9.6
9.7 -lemma sets_Collect_eventually_sequientially[measurable]:
9.8 +lemma sets_Collect_eventually_sequentially[measurable]:
9.9    "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
9.10    unfolding eventually_sequentially by simp
9.11
9.12 -lemma convergent_ereal:
9.13 -  fixes X :: "nat \<Rightarrow> ereal"
9.14 -  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
9.15 -  using ereal_Liminf_eq_Limsup_iff[of sequentially]
9.16 -  by (auto simp: convergent_def)
9.17 -
9.18 -lemma convergent_ereal_limsup:
9.19 -  fixes X :: "nat \<Rightarrow> ereal"
9.20 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
9.21 -  by (auto simp: convergent_def limI lim_imp_Limsup)
9.22 -
9.23  lemma sets_Collect_ereal_convergent[measurable]:
9.24    fixes f :: "nat \<Rightarrow> 'a => ereal"
9.25    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
```
```    10.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
10.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
10.3 @@ -262,6 +262,47 @@
10.4      using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
10.5  qed
10.6
10.7 +lemma funset_eq_UN_fun_upd_I:
10.8 +  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
10.9 +  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
10.10 +  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
10.11 +  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
10.12 +proof safe
10.13 +  fix f assume f: "f \<in> F (insert a A)"
10.14 +  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
10.15 +  proof (rule UN_I[of "f(a := d)"])
10.16 +    show "f(a := d) \<in> F A" using *[OF f] .
10.17 +    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
10.18 +    proof (rule image_eqI[of _ _ "f a"])
10.19 +      show "f a \<in> G (f(a := d))" using **[OF f] .
10.20 +    qed simp
10.21 +  qed
10.22 +next
10.23 +  fix f x assume "f \<in> F A" "x \<in> G f"
10.24 +  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
10.25 +qed
10.26 +
10.27 +lemma extensional_funcset_insert_eq[simp]:
10.28 +  assumes "a \<notin> A"
10.29 +  shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
10.30 +  apply (rule funset_eq_UN_fun_upd_I)
10.31 +  using assms
10.32 +  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
10.33 +
10.34 +lemma finite_extensional_funcset[simp, intro]:
10.35 +  assumes "finite A" "finite B"
10.36 +  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
10.37 +  using assms by induct auto
10.38 +
10.39 +lemma finite_PiE[simp, intro]:
10.40 +  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
10.41 +  shows "finite (Pi\<^isub>E A B)"
10.42 +proof -
10.43 +  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
10.44 +  show ?thesis
10.45 +    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
10.46 +qed
10.47 +
10.48  section "Finite product spaces"
10.49
10.50  section "Products"
10.51 @@ -441,6 +482,31 @@
10.52      done
10.53  qed
10.54
10.55 +lemma prod_algebra_cong:
10.56 +  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
10.57 +  shows "prod_algebra I M = prod_algebra J N"
10.58 +proof -
10.59 +  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
10.60 +    using sets_eq_imp_space_eq[OF sets] by auto
10.61 +  with sets show ?thesis unfolding `I = J`
10.62 +    by (intro antisym prod_algebra_mono) auto
10.63 +qed
10.64 +
10.65 +lemma space_in_prod_algebra:
10.66 +  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
10.67 +proof cases
10.68 +  assume "I = {}" then show ?thesis
10.69 +    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
10.70 +next
10.71 +  assume "I \<noteq> {}"
10.72 +  then obtain i where "i \<in> I" by auto
10.73 +  then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
10.74 +    by (auto simp: prod_emb_def Pi_iff)
10.75 +  also have "\<dots> \<in> prod_algebra I M"
10.76 +    using `i \<in> I` by (intro prod_algebraI) auto
10.77 +  finally show ?thesis .
10.78 +qed
10.79 +
10.80  lemma space_PiM: "space (\<Pi>\<^isub>M i\<in>I. M i) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
10.81    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
10.82
10.83 @@ -1007,6 +1073,23 @@
10.84    show ?thesis
10.85      unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
10.86  qed
10.87 +lemma (in product_sigma_finite) distr_component:
10.88 +  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
10.89 +proof (intro measure_eqI[symmetric])
10.90 +  interpret I: finite_product_sigma_finite M "{i}" by default simp
10.91 +
10.92 +  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
10.93 +    by (auto simp: extensional_def restrict_def)
10.94 +
10.95 +  fix A assume A: "A \<in> sets ?P"
10.96 +  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
10.97 +    by simp
10.98 +  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
10.99 +    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
10.100 +  also have "\<dots> = emeasure ?D A"
10.101 +    using A by (simp add: product_positive_integral_singleton emeasure_distr)
10.102 +  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
10.103 +qed simp
10.104
10.105  lemma (in product_sigma_finite) product_integral_fold:
10.106    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
10.107 @@ -1250,4 +1333,31 @@
10.108      by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
10.109  qed
10.110
10.111 +lemma pair_measure_eq_distr_PiM:
10.112 +  fixes M1 :: "'a measure" and M2 :: "'a measure"
10.113 +  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
10.114 +  shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))"
10.115 +    (is "?P = ?D")
10.116 +proof (rule pair_measure_eqI[OF assms])
10.117 +  interpret B: product_sigma_finite "bool_case M1 M2"
10.118 +    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
10.119 +  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
10.120 +
10.121 +  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
10.122 +    by auto
10.123 +  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
10.124 +  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
10.125 +    by (simp add: UNIV_bool ac_simps)
10.126 +  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
10.127 +    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
10.128 +  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
10.129 +    using A[THEN sets_into_space] B[THEN sets_into_space]
10.130 +    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
10.131 +  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
10.132 +    using A B
10.133 +      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
10.134 +      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
10.135 +    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
10.136 +qed simp
10.137 +
10.138  end
```
```    11.1 --- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:49:46 2012 +0100
11.2 +++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:45:57 2012 +0100
11.3 @@ -18,9 +18,6 @@
11.4  definition (in prob_space)
11.5    indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
11.6
11.7 -lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
11.8 -  by auto
11.9 -
11.10  lemma (in prob_space) indep_events_def:
11.11    "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
11.12      (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
11.13 @@ -827,31 +824,6 @@
11.14      using I by auto
11.15  qed fact+
11.16
11.17 -lemma prod_algebra_cong:
11.18 -  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
11.19 -  shows "prod_algebra I M = prod_algebra J N"
11.20 -proof -
11.21 -  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
11.22 -    using sets_eq_imp_space_eq[OF sets] by auto
11.23 -  with sets show ?thesis unfolding `I = J`
11.24 -    by (intro antisym prod_algebra_mono) auto
11.25 -qed
11.26 -
11.27 -lemma space_in_prod_algebra:
11.28 -  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
11.29 -proof cases
11.30 -  assume "I = {}" then show ?thesis
11.31 -    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
11.32 -next
11.33 -  assume "I \<noteq> {}"
11.34 -  then obtain i where "i \<in> I" by auto
11.35 -  then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
11.36 -    by (auto simp: prod_emb_def Pi_iff)
11.37 -  also have "\<dots> \<in> prod_algebra I M"
11.38 -    using `i \<in> I` by (intro prod_algebraI) auto
11.39 -  finally show ?thesis .
11.40 -qed
11.41 -
11.42  lemma (in prob_space) indep_vars_iff_distr_eq_PiM:
11.43    fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
11.44    assumes "I \<noteq> {}"
11.45 @@ -972,114 +944,6 @@
11.46      unfolding UNIV_bool by auto
11.47  qed
11.48
11.49 -lemma measurable_bool_case[simp, intro]:
11.50 -  "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))"
11.51 -    (is "?f \<in> measurable ?B ?P")
11.52 -proof (rule measurable_PiM_single)
11.53 -  show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))"
11.54 -    by (auto simp: space_pair_measure extensional_def split: bool.split)
11.55 -  fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)"
11.56 -  moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A}
11.57 -    = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)"
11.58 -    by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space)
11.59 -  ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B"
11.60 -    by (auto split: bool.split)
11.61 -qed
11.62 -
11.63 -lemma borel_measurable_indicator':
11.64 -  "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
11.65 -  using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
11.66 -
11.67 -lemma (in product_sigma_finite) distr_component:
11.68 -  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
11.69 -proof (intro measure_eqI[symmetric])
11.70 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
11.71 -
11.72 -  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
11.73 -    by (auto simp: extensional_def restrict_def)
11.74 -
11.75 -  fix A assume A: "A \<in> sets ?P"
11.76 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
11.77 -    by simp
11.78 -  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
11.79 -    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
11.80 -  also have "\<dots> = emeasure ?D A"
11.81 -    using A by (simp add: product_positive_integral_singleton emeasure_distr)
11.82 -  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
11.83 -qed simp
11.84 -
11.85 -lemma pair_measure_eqI:
11.86 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
11.87 -  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
11.88 -  assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
11.89 -  shows "M1 \<Otimes>\<^isub>M M2 = M"
11.90 -proof -
11.91 -  interpret M1: sigma_finite_measure M1 by fact
11.92 -  interpret M2: sigma_finite_measure M2 by fact
11.93 -  interpret pair_sigma_finite M1 M2 by default
11.94 -  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
11.95 -  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
11.96 -  let ?P = "M1 \<Otimes>\<^isub>M M2"
11.97 -  show ?thesis
11.98 -  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
11.99 -    show "?E \<subseteq> Pow (space ?P)"
11.100 -      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
11.101 -    show "sets ?P = sigma_sets (space ?P) ?E"
11.102 -      by (simp add: sets_pair_measure space_pair_measure)
11.103 -    then show "sets M = sigma_sets (space ?P) ?E"
11.104 -      using sets[symmetric] by simp
11.105 -  next
11.106 -    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
11.107 -      using F by (auto simp: space_pair_measure)
11.108 -  next
11.109 -    fix X assume "X \<in> ?E"
11.110 -    then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
11.111 -    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
11.112 -       by (simp add: M2.emeasure_pair_measure_Times)
11.113 -    also have "\<dots> = emeasure M (A \<times> B)"
11.114 -      using A B emeasure by auto
11.115 -    finally show "emeasure ?P X = emeasure M X"
11.116 -      by simp
11.117 -  qed
11.118 -qed
11.119 -
11.120 -lemma pair_measure_eq_distr_PiM:
11.121 -  fixes M1 :: "'a measure" and M2 :: "'a measure"
11.122 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
11.123 -  shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))"
11.124 -    (is "?P = ?D")
11.125 -proof (rule pair_measure_eqI[OF assms])
11.126 -  interpret B: product_sigma_finite "bool_case M1 M2"
11.127 -    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
11.128 -  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
11.129 -
11.130 -  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
11.131 -    by auto
11.132 -  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
11.133 -  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
11.134 -    by (simp add: UNIV_bool ac_simps)
11.135 -  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
11.136 -    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
11.137 -  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
11.138 -    using A[THEN sets_into_space] B[THEN sets_into_space]
11.139 -    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
11.140 -  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
11.141 -    using A B
11.142 -      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
11.143 -      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
11.144 -    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
11.145 -qed simp
11.146 -
11.147 -lemma measurable_Pair:
11.148 -  assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T"
11.149 -  shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
11.150 -proof -
11.151 -  have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)"
11.152 -    by auto
11.153 -  show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
11.154 -    by (auto simp: measurable_pair_iff rvs)
11.155 -qed
11.156 -
11.157  lemma (in prob_space) indep_var_distribution_eq:
11.158    "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
11.159      distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J")
```
```    12.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 18:49:46 2012 +0100
12.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 18:45:57 2012 +0100
12.3 @@ -9,16 +9,6 @@
12.4    imports Measure_Space Borel_Space
12.5  begin
12.6
12.7 -lemma ereal_minus_eq_PInfty_iff:
12.8 -  fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
12.9 -  by (cases x y rule: ereal2_cases) simp_all
12.10 -
12.11 -lemma real_ereal_1[simp]: "real (1::ereal) = 1"
12.12 -  unfolding one_ereal_def by simp
12.13 -
12.14 -lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
12.15 -  unfolding indicator_def by auto
12.16 -
12.17  lemma tendsto_real_max:
12.18    fixes x y :: real
12.19    assumes "(X ---> x) net"
12.20 @@ -42,11 +32,6 @@
12.21    then show ?thesis using assms by (auto intro: measurable_sets)
12.22  qed
12.23
12.24 -lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
12.25 -proof
12.26 -  assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
12.27 -qed (auto simp: incseq_def)
12.28 -
12.29  section "Simple function"
12.30
12.31  text {*
```
```    13.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
13.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
13.3 @@ -9,14 +9,32 @@
13.4    imports Finite_Product_Measure
13.5  begin
13.6
13.7 -lemma borel_measurable_indicator':
13.8 -  "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
13.9 -  using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
13.10 +lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
13.11 +  by metis
13.12 +
13.13 +lemma absolutely_integrable_on_indicator[simp]:
13.14 +  fixes A :: "'a::ordered_euclidean_space set"
13.15 +  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
13.16 +    (indicator A :: _ \<Rightarrow> real) integrable_on X"
13.17 +  unfolding absolutely_integrable_on_def by simp
13.18
13.19 -lemma borel_measurable_sets:
13.20 -  assumes "f \<in> measurable borel M" "A \<in> sets M"
13.21 -  shows "f -` A \<in> sets borel"
13.22 -  using measurable_sets[OF assms] by simp
13.23 +lemma has_integral_indicator_UNIV:
13.24 +  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
13.25 +  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
13.26 +proof -
13.27 +  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
13.28 +    by (auto simp: fun_eq_iff indicator_def)
13.29 +  then show ?thesis
13.30 +    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
13.31 +qed
13.32 +
13.33 +lemma
13.34 +  fixes s a :: "'a::ordered_euclidean_space set"
13.35 +  shows integral_indicator_UNIV:
13.36 +    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
13.37 +  and integrable_indicator_UNIV:
13.38 +    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
13.39 +  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
13.40
13.41  subsection {* Standard Cubes *}
13.42
13.43 @@ -62,6 +80,23 @@
13.44  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
13.45    unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
13.46
13.47 +lemma has_integral_interval_cube:
13.48 +  fixes a b :: "'a::ordered_euclidean_space"
13.49 +  shows "(indicator {a .. b} has_integral
13.50 +    content ({\<chi>\<chi> i. max (- real n) (a \$\$ i) .. \<chi>\<chi> i. min (real n) (b \$\$ i)} :: 'a set)) (cube n)"
13.51 +    (is "(?I has_integral content ?R) (cube n)")
13.52 +proof -
13.53 +  let "{?N .. ?P}" = ?R
13.54 +  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
13.55 +    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
13.56 +  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
13.57 +    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
13.58 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
13.59 +    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
13.60 +  finally show ?thesis
13.61 +    using has_integral_const[of "1::real" "?N" "?P"] by simp
13.62 +qed
13.63 +
13.64  subsection {* Lebesgue measure *}
13.65
13.66  definition lebesgue :: "'a::ordered_euclidean_space measure" where
13.67 @@ -74,26 +109,6 @@
13.68  lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
13.69    unfolding lebesgue_def by simp
13.70
13.71 -lemma absolutely_integrable_on_indicator[simp]:
13.72 -  fixes A :: "'a::ordered_euclidean_space set"
13.73 -  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
13.74 -    (indicator A :: _ \<Rightarrow> real) integrable_on X"
13.75 -  unfolding absolutely_integrable_on_def by simp
13.76 -
13.77 -lemma LIMSEQ_indicator_UN:
13.78 -  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
13.79 -proof cases
13.80 -  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
13.81 -  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
13.82 -    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
13.83 -  show ?thesis
13.84 -    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
13.85 -qed (auto simp: indicator_def)
13.86 -
13.88 -  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
13.89 -  unfolding indicator_def by auto
13.90 -
13.91  lemma sigma_algebra_lebesgue:
13.92    defines "leb \<equiv> {A. \<forall>n. (indicator A :: 'a::ordered_euclidean_space \<Rightarrow> real) integrable_on cube n}"
13.93    shows "sigma_algebra UNIV leb"
13.94 @@ -198,23 +213,6 @@
13.95    qed
13.96  qed (auto, fact)
13.97
13.98 -lemma has_integral_interval_cube:
13.99 -  fixes a b :: "'a::ordered_euclidean_space"
13.100 -  shows "(indicator {a .. b} has_integral
13.101 -    content ({\<chi>\<chi> i. max (- real n) (a \$\$ i) .. \<chi>\<chi> i. min (real n) (b \$\$ i)} :: 'a set)) (cube n)"
13.102 -    (is "(?I has_integral content ?R) (cube n)")
13.103 -proof -
13.104 -  let "{?N .. ?P}" = ?R
13.105 -  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
13.106 -    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
13.107 -  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
13.108 -    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
13.109 -  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
13.110 -    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
13.111 -  finally show ?thesis
13.112 -    using has_integral_const[of "1::real" "?N" "?P"] by simp
13.113 -qed
13.114 -
13.115  lemma lebesgueI_borel[intro, simp]:
13.116    fixes s::"'a::ordered_euclidean_space set"
13.117    assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
13.118 @@ -261,24 +259,6 @@
13.119      using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
13.120  qed
13.121
13.122 -lemma has_integral_indicator_UNIV:
13.123 -  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
13.124 -  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
13.125 -proof -
13.126 -  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
13.127 -    by (auto simp: fun_eq_iff indicator_def)
13.128 -  then show ?thesis
13.129 -    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
13.130 -qed
13.131 -
13.132 -lemma
13.133 -  fixes s a :: "'a::ordered_euclidean_space set"
13.134 -  shows integral_indicator_UNIV:
13.135 -    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
13.136 -  and integrable_indicator_UNIV:
13.137 -    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
13.138 -  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
13.139 -
13.140  lemma lmeasure_finite_has_integral:
13.141    fixes s :: "'a::ordered_euclidean_space set"
13.142    assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
13.143 @@ -429,11 +409,6 @@
13.144    qed
13.145  qed
13.146
13.147 -lemma integral_const[simp]:
13.148 -  fixes a b :: "'a::ordered_euclidean_space"
13.149 -  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
13.150 -  by (rule integral_unique) (rule has_integral_const)
13.151 -
13.152  lemma lmeasure_UNIV[intro]: "emeasure lebesgue (UNIV::'a::ordered_euclidean_space set) = \<infinity>"
13.153  proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI)
13.154    fix n :: nat
13.155 @@ -467,17 +442,6 @@
13.156      by (simp add: indicator_def [abs_def])
13.157  qed
13.158
13.159 -lemma atLeastAtMost_singleton_euclidean[simp]:
13.160 -  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
13.161 -  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
13.162 -
13.163 -lemma content_singleton[simp]: "content {a} = 0"
13.164 -proof -
13.165 -  have "content {a .. a} = 0"
13.166 -    by (subst content_closed_interval) auto
13.167 -  then show ?thesis by simp
13.168 -qed
13.169 -
13.170  lemma lmeasure_singleton[simp]:
13.171    fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
13.172    using lmeasure_atLeastAtMost[of a a] by simp
13.173 @@ -609,16 +573,6 @@
13.174
13.175  subsection {* Lebesgue integrable implies Gauge integrable *}
13.176
13.177 -lemma has_integral_cmult_real:
13.178 -  fixes c :: real
13.179 -  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
13.180 -  shows "((\<lambda>x. c * f x) has_integral c * x) A"
13.181 -proof cases
13.182 -  assume "c \<noteq> 0"
13.183 -  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
13.184 -    unfolding real_scaleR_def .
13.185 -qed simp
13.186 -
13.187  lemma simple_function_has_integral:
13.188    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
13.189    assumes f:"simple_function lebesgue f"
13.190 @@ -657,10 +611,6 @@
13.191    finally show "((\<lambda>x. real (\<Sum>y\<in>range f. y * ?F y x)) has_integral real (\<Sum>x\<in>range f. x * ?M x)) UNIV" .
13.192  qed fact
13.193
13.194 -lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
13.195 -  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
13.196 -  using assms by auto
13.197 -
13.198  lemma simple_function_has_integral':
13.199    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
13.200    assumes f: "simple_function lebesgue f" "\<And>x. 0 \<le> f x"
13.201 @@ -695,9 +645,6 @@
13.202    qed
13.203  qed
13.204
13.205 -lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
13.206 -  by (auto simp: indicator_def one_ereal_def)
13.207 -
13.208  lemma positive_integral_has_integral:
13.209    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
13.210    assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
13.211 @@ -843,12 +790,6 @@
13.212      unfolding lebesgue_integral_eq_borel[OF borel] by simp
13.213  qed
13.214
13.215 -lemma integrable_on_cmult_iff:
13.216 -  fixes c :: real assumes "c \<noteq> 0"
13.217 -  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
13.218 -  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
13.219 -  by auto
13.220 -
13.221  lemma positive_integral_lebesgue_has_integral:
13.222    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
13.223    assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
13.224 @@ -983,9 +924,6 @@
13.225  interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
13.226    by default auto
13.227
13.228 -lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
13.229 -  by metis
13.230 -
13.231  lemma sets_product_borel:
13.232    assumes I: "finite I"
13.233    shows "sets (\<Pi>\<^isub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^isub>E i\<in>I. UNIV) { \<Pi>\<^isub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
```
```    14.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Nov 16 18:49:46 2012 +0100
14.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Nov 16 18:45:57 2012 +0100
14.3 @@ -18,6 +18,28 @@
14.4    apply (subst LIMSEQ_Suc_iff[symmetric])
14.5    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
14.6
14.7 +subsection "Relate extended reals and the indicator function"
14.8 +
14.9 +lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
14.10 +  by (auto simp: indicator_def one_ereal_def)
14.11 +
14.12 +lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
14.13 +  unfolding indicator_def by auto
14.14 +
14.15 +lemma LIMSEQ_indicator_UN:
14.16 +  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
14.17 +proof cases
14.18 +  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
14.19 +  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
14.20 +    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
14.21 +  show ?thesis
14.22 +    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
14.23 +qed (auto simp: indicator_def)
14.24 +
14.26 +  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
14.27 +  unfolding indicator_def by auto
14.28 +
14.29  lemma suminf_cmult_indicator:
14.30    fixes f :: "nat \<Rightarrow> ereal"
14.31    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
14.32 @@ -111,7 +133,7 @@
14.33    "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> f x \<le> f y"
14.34    by (auto simp add: increasing_def)
14.35
14.38    "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
14.41 @@ -1114,6 +1136,9 @@
14.42    show "sigma_algebra (space N) (sets N)" ..
14.43  qed fact
14.44
14.45 +lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
14.46 +  by (rule measure_eqI) (auto simp: emeasure_distr)
14.47 +
14.48  lemma measure_distr:
14.49    "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
14.50    by (simp add: emeasure_distr measure_def)
14.51 @@ -1389,6 +1414,107 @@
14.52    shows "measure M A = measure M B"
14.53    using assms emeasure_eq_AE[OF assms] by (simp add: emeasure_eq_measure)
14.54
14.55 +lemma (in finite_measure) measure_increasing: "increasing M (measure M)"
14.56 +  by (auto intro!: finite_measure_mono simp: increasing_def)
14.57 +
14.58 +lemma (in finite_measure) measure_zero_union:
14.59 +  assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
14.60 +  shows "measure M (s \<union> t) = measure M s"
14.61 +using assms
14.62 +proof -
14.63 +  have "measure M (s \<union> t) \<le> measure M s"
14.64 +    using finite_measure_subadditive[of s t] assms by auto
14.65 +  moreover have "measure M (s \<union> t) \<ge> measure M s"
14.66 +    using assms by (blast intro: finite_measure_mono)
14.67 +  ultimately show ?thesis by simp
14.68 +qed
14.69 +
14.70 +lemma (in finite_measure) measure_eq_compl:
14.71 +  assumes "s \<in> sets M" "t \<in> sets M"
14.72 +  assumes "measure M (space M - s) = measure M (space M - t)"
14.73 +  shows "measure M s = measure M t"
14.74 +  using assms finite_measure_compl by auto
14.75 +
14.76 +lemma (in finite_measure) measure_eq_bigunion_image:
14.77 +  assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
14.78 +  assumes "disjoint_family f" "disjoint_family g"
14.79 +  assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
14.80 +  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
14.81 +using assms
14.82 +proof -
14.83 +  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
14.84 +    by (rule finite_measure_UNION[OF assms(1,3)])
14.85 +  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
14.86 +    by (rule finite_measure_UNION[OF assms(2,4)])
14.87 +  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
14.88 +qed
14.89 +
14.90 +lemma (in finite_measure) measure_countably_zero:
14.91 +  assumes "range c \<subseteq> sets M"
14.92 +  assumes "\<And> i. measure M (c i) = 0"
14.93 +  shows "measure M (\<Union> i :: nat. c i) = 0"
14.94 +proof (rule antisym)
14.95 +  show "measure M (\<Union> i :: nat. c i) \<le> 0"
14.98 +
14.99 +lemma (in finite_measure) measure_space_inter:
14.100 +  assumes events:"s \<in> sets M" "t \<in> sets M"
14.101 +  assumes "measure M t = measure M (space M)"
14.102 +  shows "measure M (s \<inter> t) = measure M s"
14.103 +proof -
14.104 +  have "measure M ((space M - s) \<union> (space M - t)) = measure M (space M - s)"
14.105 +    using events assms finite_measure_compl[of "t"] by (auto intro!: measure_zero_union)
14.106 +  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
14.107 +    by blast
14.108 +  finally show "measure M (s \<inter> t) = measure M s"
14.109 +    using events by (auto intro!: measure_eq_compl[of "s \<inter> t" s])
14.110 +qed
14.111 +
14.112 +lemma (in finite_measure) measure_equiprobable_finite_unions:
14.113 +  assumes s: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> sets M"
14.114 +  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> measure M {x} = measure M {y}"
14.115 +  shows "measure M s = real (card s) * measure M {SOME x. x \<in> s}"
14.116 +proof cases
14.117 +  assume "s \<noteq> {}"
14.118 +  then have "\<exists> x. x \<in> s" by blast
14.119 +  from someI_ex[OF this] assms
14.120 +  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> measure M {x} = measure M {SOME y. y \<in> s}" by blast
14.121 +  have "measure M s = (\<Sum> x \<in> s. measure M {x})"
14.122 +    using finite_measure_eq_setsum_singleton[OF s] by simp
14.123 +  also have "\<dots> = (\<Sum> x \<in> s. measure M {SOME y. y \<in> s})" using prob_some by auto
14.124 +  also have "\<dots> = real (card s) * measure M {(SOME x. x \<in> s)}"
14.125 +    using setsum_constant assms by (simp add: real_eq_of_nat)
14.126 +  finally show ?thesis by simp
14.127 +qed simp
14.128 +
14.129 +lemma (in finite_measure) measure_real_sum_image_fn:
14.130 +  assumes "e \<in> sets M"
14.131 +  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
14.132 +  assumes "finite s"
14.133 +  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
14.134 +  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
14.135 +  shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
14.136 +proof -
14.137 +  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
14.138 +    using `e \<in> sets M` sets_into_space upper by blast
14.139 +  hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
14.140 +  also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
14.141 +  proof (rule finite_measure_finite_Union)
14.142 +    show "finite s" by fact
14.143 +    show "(\<lambda>i. e \<inter> f i)`s \<subseteq> sets M" using assms(2) by auto
14.144 +    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
14.145 +      using disjoint by (auto simp: disjoint_family_on_def)
14.146 +  qed
14.147 +  finally show ?thesis .
14.148 +qed
14.149 +
14.150 +lemma (in finite_measure) measure_exclude:
14.151 +  assumes "A \<in> sets M" "B \<in> sets M"
14.152 +  assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
14.153 +  shows "measure M B = 0"
14.154 +  using measure_space_inter[of B A] assms by (auto simp: ac_simps)
14.155 +
14.156  section {* Counting space *}
14.157
14.158  lemma strict_monoI_Suc:
```
```    15.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
15.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
15.3 @@ -9,125 +9,6 @@
15.5  begin
15.6
15.7 -lemma funset_eq_UN_fun_upd_I:
15.8 -  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
15.9 -  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
15.10 -  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
15.11 -  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
15.12 -proof safe
15.13 -  fix f assume f: "f \<in> F (insert a A)"
15.14 -  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
15.15 -  proof (rule UN_I[of "f(a := d)"])
15.16 -    show "f(a := d) \<in> F A" using *[OF f] .
15.17 -    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
15.18 -    proof (rule image_eqI[of _ _ "f a"])
15.19 -      show "f a \<in> G (f(a := d))" using **[OF f] .
15.20 -    qed simp
15.21 -  qed
15.22 -next
15.23 -  fix f x assume "f \<in> F A" "x \<in> G f"
15.24 -  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
15.25 -qed
15.26 -
15.27 -lemma extensional_funcset_insert_eq[simp]:
15.28 -  assumes "a \<notin> A"
15.29 -  shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
15.30 -  apply (rule funset_eq_UN_fun_upd_I)
15.31 -  using assms
15.32 -  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
15.33 -
15.34 -lemma finite_extensional_funcset[simp, intro]:
15.35 -  assumes "finite A" "finite B"
15.36 -  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
15.37 -  using assms by induct auto
15.38 -
15.39 -lemma finite_PiE[simp, intro]:
15.40 -  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
15.41 -  shows "finite (Pi\<^isub>E A B)"
15.42 -proof -
15.43 -  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
15.44 -  show ?thesis
15.45 -    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
15.46 -qed
15.47 -
15.48 -
15.50 -  assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
15.51 -  shows "countably_additive M \<mu>"
15.52 -  using assms unfolding countably_additive_def by auto
15.53 -
15.54 -lemma convex_le_Inf_differential:
15.55 -  fixes f :: "real \<Rightarrow> real"
15.56 -  assumes "convex_on I f"
15.57 -  assumes "x \<in> interior I" "y \<in> I"
15.58 -  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
15.59 -    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
15.60 -proof -
15.61 -  show ?thesis
15.62 -  proof (cases rule: linorder_cases)
15.63 -    assume "x < y"
15.64 -    moreover
15.65 -    have "open (interior I)" by auto
15.66 -    from openE[OF this `x \<in> interior I`] guess e . note e = this
15.67 -    moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
15.68 -    ultimately have "x < t" "t < y" "t \<in> ball x e"
15.69 -      by (auto simp: dist_real_def field_simps split: split_min)
15.70 -    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
15.71 -
15.72 -    have "open (interior I)" by auto
15.73 -    from openE[OF this `x \<in> interior I`] guess e .
15.74 -    moreover def K \<equiv> "x - e / 2"
15.75 -    with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
15.76 -    ultimately have "K \<in> I" "K < x" "x \<in> I"
15.77 -      using interior_subset[of I] `x \<in> interior I` by auto
15.78 -
15.79 -    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
15.80 -    proof (rule Inf_lower2)
15.81 -      show "(f x - f t) / (x - t) \<in> ?F x"
15.82 -        using `t \<in> I` `x < t` by auto
15.83 -      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
15.84 -        using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
15.85 -    next
15.86 -      fix y assume "y \<in> ?F x"
15.87 -      with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
15.88 -      show "(f K - f x) / (K - x) \<le> y" by auto
15.89 -    qed
15.90 -    then show ?thesis
15.91 -      using `x < y` by (simp add: field_simps)
15.92 -  next
15.93 -    assume "y < x"
15.94 -    moreover
15.95 -    have "open (interior I)" by auto
15.96 -    from openE[OF this `x \<in> interior I`] guess e . note e = this
15.97 -    moreover def t \<equiv> "x + e / 2"
15.98 -    ultimately have "x < t" "t \<in> ball x e"
15.99 -      by (auto simp: dist_real_def field_simps)
15.100 -    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
15.101 -
15.102 -    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
15.103 -    proof (rule Inf_greatest)
15.104 -      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
15.105 -        using `y < x` by (auto simp: field_simps)
15.106 -      also
15.107 -      fix z  assume "z \<in> ?F x"
15.108 -      with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
15.109 -      have "(f y - f x) / (y - x) \<le> z" by auto
15.110 -      finally show "(f x - f y) / (x - y) \<le> z" .
15.111 -    next
15.112 -      have "open (interior I)" by auto
15.113 -      from openE[OF this `x \<in> interior I`] guess e . note e = this
15.114 -      then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
15.115 -      with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
15.116 -      then show "?F x \<noteq> {}" by blast
15.117 -    qed
15.118 -    then show ?thesis
15.119 -      using `y < x` by (simp add: field_simps)
15.120 -  qed simp
15.121 -qed
15.122 -
15.123 -lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
15.124 -  by (rule measure_eqI) (auto simp: emeasure_distr)
15.125 -
15.126  locale prob_space = finite_measure +
15.127    assumes emeasure_space_1: "emeasure M (space M) = 1"
15.128
15.129 @@ -230,101 +111,6 @@
15.130    then show False by auto
15.131  qed
15.132
15.133 -lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
15.134 -  by (auto intro!: finite_measure_mono simp: increasing_def)
15.135 -
15.136 -lemma (in finite_measure) prob_zero_union:
15.137 -  assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
15.138 -  shows "measure M (s \<union> t) = measure M s"
15.139 -using assms
15.140 -proof -
15.141 -  have "measure M (s \<union> t) \<le> measure M s"
15.142 -    using finite_measure_subadditive[of s t] assms by auto
15.143 -  moreover have "measure M (s \<union> t) \<ge> measure M s"
15.144 -    using assms by (blast intro: finite_measure_mono)
15.145 -  ultimately show ?thesis by simp
15.146 -qed
15.147 -
15.148 -lemma (in finite_measure) prob_eq_compl:
15.149 -  assumes "s \<in> sets M" "t \<in> sets M"
15.150 -  assumes "measure M (space M - s) = measure M (space M - t)"
15.151 -  shows "measure M s = measure M t"
15.152 -  using assms finite_measure_compl by auto
15.153 -
15.154 -lemma (in prob_space) prob_one_inter:
15.155 -  assumes events:"s \<in> events" "t \<in> events"
15.156 -  assumes "prob t = 1"
15.157 -  shows "prob (s \<inter> t) = prob s"
15.158 -proof -
15.159 -  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
15.160 -    using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)
15.161 -  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
15.162 -    by blast
15.163 -  finally show "prob (s \<inter> t) = prob s"
15.164 -    using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
15.165 -qed
15.166 -
15.167 -lemma (in finite_measure) prob_eq_bigunion_image:
15.168 -  assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
15.169 -  assumes "disjoint_family f" "disjoint_family g"
15.170 -  assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
15.171 -  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
15.172 -using assms
15.173 -proof -
15.174 -  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
15.175 -    by (rule finite_measure_UNION[OF assms(1,3)])
15.176 -  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
15.177 -    by (rule finite_measure_UNION[OF assms(2,4)])
15.178 -  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
15.179 -qed
15.180 -
15.181 -lemma (in finite_measure) prob_countably_zero:
15.182 -  assumes "range c \<subseteq> sets M"
15.183 -  assumes "\<And> i. measure M (c i) = 0"
15.184 -  shows "measure M (\<Union> i :: nat. c i) = 0"
15.185 -proof (rule antisym)
15.186 -  show "measure M (\<Union> i :: nat. c i) \<le> 0"
15.189 -
15.190 -lemma (in prob_space) prob_equiprobable_finite_unions:
15.191 -  assumes "s \<in> events"
15.192 -  assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
15.193 -  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
15.194 -  shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
15.195 -proof (cases "s = {}")
15.196 -  case False hence "\<exists> x. x \<in> s" by blast
15.197 -  from someI_ex[OF this] assms
15.198 -  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
15.199 -  have "prob s = (\<Sum> x \<in> s. prob {x})"
15.200 -    using finite_measure_eq_setsum_singleton[OF s_finite] by simp
15.201 -  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
15.202 -  also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
15.203 -    using setsum_constant assms by (simp add: real_eq_of_nat)
15.204 -  finally show ?thesis by simp
15.205 -qed simp
15.206 -
15.207 -lemma (in prob_space) prob_real_sum_image_fn:
15.208 -  assumes "e \<in> events"
15.209 -  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
15.210 -  assumes "finite s"
15.211 -  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
15.212 -  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
15.213 -  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
15.214 -proof -
15.215 -  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
15.216 -    using `e \<in> events` sets_into_space upper by blast
15.217 -  hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
15.218 -  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
15.219 -  proof (rule finite_measure_finite_Union)
15.220 -    show "finite s" by fact
15.221 -    show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto
15.222 -    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
15.223 -      using disjoint by (auto simp: disjoint_family_on_def)
15.224 -  qed
15.225 -  finally show ?thesis .
15.226 -qed
15.227 -
15.228  lemma (in prob_space) expectation_less:
15.229    assumes [simp]: "integrable M X"
15.230    assumes gt: "AE x in M. X x < b"
15.231 @@ -398,14 +184,6 @@
15.232    finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
15.233  qed
15.234
15.235 -lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0:
15.236 -  assumes "{x} \<in> events"
15.237 -  assumes "prob {x} = 1"
15.238 -  assumes "{y} \<in> events"
15.239 -  assumes "y \<noteq> x"
15.240 -  shows "prob {y} = 0"
15.241 -  using prob_one_inter[of "{y}" "{x}"] assms by auto
15.242 -
15.243  subsection  {* Introduce binder for probability *}
15.244
15.245  syntax
```
```    16.1 --- a/src/HOL/Product_Type.thy	Fri Nov 16 18:49:46 2012 +0100
16.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 16 18:45:57 2012 +0100
16.3 @@ -393,6 +393,9 @@
16.4    from `PROP P (fst x, snd x)` show "PROP P x" by simp
16.5  qed
16.6
16.7 +lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
16.8 +  by (cases x) simp
16.9 +
16.10  text {*
16.11    The rule @{thm [source] split_paired_all} does not work with the
16.12    Simplifier because it also affects premises in congrence rules,
16.13 @@ -495,6 +498,10 @@
16.14  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
16.15    by (subst surjective_pairing, rule split_conv)
16.16
16.17 +lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
16.18 +  by (auto simp: fun_eq_iff)
16.19 +
16.20 +
16.21  lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
16.22    -- {* For use with @{text split} and the Simplifier. *}
16.23    by (insert surj_pair [of p], clarify, simp)
16.24 @@ -1019,6 +1026,9 @@
16.25  lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
16.26    by auto
16.27
16.28 +lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
16.29 +  by auto
16.30 +
16.31  lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
16.32    by force
16.33
16.34 @@ -1036,6 +1046,9 @@
16.35    apply auto
16.36    done
16.37
16.38 +lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
16.39 +  by auto
16.40 +
16.41  lemma swap_inj_on:
16.42    "inj_on (\<lambda>(i, j). (j, i)) A"
16.43    by (auto intro!: inj_onI)
```