# HG changeset patch
# User hoelzl
# Date 1353337751 -3600
# Node ID 4161c834c2fdefd0aaf4f6d87e5611f82fea4100
# Parent  69b35a75caf3f0b6fc65c198237251a6d26669fc
tuned FinMap

diff -r 69b35a75caf3 -r 4161c834c2fd src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 12:29:02 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 19 16:09:11 2012 +0100
@@ -80,8 +80,7 @@
   using assms
   apply (auto simp: finmap_eq_iff restrict_def) by metis
 
-lemma
-  finmap_of_inj_on_extensional_finite:
+lemma finmap_of_inj_on_extensional_finite:
   assumes "finite K"
   assumes "S \<subseteq> extensional K"
   shows "inj_on (finmap_of K) S"
@@ -125,14 +124,6 @@
 translations
   "PI' x:A. B" == "CONST Pi' A (%x. B)"
 
-abbreviation
-  finmapset :: "['a set, 'b set] => ('a \<Rightarrow>\<^isub>F 'b) set"
-    (infixr "~>" 60) where
-  "A ~> B \<equiv> Pi' A (%_. B)"
-
-notation (xsymbols)
-  finmapset  (infixr "\<leadsto>" 60)
-
 subsubsection{*Basic Properties of @{term Pi'}*}
 
 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"
@@ -141,9 +132,6 @@
 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"
   by (simp add:Pi'_def)
 
-lemma finmapsetI: "domain f = A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f \<in> A \<leadsto> B"
-  by (simp add: Pi_def)
-
 lemma Pi'_mem: "f\<in> Pi' A B \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<in> B x"
   by (simp add: Pi'_def)
 
@@ -158,12 +146,6 @@
   "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"
   by (auto simp: Pi'_def)
 
-lemma funcset_mem: "[|f \<in> A \<leadsto> B; x \<in> A|] ==> f x \<in> B"
-  by (simp add: Pi'_def)
-
-lemma funcset_image: "f \<in> A \<leadsto> B ==> f ` A \<subseteq> B"
-by auto
-
 lemma Pi'_eq_empty[simp]:
   assumes "finite A" shows "(Pi' A B) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
   using assms
@@ -554,8 +536,7 @@
   shows "open x"
   using finmap_topological_basis assms by (auto simp: topological_basis_def)
 
-lemma
-  open_imp_ex_UNION_of_enum:
+lemma open_imp_ex_UNION_of_enum:
   fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   assumes "open X" assumes "X \<noteq> {}"
   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>
@@ -588,8 +569,7 @@
   qed
 qed
 
-lemma
-  open_imp_ex_UNION:
+lemma open_imp_ex_UNION:
   fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   assumes "open X" assumes "X \<noteq> {}"
   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>
@@ -601,20 +581,18 @@
   apply (auto simp: open_enum_basis)
   done
 
-lemma
-  open_basisE:
+lemma open_basisE:
   assumes "open X" assumes "X \<noteq> {}"
   obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   "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)"
-using open_imp_ex_UNION[OF assms] by auto
+  using open_imp_ex_UNION[OF assms] by auto
 
-lemma
-  open_basis_of_enumE:
+lemma open_basis_of_enumE:
   assumes "open X" assumes "X \<noteq> {}"
   obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   "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"
   "\<And>n. finite (A n)"
-using open_imp_ex_UNION_of_enum[OF assms] by auto
+  using open_imp_ex_UNION_of_enum[OF assms] by auto
 
 instance proof qed (blast intro: finmap_topological_basis)
 
@@ -623,9 +601,7 @@
 subsection {* Product Measurable Space of Finite Maps *}
 
 definition "PiF I M \<equiv>
-  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))}"
+  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))}"
 
 abbreviation
   "Pi\<^isub>F I M \<equiv> PiF I M"
@@ -691,8 +667,7 @@
   using assms
   by (auto intro: in_sets_PiFI intro!: singleton_space_subset_in_sets)
 
-lemma
-  finite_measurable_singletonI:
+lemma finite_measurable_singletonI:
   assumes "finite I"
   assumes "\<And>J. J \<in> I \<Longrightarrow> finite J"
   assumes MN: "\<And>J. J \<in> I \<Longrightarrow> A \<in> measurable (PiF {J} M) N"
@@ -717,8 +692,7 @@
     by (auto simp: space_PiF measurable_space Pi'_def)
 qed
 
-lemma
-  countable_finite_comprehension:
+lemma countable_finite_comprehension:
   fixes f :: "'a::countable set \<Rightarrow> _"
   assumes "\<And>s. P s \<Longrightarrow> finite s"
   assumes "\<And>s. P s \<Longrightarrow> f s \<in> sets M"
@@ -764,8 +738,7 @@
   using assms
   by (auto intro: in_sets_PiFI intro!: space_subset_in_sets)
 
-lemma
-  countable_measurable_PiFI:
+lemma countable_measurable_PiFI:
   fixes I::"'a::countable set set"
   assumes MN: "\<And>J. J \<in> I \<Longrightarrow> finite J \<Longrightarrow> A \<in> measurable (PiF {J} M) N"
   shows "A \<in> measurable (PiF I M) N"
@@ -809,18 +782,15 @@
   apply (insert S, auto)
   done
 
-lemma
-  restrict_sets_measurable:
+lemma restrict_sets_measurable:
   assumes A: "A \<in> sets (PiF I M)" and "J \<subseteq> I"
   shows "A \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
   using A[unfolded sets_PiF]
-  apply (induct A)
-  unfolding sets_PiF[symmetric] unfolding space_PiF[symmetric]
-proof -
-  fix a assume "a \<in> {Pi' J X |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
+proof (induct A)
+  case (Basic a)
   then obtain K S where S: "a = Pi' K S" "K \<in> I" "(\<forall>i\<in>K. S i \<in> sets (M i))"
     by auto
-  show "a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
+  show ?case
   proof cases
     assume "K \<in> J"
     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
@@ -834,21 +804,18 @@
     finally show ?thesis .
   qed
 next
-  show "{} \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" by simp
-next
-  fix a :: "nat \<Rightarrow> _"
-  assume a: "(\<And>i. a i \<inter> {m. domain m \<in> J} \<in> sets (PiF J M))"
+  case (Union a)
   have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
     by simp
-  also have "\<dots> \<in> sets (PiF J M)" using a by (intro countable_nat_UN) auto
-  finally show "UNION UNIV a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" .
+  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
+  finally show ?case .
 next
-  fix a assume a: "a \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)"
+  case (Compl a)
   have "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} = (space (PiF J M) - (a \<inter> {m. domain m \<in> J}))"
     using `J \<subseteq> I` by (auto simp: space_PiF Pi'_def)
-  also have "\<dots> \<in> sets (PiF J M)" using a by auto
-  finally show "(space (PiF I M) - a) \<inter> {m. domain m \<in> J} \<in> sets (PiF J M)" .
-qed
+  also have "\<dots> \<in> sets (PiF J M)" using Compl by auto
+  finally show ?case by (simp add: space_PiF)
+qed simp
 
 lemma measurable_finmap_of:
   assumes f: "\<And>i. (\<exists>x \<in> space N. i \<in> J x) \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
@@ -892,7 +859,7 @@
   done
 
 lemma proj_measurable_singleton:
-  assumes "A \<in> sets (M i)" "finite I"
+  assumes "A \<in> sets (M i)"
   shows "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) \<in> sets (PiF {I} M)"
 proof cases
   assume "i \<in> I"
@@ -910,11 +877,10 @@
 qed
 
 lemma measurable_proj_singleton:
-  fixes I
-  assumes "finite I" "i \<in> I"
+  assumes "i \<in> I"
   shows "(\<lambda>x. (x)\<^isub>F i) \<in> measurable (PiF {I} M) (M i)"
-proof (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms)
-qed (insert `i \<in> I`, auto simp: space_PiF)
+  by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms)
+     (insert `i \<in> I`, auto simp: space_PiF)
 
 lemma measurable_proj_countable:
   fixes I::"'a::countable set set"
@@ -942,13 +908,11 @@
   using assms
   by (intro measurable_finmap_of measurable_component_singleton) auto
 
-lemma
-  measurable_proj_PiM:
+lemma measurable_proj_PiM:
   fixes J K ::"'a::countable set" and I::"'a set set"
   assumes "finite J" "J \<in> I"
   assumes "x \<in> space (PiM J M)"
-  shows "proj \<in>
-    measurable (PiF {J} M) (PiM J M)"
+  shows "proj \<in> measurable (PiF {J} M) (PiM J M)"
 proof (rule measurable_PiM_single)
   show "proj \<in> space (PiF {J} M) \<rightarrow> (\<Pi>\<^isub>E i \<in> J. space (M i))"
     using assms by (auto simp add: space_PiM space_PiF extensional_def sets_PiF Pi'_def)
@@ -1187,7 +1151,7 @@
   qed
 qed
 
-lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. J \<leadsto> UNIV) = UNIV" by auto
+lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. PI' j : J. UNIV) = UNIV" by auto
 
 lemma borel_eq_PiF_borel:
   shows "(borel :: ('i::countable \<Rightarrow>\<^isub>F 'a::polish_space) measure) =
@@ -1277,59 +1241,14 @@
 
 subsection {* Isomorphism between Functions and Finite Maps *}
 
-lemma
-  measurable_finmap_compose:
-  fixes f::"'a \<Rightarrow> 'b"
-  assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
-  assumes "finite J"
+lemma measurable_finmap_compose:
   shows "(\<lambda>m. compose J m f) \<in> measurable (PiM (f ` J) (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
-proof (rule measurable_PiM)
-  show "(\<lambda>m. compose J m f) \<in> space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<rightarrow> (J \<rightarrow>\<^isub>E space M)"
-  proof safe
-    fix x and i
-    assume x: "x \<in> space (PiM (f ` J) (\<lambda>_. M))" "i \<in> J"
-    with inj show  "compose J x f i \<in> space M"
-      by (auto simp: space_PiM compose_def)
-  next
-    fix x i assume "i \<notin> J"
-    with compose_extensional[of J x f]
-    show "compose J x f i = undefined" by (auto simp: extensional_def)
-  qed
-next
-  fix S X
-  have inv: "\<And>j. j \<in> f ` J \<Longrightarrow> f (f' j) = j" using assms by auto
-  assume S: "S \<noteq> {} \<or> J = {}" "finite S" "S \<subseteq> J" and P: "\<And>i. i \<in> S \<Longrightarrow> X i \<in> sets M"
-  have "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
-    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)))"
-    using assms inv S sets_into_space[OF P]
-    by (force simp: prod_emb_iff compose_def space_PiM extensional_def Pi_def PiE_def intro: imageI)
-  also have "\<dots> \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
-  proof
-    from S show "f ` S \<subseteq> f `  J" by auto
-    show "(\<Pi>\<^isub>E b\<in>f ` S. X (f' b)) \<in> sets (Pi\<^isub>M (f ` S) (\<lambda>_. M))"
-    proof (rule sets_PiM_I_finite)
-      show "finite (f ` S)" using S by simp
-      fix i assume "i \<in> f ` S" hence "f' i \<in> S" using S assms by auto
-      thus "X (f' i) \<in> sets M" by (rule P)
-    qed
-  qed
-  finally show "(\<lambda>m. compose J m f) -` prod_emb J (\<lambda>_. M) S (Pi\<^isub>E S X) \<inter>
-    space (Pi\<^isub>M (f ` J) (\<lambda>_. M)) \<in> sets (Pi\<^isub>M (f ` J) (\<lambda>_. M))" .
-qed
+  unfolding compose_def by measurable
 
-lemma
-  measurable_compose_inv:
-  fixes f::"'a \<Rightarrow> 'b"
+lemma measurable_compose_inv:
   assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
-  assumes "finite J"
   shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))"
-proof -
-  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))"
-    using assms by (auto intro: measurable_finmap_compose)
-  moreover
-  from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI)
-  ultimately show ?thesis by simp
-qed
+  unfolding compose_def by (rule measurable_restrict) (auto simp: inj)
 
 locale function_to_finmap =
   fixes J::"'a set" and f :: "'a \<Rightarrow> 'b::countable" and f'
@@ -1390,16 +1309,6 @@
 
 definition "mf = (\<lambda>g. compose J g f) o proj"
 
-lemma
-  assumes "x \<in> space (Pi\<^isub>M J (\<lambda>_. M))" "finite J"
-  shows "proj (finmap_of J x) = x"
-  using assms by (auto simp: space_PiM extensional_def)
-
-lemma
-  assumes "x \<in> space (Pi\<^isub>F {J} (\<lambda>_. M))"
-  shows "finmap_of J (proj x) = x"
-  using assms by (auto simp: space_PiF Pi'_def finmap_eq_iff)
-
 lemma mf_fm:
   assumes "x \<in> space (Pi\<^isub>M J (\<lambda>_. M))"
   shows "mf (fm x) = x"
@@ -1423,9 +1332,8 @@
   shows "mf \<in> measurable (PiF {f ` J} (\<lambda>_. M)) (PiM J (\<lambda>_. M))"
   unfolding mf_def
 proof (rule measurable_comp, rule measurable_proj_PiM)
-  show "(\<lambda>g. compose J g f) \<in>
-    measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
-    by (rule measurable_finmap_compose, rule inv) auto
+  show "(\<lambda>g. compose J g f) \<in> measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
+    by (rule measurable_finmap_compose)
 qed (auto simp add: space_PiM extensional_def assms)
 
 lemma fm_image_measurable:
diff -r 69b35a75caf3 -r 4161c834c2fd src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:09:11 2012 +0100
@@ -124,13 +124,9 @@
   shows "limP J M P = P J" (is "?P = _")
 proof (rule measure_eqI_generator_eq)
   let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
-  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
   let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
-  show "Int_stable ?J"
-    by (rule Int_stable_PiE)
   interpret prob_space "P J" using proj_prob_space `finite J` by simp
-  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
-  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+  show "emeasure ?P (\<Pi>\<^isub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
   show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
     using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
   fix X assume "X \<in> ?J"
@@ -142,7 +138,7 @@
   show "emeasure (limP J M P) X = emeasure (P J) X"
     unfolding X using E
     by (intro emeasure_limP assms) simp
-qed (insert `finite J`, auto intro!: prod_algebraI_finite)
+qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
 
 lemma emeasure_fun_emb[simp]:
   assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
@@ -150,9 +146,12 @@
   using assms
   by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
 
+abbreviation
+  "emb L K X \<equiv> prod_emb L M K X"
+
 lemma prod_emb_injective:
-  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)"
-  assumes "prod_emb L M J X = prod_emb L M J Y"
+  assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
+  assumes "emb L J X = emb L J Y"
   shows "X = Y"
 proof (rule injective_vimage_restrict)
   show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
@@ -169,9 +168,6 @@
     using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
 qed fact
 
-abbreviation
-  "emb L K X \<equiv> prod_emb L M K X"
-
 definition generator :: "('i \<Rightarrow> 'a) set set" where
   "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
 
@@ -265,11 +261,7 @@
 lemma generatorE:
   assumes A: "A \<in> generator"
   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"
-proof -
-  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"
-    "\<mu>G A = emeasure (limP J M P) X" by auto
-  then show thesis by (intro that) auto
-qed
+  using generator_Ex[OF A] by atomize_elim auto
 
 lemma merge_sets:
   "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)"
diff -r 69b35a75caf3 -r 4161c834c2fd src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 12:29:02 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 16:09:11 2012 +0100
@@ -626,7 +626,6 @@
 hide_const (open) Abs_finmap
 hide_const (open) Rep_finmap
 hide_const (open) finmap_of
-hide_const (open) finmapset
 hide_const (open) proj
 hide_const (open) domain
 hide_const (open) enum_basis_finmap