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