merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
authorhoelzl
Mon Nov 19 12:29:02 2012 +0100 (2012-11-19)
changeset 5012369b35a75caf3
parent 50122 7ae7efef5ad8
child 50124 4161c834c2fd
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/ex/Birthday_Paradox.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Nov 19 16:14:18 2012 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Nov 19 12:29:02 2012 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
     1.5    by auto
     1.6  
     1.7 -lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
     1.8 +lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B x = {})"
     1.9  apply (simp add: Pi_def, auto)
    1.10  txt{*Converse direction requires Axiom of Choice to exhibit a function
    1.11  picking an element from each non-empty @{term "B x"}*}
    1.12 @@ -97,12 +97,31 @@
    1.13  lemma Pi_empty [simp]: "Pi {} B = UNIV"
    1.14  by (simp add: Pi_def)
    1.15  
    1.16 +lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
    1.17 +  by auto
    1.18 +
    1.19 +lemma Pi_UN:
    1.20 +  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
    1.21 +  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
    1.22 +  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
    1.23 +proof (intro set_eqI iffI)
    1.24 +  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
    1.25 +  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
    1.26 +  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
    1.27 +  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
    1.28 +    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
    1.29 +  have "f \<in> Pi I (A k)"
    1.30 +  proof (intro Pi_I)
    1.31 +    fix i assume "i \<in> I"
    1.32 +    from mono[OF this, of "n i" k] k[OF this] n[OF this]
    1.33 +    show "f i \<in> A k i" by auto
    1.34 +  qed
    1.35 +  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
    1.36 +qed auto
    1.37 +
    1.38  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
    1.39  by (simp add: Pi_def)
    1.40 -(*
    1.41 -lemma funcset_id [simp]: "(%x. x): A -> A"
    1.42 -  by (simp add: Pi_def)
    1.43 -*)
    1.44 +
    1.45  text{*Covariance of Pi-sets in their second argument*}
    1.46  lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
    1.47  by auto
    1.48 @@ -124,6 +143,25 @@
    1.49    finally show "f z \<in> B z \<times> C z" .
    1.50  qed
    1.51  
    1.52 +lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
    1.53 +  by (auto simp: Pi_def)
    1.54 +
    1.55 +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"
    1.56 +  by (auto simp: Pi_def)
    1.57 +
    1.58 +lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
    1.59 +  by (auto simp: Pi_def)
    1.60 +
    1.61 +lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    1.62 +  by (auto simp: Pi_def)
    1.63 +
    1.64 +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"
    1.65 +  apply auto
    1.66 +  apply (drule_tac x=x in Pi_mem)
    1.67 +  apply (simp_all split: split_if_asm)
    1.68 +  apply (drule_tac x=i in Pi_mem)
    1.69 +  apply (auto dest!: Pi_mem)
    1.70 +  done
    1.71  
    1.72  subsection{*Composition With a Restricted Domain: @{term compose}*}
    1.73  
    1.74 @@ -173,6 +211,19 @@
    1.75  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
    1.76    by (auto simp add: restrict_def)
    1.77  
    1.78 +lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
    1.79 +  unfolding restrict_def by (simp add: fun_eq_iff)
    1.80 +
    1.81 +lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
    1.82 +  by (auto simp: restrict_def)
    1.83 +
    1.84 +lemma restrict_upd[simp]:
    1.85 +  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
    1.86 +  by (auto simp: fun_eq_iff)
    1.87 +
    1.88 +lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
    1.89 +  by (auto simp: restrict_def Pi_def)
    1.90 +
    1.91  
    1.92  subsection{*Bijections Between Sets*}
    1.93  
    1.94 @@ -213,6 +264,9 @@
    1.95  
    1.96  subsection{*Extensionality*}
    1.97  
    1.98 +lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
    1.99 +  unfolding extensional_def by auto
   1.100 +
   1.101  lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
   1.102  by (simp add: extensional_def)
   1.103  
   1.104 @@ -230,6 +284,9 @@
   1.105  lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
   1.106  by(rule extensionalityI[OF restrict_extensional]) auto
   1.107  
   1.108 +lemma extensional_subset: "f \<in> extensional A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f \<in> extensional B"
   1.109 +  unfolding extensional_def by auto
   1.110 +
   1.111  lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
   1.112  by (unfold inv_into_def) (fast intro: someI2)
   1.113  
   1.114 @@ -246,6 +303,29 @@
   1.115  apply (simp add: f_inv_into_f)
   1.116  done
   1.117  
   1.118 +lemma extensional_insert[intro, simp]:
   1.119 +  assumes "a \<in> extensional (insert i I)"
   1.120 +  shows "a(i := b) \<in> extensional (insert i I)"
   1.121 +  using assms unfolding extensional_def by auto
   1.122 +
   1.123 +lemma extensional_Int[simp]:
   1.124 +  "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
   1.125 +  unfolding extensional_def by auto
   1.126 +
   1.127 +lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
   1.128 +  by (auto simp: extensional_def)
   1.129 +
   1.130 +lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
   1.131 +  unfolding restrict_def extensional_def by auto
   1.132 +
   1.133 +lemma extensional_insert_undefined[intro, simp]:
   1.134 +  "a \<in> extensional (insert i I) \<Longrightarrow> a(i := undefined) \<in> extensional I"
   1.135 +  unfolding extensional_def by auto
   1.136 +
   1.137 +lemma extensional_insert_cancel[intro, simp]:
   1.138 +  "a \<in> extensional I \<Longrightarrow> a \<in> extensional (insert i I)"
   1.139 +  unfolding extensional_def by auto
   1.140 +
   1.141  
   1.142  subsection{*Cardinality*}
   1.143  
   1.144 @@ -259,156 +339,207 @@
   1.145  
   1.146  subsection {* Extensional Function Spaces *} 
   1.147  
   1.148 -definition extensional_funcset
   1.149 -where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
   1.150 +definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
   1.151 +  "PiE S T = Pi S T \<inter> extensional S"
   1.152 +
   1.153 +abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
   1.154  
   1.155 -lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
   1.156 -unfolding extensional_def by auto
   1.157 +syntax "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
   1.158 +
   1.159 +syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
   1.160 +
   1.161 +syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
   1.162 +
   1.163 +translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
   1.164  
   1.165 -lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
   1.166 -unfolding extensional_funcset_def by simp
   1.167 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^isub>E" 60) where
   1.168 +  "A ->\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)"
   1.169 +
   1.170 +notation (xsymbols)
   1.171 +  extensional_funcset  (infixr "\<rightarrow>\<^isub>E" 60)
   1.172  
   1.173 -lemma extensional_funcset_empty_range:
   1.174 -  assumes "S \<noteq> {}"
   1.175 -  shows "extensional_funcset S {} = {}"
   1.176 -using assms unfolding extensional_funcset_def by auto
   1.177 +lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
   1.178 +  by (simp add: PiE_def)
   1.179 +
   1.180 +lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
   1.181 +  unfolding PiE_def by simp
   1.182 +
   1.183 +lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
   1.184 +  unfolding PiE_def by auto
   1.185  
   1.186 -lemma extensional_funcset_arb:
   1.187 -  assumes "f \<in> extensional_funcset S T" "x \<notin> S"
   1.188 -  shows "f x = undefined"
   1.189 -using assms
   1.190 -unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
   1.191 -
   1.192 -lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
   1.193 -unfolding extensional_funcset_def by auto
   1.194 -
   1.195 -lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
   1.196 -unfolding extensional_def by auto
   1.197 +lemma PiE_eq_empty_iff:
   1.198 +  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   1.199 +proof
   1.200 +  assume "Pi\<^isub>E I F = {}"
   1.201 +  show "\<exists>i\<in>I. F i = {}"
   1.202 +  proof (rule ccontr)
   1.203 +    assume "\<not> ?thesis"
   1.204 +    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
   1.205 +    from choice[OF this] guess f ..
   1.206 +    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
   1.207 +    with `Pi\<^isub>E I F = {}` show False by auto
   1.208 +  qed
   1.209 +qed (auto simp: PiE_def)
   1.210  
   1.211 -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"
   1.212 -unfolding extensional_funcset_def extensional_def by auto
   1.213 +lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
   1.214 +  unfolding PiE_def by auto (auto dest!: extensional_arb)
   1.215 +
   1.216 +lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
   1.217 +  unfolding PiE_def by auto
   1.218  
   1.219 -lemma extensional_funcset_restrict_domain:
   1.220 -  "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
   1.221 -unfolding extensional_funcset_def extensional_def by auto
   1.222 +lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
   1.223 +  unfolding PiE_def extensional_def by auto
   1.224  
   1.225 -lemma extensional_funcset_extend_domain_eq:
   1.226 +lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
   1.227 +  unfolding PiE_def extensional_def by auto
   1.228 +
   1.229 +lemma PiE_insert_eq:
   1.230    assumes "x \<notin> S"
   1.231 -  shows
   1.232 -    "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
   1.233 -  using assms
   1.234 +  shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
   1.235  proof -
   1.236    {
   1.237 -    fix f
   1.238 -    assume "f : extensional_funcset (insert x S) T"
   1.239 -    from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
   1.240 -      unfolding image_iff
   1.241 -      apply (rule_tac x="(f x, f(x := undefined))" in bexI)
   1.242 -    apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done 
   1.243 +    fix f assume "f \<in> PiE (insert x S) T"
   1.244 +    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
   1.245 +      by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   1.246    }
   1.247 -  moreover
   1.248 -  {
   1.249 -    fix f
   1.250 -    assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
   1.251 -    from this assms have "f : extensional_funcset (insert x S) T"
   1.252 -      by (auto intro: extensional_funcset_extend_domainI)
   1.253 -  }
   1.254 -  ultimately show ?thesis by auto
   1.255 +  then show ?thesis using assms by (auto intro: PiE_fun_upd)
   1.256  qed
   1.257  
   1.258 -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})"
   1.259 -unfolding extensional_funcset_def extensional_def
   1.260 -apply auto
   1.261 -apply (case_tac "x = xa")
   1.262 -apply auto done
   1.263 +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)"
   1.264 +  by (auto simp: PiE_def)
   1.265 +
   1.266 +lemma PiE_cong:
   1.267 +  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B"
   1.268 +  unfolding PiE_def by (auto simp: Pi_cong)
   1.269 +
   1.270 +lemma PiE_E [elim]:
   1.271 +  "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"
   1.272 +by(auto simp: Pi_def PiE_def extensional_def)
   1.273 +
   1.274 +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"
   1.275 +  by (simp add: PiE_def extensional_def)
   1.276 +
   1.277 +lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
   1.278 +  by auto
   1.279 +
   1.280 +lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   1.281 +  by (simp add: PiE_def Pi_iff)
   1.282 +
   1.283 +lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
   1.284 +  by (simp add: extensional_restrict PiE_def)
   1.285 +
   1.286 +lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
   1.287 +  by (auto simp: PiE_iff)
   1.288 +
   1.289 +lemma PiE_eq_subset:
   1.290 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   1.291 +  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
   1.292 +  shows "F i \<subseteq> F' i"
   1.293 +proof
   1.294 +  fix x assume "x \<in> F i"
   1.295 +  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
   1.296 +  from choice[OF this] guess f .. note f = this
   1.297 +  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
   1.298 +  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
   1.299 +  then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
   1.300 +qed
   1.301 +
   1.302 +lemma PiE_eq_iff_not_empty:
   1.303 +  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   1.304 +  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   1.305 +proof (intro iffI ballI)
   1.306 +  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
   1.307 +  show "F i = F' i"
   1.308 +    using PiE_eq_subset[of I F F', OF ne eq i]
   1.309 +    using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   1.310 +    by auto
   1.311 +qed (auto simp: PiE_def)
   1.312 +
   1.313 +lemma PiE_eq_iff:
   1.314 +  "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 = {}))"
   1.315 +proof (intro iffI disjCI)
   1.316 +  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   1.317 +  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   1.318 +  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   1.319 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
   1.320 +  with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
   1.321 +next
   1.322 +  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   1.323 +  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   1.324 +    using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
   1.325 +qed
   1.326 +
   1.327 +lemma extensional_funcset_fun_upd_restricts_rangeI: 
   1.328 +  "\<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})"
   1.329 +  unfolding extensional_funcset_def extensional_def
   1.330 +  apply auto
   1.331 +  apply (case_tac "x = xa")
   1.332 +  apply auto
   1.333 +  done
   1.334  
   1.335  lemma extensional_funcset_fun_upd_extends_rangeI:
   1.336 -  assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
   1.337 -  shows "f(x := a) : extensional_funcset (insert x S) T"
   1.338 +  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T - {a})"
   1.339 +  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E  T"
   1.340    using assms unfolding extensional_funcset_def extensional_def by auto
   1.341  
   1.342  subsubsection {* Injective Extensional Function Spaces *}
   1.343  
   1.344  lemma extensional_funcset_fun_upd_inj_onI:
   1.345 -  assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
   1.346 +  assumes "f \<in> S \<rightarrow>\<^isub>E (T - {a})" "inj_on f S"
   1.347    shows "inj_on (f(x := a)) S"
   1.348    using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
   1.349  
   1.350  lemma extensional_funcset_extend_domain_inj_on_eq:
   1.351    assumes "x \<notin> S"
   1.352 -  shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
   1.353 -    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
   1.354 +  shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} =
   1.355 +    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
   1.356  proof -
   1.357    from assms show ?thesis
   1.358 -    apply auto
   1.359 -    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
   1.360 +    apply (auto del: PiE_I PiE_E)
   1.361 +    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
   1.362      apply (auto simp add: image_iff inj_on_def)
   1.363      apply (rule_tac x="xa x" in exI)
   1.364 -    apply (auto intro: extensional_funcset_mem)
   1.365 +    apply (auto intro: PiE_mem del: PiE_I PiE_E)
   1.366      apply (rule_tac x="xa(x := undefined)" in exI)
   1.367      apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
   1.368 -    apply (auto dest!: extensional_funcset_mem split: split_if_asm)
   1.369 +    apply (auto dest!: PiE_mem split: split_if_asm)
   1.370      done
   1.371  qed
   1.372  
   1.373  lemma extensional_funcset_extend_domain_inj_onI:
   1.374    assumes "x \<notin> S"
   1.375 -  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}"
   1.376 +  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}"
   1.377  proof -
   1.378    from assms show ?thesis
   1.379      apply (auto intro!: inj_onI)
   1.380      apply (metis fun_upd_same)
   1.381 -    by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
   1.382 +    by (metis assms PiE_arb fun_upd_triv fun_upd_upd)
   1.383  qed
   1.384    
   1.385  
   1.386  subsubsection {* Cardinality *}
   1.387  
   1.388 -lemma card_extensional_funcset:
   1.389 -  assumes "finite S"
   1.390 -  shows "card (extensional_funcset S T) = (card T) ^ (card S)"
   1.391 -using assms
   1.392 -proof (induct rule: finite_induct)
   1.393 -  case empty
   1.394 -  show ?case
   1.395 -    by (auto simp add: extensional_funcset_empty_domain)
   1.396 -next
   1.397 -  case (insert x S)
   1.398 -  {
   1.399 -    fix g g' y y'
   1.400 -    assume assms: "g \<in> extensional_funcset S T"
   1.401 -      "g' \<in> extensional_funcset S T"
   1.402 -      "y \<in> T" "y' \<in> T"
   1.403 -      "g(x := y) = g'(x := y')"
   1.404 -    from this have "y = y'"
   1.405 -      by (metis fun_upd_same)
   1.406 -    have "g = g'"
   1.407 -      by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
   1.408 -  from `y = y'` `g = g'` have "y = y' & g = g'" by simp
   1.409 -  }
   1.410 -  from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
   1.411 -    by (auto intro: inj_onI)
   1.412 -  from this insert.hyps show ?case
   1.413 -    by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
   1.414 +lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
   1.415 +  by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
   1.416 +
   1.417 +lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)"
   1.418 +proof (safe intro!: inj_onI ext)
   1.419 +  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"
   1.420 +  assume "f(x := y) = g(x := z)"
   1.421 +  then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
   1.422 +    unfolding fun_eq_iff by auto
   1.423 +  from this[of x] show "y = z" by simp
   1.424 +  fix i from *[of i] `x \<notin> S` fg show "f i = g i"
   1.425 +    by (auto split: split_if_asm simp: PiE_def extensional_def)
   1.426  qed
   1.427  
   1.428 -lemma finite_extensional_funcset:
   1.429 -  assumes "finite S" "finite T"
   1.430 -  shows "finite (extensional_funcset S T)"
   1.431 -proof -
   1.432 -  from card_extensional_funcset[OF assms(1), of T] assms(2)
   1.433 -  have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
   1.434 -    by auto
   1.435 -  from this show ?thesis
   1.436 -  proof
   1.437 -    assume "card (extensional_funcset S T) \<noteq> 0"
   1.438 -    from this show ?thesis
   1.439 -      by (auto intro: card_ge_0_finite)
   1.440 -  next
   1.441 -    assume "S \<noteq> {} \<and> T = {}"
   1.442 -    from this show ?thesis
   1.443 -      by (auto simp add: extensional_funcset_empty_range)
   1.444 -  qed
   1.445 +lemma card_PiE:
   1.446 +  "finite S \<Longrightarrow> card (PIE i : S. T i) = (\<Prod> i\<in>S. card (T i))"
   1.447 +proof (induct rule: finite_induct)
   1.448 +  case empty then show ?case by auto
   1.449 +next
   1.450 +  case (insert x S) then show ?case
   1.451 +    by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product)
   1.452  qed
   1.453  
   1.454  end
     2.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 16:14:18 2012 +0100
     2.2 +++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 12:29:02 2012 +0100
     2.3 @@ -1284,17 +1284,16 @@
     2.4    assumes "finite J"
     2.5    shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
     2.6  proof (rule measurable_PiM)
     2.7 -  show "(\<lambda>m. compose J m f)
     2.8 -    \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow>
     2.9 -      (J \<rightarrow> space M) \<inter> extensional J"
    2.10 +  show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
    2.11    proof safe
    2.12      fix x and i
    2.13      assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
    2.14      with inj show  "compose J x f i \<in> space M"
    2.15        by (auto simp: space_PiM compose_def)
    2.16    next
    2.17 -    fix x assume "x \<in> space (PiM (f ` J) (\<lambda>_. M))"
    2.18 -    show "(compose J x f) \<in> extensional J" by (rule compose_extensional)
    2.19 +    fix x i assume "i \<notin> J"
    2.20 +    with compose_extensional[of J x f]
    2.21 +    show "compose J x f i = undefined" by (auto simp: extensional_def)
    2.22    qed
    2.23  next
    2.24    fix S X
    2.25 @@ -1303,7 +1302,7 @@
    2.26    have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
    2.27      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)))"
    2.28      using assms inv S sets_into_space[OF P]
    2.29 -    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def intro: imageI)
    2.30 +    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
    2.31    also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
    2.32    proof
    2.33      from S show "f ` S \<subseteq> f `  J" by auto
    2.34 @@ -1379,7 +1378,7 @@
    2.35    assumes "\<And>i. space (M i) = UNIV"
    2.36    shows "inj_on fm (space (Pi\<^isub>M J M))"
    2.37    using assms
    2.38 -  apply (auto simp: fm_def space_PiM)
    2.39 +  apply (auto simp: fm_def space_PiM PiE_def)
    2.40    apply (rule comp_inj_on)
    2.41    apply (rule inj_on_compose_f')
    2.42    apply (rule finmap_of_inj_on_extensional_finite)
    2.43 @@ -1409,7 +1408,7 @@
    2.44      by (auto simp: mf_def extensional_def compose_def)
    2.45    moreover
    2.46    have "x \<in> extensional J" using assms sets_into_space
    2.47 -    by (force simp: space_PiM)
    2.48 +    by (force simp: space_PiM PiE_def)
    2.49    moreover
    2.50    { fix i assume "i \<in> J"
    2.51      hence "mf (fm x) i = x i"
    2.52 @@ -1472,13 +1471,13 @@
    2.53  
    2.54  lemma mapmeasure_PiF:
    2.55    assumes s1: "space M = space (Pi\<^isub>M J (\<lambda>_. N))"
    2.56 -  assumes s2: "sets M = (Pi\<^isub>M J (\<lambda>_. N))"
    2.57 +  assumes s2: "sets M = sets (Pi\<^isub>M J (\<lambda>_. N))"
    2.58    assumes "space N = UNIV"
    2.59    assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
    2.60    shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
    2.61    using assms
    2.62    by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
    2.63 -    fm_measurable space_PiM)
    2.64 +    fm_measurable space_PiM PiE_def)
    2.65  
    2.66  lemma mapmeasure_PiM:
    2.67    fixes N::"'c measure"
     3.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
     3.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
     3.3 @@ -11,46 +11,7 @@
     3.4  lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
     3.5    by auto
     3.6  
     3.7 -abbreviation
     3.8 -  "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
     3.9 -
    3.10 -syntax
    3.11 -  "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
    3.12 -
    3.13 -syntax (xsymbols)
    3.14 -  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
    3.15 -
    3.16 -syntax (HTML output)
    3.17 -  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
    3.18 -
    3.19 -translations
    3.20 -  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
    3.21 -
    3.22 -abbreviation
    3.23 -  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
    3.24 -    (infixr "->\<^isub>E" 60) where
    3.25 -  "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
    3.26 -
    3.27 -notation (xsymbols)
    3.28 -  funcset_extensional  (infixr "\<rightarrow>\<^isub>E" 60)
    3.29 -
    3.30 -lemma extensional_insert[intro, simp]:
    3.31 -  assumes "a \<in> extensional (insert i I)"
    3.32 -  shows "a(i := b) \<in> extensional (insert i I)"
    3.33 -  using assms unfolding extensional_def by auto
    3.34 -
    3.35 -lemma extensional_Int[simp]:
    3.36 -  "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
    3.37 -  unfolding extensional_def by auto
    3.38 -
    3.39 -lemma extensional_UNIV[simp]: "extensional UNIV = UNIV"
    3.40 -  by (auto simp: extensional_def)
    3.41 -
    3.42 -lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
    3.43 -  unfolding restrict_def extensional_def by auto
    3.44 -
    3.45 -lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
    3.46 -  unfolding restrict_def by (simp add: fun_eq_iff)
    3.47 +subsubsection {* Merge two extensional functions *}
    3.48  
    3.49  definition
    3.50    "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    3.51 @@ -84,9 +45,6 @@
    3.52  lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
    3.53    by (auto simp: extensional_def)
    3.54  
    3.55 -lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
    3.56 -  by (auto simp: restrict_def Pi_def)
    3.57 -
    3.58  lemma restrict_merge[simp]:
    3.59    "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    3.60    "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    3.61 @@ -97,9 +55,26 @@
    3.62  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)"
    3.63    unfolding merge_def by auto
    3.64  
    3.65 +lemma PiE_cancel_merge[simp]:
    3.66 +  "I \<inter> J = {} \<Longrightarrow>
    3.67 +    merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
    3.68 +  by (auto simp: PiE_def restrict_Pi_cancel)
    3.69 +
    3.70 +lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
    3.71 +  unfolding merge_def by (auto simp: fun_eq_iff)
    3.72 +
    3.73  lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
    3.74    unfolding merge_def extensional_def by auto
    3.75  
    3.76 +lemma merge_restrict[simp]:
    3.77 +  "merge I J (restrict x I, y) = merge I J (x, y)"
    3.78 +  "merge I J (x, restrict y J) = merge I J (x, y)"
    3.79 +  unfolding merge_def by auto
    3.80 +
    3.81 +lemma merge_x_x_eq_restrict[simp]:
    3.82 +  "merge I J (x, x) = restrict x (I \<union> J)"
    3.83 +  unfolding merge_def by auto
    3.84 +
    3.85  lemma injective_vimage_restrict:
    3.86    assumes J: "J \<subseteq> I"
    3.87    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> {}"
    3.88 @@ -113,195 +88,22 @@
    3.89    proof cases
    3.90      assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
    3.91      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)"
    3.92 -      using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
    3.93 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
    3.94 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    3.95      then show "x \<in> A \<longleftrightarrow> x \<in> B"
    3.96 -      using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
    3.97 -  next
    3.98 -    assume "x \<notin> (\<Pi>\<^isub>E i\<in>J. S i)" with sets show "x \<in> A \<longleftrightarrow> x \<in> B" by auto
    3.99 -  qed
   3.100 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
   3.101 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
   3.102 +  qed (insert sets, auto)
   3.103  qed
   3.104  
   3.105 -lemma extensional_insert_undefined[intro, simp]:
   3.106 -  assumes "a \<in> extensional (insert i I)"
   3.107 -  shows "a(i := undefined) \<in> extensional I"
   3.108 -  using assms unfolding extensional_def by auto
   3.109 -
   3.110 -lemma extensional_insert_cancel[intro, simp]:
   3.111 -  assumes "a \<in> extensional I"
   3.112 -  shows "a \<in> extensional (insert i I)"
   3.113 -  using assms unfolding extensional_def by auto
   3.114 -
   3.115 -lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
   3.116 -  unfolding merge_def by (auto simp: fun_eq_iff)
   3.117 -
   3.118 -lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
   3.119 -  by auto
   3.120 -
   3.121 -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)"
   3.122 -  by auto
   3.123 -
   3.124 -lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
   3.125 -  by (auto simp: Pi_def)
   3.126 -
   3.127 -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"
   3.128 -  by (auto simp: Pi_def)
   3.129 -
   3.130 -lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
   3.131 -  by (auto simp: Pi_def)
   3.132 -
   3.133 -lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
   3.134 -  by (auto simp: Pi_def)
   3.135 -
   3.136  lemma restrict_vimage:
   3.137 -  assumes "I \<inter> J = {}"
   3.138 -  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))"
   3.139 -  using assms by (auto simp: restrict_Pi_cancel)
   3.140 +  "I \<inter> J = {} \<Longrightarrow>
   3.141 +    (\<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))"
   3.142 +  by (auto simp: restrict_Pi_cancel PiE_def)
   3.143  
   3.144  lemma merge_vimage:
   3.145 -  assumes "I \<inter> J = {}"
   3.146 -  shows "merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   3.147 -  using assms by (auto simp: restrict_Pi_cancel)
   3.148 -
   3.149 -lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
   3.150 -  by (auto simp: restrict_def)
   3.151 -
   3.152 -lemma merge_restrict[simp]:
   3.153 -  "merge I J (restrict x I, y) = merge I J (x, y)"
   3.154 -  "merge I J (x, restrict y J) = merge I J (x, y)"
   3.155 -  unfolding merge_def by auto
   3.156 -
   3.157 -lemma merge_x_x_eq_restrict[simp]:
   3.158 -  "merge I J (x, x) = restrict x (I \<union> J)"
   3.159 -  unfolding merge_def by auto
   3.160 -
   3.161 -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"
   3.162 -  apply auto
   3.163 -  apply (drule_tac x=x in Pi_mem)
   3.164 -  apply (simp_all split: split_if_asm)
   3.165 -  apply (drule_tac x=i in Pi_mem)
   3.166 -  apply (auto dest!: Pi_mem)
   3.167 -  done
   3.168 -
   3.169 -lemma Pi_UN:
   3.170 -  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
   3.171 -  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
   3.172 -  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
   3.173 -proof (intro set_eqI iffI)
   3.174 -  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
   3.175 -  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
   3.176 -  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
   3.177 -  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
   3.178 -    using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
   3.179 -  have "f \<in> Pi I (A k)"
   3.180 -  proof (intro Pi_I)
   3.181 -    fix i assume "i \<in> I"
   3.182 -    from mono[OF this, of "n i" k] k[OF this] n[OF this]
   3.183 -    show "f i \<in> A k i" by auto
   3.184 -  qed
   3.185 -  then show "f \<in> (\<Union>n. Pi I (A n))" by auto
   3.186 -qed auto
   3.187 -
   3.188 -lemma PiE_cong:
   3.189 -  assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
   3.190 -  shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
   3.191 -  using assms by (auto intro!: Pi_cong)
   3.192 -
   3.193 -lemma restrict_upd[simp]:
   3.194 -  "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
   3.195 -  by (auto simp: fun_eq_iff)
   3.196 -
   3.197 -lemma Pi_eq_subset:
   3.198 -  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   3.199 -  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
   3.200 -  shows "F i \<subseteq> F' i"
   3.201 -proof
   3.202 -  fix x assume "x \<in> F i"
   3.203 -  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
   3.204 -  from choice[OF this] guess f .. note f = this
   3.205 -  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   3.206 -  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
   3.207 -  then show "x \<in> F' i" using f `i \<in> I` by auto
   3.208 -qed
   3.209 -
   3.210 -lemma Pi_eq_iff_not_empty:
   3.211 -  assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
   3.212 -  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
   3.213 -proof (intro iffI ballI)
   3.214 -  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
   3.215 -  show "F i = F' i"
   3.216 -    using Pi_eq_subset[of I F F', OF ne eq i]
   3.217 -    using Pi_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
   3.218 -    by auto
   3.219 -qed auto
   3.220 -
   3.221 -lemma Pi_eq_empty_iff:
   3.222 -  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
   3.223 -proof
   3.224 -  assume "Pi\<^isub>E I F = {}"
   3.225 -  show "\<exists>i\<in>I. F i = {}"
   3.226 -  proof (rule ccontr)
   3.227 -    assume "\<not> ?thesis"
   3.228 -    then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
   3.229 -    from choice[OF this] guess f ..
   3.230 -    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def)
   3.231 -    with `Pi\<^isub>E I F = {}` show False by auto
   3.232 -  qed
   3.233 -qed auto
   3.234 -
   3.235 -lemma Pi_eq_iff:
   3.236 -  "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 = {}))"
   3.237 -proof (intro iffI disjCI)
   3.238 -  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   3.239 -  assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   3.240 -  then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   3.241 -    using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   3.242 -  with Pi_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
   3.243 -next
   3.244 -  assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   3.245 -  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   3.246 -    using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
   3.247 -qed
   3.248 -
   3.249 -lemma funset_eq_UN_fun_upd_I:
   3.250 -  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
   3.251 -  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
   3.252 -  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
   3.253 -  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
   3.254 -proof safe
   3.255 -  fix f assume f: "f \<in> F (insert a A)"
   3.256 -  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
   3.257 -  proof (rule UN_I[of "f(a := d)"])
   3.258 -    show "f(a := d) \<in> F A" using *[OF f] .
   3.259 -    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
   3.260 -    proof (rule image_eqI[of _ _ "f a"])
   3.261 -      show "f a \<in> G (f(a := d))" using **[OF f] .
   3.262 -    qed simp
   3.263 -  qed
   3.264 -next
   3.265 -  fix f x assume "f \<in> F A" "x \<in> G f"
   3.266 -  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
   3.267 -qed
   3.268 -
   3.269 -lemma extensional_funcset_insert_eq[simp]:
   3.270 -  assumes "a \<notin> A"
   3.271 -  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)"
   3.272 -  apply (rule funset_eq_UN_fun_upd_I)
   3.273 -  using assms
   3.274 -  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
   3.275 -
   3.276 -lemma finite_extensional_funcset[simp, intro]:
   3.277 -  assumes "finite A" "finite B"
   3.278 -  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
   3.279 -  using assms by induct auto
   3.280 -
   3.281 -lemma finite_PiE[simp, intro]:
   3.282 -  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
   3.283 -  shows "finite (Pi\<^isub>E A B)"
   3.284 -proof -
   3.285 -  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
   3.286 -  show ?thesis
   3.287 -    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
   3.288 -qed
   3.289 +  "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
   3.290 +  by (auto simp: restrict_Pi_cancel PiE_def)
   3.291  
   3.292  section "Finite product spaces"
   3.293  
   3.294 @@ -312,7 +114,7 @@
   3.295  
   3.296  lemma prod_emb_iff: 
   3.297    "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))"
   3.298 -  unfolding prod_emb_def by auto
   3.299 +  unfolding prod_emb_def PiE_def by auto
   3.300  
   3.301  lemma
   3.302    shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
   3.303 @@ -325,24 +127,25 @@
   3.304  
   3.305  lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
   3.306      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))"
   3.307 -  by (force simp: prod_emb_def Pi_iff split_if_mem2)
   3.308 +  by (force simp: prod_emb_def PiE_iff split_if_mem2)
   3.309  
   3.310 -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"
   3.311 -  by (auto simp: prod_emb_def Pi_iff)
   3.312 +lemma prod_emb_PiE_same_index[simp]:
   3.313 +    "(\<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"
   3.314 +  by (auto simp: prod_emb_def PiE_iff)
   3.315  
   3.316  lemma prod_emb_trans[simp]:
   3.317    "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"
   3.318 -  by (auto simp add: Int_absorb1 prod_emb_def)
   3.319 +  by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
   3.320  
   3.321  lemma prod_emb_Pi:
   3.322    assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
   3.323    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))"
   3.324    using assms space_closed
   3.325 -  by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
   3.326 +  by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
   3.327  
   3.328  lemma prod_emb_id:
   3.329    "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
   3.330 -  by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
   3.331 +  by (auto simp: prod_emb_def subset_eq extensional_restrict)
   3.332  
   3.333  lemma prod_emb_mono:
   3.334    "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
   3.335 @@ -392,9 +195,9 @@
   3.336      by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
   3.337  next
   3.338    fix A assume "A \<in> ?R"
   3.339 -  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
   3.340 +  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
   3.341    then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
   3.342 -    using sets_into_space by (force simp: prod_emb_def Pi_iff)
   3.343 +    by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
   3.344    from X I show "A \<in> ?L" unfolding A
   3.345      by (auto simp: prod_algebra_def)
   3.346  qed
   3.347 @@ -402,7 +205,7 @@
   3.348  lemma prod_algebraI:
   3.349    "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
   3.350      \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
   3.351 -  by (auto simp: prod_algebra_def Pi_iff)
   3.352 +  by (auto simp: prod_algebra_def)
   3.353  
   3.354  lemma prod_algebraI_finite:
   3.355    "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
   3.356 @@ -412,7 +215,7 @@
   3.357  proof (safe intro!: Int_stableI)
   3.358    fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   3.359    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))"
   3.360 -    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
   3.361 +    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
   3.362  qed
   3.363  
   3.364  lemma prod_algebraE:
   3.365 @@ -501,7 +304,7 @@
   3.366    assume "I \<noteq> {}"
   3.367    then obtain i where "i \<in> I" by auto
   3.368    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))"
   3.369 -    by (auto simp: prod_emb_def Pi_iff)
   3.370 +    by (auto simp: prod_emb_def)
   3.371    also have "\<dots> \<in> prod_algebra I M"
   3.372      using `i \<in> I` by (intro prod_algebraI) auto
   3.373    finally show ?thesis .
   3.374 @@ -529,8 +332,7 @@
   3.375    next
   3.376      assume "I \<noteq> {}"
   3.377      with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^isub>E i\<in>I. space (M i)). f j \<in> X j})"
   3.378 -      using sets_into_space[OF X(5)]
   3.379 -      by (auto simp: prod_emb_PiE[OF _ sets_into_space] Pi_iff split: split_if_asm) blast
   3.380 +      by (auto simp: prod_emb_def)
   3.381      also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
   3.382        using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
   3.383      finally show "A \<in> sigma_sets ?\<Omega> ?R" .
   3.384 @@ -540,11 +342,7 @@
   3.385    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)" 
   3.386      by auto
   3.387    then have "A = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. B)"
   3.388 -    using sets_into_space[OF A(3)]
   3.389 -    apply (subst prod_emb_PiE)
   3.390 -    apply (auto simp: Pi_iff split: split_if_asm)
   3.391 -    apply blast
   3.392 -    done
   3.393 +     by (auto simp: prod_emb_def)
   3.394    also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
   3.395      using A by (intro sigma_sets.Basic prod_algebraI) auto
   3.396    finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
   3.397 @@ -585,9 +383,8 @@
   3.398  proof (rule measurable_sigma_sets)
   3.399    fix A assume "A \<in> prod_algebra I M"
   3.400    from prod_algebraE[OF this] guess J X . note X = this
   3.401 -  have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
   3.402 -    using sets_into_space[OF X(5)] X(2-) space unfolding X(1)
   3.403 -    by (subst prod_emb_PiE) (auto simp: Pi_iff split: split_if_asm)
   3.404 +  then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
   3.405 +    using space by (auto simp: prod_emb_def del: PiE_I)
   3.406    also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
   3.407    finally show "f -` A \<inter> space N \<in> sets N" .
   3.408  qed
   3.409 @@ -654,7 +451,7 @@
   3.410    assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   3.411    shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
   3.412    using fg[THEN measurable_space]
   3.413 -  by (auto intro!: measurable_PiM_single' simp add: space_PiM Pi_iff split: nat.split)
   3.414 +  by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
   3.415  
   3.416  lemma measurable_add_dim[measurable]:
   3.417    "(\<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)"
   3.418 @@ -668,7 +465,7 @@
   3.419      using A j
   3.420      by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   3.421    finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
   3.422 -qed (auto simp: space_pair_measure space_PiM)
   3.423 +qed (auto simp: space_pair_measure space_PiM PiE_def)
   3.424  
   3.425  lemma measurable_component_update:
   3.426    "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)"
   3.427 @@ -686,7 +483,7 @@
   3.428      using A
   3.429      by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   3.430    finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
   3.431 -qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
   3.432 +qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
   3.433  
   3.434  lemma measurable_restrict[measurable (raw)]:
   3.435    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
   3.436 @@ -697,7 +494,7 @@
   3.437      by auto
   3.438    then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
   3.439      using A X by (auto intro!: measurable_sets)
   3.440 -qed (insert X, auto dest: measurable_space)
   3.441 +qed (insert X, auto simp add: PiE_def dest: measurable_space)
   3.442  
   3.443  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)"
   3.444    by (intro measurable_restrict measurable_component_singleton) auto
   3.445 @@ -762,13 +559,12 @@
   3.446    next
   3.447      fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
   3.448    next
   3.449 -    fix A assume "A \<in> (\<Union>i. ?F i)" then show "A \<in> space (PiM I M)"
   3.450 -      using `\<And>i. range (F i) \<subseteq> sets (M i)` sets_into_space
   3.451 -      by auto blast
   3.452 +    fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
   3.453 +      by (auto simp: PiE_def dest!: sets_into_space)
   3.454    next
   3.455      fix f assume "f \<in> space (PiM I M)"
   3.456      with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
   3.457 -    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def)
   3.458 +    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
   3.459    next
   3.460      fix i show "?F i \<subseteq> ?F (Suc i)"
   3.461        using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
   3.462 @@ -826,13 +622,13 @@
   3.463        by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
   3.464      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))"
   3.465        using J E[rule_format, THEN sets_into_space]
   3.466 -      by (force simp: space_pair_measure space_PiM Pi_iff prod_emb_iff split: split_if_asm)
   3.467 +      by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
   3.468      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))) =
   3.469        emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
   3.470        using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
   3.471      also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
   3.472        using J E[rule_format, THEN sets_into_space]
   3.473 -      by (auto simp: prod_emb_iff Pi_iff split: split_if_asm) blast+
   3.474 +      by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
   3.475      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)) =
   3.476        (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
   3.477        using E by (subst insert) (auto intro!: setprod_cong)
   3.478 @@ -844,7 +640,7 @@
   3.479      finally show "?\<mu> ?p = \<dots>" .
   3.480  
   3.481      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))"
   3.482 -      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff)
   3.483 +      using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
   3.484    next
   3.485      show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
   3.486        using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
   3.487 @@ -961,7 +757,7 @@
   3.488        using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
   3.489      also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
   3.490        using `finite J` `finite I` F unfolding X
   3.491 -      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
   3.492 +      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times)
   3.493      also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
   3.494        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
   3.495      also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)"
   3.496 @@ -1034,7 +830,7 @@
   3.497      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)"
   3.498        using x
   3.499        by (auto intro!: positive_integral_cong arg_cong[where f=f]
   3.500 -               simp add: space_PiM extensional_def)
   3.501 +               simp add: space_PiM extensional_def PiE_def)
   3.502    qed
   3.503  qed
   3.504  
   3.505 @@ -1085,7 +881,7 @@
   3.506    then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
   3.507      by simp
   3.508    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)" 
   3.509 -    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
   3.510 +    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
   3.511    also have "\<dots> = emeasure ?D A"
   3.512      using A by (simp add: product_positive_integral_singleton emeasure_distr)
   3.513    finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
   3.514 @@ -1160,7 +956,7 @@
   3.515        using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
   3.516        unfolding comp_def .
   3.517      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)"
   3.518 -      by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
   3.519 +      by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def PiE_def)
   3.520    qed
   3.521    finally show ?thesis .
   3.522  qed
   3.523 @@ -1233,7 +1029,7 @@
   3.524  proof
   3.525    let ?P = "sigma (space (Pi\<^isub>M I M)) P"
   3.526    have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
   3.527 -    using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
   3.528 +    using E_closed by (auto simp: space_PiM P_def subset_eq)
   3.529    then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
   3.530      by (simp add: space_PiM)
   3.531    have "sets (PiM I M) =
   3.532 @@ -1281,7 +1077,7 @@
   3.533    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"
   3.534      by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
   3.535    have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>M I M))"
   3.536 -    using E_closed by (auto simp: space_PiM P_def Pi_iff subset_eq)
   3.537 +    using E_closed by (auto simp: space_PiM P_def subset_eq)
   3.538    then have space_P: "space ?P = (\<Pi>\<^isub>E i\<in>I. space (M i))"
   3.539      by (simp add: space_PiM)
   3.540    have "sets (PiM I M) =
   3.541 @@ -1293,18 +1089,17 @@
   3.542      have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
   3.543      proof (subst measurable_iff_measure_of)
   3.544        show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
   3.545 -      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)"
   3.546 -        by (auto simp: Pi_iff)
   3.547 +      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
   3.548        show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
   3.549        proof
   3.550          fix A assume A: "A \<in> E i"
   3.551          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))"
   3.552 -          using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
   3.553 +          using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
   3.554          also have "\<dots> = (\<Pi>\<^isub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
   3.555            by (intro PiE_cong) (simp add: S_union)
   3.556          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))"
   3.557            using T
   3.558 -          apply (auto simp: Pi_iff bchoice_iff)
   3.559 +          apply (auto simp: PiE_iff bchoice_iff)
   3.560            apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
   3.561            apply (auto simp: bij_betw_def)
   3.562            done
   3.563 @@ -1352,7 +1147,7 @@
   3.564      using A B by (subst B.emeasure_PiM) (auto split: bool.split)
   3.565    also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
   3.566      using A[THEN sets_into_space] B[THEN sets_into_space]
   3.567 -    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
   3.568 +    by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
   3.569    finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
   3.570      using A B
   3.571        measurable_component_singleton[of True UNIV "bool_case M1 M2"]
     4.1 --- a/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 16:14:18 2012 +0100
     4.2 +++ b/src/HOL/Probability/Independent_Family.thy	Mon Nov 19 12:29:02 2012 +0100
     4.3 @@ -867,7 +867,7 @@
     4.4        then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
     4.5          by (simp add: emeasure_distr X)
     4.6        also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
     4.7 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
     4.8 +        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
     4.9        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))"
    4.10          using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J]
    4.11          by (auto simp: emeasure_eq_measure setprod_ereal)
    4.12 @@ -898,7 +898,7 @@
    4.13          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
    4.14        let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)"
    4.15        from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
    4.16 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm)
    4.17 +        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
    4.18        then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
    4.19          by simp
    4.20        also have "\<dots> = emeasure ?D ?E"
     5.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
     5.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
     5.3 @@ -234,11 +234,9 @@
     5.4                using w'(1) J(3)[of "Suc k"]
     5.5                by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
     5.6              show ?thesis
     5.7 -              apply (rule exI[of _ ?w])
     5.8                using w' J_mono[of k "Suc k"] wk unfolding *
     5.9 -              apply (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM)
    5.10 -              apply (force simp: extensional_def)
    5.11 -              done
    5.12 +              by (intro exI[of _ ?w])
    5.13 +                 (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
    5.14            qed
    5.15            then have "?P k (w k) (w (Suc k))"
    5.16              unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
    5.17 @@ -295,8 +293,8 @@
    5.18          using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
    5.19  
    5.20        { fix n
    5.21 -        have "restrict w' (J n) = w n" using w(1)
    5.22 -          by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def space_PiM)
    5.23 +        have "restrict w' (J n) = w n" using w(1)[of n]
    5.24 +          by (auto simp add: fun_eq_iff space_PiM)
    5.25          with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
    5.26          then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
    5.27        then have "w' \<in> (\<Inter>i. A i)" by auto
    5.28 @@ -391,7 +389,7 @@
    5.29  lemma sets_Collect_single':
    5.30    "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)"
    5.31    using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
    5.32 -  by (simp add: space_PiM Pi_iff cong: conj_cong)
    5.33 +  by (simp add: space_PiM PiE_iff cong: conj_cong)
    5.34  
    5.35  lemma (in finite_product_prob_space) finite_measure_PiM_emb:
    5.36    "(\<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))"
    5.37 @@ -462,7 +460,7 @@
    5.38    "(\<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)"
    5.39  proof (rule measurable_PiM_single)
    5.40    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)"
    5.41 -    by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
    5.42 +    by (auto simp: space_pair_measure space_PiM PiE_iff split: split_comb_seq)
    5.43    fix j :: nat and A assume A: "A \<in> sets M"
    5.44    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} =
    5.45      (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)
    5.46 @@ -550,7 +548,7 @@
    5.47    with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
    5.48      (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
    5.49      (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    5.50 -   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib Pi_iff
    5.51 +   by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
    5.52                 split: split_comb_seq split_comb_seq_asm)
    5.53    then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^isub>M S) (?E \<times> ?F)"
    5.54      by (subst emeasure_distr[OF measurable_comb_seq])
    5.55 @@ -581,7 +579,7 @@
    5.56      using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
    5.57    with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
    5.58      (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    5.59 -   by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
    5.60 +   by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
    5.61        split: nat.split nat.split_asm)
    5.62    then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
    5.63      by (subst emeasure_distr)
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
     6.3 @@ -935,7 +935,7 @@
     6.4    fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
     6.5    then obtain x where  "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
     6.6    then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
     6.7 -    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
     6.8 +    using DIM_positive by (auto simp add: set_eq_iff e2p_def
     6.9        euclidean_eq[where 'a='a] eucl_less[where 'a='a])
    6.10    then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
    6.11  qed (auto simp: e2p_def)
    6.12 @@ -953,7 +953,7 @@
    6.13    let ?A = "{w \<in> space ?P. (p2e w :: 'a) $$ i \<le> x}"
    6.14    assume "i < DIM('a)"
    6.15    then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
    6.16 -    using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
    6.17 +    using DIM_positive by (auto simp: space_PiM p2e_def PiE_def split: split_if_asm)
    6.18    then show "?A \<in> sets ?P"
    6.19      by auto
    6.20  qed
    6.21 @@ -966,7 +966,7 @@
    6.22    let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
    6.23    fix a b :: 'a
    6.24    have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
    6.25 -    by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
    6.26 +    by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff)
    6.27    have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
    6.28    proof cases
    6.29      assume "{a..b} \<noteq> {}"
     7.1 --- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:14:18 2012 +0100
     7.2 +++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
     7.3 @@ -44,7 +44,7 @@
     7.4    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))"
     7.5      using E by (simp add: K.measure_times)
     7.6    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))"
     7.7 -    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
     7.8 +    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
     7.9    finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
    7.10      using X `J \<subseteq> K` apply (subst emeasure_distr)
    7.11      by (auto intro!: measurable_restrict_subset simp: space_PiM)
    7.12 @@ -93,15 +93,10 @@
    7.13    shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
    7.14  proof -
    7.15    have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    7.16 -  proof safe
    7.17 -    fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
    7.18 -    hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
    7.19 -    also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
    7.20 -    finally show "x j \<in> space (M j)" .
    7.21 -  qed
    7.22 +    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
    7.23    hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
    7.24      emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
    7.25 -    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
    7.26 +    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
    7.27    also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
    7.28    proof (rule emeasure_extend_measure_Pair[OF limP_def])
    7.29      show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
    7.30 @@ -169,7 +164,7 @@
    7.31      from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
    7.32    qed
    7.33    from bchoice[OF this]
    7.34 -  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
    7.35 +  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
    7.36    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))"
    7.37      using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
    7.38  qed fact
    7.39 @@ -293,7 +288,7 @@
    7.40    have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
    7.41    have [simp]: "(K - J) \<inter> K = K - J" by auto
    7.42    from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
    7.43 -    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
    7.44 +    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
    7.45         auto
    7.46  qed
    7.47  
     8.1 --- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 16:14:18 2012 +0100
     8.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 12:29:02 2012 +0100
     8.3 @@ -428,7 +428,7 @@
     8.4            also have "\<dots> = P (J i) (B i) - P' i (K' i)"
     8.5              unfolding K_def P'_def
     8.6              by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric]
     8.7 -              compact_imp_closed[OF `compact (K' _)`] space_PiM)
     8.8 +              compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def)
     8.9            also have "\<dots> \<le> ereal (2 powr - real i) * ?a" using K'(1)[of i] .
    8.10            finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" .
    8.11          qed
    8.12 @@ -580,7 +580,7 @@
    8.13          ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"
    8.14            unfolding K_def by (auto simp: proj_space space_PiM)
    8.15          hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def
    8.16 -          using J by (auto simp: prod_emb_def extensional_def)
    8.17 +          using J by (auto simp: prod_emb_def PiE_def extensional_def)
    8.18          also have "\<dots> \<subseteq> Z n" using Z' by simp
    8.19          finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .
    8.20        } note in_Z = this
    8.21 @@ -602,7 +602,7 @@
    8.22        using assms by (auto simp: f_def)
    8.23    next
    8.24      fix J and X::"'i \<Rightarrow> 'a set"
    8.25 -    show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow ((I \<rightarrow> space borel) \<inter> extensional I)"
    8.26 +    show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow (I \<rightarrow>\<^isub>E space borel)"
    8.27        by (auto simp: prod_emb_def)
    8.28      assume JX: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> J \<rightarrow> sets borel"
    8.29      hence "emb I J (Pi\<^isub>E J X) \<in> generator" using assms
    8.30 @@ -645,11 +645,11 @@
    8.31      interpret prob_space "P {i}" using proj_prob_space by simp
    8.32      have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
    8.33        by (auto simp: prod_emb_def space_PiM)
    8.34 -    moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
    8.35 +    moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM PiE_def)
    8.36      ultimately show ?thesis using `i \<in> I`
    8.37        apply (subst R)
    8.38        apply (subst emeasure_limB_emb_not_empty)
    8.39 -      apply (auto simp: limP_finite emeasure_space_1)
    8.40 +      apply (auto simp: limP_finite emeasure_space_1 PiE_def)
    8.41        done
    8.42    qed
    8.43  qed
     9.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Mon Nov 19 16:14:18 2012 +0100
     9.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Mon Nov 19 12:29:02 2012 +0100
     9.3 @@ -14,21 +14,7 @@
     9.4    assumes "finite S"
     9.5    assumes "\<forall>x \<in> S. finite (T x)" 
     9.6    shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
     9.7 -proof -
     9.8 -  note `finite S`
     9.9 -  moreover
    9.10 -  have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
    9.11 -  moreover
    9.12 -  from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
    9.13 -  moreover
    9.14 -  have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
    9.15 -  moreover  
    9.16 -  ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
    9.17 -    by (auto, subst card_UN_disjoint) auto
    9.18 -  also have "... = (SUM x:S. card (T x))"
    9.19 -    by (subst card_image) (auto intro: inj_onI)
    9.20 -  finally show ?thesis by auto
    9.21 -qed
    9.22 +  using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
    9.23  
    9.24  lemma card_extensional_funcset_inj_on:
    9.25    assumes "finite S" "finite T" "card S \<le> card T"
    9.26 @@ -36,13 +22,13 @@
    9.27  using assms
    9.28  proof (induct S arbitrary: T rule: finite_induct)
    9.29    case empty
    9.30 -  from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
    9.31 +  from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
    9.32  next
    9.33    case (insert x S)
    9.34    { fix x
    9.35      from `finite T` have "finite (T - {x})" by auto
    9.36      from `finite S` this have "finite (extensional_funcset S (T - {x}))"
    9.37 -      by (rule finite_extensional_funcset)
    9.38 +      by (rule finite_PiE)
    9.39      moreover
    9.40      have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
    9.41      ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
    9.42 @@ -75,10 +61,10 @@
    9.43  proof -
    9.44    have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
    9.45    from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
    9.46 -    by (auto intro!: finite_extensional_funcset)
    9.47 +    by (auto intro!: finite_PiE)
    9.48    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 
    9.49    from assms this finite subset show ?thesis
    9.50 -    by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
    9.51 +    by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
    9.52  qed
    9.53  
    9.54  lemma setprod_upto_nat_unfold:
    9.55 @@ -93,9 +79,9 @@
    9.56  proof -
    9.57    from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
    9.58    from assms show ?thesis
    9.59 -    using card_extensional_funcset[OF `finite S`, of T]
    9.60 +    using card_PiE[OF `finite S`, of "\<lambda>i. T"] `finite S`
    9.61        card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
    9.62 -    by (simp add: fact_div_fact setprod_upto_nat_unfold)
    9.63 +    by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
    9.64  qed
    9.65  
    9.66  end