# HG changeset patch
# User hoelzl
# Date 1349863957 -7200
# Node ID ace9b5a83e603e1d564b8f769301ce8ceb6746ee
# Parent  2f076e377703f6e8e6ac91a52cf5f76dca611259
infprod generator works also with empty index set

diff -r 2f076e377703 -r ace9b5a83e60 src/HOL/Probability/Infinite_Product_Measure.thy
--- 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