src/HOL/IntDef.thy

   "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)
   int = "UNIV//intrel"
   by (auto simp add: quotient_def)
-
-definition
-  int :: "nat \<Rightarrow> int"
-where
-  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
 
 instance int :: zero
   Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
 
 instance int :: one

   show "1 * i = i" by (rule zmult_1) 
   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   show "0 \<noteq> (1::int)" by (simp add: Zero_int_def One_int_def)
 qed
 
+abbreviation
+  int_of_nat :: "nat \<Rightarrow> int"
+where
+  "int_of_nat \<equiv> of_nat"
+
 
 subsection{*The @{text "\<le>"} Ordering*}
 
 lemma le:
   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"

 apply (cases w, cases z) 
 apply (simp add: less le add One_int_def)
 done
 
 
-subsection{*@{term int}: Embedding the Naturals into the Integers*}
-
-lemma inj_int: "inj int"
-by (simp add: inj_on_def int_def)
-
-lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
-by (fast elim!: inj_int [THEN injD])
-
-lemma zadd_int: "(int m) + (int n) = int (m + n)"
-  by (simp add: int_def add)
-
-lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
-  by (simp add: zadd_int zadd_assoc [symmetric])
-
-lemma int_mult: "int (m * n) = (int m) * (int n)"
-by (simp add: int_def mult)
-
-text{*Compatibility binding*}
-lemmas zmult_int = int_mult [symmetric]
-
-lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma zless_int [simp]: "(int m < int n) = (m<n)"
-by (simp add: le add int_def linorder_not_le [symmetric]) 
-
-lemma int_less_0_conv [simp]: "~ (int k < 0)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
-by (simp add: linorder_not_less [symmetric])
-
-lemma zero_zle_int [simp]: "(0 \<le> int n)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma int_0 [simp]: "int 0 = (0::int)"
-by (simp add: Zero_int_def [folded int_def])
-
-lemma int_1 [simp]: "int 1 = 1"
-by (simp add: One_int_def [folded int_def])
-
-lemma int_Suc0_eq_1: "int (Suc 0) = 1"
-by (simp add: One_int_def [folded int_def])
-
-lemma int_Suc: "int (Suc m) = 1 + (int m)"
-by (simp add: One_int_def [folded int_def] zadd_int)
-
-
 subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*}
 
 definition
   nat :: "int \<Rightarrow> nat"
 where

     by (simp add: congruent_def) arith
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
 
-lemma nat_int [simp]: "nat(int n) = n"
-by (simp add: nat int_def) 
+lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
+by (simp add: nat int_of_nat_def)
 
 lemma nat_zero [simp]: "nat 0 = 0"
-by (simp only: Zero_int_def [folded int_def] nat_int)
-
-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 (nat z) = z"
+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)
+
+corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
 by simp
 
 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
-by (cases z, simp add: nat le int_def Zero_int_def)
+by (cases z, simp add: nat le Zero_int_def)
 
 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
 apply (cases w, cases z) 
-apply (simp add: nat le linorder_not_le [symmetric] int_def Zero_int_def, arith)
+apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
 done
 
 text{*An alternative condition is @{term "0 \<le> w"} *}
 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 

 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)"
 apply (cases w, cases z) 
-apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
-done
+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 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)
+
+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')
+
+lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
+apply (cases w)
+apply (simp add: nat le int_of_nat_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 zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
+by (insert zless_nat_conj [of 0], auto)
+
+lemma nat_add_distrib:
+     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
+by (cases z, cases z', simp add: nat add le Zero_int_def)
+
+lemma nat_diff_distrib:
+     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
+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 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)
+
+
+subsection{*Lemmas about the Function @{term int} and Orderings*}
+
+lemma negative_zless_0': "- (int_of_nat (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_zle_0': "- int_of_nat 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 not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (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 not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat 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 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)
+  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)"
+  proof
+    assume "a + d \<le> c + b" 
+    thus "\<exists>n. c + b = a + n + d" 
+      by (auto intro!: exI [where x="c+b - (a+d)"])
+  next    
+    assume "\<exists>n. c + b = a + n + d" 
+    then obtain n where "c + b = a + n + d" ..
+    thus "a + d \<le> c + b" by arith
+  qed
+qed
+
+lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
+by (rule  of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *)
+
+text{*This version is proved for all ordered rings, not just integers!
+      It is proved here because attribute @{text arith_split} is not available
+      in theory @{text Ring_and_Field}.
+      But is it really better than just rewriting with @{text abs_if}?*}
+lemma abs_split [arith_split]:
+     "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
+
+subsection {* Constants @{term neg} and @{term iszero} *}
+
+definition
+  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
+where
+  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
+
+definition (*for simplifying equalities*)
+  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
+where
+  "iszero z \<longleftrightarrow> z = 0"
+
+lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+
+subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma iszero_0: "iszero 0"
+by (simp add: iszero_def)
+
+lemma not_iszero_1: "~ iszero 1"
+by (simp add: iszero_def eq_commute)
+
+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"
+by (simp add: linorder_not_less neg_def)
+
+
+subsection{*The Set of Natural Numbers*}
+
+constdefs
+  Nats  :: "'a::semiring_1 set"
+  "Nats == range of_nat"
+
+notation (xsymbols)
+  Nats  ("\<nat>")
+
+lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
+by (simp add: Nats_def)
+
+lemma Nats_0 [simp]: "0 \<in> Nats"
+apply (simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_0 [symmetric])
+done
+
+lemma Nats_1 [simp]: "1 \<in> Nats"
+apply (simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_1 [symmetric])
+done
+
+lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
+apply (auto simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_add [symmetric])
+done
+
+lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
+apply (auto simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_mult [symmetric])
+done
+
+lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
+proof
+  fix n
+  show "of_nat n = id n"  by (induct n, simp_all)
+qed (* belongs in Nat.thy *)
+
+
+subsection{*Embedding of the Integers into any @{text ring_1}:
+@{term of_int}*}
+
+constdefs
+   of_int :: "int => 'a::ring_1"
+   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+
+
+lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
+proof -
+  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
+    by (simp add: congruent_def compare_rls of_nat_add [symmetric]
+            del: of_nat_add) 
+  thus ?thesis
+    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
+qed
+
+lemma of_int_0 [simp]: "of_int 0 = 0"
+by (simp add: of_int Zero_int_def)
+
+lemma of_int_1 [simp]: "of_int 1 = 1"
+by (simp add: of_int One_int_def)
+
+lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
+by (cases w, cases z, simp add: compare_rls of_int add)
+
+lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
+by (cases z, simp add: compare_rls of_int minus)
+
+lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
+by (simp add: diff_minus)
+
+lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
+apply (cases w, cases z)
+apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
+                 mult add_ac)
+done
+
+lemma of_int_le_iff [simp]:
+     "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
+apply (cases w)
+apply (cases z)
+apply (simp add: compare_rls of_int le diff_int_def add minus
+                 of_nat_add [symmetric]   del: of_nat_add)
+done
+
+text{*Special cases where either operand is zero*}
+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 [simp] = of_int_less_iff [of 0, simplified]
+lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
+
+text{*Class for unital rings with characteristic zero.
+ Includes non-ordered rings like the complex numbers.*}
+axclass ring_char_0 < ring_1, semiring_char_0
+
+lemma of_int_eq_iff [simp]:
+     "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
+apply (cases w, cases z, simp add: of_int)
+apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
+apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
+done
+
+text{*Every @{text ordered_idom} has characteristic zero.*}
+instance ordered_idom < ring_char_0 ..
+
+text{*Special cases where either operand is zero*}
+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
+  fix z
+  show "of_int z = id z"
+    by (cases z)
+      (simp add: of_int add minus int_of_nat_def diff_minus)
+qed
+
+
+subsection{*The Set of Integers*}
+
+constdefs
+  Ints  :: "'a::ring_1 set"
+  "Ints == range of_int"
+
+notation (xsymbols)
+  Ints  ("\<int>")
+
+lemma Ints_0 [simp]: "0 \<in> Ints"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_0 [symmetric])
+done
+
+lemma Ints_1 [simp]: "1 \<in> Ints"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_1 [symmetric])
+done
+
+lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_add [symmetric])
+done
+
+lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_minus [symmetric])
+done
+
+lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
+lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_mult [symmetric])
+done
+
+text{*Collapse nested embeddings*}
+lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
+by (induct n, auto)
+
+lemma Ints_cases [cases set: Ints]:
+  assumes "q \<in> \<int>"
+  obtains (of_int) z where "q = of_int z"
+  unfolding Ints_def
+proof -
+  from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
+  then obtain z where "q = of_int z" ..
+  then show thesis ..
+qed
+
+lemma Ints_induct [case_names of_int, induct set: Ints]:
+  "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
+  by (rule Ints_cases) auto
+
+
+(* int (Suc n) = 1 + int n *)
+
+
+
+subsection{*More Properties of @{term setsum} and  @{term setprod}*}
+
+text{*By Jeremy Avigad*}
+
+
+lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma setprod_nonzero_nat:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_nat:
+    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
+  by (rule setprod_zero_eq, auto)
+
+lemma setprod_nonzero_int:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_int:
+    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
+  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.*}
+
+lemma zless_iff_Suc_zadd':
+    "(w < z) = (\<exists>n. z = w + int_of_nat (Suc n))"
+apply (cases z, cases w)
+apply (auto simp add: le add int_of_nat_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))"
+apply (cases x)
+apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
+apply (rule_tac x="y - Suc x" in exI, arith)
+done
+
+theorem int_cases':
+     "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (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])
+done
+
+theorem int_induct':
+     "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (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"
+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)
+done
+
+lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
+by (cases z, 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)})"
+
+lemma inj_int: "inj int"
+by (simp add: inj_on_def int_def)
+
+lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
+by (fast elim!: inj_int [THEN injD])
+
+lemma zadd_int: "(int m) + (int n) = int (m + n)"
+  by (simp add: int_def add)
+
+lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
+  by (simp add: zadd_int zadd_assoc [symmetric])
+
+lemma int_mult: "int (m * n) = (int m) * (int n)"
+by (simp add: int_def mult)
+
+text{*Compatibility binding*}
+lemmas zmult_int = int_mult [symmetric]
+
+lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma zless_int [simp]: "(int m < int n) = (m<n)"
+by (simp add: le add int_def linorder_not_le [symmetric]) 
+
+lemma int_less_0_conv [simp]: "~ (int k < 0)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma zero_zle_int [simp]: "(0 \<le> int n)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma int_0 [simp]: "int 0 = (0::int)"
+by (simp add: Zero_int_def [folded int_def])
+
+lemma int_1 [simp]: "int 1 = 1"
+by (simp add: One_int_def [folded int_def])
+
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
+by (simp add: One_int_def [folded int_def])
+
+lemma int_Suc: "int (Suc m) = 1 + (int m)"
+by (simp add: One_int_def [folded int_def] zadd_int)
+
+lemma nat_int [simp]: "nat(int n) = n"
+by (simp add: nat 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 (nat z) = z"
+by simp
 
 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 m else m=0)"

 done
 
 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)
-
-lemma nat_add_distrib:
-     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
-by (cases z, cases z', simp add: nat add le int_def Zero_int_def)
-
-lemma nat_diff_distrib:
-     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
-by (cases z, cases z', 
-    simp add: nat add minus diff_minus le int_def 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 m < z)"
 by (cases z, simp add: nat le int_def  linorder_not_le [symmetric], arith)
-
-
-subsection{*Lemmas about the Function @{term int} and Orderings*}
 
 lemma negative_zless_0: "- (int (Suc n)) < 0"
 by (simp add: order_less_le)
 
 lemma negative_zless [iff]: "- (int (Suc n)) < int m"

 qed
 
 lemma abs_int_eq [simp]: "abs (int m) = int m"
 by (simp add: abs_if)
 
-text{*This version is proved for all ordered rings, not just integers!
-      It is proved here because attribute @{text arith_split} is not available
-      in theory @{text Ring_and_Field}.
-      But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split]:
-     "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
-by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
-
-subsection {* Constants @{term neg} and @{term iszero} *}
-
-definition
-  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
-where
-  [code inline]: "neg Z \<longleftrightarrow> Z < 0"
-
-definition (*for simplifying equalities*)
-  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
-where
-  "iszero z \<longleftrightarrow> z = 0"
-
 lemma not_neg_int [simp]: "~ neg(int n)"
 by (simp add: neg_def)
 
 lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
 by (simp add: neg_def neg_less_0_iff_less)
 
-lemmas neg_eq_less_0 = neg_def
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-by (simp add: neg_def linorder_not_less)
-
-
-subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_def)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
-
-lemma iszero_0: "iszero 0"
-by (simp add: iszero_def)
-
-lemma not_iszero_1: "~ iszero 1"
-by (simp add: iszero_def eq_commute)
-
-lemma neg_nat: "neg z ==> nat z = 0"
-by (simp add: neg_def order_less_imp_le) 
-
 lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
 by (simp add: linorder_not_less neg_def)
-
-
-subsection{*The Set of Natural Numbers*}
-
-constdefs
-  Nats  :: "'a::semiring_1 set"
-  "Nats == range of_nat"
-
-notation (xsymbols)
-  Nats  ("\<nat>")
-
-lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
-by (simp add: Nats_def)
-
-lemma Nats_0 [simp]: "0 \<in> Nats"
-apply (simp add: Nats_def)
-apply (rule range_eqI)
-apply (rule of_nat_0 [symmetric])
-done
-
-lemma Nats_1 [simp]: "1 \<in> Nats"
-apply (simp add: Nats_def)
-apply (rule range_eqI)
-apply (rule of_nat_1 [symmetric])
-done
-
-lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
-apply (auto simp add: Nats_def)
-apply (rule range_eqI)
-apply (rule of_nat_add [symmetric])
-done
-
-lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
-apply (auto simp add: Nats_def)
-apply (rule range_eqI)
-apply (rule of_nat_mult [symmetric])
-done
 
 text{*Agreement with the specific embedding for the integers*}
 lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
 proof
   fix n
   show "int n = of_nat n"  by (induct n, simp_all add: int_Suc add_ac)
 qed
 
-lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
-proof
-  fix n
-  show "of_nat n = id n"  by (induct n, simp_all)
-qed
-
-
-subsection{*Embedding of the Integers into any @{text ring_1}:
-@{term of_int}*}
-
-constdefs
-   of_int :: "int => 'a::ring_1"
-   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
-
-
-lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
-proof -
-  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
-    by (simp add: congruent_def compare_rls of_nat_add [symmetric]
-            del: of_nat_add) 
-  thus ?thesis
-    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
-qed
-
-lemma of_int_0 [simp]: "of_int 0 = 0"
-by (simp add: of_int Zero_int_def int_def)
-
-lemma of_int_1 [simp]: "of_int 1 = 1"
-by (simp add: of_int One_int_def int_def)
-
-lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
-by (cases w, cases z, simp add: compare_rls of_int add)
-
-lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
-by (cases z, simp add: compare_rls of_int minus)
-
-lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z"
-by (simp add: diff_minus)
-
-lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
-apply (cases w, cases z)
-apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
-                 mult add_ac)
-done
-
-lemma of_int_le_iff [simp]:
-     "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
-apply (cases w)
-apply (cases z)
-apply (simp add: compare_rls of_int le diff_int_def add minus
-                 of_nat_add [symmetric]   del: of_nat_add)
-done
-
-text{*Special cases where either operand is zero*}
-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 [simp] = of_int_less_iff [of 0, simplified]
-lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
-
-text{*Class for unital rings with characteristic zero.
- Includes non-ordered rings like the complex numbers.*}
-axclass ring_char_0 < ring_1, semiring_char_0
-
-lemma of_int_eq_iff [simp]:
-     "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
-apply (cases w, cases z, simp add: of_int)
-apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
-apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
-done
-
-text{*Every @{text ordered_idom} has characteristic zero.*}
-instance ordered_idom < ring_char_0 ..
-
-text{*Special cases where either operand is zero*}
-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
-  fix z
-  show "of_int z = id z"
-    by (cases z)
-      (simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus)
-qed
-
-
-subsection{*The Set of Integers*}
-
-constdefs
-  Ints  :: "'a::ring_1 set"
-  "Ints == range of_int"
-
-notation (xsymbols)
-  Ints  ("\<int>")
-
-lemma Ints_0 [simp]: "0 \<in> Ints"
-apply (simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_0 [symmetric])
-done
-
-lemma Ints_1 [simp]: "1 \<in> Ints"
-apply (simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_1 [symmetric])
-done
-
-lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_add [symmetric])
-done
-
-lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_minus [symmetric])
-done
-
-lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
-lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_mult [symmetric])
-done
-
-text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
-by (induct n, auto)
-
 lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
 by (simp add: int_eq_of_nat)
 
-lemma Ints_cases [cases set: Ints]:
-  assumes "q \<in> \<int>"
-  obtains (of_int) z where "q = of_int z"
-  unfolding Ints_def
-proof -
-  from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
-  then obtain z where "q = of_int z" ..
-  then show thesis ..
-qed
-
-lemma Ints_induct [case_names of_int, induct set: Ints]:
-  "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q"
-  by (rule Ints_cases) auto
-
-
-(* int (Suc n) = 1 + int n *)
-
-
-
-subsection{*More Properties of @{term setsum} and  @{term setprod}*}
-
-text{*By Jeremy Avigad*}
-
-
-lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
-lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
 lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
   by (simp add: int_eq_of_nat of_nat_setsum)
 
-lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
-lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
 lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
   by (simp add: int_eq_of_nat of_nat_setprod)
-
-lemma setprod_nonzero_nat:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_nat:
-    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
-    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
-  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.*}
 
 lemma zless_iff_Suc_zadd:

 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
-
-lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
-apply (cases z)
-apply (simp_all add: not_zle_0_negative del: int_Suc)
 done
 
 lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
 
 lemmas [simp] = int_Suc