1.1 --- a/src/HOL/Library/Function_Algebras.thy Tue Feb 21 16:42:57 2012 +0100
1.2 +++ b/src/HOL/Library/Function_Algebras.thy Tue Feb 21 16:48:10 2012 +0100
1.3 @@ -13,9 +13,7 @@
1.4 instantiation "fun" :: (type, plus) plus
1.5 begin
1.6
1.7 -definition
1.8 - "f + g = (\<lambda>x. f x + g x)"
1.9 -
1.10 +definition "f + g = (\<lambda>x. f x + g x)"
1.11 instance ..
1.12
1.13 end
1.14 @@ -23,9 +21,7 @@
1.15 instantiation "fun" :: (type, zero) zero
1.16 begin
1.17
1.18 -definition
1.19 - "0 = (\<lambda>x. 0)"
1.20 -
1.21 +definition "0 = (\<lambda>x. 0)"
1.22 instance ..
1.23
1.24 end
1.25 @@ -33,9 +29,7 @@
1.26 instantiation "fun" :: (type, times) times
1.27 begin
1.28
1.29 -definition
1.30 - "f * g = (\<lambda>x. f x * g x)"
1.31 -
1.32 +definition "f * g = (\<lambda>x. f x * g x)"
1.33 instance ..
1.34
1.35 end
1.36 @@ -43,9 +37,7 @@
1.37 instantiation "fun" :: (type, one) one
1.38 begin
1.39
1.40 -definition
1.41 - "1 = (\<lambda>x. 1)"
1.42 -
1.43 +definition "1 = (\<lambda>x. 1)"
1.44 instance ..
1.45
1.46 end
1.47 @@ -53,69 +45,70 @@
1.48
1.49 text {* Additive structures *}
1.50
1.51 -instance "fun" :: (type, semigroup_add) semigroup_add proof
1.52 -qed (simp add: plus_fun_def add.assoc)
1.53 +instance "fun" :: (type, semigroup_add) semigroup_add
1.54 + by default (simp add: plus_fun_def add.assoc)
1.55
1.56 -instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
1.57 -qed (simp_all add: plus_fun_def fun_eq_iff)
1.58 +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
1.59 + by default (simp_all add: plus_fun_def fun_eq_iff)
1.60
1.61 -instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
1.62 -qed (simp add: plus_fun_def add.commute)
1.63 +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
1.64 + by default (simp add: plus_fun_def add.commute)
1.65
1.66 -instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
1.67 -qed simp
1.68 +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
1.69 + by default simp
1.70
1.71 -instance "fun" :: (type, monoid_add) monoid_add proof
1.72 -qed (simp_all add: plus_fun_def zero_fun_def)
1.73 +instance "fun" :: (type, monoid_add) monoid_add
1.74 + by default (simp_all add: plus_fun_def zero_fun_def)
1.75
1.76 -instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
1.77 -qed simp
1.78 +instance "fun" :: (type, comm_monoid_add) comm_monoid_add
1.79 + by default simp
1.80
1.81 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
1.82
1.83 -instance "fun" :: (type, group_add) group_add proof
1.84 -qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
1.85 +instance "fun" :: (type, group_add) group_add
1.86 + by default
1.87 + (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
1.88
1.89 -instance "fun" :: (type, ab_group_add) ab_group_add proof
1.90 -qed (simp_all add: diff_minus)
1.91 +instance "fun" :: (type, ab_group_add) ab_group_add
1.92 + by default (simp_all add: diff_minus)
1.93
1.94
1.95 text {* Multiplicative structures *}
1.96
1.97 -instance "fun" :: (type, semigroup_mult) semigroup_mult proof
1.98 -qed (simp add: times_fun_def mult.assoc)
1.99 +instance "fun" :: (type, semigroup_mult) semigroup_mult
1.100 + by default (simp add: times_fun_def mult.assoc)
1.101
1.102 -instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
1.103 -qed (simp add: times_fun_def mult.commute)
1.104 +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
1.105 + by default (simp add: times_fun_def mult.commute)
1.106
1.107 -instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
1.108 -qed (simp add: times_fun_def)
1.109 +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
1.110 + by default (simp add: times_fun_def)
1.111
1.112 -instance "fun" :: (type, monoid_mult) monoid_mult proof
1.113 -qed (simp_all add: times_fun_def one_fun_def)
1.114 +instance "fun" :: (type, monoid_mult) monoid_mult
1.115 + by default (simp_all add: times_fun_def one_fun_def)
1.116
1.117 -instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
1.118 -qed simp
1.119 +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
1.120 + by default simp
1.121
1.122
1.123 text {* Misc *}
1.124
1.125 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
1.126
1.127 -instance "fun" :: (type, mult_zero) mult_zero proof
1.128 -qed (simp_all add: zero_fun_def times_fun_def)
1.129 +instance "fun" :: (type, mult_zero) mult_zero
1.130 + by default (simp_all add: zero_fun_def times_fun_def)
1.131
1.132 -instance "fun" :: (type, zero_neq_one) zero_neq_one proof
1.133 -qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
1.134 +instance "fun" :: (type, zero_neq_one) zero_neq_one
1.135 + by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
1.136
1.137
1.138 text {* Ring structures *}
1.139
1.140 -instance "fun" :: (type, semiring) semiring proof
1.141 -qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
1.142 +instance "fun" :: (type, semiring) semiring
1.143 + by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
1.144
1.145 -instance "fun" :: (type, comm_semiring) comm_semiring proof
1.146 -qed (simp add: plus_fun_def times_fun_def algebra_simps)
1.147 +instance "fun" :: (type, comm_semiring) comm_semiring
1.148 + by default (simp add: plus_fun_def times_fun_def algebra_simps)
1.149
1.150 instance "fun" :: (type, semiring_0) semiring_0 ..
1.151
1.152 @@ -127,8 +120,7 @@
1.153
1.154 instance "fun" :: (type, semiring_1) semiring_1 ..
1.155
1.156 -lemma of_nat_fun:
1.157 - shows "of_nat n = (\<lambda>x::'a. of_nat n)"
1.158 +lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
1.159 proof -
1.160 have comp: "comp = (\<lambda>f g x. f (g x))"
1.161 by (rule ext)+ simp
1.162 @@ -147,7 +139,8 @@
1.163
1.164 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
1.165
1.166 -instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
1.167 +instance "fun" :: (type, semiring_char_0) semiring_char_0
1.168 +proof
1.169 from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
1.170 by (rule inj_fun)
1.171 then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
1.172 @@ -168,23 +161,24 @@
1.173
1.174 text {* Ordereded structures *}
1.175
1.176 -instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
1.177 -qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
1.178 +instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
1.179 + by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
1.180
1.181 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
1.182
1.183 -instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
1.184 -qed (simp add: plus_fun_def le_fun_def)
1.185 +instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
1.186 + by default (simp add: plus_fun_def le_fun_def)
1.187
1.188 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
1.189
1.190 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
1.191
1.192 -instance "fun" :: (type, ordered_semiring) ordered_semiring proof
1.193 -qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
1.194 +instance "fun" :: (type, ordered_semiring) ordered_semiring
1.195 + by default
1.196 + (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
1.197
1.198 -instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
1.199 -qed (fact mult_left_mono)
1.200 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
1.201 + by default (fact mult_left_mono)
1.202
1.203 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
1.204
2.1 --- a/src/HOL/Library/Ramsey.thy Tue Feb 21 16:42:57 2012 +0100
2.2 +++ b/src/HOL/Library/Ramsey.thy Tue Feb 21 16:48:10 2012 +0100
2.3 @@ -47,11 +47,11 @@
2.4 qed
2.5 } moreover
2.6 { assume "m\<noteq>0" "n\<noteq>0"
2.7 - hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
2.8 - from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
2.9 + then have "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
2.10 + from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
2.11 obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
2.12 by auto
2.13 - hence "r1+r2 \<ge> 1" by arith
2.14 + then have "r1+r2 \<ge> 1" by arith
2.15 moreover
2.16 have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
2.17 proof clarify
2.18 @@ -62,12 +62,12 @@
2.19 let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
2.20 let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
2.21 have "V = insert v (?M \<union> ?N)" using `v : V` by auto
2.22 - hence "card V = card(insert v (?M \<union> ?N))" by metis
2.23 + then have "card V = card(insert v (?M \<union> ?N))" by metis
2.24 also have "\<dots> = card ?M + card ?N + 1" using `finite V`
2.25 by(fastforce intro: card_Un_disjoint)
2.26 finally have "card V = card ?M + card ?N + 1" .
2.27 - hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
2.28 - hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
2.29 + then have "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
2.30 + then have "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
2.31 moreover
2.32 { assume "r1 \<le> card ?M"
2.33 moreover have "finite ?M" using `finite V` by auto
2.34 @@ -82,7 +82,7 @@
2.35 with `R <= V` have "?EX V E m n" by blast
2.36 } moreover
2.37 { assume "?C"
2.38 - hence "clique (insert v R) E" using `R <= ?M`
2.39 + then have "clique (insert v R) E" using `R <= ?M`
2.40 by(auto simp:clique_def insert_commute)
2.41 moreover have "card(insert v R) = m"
2.42 using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
2.43 @@ -102,7 +102,7 @@
2.44 with `R <= V` have "?EX V E m n" by blast
2.45 } moreover
2.46 { assume "?I"
2.47 - hence "indep (insert v R) E" using `R <= ?N`
2.48 + then have "indep (insert v R) E" using `R <= ?N`
2.49 by(auto simp:indep_def insert_commute)
2.50 moreover have "card(insert v R) = n"
2.51 using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
2.52 @@ -124,17 +124,17 @@
2.53 choice_0: "choice P r 0 = (SOME x. P x)"
2.54 | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
2.55
2.56 -lemma choice_n:
2.57 +lemma choice_n:
2.58 assumes P0: "P x0"
2.59 and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
2.60 shows "P (choice P r n)"
2.61 proof (induct n)
2.62 - case 0 show ?case by (force intro: someI P0)
2.63 + case 0 show ?case by (force intro: someI P0)
2.64 next
2.65 - case Suc thus ?case by (auto intro: someI2_ex [OF Pstep])
2.66 + case Suc then show ?case by (auto intro: someI2_ex [OF Pstep])
2.67 qed
2.68
2.69 -lemma dependent_choice:
2.70 +lemma dependent_choice:
2.71 assumes trans: "trans r"
2.72 and P0: "P x0"
2.73 and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
2.74 @@ -144,7 +144,7 @@
2.75 fix n
2.76 show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
2.77 next
2.78 - have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
2.79 + have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
2.80 using Pstep [OF choice_n [OF P0 Pstep]]
2.81 by (auto intro: someI2_ex)
2.82 fix n m :: nat
2.83 @@ -156,8 +156,7 @@
2.84
2.85 subsubsection {* Partitions of a Set *}
2.86
2.87 -definition
2.88 - part :: "nat => nat => 'a set => ('a set => nat) => bool"
2.89 +definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
2.90 --{*the function @{term f} partitions the @{term r}-subsets of the typically
2.91 infinite set @{term Y} into @{term s} distinct categories.*}
2.92 where
2.93 @@ -165,52 +164,52 @@
2.94
2.95 text{*For induction, we decrease the value of @{term r} in partitions.*}
2.96 lemma part_Suc_imp_part:
2.97 - "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
2.98 + "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
2.99 ==> part r s (Y - {y}) (%u. f (insert y u))"
2.100 apply(simp add: part_def, clarify)
2.101 apply(drule_tac x="insert y X" in spec)
2.102 apply(force)
2.103 done
2.104
2.105 -lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
2.106 +lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
2.107 unfolding part_def by blast
2.108 -
2.109 +
2.110
2.111 subsection {* Ramsey's Theorem: Infinitary Version *}
2.112
2.113 -lemma Ramsey_induction:
2.114 +lemma Ramsey_induction:
2.115 fixes s and r::nat
2.116 shows
2.117 - "!!(YY::'a set) (f::'a set => nat).
2.118 + "!!(YY::'a set) (f::'a set => nat).
2.119 [|infinite YY; part r s YY f|]
2.120 - ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
2.121 + ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
2.122 (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
2.123 proof (induct r)
2.124 case 0
2.125 - thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
2.126 + then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
2.127 next
2.128 - case (Suc r)
2.129 + case (Suc r)
2.130 show ?case
2.131 proof -
2.132 from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
2.133 let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
2.134 - let ?propr = "%(y,Y,t).
2.135 + let ?propr = "%(y,Y,t).
2.136 y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
2.137 & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
2.138 have infYY': "infinite (YY-{yy})" using Suc.prems by auto
2.139 have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
2.140 by (simp add: o_def part_Suc_imp_part yy Suc.prems)
2.141 - have transr: "trans ?ramr" by (force simp add: trans_def)
2.142 + have transr: "trans ?ramr" by (force simp add: trans_def)
2.143 from Suc.hyps [OF infYY' partf']
2.144 obtain Y0 and t0
2.145 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
2.146 "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
2.147 - by blast
2.148 + by blast
2.149 with yy have propr0: "?propr(yy,Y0,t0)" by blast
2.150 - have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
2.151 + have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
2.152 proof -
2.153 fix x
2.154 - assume px: "?propr x" thus "?thesis x"
2.155 + assume px: "?propr x" then show "?thesis x"
2.156 proof (cases x)
2.157 case (fields yx Yx tx)
2.158 then obtain yx' where yx': "yx' \<in> Yx" using px
2.159 @@ -223,7 +222,7 @@
2.160 obtain Y' and t'
2.161 where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
2.162 "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
2.163 - by blast
2.164 + by blast
2.165 show ?thesis
2.166 proof
2.167 show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
2.168 @@ -258,51 +257,51 @@
2.169 show ?thesis
2.170 proof (intro exI conjI)
2.171 show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
2.172 - by (auto simp add: Let_def split_beta)
2.173 + by (auto simp add: Let_def split_beta)
2.174 show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
2.175 - by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
2.176 + by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
2.177 show "s' < s" by (rule less')
2.178 - show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
2.179 + show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
2.180 --> f X = s'"
2.181 proof -
2.182 - {fix X
2.183 + {fix X
2.184 assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
2.185 and cardX: "finite X" "card X = Suc r"
2.186 - then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
2.187 - by (auto simp add: subset_image_iff)
2.188 + then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
2.189 + by (auto simp add: subset_image_iff)
2.190 with cardX have "AA\<noteq>{}" by auto
2.191 - hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
2.192 + then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
2.193 have "f X = s'"
2.194 - proof (cases "g (LEAST x. x \<in> AA)")
2.195 + proof (cases "g (LEAST x. x \<in> AA)")
2.196 case (fields ya Ya ta)
2.197 - with AAleast Xeq
2.198 - have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
2.199 - hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
2.200 - also have "... = ta"
2.201 + with AAleast Xeq
2.202 + have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
2.203 + then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
2.204 + also have "... = ta"
2.205 proof -
2.206 have "X - {ya} \<subseteq> Ya"
2.207 - proof
2.208 + proof
2.209 fix x assume x: "x \<in> X - {ya}"
2.210 - then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
2.211 - by (auto simp add: Xeq)
2.212 - hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
2.213 - hence lessa': "(LEAST x. x \<in> AA) < a'"
2.214 + then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
2.215 + by (auto simp add: Xeq)
2.216 + then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
2.217 + then have lessa': "(LEAST x. x \<in> AA) < a'"
2.218 using Least_le [of "%x. x \<in> AA", OF a'] by arith
2.219 show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
2.220 qed
2.221 moreover
2.222 have "card (X - {ya}) = r"
2.223 by (simp add: cardX ya)
2.224 - ultimately show ?thesis
2.225 + ultimately show ?thesis
2.226 using pg [of "LEAST x. x \<in> AA"] fields cardX
2.227 by (clarsimp simp del:insert_Diff_single)
2.228 qed
2.229 also have "... = s'" using AA AAleast fields by auto
2.230 finally show ?thesis .
2.231 qed}
2.232 - thus ?thesis by blast
2.233 - qed
2.234 - qed
2.235 + then show ?thesis by blast
2.236 + qed
2.237 + qed
2.238 qed
2.239 qed
2.240
2.241 @@ -312,7 +311,7 @@
2.242 shows
2.243 "[|infinite Z;
2.244 \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
2.245 - ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
2.246 + ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
2.247 & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
2.248 by (blast intro: Ramsey_induction [unfolded part_def])
2.249
2.250 @@ -326,7 +325,7 @@
2.251 proof -
2.252 have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
2.253 using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
2.254 - obtain Y t
2.255 + obtain Y t
2.256 where "Y \<subseteq> Z" "infinite Y" "t < s"
2.257 "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
2.258 by (insert Ramsey [OF infZ part2]) auto
2.259 @@ -342,39 +341,36 @@
2.260 \cite{Podelski-Rybalchenko}.
2.261 *}
2.262
2.263 -definition
2.264 - disj_wf :: "('a * 'a)set => bool"
2.265 -where
2.266 - "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
2.267 +definition disj_wf :: "('a * 'a)set => bool"
2.268 + where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
2.269
2.270 -definition
2.271 - transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
2.272 -where
2.273 - "transition_idx s T A =
2.274 - (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
2.275 +definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
2.276 + where
2.277 + "transition_idx s T A =
2.278 + (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
2.279
2.280
2.281 lemma transition_idx_less:
2.282 "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
2.283 -apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
2.284 -apply (simp add: transition_idx_def, blast intro: Least_le)
2.285 +apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
2.286 +apply (simp add: transition_idx_def, blast intro: Least_le)
2.287 done
2.288
2.289 lemma transition_idx_in:
2.290 "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
2.291 -apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
2.292 - cong: conj_cong)
2.293 -apply (erule LeastI)
2.294 +apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
2.295 + cong: conj_cong)
2.296 +apply (erule LeastI)
2.297 done
2.298
2.299 text{*To be equal to the union of some well-founded relations is equivalent
2.300 to being the subset of such a union.*}
2.301 lemma disj_wf:
2.302 "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
2.303 -apply (auto simp add: disj_wf_def)
2.304 -apply (rule_tac x="%i. T i Int r" in exI)
2.305 -apply (rule_tac x=n in exI)
2.306 -apply (force simp add: wf_Int1)
2.307 +apply (auto simp add: disj_wf_def)
2.308 +apply (rule_tac x="%i. T i Int r" in exI)
2.309 +apply (rule_tac x=n in exI)
2.310 +apply (force simp add: wf_Int1)
2.311 done
2.312
2.313 theorem trans_disj_wf_implies_wf:
2.314 @@ -388,13 +384,13 @@
2.315 proof -
2.316 fix i and j::nat
2.317 assume less: "i<j"
2.318 - thus "(s j, s i) \<in> r"
2.319 + then show "(s j, s i) \<in> r"
2.320 proof (rule less_Suc_induct)
2.321 - show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
2.322 + show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
2.323 show "\<And>i j k. \<lbrakk>(s j, s i) \<in> r; (s k, s j) \<in> r\<rbrakk> \<Longrightarrow> (s k, s i) \<in> r"
2.324 - using transr by (unfold trans_def, blast)
2.325 + using transr by (unfold trans_def, blast)
2.326 qed
2.327 - qed
2.328 + qed
2.329 from dwf
2.330 obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
2.331 by (auto simp add: disj_wf_def)
2.332 @@ -402,20 +398,20 @@
2.333 proof -
2.334 fix i and j::nat
2.335 assume less: "i<j"
2.336 - hence "(s j, s i) \<in> r" by (rule s [of i j])
2.337 - thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
2.338 - qed
2.339 + then have "(s j, s i) \<in> r" by (rule s [of i j])
2.340 + then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
2.341 + qed
2.342 have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
2.343 apply (auto simp add: linorder_neq_iff)
2.344 - apply (blast dest: s_in_T transition_idx_less)
2.345 - apply (subst insert_commute)
2.346 - apply (blast dest: s_in_T transition_idx_less)
2.347 + apply (blast dest: s_in_T transition_idx_less)
2.348 + apply (subst insert_commute)
2.349 + apply (blast dest: s_in_T transition_idx_less)
2.350 done
2.351 have
2.352 - "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
2.353 + "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
2.354 (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
2.355 - by (rule Ramsey2) (auto intro: trless nat_infinite)
2.356 - then obtain K and k
2.357 + by (rule Ramsey2) (auto intro: trless nat_infinite)
2.358 + then obtain K and k
2.359 where infK: "infinite K" and less: "k < n" and
2.360 allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
2.361 by auto
2.362 @@ -424,18 +420,18 @@
2.363 fix m::nat
2.364 let ?j = "enumerate K (Suc m)"
2.365 let ?i = "enumerate K m"
2.366 - have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
2.367 - have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
2.368 - have ij: "?i < ?j" by (simp add: enumerate_step infK)
2.369 - have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
2.370 + have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
2.371 + have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
2.372 + have ij: "?i < ?j" by (simp add: enumerate_step infK)
2.373 + have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
2.374 by (simp add: allk)
2.375 - obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
2.376 + obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
2.377 using s_in_T [OF ij] by blast
2.378 - thus "(s ?j, s ?i) \<in> T k"
2.379 - by (simp add: ijk [symmetric] transition_idx_in ij)
2.380 + then show "(s ?j, s ?i) \<in> T k"
2.381 + by (simp add: ijk [symmetric] transition_idx_in ij)
2.382 qed
2.383 - hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
2.384 - thus False using wfT less by blast
2.385 + then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
2.386 + then show False using wfT less by blast
2.387 qed
2.388
2.389 end