diff -r 500038b6063b -r 8113992d3f45 src/HOL/Integ/IntDiv.ML --- a/src/HOL/Integ/IntDiv.ML Tue Jul 13 10:44:45 1999 +0200 +++ b/src/HOL/Integ/IntDiv.ML Tue Jul 13 10:45:09 1999 +0200 @@ -4,6 +4,30 @@ Copyright 1999 University of Cambridge The division operators div, mod and the divides relation "dvd" + +Here is 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 a = b * (a div b) + (a mod b)"; +(** Aribtrary definitions for division by zero. Useful to simplify + certain equations **) + +Goal "a div (#0::int) = #0"; +by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1); +qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*) + +Goal "a mod (#0::int) = a"; +by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1); +qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*) + +fun undefined_case_tac s i = + case_tac s i THEN + asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, + DIVISION_BY_ZERO_MOD]) i; + +(** Basic laws about division and remainder **) + +Goal "(a::int) = b * (a div b) + (a mod b)"; +by (undefined_case_tac "b = #0" 1); 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); @@ -217,6 +258,112 @@ bind_thm ("neg_mod_bound", result() RS conjunct2); +(** proving general properties of div and mod **) + +Goal "b ~= #0 ==> quorem ((a, b), (a div b, a mod b))"; +by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); +by (auto_tac + (claset(), + simpset() addsimps [quorem_def, linorder_neq_iff, + pos_mod_sign,pos_mod_bound, + neg_mod_sign, neg_mod_bound])); +qed "quorem_div_mod"; + +Goal "[| quorem((a,b),(q,r)); b ~= #0 |] ==> a div b = q"; +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); +qed "quorem_div"; + +Goal "[| quorem((a,b),(q,r)); b ~= #0 |] ==> a mod b = r"; +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); +qed "quorem_mod"; + +Goal "[| (#0::int) <= a; a < b |] ==> a div b = #0"; +by (rtac quorem_div 1); +by (auto_tac (claset(), simpset() addsimps [quorem_def])); +qed "pos_div_trivial"; + +Goal "[| a <= (#0::int); b < a |] ==> a div b = #0"; +by (rtac quorem_div 1); +by (auto_tac (claset(), simpset() addsimps [quorem_def])); +qed "neg_div_trivial"; + +Goal "[| (#0::int) <= a; a < b |] ==> a mod b = a"; +by (rtac quorem_mod 1); +by (auto_tac (claset(), simpset() addsimps [quorem_def])); +by (rtac zmult_0_right 1); +qed "pos_mod_trivial"; + +Goal "[| a <= (#0::int); b < a |] ==> a mod b = a"; +by (rtac quorem_mod 1); +by (auto_tac (claset(), simpset() addsimps [quorem_def])); +by (rtac zmult_0_right 1); +qed "neg_mod_trivial"; + + +(*Simpler laws such as -a div b = -(a div b) FAIL*) +Goal "(-a) div (-b) = a div (b::int)"; +by (undefined_case_tac "b = #0" 1); +by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) + RS quorem_div) 1); +by Auto_tac; +qed "zdiv_zminus_zminus"; +Addsimps [zdiv_zminus_zminus]; + +(*Simpler laws such as -a mod b = -(a mod b) FAIL*) +Goal "(-a) mod (-b) = - (a mod (b::int))"; +by (undefined_case_tac "b = #0" 1); +by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) + RS quorem_mod) 1); +by Auto_tac; +qed "zmod_zminus_zminus"; +Addsimps [zmod_zminus_zminus]; + + +(*** division of a number by itself ***) + +Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q"; +by (subgoal_tac "#0 < a*q" 1); +by (arith_tac 2); +by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 1); +val lemma1 = result(); + +Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1"; +by (subgoal_tac "#0 <= a*(#1-q)" 1); +by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); +by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_nonneg_iff]) 1); +by (full_simp_tac (simpset() addsimps zcompare_rls) 1); +val lemma2 = result(); + +Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> q = #1"; +by (asm_full_simp_tac + (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1); +by (rtac order_antisym 1); +by Safe_tac; +by Auto_tac; +by (res_inst_tac [("a", "-a"),("r", "-r")] lemma1 3); +by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1); +by (auto_tac (claset() addIs [lemma1,lemma2], simpset())); +qed "self_quotient"; + +Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> r = #0"; +by (forward_tac [self_quotient] 1); +by (assume_tac 1); +by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); +qed "self_remainder"; + +Goal "a ~= #0 ==> a div a = (#1::int)"; +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); +qed "zdiv_self"; +Addsimps [zdiv_self]; + +(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) +Goal "a mod a = (#0::int)"; +by (undefined_case_tac "a = #0" 1); +by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); +qed "zmod_self"; +Addsimps [zmod_self]; + + (*** Computation of division and remainder ***) Goal "(#0::int) div b = #0"; @@ -231,11 +378,11 @@ (** a positive, b positive **) -Goal "[| #0 < a; #0 < b |] ==> a div b = fst (posDivAlg(a,b))"; +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))"; +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"; @@ -261,11 +408,11 @@ (** a negative, b negative **) -Goal "[| a < #0; b < #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; +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)))"; +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"; @@ -274,7 +421,7 @@ [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 **) @@ -309,7 +456,7 @@ 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 (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); by Auto_tac; by (rtac unique_quotient_lemma 1); by (etac subst 1); @@ -319,7 +466,7 @@ 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 (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); by Auto_tac; by (rtac unique_quotient_lemma_neg 1); by (etac subst 1); @@ -328,7 +475,6 @@ qed "zdiv_mono1_neg"; - (*** Monotonicity in the second argument (dividend) ***) Goal "[| r + b*q = r' + b'*q'; #0 <= r' + b'*q'; \ @@ -356,7 +502,7 @@ by (subgoal_tac "b ~= #0" 1); by (arith_tac 2); 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 (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); by Auto_tac; by (rtac zdiv_mono2_lemma 1); by (etac subst 1); @@ -383,10 +529,8 @@ Goal "[| a < (#0::int); #0 < b'; b' <= b |] \ \ ==> a div b' <= a div b"; -by (subgoal_tac "b ~= #0" 1); -by (arith_tac 2); 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 (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); by Auto_tac; by (rtac zdiv_mono2_neg_lemma 1); by (etac subst 1); @@ -395,29 +539,257 @@ qed "zdiv_mono2_neg"; +(*** More algebraic laws for div and mod ***) -(** The division algorithm in ML **) +(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) + +Goal "[| quorem((b,c),(q,r)); c ~= #0 |] \ +\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; +by (auto_tac + (claset(), + simpset() addsimps split_ifs@ + [quorem_def, linorder_neq_iff, + zadd_zmult_distrib2, + pos_mod_sign,pos_mod_bound, + neg_mod_sign, neg_mod_bound])); +by (rtac (zmod_zdiv_equality RS trans) 2); +by (rtac (zmod_zdiv_equality RS trans) 1); +by Auto_tac; +val lemma = result(); + +Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"; +by (undefined_case_tac "c = #0" 1); +by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); +qed "zdiv_zmult1_eq"; + +Goal "(a*b) mod c = a*(b mod c) mod (c::int)"; +by (undefined_case_tac "c = #0" 1); +by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); +qed "zmod_zmult1_eq"; + +Goal "b ~= (#0::int) ==> (a*b) div b = a"; +by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); +qed "zdiv_zmult_self1"; + +Goal "b ~= (#0::int) ==> (b*a) div b = a"; +by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); +qed "zdiv_zmult_self2"; + +Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; + +Goal "(a*b) mod b = (#0::int)"; +by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); +qed "zmod_zmult_self1"; + +Goal "(b*a) mod b = (#0::int)"; +by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); +qed "zmod_zmult_self2"; + +Addsimps [zmod_zmult_self1, zmod_zmult_self2]; + + +(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) -fun posDivAlg (a,b) = - if a quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; +by (auto_tac + (claset(), + simpset() addsimps split_ifs@ + [quorem_def, linorder_neq_iff, + zadd_zmult_distrib2, + pos_mod_sign,pos_mod_bound, + neg_mod_sign, neg_mod_bound])); +by (rtac (zmod_zdiv_equality RS trans) 2); +by (rtac (zmod_zdiv_equality RS trans) 1); +by Auto_tac; +val lemma = result(); + +Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"; +by (undefined_case_tac "c = #0" 1); +by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] + MRS lemma RS quorem_div]) 1); +qed "zdiv_zadd1_eq"; + +Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c"; +by (undefined_case_tac "c = #0" 1); +by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] + MRS lemma RS quorem_mod]) 1); +qed "zmod_zadd1_eq"; + + +Goal "(a mod b) div b = (#0::int)"; +by (undefined_case_tac "b = #0" 1); +by (auto_tac (claset(), + simpset() addsimps [linorder_neq_iff, + pos_mod_sign, pos_mod_bound, pos_div_trivial, + neg_mod_sign, neg_mod_bound, neg_div_trivial])); +qed "mod_div_trivial"; +Addsimps [mod_div_trivial]; + +Goal "(a mod b) mod b = a mod (b::int)"; +by (undefined_case_tac "b = #0" 1); +by (auto_tac (claset(), + simpset() addsimps [linorder_neq_iff, + pos_mod_sign, pos_mod_bound, pos_mod_trivial, + neg_mod_sign, neg_mod_bound, neg_mod_trivial])); +qed "mod_mod_trivial"; +Addsimps [mod_mod_trivial]; + + +Goal "a ~= (#0::int) ==> (a+b) div a = b div a + #1"; +by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); +qed "zdiv_zadd_self1"; + +Goal "a ~= (#0::int) ==> (b+a) div a = b div a + #1"; +by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); +qed "zdiv_zadd_self2"; +Addsimps [zdiv_zadd_self1, zdiv_zadd_self2]; + +Goal "(a+b) mod a = b mod (a::int)"; +by (undefined_case_tac "a = #0" 1); +by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); +qed "zmod_zadd_self1"; + +Goal "(b+a) mod a = b mod (a::int)"; +by (undefined_case_tac "a = #0" 1); +by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); +qed "zmod_zadd_self2"; +Addsimps [zmod_zadd_self1, zmod_zadd_self2]; + + +(*** proving a div (b*c) = (a div b) div c ***) + +(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but + 7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems + to cause particular problems.*) + +(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) -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; +Goal "[| (#0::int) < c; b < r; r <= #0 |] ==> b*c < r + b*(q mod c)"; +by (subgoal_tac "b * (c - q mod c) < r * #1" 1); +by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); +by (rtac order_le_less_trans 1); +by (etac zmult_zless_mono1 2); +by (rtac zmult_zle_mono2_neg 1); +by (auto_tac + (claset(), + simpset() addsimps zcompare_rls@[pos_mod_bound])); +val lemma1 = result(); + +Goal "[| (#0::int) < c; b < r; r <= #0 |] ==> r + b * (q mod c) <= #0"; +by (subgoal_tac "b * (q mod c) <= #0" 1); +by (arith_tac 1); +by (asm_simp_tac (simpset() addsimps [neg_imp_zmult_nonpos_iff, + pos_mod_sign]) 1); +val lemma2 = result(); + +Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> #0 <= r + b * (q mod c)"; +by (subgoal_tac "#0 <= b * (q mod c)" 1); +by (arith_tac 1); +by (asm_simp_tac + (simpset() addsimps [pos_imp_zmult_nonneg_iff, pos_mod_sign]) 1); +val lemma3 = result(); + +Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> r + b * (q mod c) < b * c"; +by (subgoal_tac "r * #1 < b * (c - q mod c)" 1); +by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); +by (rtac order_less_le_trans 1); +by (etac zmult_zless_mono1 1); +by (rtac zmult_zle_mono2 2); +by (auto_tac + (claset(), + simpset() addsimps zcompare_rls@[pos_mod_bound])); +val lemma4 = result(); + + +Goal "[| quorem ((a,b), (q,r)); b ~= #0; #0 < c |] \ +\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; +by (auto_tac (*SLOW*) + (claset(), + simpset() addsimps split_ifs@ + [quorem_def, linorder_neq_iff, + pos_imp_zmult_pos_iff, + neg_imp_zmult_pos_iff, + zadd_zmult_distrib2 RS sym, + lemma1, lemma2, lemma3, lemma4])); +by (rtac (zmod_zdiv_equality RS trans) 2); +by (rtac (zmod_zdiv_equality RS trans) 1); +by Auto_tac; +val lemma = result(); + +Goal "(#0::int) < c ==> a div (b*c) = (a div b) div c"; +by (undefined_case_tac "b = #0" 1); +by (force_tac (claset(), + simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, + zmult_eq_0_iff]) 1); +qed "zdiv_zmult2_eq"; -fun negateSnd (q,r:int) = (q,~r); +Goal "[| (#0::int) < c |] \ +\ ==> a mod (b*c) = b*(a div b mod c) + a mod b"; +by (undefined_case_tac "b = #0" 1); +by (force_tac (claset(), + simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, + zmult_eq_0_iff]) 1); +qed "zmod_zmult2_eq"; + + +(*** Cancellation of common factors in "div" ***) + +Goal "[| (#0::int) < b; c ~= #0 |] ==> (c*a) div (c*b) = a div b"; +by (stac zdiv_zmult2_eq 1); +by Auto_tac; +val lemma1 = result(); + +Goal "[| b < (#0::int); c ~= #0 |] ==> (c*a) div (c*b) = a div b"; +by (subgoal_tac "(c * -a) div (c * -b) = -a div -b" 1); +by (rtac lemma1 2); +by (auto_tac (claset(), + simpset() addsimps [zdiv_zminus_zminus])); +val lemma2 = result(); + +Goal "c ~= (#0::int) ==> (c*a) div (c*b) = a div b"; +by (undefined_case_tac "b = #0" 1); +by (auto_tac + (claset(), + simpset() delsimps zmult_ac + addsimps [read_instantiate [("x", "b")] linorder_neq_iff, + lemma1, lemma2])); +qed "zdiv_zmult_zmult1"; -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 (a*c) div (b*c) = a div b"; +by (dtac zdiv_zmult_zmult1 1); +by Auto_tac; +qed "zdiv_zmult_zmult2"; + + + +(*** Distribution of factors over "mod" ***) + +Goal "[| (#0::int) < b; c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; +by (stac zmod_zmult2_eq 1); +by Auto_tac; +val lemma1 = result(); + +Goal "[| b < (#0::int); c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; +by (subgoal_tac "(c * -a) mod (c * -b) = c * (-a mod -b)" 1); +by (rtac lemma1 2); +by (auto_tac (claset(), + simpset() addsimps [zmod_zminus_zminus])); +val lemma2 = result(); + +Goal "c ~= (#0::int) ==> (c*a) mod (c*b) = c * (a mod b)"; +by (undefined_case_tac "b = #0" 1); +by (auto_tac + (claset(), + simpset() delsimps zmult_ac + addsimps [read_instantiate [("x", "b")] linorder_neq_iff, + lemma1, lemma2])); +qed "zmod_zmult_zmult1"; + +Goal "c ~= (#0::int) ==> (a*c) mod (b*c) = (a mod b) * c"; +by (dtac zmod_zmult_zmult1 1); +by Auto_tac; +qed "zmod_zmult_zmult2"; + + +