# HG changeset patch
# User hoelzl
# Date 1295011286 -3600
# Node ID 646a1399e7924f4e3f919116dac79b78135abbf9
# Parent  1fa4725c4656bce67605cc05e02819616c21249e
tuned theorem order

diff -r 1fa4725c4656 -r 646a1399e792 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Jan 13 23:50:16 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Jan 14 14:21:26 2011 +0100
@@ -222,7 +222,44 @@
   | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
 
 definition
-  "sigma M = (| space = space M, sets = sigma_sets (space M) (sets M) |)"
+  "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M) \<rparr>"
+
+lemma (in sigma_algebra) sigma_sets_subset:
+  assumes a: "a \<subseteq> sets M"
+  shows "sigma_sets (space M) a \<subseteq> sets M"
+proof
+  fix x
+  assume "x \<in> sigma_sets (space M) a"
+  from this show "x \<in> sets M"
+    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
+qed
+
+lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
+  by (erule sigma_sets.induct, auto)
+
+lemma sigma_algebra_sigma_sets:
+     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
+  by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
+           intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)
+
+lemma sigma_sets_least_sigma_algebra:
+  assumes "A \<subseteq> Pow S"
+  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
+proof safe
+  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
+    and X: "X \<in> sigma_sets S A"
+  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
+  show "X \<in> B" by auto
+next
+  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
+  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
+     by simp
+  have "A \<subseteq> sigma_sets S A" using assms
+    by (auto intro!: sigma_sets.Basic)
+  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
+    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
+  ultimately show "X \<in> sigma_sets S A" by auto
+qed
 
 lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)"
   unfolding sigma_def by simp
@@ -233,9 +270,6 @@
 lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
   by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
 
-lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
-  by (erule sigma_sets.induct, auto)
-
 lemma sigma_sets_Un:
   "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
 apply (simp add: Un_range_binary range_binary_eq)
@@ -274,16 +308,6 @@
   finally show ?thesis .
 qed
 
-lemma (in sigma_algebra) sigma_sets_subset:
-  assumes a: "a \<subseteq> sets M"
-  shows "sigma_sets (space M) a \<subseteq> sets M"
-proof
-  fix x
-  assume "x \<in> sigma_sets (space M) a"
-  from this show "x \<in> sets M"
-    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
-qed
-
 lemma (in sigma_algebra) sigma_sets_eq:
      "sigma_sets (space M) (sets M) = sets M"
 proof
@@ -294,14 +318,6 @@
     by (metis sigma_sets_subset subset_refl)
 qed
 
-lemma sigma_algebra_sigma_sets:
-     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
-  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
-      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
-  apply (blast dest: sigma_sets_into_sp)
-  apply (rule sigma_sets.Union, fast)
-  done
-
 lemma sigma_algebra_sigma:
     "sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
   apply (rule sigma_algebra_sigma_sets)
@@ -312,25 +328,6 @@
     "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
   by (simp add: sigma_def sigma_sets_subset)
 
-lemma sigma_sets_least_sigma_algebra:
-  assumes "A \<subseteq> Pow S"
-  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
-proof safe
-  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
-    and X: "X \<in> sigma_sets S A"
-  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
-  show "X \<in> B" by auto
-next
-  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
-  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
-     by simp
-  have "A \<subseteq> sigma_sets S A" using assms
-    by (auto intro!: sigma_sets.Basic)
-  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
-    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
-  ultimately show "X \<in> sigma_sets S A" by auto
-qed
-
 lemma (in sigma_algebra) restriction_in_sets:
   fixes A :: "nat \<Rightarrow> 'a set"
   assumes "S \<in> sets M"