src/HOL/Library/Pretty_Char_chr.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22845 5f9138bcb3d7
child 24630 351a308ab58d
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/Pretty_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 Pretty_Char_chr
     9 imports Char_nat Pretty_Char Pretty_Int
    10 begin
    11 
    12 definition
    13   "int_of_char = int o nat_of_char"
    14 
    15 lemma [code func]:
    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 
    22 lemma [code func]:
    23   "char_of_nat = char_of_int o int"
    24   unfolding char_of_int_def by (simp add: expand_fun_eq)
    25 
    26 lemmas [code func del] = char.recs char.cases char.size
    27 
    28 lemma [code func, code inline]:
    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 
    32 lemma [code func, code inline]:
    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 
    36 lemma [code func]:
    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