# HG changeset patch
# User huffman
# Date 1181698271 -7200
# Node ID f31794033ae10f629e3bcb74d8e4a2f1a4e1aed4
# Parent  1f3b832c90c123eede3d05df3f8231dc215b8338
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int

diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/IntArith.thy
--- a/src/HOL/IntArith.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntArith.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -196,25 +196,6 @@
       z is an integer literal.*}
 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
 
-lemmas int_of_nat_eq_iff_number_of [simp] =
-  int_of_nat_eq_iff [of _ "number_of v", standard]
-
-lemma split_nat':
-  "P(nat(i::int)) = ((\<forall>n. i = int_of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
-  (is "?P = (?L & ?R)")
-proof (cases "i < 0")
-  case True thus ?thesis by simp
-next
-  case False
-  have "?P = ?L"
-  proof
-    assume ?P thus ?L using False by clarsimp
-  next
-    assume ?L thus ?P using False by simp
-  qed
-  with False show ?thesis by simp
-qed
-
 lemma split_nat [arith_split]:
   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L & ?R)")
@@ -232,10 +213,6 @@
 qed
 
 
-(*Analogous to zadd_int*)
-lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
-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 (cases "0 \<le> z'")
 apply (rule inj_int [THEN injD])
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -219,9 +219,12 @@
 qed
 
 abbreviation
-  int_of_nat :: "nat \<Rightarrow> int"
+  int :: "nat \<Rightarrow> int"
 where
-  "int_of_nat \<equiv> of_nat"
+  "int \<equiv> of_nat"
+
+lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
+by (induct m, simp_all add: Zero_int_def One_int_def add)
 
 
 subsection{*The @{text "\<le>"} Ordering*}
@@ -294,18 +297,15 @@
 apply (simp_all add: add_strict_mono)
 done
 
-lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
-by (induct m, simp_all add: Zero_int_def One_int_def add)
-
 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
 apply (cases k)
-apply (auto simp add: le add int_of_nat_def Zero_int_def)
+apply (auto simp add: le add int_def Zero_int_def)
 apply (rule_tac x="x-y" in exI, simp)
 done
 
 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
 apply (cases k)
-apply (simp add: less int_of_nat_def Zero_int_def)
+apply (simp add: less int_def Zero_int_def)
 apply (rule_tac x="x-y" in exI, simp)
 done
 
@@ -352,16 +352,16 @@
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
 
-lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
-by (simp add: nat int_of_nat_def)
+lemma nat_int [simp]: "nat (int n) = n"
+by (simp add: nat int_def)
 
 lemma nat_zero [simp]: "nat 0 = 0"
 by (simp add: Zero_int_def nat)
 
-lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \<le> z then z else 0)"
-by (cases z, simp add: nat le int_of_nat_def Zero_int_def)
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
+by (cases z, simp add: nat le int_def Zero_int_def)
 
-corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
+corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
 by simp
 
 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
@@ -379,27 +379,27 @@
 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
 
-lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
+lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
 apply (cases w, cases z) 
 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
 done
 
-lemma nonneg_eq_int_of_nat: "[| 0 \<le> z;  !!m. z = int_of_nat m ==> P |] ==> P"
-by (blast dest: nat_0_le' sym)
+lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
+by (blast dest: nat_0_le sym)
 
-lemma nat_eq_iff': "(nat w = m) = (if 0 \<le> w then w = int_of_nat m else m=0)"
-by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith)
+lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
+by (cases w, simp add: nat le int_def Zero_int_def, arith)
 
-corollary nat_eq_iff2': "(m = nat w) = (if 0 \<le> w then w = int_of_nat m else m=0)"
-by (simp only: eq_commute [of m] nat_eq_iff')
+corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
+by (simp only: eq_commute [of m] nat_eq_iff)
 
-lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
+lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
 apply (cases w)
-apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith)
+apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
 done
 
-lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \<le> z)"
-by (auto simp add: nat_eq_iff2')
+lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
+by (auto simp add: nat_eq_iff2)
 
 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
 by (insert zless_nat_conj [of 0], auto)
@@ -413,42 +413,41 @@
 by (cases z, cases z', 
     simp add: nat add minus diff_minus le Zero_int_def)
 
-lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
-by (simp add: int_of_nat_def minus nat Zero_int_def) 
+lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
+by (simp add: int_def minus nat Zero_int_def) 
 
-lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
-by (cases z, simp add: nat less int_of_nat_def, arith)
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+by (cases z, simp add: nat less int_def, arith)
 
 
 subsection{*Lemmas about the Function @{term int} and Orderings*}
 
-lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0"
+lemma negative_zless_0: "- (int (Suc n)) < 0"
 by (simp add: order_less_le del: of_nat_Suc)
 
-lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m"
-by (rule negative_zless_0' [THEN order_less_le_trans], simp)
+lemma negative_zless [iff]: "- (int (Suc n)) < int m"
+by (rule negative_zless_0 [THEN order_less_le_trans], simp)
 
-lemma negative_zle_0': "- int_of_nat n \<le> 0"
+lemma negative_zle_0: "- int n \<le> 0"
 by (simp add: minus_le_iff)
 
-lemma negative_zle' [iff]: "- int_of_nat n \<le> int_of_nat m"
-by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff])
+lemma negative_zle [iff]: "- int n \<le> int m"
+by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
 
-lemma not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (Suc n)))"
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
 by (subst le_minus_iff, simp del: of_nat_Suc)
 
-lemma int_zle_neg': "(int_of_nat n \<le> - int_of_nat m) = (n = 0 & m = 0)"
-by (simp add: int_of_nat_def le minus Zero_int_def)
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
+by (simp add: int_def le minus Zero_int_def)
 
-lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)"
+lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
 by (simp add: linorder_not_less)
 
-lemma negative_eq_positive' [simp]:
-  "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
-by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
+lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
+by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
 
-lemma zle_iff_zadd': "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
-proof (cases w, cases z, simp add: le add int_of_nat_def)
+lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
+proof (cases w, cases z, simp add: le add int_def)
   fix a b c d
   assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
   show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
@@ -487,10 +486,10 @@
 where
   "iszero z \<longleftrightarrow> z = 0"
 
-lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
+lemma not_neg_int [simp]: "~ neg (int n)"
 by (simp add: neg_def)
 
-lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
+lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
 by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
 
 lemmas neg_eq_less_0 = neg_def
@@ -516,7 +515,7 @@
 lemma neg_nat: "neg z ==> nat z = 0"
 by (simp add: neg_def order_less_imp_le) 
 
-lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z"
+lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
 by (simp add: linorder_not_less neg_def)
 
 
@@ -645,7 +644,7 @@
   fix z
   show "of_int z = id z"
     by (cases z)
-      (simp add: of_int add minus int_of_nat_def diff_minus)
+      (simp add: of_int add minus int_def diff_minus)
 qed
 
 
@@ -764,245 +763,80 @@
 text{*Now we replace the case analysis rule by a more conventional one:
 whether an integer is negative or not.*}
 
-lemma zless_iff_Suc_zadd':
-    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
+lemma zless_iff_Suc_zadd:
+    "(w < z) = (\<exists>n. z = w + int (Suc n))"
 apply (cases z, cases w)
-apply (auto simp add: le add int_of_nat_def linorder_not_le [symmetric]) 
+apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
 apply (rename_tac a b c d) 
 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
 apply arith
 done
 
-lemma negD': "x<0 ==> \<exists>n. x = - (int_of_nat (Suc n))"
+lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
 apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
+apply (auto simp add: le minus Zero_int_def int_def order_less_le)
 apply (rule_tac x="y - Suc x" in exI, arith)
 done
 
-theorem int_cases' [cases type: int, case_names nonneg neg]:
-     "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
-apply (cases "z < 0", blast dest!: negD')
+theorem int_cases [cases type: int, case_names nonneg neg]:
+     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
+apply (cases "z < 0", blast dest!: negD)
 apply (simp add: linorder_not_less del: of_nat_Suc)
-apply (blast dest: nat_0_le' [THEN sym])
+apply (blast dest: nat_0_le [THEN sym])
 done
 
-theorem int_induct' [induct type: int, case_names nonneg neg]:
-     "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
-  by (cases z rule: int_cases') auto
+theorem int_induct'[induct type: int, case_names nonneg neg]:
+     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
+  by (cases z rule: int_cases) auto
 
 text{*Contributed by Brian Huffman*}
-theorem int_diff_cases' [case_names diff]:
-assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P"
+theorem int_diff_cases [case_names diff]:
+assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
 apply (cases z rule: eq_Abs_Integ)
 apply (rule_tac m=x and n=y in prem)
-apply (simp add: int_of_nat_def diff_def minus add)
+apply (simp add: int_def diff_def minus add)
 done
 
 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
 by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
 
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
 
-
-subsection{*@{term int}: Embedding the Naturals into the Integers*}
-
-definition
-  int :: "nat \<Rightarrow> int"
-where
-  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
-
-text{*Agreement with the specific embedding for the integers*}
-lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
-by (simp add: expand_fun_eq int_of_nat_def int_def)
-
-lemma inj_int: "inj int"
-by (simp add: inj_on_def int_def)
-
-lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
-unfolding int_eq_of_nat by (rule of_nat_eq_iff)
-
-lemma zadd_int: "(int m) + (int n) = int (m + n)"
-unfolding int_eq_of_nat by (rule of_nat_add [symmetric])
+subsection {* Legacy theorems *}
 
 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
-unfolding int_eq_of_nat by simp
-
-lemma int_mult: "int (m * n) = (int m) * (int n)"
-unfolding int_eq_of_nat by (rule of_nat_mult)
-
-text{*Compatibility binding*}
-lemmas zmult_int = int_mult [symmetric]
-
-lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
-unfolding int_eq_of_nat by (rule of_nat_eq_0_iff)
-
-lemma zless_int [simp]: "(int m < int n) = (m<n)"
-unfolding int_eq_of_nat by (rule of_nat_less_iff)
-
-lemma int_less_0_conv [simp]: "~ (int k < 0)"
-unfolding int_eq_of_nat by (rule of_nat_less_0_iff)
-
-lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
-unfolding int_eq_of_nat by (rule of_nat_0_less_iff)
-
-lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
-unfolding int_eq_of_nat by (rule of_nat_le_iff)
-
-lemma zero_zle_int [simp]: "(0 \<le> int n)"
-unfolding int_eq_of_nat by (rule of_nat_0_le_iff)
-
-lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
-unfolding int_eq_of_nat by (rule of_nat_le_0_iff)
-
-lemma int_0 [simp]: "int 0 = (0::int)"
-unfolding int_eq_of_nat by (rule of_nat_0)
-
-lemma int_1 [simp]: "int 1 = 1"
-unfolding int_eq_of_nat by (rule of_nat_1)
-
-lemma int_Suc0_eq_1: "int (Suc 0) = 1"
-unfolding int_eq_of_nat by simp
+by simp
 
 lemma int_Suc: "int (Suc m) = 1 + (int m)"
-unfolding int_eq_of_nat by simp
-
-lemma nat_int [simp]: "nat(int n) = n"
-unfolding int_eq_of_nat by (rule nat_int_of_nat)
-
-lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
-unfolding int_eq_of_nat by (rule int_of_nat_nat_eq)
-
-corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
-unfolding int_eq_of_nat by (rule nat_0_le')
-
-lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
-unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat)
-
-lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
-unfolding int_eq_of_nat by (rule nat_eq_iff')
-
-corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
-unfolding int_eq_of_nat by (rule nat_eq_iff2')
-
-lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
-unfolding int_eq_of_nat by (rule nat_less_iff')
-
-lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
-unfolding int_eq_of_nat by (rule int_of_nat_eq_iff)
-
-lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
-unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat)
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless')
+by simp
 
-lemma negative_zless_0: "- (int (Suc n)) < 0"
-unfolding int_eq_of_nat by (rule negative_zless_0')
-
-lemma negative_zless [iff]: "- (int (Suc n)) < int m"
-unfolding int_eq_of_nat by (rule negative_zless')
-
-lemma negative_zle_0: "- int n \<le> 0"
-unfolding int_eq_of_nat by (rule negative_zle_0')
-
-lemma negative_zle [iff]: "- int n \<le> int m"
-unfolding int_eq_of_nat by (rule negative_zle')
-
-lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
-unfolding int_eq_of_nat by (rule not_zle_0_negative')
-
-lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
-unfolding int_eq_of_nat by (rule int_zle_neg')
-
-lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
-unfolding int_eq_of_nat by (rule not_int_zless_negative')
-
-lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
-unfolding int_eq_of_nat by (rule negative_eq_positive')
-
-lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
-unfolding int_eq_of_nat by (rule zle_iff_zadd')
-
-lemma abs_int_eq [simp]: "abs (int m) = int m"
-unfolding int_eq_of_nat by (rule abs_of_nat)
-
-lemma not_neg_int [simp]: "~ neg(int n)"
-unfolding int_eq_of_nat by (rule not_neg_int_of_nat)
-
-lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
-unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat)
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
+by simp
 
-lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
-unfolding int_eq_of_nat by (rule not_neg_nat')
-
-lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
-unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
-
-lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
-unfolding int_eq_of_nat by (rule of_nat_setsum)
-
-lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
-unfolding int_eq_of_nat by (rule of_nat_setprod)
-
-text{*Now we replace the case analysis rule by a more conventional one:
-whether an integer is negative or not.*}
-
-lemma zless_iff_Suc_zadd:
-    "(w < z) = (\<exists>n. z = w + int(Suc n))"
-unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
-
-lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
-unfolding int_eq_of_nat by (rule negD')
-
-theorem int_cases [cases type: int, case_names nonneg neg]:
-     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
-unfolding int_eq_of_nat
-apply (cases "z < 0", blast dest!: negD')
-apply (simp add: linorder_not_less)
-apply (blast dest: nat_0_le' [THEN sym])
-done
-
-theorem int_induct [induct type: int, case_names nonneg neg]:
-     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
-  by (cases z) auto
+lemmas inj_int = inj_of_nat [where 'a=int]
+lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
+lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
+lemmas int_mult = of_nat_mult [where 'a=int]
+lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
+lemmas zless_int = of_nat_less_iff [where 'a=int]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
+lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
+lemmas zle_int = of_nat_le_iff [where 'a=int]
+lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
+lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
+lemmas int_1 = of_nat_1 [where 'a=int]
+lemmas abs_int_eq = abs_of_nat [where 'a=int]
+lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
+lemmas int_setsum = of_nat_setsum [where 'a=int]
+lemmas int_setprod = of_nat_setprod [where 'a=int]
+lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
+lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
+lemmas int_eq_of_nat = TrueI
 
-text{*Contributed by Brian Huffman*}
-theorem int_diff_cases [case_names diff]:
-assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
- apply (rule_tac z=z in int_cases)
-  apply (rule_tac m=n and n=0 in prem, simp)
- apply (rule_tac m=0 and n="Suc n" in prem, simp)
-done
-
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
-
-lemmas [simp] = int_Suc
-
-
-subsection {* Legacy ML bindings *}
-
-ML {*
-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};
-*}
+abbreviation
+  int_of_nat :: "nat \<Rightarrow> int"
+where
+  "int_of_nat \<equiv> of_nat"
 
 end
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntDiv.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -11,8 +11,6 @@
 imports IntArith Divides FunDef
 begin
 
-declare zless_nat_conj [simp]
-
 constdefs
   quorem :: "(int*int) * (int*int) => bool"
     --{*definition of quotient and remainder*}
@@ -266,7 +264,7 @@
   val trans = trans;
   val prove_eq_sums =
     let
-      val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
+      val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
 end)
 
@@ -1238,9 +1236,9 @@
   apply simp
   done
 
-theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
+theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   unfolding dvd_def
-  apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
+  apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
   apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
   apply (simp add: ex_nat cong add: conj_cong)
   apply (rule iffI)
@@ -1257,9 +1255,6 @@
   apply (simp add: mult_ac)
   done
 
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-  unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
-
 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
 proof
   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
@@ -1280,40 +1275,31 @@
   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
 qed
 
-lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
+lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   apply (auto simp add: dvd_def nat_abs_mult_distrib)
-  apply (auto simp add: nat_eq_iff' abs_if split add: split_if_asm)
-   apply (rule_tac x = "-(int_of_nat k)" in exI)
+  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
+   apply (rule_tac x = "-(int k)" in exI)
   apply auto
   done
 
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
-  unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
-
-lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
+lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   apply (auto simp add: dvd_def abs_if)
     apply (rule_tac [3] x = "nat k" in exI)
-    apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
+    apply (rule_tac [2] x = "-(int k)" in exI)
     apply (rule_tac x = "nat (-k)" in exI)
-    apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
-    apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
+    apply (cut_tac [3] m = m in int_less_0_conv)
+    apply (cut_tac m = m in int_less_0_conv)
     apply (auto simp add: zero_le_mult_iff mult_less_0_iff
-      nat_mult_distrib [symmetric] nat_eq_iff2')
-  done
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
-  unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
-
-lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
-  apply (auto simp add: dvd_def)
-  apply (rule_tac x = "nat k" in exI)
-  apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
-  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
-    nat_mult_distrib [symmetric] nat_eq_iff2')
+      nat_mult_distrib [symmetric] nat_eq_iff2)
   done
 
 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
-  unfolding int_eq_of_nat by (rule nat_dvd_iff')
+  apply (auto simp add: dvd_def)
+  apply (rule_tac x = "nat k" in exI)
+  apply (cut_tac m = m in int_less_0_conv)
+  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
+    nat_mult_distrib [symmetric] nat_eq_iff2)
+  done
 
 lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   apply (auto simp add: dvd_def)
@@ -1327,9 +1313,9 @@
   done
 
 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
-  apply (rule_tac z=n in int_cases')
-  apply (auto simp add: dvd_int_of_nat_iff)
-  apply (rule_tac z=z in int_cases')
+  apply (rule_tac z=n in int_cases)
+  apply (auto simp add: dvd_int_iff)
+  apply (rule_tac z=z in int_cases)
   apply (auto simp add: dvd_imp_le)
   done
 
@@ -1377,33 +1363,25 @@
 done
 
 lemma int_power: "int (m^n) = (int m) ^ n"
-  by (induct n, simp_all add: int_mult)
+  by (rule of_nat_power)
 
 text{*Compatibility binding*}
 lemmas zpower_int = int_power [symmetric]
 
-lemma int_of_nat_div:
-  "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
+lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
-apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and r="int_of_nat j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def)
-done
-
-lemma zdiv_int: "int (a div b) = (int a) div (int b)"
-  unfolding int_eq_of_nat by (rule int_of_nat_div)
-
-lemma int_of_nat_mod:
-  "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
-apply (subst split_mod, auto)
-apply (subst split_zmod, auto)
-apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and q="int_of_nat i" and q'=ia 
-       in unique_remainder)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
 apply (auto simp add: IntDiv.quorem_def)
 done
 
 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
-  unfolding int_eq_of_nat by (rule int_of_nat_mod)
+apply (subst split_mod, auto)
+apply (subst split_zmod, auto)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
+       in unique_remainder)
+apply (auto simp add: IntDiv.quorem_def)
+done
 
 text{*Suggested by Matthias Daum*}
 lemma int_power_div_base:
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -31,6 +31,19 @@
   nat_of_int :: "int \<Rightarrow> nat" where
   "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
 
+definition
+  int' :: "nat \<Rightarrow> int" where
+  "int' n = of_nat n"
+
+lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
+unfolding int'_def by simp
+
+lemma int'_add: "int' (m + n) = int' m + int' n"
+unfolding int'_def by (rule of_nat_add)
+
+lemma int'_mult: "int' (m * n) = int' m * int' n"
+unfolding int'_def by (rule of_nat_mult)
+
 lemma nat_of_int_of_number_of:
   fixes k
   assumes "k \<ge> 0"
@@ -44,8 +57,11 @@
   using prems unfolding Pls_def by simp
 
 lemma nat_of_int_int:
-  "nat_of_int (int n) = n"
-  using zero_zle_int nat_of_int_def by simp
+  "nat_of_int (int' n) = n"
+  using nat_of_int_def int'_def by simp
+
+lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
+by (erule subst, simp only: nat_of_int_int)
 
 text {*
   Case analysis on natural numbers is rephrased using a conditional
@@ -66,10 +82,10 @@
 qed
 
 lemma [code inline]:
-  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
+  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
 proof (rule ext)+
   fix f g n
-  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
+  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
   by (cases n) (simp_all add: nat_of_int_int)
 qed
 
@@ -82,43 +98,33 @@
   by (simp add: nat_of_int_def)
 lemma [code func, code inline]:  "1 = nat_of_int 1"
   by (simp add: nat_of_int_def)
-lemma [code func]: "Suc n = nat_of_int (int n + 1)"
-  by (simp add: nat_of_int_def)
-lemma [code]: "m + n = nat (int m + int n)"
-  by arith
-lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
-  by (simp add: nat_of_int_def)
-lemma [code, code inline]: "m - n = nat (int m - int n)"
-  by arith
-lemma [code]: "m * n = nat (int m * int n)"
-  unfolding zmult_int by simp
-lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
-proof -
-  have "int (m * n) = int m * int n"
-    by (induct m) (simp_all add: zadd_zmult_distrib)
-  then have "m * n = nat (int m * int n)" by auto
-  also have "\<dots> = nat_of_int (int m * int n)"
-  proof -
-    have "int m \<ge> 0" and "int n \<ge> 0" by auto
-    have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
-    with nat_of_int_def show ?thesis by auto
-  qed
-  finally show ?thesis .
-qed  
-lemma [code]: "m div n = nat (int m div int n)"
-  unfolding zdiv_int [symmetric] by simp
+lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
+  by (simp add: eq_nat_of_int)
+lemma [code]: "m + n = nat (int' m + int' n)"
+  by (simp add: int'_def nat_eq_iff2)
+lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
+  by (simp add: eq_nat_of_int int'_add)
+lemma [code, code inline]: "m - n = nat (int' m - int' n)"
+  by (simp add: int'_def nat_eq_iff2)
+lemma [code]: "m * n = nat (int' m * int' n)"
+  unfolding int'_def
+  by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
+lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
+  by (simp add: eq_nat_of_int int'_mult)
+lemma [code]: "m div n = nat (int' m div int' n)"
+  unfolding int'_def zdiv_int [symmetric] by simp
 lemma [code func]: "m div n = fst (Divides.divmod m n)"
   unfolding divmod_def by simp
-lemma [code]: "m mod n = nat (int m mod int n)"
-  unfolding zmod_int [symmetric] by simp
+lemma [code]: "m mod n = nat (int' m mod int' n)"
+  unfolding int'_def zmod_int [symmetric] by simp
 lemma [code func]: "m mod n = snd (Divides.divmod m n)"
   unfolding divmod_def by simp
-lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
-  by simp
-lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
-  by simp
-lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
-  by simp
+lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
+  unfolding int'_def by simp
+lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
+  unfolding int'_def by simp
+lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
+  unfolding int'_def by simp
 lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
 proof (cases "k < 0")
   case True then show ?thesis by simp
@@ -126,26 +132,27 @@
   case False then show ?thesis by (simp add: nat_of_int_def)
 qed
 lemma [code func]:
-  "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
+  "int_aux i n = (if int' n = 0 then i else int_aux (i + 1) (nat_of_int (int' n - 1)))"
 proof -
-  have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
+  have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
   proof -
     assume prem: "n > 0"
-    then have "int n - 1 \<ge> 0" by auto
-    then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
-    with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
+    then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
+    then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
+    with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
   qed
-  then show ?thesis unfolding int_aux_def by simp
+  then show ?thesis unfolding int_aux_def int'_def by simp
 qed
 
 lemma div_nat_code [code func]:
-  "m div k = nat_of_int (fst (divAlg (int m, int k)))"
-  unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
+  "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
+  unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
+  unfolding int'_def [symmetric] nat_of_int_int ..
 
 lemma mod_nat_code [code func]:
-  "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
-  unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
-
+  "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
+  unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
+  unfolding int'_def [symmetric] nat_of_int_int ..
 
 subsection {* Code generator setup for basic functions *}
 
@@ -185,13 +192,13 @@
 *}
 
 consts_code
-  int ("(_)")
+  int' ("(_)")
   nat ("\<module>nat")
 attach {*
 fun nat i = if i < 0 then 0 else i;
 *}
 
-code_const int
+code_const int'
   (SML "_")
   (OCaml "_")
   (Haskell "_")
@@ -392,6 +399,6 @@
   Nat Integer
   EfficientNat Integer
 
-hide const nat_of_int
+hide const nat_of_int int'
 
 end
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/GCD.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -265,7 +265,7 @@
   from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     unfolding dvd_def by blast
   from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
-  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
+  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
   then show ?thesis
     apply (subst zdvd_abs1 [symmetric])
     apply (subst zdvd_abs2 [symmetric])
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/Word.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -989,12 +989,12 @@
 next
   fix xs
   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
-  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
+  show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
   proof (rule bit_list_cases [of xs],simp_all)
     fix ys
     assume [simp]: "xs = \<one>#ys"
     from ind
-    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
+    show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
       by simp
   qed
 qed
@@ -1007,11 +1007,11 @@
     by (simp add: int_nat_two_exp)
 next
   fix bs
-  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0"
+  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0"
     by simp
   also have "... < 2 ^ length bs"
     by (induct bs,simp_all)
-  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs"
+  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
     .
 qed
 
@@ -1027,7 +1027,7 @@
 next
   fix bs
   from bv_to_nat_upper_range [of "bv_not bs"]
-  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
+  show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
     by (simp add: int_nat_two_exp)
 qed
 
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NatBin.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -58,14 +58,14 @@
 apply (case_tac "0 <= z'")
 apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int_of_nat)
+apply (auto elim!: nonneg_eq_int)
 apply (rename_tac m m')
-apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
+apply (subgoal_tac "0 <= int m div int m'")
  prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
 apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int_of_nat (m mod m') " in quorem_div)
+apply (rule_tac r = "int (m mod m') " in quorem_div)
  prefer 2 apply force
-apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
                  of_nat_add [symmetric] of_nat_mult [symmetric]
             del: of_nat_add of_nat_mult)
 done
@@ -74,14 +74,14 @@
 lemma nat_mod_distrib:
      "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
 apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int_of_nat)
+apply (auto elim!: nonneg_eq_int)
 apply (rename_tac m m')
-apply (subgoal_tac "0 <= int_of_nat m mod int_of_nat m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
+apply (subgoal_tac "0 <= int m mod int m'")
+ prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
+apply (rule int_int_eq [THEN iffD1], simp)
+apply (rule_tac q = "int (m div m') " in quorem_mod)
  prefer 2 apply force
-apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
                  of_nat_add [symmetric] of_nat_mult [symmetric]
             del: of_nat_add of_nat_mult)
 done
@@ -97,14 +97,7 @@
 
 (*"neg" is used in rewrite rules for binary comparisons*)
 lemma int_nat_number_of [simp]:
-     "int (number_of v :: nat) =  
-         (if neg (number_of v :: int) then 0  
-          else (number_of v :: int))"
-by (simp del: nat_number_of
-	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
-
-lemma int_of_nat_number_of [simp]:
-     "int_of_nat (number_of v) =  
+     "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
 by (simp del: nat_number_of
@@ -520,9 +513,6 @@
 by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 
 
-(* Push int(.) inwards: *)
-declare zadd_int [symmetric, simp]
-
 lemma lemma1: "(m+m = n+n) = (m = (n::int))"
 by auto
 
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -85,7 +85,7 @@
   (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
    else fib (Suc n) * fib (Suc n) + 1)"
   apply (rule int_int_eq [THEN iffD1]) 
-  apply (simp add: fib_Cassini_int) 
+  apply (simp add: fib_Cassini_int del: of_nat_mult) 
   apply (subst zdiff_int [symmetric]) 
    apply (insert fib_Suc_gr_0 [of n], simp_all)
   done
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -281,7 +281,7 @@
 
 lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   using P_set_card Q_set_card P_set_finite Q_set_finite
-  by (auto simp add: S_def zmult_int setsum_constant)
+  by (auto simp add: S_def setsum_constant)
 
 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   by (auto simp add: S1_def S2_def)
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Numeral.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -457,7 +457,7 @@
 
 lemma odd_less_0:
   "(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases')
+proof (cases z rule: int_cases)
   case (nonneg n)
   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
                              le_imp_0_less [THEN order_less_imp_le])  
@@ -593,7 +593,7 @@
   "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
   by (simp add: int_aux_def)+
 
-lemma [code]:
+lemma [code unfold]:
   "int n = int_aux 0 n"
   by (simp add: int_aux_def)
 
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Presburger.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -383,29 +383,14 @@
   by (simp split add: split_nat)
 
 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  by (auto split add: split_nat) 
-(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+  apply (auto split add: split_nat)
+  apply (rule_tac x="int x" in exI, simp)
+  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+  done
 
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
-  by (case_tac "y \<le> x",simp_all add: zdiff_int)
-
-lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
-  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
-    nat_0_le cong add: conj_cong)
-  apply (rule iffI)
-  apply iprover
-  apply (erule exE)
-  apply (case_tac "x=0")
-  apply (rule_tac x=0 in exI)
-  apply simp
-  apply (case_tac "0 \<le> k")
-  apply iprover
-  apply (simp add: linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-  apply assumption
-  apply (simp add: mult_ac)
-  done
+  by (case_tac "y \<le> x", simp_all)
 
 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
 lemma number_of2: "(0::int) <= Numeral0" by simp
@@ -670,4 +655,4 @@
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   less_number_of
 
-end
\ No newline at end of file
+end
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Real/Float.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -35,7 +35,8 @@
     apply (auto, induct_tac n)
     apply (simp_all add: pow2_def)
     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
-    by (auto simp add: h)
+    apply (auto simp add: h)
+    by (simp add: add_commute)
   show ?thesis
   proof (induct a)
     case (1 n)
@@ -45,7 +46,7 @@
     show ?case
       apply (auto)
       apply (subst pow2_neg[of "- int n"])
-      apply (subst pow2_neg[of "-1 - int n"])
+      apply (subst pow2_neg[of "- int n + -1"])
       apply (auto simp add: g pos)
       done
   qed
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Real/Rational.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -565,7 +565,7 @@
 by (induct n) (simp_all add: of_rat_add)
 
 lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
-by (cases z rule: int_diff_cases', simp add: of_rat_diff)
+by (cases z rule: int_diff_cases, simp add: of_rat_diff)
 
 lemma of_rat_number_of_eq [simp]:
   "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/arith_data.ML	Wed Jun 13 03:31:11 2007 +0200
@@ -601,7 +601,7 @@
         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
         val t1'         = incr_boundvars 1 t1
         val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
-                            (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+                            (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
         val t1_lt_zero  = Const (@{const_name Orderings.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/int_arith1.ML	Wed Jun 13 03:31:11 2007 +0200
@@ -573,10 +573,11 @@
      @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
      @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
      @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
-     of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
-     of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
+     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
+     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
+     @{thm of_int_mult}]
 
-val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
+val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
 
 val Int_Numeral_Base_Simprocs = assoc_fold_simproc
   :: Int_Numeral_Simprocs.combine_numerals
@@ -595,7 +596,6 @@
                       addsimprocs Int_Numeral_Base_Simprocs
                       addcongs [if_weak_cong]}) #>
   arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
-  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
   arith_discrete "IntDef.int"
 
 end;