# HG changeset patch
# User wenzelm
# Date 1546291294 -3600
# Node ID 8fd576a99a5949839b92ba668abb9da7cb58b943
# Parent  b07ccc6fb13f862819c10bca56cd0471c1eecd6e# Parent  636b3c03a61af6bd04a1b70cd8c81ffec7f92475
merged

diff -r 636b3c03a61a -r 8fd576a99a59 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Dec 31 22:21:02 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Mon Dec 31 22:21:34 2018 +0100
@@ -2193,7 +2193,7 @@
   using assms(2-3) vector_derivative_works
   by auto
 
-subsection\<open>The notion of being field differentiable\<close>
+subsection \<open>Field differentiability\<close>
 
 definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
            (infixr "(field'_differentiable)" 50)
diff -r 636b3c03a61a -r 8fd576a99a59 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Dec 31 22:21:02 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Mon Dec 31 22:21:34 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) &
@@ -1181,16 +1181,16 @@
 
 subsubsection \<open>Dynkin systems\<close>
 
-locale%important dynkin_system = subset_class +
+locale%important Dynkin_system = subset_class +
   assumes space: "\<Omega> \<in> M"
     and   compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
     and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
                            \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
 
-lemma (in dynkin_system) empty[intro, simp]: "{} \<in> M"
+lemma (in Dynkin_system) empty[intro, simp]: "{} \<in> M"
   using space compl[of "\<Omega>"] by simp
 
-lemma (in dynkin_system) diff:
+lemma (in Dynkin_system) diff:
   assumes sets: "D \<in> M" "E \<in> M" and "D \<subseteq> E"
   shows "E - D \<in> M"
 proof -
@@ -1209,41 +1209,42 @@
   finally show ?thesis .
 qed
 
-lemma dynkin_systemI:
+lemma Dynkin_systemI:
   assumes "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" "\<Omega> \<in> M"
   assumes "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
   assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
-  shows "dynkin_system \<Omega> M"
-  using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
+  shows "Dynkin_system \<Omega> M"
+  using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def)
 
-lemma dynkin_systemI':
+lemma Dynkin_systemI':
   assumes 1: "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>"
   assumes empty: "{} \<in> M"
   assumes Diff: "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
   assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
-  shows "dynkin_system \<Omega> M"
+  shows "Dynkin_system \<Omega> M"
 proof -
   from Diff[OF empty] have "\<Omega> \<in> M" by auto
   from 1 this Diff 2 show ?thesis
-    by (intro dynkin_systemI) auto
+    by (intro Dynkin_systemI) auto
 qed
 
-lemma dynkin_system_trivial:
-  shows "dynkin_system A (Pow A)"
-  by (rule dynkin_systemI) auto
+lemma Dynkin_system_trivial:
+  shows "Dynkin_system A (Pow A)"
+  by (rule Dynkin_systemI) auto
 
-lemma sigma_algebra_imp_dynkin_system:
-  assumes "sigma_algebra \<Omega> M" shows "dynkin_system \<Omega> M"
+lemma sigma_algebra_imp_Dynkin_system:
+  assumes "sigma_algebra \<Omega> M" shows "Dynkin_system \<Omega> M"
 proof -
   interpret sigma_algebra \<Omega> M by fact
-  show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
+  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
@@ -1260,7 +1261,7 @@
   "Int_stable M \<Longrightarrow> a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
   unfolding Int_stable_def by auto
 
-lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
+lemma (in Dynkin_system) sigma_algebra_eq_Int_stable:
   "sigma_algebra \<Omega> M \<longleftrightarrow> Int_stable M"
 proof
   assume "sigma_algebra \<Omega> M" then show "Int_stable M"
@@ -1283,48 +1284,48 @@
 
 subsubsection "Smallest Dynkin systems"
 
-definition%important dynkin where
-  "dynkin \<Omega> M =  (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
+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:
+lemma Dynkin_system_Dynkin:
   assumes "M \<subseteq> Pow (\<Omega>)"
-  shows "dynkin_system \<Omega> (dynkin \<Omega> M)"
-proof (rule dynkin_systemI)
-  fix A assume "A \<in> dynkin \<Omega> M"
+  shows "Dynkin_system \<Omega> (Dynkin \<Omega> M)"
+proof (rule Dynkin_systemI)
+  fix A assume "A \<in> Dynkin \<Omega> M"
   moreover
-  { fix D assume "A \<in> D" and d: "dynkin_system \<Omega> D"
-    then have "A \<subseteq> \<Omega>" by (auto simp: dynkin_system_def subset_class_def) }
-  moreover have "{D. dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}"
-    using assms dynkin_system_trivial by fastforce
+  { fix D assume "A \<in> D" and d: "Dynkin_system \<Omega> D"
+    then have "A \<subseteq> \<Omega>" by (auto simp: Dynkin_system_def subset_class_def) }
+  moreover have "{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}"
+    using assms Dynkin_system_trivial by fastforce
   ultimately show "A \<subseteq> \<Omega>"
-    unfolding dynkin_def using assms
+    unfolding Dynkin_def using assms
     by auto
 next
-  show "\<Omega> \<in> dynkin \<Omega> M"
-    unfolding dynkin_def using dynkin_system.space by fastforce
+  show "\<Omega> \<in> Dynkin \<Omega> M"
+    unfolding Dynkin_def using Dynkin_system.space by fastforce
 next
-  fix A assume "A \<in> dynkin \<Omega> M"
-  then show "\<Omega> - A \<in> dynkin \<Omega> M"
-    unfolding dynkin_def using dynkin_system.compl by force
+  fix A assume "A \<in> Dynkin \<Omega> M"
+  then show "\<Omega> - A \<in> Dynkin \<Omega> M"
+    unfolding Dynkin_def using Dynkin_system.compl by force
 next
   fix A :: "nat \<Rightarrow> 'a set"
-  assume A: "disjoint_family A" "range A \<subseteq> dynkin \<Omega> M"
-  show "(\<Union>i. A i) \<in> dynkin \<Omega> M" unfolding dynkin_def
+  assume A: "disjoint_family A" "range A \<subseteq> Dynkin \<Omega> M"
+  show "(\<Union>i. A i) \<in> Dynkin \<Omega> M" unfolding Dynkin_def
   proof (simp, safe)
-    fix D assume "dynkin_system \<Omega> D" "M \<subseteq> D"
+    fix D assume "Dynkin_system \<Omega> D" "M \<subseteq> D"
     with A have "(\<Union>i. A i) \<in> D"
-      by (intro dynkin_system.UN) (auto simp: dynkin_def)
+      by (intro Dynkin_system.UN) (auto simp: Dynkin_def)
     then show "(\<Union>i. A i) \<in> D" by auto
   qed
 qed
 
-lemma dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> dynkin \<Omega> M"
-  unfolding dynkin_def by auto
+lemma Dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> Dynkin \<Omega> M"
+  unfolding Dynkin_def by auto
 
-lemma (in dynkin_system) restricted_dynkin_system:
+lemma (in Dynkin_system) restricted_Dynkin_system:
   assumes "D \<in> M"
-  shows "dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}"
-proof (rule dynkin_systemI, simp_all)
+  shows "Dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}"
+proof (rule Dynkin_systemI, simp_all)
   have "\<Omega> \<inter> D = D"
     using \<open>D \<in> M\<close> sets_into_space by auto
   then show "\<Omega> \<inter> D \<in> M"
@@ -1345,87 +1346,87 @@
     by (auto simp del: UN_simps)
 qed
 
-lemma (in dynkin_system) dynkin_subset:
+lemma (in Dynkin_system) Dynkin_subset:
   assumes "N \<subseteq> M"
-  shows "dynkin \<Omega> N \<subseteq> M"
+  shows "Dynkin \<Omega> N \<subseteq> M"
 proof -
-  have "dynkin_system \<Omega> M" ..
-  then have "dynkin_system \<Omega> M"
-    using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
-  with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: dynkin_def)
+  have "Dynkin_system \<Omega> M" ..
+  then have "Dynkin_system \<Omega> M"
+    using assms unfolding Dynkin_system_def Dynkin_system_axioms_def subset_class_def by simp
+  with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: Dynkin_def)
 qed
 
-lemma sigma_eq_dynkin:
+lemma sigma_eq_Dynkin:
   assumes sets: "M \<subseteq> Pow \<Omega>"
   assumes "Int_stable M"
-  shows "sigma_sets \<Omega> M = dynkin \<Omega> M"
+  shows "sigma_sets \<Omega> M = Dynkin \<Omega> M"
 proof -
-  have "dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)"
-    using sigma_algebra_imp_dynkin_system
-    unfolding dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto
+  have "Dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)"
+    using sigma_algebra_imp_Dynkin_system
+    unfolding Dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto
   moreover
-  interpret dynkin_system \<Omega> "dynkin \<Omega> M"
-    using dynkin_system_dynkin[OF sets] .
-  have "sigma_algebra \<Omega> (dynkin \<Omega> M)"
+  interpret Dynkin_system \<Omega> "Dynkin \<Omega> M"
+    using Dynkin_system_Dynkin[OF sets] .
+  have "sigma_algebra \<Omega> (Dynkin \<Omega> M)"
     unfolding sigma_algebra_eq_Int_stable Int_stable_def
   proof (intro ballI)
-    fix A B assume "A \<in> dynkin \<Omega> M" "B \<in> dynkin \<Omega> M"
-    let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> dynkin \<Omega> M}"
+    fix A B assume "A \<in> Dynkin \<Omega> M" "B \<in> Dynkin \<Omega> M"
+    let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> Dynkin \<Omega> M}"
     have "M \<subseteq> ?D B"
     proof
       fix E assume "E \<in> M"
-      then have "M \<subseteq> ?D E" "E \<in> dynkin \<Omega> M"
+      then have "M \<subseteq> ?D E" "E \<in> Dynkin \<Omega> M"
         using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def)
-      then have "dynkin \<Omega> M \<subseteq> ?D E"
-        using restricted_dynkin_system \<open>E \<in> dynkin \<Omega> M\<close>
-        by (intro dynkin_system.dynkin_subset) simp_all
+      then have "Dynkin \<Omega> M \<subseteq> ?D E"
+        using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close>
+        by (intro Dynkin_system.Dynkin_subset) simp_all
       then have "B \<in> ?D E"
-        using \<open>B \<in> dynkin \<Omega> M\<close> by auto
-      then have "E \<inter> B \<in> dynkin \<Omega> M"
+        using \<open>B \<in> Dynkin \<Omega> M\<close> by auto
+      then have "E \<inter> B \<in> Dynkin \<Omega> M"
         by (subst Int_commute) simp
       then show "E \<in> ?D B"
         using sets \<open>E \<in> M\<close> by auto
     qed
-    then have "dynkin \<Omega> M \<subseteq> ?D B"
-      using restricted_dynkin_system \<open>B \<in> dynkin \<Omega> M\<close>
-      by (intro dynkin_system.dynkin_subset) simp_all
-    then show "A \<inter> B \<in> dynkin \<Omega> M"
-      using \<open>A \<in> dynkin \<Omega> M\<close> sets_into_space by auto
+    then have "Dynkin \<Omega> M \<subseteq> ?D B"
+      using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close>
+      by (intro Dynkin_system.Dynkin_subset) simp_all
+    then show "A \<inter> B \<in> Dynkin \<Omega> M"
+      using \<open>A \<in> Dynkin \<Omega> M\<close> sets_into_space by auto
   qed
   from sigma_algebra.sigma_sets_subset[OF this, of "M"]
-  have "sigma_sets (\<Omega>) (M) \<subseteq> dynkin \<Omega> M" by auto
-  ultimately have "sigma_sets (\<Omega>) (M) = dynkin \<Omega> M" by auto
+  have "sigma_sets (\<Omega>) (M) \<subseteq> Dynkin \<Omega> M" by auto
+  ultimately have "sigma_sets (\<Omega>) (M) = Dynkin \<Omega> M" by auto
   then show ?thesis
-    by (auto simp: dynkin_def)
+    by (auto simp: Dynkin_def)
 qed
 
-lemma (in dynkin_system) dynkin_idem:
-  "dynkin \<Omega> M = M"
+lemma (in Dynkin_system) Dynkin_idem:
+  "Dynkin \<Omega> M = M"
 proof -
-  have "dynkin \<Omega> M = M"
+  have "Dynkin \<Omega> M = M"
   proof
-    show "M \<subseteq> dynkin \<Omega> M"
-      using dynkin_Basic by auto
-    show "dynkin \<Omega> M \<subseteq> M"
-      by (intro dynkin_subset) auto
+    show "M \<subseteq> Dynkin \<Omega> M"
+      using Dynkin_Basic by auto
+    show "Dynkin \<Omega> M \<subseteq> M"
+      by (intro Dynkin_subset) auto
   qed
   then show ?thesis
-    by (auto simp: dynkin_def)
+    by (auto simp: Dynkin_def)
 qed
 
-lemma (in dynkin_system) dynkin_lemma:
+lemma (in Dynkin_system) Dynkin_lemma:
   assumes "Int_stable E"
   and E: "E \<subseteq> M" "M \<subseteq> sigma_sets \<Omega> E"
   shows "sigma_sets \<Omega> E = M"
 proof -
   have "E \<subseteq> Pow \<Omega>"
     using E sets_into_space by force
-  then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E"
-    using \<open>Int_stable E\<close> by (rule sigma_eq_dynkin)
-  then have "dynkin \<Omega> E = M"
-    using assms dynkin_subset[OF E(1)] by simp
+  then have *: "sigma_sets \<Omega> E = Dynkin \<Omega> E"
+    using \<open>Int_stable E\<close> by (rule sigma_eq_Dynkin)
+  then have "Dynkin \<Omega> E = M"
+    using assms Dynkin_subset[OF E(1)] by simp
   with * show ?thesis
-    using assms by (auto simp: dynkin_def)
+    using assms by (auto simp: Dynkin_def)
 qed
 
 subsubsection \<open>Induction rule for intersection-stable generators\<close>
@@ -1447,10 +1448,10 @@
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
     using closed by (rule sigma_algebra_sigma_sets)
   from compl[OF _ empty] closed have space: "P \<Omega>" by simp
-  interpret dynkin_system \<Omega> ?D
+  interpret Dynkin_system \<Omega> ?D
     by standard (auto dest: sets_into_space intro!: space compl union)
   have "sigma_sets \<Omega> G = ?D"
-    by (rule dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
+    by (rule Dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
   with A show ?thesis by auto
 qed
 
@@ -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"
diff -r 636b3c03a61a -r 8fd576a99a59 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Mon Dec 31 22:21:02 2018 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Mon Dec 31 22:21:34 2018 +0100
@@ -118,9 +118,9 @@
     and indep_setD_ev2: "B \<subseteq> events"
   using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
 
-lemma (in prob_space) indep_sets_dynkin:
+lemma (in prob_space) indep_sets_Dynkin:
   assumes indep: "indep_sets F I"
-  shows "indep_sets (\<lambda>i. dynkin (space M) (F i)) I"
+  shows "indep_sets (\<lambda>i. Dynkin (space M) (F i)) I"
     (is "indep_sets ?F I")
 proof (subst indep_sets_finite_index_sets, intro allI impI ballI)
   fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}"
@@ -178,8 +178,8 @@
           qed
         qed }
       note indep_sets_insert = this
-      have "dynkin_system (space M) ?D"
-      proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe)
+      have "Dynkin_system (space M) ?D"
+      proof (rule Dynkin_systemI', simp_all cong del: indep_sets_cong, safe)
         show "indep_sets (G(j := {{}})) K"
           by (rule indep_sets_insert) auto
       next
@@ -249,8 +249,8 @@
             by (auto dest!: sums_unique)
         qed (insert F, auto)
       qed (insert sets.sets_into_space, auto)
-      then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
-      proof (rule dynkin_system.dynkin_subset, safe)
+      then have mono: "Dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
+      proof (rule Dynkin_system.Dynkin_subset, safe)
         fix X assume "X \<in> G j"
         then show "X \<in> events" using G \<open>j \<in> K\<close> by auto
         from \<open>indep_sets G K\<close>
@@ -276,7 +276,7 @@
             by (intro indep_setsD[OF G(1)]) auto
         qed
       qed
-      then have "indep_sets (G(j := dynkin (space M) (G j))) K"
+      then have "indep_sets (G(j := Dynkin (space M) (G j))) K"
         by (rule indep_sets_mono_sets) (insert mono, auto)
       then show ?case
         by (rule indep_sets_mono_sets) (insert \<open>j \<in> K\<close> \<open>j \<notin> J\<close>, auto simp: G_def)
@@ -291,9 +291,9 @@
   assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)"
   shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
 proof -
-  from indep_sets_dynkin[OF indep]
+  from indep_sets_Dynkin[OF indep]
   show ?thesis
-  proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
+  proof (rule indep_sets_mono_sets, subst sigma_eq_Dynkin, simp_all add: stable)
     fix i assume "i \<in> I"
     with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
     with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
@@ -662,8 +662,8 @@
   have X_in: "X \<in> events"
     using tail_events_sets A X by auto
 
-  interpret D: dynkin_system "space M" ?D
-  proof (rule dynkin_systemI)
+  interpret D: Dynkin_system "space M" ?D
+  proof (rule Dynkin_systemI)
     fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
       using sets.sets_into_space by auto
   next
@@ -739,8 +739,8 @@
       by (intro sigma_sets_subseteq UN_mono) auto
    then have "tail_events A \<subseteq> sigma_sets (space M) ?A"
       unfolding tail_events_def by auto }
-  also have "sigma_sets (space M) ?A = dynkin (space M) ?A"
-  proof (rule sigma_eq_dynkin)
+  also have "sigma_sets (space M) ?A = Dynkin (space M) ?A"
+  proof (rule sigma_eq_Dynkin)
     { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
       then have "B \<subseteq> space M"
         by induct (insert A sets.sets_into_space[of _ M], auto) }
@@ -763,8 +763,8 @@
       then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto
     qed
   qed
-  also have "dynkin (space M) ?A \<subseteq> ?D"
-    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.dynkin_subset)
+  also have "Dynkin (space M) ?A \<subseteq> ?D"
+    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.Dynkin_subset)
   finally show ?thesis by auto
 qed