| author | wenzelm |
| Mon, 28 Dec 2009 22:58:25 +0100 | |
| changeset 34203 | dd2f49d88b47 |
| parent 32069 | 6d28bbd33e2c |
| child 37222 | 4d984bc33c66 |
| permissions | -rw-r--r-- |
| 24999 | 1 |
(* Title: HOL/Library/Code_Char_chr.thy |
2 |
Author: Florian Haftmann |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of pretty characters with character codes *}
|
|
6 |
||
7 |
theory Code_Char_chr |
|
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
28562
diff
changeset
|
8 |
imports Char_nat Code_Char Code_Integer Main |
| 24999 | 9 |
begin |
10 |
||
11 |
definition |
|
12 |
"int_of_char = int o nat_of_char" |
|
13 |
||
| 28562 | 14 |
lemma [code]: |
| 24999 | 15 |
"nat_of_char = nat o int_of_char" |
16 |
unfolding int_of_char_def by (simp add: expand_fun_eq) |
|
17 |
||
18 |
definition |
|
19 |
"char_of_int = char_of_nat o nat" |
|
20 |
||
| 28562 | 21 |
lemma [code]: |
| 24999 | 22 |
"char_of_nat = char_of_int o int" |
23 |
unfolding char_of_int_def by (simp add: expand_fun_eq) |
|
24 |
||
| 28562 | 25 |
lemmas [code del] = char.recs char.cases char.size |
| 24999 | 26 |
|
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
27 |
lemma [code, code_unfold]: |
| 24999 | 28 |
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))" |
29 |
by (cases c) (auto simp add: nibble_pair_of_nat_char) |
|
30 |
||
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
31 |
lemma [code, code_unfold]: |
| 24999 | 32 |
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))" |
33 |
by (cases c) (auto simp add: nibble_pair_of_nat_char) |
|
34 |
||
| 28562 | 35 |
lemma [code]: |
| 24999 | 36 |
"size (c\<Colon>char) = 0" |
37 |
by (cases c) auto |
|
38 |
||
39 |
code_const int_of_char and char_of_int |
|
40 |
(SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
|
41 |
(OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
|
42 |
(Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)") |
|
43 |
||
44 |
end |