src/HOL/Library/Code_Char_chr.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 32069 6d28bbd33e2c
child 37222 4d984bc33c66
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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
     8 imports Char_nat Code_Char Code_Integer Main
     9 begin
    10 
    11 definition
    12   "int_of_char = int o nat_of_char"
    13 
    14 lemma [code]:
    15   "nat_of_char = nat o int_of_char"
    16   unfolding int_of_char_def by (simp add: expand_fun_eq)
    17 
    18 definition
    19   "char_of_int = char_of_nat o nat"
    20 
    21 lemma [code]:
    22   "char_of_nat = char_of_int o int"
    23   unfolding char_of_int_def by (simp add: expand_fun_eq)
    24 
    25 lemmas [code del] = char.recs char.cases char.size
    26 
    27 lemma [code, code_unfold]:
    28   "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    29   by (cases c) (auto simp add: nibble_pair_of_nat_char)
    30 
    31 lemma [code, code_unfold]:
    32   "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    33   by (cases c) (auto simp add: nibble_pair_of_nat_char)
    34 
    35 lemma [code]:
    36   "size (c\<Colon>char) = 0"
    37   by (cases c) auto
    38 
    39 code_const int_of_char and char_of_int
    40   (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    41   (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    42   (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    43 
    44 end