src/HOL/Algebra/Lattice.thy

     and le_trans [trans]:
       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
     and le_cong:
       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
 
-constdefs (structure L)
+definition
   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
+  where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
 
 
 subsubsection {* The order relation *}
 
 context weak_partial_order begin

   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
 
 
 subsubsection {* Upper and lower bounds of a set *}
 
-constdefs (structure L)
+definition
   Upper :: "[_, 'a set] => 'a set"
-  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
-
+  where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
+
+definition
   Lower :: "[_, 'a set] => 'a set"
-  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
+  where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
 
 lemma Upper_closed [intro!, simp]:
   "Upper L A \<subseteq> carrier L"
   by (unfold Upper_def) clarify
 

 qed
 
 
 subsubsection {* Least and greatest, as predicate *}
 
-constdefs (structure L)
+definition
   least :: "[_, 'a, 'a set] => bool"
-  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
-
+  where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
+
+definition
   greatest :: "[_, 'a, 'a set] => bool"
-  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
+  where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
 
 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
 
 lemma least_closed [intro, simp]:

   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   by (unfold greatest_def) blast
 
 text {* Supremum and infimum *}
 
-constdefs (structure L)
+definition
   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
-  "\<Squnion>A == SOME x. least L x (Upper L A)"
-
+  where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)"
+
+definition
   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
-  "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
-
+  where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (Lower L A)"
+
+definition
   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
-  "x \<squnion> y == \<Squnion> {x, y}"
-
+  where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}"
+
+definition
   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
-  "x \<sqinter> y == \<Sqinter> {x, y}"
+  where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}"
 
 
 subsection {* Lattices *}
 
 locale weak_upper_semilattice = weak_partial_order +

     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "weak_complete_lattice L"
   proof qed (auto intro: sup_exists inf_exists)
 
-constdefs (structure L)
+definition
   top :: "_ => 'a" ("\<top>\<index>")
-  "\<top> == sup L (carrier L)"
-
+  where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)"
+
+definition
   bottom :: "_ => 'a" ("\<bottom>\<index>")
-  "\<bottom> == inf L (carrier L)"
+  where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)"
 
 
 lemma (in weak_complete_lattice) supI:
   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   ==> P (\<Squnion>A)"