src/HOL/Library/Code_Target_Int.thy
changeset 64997 067a6cca39f0
parent 64242 93c6f0da5c70
child 65552 f533820e7248
--- 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