src/ZF/Integ/Int.thy
changeset 9496 07e33cac5d9c
parent 9333 5cacc383157a
child 9548 15bee2731e43
     1.1 --- a/src/ZF/Integ/Int.thy	Wed Aug 02 16:06:54 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.thy	Wed Aug 02 16:07:32 2000 +0200
     1.3 @@ -7,54 +7,64 @@
     1.4  *)
     1.5  
     1.6  Int = EquivClass + Arith +
     1.7 -consts
     1.8 -    intrel,int::      i
     1.9 -    int_of      ::      i=>i            ("$# _" [80] 80)
    1.10 -    zminus      ::      i=>i            ("$~ _" [80] 80)
    1.11 -    znegative   ::      i=>o
    1.12 -    zmagnitude  ::      i=>i
    1.13 -    "$*"        ::      [i,i]=>i      (infixl 70)
    1.14 -    "$'/"       ::      [i,i]=>i      (infixl 70) 
    1.15 -    "$'/'/"     ::      [i,i]=>i      (infixl 70)
    1.16 -    "$+"        ::      [i,i]=>i      (infixl 65)
    1.17 -    "$-"        ::      [i,i]=>i      (infixl 65)
    1.18 -    "$<"        ::      [i,i]=>o        (infixl 50)
    1.19 +
    1.20 +constdefs
    1.21 +  intrel :: i
    1.22 +    "intrel == {p:(nat*nat)*(nat*nat).                 
    1.23 +                EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.24  
    1.25 -defs
    1.26 +  int :: i
    1.27 +    "int == (nat*nat)//intrel"  
    1.28 +
    1.29 +  int_of :: i=>i (*coercion from nat to int*)    ("$# _" [80] 80)
    1.30 +    "$# m == intrel `` {<natify(m), 0>}"
    1.31 +
    1.32 +  intify :: i=>i (*coercion from ANYTHING to int*) 
    1.33 +    "intify(m) == if m : int then m else $#0"
    1.34  
    1.35 -    intrel_def
    1.36 -     "intrel == {p:(nat*nat)*(nat*nat).                 
    1.37 -        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.38 +  raw_zminus :: i=>i
    1.39 +    "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
    1.40 +
    1.41 +  zminus :: i=>i                                 ("$~ _" [80] 80)
    1.42 +    "$~ z == raw_zminus (intify(z))"
    1.43  
    1.44 -    int_def   "int == (nat*nat)//intrel"
    1.45 -    
    1.46 -    int_of_def  "$# m == intrel `` {<m,0>}"
    1.47 -    
    1.48 -    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    1.49 -    
    1.50 -    znegative_def
    1.51 -        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    1.52 -    
    1.53 -    zmagnitude_def
    1.54 -        "zmagnitude(Z) ==
    1.55 -	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
    1.56 -	                   (znegative(Z) & $~ Z = $# m))"
    1.57 -    
    1.58 -    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    1.59 +  znegative   ::      i=>o
    1.60 +    "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
    1.61 +  
    1.62 +  zmagnitude  ::      i=>i
    1.63 +    "zmagnitude(z) ==
    1.64 +     THE m. m : nat & ((~ znegative(z) & z = $# m) |
    1.65 +		       (znegative(z) & $~ z = $# m))"
    1.66 +
    1.67 +  raw_zmult   ::      [i,i]=>i
    1.68 +    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    1.69        Perhaps a "curried" or even polymorphic congruent predicate would be
    1.70        better.*)
    1.71 -    zadd_def
    1.72 -     "Z1 $+ Z2 == 
    1.73 -       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
    1.74 +     "raw_zmult(z1,z2) == 
    1.75 +       UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
    1.76 +                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    1.77 +
    1.78 +  zmult       ::      [i,i]=>i      (infixl "$*" 70)
    1.79 +     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    1.80 +
    1.81 +  raw_zadd    ::      [i,i]=>i
    1.82 +     "raw_zadd (z1, z2) == 
    1.83 +       UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
    1.84                             in intrel``{<x1#+x2, y1#+y2>}"
    1.85 -    
    1.86 -    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    1.87 -    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    1.88 +
    1.89 +  zadd        ::      [i,i]=>i      (infixl "$+" 65)
    1.90 +     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    1.91 +
    1.92 +  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
    1.93 +     "z1 $- z2 == z1 $+ zminus(z2)"
    1.94 +
    1.95 +  zless        ::      [i,i]=>o      (infixl "$<" 50)
    1.96 +     "z1 $< z2 == znegative(z1 $- z2)"
    1.97 +  
    1.98 +(*div and mod await definitions!*)
    1.99 +consts
   1.100 +  "$'/"       ::      [i,i]=>i      (infixl 70) 
   1.101 +
   1.102 +  "$'/'/"     ::      [i,i]=>i      (infixl 70)
   1.103      
   1.104 -    (*This illustrates the primitive form of definitions (no patterns)*)
   1.105 -    zmult_def
   1.106 -     "Z1 $* Z2 == 
   1.107 -       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
   1.108 -                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
   1.109 -    
   1.110 - end
   1.111 +end