src/HOL/Library/Char_ord.thy
changeset 22483 86064f2f2188
parent 21911 e29bcab0c81c
child 22805 1166a966e7b4
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:39 2007 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Mar 20 15:52:40 2007 +0100
     1.3 @@ -11,25 +11,24 @@
     1.4  
     1.5  text {* Conversions between nibbles and integers in [0..15]. *}
     1.6  
     1.7 -consts
     1.8 -  nibble_to_int:: "nibble \<Rightarrow> int"
     1.9 -primrec
    1.10 +fun
    1.11 +  nibble_to_int:: "nibble \<Rightarrow> int" where
    1.12    "nibble_to_int Nibble0 = 0"
    1.13 -  "nibble_to_int Nibble1 = 1"
    1.14 -  "nibble_to_int Nibble2 = 2"
    1.15 -  "nibble_to_int Nibble3 = 3"
    1.16 -  "nibble_to_int Nibble4 = 4"
    1.17 -  "nibble_to_int Nibble5 = 5"
    1.18 -  "nibble_to_int Nibble6 = 6"
    1.19 -  "nibble_to_int Nibble7 = 7"
    1.20 -  "nibble_to_int Nibble8 = 8"
    1.21 -  "nibble_to_int Nibble9 = 9"
    1.22 -  "nibble_to_int NibbleA = 10"
    1.23 -  "nibble_to_int NibbleB = 11"
    1.24 -  "nibble_to_int NibbleC = 12"
    1.25 -  "nibble_to_int NibbleD = 13"
    1.26 -  "nibble_to_int NibbleE = 14"
    1.27 -  "nibble_to_int NibbleF = 15"
    1.28 +  | "nibble_to_int Nibble1 = 1"
    1.29 +  | "nibble_to_int Nibble2 = 2"
    1.30 +  | "nibble_to_int Nibble3 = 3"
    1.31 +  | "nibble_to_int Nibble4 = 4"
    1.32 +  | "nibble_to_int Nibble5 = 5"
    1.33 +  | "nibble_to_int Nibble6 = 6"
    1.34 +  | "nibble_to_int Nibble7 = 7"
    1.35 +  | "nibble_to_int Nibble8 = 8"
    1.36 +  | "nibble_to_int Nibble9 = 9"
    1.37 +  | "nibble_to_int NibbleA = 10"
    1.38 +  | "nibble_to_int NibbleB = 11"
    1.39 +  | "nibble_to_int NibbleC = 12"
    1.40 +  | "nibble_to_int NibbleD = 13"
    1.41 +  | "nibble_to_int NibbleE = 14"
    1.42 +  | "nibble_to_int NibbleF = 15"
    1.43  
    1.44  definition
    1.45    int_to_nibble :: "int \<Rightarrow> nibble" where
    1.46 @@ -51,7 +50,7 @@
    1.47      if y = 14 then NibbleE else
    1.48      NibbleF)"
    1.49  
    1.50 -lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
    1.51 +lemma int_to_nibble_nibble_to_int: "int_to_nibble (nibble_to_int x) = x"
    1.52    by (cases x) (auto simp: int_to_nibble_def Let_def)
    1.53  
    1.54  lemma inj_nibble_to_int: "inj nibble_to_int"
    1.55 @@ -67,9 +66,8 @@
    1.56  
    1.57  text {* Conversion between chars and int pairs. *}
    1.58  
    1.59 -consts
    1.60 -  char_to_int_pair :: "char \<Rightarrow> int \<times> int"
    1.61 -primrec
    1.62 +fun
    1.63 +  char_to_int_pair :: "char \<Rightarrow> int \<times> int" where
    1.64    "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
    1.65  
    1.66  lemma inj_char_to_int_pair: "inj char_to_int_pair"
    1.67 @@ -80,13 +78,12 @@
    1.68  
    1.69  lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
    1.70  
    1.71 +
    1.72  text {* Instantiation of order classes *}
    1.73  
    1.74 -instance char :: ord ..
    1.75 -
    1.76 -defs (overloaded)
    1.77 +instance char :: ord
    1.78    char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
    1.79 -  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
    1.80 +  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"  ..
    1.81  
    1.82  lemmas char_ord_defs = char_less_def char_le_def
    1.83  
    1.84 @@ -96,6 +93,15 @@
    1.85  instance char :: linorder
    1.86    by default (auto simp: char_le_def)
    1.87  
    1.88 +instance char :: distrib_lattice
    1.89 +  "inf \<equiv> min"
    1.90 +  "sup \<equiv> max"
    1.91 +  by intro_classes
    1.92 +    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.93 +
    1.94 +
    1.95 +text {* code generator setup *}
    1.96 +
    1.97  code_const char_to_int_pair
    1.98    (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
    1.99    (OCaml "failwith \"char'_to'_int'_pair\"")