src/HOL/Analysis/Sigma_Algebra.thy

   thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
 qed
 
 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?]:
   assumes "a \<in> generated_ring"
   obtains C where "finite C" "disjoint C" "C \<subseteq> M" "a = \<Union>C"

 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
   by (simp add: range_binaryset_eq cong del: SUP_cong_simp)
 
 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) &
    (\<forall>A. (range A \<subseteq> M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
         (\<Union>i. A i) \<in> M) &

   show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
 qed
 
 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
 
 lemma Int_stableI_image:

   qed auto
 qed
 
 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:
   assumes "M \<subseteq> Pow (\<Omega>)"
   shows "dynkin_system \<Omega> (dynkin \<Omega> M)"

 
 definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "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>"
-
-typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> 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> }"
 proof%unimportant
   have "sigma_algebra UNIV {{}, UNIV}"
     by (auto simp: sigma_algebra_iff2)
   then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
     by (auto simp: measure_space_def positive_def countably_additive_def)

   by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
 
 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)"
 
 lemma measure_space_0: "A \<subseteq> Pow \<Omega> \<Longrightarrow> measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>x. 0)"

   shows "sigma \<Omega> M = sigma \<Omega> N"
   by (rule measure_eqI) (simp_all add: emeasure_sigma)
 
 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>
     f \<in> measurable M N"
   by (auto simp: measurable_def)

   using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 
 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>"
     and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
   using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]

   "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
   by (auto simp add: measurable_def Pi_iff)
 
 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))"
 
 lemma space_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> space (extend_measure \<Omega> I G \<mu>) = \<Omega>"

   using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \<open>I i j\<close>
   by (auto simp: subset_eq)
 
 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"
   unfolding vimage_algebra_def by (rule space_measure_of) auto
 

     by (simp add: sets_vimage_algebra2 vimage_comp comp_def flip: ex_simps)
 qed (simp add: vimage_algebra_def emeasure_sigma)
 
 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"
   using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto