src/HOL/Nat.thy
changeset 58649 a62065b5e1e2
parent 58647 fce800afeec7
child 58820 3ad2759acc52
     1.1 --- a/src/HOL/Nat.thy	Sun Oct 12 16:31:43 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sun Oct 12 17:05:34 2014 +0200
     1.3 @@ -1950,34 +1950,6 @@
     1.4    shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
     1.5  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
     1.6  
     1.7 -lemma dvd_plusE:
     1.8 -  fixes m n q :: nat
     1.9 -  assumes "m dvd n + q" "m dvd n"
    1.10 -  obtains "m dvd q"
    1.11 -proof (cases "m = 0")
    1.12 -  case True with assms that show thesis by simp
    1.13 -next
    1.14 -  case False then have "m > 0" by simp
    1.15 -  from assms obtain r s where "n = m * r" and "n + q = m * s" by (blast elim: dvdE)
    1.16 -  then have *: "m * r + q = m * s" by simp
    1.17 -  show thesis proof (cases "r \<le> s")
    1.18 -    case False then have "s < r" by (simp add: not_le)
    1.19 -    with * have "m * r + q - m * s = m * s - m * s" by simp
    1.20 -    then have "m * r + q - m * s = 0" by simp
    1.21 -    with `m > 0` `s < r` have "m * r - m * s + q = 0" by (unfold less_le_not_le) auto
    1.22 -    then have "m * (r - s) + q = 0" by auto
    1.23 -    then have "m * (r - s) = 0" by simp
    1.24 -    then have "m = 0 \<or> r - s = 0" by simp
    1.25 -    with `s < r` have "m = 0" by (simp add: less_le_not_le)
    1.26 -    with `m > 0` show thesis by auto
    1.27 -  next
    1.28 -    case True with * have "m * r + q - m * r = m * s - m * r" by simp
    1.29 -    with `m > 0` `r \<le> s` have "m * r - m * r + q = m * s - m * r" by simp
    1.30 -    then have "q = m * (s - r)" by (simp add: diff_mult_distrib2)
    1.31 -    with assms that show thesis by (auto intro: dvdI)
    1.32 -  qed
    1.33 -qed
    1.34 -
    1.35  lemma less_eq_dvd_minus:
    1.36    fixes m n :: nat
    1.37    assumes "m \<le> n"
    1.38 @@ -1999,7 +1971,7 @@
    1.39    shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
    1.40  proof -
    1.41    have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
    1.42 -    by (auto elim: dvd_plusE)
    1.43 +    using dvd_add_times_triv_left_iff [of m r] by simp
    1.44    also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
    1.45    also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
    1.46    also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
    1.47 @@ -2015,21 +1987,6 @@
    1.48  lemma nat_mult_1_right: "n * (1::nat) = n"
    1.49    by (fact mult_1_right)
    1.50  
    1.51 -lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    1.52 -  by (fact dvd_add_triv_right_iff)
    1.53 -
    1.54 -lemma dvd_plus_eq_right:
    1.55 -  fixes m n q :: nat
    1.56 -  assumes "m dvd n"
    1.57 -  shows "m dvd n + q \<longleftrightarrow> m dvd q"
    1.58 -  using assms by (fact dvd_add_eq_right)
    1.59 -
    1.60 -lemma dvd_plus_eq_left:
    1.61 -  fixes m n q :: nat
    1.62 -  assumes "m dvd q"
    1.63 -  shows "m dvd n + q \<longleftrightarrow> m dvd n"
    1.64 -  using assms by (fact dvd_add_eq_left)
    1.65 -
    1.66  
    1.67  subsection {* Size of a datatype value *}
    1.68