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
     3     Copyright   2012
     4 
     5 Well-order relations.
     6 *)
     7 
     8 section \<open>Well-Order Relations\<close>
     9 
    10 theory Wellorder_Relation
    11 imports HOL.BNF_Wellorder_Relation Wellfounded_More
    12 begin
    13 
    14 context wo_rel
    15 begin
    16 
    17 subsection \<open>Auxiliaries\<close>
    18 
    19 lemma PREORD: "Preorder r"
    20 using WELL order_on_defs[of _ r] by auto
    21 
    22 lemma PARORD: "Partial_order r"
    23 using WELL order_on_defs[of _ r] by auto
    24 
    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
    30 
    31 
    32 subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
    33 
    34 lemma worec_unique_fixpoint:
    35 assumes ADM: "adm_wo H" and fp: "f = H f"
    36 shows "f = worec H"
    37 proof-
    38   have "adm_wf (r - Id) H"
    39   unfolding adm_wf_def
    40   using ADM adm_wo_def[of H] underS_def[of r] by auto
    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
    45 
    46 
    47 subsubsection \<open>Properties of max2\<close>
    48 
    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
    61 
    62 
    63 subsubsection \<open>Properties of minim\<close>
    64 
    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)
    68 
    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)
    73 
    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
    86 
    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
   122 
   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
   167 
   168 
   169 subsubsection \<open>Properties of supr\<close>
   170 
   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
   180 
   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
   190 
   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
   202 
   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)
   207 
   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
   218 
   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
   233 
   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
   241 
   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
   261 
   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
   288 
   289 
   290 subsubsection \<open>Properties of successor\<close>
   291 
   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)
   296 
   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
   311 
   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
   343 
   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
   366 
   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
   401 
   402 
   403 subsubsection \<open>Properties of order filters\<close>
   404 
   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
   418 
   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
   432 
   433 lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
   434 unfolding ofilter_def by blast
   435 
   436 lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
   437 unfolding ofilter_def by blast
   438 
   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
   442 
   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
   446 
   447 lemma ofilter_Union:
   448 "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
   449 unfolding ofilter_def by blast
   450 
   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
   454 
   455 
   456 subsubsection \<open>Other properties\<close>
   457 
   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
   482 
   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
   513 
   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]
   522 
   523 end
   524 
   525 abbreviation "worec \<equiv> wo_rel.worec"
   526 abbreviation "adm_wo \<equiv> wo_rel.adm_wo"
   527 abbreviation "isMinim \<equiv> wo_rel.isMinim"
   528 abbreviation "minim \<equiv> wo_rel.minim"
   529 abbreviation "max2 \<equiv> wo_rel.max2"
   530 abbreviation "supr \<equiv> wo_rel.supr"
   531 abbreviation "suc \<equiv> wo_rel.suc"
   532 
   533 end