src/ZF/Integ/Int.thy
author paulson
Thu Aug 10 11:27:34 2000 +0200 (2000-08-10)
changeset 9570 e16e168984e1
parent 9548 15bee2731e43
child 9578 ab26d6c8ebfe
permissions -rw-r--r--
installation of cancellation simprocs for the integers
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@9548
     9
Int = EquivClass + ArithSimp +
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@9548
    28
  zminus :: i=>i                                 ("$- _" [80] 80)
paulson@9548
    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@9570
    33
paulson@9570
    34
  iszero      ::      i=>o
paulson@9570
    35
    "iszero(z) == z = $# 0"
paulson@9570
    36
    
paulson@9496
    37
  zmagnitude  ::      i=>i
paulson@9496
    38
    "zmagnitude(z) ==
paulson@9496
    39
     THE m. m : nat & ((~ znegative(z) & z = $# m) |
paulson@9548
    40
		       (znegative(z) & $- z = $# m))"
paulson@9496
    41
paulson@9496
    42
  raw_zmult   ::      [i,i]=>i
paulson@9496
    43
    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
paulson@5561
    44
      Perhaps a "curried" or even polymorphic congruent predicate would be
paulson@5561
    45
      better.*)
paulson@9496
    46
     "raw_zmult(z1,z2) == 
paulson@9496
    47
       UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
paulson@9496
    48
                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
paulson@9496
    49
paulson@9496
    50
  zmult       ::      [i,i]=>i      (infixl "$*" 70)
paulson@9496
    51
     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
paulson@9496
    52
paulson@9496
    53
  raw_zadd    ::      [i,i]=>i
paulson@9496
    54
     "raw_zadd (z1, z2) == 
paulson@9496
    55
       UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
paulson@5561
    56
                           in intrel``{<x1#+x2, y1#+y2>}"
paulson@9496
    57
paulson@9496
    58
  zadd        ::      [i,i]=>i      (infixl "$+" 65)
paulson@9496
    59
     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
paulson@9496
    60
paulson@9496
    61
  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
paulson@9496
    62
     "z1 $- z2 == z1 $+ zminus(z2)"
paulson@9496
    63
paulson@9496
    64
  zless        ::      [i,i]=>o      (infixl "$<" 50)
paulson@9496
    65
     "z1 $< z2 == znegative(z1 $- z2)"
paulson@9496
    66
  
paulson@9548
    67
  zle          ::      [i,i]=>o      (infixl "$<=" 50)
paulson@9570
    68
     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
paulson@9548
    69
  
paulson@9496
    70
(*div and mod await definitions!*)
paulson@9496
    71
consts
paulson@9496
    72
  "$'/"       ::      [i,i]=>i      (infixl 70) 
paulson@9496
    73
paulson@9496
    74
  "$'/'/"     ::      [i,i]=>i      (infixl 70)
paulson@5561
    75
    
paulson@9496
    76
end