minor tuning of definitions/proofs;
authorwenzelm
Sat Jun 24 22:25:31 2006 +0200 (2006-06-24)
changeset 199481be283f3f1ba
parent 19947 29b376397cd5
child 19949 0505dce27b0b
minor tuning of definitions/proofs;
src/HOL/Library/Ramsey.thy
     1.1 --- a/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:25:30 2006 +0200
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Sat Jun 24 22:25:31 2006 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection{*``Axiom'' of Dependent Choice*}
     1.6  
     1.7 -consts choice :: "('a => bool) => (('a * 'a) set) => nat => 'a"
     1.8 +consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
     1.9    --{*An integer-indexed chain of choices*}
    1.10  primrec
    1.11    choice_0:   "choice P r 0 = (SOME x. P x)"
    1.12 @@ -22,11 +22,11 @@
    1.13    assumes P0: "P x0"
    1.14        and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
    1.15    shows "P (choice P r n)"
    1.16 - proof (induct n)
    1.17 -   case 0 show ?case by (force intro: someI P0) 
    1.18 - next
    1.19 -   case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) 
    1.20 - qed
    1.21 +proof (induct n)
    1.22 +  case 0 show ?case by (force intro: someI P0) 
    1.23 +next
    1.24 +  case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) 
    1.25 +qed
    1.26  
    1.27  lemma dependent_choice: 
    1.28    assumes trans: "trans r"
    1.29 @@ -51,10 +51,11 @@
    1.30  
    1.31  subsection {*Partitions of a Set*}
    1.32  
    1.33 -constdefs part :: "nat => nat => 'a set => ('a set => nat) => bool"
    1.34 +definition
    1.35 +  part :: "nat => nat => 'a set => ('a set => nat) => bool"
    1.36    --{*the function @{term f} partitions the @{term r}-subsets of the typically
    1.37         infinite set @{term Y} into @{term s} distinct categories.*}
    1.38 -  "part r s Y f == \<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s"
    1.39 +  "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
    1.40  
    1.41  text{*For induction, we decrease the value of @{term r} in partitions.*}
    1.42  lemma part_Suc_imp_part:
    1.43 @@ -66,7 +67,7 @@
    1.44    done
    1.45  
    1.46  lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f" 
    1.47 -  by (simp add: part_def, blast)
    1.48 +  unfolding part_def by blast
    1.49    
    1.50  
    1.51  subsection {*Ramsey's Theorem: Infinitary Version*}
    1.52 @@ -147,18 +148,15 @@
    1.53      have inj_gy: "inj ?gy"
    1.54      proof (rule linorder_injI)
    1.55        fix m and m'::nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
    1.56 -        using rg [OF less] pg [of m] by (cases "g m", cases "g m'", auto) 
    1.57 +        using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
    1.58      qed
    1.59      show ?thesis
    1.60      proof (intro exI conjI)
    1.61        show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
    1.62          by (auto simp add: Let_def split_beta) 
    1.63 -    next
    1.64        show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
    1.65          by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) 
    1.66 -    next
    1.67        show "s' < s" by (rule less')
    1.68 -    next
    1.69        show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r 
    1.70            --> f X = s'"
    1.71        proof -
    1.72 @@ -216,4 +214,3 @@
    1.73  by (blast intro: ramsey_induction [unfolded part_def]) 
    1.74  
    1.75  end
    1.76 -