# 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 \ algebra (M\sets := lambda_system M f\)" - 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 \ lambda_system M f" using A by blast + interpret l: algebra "M\sets := lambda_system M f\" + using f by (rule lambda_system_algebra) have 4: "UNION {0.. 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 \ 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\sets := lambda_system M f\" + using pos by (rule lambda_system_algebra) have A'': "range A \ sets M" by (metis A image_subset_iff lambda_system_sets) @@ -366,7 +367,7 @@ have *: "\i. 0 \ f (A i)" using pos A'' unfolding positive_def by auto have dis: "\N. disjoint_family_on A {..i. f (A i)) \ f (\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.. a) \ f a" using A'' by (blast intro: increasingD [OF inc] A'' UNION_in_sets) have ls: "(\i\{0.. 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 \ (\i\{0..i\{0..i. A i)) \ f (a - (\i\{0..measure := m\) \ algebra M'" - unfolding algebra_def by simp + unfolding algebra_iff_Un by simp lemma sigma_algebra_measure_update[simp]: "sigma_algebra (M'\measure := m\) \ 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 \ Pow (space M)" - and empty_sets [iff]: "{} \ sets M" - and compl_sets [intro]: "!!a. a \ sets M \ space M - a \ sets M" - and Un [intro]: "!!a b. a \ sets M \ b \ sets M \ a \ b \ sets M" -lemma (in algebra) top [iff]: "space M \ sets M" - by (metis Diff_empty compl_sets empty_sets) - -lemma (in algebra) sets_into_space: "x \ sets M \ x \ space M" +lemma (in subset_class) sets_into_space: "x \ sets M \ x \ space M" by (metis PowD contra_subsetD space_closed) -lemma (in algebra) Int [intro]: +locale ring_of_sets = subset_class + + assumes empty_sets [iff]: "{} \ sets M" + and Diff [intro]: "\a b. a \ sets M \ b \ sets M \ a - b \ sets M" + and Un [intro]: "\a b. a \ sets M \ b \ sets M \ a \ b \ sets M" + +lemma (in ring_of_sets) Int [intro]: assumes a: "a \ sets M" and b: "b \ sets M" shows "a \ b \ sets M" proof - - have "((space M - a) \ (space M - b)) \ sets M" - by (metis a b compl_sets Un) - moreover - have "a \ b = space M - ((space M - a) \ (space M - b))" - using space_closed a b - by blast - ultimately show ?thesis - by (metis compl_sets) + have "a \ b = a - (a - b)" + by auto + then show "a \ b \ sets M" + using a b by auto qed -lemma (in algebra) Diff [intro]: - assumes a: "a \ sets M" and b: "b \ sets M" shows "a - b \ sets M" -proof - - have "(a \ (space M - b)) \ sets M" - by (metis a b compl_sets Int) - moreover - have "a - b = (a \ (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 \ X \ sets M \ Union X \ 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 "\i. i \ I \ A i \ sets M" shows "(\i\I. A i) \ 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 \ {}" "\i. i \ I \ A i \ sets M" shows "(\i\I. A i) \ sets M" using assms by (induct rule: finite_ne_induct) auto -lemma algebra_iff_Int: - "algebra M \ - sets M \ Pow (space M) & {} \ sets M & - (\a \ sets M. space M - a \ sets M) & - (\a \ sets M. \ b \ sets M. a \ b \ sets M)" -proof (auto simp add: algebra.Int, auto simp add: algebra_def) - fix a b - assume ab: "sets M \ Pow (space M)" - "\a\sets M. space M - a \ sets M" - "\a\sets M. \b\sets M. a \ b \ sets M" - "a \ sets M" "b \ sets M" - hence "a \ b = space M - ((space M - a) \ (space M - b))" - by blast - also have "... \ sets M" - by (metis ab) - finally show "a \ b \ sets M" . -qed - -lemma (in algebra) insert_in_sets: +lemma (in ring_of_sets) insert_in_sets: assumes "{x} \ sets M" "A \ sets M" shows "insert x A \ sets M" proof - have "{x} \ A \ sets M" using assms by (rule Un) thus ?thesis by auto qed -lemma (in algebra) Int_space_eq1 [simp]: "x \ sets M \ space M \ x = x" +lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \ sets M \ space M \ x = x" by (metis Int_absorb1 sets_into_space) -lemma (in algebra) Int_space_eq2 [simp]: "x \ sets M \ x \ space M = x" +lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \ sets M \ x \ space M = x" by (metis Int_absorb2 sets_into_space) +locale algebra = ring_of_sets + + assumes top [iff]: "space M \ sets M" + +lemma (in algebra) compl_sets [intro]: + "a \ sets M \ space M - a \ sets M" + by auto + +lemma algebra_iff_Un: + "algebra M \ + sets M \ Pow (space M) & + {} \ sets M & + (\a \ sets M. space M - a \ sets M) & + (\a \ sets M. \ b \ sets M. a \ b \ sets M)" (is "_ \ ?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 \ Pow (space M)" "{} \ sets M" "space M \ sets M" + using `?Un` by auto + fix a b assume a: "a \ sets M" and b: "b \ sets M" + then show "a \ b \ sets M" using `?Un` by auto + have "a - b = space M - ((space M - a) \ b)" + using space a b by auto + then show "a - b \ sets M" + using a b `?Un` by auto + qed +qed + +lemma algebra_iff_Int: + "algebra M \ + sets M \ Pow (space M) & {} \ sets M & + (\a \ sets M. space M - a \ sets M) & + (\a \ sets M. \ b \ sets M. a \ b \ sets M)" (is "_ \ ?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 \ Pow (space M)" "{} \ sets M" + using `?Int` by auto + from `?Int` show "\a. a \ sets M \ space M - a \ sets M" by auto + fix a b assume sets: "a \ sets M" "b \ sets M" + hence "a \ b = space M - ((space M - a) \ (space M - b))" + using space by blast + also have "... \ sets M" + using sets `?Int` by auto + finally show "a \ b \ sets M" . + qed +qed + section {* Restricted algebras *} abbreviation (in algebra) @@ -174,7 +196,7 @@ lemma algebra_Pow: "algebra \ space = sp, sets = Pow sp, \ = X \" - by (auto simp add: algebra_def) + by (auto simp add: algebra_iff_Un) lemma sigma_algebra_Pow: "sigma_algebra \ space = sp, sets = Pow sp, \ = X \" @@ -205,7 +227,7 @@ {} \ sets M \ (\s \ sets M. space M - s \ sets M) \ (\A. range A \ sets M \ (\i::nat. A i) \ 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 \ space M. x \ A} \ sets M" using `A \ sets M` by auto qed -lemma (in algebra) measurable_ident[intro, simp]: "id \ measurable M M" +lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \ measurable M M" by (auto simp add: measurable_def) lemma measurable_comp[intro]: @@ -666,7 +688,7 @@ lemma disjointed_subset: "disjointed A n \ 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 \ 'a set" assumes A: "range A \ sets M " shows "(\i\{0.. 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 \ sets M " shows "range (disjointed A) \ 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 \ sets M \ range (disjointed A) \ sets M" + using range_disjointed_sets . + lemma sigma_algebra_disjoint_iff: "sigma_algebra M \ algebra M & @@ -702,7 +728,7 @@ disjoint_family (disjointed A) \ (\i. disjointed A i) \ sets M" by blast hence "(\i. disjointed A i) \ 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 "(\i::nat. A i) \ sets M" by (simp add: UN_disjointed_eq) qed @@ -868,7 +894,6 @@ (\i. A i) \ sets M) & (\A. (range A \ sets M) & disjoint_family A \ (\i::nat. A i) \ sets M)" - inductive_set smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ '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 \ Pow (space M)" - and space: "space M \ sets M" +locale dynkin_system = subset_class + + assumes space: "space M \ sets M" and compl[intro!]: "\A. A \ sets M \ space M - A \ sets M" and UN[intro!]: "\A. disjoint_family A \ range A \ sets M \ (\i::nat. A i) \ sets M" -lemma (in dynkin_system) sets_into_space: "\ A. A \ sets M \ A \ space M" - using space_closed by auto - lemma (in dynkin_system) empty[intro, simp]: "{} \ sets M" using space compl[of "space M"] by simp @@ -1156,7 +1176,7 @@ assumes "\ A. disjoint_family A \ range A \ sets M \ (\i::nat. A i) \ 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 \ space = A, sets = Pow A \" @@ -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 \ Pow (space M)" using sets_into_space by auto next @@ -1211,13 +1231,12 @@ fix A assume "A \ sets (dynkin M)" moreover { fix D assume "A \ D" and d: "dynkin_system \ space = space M, sets = D \" - from dynkin_system.sets_into_space[OF d] `A \ D` - have "A \ space M" by auto } + then have "A \ space M" by (auto simp: dynkin_system_def subset_class_def) } moreover have "{D. dynkin_system \ space = space M, sets = D\ \ sets M \ D} \ {}" using assms dynkin_system_trivial by fastsimp ultimately show "A \ 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) \ 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 \space = space N, sets = sets M \" - 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 \ sets M` show ?thesis by (auto simp add: dynkin_def) qed