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.› definition add_node where "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.› definition add_edge where "add_edge v e v' g ≡ ⦇ 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 lemma add_node_valid[simp]: assumes "valid_graph g" shows "valid_graph (add_node v g)" proof - interpret valid_graph g by fact show ?thesis unfolding add_node_def 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 lemma add_edge_valid[simp]: assumes "valid_graph g" shows "valid_graph (add_edge v e v' g)" proof - interpret valid_graph g by fact show ?thesis unfolding add_edge_def 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 lemma nodes_add_node[simp]: "nodes (add_node v g) = insert v (nodes g)" by (simp add: add_node_def) lemma nodes_add_edge[simp]: "nodes (add_edge v e v' g) = insert v (insert v' (nodes g))" by (simp add: add_edge_def) lemma edges_add_edge[simp]: "edges (add_edge v e v' g) = insert (v,e,v') (edges g)" by (simp add: add_edge_def) lemma edges_add_node[simp]: "edges (add_node v g) = edges g" by (simp add: add_node_def) 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'" by (auto simp add: is_path_split) 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" by (auto simp add: int_vertices_def) 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 by (simp add: sum_list_foldl) *) 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