author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46914  c2ca2c3d23a6 
child 58889  5b7a9633cfa8 
permissions  rwrr 
10875  1 
(* Title: HOL/Induct/Sigma_Algebra.thy 
2 
Author: Markus Wenzel, TU Muenchen 

3 
*) 

4 

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

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

6 

46914  7 
theory Sigma_Algebra 
8 
imports Main 

9 
begin 

10875  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 

46914  17 
inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set" 
18 
where 

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

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

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

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

10875  23 

24 
text {* 

25 
The following basic facts are consequences of the closure properties 

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

27 
no induction nor cases. 

28 
*} 

29 

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

31 
proof  

14717  32 
have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV) 
46914  33 
then have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 
10875  34 
also have "UNIV = {}" by simp 
35 
finally show ?thesis . 

36 
qed 

37 

38 
theorem sigma_algebra_Inter: 

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

40 
proof  

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

46914  42 
then have "!!i::nat. (a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 
43 
then have "(\<Union>i. (a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union) 

44 
then have "(\<Union>i. (a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement) 

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

47 
qed 

48 

49 
end 