added instance for lattice
authorhaftmann
Tue Mar 20 15:52:40 2007 +0100 (2007-03-20)
changeset 2248386064f2f2188
parent 22482 8fc3d7237e03
child 22484 25dfebd7b4c8
added instance for lattice
src/HOL/Integ/IntDef.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Product_ord.thy
src/HOL/Nat.thy
src/HOL/Real/PReal.thy
     1.1 --- a/src/HOL/Integ/IntDef.thy	Tue Mar 20 15:52:39 2007 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Mar 20 15:52:40 2007 +0100
     1.3 @@ -354,21 +354,23 @@
     1.4  apply (auto simp add: zmult_zless_mono2_lemma)
     1.5  done
     1.6  
     1.7 +instance int :: minus
     1.8 +  zabs_def:  "abs(i::int) == if i < 0 then -i else i" ..
     1.9  
    1.10 -defs (overloaded)
    1.11 -    zabs_def:  "abs(i::int) == if i < 0 then -i else i"
    1.12 -
    1.13 +instance int :: distrib_lattice
    1.14 +  "inf \<equiv> min"
    1.15 +  "sup \<equiv> max"
    1.16 +  by intro_classes
    1.17 +    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
    1.18  
    1.19  text{*The integers form an ordered @{text comm_ring_1}*}
    1.20  instance int :: ordered_idom
    1.21 -  "inf \<equiv> min"
    1.22 -  "sup \<equiv> max"
    1.23  proof
    1.24    fix i j k :: int
    1.25    show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
    1.26    show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
    1.27    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
    1.28 -qed (unfold inf_int_def sup_int_def, auto)
    1.29 +qed
    1.30  
    1.31  lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
    1.32  apply (cases w, cases z) 
     2.1 --- a/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:39 2007 +0100
     2.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:40 2007 +0100
     2.3 @@ -11,25 +11,24 @@
     2.4  
     2.5  text {* Conversions between nibbles and integers in [0..15]. *}
     2.6  
     2.7 -consts
     2.8 -  nibble_to_int:: "nibble \<Rightarrow> int"
     2.9 -primrec
    2.10 +fun
    2.11 +  nibble_to_int:: "nibble \<Rightarrow> int" where
    2.12    "nibble_to_int Nibble0 = 0"
    2.13 -  "nibble_to_int Nibble1 = 1"
    2.14 -  "nibble_to_int Nibble2 = 2"
    2.15 -  "nibble_to_int Nibble3 = 3"
    2.16 -  "nibble_to_int Nibble4 = 4"
    2.17 -  "nibble_to_int Nibble5 = 5"
    2.18 -  "nibble_to_int Nibble6 = 6"
    2.19 -  "nibble_to_int Nibble7 = 7"
    2.20 -  "nibble_to_int Nibble8 = 8"
    2.21 -  "nibble_to_int Nibble9 = 9"
    2.22 -  "nibble_to_int NibbleA = 10"
    2.23 -  "nibble_to_int NibbleB = 11"
    2.24 -  "nibble_to_int NibbleC = 12"
    2.25 -  "nibble_to_int NibbleD = 13"
    2.26 -  "nibble_to_int NibbleE = 14"
    2.27 -  "nibble_to_int NibbleF = 15"
    2.28 +  | "nibble_to_int Nibble1 = 1"
    2.29 +  | "nibble_to_int Nibble2 = 2"
    2.30 +  | "nibble_to_int Nibble3 = 3"
    2.31 +  | "nibble_to_int Nibble4 = 4"
    2.32 +  | "nibble_to_int Nibble5 = 5"
    2.33 +  | "nibble_to_int Nibble6 = 6"
    2.34 +  | "nibble_to_int Nibble7 = 7"
    2.35 +  | "nibble_to_int Nibble8 = 8"
    2.36 +  | "nibble_to_int Nibble9 = 9"
    2.37 +  | "nibble_to_int NibbleA = 10"
    2.38 +  | "nibble_to_int NibbleB = 11"
    2.39 +  | "nibble_to_int NibbleC = 12"
    2.40 +  | "nibble_to_int NibbleD = 13"
    2.41 +  | "nibble_to_int NibbleE = 14"
    2.42 +  | "nibble_to_int NibbleF = 15"
    2.43  
    2.44  definition
    2.45    int_to_nibble :: "int \<Rightarrow> nibble" where
    2.46 @@ -51,7 +50,7 @@
    2.47      if y = 14 then NibbleE else
    2.48      NibbleF)"
    2.49  
    2.50 -lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
    2.51 +lemma int_to_nibble_nibble_to_int: "int_to_nibble (nibble_to_int x) = x"
    2.52    by (cases x) (auto simp: int_to_nibble_def Let_def)
    2.53  
    2.54  lemma inj_nibble_to_int: "inj nibble_to_int"
    2.55 @@ -67,9 +66,8 @@
    2.56  
    2.57  text {* Conversion between chars and int pairs. *}
    2.58  
    2.59 -consts
    2.60 -  char_to_int_pair :: "char \<Rightarrow> int \<times> int"
    2.61 -primrec
    2.62 +fun
    2.63 +  char_to_int_pair :: "char \<Rightarrow> int \<times> int" where
    2.64    "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
    2.65  
    2.66  lemma inj_char_to_int_pair: "inj char_to_int_pair"
    2.67 @@ -80,13 +78,12 @@
    2.68  
    2.69  lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
    2.70  
    2.71 +
    2.72  text {* Instantiation of order classes *}
    2.73  
    2.74 -instance char :: ord ..
    2.75 -
    2.76 -defs (overloaded)
    2.77 +instance char :: ord
    2.78    char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
    2.79 -  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
    2.80 +  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"  ..
    2.81  
    2.82  lemmas char_ord_defs = char_less_def char_le_def
    2.83  
    2.84 @@ -96,6 +93,15 @@
    2.85  instance char :: linorder
    2.86    by default (auto simp: char_le_def)
    2.87  
    2.88 +instance char :: distrib_lattice
    2.89 +  "inf \<equiv> min"
    2.90 +  "sup \<equiv> max"
    2.91 +  by intro_classes
    2.92 +    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    2.93 +
    2.94 +
    2.95 +text {* code generator setup *}
    2.96 +
    2.97  code_const char_to_int_pair
    2.98    (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
    2.99    (OCaml "failwith \"char'_to'_int'_pair\"")
     3.1 --- a/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:39 2007 +0100
     3.2 +++ b/src/HOL/Library/List_lexord.thy	Tue Mar 20 15:52:40 2007 +0100
     3.3 @@ -34,6 +34,12 @@
     3.4    apply simp
     3.5    done
     3.6  
     3.7 +instance list :: (linorder) distrib_lattice
     3.8 +  "inf \<equiv> min"
     3.9 +  "sup \<equiv> max"
    3.10 +  by intro_classes
    3.11 +    (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    3.12 +
    3.13  lemma not_less_Nil [simp]: "\<not> (x < [])"
    3.14    by (unfold list_less_def) simp
    3.15  
     4.1 --- a/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:39 2007 +0100
     4.2 +++ b/src/HOL/Library/Product_ord.thy	Tue Mar 20 15:52:40 2007 +0100
     4.3 @@ -31,4 +31,10 @@
     4.4  instance * :: (linorder, linorder) linorder
     4.5    by default (auto simp: prod_le_def)
     4.6  
     4.7 +instance * :: (linorder, linorder) distrib_lattice
     4.8 +  inf_prod_def: "inf \<equiv> min"
     4.9 +  sup_prod_def: "sup \<equiv> max"
    4.10 +  by intro_classes
    4.11 +    (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    4.12 +
    4.13  end
     5.1 --- a/src/HOL/Nat.thy	Tue Mar 20 15:52:39 2007 +0100
     5.2 +++ b/src/HOL/Nat.thy	Tue Mar 20 15:52:40 2007 +0100
     5.3 @@ -1324,6 +1324,11 @@
     5.4  by (simp del: of_nat_add
     5.5  	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
     5.6  
     5.7 +instance nat :: distrib_lattice
     5.8 +  "inf \<equiv> min"
     5.9 +  "sup \<equiv> max"
    5.10 +  by intro_classes (auto simp add: inf_nat_def sup_nat_def)
    5.11 +
    5.12  
    5.13  subsection {* Size function *}
    5.14  
     6.1 --- a/src/HOL/Real/PReal.thy	Tue Mar 20 15:52:39 2007 +0100
     6.2 +++ b/src/HOL/Real/PReal.thy	Tue Mar 20 15:52:40 2007 +0100
     6.3 @@ -219,6 +219,11 @@
     6.4  instance preal :: linorder
     6.5    by intro_classes (rule preal_le_linear)
     6.6  
     6.7 +instance preal :: distrib_lattice
     6.8 +  "inf \<equiv> min"
     6.9 +  "sup \<equiv> max"
    6.10 +  by intro_classes
    6.11 +    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
    6.12  
    6.13  
    6.14  subsection{*Properties of Addition*}