# Theory Graph

```section ‹Graphs›
theory Graph
imports Main
begin
text ‹
This theory defines a notion of graphs. A graph is a record that
contains a set of nodes ‹V› and a set of labeled edges
‹E ⊆ V×W×V›, where ‹W› are the edge labels.
›

subsection ‹Definitions›
text ‹A graph is represented by a record.›
record ('v,'w) graph =
nodes :: "'v set"
edges :: "('v × 'w × 'v) set"

text ‹In a valid graph, edges only go from nodes to nodes.›
locale valid_graph =
fixes G :: "('v,'w) graph"
assumes E_valid: "fst`edges G ⊆ nodes G"
"snd`snd`edges G ⊆ nodes G"
begin
abbreviation "V ≡ nodes G"
abbreviation "E ≡ edges G"

lemma E_validD: assumes "(v,e,v')∈E"
shows "v∈V" "v'∈V"
apply -
apply (rule subsetD[OF E_valid(1)])
using assms apply force
apply (rule subsetD[OF E_valid(2)])
using assms apply force
done

end

subsection ‹Basic operations on Graphs›

text ‹The empty graph.›
definition empty where
"empty ≡ ⦇ nodes = {}, edges = {} ⦈"
text ‹Adds a node to a graph.›
"add_node v g ≡ ⦇ nodes = insert v (nodes g), edges=edges g⦈"
text ‹Deletes a node from a graph. Also deletes all adjacent edges.›
definition delete_node where "delete_node v g ≡ ⦇
nodes = nodes g - {v},
edges = edges g ∩ (-{v})×UNIV×(-{v})
⦈"
text ‹Adds an edge to a graph.›
nodes = {v,v'} ∪ nodes g,
edges = insert (v,e,v') (edges g)
⦈"
text ‹Deletes an edge from a graph.›
definition delete_edge where "delete_edge v e v' g ≡ ⦇
nodes = nodes g, edges = edges g - {(v,e,v')} ⦈"
text ‹Successors of a node.›
definition succ :: "('v,'w) graph ⇒ 'v ⇒ ('w×'v) set"
where "succ G v ≡ {(w,v'). (v,w,v')∈edges G}"

text ‹Now follow some simplification lemmas.›
lemma empty_valid[simp]: "valid_graph empty"
unfolding empty_def by unfold_locales auto
proof -
interpret valid_graph g by fact
show ?thesis
by unfold_locales (auto dest: E_validD)
qed
lemma delete_node_valid[simp]: assumes "valid_graph g"
shows "valid_graph (delete_node v g)"
proof -
interpret valid_graph g by fact
show ?thesis
unfolding delete_node_def
by unfold_locales (auto dest: E_validD)
qed
shows "valid_graph (add_edge v e v' g)"
proof -
interpret valid_graph g by fact
show ?thesis
by unfold_locales (auto dest: E_validD)
qed
lemma delete_edge_valid[simp]: assumes "valid_graph g"
shows "valid_graph (delete_edge v e v' g)"
proof -
interpret valid_graph g by fact
show ?thesis
unfolding delete_edge_def
by unfold_locales (auto dest: E_validD)
qed

lemma succ_finite[simp, intro]: "finite (edges G) ⟹ finite (succ G v)"
unfolding succ_def
by (rule finite_subset[where B="snd`edges G"]) force+

lemma nodes_empty[simp]: "nodes empty = {}" unfolding empty_def by simp
lemma edges_empty[simp]: "edges empty = {}" unfolding empty_def by simp
lemma succ_empty[simp]: "succ empty v = {}" unfolding empty_def succ_def by auto

"nodes (add_edge v e v' g) = insert v (insert v' (nodes g))"
"edges (add_edge v e v' g) = insert (v,e,v') (edges g)"
"edges (add_node v g) = edges g"

lemma (in valid_graph) succ_subset: "succ G v ⊆ UNIV×V"
unfolding succ_def using E_valid
by (force)

subsection ‹Paths›
text ‹A path is represented by a list of adjacent edges.›
type_synonym ('v,'w) path = "('v×'w×'v) list"

context valid_graph
begin
text ‹The following predicate describes a valid path:›
fun is_path :: "'v ⇒ ('v,'w) path ⇒ 'v ⇒ bool" where
"is_path v [] v' ⟷ v=v' ∧ v'∈V" |
"is_path v ((v1,w,v2)#p) v' ⟷ v=v1 ∧ (v1,w,v2)∈E ∧ is_path v2 p v'"

lemma is_path_simps[simp, intro!]:
"is_path v [] v ⟷ v∈V"
"is_path v [(v,w,v')] v' ⟷ (v,w,v')∈E"
by (auto dest: E_validD)

lemma is_path_memb[simp]:
"is_path v p v' ⟹ v∈V ∧ v'∈V"
apply (induct p arbitrary: v)
apply (auto dest: E_validD)
done

lemma is_path_split:
"is_path v (p1@p2) v' ⟷ (∃u. is_path v p1 u ∧ is_path u p2 v')"
by (induct p1 arbitrary: v) auto

lemma is_path_split'[simp]:
"is_path v (p1@(u,w,u')#p2) v'
⟷ is_path v p1 u ∧ (u,w,u')∈E ∧ is_path u' p2 v'"
end

text ‹Set of intermediate vertices of a path. These are all vertices but
the last one. Note that, if the last vertex also occurs earlier on the path,
it is contained in ‹int_vertices›.›
definition int_vertices :: "('v,'w) path ⇒ 'v set" where
"int_vertices p ≡ set (map fst p)"

lemma int_vertices_simps[simp]:
"int_vertices [] = {}"
"int_vertices (vv#p) = insert (fst vv) (int_vertices p)"
"int_vertices (p1@p2) = int_vertices p1 ∪ int_vertices p2"

lemma (in valid_graph) int_vertices_subset:
"is_path v p v' ⟹ int_vertices p ⊆ V"
apply (induct p arbitrary: v)
apply (simp)
apply (force dest: E_validD)
done

lemma int_vertices_empty[simp]: "int_vertices p = {} ⟷ p=[]"
by (cases p) auto

subsubsection ‹Splitting Paths›
text ‹Split a path at the point where it first leaves the set ‹W›:›
lemma (in valid_graph) path_split_set:
assumes "is_path v p v'" and "v∈W" and "v'∉W"
obtains p1 p2 u w u' where
"p=p1@(u,w,u')#p2" and
"int_vertices p1 ⊆ W" and "u∈W" and "u'∉W"
using assms
proof (induct p arbitrary: v thesis)
case Nil thus ?case by auto
next
case (Cons vv p)
note [simp, intro!] = ‹v∈W› ‹v'∉W›
from Cons.prems obtain w u' where
[simp]: "vv=(v,w,u')" and
REST: "is_path u' p v'"
by (cases vv) auto

txt ‹Distinguish wether the second node ‹u'› of the path is
in ‹W›. If yes, the proposition follows by the
induction hypothesis, otherwise it is straightforward, as
the split takes place at the first edge of the path.›
{
assume A [simp, intro!]: "u'∈W"
from Cons.hyps[OF _ REST] obtain p1 uu ww uu' p2 where
"p=p1@(uu,ww,uu')#p2" "int_vertices p1 ⊆ W" "uu ∈ W" "uu' ∉ W"
by blast
with Cons.prems(1)[of "vv#p1" uu ww uu' p2] have thesis by auto
} moreover {
assume "u'∉W"
with Cons.prems(1)[of "[]" v w u' p] have thesis by auto
} ultimately show thesis by blast
qed

text ‹Split a path at the point where it first enters the set ‹W›:›
lemma (in valid_graph) path_split_set':
assumes "is_path v p v'" and "v'∈W"
obtains p1 p2 u where
"p=p1@p2" and
"is_path v p1 u" and
"is_path u p2 v'" and
"int_vertices p1 ⊆ -W" and "u∈W"
using assms
proof (cases "v∈W")
case True with that[of "[]" p] assms show ?thesis
by auto
next
case False with assms that show ?thesis
proof (induct p arbitrary: v thesis)
case Nil thus ?case by auto
next
case (Cons vv p)
note [simp, intro!] = ‹v'∈W› ‹v∉W›
from Cons.prems obtain w u' where
[simp]: "vv=(v,w,u')" and [simp]: "(v,w,u')∈E" and
REST: "is_path u' p v'"
by (cases vv) auto

txt ‹Distinguish wether the second node ‹u'› of the path is
in ‹W›. If yes, the proposition is straightforward, otherwise,
it follows by the induction hypothesis.
›
{
assume A [simp, intro!]: "u'∈W"
from Cons.prems(3)[of "[vv]" p u'] REST have ?case by auto
} moreover {
assume [simp, intro!]: "u'∉W"
from Cons.hyps[OF REST] obtain p1 p2 u'' where
[simp]: "p=p1@p2" and
"is_path u' p1 u''" and
"is_path u'' p2 v'" and
"int_vertices p1 ⊆ -W" and
"u''∈W" by blast
with Cons.prems(3)[of "vv#p1"] have ?case by auto
} ultimately show ?case by blast
qed
qed

text ‹Split a path at the point where a given vertex is first visited:›
lemma (in valid_graph) path_split_vertex:
assumes "is_path v p v'" and "u∈int_vertices p"
obtains p1 p2 where
"p=p1@p2" and
"is_path v p1 u" and
"u ∉ int_vertices p1"
using assms
proof (induct p arbitrary: v thesis)
case Nil thus ?case by auto
next
case (Cons vv p)
from Cons.prems obtain w u' where
[simp]: "vv=(v,w,u')" "v∈V" "(v,w,u')∈E" and
REST: "is_path u' p v'"
by (cases vv) auto

{
assume "u=v"
with Cons.prems(1)[of "[]" "vv#p"] have thesis by auto
} moreover {
assume [simp]: "u≠v"
with Cons.hyps(1)[OF _ REST] Cons.prems(3) obtain p1 p2 where
"p=p1@p2" "is_path u' p1 u" "u∉int_vertices p1"
by auto
with Cons.prems(1)[of "vv#p1" p2] have thesis
by auto
} ultimately show ?case by blast
qed

subsection ‹Weighted Graphs›
locale valid_mgraph = valid_graph G for G::"('v,'w::monoid_add) graph"

definition path_weight :: "('v,'w::monoid_add) path ⇒ 'w"
where "path_weight p ≡ sum_list (map (fst ∘ snd) p)"

(*
lemma path_weight_alt: "path_weight p ≡ sum_list (map (fst ∘ snd) p)"
unfolding path_weight_def foldl_conv_fold
*)

lemma path_weight_split[simp]:
"(path_weight (p1@p2)::'w::monoid_add) = path_weight p1 + path_weight p2"
unfolding path_weight_def
by (auto)

lemma path_weight_empty[simp]: "path_weight [] = 0"
unfolding path_weight_def
by auto

lemma path_weight_cons[simp]:
"(path_weight (e#p)::'w::monoid_add) = fst (snd e) + path_weight p"
unfolding path_weight_def
by (auto)

end
```