home *** CD-ROM | disk | FTP | other *** search
/ GEMini Atari / GEMini_Atari_CD-ROM_Walnut_Creek_December_1993.iso / files / language / isetl / group.t < prev    next >
Encoding:
Text File  |  1987-08-20  |  821 b   |  40 lines
  1. closed :=    func(S, op);
  2.         return forall a, b in S| a .op b in S;
  3.         end;
  4.  
  5. assoc :=    func(S, op);
  6.         return forall a, b, c in S|
  7.                   a .op (b .op c) = (a .op b) .op c;
  8.         end;
  9.  
  10. id :=        func(S, op);
  11.         return arb({ i: i in S|
  12.                 forall x in S|
  13.                     i .op x = x and x .op i = x});
  14.         end;
  15.  
  16. inv :=        func(S, op, id);
  17.         return {[a,b] : a, b in S| a .op b = id };
  18.         end;
  19.  
  20. group :=    func(S, op);
  21.         local zero, minus;
  22.         if is_set(S) and (is_map(op) or is_func(op))
  23.            and closed(S, op) and assoc(S, op) 
  24.             then
  25.             zero := id(S, op);
  26.             minus := inv(S, op, zero);
  27.  
  28.             if zero in S and is_map(minus)
  29.                      and domain(minus) = S
  30.                 then return [S,op,zero,minus];
  31.                 end;
  32.             end;
  33.         end;
  34.  
  35.  
  36. I5 := {0..4};
  37. plus := func(a,b); return (a+b) mod 5; end;
  38. G := group(I5,plus);
  39. G(3) = 0 and G(4) = {[i,(5-i) mod 5] : i in I5};
  40.