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.87  apply (simp add: domain_ord_iso_map_cases)
    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)