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.80  apply(fastforce simp add: mult.assoc)
    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