src/HOL/Arith.thy
 changeset 2681 93ed51a91622 parent 2099 c5f004bfcbab child 2887 00b8ee790d89
```     1.1 --- a/src/HOL/Arith.thy	Tue Feb 25 15:05:14 1997 +0100
1.2 +++ b/src/HOL/Arith.thy	Tue Feb 25 15:11:12 1997 +0100
1.3 @@ -17,14 +17,27 @@
1.4
1.5  defs
1.6    pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
1.7 -  add_def   "m+n == nat_rec n (%u v. Suc(v)) m"
1.8 -  diff_def  "m-n == nat_rec m (%u v. pred(v)) n"
1.9 -  mult_def  "m*n == nat_rec 0 (%u v. n + v) m"
1.10
1.11    mod_def   "m mod n == wfrec (trancl pred_nat)
1.12                            (%f j. if j<n then j else f (j-n)) m"
1.13    div_def   "m div n == wfrec (trancl pred_nat)
1.14                            (%f j. if j<n then 0 else Suc (f (j-n))) m"
1.15 +
1.16 +
1.17 +primrec "op +" nat
1.18 +"0 + n = n"
1.19 +"Suc m + n = Suc(m + n)"
1.20 +
1.21 +
1.22 +primrec "op -" nat
1.23 +"m - 0 = m"
1.24 +"m - Suc n = pred(m - n)"
1.25 +
1.26 +primrec "op *"  nat
1.27 +"0 * n = 0"
1.28 +"Suc m * n = n + (m * n)"
1.29 +
1.30 +
1.31  end
1.32
1.33  (*"Difference" is subtraction of natural numbers.
```