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 


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
