# HG changeset patch
# User hoelzl
# Date 1349863941 -7200
# Node ID 92a58f80b20cd2216de9d47f9b3b9a58ee91318e
# Parent  1484b4b828558277705479efffb38fda3e2521ad
merge should operate on pairs

diff -r 1484b4b82855 -r 92a58f80b20c src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:20 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:21 2012 +0200
@@ -44,45 +44,45 @@
   unfolding extensional_def by auto
 
 definition
-  "merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
+  "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
 
 lemma merge_apply[simp]:
-  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
-  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
-  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
-  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
-  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined"
+  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
+  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
+  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
+  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
+  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined"
   unfolding merge_def by auto
 
 lemma merge_commute:
-  "I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x"
+  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
   by (auto simp: merge_def intro!: ext)
 
 lemma Pi_cancel_merge_range[simp]:
-  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
-  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
-  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
-  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
+  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
+  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
+  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
+  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
   by (auto simp: Pi_def)
 
 lemma Pi_cancel_merge[simp]:
-  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
-  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
-  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
-  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
+  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
+  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
+  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
+  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
   by (auto simp: Pi_def)
 
-lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)"
+lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
   by (auto simp: extensional_def)
 
 lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
   by (auto simp: restrict_def Pi_def)
 
 lemma restrict_merge[simp]:
-  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
-  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
-  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
-  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
+  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
+  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
+  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
+  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
   by (auto simp: restrict_def)
 
 lemma extensional_insert_undefined[intro, simp]:
@@ -95,7 +95,7 @@
   shows "a \<in> extensional (insert i I)"
   using assms unfolding extensional_def by auto
 
-lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
+lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
   unfolding merge_def by (auto simp: fun_eq_iff)
 
 lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
@@ -118,24 +118,24 @@
 
 lemma restrict_vimage:
   assumes "I \<inter> J = {}"
-  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
+  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
   using assms by (auto simp: restrict_Pi_cancel)
 
 lemma merge_vimage:
   assumes "I \<inter> J = {}"
-  shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
+  shows "merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   using assms by (auto simp: restrict_Pi_cancel)
 
 lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   by (auto simp: restrict_def)
 
 lemma merge_restrict[simp]:
-  "merge I (restrict x I) J y = merge I x J y"
-  "merge I x J (restrict y J) = merge I x J y"
+  "merge I J (restrict x I, y) = merge I J (x, y)"
+  "merge I J (x, restrict y J) = merge I J (x, y)"
   unfolding merge_def by auto
 
 lemma merge_x_x_eq_restrict[simp]:
-  "merge I x J x = restrict x (I \<union> J)"
+  "merge I J (x, x) = restrict x (I \<union> J)"
   unfolding merge_def by auto
 
 lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
@@ -518,17 +518,17 @@
 qed (auto simp: space_pair_measure space_PiM)
 
 lemma measurable_merge:
-  "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
+  "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
     (is "?f \<in> measurable ?P ?U")
 proof (rule measurable_PiM_single)
   fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
-  then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} =
+  then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
     (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
     by (auto simp: merge_def)
   also have "\<dots> \<in> sets ?P"
     using A
     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
-  finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} \<in> sets ?P" .
+  finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
 qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
 
 lemma measurable_restrict:
@@ -585,29 +585,34 @@
   qed
 qed
 
+lemma
+  shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
+    and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
+  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
+
+lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
+proof -
+  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
+  have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
+  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
+    show "positive (PiM {} M) ?\<mu>"
+      by (auto simp: positive_def)
+    show "countably_additive (PiM {} M) ?\<mu>"
+      by (rule countably_additiveI_finite)
+         (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
+  qed (auto simp: prod_emb_def)
+  also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
+    by (auto simp: prod_emb_def)
+  finally show ?thesis
+    by simp
+qed
+
+lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
+  by (rule measure_eqI) (auto simp add: sets_PiM_empty one_ereal_def)
+
 lemma (in product_sigma_finite) emeasure_PiM:
   "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
 proof (induct I arbitrary: A rule: finite_induct)
-  case empty
-  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
-  have "prod_algebra {} M = {{\<lambda>_. undefined}}"
-    by (auto simp: prod_algebra_def prod_emb_def intro!: image_eqI)
-  then have sets_empty: "sets (PiM {} M) = {{}, {\<lambda>_. undefined}}"
-    by (simp add: sets_PiM)
-  have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
-  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
-    have "finite (space (PiM {} M))"
-      by (simp add: space_PiM)
-    moreover show "positive (PiM {} M) ?\<mu>"
-      by (auto simp: positive_def)
-    ultimately show "countably_additive (PiM {} M) ?\<mu>"
-      by (rule countably_additiveI_finite) (auto simp: additive_def space_PiM sets_empty)
-  qed (auto simp: prod_emb_def)
-  also have *: "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
-    by (auto simp: prod_emb_def)
-  finally show ?case
-    using * by simp
-next
   case (insert i I)
   interpret finite_product_sigma_finite M I by default fact
   have "finite (insert i I)" using `finite I` by auto
@@ -660,7 +665,7 @@
   qed (auto intro!: setprod_cong)
   with insert show ?case
     by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
-qed
+qed (simp add: emeasure_PiM_empty)
 
 lemma (in product_sigma_finite) sigma_finite: 
   assumes "finite I"
@@ -696,18 +701,6 @@
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^isub>M I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   using emeasure_PiM[OF finite_index] by auto
 
-lemma (in product_sigma_finite) product_measure_empty[simp]:
-  "emeasure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
-proof -
-  interpret finite_product_sigma_finite M "{}" by default auto
-  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
-qed
-
-lemma
-  shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
-    and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
-  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
-
 lemma (in product_sigma_finite) positive_integral_empty:
   assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
@@ -727,7 +720,7 @@
 
 lemma (in product_sigma_finite) distr_merge:
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
-  shows "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M) (\<lambda>(x,y). merge I x J y) = Pi\<^isub>M (I \<union> J) M"
+  shows "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M) (merge I J) = Pi\<^isub>M (I \<union> J) M"
    (is "?D = ?P")
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
@@ -735,7 +728,7 @@
   have "finite (I \<union> J)" using fin by auto
   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
-  let ?g = "\<lambda>(x,y). merge I x J y"
+  let ?g = "merge I J"
 
   from IJ.sigma_finite_pairs obtain F where
     F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
@@ -793,12 +786,12 @@
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
-    (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
+    (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
   interpret J: finite_product_sigma_finite M J by default fact
   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
-  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
+  have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
     using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   show ?thesis
     apply (subst distr_merge[OF IJ, symmetric])
@@ -833,7 +826,7 @@
 qed
 
 lemma (in product_sigma_finite) product_positive_integral_insert:
-  assumes [simp]: "finite I" "i \<notin> I"
+  assumes I[simp]: "finite I" "i \<notin> I"
     and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
   shows "integral\<^isup>P (Pi\<^isub>M (insert i I) M) f = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^isub>M I M))"
 proof -
@@ -842,17 +835,17 @@
   have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
     using f by auto
   show ?thesis
-    unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
-  proof (rule positive_integral_cong, subst product_positive_integral_singleton)
+    unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
+  proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
     fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
-    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
-    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
-      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def space_PiM)
-    show "?f \<in> borel_measurable (M i)" unfolding f'_eq
+    let ?f = "\<lambda>y. f (x(i := y))"
+    show "?f \<in> borel_measurable (M i)"
       using measurable_comp[OF measurable_component_update f, OF x `i \<notin> I`]
       unfolding comp_def .
-    show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
-      unfolding f'_eq by simp
+    show "(\<integral>\<^isup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^isub>M {i} M) = (\<integral>\<^isup>+ y. f (x(i := y i)) \<partial>Pi\<^isub>M {i} M)"
+      using x
+      by (auto intro!: positive_integral_cong arg_cong[where f=f]
+               simp add: space_PiM extensional_def)
   qed
 qed
 
@@ -895,18 +888,18 @@
 lemma (in product_sigma_finite) product_integral_fold:
   assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
-  shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I x J y) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
+  shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
   interpret J: finite_product_sigma_finite M J by default fact
   have "finite (I \<union> J)" using fin by auto
   interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
-  let ?M = "\<lambda>(x, y). merge I x J y"
+  let ?M = "merge I J"
   let ?f = "\<lambda>x. f (?M x)"
   from f have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
     by auto
-  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
+  have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
     using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
   have f_int: "integrable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ?f"
     by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
@@ -921,14 +914,14 @@
 lemma (in product_sigma_finite)
   assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   shows emeasure_fold_integral:
-    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
+    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
     and emeasure_fold_measurable:
-    "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
+    "(\<lambda>x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
 proof -
   interpret I: finite_product_sigma_finite M I by default fact
   interpret J: finite_product_sigma_finite M J by default fact
   interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
-  have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
+  have merge: "merge I J -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
     by (intro measurable_sets[OF _ A] measurable_merge assms)
 
   show ?I
@@ -950,7 +943,7 @@
 proof -
   have "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = integral\<^isup>L (Pi\<^isub>M (I \<union> {i}) M) f"
     by simp
-  also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
+  also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
     using f I by (intro product_integral_fold) auto
   also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
   proof (rule integral_cong, subst product_integral_singleton[symmetric])
@@ -960,7 +953,7 @@
     show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
       using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
       unfolding comp_def .
-    from x I show "(\<integral> y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
+    from x I show "(\<integral> y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
       by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
   qed
   finally show ?thesis .
@@ -998,22 +991,24 @@
 
 lemma (in product_sigma_finite) product_integral_setprod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
-  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
+  assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^isub>M I M) = (\<Prod>i\<in>I. integral\<^isup>L (M i) (f i))"
-using assms proof (induct rule: finite_ne_induct)
-  case (singleton i)
-  then show ?case by (simp add: product_integral_singleton integrable_def)
+using assms proof induct
+  case empty
+  interpret finite_measure "Pi\<^isub>M {} M"
+    by rule (simp add: space_PiM)
+  show ?case by (simp add: space_PiM measure_def)
 next
   case (insert i I)
   then have iI: "finite (insert i I)" by auto
   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
     integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
-    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
+    by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
   interpret I: finite_product_sigma_finite M I by default fact
   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
     using `i \<notin> I` by (auto intro!: setprod_cong)
   show ?case
-    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
+    unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
     by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
 qed
 
diff -r 1484b4b82855 -r 92a58f80b20c src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:20 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:21 2012 +0200
@@ -14,10 +14,10 @@
 lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
   unfolding restrict_def by (simp add: fun_eq_iff)
 
-lemma split_merge: "P (merge I x J y i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
+lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
   unfolding merge_def by auto
 
-lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I x J y \<in> extensional K"
+lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
   unfolding merge_def extensional_def by auto
 
 lemma injective_vimage_restrict:
@@ -32,7 +32,7 @@
   show "x \<in> A \<longleftrightarrow> x \<in> B"
   proof cases
     assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
-    have "x \<in> A \<longleftrightarrow> merge J x (I - J) y \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
+    have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
       using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
     then show "x \<in> A \<longleftrightarrow> x \<in> B"
       using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
@@ -131,7 +131,7 @@
   show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
     using sets[THEN sets_into_space] by (auto simp: space_PiM)
   have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
-    using M.not_empty by auto
+      using M.not_empty by auto
   from bchoice[OF this]
   show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
   show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
@@ -230,23 +230,19 @@
 qed
 
 lemma (in product_prob_space) merge_sets:
-  assumes "finite J" "finite K" "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
-  shows "merge J x K -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
-proof -
-  from sets_Pair1[OF
-    measurable_merge[THEN measurable_sets, OF `J \<inter> K = {}`], OF A, of x] x
-  show ?thesis
-      by (simp add: space_pair_measure comp_def vimage_compose[symmetric])
-qed
+  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
+  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
+  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]  
+           measurable_const x measurable_ident)+
 
 lemma (in product_prob_space) merge_emb:
   assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
-  shows "(merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
-    emb I (K - J) (merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
+  shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
+    emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
 proof -
-  have [simp]: "\<And>x J K L. merge J y K (restrict x L) = merge J y (K \<inter> L) x"
+  have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
     by (auto simp: restrict_def merge_def)
-  have [simp]: "\<And>x J K L. restrict (merge J y K x) L = merge (J \<inter> L) y (K \<inter> L) x"
+  have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
     by (auto simp: restrict_def merge_def)
   have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
   have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
@@ -331,16 +327,16 @@
       "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^isub>M K M) X"
       by (auto simp: subset_insertI)
 
-    let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
+    let ?M = "\<lambda>y. (\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
     { fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
       note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
       moreover
       have **: "?M y \<in> sets (Pi\<^isub>M (K - J) M)"
         using J K y by (intro merge_sets) auto
       ultimately
-      have ***: "(merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
+      have ***: "((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
         using J K by (intro generatorI) auto
-      have "\<mu>G (merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
+      have "\<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
         unfolding * using K J by (subst \<mu>G_eq[OF _ _ _ **]) auto
       note * ** *** this }
     note merge_in_G = this
@@ -354,7 +350,7 @@
       using K J by simp
     also have "\<dots> = (\<integral>\<^isup>+ x. emeasure (Pi\<^isub>M (K - J) M) (?M x) \<partial>Pi\<^isub>M J M)"
       using K J by (subst emeasure_fold_integral) auto
-    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
+    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
       (is "_ = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)")
     proof (intro positive_integral_cong)
       fix x assume x: "x \<in> space (Pi\<^isub>M J M)"
@@ -370,7 +366,7 @@
         by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
     note le_1 = this
 
-    let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
+    let ?q = "\<lambda>y. \<mu>G ((\<lambda>x. merge J (I - J) (y,x)) -` Z \<inter> space (Pi\<^isub>M I M))"
     have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
       unfolding `Z = emb I K X` using J K merge_in_G(3)
       by (simp add: merge_in_G  \<mu>G_eq emeasure_fold_measurable cong: measurable_cong)
@@ -416,7 +412,7 @@
         using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
         by (auto intro!: INF_lower2[of 0] J.measure_le_1)
 
-      let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
+      let ?M = "\<lambda>K Z y. (\<lambda>x. merge K (I - K) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)"
 
       { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
         then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
@@ -524,9 +520,9 @@
             from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
             obtain w' where w': "w' \<in> space (Pi\<^isub>M ?D M)"
               "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
-            let ?w = "merge (J k) (w k) ?D w'"
-            have [simp]: "\<And>x. merge (J k) (w k) (I - J k) (merge ?D w' (I - ?D) x) =
-              merge (J (Suc k)) ?w (I - (J (Suc k))) x"
+            let ?w = "merge (J k) ?D (w k, w')"
+            have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
+              merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
               using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
               by (auto intro!: ext split: split_merge)
             have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
@@ -552,7 +548,7 @@
           using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
           by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
         then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
-        then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
+        then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
         then have "\<exists>x\<in>A k. restrict x (J k) = w k"
           using `w k \<in> space (Pi\<^isub>M (J k) M)`
           by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)