src/ZF/Integ/Int.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 11321 01cbbf33779b
child 13560 d9651081578b
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
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@9883
    37
  raw_nat_of  :: i => i
paulson@9883
    38
  "raw_nat_of(z) == if znegative(z) then 0
paulson@9883
    39
                    else (THE m. m: nat & z = int_of(m))"
paulson@9883
    40
paulson@9883
    41
  nat_of  :: i => i
paulson@9883
    42
  "nat_of(z) == raw_nat_of (intify(z))"
paulson@9883
    43
paulson@9883
    44
  (*could be replaced by an absolute value function from int to int?*)
paulson@9496
    45
  zmagnitude  ::      i=>i
paulson@9496
    46
    "zmagnitude(z) ==
paulson@9496
    47
     THE m. m : nat & ((~ znegative(z) & z = $# m) |
paulson@9548
    48
		       (znegative(z) & $- z = $# m))"
paulson@9496
    49
paulson@9496
    50
  raw_zmult   ::      [i,i]=>i
paulson@9496
    51
    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
paulson@5561
    52
      Perhaps a "curried" or even polymorphic congruent predicate would be
paulson@5561
    53
      better.*)
paulson@9496
    54
     "raw_zmult(z1,z2) == 
paulson@9496
    55
       UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
paulson@9496
    56
                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
paulson@9496
    57
paulson@9496
    58
  zmult       ::      [i,i]=>i      (infixl "$*" 70)
paulson@9496
    59
     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
paulson@9496
    60
paulson@9496
    61
  raw_zadd    ::      [i,i]=>i
paulson@9496
    62
     "raw_zadd (z1, z2) == 
paulson@9496
    63
       UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
paulson@5561
    64
                           in intrel``{<x1#+x2, y1#+y2>}"
paulson@9496
    65
paulson@9496
    66
  zadd        ::      [i,i]=>i      (infixl "$+" 65)
paulson@9496
    67
     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
paulson@9496
    68
paulson@9496
    69
  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
paulson@9496
    70
     "z1 $- z2 == z1 $+ zminus(z2)"
paulson@9496
    71
paulson@9496
    72
  zless        ::      [i,i]=>o      (infixl "$<" 50)
paulson@9496
    73
     "z1 $< z2 == znegative(z1 $- z2)"
paulson@9496
    74
  
paulson@9548
    75
  zle          ::      [i,i]=>o      (infixl "$<=" 50)
paulson@9570
    76
     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
paulson@9548
    77
  
paulson@9654
    78
wenzelm@12114
    79
syntax (xsymbols)
paulson@11321
    80
  "zmult"     :: [i,i] => i          (infixl "$\\<times>" 70)
paulson@11321
    81
  "zle"       :: [i,i] => o          (infixl "$\\<le>" 50)  (*less than / equals*)
paulson@9654
    82
wenzelm@9964
    83
syntax (HTML output)
paulson@11321
    84
  "zmult"     :: [i,i] => i          (infixl "$\\<times>" 70)
paulson@9496
    85
end