(* Title: Well-Quasi-Orders Author: Christian Sternagel <c.sternagel@gmail.com> Maintainer: Christian Sternagel License: LGPL *) section ‹A Proof of Higman's Lemma via Open Induction› theory Higman_OI imports Open_Induction.Open_Induction Minimal_Elements Almost_Full begin subsection ‹Some facts about the suffix relation› lemma wfp_on_strict_suffix: "wfp_on strict_suffix A" by (rule wfp_on_mono [OF subset_refl, of _ _ "measure_on length A"]) (auto simp: strict_suffix_def suffix_def) lemma po_on_strict_suffix: "po_on strict_suffix A" by (force simp: strict_suffix_def po_on_def transp_on_def irreflp_on_def) subsection ‹Lexicographic Order on Infinite Sequences› lemma antisymp_on_LEX: assumes "irreflp_on A P" and "antisymp_on A P" shows "antisymp_on (SEQ A) (LEX P)" proof (rule antisymp_onI) fix f g assume SEQ: "f ∈ SEQ A" "g ∈ SEQ A" and "LEX P f g" and "LEX P g f" then obtain i j where "P (f i) (g i)" and "P (g j) (f j)" and "∀k<i. f k = g k" and "∀k<j. g k = f k" by (auto simp: LEX_def) then have "P (f (min i j)) (f (min i j))" using assms(2) and SEQ by (cases "i = j") (auto simp: antisymp_on_def min_def, force) with assms(1) and SEQ show "f = g" by (auto simp: irreflp_on_def) qed lemma LEX_trans: assumes "transp_on A P" and "f ∈ SEQ A" and "g ∈ SEQ A" and "h ∈ SEQ A" and "LEX P f g" and "LEX P g h" shows "LEX P f h" using assms by (auto simp: LEX_def transp_on_def) (metis less_trans linorder_neqE_nat) lemma qo_on_LEXEQ: "transp_on A P ⟹ qo_on (LEXEQ P) (SEQ A)" by (auto simp: qo_on_def reflp_on_def transp_on_def [of _ "LEXEQ P"] dest: LEX_trans) context minimal_element begin lemma glb_LEX_lexmin: assumes "chain_on (LEX P) C (SEQ A)" and "C ≠ {}" shows "glb (LEX P) C (lexmin C)" proof have "C ⊆ SEQ A" using assms by (auto simp: chain_on_def) then have "lexmin C ∈ SEQ A" using ‹C ≠ {}› by (intro lexmin_SEQ_mem) note * = ‹C ⊆ SEQ A› ‹C ≠ {}› note lex = LEX_imp_less [folded irreflp_on_def, OF po [THEN po_on_imp_irreflp_on]] ― ‹‹lexmin C› is a lower bound› show "lb (LEX P) C (lexmin C)" proof fix f assume "f ∈ C" then show "LEXEQ P (lexmin C) f" proof (cases "f = lexmin C") define i where "i = (LEAST i. f i ≠ lexmin C i)" case False then have neq: "∃i. f i ≠ lexmin C i" by blast from LeastI_ex [OF this, folded i_def] and not_less_Least [where P = "λi. f i ≠ lexmin C i", folded i_def] have neq: "f i ≠ lexmin C i" and eq: "∀j<i. f j = lexmin C j" by auto then have **: "f ∈ eq_upto C (lexmin C) i" "f i ∈ ith (eq_upto C (lexmin C) i) i" using ‹f ∈ C› by force+ moreover from ** have "¬ P (f i) (lexmin C i)" using lexmin_minimal [OF *, of "f i" i] and ‹f ∈ C› and ‹C ⊆ SEQ A› by blast moreover obtain g where "g ∈ eq_upto C (lexmin C) (Suc i)" using eq_upto_lexmin_non_empty [OF *] by blast ultimately have "P (lexmin C i) (f i)" using neq and ‹C ⊆ SEQ A› and assms(1) and lex [of g f i] and lex [of f g i] by (auto simp: eq_upto_def chain_on_def) with eq show ?thesis by (auto simp: LEX_def) qed simp qed ― ‹‹lexmin C› is greater than or equal to any other lower bound› fix f assume lb: "lb (LEX P) C f" then show "LEXEQ P f (lexmin C)" proof (cases "f = lexmin C") define i where "i = (LEAST i. f i ≠ lexmin C i)" case False then have neq: "∃i. f i ≠ lexmin C i" by blast from LeastI_ex [OF this, folded i_def] and not_less_Least [where P = "λi. f i ≠ lexmin C i", folded i_def] have neq: "f i ≠ lexmin C i" and eq: "∀j<i. f j = lexmin C j" by auto obtain h where "h ∈ eq_upto C (lexmin C) (Suc i)" and "h ∈ C" using eq_upto_lexmin_non_empty [OF *] by (auto simp: eq_upto_def) then have [simp]: "⋀j. j < Suc i ⟹ h j = lexmin C j" by auto with lb and ‹h ∈ C› have "LEX P f h" using neq by (auto simp: lb_def) then have "P (f i) (h i)" using neq and eq and ‹C ⊆ SEQ A› and ‹h ∈ C› by (intro lex) auto with eq show ?thesis by (auto simp: LEX_def) qed simp qed lemma dc_on_LEXEQ: "dc_on (LEXEQ P) (SEQ A)" proof fix C assume "chain_on (LEXEQ P) C (SEQ A)" and "C ≠ {}" then have chain: "chain_on (LEX P) C (SEQ A)" by (auto simp: chain_on_def) then have "C ⊆ SEQ A" by (auto simp: chain_on_def) then have "lexmin C ∈ SEQ A" using ‹C ≠ {}› by (intro lexmin_SEQ_mem) have "glb (LEX P) C (lexmin C)" by (rule glb_LEX_lexmin [OF chain ‹C ≠ {}›]) then have "glb (LEXEQ P) C (lexmin C)" by (auto simp: glb_def lb_def) with ‹lexmin C ∈ SEQ A› show "∃f ∈ SEQ A. glb (LEXEQ P) C f" by blast qed end text ‹ Properties that only depend on finite initial segments of a sequence (i.e., which are open with respect to the product topology). › definition "pt_open_on Q A ⟷ (∀f∈A. Q f ⟷ (∃n. (∀g∈A. (∀i<n. g i = f i) ⟶ Q g)))" lemma pt_open_onD: "pt_open_on Q A ⟹ Q f ⟹ f ∈ A ⟹ (∃n. (∀g∈A. (∀i<n. g i = f i) ⟶ Q g))" unfolding pt_open_on_def by blast lemma pt_open_on_good: "pt_open_on (good Q) (SEQ A)" proof (unfold pt_open_on_def, intro ballI) fix f assume f: "f ∈ SEQ A" show "good Q f = (∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g)" proof assume "good Q f" then obtain i and j where *: "i < j" "Q (f i) (f j)" by auto have "∀g∈SEQ A. (∀i<Suc j. g i = f i) ⟶ good Q g" proof (intro ballI impI) fix g assume "g ∈ SEQ A" and "∀i<Suc j. g i = f i" then show "good Q g" using * by (force simp: good_def) qed then show "∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g" .. next assume "∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g" with f show "good Q f" by blast qed qed context minimal_element begin lemma pt_open_on_imp_open_on_LEXEQ: assumes "pt_open_on Q (SEQ A)" shows "open_on (LEXEQ P) Q (SEQ A)" proof fix C assume chain: "chain_on (LEXEQ P) C (SEQ A)" and ne: "C ≠ {}" and "∃g∈SEQ A. glb (LEXEQ P) C g ∧ Q g" then obtain g where g: "g ∈ SEQ A" and "glb (LEXEQ P) C g" and Q: "Q g" by blast then have glb: "glb (LEX P) C g" by (auto simp: glb_def lb_def) from chain have "chain_on (LEX P) C (SEQ A)" and C: "C ⊆ SEQ A" by (auto simp: chain_on_def) note * = glb_LEX_lexmin [OF this(1) ne] have "lexmin C ∈ SEQ A" using ne and C by (intro lexmin_SEQ_mem) from glb_unique [OF _ g this glb *] and antisymp_on_LEX [OF po_on_imp_irreflp_on [OF po] po_on_imp_antisymp_on [OF po]] have [simp]: "lexmin C = g" by auto from assms [THEN pt_open_onD, OF Q g] obtain n :: nat where **: "⋀h. h ∈ SEQ A ⟹ (∀i<n. h i = g i) ⟶ Q h" by blast from eq_upto_lexmin_non_empty [OF C ne, of n] obtain f where "f ∈ eq_upto C g n" by auto then have "f ∈ C" and "Q f" using ** [of f] and C by force+ then show "∃f∈C. Q f" by blast qed lemma open_on_good: "open_on (LEXEQ P) (good Q) (SEQ A)" by (intro pt_open_on_imp_open_on_LEXEQ pt_open_on_good) end lemma open_on_LEXEQ_imp_pt_open_on_counterexample: fixes a b :: "'a" defines "A ≡ {a, b}" and "P ≡ (λx y. False)" and "Q ≡ (λf. ∀i. f i = b)" assumes [simp]: "a ≠ b" shows "minimal_element P A" and "open_on (LEXEQ P) Q (SEQ A)" and "¬ pt_open_on Q (SEQ A)" proof - show "minimal_element P A" by standard (auto simp: P_def po_on_def irreflp_on_def transp_on_def wfp_on_def) show "open_on (LEXEQ P) Q (SEQ A)" by (auto simp: P_def open_on_def chain_on_def SEQ_def glb_def lb_def LEX_def) show "¬ pt_open_on Q (SEQ A)" proof define f :: "nat ⇒ 'a" where "f ≡ (λx. b)" have "f ∈ SEQ A" by (auto simp: A_def f_def) moreover assume "pt_open_on Q (SEQ A)" ultimately have "Q f ⟷ (∃n. (∀g∈SEQ A. (∀i<n. g i = f i) ⟶ Q g))" unfolding pt_open_on_def by blast moreover have "Q f" by (auto simp: Q_def f_def) moreover have "∃g∈SEQ A. (∀i<n. g i = f i) ∧ ¬ Q g" for n by (intro bexI [of _ "f(n := a)"]) (auto simp: f_def Q_def A_def) ultimately show False by blast qed qed lemma higman: assumes "almost_full_on P A" shows "almost_full_on (list_emb P) (lists A)" proof interpret minimal_element strict_suffix "lists A" by (unfold_locales) (intro po_on_strict_suffix wfp_on_strict_suffix)+ fix f presume "f ∈ SEQ (lists A)" with qo_on_LEXEQ [OF po_on_imp_transp_on [OF po_on_strict_suffix]] and dc_on_LEXEQ and open_on_good show "good (list_emb P) f" proof (induct rule: open_induct_on) case (less f) define h where "h i = hd (f i)" for i show ?case proof (cases "∃i. f i = []") case False then have ne: "∀i. f i ≠ []" by auto with ‹f ∈ SEQ (lists A)› have "∀i. h i ∈ A" by (auto simp: h_def ne_lists) from almost_full_on_imp_homogeneous_subseq [OF assms this] obtain φ :: "nat ⇒ nat" where mono: "⋀i j. i < j ⟹ φ i < φ j" and P: "⋀i j. i < j ⟹ P (h (φ i)) (h (φ j))" by blast define f' where "f' i = (if i < φ 0 then f i else tl (f (φ (i - φ 0))))" for i have f': "f' ∈ SEQ (lists A)" using ne and ‹f ∈ SEQ (lists A)› by (auto simp: f'_def dest: list.set_sel) have [simp]: "⋀i. φ 0 ≤ i ⟹ h (φ (i - φ 0)) # f' i = f (φ (i - φ 0))" "⋀i. i < φ 0 ⟹ f' i = f i" using ne by (auto simp: f'_def h_def) moreover have "strict_suffix (f' (φ 0)) (f (φ 0))" using ne by (auto simp: f'_def) ultimately have "LEX strict_suffix f' f" by (auto simp: LEX_def) with LEX_imp_not_LEX [OF this] have "strict (LEXEQ strict_suffix) f' f" using po_on_strict_suffix [of UNIV] unfolding po_on_def irreflp_on_def transp_on_def by blast from less(2) [OF f' this] have "good (list_emb P) f'" . then obtain i j where "i < j" and emb: "list_emb P (f' i) (f' j)" by (auto simp: good_def) consider "j < φ 0" | "φ 0 ≤ i" | "i < φ 0" and "φ 0 ≤ j" by arith then show ?thesis proof (cases) case 1 with ‹i < j› and emb show ?thesis by (auto simp: good_def) next case 2 with ‹i < j› and P have "P (h (φ (i - φ 0))) (h (φ (j - φ 0)))" by auto with emb have "list_emb P (h (φ (i - φ 0)) # f' i) (h (φ (j - φ 0)) # f' j)" by auto then have "list_emb P (f (φ (i - φ 0))) (f (φ (j - φ 0)))" using 2 and ‹i < j› by auto moreover with 2 and ‹i <j› have "φ (i - φ 0) < φ (j - φ 0)" using mono by auto ultimately show ?thesis by (auto simp: good_def) next case 3 with emb have "list_emb P (f i) (f' j)" by auto moreover have "f (φ (j - φ 0)) = h (φ (j - φ 0)) # f' j" using 3 by auto ultimately have "list_emb P (f i) (f (φ (j - φ 0)))" by auto moreover have "i < φ (j - φ 0)" using mono [of 0 "j - φ 0"] and 3 by force ultimately show ?thesis by (auto simp: good_def) qed qed auto qed qed blast end