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.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:
```