author  lcp 
Tue, 16 Aug 1994 18:58:42 +0200  
changeset 532  851df239ac8b 
parent 29  4ec9b266ccd1 
child 753  ec86863e87c8 
permissions  rwrr 
0  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 

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 
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 

29
4ec9b266ccd1
Modification of examples for the new operators, < and le.
lcp
parents:
0
diff
changeset

36 
"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z" 
0  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 