src/ZF/ex/Integ.thy
author lcp
Tue, 16 Aug 1994 18:58:42 +0200
changeset 532 851df239ac8b
parent 29 4ec9b266ccd1
child 753 ec86863e87c8
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/integ.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
The integers as equivalence classes over nat*nat.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
532
851df239ac8b ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents: 29
diff changeset
     9
Integ = EquivClass + Arith +
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    intrel,integ::      "i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    znat	::	"i=>i"		("$# _" [80] 80)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
    zminus	::	"i=>i"		("$~ _" [80] 80)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
    znegative	::	"i=>o"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
    zmagnitude	::	"i=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "$*"        ::      "[i,i]=>i"      (infixl 70)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    "$'/"       ::      "[i,i]=>i"      (infixl 70) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
    "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
    "$+"	::      "[i,i]=>i"      (infixl 65)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    "$-"        ::      "[i,i]=>i"      (infixl 65)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    "$<"	:: 	"[i,i]=>o"  	(infixl 50)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    intrel_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
     "intrel == {p:(nat*nat)*(nat*nat). 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
\        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
    integ_def   "integ == (nat*nat)/intrel"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    znat_def	"$# m == intrel `` {<m,0>}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    zminus_def	"$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
    zmagnitude_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
	"zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
    zadd_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
     "Z1 $+ Z2 == \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
\       UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. 		\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
\                                         intrel``{<x1#+x2, y1#+y2>}, p2), p1)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    zmult_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
     "Z1 $* Z2 == \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2. 	\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
 end