--- a/src/ZF/AC.ML Fri May 10 22:51:18 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Title: ZF/AC.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-The Axiom of Choice
-*)
-
-(*The same as AC, but no premise a \\<in> A*)
-val [nonempty] = goal (the_context ())
- "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> B(x)) |] ==> \\<exists>z. z \\<in> Pi(A,B)";
-by (excluded_middle_tac "A=0" 1);
-by (asm_simp_tac (simpset() addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
-(*The non-trivial case*)
-by (blast_tac (claset() addIs [AC, nonempty]) 1);
-qed "AC_Pi";
-
-(*Using dtac, this has the advantage of DELETING the universal quantifier*)
-Goal "\\<forall>x \\<in> A. \\<exists>y. y \\<in> B(x) ==> \\<exists>y. y \\<in> Pi(A,B)";
-by (rtac AC_Pi 1);
-by (etac bspec 1);
-by (assume_tac 1);
-qed "AC_ball_Pi";
-
-Goal "\\<exists>f. f \\<in> (\\<Pi>X \\<in> Pow(C)-{0}. X)";
-by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
-by (etac exI 2);
-by (Blast_tac 1);
-qed "AC_Pi_Pow";
-
-val [nonempty] = goal (the_context ())
- "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> x) \
-\ |] ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x";
-by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
-by (etac nonempty 1);
-by (blast_tac (claset() addDs [apply_type] addIs [Pi_type]) 1);
-qed "AC_func";
-
-Goal "[| 0 \\<notin> A; x \\<in> A |] ==> \\<exists>y. y \\<in> x";
-by (subgoal_tac "x \\<noteq> 0" 1);
-by (ALLGOALS Blast_tac);
-qed "non_empty_family";
-
-Goal "0 \\<notin> A ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x";
-by (rtac AC_func 1);
-by (REPEAT (ares_tac [non_empty_family] 1));
-qed "AC_func0";
-
-Goal "\\<exists>f \\<in> (Pow(C)-{0}) -> C. \\<forall>x \\<in> Pow(C)-{0}. f`x \\<in> x";
-by (resolve_tac [AC_func0 RS bexE] 1);
-by (rtac bexI 2);
-by (assume_tac 2);
-by (etac fun_weaken_type 2);
-by (ALLGOALS Blast_tac);
-qed "AC_func_Pow";
-
-Goal "0 \\<notin> A ==> \\<exists>f. f \\<in> (\\<Pi>x \\<in> A. x)";
-by (rtac AC_Pi 1);
-by (REPEAT (ares_tac [non_empty_family] 1));
-qed "AC_Pi0";
-
-(*Used in Zorn.ML*)
-Goal "[| ch \\<in> (\\<Pi>X \\<in> Pow(S) - {0}. X); X \\<subseteq> S; X\\<noteq>S |] ==> ch ` (S-X) \\<in> S-X";
-by (etac apply_type 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "choice_Diff";
-
--- a/src/ZF/Cardinal_AC.ML Fri May 10 22:51:18 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(* Title: ZF/Cardinal_AC.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Cardinal arithmetic WITH the Axiom of Choice
-
-These results help justify infinite-branching datatypes
-*)
-
-(*** Strengthened versions of existing theorems about cardinals ***)
-
-Goal "|A| eqpoll A";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (etac well_ord_cardinal_eqpoll 1);
-qed "cardinal_eqpoll";
-
-bind_thm ("cardinal_idem", cardinal_eqpoll RS cardinal_cong);
-
-Goal "|X| = |Y| ==> X eqpoll Y";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (rtac well_ord_cardinal_eqE 1);
-by (REPEAT_SOME assume_tac);
-qed "cardinal_eqE";
-
-Goal "|X| = |Y| <-> X eqpoll Y";
-by (blast_tac (claset() addIs [cardinal_cong, cardinal_eqE]) 1);
-qed "cardinal_eqpoll_iff";
-
-Goal "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \
-\ |A Un C| = |B Un D|";
-by (asm_full_simp_tac (simpset() addsimps [cardinal_eqpoll_iff,
- eqpoll_disjoint_Un]) 1);
-qed "cardinal_disjoint_Un";
-
-Goal "A lepoll B ==> |A| le |B|";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (etac well_ord_lepoll_imp_Card_le 1);
-by (assume_tac 1);
-qed "lepoll_imp_Card_le";
-
-Goal "(i |+| j) |+| k = i |+| (j |+| k)";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (rtac well_ord_cadd_assoc 1);
-by (REPEAT_SOME assume_tac);
-qed "cadd_assoc";
-
-Goal "(i |*| j) |*| k = i |*| (j |*| k)";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (rtac well_ord_cmult_assoc 1);
-by (REPEAT_SOME assume_tac);
-qed "cmult_assoc";
-
-Goal "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (rtac well_ord_cadd_cmult_distrib 1);
-by (REPEAT_SOME assume_tac);
-qed "cadd_cmult_distrib";
-
-Goal "InfCard(|A|) ==> A*A eqpoll A";
-by (resolve_tac [AC_well_ord RS exE] 1);
-by (etac well_ord_InfCard_square_eq 1);
-by (assume_tac 1);
-qed "InfCard_square_eq";
-
-
-(*** Other applications of AC ***)
-
-Goal "|A| le |B| ==> A lepoll B";
-by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS
- lepoll_trans] 1);
-by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1);
-by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
-qed "Card_le_imp_lepoll";
-
-Goal "Card(K) ==> |A| le K <-> A lepoll K";
-by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN
- rtac iffI 1 THEN
- DEPTH_SOLVE (eresolve_tac [Card_le_imp_lepoll,lepoll_imp_Card_le] 1));
-qed "le_Card_iff";
-
-Goalw [surj_def] "f: surj(X,Y) ==> EX g. g: inj(Y,X)";
-by (etac CollectE 1);
-by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
-by (fast_tac (claset() addSEs [apply_Pair]) 1);
-by (blast_tac (claset() addDs [apply_type, Pi_memberD]
- addIs [apply_equality, Pi_type, f_imp_injective]) 1);
-qed "surj_implies_inj";
-
-(*Kunen's Lemma 10.20*)
-Goal "f: surj(X,Y) ==> |Y| le |X|";
-by (rtac lepoll_imp_Card_le 1);
-by (eresolve_tac [surj_implies_inj RS exE] 1);
-by (rewtac lepoll_def);
-by (etac exI 1);
-qed "surj_implies_cardinal_le";
-
-(*Kunen's Lemma 10.21*)
-Goal "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K";
-by (asm_full_simp_tac (simpset() addsimps [InfCard_is_Card, le_Card_iff]) 1);
-by (rtac lepoll_trans 1);
-by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
-by (asm_simp_tac (simpset() addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);
-by (rewtac lepoll_def);
-by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
-by (etac (AC_ball_Pi RS exE) 1);
-by (rtac exI 1);
-(*Lemma needed in both subgoals, for a fixed z*)
-by (subgoal_tac
- "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
-by (fast_tac (claset() addSIs [Least_le RS lt_trans1 RS ltD, ltI]
- addSEs [LeastI, Ord_in_Ord]) 2);
-by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
- ("d", "%<i,j>. converse(f`i) ` j")]
- lam_injective 1);
-(*Instantiate the lemma proved above*)
-by (ALLGOALS ball_tac);
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]
- addDs [apply_type]) 1);
-by Auto_tac;
-qed "cardinal_UN_le";
-
-
-
-(*The same again, using csucc*)
-Goal "[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \
-\ |UN i:K. X(i)| < csucc(K)";
-by (asm_full_simp_tac
- (simpset() addsimps [Card_lt_csucc_iff, cardinal_UN_le,
- InfCard_is_Card, Card_cardinal]) 1);
-qed "cardinal_UN_lt_csucc";
-
-(*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). *)
-Goal "[| InfCard(K); ALL i:K. j(i) < csucc(K) |] ==> \
-\ (UN i:K. j(i)) < csucc(K)";
-by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
-by (blast_tac (claset() addSIs [Ord_UN] addEs [ltE]) 1);
-by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
-qed "cardinal_UN_Ord_lt_csucc";
-
-
-(** 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.*)
-Goal "[| 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))";
-by (rtac UN_least 1);
-by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
-by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]) 1);
-qed "inj_UN_subset";
-
-(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
- be weaker.*)
-Goal "[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \
-\ (UN w:W. j(w)) < csucc(K)";
-by (excluded_middle_tac "W=0" 1);
-by (asm_simp_tac (*solve the easy 0 case*)
- (simpset() addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc,
- Card_is_Ord, Ord_0_lt_csucc]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
-by (safe_tac (claset() addSIs [equalityI]));
-by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc]
- MRS lt_subset_trans] 1);
-by (REPEAT (assume_tac 1));
-by (blast_tac (claset() addSIs [Ord_UN] addEs [ltE]) 2);
-by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_type]) 1);
-qed "le_UN_Ord_lt_csucc";
-
--- a/src/ZF/InfDatatype.ML Fri May 10 22:51:18 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: ZF/InfDatatype.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Infinite-branching datatype definitions
-*)
-
-bind_thm ("fun_Limit_VfromE",
- [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS
- transfer (the_context ()) Limit_VfromE
- |> standard);
-
-Goal "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] \
-\ ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)";
-by (res_inst_tac [("x", "UN d:D. LEAST i. f`d : Vfrom(A,i)")] exI 1);
-by (rtac conjI 1);
-by (rtac le_UN_Ord_lt_csucc 2);
-by (rtac ballI 4 THEN
- etac fun_Limit_VfromE 4 THEN REPEAT_SOME assume_tac);
-by (fast_tac (claset() addEs [Least_le RS lt_trans1, ltE]) 2);
-by (rtac Pi_type 1);
-by (rename_tac "d" 2);
-by (etac fun_Limit_VfromE 2 THEN REPEAT_SOME assume_tac);
-by (subgoal_tac "f`d : Vfrom(A, LEAST i. f`d : Vfrom(A,i))" 1);
-by (fast_tac (claset() addEs [LeastI, ltE]) 2);
-by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
-by (assume_tac 1);
-qed "fun_Vcsucc_lemma";
-
-Goal "[| D <= Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] \
-\ ==> EX j. D <= Vfrom(A,j) & j < csucc(K)";
-by (asm_full_simp_tac (simpset() addsimps [subset_iff_id,fun_Vcsucc_lemma]) 1);
-qed "subset_Vcsucc";
-
-(*Version for arbitrary index sets*)
-Goal "[| |D| le K; InfCard(K); D <= Vfrom(A,csucc(K)) |] ==> \
-\ D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
-by (safe_tac (claset() addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
-by (resolve_tac [Vfrom RS ssubst] 1);
-by (dtac fun_is_rel 1);
-(*This level includes the function, and is below csucc(K)*)
-by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
-by (eresolve_tac [subset_trans RS PowI] 2);
-by (fast_tac (claset() addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2);
-by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit,
- Limit_has_succ, Un_least_lt] 1));
-qed "fun_Vcsucc";
-
-Goal "[| f: D -> Vfrom(A, csucc(K)); |D| le K; InfCard(K); \
-\ D <= Vfrom(A,csucc(K)) |] \
-\ ==> f: Vfrom(A,csucc(K))";
-by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
-qed "fun_in_Vcsucc";
-
-(*Remove <= from the rule above*)
-bind_thm ("fun_in_Vcsucc'", subsetI RSN (4, fun_in_Vcsucc));
-
-(** Version where K itself is the index set **)
-
-Goal "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
-by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
-by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
- i_subset_Vfrom,
- lt_csucc RS leI RS le_imp_subset RS subset_trans] 1));
-qed "Card_fun_Vcsucc";
-
-Goal "[| f: K -> Vfrom(A, csucc(K)); InfCard(K) \
-\ |] ==> f: Vfrom(A,csucc(K))";
-by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
-qed "Card_fun_in_Vcsucc";
-
-(*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
-Goal "InfCard(K) ==> Limit(csucc(K))";
-by (etac (InfCard_csucc RS InfCard_is_Limit) 1);
-qed "Limit_csucc";
-
-bind_thm ("Pair_in_Vcsucc", Limit_csucc RSN (3, Pair_in_VLimit));
-bind_thm ("Inl_in_Vcsucc", Limit_csucc RSN (2, Inl_in_VLimit));
-bind_thm ("Inr_in_Vcsucc", Limit_csucc RSN (2, Inr_in_VLimit));
-bind_thm ("zero_in_Vcsucc", Limit_csucc RS zero_in_VLimit);
-bind_thm ("nat_into_Vcsucc", Limit_csucc RSN (2, nat_into_VLimit));
-
-(*For handling Cardinals of the form (nat Un |X|) *)
-
-bind_thm ("InfCard_nat_Un_cardinal",
- [InfCard_nat, Card_cardinal] MRS InfCard_Un);
-
-bind_thm ("le_nat_Un_cardinal",
- [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le);
-
-bind_thm ("UN_upper_cardinal",
- UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le);
-
-(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
-bind_thms ("inf_datatype_intrs",
- [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] @ Data_Arg.intrs);
--- a/src/ZF/Zorn.ML Fri May 10 22:51:18 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,377 +0,0 @@
-(* Title: ZF/Zorn.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Proofs from the paper
- Abrial & Laffitte,
- Towards the Mechanization of the Proofs of Some
- Classical Theorems of Set Theory.
-*)
-
-(*** Section 1. Mathematical Preamble ***)
-
-Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
-by (Blast_tac 1);
-qed "Union_lemma0";
-
-Goal "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
-by (Blast_tac 1);
-qed "Inter_lemma0";
-
-
-(*** Section 2. The Transfinite Construction ***)
-
-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";
-by (eresolve_tac [CollectD2 RS spec RS mp] 1);
-by (assume_tac 1);
-qed "increasingD2";
-
-(*Introduction rules*)
-val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
-bind_thm ("TFin_nextI", TFin_nextI);
-bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
-bind_thm ("TFin_UnionI", PowI RS Pow_TFin_UnionI);
-
-bind_thm ("TFin_is_subset", TFin.dom_subset RS subsetD RS PowD);
-
-
-(** Structural induction on TFin(S,next) **)
-
-val major::prems = Goal
- "[| 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 TFin.induct) 1);
-by (ALLGOALS (fast_tac (claset() addIs prems)));
-qed "TFin_induct";
-
-
-(*** Section 3. Some Properties of the Transfinite Construction ***)
-
-bind_thm ("increasing_trans",
- TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
-
-(*Lemma 1 of section 3.1*)
-Goal "[| 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 (etac TFin_induct 1);
-by (etac Union_lemma0 2); (*or just Blast_tac*)
-by (blast_tac (subset_cs addIs [increasing_trans]) 1);
-qed "TFin_linear_lemma1";
-
-(*Lemma 2 of section 3.2. Interesting in its own right!
- Requires next: increasing(S) in the second induction step. *)
-val [major,ninc] = goal (the_context ())
- "[| m: TFin(S,next); next: increasing(S) \
-\ |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
-by (rtac (major RS TFin_induct) 1);
-by (rtac (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 (blast_tac (subset_cs addIs [increasing_trans]) 1);
-by (REPEAT (ares_tac [disjI1,equalityI] 1));
-(*second induction step*)
-by (rtac (impI RS ballI) 1);
-by (rtac (Union_lemma0 RS disjE) 1);
-by (etac disjI2 3);
-by (REPEAT (ares_tac [disjI1,equalityI] 2));
-by (rtac 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 (blast_tac subset_cs 1);
-by (rtac (ninc RS increasingD2 RS subset_trans RS disjI1) 1);
-by (REPEAT (ares_tac [TFin_is_subset] 1));
-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";
-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";
-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,
- TFin_is_subset]) 1);
-qed "TFin_subset_linear";
-
-
-(*Lemma 3 of section 3.3*)
-Goal "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m";
-by (etac TFin_induct 1);
-by (dtac TFin_subsetD 1);
-by (REPEAT (assume_tac 1));
-by (fast_tac (claset() addEs [ssubst]) 1);
-by (blast_tac (subset_cs addIs [TFin_is_subset]) 1);
-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))";
-by (rtac iffI 1);
-by (rtac (Union_upper RS equalityI) 1);
-by (rtac (equal_next_upper RS Union_least) 2);
-by (REPEAT (assume_tac 1));
-by (etac ssubst 1);
-by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1);
-by (ALLGOALS
- (blast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
-qed "equal_next_Union";
-
-
-(*** 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 [chain_def] "chain(A) <= Pow(A)";
-by (rtac Collect_subset 1);
-qed "chain_subset_Pow";
-
-Goalw [super_def] "super(A,c) <= chain(A)";
-by (rtac Collect_subset 1);
-qed "super_subset_chain";
-
-Goalw [maxchain_def] "maxchain(A) <= chain(A)";
-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)";
-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";
-by (rtac notI 1);
-by (dtac choice_super 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [super_def]) 1);
-qed "choice_not_equals";
-
-(*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)";
-by (rtac bexI 1);
-by (rtac ballI 1);
-by (rtac beta 1);
-by (assume_tac 1);
-by (rewtac increasing_def);
-by (rtac CollectI 1);
-by (rtac lam_type 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addDs [super_subset_chain RS subsetD,
- 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;
-by (dtac choice_super 1);
-by (REPEAT (assume_tac 1));
-by (rewtac super_def);
-by (Blast_tac 1);
-qed "Hausdorff_next_exists";
-
-(*Lemma 4*)
-Goal " [| 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 (etac TFin_induct 1);
-by (asm_simp_tac
- (simpset() addsimps [chain_subset_Pow RS subsetD RS PowD,
- choice_super RS (super_subset_chain RS subsetD)]) 1);
-by (rewtac chain_def);
-by (rtac CollectI 1 THEN Blast_tac 1);
-by Safe_tac;
-by (res_inst_tac [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
-by (ALLGOALS Fast_tac); (*Blast_tac's slow*)
-qed "TFin_chain_lemma4";
-
-Goal "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 (rtac 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 (rtac refl 2);
-by (asm_full_simp_tac
- (simpset() addsimps [subset_refl RS TFin_UnionI RS
- (TFin.dom_subset RS subsetD RS PowD)]) 1);
-by (eresolve_tac [choice_not_equals RS notE] 1);
-by (REPEAT (assume_tac 1));
-qed "Hausdorff";
-
-
-(*** 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 [chain_def]
- "[| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
-by (Blast_tac 1);
-qed "chain_extend";
-
-Goal "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 (simpset() addsimps [maxchain_def]) 1);
-by (rename_tac "c" 1);
-by (res_inst_tac [("x", "Union(c)")] bexI 1);
-by (Blast_tac 2);
-by Safe_tac;
-by (rename_tac "z" 1);
-by (rtac classical 1);
-by (subgoal_tac "cons(z,c): super(S,c)" 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
-by (rewtac super_def);
-by Safe_tac;
-by (fast_tac (claset() addEs [chain_extend]) 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";
-by (etac TFin_induct 1);
-by (Blast_tac 2); (*second induction step is easy*)
-by (rtac ballI 1);
-by (rtac (bspec RS TFin_subsetD RS disjE) 1);
-by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
-by (subgoal_tac "x = Inter(Z)" 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed "TFin_well_lemma5";
-
-(*Well-ordering of TFin(S,next)*)
-Goal "[| Z <= TFin(S,next); z:Z |] ==> Inter(Z) : Z";
-by (rtac classical 1);
-by (subgoal_tac "Z = {Union(TFin(S,next))}" 1);
-by (asm_simp_tac (simpset() addsimps [Inter_singleton]) 1);
-by (etac equal_singleton 1);
-by (rtac (Union_upper RS equalityI) 1);
-by (rtac (subset_refl RS TFin_UnionI RS TFin_well_lemma5 RS bspec) 2);
-by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
-qed "well_ord_TFin_lemma";
-
-(*This theorem just packages the previous result*)
-Goal "next: increasing(S) ==> \
-\ well_ord(TFin(S,next), Subset_rel(TFin(S,next)))";
-by (rtac 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 (Blast_tac 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 (Blast_tac 2);
-by (Blast_tac 2);
-(*Now prove the well_foundedness goal*)
-by (rtac wf_onI 1);
-by (ftac well_ord_TFin_lemma 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
-by (Blast_tac 1);
-qed "well_ord_TFin";
-
-(** Defining the "next" operation for Zermelo's Theorem **)
-
-(*This justifies Definition 6.1*)
-Goal "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 (rtac beta 1);
-by (assume_tac 1);
-by (rewtac increasing_def);
-by (rtac CollectI 1);
-by (rtac lam_type 1);
-(*Verify that it increases*)
-by (rtac allI 2);
-by (rtac impI 2);
-by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_consI, subset_refl]) 2);
-(*Type checking is surprisingly hard!*)
-by (asm_simp_tac
- (simpset() addsimps [Pow_iff, cons_subset_iff, subset_refl]) 1);
-by (blast_tac (claset() addSIs [choice_Diff RS DiffD1]) 1);
-qed "Zermelo_next_exists";
-
-
-(*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})) \
-\ : 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 (blast_tac (claset() addSIs [Collect_subset RS TFin_UnionI]
- addEs [equalityE]) 1);
-by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1);
-by (blast_tac (claset() addEs [equalityE]) 2);
-by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1);
-by (blast_tac (claset() 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
- (simpset() delsimps [Union_iff]
- addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
- Pow_iff, cons_subset_iff, subset_refl,
- choice_Diff RS DiffD2]) 2);
-by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
-by (blast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
-(*End of the lemmas!*)
-by (asm_full_simp_tac
- (simpset() addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
- Pow_iff, cons_subset_iff, subset_refl]) 1);
-by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1));
-qed "choice_imp_injection";
-
-(*The wellordering theorem*)
-Goal "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);
-by (rtac exI 1);
-by (rtac well_ord_rvimage 1);
-by (etac well_ord_TFin 2);
-by (resolve_tac [choice_imp_injection RS inj_weaken_type] 1);
-by (REPEAT (ares_tac [Diff_subset] 1));
-qed "AC_well_ord";