src/HOL/Induct/Sigma_Algebra.thy
 author haftmann Fri, 17 Jun 2005 16:12:49 +0200 changeset 16417 9bc16273c2d4 parent 14981 e73f8140af78 child 23746 a455e69c31cc permissions -rw-r--r--
migrated theory headers to new format
```
(*  Title:      HOL/Induct/Sigma_Algebra.thy
ID:         \$Id\$
Author:     Markus Wenzel, TU Muenchen
*)

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
\<sigma>}-algebra over a given set of sets.
*}

consts
\<sigma>_algebra :: "'a set set => 'a set set"

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

text {*
The following basic facts are consequences of the closure properties
of any @{text \<sigma>}-algebra, merely using the introduction rules, but
no induction nor cases.
*}

theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
proof -
have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
also have "-UNIV = {}" by simp
finally show ?thesis .
qed

theorem sigma_algebra_Inter:
"(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
proof -
assume "!!i::nat. a i \<in> \<sigma>_algebra A"
hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
finally show ?thesis .
qed

end
```