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