src/ZF/Integ/Int.thy
author paulson
Wed Aug 02 16:07:32 2000 +0200 (2000-08-02)
changeset 9496 07e33cac5d9c
parent 9333 5cacc383157a
child 9548 15bee2731e43
permissions -rw-r--r--
coercion "intify" to remove type constraints from integer algebraic laws
     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 
    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   zmagnitude  ::      i=>i
    35     "zmagnitude(z) ==
    36      THE m. m : nat & ((~ znegative(z) & z = $# m) |
    37 		       (znegative(z) & $~ z = $# m))"
    38 
    39   raw_zmult   ::      [i,i]=>i
    40     (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    41       Perhaps a "curried" or even polymorphic congruent predicate would be
    42       better.*)
    43      "raw_zmult(z1,z2) == 
    44        UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
    45                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    46 
    47   zmult       ::      [i,i]=>i      (infixl "$*" 70)
    48      "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    49 
    50   raw_zadd    ::      [i,i]=>i
    51      "raw_zadd (z1, z2) == 
    52        UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
    53                            in intrel``{<x1#+x2, y1#+y2>}"
    54 
    55   zadd        ::      [i,i]=>i      (infixl "$+" 65)
    56      "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    57 
    58   zdiff        ::      [i,i]=>i      (infixl "$-" 65)
    59      "z1 $- z2 == z1 $+ zminus(z2)"
    60 
    61   zless        ::      [i,i]=>o      (infixl "$<" 50)
    62      "z1 $< z2 == znegative(z1 $- z2)"
    63   
    64 (*div and mod await definitions!*)
    65 consts
    66   "$'/"       ::      [i,i]=>i      (infixl 70) 
    67 
    68   "$'/'/"     ::      [i,i]=>i      (infixl 70)
    69     
    70 end