# HG changeset patch
# User paulson
# Date 971345723 -7200
# Node ID 325b6279ae4f9806195721b9a01e7388045aa5f5
# Parent  f6dfed43561d9c656445d6d3db239941ca4ca216
new theorems mod_eq_0_iff and mod_eqD; also new SD rule

diff -r f6dfed43561d -r 325b6279ae4f src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Thu Oct 12 11:47:17 2000 +0200
+++ b/src/HOL/Divides.ML	Thu Oct 12 12:15:23 2000 +0200
@@ -472,3 +472,17 @@
 by (stac mult_commute 1);
 by (Asm_simp_tac 1);
 qed "dvd_eq_mod_eq_0";
+
+Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
+by (auto_tac (claset(), 
+     simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));  
+qed "mod_eq_0_iff";
+AddSDs [mod_eq_0_iff RS iffD1];
+
+(*Loses information, namely we also have r<d provided d is nonzero*)
+Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
+by (cut_inst_tac [("m","m")] mod_div_equality 1);
+by (full_simp_tac (simpset() addsimps add_ac) 1); 
+by (blast_tac (claset() addIs [sym]) 1); 
+qed "mod_eqD";
+