|
1 (* Title: HOL/ZF/HOLZF.thy |
|
2 ID: $Id$ |
|
3 Author: Steven Obua |
|
4 |
|
5 Axiomatizes the ZFC universe as an HOL type. |
|
6 See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
|
7 *) |
|
8 |
|
9 theory HOLZF |
|
10 imports Helper |
|
11 begin |
|
12 |
|
13 typedecl ZF |
|
14 |
|
15 consts |
|
16 Empty :: ZF |
|
17 Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" |
|
18 Sum :: "ZF \<Rightarrow> ZF" |
|
19 Power :: "ZF \<Rightarrow> ZF" |
|
20 Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF" |
|
21 Inf :: ZF |
|
22 |
|
23 constdefs |
|
24 Upair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
25 "Upair a b == Repl (Power (Power Empty)) (% x. if x = Empty then a else b)" |
|
26 Singleton:: "ZF \<Rightarrow> ZF" |
|
27 "Singleton x == Upair x x" |
|
28 union :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
29 "union A B == Sum (Upair A B)" |
|
30 SucNat:: "ZF \<Rightarrow> ZF" |
|
31 "SucNat x == union x (Singleton x)" |
|
32 subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" |
|
33 "subset A B == ! x. Elem x A \<longrightarrow> Elem x B" |
|
34 |
|
35 finalconsts |
|
36 Empty Elem Sum Power Repl Inf |
|
37 |
|
38 axioms |
|
39 Empty: "Not (Elem x Empty)" |
|
40 Ext: "(x = y) = (! z. Elem z x = Elem z y)" |
|
41 Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)" |
|
42 Power: "Elem y (Power x) = (subset y x)" |
|
43 Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)" |
|
44 Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))" |
|
45 Infinity: "Elem Empty Inf & (! x. Elem x Inf \<longrightarrow> Elem (SucNat x) Inf)" |
|
46 |
|
47 constdefs |
|
48 Sep:: "ZF \<Rightarrow> (ZF \<Rightarrow> bool) \<Rightarrow> ZF" |
|
49 "Sep A p == (if (!x. Elem x A \<longrightarrow> Not (p x)) then Empty else |
|
50 (let z = (\<some> x. Elem x A & p x) in |
|
51 let f = % x. (if p x then x else z) in Repl A f))" |
|
52 |
|
53 thm Power[unfolded subset_def] |
|
54 |
|
55 theorem Sep: "Elem b (Sep A p) = (Elem b A & p b)" |
|
56 apply (auto simp add: Sep_def Empty) |
|
57 apply (auto simp add: Let_def Repl) |
|
58 apply (rule someI2, auto)+ |
|
59 done |
|
60 |
|
61 lemma subset_empty: "subset Empty A" |
|
62 by (simp add: subset_def Empty) |
|
63 |
|
64 theorem Upair: "Elem x (Upair a b) = (x = a | x = b)" |
|
65 apply (auto simp add: Upair_def Repl) |
|
66 apply (rule exI[where x=Empty]) |
|
67 apply (simp add: Power subset_empty) |
|
68 apply (rule exI[where x="Power Empty"]) |
|
69 apply (auto) |
|
70 apply (auto simp add: Ext Power subset_def Empty) |
|
71 apply (drule spec[where x=Empty], simp add: Empty)+ |
|
72 done |
|
73 |
|
74 lemma Singleton: "Elem x (Singleton y) = (x = y)" |
|
75 by (simp add: Singleton_def Upair) |
|
76 |
|
77 constdefs |
|
78 Opair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
79 "Opair a b == Upair (Upair a a) (Upair a b)" |
|
80 |
|
81 lemma Upair_singleton: "(Upair a a = Upair c d) = (a = c & a = d)" |
|
82 by (auto simp add: Ext[where x="Upair a a"] Upair) |
|
83 |
|
84 lemma Upair_fsteq: "(Upair a b = Upair a c) = ((a = b & a = c) | (b = c))" |
|
85 by (auto simp add: Ext[where x="Upair a b"] Upair) |
|
86 |
|
87 lemma Upair_comm: "Upair a b = Upair b a" |
|
88 by (auto simp add: Ext Upair) |
|
89 |
|
90 theorem Opair: "(Opair a b = Opair c d) = (a = c & b = d)" |
|
91 proof - |
|
92 have fst: "(Opair a b = Opair c d) \<Longrightarrow> a = c" |
|
93 apply (simp add: Opair_def) |
|
94 apply (simp add: Ext[where x="Upair (Upair a a) (Upair a b)"]) |
|
95 apply (drule spec[where x="Upair a a"]) |
|
96 apply (auto simp add: Upair Upair_singleton) |
|
97 done |
|
98 show ?thesis |
|
99 apply (auto) |
|
100 apply (erule fst) |
|
101 apply (frule fst) |
|
102 apply (auto simp add: Opair_def Upair_fsteq) |
|
103 done |
|
104 qed |
|
105 |
|
106 constdefs |
|
107 Replacement :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF option) \<Rightarrow> ZF" |
|
108 "Replacement A f == Repl (Sep A (% a. f a \<noteq> None)) (the o f)" |
|
109 |
|
110 theorem Replacement: "Elem y (Replacement A f) = (? x. Elem x A & f x = Some y)" |
|
111 by (auto simp add: Replacement_def Repl Sep) |
|
112 |
|
113 constdefs |
|
114 Fst :: "ZF \<Rightarrow> ZF" |
|
115 "Fst q == SOME x. ? y. q = Opair x y" |
|
116 Snd :: "ZF \<Rightarrow> ZF" |
|
117 "Snd q == SOME y. ? x. q = Opair x y" |
|
118 |
|
119 theorem Fst: "Fst (Opair x y) = x" |
|
120 apply (simp add: Fst_def) |
|
121 apply (rule someI2) |
|
122 apply (simp_all add: Opair) |
|
123 done |
|
124 |
|
125 theorem Snd: "Snd (Opair x y) = y" |
|
126 apply (simp add: Snd_def) |
|
127 apply (rule someI2) |
|
128 apply (simp_all add: Opair) |
|
129 done |
|
130 |
|
131 constdefs |
|
132 isOpair :: "ZF \<Rightarrow> bool" |
|
133 "isOpair q == ? x y. q = Opair x y" |
|
134 |
|
135 lemma isOpair: "isOpair (Opair x y) = True" |
|
136 by (auto simp add: isOpair_def) |
|
137 |
|
138 lemma FstSnd: "isOpair x \<Longrightarrow> Opair (Fst x) (Snd x) = x" |
|
139 by (auto simp add: isOpair_def Fst Snd) |
|
140 |
|
141 constdefs |
|
142 CartProd :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
143 "CartProd A B == Sum(Repl A (% a. Repl B (% b. Opair a b)))" |
|
144 |
|
145 lemma CartProd: "Elem x (CartProd A B) = (? a b. Elem a A & Elem b B & x = (Opair a b))" |
|
146 apply (auto simp add: CartProd_def Sum Repl) |
|
147 apply (rule_tac x="Repl B (Opair a)" in exI) |
|
148 apply (auto simp add: Repl) |
|
149 done |
|
150 |
|
151 constdefs |
|
152 explode :: "ZF \<Rightarrow> ZF set" |
|
153 "explode z == { x. Elem x z }" |
|
154 |
|
155 lemma explode_Empty: "(explode x = {}) = (x = Empty)" |
|
156 by (auto simp add: explode_def Ext Empty) |
|
157 |
|
158 lemma explode_Elem: "(x \<in> explode X) = (Elem x X)" |
|
159 by (simp add: explode_def) |
|
160 |
|
161 lemma Elem_explode_in: "\<lbrakk> Elem a A; explode A \<subseteq> B\<rbrakk> \<Longrightarrow> a \<in> B" |
|
162 by (auto simp add: explode_def) |
|
163 |
|
164 lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \<times> (explode b))" |
|
165 by (simp add: explode_def expand_set_eq CartProd image_def) |
|
166 |
|
167 lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)" |
|
168 by (simp add: explode_def Repl image_def) |
|
169 |
|
170 constdefs |
|
171 Domain :: "ZF \<Rightarrow> ZF" |
|
172 "Domain f == Replacement f (% p. if isOpair p then Some (Fst p) else None)" |
|
173 Range :: "ZF \<Rightarrow> ZF" |
|
174 "Range f == Replacement f (% p. if isOpair p then Some (Snd p) else None)" |
|
175 |
|
176 theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)" |
|
177 apply (auto simp add: Domain_def Replacement) |
|
178 apply (rule_tac x="Snd x" in exI) |
|
179 apply (simp add: FstSnd) |
|
180 apply (rule_tac x="Opair x y" in exI) |
|
181 apply (simp add: isOpair Fst) |
|
182 done |
|
183 |
|
184 theorem Range: "Elem y (Range f) = (? x. Elem (Opair x y) f)" |
|
185 apply (auto simp add: Range_def Replacement) |
|
186 apply (rule_tac x="Fst x" in exI) |
|
187 apply (simp add: FstSnd) |
|
188 apply (rule_tac x="Opair x y" in exI) |
|
189 apply (simp add: isOpair Snd) |
|
190 done |
|
191 |
|
192 theorem union: "Elem x (union A B) = (Elem x A | Elem x B)" |
|
193 by (auto simp add: union_def Sum Upair) |
|
194 |
|
195 constdefs |
|
196 Field :: "ZF \<Rightarrow> ZF" |
|
197 "Field A == union (Domain A) (Range A)" |
|
198 |
|
199 constdefs |
|
200 "\<acute>" :: "ZF \<Rightarrow> ZF => ZF" (infixl 90) --{*function application*} |
|
201 app_def: "f \<acute> x == (THE y. Elem (Opair x y) f)" |
|
202 |
|
203 constdefs |
|
204 isFun :: "ZF \<Rightarrow> bool" |
|
205 "isFun f == (! x y1 y2. Elem (Opair x y1) f & Elem (Opair x y2) f \<longrightarrow> y1 = y2)" |
|
206 |
|
207 constdefs |
|
208 Lambda :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF" |
|
209 "Lambda A f == Repl A (% x. Opair x (f x))" |
|
210 |
|
211 lemma Lambda_app: "Elem x A \<Longrightarrow> (Lambda A f)\<acute>x = f x" |
|
212 by (simp add: app_def Lambda_def Repl Opair) |
|
213 |
|
214 lemma isFun_Lambda: "isFun (Lambda A f)" |
|
215 by (auto simp add: isFun_def Lambda_def Repl Opair) |
|
216 |
|
217 lemma domain_Lambda: "Domain (Lambda A f) = A" |
|
218 apply (auto simp add: Domain_def) |
|
219 apply (subst Ext) |
|
220 apply (auto simp add: Replacement) |
|
221 apply (simp add: Lambda_def Repl) |
|
222 apply (auto simp add: Fst) |
|
223 apply (simp add: Lambda_def Repl) |
|
224 apply (rule_tac x="Opair z (f z)" in exI) |
|
225 apply (auto simp add: Fst isOpair_def) |
|
226 done |
|
227 |
|
228 lemma Lambda_ext: "(Lambda s f = Lambda t g) = (s = t & (! x. Elem x s \<longrightarrow> f x = g x))" |
|
229 proof - |
|
230 have "Lambda s f = Lambda t g \<Longrightarrow> s = t" |
|
231 apply (subst domain_Lambda[where A = s and f = f, symmetric]) |
|
232 apply (subst domain_Lambda[where A = t and f = g, symmetric]) |
|
233 apply auto |
|
234 done |
|
235 then show ?thesis |
|
236 apply auto |
|
237 apply (subst Lambda_app[where f=f, symmetric], simp) |
|
238 apply (subst Lambda_app[where f=g, symmetric], simp) |
|
239 apply auto |
|
240 apply (auto simp add: Lambda_def Repl Ext) |
|
241 apply (auto simp add: Ext[symmetric]) |
|
242 done |
|
243 qed |
|
244 |
|
245 constdefs |
|
246 PFun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
247 "PFun A B == Sep (Power (CartProd A B)) isFun" |
|
248 Fun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF" |
|
249 "Fun A B == Sep (PFun A B) (\<lambda> f. Domain f = A)" |
|
250 |
|
251 lemma Fun_Range: "Elem f (Fun U V) \<Longrightarrow> subset (Range f) V" |
|
252 apply (simp add: Fun_def Sep PFun_def Power subset_def CartProd) |
|
253 apply (auto simp add: Domain Range) |
|
254 apply (erule_tac x="Opair xa x" in allE) |
|
255 apply (auto simp add: Opair) |
|
256 done |
|
257 |
|
258 lemma Elem_Elem_PFun: "Elem F (PFun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V" |
|
259 apply (simp add: PFun_def Sep Power subset_def, clarify) |
|
260 apply (erule_tac x=p in allE) |
|
261 apply (auto simp add: CartProd isOpair Fst Snd) |
|
262 done |
|
263 |
|
264 lemma Fun_implies_PFun[simp]: "Elem f (Fun U V) \<Longrightarrow> Elem f (PFun U V)" |
|
265 by (simp add: Fun_def Sep) |
|
266 |
|
267 lemma Elem_Elem_Fun: "Elem F (Fun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V" |
|
268 by (auto simp add: Elem_Elem_PFun dest: Fun_implies_PFun) |
|
269 |
|
270 lemma PFun_inj: "Elem F (PFun U V) \<Longrightarrow> Elem x F \<Longrightarrow> Elem y F \<Longrightarrow> Fst x = Fst y \<Longrightarrow> Snd x = Snd y" |
|
271 apply (frule Elem_Elem_PFun[where p=x], simp) |
|
272 apply (frule Elem_Elem_PFun[where p=y], simp) |
|
273 apply (subgoal_tac "isFun F") |
|
274 apply (simp add: isFun_def isOpair_def) |
|
275 apply (auto simp add: Fst Snd, blast) |
|
276 apply (auto simp add: PFun_def Sep) |
|
277 done |
|
278 |
|
279 ML {* simp_depth_limit := 2 *} |
|
280 lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F" |
|
281 by (auto simp add: Fun_def Sep Domain) |
|
282 ML {* simp_depth_limit := 1000 *} |
|
283 |
|
284 |
|
285 lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f" |
|
286 by (auto simp add: Domain isFun_def) |
|
287 |
|
288 lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)" |
|
289 apply (auto simp add: Range) |
|
290 apply (drule unique_fun_value) |
|
291 apply simp |
|
292 apply (simp add: app_def) |
|
293 apply (rule exI[where x=x]) |
|
294 apply (auto simp add: the_equality) |
|
295 done |
|
296 |
|
297 lemma fun_range_witness: "\<lbrakk>isFun f; Elem y (Range f)\<rbrakk> \<Longrightarrow> ? x. Elem x (Domain f) & f\<acute>x = y" |
|
298 apply (auto simp add: Range) |
|
299 apply (rule_tac x="x" in exI) |
|
300 apply (auto simp add: app_def the_equality isFun_def Domain) |
|
301 done |
|
302 |
|
303 lemma Elem_Fun_Lambda: "Elem F (Fun U V) \<Longrightarrow> ? f. F = Lambda U f" |
|
304 apply (rule exI[where x= "% x. (THE y. Elem (Opair x y) F)"]) |
|
305 apply (simp add: Ext Lambda_def Repl Domain) |
|
306 apply (simp add: Ext[symmetric]) |
|
307 apply auto |
|
308 apply (frule Elem_Elem_Fun) |
|
309 apply auto |
|
310 apply (rule_tac x="Fst z" in exI) |
|
311 apply (simp add: isOpair_def) |
|
312 apply (auto simp add: Fst Snd Opair) |
|
313 apply (rule theI2') |
|
314 apply auto |
|
315 apply (drule Fun_implies_PFun) |
|
316 apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj) |
|
317 apply (auto simp add: Fst Snd) |
|
318 apply (drule Fun_implies_PFun) |
|
319 apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj) |
|
320 apply (auto simp add: Fst Snd) |
|
321 apply (rule theI2') |
|
322 apply (auto simp add: Fun_total) |
|
323 apply (drule Fun_implies_PFun) |
|
324 apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj) |
|
325 apply (auto simp add: Fst Snd) |
|
326 done |
|
327 |
|
328 lemma Elem_Lambda_Fun: "Elem (Lambda A f) (Fun U V) = (A = U & (! x. Elem x A \<longrightarrow> Elem (f x) V))" |
|
329 proof - |
|
330 have "Elem (Lambda A f) (Fun U V) \<Longrightarrow> A = U" |
|
331 by (simp add: Fun_def Sep domain_Lambda) |
|
332 then show ?thesis |
|
333 apply auto |
|
334 apply (drule Fun_Range) |
|
335 apply (subgoal_tac "f x = ((Lambda U f) \<acute> x)") |
|
336 prefer 2 |
|
337 apply (simp add: Lambda_app) |
|
338 apply simp |
|
339 apply (subgoal_tac "Elem (Lambda U f \<acute> x) (Range (Lambda U f))") |
|
340 apply (simp add: subset_def) |
|
341 apply (rule fun_value_in_range) |
|
342 apply (simp_all add: isFun_Lambda domain_Lambda) |
|
343 apply (simp add: Fun_def Sep PFun_def Power domain_Lambda isFun_Lambda) |
|
344 apply (auto simp add: subset_def CartProd) |
|
345 apply (rule_tac x="Fst x" in exI) |
|
346 apply (auto simp add: Lambda_def Repl Fst) |
|
347 done |
|
348 qed |
|
349 |
|
350 |
|
351 constdefs |
|
352 is_Elem_of :: "(ZF * ZF) set" |
|
353 "is_Elem_of == { (a,b) | a b. Elem a b }" |
|
354 |
|
355 lemma cond_wf_Elem: |
|
356 assumes hyps:"\<forall>x. (\<forall>y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y) \<longrightarrow> Elem x U \<longrightarrow> P x" "Elem a U" |
|
357 shows "P a" |
|
358 proof - |
|
359 { |
|
360 fix P |
|
361 fix U |
|
362 fix a |
|
363 assume P_induct: "(\<forall>x. (\<forall>y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y) \<longrightarrow> (Elem x U \<longrightarrow> P x))" |
|
364 assume a_in_U: "Elem a U" |
|
365 have "P a" |
|
366 proof - |
|
367 term "P" |
|
368 term Sep |
|
369 let ?Z = "Sep U (Not o P)" |
|
370 have "?Z = Empty \<longrightarrow> P a" by (simp add: Ext Sep Empty a_in_U) |
|
371 moreover have "?Z \<noteq> Empty \<longrightarrow> False" |
|
372 proof |
|
373 assume not_empty: "?Z \<noteq> Empty" |
|
374 note thereis_x = Regularity[where A="?Z", simplified not_empty, simplified] |
|
375 then obtain x where x_def: "Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" .. |
|
376 then have x_induct:"! y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y" by (simp add: Sep) |
|
377 have "Elem x U \<longrightarrow> P x" |
|
378 by (rule impE[OF spec[OF P_induct, where x=x], OF x_induct], assumption) |
|
379 moreover have "Elem x U & Not(P x)" |
|
380 apply (insert x_def) |
|
381 apply (simp add: Sep) |
|
382 done |
|
383 ultimately show "False" by auto |
|
384 qed |
|
385 ultimately show "P a" by auto |
|
386 qed |
|
387 } |
|
388 with hyps show ?thesis by blast |
|
389 qed |
|
390 |
|
391 lemma cond2_wf_Elem: |
|
392 assumes |
|
393 special_P: "? U. ! x. Not(Elem x U) \<longrightarrow> (P x)" |
|
394 and P_induct: "\<forall>x. (\<forall>y. Elem y x \<longrightarrow> P y) \<longrightarrow> P x" |
|
395 shows |
|
396 "P a" |
|
397 proof - |
|
398 have "? U Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" |
|
399 proof - |
|
400 from special_P obtain U where U:"! x. Not(Elem x U) \<longrightarrow> (P x)" .. |
|
401 show ?thesis |
|
402 apply (rule_tac exI[where x=U]) |
|
403 apply (rule exI[where x="P"]) |
|
404 apply (rule ext) |
|
405 apply (auto simp add: U) |
|
406 done |
|
407 qed |
|
408 then obtain U where "? Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" .. |
|
409 then obtain Q where UQ: "P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" .. |
|
410 show ?thesis |
|
411 apply (auto simp add: UQ) |
|
412 apply (rule cond_wf_Elem) |
|
413 apply (rule P_induct[simplified UQ]) |
|
414 apply simp |
|
415 done |
|
416 qed |
|
417 |
|
418 consts |
|
419 nat2Nat :: "nat \<Rightarrow> ZF" |
|
420 |
|
421 primrec |
|
422 nat2Nat_0[intro]: "nat2Nat 0 = Empty" |
|
423 nat2Nat_Suc[intro]: "nat2Nat (Suc n) = SucNat (nat2Nat n)" |
|
424 |
|
425 constdefs |
|
426 Nat2nat :: "ZF \<Rightarrow> nat" |
|
427 "Nat2nat == inv nat2Nat" |
|
428 |
|
429 lemma Elem_nat2Nat_inf[intro]: "Elem (nat2Nat n) Inf" |
|
430 apply (induct n) |
|
431 apply (simp_all add: Infinity) |
|
432 done |
|
433 |
|
434 constdefs |
|
435 Nat :: ZF |
|
436 "Nat == Sep Inf (\<lambda> N. ? n. nat2Nat n = N)" |
|
437 |
|
438 lemma Elem_nat2Nat_Nat[intro]: "Elem (nat2Nat n) Nat" |
|
439 by (auto simp add: Nat_def Sep) |
|
440 |
|
441 lemma Elem_Empty_Nat: "Elem Empty Nat" |
|
442 by (auto simp add: Nat_def Sep Infinity) |
|
443 |
|
444 lemma Elem_SucNat_Nat: "Elem N Nat \<Longrightarrow> Elem (SucNat N) Nat" |
|
445 by (auto simp add: Nat_def Sep Infinity) |
|
446 |
|
447 lemma no_infinite_Elem_down_chain: |
|
448 "Not (? f. isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N)))" |
|
449 proof - |
|
450 { |
|
451 fix f |
|
452 assume f:"isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N))" |
|
453 let ?r = "Range f" |
|
454 have "?r \<noteq> Empty" |
|
455 apply (auto simp add: Ext Empty) |
|
456 apply (rule exI[where x="f\<acute>Empty"]) |
|
457 apply (rule fun_value_in_range) |
|
458 apply (auto simp add: f Elem_Empty_Nat) |
|
459 done |
|
460 then have "? x. Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))" |
|
461 by (simp add: Regularity) |
|
462 then obtain x where x: "Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))" .. |
|
463 then have "? N. Elem N (Domain f) & f\<acute>N = x" |
|
464 apply (rule_tac fun_range_witness) |
|
465 apply (simp_all add: f) |
|
466 done |
|
467 then have "? N. Elem N Nat & f\<acute>N = x" |
|
468 by (simp add: f) |
|
469 then obtain N where N: "Elem N Nat & f\<acute>N = x" .. |
|
470 from N have N': "Elem N Nat" by auto |
|
471 let ?y = "f\<acute>(SucNat N)" |
|
472 have Elem_y_r: "Elem ?y ?r" |
|
473 by (simp_all add: f Elem_SucNat_Nat N fun_value_in_range) |
|
474 have "Elem ?y (f\<acute>N)" by (auto simp add: f N') |
|
475 then have "Elem ?y x" by (simp add: N) |
|
476 with x have "Not (Elem ?y ?r)" by auto |
|
477 with Elem_y_r have "False" by auto |
|
478 } |
|
479 then show ?thesis by auto |
|
480 qed |
|
481 |
|
482 lemma Upair_nonEmpty: "Upair a b \<noteq> Empty" |
|
483 by (auto simp add: Ext Empty Upair) |
|
484 |
|
485 lemma Singleton_nonEmpty: "Singleton x \<noteq> Empty" |
|
486 by (auto simp add: Singleton_def Upair_nonEmpty) |
|
487 |
|
488 lemma antisym_Elem: "Not(Elem a b & Elem b a)" |
|
489 proof - |
|
490 { |
|
491 fix a b |
|
492 assume ab: "Elem a b" |
|
493 assume ba: "Elem b a" |
|
494 let ?Z = "Upair a b" |
|
495 have "?Z \<noteq> Empty" by (simp add: Upair_nonEmpty) |
|
496 then have "? x. Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))" |
|
497 by (simp add: Regularity) |
|
498 then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))" .. |
|
499 then have "x = a \<or> x = b" by (simp add: Upair) |
|
500 moreover have "x = a \<longrightarrow> Not (Elem b ?Z)" |
|
501 by (auto simp add: x ba) |
|
502 moreover have "x = b \<longrightarrow> Not (Elem a ?Z)" |
|
503 by (auto simp add: x ab) |
|
504 ultimately have "False" |
|
505 by (auto simp add: Upair) |
|
506 } |
|
507 then show ?thesis by auto |
|
508 qed |
|
509 |
|
510 lemma irreflexiv_Elem: "Not(Elem a a)" |
|
511 by (simp add: antisym_Elem[of a a, simplified]) |
|
512 |
|
513 lemma antisym_Elem: "Elem a b \<Longrightarrow> Not (Elem b a)" |
|
514 apply (insert antisym_Elem[of a b]) |
|
515 apply auto |
|
516 done |
|
517 |
|
518 consts |
|
519 NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF" |
|
520 |
|
521 primrec |
|
522 "NatInterval n 0 = Singleton (nat2Nat n)" |
|
523 "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))" |
|
524 |
|
525 lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)" |
|
526 apply (induct m) |
|
527 apply (auto simp add: Singleton union) |
|
528 apply (case_tac "q <= m") |
|
529 apply auto |
|
530 apply (subgoal_tac "q = Suc m") |
|
531 apply auto |
|
532 done |
|
533 |
|
534 lemma NatInterval_not_Empty: "NatInterval n m \<noteq> Empty" |
|
535 by (auto intro: n_Elem_NatInterval[where q = 0, simplified] simp add: Empty Ext) |
|
536 |
|
537 lemma increasing_nat2Nat[rule_format]: "0 < n \<longrightarrow> Elem (nat2Nat (n - 1)) (nat2Nat n)" |
|
538 apply (case_tac "? m. n = Suc m") |
|
539 apply (auto simp add: SucNat_def union Singleton) |
|
540 apply (drule spec[where x="n - 1"]) |
|
541 apply arith |
|
542 done |
|
543 |
|
544 lemma represent_NatInterval[rule_format]: "Elem x (NatInterval n m) \<longrightarrow> (? u. n \<le> u & u \<le> n+m & nat2Nat u = x)" |
|
545 apply (induct m) |
|
546 apply (auto simp add: Singleton union) |
|
547 apply (rule_tac x="Suc (n+m)" in exI) |
|
548 apply auto |
|
549 done |
|
550 |
|
551 lemma inj_nat2Nat: "inj nat2Nat" |
|
552 proof - |
|
553 { |
|
554 fix n m :: nat |
|
555 assume nm: "nat2Nat n = nat2Nat (n+m)" |
|
556 assume mg0: "0 < m" |
|
557 let ?Z = "NatInterval n m" |
|
558 have "?Z \<noteq> Empty" by (simp add: NatInterval_not_Empty) |
|
559 then have "? x. (Elem x ?Z) & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" |
|
560 by (auto simp add: Regularity) |
|
561 then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" .. |
|
562 then have "? u. n \<le> u & u \<le> n+m & nat2Nat u = x" |
|
563 by (simp add: represent_NatInterval) |
|
564 then obtain u where u: "n \<le> u & u \<le> n+m & nat2Nat u = x" .. |
|
565 have "n < u \<longrightarrow> False" |
|
566 proof |
|
567 assume n_less_u: "n < u" |
|
568 let ?y = "nat2Nat (u - 1)" |
|
569 have "Elem ?y (nat2Nat u)" |
|
570 apply (rule increasing_nat2Nat) |
|
571 apply (insert n_less_u) |
|
572 apply arith |
|
573 done |
|
574 with u have "Elem ?y x" by auto |
|
575 with x have "Not (Elem ?y ?Z)" by auto |
|
576 moreover have "Elem ?y ?Z" |
|
577 apply (insert n_Elem_NatInterval[where q = "u - n - 1" and n=n and m=m]) |
|
578 apply (insert n_less_u) |
|
579 apply (insert u) |
|
580 apply auto |
|
581 apply arith |
|
582 done |
|
583 ultimately show False by auto |
|
584 qed |
|
585 moreover have "u = n \<longrightarrow> False" |
|
586 proof |
|
587 assume "u = n" |
|
588 with u have "nat2Nat n = x" by auto |
|
589 then have nm_eq_x: "nat2Nat (n+m) = x" by (simp add: nm) |
|
590 let ?y = "nat2Nat (n+m - 1)" |
|
591 have "Elem ?y (nat2Nat (n+m))" |
|
592 apply (rule increasing_nat2Nat) |
|
593 apply (insert mg0) |
|
594 apply arith |
|
595 done |
|
596 with nm_eq_x have "Elem ?y x" by auto |
|
597 with x have "Not (Elem ?y ?Z)" by auto |
|
598 moreover have "Elem ?y ?Z" |
|
599 apply (insert n_Elem_NatInterval[where q = "m - 1" and n=n and m=m]) |
|
600 apply (insert mg0) |
|
601 apply auto |
|
602 done |
|
603 ultimately show False by auto |
|
604 qed |
|
605 ultimately have "False" using u by arith |
|
606 } |
|
607 note lemma_nat2Nat = this |
|
608 show ?thesis |
|
609 apply (auto simp add: inj_on_def) |
|
610 apply (case_tac "x = y") |
|
611 apply auto |
|
612 apply (case_tac "x < y") |
|
613 apply (case_tac "? m. y = x + m & 0 < m") |
|
614 apply (auto intro: lemma_nat2Nat, arith) |
|
615 apply (case_tac "y < x") |
|
616 apply (case_tac "? m. x = y + m & 0 < m") |
|
617 apply auto |
|
618 apply (drule sym) |
|
619 apply (auto intro: lemma_nat2Nat, arith) |
|
620 done |
|
621 qed |
|
622 |
|
623 lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n" |
|
624 by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat]) |
|
625 |
|
626 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n" |
|
627 apply (simp add: Nat2nat_def) |
|
628 apply (rule_tac f_inv_f) |
|
629 apply (auto simp add: image_def Nat_def Sep) |
|
630 done |
|
631 |
|
632 lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)" |
|
633 apply (auto simp add: Nat_def Sep Nat2nat_def) |
|
634 apply (auto simp add: inv_f_f[OF inj_nat2Nat]) |
|
635 apply (simp only: nat2Nat.simps[symmetric]) |
|
636 apply (simp only: inv_f_f[OF inj_nat2Nat]) |
|
637 done |
|
638 |
|
639 |
|
640 (*lemma Elem_induct: "(\<And>x. \<forall>y. Elem y x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" |
|
641 by (erule wf_induct[OF wf_is_Elem_of, simplified is_Elem_of_def, simplified])*) |
|
642 |
|
643 lemma Elem_Opair_exists: "? z. Elem x z & Elem y z & Elem z (Opair x y)" |
|
644 apply (rule exI[where x="Upair x y"]) |
|
645 by (simp add: Upair Opair_def) |
|
646 |
|
647 lemma UNIV_is_not_in_ZF: "UNIV \<noteq> explode R" |
|
648 proof |
|
649 let ?Russell = "{ x. Not(Elem x x) }" |
|
650 have "?Russell = UNIV" by (simp add: irreflexiv_Elem) |
|
651 moreover assume "UNIV = explode R" |
|
652 ultimately have russell: "?Russell = explode R" by simp |
|
653 then show "False" |
|
654 proof(cases "Elem R R") |
|
655 case True |
|
656 then show ?thesis |
|
657 by (insert irreflexiv_Elem, auto) |
|
658 next |
|
659 case False |
|
660 then have "R \<in> ?Russell" by auto |
|
661 then have "Elem R R" by (simp add: russell explode_def) |
|
662 with False show ?thesis by auto |
|
663 qed |
|
664 qed |
|
665 |
|
666 constdefs |
|
667 SpecialR :: "(ZF * ZF) set" |
|
668 "SpecialR \<equiv> { (x, y) . x \<noteq> Empty \<and> y = Empty}" |
|
669 |
|
670 lemma "wf SpecialR" |
|
671 apply (subst wf_def) |
|
672 apply (auto simp add: SpecialR_def) |
|
673 done |
|
674 |
|
675 constdefs |
|
676 Ext :: "('a * 'b) set \<Rightarrow> 'b \<Rightarrow> 'a set" |
|
677 "Ext R y \<equiv> { x . (x, y) \<in> R }" |
|
678 |
|
679 lemma Ext_Elem: "Ext is_Elem_of = explode" |
|
680 by (auto intro: ext simp add: Ext_def is_Elem_of_def explode_def) |
|
681 |
|
682 lemma "Ext SpecialR Empty \<noteq> explode z" |
|
683 proof |
|
684 have "Ext SpecialR Empty = UNIV - {Empty}" |
|
685 by (auto simp add: Ext_def SpecialR_def) |
|
686 moreover assume "Ext SpecialR Empty = explode z" |
|
687 ultimately have "UNIV = explode(union z (Singleton Empty)) " |
|
688 by (auto simp add: explode_def union Singleton) |
|
689 then show "False" by (simp add: UNIV_is_not_in_ZF) |
|
690 qed |
|
691 |
|
692 constdefs |
|
693 implode :: "ZF set \<Rightarrow> ZF" |
|
694 "implode == inv explode" |
|
695 |
|
696 lemma inj_explode: "inj explode" |
|
697 by (auto simp add: inj_on_def explode_def Ext) |
|
698 |
|
699 lemma implode_explode[simp]: "implode (explode x) = x" |
|
700 by (simp add: implode_def inj_explode) |
|
701 |
|
702 constdefs |
|
703 regular :: "(ZF * ZF) set \<Rightarrow> bool" |
|
704 "regular R == ! A. A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. (y, x) \<in> R \<longrightarrow> Not (Elem y A)))" |
|
705 implodeable_Ext :: "(ZF * ZF) set \<Rightarrow> bool" |
|
706 "implodeable_Ext R == ! y. Ext R y \<in> range explode" |
|
707 wfzf :: "(ZF * ZF) set \<Rightarrow> bool" |
|
708 "wfzf R == regular R & implodeable_Ext R" |
|
709 |
|
710 lemma regular_Elem: "regular is_Elem_of" |
|
711 by (simp add: regular_def is_Elem_of_def Regularity) |
|
712 |
|
713 lemma implodeable_Elem: "implodeable_Ext is_Elem_of" |
|
714 by (auto simp add: implodeable_Ext_def image_def Ext_Elem) |
|
715 |
|
716 lemma wfzf_is_Elem_of: "wfzf is_Elem_of" |
|
717 by (auto simp add: wfzf_def regular_Elem implodeable_Elem) |
|
718 |
|
719 constdefs |
|
720 SeqSum :: "(nat \<Rightarrow> ZF) \<Rightarrow> ZF" |
|
721 "SeqSum f == Sum (Repl Nat (f o Nat2nat))" |
|
722 |
|
723 lemma SeqSum: "Elem x (SeqSum f) = (? n. Elem x (f n))" |
|
724 apply (auto simp add: SeqSum_def Sum Repl) |
|
725 apply (rule_tac x = "f n" in exI) |
|
726 apply auto |
|
727 done |
|
728 |
|
729 constdefs |
|
730 Ext_ZF :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF" |
|
731 "Ext_ZF R s == implode (Ext R s)" |
|
732 |
|
733 lemma Elem_implode: "A \<in> range explode \<Longrightarrow> Elem x (implode A) = (x \<in> A)" |
|
734 apply (auto) |
|
735 apply (simp_all add: explode_def) |
|
736 done |
|
737 |
|
738 lemma Elem_Ext_ZF: "implodeable_Ext R \<Longrightarrow> Elem x (Ext_ZF R s) = ((x,s) \<in> R)" |
|
739 apply (simp add: Ext_ZF_def) |
|
740 apply (subst Elem_implode) |
|
741 apply (simp add: implodeable_Ext_def) |
|
742 apply (simp add: Ext_def) |
|
743 done |
|
744 |
|
745 consts |
|
746 Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF" |
|
747 |
|
748 primrec |
|
749 "Ext_ZF_n R s 0 = Ext_ZF R s" |
|
750 "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))" |
|
751 |
|
752 constdefs |
|
753 Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF" |
|
754 "Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)" |
|
755 |
|
756 lemma Elem_Ext_ZF_hull: |
|
757 assumes implodeable_R: "implodeable_Ext R" |
|
758 shows "Elem x (Ext_ZF_hull R S) = (? n. Elem x (Ext_ZF_n R S n))" |
|
759 by (simp add: Ext_ZF_hull_def SeqSum) |
|
760 |
|
761 lemma Elem_Elem_Ext_ZF_hull: |
|
762 assumes implodeable_R: "implodeable_Ext R" |
|
763 and x_hull: "Elem x (Ext_ZF_hull R S)" |
|
764 and y_R_x: "(y, x) \<in> R" |
|
765 shows "Elem y (Ext_ZF_hull R S)" |
|
766 proof - |
|
767 from Elem_Ext_ZF_hull[OF implodeable_R] x_hull |
|
768 have "? n. Elem x (Ext_ZF_n R S n)" by auto |
|
769 then obtain n where n:"Elem x (Ext_ZF_n R S n)" .. |
|
770 with y_R_x have "Elem y (Ext_ZF_n R S (Suc n))" |
|
771 apply (auto simp add: Repl Sum) |
|
772 apply (rule_tac x="Ext_ZF R x" in exI) |
|
773 apply (auto simp add: Elem_Ext_ZF[OF implodeable_R]) |
|
774 done |
|
775 with Elem_Ext_ZF_hull[OF implodeable_R, where x=y] show ?thesis |
|
776 by (auto simp del: Ext_ZF_n.simps) |
|
777 qed |
|
778 |
|
779 lemma wfzf_minimal: |
|
780 assumes hyps: "wfzf R" "C \<noteq> {}" |
|
781 shows "\<exists>x. x \<in> C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> C)" |
|
782 proof - |
|
783 from hyps have "\<exists>S. S \<in> C" by auto |
|
784 then obtain S where S:"S \<in> C" by auto |
|
785 let ?T = "Sep (Ext_ZF_hull R S) (\<lambda> s. s \<in> C)" |
|
786 from hyps have implodeable_R: "implodeable_Ext R" by (simp add: wfzf_def) |
|
787 show ?thesis |
|
788 proof (cases "?T = Empty") |
|
789 case True |
|
790 then have "\<forall> z. \<not> (Elem z (Sep (Ext_ZF R S) (\<lambda> s. s \<in> C)))" |
|
791 apply (auto simp add: Ext Empty Sep Ext_ZF_hull_def SeqSum) |
|
792 apply (erule_tac x="z" in allE, auto) |
|
793 apply (erule_tac x=0 in allE, auto) |
|
794 done |
|
795 then show ?thesis |
|
796 apply (rule_tac exI[where x=S]) |
|
797 apply (auto simp add: Sep Empty S) |
|
798 apply (erule_tac x=y in allE) |
|
799 apply (simp add: implodeable_R Elem_Ext_ZF) |
|
800 done |
|
801 next |
|
802 case False |
|
803 from hyps have regular_R: "regular R" by (simp add: wfzf_def) |
|
804 from |
|
805 regular_R[simplified regular_def, rule_format, OF False, simplified Sep] |
|
806 Elem_Elem_Ext_ZF_hull[OF implodeable_R] |
|
807 show ?thesis by blast |
|
808 qed |
|
809 qed |
|
810 |
|
811 lemma wfzf_implies_wf: "wfzf R \<Longrightarrow> wf R" |
|
812 proof (subst wf_def, rule allI) |
|
813 assume wfzf: "wfzf R" |
|
814 fix P :: "ZF \<Rightarrow> bool" |
|
815 let ?C = "{x. P x}" |
|
816 { |
|
817 assume induct: "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x)" |
|
818 let ?C = "{x. \<not> (P x)}" |
|
819 have "?C = {}" |
|
820 proof (rule ccontr) |
|
821 assume C: "?C \<noteq> {}" |
|
822 from |
|
823 wfzf_minimal[OF wfzf C] |
|
824 obtain x where x: "x \<in> ?C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> ?C)" .. |
|
825 then have "P x" |
|
826 apply (rule_tac induct[rule_format]) |
|
827 apply auto |
|
828 done |
|
829 with x show "False" by auto |
|
830 qed |
|
831 then have "! x. P x" by auto |
|
832 } |
|
833 then show "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (! x. P x)" by blast |
|
834 qed |
|
835 |
|
836 lemma wf_is_Elem_of: "wf is_Elem_of" |
|
837 by (auto simp add: wfzf_is_Elem_of wfzf_implies_wf) |
|
838 |
|
839 lemma in_Ext_RTrans_implies_Elem_Ext_ZF_hull: |
|
840 "implodeable_Ext R \<Longrightarrow> x \<in> (Ext (R^+) s) \<Longrightarrow> Elem x (Ext_ZF_hull R s)" |
|
841 apply (simp add: Ext_def Elem_Ext_ZF_hull) |
|
842 apply (erule converse_trancl_induct[where r="R"]) |
|
843 apply (rule exI[where x=0]) |
|
844 apply (simp add: Elem_Ext_ZF) |
|
845 apply auto |
|
846 apply (rule_tac x="Suc n" in exI) |
|
847 apply (simp add: Sum Repl) |
|
848 apply (rule_tac x="Ext_ZF R z" in exI) |
|
849 apply (auto simp add: Elem_Ext_ZF) |
|
850 done |
|
851 |
|
852 lemma implodeable_Ext_trancl: "implodeable_Ext R \<Longrightarrow> implodeable_Ext (R^+)" |
|
853 apply (subst implodeable_Ext_def) |
|
854 apply (auto simp add: image_def) |
|
855 apply (rule_tac x="Sep (Ext_ZF_hull R y) (\<lambda> z. z \<in> (Ext (R^+) y))" in exI) |
|
856 apply (auto simp add: explode_def Sep set_ext |
|
857 in_Ext_RTrans_implies_Elem_Ext_ZF_hull) |
|
858 done |
|
859 |
|
860 lemma Elem_Ext_ZF_hull_implies_in_Ext_RTrans[rule_format]: |
|
861 "implodeable_Ext R \<Longrightarrow> ! x. Elem x (Ext_ZF_n R s n) \<longrightarrow> x \<in> (Ext (R^+) s)" |
|
862 apply (induct_tac n) |
|
863 apply (auto simp add: Elem_Ext_ZF Ext_def Sum Repl) |
|
864 done |
|
865 |
|
866 lemma "implodeable_Ext R \<Longrightarrow> Ext_ZF (R^+) s = Ext_ZF_hull R s" |
|
867 apply (frule implodeable_Ext_trancl) |
|
868 apply (auto simp add: Ext) |
|
869 apply (erule in_Ext_RTrans_implies_Elem_Ext_ZF_hull) |
|
870 apply (simp add: Elem_Ext_ZF Ext_def) |
|
871 apply (auto simp add: Elem_Ext_ZF Elem_Ext_ZF_hull) |
|
872 apply (erule Elem_Ext_ZF_hull_implies_in_Ext_RTrans[simplified Ext_def, simplified], assumption) |
|
873 done |
|
874 |
|
875 lemma wf_implies_regular: "wf R \<Longrightarrow> regular R" |
|
876 proof (simp add: regular_def, rule allI) |
|
877 assume wf: "wf R" |
|
878 fix A |
|
879 show "A \<noteq> Empty \<longrightarrow> (\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A))" |
|
880 proof |
|
881 assume A: "A \<noteq> Empty" |
|
882 then have "? x. x \<in> explode A" |
|
883 by (auto simp add: explode_def Ext Empty) |
|
884 then obtain x where x:"x \<in> explode A" .. |
|
885 from iffD1[OF wf_eq_minimal wf, rule_format, where Q="explode A", OF x] |
|
886 obtain z where "z \<in> explode A \<and> (\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> explode A)" by auto |
|
887 then show "\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A)" |
|
888 apply (rule_tac exI[where x = z]) |
|
889 apply (simp add: explode_def) |
|
890 done |
|
891 qed |
|
892 qed |
|
893 |
|
894 lemma wf_eq_wfzf: "(wf R \<and> implodeable_Ext R) = wfzf R" |
|
895 apply (auto simp add: wfzf_implies_wf) |
|
896 apply (auto simp add: wfzf_def wf_implies_regular) |
|
897 done |
|
898 |
|
899 lemma wfzf_trancl: "wfzf R \<Longrightarrow> wfzf (R^+)" |
|
900 by (auto simp add: wf_eq_wfzf[symmetric] implodeable_Ext_trancl wf_trancl) |
|
901 |
|
902 lemma Ext_subset_mono: "R \<subseteq> S \<Longrightarrow> Ext R y \<subseteq> Ext S y" |
|
903 by (auto simp add: Ext_def) |
|
904 |
|
905 lemma implodeable_Ext_subset: "implodeable_Ext R \<Longrightarrow> S \<subseteq> R \<Longrightarrow> implodeable_Ext S" |
|
906 apply (auto simp add: implodeable_Ext_def) |
|
907 apply (erule_tac x=y in allE) |
|
908 apply (drule_tac y=y in Ext_subset_mono) |
|
909 apply (auto simp add: image_def) |
|
910 apply (rule_tac x="Sep x (% z. z \<in> (Ext S y))" in exI) |
|
911 apply (auto simp add: explode_def Sep) |
|
912 done |
|
913 |
|
914 lemma wfzf_subset: "wfzf S \<Longrightarrow> R \<subseteq> S \<Longrightarrow> wfzf R" |
|
915 by (auto intro: implodeable_Ext_subset wf_subset simp add: wf_eq_wfzf[symmetric]) |
|
916 |
|
917 end |