# HG changeset patch
# User haftmann
# Date 1174402360 -3600
# Node ID 86064f2f2188ac6beb645549be170daa03550f51
# Parent  8fc3d7237e03464554c465e4b773d90d8a653e32
added instance for lattice

diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -354,21 +354,23 @@
 apply (auto simp add: zmult_zless_mono2_lemma)
 done
 
+instance int :: minus
+  zabs_def:  "abs(i::int) == if i < 0 then -i else i" ..
 
-defs (overloaded)
-    zabs_def:  "abs(i::int) == if i < 0 then -i else i"
-
+instance int :: distrib_lattice
+  "inf \<equiv> min"
+  "sup \<equiv> max"
+  by intro_classes
+    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
 
 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 (unfold inf_int_def sup_int_def, auto)
+qed
 
 lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
 apply (cases w, cases z) 
diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -11,25 +11,24 @@
 
 text {* Conversions between nibbles and integers in [0..15]. *}
 
-consts
-  nibble_to_int:: "nibble \<Rightarrow> int"
-primrec
+fun
+  nibble_to_int:: "nibble \<Rightarrow> int" where
   "nibble_to_int Nibble0 = 0"
-  "nibble_to_int Nibble1 = 1"
-  "nibble_to_int Nibble2 = 2"
-  "nibble_to_int Nibble3 = 3"
-  "nibble_to_int Nibble4 = 4"
-  "nibble_to_int Nibble5 = 5"
-  "nibble_to_int Nibble6 = 6"
-  "nibble_to_int Nibble7 = 7"
-  "nibble_to_int Nibble8 = 8"
-  "nibble_to_int Nibble9 = 9"
-  "nibble_to_int NibbleA = 10"
-  "nibble_to_int NibbleB = 11"
-  "nibble_to_int NibbleC = 12"
-  "nibble_to_int NibbleD = 13"
-  "nibble_to_int NibbleE = 14"
-  "nibble_to_int NibbleF = 15"
+  | "nibble_to_int Nibble1 = 1"
+  | "nibble_to_int Nibble2 = 2"
+  | "nibble_to_int Nibble3 = 3"
+  | "nibble_to_int Nibble4 = 4"
+  | "nibble_to_int Nibble5 = 5"
+  | "nibble_to_int Nibble6 = 6"
+  | "nibble_to_int Nibble7 = 7"
+  | "nibble_to_int Nibble8 = 8"
+  | "nibble_to_int Nibble9 = 9"
+  | "nibble_to_int NibbleA = 10"
+  | "nibble_to_int NibbleB = 11"
+  | "nibble_to_int NibbleC = 12"
+  | "nibble_to_int NibbleD = 13"
+  | "nibble_to_int NibbleE = 14"
+  | "nibble_to_int NibbleF = 15"
 
 definition
   int_to_nibble :: "int \<Rightarrow> nibble" where
@@ -51,7 +50,7 @@
     if y = 14 then NibbleE else
     NibbleF)"
 
-lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
+lemma int_to_nibble_nibble_to_int: "int_to_nibble (nibble_to_int x) = x"
   by (cases x) (auto simp: int_to_nibble_def Let_def)
 
 lemma inj_nibble_to_int: "inj nibble_to_int"
@@ -67,9 +66,8 @@
 
 text {* Conversion between chars and int pairs. *}
 
-consts
-  char_to_int_pair :: "char \<Rightarrow> int \<times> int"
-primrec
+fun
+  char_to_int_pair :: "char \<Rightarrow> int \<times> int" where
   "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
 
 lemma inj_char_to_int_pair: "inj char_to_int_pair"
@@ -80,13 +78,12 @@
 
 lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
 
+
 text {* Instantiation of order classes *}
 
-instance char :: ord ..
-
-defs (overloaded)
+instance char :: ord
   char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
-  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
+  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"  ..
 
 lemmas char_ord_defs = char_less_def char_le_def
 
@@ -96,6 +93,15 @@
 instance char :: linorder
   by default (auto simp: char_le_def)
 
+instance char :: distrib_lattice
+  "inf \<equiv> min"
+  "sup \<equiv> max"
+  by intro_classes
+    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
+
+
+text {* code generator setup *}
+
 code_const char_to_int_pair
   (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
   (OCaml "failwith \"char'_to'_int'_pair\"")
diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -34,6 +34,12 @@
   apply simp
   done
 
+instance list :: (linorder) distrib_lattice
+  "inf \<equiv> min"
+  "sup \<equiv> max"
+  by intro_classes
+    (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
+
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp
 
diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -31,4 +31,10 @@
 instance * :: (linorder, linorder) linorder
   by default (auto simp: prod_le_def)
 
+instance * :: (linorder, linorder) distrib_lattice
+  inf_prod_def: "inf \<equiv> min"
+  sup_prod_def: "sup \<equiv> max"
+  by intro_classes
+    (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+
 end
diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -1324,6 +1324,11 @@
 by (simp del: of_nat_add
 	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
 
+instance nat :: distrib_lattice
+  "inf \<equiv> min"
+  "sup \<equiv> max"
+  by intro_classes (auto simp add: inf_nat_def sup_nat_def)
+
 
 subsection {* Size function *}
 
diff -r 8fc3d7237e03 -r 86064f2f2188 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Tue Mar 20 15:52:39 2007 +0100
+++ b/src/HOL/Real/PReal.thy	Tue Mar 20 15:52:40 2007 +0100
@@ -219,6 +219,11 @@
 instance preal :: linorder
   by intro_classes (rule preal_le_linear)
 
+instance preal :: distrib_lattice
+  "inf \<equiv> min"
+  "sup \<equiv> max"
+  by intro_classes
+    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
 
 
 subsection{*Properties of Addition*}