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