src/HOL/Lattices.thy

   less_eq  (infix "\<sqsubseteq>" 50) and
   less  (infix "\<sqsubset>" 50) and
   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"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
 begin
 
 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:
   "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   by (rule order_trans) auto

 lemma le_iff_inf:
   "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   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:
   "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   by (rule order_trans) auto

 lemma le_iff_sup:
   "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   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)
 
 end
 
 
 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)"
     by (rule antisym) (auto intro: le_infI1 le_infI2)
   show "a \<sqinter> b = b \<sqinter> a"
     by (rule antisym) auto
   show "a \<sqinter> a = a"
     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)"
   by (fact inf.assoc)
 

  
 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
 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)"
     by (rule antisym) (auto intro: le_supI1 le_supI2)
   show "a \<squnion> b = b \<squnion> a"
     by (rule antisym) auto
   show "a \<squnion> a = a"
     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)"
   by (fact sup.assoc)
 

 context lattice
 begin
 
 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"
   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
 

 
 end
 
 subsubsection {* Strict order *}
 
-context lower_semilattice
+context semilattice_inf
 begin
 
 lemma less_infI1:
   "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   by (auto simp add: less_le inf_absorb1 intro: le_infI1)

   "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   by (auto simp add: less_le inf_absorb2 intro: le_infI2)
 
 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"
     by (fact dual.less_infI1)
 qed
 
 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"
     by (fact dual.less_infI2)
 qed

 end
 
 
 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"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)

 next
   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:
+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"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)

   fix x y z
   show "max x (min y z) = min (max x y) (max x z)"
     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
 lemmas le_maxI2 = min_max.sup_ge2