--- 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
--- 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
+
--- 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
+
--- 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