src/HOL/Library/Code_Target_Nat.thy
changeset 68028 1f9f973eed2a
parent 66808 1907167b6038
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -147,6 +147,21 @@
     1.4    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
     1.5    including integer.lifting by transfer auto
     1.6  
     1.7 +definition char_of_nat :: "nat \<Rightarrow> char"
     1.8 +  where [code_abbrev]: "char_of_nat = char_of"
     1.9 +
    1.10 +definition nat_of_char :: "char \<Rightarrow> nat"
    1.11 +  where [code_abbrev]: "nat_of_char = of_char"
    1.12 +
    1.13 +lemma [code]:
    1.14 +  "char_of_nat = char_of_integer \<circ> integer_of_nat"
    1.15 +  including integer.lifting unfolding char_of_integer_def char_of_nat_def
    1.16 +  by transfer (simp add: fun_eq_iff)
    1.17 +
    1.18 +lemma [code abstract]:
    1.19 +  "integer_of_nat (nat_of_char c) = integer_of_char c"
    1.20 +  by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)
    1.21 +
    1.22  lemma term_of_nat_code [code]:
    1.23    \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
    1.24          instead of @{term Code_Target_Nat.Nat} such that reconstructed