Theory Higman_OI

(*  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