# HG changeset patch
# User wenzelm
# Date 979294010 -3600
# Node ID 1715cb1472941132456f054688e2f0b0c527bdc8
# Parent  ad7113530c327ff0630f95fb883e7ddbed9543ac
added Induct/Sigma_Algebra.thy;

diff -r ad7113530c32 -r 1715cb147294 src/HOL/Induct/Sigma_Algebra.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Sigma_Algebra.thy	Fri Jan 12 11:06:50 2001 +0100
@@ -0,0 +1,50 @@
+(*  Title:      HOL/Induct/Sigma_Algebra.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+theory Sigma_Algebra = Main:
+
+text {*
+  This is just a tiny example demonstrating the use of inductive
+  definitions in classical mathematics.  We define the least @{text
+  \<sigma>}-algebra over a given set of sets.
+*}
+
+consts
+  sigma_algebra :: "'a set set => 'a set set"    ("\<sigma>'_algebra")
+
+inductive "\<sigma>_algebra A"
+  intros
+    basic: "a \<in> A ==> a \<in> \<sigma>_algebra A"
+    UNIV: "UNIV \<in> \<sigma>_algebra A"
+    complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
+    Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
+
+text {*
+  The following basic facts are consequences of the closure properties
+  of any @{text \<sigma>}-algebra, merely using the introduction rules, but
+  no induction nor cases.
+*}
+
+theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
+proof -
+  have "UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.UNIV)
+  hence "-UNIV \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
+  also have "-UNIV = {}" by simp
+  finally show ?thesis .
+qed
+
+theorem sigma_algebra_Inter:
+  "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Inter>i. a i) \<in> \<sigma>_algebra A"
+proof -
+  assume "!!i::nat. a i \<in> \<sigma>_algebra A"
+  hence "!!i::nat. -(a i) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
+  hence "(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.Union)
+  hence "-(\<Union>i. -(a i)) \<in> \<sigma>_algebra A" by (rule sigma_algebra.complement)
+  also have "-(\<Union>i. -(a i)) = (\<Inter>i. a i)" by simp
+  finally show ?thesis .
+qed
+
+end
diff -r ad7113530c32 -r 1715cb147294 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 12 09:32:53 2001 +0100
+++ b/src/HOL/IsaMakefile	Fri Jan 12 11:06:50 2001 +0100
@@ -205,8 +205,8 @@
   Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
   Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
   Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
-  Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
-  Induct/Term.ML Induct/Term.thy
+  Induct/Sigma_Algebra.thy Induct/SList.ML Induct/SList.thy \
+  Induct/ABexp.ML Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Induct