src/ZF/Order.thy
 changeset 13356 c9cfe1638bf2 parent 13339 0f89104dd377 child 13611 2edf034c902a
```     1.1 --- a/src/ZF/Order.thy	Sun Jul 14 15:11:21 2002 +0200
1.2 +++ b/src/ZF/Order.thy	Sun Jul 14 15:14:43 2002 +0200
1.3 @@ -3,12 +3,12 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1994  University of Cambridge
1.6
1.7 -Orders in Zermelo-Fraenkel Set Theory
1.8 -
1.9  Results from the book "Set Theory: an Introduction to Independence Proofs"
1.10          by Kenneth Kunen.  Chapter 1, section 6.
1.11  *)
1.12
1.13 +header{*Partial and Total Orderings: Basic Definitions and Properties*}
1.14 +
1.15  theory Order = WF + Perm:
1.16
1.17  constdefs
1.18 @@ -48,9 +48,8 @@
1.19      ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
1.20
1.21
1.22 -(** Basic properties of the definitions **)
1.23 +subsection{*Immediate Consequences of the Definitions*}
1.24
1.25 -(*needed?*)
1.26  lemma part_ord_Imp_asym:
1.27      "part_ord(A,r) ==> asym(r Int A*A)"
1.28  by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
1.29 @@ -109,6 +108,8 @@
1.30  by (unfold trans_on_def pred_def, blast)
1.31
1.32
1.33 +subsection{*Restricting an Ordering's Domain*}
1.34 +
1.35  (** The ordering's properties hold over all subsets of its domain
1.36      [including initial segments of the form pred(A,x,r) **)
1.37
1.38 @@ -165,6 +166,8 @@
1.39  done
1.40
1.41
1.42 +subsection{*Empty and Unit Domains*}
1.43 +
1.44  (** Relations over the Empty Set **)
1.45
1.46  lemma irrefl_0: "irrefl(0,r)"
1.47 @@ -209,6 +212,10 @@
1.48  done
1.49
1.50
1.51 +subsection{*Order-Isomorphisms*}
1.52 +
1.53 +text{*Suppes calls them "similarities"*}
1.54 +
1.55  (** Order-preserving (monotone) maps **)
1.56
1.57  lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
1.58 @@ -221,9 +228,6 @@
1.59  apply (force intro: apply_type dest: wf_on_not_refl)+
1.60  done
1.61
1.62 -
1.63 -(** Order-isomorphisms -- or similarities, as Suppes calls them **)
1.64 -
1.65  lemma ord_isoI:
1.66      "[| f: bij(A, B);
1.67          !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
1.68 @@ -342,7 +346,7 @@
1.69  done
1.70
1.71
1.72 -(*** Main results of Kunen, Chapter 1 section 6 ***)
1.73 +subsection{*Main results of Kunen, Chapter 1 section 6*}
1.74
1.75  (*Inductive argument for Kunen's Lemma 6.1, etc.
1.76    Simple proof from Halmos, page 72*)
1.77 @@ -456,7 +460,7 @@
1.78                      well_ord_is_linear well_ord_ord_iso ord_iso_sym)
1.79  done
1.80
1.81 -(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
1.82 +subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*}
1.83
1.84  lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
1.85  by (unfold ord_iso_map_def, blast)
1.86 @@ -564,8 +568,8 @@
1.88  done
1.89
1.90 -(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
1.91 -lemma well_ord_trichotomy:
1.92 +text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*}
1.93 +theorem well_ord_trichotomy:
1.94     "[| well_ord(A,r);  well_ord(B,s) |]
1.95      ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
1.96          (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
1.97 @@ -585,7 +589,9 @@
1.98  done
1.99
1.100
1.101 -(*** Properties of converse(r), by Krzysztof Grabczewski ***)
1.102 +subsection{*Miscellaneous Results by Krzysztof Grabczewski*}
1.103 +
1.104 +(** Properties of converse(r) **)
1.105
1.106  lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
1.107  by (unfold irrefl_def, blast)
```