13577
|
1 |
(* Title: Integ/Int.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Type "int" is a linear order
|
|
7 |
*)
|
|
8 |
|
|
9 |
theory Int = IntDef
|
|
10 |
files ("int.ML"):
|
|
11 |
|
|
12 |
instance int :: order
|
|
13 |
proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
|
|
14 |
|
|
15 |
instance int :: plus_ac0
|
|
16 |
proof qed (rule zadd_commute zadd_assoc zadd_0)+
|
|
17 |
|
|
18 |
instance int :: linorder
|
|
19 |
proof qed (rule zle_linear)
|
|
20 |
|
|
21 |
constdefs
|
|
22 |
nat :: "int => nat"
|
|
23 |
"nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
|
|
24 |
|
|
25 |
defs (overloaded)
|
|
26 |
zabs_def: "abs(i::int) == if i < 0 then -i else i"
|
|
27 |
|
|
28 |
use "int.ML"
|
|
29 |
|
|
30 |
end
|