src/HOL/Integ/IntDef.thy

   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
     dest: zless_imp_add1_zle)
 lemma [code]: "nat i = nat_aux 0 i"
   by (simp add: nat_aux_def)
 
+lemma [code unfolt]:
+  "neg k = (k < 0)"
+  unfolding neg_def ..
+
 consts_code
   "0" :: "int"                       ("0")
   "1" :: "int"                       ("1")
   "HOL.uminus" :: "int => int"       ("~")
   "HOL.plus" :: "int => int => int"  ("(_ +/ _)")

 
 code_syntax_const
   "0 :: int"
     ml (target_atom "(0:IntInf.int)")
     haskell (target_atom "0")
-  "1 :: int"
-    ml (target_atom "(1:IntInf.int)")
-    haskell (target_atom "1")
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
     ml (infixl 8 "+")
     haskell (infixl 6 "+")
   "op * :: int \<Rightarrow> int \<Rightarrow> int"
     ml (infixl 9 "*")

     ml (infix 6 "<")
     haskell (infix 4 "<")
   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
     ml (infix 6 "<=")
     haskell (infix 4 "<=")
-  "neg :: int \<Rightarrow> bool"
-    ml ("_/ </ 0")
-    haskell ("_/ </ 0")
 
 ML {*
 fun mk_int_to_nat bin =
   Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
   $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);

   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 
 *}
 
 setup {*
-  Codegen.add_codegen "number_of_codegen" number_of_codegen #>
-  CodegenPackage.add_appconst
-    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")) #>
-  CodegenPackage.set_int_tyco "IntDef.int"
+  Codegen.add_codegen "number_of_codegen" number_of_codegen
+  #> CodegenPackage.add_appconst
+       ("Numeral.number_of", ((1, 1),
+          CodegenPackage.appgen_number_of bin_to_int))
+  #> CodegenPackage.set_int_tyco "IntDef.int"
 *}
 
 quickcheck_params [default_type = int]