--- a/src/HOL/Analysis/Sigma_Algebra.thy Mon Dec 31 12:25:21 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Mon Dec 31 13:05:15 2018 +0100
@@ -802,7 +802,7 @@
subsubsection%unimportant \<open>Ring generated by a semiring\<close>
-definition (in semiring_of_sets)
+definition (in semiring_of_sets) generated_ring :: "'a set set" where
"generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
lemma (in semiring_of_sets) generated_ringE[elim?]:
@@ -947,7 +947,7 @@
subsubsection \<open>Closed CDI\<close>
-definition%important closed_cdi where
+definition%important closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
"closed_cdi \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> &
(\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1243,7 +1243,8 @@
subsubsection "Intersection sets systems"
-definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
+definition%important Int_stable :: "'a set set \<Rightarrow> bool" where
+"Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
lemma (in algebra) Int_stable: "Int_stable M"
unfolding Int_stable_def by auto
@@ -1283,7 +1284,7 @@
subsubsection "Smallest Dynkin systems"
-definition%important dynkin where
+definition%important dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
"dynkin \<Omega> M = (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
lemma dynkin_system_dynkin:
@@ -1460,13 +1461,16 @@
"positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
- "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
+"countably_additive M f \<longleftrightarrow>
+ (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
(\<Sum>i. f (A i)) = f (\<Union>i. A i))"
definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
- "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
+"measure_space \<Omega> A \<mu> \<longleftrightarrow>
+ sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
-typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+typedef%important 'a measure =
+ "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
proof%unimportant
have "sigma_algebra UNIV {{}, UNIV}"
by (auto simp: sigma_algebra_iff2)
@@ -1498,8 +1502,10 @@
interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
using measure_space[of M] by (auto simp: measure_space_def)
-definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
- "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
+definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
+ where
+"measure_of \<Omega> A \<mu> =
+ Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
\<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)"
@@ -1715,8 +1721,9 @@
subsubsection \<open>Measurable functions\<close>
-definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
- "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
+definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ (infixr "\<rightarrow>\<^sub>M" 60) where
+"measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
lemma measurableI:
"(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
@@ -1878,7 +1885,7 @@
subsubsection \<open>Counting space\<close>
definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
- "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
+"count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
lemma
shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
@@ -1955,7 +1962,9 @@
subsubsection%unimportant \<open>Extend measure\<close>
-definition "extend_measure \<Omega> I G \<mu> =
+definition extend_measure :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('b \<Rightarrow> 'a set) \<Rightarrow> ('b \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
+ where
+"extend_measure \<Omega> I G \<mu> =
(if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>')
else measure_of \<Omega> (G`I) (\<lambda>_. 0))"
@@ -2015,7 +2024,7 @@
subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
-definition%important
+definition%important vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
"vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
@@ -2090,7 +2099,7 @@
subsubsection \<open>Restricted Space Sigma Algebra\<close>
-definition restrict_space where
+definition restrict_space :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a measure" where
"restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) (((\<inter>) \<Omega>) ` sets M) (emeasure M)"
lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"