| author | lcp |
| Fri, 19 Aug 1994 11:10:56 +0200 | |
| changeset 116 | ab4328bbff70 |
| parent 77 | d64593bb95d3 |
| child 145 | a9f7ff3a464c |
| permissions | -rw-r--r-- |
| 0 | 1 |
(* Title: HOL/arith.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Arithmetic operators and their definitions |
|
7 |
*) |
|
8 |
||
9 |
Arith = Nat + |
|
10 |
arities nat::plus |
|
11 |
nat::minus |
|
12 |
nat::times |
|
13 |
consts |
|
| 21 | 14 |
pred :: "nat => nat" |
| 0 | 15 |
div,mod :: "[nat,nat]=>nat" (infixl 70) |
16 |
rules |
|
| 21 | 17 |
pred_def "pred(m) == nat_rec(m, 0, %n r.n)" |
|
77
d64593bb95d3
HOL/Arith: definition of diff now uses pred, not nat_rec
lcp
parents:
21
diff
changeset
|
18 |
add_def "m+n == nat_rec(m, n, %u v. Suc(v))" |
|
d64593bb95d3
HOL/Arith: definition of diff now uses pred, not nat_rec
lcp
parents:
21
diff
changeset
|
19 |
diff_def "m-n == nat_rec(n, m, %u v. pred(v))" |
| 0 | 20 |
mult_def "m*n == nat_rec(m, 0, %u v. n + v)" |
21 |
mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))" |
|
22 |
div_def "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))" |
|
23 |
end |
|
24 |
||
25 |
(*"Difference" is subtraction of natural numbers. |
|
26 |
There are no negative numbers; we have |
|
27 |
m - n = 0 iff m<=n and m - n = Suc(k) iff m>n. |
|
28 |
Also, nat_rec(m, 0, %z w.z) is pred(m). *) |