# Theory Sigma_Algebra

Up to index of Isabelle/HOL/Induct

theory Sigma_Algebra
imports Main
begin

    (*  Title:      HOL/Induct/Sigma_Algebra.thy
        ID:         $Id: Sigma_Algebra.thy,v 1.5 2005/06/17 14:13:07 haftmann Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* 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 @{text
      σ}-algebra over a given set of sets.
    *}

    consts
      σ_algebra :: "'a set set => 'a set set"

    inductive "σ_algebra A"
      intros
        basic: "a ∈ A ==> a ∈ σ_algebra A"
        UNIV: "UNIV ∈ σ_algebra A"
        complement: "a ∈ σ_algebra A ==> -a ∈ σ_algebra A"
        Union: "(!!i::nat. a i ∈ σ_algebra A) ==> (\<Union>i. a i) ∈ σ_algebra A"

    text {*
      The following basic facts are consequences of the closure properties
      of any @{text σ}-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)
      hence "-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) ==> (\<Inter>i. a i) ∈ σ_algebra A"
    proof -
      assume "!!i::nat. a i ∈ σ_algebra A"
      hence "!!i::nat. -(a i) ∈ σ_algebra A" by (rule σ_algebra.complement)
      hence "(\<Union>i. -(a i)) ∈ σ_algebra A" by (rule σ_algebra.Union)
      hence "-(\<Union>i. -(a i)) ∈ σ_algebra A" by (rule σ_algebra.complement)
      also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
      finally show ?thesis .
    qed

    end

theorem sigma_algebra_empty:

      {} ∈ σ_algebra A

theorem sigma_algebra_Inter:

      (!!i. a i ∈ σ_algebra A) ==> (INT i. a i) ∈ σ_algebra A