src/HOL/Library/Code_Char_chr.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28562 4e74209f113e
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
haftmann@24999
     1
(*  Title:      HOL/Library/Code_Char_chr.thy
haftmann@24999
     2
    ID:         $Id$
haftmann@24999
     3
    Author:     Florian Haftmann
haftmann@24999
     4
*)
haftmann@24999
     5
haftmann@24999
     6
header {* Code generation of pretty characters with character codes *}
haftmann@24999
     7
haftmann@24999
     8
theory Code_Char_chr
haftmann@27368
     9
imports Plain Char_nat Code_Char Code_Integer
haftmann@24999
    10
begin
haftmann@24999
    11
haftmann@24999
    12
definition
haftmann@24999
    13
  "int_of_char = int o nat_of_char"
haftmann@24999
    14
haftmann@24999
    15
lemma [code func]:
haftmann@24999
    16
  "nat_of_char = nat o int_of_char"
haftmann@24999
    17
  unfolding int_of_char_def by (simp add: expand_fun_eq)
haftmann@24999
    18
haftmann@24999
    19
definition
haftmann@24999
    20
  "char_of_int = char_of_nat o nat"
haftmann@24999
    21
haftmann@24999
    22
lemma [code func]:
haftmann@24999
    23
  "char_of_nat = char_of_int o int"
haftmann@24999
    24
  unfolding char_of_int_def by (simp add: expand_fun_eq)
haftmann@24999
    25
haftmann@24999
    26
lemmas [code func del] = char.recs char.cases char.size
haftmann@24999
    27
haftmann@24999
    28
lemma [code func, code inline]:
haftmann@24999
    29
  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
haftmann@24999
    30
  by (cases c) (auto simp add: nibble_pair_of_nat_char)
haftmann@24999
    31
haftmann@24999
    32
lemma [code func, code inline]:
haftmann@24999
    33
  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
haftmann@24999
    34
  by (cases c) (auto simp add: nibble_pair_of_nat_char)
haftmann@24999
    35
haftmann@24999
    36
lemma [code func]:
haftmann@24999
    37
  "size (c\<Colon>char) = 0"
haftmann@24999
    38
  by (cases c) auto
haftmann@24999
    39
haftmann@24999
    40
code_const int_of_char and char_of_int
haftmann@24999
    41
  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
haftmann@24999
    42
  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
haftmann@24999
    43
  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
haftmann@24999
    44
haftmann@24999
    45
end