src/HOL/Induct/Sigma_Algebra.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46914 c2ca2c3d23a6
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
    Author:     Markus Wenzel, TU Muenchen
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     3
*)
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
     4
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10875
diff changeset
     5
header {* Sigma algebras *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10875
diff changeset
     6
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
     7
theory Sigma_Algebra
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
     8
imports Main
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
     9
begin
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    10
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    11
text {*
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    12
  This is just a tiny example demonstrating the use of inductive
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    13
  definitions in classical mathematics.  We define the least @{text
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    14
  \<sigma>}-algebra over a given set of sets.
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    15
*}
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    16
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    17
inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    18
where
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    19
  basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    20
| UNIV: "UNIV \<in> \<sigma>_algebra A"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    21
| complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    22
| Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    23
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    24
text {*
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    25
  The following basic facts are consequences of the closure properties
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    26
  of any @{text \<sigma>}-algebra, merely using the introduction rules, but
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    27
  no induction nor cases.
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    28
*}
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    29
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    30
theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    31
proof -
14717
7d8d4c9b36fd tuned notation;
wenzelm
parents: 11046
diff changeset
    32
  have "UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.UNIV)
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    33
  then have "-UNIV \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    34
  also have "-UNIV = {}" by simp
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    35
  finally show ?thesis .
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    36
qed
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    37
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    38
theorem sigma_algebra_Inter:
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    39
  "(!!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
    40
proof -
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    41
  assume "!!i::nat. a i \<in> \<sigma>_algebra A"
46914
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    42
  then have "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    43
  then have "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.Union)
c2ca2c3d23a6 misc tuning;
wenzelm
parents: 36862
diff changeset
    44
  then have "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule \<sigma>_algebra.complement)
10875
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    45
  also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    46
  finally show ?thesis .
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    47
qed
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    48
1715cb147294 added Induct/Sigma_Algebra.thy;
wenzelm
parents:
diff changeset
    49
end