src/ZF/Perm.thy
author paulson
Mon Jun 17 16:50:08 1996 +0200 (1996-06-17)
changeset 1806 12708740f58d
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01
permissions -rw-r--r--
Converted to use constdefs instead of defs
     1 (*  Title:      ZF/perm
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 The theory underlying permutation groups
     7   -- Composition of relations, the identity relation
     8   -- Injections, surjections, bijections
     9   -- Lemmas for the Schroeder-Bernstein Theorem
    10 *)
    11 
    12 Perm = ZF + "mono" +
    13 consts
    14   O     :: [i,i]=>i      (infixr 60)
    15 
    16 defs
    17   (*composition of relations and functions; NOT Suppes's relative product*)
    18   comp_def    "r O s == {xz : domain(s)*range(r) . 
    19                               EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    20 
    21 constdefs
    22   (*the identity function for A*)
    23   id    :: i=>i
    24   "id(A) == (lam x:A. x)"
    25 
    26   (*one-to-one functions from A to B*)
    27   inj   :: [i,i]=>i
    28   "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
    29 
    30   (*onto functions from A to B*)
    31   surj  :: [i,i]=>i
    32   "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
    33 
    34   (*one-to-one and onto functions*)
    35   bij   :: [i,i]=>i
    36   "bij(A,B) == inj(A,B) Int surj(A,B)"
    37 
    38 end