# Theory Higman_OI

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

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