|
1 (* Title : Zorn.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML |
|
5 *) |
|
6 |
|
7 open Zorn; |
|
8 |
|
9 (*--------------------------------------------------------------- |
|
10 Section 1. Mathematical Preamble |
|
11 ---------------------------------------------------------------*) |
|
12 |
|
13 Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"; |
|
14 by (Blast_tac 1); |
|
15 qed "Union_lemma0"; |
|
16 |
|
17 (*-- similar to subset_cs in ZF/subset.thy --*) |
|
18 val thissubset_SIs = |
|
19 [subset_refl,Union_least, UN_least, Un_least, |
|
20 Inter_greatest, Int_greatest, |
|
21 Un_upper1, Un_upper2, Int_lower1, Int_lower2]; |
|
22 |
|
23 |
|
24 (*A claset for subset reasoning*) |
|
25 val thissubset_cs = claset() |
|
26 delrules [subsetI, subsetCE] |
|
27 addSIs thissubset_SIs |
|
28 addIs [Union_upper, Inter_lower]; |
|
29 |
|
30 (* increasingD2 of ZF/Zorn.ML *) |
|
31 Goalw [succ_def] "x <= succ S x"; |
|
32 by (rtac (expand_if RS iffD2) 1); |
|
33 by (auto_tac (claset(),simpset() addsimps [super_def, |
|
34 maxchain_def,psubset_def])); |
|
35 by (rtac swap 1 THEN assume_tac 1); |
|
36 by (rtac selectI2 1); |
|
37 by (ALLGOALS(Blast_tac)); |
|
38 qed "Abrial_axiom1"; |
|
39 |
|
40 val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs; |
|
41 val TFin_UnionI = PowI RS Pow_TFin_UnionI; |
|
42 |
|
43 val major::prems = Goal |
|
44 "[| n : TFin S; \ |
|
45 \ !!x. [| x: TFin S; P(x) |] ==> P(succ S x); \ |
|
46 \ !!Y. [| Y <= TFin S; Ball Y P |] ==> P(Union Y) |] \ |
|
47 \ ==> P(n)"; |
|
48 by (rtac (major RS TFin.induct) 1); |
|
49 by (ALLGOALS (fast_tac (claset() addIs prems))); |
|
50 qed "TFin_induct"; |
|
51 |
|
52 (*Perform induction on n, then prove the major premise using prems. *) |
|
53 fun TFin_ind_tac a prems i = |
|
54 EVERY [res_inst_tac [("n",a)] TFin_induct i, |
|
55 rename_last_tac a ["1"] (i+1), |
|
56 rename_last_tac a ["2"] (i+2), |
|
57 ares_tac prems i]; |
|
58 |
|
59 Goal "x <= y ==> x <= succ S y"; |
|
60 by (etac (Abrial_axiom1 RSN (2,subset_trans)) 1); |
|
61 qed "succ_trans"; |
|
62 |
|
63 (*Lemma 1 of section 3.1*) |
|
64 Goal "[| n: TFin S; m: TFin S; \ |
|
65 \ ALL x: TFin S. x <= m --> x = m | succ S x <= m \ |
|
66 \ |] ==> n <= m | succ S m <= n"; |
|
67 by (etac TFin_induct 1); |
|
68 by (etac Union_lemma0 2); (*or just Blast_tac*) |
|
69 by (blast_tac (thissubset_cs addIs [succ_trans]) 1); |
|
70 qed "TFin_linear_lemma1"; |
|
71 |
|
72 (* Lemma 2 of section 3.2 *) |
|
73 Goal "m: TFin S ==> ALL n: TFin S. n<=m --> n=m | succ S n<=m"; |
|
74 by (etac TFin_induct 1); |
|
75 by (rtac (impI RS ballI) 1); |
|
76 (*case split using TFin_linear_lemma1*) |
|
77 by (res_inst_tac [("n1","n"), ("m1","x")] |
|
78 (TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); |
|
79 by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1); |
|
80 by (blast_tac (thissubset_cs addIs [succ_trans]) 1); |
|
81 by (REPEAT (ares_tac [disjI1,equalityI] 1)); |
|
82 (*second induction step*) |
|
83 by (rtac (impI RS ballI) 1); |
|
84 by (rtac (Union_lemma0 RS disjE) 1); |
|
85 by (rtac disjI2 3); |
|
86 by (REPEAT (ares_tac [disjI1,equalityI] 2)); |
|
87 by (rtac ballI 1); |
|
88 by (ball_tac 1); |
|
89 by (set_mp_tac 1); |
|
90 by (res_inst_tac [("n1","n"), ("m1","x")] |
|
91 (TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); |
|
92 by (blast_tac thissubset_cs 1); |
|
93 by (rtac (Abrial_axiom1 RS subset_trans RS disjI1) 1); |
|
94 by (assume_tac 1); |
|
95 qed "TFin_linear_lemma2"; |
|
96 |
|
97 (*a more convenient form for Lemma 2*) |
|
98 Goal "[| n<=m; m: TFin S; n: TFin S |] ==> n=m | succ S n<=m"; |
|
99 by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1); |
|
100 by (REPEAT (assume_tac 1)); |
|
101 qed "TFin_subsetD"; |
|
102 |
|
103 (*Consequences from section 3.3 -- Property 3.2, the ordering is total*) |
|
104 Goal "[| m: TFin S; n: TFin S|] ==> n<=m | m<=n"; |
|
105 by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1); |
|
106 by (REPEAT (assume_tac 1) THEN etac disjI2 1); |
|
107 by (blast_tac (thissubset_cs addIs [Abrial_axiom1 RS subset_trans]) 1); |
|
108 qed "TFin_subset_linear"; |
|
109 |
|
110 (*Lemma 3 of section 3.3*) |
|
111 Goal "[| n: TFin S; m: TFin S; m = succ S m |] ==> n<=m"; |
|
112 by (etac TFin_induct 1); |
|
113 by (dtac TFin_subsetD 1); |
|
114 by (REPEAT (assume_tac 1)); |
|
115 by (fast_tac (claset() addEs [ssubst]) 1); |
|
116 by (blast_tac (thissubset_cs) 1); |
|
117 qed "eq_succ_upper"; |
|
118 |
|
119 (*Property 3.3 of section 3.3*) |
|
120 Goal "m: TFin S ==> (m = succ S m) = (m = Union(TFin S))"; |
|
121 by (rtac iffI 1); |
|
122 by (rtac (Union_upper RS equalityI) 1); |
|
123 by (rtac (eq_succ_upper RS Union_least) 2); |
|
124 by (REPEAT (assume_tac 1)); |
|
125 by (etac ssubst 1); |
|
126 by (rtac (Abrial_axiom1 RS equalityI) 1); |
|
127 by (blast_tac (thissubset_cs addIs [TFin_UnionI, TFin_succI]) 1); |
|
128 qed "equal_succ_Union"; |
|
129 |
|
130 (*------------------------------------------------------------------------- |
|
131 Section 4. Hausdorff's Theorem: every set contains a maximal chain |
|
132 NB: We assume the partial ordering is <=, the subset relation! |
|
133 -------------------------------------------------------------------------*) |
|
134 |
|
135 Goalw [chain_def] "({} :: 'a set set) : chain S"; |
|
136 by (Auto_tac); |
|
137 qed "empty_set_mem_chain"; |
|
138 |
|
139 Goalw [super_def] "super S c <= chain S"; |
|
140 by (Fast_tac 1); |
|
141 qed "super_subset_chain"; |
|
142 |
|
143 Goalw [maxchain_def] "maxchain S <= chain S"; |
|
144 by (Fast_tac 1); |
|
145 qed "maxchain_subset_chain"; |
|
146 |
|
147 Goalw [succ_def] "c ~: chain S ==> succ S c = c"; |
|
148 by (fast_tac (claset() addSIs [if_P]) 1); |
|
149 qed "succI1"; |
|
150 |
|
151 Goalw [succ_def] "c: maxchain S ==> succ S c = c"; |
|
152 by (fast_tac (claset() addSIs [if_P]) 1); |
|
153 qed "succI2"; |
|
154 |
|
155 Goalw [succ_def] "c: chain S - maxchain S ==> \ |
|
156 \ succ S c = (@c'. c': super S c)"; |
|
157 by (fast_tac (claset() addSIs [if_not_P]) 1); |
|
158 qed "succI3"; |
|
159 |
|
160 Goal "c: chain S - maxchain S ==> ? d. d: super S c"; |
|
161 by (rewrite_goals_tac [super_def,maxchain_def]); |
|
162 by (Auto_tac); |
|
163 qed "mem_super_Ex"; |
|
164 |
|
165 Goal "c: chain S - maxchain S ==> \ |
|
166 \ (@c'. c': super S c): super S c"; |
|
167 by (etac (mem_super_Ex RS exE) 1); |
|
168 by (rtac selectI2 1); |
|
169 by (Auto_tac); |
|
170 qed "select_super"; |
|
171 |
|
172 Goal "c: chain S - maxchain S ==> \ |
|
173 \ (@c'. c': super S c) ~= c"; |
|
174 by (rtac notI 1); |
|
175 by (dtac select_super 1); |
|
176 by (asm_full_simp_tac (simpset() addsimps [super_def,psubset_def]) 1); |
|
177 qed "select_not_equals"; |
|
178 |
|
179 Goal "c: chain S - maxchain S ==> \ |
|
180 \ succ S c ~= c"; |
|
181 by (forward_tac [succI3] 1); |
|
182 by (Asm_simp_tac 1); |
|
183 by (rtac select_not_equals 1); |
|
184 by (assume_tac 1); |
|
185 qed "succ_not_equals"; |
|
186 |
|
187 Goal "c: TFin S ==> (c :: 'a set set): chain S"; |
|
188 by (etac TFin_induct 1); |
|
189 by (asm_simp_tac (simpset() addsimps [succ_def, |
|
190 select_super RS (super_subset_chain RS subsetD)] |
|
191 setloop split_tac [expand_if]) 1); |
|
192 by (rewtac chain_def); |
|
193 by (rtac CollectI 1); |
|
194 by (safe_tac(claset())); |
|
195 by (dtac bspec 1 THEN assume_tac 1); |
|
196 by (res_inst_tac [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2); |
|
197 by (ALLGOALS(Blast_tac)); |
|
198 qed "TFin_chain_lemm4"; |
|
199 |
|
200 Goal "EX c. (c :: 'a set set): maxchain S"; |
|
201 by (res_inst_tac [("x", "Union(TFin S)")] exI 1); |
|
202 by (rtac classical 1); |
|
203 by (subgoal_tac "succ S (Union(TFin S)) = Union(TFin S)" 1); |
|
204 by (resolve_tac [equal_succ_Union RS iffD2 RS sym] 2); |
|
205 by (resolve_tac [subset_refl RS TFin_UnionI] 2); |
|
206 by (rtac refl 2); |
|
207 by (cut_facts_tac [subset_refl RS TFin_UnionI RS TFin_chain_lemm4] 1); |
|
208 by (dtac (DiffI RS succ_not_equals) 1); |
|
209 by (ALLGOALS(Blast_tac)); |
|
210 qed "Hausdorff"; |
|
211 |
|
212 |
|
213 (*--------------------------------------------------------------- |
|
214 Section 5. Zorn's Lemma: if all chains have upper bounds |
|
215 there is a maximal element |
|
216 ----------------------------------------------------------------*) |
|
217 Goalw [chain_def] |
|
218 "[| c: chain S; z: S; \ |
|
219 \ ALL x:c. x<=(z:: 'a set) |] ==> {z} Un c : chain S"; |
|
220 by (Blast_tac 1); |
|
221 qed "chain_extend"; |
|
222 |
|
223 Goalw [chain_def] "[| c: chain S; x: c |] ==> x <= Union(c)"; |
|
224 by (Auto_tac); |
|
225 qed "chain_Union_upper"; |
|
226 |
|
227 Goalw [chain_def] "c: chain S ==> ! x: c. x <= Union(c)"; |
|
228 by (Auto_tac); |
|
229 qed "chain_ball_Union_upper"; |
|
230 |
|
231 Goal "[| c: maxchain S; u: S; Union(c) <= u |] ==> Union(c) = u"; |
|
232 by (rtac ccontr 1); |
|
233 by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1); |
|
234 by (etac conjE 1); |
|
235 by (subgoal_tac "({u} Un c): super S c" 1); |
|
236 by (Asm_full_simp_tac 1); |
|
237 by (rewrite_tac [super_def,psubset_def]); |
|
238 by (safe_tac (claset())); |
|
239 by (fast_tac (claset() addEs [chain_extend]) 1); |
|
240 by (subgoal_tac "u ~: c" 1); |
|
241 by (blast_tac (claset() addEs [equalityE]) 1); |
|
242 by (blast_tac (claset() addDs [chain_Union_upper]) 1); |
|
243 qed "maxchain_Zorn"; |
|
244 |
|
245 Goal "ALL c: chain S. Union(c): S ==> \ |
|
246 \ EX y: S. ALL z: S. y <= z --> y = z"; |
|
247 by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1); |
|
248 by (etac exE 1); |
|
249 by (dtac subsetD 1 THEN assume_tac 1); |
|
250 by (dtac bspec 1 THEN assume_tac 1); |
|
251 by (res_inst_tac [("x","Union(c)")] bexI 1); |
|
252 by (rtac ballI 1 THEN rtac impI 1); |
|
253 by (blast_tac (claset() addSDs [maxchain_Zorn]) 1); |
|
254 by (assume_tac 1); |
|
255 qed "Zorn_Lemma"; |
|
256 |
|
257 (*------------------------------------------------------------- |
|
258 Alternative version of Zorn's Lemma |
|
259 --------------------------------------------------------------*) |
|
260 Goal "ALL (c:: 'a set set): chain S. EX y : S. ALL x : c. x <= y ==> \ |
|
261 \ EX y : S. ALL x : S. (y :: 'a set) <= x --> y = x"; |
|
262 by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1); |
|
263 by (EVERY1[etac exE, dtac subsetD, assume_tac]); |
|
264 by (EVERY1[dtac bspec, assume_tac, etac bexE]); |
|
265 by (res_inst_tac [("x","y")] bexI 1); |
|
266 by (assume_tac 2); |
|
267 by (EVERY1[rtac ballI, rtac impI, rtac ccontr]); |
|
268 by (forw_inst_tac [("z","x")] chain_extend 1); |
|
269 by (assume_tac 1 THEN Blast_tac 1); |
|
270 by (rewrite_tac [maxchain_def,super_def,psubset_def]); |
|
271 by (Step_tac 1); |
|
272 by (eres_inst_tac [("c","{x} Un c")] equalityCE 1); |
|
273 by (Step_tac 1); |
|
274 by (subgoal_tac "x ~: c" 1); |
|
275 by (blast_tac (claset() addEs [equalityE]) 1); |
|
276 by (Blast_tac 1); |
|
277 qed "Zorn_Lemma2"; |
|
278 |
|
279 (** misc. lemmas **) |
|
280 |
|
281 Goalw [chain_def] "[| c : chain S; x: c; y: c |] ==> x <= y | y <= x"; |
|
282 by (Blast_tac 1); |
|
283 qed "chainD"; |
|
284 |
|
285 Goalw [chain_def] "!!(c :: 'a set set). c: chain S ==> c <= S"; |
|
286 by (Blast_tac 1); |
|
287 qed "chainD2"; |
|
288 |
|
289 (* proved elsewhere? *) |
|
290 Goal "x : Union(c) ==> EX m:c. x:m"; |
|
291 by (Blast_tac 1); |
|
292 qed "mem_UnionD"; |
|
293 |