make integer_of_char and char_of_integer work with NBE and code_simp
authorAndreas Lochbihler
Wed Feb 12 09:06:04 2014 +0100 (2014-02-12)
changeset 55427ff54d22fe357
parent 55426 90f2ceed2828
child 55428 0ab52bf7b5e6
make integer_of_char and char_of_integer work with NBE and code_simp
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Char.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:56:38 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 09:06:04 2014 +0100
     1.3 @@ -230,6 +230,15 @@
     1.4      semiring_numeral_div_class.div_mult2_eq
     1.5      semiring_numeral_div_class.discrete)+
     1.6  
     1.7 +lemma integer_of_nat_0: "integer_of_nat 0 = 0"
     1.8 +by transfer simp
     1.9 +
    1.10 +lemma integer_of_nat_1: "integer_of_nat 1 = 1"
    1.11 +by transfer simp
    1.12 +
    1.13 +lemma integer_of_nat_numeral:
    1.14 +  "integer_of_nat (numeral n) = numeral n"
    1.15 +by transfer simp
    1.16  
    1.17  subsection {* Code theorems for target language integers *}
    1.18  
     2.1 --- a/src/HOL/Library/Code_Char.thy	Wed Feb 12 08:56:38 2014 +0100
     2.2 +++ b/src/HOL/Library/Code_Char.thy	Wed Feb 12 09:06:04 2014 +0100
     2.3 @@ -74,6 +74,16 @@
     2.4    "char_of_nat = char_of_integer o integer_of_nat"
     2.5    by (simp add: char_of_integer_def fun_eq_iff)
     2.6  
     2.7 +lemmas integer_of_char_code [code] =
     2.8 +  nat_of_char_simps[
     2.9 +    THEN arg_cong[where f="integer_of_nat"],
    2.10 +    unfolded integer_of_nat_numeral integer_of_nat_1 integer_of_nat_0,
    2.11 +    folded fun_cong[OF integer_of_char_def, unfolded o_apply]]
    2.12 +
    2.13 +lemma char_of_integer_code [code]:
    2.14 +  "char_of_integer n = enum_class.enum ! (nat_of_integer n mod 256)"
    2.15 +by(simp add: char_of_integer_def char_of_nat_def)
    2.16 +
    2.17  code_printing
    2.18    constant integer_of_char \<rightharpoonup>
    2.19      (SML) "!(IntInf.fromInt o Char.ord)"