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"