|
1 (* Title: ZF/ex/integ.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The integers as equivalence classes over nat*nat. |
|
7 *) |
|
8 |
|
9 Integ = Equiv + Arith + |
|
10 consts |
|
11 intrel,integ:: "i" |
|
12 znat :: "i=>i" ("$# _" [80] 80) |
|
13 zminus :: "i=>i" ("$~ _" [80] 80) |
|
14 znegative :: "i=>o" |
|
15 zmagnitude :: "i=>i" |
|
16 "$*" :: "[i,i]=>i" (infixl 70) |
|
17 "$'/" :: "[i,i]=>i" (infixl 70) |
|
18 "$'/'/" :: "[i,i]=>i" (infixl 70) |
|
19 "$+" :: "[i,i]=>i" (infixl 65) |
|
20 "$-" :: "[i,i]=>i" (infixl 65) |
|
21 "$<" :: "[i,i]=>o" (infixl 50) |
|
22 |
|
23 rules |
|
24 |
|
25 intrel_def |
|
26 "intrel == {p:(nat*nat)*(nat*nat). \ |
|
27 \ EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
|
28 |
|
29 integ_def "integ == (nat*nat)/intrel" |
|
30 |
|
31 znat_def "$# m == intrel `` {<m,0>}" |
|
32 |
|
33 zminus_def "$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)" |
|
34 |
|
35 znegative_def |
|
36 "znegative(Z) == EX x y. x:y & y:nat & <x,y>:Z" |
|
37 |
|
38 zmagnitude_def |
|
39 "zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)" |
|
40 |
|
41 zadd_def |
|
42 "Z1 $+ Z2 == \ |
|
43 \ UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. \ |
|
44 \ intrel``{<x1#+x2, y1#+y2>}, p2), p1)" |
|
45 |
|
46 zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)" |
|
47 zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)" |
|
48 |
|
49 zmult_def |
|
50 "Z1 $* Z2 == \ |
|
51 \ UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. \ |
|
52 \ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)" |
|
53 |
|
54 end |