src/HOL/Library/Ramsey.thy
changeset 19946 e3ddb0812840
parent 19944 60e0cbeae3d8
child 19948 1be283f3f1ba
     1.1 --- a/src/HOL/Library/Ramsey.thy	Fri Jun 23 10:48:34 2006 +0200
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Jun 23 13:42:19 2006 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4   proof (induct n)
     1.5     case 0 show ?case by (force intro: someI P0) 
     1.6   next
     1.7 -   case (Suc n) thus ?case by (auto intro: someI2_ex [OF Pstep]) 
     1.8 +   case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) 
     1.9   qed
    1.10  
    1.11  lemma dependent_choice: 
    1.12 @@ -125,10 +125,8 @@
    1.13        qed
    1.14      qed
    1.15      from dependent_choice [OF transr propr0 proprstep]
    1.16 -    obtain g where "(\<forall>n::nat. ?propr(g n)) & (\<forall>n m. n<m -->(g n, g m) \<in> ?ramr)"
    1.17 -      .. --{*for some reason, can't derive the following directly from dc*}
    1.18 -    hence pg: "!!n.  ?propr (g n)"
    1.19 -      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by auto
    1.20 +    obtain g where pg: "!!n::nat.  ?propr (g n)"
    1.21 +      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by force
    1.22      let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"
    1.23      let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"
    1.24      have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    1.25 @@ -195,7 +193,7 @@
    1.26                 by (simp add: card_Diff_singleton_if cardX ya)
    1.27               ultimately show ?thesis 
    1.28                 using pg [of "LEAST x. x \<in> AA"] fields cardX
    1.29 -               by (clarify, drule_tac x="X-{ya}" in spec, simp)
    1.30 +	       by (clarsimp simp del:insert_Diff_single)
    1.31             qed
    1.32             also have "... = s'" using AA AAleast fields by auto
    1.33             finally show ?thesis .
    1.34 @@ -215,7 +213,7 @@
    1.35        \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
    1.36    ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s 
    1.37              & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
    1.38 -by (blast intro: ramsey_induction [unfolded part_def, rule_format]) 
    1.39 +by (blast intro: ramsey_induction [unfolded part_def]) 
    1.40  
    1.41  end
    1.42