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