author | wenzelm |
Fri, 07 May 2004 20:32:50 +0200 | |
changeset 14717 | 7d8d4c9b36fd |
parent 11046 | b5f5942781a0 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
10875 | 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 |
||
11046
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10875
diff
changeset
|
7 |
header {* Sigma algebras *} |
b5f5942781a0
Induct: converted some theories to new-style format;
wenzelm
parents:
10875
diff
changeset
|
8 |
|
10875 | 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 |
|
14717 | 18 |
\<sigma>_algebra :: "'a set set => 'a set set" |
10875 | 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 - |
|
14717 | 35 |
have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) |
36 |
hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) |
|
10875 | 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" |
|
14717 | 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) |
|
10875 | 48 |
also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp |
49 |
finally show ?thesis . |
|
50 |
qed |
|
51 |
||
52 |
end |