src/HOL/Probability/Fin_Map.thy
 changeset 50123 69b35a75caf3 parent 50100 9af8721ecd20 child 50124 4161c834c2fd
```     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 16:14:18 2012 +0100
1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 12:29:02 2012 +0100
1.3 @@ -1284,17 +1284,16 @@
1.4    assumes "finite J"
1.5    shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
1.6  proof (rule measurable_PiM)
1.7 -  show "(\<lambda>m. compose J m f)
1.8 -    \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow>
1.9 -      (J \<rightarrow> space M) \<inter> extensional J"
1.10 +  show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
1.11    proof safe
1.12      fix x and i
1.13      assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
1.14      with inj show  "compose J x f i \<in> space M"
1.15        by (auto simp: space_PiM compose_def)
1.16    next
1.17 -    fix x assume "x \<in> space (PiM (f ` J) (\<lambda>_. M))"
1.18 -    show "(compose J x f) \<in> extensional J" by (rule compose_extensional)
1.19 +    fix x i assume "i \<notin> J"
1.20 +    with compose_extensional[of J x f]
1.21 +    show "compose J x f i = undefined" by (auto simp: extensional_def)
1.22    qed
1.23  next
1.24    fix S X
1.25 @@ -1303,7 +1302,7 @@
1.26    have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
1.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)))"
1.28      using assms inv S sets_into_space[OF P]
1.29 -    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def intro: imageI)
1.30 +    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
1.31    also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
1.32    proof
1.33      from S show "f ` S \<subseteq> f `  J" by auto
1.34 @@ -1379,7 +1378,7 @@
1.35    assumes "\<And>i. space (M i) = UNIV"
1.36    shows "inj_on fm (space (Pi\<^isub>M J M))"
1.37    using assms
1.38 -  apply (auto simp: fm_def space_PiM)
1.39 +  apply (auto simp: fm_def space_PiM PiE_def)
1.40    apply (rule comp_inj_on)
1.41    apply (rule inj_on_compose_f')
1.42    apply (rule finmap_of_inj_on_extensional_finite)
1.43 @@ -1409,7 +1408,7 @@
1.44      by (auto simp: mf_def extensional_def compose_def)
1.45    moreover
1.46    have "x \<in> extensional J" using assms sets_into_space
1.47 -    by (force simp: space_PiM)
1.48 +    by (force simp: space_PiM PiE_def)
1.49    moreover
1.50    { fix i assume "i \<in> J"
1.51      hence "mf (fm x) i = x i"
1.52 @@ -1472,13 +1471,13 @@
1.53
1.54  lemma mapmeasure_PiF:
1.55    assumes s1: "space M = space (Pi\<^isub>M J (\<lambda>_. N))"
1.56 -  assumes s2: "sets M = (Pi\<^isub>M J (\<lambda>_. N))"
1.57 +  assumes s2: "sets M = sets (Pi\<^isub>M J (\<lambda>_. N))"
1.58    assumes "space N = UNIV"
1.59    assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
1.60    shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
1.61    using assms
1.62    by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
1.63 -    fm_measurable space_PiM)
1.64 +    fm_measurable space_PiM PiE_def)
1.65
1.66  lemma mapmeasure_PiM:
1.67    fixes N::"'c measure"
```