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