author | nipkow |
Sat, 08 Aug 2020 18:20:09 +0200 | |
changeset 72122 | 2dcb6523f6af |
parent 61980 | 6b780867d426 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
12776 | 1 |
(* Title: ZF/AC/AC15_WO6.thy |
2 |
Author: Krzysztof Grabczewski |
|
3 |
||
4 |
The proofs needed to state that AC10, ..., AC15 are equivalent to the rest. |
|
5 |
We need the following: |
|
6 |
||
7 |
WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6 |
|
8 |
||
9 |
In order to add the formulations AC13 and AC14 we need: |
|
10 |
||
11 |
AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15 |
|
12 |
||
13 |
or |
|
14 |
||
15 |
AC1 ==> AC13(1); AC13(m) ==> AC13(n) ==> AC14 ==> AC15 (m\<le>n) |
|
16 |
||
17 |
So we don't have to prove all implications of both cases. |
|
18 |
Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as |
|
19 |
Rubin & Rubin do. |
|
20 |
*) |
|
21 |
||
27678 | 22 |
theory AC15_WO6 |
23 |
imports HH Cardinal_aux |
|
24 |
begin |
|
12776 | 25 |
|
26 |
||
27 |
(* ********************************************************************** *) |
|
28 |
(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) |
|
29 |
(* or AC15 *) |
|
30 |
(* - cons_times_nat_not_Finite *) |
|
31 |
(* - ex_fun_AC13_AC15 *) |
|
32 |
(* ********************************************************************** *) |
|
33 |
||
34 |
lemma lepoll_Sigma: "A\<noteq>0 ==> B \<lesssim> A*B" |
|
35 |
apply (unfold lepoll_def) |
|
36 |
apply (erule not_emptyE) |
|
37 |
apply (rule_tac x = "\<lambda>z \<in> B. <x,z>" in exI) |
|
38 |
apply (fast intro!: snd_conv lam_injective) |
|
39 |
done |
|
40 |
||
41 |
lemma cons_times_nat_not_Finite: |
|
42 |
"0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)" |
|
43 |
apply clarify |
|
44 |
apply (rule nat_not_Finite [THEN notE] ) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
45 |
apply (subgoal_tac "x \<noteq> 0") |
13245 | 46 |
apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+ |
12776 | 47 |
done |
48 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
49 |
lemma lemma1: "[| \<Union>(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A" |
12776 | 50 |
by fast |
51 |
||
52 |
lemma lemma2: |
|
53 |
"[| pairwise_disjoint(A); B \<in> A; C \<in> A; a \<in> B; a \<in> C |] ==> B=C" |
|
54 |
by (unfold pairwise_disjoint_def, blast) |
|
55 |
||
56 |
lemma lemma3: |
|
12788 | 57 |
"\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) & |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
58 |
sets_of_size_between(f`B, 2, n) & \<Union>(f`B)=B |
12788 | 59 |
==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) & |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
60 |
0 \<in> u & 2 \<lesssim> u & u \<lesssim> n" |
12776 | 61 |
apply (unfold sets_of_size_between_def) |
62 |
apply (rule ballI) |
|
12788 | 63 |
apply (erule_tac x="cons(0, B*nat)" in ballE) |
12820 | 64 |
apply (blast dest: lemma1 intro!: lemma2, blast) |
12776 | 65 |
done |
66 |
||
67 |
lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i" |
|
68 |
apply (unfold lepoll_def) |
|
69 |
apply (erule exE) |
|
61394 | 70 |
apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) & f`a=j" |
12776 | 71 |
in exI) |
72 |
apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective) |
|
73 |
apply (erule RepFunE) |
|
74 |
apply (frule inj_is_fun [THEN apply_type], assumption) |
|
75 |
apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type]) |
|
76 |
apply (erule RepFunE) |
|
77 |
apply (rule LeastI2) |
|
78 |
apply fast |
|
79 |
apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type]) |
|
80 |
apply (fast elim: sym left_inverse [THEN ssubst]) |
|
81 |
done |
|
82 |
||
83 |
lemma lemma5_1: |
|
84 |
"[| B \<in> A; 2 \<lesssim> u(B) |] ==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<noteq> 0" |
|
85 |
apply simp |
|
86 |
apply (fast dest: lepoll_Diff_sing |
|
87 |
elim: lepoll_trans [THEN succ_lepoll_natE] ssubst |
|
88 |
intro!: lepoll_refl) |
|
89 |
done |
|
90 |
||
91 |
lemma lemma5_2: |
|
92 |
"[| B \<in> A; u(B) \<subseteq> cons(0, B*nat) |] |
|
93 |
==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<subseteq> B" |
|
94 |
apply auto |
|
95 |
done |
|
96 |
||
97 |
lemma lemma5_3: |
|
98 |
"[| n \<in> nat; B \<in> A; 0 \<in> u(B); u(B) \<lesssim> succ(n) |] |
|
99 |
==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<lesssim> n" |
|
100 |
apply simp |
|
101 |
apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]]) |
|
102 |
done |
|
103 |
||
104 |
lemma ex_fun_AC13_AC15: |
|
105 |
"[| \<forall>B \<in> {cons(0, x*nat). x \<in> A}. |
|
106 |
pairwise_disjoint(f`B) & |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
107 |
sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B; |
12776 | 108 |
n \<in> nat |] |
109 |
==> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 & f`B \<subseteq> B & f`B \<lesssim> n" |
|
110 |
by (fast del: subsetI notI |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
111 |
dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3) |
12776 | 112 |
|
113 |
||
114 |
(* ********************************************************************** *) |
|
115 |
(* The target proofs *) |
|
116 |
(* ********************************************************************** *) |
|
117 |
||
118 |
(* ********************************************************************** *) |
|
119 |
(* AC10(n) ==> AC11 *) |
|
120 |
(* ********************************************************************** *) |
|
121 |
||
12788 | 122 |
theorem AC10_AC11: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC11" |
12776 | 123 |
by (unfold AC10_def AC11_def, blast) |
124 |
||
125 |
(* ********************************************************************** *) |
|
126 |
(* AC11 ==> AC12 *) |
|
127 |
(* ********************************************************************** *) |
|
128 |
||
12788 | 129 |
theorem AC11_AC12: "AC11 ==> AC12" |
12776 | 130 |
by (unfold AC10_def AC11_def AC11_def AC12_def, blast) |
131 |
||
132 |
(* ********************************************************************** *) |
|
133 |
(* AC12 ==> AC15 *) |
|
134 |
(* ********************************************************************** *) |
|
135 |
||
12788 | 136 |
theorem AC12_AC15: "AC12 ==> AC15" |
12776 | 137 |
apply (unfold AC12_def AC15_def) |
138 |
apply (blast del: ballI |
|
139 |
intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15) |
|
140 |
done |
|
1123 | 141 |
|
12776 | 142 |
(* ********************************************************************** *) |
143 |
(* AC15 ==> WO6 *) |
|
144 |
(* ********************************************************************** *) |
|
145 |
||
146 |
lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))" |
|
147 |
by (fast intro!: ltI dest!: ltD) |
|
148 |
||
13535 | 149 |
lemma AC15_WO6_aux1: |
12776 | 150 |
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m |
61394 | 151 |
==> (\<Union>i<\<mu> x. HH(f,A,x)={A}. HH(f,A,i)) = A" |
12776 | 152 |
apply (simp add: Ord_Least [THEN OUN_eq_UN]) |
153 |
apply (rule equalityI) |
|
154 |
apply (fast dest!: less_Least_subset_x) |
|
155 |
apply (blast del: subsetI |
|
156 |
intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]]) |
|
157 |
done |
|
158 |
||
13535 | 159 |
lemma AC15_WO6_aux2: |
12776 | 160 |
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m |
61394 | 161 |
==> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m" |
12776 | 162 |
apply (rule oallI) |
163 |
apply (drule ltD [THEN less_Least_subset_x]) |
|
164 |
apply (frule HH_subset_imp_eq) |
|
165 |
apply (erule ssubst) |
|
166 |
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2]) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
167 |
(*but can't use del: DiffE despite the obvious conflict*) |
12776 | 168 |
done |
169 |
||
12788 | 170 |
theorem AC15_WO6: "AC15 ==> WO6" |
12776 | 171 |
apply (unfold AC15_def WO6_def) |
172 |
apply (rule allI) |
|
173 |
apply (erule_tac x = "Pow (A) -{0}" in allE) |
|
174 |
apply (erule impE, fast) |
|
175 |
apply (elim bexE conjE exE) |
|
176 |
apply (rule bexI) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12820
diff
changeset
|
177 |
apply (rule conjI, assumption) |
61394 | 178 |
apply (rule_tac x = "\<mu> i. HH (f,A,i) ={A}" in exI) |
179 |
apply (rule_tac x = "\<lambda>j \<in> (\<mu> i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12820
diff
changeset
|
180 |
apply (simp_all add: ltD) |
12776 | 181 |
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] |
13535 | 182 |
elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) |
12776 | 183 |
done |
184 |
||
185 |
||
186 |
(* ********************************************************************** *) |
|
187 |
(* The proof needed in the first case, not in the second *) |
|
188 |
(* ********************************************************************** *) |
|
189 |
||
190 |
(* ********************************************************************** *) |
|
191 |
(* AC10(n) ==> AC13(n-1) if 2\<le>n *) |
|
192 |
(* *) |
|
193 |
(* Because of the change to the formal definition of AC10(n) we prove *) |
|
194 |
(* the following obviously equivalent theorem \<in> *) |
|
195 |
(* AC10(n) implies AC13(n) for (1\<le>n) *) |
|
196 |
(* ********************************************************************** *) |
|
197 |
||
12788 | 198 |
theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)" |
12776 | 199 |
apply (unfold AC10_def AC13_def, safe) |
200 |
apply (erule allE) |
|
12820 | 201 |
apply (erule impE [OF _ cons_times_nat_not_Finite], assumption) |
12776 | 202 |
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite] |
203 |
dest!: ex_fun_AC13_AC15) |
|
204 |
done |
|
205 |
||
206 |
(* ********************************************************************** *) |
|
207 |
(* The proofs needed in the second case, not in the first *) |
|
208 |
(* ********************************************************************** *) |
|
209 |
||
210 |
(* ********************************************************************** *) |
|
211 |
(* AC1 ==> AC13(1) *) |
|
212 |
(* ********************************************************************** *) |
|
213 |
||
214 |
lemma AC1_AC13: "AC1 ==> AC13(1)" |
|
215 |
apply (unfold AC1_def AC13_def) |
|
216 |
apply (rule allI) |
|
217 |
apply (erule allE) |
|
218 |
apply (rule impI) |
|
219 |
apply (drule mp, assumption) |
|
220 |
apply (elim exE) |
|
221 |
apply (rule_tac x = "\<lambda>x \<in> A. {f`x}" in exI) |
|
222 |
apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll]) |
|
223 |
done |
|
224 |
||
225 |
(* ********************************************************************** *) |
|
226 |
(* AC13(m) ==> AC13(n) for m \<subseteq> n *) |
|
227 |
(* ********************************************************************** *) |
|
228 |
||
229 |
lemma AC13_mono: "[| m\<le>n; AC13(m) |] ==> AC13(n)" |
|
230 |
apply (unfold AC13_def) |
|
231 |
apply (drule le_imp_lepoll) |
|
232 |
apply (fast elim!: lepoll_trans) |
|
233 |
done |
|
234 |
||
235 |
(* ********************************************************************** *) |
|
236 |
(* The proofs necessary for both cases *) |
|
237 |
(* ********************************************************************** *) |
|
238 |
||
239 |
(* ********************************************************************** *) |
|
240 |
(* AC13(n) ==> AC14 if 1 \<subseteq> n *) |
|
241 |
(* ********************************************************************** *) |
|
242 |
||
12788 | 243 |
theorem AC13_AC14: "[| n \<in> nat; 1\<le>n; AC13(n) |] ==> AC14" |
12776 | 244 |
by (unfold AC13_def AC14_def, auto) |
245 |
||
246 |
(* ********************************************************************** *) |
|
247 |
(* AC14 ==> AC15 *) |
|
248 |
(* ********************************************************************** *) |
|
249 |
||
12788 | 250 |
theorem AC14_AC15: "AC14 ==> AC15" |
12776 | 251 |
by (unfold AC13_def AC14_def AC15_def, fast) |
252 |
||
253 |
(* ********************************************************************** *) |
|
254 |
(* The redundant proofs; however cited by Rubin & Rubin *) |
|
255 |
(* ********************************************************************** *) |
|
256 |
||
257 |
(* ********************************************************************** *) |
|
258 |
(* AC13(1) ==> AC1 *) |
|
259 |
(* ********************************************************************** *) |
|
260 |
||
261 |
lemma lemma_aux: "[| A\<noteq>0; A \<lesssim> 1 |] ==> \<exists>a. A={a}" |
|
262 |
by (fast elim!: not_emptyE lepoll_1_is_sing) |
|
263 |
||
264 |
lemma AC13_AC1_lemma: |
|
265 |
"\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1 |
|
61980 | 266 |
==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)" |
12776 | 267 |
apply (rule lam_type) |
268 |
apply (drule bspec, assumption) |
|
269 |
apply (elim conjE) |
|
270 |
apply (erule lemma_aux [THEN exE], assumption) |
|
12814 | 271 |
apply (simp add: the_equality) |
12776 | 272 |
done |
273 |
||
12788 | 274 |
theorem AC13_AC1: "AC13(1) ==> AC1" |
12776 | 275 |
apply (unfold AC13_def AC1_def) |
276 |
apply (fast elim!: AC13_AC1_lemma) |
|
277 |
done |
|
278 |
||
279 |
(* ********************************************************************** *) |
|
280 |
(* AC11 ==> AC14 *) |
|
281 |
(* ********************************************************************** *) |
|
282 |
||
12788 | 283 |
theorem AC11_AC14: "AC11 ==> AC14" |
12776 | 284 |
apply (unfold AC11_def AC14_def) |
285 |
apply (fast intro!: AC10_AC13) |
|
286 |
done |
|
287 |
||
288 |
end |
|
289 |