# HG changeset patch
# User haftmann
# Date 1486502105 -3600
# Node ID 067a6cca39f0f3dcfa81d66afe7bdeffa8356736
# Parent  b316cd527a114eaec213264718b9c70a706fbc87
dedicated computation preprocessing rules for nat, int implemented by target language literals

diff -r b316cd527a11 -r 067a6cca39f0 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 07 22:15:04 2017 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 07 22:15:05 2017 +0100
@@ -35,7 +35,24 @@
 lemma [code_abbrev]:
   "int_of_integer (- numeral k) = Int.Neg k"
   by transfer simp
-  
+
+context
+begin  
+
+qualified definition positive :: "num \<Rightarrow> int"
+  where [simp]: "positive = numeral"
+
+qualified definition negative :: "num \<Rightarrow> int"
+  where [simp]: "negative = uminus \<circ> numeral"
+
+lemma [code_computation_unfold]:
+  "numeral = positive"
+  "Int.Pos = positive"
+  "Int.Neg = negative"
+  by (simp_all add: fun_eq_iff)
+
+end
+
 lemma [code, symmetric, code_post]:
   "0 = int_of_integer 0"
   by transfer simp
diff -r b316cd527a11 -r 067a6cca39f0 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 07 22:15:04 2017 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 07 22:15:05 2017 +0100
@@ -44,6 +44,19 @@
   "nat_of_integer (numeral k) = nat_of_num k"
   by transfer (simp add: nat_of_num_numeral)
 
+context
+begin  
+
+qualified definition natural :: "num \<Rightarrow> nat"
+  where [simp]: "natural = nat_of_num"
+
+lemma [code_computation_unfold]:
+  "numeral = natural"
+  "nat_of_num = natural"
+  by (simp_all add: nat_of_num_numeral)
+
+end
+
 lemma [code abstract]:
   "integer_of_nat (nat_of_num n) = integer_of_num n"
   by transfer (simp add: nat_of_num_numeral)