(* Title: Well-Quasi-Orders Author: Christian Sternagel <c.sternagel@gmail.com> Maintainer: Christian Sternagel License: LGPL *) 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 (*TODO: move*) 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