equal
deleted
inserted
replaced
18 defs |
18 defs |
19 pred_def "pred(m) == nat_rec m 0 (%n r.n)" |
19 pred_def "pred(m) == nat_rec m 0 (%n r.n)" |
20 add_def "m+n == nat_rec m n (%u v. Suc(v))" |
20 add_def "m+n == nat_rec m n (%u v. Suc(v))" |
21 diff_def "m-n == nat_rec n m (%u v. pred(v))" |
21 diff_def "m-n == nat_rec n m (%u v. pred(v))" |
22 mult_def "m*n == nat_rec m 0 (%u v. n + v)" |
22 mult_def "m*n == nat_rec m 0 (%u v. n + v)" |
23 mod_def "m mod n == wfrec (trancl pred_nat) m (%j f.(if (j<n) j (f (j-n))))" |
23 mod_def "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))" |
24 div_def "m div n == wfrec (trancl pred_nat) m (%j f.(if (j<n) 0 (Suc (f (j-n)))))" |
24 div_def "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))" |
25 end |
25 end |
26 |
26 |
27 (*"Difference" is subtraction of natural numbers. |
27 (*"Difference" is subtraction of natural numbers. |
28 There are no negative numbers; we have |
28 There are no negative numbers; we have |
29 m - n = 0 iff m<=n and m - n = Suc(k) iff m>n. |
29 m - n = 0 iff m<=n and m - n = Suc(k) iff m>n. |