author | paulson |
Mon, 26 May 1997 12:38:29 +0200 | |
changeset 3342 | ec3b55fcb165 |
parent 3308 | da002cef7090 |
child 3366 | 2402c6ab1561 |
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) |
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3235
diff
changeset
|
17 |
(* size of a datatype value; overloaded *) |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3235
diff
changeset
|
18 |
size :: 'a => nat |
923 | 19 |
|
20 |
defs |
|
2099 | 21 |
pred_def "pred(m) == case m of 0 => 0 | Suc n => n" |
1796 | 22 |
|
23 |
mod_def "m mod n == wfrec (trancl pred_nat) |
|
1475 | 24 |
(%f j. if j<n then j else f (j-n)) m" |
1796 | 25 |
div_def "m div n == wfrec (trancl pred_nat) |
1475 | 26 |
(%f j. if j<n then 0 else Suc (f (j-n))) m" |
2681
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
27 |
|
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
28 |
primrec "op +" nat |
2887 | 29 |
"0 + n = n" |
30 |
"Suc m + n = Suc(m + n)" |
|
2681
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
31 |
|
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
32 |
primrec "op -" nat |
3235
351565b7321b
The diff laws must be named: we do "Delsimps [diff_Suc];"
paulson
parents:
2887
diff
changeset
|
33 |
diff_0 "m - 0 = m" |
351565b7321b
The diff laws must be named: we do "Delsimps [diff_Suc];"
paulson
parents:
2887
diff
changeset
|
34 |
diff_Suc "m - Suc n = pred(m - n)" |
2681
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
35 |
|
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
36 |
primrec "op *" nat |
2887 | 37 |
"0 * n = 0" |
38 |
"Suc m * n = n + (m * n)" |
|
2681
93ed51a91622
definitions of +,-,* replaced by primrec definitions
pusch
parents:
2099
diff
changeset
|
39 |
|
923 | 40 |
end |