diff -r 3d89c38408cd -r de19856feb54 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:45:57 2012 +0100
@@ -18,9 +18,6 @@
 definition (in prob_space)
   indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
 
-lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
-  by auto
-
 lemma (in prob_space) indep_events_def:
   "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
     (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
@@ -827,31 +824,6 @@
     using I by auto
 qed fact+
 
-lemma prod_algebra_cong:
-  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
-  shows "prod_algebra I M = prod_algebra J N"
-proof -
-  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
-    using sets_eq_imp_space_eq[OF sets] by auto
-  with sets show ?thesis unfolding `I = J`
-    by (intro antisym prod_algebra_mono) auto
-qed
-
-lemma space_in_prod_algebra:
-  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
-proof cases
-  assume "I = {}" then show ?thesis
-    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
-next
-  assume "I \<noteq> {}"
-  then obtain i where "i \<in> I" by auto
-  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))"
-    by (auto simp: prod_emb_def Pi_iff)
-  also have "\<dots> \<in> prod_algebra I M"
-    using `i \<in> I` by (intro prod_algebraI) auto
-  finally show ?thesis .
-qed
-
 lemma (in prob_space) indep_vars_iff_distr_eq_PiM:
   fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
   assumes "I \<noteq> {}"
@@ -972,114 +944,6 @@
     unfolding UNIV_bool by auto
 qed
 
-lemma measurable_bool_case[simp, intro]:
-  "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))"
-    (is "?f \<in> measurable ?B ?P")
-proof (rule measurable_PiM_single)
-  show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))"
-    by (auto simp: space_pair_measure extensional_def split: bool.split)
-  fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)"
-  moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A}
-    = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)" 
-    by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space)
-  ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B"
-    by (auto split: bool.split)
-qed
-
-lemma borel_measurable_indicator':
-  "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
-  using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
-
-lemma (in product_sigma_finite) distr_component:
-  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
-proof (intro measure_eqI[symmetric])
-  interpret I: finite_product_sigma_finite M "{i}" by default simp
-
-  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
-    by (auto simp: extensional_def restrict_def)
-
-  fix A assume A: "A \<in> sets ?P"
-  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
-    by simp
-  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)" 
-    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
-  also have "\<dots> = emeasure ?D A"
-    using A by (simp add: product_positive_integral_singleton emeasure_distr)
-  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
-qed simp
-
-lemma pair_measure_eqI:
-  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
-  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
-  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)"
-  shows "M1 \<Otimes>\<^isub>M M2 = M"
-proof -
-  interpret M1: sigma_finite_measure M1 by fact
-  interpret M2: sigma_finite_measure M2 by fact
-  interpret pair_sigma_finite M1 M2 by default
-  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
-  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
-  let ?P = "M1 \<Otimes>\<^isub>M M2"
-  show ?thesis
-  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
-    show "?E \<subseteq> Pow (space ?P)"
-      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
-    show "sets ?P = sigma_sets (space ?P) ?E"
-      by (simp add: sets_pair_measure space_pair_measure)
-    then show "sets M = sigma_sets (space ?P) ?E"
-      using sets[symmetric] by simp
-  next
-    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
-      using F by (auto simp: space_pair_measure)
-  next
-    fix X assume "X \<in> ?E"
-    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
-    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
-       by (simp add: M2.emeasure_pair_measure_Times)
-    also have "\<dots> = emeasure M (A \<times> B)"
-      using A B emeasure by auto
-    finally show "emeasure ?P X = emeasure M X"
-      by simp
-  qed
-qed
-
-lemma pair_measure_eq_distr_PiM:
-  fixes M1 :: "'a measure" and M2 :: "'a measure"
-  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
-  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))"
-    (is "?P = ?D")
-proof (rule pair_measure_eqI[OF assms])
-  interpret B: product_sigma_finite "bool_case M1 M2"
-    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
-  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
-
-  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)"
-    by auto
-  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
-  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
-    by (simp add: UNIV_bool ac_simps)
-  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
-    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
-  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
-    using A[THEN sets_into_space] B[THEN sets_into_space]
-    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
-  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
-    using A B
-      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
-      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
-    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
-qed simp
-
-lemma measurable_Pair:
-  assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T"
-  shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
-proof -
-  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)"
-    by auto
-  show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
-    by (auto simp: measurable_pair_iff rvs)
-qed
-
 lemma (in prob_space) indep_var_distribution_eq:
   "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
     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")