Theory Dijkstra_Shortest_Path.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.›
  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