--- 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 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));
*)
Addsimps [zless_nat_conj];
@@ -194,13 +218,30 @@
simpset() addsimps [quorem_def, linorder_neq_iff]));
qed "divAlg_correct";
-Goal "b ~= (#0::int) ==> 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<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;
+Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= #0 |] \
+\ ==> 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<b then negDivAlg (a,b)
- else negateSnd (posDivAlg (~a,~b));
+Goal "c ~= (#0::int) ==> (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";
+
+
+