# HG changeset patch
# User paulson
# Date 908789064 -7200
# Node ID 822db50b3ec56fcf88dc9379693881fbe3509266
# Parent  1dc74203b1d259d4e41bc3dae1b60d04e1cc1798
fixed some indenting; changed a VERY slow blast_tac to fast_tac

diff -r 1dc74203b1d2 -r 822db50b3ec5 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Sun Oct 18 16:49:56 1998 +0200
+++ b/src/ZF/Zorn.ML	Mon Oct 19 11:24:24 1998 +0200
@@ -25,13 +25,11 @@
 
 (*** Section 2.  The Transfinite Construction ***)
 
-Goalw [increasing_def]
-    "f: increasing(A) ==> f: Pow(A)->Pow(A)";
+Goalw [increasing_def] "f: increasing(A) ==> f: Pow(A)->Pow(A)";
 by (etac CollectD1 1);
 qed "increasingD1";
 
-Goalw [increasing_def]
-    "[| f: increasing(A); x<=A |] ==> x <= f`x";
+Goalw [increasing_def] "[| f: increasing(A); x<=A |] ==> x <= f`x";
 by (eresolve_tac [CollectD2 RS spec RS mp] 1);
 by (assume_tac 1);
 qed "increasingD2";
@@ -104,15 +102,15 @@
 qed "TFin_linear_lemma2";
 
 (*a more convenient form for Lemma 2*)
-Goal "[| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
-\           |] ==> n=m | next`n<=m";
+Goal "[| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |] \
+\     ==> n=m | next`n<=m";
 by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
 by (REPEAT (assume_tac 1));
 qed "TFin_subsetD";
 
 (*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
-Goal "[| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
-\           |] ==> n<=m | m<=n";
+Goal "[| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |] \
+\     ==> n<=m | m<=n";
 by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
 by (REPEAT (assume_tac 1) THEN etac disjI2 1);
 by (blast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
@@ -130,8 +128,8 @@
 qed "equal_next_upper";
 
 (*Property 3.3 of section 3.3*)
-Goal "[| m: TFin(S,next);  next: increasing(S) \
-\         |] ==> m = next`m <-> m = Union(TFin(S,next))";
+Goal "[| m: TFin(S,next);  next: increasing(S) |]  \
+\     ==> m = next`m <-> m = Union(TFin(S,next))";
 by (rtac iffI 1);
 by (rtac (Union_upper RS equalityI) 1);
 by (rtac (equal_next_upper RS Union_least) 2);
@@ -160,17 +158,17 @@
 by (rtac Collect_subset 1);
 qed "maxchain_subset_chain";
 
-Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X);      \
-\            X : chain(S);  X ~: maxchain(S)            \
-\         |] ==> ch ` super(S,X) : super(S,X)";
+Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X);  \
+\        X : chain(S);  X ~: maxchain(S) |]     \
+\     ==> ch ` super(S,X) : super(S,X)";
 by (etac apply_type 1);
 by (rewrite_goals_tac [super_def, maxchain_def]);
 by (Blast_tac 1);
 qed "choice_super";
 
 Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X);      \
-\            X : chain(S);  X ~: maxchain(S)            \
-\         |] ==> ch ` super(S,X) ~= X";
+\            X : chain(S);  X ~: maxchain(S) |]     \
+\     ==> ch ` super(S,X) ~= X";
 by (rtac notI 1);
 by (dtac choice_super 1);
 by (assume_tac 1);
@@ -180,8 +178,8 @@
 
 (*This justifies Definition 4.4*)
 Goal "ch: (PROD X: Pow(chain(S))-{0}. X) ==>        \
-\          EX next: increasing(S). ALL X: Pow(S).       \
-\                     next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)";
+\     EX next: increasing(S). ALL X: Pow(S).       \
+\                  next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)";
 by (rtac bexI 1);
 by (rtac ballI 1);
 by (rtac beta 1);
@@ -191,8 +189,8 @@
 by (rtac lam_type 1);
 by (Asm_simp_tac 1);
 by (fast_tac (claset() addSIs [super_subset_chain RS subsetD,
-			      chain_subset_Pow RS subsetD,
-			      choice_super]) 1);
+			       chain_subset_Pow RS subsetD,
+			       choice_super]) 1);
 (*Now, verify that it increases*)
 by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_refl]) 1);
 by Safe_tac;
@@ -265,16 +263,15 @@
 by (rewtac super_def);
 by Safe_tac;
 by (fast_tac (claset() addEs [chain_extend]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (fast_tac (claset() addEs [equalityE]) 1);
 qed "Zorn";
 
 
 (*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
 
 (*Lemma 5*)
-Goal
-    "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z      \
-\    |] ==> ALL m:Z. n<=m";
+Goal "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]  \
+\     ==> ALL m:Z. n<=m";
 by (etac TFin_induct 1);
 by (Blast_tac 2);                  (*second induction step is easy*)
 by (rtac ballI 1);
@@ -343,9 +340,9 @@
 
 (*The construction of the injection*)
 Goal "[| ch: (PROD X: Pow(S)-{0}. X);                 \
-\          next: increasing(S);                         \
-\          ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X))        \
-\       |] ==> (lam x:S. Union({y: TFin(S,next). x~: y}))       \
+\        next: increasing(S);                         \
+\        ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |] \
+\     ==> (lam x:S. Union({y: TFin(S,next). x~: y}))       \
 \              : inj(S, TFin(S,next) - {S})";
 by (res_inst_tac [("d", "%y. ch`(S-y)")] lam_injective 1);
 by (rtac DiffI 1);