hol88 (2.02.19940316-13.1) Library/wellorder/Manual/theorems.tex

--- hol88-2.02.19940316.orig/Library/wellorder/Manual/theorems.tex
+++ hol88-2.02.19940316/Library/wellorder/Manual/theorems.tex
@@ -1,7 +1,4 @@
-\chapter{Pre-proved Theorems}
-\input{theorems-intro}
-\section{Basic definitions}
-\THEOREM wo\_chain WELLORDER
+\chapter{Pre-proved Theorems}\input{theorems-intro}\section{Basic definitions}\THEOREM wo\_chain WELLORDER
 |- !l P. chain l P = (!x y. P x /\ P y ==> l(x,y) \/ l(y,x))
 \ENDTHEOREM
 \THEOREM wo\_fl WELLORDER
@@ -41,8 +38,7 @@
       (!x. P x ==> fl l x) /\ (?x. P x) ==>
       (?y. P y /\ (!z. P z ==> l(y,z))))
 \ENDTHEOREM
-\section{Miscellaneous lemmas}
-\THEOREM AGREE\_LEMMA WELLORDER
+\section{Miscellaneous lemmas}\THEOREM AGREE\_LEMMA WELLORDER
 |- !l h ms m n f g z.
     woset l /\
     (!x. fl l(ms x)) /\
@@ -152,44 +148,6 @@
 \THEOREM UNION\_INSEG WELLORDER
 |- !P l. (!m. P m ==> m inseg l) ==> (Union P) inseg l
 \ENDTHEOREM
-\THEOREM WOSET WELLORDER
-|- !l.
-    woset l =
-    (!x y. l(x,y) /\ l(y,x) ==> (x = y)) /\
-    (!P.
-      (!x. P x ==> fl l x) /\ (?x. P x) ==>
-      (?y. P y /\ (!z. P z ==> l(y,z))))
-\ENDTHEOREM
-\THEOREM WOSET\_FLEQ WELLORDER
-|- !l. woset l ==> (!x. fl l x = l(x,x))
-\ENDTHEOREM
-\THEOREM WOSET\_NUM WELLORDER
-|- woset(\(m,n). m <= n)
-\ENDTHEOREM
-\THEOREM WOSET\_POSET WELLORDER
-|- !l. woset l ==> poset l
-\ENDTHEOREM
-\THEOREM WOSET\_TOTAL\_LE WELLORDER
-|- !l. woset l ==> (!x y. fl l x /\ fl l y ==> l(x,y) \/ less l(y,x))
-\ENDTHEOREM
-\THEOREM WOSET\_TOTAL\_LT WELLORDER
-|- !l.
-    woset l ==>
-    (!x y. fl l x /\ fl l y ==> (x = y) \/ less l(x,y) \/ less l(y,x))
-\ENDTHEOREM
-\THEOREM WOSET\_TRANS\_LE WELLORDER
-|- !l. woset l ==> (!x y z. l(x,y) /\ less l(y,z) ==> less l(x,z))
-\ENDTHEOREM
-\THEOREM WOSET\_TRANS\_LESS WELLORDER
-|- !l. woset l ==> (!x y z. less l(x,y) /\ l(y,z) ==> less l(x,z))
-\ENDTHEOREM
-\THEOREM WOSET\_WELL\_CONTRAPOS WELLORDER
-|- !l.
-    woset l ==>
-    (!P.
-      (!x. P x ==> fl l x) /\ (?x. P x) ==>
-      (?y. P y /\ (!z. less l(z,y) ==> ~P z)))
-\ENDTHEOREM
 \THEOREM WO\_FL\_RESTRICT WELLORDER
 |- !l.
     woset l ==>
@@ -233,8 +191,45 @@
       (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==>
     (?! f. !x. f x = h f x)
 \ENDTHEOREM
-\section{Main theorems}
-\THEOREM HP WELLORDER
+\THEOREM WOSET WELLORDER
+|- !l.
+    woset l =
+    (!x y. l(x,y) /\ l(y,x) ==> (x = y)) /\
+    (!P.
+      (!x. P x ==> fl l x) /\ (?x. P x) ==>
+      (?y. P y /\ (!z. P z ==> l(y,z))))
+\ENDTHEOREM
+\THEOREM WOSET\_FLEQ WELLORDER
+|- !l. woset l ==> (!x. fl l x = l(x,x))
+\ENDTHEOREM
+\THEOREM WOSET\_NUM WELLORDER
+|- woset(\(m,n). m <= n)
+\ENDTHEOREM
+\THEOREM WOSET\_POSET WELLORDER
+|- !l. woset l ==> poset l
+\ENDTHEOREM
+\THEOREM WOSET\_TOTAL\_LE WELLORDER
+|- !l. woset l ==> (!x y. fl l x /\ fl l y ==> l(x,y) \/ less l(y,x))
+\ENDTHEOREM
+\THEOREM WOSET\_TOTAL\_LT WELLORDER
+|- !l.
+    woset l ==>
+    (!x y. fl l x /\ fl l y ==> (x = y) \/ less l(x,y) \/ less l(y,x))
+\ENDTHEOREM
+\THEOREM WOSET\_TRANS\_LE WELLORDER
+|- !l. woset l ==> (!x y z. l(x,y) /\ less l(y,z) ==> less l(x,z))
+\ENDTHEOREM
+\THEOREM WOSET\_TRANS\_LESS WELLORDER
+|- !l. woset l ==> (!x y z. less l(x,y) /\ l(y,z) ==> less l(x,z))
+\ENDTHEOREM
+\THEOREM WOSET\_WELL\_CONTRAPOS WELLORDER
+|- !l.
+    woset l ==>
+    (!P.
+      (!x. P x ==> fl l x) /\ (?x. P x) ==>
+      (?y. P y /\ (!z. less l(z,y) ==> ~P z)))
+\ENDTHEOREM
+\section{Main theorems}\THEOREM HP WELLORDER
 |- !l.
     poset l ==>
     (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P)))