# HG changeset patch
# User haftmann
# Date 1260039741 -3600
# Node ID aea892559fc52c411d370f81e1b86a11ec64a929
# Parent  e4fb0daadcffd58a46b8f1a1cd90cbabd4dbe1ed
tuned lattices theory fragements; generlized some lemmas from sets to lattices

diff -r e4fb0daadcff -r aea892559fc5 NEWS
--- a/NEWS	Sat Dec 05 10:18:23 2009 +0100
+++ b/NEWS	Sat Dec 05 20:02:21 2009 +0100
@@ -11,6 +11,25 @@
 
 * Code generation: ML and OCaml code is decorated with signatures.
 
+* Complete_Lattice.thy: lemmas top_def and bot_def have been replaced
+by the more convenient lemmas Inf_empty and Sup_empty.  Dropped lemmas
+Inf_insert_simp adn Sup_insert_simp, which are subsumed by Inf_insert and
+Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
+Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot respectively.
+INCOMPATIBILITY.
+
+* Finite_Set.thy and List.thy: some lemmas have been generalized from sets to lattices:
+  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
+  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
+  inter_Inter_fold_inter        ~> inf_Inf_fold_inf
+  union_Union_fold_union        ~> sup_Sup_fold_sup
+  Inter_fold_inter              ~> Inf_fold_inf
+  Union_fold_union              ~> Sup_fold_sup
+  inter_INTER_fold_inter        ~> inf_INFI_fold_inf
+  union_UNION_fold_union        ~> sup_SUPR_fold_sup
+  INTER_fold_inter              ~> INFI_fold_inf
+  UNION_fold_union              ~> SUPR_fold_sup
+
 
 *** ML ***
 
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Complete_Lattice.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -7,10 +7,10 @@
 begin
 
 notation
-  less_eq  (infix "\<sqsubseteq>" 50) and
+  less_eq (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
   top ("\<top>") and
   bot ("\<bottom>")
 
@@ -25,7 +25,7 @@
 
 subsection {* Abstract complete lattices *}
 
-class complete_lattice = lattice + bot + top + Inf + Sup +
+class complete_lattice = bounded_lattice + Inf + Sup +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
      and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
@@ -34,22 +34,23 @@
 
 lemma dual_complete_lattice:
   "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (auto intro!: complete_lattice.intro dual_lattice
-    bot.intro top.intro dual_preorder, unfold_locales)
-      (fact bot_least top_greatest
-        Sup_upper Sup_least Inf_lower Inf_greatest)+
+  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+    (unfold_locales, (fact bot_least top_greatest
+        Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
+lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
-  unfolding Sup_Inf by auto
+lemma Inf_empty:
+  "\<Sqinter>{} = \<top>"
+  by (auto intro: antisym Inf_greatest)
 
-lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
-  unfolding Inf_Sup by auto
+lemma Sup_empty:
+  "\<Squnion>{} = \<bottom>"
+  by (auto intro: antisym Sup_least)
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
@@ -65,37 +66,21 @@
   "\<Squnion>{a} = a"
   by (auto intro: antisym Sup_upper Sup_least)
 
-lemma Inf_insert_simp:
-  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
-  by (cases "A = {}") (simp_all, simp add: Inf_insert)
-
-lemma Sup_insert_simp:
-  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
-  by (cases "A = {}") (simp_all, simp add: Sup_insert)
-
 lemma Inf_binary:
   "\<Sqinter>{a, b} = a \<sqinter> b"
-  by (auto simp add: Inf_insert_simp)
+  by (simp add: Inf_empty Inf_insert)
 
 lemma Sup_binary:
   "\<Squnion>{a, b} = a \<squnion> b"
-  by (auto simp add: Sup_insert_simp)
-
-lemma bot_def:
-  "bot = \<Squnion>{}"
-  by (auto intro: antisym Sup_least)
+  by (simp add: Sup_empty Sup_insert)
 
-lemma top_def:
-  "top = \<Sqinter>{}"
-  by (auto intro: antisym Inf_greatest)
+lemma Inf_UNIV:
+  "\<Sqinter>UNIV = bot"
+  by (simp add: Sup_Inf Sup_empty [symmetric])
 
-lemma sup_bot [simp]:
-  "x \<squnion> bot = x"
-  using bot_least [of x] by (simp add: sup_commute sup_absorb2)
-
-lemma inf_top [simp]:
-  "x \<sqinter> top = x"
-  using top_greatest [of x] by (simp add: inf_commute inf_absorb2)
+lemma Sup_UNIV:
+  "\<Squnion>UNIV = top"
+  by (simp add: Inf_Sup Inf_empty [symmetric])
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f = \<Squnion> (f ` A)"
@@ -129,16 +114,16 @@
 context complete_lattice
 begin
 
-lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
+lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
   by (auto simp add: SUPR_def intro: Sup_upper)
 
-lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
+lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
   by (auto simp add: SUPR_def intro: Sup_least)
 
-lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
+lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
   by (auto simp add: INFI_def intro: Inf_lower)
 
-lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
+lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
   by (auto simp add: INFI_def intro: Inf_greatest)
 
 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -2937,37 +2937,6 @@
 
 end
 
-context complete_lattice
-begin
-
-text {*
-  Coincidence on finite sets in complete lattices:
-*}
-
-lemma Inf_fin_Inf:
-  assumes "finite A" and "A \<noteq> {}"
-  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
-proof -
-    interpret ab_semigroup_idem_mult inf
-    by (rule ab_semigroup_idem_mult_inf)
-  from assms show ?thesis
-  unfolding Inf_fin_def by (induct A set: finite)
-    (simp_all add: Inf_insert_simp)
-qed
-
-lemma Sup_fin_Sup:
-  assumes "finite A" and "A \<noteq> {}"
-  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
-proof -
-  interpret ab_semigroup_idem_mult sup
-    by (rule ab_semigroup_idem_mult_sup)
-  from assms show ?thesis
-  unfolding Sup_fin_def by (induct A set: finite)
-    (simp_all add: Sup_insert_simp)
-qed
-
-end
-
 
 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
 
@@ -3345,15 +3314,15 @@
 proof
 qed auto
 
-lemma fun_left_comm_idem_inter:
-  "fun_left_comm_idem op \<inter>"
+lemma (in lower_semilattice) fun_left_comm_idem_inf:
+  "fun_left_comm_idem inf"
 proof
-qed auto
-
-lemma fun_left_comm_idem_union:
-  "fun_left_comm_idem op \<union>"
+qed (auto simp add: inf_left_commute)
+
+lemma (in upper_semilattice) fun_left_comm_idem_sup:
+  "fun_left_comm_idem sup"
 proof
-qed auto
+qed (auto simp add: sup_left_commute)
 
 lemma union_fold_insert:
   assumes "finite A"
@@ -3371,60 +3340,95 @@
   from `finite A` show ?thesis by (induct A arbitrary: B) auto
 qed
 
-lemma inter_Inter_fold_inter:
+context complete_lattice
+begin
+
+lemma inf_Inf_fold_inf:
   assumes "finite A"
-  shows "B \<inter> Inter A = fold (op \<inter>) B A"
+  shows "inf B (Inf A) = fold inf B A"
 proof -
-  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: fold_fun_comm Int_commute)
+    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
 qed
 
-lemma union_Union_fold_union:
+lemma sup_Sup_fold_sup:
   assumes "finite A"
-  shows "B \<union> Union A = fold (op \<union>) B A"
+  shows "sup B (Sup A) = fold sup B A"
 proof -
-  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: fold_fun_comm Un_commute)
+    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
 qed
 
-lemma Inter_fold_inter:
+lemma Inf_fold_inf:
   assumes "finite A"
-  shows "Inter A = fold (op \<inter>) UNIV A"
-  using assms inter_Inter_fold_inter [of A UNIV] by simp
-
-lemma Union_fold_union:
+  shows "Inf A = fold inf top A"
+  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
   assumes "finite A"
-  shows "Union A = fold (op \<union>) {} A"
-  using assms union_Union_fold_union [of A "{}"] by simp
-
-lemma inter_INTER_fold_inter:
-  assumes "finite A"
-  shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold") 
-proof (rule sym)
-  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
-  interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
+  shows "Sup A = fold sup bot A"
+  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
+
+lemma Inf_fin_Inf:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
+proof -
+  interpret ab_semigroup_idem_mult inf
+    by (rule ab_semigroup_idem_mult_inf)
+  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+  moreover with `finite A` have "finite B" by simp
+  ultimately show ?thesis  
+  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
+    (simp add: Inf_fold_inf)
 qed
 
-lemma union_UNION_fold_union:
+lemma Sup_fin_Sup:
+  assumes "finite A" and "A \<noteq> {}"
+  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
+proof -
+  interpret ab_semigroup_idem_mult sup
+    by (rule ab_semigroup_idem_mult_sup)
+  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
+  moreover with `finite A` have "finite B" by simp
+  ultimately show ?thesis  
+  by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
+    (simp add: Sup_fold_sup)
+qed
+
+lemma inf_INFI_fold_inf:
   assumes "finite A"
-  shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold") 
+  shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
 proof (rule sym)
-  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
-  interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
-  from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
+  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+  interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?inf"
+  by (induct A arbitrary: B)
+    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
 qed
 
-lemma INTER_fold_inter:
+lemma sup_SUPR_fold_sup:
   assumes "finite A"
-  shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
-  using assms inter_INTER_fold_inter [of A UNIV] by simp
-
-lemma UNION_fold_union:
+  shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
+proof (rule sym)
+  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+  interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?sup"
+  by (induct A arbitrary: B)
+    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
+qed
+
+lemma INFI_fold_inf:
   assumes "finite A"
-  shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
-  using assms union_UNION_fold_union [of A "{}"] by simp
+  shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
+  using assms inf_INFI_fold_inf [of A top] by simp
+
+lemma SUPR_fold_sup:
+  assumes "finite A"
+  shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
+  using assms sup_SUPR_fold_sup [of A bot] by simp
 
 end
+
+end
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Lattices.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -70,7 +70,7 @@
 
 lemma mono_inf:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
-  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B"
+  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
   by (auto simp add: mono_def intro: Lattices.inf_greatest)
 
 end
@@ -104,7 +104,7 @@
 
 lemma mono_sup:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
-  shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)"
+  shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
 end
@@ -241,22 +241,22 @@
 begin
 
 lemma less_supI1:
-  "x < a \<Longrightarrow> x < a \<squnion> b"
+  "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
   interpret dual: lower_semilattice "op \<ge>" "op >" sup
     by (fact dual_semilattice)
-  assume "x < a"
-  then show "x < a \<squnion> b"
+  assume "x \<sqsubset> a"
+  then show "x \<sqsubset> a \<squnion> b"
     by (fact dual.less_infI1)
 qed
 
 lemma less_supI2:
-  "x < b \<Longrightarrow> x < a \<squnion> b"
+  "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
   interpret dual: lower_semilattice "op \<ge>" "op >" sup
     by (fact dual_semilattice)
-  assume "x < b"
-  then show "x < a \<squnion> b"
+  assume "x \<sqsubset> b"
+  then show "x \<sqsubset> a \<squnion> b"
     by (fact dual.less_infI2)
 qed
 
@@ -294,58 +294,46 @@
 end
 
 
-subsection {* Boolean algebras *}
+subsection {* Bounded lattices and boolean algebras *}
 
-class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
-  assumes inf_compl_bot: "x \<sqinter> - x = bot"
-    and sup_compl_top: "x \<squnion> - x = top"
-  assumes diff_eq: "x - y = x \<sqinter> - y"
+class bounded_lattice = lattice + top + bot
 begin
 
-lemma dual_boolean_algebra:
-  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
-  by (rule boolean_algebra.intro, rule dual_distrib_lattice)
-    (unfold_locales,
-      auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
-
-lemma compl_inf_bot:
-  "- x \<sqinter> x = bot"
-  by (simp add: inf_commute inf_compl_bot)
-
-lemma compl_sup_top:
-  "- x \<squnion> x = top"
-  by (simp add: sup_commute sup_compl_top)
+lemma dual_bounded_lattice:
+  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (rule bounded_lattice.intro, rule dual_lattice)
+    (unfold_locales, auto simp add: less_le_not_le)
 
 lemma inf_bot_left [simp]:
-  "bot \<sqinter> x = bot"
+  "\<bottom> \<sqinter> x = \<bottom>"
   by (rule inf_absorb1) simp
 
 lemma inf_bot_right [simp]:
-  "x \<sqinter> bot = bot"
+  "x \<sqinter> \<bottom> = \<bottom>"
   by (rule inf_absorb2) simp
 
 lemma sup_top_left [simp]:
-  "top \<squnion> x = top"
+  "\<top> \<squnion> x = \<top>"
   by (rule sup_absorb1) simp
 
 lemma sup_top_right [simp]:
-  "x \<squnion> top = top"
+  "x \<squnion> \<top> = \<top>"
   by (rule sup_absorb2) simp
 
 lemma inf_top_left [simp]:
-  "top \<sqinter> x = x"
+  "\<top> \<sqinter> x = x"
   by (rule inf_absorb2) simp
 
 lemma inf_top_right [simp]:
-  "x \<sqinter> top = x"
+  "x \<sqinter> \<top> = x"
   by (rule inf_absorb1) simp
 
 lemma sup_bot_left [simp]:
-  "bot \<squnion> x = x"
+  "\<bottom> \<squnion> x = x"
   by (rule sup_absorb2) simp
 
 lemma sup_bot_right [simp]:
-  "x \<squnion> bot = x"
+  "x \<squnion> \<bottom> = x"
   by (rule sup_absorb1) simp
 
 lemma inf_eq_top_eq1:
@@ -354,8 +342,8 @@
 proof (cases "B = \<top>")
   case True with assms show ?thesis by simp
 next
-  case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
-  then have "A \<sqinter> B < \<top>" by (rule less_infI2)
+  case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
+  then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
   with assms show ?thesis by simp
 qed
 
@@ -368,8 +356,8 @@
   assumes "A \<squnion> B = \<bottom>"
   shows "A = \<bottom>"
 proof -
-  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
-    by (rule dual_boolean_algebra)
+  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
+    by (rule dual_bounded_lattice)
   from dual.inf_eq_top_eq1 assms show ?thesis .
 qed
 
@@ -377,14 +365,35 @@
   assumes "A \<squnion> B = \<bottom>"
   shows "B = \<bottom>"
 proof -
-  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
-    by (rule dual_boolean_algebra)
+  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
+    by (rule dual_bounded_lattice)
   from dual.inf_eq_top_eq2 assms show ?thesis .
 qed
 
+end
+
+class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
+  assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
+    and sup_compl_top: "x \<squnion> - x = \<top>"
+  assumes diff_eq: "x - y = x \<sqinter> - y"
+begin
+
+lemma dual_boolean_algebra:
+  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
+
+lemma compl_inf_bot:
+  "- x \<sqinter> x = \<bottom>"
+  by (simp add: inf_commute inf_compl_bot)
+
+lemma compl_sup_top:
+  "- x \<squnion> x = \<top>"
+  by (simp add: sup_commute sup_compl_top)
+
 lemma compl_unique:
-  assumes "x \<sqinter> y = bot"
-    and "x \<squnion> y = top"
+  assumes "x \<sqinter> y = \<bottom>"
+    and "x \<squnion> y = \<top>"
   shows "- x = y"
 proof -
   have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
@@ -393,7 +402,7 @@
     by (simp add: inf_commute)
   then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
     by (simp add: inf_sup_distrib1)
-  then have "- x \<sqinter> top = y \<sqinter> top"
+  then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
     using sup_compl_top assms(2) by simp
   then show "- x = y" by (simp add: inf_top_right)
 qed
@@ -406,8 +415,8 @@
   "- x = - y \<longleftrightarrow> x = y"
 proof
   assume "- x = - y"
-  then have "- x \<sqinter> y = bot"
-    and "- x \<squnion> y = top"
+  then have "- x \<sqinter> y = \<bottom>"
+    and "- x \<squnion> y = \<top>"
     by (simp_all add: compl_inf_bot compl_sup_top)
   then have "- (- x) = y" by (rule compl_unique)
   then show "x = y" by simp
@@ -417,16 +426,16 @@
 qed
 
 lemma compl_bot_eq [simp]:
-  "- bot = top"
+  "- \<bottom> = \<top>"
 proof -
-  from sup_compl_top have "bot \<squnion> - bot = top" .
+  from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   then show ?thesis by simp
 qed
 
 lemma compl_top_eq [simp]:
-  "- top = bot"
+  "- \<top> = \<bottom>"
 proof -
-  from inf_compl_bot have "top \<sqinter> - top = bot" .
+  from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   then show ?thesis by simp
 qed
 
@@ -437,21 +446,21 @@
     by (rule inf_sup_distrib1)
   also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
     by (simp only: inf_commute inf_assoc inf_left_commute)
-  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
+  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
     by (simp add: inf_compl_bot)
 next
   have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
     by (rule sup_inf_distrib2)
   also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
     by (simp only: sup_commute sup_assoc sup_left_commute)
-  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
+  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
     by (simp add: sup_compl_top)
 qed
 
 lemma compl_sup [simp]:
   "- (x \<squnion> y) = - x \<sqinter> - y"
 proof -
-  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
     by (rule dual_boolean_algebra)
   then show ?thesis by simp
 qed
@@ -463,26 +472,26 @@
 
 lemma (in lower_semilattice) inf_unique:
   fixes f (infixl "\<triangle>" 70)
-  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
-  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
+  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
+  and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
-  show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
+  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
 next
-  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
-  show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
+  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
 qed
 
 lemma (in upper_semilattice) sup_unique:
   fixes f (infixl "\<nabla>" 70)
-  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
-  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
+  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
+  and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
-  show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
+  show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
 next
-  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
-  show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
+  show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
 qed
   
 
@@ -568,6 +577,8 @@
 proof
 qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
+instance "fun" :: (type, bounded_lattice) bounded_lattice ..
+
 instantiation "fun" :: (type, uminus) uminus
 begin
 
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Library/List_Set.thy
--- a/src/HOL/Library/List_Set.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Library/List_Set.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -85,50 +85,6 @@
   "project P (set xs) = set (filter P xs)"
   by (auto simp add: project_def)
 
-text {* FIXME move the following to @{text Finite_Set.thy} *}
-
-lemma fun_left_comm_idem_inf:
-  "fun_left_comm_idem inf"
-proof
-qed (auto simp add: inf_left_commute)
-
-lemma fun_left_comm_idem_sup:
-  "fun_left_comm_idem sup"
-proof
-qed (auto simp add: sup_left_commute)
-
-lemma inf_Inf_fold_inf:
-  fixes A :: "'a::complete_lattice set"
-  assumes "finite A"
-  shows "inf B (Inf A) = fold inf B A"
-proof -
-  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
-  from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
-qed
-
-lemma sup_Sup_fold_sup:
-  fixes A :: "'a::complete_lattice set"
-  assumes "finite A"
-  shows "sup B (Sup A) = fold sup B A"
-proof -
-  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
-  from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
-qed
-
-lemma Inf_fold_inf:
-  fixes A :: "'a::complete_lattice set"
-  assumes "finite A"
-  shows "Inf A = fold inf top A"
-  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
-
-lemma Sup_fold_sup:
-  fixes A :: "'a::complete_lattice set"
-  assumes "finite A"
-  shows "Sup A = fold sup bot A"
-  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-
 
 subsection {* Functorial set operations *}
 
@@ -149,14 +105,6 @@
     by (simp add: minus_fold_remove [of _ A] fold_set)
 qed
 
-lemma INFI_set_fold: -- "FIXME move to List.thy"
-  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
-  unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
-
-lemma SUPR_set_fold: -- "FIXME move to List.thy"
-  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
-  unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
-
 
 subsection {* Derived set operations *}
 
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/List.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -2359,15 +2359,29 @@
 
 lemma (in complete_lattice) Inf_set_fold [code_unfold]:
   "Inf (set xs) = foldl inf top xs"
-  by (cases xs)
-    (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
-      inf_commute del: set.simps, simp add: top_def)
+proof -
+  interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact fun_left_comm_idem_inf)
+  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
+qed
 
 lemma (in complete_lattice) Sup_set_fold [code_unfold]:
   "Sup (set xs) = foldl sup bot xs"
-  by (cases xs)
-    (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
-      sup_commute del: set.simps, simp add: bot_def)
+proof -
+  interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    by (fact fun_left_comm_idem_sup)
+  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
+qed
+
+lemma (in complete_lattice) INFI_set_fold:
+  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
+  unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
+    by (simp add: inf_commute)
+
+lemma (in complete_lattice) SUPR_set_fold:
+  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
+  unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
+    by (simp add: sup_commute)
 
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Predicate.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -726,7 +726,7 @@
 proof (cases "f ()")
   case Empty
   thus ?thesis
-    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]  sup_bot)
+    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
 next
   case Insert
   thus ?thesis