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