src/HOL/Library/Char_ord.thy
changeset 17200 3a4d03d1a31b
parent 15737 c7e522520910
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:36 2005 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:37 2005 +0200
     1.3 @@ -3,39 +3,39 @@
     1.4      Author:     Norbert Voelker
     1.5  *)
     1.6  
     1.7 -header {* Instantiation of order classes type char *}
     1.8 +header {* Order on characters *}
     1.9  
    1.10  theory Char_ord
    1.11  imports Product_ord
    1.12  begin
    1.13  
    1.14 -text {* Conversions between nibbles and integers in [0..15]. *} 
    1.15 +text {* Conversions between nibbles and integers in [0..15]. *}
    1.16  
    1.17 -consts 
    1.18 +consts
    1.19    nibble_to_int:: "nibble \<Rightarrow> int"
    1.20    int_to_nibble:: "int \<Rightarrow> nibble"
    1.21  
    1.22 -primrec 
    1.23 -  "nibble_to_int Nibble0 = 0"  
    1.24 -  "nibble_to_int Nibble1 = 1" 
    1.25 -  "nibble_to_int Nibble2 = 2" 
    1.26 -  "nibble_to_int Nibble3 = 3" 
    1.27 -  "nibble_to_int Nibble4 = 4" 
    1.28 -  "nibble_to_int Nibble5 = 5" 
    1.29 -  "nibble_to_int Nibble6 = 6" 
    1.30 -  "nibble_to_int Nibble7 = 7" 
    1.31 -  "nibble_to_int Nibble8 = 8" 
    1.32 -  "nibble_to_int Nibble9 = 9" 
    1.33 -  "nibble_to_int NibbleA = 10" 
    1.34 -  "nibble_to_int NibbleB = 11" 
    1.35 -  "nibble_to_int NibbleC = 12" 
    1.36 -  "nibble_to_int NibbleD = 13" 
    1.37 -  "nibble_to_int NibbleE = 14" 
    1.38 +primrec
    1.39 +  "nibble_to_int Nibble0 = 0"
    1.40 +  "nibble_to_int Nibble1 = 1"
    1.41 +  "nibble_to_int Nibble2 = 2"
    1.42 +  "nibble_to_int Nibble3 = 3"
    1.43 +  "nibble_to_int Nibble4 = 4"
    1.44 +  "nibble_to_int Nibble5 = 5"
    1.45 +  "nibble_to_int Nibble6 = 6"
    1.46 +  "nibble_to_int Nibble7 = 7"
    1.47 +  "nibble_to_int Nibble8 = 8"
    1.48 +  "nibble_to_int Nibble9 = 9"
    1.49 +  "nibble_to_int NibbleA = 10"
    1.50 +  "nibble_to_int NibbleB = 11"
    1.51 +  "nibble_to_int NibbleC = 12"
    1.52 +  "nibble_to_int NibbleD = 13"
    1.53 +  "nibble_to_int NibbleE = 14"
    1.54    "nibble_to_int NibbleF = 15"
    1.55  
    1.56 -defs 
    1.57 -  int_to_nibble_def:  
    1.58 -    "int_to_nibble x \<equiv> (let y = x mod 16 in 
    1.59 +defs
    1.60 +  int_to_nibble_def:
    1.61 +    "int_to_nibble x \<equiv> (let y = x mod 16 in
    1.62         if y = 0 then Nibble0 else
    1.63         if y = 1 then Nibble1 else
    1.64         if y = 2 then Nibble2 else
    1.65 @@ -54,46 +54,54 @@
    1.66         NibbleF)"
    1.67  
    1.68  lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
    1.69 -  by (case_tac x, auto simp: int_to_nibble_def Let_def)
    1.70 +  by (cases x) (auto simp: int_to_nibble_def Let_def)
    1.71  
    1.72  lemma inj_nibble_to_int: "inj nibble_to_int"
    1.73 -  by (rule inj_on_inverseI, rule int_to_nibble_nibble_to_int)
    1.74 +  by (rule inj_on_inverseI) (rule int_to_nibble_nibble_to_int)
    1.75  
    1.76  lemmas nibble_to_int_eq = inj_nibble_to_int [THEN inj_eq]
    1.77  
    1.78  lemma nibble_to_int_ge_0: "0 \<le> nibble_to_int x"
    1.79 -  by (case_tac x, auto)
    1.80 +  by (cases x) auto
    1.81  
    1.82  lemma nibble_to_int_less_16: "nibble_to_int x < 16"
    1.83 -  by (case_tac x, auto)
    1.84 +  by (cases x) auto
    1.85  
    1.86  text {* Conversion between chars and int pairs. *}
    1.87  
    1.88 -consts 
    1.89 +consts
    1.90    char_to_int_pair :: "char \<Rightarrow> int \<times> int"
    1.91  primrec
    1.92 -  "char_to_int_pair(Char a b) = (nibble_to_int a, nibble_to_int b)" 
    1.93 +  "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
    1.94  
    1.95  lemma inj_char_to_int_pair: "inj char_to_int_pair"
    1.96 -  by (rule inj_onI, case_tac x, case_tac y, auto simp: nibble_to_int_eq)
    1.97 +  apply (rule inj_onI)
    1.98 +  apply (case_tac x, case_tac y)
    1.99 +  apply (auto simp: nibble_to_int_eq)
   1.100 +  done
   1.101  
   1.102  lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
   1.103  
   1.104 -text {* Instantiation of order classes *} 
   1.105 +text {* Instantiation of order classes *}
   1.106  
   1.107  instance char :: ord ..
   1.108  
   1.109  defs (overloaded)
   1.110 -  char_le_def:  "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)" 
   1.111 -  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" 
   1.112 +  char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
   1.113 +  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
   1.114  
   1.115  lemmas char_ord_defs = char_less_def char_le_def
   1.116  
   1.117 -instance char::order
   1.118 -  apply (intro_classes, unfold char_ord_defs)
   1.119 -  by (auto simp: char_to_int_pair_eq order_less_le)
   1.120 +instance char :: order
   1.121 +  apply intro_classes
   1.122 +     apply (unfold char_ord_defs)
   1.123 +     apply (auto simp: char_to_int_pair_eq order_less_le)
   1.124 +  done
   1.125  
   1.126  instance char::linorder
   1.127 -  by (intro_classes, unfold char_le_def, auto)
   1.128 +  apply intro_classes
   1.129 +  apply (unfold char_le_def)
   1.130 +  apply auto
   1.131 +  done
   1.132  
   1.133 -end
   1.134 \ No newline at end of file
   1.135 +end