# HG changeset patch
# User haftmann
# Date 1360759132 -3600
# Node ID 7ae79f2e3cc75f3e55d46af85c2b948c246624ff
# Parent  84b03c49c2232cde27e3407fe9727e9a7f49e70d
explicit conversion integer_of_nat already in Code_Numeral_Types;
tuned code postprocessor setup: present arithmetic results as plain numerals without conversions

diff -r 84b03c49c223 -r 7ae79f2e3cc7 src/HOL/Library/Code_Numeral_Types.thy
--- a/src/HOL/Library/Code_Numeral_Types.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -83,6 +83,14 @@
   "int_of_integer (of_nat n) = of_nat n"
   by (induct n) simp_all
 
+definition integer_of_nat :: "nat \<Rightarrow> integer"
+where
+  "integer_of_nat = of_nat"
+
+lemma int_of_integer_integer_of_nat [simp]:
+  "int_of_integer (integer_of_nat n) = of_nat n"
+  by (simp add: integer_of_nat_def)
+  
 definition nat_of_integer :: "integer \<Rightarrow> nat"
 where
   "nat_of_integer k = Int.nat (int_of_integer k)"
@@ -95,7 +103,11 @@
   "int_of_integer (of_int k) = k"
   by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
 
-lemma integer_integer_of_int_eq_of_integer_integer_of_int [simp, code_abbrev]:
+lemma nat_of_integer_integer_of_nat [simp]:
+  "nat_of_integer (integer_of_nat n) = n"
+  by (simp add: integer_of_nat_def)
+
+lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   "integer_of_int = of_int"
   by rule (simp add: integer_eq_iff)
 
@@ -785,6 +797,12 @@
 where
   "Nat = natural_of_integer"
 
+lemma [code_post]:
+  "Nat 0 = 0"
+  "Nat 1 = 1"
+  "Nat (numeral k) = numeral k"
+  by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
+
 lemma [code abstype]:
   "Nat (integer_of_natural n) = n"
   by (unfold Nat_def) (fact natural_of_integer_of_natural)
diff -r 84b03c49c223 -r 7ae79f2e3cc7 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -26,18 +26,18 @@
   by (simp add: integer_of_num_def fun_eq_iff)
 
 lemma [code_abbrev]:
-  "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
+  "int_of_integer (numeral k) = Int.Pos k"
   by simp
 
 lemma [code_abbrev]:
-  "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
+  "int_of_integer (neg_numeral k) = Int.Neg k"
   by simp
-
-lemma [code]:
+  
+lemma [code, symmetric, code_post]:
   "0 = int_of_integer 0"
   by simp
 
-lemma [code]:
+lemma [code, symmetric, code_post]:
   "1 = int_of_integer 1"
   by simp
 
diff -r 84b03c49c223 -r 7ae79f2e3cc7 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -14,13 +14,15 @@
 where
   "Nat = nat_of_integer"
 
-definition integer_of_nat :: "nat \<Rightarrow> integer"
-where
-  [code_abbrev]: "integer_of_nat = of_nat"
+lemma [code_post]:
+  "Nat 0 = 0"
+  "Nat 1 = 1"
+  "Nat (numeral k) = numeral k"
+  by (simp_all add: Nat_def nat_of_integer_def)
 
-lemma int_of_integer_integer_of_nat [simp]:
-  "int_of_integer (integer_of_nat n) = of_nat n"
-  by (simp add: integer_of_nat_def)
+lemma [code_abbrev]:
+  "integer_of_nat = of_nat"
+  by (fact integer_of_nat_def)
 
 lemma [code_unfold]:
   "Int.nat (int_of_integer k) = nat_of_integer k"
@@ -35,7 +37,7 @@
   by (simp add: integer_of_nat_def)
 
 lemma [code_abbrev]:
-  "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
+  "nat_of_integer (numeral k) = nat_of_num k"
   by (simp add: nat_of_integer_def nat_of_num_numeral)
 
 lemma [code abstract]: