src/HOL/Divides.thy
 changeset 58834 773b378d9313 parent 58786 fa5b67fb70ad child 58847 c44aff8ac894
```     1.1 --- a/src/HOL/Divides.thy	Thu Oct 30 16:36:44 2014 +0000
1.2 +++ b/src/HOL/Divides.thy	Thu Oct 30 21:02:01 2014 +0100
1.3 @@ -149,20 +149,24 @@
1.4    note that ultimately show thesis by blast
1.5  qed
1.6
1.7 -lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
1.8 +lemma dvd_imp_mod_0 [simp]:
1.9 +  assumes "a dvd b"
1.10 +  shows "b mod a = 0"
1.11 +proof -
1.12 +  from assms obtain c where "b = a * c" ..
1.13 +  then have "b mod a = a * c mod a" by simp
1.14 +  then show "b mod a = 0" by simp
1.15 +qed
1.16 +
1.17 +lemma dvd_eq_mod_eq_0 [code]:
1.18 +  "a dvd b \<longleftrightarrow> b mod a = 0"
1.19  proof
1.20    assume "b mod a = 0"
1.21    with mod_div_equality [of b a] have "b div a * a = b" by simp
1.22    then have "b = a * (b div a)" unfolding mult.commute ..
1.23 -  then have "\<exists>c. b = a * c" ..
1.24 -  then show "a dvd b" unfolding dvd_def .
1.25 +  then show "a dvd b" ..
1.26  next
1.27 -  assume "a dvd b"
1.28 -  then have "\<exists>c. b = a * c" unfolding dvd_def .
1.29 -  then obtain c where "b = a * c" ..
1.30 -  then have "b mod a = a * c mod a" by simp
1.31 -  then have "b mod a = c * a mod a" by (simp add: mult.commute)
1.32 -  then show "b mod a = 0" by simp
1.33 +  assume "a dvd b" then show "b mod a = 0" by simp
1.34  qed
1.35
1.36  lemma mod_div_trivial [simp]: "a mod b div b = 0"
1.37 @@ -190,36 +194,37 @@
1.38    finally show ?thesis .
1.39  qed
1.40
1.41 -lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
1.42 -by (rule dvd_eq_mod_eq_0[THEN iffD1])
1.43 -
1.44 -lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
1.45 -by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
1.46 -
1.47 -lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
1.48 -by (drule dvd_div_mult_self) (simp add: mult.commute)
1.49 -
1.50 -lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
1.51 -apply (cases "a = 0")
1.52 - apply simp
1.53 -apply (auto simp: dvd_def mult.assoc)
1.54 -done
1.55 -
1.56 -lemma div_dvd_div[simp]:
1.57 -  "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
1.58 -apply (cases "a = 0")
1.59 - apply simp
1.60 +lemma dvd_div_mult_self [simp]:
1.61 +  "a dvd b \<Longrightarrow> (b div a) * a = b"
1.62 +  using mod_div_equality [of b a, symmetric] by simp
1.63 +
1.64 +lemma dvd_mult_div_cancel [simp]:
1.65 +  "a dvd b \<Longrightarrow> a * (b div a) = b"
1.66 +  using dvd_div_mult_self by (simp add: ac_simps)
1.67 +
1.68 +lemma dvd_div_mult:
1.69 +  "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
1.70 +  by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
1.71 +
1.72 +lemma div_dvd_div [simp]:
1.73 +  assumes "a dvd b" and "a dvd c"
1.74 +  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
1.75 +using assms apply (cases "a = 0")
1.76 +apply auto
1.77  apply (unfold dvd_def)
1.78  apply auto
1.79   apply(blast intro:mult.assoc[symmetric])
1.81  done
1.82
1.83 -lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"
1.84 -  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
1.85 -   apply (simp add: mod_div_equality)
1.86 -  apply (simp only: dvd_add dvd_mult)
1.87 -  done
1.88 +lemma dvd_mod_imp_dvd:
1.89 +  assumes "k dvd m mod n" and "k dvd n"
1.90 +  shows "k dvd m"
1.91 +proof -
1.92 +  from assms have "k dvd (m div n) * n + m mod n"
1.93 +    by (simp only: dvd_add dvd_mult)
1.94 +  then show ?thesis by (simp add: mod_div_equality)
1.95 +qed
1.96
1.97  text {* Addition respects modular equivalence. *}
1.98
1.99 @@ -593,7 +598,7 @@
1.100    "even a \<Longrightarrow> 2 * (a div 2) = a"
1.101    by (fact dvd_mult_div_cancel)
1.102
1.103 -lemma odd_two_times_div_two_succ:
1.104 +lemma odd_two_times_div_two_succ [simp]:
1.105    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.106    using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.107
1.108 @@ -1528,10 +1533,14 @@
1.109    "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1.110    using odd_succ_div_two [of n] by simp
1.111
1.112 -lemma odd_two_times_div_two_Suc:
1.113 -  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
1.114 +lemma odd_two_times_div_two_nat [simp]:
1.115 +  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
1.116    using odd_two_times_div_two_succ [of n] by simp
1.117
1.118 +lemma odd_Suc_minus_one [simp]:
1.119 +  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
1.120 +  by (auto elim: oddE)
1.121 +
1.122  lemma parity_induct [case_names zero even odd]:
1.123    assumes zero: "P 0"
1.124    assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1.125 @@ -1549,11 +1558,11 @@
1.126      proof (cases "even n")
1.127        case True
1.128        with hyp even [of "n div 2"] show ?thesis
1.129 -        by (simp add: dvd_mult_div_cancel)
1.130 +        by simp
1.131      next
1.132        case False
1.133        with hyp odd [of "n div 2"] show ?thesis
1.134 -        by (simp add: odd_two_times_div_two_Suc)
1.135 +        by simp
1.136      qed
1.137    qed
1.138  qed
```