src/HOL/Library/Ramsey.thy
changeset 19954 e4c9f6946db3
parent 19949 0505dce27b0b
child 20810 3377a830b727
     1.1 --- a/src/HOL/Library/Ramsey.thy	Tue Jun 27 10:10:20 2006 +0200
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Wed Jun 28 09:27:53 2006 +0200
     1.3 @@ -8,7 +8,9 @@
     1.4  theory Ramsey imports Main begin
     1.5  
     1.6  
     1.7 -subsection{*``Axiom'' of Dependent Choice*}
     1.8 +subsection{*Preliminaries*}
     1.9 +
    1.10 +subsubsection{*``Axiom'' of Dependent Choice*}
    1.11  
    1.12  consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
    1.13    --{*An integer-indexed chain of choices*}
    1.14 @@ -32,24 +34,23 @@
    1.15    assumes trans: "trans r"
    1.16        and P0: "P x0"
    1.17        and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
    1.18 -  shows "\<exists>f::nat=>'a. (\<forall>n. P (f n)) & (\<forall>n m. n<m --> (f n, f m) \<in> r)"
    1.19 -proof (intro exI conjI)
    1.20 -  show "\<forall>n. P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep]) 
    1.21 +  obtains f :: "nat => 'a" where
    1.22 +    "!!n. P (f n)" and "!!n m. n < m ==> (f n, f m) \<in> r"
    1.23 +proof
    1.24 +  fix n
    1.25 +  show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
    1.26  next
    1.27    have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r" 
    1.28      using Pstep [OF choice_n [OF P0 Pstep]]
    1.29      by (auto intro: someI2_ex)
    1.30 -  show "\<forall>n m. n<m --> (choice P r n, choice P r m) \<in> r"
    1.31 -  proof (intro strip)
    1.32 -    fix n m :: nat
    1.33 -    assume less: "n<m"
    1.34 -    show "(choice P r n, choice P r m) \<in> r" using PSuc
    1.35 -      by (auto intro: less_Suc_induct [OF less] transD [OF trans])
    1.36 -  qed
    1.37 -qed 
    1.38 +  fix n m :: nat
    1.39 +  assume less: "n < m"
    1.40 +  show "(choice P r n, choice P r m) \<in> r" using PSuc
    1.41 +    by (auto intro: less_Suc_induct [OF less] transD [OF trans])
    1.42 +qed
    1.43  
    1.44  
    1.45 -subsection {*Partitions of a Set*}
    1.46 +subsubsection {*Partitions of a Set*}
    1.47  
    1.48  definition
    1.49    part :: "nat => nat => 'a set => ('a set => nat) => bool"
    1.50 @@ -72,8 +73,8 @@
    1.51  
    1.52  subsection {*Ramsey's Theorem: Infinitary Version*}
    1.53  
    1.54 -lemma ramsey_induction: 
    1.55 -  fixes s r :: nat
    1.56 +lemma Ramsey_induction: 
    1.57 +  fixes s and r::nat
    1.58    shows
    1.59    "!!(YY::'a set) (f::'a set => nat). 
    1.60        [|infinite YY; part r s YY f|]
    1.61 @@ -127,7 +128,7 @@
    1.62      qed
    1.63      from dependent_choice [OF transr propr0 proprstep]
    1.64      obtain g where pg: "!!n::nat.  ?propr (g n)"
    1.65 -      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by force
    1.66 +      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
    1.67      let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"
    1.68      let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"
    1.69      have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    1.70 @@ -177,8 +178,7 @@
    1.71             proof -
    1.72               have "X - {ya} \<subseteq> Ya"
    1.73               proof 
    1.74 -               fix x
    1.75 -               assume x: "x \<in> X - {ya}"
    1.76 +               fix x assume x: "x \<in> X - {ya}"
    1.77                 then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA" 
    1.78                   by (auto simp add: Xeq) 
    1.79                 hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
    1.80 @@ -203,7 +203,6 @@
    1.81  qed
    1.82  
    1.83  
    1.84 -text{*Repackaging of Tom Ridge's final result*}
    1.85  theorem Ramsey:
    1.86    fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
    1.87    shows
    1.88 @@ -211,6 +210,129 @@
    1.89        \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
    1.90    ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s 
    1.91              & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
    1.92 -by (blast intro: ramsey_induction [unfolded part_def]) 
    1.93 +by (blast intro: Ramsey_induction [unfolded part_def])
    1.94 +
    1.95 +
    1.96 +corollary Ramsey2:
    1.97 +  fixes s::nat and Z::"'a set" and f::"'a set => nat"
    1.98 +  assumes infZ: "infinite Z"
    1.99 +      and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x\<noteq>y --> f{x,y} < s"
   1.100 +  shows
   1.101 +   "\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y --> f{x,y} = t)"
   1.102 +proof -
   1.103 +  have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
   1.104 +    by (auto simp add: numeral_2_eq_2 card_2_eq part) 
   1.105 +  obtain Y t 
   1.106 +    where "Y \<subseteq> Z" "infinite Y" "t < s"
   1.107 +          "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
   1.108 +    by (insert Ramsey [OF infZ part2]) auto
   1.109 +  moreover from this have  "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
   1.110 +  ultimately show ?thesis by iprover
   1.111 +qed
   1.112 +
   1.113 +
   1.114 +
   1.115 +
   1.116 +subsection {*Disjunctive Well-Foundedness*}
   1.117 +
   1.118 +text{*An application of Ramsey's theorem to program termination. See
   1.119 +
   1.120 +Andreas Podelski and Andrey Rybalchenko, Transition Invariants, 19th Annual
   1.121 +IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004).
   1.122 +*}
   1.123 +
   1.124 +constdefs
   1.125 +  disj_wf         :: "('a * 'a)set => bool"
   1.126 +  "disj_wf(r) == \<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i)"
   1.127 +
   1.128 +  transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
   1.129 +  "transition_idx s T A ==
   1.130 +     LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k"
   1.131 +
   1.132 +
   1.133 +lemma transition_idx_less:
   1.134 +    "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
   1.135 +apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp) 
   1.136 +apply (simp add: transition_idx_def, blast intro: Least_le) 
   1.137 +done
   1.138 +
   1.139 +lemma transition_idx_in:
   1.140 +    "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
   1.141 +apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR 
   1.142 +            cong: conj_cong) 
   1.143 +apply (erule LeastI) 
   1.144 +done
   1.145 +
   1.146 +text{*To be equal to the union of some well-founded relations is equivalent
   1.147 +to being the subset of such a union.*}
   1.148 +lemma disj_wf:
   1.149 +     "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
   1.150 +apply (auto simp add: disj_wf_def) 
   1.151 +apply (rule_tac x="%i. T i Int r" in exI) 
   1.152 +apply (rule_tac x=n in exI) 
   1.153 +apply (force simp add: wf_Int1) 
   1.154 +done
   1.155 +
   1.156 +theorem trans_disj_wf_implies_wf:
   1.157 +  assumes transr: "trans r"
   1.158 +      and dwf:    "disj_wf(r)"
   1.159 +  shows "wf r"
   1.160 +proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
   1.161 +  assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
   1.162 +  then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
   1.163 +  have s: "!!i j. i < j ==> (s j, s i) \<in> r"
   1.164 +  proof -
   1.165 +    fix i and j::nat
   1.166 +    assume less: "i<j"
   1.167 +    thus "(s j, s i) \<in> r"
   1.168 +    proof (rule less_Suc_induct)
   1.169 +      show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc) 
   1.170 +      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"
   1.171 +        using transr by (unfold trans_def, blast) 
   1.172 +    qed
   1.173 +  qed    
   1.174 +  from dwf
   1.175 +  obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
   1.176 +    by (auto simp add: disj_wf_def)
   1.177 +  have s_in_T: "\<And>i j. i<j ==> \<exists>k. (s j, s i) \<in> T k & k<n"
   1.178 +  proof -
   1.179 +    fix i and j::nat
   1.180 +    assume less: "i<j"
   1.181 +    hence "(s j, s i) \<in> r" by (rule s [of i j]) 
   1.182 +    thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
   1.183 +  qed    
   1.184 +  have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
   1.185 +    apply (auto simp add: linorder_neq_iff)
   1.186 +    apply (blast dest: s_in_T transition_idx_less) 
   1.187 +    apply (subst insert_commute)   
   1.188 +    apply (blast dest: s_in_T transition_idx_less) 
   1.189 +    done
   1.190 +  have
   1.191 +   "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n & 
   1.192 +          (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
   1.193 +    by (rule Ramsey2) (auto intro: trless nat_infinite) 
   1.194 +  then obtain K and k 
   1.195 +    where infK: "infinite K" and less: "k < n" and
   1.196 +          allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
   1.197 +    by auto
   1.198 +  have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"
   1.199 +  proof
   1.200 +    fix m::nat
   1.201 +    let ?j = "enumerate K (Suc m)"
   1.202 +    let ?i = "enumerate K m"
   1.203 +    have jK: "?j \<in> K" by (simp add: enumerate_in_set infK) 
   1.204 +    have iK: "?i \<in> K" by (simp add: enumerate_in_set infK) 
   1.205 +    have ij: "?i < ?j" by (simp add: enumerate_step infK) 
   1.206 +    have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij 
   1.207 +      by (simp add: allk)
   1.208 +    obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" 
   1.209 +      using s_in_T [OF ij] by blast
   1.210 +    thus "(s ?j, s ?i) \<in> T k" 
   1.211 +      by (simp add: ijk [symmetric] transition_idx_in ij) 
   1.212 +  qed
   1.213 +  hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain) 
   1.214 +  thus False using wfT less by blast
   1.215 +qed
   1.216 +
   1.217  
   1.218  end