misc tuning;
authorwenzelm
Tue Feb 21 16:48:10 2012 +0100 (2012-02-21)
changeset 46575f1e387195a56
parent 46574 41701fce8ac7
child 46576 ae9286f64574
misc tuning;
more indentation;
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Ramsey.thy
     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