(* 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; ∀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