src/HOL/Nat.thy
changeset 51173 3cbb4e95a565
parent 49962 a8cc904a6820
child 51263 31e786e0e6a7
     1.1 --- a/src/HOL/Nat.thy	Sun Feb 17 20:45:49 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sun Feb 17 21:29:30 2013 +0100
     1.3 @@ -1587,6 +1587,12 @@
     1.4  lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
     1.5  by arith
     1.6  
     1.7 +lemma less_diff_conv2:
     1.8 +  fixes j k i :: nat
     1.9 +  assumes "k \<le> j"
    1.10 +  shows "j - k < i \<longleftrightarrow> j < i + k"
    1.11 +  using assms by arith
    1.12 +
    1.13  lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
    1.14  by arith
    1.15  
    1.16 @@ -1801,6 +1807,74 @@
    1.17    shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
    1.18  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    1.19  
    1.20 +lemma dvd_plusE:
    1.21 +  fixes m n q :: nat
    1.22 +  assumes "m dvd n + q" "m dvd n"
    1.23 +  obtains "m dvd q"
    1.24 +proof (cases "m = 0")
    1.25 +  case True with assms that show thesis by simp
    1.26 +next
    1.27 +  case False then have "m > 0" by simp
    1.28 +  from assms obtain r s where "n = m * r" and "n + q = m * s" by (blast elim: dvdE)
    1.29 +  then have *: "m * r + q = m * s" by simp
    1.30 +  show thesis proof (cases "r \<le> s")
    1.31 +    case False then have "s < r" by (simp add: not_le)
    1.32 +    with * have "m * r + q - m * s = m * s - m * s" by simp
    1.33 +    then have "m * r + q - m * s = 0" by simp
    1.34 +    with `m > 0` `s < r` have "m * r - m * s + q = 0" by simp
    1.35 +    then have "m * (r - s) + q = 0" by auto
    1.36 +    then have "m * (r - s) = 0" by simp
    1.37 +    then have "m = 0 \<or> r - s = 0" by simp
    1.38 +    with `s < r` have "m = 0" by arith
    1.39 +    with `m > 0` show thesis by auto
    1.40 +  next
    1.41 +    case True with * have "m * r + q - m * r = m * s - m * r" by simp
    1.42 +    with `m > 0` `r \<le> s` have "m * r - m * r + q = m * s - m * r" by simp
    1.43 +    then have "q = m * (s - r)" by (simp add: diff_mult_distrib2)
    1.44 +    with assms that show thesis by (auto intro: dvdI)
    1.45 +  qed
    1.46 +qed
    1.47 +
    1.48 +lemma dvd_plus_eq_right:
    1.49 +  fixes m n q :: nat
    1.50 +  assumes "m dvd n"
    1.51 +  shows "m dvd n + q \<longleftrightarrow> m dvd q"
    1.52 +  using assms by (auto elim: dvd_plusE)
    1.53 +
    1.54 +lemma dvd_plus_eq_left:
    1.55 +  fixes m n q :: nat
    1.56 +  assumes "m dvd q"
    1.57 +  shows "m dvd n + q \<longleftrightarrow> m dvd n"
    1.58 +  using assms by (simp add: dvd_plus_eq_right add_commute [of n])
    1.59 +
    1.60 +lemma less_dvd_minus:
    1.61 +  fixes m n :: nat
    1.62 +  assumes "m < n"
    1.63 +  shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
    1.64 +proof -
    1.65 +  from assms have "n = m + (n - m)" by arith
    1.66 +  then obtain q where "n = m + q" ..
    1.67 +  then show ?thesis by (simp add: dvd_reduce add_commute [of m])
    1.68 +qed
    1.69 +
    1.70 +lemma dvd_minus_self:
    1.71 +  fixes m n :: nat
    1.72 +  shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
    1.73 +  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
    1.74 +
    1.75 +lemma dvd_minus_add:
    1.76 +  fixes m n q r :: nat
    1.77 +  assumes "q \<le> n" "q \<le> r * m"
    1.78 +  shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
    1.79 +proof -
    1.80 +  have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
    1.81 +    by (auto elim: dvd_plusE)
    1.82 +  also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
    1.83 +  also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
    1.84 +  also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
    1.85 +  finally show ?thesis .
    1.86 +qed
    1.87 +
    1.88  
    1.89  subsection {* aliasses *}
    1.90