Introduction of integer division algorithm
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
--- 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 @@
Addsimps [zdiff0, zdiff0_right, zdiff_self];
-(** Distributive laws for constants only **)
+
+(** Special simplification, for constants only **)
-Addsimps (map (read_instantiate_sg (sign_of thy) [("w", "number_of ?v")])
+fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)];
+
+(*Distributive laws*)
+Addsimps (map (inst "w" "number_of ?v")
[zadd_zmult_distrib, zadd_zmult_distrib2,
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";
+
+Addsimps [zmult_0, zmult_0_right,
+ zmult_1, zmult_1_right,
+ zmult_minus1, zmult_minus1_right];
+
+(*For specialist use: NOT as default simprules*)
Goal "#2 * z = (z+z::int)";
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
qed "zmult_2";
@@ -233,8 +255,8 @@
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
qed "zmult_2_right";
-Addsimps [zmult_0, zmult_0_right,
- zmult_1, zmult_1_right];
+
+(** Inequality reasoning **)
Goal "(w < z + (#1::int)) = (w<z | w=z)";
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
@@ -246,11 +268,11 @@
Addsimps [add1_zle_eq];
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 @@
AddIffs [zero_zle_int];
+(** 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
- (simpset() addsimps [zadd_int, neg_eq_less_nat0,
+ (simpset() addsimps [zadd_int, neg_eq_less_int0,
symmetric zdiff_def] @ zcompare_rls)));
qed "neg_number_of_BIT";
@@ -671,5 +716,7 @@
qed "nat_less_eq_zless";
+(*Towards canonical simplification*)
Addsimps zadd_ac;
Addsimps zmult_ac;
+Addsimps [zmult_zminus, zmult_zminus_right];
--- 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(),
- simpset() addsimps [neg_eq_less_nat0, zminus_zless]));
+ simpset() addsimps [neg_eq_less_int0, zminus_zless]));
qed "nat_zminus_nat";
Addsimps [nat_nat, 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);
by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd]));
qed "not_neg_nat";
Goal "neg x ==> ? n. x = - (int (Suc n))";
by (auto_tac (claset(),
- simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
+ simpset() addsimps [neg_eq_less_int0, zless_iff_Suc_zadd,
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(),
+ simpset() addsimps [order_le_less, neg_eq_less_int0,
+ 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);
-by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_nat0,
+by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_int0,
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";
-Addsimps [zminus_nat0];
+Addsimps [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);
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
-qed "zadd_nat0";
+qed "zadd_int0";
Goal "z + int 0 = z";
by (rtac (zadd_commute RS trans) 1);
-by (rtac zadd_nat0 1);
-qed "zadd_nat0_right";
+by (rtac zadd_int0 1);
+qed "zadd_int0_right";
Goalw [int_def] "z + (- z) = int 0";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
@@ -242,7 +242,7 @@
by (rtac zadd_zminus_inverse 1);
qed "zadd_zminus_inverse2";
-Addsimps [zadd_nat0, zadd_nat0_right,
+Addsimps [zadd_int0, zadd_int0_right,
zadd_zminus_inverse, zadd_zminus_inverse2];
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";
-Addsimps [zdiff_nat0, zdiff_nat0_right, zdiff_self];
+Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
(** Lemmas **)
@@ -326,13 +326,6 @@
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
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);
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 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";
-
-Addsimps [zmult_nat0, zmult_nat0_right, zmult_nat1, 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";
+Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right];
(* 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"
+*)
+
+Addsimps [zless_nat_conj];
+
+(*** 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 (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
+ zadd_zmult_distrib2]) 2);
+by (subgoal_tac "b * q' < b * (#1 + q)" 1);
+by (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
+ zadd_zmult_distrib2]) 2);
+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(),
+ simpset() addsimps zcompare_rls@[zmult_zminus_right]));
+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
+ (blast_tac (claset() addIs [order_antisym]
+ addDs [order_eq_refl RS unique_quotient_lemma,
+ 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))";
+by (simp_tac (simpset() addsimps [adjust_def]) 1);
+qed "adjust_eq";
+Addsimps [adjust_eq];
+
+(*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
+ (asm_full_simp_tac (simpset() addsimps [quorem_def,
+ 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 "add one" case*)
+by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
+(*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
+ (asm_full_simp_tac (simpset() addsimps [quorem_def,
+ 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 "add one" case*)
+by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
+(*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(),
+ simpset() addsimps [quorem_def, linorder_neq_iff]));
+qed "quorem_0";
+
+Goal "posDivAlg (#0, b) = (#0, #0)";
+by (stac posDivAlg_raw_eqn 1);
+by Auto_tac;
+qed "posDivAlg_0";
+Addsimps [posDivAlg_0];
+
+Goal "negDivAlg (#-1, b) = (#-1, b-#1)";
+by (stac negDivAlg_raw_eqn 1);
+by Auto_tac;
+qed "negDivAlg_minus1";
+Addsimps [negDivAlg_minus1];
+
+Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)";
+by Auto_tac;
+qed "negateSnd_eq";
+Addsimps [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(),
+ simpset() addsimps [quorem_0, divAlg_def]));
+by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
+ negDivAlg_correct]));
+by (auto_tac (claset(),
+ simpset() addsimps [quorem_def, linorder_neq_iff]));
+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(),
+ simpset() addsimps [quorem_def, mod_def]));
+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";
+
+Addsimps [div_zero, 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";
+
+Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
+ [("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";
+Addsimps [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";
+Addsimps [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";
+Addsimps [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";
+Addsimps [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 @@
val zadd_cancel_end = prove_goal IntDef.thy
"((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,
stac zadd_left_cancel 1,
simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);
@@ -39,8 +39,8 @@
val add_assoc = zadd_assoc
val add_commute = zadd_commute
val add_left_commute = zadd_left_commute
- val add_0 = zadd_nat0
- val add_0_right = zadd_nat0_right
+ val add_0 = zadd_int0
+ val add_0_right = zadd_int0_right
val eq_diff_eq = eq_zdiff_eq
val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI]
@@ -51,7 +51,7 @@
val diff_def = zdiff_def
val minus_add_distrib = zminus_zadd_distrib
val minus_minus = zminus_zminus
- val minus_0 = zminus_nat0
+ val minus_0 = zminus_int0
val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2];
val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel]
end;