tuned FinMap
authorhoelzl
Mon Nov 19 16:09:11 2012 +0100 (2012-11-19)
changeset 501244161c834c2fd
parent 50123 69b35a75caf3
child 50125 4319691be975
tuned FinMap
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 12:29:02 2012 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 16:09:11 2012 +0100
     1.3 @@ -80,8 +80,7 @@
     1.4    using assms
     1.5    apply (auto simp: finmap_eq_iff restrict_def) by metis
     1.6  
     1.7 -lemma
     1.8 -  finmap_of_inj_on_extensional_finite:
     1.9 +lemma finmap_of_inj_on_extensional_finite:
    1.10    assumes "finite K"
    1.11    assumes "S \<subseteq> extensional K"
    1.12    shows "inj_on (finmap_of K) S"
    1.13 @@ -125,14 +124,6 @@
    1.14  translations
    1.15    "PI' x:A. B" == "CONST Pi' A (%x. B)"
    1.16  
    1.17 -abbreviation
    1.18 -  finmapset :: "['a set, 'b set] => ('a \<Rightarrow>\<^isub>F 'b) set"
    1.19 -    (infixr "~>" 60) where
    1.20 -  "A ~> B \<equiv> Pi' A (%_. B)"
    1.21 -
    1.22 -notation (xsymbols)
    1.23 -  finmapset  (infixr "\<leadsto>" 60)
    1.24 -
    1.25  subsubsection{*Basic Properties of @{term Pi'}*}
    1.26  
    1.27  lemma Pi'_I[intro!]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B"
    1.28 @@ -141,9 +132,6 @@
    1.29  lemma Pi'_I'[simp]: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<longrightarrow> f x \<in> B x) \<Longrightarrow> f \<in> Pi' A B"
    1.30    by (simp add:Pi'_def)
    1.31  
    1.32 -lemma finmapsetI: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<leadsto> B"
    1.33 -  by (simp add: Pi_def)
    1.34 -
    1.35  lemma Pi'_mem: "f\<in> Pi' A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x"
    1.36    by (simp add: Pi'_def)
    1.37  
    1.38 @@ -158,12 +146,6 @@
    1.39    "domain f = domain g \<Longrightarrow> (\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi' A B \<longleftrightarrow> g \<in> Pi' A B"
    1.40    by (auto simp: Pi'_def)
    1.41  
    1.42 -lemma funcset_mem: "[|f \<in> A \<leadsto> B; x \<in> A|] ==> f x \<in> B"
    1.43 -  by (simp add: Pi'_def)
    1.44 -
    1.45 -lemma funcset_image: "f \<in> A \<leadsto> B ==> f ` A \<subseteq> B"
    1.46 -by auto
    1.47 -
    1.48  lemma Pi'_eq_empty[simp]:
    1.49    assumes "finite A" shows "(Pi' A B) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
    1.50    using assms
    1.51 @@ -554,8 +536,7 @@
    1.52    shows "open x"
    1.53    using finmap_topological_basis assms by (auto simp: topological_basis_def)
    1.54  
    1.55 -lemma
    1.56 -  open_imp_ex_UNION_of_enum:
    1.57 +lemma open_imp_ex_UNION_of_enum:
    1.58    fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
    1.59    assumes "open X" assumes "X \<noteq> {}"
    1.60    shows "\<exists>A::nat\<Rightarrow>'a set. \<exists>B::nat\<Rightarrow>('a \<Rightarrow> 'b set) . X = UNION UNIV (\<lambda>i. Pi' (A i) (B i)) \<and>
    1.61 @@ -588,8 +569,7 @@
    1.62    qed
    1.63  qed
    1.64  
    1.65 -lemma
    1.66 -  open_imp_ex_UNION:
    1.67 +lemma open_imp_ex_UNION:
    1.68    fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
    1.69    assumes "open X" assumes "X \<noteq> {}"
    1.70    shows "\<exists>A::nat\<Rightarrow>'a set. \<exists>B::nat\<Rightarrow>('a \<Rightarrow> 'b set) . X = UNION UNIV (\<lambda>i. Pi' (A i) (B i)) \<and>
    1.71 @@ -601,20 +581,18 @@
    1.72    apply (auto simp: open_enum_basis)
    1.73    done
    1.74  
    1.75 -lemma
    1.76 -  open_basisE:
    1.77 +lemma open_basisE:
    1.78    assumes "open X" assumes "X \<noteq> {}"
    1.79    obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
    1.80    "X = UNION UNIV (\<lambda>i. Pi' (A i) (B i))" "\<And>n i. i\<in>A n \<Longrightarrow> open ((B n) i)" "\<And>n. finite (A n)"
    1.81 -using open_imp_ex_UNION[OF assms] by auto
    1.82 +  using open_imp_ex_UNION[OF assms] by auto
    1.83  
    1.84 -lemma
    1.85 -  open_basis_of_enumE:
    1.86 +lemma open_basis_of_enumE:
    1.87    assumes "open X" assumes "X \<noteq> {}"
    1.88    obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
    1.89    "X = UNION UNIV (\<lambda>i. Pi' (A i) (B i))" "\<And>n i. i\<in>A n \<Longrightarrow> (B n) i \<in> range enum_basis"
    1.90    "\<And>n. finite (A n)"
    1.91 -using open_imp_ex_UNION_of_enum[OF assms] by auto
    1.92 +  using open_imp_ex_UNION_of_enum[OF assms] by auto
    1.93  
    1.94  instance proof qed (blast intro: finmap_topological_basis)
    1.95  
    1.96 @@ -623,9 +601,7 @@
    1.97  subsection {* Product Measurable Space of Finite Maps *}
    1.98  
    1.99  definition "PiF I M \<equiv>
   1.100 -  sigma
   1.101 -    (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))
   1.102 -    {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   1.103 +  sigma (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j))) {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   1.104  
   1.105  abbreviation
   1.106    "Pi\<^isub>F I M \<equiv> PiF I M"
   1.107 @@ -691,8 +667,7 @@
   1.108    using assms
   1.109    by (auto intro: in_sets_PiFI intro!: singleton_space_subset_in_sets)
   1.110  
   1.111 -lemma
   1.112 -  finite_measurable_singletonI:
   1.113 +lemma finite_measurable_singletonI:
   1.114    assumes "finite I"
   1.115    assumes "\<And>J. J \<in> I \<Longrightarrow> finite J"
   1.116    assumes MN: "\<And>J. J \<in> I \<Longrightarrow> A \<in> measurable (PiF {J} M) N"
   1.117 @@ -717,8 +692,7 @@
   1.118      by (auto simp: space_PiF measurable_space Pi'_def)
   1.119  qed
   1.120  
   1.121 -lemma
   1.122 -  countable_finite_comprehension:
   1.123 +lemma countable_finite_comprehension:
   1.124    fixes f :: "'a::countable set \<Rightarrow> _"
   1.125    assumes "\<And>s. P s \<Longrightarrow> finite s"
   1.126    assumes "\<And>s. P s \<Longrightarrow> f s \<in> sets M"
   1.127 @@ -764,8 +738,7 @@
   1.128    using assms
   1.129    by (auto intro: in_sets_PiFI intro!: space_subset_in_sets)
   1.130  
   1.131 -lemma
   1.132 -  countable_measurable_PiFI:
   1.133 +lemma countable_measurable_PiFI:
   1.134    fixes I::"'a::countable set set"
   1.135    assumes MN: "\<And>J. J \<in> I \<Longrightarrow> finite J \<Longrightarrow> A \<in> measurable (PiF {J} M) N"
   1.136    shows "A \<in> measurable (PiF I M) N"
   1.137 @@ -809,18 +782,15 @@
   1.138    apply (insert S, auto)
   1.139    done
   1.140  
   1.141 -lemma
   1.142 -  restrict_sets_measurable:
   1.143 +lemma restrict_sets_measurable:
   1.144    assumes A: "A \<in> sets (PiF I M)" and "J \<subseteq> I"
   1.145    shows "A \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
   1.146    using A[unfolded sets_PiF]
   1.147 -  apply (induct A)
   1.148 -  unfolding sets_PiF[symmetric] unfolding space_PiF[symmetric]
   1.149 -proof -
   1.150 -  fix a assume "a \<in> {Pi' J X |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   1.151 +proof (induct A)
   1.152 +  case (Basic a)
   1.153    then obtain K S where S: "a = Pi' K S" "K \<in> I" "(\<forall>i\<in>K. S i \<in> sets (M i))"
   1.154      by auto
   1.155 -  show "a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
   1.156 +  show ?case
   1.157    proof cases
   1.158      assume "K \<in> J"
   1.159      hence "a \<inter> {m. domain m \<in> J} \<in> {Pi' K X |X K. K \<in> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))}" using S
   1.160 @@ -834,21 +804,18 @@
   1.161      finally show ?thesis .
   1.162    qed
   1.163  next
   1.164 -  show "{} \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" by simp
   1.165 -next
   1.166 -  fix a :: "nat \<Rightarrow> _"
   1.167 -  assume a: "(\<And>i. a i \<inter> {m. domain m \<in> J} \<in> sets (PiF J M))"
   1.168 +  case (Union a)
   1.169    have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
   1.170      by simp
   1.171 -  also have "\<dots> \<in> sets (PiF J M)" using a by (intro countable_nat_UN) auto
   1.172 -  finally show "UNION UNIV a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" .
   1.173 +  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
   1.174 +  finally show ?case .
   1.175  next
   1.176 -  fix a assume a: "a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
   1.177 +  case (Compl a)
   1.178    have "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} = (space (PiF J M) - (a \<inter> {m. domain m \<in> J}))"
   1.179      using `J \<subseteq> I` by (auto simp: space_PiF Pi'_def)
   1.180 -  also have "\<dots> \<in> sets (PiF J M)" using a by auto
   1.181 -  finally show "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" .
   1.182 -qed
   1.183 +  also have "\<dots> \<in> sets (PiF J M)" using Compl by auto
   1.184 +  finally show ?case by (simp add: space_PiF)
   1.185 +qed simp
   1.186  
   1.187  lemma measurable_finmap_of:
   1.188    assumes f: "\<And>i. (\<exists>x \<in> space N. i \<in> J x) \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
   1.189 @@ -892,7 +859,7 @@
   1.190    done
   1.191  
   1.192  lemma proj_measurable_singleton:
   1.193 -  assumes "A \<in> sets (M i)" "finite I"
   1.194 +  assumes "A \<in> sets (M i)"
   1.195    shows "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) \<in> sets (PiF {I} M)"
   1.196  proof cases
   1.197    assume "i \<in> I"
   1.198 @@ -910,11 +877,10 @@
   1.199  qed
   1.200  
   1.201  lemma measurable_proj_singleton:
   1.202 -  fixes I
   1.203 -  assumes "finite I" "i \<in> I"
   1.204 +  assumes "i \<in> I"
   1.205    shows "(\<lambda>x. (x)\<^isub>F i) \<in> measurable (PiF {I} M) (M i)"
   1.206 -proof (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms)
   1.207 -qed (insert `i \<in> I`, auto simp: space_PiF)
   1.208 +  by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms)
   1.209 +     (insert `i \<in> I`, auto simp: space_PiF)
   1.210  
   1.211  lemma measurable_proj_countable:
   1.212    fixes I::"'a::countable set set"
   1.213 @@ -942,13 +908,11 @@
   1.214    using assms
   1.215    by (intro measurable_finmap_of measurable_component_singleton) auto
   1.216  
   1.217 -lemma
   1.218 -  measurable_proj_PiM:
   1.219 +lemma measurable_proj_PiM:
   1.220    fixes J K ::"'a::countable set" and I::"'a set set"
   1.221    assumes "finite J" "J \<in> I"
   1.222    assumes "x \<in> space (PiM J M)"
   1.223 -  shows "proj \<in>
   1.224 -    measurable (PiF {J} M) (PiM J M)"
   1.225 +  shows "proj \<in> measurable (PiF {J} M) (PiM J M)"
   1.226  proof (rule measurable_PiM_single)
   1.227    show "proj \<in> space (PiF {J} M) \<rightarrow> (\<Pi>\<^isub>E i \<in> J. space (M i))"
   1.228      using assms by (auto simp add: space_PiM space_PiF extensional_def sets_PiF Pi'_def)
   1.229 @@ -1187,7 +1151,7 @@
   1.230    qed
   1.231  qed
   1.232  
   1.233 -lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. J \<leadsto> UNIV) = UNIV" by auto
   1.234 +lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. PI' j : J. UNIV) = UNIV" by auto
   1.235  
   1.236  lemma borel_eq_PiF_borel:
   1.237    shows "(borel :: ('i::countable \<Rightarrow>\<^isub>F 'a::polish_space) measure) =
   1.238 @@ -1277,59 +1241,14 @@
   1.239  
   1.240  subsection {* Isomorphism between Functions and Finite Maps *}
   1.241  
   1.242 -lemma
   1.243 -  measurable_finmap_compose:
   1.244 -  fixes f::"'a \<Rightarrow> 'b"
   1.245 -  assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
   1.246 -  assumes "finite J"
   1.247 +lemma measurable_finmap_compose:
   1.248    shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
   1.249 -proof (rule measurable_PiM)
   1.250 -  show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
   1.251 -  proof safe
   1.252 -    fix x and i
   1.253 -    assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
   1.254 -    with inj show  "compose J x f i \<in> space M"
   1.255 -      by (auto simp: space_PiM compose_def)
   1.256 -  next
   1.257 -    fix x i assume "i \<notin> J"
   1.258 -    with compose_extensional[of J x f]
   1.259 -    show "compose J x f i = undefined" by (auto simp: extensional_def)
   1.260 -  qed
   1.261 -next
   1.262 -  fix S X
   1.263 -  have inv: "\<And>j. j \<in> f ` J \<Longrightarrow> f (f' j) = j" using assms by auto
   1.264 -  assume S: "S \<noteq> {} \<or> J = {}" "finite S" "S \<subseteq> J" and P: "\<And>i. i \<in> S \<Longrightarrow> X i \<in> sets M"
   1.265 -  have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
   1.266 -    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.267 -    using assms inv S sets_into_space[OF P]
   1.268 -    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
   1.269 -  also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
   1.270 -  proof
   1.271 -    from S show "f ` S \<subseteq> f `  J" by auto
   1.272 -    show "(\<Pi>\<^isub>E b\<in>f ` S. X (f' b)) \<in> sets (Pi\<^isub>M (f ` S) (\<lambda>_. M))"
   1.273 -    proof (rule sets_PiM_I_finite)
   1.274 -      show "finite (f ` S)" using S by simp
   1.275 -      fix i assume "i \<in> f ` S" hence "f' i \<in> S" using S assms by auto
   1.276 -      thus "X (f' i) \<in> sets M" by (rule P)
   1.277 -    qed
   1.278 -  qed
   1.279 -  finally show "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
   1.280 -    space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))" .
   1.281 -qed
   1.282 +  unfolding compose_def by measurable
   1.283  
   1.284 -lemma
   1.285 -  measurable_compose_inv:
   1.286 -  fixes f::"'a \<Rightarrow> 'b"
   1.287 +lemma measurable_compose_inv:
   1.288    assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
   1.289 -  assumes "finite J"
   1.290    shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))"
   1.291 -proof -
   1.292 -  have "(\<lambda>m. compose (f ` J) m f') \<in> measurable (Pi\<^isub>M (f' ` f ` J) (\<lambda>_. M)) (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
   1.293 -    using assms by (auto intro: measurable_finmap_compose)
   1.294 -  moreover
   1.295 -  from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI)
   1.296 -  ultimately show ?thesis by simp
   1.297 -qed
   1.298 +  unfolding compose_def by (rule measurable_restrict) (auto simp: inj)
   1.299  
   1.300  locale function_to_finmap =
   1.301    fixes J::"'a set" and f :: "'a \<Rightarrow> 'b::countable" and f'
   1.302 @@ -1390,16 +1309,6 @@
   1.303  
   1.304  definition "mf = (\<lambda>g. compose J g f) o proj"
   1.305  
   1.306 -lemma
   1.307 -  assumes "x \<in> space (Pi\<^isub>M J (\<lambda>_. M))" "finite J"
   1.308 -  shows "proj (finmap_of J x) = x"
   1.309 -  using assms by (auto simp: space_PiM extensional_def)
   1.310 -
   1.311 -lemma
   1.312 -  assumes "x \<in> space (Pi\<^isub>F {J} (\<lambda>_. M))"
   1.313 -  shows "finmap_of J (proj x) = x"
   1.314 -  using assms by (auto simp: space_PiF Pi'_def finmap_eq_iff)
   1.315 -
   1.316  lemma mf_fm:
   1.317    assumes "x \<in> space (Pi\<^isub>M J (\<lambda>_. M))"
   1.318    shows "mf (fm x) = x"
   1.319 @@ -1423,9 +1332,8 @@
   1.320    shows "mf \<in> measurable (PiF {f ` J} (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
   1.321    unfolding mf_def
   1.322  proof (rule measurable_comp, rule measurable_proj_PiM)
   1.323 -  show "(\<lambda>g. compose J g f) \<in>
   1.324 -    measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
   1.325 -    by (rule measurable_finmap_compose, rule inv) auto
   1.326 +  show "(\<lambda>g. compose J g f) \<in> measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
   1.327 +    by (rule measurable_finmap_compose)
   1.328  qed (auto simp add: space_PiM extensional_def assms)
   1.329  
   1.330  lemma fm_image_measurable:
     2.1 --- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
     2.2 +++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:09:11 2012 +0100
     2.3 @@ -124,13 +124,9 @@
     2.4    shows "limP J M P = P J" (is "?P = _")
     2.5  proof (rule measure_eqI_generator_eq)
     2.6    let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
     2.7 -  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
     2.8    let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
     2.9 -  show "Int_stable ?J"
    2.10 -    by (rule Int_stable_PiE)
    2.11    interpret prob_space "P J" using proj_prob_space `finite J` by simp
    2.12 -  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
    2.13 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
    2.14 +  show "emeasure ?P (\<Pi>\<^isub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
    2.15    show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
    2.16      using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
    2.17    fix X assume "X \<in> ?J"
    2.18 @@ -142,7 +138,7 @@
    2.19    show "emeasure (limP J M P) X = emeasure (P J) X"
    2.20      unfolding X using E
    2.21      by (intro emeasure_limP assms) simp
    2.22 -qed (insert `finite J`, auto intro!: prod_algebraI_finite)
    2.23 +qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
    2.24  
    2.25  lemma emeasure_fun_emb[simp]:
    2.26    assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
    2.27 @@ -150,9 +146,12 @@
    2.28    using assms
    2.29    by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
    2.30  
    2.31 +abbreviation
    2.32 +  "emb L K X \<equiv> prod_emb L M K X"
    2.33 +
    2.34  lemma prod_emb_injective:
    2.35 -  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
    2.36 -  assumes "prod_emb L M J X = prod_emb L M J Y"
    2.37 +  assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
    2.38 +  assumes "emb L J X = emb L J Y"
    2.39    shows "X = Y"
    2.40  proof (rule injective_vimage_restrict)
    2.41    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    2.42 @@ -169,9 +168,6 @@
    2.43      using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
    2.44  qed fact
    2.45  
    2.46 -abbreviation
    2.47 -  "emb L K X \<equiv> prod_emb L M K X"
    2.48 -
    2.49  definition generator :: "('i \<Rightarrow> 'a) set set" where
    2.50    "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
    2.51  
    2.52 @@ -265,11 +261,7 @@
    2.53  lemma generatorE:
    2.54    assumes A: "A \<in> generator"
    2.55    obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X"
    2.56 -proof -
    2.57 -  from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
    2.58 -    "\<mu>G A = emeasure (limP J M P) X" by auto
    2.59 -  then show thesis by (intro that) auto
    2.60 -qed
    2.61 +  using generator_Ex[OF A] by atomize_elim auto
    2.62  
    2.63  lemma merge_sets:
    2.64    "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
     3.1 --- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 12:29:02 2012 +0100
     3.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 16:09:11 2012 +0100
     3.3 @@ -626,7 +626,6 @@
     3.4  hide_const (open) Abs_finmap
     3.5  hide_const (open) Rep_finmap
     3.6  hide_const (open) finmap_of
     3.7 -hide_const (open) finmapset
     3.8  hide_const (open) proj
     3.9  hide_const (open) domain
    3.10  hide_const (open) enum_basis_finmap