theory WQO_Finite_Lists+
−
imports "Seq"+
−
begin+
−
+
−
subsection {* Auxiliary Lemmas *}+
−
+
−
lemma funpow_non_decreasing:+
−
  fixes f :: "'a::order \<Rightarrow> 'a"+
−
  assumes "\<forall>i\<ge>n. f i \<ge> i"+
−
  shows "(f ^^ i) n \<ge> n"+
−
  using assms by (induct i) auto+
−
+
−
lemma funpow_mono:+
−
  assumes "\<forall>i\<ge>n::nat. f i > i" and "j > i"+
−
  shows "(f ^^ j) n > (f ^^ i) n"+
−
using assms(2)+
−
proof (induct "j - i" arbitrary: i j)+
−
  case 0 thus ?case by simp+
−
next+
−
  case (Suc m)+
−
  then obtain j' where j: "j = Suc j'" by (cases j) auto+
−
  show ?case+
−
  proof (cases "i < j'")+
−
    case True+
−
    with Suc(1)[of j'] and Suc(2)[unfolded j]+
−
      have "(f ^^ j') n > (f ^^ i) n" by simp+
−
    moreover have "(f ^^ j) n > (f ^^ j') n"+
−
    proof -+
−
      have "(f ^^ j) n = f ((f ^^ j') n)" by (simp add: j)+
−
      also have "\<dots> > (f ^^ j') n" using assms and funpow_non_decreasing[of n f j'] by force+
−
      finally show ?thesis .+
−
    qed+
−
    ultimately show ?thesis by auto+
−
  next+
−
    case False+
−
    with Suc have i: "i = j'" unfolding j by (induct i) auto+
−
    show ?thesis unfolding i j using assms and funpow_non_decreasing[of n f j'] by force+
−
  qed+
−
qed+
−
+
−
+
−
subsection {* Basic Definitions *}+
−
+
−
definition reflp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where+
−
  "reflp_on P A \<equiv> \<forall>a\<in>A. P a a"+
−
+
−
lemma reflp_onI [Pure.intro]:+
−
  "(\<And>a. a \<in> A \<Longrightarrow> P a a) \<Longrightarrow> reflp_on P A"+
−
  unfolding reflp_on_def by blast+
−
+
−
definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where+
−
  "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"+
−
+
−
lemma transp_onI [Pure.intro]:+
−
  "(\<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"+
−
  unfolding transp_on_def by blast+
−
+
−
definition goodp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a seq \<Rightarrow> bool" where+
−
  "goodp P f \<equiv> \<exists>i j. i < j \<and> P\<^sup>=\<^sup>= (f i) (f j)"+
−
+
−
abbreviation bad where "bad P f \<equiv> \<not> goodp P f"+
−
+
−
definition wqo_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where+
−
  "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)"+
−
+
−
lemma wqo_onI [Pure.intro]:+
−
  "\<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"+
−
  unfolding wqo_on_def by blast+
−
+
−
lemma reflp_on_reflclp [simp]:+
−
  assumes "reflp_on P A" and "a \<in> A" and "b \<in> A"+
−
  shows "P\<^sup>=\<^sup>= a b = P a b"+
−
  using assms by (auto simp: reflp_on_def)+
−
+
−
lemma transp_on_tranclp:+
−
  assumes "transp_on P A"+
−
  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"+
−
    (is "?lhs = ?rhs")+
−
  by (rule iffI, induction rule: tranclp.induct)+
−
     (insert assms, auto simp: transp_on_def)+
−
+
−
lemma wqo_on_imp_reflp_on:+
−
  "wqo_on P A \<Longrightarrow> reflp_on P A"+
−
  by (auto simp: wqo_on_def)+
−
+
−
lemma wqo_on_imp_transp_on:+
−
  "wqo_on P A \<Longrightarrow> transp_on P A"+
−
  by (auto simp: wqo_on_def)+
−
+
−
lemma wqo_on_imp_goodp:+
−
  "wqo_on P A \<Longrightarrow> \<forall>i. f i \<in> A \<Longrightarrow> goodp P f"+
−
  by (auto simp: wqo_on_def)+
−
+
−
lemma reflp_on_converse:+
−
  "reflp_on P A \<Longrightarrow> reflp_on P\<inverse>\<inverse> A"+
−
  unfolding reflp_on_def by blast+
−
+
−
lemma transp_on_converse:+
−
  "transp_on P A \<Longrightarrow> transp_on P\<inverse>\<inverse> A"+
−
  unfolding transp_on_def by blast+
−
+
−
subsection {* Dickson's Lemma *}+
−
+
−
text {*When two sets are wqo, then their cartesian product is wqo.*}+
−
+
−
definition+
−
  prod_le :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"+
−
where+
−
  "prod_le P1 P2 \<equiv> \<lambda>(p1, p2) (q1, q2). P1 p1 q1 \<and> P2 p2 q2"+
−
+
−
lemma wqo_on_Sigma:+
−
  fixes A1 :: "'a set" and A2 :: "'b set"+
−
  assumes "wqo_on P1 A1" and "wqo_on P2 A2"+
−
  shows "wqo_on (prod_le P1 P2) (A1 \<times> A2)"+
−
    (is "wqo_on ?P ?A")+
−
proof+
−
  show "reflp_on ?P ?A"+
−
    using assms by (auto simp: wqo_on_def reflp_on_def prod_le_def)+
−
next+
−
  from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def)+
−
  thus "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast+
−
next+
−
  fix g :: "('a \<times> 'b) seq"+
−
  let ?p = "\<lambda>i. fst (g i)"+
−
  let ?q = "\<lambda>i. snd (g i)"+
−
  assume g: "\<forall>i. g i \<in> ?A"+
−
  have p: "\<forall>i. ?p i \<in> A1"+
−
  proof+
−
    fix i+
−
    from g have "g i \<in> ?A" by simp+
−
    thus "?p i \<in> A1" by auto+
−
  qed+
−
  have q: "\<forall>i. ?q i \<in> A2"+
−
  proof+
−
    fix i+
−
    from g have "g i \<in> ?A" by simp+
−
    thus "?q i \<in> A2" by auto+
−
  qed+
−
  let ?T = "{m. \<forall>n>m. \<not> (P1 (?p m) (?p n))}"+
−
  have "finite ?T"+
−
  proof (rule ccontr)+
−
    assume "infinite ?T"+
−
    hence "INFM m. m \<in> ?T" unfolding INFM_iff_infinite by simp+
−
    then interpret infinitely_many "\<lambda>m. m \<in> ?T" by (unfold_locales) assumption+
−
    let ?p' = "\<lambda>i. ?p (index i)"+
−
    have p': "\<forall>i. ?p' i \<in> A1" using p by auto+
−
    have "bad P1 ?p'"+
−
    proof+
−
      assume "goodp P1 ?p'"+
−
      then obtain i j :: nat where "i < j"+
−
        and "P1\<^sup>=\<^sup>= (?p' i) (?p' j)" by (auto simp: goodp_def)+
−
      hence "P1 (?p' i) (?p' j)"+
−
        using p' and reflp_on_reflclp[OF wqo_on_imp_reflp_on[OF assms(1)]] by simp+
−
      moreover from index_ordered_less[OF `i < j`] have "index j > index i" .+
−
      moreover from index_p have "index i \<in> ?T" by simp+
−
      ultimately show False by blast+
−
    qed+
−
    with assms(1) show False using p' by (auto simp: wqo_on_def)+
−
  qed+
−
  then obtain n where "\<forall>r\<ge>n. r \<notin> ?T"+
−
    using infinite_nat_iff_unbounded_le[of "?T"] by auto+
−
  hence "\<forall>i\<in>{n..}. \<exists>j>i. P1 (?p i) (?p j)" by blast+
−
  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+
−
  from bchoice[OF this] obtain f :: "nat seq"+
−
    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+
−
  from stepfun_imp_chainp[of n f "\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y" ?p, OF this]+
−
    have chain: "chainp (\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y) (\<lambda>i. ?p ((f^^i) n))" .+
−
  let ?f = "\<lambda>i. (f^^i) n"+
−
  from 1 have inc: "\<forall>i\<ge>n. f i > i" by simp+
−
  from wqo_on_imp_goodp[OF assms(2), of "?q \<circ> ?f"] and q+
−
    obtain i j where "\<And>i. ?q (?f i) \<in> A2" and "j > i" and "P2\<^sup>=\<^sup>= (?q (?f i)) (?q (?f j))"+
−
    by (auto simp: goodp_def)+
−
  hence "P2 (?q (?f i)) (?q (?f j))"+
−
    using reflp_on_reflclp[OF wqo_on_imp_reflp_on[OF assms(2)]] by simp+
−
  moreover from funpow_mono[OF inc `j > i`] have "?f j > ?f i" .+
−
  moreover from chainp_imp_tranclp[of "\<lambda>x y. x \<in> A1 \<and> y \<in> A1 \<and> P1 x y", OF chain `j > i`]+
−
    have "P1 (?p (?f i)) (?p (?f j))"+
−
    unfolding transp_on_tranclp[OF wqo_on_imp_transp_on[OF assms(1)]] by simp+
−
  ultimately have "\<exists>i j. j > i \<and> P1 (?p i) (?p j) \<and> P2 (?q i) (?q j)" by auto+
−
  thus "goodp ?P g" by (auto simp: split_def goodp_def prod_le_def)+
−
qed+
−
+
−
subsection {* Higman's Lemma *}+
−
+
−
inductive+
−
  emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"+
−
where+
−
  emb0 [intro]: "emb [] y"+
−
| emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)"+
−
| emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)"+
−
+
−
lemma emb_refl [simp]: "emb xs xs"+
−
  by (induct xs) auto+
−
+
−
lemma emb_Nil2 [simp]: "emb y [] \<Longrightarrow> y = []"+
−
  by (cases rule: emb.cases) auto+
−
+
−
lemma emb_right [intro]:+
−
  assumes a: "emb x y"+
−
  shows "emb x (y @ y')"+
−
using a +
−
by (induct arbitrary: y') (auto)+
−
+
−
lemma emb_left [intro]:+
−
  assumes a: "emb x y"+
−
  shows "emb x (y' @ y)"+
−
using a by (induct y') (auto)+
−
+
−
lemma emb_appendI [intro]:+
−
  assumes a: "emb x x'"+
−
  and     b: "emb y y'"+
−
  shows "emb (x @ y) (x' @ y')"+
−
using a b by (induct) (auto)+
−
+
−
lemma emb_cons_leftD:+
−
  assumes "emb (a # x) y"+
−
  shows "\<exists>y1 y2. y = y1 @ [a] @ y2 \<and> emb x y2"+
−
using assms+
−
apply(induct x\<equiv>"a # x" y\<equiv>"y" arbitrary: a x y)+
−
apply(auto)+
−
apply(metis append_Cons)+
−
done+
−
+
−
lemma emb_append_leftD:+
−
  assumes "emb (x1 @ x2) y"+
−
  shows "\<exists>y1 y2. y = y1 @ y2 \<and> emb x1 y1 \<and> emb x2 y2"+
−
using assms+
−
apply(induct x1 arbitrary: x2 y)+
−
apply(auto)+
−
apply(drule emb_cons_leftD)+
−
apply(auto)+
−
apply(drule_tac x="x2" in meta_spec)+
−
apply(drule_tac x="y2" in meta_spec)+
−
apply(auto)+
−
apply(rule_tac x="y1 @ (a # y1a)" in exI)+
−
apply(rule_tac x="y2a" in exI)+
−
apply(auto)+
−
done+
−
+
−
lemma emb_trans:+
−
  assumes a: "emb x1 x2"+
−
  and     b: "emb x2 x3"+
−
  shows "emb x1 x3"+
−
using a b+
−
apply(induct arbitrary: x3)+
−
apply(metis emb0)+
−
apply(metis emb_cons_leftD emb_left)+
−
apply(drule_tac emb_cons_leftD)+
−
apply(auto)+
−
done+
−
+
−
lemma empty_imp_goodp_emb [simp]:+
−
  assumes "f i = []"+
−
  shows "goodp emb f"+
−
proof (rule ccontr)+
−
  assume "bad emb f"+
−
  moreover have "(emb)\<^sup>=\<^sup>= (f i) (f (Suc i))"+
−
    unfolding assms by auto+
−
  ultimately show False+
−
    unfolding goodp_def by auto+
−
qed+
−
+
−
lemma bad_imp_not_empty:+
−
  "bad emb f \<Longrightarrow> f i \<noteq> []"+
−
  by auto+
−
+
−
text {*Replace the elements of an infinite sequence, starting from a given+
−
position, by those of another infinite sequence.*}+
−
definition repl :: "nat \<Rightarrow> 'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where+
−
  "repl i f g \<equiv> \<lambda>j. if j \<ge> i then g j else f j"+
−
+
−
lemma repl_0 [simp]:+
−
  "repl 0 f g = g"+
−
  by (simp add: repl_def)+
−
+
−
lemma repl_simps [simp]:+
−
  "j \<ge> i \<Longrightarrow> repl i f g j = g j"+
−
  "j < i \<Longrightarrow> repl i f g j = f j"+
−
  by (auto simp: repl_def)+
−
+
−
lemma repl_ident [simp]:+
−
   "repl i f f = f"+
−
   by (auto simp: repl_def)+
−
+
−
lemma repl_repl_ident [simp]:+
−
  "repl n f (repl n g h) = repl n f h"+
−
  by (auto simp: repl_def)+
−
+
−
lemma repl_repl_ident' [simp]:+
−
  "repl n (repl n f g) h = repl n f h"+
−
  by (auto simp: repl_def)+
−
+
−
lemma bad_emb_repl:+
−
  assumes "bad emb f"+
−
    and "bad emb g"+
−
    and "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (g i) (f j)"+
−
  shows "bad emb (repl n f g)" (is "bad emb ?f")+
−
proof (rule ccontr)+
−
  presume "goodp emb ?f"+
−
  then obtain i j where "i < j"+
−
    and good: "emb\<^sup>=\<^sup>= (?f i) (?f j)" by (auto simp: goodp_def)+
−
  {+
−
    assume "j < n"+
−
    with `i < j` and good have "emb\<^sup>=\<^sup>= (f i) (f j)" by simp+
−
    with assms(1) have False using `i < j` by (auto simp: goodp_def)+
−
  } moreover {+
−
    assume "n \<le> i"+
−
    with `i < j` and good have "i - n < j - n"+
−
      and "emb\<^sup>=\<^sup>= (g i) (g j)" by auto+
−
    with assms(2) have False by (auto simp: goodp_def)+
−
  } moreover {+
−
    assume "i < n" and "n \<le> j"+
−
    with assms(3) obtain k where "k \<ge> n" and emb: "emb (g j) (f k)" by blast+
−
    from `i < j` and `i < n` and `n \<le> j` and good+
−
      have "emb\<^sup>=\<^sup>= (f i) (g j)" by auto+
−
    hence "emb\<^sup>=\<^sup>= (f i) (f k)"+
−
    proof+
−
      assume fi: "f i = g j"+
−
      with emb_refl have "emb (f i) (f i)" by blast+
−
      with emb_trans[OF emb] show "emb\<^sup>=\<^sup>= (f i) (f k)" by (auto simp: fi)+
−
    next+
−
      assume "emb (f i) (g j)"+
−
      from emb_trans[OF this emb] show "emb\<^sup>=\<^sup>= (f i) (f k)" by auto+
−
    qed+
−
    with `i < n` and `n \<le> k` and assms(1) have False by (auto simp: goodp_def)+
−
  } ultimately show False using `i < j` by arith+
−
qed simp+
−
+
−
text {*A \emph{minimal bad prefix} of an infinite sequence, is a+
−
prefix of its first @{text n} elements, such that every subsequence (of subsets)+
−
starting with the same @{text n} elements is good, whenever the @{text n}-th+
−
element is replaced by a proper subset of itself.*}+
−
definition mbp :: "'a list seq \<Rightarrow> nat \<Rightarrow> bool" where+
−
  "mbp f n \<equiv>+
−
    \<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))+
−
    \<longrightarrow> goodp emb g"+
−
+
−
lemma ex_repl_conv:+
−
  "(\<exists>j\<ge>n. P (repl n f g j)) \<longleftrightarrow> (\<exists>j\<ge>n. P (g j))"+
−
  by auto+
−
+
−
lemma emb_strict_length:+
−
  assumes a: "emb x y" "x \<noteq> y" +
−
  shows "length x < length y"+
−
  using a by (induct) (auto simp add: less_Suc_eq)+
−
+
−
lemma emb_wf:+
−
  shows "wf {(x, y). emb x y \<and> x \<noteq> y}"+
−
proof -+
−
  have "wf (measure length)" by simp+
−
  moreover+
−
  have "{(x, y). emb x y \<and> x \<noteq> y} \<subseteq> measure length"+
−
    unfolding measure_def by (auto simp add: emb_strict_length)+
−
  ultimately +
−
  show "wf {(x, y). emb x y \<and> x \<noteq> y}" by (rule wf_subset)+
−
qed+
−
+
−
lemma minimal_bad_element:+
−
  fixes f :: "'a list seq"+
−
  assumes "mbp f n"+
−
    and "bad emb f"+
−
  shows "\<exists>M.+
−
    (\<forall>i\<le>n. M i = f i) \<and>+
−
    emb (M (Suc n)) (f (Suc n)) \<and>+
−
    (\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb ((repl (Suc n) f M) i) (f j)) \<and>+
−
    bad emb (repl (Suc n) f M) \<and>+
−
    mbp (repl (Suc n) f M) (Suc n)"+
−
using assms+
−
proof (induct "f (Suc n)" arbitrary: f n rule: wf_induct_rule[OF emb_wf])+
−
  case (1 g)+
−
  show ?case+
−
  proof (cases "mbp g (Suc n)")+
−
    case True+
−
    let ?g = "repl (Suc n) g g"+
−
    have "\<forall>i\<le>n. ?g i = g i" by simp+
−
    moreover have "emb (g (Suc n)) (g (Suc n))" by simp+
−
    moreover have "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb ((repl (Suc n) g g) i) (g j)" by auto+
−
    moreover from `bad emb g`+
−
      have "bad emb (repl (Suc n) g g)" by simp+
−
    moreover from True have "mbp (repl (Suc n) g g) (Suc n)" by simp+
−
    ultimately show ?thesis by blast+
−
  next+
−
    case False+
−
    then obtain h where less: "\<forall>i<Suc n. h i = g i"+
−
      and emb: "(h (Suc n), g (Suc n)) \<in> {(x, y). emb x y \<and> x \<noteq> y}"+
−
        (is "_ \<in> ?emb")+
−
      and greater: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (h i) (g j)"+
−
      and bad: "bad emb h"+
−
      unfolding mbp_def by blast+
−
    let ?g = "repl (Suc n) g h"+
−
    from emb have emb': "(?g (Suc n), g (Suc n)) \<in> ?emb" by simp+
−
    have mbp: "mbp ?g n"+
−
    proof (unfold mbp_def, intro allI impI, elim conjE)+
−
      fix e+
−
      assume "\<forall>i<n. e i = ?g i"+
−
      hence 1: "\<forall>i<n. e i = g i" by auto+
−
      assume "e n \<noteq> ?g n"+
−
      hence 2: "e n \<noteq> ?g n" .+
−
      assume "emb (e n) (?g n)"+
−
      hence 3: "emb (e n) (g n)" by auto+
−
      assume *: "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (e i) (?g j)"+
−
      have 4: "\<forall>i\<ge>n. \<exists>j\<ge>n. emb (e i) (g j)"+
−
      proof (intro allI impI)+
−
        fix i assume "n \<le> i"+
−
        with * obtain j where "j \<ge> n"+
−
          and **: "emb (e i) (?g j)" by auto+
−
        show "\<exists>j\<ge>n. emb (e i) (g j)"+
−
        proof (cases "j \<le> n")+
−
          case True with ** show ?thesis+
−
            using `j \<ge> n` by auto+
−
        next+
−
          case False+
−
          with `j \<ge> n` have "j \<ge> Suc n" by auto+
−
          with ** have "emb (e i) (h j)" by auto+
−
          with greater obtain k where "k \<ge> Suc n"+
−
            and "emb (h j) (g k)" using `j \<ge> Suc n` by auto+
−
          with `emb (e i) (h j)` have "emb (e i) (g k)" by (auto intro: emb_trans)+
−
          moreover from `k \<ge> Suc n` have "k \<ge> n" by auto+
−
          ultimately show ?thesis by blast+
−
        qed+
−
      qed+
−
      from `mbp g n`[unfolded mbp_def] and 1 and 2 and 3 and 4+
−
        show "goodp emb e" by auto+
−
    qed+
−
    have bad: "bad emb ?g"+
−
      using bad_emb_repl[OF `bad emb g` `bad emb h`, of "Suc n",+
−
      OF greater] .+
−
    let ?g' = "repl (Suc n) g"+
−
    from 1(1)[of ?g n, OF emb' mbp bad] obtain M+
−
      where "\<forall>i\<le>n. M i = g i"+
−
      and "emb (M (Suc n)) (?g' h (Suc n))"+
−
      and *: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g' M i) (h j)"+
−
      and "bad emb (?g' M)"+
−
      and "mbp (?g' M) (Suc n)"+
−
      unfolding ex_repl_conv by auto+
−
    moreover with emb have "emb (M (Suc n)) (g (Suc n))" by (auto intro: emb_trans)+
−
    moreover have "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g' M i) (g j)"+
−
    proof (intro allI impI)+
−
      fix i assume "Suc n \<le> i"+
−
      with * obtain j where "j \<ge> Suc n" and "emb (?g' M i) (h j)" by auto+
−
      hence "j \<ge> Suc n" by auto+
−
      from greater and `j \<ge> Suc n` obtain k where "k \<ge> Suc n"+
−
        and "emb (h j) (g k)" by auto+
−
      with `emb (?g' M i) (h j)` show "\<exists>j\<ge>Suc n. emb (?g' M i) (g j)" by (blast intro: emb_trans)+
−
    qed+
−
    ultimately show ?thesis by blast+
−
  qed+
−
qed+
−
+
−
lemma choice2:+
−
  "\<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)"+
−
  using bchoice[of "{(x, y). P x y}" "\<lambda>(x, y) z. Q x y z"] by force+
−
+
−
fun minimal_bad_seq :: "('a seq \<Rightarrow> nat \<Rightarrow> 'a seq) \<Rightarrow> 'a seq \<Rightarrow> nat \<Rightarrow> 'a seq" where+
−
  "minimal_bad_seq A f 0 = A f 0"+
−
| "minimal_bad_seq A f (Suc n) = (+
−
    let g = minimal_bad_seq A f n in+
−
    repl (Suc n) g (A g n))"+
−
+
−
lemma bad_imp_mbp:+
−
  assumes "bad emb f"+
−
  shows "\<exists>g. (\<forall>i. \<exists>j. emb (g i) (f j)) \<and> mbp g 0 \<and> bad emb g"+
−
using assms+
−
proof (induct "f 0" arbitrary: f rule: wf_induct_rule[OF emb_wf])+
−
  case (1 g)+
−
  show ?case+
−
  proof (cases "mbp g 0")+
−
    case True with 1 show ?thesis by (blast intro: emb_refl)+
−
  next+
−
    case False+
−
    then obtain h where less: "\<forall>i<0. h i = g i"+
−
      and emb: "(h 0, g 0) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")+
−
      and greater: "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (h i) (g j)"+
−
      and bad: "bad emb h"+
−
      unfolding mbp_def by auto+
−
    from 1(1)[of h, OF emb bad] obtain e+
−
      where "\<forall>i. \<exists>j. emb (e i) (h j)" and "mbp e 0" and "bad emb e"+
−
      by auto+
−
    moreover with greater have "\<forall>i. \<exists>j. emb (e i) (g j)" by (force intro: emb_trans)+
−
    ultimately show ?thesis by blast+
−
  qed+
−
qed+
−
+
−
lemma repl_1 [simp]:+
−
  assumes "f 0 = g 0"+
−
  shows "repl (Suc 0) f g = g"+
−
proof+
−
  fix i show "repl (Suc 0) f g i = g i"+
−
    by (induct i) (simp_all add: assms)+
−
qed+
−
+
−
lemma bad_repl:+
−
  assumes "\<forall>i. f i \<ge> f 0" and "\<forall>i j. i > j \<longrightarrow> f i > f j"+
−
    and "bad P (repl (f 0) A B)" (is "bad P ?A")+
−
  shows "bad P (B \<circ> f)"+
−
proof+
−
  assume "goodp P (B \<circ> f)"+
−
  then obtain i j where "i < j" and "P\<^sup>=\<^sup>= (B (f i)) (B (f j))" by (auto simp: goodp_def)+
−
  hence "P\<^sup>=\<^sup>= (?A (f i)) (?A (f j))" using assms by auto+
−
  moreover from `i < j` have "f i < f j" using assms by auto+
−
  ultimately show False using assms(3) by (auto simp: goodp_def)+
−
qed+
−
+
−
lemma iterated_subseq:+
−
  assumes "\<forall>n>0::nat. \<forall>i\<ge>n. \<exists>j\<ge>n. emb (g n i) (g (n - 1) j)"+
−
    and "m \<le> n"+
−
  shows "\<forall>i\<ge>n. \<exists>j\<ge>m. emb (g n i) (g m j)"+
−
using assms(2)+
−
proof (induct "n - m" arbitrary: n)+
−
  case 0 thus ?case by auto+
−
next+
−
  case (Suc k)+
−
  then obtain n' where n: "n = Suc n'" by (cases n) auto+
−
  with Suc have "k = n' - m" and "m \<le> n'" by auto+
−
  have "n > 0" by (auto simp: n)+
−
  show ?case+
−
  proof (intro allI impI)+
−
    fix i assume "i \<ge> n"+
−
    with assms(1)[rule_format, OF `n > 0`] obtain j where "j \<ge> n"+
−
      and "emb (g (Suc n') i) (g n' j)" by (auto simp: n)+
−
    with Suc(1)[OF `k = n' - m` `m \<le> n'`, THEN spec[of _ j]]+
−
      obtain k where "k \<ge> m" and "emb (g n' j) (g m k)" by (auto simp: n)+
−
    with `emb (g (Suc n') i) (g n' j)` have "emb (g n i) (g m k)" by (auto intro: emb_trans simp: n)+
−
    thus "\<exists>j\<ge>m. emb (g n i) (g m j)" using `k \<ge> m` by blast+
−
  qed+
−
qed+
−
+
−
lemma no_bad_of_special_shape_imp_goodp:+
−
  assumes "\<not> (\<exists>f:: nat seq. (\<forall>i. f 0 \<le> f i) \<and> bad P (B \<circ> f))"+
−
    and "\<forall>i. f i \<in> {B i | i. True}"+
−
  shows "goodp P f"+
−
proof (rule ccontr)+
−
  assume "bad P f"+
−
  from assms(2) have "\<forall>i. \<exists>j. f i = B j" by blast+
−
  from choice[OF this] obtain g where "\<And>i. f i = B (g i)" by blast+
−
  with `bad P f` have "bad P (B \<circ> g)" by (auto simp: goodp_def)+
−
  have "\<forall>i. \<exists>j>i. g j \<ge> g 0"+
−
  proof (rule ccontr)+
−
    assume "\<not> ?thesis"+
−
    then obtain i::nat where "\<forall>j>i. \<not> (g j \<ge> g 0)" by auto+
−
    hence *: "\<forall>j>i. g j < g 0" by auto+
−
    let ?I = "{j. j > i}"+
−
    from * have "\<forall>j>i. g j \<in> {..<g 0}" by auto+
−
    hence "\<forall>j\<in>?I. g j \<in> {..<g 0}" by auto+
−
    hence "g ` ?I \<subseteq> {..<g 0}" unfolding image_subset_iff by auto+
−
    moreover have "finite {..<g 0}" by auto+
−
    ultimately have 1: "finite (g ` ?I)" using finite_subset by blast+
−
    have 2: "infinite ?I"+
−
    proof -+
−
      {+
−
      fix m have "\<exists>n>m. i < n"+
−
      proof (cases "m > i")+
−
        case True thus ?thesis by auto+
−
      next+
−
        case False+
−
        hence "m \<le> i" by auto+
−
        hence "Suc i > m" and "i < Suc i" by auto+
−
        thus ?thesis by blast+
−
      qed+
−
      }+
−
      thus ?thesis unfolding infinite_nat_iff_unbounded by auto+
−
    qed+
−
    from pigeonhole_infinite[OF 2 1]+
−
      obtain k where "k > i" and "infinite {j. j > i \<and> g j = g k}" by auto+
−
    then obtain l where "k < l" and "g l = g k"+
−
      unfolding infinite_nat_iff_unbounded by auto+
−
    hence "P\<^sup>=\<^sup>= (B (g k)) (B (g l))" by auto+
−
    with `k < l` and `bad P (B \<circ> g)` show False by (auto simp: goodp_def)+
−
  qed+
−
  from choice[OF this] obtain h+
−
    where "\<forall>i. (h i) > i" and *: "\<And>i. g (h i) \<ge> g 0" by blast+
−
  hence "\<forall>i\<ge>0. (h i) > i" by auto+
−
  from funpow_mono[OF this] have **: "\<And>i j. i < j \<Longrightarrow> (h ^^ i) 0 < (h ^^ j) 0" by auto+
−
  let ?i = "\<lambda>i. (h ^^ i) 0"+
−
  let ?f = "\<lambda>i. g (?i i)"+
−
  have "\<forall>i. ?f i \<ge> ?f 0"+
−
  proof+
−
    fix i show "?f i \<ge> ?f 0" using * by (induct i) auto+
−
  qed+
−
  moreover have "bad P (B \<circ> ?f)"+
−
  proof+
−
    assume "goodp P (B \<circ> ?f)"+
−
    then obtain i j where "i < j" and "P\<^sup>=\<^sup>= (B (?f i)) (B (?f j))" by (auto simp: goodp_def)+
−
    hence "P\<^sup>=\<^sup>= (B (g (?i i))) (B (g (?i j)))" by simp+
−
    moreover from **[OF `i < j`] have "?i i < ?i j" .+
−
    ultimately show False using `bad P (B \<circ> g)` by (auto simp: goodp_def)+
−
  qed+
−
  ultimately have "(\<forall>i. ?f i \<ge> ?f 0) \<and> bad P (B \<circ> ?f)" by auto+
−
  hence "\<exists>f. (\<forall>i. f i \<ge> f 0) \<and> bad P (B \<circ> f)" by (rule exI[of _ ?f])+
−
  with assms(1) show False by blast+
−
qed+
−
+
−
lemma emb_tl_left [simp]: "xs \<noteq> [] \<Longrightarrow> emb (tl xs) xs"+
−
  by (induct xs) auto+
−
+
−
lemma tl_ne [simp]: "xs \<noteq> [] \<Longrightarrow> tl xs = xs \<Longrightarrow> False"+
−
  by (induct xs) auto+
−
+
−
text {*Every reflexive and transitive relation on a finite set+
−
is a wqo.*}+
−
lemma finite_wqo_on:+
−
  fixes A :: "('a::finite) set"+
−
  assumes "reflp_on P A" and "transp_on P A"+
−
  shows "wqo_on P A"+
−
proof+
−
  fix f::"'a::finite seq"+
−
  assume *: "\<forall>i. f i \<in> A"+
−
  let ?I = "UNIV::nat set"+
−
  have "f ` ?I \<subseteq> A" using * by auto+
−
  with finite[of A] and finite_subset have 1: "finite (f ` ?I)" by blast+
−
  have "infinite ?I" by auto+
−
  from pigeonhole_infinite[OF this 1]+
−
    obtain k where "infinite {j. f j = f k}" by auto+
−
  then obtain l where "k < l" and "f l = f k"+
−
    unfolding infinite_nat_iff_unbounded by auto+
−
  hence "P\<^sup>=\<^sup>= (f k) (f l)" by auto+
−
  with `k < l` show "goodp P f" by (auto simp: goodp_def)+
−
qed fact++
−
+
−
lemma finite_eq_wqo_on:+
−
  "wqo_on (op =) (A::('a::finite) set)"+
−
  using finite_wqo_on[of "op =" A]+
−
  by (auto simp: reflp_on_def transp_on_def)+
−
+
−
lemma wqo_on_finite_lists:+
−
  shows "wqo_on emb (UNIV::('a::finite) list set)"+
−
    (is "wqo_on ?P ?A")+
−
proof -+
−
  {+
−
    from emb_refl+
−
      have "reflp_on ?P ?A" unfolding reflp_on_def by auto+
−
  }+
−
  note refl = this+
−
  {+
−
    from emb_trans+
−
      have "transp_on ?P ?A" unfolding transp_on_def by auto+
−
  }+
−
  note trans = this+
−
  {+
−
    have "\<forall>f. (\<forall>i. f i \<in> ?A) \<longrightarrow> goodp ?P f"+
−
    proof (rule ccontr)+
−
      assume "\<not> ?thesis"+
−
      then obtain f where "bad ?P f" by blast+
−
      from bad_imp_mbp[of f, OF `bad ?P f`] obtain g+
−
        where "\<forall>i. \<exists>j. emb (g i) (f j)"+
−
        and "mbp g 0"+
−
        and "bad ?P g"+
−
        by blast+
−
      from minimal_bad_element+
−
        have "\<forall>f n.+
−
        mbp f n \<and>+
−
        bad ?P f \<longrightarrow>+
−
        (\<exists>M.+
−
          (\<forall>i\<le>n. M i = f i) \<and>+
−
          emb (M (Suc n)) (f (Suc n)) \<and>+
−
          (\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (repl (Suc n) f M i) (f j)) \<and>+
−
          bad ?P (repl (Suc n) f M) \<and>+
−
          mbp (repl (Suc n) f M) (Suc n))"+
−
        (is "\<forall>f n. ?Q f n \<longrightarrow> (\<exists>M. ?Q' f n M)")+
−
        by blast+
−
      from choice2[OF this] obtain M+
−
        where *[rule_format]: "\<forall>f n. ?Q f n \<longrightarrow> ?Q' f n (M f n)" by force+
−
      let ?g = "minimal_bad_seq M g"+
−
      let ?A = "\<lambda>i. ?g i i"+
−
      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)"+
−
      proof+
−
        fix n+
−
        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)"+
−
        proof (induction n)+
−
          case 0+
−
          have "mbp g 0" by fact+
−
          moreover have "bad ?P g" by fact+
−
          ultimately+
−
            have [simp]: "M g 0 0 = g 0" and "emb (M g 0 (Suc 0)) (g (Suc 0))"+
−
            and "bad ?P (M g 0)" and "mbp (M g 0) (Suc 0)"+
−
            and **: "\<forall>i\<ge>Suc 0. \<exists>j\<ge>Suc 0. emb (M g 0 i) (g j)"+
−
            using *[of g 0] by auto+
−
          moreover have "mbp (M g 0) 0"+
−
          proof (unfold mbp_def, intro allI impI, elim conjE)+
−
            fix e :: "'a list seq"+
−
            presume "(e 0, g 0) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")+
−
              and *: "\<forall>i. \<exists>j\<ge>0. emb (e i) (M g 0 j)"+
−
            have "\<forall>i. \<exists>j\<ge>0::nat. emb (e i) (g j)"+
−
            proof (intro allI impI)+
−
              fix i+
−
              from * obtain j where "j \<ge> 0" and "emb (e i) (M g 0 j)" by auto+
−
              show "\<exists>j\<ge>0. emb (e i) (g j)"+
−
              proof (cases "j = 0")+
−
                case True+
−
                with `emb (e i) (M g 0 j)` have "emb (e i) (g 0)" by auto+
−
                thus ?thesis by auto+
−
              next+
−
                case False+
−
                hence "j \<ge> Suc 0" by auto+
−
                with ** obtain k where "k \<ge> Suc 0" and "emb (M g 0 j) (g k)" by auto+
−
                with `emb (e i) (M g 0 j)` have "emb (e i) (g k)" by (blast intro: emb_trans)+
−
                moreover with `k \<ge> Suc 0` have "k \<ge> 0" by auto+
−
                ultimately show ?thesis by blast+
−
              qed+
−
            qed+
−
            with `mbp g 0`[unfolded mbp_def]+
−
            show "goodp ?P e" using `(e 0, g 0) \<in> ?emb` by (simp add: mbp_def)+
−
          qed auto+
−
          moreover have "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (?g 0 i) (g j)"+
−
          proof (intro allI impI)+
−
            fix i::nat+
−
            assume "i \<ge> 0"+
−
            hence "i = 0 \<or> i \<ge> Suc 0" by auto+
−
            thus "\<exists>j\<ge>0. emb (?g 0 i) (g j)"+
−
            proof+
−
              assume "i \<ge> Suc 0"+
−
              with ** obtain j where "j \<ge> Suc 0" and "emb (?g 0 i) (g j)" by auto+
−
              moreover from this have "j \<ge> 0" by auto+
−
              ultimately show "?thesis" by auto+
−
            next+
−
              assume "i = 0"+
−
              hence "emb (?g 0 i) (g 0)" by auto+
−
              thus ?thesis by blast+
−
            qed+
−
          qed+
−
          ultimately show ?case by simp+
−
        next+
−
          case (Suc n)+
−
          with *[of "?g n" n]+
−
            have eq: "\<forall>i\<le>n. ?A i = ?g n i"+
−
            and emb: "emb (?g (Suc n) (Suc n)) (?g n (Suc n))"+
−
            and subseq: "\<forall>i\<ge>Suc n. \<exists>j\<ge>Suc n. emb (?g (Suc n) i) (?g n j)"+
−
            and "bad ?P (?g (Suc n))"+
−
            and mbp: "mbp (?g (Suc n)) (Suc n)"+
−
            by (simp_all add: Let_def)+
−
          moreover have *: "\<forall>i\<le>Suc n. ?A i = ?g (Suc n) i"+
−
          proof (intro allI impI)+
−
            fix i assume "i \<le> Suc n"+
−
            show "?A i = ?g (Suc n) i"+
−
            proof (cases "i = Suc n")+
−
              assume "i = Suc n"+
−
              thus ?thesis by simp+
−
            next+
−
              assume "i \<noteq> Suc n"+
−
              with `i \<le> Suc n` have "i < Suc n" by auto+
−
              thus ?thesis by (simp add: Let_def eq)+
−
            qed+
−
          qed+
−
          moreover have "\<forall>i\<le>Suc n. mbp (?g (Suc n)) i"+
−
          proof (intro allI impI)+
−
            fix i assume "i \<le> Suc n"+
−
            show "mbp (?g (Suc n)) i"+
−
            proof (cases "i = Suc n")+
−
              case True with mbp show ?thesis by simp+
−
            next+
−
              case False with `i \<le> Suc n` have le: "i \<le> Suc n" "i \<le> n" by auto+
−
              show ?thesis+
−
              proof (unfold mbp_def, intro allI impI, elim conjE)+
−
                fix e+
−
                note * = *[rule_format, symmetric] eq[rule_format, symmetric]+
−
                assume "\<forall>i'<i. e i' = ?g (Suc n) i'"+
−
                hence 1: "\<forall>i'<i. e i' = ?g n i'" using * and le by auto+
−
                presume "(e i, ?g (Suc n) i) \<in> {(x, y). emb x y \<and> x \<noteq> y}" (is "_ \<in> ?emb")+
−
                hence 2: "(e i, ?g n i) \<in> ?emb" using * and le by simp+
−
                assume **: "\<forall>j\<ge>i. \<exists>k\<ge>i. emb (e j) (?g (Suc n) k)"+
−
                have 3: "\<forall>j\<ge>i. \<exists>k\<ge>i. emb (e j) (?g n k)"+
−
                proof (intro allI impI)+
−
                  fix j assume "i \<le> j"+
−
                  with ** obtain k where "k \<ge> i" and "emb (e j) (?g (Suc n) k)" by blast+
−
                  show "\<exists>k\<ge>i. emb (e j) (?g n k)"+
−
                  proof (cases "k \<le> n")+
−
                    case True with `emb (e j) (?g (Suc n) k)`+
−
                      have "emb (e j) (?g n k)" using * by auto+
−
                    thus ?thesis using `k \<ge> i` by auto+
−
                  next+
−
                    case False hence "k \<ge> Suc n" by auto+
−
                    with subseq obtain l where "l \<ge> Suc n"+
−
                      and "emb (?g (Suc n) k) (?g n l)" by blast+
−
                    with `emb (e j) (?g (Suc n) k)` have "emb (e j) (?g n l)" by (auto intro: emb_trans)+
−
                    moreover from `i \<le> Suc n` and `l \<ge> Suc n` have "l \<ge> i" by auto+
−
                    ultimately show ?thesis by blast+
−
                  qed+
−
                qed+
−
                from 1 2 3 and Suc[THEN conjunct2, THEN conjunct2] and `i \<le> n`+
−
                show "goodp ?P e" unfolding mbp_def by blast+
−
              qed simp+
−
            qed+
−
          qed+
−
          ultimately show ?case by simp+
−
        qed+
−
      qed+
−
      hence 1: "\<forall>n. \<forall>i\<le>n. mbp (?g n) i"+
−
        and 2: "\<forall>n. \<forall>i\<le>n. ?A i = ?g n i"+
−
        and 3: "\<forall>n. bad ?P (?g n)"+
−
        and 6: "\<forall>i\<ge>0. \<exists>j\<ge>0. emb (?g 0 i) (g j)"+
−
        and 7: "\<forall>n>0. \<forall>i\<ge>n. \<exists>j\<ge>n. emb (?g n i) (?g (n - 1) j)"+
−
        by auto+
−
      have ex_subset: "\<forall>n. \<forall>i. \<exists>j. emb (?g n i) (g j)"+
−
      proof+
−
        fix n show "\<forall>i. \<exists>j. emb (?g n i) (g j)"+
−
        proof (induct n)+
−
          case 0 with 6 show ?case by simp+
−
        next+
−
          case (Suc n)+
−
          show ?case+
−
          proof+
−
            fix i+
−
            have "i < Suc n \<or> i \<ge> Suc n" by auto+
−
            thus "\<exists>j. emb (?g (Suc n) i) (g j)"+
−
            proof+
−
              assume "i < Suc n" hence "i \<le> Suc n" and "i \<le> n" by auto+
−
              from `i \<le> Suc n` have "?g (Suc n) i = ?g i i" using 2 by auto+
−
              moreover from `i \<le> n` have "?g n i = ?g i i" using 2 by auto+
−
              ultimately have "?g (Suc n) i = ?g n i" by auto+
−
              with Suc show ?thesis by auto+
−
            next+
−
              assume "i \<ge> Suc n"+
−
              with 7[THEN spec[of _ "Suc n"]]+
−
                obtain j where "j \<ge> Suc n" and "emb (?g (Suc n) i) (?g n j)" by auto+
−
              moreover from Suc obtain k where "emb (?g n j) (g k)" by blast+
−
              ultimately show ?thesis by (blast intro: emb_trans)+
−
            qed+
−
          qed+
−
        qed+
−
      qed+
−
      have bad: "bad ?P ?A"+
−
      proof+
−
        assume "goodp ?P ?A"+
−
        then obtain i j :: nat where "i < j"+
−
          and "?P\<^sup>=\<^sup>= (?g i i) (?g j j)" unfolding goodp_def by auto+
−
        moreover with 2[rule_format, of i j]+
−
          have "?P\<^sup>=\<^sup>= (?g j i) (?g j j)" by auto+
−
        ultimately have "goodp ?P (?g j)" unfolding goodp_def by blast+
−
        with 3 show False by auto+
−
      qed+
−
      have non_empty: "\<forall>i. ?A i \<noteq> []" using bad and bad_imp_not_empty[of ?A] by auto+
−
      then obtain a as where a: "\<forall>i. hd (?A i) = a i \<and> tl (?A i) = as i" by force+
−
      let ?B = "\<lambda>i. tl (?A i)"+
−
      {+
−
        assume "\<exists>f::nat seq. (\<forall>i. f i \<ge> f 0) \<and> bad ?P (?B \<circ> f)"+
−
        then obtain f :: "nat seq" where ge: "\<forall>i. f i \<ge> f 0"+
−
          and "bad ?P (?B \<circ> f)" by auto+
−
        let ?C = "\<lambda>i. if i < f 0 then ?A i else ?B (f (i - f 0))"+
−
        have [simp]: "\<And>i. i < f 0 \<Longrightarrow> ?C i = ?A i" by auto+
−
        have [simp]: "\<And>i. f 0 \<le> i \<Longrightarrow> ?C i = ?B (f (i - f 0))" by auto+
−
        have "bad ?P ?C"+
−
        proof+
−
          assume "goodp ?P ?C"+
−
          then obtain i j where "i < j" and *: "?P\<^sup>=\<^sup>= (?C i) (?C j)" by (auto simp: goodp_def)+
−
          {+
−
            assume "j < f 0" with `i < j` and * have "?P\<^sup>=\<^sup>= (?A i) (?A j)" by simp+
−
            with `i < j` and `bad ?P ?A` have False by (auto simp: goodp_def)+
−
          } moreover {+
−
            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+
−
            moreover with `i < j` and `f 0 \<le> i` have "i - f 0 < j - f 0" by auto+
−
            ultimately have False using `bad ?P (?B \<circ> f)` by (auto simp: goodp_def)+
−
          } moreover {+
−
            have emb: "emb (?B (f (j - f 0))) (?A (f (j - f 0)))" using non_empty by simp+
−
            assume "i < f 0" and "f 0 \<le> j"+
−
            with * have "?P\<^sup>=\<^sup>= (?A i) (?B (f (j - f 0)))" by auto+
−
            hence "?P (?A i) (?B (f (j - f 0))) \<or> ?A i = ?B (f (j - f 0))" by simp+
−
            hence False+
−
            proof+
−
              assume "?P (?A i) (?B (f (j - f 0)))"+
−
              with emb have "?P (?A i) (?A (f (j - f 0)))" by (blast intro: emb_trans)+
−
              moreover from ge[THEN spec[of _ "j - f 0"]] and `i < f 0` have "i < f (j - f 0)" by auto+
−
              ultimately show ?thesis using `bad ?P ?A` by (auto simp: goodp_def)+
−
            next+
−
              assume "?A i = ?B (f (j - f 0))"+
−
              with emb have "emb (?A i) (?A (f (j - f 0)))" by auto+
−
              moreover have "?P (?A i) (?A i)" using emb_refl by auto+
−
              ultimately have "?P (?A i) (?A (f (j - f 0)))" by (blast intro: emb_trans)+
−
              moreover from ge[THEN spec[of _ "j - f 0"]] and `i < f 0` have "i < f (j - f 0)" by auto+
−
              ultimately show ?thesis using `bad ?P ?A` by (auto simp: goodp_def)+
−
            qed+
−
          } ultimately show False by arith+
−
        qed+
−
        have "\<forall>i<f 0. ?C i = ?g (f 0) i" using 2 by auto+
−
        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+
−
        moreover have "\<forall>i\<ge>f 0. \<exists>j\<ge>f 0. emb (?C i) (?g (f 0) j)"+
−
        proof (intro allI impI)+
−
          fix i+
−
          let ?i = "f (i - f 0)"+
−
          assume "f 0 \<le> i"+
−
          with `\<forall>i. f 0 \<le> f i` have "f 0 \<le> ?i" by auto+
−
          from `f 0 \<le> i` have *: "?C i = ?B ?i" by auto+
−
          have "emb (?C i) (?g ?i ?i)" unfolding * using non_empty emb_tl_left by auto+
−
          from iterated_subseq[OF 7, of "f 0" "?i", THEN spec[of _ "?i"], OF `f 0 \<le> ?i`]+
−
            obtain j where "j \<ge> f 0" and "emb (?g ?i ?i) (?g (f 0) j)" by blast+
−
          with `emb (?C i) (?g ?i ?i)`+
−
            show "\<exists>j\<ge>f 0. emb (?C i) (?g (f 0) j)" by (blast intro: emb_trans)+
−
        qed+
−
        ultimately have "goodp ?P ?C"+
−
          using 1[rule_format, of "f 0", OF le_refl, unfolded mbp_def] by auto+
−
        with `bad ?P ?C` have False by blast+
−
      }+
−
      hence no_index: "\<not> (\<exists>f. (\<forall>i. f 0 \<le> f i) \<and> bad ?P (?B \<circ> f))" by blast+
−
      let ?B' = "{?B i | i. True}"+
−
      have subset: "?B' \<subseteq> UNIV" by auto+
−
      have "wqo_on ?P ?B'"+
−
      proof+
−
        from emb_refl show "reflp_on ?P ?B'" by (auto simp: reflp_on_def)+
−
      next+
−
        from emb_trans show "transp_on ?P ?B'" by (auto simp: transp_on_def)+
−
      next+
−
        fix f :: "'a list seq" assume "\<forall>i. f i \<in> ?B'"+
−
        from no_bad_of_special_shape_imp_goodp[of ?P ?B f, OF no_index this]+
−
          show "goodp ?P f" .+
−
      qed+
−
      let ?a' = "{a i | i. True}"+
−
      have "?a' \<subseteq> UNIV" by auto+
−
      with finite_eq_wqo_on+
−
        have "wqo_on op = ?a'"+
−
        using finite[of UNIV] and finite_subset by blast+
−
      from wqo_on_Sigma[OF `wqo_on op = ?a'` `wqo_on ?P ?B'`]+
−
        have wqo: "wqo_on (prod_le op = ?P) (?a' \<times> ?B')" .+
−
      let ?aB = "\<lambda>i. (a i, ?B i)"+
−
      let ?P' = "prod_le op = ?P"+
−
      have "\<forall>i. ?aB i \<in> (?a' \<times> ?B')" by auto+
−
      with wqo have "goodp ?P' ?aB" unfolding wqo_on_def by auto+
−
      then obtain i j where "i < j" and *: "?P'\<^sup>=\<^sup>= (?aB i) (?aB j)"+
−
        by (auto simp: goodp_def)+
−
      from hd_Cons_tl and non_empty+
−
        have hd_tl: "hd (?A i) # tl (?A i) = ?A i"+
−
          "hd (?A j) # tl (?A j) = ?A j" by auto+
−
      from * have "(a i = a j \<and> ?B i = ?B j) \<or> (a i = a j \<and> ?P (?B i) (?B j))"+
−
        unfolding prod_le_def by auto+
−
      thus False+
−
      proof+
−
        assume *: "a i = a j \<and> ?B i = ?B j"+
−
        hence "?A i = ?A j" using a and hd_tl by auto+
−
        hence "?P\<^sup>=\<^sup>= (?A i) (?A j)" by auto+
−
        with `i < j` and `bad ?P ?A` show False by (auto simp: goodp_def)+
−
      next+
−
        assume "op = (a i) (a j) \<and> ?P (?B i) (?B j)"+
−
        hence *: "op = (a i) (a j)" and **: "?P (?B i) (?B j)" by auto+
−
        with emb_appendI[OF emb_refl[of "[hd (?A i)]"] **]+
−
          have "emb (?A i) (?A j)" using hd_tl a by simp+
−
        hence "?P\<^sup>=\<^sup>= (?A i) (?A j)" by auto+
−
        with `i < j` and `bad ?P ?A` show False by (auto simp: goodp_def)+
−
      qed+
−
    qed+
−
  }+
−
  with refl and trans show ?thesis unfolding wqo_on_def by blast+
−
qed+
−
+
−
lemma Higman_antichains:+
−
  fixes A :: "('a::finite) list set"+
−
  assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(emb x y) \<and> \<not>(emb y x)"+
−
  shows "finite A"+
−
proof (rule ccontr)+
−
  assume "infinite A"+
−
  then obtain f :: "nat \<Rightarrow> ('a::finite) list" where b: "inj f" and c: "range f \<subseteq> A"+
−
    by (auto simp add: infinite_iff_countable_subset)+
−
  from wqo_on_imp_goodp[OF wqo_on_finite_lists, simplified, of f]+
−
    obtain i j where d: "i < j" and e: "emb (f i) (f j)" by (auto simp: goodp_def)+
−
  have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)+
−
  moreover+
−
  have "f i \<in> A" using c by auto+
−
  moreover+
−
  have "f j \<in> A" using c by auto+
−
  ultimately have "\<not> (emb (f i) (f j))" using a by simp+
−
  with e show "False" by simp+
−
qed+
−
+
−
end+
−