author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 19736  d8d0f8f51d69 
child 21871  9ce66839d9f1 
permissions  rwrr 
15737  1 
(* Title: HOL/Library/Char_ord.thy 
2 
ID: $Id$ 

3 
Author: Norbert Voelker 

4 
*) 

5 

17200  6 
header {* Order on characters *} 
15737  7 

8 
theory Char_ord 

9 
imports Product_ord 

10 
begin 

11 

17200  12 
text {* Conversions between nibbles and integers in [0..15]. *} 
15737  13 

17200  14 
consts 
15737  15 
nibble_to_int:: "nibble \<Rightarrow> int" 
17200  16 
primrec 
17 
"nibble_to_int Nibble0 = 0" 

18 
"nibble_to_int Nibble1 = 1" 

19 
"nibble_to_int Nibble2 = 2" 

20 
"nibble_to_int Nibble3 = 3" 

21 
"nibble_to_int Nibble4 = 4" 

22 
"nibble_to_int Nibble5 = 5" 

23 
"nibble_to_int Nibble6 = 6" 

24 
"nibble_to_int Nibble7 = 7" 

25 
"nibble_to_int Nibble8 = 8" 

26 
"nibble_to_int Nibble9 = 9" 

27 
"nibble_to_int NibbleA = 10" 

28 
"nibble_to_int NibbleB = 11" 

29 
"nibble_to_int NibbleC = 12" 

30 
"nibble_to_int NibbleD = 13" 

31 
"nibble_to_int NibbleE = 14" 

15737  32 
"nibble_to_int NibbleF = 15" 
33 

19736  34 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

35 
int_to_nibble :: "int \<Rightarrow> nibble" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

36 
"int_to_nibble x = (let y = x mod 16 in 
19736  37 
if y = 0 then Nibble0 else 
38 
if y = 1 then Nibble1 else 

39 
if y = 2 then Nibble2 else 

40 
if y = 3 then Nibble3 else 

41 
if y = 4 then Nibble4 else 

42 
if y = 5 then Nibble5 else 

43 
if y = 6 then Nibble6 else 

44 
if y = 7 then Nibble7 else 

45 
if y = 8 then Nibble8 else 

46 
if y = 9 then Nibble9 else 

47 
if y = 10 then NibbleA else 

48 
if y = 11 then NibbleB else 

49 
if y = 12 then NibbleC else 

50 
if y = 13 then NibbleD else 

51 
if y = 14 then NibbleE else 

52 
NibbleF)" 

15737  53 

54 
lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x" 

17200  55 
by (cases x) (auto simp: int_to_nibble_def Let_def) 
15737  56 

57 
lemma inj_nibble_to_int: "inj nibble_to_int" 

17200  58 
by (rule inj_on_inverseI) (rule int_to_nibble_nibble_to_int) 
15737  59 

60 
lemmas nibble_to_int_eq = inj_nibble_to_int [THEN inj_eq] 

61 

62 
lemma nibble_to_int_ge_0: "0 \<le> nibble_to_int x" 

17200  63 
by (cases x) auto 
15737  64 

65 
lemma nibble_to_int_less_16: "nibble_to_int x < 16" 

17200  66 
by (cases x) auto 
15737  67 

68 
text {* Conversion between chars and int pairs. *} 

69 

17200  70 
consts 
15737  71 
char_to_int_pair :: "char \<Rightarrow> int \<times> int" 
72 
primrec 

17200  73 
"char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)" 
15737  74 

75 
lemma inj_char_to_int_pair: "inj char_to_int_pair" 

17200  76 
apply (rule inj_onI) 
77 
apply (case_tac x, case_tac y) 

78 
apply (auto simp: nibble_to_int_eq) 

79 
done 

15737  80 

81 
lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq] 

82 

17200  83 
text {* Instantiation of order classes *} 
15737  84 

85 
instance char :: ord .. 

86 

87 
defs (overloaded) 

17200  88 
char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)" 
89 
char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" 

15737  90 

91 
lemmas char_ord_defs = char_less_def char_le_def 

92 

17200  93 
instance char :: order 
19736  94 
by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le) 
15737  95 

19736  96 
instance char :: linorder 
97 
by default (auto simp: char_le_def) 

15737  98 

17200  99 
end 