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