# HG changeset patch # User huffman # Date 1314396000 25200 # Node ID c10485a6a7af5a0da275bd9c8754aeef33f8df1a # Parent 5e681762d53896849d2d2b0cc438147a9c8464b9 make HOL-Probability respect set/pred distinction diff -r 5e681762d538 -r c10485a6a7af src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Wed Sep 08 16:10:49 2010 -0700 +++ b/src/HOL/Probability/Borel_Space.thy Fri Aug 26 15:00:00 2011 -0700 @@ -11,7 +11,7 @@ section "Generic Borel spaces" -definition "borel = sigma \ space = UNIV::'a::topological_space set, sets = open\" +definition "borel = sigma \ space = UNIV::'a::topological_space set, sets = {S. open S}\" abbreviation "borel_measurable M \ measurable M borel" interpretation borel: sigma_algebra borel @@ -19,7 +19,7 @@ lemma in_borel_measurable: "f \ borel_measurable M \ - (\S \ sets (sigma \ space = UNIV, sets = open\). + (\S \ sets (sigma \ space = UNIV, sets = {S. open S}\). f -` S \ space M \ sets M)" by (auto simp add: measurable_def borel_def) @@ -35,7 +35,7 @@ lemma borel_open[simp]: assumes "open A" shows "A \ sets borel" proof - - have "A \ open" unfolding mem_def using assms . + have "A \ {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic) qed @@ -71,8 +71,8 @@ shows "f \ borel_measurable M" unfolding borel_def proof (rule measurable_sigma, simp_all) - fix S :: "'x set" assume "S \ open" thus "f -` S \ space M \ sets M" - using assms[of S] by (simp add: mem_def) + fix S :: "'x set" assume "open S" thus "f -` S \ space M \ sets M" + using assms[of S] by simp qed lemma borel_singleton[simp, intro]: @@ -391,7 +391,8 @@ proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp then interpret sigma_algebra ?SIGMA . - { fix S :: "'a set" assume "S \ open" then have "open S" unfolding mem_def . + { fix S :: "'a set" assume "S \ {S. open S}" + then have "open S" unfolding mem_Collect_eq . from open_UNION[OF this] obtain I where *: "S = (\(a, b)\I. @@ -647,8 +648,8 @@ proof - have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto then interpret sigma_algebra ?SIGMA . - { fix M :: "'a set" assume "M \ open" - then have "open M" by (simp add: mem_def) + { fix M :: "'a set" assume "M \ {S. open S}" + then have "open M" by simp have "M \ sets ?SIGMA" apply (subst open_UNION[OF `open M`]) apply (safe intro!: countable_UN) @@ -784,7 +785,7 @@ "(\x::'a::euclidean_space. x $$ i) \ borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma, simp_all) - fix S::"real set" assume "S \ open" then have "open S" unfolding mem_def . + fix S::"real set" assume "open S" from open_vimage_euclidean_component[OF this] show "(\x. x $$ i) -` S \ sets borel" by (auto intro: borel_open) @@ -815,8 +816,8 @@ show "(\x. a + b *\<^sub>R f x) -` S \ space M \ sets M" proof cases assume "b \ 0" - with `open S` have "((\x. (- a + x) /\<^sub>R b) ` S) \ open" (is "?S \ open") - by (auto intro!: open_affinity simp: scaleR_add_right mem_def) + with `open S` have "open ((\x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S") + by (auto intro!: open_affinity simp: scaleR_add_right) hence "?S \ sets borel" unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic) moreover @@ -1099,8 +1100,8 @@ "ereal \ borel_measurable borel" unfolding borel_def[where 'a=ereal] proof (rule borel.measurable_sigma) - fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = open \" - then have "open X" by (auto simp: mem_def) + fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S} \" + then have "open X" by simp then have "open (ereal -` X \ space borel)" by (simp add: open_ereal_vimage) then show "ereal -` X \ space borel \ sets borel" by auto @@ -1114,8 +1115,8 @@ "(real :: ereal \ real) \ borel_measurable borel" unfolding borel_def[where 'a=real] proof (rule borel.measurable_sigma) - fix B :: "real set" assume "B \ sets \space = UNIV, sets = open \" - then have "open B" by (auto simp: mem_def) + fix B :: "real set" assume "B \ sets \space = UNIV, sets = {S. open S} \" + then have "open B" by simp have *: "ereal -` real -` (B - {0}) = B - {0}" by auto have open_real: "open (real -` (B - {0}) :: ereal set)" unfolding open_ereal_def * using `open B` by auto @@ -1190,8 +1191,8 @@ lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal: "(uminus :: ereal \ ereal) \ borel_measurable borel" proof (subst borel_def, rule borel.measurable_sigma) - fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = open\" - then have "open X" by (simp add: mem_def) + fix X :: "ereal set" assume "X \ sets \space = UNIV, sets = {S. open S}\" + then have "open X" by simp have "uminus -` X = uminus ` X" by (force simp: image_iff) then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto then show "uminus -` X \ space borel \ sets borel" by auto diff -r 5e681762d538 -r c10485a6a7af src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Sep 08 16:10:49 2010 -0700 +++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Aug 26 15:00:00 2011 -0700 @@ -1136,7 +1136,6 @@ | Disj: "range A \ Pow(smallest_ccdi_sets M) \ disjoint_family A \ (\i::nat. A i) \ smallest_ccdi_sets M" - monos Pow_mono definition @@ -1485,7 +1484,7 @@ using assms dynkin_system_trivial by fastsimp ultimately show "A \ space (dynkin M)" unfolding dynkin_def using assms - by simp (metis dynkin_system_def subset_class_def in_mono mem_def) + by simp (metis dynkin_system_def subset_class_def in_mono) next show "space (dynkin M) \ sets (dynkin M)" unfolding dynkin_def using dynkin_system.space by fastsimp