author paulson Thu, 08 Jul 1999 13:43:42 +0200 changeset 6917 eba301caceea parent 6916 4957978b6f9e child 6918 63c9df6b5c4b
Introduction of integer division algorithm Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
 src/HOL/Integ/Bin.ML file | annotate | diff | comparison | revisions src/HOL/Integ/Int.ML file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.ML file | annotate | diff | comparison | revisions src/HOL/Integ/IntDiv.ML file | annotate | diff | comparison | revisions src/HOL/Integ/IntDiv.thy file | annotate | diff | comparison | revisions src/HOL/Integ/simproc.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/Bin.ML	Thu Jul 08 13:42:31 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Thu Jul 08 13:43:42 1999 +0200
@@ -200,12 +200,22 @@

-(** Distributive laws for constants only **)
+
+(** Special simplification, for constants only **)

+fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)];
+
+(*Distributive laws*)
+Addsimps (map (inst "w" "number_of ?v")
zdiff_zmult_distrib, zdiff_zmult_distrib2]);

+Addsimps (map (inst "x" "number_of ?v")
+	  [zless_zminus, zle_zminus, equation_zminus]);
+Addsimps (map (inst "y" "number_of ?v")
+	  [zminus_zless, zminus_zle, zminus_equation]);
+
+
(** Special-case simplification for small constants **)

Goal "#0 * z = (#0::int)";
@@ -224,7 +234,19 @@
by (Simp_tac 1);
qed "zmult_1_right";

-(*For specialist use*)
+Goal "#-1 * z = -(z::int)";
+by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
+qed "zmult_minus1";
+
+Goal "z * #-1 = -(z::int)";
+by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
+qed "zmult_minus1_right";
+
+	  zmult_1, zmult_1_right,
+	  zmult_minus1, zmult_minus1_right];
+
+(*For specialist use: NOT as default simprules*)
Goal "#2 * z = (z+z::int)";
qed "zmult_2";
@@ -233,8 +255,8 @@
qed "zmult_2_right";

-	  zmult_1, zmult_1_right];
+
+(** Inequality reasoning **)

Goal "(w < z + (#1::int)) = (w<z | w=z)";
@@ -246,11 +268,11 @@

Goal "neg x = (x < #0)";
-by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1);
+by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1);
qed "neg_eq_less_0";

Goal "(~neg x) = (int 0 <= x)";
-by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1);
+by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1);
qed "not_neg_eq_ge_0";

Goal "#0 <= int m";
@@ -259,6 +281,29 @@

+(** Products of signs  **)
+
+Goal "[| (m::int) < #0;  n < #0 |] ==> #0 < m*n";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "neg_times_neg_is_pos";
+
+Goal "[| (m::int) < #0;  #0 < n |] ==> m*n < #0";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac;
+qed "neg_times_pos_is_neg";
+
+Goal "[| #0 < (m::int);  n < #0 |] ==> m*n < #0";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "pos_times_neg_is_neg";
+
+Goal "[| #0 < (m::int);  #0 < n |] ==> #0 < m*n";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac;
+qed "pos_times_pos_is_pos";
+
+
(** Needed because (int 0) rewrites to #0.
Can these be generalized without evaluating large numbers?**)

@@ -339,7 +384,7 @@
by (Asm_simp_tac 1);
by (int_case_tac "number_of w" 1);
by (ALLGOALS (asm_simp_tac
symmetric zdiff_def] @ zcompare_rls)));
qed "neg_number_of_BIT";

@@ -671,5 +716,7 @@
qed "nat_less_eq_zless";

+(*Towards canonical simplification*)
```--- a/src/HOL/Integ/Int.ML	Thu Jul 08 13:42:31 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Thu Jul 08 13:43:42 1999 +0200
@@ -125,6 +125,14 @@
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";
+
Goal "- (int (Suc n)) < int 0";
by (simp_tac (simpset() addsimps [zless_def]) 1);
qed "negative_zless_0";
@@ -180,11 +188,11 @@

Goalw [zdiff_def,zless_def] "neg x = (x < int 0)";
by Auto_tac;
-qed "neg_eq_less_nat0";
+qed "neg_eq_less_int0";

Goalw [zle_def] "(~neg x) = (int 0 <= x)";
-by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1);
-qed "not_neg_eq_ge_nat0";
+by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1);
+qed "not_neg_eq_ge_int0";

(**** nat: magnitide of an integer, as a natural number ****)
@@ -195,20 +203,20 @@

Goalw [nat_def] "nat(- int n) = 0";
by (auto_tac (claset(),
qed "nat_zminus_nat";

Goal "~ neg z ==> int (nat z) = z";
-by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1);
+by (dtac (not_neg_eq_ge_int0 RS iffD1) 1);
by (dtac zle_imp_zless_or_eq 1);
qed "not_neg_nat";

Goal "neg x ==> ? n. x = - (int (Suc n))";
by (auto_tac (claset(),
zdiff_eq_eq RS sym, zdiff_def]));
qed "negD";

@@ -219,13 +227,26 @@
(*An alternative condition is  int 0 <= w  *)
Goal "int 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_nat0,
+by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_int0,
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_nat0, neg_nat]) 1);
+by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_int0, neg_nat]) 1);
by (blast_tac (claset() addIs [order_less_trans]) 1);
-qed "zless_nat";
+val lemma = result();
+
+Goal "z <= int 0 ==> nat z = 0";
+by (auto_tac (claset(),
+				  zle_def, neg_nat]));
+qed "nat_le_0";
+
+Goal "(nat w < nat z) = (int 0 < z & w < z)";
+by (case_tac "int 0 < z" 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [lemma, nat_le_0, linorder_not_less]));
+qed "zless_nat_conj";
+

(* a case theorem distinguishing non-negative and negative int *)

@@ -251,7 +272,7 @@
Goal "[| i <= j;  int 0 <= 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_nat0]) 1);
+by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1);
qed "zmult_zle_mono1";

Goal "[| i <= j;  k <= int 0 |] ==> j*k <= i*k";
@@ -286,9 +307,9 @@
Goal "[| i<j;  int 0 < k |] ==> k*i < k*j";
by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1);
by (etac lemma 2);
order_le_less]) 1);
-by (forward_tac [zless_nat RS iffD2] 1);
+by (forward_tac [conjI RS (zless_nat_conj RS iffD2)] 1);
by Auto_tac;
qed "zmult_zless_mono2";

@@ -310,28 +331,6 @@
qed "zmult_zless_mono2_neg";

-(** Products of signs.  Useful?  **)
-
-Goal "[| m < int 0;  n < int 0 |] ==> int 0 < m*n";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "neg_times_neg_is_pos";
-
-Goal "[| m < int 0;  int 0 < n |] ==> m*n < int 0";
-by (dtac zmult_zless_mono1 1);
-by Auto_tac;
-qed "neg_times_pos_is_neg";
-
-Goal "[| int 0 < m;  n < int 0 |] ==> m*n < int 0";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "pos_times_neg_is_neg";
-
-Goal "[| int 0 < m;  int 0 < n |] ==> int 0 < m*n";
-by (dtac zmult_zless_mono1 1);
-by Auto_tac;
-qed "pos_times_pos_is_pos";
-
Goal "(m*n = int 0) = (m = int 0 | n = int 0)";
by (case_tac "m < int 0" 1);
by (auto_tac (claset(), ```
```--- a/src/HOL/Integ/IntDef.ML	Thu Jul 08 13:42:31 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Thu Jul 08 13:43:42 1999 +0200
@@ -139,9 +139,9 @@

Goalw [int_def] "- (int 0) = int 0";
by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_nat0";
+qed "zminus_int0";

(**** neg: the test for negative integers ****)
@@ -225,12 +225,12 @@
Goalw [int_def] "int 0 + z = z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);

Goal "z + int 0 = z";
by (rtac (zadd_commute RS trans) 1);

Goalw [int_def] "z + (- z) = int 0";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
@@ -242,7 +242,7 @@

Goal "z + (- z + w) = (w::int)";
@@ -257,17 +257,17 @@

Goal "int 0 - x = -x";
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_nat0";
+qed "zdiff_int0";

Goal "x - int 0 = x";
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_nat0_right";
+qed "zdiff_int0_right";

Goal "x - x = int 0";
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
qed "zdiff_self";

(** Lemmas **)
@@ -326,13 +326,6 @@
qed "zmult_zminus";

-
-Goal "(- z) * (- w) = (z * (w::int))";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-qed "zmult_zminus_zminus";
-
Goal "(z::int) * w = w * z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -388,29 +381,22 @@
Goalw [int_def] "int 0 * z = int 0";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_nat0";
+qed "zmult_int0";

Goalw [int_def] "int 1 * z = z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_nat1";
+qed "zmult_int1";

Goal "z * int 0 = int 0";
-by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1);
-qed "zmult_nat0_right";
+by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
+qed "zmult_int0_right";

Goal "z * int 1 = z";
-by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1);
-qed "zmult_nat1_right";
-
-
+by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
+qed "zmult_int1_right";

-Goal "(- z = w) = (z = - (w::int))";
-by Safe_tac;
-by (rtac (zminus_zminus RS sym) 1);
-by (rtac zminus_zminus 1);
-qed "zminus_exchange";

(* Theorems about less and less_equal *)```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntDiv.ML	Thu Jul 08 13:43:42 1999 +0200
@@ -0,0 +1,351 @@
+(*  Title:      HOL/IntDiv.ML
+    ID:         \$Id\$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+The division operators div, mod and the divides relation "dvd"
+*)
+
+
+(*** Uniqueness and monotonicity of quotients and remainders ***)
+
+Goal "[| r' + b*q' <= r + b*q;  #0 <= r';  #0 < b;  r < b |] \
+\     ==> q' <= (q::int)";
+by (subgoal_tac "r' + b * (q'-q) <= r" 1);
+by (simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2]) 2);
+by (subgoal_tac "#0 < b * (#1 + q - q')" 1);
+by (etac order_le_less_trans 2);
+by (subgoal_tac "b * q' < b * (#1 + q)" 1);
+by (Asm_full_simp_tac 1);
+qed "unique_quotient_lemma";
+
+Goal "[| r' + b*q' <= r + b*q;  r <= #0;  b < #0;  b < r' |] \
+\     ==> q <= (q'::int)";
+by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")]
+    unique_quotient_lemma 1);
+by (auto_tac (claset(),
+qed "unique_quotient_lemma_neg";
+
+
+Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
+\     ==> q = q'";
+by (asm_full_simp_tac
+    (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
+by Safe_tac;
+by (ALLGOALS Asm_full_simp_tac);
+by (REPEAT
+				order_eq_refl RS unique_quotient_lemma_neg,
+				sym]) 1));
+qed "unique_quotient";
+
+
+Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
+\     ==> r = r'";
+by (subgoal_tac "q = q'" 1);
+by (blast_tac (claset() addIs [unique_quotient]) 2);
+by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
+qed "unique_remainder";
+
+
+(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
+
+Goal "adjust a b (q,r) = (if #0 <= r-b then (#2*q + #1, r-b)  \
+\                         else (#2*q, r))";
+
+(*Proving posDivAlg's termination condition*)
+val [tc] = posDivAlg.tcs;
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
+val lemma = result();
+
+(* removing the termination condition from the generated theorems *)
+
+bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.rules);
+
+(**use with simproc to avoid re-proving the premise*)
+Goal "#0 < b ==> \
+\     posDivAlg (a,b) =      \
+\      (if a<b then (#0,a) else adjust a b (posDivAlg(a, #2*b)))";
+by (rtac (posDivAlg_raw_eqn RS trans) 1);
+by (Asm_simp_tac 1);
+qed "posDivAlg_eqn";
+
+val posDivAlg_induct = lemma RS posDivAlg.induct;
+
+
+(*Correctness of posDivAlg: it computes quotients correctly*)
+Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
+by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
+by Auto_tac;
+by (ALLGOALS
+					    pos_times_pos_is_pos])));
+(*base case: a<b*)
+by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
+(*main argument*)
+by (stac posDivAlg_eqn 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac splitE 1);
+by Auto_tac;
+(*the "just double" case*)
+by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
+qed_spec_mp "posDivAlg_correct";
+
+
+(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
+
+(*Proving negDivAlg's termination condition*)
+val [tc] = negDivAlg.tcs;
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
+val lemma = result();
+
+(* removing the termination condition from the generated theorems *)
+
+bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.rules);
+
+(**use with simproc to avoid re-proving the premise*)
+Goal "#0 < b ==> \
+\     negDivAlg (a,b) =      \
+\      (if #0<=a+b then (#-1,a+b) else adjust a b (negDivAlg(a, #2*b)))";
+by (rtac (negDivAlg_raw_eqn RS trans) 1);
+by (Asm_simp_tac 1);
+qed "negDivAlg_eqn";
+
+val negDivAlg_induct = lemma RS negDivAlg.induct;
+
+
+(*Correctness of negDivAlg: it computes quotients correctly
+  It doesn't work if a=0 because the 0/b=0 rather than -1*)
+Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
+by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
+by Auto_tac;
+by (ALLGOALS
+					    pos_times_pos_is_pos])));
+(*base case: 0<=a+b*)
+by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
+(*main argument*)
+by (stac negDivAlg_eqn 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac splitE 1);
+by Auto_tac;
+(*the "just double" case*)
+by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
+qed_spec_mp "negDivAlg_correct";
+
+
+(*** Existence shown by proving the division algorithm to be correct ***)
+
+(*the case a=0*)
+Goal "b ~= #0 ==> quorem ((#0,b), (#0,#0))";
+by (auto_tac (claset(),
+qed "quorem_0";
+
+Goal "posDivAlg (#0, b) = (#0, #0)";
+by (stac posDivAlg_raw_eqn 1);
+by Auto_tac;
+qed "posDivAlg_0";
+
+Goal "negDivAlg (#-1, b) = (#-1, b-#1)";
+by (stac negDivAlg_raw_eqn 1);
+by Auto_tac;
+qed "negDivAlg_minus1";
+
+Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)";
+by Auto_tac;
+qed "negateSnd_eq";
+
+Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
+by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
+qed "quorem_neg";
+
+Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))";
+by (auto_tac (claset(),
+by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
+			       negDivAlg_correct]));
+by (auto_tac (claset(),
+qed "divAlg_correct";
+
+Goal "b ~= (#0::int) ==> a = b * (a div b) + (a mod b)";
+by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [quorem_def, div_def, mod_def]));
+qed "zmod_zdiv_equality";
+   (*the name mod_div_equality would hide the other one proved in Divides.ML
+     existing users aren't using name spaces for theorems*)
+
+Goal "(#0::int) < b ==> #0 <= a mod b & a mod b < b";
+by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
+by (auto_tac (claset(),
+bind_thm ("pos_mod_sign", result() RS conjunct1);
+bind_thm ("pos_mod_bound", result() RS conjunct2);
+
+Goal "b < (#0::int) ==> a mod b <= #0 & b < a mod b";
+by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [quorem_def, div_def, mod_def]));
+bind_thm ("neg_mod_sign", result() RS conjunct1);
+bind_thm ("neg_mod_bound", result() RS conjunct2);
+
+
+(*** Computation of division and remainder ***)
+
+Goal "(#0::int) div b = #0";
+by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
+qed "div_zero";
+
+Goal "(#0::int) mod b = #0";
+by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
+qed "mod_zero";
+
+
+(** a positive, b positive **)
+
+Goal "[| #0 < a;  #0 < b |] ==> a div b = fst (posDivAlg(a,b))";
+by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
+qed "div_pos_pos";
+
+Goal "[| #0 < a;  #0 < b |] ==> a mod b = snd (posDivAlg(a,b))";
+by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
+qed "mod_pos_pos";
+
+(** a negative, b positive **)
+
+Goal "[| a < #0;  #0 < b |] ==> a div b = fst (negDivAlg(a,b))";
+by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
+qed "div_neg_pos";
+
+Goal "[| a < #0;  #0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
+by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
+qed "mod_neg_pos";
+
+(** a positive, b negative **)
+
+Goal "[| #0 < a;  b < #0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
+by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
+qed "div_pos_neg";
+
+Goal "[| #0 < a;  b < #0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
+by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
+qed "mod_pos_neg";
+
+(** a negative, b negative **)
+
+Goal "[| a < #0;  b < #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
+by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
+qed "div_neg_neg";
+
+Goal "[| a < #0;  b < #0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
+by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
+qed "mod_neg_neg";
+
+	       [("a", "number_of ?v"), ("b", "number_of ?w")])
+	  [div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
+	   mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
+	   posDivAlg_eqn, negDivAlg_eqn]);
+
+
+(** Special-case simplification **)
+
+Goal "a mod (#1::int) = #0";
+by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1);
+by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2);
+by Auto_tac;
+qed "zmod_1";
+
+Goal "a div (#1::int) = a";
+by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1);
+by Auto_tac;
+qed "zdiv_1";
+
+Goal "a mod (#-1::int) = #0";
+by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1);
+by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2);
+by Auto_tac;
+qed "zmod_minus1";
+
+Goal "a div (#-1::int) = -a";
+by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1);
+by Auto_tac;
+qed "zdiv_minus1";
+
+
+(** Monotonicity results **)
+
+
+Goal "[| a <= a';  #0 < (b::int) |] ==> a div b <= a' div b";
+by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
+by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
+by Auto_tac;
+by (rtac unique_quotient_lemma 1);
+by (etac subst 1);
+by (etac subst 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
+qed "zdiv_mono1";
+
+Goal "[| a <= a';  (b::int) < #0 |] ==> a' div b <= a div b";
+by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
+by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
+by Auto_tac;
+by (rtac unique_quotient_lemma_neg 1);
+by (etac subst 1);
+by (etac subst 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound])));
+qed "zdiv_mono1_neg";
+
+
+
+(** The division algorithm in ML **)
+
+fun posDivAlg (a,b) =
+  if a<b then (0,a)
+  else let val (q,r) = posDivAlg(a, 2*b)
+           in  if 0<=r-b then (2*q+1, r-b)
+               else (2*q, r)
+       end;
+
+fun negDivAlg (a,b) =
+  if 0<=a+b then (~1,a+b)
+  else let val (q,r) = negDivAlg(a, 2*b)
+           in  if 0<=r-b then (2*q+1, r-b)
+               else (2*q, r)
+       end;
+
+fun negateSnd (q,r:int) = (q,~r);
+
+fun divAlg (a,b) = if 0<=a then
+                      if b>0 then posDivAlg (a,b)
+                       else if a=0 then (0,0)
+                            else negateSnd (negDivAlg (~a,~b))
+                   else
+                      if 0<b then negDivAlg (a,b)
+                      else        negateSnd (posDivAlg (~a,~b));```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntDiv.thy	Thu Jul 08 13:43:42 1999 +0200
@@ -0,0 +1,63 @@
+(*  Title:      HOL/IntDiv.thy
+    ID:         \$Id\$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+The division operators div, mod and the divides relation "dvd"
+*)
+
+IntDiv = Bin + Recdef +
+
+constdefs
+  quorem :: "(int*int) * (int*int) => bool"
+    "quorem == %((a,b), (q,r)).
+                      a = b*q + r &
+                      (if #0<b then #0<=r & r<b else b<r & r <= #0)"
+
+  adjust :: "[int, int, int*int] => int*int"
+    "adjust a b == %(q,r). if #0 <= r-b then (#2*q + #1, r-b)
+                           else (#2*q, r)"
+
+(** the division algorithm **)
+
+(*for the case a>=0, b>0*)
+consts posDivAlg :: "int*int => int*int"
+recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + #1))"
+    "posDivAlg (a,b) =
+       (if (a<b | b<=#0) then (#0,a)
+        else adjust a b (posDivAlg(a, #2*b)))"
+
+(*for the case a<0, b>0*)
+consts negDivAlg :: "int*int => int*int"
+recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
+    "negDivAlg (a,b) =
+       (if (#0<=a+b | b<=#0) then (#-1,a+b)
+        else adjust a b (negDivAlg(a, #2*b)))"
+
+(*for the general case b~=0*)
+
+constdefs
+  negateSnd :: "int*int => int*int"
+    "negateSnd == %(q,r). (q,-r)"
+
+  (*The full division algorithm considers all possible signs for a, b
+    including the special case a=0, b<0, because negDivAlg requires a<0*)
+  divAlg :: "int*int => int*int"
+    "divAlg ==
+       %(a,b). if #0<=a then
+                  if #0<b then posDivAlg (a,b)
+                  else if a=#0 then (#0,#0)
+                       else negateSnd (negDivAlg (-a,-b))
+               else
+                  if #0<b then negDivAlg (a,b)
+                  else         negateSnd (posDivAlg (-a,-b))"
+
+instance
+  int :: {div}
+
+defs
+  div_def   "a div b == fst (divAlg (a,b))"
+  mod_def   "a mod b == snd (divAlg (a,b))"
+
+
+end```
```--- a/src/HOL/Integ/simproc.ML	Thu Jul 08 13:42:31 1999 +0200
+++ b/src/HOL/Integ/simproc.ML	Thu Jul 08 13:43:42 1999 +0200
@@ -20,7 +20,7 @@
"((x::int) + (y + z) = y) = (x = -z)"
(fn _ => [stac zadd_left_commute 1,
-	    res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1,
+	    res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1,
simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);

@@ -39,8 +39,8 @@