# HG changeset patch
# User paulson
# Date 1031071770 -7200
# Node ID 18acbbd4d22518167ca049f46e15a9b8b2ec6d16
# Parent  6061d0045409833a4db38722368dea2f313b0c1e
tidied

diff -r 6061d0045409 -r 18acbbd4d225 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Tue Sep 03 18:49:10 2002 +0200
+++ b/src/ZF/Zorn.thy	Tue Sep 03 18:49:30 2002 +0200
@@ -14,29 +14,29 @@
 
 constdefs
   Subset_rel :: "i=>i"
-   "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
+   "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
 
   chain      :: "i=>i"
-   "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
+   "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
 
   maxchain   :: "i=>i"
-   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
-  
+   "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
+
   super      :: "[i,i]=>i"
-   "super(A,c)    == {d: chain(A). c<=d & c~=d}"
+   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
 
 
 constdefs
   increasing :: "i=>i"
-    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A --> x<=f`x}"
 
 
-(*Lemma for the inductive definition below*)
-lemma Union_in_Pow: "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
+text{*Lemma for the inductive definition below*}
+lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> Union(Y) \<in> Pow(A)"
 by blast
 
 
-text{*We could make the inductive definition conditional on 
+text{*We could make the inductive definition conditional on
     @{term "next \<in> increasing(S)"}
     but instead we make this a side-condition of an introduction rule.  Thus
     the induction rule lets us assume that condition!  Many inductive proofs
@@ -47,10 +47,10 @@
 inductive
   domains       "TFin(S,next)" <= "Pow(S)"
   intros
-    nextI:       "[| x : TFin(S,next);  next: increasing(S) |]
-                  ==> next`x : TFin(S,next)"
+    nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
+                  ==> next`x \<in> TFin(S,next)"
 
-    Pow_UnionI: "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
+    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> Union(Y) \<in> TFin(S,next)"
 
   monos         Pow_mono
   con_defs      increasing_def
@@ -59,22 +59,22 @@
 
 subsection{*Mathematical Preamble *}
 
-lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
+lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
 by blast
 
 lemma Inter_lemma0:
-     "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
+     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A <= Inter(C) | Inter(C) <= B"
 by blast
 
 
 subsection{*The Transfinite Construction *}
 
-lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)"
+lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
 apply (unfold increasing_def)
 apply (erule CollectD1)
 done
 
-lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
+lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
 by (unfold increasing_def, blast)
 
 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
@@ -82,25 +82,24 @@
 lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
 
 
-(** Structural induction on TFin(S,next) **)
-
+text{*Structural induction on @{term "TFin(S,next)"} *}
 lemma TFin_induct:
-  "[| n: TFin(S,next);   
-      !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x);  
-      !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y))  
+  "[| n \<in> TFin(S,next);
+      !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
+      !!Y. [| Y <= TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(Union(Y))
    |] ==> P(n)"
 by (erule TFin.induct, blast+)
 
 
 subsection{*Some Properties of the Transfinite Construction *}
 
-lemmas increasing_trans = subset_trans [OF _ increasingD2, 
+lemmas increasing_trans = subset_trans [OF _ increasingD2,
                                         OF _ _ TFin_is_subset]
 
-(*Lemma 1 of section 3.1*)
+text{*Lemma 1 of section 3.1*}
 lemma TFin_linear_lemma1:
-     "[| n: TFin(S,next);  m: TFin(S,next);   
-         ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m |] 
+     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
+         \<forall>x \<in> TFin(S,next) . x<=m --> x=m | next`x<=m |]
       ==> n<=m | next`m<=n"
 apply (erule TFin_induct)
 apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
@@ -108,61 +107,62 @@
 apply (blast dest: increasing_trans)
 done
 
-(*Lemma 2 of section 3.2.  Interesting in its own right!
-  Requires next: increasing(S) in the second induction step. *)
+text{*Lemma 2 of section 3.2.  Interesting in its own right!
+  Requires @{term "next \<in> increasing(S)"} in the second induction step.*}
 lemma TFin_linear_lemma2:
-    "[| m: TFin(S,next);  next: increasing(S) |] 
-     ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m"
+    "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
+     ==> \<forall>n \<in> TFin(S,next). n<=m --> n=m | next`n <= m"
 apply (erule TFin_induct)
 apply (rule impI [THEN ballI])
-(*case split using TFin_linear_lemma1*)
+txt{*case split using @{text TFin_linear_lemma1}*}
 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
        assumption+)
 apply (blast del: subsetI
-	     intro: increasing_trans subsetI, blast) 
-(*second induction step*)
+	     intro: increasing_trans subsetI, blast)
+txt{*second induction step*}
 apply (rule impI [THEN ballI])
 apply (rule Union_lemma0 [THEN disjE])
 apply (erule_tac [3] disjI2)
-prefer 2 apply blast 
+prefer 2 apply blast
 apply (rule ballI)
-apply (drule bspec, assumption) 
-apply (drule subsetD, assumption) 
+apply (drule bspec, assumption)
+apply (drule subsetD, assumption)
 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
-       assumption+, blast) 
+       assumption+, blast)
 apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
 apply (blast dest: TFin_is_subset)+
 done
 
-(*a more convenient form for Lemma 2*)
+text{*a more convenient form for Lemma 2*}
 lemma TFin_subsetD:
-     "[| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |]  
-      ==> n=m | next`n<=m"
-by (blast dest: TFin_linear_lemma2 [rule_format]) 
+     "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
+      ==> n=m | next`n <= m"
+by (blast dest: TFin_linear_lemma2 [rule_format])
 
-(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
+text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
 lemma TFin_subset_linear:
-     "[| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |]  
-      ==> n<=m | m<=n"
-apply (rule disjE) 
+     "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
+      ==> n <= m | m<=n"
+apply (rule disjE)
 apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
 apply (assumption+, erule disjI2)
-apply (blast del: subsetI 
+apply (blast del: subsetI
              intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
 done
 
 
-(*Lemma 3 of section 3.3*)
+text{*Lemma 3 of section 3.3*}
 lemma equal_next_upper:
-     "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m"
+     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
 apply (erule TFin_induct)
 apply (drule TFin_subsetD)
-apply (assumption+, force) 
+apply (assumption+, force)
 apply blast
 done
 
-(*Property 3.3 of section 3.3*)
-lemma equal_next_Union: "[| m: TFin(S,next);  next: increasing(S) |]   
+text{*Property 3.3 of section 3.3*}
+lemma equal_next_Union:
+     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
       ==> m = next`m <-> m = Union(TFin(S,next))"
 apply (rule iffI)
 apply (rule Union_upper [THEN equalityI])
@@ -180,7 +180,7 @@
 text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
 relation!*}
 
-(** Defining the "next" operation for Hausdorff's Theorem **)
+text{** Defining the "next" operation for Hausdorff's Theorem **}
 
 lemma chain_subset_Pow: "chain(A) <= Pow(A)"
 apply (unfold chain_def)
@@ -197,38 +197,38 @@
 apply (rule Collect_subset)
 done
 
-lemma choice_super: "[| ch : (PROD X:Pow(chain(S)) - {0}. X);   
-         X : chain(S);  X ~: maxchain(S) |]      
-      ==> ch ` super(S,X) : super(S,X)"
+lemma choice_super:
+     "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+      ==> ch ` super(S,X) \<in> super(S,X)"
 apply (erule apply_type)
 apply (unfold super_def maxchain_def, blast)
 done
 
 lemma choice_not_equals:
-     "[| ch : (PROD X:Pow(chain(S)) - {0}. X);       
-         X : chain(S);  X ~: maxchain(S) |]      
-      ==> ch ` super(S,X) ~= X"
+     "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+      ==> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
 apply (drule choice_super, assumption)
 apply assumption
 apply (simp add: super_def)
 done
 
-(*This justifies Definition 4.4*)
+text{*This justifies Definition 4.4*}
 lemma Hausdorff_next_exists:
-     "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)"
-apply (rule_tac x="\<lambda>X\<in>Pow(S). 
-                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X" 
+     "ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X) ==>
+      \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
+                   next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
+apply (rule_tac x="\<lambda>X\<in>Pow(S).
+                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
        in bexI)
-apply force 
+apply force
 apply (unfold increasing_def)
 apply (rule CollectI)
 apply (rule lam_type)
 apply (simp (no_asm_simp))
-apply (blast dest: super_subset_chain [THEN subsetD] chain_subset_Pow [THEN subsetD] choice_super)
-(*Now, verify that it increases*)
+apply (blast dest: super_subset_chain [THEN subsetD] 
+                   chain_subset_Pow [THEN subsetD] choice_super)
+txt{*Now, verify that it increases*}
 apply (simp (no_asm_simp) add: Pow_iff subset_refl)
 apply safe
 apply (drule choice_super)
@@ -236,28 +236,28 @@
 apply (simp add: super_def, blast)
 done
 
-(*Lemma 4*)
+text{*Lemma 4*}
 lemma TFin_chain_lemma4:
-     "[| c: TFin(S,next);                               
-         ch: (PROD X: Pow(chain(S))-{0}. X);            
-         next: increasing(S);                           
-         ALL X: Pow(S). next`X =        
-                          if(X: chain(S)-maxchain(S), ch`super(S,X), X) |] 
-     ==> c: chain(S)"
+     "[| c \<in> TFin(S,next);
+         ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X);
+         next \<in> increasing(S);
+         \<forall>X \<in> Pow(S). next`X =
+                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
+     ==> c \<in> chain(S)"
 apply (erule TFin_induct)
-apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] 
+apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
             choice_super [THEN super_subset_chain [THEN subsetD]])
 apply (unfold chain_def)
 apply (rule CollectI, blast, safe)
-apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) 
-      (*Blast_tac's slow*)
+apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
+      txt{*@{text "Blast_tac's"} slow*}
 done
 
-theorem Hausdorff: "EX c. c : maxchain(S)"
+theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
 apply (rule AC_Pi_Pow [THEN exE])
 apply (rule Hausdorff_next_exists [THEN bexE], assumption)
 apply (rename_tac ch "next")
-apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ")
+apply (subgoal_tac "Union (TFin (S,next)) \<in> chain (S) ")
 prefer 2
  apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
 apply (rule_tac x = "Union (TFin (S,next))" in exI)
@@ -267,24 +267,22 @@
 apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
 prefer 2 apply assumption
 apply (rule_tac [2] refl)
-apply (simp add: subset_refl [THEN TFin_UnionI, 
+apply (simp add: subset_refl [THEN TFin_UnionI,
                               THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
 apply (erule choice_not_equals [THEN notE])
 apply (assumption+)
 done
 
 
-subsection{*Zorn's Lemma*}
+subsection{*Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
+       then S contains a Maximal Element*}
 
-text{*If all chains in S have upper bounds in S,
-       then S contains a maximal element *}
-
-(*Used in the proof of Zorn's Lemma*)
-lemma chain_extend: 
-    "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
+text{*Used in the proof of Zorn's Lemma*}
+lemma chain_extend:
+    "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
 by (unfold chain_def, blast)
 
-lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
+lemma Zorn: "\<forall>c \<in> chain(S). Union(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z"
 apply (rule Hausdorff [THEN exE])
 apply (simp add: maxchain_def)
 apply (rename_tac c)
@@ -293,7 +291,7 @@
 apply safe
 apply (rename_tac z)
 apply (rule classical)
-apply (subgoal_tac "cons (z,c) : super (S,c) ")
+apply (subgoal_tac "cons (z,c) \<in> super (S,c) ")
 apply (blast elim: equalityE)
 apply (unfold super_def, safe)
 apply (fast elim: chain_extend)
@@ -303,20 +301,20 @@
 
 subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}
 
-(*Lemma 5*)
+text{*Lemma 5*}
 lemma TFin_well_lemma5:
-     "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]   
-      ==> ALL m:Z. n<=m"
+     "[| n \<in> TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) \<in> Z |]
+      ==> \<forall>m \<in> Z. n <= m"
 apply (erule TFin_induct)
-prefer 2 apply blast (*second induction step is easy*)
+prefer 2 apply blast txt{*second induction step is easy*}
 apply (rule ballI)
-apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) 
+apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
 apply (subgoal_tac "m = Inter (Z) ")
 apply blast+
 done
 
-(*Well-ordering of TFin(S,next)*)
-lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z:Z |] ==> Inter(Z) : Z"
+text{*Well-ordering of @{term "TFin(S,next)"} *}
+lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z \<in> Z |] ==> Inter(Z) \<in> Z"
 apply (rule classical)
 apply (subgoal_tac "Z = {Union (TFin (S,next))}")
 apply (simp (no_asm_simp) add: Inter_singleton)
@@ -325,26 +323,27 @@
 apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
 done
 
-(*This theorem just packages the previous result*)
+text{*This theorem just packages the previous result*}
 lemma well_ord_TFin:
-     "next: increasing(S) ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
+     "next \<in> increasing(S) 
+      ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
 apply (rule well_ordI)
 apply (unfold Subset_rel_def linear_def)
-(*Prove the well-foundedness goal*)
+txt{*Prove the well-foundedness goal*}
 apply (rule wf_onI)
 apply (frule well_ord_TFin_lemma, assumption)
 apply (drule_tac x = "Inter (Z) " in bspec, assumption)
 apply blast
-(*Now prove the linearity goal*)
+txt{*Now prove the linearity goal*}
 apply (intro ballI)
 apply (case_tac "x=y")
  apply blast
-(*The x~=y case remains*)
+txt{*The @{term "x\<noteq>y"} case remains*}
 apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
        assumption+, blast+)
 done
 
-(** Defining the "next" operation for Zermelo's Theorem **)
+text{** Defining the "next" operation for Zermelo's Theorem **}
 
 lemma choice_Diff:
      "[| ch \<in> (\<Pi>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
@@ -352,57 +351,58 @@
 apply (blast elim!: equalityE)
 done
 
-(*This justifies Definition 6.1*)
+text{*This justifies Definition 6.1*}
 lemma Zermelo_next_exists:
-     "ch: (PROD X: Pow(S)-{0}. X) ==>                
-           EX next: increasing(S). ALL X: Pow(S).        
+     "ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X) ==>
+           \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                       next`X = (if X=S then S else cons(ch`(S-X), X))"
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
        in bexI)
-apply force  
+apply force
 apply (unfold increasing_def)
 apply (rule CollectI)
 apply (rule lam_type)
-(*Type checking is surprisingly hard!*)
+txt{*Type checking is surprisingly hard!*}
 apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
 apply (blast intro!: choice_Diff [THEN DiffD1])
-(*Verify that it increases*)
-apply (intro allI impI) 
+txt{*Verify that it increases*}
+apply (intro allI impI)
 apply (simp add: Pow_iff subset_consI subset_refl)
 done
 
 
-(*The construction of the injection*)
+text{*The construction of the injection*}
 lemma choice_imp_injection:
-     "[| 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}))        
-               : inj(S, TFin(S,next) - {S})"
+     "[| ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X);
+         next \<in> increasing(S);
+         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
+      ==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
+               \<in> inj(S, TFin(S,next) - {S})"
 apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
 apply (rule DiffI)
 apply (rule Collect_subset [THEN TFin_UnionI])
 apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
-apply (subgoal_tac "x ~: Union ({y: TFin (S,next) . x~: y}) ")
+apply (subgoal_tac "x \<notin> Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
 prefer 2 apply (blast elim: equalityE)
-apply (subgoal_tac "Union ({y: TFin (S,next) . x~: y}) ~= S")
+apply (subgoal_tac "Union ({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
 prefer 2 apply (blast elim: equalityE)
-(*For proving x : next`Union(...)
-  Abrial & Laffitte's justification appears to be faulty.*)
-apply (subgoal_tac "~ next ` Union ({y: TFin (S,next) . x~: y}) <= Union ({y: TFin (S,next) . x~: y}) ")
-prefer 2
-apply (simp del: Union_iff 
-            add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] 
-            Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
-apply (subgoal_tac "x : next ` Union ({y: TFin (S,next) . x~: y}) ")
-prefer 2
-apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
-(*End of the lemmas!*)
+txt{*For proving @{text "x \<in> next`Union(...)"}.
+  Abrial and Laffitte's justification appears to be faulty.*}
+apply (subgoal_tac "~ next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) 
+                    <= Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
+ prefer 2
+ apply (simp del: Union_iff
+	     add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
+	     Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
+apply (subgoal_tac "x \<in> next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
+ prefer 2
+ apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
+txt{*End of the lemmas!*}
 apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
 done
 
-(*The wellordering theorem*)
-theorem AC_well_ord: "EX r. well_ord(S,r)"
+text{*The wellordering theorem*}
+theorem AC_well_ord: "\<exists>r. well_ord(S,r)"
 apply (rule AC_Pi_Pow [THEN exE])
 apply (rule Zermelo_next_exists [THEN bexE], assumption)
 apply (rule exI)
@@ -410,5 +410,5 @@
 apply (erule_tac [2] well_ord_TFin)
 apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
 done
-  
+
 end