src/HOL/Library/Ramsey.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61585 a9599d3d7610
child 63060 293ede07b775
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/Ramsey.thy
     2     Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
     3 *)
     4 
     5 section "Ramsey's Theorem"
     6 
     7 theory Ramsey
     8 imports Main Infinite_Set
     9 begin
    10 
    11 subsection\<open>Finite Ramsey theorem(s)\<close>
    12 
    13 text\<open>To distinguish the finite and infinite ones, lower and upper case
    14 names are used.
    15 
    16 This is the most basic version in terms of cliques and independent
    17 sets, i.e. the version for graphs and 2 colours.\<close>
    18 
    19 definition "clique V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> {v,w} : E)"
    20 definition "indep V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> \<not> {v,w} : E)"
    21 
    22 lemma ramsey2:
    23   "\<exists>r\<ge>1. \<forall> (V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
    24   (\<exists> R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
    25   (is "\<exists>r\<ge>1. ?R m n r")
    26 proof(induct k == "m+n" arbitrary: m n)
    27   case 0
    28   show ?case (is "EX r. ?R r")
    29   proof
    30     show "?R 1" using 0
    31       by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI)
    32   qed
    33 next
    34   case (Suc k)
    35   { assume "m=0"
    36     have ?case (is "EX r. ?R r")
    37     proof
    38       show "?R 1" using \<open>m=0\<close>
    39         by (simp add:clique_def)(metis card.empty emptyE empty_subsetI)
    40     qed
    41   } moreover
    42   { assume "n=0"
    43     have ?case (is "EX r. ?R r")
    44     proof
    45       show "?R 1" using \<open>n=0\<close>
    46         by (simp add:indep_def)(metis card.empty emptyE empty_subsetI)
    47     qed
    48   } moreover
    49   { assume "m\<noteq>0" "n\<noteq>0"
    50     then have "k = (m - 1) + n" "k = m + (n - 1)" using \<open>Suc k = m+n\<close> by auto
    51     from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
    52     obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
    53       by auto
    54     then have "r1+r2 \<ge> 1" by arith
    55     moreover
    56     have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
    57     proof clarify
    58       fix V :: "'a set" and E :: "'a set set"
    59       assume "finite V" "r1+r2 \<le> card V"
    60       with \<open>r1\<ge>1\<close> have "V \<noteq> {}" by auto
    61       then obtain v where "v : V" by blast
    62       let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
    63       let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
    64       have "V = insert v (?M \<union> ?N)" using \<open>v : V\<close> by auto
    65       then have "card V = card(insert v (?M \<union> ?N))" by metis
    66       also have "\<dots> = card ?M + card ?N + 1" using \<open>finite V\<close>
    67         by(fastforce intro: card_Un_disjoint)
    68       finally have "card V = card ?M + card ?N + 1" .
    69       then have "r1+r2 \<le> card ?M + card ?N + 1" using \<open>r1+r2 \<le> card V\<close> by simp
    70       then have "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
    71       moreover
    72       { assume "r1 \<le> card ?M"
    73         moreover have "finite ?M" using \<open>finite V\<close> by auto
    74         ultimately have "?EX ?M E (m - 1) n" using \<open>?R (m - 1) n r1\<close> by blast
    75         then obtain R where "R \<subseteq> ?M" "v ~: R" and
    76           CI: "card R = m - 1 \<and> clique R E \<or>
    77                card R = n \<and> indep R E" (is "?C \<or> ?I")
    78           by blast
    79         have "R <= V" using \<open>R <= ?M\<close> by auto
    80         have "finite R" using \<open>finite V\<close> \<open>R \<subseteq> V\<close> by (metis finite_subset)
    81         { assume "?I"
    82           with \<open>R <= V\<close> have "?EX V E m n" by blast
    83         } moreover
    84         { assume "?C"
    85           then have "clique (insert v R) E" using \<open>R <= ?M\<close>
    86            by(auto simp:clique_def insert_commute)
    87           moreover have "card(insert v R) = m"
    88             using \<open>?C\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>m\<noteq>0\<close> by simp
    89           ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
    90         } ultimately have "?EX V E m n" using CI by blast
    91       } moreover
    92       { assume "r2 \<le> card ?N"
    93         moreover have "finite ?N" using \<open>finite V\<close> by auto
    94         ultimately have "?EX ?N E m (n - 1)" using \<open>?R m (n - 1) r2\<close> by blast
    95         then obtain R where "R \<subseteq> ?N" "v ~: R" and
    96           CI: "card R = m \<and> clique R E \<or>
    97                card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
    98           by blast
    99         have "R <= V" using \<open>R <= ?N\<close> by auto
   100         have "finite R" using \<open>finite V\<close> \<open>R \<subseteq> V\<close> by (metis finite_subset)
   101         { assume "?C"
   102           with \<open>R <= V\<close> have "?EX V E m n" by blast
   103         } moreover
   104         { assume "?I"
   105           then have "indep (insert v R) E" using \<open>R <= ?N\<close>
   106             by(auto simp:indep_def insert_commute)
   107           moreover have "card(insert v R) = n"
   108             using \<open>?I\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>n\<noteq>0\<close> by simp
   109           ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
   110         } ultimately have "?EX V E m n" using CI by blast
   111       } ultimately show "?EX V E m n" by blast
   112     qed
   113     ultimately have ?case by blast
   114   } ultimately show ?case by blast
   115 qed
   116 
   117 
   118 subsection \<open>Preliminaries\<close>
   119 
   120 subsubsection \<open>``Axiom'' of Dependent Choice\<close>
   121 
   122 primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
   123   \<comment>\<open>An integer-indexed chain of choices\<close>
   124     choice_0:   "choice P r 0 = (SOME x. P x)"
   125   | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
   126 
   127 lemma choice_n:
   128   assumes P0: "P x0"
   129       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
   130   shows "P (choice P r n)"
   131 proof (induct n)
   132   case 0 show ?case by (force intro: someI P0)
   133 next
   134   case Suc then show ?case by (auto intro: someI2_ex [OF Pstep])
   135 qed
   136 
   137 lemma dependent_choice:
   138   assumes trans: "trans r"
   139       and P0: "P x0"
   140       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
   141   obtains f :: "nat => 'a" where
   142     "!!n. P (f n)" and "!!n m. n < m ==> (f n, f m) \<in> r"
   143 proof
   144   fix n
   145   show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
   146 next
   147   have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
   148     using Pstep [OF choice_n [OF P0 Pstep]]
   149     by (auto intro: someI2_ex)
   150   fix n m :: nat
   151   assume less: "n < m"
   152   show "(choice P r n, choice P r m) \<in> r" using PSuc
   153     by (auto intro: less_Suc_induct [OF less] transD [OF trans])
   154 qed
   155 
   156 
   157 subsubsection \<open>Partitions of a Set\<close>
   158 
   159 definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
   160   \<comment>\<open>the function @{term f} partitions the @{term r}-subsets of the typically
   161        infinite set @{term Y} into @{term s} distinct categories.\<close>
   162 where
   163   "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
   164 
   165 text\<open>For induction, we decrease the value of @{term r} in partitions.\<close>
   166 lemma part_Suc_imp_part:
   167      "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
   168       ==> part r s (Y - {y}) (%u. f (insert y u))"
   169   apply(simp add: part_def, clarify)
   170   apply(drule_tac x="insert y X" in spec)
   171   apply(force)
   172   done
   173 
   174 lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
   175   unfolding part_def by blast
   176 
   177 
   178 subsection \<open>Ramsey's Theorem: Infinitary Version\<close>
   179 
   180 lemma Ramsey_induction:
   181   fixes s and r::nat
   182   shows
   183   "!!(YY::'a set) (f::'a set => nat).
   184       [|infinite YY; part r s YY f|]
   185       ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
   186                   (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
   187 proof (induct r)
   188   case 0
   189   then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
   190 next
   191   case (Suc r)
   192   show ?case
   193   proof -
   194     from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
   195     let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
   196     let ?propr = "%(y,Y,t).
   197                  y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
   198                  & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
   199     have infYY': "infinite (YY-{yy})" using Suc.prems by auto
   200     have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
   201       by (simp add: o_def part_Suc_imp_part yy Suc.prems)
   202     have transr: "trans ?ramr" by (force simp add: trans_def)
   203     from Suc.hyps [OF infYY' partf']
   204     obtain Y0 and t0
   205     where "Y0 \<subseteq> YY - {yy}"  "infinite Y0"  "t0 < s"
   206           "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
   207         by blast
   208     with yy have propr0: "?propr(yy,Y0,t0)" by blast
   209     have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
   210     proof -
   211       fix x
   212       assume px: "?propr x" then show "?thesis x"
   213       proof (cases x)
   214         case (fields yx Yx tx)
   215         then obtain yx' where yx': "yx' \<in> Yx" using px
   216                by (blast dest: infinite_imp_nonempty)
   217         have infYx': "infinite (Yx-{yx'})" using fields px by auto
   218         with fields px yx' Suc.prems
   219         have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
   220           by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
   221         from Suc.hyps [OF infYx' partfx']
   222         obtain Y' and t'
   223         where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
   224                "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
   225             by blast
   226         show ?thesis
   227         proof
   228           show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
   229             using fields Y' yx' px by blast
   230         qed
   231       qed
   232     qed
   233     from dependent_choice [OF transr propr0 proprstep]
   234     obtain g where pg: "!!n::nat.  ?propr (g n)"
   235       and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
   236     let ?gy = "fst o g"
   237     let ?gt = "snd o snd o g"
   238     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
   239     proof (intro exI subsetI)
   240       fix x
   241       assume "x \<in> range ?gt"
   242       then obtain n where "x = ?gt n" ..
   243       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
   244     qed
   245     have "finite (range ?gt)"
   246       by (simp add: finite_nat_iff_bounded rangeg)
   247     then obtain s' and n'
   248       where s': "s' = ?gt n'"
   249         and infeqs': "infinite {n. ?gt n = s'}"
   250       by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
   251     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
   252     have inj_gy: "inj ?gy"
   253     proof (rule linorder_injI)
   254       fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
   255         using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
   256     qed
   257     show ?thesis
   258     proof (intro exI conjI)
   259       show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
   260         by (auto simp add: Let_def split_beta)
   261       show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
   262         by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
   263       show "s' < s" by (rule less')
   264       show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
   265           --> f X = s'"
   266       proof -
   267         {fix X
   268          assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
   269             and cardX: "finite X" "card X = Suc r"
   270          then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
   271              by (auto simp add: subset_image_iff)
   272          with cardX have "AA\<noteq>{}" by auto
   273          then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
   274          have "f X = s'"
   275          proof (cases "g (LEAST x. x \<in> AA)")
   276            case (fields ya Ya ta)
   277            with AAleast Xeq
   278            have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
   279            then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
   280            also have "... = ta"
   281            proof -
   282              have "X - {ya} \<subseteq> Ya"
   283              proof
   284                fix x assume x: "x \<in> X - {ya}"
   285                then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
   286                  by (auto simp add: Xeq)
   287                then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
   288                then have lessa': "(LEAST x. x \<in> AA) < a'"
   289                  using Least_le [of "%x. x \<in> AA", OF a'] by arith
   290                show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
   291              qed
   292              moreover
   293              have "card (X - {ya}) = r"
   294                by (simp add: cardX ya)
   295              ultimately show ?thesis
   296                using pg [of "LEAST x. x \<in> AA"] fields cardX
   297                by (clarsimp simp del:insert_Diff_single)
   298            qed
   299            also have "... = s'" using AA AAleast fields by auto
   300            finally show ?thesis .
   301          qed}
   302         then show ?thesis by blast
   303       qed
   304     qed
   305   qed
   306 qed
   307 
   308 
   309 theorem Ramsey:
   310   fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
   311   shows
   312    "[|infinite Z;
   313       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
   314   ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
   315             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
   316 by (blast intro: Ramsey_induction [unfolded part_def])
   317 
   318 
   319 corollary Ramsey2:
   320   fixes s::nat and Z::"'a set" and f::"'a set => nat"
   321   assumes infZ: "infinite Z"
   322       and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x\<noteq>y --> f{x,y} < s"
   323   shows
   324    "\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y --> f{x,y} = t)"
   325 proof -
   326   have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
   327     using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
   328   obtain Y t
   329     where *: "Y \<subseteq> Z" "infinite Y" "t < s"
   330           "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
   331     by (insert Ramsey [OF infZ part2]) auto
   332   then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
   333   with * show ?thesis by iprover
   334 qed
   335 
   336 
   337 subsection \<open>Disjunctive Well-Foundedness\<close>
   338 
   339 text \<open>
   340   An application of Ramsey's theorem to program termination. See
   341   @{cite "Podelski-Rybalchenko"}.
   342 \<close>
   343 
   344 definition disj_wf :: "('a * 'a)set => bool"
   345   where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
   346 
   347 definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
   348   where
   349     "transition_idx s T A =
   350       (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
   351 
   352 
   353 lemma transition_idx_less:
   354     "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
   355 apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
   356 apply (simp add: transition_idx_def, blast intro: Least_le)
   357 done
   358 
   359 lemma transition_idx_in:
   360     "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
   361 apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
   362             cong: conj_cong)
   363 apply (erule LeastI)
   364 done
   365 
   366 text\<open>To be equal to the union of some well-founded relations is equivalent
   367 to being the subset of such a union.\<close>
   368 lemma disj_wf:
   369      "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
   370 apply (auto simp add: disj_wf_def)
   371 apply (rule_tac x="%i. T i Int r" in exI)
   372 apply (rule_tac x=n in exI)
   373 apply (force simp add: wf_Int1)
   374 done
   375 
   376 theorem trans_disj_wf_implies_wf:
   377   assumes transr: "trans r"
   378       and dwf:    "disj_wf(r)"
   379   shows "wf r"
   380 proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
   381   assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
   382   then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
   383   have s: "!!i j. i < j ==> (s j, s i) \<in> r"
   384   proof -
   385     fix i and j::nat
   386     assume less: "i<j"
   387     then show "(s j, s i) \<in> r"
   388     proof (rule less_Suc_induct)
   389       show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
   390       show "\<And>i j k. \<lbrakk>(s j, s i) \<in> r; (s k, s j) \<in> r\<rbrakk> \<Longrightarrow> (s k, s i) \<in> r"
   391         using transr by (unfold trans_def, blast)
   392     qed
   393   qed
   394   from dwf
   395   obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
   396     by (auto simp add: disj_wf_def)
   397   have s_in_T: "\<And>i j. i<j ==> \<exists>k. (s j, s i) \<in> T k & k<n"
   398   proof -
   399     fix i and j::nat
   400     assume less: "i<j"
   401     then have "(s j, s i) \<in> r" by (rule s [of i j])
   402     then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
   403   qed
   404   have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
   405     apply (auto simp add: linorder_neq_iff)
   406     apply (blast dest: s_in_T transition_idx_less)
   407     apply (subst insert_commute)
   408     apply (blast dest: s_in_T transition_idx_less)
   409     done
   410   have
   411    "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
   412           (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
   413     by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
   414   then obtain K and k
   415     where infK: "infinite K" and less: "k < n" and
   416           allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
   417     by auto
   418   have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"
   419   proof
   420     fix m::nat
   421     let ?j = "enumerate K (Suc m)"
   422     let ?i = "enumerate K m"
   423     have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
   424     have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
   425     have ij: "?i < ?j" by (simp add: enumerate_step infK)
   426     have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
   427       by (simp add: allk)
   428     obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
   429       using s_in_T [OF ij] by blast
   430     then show "(s ?j, s ?i) \<in> T k"
   431       by (simp add: ijk [symmetric] transition_idx_in ij)
   432   qed
   433   then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
   434   then show False using wfT less by blast
   435 qed
   436 
   437 end