author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 1478 | 2b8c2a7547ab |
child 5507 | 2fd99b2d41e1 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/integ.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
The integers as equivalence classes over nat*nat. |
|
7 |
*) |
|
8 |
||
532
851df239ac8b
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents:
29
diff
changeset
|
9 |
Integ = EquivClass + Arith + |
0 | 10 |
consts |
1401 | 11 |
intrel,integ:: i |
1478 | 12 |
znat :: i=>i ("$# _" [80] 80) |
13 |
zminus :: i=>i ("$~ _" [80] 80) |
|
14 |
znegative :: i=>o |
|
15 |
zmagnitude :: i=>i |
|
1401 | 16 |
"$*" :: [i,i]=>i (infixl 70) |
17 |
"$'/" :: [i,i]=>i (infixl 70) |
|
18 |
"$'/'/" :: [i,i]=>i (infixl 70) |
|
1478 | 19 |
"$+" :: [i,i]=>i (infixl 65) |
1401 | 20 |
"$-" :: [i,i]=>i (infixl 65) |
1478 | 21 |
"$<" :: [i,i]=>o (infixl 50) |
0 | 22 |
|
753 | 23 |
defs |
0 | 24 |
|
25 |
intrel_def |
|
1478 | 26 |
"intrel == {p:(nat*nat)*(nat*nat). |
1155 | 27 |
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
0 | 28 |
|
29 |
integ_def "integ == (nat*nat)/intrel" |
|
30 |
||
1478 | 31 |
znat_def "$# m == intrel `` {<m,0>}" |
0 | 32 |
|
1478 | 33 |
zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}" |
0 | 34 |
|
35 |
znegative_def |
|
1478 | 36 |
"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z" |
0 | 37 |
|
38 |
zmagnitude_def |
|
1478 | 39 |
"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)" |
0 | 40 |
|
1110
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
753
diff
changeset
|
41 |
(*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2. |
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
753
diff
changeset
|
42 |
Perhaps a "curried" or even polymorphic congruent predicate would be |
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
753
diff
changeset
|
43 |
better.*) |
0 | 44 |
zadd_def |
1155 | 45 |
"Z1 $+ Z2 == |
46 |
UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2 |
|
47 |
in intrel``{<x1#+x2, y1#+y2>}" |
|
0 | 48 |
|
49 |
zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)" |
|
1478 | 50 |
zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)" |
0 | 51 |
|
1110
756aa2e81f6e
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
753
diff
changeset
|
52 |
(*This illustrates the primitive form of definitions (no patterns)*) |
0 | 53 |
zmult_def |
1155 | 54 |
"Z1 $* Z2 == |
55 |
UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. |
|
56 |
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)" |
|
0 | 57 |
|
58 |
end |