Theory Well_Quasi_Orders.Almost_Full_Relations
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
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