author | nipkow |
Sat, 08 Aug 2020 18:20:09 +0200 | |
changeset 72122 | 2dcb6523f6af |
parent 68847 | 511d163ab623 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/AC/AC16_WO4.thy |
2 |
Author: Krzysztof Grabczewski |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
3 |
|
12776 | 4 |
The proof of AC16(n, k) ==> WO4(n-k) |
5 |
||
6 |
Tidied (using locales) by LCP |
|
1196 | 7 |
*) |
8 |
||
27678 | 9 |
theory AC16_WO4 |
10 |
imports AC16_lemmas |
|
11 |
begin |
|
12776 | 12 |
|
13 |
(* ********************************************************************** *) |
|
14 |
(* The case of finite set *) |
|
15 |
(* ********************************************************************** *) |
|
16 |
||
17 |
lemma lemma1: |
|
18 |
"[| Finite(A); 0<m; m \<in> nat |] |
|
19 |
==> \<exists>a f. Ord(a) & domain(f) = a & |
|
20 |
(\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m)" |
|
21 |
apply (unfold Finite_def) |
|
22 |
apply (erule bexE) |
|
23 |
apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]]) |
|
24 |
apply (erule exE) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13175
diff
changeset
|
25 |
apply (rule_tac x = n in exI) |
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12960
diff
changeset
|
26 |
apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI) |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12960
diff
changeset
|
27 |
apply (simp add: ltD bij_def surj_def) |
12776 | 28 |
apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun] |
29 |
singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans] |
|
30 |
nat_1_lepoll_iff [THEN iffD2] |
|
31 |
elim!: apply_type ltE) |
|
32 |
done |
|
33 |
||
34 |
(* ********************************************************************** *) |
|
35 |
(* The case of infinite set *) |
|
36 |
(* ********************************************************************** *) |
|
37 |
||
38 |
(* well_ord(x,r) ==> well_ord({{y,z}. y \<in> x}, Something(x,z)) **) |
|
39 |
lemmas well_ord_paired = paired_bij [THEN bij_is_inj, THEN well_ord_rvimage] |
|
40 |
||
41 |
lemma lepoll_trans1: "[| A \<lesssim> B; ~ A \<lesssim> C |] ==> ~ B \<lesssim> C" |
|
42 |
by (blast intro: lepoll_trans) |
|
43 |
||
44 |
(* ********************************************************************** *) |
|
45 |
(* There exists a well ordered set y such that ... *) |
|
46 |
(* ********************************************************************** *) |
|
47 |
||
58860 | 48 |
lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll] |
12776 | 49 |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
50 |
lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)" |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
51 |
apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI) |
12776 | 52 |
apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel] |
53 |
Ord_Hartog [THEN well_ord_Memrel], THEN exE]) |
|
54 |
apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired |
|
55 |
lepoll_trans1 [OF _ not_Hartog_lepoll_self] |
|
56 |
lepoll_trans [OF subset_imp_lepoll lepoll_paired] |
|
57 |
elim!: nat_not_Finite [THEN notE] |
|
58 |
elim: mem_asym |
|
59 |
dest!: Un_upper1 [THEN subset_imp_lepoll, THEN lepoll_Finite] |
|
60 |
lepoll_paired [THEN lepoll_Finite]) |
|
61 |
done |
|
62 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
63 |
lemma infinite_Un: "~Finite(B) ==> ~Finite(A \<union> B)" |
12776 | 64 |
by (blast intro: subset_Finite) |
65 |
||
66 |
(* ********************************************************************** *) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
67 |
(* There is a v \<in> s(u) such that k \<lesssim> x \<inter> y (in our case succ(k)) *) |
12776 | 68 |
(* The idea of the proof is the following \<in> *) |
69 |
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y *) |
|
70 |
(* Thence y is less than or equipollent to {v \<in> Pow(x). v \<approx> n#-k} *) |
|
71 |
(* We have obtained this result in two steps \<in> *) |
|
72 |
(* 1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v} *) |
|
73 |
(* where a is certain k-2 element subset of y *) |
|
74 |
(* 2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent *) |
|
75 |
(* to {v \<in> Pow(x). v \<approx> n-k} *) |
|
76 |
(* ********************************************************************** *) |
|
77 |
||
78 |
(*Proof simplified by LCP*) |
|
79 |
lemma succ_not_lepoll_lemma: |
|
80 |
"[| ~(\<exists>x \<in> A. f`x=y); f \<in> inj(A, B); y \<in> B |] |
|
81 |
==> (\<lambda>a \<in> succ(A). if(a=A, y, f`a)) \<in> inj(succ(A), B)" |
|
82 |
apply (rule_tac d = "%z. if (z=y, A, converse (f) `z) " in lam_injective) |
|
83 |
apply (force simp add: inj_is_fun [THEN apply_type]) |
|
84 |
(*this preliminary simplification prevents looping somehow*) |
|
85 |
apply (simp (no_asm_simp)) |
|
86 |
apply force |
|
87 |
done |
|
88 |
||
89 |
lemma succ_not_lepoll_imp_eqpoll: "[| ~A \<approx> B; A \<lesssim> B |] ==> succ(A) \<lesssim> B" |
|
90 |
apply (unfold lepoll_def eqpoll_def bij_def surj_def) |
|
91 |
apply (fast elim!: succ_not_lepoll_lemma inj_is_fun) |
|
92 |
done |
|
93 |
||
94 |
||
95 |
(* ********************************************************************** *) |
|
96 |
(* There is a k-2 element subset of y *) |
|
97 |
(* ********************************************************************** *) |
|
98 |
||
99 |
lemmas ordertype_eqpoll = |
|
100 |
ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]] |
|
101 |
||
102 |
lemma cons_cons_subset: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
103 |
"[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x \<union> y)" |
12776 | 104 |
by fast |
105 |
||
106 |
lemma cons_cons_eqpoll: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
107 |
"[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x \<inter> y = 0 |] |
12776 | 108 |
==> cons(b, cons(u, a)) \<approx> succ(succ(k))" |
109 |
by (fast intro!: cons_eqpoll_succ) |
|
110 |
||
111 |
lemma set_eq_cons: |
|
112 |
"[| succ(k) \<approx> A; k \<approx> B; B \<subseteq> A; a \<in> A-B; k \<in> nat |] ==> A = cons(a, B)" |
|
113 |
apply (rule equalityI) |
|
114 |
prefer 2 apply fast |
|
115 |
apply (rule Diff_eq_0_iff [THEN iffD1]) |
|
116 |
apply (rule equals0I) |
|
117 |
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) |
|
118 |
apply (drule eqpoll_sym [THEN cons_eqpoll_succ], fast) |
|
119 |
apply (drule cons_eqpoll_succ, fast) |
|
120 |
apply (fast elim!: lepoll_trans [THEN lepoll_trans, THEN succ_lepoll_natE, |
|
121 |
OF eqpoll_sym [THEN eqpoll_imp_lepoll] subset_imp_lepoll]) |
|
122 |
done |
|
123 |
||
124 |
lemma cons_eqE: "[| cons(x,a) = cons(y,a); x \<notin> a |] ==> x = y " |
|
125 |
by (fast elim!: equalityE) |
|
126 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
127 |
lemma eq_imp_Int_eq: "A = B ==> A \<inter> C = B \<inter> C" |
12776 | 128 |
by blast |
129 |
||
130 |
(* ********************************************************************** *) |
|
131 |
(* some arithmetic *) |
|
132 |
(* ********************************************************************** *) |
|
133 |
||
134 |
lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]: |
|
135 |
"[| k \<in> nat; m \<in> nat |] |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
136 |
==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A \<longrightarrow> A-B \<lesssim> m" |
12776 | 137 |
apply (induct_tac "k") |
138 |
apply (simp add: add_0) |
|
139 |
apply (blast intro: eqpoll_imp_lepoll lepoll_trans |
|
140 |
Diff_subset [THEN subset_imp_lepoll]) |
|
141 |
apply (intro allI impI) |
|
142 |
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], fast) |
|
143 |
apply (erule_tac x = "A - {xa}" in allE) |
|
144 |
apply (erule_tac x = "B - {xa}" in allE) |
|
145 |
apply (erule impE) |
|
146 |
apply (simp add: add_succ) |
|
147 |
apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing) |
|
12820 | 148 |
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp) |
12776 | 149 |
apply blast |
150 |
done |
|
151 |
||
152 |
lemma eqpoll_sum_imp_Diff_lepoll: |
|
153 |
"[| A \<approx> succ(k #+ m); B \<subseteq> A; succ(k) \<lesssim> B; k \<in> nat; m \<in> nat |] |
|
154 |
==> A-B \<lesssim> m" |
|
155 |
apply (simp only: add_succ [symmetric]) |
|
156 |
apply (blast intro: eqpoll_sum_imp_Diff_lepoll_lemma) |
|
157 |
done |
|
158 |
||
159 |
(* ********************************************************************** *) |
|
160 |
(* similar properties for \<approx> *) |
|
161 |
(* ********************************************************************** *) |
|
162 |
||
163 |
lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]: |
|
164 |
"[| k \<in> nat; m \<in> nat |] |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
165 |
==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A \<longrightarrow> A-B \<approx> m" |
12776 | 166 |
apply (induct_tac "k") |
167 |
apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0]) |
|
168 |
apply (intro allI impI) |
|
169 |
apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE]) |
|
170 |
apply (fast elim!: eqpoll_imp_lepoll) |
|
171 |
apply (erule_tac x = "A - {xa}" in allE) |
|
172 |
apply (erule_tac x = "B - {xa}" in allE) |
|
173 |
apply (erule impE) |
|
174 |
apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll) |
|
12820 | 175 |
apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp) |
12776 | 176 |
apply blast |
177 |
done |
|
178 |
||
179 |
lemma eqpoll_sum_imp_Diff_eqpoll: |
|
180 |
"[| A \<approx> succ(k #+ m); B \<subseteq> A; succ(k) \<approx> B; k \<in> nat; m \<in> nat |] |
|
181 |
==> A-B \<approx> m" |
|
182 |
apply (simp only: add_succ [symmetric]) |
|
183 |
apply (blast intro: eqpoll_sum_imp_Diff_eqpoll_lemma) |
|
184 |
done |
|
185 |
||
186 |
||
187 |
(* ********************************************************************** *) |
|
188 |
(* LL can be well ordered *) |
|
189 |
(* ********************************************************************** *) |
|
190 |
||
191 |
lemma subsets_lepoll_0_eq_unit: "{x \<in> Pow(X). x \<lesssim> 0} = {0}" |
|
192 |
by (fast dest!: lepoll_0_is_0 intro!: lepoll_refl) |
|
193 |
||
194 |
lemma subsets_lepoll_succ: |
|
195 |
"n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> succ(n)} = |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
196 |
{z \<in> Pow(y). z \<lesssim> n} \<union> {z \<in> Pow(y). z \<approx> succ(n)}" |
12776 | 197 |
by (blast intro: leI le_imp_lepoll nat_into_Ord |
198 |
lepoll_trans eqpoll_imp_lepoll |
|
199 |
dest!: lepoll_succ_disj) |
|
200 |
||
201 |
lemma Int_empty: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
202 |
"n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} \<inter> {z \<in> Pow(y). z \<approx> succ(n)} = 0" |
12776 | 203 |
by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] |
204 |
succ_lepoll_natE) |
|
205 |
||
27678 | 206 |
locale AC16 = |
12776 | 207 |
fixes x and y and k and l and m and t_n and R and MM and LL and GG and s |
208 |
defines k_def: "k == succ(l)" |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
209 |
and MM_def: "MM == {v \<in> t_n. succ(k) \<lesssim> v \<inter> y}" |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
210 |
and LL_def: "LL == {v \<inter> y. v \<in> MM}" |
12776 | 211 |
and GG_def: "GG == \<lambda>v \<in> LL. (THE w. w \<in> MM & v \<subseteq> w) - v" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
212 |
and s_def: "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v \<inter> y}" |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
213 |
assumes all_ex: "\<forall>z \<in> {z \<in> Pow(x \<union> y) . z \<approx> succ(k)}. |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
214 |
\<exists>! w. w \<in> t_n & z \<subseteq> w " |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
215 |
and disjoint[iff]: "x \<inter> y = 0" |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
216 |
and "includes": "t_n \<subseteq> {v \<in> Pow(x \<union> y). v \<approx> succ(k #+ m)}" |
12776 | 217 |
and WO_R[iff]: "well_ord(y,R)" |
218 |
and lnat[iff]: "l \<in> nat" |
|
219 |
and mnat[iff]: "m \<in> nat" |
|
220 |
and mpos[iff]: "0<m" |
|
221 |
and Infinite[iff]: "~ Finite(y)" |
|
222 |
and noLepoll: "~ y \<lesssim> {v \<in> Pow(x). v \<approx> m}" |
|
68847 | 223 |
begin |
12776 | 224 |
|
68847 | 225 |
lemma knat [iff]: "k \<in> nat" |
12776 | 226 |
by (simp add: k_def) |
227 |
||
228 |
||
229 |
(* ********************************************************************** *) |
|
230 |
(* 1. y is less than or equipollent to {v \<in> s(u). a \<subseteq> v} *) |
|
231 |
(* where a is certain k-2 element subset of y *) |
|
232 |
(* ********************************************************************** *) |
|
233 |
||
68847 | 234 |
lemma Diff_Finite_eqpoll: "[| l \<approx> a; a \<subseteq> y |] ==> y - a \<approx> y" |
12776 | 235 |
apply (insert WO_R Infinite lnat) |
236 |
apply (rule eqpoll_trans) |
|
237 |
apply (rule Diff_lesspoll_eqpoll_Card) |
|
238 |
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) |
|
239 |
apply (blast intro: lesspoll_trans1 |
|
240 |
intro!: Card_cardinal |
|
241 |
Card_cardinal [THEN Card_is_Ord, THEN nat_le_infinite_Ord, |
|
242 |
THEN le_imp_lepoll] |
|
243 |
dest: well_ord_cardinal_eqpoll |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
244 |
eqpoll_sym eqpoll_imp_lepoll |
12776 | 245 |
n_lesspoll_nat [THEN lesspoll_trans2] |
246 |
well_ord_cardinal_eqpoll [THEN eqpoll_sym, |
|
247 |
THEN eqpoll_imp_lepoll, THEN lepoll_infinite])+ |
|
248 |
done |
|
249 |
||
250 |
||
68847 | 251 |
lemma s_subset: "s(u) \<subseteq> t_n" |
12776 | 252 |
by (unfold s_def, blast) |
253 |
||
68847 | 254 |
lemma sI: |
12776 | 255 |
"[| w \<in> t_n; cons(b,cons(u,a)) \<subseteq> w; a \<subseteq> y; b \<in> y-a; l \<approx> a |] |
256 |
==> w \<in> s(u)" |
|
257 |
apply (unfold s_def succ_def k_def) |
|
258 |
apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong] |
|
259 |
intro: subset_imp_lepoll lepoll_trans) |
|
260 |
done |
|
261 |
||
68847 | 262 |
lemma in_s_imp_u_in: "v \<in> s(u) ==> u \<in> v" |
12776 | 263 |
by (unfold s_def, blast) |
264 |
||
265 |
||
68847 | 266 |
lemma ex1_superset_a: |
12776 | 267 |
"[| l \<approx> a; a \<subseteq> y; b \<in> y - a; u \<in> x |] |
268 |
==> \<exists>! c. c \<in> s(u) & a \<subseteq> c & b \<in> c" |
|
269 |
apply (rule all_ex [simplified k_def, THEN ballE]) |
|
270 |
apply (erule ex1E) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13175
diff
changeset
|
271 |
apply (rule_tac a = w in ex1I, blast intro: sI) |
12776 | 272 |
apply (blast dest: s_subset [THEN subsetD] in_s_imp_u_in) |
273 |
apply (blast del: PowI |
|
274 |
intro!: cons_cons_subset eqpoll_sym [THEN cons_cons_eqpoll]) |
|
275 |
done |
|
276 |
||
68847 | 277 |
lemma the_eq_cons: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
278 |
"[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; |
12776 | 279 |
l \<approx> a; a \<subseteq> y; b \<in> y - a; u \<in> x |] |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
280 |
==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) \<inter> y = cons(b, a)" |
12776 | 281 |
apply (frule ex1_superset_a [THEN theI], assumption+) |
282 |
apply (rule set_eq_cons) |
|
283 |
apply (fast+) |
|
284 |
done |
|
285 |
||
68847 | 286 |
lemma y_lepoll_subset_s: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
287 |
"[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; |
12776 | 288 |
l \<approx> a; a \<subseteq> y; u \<in> x |] |
289 |
==> y \<lesssim> {v \<in> s(u). a \<subseteq> v}" |
|
290 |
apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, |
|
291 |
THEN lepoll_trans], fast+) |
|
292 |
apply (rule_tac f3 = "\<lambda>b \<in> y-a. THE c. c \<in> s (u) & a \<subseteq> c & b \<in> c" |
|
293 |
in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]]) |
|
294 |
apply (simp add: inj_def) |
|
295 |
apply (rule conjI) |
|
296 |
apply (rule lam_type) |
|
297 |
apply (frule ex1_superset_a [THEN theI], fast+, clarify) |
|
298 |
apply (rule cons_eqE [of _ a]) |
|
59788 | 299 |
apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq) |
12776 | 300 |
apply (simp_all add: the_eq_cons) |
301 |
done |
|
302 |
||
303 |
||
304 |
(* ********************************************************************** *) |
|
305 |
(* back to the second part *) |
|
306 |
(* ********************************************************************** *) |
|
307 |
||
308 |
||
309 |
(*relies on the disjointness of x, y*) |
|
68847 | 310 |
lemma x_imp_not_y [dest]: "a \<in> x ==> a \<notin> y" |
12776 | 311 |
by (blast dest: disjoint [THEN equalityD1, THEN subsetD, OF IntI]) |
312 |
||
68847 | 313 |
lemma w_Int_eq_w_Diff: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
314 |
"w \<subseteq> x \<union> y ==> w \<inter> (x - {u}) = w - cons(u, w \<inter> y)" |
12776 | 315 |
by blast |
316 |
||
68847 | 317 |
lemma w_Int_eqpoll_m: |
12776 | 318 |
"[| w \<in> {v \<in> s(u). a \<subseteq> v}; |
319 |
l \<approx> a; u \<in> x; |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
320 |
\<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y |] |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
321 |
==> w \<inter> (x - {u}) \<approx> m" |
12776 | 322 |
apply (erule CollectE) |
323 |
apply (subst w_Int_eq_w_Diff) |
|
324 |
apply (fast dest!: s_subset [THEN subsetD] |
|
12960 | 325 |
"includes" [simplified k_def, THEN subsetD]) |
12776 | 326 |
apply (blast dest: s_subset [THEN subsetD] |
12960 | 327 |
"includes" [simplified k_def, THEN subsetD] |
12776 | 328 |
dest: eqpoll_sym [THEN cons_eqpoll_succ, THEN eqpoll_sym] |
329 |
in_s_imp_u_in |
|
330 |
intro!: eqpoll_sum_imp_Diff_eqpoll) |
|
331 |
done |
|
332 |
||
333 |
||
334 |
(* ********************************************************************** *) |
|
335 |
(* 2. {v \<in> s(u). a \<subseteq> v} is less than or equipollent *) |
|
336 |
(* to {v \<in> Pow(x). v \<approx> n-k} *) |
|
337 |
(* ********************************************************************** *) |
|
338 |
||
68847 | 339 |
lemma eqpoll_m_not_empty: "a \<approx> m ==> a \<noteq> 0" |
12776 | 340 |
apply (insert mpos) |
341 |
apply (fast elim!: zero_lt_natE dest!: eqpoll_succ_imp_not_empty) |
|
342 |
done |
|
343 |
||
68847 | 344 |
lemma cons_cons_in: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
345 |
"[| z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |] |
12776 | 346 |
==> \<exists>! w. w \<in> t_n & cons(z, cons(u, a)) \<subseteq> w" |
347 |
apply (rule all_ex [THEN bspec]) |
|
348 |
apply (unfold k_def) |
|
349 |
apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym) |
|
350 |
done |
|
351 |
||
68847 | 352 |
lemma subset_s_lepoll_w: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
353 |
"[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; a \<subseteq> y; l \<approx> a; u \<in> x |] |
12776 | 354 |
==> {v \<in> s(u). a \<subseteq> v} \<lesssim> {v \<in> Pow(x). v \<approx> m}" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
355 |
apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w \<inter> (x - {u})" |
12776 | 356 |
in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]]) |
357 |
apply (simp add: inj_def) |
|
358 |
apply (intro conjI lam_type CollectI) |
|
359 |
apply fast |
|
360 |
apply (blast intro: w_Int_eqpoll_m) |
|
361 |
apply (intro ballI impI) |
|
362 |
(** LEVEL 8 **) |
|
363 |
apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE]) |
|
364 |
apply (blast, assumption+) |
|
12820 | 365 |
apply (drule equalityD1 [THEN subsetD], assumption) |
12776 | 366 |
apply (frule cons_cons_in, assumption+) |
367 |
apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+ |
|
368 |
done |
|
369 |
||
370 |
||
371 |
(* ********************************************************************** *) |
|
372 |
(* well_ord_subsets_lepoll_n *) |
|
373 |
(* ********************************************************************** *) |
|
374 |
||
68847 | 375 |
lemma well_ord_subsets_eqpoll_n: |
12776 | 376 |
"n \<in> nat ==> \<exists>S. well_ord({z \<in> Pow(y) . z \<approx> succ(n)}, S)" |
377 |
apply (rule WO_R [THEN well_ord_infinite_subsets_eqpoll_X, |
|
378 |
THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE]) |
|
379 |
apply (fast intro: bij_is_inj [THEN well_ord_rvimage])+ |
|
380 |
done |
|
381 |
||
68847 | 382 |
lemma well_ord_subsets_lepoll_n: |
12776 | 383 |
"n \<in> nat ==> \<exists>R. well_ord({z \<in> Pow(y). z \<lesssim> n}, R)" |
384 |
apply (induct_tac "n") |
|
385 |
apply (force intro!: well_ord_unit simp add: subsets_lepoll_0_eq_unit) |
|
386 |
apply (erule exE) |
|
387 |
apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption) |
|
388 |
apply (simp add: subsets_lepoll_succ) |
|
12820 | 389 |
apply (drule well_ord_radd, assumption) |
12776 | 390 |
apply (erule Int_empty [THEN disj_Un_eqpoll_sum, |
391 |
THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE]) |
|
392 |
apply (fast elim!: bij_is_inj [THEN well_ord_rvimage]) |
|
393 |
done |
|
394 |
||
395 |
||
68847 | 396 |
lemma LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}" |
12776 | 397 |
apply (unfold LL_def MM_def) |
12960 | 398 |
apply (insert "includes") |
12776 | 399 |
apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans) |
400 |
done |
|
401 |
||
68847 | 402 |
lemma well_ord_LL: "\<exists>S. well_ord(LL,S)" |
12776 | 403 |
apply (rule well_ord_subsets_lepoll_n [THEN exE, of "succ(k#+m)"]) |
404 |
apply simp |
|
405 |
apply (blast intro: well_ord_subset [OF _ LL_subset]) |
|
406 |
done |
|
407 |
||
408 |
(* ********************************************************************** *) |
|
409 |
(* every element of LL is a contained in exactly one element of MM *) |
|
410 |
(* ********************************************************************** *) |
|
411 |
||
68847 | 412 |
lemma unique_superset_in_MM: |
12776 | 413 |
"v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w" |
12820 | 414 |
apply (unfold MM_def LL_def, safe, fast) |
415 |
apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13175
diff
changeset
|
416 |
apply (rule_tac x = x in all_ex [THEN ballE]) |
12776 | 417 |
apply (blast intro: eqpoll_sym)+ |
418 |
done |
|
419 |
||
420 |
||
421 |
(* ********************************************************************** *) |
|
422 |
(* The function GG satisfies the conditions of WO4 *) |
|
423 |
(* ********************************************************************** *) |
|
424 |
||
425 |
(* ********************************************************************** *) |
|
426 |
(* The union of appropriate values is the whole x *) |
|
427 |
(* ********************************************************************** *) |
|
428 |
||
68847 | 429 |
lemma Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL" |
12776 | 430 |
by (unfold LL_def, fast) |
431 |
||
68847 | 432 |
lemma in_LL_eq_Int: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
433 |
"v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) \<inter> y" |
12776 | 434 |
apply (unfold LL_def, clarify) |
435 |
apply (subst unique_superset_in_MM [THEN the_equality2]) |
|
436 |
apply (auto simp add: Int_in_LL) |
|
437 |
done |
|
438 |
||
68847 | 439 |
lemma unique_superset1: "a \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> a \<subseteq> x) \<in> MM" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13175
diff
changeset
|
440 |
by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) |
12776 | 441 |
|
68847 | 442 |
lemma the_in_MM_subset: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
443 |
"v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x \<union> y" |
12776 | 444 |
apply (drule unique_superset1) |
445 |
apply (unfold MM_def) |
|
12960 | 446 |
apply (fast dest!: unique_superset1 "includes" [THEN subsetD]) |
12776 | 447 |
done |
448 |
||
68847 | 449 |
lemma GG_subset: "v \<in> LL ==> GG ` v \<subseteq> x" |
12776 | 450 |
apply (unfold GG_def) |
451 |
apply (frule the_in_MM_subset) |
|
452 |
apply (frule in_LL_eq_Int) |
|
453 |
apply (force elim: equalityE) |
|
454 |
done |
|
455 |
||
68847 | 456 |
lemma nat_lepoll_ordertype: "nat \<lesssim> ordertype(y, R)" |
12776 | 457 |
apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll]) |
458 |
apply (rule Ord_ordertype [OF WO_R]) |
|
459 |
apply (rule ordertype_eqpoll [THEN eqpoll_imp_lepoll, THEN lepoll_infinite]) |
|
460 |
apply (rule WO_R) |
|
461 |
apply (rule Infinite) |
|
462 |
done |
|
463 |
||
68847 | 464 |
lemma ex_subset_eqpoll_n: "n \<in> nat ==> \<exists>z. z \<subseteq> y & n \<approx> z" |
12776 | 465 |
apply (erule nat_lepoll_imp_ex_eqpoll_n) |
466 |
apply (rule lepoll_trans [OF nat_lepoll_ordertype]) |
|
467 |
apply (rule ordertype_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]) |
|
468 |
apply (rule WO_R) |
|
469 |
done |
|
470 |
||
471 |
||
68847 | 472 |
lemma exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y" |
12776 | 473 |
apply (rule ccontr) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
474 |
apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y") |
12776 | 475 |
prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll) |
476 |
apply (unfold k_def) |
|
12960 | 477 |
apply (insert all_ex "includes" lnat) |
12776 | 478 |
apply (rule ex_subset_eqpoll_n [THEN exE], assumption) |
479 |
apply (rule noLepoll [THEN notE]) |
|
480 |
apply (blast intro: lepoll_trans [OF y_lepoll_subset_s subset_s_lepoll_w]) |
|
481 |
done |
|
482 |
||
68847 | 483 |
lemma exists_in_MM: "u \<in> x ==> \<exists>w \<in> MM. u \<in> w" |
12776 | 484 |
apply (erule exists_proper_in_s [THEN bexE]) |
485 |
apply (unfold MM_def s_def, fast) |
|
486 |
done |
|
487 |
||
68847 | 488 |
lemma exists_in_LL: "u \<in> x ==> \<exists>w \<in> LL. u \<in> GG`w" |
12776 | 489 |
apply (rule exists_in_MM [THEN bexE], assumption) |
490 |
apply (rule bexI) |
|
491 |
apply (erule_tac [2] Int_in_LL) |
|
492 |
apply (unfold GG_def) |
|
493 |
apply (simp add: Int_in_LL) |
|
494 |
apply (subst unique_superset_in_MM [THEN the_equality2]) |
|
495 |
apply (fast elim!: Int_in_LL)+ |
|
496 |
done |
|
497 |
||
68847 | 498 |
lemma OUN_eq_x: "well_ord(LL,S) ==> |
12776 | 499 |
(\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x" |
500 |
apply (rule equalityI) |
|
501 |
apply (rule subsetI) |
|
502 |
apply (erule OUN_E) |
|
503 |
apply (rule GG_subset [THEN subsetD]) |
|
504 |
prefer 2 apply assumption |
|
505 |
apply (blast intro: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, |
|
506 |
THEN apply_type]) |
|
507 |
apply (rule subsetI) |
|
508 |
apply (erule exists_in_LL [THEN bexE]) |
|
509 |
apply (force intro: ltI [OF _ Ord_ordertype] |
|
510 |
ordermap_type [THEN apply_type] |
|
511 |
simp add: ordermap_bij [THEN bij_is_inj, THEN left_inverse]) |
|
512 |
done |
|
513 |
||
514 |
(* ********************************************************************** *) |
|
515 |
(* Every element of the family is less than or equipollent to n-k (m) *) |
|
516 |
(* ********************************************************************** *) |
|
517 |
||
68847 | 518 |
lemma in_MM_eqpoll_n: "w \<in> MM ==> w \<approx> succ(k #+ m)" |
12776 | 519 |
apply (unfold MM_def) |
12960 | 520 |
apply (fast dest: "includes" [THEN subsetD]) |
12776 | 521 |
done |
522 |
||
68847 | 523 |
lemma in_LL_eqpoll_n: "w \<in> LL ==> succ(k) \<lesssim> w" |
12776 | 524 |
by (unfold LL_def MM_def, fast) |
525 |
||
68847 | 526 |
lemma in_LL: "w \<in> LL ==> w \<subseteq> (THE x. x \<in> MM \<and> w \<subseteq> x)" |
12776 | 527 |
by (erule subset_trans [OF in_LL_eq_Int [THEN equalityD1] Int_lower1]) |
528 |
||
68847 | 529 |
lemma all_in_lepoll_m: |
12776 | 530 |
"well_ord(LL,S) ==> |
531 |
\<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m" |
|
532 |
apply (unfold GG_def) |
|
533 |
apply (rule oallI) |
|
534 |
apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type]) |
|
12960 | 535 |
apply (insert "includes") |
12776 | 536 |
apply (rule eqpoll_sum_imp_Diff_lepoll) |
537 |
apply (blast del: subsetI |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
538 |
dest!: ltD |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
539 |
intro!: eqpoll_sum_imp_Diff_lepoll in_LL_eqpoll_n |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
540 |
intro: in_LL unique_superset1 [THEN in_MM_eqpoll_n] |
12776 | 541 |
ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, |
542 |
THEN apply_type])+ |
|
543 |
done |
|
544 |
||
68847 | 545 |
lemma "conclusion": |
12776 | 546 |
"\<exists>a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (\<forall>b<a. f ` b \<lesssim> m)" |
547 |
apply (rule well_ord_LL [THEN exE]) |
|
548 |
apply (rename_tac S) |
|
549 |
apply (rule_tac x = "ordertype (LL,S)" in exI) |
|
550 |
apply (rule_tac x = "\<lambda>b \<in> ordertype(LL,S). |
|
551 |
GG ` (converse (ordermap (LL,S)) ` b)" in exI) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
12960
diff
changeset
|
552 |
apply (simp add: ltD) |
12776 | 553 |
apply (blast intro: lam_funtype [THEN domain_of_fun] |
554 |
Ord_ordertype OUN_eq_x all_in_lepoll_m [THEN ospec]) |
|
555 |
done |
|
556 |
||
68847 | 557 |
end |
558 |
||
12776 | 559 |
|
560 |
(* ********************************************************************** *) |
|
561 |
(* The main theorem AC16(n, k) ==> WO4(n-k) *) |
|
562 |
(* ********************************************************************** *) |
|
563 |
||
564 |
theorem AC16_WO4: |
|
27678 | 565 |
"[| AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)" |
566 |
apply (unfold AC_Equiv.AC16_def WO4_def) |
|
12776 | 567 |
apply (rule allI) |
568 |
apply (case_tac "Finite (A)") |
|
569 |
apply (rule lemma1, assumption+) |
|
570 |
apply (cut_tac lemma2) |
|
571 |
apply (elim exE conjE) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
32960
diff
changeset
|
572 |
apply (erule_tac x = "A \<union> y" in allE) |
12776 | 573 |
apply (frule infinite_Un, drule mp, assumption) |
574 |
apply (erule zero_lt_natE, assumption, clarify) |
|
27678 | 575 |
apply (blast intro: AC16.conclusion [OF AC16.intro]) |
12776 | 576 |
done |
1196 | 577 |
|
578 |
end |