# Theory Almost_Full_Relations

```(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Almost-Full Relations›

theory Almost_Full_Relations
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)
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⇩⊥"

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)
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"
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"
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"
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
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

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)
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
```