author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 48431 | 6efff142bb54 |
child 51143 | 0a2371e7ced3 |
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" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
16 |
unfolding int_of_char_def by (simp add: fun_eq_iff) |
24999 | 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" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
23 |
unfolding char_of_int_def by (simp add: fun_eq_iff) |
24999 | 24 |
|
25 |
code_const int_of_char and char_of_int |
|
26 |
(SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
|
27 |
(OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
|
48431
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
39302
diff
changeset
|
28 |
(Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)") |
37222 | 29 |
(Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
24999 | 30 |
|
37222 | 31 |
end |