1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/AC/OrdQuant.thy Fri Mar 31 11:55:29 1995 +0200
1.3 @@ -0,0 +1,39 @@
1.4 +(* Title: ZF/AC/OrdQuant.thy
1.5 + ID: $Id$
1.6 + Author: Krzysztof Gr`abczewski
1.7 +
1.8 +Quantifiers and union operator for ordinals.
1.9 +*)
1.10 +
1.11 +OrdQuant = Ordinal +
1.12 +
1.13 +consts
1.14 +
1.15 + (* Ordinal Quantifiers *)
1.16 + Oall, Oex :: "[i, i => o] => o"
1.17 + (* General Union and Intersection *)
1.18 + OUnion :: "[i, i => i] => i"
1.19 +
1.20 +syntax
1.21 +
1.22 + "@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
1.23 + "@Oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
1.24 + "@Oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
1.25 +
1.26 +translations
1.27 +
1.28 + "UN x<a. B" == "OUnion(a, %x. B)"
1.29 + "ALL x<a. P" == "Oall(a, %x. P)"
1.30 + "EX x<a. P" == "Oex(a, %x. P)"
1.31 +
1.32 +rules
1.33 +
1.34 + OUnion_iff "A : OUnion(a, %z. B(z)) <-> (EX x<a. A: B(x))"
1.35 +
1.36 +defs
1.37 +
1.38 + (* Ordinal Quantifiers *)
1.39 + Oall_def "Oall(A, P) == ALL x. x<A --> P(x)"
1.40 + Oex_def "Oex(A, P) == EX x. x<A & P(x)"
1.41 +
1.42 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/ZF/AC/ROOT.ML Fri Mar 31 11:55:29 1995 +0200
2.3 @@ -0,0 +1,18 @@
2.4 +(* Title: ZF/ex/ROOT
2.5 + ID: $Id$
2.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.7 + Copyright 1995 University of Cambridge
2.8 +
2.9 +Executes the proofs of the AC-equivalences, by Krzysztof Gr`abczewski
2.10 +*)
2.11 +
2.12 +ZF_build_completed; (*Make examples fail if ZF did*)
2.13 +
2.14 +writeln"Root file for ZF/AC";
2.15 +proof_timing := true;
2.16 +
2.17 +loadpath := [".", "AC"];
2.18 +
2.19 +time_use_thy "WO6_WO1";
2.20 +
2.21 +writeln"END: Root file for ZF/AC";
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/ZF/AC/Transrec2.ML Fri Mar 31 11:55:29 1995 +0200
3.3 @@ -0,0 +1,36 @@
3.4 +(* Title: ZF/AC/Transrec2.ML
3.5 + ID: $Id$
3.6 + Author: Krzysztof Gr`abczewski
3.7 +
3.8 +Transfinite recursion introduced to handle definitions based on the three
3.9 +cases of ordinals.
3.10 +*)
3.11 +
3.12 +open Transrec2;
3.13 +
3.14 +val AC_cs = OrdQuant_cs;
3.15 +val AC_ss = OrdQuant_ss;
3.16 +
3.17 +goal thy "transrec2(0,a,b) = a";
3.18 +by (rtac (transrec2_def RS def_transrec RS trans) 1);
3.19 +by (simp_tac ZF_ss 1);
3.20 +val transrec2_0 = result();
3.21 +
3.22 +goal thy "(THE j. succ(i)=succ(j)) = i";
3.23 +by (fast_tac (AC_cs addSIs [the_equality]) 1);
3.24 +val THE_succ_eq = result();
3.25 +
3.26 +goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
3.27 +by (rtac (transrec2_def RS def_transrec RS trans) 1);
3.28 +by (simp_tac (ZF_ss addsimps [succ_not_0, THE_succ_eq, if_P]
3.29 + setsolver K (fast_tac FOL_cs)) 1);
3.30 +val transrec2_succ = result();
3.31 +
3.32 +goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
3.33 +by (rtac (transrec2_def RS def_transrec RS trans) 1);
3.34 +by (resolve_tac [if_not_P RS trans] 1 THEN
3.35 + fast_tac (AC_cs addSDs [Limit_has_0] addSEs [ltE]) 1);
3.36 +by (resolve_tac [if_not_P RS trans] 1 THEN
3.37 + fast_tac (AC_cs addSEs [succ_LimitE]) 1);
3.38 +by (simp_tac AC_ss 1);
3.39 +val transrec2_Limit = result();
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/ZF/AC/Transrec2.thy Fri Mar 31 11:55:29 1995 +0200
4.3 @@ -0,0 +1,23 @@
4.4 +(* Title: ZF/AC/Transrec2.thy
4.5 + ID: $Id$
4.6 + Author: Krzysztof Gr`abczewski
4.7 +
4.8 +Transfinite recursion introduced to handle definitions based on the three
4.9 +cases of ordinals.
4.10 +*)
4.11 +
4.12 +Transrec2 = OrdQuant + Epsilon +
4.13 +
4.14 +consts
4.15 +
4.16 + transrec2 :: "[i, i, [i,i]=>i] =>i"
4.17 +
4.18 +defs
4.19 +
4.20 + transrec2_def "transrec2(alpha, a, b) == \
4.21 +\ transrec(alpha, %i r. if(i=0, \
4.22 +\ a, if(EX j. i=succ(j), \
4.23 +\ b(THE j. i=succ(j), r`(THE j. i=succ(j))), \
4.24 +\ UN j<i. r`j)))"
4.25 +
4.26 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/ZF/AC/WO6_WO1.ML Fri Mar 31 11:55:29 1995 +0200
5.3 @@ -0,0 +1,534 @@
5.4 +(* Title: ZF/AC/WO6_WO1.ML
5.5 + ID: $Id$
5.6 + Author: Krzysztof Gr`abczewski
5.7 +
5.8 +The proof of "WO6 ==> WO1".
5.9 +
5.10 +From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
5.11 +pages 2-5
5.12 +*)
5.13 +
5.14 +(* ********************************************************************** *)
5.15 +(* The most complicated part of the proof - lemma ii - p. 2-4 *)
5.16 +(* ********************************************************************** *)
5.17 +
5.18 +(* ********************************************************************** *)
5.19 +(* some properties of relation uu(beta, gamma, delta) - p. 2 *)
5.20 +(* ********************************************************************** *)
5.21 +
5.22 +goalw thy [uu_def] "domain(uu(f,b,g,d)) <= f`b";
5.23 +by (fast_tac ZF_cs 1);
5.24 +val domain_uu_subset = result();
5.25 +
5.26 +goal thy "!!a. [| ALL b<a. f`b lepoll m; b<a |] \
5.27 +\ ==> domain(uu(f, b, g, d)) lepoll m";
5.28 +by (fast_tac (AC_cs addSEs
5.29 + [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
5.30 +val domain_uu_lepoll_m = result();
5.31 +
5.32 +goal thy "!! a. ALL b<a. f`b lepoll m ==> \
5.33 +\ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
5.34 +by (fast_tac (AC_cs addEs [domain_uu_lepoll_m]) 1);
5.35 +val quant_domain_uu_lepoll_m = result();
5.36 +
5.37 +(* used in case 2 *)
5.38 +goalw thy [uu_def] "uu(f,b,g,d) <= f`b * f`g";
5.39 +by (fast_tac ZF_cs 1);
5.40 +val uu_subset1 = result();
5.41 +
5.42 +goalw thy [uu_def] "uu(f,b,g,d) <= f`d";
5.43 +by (fast_tac ZF_cs 1);
5.44 +val uu_subset2 = result();
5.45 +
5.46 +goal thy "!! a. [| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
5.47 +by (fast_tac (AC_cs
5.48 + addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
5.49 +val uu_lepoll_m = result();
5.50 +
5.51 +(* ********************************************************************** *)
5.52 +(* Two cases for lemma ii *)
5.53 +(* ********************************************************************** *)
5.54 +goalw thy [lesspoll_def]
5.55 + "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \
5.56 +\ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \
5.57 +\ u(f,b,g,d) lesspoll m)) | \
5.58 +\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
5.59 +\ u(f,b,g,d) eqpoll m))";
5.60 +by (fast_tac AC_cs 1);
5.61 +val cases = result();
5.62 +
5.63 +(* ********************************************************************** *)
5.64 +(* Lemmas used in both cases *)
5.65 +(* ********************************************************************** *)
5.66 +goal thy "!!a f. Ord(a) ==> (UN b<a++a. f`b) = (UN b<a. f`b Un f`(a++b))";
5.67 +by (resolve_tac [equalityI] 1);
5.68 +by (fast_tac (AC_cs addIs [ltI, OUN_I] addSEs [OUN_E]
5.69 + addSDs [lt_oadd_disj]) 1);
5.70 +by (fast_tac (AC_cs addSEs [lt_oadd1, oadd_lt_mono2, OUN_E]
5.71 + addSIs [OUN_I]) 1);
5.72 +val UN_oadd = result();
5.73 +
5.74 +val [prem] = goal thy
5.75 + "(!!b. b<a ==> P(b)=Q(b)) ==> (UN b<a. P(b)) = (UN b<a. Q(b))";
5.76 +by (fast_tac (ZF_cs addSIs [OUN_I, equalityI]
5.77 + addSEs [OUN_E, prem RS equalityD1 RS subsetD,
5.78 + prem RS sym RS equalityD1 RS subsetD]) 1);
5.79 +val UN_eq = result();
5.80 +
5.81 +goal thy "!!a. b<a ==> b = (THE l. l<a & a ++ b = a ++ l)";
5.82 +by (fast_tac (ZF_cs addSIs [the_equality RS sym]
5.83 + addIs [lt_Ord2, lt_Ord]
5.84 + addSEs [oadd_inject RS sym]) 1);
5.85 +val the_only_b = result();
5.86 +
5.87 +goal thy "!!A. B <= A ==> B Un (A-B) = A";
5.88 +by (fast_tac (ZF_cs addSIs [equalityI]) 1);
5.89 +val subset_imp_Un_Diff_eq = result();
5.90 +
5.91 +(* ********************************************************************** *)
5.92 +(* Case 1 : lemmas *)
5.93 +(* ********************************************************************** *)
5.94 +
5.95 +goalw thy [vv1_def] "vv1(f,b,succ(m)) <= f`b";
5.96 +by (resolve_tac [expand_if RS iffD2] 1);
5.97 +by (fast_tac (ZF_cs addSIs [domain_uu_subset]) 1);
5.98 +val vv1_subset = result();
5.99 +
5.100 +(* ********************************************************************** *)
5.101 +(* Case 1 : Union of images is the whole "y" *)
5.102 +(* ********************************************************************** *)
5.103 +goal thy "!! a f y. [| (UN b<a. f`b) = y; Ord(a); m:nat |] ==> \
5.104 +\ (UN b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \
5.105 +\ ww1(f, THE l. l<a & b=a++l, succ(m)))) ` b) = y";
5.106 +by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1));
5.107 +by (eresolve_tac [subst] 1);
5.108 +by (resolve_tac [UN_eq] 1);
5.109 +by (forw_inst_tac [("i","a")] lt_oadd1 1
5.110 + THEN (REPEAT (atac 1)));
5.111 +by (forw_inst_tac [("j","a")] oadd_lt_mono2 1
5.112 + THEN (REPEAT (atac 1)));
5.113 +by (asm_simp_tac (ZF_ss addsimps [ltD RS beta,
5.114 + oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1);
5.115 +by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1));
5.116 +by (asm_simp_tac (ZF_ss
5.117 + addsimps [vv1_subset RS subset_imp_Un_Diff_eq, ltD, ww1_def]) 1);
5.118 +val UN_eq_y = result();
5.119 +
5.120 +(* ********************************************************************** *)
5.121 +(* every value of defined function is less than or equipollent to m *)
5.122 +(* ********************************************************************** *)
5.123 +goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \
5.124 +\ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \
5.125 +\ ==> P(Least_a, LEAST b. P(Least_a, b))";
5.126 +by (eresolve_tac [ssubst] 1);
5.127 +by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
5.128 +by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
5.129 +val nested_LeastI = result();
5.130 +
5.131 +val nested_Least_instance = read_instantiate
5.132 + [("P","%g d. domain(uu(f,b,g,d)) ~= 0 & \
5.133 +\ domain(uu(f,b,g,d)) lesspoll succ(m)")] nested_LeastI;
5.134 +
5.135 +goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \
5.136 +\ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \
5.137 +\ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a |] \
5.138 +\ ==> vv1(f,b,succ(m)) lesspoll succ(m)";
5.139 +by (resolve_tac [expand_if RS iffD2] 1);
5.140 +by (fast_tac (AC_cs addIs [nested_Least_instance RS conjunct2]
5.141 + addSEs [lt_Ord]
5.142 + addSIs [empty_lepollI RS lepoll_imp_lesspoll_succ]) 1);
5.143 +val vv1_lesspoll_succ = result();
5.144 +
5.145 +goalw thy [vv1_def] "!!a. [| ALL b<a. f`b ~=0 --> \
5.146 +\ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \
5.147 +\ domain(uu(f,b,g,d)) lesspoll succ(m)); m:nat; b<a; f`b ~= 0 |] \
5.148 +\ ==> vv1(f,b,succ(m)) ~= 0";
5.149 +by (resolve_tac [expand_if RS iffD2] 1);
5.150 +by (resolve_tac [conjI] 1);
5.151 +by (fast_tac ZF_cs 2);
5.152 +by (resolve_tac [impI] 1);
5.153 +by (eresolve_tac [oallE] 1);
5.154 +by (mp_tac 1);
5.155 +by (contr_tac 2);
5.156 +by (REPEAT (eresolve_tac [oexE] 1));
5.157 +by (asm_simp_tac (ZF_ss
5.158 + addsimps [lt_Ord, nested_Least_instance RS conjunct1]) 1);
5.159 +val vv1_not_0 = result();
5.160 +
5.161 +goalw thy [ww1_def] "!!a. [| ALL b<a. f`b ~=0 --> \
5.162 +\ (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \
5.163 +\ domain(uu(f,b,g,d)) lesspoll succ(m)); \
5.164 +\ ALL b<a. f`b lepoll succ(m); m:nat; b<a |] \
5.165 +\ ==> ww1(f,b,succ(m)) lesspoll succ(m)";
5.166 +by (excluded_middle_tac "f`b = 0" 1);
5.167 +by (asm_full_simp_tac (AC_ss
5.168 + addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
5.169 +by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1);
5.170 +by (fast_tac AC_cs 1);
5.171 +by (REPEAT (ares_tac [vv1_subset, vv1_not_0] 1));
5.172 +val ww1_lesspoll_succ = result();
5.173 +
5.174 +goal thy "!!a. [| Ord(a); m:nat; \
5.175 +\ ALL b<a. f`b ~=0 --> (EX g<a. EX d<a. domain(uu(f,b,g,d))~=0 & \
5.176 +\ domain(uu(f,b,g,d)) lesspoll succ(m)); \
5.177 +\ ALL b<a. f`b lepoll succ(m) |] \
5.178 +\ ==> ALL b<a++a. (lam b:a++a. if(b<a, vv1(f,b,succ(m)), \
5.179 +\ ww1(f,THE l. l<a & b = a ++ l,succ(m))))`b lepoll m";
5.180 +by (resolve_tac [oallI] 1);
5.181 +by (asm_full_simp_tac (ZF_ss addsimps [ltD RS beta]) 1);
5.182 +by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2));
5.183 +by (resolve_tac [expand_if RS iffD2] 1);
5.184 +by (resolve_tac [conjI] 1);
5.185 +by (resolve_tac [impI] 1);
5.186 +by (forward_tac [lt_oadd_disj1] 2 THEN (REPEAT (atac 2)));
5.187 +by (resolve_tac [impI] 2);
5.188 +by (eresolve_tac [disjE] 2 THEN (fast_tac (ZF_cs addSEs [ltE]) 2));
5.189 +by (asm_full_simp_tac (ZF_ss addsimps [vv1_lesspoll_succ]) 1);
5.190 +by (dresolve_tac [theI] 1);
5.191 +by (eresolve_tac [conjE] 1);
5.192 +by (resolve_tac [ww1_lesspoll_succ] 1 THEN (REPEAT (atac 1)));
5.193 +val all_sum_lepoll_m = result();
5.194 +
5.195 +(* ********************************************************************** *)
5.196 +(* Case 2 : lemmas *)
5.197 +(* ********************************************************************** *)
5.198 +
5.199 +(* ********************************************************************** *)
5.200 +(* Case 2 : vv2_subset *)
5.201 +(* ********************************************************************** *)
5.202 +
5.203 +goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
5.204 +\ y*y <= y; (UN b<a. f`b)=y |] \
5.205 +\ ==> EX d<a. uu(f,b,g,d)~=0";
5.206 +by (fast_tac (AC_cs addSIs [not_emptyI]
5.207 + addSDs [SigmaI RSN (2, subsetD)]
5.208 + addSEs [not_emptyE]) 1);
5.209 +val ex_d_uu_not_empty = result();
5.210 +
5.211 +goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
5.212 +\ y*y<=y; (UN b<a. f`b)=y |] \
5.213 +\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
5.214 +by (dresolve_tac [ex_d_uu_not_empty] 1 THEN (REPEAT (atac 1)));
5.215 +by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1);
5.216 +val uu_not_empty = result();
5.217 +
5.218 +(* moved from ZF_aux.ML *)
5.219 +goal thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
5.220 +by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE,
5.221 + sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
5.222 +val not_empty_rel_imp_domain = result();
5.223 +
5.224 +goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
5.225 +\ y*y <= y; (UN b<a. f`b)=y |] \
5.226 +\ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
5.227 +by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
5.228 + THEN (REPEAT (atac 1)));
5.229 +by (resolve_tac [Least_le RS lt_trans1] 1
5.230 + THEN (REPEAT (ares_tac [lt_Ord] 1)));
5.231 +val Least_uu_not_empty_lt_a = result();
5.232 +
5.233 +goal thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
5.234 +by (fast_tac ZF_cs 1);
5.235 +val subset_Diff_sing = result();
5.236 +
5.237 +goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
5.238 +by (eresolve_tac [natE] 1);
5.239 +by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
5.240 +by (hyp_subst_tac 1);
5.241 +by (resolve_tac [equalityI] 1);
5.242 +by (atac 2);
5.243 +by (resolve_tac [subsetI] 1);
5.244 +by (excluded_middle_tac "?P" 1 THEN (atac 2));
5.245 +by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2,
5.246 + diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
5.247 + succ_lepoll_natE] 1
5.248 + THEN (REPEAT (atac 1)));
5.249 +val supset_lepoll_imp_eq = result();
5.250 +
5.251 +goalw thy [vv2_def]
5.252 + "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
5.253 +\ domain(uu(f, b, g, d)) eqpoll succ(m); \
5.254 +\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
5.255 +\ (UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; aa:f`b |] \
5.256 +\ ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
5.257 +by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2));
5.258 +by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1);
5.259 +by (eresolve_tac [impE] 1);
5.260 +by (eresolve_tac [uu_not_empty RS (uu_subset1 RS
5.261 + not_empty_rel_imp_domain)] 1
5.262 + THEN (REPEAT (atac 1)));
5.263 +by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2
5.264 + THEN (TRYALL atac));
5.265 +by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
5.266 + (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2,
5.267 + uu_subset1 RSN (4, rel_is_fun)))] 1
5.268 + THEN (TRYALL atac));
5.269 +by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2,
5.270 + supset_lepoll_imp_eq)] 1);
5.271 +by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1));
5.272 +val uu_Least_is_fun = result();
5.273 +
5.274 +goalw thy [vv2_def]
5.275 + "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
5.276 +\ domain(uu(f, b, g, d)) eqpoll succ(m); \
5.277 +\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
5.278 +\ (UN b<a. f`b)=y; b<a; g<a; m:nat; aa:f`b |] \
5.279 +\ ==> vv2(f,b,g,aa) <= f`g";
5.280 +by (fast_tac (FOL_cs addIs [expand_if RS iffD2]
5.281 + addSEs [uu_Least_is_fun]
5.282 + addSIs [empty_subsetI, not_emptyI,
5.283 + singleton_subsetI, apply_type]) 1);
5.284 +val vv2_subset = result();
5.285 +
5.286 +(* ********************************************************************** *)
5.287 +(* Case 2 : Union of images is the whole "y" *)
5.288 +(* ********************************************************************** *)
5.289 +goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
5.290 +\ domain(uu(f,b,g,d)) eqpoll succ(m); \
5.291 +\ ALL b<a. f`b lepoll succ(m); y*y<=y; \
5.292 +\ (UN b<a.f`b)=y; Ord(a); m:nat; aa:f`b; b<a |] \
5.293 +\ ==> (UN g<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \
5.294 +\ ww2(f,b,THE l. l<a & g=a++l,aa)))`g) = y";
5.295 +by (resolve_tac [UN_oadd RS ssubst] 1 THEN (atac 1));
5.296 +by (resolve_tac [subst] 1 THEN (atac 1));
5.297 +by (resolve_tac [UN_eq] 1);
5.298 +by (forw_inst_tac [("i","a"),("k","ba")] lt_oadd1 1
5.299 + THEN (REPEAT (atac 1)));
5.300 +by (forw_inst_tac [("j","a"),("k","ba")] oadd_lt_mono2 1
5.301 + THEN (REPEAT (atac 1)));
5.302 +by (asm_simp_tac (ZF_ss addsimps [ltD RS beta,
5.303 + oadd_le_self RS le_imp_not_lt RS if_not_P, lt_Ord]) 1);
5.304 +by (resolve_tac [the_only_b RS subst] 1 THEN (atac 1));
5.305 +by (asm_simp_tac (ZF_ss
5.306 + addsimps [vv2_subset RS subset_imp_Un_Diff_eq, ltI, ww2_def]) 1);
5.307 +val UN_eq_y_2 = result();
5.308 +
5.309 +(* ********************************************************************** *)
5.310 +(* every value of defined function is less than or equipollent to m *)
5.311 +(* ********************************************************************** *)
5.312 +
5.313 +goalw thy [vv2_def]
5.314 + "!!m. [| m:nat; m~=0 |] ==> vv2(f,b,g,aa) lesspoll succ(m)";
5.315 +by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
5.316 +by (asm_simp_tac (AC_ss
5.317 + addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
5.318 +by (fast_tac (AC_cs
5.319 + addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
5.320 + addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS
5.321 + lepoll_trans RS lepoll_imp_lesspoll_succ,
5.322 + not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
5.323 + nat_into_Ord, nat_1I]) 1);
5.324 +val vv2_lesspoll_succ = result();
5.325 +
5.326 +goalw thy [ww2_def] "!!m. [| ALL b<a. f`b lepoll succ(m); g<a; m:nat; \
5.327 +\ vv2(f,b,g,d) <= f`g |] \
5.328 +\ ==> ww2(f,b,g,d) lesspoll succ(m)";
5.329 +by (excluded_middle_tac "f`g = 0" 1);
5.330 +by (asm_simp_tac (AC_ss
5.331 + addsimps [empty_lepollI RS lepoll_imp_lesspoll_succ]) 2);
5.332 +by (dresolve_tac [ospec] 1 THEN (atac 1));
5.333 +by (resolve_tac [Diff_lepoll RS lepoll_imp_lesspoll_succ] 1
5.334 + THEN (TRYALL atac));
5.335 +by (asm_simp_tac (AC_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
5.336 +val ww2_lesspoll_succ = result();
5.337 +
5.338 +goal thy "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
5.339 +\ domain(uu(f,b,g,d)) eqpoll succ(m); \
5.340 +\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
5.341 +\ (UN b<a. f`b)=y; b<a; aa:f`b; m:nat; m~= 0 |] \
5.342 +\ ==> ALL ba<a++a. (lam g:a++a. if(g<a, vv2(f,b,g,aa), \
5.343 +\ ww2(f,b,THE l. l<a & g=a++l,aa)))`ba lepoll m";
5.344 +by (resolve_tac [oallI] 1);
5.345 +by (asm_full_simp_tac AC_ss 1);
5.346 +by (resolve_tac [lesspoll_succ_imp_lepoll] 1 THEN (atac 2));
5.347 +by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
5.348 +by (asm_simp_tac (AC_ss addsimps [vv2_lesspoll_succ]) 1);
5.349 +by (forward_tac [lt_oadd_disj1] 1 THEN (REPEAT (ares_tac [lt_Ord2] 1)));
5.350 +by (fast_tac (FOL_cs addSIs [ww2_lesspoll_succ, vv2_subset]
5.351 + addSDs [theI]) 1);
5.352 +val all_sum_lepoll_m_2 = result();
5.353 +
5.354 +(* ********************************************************************** *)
5.355 +(* lemma ii *)
5.356 +(* ********************************************************************** *)
5.357 +goalw thy [NN_def]
5.358 + "!!y. [| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
5.359 +by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
5.360 +by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
5.361 + THEN (atac 1));
5.362 +(* case 1 *)
5.363 +by (resolve_tac [CollectI] 1);
5.364 +by (atac 1);
5.365 +by (res_inst_tac [("x","a ++ a")] exI 1);
5.366 +by (res_inst_tac [("x","lam b:a++a. if (b<a, vv1(f,b,succ(m)), \
5.367 +\ ww1(f,THE l. l<a & b=a++l,succ(m)))")] exI 1);
5.368 +by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun,
5.369 + UN_eq_y, all_sum_lepoll_m]) 1);
5.370 +(* case 2 *)
5.371 +by (REPEAT (eresolve_tac [oexE, conjE] 1));
5.372 +by (resolve_tac [CollectI] 1);
5.373 +by (eresolve_tac [succ_natD] 1);
5.374 +by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (atac 1));
5.375 +by (res_inst_tac [("x","a++a")] exI 1);
5.376 +by (res_inst_tac [("x","lam g:a++a. if (g<a, vv2(f,b,g,x), \
5.377 +\ ww2(f,b,THE l. l<a & g=a++l,x))")] exI 1);
5.378 +by (fast_tac (FOL_cs addSIs [Ord_oadd, lam_funtype RS domain_of_fun,
5.379 + UN_eq_y_2, all_sum_lepoll_m_2]) 1);
5.380 +val lemma_ii = result();
5.381 +
5.382 +
5.383 +(* ********************************************************************** *)
5.384 +(* lemma iv - p. 4 : *)
5.385 +(* For every set x there is a set y such that x Un (y * y) <= y *)
5.386 +(* ********************************************************************** *)
5.387 +
5.388 +(* the quantifier ALL looks inelegant but makes the proofs shorter *)
5.389 +(* (used only in the following two lemmas) *)
5.390 +
5.391 +goal thy "ALL n:nat. rec(n, x, %k r. r Un r*r) <= \
5.392 +\ rec(succ(n), x, %k r. r Un r*r)";
5.393 +by (fast_tac (ZF_cs addIs [rec_succ RS ssubst]) 1);
5.394 +val z_n_subset_z_succ_n = result();
5.395 +
5.396 +goal thy "!!n. [| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \
5.397 +\ ==> f(n)<=f(m)";
5.398 +by (res_inst_tac [("P","n le m")] impE 1 THEN (REPEAT (atac 2)));
5.399 +by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
5.400 +by (REPEAT (fast_tac lt_cs 1));
5.401 +val le_subsets = result();
5.402 +
5.403 +goal thy "!!n m. [| n le m; m:nat |] ==> \
5.404 +\ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
5.405 +by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1
5.406 + THEN (TRYALL atac));
5.407 +by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
5.408 + THEN (atac 1));
5.409 +val le_imp_rec_subset = result();
5.410 +
5.411 +goal thy "!!x. EX y. x Un y*y <= y";
5.412 +by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
5.413 +by (resolve_tac [subsetI] 1);
5.414 +by (eresolve_tac [UnE] 1);
5.415 +by (resolve_tac [UN_I] 1);
5.416 +by (eresolve_tac [rec_0 RS ssubst] 2);
5.417 +by (resolve_tac [nat_0I] 1);
5.418 +by (eresolve_tac [SigmaE] 1);
5.419 +by (REPEAT (eresolve_tac [UN_E] 1));
5.420 +by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
5.421 +by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (atac 1));
5.422 +by (resolve_tac [rec_succ RS ssubst] 1);
5.423 +by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
5.424 + addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
5.425 + addSEs [nat_into_Ord]) 1);
5.426 +val lemma_iv = result();
5.427 +
5.428 +(* ********************************************************************** *)
5.429 +(* Rubin & Rubin wrote : *)
5.430 +(* "It follows from (ii) and mathematical induction that if y*y <= y then *)
5.431 +(* y can be well-ordered" *)
5.432 +
5.433 +(* In fact we have to prove : *)
5.434 +(* * WO6 ==> NN(y) ~= 0 *)
5.435 +(* * reverse induction which lets us infer that 1 : NN(y) *)
5.436 +(* * 1 : NN(y) ==> y can be well-ordered *)
5.437 +(* ********************************************************************** *)
5.438 +
5.439 +(* ********************************************************************** *)
5.440 +(* WO6 ==> NN(y) ~= 0 *)
5.441 +(* ********************************************************************** *)
5.442 +
5.443 +goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
5.444 +by (eresolve_tac [allE] 1);
5.445 +by (fast_tac (ZF_cs addSIs [not_emptyI]) 1);
5.446 +val WO6_imp_NN_not_empty = result();
5.447 +
5.448 +(* ********************************************************************** *)
5.449 +(* 1 : NN(y) ==> y can be well-ordered *)
5.450 +(* ********************************************************************** *)
5.451 +
5.452 +goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
5.453 +\ ==> EX c<a. f`c = {x}";
5.454 +by (fast_tac (AC_cs addSEs [lepoll_1_is_sing]) 1);
5.455 +val lemma1 = result();
5.456 +
5.457 +goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
5.458 +\ ==> f` (LEAST i. f`i = {x}) = {x}";
5.459 +by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1)));
5.460 +by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
5.461 +val lemma2 = result();
5.462 +
5.463 +goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
5.464 +by (eresolve_tac [CollectE] 1);
5.465 +by (REPEAT (eresolve_tac [exE, conjE] 1));
5.466 +by (res_inst_tac [("x","a")] exI 1);
5.467 +by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
5.468 +by (resolve_tac [conjI] 1 THEN (atac 1));
5.469 +by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
5.470 +by (dresolve_tac [lemma1] 1 THEN (REPEAT (atac 1)));
5.471 +by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
5.472 +by (resolve_tac [lemma2 RS ssubst] 1 THEN (REPEAT (atac 1)));
5.473 +by (fast_tac (ZF_cs addSIs [the_equality]) 1);
5.474 +val NN_imp_ex_inj = result();
5.475 +
5.476 +goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
5.477 +by (dresolve_tac [NN_imp_ex_inj] 1);
5.478 +by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
5.479 +val y_well_ord = result();
5.480 +
5.481 +(* ********************************************************************** *)
5.482 +(* reverse induction which lets us infer that 1 : NN(y) *)
5.483 +(* ********************************************************************** *)
5.484 +
5.485 +val [prem1, prem2] = goal thy
5.486 + "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
5.487 +\ ==> n~=0 --> P(n) --> P(1)";
5.488 +by (res_inst_tac [("n","n")] nat_induct 1);
5.489 +by (resolve_tac [prem1] 1);
5.490 +by (fast_tac ZF_cs 1);
5.491 +by (excluded_middle_tac "x=0" 1);
5.492 +by (fast_tac ZF_cs 2);
5.493 +by (fast_tac (ZF_cs addSIs [prem2]) 1);
5.494 +val rev_induct_lemma = result();
5.495 +
5.496 +val prems = goal thy
5.497 + "[| P(n); n:nat; n~=0; \
5.498 +\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
5.499 +\ ==> P(1)";
5.500 +by (resolve_tac [rev_induct_lemma RS impE] 1);
5.501 +by (eresolve_tac [impE] 4 THEN (atac 5));
5.502 +by (REPEAT (ares_tac prems 1));
5.503 +val rev_induct = result();
5.504 +
5.505 +goalw thy [NN_def] "!!n. n:NN(y) ==> n:nat";
5.506 +by (fast_tac ZF_cs 1);
5.507 +val NN_into_nat = result();
5.508 +
5.509 +goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
5.510 +by (resolve_tac [rev_induct] 1 THEN (REPEAT (ares_tac [NN_into_nat] 1)));
5.511 +by (resolve_tac [lemma_ii] 1 THEN (REPEAT (atac 1)));
5.512 +val lemma3 = result();
5.513 +
5.514 +(* ********************************************************************** *)
5.515 +(* Main theorem "WO6 ==> WO1" *)
5.516 +(* ********************************************************************** *)
5.517 +
5.518 +(* another helpful lemma *)
5.519 +goalw thy [NN_def] "!!y. 0:NN(y) ==> y=0";
5.520 +by (fast_tac (AC_cs addSIs [equalityI]
5.521 + addSDs [lepoll_0_is_0] addEs [subst]) 1);
5.522 +val NN_y_0 = result();
5.523 +
5.524 +goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
5.525 +by (resolve_tac [allI] 1);
5.526 +by (excluded_middle_tac "A=0" 1);
5.527 +by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
5.528 +by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
5.529 +by (eresolve_tac [exE] 1);
5.530 +by (dresolve_tac [WO6_imp_NN_not_empty] 1);
5.531 +by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
5.532 +by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
5.533 +by (forward_tac [y_well_ord] 1);
5.534 +by (fast_tac (ZF_cs addEs [well_ord_subset]) 2);
5.535 +by (fast_tac (ZF_cs addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
5.536 +qed "WO6_imp_WO1";
5.537 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/ZF/AC/WO6_WO1.thy Fri Mar 31 11:55:29 1995 +0200
6.3 @@ -0,0 +1,3 @@
6.4 +(*Dummy theory to document dependencies *)
6.5 +
6.6 +WO6_WO1 = "rel_is_fun" + AC_Equiv
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/ZF/AC/rel_is_fun.ML Fri Mar 31 11:55:29 1995 +0200
7.3 @@ -0,0 +1,75 @@
7.4 +(* Title: ZF/AC/rel_is_fun.ML
7.5 + ID: $Id$
7.6 + Author: Krzysztof Gr`abczewski
7.7 +
7.8 +Lemmas needed to state when a finite relation is a function.
7.9 +
7.10 +The criteria are cardinalities of the relation and its domain.
7.11 +Used in WO6WO1.ML
7.12 +*)
7.13 +
7.14 +goalw Cardinal.thy [lepoll_def]
7.15 + "!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m";
7.16 +by (eresolve_tac [exE] 1);
7.17 +by (res_inst_tac [("x",
7.18 + "lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1);
7.19 +by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1);
7.20 +by (fast_tac (ZF_cs addIs [LeastI2, nat_into_Ord RS Ord_in_Ord,
7.21 + inj_is_fun RS apply_type]) 1);
7.22 +by (eresolve_tac [domainE] 1);
7.23 +by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
7.24 +by (resolve_tac [LeastI2] 1);
7.25 +by (REPEAT (fast_tac (ZF_cs addIs [fst_conv, left_inverse RS ssubst]
7.26 + addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
7.27 +val lepoll_m_imp_domain_lepoll_m = result();
7.28 +
7.29 +goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
7.30 +by (resolve_tac [equalityI] 1);
7.31 +by (fast_tac (ZF_cs addSIs [domain_mono]) 1);
7.32 +by (resolve_tac [subsetI] 1);
7.33 +by (excluded_middle_tac "x = a" 1);
7.34 +by (REPEAT (fast_tac (ZF_cs addSIs [domainI] addSEs [domainE]) 1));
7.35 +val domain_diff_eq_domain = result();
7.36 +
7.37 +goal Cardinal.thy
7.38 + "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
7.39 +\ ALL a:domain(r). EX! b. <a, b> : r";
7.40 +by (resolve_tac [ballI] 1);
7.41 +by (eresolve_tac [domainE] 1);
7.42 +by (resolve_tac [ex1I] 1 THEN (atac 1));
7.43 +by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2));
7.44 +by (fast_tac (ZF_cs addSEs [lepoll_trans RS succ_lepoll_natE,
7.45 + diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)]
7.46 + addEs [not_sym RSN (2, domain_diff_eq_domain) RS subst]) 1);
7.47 +val rel_domain_ex1 = result();
7.48 +
7.49 +goal ZF.thy "!! r. [| ALL a:A. EX! b. <a,b> : r; r<=A*B |] \
7.50 +\ ==> r = (lam a:A. THE b. <a,b> : r)";
7.51 +by (resolve_tac [equalityI] 1);
7.52 +by (resolve_tac [subsetI] 1);
7.53 +by (dresolve_tac [subsetD] 1 THEN (atac 1));
7.54 +by (eresolve_tac [SigmaE] 1);
7.55 +by (hyp_subst_tac 1);
7.56 +by (dresolve_tac [bspec] 1 THEN (atac 1));
7.57 +by (eresolve_tac [lamI RS subst_elem] 1);
7.58 +by (forward_tac [theI] 1);
7.59 +by (asm_simp_tac ZF_ss 1);
7.60 +by (fast_tac (ZF_cs addIs [theI] addSEs [bspec] addSEs [lamE]) 2);
7.61 +by (eresolve_tac [ex1_equalsE] 1 THEN (REPEAT (atac 1)));
7.62 +val rel_is_lam = result();
7.63 +
7.64 +goal ZF.thy "!! r. [| ALL a:A. EX! b. <a,b> : r; r<=A*B |] \
7.65 +\ ==> (lam a:A. THE b. <a,b> : r) : A->B";
7.66 +by (fast_tac (ZF_cs addSIs [lam_type] addSEs [Pair_inject]
7.67 + addSDs [bspec, theI]) 1);
7.68 +val lam_the_type = result();
7.69 +
7.70 +goal Cardinal.thy
7.71 + "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat; \
7.72 +\ r<=A*B; A=domain(r) |] ==> r: A->B";
7.73 +by (hyp_subst_tac 1);
7.74 +by (resolve_tac [rel_domain_ex1 RS
7.75 + (rel_domain_ex1 RS rel_is_lam RSN (3,
7.76 + lam_the_type RS subst_elem))] 1
7.77 + THEN (TRYALL atac));
7.78 +val rel_is_fun = result();
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/ZF/AC/rel_is_fun.thy Fri Mar 31 11:55:29 1995 +0200
8.3 @@ -0,0 +1,3 @@
8.4 +(*Dummy theory to document dependencies *)
8.5 +
8.6 +rel_is_fun = "Cardinal"