src/HOL/Lattices.thy

 lemma orderE:
   assumes "a \<preceq> b"
   obtains "a = a * b"
   using assms by (unfold order_iff)
 
-end
-
-sublocale semilattice_order < ordering less_eq less
+sublocale ordering less_eq less
 proof
   fix a b
   show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
     by (fact semilattice_strict_iff_order)
 next

     by (simp add: assoc)
   with `a = a * b` [symmetric] have "a = a * c" by simp
   then show "a \<preceq> c" by (rule orderI)
 qed
 
-context semilattice_order
-begin
-
 lemma cobounded1 [simp]:
   "a * b \<preceq> a"
   by (simp add: order_iff commute)  
 
 lemma cobounded2 [simp]:

   by (rule antisym) (auto simp add: refl bounded_iff)
 
 end
 
 locale semilattice_neutr_order = semilattice_neutr + semilattice_order
-
-sublocale semilattice_neutr_order < ordering_top less_eq less 1
+begin
+
+sublocale ordering_top less_eq less 1
   by default (simp add: order_iff)
+
+end
 
 notation times (infixl "*" 70)
 notation Groups.one ("1")
 
 

 end
 
 
 subsubsection {* Equational laws *}
 
-sublocale semilattice_inf < inf!: semilattice inf
+context semilattice_inf
+begin
+
+sublocale 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
 
-sublocale semilattice_sup < sup!: semilattice sup
+sublocale inf!: semilattice_order inf less_eq less
+  by default (auto simp add: le_iff_inf less_le)
+
+lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+  by (fact inf.assoc)
+
+lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
+  by (fact inf.commute)
+
+lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
+  by (fact inf.left_commute)
+
+lemma inf_idem: "x \<sqinter> x = x"
+  by (fact inf.idem) (* already simp *)
+
+lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+  by (fact inf.left_idem) (* already simp *)
+
+lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
+  by (fact inf.right_idem) (* already simp *)
+
+lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+  by (rule antisym) auto
+
+lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+  by (rule antisym) auto
+ 
+lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
+
+end
+
+context semilattice_sup
+begin
+
+sublocale 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
 
-sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
-  by default (auto simp add: le_iff_inf less_le)
-
-sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
+sublocale sup!: semilattice_order sup greater_eq greater
   by default (auto simp add: le_iff_sup sup.commute less_le)
-
-context semilattice_inf
-begin
-
-lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  by (fact inf.assoc)
-
-lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
-  by (fact inf.commute)
-
-lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
-  by (fact inf.left_commute)
-
-lemma inf_idem: "x \<sqinter> x = x"
-  by (fact inf.idem) (* already simp *)
-
-lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-  by (fact inf.left_idem) (* already simp *)
-
-lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
-  by (fact inf.right_idem) (* already simp *)
-
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
-  by (rule antisym) auto
-
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
-  by (rule antisym) auto
- 
-lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
-
-end
-
-context semilattice_sup
-begin
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   by (fact sup.assoc)
 
 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"

 
 
 subsection {* Bounded lattices and boolean algebras *}
 
 class bounded_semilattice_inf_top = semilattice_inf + top
-
-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+begin
+
+sublocale inf_top!: semilattice_neutr inf top
   + inf_top!: semilattice_neutr_order inf top less_eq less
 proof
   fix x
   show "x \<sqinter> \<top> = x"
     by (rule inf_absorb1) simp
 qed
 
+end
+
 class bounded_semilattice_sup_bot = semilattice_sup + bot
-
-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+begin
+
+sublocale sup_bot!: semilattice_neutr sup bot
   + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
 proof
   fix x
   show "x \<squnion> \<bottom> = x"
     by (rule sup_absorb1) simp
 qed
+
+end
 
 class bounded_lattice_bot = lattice + bot
 begin
 
 subclass bounded_semilattice_sup_bot ..