# HG changeset patch
# User huffman
# Date 1312827918 25200
# Node ID 5feac96f0e78602ca4064643e04b1ef9e9a5cc10
# Parent  d74182c93f04072a463d2a92486ae10a2d3b51e9
declare {INF,SUP}_empty [simp]

diff -r d74182c93f04 -r 5feac96f0e78 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 10:32:55 2011 -0700
+++ b/src/HOL/Complete_Lattice.thy	Mon Aug 08 11:25:18 2011 -0700
@@ -142,14 +142,14 @@
   "\<Sqinter>{} = \<top>"
   by (auto intro: antisym Inf_greatest)
 
-lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
+lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
   by (simp add: INF_def)
 
 lemma Sup_empty [simp]:
   "\<Squnion>{} = \<bottom>"
   by (auto intro: antisym Sup_least)
 
-lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
+lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   by (simp add: SUP_def)
 
 lemma Inf_UNIV [simp]:
@@ -700,11 +700,11 @@
 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
   by (fact Inf_binary [symmetric])
 
-lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
-  by (fact Inf_empty)
+lemma Inter_empty: "\<Inter>{} = UNIV"
+  by (fact Inf_empty) (* already simp *)
 
-lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
-  by (fact Inf_UNIV)
+lemma Inter_UNIV: "\<Inter>UNIV = {}"
+  by (fact Inf_UNIV) (* already simp *)
 
 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   by (fact Inf_insert)
@@ -801,8 +801,8 @@
 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
   by (fact le_INF_I)
 
-lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
-  by (fact INF_empty)
+lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
+  by (fact INF_empty) (* already simp *)
 
 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
   by (fact INF_absorb)
@@ -1010,8 +1010,8 @@
 lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
-lemma UN_empty [simp, no_atp]: "(\<Union>x\<in>{}. B x) = {}"
-  by (fact SUP_empty)
+lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
+  by (fact SUP_empty) (* already simp *)
 
 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
   by (fact SUP_bot)