src/HOL/Induct/Sigma_Algebra.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 16417 9bc16273c2d4
child 23746 a455e69c31cc
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
wenzelm@10875
     1
(*  Title:      HOL/Induct/Sigma_Algebra.thy
wenzelm@10875
     2
    ID:         $Id$
wenzelm@10875
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10875
     4
*)
wenzelm@10875
     5
wenzelm@11046
     6
header {* Sigma algebras *}
wenzelm@11046
     7
haftmann@16417
     8
theory Sigma_Algebra imports Main begin
wenzelm@10875
     9
wenzelm@10875
    10
text {*
wenzelm@10875
    11
  This is just a tiny example demonstrating the use of inductive
wenzelm@10875
    12
  definitions in classical mathematics.  We define the least @{text
wenzelm@10875
    13
  \<sigma>}-algebra over a given set of sets.
wenzelm@10875
    14
*}
wenzelm@10875
    15
wenzelm@10875
    16
consts
wenzelm@14717
    17
  \<sigma>_algebra :: "'a set set => 'a set set"
wenzelm@10875
    18
wenzelm@10875
    19
inductive "\<sigma>_algebra A"
wenzelm@10875
    20
  intros
wenzelm@10875
    21
    basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
wenzelm@10875
    22
    UNIV: "UNIV \<in> \<sigma>_algebra A"
wenzelm@10875
    23
    complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
wenzelm@10875
    24
    Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
wenzelm@10875
    25
wenzelm@10875
    26
text {*
wenzelm@10875
    27
  The following basic facts are consequences of the closure properties
wenzelm@10875
    28
  of any @{text \<sigma>}-algebra, merely using the introduction rules, but
wenzelm@10875
    29
  no induction nor cases.
wenzelm@10875
    30
*}
wenzelm@10875
    31
wenzelm@10875
    32
theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
wenzelm@10875
    33
proof -
wenzelm@14717
    34
  have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
wenzelm@14717
    35
  hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
wenzelm@10875
    36
  also have "-UNIV = {}" by simp
wenzelm@10875
    37
  finally show ?thesis .
wenzelm@10875
    38
qed
wenzelm@10875
    39
wenzelm@10875
    40
theorem sigma_algebra_Inter:
wenzelm@10875
    41
  "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
wenzelm@10875
    42
proof -
wenzelm@10875
    43
  assume "!!i::nat. a i \<in> \<sigma>_algebra A"
wenzelm@14717
    44
  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
wenzelm@14717
    45
  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
wenzelm@14717
    46
  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
wenzelm@10875
    47
  also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
wenzelm@10875
    48
  finally show ?thesis .
wenzelm@10875
    49
qed
wenzelm@10875
    50
wenzelm@10875
    51
end