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
paulson@5561
     1
(*  Title:      ZF/Integ/Int.thy
paulson@5561
     2
    ID:         $Id$
paulson@5561
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5561
     4
    Copyright   1993  University of Cambridge
paulson@5561
     5
paulson@5561
     6
The integers as equivalence classes over nat*nat.
paulson@5561
     7
*)
paulson@5561
     8
paulson@5561
     9
Int = EquivClass + Arith +
paulson@9496
    10
paulson@9496
    11
constdefs
paulson@9496
    12
  intrel :: i
paulson@9496
    13
    "intrel == {p:(nat*nat)*(nat*nat).                 
paulson@9496
    14
                EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
paulson@5561
    15
paulson@9496
    16
  int :: i
paulson@9496
    17
    "int == (nat*nat)//intrel"  
paulson@9496
    18
paulson@9496
    19
  int_of :: i=>i (*coercion from nat to int*)    ("$# _" [80] 80)
paulson@9496
    20
    "$# m == intrel `` {<natify(m), 0>}"
paulson@9496
    21
paulson@9496
    22
  intify :: i=>i (*coercion from ANYTHING to int*) 
paulson@9496
    23
    "intify(m) == if m : int then m else $#0"
paulson@5561
    24
paulson@9496
    25
  raw_zminus :: i=>i
paulson@9496
    26
    "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
paulson@9496
    27
paulson@9496
    28
  zminus :: i=>i                                 ("$~ _" [80] 80)
paulson@9496
    29
    "$~ z == raw_zminus (intify(z))"
paulson@5561
    30
paulson@9496
    31
  znegative   ::      i=>o
paulson@9496
    32
    "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
paulson@9496
    33
  
paulson@9496
    34
  zmagnitude  ::      i=>i
paulson@9496
    35
    "zmagnitude(z) ==
paulson@9496
    36
     THE m. m : nat & ((~ znegative(z) & z = $# m) |
paulson@9496
    37
		       (znegative(z) & $~ z = $# m))"
paulson@9496
    38
paulson@9496
    39
  raw_zmult   ::      [i,i]=>i
paulson@9496
    40
    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
paulson@5561
    41
      Perhaps a "curried" or even polymorphic congruent predicate would be
paulson@5561
    42
      better.*)
paulson@9496
    43
     "raw_zmult(z1,z2) == 
paulson@9496
    44
       UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
paulson@9496
    45
                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
paulson@9496
    46
paulson@9496
    47
  zmult       ::      [i,i]=>i      (infixl "$*" 70)
paulson@9496
    48
     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
paulson@9496
    49
paulson@9496
    50
  raw_zadd    ::      [i,i]=>i
paulson@9496
    51
     "raw_zadd (z1, z2) == 
paulson@9496
    52
       UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
paulson@5561
    53
                           in intrel``{<x1#+x2, y1#+y2>}"
paulson@9496
    54
paulson@9496
    55
  zadd        ::      [i,i]=>i      (infixl "$+" 65)
paulson@9496
    56
     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
paulson@9496
    57
paulson@9496
    58
  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
paulson@9496
    59
     "z1 $- z2 == z1 $+ zminus(z2)"
paulson@9496
    60
paulson@9496
    61
  zless        ::      [i,i]=>o      (infixl "$<" 50)
paulson@9496
    62
     "z1 $< z2 == znegative(z1 $- z2)"
paulson@9496
    63
  
paulson@9496
    64
(*div and mod await definitions!*)
paulson@9496
    65
consts
paulson@9496
    66
  "$'/"       ::      [i,i]=>i      (infixl 70) 
paulson@9496
    67
paulson@9496
    68
  "$'/'/"     ::      [i,i]=>i      (infixl 70)
paulson@5561
    69
    
paulson@9496
    70
end