author | paulson |
Fri, 23 Mar 2012 16:16:15 +0000 | |
changeset 47101 | ded5cc757bc9 |
parent 46822 | 95f1e700b712 |
child 60770 | 240563fbf41d |
permissions | -rw-r--r-- |
12776 | 1 |
(* Title: ZF/AC/Cardinal_aux.thy |
2 |
Author: Krzysztof Grabczewski |
|
3 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
4 |
Auxiliary lemmas concerning cardinalities. |
12776 | 5 |
*) |
6 |
||
16417 | 7 |
theory Cardinal_aux imports AC_Equiv begin |
12776 | 8 |
|
9 |
lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m" |
|
12820 | 10 |
apply (rule not_emptyE, assumption) |
12776 | 11 |
apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll]) |
12 |
done |
|
13 |
||
14 |
||
15 |
(* ********************************************************************** *) |
|
16 |
(* Lemmas involving ordinals and cardinalities used in the proofs *) |
|
17 |
(* concerning AC16 and DC *) |
|
18 |
(* ********************************************************************** *) |
|
19 |
||
20 |
||
21 |
(* j=|A| *) |
|
22 |
lemma lepoll_imp_ex_le_eqpoll: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
23 |
"[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j \<le> i & A \<approx> j" |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
24 |
by (blast intro!: lepoll_cardinal_le well_ord_Memrel |
12776 | 25 |
well_ord_cardinal_eqpoll [THEN eqpoll_sym] |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12820
diff
changeset
|
26 |
dest: lepoll_well_ord) |
12776 | 27 |
|
28 |
(* j=|A| *) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
29 |
lemma lesspoll_imp_ex_lt_eqpoll: |
12776 | 30 |
"[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j" |
31 |
by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE) |
|
32 |
||
33 |
lemma Un_eqpoll_Inf_Ord: |
|
47101 | 34 |
assumes A: "A \<approx> i" and B: "B \<approx> i" and NFI: "\<not> Finite(i)" and i: "Ord(i)" |
35 |
shows "A \<union> B \<approx> i" |
|
36 |
proof (rule eqpollI) |
|
37 |
have AB: "A \<approx> B" using A B by (blast intro: eqpoll_sym eqpoll_trans) |
|
38 |
have "2 \<lesssim> nat" |
|
39 |
by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat]) |
|
40 |
also have "... \<lesssim> i" |
|
41 |
by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+ |
|
42 |
also have "... \<approx> A" by (blast intro: eqpoll_sym A) |
|
43 |
finally have "2 \<lesssim> A" . |
|
44 |
have ICI: "InfCard(|i|)" |
|
45 |
by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i) |
|
46 |
have "A \<union> B \<lesssim> A + B" by (rule Un_lepoll_sum) |
|
47 |
also have "... \<lesssim> A \<times> B" |
|
48 |
by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] `2 \<lesssim> A`]) |
|
49 |
also have "... \<approx> i \<times> i" |
|
50 |
by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B) |
|
51 |
also have "... \<approx> i" |
|
52 |
by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i) |
|
53 |
finally show "A \<union> B \<lesssim> i" . |
|
54 |
next |
|
55 |
have "i \<approx> A" by (blast intro: A eqpoll_sym) |
|
56 |
also have "... \<lesssim> A \<union> B" by (blast intro: subset_imp_lepoll) |
|
57 |
finally show "i \<lesssim> A \<union> B" . |
|
58 |
qed |
|
12776 | 59 |
|
36319 | 60 |
schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)" |
12776 | 61 |
apply (rule RepFun_bijective) |
62 |
apply (simp add: doubleton_eq_iff, blast) |
|
63 |
done |
|
64 |
||
65 |
lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x" |
|
66 |
by (unfold eqpoll_def, fast intro!: paired_bij) |
|
67 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
68 |
lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0" |
12776 | 69 |
by (fast intro!: paired_eqpoll equals0I elim: mem_asym) |
70 |
||
47101 | 71 |
(*Finally we reach this result. Surely there's a simpler proof?*) |
12776 | 72 |
lemma Un_lepoll_Inf_Ord: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
73 |
"[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12820
diff
changeset
|
74 |
apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE]) |
12776 | 75 |
apply (erule conjE) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
76 |
apply (drule lepoll_trans) |
12776 | 77 |
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) |
78 |
apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+)) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
79 |
apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll) |
12776 | 80 |
done |
81 |
||
82 |
lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (LEAST i. P(i)) \<in> j" |
|
83 |
apply (erule Least_le [THEN leE]) |
|
84 |
apply (erule Ord_in_Ord, assumption) |
|
85 |
apply (erule ltE) |
|
86 |
apply (fast dest: OrdmemD) |
|
87 |
apply (erule subst_elem, assumption) |
|
88 |
done |
|
1196 | 89 |
|
12776 | 90 |
lemma Diff_first_lepoll: |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
91 |
"[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |] |
12776 | 92 |
==> y - {THE b. first(b,y,r)} \<lesssim> n" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
93 |
apply (case_tac "y=0", simp add: empty_lepollI) |
12776 | 94 |
apply (fast intro!: Diff_sing_lepoll the_first_in) |
95 |
done |
|
96 |
||
97 |
lemma UN_subset_split: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
98 |
"(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) \<union> (\<Union>x \<in> X. Q(x))" |
12776 | 99 |
by blast |
100 |
||
101 |
lemma UN_sing_lepoll: "Ord(a) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a" |
|
102 |
apply (unfold lepoll_def) |
|
103 |
apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (LEAST i. P (i) =z) " in exI) |
|
104 |
apply (rule_tac d = "%z. P (z) " in lam_injective) |
|
105 |
apply (fast intro!: Least_in_Ord) |
|
106 |
apply (fast intro: LeastI elim!: Ord_in_Ord) |
|
107 |
done |
|
108 |
||
109 |
lemma UN_fun_lepoll_lemma [rule_format]: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
110 |
"[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |] |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
111 |
==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) \<longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a" |
12776 | 112 |
apply (induct_tac "n") |
113 |
apply (rule allI) |
|
114 |
apply (rule impI) |
|
115 |
apply (rule_tac b = "\<Union>b \<in> a. f`b" in subst) |
|
116 |
apply (rule_tac [2] empty_lepollI) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
117 |
apply (rule equals0I [symmetric], clarify) |
12776 | 118 |
apply (fast dest: lepoll_0_is_0 [THEN subst]) |
119 |
apply (rule allI) |
|
120 |
apply (rule impI) |
|
121 |
apply (erule_tac x = "\<lambda>x \<in> a. f`x - {THE b. first (b,f`x,R) }" in allE) |
|
122 |
apply (erule impE, simp) |
|
123 |
apply (fast intro!: Diff_first_lepoll, simp) |
|
124 |
apply (rule UN_subset_split [THEN subset_imp_lepoll, THEN lepoll_trans]) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
125 |
apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll) |
12776 | 126 |
done |
127 |
||
128 |
lemma UN_fun_lepoll: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
129 |
"[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R); |
12776 | 130 |
~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
131 |
by (blast intro: UN_fun_lepoll_lemma) |
12776 | 132 |
|
133 |
lemma UN_lepoll: |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
134 |
"[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R); |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
135 |
~Finite(a); Ord(a); n \<in> nat |] |
12776 | 136 |
==> (\<Union>b \<in> a. F(b)) \<lesssim> a" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
137 |
apply (rule rev_mp) |
12820 | 138 |
apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll) |
12776 | 139 |
apply auto |
140 |
done |
|
141 |
||
142 |
lemma UN_eq_UN_Diffs: |
|
143 |
"Ord(a) ==> (\<Union>b \<in> a. F(b)) = (\<Union>b \<in> a. F(b) - (\<Union>c \<in> b. F(c)))" |
|
144 |
apply (rule equalityI) |
|
145 |
prefer 2 apply fast |
|
146 |
apply (rule subsetI) |
|
147 |
apply (erule UN_E) |
|
148 |
apply (rule UN_I) |
|
149 |
apply (rule_tac P = "%z. x \<in> F (z) " in Least_in_Ord, (assumption+)) |
|
150 |
apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12820
diff
changeset
|
151 |
apply (erule_tac P = "%z. x \<in> F (z) " and i = c in less_LeastE) |
12776 | 152 |
apply (blast intro: Ord_Least ltI) |
153 |
done |
|
154 |
||
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
155 |
lemma lepoll_imp_eqpoll_subset: |
12776 | 156 |
"a \<lesssim> X ==> \<exists>Y. Y \<subseteq> X & a \<approx> Y" |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
157 |
apply (unfold lepoll_def eqpoll_def, clarify) |
12776 | 158 |
apply (blast intro: restrict_bij |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
159 |
dest: inj_is_fun [THEN fun_is_rel, THEN image_subset]) |
12776 | 160 |
done |
161 |
||
162 |
(* ********************************************************************** *) |
|
163 |
(* Diff_lesspoll_eqpoll_Card *) |
|
164 |
(* ********************************************************************** *) |
|
165 |
||
166 |
lemma Diff_lesspoll_eqpoll_Card_lemma: |
|
167 |
"[| A\<approx>a; ~Finite(a); Card(a); B \<prec> a; A-B \<prec> a |] ==> P" |
|
168 |
apply (elim lesspoll_imp_ex_lt_eqpoll [THEN exE] Card_is_Ord conjE) |
|
169 |
apply (frule_tac j=xa in Un_upper1_le [OF lt_Ord lt_Ord], assumption) |
|
170 |
apply (frule_tac j=xa in Un_upper2_le [OF lt_Ord lt_Ord], assumption) |
|
171 |
apply (drule Un_least_lt, assumption) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
172 |
apply (drule eqpoll_imp_lepoll [THEN lepoll_trans], |
12776 | 173 |
rule le_imp_lepoll, assumption)+ |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
174 |
apply (case_tac "Finite(x \<union> xa)") |
12776 | 175 |
txt{*finite case*} |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
176 |
apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+) |
12776 | 177 |
apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite]) |
178 |
apply (fast dest: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_Finite]) |
|
179 |
txt{*infinite case*} |
|
180 |
apply (drule Un_lepoll_Inf_Ord, (assumption+)) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
181 |
apply (blast intro: le_Ord2) |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
182 |
apply (drule lesspoll_trans1 |
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
183 |
[OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans] |
12776 | 184 |
lt_Card_imp_lesspoll], assumption+) |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
185 |
apply (simp add: lesspoll_def) |
12776 | 186 |
done |
187 |
||
188 |
lemma Diff_lesspoll_eqpoll_Card: |
|
189 |
"[| A \<approx> a; ~Finite(a); Card(a); B \<prec> a |] ==> A - B \<approx> a" |
|
190 |
apply (rule ccontr) |
|
191 |
apply (rule Diff_lesspoll_eqpoll_Card_lemma, (assumption+)) |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
36319
diff
changeset
|
192 |
apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2] |
12776 | 193 |
subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans) |
194 |
done |
|
195 |
||
196 |
end |