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