# HG changeset patch
# User wenzelm
# Date 1414707251 -3600
# Node ID f4bb3068d819f12a719074e7466e4b713e4a23a1
# Parent  773b378d9313520264c571320cd4d73256e83d20# Parent  ccda99401bc8e8f0f54c986f3e8cf4bbf578fbc8
merged

diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -1,4 +1,4 @@
-(* Author:     Johannes Hoelzl, TU Muenchen
+ (* Author:     Johannes Hoelzl, TU Muenchen
    Coercions removed by Dmitriy Traytel *)
 
 header {* Prove Real Valued Inequalities by Computation *}
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -269,7 +269,7 @@
         by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two)
     next
       case False with * show ?thesis
-        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric] odd_two_times_div_two_Suc)
+        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric])
     qed
   qed
 qed
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -211,11 +211,7 @@
 
 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
     (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
-  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
-  apply simp
-  apply (simp add: dvd_eq_mod_eq_0)
-  done
-
+  using of_int_div_aux [of d n, where ?'a = 'a] by simp
 
 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
 proof -
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -790,7 +790,7 @@
     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
       by (simp only: th)
     finally have ?case unfolding numeral_2_eq_2 [symmetric]
-    using odd_two_times_div_two_Suc [OF odd] by simp
+    using odd_two_times_div_two_nat [OF odd] by simp
   }
   moreover
   {
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -149,20 +149,24 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_imp_mod_0 [simp]:
+  assumes "a dvd b"
+  shows "b mod a = 0"
+proof -
+  from assms obtain c where "b = a * c" ..
+  then have "b mod a = a * c mod a" by simp
+  then show "b mod a = 0" by simp
+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 have "\<exists>c. b = a * c" ..
-  then show "a dvd b" unfolding dvd_def .
+  then show "a dvd b" ..
 next
-  assume "a dvd b"
-  then have "\<exists>c. b = a * c" unfolding dvd_def .
-  then obtain c where "b = a * c" ..
-  then have "b mod a = a * c mod a" by simp
-  then have "b mod a = c * a mod a" by (simp add: mult.commute)
-  then show "b mod a = 0" by simp
+  assume "a dvd b" then show "b mod a = 0" by simp
 qed
 
 lemma mod_div_trivial [simp]: "a mod b div b = 0"
@@ -190,36 +194,37 @@
   finally show ?thesis .
 qed
 
-lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
-by (rule dvd_eq_mod_eq_0[THEN iffD1])
-
-lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
-by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
-
-lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
-by (drule dvd_div_mult_self) (simp add: mult.commute)
-
-lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
-apply (cases "a = 0")
- apply simp
-apply (auto simp: dvd_def mult.assoc)
-done
-
-lemma div_dvd_div[simp]:
-  "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
-apply (cases "a = 0")
- apply simp
+lemma dvd_div_mult_self [simp]:
+  "a dvd b \<Longrightarrow> (b div a) * a = b"
+  using mod_div_equality [of b a, symmetric] by simp
+
+lemma dvd_mult_div_cancel [simp]:
+  "a dvd b \<Longrightarrow> a * (b div a) = b"
+  using dvd_div_mult_self by (simp add: ac_simps)
+
+lemma dvd_div_mult:
+  "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
+  by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
+
+lemma div_dvd_div [simp]:
+  assumes "a dvd b" and "a dvd c"
+  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
+using assms apply (cases "a = 0")
+apply auto
 apply (unfold dvd_def)
 apply auto
  apply(blast intro:mult.assoc[symmetric])
 apply(fastforce simp add: mult.assoc)
 done
 
-lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"
-  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
-   apply (simp add: mod_div_equality)
-  apply (simp only: dvd_add dvd_mult)
-  done
+lemma dvd_mod_imp_dvd:
+  assumes "k dvd m mod n" and "k dvd n"
+  shows "k dvd m"
+proof -
+  from assms have "k dvd (m div n) * n + m mod n"
+    by (simp only: dvd_add dvd_mult)
+  then show ?thesis by (simp add: mod_div_equality)
+qed
 
 text {* Addition respects modular equivalence. *}
 
@@ -593,7 +598,7 @@
   "even a \<Longrightarrow> 2 * (a div 2) = a"
   by (fact dvd_mult_div_cancel)
 
-lemma odd_two_times_div_two_succ:
+lemma odd_two_times_div_two_succ [simp]:
   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
 
@@ -1528,10 +1533,14 @@
   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   using odd_succ_div_two [of n] by simp
 
-lemma odd_two_times_div_two_Suc:
-  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
+lemma odd_two_times_div_two_nat [simp]:
+  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
   using odd_two_times_div_two_succ [of n] by simp
 
+lemma odd_Suc_minus_one [simp]:
+  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+  by (auto elim: oddE)
+
 lemma parity_induct [case_names zero even odd]:
   assumes zero: "P 0"
   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
@@ -1549,11 +1558,11 @@
     proof (cases "even n")
       case True
       with hyp even [of "n div 2"] show ?thesis
-        by (simp add: dvd_mult_div_cancel)
+        by simp
     next
       case False
       with hyp odd [of "n div 2"] show ?thesis 
-        by (simp add: odd_two_times_div_two_Suc)
+        by simp
     qed
   qed
 qed
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/GCD.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -584,8 +584,8 @@
   from dvdg dvdg' obtain ka kb ka' kb' where
       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     unfolding dvd_def by blast
-  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
-    by simp_all
+  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Library/Float.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -935,8 +935,7 @@
       unfolding normfloat_def
       using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
         l_def[symmetric, THEN meta_eq_to_obj_eq]
-      by transfer
-         (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
+      by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
    next
     assume "\<not> 0 \<le> l"
     def y' \<equiv> "y * 2 ^ nat (- l)"
@@ -950,7 +949,7 @@
       using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
         l_def[symmetric, THEN meta_eq_to_obj_eq]
       by transfer
-         (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
+         (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
   qed
 qed
 hide_fact (open) compute_rapprox_posrat
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -122,7 +122,7 @@
 by (induct x) simp_all
 
 lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
-  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
+  by (simp add: even_two_times_div_two sum_decode_def sum_encode_def)
 
 lemma inj_sum_encode: "inj_on sum_encode A"
 by (rule inj_on_inverseI, rule sum_encode_inverse)
@@ -269,12 +269,18 @@
 by auto
 
 lemma div2_even_ext_nat:
-  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
-apply (rule mod_div_equality [of x 2, THEN subst])
-apply (rule mod_div_equality [of y 2, THEN subst])
-apply (cases "even x")
-apply (simp_all add: even_iff_mod_2_eq_zero)
-done
+  fixes x y :: nat
+  assumes "x div 2 = y div 2"
+  and "even x \<longleftrightarrow> even y"
+  shows "x = y"
+proof -
+  from `even x \<longleftrightarrow> even y` have "x mod 2 = y mod 2"
+    by (simp only: even_iff_mod_2_eq_zero) auto
+  with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2"
+    by simp
+  then show ?thesis
+    by simp
+qed
 
 
 subsubsection {* From sets to naturals *}
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -32,8 +32,8 @@
 
 lemma choose_reduce_nat: 
   "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>
-    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
-  by (metis Suc_diff_1 binomial.simps(2) add.commute neq0_conv)
+    (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
+  by (metis Suc_diff_1 binomial.simps(2) neq0_conv)
 
 lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"
   by (induct n arbitrary: k) auto
@@ -524,7 +524,6 @@
       using Suc
       apply auto
     done
-
   have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
     ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
     apply (simp add: Suc field_simps del: fact_Suc)
@@ -547,6 +546,10 @@
   finally show ?thesis by (simp del: fact_Suc)
 qed
 
+lemma gbinomial_reduce_nat:
+  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
+by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
+
 
 lemma binomial_symmetric:
   assumes kn: "k \<le> n"
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -53,7 +53,7 @@
 
 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
   using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
-  by auto presburger
+  by simp
 
 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
   using odd_p p_ge_2
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -774,8 +774,8 @@
         unfolding mod_eq_0_iff by blast
       hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
       from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
-      from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
-      have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
+      from dvd_trans[OF p(2) qn1]
+      have npp: "(n - 1) div p * p = n - 1" by simp
       with eq0 have "a^ (n - 1) = (n*s)^p"
         by (simp add: power_mult[symmetric])
       hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -207,7 +207,8 @@
   from dvdg dvdg' obtain ka kb ka' kb' where
       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     unfolding dvd_def by blast
-  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
+  from this(3-4) [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+    by (simp_all only: ac_simps mult.left_commute [of _ "gcd a b"])
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
@@ -351,7 +352,7 @@
           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
-            by (simp only: diff_mult_distrib2 add.commute ac_simps)
+            by (simp only: diff_mult_distrib2 ac_simps)
           hence ?thesis using H(1,2)
             apply -
             apply (rule exI[where x=d], simp)
@@ -641,7 +642,8 @@
   from dvdg dvdg' obtain ka kb ka' kb' where
    kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
     unfolding dvd_def by blast
-  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
+  from this(3-4) [symmetric] have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'"
+    by (simp_all only: ac_simps mult.left_commute [of _ "zgcd a b"])
   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Rat.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -73,8 +73,8 @@
   let ?a = "a div gcd a b"
   let ?b = "b div gcd a b"
   from `b \<noteq> 0` have "?b * gcd a b = b"
-    by (simp add: dvd_div_mult_self)
-  with `b \<noteq> 0` have "?b \<noteq> 0" by auto
+    by simp
+  with `b \<noteq> 0` have "?b \<noteq> 0" by fastforce
   from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
     by (simp add: eq_rat dvd_div_mult mult.commute [of a])
   from `b \<noteq> 0` have coprime: "coprime ?a ?b"
@@ -253,7 +253,8 @@
   case False
   moreover have "b div gcd a b * gcd a b = b"
     by (rule dvd_div_mult_self) simp
-  ultimately have "b div gcd a b \<noteq> 0" by auto
+  ultimately have "b div gcd a b * gcd a b \<noteq> 0" by simp
+  then have "b div gcd a b \<noteq> 0" by fastforce
   with False show ?thesis by (simp add: eq_rat dvd_div_mult mult.commute [of a])
 qed
 
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Real.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -1132,12 +1132,10 @@
     by (auto simp add: add_divide_distrib algebra_simps)
 qed
 
-lemma real_of_int_div: "(d :: int) dvd n ==>
-    real(n div d) = real n / real d"
-  apply (subst real_of_int_div_aux)
-  apply simp
-  apply (simp add: dvd_eq_mod_eq_0)
-done
+lemma real_of_int_div:
+  fixes d n :: int
+  shows "d dvd n \<Longrightarrow> real (n div d) = real n / real d"
+  by (simp add: real_of_int_div_aux)
 
 lemma real_of_int_div2:
   "0 <= real (n::int) / real (x) - real (n div x)"
@@ -1391,12 +1389,15 @@
     by (rule dvd_mult_div_cancel)
   have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
     by (rule dvd_mult_div_cancel)
-  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
+  from `n \<noteq> 0` and gcd_l
+  have "?gcd * ?l \<noteq> 0" by simp
+  then have "?l \<noteq> 0" by (blast dest!: mult_not_zero) 
   moreover
   have "\<bar>x\<bar> = real ?k / real ?l"
   proof -
     from gcd have "real ?k / real ?l =
-        real (?gcd * ?k) / real (?gcd * ?l)" by simp
+      real (?gcd * ?k) / real (?gcd * ?l)"
+      by (simp only: real_of_nat_mult) simp
     also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
     also from x_rat have "\<dots> = \<bar>x\<bar>" ..
     finally show ?thesis ..
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Transcendental.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -203,7 +203,7 @@
       then show ?thesis by (auto simp add: even_two_times_div_two)
     next
       case False
-      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
+      then have eq: "Suc (2 * (m div 2)) = m" by simp
       hence "even (2 * (m div 2))" using `odd m` by auto
       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
diff -r ccda99401bc8 -r f4bb3068d819 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 22:45:19 2014 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 23:14:11 2014 +0100
@@ -316,8 +316,7 @@
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
-     apply auto
-  apply (auto simp: even_iff_mod_2_eq_zero)
+  apply auto
   done
 
 subsection "Simplifications for (s)bintrunc"