1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Fri Oct 12 10:26:18 2007 +0200
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      HOL/Library/Code_Char_chr.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann
     1.7 +*)
     1.8 +
     1.9 +header {* Code generation of pretty characters with character codes *}
    1.10 +
    1.11 +theory Code_Char_chr
    1.12 +imports Char_nat Code_Char Code_Integer
    1.13 +begin
    1.14 +
    1.15 +definition
    1.16 +  "int_of_char = int o nat_of_char"
    1.17 +
    1.18 +lemma [code func]:
    1.19 +  "nat_of_char = nat o int_of_char"
    1.20 +  unfolding int_of_char_def by (simp add: expand_fun_eq)
    1.21 +
    1.22 +definition
    1.23 +  "char_of_int = char_of_nat o nat"
    1.24 +
    1.25 +lemma [code func]:
    1.26 +  "char_of_nat = char_of_int o int"
    1.27 +  unfolding char_of_int_def by (simp add: expand_fun_eq)
    1.28 +
    1.29 +lemmas [code func del] = char.recs char.cases char.size
    1.30 +
    1.31 +lemma [code func, code inline]:
    1.32 +  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    1.33 +  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    1.34 +
    1.35 +lemma [code func, code inline]:
    1.36 +  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    1.37 +  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    1.38 +
    1.39 +lemma [code func]:
    1.40 +  "size (c\<Colon>char) = 0"
    1.41 +  by (cases c) auto
    1.42 +
    1.43 +code_const int_of_char and char_of_int
    1.44 +  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    1.45 +  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    1.46 +  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    1.47 +
    1.48 +end
    1.49 \ No newline at end of file