# HG changeset patch
# User paulson
# Date 1020845675 -7200
# Node ID d1fea11b2fb680cd3682db3a52442df90035be1e
# Parent  6f7526467e5ad15d4e884a329349be21c3333daa
tidied

diff -r 6f7526467e5a -r d1fea11b2fb6 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Wed May 08 10:14:07 2002 +0200
+++ b/src/ZF/Order.ML	Wed May 08 10:14:35 2002 +0200
@@ -233,8 +233,7 @@
 
 (*Needed?  But ord_iso_converse is!*)
 Goalw [ord_iso_def] 
-    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> \
-\         <f`x, f`y> : s";
+    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s";
 by (Blast_tac 1);
 qed "ord_iso_apply";
 
@@ -246,8 +245,8 @@
           addsimps [right_inverse_bij];
 
 Goalw [ord_iso_def] 
-    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] ==> \
-\         <converse(f) ` x, converse(f) ` y> : r";
+    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] \
+\    ==> <converse(f) ` x, converse(f) ` y> : r";
 by (etac CollectE 1);
 by (etac (bspec RS bspec RS iffD2) 1);
 by (REPEAT (eresolve_tac [asm_rl, 
@@ -287,7 +286,7 @@
 
 Goalw [ord_iso_def, mono_map_def]
     "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);     \
-\              f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
+\       f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
 by Safe_tac;
 by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
 by (Blast_tac 1);
@@ -296,9 +295,9 @@
 by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
 qed "mono_ord_isoI";
 
-Goal "[| well_ord(A,r);  well_ord(B,s);                             \
-\            f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r)      \
-\         |] ==> f: ord_iso(A,r,B,s)";
+Goal "[| well_ord(A,r);  well_ord(B,s);                           \
+\        f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |] \
+\     ==> f: ord_iso(A,r,B,s)";
 by (REPEAT (ares_tac [mono_ord_isoI] 1));
 by (forward_tac [mono_map_is_fun RS fun_is_rel] 1);
 by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1);
@@ -385,8 +384,7 @@
 
 (*Does not assume r is a wellordering!*)
 Goalw [ord_iso_def, pred_def]
- "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
-\      f `` pred(A,a,r) = pred(B, f`a, s)";
+     "[|f : ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)";
 by (etac CollectE 1);
 by (asm_simp_tac 
     (simpset() addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
@@ -434,8 +432,8 @@
 
 (*See Halmos, page 72*)
 Goal "[| well_ord(A,r);  \
-\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
-\         ==> ~ <g`y, f`y> : s";
+\        f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
+\     ==> ~ <g`y, f`y> : s";
 by (ftac well_ord_iso_subset_lemma 1);
 by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
 by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
@@ -447,7 +445,7 @@
 
 (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
 Goal "[| well_ord(A,r);  \
-\            f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
+\        f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
 by (rtac fun_extension 1);
 by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
 by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
@@ -594,28 +592,23 @@
 
 (*** Properties of converse(r), by Krzysztof Grabczewski ***)
 
-Goalw [irrefl_def] 
-            "irrefl(A,r) ==> irrefl(A,converse(r))";
+Goalw [irrefl_def] "irrefl(A,r) ==> irrefl(A,converse(r))";
 by (Blast_tac 1);
 qed "irrefl_converse";
 
-Goalw [trans_on_def] 
-    "trans[A](r) ==> trans[A](converse(r))";
+Goalw [trans_on_def] "trans[A](r) ==> trans[A](converse(r))";
 by (Blast_tac 1);
 qed "trans_on_converse";
 
-Goalw [part_ord_def] 
-    "part_ord(A,r) ==> part_ord(A,converse(r))";
+Goalw [part_ord_def] "part_ord(A,r) ==> part_ord(A,converse(r))";
 by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1);
 qed "part_ord_converse";
 
-Goalw [linear_def] 
-    "linear(A,r) ==> linear(A,converse(r))";
+Goalw [linear_def] "linear(A,r) ==> linear(A,converse(r))";
 by (Blast_tac 1);
 qed "linear_converse";
 
-Goalw [tot_ord_def] 
-    "tot_ord(A,r) ==> tot_ord(A,converse(r))";
+Goalw [tot_ord_def] "tot_ord(A,r) ==> tot_ord(A,converse(r))";
 by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1);
 qed "tot_ord_converse";