src/HOL/Library/Char_ord.thy
changeset 19736 d8d0f8f51d69
parent 17200 3a4d03d1a31b
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/Char_ord.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -13,8 +13,6 @@
     1.4  
     1.5  consts
     1.6    nibble_to_int:: "nibble \<Rightarrow> int"
     1.7 -  int_to_nibble:: "int \<Rightarrow> nibble"
     1.8 -
     1.9  primrec
    1.10    "nibble_to_int Nibble0 = 0"
    1.11    "nibble_to_int Nibble1 = 1"
    1.12 @@ -33,25 +31,25 @@
    1.13    "nibble_to_int NibbleE = 14"
    1.14    "nibble_to_int NibbleF = 15"
    1.15  
    1.16 -defs
    1.17 -  int_to_nibble_def:
    1.18 -    "int_to_nibble x \<equiv> (let y = x mod 16 in
    1.19 -       if y = 0 then Nibble0 else
    1.20 -       if y = 1 then Nibble1 else
    1.21 -       if y = 2 then Nibble2 else
    1.22 -       if y = 3 then Nibble3 else
    1.23 -       if y = 4 then Nibble4 else
    1.24 -       if y = 5 then Nibble5 else
    1.25 -       if y = 6 then Nibble6 else
    1.26 -       if y = 7 then Nibble7 else
    1.27 -       if y = 8 then Nibble8 else
    1.28 -       if y = 9 then Nibble9 else
    1.29 -       if y = 10 then NibbleA else
    1.30 -       if y = 11 then NibbleB else
    1.31 -       if y = 12 then NibbleC else
    1.32 -       if y = 13 then NibbleD else
    1.33 -       if y = 14 then NibbleE else
    1.34 -       NibbleF)"
    1.35 +definition
    1.36 +  int_to_nibble :: "int \<Rightarrow> nibble"
    1.37 +  "int_to_nibble x \<equiv> (let y = x mod 16 in
    1.38 +    if y = 0 then Nibble0 else
    1.39 +    if y = 1 then Nibble1 else
    1.40 +    if y = 2 then Nibble2 else
    1.41 +    if y = 3 then Nibble3 else
    1.42 +    if y = 4 then Nibble4 else
    1.43 +    if y = 5 then Nibble5 else
    1.44 +    if y = 6 then Nibble6 else
    1.45 +    if y = 7 then Nibble7 else
    1.46 +    if y = 8 then Nibble8 else
    1.47 +    if y = 9 then Nibble9 else
    1.48 +    if y = 10 then NibbleA else
    1.49 +    if y = 11 then NibbleB else
    1.50 +    if y = 12 then NibbleC else
    1.51 +    if y = 13 then NibbleD else
    1.52 +    if y = 14 then NibbleE else
    1.53 +    NibbleF)"
    1.54  
    1.55  lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
    1.56    by (cases x) (auto simp: int_to_nibble_def Let_def)
    1.57 @@ -93,15 +91,9 @@
    1.58  lemmas char_ord_defs = char_less_def char_le_def
    1.59  
    1.60  instance char :: order
    1.61 -  apply intro_classes
    1.62 -     apply (unfold char_ord_defs)
    1.63 -     apply (auto simp: char_to_int_pair_eq order_less_le)
    1.64 -  done
    1.65 +  by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
    1.66  
    1.67 -instance char::linorder
    1.68 -  apply intro_classes
    1.69 -  apply (unfold char_le_def)
    1.70 -  apply auto
    1.71 -  done
    1.72 +instance char :: linorder
    1.73 +  by default (auto simp: char_le_def)
    1.74  
    1.75  end