1 (* Title: ZF/ex/integ.thy |
1 (* Title: ZF/ex/integ.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 The integers as equivalence classes over nat*nat. |
6 The integers as equivalence classes over nat*nat. |
7 *) |
7 *) |
8 |
8 |
9 Integ = EquivClass + Arith + |
9 Integ = EquivClass + Arith + |
10 consts |
10 consts |
11 intrel,integ:: i |
11 intrel,integ:: i |
12 znat :: i=>i ("$# _" [80] 80) |
12 znat :: i=>i ("$# _" [80] 80) |
13 zminus :: i=>i ("$~ _" [80] 80) |
13 zminus :: i=>i ("$~ _" [80] 80) |
14 znegative :: i=>o |
14 znegative :: i=>o |
15 zmagnitude :: i=>i |
15 zmagnitude :: i=>i |
16 "$*" :: [i,i]=>i (infixl 70) |
16 "$*" :: [i,i]=>i (infixl 70) |
17 "$'/" :: [i,i]=>i (infixl 70) |
17 "$'/" :: [i,i]=>i (infixl 70) |
18 "$'/'/" :: [i,i]=>i (infixl 70) |
18 "$'/'/" :: [i,i]=>i (infixl 70) |
19 "$+" :: [i,i]=>i (infixl 65) |
19 "$+" :: [i,i]=>i (infixl 65) |
20 "$-" :: [i,i]=>i (infixl 65) |
20 "$-" :: [i,i]=>i (infixl 65) |
21 "$<" :: [i,i]=>o (infixl 50) |
21 "$<" :: [i,i]=>o (infixl 50) |
22 |
22 |
23 defs |
23 defs |
24 |
24 |
25 intrel_def |
25 intrel_def |
26 "intrel == {p:(nat*nat)*(nat*nat). |
26 "intrel == {p:(nat*nat)*(nat*nat). |
27 EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
27 EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
28 |
28 |
29 integ_def "integ == (nat*nat)/intrel" |
29 integ_def "integ == (nat*nat)/intrel" |
30 |
30 |
31 znat_def "$# m == intrel `` {<m,0>}" |
31 znat_def "$# m == intrel `` {<m,0>}" |
32 |
32 |
33 zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}" |
33 zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}" |
34 |
34 |
35 znegative_def |
35 znegative_def |
36 "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z" |
36 "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z" |
37 |
37 |
38 zmagnitude_def |
38 zmagnitude_def |
39 "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)" |
39 "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)" |
40 |
40 |
41 (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2. |
41 (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2. |
42 Perhaps a "curried" or even polymorphic congruent predicate would be |
42 Perhaps a "curried" or even polymorphic congruent predicate would be |
43 better.*) |
43 better.*) |
44 zadd_def |
44 zadd_def |
45 "Z1 $+ Z2 == |
45 "Z1 $+ Z2 == |
46 UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2 |
46 UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2 |
47 in intrel``{<x1#+x2, y1#+y2>}" |
47 in intrel``{<x1#+x2, y1#+y2>}" |
48 |
48 |
49 zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)" |
49 zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)" |
50 zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)" |
50 zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)" |
51 |
51 |
52 (*This illustrates the primitive form of definitions (no patterns)*) |
52 (*This illustrates the primitive form of definitions (no patterns)*) |
53 zmult_def |
53 zmult_def |
54 "Z1 $* Z2 == |
54 "Z1 $* Z2 == |
55 UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. |
55 UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. |