author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 2469 | b50b8c0eec01 |
child 9683 | f87c8c449018 |
permissions | -rw-r--r-- |
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 Zermelo-Fraenkel 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 (*Well-ordering*) |
|
14 |
mono_map :: [i,i,i,i]=>i (*Order-preserving maps*) |
|
15 |
ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*) |
|
1851 | 16 |
pred :: [i,i,i]=>i (*Set of predecessors*) |
1478 | 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 re-building 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 |
|
2469 | 41 |
constdefs |
42 |
||
43 |
first :: [i, i, i] => o |
|
44 |
"first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
|
45 |
||
435 | 46 |
end |