src/HOL/BNF_Wellorder_Relation.thy
 author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 61799 4cf66f21b764 child 69593 3dda49e08b9d permissions -rw-r--r--
generalize more theorems to support enat and ennreal
1 (*  Title:      HOL/BNF_Wellorder_Relation.thy
2     Author:     Andrei Popescu, TU Muenchen
5 Well-order relations as needed by bounded natural functors.
6 *)
8 section \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close>
10 theory BNF_Wellorder_Relation
11 imports Order_Relation
12 begin
14 text\<open>In this section, we develop basic concepts and results pertaining
15 to well-order relations.  Note that we consider well-order relations
16 as {\em non-strict relations},
17 i.e., as containing the diagonals of their fields.\<close>
19 locale wo_rel =
20   fixes r :: "'a rel"
21   assumes WELL: "Well_order r"
22 begin
24 text\<open>The following context encompasses all this section. In other words,
25 for the whole section, we consider a fixed well-order relation @{term "r"}.\<close>
27 (* context wo_rel  *)
29 abbreviation under where "under \<equiv> Order_Relation.under r"
30 abbreviation underS where "underS \<equiv> Order_Relation.underS r"
31 abbreviation Under where "Under \<equiv> Order_Relation.Under r"
32 abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r"
33 abbreviation above where "above \<equiv> Order_Relation.above r"
34 abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
35 abbreviation Above where "Above \<equiv> Order_Relation.Above r"
36 abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r"
37 abbreviation ofilter where "ofilter \<equiv> Order_Relation.ofilter r"
38 lemmas ofilter_def = Order_Relation.ofilter_def[of r]
41 subsection \<open>Auxiliaries\<close>
43 lemma REFL: "Refl r"
44 using WELL order_on_defs[of _ r] by auto
46 lemma TRANS: "trans r"
47 using WELL order_on_defs[of _ r] by auto
49 lemma ANTISYM: "antisym r"
50 using WELL order_on_defs[of _ r] by auto
52 lemma TOTAL: "Total r"
53 using WELL order_on_defs[of _ r] by auto
55 lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
56 using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
58 lemma LIN: "Linear_order r"
59 using WELL well_order_on_def[of _ r] by auto
61 lemma WF: "wf (r - Id)"
62 using WELL well_order_on_def[of _ r] by auto
64 lemma cases_Total:
65 "\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
66              \<Longrightarrow> phi a b"
67 using TOTALS by auto
69 lemma cases_Total3:
70 "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
71               (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
72 using TOTALS by auto
75 subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
77 text\<open>Here we provide induction and recursion principles specific to {\em non-strict}
78 well-order relations.
79 Although minor variations of those for well-founded relations, they will be useful
80 for doing away with the tediousness of
81 having to take out the diagonal each time in order to switch to a well-founded relation.\<close>
83 lemma well_order_induct:
84 assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
85 shows "P a"
86 proof-
87   have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
88   using IND by blast
89   thus "P a" using WF wf_induct[of "r - Id" P a] by blast
90 qed
92 definition
93 worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
94 where
95 "worec F \<equiv> wfrec (r - Id) F"
97 definition
98 adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
99 where
100 "adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
102 lemma worec_fixpoint:
104 shows "worec H = H (worec H)"
105 proof-
106   let ?rS = "r - Id"
107   have "adm_wf (r - Id) H"
109   using ADM adm_wo_def[of H] underS_def[of r] by auto
110   hence "wfrec ?rS H = H (wfrec ?rS H)"
111   using WF wfrec_fixpoint[of ?rS H] by simp
112   thus ?thesis unfolding worec_def .
113 qed
116 subsection \<open>The notions of maximum, minimum, supremum, successor and order filter\<close>
118 text\<open>
119 We define the successor {\em of a set}, and not of an element (the latter is of course
120 a particular case).  Also, we define the maximum {\em of two elements}, \<open>max2\<close>,
121 and the minimum {\em of a set}, \<open>minim\<close> -- we chose these variants since we
122 consider them the most useful for well-orders.  The minimum is defined in terms of the
123 auxiliary relational operator \<open>isMinim\<close>.  Then, supremum and successor are
124 defined in terms of minimum as expected.
125 The minimum is only meaningful for non-empty sets, and the successor is only
126 meaningful for sets for which strict upper bounds exist.
127 Order filters for well-orders are also known as initial segments".\<close>
129 definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
130 where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
132 definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
133 where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
135 definition minim :: "'a set \<Rightarrow> 'a"
136 where "minim A \<equiv> THE b. isMinim A b"
138 definition supr :: "'a set \<Rightarrow> 'a"
139 where "supr A \<equiv> minim (Above A)"
141 definition suc :: "'a set \<Rightarrow> 'a"
142 where "suc A \<equiv> minim (AboveS A)"
145 subsubsection \<open>Properties of max2\<close>
147 lemma max2_greater_among:
148 assumes "a \<in> Field r" and "b \<in> Field r"
149 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
150 proof-
151   {assume "(a,b) \<in> r"
152    hence ?thesis using max2_def assms REFL refl_on_def
153    by (auto simp add: refl_on_def)
154   }
155   moreover
156   {assume "a = b"
157    hence "(a,b) \<in> r" using REFL  assms
158    by (auto simp add: refl_on_def)
159   }
160   moreover
161   {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
162    hence "(a,b) \<notin> r" using ANTISYM
163    by (auto simp add: antisym_def)
164    hence ?thesis using * max2_def assms REFL refl_on_def
165    by (auto simp add: refl_on_def)
166   }
167   ultimately show ?thesis using assms TOTAL
168   total_on_def[of "Field r" r] by blast
169 qed
171 lemma max2_greater:
172 assumes "a \<in> Field r" and "b \<in> Field r"
173 shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
174 using assms by (auto simp add: max2_greater_among)
176 lemma max2_among:
177 assumes "a \<in> Field r" and "b \<in> Field r"
178 shows "max2 a b \<in> {a, b}"
179 using assms max2_greater_among[of a b] by simp
181 lemma max2_equals1:
182 assumes "a \<in> Field r" and "b \<in> Field r"
183 shows "(max2 a b = a) = ((b,a) \<in> r)"
184 using assms ANTISYM unfolding antisym_def using TOTALS
185 by(auto simp add: max2_def max2_among)
187 lemma max2_equals2:
188 assumes "a \<in> Field r" and "b \<in> Field r"
189 shows "(max2 a b = b) = ((a,b) \<in> r)"
190 using assms ANTISYM unfolding antisym_def using TOTALS
191 unfolding max2_def by auto
194 subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>
196 lemma isMinim_unique:
197 assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
198 shows "a = a'"
199 proof-
200   {have "a \<in> B"
201    using MINIM isMinim_def by simp
202    hence "(a',a) \<in> r"
203    using MINIM' isMinim_def by simp
204   }
205   moreover
206   {have "a' \<in> B"
207    using MINIM' isMinim_def by simp
208    hence "(a,a') \<in> r"
209    using MINIM isMinim_def by simp
210   }
211   ultimately
212   show ?thesis using ANTISYM antisym_def[of r] by blast
213 qed
215 lemma Well_order_isMinim_exists:
216 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
217 shows "\<exists>b. isMinim B b"
218 proof-
219   from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
220   *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
221   show ?thesis
222   proof(simp add: isMinim_def, rule exI[of _ b], auto)
223     show "b \<in> B" using * by simp
224   next
225     fix b' assume As: "b' \<in> B"
226     hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
227     (*  *)
228     from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
229     moreover
230     {assume "b' = b"
231      hence "(b,b') \<in> r"
232      using ** REFL by (auto simp add: refl_on_def)
233     }
234     moreover
235     {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
236      hence "(b,b') \<in> r"
237      using ** TOTAL by (auto simp add: total_on_def)
238     }
239     ultimately show "(b,b') \<in> r" by blast
240   qed
241 qed
243 lemma minim_isMinim:
244 assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
245 shows "isMinim B (minim B)"
246 proof-
247   let ?phi = "(\<lambda> b. isMinim B b)"
248   from assms Well_order_isMinim_exists
249   obtain b where *: "?phi b" by blast
250   moreover
251   have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
252   using isMinim_unique * by auto
253   ultimately show ?thesis
254   unfolding minim_def using theI[of ?phi b] by blast
255 qed
257 subsubsection\<open>Properties of minim\<close>
259 lemma minim_in:
260 assumes "B \<le> Field r" and "B \<noteq> {}"
261 shows "minim B \<in> B"
262 proof-
263   from minim_isMinim[of B] assms
264   have "isMinim B (minim B)" by simp
265   thus ?thesis by (simp add: isMinim_def)
266 qed
268 lemma minim_inField:
269 assumes "B \<le> Field r" and "B \<noteq> {}"
270 shows "minim B \<in> Field r"
271 proof-
272   have "minim B \<in> B" using assms by (simp add: minim_in)
273   thus ?thesis using assms by blast
274 qed
276 lemma minim_least:
277 assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
278 shows "(minim B, b) \<in> r"
279 proof-
280   from minim_isMinim[of B] assms
281   have "isMinim B (minim B)" by auto
282   thus ?thesis by (auto simp add: isMinim_def IN)
283 qed
285 lemma equals_minim:
286 assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
287         LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
288 shows "a = minim B"
289 proof-
290   from minim_isMinim[of B] assms
291   have "isMinim B (minim B)" by auto
292   moreover have "isMinim B a" using IN LEAST isMinim_def by auto
293   ultimately show ?thesis
294   using isMinim_unique by auto
295 qed
297 subsubsection\<open>Properties of successor\<close>
299 lemma suc_AboveS:
300 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
301 shows "suc B \<in> AboveS B"
302 proof(unfold suc_def)
303   have "AboveS B \<le> Field r"
304   using AboveS_Field[of r] by auto
305   thus "minim (AboveS B) \<in> AboveS B"
306   using assms by (simp add: minim_in)
307 qed
309 lemma suc_greater:
310 assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
311         IN: "b \<in> B"
312 shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
313 proof-
314   from assms suc_AboveS
315   have "suc B \<in> AboveS B" by simp
316   with IN AboveS_def[of r] show ?thesis by simp
317 qed
319 lemma suc_least_AboveS:
320 assumes ABOVES: "a \<in> AboveS B"
321 shows "(suc B,a) \<in> r"
322 proof(unfold suc_def)
323   have "AboveS B \<le> Field r"
324   using AboveS_Field[of r] by auto
325   thus "(minim (AboveS B),a) \<in> r"
326   using assms minim_least by simp
327 qed
329 lemma suc_inField:
330 assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
331 shows "suc B \<in> Field r"
332 proof-
333   have "suc B \<in> AboveS B" using suc_AboveS assms by simp
334   thus ?thesis
335   using assms AboveS_Field[of r] by auto
336 qed
338 lemma equals_suc_AboveS:
339 assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
340         MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
341 shows "a = suc B"
342 proof(unfold suc_def)
343   have "AboveS B \<le> Field r"
344   using AboveS_Field[of r B] by auto
345   thus "a = minim (AboveS B)"
346   using assms equals_minim
347   by simp
348 qed
350 lemma suc_underS:
351 assumes IN: "a \<in> Field r"
352 shows "a = suc (underS a)"
353 proof-
354   have "underS a \<le> Field r"
355   using underS_Field[of r] by auto
356   moreover
357   have "a \<in> AboveS (underS a)"
358   using in_AboveS_underS IN by fast
359   moreover
360   have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
361   proof(clarify)
362     fix a'
363     assume *: "a' \<in> AboveS (underS a)"
364     hence **: "a' \<in> Field r"
365     using AboveS_Field by fast
366     {assume "(a,a') \<notin> r"
367      hence "a' = a \<or> (a',a) \<in> r"
368      using TOTAL IN ** by (auto simp add: total_on_def)
369      moreover
370      {assume "a' = a"
371       hence "(a,a') \<in> r"
372       using REFL IN ** by (auto simp add: refl_on_def)
373      }
374      moreover
375      {assume "a' \<noteq> a \<and> (a',a) \<in> r"
376       hence "a' \<in> underS a"
377       unfolding underS_def by simp
378       hence "a' \<notin> AboveS (underS a)"
379       using AboveS_disjoint by fast
380       with * have False by simp
381      }
382      ultimately have "(a,a') \<in> r" by blast
383     }
384     thus  "(a, a') \<in> r" by blast
385   qed
386   ultimately show ?thesis
387   using equals_suc_AboveS by auto
388 qed
391 subsubsection \<open>Properties of order filters\<close>
393 lemma under_ofilter:
394 "ofilter (under a)"
395 proof(unfold ofilter_def under_def, auto simp add: Field_def)
396   fix aa x
397   assume "(aa,a) \<in> r" "(x,aa) \<in> r"
398   thus "(x,a) \<in> r"
399   using TRANS trans_def[of r] by blast
400 qed
402 lemma underS_ofilter:
403 "ofilter (underS a)"
404 proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
405   fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
406   thus False
407   using ANTISYM antisym_def[of r] by blast
408 next
409   fix aa x
410   assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
411   thus "(x,a) \<in> r"
412   using TRANS trans_def[of r] by blast
413 qed
415 lemma Field_ofilter:
416 "ofilter (Field r)"
417 by(unfold ofilter_def under_def, auto simp add: Field_def)
419 lemma ofilter_underS_Field:
420 "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
421 proof
422   assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
423   thus "ofilter A"
424   by (auto simp: underS_ofilter Field_ofilter)
425 next
426   assume *: "ofilter A"
427   let ?One = "(\<exists>a\<in>Field r. A = underS a)"
428   let ?Two = "(A = Field r)"
429   show "?One \<or> ?Two"
430   proof(cases ?Two, simp)
431     let ?B = "(Field r) - A"
432     let ?a = "minim ?B"
433     assume "A \<noteq> Field r"
434     moreover have "A \<le> Field r" using * ofilter_def by simp
435     ultimately have 1: "?B \<noteq> {}" by blast
436     hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
437     have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
438     hence 4: "?a \<notin> A" by blast
439     have 5: "A \<le> Field r" using * ofilter_def by auto
440     (*  *)
441     moreover
442     have "A = underS ?a"
443     proof
444       show "A \<le> underS ?a"
445       proof(unfold underS_def, auto simp add: 4)
446         fix x assume **: "x \<in> A"
447         hence 11: "x \<in> Field r" using 5 by auto
448         have 12: "x \<noteq> ?a" using 4 ** by auto
449         have 13: "under x \<le> A" using * ofilter_def ** by auto
450         {assume "(x,?a) \<notin> r"
451          hence "(?a,x) \<in> r"
452          using TOTAL total_on_def[of "Field r" r]
453                2 4 11 12 by auto
454          hence "?a \<in> under x" using under_def[of r] by auto
455          hence "?a \<in> A" using ** 13 by blast
456          with 4 have False by simp
457         }
458         thus "(x,?a) \<in> r" by blast
459       qed
460     next
461       show "underS ?a \<le> A"
462       proof(unfold underS_def, auto)
463         fix x
464         assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
465         hence 11: "x \<in> Field r" using Field_def by fastforce
466          {assume "x \<notin> A"
467           hence "x \<in> ?B" using 11 by auto
468           hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
469           hence False
470           using ANTISYM antisym_def[of r] ** *** by auto
471          }
472         thus "x \<in> A" by blast
473       qed
474     qed
475     ultimately have ?One using 2 by blast
476     thus ?thesis by simp
477   qed
478 qed
480 lemma ofilter_UNION:
481 "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union>i \<in> I. A i)"
482 unfolding ofilter_def by blast
484 lemma ofilter_under_UNION:
485 assumes "ofilter A"
486 shows "A = (\<Union>a \<in> A. under a)"
487 proof
488   have "\<forall>a \<in> A. under a \<le> A"
489   using assms ofilter_def by auto
490   thus "(\<Union>a \<in> A. under a) \<le> A" by blast
491 next
492   have "\<forall>a \<in> A. a \<in> under a"
493   using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
494   thus "A \<le> (\<Union>a \<in> A. under a)" by blast
495 qed
497 subsubsection\<open>Other properties\<close>
499 lemma ofilter_linord:
500 assumes OF1: "ofilter A" and OF2: "ofilter B"
501 shows "A \<le> B \<or> B \<le> A"
502 proof(cases "A = Field r")
503   assume Case1: "A = Field r"
504   hence "B \<le> A" using OF2 ofilter_def by auto
505   thus ?thesis by simp
506 next
507   assume Case2: "A \<noteq> Field r"
508   with ofilter_underS_Field OF1 obtain a where
509   1: "a \<in> Field r \<and> A = underS a" by auto
510   show ?thesis
511   proof(cases "B = Field r")
512     assume Case21: "B = Field r"
513     hence "A \<le> B" using OF1 ofilter_def by auto
514     thus ?thesis by simp
515   next
516     assume Case22: "B \<noteq> Field r"
517     with ofilter_underS_Field OF2 obtain b where
518     2: "b \<in> Field r \<and> B = underS b" by auto
519     have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
520     using 1 2 TOTAL total_on_def[of _ r] by auto
521     moreover
522     {assume "a = b" with 1 2 have ?thesis by auto
523     }
524     moreover
525     {assume "(a,b) \<in> r"
526      with underS_incr[of r] TRANS ANTISYM 1 2
527      have "A \<le> B" by auto
528      hence ?thesis by auto
529     }
530     moreover
531      {assume "(b,a) \<in> r"
532      with underS_incr[of r] TRANS ANTISYM 1 2
533      have "B \<le> A" by auto
534      hence ?thesis by auto
535     }
536     ultimately show ?thesis by blast
537   qed
538 qed
540 lemma ofilter_AboveS_Field:
541 assumes "ofilter A"
542 shows "A \<union> (AboveS A) = Field r"
543 proof
544   show "A \<union> (AboveS A) \<le> Field r"
545   using assms ofilter_def AboveS_Field[of r] by auto
546 next
547   {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
548    {fix y assume ***: "y \<in> A"
549     with ** have 1: "y \<noteq> x" by auto
550     {assume "(y,x) \<notin> r"
551      moreover
552      have "y \<in> Field r" using assms ofilter_def *** by auto
553      ultimately have "(x,y) \<in> r"
554      using 1 * TOTAL total_on_def[of _ r] by auto
555      with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
556      with ** have False by contradiction
557     }
558     hence "(y,x) \<in> r" by blast
559     with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
560    }
561    with * have "x \<in> AboveS A" unfolding AboveS_def by auto
562   }
563   thus "Field r \<le> A \<union> (AboveS A)" by blast
564 qed
566 lemma suc_ofilter_in:
567 assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
568         REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
569 shows "b \<in> A"
570 proof-
571   have *: "suc A \<in> Field r \<and> b \<in> Field r"
572   using WELL REL well_order_on_domain[of "Field r"] by auto
573   {assume **: "b \<notin> A"
574    hence "b \<in> AboveS A"
575    using OF * ofilter_AboveS_Field by auto
576    hence "(suc A, b) \<in> r"
577    using suc_least_AboveS by auto
578    hence False using REL DIFF ANTISYM *
579    by (auto simp add: antisym_def)
580   }
581   thus ?thesis by blast
582 qed
584 end (* context wo_rel *)
586 end