# HG changeset patch
# User paulson
# Date 968315884 -7200
# Node ID d9ea690001ce1c466ef6f78d35fb3557374d1cda
# Parent  3b63a8dd56e3a8e342caf3be4b196e64e62db6af
strengthened dvd_mod & proofed dvd_mod_iff

diff -r 3b63a8dd56e3 -r d9ea690001ce src/HOL/Divides.ML
--- 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);