src/ZF/Integ/Int.thy
author paulson
Fri Sep 25 13:18:07 1998 +0200 (1998-09-25)
changeset 5561 426c1e330903
child 9333 5cacc383157a
permissions -rw-r--r--
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
     1 (*  Title:      ZF/Integ/Int.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 
     9 Int = EquivClass + Arith +
    10 consts
    11     intrel,int::      i
    12     int_of      ::      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 defs
    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     int_def   "int == (nat*nat)/intrel"
    30     
    31     int_of_def  "$# m == intrel `` {<m,0>}"
    32     
    33     zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    34     
    35     znegative_def
    36         "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    37     
    38     zmagnitude_def
    39         "zmagnitude(Z) ==
    40 	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
    41 	                   (znegative(Z) & $~ Z = $# m))"
    42     
    43     (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    44       Perhaps a "curried" or even polymorphic congruent predicate would be
    45       better.*)
    46     zadd_def
    47      "Z1 $+ Z2 == 
    48        UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
    49                            in intrel``{<x1#+x2, y1#+y2>}"
    50     
    51     zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    52     zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    53     
    54     (*This illustrates the primitive form of definitions (no patterns)*)
    55     zmult_def
    56      "Z1 $* Z2 == 
    57        UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
    58                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    59     
    60  end