# HG changeset patch # User lcp # Date 775223082 -7200 # Node ID 5e00a676a211fc99db3b095489ec618a625a483f # Parent 70b789956bd3cedc1a331d2b8ae8e2ad3c3210d3 Axiom of choice, cardinality results, etc. diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/WF.ML --- 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. : 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 ***) diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/ZF.ML --- 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]; diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/ZF.thy --- 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. *) diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/Zorn.ML --- /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(); diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/Zorn.thy --- /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 diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/Zorn0.ML --- /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. +**) + + diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/Zorn0.thy --- /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}" + 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 diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/func.ML --- 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. [| : f; : 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(, 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(, 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(); + diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/mono.ML --- 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}"; diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/simpdata.ML --- 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 diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/simpdata.thy --- 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" diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/upair.ML --- 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 ***)