src/HOL/Algebra/Lattice.thy

 (*
   Title:     HOL/Algebra/Lattice.thy
-  Id:        $Id$
   Author:    Clemens Ballarin, started 7 November 2003
   Copyright: Clemens Ballarin
 
 Most congruence rules by Stephan Hohe.
 *)

 subsection {* Partial Orders *}
 
 record 'a gorder = "'a eq_object" +
   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
 
-locale weak_partial_order = equivalence L +
+locale weak_partial_order = equivalence L for L (structure) +
   assumes le_refl [intro, simp]:
       "x \<in> carrier L ==> x \<sqsubseteq> x"
     and weak_le_anti_sym [intro]:
       "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
     and le_trans [trans]:

   shows "weak_total_order L"
   proof qed (rule total)
 
 text {* Total orders are lattices. *}
 
-interpretation weak_total_order < weak_lattice
+sublocale weak_total_order < weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   show "EX s. least L s (Upper L {x, y})"
   proof -

 
 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
-interpretation upper_semilattice < weak_upper_semilattice
+sublocale upper_semilattice < weak_upper_semilattice
   proof qed (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
-interpretation lower_semilattice < weak_lower_semilattice
+sublocale lower_semilattice < weak_lower_semilattice
   proof qed (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
 

 text {* Total Orders *}
 
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
-interpretation total_order < weak_total_order
+sublocale total_order < weak_total_order
   proof qed (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
 
 lemma (in partial_order) total_orderI:

   shows "total_order L"
   proof qed (rule total)
 
 text {* Total orders are lattices. *}
 
-interpretation total_order < lattice
+sublocale total_order < lattice
   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
 text {* Complete lattices *}
 

   assumes sup_exists:
     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-interpretation complete_lattice < weak_complete_lattice
+sublocale complete_lattice < weak_complete_lattice
   proof qed (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
 lemma (in partial_order) complete_latticeI: