|
1 (* Title: HOL/Cardinals/Wellorder_Relation.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Well-order relations. |
|
6 *) |
|
7 |
|
8 header {* Well-Order Relations *} |
|
9 |
|
10 theory Wellorder_Relation |
|
11 imports Wellorder_Relation_Base Wellfounded_More |
|
12 begin |
|
13 |
|
14 |
|
15 subsection {* Auxiliaries *} |
|
16 |
|
17 lemma (in wo_rel) PREORD: "Preorder r" |
|
18 using WELL order_on_defs[of _ r] by auto |
|
19 |
|
20 lemma (in wo_rel) PARORD: "Partial_order r" |
|
21 using WELL order_on_defs[of _ r] by auto |
|
22 |
|
23 lemma (in wo_rel) cases_Total2: |
|
24 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b); |
|
25 ((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk> |
|
26 \<Longrightarrow> phi a b" |
|
27 using TOTALS by auto |
|
28 |
|
29 |
|
30 subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *} |
|
31 |
|
32 lemma (in wo_rel) worec_unique_fixpoint: |
|
33 assumes ADM: "adm_wo H" and fp: "f = H f" |
|
34 shows "f = worec H" |
|
35 proof- |
|
36 have "adm_wf (r - Id) H" |
|
37 unfolding adm_wf_def |
|
38 using ADM adm_wo_def[of H] underS_def by auto |
|
39 hence "f = wfrec (r - Id) H" |
|
40 using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp |
|
41 thus ?thesis unfolding worec_def . |
|
42 qed |
|
43 |
|
44 |
|
45 subsubsection {* Properties of max2 *} |
|
46 |
|
47 lemma (in wo_rel) max2_iff: |
|
48 assumes "a \<in> Field r" and "b \<in> Field r" |
|
49 shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)" |
|
50 proof |
|
51 assume "(max2 a b, c) \<in> r" |
|
52 thus "(a,c) \<in> r \<and> (b,c) \<in> r" |
|
53 using assms max2_greater[of a b] TRANS trans_def[of r] by blast |
|
54 next |
|
55 assume "(a,c) \<in> r \<and> (b,c) \<in> r" |
|
56 thus "(max2 a b, c) \<in> r" |
|
57 using assms max2_among[of a b] by auto |
|
58 qed |
|
59 |
|
60 |
|
61 subsubsection{* Properties of minim *} |
|
62 |
|
63 lemma (in wo_rel) minim_Under: |
|
64 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B" |
|
65 by(auto simp add: Under_def |
|
66 minim_in |
|
67 minim_inField |
|
68 minim_least |
|
69 under_ofilter |
|
70 underS_ofilter |
|
71 Field_ofilter |
|
72 ofilter_Under |
|
73 ofilter_UnderS |
|
74 ofilter_Un |
|
75 ) |
|
76 |
|
77 lemma (in wo_rel) equals_minim_Under: |
|
78 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk> |
|
79 \<Longrightarrow> a = minim B" |
|
80 by(auto simp add: Under_def equals_minim) |
|
81 |
|
82 lemma (in wo_rel) minim_iff_In_Under: |
|
83 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}" |
|
84 shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)" |
|
85 proof |
|
86 assume "a = minim B" |
|
87 thus "a \<in> B \<and> a \<in> Under B" |
|
88 using assms minim_in minim_Under by simp |
|
89 next |
|
90 assume "a \<in> B \<and> a \<in> Under B" |
|
91 thus "a = minim B" |
|
92 using assms equals_minim_Under by simp |
|
93 qed |
|
94 |
|
95 lemma (in wo_rel) minim_Under_under: |
|
96 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
|
97 shows "Under A = under (minim A)" |
|
98 proof- |
|
99 (* Preliminary facts *) |
|
100 have 1: "minim A \<in> A" |
|
101 using assms minim_in by auto |
|
102 have 2: "\<forall>x \<in> A. (minim A, x) \<in> r" |
|
103 using assms minim_least by auto |
|
104 (* Main proof *) |
|
105 have "Under A \<le> under (minim A)" |
|
106 proof |
|
107 fix x assume "x \<in> Under A" |
|
108 with 1 Under_def have "(x,minim A) \<in> r" by auto |
|
109 thus "x \<in> under(minim A)" unfolding under_def by simp |
|
110 qed |
|
111 (* *) |
|
112 moreover |
|
113 (* *) |
|
114 have "under (minim A) \<le> Under A" |
|
115 proof |
|
116 fix x assume "x \<in> under(minim A)" |
|
117 hence 11: "(x,minim A) \<in> r" unfolding under_def by simp |
|
118 hence "x \<in> Field r" unfolding Field_def by auto |
|
119 moreover |
|
120 {fix a assume "a \<in> A" |
|
121 with 2 have "(minim A, a) \<in> r" by simp |
|
122 with 11 have "(x,a) \<in> r" |
|
123 using TRANS trans_def[of r] by blast |
|
124 } |
|
125 ultimately show "x \<in> Under A" by (unfold Under_def, auto) |
|
126 qed |
|
127 (* *) |
|
128 ultimately show ?thesis by blast |
|
129 qed |
|
130 |
|
131 lemma (in wo_rel) minim_UnderS_underS: |
|
132 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
|
133 shows "UnderS A = underS (minim A)" |
|
134 proof- |
|
135 (* Preliminary facts *) |
|
136 have 1: "minim A \<in> A" |
|
137 using assms minim_in by auto |
|
138 have 2: "\<forall>x \<in> A. (minim A, x) \<in> r" |
|
139 using assms minim_least by auto |
|
140 (* Main proof *) |
|
141 have "UnderS A \<le> underS (minim A)" |
|
142 proof |
|
143 fix x assume "x \<in> UnderS A" |
|
144 with 1 UnderS_def have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto |
|
145 thus "x \<in> underS(minim A)" unfolding underS_def by simp |
|
146 qed |
|
147 (* *) |
|
148 moreover |
|
149 (* *) |
|
150 have "underS (minim A) \<le> UnderS A" |
|
151 proof |
|
152 fix x assume "x \<in> underS(minim A)" |
|
153 hence 11: "x \<noteq> minim A \<and> (x,minim A) \<in> r" unfolding underS_def by simp |
|
154 hence "x \<in> Field r" unfolding Field_def by auto |
|
155 moreover |
|
156 {fix a assume "a \<in> A" |
|
157 with 2 have 3: "(minim A, a) \<in> r" by simp |
|
158 with 11 have "(x,a) \<in> r" |
|
159 using TRANS trans_def[of r] by blast |
|
160 moreover |
|
161 have "x \<noteq> a" |
|
162 proof |
|
163 assume "x = a" |
|
164 with 11 3 ANTISYM antisym_def[of r] |
|
165 show False by auto |
|
166 qed |
|
167 ultimately |
|
168 have "x \<noteq> a \<and> (x,a) \<in> r" by simp |
|
169 } |
|
170 ultimately show "x \<in> UnderS A" by (unfold UnderS_def, auto) |
|
171 qed |
|
172 (* *) |
|
173 ultimately show ?thesis by blast |
|
174 qed |
|
175 |
|
176 |
|
177 subsubsection{* Properties of supr *} |
|
178 |
|
179 lemma (in wo_rel) supr_Above: |
|
180 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" |
|
181 shows "supr B \<in> Above B" |
|
182 proof(unfold supr_def) |
|
183 have "Above B \<le> Field r" |
|
184 using Above_Field by auto |
|
185 thus "minim (Above B) \<in> Above B" |
|
186 using assms by (simp add: minim_in) |
|
187 qed |
|
188 |
|
189 lemma (in wo_rel) supr_greater: |
|
190 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and |
|
191 IN: "b \<in> B" |
|
192 shows "(b, supr B) \<in> r" |
|
193 proof- |
|
194 from assms supr_Above |
|
195 have "supr B \<in> Above B" by simp |
|
196 with IN Above_def show ?thesis by simp |
|
197 qed |
|
198 |
|
199 lemma (in wo_rel) supr_least_Above: |
|
200 assumes SUB: "B \<le> Field r" and |
|
201 ABOVE: "a \<in> Above B" |
|
202 shows "(supr B, a) \<in> r" |
|
203 proof(unfold supr_def) |
|
204 have "Above B \<le> Field r" |
|
205 using Above_Field by auto |
|
206 thus "(minim (Above B), a) \<in> r" |
|
207 using assms minim_least |
|
208 by simp |
|
209 qed |
|
210 |
|
211 lemma (in wo_rel) supr_least: |
|
212 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk> |
|
213 \<Longrightarrow> (supr B, a) \<in> r" |
|
214 by(auto simp add: supr_least_Above Above_def) |
|
215 |
|
216 lemma (in wo_rel) equals_supr_Above: |
|
217 assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and |
|
218 MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r" |
|
219 shows "a = supr B" |
|
220 proof(unfold supr_def) |
|
221 have "Above B \<le> Field r" |
|
222 using Above_Field by auto |
|
223 thus "a = minim (Above B)" |
|
224 using assms equals_minim by simp |
|
225 qed |
|
226 |
|
227 lemma (in wo_rel) equals_supr: |
|
228 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and |
|
229 ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and |
|
230 MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r" |
|
231 shows "a = supr B" |
|
232 proof- |
|
233 have "a \<in> Above B" |
|
234 unfolding Above_def using ABV IN by simp |
|
235 moreover |
|
236 have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r" |
|
237 unfolding Above_def using MINIM by simp |
|
238 ultimately show ?thesis |
|
239 using equals_supr_Above SUB by auto |
|
240 qed |
|
241 |
|
242 lemma (in wo_rel) supr_inField: |
|
243 assumes "B \<le> Field r" and "Above B \<noteq> {}" |
|
244 shows "supr B \<in> Field r" |
|
245 proof- |
|
246 have "supr B \<in> Above B" using supr_Above assms by simp |
|
247 thus ?thesis using assms Above_Field by auto |
|
248 qed |
|
249 |
|
250 lemma (in wo_rel) supr_above_Above: |
|
251 assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" |
|
252 shows "Above B = above (supr B)" |
|
253 proof(unfold Above_def above_def, auto) |
|
254 fix a assume "a \<in> Field r" "\<forall>b \<in> B. (b,a) \<in> r" |
|
255 with supr_least assms |
|
256 show "(supr B, a) \<in> r" by auto |
|
257 next |
|
258 fix b assume "(supr B, b) \<in> r" |
|
259 thus "b \<in> Field r" |
|
260 using REFL refl_on_def[of _ r] by auto |
|
261 next |
|
262 fix a b |
|
263 assume 1: "(supr B, b) \<in> r" and 2: "a \<in> B" |
|
264 with assms supr_greater |
|
265 have "(a,supr B) \<in> r" by auto |
|
266 thus "(a,b) \<in> r" |
|
267 using 1 TRANS trans_def[of r] by blast |
|
268 qed |
|
269 |
|
270 lemma (in wo_rel) supr_under: |
|
271 assumes IN: "a \<in> Field r" |
|
272 shows "a = supr (under a)" |
|
273 proof- |
|
274 have "under a \<le> Field r" |
|
275 using under_Field by auto |
|
276 moreover |
|
277 have "under a \<noteq> {}" |
|
278 using IN Refl_under_in REFL by auto |
|
279 moreover |
|
280 have "a \<in> Above (under a)" |
|
281 using in_Above_under IN by auto |
|
282 moreover |
|
283 have "\<forall>a' \<in> Above (under a). (a,a') \<in> r" |
|
284 proof(unfold Above_def under_def, auto) |
|
285 fix a' |
|
286 assume "\<forall>aa. (aa, a) \<in> r \<longrightarrow> (aa, a') \<in> r" |
|
287 hence "(a,a) \<in> r \<longrightarrow> (a,a') \<in> r" by blast |
|
288 moreover have "(a,a) \<in> r" |
|
289 using REFL IN by (auto simp add: refl_on_def) |
|
290 ultimately |
|
291 show "(a, a') \<in> r" by (rule mp) |
|
292 qed |
|
293 ultimately show ?thesis |
|
294 using equals_supr_Above by auto |
|
295 qed |
|
296 |
|
297 |
|
298 subsubsection{* Properties of successor *} |
|
299 |
|
300 lemma (in wo_rel) suc_least: |
|
301 "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk> |
|
302 \<Longrightarrow> (suc B, a) \<in> r" |
|
303 by(auto simp add: suc_least_AboveS AboveS_def) |
|
304 |
|
305 lemma (in wo_rel) equals_suc: |
|
306 assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and |
|
307 ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and |
|
308 MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r" |
|
309 shows "a = suc B" |
|
310 proof- |
|
311 have "a \<in> AboveS B" |
|
312 unfolding AboveS_def using ABVS IN by simp |
|
313 moreover |
|
314 have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r" |
|
315 unfolding AboveS_def using MINIM by simp |
|
316 ultimately show ?thesis |
|
317 using equals_suc_AboveS SUB by auto |
|
318 qed |
|
319 |
|
320 lemma (in wo_rel) suc_above_AboveS: |
|
321 assumes SUB: "B \<le> Field r" and |
|
322 ABOVE: "AboveS B \<noteq> {}" |
|
323 shows "AboveS B = above (suc B)" |
|
324 proof(unfold AboveS_def above_def, auto) |
|
325 fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r" |
|
326 with suc_least assms |
|
327 show "(suc B,a) \<in> r" by auto |
|
328 next |
|
329 fix b assume "(suc B, b) \<in> r" |
|
330 thus "b \<in> Field r" |
|
331 using REFL refl_on_def[of _ r] by auto |
|
332 next |
|
333 fix a b |
|
334 assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B" |
|
335 with assms suc_greater[of B a] |
|
336 have "(a,suc B) \<in> r" by auto |
|
337 thus "(a,b) \<in> r" |
|
338 using 1 TRANS trans_def[of r] by blast |
|
339 next |
|
340 fix a |
|
341 assume 1: "(suc B, a) \<in> r" and 2: "a \<in> B" |
|
342 with assms suc_greater[of B a] |
|
343 have "(a,suc B) \<in> r" by auto |
|
344 moreover have "suc B \<in> Field r" |
|
345 using assms suc_inField by simp |
|
346 ultimately have "a = suc B" |
|
347 using 1 2 SUB ANTISYM antisym_def[of r] by auto |
|
348 thus False |
|
349 using assms suc_greater[of B a] 2 by auto |
|
350 qed |
|
351 |
|
352 lemma (in wo_rel) suc_singl_pred: |
|
353 assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and |
|
354 REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}" |
|
355 shows "a' = a \<or> (a',a) \<in> r" |
|
356 proof- |
|
357 have *: "suc {a} \<in> Field r \<and> a' \<in> Field r" |
|
358 using WELL REL well_order_on_domain by auto |
|
359 {assume **: "a' \<noteq> a" |
|
360 hence "(a,a') \<in> r \<or> (a',a) \<in> r" |
|
361 using TOTAL IN * by (auto simp add: total_on_def) |
|
362 moreover |
|
363 {assume "(a,a') \<in> r" |
|
364 with ** * assms WELL suc_least[of "{a}" a'] |
|
365 have "(suc {a},a') \<in> r" by auto |
|
366 with REL DIFF * ANTISYM antisym_def[of r] |
|
367 have False by simp |
|
368 } |
|
369 ultimately have "(a',a) \<in> r" |
|
370 by blast |
|
371 } |
|
372 thus ?thesis by blast |
|
373 qed |
|
374 |
|
375 lemma (in wo_rel) under_underS_suc: |
|
376 assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}" |
|
377 shows "underS (suc {a}) = under a" |
|
378 proof- |
|
379 have 1: "AboveS {a} \<noteq> {}" |
|
380 using ABV aboveS_AboveS_singl by auto |
|
381 have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r" |
|
382 using suc_greater[of "{a}" a] IN 1 by auto |
|
383 (* *) |
|
384 have "underS (suc {a}) \<le> under a" |
|
385 proof(unfold underS_def under_def, auto) |
|
386 fix x assume *: "x \<noteq> suc {a}" and **: "(x,suc {a}) \<in> r" |
|
387 with suc_singl_pred[of a x] IN ABV |
|
388 have "x = a \<or> (x,a) \<in> r" by auto |
|
389 with REFL refl_on_def[of _ r] IN |
|
390 show "(x,a) \<in> r" by auto |
|
391 qed |
|
392 (* *) |
|
393 moreover |
|
394 (* *) |
|
395 have "under a \<le> underS (suc {a})" |
|
396 proof(unfold underS_def under_def, auto) |
|
397 assume "(suc {a}, a) \<in> r" |
|
398 with 2 ANTISYM antisym_def[of r] |
|
399 show False by auto |
|
400 next |
|
401 fix x assume *: "(x,a) \<in> r" |
|
402 with 2 TRANS trans_def[of r] |
|
403 show "(x,suc {a}) \<in> r" by blast |
|
404 (* blast is often better than auto/auto for transitivity-like properties *) |
|
405 qed |
|
406 (* *) |
|
407 ultimately show ?thesis by blast |
|
408 qed |
|
409 |
|
410 |
|
411 subsubsection {* Properties of order filters *} |
|
412 |
|
413 lemma (in wo_rel) ofilter_INTER: |
|
414 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)" |
|
415 unfolding ofilter_def by blast |
|
416 |
|
417 lemma (in wo_rel) ofilter_Inter: |
|
418 "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)" |
|
419 unfolding ofilter_def by blast |
|
420 |
|
421 lemma (in wo_rel) ofilter_Union: |
|
422 "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)" |
|
423 unfolding ofilter_def by blast |
|
424 |
|
425 lemma (in wo_rel) ofilter_under_Union: |
|
426 "ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}" |
|
427 using ofilter_under_UNION[of A] |
|
428 by(unfold Union_eq, auto) |
|
429 |
|
430 |
|
431 subsubsection{* Other properties *} |
|
432 |
|
433 lemma (in wo_rel) Trans_Under_regressive: |
|
434 assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
|
435 shows "Under(Under A) \<le> Under A" |
|
436 proof |
|
437 let ?a = "minim A" |
|
438 (* Preliminary facts *) |
|
439 have 1: "minim A \<in> Under A" |
|
440 using assms minim_Under by auto |
|
441 have 2: "\<forall>y \<in> A. (minim A, y) \<in> r" |
|
442 using assms minim_least by auto |
|
443 (* Main proof *) |
|
444 fix x assume "x \<in> Under(Under A)" |
|
445 with 1 have 1: "(x,minim A) \<in> r" |
|
446 using Under_def by auto |
|
447 with Field_def have "x \<in> Field r" by fastforce |
|
448 moreover |
|
449 {fix y assume *: "y \<in> A" |
|
450 hence "(x,y) \<in> r" |
|
451 using 1 2 TRANS trans_def[of r] by blast |
|
452 with Field_def have "(x,y) \<in> r" by auto |
|
453 } |
|
454 ultimately |
|
455 show "x \<in> Under A" unfolding Under_def by auto |
|
456 qed |
|
457 |
|
458 lemma (in wo_rel) ofilter_suc_Field: |
|
459 assumes OF: "ofilter A" and NE: "A \<noteq> Field r" |
|
460 shows "ofilter (A \<union> {suc A})" |
|
461 proof- |
|
462 (* Preliminary facts *) |
|
463 have 1: "A \<le> Field r" using OF ofilter_def by auto |
|
464 hence 2: "AboveS A \<noteq> {}" |
|
465 using ofilter_AboveS_Field NE OF by blast |
|
466 from 1 2 suc_inField |
|
467 have 3: "suc A \<in> Field r" by auto |
|
468 (* Main proof *) |
|
469 show ?thesis |
|
470 proof(unfold ofilter_def, auto simp add: 1 3) |
|
471 fix a x |
|
472 assume "a \<in> A" "x \<in> under a" "x \<notin> A" |
|
473 with OF ofilter_def have False by auto |
|
474 thus "x = suc A" by simp |
|
475 next |
|
476 fix x assume *: "x \<in> under (suc A)" and **: "x \<notin> A" |
|
477 hence "x \<in> Field r" using under_def Field_def by fastforce |
|
478 with ** have "x \<in> AboveS A" |
|
479 using ofilter_AboveS_Field[of A] OF by auto |
|
480 hence "(suc A,x) \<in> r" |
|
481 using suc_least_AboveS by auto |
|
482 moreover |
|
483 have "(x,suc A) \<in> r" using * under_def by auto |
|
484 ultimately show "x = suc A" |
|
485 using ANTISYM antisym_def[of r] by auto |
|
486 qed |
|
487 qed |
|
488 |
|
489 (* FIXME: needed? *) |
|
490 declare (in wo_rel) |
|
491 minim_in[simp] |
|
492 minim_inField[simp] |
|
493 minim_least[simp] |
|
494 under_ofilter[simp] |
|
495 underS_ofilter[simp] |
|
496 Field_ofilter[simp] |
|
497 ofilter_Under[simp] |
|
498 ofilter_UnderS[simp] |
|
499 ofilter_Int[simp] |
|
500 ofilter_Un[simp] |
|
501 |
|
502 abbreviation "worec \<equiv> wo_rel.worec" |
|
503 abbreviation "adm_wo \<equiv> wo_rel.adm_wo" |
|
504 abbreviation "isMinim \<equiv> wo_rel.isMinim" |
|
505 abbreviation "minim \<equiv> wo_rel.minim" |
|
506 abbreviation "max2 \<equiv> wo_rel.max2" |
|
507 abbreviation "supr \<equiv> wo_rel.supr" |
|
508 abbreviation "suc \<equiv> wo_rel.suc" |
|
509 abbreviation "ofilter \<equiv> wo_rel.ofilter" |
|
510 |
|
511 end |