(*  Title:      HOL/Induct/Sigma_Algebra.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section ‹Sigma algebras›

theory Sigma_Algebra
imports Main
begin

text ‹
 This is just a tiny example demonstrating the use of inductive
 definitions in classical mathematics. We define the least ‹σ›-algebra over a given set of sets.
 ›

inductive_set σ_algebra :: "'a set set → 'a set set" for A :: "'a set set"
where
  basic: "a ∈ σ_algebra A" if "a ∈ A" for a
| UNIV: "UNIV ∈ σ_algebra A"
| complement: "- a ∈ σ_algebra A" if "a ∈ σ_algebra A" for a
| Union: "(∪i. a i) ∈ σ_algebra A" if "∧i::nat. a i ∈ σ_algebra A" for a

text ‹
 The following basic facts are consequences of the closure properties
 of any ‹σ›-algebra, merely using the introduction rules, but
 no induction nor cases.
 ›

theorem sigma_algebra_empty: "{} ∈ σ_algebra A"
proof -
  have "UNIV ∈ σ_algebra A" by (rule σ_algebra.UNIV)
  then have "-UNIV ∈ σ_algebra A" by (rule σ_algebra.complement)
  also have "-UNIV = {}" by simp
  finally show ?thesis .
qed

theorem sigma_algebra_Inter:
  "(∧i::nat. a i ∈ σ_algebra A) ==> (∩i. a i) ∈ σ_algebra A"
proof -
  assume "∧i::nat. a i ∈ σ_algebra A"
  then have "∧i::nat. -(a i) ∈ σ_algebra A" by (rule σ_algebra.complement)
  then have "(∪i. -(a i)) ∈ σ_algebra A" by (rule σ_algebra.Union)
  then have "-(∪i. -(a i)) ∈ σ_algebra A" by (rule σ_algebra.complement)
  also have "-(∪i. -(a i)) = (∩i. a i)" by simp
  finally show ?thesis .
qed

end