more simp rules concerning dvd and even/odd
authorhaftmann
Thu Oct 30 21:02:01 2014 +0100 (2014-10-30)
changeset 58834773b378d9313
parent 58833 09974789e483
child 58840 f4bb3068d819
more simp rules concerning dvd and even/odd
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Library/Float.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Transcendental.thy
src/HOL/Word/Bit_Representation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Author:     Johannes Hoelzl, TU Muenchen
     1.5 + (* Author:     Johannes Hoelzl, TU Muenchen
     1.6     Coercions removed by Dmitriy Traytel *)
     1.7  
     1.8  header {* Prove Real Valued Inequalities by Computation *}
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 16:36:44 2014 +0000
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 21:02:01 2014 +0100
     2.3 @@ -269,7 +269,7 @@
     2.4          by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two)
     2.5      next
     2.6        case False with * show ?thesis
     2.7 -        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)
     2.8 +        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric])
     2.9      qed
    2.10    qed
    2.11  qed
     3.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 16:36:44 2014 +0000
     3.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 30 21:02:01 2014 +0100
     3.3 @@ -211,11 +211,7 @@
     3.4  
     3.5  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
     3.6      (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
     3.7 -  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
     3.8 -  apply simp
     3.9 -  apply (simp add: dvd_eq_mod_eq_0)
    3.10 -  done
    3.11 -
    3.12 +  using of_int_div_aux [of d n, where ?'a = 'a] by simp
    3.13  
    3.14  lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
    3.15  proof -
     4.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 16:36:44 2014 +0000
     4.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 21:02:01 2014 +0100
     4.3 @@ -790,7 +790,7 @@
     4.4      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
     4.5        by (simp only: th)
     4.6      finally have ?case unfolding numeral_2_eq_2 [symmetric]
     4.7 -    using odd_two_times_div_two_Suc [OF odd] by simp
     4.8 +    using odd_two_times_div_two_nat [OF odd] by simp
     4.9    }
    4.10    moreover
    4.11    {
     5.1 --- a/src/HOL/Divides.thy	Thu Oct 30 16:36:44 2014 +0000
     5.2 +++ b/src/HOL/Divides.thy	Thu Oct 30 21:02:01 2014 +0100
     5.3 @@ -149,20 +149,24 @@
     5.4    note that ultimately show thesis by blast
     5.5  qed
     5.6  
     5.7 -lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
     5.8 +lemma dvd_imp_mod_0 [simp]:
     5.9 +  assumes "a dvd b"
    5.10 +  shows "b mod a = 0"
    5.11 +proof -
    5.12 +  from assms obtain c where "b = a * c" ..
    5.13 +  then have "b mod a = a * c mod a" by simp
    5.14 +  then show "b mod a = 0" by simp
    5.15 +qed
    5.16 +  
    5.17 +lemma dvd_eq_mod_eq_0 [code]:
    5.18 +  "a dvd b \<longleftrightarrow> b mod a = 0"
    5.19  proof
    5.20    assume "b mod a = 0"
    5.21    with mod_div_equality [of b a] have "b div a * a = b" by simp
    5.22    then have "b = a * (b div a)" unfolding mult.commute ..
    5.23 -  then have "\<exists>c. b = a * c" ..
    5.24 -  then show "a dvd b" unfolding dvd_def .
    5.25 +  then show "a dvd b" ..
    5.26  next
    5.27 -  assume "a dvd b"
    5.28 -  then have "\<exists>c. b = a * c" unfolding dvd_def .
    5.29 -  then obtain c where "b = a * c" ..
    5.30 -  then have "b mod a = a * c mod a" by simp
    5.31 -  then have "b mod a = c * a mod a" by (simp add: mult.commute)
    5.32 -  then show "b mod a = 0" by simp
    5.33 +  assume "a dvd b" then show "b mod a = 0" by simp
    5.34  qed
    5.35  
    5.36  lemma mod_div_trivial [simp]: "a mod b div b = 0"
    5.37 @@ -190,36 +194,37 @@
    5.38    finally show ?thesis .
    5.39  qed
    5.40  
    5.41 -lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
    5.42 -by (rule dvd_eq_mod_eq_0[THEN iffD1])
    5.43 -
    5.44 -lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
    5.45 -by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
    5.46 -
    5.47 -lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
    5.48 -by (drule dvd_div_mult_self) (simp add: mult.commute)
    5.49 -
    5.50 -lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
    5.51 -apply (cases "a = 0")
    5.52 - apply simp
    5.53 -apply (auto simp: dvd_def mult.assoc)
    5.54 -done
    5.55 -
    5.56 -lemma div_dvd_div[simp]:
    5.57 -  "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
    5.58 -apply (cases "a = 0")
    5.59 - apply simp
    5.60 +lemma dvd_div_mult_self [simp]:
    5.61 +  "a dvd b \<Longrightarrow> (b div a) * a = b"
    5.62 +  using mod_div_equality [of b a, symmetric] by simp
    5.63 +
    5.64 +lemma dvd_mult_div_cancel [simp]:
    5.65 +  "a dvd b \<Longrightarrow> a * (b div a) = b"
    5.66 +  using dvd_div_mult_self by (simp add: ac_simps)
    5.67 +
    5.68 +lemma dvd_div_mult:
    5.69 +  "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
    5.70 +  by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
    5.71 +
    5.72 +lemma div_dvd_div [simp]:
    5.73 +  assumes "a dvd b" and "a dvd c"
    5.74 +  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
    5.75 +using assms apply (cases "a = 0")
    5.76 +apply auto
    5.77  apply (unfold dvd_def)
    5.78  apply auto
    5.79   apply(blast intro:mult.assoc[symmetric])
    5.80  apply(fastforce simp add: mult.assoc)
    5.81  done
    5.82  
    5.83 -lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"
    5.84 -  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
    5.85 -   apply (simp add: mod_div_equality)
    5.86 -  apply (simp only: dvd_add dvd_mult)
    5.87 -  done
    5.88 +lemma dvd_mod_imp_dvd:
    5.89 +  assumes "k dvd m mod n" and "k dvd n"
    5.90 +  shows "k dvd m"
    5.91 +proof -
    5.92 +  from assms have "k dvd (m div n) * n + m mod n"
    5.93 +    by (simp only: dvd_add dvd_mult)
    5.94 +  then show ?thesis by (simp add: mod_div_equality)
    5.95 +qed
    5.96  
    5.97  text {* Addition respects modular equivalence. *}
    5.98  
    5.99 @@ -593,7 +598,7 @@
   5.100    "even a \<Longrightarrow> 2 * (a div 2) = a"
   5.101    by (fact dvd_mult_div_cancel)
   5.102  
   5.103 -lemma odd_two_times_div_two_succ:
   5.104 +lemma odd_two_times_div_two_succ [simp]:
   5.105    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   5.106    using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
   5.107  
   5.108 @@ -1528,10 +1533,14 @@
   5.109    "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   5.110    using odd_succ_div_two [of n] by simp
   5.111  
   5.112 -lemma odd_two_times_div_two_Suc:
   5.113 -  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
   5.114 +lemma odd_two_times_div_two_nat [simp]:
   5.115 +  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
   5.116    using odd_two_times_div_two_succ [of n] by simp
   5.117  
   5.118 +lemma odd_Suc_minus_one [simp]:
   5.119 +  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   5.120 +  by (auto elim: oddE)
   5.121 +
   5.122  lemma parity_induct [case_names zero even odd]:
   5.123    assumes zero: "P 0"
   5.124    assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
   5.125 @@ -1549,11 +1558,11 @@
   5.126      proof (cases "even n")
   5.127        case True
   5.128        with hyp even [of "n div 2"] show ?thesis
   5.129 -        by (simp add: dvd_mult_div_cancel)
   5.130 +        by simp
   5.131      next
   5.132        case False
   5.133        with hyp odd [of "n div 2"] show ?thesis 
   5.134 -        by (simp add: odd_two_times_div_two_Suc)
   5.135 +        by simp
   5.136      qed
   5.137    qed
   5.138  qed
     6.1 --- a/src/HOL/GCD.thy	Thu Oct 30 16:36:44 2014 +0000
     6.2 +++ b/src/HOL/GCD.thy	Thu Oct 30 21:02:01 2014 +0100
     6.3 @@ -584,8 +584,8 @@
     6.4    from dvdg dvdg' obtain ka kb ka' kb' where
     6.5        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     6.6      unfolding dvd_def by blast
     6.7 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
     6.8 -    by simp_all
     6.9 +  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
    6.10 +    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
    6.11    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    6.12      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    6.13        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
     7.1 --- a/src/HOL/Library/Float.thy	Thu Oct 30 16:36:44 2014 +0000
     7.2 +++ b/src/HOL/Library/Float.thy	Thu Oct 30 21:02:01 2014 +0100
     7.3 @@ -935,8 +935,7 @@
     7.4        unfolding normfloat_def
     7.5        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
     7.6          l_def[symmetric, THEN meta_eq_to_obj_eq]
     7.7 -      by transfer
     7.8 -         (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
     7.9 +      by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
    7.10     next
    7.11      assume "\<not> 0 \<le> l"
    7.12      def y' \<equiv> "y * 2 ^ nat (- l)"
    7.13 @@ -950,7 +949,7 @@
    7.14        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
    7.15          l_def[symmetric, THEN meta_eq_to_obj_eq]
    7.16        by transfer
    7.17 -         (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
    7.18 +         (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
    7.19    qed
    7.20  qed
    7.21  hide_fact (open) compute_rapprox_posrat
     8.1 --- a/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 16:36:44 2014 +0000
     8.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 21:02:01 2014 +0100
     8.3 @@ -122,7 +122,7 @@
     8.4  by (induct x) simp_all
     8.5  
     8.6  lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
     8.7 -  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
     8.8 +  by (simp add: even_two_times_div_two sum_decode_def sum_encode_def)
     8.9  
    8.10  lemma inj_sum_encode: "inj_on sum_encode A"
    8.11  by (rule inj_on_inverseI, rule sum_encode_inverse)
    8.12 @@ -269,12 +269,18 @@
    8.13  by auto
    8.14  
    8.15  lemma div2_even_ext_nat:
    8.16 -  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
    8.17 -apply (rule mod_div_equality [of x 2, THEN subst])
    8.18 -apply (rule mod_div_equality [of y 2, THEN subst])
    8.19 -apply (cases "even x")
    8.20 -apply (simp_all add: even_iff_mod_2_eq_zero)
    8.21 -done
    8.22 +  fixes x y :: nat
    8.23 +  assumes "x div 2 = y div 2"
    8.24 +  and "even x \<longleftrightarrow> even y"
    8.25 +  shows "x = y"
    8.26 +proof -
    8.27 +  from `even x \<longleftrightarrow> even y` have "x mod 2 = y mod 2"
    8.28 +    by (simp only: even_iff_mod_2_eq_zero) auto
    8.29 +  with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2"
    8.30 +    by simp
    8.31 +  then show ?thesis
    8.32 +    by simp
    8.33 +qed
    8.34  
    8.35  
    8.36  subsubsection {* From sets to naturals *}
     9.1 --- a/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 16:36:44 2014 +0000
     9.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 30 21:02:01 2014 +0100
     9.3 @@ -53,7 +53,7 @@
     9.4  
     9.5  lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
     9.6    using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
     9.7 -  by auto presburger
     9.8 +  by simp
     9.9  
    9.10  lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
    9.11    using odd_p p_ge_2
    10.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 16:36:44 2014 +0000
    10.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Oct 30 21:02:01 2014 +0100
    10.3 @@ -774,8 +774,8 @@
    10.4          unfolding mod_eq_0_iff by blast
    10.5        hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
    10.6        from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
    10.7 -      from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
    10.8 -      have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
    10.9 +      from dvd_trans[OF p(2) qn1]
   10.10 +      have npp: "(n - 1) div p * p = n - 1" by simp
   10.11        with eq0 have "a^ (n - 1) = (n*s)^p"
   10.12          by (simp add: power_mult[symmetric])
   10.13        hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
    11.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 16:36:44 2014 +0000
    11.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 21:02:01 2014 +0100
    11.3 @@ -207,7 +207,8 @@
    11.4    from dvdg dvdg' obtain ka kb ka' kb' where
    11.5        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
    11.6      unfolding dvd_def by blast
    11.7 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
    11.8 +  from this(3-4) [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
    11.9 +    by (simp_all only: ac_simps mult.left_commute [of _ "gcd a b"])
   11.10    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   11.11      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   11.12        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   11.13 @@ -351,7 +352,7 @@
   11.14            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
   11.15              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
   11.16            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
   11.17 -            by (simp only: diff_mult_distrib2 add.commute ac_simps)
   11.18 +            by (simp only: diff_mult_distrib2 ac_simps)
   11.19            hence ?thesis using H(1,2)
   11.20              apply -
   11.21              apply (rule exI[where x=d], simp)
   11.22 @@ -641,7 +642,8 @@
   11.23    from dvdg dvdg' obtain ka kb ka' kb' where
   11.24     kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
   11.25      unfolding dvd_def by blast
   11.26 -  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   11.27 +  from this(3-4) [symmetric] have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'"
   11.28 +    by (simp_all only: ac_simps mult.left_commute [of _ "zgcd a b"])
   11.29    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   11.30      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   11.31        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    12.1 --- a/src/HOL/Rat.thy	Thu Oct 30 16:36:44 2014 +0000
    12.2 +++ b/src/HOL/Rat.thy	Thu Oct 30 21:02:01 2014 +0100
    12.3 @@ -73,8 +73,8 @@
    12.4    let ?a = "a div gcd a b"
    12.5    let ?b = "b div gcd a b"
    12.6    from `b \<noteq> 0` have "?b * gcd a b = b"
    12.7 -    by (simp add: dvd_div_mult_self)
    12.8 -  with `b \<noteq> 0` have "?b \<noteq> 0" by auto
    12.9 +    by simp
   12.10 +  with `b \<noteq> 0` have "?b \<noteq> 0" by fastforce
   12.11    from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
   12.12      by (simp add: eq_rat dvd_div_mult mult.commute [of a])
   12.13    from `b \<noteq> 0` have coprime: "coprime ?a ?b"
   12.14 @@ -253,7 +253,8 @@
   12.15    case False
   12.16    moreover have "b div gcd a b * gcd a b = b"
   12.17      by (rule dvd_div_mult_self) simp
   12.18 -  ultimately have "b div gcd a b \<noteq> 0" by auto
   12.19 +  ultimately have "b div gcd a b * gcd a b \<noteq> 0" by simp
   12.20 +  then have "b div gcd a b \<noteq> 0" by fastforce
   12.21    with False show ?thesis by (simp add: eq_rat dvd_div_mult mult.commute [of a])
   12.22  qed
   12.23  
    13.1 --- a/src/HOL/Real.thy	Thu Oct 30 16:36:44 2014 +0000
    13.2 +++ b/src/HOL/Real.thy	Thu Oct 30 21:02:01 2014 +0100
    13.3 @@ -1132,12 +1132,10 @@
    13.4      by (auto simp add: add_divide_distrib algebra_simps)
    13.5  qed
    13.6  
    13.7 -lemma real_of_int_div: "(d :: int) dvd n ==>
    13.8 -    real(n div d) = real n / real d"
    13.9 -  apply (subst real_of_int_div_aux)
   13.10 -  apply simp
   13.11 -  apply (simp add: dvd_eq_mod_eq_0)
   13.12 -done
   13.13 +lemma real_of_int_div:
   13.14 +  fixes d n :: int
   13.15 +  shows "d dvd n \<Longrightarrow> real (n div d) = real n / real d"
   13.16 +  by (simp add: real_of_int_div_aux)
   13.17  
   13.18  lemma real_of_int_div2:
   13.19    "0 <= real (n::int) / real (x) - real (n div x)"
   13.20 @@ -1391,12 +1389,15 @@
   13.21      by (rule dvd_mult_div_cancel)
   13.22    have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
   13.23      by (rule dvd_mult_div_cancel)
   13.24 -  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
   13.25 +  from `n \<noteq> 0` and gcd_l
   13.26 +  have "?gcd * ?l \<noteq> 0" by simp
   13.27 +  then have "?l \<noteq> 0" by (blast dest!: mult_not_zero) 
   13.28    moreover
   13.29    have "\<bar>x\<bar> = real ?k / real ?l"
   13.30    proof -
   13.31      from gcd have "real ?k / real ?l =
   13.32 -        real (?gcd * ?k) / real (?gcd * ?l)" by simp
   13.33 +      real (?gcd * ?k) / real (?gcd * ?l)"
   13.34 +      by (simp only: real_of_nat_mult) simp
   13.35      also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
   13.36      also from x_rat have "\<dots> = \<bar>x\<bar>" ..
   13.37      finally show ?thesis ..
    14.1 --- a/src/HOL/Transcendental.thy	Thu Oct 30 16:36:44 2014 +0000
    14.2 +++ b/src/HOL/Transcendental.thy	Thu Oct 30 21:02:01 2014 +0100
    14.3 @@ -203,7 +203,7 @@
    14.4        then show ?thesis by (auto simp add: even_two_times_div_two)
    14.5      next
    14.6        case False
    14.7 -      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
    14.8 +      then have eq: "Suc (2 * (m div 2)) = m" by simp
    14.9        hence "even (2 * (m div 2))" using `odd m` by auto
   14.10        have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
   14.11        also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
    15.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 16:36:44 2014 +0000
    15.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 21:02:01 2014 +0100
    15.3 @@ -316,8 +316,7 @@
    15.4    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
    15.5           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    15.6    apply (rule trans [symmetric, OF _ emep1])
    15.7 -     apply auto
    15.8 -  apply (auto simp: even_iff_mod_2_eq_zero)
    15.9 +  apply auto
   15.10    done
   15.11  
   15.12  subsection "Simplifications for (s)bintrunc"