|
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 theory Sigma_Algebra = Main: |
|
8 |
|
9 text {* |
|
10 This is just a tiny example demonstrating the use of inductive |
|
11 definitions in classical mathematics. We define the least @{text |
|
12 \<sigma>}-algebra over a given set of sets. |
|
13 *} |
|
14 |
|
15 consts |
|
16 sigma_algebra :: "'a set set => 'a set set" ("\<sigma>'_algebra") |
|
17 |
|
18 inductive "\<sigma>_algebra A" |
|
19 intros |
|
20 basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" |
|
21 UNIV: "UNIV \<in> \<sigma>_algebra A" |
|
22 complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A" |
|
23 Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A" |
|
24 |
|
25 text {* |
|
26 The following basic facts are consequences of the closure properties |
|
27 of any @{text \<sigma>}-algebra, merely using the introduction rules, but |
|
28 no induction nor cases. |
|
29 *} |
|
30 |
|
31 theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" |
|
32 proof - |
|
33 have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV) |
|
34 hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
|
35 also have "-UNIV = {}" by simp |
|
36 finally show ?thesis . |
|
37 qed |
|
38 |
|
39 theorem sigma_algebra_Inter: |
|
40 "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" |
|
41 proof - |
|
42 assume "!!i::nat. a i \<in> \<sigma>_algebra A" |
|
43 hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
|
44 hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.Union) |
|
45 hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement) |
|
46 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
|
47 finally show ?thesis . |
|
48 qed |
|
49 |
|
50 end |