# HG changeset patch
# User hoelzl
# Date 1300808697 -3600
# Node ID 2b98b4c2e2f1f7da0d4bd5dde0993e7ecc367f06
# Parent  f4e53c8630c06e56632d46686b288500bd3ad939
add ring_of_sets and subset_class as basis for algebra

diff -r f4e53c8630c0 -r 2b98b4c2e2f1 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 19:04:32 2011 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
@@ -217,7 +217,7 @@
 
 lemma (in algebra) lambda_system_algebra:
   "positive M f \<Longrightarrow> algebra (M\<lparr>sets := lambda_system M f\<rparr>)"
-  apply (auto simp add: algebra_def)
+  apply (auto simp add: algebra_iff_Un)
   apply (metis lambda_system_sets set_mp sets_into_space)
   apply (metis lambda_system_empty)
   apply (metis lambda_system_Compl)
@@ -332,9 +332,10 @@
     by (force simp add: disjoint_family_on_def neq_iff)
   have 3: "A n \<in> lambda_system M f" using A
     by blast
+  interpret l: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
+    using f by (rule lambda_system_algebra)
   have 4: "UNION {0..<n} A \<in> lambda_system M f"
-    using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
-    by simp
+    using A l.UNION_in_sets by simp
   from Suc.hyps show ?case
     by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
 qed
@@ -352,8 +353,8 @@
     by (metis countably_subadditive_subadditive csa pos)
   have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
     by simp
-  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
-    by (rule lambda_system_algebra) (rule pos)
+  interpret ls: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
+    using pos by (rule lambda_system_algebra)
   have A'': "range A \<subseteq> sets M"
      by (metis A image_subset_iff lambda_system_sets)
 
@@ -366,7 +367,7 @@
     have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
     have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
     show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
-      using algebra.additive_sum [OF alg_ls lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
+      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
       using A''
       by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI countable_UN)
   qed
@@ -401,8 +402,7 @@
             have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
               by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
             have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
-              using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
-              by (simp add: A)
+              using ls.UNION_in_sets by (simp add: A)
             hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
               by (simp add: lambda_system_eq UNION_in)
             have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
@@ -441,8 +441,8 @@
     by (metis oms outer_measure_space_def)
   have alg: "algebra ?M"
     using lambda_system_algebra [of f, OF pos]
-    by (simp add: algebra_def)
-  then moreover
+    by (simp add: algebra_iff_Un)
+  then
   have "sigma_algebra ?M"
     using lambda_system_caratheodory [OF oms]
     by (simp add: sigma_algebra_disjoint_iff)
@@ -453,7 +453,7 @@
                   countably_additive_def o_def)
   ultimately
   show ?thesis
-    by intro_locales (auto simp add: sigma_algebra_def)
+    by (simp add: measure_space_def)
 qed
 
 lemma (in algebra) additive_increasing:
diff -r f4e53c8630c0 -r 2b98b4c2e2f1 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue Mar 22 19:04:32 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 16:44:57 2011 +0100
@@ -18,7 +18,7 @@
 
 lemma algebra_measure_update[simp]:
   "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
-  unfolding algebra_def by simp
+  unfolding algebra_iff_Un by simp
 
 lemma sigma_algebra_measure_update[simp]:
   "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
diff -r f4e53c8630c0 -r 2b98b4c2e2f1 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 19:04:32 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Mar 22 16:44:57 2011 +0100
@@ -28,89 +28,111 @@
   space :: "'a set"
   sets :: "'a set set"
 
-locale algebra =
+locale subset_class =
   fixes M :: "('a, 'b) algebra_scheme"
   assumes space_closed: "sets M \<subseteq> Pow (space M)"
-     and  empty_sets [iff]: "{} \<in> sets M"
-     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
-     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
 
-lemma (in algebra) top [iff]: "space M \<in> sets M"
-  by (metis Diff_empty compl_sets empty_sets)
-
-lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
+lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
   by (metis PowD contra_subsetD space_closed)
 
-lemma (in algebra) Int [intro]:
+locale ring_of_sets = subset_class +
+  assumes empty_sets [iff]: "{} \<in> sets M"
+     and  Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a - b \<in> sets M"
+     and  Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
+
+lemma (in ring_of_sets) Int [intro]:
   assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
 proof -
-  have "((space M - a) \<union> (space M - b)) \<in> sets M"
-    by (metis a b compl_sets Un)
-  moreover
-  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
-    using space_closed a b
-    by blast
-  ultimately show ?thesis
-    by (metis compl_sets)
+  have "a \<inter> b = a - (a - b)"
+    by auto
+  then show "a \<inter> b \<in> sets M"
+    using a b by auto
 qed
 
-lemma (in algebra) Diff [intro]:
-  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
-proof -
-  have "(a \<inter> (space M - b)) \<in> sets M"
-    by (metis a b compl_sets Int)
-  moreover
-  have "a - b = (a \<inter> (space M - b))"
-    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
-  ultimately show ?thesis
-    by metis
-qed
-
-lemma (in algebra) finite_union [intro]:
+lemma (in ring_of_sets) finite_Union [intro]:
   "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
   by (induct set: finite) (auto simp add: Un)
 
-lemma (in algebra) finite_UN[intro]:
+lemma (in ring_of_sets) finite_UN[intro]:
   assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   shows "(\<Union>i\<in>I. A i) \<in> sets M"
   using assms by induct auto
 
-lemma (in algebra) finite_INT[intro]:
+lemma (in ring_of_sets) finite_INT[intro]:
   assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   shows "(\<Inter>i\<in>I. A i) \<in> sets M"
   using assms by (induct rule: finite_ne_induct) auto
 
-lemma algebra_iff_Int:
-     "algebra M \<longleftrightarrow>
-       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
-       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
-       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
-proof (auto simp add: algebra.Int, auto simp add: algebra_def)
-  fix a b
-  assume ab: "sets M \<subseteq> Pow (space M)"
-             "\<forall>a\<in>sets M. space M - a \<in> sets M"
-             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
-             "a \<in> sets M" "b \<in> sets M"
-  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
-    by blast
-  also have "... \<in> sets M"
-    by (metis ab)
-  finally show "a \<union> b \<in> sets M" .
-qed
-
-lemma (in algebra) insert_in_sets:
+lemma (in ring_of_sets) insert_in_sets:
   assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M"
 proof -
   have "{x} \<union> A \<in> sets M" using assms by (rule Un)
   thus ?thesis by auto
 qed
 
-lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
+lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
   by (metis Int_absorb1 sets_into_space)
 
-lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
+lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
   by (metis Int_absorb2 sets_into_space)
 
+locale algebra = ring_of_sets +
+  assumes top [iff]: "space M \<in> sets M"
+
+lemma (in algebra) compl_sets [intro]:
+  "a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
+  by auto
+
+lemma algebra_iff_Un:
+  "algebra M \<longleftrightarrow>
+    sets M \<subseteq> Pow (space M) &
+    {} \<in> sets M &
+    (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+    (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un")
+proof
+  assume "algebra M"
+  then interpret algebra M .
+  show ?Un using sets_into_space by auto
+next
+  assume ?Un
+  show "algebra M"
+  proof
+    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M"
+      using `?Un` by auto
+    fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M"
+    then show "a \<union> b \<in> sets M" using `?Un` by auto
+    have "a - b = space M - ((space M - a) \<union> b)"
+      using space a b by auto
+    then show "a - b \<in> sets M"
+      using a b  `?Un` by auto
+  qed
+qed
+
+lemma algebra_iff_Int:
+     "algebra M \<longleftrightarrow>
+       sets M \<subseteq> Pow (space M) & {} \<in> sets M &
+       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int")
+proof
+  assume "algebra M"
+  then interpret algebra M .
+  show ?Int using sets_into_space by auto
+next
+  assume ?Int
+  show "algebra M"
+  proof (unfold algebra_iff_Un, intro conjI ballI)
+    show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M"
+      using `?Int` by auto
+    from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M" by auto
+    fix a b assume sets: "a \<in> sets M" "b \<in> sets M"
+    hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
+      using space by blast
+    also have "... \<in> sets M"
+      using sets `?Int` by auto
+    finally show "a \<union> b \<in> sets M" .
+  qed
+qed
+
 section {* Restricted algebras *}
 
 abbreviation (in algebra)
@@ -174,7 +196,7 @@
 
 lemma algebra_Pow:
      "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
-  by (auto simp add: algebra_def)
+  by (auto simp add: algebra_iff_Un)
 
 lemma sigma_algebra_Pow:
      "sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
@@ -205,7 +227,7 @@
        {} \<in> sets M \<and> (\<forall>s \<in> sets M. space M - s \<in> sets M) \<and>
        (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
-         algebra_def Un_range_binary)
+         algebra_iff_Un Un_range_binary)
 
 subsection {* Initial Sigma Algebra *}
 
@@ -513,7 +535,7 @@
   thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
 qed
 
-lemma (in algebra) measurable_ident[intro, simp]: "id \<in> measurable M M"
+lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M"
   by (auto simp add: measurable_def)
 
 lemma measurable_comp[intro]:
@@ -666,7 +688,7 @@
 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   by (auto simp add: disjointed_def)
 
-lemma (in algebra) UNION_in_sets:
+lemma (in ring_of_sets) UNION_in_sets:
   fixes A:: "nat \<Rightarrow> 'a set"
   assumes A: "range A \<subseteq> sets M "
   shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
@@ -678,7 +700,7 @@
     by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
 qed
 
-lemma (in algebra) range_disjointed_sets:
+lemma (in ring_of_sets) range_disjointed_sets:
   assumes A: "range A \<subseteq> sets M "
   shows  "range (disjointed A) \<subseteq> sets M"
 proof (auto simp add: disjointed_def)
@@ -687,6 +709,10 @@
     by (metis A Diff UNIV_I image_subset_iff)
 qed
 
+lemma (in algebra) range_disjointed_sets':
+  "range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
+  using range_disjointed_sets .
+
 lemma sigma_algebra_disjoint_iff:
      "sigma_algebra M \<longleftrightarrow>
       algebra M &
@@ -702,7 +728,7 @@
          disjoint_family (disjointed A) \<longrightarrow>
          (\<Union>i. disjointed A i) \<in> sets M" by blast
   hence "(\<Union>i. disjointed A i) \<in> sets M"
-    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed)
+    by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed)
   thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
 qed
 
@@ -868,7 +894,6 @@
         (\<Union>i. A i) \<in> sets M) &
    (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
 
-
 inductive_set
   smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
   for M
@@ -1117,17 +1142,12 @@
 
 section {* Dynkin systems *}
 
-locale dynkin_system =
-  fixes M :: "('a, 'b) algebra_scheme"
-  assumes space_closed: "sets M \<subseteq> Pow (space M)"
-    and   space: "space M \<in> sets M"
+locale dynkin_system = subset_class +
+  assumes space: "space M \<in> sets M"
     and   compl[intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
     and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
                            \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
 
-lemma (in dynkin_system) sets_into_space: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
-  using space_closed by auto
-
 lemma (in dynkin_system) empty[intro, simp]: "{} \<in> sets M"
   using space compl[of "space M"] by simp
 
@@ -1156,7 +1176,7 @@
   assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
           \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   shows "dynkin_system M"
-  using assms by (auto simp: dynkin_system_def)
+  using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
 
 lemma dynkin_system_trivial:
   shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
@@ -1184,7 +1204,7 @@
 next
   assume "Int_stable M"
   show "sigma_algebra M"
-    unfolding sigma_algebra_disjoint_iff algebra_def
+    unfolding sigma_algebra_disjoint_iff algebra_iff_Un
   proof (intro conjI ballI allI impI)
     show "sets M \<subseteq> Pow (space M)" using sets_into_space by auto
   next
@@ -1211,13 +1231,12 @@
   fix A assume "A \<in> sets (dynkin M)"
   moreover
   { fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
-    from dynkin_system.sets_into_space[OF d] `A \<in> D`
-    have "A \<subseteq> space M" by auto }
+    then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
   moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
     using assms dynkin_system_trivial by fastsimp
   ultimately show "A \<subseteq> space (dynkin M)"
     unfolding dynkin_def using assms
-    by simp (metis dynkin_system.sets_into_space in_mono mem_def)
+    by simp (metis dynkin_system_def subset_class_def in_mono mem_def)
 next
   show "space (dynkin M) \<in> sets (dynkin M)"
     unfolding dynkin_def using dynkin_system.space by fastsimp
@@ -1277,7 +1296,7 @@
 proof -
   have "dynkin_system M" by default
   then have "dynkin_system \<lparr>space = space N, sets = sets M \<rparr>"
-    using assms unfolding dynkin_system_def by simp
+    using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
   with `sets N \<subseteq> sets M` show ?thesis by (auto simp add: dynkin_def)
 qed