# HG changeset patch
# User haftmann
# Date 1174077131 -3600
# Node ID f6f22aba2e0ed72084e2ad2dfa2d08a7b4b859a1
# Parent  c3654ba76a09aef385e7bece4c24befb6ed4de1e
added instance of sets as distributive lattices

diff -r c3654ba76a09 -r f6f22aba2e0e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Mar 16 21:32:10 2007 +0100
+++ b/src/HOL/Set.thy	Fri Mar 16 21:32:11 2007 +0100
@@ -1036,12 +1036,15 @@
   and [symmetric, defn] = atomize_ball
 
 
-subsection {* Further set-theory lemmas *}
+subsection {* Order on sets *}
 
 instance set :: (type) order
   by (intro_classes,
       (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
 
+
+subsection {* Further set-theory lemmas *}
+
 subsubsection {* Derived rules involving subsets. *}
 
 text {* @{text insert}. *}
@@ -2116,6 +2119,14 @@
   order_trans_rules set_rev_mp set_mp
 
 
+subsection {* Sets as lattice *}
+
+instance set :: (type) distrib_lattice
+  inf_set_eq: "inf A B \<equiv> A \<inter> B"
+  sup_set_eq: "sup A B \<equiv> A \<union> B"
+  by intro_classes (auto simp add: inf_set_eq sup_set_eq)
+
+
 subsection {* Basic ML bindings *}
 
 ML {*