Axiom of choice, cardinality results, etc.

--- a/src/ZF/WF.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/WF.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -95,7 +95,7 @@
 	   rename_last_tac a ["1"] (i+1),
 	   ares_tac prems i];
 
-(*The form of this rule is designed to match wfI2*)
+(*The form of this rule is designed to match wfI*)
 val wfr::amem::prems = goal WF.thy
     "[| wf(r);  a:A;  field(r)<=A;  \
 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
@@ -133,7 +133,7 @@
 \    ==>  wf(r)";
 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
 by (REPEAT (ares_tac [indhyp] 1));
-val wfI2 = result();
+val wfI = result();
 
 
 (*** Properties of well-founded relations ***)

--- a/src/ZF/ZF.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/ZF.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -39,6 +39,7 @@
   val InterD	: thm
   val InterE	: thm
   val InterI	: thm
+  val Inter_iff : thm
   val INT_E	: thm
   val INT_I	: thm
   val INT_cong	: thm
@@ -49,7 +50,9 @@
   val RepFunI	: thm
   val RepFun_eqI	: thm
   val RepFun_cong	: thm
+  val RepFun_iff	: thm
   val ReplaceE	: thm
+  val ReplaceE2	: thm
   val ReplaceI	: thm
   val Replace_iff	: thm
   val Replace_cong	: thm
@@ -244,7 +247,7 @@
 
 (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
 val ReplaceI = prove_goal ZF.thy
-    "[| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> \
+    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==> \
 \    b : {y. x:A, P(x,y)}"
  (fn prems=>
   [ (rtac (Replace_iff RS iffD2) 1),
@@ -260,6 +263,15 @@
     (etac conjE 2),
     (REPEAT (ares_tac prems 1)) ]);
 
+(*As above but without the (generally useless) 3rd assumption*)
+val ReplaceE2 = prove_goal ZF.thy 
+    "[| b : {y. x:A, P(x,y)};  \
+\       !!x. [| x: A;  P(x,b) |] ==> R \
+\    |] ==> R"
+ (fn major::prems=>
+  [ (rtac (major RS ReplaceE) 1),
+    (REPEAT (ares_tac prems 1)) ]);
+
 val Replace_cong = prove_goal ZF.thy
     "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
 \    Replace(A,P) = Replace(B,Q)"
@@ -295,6 +307,10 @@
     "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
  (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
 
+val RepFun_iff = prove_goalw ZF.thy [Bex_def]
+    "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
+ (fn _ => [ (fast_tac (FOL_cs addIs [RepFunI] addSEs [RepFunE]) 1) ]);
+
 
 (*** Rules for Collect -- forming a subset by separation ***)
 
@@ -335,13 +351,13 @@
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
 val UnionI = prove_goal ZF.thy "[| B: C;  A: B |] ==> A: Union(C)"
  (fn prems=>
-  [ (resolve_tac [union_iff RS iffD2] 1),
+  [ (resolve_tac [Union_iff RS iffD2] 1),
     (REPEAT (resolve_tac (prems @ [bexI]) 1)) ]);
 
 val UnionE = prove_goal ZF.thy
     "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
  (fn prems=>
-  [ (resolve_tac [union_iff RS iffD1 RS bexE] 1),
+  [ (resolve_tac [Union_iff RS iffD1 RS bexE] 1),
     (REPEAT (ares_tac prems 1)) ]);
 
 (*** Rules for Inter ***)
@@ -376,6 +392,11 @@
 (*** Rules for Unions of families ***)
 (* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
 
+val UN_iff = prove_goalw ZF.thy [Bex_def]
+    "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
+ (fn _=> [ (fast_tac (FOL_cs addIs [UnionI, RepFunI] 
+                             addSEs [UnionE, RepFunE]) 1) ]);
+
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 val UN_I = prove_goal ZF.thy "[| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))"
  (fn prems=>
@@ -395,6 +416,12 @@
 (*** Rules for Intersections of families ***)
 (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
 
+val INT_iff = prove_goal ZF.thy
+    "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
+ (fn _=> [ (simp_tac (FOL_ss addsimps [Inter_def, Ball_def, Bex_def, 
+				       separation, Union_iff, RepFun_iff]) 1),
+	   (fast_tac FOL_cs 1) ]);
+
 val INT_I = prove_goal ZF.thy
     "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))"
  (fn prems=>
@@ -415,10 +442,10 @@
 (*** Rules for Powersets ***)
 
 val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)"
- (fn [prem]=> [ (rtac (prem RS (power_set RS iffD2)) 1) ]);
+ (fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]);
 
 val PowD = prove_goal ZF.thy "A : Pow(B)  ==>  A<=B"
- (fn [major]=> [ (rtac (major RS (power_set RS iffD1)) 1) ]);
+ (fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]);
 
 
 (*** Rules for the empty set ***)
@@ -448,7 +475,7 @@
 val lemmas_cs = FOL_cs
   addSIs [ballI, InterI, CollectI, PowI, subsetI]
   addIs [bexI, UnionI, ReplaceI, RepFunI]
-  addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,
+  addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
 	  CollectE, emptyE]
   addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
 

--- a/src/ZF/ZF.thy	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/ZF.thy	Tue Jul 26 13:44:42 1994 +0200
@@ -133,8 +133,8 @@
         uniqueness is derivable using extensionality.  *)
 
 extension       "A = B <-> A <= B & B <= A"
-union_iff       "A : Union(C) <-> (EX B:C. A:B)"
-power_set       "A : Pow(B) <-> A <= B"
+Union_iff       "A : Union(C) <-> (EX B:C. A:B)"
+Pow_iff         "A : Pow(B) <-> A <= B"
 succ_def        "succ(i) == cons(i,i)"
 
  (*We may name this set, though it is not uniquely defined. *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Zorn.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -0,0 +1,406 @@
+(*  Title: 	ZF/Zorn.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Conclusion to proofs from the paper
+    Abrial & Laffitte, 
+    Towards the Mechanization of the Proofs of Some 
+    Classical Theorems of Set Theory. 
+*)
+
+
+structure Zorn = Inductive_Fun
+ (val thy        = Zorn0.thy |> add_consts [("TFin", "[i,i]=>i", NoSyn)]
+  val thy_name   = "Zorn"
+  val rec_doms   = [("TFin","Pow(S)")]
+  val sintrs     = ["[| x : TFin(S,next);  next: increasing(S) \
+\                    |] ==> next`x : TFin(S,next)",
+                    "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"]
+  val monos      = [Pow_mono]
+  val con_defs   = []
+  val type_intrs = [next_bounded, Union_in_Pow]
+  val type_elims = []);
+
+(*Introduction rules*)
+val [TFin_nextI, Pow_TFin_UnionI] = Zorn.intrs;
+val TFin_UnionI = PowI RS Pow_TFin_UnionI;
+
+val TFin_is_subset = Zorn.dom_subset RS subsetD RS PowD;
+
+
+(** Structural induction on TFin(S,next) **)
+
+val major::prems = goal Zorn.thy
+  "[| 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)) \
+\  |] ==> P(n)";
+by (rtac (major RS Zorn.induct) 1);
+by (ALLGOALS (fast_tac (ZF_cs addIs prems)));
+val TFin_induct = result();
+
+(*Perform induction on n, then prove the major premise using prems. *)
+fun TFin_ind_tac a prems i = 
+    EVERY [res_inst_tac [("n",a)] TFin_induct i,
+	   rename_last_tac a ["1"] (i+1),
+	   rename_last_tac a ["2"] (i+2),
+	   ares_tac prems i];
+
+(*** Section 3.  Some Properties of the Transfinite Construction ***)
+
+val increasing_trans = 
+    TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)) |> standard;
+
+(*Lemma 1 of section 3.1*)
+val major::prems = goal Zorn.thy
+    "[| n: TFin(S,next);  m: TFin(S,next);  \
+\       ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
+\    |] ==> n<=m | next`m<=n";
+by (cut_facts_tac prems 1);
+br (major RS TFin_induct) 1;
+by (etac Union_lemma0 2);		(*or just fast_tac ZF_cs*)
+by (fast_tac (subset_cs addIs [increasing_trans]) 1);
+val TFin_linear_lemma1 = result();
+
+(*Lemma 2 of section 3.2.  Interesting in its own right!
+  Requires next: increasing(S) in the second induction step. *)
+val [major,ninc] = goal Zorn.thy
+    "[| m: TFin(S,next);  next: increasing(S) \
+\    |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
+br (major RS TFin_induct) 1;
+br (impI RS ballI) 1;
+(*case split using TFin_linear_lemma1*)
+by (res_inst_tac [("n1","n"), ("m1","x")] 
+    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
+by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
+by (fast_tac (subset_cs addIs [increasing_trans]) 1);
+by (REPEAT (ares_tac [disjI1,equalityI] 1));
+(*second induction step*)
+br (impI RS ballI) 1;
+br (Union_lemma0 RS disjE) 1;
+be disjI2 3;
+by (REPEAT (ares_tac [disjI1,equalityI] 2));
+br ballI 1;
+by (ball_tac 1);
+by (set_mp_tac 1);
+by (res_inst_tac [("n1","n"), ("m1","x")] 
+    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
+by (fast_tac subset_cs 1);
+br (ninc RS increasingD2 RS subset_trans RS disjI1) 1;
+by (REPEAT (ares_tac [TFin_is_subset] 1));
+val TFin_linear_lemma2 = result();
+
+(*a more convenient form for Lemma 2*)
+goal Zorn.thy
+    "!!m n. [| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
+\           |] ==> n=m | next`n<=m";
+br (TFin_linear_lemma2 RS bspec RS mp) 1;
+by (REPEAT (assume_tac 1));
+val TFin_subsetD = result();
+
+(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
+goal Zorn.thy
+    "!!m n. [| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
+\           |] ==> n<=m | m<=n";
+br (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1;
+by (REPEAT (assume_tac 1) THEN etac disjI2 1);
+by (fast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
+			       TFin_is_subset]) 1);
+val TFin_subset_linear = result();
+
+
+(*Lemma 3 of section 3.3*)
+val major::prems = goal Zorn.thy
+    "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m";
+by (cut_facts_tac prems 1);
+br (major RS TFin_induct) 1;
+bd TFin_subsetD 1;
+by (REPEAT (assume_tac 1));
+by (fast_tac (ZF_cs addEs [ssubst]) 1);
+by (fast_tac (subset_cs addIs [TFin_is_subset]) 1);
+val equal_next_upper = result();
+
+(*Property 3.3 of section 3.3*)
+goal Zorn.thy
+    "!!m. [| m: TFin(S,next);  next: increasing(S) \
+\         |] ==> m = next`m <-> m = Union(TFin(S,next))";
+br iffI 1;
+br (Union_upper RS equalityI) 1;
+br (equal_next_upper RS Union_least) 2;
+by (REPEAT (assume_tac 1));
+be ssubst 1;
+by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1);
+by (ALLGOALS
+    (fast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
+val equal_next_Union = result();
+
+
+(*** Section 4.  Hausdorff's Theorem: every set contains a maximal chain ***)
+(*** NB: We assume the partial ordering is <=, the subset relation! **)
+
+(** Defining the "next" operation for Hausdorff's Theorem **)
+
+goalw Zorn.thy [chain_def] "chain(A) <= Pow(A)";
+by (resolve_tac [Collect_subset] 1);
+val chain_subset_Pow = result();
+
+goalw Zorn.thy [super_def] "super(A,c) <= chain(A)";
+by (resolve_tac [Collect_subset] 1);
+val super_subset_chain = result();
+
+goalw Zorn.thy [maxchain_def] "maxchain(A) <= chain(A)";
+by (resolve_tac [Collect_subset] 1);
+val maxchain_subset_chain = result();
+
+goal Zorn.thy
+    "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X);	\
+\            X : chain(S);  X ~: maxchain(S)		\
+\         |] ==> ch ` super(S,X) : super(S,X)";
+by (eresolve_tac [apply_type] 1);
+by (rewrite_goals_tac [super_def, maxchain_def]);
+by (fast_tac ZF_cs 1);
+val choice_super = result();
+
+goal Zorn.thy
+    "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X);	\
+\            X : chain(S);  X ~: maxchain(S)		\
+\         |] ==> ch ` super(S,X) ~= X";
+by (resolve_tac [notI] 1);
+by (dresolve_tac [choice_super] 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps [super_def]) 1);
+val choice_not_equals = result();
+
+(*This justifies Definition 4.4*)
+goal Zorn.thy
+    "!!S. 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)";
+by (rtac bexI 1);
+by (rtac ballI 1);
+by (resolve_tac [beta] 1);
+by (assume_tac 1);
+bw increasing_def;
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
+by (fast_tac (ZF_cs addSIs [super_subset_chain RS subsetD,
+			    chain_subset_Pow RS subsetD,
+			    choice_super]) 1);
+(*Now, verify that it increases*)
+by (resolve_tac [allI] 1);
+by (resolve_tac [impI] 1);
+by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl]
+                        setloop split_tac [expand_if]) 1);
+by (safe_tac ZF_cs);
+by (dresolve_tac [choice_super] 1);
+by (REPEAT (assume_tac 1));
+bw super_def;
+by (fast_tac ZF_cs 1);
+val Hausdorff_next_exists = result();
+
+(*Lemma 4*)
+goal Zorn.thy
+ "!!S. [| 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)";
+by (eresolve_tac [TFin_induct] 1);
+by (asm_simp_tac 
+    (ZF_ss addsimps [chain_subset_Pow RS subsetD, 
+		     choice_super RS (super_subset_chain RS subsetD)]
+           setloop split_tac [expand_if]) 1);
+bw chain_def;
+by (rtac CollectI 1 THEN fast_tac ZF_cs 1);
+(*Cannot use safe_tac: the disjunction must be left alone*)
+by (REPEAT (rtac ballI 1 ORELSE etac UnionE 1));
+by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
+(*fast_tac is just too slow here!*)
+by (DEPTH_SOLVE (eresolve_tac [asm_rl, subsetD] 1
+       ORELSE ball_tac 1 THEN etac (CollectD2 RS bspec RS bspec) 1));
+val TFin_chain_lemma4 = result();
+
+goal Zorn.thy "EX c. c : maxchain(S)";
+by (rtac (AC_Pi_Pow RS exE) 1);
+by (rtac (Hausdorff_next_exists RS bexE) 1);
+by (assume_tac 1);
+by (rename_tac "ch next" 1);
+by (subgoal_tac "Union(TFin(S,next)) : chain(S)" 1);
+by (REPEAT (ares_tac [TFin_chain_lemma4, subset_refl RS TFin_UnionI] 2));
+by (res_inst_tac [("x", "Union(TFin(S,next))")] exI 1);
+by (resolve_tac [classical] 1);
+by (subgoal_tac "next ` Union(TFin(S,next)) = Union(TFin(S,next))" 1);
+by (resolve_tac [equal_next_Union RS iffD2 RS sym] 2);
+by (resolve_tac [subset_refl RS TFin_UnionI] 2);
+by (assume_tac 2);
+by (resolve_tac [refl] 2);
+by (asm_full_simp_tac 
+    (ZF_ss addsimps [subset_refl RS TFin_UnionI RS
+		     (Zorn.dom_subset RS subsetD)]
+           setloop split_tac [expand_if]) 1);
+by (eresolve_tac [choice_not_equals RS notE] 1);
+by (REPEAT (assume_tac 1));
+val Hausdorff = result();
+
+
+(*** Section 5.  Zorn's Lemma: if all chains in S have upper bounds in S 
+                               then S contains a maximal element ***)
+
+(*Used in the proof of Zorn's Lemma*)
+goalw Zorn.thy [chain_def]
+    "!!c. [| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
+by (fast_tac ZF_cs 1);
+val chain_extend = result();
+
+goal Zorn.thy
+    "!!S. ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z";
+by (resolve_tac [Hausdorff RS exE] 1);
+by (asm_full_simp_tac (ZF_ss addsimps [maxchain_def]) 1);
+by (rename_tac "c" 1);
+by (res_inst_tac [("x", "Union(c)")] bexI 1);
+by (fast_tac ZF_cs 2);
+by (safe_tac ZF_cs);
+by (rename_tac "z" 1);
+by (resolve_tac [classical] 1);
+by (subgoal_tac "cons(z,c): super(S,c)" 1);
+by (fast_tac (ZF_cs addEs [equalityE]) 1);
+bw super_def;
+by (safe_tac eq_cs);
+by (fast_tac (ZF_cs addEs [chain_extend]) 1);
+by (best_tac (ZF_cs addEs [equalityE]) 1);
+val Zorn = result();
+
+
+(*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
+
+(*Lemma 5*)
+val major::prems = goal Zorn.thy
+    "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z	\
+\    |] ==> ALL m:Z. n<=m";
+by (cut_facts_tac prems 1);
+br (major RS TFin_induct) 1;
+by (fast_tac ZF_cs 2);			(*second induction step is easy*)
+br ballI 1;
+br (bspec RS TFin_subsetD RS disjE) 1;
+by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
+by (subgoal_tac "x = Inter(Z)" 1);
+by (fast_tac ZF_cs 1);
+by (fast_tac eq_cs 1);
+val TFin_well_lemma5 = result();
+
+(*Well-ordering of TFin(S,next)*)
+goal Zorn.thy "!!Z. [| Z <= TFin(S,next);  z:Z |] ==> Inter(Z) : Z";
+br classical 1;
+by (subgoal_tac "Z = {Union(TFin(S,next))}" 1);
+by (asm_simp_tac (ZF_ss addsimps [Inter_singleton]) 1);
+be equal_singleton 1;
+br (Union_upper RS equalityI) 1;
+br (subset_refl RS TFin_UnionI RS TFin_well_lemma5 RS bspec) 2;
+by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
+val well_ord_TFin_lemma = result();
+
+(*This theorem just packages the previous result*)
+goal Zorn.thy
+    "!!S. next: increasing(S) ==> \
+\         well_ord(TFin(S,next), Subset_rel(TFin(S,next)))";
+by (resolve_tac [well_ordI] 1);
+by (rewrite_goals_tac [Subset_rel_def, linear_def]);
+(*Prove the linearity goal first*)
+by (REPEAT (rtac ballI 2));
+by (excluded_middle_tac "x=y" 2);
+by (fast_tac ZF_cs 3);
+(*The x~=y case remains*)
+by (res_inst_tac [("n1","x"), ("m1","y")] 
+    (TFin_subset_linear RS disjE) 2  THEN  REPEAT (assume_tac 2));
+by (fast_tac ZF_cs 2);
+by (fast_tac ZF_cs 2);
+(*Now prove the well_foundedness goal*)
+by (resolve_tac [wf_onI] 1);
+by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
+by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
+by (fast_tac eq_cs 1);
+val well_ord_TFin = result();
+
+(** Defining the "next" operation for Zermelo's Theorem **)
+
+goal AC.thy
+    "!!S. [| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S	\
+\         |] ==> ch ` (S-X) : S-X";
+by (eresolve_tac [apply_type] 1);
+by (fast_tac (eq_cs addEs [equalityE]) 1);
+val choice_Diff = result();
+
+(*This justifies Definition 6.1*)
+goal Zorn.thy
+    "!!S. ch: (PROD X: Pow(S)-{0}. X) ==>		\
+\          EX next: increasing(S). ALL X: Pow(S). 	\
+\                     next`X = if(X=S, S, cons(ch`(S-X), X))";
+by (rtac bexI 1);
+by (rtac ballI 1);
+by (resolve_tac [beta] 1);
+by (assume_tac 1);
+bw increasing_def;
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+(*Verify that it increases*)
+by (resolve_tac [allI] 2);
+by (resolve_tac [impI] 2);
+by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_consI, subset_refl]
+                        setloop split_tac [expand_if]) 2);
+(*Type checking is surprisingly hard!*)
+by (asm_simp_tac (ZF_ss addsimps [Pow_iff, cons_subset_iff, subset_refl]
+                        setloop split_tac [expand_if]) 1);
+by (fast_tac (ZF_cs addSIs [choice_Diff RS DiffD1]) 1);
+val Zermelo_next_exists = result();
+
+
+(*The construction of the injection*)
+goal Zorn.thy
+  "!!S. [| 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})";
+by (res_inst_tac [("d", "%y. ch`(S-y)")] lam_injective 1);
+by (rtac DiffI 1);
+by (resolve_tac [Collect_subset RS TFin_UnionI] 1);
+by (fast_tac (ZF_cs addSIs [Collect_subset RS TFin_UnionI]
+                    addEs [equalityE]) 1);
+by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1);
+by (fast_tac (ZF_cs addEs [equalityE]) 2);
+by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1);
+by (fast_tac (ZF_cs addEs [equalityE]) 2);
+(*For proving x : next`Union(...);
+  Abrial & Laffitte's justification appears to be faulty.*)
+by (subgoal_tac "~ next ` Union({y: TFin(S,next). x~: y}) <= \
+\                  Union({y: TFin(S,next). x~: y})" 1);
+by (asm_simp_tac 
+    (ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
+		     Pow_iff, cons_subset_iff, subset_refl,
+		     choice_Diff RS DiffD2]
+           setloop split_tac [expand_if]) 2);
+by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
+by (fast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
+(*End of the lemmas!*)
+by (asm_full_simp_tac 
+    (ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
+		     Pow_iff, cons_subset_iff, subset_refl]
+           setloop split_tac [expand_if]) 1);
+by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1));
+val choice_imp_injection = result();
+
+(*The wellordering theorem*)
+goal Zorn.thy "EX r. well_ord(S,r)";
+by (rtac (AC_Pi_Pow RS exE) 1);
+by (rtac (Zermelo_next_exists RS bexE) 1);
+by (assume_tac 1);
+br exI 1;
+by (resolve_tac [well_ord_rvimage] 1);
+by (eresolve_tac [well_ord_TFin] 2);
+by (resolve_tac [choice_imp_injection RS inj_weaken_type] 1);
+by (REPEAT (ares_tac [Diff_subset] 1));
+val AC_well_ord = result();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Zorn.thy	Tue Jul 26 13:44:42 1994 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+Zorn = Zorn0

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Zorn0.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -0,0 +1,56 @@
+(*  Title: 	ZF/Zorn0.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Preamble to proofs from the paper
+    Abrial & Laffitte, 
+    Towards the Mechanization of the Proofs of Some 
+    Classical Theorems of Set Theory. 
+*)
+
+
+(*** Section 1.  Mathematical Preamble ***)
+
+goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+by (fast_tac ZF_cs 1);
+val Union_lemma0 = result();
+
+goal ZF.thy
+    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
+by (fast_tac ZF_cs 1);
+val Inter_lemma0 = result();
+
+open Zorn0;
+
+(*** Section 2.  The Transfinite Construction ***)
+
+goalw Zorn0.thy [increasing_def]
+    "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
+by (eresolve_tac [CollectD1] 1);
+val increasingD1 = result();
+
+goalw Zorn0.thy [increasing_def]
+    "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
+by (eresolve_tac [CollectD2 RS spec RS mp] 1);
+by (assume_tac 1);
+val increasingD2 = result();
+
+goal Zorn0.thy
+    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
+by (eresolve_tac [increasingD1 RS apply_type] 1);
+by (assume_tac 1);
+val next_bounded = result();
+
+(*Trivial to prove here; hard to prove within Inductive_Fun*)
+goal ZF.thy "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
+by (fast_tac ZF_cs 1);
+val Union_in_Pow = result();
+
+(** We could make the inductive definition conditional on next: 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
+    are therefore unconditional.
+**)
+    
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Zorn0.thy	Tue Jul 26 13:44:42 1994 +0200
@@ -0,0 +1,28 @@
+(*  Title: 	ZF/Zorn0.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Based upon the article
+    Abrial & Laffitte, 
+    Towards the Mechanization of the Proofs of Some 
+    Classical Theorems of Set Theory. 
+*)
+
+Zorn0 = OrderArith + AC + "inductive" +
+
+consts
+  Subset_rel      :: "i=>i"
+  increasing      :: "i=>i"
+  chain, maxchain :: "i=>i"
+  super           :: "[i,i]=>i"
+
+rules
+  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
+  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+
+  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
+  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
+  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
+
+end

--- a/src/ZF/func.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/func.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -40,7 +40,7 @@
 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
 val Pi_cong = result();
 
-(*Weaking one function type to another*)
+(*Weakening one function type to another; see also Pi_type*)
 goalw ZF.thy [Pi_def] "!!f. [| f: A->B;  B<=D |] ==> f: A->D";
 by (safe_tac ZF_cs);
 by (set_mp_tac 1);
@@ -56,7 +56,6 @@
 by (fast_tac (ZF_cs addIs [equalityI]) 1);
 val Pi_empty2 = result();
 
-
 (*** Function Application ***)
 
 goal ZF.thy "!!a b f. [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
@@ -381,3 +380,23 @@
 by (REPEAT (ares_tac [fun_extend,fun_empty,notI] 1 ORELSE etac emptyE 1));
 val fun_single = result();
 
+goal ZF.thy
+    "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
+by (safe_tac eq_cs);
+(*Inclusion of right into left is easy*)
+by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 2);
+(*Inclusion of left into right*)
+by (subgoal_tac "restrict(x, A) : A -> B" 1);
+by (fast_tac (ZF_cs addEs [restrict_type2]) 2);
+by (rtac UN_I 1 THEN assume_tac 1);
+by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1);
+by (subgoal_tac "x = cons(<c, x ` c>, restrict(x, A))" 1);
+by (fast_tac ZF_cs 1);
+(*Proving the lemma*)
+by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1));
+by (etac consE 1);
+by (ALLGOALS 
+    (asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 
+				   fun_extend_apply2])));
+val cons_fun_eq = result();
+

--- a/src/ZF/mono.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/mono.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -11,7 +11,7 @@
 (*Not easy to express monotonicity in P, since any "bigger" predicate
   would have to be single-valued*)
 goal ZF.thy "!!A B. A<=B ==> Replace(A,P) <= Replace(B,P)";
-by (fast_tac ZF_cs 1);
+by (fast_tac (ZF_cs addSEs [ReplaceE]) 1);
 val Replace_mono = result();
 
 goal ZF.thy "!!A B. A<=B ==> {f(x). x:A} <= {f(x). x:B}";

--- a/src/ZF/simpdata.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/simpdata.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -95,7 +95,7 @@
 
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
-		triv_RepFun];
+		triv_RepFun, subset_refl];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause
   flex-flex pairs and the "Check your prover" error -- because most

--- a/src/ZF/simpdata.thy	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/simpdata.thy	Tue Jul 26 13:44:42 1994 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-simpdata = "func"
\ No newline at end of file
+simpdata = "func"

--- a/src/ZF/upair.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/upair.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -99,14 +99,14 @@
  (fn [major]=> [ (rtac (major RS CollectD1) 1) ]);
 
 val DiffD2 = prove_goalw ZF.thy [Diff_def]
-    "[| c : A - B;  c : B |] ==> P"
- (fn [major,minor]=> [ (rtac (minor RS (major RS CollectD2 RS notE)) 1) ]);
+    "c : A - B ==> c ~: B"
+ (fn [major]=> [ (rtac (major RS CollectD2) 1) ]);
 
 val DiffE = prove_goal ZF.thy
     "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
-    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
+    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]);
 
 val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & c~:B)"
  (fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
@@ -174,7 +174,7 @@
 val the_0 = prove_goalw ZF.thy [the_def]
     "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
  (fn _ =>
-  [ (fast_tac (lemmas_cs addIs [equalityI]) 1) ]);
+  [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]);
 
 
 (*** if -- a conditional expression for formulae ***)