wneuper/isa: src/HOL/Library/Code_Char

     1 (*  Title:      HOL/Library/Code_Char_chr.thy

     2     Author:     Florian Haftmann

     3 *)

     5 header {* Code generation of pretty characters with character codes *}

     7 theory Code_Char_chr

     8 imports Char_nat Code_Char Code_Integer Main

     9 begin

    11 definition

    12   "int_of_char = int o nat_of_char"

    14 lemma [code]:

    15   "nat_of_char = nat o int_of_char"

    16   unfolding int_of_char_def by (simp add: expand_fun_eq)

    18 definition

    19   "char_of_int = char_of_nat o nat"

    21 lemma [code]:

    22   "char_of_nat = char_of_int o int"

    23   unfolding char_of_int_def by (simp add: expand_fun_eq)

    25 lemmas [code del] = char.recs char.cases char.size

    27 lemma [code, code_inline]:

    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)

    31 lemma [code, code_inline]:

    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)

    35 lemma [code]:

    36   "size (c\<Colon>char) = 0"

    37   by (cases c) auto

    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)")

    44 end

author	haftmann
	Tue, 14 Jul 2009 10:54:04 +0200
changeset 31998	2c7a24f74db9
parent 30663	0b6aff7451b2
child 32061	6d28bbd33e2c
permissions	-rw-r--r--