summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 12 Jan 2001 11:06:50 +0100 | |

changeset 10875 | 1715cb147294 |

parent 10874 | ad7113530c32 |

child 10876 | e12892e4666a |

added Induct/Sigma_Algebra.thy;

src/HOL/Induct/Sigma_Algebra.thy | file | annotate | diff | comparison | revisions | |

src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions |

--- /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

--- 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