src/HOL/Induct/Sigma_Algebra.thy
 author wenzelm Sat Feb 03 17:40:16 2001 +0100 (2001-02-03) changeset 11046 b5f5942781a0 parent 10875 1715cb147294 child 14717 7d8d4c9b36fd permissions -rw-r--r--
Induct: converted some theories to new-style format;
```     1 (*  Title:      HOL/Induct/Sigma_Algebra.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Markus Wenzel, TU Muenchen
```
```     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
```
```     5 *)
```
```     6
```
```     7 header {* Sigma algebras *}
```
```     8
```
```     9 theory Sigma_Algebra = Main:
```
```    10
```
```    11 text {*
```
```    12   This is just a tiny example demonstrating the use of inductive
```
```    13   definitions in classical mathematics.  We define the least @{text
```
```    14   \<sigma>}-algebra over a given set of sets.
```
```    15 *}
```
```    16
```
```    17 consts
```
```    18   sigma_algebra :: "'a set set => 'a set set"    ("\<sigma>'_algebra")
```
```    19
```
```    20 inductive "\<sigma>_algebra A"
```
```    21   intros
```
```    22     basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
```
```    23     UNIV: "UNIV \<in> \<sigma>_algebra A"
```
```    24     complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
```
```    25     Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
```
```    26
```
```    27 text {*
```
```    28   The following basic facts are consequences of the closure properties
```
```    29   of any @{text \<sigma>}-algebra, merely using the introduction rules, but
```
```    30   no induction nor cases.
```
```    31 *}
```
```    32
```
```    33 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
```
```    34 proof -
```
```    35   have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV)
```
```    36   hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
```
```    37   also have "-UNIV = {}" by simp
```
```    38   finally show ?thesis .
```
```    39 qed
```
```    40
```
```    41 theorem sigma_algebra_Inter:
```
```    42   "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
```
```    43 proof -
```
```    44   assume "!!i::nat. a i \<in> \<sigma>_algebra A"
```
```    45   hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
```
```    46   hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.Union)
```
```    47   hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
```
```    48   also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
```
```    49   finally show ?thesis .
```
```    50 qed
```
```    51
```
```    52 end
```