src/HOL/Library/Ramsey.thy
 changeset 19946 e3ddb0812840 parent 19944 60e0cbeae3d8 child 19948 1be283f3f1ba
equal inserted replaced
19945:ed388c5c7e54 19946:e3ddb0812840
`    23       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"`
`    23       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"`
`    24   shows "P (choice P r n)"`
`    24   shows "P (choice P r n)"`
`    25  proof (induct n)`
`    25  proof (induct n)`
`    26    case 0 show ?case by (force intro: someI P0) `
`    26    case 0 show ?case by (force intro: someI P0) `
`    27  next`
`    27  next`
`    28    case (Suc n) thus ?case by (auto intro: someI2_ex [OF Pstep]) `
`    28    case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) `
`    29  qed`
`    29  qed`
`    30 `
`    30 `
`    31 lemma dependent_choice: `
`    31 lemma dependent_choice: `
`    32   assumes trans: "trans r"`
`    32   assumes trans: "trans r"`
`    33       and P0: "P x0"`
`    33       and P0: "P x0"`
`   123   	    using fields Y' yx' px by blast`
`   123   	    using fields Y' yx' px by blast`
`   124 	qed`
`   124 	qed`
`   125       qed`
`   125       qed`
`   126     qed`
`   126     qed`
`   127     from dependent_choice [OF transr propr0 proprstep]`
`   127     from dependent_choice [OF transr propr0 proprstep]`
`   128     obtain g where "(\<forall>n::nat. ?propr(g n)) & (\<forall>n m. n<m -->(g n, g m) \<in> ?ramr)"`
`   128     obtain g where pg: "!!n::nat.  ?propr (g n)"`
`   129       .. --{*for some reason, can't derive the following directly from dc*}`
`   129       and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by force`
`   130     hence pg: "!!n.  ?propr (g n)"`
`       `
`   131       and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by auto`
`       `
`   132     let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"`
`   130     let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"`
`   133     let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"`
`   131     let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"`
`   134     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"`
`   132     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"`
`   135     proof (intro exI subsetI)`
`   133     proof (intro exI subsetI)`
`   136       fix x`
`   134       fix x`
`   193              moreover`
`   191              moreover`
`   194              have "card (X - {ya}) = r"`
`   192              have "card (X - {ya}) = r"`
`   195                by (simp add: card_Diff_singleton_if cardX ya)`
`   193                by (simp add: card_Diff_singleton_if cardX ya)`
`   196              ultimately show ?thesis `
`   194              ultimately show ?thesis `
`   197                using pg [of "LEAST x. x \<in> AA"] fields cardX`
`   195                using pg [of "LEAST x. x \<in> AA"] fields cardX`
`   198                by (clarify, drule_tac x="X-{ya}" in spec, simp)`
`   196 	       by (clarsimp simp del:insert_Diff_single)`
`   199            qed`
`   197            qed`
`   200            also have "... = s'" using AA AAleast fields by auto`
`   198            also have "... = s'" using AA AAleast fields by auto`
`   201            finally show ?thesis .`
`   199            finally show ?thesis .`
`   202          qed}`
`   200          qed}`
`   203         thus ?thesis by blast`
`   201         thus ?thesis by blast`
`   213   shows`
`   211   shows`
`   214    "[|infinite Z;`
`   212    "[|infinite Z;`
`   215       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]`
`   213       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]`
`   216   ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s `
`   214   ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s `
`   217             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"`
`   215             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"`
`   218 by (blast intro: ramsey_induction [unfolded part_def, rule_format]) `
`   216 by (blast intro: ramsey_induction [unfolded part_def]) `
`   219 `
`   217 `
`   220 end`
`   218 end`
`   221 `
`   219 `