author hoelzl Wed, 10 Oct 2012 12:12:37 +0200 changeset 49804 ace9b5a83e60 parent 49803 2f076e377703 child 49805 9a2a53be24a2
infprod generator works also with empty index set
```--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:36 2012 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:37 2012 +0200
@@ -174,15 +174,24 @@
qed

lemma (in product_prob_space) sets_PiM_generator:
-  assumes "I \<noteq> {}" shows "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
-proof
-  show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
-    unfolding sets_PiM
-  proof (safe intro!: sigma_sets_subseteq)
-    fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
-      by (auto intro!: generatorI' elim!: prod_algebraE)
-  qed
-qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+  "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+proof cases
+  assume "I = {}" then show ?thesis
+    unfolding generator_def
+    by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof
+    show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
+      unfolding sets_PiM
+    proof (safe intro!: sigma_sets_subseteq)
+      fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
+        by (auto intro!: generatorI' elim!: prod_algebraE)
+    qed
+  qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+qed
+

lemma (in product_prob_space) generatorI:
"J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
@@ -628,7 +637,7 @@
using X by (auto simp add: emeasure_PiM)
next
show "positive (sets (Pi\<^isub>M I M)) \<mu>" "countably_additive (sets (Pi\<^isub>M I M)) \<mu>"
-      using \<mu> unfolding sets_PiM_generator[OF `I \<noteq> {}`] by (auto simp: measure_space_def)
+      using \<mu> unfolding sets_PiM_generator by (auto simp: measure_space_def)
qed
qed
```