# HG changeset patch
# User haftmann
# Date 1177597453 -7200
# Node ID d2b05f9462e071f19f4e47e65c8e09a43a0a6da3
# Parent  4cd25f1706bbb4b9cc80f48010f9367ae1d10532
added

diff -r 4cd25f1706bb -r d2b05f9462e0 src/HOL/Library/Pretty_Char_chr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Pretty_Char_chr.thy	Thu Apr 26 16:24:13 2007 +0200
@@ -0,0 +1,45 @@
+(*  Title:      HOL/Library/Pretty_Char_chr.thy
+    ID:         $Id$
+    Author:     Florian Haftmann
+*)
+
+header {* Code generation of pretty characters with character codes *}
+
+theory Pretty_Char_chr
+imports Char_nat Pretty_Char Pretty_Int
+begin
+
+definition
+  "int_of_char = int o nat_of_char"
+
+lemma [code func]:
+  "nat_of_char = nat o int_of_char"
+  unfolding int_of_char_def by (simp add: expand_fun_eq)
+
+definition
+  "char_of_int = char_of_nat o nat"
+
+lemma [code func]:
+  "char_of_nat = char_of_int o int"
+  unfolding char_of_int_def by (simp add: expand_fun_eq)
+
+lemmas [code nofunc] = char.recs char.cases char.size
+
+lemma [code func, code inline]:
+  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
+  by (cases c) (auto simp add: nibble_pair_of_nat_char)
+
+lemma [code func, code inline]:
+  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
+  by (cases c) (auto simp add: nibble_pair_of_nat_char)
+
+lemma [code func]:
+  "size (c\<Colon>char) = 0"
+  by (cases c) auto
+
+code_const int_of_char and char_of_int
+  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
+  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
+  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
+
+end
\ No newline at end of file