Theory Kruskal

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <>
    Maintainer: Christian Sternagel
    License:    LGPL

section ‹Kruskal's Tree Theorem›

theory Kruskal
imports Well_Quasi_Orders

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"

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

inductive emb for P
  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'"
      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 }
      { 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 }
      { 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
    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)
    ultimately show False using min by blast
  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

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

  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)
  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)
    case list_emb
    then show ?thesis using IH by (auto intro: emb.intros dest: trans list_emb_trans_right)

lemma transp_on_emb:
  assumes "transp_on F P"
  shows "transp_on trees (emb P)"
  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)