equal
deleted
inserted
replaced
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 |
|
15 pred :: "nat => nat" |
|
16 div, mod :: "[nat, nat] => nat" (infixl 70) |
|
17 |
|
18 defs |
|
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))" |
|
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)" |
|
23 mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))" |
|
24 div_def "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))" |
|
25 end |
|
26 |
|
27 (*"Difference" is subtraction of natural numbers. |
|
28 There are no negative numbers; we have |
|
29 m - n = 0 iff m<=n and m - n = Suc(k) iff m>n. |
|
30 Also, nat_rec(m, 0, %z w.z) is pred(m). *) |
|
31 |
|