11 |
11 |
12 text {* Conversions between nibbles and integers in [0..15]. *} |
12 text {* Conversions between nibbles and integers in [0..15]. *} |
13 |
13 |
14 consts |
14 consts |
15 nibble_to_int:: "nibble \<Rightarrow> int" |
15 nibble_to_int:: "nibble \<Rightarrow> int" |
16 int_to_nibble:: "int \<Rightarrow> nibble" |
|
17 |
|
18 primrec |
16 primrec |
19 "nibble_to_int Nibble0 = 0" |
17 "nibble_to_int Nibble0 = 0" |
20 "nibble_to_int Nibble1 = 1" |
18 "nibble_to_int Nibble1 = 1" |
21 "nibble_to_int Nibble2 = 2" |
19 "nibble_to_int Nibble2 = 2" |
22 "nibble_to_int Nibble3 = 3" |
20 "nibble_to_int Nibble3 = 3" |
31 "nibble_to_int NibbleC = 12" |
29 "nibble_to_int NibbleC = 12" |
32 "nibble_to_int NibbleD = 13" |
30 "nibble_to_int NibbleD = 13" |
33 "nibble_to_int NibbleE = 14" |
31 "nibble_to_int NibbleE = 14" |
34 "nibble_to_int NibbleF = 15" |
32 "nibble_to_int NibbleF = 15" |
35 |
33 |
36 defs |
34 definition |
37 int_to_nibble_def: |
35 int_to_nibble :: "int \<Rightarrow> nibble" |
38 "int_to_nibble x \<equiv> (let y = x mod 16 in |
36 "int_to_nibble x \<equiv> (let y = x mod 16 in |
39 if y = 0 then Nibble0 else |
37 if y = 0 then Nibble0 else |
40 if y = 1 then Nibble1 else |
38 if y = 1 then Nibble1 else |
41 if y = 2 then Nibble2 else |
39 if y = 2 then Nibble2 else |
42 if y = 3 then Nibble3 else |
40 if y = 3 then Nibble3 else |
43 if y = 4 then Nibble4 else |
41 if y = 4 then Nibble4 else |
44 if y = 5 then Nibble5 else |
42 if y = 5 then Nibble5 else |
45 if y = 6 then Nibble6 else |
43 if y = 6 then Nibble6 else |
46 if y = 7 then Nibble7 else |
44 if y = 7 then Nibble7 else |
47 if y = 8 then Nibble8 else |
45 if y = 8 then Nibble8 else |
48 if y = 9 then Nibble9 else |
46 if y = 9 then Nibble9 else |
49 if y = 10 then NibbleA else |
47 if y = 10 then NibbleA else |
50 if y = 11 then NibbleB else |
48 if y = 11 then NibbleB else |
51 if y = 12 then NibbleC else |
49 if y = 12 then NibbleC else |
52 if y = 13 then NibbleD else |
50 if y = 13 then NibbleD else |
53 if y = 14 then NibbleE else |
51 if y = 14 then NibbleE else |
54 NibbleF)" |
52 NibbleF)" |
55 |
53 |
56 lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x" |
54 lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x" |
57 by (cases x) (auto simp: int_to_nibble_def Let_def) |
55 by (cases x) (auto simp: int_to_nibble_def Let_def) |
58 |
56 |
59 lemma inj_nibble_to_int: "inj nibble_to_int" |
57 lemma inj_nibble_to_int: "inj nibble_to_int" |
91 char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" |
89 char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" |
92 |
90 |
93 lemmas char_ord_defs = char_less_def char_le_def |
91 lemmas char_ord_defs = char_less_def char_le_def |
94 |
92 |
95 instance char :: order |
93 instance char :: order |
96 apply intro_classes |
94 by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le) |
97 apply (unfold char_ord_defs) |
|
98 apply (auto simp: char_to_int_pair_eq order_less_le) |
|
99 done |
|
100 |
95 |
101 instance char::linorder |
96 instance char :: linorder |
102 apply intro_classes |
97 by default (auto simp: char_le_def) |
103 apply (unfold char_le_def) |
|
104 apply auto |
|
105 done |
|
106 |
98 |
107 end |
99 end |