src/HOL/Library/Ramsey.thy
 author haftmann Fri Mar 27 10:05:11 2009 +0100 (2009-03-27) changeset 30738 0842e906300c parent 28741 1b257449f804 child 32960 69916a850301 permissions -rw-r--r--
normalized imports
 paulson@19944 ` 1` ```(* Title: HOL/Library/Ramsey.thy ``` paulson@19944 ` 2` ``` Author: Tom Ridge. Converted to structured Isar by L C Paulson ``` paulson@19944 ` 3` ```*) ``` paulson@19944 ` 4` paulson@19944 ` 5` ```header "Ramsey's Theorem" ``` paulson@19944 ` 6` haftmann@25594 ` 7` ```theory Ramsey ``` haftmann@30738 ` 8` ```imports Main Infinite_Set ``` haftmann@25594 ` 9` ```begin ``` paulson@19944 ` 10` wenzelm@22665 ` 11` ```subsection {* Preliminaries *} ``` paulson@19944 ` 12` wenzelm@22665 ` 13` ```subsubsection {* ``Axiom'' of Dependent Choice *} ``` paulson@19944 ` 14` wenzelm@19948 ` 15` ```consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a" ``` paulson@19944 ` 16` ``` --{*An integer-indexed chain of choices*} ``` paulson@19944 ` 17` ```primrec ``` paulson@19944 ` 18` ``` choice_0: "choice P r 0 = (SOME x. P x)" ``` paulson@19944 ` 19` paulson@19944 ` 20` ``` choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \ r)" ``` paulson@19944 ` 21` paulson@19944 ` 22` paulson@19944 ` 23` ```lemma choice_n: ``` paulson@19944 ` 24` ``` assumes P0: "P x0" ``` paulson@19944 ` 25` ``` and Pstep: "!!x. P x ==> \y. P y & (x,y) \ r" ``` paulson@19944 ` 26` ``` shows "P (choice P r n)" ``` wenzelm@19948 ` 27` ```proof (induct n) ``` wenzelm@19948 ` 28` ``` case 0 show ?case by (force intro: someI P0) ``` wenzelm@19948 ` 29` ```next ``` wenzelm@19948 ` 30` ``` case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) ``` wenzelm@19948 ` 31` ```qed ``` paulson@19944 ` 32` paulson@19944 ` 33` ```lemma dependent_choice: ``` paulson@19944 ` 34` ``` assumes trans: "trans r" ``` paulson@19944 ` 35` ``` and P0: "P x0" ``` paulson@19944 ` 36` ``` and Pstep: "!!x. P x ==> \y. P y & (x,y) \ r" ``` paulson@19954 ` 37` ``` obtains f :: "nat => 'a" where ``` paulson@19954 ` 38` ``` "!!n. P (f n)" and "!!n m. n < m ==> (f n, f m) \ r" ``` paulson@19954 ` 39` ```proof ``` paulson@19954 ` 40` ``` fix n ``` paulson@19954 ` 41` ``` show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep]) ``` paulson@19944 ` 42` ```next ``` paulson@19944 ` 43` ``` have PSuc: "\n. (choice P r n, choice P r (Suc n)) \ r" ``` paulson@19944 ` 44` ``` using Pstep [OF choice_n [OF P0 Pstep]] ``` paulson@19944 ` 45` ``` by (auto intro: someI2_ex) ``` paulson@19954 ` 46` ``` fix n m :: nat ``` paulson@19954 ` 47` ``` assume less: "n < m" ``` paulson@19954 ` 48` ``` show "(choice P r n, choice P r m) \ r" using PSuc ``` paulson@19954 ` 49` ``` by (auto intro: less_Suc_induct [OF less] transD [OF trans]) ``` paulson@19954 ` 50` ```qed ``` paulson@19944 ` 51` paulson@19944 ` 52` wenzelm@22665 ` 53` ```subsubsection {* Partitions of a Set *} ``` paulson@19944 ` 54` wenzelm@19948 ` 55` ```definition ``` wenzelm@19948 ` 56` ``` part :: "nat => nat => 'a set => ('a set => nat) => bool" ``` paulson@19944 ` 57` ``` --{*the function @{term f} partitions the @{term r}-subsets of the typically ``` paulson@19944 ` 58` ``` infinite set @{term Y} into @{term s} distinct categories.*} ``` krauss@21634 ` 59` ```where ``` wenzelm@19948 ` 60` ``` "part r s Y f = (\X. X \ Y & finite X & card X = r --> f X < s)" ``` paulson@19944 ` 61` paulson@19944 ` 62` ```text{*For induction, we decrease the value of @{term r} in partitions.*} ``` paulson@19944 ` 63` ```lemma part_Suc_imp_part: ``` paulson@19944 ` 64` ``` "[| infinite Y; part (Suc r) s Y f; y \ Y |] ``` paulson@19944 ` 65` ``` ==> part r s (Y - {y}) (%u. f (insert y u))" ``` paulson@19944 ` 66` ``` apply(simp add: part_def, clarify) ``` paulson@19944 ` 67` ``` apply(drule_tac x="insert y X" in spec) ``` nipkow@24853 ` 68` ``` apply(force) ``` paulson@19944 ` 69` ``` done ``` paulson@19944 ` 70` paulson@19944 ` 71` ```lemma part_subset: "part r s YY f ==> Y \ YY ==> part r s Y f" ``` wenzelm@19948 ` 72` ``` unfolding part_def by blast ``` paulson@19944 ` 73` ``` ``` paulson@19944 ` 74` wenzelm@22665 ` 75` ```subsection {* Ramsey's Theorem: Infinitary Version *} ``` paulson@19944 ` 76` paulson@19954 ` 77` ```lemma Ramsey_induction: ``` paulson@19954 ` 78` ``` fixes s and r::nat ``` paulson@19944 ` 79` ``` shows ``` paulson@19944 ` 80` ``` "!!(YY::'a set) (f::'a set => nat). ``` paulson@19944 ` 81` ``` [|infinite YY; part r s YY f|] ``` paulson@19944 ` 82` ``` ==> \Y' t'. Y' \ YY & infinite Y' & t' < s & ``` paulson@19944 ` 83` ``` (\X. X \ Y' & finite X & card X = r --> f X = t')" ``` paulson@19944 ` 84` ```proof (induct r) ``` paulson@19944 ` 85` ``` case 0 ``` nipkow@24853 ` 86` ``` thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong) ``` paulson@19944 ` 87` ```next ``` paulson@19944 ` 88` ``` case (Suc r) ``` paulson@19944 ` 89` ``` show ?case ``` paulson@19944 ` 90` ``` proof - ``` paulson@19944 ` 91` ``` from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \ YY" by blast ``` paulson@19944 ` 92` ``` let ?ramr = "{((y,Y,t),(y',Y',t')). y' \ Y & Y' \ Y}" ``` paulson@19944 ` 93` ``` let ?propr = "%(y,Y,t). ``` paulson@19944 ` 94` ``` y \ YY & y \ Y & Y \ YY & infinite Y & t < s ``` paulson@19944 ` 95` ``` & (\X. X\Y & finite X & card X = r --> (f o insert y) X = t)" ``` paulson@19944 ` 96` ``` have infYY': "infinite (YY-{yy})" using Suc.prems by auto ``` paulson@19944 ` 97` ``` have partf': "part r s (YY - {yy}) (f \ insert yy)" ``` paulson@19944 ` 98` ``` by (simp add: o_def part_Suc_imp_part yy Suc.prems) ``` paulson@19944 ` 99` ``` have transr: "trans ?ramr" by (force simp add: trans_def) ``` paulson@19944 ` 100` ``` from Suc.hyps [OF infYY' partf'] ``` paulson@19944 ` 101` ``` obtain Y0 and t0 ``` paulson@19944 ` 102` ``` where "Y0 \ YY - {yy}" "infinite Y0" "t0 < s" ``` paulson@19944 ` 103` ``` "\X. X\Y0 \ finite X \ card X = r \ (f \ insert yy) X = t0" ``` paulson@19944 ` 104` ``` by blast ``` paulson@19944 ` 105` ``` with yy have propr0: "?propr(yy,Y0,t0)" by blast ``` paulson@19944 ` 106` ``` have proprstep: "\x. ?propr x \ \y. ?propr y \ (x, y) \ ?ramr" ``` paulson@19944 ` 107` ``` proof - ``` paulson@19944 ` 108` ``` fix x ``` paulson@19944 ` 109` ``` assume px: "?propr x" thus "?thesis x" ``` paulson@19944 ` 110` ``` proof (cases x) ``` paulson@19944 ` 111` ``` case (fields yx Yx tx) ``` paulson@19944 ` 112` ``` then obtain yx' where yx': "yx' \ Yx" using px ``` paulson@19944 ` 113` ``` by (blast dest: infinite_imp_nonempty) ``` paulson@19944 ` 114` ``` have infYx': "infinite (Yx-{yx'})" using fields px by auto ``` paulson@19944 ` 115` ``` with fields px yx' Suc.prems ``` paulson@19944 ` 116` ``` have partfx': "part r s (Yx - {yx'}) (f \ insert yx')" ``` paulson@19944 ` 117` ``` by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY]) ``` paulson@19944 ` 118` ``` from Suc.hyps [OF infYx' partfx'] ``` paulson@19944 ` 119` ``` obtain Y' and t' ``` paulson@19944 ` 120` ``` where Y': "Y' \ Yx - {yx'}" "infinite Y'" "t' < s" ``` paulson@19944 ` 121` ``` "\X. X\Y' \ finite X \ card X = r \ (f \ insert yx') X = t'" ``` paulson@19944 ` 122` ``` by blast ``` paulson@19944 ` 123` ``` show ?thesis ``` paulson@19944 ` 124` ``` proof ``` paulson@19944 ` 125` ``` show "?propr (yx',Y',t') & (x, (yx',Y',t')) \ ?ramr" ``` paulson@19944 ` 126` ``` using fields Y' yx' px by blast ``` paulson@19944 ` 127` ``` qed ``` paulson@19944 ` 128` ``` qed ``` paulson@19944 ` 129` ``` qed ``` paulson@19944 ` 130` ``` from dependent_choice [OF transr propr0 proprstep] ``` nipkow@19946 ` 131` ``` obtain g where pg: "!!n::nat. ?propr (g n)" ``` paulson@19954 ` 132` ``` and rg: "!!n m. n (g n, g m) \ ?ramr" by blast ``` haftmann@28741 ` 133` ``` let ?gy = "fst o g" ``` haftmann@28741 ` 134` ``` let ?gt = "snd o snd o g" ``` paulson@19944 ` 135` ``` have rangeg: "\k. range ?gt \ {.. range ?gt" ``` paulson@19944 ` 139` ``` then obtain n where "x = ?gt n" .. ``` paulson@19944 ` 140` ``` with pg [of n] show "x \ {.. ?gy m'" ``` wenzelm@19948 ` 152` ``` using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto ``` paulson@19944 ` 153` ``` qed ``` paulson@19944 ` 154` ``` show ?thesis ``` paulson@19944 ` 155` ``` proof (intro exI conjI) ``` paulson@19944 ` 156` ``` show "?gy ` {n. ?gt n = s'} \ YY" using pg ``` paulson@19944 ` 157` ``` by (auto simp add: Let_def split_beta) ``` paulson@19944 ` 158` ``` show "infinite (?gy ` {n. ?gt n = s'})" using infeqs' ``` paulson@19944 ` 159` ``` by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) ``` paulson@19944 ` 160` ``` show "s' < s" by (rule less') ``` paulson@19944 ` 161` ``` show "\X. X \ ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r ``` paulson@19944 ` 162` ``` --> f X = s'" ``` paulson@19944 ` 163` ``` proof - ``` paulson@19944 ` 164` ``` {fix X ``` paulson@19944 ` 165` ``` assume "X \ ?gy ` {n. ?gt n = s'}" ``` paulson@19944 ` 166` ``` and cardX: "finite X" "card X = Suc r" ``` paulson@19944 ` 167` ``` then obtain AA where AA: "AA \ {n. ?gt n = s'}" and Xeq: "X = ?gy`AA" ``` paulson@19944 ` 168` ``` by (auto simp add: subset_image_iff) ``` paulson@19944 ` 169` ``` with cardX have "AA\{}" by auto ``` paulson@19944 ` 170` ``` hence AAleast: "(LEAST x. x \ AA) \ AA" by (auto intro: LeastI_ex) ``` paulson@19944 ` 171` ``` have "f X = s'" ``` paulson@19944 ` 172` ``` proof (cases "g (LEAST x. x \ AA)") ``` paulson@19944 ` 173` ``` case (fields ya Ya ta) ``` paulson@19944 ` 174` ``` with AAleast Xeq ``` paulson@19944 ` 175` ``` have ya: "ya \ X" by (force intro!: rev_image_eqI) ``` paulson@19944 ` 176` ``` hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb) ``` paulson@19944 ` 177` ``` also have "... = ta" ``` paulson@19944 ` 178` ``` proof - ``` paulson@19944 ` 179` ``` have "X - {ya} \ Ya" ``` paulson@19944 ` 180` ``` proof ``` paulson@19954 ` 181` ``` fix x assume x: "x \ X - {ya}" ``` paulson@19944 ` 182` ``` then obtain a' where xeq: "x = ?gy a'" and a': "a' \ AA" ``` paulson@19944 ` 183` ``` by (auto simp add: Xeq) ``` paulson@19944 ` 184` ``` hence "a' \ (LEAST x. x \ AA)" using x fields by auto ``` paulson@19944 ` 185` ``` hence lessa': "(LEAST x. x \ AA) < a'" ``` paulson@19944 ` 186` ``` using Least_le [of "%x. x \ AA", OF a'] by arith ``` paulson@19944 ` 187` ``` show "x \ Ya" using xeq fields rg [OF lessa'] by auto ``` paulson@19944 ` 188` ``` qed ``` paulson@19944 ` 189` ``` moreover ``` paulson@19944 ` 190` ``` have "card (X - {ya}) = r" ``` nipkow@24853 ` 191` ``` by (simp add: cardX ya) ``` paulson@19944 ` 192` ``` ultimately show ?thesis ``` paulson@19944 ` 193` ``` using pg [of "LEAST x. x \ AA"] fields cardX ``` nipkow@19946 ` 194` ``` by (clarsimp simp del:insert_Diff_single) ``` paulson@19944 ` 195` ``` qed ``` paulson@19944 ` 196` ``` also have "... = s'" using AA AAleast fields by auto ``` paulson@19944 ` 197` ``` finally show ?thesis . ``` paulson@19944 ` 198` ``` qed} ``` paulson@19944 ` 199` ``` thus ?thesis by blast ``` paulson@19944 ` 200` ``` qed ``` paulson@19944 ` 201` ``` qed ``` paulson@19944 ` 202` ``` qed ``` paulson@19944 ` 203` ```qed ``` paulson@19944 ` 204` paulson@19944 ` 205` paulson@19944 ` 206` ```theorem Ramsey: ``` wenzelm@19949 ` 207` ``` fixes s r :: nat and Z::"'a set" and f::"'a set => nat" ``` paulson@19944 ` 208` ``` shows ``` paulson@19944 ` 209` ``` "[|infinite Z; ``` paulson@19944 ` 210` ``` \X. X \ Z & finite X & card X = r --> f X < s|] ``` paulson@19944 ` 211` ``` ==> \Y t. Y \ Z & infinite Y & t < s ``` paulson@19944 ` 212` ``` & (\X. X \ Y & finite X & card X = r --> f X = t)" ``` paulson@19954 ` 213` ```by (blast intro: Ramsey_induction [unfolded part_def]) ``` paulson@19954 ` 214` paulson@19954 ` 215` paulson@19954 ` 216` ```corollary Ramsey2: ``` paulson@19954 ` 217` ``` fixes s::nat and Z::"'a set" and f::"'a set => nat" ``` paulson@19954 ` 218` ``` assumes infZ: "infinite Z" ``` paulson@19954 ` 219` ``` and part: "\x\Z. \y\Z. x\y --> f{x,y} < s" ``` paulson@19954 ` 220` ``` shows ``` paulson@19954 ` 221` ``` "\Y t. Y \ Z & infinite Y & t < s & (\x\Y. \y\Y. x\y --> f{x,y} = t)" ``` paulson@19954 ` 222` ```proof - ``` paulson@19954 ` 223` ``` have part2: "\X. X \ Z & finite X & card X = 2 --> f X < s" ``` nipkow@24853 ` 224` ``` using part by (fastsimp simp add: nat_number card_Suc_eq) ``` paulson@19954 ` 225` ``` obtain Y t ``` paulson@19954 ` 226` ``` where "Y \ Z" "infinite Y" "t < s" ``` paulson@19954 ` 227` ``` "(\X. X \ Y & finite X & card X = 2 --> f X = t)" ``` paulson@19954 ` 228` ``` by (insert Ramsey [OF infZ part2]) auto ``` paulson@19954 ` 229` ``` moreover from this have "\x\Y. \y\Y. x \ y \ f {x, y} = t" by auto ``` paulson@19954 ` 230` ``` ultimately show ?thesis by iprover ``` paulson@19954 ` 231` ```qed ``` paulson@19954 ` 232` paulson@19954 ` 233` wenzelm@22665 ` 234` ```subsection {* Disjunctive Well-Foundedness *} ``` paulson@19954 ` 235` wenzelm@22367 ` 236` ```text {* ``` wenzelm@22367 ` 237` ``` An application of Ramsey's theorem to program termination. See ``` wenzelm@22367 ` 238` ``` \cite{Podelski-Rybalchenko}. ``` paulson@19954 ` 239` ```*} ``` paulson@19954 ` 240` wenzelm@20810 ` 241` ```definition ``` paulson@19954 ` 242` ``` disj_wf :: "('a * 'a)set => bool" ``` krauss@21634 ` 243` ```where ``` wenzelm@20810 ` 244` ``` "disj_wf r = (\T. \n::nat. (\ii 'a, nat => ('a*'a)set, nat set] => nat" ``` krauss@21634 ` 248` ```where ``` wenzelm@20810 ` 249` ``` "transition_idx s T A = ``` wenzelm@20810 ` 250` ``` (LEAST k. \i j. A = {i,j} & i T k)" ``` paulson@19954 ` 251` paulson@19954 ` 252` paulson@19954 ` 253` ```lemma transition_idx_less: ``` paulson@19954 ` 254` ``` "[|i T k; k transition_idx s T {i,j} < n" ``` paulson@19954 ` 255` ```apply (subgoal_tac "transition_idx s T {i, j} \ k", simp) ``` paulson@19954 ` 256` ```apply (simp add: transition_idx_def, blast intro: Least_le) ``` paulson@19954 ` 257` ```done ``` paulson@19954 ` 258` paulson@19954 ` 259` ```lemma transition_idx_in: ``` paulson@19954 ` 260` ``` "[|i T k|] ==> (s j, s i) \ T (transition_idx s T {i,j})" ``` paulson@19954 ` 261` ```apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR ``` paulson@19954 ` 262` ``` cong: conj_cong) ``` paulson@19954 ` 263` ```apply (erule LeastI) ``` paulson@19954 ` 264` ```done ``` paulson@19954 ` 265` paulson@19954 ` 266` ```text{*To be equal to the union of some well-founded relations is equivalent ``` paulson@19954 ` 267` ```to being the subset of such a union.*} ``` paulson@19954 ` 268` ```lemma disj_wf: ``` paulson@19954 ` 269` ``` "disj_wf(r) = (\T. \n::nat. (\i (\is. \i. (s (Suc i), s i) \ r" ``` paulson@19954 ` 282` ``` then obtain s where sSuc: "\i. (s (Suc i), s i) \ r" .. ``` paulson@19954 ` 283` ``` have s: "!!i j. i < j ==> (s j, s i) \ r" ``` paulson@19954 ` 284` ``` proof - ``` paulson@19954 ` 285` ``` fix i and j::nat ``` paulson@19954 ` 286` ``` assume less: "i r" ``` paulson@19954 ` 288` ``` proof (rule less_Suc_induct) ``` paulson@19954 ` 289` ``` show "\i. (s (Suc i), s i) \ r" by (simp add: sSuc) ``` paulson@19954 ` 290` ``` show "\i j k. \(s j, s i) \ r; (s k, s j) \ r\ \ (s k, s i) \ r" ``` paulson@19954 ` 291` ``` using transr by (unfold trans_def, blast) ``` paulson@19954 ` 292` ``` qed ``` paulson@19954 ` 293` ``` qed ``` paulson@19954 ` 294` ``` from dwf ``` paulson@19954 ` 295` ``` obtain T and n::nat where wfT: "\kki j. i \k. (s j, s i) \ T k & k r" by (rule s [of i j]) ``` paulson@19954 ` 302` ``` thus "\k. (s j, s i) \ T k & kj ==> transition_idx s T {i,j} < n" ``` paulson@19954 ` 305` ``` apply (auto simp add: linorder_neq_iff) ``` paulson@19954 ` 306` ``` apply (blast dest: s_in_T transition_idx_less) ``` paulson@19954 ` 307` ``` apply (subst insert_commute) ``` paulson@19954 ` 308` ``` apply (blast dest: s_in_T transition_idx_less) ``` paulson@19954 ` 309` ``` done ``` paulson@19954 ` 310` ``` have ``` paulson@19954 ` 311` ``` "\K k. K \ UNIV & infinite K & k < n & ``` paulson@19954 ` 312` ``` (\i\K. \j\K. i\j --> transition_idx s T {i,j} = k)" ``` paulson@19954 ` 313` ``` by (rule Ramsey2) (auto intro: trless nat_infinite) ``` paulson@19954 ` 314` ``` then obtain K and k ``` paulson@19954 ` 315` ``` where infK: "infinite K" and less: "k < n" and ``` paulson@19954 ` 316` ``` allk: "\i\K. \j\K. i\j --> transition_idx s T {i,j} = k" ``` paulson@19954 ` 317` ``` by auto ``` paulson@19954 ` 318` ``` have "\m. (s (enumerate K (Suc m)), s(enumerate K m)) \ T k" ``` paulson@19954 ` 319` ``` proof ``` paulson@19954 ` 320` ``` fix m::nat ``` paulson@19954 ` 321` ``` let ?j = "enumerate K (Suc m)" ``` paulson@19954 ` 322` ``` let ?i = "enumerate K m" ``` paulson@19954 ` 323` ``` have jK: "?j \ K" by (simp add: enumerate_in_set infK) ``` paulson@19954 ` 324` ``` have iK: "?i \ K" by (simp add: enumerate_in_set infK) ``` paulson@19954 ` 325` ``` have ij: "?i < ?j" by (simp add: enumerate_step infK) ``` paulson@19954 ` 326` ``` have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij ``` paulson@19954 ` 327` ``` by (simp add: allk) ``` paulson@19954 ` 328` ``` obtain k' where "(s ?j, s ?i) \ T k'" "k' T k" ``` paulson@19954 ` 331` ``` by (simp add: ijk [symmetric] transition_idx_in ij) ``` paulson@19954 ` 332` ``` qed ``` paulson@19954 ` 333` ``` hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain) ``` paulson@19954 ` 334` ``` thus False using wfT less by blast ``` paulson@19954 ` 335` ```qed ``` paulson@19954 ` 336` paulson@19944 ` 337` ```end ```