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 *)
     6 
     7 header {* Sigma algebras *}
     8 
     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
    18   sigma_algebra :: "'a set set => 'a set set"    ("\<sigma>'_algebra")
    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 -
    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
    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"
    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
    51 
    52 end