# HG changeset patch
# User urbanc
# Date 1346245776 0
# Node ID 2d6beddb6fa6bcab2f730dda3dc1e9f154f2aecb
# Parent  79401279ba21c902453cb2c30406d873563f1755
some addition to the MN-paper

diff -r 79401279ba21 -r 2d6beddb6fa6 Closures2.thy
--- a/Closures2.thy	Wed Aug 29 13:05:46 2012 +0000
+++ b/Closures2.thy	Wed Aug 29 13:09:36 2012 +0000
@@ -1,7 +1,8 @@
 theory Closures2
 imports 
   Closures
-  Higman
+  (*Higman*)
+  WQO_Finite_Lists
 begin
 
 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
@@ -14,6 +15,7 @@
 declare  emb1 [intro]
 declare  emb2 [intro]
 
+(*
 lemma letter_UNIV:
   shows "UNIV = {A, B::letter}"
 apply(auto)
@@ -29,7 +31,7 @@
 hide_const A
 hide_const B
 hide_const R
-
+*)
 (*
 inductive 
   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
@@ -190,16 +192,16 @@
 | "UP (Star r) = Star Allreg"
 
 lemma lang_UP:
-  fixes r::"letter rexp"
+  fixes r::"'a::finite rexp"
   shows "lang (UP r) = SUPSEQ (lang r)"
 by (induct r) (simp_all)
 
 lemma regular_SUPSEQ: 
-  fixes A::"letter lang"
+  fixes A::"('a::finite) lang"
   assumes "regular A"
   shows "regular (SUPSEQ A)"
 proof -
-  from assms obtain r::"letter rexp" where "lang r = A" by auto
+  from assms obtain r::"'a::finite rexp" where "lang r = A" by auto
   then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP)
   then show "regular (SUPSEQ A)" by auto
 qed
@@ -236,6 +238,7 @@
   ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp
 qed
 
+(*
 lemma Higman_antichains:
   assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
   shows "finite A"
@@ -252,13 +255,15 @@
   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   with e show "False" by simp
 qed
+*)
 
 definition
-  minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
+  minimal :: "'a::finite list \<Rightarrow> 'a lang \<Rightarrow> bool"
 where
   "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
 
 lemma main_lemma:
+  fixes A::"('a::finite) list set" 
   shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
 proof -
   def M \<equiv> "{x \<in> A. minimal x A}"
@@ -288,7 +293,7 @@
 qed
 
 lemma closure_SUPSEQ:
-  fixes A::"letter lang" 
+  fixes A::"'a::finite lang" 
   shows "regular (SUPSEQ A)"
 proof -
   obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"
@@ -299,7 +304,7 @@
 qed
 
 lemma closure_SUBSEQ:
-  fixes A::"letter lang"
+  fixes A::"'a::finite lang"
   shows "regular (SUBSEQ A)"
 proof -
   have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)
diff -r 79401279ba21 -r 2d6beddb6fa6 Seq.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Seq.thy	Wed Aug 29 13:09:36 2012 +0000
@@ -0,0 +1,541 @@
+(*  Title:       Infinite Sequences
+    Author:      Christian Sternagel <c-sterna@jaist.ac.jp>
+                 René Thiemann       <rene.thiemann@uibk.ac.at>
+    Maintainer:  Christian Sternagel and René Thiemann
+    License:     LGPL
+*)
+
+(*
+Copyright 2012 Christian Sternagel, René Thiemann
+
+This file is part of IsaFoR/CeTA.
+
+IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
+terms of the GNU Lesser General Public License as published by the Free Software
+Foundation, either version 3 of the License, or (at your option) any later
+version.
+
+IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
+WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.
+
+You should have received a copy of the GNU Lesser General Public License along
+with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
+*)
+header {* Infinite Sequences *}
+theory Seq
+imports
+  Main
+  "~~/src/HOL/Library/Infinite_Set"
+begin
+
+text {*Infinite sequences are represented by functions of type @{typ "nat \<Rightarrow> 'a"}.*}
+type_synonym 'a seq = "nat \<Rightarrow> 'a"
+
+subsection {*Operations on Infinite Sequences*}
+
+text {*Adding a new element at the front.*}
+abbreviation cons :: "'a \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "#s" 65) where (*FIXME: find better infix symbol*)
+  "x #s S \<equiv> (\<lambda>i. case i of 0 \<Rightarrow> x | Suc n \<Rightarrow> S n)"
+
+text {*An infinite sequence is \emph{linked} by a binary predicate @{term P} if every two
+consecutive elements satisfy it. Such a sequence is called a \emph{@{term P}-chain}. *}
+abbreviation (input) chainp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a seq \<Rightarrow> bool" where
+  "chainp P S \<equiv> \<forall>i. P (S i) (S (Suc i))"
+
+text {*Special version for relations.*}
+abbreviation (input) chain :: "'a rel \<Rightarrow> 'a seq \<Rightarrow> bool" where
+  "chain r S \<equiv> chainp (\<lambda>x y. (x, y) \<in> r) S"
+
+text {*Extending a chain at the front.*}
+lemma cons_chainp:
+  assumes "P x (S 0)" and "chainp P S"
+  shows "chainp P (x #s S)" (is "chainp P ?S")
+proof
+  fix i show "P (?S i) (?S (Suc i))" using assms by (cases i) simp_all
+qed
+
+text {*Special version for relations.*}
+lemma cons_chain:
+  assumes "(x, S 0) \<in> r" and "chain r S" shows "chain r (x #s S)"
+  using cons_chainp[of "\<lambda>x y. (x, y) \<in> r", OF assms] .
+
+text {*A chain admits arbitrary transitive steps.*}
+lemma chainp_imp_relpowp:
+  assumes "chainp P S" shows "(P^^j) (S i) (S (i + j))"
+proof (induct "i + j" arbitrary: j)
+  case (Suc n) thus ?case using assms by (cases j) auto
+qed simp
+
+lemma chain_imp_relpow:
+  assumes "chain r S" shows "(S i, S (i + j)) \<in> r^^j"
+proof (induct "i + j" arbitrary: j)
+  case (Suc n) thus ?case using assms by (cases j) auto
+qed simp
+
+lemma chainp_imp_tranclp:
+  assumes "chainp P S" and "i < j" shows "P^++ (S i) (S j)"
+proof -
+  from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto
+  with chainp_imp_relpowp[of P S "Suc n" i, OF assms(1)]
+    show ?thesis
+      unfolding trancl_power[of "(S i, S j)", to_pred]
+      by force
+qed
+
+lemma chain_imp_trancl:
+  assumes "chain r S" and "i < j" shows "(S i, S j) \<in> r^+"
+proof -
+  from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto
+  with chain_imp_relpow[OF assms(1), of i "Suc n"]
+    show ?thesis unfolding trancl_power by force
+qed
+
+text {*A chain admits arbitrary reflexive and transitive steps.*}
+lemma chainp_imp_rtranclp:
+  assumes "chainp P S" and "i \<le> j" shows "P^** (S i) (S j)"
+proof -
+  from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+
+  with chainp_imp_relpowp[of P S, OF assms(1), of n i] show ?thesis
+    by (simp add: relpow_imp_rtrancl[of "(S i, S (i + n))", to_pred])
+qed
+
+lemma chain_imp_rtrancl:
+  assumes "chain r S" and "i \<le> j" shows "(S i, S j) \<in> r^*"
+proof -
+  from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+
+  with chain_imp_relpow[OF assms(1), of i n] show ?thesis by (simp add: relpow_imp_rtrancl)
+qed
+
+text {*If for every @{term i} there is a later index @{term "f i"} such that the
+corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.*}
+lemma stepfun_imp_chainp:
+  assumes "\<forall>i\<ge>n::nat. f i > i \<and> P (S i) (S (f i))"
+  shows "chainp P (\<lambda>i. S ((f ^^ i) n))" (is "chainp P ?T")
+proof
+  fix i
+  from assms have "(f ^^ i) n \<ge> n" by (induct i) auto
+  with assms[THEN spec[of _ "(f ^^ i) n"]]
+    show "P (?T i) (?T (Suc i))" by simp
+qed
+
+text {*If for every @{term i} there is a later index @{term j} such that the
+corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.*}
+lemma steps_imp_chainp:
+  assumes "\<forall>i\<ge>n::nat. \<exists>j>i. P (S i) (S j)" shows "\<exists>T. chainp P T"
+proof -
+  from assms have "\<forall>i\<in>{i. i \<ge> n}. \<exists>j>i. P (S i) (S j)" by auto
+  from bchoice[OF this]
+    obtain f where seq: "\<forall>i\<ge>n. f i > i \<and> P (S i) (S (f i))" by auto
+  from stepfun_imp_chainp[of n f P S, OF this] show ?thesis by fast
+qed
+
+
+subsection {* Predicates on Natural Numbers *}
+
+text {*If some property holds for infinitely many natural numbers, obtain
+an index function that points to these numbers in increasing order.*}
+
+locale infinitely_many =
+  fixes p :: "nat \<Rightarrow> bool"
+  assumes infinite: "INFM j. p j"
+begin
+
+lemma inf: "\<exists>j\<ge>i. p j" using infinite[unfolded INFM_nat_le] by auto
+
+fun index :: "nat seq" where
+  "index 0 = (LEAST n. p n)"
+| "index (Suc n) = (LEAST k. p k \<and> k > index n)"
+
+lemma index_p: "p (index n)"
+proof (induct n)
+  case 0
+  from inf obtain j where "p j" by auto
+  with LeastI[of p j] show ?case by auto
+next
+  case (Suc n)
+  from inf obtain k where "k \<ge> Suc (index n) \<and> p k" by auto
+  with LeastI[of "\<lambda> k. p k \<and> k > index n" k] show ?case by auto
+qed
+
+lemma index_ordered: "index n < index (Suc n)"
+proof -
+  from inf obtain k where "k \<ge> Suc (index n) \<and> p k" by auto
+  with LeastI[of "\<lambda> k. p k \<and> k > index n" k] show ?thesis by auto
+qed
+
+lemma index_not_p_between:
+  assumes i1: "index n < i"
+    and i2: "i < index (Suc n)"
+  shows "\<not> p i"
+proof -
+  from not_less_Least[OF i2[simplified]] i1 show ?thesis by auto
+qed
+
+lemma index_ordered_le:
+  assumes "i \<le> j" shows "index i \<le> index j"
+proof - 
+  from assms have "j = i + (j - i)" by auto
+  then obtain k where j: "j = i + k" by auto
+  have "index i \<le> index (i + k)"
+  proof (induct k)
+    case (Suc k)
+    with index_ordered[of "i + k"]
+    show ?case by auto
+  qed simp
+  thus ?thesis unfolding j .
+qed
+
+lemma index_surj:
+  assumes "k \<ge> index l"
+  shows "\<exists>i j. k = index i + j \<and> index i + j < index (Suc i)"
+proof -
+  from assms have "k = index l + (k - index l)" by auto
+  then obtain u where k: "k = index l + u" by auto
+  show ?thesis unfolding k
+  proof (induct u)
+    case 0
+    show ?case
+      by (intro exI conjI, rule refl, insert index_ordered[of l], simp)
+  next
+    case (Suc u)
+    then obtain i j
+      where lu: "index l + u = index i + j" and lt: "index i + j < index (Suc i)" by auto
+    hence "index l + u < index (Suc i)" by auto
+    show ?case
+    proof (cases "index l + (Suc u) = index (Suc i)")
+      case False
+      show ?thesis
+        by (rule exI[of _ i], rule exI[of _ "Suc j"], insert lu lt False, auto)
+    next
+      case True
+      show ?thesis
+        by (rule exI[of _ "Suc i"], rule exI[of _ 0], insert True index_ordered[of "Suc i"], auto)
+    qed
+  qed
+qed
+
+lemma index_ordered_less:
+  assumes "i < j" shows "index i < index j"
+proof - 
+  from assms have "Suc i \<le> j" by auto
+  from index_ordered_le[OF this]
+  have "index (Suc i) \<le> index j" .
+  with index_ordered[of i] show ?thesis by auto
+qed
+
+lemma index_not_p_start: assumes i: "i < index 0" shows "\<not> p i"
+proof -
+  from i[simplified index.simps] have "i < Least p" .
+  from not_less_Least[OF this] show ?thesis .
+qed
+
+end
+
+
+subsection {* Assembling Infinite Words from Finite Words *}
+
+text {*Concatenate infinitely many non-empty words to an infinite word.*}
+
+fun inf_concat_simple :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> (nat \<times> nat)" where
+  "inf_concat_simple f 0 = (0, 0)"
+| "inf_concat_simple f (Suc n) = (
+    let (i, j) = inf_concat_simple f n in 
+    if Suc j < f i then (i, Suc j)
+    else (Suc i, 0))"
+
+lemma inf_concat_simple_add:
+  assumes ck: "inf_concat_simple f k = (i, j)"
+    and jl: "j + l < f i"
+  shows "inf_concat_simple f (k + l) = (i,j + l)"
+using jl
+proof (induct l)
+  case 0
+  thus ?case using ck by simp
+next
+  case (Suc l)
+  hence c: "inf_concat_simple f (k + l) = (i, j+ l)" by auto
+  show ?case 
+    by (simp add: c, insert Suc(2), auto)
+qed
+
+lemma inf_concat_simple_surj_zero: "\<exists> k. inf_concat_simple f k = (i,0)"
+proof (induct i)
+  case 0
+  show ?case 
+    by (rule exI[of _ 0], simp)
+next
+  case (Suc i)
+  then obtain k where ck: "inf_concat_simple f k = (i,0)" by auto
+  show ?case
+  proof (cases "f i")
+    case 0
+    show ?thesis
+      by (rule exI[of _ "Suc k"], simp add: ck 0)
+  next
+    case (Suc n)
+    hence "0 + n < f i" by auto
+    from inf_concat_simple_add[OF ck, OF this] Suc
+    show ?thesis
+      by (intro exI[of _ "k + Suc n"], auto)
+  qed
+qed
+
+lemma inf_concat_simple_surj:
+  assumes "j < f i"
+  shows "\<exists> k. inf_concat_simple f k = (i,j)"
+proof -
+  from assms have j: "0 + j < f i" by auto
+  from inf_concat_simple_surj_zero obtain k where "inf_concat_simple f k = (i,0)" by auto
+  from inf_concat_simple_add[OF this, OF j] show ?thesis by auto
+qed
+
+lemma inf_concat_simple_mono:
+  assumes "k \<le> k'" shows "fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')"
+proof -
+  from assms have "k' = k + (k' - k)" by auto
+  then obtain l where k': "k' = k + l" by auto
+  show ?thesis  unfolding k'
+  proof (induct l)
+    case (Suc l)
+    obtain i j where ckl: "inf_concat_simple f (k+l) = (i,j)" by (cases "inf_concat_simple f (k+l)", auto)
+    with Suc have "fst (inf_concat_simple f k) \<le> i" by auto
+    also have "... \<le> fst (inf_concat_simple f (k + Suc l))"
+      by (simp add: ckl)
+    finally show ?case .
+  qed simp
+qed
+
+
+(* inf_concat assembles infinitely many (possibly empty) words to an infinite word *)
+fun inf_concat :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
+  "inf_concat n 0 = (LEAST j. n j > 0, 0)"
+| "inf_concat n (Suc k) = (let (i, j) = inf_concat n k in (if Suc j < n i then (i, Suc j) else (LEAST i'. i' > i \<and> n i' > 0, 0)))"
+
+lemma inf_concat_bounds:
+  assumes inf: "INFM i. n i > 0"
+    and res: "inf_concat n k = (i,j)"
+  shows "j < n i"
+proof (cases k)
+  case 0
+  with res have i: "i = (LEAST i. n i > 0)" and j: "j = 0" by auto
+  from inf[unfolded INFM_nat_le] obtain i' where i': "0 < n i'" by auto
+  have "0 < n (LEAST i. n i > 0)" 
+    by (rule LeastI, rule i')
+  with i j show ?thesis by auto
+next
+  case (Suc k')
+  obtain i' j' where res': "inf_concat n k' = (i',j')" by force
+  note res = res[unfolded Suc inf_concat.simps res' Let_def split]
+  show ?thesis 
+  proof (cases "Suc j' < n i'")
+    case True
+    with res show ?thesis by auto
+  next
+    case False
+    with res have i: "i = (LEAST f. i' < f \<and> 0 < n f)" and j: "j = 0" by auto
+    from inf[unfolded INFM_nat] obtain f where f: "i' < f \<and> 0 < n f" by auto
+    have "0 < n (LEAST f. i' < f \<and> 0 < n f)"
+      using LeastI[of "\<lambda> f. i' < f \<and> 0 < n f", OF f]
+      by auto
+    with i j show ?thesis by auto
+  qed
+qed
+
+lemma inf_concat_add:
+  assumes res: "inf_concat n k = (i,j)"
+    and j: "j + m < n i"
+  shows "inf_concat n (k + m) = (i,j+m)"
+  using j
+proof (induct m)
+  case 0 show ?case using res by auto
+next
+  case (Suc m)
+  hence "inf_concat n (k + m) = (i, j+m)" by auto
+  with Suc(2)
+  show ?case by auto
+qed
+
+lemma inf_concat_step:
+  assumes res: "inf_concat n k = (i,j)"
+    and j: "Suc (j + m) = n i"
+  shows "inf_concat n (k + Suc m) = (LEAST i'. i' > i \<and> 0 < n i', 0)"
+proof -
+  from j have "j + m < n i" by auto
+  note res = inf_concat_add[OF res, OF this]
+  show ?thesis by (simp add: res j)
+qed
+
+lemma inf_concat_surj_zero:
+  assumes "0 < n i"
+  shows "\<exists>k. inf_concat n k = (i, 0)"
+proof -
+  {
+    fix l
+    have "\<forall> j. j < l \<and> 0 < n j \<longrightarrow> (\<exists> k. inf_concat n k = (j,0))"
+    proof (induct l)
+      case 0
+      thus ?case by auto
+    next
+      case (Suc l)
+      show ?case
+      proof (intro allI impI, elim conjE)
+        fix j
+        assume j: "j < Suc l" and nj: "0 < n j"
+        show "\<exists> k. inf_concat n k = (j, 0)"
+        proof (cases "j < l")
+          case True
+          from Suc[THEN spec[of _ j]] True nj show ?thesis by auto
+        next
+          case False
+          with j have j: "j = l" by auto
+          show ?thesis
+          proof (cases "\<exists> j'. j' < l \<and> 0 < n j'")
+            case False
+            have l: "(LEAST i. 0 < n i) = l"
+            proof (rule Least_equality, rule nj[unfolded j])
+              fix l'
+              assume "0 < n l'"
+              with False have "\<not> l' < l" by auto
+              thus "l \<le> l'" by auto
+            qed
+            show ?thesis
+              by (rule exI[of _ 0], simp add: l j)
+          next
+            case True
+            then obtain lll where lll: "lll < l" and nlll: "0 < n lll" by auto 
+            then obtain ll where l: "l = Suc ll" by (cases l, auto)   
+            from lll l have lll: "lll = ll - (ll - lll)" by auto
+            let ?l' = "LEAST d. 0 < n (ll - d)"
+            have nl': "0 < n (ll - ?l')"
+            proof (rule LeastI)
+              show "0 < n (ll - (ll - lll))" using lll nlll by auto
+            qed
+            with Suc[THEN spec[of _ "ll - ?l'"]] obtain k where k:
+              "inf_concat n k = (ll - ?l',0)" unfolding l by auto
+            from nl' obtain off where off: "Suc (0 + off) = n (ll - ?l')" by (cases "n (ll - ?l')", auto)
+            from inf_concat_step[OF k, OF off]
+            have id: "inf_concat n (k + Suc off) = (LEAST i'. ll - ?l' < i' \<and> 0 < n i',0)" (is "_ = (?l,0)") .
+            have ll: "?l = l" unfolding l
+            proof (rule Least_equality)
+              show "ll - ?l' < Suc ll \<and> 0 < n (Suc ll)" using nj[unfolded j l] by simp
+            next
+              fix l'
+              assume ass: "ll - ?l' < l' \<and> 0 < n l'"
+              show "Suc ll \<le> l'" 
+              proof (rule ccontr)
+                assume not: "\<not> ?thesis"
+                hence "l' \<le> ll" by auto
+                hence "ll = l' + (ll - l')" by auto
+                then obtain k where ll: "ll = l' + k" by auto
+                from ass have "l' + k - ?l' < l'" unfolding ll by auto
+                hence kl': "k < ?l'" by auto
+                have "0 < n (ll - k)" using ass unfolding ll by simp
+                from Least_le[of "\<lambda> k. 0 < n (ll - k)", OF this] kl'
+                show False by auto
+              qed
+            qed            
+            show ?thesis unfolding j
+              by (rule exI[of _ "k + Suc off"], unfold id ll, simp)
+          qed
+        qed
+      qed
+    qed
+  }
+  with assms show ?thesis by auto
+qed
+
+lemma inf_concat_surj:
+  assumes j: "j < n i"
+  shows "\<exists>k. inf_concat n k = (i, j)"
+proof -
+  from j have "0 < n i" by auto
+  from inf_concat_surj_zero[of n, OF this]
+  obtain k where "inf_concat n k = (i,0)" by auto
+  from inf_concat_add[OF this, of j] j
+  show ?thesis by auto
+qed
+
+lemma inf_concat_mono:
+  assumes inf: "INFM i. n i > 0"
+    and resk: "inf_concat n k = (i, j)"
+    and reskp: "inf_concat n k' = (i', j')"
+    and lt: "i < i'"
+  shows "k < k'"
+proof -
+  note bounds = inf_concat_bounds[OF inf]
+  {
+    assume "k' \<le> k"
+    hence "k = k' + (k - k')" by auto
+    then obtain l where k: "k = k' + l" by auto
+    have "i' \<le> fst (inf_concat n (k' + l))" 
+    proof (induct l)
+      case 0
+      with reskp show ?case by auto
+    next      
+      case (Suc l)
+      obtain i'' j'' where l: "inf_concat n (k' + l) = (i'',j'')" by force
+      with Suc have one: "i' \<le> i''" by auto
+      from bounds[OF l] have j'': "j'' < n i''" by auto
+      show ?case 
+      proof (cases "Suc j'' < n i''")
+        case True
+        show ?thesis by (simp add: l True one)
+      next
+        case False
+        let ?i = "LEAST i'. i'' < i' \<and> 0 < n i'"
+        from inf[unfolded INFM_nat] obtain k where "i'' < k \<and> 0 < n k" by auto
+        from LeastI[of "\<lambda> k. i'' < k \<and> 0 < n k", OF this]
+        have "i'' < ?i" by auto
+        with one show ?thesis by (simp add: l False)
+      qed
+    qed      
+    with resk k lt have False by auto
+  }
+  thus ?thesis by arith
+qed
+
+lemma inf_concat_Suc:
+  assumes inf: "INFM i. n i > 0"
+    and f: "\<And> i. f i (n i) = f (Suc i) 0"
+    and resk: "inf_concat n k = (i, j)"
+    and ressk: "inf_concat n (Suc k) = (i', j')"
+  shows "f i' j' = f i (Suc j)"
+proof - 
+  note bounds = inf_concat_bounds[OF inf]
+  from bounds[OF resk] have j: "j < n i" .
+  show ?thesis
+  proof (cases "Suc j < n i")
+    case True
+    with ressk resk
+    show ?thesis by simp
+  next
+    case False
+    let ?p = "\<lambda> i'. i < i' \<and> 0 < n i'"
+    let ?i' = "LEAST i'. ?p i'"
+    from False j have id: "Suc (j + 0) = n i" by auto
+    from inf_concat_step[OF resk, OF id] ressk
+    have i': "i' = ?i'" and j': "j' = 0" by auto
+    from id have j: "Suc j = n i" by simp
+    from inf[unfolded INFM_nat] obtain k where "?p k" by auto
+    from LeastI[of ?p, OF this] have "?p ?i'" .
+    hence "?i' = Suc i + (?i' - Suc i)" by simp
+    then obtain d where ii': "?i' = Suc i + d" by auto
+    from not_less_Least[of _ ?p, unfolded ii'] have d': "\<And> d'. d' < d \<Longrightarrow> n (Suc i + d') = 0" by auto
+    have "f (Suc i) 0 = f ?i' 0" unfolding ii' using d'
+    proof (induct d)
+      case 0
+      show ?case by simp
+    next
+      case (Suc d)
+      hence "f (Suc i) 0 = f (Suc i + d) 0" by auto
+      also have "... = f (Suc (Suc i + d)) 0"
+        unfolding f[symmetric]
+        using Suc(2)[of d] by simp
+      finally show ?case by simp
+    qed
+    thus ?thesis unfolding i' j' j f by simp
+  qed
+qed
+
+end
\ No newline at end of file
diff -r 79401279ba21 -r 2d6beddb6fa6 Slides/slides1.pdf
Binary file Slides/slides1.pdf has changed
diff -r 79401279ba21 -r 2d6beddb6fa6 Slides/slides2.pdf
Binary file Slides/slides2.pdf has changed
diff -r 79401279ba21 -r 2d6beddb6fa6 WQO_Finite_Lists.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/WQO_Finite_Lists.thy	Wed Aug 29 13:09:36 2012 +0000
@@ -0,0 +1,961 @@
+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
diff -r 79401279ba21 -r 2d6beddb6fa6 csupp.pdf
Binary file csupp.pdf has changed
diff -r 79401279ba21 -r 2d6beddb6fa6 prio/paper.pdf
Binary file prio/paper.pdf has changed