author | wenzelm |
Mon, 28 Aug 2000 14:09:33 +0200 | |
changeset 9697 | c5fc121c2067 |
parent 9654 | 9754ba005b64 |
child 9883 | c1c8647af477 |
permissions | -rw-r--r-- |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/Integ/Int.thy |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
5 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
6 |
The integers as equivalence classes over nat*nat. |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
7 |
*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
8 |
|
9548 | 9 |
Int = EquivClass + ArithSimp + |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
10 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
11 |
constdefs |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
12 |
intrel :: i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
13 |
"intrel == {p:(nat*nat)*(nat*nat). |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
14 |
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
15 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
16 |
int :: i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
17 |
"int == (nat*nat)//intrel" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
18 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
19 |
int_of :: i=>i (*coercion from nat to int*) ("$# _" [80] 80) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
20 |
"$# m == intrel `` {<natify(m), 0>}" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
21 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
22 |
intify :: i=>i (*coercion from ANYTHING to int*) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
23 |
"intify(m) == if m : int then m else $#0" |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
24 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
25 |
raw_zminus :: i=>i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
26 |
"raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
27 |
|
9548 | 28 |
zminus :: i=>i ("$- _" [80] 80) |
29 |
"$- z == raw_zminus (intify(z))" |
|
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
30 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
31 |
znegative :: i=>o |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
32 |
"znegative(z) == EX x y. x<y & y:nat & <x,y>:z" |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
33 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
34 |
iszero :: i=>o |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
35 |
"iszero(z) == z = $# 0" |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
36 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
37 |
zmagnitude :: i=>i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
38 |
"zmagnitude(z) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
39 |
THE m. m : nat & ((~ znegative(z) & z = $# m) | |
9548 | 40 |
(znegative(z) & $- z = $# m))" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
41 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
42 |
raw_zmult :: [i,i]=>i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
43 |
(*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2. |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
44 |
Perhaps a "curried" or even polymorphic congruent predicate would be |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
45 |
better.*) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
46 |
"raw_zmult(z1,z2) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
47 |
UN p1:z1. UN p2:z2. split(%x1 y1. split(%x2 y2. |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
48 |
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
49 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
50 |
zmult :: [i,i]=>i (infixl "$*" 70) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
51 |
"z1 $* z2 == raw_zmult (intify(z1),intify(z2))" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
52 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
53 |
raw_zadd :: [i,i]=>i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
54 |
"raw_zadd (z1, z2) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
55 |
UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2 |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
56 |
in intrel``{<x1#+x2, y1#+y2>}" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
57 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
58 |
zadd :: [i,i]=>i (infixl "$+" 65) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
59 |
"z1 $+ z2 == raw_zadd (intify(z1),intify(z2))" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
60 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
61 |
zdiff :: [i,i]=>i (infixl "$-" 65) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
62 |
"z1 $- z2 == z1 $+ zminus(z2)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
63 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
64 |
zless :: [i,i]=>o (infixl "$<" 50) |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
65 |
"z1 $< z2 == znegative(z1 $- z2)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
66 |
|
9548 | 67 |
zle :: [i,i]=>o (infixl "$<=" 50) |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
68 |
"z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)" |
9548 | 69 |
|
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
70 |
|
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
71 |
syntax (symbols) |
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
72 |
"zmult" :: [i,i] => i (infixr "$\\<times>" 70) |
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
73 |
"zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than or equals*) |
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
74 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
75 |
end |