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
```