Theory Well_Quasi_Orders.Almost_Full
section ‹The Almost-Full Property›
theory Almost_Full
imports
"HOL-Library.Sublist"
"HOL-Library.Ramsey"
"Regular-Sets.Regexp_Method"
"Abstract-Rewriting.Seq"
Least_Enum
Infinite_Sequences
Open_Induction.Restricted_Predicates
begin
lemma le_Suc_eq':
"x ≤ Suc y ⟷ x = 0 ∨ (∃x'. x = Suc x' ∧ x' ≤ y)"
by (cases x) auto
lemma ex_leq_Suc:
"(∃i≤Suc j. P i) ⟷ P 0 ∨ (∃i≤j. P (Suc i))"
by (auto simp: le_Suc_eq')
lemma ex_less_Suc:
"(∃i<Suc j. P i) ⟷ P 0 ∨ (∃i<j. P (Suc i))"
by (auto simp: less_Suc_eq_0_disj)
subsection ‹Basic Definitions and Facts›
text ‹
An infinite sequence is \emph{good} whenever there are indices @{term "i < j"} such that
@{term "P (f i) (f j)"}.
›
definition good :: "('a ⇒ 'a ⇒ bool) ⇒ (nat ⇒ 'a) ⇒ bool"
where
"good P f ⟷ (∃i j. i < j ∧ P (f i) (f j))"
text ‹A sequence that is not good is called \emph{bad}.›
abbreviation "bad P f ≡ ¬ good P f"
lemma goodI:
"⟦i < j; P (f i) (f j)⟧ ⟹ good P f"
by (auto simp: good_def)
lemma goodE [elim]:
"good P f ⟹ (⋀i j. ⟦i < j; P (f i) (f j)⟧ ⟹ Q) ⟹ Q"
by (auto simp: good_def)
lemma badE [elim]:
"bad P f ⟹ ((⋀i j. i < j ⟹ ¬ P (f i) (f j)) ⟹ Q) ⟹ Q"
by (auto simp: good_def)
definition almost_full_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
"almost_full_on P A ⟷ (∀f ∈ SEQ A. good P f)"
lemma almost_full_onI [Pure.intro]:
"(⋀f. ∀i. f i ∈ A ⟹ good P f) ⟹ almost_full_on P A"
unfolding almost_full_on_def by blast
lemma almost_full_onD:
fixes f :: "nat ⇒ 'a" and A :: "'a set"
assumes "almost_full_on P A" and "⋀i. f i ∈ A"
obtains i j where "i < j" and "P (f i) (f j)"
using assms unfolding almost_full_on_def by blast
subsection ‹An equivalent inductive definition›
inductive af for A
where
now: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x y) ⟹ af A P"
| later: "(⋀x. x ∈ A ⟹ af A (λy z. P y z ∨ P x y)) ⟹ af A P"
lemma af_imp_almost_full_on:
assumes "af A P"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a" assume "∀i. f i ∈ A"
with assms obtain i and j where "i < j" and "P (f i) (f j)"
proof (induct arbitrary: f thesis)
case (later P)
define g where [simp]: "g i = f (Suc i)" for i
have "f 0 ∈ A" and "∀i. g i ∈ A" using later by auto
then obtain i and j where "i < j" and "P (g i) (g j) ∨ P (f 0) (g i)" using later by blast
then consider "P (g i) (g j)" | "P (f 0) (g i)" by blast
then show ?case using ‹i < j› by (cases) (auto intro: later)
qed blast
then show "good P f" by (auto simp: good_def)
qed
lemma af_mono:
assumes "af A P"
and "∀x y. x ∈ A ∧ y ∈ A ∧ P x y ⟶ Q x y"
shows "af A Q"
using assms
proof (induct arbitrary: Q)
case (now P)
then have "⋀x y. x ∈ A ⟹ y ∈ A ⟹ Q x y" by blast
then show ?case by (rule af.now)
next
case (later P)
show ?case
proof (intro af.later [of A Q])
fix x assume "x ∈ A"
then show "af A (λy z. Q y z ∨ Q x y)"
using later(3) by (intro later(2) [of x]) auto
qed
qed
lemma accessible_on_imp_af:
assumes "accessible_on P A x"
shows "af A (λu v. ¬ P v u ∨ ¬ P u x)"
using assms
proof (induct)
case (1 x)
then have "af A (λu v. (¬ P v u ∨ ¬ P u x) ∨ ¬ P u y ∨ ¬ P y x)" if "y ∈ A" for y
using that by (cases "P y x") (auto intro: af.now af_mono)
then show ?case by (rule af.later)
qed
lemma wfp_on_imp_af:
assumes "wfp_on P A"
shows "af A (λx y. ¬ P y x)"
using assms by (auto simp: wfp_on_accessible_on_iff intro: accessible_on_imp_af af.later)
lemma af_leq:
"af UNIV ((≤) :: nat ⇒ nat ⇒ bool)"
using wf_less [folded wfP_def wfp_on_UNIV, THEN wfp_on_imp_af] by (simp add: not_less)
definition "NOTAF A P = (SOME x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y))"
lemma not_af:
"¬ af A P ⟹ (∃x y. x ∈ A ∧ y ∈ A ∧ ¬ P x y) ∧ (∃x∈A. ¬ af A (λy z. P y z ∨ P x y))"
unfolding af.simps [of A P] by blast
fun F
where
"F A P 0 = NOTAF A P"
| "F A P (Suc i) = (let x = NOTAF A P in F A (λy z. P y z ∨ P x y) i)"
lemma almost_full_on_imp_af:
assumes af: "almost_full_on P A"
shows "af A P"
proof (rule ccontr)
assume "¬ af A P"
then have *: "F A P n ∈ A ∧
¬ af A (λy z. P y z ∨ (∃i≤n. P (F A P i) y) ∨ (∃j≤n. ∃i. i < j ∧ P (F A P i) (F A P j)))" for n
proof (induct n arbitrary: P)
case 0
from ‹¬ af A P› have "∃x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y)" by (auto intro: af.intros)
then have "NOTAF A P ∈ A ∧ ¬ af A (λy z. P y z ∨ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
with 0 show ?case by simp
next
case (Suc n)
from ‹¬ af A P› have "∃x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y)" by (auto intro: af.intros)
then have "NOTAF A P ∈ A ∧ ¬ af A (λy z. P y z ∨ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
from Suc(1) [OF this [THEN conjunct2]]
show ?case
by (fastforce simp: ex_leq_Suc ex_less_Suc elim!: back_subst [where P = "λx. ¬ af A x"])
qed
then have "F A P ∈ SEQ A" by auto
from af [unfolded almost_full_on_def, THEN bspec, OF this] and not_af [OF * [THEN conjunct2]]
show False unfolding good_def by blast
qed
hide_const NOTAF F
lemma almost_full_on_UNIV:
"almost_full_on (λ_ _. True) UNIV"
by (auto simp: almost_full_on_def good_def)
lemma almost_full_on_imp_reflp_on:
assumes "almost_full_on P A"
shows "reflp_on A P"
using assms by (auto simp: almost_full_on_def reflp_on_def)
lemma almost_full_on_subset:
"A ⊆ B ⟹ almost_full_on P B ⟹ almost_full_on P A"
by (auto simp: almost_full_on_def)
lemma almost_full_on_mono:
assumes "A ⊆ B" and "⋀x y. Q x y ⟹ P x y"
and "almost_full_on Q B"
shows "almost_full_on P A"
using assms by (metis almost_full_on_def almost_full_on_subset good_def)
text ‹
Every sequence over elements of an almost-full set has a homogeneous subsequence.
›
lemma almost_full_on_imp_homogeneous_subseq:
assumes "almost_full_on P A"
and "∀i::nat. f i ∈ A"
shows "∃φ::nat ⇒ nat. ∀i j. i < j ⟶ φ i < φ j ∧ P (f (φ i)) (f (φ j))"
proof -
define X where "X = {{i, j} | i j::nat. i < j ∧ P (f i) (f j)}"
define Y where "Y = - X"
define h where "h = (λZ. if Z ∈ X then 0 else Suc 0)"
have [iff]: "⋀x y. h {x, y} = 0 ⟷ {x, y} ∈ X" by (auto simp: h_def)
have [iff]: "⋀x y. h {x, y} = Suc 0 ⟷ {x, y} ∈ Y" by (auto simp: h_def Y_def)
have "∀x∈UNIV. ∀y∈UNIV. x ≠ y ⟶ h {x, y} < 2" by (simp add: h_def)
from Ramsey2 [OF infinite_UNIV_nat this] obtain I c
where "infinite I" and "c < 2"
and *: "∀x∈I. ∀y∈I. x ≠ y ⟶ h {x, y} = c" by blast
then interpret infinitely_many1 "λi. i ∈ I"
by (unfold_locales) (simp add: infinite_nat_iff_unbounded)
have "c = 0 ∨ c = 1" using ‹c < 2› by arith
then show ?thesis
proof
assume [simp]: "c = 0"
have "∀i j. i < j ⟶ P (f (enum i)) (f (enum j))"
proof (intro allI impI)
fix i j :: nat
assume "i < j"
from * and enum_P and enum_less [OF ‹i < j›] have "{enum i, enum j} ∈ X" by auto
with enum_less [OF ‹i < j›]
show "P (f (enum i)) (f (enum j))" by (auto simp: X_def doubleton_eq_iff)
qed
then show ?thesis using enum_less by blast
next
assume [simp]: "c = 1"
have "∀i j. i < j ⟶ ¬ P (f (enum i)) (f (enum j))"
proof (intro allI impI)
fix i j :: nat
assume "i < j"
from * and enum_P and enum_less [OF ‹i < j›] have "{enum i, enum j} ∈ Y" by auto
with enum_less [OF ‹i < j›]
show "¬ P (f (enum i)) (f (enum j))" by (auto simp: Y_def X_def doubleton_eq_iff)
qed
then have "¬ good P (f ∘ enum)" by auto
moreover have "∀i. f (enum i) ∈ A" using assms by auto
ultimately show ?thesis using ‹almost_full_on P A› by (simp add: almost_full_on_def)
qed
qed
text ‹
Almost full relations do not admit infinite antichains.
›
lemma almost_full_on_imp_no_antichain_on:
assumes "almost_full_on P A"
shows "¬ antichain_on P f A"
proof
assume *: "antichain_on P f A"
then have "∀i. f i ∈ A" by simp
with assms have "good P f" by (auto simp: almost_full_on_def)
then obtain i j where "i < j" and "P (f i) (f j)"
unfolding good_def by auto
moreover with * have "incomparable P (f i) (f j)" by auto
ultimately show False by blast
qed
text ‹
If the image of a function is almost-full then also its preimage is almost-full.
›
lemma almost_full_on_map:
assumes "almost_full_on Q B"
and "h ` A ⊆ B"
shows "almost_full_on (λx y. Q (h x) (h y)) A" (is "almost_full_on ?P A")
proof
fix f
assume "∀i::nat. f i ∈ A"
then have "⋀i. h (f i) ∈ B" using ‹h ` A ⊆ B› by auto
with ‹almost_full_on Q B› [unfolded almost_full_on_def, THEN bspec, of "h ∘ f"]
show "good ?P f" unfolding good_def comp_def by blast
qed
text ‹
The homomorphic image of an almost-full set is almost-full.
›
lemma almost_full_on_hom:
fixes h :: "'a ⇒ 'b"
assumes hom: "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q (h x) (h y)"
and af: "almost_full_on P A"
shows "almost_full_on Q (h ` A)"
proof
fix f :: "nat ⇒ 'b"
assume "∀i. f i ∈ h ` A"
then have "∀i. ∃x. x ∈ A ∧ f i = h x" by (auto simp: image_def)
from choice [OF this] obtain g
where *: "∀i. g i ∈ A ∧ f i = h (g i)" by blast
show "good Q f"
proof (rule ccontr)
assume bad: "bad Q f"
{ fix i j :: nat
assume "i < j"
from bad have "¬ Q (f i) (f j)" using ‹i < j› by (auto simp: good_def)
with hom have "¬ P (g i) (g j)" using * by auto }
then have "bad P g" by (auto simp: good_def)
with af and * show False by (auto simp: good_def almost_full_on_def)
qed
qed
text ‹
The monomorphic preimage of an almost-full set is almost-full.
›
lemma almost_full_on_mon:
assumes mon: "⋀x y. ⟦x ∈ A; y ∈ A⟧ ⟹ P x y = Q (h x) (h y)" "bij_betw h A B"
and af: "almost_full_on Q B"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a"
assume *: "∀i. f i ∈ A"
then have **: "∀i. (h ∘ f) i ∈ B" using mon by (auto simp: bij_betw_def)
show "good P f"
proof (rule ccontr)
assume bad: "bad P f"
{ fix i j :: nat
assume "i < j"
from bad have "¬ P (f i) (f j)" using ‹i < j› by (auto simp: good_def)
with mon have "¬ Q (h (f i)) (h (f j))"
using * by (auto simp: bij_betw_def inj_on_def) }
then have "bad Q (h ∘ f)" by (auto simp: good_def)
with af and ** show False by (auto simp: good_def almost_full_on_def)
qed
qed
text ‹
Every total and well-founded relation is almost-full.
›
lemma total_on_and_wfp_on_imp_almost_full_on:
assumes "totalp_on A P" and "wfp_on P A"
shows "almost_full_on P⇧=⇧= A"
proof (rule ccontr)
assume "¬ almost_full_on P⇧=⇧= A"
then obtain f :: "nat ⇒ 'a" where *: "⋀i. f i ∈ A"
and "∀i j. i < j ⟶ ¬ P⇧=⇧= (f i) (f j)"
unfolding almost_full_on_def by (auto dest: badE)
with ‹totalp_on A P› have "∀i j. i < j ⟶ P (f j) (f i)"
unfolding totalp_on_def by blast
then have "⋀i. P (f (Suc i)) (f i)" by auto
with ‹wfp_on P A› and * show False
unfolding wfp_on_def by blast
qed
lemma Nil_imp_good_list_emb [simp]:
assumes "f i = []"
shows "good (list_emb P) f"
proof (rule ccontr)
assume "bad (list_emb P) f"
moreover have "(list_emb P) (f i) (f (Suc i))"
unfolding assms by auto
ultimately show False
unfolding good_def by auto
qed
lemma ne_lists:
assumes "xs ≠ []" and "xs ∈ lists A"
shows "hd xs ∈ A" and "tl xs ∈ lists A"
using assms by (case_tac [!] xs) simp_all
lemma list_emb_eq_length_induct [consumes 2, case_names Nil Cons]:
assumes "length xs = length ys"
and "list_emb P xs ys"
and "Q [] []"
and "⋀x y xs ys. ⟦P x y; list_emb P xs ys; Q xs ys⟧ ⟹ Q (x#xs) (y#ys)"
shows "Q xs ys"
using assms(2, 1, 3-) by (induct) (auto dest: list_emb_length)
lemma list_emb_eq_length_P:
assumes "length xs = length ys"
and "list_emb P xs ys"
shows "∀i<length xs. P (xs ! i) (ys ! i)"
using assms
proof (induct rule: list_emb_eq_length_induct)
case (Cons x y xs ys)
show ?case
proof (intro allI impI)
fix i assume "i < length (x # xs)"
with Cons show "P ((x#xs)!i) ((y#ys)!i)"
by (cases i) simp_all
qed
qed simp
subsection ‹Special Case: Finite Sets›
text ‹
Every reflexive relation on a finite set is almost-full.
›
lemma finite_almost_full_on:
assumes finite: "finite A"
and refl: "reflp_on A P"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a"
assume *: "∀i. f i ∈ A"
let ?I = "UNIV::nat set"
have "f ` ?I ⊆ A" using * by auto
with finite and finite_subset have 1: "finite (f ` ?I)" by blast
have "infinite ?I" by auto
from pigeonhole_infinite [OF this 1]
obtain k where "infinite {j. f j = f k}" by auto
then obtain l where "k < l" and "f l = f k"
unfolding infinite_nat_iff_unbounded by auto
then have "P (f k) (f l)" using refl and * by (auto simp: reflp_on_def)
with ‹k < l› show "good P f" by (auto simp: good_def)
qed
lemma eq_almost_full_on_finite_set:
assumes "finite A"
shows "almost_full_on (=) A"
using finite_almost_full_on [OF assms, of "(=)"]
by (auto simp: reflp_on_def)
subsection ‹Further Results›
lemma af_trans_extension_imp_wf:
assumes subrel: "⋀x y. P x y ⟹ Q x y"
and af: "almost_full_on P A"
and trans: "transp_on A Q"
shows "wfp_on (strict Q) A"
proof (unfold wfp_on_def, rule notI)
assume "∃f. ∀i. f i ∈ A ∧ strict Q (f (Suc i)) (f i)"
then obtain f where *: "∀i. f i ∈ A ∧ ((strict Q)¯¯) (f i) (f (Suc i))" by blast
from chain_transp_on_less[OF this]
have "∀i j. i < j ⟶ ¬ Q (f i) (f j)" using trans using transp_on_conversep transp_on_strict by blast
with subrel have "∀i j. i < j ⟶ ¬ P (f i) (f j)" by blast
with af show False
using * by (auto simp: almost_full_on_def good_def)
qed
lemma af_trans_imp_wf:
assumes "almost_full_on P A"
and "transp_on A P"
shows "wfp_on (strict P) A"
using assms by (intro af_trans_extension_imp_wf)
lemma wf_and_no_antichain_imp_qo_extension_wf:
assumes wf: "wfp_on (strict P) A"
and anti: "¬ (∃f. antichain_on P f A)"
and subrel: "∀x∈A. ∀y∈A. P x y ⟶ Q x y"
and qo: "qo_on Q A"
shows "wfp_on (strict Q) A"
proof (rule ccontr)
have "transp_on A (strict Q)"
using qo unfolding qo_on_def transp_on_def by blast
then have *: "transp_on A ((strict Q)¯¯)" by simp
assume "¬ wfp_on (strict Q) A"
then obtain f :: "nat ⇒ 'a" where A: "⋀i. f i ∈ A"
and "∀i. strict Q (f (Suc i)) (f i)" unfolding wfp_on_def by blast+
then have "∀i. f i ∈ A ∧ ((strict Q)¯¯) (f i) (f (Suc i))" by auto
from chain_transp_on_less [OF this *]
have *: "⋀i j. i < j ⟹ ¬ P (f i) (f j)"
using subrel and A by blast
show False
proof (cases)
assume "∃k. ∀i>k. ∃j>i. P (f j) (f i)"
then obtain k where "∀i>k. ∃j>i. P (f j) (f i)" by auto
from subchain [of k _ f, OF this] obtain g
where "⋀i j. i < j ⟹ g i < g j"
and "⋀i. P (f (g (Suc i))) (f (g i))" by auto
with * have "⋀i. strict P (f (g (Suc i))) (f (g i))" by blast
with wf [unfolded wfp_on_def not_ex, THEN spec, of "λi. f (g i)"] and A
show False by fast
next
assume "¬ (∃k. ∀i>k. ∃j>i. P (f j) (f i))"
then have "∀k. ∃i>k. ∀j>i. ¬ P (f j) (f i)" by auto
from choice [OF this] obtain h
where "∀k. h k > k"
and **: "∀k. (∀j>h k. ¬ P (f j) (f (h k)))" by auto
define φ where [simp]: "φ = (λi. (h ^^ Suc i) 0)"
have "⋀i. φ i < φ (Suc i)"
using ‹∀k. h k > k› by (induct_tac i) auto
then have mono: "⋀i j. i < j ⟹ φ i < φ j" by (metis lift_Suc_mono_less)
then have "∀i j. i < j ⟶ ¬ P (f (φ j)) (f (φ i))"
using ** by auto
with mono [THEN *]
have "∀i j. i < j ⟶ incomparable P (f (φ j)) (f (φ i))" by blast
moreover have "∃i j. i < j ∧ ¬ incomparable P (f (φ i)) (f (φ j))"
using anti [unfolded not_ex, THEN spec, of "λi. f (φ i)"] and A by blast
ultimately show False by blast
qed
qed
lemma every_qo_extension_wf_imp_af:
assumes ext: "∀Q. (∀x∈A. ∀y∈A. P x y ⟶ Q x y) ∧
qo_on Q A ⟶ wfp_on (strict Q) A"
and "qo_on P A"
shows "almost_full_on P A"
proof
from ‹qo_on P A›
have refl: "reflp_on A P"
and trans: "transp_on A P"
by (auto intro: qo_on_imp_reflp_on qo_on_imp_transp_on)
fix f :: "nat ⇒ 'a"
assume "∀i. f i ∈ A"
then have A: "⋀i. f i ∈ A" ..
show "good P f"
proof (rule ccontr)
assume "¬ ?thesis"
then have bad: "∀i j. i < j ⟶ ¬ P (f i) (f j)" by (auto simp: good_def)
then have *: "⋀i j. P (f i) (f j) ⟹ i ≥ j" by (metis not_le_imp_less)
define D where [simp]: "D = (λx y. ∃i. x = f (Suc i) ∧ y = f i)"
define P' where "P' = restrict_to P A"
define Q where [simp]: "Q = (sup P' D)⇧*⇧*"
have **: "⋀i j. (D OO P'⇧*⇧*)⇧+⇧+ (f i) (f j) ⟹ i > j"
proof -
fix i j
assume "(D OO P'⇧*⇧*)⇧+⇧+ (f i) (f j)"
then show "i > j"
apply (induct "f i" "f j" arbitrary: j)
apply (insert A, auto dest!: * simp: P'_def reflp_on_restrict_to_rtranclp [OF refl trans])
apply (metis "*" dual_order.strict_trans1 less_Suc_eq_le refl reflp_on_def)
by (metis le_imp_less_Suc less_trans)
qed
have "∀x∈A. ∀y∈A. P x y ⟶ Q x y" by (auto simp: P'_def)
moreover have "qo_on Q A" by (auto simp: qo_on_def reflp_on_def transp_on_def)
ultimately have "wfp_on (strict Q) A"
using ext [THEN spec, of Q] by blast
moreover have "∀i. f i ∈ A ∧ strict Q (f (Suc i)) (f i)"
proof
fix i
have "¬ Q (f i) (f (Suc i))"
proof
assume "Q (f i) (f (Suc i))"
then have "(sup P' D)⇧*⇧* (f i) (f (Suc i))" by auto
moreover have "(sup P' D)⇧*⇧* = sup (P'⇧*⇧*) (P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+)"
proof -
have "⋀A B. (A ∪ B)⇧* = A⇧* ∪ A⇧* O (B O A⇧*)⇧+" by regexp
from this [to_pred] show ?thesis by blast
qed
ultimately have "sup (P'⇧*⇧*) (P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+) (f i) (f (Suc i))" by simp
then have "(P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+) (f i) (f (Suc i))" by auto
then have "Suc i < i"
using ** apply auto
by (metis (lifting, mono_tags) less_le relcompp.relcompI tranclp_into_tranclp2)
then show False by auto
qed
with A [of i] show "f i ∈ A ∧ strict Q (f (Suc i)) (f i)" by auto
qed
ultimately show False unfolding wfp_on_def by blast
qed
qed
end