# HG changeset patch
# User nipkow
# Date 1235899497 -3600
# Node ID 6d29a873141f4c99c3c119283705a4e1f57ef2ba
# Parent  c703c9368c127381f4e813c08b78d4c385361b5b
added lemmas by Jeremy Avigad

diff -r c703c9368c12 -r 6d29a873141f src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Feb 28 21:34:33 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Mar 01 10:24:57 2009 +0100
@@ -44,10 +44,10 @@
 by (simp add: mod_div_equality2)
 
 lemma mod_by_0 [simp]: "a mod 0 = a"
-  using mod_div_equality [of a zero] by simp
+using mod_div_equality [of a zero] by simp
 
 lemma mod_0 [simp]: "0 mod a = 0"
-  using mod_div_equality [of zero a] div_0 by simp 
+using mod_div_equality [of zero a] div_0 by simp
 
 lemma div_mult_self2 [simp]:
   assumes "b \<noteq> 0"
@@ -342,6 +342,25 @@
   unfolding diff_minus using assms
   by (intro mod_add_cong mod_minus_cong)
 
+lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
+apply (case_tac "y = 0") apply simp
+apply (auto simp add: dvd_def)
+apply (subgoal_tac "-(y * k) = y * - k")
+ apply (erule ssubst)
+ apply (erule div_mult_self1_is_id)
+apply simp
+done
+
+lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
+apply (case_tac "y = 0") apply simp
+apply (auto simp add: dvd_def)
+apply (subgoal_tac "y * k = -y * -k")
+ apply (erule ssubst)
+ apply (rule div_mult_self1_is_id)
+ apply simp
+apply simp
+done
+
 end
 
 
diff -r c703c9368c12 -r 6d29a873141f src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sat Feb 28 21:34:33 2009 +0100
+++ b/src/HOL/IntDiv.thy	Sun Mar 01 10:24:57 2009 +0100
@@ -1225,6 +1225,9 @@
 apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
 done
 
+lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
+by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
+
 text{*Suggested by Matthias Daum*}
 lemma int_power_div_base:
      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"