1 theory WQO_Finite_Lists

     2 imports "Seq"

     3 begin

     4 

     5 subsection {* Auxiliary Lemmas *}

     6 

     7 lemma funpow_non_decreasing:

     8   fixes f :: "'a::order \<Rightarrow> 'a"

     9   assumes "\<forall>i\<ge>n. f i \<ge> i"

    10   shows "(f ^^ i) n \<ge> n"

    11   using assms by (induct i) auto

    12 

    13 lemma funpow_mono:

    14   assumes "\<forall>i\<ge>n::nat. f i > i" and "j > i"

    15   shows "(f ^^ j) n > (f ^^ i) n"

    16 using assms(2)

    17 proof (induct "j - i" arbitrary: i j)

    18   case 0 thus ?case by simp

    19 next

    20   case (Suc m)

    21   then obtain j' where j: "j = Suc j'" by (cases j) auto

    22   show ?case

    23   proof (cases "i < j'")

    24     case True

    25     with Suc(1)[of j'] and Suc(2)[unfolded j]

    26       have "(f ^^ j') n > (f ^^ i) n" by simp

    27     moreover have "(f ^^ j) n > (f ^^ j') n"

    28     proof -

    29       have "(f ^^ j) n = f ((f ^^ j') n)" by (simp add: j)

    30       also have "\<dots> > (f ^^ j') n" using assms and funpow_non_decreasing[of n f j'] by force

    31       finally show ?thesis .

    32     qed

    33     ultimately show ?thesis by auto

    34   next

    35     case False

    36     with Suc have i: "i = j'" unfolding j by (induct i) auto

    37     show ?thesis unfolding i j using assms and funpow_non_decreasing[of n f j'] by force

    38   qed

    39 qed

    40 

    41 

    42 subsection {* Basic Definitions *}

    43 

    44 definition reflp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where

    45   "reflp_on P A \<equiv> \<forall>a\<in>A. P a a"

    46 

    47 lemma reflp_onI [Pure.intro]:

    48   "(\<And>a. a \<in> A \<Longrightarrow> P a a) \<Longrightarrow> reflp_on P A"

    49   unfolding reflp_on_def by blast

    50 

    51 definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where

    52   "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c"

    53 

    54 lemma transp_onI [Pure.intro]:

    55   "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"

    56   unfolding transp_on_def by blast

    57 

    58 definition goodp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a seq \<Rightarrow> bool" where

    59   "goodp P f \<equiv> \<exists>i j. i < j \<and> P\<^sup>=\<^sup>= (f i) (f j)"

    60 

    61 abbreviation bad where "bad P f \<equiv> \<not> goodp P f"

    62 

    63 definition wqo_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where

    64   "wqo_on P A \<equiv> reflp_on P A \<and> transp_on P A \<and> (\<forall>f. (\<forall>i. f i \<in> A) \<longrightarrow> goodp P f)"

    65 

    66 lemma wqo_onI [Pure.intro]:

    67   "\<lbrakk>reflp_on P A; transp_on P A; \<And>f. \<forall>i. f i \<in> A \<Longrightarrow> goodp P f\<rbrakk> \<Longrightarrow> wqo_on P A"

    68   unfolding wqo_on_def by blast

    69 

    70 lemma reflp_on_reflclp [simp]:

    71   assumes "reflp_on P A" and "a \<in> A" and "b \<in> A"

    72   shows "P\<^sup>=\<^sup>= a b = P a b"

    73   using assms by (auto simp: reflp_on_def)

    74 

    75 lemma transp_on_tranclp:

    76   assumes "transp_on P A"

    77   shows "(\<lambda>x y. x \<in> A \<and> y \<in> A \<and> P x y)\<^sup>+\<^sup>+ a b \<longleftrightarrow> a \<in> A \<and> b \<in> A \<and> P a b"

    78     (is "?lhs = ?rhs")

    79   by (rule iffI, induction rule: tranclp.induct)

    80      (insert assms, auto simp: transp_on_def)

    81 

    82 lemma wqo_on_imp_reflp_on:

    83   "wqo_on P A \<Longrightarrow> reflp_on P A"

    84   by (auto simp: wqo_on_def)

    85 

    86 lemma wqo_on_imp_transp_on:

    87   "wqo_on P A \<Longrightarrow> transp_on P A"

    88   by (auto simp: wqo_on_def)

    89 

    90 lemma wqo_on_imp_goodp:

    91   "wqo_on P A \<Longrightarrow> \<forall>i. f i \<in> A \<Longrightarrow> goodp P f"

    92   by (auto simp: wqo_on_def)

    93 

    94 lemma reflp_on_converse:

    95   "reflp_on P A \<Longrightarrow> reflp_on P\<inverse>\<inverse> A"

    96   unfolding reflp_on_def by blast

    97 

    98 lemma transp_on_converse:

    99   "transp_on P A \<Longrightarrow> transp_on P\<inverse>\<inverse> A"

   100   unfolding transp_on_def by blast

   101 

   102 subsection {* Dickson's Lemma *}

   103 

   104 text {*When two sets are wqo, then their cartesian product is wqo.*}

   105 

   106 definition

   107   prod_le :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"

   108 where

   109   "prod_le P1 P2 \<equiv> \<lambda>(p1, p2) (q1, q2). P1 p1 q1 \<and> P2 p2 q2"

   110 

   111 lemma wqo_on_Sigma:

   112   fixes A1 :: "'a set" and A2 :: "'b set"

   113   assumes "wqo_on P1 A1" and "wqo_on P2 A2"

   114   shows "wqo_on (prod_le P1 P2) (A1 \<times> A2)"

   115     (is "wqo_on ?P ?A")

   116 proof

   117   show "reflp_on ?P ?A"

   118     using assms by (auto simp: wqo_on_def reflp_on_def prod_le_def)

   119 next

   120   from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def)

   121   thus "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast

   122 next

   123   fix g :: "('a \<times> 'b) seq"

   124   let ?p = "\<lambda>i. fst (g i)"

   125   let ?q = "\<lambda>i. snd (g i)"

   126   assume g: "\<forall>i. g i \<in> ?A"

   127   have p: "\<forall>i. ?p i \<in> A1"

   128   proof

   129     fix i

   130     from g have "g i \<in> ?A" by simp

   131     thus "?p i \<in> A1" by auto

   132   qed

   133   have q: "\<forall>i. ?q i \<in> A2"

   134   proof

   135     fix i

   136     from g have "g i \<in> ?A" by simp

   137     thus "?q i \<in> A2" by auto

   138   qed

   139   let ?T = "{m. \<forall>n>m. \<not> (P1 (?p m) (?p n))}"

   140   have "finite ?T"

   141   proof (rule ccontr)

   142     assume "infinite ?T"

   143     hence "INFM m. m \<in> ?T" unfolding INFM_iff_infinite by simp

   144     then interpret infinitely_many "\<lambda>m. m \<in> ?T" by (unfold_locales) assumption

   145     let ?p' = "\<lambda>i. ?p (index i)"

   146     have p': "\<forall>i. ?p' i \<in> A1" using p by auto

   147     have "bad P1 ?p'"

   148     proof

   149       assume "goodp P1 ?p'"

   150       then obtain i j :: nat where "i < j"

   151         and "P1\<^sup>=\<^sup>= (?p' i) (?p' j)" by (auto simp: goodp_def)

   152       hence "P1 (?p' i) (?p' j)"

   153         using p' and reflp_on_reflclp[OF wqo_on_imp_reflp_on[OF assms(1)]] by simp

   154       moreover from index_ordered_less[OF `i < j`] have "index j > index i" .

   155       moreover from index_p have "index i \<in> ?T" by simp

   156       ultimately show False by blast

   157     qed

   158     with assms(1) show False using p' by (auto simp: wqo_on_def)

   159   qed

   160   then obtain n where "\<forall>r\<ge>n. r \<notin> ?T"

   161     using infinite_nat_iff_unbounded_le[of "?T"] by auto

   162   hence "\<forall>i\<in>{n..}. \<exists>j>i. P1 (?p i) (?p j)" by blast

   163   with p have "\<forall>i\<in>{n..}. \<exists>j>i. ?p j \<in> A1 \<and> ?p i \<in> A1 \<and> P1 (?p i) (?p j)" by auto

   164   from bchoice[OF this] obtain f :: "nat seq"

   165     where 1: "\<forall>i\<ge>n. i < f i \<and> ?p i \<in> A1 \<and> ?p (f i) \<in> A1 \<and> P1 (?p i) (?p (f i))" by blast

   166   from stepfun_imp_chainp[of n f "\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y" ?p, OF this]

   167     have chain: "chainp (\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y) (\<lambda>i. ?p ((f^^i) n))" .

   168   let ?f = "\<lambda>i. (f^^i) n"

   169   from 1 have inc: "\<forall>i\<ge>n. f i > i" by simp

   170   from wqo_on_imp_goodp[OF assms(2), of "?q \<circ> ?f"] and q

   171     obtain i j where "\<And>i. ?q (?f i) \<in> A2" and "j > i" and "P2\<^sup>=\<^sup>= (?q (?f i)) (?q (?f j))"

   172     by (auto simp: goodp_def)

   173   hence "P2 (?q (?f i)) (?q (?f j))"

   174     using reflp_on_reflclp[OF wqo_on_imp_reflp_on[OF assms(2)]] by simp

   175   moreover from funpow_mono[OF inc `j > i`] have "?f j > ?f i" .

   176   moreover from chainp_imp_tranclp[of "\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y", OF chain `j > i`]

   177     have "P1 (?p (?f i)) (?p (?f j))"

   178     unfolding transp_on_tranclp[OF wqo_on_imp_transp_on[OF assms(1)]] by simp

   179   ultimately have "\<exists>i j. j > i \<and> P1 (?p i) (?p j) \<and> P2 (?q i) (?q j)" by auto

   180   thus "goodp ?P g" by (auto simp: split_def goodp_def prod_le_def)

   181 qed

   182 

   183 subsection {* Higman's Lemma *}

   184 

   185 inductive

   186   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   187 where

   188   emb0 [intro]: "emb [] y"

   189 | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)"

   190 | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)"

   191 

   192 lemma emb_refl [simp]: "emb xs xs"

   193   by (induct xs) auto

   194 

   195 lemma emb_Nil2 [simp]: "emb y [] \<Longrightarrow> y = []"

   196   by (cases rule: emb.cases) auto

   197 

   198 lemma emb_right [intro]:

   199   assumes a: "emb x y"

   200   shows "emb x (y @ y')"

   201 using a 

   202 by (induct arbitrary: y') (auto)

   203 

   204 lemma emb_left [intro]:

   205   assumes a: "emb x y"

   206   shows "emb x (y' @ y)"

   207 using a by (induct y') (auto)

   208 

   209 lemma emb_appendI [intro]:

   210   assumes a: "emb x x'"

   211   and     b: "emb y y'"

   212   shows "emb (x @ y) (x' @ y')"

   213 using a b by (induct) (auto)

   214 

   215 lemma emb_cons_leftD:

   216   assumes "emb (a # x) y"

   217   shows "\<exists>y1 y2. y = y1 @ [a] @ y2 \<and> emb x y2"

   218 using assms

   219 apply(induct x\<equiv>"a # x" y\<equiv>"y" arbitrary: a x y)

   220 apply(auto)

   221 apply(metis append_Cons)

   222 done

   223 

   224 lemma emb_append_leftD:

   225   assumes "emb (x1 @ x2) y"

   226   shows "\<exists>y1 y2. y = y1 @ y2 \<and> emb x1 y1 \<and> emb x2 y2"

   227 using assms

   228 apply(induct x1 arbitrary: x2 y)

   229 apply(auto)

   230 apply(drule emb_cons_leftD)

   231 apply(auto)

   232 apply(drule_tac x="x2" in meta_spec)

   233 apply(drule_tac x="y2" in meta_spec)

   234 apply(auto)

   235 apply(rule_tac x="y1 @ (a # y1a)" in exI)

   236 apply(rule_tac x="y2a" in exI)

   237 apply(auto)

   238 done

   239 

   240 lemma emb_trans:

   241   assumes a: "emb x1 x2"

   242   and     b: "emb x2 x3"

   243   shows "emb x1 x3"

   244 using a b

   245 apply(induct arbitrary: x3)

   246 apply(metis emb0)

   247 apply(metis emb_cons_leftD emb_left)

   248 apply(drule_tac emb_cons_leftD)

   249 apply(auto)

   250 done

   251 

   252 lemma empty_imp_goodp_emb [simp]:

   253   assumes "f i = []"

   254   shows "goodp emb f"

   255 proof (rule ccontr)

   256   assume "bad emb f"

   257   moreover have "(emb)\<^sup>=\<^sup>= (f i) (f (Suc i))"

   258     unfolding assms by auto

   259   ultimately show False

   260     unfolding goodp_def by auto

   261 qed

   262 

   263 lemma bad_imp_not_empty:

   264   "bad emb f \<Longrightarrow> f i \<noteq> []"

   265   by auto

   266 

   267 text {*Replace the elements of an infinite sequence, starting from a given

   268 position, by those of another infinite sequence.*}

   269 definition repl :: "nat \<Rightarrow> 'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where

   270   "repl i f g \<equiv> \<lambda>j. if j \<ge> i then g j else f j"

   271 

   272 lemma repl_0 [simp]:

   273   "repl 0 f g = g"

   274   by (simp add: repl_def)

   275 

   276 lemma repl_simps [simp]:

   277   "j \<ge> i \<Longrightarrow> repl i f g j = g j"

   278   "j < i \<Longrightarrow> repl i f g j = f j"

   279   by (auto simp: repl_def)

   280 

   281 lemma repl_ident [simp]:

   282    "repl i f f = f"

   283    by (auto simp: repl_def)

   284 

   285 lemma repl_repl_ident [simp]:

   286   "repl n f (repl n g h) = repl n f h"

   287   by (auto simp: repl_def)

   288 

   289 lemma repl_repl_ident' [simp]:

   290   "repl n (repl n f g) h = repl n f h"

   291   by (auto simp: repl_def)

   292 

   293 lemma bad_emb_repl:

   294   assumes "bad emb f"

   295     and "bad emb g"

   296     and "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (g i) (f j)"

   297   shows "bad emb (repl n f g)" (is "bad emb ?f")

   298 proof (rule ccontr)

   299   presume "goodp emb ?f"

   300   then obtain i j where "i < j"

   301     and good: "emb\<^sup>=\<^sup>= (?f i) (?f j)" by (auto simp: goodp_def)

   302   {

   303     assume "j < n"

   304     with `i < j` and good have "emb\<^sup>=\<^sup>= (f i) (f j)" by simp

   305     with assms(1) have False using `i < j` by (auto simp: goodp_def)

   306   } moreover {

   307     assume "n \<le> i"

   308     with `i < j` and good have "i - n < j - n"

   309       and "emb\<^sup>=\<^sup>= (g i) (g j)" by auto

   310     with assms(2) have False by (auto simp: goodp_def)

   311   } moreover {

   312     assume "i < n" and "n \<le> j"

   313     with assms(3) obtain k where "k \<ge> n" and emb: "emb (g j) (f k)" by blast

   314     from `i < j` and `i < n` and `n \<le> j` and good

   315       have "emb\<^sup>=\<^sup>= (f i) (g j)" by auto

   316     hence "emb\<^sup>=\<^sup>= (f i) (f k)"

   317     proof

   318       assume fi: "f i = g j"

   319       with emb_refl have "emb (f i) (f i)" by blast

   320       with emb_trans[OF emb] show "emb\<^sup>=\<^sup>= (f i) (f k)" by (auto simp: fi)

   321     next

   322       assume "emb (f i) (g j)"

   323       from emb_trans[OF this emb] show "emb\<^sup>=\<^sup>= (f i) (f k)" by auto

   324     qed

   325     with `i < n` and `n \<le> k` and assms(1) have False by (auto simp: goodp_def)

   326   } ultimately show False using `i < j` by arith

   327 qed simp

   328 

   329 text {*A \emph{minimal bad prefix} of an infinite sequence, is a

   330 prefix of its first @{text n} elements, such that every subsequence (of subsets)

   331 starting with the same @{text n} elements is good, whenever the @{text n}-th

   332 element is replaced by a proper subset of itself.*}

   333 definition mbp :: "'a list seq \<Rightarrow> nat \<Rightarrow> bool" where

   334   "mbp f n \<equiv>

   335     \<forall>g. (\<forall>i<n. g i = f i) \<and> g n \<noteq> f n \<and> emb (g n) (f n) \<and> (\<forall>i\<ge>n. \<exists>j\<ge>n. emb (g i) (f j))

   336     \<longrightarrow> goodp emb g"

   337 

   338 lemma ex_repl_conv:

   339   "(\<exists>j\<ge>n. P (repl n f g j)) \<longleftrightarrow> (\<exists>j\<ge>n. P (g j))"

   340   by auto

   341 

   342 lemma emb_strict_length:

   343   assumes a: "emb x y" "x \<noteq> y" 

   344   shows "length x < length y"

   345   using a by (induct) (auto simp add: less_Suc_eq)

   346 

   347 lemma emb_wf:

   348   shows "wf {(x, y). emb x y \<and> x \<noteq> y}"

   349 proof -

   350   have "wf (measure length)" by simp

   351   moreover

   352   have "{(x, y). emb x y \<and> x \<noteq> y} \<subseteq> measure length"

   353     unfolding measure_def by (auto simp add: emb_strict_length)

   354   ultimately 

   355   show "wf {(x, y). emb x y \<and> x \<noteq> y}" by (rule wf_subset)

   356 qed

   357 

   358 lemma minimal_bad_element:

   359   fixes f :: "'a list seq"

   360   assumes "mbp f n"

   361     and "bad emb f"

   362   shows "\<exists>M.

   363     (\<forall>i\<le>n. M i = f i) \<and>

   364     emb (M (Suc n)) (f (Suc n)) \<and>

   365     (\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb ((repl (Suc n) f M) i) (f j)) \<and>

   366     bad emb (repl (Suc n) f M) \<and>

   367     mbp (repl (Suc n) f M) (Suc n)"

   368 using assms

   369 proof (induct "f (Suc n)" arbitrary: f n rule: wf_induct_rule[OF emb_wf])

   370   case (1 g)

   371   show ?case

   372   proof (cases "mbp g (Suc n)")

   373     case True

   374     let ?g = "repl (Suc n) g g"

   375     have "\<forall>i\<le>n. ?g i = g i" by simp

   376     moreover have "emb (g (Suc n)) (g (Suc n))" by simp

   377     moreover have "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb ((repl (Suc n) g g) i) (g j)" by auto

   378     moreover from `bad emb g`

   379       have "bad emb (repl (Suc n) g g)" by simp

   380     moreover from True have "mbp (repl (Suc n) g g) (Suc n)" by simp

   381     ultimately show ?thesis by blast

   382   next

   383     case False

   384     then obtain h where less: "\<forall>i<Suc n. h i = g i"

   385       and emb: "(h (Suc n), g (Suc n)) \<in> {(x, y). emb x y \<and> x \<noteq> y}"

   386         (is "_ \<in> ?emb")

   387       and greater: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (h i) (g j)"

   388       and bad: "bad emb h"

   389       unfolding mbp_def by blast

   390     let ?g = "repl (Suc n) g h"

   391     from emb have emb': "(?g (Suc n), g (Suc n)) \<in> ?emb" by simp

   392     have mbp: "mbp ?g n"

   393     proof (unfold mbp_def, intro allI impI, elim conjE)

   394       fix e

   395       assume "\<forall>i<n. e i = ?g i"

   396       hence 1: "\<forall>i<n. e i = g i" by auto

   397       assume "e n \<noteq> ?g n"

   398       hence 2: "e n \<noteq> ?g n" .

   399       assume "emb (e n) (?g n)"

   400       hence 3: "emb (e n) (g n)" by auto

   401       assume *: "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (e i) (?g j)"

   402       have 4: "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (e i) (g j)"

   403       proof (intro allI impI)

   404         fix i assume "n \<le> i"

   405         with * obtain j where "j \<ge> n"

   406           and **: "emb (e i) (?g j)" by auto

   407         show "\<exists>j\<ge>n. emb (e i) (g j)"

   408         proof (cases "j \<le> n")

   409           case True with ** show ?thesis

   410             using `j \<ge> n` by auto

   411         next

   412           case False

   413           with `j \<ge> n` have "j \<ge> Suc n" by auto

   414           with ** have "emb (e i) (h j)" by auto

   415           with greater obtain k where "k \<ge> Suc n"

   416             and "emb (h j) (g k)" using `j \<ge> Suc n` by auto

   417           with `emb (e i) (h j)` have "emb (e i) (g k)" by (auto intro: emb_trans)

   418           moreover from `k \<ge> Suc n` have "k \<ge> n" by auto

   419           ultimately show ?thesis by blast

   420         qed

   421       qed

   422       from `mbp g n`[unfolded mbp_def] and 1 and 2 and 3 and 4

   423         show "goodp emb e" by auto

   424     qed

   425     have bad: "bad emb ?g"

   426       using bad_emb_repl[OF `bad emb g` `bad emb h`, of "Suc n",

   427       OF greater] .

   428     let ?g' = "repl (Suc n) g"

   429     from 1(1)[of ?g n, OF emb' mbp bad] obtain M

   430       where "\<forall>i\<le>n. M i = g i"

   431       and "emb (M (Suc n)) (?g' h (Suc n))"

   432       and *: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g' M i) (h j)"

   433       and "bad emb (?g' M)"

   434       and "mbp (?g' M) (Suc n)"

   435       unfolding ex_repl_conv by auto

   436     moreover with emb have "emb (M (Suc n)) (g (Suc n))" by (auto intro: emb_trans)

   437     moreover have "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g' M i) (g j)"

   438     proof (intro allI impI)

   439       fix i assume "Suc n \<le> i"

   440       with * obtain j where "j \<ge> Suc n" and "emb (?g' M i) (h j)" by auto

   441       hence "j \<ge> Suc n" by auto

   442       from greater and `j \<ge> Suc n` obtain k where "k \<ge> Suc n"

   443         and "emb (h j) (g k)" by auto

   444       with `emb (?g' M i) (h j)` show "\<exists>j\<ge>Suc n. emb (?g' M i) (g j)" by (blast intro: emb_trans)

   445     qed

   446     ultimately show ?thesis by blast

   447   qed

   448 qed

   449 

   450 lemma choice2:

   451   "\<forall>x y. P x y \<longrightarrow> (\<exists>z. Q x y z) \<Longrightarrow> \<exists>f. \<forall>x y. P x y \<longrightarrow> Q x y (f x y)"

   452   using bchoice[of "{(x, y). P x y}" "\<lambda>(x, y) z. Q x y z"] by force

   453 

   454 fun minimal_bad_seq :: "('a seq \<Rightarrow> nat \<Rightarrow> 'a seq) \<Rightarrow> 'a seq \<Rightarrow> nat \<Rightarrow> 'a seq" where

   455   "minimal_bad_seq A f 0 = A f 0"

   456 | "minimal_bad_seq A f (Suc n) = (

   457     let g = minimal_bad_seq A f n in

   458     repl (Suc n) g (A g n))"

   459 

   460 lemma bad_imp_mbp:

   461   assumes "bad emb f"

   462   shows "\<exists>g. (\<forall>i. \<exists>j. emb (g i) (f j)) \<and> mbp g 0 \<and> bad emb g"

   463 using assms

   464 proof (induct "f 0" arbitrary: f rule: wf_induct_rule[OF emb_wf])

   465   case (1 g)

   466   show ?case

   467   proof (cases "mbp g 0")

   468     case True with 1 show ?thesis by (blast intro: emb_refl)

   469   next

   470     case False

   471     then obtain h where less: "\<forall>i<0. h i = g i"

   472       and emb: "(h 0, g 0) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")

   473       and greater: "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (h i) (g j)"

   474       and bad: "bad emb h"

   475       unfolding mbp_def by auto

   476     from 1(1)[of h, OF emb bad] obtain e

   477       where "\<forall>i. \<exists>j. emb (e i) (h j)" and "mbp e 0" and "bad emb e"

   478       by auto

   479     moreover with greater have "\<forall>i. \<exists>j. emb (e i) (g j)" by (force intro: emb_trans)

   480     ultimately show ?thesis by blast

   481   qed

   482 qed

   483 

   484 lemma repl_1 [simp]:

   485   assumes "f 0 = g 0"

   486   shows "repl (Suc 0) f g = g"

   487 proof

   488   fix i show "repl (Suc 0) f g i = g i"

   489     by (induct i) (simp_all add: assms)

   490 qed

   491 

   492 lemma bad_repl:

   493   assumes "\<forall>i. f i \<ge> f 0" and "\<forall>i j. i > j \<longrightarrow> f i > f j"

   494     and "bad P (repl (f 0) A B)" (is "bad P ?A")

   495   shows "bad P (B \<circ> f)"

   496 proof

   497   assume "goodp P (B \<circ> f)"

   498   then obtain i j where "i < j" and "P\<^sup>=\<^sup>= (B (f i)) (B (f j))" by (auto simp: goodp_def)

   499   hence "P\<^sup>=\<^sup>= (?A (f i)) (?A (f j))" using assms by auto

   500   moreover from `i < j` have "f i < f j" using assms by auto

   501   ultimately show False using assms(3) by (auto simp: goodp_def)

   502 qed

   503 

   504 lemma iterated_subseq:

   505   assumes "\<forall>n>0::nat. \<forall>i\<ge>n. \<exists>j\<ge>n. emb (g n i) (g (n - 1) j)"

   506     and "m \<le> n"

   507   shows "\<forall>i\<ge>n. \<exists>j\<ge>m. emb (g n i) (g m j)"

   508 using assms(2)

   509 proof (induct "n - m" arbitrary: n)

   510   case 0 thus ?case by auto

   511 next

   512   case (Suc k)

   513   then obtain n' where n: "n = Suc n'" by (cases n) auto

   514   with Suc have "k = n' - m" and "m \<le> n'" by auto

   515   have "n > 0" by (auto simp: n)

   516   show ?case

   517   proof (intro allI impI)

   518     fix i assume "i \<ge> n"

   519     with assms(1)[rule_format, OF `n > 0`] obtain j where "j \<ge> n"

   520       and "emb (g (Suc n') i) (g n' j)" by (auto simp: n)

   521     with Suc(1)[OF `k = n' - m` `m \<le> n'`, THEN spec[of _ j]]

   522       obtain k where "k \<ge> m" and "emb (g n' j) (g m k)" by (auto simp: n)

   523     with `emb (g (Suc n') i) (g n' j)` have "emb (g n i) (g m k)" by (auto intro: emb_trans simp: n)

   524     thus "\<exists>j\<ge>m. emb (g n i) (g m j)" using `k \<ge> m` by blast

   525   qed

   526 qed

   527 

   528 lemma no_bad_of_special_shape_imp_goodp:

   529   assumes "\<not> (\<exists>f:: nat seq. (\<forall>i. f 0 \<le> f i) \<and> bad P (B \<circ> f))"

   530     and "\<forall>i. f i \<in> {B i | i. True}"

   531   shows "goodp P f"

   532 proof (rule ccontr)

   533   assume "bad P f"

   534   from assms(2) have "\<forall>i. \<exists>j. f i = B j" by blast

   535   from choice[OF this] obtain g where "\<And>i. f i = B (g i)" by blast

   536   with `bad P f` have "bad P (B \<circ> g)" by (auto simp: goodp_def)

   537   have "\<forall>i. \<exists>j>i. g j \<ge> g 0"

   538   proof (rule ccontr)

   539     assume "\<not> ?thesis"

   540     then obtain i::nat where "\<forall>j>i. \<not> (g j \<ge> g 0)" by auto

   541     hence *: "\<forall>j>i. g j < g 0" by auto

   542     let ?I = "{j. j > i}"

   543     from * have "\<forall>j>i. g j \<in> {..<g 0}" by auto

   544     hence "\<forall>j\<in>?I. g j \<in> {..<g 0}" by auto

   545     hence "g ` ?I \<subseteq> {..<g 0}" unfolding image_subset_iff by auto

   546     moreover have "finite {..<g 0}" by auto

   547     ultimately have 1: "finite (g ` ?I)" using finite_subset by blast

   548     have 2: "infinite ?I"

   549     proof -

   550       {

   551       fix m have "\<exists>n>m. i < n"

   552       proof (cases "m > i")

   553         case True thus ?thesis by auto

   554       next

   555         case False

   556         hence "m \<le> i" by auto

   557         hence "Suc i > m" and "i < Suc i" by auto

   558         thus ?thesis by blast

   559       qed

   560       }

   561       thus ?thesis unfolding infinite_nat_iff_unbounded by auto

   562     qed

   563     from pigeonhole_infinite[OF 2 1]

   564       obtain k where "k > i" and "infinite {j. j > i \<and> g j = g k}" by auto

   565     then obtain l where "k < l" and "g l = g k"

   566       unfolding infinite_nat_iff_unbounded by auto

   567     hence "P\<^sup>=\<^sup>= (B (g k)) (B (g l))" by auto

   568     with `k < l` and `bad P (B \<circ> g)` show False by (auto simp: goodp_def)

   569   qed

   570   from choice[OF this] obtain h

   571     where "\<forall>i. (h i) > i" and *: "\<And>i. g (h i) \<ge> g 0" by blast

   572   hence "\<forall>i\<ge>0. (h i) > i" by auto

   573   from funpow_mono[OF this] have **: "\<And>i j. i < j \<Longrightarrow> (h ^^ i) 0 < (h ^^ j) 0" by auto

   574   let ?i = "\<lambda>i. (h ^^ i) 0"

   575   let ?f = "\<lambda>i. g (?i i)"

   576   have "\<forall>i. ?f i \<ge> ?f 0"

   577   proof

   578     fix i show "?f i \<ge> ?f 0" using * by (induct i) auto

   579   qed

   580   moreover have "bad P (B \<circ> ?f)"

   581   proof

   582     assume "goodp P (B \<circ> ?f)"

   583     then obtain i j where "i < j" and "P\<^sup>=\<^sup>= (B (?f i)) (B (?f j))" by (auto simp: goodp_def)

   584     hence "P\<^sup>=\<^sup>= (B (g (?i i))) (B (g (?i j)))" by simp

   585     moreover from **[OF `i < j`] have "?i i < ?i j" .

   586     ultimately show False using `bad P (B \<circ> g)` by (auto simp: goodp_def)

   587   qed

   588   ultimately have "(\<forall>i. ?f i \<ge> ?f 0) \<and> bad P (B \<circ> ?f)" by auto

   589   hence "\<exists>f. (\<forall>i. f i \<ge> f 0) \<and> bad P (B \<circ> f)" by (rule exI[of _ ?f])

   590   with assms(1) show False by blast

   591 qed

   592 

   593 lemma emb_tl_left [simp]: "xs \<noteq> [] \<Longrightarrow> emb (tl xs) xs"

   594   by (induct xs) auto

   595 

   596 lemma tl_ne [simp]: "xs \<noteq> [] \<Longrightarrow> tl xs = xs \<Longrightarrow> False"

   597   by (induct xs) auto

   598 

   599 text {*Every reflexive and transitive relation on a finite set

   600 is a wqo.*}

   601 lemma finite_wqo_on:

   602   fixes A :: "('a::finite) set"

   603   assumes "reflp_on P A" and "transp_on P A"

   604   shows "wqo_on P A"

   605 proof

   606   fix f::"'a::finite seq"

   607   assume *: "\<forall>i. f i \<in> A"

   608   let ?I = "UNIV::nat set"

   609   have "f ` ?I \<subseteq> A" using * by auto

   610   with finite[of A] and finite_subset have 1: "finite (f ` ?I)" by blast

   611   have "infinite ?I" by auto

   612   from pigeonhole_infinite[OF this 1]

   613     obtain k where "infinite {j. f j = f k}" by auto

   614   then obtain l where "k < l" and "f l = f k"

   615     unfolding infinite_nat_iff_unbounded by auto

   616   hence "P\<^sup>=\<^sup>= (f k) (f l)" by auto

   617   with `k < l` show "goodp P f" by (auto simp: goodp_def)

   618 qed fact+

   619 

   620 lemma finite_eq_wqo_on:

   621   "wqo_on (op =) (A::('a::finite) set)"

   622   using finite_wqo_on[of "op =" A]

   623   by (auto simp: reflp_on_def transp_on_def)

   624 

   625 lemma wqo_on_finite_lists:

   626   shows "wqo_on emb (UNIV::('a::finite) list set)"

   627     (is "wqo_on ?P ?A")

   628 proof -

   629   {

   630     from emb_refl

   631       have "reflp_on ?P ?A" unfolding reflp_on_def by auto

   632   }

   633   note refl = this

   634   {

   635     from emb_trans

   636       have "transp_on ?P ?A" unfolding transp_on_def by auto

   637   }

   638   note trans = this

   639   {

   640     have "\<forall>f. (\<forall>i. f i \<in> ?A) \<longrightarrow> goodp ?P f"

   641     proof (rule ccontr)

   642       assume "\<not> ?thesis"

   643       then obtain f where "bad ?P f" by blast

   644       from bad_imp_mbp[of f, OF `bad ?P f`] obtain g

   645         where "\<forall>i. \<exists>j. emb (g i) (f j)"

   646         and "mbp g 0"

   647         and "bad ?P g"

   648         by blast

   649       from minimal_bad_element

   650         have "\<forall>f n.

   651         mbp f n \<and>

   652         bad ?P f \<longrightarrow>

   653         (\<exists>M.

   654           (\<forall>i\<le>n. M i = f i) \<and>

   655           emb (M (Suc n)) (f (Suc n)) \<and>

   656           (\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (repl (Suc n) f M i) (f j)) \<and>

   657           bad ?P (repl (Suc n) f M) \<and>

   658           mbp (repl (Suc n) f M) (Suc n))"

   659         (is "\<forall>f n. ?Q f n \<longrightarrow> (\<exists>M. ?Q' f n M)")

   660         by blast

   661       from choice2[OF this] obtain M

   662         where *[rule_format]: "\<forall>f n. ?Q f n \<longrightarrow> ?Q' f n (M f n)" by force

   663       let ?g = "minimal_bad_seq M g"

   664       let ?A = "\<lambda>i. ?g i i"

   665       have "\<forall>n. (n = 0 \<longrightarrow> (\<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (g j))) \<and> (n > 0 \<longrightarrow> (\<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (?g (n - 1) j))) \<and> (\<forall>i\<le>n. mbp (?g n) i) \<and> (\<forall>i\<le>n. ?A i = ?g n i) \<and> bad ?P (?g n)"

   666       proof

   667         fix n

   668         show "(n = 0 \<longrightarrow> (\<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (g j))) \<and> (n > 0 \<longrightarrow> (\<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (?g (n - 1) j))) \<and> (\<forall>i\<le>n. mbp (?g n) i) \<and> (\<forall>i\<le>n. ?A i = ?g n i) \<and> bad ?P (?g n)"

   669         proof (induction n)

   670           case 0

   671           have "mbp g 0" by fact

   672           moreover have "bad ?P g" by fact

   673           ultimately

   674             have [simp]: "M g 0 0 = g 0" and "emb (M g 0 (Suc 0)) (g (Suc 0))"

   675             and "bad ?P (M g 0)" and "mbp (M g 0) (Suc 0)"

   676             and **: "\<forall>i\<ge>Suc 0. \<exists>j\<ge>Suc 0. emb (M g 0 i) (g j)"

   677             using *[of g 0] by auto

   678           moreover have "mbp (M g 0) 0"

   679           proof (unfold mbp_def, intro allI impI, elim conjE)

   680             fix e :: "'a list seq"

   681             presume "(e 0, g 0) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")

   682               and *: "\<forall>i. \<exists>j\<ge>0. emb (e i) (M g 0 j)"

   683             have "\<forall>i. \<exists>j\<ge>0::nat. emb (e i) (g j)"

   684             proof (intro allI impI)

   685               fix i

   686               from * obtain j where "j \<ge> 0" and "emb (e i) (M g 0 j)" by auto

   687               show "\<exists>j\<ge>0. emb (e i) (g j)"

   688               proof (cases "j = 0")

   689                 case True

   690                 with `emb (e i) (M g 0 j)` have "emb (e i) (g 0)" by auto

   691                 thus ?thesis by auto

   692               next

   693                 case False

   694                 hence "j \<ge> Suc 0" by auto

   695                 with ** obtain k where "k \<ge> Suc 0" and "emb (M g 0 j) (g k)" by auto

   696                 with `emb (e i) (M g 0 j)` have "emb (e i) (g k)" by (blast intro: emb_trans)

   697                 moreover with `k \<ge> Suc 0` have "k \<ge> 0" by auto

   698                 ultimately show ?thesis by blast

   699               qed

   700             qed

   701             with `mbp g 0`[unfolded mbp_def]

   702             show "goodp ?P e" using `(e 0, g 0) \<in> ?emb` by (simp add: mbp_def)

   703           qed auto

   704           moreover have "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (?g 0 i) (g j)"

   705           proof (intro allI impI)

   706             fix i::nat

   707             assume "i \<ge> 0"

   708             hence "i = 0 \<or> i \<ge> Suc 0" by auto

   709             thus "\<exists>j\<ge>0. emb (?g 0 i) (g j)"

   710             proof

   711               assume "i \<ge> Suc 0"

   712               with ** obtain j where "j \<ge> Suc 0" and "emb (?g 0 i) (g j)" by auto

   713               moreover from this have "j \<ge> 0" by auto

   714               ultimately show "?thesis" by auto

   715             next

   716               assume "i = 0"

   717               hence "emb (?g 0 i) (g 0)" by auto

   718               thus ?thesis by blast

   719             qed

   720           qed

   721           ultimately show ?case by simp

   722         next

   723           case (Suc n)

   724           with *[of "?g n" n]

   725             have eq: "\<forall>i\<le>n. ?A i = ?g n i"

   726             and emb: "emb (?g (Suc n) (Suc n)) (?g n (Suc n))"

   727             and subseq: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g (Suc n) i) (?g n j)"

   728             and "bad ?P (?g (Suc n))"

   729             and mbp: "mbp (?g (Suc n)) (Suc n)"

   730             by (simp_all add: Let_def)

   731           moreover have *: "\<forall>i\<le>Suc n. ?A i = ?g (Suc n) i"

   732           proof (intro allI impI)

   733             fix i assume "i \<le> Suc n"

   734             show "?A i = ?g (Suc n) i"

   735             proof (cases "i = Suc n")

   736               assume "i = Suc n"

   737               thus ?thesis by simp

   738             next

   739               assume "i \<noteq> Suc n"

   740               with `i \<le> Suc n` have "i < Suc n" by auto

   741               thus ?thesis by (simp add: Let_def eq)

   742             qed

   743           qed

   744           moreover have "\<forall>i\<le>Suc n. mbp (?g (Suc n)) i"

   745           proof (intro allI impI)

   746             fix i assume "i \<le> Suc n"

   747             show "mbp (?g (Suc n)) i"

   748             proof (cases "i = Suc n")

   749               case True with mbp show ?thesis by simp

   750             next

   751               case False with `i \<le> Suc n` have le: "i \<le> Suc n" "i \<le> n" by auto

   752               show ?thesis

   753               proof (unfold mbp_def, intro allI impI, elim conjE)

   754                 fix e

   755                 note * = *[rule_format, symmetric] eq[rule_format, symmetric]

   756                 assume "\<forall>i'<i. e i' = ?g (Suc n) i'"

   757                 hence 1: "\<forall>i'<i. e i' = ?g n i'" using * and le by auto

   758                 presume "(e i, ?g (Suc n) i) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")

   759                 hence 2: "(e i, ?g n i) \<in> ?emb" using * and le by simp

   760                 assume **: "\<forall>j\<ge>i. \<exists>k\<ge>i. emb (e j) (?g (Suc n) k)"

   761                 have 3: "\<forall>j\<ge>i. \<exists>k\<ge>i. emb (e j) (?g n k)"

   762                 proof (intro allI impI)

   763                   fix j assume "i \<le> j"

   764                   with ** obtain k where "k \<ge> i" and "emb (e j) (?g (Suc n) k)" by blast

   765                   show "\<exists>k\<ge>i. emb (e j) (?g n k)"

   766                   proof (cases "k \<le> n")

   767                     case True with `emb (e j) (?g (Suc n) k)`

   768                       have "emb (e j) (?g n k)" using * by auto

   769                     thus ?thesis using `k \<ge> i` by auto

   770                   next

   771                     case False hence "k \<ge> Suc n" by auto

   772                     with subseq obtain l where "l \<ge> Suc n"

   773                       and "emb (?g (Suc n) k) (?g n l)" by blast

   774                     with `emb (e j) (?g (Suc n) k)` have "emb (e j) (?g n l)" by (auto intro: emb_trans)

   775                     moreover from `i \<le> Suc n` and `l \<ge> Suc n` have "l \<ge> i" by auto

   776                     ultimately show ?thesis by blast

   777                   qed

   778                 qed

   779                 from 1 2 3 and Suc[THEN conjunct2, THEN conjunct2] and `i \<le> n`

   780                 show "goodp ?P e" unfolding mbp_def by blast

   781               qed simp

   782             qed

   783           qed

   784           ultimately show ?case by simp

   785         qed

   786       qed

   787       hence 1: "\<forall>n. \<forall>i\<le>n. mbp (?g n) i"

   788         and 2: "\<forall>n. \<forall>i\<le>n. ?A i = ?g n i"

   789         and 3: "\<forall>n. bad ?P (?g n)"

   790         and 6: "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (?g 0 i) (g j)"

   791         and 7: "\<forall>n>0. \<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (?g (n - 1) j)"

   792         by auto

   793       have ex_subset: "\<forall>n. \<forall>i. \<exists>j. emb (?g n i) (g j)"

   794       proof

   795         fix n show "\<forall>i. \<exists>j. emb (?g n i) (g j)"

   796         proof (induct n)

   797           case 0 with 6 show ?case by simp

   798         next

   799           case (Suc n)

   800           show ?case

   801           proof

   802             fix i

   803             have "i < Suc n \<or> i \<ge> Suc n" by auto

   804             thus "\<exists>j. emb (?g (Suc n) i) (g j)"

   805             proof

   806               assume "i < Suc n" hence "i \<le> Suc n" and "i \<le> n" by auto

   807               from `i \<le> Suc n` have "?g (Suc n) i = ?g i i" using 2 by auto

   808               moreover from `i \<le> n` have "?g n i = ?g i i" using 2 by auto

   809               ultimately have "?g (Suc n) i = ?g n i" by auto

   810               with Suc show ?thesis by auto

   811             next

   812               assume "i \<ge> Suc n"

   813               with 7[THEN spec[of _ "Suc n"]]

   814                 obtain j where "j \<ge> Suc n" and "emb (?g (Suc n) i) (?g n j)" by auto

   815               moreover from Suc obtain k where "emb (?g n j) (g k)" by blast

   816               ultimately show ?thesis by (blast intro: emb_trans)

   817             qed

   818           qed

   819         qed

   820       qed

   821       have bad: "bad ?P ?A"

   822       proof

   823         assume "goodp ?P ?A"

   824         then obtain i j :: nat where "i < j"

   825           and "?P\<^sup>=\<^sup>= (?g i i) (?g j j)" unfolding goodp_def by auto

   826         moreover with 2[rule_format, of i j]

   827           have "?P\<^sup>=\<^sup>= (?g j i) (?g j j)" by auto

   828         ultimately have "goodp ?P (?g j)" unfolding goodp_def by blast

   829         with 3 show False by auto

   830       qed

   831       have non_empty: "\<forall>i. ?A i \<noteq> []" using bad and bad_imp_not_empty[of ?A] by auto

   832       then obtain a as where a: "\<forall>i. hd (?A i) = a i \<and> tl (?A i) = as i" by force

   833       let ?B = "\<lambda>i. tl (?A i)"

   834       {

   835         assume "\<exists>f::nat seq. (\<forall>i. f i \<ge> f 0) \<and> bad ?P (?B \<circ> f)"

   836         then obtain f :: "nat seq" where ge: "\<forall>i. f i \<ge> f 0"

   837           and "bad ?P (?B \<circ> f)" by auto

   838         let ?C = "\<lambda>i. if i < f 0 then ?A i else ?B (f (i - f 0))"

   839         have [simp]: "\<And>i. i < f 0 \<Longrightarrow> ?C i = ?A i" by auto

   840         have [simp]: "\<And>i. f 0 \<le> i \<Longrightarrow> ?C i = ?B (f (i - f 0))" by auto

   841         have "bad ?P ?C"

   842         proof

   843           assume "goodp ?P ?C"

   844           then obtain i j where "i < j" and *: "?P\<^sup>=\<^sup>= (?C i) (?C j)" by (auto simp: goodp_def)

   845           {

   846             assume "j < f 0" with `i < j` and * have "?P\<^sup>=\<^sup>= (?A i) (?A j)" by simp

   847             with `i < j` and `bad ?P ?A` have False by (auto simp: goodp_def)

   848           } moreover {

   849             assume "f 0 \<le> i" with `i < j` and * have "?P\<^sup>=\<^sup>= (?B (f (i - f 0))) (?B (f (j - f 0)))" by simp

   850             moreover with `i < j` and `f 0 \<le> i` have "i - f 0 < j - f 0" by auto

   851             ultimately have False using `bad ?P (?B \<circ> f)` by (auto simp: goodp_def)

   852           } moreover {

   853             have emb: "emb (?B (f (j - f 0))) (?A (f (j - f 0)))" using non_empty by simp

   854             assume "i < f 0" and "f 0 \<le> j"

   855             with * have "?P\<^sup>=\<^sup>= (?A i) (?B (f (j - f 0)))" by auto

   856             hence "?P (?A i) (?B (f (j - f 0))) \<or> ?A i = ?B (f (j - f 0))" by simp

   857             hence False

   858             proof

   859               assume "?P (?A i) (?B (f (j - f 0)))"

   860               with emb have "?P (?A i) (?A (f (j - f 0)))" by (blast intro: emb_trans)

   861               moreover from ge[THEN spec[of _ "j - f 0"]] and `i < f 0` have "i < f (j - f 0)" by auto

   862               ultimately show ?thesis using `bad ?P ?A` by (auto simp: goodp_def)

   863             next

   864               assume "?A i = ?B (f (j - f 0))"

   865               with emb have "emb (?A i) (?A (f (j - f 0)))" by auto

   866               moreover have "?P (?A i) (?A i)" using emb_refl by auto

   867               ultimately have "?P (?A i) (?A (f (j - f 0)))" by (blast intro: emb_trans)

   868               moreover from ge[THEN spec[of _ "j - f 0"]] and `i < f 0` have "i < f (j - f 0)" by auto

   869               ultimately show ?thesis using `bad ?P ?A` by (auto simp: goodp_def)

   870             qed

   871           } ultimately show False by arith

   872         qed

   873         have "\<forall>i<f 0. ?C i = ?g (f 0) i" using 2 by auto

   874         moreover have "(?C (f 0), ?g (f 0) (f 0)) \<in> {(x, y). emb x y \<and> x \<noteq> y}" using non_empty tl_ne by auto

   875         moreover have "\<forall>i\<ge>f 0. \<exists>j\<ge>f 0. emb (?C i) (?g (f 0) j)"

   876         proof (intro allI impI)

   877           fix i

   878           let ?i = "f (i - f 0)"

   879           assume "f 0 \<le> i"

   880           with `\<forall>i. f 0 \<le> f i` have "f 0 \<le> ?i" by auto

   881           from `f 0 \<le> i` have *: "?C i = ?B ?i" by auto

   882           have "emb (?C i) (?g ?i ?i)" unfolding * using non_empty emb_tl_left by auto

   883           from iterated_subseq[OF 7, of "f 0" "?i", THEN spec[of _ "?i"], OF `f 0 \<le> ?i`]

   884             obtain j where "j \<ge> f 0" and "emb (?g ?i ?i) (?g (f 0) j)" by blast

   885           with `emb (?C i) (?g ?i ?i)`

   886             show "\<exists>j\<ge>f 0. emb (?C i) (?g (f 0) j)" by (blast intro: emb_trans)

   887         qed

   888         ultimately have "goodp ?P ?C"

   889           using 1[rule_format, of "f 0", OF le_refl, unfolded mbp_def] by auto

   890         with `bad ?P ?C` have False by blast

   891       }

   892       hence no_index: "\<not> (\<exists>f. (\<forall>i. f 0 \<le> f i) \<and> bad ?P (?B \<circ> f))" by blast

   893       let ?B' = "{?B i | i. True}"

   894       have subset: "?B' \<subseteq> UNIV" by auto

   895       have "wqo_on ?P ?B'"

   896       proof

   897         from emb_refl show "reflp_on ?P ?B'" by (auto simp: reflp_on_def)

   898       next

   899         from emb_trans show "transp_on ?P ?B'" by (auto simp: transp_on_def)

   900       next

   901         fix f :: "'a list seq" assume "\<forall>i. f i \<in> ?B'"

   902         from no_bad_of_special_shape_imp_goodp[of ?P ?B f, OF no_index this]

   903           show "goodp ?P f" .

   904       qed

   905       let ?a' = "{a i | i. True}"

   906       have "?a' \<subseteq> UNIV" by auto

   907       with finite_eq_wqo_on

   908         have "wqo_on op = ?a'"

   909         using finite[of UNIV] and finite_subset by blast

   910       from wqo_on_Sigma[OF `wqo_on op = ?a'` `wqo_on ?P ?B'`]

   911         have wqo: "wqo_on (prod_le op = ?P) (?a' \<times> ?B')" .

   912       let ?aB = "\<lambda>i. (a i, ?B i)"

   913       let ?P' = "prod_le op = ?P"

   914       have "\<forall>i. ?aB i \<in> (?a' \<times> ?B')" by auto

   915       with wqo have "goodp ?P' ?aB" unfolding wqo_on_def by auto

   916       then obtain i j where "i < j" and *: "?P'\<^sup>=\<^sup>= (?aB i) (?aB j)"

   917         by (auto simp: goodp_def)

   918       from hd_Cons_tl and non_empty

   919         have hd_tl: "hd (?A i) # tl (?A i) = ?A i"

   920           "hd (?A j) # tl (?A j) = ?A j" by auto

   921       from * have "(a i = a j \<and> ?B i = ?B j) \<or> (a i = a j \<and> ?P (?B i) (?B j))"

   922         unfolding prod_le_def by auto

   923       thus False

   924       proof

   925         assume *: "a i = a j \<and> ?B i = ?B j"

   926         hence "?A i = ?A j" using a and hd_tl by auto

   927         hence "?P\<^sup>=\<^sup>= (?A i) (?A j)" by auto

   928         with `i < j` and `bad ?P ?A` show False by (auto simp: goodp_def)

   929       next

   930         assume "op = (a i) (a j) \<and> ?P (?B i) (?B j)"

   931         hence *: "op = (a i) (a j)" and **: "?P (?B i) (?B j)" by auto

   932         with emb_appendI[OF emb_refl[of "[hd (?A i)]"] **]

   933           have "emb (?A i) (?A j)" using hd_tl a by simp

   934         hence "?P\<^sup>=\<^sup>= (?A i) (?A j)" by auto

   935         with `i < j` and `bad ?P ?A` show False by (auto simp: goodp_def)

   936       qed

   937     qed

   938   }

   939   with refl and trans show ?thesis unfolding wqo_on_def by blast

   940 qed

   941 

   942 lemma Higman_antichains:

   943   fixes A :: "('a::finite) list set"

   944   assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(emb x y) \<and> \<not>(emb y x)"

   945   shows "finite A"

   946 proof (rule ccontr)

   947   assume "infinite A"

   948   then obtain f :: "nat \<Rightarrow> ('a::finite) list" where b: "inj f" and c: "range f \<subseteq> A"

   949     by (auto simp add: infinite_iff_countable_subset)

   950   from wqo_on_imp_goodp[OF wqo_on_finite_lists, simplified, of f]

   951     obtain i j where d: "i < j" and e: "emb (f i) (f j)" by (auto simp: goodp_def)

   952   have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)

   953   moreover

   954   have "f i \<in> A" using c by auto

   955   moreover

   956   have "f j \<in> A" using c by auto

   957   ultimately have "\<not> (emb (f i) (f j))" using a by simp

   958   with e show "False" by simp

   959 qed

   960 

   961 end