author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1478  2b8c2a7547ab 
child 1851  7b1e1c298e50 
permissions  rwrr 
1478  1 
(* Title: ZF/Order.thy 
435  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
435  4 
Copyright 1994 University of Cambridge 
5 

6 
Orders in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
Order = WF + Perm + 

10 
consts 

1478  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 (*Wellordering*) 

14 
mono_map :: [i,i,i,i]=>i (*Orderpreserving 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*) 

435  18 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
435
diff
changeset

19 
defs 
435  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 

1155  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}" 

786  30 

1155  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}" 

435  33 

34 
pred_def "pred(A,x,r) == {y:A. <y,x>:r}" 

35 

786  36 
ord_iso_map_def 
1155  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). 

39 
{<x,y>}" 

786  40 

435  41 
end 