products/sources/formale Sprachen/Delphi/Agenda 1.1/Auslieferung/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sigma_Algebra.thy   Sprache: Unknown

(*  Title:      HOL/Induct/Sigma_Algebra.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section \<open>Sigma algebras\<close>

theory Sigma_Algebra
imports Main
begin

text \<open>
  This is just a tiny example demonstrating the use of inductive
  definitions in classical mathematics.  We define the least \<open>\<sigma>\<close>-algebra over a given set of sets.
\<close>

inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
where
  basic: "a \ \_algebra A" if "a \ A" for a
| UNIV: "UNIV \ \_algebra A"
| complement: "- a \ \_algebra A" if "a \ \_algebra A" for a
| Union: "(\i. a i) \ \_algebra A" if "\i::nat. a i \ \_algebra A" for a

text \<open>
  The following basic facts are consequences of the closure properties
  of any \<open>\<sigma>\<close>-algebra, merely using the introduction rules, but
  no induction nor cases.
\<close>

theorem sigma_algebra_empty: "{} \ \_algebra A"
proof -
  have "UNIV \ \_algebra A" by (rule \_algebra.UNIV)
  then have "-UNIV \ \_algebra A" by (rule \_algebra.complement)
  also have "-UNIV = {}" by simp
  finally show ?thesis .
qed

theorem sigma_algebra_Inter:
  "(\i::nat. a i \ \_algebra A) \ (\i. a i) \ \_algebra A"
proof -
  assume "\i::nat. a i \ \_algebra A"
  then have "\i::nat. -(a i) \ \_algebra A" by (rule \_algebra.complement)
  then have "(\i. -(a i)) \ \_algebra A" by (rule \_algebra.Union)
  then have "-(\i. -(a i)) \ \_algebra A" by (rule \_algebra.complement)
  also have "-(\i. -(a i)) = (\i. a i)" by simp
  finally show ?thesis .
qed

end

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]