src/HOL/Library/Ramsey.thy
changeset 20810 3377a830b727
parent 19954 e4c9f6946db3
child 21634 369e38e35686
     1.1 --- a/src/HOL/Library/Ramsey.thy	Sun Oct 01 18:29:26 2006 +0200
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Sun Oct 01 18:29:28 2006 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header "Ramsey's Theorem"
     1.6  
     1.7 -theory Ramsey imports Main begin
     1.8 +theory Ramsey imports Main Infinite_Set begin
     1.9  
    1.10  
    1.11  subsection{*Preliminaries*}
    1.12 @@ -138,13 +138,12 @@
    1.13        then obtain n where "x = ?gt n" ..
    1.14        with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
    1.15      qed
    1.16 -    have "\<exists>s' \<in> range ?gt. infinite (?gt -` {s'})" 
    1.17 -     by (rule inf_img_fin_dom [OF _ nat_infinite]) 
    1.18 -        (simp add: finite_nat_iff_bounded rangeg)
    1.19 +    have "finite (range ?gt)"
    1.20 +      by (simp add: finite_nat_iff_bounded rangeg)
    1.21      then obtain s' and n'
    1.22 -            where s':      "s' = ?gt n'"
    1.23 -              and infeqs': "infinite {n. ?gt n = s'}"
    1.24 -       by (auto simp add: vimage_def)
    1.25 +      where s': "s' = ?gt n'"
    1.26 +        and infeqs': "infinite {n. ?gt n = s'}"
    1.27 +      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
    1.28      with pg [of n'] have less': "s'<s" by (cases "g n'") auto
    1.29      have inj_gy: "inj ?gy"
    1.30      proof (rule linorder_injI)
    1.31 @@ -241,13 +240,13 @@
    1.32  IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004).
    1.33  *}
    1.34  
    1.35 -constdefs
    1.36 +definition
    1.37    disj_wf         :: "('a * 'a)set => bool"
    1.38 -  "disj_wf(r) == \<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i)"
    1.39 +  "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
    1.40  
    1.41    transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
    1.42 -  "transition_idx s T A ==
    1.43 -     LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k"
    1.44 +  "transition_idx s T A =
    1.45 +    (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
    1.46  
    1.47  
    1.48  lemma transition_idx_less: