Theory Almost_Full

(*  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:
  "(iSuc j. P i)  P 0  (ij. 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)  (xA. ¬ 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  (in. P (F A P i) y)  (jn. 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 "xUNIV. yUNIV. 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 *: "xI. yI. 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: "xA. yA. 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. (xA. yA. 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 "xA. yA. 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