# HG changeset patch
# User wenzelm
# Date 1235907479 -3600
# Node ID 048fd5b942ae0ff13f91dfdc40787dc8df5458d4
# Parent  05629f28f0f78438ef37e072187a7ff82692c9cb# Parent  db768c888dfa3be380fcd40a2c8fa1608721fda0
merged

diff -r db768c888dfa -r 048fd5b942ae NEWS
--- a/NEWS	Sun Mar 01 12:37:42 2009 +0100
+++ b/NEWS	Sun Mar 01 12:37:59 2009 +0100
@@ -385,6 +385,7 @@
 nat_mod_mod_trivial    -> mod_mod_trivial
 zdiv_zadd_self1        -> div_add_self1
 zdiv_zadd_self2        -> div_add_self2
+zdiv_zmult_self1       -> div_mult_self2_is_id
 zdiv_zmult_self2       -> div_mult_self1_is_id
 zdvd_triv_left         -> dvd_triv_left
 zdvd_triv_right        -> dvd_triv_right
diff -r db768c888dfa -r 048fd5b942ae src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Mar 01 12:37:42 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Mar 01 12:37:59 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 db768c888dfa -r 048fd5b942ae src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sun Mar 01 12:37:42 2009 +0100
+++ b/src/HOL/IntDiv.thy	Sun Mar 01 12:37:59 2009 +0100
@@ -689,9 +689,6 @@
 apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
 done
 
-lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
-by (simp add: zdiv_zmult1_eq)
-
 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
 apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
@@ -717,7 +714,7 @@
   assume not0: "b \<noteq> 0"
   show "(a + c * b) div b = c + a div b"
     unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
-      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
+      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
 qed auto
 
 lemma posDivAlg_div_mod:
@@ -1225,6 +1222,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)"
diff -r db768c888dfa -r 048fd5b942ae src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Mar 01 12:37:42 2009 +0100
+++ b/src/HOL/Library/Float.thy	Sun Mar 01 12:37:59 2009 +0100
@@ -1093,7 +1093,7 @@
   { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto)
     also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
     finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1)
-    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding zdiv_zmult_self1[OF `m \<noteq> 0`] .
+    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
     hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
       unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
   from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"]