| author | paulson |
| Mon, 22 Oct 2001 11:54:22 +0200 | |
| changeset 11868 | 56db9f3a6b3e |
| parent 11451 | 8abfb4f7bd02 |
| child 13575 | ecb6ecd9af13 |
| permissions | -rw-r--r-- |
| paulson@5562 | 1 |
(* Title: Integ/Int.thy |
| paulson@5562 | 2 |
ID: $Id$ |
| paulson@5562 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| paulson@5562 | 4 |
Copyright 1998 University of Cambridge |
| paulson@5562 | 5 |
|
| paulson@5562 | 6 |
Type "int" is a linear order |
| paulson@5562 | 7 |
*) |
| paulson@5562 | 8 |
|
| paulson@11451 | 9 |
Int = IntDef + |
| paulson@5562 | 10 |
|
| paulson@5562 | 11 |
instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) |
| paulson@11868 | 12 |
instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_0) |
| paulson@5562 | 13 |
instance int :: linorder (zle_linear) |
| paulson@5562 | 14 |
|
| paulson@5562 | 15 |
constdefs |
| paulson@5562 | 16 |
nat :: int => nat |
| paulson@11451 | 17 |
"nat(Z) == if neg Z then 0 else (THE m. Z = int m)" |
| paulson@5562 | 18 |
|
| nipkow@9214 | 19 |
defs |
| nipkow@9214 | 20 |
zabs_def "abs(i::int) == if i < 0 then -i else i" |
| nipkow@9214 | 21 |
|
| paulson@5562 | 22 |
end |