src/HOL/Nat.thy
changeset 59815 cce82e360c2f
parent 59582 0fbed69ff081
child 59816 034b13f4efae
     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 @@ -246,11 +246,10 @@
     1.4    fix n m q :: nat
     1.5    show "(n + m) + q = n + (m + q)" by (induct n) simp_all
     1.6    show "n + m = m + n" by (induct n) simp_all
     1.7 +  show "m + n - m = n" by (induct m) simp_all
     1.8 +  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
     1.9    show "0 + n = n" by simp
    1.10 -  show "n - 0 = n" by simp
    1.11    show "0 - n = 0" by simp
    1.12 -  show "(q + n) - (q + m) = n - m" by (induct q) simp_all
    1.13 -  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
    1.14  qed
    1.15  
    1.16  end
    1.17 @@ -283,7 +282,6 @@
    1.18    show "n * m = m * n" by (induct n) simp_all
    1.19    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
    1.20    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
    1.21 -  assume "n + m = n + q" thus "m = q" by (induct n) simp_all
    1.22  qed
    1.23  
    1.24  end
    1.25 @@ -355,7 +353,7 @@
    1.26    by (fact add_diff_cancel_right')
    1.27  
    1.28  lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
    1.29 -  by (fact comm_monoid_diff_class.add_diff_cancel_left)
    1.30 +  by (fact add_diff_cancel_left)
    1.31  
    1.32  lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
    1.33    by (fact add_diff_cancel_right)