author hoelzl Mon Nov 19 12:29:02 2012 +0100 (2012-11-19) changeset 50123 69b35a75caf3 parent 50122 7ae7efef5ad8 child 50124 4161c834c2fd
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
```     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.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
```