Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/ZF/UNITY/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 8 kB

SSL Sigma_Algebra.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Sigma_Algebra.thy
    Author:     Stefan Richter, Markus Wenzel, TU München
    Author:     Johannes Hölzl, TU München
    Plus material from the Hurd/Coble measure theory development,
    translated by Lawrence Paulson.
*)

chapter \<open>Measure and Integration Theory\<close>

theory Sigma_Algebra
imports
  Complex_Main
  "HOL-Library.Countable_Set"
  "HOL-Library.FuncSet"
  "HOL-Library.Indicator_Function"
  "HOL-Library.Extended_Nonnegative_Real"
  "HOL-Library.Disjoint_Sets"
begin

section \<open>Sigma Algebra\<close>

text \<open>Sigma algebras are an elementary concept in measure
  theory. To measure --- that is to integrate --- functions, we first have
  to measure sets. Unfortunately, when dealing with a large universe,
  it is often not possible to consistently assign a measure to every
  subset. Therefore it is necessary to define the set of measurable
  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\<^marker>\<open>tag important\<close> subset_class =
  fixes \<Omega> :: "'a set" and M :: "'a set set"
  assumes space_closed: "M \ Pow \"

lemma (in subset_class) sets_into_space: "x \ M \ x \ \"
  by (metis PowD contra_subsetD space_closed)

subsubsection \<open>Semiring of sets\<close>

locale\<^marker>\<open>tag important\<close> semiring_of_sets = subset_class +
  assumes empty_sets[iff]: "{} \ M"
  assumes Int[intro]: "\a b. a \ M \ b \ M \ a \ b \ M"
  assumes Diff_cover:
    "\a b. a \ M \ b \ M \ \C\M. finite C \ disjoint C \ a - b = \C"

lemma (in semiring_of_sets) finite_INT[intro]:
  assumes "finite I" "I \ {}" "\i. i \ I \ A i \ M"
  shows "(\i\I. A i) \ M"
  using assms by (induct rule: finite_ne_induct) auto

lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \ M \ \ \ x = x"
  by (metis Int_absorb1 sets_into_space)

lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \ M \ x \ \ = x"
  by (metis Int_absorb2 sets_into_space)

lemma (in semiring_of_sets) sets_Collect_conj:
  assumes "{x\\. P x} \ M" "{x\\. Q x} \ M"
  shows "{x\\. Q x \ P x} \ M"
proof -
  have "{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}"
    by auto
  with assms show ?thesis by auto
qed

lemma (in semiring_of_sets) sets_Collect_finite_All':
  assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S" "S \ {}"
  shows "{x\\. \i\S. P i x} \ M"
proof -
  have "{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})"
    using \<open>S \<noteq> {}\<close> by auto
  with assms show ?thesis by auto
qed

subsubsection \<open>Ring of sets\<close>

locale\<^marker>\<open>tag important\<close> ring_of_sets = semiring_of_sets +
  assumes Un [intro]: "\a b. a \ M \ b \ M \ a \ b \ M"

lemma (in ring_of_sets) finite_Union [intro]:
  "finite X \ X \ M \ \X \ M"
  by (induct set: finite) (auto simp add: Un)

lemma (in ring_of_sets) finite_UN[intro]:
  assumes "finite I" and "\i. i \ I \ A i \ M"
  shows "(\i\I. A i) \ M"
  using assms by induct auto

lemma (in ring_of_sets) Diff [intro]:
  assumes "a \ M" "b \ M" shows "a - b \ M"
  using Diff_cover[OF assms] by auto

lemma ring_of_setsI:
  assumes space_closed: "M \ Pow \"
  assumes empty_sets[iff]: "{} \ M"
  assumes Un[intro]: "\a b. a \ M \ b \ M \ a \ b \ M"
  assumes Diff[intro]: "\a b. a \ M \ b \ M \ a - b \ M"
  shows "ring_of_sets \ M"
proof
  fix a b assume ab: "a \ M" "b \ M"
  from ab show "\C\M. finite C \ disjoint C \ a - b = \C"
    by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def)
  have "a \ b = a - (a - b)" by auto
  also have "\ \ M" using ab by auto
  finally show "a \ b \ M" .
qed fact+

lemma ring_of_sets_iff: "ring_of_sets \ M \ M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \ b \ M) \ (\a\M. \b\M. a - b \ M)"
proof
  assume "ring_of_sets \ M"
  then interpret ring_of_sets \<Omega> M .
  show "M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \ b \ M) \ (\a\M. \b\M. a - b \ M)"
    using space_closed by auto
qed (auto intro!: ring_of_setsI)

lemma (in ring_of_sets) insert_in_sets:
  assumes "{x} \ M" "A \ M" shows "insert x A \ M"
proof -
  have "{x} \ A \ M" using assms by (rule Un)
  thus ?thesis by auto
qed

lemma (in ring_of_sets) sets_Collect_disj:
  assumes "{x\\. P x} \ M" "{x\\. Q x} \ M"
  shows "{x\\. Q x \ P x} \ M"
proof -
  have "{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}"
    by auto
  with assms show ?thesis by auto
qed

lemma (in ring_of_sets) sets_Collect_finite_Ex:
  assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S"
  shows "{x\\. \i\S. P i x} \ M"
proof -
  have "{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})"
    by auto
  with assms show ?thesis by auto
qed

subsubsection \<open>Algebra of sets\<close>

locale\<^marker>\<open>tag important\<close> algebra = ring_of_sets +
  assumes top [iff]: "\ \ M"

lemma (in algebra) compl_sets [intro]:
  "a \ M \ \ - a \ M"
  by auto

proposition algebra_iff_Un:
  "algebra \ M \
    M \<subseteq> Pow \<Omega> \<and>
    {} \<in> M \<and>
    (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
    (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
proof
  assume "algebra \ M"
  then interpret algebra \<Omega> M .
  show ?Un using sets_into_space by auto
next
  assume ?Un
  then have "\ \ M" by auto
  interpret ring_of_sets \<Omega> M
  proof (rule ring_of_setsI)
    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
      using \<open>?Un\<close> by auto
    fix a b assume a: "a \ M" and b: "b \ M"
    then show "a \ b \ M" using \?Un\ by auto
    have "a - b = \ - ((\ - a) \ b)"
      using \<Omega> a b by auto
    then show "a - b \ M"
      using a b  \<open>?Un\<close> by auto
  qed
  show "algebra \ M" proof qed fact
qed

proposition algebra_iff_Int:
     "algebra \ M \
       M \<subseteq> Pow \<Omega> & {} \<in> M &
       (\<forall>a \<in> M. \<Omega> - a \<in> M) &
       (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
proof
  assume "algebra \ M"
  then interpret algebra \<Omega> M .
  show ?Int using sets_into_space by auto
next
  assume ?Int
  show "algebra \ M"
    unfolding algebra_iff_Un
  proof (intro conjI ballI)
    show \<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M"
      using \<open>?Int\<close> by auto
    from \<open>?Int\<close> show "\<And>a. a \<in> M \<Longrightarrow> \<Omega> - a \<in> M" by auto
    fix a b assume M: "a \ M" "b \ M"
    hence "a \ b = \ - ((\ - a) \ (\ - b))"
      using \<Omega> by blast
    also have "... \ M"
      using M \<open>?Int\<close> by auto
    finally show "a \ b \ M" .
  qed
qed

lemma (in algebra) sets_Collect_neg:
  assumes "{x\\. P x} \ M"
  shows "{x\\. \ P x} \ M"
proof -
  have "{x\\. \ P x} = \ - {x\\. P x}" by auto
  with assms show ?thesis by auto
qed

lemma (in algebra) sets_Collect_imp:
  "{x\\. P x} \ M \ {x\\. Q x} \ M \ {x\\. Q x \ P x} \ M"
  unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)

lemma (in algebra) sets_Collect_const:
  "{x\\. P} \ M"
  by (cases P) auto

lemma algebra_single_set:
  "X \ S \ algebra S { {}, X, S - X, S }"
  by (auto simp: algebra_iff_Int)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Restricted algebras\<close>

abbreviation (in algebra)
  "restricted_space A \ ((\) A) ` M"

lemma (in algebra) restricted_algebra:
  assumes "A \ M" shows "algebra A (restricted_space A)"
  using assms by (auto simp: algebra_iff_Int)

subsubsection \<open>Sigma Algebras\<close>

locale\<^marker>\<open>tag important\<close> sigma_algebra = algebra +
  assumes countable_nat_UN [intro]: "\A. range A \ M \ (\i::nat. A i) \ M"

lemma (in algebra) is_sigma_algebra:
  assumes "finite M"
  shows "sigma_algebra \ M"
proof
  fix A :: "nat \ 'a set" assume "range A \ M"
  then have "(\i. A i) = (\s\M \ range A. s)"
    by auto
  also have "(\s\M \ range A. s) \ M"
    using \<open>finite M\<close> by auto
  finally show "(\i. A i) \ M" .
qed

lemma countable_UN_eq:
  fixes A :: "'i::countable \ 'a set"
  shows "(range A \ M \ (\i. A i) \ M) \
    (range (A \<circ> from_nat) \<subseteq> M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> M)"
proof -
  let ?A' = "A \ from_nat"
  have *: "(\i. ?A' i) = (\i. A i)"
    by (metis fun.set_map surj_from_nat)
  have "A ` range from_nat = range A"
    using surj_from_nat by simp
  then have **: "range ?A' = range A"
    by (metis image_comp)
  show ?thesis unfolding * ** ..
qed

lemma (in sigma_algebra) countable_Union [intro]:
  assumes "countable X" "X \ M" shows "\X \ M"
proof cases
  assume "X \ {}"
  hence "\X = (\n. from_nat_into X n)"
    using assms by (auto cong del: SUP_cong)
  also have "\ \ M" using assms
    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD)
  finally show ?thesis .
qed simp

lemma (in sigma_algebra) countable_UN[intro]:
  fixes A :: "'i::countable \ 'a set"
  assumes "A`X \ M"
  shows  "(\x\X. A x) \ M"
proof -
  let ?A = "\i. if i \ X then A i else {}"
  from assms have "range ?A \ M" by auto
  with countable_nat_UN[of "?A \ from_nat"] countable_UN_eq[of ?A M]
  have "(\x. ?A x) \ M" by auto
  moreover have "(\x. ?A x) = (\x\X. A x)" by (auto split: if_split_asm)
  ultimately show ?thesis by simp
qed

lemma (in sigma_algebra) countable_UN':
  fixes A :: "'i \ 'a set"
  assumes X: "countable X"
  assumes A: "A`X \ M"
  shows  "(\x\X. A x) \ M"
  using A X countable_Union countable_image by blast

lemma (in sigma_algebra) countable_UN'':
  "\ countable X; \x y. x \ X \ A x \ M \ \ (\x\X. A x) \ M"
  by blast

lemma (in sigma_algebra) countable_INT [intro]:
  fixes A :: "'i::countable \ 'a set"
  assumes A: "A`X \ M" "X \ {}"
  shows "(\i\X. A i) \ M"
proof -
  from A have "\i\X. A i \ M" by fast
  hence "\ - (\i\X. \ - A i) \ M" by blast
  moreover
  have "(\i\X. A i) = \ - (\i\X. \ - A i)" using space_closed A
    by blast
  ultimately show ?thesis by metis
qed

lemma (in sigma_algebra) countable_INT':
  fixes A :: "'i \ 'a set"
  assumes X: "countable X" "X \ {}"
  assumes A: "A`X \ M"
  shows  "(\x\X. A x) \ M"
proof -
  have "(\x\X. A x) = (\i\to_nat_on X ` X. A (from_nat_into X i))"
    using X by auto
  also have "\ \ M"
    using A X by (intro countable_INT) auto
  finally show ?thesis .
qed

lemma (in sigma_algebra) countable_INT'':
  "UNIV \ M \ countable I \ (\i. i \ I \ F i \ M) \ (\i\I. F i) \ M"
  by (cases "I = {}") (auto intro: countable_INT')

lemma (in sigma_algebra) countable:
  assumes "\a. a \ A \ {a} \ M" "countable A"
  shows "A \ M"
proof -
  have "(\a\A. {a}) \ M"
    using assms by (intro countable_UN') auto
  also have "(\a\A. {a}) = A" by auto
  finally show ?thesis by auto
qed

lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
  by (auto simp: ring_of_sets_iff)

lemma algebra_Pow: "algebra sp (Pow sp)"
  by (auto simp: algebra_iff_Un)

lemma sigma_algebra_iff:
  "sigma_algebra \ M \ algebra \ M \ (\A. range A \ M \ (\i::nat. A i) \ M)"
  by (simp add: sigma_algebra_def sigma_algebra_axioms_def)

lemma sigma_algebra_Pow: "sigma_algebra sp (Pow sp)"
  by (auto simp: sigma_algebra_iff algebra_iff_Int)

lemma (in sigma_algebra) sets_Collect_countable_All:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable. P i x} \ M"
proof -
  have "{x\\. \i. P i x} = (\i. {x\\. P i x})" by auto
  with assms show ?thesis by auto
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable. P i x} \ M"
proof -
  have "{x\\. \i. P i x} = (\i. {x\\. P i x})" by auto
  with assms show ?thesis by auto
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \i\I. P i x} \ M"
proof -
  have "{x\\. \i\I. P i x} = (\i\I. {x\\. P i x})" by auto
  with assms show ?thesis
    by (auto intro!: countable_UN')
qed

lemma (in sigma_algebra) sets_Collect_countable_All':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \i\I. P i x} \ M"
proof -
  have "{x\\. \i\I. P i x} = (\i\I. {x\\. P i x}) \ \" by auto
  with assms show ?thesis
    by (cases "I = {}") (auto intro!: countable_INT')
qed

lemma (in sigma_algebra) sets_Collect_countable_Ex1':
  assumes "\i. i \ I \ {x\\. P i x} \ M"
  assumes "countable I"
  shows "{x\\. \!i\I. P i x} \ M"
proof -
  have "{x\\. \!i\I. P i x} = {x\\. \i\I. P i x \ (\j\I. P j x \ i = j)}"
    by auto
  with assms show ?thesis
    by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const)
qed

lemmas (in sigma_algebra) sets_Collect =
  sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
  sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All

lemma (in sigma_algebra) sets_Collect_countable_Ball:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable\X. P i x} \ M"
  unfolding Ball_def by (intro sets_Collect assms)

lemma (in sigma_algebra) sets_Collect_countable_Bex:
  assumes "\i. {x\\. P i x} \ M"
  shows "{x\\. \i::'i::countable\X. P i x} \ M"
  unfolding Bex_def by (intro sets_Collect assms)

lemma sigma_algebra_single_set:
  assumes "X \ 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\<^marker>\<open>tag unimportant\<close> \<open>Binary Unions\<close>

definition binary :: "'a \ 'a \ nat \ 'a"
  where "binary a b = (\x. b)(0 := a)"

lemma range_binary_eq: "range(binary a b) = {a,b}"
  by (auto simp add: binary_def)

lemma Un_range_binary: "a \ b = (\i::nat. binary a b i)"
  by (simp add: range_binary_eq cong del: SUP_cong_simp)

lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)"
  by (simp add: range_binary_eq cong del: INF_cong_simp)

lemma sigma_algebra_iff2:
  "sigma_algebra \ M \
    M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M)
    \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow>(\<Union> i::nat. A i) \<in> M)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?V \<and> ?W")
proof
  assume ?P
  then interpret sigma_algebra \<Omega> M .
  from space_closed show "?R \ ?S \ ?V \ ?W"
    by auto
next
  assume "?R \ ?S \ ?V \ ?W"
  then have ?R ?S ?V ?W
    by simp_all
  show ?P
  proof (rule sigma_algebra.intro)
    show "sigma_algebra_axioms M"
      using \<open>?W\<close> sigma_algebra_axioms_def by blast
    from \<open>?W\<close> have *: "range (binary a b) \<subseteq> M \<Longrightarrow> \<Union> (range (binary a b)) \<in> M" for a b
      by auto
    show "algebra \ M"
      unfolding algebra_iff_Un using \<open>?R\<close> \<open>?S\<close> \<open>?V\<close> *
      by (auto simp add: range_binary_eq)
  qed
qed

subsubsection \<open>Initial Sigma Algebra\<close>

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\<^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 \ A \ a \ sigma_sets sp A"
  | Empty: "{} \ sigma_sets sp A"
  | Compl: "a \ sigma_sets sp A \ sp - a \ sigma_sets sp A"
  | Union: "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A"

lemma (in sigma_algebra) sigma_sets_subset:
  assumes a: "a \ M"
  shows "sigma_sets \ a \ M"
proof
  fix x
  assume "x \ sigma_sets \ a"
  then show "x \ M"
    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
qed

lemma sigma_sets_into_sp: "A \ Pow sp \ x \ sigma_sets sp A \ x \ sp"
  by (erule sigma_sets.induct, auto)

lemma sigma_sets_finite: "\x \ sigma_sets \ (Pow \); finite \\ \ finite x"
  by (meson finite_subset order.refl sigma_sets_into_sp)

lemma sigma_algebra_sigma_sets:
     "a \ Pow \ \ sigma_algebra \ (sigma_sets \ a)"
  by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
           intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)

lemma sigma_sets_least_sigma_algebra:
  assumes "A \ Pow S"
  shows "sigma_sets S A = \{B. A \ B \ sigma_algebra S B}"
proof safe
  fix B X assume "A \ B" and sa: "sigma_algebra S B"
    and X: "X \ sigma_sets S A"
  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF \<open>A \<subseteq> B\<close>] X
  show "X \ B" by auto
next
  fix X assume "X \ \{B. A \ B \ sigma_algebra S B}"
  then have [intro!]: "\B. A \ B \ sigma_algebra S B \ X \ B"
     by simp
  have "A \ sigma_sets S A" using assms by auto
  moreover have "sigma_algebra S (sigma_sets S A)"
    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
  ultimately show "X \ sigma_sets S A" by auto
qed

lemma sigma_sets_top: "sp \ sigma_sets sp A"
  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)

lemma binary_in_sigma_sets:
  "binary a b i \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A"
  using that by (simp add: binary_def)

lemma sigma_sets_Un:
  "a \ b \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A"
  using that by (simp add: Un_range_binary binary_in_sigma_sets Union)

lemma sigma_sets_Inter:
  assumes Asb: "A \ Pow sp"
  shows "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A"
proof -
  assume ai: "\i::nat. a i \ sigma_sets sp A"
  hence "\i::nat. sp-(a i) \ sigma_sets sp A"
    by (rule sigma_sets.Compl)
  hence "(\i. sp-(a i)) \ sigma_sets sp A"
    by (rule sigma_sets.Union)
  hence "sp-(\i. sp-(a i)) \ sigma_sets sp A"
    by (rule sigma_sets.Compl)
  also have "sp-(\i. sp-(a i)) = sp Int (\i. a i)"
    by auto
  also have "... = (\i. a i)" using ai
    by (blast dest: sigma_sets_into_sp [OF Asb])
  finally show ?thesis .
qed

lemma sigma_sets_INTER:
  assumes Asb: "A \ Pow sp"
      and ai: "\i::nat. i \ S \ a i \ sigma_sets sp A" and non: "S \ {}"
  shows "(\i\S. a i) \ sigma_sets sp A"
proof -
  from ai have "\i. (if i\S then a i else sp) \ sigma_sets sp A"
    by (simp add: sigma_sets.intros(2-) sigma_sets_top)
  hence "(\i. (if i\S then a i else sp)) \ sigma_sets sp A"
    by (rule sigma_sets_Inter [OF Asb])
  also have "(\i. (if i\S then a i else sp)) = (\i\S. a i)"
    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
  finally show ?thesis .
qed

lemma sigma_sets_UNION:
  "countable B \ (\b. b \ B \ b \ sigma_sets X A) \ \ B \ sigma_sets X A"
  using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A]
  by (cases "B = {}") (simp_all add: sigma_sets.Empty cong del: SUP_cong)

lemma (in sigma_algebra) sigma_sets_eq: "sigma_sets \ M = M"
  using sigma_sets_subset by blast

lemma sigma_sets_eqI:
  assumes A: "\a. a \ A \ a \ sigma_sets M B"
  assumes B: "\b. b \ B \ b \ sigma_sets M A"
  shows "sigma_sets M A = sigma_sets M B"
proof (intro set_eqI iffI)
  fix a assume "a \ sigma_sets M A"
  from this A show "a \ sigma_sets M B"
    by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic)
next
  fix b assume "b \ sigma_sets M B"
  from this B show "b \ sigma_sets M A"
    by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic)
qed

lemma sigma_sets_subseteq:
  assumes "A \ B"
  shows "sigma_sets X A \ sigma_sets X B"
proof
  fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B"
    by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-))
qed

lemma sigma_sets_mono:
  assumes "A \ sigma_sets X B"
  shows "sigma_sets X A \ sigma_sets X B"
proof
  fix x assume "x \ sigma_sets X A"
  then show "x \ sigma_sets X B"
    by induct (insert \<open>A \<subseteq> sigma_sets X B\<close>, auto intro: sigma_sets.intros(2-))
qed

lemma sigma_sets_mono':
  assumes "A \ B"
  shows "sigma_sets X A \ sigma_sets X B"
  by (simp add: assms sigma_sets_subseteq)

lemma sigma_sets_superset_generator: "A \ sigma_sets X A"
  by auto

lemma (in sigma_algebra) restriction_in_sets:
  fixes A :: "nat \ 'a set"
  assumes "S \ M"
  and *: "range A \ (\A. S \ A) ` M" (is "_ \ ?r")
  shows "range A \ M" "(\i. A i) \ (\A. S \ A) ` M"
proof -
  { fix i have "A i \ ?r" using * by auto
    hence "\B. A i = B \ S \ B \ M" by auto
    hence "A i \ S" "A i \ M" using \S \ M\ by auto }
  thus "range A \ M" "(\i. A i) \ (\A. S \ A) ` M"
    by (auto intro!: image_eqI[of _ _ "(\i. A i)"])
qed

lemma (in sigma_algebra) restricted_sigma_algebra:
  assumes "S \ M"
  shows "sigma_algebra S (restricted_space S)"
  unfolding sigma_algebra_def sigma_algebra_axioms_def
  using assms restricted_algebra restriction_in_sets(2) by presburger

lemma sigma_sets_Int:
  assumes "A \ sigma_sets sp st" "A \ sp"
  shows "(\) A ` sigma_sets sp st = sigma_sets A ((\) A ` st)"
proof (intro equalityI subsetI)
  fix x assume "x \ (\) A ` sigma_sets sp st"
  then obtain y where "y \ sigma_sets sp st" "x = y \ A" by auto
  then have "x \ sigma_sets (A \ sp) ((\) A ` st)"
  proof (induct arbitrary: x)
    case (Compl a)
    then show ?case
      by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps)
  next
    case (Union a)
    then show ?case
      by (auto intro!: sigma_sets.Union
               simp add: UN_extend_simps simp del: UN_simps)
  qed (auto intro!: sigma_sets.intros(2-))
  then show "x \ sigma_sets A ((\) A ` st)"
    using \<open>A \<subseteq> sp\<close> by (simp add: Int_absorb2)
next
  fix x assume "x \ sigma_sets A ((\) A ` st)"
  then show "x \ (\) A ` sigma_sets sp st"
  proof induct
    case (Compl a)
    then obtain x where "a = A \ x" "x \ sigma_sets sp st" by auto
    then show ?case using \<open>A \<subseteq> sp\<close>
      by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl)
  next
    case (Union a)
    then have "\i. \x. x \ sigma_sets sp st \ a i = A \ x"
      by (auto simp: image_iff Bex_def)
    then obtain f where "\x. f x \ sigma_sets sp st \ a x = A \ f x"
      by metis
    then show ?case
      by (auto intro!: bexI[of _ "(\x. f x)"] sigma_sets.Union
               simp add: image_iff)
  qed (auto intro!: sigma_sets.intros(2-))
qed

lemma sigma_sets_empty_eq: "sigma_sets A {} = {{}, A}"
proof (intro set_eqI iffI)
  fix a assume "a \ sigma_sets A {}" then show "a \ {{}, A}"
    by induct blast+
qed (auto intro: sigma_sets.Empty sigma_sets_top)

lemma sigma_sets_single[simp]: "sigma_sets A {A} = {{}, A}"
proof (intro set_eqI iffI)
  fix x assume "x \ sigma_sets A {A}"
  then show "x \ {{}, A}"
    by induct blast+
next
  fix x assume "x \ {{}, A}"
  then show "x \ sigma_sets A {A}"
    by (auto intro: sigma_sets.Empty sigma_sets_top)
qed

lemma sigma_sets_sigma_sets_eq:
  "M \ Pow S \ sigma_sets S (sigma_sets S M) = sigma_sets S M"
  by (rule sigma_algebra.sigma_sets_eq[OF sigma_algebra_sigma_sets, of M S]) auto

lemma sigma_sets_singleton:
  assumes "X \ S"
  shows "sigma_sets S { X } = { {}, X, S - X, S }"
proof -
  interpret sigma_algebra S "{ {}, X, S - X, S }"
    by (rule sigma_algebra_single_set) fact
  have "sigma_sets S { X } \ sigma_sets S { {}, X, S - X, S }"
    by (rule sigma_sets_subseteq) simp
  moreover have "\ = { {}, X, S - X, S }"
    using sigma_sets_eq by simp
  moreover
  { fix A assume "A \ { {}, X, S - X, S }"
    then have "A \ sigma_sets S { X }"
      by (auto intro: sigma_sets.intros(2-) sigma_sets_top) }
  ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }"
    by (intro antisym) auto
  with sigma_sets_eq show ?thesis by simp
qed

lemma restricted_sigma:
  assumes S: "S \ sigma_sets \ M" and M: "M \ Pow \"
  shows "algebra.restricted_space (sigma_sets \ M) S = sigma_sets S (algebra.restricted_space M S)"
  by (meson M S sigma_sets_Int sigma_sets_into_sp)

lemma sigma_sets_vimage_commute:
  assumes X: "X \ \ \ \'"
  shows "{X -` A \ \ |A. A \ sigma_sets \' M'}
       = sigma_sets \<Omega> {X -` A \<inter> \<Omega> |A. A \<in> M'}" (is "?L = ?R")
proof
  show "?L \ ?R"
  proof clarify
    fix A assume "A \ sigma_sets \' M'"
    then show "X -` A \ \ \ ?R"
    proof induct
      case Empty then show ?case
        by (auto intro!: sigma_sets.Empty)
    next
      case (Compl B)
      have [simp]: "X -` (\' - B) \ \ = \ - (X -` B \ \)"
        by (auto simp add: funcset_mem [OF X])
      with Compl show ?case
        by (auto intro!: sigma_sets.Compl)
    next
      case (Union F)
      then show ?case
        by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
                 intro!: sigma_sets.Union)
    qed auto
  qed
  show "?R \ ?L"
  proof clarify
    fix A assume "A \ ?R"
    then show "\B. A = X -` B \ \ \ B \ sigma_sets \' M'"
    proof induct
      case (Basic B) then show ?case by auto
    next
      case Empty then show ?case
        by (auto intro!: sigma_sets.Empty exI[of _ "{}"])
    next
      case (Compl B)
      then obtain A where A: "B = X -` A \ \" "A \ sigma_sets \' M'" by auto
      then have [simp]: "\ - B = X -` (\' - A) \ \"
        by (auto simp add: funcset_mem [OF X])
      with A(2) show ?case
        by (auto intro: sigma_sets.Compl)
    next
      case (Union F)
      then have "\i. \B. F i = X -` B \ \ \ B \ sigma_sets \' M'" by auto
      then obtain A where "\x. F x = X -` A x \ \ \ A x \ sigma_sets \' M'"
        by metis
      then show ?case
        by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union)
    qed
  qed
qed

lemma (in ring_of_sets) UNION_in_sets:
  fixes A:: "nat \ 'a set"
  assumes A: "range A \ M"
  shows  "(\i\{0.. M"
proof (induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  thus ?case
    using assms by blast
qed

lemma (in ring_of_sets) range_disjointed_sets:
  assumes A: "range A \ M"
  shows  "range (disjointed A) \ M"
proof -
  have "A n - (\i\{0.. M" for n
    using UNION_in_sets by (metis A Diff UNIV_I image_subset_iff)
  then show ?thesis
    by (auto simp: disjointed_def)
qed

lemma (in algebra) range_disjointed_sets':
  "range A \ M \ range (disjointed A) \ M"
  using range_disjointed_sets .

lemma sigma_algebra_disjoint_iff:
  "sigma_algebra \ M \ algebra \ M \
    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
proof (auto simp add: sigma_algebra_iff)
  fix A :: "nat \ 'a set"
  assume M: "algebra \ M"
     and A: "range A \ M"
     and UnA: "\A. range A \ M \ disjoint_family A \ (\i::nat. A i) \ M"
  hence "range (disjointed A) \ M \
         disjoint_family (disjointed A) \<longrightarrow>
         (\<Union>i. disjointed A i) \<in> M" by blast
  hence "(\i. disjointed A i) \ M"
    by (simp add: algebra.range_disjointed_sets'[of \] M A disjoint_family_disjointed)
  thus "(\i::nat. A i) \ M" by (simp add: UN_disjointed_eq)
qed

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 = { \C | C. C \ M \ finite C \ disjoint C }"

lemma (in semiring_of_sets) generated_ringE[elim?]:
  assumes "a \ generated_ring"
  obtains C where "finite C" "disjoint C" "C \ M" "a = \C"
  using assms unfolding generated_ring_def by auto

lemma (in semiring_of_sets) generated_ringI[intro?]:
  assumes "finite C" "disjoint C" "C \ M" "a = \C"
  shows "a \ generated_ring"
  using assms unfolding generated_ring_def by auto

lemma (in semiring_of_sets) generated_ringI_Basic:
  "A \ M \ A \ generated_ring"
  using generated_ring_def by auto

lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]:
  assumes a: "a \ generated_ring" and b: "b \ generated_ring"
  and "a \ b = {}"
  shows "a \ b \ generated_ring"
proof -
  from a b obtain Ca Cb
    where "finite Ca" "disjoint Ca" "Ca \ M" "a = \ Ca"
      and "finite Cb" "disjoint Cb" "Cb \ M" "b = \ Cb"
    using generated_ringE by metis
  then show ?thesis
    by (metis (mono_tags) Union_Un_distrib
        \<open>a \<inter> b = {}\<close> disjoint_union finite_Un generated_ringI le_sup_iff)
qed

lemma (in semiring_of_sets) generated_ring_empty: "{} \ generated_ring"
  by (auto simp: generated_ring_def disjoint_def)

lemma (in semiring_of_sets) generated_ring_disjoint_Union:
  assumes "finite A" shows "A \ generated_ring \ disjoint A \ \A \ generated_ring"
  using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)

lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
  "finite I \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring"
  by (intro generated_ring_disjoint_Union) auto

lemma (in semiring_of_sets) generated_ring_Int:
  assumes a: "a \ generated_ring" and b: "b \ generated_ring"
  shows "a \ b \ generated_ring"
proof -
  from a b obtain Ca Cb
    where Ca: "finite Ca" "disjoint Ca" "Ca \ M" "a = \ Ca"
      and Cb: "finite Cb" "disjoint Cb" "Cb \ M" "b = \ Cb"
    using generated_ringE by metis
  define C where "C = (\(a,b). a \ b)` (Ca\Cb)"
  show ?thesis
  proof
    show "disjoint C"
    proof (simp add: disjoint_def C_def, intro ballI impI)
      fix a1 b1 a2 b2
      assume sets: "a1 \ Ca" "b1 \ Cb" "a2 \ Ca" "b2 \ Cb"
      assume "a1 \ b1 \ a2 \ b2"
      then have "a1 \ a2 \ b1 \ b2" by auto
      with Ca Cb show "(a1 \ b1) \ (a2 \ b2) = {}"
        by (metis (no_types, opaque_lifting) boolean_algebra.conj_zero_left
            disjoint_def inf.left_commute inf_assoc sets)
    qed
  qed (use Ca Cb in \<open>auto simp: C_def\<close>)
qed

lemma (in semiring_of_sets) generated_ring_Inter:
  assumes "finite A" "A \ {}" shows "A \ generated_ring \ \A \ generated_ring"
  using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)

lemma (in semiring_of_sets) generated_ring_INTER:
  "finite I \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring"
  by (intro generated_ring_Inter) auto

lemma (in semiring_of_sets) generating_ring:
  "ring_of_sets \ generated_ring"
proof (rule ring_of_setsI)
  let ?R = generated_ring
  show "?R \ Pow \"
    using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
  show "{} \ ?R" by (rule generated_ring_empty)

  {
    fix a b assume "a \ ?R" "b \ ?R"
    then obtain Ca Cb
      where Ca: "finite Ca" "disjoint Ca" "Ca \ M" "a = \ Ca"
        and Cb: "finite Cb" "disjoint Cb" "Cb \ M" "b = \ Cb"
      using generated_ringE by metis
    show "a - b \ ?R"
    proof cases
      assume "Cb = {}" with Cb \<open>a \<in> ?R\<close> show ?thesis
        by simp
    next
      assume "Cb \ {}"
      with Ca Cb have "a - b = (\a'\Ca. \b'\Cb. a' - b')" by auto
      also have "\ \ ?R"
      proof (intro generated_ring_INTER generated_ring_disjoint_UNION)
        fix a b assume "a \ Ca" "b \ Cb"
        with Ca Cb Diff_cover[of a b] show "a - b \ ?R"
          by (auto simp add: generated_ring_def)
            (metis DiffI Diff_eq_empty_iff empty_iff)
      next
        show "disjoint ((\a'. \b'\Cb. a' - b')`Ca)"
          using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>)
      next
        show "finite Ca" "finite Cb" "Cb \ {}" by fact+
      qed
      finally show "a - b \ ?R" .
    qed
  }
  note Diff = this

  fix a b assume sets: "a \ ?R" "b \ ?R"
  have "a \ b = (a - b) \ (a \ b) \ (b - a)" by auto
  also have "\ \ ?R"
    by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto
  finally show "a \ b \ ?R" .
qed

lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \ generated_ring = sigma_sets \ M"
proof
  interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M"
    using space_closed by (rule sigma_algebra_sigma_sets)
  show "sigma_sets \ generated_ring \ sigma_sets \ M"
    by (blast intro!: sigma_sets_mono elim: generated_ringE)
qed (auto intro!: generated_ringI_Basic sigma_sets_mono)

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>A Two-Element Series\<close>

definition binaryset :: "'a set \ 'a set \ nat \ 'a set"
  where "binaryset A B = (\x. {})(0 := A, Suc 0 := B)"

lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
  by (auto simp add: binaryset_def)

lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B"
  by (simp add: range_binaryset_eq cong del: SUP_cong_simp)

subsubsection \<open>Closed CDI\<close>

definition\<^marker>\<open>tag important\<close> closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
  "closed_cdi \ M \
   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) &
   (\<forall>A. (range A \<subseteq> M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"

inductive_set
  smallest_ccdi_sets :: "'a set \ 'a set set \ 'a set set"
  for \<Omega> M
  where
    Basic [intro]:
      "a \ M \ a \ smallest_ccdi_sets \ M"
  | Compl [intro]:
      "a \ smallest_ccdi_sets \ M \ \ - a \ smallest_ccdi_sets \ M"
  | Inc:
      "range A \ Pow(smallest_ccdi_sets \ M) \ A 0 = {} \ (\n. A n \ A (Suc n))
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets \<Omega> M"
  | Disj:
      "range A \ Pow(smallest_ccdi_sets \ M) \ disjoint_family A
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets \<Omega> M"

lemma (in subset_class) smallest_closed_cdi1: "M \ smallest_ccdi_sets \ M"
  by auto

lemma (in subset_class) smallest_ccdi_sets: "smallest_ccdi_sets \ M \ Pow \"
  apply (rule subsetI)
  apply (erule smallest_ccdi_sets.induct)
  apply (auto intro: range_subsetD dest: sets_into_space)
  done

lemma (in subset_class) smallest_closed_cdi2: "closed_cdi \ (smallest_ccdi_sets \ M)"
  by (simp add: closed_cdi_def smallest_ccdi_sets smallest_ccdi_sets.intros)

lemma closed_cdi_subset: "closed_cdi \ M \ M \ Pow \"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Compl: "closed_cdi \ M \ s \ M \ \ - s \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Inc:
  "closed_cdi \ M \ range A \ M \ A 0 = {} \ (!!n. A n \ A (Suc n)) \ (\i. A i) \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Disj:
  "closed_cdi \ M \ range A \ M \ disjoint_family A \ (\i::nat. A i) \ M"
  by (simp add: closed_cdi_def)

lemma closed_cdi_Un:
  assumes cdi: "closed_cdi \ M" and empty: "{} \ M"
      and A: "A \ M" and B: "B \ M"
      and disj: "A \ B = {}"
    shows "A \ B \ M"
proof -
  have ra: "range (binaryset A B) \ M"
   by (simp add: range_binaryset_eq empty A B)
have di:  "disjoint_family (binaryset A B)" using disj
   by (simp add: disjoint_family_on_def binaryset_def Int_commute)
from closed_cdi_Disj [OF cdi ra di]
show ?thesis
   by (simp add: UN_binaryset_eq)
qed

lemma (in algebra) smallest_ccdi_sets_Un:
  assumes A: "A \ smallest_ccdi_sets \ M" and B: "B \ smallest_ccdi_sets \ M"
      and disj: "A \ B = {}"
    shows "A \ B \ smallest_ccdi_sets \ M"
proof -
  have ra: "range (binaryset A B) \ Pow (smallest_ccdi_sets \ M)"
    by (simp add: range_binaryset_eq  A B smallest_ccdi_sets.Basic)
  have di:  "disjoint_family (binaryset A B)" using disj
    by (simp add: disjoint_family_on_def binaryset_def Int_commute)
  from Disj [OF ra di]
  show ?thesis
    by (simp add: UN_binaryset_eq)
qed

lemma (in algebra) smallest_ccdi_sets_Int1:
  assumes a: "a \ M"
  shows "b \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M"
proof (induct rule: smallest_ccdi_sets.induct)
  case (Basic x)
  thus ?case
    by (metis a Int smallest_ccdi_sets.Basic)
next
  case (Compl x)
  have 0: "(\ - a) \ (a \ x) = {}"
    by blast
  have "a \ (\ - x) = \ - ((\ - a) \ (a \ x))"
    by blast
  also have "... \ smallest_ccdi_sets \ M"
    by (intro 0 smallest_ccdi_sets.intros smallest_ccdi_sets_Un Compl.hyps assms)
  finally show ?case .
next
  case (Inc A)
  have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Inc
    by blast
  moreover have "(\i. a \ A i) 0 = {}"
    by (simp add: Inc)
  moreover have "!!n. (\i. a \ A i) n \ (\i. a \ A i) (Suc n)" using Inc
    by blast
  ultimately have "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Inc)
  moreover have "(\i. (\i. a \ A i) i) = a \ (\i. A i)"
    by blast
  ultimately show ?case
    by metis
next
  case (Disj A)
  have "range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Disj
    by blast
  moreover have "disjoint_family (\i. a \ A i)" using Disj
    by (auto simp add: disjoint_family_on_def)
  ultimately have "(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Disj)
  moreover have "(\i. (\i. a \ A i) i) = a \ (\i. A i)"
    by blast
  ultimately show ?case
    by metis
qed

lemma (in algebra) smallest_ccdi_sets_Int:
  assumes b: "b \ smallest_ccdi_sets \ M"
  shows "a \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M"
proof (induct rule: smallest_ccdi_sets.induct)
  case (Basic x)
  thus ?case
    by (metis b smallest_ccdi_sets_Int1)
next
  case (Compl x)
  have "(\ - x) \ b = \ - (x \ b \ (\ - b))"
    by blast
  also have "... \ smallest_ccdi_sets \ M"
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
  finally show ?case .
next
  case (Inc A)
  have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Inc
    by blast
  moreover have "(\i. A i \ b) 0 = {}"
    by (simp add: Inc)
  moreover have "!!n. (\i. A i \ b) n \ (\i. A i \ b) (Suc n)" using Inc
    by blast
  ultimately have "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Inc)
  moreover have "(\i. (\i. A i \ b) i) = (\i. A i) \ b"
    by blast
  ultimately show ?case
    by metis
next
  case (Disj A)
  have "range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Disj
    by blast
  moreover have "disjoint_family (\i. A i \ b)" using Disj
    by (auto simp add: disjoint_family_on_def)
  ultimately have "(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M"
    by (rule smallest_ccdi_sets.Disj)
  moreover have "(\i. (\i. A i \ b) i) = (\i. A i) \ b"
    by blast
  ultimately show ?case
    by metis
qed

lemma (in algebra) sigma_property_disjoint_lemma:
  assumes sbC: "M \ C"
      and ccdi: "closed_cdi \ C"
  shows "sigma_sets \ M \ C"
proof -
  have "smallest_ccdi_sets \ M \ {B . M \ B \ sigma_algebra \ B}"
    using smallest_ccdi_sets
    by (auto simp: sigma_algebra_disjoint_iff algebra_iff_Int
            smallest_ccdi_sets_Int intro: smallest_ccdi_sets.Disj)
  hence "sigma_sets (\) (M) \ smallest_ccdi_sets \ M"
    by (simp add: sigma_algebra.sigma_sets_subset)
  also have "... \ C"
  proof
    fix x
    assume x: "x \ smallest_ccdi_sets \ M"
    thus "x \ C"
    proof (induct rule: smallest_ccdi_sets.induct)
      case (Basic x)
      thus ?case
        by (metis Basic subsetD sbC)
    next
      case (Compl x)
      thus ?case
        by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
    next
      case (Inc A)
      thus ?case
        by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
    next
      case (Disj A)
      thus ?case
        by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
    qed
  qed
  finally show ?thesis .
qed

lemma (in algebra) sigma_property_disjoint:
  assumes sbC: "M \ C"
      and compl: "!!s. s \ C \ sigma_sets (\) (M) \ \ - s \ C"
      and inc: "!!A. range A \ C \ sigma_sets (\) (M)
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
      and disj: "!!A. range A \ C \ sigma_sets (\) (M)
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
  shows "sigma_sets (\) (M) \ C"
proof -
  have "sigma_sets (\) (M) \ C \ sigma_sets (\) (M)"
    proof (rule sigma_property_disjoint_lemma)
      show "M \ C \ sigma_sets (\) (M)"
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
    next
      show "closed_cdi \ (C \ sigma_sets (\) (M))"
        unfolding closed_cdi_def compl inc disj
        by (auto simp: image_subset_iff compl inc disj le_infI2 sigma_algebra.sigma_sets_subset sigma_algebra_Pow
            space_closed intro: sigma_sets.intros)
    qed
  thus ?thesis
    by blast
qed

subsubsection \<open>Dynkin systems\<close>

locale\<^marker>\<open>tag important\<close> Dynkin_system = subset_class +
  assumes space: "\ \ M"
    and   compl[intro!]: "\A. A \ M \ \ - A \ M"
    and   UN[intro!]: "\A. disjoint_family A \ range A \ M
                           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"

lemma (in Dynkin_system) empty[intro, simp]: "{} \ M"
  using space compl[of "\"] by simp

lemma (in Dynkin_system) diff:
  assumes sets: "D \ M" "E \ M" and "D \ E"
  shows "E - D \ M"
proof -
  let ?f = "\x. if x = 0 then D else if x = Suc 0 then \ - E else {}"
  have "range ?f = {D, \ - E, {}}"
    by (auto simp: image_iff)
  moreover have "D \ (\ - E) = (\i. ?f i)"
    by (auto simp: image_iff split: if_split_asm)
  moreover
  have "disjoint_family ?f" unfolding disjoint_family_on_def
    using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto
  ultimately have "\ - (D \ (\ - E)) \ M"
    using sets UN by auto fastforce
  also have "\ - (D \ (\ - E)) = E - D"
    using assms sets_into_space by auto
  finally show ?thesis .
qed

lemma Dynkin_systemI:
  assumes "\ A. A \ M \ A \ \" "\ \ M"
  assumes "\ A. A \ M \ \ - A \ M"
  assumes "\ A. disjoint_family A \ range A \ M
          \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
  shows "Dynkin_system \ M"
  using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def)

lemma Dynkin_systemI':
  assumes "\ A. A \ M \ A \ \"
  assumes empty: "{} \ M"
  assumes Diff: "\ A. A \ M \ \ - A \ M"
  assumes "\A. disjoint_family A \ range A \ M \ (\i::nat. A i) \ M"
  shows "Dynkin_system \ M"
  using Diff[OF empty]  assms by (simp add: Dynkin_systemI)

lemma Dynkin_system_trivial:
  shows "Dynkin_system A (Pow A)"
  by (rule Dynkin_systemI) auto

lemma sigma_algebra_imp_Dynkin_system:
  assumes "sigma_algebra \ M" shows "Dynkin_system \ M"
proof -
  interpret sigma_algebra \<Omega> M by fact
  show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI)
qed

subsubsection "Intersection sets systems"

definition\<^marker>\<open>tag important\<close> Int_stable :: "'a set set \<Rightarrow> bool" where
"Int_stable M \ (\ a \ M. \ b \ M. a \ b \ M)"

lemma (in algebra) Int_stable: "Int_stable M"
  unfolding Int_stable_def by auto

lemma Int_stableI_image:
  "(\i j. i \ I \ j \ I \ \k\I. A i \ A j = A k) \ Int_stable (A ` I)"
  by (auto simp: Int_stable_def image_def)

lemma Int_stableI:
  "(\a b. a \ A \ b \ A \ a \ b \ A) \ Int_stable A"
  unfolding Int_stable_def by auto

lemma Int_stableD:
  "Int_stable M \ a \ M \ b \ M \ a \ b \ M"
  unfolding Int_stable_def by auto

lemma (in Dynkin_system) sigma_algebra_eq_Int_stable:
  "sigma_algebra \ M \ Int_stable M"
proof
  assume "sigma_algebra \ M" then show "Int_stable M"
    unfolding sigma_algebra_def using algebra.Int_stable by auto
next
  assume "Int_stable M"
  show "sigma_algebra \ M"
    unfolding sigma_algebra_disjoint_iff algebra_iff_Un
  proof (intro conjI ballI allI impI)
    show "M \ Pow (\)" using sets_into_space by auto
  next
    fix A B assume "A \ M" "B \ M"
    then have "A \ B = \ - ((\ - A) \ (\ - B))"
              "\ - A \ M" "\ - B \ M"
      using sets_into_space by auto
    then show "A \ B \ M"
      using \<open>Int_stable M\<close> unfolding Int_stable_def by auto
  qed auto
qed

subsubsection "Smallest Dynkin systems"

definition\<^marker>\<open>tag important\<close> Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
  "Dynkin \ M = (\{D. Dynkin_system \ D \ M \ D})"

lemma Dynkin_system_Dynkin:
  assumes "M \ Pow (\)"
  shows "Dynkin_system \ (Dynkin \ M)"
proof (rule Dynkin_systemI)
  fix A assume "A \ Dynkin \ M"
  moreover
  { fix D assume "A \ D" and d: "Dynkin_system \ D"
    then have "A \ \" by (auto simp: Dynkin_system_def subset_class_def) }
  moreover have "{D. Dynkin_system \ D \ M \ D} \ {}"
    using assms Dynkin_system_trivial by fastforce
  ultimately show "A \ \"
    unfolding Dynkin_def using assms
    by auto
next
  show "\ \ Dynkin \ M"
    unfolding Dynkin_def using Dynkin_system.space by fastforce
next
  fix A assume "A \ Dynkin \ M"
  then show "\ - A \ Dynkin \ M"
    unfolding Dynkin_def using Dynkin_system.compl by force
next
  fix A :: "nat \ 'a set"
  assume A: "disjoint_family A" "range A \ Dynkin \ M"
  then show "(\i. A i) \ Dynkin \ M" unfolding Dynkin_def
    by (auto intro!: Dynkin_system.UN)
qed

lemma Dynkin_Basic[intro]: "A \ M \ A \ Dynkin \ M"
  unfolding Dynkin_def by auto

lemma (in Dynkin_system) restricted_Dynkin_system:
  assumes "D \ M"
  shows "Dynkin_system \ {Q. Q \ \ \ Q \ D \ M}"
proof (rule Dynkin_systemI, simp_all)
  have "\ \ D = D"
    using \<open>D \<in> M\<close> sets_into_space by auto
  then show "\ \ D \ M"
    using \<open>D \<in> M\<close> by auto
next
  fix A assume "A \ \ \ A \ D \ M"
  moreover have "(\ - A) \ D = (\ - (A \ D)) - (\ - D)"
    by auto
  ultimately show "(\ - A) \ D \ M"
    using  \<open>D \<in> M\<close> by (auto intro: diff)
next
  fix A :: "nat \ 'a set"
  assume "disjoint_family A" "range A \ {Q. Q \ \ \ Q \ D \ M}"
  then have "\i. A i \ \" "disjoint_family (\i. A i \ D)"
    "range (\i. A i \ D) \ M" "(\x. A x) \ D = (\x. A x \ D)"
    by ((fastforce simp: disjoint_family_on_def)+)
  then show "(\x. A x) \ \ \ (\x. A x) \ D \ M"
    by (auto simp del: UN_simps)
qed

lemma (in Dynkin_system) Dynkin_subset:
  assumes "N \ M"
  shows "Dynkin \ N \ M"
proof -
  have "Dynkin_system \ M" ..
  then have "Dynkin_system \ 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:
  assumes sets: "M \ Pow \"
  assumes "Int_stable M"
  shows "sigma_sets \ M = Dynkin \ M"
proof -
  have "Dynkin \ M \ sigma_sets (\) (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 \ (Dynkin \ M)"
    unfolding sigma_algebra_eq_Int_stable Int_stable_def
  proof (intro ballI)
    fix A B assume "A \ Dynkin \ M" "B \ Dynkin \ M"
    let ?D = "\E. {Q. Q \ \ \ Q \ E \ Dynkin \ M}"
    have "M \ ?D B"
    proof
      fix E assume "E \ M"
      then have "M \ ?D E" "E \ Dynkin \ M"
        using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def)
      then have "Dynkin \ M \ ?D E"
        using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close>
        by (intro Dynkin_system.Dynkin_subset) simp_all
      then have "B \ ?D E"
        using \<open>B \<in> Dynkin \<Omega> M\<close> by auto
      then have "E \ B \ Dynkin \ M"
        by (subst Int_commute) simp
      then show "E \ ?D B"
        using sets \<open>E \<in> M\<close> by auto
    qed
    then have "Dynkin \ M \ ?D B"
      using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close>
      by (intro Dynkin_system.Dynkin_subset) simp_all
    then show "A \ B \ Dynkin \ 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 (\) (M) \ Dynkin \ M" by auto
  ultimately have "sigma_sets (\) (M) = Dynkin \ M" by auto
  then show ?thesis
    by (auto simp: Dynkin_def)
qed

lemma (in Dynkin_system) Dynkin_idem:
  "Dynkin \ M = M"
proof -
  have "Dynkin \ M = M"
    using Dynkin_subset by blast
  then show ?thesis
    by (auto simp: Dynkin_def)
qed

lemma (in Dynkin_system) Dynkin_lemma:
  assumes "Int_stable E"
  and E: "E \ M" "M \ sigma_sets \ E"
  shows "sigma_sets \ E = M"
proof -
  have "E \ Pow \"
    using E sets_into_space by force
  then have *: "sigma_sets \ E = Dynkin \ E"
    using \<open>Int_stable E\<close> by (rule sigma_eq_Dynkin)
  then have "Dynkin \ E = M"
    using assms Dynkin_subset[OF \<open>E \<subseteq> M\<close>] by simp
  with * show ?thesis
    using assms by (auto simp: Dynkin_def)
qed

subsubsection \<open>Induction rule for intersection-stable generators\<close>

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 \ Pow \"
    and A: "A \ sigma_sets \ G"
  assumes basic: "\A. A \ G \ P A"
    and empty: "P {}"
    and compl: "\A. A \ sigma_sets \ G \ P A \ P (\ - A)"
    and union: "\A. disjoint_family A \ range A \ sigma_sets \ G \ (\i. P (A i)) \ P (\i::nat. A i)"
  shows "P A"
proof -
  let ?D = "{ A \ sigma_sets \ G. P A }"
  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
    using closed by (rule sigma_algebra_sigma_sets)
  from compl[OF _ empty] closed have space: "P \" by simp
  interpret Dynkin_system \<Omega> ?D
    by standard (auto dest: sets_into_space intro!: space compl union)
  have "sigma_sets \ G = ?D"
    by (rule Dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
  with A show ?thesis by auto
qed

subsection \<open>Measure type\<close>

definition\<^marker>\<open>tag important\<close> positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  "positive M \ \ \ {} = 0"

definition\<^marker>\<open>tag important\<close> countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"countably_additive M f \
  (\<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\<^marker>\<open>tag important\<close> measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"measure_space \ A \ \
  sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"

typedef\<^marker>\<open>tag important\<close> 'a measure =
  "{(\::'a set, A, \). (\a\-A. \ a = 0) \ measure_space \ A \ }"
proof
  have "sigma_algebra UNIV {{}, UNIV}"
    by (auto simp: sigma_algebra_iff2)
  then show "(UNIV, {{}, UNIV}, \A. 0) \ {(\, A, \). (\a\-A. \ a = 0) \ measure_space \ A \} "
    by (auto simp: measure_space_def positive_def countably_additive_def)
qed

definition\<^marker>\<open>tag important\<close> space :: "'a measure \<Rightarrow> 'a set" where
  "space M = fst (Rep_measure M)"

definition\<^marker>\<open>tag important\<close> sets :: "'a measure \<Rightarrow> 'a set set" where
  "sets M = fst (snd (Rep_measure M))"

definition\<^marker>\<open>tag important\<close> emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
  "emeasure M = snd (snd (Rep_measure M))"

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]]

declare [[coercion emeasure]]

lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
  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\<^marker>\<open>tag important\<close> measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
  where
    "measure_of \ A \ \
      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 \ A \ measure_of \ A (\x. 0)"

lemma measure_space_0: "A \ Pow \ \ measure_space \ (sigma_sets \ A) (\x. 0)"
  unfolding measure_space_def
  by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def)

lemma sigma_algebra_trivial: "sigma_algebra \ {{}, \}"
  by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\}"])+

lemma measure_space_0': "measure_space \ {{}, \} (\x. 0)"
  by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial)

lemma measure_space_closed:
  assumes "measure_space \ M \"
  shows "M \ Pow \"
proof -
  interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def)
  show ?thesis by(rule space_closed)
qed

lemma (in ring_of_sets) positive_cong_eq:
  "(\a. a \ M \ \' a = \ a) \ positive M \' = positive M \"
  by (auto simp add: positive_def)

lemma (in sigma_algebra) countably_additive_eq:
  "(\a. a \ M \ \' a = \ a) \ countably_additive M \' = countably_additive M \"
  unfolding countably_additive_def
  by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq)

lemma measure_space_eq:
  assumes closed: "A \ Pow \" and eq: "\a. a \ sigma_sets \ A \ \ a = \' a"
  shows "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) \'"
proof -
  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets)
  from positive_cong_eq[OF eq, of "\i. i"] countably_additive_eq[OF eq, of "\i. i"] show ?thesis
    by (auto simp: measure_space_def)
qed

lemma measure_of_eq:
  assumes closed: "A \ Pow \" and eq: "(\a. a \ sigma_sets \ A \ \ a = \' a)"
  shows "measure_of \ A \ = measure_of \ A \'"
proof -
  have "measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) \'"
    using assms by (rule measure_space_eq)
  with eq show ?thesis
    by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure])
qed

lemma measure_space_Pow_eq:
  assumes "\X. X \ Pow \ \ \ X = \' X"
  shows "measure_space \ (Pow \) \ = measure_space \ (Pow \) \'"
  by (smt (verit, best) assms measure_space_eq sigma_algebra.sigma_sets_eq sigma_algebra_Pow subset_eq)

lemma
--> --------------------

--> maximum size reached

--> --------------------

quality99%