# HG changeset patch
# User haftmann
# Date 1415217564 -3600
# Node ID 2cf595ee508b3931d1f74822f3dca09d18dbe1de
# Parent  edcd9339bda1f8d80a168f183532881b84ff02c9
proper oriented equivalence of dvd predicate and mod

diff -r edcd9339bda1 -r 2cf595ee508b src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/HOL/Divides.thy	Wed Nov 05 20:59:24 2014 +0100
@@ -157,19 +157,25 @@
   then have "b mod a = a * c mod a" by simp
   then show "b mod a = 0" by simp
 qed
-  
+
+lemma mod_eq_0_iff_dvd:
+  "a mod b = 0 \<longleftrightarrow> b dvd a"
+proof
+  assume "b dvd a"
+  then show "a mod b = 0" by simp
+next
+  assume "a mod b = 0"
+  with mod_div_equality [of a b] have "a div b * b = a" by simp
+  then have "a = b * (a div b)" by (simp add: ac_simps)
+  then show "b dvd a" ..
+qed
+
 lemma dvd_eq_mod_eq_0 [code]:
   "a dvd b \<longleftrightarrow> b mod a = 0"
-proof
-  assume "b mod a = 0"
-  with mod_div_equality [of b a] have "b div a * a = b" by simp
-  then have "b = a * (b div a)" unfolding mult.commute ..
-  then show "a dvd b" ..
-next
-  assume "a dvd b" then show "b mod a = 0" by simp
-qed
-
-lemma mod_div_trivial [simp]: "a mod b div b = 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma mod_div_trivial [simp]:
+  "a mod b div b = 0"
 proof (cases "b = 0")
   assume "b = 0"
   thus ?thesis by simp
@@ -185,7 +191,8 @@
     by (rule add_left_imp_eq)
 qed
 
-lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
+lemma mod_mod_trivial [simp]:
+  "a mod b mod b = a mod b"
 proof -
   have "a mod b mod b = (a mod b + a div b * b) mod b"
     by (simp only: mod_mult_self1)