generalized and consolidated some theorems concerning divisibility
authorhaftmann
Sun Oct 12 17:05:34 2014 +0200 (2014-10-12)
changeset 58649a62065b5e1e2
parent 58648 3ccafeb9a1d1
child 58650 1ddba8bcbb58
generalized and consolidated some theorems concerning divisibility
NEWS
src/HOL/Int.thy
src/HOL/Nat.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Rings.thy
     1.1 --- a/NEWS	Sun Oct 12 16:31:43 2014 +0200
     1.2 +++ b/NEWS	Sun Oct 12 17:05:34 2014 +0200
     1.3 @@ -42,6 +42,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Generalized and consolidated some theorems concerning divsibility:
     1.8 +  dvd_reduce ~> dvd_add_triv_right_iff
     1.9 +  dvd_plus_eq_right ~> dvd_add_right_iff
    1.10 +  dvd_plus_eq_left ~> dvd_add_left_iff
    1.11 +Minor INCOMPATIBILITY.
    1.12 +
    1.13  * More foundational definition for predicate "even":
    1.14    even_def ~> even_iff_mod_2_eq_zero
    1.15  Minor INCOMPATIBILITY.
     2.1 --- a/src/HOL/Int.thy	Sun Oct 12 16:31:43 2014 +0200
     2.2 +++ b/src/HOL/Int.thy	Sun Oct 12 17:05:34 2014 +0200
     2.3 @@ -1242,19 +1242,10 @@
     2.4  qed
     2.5  
     2.6  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
     2.7 -  apply (subgoal_tac "m = n + (m - n)")
     2.8 -   apply (erule ssubst)
     2.9 -   apply (blast intro: dvd_add, simp)
    2.10 -  done
    2.11 +  using dvd_add_right_iff [of k "- n" m] by simp 
    2.12  
    2.13  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
    2.14 -apply (rule iffI)
    2.15 - apply (erule_tac [2] dvd_add)
    2.16 - apply (subgoal_tac "n = (n + k * m) - k * m")
    2.17 -  apply (erule ssubst)
    2.18 -  apply (erule dvd_diff)
    2.19 -  apply(simp_all)
    2.20 -done
    2.21 +  using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
    2.22  
    2.23  lemma dvd_imp_le_int:
    2.24    fixes d i :: int
     3.1 --- a/src/HOL/Nat.thy	Sun Oct 12 16:31:43 2014 +0200
     3.2 +++ b/src/HOL/Nat.thy	Sun Oct 12 17:05:34 2014 +0200
     3.3 @@ -1950,34 +1950,6 @@
     3.4    shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
     3.5  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
     3.6  
     3.7 -lemma dvd_plusE:
     3.8 -  fixes m n q :: nat
     3.9 -  assumes "m dvd n + q" "m dvd n"
    3.10 -  obtains "m dvd q"
    3.11 -proof (cases "m = 0")
    3.12 -  case True with assms that show thesis by simp
    3.13 -next
    3.14 -  case False then have "m > 0" by simp
    3.15 -  from assms obtain r s where "n = m * r" and "n + q = m * s" by (blast elim: dvdE)
    3.16 -  then have *: "m * r + q = m * s" by simp
    3.17 -  show thesis proof (cases "r \<le> s")
    3.18 -    case False then have "s < r" by (simp add: not_le)
    3.19 -    with * have "m * r + q - m * s = m * s - m * s" by simp
    3.20 -    then have "m * r + q - m * s = 0" by simp
    3.21 -    with `m > 0` `s < r` have "m * r - m * s + q = 0" by (unfold less_le_not_le) auto
    3.22 -    then have "m * (r - s) + q = 0" by auto
    3.23 -    then have "m * (r - s) = 0" by simp
    3.24 -    then have "m = 0 \<or> r - s = 0" by simp
    3.25 -    with `s < r` have "m = 0" by (simp add: less_le_not_le)
    3.26 -    with `m > 0` show thesis by auto
    3.27 -  next
    3.28 -    case True with * have "m * r + q - m * r = m * s - m * r" by simp
    3.29 -    with `m > 0` `r \<le> s` have "m * r - m * r + q = m * s - m * r" by simp
    3.30 -    then have "q = m * (s - r)" by (simp add: diff_mult_distrib2)
    3.31 -    with assms that show thesis by (auto intro: dvdI)
    3.32 -  qed
    3.33 -qed
    3.34 -
    3.35  lemma less_eq_dvd_minus:
    3.36    fixes m n :: nat
    3.37    assumes "m \<le> n"
    3.38 @@ -1999,7 +1971,7 @@
    3.39    shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
    3.40  proof -
    3.41    have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
    3.42 -    by (auto elim: dvd_plusE)
    3.43 +    using dvd_add_times_triv_left_iff [of m r] by simp
    3.44    also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
    3.45    also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
    3.46    also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
    3.47 @@ -2015,21 +1987,6 @@
    3.48  lemma nat_mult_1_right: "n * (1::nat) = n"
    3.49    by (fact mult_1_right)
    3.50  
    3.51 -lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    3.52 -  by (fact dvd_add_triv_right_iff)
    3.53 -
    3.54 -lemma dvd_plus_eq_right:
    3.55 -  fixes m n q :: nat
    3.56 -  assumes "m dvd n"
    3.57 -  shows "m dvd n + q \<longleftrightarrow> m dvd q"
    3.58 -  using assms by (fact dvd_add_eq_right)
    3.59 -
    3.60 -lemma dvd_plus_eq_left:
    3.61 -  fixes m n q :: nat
    3.62 -  assumes "m dvd q"
    3.63 -  shows "m dvd n + q \<longleftrightarrow> m dvd n"
    3.64 -  using assms by (fact dvd_add_eq_left)
    3.65 -
    3.66  
    3.67  subsection {* Size of a datatype value *}
    3.68  
     4.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 12 16:31:43 2014 +0200
     4.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Oct 12 17:05:34 2014 +0200
     4.3 @@ -142,7 +142,7 @@
     4.4      }
     4.5      then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)"
     4.6        by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v]
     4.7 -        dvd_plus_eq_left dvd_plus_eq_right)
     4.8 +        dvd_add_left_iff dvd_add_right_iff)
     4.9      moreover from q have "Suc q = m + w + r" by (simp add: w_def)
    4.10      moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def)
    4.11      ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))"
     5.1 --- a/src/HOL/Rings.thy	Sun Oct 12 16:31:43 2014 +0200
     5.2 +++ b/src/HOL/Rings.thy	Sun Oct 12 17:05:34 2014 +0200
     5.3 @@ -228,15 +228,15 @@
     5.4    "a dvd b + a \<longleftrightarrow> a dvd b"
     5.5    using dvd_add_times_triv_right_iff [of a b 1] by simp
     5.6  
     5.7 -lemma dvd_add_eq_right:
     5.8 +lemma dvd_add_right_iff:
     5.9    assumes "a dvd b"
    5.10    shows "a dvd b + c \<longleftrightarrow> a dvd c"
    5.11    using assms by (auto dest: dvd_addD)
    5.12  
    5.13 -lemma dvd_add_eq_left:
    5.14 +lemma dvd_add_left_iff:
    5.15    assumes "a dvd c"
    5.16    shows "a dvd b + c \<longleftrightarrow> a dvd b"
    5.17 -  using assms dvd_add_eq_right [of a c b] by (simp add: ac_simps)
    5.18 +  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
    5.19  
    5.20  end
    5.21