--- a/src/HOL/Divides.ML Wed Sep 06 19:12:26 2000 +0200
+++ b/src/HOL/Divides.ML Thu Sep 07 10:38:04 2000 +0200
@@ -421,6 +421,23 @@
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
qed "dvd_mod_imp_dvd";
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd (m mod n)";
+by (div_undefined_case_tac "n=0" 1);
+by (Clarify_tac 1);
+by (Full_simp_tac 1);
+by (rename_tac "j" 1);
+by (res_inst_tac
+ [("x", "(((k div j)*j + k mod j) - ((f*k) div (f*j)) * j)")]
+ exI 1);
+by (asm_simp_tac
+ (simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym,
+ add_mult_distrib2]) 1);
+qed "dvd_mod";
+
+Goal "k dvd n ==> (k::nat) dvd (m mod n) = k dvd m";
+by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1);
+qed "dvd_mod_iff";
+
Goalw [dvd_def] "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
by (etac exE 1);
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);