# HG changeset patch
# User haftmann
# Date 1177587184 -7200
# Node ID eaf5e7ef35d9a4299a8419b3eb39b758ed179a1e
# Parent  ed7d53db217026e3bf5291656fb1893907a84911
added lemmatas

diff -r ed7d53db2170 -r eaf5e7ef35d9 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Apr 26 13:32:59 2007 +0200
+++ b/src/HOL/Divides.thy	Thu Apr 26 13:33:04 2007 +0200
@@ -769,6 +769,20 @@
   apply arith
   done
 
+lemma div_mod_equality':
+  fixes m n :: nat
+  shows "m div n * n = m - m mod n"
+proof -
+  have "m mod n \<le> m mod n" ..
+  from div_mod_equality have 
+    "m div n * n + m mod n - m mod n = m - m mod n" by simp
+  with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have
+    "m div n * n + (m mod n - m mod n) = m - m mod n"
+    by simp
+  then show ?thesis by simp
+qed
+
+
 subsection {*An ``induction'' law for modulus arithmetic.*}
 
 lemma mod_induct_0:
@@ -870,6 +884,17 @@
   apply (rule mod_add1_eq [symmetric])
   done
 
+lemma mod_div_decomp:
+  fixes n k :: nat
+  obtains m q where "m = n div k" and "q = n mod k"
+    and "n = m * k + q"
+proof -
+  from mod_div_equality have "n = n div k * k + n mod k" by auto
+  moreover have "n div k = n div k" ..
+  moreover have "n mod k = n mod k" ..
+  note that ultimately show thesis by blast
+qed
+
 
 subsection {* Code generation for div, mod and dvd on nat *}