# HG changeset patch
# User paulson
# Date 1021063808 -7200
# Node ID bf37a3049251500fa92d5d17404d66f0480d0c18
# Parent  03d20664cb792ce6b99b38319579d06af703eee7
converted the AC branch to Isar

diff -r 03d20664cb79 -r bf37a3049251 src/ZF/AC.thy
--- a/src/ZF/AC.thy	Fri May 10 18:00:48 2002 +0200
+++ b/src/ZF/AC.thy	Fri May 10 22:50:08 2002 +0200
@@ -8,13 +8,59 @@
 This definition comes from Halmos (1960), page 59.
 *)
 
-AC = func +
+theory AC = Main:
+
+axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
+
+(*The same as AC, but no premise a \<in> A*)
+lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
+apply (case_tac "A=0")
+apply (simp add: Pi_empty1, blast)
+(*The non-trivial case*)
+apply (blast intro: AC)
+done
+
+(*Using dtac, this has the advantage of DELETING the universal quantifier*)
+lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
+apply (rule AC_Pi)
+apply (erule bspec)
+apply assumption
+done
+
+lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
+apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
+apply (erule_tac [2] exI)
+apply blast
+done
 
-constdefs
-  (*Needs to be visible for Zorn.thy*)
-  increasing :: i=>i
-    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
+lemma AC_func:
+     "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
+apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
+prefer 2 apply (blast dest: apply_type intro: Pi_type)
+apply (blast intro: elim:); 
+done
+
+lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
+apply (subgoal_tac "x \<noteq> 0")
+apply blast+
+done
 
-rules
-  AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
+lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
+apply (rule AC_func)
+apply (simp_all add: non_empty_family) 
+done
+
+lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
+apply (rule AC_func0 [THEN bexE])
+apply (rule_tac [2] bexI)
+prefer 2 apply (assumption)
+apply (erule_tac [2] fun_weaken_type)
+apply blast+
+done
+
+lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
+apply (rule AC_Pi)
+apply (simp_all add: non_empty_family) 
+done
+
 end
diff -r 03d20664cb79 -r bf37a3049251 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Fri May 10 18:00:48 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy	Fri May 10 22:50:08 2002 +0200
@@ -4,6 +4,180 @@
     Copyright   1994  University of Cambridge
 
 Cardinal Arithmetic WITH the Axiom of Choice
+
+These results help justify infinite-branching datatypes
 *)
 
-Cardinal_AC = CardinalArith + Zorn
+theory Cardinal_AC = CardinalArith + Zorn:
+
+(*** Strengthened versions of existing theorems about cardinals ***)
+
+lemma cardinal_eqpoll: "|A| eqpoll A"
+apply (rule AC_well_ord [THEN exE])
+apply (erule well_ord_cardinal_eqpoll)
+done
+
+lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard]
+
+lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule well_ord_cardinal_eqE)
+apply assumption+
+done
+
+lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
+apply (blast intro: cardinal_cong cardinal_eqE)
+done
+
+lemma cardinal_disjoint_Un: "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==>  
+          |A Un C| = |B Un D|"
+apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
+done
+
+lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
+apply (rule AC_well_ord [THEN exE])
+apply (erule well_ord_lepoll_imp_Card_le)
+apply assumption
+done
+
+lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule well_ord_cadd_assoc)
+apply assumption+
+done
+
+lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule well_ord_cmult_assoc)
+apply assumption+
+done
+
+lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule AC_well_ord [THEN exE])
+apply (rule well_ord_cadd_cmult_distrib)
+apply assumption+
+done
+
+lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
+apply (rule AC_well_ord [THEN exE])
+apply (erule well_ord_InfCard_square_eq)
+apply assumption
+done
+
+
+(*** Other applications of AC ***)
+
+lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
+apply (rule cardinal_eqpoll
+              [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
+apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
+apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
+done
+
+lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
+apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
+       erule Card_le_imp_lepoll);
+apply (erule lepoll_imp_Card_le) 
+done
+
+lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
+apply (unfold surj_def)
+apply (erule CollectE)
+apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
+apply (fast elim!: apply_Pair)
+apply (blast dest: apply_type Pi_memberD intro: apply_equality Pi_type f_imp_injective)
+done
+
+(*Kunen's Lemma 10.20*)
+lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| le |X|"
+apply (rule lepoll_imp_Card_le)
+apply (erule surj_implies_inj [THEN exE])
+apply (unfold lepoll_def)
+apply (erule exI)
+done
+
+(*Kunen's Lemma 10.21*)
+lemma cardinal_UN_le: "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"
+apply (simp add: InfCard_is_Card le_Card_iff)
+apply (rule lepoll_trans)
+ prefer 2
+ apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
+ apply (simp add: InfCard_is_Card Card_cardinal_eq)
+apply (unfold lepoll_def)
+apply (frule InfCard_is_Card [THEN Card_is_Ord])
+apply (erule AC_ball_Pi [THEN exE])
+apply (rule exI)
+(*Lemma needed in both subgoals, for a fixed z*)
+apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K")
+ prefer 2
+ apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
+             elim!: LeastI Ord_in_Ord)
+apply (rule_tac c = "%z. <LEAST i. z:X (i) , f ` (LEAST i. z:X (i)) ` z>" 
+            and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
+(*Instantiate the lemma proved above*)
+apply (blast intro: inj_is_fun [THEN apply_type] dest: apply_type)
+apply (force ); 
+done
+
+
+(*The same again, using csucc*)
+lemma cardinal_UN_lt_csucc:
+     "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
+      ==> |UN i:K. X(i)| < csucc(K)"
+apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
+done
+
+(*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
+  the least ordinal j such that i:Vfrom(A,j). *)
+lemma cardinal_UN_Ord_lt_csucc:
+     "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
+      ==> (UN i:K. j(i)) < csucc(K)"
+apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt])
+apply assumption
+apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
+apply (blast intro!: Ord_UN elim: ltE)
+apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
+done
+
+
+(** Main result for infinite-branching datatypes.  As above, but the index
+    set need not be a cardinal.  Surprisingly complicated proof!
+**)
+
+(*Work backwards along the injection from W into K, given that W~=0.*)
+lemma inj_UN_subset:
+     "[| f: inj(A,B);  a:A |] ==>            
+      (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"
+apply (rule UN_least)
+apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
+ apply (simp add: inj_is_fun [THEN apply_rangeI])
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
+  be weaker.*)
+lemma le_UN_Ord_lt_csucc:
+     "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
+      ==> (UN w:W. j(w)) < csucc(K)"
+apply (case_tac "W=0")
+(*solve the easy 0 case*)
+ apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] 
+                  Card_is_Ord Ord_0_lt_csucc)
+apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
+apply (safe intro!: equalityI)
+apply (erule swap); 
+apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc])
+apply assumption+
+ apply (simp add: inj_converse_fun [THEN apply_type])
+apply (blast intro!: Ord_UN elim: ltE)
+done
+
+end
+
diff -r 03d20664cb79 -r bf37a3049251 src/ZF/InfDatatype.thy
--- a/src/ZF/InfDatatype.thy	Fri May 10 18:00:48 2002 +0200
+++ b/src/ZF/InfDatatype.thy	Fri May 10 22:50:08 2002 +0200
@@ -1,1 +1,107 @@
-InfDatatype = Datatype + Univ + Finite + Cardinal_AC
+(*  Title:      ZF/InfDatatype.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Infinite-branching datatype definitions
+*)
+
+theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC:
+
+lemmas fun_Limit_VfromE = 
+    Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
+
+lemma fun_Vcsucc_lemma:
+     "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]   
+      ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"
+apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
+apply (rule conjI)
+apply (rule_tac [2] le_UN_Ord_lt_csucc) 
+apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE)
+apply (simp_all add: ) 
+ prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
+apply (rule Pi_type)
+apply (rename_tac [2] d)
+apply (erule_tac [2] fun_Limit_VfromE, simp_all)
+apply (subgoal_tac "f`d : Vfrom (A, LEAST i. f`d : Vfrom (A,i))")
+ apply (erule Vfrom_mono [OF subset_refl UN_upper, THEN subsetD])
+ apply assumption
+apply (fast elim: LeastI ltE)
+done
+
+lemma subset_Vcsucc:
+     "[| D <= Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]     
+      ==> EX j. D <= Vfrom(A,j) & j < csucc(K)"
+by (simp add: subset_iff_id fun_Vcsucc_lemma)
+
+(*Version for arbitrary index sets*)
+lemma fun_Vcsucc:
+     "[| |D| le K;  InfCard(K);  D <= Vfrom(A,csucc(K)) |] ==>  
+          D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
+apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc)
+apply (rule Vfrom [THEN ssubst])
+apply (drule fun_is_rel)
+(*This level includes the function, and is below csucc(K)*)
+apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
+apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
+                    Un_least_lt); 
+apply (erule subset_trans [THEN PowI])
+apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
+done
+
+lemma fun_in_Vcsucc:
+     "[| f: D -> Vfrom(A, csucc(K));  |D| le K;  InfCard(K);         
+         D <= Vfrom(A,csucc(K)) |]                                   
+       ==> f: Vfrom(A,csucc(K))"
+by (blast intro: fun_Vcsucc [THEN subsetD])
+
+(*Remove <= from the rule above*)
+lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
+
+(** Version where K itself is the index set **)
+
+lemma Card_fun_Vcsucc:
+     "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
+apply (frule InfCard_is_Card [THEN Card_is_Ord])
+apply (blast del: subsetI
+	     intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom 
+                   lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans]) 
+done
+
+lemma Card_fun_in_Vcsucc:
+     "[| f: K -> Vfrom(A, csucc(K));  InfCard(K) |] ==> f: Vfrom(A,csucc(K))"
+by (blast intro: Card_fun_Vcsucc [THEN subsetD]) 
+
+lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))"
+by (erule InfCard_csucc [THEN InfCard_is_Limit])
+
+lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc]
+lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc]
+lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc]
+lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit]
+lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc]
+
+(*For handling Cardinals of the form  (nat Un |X|) *)
+
+lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal]
+
+lemmas le_nat_Un_cardinal =
+     Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
+
+lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
+
+(*The new version of Data_Arg.intrs, declared in Datatype.ML*)
+lemmas Data_Arg_intros =
+       SigmaI InlI InrI
+       Pair_in_univ Inl_in_univ Inr_in_univ 
+       zero_in_univ A_into_univ nat_into_univ UnCI
+
+(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
+lemmas inf_datatype_intros =
+     InfCard_nat InfCard_nat_Un_cardinal
+     Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc 
+     zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc
+     Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I 
+
+end
+
diff -r 03d20664cb79 -r bf37a3049251 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Fri May 10 18:00:48 2002 +0200
+++ b/src/ZF/Zorn.thy	Fri May 10 22:50:08 2002 +0200
@@ -11,20 +11,25 @@
 Union_in_Pow is proved in ZF.ML
 *)
 
-Zorn = OrderArith + AC + Inductive +
+theory Zorn = OrderArith + AC + Inductive:
 
-consts
-  Subset_rel      :: i=>i
-  chain, maxchain :: i=>i
-  super           :: [i,i]=>i
+constdefs
+  Subset_rel :: "i=>i"
+   "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
+
+  chain      :: "i=>i"
+   "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
 
-defs
-  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
+  maxchain   :: "i=>i"
+   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
+  
+  super      :: "[i,i]=>i"
+   "super(A,c)    == {d: chain(A). c<=d & c~=d}"
 
-  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}"
 
+constdefs
+  increasing :: "i=>i"
+    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
 
 (** We could make the inductive definition conditional on next: increasing(S)
     but instead we make this a side-condition of an introduction rule.  Thus
@@ -32,18 +37,391 @@
     are therefore unconditional.
 **)
 consts
-  "TFin" :: [i,i]=>i
+  "TFin" :: "[i,i]=>i"
 
 inductive
   domains       "TFin(S,next)" <= "Pow(S)"
-  intrs
-    nextI       "[| x : TFin(S,next);  next: increasing(S) 
-                |] ==> next`x : TFin(S,next)"
+  intros
+    nextI:       "[| x : TFin(S,next);  next: increasing(S) |]
+                  ==> next`x : TFin(S,next)"
 
-    Pow_UnionI  "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
+    Pow_UnionI: "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
 
   monos         Pow_mono
   con_defs      increasing_def
-  type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
+  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
+
+
+(*** Section 1.  Mathematical Preamble ***)
+
+lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
+apply blast
+done
+
+lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
+apply blast
+done
+
+
+(*** Section 2.  The Transfinite Construction ***)
+
+lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)"
+apply (unfold increasing_def)
+apply (erule CollectD1)
+done
+
+lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
+apply (unfold increasing_def)
+apply (blast intro: elim:); 
+done
+
+lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
+
+lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
+
+
+(** Structural induction on 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))  
+   |] ==> P(n)"
+apply (erule TFin.induct)
+apply blast+
+done
+
+
+(*** Section 3.  Some Properties of the Transfinite Construction ***)
+
+lemmas increasing_trans = subset_trans [OF _ increasingD2, 
+                                        OF _ _ TFin_is_subset]
+
+(*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<=m | next`m<=n"
+apply (erule TFin_induct)
+apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
+(*downgrade subsetI from intro! to intro*)
+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. *)
+lemma TFin_linear_lemma2:
+    "[| m: TFin(S,next);  next: increasing(S) |] 
+     ==> ALL n: 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*)
+apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+       assumption+)
+apply (blast del: subsetI
+	     intro: increasing_trans subsetI)
+apply (blast intro: elim:); 
+(*second induction step*)
+apply (rule impI [THEN ballI])
+apply (rule Union_lemma0 [THEN disjE])
+apply (erule_tac [3] disjI2)
+prefer 2 apply (blast intro: elim:); 
+apply (rule ballI)
+apply (drule bspec, assumption) 
+apply (drule subsetD, assumption) 
+apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+       assumption+)
+apply (blast intro: elim:); 
+apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
+apply (blast dest: TFin_is_subset)+
+done
+
+(*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]) 
+
+(*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) 
+apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
+apply (assumption+, erule disjI2)
+apply (blast del: subsetI 
+             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
+done
+
+
+(*Lemma 3 of section 3.3*)
+lemma equal_next_upper:
+     "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m"
+apply (erule TFin_induct)
+apply (drule TFin_subsetD)
+apply (assumption+)
+apply (force ); 
+apply (blast)
+done
+
+(*Property 3.3 of section 3.3*)
+lemma equal_next_Union: "[| m: TFin(S,next);  next: increasing(S) |]   
+      ==> m = next`m <-> m = Union(TFin(S,next))"
+apply (rule iffI)
+apply (rule Union_upper [THEN equalityI])
+apply (rule_tac [2] equal_next_upper [THEN Union_least])
+apply (assumption+)
+apply (erule ssubst)
+apply (rule increasingD2 [THEN equalityI] , assumption)
+apply (blast del: subsetI
+	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
+done
+
+
+(*** 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 **)
+
+lemma chain_subset_Pow: "chain(A) <= Pow(A)"
+apply (unfold chain_def)
+apply (rule Collect_subset)
+done
+
+lemma super_subset_chain: "super(A,c) <= chain(A)"
+apply (unfold super_def)
+apply (rule Collect_subset)
+done
+
+lemma maxchain_subset_chain: "maxchain(A) <= chain(A)"
+apply (unfold maxchain_def)
+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)"
+apply (erule apply_type)
+apply (unfold super_def maxchain_def)
+apply 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"
+apply (rule notI)
+apply (drule choice_super)
+apply assumption
+apply assumption
+apply (simp add: super_def)
+done
+
+(*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 bexI)
+apply (rule ballI)
+apply (rule beta)
+apply assumption
+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 (simp (no_asm_simp) add: Pow_iff subset_refl)
+apply safe
+apply (drule choice_super)
+apply (assumption+)
+apply (unfold super_def)
+apply blast
+done
+
+(*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)"
+apply (erule TFin_induct)
+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)
+apply safe
+apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE])
+apply fast+ (*Blast_tac's slow*)
+done
+
+lemma Hausdorff: "EX c. c : maxchain(S)"
+apply (rule AC_Pi_Pow [THEN exE])
+apply (rule Hausdorff_next_exists [THEN bexE])
+apply assumption
+apply (rename_tac ch "next")
+apply (subgoal_tac "Union (TFin (S,next)) : 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)
+apply (rule classical)
+apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
+apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
+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, 
+                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
+apply (erule choice_not_equals [THEN notE])
+apply (assumption+)
+done
+
+
+(*** 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*)
+lemma chain_extend: 
+    "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
+apply (unfold chain_def)
+apply blast
+done
+
+lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
+apply (rule Hausdorff [THEN exE])
+apply (simp add: maxchain_def)
+apply (rename_tac c)
+apply (rule_tac x = "Union (c)" in bexI)
+prefer 2 apply (blast)
+apply safe
+apply (rename_tac z)
+apply (rule classical)
+apply (subgoal_tac "cons (z,c) : super (S,c) ")
+apply (blast elim: equalityE)
+apply (unfold super_def)
+apply safe
+apply (fast elim: chain_extend)
+apply (fast elim: equalityE)
+done
+
+
+(*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
+
+(*Lemma 5*)
+lemma TFin_well_lemma5:
+     "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]   
+      ==> ALL m:Z. n<=m"
+apply (erule TFin_induct)
+prefer 2 apply (blast) (*second induction step is easy*)
+apply (rule ballI)
+apply (rule bspec [THEN TFin_subsetD, THEN disjE])
+apply (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"
+apply (rule classical)
+apply (subgoal_tac "Z = {Union (TFin (S,next))}")
+apply (simp (no_asm_simp) add: Inter_singleton)
+apply (erule equal_singleton)
+apply (rule Union_upper [THEN equalityI])
+apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec])
+apply (blast intro: elim:)+
+done
+
+(*This theorem just packages the previous result*)
+lemma well_ord_TFin:
+     "next: 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*)
+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*)
+apply (intro ballI)
+apply (case_tac "x=y")
+ apply (blast)
+(*The x~=y case remains*)
+apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
+       assumption+)
+apply (blast intro: elim:)+
+done
+
+(** 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"
+apply (erule apply_type)
+apply (blast elim!: equalityE)
+done
+
+(*This justifies Definition 6.1*)
+lemma Zermelo_next_exists:
+     "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))"
+apply (rule bexI)
+apply (rule ballI)
+apply (rule beta)
+apply assumption
+apply (unfold increasing_def)
+apply (rule CollectI)
+apply (rule lam_type)
+(*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) 
+apply (simp add: Pow_iff subset_consI subset_refl)
+done
+
+
+(*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})"
+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}) ")
+prefer 2 apply (blast elim: equalityE)
+apply (subgoal_tac "Union ({y: TFin (S,next) . x~: y}) ~= 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!*)
+apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
+done
+
+(*The wellordering theorem*)
+lemma AC_well_ord: "EX r. well_ord(S,r)"
+apply (rule AC_Pi_Pow [THEN exE])
+apply (rule Zermelo_next_exists [THEN bexE])
+apply assumption
+apply (rule exI)
+apply (rule well_ord_rvimage)
+apply (erule_tac [2] well_ord_TFin)
+apply (rule choice_imp_injection [THEN inj_weaken_type])
+apply (blast intro: elim:)+
+done
   
 end