author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14981  e73f8140af78 
child 23746  a455e69c31cc 
permissions  rwrr 
10875  1 
(* Title: HOL/Induct/Sigma_Algebra.thy 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 
*) 

5 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
10875
diff
changeset

6 
header {* Sigma algebras *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
10875
diff
changeset

7 

16417  8 
theory Sigma_Algebra imports Main begin 
10875  9 

10 
text {* 

11 
This is just a tiny example demonstrating the use of inductive 

12 
definitions in classical mathematics. We define the least @{text 

13 
\<sigma>}algebra over a given set of sets. 

14 
*} 

15 

16 
consts 

14717  17 
\<sigma>_algebra :: "'a set set => 'a set set" 
10875  18 

19 
inductive "\<sigma>_algebra A" 

20 
intros 

21 
basic: "a \<in> A ==> a \<in> \<sigma>_algebra A" 

22 
UNIV: "UNIV \<in> \<sigma>_algebra A" 

23 
complement: "a \<in> \<sigma>_algebra A ==> a \<in> \<sigma>_algebra A" 

24 
Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A" 

25 

26 
text {* 

27 
The following basic facts are consequences of the closure properties 

28 
of any @{text \<sigma>}algebra, merely using the introduction rules, but 

29 
no induction nor cases. 

30 
*} 

31 

32 
theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A" 

33 
proof  

14717  34 
have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) 
35 
hence "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 

10875  36 
also have "UNIV = {}" by simp 
37 
finally show ?thesis . 

38 
qed 

39 

40 
theorem sigma_algebra_Inter: 

41 
"(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A" 

42 
proof  

43 
assume "!!i::nat. a i \<in> \<sigma>_algebra A" 

14717  44 
hence "!!i::nat. (a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 
45 
hence "(\<Union>i. (a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union) 

46 
hence "(\<Union>i. (a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 

10875  47 
also have "(\<Union>i. (a i)) = (\<Inter>i. a i)" by simp 
48 
finally show ?thesis . 

49 
qed 

50 

51 
end 