Experimenting with interpretations of "definition".

--- a/NEWS	Thu Dec 21 13:55:15 2006 +0100
+++ b/NEWS	Fri Dec 22 14:03:30 2006 +0100
@@ -710,8 +710,11 @@
 * Order and lattice theory no longer based on records.
 INCOMPATIBILITY.
 
+* Renamed lemmas least_carrier -> least_closed and
+greatest_carrier -> greatest_closed.  INCOMPATIBILITY.
+
 * Method algebra is now set up via an attribute.  For examples see
-CRing.thy.  INCOMPATIBILITY: the method is now weaker on combinations
+Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
 of algebraic structures.
 
 * Renamed `CRing.thy' to `Ring.thy'.  INCOMPATIBILITY.

--- a/src/HOL/Algebra/IntRing.thy	Thu Dec 21 13:55:15 2006 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 22 14:03:30 2006 +0100
@@ -102,7 +102,48 @@
 apply clarsimp
 done
 
-interpretation total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
+lemma less_int:
+  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
+  by (auto simp add: expand_fun_eq order_syntax.less_def)
+
+lemma join_int:
+  "order_syntax.join (UNIV::int set) (op \<le>) = max"
+  apply (simp add: expand_fun_eq max_def)
+  apply (rule+)
+  apply (rule lattice.joinI)
+  apply (simp add: int_le_total_order total_order.axioms)
+  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
+  apply arith
+  apply simp apply simp
+  apply (rule lattice.joinI)
+  apply (simp add: int_le_total_order total_order.axioms)
+  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
+  apply arith
+  apply simp apply simp
+  done
+
+lemma meet_int:
+  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
+  apply (simp add: expand_fun_eq min_def)
+  apply (rule+)
+  apply (rule lattice.meetI)
+  apply (simp add: int_le_total_order total_order.axioms)
+  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
+  apply arith
+  apply simp apply simp
+  apply (rule lattice.meetI)
+  apply (simp add: int_le_total_order total_order.axioms)
+  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
+  apply arith
+  apply simp apply simp
+  done
+
+text {* Interpretation unfolding @{text less}, @{text join} and @{text
+  meet} since they have natural representations in @{typ int}. *}
+
+interpretation 
+  int [unfolded less_int join_int meet_int]:
+  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
 
 
 subsubsection {* Generated Ideals of @{text "\<Z>"} *}

--- a/src/HOL/Algebra/Lattice.thy	Thu Dec 21 13:55:15 2006 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Fri Dec 22 14:03:30 2006 +0100
@@ -34,7 +34,7 @@
 text {* Upper and lower bounds of a set. *}
 
 definition (in order_syntax)
-  Upper where
+  Upper :: "'a set => 'a set" where
   "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L"
 
 definition (in order_syntax)

--- a/src/HOL/Algebra/Ring.thy	Thu Dec 21 13:55:15 2006 +0100
+++ b/src/HOL/Algebra/Ring.thy	Fri Dec 22 14:03:30 2006 +0100
@@ -454,7 +454,7 @@
   also from R have "... = \<zero>" by (simp add: l_neg l_null)
   finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
   with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
-  with R show ?thesis by (simp add: a_assoc r_neg )
+  with R show ?thesis by (simp add: a_assoc r_neg)
 qed
 
 lemma (in ring) r_minus: