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
```