src/HOL/Library/Ramsey.thy
changeset 21634 369e38e35686
parent 20810 3377a830b727
child 22367 6860f09242bf
     1.1 --- a/src/HOL/Library/Ramsey.thy	Mon Dec 04 00:06:59 2006 +0100
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Mon Dec 04 15:15:09 2006 +0100
     1.3 @@ -56,6 +56,7 @@
     1.4    part :: "nat => nat => 'a set => ('a set => nat) => bool"
     1.5    --{*the function @{term f} partitions the @{term r}-subsets of the typically
     1.6         infinite set @{term Y} into @{term s} distinct categories.*}
     1.7 +where
     1.8    "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
     1.9  
    1.10  text{*For induction, we decrease the value of @{term r} in partitions.*}
    1.11 @@ -242,9 +243,12 @@
    1.12  
    1.13  definition
    1.14    disj_wf         :: "('a * 'a)set => bool"
    1.15 +where
    1.16    "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
    1.17  
    1.18 +definition
    1.19    transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
    1.20 +where
    1.21    "transition_idx s T A =
    1.22      (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
    1.23