src/HOL/Library/Code_Char_chr.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 48431 6efff142bb54
child 51143 0a2371e7ced3
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
haftmann@24999
     1
(*  Title:      HOL/Library/Code_Char_chr.thy
haftmann@24999
     2
    Author:     Florian Haftmann
haftmann@24999
     3
*)
haftmann@24999
     4
haftmann@24999
     5
header {* Code generation of pretty characters with character codes *}
haftmann@24999
     6
haftmann@24999
     7
theory Code_Char_chr
haftmann@30663
     8
imports Char_nat Code_Char Code_Integer Main
haftmann@24999
     9
begin
haftmann@24999
    10
haftmann@24999
    11
definition
haftmann@24999
    12
  "int_of_char = int o nat_of_char"
haftmann@24999
    13
haftmann@28562
    14
lemma [code]:
haftmann@24999
    15
  "nat_of_char = nat o int_of_char"
nipkow@39302
    16
  unfolding int_of_char_def by (simp add: fun_eq_iff)
haftmann@24999
    17
haftmann@24999
    18
definition
haftmann@24999
    19
  "char_of_int = char_of_nat o nat"
haftmann@24999
    20
haftmann@28562
    21
lemma [code]:
haftmann@24999
    22
  "char_of_nat = char_of_int o int"
nipkow@39302
    23
  unfolding char_of_int_def by (simp add: fun_eq_iff)
haftmann@24999
    24
haftmann@24999
    25
code_const int_of_char and char_of_int
haftmann@24999
    26
  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
haftmann@24999
    27
  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
haftmann@48431
    28
  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
haftmann@37222
    29
  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
haftmann@24999
    30
haftmann@37222
    31
end