# HG changeset patch
# User Andreas Lochbihler
# Date 1376495116 -7200
# Node ID 1774d569b60439e9be9340fbd2c60ca3481cfcb7
# Parent  e1a548c118453567b4afd9cbb8666f33f5af4967
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator

diff -r e1a548c11845 -r 1774d569b604 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Aug 13 18:22:55 2013 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Wed Aug 14 17:45:16 2013 +0200
@@ -123,9 +123,27 @@
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   by transfer auto
 
+lemma term_of_nat_code [code]:
+  -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
+        instead of @{term Code_Target_Nat.Nat} such that reconstructed
+        terms can be fed back to the code generator *}
+  "term_of_class.term_of n =
+   Code_Evaluation.App
+     (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
+        (typerep.Typerep (STR ''fun'')
+           [typerep.Typerep (STR ''Code_Numeral.integer'') [],
+         typerep.Typerep (STR ''Nat.nat'') []]))
+     (term_of_class.term_of (integer_of_nat n))"
+by(simp add: term_of_anything)
+
+lemma nat_of_integer_code_post [code_post]:
+  "nat_of_integer 0 = 0"
+  "nat_of_integer 1 = 1"
+  "nat_of_integer (numeral k) = numeral k"
+by(transfer, simp)+
+
 code_identifier
   code_module Code_Target_Nat \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-