src/HOL/Library/Ramsey.thy
changeset 19946 e3ddb0812840
parent 19944 60e0cbeae3d8
child 19948 1be283f3f1ba
equal deleted 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