src/ZF/Integ/Int.thy
author paulson
Fri Aug 11 13:27:17 2000 +0200 (2000-08-11)
changeset 9578 ab26d6c8ebfe
parent 9570 e16e168984e1
child 9654 9754ba005b64
permissions -rw-r--r--
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
     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 + ArithSimp +
    10 
    11 constdefs
    12   intrel :: i
    13     "intrel == {p:(nat*nat)*(nat*nat).                 
    14                 EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    15 
    16   int :: i
    17     "int == (nat*nat)//intrel"  
    18 
    19   int_of :: i=>i (*coercion from nat to int*)    ("$# _" [80] 80)
    20     "$# m == intrel `` {<natify(m), 0>}"
    21 
    22   intify :: i=>i (*coercion from ANYTHING to int*) 
    23     "intify(m) == if m : int then m else $#0"
    24 
    25   raw_zminus :: i=>i
    26     "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
    27 
    28   zminus :: i=>i                                 ("$- _" [80] 80)
    29     "$- z == raw_zminus (intify(z))"
    30 
    31   znegative   ::      i=>o
    32     "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
    33 
    34   iszero      ::      i=>o
    35     "iszero(z) == z = $# 0"
    36     
    37   zmagnitude  ::      i=>i
    38     "zmagnitude(z) ==
    39      THE m. m : nat & ((~ znegative(z) & z = $# m) |
    40 		       (znegative(z) & $- z = $# m))"
    41 
    42   raw_zmult   ::      [i,i]=>i
    43     (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    44       Perhaps a "curried" or even polymorphic congruent predicate would be
    45       better.*)
    46      "raw_zmult(z1,z2) == 
    47        UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
    48                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    49 
    50   zmult       ::      [i,i]=>i      (infixl "$*" 70)
    51      "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    52 
    53   raw_zadd    ::      [i,i]=>i
    54      "raw_zadd (z1, z2) == 
    55        UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
    56                            in intrel``{<x1#+x2, y1#+y2>}"
    57 
    58   zadd        ::      [i,i]=>i      (infixl "$+" 65)
    59      "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    60 
    61   zdiff        ::      [i,i]=>i      (infixl "$-" 65)
    62      "z1 $- z2 == z1 $+ zminus(z2)"
    63 
    64   zless        ::      [i,i]=>o      (infixl "$<" 50)
    65      "z1 $< z2 == znegative(z1 $- z2)"
    66   
    67   zle          ::      [i,i]=>o      (infixl "$<=" 50)
    68      "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    69   
    70 end