# HG changeset patch
# User haftmann
# Date 1177587185 -7200
# Node ID caffcb450ef4d7f22fe2c663b2994aa6617d1ac0
# Parent  eaf5e7ef35d9a4299a8419b3eb39b758ed179a1e
cleaned up code generator setup for int

diff -r eaf5e7ef35d9 -r caffcb450ef4 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu Apr 26 13:33:04 2007 +0200
+++ b/src/HOL/Integ/IntArith.thy	Thu Apr 26 13:33:05 2007 +0200
@@ -14,13 +14,6 @@
 declare numeral_0_eq_0 [simp]
 
 
-subsection{*Instantiating Binary Arithmetic for the Integers*}
-
-instance int :: number_ring
-  int_number_of_def: "number_of w \<equiv> of_int w"
-  by intro_classes (simp only: int_number_of_def)
-
-
 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
 
 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
@@ -191,8 +184,7 @@
 
 text{*This simplifies expressions of the form @{term "int n = z"} where
       z is an integer literal.*}
-lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard]
-declare int_eq_iff_number_of [simp]
+lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
 
 
 lemma split_nat [arith_split]:
@@ -217,7 +209,7 @@
 by (induct m n rule: diff_induct, simp_all)
 
 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
-apply (case_tac "0 \<le> z'")
+apply (cases "0 \<le> z'")
 apply (rule inj_int [THEN injD])
 apply (simp add: int_mult zero_le_mult_iff)
 apply (simp add: mult_le_0_iff)
@@ -229,7 +221,7 @@
 done
 
 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
-apply (case_tac "z=0 | w=0")
+apply (cases "z=0 | w=0")
 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
 done
@@ -375,7 +367,7 @@
 by arith
 
 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
-apply (case_tac "\<bar>n\<bar>=1") 
+apply (cases "\<bar>n\<bar>=1") 
 apply (simp add: abs_mult) 
 apply (rule ccontr) 
 apply (auto simp add: linorder_neq_iff abs_mult) 
@@ -402,110 +394,12 @@
 done
 
 
-subsection {* code generator setup *}
-
-code_modulename SML
-  Numeral Integer
-
-code_modulename OCaml
-  Numeral Integer
-
-lemma Numeral_Pls_refl [code func]:
-  "Numeral.Pls = Numeral.Pls" ..
-
-lemma Numeral_Min_refl [code func]:
-  "Numeral.Min = Numeral.Min" ..
-
-lemma zero_int_refl [code func]:
-  "(0\<Colon>int) = 0" ..
-
-lemma one_int_refl [code func]:
-  "(1\<Colon>int) = 1" ..
-
-lemma number_of_int_refl [code func]:
-  "(number_of \<Colon> int \<Rightarrow> int) = number_of" ..
-
-lemma number_of_is_id:
-  "number_of (k::int) = k"
-  unfolding int_number_of_def by simp
-
-lemma zero_is_num_zero [code inline, symmetric, normal post]:
-  "(0::int) = number_of Numeral.Pls" 
-  by simp
-
-lemma one_is_num_one [code inline, symmetric, normal post]:
-  "(1::int) = number_of  (Numeral.Pls BIT bit.B1)" 
-  by simp 
-
-lemmas int_code_rewrites =
-  arith_simps(5-27)
-  arith_extra_simps(1-5) [where 'a = int]
-
-declare int_code_rewrites [code func]
-
-code_type bit
-  (SML "bool")
-  (OCaml "bool")
-  (Haskell "Bool")
-code_const "Numeral.bit.B0" and "Numeral.bit.B1"
-  (SML "false" and "true")
-  (OCaml "false" and "true")
-  (Haskell "False" and "True")
+subsection {* Legavy ML bindings *}
 
-code_const "number_of \<Colon> int \<Rightarrow> int"
-  and "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
-  and "Numeral.succ" and "Numeral.pred"
-  (SML "_"
-     and "0/ :/ IntInf.int"
-     and "~1/ :/ IntInf.int"
-     and "!(_; _; raise Fail \"BIT\")"
-     and "IntInf.+/ (_,/ 1)"
-     and "IntInf.-/ (_,/ 1))")
-  (OCaml "_"
-     and "Big'_int.big'_int'_of'_int/ 0"
-     and "Big'_int.big'_int'_of'_int/ (-1)"
-     and "!(_; _; failwith \"BIT\")"
-     and "Big'_int.succ'_big'_int"
-     and "Big'_int.pred'_big'_int")
-  (Haskell "_"
-     and "0"
-     and "!(-1)"
-     and "error/ \"BIT\""
-     and "(+)/ 1"
-     and "(-)/ _/ 1")
-
-setup {*
-  CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral (try HOLogic.dest_numeral))
-*}
-
-
-subsection {* legacy ML bindings *}
-
-ML
-{*
-val zle_diff1_eq = thm "zle_diff1_eq";
-val zle_add1_eq_le = thm "zle_add1_eq_le";
-val nonneg_eq_int = thm "nonneg_eq_int";
-val abs_minus_one = thm "abs_minus_one";
-val of_int_number_of_eq = thm"of_int_number_of_eq";
-val nat_eq_iff = thm "nat_eq_iff";
-val nat_eq_iff2 = thm "nat_eq_iff2";
-val nat_less_iff = thm "nat_less_iff";
-val int_eq_iff = thm "int_eq_iff";
-val nat_0 = thm "nat_0";
-val nat_1 = thm "nat_1";
-val nat_2 = thm "nat_2";
-val nat_less_eq_zless = thm "nat_less_eq_zless";
-val nat_le_eq_zle = thm "nat_le_eq_zle";
-
-val nat_intermed_int_val = thm "nat_intermed_int_val";
-val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
-val zmult_eq_1_iff = thm "zmult_eq_1_iff";
-val nat_add_distrib = thm "nat_add_distrib";
-val nat_diff_distrib = thm "nat_diff_distrib";
-val nat_mult_distrib = thm "nat_mult_distrib";
-val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
-val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
+ML {*
+val of_int_number_of_eq = @{thm of_int_number_of_eq};
+val nat_0 = @{thm nat_0};
+val nat_1 = @{thm nat_1};
 *}
 
 end
diff -r eaf5e7ef35d9 -r caffcb450ef4 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Apr 26 13:33:04 2007 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Apr 26 13:33:05 2007 +0200
@@ -11,47 +11,50 @@
 imports Equiv_Relations Nat
 begin
 
-constdefs
-  intrel :: "((nat * nat) * (nat * nat)) set"
-    --{*the equivalence relation underlying the integers*}
-    "intrel == {((x,y),(u,v)) | x y u v. x+v = u+y}"
+text {* the equivalence relation underlying the integers *}
+
+definition
+  intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
+where
+  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)
   int = "UNIV//intrel"
-    by (auto simp add: quotient_def)
-
-instance int :: "{ord, zero, one, plus, times, minus}" ..
+  by (auto simp add: quotient_def)
 
-constdefs
-  int :: "nat => int"
-  "int m == Abs_Integ(intrel `` {(m,0)})"
+definition
+  int :: "nat \<Rightarrow> int"
+where
+  [code nofunc]: "int m = Abs_Integ (intrel `` {(m, 0)})"
 
-
-defs (overloaded)
+instance int :: zero
+  Zero_int_def: "0 \<equiv> int 0" ..
 
-  Zero_int_def:  "0 == int 0"
-  One_int_def:   "1 == int 1"
+instance int :: one
+  One_int_def: "1 \<equiv> int 1" ..
 
-  minus_int_def:
-    "- z == Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. intrel``{(y,x)})"
+instance int :: plus
+  add_int_def: "z + w \<equiv> Abs_Integ
+    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
+      intrel `` {(x + u, y + v)})" ..
 
-  add_int_def:
-   "z + w ==
-       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
-		 intrel``{(x+u, y+v)})"
-
-  diff_int_def:  "z - (w::int) == z + (-w)"
+instance int :: minus
+  minus_int_def:
+    "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
+  diff_int_def:  "z - w \<equiv> z + (-w)" ..
 
-  mult_int_def:
-   "z * w ==
-       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
-		  intrel``{(x*u + y*v, x*v + y*u)})"
+instance int :: times
+  mult_int_def: "z * w \<equiv>  Abs_Integ
+    (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
+      intrel `` {(x*u + y*v, x*v + y*u)})" ..
 
+instance int :: ord
   le_int_def:
-   "z \<le> (w::int) == 
-    \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Integ z & (u,v) \<in> Rep_Integ w"
+   "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
+  less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
 
-  less_int_def: "(z < (w::int)) == (z \<le> w & z \<noteq> w)"
+lemmas [code nofunc] = Zero_int_def One_int_def add_int_def
+  minus_int_def mult_int_def le_int_def less_int_def
 
 
 subsection{*Construction of the Integers*}
@@ -66,10 +69,7 @@
 
 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
-lemmas equiv_intrel_iff = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
-
-declare equiv_intrel_iff [simp]
-
+lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
 
 text{*All equivalence classes belong to set of representatives*}
 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
@@ -154,9 +154,6 @@
 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   by (simp add: zadd_int zadd_assoc [symmetric])
 
-lemma int_Suc: "int (Suc m) = 1 + (int m)"
-  by (simp add: One_int_def zadd_int)
-
 (*also for the instance declaration int :: comm_monoid_add*)
 lemma zadd_0: "(0::int) + z = z"
 apply (simp add: Zero_int_def int_def)
@@ -268,14 +265,12 @@
     (assumption |
       rule zle_refl zle_trans zle_anti_sym less_int_def [THEN meta_eq_to_obj_eq])+
 
-(* Axiom 'linorder_linear' of class 'linorder': *)
-lemma zle_linear: "(z::int) \<le> w | w \<le> z"
+lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
 by (cases z, cases w) (simp add: le linorder_linear)
 
 instance int :: linorder
   by intro_classes (rule zle_linear)
 
-
 lemmas zless_linear = linorder_less_linear [where 'a = int]
 
 
@@ -315,6 +310,9 @@
 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
 by (simp add: One_int_def One_nat_def)
 
+lemma int_Suc: "int (Suc m) = 1 + (int m)"
+by (simp add: One_int_def zadd_int)
+
 
 subsection{*Monotonicity results*}
 
@@ -355,7 +353,7 @@
 done
 
 instance int :: minus
-  zabs_def:  "abs(i::int) == if i < 0 then -i else i" ..
+  zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
 
 instance int :: distrib_lattice
   "inf \<equiv> min"
@@ -379,9 +377,10 @@
 
 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
 
-constdefs
-   nat  :: "int => nat"
-    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })"
+definition
+  nat :: "int \<Rightarrow> nat"
+where
+  [code nofunc]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
 
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
@@ -514,16 +513,14 @@
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
 
-
-subsection{*The Constants @{term neg} and @{term iszero}*}
+subsection {* Constants @{term neg} and @{term iszero} *}
 
 definition
   neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
 where
-  "neg Z \<longleftrightarrow> Z < 0"
+  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
 
-definition
-  (*For simplifying equalities*)
+definition (*for simplifying equalities*)
   iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
 where
   "iszero z \<longleftrightarrow> z = 0"
@@ -658,20 +655,18 @@
 done
 
 text{*Special cases where either operand is zero*}
-lemmas of_int_0_le_iff = of_int_le_iff [of 0, simplified]
-lemmas of_int_le_0_iff = of_int_le_iff [of _ 0, simplified]
-declare of_int_0_le_iff [simp]
-declare of_int_le_0_iff [simp]
+lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
+lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
+
 
 lemma of_int_less_iff [simp]:
      "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
 by (simp add: linorder_not_le [symmetric])
 
 text{*Special cases where either operand is zero*}
-lemmas of_int_0_less_iff = of_int_less_iff [of 0, simplified]
-lemmas of_int_less_0_iff = of_int_less_iff [of _ 0, simplified]
-declare of_int_0_less_iff [simp]
-declare of_int_less_0_iff [simp]
+lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
+lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
+
 
 text{*The ordering on the @{text ring_1} is necessary.
  See @{text of_nat_eq_iff} above.*}
@@ -680,10 +675,8 @@
 by (simp add: order_eq_iff)
 
 text{*Special cases where either operand is zero*}
-lemmas of_int_0_eq_iff = of_int_eq_iff [of 0, simplified]
-lemmas of_int_eq_0_iff = of_int_eq_iff [of _ 0, simplified]
-declare of_int_0_eq_iff [simp]
-declare of_int_eq_0_iff [simp]
+lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
+lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
 
 lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
 proof
@@ -762,7 +755,7 @@
 
 
 (* int (Suc n) = 1 + int n *)
-declare int_Suc [simp]
+
 
 
 subsection{*More Properties of @{term setsum} and  @{term setprod}*}
@@ -813,6 +806,8 @@
   by (rule setprod_zero_eq, auto)
 
 
+subsection {* Further properties *}
+
 text{*Now we replace the case analysis rule by a more conventional one:
 whether an integer is negative or not.*}
 
@@ -833,7 +828,7 @@
 
 theorem int_cases [cases type: int, case_names nonneg neg]:
      "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
-apply (case_tac "z < 0", blast dest!: negD)
+apply (cases "z < 0", blast dest!: negD)
 apply (simp add: linorder_not_less)
 apply (blast dest: nat_0_le [THEN sym])
 done
@@ -857,248 +852,33 @@
 
 lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
 
-subsection {* Configuration of the code generator *}
-
-(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
-
-types_code
-  "int" ("int")
-attach (term_of) {*
-val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
-*}
-attach (test) {*
-fun gen_int i = one_of [~1, 1] * random_range 0 i;
-*}
-
-definition
-  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
-  "int_aux i n = (i + int n)"
-
-definition
-  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
-  "nat_aux n i = (n + nat i)"
-
-lemma [code]:
-  "int_aux i 0 = i"
-  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
-  "int n = int_aux 0 n"
-  by (simp add: int_aux_def)+
-
-lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
-  -- {* tail recursive *}
-  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 inline]:
-  "neg k \<longleftrightarrow> k < 0"
-  unfolding neg_def ..
-
-lemma [code func]:
-  "\<bar>k\<Colon>int\<bar> = (if k < 0 then - k else k)"
-  unfolding zabs_def ..
-
-consts_code
-  "HOL.zero" :: "int"                ("0")
-  "HOL.one" :: "int"                 ("1")
-  "HOL.uminus" :: "int => int"       ("~")
-  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
-  "HOL.times" :: "int => int => int" ("(_ */ _)")
-  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
-  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
-  "neg"                              ("(_ < 0)")
+lemmas [simp] = int_Suc
 
-instance int :: eq ..
 
-code_type int
-  (SML "IntInf.int")
-  (OCaml "Big'_int.big'_int")
-  (Haskell "Integer")
-
-code_instance int :: eq
-  (Haskell -)
-
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "!((_ : IntInf.int) = _)")
-  (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.<= (_, _)")
-  (OCaml "Big'_int.le'_big'_int")
-  (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.< (_, _)")
-  (OCaml "Big'_int.lt'_big'_int")
-  (Haskell infix 4 "<")
-
-code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.+ (_, _)")
-  (OCaml "Big'_int.add'_big'_int")
-  (Haskell infixl 6 "+")
-
-code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.- (_, _)")
-  (OCaml "Big'_int.sub'_big'_int")
-  (Haskell infixl 6 "-")
-
-code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.* (_, _)")
-  (OCaml "Big'_int.mult'_big'_int")
-  (Haskell infixl 7 "*")
-
-code_const "uminus \<Colon> int \<Rightarrow> int"
-  (SML "IntInf.~")
-  (OCaml "Big'_int.minus'_big'_int")
-  (Haskell "negate")
-
-code_reserved SML IntInf
-code_reserved OCaml Big_int
-
-code_modulename SML
-  IntDef Integer
-
-code_modulename Haskell
-  IntDef Integer
+subsection {* Legacy ML bindings *}
 
 ML {*
-fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
-      if T = HOLogic.intT then
-        (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
-          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
-      else if T = HOLogic.natT then
-        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
-          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
-      else NONE
-  | number_of_codegen _ _ _ _ _ _ _ = NONE;
-*}
-
-setup {*
-  Codegen.add_codegen "number_of_codegen" number_of_codegen
+val of_nat_0 = @{thm of_nat_0};
+val of_nat_1 = @{thm of_nat_1};
+val of_nat_Suc = @{thm of_nat_Suc};
+val of_nat_add = @{thm of_nat_add};
+val of_nat_mult = @{thm of_nat_mult};
+val of_int_0 = @{thm of_int_0};
+val of_int_1 = @{thm of_int_1};
+val of_int_add = @{thm of_int_add};
+val of_int_mult = @{thm of_int_mult};
+val int_eq_of_nat = @{thm int_eq_of_nat};
+val zle_int = @{thm zle_int};
+val int_int_eq = @{thm int_int_eq};
+val diff_int_def = @{thm diff_int_def};
+val zadd_ac = @{thms zadd_ac};
+val zless_int = @{thm zless_int};
+val zadd_int = @{thm zadd_int};
+val zmult_int = @{thm zmult_int};
+val nat_0_le = @{thm nat_0_le};
+val int_0 = @{thm int_0};
+val int_1 = @{thm int_1};
+val abs_split = @{thm abs_split};
 *}
 
-quickcheck_params [default_type = int]
-
-
-(*Legacy ML bindings, but no longer the structure Int.*)
-ML
-{*
-val zabs_def = thm "zabs_def"
-
-val int_0 = thm "int_0";
-val int_1 = thm "int_1";
-val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
-val neg_eq_less_0 = thm "neg_eq_less_0";
-val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
-val not_neg_0 = thm "not_neg_0";
-val not_neg_1 = thm "not_neg_1";
-val iszero_0 = thm "iszero_0";
-val not_iszero_1 = thm "not_iszero_1";
-val int_0_less_1 = thm "int_0_less_1";
-val int_0_neq_1 = thm "int_0_neq_1";
-val negative_zless = thm "negative_zless";
-val negative_zle = thm "negative_zle";
-val not_zle_0_negative = thm "not_zle_0_negative";
-val not_int_zless_negative = thm "not_int_zless_negative";
-val negative_eq_positive = thm "negative_eq_positive";
-val zle_iff_zadd = thm "zle_iff_zadd";
-val abs_int_eq = thm "abs_int_eq";
-val abs_split = thm"abs_split";
-val nat_int = thm "nat_int";
-val nat_zminus_int = thm "nat_zminus_int";
-val nat_zero = thm "nat_zero";
-val not_neg_nat = thm "not_neg_nat";
-val neg_nat = thm "neg_nat";
-val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
-val nat_0_le = thm "nat_0_le";
-val nat_le_0 = thm "nat_le_0";
-val zless_nat_conj = thm "zless_nat_conj";
-val int_cases = thm "int_cases";
-
-val int_def = thm "int_def";
-val Zero_int_def = thm "Zero_int_def";
-val One_int_def = thm "One_int_def";
-val diff_int_def = thm "diff_int_def";
-
-val inj_int = thm "inj_int";
-val zminus_zminus = thm "zminus_zminus";
-val zminus_0 = thm "zminus_0";
-val zminus_zadd_distrib = thm "zminus_zadd_distrib";
-val zadd_commute = thm "zadd_commute";
-val zadd_assoc = thm "zadd_assoc";
-val zadd_left_commute = thm "zadd_left_commute";
-val zadd_ac = thms "zadd_ac";
-val zmult_ac = thms "zmult_ac";
-val zadd_int = thm "zadd_int";
-val zadd_int_left = thm "zadd_int_left";
-val int_Suc = thm "int_Suc";
-val zadd_0 = thm "zadd_0";
-val zadd_0_right = thm "zadd_0_right";
-val zmult_zminus = thm "zmult_zminus";
-val zmult_commute = thm "zmult_commute";
-val zmult_assoc = thm "zmult_assoc";
-val zadd_zmult_distrib = thm "zadd_zmult_distrib";
-val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
-val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
-val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
-val int_distrib = thms "int_distrib";
-val zmult_int = thm "zmult_int";
-val zmult_1 = thm "zmult_1";
-val zmult_1_right = thm "zmult_1_right";
-val int_int_eq = thm "int_int_eq";
-val int_eq_0_conv = thm "int_eq_0_conv";
-val zless_int = thm "zless_int";
-val int_less_0_conv = thm "int_less_0_conv";
-val zero_less_int_conv = thm "zero_less_int_conv";
-val zle_int = thm "zle_int";
-val zero_zle_int = thm "zero_zle_int";
-val int_le_0_conv = thm "int_le_0_conv";
-val zle_refl = thm "zle_refl";
-val zle_linear = thm "zle_linear";
-val zle_trans = thm "zle_trans";
-val zle_anti_sym = thm "zle_anti_sym";
-
-val Ints_def = thm "Ints_def";
-val Nats_def = thm "Nats_def";
-
-val of_nat_0 = thm "of_nat_0";
-val of_nat_Suc = thm "of_nat_Suc";
-val of_nat_1 = thm "of_nat_1";
-val of_nat_add = thm "of_nat_add";
-val of_nat_mult = thm "of_nat_mult";
-val zero_le_imp_of_nat = thm "zero_le_imp_of_nat";
-val less_imp_of_nat_less = thm "less_imp_of_nat_less";
-val of_nat_less_imp_less = thm "of_nat_less_imp_less";
-val of_nat_less_iff = thm "of_nat_less_iff";
-val of_nat_le_iff = thm "of_nat_le_iff";
-val of_nat_eq_iff = thm "of_nat_eq_iff";
-val Nats_0 = thm "Nats_0";
-val Nats_1 = thm "Nats_1";
-val Nats_add = thm "Nats_add";
-val Nats_mult = thm "Nats_mult";
-val int_eq_of_nat = thm"int_eq_of_nat";
-val of_int = thm "of_int";
-val of_int_0 = thm "of_int_0";
-val of_int_1 = thm "of_int_1";
-val of_int_add = thm "of_int_add";
-val of_int_minus = thm "of_int_minus";
-val of_int_diff = thm "of_int_diff";
-val of_int_mult = thm "of_int_mult";
-val of_int_le_iff = thm "of_int_le_iff";
-val of_int_less_iff = thm "of_int_less_iff";
-val of_int_eq_iff = thm "of_int_eq_iff";
-val Ints_0 = thm "Ints_0";
-val Ints_1 = thm "Ints_1";
-val Ints_add = thm "Ints_add";
-val Ints_minus = thm "Ints_minus";
-val Ints_diff = thm "Ints_diff";
-val Ints_mult = thm "Ints_mult";
-val of_int_of_nat_eq = thm"of_int_of_nat_eq";
-val Ints_cases = thm "Ints_cases";
-val Ints_induct = thm "Ints_induct";
-*}
-
-end
+end
\ No newline at end of file
diff -r eaf5e7ef35d9 -r caffcb450ef4 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Thu Apr 26 13:33:04 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Thu Apr 26 13:33:05 2007 +0200
@@ -7,10 +7,12 @@
 header {* Arithmetic on Binary Integers *}
 
 theory Numeral
-imports IntDef Datatype
+imports IntDef
 uses "../Tools/numeral_syntax.ML"
 begin
 
+subsection {* Binary representation *}
+
 text {*
   This formalization defines binary arithmetic in terms of the integers
   rather than using a datatype. This avoids multiple representations (leading
@@ -23,13 +25,13 @@
   @{text "-5 = (-3)*2 + 1"}.
 *}
 
+datatype bit = B0 | B1
+
 text{*
-  This type avoids the use of type @{typ bool}, which would make
+  Type @{typ bit} avoids the use of type @{typ bool}, which would make
   all of the rewrite rules higher-order.
 *}
 
-datatype bit = B0 | B1
-
 definition
   Pls :: int where
   [code nofunc]:"Pls = 0"
@@ -74,9 +76,12 @@
   pred :: "int \<Rightarrow> int" where
   [code nofunc]: "pred k = k - 1"
 
-declare
- max_def[of "number_of u" "number_of v", standard, simp]
- min_def[of "number_of u" "number_of v", standard, simp]
+lemmas
+  max_number_of [simp] = max_def
+    [of "number_of u" "number_of v", standard, simp]
+and
+  min_number_of [simp] = min_def 
+    [of "number_of u" "number_of v", standard, simp]
   -- {* unfolding @{text minx} and @{text max} on numerals *}
 
 lemmas numeral_simps = 
@@ -84,11 +89,11 @@
 
 text {* Removal of leading zeroes *}
 
-lemma Pls_0_eq [simp, code func]:
+lemma Pls_0_eq [simp, normal post]:
   "Pls BIT B0 = Pls"
   unfolding numeral_simps by simp
 
-lemma Min_1_eq [simp, code func]:
+lemma Min_1_eq [simp, normal post]:
   "Min BIT B1 = Min"
   unfolding numeral_simps by simp
 
@@ -200,6 +205,18 @@
 axclass number_ring \<subseteq> number, comm_ring_1
   number_of_eq: "number_of k = of_int k"
 
+text {* self-embedding of the intergers *}
+
+instance int :: number_ring
+  int_number_of_def: "number_of w \<equiv> of_int w"
+  by intro_classes (simp only: int_number_of_def)
+
+lemmas [code nofunc] = int_number_of_def
+
+lemma number_of_is_id:
+  "number_of (k::int) = k"
+  unfolding int_number_of_def by simp
+
 lemma number_of_succ:
   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   unfolding number_of_eq numeral_simps by simp
@@ -483,7 +500,7 @@
 
 subsection {* Simplification of arithmetic operations on integer constants. *}
 
-lemmas arith_extra_simps [standard] =
+lemmas arith_extra_simps [standard, simp] =
   number_of_add [symmetric]
   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
   number_of_mult [symmetric]
@@ -507,7 +524,7 @@
 
 text {* Simplification of relational operations *}
 
-lemmas rel_simps = 
+lemmas rel_simps [simp] = 
   eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
   iszero_number_of_0 iszero_number_of_1
   less_number_of_eq_neg
@@ -515,9 +532,6 @@
   neg_number_of_Min neg_number_of_BIT
   le_number_of_eq
 
-declare arith_extra_simps [simp]
-declare rel_simps [simp]
-
 
 subsection {* Simplification of arithmetic when nested to the right. *}
 
@@ -544,6 +558,109 @@
 done
 
 
+subsection {* Configuration of the code generator *}
+
+instance int :: eq ..
+
+code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
+
+definition
+  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
+  "int_aux i n = (i + int n)"
+
+lemma [code]:
+  "int_aux i 0 = i"
+  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
+  by (simp add: int_aux_def)+
+
+lemma [code]:
+  "int n = int_aux 0 n"
+  by (simp add: int_aux_def)
+
+definition
+  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
+  "nat_aux n i = (n + nat i)"
+
+lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
+  -- {* tail recursive *}
+  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 zero_is_num_zero [code func, code inline, symmetric, normal post]:
+  "(0\<Colon>int) = number_of Numeral.Pls" 
+  by simp
+
+lemma one_is_num_one [code func, code inline, symmetric, normal post]:
+  "(1\<Colon>int) = number_of (Numeral.Pls BIT bit.B1)" 
+  by simp 
+
+code_modulename SML
+  IntDef Integer
+
+code_modulename OCaml
+  IntDef Integer
+
+code_modulename Haskell
+  IntDef Integer
+
+code_modulename SML
+  Numeral Integer
+
+code_modulename OCaml
+  Numeral Integer
+
+code_modulename Haskell
+  Numeral Integer
+
+(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
+
+types_code
+  "int" ("int")
+attach (term_of) {*
+val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
+*}
+attach (test) {*
+fun gen_int i = one_of [~1, 1] * random_range 0 i;
+*}
+
+setup {*
+let
+
+fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T])) $ t) =
+      if T = HOLogic.intT then
+        (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
+          (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
+      else if T = HOLogic.natT then
+        SOME (Codegen.invoke_codegen thy defs dep module b (gr,
+          Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
+            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ t)))
+      else NONE
+  | number_of_codegen _ _ _ _ _ _ _ = NONE;
+
+in
+
+Codegen.add_codegen "number_of_codegen" number_of_codegen
+
+end
+*}
+
+consts_code
+  "HOL.zero" :: "int"                ("0")
+  "HOL.one" :: "int"                 ("1")
+  "HOL.uminus" :: "int => int"       ("~")
+  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
+  "HOL.times" :: "int => int => int" ("(_ */ _)")
+  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
+  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
+  "neg"                              ("(_ < 0)")
+
+quickcheck_params [default_type = int]
+
+(* setup continues in theory Presburger *)
+
 hide (open) const Pls Min B0 B1 succ pred
 
 end
diff -r eaf5e7ef35d9 -r caffcb450ef4 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Thu Apr 26 13:33:04 2007 +0200
+++ b/src/HOL/Integ/Presburger.thy	Thu Apr 26 13:33:05 2007 +0200
@@ -9,7 +9,7 @@
 header {* Presburger Arithmetic: Cooper's Algorithm *}
 
 theory Presburger
-imports NatSimprocs
+imports NatSimprocs "../SetInterval"
 uses
   ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
   ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
@@ -1059,17 +1059,14 @@
 
 setup "Presburger.setup"
 
-text {* Code generator setup *}
+
+subsection {* Code generator setup *}
 
 text {*
-  Presburger arithmetic is necessary (at least convenient) to prove some
-  of the following code lemmas on integer numerals.
+  Presburger arithmetic is convenient to prove some
+  of the following code lemmas on integer numerals:
 *}
 
-lemma eq_number_of [code func]:
-  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
-  unfolding number_of_is_id ..
-
 lemma eq_Pls_Pls:
   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
 
@@ -1131,14 +1128,10 @@
   apply auto
 done
 
-lemmas eq_numeral_code [code func] =
-  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
-  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
-  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+lemma eq_number_of:
+  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
+  unfolding number_of_is_id ..
 
-lemma less_eq_number_of [code func]:
-  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
-  unfolding number_of_is_id ..
 
 lemma less_eq_Pls_Pls:
   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
@@ -1190,13 +1183,10 @@
   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   unfolding Bit_def by (auto split: bit.split)
 
-lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
-  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
-  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+lemma less_eq_number_of:
+  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
+  unfolding number_of_is_id ..
 
-lemma less_eq_number_of [code func]:
-  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
-  unfolding number_of_is_id ..
 
 lemma less_Pls_Pls:
   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
@@ -1248,8 +1238,42 @@
   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   unfolding Bit_def bit.cases by auto
 
+lemma less_number_of:
+  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
+  unfolding number_of_is_id ..
+
+
+lemmas pred_succ_numeral_code [code func] =
+  arith_simps(5-12)
+
+lemmas plus_numeral_code [code func] =
+  arith_simps(13-17)
+  arith_simps(26-27)
+  arith_extra_simps(1) [where 'a = int]
+
+lemmas minus_numeral_code [code func] =
+  arith_simps(18-21)
+  arith_extra_simps(2) [where 'a = int]
+  arith_extra_simps(5) [where 'a = int]
+
+lemmas times_numeral_code [code func] =
+  arith_simps(22-25)
+  arith_extra_simps(4) [where 'a = int]
+
+lemmas eq_numeral_code [code func] =
+  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
+  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
+  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+  eq_number_of
+
+lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
+  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+  less_eq_number_of
+
 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
+  less_number_of
 
 end
diff -r eaf5e7ef35d9 -r caffcb450ef4 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Apr 26 13:33:04 2007 +0200
+++ b/src/HOL/Presburger.thy	Thu Apr 26 13:33:05 2007 +0200
@@ -9,7 +9,7 @@
 header {* Presburger Arithmetic: Cooper's Algorithm *}
 
 theory Presburger
-imports NatSimprocs
+imports NatSimprocs "../SetInterval"
 uses
   ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
   ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
@@ -1059,17 +1059,14 @@
 
 setup "Presburger.setup"
 
-text {* Code generator setup *}
+
+subsection {* Code generator setup *}
 
 text {*
-  Presburger arithmetic is necessary (at least convenient) to prove some
-  of the following code lemmas on integer numerals.
+  Presburger arithmetic is convenient to prove some
+  of the following code lemmas on integer numerals:
 *}
 
-lemma eq_number_of [code func]:
-  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
-  unfolding number_of_is_id ..
-
 lemma eq_Pls_Pls:
   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
 
@@ -1131,14 +1128,10 @@
   apply auto
 done
 
-lemmas eq_numeral_code [code func] =
-  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
-  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
-  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+lemma eq_number_of:
+  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
+  unfolding number_of_is_id ..
 
-lemma less_eq_number_of [code func]:
-  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
-  unfolding number_of_is_id ..
 
 lemma less_eq_Pls_Pls:
   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
@@ -1190,13 +1183,10 @@
   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   unfolding Bit_def by (auto split: bit.split)
 
-lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
-  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
-  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+lemma less_eq_number_of:
+  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
+  unfolding number_of_is_id ..
 
-lemma less_eq_number_of [code func]:
-  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
-  unfolding number_of_is_id ..
 
 lemma less_Pls_Pls:
   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
@@ -1248,8 +1238,42 @@
   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   unfolding Bit_def bit.cases by auto
 
+lemma less_number_of:
+  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
+  unfolding number_of_is_id ..
+
+
+lemmas pred_succ_numeral_code [code func] =
+  arith_simps(5-12)
+
+lemmas plus_numeral_code [code func] =
+  arith_simps(13-17)
+  arith_simps(26-27)
+  arith_extra_simps(1) [where 'a = int]
+
+lemmas minus_numeral_code [code func] =
+  arith_simps(18-21)
+  arith_extra_simps(2) [where 'a = int]
+  arith_extra_simps(5) [where 'a = int]
+
+lemmas times_numeral_code [code func] =
+  arith_simps(22-25)
+  arith_extra_simps(4) [where 'a = int]
+
+lemmas eq_numeral_code [code func] =
+  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
+  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
+  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
+  eq_number_of
+
+lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
+  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
+  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
+  less_eq_number_of
+
 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
+  less_number_of
 
 end