author wenzelm Sat Jun 24 22:25:31 2006 +0200 (2006-06-24) changeset 19948 1be283f3f1ba parent 19947 29b376397cd5 child 19949 0505dce27b0b
minor tuning of definitions/proofs;
```     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 -
```