# HG changeset patch # User paulson # Date 931434222 -7200 # Node ID eba301caceea73f9262d68fd1f298060c03d55ff # Parent 4957978b6f9e00336342ec850f3eae8a8d256a1b Introduction of integer division algorithm Renaming of theorems from _nat0 to _int0 and _nat1 to _int1 diff -r 4957978b6f9e -r eba301caceea src/HOL/Integ/Bin.ML --- 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 #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]; diff -r 4957978b6f9e -r eba301caceea src/HOL/Integ/Int.ML --- 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 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(), diff -r 4957978b6f9e -r eba301caceea src/HOL/Integ/IntDef.ML --- 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 *) diff -r 4957978b6f9e -r eba301caceea src/HOL/Integ/IntDiv.ML --- /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 #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: a0 ***) + +(*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 a0 then posDivAlg (a,b) + else if a=0 then (0,0) + else negateSnd (negDivAlg (~a,~b)) + else + if 0 bool" + "quorem == %((a,b), (q,r)). + a = b*q + r & + (if #0 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 (a0*) +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 [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;