equal
deleted
inserted
replaced
26 satisfy the traditional definition (theorem mod_div_equality) |
26 satisfy the traditional definition (theorem mod_div_equality) |
27 *) |
27 *) |
28 defs |
28 defs |
29 |
29 |
30 mod_def "m mod n == wfrec (trancl pred_nat) |
30 mod_def "m mod n == wfrec (trancl pred_nat) |
31 (%f j. if j<n then j else f (j-n)) m" |
31 (%f j. if j<n | n=0 then j else f (j-n)) m" |
32 |
32 |
33 div_def "m div n == wfrec (trancl pred_nat) |
33 div_def "m div n == wfrec (trancl pred_nat) |
34 (%f j. if j<n then 0 else Suc (f (j-n))) m" |
34 (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" |
35 |
35 |
36 (*The definition of dvd is polymorphic!*) |
36 (*The definition of dvd is polymorphic!*) |
37 dvd_def "m dvd n == EX k. n = m*k" |
37 dvd_def "m dvd n == EX k. n = m*k" |
38 |
38 |
39 end |
39 end |