src/HOL/Library/Ramsey.thy

tuned proofs;

(*  Title:      HOL/Library/Ramsey.thy
    Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
*)

section \<open>Ramsey's Theorem\<close>

theory Ramsey
  imports Infinite_Set
begin

subsection \<open>Finite Ramsey theorem(s)\<close>

text \<open>
  To distinguish the finite and infinite ones, lower and upper case
  names are used.

  This is the most basic version in terms of cliques and independent
  sets, i.e. the version for graphs and 2 colours.
\<close>

definition "clique V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<in> E)"
definition "indep V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<notin> E)"

lemma ramsey2:
  "\<exists>r\<ge>1. \<forall>(V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
    (\<exists>R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
  (is "\<exists>r\<ge>1. ?R m n r")
proof (induct k \<equiv> "m + n" arbitrary: m n)
  case 0
  show ?case (is "EX r. ?Q r")
  proof
    from 0 show "?Q 1"
      by (clarsimp simp: indep_def) (metis card.empty emptyE empty_subsetI)
  qed
next
  case (Suc k)
  consider "m = 0 \<or> n = 0" | "m \<noteq> 0" "n \<noteq> 0" by auto
  then show ?case (is "EX r. ?Q r")
  proof cases
    case 1
    then have "?Q 1"
      by (simp add: clique_def) (meson card_empty empty_iff empty_subsetI indep_def)
    then show ?thesis ..
  next
    case 2
    with Suc(2) have "k = (m - 1) + n" "k = m + (n - 1)" by auto
    from this [THEN Suc(1)]
    obtain r1 r2 where "r1 \<ge> 1" "r2 \<ge> 1" "?R (m - 1) n r1" "?R m (n - 1) r2" by auto
    then have "r1 + r2 \<ge> 1" by arith
    moreover have "?R m n (r1 + r2)" (is "\<forall>V E. _ \<longrightarrow> ?EX V E m n")
    proof clarify
      fix V :: "'a set"
      fix E :: "'a set set"
      assume "finite V" "r1 + r2 \<le> card V"
      with \<open>r1 \<ge> 1\<close> have "V \<noteq> {}" by auto
      then obtain v where "v \<in> V" by blast
      let ?M = "{w \<in> V. w \<noteq> v \<and> {v, w} \<in> E}"
      let ?N = "{w \<in> V. w \<noteq> v \<and> {v, w} \<notin> E}"
      from \<open>v \<in> V\<close> have "V = insert v (?M \<union> ?N)" by auto
      then have "card V = card (insert v (?M \<union> ?N))" by metis
      also from \<open>finite V\<close> have "\<dots> = card ?M + card ?N + 1"
        by (fastforce intro: card_Un_disjoint)
      finally have "card V = card ?M + card ?N + 1" .
      with \<open>r1 + r2 \<le> card V\<close> have "r1 + r2 \<le> card ?M + card ?N + 1" by simp
      then consider "r1 \<le> card ?M" | "r2 \<le> card ?N" by arith
      then show "?EX V E m n"
      proof cases
        case 1
        from \<open>finite V\<close> have "finite ?M" by auto
        with \<open>?R (m - 1) n r1\<close> and 1 have "?EX ?M E (m - 1) n" by blast
        then obtain R where "R \<subseteq> ?M" "v \<notin> R"
          and CI: "card R = m - 1 \<and> clique R E \<or> card R = n \<and> indep R E" (is "?C \<or> ?I")
          by blast
        from \<open>R \<subseteq> ?M\<close> have "R \<subseteq> V" by auto
        with \<open>finite V\<close> have "finite R" by (metis finite_subset)
        from CI show ?thesis
        proof
          assume "?I"
          with \<open>R \<subseteq> V\<close> show ?thesis by blast
        next
          assume "?C"
          with \<open>R \<subseteq> ?M\<close> have *: "clique (insert v R) E"
            by (auto simp: clique_def insert_commute)
          from \<open>?C\<close> \<open>finite R\<close> \<open>v \<notin> R\<close> \<open>m \<noteq> 0\<close> have "card (insert v R) = m" by simp
          with \<open>R \<subseteq> V\<close> \<open>v \<in> V\<close> * show ?thesis by (metis insert_subset)
        qed
      next
        case 2
        from \<open>finite V\<close> have "finite ?N" by auto
        with \<open>?R m (n - 1) r2\<close> 2 have "?EX ?N E m (n - 1)" by blast
        then obtain R where "R \<subseteq> ?N" "v \<notin> R"
          and CI: "card R = m \<and> clique R E \<or> card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
          by blast
        from \<open>R \<subseteq> ?N\<close> have "R \<subseteq> V" by auto
        with \<open>finite V\<close> have "finite R" by (metis finite_subset)
        from CI show ?thesis
        proof
          assume "?C"
          with \<open>R \<subseteq> V\<close> show ?thesis by blast
        next
          assume "?I"
          with \<open>R \<subseteq> ?N\<close> have *: "indep (insert v R) E"
            by (auto simp: indep_def insert_commute)
          from \<open>?I\<close> \<open>finite R\<close> \<open>v \<notin> R\<close> \<open>n \<noteq> 0\<close> have "card (insert v R) = n" by simp
          with \<open>R \<subseteq> V\<close> \<open>v \<in> V\<close> * show ?thesis by (metis insert_subset)
        qed
      qed
    qed
    ultimately show ?thesis by blast
  qed
qed


subsection \<open>Preliminaries\<close>

subsubsection \<open>``Axiom'' of Dependent Choice\<close>

primrec choice :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a"
  where \<comment> \<open>An integer-indexed chain of choices\<close>
    choice_0: "choice P r 0 = (SOME x. P x)"
  | choice_Suc: "choice P r (Suc n) = (SOME y. P y \<and> (choice P r n, y) \<in> r)"

lemma choice_n:
  assumes P0: "P x0"
    and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r"
  shows "P (choice P r n)"
proof (induct n)
  case 0
  show ?case by (force intro: someI P0)
next
  case Suc
  then show ?case by (auto intro: someI2_ex [OF Pstep])
qed

lemma dependent_choice:
  assumes trans: "trans r"
    and P0: "P x0"
    and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r"
  obtains f :: "nat \<Rightarrow> 'a" where "\<And>n. P (f n)" and "\<And>n m. n < m \<Longrightarrow> (f n, f m) \<in> r"
proof
  fix n
  show "P (choice P r n)"
    by (blast intro: choice_n [OF P0 Pstep])
next
  fix n m :: nat
  assume "n < m"
  from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) \<in> r" for k
    by (auto intro: someI2_ex)
  then show "(choice P r n, choice P r m) \<in> r"
    by (auto intro: less_Suc_induct [OF \<open>n < m\<close>] transD [OF trans])
qed


subsubsection \<open>Partitions of a Set\<close>

definition part :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
  \<comment> \<open>the function @{term f} partitions the @{term r}-subsets of the typically
      infinite set @{term Y} into @{term s} distinct categories.\<close>
  where "part r s Y f \<longleftrightarrow> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X < s)"

text \<open>For induction, we decrease the value of @{term r} in partitions.\<close>
lemma part_Suc_imp_part:
  "\<lbrakk>infinite Y; part (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part r s (Y - {y}) (\<lambda>u. f (insert y u))"
  apply (simp add: part_def)
  apply clarify
  apply (drule_tac x="insert y X" in spec)
  apply force
  done

lemma part_subset: "part r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part r s Y f"
  unfolding part_def by blast


subsection \<open>Ramsey's Theorem: Infinitary Version\<close>

lemma Ramsey_induction:
  fixes s r :: nat
    and YY :: "'a set"
    and f :: "'a set \<Rightarrow> nat"
  assumes "infinite YY" "part r s YY f"
  shows "\<exists>Y' t'. Y' \<subseteq> YY \<and> infinite Y' \<and> t' < s \<and> (\<forall>X. X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> f X = t')"
  using assms
proof (induct r arbitrary: YY f)
  case 0
  then show ?case
    by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
next
  case (Suc r)
  show ?case
  proof -
    from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY"
      by blast
    let ?ramr = "{((y, Y, t), (y', Y', t')). y' \<in> Y \<and> Y' \<subseteq> Y}"
    let ?propr = "\<lambda>(y, Y, t).
                 y \<in> YY \<and> y \<notin> Y \<and> Y \<subseteq> YY \<and> infinite Y \<and> t < s
                 \<and> (\<forall>X. X\<subseteq>Y \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert y) X = t)"
    from Suc.prems have infYY': "infinite (YY - {yy})" by auto
    from Suc.prems have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
      by (simp add: o_def part_Suc_imp_part yy)
    have transr: "trans ?ramr" by (force simp add: trans_def)
    from Suc.hyps [OF infYY' partf']
    obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
      "X \<subseteq> Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0" for X
      by blast
    with yy have propr0: "?propr(yy, Y0, t0)" by blast
    have proprstep: "\<exists>y. ?propr y \<and> (x, y) \<in> ?ramr" if x: "?propr x" for x
    proof (cases x)
      case (fields yx Yx tx)
      with x obtain yx' where yx': "yx' \<in> Yx"
        by (blast dest: infinite_imp_nonempty)
      from fields x have infYx': "infinite (Yx - {yx'})" by auto
      with fields x yx' Suc.prems have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
        by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
      from Suc.hyps [OF infYx' partfx'] obtain Y' and t'
        where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
          "X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'" for X
        by blast
      from fields x Y' yx' have "?propr (yx', Y', t') \<and> (x, (yx', Y', t')) \<in> ?ramr"
        by blast
      then show ?thesis ..
    qed
    from dependent_choice [OF transr propr0 proprstep]
    obtain g where pg: "?propr (g n)" and rg: "n < m \<Longrightarrow> (g n, g m) \<in> ?ramr" for n m :: nat
      by blast
    let ?gy = "fst \<circ> g"
    let ?gt = "snd \<circ> snd \<circ> g"
    have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    proof (intro exI subsetI)
      fix x
      assume "x \<in> range ?gt"
      then obtain n where "x = ?gt n" ..
      with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
    qed
    have "finite (range ?gt)"
      by (simp add: finite_nat_iff_bounded rangeg)
    then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}"
      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
    with pg [of n'] have less': "s'<s" by (cases "g n'") auto
    have inj_gy: "inj ?gy"
    proof (rule linorder_injI)
      fix m m' :: nat
      assume "m < m'"
      from rg [OF this] pg [of m] show "?gy m \<noteq> ?gy m'"
        by (cases "g m", cases "g m'") auto
    qed
    show ?thesis
    proof (intro exI conjI)
      from pg show "?gy ` {n. ?gt n = s'} \<subseteq> YY"
        by (auto simp add: Let_def split_beta)
      from infeqs' show "infinite (?gy ` {n. ?gt n = s'})"
        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
      show "s' < s" by (rule less')
      show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} \<and> finite X \<and> card X = Suc r \<longrightarrow> f X = s'"
      proof -
        have "f X = s'"
          if X: "X \<subseteq> ?gy ` {n. ?gt n = s'}"
          and cardX: "finite X" "card X = Suc r"
          for X
        proof -
          from X obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
            by (auto simp add: subset_image_iff)
          with cardX have "AA \<noteq> {}" by auto
          then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
          show ?thesis
          proof (cases "g (LEAST x. x \<in> AA)")
            case (fields ya Ya ta)
            with AAleast Xeq have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
            then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
            also have "\<dots> = ta"
            proof -
              have *: "X - {ya} \<subseteq> Ya"
              proof
                fix x assume x: "x \<in> X - {ya}"
                then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
                  by (auto simp add: Xeq)
                with fields x have "a' \<noteq> (LEAST x. x \<in> AA)" by auto
                with Least_le [of "\<lambda>x. x \<in> AA", OF a'] have "(LEAST x. x \<in> AA) < a'"
                  by arith
                from xeq fields rg [OF this] show "x \<in> Ya" by auto
              qed
              have "card (X - {ya}) = r"
                by (simp add: cardX ya)
              with pg [of "LEAST x. x \<in> AA"] fields cardX * show ?thesis
                by (auto simp del: insert_Diff_single)
            qed
            also from AA AAleast fields have "\<dots> = s'" by auto
            finally show ?thesis .
          qed
        qed
        then show ?thesis by blast
      qed
    qed
  qed
qed


theorem Ramsey:
  fixes s r :: nat
    and Z :: "'a set"
    and f :: "'a set \<Rightarrow> nat"
  shows
   "\<lbrakk>infinite Z;
      \<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = r \<longrightarrow> f X < s\<rbrakk>
    \<Longrightarrow> \<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s
            \<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
  by (blast intro: Ramsey_induction [unfolded part_def])


corollary Ramsey2:
  fixes s :: nat
    and Z :: "'a set"
    and f :: "'a set \<Rightarrow> nat"
  assumes infZ: "infinite Z"
    and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x \<noteq> y \<longrightarrow> f {x, y} < s"
  shows "\<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s \<and> (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y \<longrightarrow> f {x, y} = t)"
proof -
  from part have part2: "\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = 2 \<longrightarrow> f X < s"
    by (fastforce simp add: eval_nat_numeral card_Suc_eq)
  obtain Y t where *:
    "Y \<subseteq> Z" "infinite Y" "t < s" "(\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = 2 \<longrightarrow> f X = t)"
    by (insert Ramsey [OF infZ part2]) auto
  then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
  with * show ?thesis by iprover
qed


subsection \<open>Disjunctive Well-Foundedness\<close>

text \<open>
  An application of Ramsey's theorem to program termination. See
  @{cite "Podelski-Rybalchenko"}.
\<close>

definition disj_wf :: "('a \<times> 'a) set \<Rightarrow> bool"
  where "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf (T i)) \<and> r = (\<Union>i<n. T i))"

definition transition_idx :: "(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> ('a \<times> 'a) set) \<Rightarrow> nat set \<Rightarrow> nat"
  where "transition_idx s T A = (LEAST k. \<exists>i j. A = {i, j} \<and> i < j \<and> (s j, s i) \<in> T k)"


lemma transition_idx_less:
  assumes "i < j" "(s j, s i) \<in> T k" "k < n"
  shows "transition_idx s T {i, j} < n"
proof -
  from assms(1,2) have "transition_idx s T {i, j} \<le> k"
    by (simp add: transition_idx_def, blast intro: Least_le)
  with assms(3) show ?thesis by simp
qed

lemma transition_idx_in:
  assumes "i < j" "(s j, s i) \<in> T k"
  shows "(s j, s i) \<in> T (transition_idx s T {i, j})"
  using assms
  by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI)

text \<open>To be equal to the union of some well-founded relations is equivalent
  to being the subset of such a union.\<close>
lemma disj_wf: "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) \<and> r \<subseteq> (\<Union>i<n. T i))"
  apply (auto simp add: disj_wf_def)
  apply (rule_tac x="\<lambda>i. T i Int r" in exI)
  apply (rule_tac x=n in exI)
  apply (force simp add: wf_Int1)
  done

theorem trans_disj_wf_implies_wf:
  assumes "trans r"
    and "disj_wf r"
  shows "wf r"
proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
  assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
  then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
  from \<open>disj_wf r\<close> obtain T and n :: nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
    by (auto simp add: disj_wf_def)
  have s_in_T: "\<exists>k. (s j, s i) \<in> T k \<and> k<n" if "i < j" for i j
  proof -
    from \<open>i < j\<close> have "(s j, s i) \<in> r"
    proof (induct rule: less_Suc_induct)
      case 1
      then show ?case by (simp add: sSuc)
    next
      case 2
      with \<open>trans r\<close> show ?case
        unfolding trans_def by blast
    qed
    then show ?thesis by (auto simp add: r)
  qed
  have trless: "i \<noteq> j \<Longrightarrow> transition_idx s T {i, j} < n" for i j
    apply (auto simp add: linorder_neq_iff)
     apply (blast dest: s_in_T transition_idx_less)
    apply (subst insert_commute)
    apply (blast dest: s_in_T transition_idx_less)
    done
  have "\<exists>K k. K \<subseteq> UNIV \<and> infinite K \<and> k < n \<and>
      (\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k)"
    by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
  then obtain K and k where infK: "infinite K" and "k < n"
    and allk: "\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k"
    by auto
  have "(s (enumerate K (Suc m)), s (enumerate K m)) \<in> T k" for m :: nat
  proof -
    let ?j = "enumerate K (Suc m)"
    let ?i = "enumerate K m"
    have ij: "?i < ?j" by (simp add: enumerate_step infK)
    have "?j \<in> K" "?i \<in> K" by (simp_all add: enumerate_in_set infK)
    with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk)
    from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" by blast
    then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij)
  qed
  then have "\<not> wf (T k)"
    unfolding wf_iff_no_infinite_down_chain by fast
  with wfT \<open>k < n\<close> show False by blast
qed

end