author | nipkow |
Sat, 08 Aug 2020 18:20:09 +0200 | |
changeset 72122 | 2dcb6523f6af |
parent 61980 | 6b780867d426 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/AC/HH.thy |
2 |
Author: Krzysztof Grabczewski |
|
1123 | 3 |
|
12776 | 4 |
Some properties of the recursive definition of HH used in the proofs of |
1123 | 5 |
AC17 ==> AC1 |
6 |
AC1 ==> WO2 |
|
7 |
AC15 ==> WO6 |
|
8 |
*) |
|
9 |
||
27678 | 10 |
theory HH |
11 |
imports AC_Equiv Hartog |
|
12 |
begin |
|
1123 | 13 |
|
24894 | 14 |
definition |
15 |
HH :: "[i, i, i] => i" where |
|
12776 | 16 |
"HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c) |
17 |
in if f`z \<in> Pow(z)-{0} then f`z else {x})" |
|
18 |
||
60770 | 19 |
subsection\<open>Lemmas useful in each of the three proofs\<close> |
12776 | 20 |
|
21 |
lemma HH_def_satisfies_eq: |
|
22 |
"HH(f,x,a) = (let z = x - (\<Union>b \<in> a. HH(f,x,b)) |
|
23 |
in if f`z \<in> Pow(z)-{0} then f`z else {x})" |
|
24 |
by (rule HH_def [THEN def_transrec, THEN trans], simp) |
|
25 |
||
26 |
lemma HH_values: "HH(f,x,a) \<in> Pow(x)-{0} | HH(f,x,a)={x}" |
|
27 |
apply (rule HH_def_satisfies_eq [THEN ssubst]) |
|
28 |
apply (simp add: Let_def Diff_subset [THEN PowI], fast) |
|
29 |
done |
|
30 |
||
31 |
lemma subset_imp_Diff_eq: |
|
32 |
"B \<subseteq> A ==> X-(\<Union>a \<in> A. P(a)) = X-(\<Union>a \<in> A-B. P(a))-(\<Union>b \<in> B. P(b))" |
|
33 |
by fast |
|
34 |
||
35 |
lemma Ord_DiffE: "[| c \<in> a-b; b<a |] ==> c=b | b<c & c<a" |
|
36 |
apply (erule ltE) |
|
37 |
apply (drule Ord_linear [of _ c]) |
|
38 |
apply (fast elim: Ord_in_Ord) |
|
39 |
apply (fast intro!: ltI intro: Ord_in_Ord) |
|
40 |
done |
|
41 |
||
15481 | 42 |
lemma Diff_UN_eq_self: "(!!y. y\<in>A ==> P(y) = {x}) ==> x - (\<Union>y \<in> A. P(y)) = x" |
43 |
by (simp, fast elim!: mem_irrefl) |
|
12776 | 44 |
|
45 |
lemma HH_eq: "x - (\<Union>b \<in> a. HH(f,x,b)) = x - (\<Union>b \<in> a1. HH(f,x,b)) |
|
46 |
==> HH(f,x,a) = HH(f,x,a1)" |
|
15481 | 47 |
apply (subst HH_def_satisfies_eq [of _ _ a1]) |
12776 | 48 |
apply (rule HH_def_satisfies_eq [THEN trans], simp) |
49 |
done |
|
50 |
||
51 |
lemma HH_is_x_gt_too: "[| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}" |
|
52 |
apply (rule_tac P = "b<a" in impE) |
|
53 |
prefer 2 apply assumption+ |
|
54 |
apply (erule lt_Ord2 [THEN trans_induct]) |
|
55 |
apply (rule impI) |
|
56 |
apply (rule HH_eq [THEN trans]) |
|
57 |
prefer 2 apply assumption+ |
|
58 |
apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst], |
|
59 |
assumption) |
|
59788 | 60 |
apply (rule_tac t = "%z. z-X" for X in subst_context) |
12776 | 61 |
apply (rule Diff_UN_eq_self) |
62 |
apply (drule Ord_DiffE, assumption) |
|
63 |
apply (fast elim: ltE, auto) |
|
64 |
done |
|
65 |
||
66 |
lemma HH_subset_x_lt_too: |
|
67 |
"[| HH(f,x,a) \<in> Pow(x)-{0}; b<a |] ==> HH(f,x,b) \<in> Pow(x)-{0}" |
|
68 |
apply (rule HH_values [THEN disjE], assumption) |
|
69 |
apply (drule HH_is_x_gt_too, assumption) |
|
70 |
apply (drule subst, assumption) |
|
71 |
apply (fast elim!: mem_irrefl) |
|
72 |
done |
|
73 |
||
74 |
lemma HH_subset_x_imp_subset_Diff_UN: |
|
75 |
"HH(f,x,a) \<in> Pow(x)-{0} ==> HH(f,x,a) \<in> Pow(x - (\<Union>b \<in> a. HH(f,x,b)))-{0}" |
|
76 |
apply (drule HH_def_satisfies_eq [THEN subst]) |
|
77 |
apply (rule HH_def_satisfies_eq [THEN ssubst]) |
|
78 |
apply (simp add: Let_def Diff_subset [THEN PowI]) |
|
79 |
apply (drule split_if [THEN iffD1]) |
|
80 |
apply (fast elim!: mem_irrefl) |
|
81 |
done |
|
82 |
||
83 |
lemma HH_eq_arg_lt: |
|
84 |
"[| HH(f,x,v)=HH(f,x,w); HH(f,x,v) \<in> Pow(x)-{0}; v \<in> w |] ==> P" |
|
85 |
apply (frule_tac P = "%y. y \<in> Pow (x) -{0}" in subst, assumption) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12820
diff
changeset
|
86 |
apply (drule_tac a = w in HH_subset_x_imp_subset_Diff_UN) |
12776 | 87 |
apply (drule subst_elem, assumption) |
88 |
apply (fast intro!: singleton_iff [THEN iffD2] equals0I) |
|
89 |
done |
|
90 |
||
91 |
lemma HH_eq_imp_arg_eq: |
|
92 |
"[| HH(f,x,v)=HH(f,x,w); HH(f,x,w) \<in> Pow(x)-{0}; Ord(v); Ord(w) |] ==> v=w" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12820
diff
changeset
|
93 |
apply (rule_tac j = w in Ord_linear_lt) |
12776 | 94 |
apply (simp_all (no_asm_simp)) |
95 |
apply (drule subst_elem, assumption) |
|
96 |
apply (blast dest: ltD HH_eq_arg_lt) |
|
97 |
apply (blast dest: HH_eq_arg_lt [OF sym] ltD) |
|
98 |
done |
|
99 |
||
100 |
lemma HH_subset_x_imp_lepoll: |
|
46954 | 101 |
"[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i \<lesssim> Pow(x)-{0}" |
12776 | 102 |
apply (unfold lepoll_def inj_def) |
103 |
apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI) |
|
104 |
apply (simp (no_asm_simp)) |
|
105 |
apply (fast del: DiffE |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
106 |
elim!: HH_eq_imp_arg_eq Ord_in_Ord HH_subset_x_lt_too |
12776 | 107 |
intro!: lam_type ballI ltI intro: bexI) |
108 |
done |
|
109 |
||
110 |
lemma HH_Hartog_is_x: "HH(f, x, Hartog(Pow(x)-{0})) = {x}" |
|
111 |
apply (rule HH_values [THEN disjE]) |
|
112 |
prefer 2 apply assumption |
|
113 |
apply (fast del: DiffE |
|
114 |
intro!: Ord_Hartog |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
115 |
dest!: HH_subset_x_imp_lepoll |
12776 | 116 |
elim!: Hartog_lepoll_selfE) |
117 |
done |
|
118 |
||
61394 | 119 |
lemma HH_Least_eq_x: "HH(f, x, \<mu> i. HH(f, x, i) = {x}) = {x}" |
12776 | 120 |
by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI) |
121 |
||
122 |
lemma less_Least_subset_x: |
|
61394 | 123 |
"a \<in> (\<mu> i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> Pow(x)-{0}" |
12776 | 124 |
apply (rule HH_values [THEN disjE], assumption) |
125 |
apply (rule less_LeastE) |
|
126 |
apply (erule_tac [2] ltI [OF _ Ord_Least], assumption) |
|
127 |
done |
|
1123 | 128 |
|
60770 | 129 |
subsection\<open>Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\<close> |
12776 | 130 |
|
131 |
lemma lam_Least_HH_inj_Pow: |
|
61394 | 132 |
"(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a)) |
133 |
\<in> inj(\<mu> i. HH(f,x,i)={x}, Pow(x)-{0})" |
|
12776 | 134 |
apply (unfold inj_def, simp) |
135 |
apply (fast intro!: lam_type dest: less_Least_subset_x |
|
136 |
elim!: HH_eq_imp_arg_eq Ord_Least [THEN Ord_in_Ord]) |
|
137 |
done |
|
138 |
||
139 |
lemma lam_Least_HH_inj: |
|
61394 | 140 |
"\<forall>a \<in> (\<mu> i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z} |
141 |
==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a)) |
|
142 |
\<in> inj(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})" |
|
12776 | 143 |
by (rule lam_Least_HH_inj_Pow [THEN inj_strengthen_type], simp) |
144 |
||
145 |
lemma lam_surj_sing: |
|
146 |
"[| x - (\<Union>a \<in> A. F(a)) = 0; \<forall>a \<in> A. \<exists>z \<in> x. F(a) = {z} |] |
|
147 |
==> (\<lambda>a \<in> A. F(a)) \<in> surj(A, {{y}. y \<in> x})" |
|
148 |
apply (simp add: surj_def lam_type Diff_eq_0_iff) |
|
149 |
apply (blast elim: equalityE) |
|
150 |
done |
|
151 |
||
152 |
lemma not_emptyI2: "y \<in> Pow(x)-{0} ==> x \<noteq> 0" |
|
153 |
by auto |
|
154 |
||
155 |
lemma f_subset_imp_HH_subset: |
|
156 |
"f`(x - (\<Union>j \<in> i. HH(f,x,j))) \<in> Pow(x - (\<Union>j \<in> i. HH(f,x,j)))-{0} |
|
157 |
==> HH(f, x, i) \<in> Pow(x) - {0}" |
|
158 |
apply (rule HH_def_satisfies_eq [THEN ssubst]) |
|
159 |
apply (simp add: Let_def Diff_subset [THEN PowI] not_emptyI2 [THEN if_P], fast) |
|
160 |
done |
|
161 |
||
162 |
lemma f_subsets_imp_UN_HH_eq_x: |
|
163 |
"\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0} |
|
61394 | 164 |
==> x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0" |
59788 | 165 |
apply (case_tac "P \<in> {0}" for P, fast) |
12776 | 166 |
apply (drule Diff_subset [THEN PowI, THEN DiffI]) |
167 |
apply (drule bspec, assumption) |
|
168 |
apply (drule f_subset_imp_HH_subset) |
|
169 |
apply (blast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]] |
|
170 |
elim!: mem_irrefl) |
|
171 |
done |
|
172 |
||
173 |
lemma HH_values2: "HH(f,x,i) = f`(x - (\<Union>j \<in> i. HH(f,x,j))) | HH(f,x,i)={x}" |
|
174 |
apply (rule HH_def_satisfies_eq [THEN ssubst]) |
|
175 |
apply (simp add: Let_def Diff_subset [THEN PowI]) |
|
176 |
done |
|
177 |
||
178 |
lemma HH_subset_imp_eq: |
|
179 |
"HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (\<Union>j \<in> i. HH(f,x,j)))" |
|
180 |
apply (rule HH_values2 [THEN disjE], assumption) |
|
181 |
apply (fast elim!: equalityE mem_irrefl dest!: singleton_subsetD) |
|
182 |
done |
|
1123 | 183 |
|
12776 | 184 |
lemma f_sing_imp_HH_sing: |
185 |
"[| f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x}; |
|
61394 | 186 |
a \<in> (\<mu> i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> x. HH(f,x,a) = {z}" |
12776 | 187 |
apply (drule less_Least_subset_x) |
188 |
apply (frule HH_subset_imp_eq) |
|
189 |
apply (drule apply_type) |
|
190 |
apply (rule Diff_subset [THEN PowI, THEN DiffI]) |
|
191 |
apply (fast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2], force) |
|
192 |
done |
|
193 |
||
194 |
lemma f_sing_lam_bij: |
|
61394 | 195 |
"[| x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0; |
12776 | 196 |
f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x} |] |
61394 | 197 |
==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a)) |
198 |
\<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})" |
|
12776 | 199 |
apply (unfold bij_def) |
200 |
apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing) |
|
201 |
done |
|
202 |
||
203 |
lemma lam_singI: |
|
61980 | 204 |
"f \<in> (\<Prod>X \<in> Pow(x)-{0}. F(X)) |
205 |
==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Prod>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})" |
|
12776 | 206 |
by (fast del: DiffI DiffE |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27678
diff
changeset
|
207 |
intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type) |
12776 | 208 |
|
209 |
(*FIXME: both uses have the form ...[THEN bij_converse_bij], so |
|
210 |
simplification is needed!*) |
|
211 |
lemmas bij_Least_HH_x = |
|
212 |
comp_bij [OF f_sing_lam_bij [OF _ lam_singI] |
|
45602 | 213 |
lam_sing_bij [THEN bij_converse_bij]] |
12776 | 214 |
|
215 |
||
60770 | 216 |
subsection\<open>The proof of AC1 ==> WO2\<close> |
12776 | 217 |
|
218 |
(*Establishing the existence of a bijection, namely |
|
219 |
converse |
|
220 |
(converse(\<lambda>x\<in>x. {x}) O |
|
221 |
Lambda |
|
61394 | 222 |
(\<mu> i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x}, |
12776 | 223 |
HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x))) |
224 |
Perhaps it could be simplified. *) |
|
225 |
||
226 |
lemma bijection: |
|
61980 | 227 |
"f \<in> (\<Prod>X \<in> Pow(x) - {0}. X) |
61394 | 228 |
==> \<exists>g. g \<in> bij(x, \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})" |
12776 | 229 |
apply (rule exI) |
230 |
apply (rule bij_Least_HH_x [THEN bij_converse_bij]) |
|
231 |
apply (rule f_subsets_imp_UN_HH_eq_x) |
|
232 |
apply (intro ballI apply_type) |
|
12820 | 233 |
apply (fast intro: lam_type apply_type del: DiffE, assumption) |
12776 | 234 |
apply (fast intro: Pi_weaken_type) |
235 |
done |
|
236 |
||
237 |
lemma AC1_WO2: "AC1 ==> WO2" |
|
238 |
apply (unfold AC1_def WO2_def eqpoll_def) |
|
239 |
apply (intro allI) |
|
240 |
apply (drule_tac x = "Pow(A) - {0}" in spec) |
|
241 |
apply (blast dest: bijection) |
|
242 |
done |
|
1123 | 243 |
|
244 |
end |
|
245 |