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))"