Theory Kruskal
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; ∀t∈set 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 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)
end
end