src/HOL/Nat.thy
 changeset 59816 034b13f4efae parent 59815 cce82e360c2f child 59833 ab828c2c5d67
```     1.1 --- a/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
1.2 +++ b/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
1.3 @@ -366,12 +366,20 @@
1.4
1.5  text {* Difference distributes over multiplication *}
1.6
1.7 -lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
1.8 -by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
1.9 -
1.10 -lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
1.11 -by (simp add: diff_mult_distrib mult.commute [of k])
1.12 -  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
1.13 +instance nat :: comm_semiring_1_diff_distrib
1.14 +proof
1.15 +  fix k m n :: nat
1.16 +  show "k * ((m::nat) - n) = (k * m) - (k * n)"
1.17 +    by (induct m n rule: diff_induct) simp_all
1.18 +qed
1.19 +
1.20 +lemma diff_mult_distrib:
1.21 +  "((m::nat) - n) * k = (m * k) - (n * k)"
1.22 +  by (fact left_diff_distrib')
1.23 +
1.24 +lemma diff_mult_distrib2:
1.25 +  "k * ((m::nat) - n) = (k * m) - (k * n)"
1.26 +  by (fact right_diff_distrib')
1.27
1.28
1.29  subsubsection {* Multiplication *}
1.30 @@ -1876,48 +1884,6 @@
1.31
1.32  subsection {* The divides relation on @{typ nat} *}
1.33
1.34 -instance nat :: semiring_dvd
1.35 -proof
1.36 -  fix m n q :: nat
1.37 -  show "m dvd q * m + n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
1.38 -  proof
1.39 -    assume ?Q then show ?P by simp
1.40 -  next
1.41 -    assume ?P then obtain d where *: "q * m + n = m * d" ..
1.42 -    show ?Q
1.43 -    proof (cases "n = 0")
1.44 -      case True then show ?Q by simp
1.45 -    next
1.46 -      case False
1.47 -      with * have "q * m < m * d"
1.48 -        using less_add_eq_less [of 0 n "q * m" "m * d"] by simp
1.49 -      then have "q \<le> d" by (auto intro: ccontr simp add: mult.commute [of m])
1.50 -      with * [symmetric] have "n = m * (d - q)"
1.51 -        by (simp add: diff_mult_distrib2 mult.commute [of m])
1.52 -      then show ?Q ..
1.53 -    qed
1.54 -  qed
1.55 -  assume "m dvd n + q" and "m dvd n"
1.56 -  show "m dvd q"
1.57 -  proof -
1.58 -    from `m dvd n` obtain d where "n = m * d" ..
1.59 -    moreover from `m dvd n + q` obtain e where "n + q = m * e" ..
1.60 -    ultimately have *: "m * d + q = m * e" by simp
1.61 -    show "m dvd q"
1.62 -    proof (cases "q = 0")
1.63 -      case True then show ?thesis by simp
1.64 -    next
1.65 -      case False
1.66 -      with * have "m * d < m * e"
1.67 -        using less_add_eq_less [of 0 q "m * d" "m * e"] by simp
1.68 -      then have "d \<le> e" by (auto intro: ccontr)
1.69 -      with * have "q = m * (e - d)"
1.70 -        by (simp add: diff_mult_distrib2)
1.71 -      then show ?thesis ..
1.72 -    qed
1.73 -  qed
1.74 -qed
1.75 -
1.76  lemma dvd_1_left [iff]: "Suc 0 dvd k"
1.77  unfolding dvd_def by simp
1.78
```