# HG changeset patch # User wenzelm # Date 1151180731 -7200 # Node ID 1be283f3f1baaca4ae2904fc98008b608684e7bf # Parent 29b376397cd54be3bba1a35a8b55f1bb1f4c4409 minor tuning of definitions/proofs; diff -r 29b376397cd5 -r 1be283f3f1ba src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Sat Jun 24 22:25:30 2006 +0200 +++ b/src/HOL/Library/Ramsey.thy Sat Jun 24 22:25:31 2006 +0200 @@ -10,7 +10,7 @@ subsection{*``Axiom'' of Dependent Choice*} -consts choice :: "('a => bool) => (('a * 'a) set) => nat => 'a" +consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a" --{*An integer-indexed chain of choices*} primrec choice_0: "choice P r 0 = (SOME x. P x)" @@ -22,11 +22,11 @@ assumes P0: "P x0" and Pstep: "!!x. P x ==> \y. P y & (x,y) \ r" shows "P (choice P r n)" - proof (induct n) - case 0 show ?case by (force intro: someI P0) - next - case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) - qed +proof (induct n) + case 0 show ?case by (force intro: someI P0) +next + case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) +qed lemma dependent_choice: assumes trans: "trans r" @@ -51,10 +51,11 @@ subsection {*Partitions of a Set*} -constdefs part :: "nat => nat => 'a set => ('a set => nat) => bool" +definition + part :: "nat => nat => 'a set => ('a set => nat) => bool" --{*the function @{term f} partitions the @{term r}-subsets of the typically infinite set @{term Y} into @{term s} distinct categories.*} - "part r s Y f == \X. X \ Y & finite X & card X = r --> f X < s" + "part r s Y f = (\X. X \ Y & finite X & card X = r --> f X < s)" text{*For induction, we decrease the value of @{term r} in partitions.*} lemma part_Suc_imp_part: @@ -66,7 +67,7 @@ done lemma part_subset: "part r s YY f ==> Y \ YY ==> part r s Y f" - by (simp add: part_def, blast) + unfolding part_def by blast subsection {*Ramsey's Theorem: Infinitary Version*} @@ -147,18 +148,15 @@ have inj_gy: "inj ?gy" proof (rule linorder_injI) fix m and m'::nat assume less: "m < m'" show "?gy m \ ?gy m'" - using rg [OF less] pg [of m] by (cases "g m", cases "g m'", auto) + using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto qed show ?thesis proof (intro exI conjI) show "?gy ` {n. ?gt n = s'} \ YY" using pg by (auto simp add: Let_def split_beta) - next show "infinite (?gy ` {n. ?gt n = s'})" using infeqs' by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) - next show "s' < s" by (rule less') - next show "\X. X \ ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r --> f X = s'" proof - @@ -216,4 +214,3 @@ by (blast intro: ramsey_induction [unfolded part_def]) end -