src/HOL/Analysis/Sigma_Algebra.thy

   subsets of the universe. A sigma algebra is such a set that has
   three very natural and desirable properties.\<close>
 
 subsection \<open>Families of sets\<close>
 
-locale%important subset_class =
+locale\<^marker>\<open>tag important\<close> subset_class =
   fixes \<Omega> :: "'a set" and M :: "'a set set"
   assumes space_closed: "M \<subseteq> Pow \<Omega>"
 
 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>"
   by (metis PowD contra_subsetD space_closed)
 
 subsubsection \<open>Semiring of sets\<close>
 
-locale%important semiring_of_sets = subset_class +
+locale\<^marker>\<open>tag important\<close> semiring_of_sets = subset_class +
   assumes empty_sets[iff]: "{} \<in> M"
   assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
   assumes Diff_cover:
     "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
 

   with assms show ?thesis by auto
 qed
 
 subsubsection \<open>Ring of sets\<close>
 
-locale%important ring_of_sets = semiring_of_sets +
+locale\<^marker>\<open>tag important\<close> ring_of_sets = semiring_of_sets +
   assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
 
 lemma (in ring_of_sets) finite_Union [intro]:
   "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M"
   by (induct set: finite) (auto simp add: Un)

   with assms show ?thesis by auto
 qed
 
 subsubsection \<open>Algebra of sets\<close>
 
-locale%important algebra = ring_of_sets +
+locale\<^marker>\<open>tag important\<close> algebra = ring_of_sets +
   assumes top [iff]: "\<Omega> \<in> M"
 
 lemma (in algebra) compl_sets [intro]:
   "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
   by auto

 
 lemma algebra_single_set:
   "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   by (auto simp: algebra_iff_Int)
 
-subsubsection%unimportant \<open>Restricted algebras\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Restricted algebras\<close>
 
 abbreviation (in algebra)
   "restricted_space A \<equiv> ((\<inter>) A) ` M"
 
 lemma (in algebra) restricted_algebra:
   assumes "A \<in> M" shows "algebra A (restricted_space A)"
   using assms by (auto simp: algebra_iff_Int)
 
 subsubsection \<open>Sigma Algebras\<close>
 
-locale%important sigma_algebra = algebra +
+locale\<^marker>\<open>tag important\<close> sigma_algebra = algebra +
   assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
 
 lemma (in algebra) is_sigma_algebra:
   assumes "finite M"
   shows "sigma_algebra \<Omega> M"

 lemma sigma_algebra_single_set:
   assumes "X \<subseteq> S"
   shows "sigma_algebra S { {}, X, S - X, S }"
   using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp
 
-subsubsection%unimportant \<open>Binary Unions\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Binary Unions\<close>
 
 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
   where "binary a b =  (\<lambda>x. b)(0 := a)"
 
 lemma range_binary_eq: "range(binary a b) = {a,b}"

 qed
 
 
 subsubsection \<open>Initial Sigma Algebra\<close>
 
-text%important \<open>Sigma algebras can naturally be created as the closure of any set of
+text\<^marker>\<open>tag important\<close> \<open>Sigma algebras can naturally be created as the closure of any set of
   M with regard to the properties just postulated.\<close>
 
-inductive_set%important sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+inductive_set\<^marker>\<open>tag important\<close> sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
   for sp :: "'a set" and A :: "'a set set"
   where
     Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
   | Empty: "{} \<in> sigma_sets sp A"
   | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"

   hence "(\<Union>i. disjointed A i) \<in> M"
     by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed)
   thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
 qed
 
-subsubsection%unimportant \<open>Ring generated by a semiring\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Ring generated by a semiring\<close>
 
 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?]:

     using space_closed by (rule sigma_algebra_sigma_sets)
   show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M"
     by (blast intro!: sigma_sets_mono elim: generated_ringE)
 qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
 
-subsubsection%unimportant \<open>A Two-Element Series\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>A Two-Element Series\<close>
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
   where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
 
 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"

 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 :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> 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) &

     by blast
 qed
 
 subsubsection \<open>Dynkin systems\<close>
 
-locale%important Dynkin_system = subset_class +
+locale\<^marker>\<open>tag important\<close> 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"
 

   show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI)
 qed
 
 subsubsection "Intersection sets systems"
 
-definition%important Int_stable :: "'a set set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> 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
 

   qed auto
 qed
 
 subsubsection "Smallest Dynkin systems"
 
-definition%important Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
+definition\<^marker>\<open>tag important\<close> 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)"

     using assms by (auto simp: Dynkin_def)
 qed
 
 subsubsection \<open>Induction rule for intersection-stable generators\<close>
 
-text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
+text\<^marker>\<open>tag important\<close> \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
 generated by a generator closed under intersection.\<close>
 
 proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
   assumes "Int_stable G"
     and closed: "G \<subseteq> Pow \<Omega>"

   with A show ?thesis by auto
 qed
 
 subsection \<open>Measure type\<close>
 
-definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> 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
+definition\<^marker>\<open>tag important\<close> 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>
     (\<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
+definition\<^marker>\<open>tag important\<close> 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 =
+typedef\<^marker>\<open>tag important\<close> 'a measure =
   "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
-proof%unimportant
+proof
   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)
 qed
 
-definition%important space :: "'a measure \<Rightarrow> 'a set" where
+definition\<^marker>\<open>tag important\<close> space :: "'a measure \<Rightarrow> 'a set" where
   "space M = fst (Rep_measure M)"
 
-definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
+definition\<^marker>\<open>tag important\<close> sets :: "'a measure \<Rightarrow> 'a set set" where
   "sets M = fst (snd (Rep_measure M))"
 
-definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition\<^marker>\<open>tag important\<close> emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
   "emeasure M = snd (snd (Rep_measure M))"
 
-definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
+definition\<^marker>\<open>tag important\<close> measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
   "measure M A = enn2real (emeasure M A)"
 
 declare [[coercion sets]]
 
 declare [[coercion measure]]

   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"
+definition\<^marker>\<open>tag important\<close> 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)"
 

   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"
+definition\<^marker>\<open>tag important\<close> 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>

     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
   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
+definition\<^marker>\<open>tag important\<close> 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>)"
 
 lemma
   shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
     and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"

 
 lemma measurable_empty_iff:
   "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>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Extend measure\<close>
 
 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)

   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 \<open>\<sigma>\<close>-algebra regarding a function\<close>
 
-definition%important vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
+definition\<^marker>\<open>tag important\<close> 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