# HG changeset patch
# User Andreas Lochbihler
# Date 1392192364 -3600
# Node ID ff54d22fe357beb377fd96983940c0821330167f
# Parent  90f2ceed2828f45ff46ef2315f94f622972a3c38
make integer_of_char and char_of_integer work with NBE and code_simp

diff -r 90f2ceed2828 -r ff54d22fe357 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:56:38 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 09:06:04 2014 +0100
@@ -230,6 +230,15 @@
     semiring_numeral_div_class.div_mult2_eq
     semiring_numeral_div_class.discrete)+
 
+lemma integer_of_nat_0: "integer_of_nat 0 = 0"
+by transfer simp
+
+lemma integer_of_nat_1: "integer_of_nat 1 = 1"
+by transfer simp
+
+lemma integer_of_nat_numeral:
+  "integer_of_nat (numeral n) = numeral n"
+by transfer simp
 
 subsection {* Code theorems for target language integers *}
 
diff -r 90f2ceed2828 -r ff54d22fe357 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Wed Feb 12 08:56:38 2014 +0100
+++ b/src/HOL/Library/Code_Char.thy	Wed Feb 12 09:06:04 2014 +0100
@@ -74,6 +74,16 @@
   "char_of_nat = char_of_integer o integer_of_nat"
   by (simp add: char_of_integer_def fun_eq_iff)
 
+lemmas integer_of_char_code [code] =
+  nat_of_char_simps[
+    THEN arg_cong[where f="integer_of_nat"],
+    unfolded integer_of_nat_numeral integer_of_nat_1 integer_of_nat_0,
+    folded fun_cong[OF integer_of_char_def, unfolded o_apply]]
+
+lemma char_of_integer_code [code]:
+  "char_of_integer n = enum_class.enum ! (nat_of_integer n mod 256)"
+by(simp add: char_of_integer_def char_of_nat_def)
+
 code_printing
   constant integer_of_char \<rightharpoonup>
     (SML) "!(IntInf.fromInt o Char.ord)"