equal
deleted
inserted
replaced
21 mod_def "m mod n == wfrec (trancl pred_nat) |
21 mod_def "m mod n == wfrec (trancl pred_nat) |
22 (%f j. if j<n then j else f (j-n)) m" |
22 (%f j. if j<n then j else f (j-n)) m" |
23 div_def "m div n == wfrec (trancl pred_nat) |
23 div_def "m div n == wfrec (trancl pred_nat) |
24 (%f j. if j<n then 0 else Suc (f (j-n))) m" |
24 (%f j. if j<n then 0 else Suc (f (j-n))) m" |
25 |
25 |
26 |
|
27 primrec "op +" nat |
26 primrec "op +" nat |
28 "0 + n = n" |
27 "0 + n = n" |
29 "Suc m + n = Suc(m + n)" |
28 "Suc m + n = Suc(m + n)" |
30 |
|
31 |
29 |
32 primrec "op -" nat |
30 primrec "op -" nat |
33 "m - 0 = m" |
31 "m - 0 = m" |
34 "m - Suc n = pred(m - n)" |
32 "m - Suc n = pred(m - n)" |
35 |
33 |
36 primrec "op *" nat |
34 primrec "op *" nat |
37 "0 * n = 0" |
35 "0 * n = 0" |
38 "Suc m * n = n + (m * n)" |
36 "Suc m * n = n + (m * n)" |
39 |
|
40 |
37 |
41 end |
38 end |
42 |
|
43 (*"Difference" is subtraction of natural numbers. |
|
44 There are no negative numbers; we have |
|
45 m - n = 0 iff m<=n and m - n = Suc(k) iff m)n. |
|
46 Also, nat_rec(0, %z w.z, m) is pred(m). *) |
|
47 |
|