src/ZF/perm.thy
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 124 858ab9a9b047
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/perm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
The theory underlying permutation groups
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
  -- Composition of relations, the identity relation
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
  -- Injections, surjections, bijections
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
  -- Lemmas for the Schroeder-Bernstein Theorem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
Perm = ZF +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
    O    	::      "[i,i]=>i"      (infixr 60)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
    id  	::      "i=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    inj,surj,bij::      "[i,i]=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    (*composition of relations and functions; NOT Suppes's relative product*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    comp_def	"r O s == {xz : domain(s)*range(r) . \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
\                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
    (*the identity function for A*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    id_def	"id(A) == (lam x:A. x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
    (*one-to-one functions from A to B*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    inj_def      "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
    (*onto functions from A to B*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    surj_def	"surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
    (*one-to-one and onto functions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    bij_def	"bij(A,B) == inj(A,B) Int surj(A,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
end