src/HOL/Induct/Sigma_Algebra.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 23746 a455e69c31cc
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Sigma_Algebra.thy
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     4
*)
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     5
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10875
diff changeset
     6
header {* Sigma algebras *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10875
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     8
theory Sigma_Algebra imports Main begin
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     9
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    10
text {*
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    11
  This is just a tiny example demonstrating the use of inductive
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    12
  definitions in classical mathematics.  We define the least @{text
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    13
  \<sigma>}-algebra over a given set of sets.
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    14
*}
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    15
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    16
consts
14717
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    17
  \<sigma>_algebra :: "'a set set => 'a set set"
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    18
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    19
inductive "\<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    20
  intros
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    21
    basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    22
    UNIV: "UNIV \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    23
    complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    24
    Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    25
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    26
text {*
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    27
  The following basic facts are consequences of the closure properties
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    28
  of any @{text \<sigma>}-algebra, merely using the introduction rules, but
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    29
  no induction nor cases.
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    30
*}
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    31
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    32
theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    33
proof -
14717
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    34
  have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    35
  hence "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    36
  also have "-UNIV = {}" by simp
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    37
  finally show ?thesis .
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    38
qed
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    39
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    40
theorem sigma_algebra_Inter:
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    41
  "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    42
proof -
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    43
  assume "!!i::nat. a i \<in> \<sigma>_algebra A"
14717
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    44
  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    45
  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    46
  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    47
  also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    48
  finally show ?thesis .
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    49
qed
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    50
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    51
end