src/HOL/Nat.thy
changeset 49388 1ffd5a055acf
parent 48891 c0eafbd55de3
child 49723 bbc2942ba09f
     1.1 --- a/src/HOL/Nat.thy	Sat Sep 15 20:13:25 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Sep 15 20:14:29 2012 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  
     1.5  subsection {* Arithmetic operators *}
     1.6  
     1.7 -instantiation nat :: "{minus, comm_monoid_add}"
     1.8 +instantiation nat :: comm_monoid_diff
     1.9  begin
    1.10  
    1.11  primrec plus_nat where
    1.12 @@ -169,6 +169,10 @@
    1.13    show "(n + m) + q = n + (m + q)" by (induct n) simp_all
    1.14    show "n + m = m + n" by (induct n) simp_all
    1.15    show "0 + n = n" by simp
    1.16 +  show "n - 0 = n" by simp
    1.17 +  show "0 - n = 0" by simp
    1.18 +  show "(q + n) - (q + m) = n - m" by (induct q) simp_all
    1.19 +  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
    1.20  qed
    1.21  
    1.22  end
    1.23 @@ -1814,3 +1818,4 @@
    1.24  hide_const (open) of_nat_aux
    1.25  
    1.26  end
    1.27 +