diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Lattices.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -16,13 +16,13 @@
   top ("\<top>") and
   bot ("\<bottom>")
 
-class lower_semilattice = order +
+class semilattice_inf = order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
   and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
 
-class upper_semilattice = order +
+class semilattice_sup = order +
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
@@ -32,18 +32,18 @@
 text {* Dual lattice *}
 
 lemma dual_semilattice:
-  "lower_semilattice (op \<ge>) (op >) sup"
-by (rule lower_semilattice.intro, rule dual_order)
+  "semilattice_inf (op \<ge>) (op >) sup"
+by (rule semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
 
 end
 
-class lattice = lower_semilattice + upper_semilattice
+class lattice = semilattice_inf + semilattice_sup
 
 
 subsubsection {* Intro and elim rules*}
 
-context lower_semilattice
+context semilattice_inf
 begin
 
 lemma le_infI1:
@@ -69,13 +69,13 @@
   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_inf:
-  fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
   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
 
-context upper_semilattice
+context semilattice_sup
 begin
 
 lemma le_supI1:
@@ -103,7 +103,7 @@
   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_sup:
-  fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
   shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
@@ -112,7 +112,7 @@
 
 subsubsection {* Equational laws *}
 
-sublocale lower_semilattice < inf!: semilattice inf
+sublocale semilattice_inf < inf!: semilattice inf
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -123,7 +123,7 @@
     by (rule antisym) auto
 qed
 
-context lower_semilattice
+context semilattice_inf
 begin
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
@@ -151,7 +151,7 @@
 
 end
 
-sublocale upper_semilattice < sup!: semilattice sup
+sublocale semilattice_sup < sup!: semilattice sup
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
@@ -162,7 +162,7 @@
     by (rule antisym) auto
 qed
 
-context upper_semilattice
+context semilattice_sup
 begin
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
@@ -195,7 +195,7 @@
 
 lemma dual_lattice:
   "lattice (op \<ge>) (op >) sup inf"
-  by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order)
+  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -246,7 +246,7 @@
 
 subsubsection {* Strict order *}
 
-context lower_semilattice
+context semilattice_inf
 begin
 
 lemma less_infI1:
@@ -259,13 +259,13 @@
 
 end
 
-context upper_semilattice
+context semilattice_sup
 begin
 
 lemma less_supI1:
   "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
-  interpret dual: lower_semilattice "op \<ge>" "op >" sup
+  interpret dual: semilattice_inf "op \<ge>" "op >" sup
     by (fact dual_semilattice)
   assume "x \<sqsubset> a"
   then show "x \<sqsubset> a \<squnion> b"
@@ -275,7 +275,7 @@
 lemma less_supI2:
   "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
-  interpret dual: lower_semilattice "op \<ge>" "op >" sup
+  interpret dual: semilattice_inf "op \<ge>" "op >" sup
     by (fact dual_semilattice)
   assume "x \<sqsubset> b"
   then show "x \<sqsubset> a \<squnion> b"
@@ -492,7 +492,7 @@
 
 subsection {* Uniqueness of inf and sup *}
 
-lemma (in lower_semilattice) inf_unique:
+lemma (in semilattice_inf) inf_unique:
   fixes f (infixl "\<triangle>" 70)
   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"
@@ -504,7 +504,7 @@
   show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
 qed
 
-lemma (in upper_semilattice) sup_unique:
+lemma (in semilattice_sup) sup_unique:
   fixes f (infixl "\<nabla>" 70)
   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"
@@ -527,10 +527,10 @@
     by (auto simp add: min_def max_def)
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
-lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (rule ext)+ (auto intro: antisym)
 
-lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (rule ext)+ (auto intro: antisym)
 
 lemmas le_maxI1 = min_max.sup_ge1