src/ZF/Order.thy

 (*  Title:      ZF/Order.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Orders in Zermelo-Fraenkel Set Theory
-
 Results from the book "Set Theory: an Introduction to Independence Proofs"
         by Kenneth Kunen.  Chapter 1, section 6.
 *)
 
+header{*Partial and Total Orderings: Basic Definitions and Properties*}
+
 theory Order = WF + Perm:
 
 constdefs
 
   part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)

 
 syntax (xsymbols)
     ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
 
 
-(** Basic properties of the definitions **)
-
-(*needed?*)
+subsection{*Immediate Consequences of the Definitions*}
+
 lemma part_ord_Imp_asym:
     "part_ord(A,r) ==> asym(r Int A*A)"
 by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
 
 lemma linearE:

     "[| trans[A](r);  <y,x>:r;  x:A;  y:A |]
      ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
 by (unfold trans_on_def pred_def, blast)
 
 
+subsection{*Restricting an Ordering's Domain*}
+
 (** The ordering's properties hold over all subsets of its domain
     [including initial segments of the form pred(A,x,r) **)
 
 (*Note: a relation s such that s<=r need not be a partial ordering*)
 lemma part_ord_subset:

 apply (unfold well_ord_def)
 apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
 done
 
 
+subsection{*Empty and Unit Domains*}
+
 (** Relations over the Empty Set **)
 
 lemma irrefl_0: "irrefl(0,r)"
 by (unfold irrefl_def, blast)
 

 lemma well_ord_unit: "well_ord({a},0)"
 apply (unfold well_ord_def)
 apply (simp add: tot_ord_unit wf_on_unit)
 done
 
+
+subsection{*Order-Isomorphisms*}
+
+text{*Suppes calls them "similarities"*}
 
 (** Order-preserving (monotone) maps **)
 
 lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
 by (simp add: mono_map_def)

     "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
 apply (unfold mono_map_def inj_def, clarify)
 apply (erule_tac x=w and y=x in linearE, assumption+)
 apply (force intro: apply_type dest: wf_on_not_refl)+
 done
-
-
-(** Order-isomorphisms -- or similarities, as Suppes calls them **)
 
 lemma ord_isoI:
     "[| f: bij(A, B);
         !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
      ==> f: ord_iso(A,r,B,s)"

 apply (unfold well_ord_def tot_ord_def)
 apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
 done
 
 
-(*** Main results of Kunen, Chapter 1 section 6 ***)
+subsection{*Main results of Kunen, Chapter 1 section 6*}
 
 (*Inductive argument for Kunen's Lemma 6.1, etc.
   Simple proof from Halmos, page 72*)
 lemma well_ord_iso_subset_lemma:
      "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |]

  apply (blast dest: well_ord_iso_unique_lemma)
 apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
                     well_ord_is_linear well_ord_ord_iso ord_iso_sym)
 done
 
-(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
+subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*}
 
 lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
 by (unfold ord_iso_map_def, blast)
 
 lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A"

          (EX y:B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))"
 apply (rule converse_ord_iso_map [THEN subst])
 apply (simp add: domain_ord_iso_map_cases)
 done
 
-(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
-lemma well_ord_trichotomy:
+text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*}
+theorem well_ord_trichotomy:
    "[| well_ord(A,r);  well_ord(B,s) |]
     ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
         (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
         (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"
 apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)

  apply (simp add: pred_def)
 apply (unfold ord_iso_map_def, blast)
 done
 
 
-(*** Properties of converse(r), by Krzysztof Grabczewski ***)
+subsection{*Miscellaneous Results by Krzysztof Grabczewski*}
+
+(** Properties of converse(r) **)
 
 lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
 by (unfold irrefl_def, blast)
 
 lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"