# Theory Well_Quasi_Orders

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

section ‹Well-Quasi-Orders›

theory Well_Quasi_Orders
imports Almost_Full_Relations
begin

subsection ‹Basic Definitions›

definition wqo_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"wqo_on P A ⟷ transp_on A P ∧ almost_full_on P A"

lemma wqo_on_UNIV:
"wqo_on (λ_ _. True) UNIV"
using almost_full_on_UNIV by (auto simp: wqo_on_def transp_on_def)

lemma wqo_onI [Pure.intro]:
"⟦transp_on A P; almost_full_on P A⟧ ⟹ wqo_on P A"
unfolding wqo_on_def almost_full_on_def by blast

lemma wqo_on_imp_reflp_on:
"wqo_on P A ⟹ reflp_on A P"
using almost_full_on_imp_reflp_on by (auto simp: wqo_on_def)

lemma wqo_on_imp_transp_on:
"wqo_on P A ⟹ transp_on A P"
by (auto simp: wqo_on_def)

lemma wqo_on_imp_almost_full_on:
"wqo_on P A ⟹ almost_full_on P A"
by (auto simp: wqo_on_def)

lemma wqo_on_imp_qo_on:
"wqo_on P A ⟹ qo_on P A"
by (metis qo_on_def wqo_on_imp_reflp_on wqo_on_imp_transp_on)

lemma wqo_on_imp_good:
"wqo_on P A ⟹ ∀i. f i ∈ A ⟹ good P f"
by (auto simp: wqo_on_def almost_full_on_def)

lemma wqo_on_subset:
"A ⊆ B ⟹ wqo_on P B ⟹ wqo_on P A"
using almost_full_on_subset [of A B P]
and transp_on_subset [of B P A]
unfolding wqo_on_def by blast

subsection ‹Equivalent Definitions›

text ‹
Given a quasi-order @{term P}, the following statements are equivalent:
\begin{enumerate}
\item @{term P} is a almost-full.
\item @{term P} does neither allow decreasing chains nor antichains.
\item Every quasi-order extending @{term P} is well-founded.
\end{enumerate}
›

lemma wqo_af_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ almost_full_on P A"
using assms by (metis qo_on_def wqo_on_def)

lemma wqo_wf_and_no_antichain_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ wfp_on (strict P) A ∧ ¬ (∃f. antichain_on P f A)"
unfolding wqo_af_conv [OF assms]
using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
and almost_full_on_imp_no_antichain_on [of P A]
and wf_and_no_antichain_imp_qo_extension_wf [of P A]
and every_qo_extension_wf_imp_af [OF _ assms]
by blast

lemma wqo_extensions_wf_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ (∀Q. (∀x∈A. ∀y∈A. P x y ⟶ Q x y) ∧ qo_on Q A ⟶ wfp_on (strict Q) A)"
unfolding wqo_af_conv [OF assms]
using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
and almost_full_on_imp_no_antichain_on [of P A]
and wf_and_no_antichain_imp_qo_extension_wf [of P A]
and every_qo_extension_wf_imp_af [OF _ assms]
by blast

lemma wqo_on_imp_wfp_on:
"wqo_on P A ⟹ wfp_on (strict P) A"
by (metis (no_types) wqo_on_imp_qo_on wqo_wf_and_no_antichain_conv)

text ‹
The homomorphic image of a wqo set is wqo.
›
lemma wqo_on_hom:
assumes "transp_on (h  A) Q"
and "∀x∈A. ∀y∈A. P x y ⟶ Q (h x) (h y)"
and "wqo_on P A"
shows "wqo_on Q (h  A)"
using assms and almost_full_on_hom [of A P Q h]
unfolding wqo_on_def by blast

text ‹
The monomorphic preimage of a wqo set is wqo.
›
lemma wqo_on_mon:
assumes *: "∀x∈A. ∀y∈A. P x y ⟷ Q (h x) (h y)"
and bij: "bij_betw h A B"
and wqo: "wqo_on Q B"
shows "wqo_on P A"
proof -
have "transp_on A P"
proof (rule transp_onI)
fix x y z assume [intro!]: "x ∈ A" "y ∈ A" "z ∈ A"
and "P x y" and "P y z"
with * have "Q (h x) (h y)" and "Q (h y) (h z)" by blast+
with wqo_on_imp_transp_on [OF wqo] have "Q (h x) (h z)"
using bij by (auto simp: bij_betw_def transp_on_def)
with * show "P x z" by blast
qed
with assms and almost_full_on_mon [of A P Q h]
show ?thesis unfolding wqo_on_def by blast
qed

subsection ‹A Type Class for Well-Quasi-Orders›

text ‹
In a well-quasi-order (wqo) every infinite sequence is good.
›
class wqo = preorder +
assumes good: "good (≤) f"

lemma wqo_on_class [simp, intro]:
"wqo_on (≤) (UNIV :: ('a :: wqo) set)"
using good by (auto simp: wqo_on_def transp_on_def almost_full_on_def dest: order_trans)

lemma wqo_on_UNIV_class_wqo [intro!]:
"wqo_on P UNIV ⟹ class.wqo P (strict P)"
by (unfold_locales) (auto simp: wqo_on_def almost_full_on_def, unfold transp_on_def, blast)

text ‹
The following lemma converts between @{const wqo_on} (for the special case that the domain is the
universe of a type) and the class predicate @{const class.wqo}.
›
lemma wqo_on_UNIV_conv:
"wqo_on P UNIV ⟷ class.wqo P (strict P)" (is "?lhs = ?rhs")
proof
assume "?lhs" then show "?rhs" by auto
next
assume "?rhs" then show "?lhs"
unfolding class.wqo_def class.preorder_def class.wqo_axioms_def
by (auto simp: wqo_on_def almost_full_on_def transp_on_def)
qed

text ‹
The strict part of a wqo is well-founded.
›
lemma (in wqo) "wfP (<)"
proof -
have "class.wqo (≤) (<)" ..
hence "wqo_on (≤) UNIV"
unfolding less_le_not_le [abs_def] wqo_on_UNIV_conv [symmetric] .
from wqo_on_imp_wfp_on [OF this]
show ?thesis unfolding less_le_not_le [abs_def] wfp_on_UNIV .
qed

lemma wqo_on_with_bot:
assumes "wqo_on P A"
shows "wqo_on (option_le P) A⇩⊥" (is "wqo_on ?P ?A")
proof -
{ from assms have trans [unfolded transp_on_def]: "transp_on A P"
by (auto simp: wqo_on_def)
have "transp_on ?A ?P"
by (auto simp: transp_on_def elim!: with_bot_cases, insert trans) blast }
moreover
{ from assms and almost_full_on_with_bot
have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_option_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on (option_le P) UNIV"
using wqo_on_with_bot [of P UNIV] by simp

text ‹
When two sets are wqo, then their disjoint sum is wqo.
›
lemma wqo_on_Plus:
assumes "wqo_on P A" and "wqo_on Q B"
shows "wqo_on (sum_le P Q) (A <+> B)" (is "wqo_on ?P ?A")
proof -
{ from assms have trans [unfolded transp_on_def]: "transp_on A P" "transp_on B Q"
by (auto simp: wqo_on_def)
have "transp_on ?A ?P"
unfolding transp_on_def by (auto, insert trans) (blast+) }
moreover
{ from assms and almost_full_on_Plus have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_sum_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on Q UNIV ⟹ wqo_on (sum_le P Q) UNIV"
using wqo_on_Plus [of P UNIV Q UNIV] by simp

subsection ‹Dickson's Lemma›

lemma wqo_on_Sigma:
fixes A1 :: "'a set" and A2 :: "'b set"
assumes "wqo_on P1 A1" and "wqo_on P2 A2"
shows "wqo_on (prod_le P1 P2) (A1 × A2)" (is "wqo_on ?P ?A")
proof -
{ from assms have "transp_on A1 P1" and "transp_on A2 P2" by (auto simp: wqo_on_def)
hence "transp_on ?A ?P" unfolding transp_on_def prod_le_def by blast }
moreover
{ from assms and almost_full_on_Sigma [of P1 A1 P2 A2]
have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemmas dickson = wqo_on_Sigma

lemma wqo_on_prod_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on Q UNIV ⟹ wqo_on (prod_le P Q) UNIV"
using wqo_on_Sigma [of P UNIV Q UNIV] by simp

subsection ‹Higman's Lemma›

lemma transp_on_list_emb:
assumes "transp_on A P"
shows "transp_on (lists A) (list_emb P)"
using assms and list_emb_trans [of _ _ _ P]
unfolding transp_on_def by blast

lemma wqo_on_lists:
assumes "wqo_on P A" shows "wqo_on (list_emb P) (lists A)"
using assms and almost_full_on_lists
and transp_on_list_emb by (auto simp: wqo_on_def)

lemmas higman = wqo_on_lists

lemma wqo_on_list_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on (list_emb P) UNIV"
using wqo_on_lists [of P UNIV] by simp

text ‹
Every reflexive and transitive relation on a finite set is a wqo.
›
lemma finite_wqo_on:
assumes "finite A" and refl: "reflp_on A P" and "transp_on A P"
shows "wqo_on P A"
using assms and finite_almost_full_on by (auto simp: wqo_on_def)

lemma finite_eq_wqo_on:
assumes "finite A"
shows "wqo_on (=) A"
using finite_wqo_on [OF assms, of "(=)"]
by (auto simp: reflp_on_def transp_on_def)

lemma wqo_on_lists_over_finite_sets:
"wqo_on (list_emb (=)) (UNIV::('a::finite) list set)"
using wqo_on_lists [OF finite_eq_wqo_on [OF finite [of "UNIV::('a::finite) set"]]] by simp

lemma wqo_on_map:
fixes P and Q and h
defines "P' ≡ λx y. P x y ∧ Q (h x) (h y)"
assumes "wqo_on P A"
and "wqo_on Q B"
and subset: "h  A ⊆ B"
shows "wqo_on P' A"
proof
let ?Q = "λx y. Q (h x) (h y)"
from ‹wqo_on P A› have "transp_on A P"
by (rule wqo_on_imp_transp_on)
then show "transp_on A P'"
using ‹wqo_on Q B› and subset
unfolding wqo_on_def transp_on_def P'_def by blast

from ‹wqo_on P A› have "almost_full_on P A"
by (rule wqo_on_imp_almost_full_on)
from ‹wqo_on Q B› have "almost_full_on Q B"
by (rule wqo_on_imp_almost_full_on)

show "almost_full_on P' A"
proof
fix f
assume *: "∀i::nat. f i ∈ A"
from almost_full_on_imp_homogeneous_subseq [OF ‹almost_full_on P A› this]
obtain g :: "nat ⇒ nat"
where g: "⋀i j. i < j ⟹ g i < g j"
and **: "∀i. f (g i) ∈ A ∧ P (f (g i)) (f (g (Suc i)))"
using * by auto
from chain_transp_on_less [OF ** ‹transp_on A P›]
have **: "⋀i j. i < j ⟹ P (f (g i)) (f (g j))" .
let ?g = "λi. h (f (g i))"
from * and subset have B: "⋀i. ?g i ∈ B" by auto
with ‹almost_full_on Q B› [unfolded almost_full_on_def good_def, THEN bspec, of ?g]
obtain i j :: nat
where "i < j" and "Q (?g i) (?g j)" by blast
with ** [OF ‹i < j›] have "P' (f (g i)) (f (g j))"
by (auto simp: P'_def)
with g [OF ‹i < j›] show "good P' f" by (auto simp: good_def)
qed
qed

lemma wqo_on_UNIV_nat:
"wqo_on (≤) (UNIV :: nat set)"
unfolding wqo_on_def transp_on_def
using almost_full_on_UNIV_nat by simp

end
`