src/ZF/Perm.thy
author paulson
Mon, 17 Jun 1996 16:50:08 +0200
changeset 1806 12708740f58d
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01
permissions -rw-r--r--
Converted to use constdefs instead of defs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/perm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
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
124
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents: 0
diff changeset
    12
Perm = ZF + "mono" +
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
consts
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    14
  O     :: [i,i]=>i      (infixr 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 124
diff changeset
    16
defs
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    17
  (*composition of relations and functions; NOT Suppes's relative product*)
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    18
  comp_def    "r O s == {xz : domain(s)*range(r) . 
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    19
                              EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    21
constdefs
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    22
  (*the identity function for A*)
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    23
  id    :: i=>i
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    24
  "id(A) == (lam x:A. x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    26
  (*one-to-one functions from A to B*)
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    27
  inj   :: [i,i]=>i
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    28
  "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    30
  (*onto functions from A to B*)
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    31
  surj  :: [i,i]=>i
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    32
  "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    34
  (*one-to-one and onto functions*)
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    35
  bij   :: [i,i]=>i
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    36
  "bij(A,B) == inj(A,B) Int surj(A,B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
end