# HG changeset patch
# User paulson
# Date 1069321320 -3600
# Node ID 3d0c6238162a66931a21a597f2458ddf9a9244b8
# Parent  a431e0aa34c9642b9286619fd76d8dafeb192c40
conversion of Integ/Int_lemmas.ML to Isar script

diff -r a431e0aa34c9 -r 3d0c6238162a src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Nov 20 10:41:39 2003 +0100
+++ b/src/HOL/Integ/Bin.ML	Thu Nov 20 10:42:00 2003 +0100
@@ -254,6 +254,8 @@
 by (Simp_tac 1);
 qed "nonzero_number_of_Min"; 
 
+fun int_case_tac x = res_inst_tac [("z",x)] int_cases;
+
 Goalw [iszero_def]
      "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
 by (int_case_tac "number_of w" 1); 
diff -r a431e0aa34c9 -r 3d0c6238162a src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Thu Nov 20 10:41:39 2003 +0100
+++ b/src/HOL/Integ/Int.thy	Thu Nov 20 10:42:00 2003 +0100
@@ -2,12 +2,11 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
-
-Type "int" is a linear order
 *)
 
-theory Int = IntDef
-files ("Int_lemmas.ML"):
+header {*Type "int" is a Linear Order and Other Lemmas*}
+
+theory Int = IntDef:
 
 instance int :: order
 proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
@@ -19,12 +18,527 @@
 proof qed (rule zle_linear)
 
 constdefs
- nat  :: "int => nat"
-"nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
+   nat  :: "int => nat"
+    "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
 
 defs (overloaded)
-zabs_def:  "abs(i::int) == if i < 0 then -i else i"
+    zabs_def:  "abs(i::int) == if i < 0 then -i else i"
+
+
+lemma int_0 [simp]: "int 0 = (0::int)"
+by (simp add: Zero_int_def)
+
+lemma int_1 [simp]: "int 1 = 1"
+by (simp add: One_int_def)
+
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
+by (simp add: One_int_def One_nat_def)
+
+lemma neg_eq_less_0: "neg x = (x < 0)"
+by (unfold zdiff_def zless_def, auto)
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 <= x)"
+apply (unfold zle_def)
+apply (simp add: neg_eq_less_0)
+done
+
+subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_eq_less_0)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: One_int_def neg_eq_less_0)
+
+lemma iszero_0: "iszero 0"
+by (simp add: iszero_def)
+
+lemma not_iszero_1: "~ iszero 1"
+by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
+
+lemma int_0_less_1: "0 < (1::int)"
+by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
+
+lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
+by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
+
+
+
+subsection{*@{text Abel_Cancel} simproc on the integers*}
+
+(* Lemmas needed for the simprocs *)
+
+(*Deletion of other terms in the formula, seeking the -x at the front of z*)
+lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
+apply (subst zadd_left_commute)
+apply (rule zadd_left_cancel)
+done
+
+(*A further rule to deal with the case that
+  everything gets cancelled on the right.*)
+lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
+apply (subst zadd_left_commute)
+apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
+apply (simp add: eq_zdiff_eq [symmetric])
+done
+
+(*Legacy ML bindings, but no longer the structure Int.*)
+ML
+{*
+val Int_thy = the_context ()
+val zabs_def = thm "zabs_def"
+val nat_def  = thm "nat_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 zadd_cancel_21 = thm "zadd_cancel_21";
+val zadd_cancel_end = thm "zadd_cancel_end";
+
+structure Int_Cancel_Data =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+
+  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context()))
+  val T		= HOLogic.intT
+  val zero		= Const ("0", HOLogic.intT)
+  val restrict_to_left  = restrict_to_left
+  val add_cancel_21	= zadd_cancel_21
+  val add_cancel_end	= zadd_cancel_end
+  val add_left_cancel	= zadd_left_cancel
+  val add_assoc		= zadd_assoc
+  val add_commute	= zadd_commute
+  val add_left_commute	= zadd_left_commute
+  val add_0		= zadd_0
+  val add_0_right	= zadd_0_right
+
+  val eq_diff_eq	= eq_zdiff_eq
+  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
+  fun dest_eqI th = 
+      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
+	      (HOLogic.dest_Trueprop (concl_of th)))
+
+  val diff_def		= zdiff_def
+  val minus_add_distrib	= zminus_zadd_distrib
+  val minus_minus	= zminus_zminus
+  val minus_0		= zminus_0
+  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2]
+  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
+end;
+
+structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
+
+Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
+*}
+
+
+subsection{*Misc Results*}
+
+lemma zminus_zdiff_eq [simp]: "- (z - y) = y - (z::int)"
+by simp
+
+lemma zless_eq_neg: "(w<z) = neg(w-z)"
+by (simp add: zless_def)
+
+lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
+by (simp add: iszero_def zdiff_eq_eq)
+
+lemma zle_eq_not_neg: "(w<=z) = (~ neg(z-w))"
+by (simp add: zle_def zless_def)
+
+subsection{*Inequality reasoning*}
+
+lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
+apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
+apply (rule_tac x = "Suc n" in exI)
+apply (simp add: int_Suc)
+done
+
+lemma add1_zle_eq: "(w + (1::int) <= z) = (w<z)"
+apply (simp add: zle_def zless_add1_eq)
+apply (auto intro: zless_asym zle_anti_sym
+            simp add: order_less_imp_le symmetric zle_def)
+done
+
+lemma add1_left_zle_eq: "((1::int) + w <= z) = (w<z)"
+apply (subst zadd_commute)
+apply (rule add1_zle_eq)
+done
+
+
+subsection{*Monotonicity results*}
+
+lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
+by simp
+
+lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
+by simp
+
+lemma zadd_right_cancel_zle [simp] : "(v+z <= w+z) = (v <= (w::int))"
+by simp
+
+lemma zadd_left_cancel_zle [simp] : "(z+v <= z+w) = (v <= (w::int))"
+by simp
+
+(*"v<=w ==> v+z <= w+z"*)
+lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
+
+(*"v<=w ==> z+v <= z+w"*)
+lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
+
+(*"v<=w ==> v+z <= w+z"*)
+lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
+
+(*"v<=w ==> z+v <= z+w"*)
+lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
+
+lemma zadd_zle_mono: "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)"
+by (erule zadd_zle_mono1 [THEN zle_trans], simp)
+
+lemma zadd_zless_mono: "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)"
+by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
+
+
+subsection{*Comparison laws*}
+
+lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zminus_zle_zminus [simp]: "(- x <= - y) = (y <= (x::int))"
+by (simp add: zle_def)
+
+text{*The next several equations can make the simplifier loop!*}
+
+lemma zless_zminus: "(x < - y) = (y < - (x::int))"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zminus_zless: "(- x < y) = (- y < (x::int))"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zle_zminus: "(x <= - y) = (y <= - (x::int))"
+by (simp add: zle_def zminus_zless)
+
+lemma zminus_zle: "(- x <= y) = (- y <= (x::int))"
+by (simp add: zle_def zless_zminus)
+
+lemma equation_zminus: "(x = - y) = (y = - (x::int))"
+by auto
+
+lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
+by auto
+
+
+subsection{*Instances of the equations above, for zero*}
+
+(*instantiate a variable to zero and simplify*)
+
+declare zless_zminus [of 0, simplified, simp]
+declare zminus_zless [of _ 0, simplified, simp]
+declare zle_zminus   [of 0, simplified, simp]
+declare zminus_zle [of _ 0, simplified, simp]
+declare equation_zminus [of 0, simplified, simp]
+declare zminus_equation [of _ 0, simplified, simp]
+
+lemma negative_zless_0: "- (int (Suc n)) < 0"
+by (simp add: zless_def)
+
+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 n <= 0"
+by (simp add: zminus_zle)
+
+lemma negative_zle [iff]: "- int n <= int m"
+by (simp add: zless_def zle_def zdiff_def zadd_int)
+
+lemma not_zle_0_negative [simp]: "~(0 <= - (int (Suc n)))"
+by (subst zle_zminus, simp)
+
+lemma int_zle_neg: "(int n <= - int m) = (n = 0 & m = 0)"
+apply safe 
+apply (drule_tac [2] zle_zminus [THEN iffD1])
+apply (auto dest: zle_trans [OF _ negative_zle_0]) 
+done
+
+lemma not_int_zless_negative [simp]: "~(int n < - int m)"
+by (simp add: zle_def [symmetric])
+
+lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
+apply (rule iffI)
+apply (rule int_zle_neg [THEN iffD1])
+apply (drule sym)
+apply (simp_all (no_asm_simp))
+done
 
-use "Int_lemmas.ML"
+lemma zle_iff_zadd: "(w <= z) = (EX n. z = w + int n)"
+by (force intro: exI [of _ "0::nat"] 
+            intro!: not_sym [THEN not0_implies_Suc]
+            simp add: zless_iff_Suc_zadd int_le_less)
+
+lemma abs_int_eq [simp]: "abs (int m) = int m"
+by (simp add: zabs_def)
+
+
+subsection{*nat: magnitide of an integer, as a natural number*}
+
+lemma nat_int [simp]: "nat(int n) = n"
+by (unfold nat_def, auto)
+
+lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
+apply (unfold nat_def)
+apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
+done
+
+lemma nat_zero [simp]: "nat 0 = 0"
+apply (unfold Zero_int_def)
+apply (rule nat_int)
+done
+
+lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
+apply (drule not_neg_eq_ge_0 [THEN iffD1])
+apply (drule zle_imp_zless_or_eq)
+apply (auto simp add: zless_iff_Suc_zadd)
+done
+
+lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
+by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd zdiff_eq_eq [symmetric] zdiff_def)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (unfold nat_def, auto)
+
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+apply (case_tac "neg z")
+apply (erule_tac [2] not_neg_nat [THEN subst])
+apply (auto simp add: neg_nat)
+apply (auto dest: order_less_trans simp add: neg_eq_less_0)
+done
+
+lemma nat_0_le [simp]: "0 <= z ==> int (nat z) = z"
+by (simp add: neg_eq_less_0 zle_def not_neg_nat)
+
+lemma nat_le_0 [simp]: "z <= 0 ==> nat z = 0"
+by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
+
+(*An alternative condition is  0 <= w  *)
+lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
+apply (subst zless_int [symmetric])
+apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
+apply (case_tac "neg w")
+ apply (simp add: neg_eq_less_0 neg_nat)
+ apply (blast intro: order_less_trans)
+apply (simp add: not_neg_nat)
+done
+
+lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
+apply (case_tac "0 < z")
+apply (auto simp add: nat_mono_iff linorder_not_less)
+done
+
+(* a case theorem distinguishing non-negative and negative int *)  
+
+lemma int_cases: 
+     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
+apply (case_tac "neg z")
+apply (fast dest!: negD)
+apply (drule not_neg_nat [symmetric], auto) 
+done
+
+
+subsection{*Monotonicity of Multiplication*}
+
+lemma zmult_zle_mono1_lemma: "i <= (j::int) ==> i * int k <= j * int k"
+apply (induct_tac "k")
+apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
+done
+
+lemma zmult_zle_mono1: "[| i <= j;  (0::int) <= k |] ==> i*k <= j*k"
+apply (rule_tac t = k in not_neg_nat [THEN subst])
+apply (erule_tac [2] zmult_zle_mono1_lemma)
+apply (simp (no_asm_use) add: not_neg_eq_ge_0)
+done
+
+lemma zmult_zle_mono1_neg: "[| i <= j;  k <= (0::int) |] ==> j*k <= i*k"
+apply (rule zminus_zle_zminus [THEN iffD1])
+apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
+done
+
+lemma zmult_zle_mono2: "[| i <= j;  (0::int) <= k |] ==> k*i <= k*j"
+apply (drule zmult_zle_mono1)
+apply (simp_all add: zmult_commute)
+done
+
+lemma zmult_zle_mono2_neg: "[| i <= j;  k <= (0::int) |] ==> k*j <= k*i"
+apply (drule zmult_zle_mono1_neg)
+apply (simp_all add: zmult_commute)
+done
+
+(* <= monotonicity, BOTH arguments*)
+lemma zmult_zle_mono: "[| i <= j;  k <= l;  (0::int) <= j;  (0::int) <= k |] ==> i*k <= j*l"
+apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
+apply (erule zmult_zle_mono2, assumption)
+done
+
+
+subsection{*strict, in 1st argument; proof is by induction on k>0*}
+
+lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
+apply (induct_tac "k", simp) 
+apply (simp add: int_Suc)
+apply (case_tac "n=0")
+apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
+done
+
+lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
+apply (rule_tac t = k in not_neg_nat [THEN subst])
+apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
+apply (simp add: not_neg_eq_ge_0 order_le_less)
+apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
+done
+
+lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
+apply (drule zmult_zless_mono2)
+apply (simp_all add: zmult_commute)
+done
+
+(* < monotonicity, BOTH arguments*)
+lemma zmult_zless_mono: "[| i < j;  k < l;  (0::int) < j;  (0::int) < k |] ==> i*k < j*l"
+apply (erule zmult_zless_mono1 [THEN order_less_trans], assumption)
+apply (erule zmult_zless_mono2, assumption)
+done
+
+lemma zmult_zless_mono1_neg: "[| i<j;  k < (0::int) |] ==> j*k < i*k"
+apply (rule zminus_zless_zminus [THEN iffD1])
+apply (simp add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
+done
+
+lemma zmult_zless_mono2_neg: "[| i<j;  k < (0::int) |] ==> k*j < k*i"
+apply (rule zminus_zless_zminus [THEN iffD1])
+apply (simp add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
+done
+
+lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
+apply (case_tac "m < (0::int) ")
+apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
+apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
+done
+
+
+text{*Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
+    but not (yet?) for k*m < n*k.*}
+
+lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))"
+apply (case_tac "k = (0::int) ")
+apply (auto simp add: linorder_neq_iff zmult_zless_mono1 zmult_zless_mono1_neg)
+apply (auto simp add: linorder_not_less 
+                      linorder_not_le [symmetric, of "m*k"]
+                      linorder_not_le [symmetric, of m])
+apply (erule_tac [!] notE)
+apply (auto simp add: order_less_imp_le zmult_zle_mono1 zmult_zle_mono1_neg)
+done
+
+
+lemma zmult_zless_cancel1:
+     "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
+by (simp add: zmult_commute [of k] zmult_zless_cancel2)
+
+lemma zmult_zle_cancel2:
+     "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
+by (simp add: linorder_not_less [symmetric] zmult_zless_cancel2)
+
+lemma zmult_zle_cancel1:
+     "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"
+by (simp add: linorder_not_less [symmetric] zmult_zless_cancel1)
+
+lemma zmult_cancel2 [simp]: "(m*k = n*k) = (k = (0::int) | m=n)"
+apply (cut_tac linorder_less_linear [of 0 k])
+apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1 
+             simp add: linorder_neq_iff)
+done
+
+lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
+by (simp add: zmult_commute [of k] zmult_cancel2)
+
+(*Analogous to zadd_int*)
+lemma zdiff_int [rule_format (no_asm)]: "n<=m --> int m - int n = int (m-n)"
+apply (induct_tac m n rule: diff_induct)
+apply (auto simp add: int_Suc symmetric zdiff_def)
+done
+
+ML
+{*
+val zminus_zdiff_eq = thm "zminus_zdiff_eq";
+val zless_eq_neg = thm "zless_eq_neg";
+val eq_eq_iszero = thm "eq_eq_iszero";
+val zle_eq_not_neg = thm "zle_eq_not_neg";
+val zless_add1_eq = thm "zless_add1_eq";
+val add1_zle_eq = thm "add1_zle_eq";
+val add1_left_zle_eq = thm "add1_left_zle_eq";
+val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
+val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
+val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
+val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
+val zadd_zless_mono1 = thm "zadd_zless_mono1";
+val zadd_zless_mono2 = thm "zadd_zless_mono2";
+val zadd_zle_mono1 = thm "zadd_zle_mono1";
+val zadd_zle_mono2 = thm "zadd_zle_mono2";
+val zadd_zle_mono = thm "zadd_zle_mono";
+val zadd_zless_mono = thm "zadd_zless_mono";
+val zminus_zless_zminus = thm "zminus_zless_zminus";
+val zminus_zle_zminus = thm "zminus_zle_zminus";
+val zless_zminus = thm "zless_zminus";
+val zminus_zless = thm "zminus_zless";
+val zle_zminus = thm "zle_zminus";
+val zminus_zle = thm "zminus_zle";
+val equation_zminus = thm "equation_zminus";
+val zminus_equation = thm "zminus_equation";
+val negative_zless_0 = thm "negative_zless_0";
+val negative_zless = thm "negative_zless";
+val negative_zle_0 = thm "negative_zle_0";
+val negative_zle = thm "negative_zle";
+val not_zle_0_negative = thm "not_zle_0_negative";
+val int_zle_neg = thm "int_zle_neg";
+val not_int_zless_negative = thm "not_int_zless_negative";
+val negative_eq_positive = thm "negative_eq_positive";
+val zle_iff_zadd = thm "zle_iff_zadd";
+val abs_int_eq = thm "abs_int_eq";
+val 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 negD = thm "negD";
+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 zmult_zle_mono1 = thm "zmult_zle_mono1";
+val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
+val zmult_zle_mono2 = thm "zmult_zle_mono2";
+val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
+val zmult_zle_mono = thm "zmult_zle_mono";
+val zmult_zless_mono2 = thm "zmult_zless_mono2";
+val zmult_zless_mono1 = thm "zmult_zless_mono1";
+val zmult_zless_mono = thm "zmult_zless_mono";
+val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
+val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
+val zmult_eq_0_iff = thm "zmult_eq_0_iff";
+val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
+val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
+val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
+val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
+val zmult_cancel2 = thm "zmult_cancel2";
+val zmult_cancel1 = thm "zmult_cancel1";
+val zdiff_int = thm "zdiff_int";
+*}
 
 end
diff -r a431e0aa34c9 -r 3d0c6238162a src/HOL/Integ/Int_lemmas.ML
--- a/src/HOL/Integ/Int_lemmas.ML	Thu Nov 20 10:41:39 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,557 +0,0 @@
-(*  Title:      HOL/Integ/Int_lemmas.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Type "int" is a linear order
-
-And many further lemmas
-*)
-
-(*Legacy ML bindings, but no longer the structure Int.*)
-val Int_thy = the_context ();
-val zabs_def = thm "zabs_def";
-val nat_def  = thm "nat_def";
-
-Goal "int 0 = (0::int)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "int_0";
-
-Goal "int 1 = 1";
-by (simp_tac (simpset() addsimps [One_int_def]) 1); 
-qed "int_1";
-
-Goal "int (Suc 0) = 1";
-by (simp_tac (simpset() addsimps [One_int_def, One_nat_def]) 1); 
-qed "int_Suc0_eq_1";
-
-Goalw [zdiff_def,zless_def] "neg x = (x < 0)";
-by Auto_tac; 
-qed "neg_eq_less_0"; 
-
-Goalw [zle_def] "(~neg x) = (0 <= x)";
-by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1); 
-qed "not_neg_eq_ge_0"; 
-
-(** Needed to simplify inequalities when Numeral1 can get simplified to 1 **)
-
-Goal "~ neg 0";
-by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1);  
-qed "not_neg_0"; 
-
-Goal "~ neg 1";
-by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1);  
-qed "not_neg_1"; 
-
-Goal "iszero 0";
-by (simp_tac (simpset() addsimps [iszero_def]) 1);
-qed "iszero_0"; 
-
-Goal "~ iszero 1";
-by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def, 
-                                  iszero_def]) 1);
-qed "not_iszero_1"; 
-
-Goal "0 < (1::int)";
-by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); 
-qed "int_0_less_1";
-
-Goal "0 \\<noteq> (1::int)";
-by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); 
-qed "int_0_neq_1";
-
-Addsimps [int_0, int_1, int_0_neq_1];
-
-
-(*** Abel_Cancel simproc on the integers ***)
-
-(* Lemmas needed for the simprocs *)
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)";
-by (stac zadd_left_commute 1);
-by (rtac zadd_left_cancel 1);
-qed "zadd_cancel_21";
-
-(*A further rule to deal with the case that
-  everything gets cancelled on the right.*)
-Goal "((x::int) + (y + z) = y) = (x = -z)";
-by (stac zadd_left_commute 1);
-by (res_inst_tac [("t", "y")] (zadd_0_right RS subst) 1
-    THEN stac zadd_left_cancel 1);
-by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1);
-qed "zadd_cancel_end";
-
-
-structure Int_Cancel_Data =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-
-  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context ()))
-  val T		= HOLogic.intT
-  val zero		= Const ("0", HOLogic.intT)
-  val restrict_to_left  = restrict_to_left
-  val add_cancel_21	= zadd_cancel_21
-  val add_cancel_end	= zadd_cancel_end
-  val add_left_cancel	= zadd_left_cancel
-  val add_assoc		= zadd_assoc
-  val add_commute	= zadd_commute
-  val add_left_commute	= zadd_left_commute
-  val add_0		= zadd_0
-  val add_0_right	= zadd_0_right
-
-  val eq_diff_eq	= eq_zdiff_eq
-  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
-  fun dest_eqI th = 
-      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
-	      (HOLogic.dest_Trueprop (concl_of th)))
-
-  val diff_def		= zdiff_def
-  val minus_add_distrib	= zminus_zadd_distrib
-  val minus_minus	= zminus_zminus
-  val minus_0		= zminus_0
-  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2]
-  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
-end;
-
-structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
-
-Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-
-
-
-(*** misc ***)
-
-Goal "- (z - y) = y - (z::int)";
-by (Simp_tac 1);
-qed "zminus_zdiff_eq";
-Addsimps [zminus_zdiff_eq];
-
-Goal "(w<z) = neg(w-z)";
-by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eq_neg";
-
-Goal "(w=z) = iszero(w-z)";
-by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1);
-qed "eq_eq_iszero";
-
-Goal "(w<=z) = (~ neg(z-w))";
-by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
-qed "zle_eq_not_neg";
-
-(** Inequality reasoning **)
-
-Goal "(w < z + (1::int)) = (w<z | w=z)";
-by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, int_Suc,
-                                  gr0_conv_Suc, zero_reorient]));
-by (res_inst_tac [("x","Suc n")] exI 1); 
-by (simp_tac (simpset() addsimps [int_Suc]) 1); 
-qed "zless_add1_eq";
-
-Goal "(w + (1::int) <= z) = (w<z)";
-by (asm_full_simp_tac (simpset() addsimps [zle_def, zless_add1_eq]) 1); 
-by (auto_tac (claset() addIs [zle_anti_sym],
-	      simpset() addsimps [order_less_imp_le, symmetric zle_def]));
-qed "add1_zle_eq";
-
-Goal "((1::int) + w <= z) = (w<z)";
-by (stac zadd_commute 1);
-by (rtac add1_zle_eq 1);
-qed "add1_left_zle_eq";
-
-
-(*** Monotonicity results ***)
-
-Goal "(v+z < w+z) = (v < (w::int))";
-by (Simp_tac 1);
-qed "zadd_right_cancel_zless";
-
-Goal "(z+v < z+w) = (v < (w::int))";
-by (Simp_tac 1);
-qed "zadd_left_cancel_zless";
-
-Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
-
-Goal "(v+z <= w+z) = (v <= (w::int))";
-by (Simp_tac 1);
-qed "zadd_right_cancel_zle";
-
-Goal "(z+v <= z+w) = (v <= (w::int))";
-by (Simp_tac 1);
-qed "zadd_left_cancel_zle";
-
-Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
-
-(*"v<=w ==> v+z <= w+z"*)
-bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
-
-(*"v<=w ==> z+v <= z+w"*)
-bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
-
-(*"v<=w ==> v+z <= w+z"*)
-bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
-
-(*"v<=w ==> z+v <= z+w"*)
-bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
-
-Goal "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)";
-by (etac (zadd_zle_mono1 RS zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zle_mono";
-
-Goal "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)";
-by (etac (zadd_zless_mono1 RS order_less_le_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zless_mono";
-
-
-(*** Comparison laws ***)
-
-Goal "(- x < - y) = (y < (x::int))";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zminus_zless_zminus"; 
-Addsimps [zminus_zless_zminus];
-
-Goal "(- x <= - y) = (y <= (x::int))";
-by (simp_tac (simpset() addsimps [zle_def]) 1);
-qed "zminus_zle_zminus"; 
-Addsimps [zminus_zle_zminus];
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::int))";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zless_zminus"; 
-
-Goal "(- x < y) = (- y < (x::int))";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zminus_zless"; 
-
-Goal "(x <= - y) = (y <= - (x::int))";
-by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1);
-qed "zle_zminus"; 
-
-Goal "(- x <= y) = (- y <= (x::int))";
-by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1);
-qed "zminus_zle"; 
-
-Goal "(x = - y) = (y = - (x::int))";
-by Auto_tac;
-qed "equation_zminus";
-
-Goal "(- x = y) = (- (y::int) = x)";
-by Auto_tac;
-qed "zminus_equation";
-
-
-(** Instances of the equations above, for zero **)
-
-(*instantiate a variable to zero and simplify*)
-fun zero_instance v th = simplify (simpset()) (inst v "0" th);
-
-Addsimps [zero_instance "x" zless_zminus,
-          zero_instance "y" zminus_zless,
-          zero_instance "x" zle_zminus,
-          zero_instance "y" zminus_zle,
-          zero_instance "x" equation_zminus,
-          zero_instance "y" zminus_equation];
-
-
-Goal "- (int (Suc n)) < 0";
-by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "negative_zless_0"; 
-
-Goal "- (int (Suc n)) < int m";
-by (rtac (negative_zless_0 RS order_less_le_trans) 1);
-by (Simp_tac 1); 
-qed "negative_zless"; 
-AddIffs [negative_zless]; 
-
-Goal "- int n <= 0";
-by (simp_tac (simpset() addsimps [zminus_zle]) 1);
-qed "negative_zle_0"; 
-
-Goal "- int n <= int m";
-by (simp_tac (simpset() addsimps [zless_def, zle_def, zdiff_def, zadd_int]) 1);
-qed "negative_zle"; 
-AddIffs [negative_zle]; 
-
-Goal "~(0 <= - (int (Suc n)))";
-by (stac zle_zminus 1);
-by (Simp_tac 1);
-qed "not_zle_0_negative"; 
-Addsimps [not_zle_0_negative]; 
-
-Goal "(int n <= - int m) = (n = 0 & m = 0)"; 
-by Safe_tac; 
-by (Simp_tac 3); 
-by (dtac (zle_zminus RS iffD1) 2); 
-by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); 
-by (ALLGOALS Asm_full_simp_tac); 
-qed "int_zle_neg"; 
-
-Goal "~(int n < - int m)";
-by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); 
-qed "not_int_zless_negative"; 
-
-Goal "(- int n = int m) = (n = 0 & m = 0)"; 
-by (rtac iffI 1);
-by (rtac (int_zle_neg RS iffD1) 1); 
-by (dtac sym 1); 
-by (ALLGOALS Asm_simp_tac); 
-qed "negative_eq_positive"; 
-
-Addsimps [negative_eq_positive, not_int_zless_negative]; 
-
-
-Goal "(w <= z) = (EX n. z = w + int n)";
-by (auto_tac (claset() addIs [inst "x" "0::nat" exI]
-		       addSIs [not_sym RS not0_implies_Suc],
-	      simpset() addsimps [zless_iff_Suc_zadd, int_le_less]));
-qed "zle_iff_zadd";
-
-Goal "abs (int m) = int m";
-by (simp_tac (simpset() addsimps [zabs_def]) 1); 
-qed "abs_int_eq";
-Addsimps [abs_int_eq];
-
-
-(**** nat: magnitide of an integer, as a natural number ****)
-
-Goalw [nat_def] "nat(int n) = n";
-by Auto_tac;
-qed "nat_int";
-Addsimps [nat_int];
-
-Goalw [nat_def] "nat(- (int n)) = 0";
-by (auto_tac (claset(),
-     simpset() addsimps [neg_eq_less_0, zero_reorient, zminus_zless])); 
-qed "nat_zminus_int";
-Addsimps [nat_zminus_int];
-
-Goalw [Zero_int_def] "nat 0 = 0";
-by (rtac nat_int 1);
-qed "nat_zero";
-Addsimps [nat_zero];
-
-Goal "~ neg z ==> int (nat z) = z"; 
-by (dtac (not_neg_eq_ge_0 RS iffD1) 1); 
-by (dtac zle_imp_zless_or_eq 1); 
-by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
-qed "not_neg_nat"; 
-
-Goal "neg x ==> EX n. x = - (int (Suc n))"; 
-by (auto_tac (claset(), 
-	      simpset() addsimps [neg_eq_less_0, zless_iff_Suc_zadd,
-				  zdiff_eq_eq RS sym, zdiff_def])); 
-qed "negD"; 
-
-Goalw [nat_def] "neg z ==> nat z = 0"; 
-by Auto_tac; 
-qed "neg_nat"; 
-
-Goal "(m < nat z) = (int m < z)";
-by (case_tac "neg z" 1);
-by (etac (not_neg_nat RS subst) 2);
-by (auto_tac (claset(), simpset() addsimps [neg_nat])); 
-by (auto_tac (claset() addDs [order_less_trans], 
-	      simpset() addsimps [neg_eq_less_0])); 
-qed "zless_nat_eq_int_zless";
-
-Goal "0 <= z ==> int (nat z) = z"; 
-by (asm_full_simp_tac
-    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
-qed "nat_0_le"; 
-
-Goal "z <= 0 ==> nat z = 0"; 
-by (auto_tac (claset(), 
-	      simpset() addsimps [order_le_less, neg_eq_less_0, 
-				  zle_def, neg_nat])); 
-qed "nat_le_0"; 
-Addsimps [nat_0_le, nat_le_0];
-
-(*An alternative condition is  0 <= w  *)
-Goal "0 < z ==> (nat w < nat z) = (w < z)";
-by (stac (zless_int RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_0, 
-				      order_le_less]) 1);
-by (case_tac "neg w" 1);
-by (asm_simp_tac (simpset() addsimps [not_neg_nat]) 2);
-by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_0, neg_nat]) 1);
-by (blast_tac (claset() addIs [order_less_trans]) 1);
-val lemma = result();
-
-Goal "(nat w < nat z) = (0 < z & w < z)";
-by (case_tac "0 < z" 1);
-by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less])); 
-qed "zless_nat_conj";
-
-(* a case theorem distinguishing non-negative and negative int *)  
-
-val prems = Goal
-     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"; 
-by (case_tac "neg z" 1); 
-by (fast_tac (claset() addSDs [negD] addSEs prems) 1); 
-by (dtac (not_neg_nat RS sym) 1);
-by (eresolve_tac prems 1);
-qed "int_cases"; 
-
-fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
-
-
-(*** Monotonicity of Multiplication ***)
-
-Goal "i <= (j::int) ==> i * int k <= j * int k";
-by (induct_tac "k" 1);
-by (stac int_Suc 2);
-by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono, 
-                                       int_Suc0_eq_1])));
-val lemma = result();
-
-Goal "[| i <= j;  (0::int) <= k |] ==> i*k <= j*k";
-by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1);
-by (etac lemma 2);
-by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_0]) 1);
-qed "zmult_zle_mono1";
-
-Goal "[| i <= j;  k <= (0::int) |] ==> j*k <= i*k";
-by (rtac (zminus_zle_zminus RS iffD1) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym,
-				      zmult_zle_mono1, zle_zminus]) 1);
-qed "zmult_zle_mono1_neg";
-
-Goal "[| i <= j;  (0::int) <= k |] ==> k*i <= k*j";
-by (dtac zmult_zle_mono1 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
-qed "zmult_zle_mono2";
-
-Goal "[| i <= j;  k <= (0::int) |] ==> k*j <= k*i";
-by (dtac zmult_zle_mono1_neg 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
-qed "zmult_zle_mono2_neg";
-
-(* <= monotonicity, BOTH arguments*)
-Goal "[| i <= j;  k <= l;  (0::int) <= j;  (0::int) <= k |] ==> i*k <= j*l";
-by (etac (zmult_zle_mono1 RS order_trans) 1);
-by (assume_tac 1);
-by (etac zmult_zle_mono2 1);
-by (assume_tac 1);
-qed "zmult_zle_mono";
-
-
-(** strict, in 1st argument; proof is by induction on k>0 **)
-
-Goal "i<j ==> 0<k --> int k * i < int k * j";
-by (induct_tac "k" 1);
-by (stac int_Suc 2);
-by (case_tac "n=0" 2);
-by (ALLGOALS (asm_full_simp_tac
-	      (simpset() addsimps [zadd_zmult_distrib, zadd_zless_mono, 
-				   int_Suc0_eq_1, order_le_less])));
-val lemma = result();
-
-Goal "[| i<j;  (0::int) < k |] ==> k*i < k*j";
-by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1);
-by (etac (lemma RS mp) 2);
-by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_0, 
-				      order_le_less]) 1);
-by (forward_tac [conjI RS (zless_nat_conj RS iffD2)] 1);
-by Auto_tac;
-qed "zmult_zless_mono2";
-
-Goal "[| i<j;  (0::int) < k |] ==> i*k < j*k";
-by (dtac zmult_zless_mono2 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
-qed "zmult_zless_mono1";
-
-(* < monotonicity, BOTH arguments*)
-Goal "[| i < j;  k < l;  (0::int) < j;  (0::int) < k |] ==> i*k < j*l";
-by (etac (zmult_zless_mono1 RS order_less_trans) 1);
-by (assume_tac 1);
-by (etac zmult_zless_mono2 1);
-by (assume_tac 1);
-qed "zmult_zless_mono";
-
-Goal "[| i<j;  k < (0::int) |] ==> j*k < i*k";
-by (rtac (zminus_zless_zminus RS iffD1) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym,
-				      zmult_zless_mono1, zless_zminus]) 1);
-qed "zmult_zless_mono1_neg";
-
-Goal "[| i<j;  k < (0::int) |] ==> k*j < k*i";
-by (rtac (zminus_zless_zminus RS iffD1) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_zminus RS sym,
-				      zmult_zless_mono2, zless_zminus]) 1);
-qed "zmult_zless_mono2_neg";
-
-
-Goal "(m*n = (0::int)) = (m = 0 | n = 0)";
-by (case_tac "m < (0::int)" 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [linorder_not_less, order_le_less, 
-				  linorder_neq_iff])); 
-by (REPEAT 
-    (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], 
-		simpset()) 1));
-qed "zmult_eq_0_iff";
-AddIffs [zmult_eq_0_iff];
-
-
-(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
-    but not (yet?) for k*m < n*k. **)
-
-Goal "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))";
-by (case_tac "k = (0::int)" 1);
-by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, 
-                              zmult_zless_mono1, zmult_zless_mono1_neg]));  
-by (auto_tac (claset(), 
-              simpset() addsimps [linorder_not_less,
-				  inst "y1" "m*k" (linorder_not_le RS sym),
-                                  inst "y1" "m" (linorder_not_le RS sym)]));
-by (ALLGOALS (etac notE));
-by (auto_tac (claset(), simpset() addsimps [order_less_imp_le, zmult_zle_mono1,
-                                            zmult_zle_mono1_neg]));  
-qed "zmult_zless_cancel2";
-
-
-Goal "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
-                                  zmult_zless_cancel2]) 1);
-qed "zmult_zless_cancel1";
-
-Goal "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
-                                  zmult_zless_cancel2]) 1);
-qed "zmult_zle_cancel2";
-
-Goal "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
-                                  zmult_zless_cancel1]) 1);
-qed "zmult_zle_cancel1";
-
-Goal "(m*k = n*k) = (k = (0::int) | m=n)";
-by (cut_facts_tac [linorder_less_linear] 1);
-by Safe_tac;
-by Auto_tac;  
-by (REPEAT 
-    (force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg)
-                         addD2 ("mono_pos", zmult_zless_mono1), 
-		simpset() addsimps [linorder_neq_iff]) 1));
-
-qed "zmult_cancel2";
-
-Goal "(k*m = k*n) = (k = (0::int) | m=n)";
-by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
-                                  zmult_cancel2]) 1);
-qed "zmult_cancel1";
-Addsimps [zmult_cancel1, zmult_cancel2];
-
-
-(*Analogous to zadd_int*)
-Goal "n<=m --> int m - int n = int (m-n)";
-by (induct_thm_tac diff_induct "m n" 1);
-by (auto_tac (claset(), simpset() addsimps [int_Suc, symmetric zdiff_def])); 
-qed_spec_mp "zdiff_int";
diff -r a431e0aa34c9 -r 3d0c6238162a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Nov 20 10:41:39 2003 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 20 10:42:00 2003 +0100
@@ -86,8 +86,7 @@
   Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
   HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
-  Integ/Equiv.thy Integ/Int_lemmas.ML Integ/Int.thy \
-  Integ/IntArith.thy Integ/IntDef.thy \
+  Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
   Integ/IntDiv.thy Integ/IntPower.thy \
   Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
   Integ/NatSimprocs.thy Integ/int_arith1.ML \