# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272287654 -7200
# Node ID f71978e47cd50814c079d0bc381ff0a9180aff97
# Parent  85ee44388f7bcfac5e9ca4f7ca90797455063eeb
add bounded_lattice_bot and bounded_lattice_top type classes

diff -r 85ee44388f7b -r f71978e47cd5 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Apr 26 13:43:31 2010 +0200
+++ b/src/HOL/Lattices.thy	Mon Apr 26 15:14:14 2010 +0200
@@ -365,13 +365,9 @@
 
 subsection {* Bounded lattices and boolean algebras *}
 
-class bounded_lattice = lattice + top + bot
+class bounded_lattice_bot = lattice + bot
 begin
 
-lemma dual_bounded_lattice:
-  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by unfold_locales (auto simp add: less_le_not_le)
-
 lemma inf_bot_left [simp]:
   "\<bottom> \<sqinter> x = \<bottom>"
   by (rule inf_absorb1) simp
@@ -380,6 +376,23 @@
   "x \<sqinter> \<bottom> = \<bottom>"
   by (rule inf_absorb2) simp
 
+lemma sup_bot_left [simp]:
+  "\<bottom> \<squnion> x = x"
+  by (rule sup_absorb2) simp
+
+lemma sup_bot_right [simp]:
+  "x \<squnion> \<bottom> = x"
+  by (rule sup_absorb1) simp
+
+lemma sup_eq_bot_iff [simp]:
+  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  by (simp add: eq_iff)
+
+end
+
+class bounded_lattice_top = lattice + top
+begin
+
 lemma sup_top_left [simp]:
   "\<top> \<squnion> x = \<top>"
   by (rule sup_absorb1) simp
@@ -396,21 +409,18 @@
   "x \<sqinter> \<top> = x"
   by (rule inf_absorb1) simp
 
-lemma sup_bot_left [simp]:
-  "\<bottom> \<squnion> x = x"
-  by (rule sup_absorb2) simp
-
-lemma sup_bot_right [simp]:
-  "x \<squnion> \<bottom> = x"
-  by (rule sup_absorb1) simp
-
 lemma inf_eq_top_iff [simp]:
   "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   by (simp add: eq_iff)
 
-lemma sup_eq_bot_iff [simp]:
-  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-  by (simp add: eq_iff)
+end
+
+class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
+begin
+
+lemma dual_bounded_lattice:
+  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by unfold_locales (auto simp add: less_le_not_le)
 
 end
 
diff -r 85ee44388f7b -r f71978e47cd5 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Mon Apr 26 13:43:31 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Mon Apr 26 15:14:14 2010 +0200
@@ -387,7 +387,7 @@
   apply (simp add: memb_def[symmetric] memb_finter_raw)
   by (auto simp add: memb_def)
 
-instantiation fset :: (type) "{bot,distrib_lattice}"
+instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice}"
 begin
 
 quotient_definition
@@ -922,14 +922,13 @@
 
 text {* funion *}
 
-lemma funion_simps[simp]:
-  shows "{||} |\<union>| S = S"
-  and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
-  by (lifting append.simps)
+lemmas [simp] =
+  sup_bot_left[where 'a="'a fset"]
+  sup_bot_right[where 'a="'a fset"]
 
-lemma funion_empty[simp]:
-  shows "S |\<union>| {||} = S"
-  by (lifting append_Nil2)
+lemma funion_finsert[simp]:
+  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+  by (lifting append.simps(2))
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"