src/ZF/Integ/Int.thy
changeset 5561 426c1e330903
child 9333 5cacc383157a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Integ/Int.thy	Fri Sep 25 13:18:07 1998 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +(*  Title:      ZF/Integ/Int.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +The integers as equivalence classes over nat*nat.
    1.10 +*)
    1.11 +
    1.12 +Int = EquivClass + Arith +
    1.13 +consts
    1.14 +    intrel,int::      i
    1.15 +    int_of      ::      i=>i            ("$# _" [80] 80)
    1.16 +    zminus      ::      i=>i            ("$~ _" [80] 80)
    1.17 +    znegative   ::      i=>o
    1.18 +    zmagnitude  ::      i=>i
    1.19 +    "$*"        ::      [i,i]=>i      (infixl 70)
    1.20 +    "$'/"       ::      [i,i]=>i      (infixl 70) 
    1.21 +    "$'/'/"     ::      [i,i]=>i      (infixl 70)
    1.22 +    "$+"        ::      [i,i]=>i      (infixl 65)
    1.23 +    "$-"        ::      [i,i]=>i      (infixl 65)
    1.24 +    "$<"        ::      [i,i]=>o        (infixl 50)
    1.25 +
    1.26 +defs
    1.27 +
    1.28 +    intrel_def
    1.29 +     "intrel == {p:(nat*nat)*(nat*nat).                 
    1.30 +        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.31 +
    1.32 +    int_def   "int == (nat*nat)/intrel"
    1.33 +    
    1.34 +    int_of_def  "$# m == intrel `` {<m,0>}"
    1.35 +    
    1.36 +    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    1.37 +    
    1.38 +    znegative_def
    1.39 +        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    1.40 +    
    1.41 +    zmagnitude_def
    1.42 +        "zmagnitude(Z) ==
    1.43 +	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
    1.44 +	                   (znegative(Z) & $~ Z = $# m))"
    1.45 +    
    1.46 +    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    1.47 +      Perhaps a "curried" or even polymorphic congruent predicate would be
    1.48 +      better.*)
    1.49 +    zadd_def
    1.50 +     "Z1 $+ Z2 == 
    1.51 +       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
    1.52 +                           in intrel``{<x1#+x2, y1#+y2>}"
    1.53 +    
    1.54 +    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    1.55 +    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    1.56 +    
    1.57 +    (*This illustrates the primitive form of definitions (no patterns)*)
    1.58 +    zmult_def
    1.59 +     "Z1 $* Z2 == 
    1.60 +       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
    1.61 +                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    1.62 +    
    1.63 + end