src/HOL/Library/SCT_Theorem.thy
author wenzelm
Thu Jun 14 23:04:39 2007 +0200 (2007-06-14)
changeset 23394 474ff28210c0
parent 23389 aaca6a8e5414
child 23416 b73a6b72f706
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/SCT_Theorem.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 *)
     5 
     6 header ""   (* FIXME proper header *)
     7 
     8 theory SCT_Theorem
     9 imports Main Ramsey SCT_Misc SCT_Definition
    10 begin
    11 
    12 subsection {* The size change criterion SCT *}
    13 
    14 definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
    15 where
    16   "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
    17 
    18 definition is_fthread :: 
    19   "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    20 where
    21   "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
    22 
    23 definition is_desc_fthread ::
    24   "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    25 where
    26   "is_desc_fthread \<theta> mp i j = 
    27   (is_fthread \<theta> mp i j \<and>
    28   (\<exists>k\<in>{i..<j}. descat mp \<theta> k))"
    29 
    30 definition
    31   "has_fth p i j n m = 
    32   (\<exists>\<theta>. is_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
    33 
    34 definition
    35   "has_desc_fth p i j n m = 
    36   (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
    37 
    38 
    39 subsection {* Bounded graphs and threads *}
    40 
    41 definition 
    42   "bounded_scg (P::nat) (G::scg) = 
    43   (\<forall>p e p'. has_edge G p e p' \<longrightarrow> p < P \<and> p' < P)"
    44 
    45 definition
    46   "bounded_acg P ACG = 
    47   (\<forall>n G n'. has_edge ACG n G n' \<longrightarrow> n < P \<and> n' < P \<and> bounded_scg P G)"
    48   
    49 definition
    50   "bounded_mp P mp = (\<forall>i. bounded_scg P (snd (mp i)))"
    51 
    52 definition (* = finite (range \<theta>) *)
    53   "bounded_th (P::nat) n \<theta> = (\<forall>i>n. \<theta> i < P)"
    54 
    55 definition 
    56   "finite_scg (G::scg) = (\<exists>P. bounded_scg P G)"
    57 
    58 definition
    59   "finite_acg (A::acg) = (\<exists>P. bounded_acg P A)"
    60 
    61 lemma "finite (insert x A) = finite A"
    62 by simp
    63 
    64 
    65 lemma finite_scg_finite[simp]: "finite_scg (Graph G) = finite G"
    66 proof
    67   assume "finite_scg (Graph G)"
    68   thm bounded_scg_def
    69   
    70   then obtain P where bounded: "bounded_scg P (Graph G)" 
    71     by (auto simp:finite_scg_def)
    72 
    73   show "finite G"
    74   proof (rule finite_subset)
    75     from bounded 
    76     show "G \<subseteq> {0 .. P - 1} \<times> { LESS, LEQ } \<times> { 0 .. P - 1}"
    77       apply (auto simp:bounded_scg_def has_edge_def)
    78       apply force
    79       apply (case_tac "aa", auto)
    80       apply force
    81       done
    82 
    83     show "finite \<dots>"
    84       by (auto intro: finite_cartesian_product finite_atLeastAtMost)
    85   qed
    86 next
    87   assume "finite G"
    88   thus "finite_scg (Graph G)"
    89   proof induct
    90     show "finite_scg (Graph {})"
    91       unfolding finite_scg_def bounded_scg_def has_edge_def by auto
    92   next
    93     fix x G 
    94     assume "finite G" "x \<notin> G" "finite_scg (Graph G)"
    95     then obtain P
    96       where bG: "bounded_scg P (Graph G)" 
    97       by (auto simp:finite_scg_def)
    98     
    99     obtain p e p' where x: "x = (p, e, p')" by (cases x, auto)
   100     
   101     let ?Q = "max P (max (Suc p) (Suc p'))"
   102     have "P \<le> ?Q" "Suc p \<le> ?Q" "Suc p' \<le> ?Q" by auto
   103     with bG
   104     have "bounded_scg ?Q (Graph (insert x G))" 
   105       unfolding x bounded_scg_def has_edge_def
   106       apply simp
   107       apply (intro allI, elim allE)
   108       by auto
   109     thus "finite_scg (Graph (insert x G))"
   110       by (auto simp:finite_scg_def)
   111   qed
   112 qed
   113 
   114 lemma finite_acg_empty:
   115   "finite_acg (Graph {})"
   116 unfolding finite_acg_def bounded_acg_def has_edge_def
   117 by auto
   118 
   119 lemma bounded_scg_up: "bounded_scg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_scg Q G"
   120   unfolding bounded_scg_def
   121   by force
   122 
   123 lemma bounded_up: "bounded_acg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_acg Q G"
   124   unfolding bounded_acg_def 
   125   apply auto
   126   apply force+
   127   apply (rule bounded_scg_up)
   128   by auto
   129 
   130 lemma bacg_insert:
   131   assumes "bounded_acg P (Graph A)"
   132   assumes "n < P" "m < P" "bounded_scg P G"
   133   shows "bounded_acg P (Graph (insert (n, G, m) A))"
   134   using prems
   135   unfolding bounded_acg_def has_edge_def 
   136   by auto
   137 
   138 lemma finite_acg_ins:
   139   "finite_acg (Graph (insert (n,G,m) A)) = 
   140   (finite_scg G \<and> finite_acg (Graph A))" (is "?A = (?B \<and> ?C)")
   141 proof
   142   assume "?A"
   143   thus "?B \<and> ?C"
   144     unfolding finite_acg_def bounded_acg_def finite_scg_def has_edge_def
   145     by auto
   146 next
   147   assume "?B \<and> ?C"
   148   thus ?A
   149   proof
   150     assume "?B" "?C"
   151 
   152     from `?C`
   153     obtain P where bA: "bounded_acg P (Graph A)" by (auto simp:finite_acg_def)
   154     from `?B` 
   155     obtain P' where bG: "bounded_scg P' G" by (auto simp:finite_scg_def)
   156 
   157     let ?Q = "max (max P P') (max (Suc n) (Suc m))"
   158     have "P \<le> ?Q" "n < ?Q" "m < ?Q" by auto
   159     have "bounded_acg ?Q (Graph (insert (n, G, m) A))"
   160       apply (rule bacg_insert)
   161       apply (rule bounded_up)
   162       apply (rule bA)
   163       apply auto
   164       apply (rule bounded_scg_up)
   165       apply (rule bG)
   166       by auto
   167     thus "finite_acg (Graph (insert (n, G, m) A))"
   168       by (auto simp:finite_acg_def)
   169   qed
   170 qed
   171 
   172 
   173 lemma bounded_mpath:
   174   assumes "has_ipath acg mp"
   175   and "bounded_acg P acg"
   176   shows "bounded_mp P mp"
   177   using prems
   178   unfolding bounded_acg_def bounded_mp_def has_ipath_def
   179   by blast
   180 
   181 lemma bounded_th: 
   182   assumes th: "is_thread n \<theta> mp"
   183   and mp: "bounded_mp P mp"
   184   shows "bounded_th P n \<theta>"
   185   unfolding bounded_th_def
   186 proof (intro allI impI)
   187   fix i assume "n < i"
   188   
   189   from mp have "bounded_scg P (snd (mp i))" unfolding bounded_mp_def ..
   190   moreover
   191   from th `n < i` have "eqlat mp \<theta> i" unfolding is_thread_def by auto
   192   ultimately
   193   show "\<theta> i < P" unfolding bounded_scg_def by auto
   194 qed
   195 
   196 
   197 lemma finite_range:
   198   fixes f :: "nat \<Rightarrow> 'a"
   199   assumes fin: "finite (range f)"
   200   shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x"
   201 proof (rule classical)
   202   assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)"
   203   hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x"
   204     unfolding INF_nat by blast
   205   with choice
   206   have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" .
   207   then obtain j where 
   208     neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
   209 
   210   from fin have "finite (range (j o f))" 
   211     by (auto simp:comp_def)
   212   with finite_nat_bounded
   213   obtain m where "range (j o f) \<subseteq> {..<m}" by blast
   214   hence "j (f m) < m" unfolding comp_def by auto
   215 
   216   with neq[of "f m" m] show ?thesis by blast
   217 qed
   218 
   219 
   220 lemma bounded_th_infinite_visit:
   221   fixes \<theta> :: "nat sequence"
   222   assumes b: "bounded_th P n \<theta>"
   223   shows "\<exists>p. \<exists>\<^sub>\<infinity>i. \<theta> i = p" 
   224 proof -
   225   have split: "range \<theta> = (\<theta> ` {0 .. n}) \<union> (\<theta> ` {i. n < i})"
   226     (is "\<dots> = ?A \<union> ?B")
   227     unfolding image_Un[symmetric] by auto
   228 
   229   have "finite ?A" by (rule finite_imageI) auto
   230   moreover
   231   have "finite ?B"
   232   proof (rule finite_subset)
   233     from b
   234     show "?B \<subseteq> { 0 ..< P }"
   235       unfolding bounded_th_def
   236       by auto
   237     show "finite \<dots>" by auto
   238   qed
   239 
   240   ultimately have "finite (range \<theta>)"
   241     unfolding split by auto
   242 
   243   with finite_range show ?thesis .
   244 qed
   245 
   246 
   247 lemma bounded_scgcomp:
   248   "bounded_scg P A 
   249   \<Longrightarrow> bounded_scg P B 
   250   \<Longrightarrow> bounded_scg P (A * B)"
   251   unfolding bounded_scg_def
   252   by (auto simp:in_grcomp)
   253 
   254 lemma bounded_acgcomp:
   255   "bounded_acg P A 
   256   \<Longrightarrow> bounded_acg P B 
   257   \<Longrightarrow> bounded_acg P (A * B)"
   258   unfolding bounded_acg_def
   259   by (auto simp:in_grcomp intro!:bounded_scgcomp) 
   260 
   261 lemma bounded_acgpow:
   262   "bounded_acg P A
   263   \<Longrightarrow> bounded_acg P (A ^ (Suc n))"
   264   by (induct n, simp add:power_Suc) 
   265    (subst power_Suc, blast intro:bounded_acgcomp)
   266 
   267 lemma bounded_plus:
   268   assumes b: "bounded_acg P acg"
   269   shows "bounded_acg P (tcl acg)"
   270   unfolding bounded_acg_def
   271 proof (intro allI impI conjI)
   272   fix n G m
   273   assume "tcl acg \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
   274   then obtain i where "0 < i" and i: "acg ^ i \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
   275     unfolding in_tcl by auto (* FIXME: Disambiguate \<turnstile> Grammar *)
   276   from b have "bounded_acg P (acg ^ (Suc (i - 1)))"
   277     by (rule bounded_acgpow)
   278   with `0 < i` have "bounded_acg P (acg ^ i)" by simp
   279   with i
   280   show "n < P" "m < P" "bounded_scg P G"
   281     unfolding bounded_acg_def
   282     by auto
   283 qed
   284 
   285 
   286 lemma bounded_scg_def':
   287   "bounded_scg P G = (\<forall>(p,e,p')\<in>dest_graph G. p < P \<and> p' < P)"
   288   unfolding bounded_scg_def has_edge_def
   289   by auto
   290 
   291 
   292 lemma finite_bounded_scg: "finite { G. bounded_scg P G }"
   293 proof (rule finite_subset)
   294   show "{G. bounded_scg P G} \<subseteq> 
   295     Graph ` (Pow ({0 .. P - 1} \<times> UNIV \<times> {0 .. P - 1}))"
   296   proof (rule, simp)
   297     fix G 
   298     
   299     assume b: "bounded_scg P G"
   300 
   301     show "G \<in> Graph ` Pow ({0..P - Suc 0} \<times> UNIV \<times> {0..P - Suc 0})"
   302     proof (cases G)
   303       fix G' assume [simp]: "G = Graph G'"
   304       
   305       from b show ?thesis
   306         by (auto simp:bounded_scg_def' image_def)
   307     qed
   308   qed
   309 
   310   show "finite \<dots>"
   311     apply (rule finite_imageI)
   312     apply (unfold finite_Pow_iff)
   313     by (intro finite_cartesian_product finite_atLeastAtMost 
   314       finite_class.finite)
   315 qed
   316 
   317 lemma bounded_finite:
   318   assumes bounded: "bounded_acg P A"
   319   shows "finite (dest_graph A)"
   320 proof (rule finite_subset)
   321   
   322   from bounded
   323   show "dest_graph A \<subseteq> {0 .. P - 1} \<times> { G. bounded_scg P G } \<times> { 0 .. P - 1}"
   324     by (auto simp:bounded_acg_def has_edge_def) force+
   325 
   326   show "finite \<dots>"
   327     by (intro finite_cartesian_product finite_atLeastAtMost finite_bounded_scg)
   328 qed
   329 
   330 
   331 subsection {* Contraction and more *}
   332 
   333 abbreviation 
   334   "pdesc P == (fst P, prod P, end_node P)"
   335 
   336 lemma pdesc_acgplus: 
   337   assumes "has_ipath \<A> p"
   338   and "i < j"
   339   shows "has_edge (tcl \<A>) (fst (p\<langle>i,j\<rangle>)) (prod (p\<langle>i,j\<rangle>)) (end_node (p\<langle>i,j\<rangle>))"
   340   unfolding plus_paths
   341   apply (rule exI)
   342   apply (insert prems)  
   343   by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
   344 
   345 
   346 lemma combine_fthreads: 
   347   assumes range: "i < j" "j \<le> k"
   348   shows 
   349   "has_fth p i k m r =
   350   (\<exists>n. has_fth p i j m n \<and> has_fth p j k n r)" (is "?L = ?R")
   351 proof (intro iffI)
   352   assume "?L"
   353   then obtain \<theta>
   354     where "is_fthread \<theta> p i k" 
   355     and [simp]: "\<theta> i = m" "\<theta> k = r"
   356     by (auto simp:has_fth_def)
   357 
   358   with range
   359   have "is_fthread \<theta> p i j" and "is_fthread \<theta> p j k"
   360     by (auto simp:is_fthread_def)
   361   hence "has_fth p i j m (\<theta> j)" and "has_fth p j k (\<theta> j) r"
   362     by (auto simp:has_fth_def)
   363   thus "?R" by auto
   364 next
   365   assume "?R"
   366   then obtain n \<theta>1 \<theta>2
   367     where ths: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
   368     and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
   369     by (auto simp:has_fth_def)
   370 
   371   let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
   372   have "is_fthread ?\<theta> p i k"
   373     unfolding is_fthread_def
   374   proof
   375     fix l assume range: "l \<in> {i..<k}"
   376     
   377     show "eqlat p ?\<theta> l"
   378     proof (cases rule:three_cases)
   379       assume "Suc l < j"
   380       with ths range show ?thesis 
   381 	unfolding is_fthread_def Ball_def
   382 	by simp
   383     next
   384       assume "Suc l = j"
   385       hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
   386       with ths range show ?thesis 
   387 	unfolding is_fthread_def Ball_def
   388 	by simp
   389     next
   390       assume "j \<le> l"
   391       with ths range show ?thesis 
   392 	unfolding is_fthread_def Ball_def
   393 	by simp
   394     qed arith
   395   qed
   396   moreover 
   397   have "?\<theta> i = m" "?\<theta> k = r" using range by auto
   398   ultimately show "has_fth p i k m r" 
   399     by (auto simp:has_fth_def)
   400 qed 
   401 
   402 
   403 lemma desc_is_fthread:
   404   "is_desc_fthread \<theta> p i k \<Longrightarrow> is_fthread \<theta> p i k"
   405   unfolding is_desc_fthread_def
   406   by simp
   407 
   408 
   409 lemma combine_dfthreads: 
   410   assumes range: "i < j" "j \<le> k"
   411   shows 
   412   "has_desc_fth p i k m r =
   413   (\<exists>n. (has_desc_fth p i j m n \<and> has_fth p j k n r)
   414   \<or> (has_fth p i j m n \<and> has_desc_fth p j k n r))" (is "?L = ?R")
   415 proof 
   416   assume "?L"
   417   then obtain \<theta>
   418     where desc: "is_desc_fthread \<theta> p i k" 
   419     and [simp]: "\<theta> i = m" "\<theta> k = r"
   420     by (auto simp:has_desc_fth_def)
   421 
   422   hence "is_fthread \<theta> p i k"
   423     by (simp add: desc_is_fthread)
   424   with range have fths: "is_fthread \<theta> p i j" "is_fthread \<theta> p j k"
   425     unfolding is_fthread_def
   426     by auto
   427   hence hfths: "has_fth p i j m (\<theta> j)" "has_fth p j k (\<theta> j) r"
   428     by (auto simp:has_fth_def)
   429 
   430   from desc obtain l 
   431     where "i \<le> l" "l < k"
   432     and "descat p \<theta> l"
   433     by (auto simp:is_desc_fthread_def)
   434 
   435   with fths
   436   have "is_desc_fthread \<theta> p i j \<or> is_desc_fthread \<theta> p j k"
   437     unfolding is_desc_fthread_def
   438     by (cases "l < j") auto
   439   hence "has_desc_fth p i j m (\<theta> j) \<or> has_desc_fth p j k (\<theta> j) r"
   440     by (auto simp:has_desc_fth_def)
   441   with hfths show ?R
   442     by auto
   443 next
   444   assume "?R"
   445   then obtain n \<theta>1 \<theta>2
   446     where "(is_desc_fthread \<theta>1 p i j \<and> is_fthread \<theta>2 p j k)
   447     \<or> (is_fthread \<theta>1 p i j \<and> is_desc_fthread \<theta>2 p j k)"
   448     and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
   449     by (auto simp:has_fth_def has_desc_fth_def)
   450 
   451   hence ths2: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
   452     and dths: "is_desc_fthread \<theta>1 p i j \<or> is_desc_fthread \<theta>2 p j k"
   453     by (auto simp:desc_is_fthread)
   454 
   455   let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
   456   have "is_fthread ?\<theta> p i k"
   457     unfolding is_fthread_def
   458   proof
   459     fix l assume range: "l \<in> {i..<k}"
   460     
   461     show "eqlat p ?\<theta> l"
   462     proof (cases rule:three_cases)
   463       assume "Suc l < j"
   464       with ths2 range show ?thesis 
   465 	unfolding is_fthread_def Ball_def
   466 	by simp
   467     next
   468       assume "Suc l = j"
   469       hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
   470       with ths2 range show ?thesis 
   471 	unfolding is_fthread_def Ball_def
   472 	by simp
   473     next
   474       assume "j \<le> l"
   475       with ths2 range show ?thesis 
   476 	unfolding is_fthread_def Ball_def
   477 	by simp
   478     qed arith
   479   qed
   480   moreover
   481   from dths
   482   have "\<exists>l. i \<le> l \<and> l < k \<and> descat p ?\<theta> l"
   483   proof
   484     assume "is_desc_fthread \<theta>1 p i j"
   485 
   486     then obtain l where range: "i \<le> l" "l < j" and "descat p \<theta>1 l"
   487       unfolding is_desc_fthread_def Bex_def by auto
   488     hence "descat p ?\<theta> l" 
   489       by (cases "Suc l = j", auto)
   490     with `j \<le> k` and range show ?thesis 
   491       by (rule_tac x="l" in exI, auto)
   492   next
   493     assume "is_desc_fthread \<theta>2 p j k"
   494     then obtain l where range: "j \<le> l" "l < k" and "descat p \<theta>2 l"
   495       unfolding is_desc_fthread_def Bex_def by auto
   496     with `i < j` have "descat p ?\<theta> l" "i \<le> l"
   497       by auto
   498     with range show ?thesis 
   499       by (rule_tac x="l" in exI, auto)
   500   qed
   501   ultimately have "is_desc_fthread ?\<theta> p i k"
   502     by (simp add: is_desc_fthread_def Bex_def)
   503 
   504   moreover 
   505   have "?\<theta> i = m" "?\<theta> k = r" using range by auto
   506 
   507   ultimately show "has_desc_fth p i k m r" 
   508     by (auto simp:has_desc_fth_def)
   509 qed 
   510 
   511     
   512 
   513 lemma fth_single:
   514   "has_fth p i (Suc i) m n = eql (snd (p i)) m n" (is "?L = ?R")
   515 proof 
   516   assume "?L" thus "?R"
   517     unfolding is_fthread_def Ball_def has_fth_def
   518     by auto
   519 next
   520   let ?\<theta> = "\<lambda>k. if k = i then m else n"
   521   assume edge: "?R"
   522   hence "is_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
   523     unfolding is_fthread_def Ball_def
   524     by auto
   525 
   526   thus "?L"
   527     unfolding has_fth_def 
   528     by auto
   529 qed
   530 
   531 lemma desc_fth_single:
   532   "has_desc_fth p i (Suc i) m n = 
   533   dsc (snd (p i)) m n" (is "?L = ?R")
   534 proof 
   535   assume "?L" thus "?R"
   536     unfolding is_desc_fthread_def has_desc_fth_def is_fthread_def
   537     Bex_def 
   538     by (elim exE conjE) (case_tac "k = i", auto)
   539 next
   540   let ?\<theta> = "\<lambda>k. if k = i then m else n"
   541   assume edge: "?R"
   542   hence "is_desc_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
   543     unfolding is_desc_fthread_def is_fthread_def Ball_def Bex_def
   544     by auto
   545   thus "?L"
   546     unfolding has_desc_fth_def 
   547     by auto
   548 qed
   549 
   550 lemma mk_eql: "(G \<turnstile> m \<leadsto>\<^bsup>e\<^esup> n) \<Longrightarrow> eql G m n"
   551   by (cases e, auto)
   552 
   553 lemma eql_scgcomp:
   554   "eql (G * H) m r =
   555   (\<exists>n. eql G m n \<and> eql H n r)" (is "?L = ?R")
   556 proof
   557   show "?L \<Longrightarrow> ?R"
   558     by (auto simp:in_grcomp intro!:mk_eql)
   559 
   560   assume "?R"
   561   then obtain n where l: "eql G m n" and r:"eql H n r" by auto
   562   thus ?L
   563     by (cases "dsc G m n") (auto simp:in_grcomp mult_sedge_def)
   564 qed
   565 
   566 lemma desc_scgcomp:
   567   "dsc (G * H) m r =
   568   (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R")
   569 proof
   570   show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
   571 
   572   assume "?L"
   573   thus ?R
   574     by (auto simp:in_grcomp mult_sedge_def)
   575   (case_tac "e", auto, case_tac "e'", auto)
   576 qed
   577 
   578 
   579 lemma has_fth_unfold:
   580   assumes "i < j"
   581   shows "has_fth p i j m n = 
   582     (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
   583     by (rule combine_fthreads) (insert `i < j`, auto)
   584 
   585 lemma has_dfth_unfold:
   586   assumes range: "i < j"
   587   shows 
   588   "has_desc_fth p i j m r =
   589   (\<exists>n. (has_desc_fth p i (Suc i) m n \<and> has_fth p (Suc i) j n r)
   590   \<or> (has_fth p i (Suc i) m n \<and> has_desc_fth p (Suc i) j n r))"
   591   by (rule combine_dfthreads) (insert `i < j`, auto)
   592 
   593 
   594 lemma Lemma7a:
   595  "i \<le> j \<Longrightarrow> has_fth p i j m n = eql (prod (p\<langle>i,j\<rangle>)) m n"
   596 proof (induct i arbitrary: m rule:inc_induct)
   597   case base show ?case
   598     unfolding has_fth_def is_fthread_def sub_path_def
   599     by (auto simp:in_grunit one_sedge_def)
   600 next
   601   case (step i)
   602   note IH = `\<And>m. has_fth p (Suc i) j m n = 
   603   eql (prod (p\<langle>Suc i,j\<rangle>)) m n`
   604 
   605   have "has_fth p i j m n 
   606     = (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
   607     by (rule has_fth_unfold[OF `i < j`])
   608   also have "\<dots> = (\<exists>r. has_fth p i (Suc i) m r 
   609     \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
   610     by (simp only:IH)
   611   also have "\<dots> = (\<exists>r. eql (snd (p i)) m r
   612     \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
   613     by (simp only:fth_single)
   614   also have "\<dots> = eql (snd (p i) * prod (p\<langle>Suc i,j\<rangle>)) m n"
   615     by (simp only:eql_scgcomp)
   616   also have "\<dots> = eql (prod (p\<langle>i,j\<rangle>)) m n"
   617     by (simp only:prod_unfold[OF `i < j`])
   618   finally show ?case .
   619 qed
   620 
   621 
   622 lemma Lemma7b:
   623 assumes "i \<le> j"
   624 shows
   625   "has_desc_fth p i j m n = 
   626   dsc (prod (p\<langle>i,j\<rangle>)) m n"
   627 using prems
   628 proof (induct i arbitrary: m rule:inc_induct)
   629   case base show ?case
   630     unfolding has_desc_fth_def is_desc_fthread_def sub_path_def 
   631     by (auto simp:in_grunit one_sedge_def)
   632 next
   633   case (step i)
   634   thus ?case 
   635     by (simp only:prod_unfold desc_scgcomp desc_fth_single
   636     has_dfth_unfold fth_single Lemma7a) auto
   637 qed
   638 
   639 
   640 lemma descat_contract:
   641   assumes [simp]: "increasing s"
   642   shows
   643   "descat (contract s p) \<theta> i = 
   644   has_desc_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
   645   by (simp add:Lemma7b increasing_weak contract_def)
   646 
   647 lemma eqlat_contract:
   648   assumes [simp]: "increasing s"
   649   shows
   650   "eqlat (contract s p) \<theta> i = 
   651   has_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
   652   by (auto simp:Lemma7a increasing_weak contract_def)
   653 
   654 
   655 subsubsection {* Connecting threads *}
   656 
   657 definition
   658   "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
   659 
   660 
   661 lemma next_in_range:
   662   assumes [simp]: "increasing s"
   663   assumes a: "k \<in> section s i"
   664   shows "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
   665 proof -
   666   from a have "k < s (Suc i)" by simp
   667   
   668   hence "Suc k < s (Suc i) \<or> Suc k = s (Suc i)" by arith
   669   thus ?thesis
   670   proof
   671     assume "Suc k < s (Suc i)"
   672     with a have "Suc k \<in> section s i" by simp
   673     thus ?thesis ..
   674   next
   675     assume eq: "Suc k = s (Suc i)"
   676     with increasing_strict have "Suc k < s (Suc (Suc i))" by simp
   677     with eq have "Suc k \<in> section s (Suc i)" by simp
   678     thus ?thesis ..
   679   qed
   680 qed
   681 
   682 
   683 lemma connect_threads:
   684   assumes [simp]: "increasing s"
   685   assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   686   assumes fth: "is_fthread (\<theta>s i) p (s i) (s (Suc i))"
   687 
   688   shows
   689   "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   690   unfolding is_fthread_def
   691 proof 
   692   fix k assume krng: "k \<in> section s i"
   693 
   694   with fth have eqlat: "eqlat p (\<theta>s i) k" 
   695     unfolding is_fthread_def by simp
   696 
   697   from krng and next_in_range 
   698   have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
   699     by simp
   700   thus "eqlat p (connect s \<theta>s) k"
   701   proof
   702     assume "Suc k \<in> section s i"
   703     with krng eqlat show ?thesis
   704       unfolding connect_def
   705       by (simp only:section_of_known `increasing s`)
   706   next
   707     assume skrng: "Suc k \<in> section s (Suc i)"
   708     with krng have "Suc k = s (Suc i)" by auto
   709 
   710     with krng skrng eqlat show ?thesis
   711       unfolding connect_def
   712       by (simp only:section_of_known connected[symmetric] `increasing s`)
   713   qed
   714 qed
   715 
   716 
   717 lemma connect_dthreads:
   718   assumes inc[simp]: "increasing s"
   719   assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   720   assumes fth: "is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
   721 
   722   shows
   723   "is_desc_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   724   unfolding is_desc_fthread_def
   725 proof 
   726   show "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   727     apply (rule connect_threads)
   728     apply (insert fth)
   729     by (auto simp:connected is_desc_fthread_def)
   730 
   731   from fth
   732   obtain k where dsc: "descat p (\<theta>s i) k" and krng: "k \<in> section s i"
   733     unfolding is_desc_fthread_def by blast
   734   
   735   from krng and next_in_range 
   736   have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
   737     by simp
   738   hence "descat p (connect s \<theta>s) k"
   739   proof
   740     assume "Suc k \<in> section s i"
   741     with krng dsc show ?thesis unfolding connect_def
   742       by (simp only:section_of_known inc)
   743   next
   744     assume skrng: "Suc k \<in> section s (Suc i)"
   745     with krng have "Suc k = s (Suc i)" by auto
   746 
   747     with krng skrng dsc show ?thesis unfolding connect_def
   748       by (simp only:section_of_known connected[symmetric] inc)
   749   qed
   750   with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" ..
   751 qed
   752 
   753 
   754 
   755 lemma mk_inf_thread:
   756   assumes [simp]: "increasing s"
   757   assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
   758   shows "is_thread (s (Suc n)) \<theta> p"
   759   unfolding is_thread_def 
   760 proof (intro allI impI)
   761   fix j assume st: "s (Suc n) \<le> j"
   762 
   763   let ?k = "section_of s j"
   764   from in_section_of st
   765   have rs: "j \<in> section s ?k" by simp
   766 
   767   with st have "s (Suc n) < s (Suc ?k)" by simp
   768   with increasing_bij have "n < ?k" by simp
   769   with rs and fths[of ?k]
   770   show "eqlat p \<theta> j" by (simp add:is_fthread_def)
   771 qed
   772 
   773 
   774 lemma mk_inf_desc_thread:
   775   assumes [simp]: "increasing s"
   776   assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
   777   assumes fdths: "\<exists>\<^sub>\<infinity>i. is_desc_fthread \<theta> p (s i) (s (Suc i))"
   778   shows "is_desc_thread \<theta> p"
   779   unfolding is_desc_thread_def 
   780 proof (intro exI conjI)
   781 
   782   from mk_inf_thread[of s n] is_thread_def fths
   783   show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" by simp
   784 
   785   show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
   786     unfolding INF_nat
   787   proof
   788     fix i 
   789     
   790     let ?k = "section_of s i"
   791     from fdths obtain j
   792       where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))"
   793       unfolding INF_nat by auto
   794     then obtain l where "s j \<le> l" and desc: "descat p \<theta> l"
   795       unfolding is_desc_fthread_def
   796       by auto
   797 
   798     have "i < s (Suc ?k)" by (rule section_of2) simp
   799     also have "\<dots> \<le> s j"
   800       by (rule increasing_weak [OF `increasing s`]) (insert `?k < j`, arith)
   801     also note `\<dots> \<le> l`
   802     finally have "i < l" .
   803     with desc
   804     show "\<exists>l. i < l \<and> descat p \<theta> l" by blast
   805   qed
   806 qed
   807 
   808 
   809 lemma desc_ex_choice:
   810   assumes A: "((\<exists>n.\<forall>i\<ge>n. \<exists>x. P x i) \<and> (\<exists>\<^sub>\<infinity>i. \<exists>x. Q x i))"
   811   and imp: "\<And>x i. Q x i \<Longrightarrow> P x i"
   812   shows "\<exists>xs. ((\<exists>n.\<forall>i\<ge>n. P (xs i) i) \<and> (\<exists>\<^sub>\<infinity>i. Q (xs i) i))"
   813   (is "\<exists>xs. ?Ps xs \<and> ?Qs xs")
   814 proof
   815   let ?w = "\<lambda>i. (if (\<exists>x. Q x i) then (SOME x. Q x i)
   816                                  else (SOME x. P x i))"
   817 
   818   from A
   819   obtain n where P: "\<And>i. n \<le> i \<Longrightarrow> \<exists>x. P x i"
   820     by auto
   821   {
   822     fix i::'a assume "n \<le> i"
   823 
   824     have "P (?w i) i"
   825     proof (cases "\<exists>x. Q x i")
   826       case True
   827       hence "Q (?w i) i" by (auto intro:someI)
   828       with imp show "P (?w i) i" .
   829     next
   830       case False
   831       with P[OF `n \<le> i`] show "P (?w i) i" 
   832         by (auto intro:someI)
   833     qed
   834   }
   835 
   836   hence "?Ps ?w" by (rule_tac x=n in exI) auto
   837 
   838   moreover
   839   from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" ..
   840   hence "?Qs ?w" by (rule INF_mono) (auto intro:someI)
   841   ultimately
   842   show "?Ps ?w \<and> ?Qs ?w" ..
   843 qed
   844 
   845 
   846 
   847 lemma dthreads_join:
   848   assumes [simp]: "increasing s"
   849   assumes dthread: "is_desc_thread \<theta> (contract s p)"
   850   shows "\<exists>\<theta>s. desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
   851                            \<and> \<theta>s i (s i) = \<theta> i 
   852                            \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
   853                    (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
   854                            \<and> \<theta>s i (s i) = \<theta> i 
   855                            \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))"
   856     apply (rule desc_ex_choice)
   857     apply (insert dthread)
   858     apply (simp only:is_desc_thread_def)
   859     apply (simp add:eqlat_contract)
   860     apply (simp add:descat_contract)
   861     apply (simp only:has_fth_def has_desc_fth_def)
   862     by (auto simp:is_desc_fthread_def)
   863 
   864 
   865 
   866 lemma INF_drop_prefix:
   867   "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
   868   apply (auto simp:INF_nat)
   869   apply (drule_tac x = "max m n" in spec)
   870   apply (elim exE conjE)
   871   apply (rule_tac x = "na" in exI)
   872   by auto
   873 
   874 
   875 
   876 lemma contract_keeps_threads:
   877   assumes inc[simp]: "increasing s"
   878   shows "(\<exists>\<theta>. is_desc_thread \<theta> p) 
   879   \<longleftrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> (contract s p))"
   880   (is "?A \<longleftrightarrow> ?B")
   881 proof 
   882   assume "?A"
   883   then obtain \<theta> n 
   884     where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" 
   885       and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
   886     unfolding is_desc_thread_def 
   887     by auto
   888 
   889   let ?c\<theta> = "\<lambda>i. \<theta> (s i)"
   890 
   891   have "is_desc_thread ?c\<theta> (contract s p)"
   892     unfolding is_desc_thread_def
   893   proof (intro exI conjI)
   894     
   895     show "\<forall>i\<ge>n. eqlat (contract s p) ?c\<theta> i"
   896     proof (intro allI impI)
   897       fix i assume "n \<le> i"
   898       also have "i \<le> s i" 
   899 	using increasing_inc by auto
   900       finally have "n \<le> s i" .
   901 
   902       with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
   903 	unfolding is_fthread_def by auto
   904       hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   905 	unfolding has_fth_def by auto
   906       with less_imp_le[OF increasing_strict]
   907       have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   908 	by (simp add:Lemma7a)
   909       thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
   910 	by auto
   911     qed
   912 
   913     show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
   914       unfolding INF_nat 
   915     proof 
   916       fix i
   917 
   918       let ?K = "section_of s (max (s (Suc i)) n)"
   919       from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
   920 	  where "s (Suc ?K) < j" "descat p \<theta> j"
   921 	unfolding INF_nat by blast
   922       
   923       let ?L = "section_of s j"
   924       {
   925 	fix x assume r: "x \<in> section s ?L"
   926 	
   927 	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp
   928         note `s (Suc ?K) < j`
   929         also have "j < s (Suc ?L)"
   930           by (rule section_of2) simp
   931         finally have "Suc ?K \<le> ?L"
   932           by (simp add:increasing_bij)          
   933 	with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
   934 	with e1 r have "max (s (Suc i)) n < x" by simp
   935         
   936 	hence "(s (Suc i)) < x" "n < x" by auto
   937       }
   938       note range_est = this
   939       
   940       have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
   941 	unfolding is_desc_fthread_def is_fthread_def
   942       proof
   943 	show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
   944         proof 
   945           fix m assume "m\<in>section s ?L"
   946           with range_est(2) have "n < m" . 
   947           with fr show "eqlat p \<theta> m" by simp
   948         qed
   949 
   950         from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
   951 	have "j \<in> section s ?L" .
   952 
   953 	with `descat p \<theta> j`
   954 	show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
   955       qed
   956       
   957       with less_imp_le[OF increasing_strict]
   958       have a: "descat (contract s p) ?c\<theta> ?L"
   959 	unfolding contract_def Lemma7b[symmetric]
   960 	by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
   961       
   962       have "i < ?L"
   963       proof (rule classical)
   964 	assume "\<not> i < ?L" 
   965 	hence "s ?L < s (Suc i)" 
   966           by (simp add:increasing_bij)
   967 	also have "\<dots> < s ?L"
   968 	  by (rule range_est(1)) (simp add:increasing_strict)
   969 	finally show ?thesis .
   970       qed
   971       with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
   972         by blast
   973     qed
   974   qed
   975   with exI show "?B" .
   976 next
   977   assume "?B"
   978   then obtain \<theta> 
   979     where dthread: "is_desc_thread \<theta> (contract s p)" ..
   980 
   981   with dthreads_join inc 
   982   obtain \<theta>s where ths_spec:
   983     "desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
   984                   \<and> \<theta>s i (s i) = \<theta> i 
   985                   \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
   986           (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
   987                   \<and> \<theta>s i (s i) = \<theta> i 
   988                   \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" 
   989       (is "desc ?alw ?inf") 
   990     by blast
   991 
   992   then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
   993   hence connected: "\<And>i. n < i \<Longrightarrow> \<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   994     by auto
   995   
   996   let ?j\<theta> = "connect s \<theta>s"
   997   
   998   from fr ths_spec have ths_spec2:
   999       "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
  1000       "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  1001     by (auto intro:INF_mono)
  1002   
  1003   have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
  1004     by (rule connect_threads) (auto simp:connected ths_spec2)
  1005   
  1006   from ths_spec2(2)
  1007   have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  1008     unfolding INF_drop_prefix .
  1009   
  1010   hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
  1011     apply (rule INF_mono)
  1012     apply (rule connect_dthreads)
  1013     by (auto simp:connected)
  1014   
  1015   with `increasing s` p1
  1016   have "is_desc_thread ?j\<theta> p" 
  1017     by (rule mk_inf_desc_thread)
  1018   with exI show "?A" .
  1019 qed
  1020 
  1021 
  1022 lemma repeated_edge:
  1023   assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
  1024   shows "is_desc_thread (\<lambda>i. k) p"
  1025 proof-
  1026   have th: "\<forall> m. \<exists>na>m. n < na" by arith
  1027   show ?thesis using prems
  1028   unfolding is_desc_thread_def 
  1029   apply (auto)
  1030   apply (rule_tac x="Suc n" in exI, auto)
  1031   apply (rule INF_mono[where P="\<lambda>i. n < i"])
  1032   apply (simp only:INF_nat)
  1033   by (auto simp add: th)
  1034 qed
  1035 
  1036 lemma fin_from_inf:
  1037   assumes "is_thread n \<theta> p"
  1038   assumes "n < i"
  1039   assumes "i < j"
  1040   shows "is_fthread \<theta> p i j"
  1041   using prems
  1042   unfolding is_thread_def is_fthread_def 
  1043   by auto
  1044 
  1045 
  1046 subsection {* Ramsey's Theorem *}
  1047 
  1048 definition 
  1049   "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
  1050 
  1051 lemma set2pair_conv: 
  1052   fixes x y :: nat
  1053   assumes "x < y"
  1054   shows "set2pair {x, y} = (x, y)"
  1055   unfolding set2pair_def
  1056 proof (rule the_equality, simp_all only:split_conv split_paired_all)
  1057   from `x < y` show "x < y \<and> {x,y}={x,y}" by simp
  1058 next
  1059   fix a b
  1060   assume a: "a < b \<and> {x, y} = {a, b}"
  1061   hence "{a, b} = {x, y}" by simp_all
  1062   hence "(a, b) = (x, y) \<or> (a, b) = (y, x)" 
  1063     by (cases "x = y") auto
  1064   thus "(a, b) = (x, y)"
  1065   proof 
  1066     assume "(a, b) = (y, x)"
  1067     with a and `x < y`
  1068     show ?thesis by auto (* contradiction *)
  1069   qed
  1070 qed  
  1071 
  1072 definition 
  1073   "set2list = inv set"
  1074 
  1075 lemma finite_set2list: 
  1076   assumes "finite S" 
  1077   shows "set (set2list S) = S"
  1078   unfolding set2list_def 
  1079 proof (rule f_inv_f)
  1080   from `finite S` have "\<exists>l. set l = S"
  1081     by (rule finite_list)
  1082   thus "S \<in> range set"
  1083     unfolding image_def
  1084     by auto
  1085 qed
  1086 
  1087 
  1088 corollary RamseyNatpairs:
  1089   fixes S :: "'a set"
  1090     and f :: "nat \<times> nat \<Rightarrow> 'a"
  1091 
  1092   assumes "finite S"
  1093   and inS: "\<And>x y. x < y \<Longrightarrow> f (x, y) \<in> S"
  1094 
  1095   obtains T :: "nat set" and s :: "'a"
  1096   where "infinite T"
  1097     and "s \<in> S"
  1098     and "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; x < y\<rbrakk> \<Longrightarrow> f (x, y) = s"
  1099 proof -
  1100   from `finite S`
  1101   have "set (set2list S) = S" by (rule finite_set2list)
  1102   then 
  1103   obtain l where S: "S = set l" by auto
  1104   also from set_conv_nth have "\<dots> = {l ! i |i. i < length l}" .
  1105   finally have "S = {l ! i |i. i < length l}" .
  1106 
  1107   let ?s = "length l"
  1108 
  1109   from inS 
  1110   have index_less: "\<And>x y. x \<noteq> y \<Longrightarrow> index_of l (f (set2pair {x, y})) < ?s"
  1111   proof -
  1112     fix x y :: nat
  1113     assume neq: "x \<noteq> y"
  1114     have "f (set2pair {x, y}) \<in> S"
  1115     proof (cases "x < y")
  1116       case True hence "set2pair {x, y} = (x, y)"
  1117 	by (rule set2pair_conv)
  1118       with True inS
  1119       show ?thesis by simp
  1120     next
  1121       case False 
  1122       with neq have y_less: "y < x" by simp
  1123       have x:"{x,y} = {y,x}" by auto
  1124       with y_less have "set2pair {x, y} = (y, x)"
  1125 	by (simp add:set2pair_conv)
  1126       with y_less inS
  1127       show ?thesis by simp
  1128     qed
  1129 
  1130     thus "index_of l (f (set2pair {x, y})) < length l"
  1131       by (simp add: S index_of_length)
  1132   qed
  1133 
  1134   have "\<exists>Y. infinite Y \<and>
  1135     (\<exists>t. t < ?s \<and>
  1136          (\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow>
  1137                       index_of l (f (set2pair {x, y})) = t))"
  1138     by (rule Ramsey2[of "UNIV::nat set", simplified])
  1139        (auto simp:index_less)
  1140   then obtain T i
  1141     where inf: "infinite T"
  1142     and i: "i < length l"
  1143     and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
  1144     \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
  1145     by auto
  1146 
  1147   have "l ! i \<in> S" unfolding S using i
  1148     by (rule nth_mem)
  1149   moreover
  1150   have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
  1151     \<Longrightarrow> f (x, y) = l ! i"
  1152   proof -
  1153     fix x y assume "x \<in> T" "y \<in> T" "x < y"
  1154     with d have 
  1155       "index_of l (f (set2pair {x, y})) = i" by auto
  1156     with `x < y`
  1157     have "i = index_of l (f (x, y))" 
  1158       by (simp add:set2pair_conv)
  1159     with `i < length l`
  1160     show "f (x, y) = l ! i" 
  1161       by (auto intro:index_of_member[symmetric] iff:index_of_length)
  1162   qed
  1163   moreover note inf
  1164   ultimately
  1165   show ?thesis using prems
  1166     by blast
  1167 qed
  1168 
  1169 
  1170 subsection {* Main Result *}
  1171 
  1172 theorem LJA_Theorem4: 
  1173   assumes "bounded_acg P \<A>"
  1174   shows "SCT \<A> \<longleftrightarrow> SCT' \<A>"
  1175 proof
  1176   assume "SCT \<A>"
  1177   
  1178   show "SCT' \<A>"
  1179   proof (rule classical)
  1180     assume "\<not> SCT' \<A>"
  1181     
  1182     then obtain n G
  1183       where in_closure: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
  1184       and idemp: "G * G = G"
  1185       and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)"
  1186       unfolding SCT'_def no_bad_graphs_def by auto
  1187     
  1188     from in_closure obtain k
  1189       where k_pow: "\<A> ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
  1190       and "0 < k"
  1191       unfolding in_tcl by auto
  1192 	
  1193     from power_induces_path k_pow
  1194     obtain loop where loop_props:
  1195       "has_fpath \<A> loop"
  1196       "n = fst loop" "n = end_node loop"
  1197       "G = prod loop" "k = length (snd loop)" . 
  1198 
  1199     with `0 < k` and path_loop_graph
  1200     have "has_ipath \<A> (omega loop)" by blast
  1201     with `SCT \<A>` 
  1202     have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def)
  1203 
  1204     let ?s = "\<lambda>i. k * i"
  1205     let ?cp = "\<lambda>i. (n, G)"
  1206 
  1207     from loop_props have "fst loop = end_node loop" by auto
  1208     with `0 < k` `k = length (snd loop)`
  1209     have "\<And>i. (omega loop)\<langle>?s i,?s (Suc i)\<rangle> = loop"
  1210       by (rule sub_path_loop)
  1211 
  1212     with `n = fst loop` `G = prod loop` `k = length (snd loop)`
  1213     have a: "contract ?s (omega loop) = ?cp"
  1214       unfolding contract_def
  1215       by (simp add:path_loop_def split_def fst_p0)
  1216 
  1217     from `0 < k` have "increasing ?s"
  1218       by (auto simp:increasing_def)
  1219     with thread have "\<exists>\<theta>. is_desc_thread \<theta> ?cp"
  1220       unfolding a[symmetric] 
  1221       by (unfold contract_keeps_threads[symmetric])
  1222 
  1223     then obtain \<theta> where desc: "is_desc_thread \<theta> ?cp" by auto
  1224 
  1225     then obtain n where thr: "is_thread n \<theta> ?cp" 
  1226       unfolding is_desc_thread_def is_thread_def 
  1227       by auto
  1228 
  1229     have "bounded_th P n \<theta>" 
  1230     proof -
  1231       from `bounded_acg P \<A>`
  1232       have "bounded_acg P (tcl \<A>)" by (rule bounded_plus)
  1233       with in_closure have "bounded_scg P G"
  1234         unfolding bounded_acg_def by simp
  1235       hence "bounded_mp P ?cp"
  1236         unfolding bounded_mp_def by simp
  1237       with thr bounded_th 
  1238       show ?thesis by auto
  1239     qed
  1240     with bounded_th_infinite_visit
  1241     obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by blast
  1242 
  1243     then obtain i where "n < i" "\<theta> i = p" 
  1244       by (auto simp:INF_nat)
  1245 
  1246     from desc
  1247     have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i"
  1248       unfolding is_desc_thread_def by auto
  1249     then obtain j 
  1250       where "i < j" and "descat ?cp \<theta> j"
  1251       unfolding INF_nat by auto
  1252     from inf_visit obtain k where "j < k" "\<theta> k = p"
  1253       by (auto simp:INF_nat)
  1254 
  1255     from `i < j` `j < k` `n < i` thr fin_from_inf `descat ?cp \<theta> j`
  1256     have "is_desc_fthread \<theta> ?cp i k"
  1257       unfolding is_desc_fthread_def
  1258       by auto
  1259 
  1260     with `\<theta> k = p` `\<theta> i = p`
  1261     have dfth: "has_desc_fth ?cp i k p p"
  1262       unfolding has_desc_fth_def
  1263       by auto
  1264 
  1265     from `i < j` `j < k` have "i < k" by auto
  1266     hence "prod (?cp\<langle>i, k\<rangle>) = G"
  1267     proof (induct i rule:strict_inc_induct)
  1268       case base thus ?case by (simp add:sub_path_def)
  1269     next
  1270       case (step i) thus ?case
  1271 	by (simp add:sub_path_def upt_rec[of i k] idemp)
  1272     qed
  1273 
  1274     with `i < j` `j < k` dfth Lemma7b
  1275     have "dsc G p p" by auto
  1276     with no_strict_arc have False by auto
  1277     thus ?thesis ..
  1278   qed
  1279 next
  1280   assume "SCT' \<A>"
  1281 
  1282   show "SCT \<A>"
  1283   proof (rule classical)
  1284     assume "\<not> SCT \<A>"
  1285 
  1286     with SCT_def
  1287     obtain p 
  1288       where ipath: "has_ipath \<A> p"
  1289       and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)"
  1290       by auto
  1291 
  1292     from `bounded_acg P \<A>`
  1293     have "finite (dest_graph (tcl \<A>))" (is "finite ?AG")
  1294       by (intro bounded_finite bounded_plus)
  1295 
  1296     from pdesc_acgplus[OF ipath]
  1297     have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl \<A>)"
  1298       unfolding has_edge_def .
  1299       
  1300     obtain S G
  1301       where "infinite S" "G \<in> dest_graph (tcl \<A>)" 
  1302       and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow> 
  1303       pdesc (p\<langle>x,y\<rangle>) = G"
  1304       apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"])
  1305       apply (rule `finite (dest_graph (tcl \<A>))`)
  1306       by (simp only:split_conv, rule a, auto)
  1307 
  1308     obtain n H m where
  1309       G_struct: "G = (n, H, m)" by (cases G)
  1310 
  1311     let ?s = "enumerate S"
  1312     let ?q = "contract ?s p"
  1313 
  1314     note all_in_S[simp] = enumerate_in_set[OF `infinite S`]
  1315 	from `infinite S` 
  1316     have inc[simp]: "increasing ?s" 
  1317       unfolding increasing_def by (simp add:enumerate_mono)
  1318     note increasing_bij[OF this, simp]
  1319       
  1320     from ipath_contract inc ipath
  1321     have "has_ipath (tcl \<A>) ?q" .
  1322 
  1323     from all_G G_struct 
  1324     have all_H: "\<And>i. (snd (?q i)) = H"
  1325 	  unfolding contract_def 
  1326       by simp
  1327     
  1328     have loop: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
  1329       and idemp: "H * H = H"
  1330     proof - 
  1331       let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))"
  1332       
  1333       have "pdesc (p\<langle>?i,?j\<rangle>) = G"
  1334 		and "pdesc (p\<langle>?j,?k\<rangle>) = G"
  1335 		and "pdesc (p\<langle>?i,?k\<rangle>) = G"
  1336 		using all_G 
  1337 		by auto
  1338 	  
  1339       with G_struct 
  1340       have "m = end_node (p\<langle>?i,?j\<rangle>)"
  1341 				"n = fst (p\<langle>?j,?k\<rangle>)"
  1342 				and Hs:	"prod (p\<langle>?i,?j\<rangle>) = H"
  1343 				"prod (p\<langle>?j,?k\<rangle>) = H"
  1344 				"prod (p\<langle>?i,?k\<rangle>) = H"
  1345 		by auto
  1346 			
  1347       hence "m = n" by simp
  1348       thus "tcl \<A> \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
  1349 		using G_struct `G \<in> dest_graph (tcl \<A>)`
  1350 		by (simp add:has_edge_def)
  1351 	  
  1352       from sub_path_prod[of ?i ?j ?k p]      
  1353       show "H * H = H"
  1354 		unfolding Hs by simp
  1355     qed
  1356     moreover have "\<And>k. \<not>dsc H k k"
  1357     proof
  1358       fix k :: nat assume "dsc H k k"
  1359       
  1360       with all_H repeated_edge
  1361       have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast
  1362 	  with inc have "\<exists>\<theta>. is_desc_thread \<theta> p"
  1363 		by (subst contract_keeps_threads) 
  1364       with no_desc_th
  1365       show False ..
  1366     qed
  1367     ultimately 
  1368     have False
  1369       using `SCT' \<A>`[unfolded SCT'_def no_bad_graphs_def]
  1370       by blast
  1371     thus ?thesis ..
  1372   qed
  1373 qed
  1374 
  1375 
  1376 lemma LJA_apply:
  1377   assumes fin: "finite_acg A"
  1378   assumes "SCT' A"
  1379   shows "SCT A"
  1380 proof -
  1381   from fin obtain P where b: "bounded_acg P A"
  1382     unfolding finite_acg_def ..
  1383   show ?thesis using LJA_Theorem4[OF b] and `SCT' A`
  1384     by simp
  1385 qed
  1386 
  1387 end