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.

*}

inductive_set σ_algebra :: "'a set set => 'a set set" for A :: "'a set set"

where

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)

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) ==> (\<Inter>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 "(\<Union>i. -(a i)) ∈ σ_algebra A" by (rule σ_algebra.Union)

then have "-(\<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