author haftmann Thu, 26 Apr 2007 13:33:05 +0200 changeset 22801 caffcb450ef4 parent 22800 eaf5e7ef35d9 child 22802 92026479179e
cleaned up code generator setup for int
 src/HOL/Integ/IntArith.thy file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions src/HOL/Integ/Numeral.thy file | annotate | diff | comparison | revisions src/HOL/Integ/Presburger.thy file | annotate | diff | comparison | revisions src/HOL/Presburger.thy file | annotate | diff | comparison | revisions
```--- 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])
@@ -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 (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")
-code_const "Numeral.bit.B0" and "Numeral.bit.B1"
-  (SML "false" and "true")
-  (OCaml "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")
-     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 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_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```
```--- 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)})"

-
+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)})" ..

-   "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"

-lemma int_Suc: "int (Suc m) = 1 + (int m)"
-
(*also for the instance declaration int :: comm_monoid_add*)
lemma zadd_0: "(0::int) + z = z"
@@ -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"

+lemma int_Suc: "int (Suc m) = 1 + (int m)"
+

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)"

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 @@

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 (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"
-
-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
-lemma [code]: "nat i = nat_aux 0 i"
-
-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")
-
-code_instance int :: eq
-
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "!((_ : IntInf.int) = _)")
-  (OCaml "Big'_int.eq'_big'_int")
-
-code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.<= (_, _)")
-  (OCaml "Big'_int.le'_big'_int")
-
-code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.< (_, _)")
-  (OCaml "Big'_int.lt'_big'_int")
-
-code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.+ (_, _)")
-
-code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.- (_, _)")
-  (OCaml "Big'_int.sub'_big'_int")
-
-code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.* (_, _)")
-  (OCaml "Big'_int.mult'_big'_int")
-
-code_const "uminus \<Colon> int \<Rightarrow> int"
-  (SML "IntInf.~")
-  (OCaml "Big'_int.minus'_big'_int")
-
-code_reserved SML IntInf
-code_reserved OCaml Big_int
-
-code_modulename SML
-  IntDef Integer
-
-  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 {*
+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_mult = @{thm of_nat_mult};
+val of_int_0 = @{thm of_int_0};
+val of_int_1 = @{thm of_int_1};
+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 zless_int = @{thm zless_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 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 zmult_ac = thms "zmult_ac";
-val int_Suc = thm "int_Suc";
-val zmult_zminus = thm "zmult_zminus";
-val zmult_commute = thm "zmult_commute";
-val zmult_assoc = thm "zmult_assoc";
-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_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_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_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_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```
```--- 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_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 *}
+
+lemma [code]:
+  "int n = int_aux 0 n"
+
+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
+
+lemma [code]: "nat i = nat_aux 0 i"
+
+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
+
+  IntDef Integer
+
+code_modulename SML
+  Numeral Integer
+
+code_modulename OCaml
+  Numeral Integer
+
+  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
+
+
+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```
```--- 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```
```--- 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```