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