src/HOL/SizeChange/Graphs.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30282 a16af775e08d
child 30968 10fef94f40fc
permissions -rw-r--r--
simplified method setup;
krauss@25314
     1
(*  Title:      HOL/Library/Graphs.thy
krauss@25314
     2
    ID:         $Id$
krauss@25314
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@25314
     4
*)
krauss@25314
     5
krauss@25314
     6
header {* General Graphs as Sets *}
krauss@25314
     7
krauss@25314
     8
theory Graphs
krauss@25314
     9
imports Main Misc_Tools Kleene_Algebras
krauss@25314
    10
begin
krauss@25314
    11
krauss@25314
    12
subsection {* Basic types, Size Change Graphs *}
krauss@25314
    13
krauss@25314
    14
datatype ('a, 'b) graph = 
krauss@25314
    15
  Graph "('a \<times> 'b \<times> 'a) set"
krauss@25314
    16
haftmann@25764
    17
primrec dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
krauss@25314
    18
  where "dest_graph (Graph G) = G"
krauss@25314
    19
krauss@25314
    20
lemma graph_dest_graph[simp]:
krauss@25314
    21
  "Graph (dest_graph G) = G"
krauss@25314
    22
  by (cases G) simp
krauss@25314
    23
krauss@25314
    24
lemma split_graph_all:
krauss@25314
    25
  "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
krauss@25314
    26
proof
krauss@25314
    27
  fix set
krauss@25314
    28
  assume "\<And>gr. PROP P gr"
krauss@25314
    29
  then show "PROP P (Graph set)" .
krauss@25314
    30
next
krauss@25314
    31
  fix gr
krauss@25314
    32
  assume "\<And>set. PROP P (Graph set)"
krauss@25314
    33
  then have "PROP P (Graph (dest_graph gr))" .
krauss@25314
    34
  then show "PROP P gr" by simp
krauss@25314
    35
qed
krauss@25314
    36
krauss@25314
    37
definition 
krauss@25314
    38
  has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
krauss@25314
    39
("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
krauss@25314
    40
where
krauss@25314
    41
  "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
krauss@25314
    42
krauss@25314
    43
krauss@25314
    44
subsection {* Graph composition *}
krauss@25314
    45
krauss@25314
    46
fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph  \<Rightarrow> ('n, 'e) graph"
krauss@25314
    47
where
krauss@25314
    48
  "grcomp (Graph G) (Graph H) = 
krauss@25314
    49
  Graph {(p,b,q) | p b q. 
krauss@25314
    50
  (\<exists>k e e'. (p,e,k)\<in>G \<and> (k,e',q)\<in>H \<and> b = e * e')}"
krauss@25314
    51
krauss@25314
    52
krauss@25314
    53
declare grcomp.simps[code del]
krauss@25314
    54
krauss@25314
    55
krauss@25314
    56
lemma graph_ext:
krauss@25314
    57
  assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
krauss@25314
    58
  shows "G = H"
krauss@25314
    59
  using assms
krauss@25314
    60
  by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
krauss@25314
    61
krauss@25314
    62
haftmann@25764
    63
instantiation graph :: (type, type) comm_monoid_add
haftmann@25764
    64
begin
haftmann@25764
    65
haftmann@25764
    66
definition
haftmann@25764
    67
  graph_zero_def: "0 = Graph {}" 
haftmann@25764
    68
haftmann@25764
    69
definition
haftmann@28562
    70
  graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
haftmann@25764
    71
haftmann@25764
    72
instance proof
krauss@25314
    73
  fix x y z :: "('a,'b) graph"
krauss@25314
    74
  show "x + y + z = x + (y + z)" 
krauss@25314
    75
   and "x + y = y + x" 
krauss@25314
    76
   and "0 + x = x"
haftmann@25764
    77
  unfolding graph_plus_def graph_zero_def by auto
krauss@25314
    78
qed
krauss@25314
    79
haftmann@25764
    80
end
haftmann@25764
    81
haftmann@25764
    82
instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
haftmann@25764
    83
begin
haftmann@25764
    84
haftmann@25764
    85
definition
haftmann@28562
    86
  graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
haftmann@25764
    87
haftmann@25764
    88
definition
haftmann@28562
    89
  graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
krauss@25314
    90
haftmann@25764
    91
definition
haftmann@28685
    92
  [code del]: "bot = Graph {}"
haftmann@28685
    93
haftmann@28685
    94
definition
haftmann@28685
    95
  [code del]: "top = Graph UNIV"
haftmann@28685
    96
haftmann@28685
    97
definition
haftmann@28562
    98
  [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
haftmann@25764
    99
haftmann@25764
   100
definition
haftmann@28562
   101
  [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
haftmann@25764
   102
haftmann@25764
   103
definition
haftmann@28562
   104
  Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
haftmann@25764
   105
haftmann@25764
   106
definition
haftmann@28562
   107
  Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
haftmann@25764
   108
haftmann@25764
   109
instance proof
krauss@25314
   110
  fix x y z :: "('a,'b) graph"
krauss@25314
   111
  fix A :: "('a, 'b) graph set"
krauss@25314
   112
haftmann@27682
   113
  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
krauss@25314
   114
    unfolding graph_leq_def graph_less_def
krauss@25314
   115
    by (cases x, cases y) auto
krauss@25314
   116
krauss@25314
   117
  show "x \<le> x" unfolding graph_leq_def ..
krauss@25314
   118
krauss@25314
   119
  { assume "x \<le> y" "y \<le> z" 
krauss@25314
   120
    with order_trans show "x \<le> z"
krauss@25314
   121
      unfolding graph_leq_def . }
krauss@25314
   122
krauss@25314
   123
  { assume "x \<le> y" "y \<le> x" thus "x = y" 
krauss@25314
   124
      unfolding graph_leq_def 
krauss@25314
   125
      by (cases x, cases y) simp }
krauss@25314
   126
krauss@25314
   127
  show "inf x y \<le> x" "inf x y \<le> y"
krauss@25314
   128
    unfolding inf_graph_def graph_leq_def 
krauss@25314
   129
    by auto    
krauss@25314
   130
  
krauss@25314
   131
  { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z"
krauss@25314
   132
      unfolding inf_graph_def graph_leq_def 
krauss@25314
   133
      by auto }
krauss@25314
   134
krauss@25314
   135
  show "x \<le> sup x y" "y \<le> sup x y"
krauss@25314
   136
    unfolding sup_graph_def graph_leq_def graph_plus_def by auto
krauss@25314
   137
krauss@25314
   138
  { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
krauss@25314
   139
      unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
haftmann@28685
   140
haftmann@28685
   141
  show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
haftmann@28685
   142
haftmann@28685
   143
  show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
krauss@25314
   144
  
krauss@25314
   145
  show "sup x (inf y z) = inf (sup x y) (sup x z)"
krauss@25314
   146
    unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
krauss@25314
   147
krauss@25314
   148
  { assume "x \<in> A" thus "Inf A \<le> x" 
krauss@25314
   149
      unfolding Inf_graph_def graph_leq_def by auto }
krauss@25314
   150
krauss@25314
   151
  { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
krauss@25314
   152
    unfolding Inf_graph_def graph_leq_def by auto }
krauss@25314
   153
krauss@25314
   154
  { assume "x \<in> A" thus "x \<le> Sup A" 
krauss@25314
   155
      unfolding Sup_graph_def graph_leq_def by auto }
krauss@25314
   156
krauss@25314
   157
  { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
krauss@25314
   158
    unfolding Sup_graph_def graph_leq_def by auto }
krauss@25314
   159
qed
krauss@25314
   160
haftmann@25764
   161
end
krauss@25314
   162
krauss@25314
   163
lemma in_grplus:
krauss@25314
   164
  "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
krauss@25314
   165
  by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
krauss@25314
   166
krauss@25314
   167
lemma in_grzero:
krauss@25314
   168
  "has_edge 0 p b q = False"
krauss@25314
   169
  by (simp add:graph_zero_def has_edge_def)
krauss@25314
   170
krauss@25314
   171
krauss@25314
   172
subsubsection {* Multiplicative Structure *}
krauss@25314
   173
haftmann@25764
   174
instantiation graph :: (type, times) mult_zero
haftmann@25764
   175
begin
haftmann@25764
   176
haftmann@25764
   177
definition
haftmann@28562
   178
  graph_mult_def [code del]: "G * H = grcomp G H" 
haftmann@25764
   179
haftmann@25764
   180
instance proof
krauss@25314
   181
  fix a :: "('a, 'b) graph"
krauss@25314
   182
krauss@25314
   183
  show "0 * a = 0" 
krauss@25314
   184
    unfolding graph_mult_def graph_zero_def
krauss@25314
   185
    by (cases a) (simp add:grcomp.simps)
krauss@25314
   186
  show "a * 0 = 0" 
krauss@25314
   187
    unfolding graph_mult_def graph_zero_def
krauss@25314
   188
    by (cases a) (simp add:grcomp.simps)
krauss@25314
   189
qed
krauss@25314
   190
haftmann@25764
   191
end
haftmann@25764
   192
haftmann@25764
   193
instantiation graph :: (type, one) one 
haftmann@25764
   194
begin
krauss@25314
   195
haftmann@25764
   196
definition
haftmann@25764
   197
  graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
haftmann@25764
   198
haftmann@25764
   199
instance ..
haftmann@25764
   200
haftmann@25764
   201
end
krauss@25314
   202
krauss@25314
   203
lemma in_grcomp:
krauss@25314
   204
  "has_edge (G * H) p b q
krauss@25314
   205
  = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
krauss@25314
   206
  by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def)
krauss@25314
   207
krauss@25314
   208
lemma in_grunit:
krauss@25314
   209
  "has_edge 1 p b q = (p = q \<and> b = 1)"
krauss@25314
   210
  by (auto simp:graph_one_def has_edge_def)
krauss@25314
   211
krauss@25314
   212
instance graph :: (type, semigroup_mult) semigroup_mult
krauss@25314
   213
proof
krauss@25314
   214
  fix G1 G2 G3 :: "('a,'b) graph"
krauss@25314
   215
  
krauss@25314
   216
  show "G1 * G2 * G3 = G1 * (G2 * G3)"
krauss@25314
   217
  proof (rule graph_ext, rule trans)
krauss@25314
   218
    fix p J q
krauss@25314
   219
    show "has_edge ((G1 * G2) * G3) p J q =
krauss@25314
   220
      (\<exists>G i H j I.
krauss@25314
   221
      has_edge G1 p G i
krauss@25314
   222
      \<and> has_edge G2 i H j
krauss@25314
   223
      \<and> has_edge G3 j I q
krauss@25314
   224
      \<and> J = (G * H) * I)"
krauss@25314
   225
      by (simp only:in_grcomp) blast
krauss@25314
   226
    show "\<dots> = has_edge (G1 * (G2 * G3)) p J q"
krauss@25314
   227
      by (simp only:in_grcomp mult_assoc) blast
krauss@25314
   228
  qed
krauss@25314
   229
qed
krauss@25314
   230
haftmann@25764
   231
instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
haftmann@25764
   232
begin
krauss@25314
   233
haftmann@25764
   234
primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
haftmann@25764
   235
where
haftmann@25764
   236
  "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
haftmann@25764
   237
| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
haftmann@25764
   238
haftmann@25764
   239
definition
haftmann@25764
   240
  graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)" 
haftmann@25764
   241
haftmann@25764
   242
instance proof
krauss@25314
   243
  fix a b c :: "('a, 'b) graph"
krauss@25314
   244
  
krauss@25314
   245
  show "1 * a = a" 
krauss@25314
   246
    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
krauss@25314
   247
  show "a * 1 = a"
krauss@25314
   248
    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
krauss@25314
   249
krauss@25314
   250
  show "(a + b) * c = a * c + b * c"
krauss@25314
   251
    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
krauss@25314
   252
krauss@25314
   253
  show "a * (b + c) = a * b + a * c"
krauss@25314
   254
    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
krauss@25314
   255
krauss@25314
   256
  show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
krauss@25314
   257
    by simp
krauss@25314
   258
krauss@25314
   259
  show "a + a = a" unfolding graph_plus_def by simp
krauss@25314
   260
  
krauss@25314
   261
  show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
haftmann@25764
   262
    by simp_all
krauss@25314
   263
qed
krauss@25314
   264
haftmann@25764
   265
end
haftmann@25764
   266
krauss@25314
   267
lemma graph_leqI:
krauss@25314
   268
  assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
krauss@25314
   269
  shows "G \<le> H"
krauss@25314
   270
  using assms
krauss@25314
   271
  unfolding graph_leq_def has_edge_def
krauss@25314
   272
  by auto
krauss@25314
   273
krauss@25314
   274
lemma in_graph_plusE:
krauss@25314
   275
  assumes "has_edge (G + H) n e n'"
krauss@25314
   276
  assumes "has_edge G n e n' \<Longrightarrow> P"
krauss@25314
   277
  assumes "has_edge H n e n' \<Longrightarrow> P"
krauss@25314
   278
  shows P
krauss@25314
   279
  using assms
krauss@25314
   280
  by (auto simp: in_grplus)
krauss@25314
   281
krauss@25314
   282
lemma in_graph_compE:
krauss@25314
   283
  assumes GH: "has_edge (G * H) n e n'"
krauss@25314
   284
  obtains e1 k e2 
krauss@25314
   285
  where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2"
krauss@25314
   286
  using GH
krauss@25314
   287
  by (auto simp: in_grcomp)
krauss@25314
   288
krauss@25314
   289
lemma 
krauss@25314
   290
  assumes "x \<in> S k"
krauss@25314
   291
  shows "x \<in> (\<Union>k. S k)"
krauss@25314
   292
  using assms by blast
krauss@25314
   293
krauss@25314
   294
lemma graph_union_least:
krauss@25314
   295
  assumes "\<And>n. Graph (G n) \<le> C"
krauss@25314
   296
  shows "Graph (\<Union>n. G n) \<le> C"
krauss@25314
   297
  using assms unfolding graph_leq_def
krauss@25314
   298
  by auto
krauss@25314
   299
krauss@25314
   300
lemma Sup_graph_eq:
krauss@25314
   301
  "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
krauss@25314
   302
proof (rule order_antisym)
krauss@25314
   303
  show "(SUP n. Graph (G n)) \<le> Graph (\<Union>n. G n)"
krauss@25314
   304
    by  (rule SUP_leI) (auto simp add: graph_leq_def)
krauss@25314
   305
krauss@25314
   306
  show "Graph (\<Union>n. G n) \<le> (SUP n. Graph (G n))"
krauss@25314
   307
  by (rule graph_union_least, rule le_SUPI', rule) 
krauss@25314
   308
qed
krauss@25314
   309
krauss@25314
   310
lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)"
krauss@25314
   311
  unfolding has_edge_def graph_leq_def
krauss@25314
   312
  by (cases G) simp
krauss@25314
   313
krauss@25314
   314
krauss@25314
   315
lemma Sup_graph_eq2:
krauss@25314
   316
  "(SUP n. G n) = Graph (\<Union>n. dest_graph (G n))"
krauss@25314
   317
  using Sup_graph_eq[of "\<lambda>n. dest_graph (G n)", simplified]
krauss@25314
   318
  by simp
krauss@25314
   319
krauss@25314
   320
lemma in_SUP:
krauss@25314
   321
  "has_edge (SUP x. Gs x) p b q = (\<exists>x. has_edge (Gs x) p b q)"
krauss@25314
   322
  unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
krauss@25314
   323
  by simp
krauss@25314
   324
krauss@25314
   325
instance graph :: (type, monoid_mult) kleene_by_complete_lattice
krauss@25314
   326
proof
krauss@25314
   327
  fix a b c :: "('a, 'b) graph"
krauss@25314
   328
krauss@25314
   329
  show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
krauss@25314
   330
    by (cases a, cases b) auto
krauss@25314
   331
haftmann@27682
   332
  from less_le_not_le show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" .
krauss@25314
   333
krauss@25314
   334
  show "a * star b * c = (SUP n. a * b ^ n * c)"
krauss@25314
   335
    unfolding graph_star_def
krauss@25314
   336
    by (rule graph_ext) (force simp:in_SUP in_grcomp)
krauss@25314
   337
qed
krauss@25314
   338
krauss@25314
   339
krauss@25314
   340
lemma in_star: 
krauss@25314
   341
  "has_edge (star G) a x b = (\<exists>n. has_edge (G ^ n) a x b)"
krauss@25314
   342
  by (auto simp:graph_star_def in_SUP)
krauss@25314
   343
krauss@25314
   344
lemma tcl_is_SUP:
krauss@25314
   345
  "tcl (G::('a::type, 'b::monoid_mult) graph) =
krauss@25314
   346
  (SUP n. G ^ (Suc n))"
krauss@25314
   347
  unfolding tcl_def 
krauss@25314
   348
  using star_cont[of 1 G G]
krauss@25314
   349
  by (simp add:power_Suc power_commutes)
krauss@25314
   350
krauss@25314
   351
krauss@25314
   352
lemma in_tcl: 
krauss@25314
   353
  "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
wenzelm@30282
   354
  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps power_Suc)
krauss@25314
   355
  apply (rule_tac x = "n - 1" in exI, auto)
krauss@25314
   356
  done
krauss@25314
   357
krauss@25314
   358
krauss@25314
   359
subsection {* Infinite Paths *}
krauss@25314
   360
krauss@25314
   361
types ('n, 'e) ipath = "('n \<times> 'e) sequence"
krauss@25314
   362
krauss@25314
   363
definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool"
krauss@25314
   364
where
krauss@25314
   365
  "has_ipath G p = 
krauss@25314
   366
  (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
krauss@25314
   367
krauss@25314
   368
krauss@25314
   369
subsection {* Finite Paths *}
krauss@25314
   370
krauss@25314
   371
types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
krauss@25314
   372
krauss@25314
   373
inductive  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
krauss@25314
   374
  for G :: "('n, 'e) graph"
krauss@25314
   375
where
krauss@25314
   376
  has_fpath_empty: "has_fpath G (n, [])"
krauss@25314
   377
| has_fpath_join: "\<lbrakk>G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'; has_fpath G (n', es)\<rbrakk> \<Longrightarrow> has_fpath G (n, (e, n')#es)"
krauss@25314
   378
krauss@25314
   379
definition 
krauss@25314
   380
  "end_node p = 
krauss@25314
   381
  (if snd p = [] then fst p else snd (snd p ! (length (snd p) - 1)))"
krauss@25314
   382
krauss@25314
   383
definition path_nth :: "('n, 'e) fpath \<Rightarrow> nat \<Rightarrow> ('n \<times> 'e \<times> 'n)"
krauss@25314
   384
where
krauss@25314
   385
  "path_nth p k = (if k = 0 then fst p else snd (snd p ! (k - 1)), snd p ! k)"
krauss@25314
   386
krauss@25314
   387
lemma endnode_nth:
krauss@25314
   388
  assumes "length (snd p) = Suc k"
krauss@25314
   389
  shows "end_node p = snd (snd (path_nth p k))"
krauss@25314
   390
  using assms unfolding end_node_def path_nth_def
krauss@25314
   391
  by auto
krauss@25314
   392
krauss@25314
   393
lemma path_nth_graph:
krauss@25314
   394
  assumes "k < length (snd p)"
krauss@25314
   395
  assumes "has_fpath G p"
krauss@25314
   396
  shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
krauss@25314
   397
using assms
krauss@25314
   398
proof (induct k arbitrary: p)
krauss@25314
   399
  case 0 thus ?case 
krauss@25314
   400
    unfolding path_nth_def by (auto elim:has_fpath.cases)
krauss@25314
   401
next
krauss@25314
   402
  case (Suc k p)
krauss@25314
   403
krauss@25314
   404
  from `has_fpath G p` show ?case 
krauss@25314
   405
  proof (rule has_fpath.cases)
krauss@25314
   406
    case goal1 with Suc show ?case by simp
krauss@25314
   407
  next
krauss@25314
   408
    fix n e n' es
krauss@25314
   409
    assume st: "p = (n, (e, n') # es)"
krauss@25314
   410
       "G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'"
krauss@25314
   411
       "has_fpath G (n', es)"
krauss@25314
   412
    with Suc
krauss@25314
   413
    have "(\<lambda>(n, b, a). G \<turnstile> n \<leadsto>\<^bsup>b\<^esup> a) (path_nth (n', es) k)" by simp
krauss@25314
   414
    with st show ?thesis by (cases k, auto simp:path_nth_def)
krauss@25314
   415
  qed
krauss@25314
   416
qed
krauss@25314
   417
krauss@25314
   418
lemma path_nth_connected:
krauss@25314
   419
  assumes "Suc k < length (snd p)"
krauss@25314
   420
  shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
krauss@25314
   421
  using assms
krauss@25314
   422
  unfolding path_nth_def
krauss@25314
   423
  by auto
krauss@25314
   424
krauss@25314
   425
definition path_loop :: "('n, 'e) fpath \<Rightarrow> ('n, 'e) ipath" ("omega")
krauss@25314
   426
where
krauss@25314
   427
  "omega p \<equiv> (\<lambda>i. (\<lambda>(n,e,n'). (n,e)) (path_nth p (i mod (length (snd p)))))"
krauss@25314
   428
krauss@25314
   429
lemma fst_p0: "fst (path_nth p 0) = fst p"
krauss@25314
   430
  unfolding path_nth_def by simp
krauss@25314
   431
krauss@25314
   432
lemma path_loop_connect:
krauss@25314
   433
  assumes "fst p = end_node p"
krauss@25314
   434
  and "0 < length (snd p)" (is "0 < ?l")
krauss@25314
   435
  shows "fst (path_nth p (Suc i mod (length (snd p))))
krauss@25314
   436
  = snd (snd (path_nth p (i mod length (snd p))))"
krauss@25314
   437
  (is "\<dots> = snd (snd (path_nth p ?k))")
krauss@25314
   438
proof -
krauss@25314
   439
  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
krauss@25314
   440
    by simp
krauss@25314
   441
krauss@25314
   442
  show ?thesis 
krauss@25314
   443
  proof (cases "Suc ?k < ?l")
krauss@25314
   444
    case True
krauss@25314
   445
    hence "Suc ?k \<noteq> ?l" by simp
krauss@25314
   446
    with path_nth_connected[OF True]
krauss@25314
   447
    show ?thesis
krauss@25314
   448
      by (simp add:mod_Suc)
krauss@25314
   449
  next
krauss@25314
   450
    case False 
krauss@25314
   451
    with `?k < ?l` have wrap: "Suc ?k = ?l" by simp
krauss@25314
   452
krauss@25314
   453
    hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
krauss@25314
   454
      by (simp add: mod_Suc)
krauss@25314
   455
    also from fst_p0 have "\<dots> = fst p" .
krauss@25314
   456
    also have "\<dots> = end_node p" by fact
krauss@25314
   457
    also have "\<dots> = snd (snd (path_nth p ?k))" 
krauss@25314
   458
      by (auto simp: endnode_nth wrap)
krauss@25314
   459
    finally show ?thesis .
krauss@25314
   460
  qed
krauss@25314
   461
qed
krauss@25314
   462
krauss@25314
   463
lemma path_loop_graph:
krauss@25314
   464
  assumes "has_fpath G p"
krauss@25314
   465
  and loop: "fst p = end_node p"
krauss@25314
   466
  and nonempty: "0 < length (snd p)" (is "0 < ?l")
krauss@25314
   467
  shows "has_ipath G (omega p)"
krauss@25314
   468
proof -
krauss@25314
   469
  {
krauss@25314
   470
    fix i 
krauss@25314
   471
    from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
krauss@25314
   472
      by simp
krauss@25314
   473
    from this and `has_fpath G p`
krauss@25314
   474
    have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
krauss@25314
   475
      by (rule path_nth_graph)
krauss@25314
   476
krauss@25314
   477
    from path_loop_connect[OF loop nonempty] pk_G
krauss@25314
   478
    have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
krauss@25314
   479
      unfolding path_loop_def has_edge_def split_def
krauss@25314
   480
      by simp
krauss@25314
   481
  }
krauss@25314
   482
  then show ?thesis by (auto simp:has_ipath_def)
krauss@25314
   483
qed
krauss@25314
   484
krauss@25314
   485
definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
krauss@25314
   486
where
krauss@25314
   487
  "prod p = foldr (op *) (map fst (snd p)) 1"
krauss@25314
   488
krauss@25314
   489
lemma prod_simps[simp]:
krauss@25314
   490
  "prod (n, []) = 1"
krauss@25314
   491
  "prod (n, (e,n')#es) = e * (prod (n',es))"
krauss@25314
   492
unfolding prod_def
krauss@25314
   493
by simp_all
krauss@25314
   494
krauss@25314
   495
lemma power_induces_path:
krauss@25314
   496
  assumes a: "has_edge (A ^ k) n G m"
krauss@25314
   497
  obtains p 
krauss@25314
   498
    where "has_fpath A p"
krauss@25314
   499
      and "n = fst p" "m = end_node p"
krauss@25314
   500
      and "G = prod p"
krauss@25314
   501
      and "k = length (snd p)"
krauss@25314
   502
  using a
krauss@25314
   503
proof (induct k arbitrary:m n G thesis)
krauss@25314
   504
  case (0 m n G)
krauss@25314
   505
  let ?p = "(n, [])"
krauss@25314
   506
  from 0 have "has_fpath A ?p" "m = end_node ?p" "G = prod ?p"
krauss@25314
   507
    by (auto simp:in_grunit end_node_def intro:has_fpath.intros)
krauss@25314
   508
  thus ?case using 0 by (auto simp:end_node_def)
krauss@25314
   509
next
krauss@25314
   510
  case (Suc k m n G)
krauss@25314
   511
  hence "has_edge (A * A ^ k) n G m" 
krauss@25314
   512
    by (simp add:power_Suc power_commutes)
krauss@25314
   513
  then obtain G' H j where 
krauss@25314
   514
    a_A: "has_edge A n G' j"
krauss@25314
   515
    and H_pow: "has_edge (A ^ k) j H m"
krauss@25314
   516
    and [simp]: "G = G' * H"
krauss@25314
   517
    by (auto simp:in_grcomp) 
krauss@25314
   518
krauss@25314
   519
  from H_pow and Suc
krauss@25314
   520
  obtain p
krauss@25314
   521
    where p_path: "has_fpath A p"
krauss@25314
   522
    and [simp]: "j = fst p" "m = end_node p" "H = prod p" 
krauss@25314
   523
    "k = length (snd p)"
krauss@25314
   524
    by blast
krauss@25314
   525
krauss@25314
   526
  let ?p' = "(n, (G', j)#snd p)"
krauss@25314
   527
  from a_A and p_path
krauss@25314
   528
  have "has_fpath A ?p'" "m = end_node ?p'" "G = prod ?p'"
krauss@25314
   529
    by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split)
krauss@25314
   530
  thus ?case using Suc by auto
krauss@25314
   531
qed
krauss@25314
   532
krauss@25314
   533
krauss@25314
   534
subsection {* Sub-Paths *}
krauss@25314
   535
krauss@25314
   536
definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
krauss@25314
   537
("(_\<langle>_,_\<rangle>)")
krauss@25314
   538
where
krauss@25314
   539
  "p\<langle>i,j\<rangle> =
krauss@25314
   540
  (fst (p i), map (\<lambda>k. (snd (p k), fst (p (Suc k)))) [i ..< j])"
krauss@25314
   541
krauss@25314
   542
krauss@25314
   543
lemma sub_path_is_path: 
krauss@25314
   544
  assumes ipath: "has_ipath G p"
krauss@25314
   545
  assumes l: "i \<le> j"
krauss@25314
   546
  shows "has_fpath G (p\<langle>i,j\<rangle>)"
krauss@25314
   547
  using l
krauss@25314
   548
proof (induct i rule:inc_induct)
krauss@25314
   549
  case base show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
krauss@25314
   550
next
krauss@25314
   551
  case (step i)
krauss@25314
   552
  with ipath upt_rec[of i j]
krauss@25314
   553
  show ?case
krauss@25314
   554
    by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)
krauss@25314
   555
qed
krauss@25314
   556
krauss@25314
   557
krauss@25314
   558
lemma sub_path_start[simp]:
krauss@25314
   559
  "fst (p\<langle>i,j\<rangle>) = fst (p i)"
krauss@25314
   560
  by (simp add:sub_path_def)
krauss@25314
   561
krauss@25314
   562
lemma nth_upto[simp]: "k < j - i \<Longrightarrow> [i ..< j] ! k = i + k"
krauss@25314
   563
  by (induct k) auto
krauss@25314
   564
krauss@25314
   565
lemma sub_path_end[simp]:
krauss@25314
   566
  "i < j \<Longrightarrow> end_node (p\<langle>i,j\<rangle>) = fst (p j)"
krauss@25314
   567
  by (auto simp:sub_path_def end_node_def)
krauss@25314
   568
krauss@25314
   569
lemma foldr_map: "foldr f (map g xs) = foldr (f o g) xs"
krauss@25314
   570
  by (induct xs) auto
krauss@25314
   571
krauss@25314
   572
lemma upto_append[simp]:
krauss@25314
   573
  assumes "i \<le> j" "j \<le> k"
krauss@25314
   574
  shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
krauss@25314
   575
  using assms and upt_add_eq_append[of i j "k - j"]
krauss@25314
   576
  by simp
krauss@25314
   577
krauss@25314
   578
lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
krauss@25314
   579
  = foldr (op *) (xs @ ys) (1::'a::monoid_mult)"
krauss@25314
   580
  by (induct xs) (auto simp:mult_assoc)
krauss@25314
   581
krauss@25314
   582
lemma sub_path_prod:
krauss@25314
   583
  assumes "i < j"
krauss@25314
   584
  assumes "j < k"
krauss@25314
   585
  shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
krauss@25314
   586
  using assms
krauss@25314
   587
  unfolding prod_def sub_path_def
krauss@25314
   588
  by (simp add:map_compose[symmetric] comp_def)
krauss@25314
   589
   (simp only:foldr_monoid map_append[symmetric] upto_append)
krauss@25314
   590
krauss@25314
   591
krauss@25314
   592
lemma path_acgpow_aux:
krauss@25314
   593
  assumes "length es = l"
krauss@25314
   594
  assumes "has_fpath G (n,es)"
krauss@25314
   595
  shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
krauss@25314
   596
using assms
krauss@25314
   597
proof (induct l arbitrary:n es)
krauss@25314
   598
  case 0 thus ?case
krauss@25314
   599
    by (simp add:in_grunit end_node_def) 
krauss@25314
   600
next
krauss@25314
   601
  case (Suc l n es)
krauss@25314
   602
  hence "es \<noteq> []" by auto
krauss@25314
   603
  let ?n' = "snd (hd es)"
krauss@25314
   604
  let ?es' = "tl es"
krauss@25314
   605
  let ?e = "fst (hd es)"
krauss@25314
   606
krauss@25314
   607
  from Suc have len: "length ?es' = l" by auto
krauss@25314
   608
krauss@25314
   609
  from Suc
krauss@25314
   610
  have [simp]: "end_node (n, es) = end_node (?n', ?es')"
krauss@25314
   611
    by (cases es) (auto simp:end_node_def nth.simps split:nat.split)
krauss@25314
   612
krauss@25314
   613
  from `has_fpath G (n,es)`
krauss@25314
   614
  have "has_fpath G (?n', ?es')"
krauss@25314
   615
    by (rule has_fpath.cases) (auto intro:has_fpath.intros)
krauss@25314
   616
  with Suc len
krauss@25314
   617
  have "has_edge (G ^ l) ?n' (prod (?n', ?es')) (end_node (?n', ?es'))"
krauss@25314
   618
    by auto
krauss@25314
   619
  moreover
krauss@25314
   620
  from `es \<noteq> []`
krauss@25314
   621
  have "prod (n, es) = ?e * (prod (?n', ?es'))"
krauss@25314
   622
    by (cases es) auto
krauss@25314
   623
  moreover
krauss@25314
   624
  from `has_fpath G (n,es)` have c:"has_edge G n ?e ?n'"
krauss@25314
   625
    by (rule has_fpath.cases) (insert `es \<noteq> []`, auto)
krauss@25314
   626
krauss@25314
   627
  ultimately
krauss@25314
   628
  show ?case
krauss@25314
   629
     unfolding power_Suc 
krauss@25314
   630
     by (auto simp:in_grcomp)
krauss@25314
   631
qed
krauss@25314
   632
krauss@25314
   633
krauss@25314
   634
lemma path_acgpow:
krauss@25314
   635
   "has_fpath G p
krauss@25314
   636
  \<Longrightarrow> has_edge (G ^ length (snd p)) (fst p) (prod p) (end_node p)"
krauss@25314
   637
by (cases p)
krauss@25314
   638
   (rule path_acgpow_aux[of "snd p" "length (snd p)" _ "fst p", simplified])
krauss@25314
   639
krauss@25314
   640
krauss@25314
   641
lemma star_paths:
krauss@25314
   642
  "has_edge (star G) a x b =
krauss@25314
   643
   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p)"
krauss@25314
   644
proof
krauss@25314
   645
  assume "has_edge (star G) a x b"
krauss@25314
   646
  then obtain n where pow: "has_edge (G ^ n) a x b"
krauss@25314
   647
    by (auto simp:in_star)
krauss@25314
   648
krauss@25314
   649
  then obtain p where
krauss@25314
   650
    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
krauss@25314
   651
    by (rule power_induces_path)
krauss@25314
   652
krauss@25314
   653
  thus "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
krauss@25314
   654
    by blast
krauss@25314
   655
next
krauss@25314
   656
  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
krauss@25314
   657
  then obtain p where
krauss@25314
   658
    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
krauss@25314
   659
    by blast
krauss@25314
   660
krauss@25314
   661
  hence "has_edge (G ^ length (snd p)) a x b"
krauss@25314
   662
    by (auto intro:path_acgpow)
krauss@25314
   663
krauss@25314
   664
  thus "has_edge (star G) a x b"
krauss@25314
   665
    by (auto simp:in_star)
krauss@25314
   666
qed
krauss@25314
   667
krauss@25314
   668
krauss@25314
   669
lemma plus_paths:
krauss@25314
   670
  "has_edge (tcl G) a x b =
krauss@25314
   671
   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p))"
krauss@25314
   672
proof
krauss@25314
   673
  assume "has_edge (tcl G) a x b"
krauss@25314
   674
  
krauss@25314
   675
  then obtain n where pow: "has_edge (G ^ n) a x b" and "0 < n"
krauss@25314
   676
    by (auto simp:in_tcl)
krauss@25314
   677
krauss@25314
   678
  from pow obtain p where
krauss@25314
   679
    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
krauss@25314
   680
    "n = length (snd p)"
krauss@25314
   681
    by (rule power_induces_path)
krauss@25314
   682
krauss@25314
   683
  with `0 < n`
krauss@25314
   684
  show "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p) "
krauss@25314
   685
    by blast
krauss@25314
   686
next
krauss@25314
   687
  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p
krauss@25314
   688
    \<and> 0 < length (snd p)"
krauss@25314
   689
  then obtain p where
krauss@25314
   690
    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
krauss@25314
   691
    "0 < length (snd p)"
krauss@25314
   692
    by blast
krauss@25314
   693
krauss@25314
   694
  hence "has_edge (G ^ length (snd p)) a x b"
krauss@25314
   695
    by (auto intro:path_acgpow)
krauss@25314
   696
krauss@25314
   697
  with `0 < length (snd p)`
krauss@25314
   698
  show "has_edge (tcl G) a x b"
krauss@25314
   699
    by (auto simp:in_tcl)
krauss@25314
   700
qed
krauss@25314
   701
krauss@25314
   702
krauss@25314
   703
definition
krauss@25314
   704
  "contract s p = 
krauss@25314
   705
  (\<lambda>i. (fst (p (s i)), prod (p\<langle>s i,s (Suc i)\<rangle>)))"
krauss@25314
   706
krauss@25314
   707
lemma ipath_contract:
krauss@25314
   708
  assumes [simp]: "increasing s"
krauss@25314
   709
  assumes ipath: "has_ipath G p"
krauss@25314
   710
  shows "has_ipath (tcl G) (contract s p)"
krauss@25314
   711
  unfolding has_ipath_def 
krauss@25314
   712
proof
krauss@25314
   713
  fix i
krauss@25314
   714
  let ?p = "p\<langle>s i,s (Suc i)\<rangle>"
krauss@25314
   715
krauss@25314
   716
  from increasing_strict 
krauss@25314
   717
	have "fst (p (s (Suc i))) = end_node ?p" by simp
krauss@25314
   718
  moreover
krauss@25314
   719
  from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []"
krauss@25314
   720
    by (simp add:sub_path_def)
krauss@25314
   721
  moreover
krauss@25314
   722
  from ipath increasing_weak[of s] have "has_fpath G ?p"
krauss@25314
   723
    by (rule sub_path_is_path) auto
krauss@25314
   724
  ultimately
krauss@25314
   725
  show "has_edge (tcl G) 
krauss@25314
   726
    (fst (contract s p i)) (snd (contract s p i)) (fst (contract s p (Suc i)))"
krauss@25314
   727
    unfolding contract_def plus_paths
krauss@25314
   728
    by (intro exI) auto
krauss@25314
   729
qed
krauss@25314
   730
krauss@25314
   731
lemma prod_unfold:
krauss@25314
   732
  "i < j \<Longrightarrow> prod (p\<langle>i,j\<rangle>) 
krauss@25314
   733
  = snd (p i) * prod (p\<langle>Suc i, j\<rangle>)"
krauss@25314
   734
  unfolding prod_def
krauss@25314
   735
  by (simp add:sub_path_def upt_rec[of "i" j])
krauss@25314
   736
krauss@25314
   737
krauss@25314
   738
lemma sub_path_loop:
krauss@25314
   739
  assumes "0 < k"
krauss@25314
   740
  assumes k: "k = length (snd loop)"
krauss@25314
   741
  assumes loop: "fst loop = end_node loop"
krauss@25314
   742
  shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
krauss@25314
   743
proof (rule prod_eqI)
krauss@25314
   744
  show "fst ?\<omega> = fst loop"
krauss@25314
   745
    by (auto simp:path_loop_def path_nth_def split_def k)
krauss@25314
   746
krauss@25314
   747
  show "snd ?\<omega> = snd loop"
krauss@25314
   748
  proof (rule nth_equalityI[rule_format])
krauss@25314
   749
    show leneq: "length (snd ?\<omega>) = length (snd loop)"
krauss@25314
   750
      unfolding sub_path_def k by simp
krauss@25314
   751
krauss@25314
   752
    fix j assume "j < length (snd (?\<omega>))"
krauss@25314
   753
    with leneq and k have "j < k" by simp
krauss@25314
   754
krauss@25314
   755
    have a: "\<And>i. fst (path_nth loop (Suc i mod k))
krauss@25314
   756
      = snd (snd (path_nth loop (i mod k)))"
krauss@25314
   757
      unfolding k
krauss@25314
   758
      apply (rule path_loop_connect[OF loop])
krauss@25314
   759
      using `0 < k` and k
krauss@25314
   760
      apply auto
krauss@25314
   761
      done
krauss@25314
   762
krauss@25314
   763
    from `j < k` 
krauss@25314
   764
    show "snd ?\<omega> ! j = snd loop ! j"
krauss@25314
   765
      unfolding sub_path_def
krauss@25314
   766
      apply (simp add:path_loop_def split_def add_ac)
krauss@25314
   767
      apply (simp add:a k[symmetric])
krauss@25314
   768
      apply (simp add:path_nth_def)
krauss@25314
   769
      done
krauss@25314
   770
  qed
krauss@25314
   771
qed
krauss@25314
   772
krauss@25314
   773
end