src/ZF/Order.thy
author paulson
Thu Aug 24 11:05:20 2000 +0200 (2000-08-24)
changeset 9683 f87c8c449018
parent 2469 b50b8c0eec01
child 13119 6f7526467e5a
permissions -rw-r--r--
added some xsymbols, and tidied
     1 (*  Title:      ZF/Order.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Orders in Zermelo-Fraenkel Set Theory 
     7 *)
     8 
     9 Order = WF + Perm + 
    10 consts
    11   part_ord        :: [i,i]=>o           (*Strict partial ordering*)
    12   linear, tot_ord :: [i,i]=>o           (*Strict total ordering*)
    13   well_ord        :: [i,i]=>o           (*Well-ordering*)
    14   mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
    15   ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
    16   pred            :: [i,i,i]=>i		(*Set of predecessors*)
    17   ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
    18 
    19 defs
    20   part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    21 
    22   linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
    23 
    24   tot_ord_def  "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
    25 
    26   well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
    27 
    28   mono_map_def "mono_map(A,r,B,s) == 
    29                    {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
    30 
    31   ord_iso_def  "ord_iso(A,r,B,s) == 
    32                    {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
    33 
    34   pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
    35 
    36   ord_iso_map_def
    37      "ord_iso_map(A,r,B,s) == 
    38        UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
    39 
    40 constdefs
    41 
    42   first :: [i, i, i] => o
    43     "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
    44 
    45 syntax (xsymbols)
    46     ord_iso :: [i,i,i,i]=>i       ("('(_,_') \\<cong> '(_,_'))" 50)
    47 
    48 
    49 end