summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Induct/Sigma_Algebra.thy

author | wenzelm |

Sat Feb 03 17:40:16 2001 +0100 (2001-02-03) | |

changeset 11046 | b5f5942781a0 |

parent 10875 | 1715cb147294 |

child 14717 | 7d8d4c9b36fd |

permissions | -rw-r--r-- |

Induct: converted some theories to new-style format;

1 (* Title: HOL/Induct/Sigma_Algebra.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 License: GPL (GNU GENERAL PUBLIC LICENSE)

5 *)

7 header {* Sigma algebras *}

9 theory Sigma_Algebra = Main:

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 *}

17 consts

18 sigma_algebra :: "'a set set => 'a set set" ("\<sigma>'_algebra")

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"

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 *}

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

34 proof -

35 have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV)

36 hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)

37 also have "-UNIV = {}" by simp

38 finally show ?thesis .

39 qed

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"

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)

48 also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp

49 finally show ?thesis .

50 qed

52 end