Theory Well_Quasi_Orders.Almost_Full_Relations

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

section ‹Almost-Full Relations›

theory Almost_Full_Relations
imports Minimal_Bad_Sequences
begin

lemma (in mbs) mbs':
  assumes "¬ almost_full_on P A"
  shows "m  BAD P. g. (m, g)  gseq  good P g"
using assms and mbs unfolding almost_full_on_def by blast

(*TODO: move to Option.thy of Isabelle/HOL?*)
subsection ‹Adding a Bottom Element to a Set›

definition with_bot :: "'a set  'a option set" ("_" [1000] 1000)
where
  "A = {None}  Some ` A"

lemma with_bot_iff [iff]:
  "Some x  A  x  A"
  by (auto simp: with_bot_def)

lemma NoneI [simp, intro]:
  "None  A"
  by (simp add: with_bot_def)

lemma not_None_the_mem [simp]:
  "x  None  the x  A  x  A"
  by auto

lemma with_bot_cases:
  "u  A  (x. x  A  u = Some x  P)  (u = None  P)  P"
  by auto

lemma with_bot_empty_conv [iff]:
  "A = {None}  A = {}"
  by (auto elim: with_bot_cases)

lemma with_bot_UNIV [simp]:
  "UNIV = UNIV"
proof (rule set_eqI)
  fix x :: "'a option"
  show "x  UNIV  x  UNIV" by (cases x) auto
qed


subsection ‹Adding a Bottom Element to an Almost-Full Set›

fun
  option_le :: "('a  'a  bool)  'a option  'a option  bool"
where
  "option_le P None y = True" |
  "option_le P (Some x) None = False" |
  "option_le P (Some x) (Some y) = P x y"

lemma None_imp_good_option_le [simp]:
  assumes "f i = None"
  shows "good (option_le P) f"
  by (rule goodI [of i "Suc i"]) (auto simp: assms)

lemma almost_full_on_with_bot:
  assumes "almost_full_on P A"
  shows "almost_full_on (option_le P) A" (is "almost_full_on ?P ?A")
proof
  fix f :: "nat  'a option"
  assume *: "i. f i  ?A"
  show "good ?P f"
  proof (cases "i. f i  None")
    case True
    then have **: "i. Some (the (f i)) = f i"
      and "i. the (f i)  A" using * by auto
    with almost_full_onD [OF assms, of "the  f"] obtain i j where "i < j"
      and "P (the (f i)) (the (f j))" by auto
    then have "?P (Some (the (f i))) (Some (the (f j)))" by simp
    then have "?P (f i) (f j)" unfolding ** .
    with i < j show "good ?P f" by (auto simp: good_def)
  qed auto
qed


subsection ‹Disjoint Union of Almost-Full Sets›

fun
  sum_le :: "('a  'a  bool)  ('b  'b  bool)  'a + 'b  'a + 'b  bool"
where
  "sum_le P Q (Inl x) (Inl y) = P x y" |
  "sum_le P Q (Inr x) (Inr y) = Q x y" |
  "sum_le P Q x y = False"

lemma not_sum_le_cases:
  assumes "¬ sum_le P Q a b"
    and "x y. a = Inl x; b = Inl y; ¬ P x y  thesis"
    and "x y. a = Inr x; b = Inr y; ¬ Q x y  thesis"
    and "x y. a = Inl x; b = Inr y  thesis"
    and "x y. a = Inr x; b = Inl y  thesis"
  shows thesis
  using assms by (cases a b rule: sum.exhaust [case_product sum.exhaust]) auto

text ‹
  When two sets are almost-full, then their disjoint sum is almost-full.
›
lemma almost_full_on_Plus:
  assumes "almost_full_on P A" and "almost_full_on Q B"
  shows "almost_full_on (sum_le P Q) (A <+> B)" (is "almost_full_on ?P ?A")
proof
  fix f :: "nat  ('a + 'b)"
  let ?I = "f -` Inl ` A"
  let ?J = "f -` Inr ` B"
  assume "i. f i  ?A"
  then have *: "?J = (UNIV::nat set) - ?I" by (fastforce)
  show "good ?P f"
  proof (rule ccontr)
    assume bad: "bad ?P f"
    show False
    proof (cases "finite ?I")
      assume "finite ?I"
      then have "infinite ?J" by (auto simp: *)
      then interpret infinitely_many1 "λi. f i  Inr ` B"
        by (unfold_locales) (simp add: infinite_nat_iff_unbounded)
      have [dest]: "i x. f (enum i) = Inl x  False"
        using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
      let ?f = "λi. projr (f (enum i))"
      have B: "i. ?f i  B" using enum_P by (auto simp: image_iff) (metis sum.sel(2))
      { fix i j :: nat
        assume "i < j"
        then have "enum i < enum j" using enum_less by auto
        with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
        then have "¬ Q (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
      then have "bad Q ?f" by (auto simp: good_def)
      moreover from almost_full_on Q B and B
        have "good Q ?f" by (auto simp: good_def almost_full_on_def)
      ultimately show False by blast
    next
      assume "infinite ?I"
      then interpret infinitely_many1 "λi. f i  Inl ` A"
        by (unfold_locales) (simp add: infinite_nat_iff_unbounded)
      have [dest]: "i x. f (enum i) = Inr x  False"
        using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
      let ?f = "λi. projl (f (enum i))"
      have A: "i. ?f i  A" using enum_P by (auto simp: image_iff) (metis sum.sel(1))
      { fix i j :: nat
        assume "i < j"
        then have "enum i < enum j" using enum_less by auto
        with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
        then have "¬ P (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
      then have "bad P ?f" by (auto simp: good_def)
      moreover from almost_full_on P A and A
        have "good P ?f" by (auto simp: good_def almost_full_on_def)
      ultimately show False by blast
    qed
  qed
qed


subsection ‹Dickson's Lemma for Almost-Full Relations›

text ‹
  When two sets are almost-full, then their Cartesian product is almost-full.
›

definition
  prod_le :: "('a  'a  bool)  ('b  'b  bool)  'a × 'b  'a × 'b  bool"
where
  "prod_le P1 P2 = (λ(p1, p2) (q1, q2). P1 p1 q1  P2 p2 q2)"

lemma prod_le_True [simp]:
  "prod_le P (λ_ _. True) a b = P (fst a) (fst b)"
  by (auto simp: prod_le_def)

lemma almost_full_on_Sigma:
  assumes "almost_full_on P1 A1" and "almost_full_on P2 A2"
  shows "almost_full_on (prod_le P1 P2) (A1 × A2)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
  assume "¬ almost_full_on ?P ?A"
  then obtain f where f: "i. f i  ?A"
    and bad: "bad ?P f" by (auto simp: almost_full_on_def)
  let ?W = "λx y. P1 (fst x) (fst y)"
  let ?B = "λx y. P2 (snd x) (snd y)"
  from f have fst: "i. fst (f i)  A1" and snd: "i. snd (f i)  A2"
    by (metis SigmaE fst_conv, metis SigmaE snd_conv)
  from almost_full_on_imp_homogeneous_subseq [OF assms(1) fst]
    obtain φ :: "nat  nat" where mono: "i j. i < j  φ i < φ j"
    and *: "i j. i < j  ?W (f (φ i)) (f (φ j))" by auto
  from snd have "i. snd (f (φ i))  A2" by auto
  then have "snd  f  φ  SEQ A2" by auto
  with assms(2) have "good P2 (snd  f  φ)" by (auto simp: almost_full_on_def)
  then obtain i j :: nat
    where "i < j" and "?B (f (φ i)) (f (φ j))" by auto
  with * [OF i < j] have "?P (f (φ i)) (f (φ j))" by (simp add: case_prod_beta prod_le_def)
  with mono [OF i < j] and bad show False by auto
qed


subsection ‹Higman's Lemma for Almost-Full Relations›

lemma almost_full_on_lists:
  assumes "almost_full_on P A"
  shows "almost_full_on (list_emb P) (lists A)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
  interpret mbs ?A .
  assume "¬ ?thesis"
  from mbs' [OF this] obtain m
    where bad: "m  BAD ?P"
    and min: "g. (m, g)  gseq  good ?P g" ..
  then have lists: "i. m i  lists A"
    and ne: "i. m i  []" by auto

  define h t where "h = (λi. hd (m i))" and "t = (λi. tl (m i))"
  have m: "i. m i = h i # t i" using ne by (simp add: h_def t_def)
  
  have "i. h i  A" using ne_lists [OF ne] and lists by (auto simp add: h_def)
  from almost_full_on_imp_homogeneous_subseq [OF assms this] obtain φ :: "nat  nat"
    where less: "i j. i < j  φ i < φ j"
      and P: "i j. i < j  P (h (φ i)) (h (φ j))" by blast

  have bad_t: "bad ?P (t  φ)"
  proof
    assume "good ?P (t  φ)"
    then obtain i j where "i < j" and "?P (t (φ i)) (t (φ j))" by auto
    moreover with P have "P (h (φ i)) (h (φ j))" by blast
    ultimately have "?P (m (φ i)) (m (φ j))"
      by (subst (1 2) m) (rule list_emb_Cons2, auto)
    with less and i < j have "good ?P m" by (auto simp: good_def)
    with bad show False by blast
  qed
  
  define m' where "m' = (λi. if i < φ 0 then m i else t (φ (i - φ 0)))"

  have m'_less: "i. i < φ 0  m' i = m i" by (simp add: m'_def)
  have m'_geq: "i. i  φ 0  m' i = t (φ (i - φ 0))" by (simp add: m'_def)

  have "i. m' i  lists A" using ne_lists [OF ne] and lists by (auto simp: m'_def t_def)
  moreover have "length (m' (φ 0)) < length (m (φ 0))" using ne by (simp add: t_def m'_geq)
  moreover have "j<φ 0. m' j = m j" by (auto simp: m'_less)
  ultimately have "(m, m')  gseq" using lists by (auto simp: gseq_def)
  moreover have "bad ?P m'"
  proof
    assume "good ?P m'"
    then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by (auto simp: good_def)
    { assume "j < φ 0"
      with i < j and emb have "?P (m i) (m j)" by (auto simp: m'_less)
      with i < j and bad have False by blast }
    moreover
    { assume "φ 0  i"
      with i < j and emb have "?P (t (φ (i - φ 0))) (t (φ (j - φ 0)))"
        and "i - φ 0 < j - φ 0" by (auto simp: m'_geq)
      with bad_t have False by auto }
    moreover
    { assume "i < φ 0" and "φ 0  j"
      with i < j and emb have "?P (m i) (t (φ (j - φ 0)))" by (simp add: m'_less m'_geq)
      from list_emb_Cons [OF this, of "h (φ (j - φ 0))"]
        have "?P (m i) (m (φ (j - φ 0)))" using ne by (simp add: h_def t_def)
      moreover have "i < φ (j - φ 0)"
        using less [of 0 "j - φ 0"] and i < φ 0 and φ 0  j
        by (cases "j = φ 0") auto
      ultimately have False using bad by blast }
    ultimately show False using i < j by arith
  qed
  ultimately show False using min by blast
qed


subsection ‹Natural Numbers›

lemma almost_full_on_UNIV_nat:
  "almost_full_on (≤) (UNIV :: nat set)"
proof -
  let ?P = "subseq :: bool list  bool list  bool"
  have *: "length ` (UNIV :: bool list set) = (UNIV :: nat set)"
    by (metis Ex_list_of_length surj_def)
  have "almost_full_on (≤) (length ` (UNIV :: bool list set))"
  proof (rule almost_full_on_hom)
    fix xs ys :: "bool list"
    assume "?P xs ys"
    then show "length xs  length ys"
      by (metis list_emb_length)
  next
    have "finite (UNIV :: bool set)" by auto
    from almost_full_on_lists [OF eq_almost_full_on_finite_set [OF this]]
      show "almost_full_on ?P UNIV" unfolding lists_UNIV .
  qed
  then show ?thesis unfolding * .
qed

end