| author | nipkow |
| Wed, 16 Oct 1996 10:37:17 +0200 | |
| changeset 2099 | c5f004bfcbab |
| parent 1824 | 44254696843a |
| child 2681 | 93ed51a91622 |
| permissions | -rw-r--r-- |
| 923 | 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 |
||
11 |
instance |
|
12 |
nat :: {plus, minus, times}
|
|
13 |
||
14 |
consts |
|
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
972
diff
changeset
|
15 |
pred :: nat => nat |
|
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
972
diff
changeset
|
16 |
div, mod :: [nat, nat] => nat (infixl 70) |
| 923 | 17 |
|
18 |
defs |
|
| 2099 | 19 |
pred_def "pred(m) == case m of 0 => 0 | Suc n => n" |
| 1824 | 20 |
add_def "m+n == nat_rec n (%u v. Suc(v)) m" |
21 |
diff_def "m-n == nat_rec m (%u v. pred(v)) n" |
|
22 |
mult_def "m*n == nat_rec 0 (%u v. n + v) m" |
|
| 1796 | 23 |
|
24 |
mod_def "m mod n == wfrec (trancl pred_nat) |
|
| 1475 | 25 |
(%f j. if j<n then j else f (j-n)) m" |
| 1796 | 26 |
div_def "m div n == wfrec (trancl pred_nat) |
| 1475 | 27 |
(%f j. if j<n then 0 else Suc (f (j-n))) m" |
| 923 | 28 |
end |
29 |
||
30 |
(*"Difference" is subtraction of natural numbers. |
|
31 |
There are no negative numbers; we have |
|
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
32 |
m - n = 0 iff m<=n and m - n = Suc(k) iff m)n. |
| 1824 | 33 |
Also, nat_rec(0, %z w.z, m) is pred(m). *) |
| 923 | 34 |