# HG changeset patch
# User oheimb
# Date 936634710 -7200
# Node ID e6f74eebfab31426ec2eada1c44e27c9de1ead1a
# Parent  44b333fb5b8049494efef677dae00a890bf7c502
added theorem dvd_reduce

diff -r 44b333fb5b80 -r e6f74eebfab3 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Mon Sep 06 18:18:23 1999 +0200
+++ b/src/HOL/Divides.ML	Mon Sep 06 18:18:30 1999 +0200
@@ -437,6 +437,17 @@
 (* k dvd (m*k) *)
 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
 
+Goal "k dvd (n + k) = k dvd (n::nat)";
+br iffI 1;
+be  dvd_add 2;
+br  dvd_refl 2;
+by (subgoal_tac "n = (n+k)-k" 1);
+by  (Simp_tac 2);
+be ssubst 1;
+be dvd_diff 1;
+br dvd_refl 1;
+qed "dvd_reduce";
+
 Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
 by (Clarify_tac 1);
 by (Full_simp_tac 1);