# HG changeset patch
# User nipkow
# Date 1352485307 -3600
# Node ID 20bacff859842e3ae480ae1bca9425958861f5f6
# Parent  6fe18351e9ddfe83f19cf19653cc605363655f52# Parent  e8af1889606092521e1bdb7136699fe718b43b9a
merged

diff -r e8af18896060 -r 20bacff85984 NEWS
--- a/NEWS	Fri Nov 09 19:16:31 2012 +0100
+++ b/NEWS	Fri Nov 09 19:21:47 2012 +0100
@@ -207,6 +207,9 @@
 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
 expressions.
 
+* Preprocessing of the code generator rewrites set comprehensions into
+pointfree expressions.
+
 * Quickcheck:
 
   - added an optimisation for equality premises.
diff -r e8af18896060 -r 20bacff85984 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -244,7 +244,7 @@
  apply (elim dividesE, intro dividesI, assumption)
  apply (rule l_cancel[of c])
     apply (simp add: m_assoc carr)+
-apply (fast intro: divides_mult_lI carr)
+apply (fast intro: carr)
 done
 
 lemma (in comm_monoid) divides_mult_rI [intro]:
diff -r e8af18896060 -r 20bacff85984 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Library/Permutation.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -193,7 +193,7 @@
   show ?case
   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
-      by (auto simp: bij_betw_def bij_betw_swap_iff)
+      by (auto simp: bij_betw_def)
     fix i assume "i < length(y#x#l)"
     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
diff -r e8af18896060 -r 20bacff85984 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -24,7 +24,7 @@
 
 lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
   apply (auto simp add: prime_def)
-  apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
+  apply (metis gcd_dvd1 gcd_dvd2)
   done
 
 text {*
diff -r e8af18896060 -r 20bacff85984 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -43,6 +43,15 @@
   "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
   unfolding extensional_def by auto
 
+lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
+  by (auto simp: extensional_def)
+
+lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
+  unfolding restrict_def extensional_def by auto
+
+lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
+  unfolding restrict_def by (simp add: fun_eq_iff)
+
 definition
   "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
 
@@ -85,6 +94,33 @@
   "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
   by (auto simp: restrict_def)
 
+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 J (x, y) \<in> extensional K"
+  unfolding merge_def extensional_def by auto
+
+lemma injective_vimage_restrict:
+  assumes J: "J \<subseteq> I"
+  and sets: "A \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" and ne: "(\<Pi>\<^isub>E i\<in>I. S i) \<noteq> {}"
+  and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
+  shows "A = B"
+proof  (intro set_eqI)
+  fix x
+  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
+  have "J \<inter> (I - J) = {}" by auto
+  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 (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)
+  next
+    assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
+  qed
+qed
+
 lemma extensional_insert_undefined[intro, simp]:
   assumes "a \<in> extensional (insert i I)"
   shows "a(i := undefined) \<in> extensional I"
@@ -253,6 +289,24 @@
 lemma prod_emb_PiE_same_index[simp]: "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^isub>E I E) = Pi\<^isub>E I E"
   by (auto simp: prod_emb_def Pi_iff)
 
+lemma prod_emb_trans[simp]:
+  "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
+  by (auto simp add: Int_absorb1 prod_emb_def)
+
+lemma prod_emb_Pi:
+  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
+  shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
+  using assms space_closed
+  by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
+
+lemma prod_emb_id:
+  "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
+  by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
+
+lemma prod_emb_mono:
+  "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
+  by (auto simp: prod_emb_def)
+
 definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   "PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
@@ -309,6 +363,17 @@
     \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
   by (auto simp: prod_algebra_def Pi_iff)
 
+lemma prod_algebraI_finite:
+  "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
+  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
+
+lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
+proof (safe intro!: Int_stableI)
+  fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
+  then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
+    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
+qed
+
 lemma prod_algebraE:
   assumes A: "A \<in> prod_algebra I M"
   obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
@@ -546,6 +611,14 @@
     using A X by (auto intro!: measurable_sets)
 qed (insert X, auto dest: measurable_space)
 
+lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
+  by (intro measurable_restrict measurable_component_singleton) auto
+
+lemma measurable_prod_emb[intro, simp]:
+  "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
+  unfolding prod_emb_def space_PiM[symmetric]
+  by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
+
 lemma sets_in_Pi_aux:
   "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
diff -r e8af18896060 -r 20bacff85984 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -5,78 +5,9 @@
 header {*Infinite Product Measure*}
 
 theory Infinite_Product_Measure
-  imports Probability_Measure Caratheodory
+  imports Probability_Measure Caratheodory Projective_Family
 begin
 
-lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
-  by (auto simp: extensional_def)
-
-lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
-  unfolding restrict_def extensional_def by auto
-
-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 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 J (x, y) \<in> extensional K"
-  unfolding merge_def extensional_def by auto
-
-lemma injective_vimage_restrict:
-  assumes J: "J \<subseteq> I"
-  and sets: "A \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^isub>E i\<in>J. S i)" and ne: "(\<Pi>\<^isub>E i\<in>I. S i) \<noteq> {}"
-  and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
-  shows "A = B"
-proof  (intro set_eqI)
-  fix x
-  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
-  have "J \<inter> (I - J) = {}" by auto
-  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 (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)
-  next
-    assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
-  qed
-qed
-
-lemma prod_algebraI_finite:
-  "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
-  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
-
-lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
-proof (safe intro!: Int_stableI)
-  fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
-  then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
-    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
-qed
-
-lemma prod_emb_trans[simp]:
-  "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
-  by (auto simp add: Int_absorb1 prod_emb_def)
-
-lemma prod_emb_Pi:
-  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
-  shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
-  using assms space_closed
-  by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
-
-lemma prod_emb_id:
-  "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
-  by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
-
-lemma measurable_prod_emb[intro, simp]:
-  "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
-  unfolding prod_emb_def space_PiM[symmetric]
-  by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
-
-lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
-  by (intro measurable_restrict measurable_component_singleton) auto
-
 lemma (in product_prob_space) distr_restrict:
   assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
   shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
@@ -118,200 +49,27 @@
     by (auto intro!: measurable_restrict_subset simp: space_PiM)
 qed
 
-abbreviation (in product_prob_space)
-  "emb L K X \<equiv> prod_emb L M K X"
-
 lemma (in product_prob_space) emeasure_prod_emb[simp]:
   assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
-  shows "emeasure (Pi\<^isub>M L M) (emb L J X) = emeasure (Pi\<^isub>M J M) X"
+  shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X"
   by (subst distr_restrict[OF L])
      (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
 
-lemma (in product_prob_space) prod_emb_injective:
-  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
-  assumes "prod_emb L M J X = prod_emb L M J Y"
-  shows "X = Y"
-proof (rule injective_vimage_restrict)
-  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
-  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))"
-    using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
-qed fact
-
-definition (in product_prob_space) generator :: "('i \<Rightarrow> 'a) set set" where
-  "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
-
-lemma (in product_prob_space) generatorI':
-  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator"
-  unfolding generator_def by auto
-
-lemma (in product_prob_space) algebra_generator:
-  assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
-  unfolding algebra_def algebra_axioms_def ring_of_sets_iff
-proof (intro conjI ballI)
-  let ?G = generator
-  show "?G \<subseteq> Pow ?\<Omega>"
-    by (auto simp: generator_def prod_emb_def)
-  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
-  then show "{} \<in> ?G"
-    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
-             simp: sigma_sets.Empty generator_def prod_emb_def)
-  from `i \<in> I` show "?\<Omega> \<in> ?G"
-    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
-             simp: generator_def prod_emb_def)
-  fix A assume "A \<in> ?G"
-  then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
-    by (auto simp: generator_def)
-  fix B assume "B \<in> ?G"
-  then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
-    by (auto simp: generator_def)
-  let ?RA = "emb (JA \<union> JB) JA XA"
-  let ?RB = "emb (JA \<union> JB) JB XB"
-  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
-    using XA A XB B by auto
-  show "A - B \<in> ?G" "A \<union> B \<in> ?G"
-    unfolding * using XA XB by (safe intro!: generatorI') auto
-qed
-
-lemma (in product_prob_space) sets_PiM_generator:
-  "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
-proof cases
-  assume "I = {}" then show ?thesis
-    unfolding generator_def
-    by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
-next
-  assume "I \<noteq> {}"
-  show ?thesis
-  proof
-    show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
-      unfolding sets_PiM
-    proof (safe intro!: sigma_sets_subseteq)
-      fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
-        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
-    qed
-  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
-qed
-
-
-lemma (in product_prob_space) generatorI:
-  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
-  unfolding generator_def by auto
-
-definition (in product_prob_space)
-  "\<mu>G A =
-    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (Pi\<^isub>M J M) X))"
-
-lemma (in product_prob_space) \<mu>G_spec:
-  assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
-  shows "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
-  unfolding \<mu>G_def
-proof (intro the_equality allI impI ballI)
-  fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
-  have "emeasure (Pi\<^isub>M K M) Y = emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) K Y)"
-    using K J by simp
-  also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
-    using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
-  also have "emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) J X) = emeasure (Pi\<^isub>M J M) X"
-    using K J by simp
-  finally show "emeasure (Pi\<^isub>M J M) X = emeasure (Pi\<^isub>M K M) Y" ..
-qed (insert J, force)
+sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
+proof
+  fix J::"'i set" assume "finite J"
+  interpret f: finite_product_prob_space M J proof qed fact
+  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
+  show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
+            (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
+            (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
+    by (auto simp add: sigma_finite_measure_def)
+  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
+qed simp_all
 
-lemma (in product_prob_space) \<mu>G_eq:
-  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (Pi\<^isub>M J M) X"
-  by (intro \<mu>G_spec) auto
-
-lemma (in product_prob_space) generator_Ex:
-  assumes *: "A \<in> generator"
-  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (Pi\<^isub>M J M) X"
-proof -
-  from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
-    unfolding generator_def by auto
-  with \<mu>G_spec[OF this] show ?thesis by auto
-qed
-
-lemma (in product_prob_space) generatorE:
-  assumes A: "A \<in> generator"
-  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
-proof -
-  from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
-    "\<mu>G A = emeasure (Pi\<^isub>M J M) X" by auto
-  then show thesis by (intro that) auto
-qed
-
-lemma (in product_prob_space) merge_sets:
-  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
-  by simp
-
-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 "((\<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 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 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
-  have [simp]: "(K - J) \<inter> K = K - J" by auto
-  from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
-    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
-       auto
-qed
-
-lemma (in product_prob_space) positive_\<mu>G: 
-  assumes "I \<noteq> {}"
-  shows "positive generator \<mu>G"
-proof -
-  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
-  show ?thesis
-  proof (intro positive_def[THEN iffD2] conjI ballI)
-    from generatorE[OF G.empty_sets] guess J X . note this[simp]
-    interpret J: finite_product_sigma_finite M J by default fact
-    have "X = {}"
-      by (rule prod_emb_injective[of J I]) simp_all
-    then show "\<mu>G {} = 0" by simp
-  next
-    fix A assume "A \<in> generator"
-    from generatorE[OF this] guess J X . note this[simp]
-    interpret J: finite_product_sigma_finite M J by default fact
-    show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
-  qed
-qed
-
-lemma (in product_prob_space) additive_\<mu>G: 
-  assumes "I \<noteq> {}"
-  shows "additive generator \<mu>G"
-proof -
-  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
-  show ?thesis
-  proof (intro additive_def[THEN iffD2] ballI impI)
-    fix A assume "A \<in> generator" with generatorE guess J X . note J = this
-    fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
-    assume "A \<inter> B = {}"
-    have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
-      using J K by auto
-    interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
-    have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
-      apply (rule prod_emb_injective[of "J \<union> K" I])
-      apply (insert `A \<inter> B = {}` JK J K)
-      apply (simp_all add: Int prod_emb_Int)
-      done
-    have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
-      using J K by simp_all
-    then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
-      by simp
-    also have "\<dots> = emeasure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
-      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
-    also have "\<dots> = \<mu>G A + \<mu>G B"
-      using J K JK_disj by (simp add: plus_emeasure[symmetric])
-    finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
-  qed
-qed
+lemma (in product_prob_space) PiP_PiM_finite[simp]:
+  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M"
+  using assms by (simp add: PiP_finite)
 
 lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
   assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
@@ -337,7 +95,6 @@
     ultimately have K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "X \<in> sets (Pi\<^isub>M K M)" "Z = emb I K X"
       "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. (\<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]
@@ -402,7 +159,7 @@
         using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
       ultimately have "0 < ?a" by auto
 
-      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (Pi\<^isub>M J M) X"
+      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (PiP J M (\<lambda>J. (Pi\<^isub>M J M))) X"
         using A by (intro allI generator_Ex) auto
       then obtain J' X' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I" "\<And>n. X' n \<in> sets (Pi\<^isub>M (J' n) M)"
         and A': "\<And>n. A n = emb I (J' n) (X' n)"
diff -r e8af18896060 -r 20bacff85984 src/HOL/Probability/Projective_Family.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 09 19:21:47 2012 +0100
@@ -0,0 +1,300 @@
+(*  Title:      HOL/Probability/Projective_Family.thy
+    Author:     Fabian Immler, TU München
+    Author:     Johannes Hölzl, TU München
+*)
+
+header {*Projective Family*}
+
+theory Projective_Family
+imports Finite_Product_Measure Probability_Measure
+begin
+
+definition
+  PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
+  "PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
+    {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
+    (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j))
+    (\<lambda>(J, X). emeasure (P J) (Pi\<^isub>E J X))"
+
+lemma space_PiP[simp]: "space (PiP I M P) = space (PiM I M)"
+  by (auto simp add: PiP_def space_PiM prod_emb_def intro!: space_extend_measure)
+
+lemma sets_PiP[simp]: "sets (PiP I M P) = sets (PiM I M)"
+  by (auto simp add: PiP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
+
+lemma measurable_PiP1[simp]: "measurable (PiP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'"
+  unfolding measurable_def by auto
+
+lemma measurable_PiP2[simp]: "measurable M' (PiP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)"
+  unfolding measurable_def by auto
+
+locale projective_family =
+  fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
+  assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
+     (P H) (prod_emb H M J X) = (P J) X"
+  assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
+  assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
+  assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
+begin
+
+lemma emeasure_PiP:
+  assumes "finite J"
+  assumes "J \<subseteq> I"
+  assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)"
+  shows "emeasure (PiP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
+proof -
+  have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
+  proof safe
+    fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
+    hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
+    also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
+    finally show "x j \<in> space (M j)" .
+  qed
+  hence "emeasure (PiP J M P) (Pi\<^isub>E J A) =
+    emeasure (PiP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
+    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
+  also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
+  proof (rule emeasure_extend_measure_Pair[OF PiP_def])
+    show "positive (sets (PiP J M P)) (P J)" unfolding positive_def by auto
+    show "countably_additive (sets (PiP J M P)) (P J)" unfolding countably_additive_def
+      by (auto simp: suminf_emeasure proj_sets[OF `finite J`])
+    show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))"
+      using assms by auto
+    fix K and X::"'i \<Rightarrow> 'a set"
+    show "prod_emb J M K (Pi\<^isub>E K X) \<in> Pow (\<Pi>\<^isub>E i\<in>J. space (M i))"
+      by (auto simp: prod_emb_def)
+    assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))"
+    thus "emeasure (P J) (prod_emb J M K (Pi\<^isub>E K X)) = emeasure (P K) (Pi\<^isub>E K X)"
+      using assms
+      apply (cases "J = {}")
+      apply (simp add: prod_emb_id)
+      apply (fastforce simp add: intro!: projective sets_PiM_I_finite)
+      done
+  qed
+  finally show ?thesis .
+qed
+
+lemma PiP_finite:
+  assumes "finite J"
+  assumes "J \<subseteq> I"
+  shows "PiP J M P = P J" (is "?P = _")
+proof (rule measure_eqI_generator_eq)
+  let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
+  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
+  let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
+  show "Int_stable ?J"
+    by (rule Int_stable_PiE)
+  interpret prob_space "P J" using prob_space `finite J` by simp
+  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
+  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+  show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
+    using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
+  fix X assume "X \<in> ?J"
+  then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
+  with `finite J` have "X \<in> sets (PiP J M P)" by simp
+  have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
+    using E sets_into_space
+    by (auto intro!: prod_emb_PiE_same_index)
+  show "emeasure (PiP J M P) X = emeasure (P J) X"
+    unfolding X using E
+    by (intro emeasure_PiP assms) simp
+qed (insert `finite J`, auto intro!: prod_algebraI_finite)
+
+lemma emeasure_fun_emb[simp]:
+  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
+  shows "emeasure (PiP L M P) (prod_emb L M J X) = emeasure (PiP J M P) X"
+  using assms
+  by (subst PiP_finite) (auto simp: PiP_finite finite_subset projective)
+
+lemma prod_emb_injective:
+  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
+  assumes "prod_emb L M J X = prod_emb L M J Y"
+  shows "X = Y"
+proof (rule injective_vimage_restrict)
+  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)"
+  proof
+    fix i assume "i \<in> L"
+    interpret prob_space "P {i}" using prob_space by simp
+    from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
+  qed
+  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))"
+    using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
+qed fact
+
+abbreviation
+  "emb L K X \<equiv> prod_emb L M K X"
+
+definition generator :: "('i \<Rightarrow> 'a) set set" where
+  "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
+
+lemma generatorI':
+  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator"
+  unfolding generator_def by auto
+
+lemma algebra_generator:
+  assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
+  unfolding algebra_def algebra_axioms_def ring_of_sets_iff
+proof (intro conjI ballI)
+  let ?G = generator
+  show "?G \<subseteq> Pow ?\<Omega>"
+    by (auto simp: generator_def prod_emb_def)
+  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
+  then show "{} \<in> ?G"
+    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
+             simp: sigma_sets.Empty generator_def prod_emb_def)
+  from `i \<in> I` show "?\<Omega> \<in> ?G"
+    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
+             simp: generator_def prod_emb_def)
+  fix A assume "A \<in> ?G"
+  then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
+    by (auto simp: generator_def)
+  fix B assume "B \<in> ?G"
+  then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
+    by (auto simp: generator_def)
+  let ?RA = "emb (JA \<union> JB) JA XA"
+  let ?RB = "emb (JA \<union> JB) JB XB"
+  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
+    using XA A XB B by auto
+  show "A - B \<in> ?G" "A \<union> B \<in> ?G"
+    unfolding * using XA XB by (safe intro!: generatorI') auto
+qed
+
+lemma sets_PiM_generator:
+  "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+proof cases
+  assume "I = {}" then show ?thesis
+    unfolding generator_def
+    by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof
+    show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+      unfolding sets_PiM
+    proof (safe intro!: sigma_sets_subseteq)
+      fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
+        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
+    qed
+  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+qed
+
+lemma generatorI:
+  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
+  unfolding generator_def by auto
+
+definition
+  "\<mu>G A =
+    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (PiP J M P) X))"
+
+lemma \<mu>G_spec:
+  assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
+  shows "\<mu>G A = emeasure (PiP J M P) X"
+  unfolding \<mu>G_def
+proof (intro the_equality allI impI ballI)
+  fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
+  have "emeasure (PiP K M P) Y = emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) K Y)"
+    using K J by simp
+  also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
+    using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
+  also have "emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (PiP J M P) X"
+    using K J by simp
+  finally show "emeasure (PiP J M P) X = emeasure (PiP K M P) Y" ..
+qed (insert J, force)
+
+lemma \<mu>G_eq:
+  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (PiP J M P) X"
+  by (intro \<mu>G_spec) auto
+
+lemma generator_Ex:
+  assumes *: "A \<in> generator"
+  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (PiP J M P) X"
+proof -
+  from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
+    unfolding generator_def by auto
+  with \<mu>G_spec[OF this] show ?thesis by auto
+qed
+
+lemma generatorE:
+  assumes A: "A \<in> generator"
+  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (PiP J M P) X"
+proof -
+  from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
+    "\<mu>G A = emeasure (PiP J M P) X" by auto
+  then show thesis by (intro that) auto
+qed
+
+lemma merge_sets:
+  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
+  by simp
+
+lemma merge_emb:
+  assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M 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 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 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
+  have [simp]: "(K - J) \<inter> K = K - J" by auto
+  from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
+    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
+       auto
+qed
+
+lemma positive_\<mu>G:
+  assumes "I \<noteq> {}"
+  shows "positive generator \<mu>G"
+proof -
+  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
+  show ?thesis
+  proof (intro positive_def[THEN iffD2] conjI ballI)
+    from generatorE[OF G.empty_sets] guess J X . note this[simp]
+    have "X = {}"
+      by (rule prod_emb_injective[of J I]) simp_all
+    then show "\<mu>G {} = 0" by simp
+  next
+    fix A assume "A \<in> generator"
+    from generatorE[OF this] guess J X . note this[simp]
+    show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
+  qed
+qed
+
+lemma additive_\<mu>G:
+  assumes "I \<noteq> {}"
+  shows "additive generator \<mu>G"
+proof -
+  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
+  show ?thesis
+  proof (intro additive_def[THEN iffD2] ballI impI)
+    fix A assume "A \<in> generator" with generatorE guess J X . note J = this
+    fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
+    assume "A \<inter> B = {}"
+    have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
+      using J K by auto
+    have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
+      apply (rule prod_emb_injective[of "J \<union> K" I])
+      apply (insert `A \<inter> B = {}` JK J K)
+      apply (simp_all add: Int prod_emb_Int)
+      done
+    have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
+      using J K by simp_all
+    then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
+      by simp
+    also have "\<dots> = emeasure (PiP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
+      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
+    also have "\<dots> = \<mu>G A + \<mu>G B"
+      using J K JK_disj by (simp add: plus_emeasure[symmetric])
+    finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+  qed
+qed
+
+end
+
+end
diff -r e8af18896060 -r 20bacff85984 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Nov 09 19:21:47 2012 +0100
@@ -15,7 +15,6 @@
 structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
 struct
 
-
 (* syntactic operations *)
 
 fun mk_inf (t1, t2) =
@@ -110,10 +109,6 @@
 fun dest_bound (Bound i) = i
   | dest_bound t = raise TERM("dest_bound", [t]);
 
-fun mk_pattern t = case try ((map dest_bound) o HOLogic.strip_tuple) t of
-    SOME p => Pattern p 
-  | NONE => raise TERM ("mk_pattern: only tuples of bound variables supported", [t]);
-
 fun type_of_pattern Ts (Pattern bs) = HOLogic.mk_tupleT (map (nth Ts) bs)
 
 fun term_of_pattern Ts (Pattern bs) =
@@ -141,40 +136,40 @@
       val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
     in (domain_type (fastype_of t''), t'') end
 
-fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) =
+fun mk_term vs t =
+  let
+    val bs = loose_bnos t
+    val vs' = map (nth (rev vs)) bs
+    val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
+      |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
+      |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))
+    val t' = subst_bounds (subst, t)
+    val tuple = Pattern bs
+  in (tuple, (vs', t')) end
+
+fun default_atom vs t =
+  let
+    val (tuple, (vs', t')) = mk_term vs t
+    val T = HOLogic.mk_tupleT (map snd vs')
+    val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t'))
+  in
+    (tuple, Atom (tuple, s))
+  end
+
+fun mk_atom vs (t as Const (@{const_name "Set.member"}, _) $ x $ s) =
     if not (null (loose_bnos s)) then
-      raise TERM ("mk_atom: bound variables in the set expression", [s])
+      default_atom vs t
     else
-      (case try mk_pattern x of
-      SOME pat => (pat, Atom (pat, s))
+      (case try ((map dest_bound) o HOLogic.strip_tuple) x of
+      SOME pat => (Pattern pat, Atom (Pattern pat, s))
     | NONE =>
         let
-          val bs = loose_bnos x
-          val vs' = map (nth (rev vs)) bs
-          val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
-            |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
-            |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))  
-          val x' = subst_bounds (subst, x)
-          val tuple = Pattern bs
+          val (tuple, (vs', x')) = mk_term vs x 
           val rT = HOLogic.dest_setT (fastype_of s)
-          val (_, f) = mk_split rT vs' x'
-        in (tuple, Atom (tuple, mk_vimage f s)) end)
-  | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) =
-      apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
-  | mk_atom vs t =
-    let
-      val bs = loose_bnos t
-      val vs' = map (nth (rev vs)) bs
-      val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs)
-        |> sort (fn (p1, p2) => int_ord (fst p1, fst p2))
-        |> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst')))))
-      val t' = subst_bounds (subst, t)
-      val tuple = Pattern bs
-      val setT = HOLogic.mk_tupleT (map snd vs')
-      val (_, s) = mk_split @{typ bool} vs' t'
-    in
-      (tuple, Atom (tuple, HOLogic.Collect_const setT $ s))
-    end
+          val s = mk_vimage (snd (mk_split rT vs' x')) s
+        in (tuple, Atom (tuple, s)) end)
+  | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
+  | mk_atom vs t = default_atom vs t
 
 fun merge' [] (pats1, pats2) = ([], (pats1, pats2))
   | merge' pat (pats, []) = (pat, (pats, []))
@@ -294,7 +289,7 @@
       (0 upto (length vs - 1))
     val (pats, fm) =
       mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
-    fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
+    fun mk_set (Atom pt) = foldr1 mk_sigma (map (lookup pt) pats)
       | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
       | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
     val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
@@ -331,10 +326,10 @@
 val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
 val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
 
-val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
+fun elim_Collect_tac ss = dtac @{thm iffD1[OF mem_Collect_eq]}
   THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
   THEN' REPEAT_DETERM o etac @{thm conjE}
-  THEN' TRY o hyp_subst_tac;
+  THEN' TRY o hyp_subst_tac' ss;
 
 fun intro_image_tac ctxt = rtac @{thm image_eqI}
     THEN' (REPEAT_DETERM1 o
@@ -348,7 +343,7 @@
   THEN' REPEAT_DETERM o CHANGED o
     (TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}))
     THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-    THEN' TRY o hyp_subst_tac)
+    THEN' TRY o hyp_subst_tac' ss)
 
 fun tac1_of_formula ss (Int (fm1, fm2)) =
     TRY o etac @{thm conjE}
@@ -392,21 +387,21 @@
        ORELSE' etac @{thm conjE}
        ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
          TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps [@{thm prod.cases}])) THEN'
-         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})
+         REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl})
        ORELSE' (etac @{thm imageE}
          THEN' (REPEAT_DETERM o CHANGED o
          (TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}))
          THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-         THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})))
+         THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl})))
        ORELSE' etac @{thm ComplE}
        ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
         THEN' TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps [@{thm prod.cases}]))
-        THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl}))
+        THEN' TRY o hyp_subst_tac' ss THEN' TRY o rtac @{thm refl}))
 
 fun tac ss ctxt fm =
   let
     val subset_tac1 = rtac @{thm subsetI}
-      THEN' elim_Collect_tac
+      THEN' elim_Collect_tac ss
       THEN' intro_image_tac ctxt
       THEN' tac1_of_formula ss fm
     val subset_tac2 = rtac @{thm subsetI}
@@ -414,7 +409,7 @@
       THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
       THEN' REPEAT_DETERM o resolve_tac @{thms exI}
       THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
-      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
+      THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac' ss) THEN' rtac @{thm refl}))))
       THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
         REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ss f (i + j)) (strip_Int fm))))
   in
@@ -528,11 +523,14 @@
 
 fun code_simproc ss redex =
   let
-    val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
+    fun unfold_conv thms =
+      Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+        (Raw_Simplifier.inherit_context ss empty_ss addsimps thms)
+    val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
   in
     case base_simproc ss (Thm.rhs_of prep_thm) of
       SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
-        Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
+        unfold_conv @{thms eq_equal} (Thm.rhs_of rewr_thm)])
     | NONE => NONE
   end;
 
diff -r e8af18896060 -r 20bacff85984 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Nov 09 19:16:31 2012 +0100
+++ b/src/Provers/hypsubst.ML	Fri Nov 09 19:21:47 2012 +0100
@@ -48,6 +48,7 @@
 sig
   val bound_hyp_subst_tac    : int -> tactic
   val hyp_subst_tac          : int -> tactic
+  val hyp_subst_tac'         : simpset -> int -> tactic
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
@@ -126,12 +127,14 @@
 
   (*Select a suitable equality assumption; substitute throughout the subgoal
     If bnd is true, then it replaces Bound variables only. *)
-  fun gen_hyp_subst_tac bnd =
+  fun gen_hyp_subst_tac opt_ss bnd =
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
         val (k, _) = eq_var bnd true Bi
-        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          |> Simplifier.set_mksimps (K (mk_eqs bnd))
+        val map_simpset = case opt_ss of
+          NONE => Simplifier.global_context (Thm.theory_of_thm st)
+        | SOME ss => Simplifier.inherit_context ss
+        val hyp_subst_ss = map_simpset empty_ss |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
@@ -195,11 +198,14 @@
 
 (*Substitutes for Free or Bound variables*)
 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
+        gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
+
+fun hyp_subst_tac' ss = FIRST' [ematch_tac [Data.thin_refl],
+        gen_hyp_subst_tac (SOME ss) false, vars_gen_hyp_subst_tac false];
 
 (*Substitutes for Bound variables only -- this is always safe*)
 val bound_hyp_subst_tac =
-    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
+    gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
 
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are