# HG changeset patch
# User haftmann
# Date 1174077132 -3600
# Node ID 6070e48ecb789a9935a66e35c9984a1b9598b83b
# Parent  f6f22aba2e0ed72084e2ad2dfa2d08a7b4b859a1
added lattice definitions

diff -r f6f22aba2e0e -r 6070e48ecb78 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Mar 16 21:32:11 2007 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Mar 16 21:32:12 2007 +0100
@@ -361,13 +361,14 @@
 
 text{*The integers form an ordered @{text comm_ring_1}*}
 instance int :: ordered_idom
+  "inf \<equiv> min"
+  "sup \<equiv> max"
 proof
   fix i j k :: int
   show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
   show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
-qed
-
+qed (unfold inf_int_def sup_int_def, auto)
 
 lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
 apply (cases w, cases z) 
diff -r f6f22aba2e0e -r 6070e48ecb78 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Mar 16 21:32:11 2007 +0100
+++ b/src/HOL/Real/Rational.thy	Fri Mar 16 21:32:12 2007 +0100
@@ -348,6 +348,11 @@
   }
 qed
 
+instance rat :: distrib_lattice
+  "inf r s \<equiv> min r s"
+  "sup r s \<equiv> max r s"
+  by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
+
 instance rat :: ordered_field
 proof
   fix q r s :: rat
@@ -390,7 +395,7 @@
   qed
   show "\<bar>q\<bar> = (if q < 0 then -q else q)"
     by (simp only: abs_rat_def)
-qed
+qed auto
 
 instance rat :: division_by_zero
 proof
@@ -461,11 +466,8 @@
 
 subsection {* Numerals and Arithmetic *}
 
-instance rat :: number ..
-
-defs (overloaded)
-  rat_number_of_def: "(number_of w :: rat) == of_int w"
-    --{*the type constraint is essential!*}
+instance rat :: number
+  rat_number_of_def: "(number_of w :: rat) \<equiv> of_int w" ..
 
 instance rat :: number_ring
   by default (simp add: rat_number_of_def) 
diff -r f6f22aba2e0e -r 6070e48ecb78 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Mar 16 21:32:11 2007 +0100
+++ b/src/HOL/Real/RealDef.thy	Fri Mar 16 21:32:12 2007 +0100
@@ -434,6 +434,11 @@
 by (simp add: real_zero_def real_one_def real_le 
                  preal_self_less_add_left order_less_imp_le)
 
+instance real :: distrib_lattice
+  "inf x y \<equiv> min x y"
+  "sup x y \<equiv> max x y"
+  by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+
 
 subsection{*The Reals Form an Ordered Field*}
 
@@ -446,8 +451,6 @@
     by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
 qed
 
-
-
 text{*The function @{term real_of_preal} requires many proofs, but it seems
 to be essential for proving completeness of the reals from that of the
 positive reals.*}