# HG changeset patch
# User hoelzl
# Date 1353324542 -3600
# Node ID 69b35a75caf3f0b6fc65c198237251a6d26669fc
# Parent  7ae7efef5ad8c373022212c0808d2520d54ac092
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -86,7 +86,7 @@
 lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
   by auto
 
-lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
+lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})"
 apply (simp add: Pi_def, auto)
 txt{*Converse direction requires Axiom of Choice to exhibit a function
 picking an element from each non-empty @{term "B x"}*}
@@ -97,12 +97,31 @@
 lemma Pi_empty [simp]: "Pi {} B = UNIV"
 by (simp add: Pi_def)
 
+lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
+  by auto
+
+lemma Pi_UN:
+  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
+  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
+  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
+proof (intro set_eqI iffI)
+  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
+  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
+  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
+  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
+  have "f \<in> Pi I (A k)"
+  proof (intro Pi_I)
+    fix i assume "i \<in> I"
+    from mono[OF this, of "n i" k] k[OF this] n[OF this]
+    show "f i \<in> A k i" by auto
+  qed
+  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
+qed auto
+
 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
 by (simp add: Pi_def)
-(*
-lemma funcset_id [simp]: "(%x. x): A -> A"
-  by (simp add: Pi_def)
-*)
+
 text{*Covariance of Pi-sets in their second argument*}
 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
 by auto
@@ -124,6 +143,25 @@
   finally show "f z \<in> B z \<times> C z" .
 qed
 
+lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
+  by (auto simp: Pi_def)
+
+lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
+  by (auto simp: Pi_def)
+
+lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
+  by (auto simp: Pi_def)
+
+lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
+  by (auto simp: Pi_def)
+
+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"
+  apply auto
+  apply (drule_tac x=x in Pi_mem)
+  apply (simp_all split: split_if_asm)
+  apply (drule_tac x=i in Pi_mem)
+  apply (auto dest!: Pi_mem)
+  done
 
 subsection{*Composition With a Restricted Domain: @{term compose}*}
 
@@ -173,6 +211,19 @@
 lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
   by (auto simp add: restrict_def)
 
+lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
+  unfolding restrict_def by (simp add: fun_eq_iff)
+
+lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
+  by (auto simp: restrict_def)
+
+lemma restrict_upd[simp]:
+  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
+  by (auto simp: fun_eq_iff)
+
+lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
+  by (auto simp: restrict_def Pi_def)
+
 
 subsection{*Bijections Between Sets*}
 
@@ -213,6 +264,9 @@
 
 subsection{*Extensionality*}
 
+lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
+  unfolding extensional_def by auto
+
 lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
 by (simp add: extensional_def)
 
@@ -230,6 +284,9 @@
 lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
 by(rule extensionalityI[OF restrict_extensional]) auto
 
+lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
+  unfolding extensional_def by auto
+
 lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
 by (unfold inv_into_def) (fast intro: someI2)
 
@@ -246,6 +303,29 @@
 apply (simp add: f_inv_into_f)
 done
 
+lemma extensional_insert[intro, simp]:
+  assumes "a \<in> extensional (insert i I)"
+  shows "a(i := b) \<in> extensional (insert i I)"
+  using assms unfolding extensional_def by auto
+
+lemma extensional_Int[simp]:
+  "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 extensional_insert_undefined[intro, simp]:
+  "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
+  unfolding extensional_def by auto
+
+lemma extensional_insert_cancel[intro, simp]:
+  "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
+  unfolding extensional_def by auto
+
 
 subsection{*Cardinality*}
 
@@ -259,156 +339,207 @@
 
 subsection {* Extensional Function Spaces *} 
 
-definition extensional_funcset
-where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
+definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+  "PiE S T = Pi S T \<inter> extensional S"
+
+abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
 
-lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
-unfolding extensional_def by auto
+syntax "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
+
+syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
+
+syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
+
+translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
 
-lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
-unfolding extensional_funcset_def by simp
+abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^isub>E" 60) where
+  "A ->\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)"
+
+notation (xsymbols)
+  extensional_funcset  (infixr "\<rightarrow>\<^isub>E" 60)
 
-lemma extensional_funcset_empty_range:
-  assumes "S \<noteq> {}"
-  shows "extensional_funcset S {} = {}"
-using assms unfolding extensional_funcset_def by auto
+lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
+  by (simp add: PiE_def)
+
+lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
+  unfolding PiE_def by simp
+
+lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
+  unfolding PiE_def by auto
 
-lemma extensional_funcset_arb:
-  assumes "f \<in> extensional_funcset S T" "x \<notin> S"
-  shows "f x = undefined"
-using assms
-unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
-
-lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
-unfolding extensional_funcset_def by auto
-
-lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
-unfolding extensional_def by auto
+lemma PiE_eq_empty_iff:
+  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
+proof
+  assume "Pi\<^isub>E I F = {}"
+  show "\<exists>i\<in>I. F i = {}"
+  proof (rule ccontr)
+    assume "\<not> ?thesis"
+    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
+    from choice[OF this] guess f ..
+    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
+    with `Pi\<^isub>E I F = {}` show False by auto
+  qed
+qed (auto simp: PiE_def)
 
-lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T"
-unfolding extensional_funcset_def extensional_def by auto
+lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
+  unfolding PiE_def by auto (auto dest!: extensional_arb)
+
+lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
+  unfolding PiE_def by auto
 
-lemma extensional_funcset_restrict_domain:
-  "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
-unfolding extensional_funcset_def extensional_def by auto
+lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
+  unfolding PiE_def extensional_def by auto
 
-lemma extensional_funcset_extend_domain_eq:
+lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
+  unfolding PiE_def extensional_def by auto
+
+lemma PiE_insert_eq:
   assumes "x \<notin> S"
-  shows
-    "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
-  using assms
+  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
 proof -
   {
-    fix f
-    assume "f : extensional_funcset (insert x S) T"
-    from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
-      unfolding image_iff
-      apply (rule_tac x="(f x, f(x := undefined))" in bexI)
-    apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done 
+    fix f assume "f \<in> PiE (insert x S) T"
+    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   }
-  moreover
-  {
-    fix f
-    assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
-    from this assms have "f : extensional_funcset (insert x S) T"
-      by (auto intro: extensional_funcset_extend_domainI)
-  }
-  ultimately show ?thesis by auto
+  then show ?thesis using assms by (auto intro: PiE_fun_upd)
 qed
 
-lemma extensional_funcset_fun_upd_restricts_rangeI:  "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T - {f x})"
-unfolding extensional_funcset_def extensional_def
-apply auto
-apply (case_tac "x = xa")
-apply auto done
+lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
+  by (auto simp: PiE_def)
+
+lemma PiE_cong:
+  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B"
+  unfolding PiE_def by (auto simp: Pi_cong)
+
+lemma PiE_E [elim]:
+  "f \<in> PiE A B \<Longrightarrow> (x \<in> A \<Longrightarrow> f x \<in> B x \<Longrightarrow> Q) \<Longrightarrow> (x \<notin> A \<Longrightarrow> f x = undefined \<Longrightarrow> Q) \<Longrightarrow> Q"
+by(auto simp: Pi_def PiE_def extensional_def)
+
+lemma PiE_I[intro!]: "(\<And>x. x \<in> A ==> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
+  by (simp add: PiE_def extensional_def)
+
+lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
+  by auto
+
+lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
+  by (simp add: PiE_def Pi_iff)
+
+lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
+  by (simp add: extensional_restrict PiE_def)
+
+lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
+  by (auto simp: PiE_iff)
+
+lemma PiE_eq_subset:
+  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
+  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
+  shows "F i \<subseteq> F' i"
+proof
+  fix x assume "x \<in> F i"
+  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
+  from choice[OF this] guess f .. note f = this
+  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
+  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
+  then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
+qed
+
+lemma PiE_eq_iff_not_empty:
+  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
+  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
+proof (intro iffI ballI)
+  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
+  show "F i = F' i"
+    using PiE_eq_subset[of I F F', OF ne eq i]
+    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
+    by auto
+qed (auto simp: PiE_def)
+
+lemma PiE_eq_iff:
+  "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
+proof (intro iffI disjCI)
+  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
+  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
+  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
+    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
+  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
+next
+  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
+  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
+    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
+qed
+
+lemma extensional_funcset_fun_upd_restricts_rangeI: 
+  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^isub>E T ==> f(x := undefined) : S \<rightarrow>\<^isub>E (T - {f x})"
+  unfolding extensional_funcset_def extensional_def
+  apply auto
+  apply (case_tac "x = xa")
+  apply auto
+  done
 
 lemma extensional_funcset_fun_upd_extends_rangeI:
-  assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
-  shows "f(x := a) : extensional_funcset (insert x S) T"
+  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T - {a})"
+  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E  T"
   using assms unfolding extensional_funcset_def extensional_def by auto
 
 subsubsection {* Injective Extensional Function Spaces *}
 
 lemma extensional_funcset_fun_upd_inj_onI:
-  assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
+  assumes "f \<in> S \<rightarrow>\<^isub>E (T - {a})" "inj_on f S"
   shows "inj_on (f(x := a)) S"
   using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
 
 lemma extensional_funcset_extend_domain_inj_on_eq:
   assumes "x \<notin> S"
-  shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
-    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+  shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} =
+    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
 proof -
   from assms show ?thesis
-    apply auto
-    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
+    apply (auto del: PiE_I PiE_E)
+    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
     apply (auto simp add: image_iff inj_on_def)
     apply (rule_tac x="xa x" in exI)
-    apply (auto intro: extensional_funcset_mem)
+    apply (auto intro: PiE_mem del: PiE_I PiE_E)
     apply (rule_tac x="xa(x := undefined)" in exI)
     apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
-    apply (auto dest!: extensional_funcset_mem split: split_if_asm)
+    apply (auto dest!: PiE_mem split: split_if_asm)
     done
 qed
 
 lemma extensional_funcset_extend_domain_inj_onI:
   assumes "x \<notin> S"
-  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
 proof -
   from assms show ?thesis
     apply (auto intro!: inj_onI)
     apply (metis fun_upd_same)
-    by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
+    by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
 qed
   
 
 subsubsection {* Cardinality *}
 
-lemma card_extensional_funcset:
-  assumes "finite S"
-  shows "card (extensional_funcset S T) = (card T) ^ (card S)"
-using assms
-proof (induct rule: finite_induct)
-  case empty
-  show ?case
-    by (auto simp add: extensional_funcset_empty_domain)
-next
-  case (insert x S)
-  {
-    fix g g' y y'
-    assume assms: "g \<in> extensional_funcset S T"
-      "g' \<in> extensional_funcset S T"
-      "y \<in> T" "y' \<in> T"
-      "g(x := y) = g'(x := y')"
-    from this have "y = y'"
-      by (metis fun_upd_same)
-    have "g = g'"
-      by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
-  from `y = y'` `g = g'` have "y = y' & g = g'" by simp
-  }
-  from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
-    by (auto intro: inj_onI)
-  from this insert.hyps show ?case
-    by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
+lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
+  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
+
+lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)"
+proof (safe intro!: inj_onI ext)
+  fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^isub>E S T" "g \<in> Pi\<^isub>E S T"
+  assume "f(x := y) = g(x := z)"
+  then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
+    unfolding fun_eq_iff by auto
+  from this[of x] show "y = z" by simp
+  fix i from *[of i] `x \<notin> S` fg show "f i = g i"
+    by (auto split: split_if_asm simp: PiE_def extensional_def)
 qed
 
-lemma finite_extensional_funcset:
-  assumes "finite S" "finite T"
-  shows "finite (extensional_funcset S T)"
-proof -
-  from card_extensional_funcset[OF assms(1), of T] assms(2)
-  have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
-    by auto
-  from this show ?thesis
-  proof
-    assume "card (extensional_funcset S T) \<noteq> 0"
-    from this show ?thesis
-      by (auto intro: card_ge_0_finite)
-  next
-    assume "S \<noteq> {} \<and> T = {}"
-    from this show ?thesis
-      by (auto simp add: extensional_funcset_empty_range)
-  qed
+lemma card_PiE:
+  "finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))"
+proof (induct rule: finite_induct)
+  case empty then show ?case by auto
+next
+  case (insert x S) then show ?case
+    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
 qed
 
 end
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -1284,17 +1284,16 @@
   assumes "finite J"
   shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
 proof (rule measurable_PiM)
-  show "(\<lambda>m. compose J m f)
-    \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow>
-      (J \<rightarrow> space M) \<inter> extensional J"
+  show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
   proof safe
     fix x and i
     assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
     with inj show  "compose J x f i \<in> space M"
       by (auto simp: space_PiM compose_def)
   next
-    fix x assume "x \<in> space (PiM (f ` J) (\<lambda>_. M))"
-    show "(compose J x f) \<in> extensional J" by (rule compose_extensional)
+    fix x i assume "i \<notin> J"
+    with compose_extensional[of J x f]
+    show "compose J x f i = undefined" by (auto simp: extensional_def)
   qed
 next
   fix S X
@@ -1303,7 +1302,7 @@
   have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
     space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) = prod_emb (f ` J) (\<lambda>_. M) (f ` S) (Pi\<^isub>E (f ` S) (\<lambda>b. X (f' b)))"
     using assms inv S sets_into_space[OF P]
-    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def intro: imageI)
+    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
   also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
   proof
     from S show "f ` S \<subseteq> f `  J" by auto
@@ -1379,7 +1378,7 @@
   assumes "\<And>i. space (M i) = UNIV"
   shows "inj_on fm (space (Pi\<^isub>M J M))"
   using assms
-  apply (auto simp: fm_def space_PiM)
+  apply (auto simp: fm_def space_PiM PiE_def)
   apply (rule comp_inj_on)
   apply (rule inj_on_compose_f')
   apply (rule finmap_of_inj_on_extensional_finite)
@@ -1409,7 +1408,7 @@
     by (auto simp: mf_def extensional_def compose_def)
   moreover
   have "x \<in> extensional J" using assms sets_into_space
-    by (force simp: space_PiM)
+    by (force simp: space_PiM PiE_def)
   moreover
   { fix i assume "i \<in> J"
     hence "mf (fm x) i = x i"
@@ -1472,13 +1471,13 @@
 
 lemma mapmeasure_PiF:
   assumes s1: "space M = space (Pi\<^isub>M J (\<lambda>_. N))"
-  assumes s2: "sets M = (Pi\<^isub>M J (\<lambda>_. N))"
+  assumes s2: "sets M = sets (Pi\<^isub>M J (\<lambda>_. N))"
   assumes "space N = UNIV"
   assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
   shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
   using assms
   by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
-    fm_measurable space_PiM)
+    fm_measurable space_PiM PiE_def)
 
 lemma mapmeasure_PiM:
   fixes N::"'c measure"
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -11,46 +11,7 @@
 lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   by auto
 
-abbreviation
-  "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
-
-syntax
-  "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
-
-syntax (xsymbols)
-  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
-
-syntax (HTML output)
-  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
-
-translations
-  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
-
-abbreviation
-  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
-    (infixr "->\<^isub>E" 60) where
-  "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
-
-notation (xsymbols)
-  funcset_extensional  (infixr "\<rightarrow>\<^isub>E" 60)
-
-lemma extensional_insert[intro, simp]:
-  assumes "a \<in> extensional (insert i I)"
-  shows "a(i := b) \<in> extensional (insert i I)"
-  using assms unfolding extensional_def by auto
-
-lemma extensional_Int[simp]:
-  "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)
+subsubsection {* Merge two extensional functions *}
 
 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)"
@@ -84,9 +45,6 @@
 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 J (x, y)) I = restrict x I"
   "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
@@ -97,9 +55,26 @@
 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 PiE_cancel_merge[simp]:
+  "I \<inter> J = {} \<Longrightarrow>
+    merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
+  by (auto simp: PiE_def restrict_Pi_cancel)
+
+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 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 merge_restrict[simp]:
+  "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 J (x, x) = restrict x (I \<union> J)"
+  unfolding merge_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> {}"
@@ -113,195 +88,22 @@
   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)
+      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
+      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
     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
+      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
+      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
+  qed (insert sets, auto)
 qed
 
-lemma extensional_insert_undefined[intro, simp]:
-  assumes "a \<in> extensional (insert i I)"
-  shows "a(i := undefined) \<in> extensional I"
-  using assms unfolding extensional_def by auto
-
-lemma extensional_insert_cancel[intro, simp]:
-  assumes "a \<in> extensional I"
-  shows "a \<in> extensional (insert i I)"
-  using assms unfolding extensional_def by auto
-
-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)"
-  by auto
-
-lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
-  by auto
-
-lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
-  by (auto simp: Pi_def)
-
-lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
-  by (auto simp: Pi_def)
-
-lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
-  by (auto simp: Pi_def)
-
-lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
-  by (auto simp: Pi_def)
-
 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 J (E, F))"
-  using assms by (auto simp: restrict_Pi_cancel)
+  "I \<inter> J = {} \<Longrightarrow>
+    (\<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))"
+  by (auto simp: restrict_Pi_cancel PiE_def)
 
 lemma merge_vimage:
-  assumes "I \<inter> J = {}"
-  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 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 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"
-  apply auto
-  apply (drule_tac x=x in Pi_mem)
-  apply (simp_all split: split_if_asm)
-  apply (drule_tac x=i in Pi_mem)
-  apply (auto dest!: Pi_mem)
-  done
-
-lemma Pi_UN:
-  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
-  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
-  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
-proof (intro set_eqI iffI)
-  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
-  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
-  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
-  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
-    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
-  have "f \<in> Pi I (A k)"
-  proof (intro Pi_I)
-    fix i assume "i \<in> I"
-    from mono[OF this, of "n i" k] k[OF this] n[OF this]
-    show "f i \<in> A k i" by auto
-  qed
-  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
-qed auto
-
-lemma PiE_cong:
-  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
-  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
-  using assms by (auto intro!: Pi_cong)
-
-lemma restrict_upd[simp]:
-  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
-  by (auto simp: fun_eq_iff)
-
-lemma Pi_eq_subset:
-  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
-  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
-  shows "F i \<subseteq> F' i"
-proof
-  fix x assume "x \<in> F i"
-  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
-  from choice[OF this] guess f .. note f = this
-  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
-  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
-  then show "x \<in> F' i" using f `i \<in> I` by auto
-qed
-
-lemma Pi_eq_iff_not_empty:
-  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
-  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
-proof (intro iffI ballI)
-  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
-  show "F i = F' i"
-    using Pi_eq_subset[of I F F', OF ne eq i]
-    using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
-    by auto
-qed auto
-
-lemma Pi_eq_empty_iff:
-  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
-proof
-  assume "Pi\<^isub>E I F = {}"
-  show "\<exists>i\<in>I. F i = {}"
-  proof (rule ccontr)
-    assume "\<not> ?thesis"
-    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
-    from choice[OF this] guess f ..
-    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
-    with `Pi\<^isub>E I F = {}` show False by auto
-  qed
-qed auto
-
-lemma Pi_eq_iff:
-  "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
-proof (intro iffI disjCI)
-  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
-  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
-  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
-    using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
-  with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
-next
-  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
-  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
-    using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
-qed
-
-lemma funset_eq_UN_fun_upd_I:
-  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
-  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
-  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
-  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
-proof safe
-  fix f assume f: "f \<in> F (insert a A)"
-  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
-  proof (rule UN_I[of "f(a := d)"])
-    show "f(a := d) \<in> F A" using *[OF f] .
-    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
-    proof (rule image_eqI[of _ _ "f a"])
-      show "f a \<in> G (f(a := d))" using **[OF f] .
-    qed simp
-  qed
-next
-  fix f x assume "f \<in> F A" "x \<in> G f"
-  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
-qed
-
-lemma extensional_funcset_insert_eq[simp]:
-  assumes "a \<notin> A"
-  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)"
-  apply (rule funset_eq_UN_fun_upd_I)
-  using assms
-  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
-
-lemma finite_extensional_funcset[simp, intro]:
-  assumes "finite A" "finite B"
-  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
-  using assms by induct auto
-
-lemma finite_PiE[simp, intro]:
-  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
-  shows "finite (Pi\<^isub>E A B)"
-proof -
-  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
-  show ?thesis
-    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
-qed
+  "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
+  by (auto simp: restrict_Pi_cancel PiE_def)
 
 section "Finite product spaces"
 
@@ -312,7 +114,7 @@
 
 lemma prod_emb_iff: 
   "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
-  unfolding prod_emb_def by auto
+  unfolding prod_emb_def PiE_def by auto
 
 lemma
   shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
@@ -325,24 +127,25 @@
 
 lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
     prod_emb I M J (\<Pi>\<^isub>E i\<in>J. E i) = (\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i))"
-  by (force simp: prod_emb_def Pi_iff split_if_mem2)
+  by (force simp: prod_emb_def PiE_iff split_if_mem2)
 
-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_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 PiE_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)
+  by (auto simp add: Int_absorb1 prod_emb_def PiE_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+
+  by (auto simp: prod_emb_def PiE_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)
+  by (auto simp: prod_emb_def 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"
@@ -392,9 +195,9 @@
     by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
 next
   fix A assume "A \<in> ?R"
-  then obtain X where "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
+  then obtain X where A: "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
   then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
-    using sets_into_space by (force simp: prod_emb_def Pi_iff)
+    by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
   from X I show "A \<in> ?L" unfolding A
     by (auto simp: prod_algebra_def)
 qed
@@ -402,7 +205,7 @@
 lemma prod_algebraI:
   "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
     \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
-  by (auto simp: prod_algebra_def Pi_iff)
+  by (auto simp: prod_algebra_def)
 
 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"
@@ -412,7 +215,7 @@
 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"])
+    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
 qed
 
 lemma prod_algebraE:
@@ -501,7 +304,7 @@
   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)
+    by (auto simp: prod_emb_def)
   also have "\<dots> \<in> prod_algebra I M"
     using `i \<in> I` by (intro prod_algebraI) auto
   finally show ?thesis .
@@ -529,8 +332,7 @@
   next
     assume "I \<noteq> {}"
     with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^isub>E i\<in>I. space (M i)). f j \<in> X j})"
-      using sets_into_space[OF X(5)]
-      by (auto simp: prod_emb_PiE[OF _ sets_into_space] Pi_iff split: split_if_asm) blast
+      by (auto simp: prod_emb_def)
     also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
       using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
     finally show "A \<in> sigma_sets ?\<Omega> ?R" .
@@ -540,11 +342,7 @@
   then obtain i B where A: "A = {f\<in>\<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)" 
     by auto
   then have "A = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. B)"
-    using sets_into_space[OF A(3)]
-    apply (subst prod_emb_PiE)
-    apply (auto simp: Pi_iff split: split_if_asm)
-    apply blast
-    done
+     by (auto simp: prod_emb_def)
   also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
     using A by (intro sigma_sets.Basic prod_algebraI) auto
   finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
@@ -585,9 +383,8 @@
 proof (rule measurable_sigma_sets)
   fix A assume "A \<in> prod_algebra I M"
   from prod_algebraE[OF this] guess J X . note X = this
-  have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
-    using sets_into_space[OF X(5)] X(2-) space unfolding X(1)
-    by (subst prod_emb_PiE) (auto simp: Pi_iff split: split_if_asm)
+  then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
+    using space by (auto simp: prod_emb_def del: PiE_I)
   also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
   finally show "f -` A \<inter> space N \<in> sets N" .
 qed
@@ -654,7 +451,7 @@
   assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   using fg[THEN measurable_space]
-  by (auto intro!: measurable_PiM_single' simp add: space_PiM Pi_iff split: nat.split)
+  by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
 
 lemma measurable_add_dim[measurable]:
   "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
@@ -668,7 +465,7 @@
     using A j
     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
-qed (auto simp: space_pair_measure space_PiM)
+qed (auto simp: space_pair_measure space_PiM PiE_def)
 
 lemma measurable_component_update:
   "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
@@ -686,7 +483,7 @@
     using A
     by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   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)
+qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
 
 lemma measurable_restrict[measurable (raw)]:
   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
@@ -697,7 +494,7 @@
     by auto
   then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
     using A X by (auto intro!: measurable_sets)
-qed (insert X, auto dest: measurable_space)
+qed (insert X, auto simp add: PiE_def 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
@@ -762,13 +559,12 @@
   next
     fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
   next
-    fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space (PiM I M)"
-      using `\<And>i. range (F i) \<subseteq> sets (M i)` sets_into_space
-      by auto blast
+    fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
+      by (auto simp: PiE_def dest!: sets_into_space)
   next
     fix f assume "f \<in> space (PiM I M)"
     with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
-    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
+    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
   next
     fix i show "?F i \<subseteq> ?F (Suc i)"
       using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
@@ -826,13 +622,13 @@
       by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
     also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
       using J E[rule_format, THEN sets_into_space]
-      by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
+      by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
     also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
       emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
       using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
     also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
       using J E[rule_format, THEN sets_into_space]
-      by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
+      by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
     also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
       (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
       using E by (subst insert) (auto intro!: setprod_cong)
@@ -844,7 +640,7 @@
     finally show "?\<mu> ?p = \<dots>" .
 
     show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
-      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
+      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   next
     show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
       using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
@@ -961,7 +757,7 @@
       using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
     also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
       using `finite J` `finite I` F unfolding X
-      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
+      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times)
     also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
     also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
@@ -1034,7 +830,7 @@
     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)
+               simp add: space_PiM extensional_def PiE_def)
   qed
 qed
 
@@ -1085,7 +881,7 @@
   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)
+    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def 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" .
@@ -1160,7 +956,7 @@
       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 {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)
+      by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
   qed
   finally show ?thesis .
 qed
@@ -1233,7 +1029,7 @@
 proof
   let ?P = "sigma (space (Pi\<^isub>M I M)) P"
   have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
-    using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+    using E_closed by (auto simp: space_PiM P_def subset_eq)
   then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
     by (simp add: space_PiM)
   have "sets (PiM I M) =
@@ -1281,7 +1077,7 @@
   then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
     by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
   have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
-    using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
+    using E_closed by (auto simp: space_PiM P_def subset_eq)
   then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
     by (simp add: space_PiM)
   have "sets (PiM I M) =
@@ -1293,18 +1089,17 @@
     have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
     proof (subst measurable_iff_measure_of)
       show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
-      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)"
-        by (auto simp: Pi_iff)
+      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
       show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
       proof
         fix A assume A: "A \<in> E i"
         then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
-          using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
+          using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
         also have "\<dots> = (\<Pi>\<^isub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
           by (intro PiE_cong) (simp add: S_union)
         also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j))"
           using T
-          apply (auto simp: Pi_iff bchoice_iff)
+          apply (auto simp: PiE_iff bchoice_iff)
           apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
           apply (auto simp: bij_betw_def)
           done
@@ -1352,7 +1147,7 @@
     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)
+    by (auto simp: PiE_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"]
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -867,7 +867,7 @@
       then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
         by (simp add: emeasure_distr X)
       also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
-        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
+        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
       also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
         using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J]
         by (auto simp: emeasure_eq_measure setprod_ereal)
@@ -898,7 +898,7 @@
         Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
       let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)"
       from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
-        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
+        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
       then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
         by simp
       also have "\<dots> = emeasure ?D ?E"
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -234,11 +234,9 @@
               using w'(1) J(3)[of "Suc k"]
               by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
             show ?thesis
-              apply (rule exI[of _ ?w])
               using w' J_mono[of k "Suc k"] wk unfolding *
-              apply (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM)
-              apply (force simp: extensional_def)
-              done
+              by (intro exI[of _ ?w])
+                 (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
           qed
           then have "?P k (w k) (w (Suc k))"
             unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
@@ -295,8 +293,8 @@
         using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
 
       { fix n
-        have "restrict w' (J n) = w n" using w(1)
-          by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def space_PiM)
+        have "restrict w' (J n) = w n" using w(1)[of n]
+          by (auto simp add: fun_eq_iff space_PiM)
         with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
         then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
       then have "w' \<in> (\<Inter>i. A i)" by auto
@@ -391,7 +389,7 @@
 lemma sets_Collect_single':
   "i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
   using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
-  by (simp add: space_PiM Pi_iff cong: conj_cong)
+  by (simp add: space_PiM PiE_iff cong: conj_cong)
 
 lemma (in finite_product_prob_space) finite_measure_PiM_emb:
   "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
@@ -462,7 +460,7 @@
   "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
 proof (rule measurable_PiM_single)
   show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
-    by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
+    by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
   fix j :: nat and A assume A: "A \<in> sets M"
   then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
     (if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
@@ -550,7 +548,7 @@
   with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
     (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
     (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
-   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib Pi_iff
+   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
                split: split_comb_seq split_comb_seq_asm)
   then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^isub>M S) (?E \<times> ?F)"
     by (subst emeasure_distr[OF measurable_comb_seq])
@@ -581,7 +579,7 @@
     using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
     (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
-   by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
+   by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
       split: nat.split nat.split_asm)
   then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
     by (subst emeasure_distr)
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -935,7 +935,7 @@
   fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
   then obtain x where  "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
   then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
-    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
+    using DIM_positive by (auto simp add: set_eq_iff e2p_def
       euclidean_eq[where 'a='a] eucl_less[where 'a='a])
   then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
 qed (auto simp: e2p_def)
@@ -953,7 +953,7 @@
   let ?A = "{w \<in> space ?P. (p2e w :: 'a) $$ i \<le> x}"
   assume "i < DIM('a)"
   then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
-    using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
+    using DIM_positive by (auto simp: space_PiM p2e_def PiE_def split: split_if_asm)
   then show "?A \<in> sets ?P"
     by auto
 qed
@@ -966,7 +966,7 @@
   let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
   fix a b :: 'a
   have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
-    by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
+    by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff)
   have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
   proof cases
     assume "{a..b} \<noteq> {}"
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -44,7 +44,7 @@
   also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
     using E by (simp add: K.measure_times)
   also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
-    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
+    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
     using X `J \<subseteq> K` apply (subst emeasure_distr)
     by (auto intro!: measurable_restrict_subset simp: space_PiM)
@@ -93,15 +93,10 @@
   shows "emeasure (limP 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
+    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
   hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
     emeasure (limP 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)
+    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
   proof (rule emeasure_extend_measure_Pair[OF limP_def])
     show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
@@ -169,7 +164,7 @@
     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 "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
   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
@@ -293,7 +288,7 @@
   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)
+    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
        auto
 qed
 
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -428,7 +428,7 @@
           also have "\<dots> = P (J i) (B i) - P' i (K' i)"
             unfolding K_def P'_def
             by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric]
-              compact_imp_closed[OF `compact (K' _)`] space_PiM)
+              compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def)
           also have "\<dots> \<le> ereal (2 powr - real i) * ?a" using K'(1)[of i] .
           finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" .
         qed
@@ -580,7 +580,7 @@
         ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"
           unfolding K_def by (auto simp: proj_space space_PiM)
         hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def
-          using J by (auto simp: prod_emb_def extensional_def)
+          using J by (auto simp: prod_emb_def PiE_def extensional_def)
         also have "\<dots> \<subseteq> Z n" using Z' by simp
         finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .
       } note in_Z = this
@@ -602,7 +602,7 @@
       using assms by (auto simp: f_def)
   next
     fix J and X::"'i \<Rightarrow> 'a set"
-    show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow ((I \<rightarrow> space borel) \<inter> extensional I)"
+    show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow (I \<rightarrow>\<^isub>E space borel)"
       by (auto simp: prod_emb_def)
     assume JX: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> J \<rightarrow> sets borel"
     hence "emb I J (Pi\<^isub>E J X) \<in> generator" using assms
@@ -645,11 +645,11 @@
     interpret prob_space "P {i}" using proj_prob_space by simp
     have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
       by (auto simp: prod_emb_def space_PiM)
-    moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
+    moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM PiE_def)
     ultimately show ?thesis using `i \<in> I`
       apply (subst R)
       apply (subst emeasure_limB_emb_not_empty)
-      apply (auto simp: limP_finite emeasure_space_1)
+      apply (auto simp: limP_finite emeasure_space_1 PiE_def)
       done
   qed
 qed
diff -r 7ae7efef5ad8 -r 69b35a75caf3 src/HOL/ex/Birthday_Paradox.thy
--- a/src/HOL/ex/Birthday_Paradox.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/ex/Birthday_Paradox.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -14,21 +14,7 @@
   assumes "finite S"
   assumes "\<forall>x \<in> S. finite (T x)" 
   shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
-proof -
-  note `finite S`
-  moreover
-  have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
-  moreover
-  from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
-  moreover
-  have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
-  moreover  
-  ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
-    by (auto, subst card_UN_disjoint) auto
-  also have "... = (SUM x:S. card (T x))"
-    by (subst card_image) (auto intro: inj_onI)
-  finally show ?thesis by auto
-qed
+  using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
 
 lemma card_extensional_funcset_inj_on:
   assumes "finite S" "finite T" "card S \<le> card T"
@@ -36,13 +22,13 @@
 using assms
 proof (induct S arbitrary: T rule: finite_induct)
   case empty
-  from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
+  from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
 next
   case (insert x S)
   { fix x
     from `finite T` have "finite (T - {x})" by auto
     from `finite S` this have "finite (extensional_funcset S (T - {x}))"
-      by (rule finite_extensional_funcset)
+      by (rule finite_PiE)
     moreover
     have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
     ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
@@ -75,10 +61,10 @@
 proof -
   have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
   from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
-    by (auto intro!: finite_extensional_funcset)
+    by (auto intro!: finite_PiE)
   have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto 
   from assms this finite subset show ?thesis
-    by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
+    by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
 qed
 
 lemma setprod_upto_nat_unfold:
@@ -93,9 +79,9 @@
 proof -
   from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
   from assms show ?thesis
-    using card_extensional_funcset[OF `finite S`, of T]
+    using card_PiE[OF `finite S`, of "\<lambda>i. T"] `finite S`
       card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
-    by (simp add: fact_div_fact setprod_upto_nat_unfold)
+    by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
 qed
 
 end