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.