--- 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)
--- 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\"")
--- 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
--- 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
--- 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 *}
--- 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*}