Session Well_Quasi_Orders

Theory Infinite_Sequences

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Infinite Sequences›

text ‹Some useful constructions on and facts about infinite sequences.›

theory Infinite_Sequences
imports Main
begin

text ‹The set of all infinite sequences over elements from @{term A}.›
definition "SEQ A = {f::nat  'a. i. f i  A}"

lemma SEQ_iff [iff]:
  "f  SEQ A  (i. f i  A)"
by (auto simp: SEQ_def)


text ‹The i›-th "column" of a set B› of infinite sequences.›
definition "ith B i = {f i | f. f  B}"

lemma ithI [intro]:
  "f  B  f i = x  x  ith B i"
by (auto simp: ith_def)

lemma ithE [elim]:
  "x  ith B i; f. f  B; f i = x  Q  Q"
by (auto simp: ith_def)

lemma ith_conv:
  "x  ith B i  (f  B. x = f i)"
by auto

text ‹
  The restriction of a set B› of sequences to sequences that are equal to a given sequence
  f› up to position i›.
›
definition eq_upto :: "(nat  'a) set  (nat  'a)  nat  (nat  'a) set"
where
  "eq_upto B f i = {g  B. j < i. f j = g j}"

lemma eq_uptoI [intro]:
  "g  B; j. j < i  f j = g j  g  eq_upto B f i"
by (auto simp: eq_upto_def)

lemma eq_uptoE [elim]:
  "g  eq_upto B f i; g  B; j. j < i  f j = g j  Q  Q"
by (auto simp: eq_upto_def)

lemma eq_upto_Suc:
  "g  eq_upto B f i; g i = f i  g  eq_upto B f (Suc i)"
by (auto simp: eq_upto_def less_Suc_eq)

lemma eq_upto_0 [simp]:
  "eq_upto B f 0 = B"
by (auto simp: eq_upto_def)

lemma eq_upto_cong [fundef_cong]:
  assumes "j. j < i  f j = g j" and "B = C"
  shows "eq_upto B f i = eq_upto C g i"
using assms by (auto simp: eq_upto_def)


subsection ‹Lexicographic Order on Infinite Sequences›

definition "LEX P f g  (i::nat. P (f i) (g i)  (j<i. f j = g j))"
abbreviation "LEXEQ P  (LEX P)=="

lemma LEX_imp_not_LEX:
  assumes "LEX P f g"
    and [dest]: "x y z. P x y  P y z  P x z"
    and [simp]: "x. ¬ P x x"
  shows "¬ LEX P g f"
proof -
  { fix i j :: nat
    assume "P (f i) (g i)" and "k<i. f k = g k"
      and "P (g j) (f j)" and "k<j. g k = f k"
    then have False by (cases "i < j") (auto simp: not_less dest!: le_imp_less_or_eq) }
  then show "¬ LEX P g f" using ‹LEX P f g unfolding LEX_def by blast
qed

lemma LEX_cases:
  assumes "LEX P f g"
  obtains (eq) "f = g" | (neq) k where "i<k. f i = g i" and "P (f k) (g k)"
using assms by (auto simp: LEX_def)

lemma LEX_imp_less:
  assumes "xA. ¬ P x x" and "f  SEQ A  g  SEQ A"
    and "LEX P f g" and "i<k. f i = g i" and "f k  g k"
  shows "P (f k) (g k)"
using assms by (auto elim!: LEX_cases) (metis linorder_neqE_nat)+

end

Theory Minimal_Elements

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Minimal elements of sets w.r.t. a well-founded and transitive relation›

theory Minimal_Elements
imports
  Infinite_Sequences
  Open_Induction.Restricted_Predicates
begin

locale minimal_element =
  fixes P A
  assumes po: "po_on P A"
    and wf: "wfp_on P A"
begin

definition "min_elt B = (SOME x. x  B  (y  A. P y x  y  B))"

lemma minimal:
  assumes "x  A" and "Q x"
  shows "y  A. P== y x  Q y  (z  A. P z y  ¬ Q z)"
using wf and assms
proof (induction rule: wfp_on_induct)
  case (less x)
  then show ?case
  proof (cases "y  A. P y x  ¬ Q y")
    case True
    with less show ?thesis by blast
  next
    case False
    then obtain y where "y  A" and "P y x" and "Q y" by blast
    with less show ?thesis
      using po [THEN po_on_imp_transp_on, unfolded transp_on_def, rule_format, of _ y x] by blast
  qed
qed

lemma min_elt_ex:
  assumes "B  A" and "B  {}"
  shows "x. x  B  (y  A. P y x  y  B)"
using assms using minimal [of _ "λx. x  B"] by auto

lemma min_elt_mem:
  assumes "B  A" and "B  {}"
  shows "min_elt B  B"
using someI_ex [OF min_elt_ex [OF assms]] by (auto simp: min_elt_def)

lemma min_elt_minimal:
  assumes *: "B  A" "B  {}"
  assumes "y  A" and "P y (min_elt B)"
  shows "y  B"
using someI_ex [OF min_elt_ex [OF *]] and assms by (auto simp: min_elt_def)

text ‹A lexicographically minimal sequence w.r.t.\ a given set of sequences C›
fun lexmin
where
  lexmin: "lexmin C i = min_elt (ith (eq_upto C (lexmin C) i) i)"
declare lexmin [simp del]

lemma eq_upto_lexmin_non_empty:
  assumes "C  SEQ A" and "C  {}"
  shows "eq_upto C (lexmin C) i  {}"
proof (induct i)
  case 0
  show ?case using assms by auto
next
  let ?A = "λi. ith (eq_upto C (lexmin C) i) i"
  case (Suc i)
  then have "?A i  {}" by force
  moreover have "eq_upto C (lexmin C) i  eq_upto C (lexmin C) 0" by auto
  ultimately have "?A i  A" and "?A i  {}" using assms by (auto simp: ith_def)
  from min_elt_mem [OF this, folded lexmin]
    obtain f where "f  eq_upto C (lexmin C) (Suc i)" by (auto dest: eq_upto_Suc)
  then show ?case by blast
qed

lemma lexmin_SEQ_mem:
  assumes "C  SEQ A" and "C  {}"
  shows "lexmin C  SEQ A"
proof -
  { fix i
    let ?X = "ith (eq_upto C (lexmin C) i) i"
    have "?X  A" using assms by (auto simp: ith_def)
    moreover have "?X  {}" using eq_upto_lexmin_non_empty [OF assms] by auto
    ultimately have "lexmin C i  A" using min_elt_mem [of ?X] by (subst lexmin) blast }
  then show ?thesis by auto
qed

lemma non_empty_ith:
  assumes "C  SEQ A" and "C  {}"
  shows "ith (eq_upto C (lexmin C) i) i  A"
  and "ith (eq_upto C (lexmin C) i) i  {}"
using eq_upto_lexmin_non_empty [OF assms, of i] and assms by (auto simp: ith_def)

lemma lexmin_minimal:
  "C  SEQ A  C  {}  y  A  P y (lexmin C i)  y  ith (eq_upto C (lexmin C) i) i"
using min_elt_minimal [OF non_empty_ith, folded lexmin] .

lemma lexmin_mem:
  "C  SEQ A  C  {}  lexmin C i  ith (eq_upto C (lexmin C) i) i"
using min_elt_mem [OF non_empty_ith, folded lexmin] .

lemma LEX_chain_on_eq_upto_imp_ith_chain_on:
  assumes "chain_on (LEX P) (eq_upto C f i) (SEQ A)"
  shows "chain_on P (ith (eq_upto C f i) i) A"
using assms
proof -
  { fix x y assume "x  ith (eq_upto C f i) i" and "y  ith (eq_upto C f i) i"
      and "¬ P x y" and "y  x"
    then obtain g h where *: "g  eq_upto C f i" "h  eq_upto C f i"
      and [simp]: "x = g i" "y = h i" and eq: "j<i. g j = f j  h j = f j"
      by (auto simp: ith_def eq_upto_def)
    with assms and y  x consider "LEX P g h" | "LEX P h g" by (force simp: chain_on_def)
    then have "P y x"
    proof (cases)
      assume "LEX P g h"
      with eq and y  x have "P x y" using assms and *
        by (auto simp: LEX_def)
           (metis SEQ_iff chain_on_imp_subset linorder_neqE_nat minimal subsetCE)
      with ¬ P x y show "P y x" ..
    next
      assume "LEX P h g"
      with eq and y  x show "P y x" using assms and *
        by (auto simp: LEX_def)
           (metis SEQ_iff chain_on_imp_subset linorder_neqE_nat minimal subsetCE)
    qed }
  then show ?thesis using assms by (auto simp: chain_on_def) blast
qed

end

end

Theory Least_Enum

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Enumerations of Well-Ordered Sets in Increasing Order›

theory Least_Enum
imports Main
begin
  
locale infinitely_many1 =
  fixes P :: "'a :: wellorder  bool"
  assumes infm: "i. j>i. P j"
begin

text ‹
  Enumerate the elements of a well-ordered infinite set in increasing order.
›
fun enum :: "nat  'a" where
  "enum 0 = (LEAST n. P n)" |
  "enum (Suc i) = (LEAST n. n > enum i  P n)"

lemma enum_mono:
  shows "enum i < enum (Suc i)"
  using infm by (cases i, auto) (metis (lifting) LeastI)+

lemma enum_less:
  "i < j  enum i < enum j"
  using enum_mono by (metis lift_Suc_mono_less)

lemma enum_P:
  shows "P (enum i)"
  using infm by (cases i, auto) (metis (lifting) LeastI)+

end

locale infinitely_many2 =
  fixes P :: "'a :: wellorder  'a  bool"
    and N :: "'a"
  assumes infm: "iN. j>i. P i j"
begin

text ‹
  Enumerate the elements of a well-ordered infinite set that form a chain w.r.t.\ a given predicate
  @{term P} starting from a given index @{term N} in increasing order.
›
fun enumchain :: "nat  'a" where
  "enumchain 0 = N" |
  "enumchain (Suc n) = (LEAST m. m > enumchain n  P (enumchain n) m)"

lemma enumchain_mono:
  shows "N  enumchain i  enumchain i < enumchain (Suc i)"
proof (induct i)
  case 0
  have "enumchain 0  N" by simp
  moreover then have "m>enumchain 0. P (enumchain 0) m" using infm by blast
  ultimately show ?case by auto (metis (lifting) LeastI)
next
  case (Suc i)
  then have "N  enumchain (Suc i)" by auto
  moreover then have "m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by blast
  ultimately show ?case by (auto) (metis (lifting) LeastI)
qed

lemma enumchain_chain:
  shows "P (enumchain i) (enumchain (Suc i))"
proof (cases i)
  case 0
  moreover have "m>enumchain 0. P (enumchain 0) m" using infm by auto
  ultimately show ?thesis by auto (metis (lifting) LeastI)
next
  case (Suc i)
  moreover have "enumchain (Suc i) > N" using enumchain_mono by (metis le_less_trans)
  moreover then have "m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by auto
  ultimately show ?thesis by (auto) (metis (lifting) LeastI)
qed

end

end

Theory Almost_Full

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹The Almost-Full Property›

theory Almost_Full
imports
  "HOL-Library.Sublist"
  "HOL-Library.Ramsey"
  "Regular-Sets.Regexp_Method"
  "Abstract-Rewriting.Seq"
  Least_Enum
  Infinite_Sequences
  Open_Induction.Restricted_Predicates
begin

(*TODO: move*)
lemma le_Suc_eq':
  "x  Suc y  x = 0  (x'. x = Suc x'  x'  y)"
  by (cases x) auto

lemma ex_leq_Suc:
  "(iSuc j. P i)  P 0  (ij. P (Suc i))"
  by (auto simp: le_Suc_eq')

lemma ex_less_Suc:
  "(i<Suc j. P i)  P 0  (i<j. P (Suc i))"
  by (auto simp: less_Suc_eq_0_disj)


subsection ‹Basic Definitions and Facts›

text ‹
  An infinite sequence is \emph{good} whenever there are indices @{term "i < j"} such that
  @{term "P (f i) (f j)"}.
›
definition good :: "('a  'a  bool)  (nat  'a)  bool"
where
  "good P f  (i j. i < j  P (f i) (f j))"

text ‹A sequence that is not good is called \emph{bad}.›
abbreviation "bad P f  ¬ good P f"

lemma goodI:
  "i < j; P (f i) (f j)  good P f"
by (auto simp: good_def)

lemma goodE [elim]:
  "good P f  (i j. i < j; P (f i) (f j)  Q)  Q"
 by (auto simp: good_def)

lemma badE [elim]:
  "bad P f  ((i j. i < j  ¬ P (f i) (f j))  Q)  Q"
by (auto simp: good_def)


definition almost_full_on :: "('a  'a  bool)  'a set  bool"
where
  "almost_full_on P A  (f  SEQ A. good P f)"

lemma almost_full_onI [Pure.intro]:
  "(f. i. f i  A  good P f)  almost_full_on P A"
  unfolding almost_full_on_def by blast

lemma almost_full_onD:
  fixes f :: "nat  'a" and A :: "'a set"
  assumes "almost_full_on P A" and "i. f i  A"
  obtains i j where "i < j" and "P (f i) (f j)"
  using assms unfolding almost_full_on_def by blast


subsection ‹An equivalent inductive definition›

inductive af for A
  where
    now: "(x y. x  A  y  A  P x y)  af A P"
  | later: "(x. x  A  af A (λy z. P y z  P x y))  af A P"

lemma af_imp_almost_full_on:
  assumes "af A P"
  shows "almost_full_on P A"
proof
  fix f :: "nat  'a" assume "i. f i  A"
  with assms obtain i and j where "i < j" and "P (f i) (f j)"
  proof (induct arbitrary: f thesis)
    case (later P)
    define g where [simp]: "g i = f (Suc i)" for i
    have "f 0  A" and "i. g i  A" using later by auto
    then obtain i and j where "i < j" and "P (g i) (g j)  P (f 0) (g i)" using later by blast
    then consider "P (g i) (g j)" | "P (f 0) (g i)" by blast
    then show ?case using i < j by (cases) (auto intro: later)
  qed blast
  then show "good P f" by (auto simp: good_def)
qed

lemma af_mono:
  assumes "af A P"
    and "x y. x  A  y  A  P x y  Q x y"
  shows "af A Q"
  using assms
proof (induct arbitrary: Q)
  case (now P)
  then have "x y. x  A  y  A  Q x y" by blast
  then show ?case by (rule af.now)
next
  case (later P)
  show ?case
  proof (intro af.later [of A Q])
    fix x assume "x  A"
    then show "af A (λy z. Q y z  Q x y)"
      using later(3) by (intro later(2) [of x]) auto
  qed
qed

lemma accessible_on_imp_af:
  assumes "accessible_on P A x"
  shows "af A (λu v. ¬ P v u  ¬ P u x)"
  using assms
proof (induct)
  case (1 x)
  then have "af A (λu v. (¬ P v u  ¬ P u x)  ¬ P u y  ¬ P y x)" if "y  A" for y
    using that by (cases "P y x") (auto intro: af.now af_mono)
  then show ?case by (rule af.later)
qed

lemma wfp_on_imp_af:
  assumes "wfp_on P A"
  shows "af A (λx y. ¬ P y x)"
  using assms by (auto simp: wfp_on_accessible_on_iff intro: accessible_on_imp_af af.later)

lemma af_leq:
  "af UNIV ((≤) :: nat  nat  bool)"
  using wf_less [folded wfP_def wfp_on_UNIV, THEN wfp_on_imp_af] by (simp add: not_less)

definition "NOTAF A P = (SOME x. x  A  ¬ af A (λy z. P y z  P x y))"

lemma not_af:
  "¬ af A P  (x y. x  A  y  A  ¬ P x y)  (xA. ¬ af A (λy z. P y z  P x y))"
  unfolding af.simps [of A P] by blast

fun F
  where
    "F A P 0 = NOTAF A P"
  | "F A P (Suc i) = (let x = NOTAF A P in F A (λy z. P y z  P x y) i)"

lemma almost_full_on_imp_af:
  assumes af: "almost_full_on P A"
  shows "af A P"
proof (rule ccontr)
  assume "¬ af A P"
  then have *: "F A P n  A 
    ¬ af A (λy z. P y z  (in. P (F A P i) y)  (jn. i. i < j  P (F A P i) (F A P j)))" for n
  proof (induct n arbitrary: P)
    case 0
    from ¬ af A P have "x. x  A  ¬ af A (λy z. P y z  P x y)" by (auto intro: af.intros)
    then have "NOTAF A P  A  ¬ af A (λy z. P y z  P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
    with 0 show ?case by simp
  next
    case (Suc n)
    from ¬ af A P have "x. x  A  ¬ af A (λy z. P y z  P x y)" by (auto intro: af.intros)
    then have "NOTAF A P  A  ¬ af A (λy z. P y z  P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
    from Suc(1) [OF this [THEN conjunct2]]
    show ?case
      by (fastforce simp: ex_leq_Suc ex_less_Suc elim!: back_subst [where P = "λx. ¬ af A x"])
  qed
  then have "F A P  SEQ A" by auto
  from af [unfolded almost_full_on_def, THEN bspec, OF this] and not_af [OF * [THEN conjunct2]]
  show False unfolding good_def by blast
qed

hide_const NOTAF F

lemma almost_full_on_UNIV:
  "almost_full_on (λ_ _. True) UNIV"
by (auto simp: almost_full_on_def good_def)

lemma almost_full_on_imp_reflp_on:
  assumes "almost_full_on P A"
  shows "reflp_on P A"
using assms by (auto simp: almost_full_on_def reflp_on_def)

lemma almost_full_on_subset:
  "A  B  almost_full_on P B  almost_full_on P A"
by (auto simp: almost_full_on_def)

lemma almost_full_on_mono:
  assumes "A  B" and "x y. Q x y  P x y"
    and "almost_full_on Q B"
  shows "almost_full_on P A"
  using assms by (metis almost_full_on_def almost_full_on_subset good_def)

text ‹
  Every sequence over elements of an almost-full set has a homogeneous subsequence.
›
lemma almost_full_on_imp_homogeneous_subseq:
  assumes "almost_full_on P A"
    and "i::nat. f i  A"
  shows "φ::nat  nat. i j. i < j  φ i < φ j  P (f (φ i)) (f (φ j))"
proof -
  define X where "X = {{i, j} | i j::nat. i < j  P (f i) (f j)}"
  define Y where "Y = - X"
  define h where "h = (λZ. if Z  X then 0 else Suc 0)"

  have [iff]: "x y. h {x, y} = 0  {x, y}  X" by (auto simp: h_def)
  have [iff]: "x y. h {x, y} = Suc 0  {x, y}  Y" by (auto simp: h_def Y_def)

  have "xUNIV. yUNIV. x  y  h {x, y} < 2" by (simp add: h_def)
  from Ramsey2 [OF infinite_UNIV_nat this] obtain I c
    where "infinite I" and "c < 2"
    and *: "xI. yI. x  y  h {x, y} = c" by blast
  then interpret infinitely_many1 "λi. i  I"
    by (unfold_locales) (simp add: infinite_nat_iff_unbounded)

  have "c = 0  c = 1" using c < 2 by arith
  then show ?thesis
  proof
    assume [simp]: "c = 0"
    have "i j. i < j  P (f (enum i)) (f (enum j))"
    proof (intro allI impI)
      fix i j :: nat
      assume "i < j"
      from * and enum_P and enum_less [OF i < j] have "{enum i, enum j}  X" by auto
      with enum_less [OF i < j]
        show "P (f (enum i)) (f (enum j))" by (auto simp: X_def doubleton_eq_iff)
    qed
    then show ?thesis using enum_less by blast
  next
    assume [simp]: "c = 1"
    have "i j. i < j  ¬ P (f (enum i)) (f (enum j))"
    proof (intro allI impI)
      fix i j :: nat
      assume "i < j"
      from * and enum_P and enum_less [OF i < j] have "{enum i, enum j}  Y" by auto
      with enum_less [OF i < j]
        show "¬ P (f (enum i)) (f (enum j))" by (auto simp: Y_def X_def doubleton_eq_iff)
    qed
    then have "¬ good P (f  enum)" by auto
    moreover have "i. f (enum i)  A" using assms by auto
    ultimately show ?thesis using ‹almost_full_on P A by (simp add: almost_full_on_def)
  qed
qed

text ‹
  Almost full relations do not admit infinite antichains.
›
lemma almost_full_on_imp_no_antichain_on:
  assumes "almost_full_on P A"
  shows "¬ antichain_on P f A"
proof
  assume *: "antichain_on P f A"
  then have "i. f i  A" by simp
  with assms have "good P f" by (auto simp: almost_full_on_def)
  then obtain i j where "i < j" and "P (f i) (f j)"
    unfolding good_def by auto
  moreover with * have "incomparable P (f i) (f j)" by auto
  ultimately show False by blast
qed

text ‹
  If the image of a function is almost-full then also its preimage is almost-full.
›
lemma almost_full_on_map:
  assumes "almost_full_on Q B"
    and "h ` A  B"
  shows "almost_full_on (λx y. Q (h x) (h y)) A" (is "almost_full_on ?P A")
proof
  fix f
  assume "i::nat. f i  A"
  then have "i. h (f i)  B" using h ` A  B by auto
  with ‹almost_full_on Q B [unfolded almost_full_on_def, THEN bspec, of "h  f"]
    show "good ?P f" unfolding good_def comp_def by blast
qed

text ‹
  The homomorphic image of an almost-full set is almost-full.
›
lemma almost_full_on_hom:
  fixes h :: "'a  'b"
  assumes hom: "x y. x  A; y  A; P x y  Q (h x) (h y)"
    and af: "almost_full_on P A"
  shows "almost_full_on Q (h ` A)"
proof
  fix f :: "nat  'b"
  assume "i. f i  h ` A"
  then have "i. x. x  A  f i = h x" by (auto simp: image_def)
  from choice [OF this] obtain g
    where *: "i. g i  A  f i = h (g i)" by blast
  show "good Q f"
  proof (rule ccontr)
    assume bad: "bad Q f"
    { fix i j :: nat
      assume "i < j"
      from bad have "¬ Q (f i) (f j)" using i < j by (auto simp: good_def)
      with hom have "¬ P (g i) (g j)" using * by auto }
    then have "bad P g" by (auto simp: good_def)
    with af and * show False by (auto simp: good_def almost_full_on_def)
  qed
qed

text ‹
  The monomorphic preimage of an almost-full set is almost-full.
›
lemma almost_full_on_mon:
  assumes mon: "x y. x  A; y  A  P x y = Q (h x) (h y)" "bij_betw h A B"
    and af: "almost_full_on Q B"
  shows "almost_full_on P A"
proof
  fix f :: "nat  'a"
  assume *: "i. f i  A"
  then have **: "i. (h  f) i  B" using mon by (auto simp: bij_betw_def)
  show "good P f"
  proof (rule ccontr)
    assume bad: "bad P f"
    { fix i j :: nat
      assume "i < j"
      from bad have "¬ P (f i) (f j)" using i < j by (auto simp: good_def)
      with mon have "¬ Q (h (f i)) (h (f j))"
        using * by (auto simp: bij_betw_def inj_on_def) }
    then have "bad Q (h  f)" by (auto simp: good_def)
    with af and ** show False by (auto simp: good_def almost_full_on_def)
  qed
qed

text ‹
  Every total and well-founded relation is almost-full.
›
lemma total_on_and_wfp_on_imp_almost_full_on:
  assumes "total_on P A" and "wfp_on P A"
  shows "almost_full_on P== A"
proof (rule ccontr)
  assume "¬ almost_full_on P== A"
  then obtain f :: "nat  'a" where *: "i. f i  A"
    and "i j. i < j  ¬ P== (f i) (f j)"
    unfolding almost_full_on_def by (auto dest: badE)
  with ‹total_on P A have "i j. i < j  P (f j) (f i)"
    unfolding total_on_def by blast
  then have "i. P (f (Suc i)) (f i)" by auto
  with ‹wfp_on P A and * show False
    unfolding wfp_on_def by blast
qed

lemma Nil_imp_good_list_emb [simp]:
  assumes "f i = []"
  shows "good (list_emb P) f"
proof (rule ccontr)
  assume "bad (list_emb P) f"
  moreover have "(list_emb P) (f i) (f (Suc i))"
    unfolding assms by auto
  ultimately show False
    unfolding good_def by auto
qed

lemma ne_lists:
  assumes "xs  []" and "xs  lists A"
  shows "hd xs  A" and "tl xs  lists A"
  using assms by (case_tac [!] xs) simp_all

lemma list_emb_eq_length_induct [consumes 2, case_names Nil Cons]:
  assumes "length xs = length ys"
    and "list_emb P xs ys"
    and "Q [] []"
    and "x y xs ys. P x y; list_emb P xs ys; Q xs ys  Q (x#xs) (y#ys)"
  shows "Q xs ys"
  using assms(2, 1, 3-) by (induct) (auto dest: list_emb_length)

lemma list_emb_eq_length_P:
  assumes "length xs = length ys"
    and "list_emb P xs ys"
  shows "i<length xs. P (xs ! i) (ys ! i)"
using assms
proof (induct rule: list_emb_eq_length_induct)
  case (Cons x y xs ys)
  show ?case
  proof (intro allI impI)
    fix i assume "i < length (x # xs)"
    with Cons show "P ((x#xs)!i) ((y#ys)!i)"
      by (cases i) simp_all
  qed
qed simp


subsection ‹Special Case: Finite Sets›

text ‹
  Every reflexive relation on a finite set is almost-full.
›
lemma finite_almost_full_on:
  assumes finite: "finite A"
    and refl: "reflp_on P A"
  shows "almost_full_on P A"
proof
  fix f :: "nat  'a"
  assume *: "i. f i  A"
  let ?I = "UNIV::nat set"
  have "f ` ?I  A" using * by auto
  with finite 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
  then have "P (f k) (f l)" using refl and * by (auto simp: reflp_on_def)
  with k < l show "good P f" by (auto simp: good_def)
qed

lemma eq_almost_full_on_finite_set:
  assumes "finite A"
  shows "almost_full_on (=) A"
  using finite_almost_full_on [OF assms, of "(=)"]
  by (auto simp: reflp_on_def)


subsection ‹Further Results›

lemma af_trans_extension_imp_wf:
  assumes subrel: "x y. P x y  Q x y"
    and af: "almost_full_on P A"
    and trans: "transp_on Q A"
  shows "wfp_on (strict Q) A"
proof (unfold wfp_on_def, rule notI)
  assume "f. i. f i  A  strict Q (f (Suc i)) (f i)"
  then obtain f where *: "i. f i  A  ((strict Q)¯¯) (f i) (f (Suc i))" by blast
  from chain_transp_on_less [OF this]
    and transp_on_strict [THEN transp_on_converse, OF trans]
  have "i j. i < j  ¬ Q (f i) (f j)" by blast
  with subrel have "i j. i < j  ¬ P (f i) (f j)" by blast
  with af show False
    using * by (auto simp: almost_full_on_def good_def)
qed

lemma af_trans_imp_wf:
  assumes "almost_full_on P A"
    and "transp_on P A"
  shows "wfp_on (strict P) A"
  using assms by (intro af_trans_extension_imp_wf)

lemma wf_and_no_antichain_imp_qo_extension_wf:
  assumes wf: "wfp_on (strict P) A"
    and anti: "¬ (f. antichain_on P f A)"
    and subrel: "xA. yA. P x y  Q x y"
    and qo: "qo_on Q A"
  shows "wfp_on (strict Q) A"
proof (rule ccontr)
  have "transp_on (strict Q) A"
    using qo unfolding qo_on_def transp_on_def by blast
  then have *: "transp_on ((strict Q)¯¯) A" by (rule transp_on_converse)
  assume "¬ wfp_on (strict Q) A"
  then obtain f :: "nat  'a" where A: "i. f i  A"
    and "i. strict Q (f (Suc i)) (f i)" unfolding wfp_on_def by blast+
  then have "i. f i  A  ((strict Q)¯¯) (f i) (f (Suc i))" by auto
  from chain_transp_on_less [OF this *]
    have *: "i j. i < j  ¬ P (f i) (f j)"
    using subrel and A by blast
  show False
  proof (cases)
    assume "k. i>k. j>i. P (f j) (f i)"
    then obtain k where "i>k. j>i. P (f j) (f i)" by auto
    from subchain [of k _ f, OF this] obtain g
      where "i j. i < j  g i < g j"
      and "i. P (f (g (Suc i))) (f (g i))" by auto
    with * have "i. strict P (f (g (Suc i))) (f (g i))" by blast
    with wf [unfolded wfp_on_def not_ex, THEN spec, of "λi. f (g i)"] and A
      show False by fast
  next
    assume "¬ (k. i>k. j>i. P (f j) (f i))"
    then have "k. i>k. j>i. ¬ P (f j) (f i)" by auto
    from choice [OF this] obtain h
      where "k. h k > k"
      and **: "k. (j>h k. ¬ P (f j) (f (h k)))" by auto
    define φ where [simp]: "φ = (λi. (h ^^ Suc i) 0)"
    have "i. φ i < φ (Suc i)"
      using k. h k > k by (induct_tac i) auto
    then have mono: "i j. i < j  φ i < φ j" by (metis lift_Suc_mono_less)
    then have "i j. i < j  ¬ P (f (φ j)) (f (φ i))"
      using ** by auto
    with mono [THEN *]
      have "i j. i < j  incomparable P (f (φ j)) (f (φ i))" by blast
    moreover have "i j. i < j  ¬ incomparable P (f (φ i)) (f (φ j))"
      using anti [unfolded not_ex, THEN spec, of "λi. f (φ i)"] and A by blast
    ultimately show False by blast
  qed
qed

lemma every_qo_extension_wf_imp_af:
  assumes ext: "Q. (xA. yA. P x y  Q x y) 
    qo_on Q A  wfp_on (strict Q) A"
    and "qo_on P A"
  shows "almost_full_on P A"
proof
  from ‹qo_on P A
    have refl: "reflp_on P A"
    and trans: "transp_on P A"
    by (auto intro: qo_on_imp_reflp_on qo_on_imp_transp_on)

  fix f :: "nat  'a"
  assume "i. f i  A"
  then have A: "i. f i  A" ..
  show "good P f"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then have bad: "i j. i < j  ¬ P (f i) (f j)" by (auto simp: good_def)
    then have *: "i j. P (f i) (f j)  i  j" by (metis not_le_imp_less)

    define D where [simp]: "D = (λx y. i. x = f (Suc i)  y = f i)"
    define P' where "P' = restrict_to P A"
    define Q where [simp]: "Q = (sup P' D)**"

    have **: "i j. (D OO P'**)++ (f i) (f j)  i > j"
    proof -
      fix i j
      assume "(D OO P'**)++ (f i) (f j)"
      then show "i > j"
        apply (induct "f i" "f j" arbitrary: j)
        apply (insert A, auto dest!: * simp: P'_def reflp_on_restrict_to_rtranclp [OF refl trans])
        apply (metis "*" dual_order.strict_trans1 less_Suc_eq_le refl reflp_on_def)
        by (metis le_imp_less_Suc less_trans)
    qed

    have "xA. yA. P x y  Q x y" by (auto simp: P'_def)
    moreover have "qo_on Q A" by (auto simp: qo_on_def reflp_on_def transp_on_def)
    ultimately have "wfp_on (strict Q) A"
        using ext [THEN spec, of Q] by blast
    moreover have "i. f i  A  strict Q (f (Suc i)) (f i)"
    proof
      fix i
      have "¬ Q (f i) (f (Suc i))"
      proof
        assume "Q (f i) (f (Suc i))"
        then have "(sup P' D)** (f i) (f (Suc i))" by auto
        moreover have "(sup P' D)** = sup (P'**) (P'** OO (D OO P'**)++)"
        proof -
          have "A B. (A  B)* = A*  A* O (B O A*)+" by regexp
          from this [to_pred] show ?thesis by blast
        qed
        ultimately have "sup (P'**) (P'** OO (D OO P'**)++) (f i) (f (Suc i))" by simp
        then have "(P'** OO (D OO P'**)++) (f i) (f (Suc i))" by auto
        then have "Suc i < i"
          using ** apply auto
          by (metis (lifting, mono_tags) less_le relcompp.relcompI tranclp_into_tranclp2)
        then show False by auto
      qed
      with A [of i] show "f i  A  strict Q (f (Suc i)) (f i)" by auto
    qed
    ultimately show False unfolding wfp_on_def by blast
  qed
qed

end

Theory Minimal_Bad_Sequences

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Constructing Minimal Bad Sequences›

theory Minimal_Bad_Sequences
imports
  Almost_Full
  Minimal_Elements
begin

text ‹
  A locale capturing the construction of minimal bad sequences over values from @{term "A"}. Where
  minimality is to be understood w.r.t.\ @{term size} of an element.
›
locale mbs =
  fixes A :: "('a :: size) set"
begin

text ‹
  Since the @{term size} is a well-founded measure, whenever some element satisfies a property
  @{term P}, then there is a size-minimal such element.
›
lemma minimal:
  assumes "x  A" and "P x"
  shows "y  A. size y  size x  P y  (z  A. size z < size y  ¬ P z)"
using assms
proof (induction x taking: size rule: measure_induct)
  case (1 x)
  then show ?case
  proof (cases "y  A. size y < size x  ¬ P y")
    case True
    with 1 show ?thesis by blast
  next
    case False
    then obtain y where "y  A" and "size y < size x" and "P y" by blast
    with "1.IH" show ?thesis by (fastforce elim!: order_trans)
  qed
qed

lemma less_not_eq [simp]:
  "x  A  size x < size y  x = y  False"
  by simp

text ‹
  The set of all bad sequences over @{term A}.
›
definition "BAD P = {f  SEQ A. bad P f}"

lemma BAD_iff [iff]:
  "f  BAD P  (i. f i  A)  bad P f"
  by (auto simp: BAD_def)

text ‹
  A partial order on infinite bad sequences.
›
definition geseq :: "((nat  'a) × (nat  'a)) set"
where
  "geseq =
    {(f, g). f  SEQ A  g  SEQ A  (f = g  (i. size (g i) < size (f i)  (j < i. f j = g j)))}"

text ‹
  The strict part of the above order.
›
definition gseq :: "((nat  'a) × (nat  'a)) set" where
  "gseq = {(f, g). f  SEQ A  g  SEQ A  (i. size (g i) < size (f i)  (j < i. f j = g j))}"

lemma geseq_iff:
  "(f, g)  geseq 
    f  SEQ A  g  SEQ A  (f = g  (i. size (g i) < size (f i)  (j < i. f j = g j)))"
  by (auto simp: geseq_def)

lemma gseq_iff:
  "(f, g)  gseq  f  SEQ A  g  SEQ A  (i. size (g i) < size (f i)  (j < i. f j = g j))"
  by (auto simp: gseq_def)

lemma geseqE:
  assumes "(f, g)  geseq"
    and "i. f i  A; i. g i  A; f = g  Q"
    and "i. i. f i  A; i. g i  A; size (g i) < size (f i); j < i. f j = g j  Q"
  shows "Q"
  using assms by (auto simp: geseq_iff)

lemma gseqE:
  assumes "(f, g)  gseq"
    and "i. i. f i  A; i. g i  A; size (g i) < size (f i); j < i. f j = g j  Q"
  shows "Q"
  using assms by (auto simp: gseq_iff)

sublocale min_elt_size?: minimal_element "measure_on size UNIV" A
rewrites "measure_on size UNIV  λx y. size x < size y"
apply (unfold_locales)
apply (auto simp: po_on_def irreflp_on_def transp_on_def simp del: wfp_on_UNIV intro: wfp_on_subset)
apply (auto simp: measure_on_def inv_image_betw_def)
done

context
  fixes P :: "'a  'a  bool"
begin

text ‹
  A lower bound to all sequences in a set of sequences @{term B}.
›
abbreviation "lb  lexmin (BAD P)"

lemma eq_upto_BAD_mem:
  assumes "f  eq_upto (BAD P) g i"
  shows "f j  A"
  using assms by (auto)

text ‹
  Assume that there is some infinite bad sequence @{term h}.
›
context
  fixes h :: "nat  'a"
  assumes BAD_ex: "h  BAD P"
begin

text ‹
  When there is a bad sequence, then filtering @{term "BAD P"} w.r.t.~positions in @{term lb} never
  yields an empty set of sequences.
›
lemma eq_upto_BAD_non_empty:
  "eq_upto (BAD P) lb i  {}"
using eq_upto_lexmin_non_empty [of "BAD P"] and BAD_ex by auto

lemma non_empty_ith:
  shows "ith (eq_upto (BAD P) lb i) i  A"
  and "ith (eq_upto (BAD P) lb i) i  {}"
  using eq_upto_BAD_non_empty [of i] by auto

lemmas
  lb_minimal = min_elt_minimal [OF non_empty_ith, folded lexmin] and
  lb_mem = min_elt_mem [OF non_empty_ith, folded lexmin]

text @{term "lb"} is a infinite bad sequence.
›
lemma lb_BAD:
  "lb  BAD P"
proof -
  have *: "j. lb j  ith (eq_upto (BAD P) lb j) j" by (rule lb_mem)
  then have "i. lb i  A" by (auto simp: ith_conv) (metis eq_upto_BAD_mem)
  moreover
  { assume "good P lb"
    then obtain i j where "i < j" and "P (lb i) (lb j)" by (auto simp: good_def)
    from * have "lb j  ith (eq_upto (BAD P) lb j) j" by (auto)
    then obtain g where "g  eq_upto (BAD P) lb j" and "g j = lb j" by force
    then have "k  j. g k = lb k" by (auto simp: order_le_less)
    with i < j and P (lb i) (lb j) have "P (g i) (g j)" by auto
    with i < j have "good P g" by (auto simp: good_def)
    with g  eq_upto (BAD P) lb j have False by auto }
  ultimately show ?thesis by blast
qed

text ‹
  There is no infinite bad sequence that is strictly smaller than @{term lb}.
›
lemma lb_lower_bound:
  "g. (lb, g)  gseq  g  BAD P"
proof (intro allI impI)
  fix g
  assume "(lb, g)  gseq"
  then obtain i where "g i  A" and "size (g i) < size (lb i)"
    and "j < i. lb j = g j" by (auto simp: gseq_iff)
  moreover with lb_minimal
    have "g i  ith (eq_upto (BAD P) lb i) i" by auto
  ultimately show "g  BAD P" by blast
qed

text ‹
  If there is at least one bad sequence, then there is also a minimal one.
›
lemma lower_bound_ex:
  "f  BAD P. g. (f, g)  gseq  g  BAD P"
  using lb_BAD and lb_lower_bound by blast

lemma gseq_conv:
  "(f, g)  gseq  f  g  (f, g)  geseq"
  by (auto simp: gseq_def geseq_def dest: less_not_eq)

text ‹There is a minimal bad sequence.›
lemma mbs:
  "f  BAD P. g. (f, g)  gseq  good P g"
  using lower_bound_ex by (auto simp: gseq_conv geseq_iff)

end

end

end

end

Theory Higman_OI

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹A Proof of Higman's Lemma via Open Induction›

theory Higman_OI
imports
  Open_Induction.Open_Induction
  Minimal_Elements
  Almost_Full
begin

subsection ‹Some facts about the suffix relation›

lemma wfp_on_strict_suffix:
  "wfp_on strict_suffix A"
by (rule wfp_on_mono [OF subset_refl, of _ _ "measure_on length A"])
   (auto simp: strict_suffix_def suffix_def)

lemma po_on_strict_suffix:
  "po_on strict_suffix A"
by (force simp: strict_suffix_def po_on_def transp_on_def irreflp_on_def)


subsection ‹Lexicographic Order on Infinite Sequences›

lemma antisymp_on_LEX:
  assumes "irreflp_on P A" and "antisymp_on P A"
  shows "antisymp_on (LEX P) (SEQ A)"
proof
  fix f g assume SEQ: "f  SEQ A" "g  SEQ A" and "LEX P f g" and "LEX P g f"
  then obtain i j where "P (f i) (g i)" and "P (g j) (f j)"
    and "k<i. f k = g k" and "k<j. g k = f k" by (auto simp: LEX_def)
  then have "P (f (min i j)) (f (min i j))"
    using assms(2) and SEQ by (cases "i = j") (auto simp: antisymp_on_def min_def, force)
  with assms(1) and SEQ show  "f = g" by (auto simp: irreflp_on_def)
qed

lemma LEX_trans:
  assumes "transp_on P A" and "f  SEQ A" and "g  SEQ A" and "h  SEQ A"
    and "LEX P f g" and "LEX P g h"
  shows "LEX P f h"
using assms by (auto simp: LEX_def transp_on_def) (metis less_trans linorder_neqE_nat)

lemma qo_on_LEXEQ:
  "transp_on P A  qo_on (LEXEQ P) (SEQ A)"
by (auto simp: qo_on_def reflp_on_def transp_on_def [of "LEXEQ P"] dest: LEX_trans)

context minimal_element
begin

lemma glb_LEX_lexmin:
  assumes "chain_on (LEX P) C (SEQ A)" and "C  {}"
  shows "glb (LEX P) C (lexmin C)"
proof
  have "C  SEQ A" using assms by (auto simp: chain_on_def)
  then have "lexmin C  SEQ A" using C  {} by (intro lexmin_SEQ_mem)
  note * = C  SEQ A C  {}
  note lex = LEX_imp_less [folded irreflp_on_def, OF po [THEN po_on_imp_irreflp_on]]
  ― ‹lexmin C› is a lower bound›
  show "lb (LEX P) C (lexmin C)"
  proof
    fix f assume "f  C"
    then show "LEXEQ P (lexmin C) f"
    proof (cases "f = lexmin C")
      define i where "i = (LEAST i. f i  lexmin C i)"
      case False
      then have neq: "i. f i  lexmin C i" by blast
      from LeastI_ex [OF this, folded i_def]
        and not_less_Least [where P = "λi. f i  lexmin C i", folded i_def]
      have neq: "f i  lexmin C i" and eq: "j<i. f j = lexmin C j" by auto
      then have **: "f  eq_upto C (lexmin C) i" "f i  ith (eq_upto C (lexmin C) i) i"
        using f  C by force+
      moreover from ** have "¬ P (f i) (lexmin C i)"
        using lexmin_minimal [OF *, of "f i" i] and f  C and C  SEQ A by blast
      moreover obtain g where "g  eq_upto C (lexmin C) (Suc i)"
        using eq_upto_lexmin_non_empty [OF *] by blast
      ultimately have "P (lexmin C i) (f i)"
        using neq and C  SEQ A and assms(1) and lex [of g f i] and lex [of f g i]
        by (auto simp: eq_upto_def chain_on_def)
      with eq show ?thesis by (auto simp: LEX_def)
    qed simp
  qed

  ― ‹lexmin C› is greater than or equal to any other lower bound›
  fix f assume lb: "lb (LEX P) C f"
  then show "LEXEQ P f (lexmin C)"
  proof (cases "f = lexmin C")
    define i where "i = (LEAST i. f i  lexmin C i)"
    case False
    then have neq: "i. f i  lexmin C i" by blast
    from LeastI_ex [OF this, folded i_def]
      and not_less_Least [where P = "λi. f i  lexmin C i", folded i_def]
    have neq: "f i  lexmin C i" and eq: "j<i. f j = lexmin C j" by auto
    obtain h where "h  eq_upto C (lexmin C) (Suc i)" and "h  C"
      using eq_upto_lexmin_non_empty [OF *] by (auto simp: eq_upto_def)
    then have [simp]: "j. j < Suc i  h j = lexmin C j" by auto
    with lb and h  C have "LEX P f h" using neq by (auto simp: lb_def)
    then have "P (f i) (h i)"
      using neq and eq and C  SEQ A and h  C by (intro lex) auto
    with eq show ?thesis by (auto simp: LEX_def)
  qed simp
qed

lemma dc_on_LEXEQ:
  "dc_on (LEXEQ P) (SEQ A)"
proof
  fix C assume "chain_on (LEXEQ P) C (SEQ A)" and "C  {}"
  then have chain: "chain_on (LEX P) C (SEQ A)" by (auto simp: chain_on_def)
  then have "C  SEQ A" by (auto simp: chain_on_def)
  then have "lexmin C  SEQ A" using C  {} by (intro lexmin_SEQ_mem)
  have "glb (LEX P) C (lexmin C)" by (rule glb_LEX_lexmin [OF chain C  {}])
  then have "glb (LEXEQ P) C (lexmin C)" by (auto simp: glb_def lb_def)
  with ‹lexmin C  SEQ A show "f  SEQ A. glb (LEXEQ P) C f" by blast
qed

end

text ‹
  Properties that only depend on finite initial segments of a sequence
  (i.e., which are open with respect to the product topology).
›
definition "pt_open_on Q A  (fA. Q f  (n. (gA. (i<n. g i = f i)  Q g)))"

lemma pt_open_onD:
  "pt_open_on Q A  Q f  f  A  (n. (gA. (i<n. g i = f i)  Q g))"
  unfolding pt_open_on_def by blast

lemma pt_open_on_good:
  "pt_open_on (good Q) (SEQ A)"
proof (unfold pt_open_on_def, intro ballI)
  fix f assume f: "f  SEQ A"
  show "good Q f = (n. gSEQ A. (i<n. g i = f i)  good Q g)"
  proof
    assume "good Q f"
    then obtain i and j where *: "i < j" "Q (f i) (f j)" by auto
    have "gSEQ A. (i<Suc j. g i = f i)  good Q g"
    proof (intro ballI impI)
      fix g assume "g  SEQ A" and "i<Suc j. g i = f i"
      then show "good Q g" using * by (force simp: good_def)
    qed
    then show "n. gSEQ A. (i<n. g i = f i)  good Q g" ..
  next
    assume "n. gSEQ A. (i<n. g i = f i)  good Q g"
    with f show "good Q f" by blast
  qed
qed

context minimal_element
begin

lemma pt_open_on_imp_open_on_LEXEQ:
  assumes "pt_open_on Q (SEQ A)"
  shows "open_on (LEXEQ P) Q (SEQ A)"
proof
  fix C assume chain: "chain_on (LEXEQ P) C (SEQ A)" and ne: "C  {}"
    and "gSEQ A. glb (LEXEQ P) C g  Q g"
  then obtain g where g: "g  SEQ A" and "glb (LEXEQ P) C g"
    and Q: "Q g" by blast
  then have glb: "glb (LEX P) C g" by (auto simp: glb_def lb_def)
  from chain have "chain_on (LEX P) C (SEQ A)" and C: "C  SEQ A" by (auto simp: chain_on_def)
  note * = glb_LEX_lexmin [OF this(1) ne]
  have "lexmin C  SEQ A" using ne and C by (intro lexmin_SEQ_mem)
  from glb_unique [OF _ g this glb *]
    and antisymp_on_LEX [OF po_on_imp_irreflp_on [OF po] po_on_imp_antisymp_on [OF po]]
  have [simp]: "lexmin C = g" by auto
  from assms [THEN pt_open_onD, OF Q g]
  obtain n :: nat where **: "h. h  SEQ A  (i<n. h i = g i)  Q h" by blast
  from eq_upto_lexmin_non_empty [OF C ne, of n]
  obtain f where "f  eq_upto C g n" by auto
  then have "f  C" and "Q f" using ** [of f] and C by force+
  then show "fC. Q f" by blast
qed

lemma open_on_good:
  "open_on (LEXEQ P) (good Q) (SEQ A)"
  by (intro pt_open_on_imp_open_on_LEXEQ pt_open_on_good)

end

lemma open_on_LEXEQ_imp_pt_open_on_counterexample:
  fixes a b :: "'a"
  defines "A  {a, b}" and "P  (λx y. False)" and "Q  (λf. i. f i = b)"
  assumes [simp]: "a  b"
  shows "minimal_element P A" and "open_on (LEXEQ P) Q (SEQ A)"
    and "¬ pt_open_on Q (SEQ A)"
proof -
  show "minimal_element P A"
    by standard (auto simp: P_def po_on_def irreflp_on_def transp_on_def wfp_on_def)
  show "open_on (LEXEQ P) Q (SEQ A)"
    by (auto simp: P_def open_on_def chain_on_def SEQ_def glb_def lb_def LEX_def)
  show "¬ pt_open_on Q (SEQ A)"
  proof
    define f :: "nat  'a" where "f  (λx. b)"
    have "f  SEQ A" by (auto simp: A_def f_def)
    moreover assume "pt_open_on Q (SEQ A)"
    ultimately have "Q f  (n. (gSEQ A. (i<n. g i = f i)  Q g))"
      unfolding pt_open_on_def by blast
    moreover have "Q f" by (auto simp: Q_def f_def)
    moreover have "gSEQ A. (i<n. g i = f i)  ¬ Q g" for n
      by (intro bexI [of _ "f(n := a)"]) (auto simp: f_def Q_def A_def)
    ultimately show False by blast
  qed
qed

lemma higman:
  assumes "almost_full_on P A"
  shows "almost_full_on (list_emb P) (lists A)"
proof
  interpret minimal_element strict_suffix "lists A"
    by (unfold_locales) (intro po_on_strict_suffix wfp_on_strict_suffix)+
  fix f presume "f  SEQ (lists A)"
  with qo_on_LEXEQ [OF po_on_imp_transp_on [OF po_on_strict_suffix]] and dc_on_LEXEQ and open_on_good
    show "good (list_emb P) f"
  proof (induct rule: open_induct_on)
    case (less f)
    define h where "h i = hd (f i)" for i
    show ?case
    proof (cases "i. f i = []")
      case False
      then have ne: "i. f i  []" by auto
      with f  SEQ (lists A) have "i. h i  A" by (auto simp: h_def ne_lists)
      from almost_full_on_imp_homogeneous_subseq [OF assms this]
      obtain φ :: "nat  nat" where mono: "i j. i < j  φ i < φ j"
        and P: "i j. i < j  P (h (φ i)) (h (φ j))" by blast
      define f' where "f' i = (if i < φ 0 then f i else tl (f (φ (i - φ 0))))" for i
      have f': "f'  SEQ (lists A)" using ne and f  SEQ (lists A)
        by (auto simp: f'_def dest: list.set_sel)
      have [simp]: "i. φ 0  i  h (φ (i - φ 0)) # f' i = f (φ (i - φ 0))"
        "i. i < φ 0  f' i = f i" using ne by (auto simp: f'_def h_def)
      moreover have "strict_suffix (f' (φ 0)) (f (φ 0))" using ne by (auto simp: f'_def)
      ultimately have "LEX strict_suffix f' f" by (auto simp: LEX_def)
      with LEX_imp_not_LEX [OF this] have "strict (LEXEQ strict_suffix) f' f"
        using po_on_strict_suffix [of UNIV] unfolding po_on_def irreflp_on_def transp_on_def by blast
      from less(2) [OF f' this] have "good (list_emb P) f'" .
      then obtain i j where "i < j" and emb: "list_emb P (f' i) (f' j)" by (auto simp: good_def)
      consider "j < φ 0" | "φ 0  i" | "i < φ 0" and "φ 0  j" by arith
      then show ?thesis
      proof (cases)
        case 1 with i < j and emb show ?thesis by (auto simp: good_def)
      next
        case 2
        with i < j and P have "P (h (φ (i - φ 0))) (h (φ (j - φ 0)))" by auto
        with emb have "list_emb P (h (φ (i - φ 0)) # f' i) (h (φ (j - φ 0)) # f' j)" by auto
        then have "list_emb P (f (φ (i - φ 0))) (f (φ (j - φ 0)))" using 2 and i < j by auto
        moreover with 2 and i <j have "φ (i - φ 0) < φ (j - φ 0)" using mono by auto
        ultimately show ?thesis by (auto simp: good_def)
      next
        case 3
        with emb have "list_emb P (f i) (f' j)" by auto
        moreover have "f (φ (j - φ 0)) = h (φ (j - φ 0)) # f' j" using 3 by auto
        ultimately have "list_emb P (f i) (f (φ (j - φ 0)))" by auto
        moreover have "i < φ (j - φ 0)" using mono [of 0 "j - φ 0"] and 3 by force
        ultimately show ?thesis by (auto simp: good_def)
      qed
    qed auto
  qed
qed blast

end

Theory Almost_Full_Relations

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Almost-Full Relations›

theory Almost_Full_Relations
imports Minimal_Bad_Sequences
begin

lemma (in mbs) mbs':
  assumes "¬ almost_full_on P A"
  shows "m  BAD P. g. (m, g)  gseq  good P g"
using assms and mbs unfolding almost_full_on_def by blast

(*TODO: move to Option.thy of Isabelle/HOL?*)
subsection ‹Adding a Bottom Element to a Set›

definition with_bot :: "'a set  'a option set" ("_" [1000] 1000)
where
  "A = {None}  Some ` A"

lemma with_bot_iff [iff]:
  "Some x  A  x  A"
  by (auto simp: with_bot_def)

lemma NoneI [simp, intro]:
  "None  A"
  by (simp add: with_bot_def)

lemma not_None_the_mem [simp]:
  "x  None  the x  A  x  A"
  by auto

lemma with_bot_cases:
  "u  A  (x. x  A  u = Some x  P)  (u = None  P)  P"
  by auto

lemma with_bot_empty_conv [iff]:
  "A = {None}  A = {}"
  by (auto elim: with_bot_cases)

lemma with_bot_UNIV [simp]:
  "UNIV = UNIV"
proof (rule set_eqI)
  fix x :: "'a option"
  show "x  UNIV  x  UNIV" by (cases x) auto
qed


subsection ‹Adding a Bottom Element to an Almost-Full Set›

fun
  option_le :: "('a  'a  bool)  'a option  'a option  bool"
where
  "option_le P None y = True" |
  "option_le P (Some x) None = False" |
  "option_le P (Some x) (Some y) = P x y"

lemma None_imp_good_option_le [simp]:
  assumes "f i = None"
  shows "good (option_le P) f"
  by (rule goodI [of i "Suc i"]) (auto simp: assms)

lemma almost_full_on_with_bot:
  assumes "almost_full_on P A"
  shows "almost_full_on (option_le P) A" (is "almost_full_on ?P ?A")
proof
  fix f :: "nat  'a option"
  assume *: "i. f i  ?A"
  show "good ?P f"
  proof (cases "i. f i  None")
    case True
    then have **: "i. Some (the (f i)) = f i"
      and "i. the (f i)  A" using * by auto
    with almost_full_onD [OF assms, of "the  f"] obtain i j where "i < j"
      and "P (the (f i)) (the (f j))" by auto
    then have "?P (Some (the (f i))) (Some (the (f j)))" by simp
    then have "?P (f i) (f j)" unfolding ** .
    with i < j show "good ?P f" by (auto simp: good_def)
  qed auto
qed


subsection ‹Disjoint Union of Almost-Full Sets›

fun
  sum_le :: "('a  'a  bool)  ('b  'b  bool)  'a + 'b  'a + 'b  bool"
where
  "sum_le P Q (Inl x) (Inl y) = P x y" |
  "sum_le P Q (Inr x) (Inr y) = Q x y" |
  "sum_le P Q x y = False"

lemma not_sum_le_cases:
  assumes "¬ sum_le P Q a b"
    and "x y. a = Inl x; b = Inl y; ¬ P x y  thesis"
    and "x y. a = Inr x; b = Inr y; ¬ Q x y  thesis"
    and "x y. a = Inl x; b = Inr y  thesis"
    and "x y. a = Inr x; b = Inl y  thesis"
  shows thesis
  using assms by (cases a b rule: sum.exhaust [case_product sum.exhaust]) auto

text ‹
  When two sets are almost-full, then their disjoint sum is almost-full.
›
lemma almost_full_on_Plus:
  assumes "almost_full_on P A" and "almost_full_on Q B"
  shows "almost_full_on (sum_le P Q) (A <+> B)" (is "almost_full_on ?P ?A")
proof
  fix f :: "nat  ('a + 'b)"
  let ?I = "f -` Inl ` A"
  let ?J = "f -` Inr ` B"
  assume "i. f i  ?A"
  then have *: "?J = (UNIV::nat set) - ?I" by (fastforce)
  show "good ?P f"
  proof (rule ccontr)
    assume bad: "bad ?P f"
    show False
    proof (cases "finite ?I")
      assume "finite ?I"
      then have "infinite ?J" by (auto simp: *)
      then interpret infinitely_many1 "λi. f i  Inr ` B"
        by (unfold_locales) (simp add: infinite_nat_iff_unbounded)
      have [dest]: "i x. f (enum i) = Inl x  False"
        using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
      let ?f = "λi. projr (f (enum i))"
      have B: "i. ?f i  B" using enum_P by (auto simp: image_iff) (metis sum.sel(2))
      { fix i j :: nat
        assume "i < j"
        then have "enum i < enum j" using enum_less by auto
        with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
        then have "¬ Q (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
      then have "bad Q ?f" by (auto simp: good_def)
      moreover from ‹almost_full_on Q B and B
        have "good Q ?f" by (auto simp: good_def almost_full_on_def)
      ultimately show False by blast
    next
      assume "infinite ?I"
      then interpret infinitely_many1 "λi. f i  Inl ` A"
        by (unfold_locales) (simp add: infinite_nat_iff_unbounded)
      have [dest]: "i x. f (enum i) = Inr x  False"
        using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
      let ?f = "λi. projl (f (enum i))"
      have A: "i. ?f i  A" using enum_P by (auto simp: image_iff) (metis sum.sel(1))
      { fix i j :: nat
        assume "i < j"
        then have "enum i < enum j" using enum_less by auto
        with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
        then have "¬ P (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
      then have "bad P ?f" by (auto simp: good_def)
      moreover from ‹almost_full_on P A and A
        have "good P ?f" by (auto simp: good_def almost_full_on_def)
      ultimately show False by blast
    qed
  qed
qed


subsection ‹Dickson's Lemma for Almost-Full Relations›

text ‹
  When two sets are almost-full, then their Cartesian product is almost-full.
›

definition
  prod_le :: "('a  'a  bool)  ('b  'b  bool)  'a × 'b  'a × 'b  bool"
where
  "prod_le P1 P2 = (λ(p1, p2) (q1, q2). P1 p1 q1  P2 p2 q2)"

lemma prod_le_True [simp]:
  "prod_le P (λ_ _. True) a b = P (fst a) (fst b)"
  by (auto simp: prod_le_def)

lemma almost_full_on_Sigma:
  assumes "almost_full_on P1 A1" and "almost_full_on P2 A2"
  shows "almost_full_on (prod_le P1 P2) (A1 × A2)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
  assume "¬ almost_full_on ?P ?A"
  then obtain f where f: "i. f i  ?A"
    and bad: "bad ?P f" by (auto simp: almost_full_on_def)
  let ?W = "λx y. P1 (fst x) (fst y)"
  let ?B = "λx y. P2 (snd x) (snd y)"
  from f have fst: "i. fst (f i)  A1" and snd: "i. snd (f i)  A2"
    by (metis SigmaE fst_conv, metis SigmaE snd_conv)
  from almost_full_on_imp_homogeneous_subseq [OF assms(1) fst]
    obtain φ :: "nat  nat" where mono: "i j. i < j  φ i < φ j"
    and *: "i j. i < j  ?W (f (φ i)) (f (φ j))" by auto
  from snd have "i. snd (f (φ i))  A2" by auto
  then have "snd  f  φ  SEQ A2" by auto
  with assms(2) have "good P2 (snd  f  φ)" by (auto simp: almost_full_on_def)
  then obtain i j :: nat
    where "i < j" and "?B (f (φ i)) (f (φ j))" by auto
  with * [OF i < j] have "?P (f (φ i)) (f (φ j))" by (simp add: case_prod_beta prod_le_def)
  with mono [OF i < j] and bad show False by auto
qed


subsection ‹Higman's Lemma for Almost-Full Relations›

lemma almost_full_on_lists:
  assumes "almost_full_on P A"
  shows "almost_full_on (list_emb P) (lists A)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
  interpret mbs ?A .
  assume "¬ ?thesis"
  from mbs' [OF this] obtain m
    where bad: "m  BAD ?P"
    and min: "g. (m, g)  gseq  good ?P g" ..
  then have lists: "i. m i  lists A"
    and ne: "i. m i  []" by auto

  define h t where "h = (λi. hd (m i))" and "t = (λi. tl (m i))"
  have m: "i. m i = h i # t i" using ne by (simp add: h_def t_def)
  
  have "i. h i  A" using ne_lists [OF ne] and lists by (auto simp add: h_def)
  from almost_full_on_imp_homogeneous_subseq [OF assms this] obtain φ :: "nat  nat"
    where less: "i j. i < j  φ i < φ j"
      and P: "i j. i < j  P (h (φ i)) (h (φ j))" by blast

  have bad_t: "bad ?P (t  φ)"
  proof
    assume "good ?P (t  φ)"
    then obtain i j where "i < j" and "?P (t (φ i)) (t (φ j))" by auto
    moreover with P have "P (h (φ i)) (h (φ j))" by blast
    ultimately have "?P (m (φ i)) (m (φ j))"
      by (subst (1 2) m) (rule list_emb_Cons2, auto)
    with less and i < j have "good ?P m" by (auto simp: good_def)
    with bad show False by blast
  qed
  
  define m' where "m' = (λi. if i < φ 0 then m i else t (φ (i - φ 0)))"

  have m'_less: "i. i < φ 0  m' i = m i" by (simp add: m'_def)
  have m'_geq: "i. i  φ 0  m' i = t (φ (i - φ 0))" by (simp add: m'_def)

  have "i. m' i  lists A" using ne_lists [OF ne] and lists by (auto simp: m'_def t_def)
  moreover have "length (m' (φ 0)) < length (m (φ 0))" using ne by (simp add: t_def m'_geq)
  moreover have "j<φ 0. m' j = m j" by (auto simp: m'_less)
  ultimately have "(m, m')  gseq" using lists by (auto simp: gseq_def)
  moreover have "bad ?P m'"
  proof
    assume "good ?P m'"
    then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by (auto simp: good_def)
    { assume "j < φ 0"
      with i < j and emb have "?P (m i) (m j)" by (auto simp: m'_less)
      with i < j and bad have False by blast }
    moreover
    { assume "φ 0  i"
      with i < j and emb have "?P (t (φ (i - φ 0))) (t (φ (j - φ 0)))"
        and "i - φ 0 < j - φ 0" by (auto simp: m'_geq)
      with bad_t have False by auto }
    moreover
    { assume "i < φ 0" and "φ 0  j"
      with i < j and emb have "?P (m i) (t (φ (j - φ 0)))" by (simp add: m'_less m'_geq)
      from list_emb_Cons [OF this, of "h (φ (j - φ 0))"]
        have "?P (m i) (m (φ (j - φ 0)))" using ne by (simp add: h_def t_def)
      moreover have "i < φ (j - φ 0)"
        using less [of 0 "j - φ 0"] and i < φ 0 and φ 0  j
        by (cases "j = φ 0") auto
      ultimately have False using bad by blast }
    ultimately show False using i < j by arith
  qed
  ultimately show False using min by blast
qed


subsection ‹Natural Numbers›

lemma almost_full_on_UNIV_nat:
  "almost_full_on (≤) (UNIV :: nat set)"
proof -
  let ?P = "subseq :: bool list  bool list  bool"
  have *: "length ` (UNIV :: bool list set) = (UNIV :: nat set)"
    by (metis Ex_list_of_length surj_def)
  have "almost_full_on (≤) (length ` (UNIV :: bool list set))"
  proof (rule almost_full_on_hom)
    fix xs ys :: "bool list"
    assume "?P xs ys"
    then show "length xs  length ys"
      by (metis list_emb_length)
  next
    have "finite (UNIV :: bool set)" by auto
    from almost_full_on_lists [OF eq_almost_full_on_finite_set [OF this]]
      show "almost_full_on ?P UNIV" unfolding lists_UNIV .
  qed
  then show ?thesis unfolding * .
qed

end

Theory Well_Quasi_Orders

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Well-Quasi-Orders›

theory Well_Quasi_Orders
imports Almost_Full_Relations
begin

subsection ‹Basic Definitions›

definition wqo_on :: "('a  'a  bool)  'a set  bool" where
  "wqo_on P A  transp_on P A  almost_full_on P A"

lemma wqo_on_UNIV:
  "wqo_on (λ_ _. True) UNIV"
  using almost_full_on_UNIV by (auto simp: wqo_on_def transp_on_def)

lemma wqo_onI [Pure.intro]:
  "transp_on P A; almost_full_on P A  wqo_on P A"
  unfolding wqo_on_def almost_full_on_def by blast

lemma wqo_on_imp_reflp_on:
  "wqo_on P A  reflp_on P A"
  using almost_full_on_imp_reflp_on by (auto simp: wqo_on_def)

lemma wqo_on_imp_transp_on:
  "wqo_on P A  transp_on P A"
  by (auto simp: wqo_on_def)

lemma wqo_on_imp_almost_full_on:
  "wqo_on P A  almost_full_on P A"
  by (auto simp: wqo_on_def)

lemma wqo_on_imp_qo_on:
  "wqo_on P A  qo_on P A"
  by (metis qo_on_def wqo_on_imp_reflp_on wqo_on_imp_transp_on)

lemma wqo_on_imp_good:
  "wqo_on P A  i. f i  A  good P f"
  by (auto simp: wqo_on_def almost_full_on_def)

lemma wqo_on_subset:
  "A  B  wqo_on P B  wqo_on P A"
  using almost_full_on_subset [of A B P]
    and transp_on_subset [of A B P]
  unfolding wqo_on_def by blast


subsection ‹Equivalent Definitions›

text ‹
  Given a quasi-order @{term P}, the following statements are equivalent:
  \begin{enumerate}
  \item @{term P} is a almost-full.
  \item @{term P} does neither allow decreasing chains nor antichains.
  \item Every quasi-order extending @{term P} is well-founded.
  \end{enumerate}
›

lemma wqo_af_conv:
  assumes "qo_on P A"
  shows "wqo_on P A  almost_full_on P A"
  using assms by (metis qo_on_def wqo_on_def)

lemma wqo_wf_and_no_antichain_conv:
  assumes "qo_on P A"
  shows "wqo_on P A  wfp_on (strict P) A  ¬ (f. antichain_on P f A)"
  unfolding wqo_af_conv [OF assms]
  using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
    and almost_full_on_imp_no_antichain_on [of P A]
    and wf_and_no_antichain_imp_qo_extension_wf [of P A]
    and every_qo_extension_wf_imp_af [OF _ assms]
    by blast

lemma wqo_extensions_wf_conv:
  assumes "qo_on P A"
  shows "wqo_on P A  (Q. (xA. yA. P x y  Q x y)  qo_on Q A  wfp_on (strict Q) A)"
  unfolding wqo_af_conv [OF assms]
  using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
    and almost_full_on_imp_no_antichain_on [of P A]
    and wf_and_no_antichain_imp_qo_extension_wf [of P A]
    and every_qo_extension_wf_imp_af [OF _ assms]
    by blast

lemma wqo_on_imp_wfp_on:
  "wqo_on P A  wfp_on (strict P) A"
  by (metis (no_types) wqo_on_imp_qo_on wqo_wf_and_no_antichain_conv)

text ‹
  The homomorphic image of a wqo set is wqo.
›
lemma wqo_on_hom:
  assumes "transp_on Q (h ` A)"
    and "xA. yA. P x y  Q (h x) (h y)"
    and "wqo_on P A"
  shows "wqo_on Q (h ` A)"
  using assms and almost_full_on_hom [of A P Q h]
  unfolding wqo_on_def by blast

text ‹
  The monomorphic preimage of a wqo set is wqo.
›
lemma wqo_on_mon:
  assumes *: "xA. yA. P x y  Q (h x) (h y)"
    and bij: "bij_betw h A B"
    and wqo: "wqo_on Q B"
  shows "wqo_on P A"
proof -
  have "transp_on P A"
  proof
    fix x y z assume [intro!]: "x  A" "y  A" "z  A"
      and "P x y" and "P y z"
    with * have "Q (h x) (h y)" and "Q (h y) (h z)" by blast+
    with wqo_on_imp_transp_on [OF wqo] have "Q (h x) (h z)"
      using bij by (auto simp: bij_betw_def transp_on_def)
    with * show "P x z" by blast
  qed
  with assms and almost_full_on_mon [of A P Q h]
    show ?thesis unfolding wqo_on_def by blast
qed


subsection ‹A Type Class for Well-Quasi-Orders›

text ‹
  In a well-quasi-order (wqo) every infinite sequence is good.
›
class wqo = preorder +
  assumes good: "good (≤) f"

lemma wqo_on_class [simp, intro]:
  "wqo_on (≤) (UNIV :: ('a :: wqo) set)"
  using good by (auto simp: wqo_on_def transp_on_def almost_full_on_def dest: order_trans)

lemma wqo_on_UNIV_class_wqo [intro!]:
  "wqo_on P UNIV  class.wqo P (strict P)"
  by (unfold_locales) (auto simp: wqo_on_def almost_full_on_def, unfold transp_on_def, blast)

text ‹
  The following lemma converts between @{const wqo_on} (for the special case that the domain is the
  universe of a type) and the class predicate @{const class.wqo}.
›
lemma wqo_on_UNIV_conv:
  "wqo_on P UNIV  class.wqo P (strict P)" (is "?lhs = ?rhs")
proof
  assume "?lhs" then show "?rhs" by auto
next
  assume "?rhs" then show "?lhs"
    unfolding class.wqo_def class.preorder_def class.wqo_axioms_def
    by (auto simp: wqo_on_def almost_full_on_def transp_on_def)
qed

text ‹
  The strict part of a wqo is well-founded.
›
lemma (in wqo) "wfP (<)"
proof -
  have "class.wqo (≤) (<)" ..
  hence "wqo_on (≤) UNIV"
    unfolding less_le_not_le [abs_def] wqo_on_UNIV_conv [symmetric] .
  from wqo_on_imp_wfp_on [OF this]
    show ?thesis unfolding less_le_not_le [abs_def] wfp_on_UNIV .
qed

lemma wqo_on_with_bot:
  assumes "wqo_on P A"
  shows "wqo_on (option_le P) A" (is "wqo_on ?P ?A")
proof -
  { from assms have trans [unfolded transp_on_def]: "transp_on P A"
      by (auto simp: wqo_on_def)
    have "transp_on ?P ?A"
      by (auto simp: transp_on_def elim!: with_bot_cases, insert trans) blast }
  moreover
  { from assms and almost_full_on_with_bot
      have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
  ultimately
  show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_option_UNIV [intro]:
  "wqo_on P UNIV  wqo_on (option_le P) UNIV"
  using wqo_on_with_bot [of P UNIV] by simp

text ‹
  When two sets are wqo, then their disjoint sum is wqo.
›
lemma wqo_on_Plus:
  assumes "wqo_on P A" and "wqo_on Q B"
  shows "wqo_on (sum_le P Q) (A <+> B)" (is "wqo_on ?P ?A")
proof -
  { from assms have trans [unfolded transp_on_def]: "transp_on P A" "transp_on Q B"
      by (auto simp: wqo_on_def)
    have "transp_on ?P ?A"
      unfolding transp_on_def by (auto, insert trans) (blast+) }
  moreover
  { from assms and almost_full_on_Plus have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
  ultimately
  show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_sum_UNIV [intro]:
  "wqo_on P UNIV  wqo_on Q UNIV  wqo_on (sum_le P Q) UNIV"
  using wqo_on_Plus [of P UNIV Q UNIV] by simp


subsection ‹Dickson's Lemma›

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 × A2)" (is "wqo_on ?P ?A")
proof -
  { from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def)
    hence "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast }
  moreover
  { from assms and almost_full_on_Sigma [of P1 A1 P2 A2]
      have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
  ultimately
  show ?thesis by (auto simp: wqo_on_def)
qed

lemmas dickson = wqo_on_Sigma

lemma wqo_on_prod_UNIV [intro]:
  "wqo_on P UNIV  wqo_on Q UNIV  wqo_on (prod_le P Q) UNIV"
  using wqo_on_Sigma [of P UNIV Q UNIV] by simp


subsection ‹Higman's Lemma›

lemma transp_on_list_emb:
  assumes "transp_on P A"
  shows "transp_on (list_emb P) (lists A)"
  using assms and list_emb_trans [of _ _ _ P]
    unfolding transp_on_def by blast

lemma wqo_on_lists:
  assumes "wqo_on P A" shows "wqo_on (list_emb P) (lists A)"
  using assms and almost_full_on_lists
    and transp_on_list_emb by (auto simp: wqo_on_def)

lemmas higman = wqo_on_lists

lemma wqo_on_list_UNIV [intro]:
  "wqo_on P UNIV  wqo_on (list_emb P) UNIV"
  using wqo_on_lists [of P UNIV] by simp

text ‹
  Every reflexive and transitive relation on a finite set is a wqo.
›
lemma finite_wqo_on:
  assumes "finite A" and refl: "reflp_on P A" and "transp_on P A"
  shows "wqo_on P A"
  using assms and finite_almost_full_on by (auto simp: wqo_on_def)

lemma finite_eq_wqo_on:
  assumes "finite A"
  shows "wqo_on (=) A"
  using finite_wqo_on [OF assms, of "(=)"]
  by (auto simp: reflp_on_def transp_on_def)

lemma wqo_on_lists_over_finite_sets:
  "wqo_on (list_emb (=)) (UNIV::('a::finite) list set)"
  using wqo_on_lists [OF finite_eq_wqo_on [OF finite [of "UNIV::('a::finite) set"]]] by simp

lemma wqo_on_map:
  fixes P and Q and h
  defines "P'  λx y. P x y  Q (h x) (h y)"
  assumes "wqo_on P A"
    and "wqo_on Q B"
    and subset: "h ` A  B"
  shows "wqo_on P' A"
proof
  let ?Q = "λx y. Q (h x) (h y)"
  from ‹wqo_on P A have "transp_on P A"
    by (rule wqo_on_imp_transp_on)
  then show "transp_on P' A"
    using ‹wqo_on Q B and subset
    unfolding wqo_on_def transp_on_def P'_def by blast

  from ‹wqo_on P A have "almost_full_on P A"
    by (rule wqo_on_imp_almost_full_on)
  from ‹wqo_on Q B have "almost_full_on Q B"
    by (rule wqo_on_imp_almost_full_on)

  show "almost_full_on P' A"
  proof
    fix f
    assume *: "i::nat. f i  A"
    from almost_full_on_imp_homogeneous_subseq [OF ‹almost_full_on P A this]
      obtain g :: "nat  nat"
      where g: "i j. i < j  g i < g j"
      and **: "i. f (g i)  A  P (f (g i)) (f (g (Suc i)))"
      using * by auto
    from chain_transp_on_less [OF ** ‹transp_on P A]
      have **: "i j. i < j  P (f (g i)) (f (g j))" .
    let ?g = "λi. h (f (g i))"
    from * and subset have B: "i. ?g i  B" by auto
    with ‹almost_full_on Q B [unfolded almost_full_on_def good_def, THEN bspec, of ?g]
      obtain i j :: nat
      where "i < j" and "Q (?g i) (?g j)" by blast
    with ** [OF i < j] have "P' (f (g i)) (f (g j))"
      by (auto simp: P'_def)
    with g [OF i < j] show "good P' f" by (auto simp: good_def)
  qed
qed

lemma wqo_on_UNIV_nat:
  "wqo_on (≤) (UNIV :: nat set)"
  unfolding wqo_on_def transp_on_def
  using almost_full_on_UNIV_nat by simp

end

Theory Kruskal

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Kruskal's Tree Theorem›

theory Kruskal
imports Well_Quasi_Orders
begin

locale kruskal_tree =
  fixes F :: "('b × nat) set"
    and mk :: "'b  'a list  ('a::size)"
    and root :: "'a  'b × nat"
    and args :: "'a  'a list"
    and trees :: "'a set"
  assumes size_arg: "t  trees  s  set (args t)  size s < size t"
    and root_mk: "(f, length ts)  F  root (mk f ts) = (f, length ts)"
    and args_mk: "(f, length ts)  F  args (mk f ts) = ts"
    and mk_root_args: "t  trees  mk (fst (root t)) (args t) = t"
    and trees_root: "t  trees  root t  F"
    and trees_arity: "t  trees  length (args t) = snd (root t)"
    and trees_args: "s. t  trees  s  set (args t)  s  trees"
begin

lemma mk_inject [iff]:
  assumes "(f, length ss)  F" and "(g, length ts)  F"
  shows "mk f ss = mk g ts  f = g  ss = ts"
proof -
  { assume "mk f ss = mk g ts"
    then have "root (mk f ss) = root (mk g ts)"
      and "args (mk f ss) = args (mk g ts)" by auto }
  show ?thesis
    using root_mk [OF assms(1)] and root_mk [OF assms(2)]
      and args_mk [OF assms(1)] and args_mk [OF assms(2)] by auto
qed

inductive emb for P
where
  arg: "(f, m)  F; length ts = m; tset ts. t  trees;
    t  set ts; emb P s t  emb P s (mk f ts)" |
  list_emb: "(f, m)  F; (g, n)  F; length ss = m; length ts = n;
    s  set ss. s  trees; t  set ts. t  trees;
    P (f, m) (g, n); list_emb (emb P) ss ts  emb P (mk f ss) (mk g ts)"
  monos list_emb_mono

lemma almost_full_on_trees:
  assumes "almost_full_on P F"
  shows "almost_full_on (emb P) trees" (is "almost_full_on ?P ?A")
proof (rule ccontr)
  interpret mbs ?A .
  assume "¬ ?thesis"
  from mbs' [OF this] obtain m
    where bad: "m  BAD ?P"
    and min: "g. (m, g)  gseq  good ?P g" ..
  then have trees: "i. m i  trees" by auto

  define r where "r i = root (m i)" for i
  define a where "a i = args (m i)" for i
  define S where "S = {set (a i) | i. True}"

  have m: "i. m i = mk (fst (r i)) (a i)"
   by (simp add: r_def a_def mk_root_args [OF trees])
  have lists: "i. a i  lists S" by (auto simp: a_def S_def)
  have arity: "i. length (a i) = snd (r i)"
    using trees_arity [OF trees] by (auto simp: r_def a_def)
  then have sig: "i. (fst (r i), length (a i))  F"
    using trees_root [OF trees] by (auto simp: a_def r_def)
  have a_trees: "i. t  set (a i). t  trees" by (auto simp: a_def trees_args [OF trees])

  have "almost_full_on ?P S"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain s :: "nat  'a"
      where S: "i. s i  S" and bad_s: "bad ?P s" by (auto simp: almost_full_on_def)

    define n where "n = (LEAST n. k. s k  set (a n))"
    have "n. k. s k  set (a n)" using S by (force simp: S_def)
    from LeastI_ex [OF this] obtain k
      where sk: "s k  set (a n)" by (auto simp: n_def)
    have args: "k. m  n. s k  set (a m)"
      using S by (auto simp: S_def) (metis Least_le n_def)

    define m' where "m' i = (if i < n then m i else s (k + (i - n)))" for i
    
    have m'_less: "i. i < n  m' i = m i" by (simp add: m'_def)
    have m'_geq: "i. i  n  m' i = s (k + (i - n))" by (simp add: m'_def)

    have "bad ?P m'"
    proof
      assume "good ?P m'"
      then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by auto
      { assume "j < n"
        with i < j and emb have "?P (m i) (m j)" by (auto simp: m'_less)
        with i < j and bad have False by blast }
      moreover
      { assume "n  i"
        with i < j and emb have "?P (s (k + (i - n))) (s (k + (j - n)))"
          and "k + (i - n) < k + (j - n)" by (auto simp: m'_geq)
        with bad_s have False by auto }
      moreover
      { assume "i < n" and "n  j"
        with i < j and emb have *: "?P (m i) (s (k + (j - n)))" by (auto simp: m'_less m'_geq)
        with args obtain l where "l  n" and **: "s (k + (j - n))  set (a l)" by blast
        from emb.arg [OF sig [of l] _ a_trees [of l] ** *]
          have "?P (m i) (m l)" by (simp add: m)
        moreover have "i < l" using i < n and n  l by auto
        ultimately have False using bad by blast }
      ultimately show False using i < j by arith
    qed
    moreover have "(m, m')  gseq"
    proof -
      have "m  SEQ ?A" using trees by auto
      moreover have "m'  SEQ ?A"
        using trees and S and trees_args [OF trees] by (auto simp: m'_def a_def S_def)
      moreover have "i < n. m i = m' i" by (auto simp: m'_less)
      moreover have "size (m' n) < size (m n)"
        using sk and size_arg [OF trees, unfolded m]
        by (auto simp: m m'_geq root_mk [OF sig] args_mk [OF sig])
      ultimately show ?thesis by (auto simp: gseq_def)
    qed
    ultimately show False using min by blast
  qed
  from almost_full_on_lists [OF this, THEN almost_full_on_imp_homogeneous_subseq, OF lists]
    obtain φ :: "nat  nat"
    where less: "i j. i < j  φ i < φ j"
      and lemb: "i j. i < j  list_emb ?P (a (φ i)) (a (φ j))" by blast
  have roots: "i. r (φ i)  F" using trees [THEN trees_root] by (auto simp: r_def)
  then have "r  φ  SEQ F" by auto
  with assms have "good P (r  φ)" by (auto simp: almost_full_on_def)
  then obtain i j
    where "i < j" and "P (r (φ i)) (r (φ j))" by auto
  with lemb [OF i < j] have "?P (m (φ i)) (m (φ j))"
    using sig and arity and a_trees by (auto simp: m intro!: emb.list_emb)
  with less [OF i < j] and bad show False by blast
qed

inductive_cases
  emb_mk2 [consumes 1, case_names arg list_emb]: "emb P s (mk g ts)"

inductive_cases
  list_emb_Nil2_cases: "list_emb P xs []" and
  list_emb_Cons_cases: "list_emb P xs (y#ys)"

lemma list_emb_trans_right:
  assumes "list_emb P xs ys" and "list_emb (λy z. P y z  (x. P x y  P x z)) ys zs" 
  shows "list_emb P xs zs"
  using assms(2, 1) by (induct arbitrary: xs) (auto elim!: list_emb_Nil2_cases list_emb_Cons_cases)

lemma emb_trans:
  assumes trans: "f g h. f  F  g  F  h  F  P f g  P g h  P f h"
  assumes "emb P s t" and "emb P t u"
  shows "emb P s u"
using assms(3, 2)
proof (induct arbitrary: s)
  case (arg f m ts v)
  then show ?case by (auto intro: emb.arg)
next
  case (list_emb f m g n ss ts)
  note IH = this
  from ‹emb P s (mk f ss)
    show ?case
  proof (cases rule: emb_mk2)
    case arg
    then show ?thesis using IH by (auto elim!: list_emb_set intro: emb.arg)
  next
    case list_emb
    then show ?thesis using IH by (auto intro: emb.intros dest: trans list_emb_trans_right)
  qed
qed

lemma transp_on_emb:
  assumes "transp_on P F"
  shows "transp_on (emb P) trees"
  using assms and emb_trans [of P] unfolding transp_on_def by blast

lemma kruskal:
  assumes "wqo_on P F"
  shows "wqo_on (emb P) trees"
  using almost_full_on_trees [of P] and assms by (metis transp_on_emb wqo_on_def)

end

end

Theory Kruskal_Examples

theory Kruskal_Examples
imports Kruskal
begin

datatype 'a tree = Node 'a "'a tree list"

fun node
where
  "node (Node f ts) = (f, length ts)"

fun succs
where
  "succs (Node f ts) = ts"

inductive_set trees for A
where
  "f  A  t  set ts. t  trees A  Node f ts  trees A"

lemma [simp]:
  "trees UNIV = UNIV"
proof -
  { fix t :: "'a tree"
    have "t  trees UNIV"
      by (induct t) (auto intro: trees.intros) }
  then show ?thesis by auto
qed

interpretation kruskal_tree_tree: kruskal_tree "A × UNIV" Node node succs "trees A" for A
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: trees.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_tree_tree.almost_full_on_trees
thm kruskal_tree_tree.kruskal

definition "tree_emb A P = kruskal_tree_tree.emb A (prod_le P (λ_ _. True))"

lemma wqo_on_trees:
  assumes "wqo_on P A"
  shows "wqo_on (tree_emb A P) (trees A)"
  using wqo_on_Sigma [OF assms wqo_on_UNIV, THEN kruskal_tree_tree.kruskal]
  by (simp add: tree_emb_def)

text ‹
If the type @{typ "'a"} is well-quasi-ordered by P›, then trees of type @{typ "'a tree"}
are well-quasi-ordered by the homeomorphic embedding relation.
›
instantiation tree :: (wqo) wqo
begin
definition "s  t  tree_emb UNIV (≤) s t"
definition "(s :: 'a tree) < t  s  t  ¬ (t  s)"

instance
  by (rule class.wqo.of_class.intro)
     (auto simp: less_eq_tree_def [abs_def] less_tree_def [abs_def]
           intro: wqo_on_trees [of _ UNIV, simplified])
end

datatype ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"

fun root
where
  "root (Fun f ts) = (f, length ts)"

fun args
where
  "args (Fun f ts) = ts"

inductive_set gterms for F
where
  "(f, n)  F  length ts = n  s  set ts. s  gterms F  Fun f ts  gterms F"

interpretation kruskal_term: kruskal_tree F Fun root args "gterms F" for F
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: gterms.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_term.almost_full_on_trees

inductive_set terms
where
  "t  set ts. t  terms  Fun f ts  terms"

interpretation kruskal_variadic: kruskal_tree UNIV Fun root args terms
  apply (unfold_locales)
  apply auto
  apply (case_tac [!] t rule: terms.cases)
  apply auto
  by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_variadic.almost_full_on_trees

datatype 'a exp = V 'a | C nat | Plus "'a exp" "'a exp"

datatype 'a symb = v 'a | c nat | p

fun mk
where
  "mk (v x) [] = V x" |
  "mk (c n) [] = C n" |
  "mk p [a, b] = Plus a b"

fun rt
where
  "rt (V x) = (v x, 0::nat)" |
  "rt (C n) = (c n, 0)" |
  "rt (Plus a b) = (p, 2)"

fun ags
where
  "ags (V x) = []" |
  "ags (C n) = []" |
  "ags (Plus a b) = [a, b]"

inductive_set exps
where
  "V x  exps" |
  "C n  exps" |
  "a  exps  b  exps  Plus a b  exps"

lemma [simp]:
  assumes "length ts = 2"
  shows "rt (mk p ts) = (p, 2)"
  using assms by (induct ts) (auto, case_tac ts, auto)

lemma [simp]:
  assumes "length ts = 2"
  shows "ags (mk p ts) = ts"
  using assms by (induct ts) (auto, case_tac ts, auto)

interpretation kruskal_exp: kruskal_tree
  "{(v x, 0) | x. True}  {(c n, 0) | n. True}  {(p, 2)}"
  mk rt ags exps
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: exps.cases)
by auto

thm kruskal_exp.almost_full_on_trees

hide_const (open) tree_emb V C Plus v c p

end

Theory Wqo_Instances

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Instances of Well-Quasi-Orders›

theory Wqo_Instances
imports Kruskal
begin


subsection ‹The Option Type is Well-Quasi-Ordered›

instantiation option :: (wqo) wqo
begin
definition "x  y  option_le (≤) x y"
definition "(x :: 'a option) < y  x  y  ¬ (y  x)"

instance
  by (rule class.wqo.of_class.intro)
     (auto simp: less_eq_option_def [abs_def] less_option_def [abs_def])
end


subsection ‹The Sum Type is Well-Quasi-Ordered›

instantiation sum :: (wqo, wqo) wqo
begin
definition "x  y  sum_le (≤) (≤) x y"
definition "(x :: 'a + 'b) < y  x  y  ¬ (y  x)"

instance
  by (rule class.wqo.of_class.intro)
     (auto simp: less_eq_sum_def [abs_def] less_sum_def [abs_def])
end


subsection ‹Pairs are Well-Quasi-Ordered›

text ‹If types @{typ "'a"} and @{typ "'b"} are well-quasi-ordered by P›
and Q›, then pairs of type @{typ "'a × 'b"} are well-quasi-ordered by
the pointwise combination of P› and Q›.›

instantiation prod :: (wqo, wqo) wqo
begin
definition "p  q  prod_le (≤) (≤) p q"
definition "(p :: 'a × 'b) < q  p  q  ¬ (q  p)"

instance
  by (rule class.wqo.of_class.intro)
     (auto simp: less_eq_prod_def [abs_def] less_prod_def [abs_def])
end


subsection ‹Lists are Well-Quasi-Ordered›

text ‹If the type @{typ "'a"} is well-quasi-ordered by P›, then
lists of type @{typ "'a list"} are well-quasi-ordered by the homeomorphic
embedding relation.›

instantiation list :: (wqo) wqo
begin
definition "xs  ys  list_emb (≤) xs ys"
definition "(xs :: 'a list) < ys  xs  ys  ¬ (ys  xs)"

instance
  by (rule class.wqo.of_class.intro)
     (auto simp: less_eq_list_def [abs_def] less_list_def [abs_def])
end

end

Theory Multiset_Extension

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Multiset Extension of Orders (as Binary Predicates)›

(*TODO: move theory (and maybe rename)*)

theory Multiset_Extension
imports
  Open_Induction.Restricted_Predicates
  "HOL-Library.Multiset"
begin

definition multisets :: "'a set  'a multiset set" where
  "multisets A = {M. set_mset M  A}"

lemma in_multisets_iff:
  "M  multisets A  set_mset M  A"
  by (simp add: multisets_def)

lemma empty_multisets [simp]:
  "{#}  multisets F"
  by (simp add: in_multisets_iff)

lemma multisets_union [simp]:
  "M  multisets A  N  multisets A  M + N  multisets A"
  by (auto simp add: in_multisets_iff)

definition mulex1 :: "('a  'a  bool)  'a multiset  'a multiset  bool" where
  "mulex1 P = (λM N. (M, N)  mult1 {(x, y). P x y})"

lemma mulex1_empty [iff]:
  "mulex1 P M {#}  False"
  using not_less_empty [of M "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_add: "mulex1 P N (M0 + {#a#}) 
  (M. mulex1 P M M0  N = M + {#a#}) 
  (K. (b. b ∈# K  P b a)  N = M0 + K)"
  using less_add [of N a M0 "{(x, y). P x y}"]
  by (auto simp: mulex1_def)

lemma mulex1_self_add_right [simp]:
  "mulex1 P A (add_mset a A)"
proof -
  let ?R = "{(x, y). P x y}"
  thm mult1_def
  have "A + {#a#} = A + {#a#}" by simp
  moreover have "A = A + {#}" by simp
  moreover have "b. b ∈# {#}  (b, a)  ?R" by simp
  ultimately have "(A, add_mset a A)  mult1 ?R"
    unfolding mult1_def by blast
  then show ?thesis by (simp add: mulex1_def)
qed

lemma empty_mult1 [simp]:
  "({#}, {#a#})  mult1 R"
proof -
  have "{#a#} = {#} + {#a#}" by simp
  moreover have "{#} = {#} + {#}" by simp
  moreover have "b. b ∈# {#}  (b, a)  R" by simp
  ultimately show ?thesis unfolding mult1_def by force
qed

lemma empty_mulex1 [simp]:
  "mulex1 P {#} {#a#}"
  using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def)

definition mulex_on :: "('a  'a  bool)  'a set  'a multiset  'a multiset  bool" where
  "mulex_on P A = (restrict_to (mulex1 P) (multisets A))++"

abbreviation mulex :: "('a  'a  bool)  'a multiset  'a multiset  bool" where
  "mulex P  mulex_on P UNIV"

lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]:
  assumes "mulex_on P A M N"
    and "M N. M  multisets A; N  multisets A; mulex1 P M N  Q M N"
    and "L M N. mulex_on P A L M; Q L M; N  multisets A; mulex1 P M N  Q L N"
  shows "Q M N"
  using assms unfolding mulex_on_def by (induct) blast+

lemma mulex_on_self_add_singleton_right [simp]:
  assumes "a  A" and "M  multisets A"
  shows "mulex_on P A M (add_mset a M)"
proof -
  have "mulex1 P M (M + {#a#})" by simp
  with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)"
    by (auto simp: multisets_def)
  then show ?thesis unfolding mulex_on_def by blast
qed

lemma singleton_multisets [iff]:
  "{#x#}  multisets A  x  A"
  by (auto simp: multisets_def)

lemma union_multisetsD:
  assumes "M + N  multisets A"
  shows "M  multisets A  N  multisets A"
  using assms by (auto simp: multisets_def)

lemma mulex_on_multisetsD [dest]:
  assumes "mulex_on P F M N"
  shows "M  multisets F" and "N  multisets F"
  using assms by (induct) auto

lemma union_multisets_iff [iff]:
  "M + N  multisets A  M  multisets A  N  multisets A"
  by (auto dest: union_multisetsD)

lemma add_mset_multisets_iff [iff]:
  "add_mset a M  multisets A  a  A  M  multisets A"
  unfolding add_mset_add_single[of a M] union_multisets_iff by auto

lemma mulex_on_trans:
  "mulex_on P A L M  mulex_on P A M N  mulex_on P A L N"
  by (auto simp: mulex_on_def)

lemma transp_on_mulex_on:
  "transp_on (mulex_on P A) B"
  using mulex_on_trans [of P A] by (auto simp: transp_on_def)
  
lemma mulex_on_add_right [simp]:
  assumes "mulex_on P A M N" and "a  A"
  shows "mulex_on P A M (add_mset a N)"
proof -
  from assms have "a  A" and "N  multisets A" by auto
  then have "mulex_on P A N (add_mset a N)" by simp
  with ‹mulex_on P A M N show ?thesis by (rule mulex_on_trans)
qed

lemma empty_mulex_on [simp]:
  assumes "M  {#}" and "M  multisets A"
  shows "mulex_on P A {#} M"
using assms
proof (induct M)
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}"
    with add show ?thesis by (auto simp: mulex_on_def)
  next
    assume "M  {#}"
    with add show ?thesis by (auto intro: mulex_on_trans)
  qed
qed simp

lemma mulex_on_self_add_right [simp]:
  assumes "M  multisets A" and "K  multisets A" and "K  {#}"
  shows "mulex_on P A M (M + K)"
using assms
proof (induct K)
  case empty
  then show ?case by (cases "K = {#}") auto
next
  case (add a M)
  show ?case
  proof (cases "M = {#}")
    assume "M = {#}" with add show ?thesis by auto
  next
    assume "M  {#}" with add show ?thesis
      by (auto dest: mulex_on_add_right simp add: ac_simps)
  qed
qed

lemma mult1_singleton [iff]:
  "({#x#}, {#y#})  mult1 R  (x, y)  R"
proof
  assume "(x, y)  R"
  then have "{#y#} = {#} + {#y#}"
    and "{#x#} = {#} + {#x#}"
    and "b. b ∈# {#x#}  (b, y)  R" by auto
  then show "({#x#}, {#y#})  mult1 R" unfolding mult1_def by blast
next
  assume "({#x#}, {#y#})  mult1 R"
  then obtain M0 K a
    where "{#y#} = add_mset a M0"
    and "{#x#} = M0 + K"
    and "b. b ∈# K  (b, a)  R"
    unfolding mult1_def by blast
  then show "(x, y)  R" by (auto simp: add_eq_conv_diff)
qed

lemma mulex1_singleton [iff]:
  "mulex1 P {#x#} {#y#}  P x y"
  using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def)

lemma singleton_mulex_onI:
  "P x y  x  A  y  A  mulex_on P A {#x#} {#y#}"
  by (auto simp: mulex_on_def)

lemma reflclp_mulex_on_add_right [simp]:
  assumes "(mulex_on P A)== M N" and "M  multisets A" and "a  A"
  shows "mulex_on P A M (N + {#a#})"
  using assms by (cases "M = N") simp_all

lemma reflclp_mulex_on_add_right' [simp]:
  assumes "(mulex_on P A)== M N" and "M  multisets A" and "a  A"
  shows "mulex_on P A M ({#a#} + N)"
  using reflclp_mulex_on_add_right [OF assms] by (simp add: ac_simps)

lemma mulex_on_union_right [simp]:
  assumes "mulex_on P F A B" and "K  multisets F"
  shows "mulex_on P F A (K + B)"
using assms
proof (induct K)
  case (add a K)
  then have "a  F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps)
  then have "mulex_on P F A ((B + K) + {#a#})" by simp
  then show ?case by (simp add: ac_simps)
qed simp

lemma mulex_on_union_right' [simp]:
  assumes "mulex_on P F A B" and "K  multisets F"
  shows "mulex_on P F A (B + K)"
  using mulex_on_union_right [OF assms] by (simp add: ac_simps)

text ‹Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.›
lemma accessible_on_mulex1_multisets:
  assumes wf: "wfp_on P A"
  shows "Mmultisets A. accessible_on (mulex1 P) (multisets A) M"
proof
  let ?P = "mulex1 P"
  let ?A = "multisets A"
  let ?acc = "accessible_on ?P ?A"
  {
    fix M M0 a
    assume M0: "?acc M0"
      and "a  A"
      and "M0  ?A"
      and wf_hyp: "b. b  A; P b a  (M. ?acc (M)  ?acc (M + {#b#}))"
      and acc_hyp: "M. M  ?A  ?P M M0  ?acc (M + {#a#})"
    then have "add_mset a M0  ?A" by (auto simp: multisets_def)
    then have "?acc (add_mset a M0)"
    proof (rule accessible_onI [of "add_mset a M0"])
      fix N
      assume "N  ?A"
        and "?P N (add_mset a M0)"
      then have "((M. M  ?A  ?P M M0  N = M + {#a#}) 
          (K. (b. b ∈# K  P b a)  N = M0 + K))"
        using mulex1_add [of P N M0 a] by (auto simp: multisets_def)
      then show "?acc (N)"
      proof (elim exE disjE conjE)
        fix M assume "M  ?A" and "?P M M0" and N: "N = M + {#a#}"
        from acc_hyp have "M  ?A  ?P M M0  ?acc (M + {#a#})" ..
        with M  ?A and ?P M M0 have "?acc (M + {#a#})" by blast
        then show "?acc (N)" by (simp only: N)
      next
        fix K
        assume N: "N = M0 + K"
        assume "b. b ∈# K  P b a"
        moreover from N and N  ?A have "K  ?A" by (auto simp: multisets_def)
        ultimately have "?acc (M0 + K)"
        proof (induct K)
          case empty
          from M0 show "?acc (M0 + {#})" by simp
        next
          case (add x K)
          from add.prems have "x  A" and "P x a" by (auto simp: multisets_def)
          with wf_hyp have "M. ?acc M  ?acc (M + {#x#})" by blast
          moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def)
          ultimately show "?acc (M0 + (add_mset x K))" by simp
        qed
        then show "?acc N" by (simp only: N)
      qed
    qed
  } note tedious_reasoning = this

  fix M
  assume "M  ?A"
  then show "?acc M"
  proof (induct M)
    show "?acc {#}"
    proof (rule accessible_onI)
      show "{#}  ?A" by (auto simp: multisets_def)
    next
      fix b assume "?P b {#}" then show "?acc b" by simp
    qed
  next
    case (add a M)
    then have "?acc M" by (auto simp: multisets_def)
    from add have "a  A" by (auto simp: multisets_def)
    with wf have "M. ?acc M  ?acc (add_mset a M)"
    proof (induct)
      case (less a)
      then have r: "b. b  A; P b a  (M. ?acc M  ?acc (M + {#b#}))" by auto
      show "M. ?acc M  ?acc (add_mset a M)"
      proof (intro allI impI)
        fix M'
        assume "?acc M'"
        moreover then have "M'  ?A" by (blast dest: accessible_on_imp_mem)
        ultimately show "?acc (add_mset a M')"
          by (induct) (rule tedious_reasoning [OF _ a  A _ r], auto)
      qed
    qed
    with ?acc (M) show "?acc (add_mset a M)" by blast
  qed
qed

lemmas wfp_on_mulex1_multisets =
  accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on]

lemmas irreflp_on_mulex1 =
  wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on]

lemma wfp_on_mulex_on_multisets:
  assumes "wfp_on P A"
  shows "wfp_on (mulex_on P A) (multisets A)"
  using wfp_on_mulex1_multisets [OF assms]
  by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv)

lemmas irreflp_on_mulex_on =
  wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on]

lemma mulex1_union:
  "mulex1 P M N  mulex1 P (K + M) (K + N)"
  by (auto simp: mulex1_def mult1_union)

lemma mulex_on_union:
  assumes "mulex_on P A M N" and "K  multisets A"
  shows "mulex_on P A (K + M) (K + N)"
using assms
proof (induct)
  case (base M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from base have "(K + M)  multisets A"
    and "(K + N)  multisets A" by (auto simp: multisets_def)
  ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto
  then show ?case by (auto simp: mulex_on_def)
next
  case (step L M N)
  then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
  moreover from step have "(K + M)  multisets A" and "(K + N)  multisets A" by blast+
  ultimately have "(restrict_to (mulex1 P) (multisets A))++ (K + M) (K + N)" by auto
  moreover have "mulex_on P A (K + L) (K + M)" using step by blast
  ultimately show ?case by (auto simp: mulex_on_def)
qed

lemma mulex_on_union':
  assumes "mulex_on P A M N" and "K  multisets A"
  shows "mulex_on P A (M + K) (N + K)"
  using mulex_on_union [OF assms] by (simp add: ac_simps)

lemma mulex_on_add_mset:
  assumes "mulex_on P A M N" and "m  A"
  shows "mulex_on P A (add_mset m M) (add_mset m N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of m N]
  apply (rule mulex_on_union')
  using assms by auto

lemma union_mulex_on_mono:
  "mulex_on P F A C  mulex_on P F B D  mulex_on P F (A + B) (C + D)"
  by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union')

lemma mulex_on_add_mset':
  assumes "P m n" and "m  A" and "n  A" and "M  multisets A"
  shows "mulex_on P A (add_mset m M) (add_mset n M)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n M]
  apply (rule mulex_on_union)
  using assms by (auto simp: mulex_on_def)

lemma mulex_on_add_mset_mono:
  assumes "P m n" and "m  A" and "n  A" and "mulex_on P A M N"
  shows "mulex_on P A (add_mset m M) (add_mset n N)"
  unfolding add_mset_add_single[of m M] add_mset_add_single[of n N]
  apply (rule union_mulex_on_mono)
  using assms by (auto simp: mulex_on_def)

lemma union_mulex_on_mono1:
  "A  multisets F  (mulex_on P F)== A C  mulex_on P F B D 
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union)

lemma union_mulex_on_mono2:
  "B  multisets F  mulex_on P F A C  (mulex_on P F)== B D 
    mulex_on P F (A + B) (C + D)"
  by (auto intro: union_mulex_on_mono mulex_on_union')

lemma mult1_mono:
  assumes "x y. x  A; y  A; (x, y)  R  (x, y)  S"
    and "M  multisets A"
    and "N  multisets A"
    and "(M, N)  mult1 R"
  shows "(M, N)  mult1 S"
  using assms unfolding mult1_def multisets_def
  by auto (metis (full_types) subsetD)

lemma mulex1_mono:
  assumes "x y. x  A; y  A; P x y  Q x y"
    and "M  multisets A"
    and "N  multisets A"
    and "mulex1 P M N"
  shows "mulex1 Q M N"
  using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N]
    and assms unfolding mulex1_def by blast

lemma mulex_on_mono:
  assumes *: "x y. x  A; y  A; P x y  Q x y"
    and "mulex_on P A M N"
  shows "mulex_on Q A M N"
proof -
  let ?rel = "λP. (restrict_to (mulex1 P) (multisets A))"
  from ‹mulex_on P A M N have "(?rel P)++ M N" by (simp add: mulex_on_def)
  then have "(?rel Q)++ M N"
  proof (induct rule: tranclp.induct)
    case (r_into_trancl M N)
    then have "M  multisets A" and "N  multisets A" by auto
    from mulex1_mono [OF * this] and r_into_trancl
      show ?case by auto
  next
    case (trancl_into_trancl L M N)
    then have "M  multisets A" and "N  multisets A" by auto
    from mulex1_mono [OF * this] and trancl_into_trancl
      have "?rel Q M N" by auto
    with (?rel Q)++ L M show ?case by (rule tranclp.trancl_into_trancl)
  qed
  then show ?thesis by (simp add: mulex_on_def)
qed

lemma mult1_reflcl:
  assumes "(M, N)  mult1 R"
  shows "(M, N)  mult1 (R=)"
  using assms by (auto simp: mult1_def)

lemma mulex1_reflclp:
  assumes "mulex1 P M N"
  shows "mulex1 (P==) M N"
  using mulex1_mono [of UNIV P "P==" M N, OF _ _ _ assms]
  by (auto simp: multisets_def)

lemma mulex_on_reflclp:
  assumes "mulex_on P A M N"
  shows "mulex_on (P==) A M N"
  using mulex_on_mono [OF _ assms, of "P=="] by auto                  

lemma surj_on_multisets_mset:
  "Mmultisets A. xslists A. M = mset xs"
proof
  fix M
  assume "M  multisets A"
  then show "xslists A. M = mset xs"
  proof (induct M)
    case empty show ?case by simp
  next
    case (add a M)
    then obtain xs where "xs  lists A" and "M = mset xs" by auto
    then have "add_mset a M = mset (a # xs)" by simp
    moreover have "a # xs  lists A" using xs  lists A and add by auto
    ultimately show ?case by blast
  qed
qed

lemma image_mset_lists [simp]:
  "mset ` lists A = multisets A"
  using surj_on_multisets_mset [of A]
  by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI)

lemma multisets_UNIV [simp]: "multisets UNIV = UNIV"
  by (metis image_mset_lists lists_UNIV surj_mset)

lemma non_empty_multiset_induct [consumes 1, case_names singleton add]:
  assumes "M  {#}"
    and "x. P {#x#}"
    and "x M. P M  P (add_mset x M)"
  shows "P M"
  using assms by (induct M) auto

lemma mulex_on_all_strict:
  assumes "X  {#}"
  assumes "X  multisets A" and "Y  multisets A"
    and *: "y. y ∈# Y  (x. x ∈# X  P y x)"
  shows "mulex_on P A Y X"
using assms
proof (induction X arbitrary: Y rule: non_empty_multiset_induct)
  case (singleton x)
  then have "mulex1 P Y {#x#}"
    unfolding mulex1_def mult1_def
    by auto
  with singleton show ?case by (auto simp: mulex_on_def)
next
  case (add x M)
  let ?Y = "{# y ∈# Y. x. x ∈# M  P y x #}"
  let ?Z = "Y - ?Y"
  have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto
  from Y  multisets A have "?Y  multisets A" by (metis multiset_partition union_multisets_iff)
  moreover have "y. y ∈# ?Y  (x. x ∈# M  P y x)" by auto
  moreover have "M  multisets A" using add by auto
  ultimately have "mulex_on P A ?Y M" using add by blast
  moreover have "mulex_on P A ?Z {#x#}"
  proof -
    have "{#x#} = {#} + {#x#}" by simp
    moreover have "?Z = {#} + ?Z" by simp
    moreover have "y. y ∈# ?Z  P y x"
      using add.prems by (auto simp add: in_diff_count split: if_splits)
    ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast
    moreover have "{#x#}  multisets A" using add.prems by auto
    moreover have "?Z  multisets A"
      using Y  multisets A by (metis diff_union_cancelL multiset_partition union_multisetsD)
    ultimately show ?thesis by (auto simp: mulex_on_def)
  qed
  ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono)
  then show ?case using Y by (simp add: ac_simps)
qed

text ‹The following lemma shows that the textbook definition (e.g.,
``Term Rewriting and All That'') is the same as the one used below.›
lemma diff_set_Ex_iff:
  "X  {#}  X ⊆# M  N = (M - X) + Y  X  {#}  (Z. M = Z + X  N = Z + Y)"
  by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute)

text ‹Show that @{const mulex_on} is equivalent to the textbook definition
of multiset-extension for transitive base orders.›
lemma mulex_on_alt_def:
  assumes trans: "transp_on P A"
  shows "mulex_on P A M N  M  multisets A  N  multisets A  (X Y Z.
    X  {#}  N = Z + X  M = Z + Y  (y. y ∈# Y  (x. x ∈# X  P y x)))"
  (is "?P M N  ?Q M N")
proof
  assume "?P M N" then show "?Q M N"
  proof (induct M N)
    case (base M N)
    then obtain a M0 K where N: "N = M0 + {#a#}"
      and M: "M = M0 + K"
      and *: "b. b ∈# K  P b a"
      and "M  multisets A" and "N  multisets A" by (auto simp: mulex1_def mult1_def)
    moreover then have "{#a#}  multisets A" and "K  multisets A" by auto
    moreover have "{#a#}  {#}" by auto
    moreover have "N = M0 + {#a#}" by fact
    moreover have "M = M0 + K" by fact
    moreover have "y. y ∈# K  (x. x ∈# {#a#}  P y x)" using * by auto
    ultimately show ?case by blast
  next
    case (step L M N)
    then obtain X Y Z
      where "L  multisets A" and "M  multisets A" and "N  multisets A"
      and "X  multisets A" and "Y  multisets A"
      and M: "M = Z + X"
      and L: "L = Z + Y" and "X  {#}"
      and Y: "y. y ∈# Y  (x. x ∈# X  P y x)"
      and "mulex1 P M N"
      by blast
    from ‹mulex1 P M N obtain a M0 K
      where N: "N = add_mset a M0" and M': "M = M0 + K"
      and *: "b. b ∈# K  P b a" unfolding mulex1_def mult1_def by blast
    have L': "L = (M - X) + Y" by (simp add: L M)
    have K: "y. y ∈# K  (x. x ∈# {#a#}  P y x)" using * by auto

    txt ‹The remainder of the proof is adapted from the proof of Lemma 2.5.4. of
    the book ``Term Rewriting and All That.''›
    let ?X = "add_mset a (X - K)"
    let ?Y = "(K - X) + Y"
    
    have "L  multisets A" and "N  multisets A" by fact+
    moreover have "?X  {#}  (Z. N = Z + ?X  L = Z + ?Y)"
    proof -
      have "?X  {#}" by auto
      moreover have "?X ⊆# N"
        using M N M' by (simp add: add.commute [of "{#a#}"])
          (metis Multiset.diff_subset_eq_self add.commute add_diff_cancel_right)
      moreover have "L = (N - ?X) + ?Y"
      proof (rule multiset_eqI)
        fix x :: 'a
        let ?c = "λM. count M x"
        let ?ic = "λx. int (?c x)"
        from ?X ⊆# N have *: "?c {#a#} + ?c (X - K)  ?c N"
          by (auto simp add: subseteq_mset_def split: if_splits)
        from * have **: "?c (X - K)  ?c M0" unfolding N by (auto split: if_splits)
        have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp
        also have " = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp
        also have " = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y"
          using of_nat_diff [OF *] by simp
        also have " = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp
        also have " = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp
        also have " = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp
        also have " = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N)
        also have " = ?ic L"
          unfolding L' M' N
          using ** by (simp add: algebra_simps)
        finally show "?c L = ?c (N - ?X + ?Y)" by simp
      qed
      ultimately show ?thesis by (metis diff_set_Ex_iff)
    qed
    moreover have "y. y ∈# ?Y  (x. x ∈# ?X  P y x)"
    proof (intro allI impI)
      fix y assume "y ∈# ?Y"
      then have "y ∈# K - X  y ∈# Y" by auto
      then show "x. x ∈# ?X  P y x"
      proof
        assume "y ∈# K - X"
        then have "y ∈# K" by (rule in_diffD)
        with K show ?thesis by auto
      next
        assume "y ∈# Y"
        with Y obtain x where "x ∈# X" and "P y x" by blast
        { assume "x ∈# X - K" with P y x have ?thesis by auto }
        moreover
        { assume "x ∈# K" with * have "P x a" by auto
          moreover have "y  A" using Y  multisets A and y ∈# Y by (auto simp: multisets_def)
          moreover have "a  A" using N  multisets A by (auto simp: N)
          moreover have "x  A" using M  multisets A and x ∈# K by (auto simp: M' multisets_def)
          ultimately have "P y a" using P y x and trans unfolding transp_on_def by blast
          then have ?thesis by force }
        moreover from x ∈# X have "x ∈# X - K  x ∈# K"
          by (auto simp add: in_diff_count not_in_iff)
        ultimately show ?thesis by auto
      qed
    qed
    ultimately show ?case by blast
  qed
next
  assume "?Q M N"
  then obtain X Y Z where "M  multisets A" and "N  multisets A"
    and "X  {#}" and N: "N = Z + X" and M: "M = Z + Y"
    and *: "y. y ∈# Y  (x. x ∈# X  P y x)" by blast
  with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto
  moreover from N  multisets A have "Z  multisets A" by (auto simp: N)
  ultimately show "?P M N" unfolding M N by (metis mulex_on_union)
qed

end

Theory Wqo_Multiset

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Multiset Extension Preserves Well-Quasi-Orders›

theory Wqo_Multiset
imports
  Multiset_Extension
  Well_Quasi_Orders
begin

lemma list_emb_imp_reflclp_mulex_on:
  assumes "xs  lists A" and "ys  lists A"
    and "list_emb P xs ys"
  shows "(mulex_on P A)== (mset xs) (mset ys)"
using assms(3, 1, 2)
proof (induct)
  case (list_emb_Nil ys)
  then show ?case
    by (cases ys) (auto intro!: empty_mulex_on simp: multisets_def)
next
  case (list_emb_Cons xs ys y)
  then show ?case by (auto intro!: mulex_on_self_add_singleton_right simp: multisets_def)
next
  case (list_emb_Cons2 x y xs ys)
  then show ?case
    by (force intro: union_mulex_on_mono mulex_on_add_mset
             mulex_on_add_mset' mulex_on_add_mset_mono
             simp: multisets_def)
qed

text ‹The (reflexive closure of the) multiset extension of an almost-full relation
is almost-full.›
lemma almost_full_on_multisets:
  assumes "almost_full_on P A"
  shows "almost_full_on (mulex_on P A)== (multisets A)"
proof -
  let ?P = "(mulex_on P A)=="
  from almost_full_on_hom [OF _ almost_full_on_lists, of A P ?P mset,
    OF list_emb_imp_reflclp_mulex_on, simplified]
    show ?thesis using assms by blast
qed

lemma wqo_on_multisets:
  assumes "wqo_on P A"
  shows "wqo_on (mulex_on P A)== (multisets A)"
proof
  from transp_on_mulex_on [of P A "multisets A"]
    show "transp_on (mulex_on P A)== (multisets A)"
    unfolding transp_on_def by blast
next
  from almost_full_on_multisets [OF assms [THEN wqo_on_imp_almost_full_on]]
    show "almost_full_on (mulex_on P A)== (multisets A)" .
qed

end