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