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