# HG changeset patch
# User haftmann
# Date 1312834260 -7200
# Node ID caac24afcadb89747c161bb0601a088a0f05555d
# Parent  cebb7abb54b18bcac5705320cbd11e5d70b80a74# Parent  9f8790f8e589d108da50cbf7cebee4fd531b8208
merged

diff -r cebb7abb54b1 -r caac24afcadb NEWS
--- a/NEWS	Mon Aug 08 16:47:55 2011 +0200
+++ b/NEWS	Mon Aug 08 22:11:00 2011 +0200
@@ -68,6 +68,8 @@
 boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
 Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
+been discarded.
 More consistent and less misunderstandable names:
   INFI_def ~> INF_def
   SUPR_def ~> SUP_def
diff -r cebb7abb54b1 -r caac24afcadb src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Mon Aug 08 22:11:00 2011 +0200
@@ -129,13 +129,13 @@
 lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
 
-lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
+lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
   by (auto simp add: INF_def le_Inf_iff)
 
 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   by (auto intro: Sup_least dest: Sup_upper)
 
-lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
+lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
   by (auto simp add: SUP_def Sup_le_iff)
 
 lemma Inf_empty [simp]:
@@ -160,13 +160,13 @@
   "\<Squnion>UNIV = \<top>"
   by (auto intro!: antisym Sup_upper)
 
-lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
   by (simp add: INF_def Inf_insert)
 
-lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
@@ -184,22 +184,6 @@
 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_singleton [simp]:
-  "\<Sqinter>{a} = a"
-  by (auto intro: antisym Inf_lower Inf_greatest)
-
-lemma Sup_singleton [simp]:
-  "\<Squnion>{a} = a"
-  by (auto intro: antisym Sup_upper Sup_least)
-
-lemma Inf_binary:
-  "\<Sqinter>{a, b} = a \<sqinter> b"
-  by (simp add: Inf_insert)
-
-lemma Sup_binary:
-  "\<Squnion>{a, b} = a \<squnion> b"
-  by (simp add: Sup_insert)
-
 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
   by (auto intro: Inf_greatest Inf_lower)
 
@@ -306,7 +290,7 @@
   proof
     assume "\<forall>x\<in>A. x = \<top>"
     then have "A = {} \<or> A = {\<top>}" by auto
-    then show "\<Sqinter>A = \<top>" by auto
+    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
   next
     assume "\<Sqinter>A = \<top>"
     show "\<forall>x\<in>A. x = \<top>"
@@ -450,7 +434,7 @@
   and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
   fix a b c
   from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
-  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
+  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
 qed
 
 lemma Inf_sup:
@@ -704,7 +688,7 @@
   by (fact Inf_greatest)
 
 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
-  by (fact Inf_binary [symmetric])
+  by (simp add: Inf_insert)
 
 lemma Inter_empty: "\<Inter>{} = UNIV"
   by (fact Inf_empty) (* already simp *)
@@ -1212,6 +1196,22 @@
 
 text {* Legacy names *}
 
+lemma (in complete_lattice) Inf_singleton [simp]:
+  "\<Sqinter>{a} = a"
+  by (simp add: Inf_insert)
+
+lemma (in complete_lattice) Sup_singleton [simp]:
+  "\<Squnion>{a} = a"
+  by (simp add: Sup_insert)
+
+lemma (in complete_lattice) Inf_binary:
+  "\<Sqinter>{a, b} = a \<sqinter> b"
+  by (simp add: Inf_insert)
+
+lemma (in complete_lattice) Sup_binary:
+  "\<Squnion>{a, b} = a \<squnion> b"
+  by (simp add: Sup_insert)
+
 lemmas (in complete_lattice) INFI_def = INF_def
 lemmas (in complete_lattice) SUPR_def = SUP_def
 lemmas (in complete_lattice) le_SUPI = le_SUP_I
diff -r cebb7abb54b1 -r caac24afcadb src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 08 22:11:00 2011 +0200
@@ -591,7 +591,6 @@
   "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
   "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
   "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
-  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
   "UNIONS_0" > "Complete_Lattice.Union_empty"
   "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
   "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1598,7 +1597,6 @@
   "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
   "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
   "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
-  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
   "INTERS_0" > "Complete_Lattice.Inter_empty"
   "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
   "INSERT_UNION_EQ" > "Set.Un_insert_left"